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

ROADMAP.adoc

@@ -23,7 +23,7 @@
 * [ ] **Constraints** / drift detection — read-path observer; eight categories (ADR-0003)
 * [x] **Constraints** category 1 of 8: Temporal drift detector (V-L1-E2 / #49)
 * [ ] **Constraints** categories 2–8 of 8: Structural, Semantic, Statistical, Referential, Provenance, Spatial, Embedding
-* [ ] Idris2 ABI proofs: sidecar isolation, hash-chain integrity, version ordering, lineage acyclicity
+* [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)
 * [ ] Zig FFI bridge: database connection, sidecar operations, VCL-total queries
 * [ ] End-to-end test: PostgreSQL → verisimiser concerns → VCL-total query
 

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

@@ -0,0 +1,141 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Provenance hash-chain integrity for VeriSimiser.
+|||
+||| The Provenance octad dimension is a hash chain (ROADMAP Phase 1 — a write-path
+||| observer with a SHA-256 hash chain): every entry records the hash of its
+||| predecessor, so tampering with an earlier entry breaks every hash downstream.
+||| This module models that chain and proves its integrity properties:
+|||
+|||   1. Integrity by construction — `ProvChain` can only be extended by an entry
+|||      that links onto the chain's *current* tip, so a `ProvChain t` value is a
+|||      proof that every link is intact.
+|||   2. The runtime replay verifier accepts a correctly-linked entry
+|||      (`replayOne`) and rejects a forged predecessor link (`replayReject`).
+|||   3. No link can masquerade as the genesis record (`linkHashNeverGenesis`),
+|||      and changing the hashed content changes the tip (`contentChangesTip`) —
+|||      so the chain genuinely binds its contents.
+module Verisimiser.ABI.HashChain
+
+import Verisimiser.ABI.Types
+import Data.Nat
+
+%default total
+
+||| Integer tag for the operation recorded in a provenance entry.
+public export
+opTag : ProvenanceOperation -> Nat
+opTag Create    = 0
+opTag Update    = 1
+opTag Delete    = 2
+opTag Transform = 3
+
+||| The tip hash of an empty provenance log.
+public export
+genesisHash : Nat
+genesisHash = 0
+
+||| Deterministic modelled digest of a new link: folds the predecessor tip with
+||| the operation tag and the content digest. The leading `S` makes every link
+||| hash non-zero, so no link can be confused with `genesisHash`.
+public export
+linkHash : (prev : Nat) -> (op : ProvenanceOperation) -> (content : Nat) -> Nat
+linkHash prev op content = S (prev + opTag op + content)
+
+||| A provenance hash chain indexed by its current tip hash.
+|||
+||| `Append` forces the new entry to chain onto the chain's *actual* current tip,
+||| and the resulting tip is `linkHash` of that entry. A value of `ProvChain t` is
+||| therefore a proof that every link is intact: integrity by construction.
+public export
+data ProvChain : (tip : Nat) -> Type where
+  ||| The empty log: its tip is `genesisHash` (= 0). Written as the literal `0`
+  ||| because a bare lowercase `genesisHash` in an index position would be
+  ||| auto-bound as a fresh implicit (inhabiting every tip and silently voiding
+  ||| the integrity guarantee).
+  Origin : ProvChain 0
+  Append : (op : ProvenanceOperation) -> (content : Nat) ->
+           ProvChain prev -> ProvChain (linkHash prev op content)
+
+||| A stored provenance entry as it appears on disk / over the FFI: the operation,
+||| the content digest, and the predecessor hash the writer *recorded*.
+public export
+record StoredLink where
+  constructor MkLink
+  op      : ProvenanceOperation
+  content : Nat
+  recPrev : Nat
+
+||| Runtime verifier: replay stored links from a starting tip, checking that each
+||| entry's recorded predecessor hash matches the running tip. Returns the final
+||| tip if intact, `Nothing` at the first broken link.
+public export
+replay : (tip : Nat) -> List StoredLink -> Maybe Nat
+replay tip []                            = Just tip
+replay tip (MkLink op content recPrev :: rest) =
+  if recPrev == tip
+    then replay (linkHash tip op content) rest
+    else Nothing
+
+--------------------------------------------------------------------------------
+-- Verifier soundness lemmas (general, not just concrete witnesses)
+--------------------------------------------------------------------------------
+
+||| `==` on `Nat` is reflexive — needed to discharge the "predecessor matches the
+||| running tip" branch of `replay` for an arbitrary tip.
+eqNatRefl : (n : Nat) -> (n == n) = True
+eqNatRefl 0     = Refl
+eqNatRefl (S k) = eqNatRefl k
+
+||| The verifier ACCEPTS a correctly-linked entry: when the recorded predecessor
+||| equals the current tip, replay advances the tip by `linkHash`.
+export
+replayOne : (tip : Nat) -> (op : ProvenanceOperation) -> (content : Nat) ->
+            replay tip [MkLink op content tip] = Just (linkHash tip op content)
+replayOne tip op content = rewrite eqNatRefl tip in Refl
+
+||| The verifier REJECTS a forged link: when the recorded predecessor differs from
+||| the current tip, replay fails at that entry. (Non-vacuous tamper detection.)
+export
+replayReject : (tip, bad : Nat) -> (op : ProvenanceOperation) -> (content : Nat) ->
+               (bad == tip) = False ->
+               replay tip [MkLink op content bad] = Nothing
+replayReject tip bad op content noteq = rewrite noteq in Refl
+
+--------------------------------------------------------------------------------
+-- Anti-forgery properties of the hash itself
+--------------------------------------------------------------------------------
+
+||| No link hash can equal the genesis hash, so a forged entry can never pose as
+||| the start of the chain.
+export
+linkHashNeverGenesis : (prev : Nat) -> (op : ProvenanceOperation) -> (content : Nat) ->
+                       Not (linkHash prev op content = 0)
+linkHashNeverGenesis prev op content Refl impossible
+
+||| The tip binds the hashed content: distinct content under the same predecessor
+||| and operation yields a distinct tip (a concrete, non-vacuous witness that the
+||| chain is not blind to its payload).
+export
+contentChangesTip : Not (linkHash 0 Create 1 = linkHash 0 Create 2)
+contentChangesTip Refl impossible
+
+--------------------------------------------------------------------------------
+-- Concrete end-to-end controls
+--------------------------------------------------------------------------------
+
+||| A correctly-linked two-entry chain replays from genesis to its computed tip.
+||| (genesis = 0; first tip = linkHash 0 Create 10 = S (0+0+10) = 11;
+|||  second tip = linkHash 11 Update 5 = S (11+1+5) = 18.)
+export
+intactChainReplays :
+  replay 0 [MkLink Create 10 0, MkLink Update 5 11] = Just 18
+intactChainReplays = Refl
+
+||| Tampering with the second entry's recorded predecessor (12 instead of 11)
+||| makes replay fail — the end-to-end negative control.
+export
+tamperedChainFails :
+  replay 0 [MkLink Create 10 0, MkLink Update 5 12] = Nothing
+tamperedChainFails = Refl

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

@@ -0,0 +1,107 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Lineage acyclicity for VeriSimiser.
+|||
+||| The Lineage octad dimension is a DAG: "what was derived from what" (ROADMAP
+||| Phase 1, ADR-0005 — acyclic edges enforced via recursive CTE). This module
+||| models lineage as edges over a topological index and proves the *defining*
+||| invariant — the lineage graph is acyclic — as a genuine theorem, not a
+||| runtime check:
+|||
+|||   1. A derivation edge always moves to a strictly greater topological index
+|||      (`DerivedFrom`), so a derived node is never its own source.
+|||   2. Any lineage *path* (transitive derivation) strictly increases the index
+|||      (`lineageIncreases`).
+|||   3. Therefore no node lies in its own lineage — there are no cycles
+|||      (`noCycle`), and in particular no self-loops (`noSelfLoop`).
+|||
+||| The `LTE` helper lemmas are proved here from the constructors directly, so the
+||| module depends on nothing that could hide an axiom.
+module Verisimiser.ABI.Lineage
+
+import Verisimiser.ABI.Types
+import Data.Nat
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Order lemmas (proved constructively from LTE's constructors)
+--------------------------------------------------------------------------------
+
+||| Weakening on the right: `n <= m` implies `n <= S m`.
+lteUp : LTE n m -> LTE n (S m)
+lteUp LTEZero     = LTEZero
+lteUp (LTESucc p) = LTESucc (lteUp p)
+
+||| Strip a successor on the left: `S n <= m` implies `n <= m`.
+lteDownLeft : LTE (S n) m -> LTE n m
+lteDownLeft (LTESucc p) = lteUp p
+
+||| Transitivity of `<=`.
+lteChain : LTE a b -> LTE b c -> LTE a c
+lteChain LTEZero     _           = LTEZero
+lteChain (LTESucc p) (LTESucc q) = LTESucc (lteChain p q)
+
+||| Transitivity of strict `<` (recall `LT a b = LTE (S a) b`).
+ltChain : LT a b -> LT b c -> LT a c
+ltChain ab bc = lteChain ab (lteDownLeft bc)
+
+||| No natural is strictly less than itself — `S n <= n` is uninhabited.
+ltIrreflexive : LT n n -> Void
+ltIrreflexive (LTESucc p) = ltIrreflexive p
+
+--------------------------------------------------------------------------------
+-- Lineage model
+--------------------------------------------------------------------------------
+
+||| A single derivation edge: `dst` was derived from `src`. Well-formed exactly
+||| when the derived node has a strictly greater topological index than its
+||| source — this strict-decrease-toward-roots discipline is what makes the graph
+||| a DAG.
+public export
+data DerivedFrom : (src, dst : Nat) -> Type where
+  Derive : LT src dst -> DerivedFrom src dst
+
+||| A lineage path: the transitive closure of derivation. `src` is (transitively)
+||| an ancestor of `dst`.
+public export
+data Lineage : (src, dst : Nat) -> Type where
+  ||| One derivation step.
+  Direct : DerivedFrom src dst -> Lineage src dst
+  ||| Compose a step with a longer tail.
+  Then   : DerivedFrom src mid -> Lineage mid dst -> Lineage src dst
+
+--------------------------------------------------------------------------------
+-- Acyclicity theorems
+--------------------------------------------------------------------------------
+
+||| Every lineage path strictly increases the topological index.
+export
+lineageIncreases : Lineage src dst -> LT src dst
+lineageIncreases (Direct (Derive lt))   = lt
+lineageIncreases (Then (Derive lt) rest) = ltChain lt (lineageIncreases rest)
+
+||| ACYCLICITY (the defining invariant): no node lies in its own lineage. If it
+||| did, the path would force `LT n n`, which is impossible.
+export
+noCycle : Not (Lineage n n)
+noCycle l = ltIrreflexive (lineageIncreases l)
+
+||| In particular there are no self-loops: a node is never directly derived from
+||| itself.
+export
+noSelfLoop : Not (DerivedFrom n n)
+noSelfLoop (Derive lt) = ltIrreflexive lt
+
+||| Non-vacuity: genuine derivations do exist (0 -> 1 is a well-formed edge), so
+||| `DerivedFrom` is not the empty relation.
+export
+derivationsExist : DerivedFrom 0 1
+derivationsExist = Derive (LTESucc LTEZero)
+
+||| Non-vacuity: multi-hop lineage exists (0 -> 1 -> 2), so the acyclicity result
+||| above is not vacuously true over an empty path space.
+export
+lineageExists : Lineage 0 2
+lineageExists = Then (Derive (LTESucc LTEZero)) (Direct (Derive (LTESucc (LTESucc LTEZero))))

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

@@ -0,0 +1,107 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Temporal version ordering for VeriSimiser.
+|||
+||| The Temporal octad dimension keeps a value's version history and answers
+||| point-in-time ("as-of") queries (ROADMAP Phase 1 — `verisimdb_temporal_versions`).
+||| This module proves the defining invariants:
+|||
+|||   1. Strict monotonicity by construction — a `History` can only be extended by
+|||      a snapshot whose version strictly exceeds the previous one, so there is no
+|||      version skew and no duplicate versions.
+|||   2. A runtime `asOf` query and an `ascending` validity check, each pinned by
+|||      concrete positive and negative controls (the controls are non-vacuous: the
+|||      checks really do separate good histories from bad ones).
+module Verisimiser.ABI.Version
+
+import Verisimiser.ABI.Types
+import Data.Nat
+
+%default total
+
+||| A versioned snapshot: a logical version number and an (abstract) value digest.
+public export
+record Snapshot where
+  constructor At
+  version : Nat
+  value   : Nat
+
+||| A version history with strictly increasing version numbers, indexed by a
+||| strict lower bound that the head snapshot's version must exceed.
+|||
+||| Being able to *construct* a `History above` is itself a proof that the whole
+||| history is strictly monotonic in version — hence free of duplicate versions
+||| and temporal skew.
+public export
+data History : (above : Nat) -> Type where
+  Empty : History above
+  Snap  : (s : Snapshot) -> LT above (version s) ->
+          History (version s) -> History above
+
+||| The strict lower bound really is a strict lower bound on the head version —
+||| recovered directly from the constructor (monotonicity is not assumed, it is
+||| carried by the structure).
+export
+headStrictlyAbove : History above -> (s : Snapshot) -> LT above (version s) ->
+                    History (version s) -> LT above (version s)
+headStrictlyAbove _ _ prf _ = prf
+
+--------------------------------------------------------------------------------
+-- Runtime validity check (what an implementation computes) + controls
+--------------------------------------------------------------------------------
+
+||| Runtime check that a flat list of snapshots is strictly ascending in version
+||| starting above `lo`.
+public export
+ascending : (lo : Nat) -> List Snapshot -> Bool
+ascending _  []              = True
+ascending lo (At v _ :: xs)  = lo < v && ascending v xs
+
+||| Positive control: a genuinely ascending history passes.
+export
+ascendingAccepts : ascending 0 [At 1 100, At 3 300, At 7 700] = True
+ascendingAccepts = Refl
+
+||| Negative control (non-vacuity): an out-of-order history is rejected, so the
+||| check is not constantly `True`.
+export
+ascendingRejects : ascending 0 [At 3 300, At 1 100] = False
+ascendingRejects = Refl
+
+--------------------------------------------------------------------------------
+-- Point-in-time ("as-of") query + controls
+--------------------------------------------------------------------------------
+
+||| Point-in-time query: the value of the latest snapshot whose version is `<= t`.
+||| For an ascending history this is the most recent committed value as of `t`.
+public export
+asOf : (t : Nat) -> List Snapshot -> Maybe Nat
+asOf _ []              = Nothing
+asOf t (At v val :: xs) =
+  if v <= t
+    then case asOf t xs of
+           Just later => Just later
+           Nothing    => Just val
+    else Nothing
+
+||| Querying before the first version yields nothing.
+export
+asOfBeforeStart : asOf 0 [At 1 100, At 3 300, At 7 700] = Nothing
+asOfBeforeStart = Refl
+
+||| Querying at t = 5 returns version 3's value (300): the latest version `<= 5`,
+||| not the newest (7) and not an earlier one (1).
+export
+asOfPicksLatest : asOf 5 [At 1 100, At 3 300, At 7 700] = Just 300
+asOfPicksLatest = Refl
+
+||| Querying at or beyond the newest version returns the newest value.
+export
+asOfPicksNewest : asOf 9 [At 1 100, At 3 300, At 7 700] = Just 700
+asOfPicksNewest = Refl
+
+||| Non-vacuity for the construction side: a strictly-ascending history exists.
+export
+historyExists : History 0
+historyExists = Snap (At 1 100) (LTESucc LTEZero) Empty

src/interface/abi/verisimiser-abi.ipkg

@@ -10,3 +10,6 @@ modules = Verisimiser.ABI.Types
         , Verisimiser.ABI.Foreign
         , Verisimiser.ABI.Proofs
         , Verisimiser.ABI.Octad
+        , Verisimiser.ABI.HashChain
+        , Verisimiser.ABI.Version
+        , Verisimiser.ABI.Lineage