From dafdcded6ac8a745c00c9838feda0e8bf4f9bcb4 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 19:38:20 +0000 Subject: [PATCH] feat(abi): prove hash-chain integrity, version ordering & lineage acyclicity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01JdqVWGSSv36Ph8ZWvizGMp --- ROADMAP.adoc | 2 +- .../abi/Verisimiser/ABI/HashChain.idr | 141 ++++++++++++++++++ src/interface/abi/Verisimiser/ABI/Lineage.idr | 107 +++++++++++++ src/interface/abi/Verisimiser/ABI/Version.idr | 107 +++++++++++++ src/interface/abi/verisimiser-abi.ipkg | 3 + 5 files changed, 359 insertions(+), 1 deletion(-) create mode 100644 src/interface/abi/Verisimiser/ABI/HashChain.idr create mode 100644 src/interface/abi/Verisimiser/ABI/Lineage.idr create mode 100644 src/interface/abi/Verisimiser/ABI/Version.idr diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 9a675c1..317f5c5 100644 --- a/ROADMAP.adoc +++ b/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 diff --git a/src/interface/abi/Verisimiser/ABI/HashChain.idr b/src/interface/abi/Verisimiser/ABI/HashChain.idr new file mode 100644 index 0000000..fbe0b4c --- /dev/null +++ b/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) +-- +||| 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 diff --git a/src/interface/abi/Verisimiser/ABI/Lineage.idr b/src/interface/abi/Verisimiser/ABI/Lineage.idr new file mode 100644 index 0000000..bc12334 --- /dev/null +++ b/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) +-- +||| 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)))) diff --git a/src/interface/abi/Verisimiser/ABI/Version.idr b/src/interface/abi/Verisimiser/ABI/Version.idr new file mode 100644 index 0000000..723f573 --- /dev/null +++ b/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) +-- +||| 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 diff --git a/src/interface/abi/verisimiser-abi.ipkg b/src/interface/abi/verisimiser-abi.ipkg index 8533052..5ea54b8 100644 --- a/src/interface/abi/verisimiser-abi.ipkg +++ b/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