Skip to content

Commit 93181d1

Browse files
claudehyperpolymath
claude
authored and
hyperpolymath
committed
proof(repair): Stage 3.1 — pure repair primitive correctness (idempotence proved)
FSState's verifiable content is its hash map (no separate block data), so the pure repairBlockPure — installing a hash at one index — is the genuine repair semantics, not a no-op. Factored it out of the IO repairBlock (IO↔pure pattern: repairBlock = repairBlockPure + range check), making the correctness theorems well-founded. RepairProof (axiom-free, machine-checked): - repairBlockSets — the repaired index now holds exactly the new hash; - repairBlockPreserves — every other index is untouched; - repairBlockNumBlocks — the block count is unchanged; - repairBlockIdempotent — repairing the same (index, hash) twice = once (the ledger's "idempotence as a proof", delivered). Index test is Nat == (structural reflexivity eqNatReflTrue / neqNatFalse), so wall-free — unlike the primitive Hash ==. Idempotence decided via decEq to avoid the with-on-(==) asymmetric-reduction trap. NEXT (3.2): whole-manifest repair ⇒ verifyRefsHelper passes — builds on 2.2 + these lemmas, needs a distinct-in-range ref-name precondition and the isolated Hash-reflexivity hypothesis (documented). Verified: idris2 0.8.0, --build (--total), 25/25 modules, axiom-free. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
1 parent 04ce0c8 commit 93181d1

5 files changed

Lines changed: 132 additions & 30 deletions

File tree

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,12 @@ project = "ochrance"
77
version = "0.1.0"
88
last-updated = "2026-06-18"
99
status = "active"
10-
session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 provable core complete: validator, verifier, hex)"
10+
session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 provable core complete; Stage 3.1 pure repair correctness done)"
1111

1212
[project-context]
1313
name = "Ochránce"
1414
purpose = """Neurosymbolic filesystem verification framework in Idris2 dependent types: a pluggable VerifiedSubsystem interface, A2ML attestation/audit markup, a verified Merkle tree with a combiner-generic soundness theorem, and ECHIDNA integration."""
15-
completion-percentage = 58
15+
completion-percentage = 62
1616

1717
[position]
1818
phase = "implementation" # design | implementation | testing | maintenance | archived
@@ -30,6 +30,7 @@ theorems = [
3030
"validateManifestSound (Stage 2.1) — validator soundness: accepted manifest ⇒ supported version, non-empty subsystem, All RefValid refs (Bool-level, Either-pipeline inversion)",
3131
"parsePairsRoundtrip (Stage 2.3) — hex codec structural soundness: parsePairs (bytesToHexChars bs) = Just bs, given isolated per-byte Bits8 hypothesis (pack/unpack wall explicit)",
3232
"verifyRefsSound (Stage 2.2) — verifier soundness: verifyRefsHelper fs refs = Right () ⇒ All (RefMatches fs) refs (four-guard per-ref inversion; merkle-root wiring deferred as architectural)",
33+
"repairBlock{Sets,Preserves,NumBlocks,Idempotent} (Stage 3.1) — pure repair primitive correctness over repairBlockPure: installs hash at index, preserves others + count, idempotent (wall-free Nat == via eqNatReflTrue/neqNatFalse)",
3334
"roundtripManifest (+ algoRT/modeRT/refsRT/mpolRT codecs) — decodeManifest (encodeManifest m) = Just m",
3435
"SatisfiesMinimum / attestedSatisfiesLax — progressive-assurance threshold witness",
3536
"ABI Handle / createHandle — So (ptr /= 0) non-null invariant",
@@ -57,7 +58,8 @@ issues = [
5758
actions = [
5859
"Stage 1 COMPLETE — 1.1 buildGetLeaf, 1.2 rootFoldLaw, 1.3 IO↔pure bridge, 1.4 merkleBinding/CollisionResistant — all machine-checked (idris2 0.8.0, --total)",
5960
"Stage 2 provable core COMPLETE — 2.1 validateManifestSound, 2.2 verifyRefsSound, 2.3 parsePairsRoundtrip; all machine-checked. DEFERRED (architectural decision): wire verify to merkleCorrect — the verify path builds no Merkle tree today",
60-
"Stage 3 (Opus) — repair correctness (L3 linear types). PRECONDITION: repair is a stub; introduce a pure repairPure that genuinely reconstructs the hash map and prove over that (IO↔pure pattern), else the theorem is vacuous",
61+
"Stage 3.1 DONE — pure repair primitive correctness (repairBlockPure factored out; sets/preserves/numBlocks/idempotent machine-checked). NEXT 3.2: whole-manifest repair ⇒ verifyRefsHelper passes (needs distinct-in-range ref-name precondition + isolated Hash-reflexivity hypothesis)",
62+
"Then: verify→merkleCorrect wiring (architectural — verify builds no Merkle tree today; would carry merkleBinding's no-collision guarantee into verification)",
6163
"Remove Idris-side crypto stubs and build + link libochrance.so into the flow (unblocks the crypto-integrity claim)",
6264
"Sync .machine_readable scaffold to rsr-template (ai/, compliance/, configs/, policies/, scripts/, 0.1-AI-MANIFEST, ENSAID_CONFIG, root README, root-allow) — pending template access",
6365
]

‎docs/PROOFS.adoc‎

Lines changed: 28 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,10 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the
111111
| verifier soundness: `verifyRefsHelper fs refs = Right ()` ⇒ `All (RefMatches fs) refs`
112112
— every accepted ref names an in-range block whose stored hash equals the ref's
113113
(four-guard per-ref inversion, Bool-level).
114+
| `repairBlock{Sets,Preserves,NumBlocks,Idempotent}` (Stage 3.1)
115+
| pure repair primitive correctness over `repairBlockPure`: installs the hash at the
116+
index, preserves other indices and the count, idempotent. Wall-free (`Nat`
117+
structural `==`: `eqNatReflTrue` / `neqNatFalse`).
114118
| `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …)
115119
| grammar invertibility: `decodeManifest (encodeManifest m) = Just m`.
116120
| `SatisfiesMinimum` / `attestedSatisfiesLax`
@@ -208,19 +212,30 @@ let `merkleBinding` carry the no-collision guarantee into verification).
208212

209213
=== Stage 3 — Repair correctness (L3, linear types) [model: Opus]
210214

211-
PRECONDITION (surfaced at Compaction 2): `repair` is currently a *stub* —
212-
`repairBlock` (`Repair.idr`) updates the hash map but does **not** read or write
213-
block data. Proving `verify (repair s) = Valid` against a no-op would be vacuous or
214-
false. DECISION (recommended): introduce a pure
215-
`repairPure : FSState -> Manifest -> FSState` that genuinely reconstructs the hash
216-
map, prove correctness over *that*, and make the IO `repair` a proven-equivalent
217-
shell (the IO↔pure pattern). Alternative: leave repair honestly-bounded until real
218-
block-I/O lands (defers the linear-type theorem).
219-
220-
. `verifyPure (repairPure s m) m = True` — the meaty (now well-founded) theorem.
221-
. Repair idempotence as a *proof* (today only a property test).
222-
. Harvest framework's mode-indexed Interface; state the `VerifiedSubsystem` law
223-
`verify (repair s m) m = Right …` and prove the FSState instance satisfies it.
215+
RESOLVED (was PRECONDITION): the pure repair core is now factored out —
216+
`repairBlockPure : FSState -> BlockIndex -> Hash -> FSState` installs a hash in the
217+
map, and the IO `repairBlock` is `repairBlockPure` + the range check (IO↔pure
218+
pattern). Because FSState's verifiable content *is* its hash map (it carries no
219+
separate block data), this is the genuine repair semantics, so the theorems are
220+
well-founded, not vacuous.
221+
222+
. *[DONE — 3.1]* Pure repair primitive correctness, machine-checked
223+
(`Ochrance.Filesystem.RepairProof`, axiom-free): `repairBlockSets` (the repaired
224+
index now holds the new hash), `repairBlockPreserves` (every other index
225+
untouched), `repairBlockNumBlocks` (block count preserved), and
226+
`repairBlockIdempotent` (repairing the same (index, hash) twice = once) — the
227+
ledger's "idempotence as a proof", delivered. The index test is `Nat` `==`
228+
(structural — `eqNatReflTrue` / `neqNatFalse`), so wall-free, unlike the primitive
229+
`Hash` `==`.
230+
. *[3.2 — next]* Whole-manifest repair ⇒ verify:
231+
`verifyRefsHelper (repairPure s m) m.refs = Right ()`. Builds on 2.2's
232+
`verifyRefsHelper` and the 3.1 lemmas, but needs (a) a precondition that ref names
233+
parse to *distinct* in-range indices (so the rebuilt map is per-ref consistent),
234+
and (b) the isolated `Hash`-reflexivity hypothesis `(h == h) = True` — the same
235+
primitive `==` wall as `merkleCorrect`'s residual step — named explicitly, never
236+
faked.
237+
. Harvest framework's mode-indexed Interface; state the `VerifiedSubsystem` law and
238+
prove the FSState instance satisfies it.
224239
+
225240
WATCH-FOR: may need proof witnesses threaded through the `1`-quantified API —
226241
possible signature changes to `Repair.idr`.

‎ochrance-core/Ochrance/Filesystem/Repair.idr‎

Lines changed: 19 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,19 @@ import Ochrance.FFI.Crypto
2727
-- Linear Repair Operations
2828
--------------------------------------------------------------------------------
2929

30+
||| Pure core of a single-block repair: install `expectedHash` at `blockIdx` in the
31+
||| state's hash map, leaving every other block and the block count untouched. The
32+
||| filesystem state's verifiable content *is* this hash map (FSState carries no
33+
||| separate block data), so this is the genuine repair semantics, not a no-op - the
34+
||| IO `repairBlock` is this plus the range check. Correctness is proved in
35+
||| `Ochrance.Filesystem.RepairProof`.
36+
public export
37+
repairBlockPure : FSState -> BlockIndex -> Hash -> FSState
38+
repairBlockPure s blockIdx expectedHash =
39+
MkFSState s.numBlocks
40+
(\idx => if idx == blockIdx then Just expectedHash else s.blockHash idx)
41+
s.metadata
42+
3043
||| Repair a single block in the filesystem.
3144
||| Uses linear types to ensure oldState is consumed exactly once.
3245
|||
@@ -46,20 +59,12 @@ repairBlock oldState blockIdx expectedHash = do
4659
-- Check if block index is valid
4760
if blockIdx >= numBlocks
4861
then pure (Left (QError (InvalidManifestPath ("Block index out of range: " ++ show blockIdx))))
49-
else do
50-
-- In a real implementation, this would:
51-
-- 1. Read the corrupted block
52-
-- 2. Attempt to repair from redundancy/parity data
53-
-- 3. Verify the repaired block matches expectedHash
54-
-- 4. Write the repaired block back to disk
55-
56-
-- For now, we create a new state with the hash updated
57-
let newState = MkFSState
58-
numBlocks
59-
(\idx => if idx == blockIdx then Just expectedHash else blockHashFunc idx)
60-
metadata
61-
62-
pure (Right newState)
62+
else
63+
-- The verifiable state is the hash map; repairBlockPure installs the hash.
64+
-- (A real backend would also read/repair/write block bytes; FSState models
65+
-- only the hashes, so this is the complete pure repair of the modelled state.)
66+
pure (Right (repairBlockPure (MkFSState numBlocks blockHashFunc metadata)
67+
blockIdx expectedHash))
6368

6469
||| Repair filesystem from a snapshot (linear version).
6570
||| Consumes the old state and produces a new state matching the snapshot.

‎ochrance-core/Ochrance/Filesystem/RepairProof.idr‎

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
||| SPDX-License-Identifier: MPL-2.0
2+
|||
3+
||| Ochrance.Filesystem.RepairProof - Stage 3: pure repair correctness.
4+
|||
5+
||| FSState's verifiable content is its hash map (`BlockIndex -> Maybe Hash`); there
6+
||| is no separate block data. So `repairBlockPure` - which installs a hash at one
7+
||| index - is the genuine repair semantics (not a no-op against which a theorem
8+
||| would be vacuous), and these lemmas pin it down:
9+
|||
10+
||| * `repairBlockSets` - the repaired index now holds exactly the new hash;
11+
||| * `repairBlockPreserves` - every other index is untouched;
12+
||| * `repairBlockNumBlocks` - the block count is unchanged;
13+
||| * `repairBlockIdempotent` - repairing the same (index, hash) twice equals once.
14+
|||
15+
||| All axiom-free: the index test is `Nat` `==`, whose reflexivity is *structural*
16+
||| (`eqNatReflTrue`) - unlike the primitive `Hash`/`String` `==`. No `believe_me`,
17+
||| no `postulate`.
18+
module Ochrance.Filesystem.RepairProof
19+
20+
import Decidable.Equality
21+
22+
import Ochrance.A2ML.Types
23+
import Ochrance.Filesystem.Types
24+
import Ochrance.Filesystem.Repair
25+
26+
%default total
27+
28+
||| `Nat` equality is reflexively `True` - provable because `Eq Nat` is structural
29+
||| (the wall-free counterpart of the primitive `String`/`Bits8` reflexivity that
30+
||| the `Hash` comparison would need).
31+
public export
32+
eqNatReflTrue : (n : Nat) -> (n == n) = True
33+
eqNatReflTrue Z = Refl
34+
eqNatReflTrue (S k) = eqNatReflTrue k
35+
36+
||| Repair installs the requested hash at the repaired index.
37+
export
38+
repairBlockSets : (s : FSState) -> (i : BlockIndex) -> (h : Hash) ->
39+
blockHash (repairBlockPure s i h) i = Just h
40+
repairBlockSets s i h = rewrite eqNatReflTrue i in Refl
41+
42+
||| Repair leaves every other index untouched.
43+
export
44+
repairBlockPreserves : (s : FSState) -> (i : BlockIndex) -> (h : Hash) ->
45+
(j : BlockIndex) -> (j == i) = False ->
46+
blockHash (repairBlockPure s i h) j = blockHash s j
47+
repairBlockPreserves s i h j neq = rewrite neq in Refl
48+
49+
||| Repair preserves the block count.
50+
export
51+
repairBlockNumBlocks : (s : FSState) -> (i : BlockIndex) -> (h : Hash) ->
52+
numBlocks (repairBlockPure s i h) = numBlocks s
53+
repairBlockNumBlocks s i h = Refl
54+
55+
||| `Nat` inequality reflects as `== = False` (structural counterpart of the
56+
||| primitive-equality wall). Used to drive `repairBlockPreserves` on the `j /= i`
57+
||| branch of idempotence.
58+
neqNatFalse : (m, n : Nat) -> Not (m = n) -> (m == n) = False
59+
neqNatFalse Z Z ctra = absurd (ctra Refl)
60+
neqNatFalse Z (S _) _ = Refl
61+
neqNatFalse (S _) Z _ = Refl
62+
neqNatFalse (S k) (S l) ctra = neqNatFalse k l (\p => ctra (cong S p))
63+
64+
||| Repair idempotence: repairing the same index with the same hash twice agrees
65+
||| with doing it once, at every index (extensional equality of the hash maps).
66+
||| Decided on `j` vs `i`: at `i`, both sides read `Just h` (`repairBlockSets`);
67+
||| elsewhere, both read the original (`repairBlockPreserves`). Uses `decEq` rather
68+
||| than a `with` on `j == i` (whose reduct `equalNat` collapses the two `if`s
69+
||| asymmetrically).
70+
export
71+
repairBlockIdempotent : (s : FSState) -> (i : BlockIndex) -> (h : Hash) ->
72+
(j : BlockIndex) ->
73+
blockHash (repairBlockPure (repairBlockPure s i h) i h) j
74+
= blockHash (repairBlockPure s i h) j
75+
repairBlockIdempotent s i h j = case decEq j i of
76+
Yes prf => rewrite prf in
77+
trans (repairBlockSets (repairBlockPure s i h) i h)
78+
(sym (repairBlockSets s i h))
79+
No ctra => repairBlockPreserves (repairBlockPure s i h) i h j (neqNatFalse j i ctra)

‎ochrance.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ modules = Ochrance.A2ML.Types
3232
, Ochrance.Filesystem.Verify
3333
, Ochrance.Filesystem.VerifyProof
3434
, Ochrance.Filesystem.Repair
35+
, Ochrance.Filesystem.RepairProof
3536
, Ochrance.FFI.Echidna
3637

3738
opts = "--total"

0 commit comments

Comments
 (0)