Skip to content

Commit b53a4c8

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(abi): prove hash-chain integrity, version ordering & lineage acyclicity (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>
1 parent 5c1c44c commit b53a4c8

5 files changed

Lines changed: 359 additions & 1 deletion

File tree

‎ROADMAP.adoc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
* [ ] **Constraints** / drift detection — read-path observer; eight categories (ADR-0003)
2424
* [x] **Constraints** category 1 of 8: Temporal drift detector (V-L1-E2 / #49)
2525
* [ ] **Constraints** categories 2–8 of 8: Structural, Semantic, Statistical, Referential, Provenance, Spatial, Embedding
26-
* [ ] Idris2 ABI proofs: sidecar isolation, hash-chain integrity, version ordering, lineage acyclicity
26+
* [x] Idris2 ABI proofs: sidecar isolation (`Octad`), hash-chain integrity (`HashChain`), version ordering (`Version`), lineage acyclicity (`Lineage`) — machine-checked by `provable.yml` (the `*.idr` are abstract models of the invariants; live-DB enforcement of them is still TODO below)
2727
* [ ] Zig FFI bridge: database connection, sidecar operations, VCL-total queries
2828
* [ ] End-to-end test: PostgreSQL → verisimiser concerns → VCL-total query
2929

‎src/interface/abi/Verisimiser/ABI/HashChain.idr‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Provenance hash-chain integrity for VeriSimiser.
5+
|||
6+
||| The Provenance octad dimension is a hash chain (ROADMAP Phase 1 — a write-path
7+
||| observer with a SHA-256 hash chain): every entry records the hash of its
8+
||| predecessor, so tampering with an earlier entry breaks every hash downstream.
9+
||| This module models that chain and proves its integrity properties:
10+
|||
11+
||| 1. Integrity by construction — `ProvChain` can only be extended by an entry
12+
||| that links onto the chain's *current* tip, so a `ProvChain t` value is a
13+
||| proof that every link is intact.
14+
||| 2. The runtime replay verifier accepts a correctly-linked entry
15+
||| (`replayOne`) and rejects a forged predecessor link (`replayReject`).
16+
||| 3. No link can masquerade as the genesis record (`linkHashNeverGenesis`),
17+
||| and changing the hashed content changes the tip (`contentChangesTip`) —
18+
||| so the chain genuinely binds its contents.
19+
module Verisimiser.ABI.HashChain
20+
21+
import Verisimiser.ABI.Types
22+
import Data.Nat
23+
24+
%default total
25+
26+
||| Integer tag for the operation recorded in a provenance entry.
27+
public export
28+
opTag : ProvenanceOperation -> Nat
29+
opTag Create = 0
30+
opTag Update = 1
31+
opTag Delete = 2
32+
opTag Transform = 3
33+
34+
||| The tip hash of an empty provenance log.
35+
public export
36+
genesisHash : Nat
37+
genesisHash = 0
38+
39+
||| Deterministic modelled digest of a new link: folds the predecessor tip with
40+
||| the operation tag and the content digest. The leading `S` makes every link
41+
||| hash non-zero, so no link can be confused with `genesisHash`.
42+
public export
43+
linkHash : (prev : Nat) -> (op : ProvenanceOperation) -> (content : Nat) -> Nat
44+
linkHash prev op content = S (prev + opTag op + content)
45+
46+
||| A provenance hash chain indexed by its current tip hash.
47+
|||
48+
||| `Append` forces the new entry to chain onto the chain's *actual* current tip,
49+
||| and the resulting tip is `linkHash` of that entry. A value of `ProvChain t` is
50+
||| therefore a proof that every link is intact: integrity by construction.
51+
public export
52+
data ProvChain : (tip : Nat) -> Type where
53+
||| The empty log: its tip is `genesisHash` (= 0). Written as the literal `0`
54+
||| because a bare lowercase `genesisHash` in an index position would be
55+
||| auto-bound as a fresh implicit (inhabiting every tip and silently voiding
56+
||| the integrity guarantee).
57+
Origin : ProvChain 0
58+
Append : (op : ProvenanceOperation) -> (content : Nat) ->
59+
ProvChain prev -> ProvChain (linkHash prev op content)
60+
61+
||| A stored provenance entry as it appears on disk / over the FFI: the operation,
62+
||| the content digest, and the predecessor hash the writer *recorded*.
63+
public export
64+
record StoredLink where
65+
constructor MkLink
66+
op : ProvenanceOperation
67+
content : Nat
68+
recPrev : Nat
69+
70+
||| Runtime verifier: replay stored links from a starting tip, checking that each
71+
||| entry's recorded predecessor hash matches the running tip. Returns the final
72+
||| tip if intact, `Nothing` at the first broken link.
73+
public export
74+
replay : (tip : Nat) -> List StoredLink -> Maybe Nat
75+
replay tip [] = Just tip
76+
replay tip (MkLink op content recPrev :: rest) =
77+
if recPrev == tip
78+
then replay (linkHash tip op content) rest
79+
else Nothing
80+
81+
--------------------------------------------------------------------------------
82+
-- Verifier soundness lemmas (general, not just concrete witnesses)
83+
--------------------------------------------------------------------------------
84+
85+
||| `==` on `Nat` is reflexive — needed to discharge the "predecessor matches the
86+
||| running tip" branch of `replay` for an arbitrary tip.
87+
eqNatRefl : (n : Nat) -> (n == n) = True
88+
eqNatRefl 0 = Refl
89+
eqNatRefl (S k) = eqNatRefl k
90+
91+
||| The verifier ACCEPTS a correctly-linked entry: when the recorded predecessor
92+
||| equals the current tip, replay advances the tip by `linkHash`.
93+
export
94+
replayOne : (tip : Nat) -> (op : ProvenanceOperation) -> (content : Nat) ->
95+
replay tip [MkLink op content tip] = Just (linkHash tip op content)
96+
replayOne tip op content = rewrite eqNatRefl tip in Refl
97+
98+
||| The verifier REJECTS a forged link: when the recorded predecessor differs from
99+
||| the current tip, replay fails at that entry. (Non-vacuous tamper detection.)
100+
export
101+
replayReject : (tip, bad : Nat) -> (op : ProvenanceOperation) -> (content : Nat) ->
102+
(bad == tip) = False ->
103+
replay tip [MkLink op content bad] = Nothing
104+
replayReject tip bad op content noteq = rewrite noteq in Refl
105+
106+
--------------------------------------------------------------------------------
107+
-- Anti-forgery properties of the hash itself
108+
--------------------------------------------------------------------------------
109+
110+
||| No link hash can equal the genesis hash, so a forged entry can never pose as
111+
||| the start of the chain.
112+
export
113+
linkHashNeverGenesis : (prev : Nat) -> (op : ProvenanceOperation) -> (content : Nat) ->
114+
Not (linkHash prev op content = 0)
115+
linkHashNeverGenesis prev op content Refl impossible
116+
117+
||| The tip binds the hashed content: distinct content under the same predecessor
118+
||| and operation yields a distinct tip (a concrete, non-vacuous witness that the
119+
||| chain is not blind to its payload).
120+
export
121+
contentChangesTip : Not (linkHash 0 Create 1 = linkHash 0 Create 2)
122+
contentChangesTip Refl impossible
123+
124+
--------------------------------------------------------------------------------
125+
-- Concrete end-to-end controls
126+
--------------------------------------------------------------------------------
127+
128+
||| A correctly-linked two-entry chain replays from genesis to its computed tip.
129+
||| (genesis = 0; first tip = linkHash 0 Create 10 = S (0+0+10) = 11;
130+
||| second tip = linkHash 11 Update 5 = S (11+1+5) = 18.)
131+
export
132+
intactChainReplays :
133+
replay 0 [MkLink Create 10 0, MkLink Update 5 11] = Just 18
134+
intactChainReplays = Refl
135+
136+
||| Tampering with the second entry's recorded predecessor (12 instead of 11)
137+
||| makes replay fail — the end-to-end negative control.
138+
export
139+
tamperedChainFails :
140+
replay 0 [MkLink Create 10 0, MkLink Update 5 12] = Nothing
141+
tamperedChainFails = Refl

‎src/interface/abi/Verisimiser/ABI/Lineage.idr‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Lineage acyclicity for VeriSimiser.
5+
|||
6+
||| The Lineage octad dimension is a DAG: "what was derived from what" (ROADMAP
7+
||| Phase 1, ADR-0005 — acyclic edges enforced via recursive CTE). This module
8+
||| models lineage as edges over a topological index and proves the *defining*
9+
||| invariant — the lineage graph is acyclic — as a genuine theorem, not a
10+
||| runtime check:
11+
|||
12+
||| 1. A derivation edge always moves to a strictly greater topological index
13+
||| (`DerivedFrom`), so a derived node is never its own source.
14+
||| 2. Any lineage *path* (transitive derivation) strictly increases the index
15+
||| (`lineageIncreases`).
16+
||| 3. Therefore no node lies in its own lineage — there are no cycles
17+
||| (`noCycle`), and in particular no self-loops (`noSelfLoop`).
18+
|||
19+
||| The `LTE` helper lemmas are proved here from the constructors directly, so the
20+
||| module depends on nothing that could hide an axiom.
21+
module Verisimiser.ABI.Lineage
22+
23+
import Verisimiser.ABI.Types
24+
import Data.Nat
25+
26+
%default total
27+
28+
--------------------------------------------------------------------------------
29+
-- Order lemmas (proved constructively from LTE's constructors)
30+
--------------------------------------------------------------------------------
31+
32+
||| Weakening on the right: `n <= m` implies `n <= S m`.
33+
lteUp : LTE n m -> LTE n (S m)
34+
lteUp LTEZero = LTEZero
35+
lteUp (LTESucc p) = LTESucc (lteUp p)
36+
37+
||| Strip a successor on the left: `S n <= m` implies `n <= m`.
38+
lteDownLeft : LTE (S n) m -> LTE n m
39+
lteDownLeft (LTESucc p) = lteUp p
40+
41+
||| Transitivity of `<=`.
42+
lteChain : LTE a b -> LTE b c -> LTE a c
43+
lteChain LTEZero _ = LTEZero
44+
lteChain (LTESucc p) (LTESucc q) = LTESucc (lteChain p q)
45+
46+
||| Transitivity of strict `<` (recall `LT a b = LTE (S a) b`).
47+
ltChain : LT a b -> LT b c -> LT a c
48+
ltChain ab bc = lteChain ab (lteDownLeft bc)
49+
50+
||| No natural is strictly less than itself — `S n <= n` is uninhabited.
51+
ltIrreflexive : LT n n -> Void
52+
ltIrreflexive (LTESucc p) = ltIrreflexive p
53+
54+
--------------------------------------------------------------------------------
55+
-- Lineage model
56+
--------------------------------------------------------------------------------
57+
58+
||| A single derivation edge: `dst` was derived from `src`. Well-formed exactly
59+
||| when the derived node has a strictly greater topological index than its
60+
||| source — this strict-decrease-toward-roots discipline is what makes the graph
61+
||| a DAG.
62+
public export
63+
data DerivedFrom : (src, dst : Nat) -> Type where
64+
Derive : LT src dst -> DerivedFrom src dst
65+
66+
||| A lineage path: the transitive closure of derivation. `src` is (transitively)
67+
||| an ancestor of `dst`.
68+
public export
69+
data Lineage : (src, dst : Nat) -> Type where
70+
||| One derivation step.
71+
Direct : DerivedFrom src dst -> Lineage src dst
72+
||| Compose a step with a longer tail.
73+
Then : DerivedFrom src mid -> Lineage mid dst -> Lineage src dst
74+
75+
--------------------------------------------------------------------------------
76+
-- Acyclicity theorems
77+
--------------------------------------------------------------------------------
78+
79+
||| Every lineage path strictly increases the topological index.
80+
export
81+
lineageIncreases : Lineage src dst -> LT src dst
82+
lineageIncreases (Direct (Derive lt)) = lt
83+
lineageIncreases (Then (Derive lt) rest) = ltChain lt (lineageIncreases rest)
84+
85+
||| ACYCLICITY (the defining invariant): no node lies in its own lineage. If it
86+
||| did, the path would force `LT n n`, which is impossible.
87+
export
88+
noCycle : Not (Lineage n n)
89+
noCycle l = ltIrreflexive (lineageIncreases l)
90+
91+
||| In particular there are no self-loops: a node is never directly derived from
92+
||| itself.
93+
export
94+
noSelfLoop : Not (DerivedFrom n n)
95+
noSelfLoop (Derive lt) = ltIrreflexive lt
96+
97+
||| Non-vacuity: genuine derivations do exist (0 -> 1 is a well-formed edge), so
98+
||| `DerivedFrom` is not the empty relation.
99+
export
100+
derivationsExist : DerivedFrom 0 1
101+
derivationsExist = Derive (LTESucc LTEZero)
102+
103+
||| Non-vacuity: multi-hop lineage exists (0 -> 1 -> 2), so the acyclicity result
104+
||| above is not vacuously true over an empty path space.
105+
export
106+
lineageExists : Lineage 0 2
107+
lineageExists = Then (Derive (LTESucc LTEZero)) (Direct (Derive (LTESucc (LTESucc LTEZero))))

‎src/interface/abi/Verisimiser/ABI/Version.idr‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Temporal version ordering for VeriSimiser.
5+
|||
6+
||| The Temporal octad dimension keeps a value's version history and answers
7+
||| point-in-time ("as-of") queries (ROADMAP Phase 1 — `verisimdb_temporal_versions`).
8+
||| This module proves the defining invariants:
9+
|||
10+
||| 1. Strict monotonicity by construction — a `History` can only be extended by
11+
||| a snapshot whose version strictly exceeds the previous one, so there is no
12+
||| version skew and no duplicate versions.
13+
||| 2. A runtime `asOf` query and an `ascending` validity check, each pinned by
14+
||| concrete positive and negative controls (the controls are non-vacuous: the
15+
||| checks really do separate good histories from bad ones).
16+
module Verisimiser.ABI.Version
17+
18+
import Verisimiser.ABI.Types
19+
import Data.Nat
20+
21+
%default total
22+
23+
||| A versioned snapshot: a logical version number and an (abstract) value digest.
24+
public export
25+
record Snapshot where
26+
constructor At
27+
version : Nat
28+
value : Nat
29+
30+
||| A version history with strictly increasing version numbers, indexed by a
31+
||| strict lower bound that the head snapshot's version must exceed.
32+
|||
33+
||| Being able to *construct* a `History above` is itself a proof that the whole
34+
||| history is strictly monotonic in version — hence free of duplicate versions
35+
||| and temporal skew.
36+
public export
37+
data History : (above : Nat) -> Type where
38+
Empty : History above
39+
Snap : (s : Snapshot) -> LT above (version s) ->
40+
History (version s) -> History above
41+
42+
||| The strict lower bound really is a strict lower bound on the head version —
43+
||| recovered directly from the constructor (monotonicity is not assumed, it is
44+
||| carried by the structure).
45+
export
46+
headStrictlyAbove : History above -> (s : Snapshot) -> LT above (version s) ->
47+
History (version s) -> LT above (version s)
48+
headStrictlyAbove _ _ prf _ = prf
49+
50+
--------------------------------------------------------------------------------
51+
-- Runtime validity check (what an implementation computes) + controls
52+
--------------------------------------------------------------------------------
53+
54+
||| Runtime check that a flat list of snapshots is strictly ascending in version
55+
||| starting above `lo`.
56+
public export
57+
ascending : (lo : Nat) -> List Snapshot -> Bool
58+
ascending _ [] = True
59+
ascending lo (At v _ :: xs) = lo < v && ascending v xs
60+
61+
||| Positive control: a genuinely ascending history passes.
62+
export
63+
ascendingAccepts : ascending 0 [At 1 100, At 3 300, At 7 700] = True
64+
ascendingAccepts = Refl
65+
66+
||| Negative control (non-vacuity): an out-of-order history is rejected, so the
67+
||| check is not constantly `True`.
68+
export
69+
ascendingRejects : ascending 0 [At 3 300, At 1 100] = False
70+
ascendingRejects = Refl
71+
72+
--------------------------------------------------------------------------------
73+
-- Point-in-time ("as-of") query + controls
74+
--------------------------------------------------------------------------------
75+
76+
||| Point-in-time query: the value of the latest snapshot whose version is `<= t`.
77+
||| For an ascending history this is the most recent committed value as of `t`.
78+
public export
79+
asOf : (t : Nat) -> List Snapshot -> Maybe Nat
80+
asOf _ [] = Nothing
81+
asOf t (At v val :: xs) =
82+
if v <= t
83+
then case asOf t xs of
84+
Just later => Just later
85+
Nothing => Just val
86+
else Nothing
87+
88+
||| Querying before the first version yields nothing.
89+
export
90+
asOfBeforeStart : asOf 0 [At 1 100, At 3 300, At 7 700] = Nothing
91+
asOfBeforeStart = Refl
92+
93+
||| Querying at t = 5 returns version 3's value (300): the latest version `<= 5`,
94+
||| not the newest (7) and not an earlier one (1).
95+
export
96+
asOfPicksLatest : asOf 5 [At 1 100, At 3 300, At 7 700] = Just 300
97+
asOfPicksLatest = Refl
98+
99+
||| Querying at or beyond the newest version returns the newest value.
100+
export
101+
asOfPicksNewest : asOf 9 [At 1 100, At 3 300, At 7 700] = Just 700
102+
asOfPicksNewest = Refl
103+
104+
||| Non-vacuity for the construction side: a strictly-ascending history exists.
105+
export
106+
historyExists : History 0
107+
historyExists = Snap (At 1 100) (LTESucc LTEZero) Empty

‎src/interface/abi/verisimiser-abi.ipkg‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,6 @@ modules = Verisimiser.ABI.Types
1010
, Verisimiser.ABI.Foreign
1111
, Verisimiser.ABI.Proofs
1212
, Verisimiser.ABI.Octad
13+
, Verisimiser.ABI.HashChain
14+
, Verisimiser.ABI.Version
15+
, Verisimiser.ABI.Lineage

0 commit comments

Comments
 (0)