|
| 1 | +||| SPDX-License-Identifier: MPL-2.0 |
| 2 | +||| |
| 3 | +||| Ochrance.Filesystem.RepairVerify - Stage 3.2: whole-manifest repair => verify. |
| 4 | +||| |
| 5 | +||| The end-to-end guarantee that ties Stage 2.2 (verifier soundness) to Stage 3.1 |
| 6 | +||| (pure repair): after repairing every ref of a manifest, the verifier ACCEPTS |
| 7 | +||| that manifest - `verifyRefsHelper (repairRefsPure s refs) refs = Right ()`. |
| 8 | +||| |
| 9 | +||| `repairRefsPure` folds the 3.1 single-block primitive `repairBlockPure` over the |
| 10 | +||| refs, installing each ref's hash at its parsed index. The proof factors as: |
| 11 | +||| |
| 12 | +||| * `verifyRefsComplete` (Lemma A) - COMPLETENESS, the exact converse of 2.2's |
| 13 | +||| `verifyRefsSound`: if every ref matches the state (`All (RefMatches fs)`), the |
| 14 | +||| verifier accepts. Drives the four guards forward from the witness equalities. |
| 15 | +||| * `repairRefsConsistent` (Lemma B) - repair ESTABLISHES that match witness for |
| 16 | +||| every ref, via `repairBlockSets` (the head's index now holds its hash) and |
| 17 | +||| `repairRefsPurePreserves` (no later repair clobbers it - this is where |
| 18 | +||| distinctness is consumed). |
| 19 | +||| |
| 20 | +||| Two boundaries are named explicitly, never faked (the house style of |
| 21 | +||| `CollisionResistant` / `HexByteRoundtrip`): |
| 22 | +||| * `hashRefl : (h : Hash) -> (h == h) = True` - reflexivity of the PRIMITIVE |
| 23 | +||| `Hash`/`String` `==` (the same wall as `merkleCorrect`'s residual `root==root` |
| 24 | +||| step; `Nat` reflexivity, by contrast, is structural - `eqNatReflTrue`); |
| 25 | +||| * `GoodRefs` - the precondition that ref names parse to DISTINCT in-range |
| 26 | +||| indices. Without distinctness a later repair would overwrite an earlier ref's |
| 27 | +||| block, so the theorem would be false; it is a genuine hypothesis, not a dodge. |
| 28 | +||| |
| 29 | +||| No `believe_me`, no `assert_total`, no `postulate`. |
| 30 | +module Ochrance.Filesystem.RepairVerify |
| 31 | + |
| 32 | +import Data.List.Quantifiers |
| 33 | + |
| 34 | +import Ochrance.A2ML.Types |
| 35 | +import Ochrance.Framework.Error |
| 36 | +import Ochrance.Filesystem.Types |
| 37 | +import Ochrance.Filesystem.Verify |
| 38 | +import Ochrance.Filesystem.VerifyProof |
| 39 | +import Ochrance.Filesystem.Repair |
| 40 | +import Ochrance.Filesystem.RepairProof |
| 41 | + |
| 42 | +%default total |
| 43 | + |
| 44 | +-------------------------------------------------------------------------------- |
| 45 | +-- Pure whole-manifest repair |
| 46 | +-------------------------------------------------------------------------------- |
| 47 | + |
| 48 | +||| Repair every ref of a manifest: install each ref's hash at its parsed block |
| 49 | +||| index (refs whose name does not parse are skipped - `GoodRefs` rules that out). |
| 50 | +||| Folds the Stage 3.1 primitive `repairBlockPure`. |
| 51 | +public export |
| 52 | +repairRefsPure : FSState -> List Ref -> FSState |
| 53 | +repairRefsPure s [] = s |
| 54 | +repairRefsPure s (ref :: refs) = |
| 55 | + case parseBlockIdx ref.name of |
| 56 | + Nothing => repairRefsPure s refs |
| 57 | + Just idx => repairRefsPure (repairBlockPure s idx ref.hash) refs |
| 58 | + |
| 59 | +-------------------------------------------------------------------------------- |
| 60 | +-- Precondition: distinct, in-range, parseable ref names |
| 61 | +-------------------------------------------------------------------------------- |
| 62 | + |
| 63 | +||| "This ref's name does NOT parse to index `i`." The atom of distinctness. |
| 64 | +public export |
| 65 | +NotParsedAs : BlockIndex -> Ref -> Type |
| 66 | +NotParsedAs i ref = Not (parseBlockIdx ref.name = Just i) |
| 67 | + |
| 68 | +||| Every ref name parses to a distinct, in-range block index. Indexed by the block |
| 69 | +||| count (a `Nat`) rather than the whole state, since repair preserves the count - |
| 70 | +||| so the same `GoodRefs` serves the original and every repaired state. |
| 71 | +public export |
| 72 | +data GoodRefs : Nat -> List Ref -> Type where |
| 73 | + GoodNil : GoodRefs nb [] |
| 74 | + GoodCons : {0 ref : Ref} -> {0 refs : List Ref} -> |
| 75 | + (idx : BlockIndex) -> |
| 76 | + parseBlockIdx ref.name = Just idx -> |
| 77 | + (idx >= nb) = False -> |
| 78 | + All (NotParsedAs idx) refs -> |
| 79 | + GoodRefs nb refs -> |
| 80 | + GoodRefs nb (ref :: refs) |
| 81 | + |
| 82 | +-------------------------------------------------------------------------------- |
| 83 | +-- Lemma A: completeness (converse of Stage 2.2) |
| 84 | +-------------------------------------------------------------------------------- |
| 85 | + |
| 86 | +||| COMPLETENESS: if every ref matches the filesystem state, the verifier accepts. |
| 87 | +||| The exact converse of `verifyRefsSound` - drives the four guards forward from |
| 88 | +||| each ref's `RefMatches` witness (name-parse, range, block-present, hash-equal). |
| 89 | +export |
| 90 | +verifyRefsComplete : (fs : FSState) -> (refs : List Ref) -> |
| 91 | + All (RefMatches fs) refs -> verifyRefsHelper fs refs = Right () |
| 92 | +verifyRefsComplete fs [] [] = Refl |
| 93 | +verifyRefsComplete fs (ref :: rs) ((idx ** (pi, rng, (h ** (bh, heq)))) :: rest) = |
| 94 | + rewrite pi in |
| 95 | + rewrite rng in |
| 96 | + rewrite bh in |
| 97 | + rewrite heq in |
| 98 | + verifyRefsComplete fs rs rest |
| 99 | + |
| 100 | +-------------------------------------------------------------------------------- |
| 101 | +-- Repair structural lemmas |
| 102 | +-------------------------------------------------------------------------------- |
| 103 | + |
| 104 | +||| Whole-manifest repair preserves the block count (folds 3.1's |
| 105 | +||| `repairBlockNumBlocks`). |
| 106 | +export |
| 107 | +repairRefsPureNumBlocks : (s : FSState) -> (refs : List Ref) -> |
| 108 | + numBlocks (repairRefsPure s refs) = numBlocks s |
| 109 | +repairRefsPureNumBlocks s [] = Refl |
| 110 | +repairRefsPureNumBlocks s (ref :: rs) with (parseBlockIdx ref.name) |
| 111 | + repairRefsPureNumBlocks s (ref :: rs) | Nothing = repairRefsPureNumBlocks s rs |
| 112 | + repairRefsPureNumBlocks s (ref :: rs) | Just idx = |
| 113 | + repairRefsPureNumBlocks (repairBlockPure s idx ref.hash) rs |
| 114 | + |
| 115 | +||| Repairing a list whose parsed indices all differ from `i` leaves block `i` |
| 116 | +||| untouched - the no-clobber lemma. Folds 3.1's `repairBlockPreserves`; the per- |
| 117 | +||| step inequality comes from `NotParsedAs` via `neqNatFalse`. |
| 118 | +export |
| 119 | +repairRefsPurePreserves : (s : FSState) -> (refs : List Ref) -> (i : BlockIndex) -> |
| 120 | + All (NotParsedAs i) refs -> |
| 121 | + blockHash (repairRefsPure s refs) i = blockHash s i |
| 122 | +repairRefsPurePreserves s [] i _ = Refl |
| 123 | +repairRefsPurePreserves s (ref :: rs) i (notHere :: notRest) with (parseBlockIdx ref.name) |
| 124 | + repairRefsPurePreserves s (ref :: rs) i (notHere :: notRest) | Nothing = |
| 125 | + repairRefsPurePreserves s rs i notRest |
| 126 | + repairRefsPurePreserves s (ref :: rs) i (notHere :: notRest) | Just j = |
| 127 | + -- `with` has refined `notHere : Not (Just j = Just i)` |
| 128 | + let iNotJ : Not (i = j) |
| 129 | + iNotJ = \p => notHere (cong Just (sym p)) |
| 130 | + in trans (repairRefsPurePreserves (repairBlockPure s j ref.hash) rs i notRest) |
| 131 | + (repairBlockPreserves s j ref.hash i (neqNatFalse i j iNotJ)) |
| 132 | + |
| 133 | +||| Unfold one step of `repairRefsPure` once the head ref's index is known. |
| 134 | +export |
| 135 | +repairRefsUnfold : (s : FSState) -> (ref : Ref) -> (refs : List Ref) -> |
| 136 | + (idx : BlockIndex) -> parseBlockIdx ref.name = Just idx -> |
| 137 | + repairRefsPure s (ref :: refs) = repairRefsPure (repairBlockPure s idx ref.hash) refs |
| 138 | +repairRefsUnfold s ref refs idx pi = rewrite pi in Refl |
| 139 | + |
| 140 | +-------------------------------------------------------------------------------- |
| 141 | +-- Lemma B: repair establishes the match witness |
| 142 | +-------------------------------------------------------------------------------- |
| 143 | + |
| 144 | +||| Repair ESTABLISHES consistency: after `repairRefsPure`, every ref matches the |
| 145 | +||| repaired state. The head's hash is installed (`repairBlockSets`) and protected |
| 146 | +||| from later repairs (`repairRefsPurePreserves`, fed the head's distinctness); the |
| 147 | +||| tail is the induction hypothesis (the repaired state's count equals the |
| 148 | +||| original's, definitionally, so the same `GoodRefs` carries through). The hash |
| 149 | +||| equality of each ref against itself is the named `hashRefl` boundary. |
| 150 | +export |
| 151 | +repairRefsConsistent : (s : FSState) -> (refs : List Ref) -> |
| 152 | + GoodRefs (numBlocks s) refs -> |
| 153 | + (hashRefl : (h : Hash) -> (h == h) = True) -> |
| 154 | + All (RefMatches (repairRefsPure s refs)) refs |
| 155 | +repairRefsConsistent s [] GoodNil hashRefl = [] |
| 156 | +repairRefsConsistent s (ref :: rs) (GoodCons idx pi rng notI good') hashRefl = |
| 157 | + let s' : FSState |
| 158 | + s' = repairBlockPure s idx ref.hash |
| 159 | + bhF : blockHash (repairRefsPure s' rs) idx = Just ref.hash |
| 160 | + bhF = trans (repairRefsPurePreserves s' rs idx notI) |
| 161 | + (repairBlockSets s idx ref.hash) |
| 162 | + rngF : (idx >= numBlocks (repairRefsPure s' rs)) = False |
| 163 | + rngF = rewrite repairRefsPureNumBlocks s' rs in rng |
| 164 | + headW : RefMatches (repairRefsPure s' rs) ref |
| 165 | + headW = (idx ** (pi, rngF, (ref.hash ** (bhF, hashRefl ref.hash)))) |
| 166 | + tailW : All (RefMatches (repairRefsPure s' rs)) rs |
| 167 | + tailW = repairRefsConsistent s' rs good' hashRefl |
| 168 | + in rewrite repairRefsUnfold s ref rs idx pi in (headW :: tailW) |
| 169 | + |
| 170 | +-------------------------------------------------------------------------------- |
| 171 | +-- Stage 3.2: whole-manifest repair => verify |
| 172 | +-------------------------------------------------------------------------------- |
| 173 | + |
| 174 | +||| STAGE 3.2: repairing a manifest's refs makes the verifier accept it. Composes |
| 175 | +||| Lemma B (repair => match witnesses) with Lemma A (witnesses => acceptance). |
| 176 | +||| Honest hypotheses: `GoodRefs` (distinct in-range parseable names) and `hashRefl` |
| 177 | +||| (primitive `Hash` `==` reflexivity). |
| 178 | +export |
| 179 | +repairThenVerify : (s : FSState) -> (refs : List Ref) -> |
| 180 | + GoodRefs (numBlocks s) refs -> |
| 181 | + (hashRefl : (h : Hash) -> (h == h) = True) -> |
| 182 | + verifyRefsHelper (repairRefsPure s refs) refs = Right () |
| 183 | +repairThenVerify s refs good hashRefl = |
| 184 | + verifyRefsComplete (repairRefsPure s refs) refs |
| 185 | + (repairRefsConsistent s refs good hashRefl) |
0 commit comments