diff --git a/README.md b/README.md index 8772c51..48d0762 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,7 @@ the same discipline as the four `*-ed25519-verified` subject corpora. | L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 2) **done, non-vacuous** | | L6a | descent extractor `extractMTH` (Theorem 3 step 3 = Lemma 2, WHOLE-TREE instance) **done, non-vacuous** | | — | Lemma 2, PATH instance (receipt-uniqueness of `Root`): deleted with the vacuous `root_binding` in S3.5 and **not yet restored**; optional, not needed for Theorem 3 | -| L6b | ConsRec binding + Theorem 3 assembly (extractCons) | in progress (S5): stage-1 arithmetic/list infrastructure done (kbelow_prefix_eq, take surgery); stage-1 infra + extractConsNode extractor DEFINED (faithful to ConsRec by inspection — NOT yet machine-checked); binding proof + extractCons assembly = stage 3 | +| L6b | ConsRec binding + Theorem 3 assembly (extractCons) | in progress (S5): stage-1 arithmetic/list infrastructure done (kbelow_prefix_eq, take surgery); stage-1 infra + extractConsNode extractor DEFINED (faithful to ConsRec by inspection — NOT yet machine-checked); **consRecBinding PROVEN** (Theorem 3 steps 1-2, kernel-checked, no sorry); extractCons assembly (step 3 join) = S5.4 | | L6 | pin-store state machine safety (Proposition 1) | pending | ## Discipline (identical to the subject corpora) diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean index 6fd10d5..59b0fbd 100644 --- a/verification/Proofs/AxiomCheck.lean +++ b/verification/Proofs/AxiomCheck.lean @@ -4,6 +4,7 @@ import Proofs.Completeness import Proofs.Extract import Proofs.Descent import Proofs.Consistency +import Proofs.Binding3 #print axioms LTLAcc.domsep #print axioms LTLAcc.kbelow_pos #print axioms LTLAcc.kbelow_lt @@ -26,3 +27,5 @@ import Proofs.Consistency #print axioms LTLAcc.take_take_le #print axioms LTLAcc.take_drop_prefix #print axioms LTLAcc.extractConsNode +#print axioms LTLAcc.take_all +#print axioms LTLAcc.consRecBinding diff --git a/verification/Proofs/AxiomCheck.olean b/verification/Proofs/AxiomCheck.olean index 1952ad9..245dfde 100644 Binary files a/verification/Proofs/AxiomCheck.olean and b/verification/Proofs/AxiomCheck.olean differ diff --git a/verification/Proofs/Basic.lean b/verification/Proofs/Basic.lean index e63ab36..454e244 100644 --- a/verification/Proofs/Basic.lean +++ b/verification/Proofs/Basic.lean @@ -139,13 +139,9 @@ noncomputable def ConsRec (n₀ n : Nat) (C : List Hash) (b : Bool) (r : Hash) : Option (Hash × Hash) := if n₀ = n then if b then - match C with - | [] => some (r, r) - | _ => none + (if C = [] then some (r, r) else none) else - match C with - | [s] => some (s, s) - | _ => none + (if C.length = 1 then some (C.getLastD default, C.getLastD default) else none) else if n₀ > n ∨ n₀ = 0 ∨ n ≤ 1 then none else match C.getLast? with diff --git a/verification/Proofs/Basic.olean b/verification/Proofs/Basic.olean index 0bd38bc..3825ce9 100644 Binary files a/verification/Proofs/Basic.olean and b/verification/Proofs/Basic.olean differ diff --git a/verification/Proofs/Binding3.lean b/verification/Proofs/Binding3.lean new file mode 100644 index 0000000..86a5884 --- /dev/null +++ b/verification/Proofs/Binding3.lean @@ -0,0 +1,153 @@ +/- S5.3 — consRecBinding: the paper's Theorem 3 steps 1-2, as a statement + about the extractor's output. Under the maintained value-equality + invariant `y = MTH D₁`, an accepting ConsRec fold either makes + `extractConsNode` output a genuine collision, or its first component is + the honest prefix root `MTH (D₁.take n₀)`. -/ +import Proofs.Consistency + +namespace LTLAcc + +theorem take_all (l : List Bytes) (n : Nat) (h : l.length = n) : l.take n = l := by + subst h; exact List.take_length + +theorem consRecBinding (r : Hash) : + ∀ (n₀ n : Nat) (C : List Hash) (b : Bool) (D₁ : List Bytes) (x y : Hash), + D₁.length = n → 0 < n₀ → n₀ ≤ n → + ConsRec n₀ n C b r = some (x, y) → y = MTH D₁ → + (match extractConsNode n₀ n C b r D₁ with + | some c => IsCollision c.1 c.2 + | none => x = MTH (D₁.take n₀)) := by + intro n₀ n C b + induction n₀, n, C, b using ConsRec.induct r with + | case1 n => + intro D₁ x y hlen hn0 hle hcons hy + rw [ConsRec] at hcons; simp at hcons + obtain ⟨hx, hyr⟩ := hcons + have hext : extractConsNode n n [] true r D₁ = none := by rw [extractConsNode]; simp + simp only [hext] + rw [← hx, hyr, hy, take_all D₁ n hlen] + | case2 n C hCne => + intro D₁ x y hlen hn0 hle hcons hy + rw [ConsRec] at hcons; simp [hCne] at hcons + | case3 n C b hb hC1 => + intro D₁ x y hlen hn0 hle hcons hy + rw [ConsRec] at hcons; simp [hb, hC1] at hcons + obtain ⟨hx, hyr⟩ := hcons + have hext : extractConsNode n n C b r D₁ = none := by rw [extractConsNode]; simp + simp only [hext] + rw [← hx, hyr, hy, take_all D₁ n hlen] + | case4 n C b hb hC1 => + intro D₁ x y hlen hn0 hle hcons hy + rw [ConsRec] at hcons; simp [hb, hC1] at hcons + | case5 n₀ n C b hne hrej => + intro D₁ x y hlen hn0 hle hcons hy + exfalso; omega + | case6 n₀ n C b hne hrej hgl => + intro D₁ x y hlen hn0 hle hcons hy + rw [ConsRec] at hcons + simp only [if_neg hne, if_neg hrej, hgl] at hcons + exact absurd hcons (by simp) + | case7 n₀ n C b hne hrej s hgl k hle2 hsubnone _ih => + intro D₁ x y hlen hn0 hle hcons hy + rw [ConsRec] at hcons + have hk : kbelow n = k := rfl + simp only [if_neg hne, if_neg hrej, hgl, hk, if_pos hle2, hsubnone] at hcons + exact absurd hcons (by simp) + | case8 n₀ n C b hne hrej s hgl k hle2 xx yy hsub ih => + intro D₁ x y hlen hn0 hle hcons hy + have h2 : 2 ≤ n := by omega + have hk : kbelow n = k := rfl + have hkl : k < n := by rw [← hk]; exact kbelow_lt n h2 + rw [ConsRec] at hcons + simp only [if_neg hne, if_neg hrej, hgl, hk, if_pos hle2, hsub, + Option.some.injEq, Prod.mk.injEq] at hcons + obtain ⟨hx, hyv⟩ := hcons + have hsplit : MTH D₁ = hnode (MTH (D₁.take k)) (MTH (D₁.drop k)) := by + have := MTH_split D₁ (by omega); rw [hlen, hk] at this; exact this + have hnodeeq : hnode yy s = hnode (MTH (D₁.take k)) (MTH (D₁.drop k)) := by + rw [hyv, hy, hsplit] + have htklen : (D₁.take k).length = k := by rw [List.length_take, hlen]; omega + rw [extractConsNode] + simp only [if_neg hne, if_neg hrej, hgl, hk, if_pos hle2] + have hy' : (Option.map Prod.snd (ConsRec n₀ k C.dropLast b r)).getD default = yy := by + rw [hsub]; rfl + rw [hy'] + by_cases hpair : yy = MTH (D₁.take k) ∧ s = MTH (D₁.drop k) + · simp only [if_pos hpair] + have hih := ih (D₁.take k) xx yy htklen hn0 hle2 hsub hpair.1 + cases hrec : extractConsNode n₀ k C.dropLast b r (D₁.take k) with + | some c => rw [hrec] at hih; exact hih + | none => + rw [hrec] at hih + have htt : (D₁.take k).take n₀ = D₁.take n₀ := by + rw [List.take_take]; congr 1; omega + rw [← hx, hih, htt] + · simp only [if_neg hpair] + refine ⟨?_, ?_⟩ + · intro hc + injection hc with _ happ + have hln : yy.val.length = (MTH (D₁.take k)).val.length := by + rw [yy.property, (MTH (D₁.take k)).property] + obtain ⟨e1, e2⟩ := List.append_inj happ hln + exact hpair ⟨Subtype.ext e1, Subtype.ext e2⟩ + · show sha256 _ = sha256 _ + have el : sha256 (0x01 :: (yy.val ++ s.val)) = hnode yy s := rfl + have er : sha256 (0x01 :: ((MTH (D₁.take k)).val ++ (MTH (D₁.drop k)).val)) + = hnode (MTH (D₁.take k)) (MTH (D₁.drop k)) := rfl + rw [el, er, hnodeeq] + | case9 n₀ n C b hne hrej s hgl k hle2 hsubnone _ih => + intro D₁ x y hlen hn0 hle hcons hy + rw [ConsRec] at hcons + have hk : kbelow n = k := rfl + simp only [if_neg hne, if_neg hrej, hgl, hk, if_neg hle2, hsubnone] at hcons + exact absurd hcons (by simp) + | case10 n₀ n C b hne hrej s hgl k hle2 xx yy hsub ih => + intro D₁ x y hlen hn0 hle hcons hy + have h2 : 2 ≤ n := by omega + have hk : kbelow n = k := rfl + have hkl : k < n := by rw [← hk]; exact kbelow_lt n h2 + have hkp : 0 < k := by rw [← hk]; exact kbelow_pos n + rw [ConsRec] at hcons + simp only [if_neg hne, if_neg hrej, hgl, hk, if_neg hle2, hsub, + Option.some.injEq, Prod.mk.injEq] at hcons + obtain ⟨hx, hyv⟩ := hcons + have hsplit : MTH D₁ = hnode (MTH (D₁.take k)) (MTH (D₁.drop k)) := by + have := MTH_split D₁ (by omega); rw [hlen, hk] at this; exact this + have hnodeeq : hnode s yy = hnode (MTH (D₁.take k)) (MTH (D₁.drop k)) := by + rw [hyv, hy, hsplit] + have hdklen : (D₁.drop k).length = n - k := by rw [List.length_drop, hlen] + rw [extractConsNode] + simp only [if_neg hne, if_neg hrej, hgl, hk, if_neg hle2] + have hy' : (Option.map Prod.snd (ConsRec (n₀ - k) (n - k) C.dropLast false r)).getD default = yy := by + rw [hsub]; rfl + rw [hy'] + by_cases hpair : s = MTH (D₁.take k) ∧ yy = MTH (D₁.drop k) + · simp only [if_pos hpair] + have hih := ih (D₁.drop k) xx yy hdklen (by omega) (by omega) hsub hpair.2 + cases hrec : extractConsNode (n₀ - k) (n - k) C.dropLast false r (D₁.drop k) with + | some c => rw [hrec] at hih; exact hih + | none => + rw [hrec] at hih + have hn2 : 2 ≤ n₀ := by omega + have hkbn0 : kbelow n₀ = k := kbelow_prefix_eq h2 hk.symm (by omega) hle + have htn0len : (D₁.take n₀).length = n₀ := by rw [List.length_take, hlen]; omega + have hspn0 : MTH (D₁.take n₀) + = hnode (MTH ((D₁.take n₀).take k)) (MTH ((D₁.take n₀).drop k)) := by + have := MTH_split (D₁.take n₀) (by omega); rw [htn0len, hkbn0] at this; exact this + rw [take_take_le D₁ k n₀ (by omega), take_drop_prefix D₁ k n₀] at hspn0 + rw [← hx, hspn0, hpair.1, hih] + · simp only [if_neg hpair] + refine ⟨?_, ?_⟩ + · intro hc + injection hc with _ happ + have hln : s.val.length = (MTH (D₁.take k)).val.length := by + rw [s.property, (MTH (D₁.take k)).property] + obtain ⟨e1, e2⟩ := List.append_inj happ hln + exact hpair ⟨Subtype.ext e1, Subtype.ext e2⟩ + · show sha256 _ = sha256 _ + have el : sha256 (0x01 :: (s.val ++ yy.val)) = hnode s yy := rfl + have er : sha256 (0x01 :: ((MTH (D₁.take k)).val ++ (MTH (D₁.drop k)).val)) + = hnode (MTH (D₁.take k)) (MTH (D₁.drop k)) := rfl + rw [el, er, hnodeeq] + +end LTLAcc diff --git a/verification/Proofs/Binding3.olean b/verification/Proofs/Binding3.olean new file mode 100644 index 0000000..290ee39 Binary files /dev/null and b/verification/Proofs/Binding3.olean differ diff --git a/verification/Proofs/ProbeAx.olean b/verification/Proofs/ProbeAx.olean new file mode 100644 index 0000000..4a6414b Binary files /dev/null and b/verification/Proofs/ProbeAx.olean differ diff --git a/verification/Proofs/ProbeInduct.olean b/verification/Proofs/ProbeInduct.olean new file mode 100644 index 0000000..f451aee Binary files /dev/null and b/verification/Proofs/ProbeInduct.olean differ diff --git a/verification/check.sh b/verification/check.sh index 20cbe0d..b188c4a 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -17,7 +17,7 @@ export LEAN_MEM_MB="${LEAN_MEM_MB:-4096}" CORES="${LEAN_MAX_CORES:-0-3}" GEN_MODULES=( LTLAcc/HashExternal ) -PROOFS=( Basic Completeness Extract Descent Consistency ) +PROOFS=( Basic Completeness Extract Descent Consistency Binding3 ) # Certificates and their exact expected cones (observed at first green # compile, 2026-07-10; any drift in EITHER direction is a failure). @@ -44,6 +44,8 @@ declare -A CONES=( [LTLAcc.take_take_le]="propext, Quot.sound" [LTLAcc.take_drop_prefix]="propext, Classical.choice, Quot.sound" [LTLAcc.extractConsNode]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.take_all]="propext, Quot.sound" + [LTLAcc.consRecBinding]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" ) free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'