feat(abi): prove hash-chain integrity, version ordering & lineage acyclicity (Idris2) by hyperpolymath · Pull Request #173 · hyperpolymath/verisimiser

hyperpolymath · 2026-06-27T19:39:50Z

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

Tests pass — idris2 --build verisimiser-abi.ipkg builds all 8 modules clean (idris2 0.8.0); cargo/Zig surface untouched
Code is formatted — consistent with the existing Octad.idr / Proofs.idr idiom
Linter is clean — no warnings emitted by the build
No banned language patterns — Idris2 is an allowed language
No unsafe blocks without // SAFETY: — n/a
No banned functions — zero believe_me / postulate / assert_total / assert_smaller / holes (grep-verified)
SPDX license headers present on all three new modules (MPL-2.0)
No secrets, credentials, or .env files

As Applicable

ABI/FFI changes validated — src/interface/abi/ type-checks; no FFI surface change (these are proof-only modules)
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

Generated by Claude Code

…clicity Completes the ROADMAP Phase-1 "Idris2 ABI proofs" line. #168 proved sidecar isolation (Octad.idr); this adds the remaining three, each a constructive, total, hole-free module that `idris2 --build` (provable.yml's idris2-proofs job) machine-checks — zero believe_me / postulate / assert_total / holes. - HashChain.idr — provenance hash chain. Integrity by construction (`ProvChain` only extends onto its actual current tip); the runtime `replay` verifier provably accepts a correctly-linked entry (`replayOne`) and rejects a forged predecessor (`replayReject`); no link can pose as genesis (`linkHashNeverGenesis`); end-to-end intact/tampered controls. - Version.idr — temporal versions. Strict monotonicity by construction (`History` indexed by a strict lower bound => no skew, no duplicate versions); `asOf` point-in-time query + `ascending` check with concrete pos/neg controls. - Lineage.idr — lineage DAG. Every derivation strictly increases the topological index, so any path does too (`lineageIncreases`) => acyclicity (`noCycle`, `noSelfLoop`); LTE order lemmas proved from constructors (no stdlib axioms). Verified locally with idris2 0.8.0 (the estate's pinned toolchain, via echidna/scripts/install-proof-toolchains.sh): full package builds clean, and an adversarial pass confirms the type-checker REJECTS false claims (Origin at a non-zero tip, a tampered chain replaying as valid, a self-loop edge). ROADMAP Phase-1 proof line ticked; live-DB enforcement of these invariants remains TODO (a separate, larger systems change). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JdqVWGSSv36Ph8ZWvizGMp

…#174) ## Summary Clears the one pre-existing red on the estate's `governance / Language / package anti-pattern policy` check. `scripts/abi-ffi-gate.py` was the repo's **last Python file** (RSR-H4 bans Python — Julia for scripts/data, Rust for systems), and the whole-tree scanner flags it. Rather than suppress the scanner, this **ports the gate to Julia** and removes the `.py`, so the check goes green *and* the ABI↔FFI conformance gate keeps doing its job. (Follow-up to #173 — this is the cleanup of the lone pre-existing failure carried on #172/#173.) ## Changes - **`scripts/abi-ffi-gate.jl`** (new) — a 1:1 Julia port of the former Python gate (Julia PCRE maps directly onto Python `re`). Same three checks, same messages, same exit codes: 1. the Zig FFI carries no unrendered `{{...}}` template tokens; 2. every `%foreign "C:<name>"` symbol in the ABI `.idr` sources is `export fn`-ed by the Zig FFI; 3. the Idris `resultToInt` map and the Zig `Result = enum(c_int)` agree on **names and values** (`Error`/`err` unified). - **`.github/workflows/abi-ffi-gate.yml`** — the `ABI ↔ FFI structural conformance` job now installs the pinned **Julia 1.11.5** release tarball (mirroring the adjacent `zig-build` job's pinned-tarball pattern) and runs `julia scripts/abi-ffi-gate.jl`. - **`scripts/abi-ffi-gate.py`** (removed) — the last Python file in the repo. ## RSR Quality Checklist ### Required - [x] Tests pass — gate runs clean locally (julia 1.11.5); `cargo`/Zig/Idris surfaces untouched - [x] Code is formatted — idiomatic Julia - [x] Linter is clean - [x] **No banned language patterns — this PR *removes* the last Python file** (RSR-H4) - [x] No `unsafe` blocks without `// SAFETY:` — n/a - [x] No banned functions - [x] SPDX license header present on `abi-ffi-gate.jl` (MPL-2.0) - [x] No secrets, credentials, or `.env` files ### As Applicable - [x] ABI/FFI changes validated — the conformance gate's behaviour is preserved (verified below) - [ ] State files / CHANGELOG — no released-version change ## Testing Verified locally with **julia 1.11.5** against this tree: ``` # OK path is byte-identical to the Python it replaces: $ diff <(python3 abi-ffi-gate.py) <(julia abi-ffi-gate.jl) → identical ABI-FFI GATE: OK (verisimiser) — 24 ABI functions exported, 8 result codes match (exit 0) ``` Adversarial (the gate must **fail** on drift) — each returns exit 1 with the right diagnosis: | Injected drift | Result | |---|---| | `null_pointer = 4` → `9` in the Zig enum | ❌ "Result-code map differs (name or value)" | | remove an `export fn` | ❌ "1 ABI function(s) not exported by the Zig FFI" | | add a `{{PROJECT_NAME}}` token to the Zig | ❌ "Zig FFI has unrendered template tokens" | So the port is behaviour-equivalent **and** non-vacuous. ## Screenshots n/a (script + workflow) --- 🤖 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>

hyperpolymath marked this pull request as ready for review June 27, 2026 19:47

hyperpolymath merged commit b53a4c8 into main Jun 27, 2026
31 of 32 checks passed

hyperpolymath deleted the claude/verisimiser-abi-proofs branch June 27, 2026 19:48

hyperpolymath mentioned this pull request Jun 27, 2026

chore: port the ABI-FFI gate from Python to Julia (RSR-H4: no Python) #174

Merged

10 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(abi): prove hash-chain integrity, version ordering & lineage acyclicity (Idris2)#173

feat(abi): prove hash-chain integrity, version ordering & lineage acyclicity (Idris2)#173
hyperpolymath merged 1 commit into
mainfrom
claude/verisimiser-abi-proofs

hyperpolymath commented Jun 27, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jun 27, 2026

Summary

Changes

RSR Quality Checklist

Required

As Applicable

Testing

Screenshots

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants