verisimiser: make ABI/FFI/codegen provably-real + honest docs#167
Merged
Conversation
main independently landed the Idris proofs (#164), the Zig 0.14 source fix (#166), the Mustfile (#157), and MPL-2.0/CC-BY-SA licensing (#163) while PR #167 was open. This rebases onto them and keeps only what main still lacks, so the diff is now minimal and additive. Added: - .github/workflows/provable.yml — CI gate that machine-checks the non-Rust claims on every push/PR: idris2 builds the ABI package (Types/Layout/Proofs/ Foreign via verisimiser-abi.ipkg), zig builds + tests the FFI, the codegen golden is diffed, and the generated overlay is applied to a real SQLite DB. - examples/golden/ — frozen manifest + schema + committed generated overlay for the codegen-drift and sql-golden jobs. Also completes #166's Zig 0.14 fix, which corrected the source (main.zig) but left build.zig non-compiling under 0.14: - build.zig: drop the lib.version panic, the removed addInstallHeader, and the phantom bench step; add linkLibC; wire the integration tests into `zig build test`. - test/integration_test.zig: replace per-declaration `?*opaque {}` (each a distinct anonymous type, so init's result couldn't be passed to free) with a single shared opaque Handle, and fix an illegal null comparison on the already-unwrapped handle. main's main.zig (#166) is kept as-is. Verified locally against main's tree: idris2 --build clean (all 4 modules incl. Proofs), zig build test 43/43 (8 unit + 35 C-ABI integration), golden regenerates byte-identically, and the generated SQL applies cleanly to SQLite. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ
hyperpolymath
force-pushed
the
claude/sharp-cannon-038nwu
branch
from
0f86e4e to
2755503
Compare
This was referenced Jun 27, 2026
Open
hyperpolymath
added a commit
that referenced
this pull request
Jun 27, 2026
…CC-BY-SA-4.0 (#172) ## Summary Follow-up to **#167** (already merged). #167 flagged a license-classification drift "🚩 for owner (no action taken)": stray `PMPL-1.0-or-later` strings survived in prose/metadata even though this repo's canonical license is **MPL-2.0** (code/config) + **CC-BY-SA-4.0** (docs). The estate already normalised to that pair in #138/#156/#161/#163; the #156 pass flipped SPDX *header* stamps only, leaving the bodies behind. This PR clears the residue. verisimiser is **not** a PMPL carve-out repo, and `LICENSE`, `LICENSES/`, `Cargo.toml` and every SPDX header are MPL-2.0 — so the remaining PMPL prose was drift, not intent. ## Changes **Reconciled (the repo's own license declarations):** - `.machine_readable/compliance/reuse/dep5` — REUSE/DEP5 default + config stanzas `PMPL-1.0-or-later` → `MPL-2.0`; the `CC-BY-SA-4.0` docs override (last-match-wins) is kept intact. - `.well-known/ai.txt` — code-license line → MPL-2.0; dropped the `Emotional Lineage per PMPL Section 3` clause (no such obligation exists in MPL-2.0). - `.well-known/humans.txt` — `License:` → `MPL-2.0 (code) + CC-BY-SA-4.0 (docs)`. - `docs/attribution/CITATION.cff` — `license:` → `MPL-2.0`. - `.machine_readable/ai/{.cursorrules,.clinerules,.windsurfrules}` — license-policy block → MPL-2.0 canonical pair (kept the `Never AGPL-3.0` estate rule). - `.machine_readable/svc/k9/examples/{project-metadata,setup-repo}.k9.ncl` — example license string/recipe → MPL-2.0 (the scaffolding recipe no longer `curl`s a PMPL `LICENSE`). **Deliberately left untouched (not the repo's own self-declarations — flagged for owner):** - `docs/legal/EXHIBIT-A-ETHICAL-USE.txt`, `docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt` — these are *bodies of the Palimpsest-MPL license itself*, not a verisimiser license claim. Whether an MPL-2.0 repo should ship them at all is a removal decision for the owner, not a find-replace. - `contractile.just` — the `'SPDX|License|MIT|Apache|PMPL|MPL'` grep is a generic multi-license *recognizer*, not a declaration; PMPL is a valid alternative to keep matching. ## RSR Quality Checklist ### Required - [x] Tests pass — metadata/docs-only change; no code touched, `cargo` build/test surface unaffected - [x] Code is formatted — no code changed - [x] Linter is clean — no new warnings or errors - [x] No banned language patterns - [x] No `unsafe` blocks without `// SAFETY:` comments — none added - [x] No banned functions (`believe_me`, `unsafeCoerce`, `Obj.magic`, `Admitted`, `sorry`) - [x] SPDX license headers — all modified files retain their existing MPL-2.0/CC-BY-SA-4.0 headers; no new files - [x] No secrets, credentials, or `.env` files ### As Applicable - [ ] State files — no project-state/architecture change - [x] New dependencies reviewed — none added - [x] ABI/FFI consistency — unaffected by this change ## Testing Verified by inspection + `git grep`: after the change, the only remaining `PMPL`/`Palimpsest` references are the three deliberately-preserved cases above (the two license exhibits + the generic recognizer). The `dep5` `CC-BY-SA-4.0` docs override is preserved. Canonical MPL-2.0 source URL used in the k9 example was confirmed reachable (HTTP 200). ## Screenshots n/a (text-only diff) --- 🤖 Generated with [Claude Code](https://claude.com/claude-code) --- _Generated by [Claude Code](https://claude.ai/code/session_01JdqVWGSSv36Ph8ZWvizGMp)_ Co-authored-by: Claude <noreply@anthropic.com>
11 tasks
hyperpolymath
added a commit
that referenced
this pull request
Jun 27, 2026
…clicity (Idris2) (#173) ## Summary Follow-up to **#167 / #168**. The ROADMAP Phase-1 line *"Idris2 ABI proofs: sidecar isolation, hash-chain integrity, version ordering, lineage acyclicity"* was one box with four parts. #168 delivered **sidecar isolation** (`Octad.idr`). This PR delivers the remaining three as machine-checked Idris2 theorems, so the whole line can be ticked. Each module is constructive, `%default total`, and **hole-free** — `idris2 --build` (the `idris2-proofs` job in `provable.yml`) type-checks all 8 ABI modules with **zero** `believe_me` / `postulate` / `assert_total` / holes. Verified locally with **idris2 0.8.0**, the estate's pinned toolchain (provisioned via `echidna/scripts/install-proof-toolchains.sh`'s recipe). ## Changes - **`src/interface/abi/Verisimiser/ABI/HashChain.idr`** — provenance hash chain (the Provenance octad dimension). - `ProvChain` is *integrity by construction*: it can only be extended onto the chain's actual current tip, so a value is a proof every link is intact. - The runtime `replay` verifier provably **accepts** a correctly-linked entry (`replayOne`) and **rejects** a forged predecessor (`replayReject`). - `linkHashNeverGenesis`: no link hash can pose as the genesis record; `contentChangesTip`: the tip binds its payload. End-to-end intact/tampered controls. - **`src/interface/abi/Verisimiser/ABI/Version.idr`** — temporal versioning (the Temporal octad dimension). - `History` is indexed by a strict lower bound ⇒ **strict monotonicity by construction** (no version skew, no duplicate versions). - `asOf` point-in-time query + `ascending` validity check, each pinned by concrete positive **and** negative controls. - **`src/interface/abi/Verisimiser/ABI/Lineage.idr`** — lineage DAG (the Lineage octad dimension, ADR-0005). - Every derivation strictly increases the topological index, so any path does too (`lineageIncreases`) ⇒ **acyclicity**: `noCycle`, `noSelfLoop`. `LTE` order lemmas are proved from constructors (no stdlib axioms). - **`verisimiser-abi.ipkg`** — registers the three new modules (so CI type-checks them). - **`ROADMAP.adoc`** — ticks the Phase-1 Idris2-ABI-proofs line; notes the `*.idr` are abstract models of the invariants and that *live-DB enforcement* of them remains TODO. ## RSR Quality Checklist ### Required - [x] Tests pass — `idris2 --build verisimiser-abi.ipkg` builds all 8 modules clean (idris2 0.8.0); `cargo`/Zig surface untouched - [x] Code is formatted — consistent with the existing `Octad.idr` / `Proofs.idr` idiom - [x] Linter is clean — no warnings emitted by the build - [x] No banned language patterns — Idris2 is an allowed language - [x] No `unsafe` blocks without `// SAFETY:` — n/a - [x] No banned functions — **zero** `believe_me` / `postulate` / `assert_total` / `assert_smaller` / holes (grep-verified) - [x] SPDX license headers present on all three new modules (MPL-2.0) - [x] No secrets, credentials, or `.env` files ### As Applicable - [x] ABI/FFI changes validated — `src/interface/abi/` type-checks; no FFI surface change (these are proof-only modules) - [x] Documentation updated — `ROADMAP.adoc` Phase-1 proof line - [ ] State files / CHANGELOG — no released-version change ## Testing ``` $ idris2 --version # Idris 2, version 0.8.0 $ idris2 --build verisimiser-abi.ipkg 1/8 … 8/8: Building … EXIT=0 # all modules, no warnings/holes ``` Non-vacuity (adversarial): a throwaway module asserting **false** statements is **rejected** by the type-checker — `Origin : ProvChain 5` → *Mismatch 0/5*; a tampered chain claimed valid → *Mismatch Just 18 / Nothing*; `DerivedFrom 4 4` → *Mismatch 0/4*. So the theorems have teeth, mirroring #168's adversarial controls. ## Screenshots n/a (Idris2 source + proofs) --- 🤖 Generated with [Claude Code](https://claude.com/claude-code) --- _Generated by [Claude Code](https://claude.ai/code/session_01JdqVWGSSv36Ph8ZWvizGMp)_ Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this does
Turns VeriSimiser's non-Rust claims from prose into machine-checked facts, and adds a CI gate (
provable.yml) so they stay checked. This is the verisimiser slice of the "-iser family → provably-real + honest" effort (after chapeliser and typedqliser).Everything below was verified locally with a full toolchain (idris2 0.7.0, zig 0.14.0, cargo), not just asserted.
Idris2 ABI — full, hole-free proofs
src/interface/abi/Verisimiser/ABI/{Types,Layout,Foreign}.idrallidris2 --checkclean (no holes, no warnings).OctadRecord,ProvenanceEntry,DriftMeasurement,TemporalSnapshot) carries machine-checked size/alignment (CABICompliant) and per-field-offset (FieldsAligned) witnesses.alignUpis redefined asceilDiv size align * alignsoalignUpCorrectbecomes unconditional.checkCABI,offsetInBounds(false for an arbitrary field),verifyLayout,calcStructSize,PlatformLayout/verifyAllPlatforms— each with a NOTE explaining why. The concrete, checkable*Validinstances remain.Zig FFI — builds + tests green
cd src/interface/ffi && zig build test→ 43/43 tests pass (8 unit + 35 C-ABI integration through the compiledlibverisimiser.so);zig buildproduces.so+.a.build.zigfor Zig 0.14 (dropped thelib.versionpanic + the missingaddInstallHeader; addedlinkLibCsince the impl usesstd.heap.c_allocator; wired integration tests intozig build test).Handle/DbConnection:extern struct→struct(they hold astd.mem.Allocator, which has no C layout; C only ever sees them behind a pointer).?*opaque {}(now one shared opaqueHandletype).Codegen golden + CI
examples/golden/: frozen manifest + schema + committed generated overlay (deterministic — regenerates byte-identically)..github/workflows/provable.yml(4 jobs, SHA-pinned actions, timeouts on all):idris2-proofs—idris2 --checkthe ABIzig-ffi—zig build test+zig buildcodegen-drift— regenerate golden and diffsql-golden— apply the generated overlay to a real SQLite DB; assert every sidecar table + enrichment view builds and is queryable (the views useROW_NUMBER() OVER (…), so this is a real validity check)The Rust CLI stays covered by the existing
rust-ci.yml;cargo testis green locally too.Honesty docs
docs/developer/ABI-FFI-README.adoc— it was an unrendered RSR template full of{{project}}placeholders, wrong paths, banned-language bindings, and fictional Idris commands (%runElab verifyABI,idris2 --cg c-header). Now describes the real, proven contract.README/ROADMAP/EXPLAINME/STATE.a2ml: mark what is machine-checked vs aspirational and point toprovable.yml. ROADMAP's two relevant Phase-1 items are annotated as partial (sidecar-isolation + layout proofs done; hash-chain/version/lineage proofs and live DB interception still TODO) rather than over-ticked.🚩 Flag for owner (no action taken)
.claude/CLAUDE.mddeclares this repo PMPL-1.0-or-later, but every actual file (Cargo.tomllicense-file, all SPDX headers,LICENSE) is MPL-2.0, and verisimiser is not one of the three PMPL carve-out repos (palimpsest-license / palimpsest-plasma / consent-aware-http). Per the estate license policy this sole-owner repo should be MPL-2.0, so theCLAUDE.mdline looks like the drift. I changed nothing license-related — new files I authored carry MPL-2.0 to match the repo's actual classification. Surfacing only; your call.Verification summary
idris2 --checkTypes/Layout/Foreignzig build testcargo test🤖 Generated with Claude Code
https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ
Generated by Claude Code