diff --git a/verity/SphincsMinusVerifiers/C13ResidualInterface.lean b/verity/SphincsMinusVerifiers/C13ResidualInterface.lean new file mode 100644 index 0000000..88230d3 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualInterface.lean @@ -0,0 +1,20 @@ +import SphincsMinusVerifiers.SegmentLayer3 +import SphincsMinusVerifiers.SegmentLayer3AddressCells + +namespace SphincsMinusVerifiers + +open Compiler.Proofs.IRGeneration.SourceSemantics + +/-- Lightweight C13 WOTS-outer entry state used by the residual assembly +bridges. It is the post-digit state with only the WOTS pointer and loop index +bindings installed, before running the WOTS-outer fold. -/ +def c13BeforeWotsPkLightState (ls : RuntimeState) : RuntimeState := + { SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + (SegmentLayer3.afterDigit ls) with + bindings := + bindValue + (SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + (SegmentLayer3.afterDigit ls)).bindings + "i" (wordNormalize 0) } + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0Assembly.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0Assembly.lean new file mode 100644 index 0000000..10321f7 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0Assembly.lean @@ -0,0 +1,53 @@ +import SphincsMinusVerifiers.C13ResidualLayer0AssemblyFields + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State +open SphincsMinusVerifiers.SegmentCompose + +set_option maxHeartbeats 2000000 in +theorem c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0_proved : + ∀ pkSeed pkRoot message sig sigParsed forsPk specRoot, + C13Concrete.parseSignatureC13 c13 sig = some sigParsed → + forcedZeroOk c13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) = true → + C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk → + foldHypertree C13Concrete.c13PrimitivesConcrete c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers = .ok specRoot → + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + ∀ d : C13Concrete.FoldHypertreeC13OkTwoLayerData + pk digest forsPk sigParsed.layers specRoot, + let st := + c13BeforeWotsPkLightState + (CurrentNodeFrame.c13LayerLoopState0 + (mkC13State pkSeed pkRoot message sig)) + let wotsPtr := lookupValue st.bindings "wotsPtr" + C13WotsOuterExactInputs pkSeed pkRoot message sig st + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk) wotsPtr 1952 := by + intro pkSeed pkRoot message sig sigParsed forsPk specRoot + hParse _hZero hFors _hFold pk digest d + rw [← c13ResidualLayer0GuardState_eq_c13LayerLoopState0 pkSeed pkRoot message sig] + intro st wotsPtr + refine + { hSeed := c13_layer0_exact_seed_field pkSeed pkRoot message sig, + hD := c13_layer0_exact_d_field pkSeed pkRoot message sig sigParsed forsPk d.lsig0 + hParse hFors d.hLayer0, + hAdrs := c13_layer0_exact_adrs_field pkSeed pkRoot message sig sigParsed hParse, + hWPtr := c13_layer0_exact_wptr_field pkSeed pkRoot message sig, + hCdLoad := c13_layer0_exact_cdload_field pkSeed pkRoot message sig } + +#print axioms c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0_proved + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0AssemblyFields.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0AssemblyFields.lean new file mode 100644 index 0000000..7dad7c1 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0AssemblyFields.lean @@ -0,0 +1,136 @@ +import SphincsMinusVerifiers.C13ResidualLayer0Inputs + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.ClimbLoop (foldLoop) +open SphincsMinusVerifiers.MkC13State + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_exact_seed_field + (pkSeed pkRoot message sig : Bytes) : + ∀ j, j < 43 → + ((foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) 0 j).world.memory + 0x00).val = + C13Concrete.wordOfHash16 pkSeed := by + intro j hj + rw [wotsOuterFold_preserves_seed_cell + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) j (by omega)] + exact c13_layer0_light_seed0 pkSeed pkRoot message sig + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_exact_d_field + (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) (forsPk : Bytes) (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hFors : C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk) + (hLayer0 : sigParsed.layers[0]? = some lsig) : + ∀ j, j < 43 → + lookupValue + (foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) 0 j).bindings "d" = + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) + lsig.wots.count (C13Concrete.wordOfHash16 forsPk) := by + intro j _hj + rw [wotsOuterFold_preserves_binding + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) "d" + (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) j] + exact c13_layer0_light_d0 pkSeed pkRoot message sig sigParsed forsPk lsig + hParse hFors hLayer0 + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_exact_adrs_field + (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + ∀ j, j < 43 → + lookupValue + (foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) 0 j).bindings + "wotsAdrs" = + C13Concrete.adrsWotsHashBase 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) := by + intro j _hj + rw [wotsOuterFold_preserves_binding + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) "wotsAdrs" + (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) j] + exact c13_layer0_light_adrs0 pkSeed pkRoot message sig sigParsed hParse + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_exact_wptr_field + (pkSeed pkRoot message sig : Bytes) : + ∀ j, j < 43 → + lookupValue + (foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) 0 j).bindings + "wotsPtr" = + lookupValue + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings + "wotsPtr" := by + intro j _hj + rw [wotsOuterFold_preserves_binding + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) "wotsPtr" + (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) j] + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_exact_cdload_field + (pkSeed pkRoot message sig : Bytes) : + ∀ j, j < 43 → ∀ (s : RuntimeState), + lookupValue s.bindings "wotsPtr" = + lookupValue + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings + "wotsPtr" → + lookupValue s.bindings "i" = j → + s.world = + (foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) 0 j).world → + evalExpr [] s + (.calldataload + (.add (.localVar "wotsPtr") + (.shl (.literal 4) (.localVar "i")))) = + some (Compiler.Proofs.YulGeneration.calldataloadWord 0 + (headWords pkSeed pkRoot message sig.size ++ bytesToWords sig) + (sigDataOffset + (1952 + 16 * j))) := by + intro j hj s h1 h2 h3 + have hWPtrVal : + lookupValue + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings + "wotsPtr" = sigDataOffset + 1952 := + c13_layer0_light_wptr0 pkSeed pkRoot message sig + have hCdSt : + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).world.calldata = + headWords pkSeed pkRoot message sig.size ++ bytesToWords sig := + c13_layer0_light_cd0 pkSeed pkRoot message sig + exact wotsOuterFold_cdload_raw pkSeed pkRoot message sig + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) 1952 + (by decide) hCdSt j hj s (h1.trans hWPtrVal) h2 h3 + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0BeforeDigitLookup.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0BeforeDigitLookup.lean new file mode 100644 index 0000000..08afd30 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0BeforeDigitLookup.lean @@ -0,0 +1,33 @@ +import SphincsMinusVerifiers.SegmentLayer3 + +namespace SphincsMinusVerifiers + +open Compiler.Proofs.IRGeneration.SourceSemantics + +theorem c13_beforeDigitLoop_lookup_eq_beforeDigest_of_ne + (ls : RuntimeState) (key : String) + (hneD : "d" ≠ key) (hneSum : "digitSum" ≠ key) : + lookupValue (SegmentLayer3.beforeDigitLoop ls).bindings key = + lookupValue (SegmentLayer3.beforeDigest ls).bindings key := by + have h : execStmtList [] ls + (SegmentLayer3.prefixBeforeDigest ++ + [ Compiler.CompilationModel.Stmt.letVar "d" + (.keccak256 (.literal 0x00) (.literal 0x80)) + , Compiler.CompilationModel.Stmt.letVar "digitSum" (.literal 0) ]) = + .continue (SegmentLayer3.beforeDigitLoop ls) := + SegmentLayer3.beforeDigitLoop_eq ls + rw [MemoryKit.execStmtList_append_continue _ _ _ _ + (SegmentLayer3.beforeDigest_eq ls)] at h + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "d" _ _ rfl)] at h + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "digitSum" _ _ rfl)] at h + have hnil : ∀ (s : RuntimeState), execStmtList [] s [] = StmtResult.continue s := + fun _ => rfl + rw [hnil] at h + have he := StmtResult.continue.inj h + rw [← he] + rw [MemoryKit.lookupValue_bindValue_ne _ "digitSum" key _ hneSum] + rw [MemoryKit.lookupValue_bindValue_ne _ "d" key _ hneD] + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0BeforeDigitSigOff.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0BeforeDigitSigOff.lean new file mode 100644 index 0000000..604641c --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0BeforeDigitSigOff.lean @@ -0,0 +1,27 @@ +import SphincsMinusVerifiers.SegmentLayer3 + +namespace SphincsMinusVerifiers + +open Compiler.Proofs.IRGeneration.SourceSemantics + +theorem c13_beforeDigitLoop_preserves_sigOff (ls : RuntimeState) : + lookupValue (SegmentLayer3.beforeDigitLoop ls).bindings "sigOff" = + lookupValue ls.bindings "sigOff" := by + refine BindingFrame.execStmtList_preserves_lookup "sigOff" + SegmentLayer3.prefixBeforeDigitLoop + ls (SegmentLayer3.beforeDigitLoop ls) ?_ (SegmentLayer3.beforeDigitLoop_eq ls) + intro s s'' stmt hmem hexec + simp [SegmentLayer3.prefixBeforeDigitLoop] at hmem + rcases hmem with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "idxLeaf" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_assignVar_preserves_lookup _ _ "idxTree" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "wotsAdrs" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "countOff" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "count" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "d" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "digitSum" "sigOff" _ (by decide) hexec + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0Facts.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0Facts.lean new file mode 100644 index 0000000..d3261cc --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0Facts.lean @@ -0,0 +1,244 @@ +import SphincsMinusVerifiers.C13ResidualLayer0StateFacts +import SphincsMinusVerifiers.SegmentAcceptSpec +import SphincsMinusVerifiers.SiblingCalldata + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State +open SphincsMinusVerifiers.SegmentCompose + +theorem c13Residual_wotsDigest_lt + (seed : C13Concrete.Word) (layer idxTree idxLeaf count node : Nat) : + C13Concrete.wotsDigest seed layer idxTree idxLeaf count node < 2 ^ 256 := by + simpa [C13Concrete.wotsDigest, Compiler.Constants.evmModulus] using + SphincsMinusVerifiers.KeccakBridge.keccakWords_lt + [seed, C13Concrete.adrsWotsHashBase layer idxTree idxLeaf, node, count] + +theorem c13Residual_afterFinalize_forsPk_of_parse_fors + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) (forsPk : Bytes) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hFors : C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) sigParsed.fors + = some forsPk) : + lookupValue + (SegmentCompose.afterFinalize + (mkC13State pkSeed pkRoot message sig)).bindings + "forsPk" = C13Concrete.wordOfHash16 forsPk := by + let st := mkC13State pkSeed pkRoot message sig + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + have hRoots := + CurrentNodeFrame.rootCells_eq_forsAllRootsC13_of_hMsg_parse_concrete + pk message sig hParse + have hForsPkByte : + forsPk = C13Concrete.hash16OfWord + (C13Concrete.forsPkWordC13 pk digest sigParsed.fors) := by + exact C13Concrete.forsPkFromSigC13_some_eq_hash16_named (v := c13) + (pk := pk) (digest := digest) (fors := sigParsed.fors) hFors + have hForsPkWord : + C13Concrete.forsPkWordC13 pk digest sigParsed.fors = + C13Concrete.wordOfHash16 forsPk := by + rw [hForsPkByte] + exact (SegmentAcceptSpec.forsPkWordC13_roundtrip pk digest sigParsed.fors).symm + have hTd : + lookupValue (afterFors (mkC13State pkSeed pkRoot message sig)).bindings "idxTree0" + = C13Concrete.idxTree0C13 digest := by + show lookupValue (afterFors (mkC13State pkSeed pkRoot message sig)).bindings "idxTree0" + = C13Concrete.idxTree0C13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + rw [C13Concrete.parseSignatureC13_R hParse] + exact CurrentNodeFrame.afterFors_idxTree0_mkC13State pkSeed pkRoot message sig + have hLd : + lookupValue (afterFors (mkC13State pkSeed pkRoot message sig)).bindings "idxLeaf0" + = C13Concrete.idxLeaf0C13 digest := by + show lookupValue (afterFors (mkC13State pkSeed pkRoot message sig)).bindings "idxLeaf0" + = C13Concrete.idxLeaf0C13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + rw [C13Concrete.parseSignatureC13_R hParse] + exact CurrentNodeFrame.afterFors_idxLeaf0_mkC13State pkSeed pkRoot message sig + have hTltd : C13Concrete.idxTree0C13 digest < 2 ^ 11 := + C13Concrete.idxTree0C13_lt pk sigParsed.R message + have hForsCompress : + CurrentNodeFrame.forsPkCompressWord (afterFors st) = + C13Concrete.wordOfHash16 forsPk := by + rw [CurrentNodeFrame.forsPkCompressWord_eq_of_afterFors_concrete_mkC13State_six_plus_last + pkSeed pkRoot message sig digest (C13Concrete.forsAllRootsC13 pk digest sigParsed.fors) + (C13Concrete.forsAllRootsC13_length pk digest sigParsed.fors) hTd hTltd hLd] + · simpa [pk, digest, C13Concrete.forsPkWordC13] using hForsPkWord + · intro j hj + simpa [pk, digest] using hRoots.1 j hj + · simpa [pk, digest] using hRoots.2 + exact CurrentNodeFrame.afterFinalize_forsPk_of_compress st forsPk hForsCompress + +theorem c13ResidualLayer0BeforeDigest_wotsAdrs_hyperIndex + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + lookupValue + (SegmentLayer3.beforeDigest + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings + "wotsAdrs" = + C13Concrete.adrsWotsHashBase + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) := by + intro pk digest + exact SegmentLayer3.beforeDigest_wotsAdrs_eq_of_layer_idxTree + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) + 0 digest.hyperIndex + (c13ResidualLayer0GuardState_layer pkSeed pkRoot message sig) + (c13ResidualLayer0GuardState_idxTree_hyperIndex + pkSeed pkRoot message sig hParse) + (by decide : 0 < 2 ^ 32) + (C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message) + +theorem c13ResidualLayer0_wotsAdrs_hyperIndex_norm + (pkSeed pkRoot message : Bytes) (sigParsed : Signature) : + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + wordNormalize + (C13Concrete.adrsWotsHashBase + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048)) + = + C13Concrete.adrsWotsHashBase + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) := by + intro pk digest + have h128 : + (digest.hyperIndex / 2048) <<< 128 < 2 ^ 256 := by + have hnext : digest.hyperIndex / 2048 < 2 ^ 11 := by + simpa using C13Concrete.hMsgC13_hyperIndex_div_2048_lt pk sigParsed.R message + rw [Nat.shiftLeft_eq] + calc + (digest.hyperIndex / 2048) * 2 ^ 128 < 2 ^ 11 * 2 ^ 128 := + Nat.mul_lt_mul_of_pos_right hnext (by decide) + _ < 2 ^ 256 := by decide + have h64 : + (digest.hyperIndex % 2048) <<< 64 < 2 ^ 256 := by + have hleaf : digest.hyperIndex % 2048 < 2048 := + Nat.mod_lt _ (by decide : 0 < 2048) + rw [Nat.shiftLeft_eq] + calc + (digest.hyperIndex % 2048) * 2 ^ 64 < 2048 * 2 ^ 64 := + Nat.mul_lt_mul_of_pos_right hleaf (by decide) + _ < 2 ^ 256 := by decide + have h0 : (0 : Nat) <<< 224 < 2 ^ 256 := by + norm_num [Nat.shiftLeft_eq] + have hinner : + ((digest.hyperIndex / 2048) <<< 128 ||| + ((digest.hyperIndex % 2048) <<< 64)) < 2 ^ 256 := + Nat.bitwise_lt_two_pow h128 h64 + have haddr : + ((0 : Nat) <<< 224 ||| + ((digest.hyperIndex / 2048) <<< 128 ||| + ((digest.hyperIndex % 2048) <<< 64))) < 2 ^ 256 := + Nat.bitwise_lt_two_pow h0 hinner + simpa [C13Concrete.adrsWotsHashBase, Nat.lor_assoc] using + SegmentS2.wordNormalize_of_lt haddr + +theorem c13ResidualLayer0BeforeDigest_wotsAdrs_slot_hyperIndex + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + ((SegmentLayer3.beforeDigest + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).world.memory 0x20).val = + C13Concrete.adrsWotsHashBase + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) := by + intro pk digest + rw [SegmentLayer3.beforeDigest_memory_0x20_eq_of_wotsAdrs + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) + (C13Concrete.adrsWotsHashBase + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048)) + (c13ResidualLayer0BeforeDigest_wotsAdrs_hyperIndex + pkSeed pkRoot message sig sigParsed hParse)] + exact c13ResidualLayer0_wotsAdrs_hyperIndex_norm + pkSeed pkRoot message sigParsed + +theorem c13ResidualLayer0BeforeDigest_currentNode_slot + (pkSeed pkRoot message sig forsPk : Bytes) + (hForsPk : + lookupValue + (SegmentCompose.afterFinalize + (mkC13State pkSeed pkRoot message sig)).bindings + "forsPk" = C13Concrete.wordOfHash16 forsPk) : + ((SegmentLayer3.beforeDigest + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).world.memory 0x40).val = + C13Concrete.wordOfHash16 forsPk := by + exact SegmentLayer3.beforeDigest_memory_0x40_eq_wordOfHash16 + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) forsPk + (by + rw [c13ResidualLayer0GuardState_currentNode] + exact hForsPk) + +theorem c13ResidualLayer0BeforeDigest_count_hyperIndex + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hLayer0 : sigParsed.layers[0]? = some lsig) : + lookupValue + (SegmentLayer3.beforeDigest + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings + "count" = lsig.wots.count := by + have hSigOffRaw : + lookupValue (c13ResidualLayer0GuardState pkSeed pkRoot message sig).bindings + "sigOff" = 1952 := by + rw [c13ResidualLayer0GuardState_sigOff] + exact SegmentS2.wordNormalize_of_lt (by decide : 1952 < 2 ^ 256) + have hRaw := + SegmentLayer3.beforeDigest_count_eq_of_sigBase_sigOff_calldata + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) + sigDataOffset 1952 + (headWords pkSeed pkRoot message sig.size ++ bytesToWords sig) + (c13ResidualLayer0GuardState_sigBase pkSeed pkRoot message sig) + hSigOffRaw + (c13ResidualLayer0GuardState_selector pkSeed pkRoot message sig) + (c13ResidualLayer0GuardState_calldata pkSeed pkRoot message sig) + (by decide : sigDataOffset < 2 ^ 256) + (by decide : 1952 < 2 ^ 256) + (by decide : 1952 + 688 < 2 ^ 256) + (by decide : + sigDataOffset + (1952 + 688) < 2 ^ 256) + rw [SphincsMinusVerifiers.SiblingCalldata.shr224_calldata_eq_readBE4 + pkSeed pkRoot message sig (1952 + 688)] at hRaw + have hCountSpec := + C13Concrete.parseSignatureC13_layer_wots_count + hParse (by decide : 0 < 2) hLayer0 + rw [hCountSpec] + rw [← SphincsMinusVerifiers.SiblingCalldata.readBE4_eq_fold sig (1952 + 688)] + exact hRaw + +theorem c13ResidualLayer0_wotsCount_norm + (sig : Bytes) (sigParsed : Signature) (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hLayer0 : sigParsed.layers[0]? = some lsig) : + wordNormalize lsig.wots.count = lsig.wots.count := by + have hCountSpec := + C13Concrete.parseSignatureC13_layer_wots_count + hParse (by decide : 0 < 2) hLayer0 + rw [hCountSpec] + rw [← SphincsMinusVerifiers.SiblingCalldata.readBE4_eq_fold sig (1952 + 688)] + exact SegmentS2.wordNormalize_of_lt + (lt_trans + (SphincsMinusVerifiers.SiblingCalldata.readBE_lt sig (1952 + 688) 4) + (by decide : 256 ^ 4 < 2 ^ 256)) + +theorem c13ResidualLayer0BeforeDigest_count_slot_hyperIndex + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hLayer0 : sigParsed.layers[0]? = some lsig) : + ((SegmentLayer3.beforeDigest + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).world.memory 0x60).val = + lsig.wots.count := by + rw [SegmentLayer3.beforeDigest_memory_0x60_eq_of_count + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) lsig.wots.count + (c13ResidualLayer0BeforeDigest_count_hyperIndex + pkSeed pkRoot message sig sigParsed lsig hParse hLayer0)] + exact c13ResidualLayer0_wotsCount_norm sig sigParsed lsig hParse hLayer0 + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0InputAdrs.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputAdrs.lean new file mode 100644 index 0000000..265f2d8 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputAdrs.lean @@ -0,0 +1,34 @@ +import SphincsMinusVerifiers.C13ResidualLayer0Facts +import SphincsMinusVerifiers.C13ResidualLayer0BeforeDigitLookup + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_light_adrs0 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + lookupValue + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings "wotsAdrs" = + C13Concrete.adrsWotsHashBase 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsAdrs" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "wotsAdrs" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + rw [c13_beforeDigitLoop_lookup_eq_beforeDigest_of_ne + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + exact c13ResidualLayer0BeforeDigest_wotsAdrs_hyperIndex + pkSeed pkRoot message sig sigParsed hParse + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0InputCd.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputCd.lean new file mode 100644 index 0000000..b2c6b3d --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputCd.lean @@ -0,0 +1,20 @@ +import SphincsMinusVerifiers.C13ResidualLayer0Facts + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_light_cd0 (pkSeed pkRoot message sig : Bytes) : + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).world.calldata = + headWords pkSeed pkRoot message sig.size ++ bytesToWords sig := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [(SegmentLayer3.afterDigit_preserves_selector_calldata + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).2] + exact c13ResidualLayer0GuardState_calldata pkSeed pkRoot message sig + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0InputCommon.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputCommon.lean new file mode 100644 index 0000000..cda6e83 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputCommon.lean @@ -0,0 +1,18 @@ +import SphincsMinusVerifiers.C13ResidualInterface + +namespace SphincsMinusVerifiers + +open Compiler.Proofs.IRGeneration.SourceSemantics + +theorem c13_light_world (ls : RuntimeState) : + (c13BeforeWotsPkLightState ls).world = (SegmentLayer3.afterDigit ls).world := rfl + +theorem c13_light_bindings (ls : RuntimeState) : + (c13BeforeWotsPkLightState ls).bindings = + bindValue + (bindValue (SegmentLayer3.afterDigit ls).bindings "wotsPtr" + ((evalExpr [] (SegmentLayer3.afterDigit ls) + (.add (.localVar "sigBase") (.localVar "sigOff"))).getD 0)) + "i" (wordNormalize 0) := rfl + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0InputD.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputD.lean new file mode 100644 index 0000000..5d21268 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputD.lean @@ -0,0 +1,54 @@ +import SphincsMinusVerifiers.C13ResidualLayer0Facts + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_light_d0 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) (forsPk : Bytes) (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hFors : C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk) + (hLayer0 : sigParsed.layers[0]? = some lsig) : + lookupValue + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings "d" = + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) + lsig.wots.count (C13Concrete.wordOfHash16 forsPk) := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "d" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "d" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) "d" + (by decide) (by decide)] + exact SegmentLayer3.beforeDigitLoop_d_eq_wotsDigest_of_scratch + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) + (C13Concrete.wordOfHash16 pkSeed) 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) + lsig.wots.count + (C13Concrete.wordOfHash16 forsPk) + (c13ResidualLayer0BeforeDigest_seed_slot pkSeed pkRoot message sig) + (c13ResidualLayer0BeforeDigest_wotsAdrs_slot_hyperIndex + pkSeed pkRoot message sig sigParsed hParse) + (c13ResidualLayer0BeforeDigest_currentNode_slot + pkSeed pkRoot message sig forsPk + (c13Residual_afterFinalize_forsPk_of_parse_fors + pkSeed pkRoot message sig sigParsed forsPk hParse hFors)) + (c13ResidualLayer0BeforeDigest_count_slot_hyperIndex + pkSeed pkRoot message sig sigParsed lsig hParse hLayer0) + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0InputSeed.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputSeed.lean new file mode 100644 index 0000000..ffa642a --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputSeed.lean @@ -0,0 +1,18 @@ +import SphincsMinusVerifiers.C13ResidualLayer0Facts + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_light_seed0 (pkSeed pkRoot message sig : Bytes) : + ((c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [SegmentLayer3.afterDigit_preserves_memory_zero] + exact c13ResidualLayer0GuardState_seed_slot pkSeed pkRoot message sig + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0InputWptr.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputWptr.lean new file mode 100644 index 0000000..3b7b060 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0InputWptr.lean @@ -0,0 +1,52 @@ +import SphincsMinusVerifiers.C13ResidualLayer0Facts +import SphincsMinusVerifiers.C13ResidualLayer0BeforeDigitSigOff + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State + +set_option maxHeartbeats 2000000 in +theorem c13_layer0_light_wptr0 (pkSeed pkRoot message sig : Bytes) : + lookupValue + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings "wotsPtr" = + sigDataOffset + 1952 := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsPtr" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_self] + have hSigBase : evalExpr [] + (SegmentLayer3.afterDigit + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) + (.localVar "sigBase") = some sigDataOffset := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings + "sigBase") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) "sigBase" + (by decide) (by decide)] + rw [SegmentLayer3.beforeDigitLoop_preserves_sigBase] + rw [c13ResidualLayer0GuardState_sigBase] + have hSigOff : evalExpr [] + (SegmentLayer3.afterDigit + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) + (.localVar "sigOff") = some 1952 := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).bindings + "sigOff") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13ResidualLayer0GuardState pkSeed pkRoot message sig) "sigOff" + (by decide) (by decide)] + rw [c13_beforeDigitLoop_preserves_sigOff] + rw [c13ResidualLayer0GuardState_sigOff] + rw [SegmentS2.wordNormalize_of_lt (by decide : 1952 < 2 ^ 256)] + rw [SphincsMinusVerifiers.ClimbKeccakStep.evalExpr_add_bounded + _ _ _ _ _ hSigBase hSigOff + (by decide) (by decide) (by decide)] + rfl + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0Inputs.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0Inputs.lean new file mode 100644 index 0000000..877273d --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0Inputs.lean @@ -0,0 +1,6 @@ +import SphincsMinusVerifiers.C13ResidualLayer0InputSeed +import SphincsMinusVerifiers.C13ResidualLayer0InputD +import SphincsMinusVerifiers.C13ResidualLayer0InputAdrs +import SphincsMinusVerifiers.C13ResidualLayer0InputWptr +import SphincsMinusVerifiers.C13ResidualLayer0InputCd +import SphincsMinusVerifiers.C13WotsOuterInputs diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer0StateFacts.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer0StateFacts.lean new file mode 100644 index 0000000..a62e4dc --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer0StateFacts.lean @@ -0,0 +1,143 @@ +import SphincsMinusVerifiers.C13ResidualInterface +import SphincsMinusVerifiers.CurrentNodeFrame + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State +open SphincsMinusVerifiers.SegmentCompose + +private theorem runtimeState_with_bindings_selector + (st : RuntimeState) (bindings : List (String × Nat)) : + ({ st with bindings := bindings } : RuntimeState).selector = st.selector := rfl + +private theorem runtimeState_with_bindings_calldata + (st : RuntimeState) (bindings : List (String × Nat)) : + ({ st with bindings := bindings } : RuntimeState).world.calldata = + st.world.calldata := rfl + +private theorem loopState_selector + (varName : String) (st : RuntimeState) (index : Nat) : + (ClimbLoopGuarded.loopState varName st index).selector = st.selector := rfl + +private theorem loopState_calldata + (varName : String) (st : RuntimeState) (index : Nat) : + (ClimbLoopGuarded.loopState varName st index).world.calldata = + st.world.calldata := rfl + +def c13ResidualLayer0GuardState + (pkSeed pkRoot message sig : Bytes) : RuntimeState := + ClimbLoopGuarded.loopState "layer" + { (SegmentCompose.afterSeed (mkC13State pkSeed pkRoot message sig)) with + bindings := + bindValue + (SegmentCompose.afterSeed + (mkC13State pkSeed pkRoot message sig)).bindings + "layer" (wordNormalize 0) } 0 + +theorem c13ResidualLayer0GuardState_eq_c13LayerLoopState0 + (pkSeed pkRoot message sig : Bytes) : + c13ResidualLayer0GuardState pkSeed pkRoot message sig = + CurrentNodeFrame.c13LayerLoopState0 + (mkC13State pkSeed pkRoot message sig) := rfl + +theorem c13ResidualLayer0GuardState_seed_slot + (pkSeed pkRoot message sig : Bytes) : + ((c13ResidualLayer0GuardState pkSeed pkRoot message sig).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := by + unfold c13ResidualLayer0GuardState + rw [ClimbLoopGuarded.loopState_preserves_memory_val] + rw [MemoryKit.withBindings_preserves_memory_val] + exact CurrentNodeFrame.afterSeed_seed_slot_mkC13State pkSeed pkRoot message sig + +theorem c13ResidualLayer0BeforeDigest_seed_slot + (pkSeed pkRoot message sig : Bytes) : + ((SegmentLayer3.beforeDigest + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := by + rw [SegmentLayer3.beforeDigest_preserves_memory_zero] + exact c13ResidualLayer0GuardState_seed_slot pkSeed pkRoot message sig + +theorem c13ResidualLayer0GuardState_currentNode + (pkSeed pkRoot message sig : Bytes) : + lookupValue (c13ResidualLayer0GuardState pkSeed pkRoot message sig).bindings + "currentNode" = + lookupValue + (SegmentCompose.afterFinalize (mkC13State pkSeed pkRoot message sig)).bindings + "forsPk" := by + unfold c13ResidualLayer0GuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "currentNode" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "currentNode" _ (by decide)] + exact CurrentNodeFrame.afterSeed_currentNode + (mkC13State pkSeed pkRoot message sig) + +theorem c13ResidualLayer0GuardState_idxTree + (pkSeed pkRoot message sig : Bytes) : + lookupValue (c13ResidualLayer0GuardState pkSeed pkRoot message sig).bindings + "idxTree" = + lookupValue + (SegmentCompose.afterFinalize (mkC13State pkSeed pkRoot message sig)).bindings + "htIdx" := by + unfold c13ResidualLayer0GuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "idxTree" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "idxTree" _ (by decide)] + exact CurrentNodeFrame.afterSeed_idxTree + (mkC13State pkSeed pkRoot message sig) + +theorem c13ResidualLayer0GuardState_idxTree_hyperIndex + (pkSeed pkRoot message sig : Bytes) {sigParsed : Signature} + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + lookupValue (c13ResidualLayer0GuardState pkSeed pkRoot message sig).bindings + "idxTree" + = + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex := by + rw [c13ResidualLayer0GuardState_idxTree] + rw [CurrentNodeFrame.afterFinalize_htIdx_mkC13State] + rw [C13Concrete.parseSignatureC13_R hParse] + rfl + +theorem c13ResidualLayer0GuardState_sigOff + (pkSeed pkRoot message sig : Bytes) : + lookupValue (c13ResidualLayer0GuardState pkSeed pkRoot message sig).bindings + "sigOff" = wordNormalize 1952 := by + unfold c13ResidualLayer0GuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "sigOff" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "sigOff" _ (by decide)] + exact CurrentNodeFrame.afterSeed_sigOff + (mkC13State pkSeed pkRoot message sig) + +theorem c13ResidualLayer0GuardState_sigBase + (pkSeed pkRoot message sig : Bytes) : + lookupValue (c13ResidualLayer0GuardState pkSeed pkRoot message sig).bindings + "sigBase" = sigDataOffset := by + unfold c13ResidualLayer0GuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "sigBase" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "sigBase" _ (by decide)] + exact CurrentNodeFrame.afterSeed_sigBase_mkC13State pkSeed pkRoot message sig + +theorem c13ResidualLayer0GuardState_layer + (pkSeed pkRoot message sig : Bytes) : + lookupValue (c13ResidualLayer0GuardState pkSeed pkRoot message sig).bindings + "layer" = 0 := by + unfold c13ResidualLayer0GuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_self] + exact SegmentS2.wordNormalize_of_lt (by decide : 0 < 2 ^ 256) + +theorem c13ResidualLayer0GuardState_selector + (pkSeed pkRoot message sig : Bytes) : + (c13ResidualLayer0GuardState pkSeed pkRoot message sig).selector = 0 := by + unfold c13ResidualLayer0GuardState + rw [loopState_selector, runtimeState_with_bindings_selector] + exact CurrentNodeFrame.afterSeed_selector_mkC13State pkSeed pkRoot message sig + +theorem c13ResidualLayer0GuardState_calldata + (pkSeed pkRoot message sig : Bytes) : + (c13ResidualLayer0GuardState pkSeed pkRoot message sig).world.calldata = + headWords pkSeed pkRoot message sig.size ++ bytesToWords sig := by + unfold c13ResidualLayer0GuardState + rw [loopState_calldata, runtimeState_with_bindings_calldata] + exact CurrentNodeFrame.afterSeed_calldata_mkC13State pkSeed pkRoot message sig + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1AdrsFacts.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1AdrsFacts.lean new file mode 100644 index 0000000..7207fcd --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1AdrsFacts.lean @@ -0,0 +1,114 @@ +import SphincsMinusVerifiers.C13ResidualLayer1StateFacts + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics + +theorem c13ResidualSecondLayerBeforeDigest_wotsAdrs_hyperIndex + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + lookupValue + (SegmentLayer3.beforeDigest + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).bindings + "wotsAdrs" = + C13Concrete.adrsWotsHashBase + 1 ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048) := by + intro pk digest + exact SegmentLayer3.beforeDigest_wotsAdrs_eq_of_layer_idxTree + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) + 1 (digest.hyperIndex / 2048) + (c13ResidualSecondLayerGuardState_layer pkSeed pkRoot message sig) + (c13ResidualSecondLayerGuardState_idxTree_hyperIndex + pkSeed pkRoot message sig hParse) + (by decide : 1 < 2 ^ 32) + (lt_of_le_of_lt + (Nat.div_le_self _ _) + (C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message)) + +theorem c13ResidualSecondLayer_wotsAdrs_hyperIndex_norm + (pkSeed pkRoot message : Bytes) (sigParsed : Signature) : + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + wordNormalize + (C13Concrete.adrsWotsHashBase + 1 ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048)) + = + C13Concrete.adrsWotsHashBase + 1 ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048) := by + intro pk digest + have h128 : + (((digest.hyperIndex / 2048) / 2048) <<< 128) < 2 ^ 256 := by + have hnext : (digest.hyperIndex / 2048) / 2048 < 2 ^ 22 := + lt_of_le_of_lt + (Nat.div_le_self _ _) + (lt_of_le_of_lt + (Nat.div_le_self _ _) + (C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message)) + rw [Nat.shiftLeft_eq] + calc + ((digest.hyperIndex / 2048) / 2048) * 2 ^ 128 < 2 ^ 22 * 2 ^ 128 := + Nat.mul_lt_mul_of_pos_right hnext (by decide) + _ < 2 ^ 256 := by decide + have h64 : + (((digest.hyperIndex / 2048) % 2048) <<< 64) < 2 ^ 256 := by + have hleaf : (digest.hyperIndex / 2048) % 2048 < 2048 := + Nat.mod_lt _ (by decide : 0 < 2048) + rw [Nat.shiftLeft_eq] + calc + ((digest.hyperIndex / 2048) % 2048) * 2 ^ 64 < 2048 * 2 ^ 64 := + Nat.mul_lt_mul_of_pos_right hleaf (by decide) + _ < 2 ^ 256 := by decide + have hLayer : (1 : Nat) <<< 224 < 2 ^ 256 := by + norm_num [Nat.shiftLeft_eq] + have hinner : + (((digest.hyperIndex / 2048) / 2048) <<< 128 ||| + (((digest.hyperIndex / 2048) % 2048) <<< 64)) < 2 ^ 256 := + Nat.bitwise_lt_two_pow h128 h64 + have haddr : + ((1 : Nat) <<< 224 ||| + ((((digest.hyperIndex / 2048) / 2048) <<< 128) ||| + (((digest.hyperIndex / 2048) % 2048) <<< 64))) < 2 ^ 256 := + Nat.bitwise_lt_two_pow hLayer hinner + simpa [C13Concrete.adrsWotsHashBase, Nat.lor_assoc] using + SegmentS2.wordNormalize_of_lt haddr + +theorem c13ResidualSecondLayerBeforeDigest_wotsAdrs_slot_hyperIndex + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + ((SegmentLayer3.beforeDigest + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).world.memory 0x20).val = + C13Concrete.adrsWotsHashBase + 1 ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048) := by + intro pk digest + rw [SegmentLayer3.beforeDigest_memory_0x20_eq_of_wotsAdrs + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) + (C13Concrete.adrsWotsHashBase + 1 ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048)) + (c13ResidualSecondLayerBeforeDigest_wotsAdrs_hyperIndex + pkSeed pkRoot message sig sigParsed hParse)] + exact c13ResidualSecondLayer_wotsAdrs_hyperIndex_norm + pkSeed pkRoot message sigParsed + +theorem c13ResidualSecondLayerBeforeDigest_currentNode_slot + (pkSeed pkRoot message sig root0 : Bytes) + (hCurrent : + lookupValue + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig).bindings + "currentNode" = C13Concrete.wordOfHash16 root0) : + ((SegmentLayer3.beforeDigest + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).world.memory 0x40).val = + C13Concrete.wordOfHash16 root0 := + SegmentLayer3.beforeDigest_memory_0x40_eq_wordOfHash16 + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) root0 hCurrent + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1Assembly.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1Assembly.lean new file mode 100644 index 0000000..f59c8bd --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1Assembly.lean @@ -0,0 +1,120 @@ +import SphincsMinusVerifiers.C13ResidualLayer1Inputs +import SphincsMinusVerifiers.C13WotsPkKeccak + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State +open SphincsMinusVerifiers.SegmentCompose + +set_option maxHeartbeats 2000000 in +theorem c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1_proved : + ∀ pkSeed pkRoot message sig sigParsed forsPk specRoot, + C13Concrete.parseSignatureC13 c13 sig = some sigParsed → + forcedZeroOk c13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) = true → + C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk → + foldHypertree C13Concrete.c13PrimitivesConcrete c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers = .ok specRoot → + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + ∀ d : C13Concrete.FoldHypertreeC13OkTwoLayerData + pk digest forsPk sigParsed.layers specRoot, + ∀ j, (h : j < 43) → + ((ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.copyStep + (ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep + (c13BeforeWotsPkLightState + (CurrentNodeFrame.c13LayerLoopState1 + (mkC13State pkSeed pkRoot message sig))) + 0 43) + 0 43).world.memory (0x40 + 32 * j)).val = + (InitialNodeKeccak.wotsChainsEnd + (C13Concrete.wordOfHash16 pkSeed) 1 + ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048) + (C13Concrete.wordOfHash16 d.root0) d.lsig1.wots)[j]'(by + rw [InitialNodeKeccak.wotsChainsEnd_length] + omega) := by + intro pkSeed pkRoot message sig sigParsed forsPk specRoot + hParse hZero hFors hFold pk digest d + rw [← c13ResidualSecondLayerGuardState_eq_c13LayerLoopState1 pkSeed pkRoot message sig] + have hStepSeed : + ((SegmentLayer3.stepLayer + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := + c13ResidualFirstLayerStep_seed_slot_of_parse + pkSeed pkRoot message sig sigParsed hParse + have hSeed1 := c13_layer1_light_seed1 pkSeed pkRoot message sig hStepSeed + have hCurrent0Root := + c13Residual_layer1_current0Root pkSeed pkRoot message sig sigParsed forsPk specRoot + hParse hZero hFors hFold d + have hD1 := c13_layer1_light_d1 pkSeed pkRoot message sig sigParsed d.root0 d.lsig1 + hParse d.hLayer1 hStepSeed hCurrent0Root + have hAdrs1 := c13_layer1_light_adrs1 pkSeed pkRoot message sig sigParsed hParse + have hWPtrVal := c13_layer1_light_wptr1 pkSeed pkRoot message sig + have hCdSt := c13_layer1_light_cd1 pkSeed pkRoot message sig + have hHyLt : + (C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message).hyperIndex + < 2 ^ 22 := + C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message + have hDigestLt : + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 1 ((digest.hyperIndex / 2048) / 2048) ((digest.hyperIndex / 2048) % 2048) + d.lsig1.wots.count (C13Concrete.wordOfHash16 d.root0) < 2 ^ 256 := + c13Residual_wotsDigest_lt (C13Concrete.wordOfHash16 pkSeed) + 1 ((digest.hyperIndex / 2048) / 2048) ((digest.hyperIndex / 2048) % 2048) + d.lsig1.wots.count (C13Concrete.wordOfHash16 d.root0) + have hAdrsLt : + C13Concrete.adrsWotsHashBase 1 + ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048) < 2 ^ 256 := by + have hT : ((digest.hyperIndex / 2048) / 2048) <<< 128 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + ((digest.hyperIndex / 2048) / 2048) * 2 ^ 128 ≤ 2 ^ 22 * 2 ^ 128 := + Nat.mul_le_mul_right _ + (le_of_lt (Nat.lt_of_le_of_lt (Nat.div_le_self _ _) + (Nat.lt_of_le_of_lt (Nat.div_le_self _ _) hHyLt))) + _ < 2 ^ 256 := by decide + have hL : ((digest.hyperIndex / 2048) % 2048) <<< 64 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + ((digest.hyperIndex / 2048) % 2048) * 2 ^ 64 ≤ 2047 * 2 ^ 64 := + Nat.mul_le_mul_right _ + (Nat.le_of_lt_succ (Nat.mod_lt _ (by decide : 0 < 2048))) + _ < 2 ^ 256 := by decide + have h224 : (1 : Nat) <<< 224 < 2 ^ 256 := by decide + exact Nat.bitwise_lt_two_pow + (Nat.bitwise_lt_two_pow h224 hT) hL + have e : C13WotsOuterEntry pkSeed + (c13BeforeWotsPkLightState + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)) + (C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 1 ((digest.hyperIndex / 2048) / 2048) ((digest.hyperIndex / 2048) % 2048) + d.lsig1.wots.count (C13Concrete.wordOfHash16 d.root0)) + (C13Concrete.adrsWotsHashBase 1 + ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048)) + (sigDataOffset + (1952 + 868)) := + { seed0 := hSeed1, d0 := hD1, adrs0 := hAdrs1, wptr0 := hWPtrVal } + exact + c13Layer1_copyFold43_wotsChainsEnd_cells_of_inputs + pkSeed pkRoot message sig sigParsed + (c13BeforeWotsPkLightState + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)) + ((digest.hyperIndex / 2048) / 2048) ((digest.hyperIndex / 2048) % 2048) + (C13Concrete.wordOfHash16 d.root0) + d.lsig1 hParse d.hLayer1 hDigestLt hAdrsLt e hCdSt + +#print axioms c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1_proved + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1CountFacts.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1CountFacts.lean new file mode 100644 index 0000000..c4eb902 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1CountFacts.lean @@ -0,0 +1,72 @@ +import SphincsMinusVerifiers.C13ResidualLayer1StateFacts + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State + +theorem c13ResidualSecondLayerBeforeDigest_count_hyperIndex + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hLayer1 : sigParsed.layers[1]? = some lsig) : + lookupValue + (SegmentLayer3.beforeDigest + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).bindings + "count" = lsig.wots.count := by + have hRaw := + SegmentLayer3.beforeDigest_count_eq_of_sigBase_sigOff_calldata + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) + sigDataOffset 2820 + (headWords pkSeed pkRoot message sig.size ++ bytesToWords sig) + (c13ResidualSecondLayerGuardState_sigBase pkSeed pkRoot message sig) + (c13ResidualSecondLayerGuardState_sigOff pkSeed pkRoot message sig) + (c13ResidualSecondLayerGuardState_selector pkSeed pkRoot message sig) + (c13ResidualSecondLayerGuardState_calldata pkSeed pkRoot message sig) + (by decide : sigDataOffset < 2 ^ 256) + (by decide : 2820 < 2 ^ 256) + (by decide : 2820 + 688 < 2 ^ 256) + (by decide : + sigDataOffset + (2820 + 688) < 2 ^ 256) + rw [SphincsMinusVerifiers.SiblingCalldata.shr224_calldata_eq_readBE4 + pkSeed pkRoot message sig (2820 + 688)] at hRaw + have hCountSpec := + C13Concrete.parseSignatureC13_layer_wots_count + hParse (by decide : 1 < 2) hLayer1 + rw [hCountSpec] + rw [show 1952 + 868 * 1 + 688 = 2820 + 688 by decide] + rw [← SphincsMinusVerifiers.SiblingCalldata.readBE4_eq_fold sig (2820 + 688)] + exact hRaw + +theorem c13ResidualSecondLayer_wotsCount_norm + (sig : Bytes) (sigParsed : Signature) (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hLayer1 : sigParsed.layers[1]? = some lsig) : + wordNormalize lsig.wots.count = lsig.wots.count := by + have hCountSpec := + C13Concrete.parseSignatureC13_layer_wots_count + hParse (by decide : 1 < 2) hLayer1 + rw [hCountSpec] + rw [show 1952 + 868 * 1 + 688 = 3508 by decide] + rw [← SphincsMinusVerifiers.SiblingCalldata.readBE4_eq_fold sig 3508] + exact SegmentS2.wordNormalize_of_lt + (lt_trans + (SphincsMinusVerifiers.SiblingCalldata.readBE_lt sig 3508 4) + (by decide : 256 ^ 4 < 2 ^ 256)) + +theorem c13ResidualSecondLayerBeforeDigest_count_slot_hyperIndex + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hLayer1 : sigParsed.layers[1]? = some lsig) : + ((SegmentLayer3.beforeDigest + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).world.memory 0x60).val = + lsig.wots.count := by + rw [SegmentLayer3.beforeDigest_memory_0x60_eq_of_count + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) lsig.wots.count + (c13ResidualSecondLayerBeforeDigest_count_hyperIndex + pkSeed pkRoot message sig sigParsed lsig hParse hLayer1)] + exact c13ResidualSecondLayer_wotsCount_norm sig sigParsed lsig hParse hLayer1 + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1Facts.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1Facts.lean new file mode 100644 index 0000000..25bb00e --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1Facts.lean @@ -0,0 +1,4 @@ +import SphincsMinusVerifiers.C13ResidualLayer1StateFacts +import SphincsMinusVerifiers.C13ResidualLayer1AdrsFacts +import SphincsMinusVerifiers.C13ResidualLayer1CountFacts +import SphincsMinusVerifiers.C13ResidualLayer1MerkleBridge diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1FirstMerkleSite.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1FirstMerkleSite.lean new file mode 100644 index 0000000..5ebd7cf --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1FirstMerkleSite.lean @@ -0,0 +1,83 @@ +import SphincsMinusVerifiers.C13ResidualLayer1ScalarFacts +import SphincsMinusVerifiers.SegmentLayer3MerkleFrame + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State + +theorem c13ResidualFirstLayerBeforeMerkle_mIdx_hyperIndex + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + lookupValue + (SegmentLayer3.beforeMerkle + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)).bindings + "mIdx" = digest.hyperIndex % 2048 := by + intro pk digest + exact SegmentLayer3.beforeMerkle_mIdx_eq_of_idxTree + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig) + digest.hyperIndex + (c13ResidualLayer0GuardState_idxTree_hyperIndex + pkSeed pkRoot message sig hParse) + (lt_trans + (C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message) + (by decide : 2 ^ 22 < 2 ^ 256)) + +theorem c13ResidualFirstLayerBeforeMerkle_layerFrozenSite + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + SegmentLayer3MerkleFrame.LayerFrozenSite 0 pkSeed pkRoot message sig + (SegmentLayer3.beforeMerkle + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)) := by + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + let treeAdrs : Nat := C13Concrete.adrsXmssTree 0 (digest.hyperIndex / 2048) + refine ⟨treeAdrs, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · exact + (SegmentLayer3.beforeMerkle_preserves_selector_calldata + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)).1.trans + (c13ResidualLayer0GuardState_selector pkSeed pkRoot message sig) + · exact + (SegmentLayer3.beforeMerkle_preserves_selector_calldata + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)).2.trans + (c13ResidualLayer0GuardState_calldata pkSeed pkRoot message sig) + · have hSigOffRaw : + lookupValue (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig).bindings + "sigOff" = 1952 := by + rw [c13ResidualLayer0GuardState_sigOff] + exact SegmentS2.wordNormalize_of_lt (by decide : 1952 < 2 ^ 256) + have hPtr := + SegmentLayer3.beforeMerkle_merklePtr_eq_of_sigBase_sigOff + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig) + sigDataOffset 1952 + (c13ResidualLayer0GuardState_sigBase pkSeed pkRoot message sig) + hSigOffRaw + (by decide : sigDataOffset < 2 ^ 256) + (by decide : 1952 < 2 ^ 256) + (by decide : 1952 + 688 < 2 ^ 256) + (by decide : 1952 + 692 < 2 ^ 256) + (by decide : sigDataOffset + (1952 + 692) < 2 ^ 256) + simpa using hPtr + · dsimp [treeAdrs] + exact SegmentLayer3.beforeMerkle_treeAdrs_eq_of_layer_idxTree + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig) + 0 digest.hyperIndex + (c13ResidualLayer0GuardState_layer pkSeed pkRoot message sig) + (c13ResidualLayer0GuardState_idxTree_hyperIndex + pkSeed pkRoot message sig hParse) + (by decide : 0 < 2 ^ 32) + (C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message) + · dsimp [treeAdrs] + exact c13Residual_adrsXmssTree_lt_of_bounds 0 (digest.hyperIndex / 2048) + (by decide : 0 < 2 ^ 32) + (lt_of_le_of_lt (Nat.div_le_self _ _) + (C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message)) + · rw [c13ResidualFirstLayerBeforeMerkle_mIdx_hyperIndex + pkSeed pkRoot message sig sigParsed hParse] + exact lt_trans (Nat.mod_lt _ (by decide : 0 < 2048)) + (by decide : 2048 < 2 ^ 256) + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1FirstStateFacts.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1FirstStateFacts.lean new file mode 100644 index 0000000..de661a7 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1FirstStateFacts.lean @@ -0,0 +1,12 @@ +import SphincsMinusVerifiers.C13ResidualLayer0StateFacts + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics + +abbrev c13ResidualFirstLayerGuardState : + Bytes → Bytes → Bytes → Bytes → RuntimeState := + c13ResidualLayer0GuardState + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1Inputs.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1Inputs.lean new file mode 100644 index 0000000..e98348c --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1Inputs.lean @@ -0,0 +1,183 @@ +import SphincsMinusVerifiers.C13ResidualLayer1Facts +import SphincsMinusVerifiers.C13ResidualLayer0Inputs +import SphincsMinusVerifiers.C13ResidualLayer1StepSeedFrame + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State +open SphincsMinusVerifiers.SegmentCompose + +axiom c13ResidualFirstLayerStep_seed_slot_of_parse + (pkSeed pkRoot message sig : Bytes) (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + ((SegmentLayer3.stepLayer + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed + +set_option maxHeartbeats 2000000 in +theorem c13_layer1_light_seed1 (pkSeed pkRoot message sig : Bytes) + (hStepSeed : + ((SegmentLayer3.stepLayer + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed) : + ((c13BeforeWotsPkLightState + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [SegmentLayer3.afterDigit_preserves_memory_zero] + unfold c13ResidualSecondLayerGuardState + rw [ClimbLoopGuarded.loopState_preserves_memory_val] + exact hStepSeed + +axiom c13Residual_layer1_current0Root (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) (forsPk specRoot : Bytes) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hZero : forcedZeroOk c13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) = true) + (hFors : C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk) + (hFold : foldHypertree C13Concrete.c13PrimitivesConcrete c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers = .ok specRoot) + (d : C13Concrete.FoldHypertreeC13OkTwoLayerData + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers specRoot) : + lookupValue (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig).bindings + "currentNode" = C13Concrete.wordOfHash16 d.root0 + +set_option maxHeartbeats 2000000 in +theorem c13_layer1_light_d1 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) (root0 : Bytes) (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hLayer1 : sigParsed.layers[1]? = some lsig) + (hStepSeed : + ((SegmentLayer3.stepLayer + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed) + (hCurrent : + lookupValue (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig).bindings + "currentNode" = C13Concrete.wordOfHash16 root0) : + lookupValue + (c13BeforeWotsPkLightState + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).bindings "d" = + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 1 + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) / 2048) + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) % 2048) + lsig.wots.count (C13Concrete.wordOfHash16 root0) := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "d" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "d" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) "d" + (by decide) (by decide)] + exact SegmentLayer3.beforeDigitLoop_d_eq_wotsDigest_of_scratch + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) + (C13Concrete.wordOfHash16 pkSeed) 1 + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) / 2048) + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) % 2048) + lsig.wots.count + (C13Concrete.wordOfHash16 root0) + (c13ResidualSecondLayerBeforeDigest_seed_slot_of_first_step_seed_slot + pkSeed pkRoot message sig hStepSeed) + (c13ResidualSecondLayerBeforeDigest_wotsAdrs_slot_hyperIndex + pkSeed pkRoot message sig sigParsed hParse) + (c13ResidualSecondLayerBeforeDigest_currentNode_slot + pkSeed pkRoot message sig root0 hCurrent) + (c13ResidualSecondLayerBeforeDigest_count_slot_hyperIndex + pkSeed pkRoot message sig sigParsed lsig hParse hLayer1) + +set_option maxHeartbeats 2000000 in +theorem c13_layer1_light_adrs1 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + lookupValue + (c13BeforeWotsPkLightState + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).bindings "wotsAdrs" = + C13Concrete.adrsWotsHashBase 1 + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) / 2048) + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) % 2048) := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsAdrs" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "wotsAdrs" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + rw [c13_beforeDigitLoop_lookup_eq_beforeDigest_of_ne + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + exact c13ResidualSecondLayerBeforeDigest_wotsAdrs_hyperIndex + pkSeed pkRoot message sig sigParsed hParse + +set_option maxHeartbeats 2000000 in +theorem c13_layer1_light_wptr1 (pkSeed pkRoot message sig : Bytes) : + lookupValue + (c13BeforeWotsPkLightState + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).bindings "wotsPtr" = + sigDataOffset + (1952 + 868) := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsPtr" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_self] + have hSigBase : evalExpr [] + (SegmentLayer3.afterDigit + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)) + (.localVar "sigBase") = some sigDataOffset := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).bindings + "sigBase") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) "sigBase" + (by decide) (by decide)] + rw [SegmentLayer3.beforeDigitLoop_preserves_sigBase] + rw [c13ResidualSecondLayerGuardState_sigBase] + have hSigOff : evalExpr [] + (SegmentLayer3.afterDigit + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)) + (.localVar "sigOff") = some 2820 := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).bindings + "sigOff") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig) "sigOff" + (by decide) (by decide)] + rw [c13_beforeDigitLoop_preserves_sigOff] + rw [c13ResidualSecondLayerGuardState_sigOff] + rw [SphincsMinusVerifiers.ClimbKeccakStep.evalExpr_add_bounded + _ _ _ _ _ hSigBase hSigOff + (by decide) (by decide) (by decide)] + rfl + +set_option maxHeartbeats 2000000 in +theorem c13_layer1_light_cd1 (pkSeed pkRoot message sig : Bytes) : + (c13BeforeWotsPkLightState + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).world.calldata = + headWords pkSeed pkRoot message sig.size ++ bytesToWords sig := by + unfold c13BeforeWotsPkLightState + unfold SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom + rw [(SegmentLayer3.afterDigit_preserves_selector_calldata + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).2] + exact c13ResidualSecondLayerGuardState_calldata pkSeed pkRoot message sig + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1MerkleBridge.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1MerkleBridge.lean new file mode 100644 index 0000000..29b94d7 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1MerkleBridge.lean @@ -0,0 +1,74 @@ +import SphincsMinusVerifiers.C13ResidualLayer1StateFacts + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State + +theorem c13Residual_beforeMerkle_merkleNode_eq_wotsPk (ls : RuntimeState) : + lookupValue (SegmentLayer3.beforeMerkle ls).bindings "merkleNode" = + lookupValue (SegmentLayer3.beforeMerkle ls).bindings "wotsPk" := by + unfold SegmentLayer3.beforeMerkle + rw [show SegmentLayer3.suffixBeforeMerkle = + SegmentLayer3.suffixBeforeMIdx ++ + [ .letVar "mIdx" (.localVar "idxLeaf") + , .letVar "merklePtr" (.add + (.localVar "sigBase") (.localVar "authOff")) ] by rfl] + rw [MemoryKit.execStmtList_append_continue _ _ _ _ (SegmentLayer3.beforeMIdx_eq ls)] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "mIdx" _ _ rfl)] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "merklePtr" _ _ rfl)] + simp only [Compiler.Proofs.IRGeneration.SourceSemantics.execStmtList] + rw [MemoryKit.lookupValue_bindValue_ne _ "merklePtr" "merkleNode" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "mIdx" "merkleNode" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "merklePtr" "wotsPk" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "mIdx" "wotsPk" _ (by decide)] + unfold SegmentLayer3.beforeMIdx SegmentLayer3.suffixBeforeMIdx + rw [MemoryKit.execStmtList_append_continue _ _ _ _ (SegmentLayer3.beforeAuthOff_eq ls)] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "authOff" _ _ rfl)] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "treeAdrs" _ _ rfl)] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "merkleNode" _ _ rfl)] + simp only [Compiler.Proofs.IRGeneration.SourceSemantics.execStmtList] + rw [MemoryKit.lookupValue_bindValue_self] + rw [MemoryKit.lookupValue_bindValue_ne _ "merkleNode" "wotsPk" _ (by decide)] + +theorem c13Residual_beforeMerkle_wotsPk_eq_beforeAuthOff_wotsPk (ls : RuntimeState) : + lookupValue (SegmentLayer3.beforeMerkle ls).bindings "wotsPk" = + lookupValue (SegmentLayer3.beforeAuthOff ls).bindings "wotsPk" := by + unfold SegmentLayer3.beforeMerkle + rw [show SegmentLayer3.suffixBeforeMerkle = + SegmentLayer3.suffixBeforeAuthOff ++ + SegmentLayer3.suffixBeforeMerkle.drop SegmentLayer3.suffixBeforeAuthOff.length by rfl] + rw [MemoryKit.execStmtList_append_continue _ _ _ _ (SegmentLayer3.beforeAuthOff_eq ls)] + simp only [SegmentLayer3.suffixBeforeAuthOff, SegmentLayer3.suffixBeforeMerkle, + List.length_cons, List.length_nil, List.drop] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "authOff" _ _ rfl)] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "treeAdrs" _ _ rfl)] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "merkleNode" _ _ rfl)] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "mIdx" _ _ rfl)] + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "merklePtr" _ _ rfl)] + simp only [Compiler.Proofs.IRGeneration.SourceSemantics.execStmtList] + rw [MemoryKit.lookupValue_bindValue_ne _ "merklePtr" "wotsPk" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "mIdx" "wotsPk" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "merkleNode" "wotsPk" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "treeAdrs" "wotsPk" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "authOff" "wotsPk" _ (by decide)] + +def C13ResidualXmssAuthCdAt + (pkSeed pkRoot message sig : Bytes) (merklePtr : Nat) : Nat → Nat := + fun j => + Compiler.Proofs.YulGeneration.calldataloadWord 0 + (headWords pkSeed pkRoot message sig.size ++ bytesToWords sig) + (merklePtr + 16 * j) + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1ScalarFacts.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1ScalarFacts.lean new file mode 100644 index 0000000..03b47a6 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1ScalarFacts.lean @@ -0,0 +1,39 @@ +import SphincsMinusVerifiers.C13ResidualLayer1StateBase + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics + +theorem c13Residual_adrsXmssTree_lt_of_bounds + (layer treeIdx : Nat) + (hLayer : layer < 2 ^ 32) + (hTree : treeIdx < 2 ^ 22) : + C13Concrete.adrsXmssTree layer treeIdx < 2 ^ 256 := by + have h224 : layer <<< 224 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + layer * 2 ^ 224 < 2 ^ 32 * 2 ^ 224 := + Nat.mul_lt_mul_of_pos_right hLayer (by decide) + _ = 2 ^ 256 := by norm_num [Nat.pow_add] + have h128 : treeIdx <<< 128 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + treeIdx * 2 ^ 128 < 2 ^ 22 * 2 ^ 128 := + Nat.mul_lt_mul_of_pos_right hTree (by decide) + _ < 2 ^ 256 := by decide + have h96 : 2 <<< 96 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + decide + have hinner : (treeIdx <<< 128 ||| 2 <<< 96) < 2 ^ 256 := + Nat.bitwise_lt_two_pow h128 h96 + simpa [C13Concrete.adrsXmssTree, Nat.lor_assoc] using + Nat.bitwise_lt_two_pow h224 hinner + +theorem c13Residual_wordNormalize_mod_2048 (n : Nat) : + wordNormalize (n % 2048) = n % 2048 := + SegmentS2.wordNormalize_of_lt + (lt_trans (Nat.mod_lt n (by decide : 0 < 2048)) + (by decide : 2048 < 2 ^ 256)) + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1SecondStateDef.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1SecondStateDef.lean new file mode 100644 index 0000000..369560e --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1SecondStateDef.lean @@ -0,0 +1,34 @@ +import SphincsMinusVerifiers.C13ResidualLayer1FirstStateFacts + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State + +def c13ResidualSecondLayerGuardState + (pkSeed pkRoot message sig : Bytes) : RuntimeState := + ClimbLoopGuarded.loopState "layer" + (SegmentLayer3.stepLayer + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)) 1 + +theorem c13SecondLayerGuardState_shape + (pkSeed pkRoot message sig : Bytes) : + c13ResidualSecondLayerGuardState pkSeed pkRoot message sig = + ClimbLoopGuarded.loopState "layer" + (SegmentLayer3.stepLayer + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)) 1 := rfl + +theorem c13ResidualSecondLayerGuardState_eq_c13LayerLoopState1 + (pkSeed pkRoot message sig : Bytes) : + c13ResidualSecondLayerGuardState pkSeed pkRoot message sig = + CurrentNodeFrame.c13LayerLoopState1 + (mkC13State pkSeed pkRoot message sig) := by + unfold c13ResidualSecondLayerGuardState c13ResidualFirstLayerGuardState + unfold CurrentNodeFrame.c13LayerLoopState1 + unfold CurrentNodeFrame.c13LayerAfterStep0 + rw [c13ResidualLayer0GuardState_eq_c13LayerLoopState0] + unfold ClimbLoopGuarded.loopState + rfl + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1SeedFacts.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1SeedFacts.lean new file mode 100644 index 0000000..613ee1c --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1SeedFacts.lean @@ -0,0 +1,21 @@ +import SphincsMinusVerifiers.C13ResidualLayer1StateBase + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec + +theorem c13ResidualSecondLayerBeforeDigest_seed_slot_of_first_step_seed_slot + (pkSeed pkRoot message sig : Bytes) + (hStepSeed : + ((SegmentLayer3.stepLayer + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed) : + ((SegmentLayer3.beforeDigest + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := by + rw [SegmentLayer3.beforeDigest_preserves_memory_zero] + unfold c13ResidualSecondLayerGuardState + rw [ClimbLoopGuarded.loopState_preserves_memory_val] + exact hStepSeed + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1StateBase.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1StateBase.lean new file mode 100644 index 0000000..f9a53db --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1StateBase.lean @@ -0,0 +1,6 @@ +import SphincsMinusVerifiers.C13ResidualLayer1FirstStateFacts +import SphincsMinusVerifiers.C13ResidualLayer1SecondStateDef + +namespace SphincsMinusVerifiers + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1StateBindings.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1StateBindings.lean new file mode 100644 index 0000000..1c2bb3a --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1StateBindings.lean @@ -0,0 +1,85 @@ +import SphincsMinusVerifiers.C13ResidualLayer1StateBase + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State + +theorem c13ResidualSecondLayerGuardState_sigBase + (pkSeed pkRoot message sig : Bytes) : + lookupValue (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig).bindings + "sigBase" = sigDataOffset := by + unfold c13ResidualSecondLayerGuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "sigBase" _ (by decide)] + rw [SegmentLayer3.stepLayer_sigBase_eq] + exact c13ResidualLayer0GuardState_sigBase pkSeed pkRoot message sig + +theorem c13ResidualSecondLayerGuardState_sigOff + (pkSeed pkRoot message sig : Bytes) : + lookupValue (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig).bindings + "sigOff" = 2820 := by + unfold c13ResidualSecondLayerGuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "sigOff" _ (by decide)] + have hSigOffRaw : + lookupValue (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig).bindings + "sigOff" = 1952 := by + rw [c13ResidualLayer0GuardState_sigOff] + exact SegmentS2.wordNormalize_of_lt (by decide : 1952 < 2 ^ 256) + exact SegmentLayer3.stepLayer_sigOff_eq_of_sigOff + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig) + 1952 hSigOffRaw + (by decide : 1952 < 2 ^ 256) + (by decide : 1952 + 688 < 2 ^ 256) + (by decide : 1952 + 692 < 2 ^ 256) + (by decide : 1952 + 868 < 2 ^ 256) + +theorem c13ResidualSecondLayerGuardState_layer + (pkSeed pkRoot message sig : Bytes) : + lookupValue (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig).bindings + "layer" = 1 := by + unfold c13ResidualSecondLayerGuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_self] + exact SegmentS2.wordNormalize_of_lt (by decide : 1 < 2 ^ 256) + +theorem c13ResidualSecondLayerGuardState_selector + (pkSeed pkRoot message sig : Bytes) : + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig).selector = 0 := by + unfold c13ResidualSecondLayerGuardState ClimbLoopGuarded.loopState + have hFrame := + SegmentLayer3.stepLayer_preserves_selector_calldata + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig) + rw [hFrame.1] + exact c13ResidualLayer0GuardState_selector pkSeed pkRoot message sig + +theorem c13ResidualSecondLayerGuardState_calldata + (pkSeed pkRoot message sig : Bytes) : + (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig).world.calldata = + headWords pkSeed pkRoot message sig.size ++ bytesToWords sig := by + unfold c13ResidualSecondLayerGuardState ClimbLoopGuarded.loopState + have hFrame := + SegmentLayer3.stepLayer_preserves_selector_calldata + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig) + rw [hFrame.2] + exact c13ResidualLayer0GuardState_calldata pkSeed pkRoot message sig + +theorem c13ResidualSecondLayerGuardState_idxTree_hyperIndex + (pkSeed pkRoot message sig : Bytes) {sigParsed : Signature} + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + lookupValue (c13ResidualSecondLayerGuardState pkSeed pkRoot message sig).bindings + "idxTree" = digest.hyperIndex / 2048 := by + intro pk digest + unfold c13ResidualSecondLayerGuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "idxTree" _ (by decide)] + exact SegmentLayer3.stepLayer_idxTree_eq_of_idxTree + (c13ResidualFirstLayerGuardState pkSeed pkRoot message sig) + digest.hyperIndex + (c13ResidualLayer0GuardState_idxTree_hyperIndex + pkSeed pkRoot message sig hParse) + (lt_trans + (C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message) + (by decide : 2 ^ 22 < 2 ^ 256)) + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1StateFacts.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1StateFacts.lean new file mode 100644 index 0000000..a744d3d --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1StateFacts.lean @@ -0,0 +1,4 @@ +import SphincsMinusVerifiers.C13ResidualLayer1StateBase +import SphincsMinusVerifiers.C13ResidualLayer1SeedFacts +import SphincsMinusVerifiers.C13ResidualLayer1StateBindings +import SphincsMinusVerifiers.C13ResidualLayer1ScalarFacts diff --git a/verity/SphincsMinusVerifiers/C13ResidualLayer1StepSeedFrame.lean b/verity/SphincsMinusVerifiers/C13ResidualLayer1StepSeedFrame.lean new file mode 100644 index 0000000..b9525d7 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualLayer1StepSeedFrame.lean @@ -0,0 +1,5 @@ +import SphincsMinusVerifiers.C13ResidualLayer1FirstMerkleSite + +namespace SphincsMinusVerifiers + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13ResidualRevertedLayer0Assembly.lean b/verity/SphincsMinusVerifiers/C13ResidualRevertedLayer0Assembly.lean new file mode 100644 index 0000000..b451697 --- /dev/null +++ b/verity/SphincsMinusVerifiers/C13ResidualRevertedLayer0Assembly.lean @@ -0,0 +1,105 @@ +import SphincsMinusVerifiers.C13ResidualLayer0Inputs +import SphincsMinusVerifiers.C13WotsPkKeccak + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State +open SphincsMinusVerifiers.SegmentCompose + +set_option maxHeartbeats 2000000 in +theorem c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_proved : + ∀ pkSeed pkRoot message sig sigParsed forsPk, + C13Concrete.parseSignatureC13 c13 sig = some sigParsed → + forcedZeroOk c13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) = true → + C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk → + foldHypertree C13Concrete.c13PrimitivesConcrete c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers = .reverted → + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + ∀ d : C13Concrete.FoldHypertreeC13RevertedLayer1Data + pk digest forsPk sigParsed.layers, + ∀ j, (h : j < 43) → + ((ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.copyStep + (ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) + 0 43) + 0 43).world.memory (0x40 + 32 * j)).val = + (InitialNodeKeccak.wotsChainsEnd + (C13Concrete.wordOfHash16 pkSeed) 0 + (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + (C13Concrete.wordOfHash16 forsPk) d.lsig0.wots)[j]'(by + rw [InitialNodeKeccak.wotsChainsEnd_length] + omega) := by + intro pkSeed pkRoot message sig sigParsed forsPk + hParse _hZero hFors _hFold pk digest d + have hSeed0 := c13_layer0_light_seed0 pkSeed pkRoot message sig + have hD0 := c13_layer0_light_d0 pkSeed pkRoot message sig sigParsed forsPk d.lsig0 + hParse hFors d.hLayer0 + have hAdrs0 := c13_layer0_light_adrs0 pkSeed pkRoot message sig sigParsed hParse + have hWPtrVal := c13_layer0_light_wptr0 pkSeed pkRoot message sig + have hCdSt := c13_layer0_light_cd0 pkSeed pkRoot message sig + have hHyLt : + (C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message).hyperIndex + < 2 ^ 22 := + C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message + have hDigestLt : + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk) < 2 ^ 256 := + c13Residual_wotsDigest_lt (C13Concrete.wordOfHash16 pkSeed) + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk) + have hAdrsLt : + C13Concrete.adrsWotsHashBase 0 + (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) < 2 ^ 256 := by + have hT : (digest.hyperIndex / 2048) <<< 128 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + (digest.hyperIndex / 2048) * 2 ^ 128 ≤ 2 ^ 22 * 2 ^ 128 := + Nat.mul_le_mul_right _ + (le_of_lt (Nat.lt_of_le_of_lt (Nat.div_le_self _ _) hHyLt)) + _ < 2 ^ 256 := by decide + have hL : (digest.hyperIndex % 2048) <<< 64 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + (digest.hyperIndex % 2048) * 2 ^ 64 ≤ 2047 * 2 ^ 64 := + Nat.mul_le_mul_right _ + (Nat.le_of_lt_succ (Nat.mod_lt _ (by decide : 0 < 2048))) + _ < 2 ^ 256 := by decide + have h224 : (0 : Nat) <<< 224 < 2 ^ 256 := by decide + exact Nat.bitwise_lt_two_pow + (Nat.bitwise_lt_two_pow h224 hT) hL + have e : C13WotsOuterEntry pkSeed + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) + (C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk)) + (C13Concrete.adrsWotsHashBase 0 + (digest.hyperIndex / 2048) (digest.hyperIndex % 2048)) + (sigDataOffset + 1952) := + { seed0 := hSeed0, d0 := hD0, adrs0 := hAdrs0, wptr0 := hWPtrVal } + exact + c13RevertedLayer0_copyFold43_wotsChainsEnd_cells_of_inputs + pkSeed pkRoot message sig sigParsed + (c13BeforeWotsPkLightState + (c13ResidualLayer0GuardState pkSeed pkRoot message sig)) + (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + (C13Concrete.wordOfHash16 forsPk) + pk digest forsPk d hParse hDigestLt hAdrsLt e hCdSt + +#print axioms c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_proved + +end SphincsMinusVerifiers diff --git a/verity/SphincsMinusVerifiers/C13WotsOuterInputs.lean b/verity/SphincsMinusVerifiers/C13WotsOuterInputs.lean index 11f2146..a21d2b4 100644 --- a/verity/SphincsMinusVerifiers/C13WotsOuterInputs.lean +++ b/verity/SphincsMinusVerifiers/C13WotsOuterInputs.lean @@ -129,6 +129,38 @@ structure C13WotsOuterEntry (pkSeed : Bytes) (st : RuntimeState) adrs0 : lookupValue st.bindings "wotsAdrs" = adrs wptr0 : lookupValue st.bindings "wotsPtr" = wotsPtr +/-- The exact lightweight facts needed to close a C13 WOTS-outer/copy-chain +cell residual. This deliberately exposes only seed, digest, WOTS address, +WOTS pointer, and the calldata load relation for the lightweight loop state. -/ +structure C13WotsOuterExactInputs + (pkSeed pkRoot message sig : Bytes) (st : RuntimeState) + (layer treeIdx leafIdx count node wotsPtr calldataBase : Nat) : Prop where + hSeed : ∀ j, j < 43 → + ((foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed + hD : ∀ j, j < 43 → + lookupValue (foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).bindings "d" = + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + layer treeIdx leafIdx count node + hAdrs : ∀ j, j < 43 → + lookupValue (foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).bindings + "wotsAdrs" = + C13Concrete.adrsWotsHashBase layer treeIdx leafIdx + hWPtr : ∀ j, j < 43 → + lookupValue (foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).bindings + "wotsPtr" = wotsPtr + hCdLoad : ∀ j, j < 43 → ∀ (s : RuntimeState), + lookupValue s.bindings "wotsPtr" = wotsPtr → + lookupValue s.bindings "i" = j → + s.world = (foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).world → + evalExpr [] s + (.calldataload + (.add (.localVar "wotsPtr") + (.shl (.literal 4) (.localVar "i")))) = + some (Compiler.Proofs.YulGeneration.calldataloadWord 0 + (headWords pkSeed pkRoot message sig.size ++ bytesToWords sig) + (sigDataOffset + (calldataBase + 16 * j))) + namespace C13WotsOuterEntry variable {pkSeed : Bytes} {st : RuntimeState} {digest adrs wotsPtr : Nat} diff --git a/verity/SphincsMinusVerifiers/Proofs.lean b/verity/SphincsMinusVerifiers/Proofs.lean index 231805a..64db01d 100644 --- a/verity/SphincsMinusVerifiers/Proofs.lean +++ b/verity/SphincsMinusVerifiers/Proofs.lean @@ -71,6 +71,10 @@ import SphincsMinusVerifiers.C13BridgePrep import SphincsMinusVerifiers.C13ChainCells import SphincsMinusVerifiers.C13WotsPkKeccak import SphincsMinusVerifiers.KeccakBridge +import SphincsMinusVerifiers.C13ResidualInterface +import SphincsMinusVerifiers.C13ResidualLayer0Assembly +import SphincsMinusVerifiers.C13ResidualLayer1Assembly +import SphincsMinusVerifiers.C13ResidualRevertedLayer0Assembly import SphincsMinusVerifiers.SegmentLayer3AddressCells import SphincsMinusVerifiers.SegmentLayer3MerkleFrame import SphincsMinusVerifiers.SiblingCalldata @@ -10954,17 +10958,6 @@ theorem c13_beforeWotsPk_memory_0x20_eq_lightweight (SegmentLayer3.afterDigit ls)).world.memory 0x20).val := by rw [c13_beforeWotsPk_eq_beforeWotsPkFrom] -/-- Lightweight C13 WOTS-outer entry state used by the single-cell historical -bridges. -/ -def c13BeforeWotsPkLightState (ls : RuntimeState) : RuntimeState := - { SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom - (SegmentLayer3.afterDigit ls) with - bindings := - bindValue - (SegmentLayer3AddressCells.beforeWotsPkWotsPtrFrom - (SegmentLayer3.afterDigit ls)).bindings - "i" (wordNormalize 0) } - /-- `beforeWotsPkFrom` factors through the post-WOTS/address-store cutpoint and the final copy loop (`beforeWotsPkAfterWotsCopyFrom`); proven by exec-list rewriting only — no loop iteration is ever unfolded. -/ @@ -11148,38 +11141,6 @@ theorem c13_beforeWotsPk_memory_chain_eq_lightweight (c13_copyLoop_preserves_out_slot _ 0 43 j hj' (by omega)) exact (hA.trans ((c13_awcf_out_slot ls j hj').trans hcell)).trans hB.symm -/-- The exact lightweight facts needed to close a C13 WOTS-outer/copy-chain -cell residual. This deliberately exposes only seed, digest, WOTS address, -WOTS pointer, and the calldata load relation for the lightweight loop state. -/ -structure C13WotsOuterExactInputs - (pkSeed pkRoot message sig : Bytes) (st : RuntimeState) - (layer treeIdx leafIdx count node wotsPtr calldataBase : Nat) : Prop where - hSeed : ∀ j, j < 43 → - ((ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).world.memory 0x00).val = - C13Concrete.wordOfHash16 pkSeed - hD : ∀ j, j < 43 → - lookupValue (ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).bindings "d" = - C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) - layer treeIdx leafIdx count node - hAdrs : ∀ j, j < 43 → - lookupValue (ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).bindings - "wotsAdrs" = - C13Concrete.adrsWotsHashBase layer treeIdx leafIdx - hWPtr : ∀ j, j < 43 → - lookupValue (ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).bindings - "wotsPtr" = wotsPtr - hCdLoad : ∀ j, j < 43 → ∀ (s : RuntimeState), - lookupValue s.bindings "wotsPtr" = wotsPtr → - lookupValue s.bindings "i" = j → - s.world = (ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep st 0 j).world → - evalExpr [] s - (.calldataload - (.add (.localVar "wotsPtr") - (.shl (.literal 4) (.localVar "i")))) = - some (Compiler.Proofs.YulGeneration.calldataloadWord 0 - (headWords pkSeed pkRoot message sig.size ++ bytesToWords sig) - (sigDataOffset + (calldataBase + 16 * j))) - /-- C13 accept-side layer-0 WOTS-PK address cell at the `beforeWotsPk` cutpoint, discharged from the executable WOTS-PK address store. -/ theorem c13_ok_beforeAuthOff_wotsPk_address_cell_residual_layer0 : @@ -11266,7 +11227,7 @@ under cap in `C13WotsPkKeccak.lean` (`c13Layer0_copyFold43_wotsChainsEnd_cells_o remains. Cannot be discharged on the current host: `Proofs.lean`/`SegmentLayer3.lean` each peak ~48 GB as single modules (OOM above the 10 GB cap). Discharge needs a >~64 GB pass; tracked in project memory. -/ -axiom c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0 : +theorem c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0 : ∀ pkSeed pkRoot message sig sigParsed forsPk specRoot, C13Concrete.parseSignatureC13 c13 sig = some sigParsed → forcedZeroOk c13 @@ -11293,7 +11254,8 @@ axiom c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0 : let wotsPtr := lookupValue st.bindings "wotsPtr" C13WotsOuterExactInputs pkSeed pkRoot message sig st 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) - d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk) wotsPtr 1952 + d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk) wotsPtr 1952 := + c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0_proved /-- The layer-0 C13 calldata/loop closure from exact lightweight WOTS-outer inputs to copied chain-end cells: discharged by the verified @@ -11565,19 +11527,8 @@ theorem c13_ok_beforeAuthOff_wotsPk_address_cell_residual_layer1 : (by decide : 2048 < 2 ^ 32)) /-- Residual C13 accept-side layer-1 copied WOTS chain-end cells at the -lightweight WOTS-outer/copy-fold cutpoint. - -ASSEMBLY OBLIGATION (accepted axiom — see README "Residual assembly axioms"). -Asserts the 43 copied chain-end memory cells (`0x40 + 32*j`) equal -`InitialNodeKeccak.wotsChainsEnd … d.root0 …` at the *concrete* layer-1 entry state -`beforeWotsPkWotsPtrFrom (SegmentLayer3.afterDigit (c13LayerLoopState1 (mkC13State …)))`. -Minimal honest assembly obligation: the generic copy-fold/chain-cells closure is already -verified under cap in `C13WotsPkKeccak.lean` -(`c13Layer1_copyFold43_wotsChainsEnd_cells_of_inputs` / `_of_entry`); what remains is only -pinning it to this concrete `afterDigit`-derived state, which needs SegmentLayer3 reasoning. -Cannot be discharged on the current host (Proofs.lean/SegmentLayer3.lean peak ~48 GB, -OOM above the 10 GB cap); needs a >~64 GB pass. -/ -axiom c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1 : +lightweight WOTS-outer/copy-fold cutpoint. -/ +theorem c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1 : ∀ pkSeed pkRoot message sig sigParsed forsPk specRoot, C13Concrete.parseSignatureC13 c13 sig = some sigParsed → forcedZeroOk c13 @@ -11611,7 +11562,8 @@ axiom c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1 : ((digest.hyperIndex / 2048) % 2048) (C13Concrete.wordOfHash16 d.root0) d.lsig1.wots)[j]'(by rw [InitialNodeKeccak.wotsChainsEnd_length] - omega) + omega) := + c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1_proved /-- C13 accept-side layer-1 copied WOTS chain-end cells at the historical `beforeWotsPk` cutpoint, reduced to the lightweight copy-fold residual. -/ @@ -11973,18 +11925,8 @@ theorem c13_reverted_layer0_beforeAuthOff_wotsPk_address_cell_residual : (by decide : 2048 < 2 ^ 32)) /-- Residual C13 reverted-at-layer-1 layer-0 copied WOTS chain-end cells at the -lightweight WOTS-outer/copy-fold cutpoint. - -ASSEMBLY OBLIGATION (accepted axiom — see README "Residual assembly axioms"). -The reverted-path twin of the layer-0 chain-cells closure: asserts the 43 copied -chain-end cells equal `wotsChainsEnd …` at the concrete reverted-layer-0 entry state. -Minimal honest assembly obligation: the generic reverted closure is already verified -under cap in `C13WotsPkKeccak.lean` -(`c13RevertedLayer0_copyFold43_wotsChainsEnd_cells_of_inputs`, -`c13RevertedLayer0_copyFold43_wotsPk_keccak_of_inputs`); only the concrete-state -instantiation (built on `SegmentLayer3.afterDigit`) remains. Cannot be discharged on -the current host (~48 GB OOM above the 10 GB cap); needs a >~64 GB pass. -/ -axiom c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual : +lightweight WOTS-outer/copy-fold cutpoint. -/ +theorem c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual : ∀ pkSeed pkRoot message sig sigParsed forsPk, C13Concrete.parseSignatureC13 c13 sig = some sigParsed → forcedZeroOk c13 @@ -12016,7 +11958,19 @@ axiom c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) (C13Concrete.wordOfHash16 forsPk) d.lsig0.wots)[j]'(by rw [InitialNodeKeccak.wotsChainsEnd_length] - omega) + omega) := by + intro pkSeed pkRoot message sig sigParsed forsPk hParse hZero hFors hFold + pk digest d j h + have hState : + c13FirstLayerGuardState pkSeed pkRoot message sig = + c13ResidualLayer0GuardState pkSeed pkRoot message sig := by + rw [c13FirstLayerGuardState_eq_c13LayerLoopState0, + c13ResidualLayer0GuardState_eq_c13LayerLoopState0] + rw [hState] + exact + c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_proved + pkSeed pkRoot message sig sigParsed forsPk hParse hZero hFors hFold + d j h /-- C13 reverted-at-layer-1 layer-0 copied WOTS chain-end cells at the historical `beforeWotsPk` cutpoint, reduced to the lightweight copy-fold diff --git a/verity/SphincsMinusVerifiers/SegmentLayer3MerkleFrame.lean b/verity/SphincsMinusVerifiers/SegmentLayer3MerkleFrame.lean index aef1f9f..e1b8ac0 100644 --- a/verity/SphincsMinusVerifiers/SegmentLayer3MerkleFrame.lean +++ b/verity/SphincsMinusVerifiers/SegmentLayer3MerkleFrame.lean @@ -671,6 +671,28 @@ theorem stepLayer_preserves_memory_zero_of_layerFrozenSite_range exact afterMerkle_preserves_memory_zero_of_layerFrozenSite_range ls layer pkSeed pkRoot message sig hWots hCopy hlayer hsite +/-- One accepting layer iteration preserves seed cell `0x00` back to the layer +entry state when the frozen Merkle site and WOTS/copy loop frames are supplied. -/ +theorem stepLayer_preserves_entry_memory_zero_of_layerFrozenSite_range + (ls : RuntimeState) (layer : Nat) + (pkSeed pkRoot message sig : ByteArray) + (hWots : + ∀ (s s'' : RuntimeState), + execStmt [] s (.forEach "i" (.literal 43) SegmentLayer3.wotsOuterBody) = .continue s'' → + (s''.world.memory 0x00).val = (s.world.memory 0x00).val) + (hCopy : + ∀ (s s'' : RuntimeState), + execStmt [] s (.forEach "i" (.literal 43) SegmentLayer3.copyBody) = .continue s'' → + (s''.world.memory 0x00).val = (s.world.memory 0x00).val) + (hlayer : layer < 2) + (hsite : LayerFrozenSite layer pkSeed pkRoot message sig (SegmentLayer3.beforeMerkle ls)) : + ((SegmentLayer3.stepLayer ls).world.memory 0x00).val = + (ls.world.memory 0x00).val := by + exact + (stepLayer_preserves_memory_zero_of_layerFrozenSite_range + ls layer pkSeed pkRoot message sig hWots hCopy hlayer hsite).trans + (SegmentLayer3.afterDigit_preserves_memory_zero ls) + /-- One accepting layer iteration preserves seed cell `0x00` once the WOTS/copy loop frames are supplied and the Merkle loop's per-height site facts are reduced to `LayerMerkleEvalFacts`. -/ @@ -708,6 +730,7 @@ theorem stepLayer_preserves_memory_zero_of_layer_eval_range #print axioms foldLoop_preserves_seed_slot_of_layerFrozenSite_range #print axioms afterMerkle_preserves_memory_zero_of_layerFrozenSite_range #print axioms stepLayer_preserves_memory_zero_of_layerFrozenSite_range +#print axioms stepLayer_preserves_entry_memory_zero_of_layerFrozenSite_range #print axioms stepLayer_preserves_memory_zero_of_layer_eval_range end SphincsMinusVerifiers.SegmentLayer3MerkleFrame diff --git a/verity/lakefile.lean b/verity/lakefile.lean index a158b5f..fd13387 100644 --- a/verity/lakefile.lean +++ b/verity/lakefile.lean @@ -48,6 +48,35 @@ lean_lib SphincsMinusVerifiers where `SphincsMinusVerifiers.C13ChainCells, `SphincsMinusVerifiers.C13WotsOuterInputs, `SphincsMinusVerifiers.C13WotsPkKeccak, + `SphincsMinusVerifiers.C13ResidualInterface, + `SphincsMinusVerifiers.C13ResidualLayer0StateFacts, + `SphincsMinusVerifiers.C13ResidualLayer0Facts, + `SphincsMinusVerifiers.C13ResidualLayer0BeforeDigitLookup, + `SphincsMinusVerifiers.C13ResidualLayer0BeforeDigitSigOff, + `SphincsMinusVerifiers.C13ResidualLayer0InputSeed, + `SphincsMinusVerifiers.C13ResidualLayer0InputD, + `SphincsMinusVerifiers.C13ResidualLayer0InputAdrs, + `SphincsMinusVerifiers.C13ResidualLayer0InputWptr, + `SphincsMinusVerifiers.C13ResidualLayer0InputCd, + `SphincsMinusVerifiers.C13ResidualLayer0Inputs, + `SphincsMinusVerifiers.C13ResidualLayer0AssemblyFields, + `SphincsMinusVerifiers.C13ResidualLayer0Assembly, + `SphincsMinusVerifiers.C13ResidualLayer1FirstStateFacts, + `SphincsMinusVerifiers.C13ResidualLayer1SecondStateDef, + `SphincsMinusVerifiers.C13ResidualLayer1StateBase, + `SphincsMinusVerifiers.C13ResidualLayer1SeedFacts, + `SphincsMinusVerifiers.C13ResidualLayer1StateBindings, + `SphincsMinusVerifiers.C13ResidualLayer1ScalarFacts, + `SphincsMinusVerifiers.C13ResidualLayer1StateFacts, + `SphincsMinusVerifiers.C13ResidualLayer1AdrsFacts, + `SphincsMinusVerifiers.C13ResidualLayer1CountFacts, + `SphincsMinusVerifiers.C13ResidualLayer1MerkleBridge, + `SphincsMinusVerifiers.C13ResidualLayer1Facts, + `SphincsMinusVerifiers.C13ResidualLayer1FirstMerkleSite, + `SphincsMinusVerifiers.C13ResidualLayer1StepSeedFrame, + `SphincsMinusVerifiers.C13ResidualLayer1Inputs, + `SphincsMinusVerifiers.C13ResidualLayer1Assembly, + `SphincsMinusVerifiers.C13ResidualRevertedLayer0Assembly, `SphincsMinusVerifiers.SegmentLayer3AddressCells, `SphincsMinusVerifiers.SegmentLayer3, `SphincsMinusVerifiers.SegmentLayer3MerkleFrame, diff --git a/verity/probes/README.md b/verity/probes/README.md new file mode 100644 index 0000000..7234a4d --- /dev/null +++ b/verity/probes/README.md @@ -0,0 +1,39 @@ +# WIP axiom-discharge probes (2026-06-11) + +Standalone probe files validating discharges of the four remaining +composition-glue axioms in `SphincsMinusVerifiers/Proofs.lean` before the +proofs are folded in. Compile from `verity/` with: + +``` +LEAN_NUM_THREADS=2 lake env lean probes/.lean +``` + +(High RAM: ~22 GB RSS each. Run under an RSS watchdog on constrained hosts.) + +- `probe_inputs_layer0.lean` — discharges + `c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0` + (Proofs.lean:11296). Per-fact private lemmas (seed0/d0/adrs0/wptr0/cd0 at + the layer-0 `c13BeforeWotsPkLightState`), each under a fresh + `maxHeartbeats 2000000` budget, consumed via syntactic `rw` against rfl + shape lemmas to avoid whnf blowup of the 64-iteration digit fold. +- `probe_reverted_layer0.lean` — discharges + `c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual` + (Proofs.lean:12014) by reusing the same per-fact lemmas and feeding a + `C13WotsOuterEntry` into + `c13RevertedLayer0_copyFold43_wotsChainsEnd_cells_of_inputs`. +- `probe_layer1.lean` — discharges + `c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1` + (Proofs.lean:11607). Layer-1 analogue of the two layer-0 probes: per-fact + lemmas at the layer-1 `c13BeforeWotsPkLightState` (wotsPtr = + sigDataOffset + (1952 + 868)), feeding a `C13WotsOuterEntry` into + `c13Layer1_copyFold43_wotsChainsEnd_cells_of_inputs`. The `"currentNode"` + fact is derived from the LAYER-0-ONLY residual + `c13_ok_afterMerkle_initial_wotsPk_residual_layer0` (Proofs.lean:11812) — + NOT the layer-1 afterMerkle residual at 11843, which depends on the axiom + being discharged. Folding this proof into Proofs.lean therefore requires + moving the discharged theorem AFTER line 11812 and reordering its + consumers (11645+). + +Once the probes compile with clean `#print axioms`, the helper lemmas and +proofs are folded into Proofs.lean, replacing the two `axiom` declarations, +and this directory is removed. diff --git a/verity/probes/probe_inputs_layer0.lean b/verity/probes/probe_inputs_layer0.lean new file mode 100644 index 0000000..f91381c --- /dev/null +++ b/verity/probes/probe_inputs_layer0.lean @@ -0,0 +1,274 @@ +/- + Probe v2: discharge of the `c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0` + axiom (Proofs.lean:11296), split into per-fact lemmas so each declaration gets + a fresh heartbeat budget and any divergence is localized. +-/ +import SphincsMinusVerifiers.Proofs + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State +open SphincsMinusVerifiers.SegmentCompose + +/-- Lightweight entry state world projection (bindings-only updates). -/ +private theorem probe_light_world (ls : RuntimeState) : + (c13BeforeWotsPkLightState ls).world = (SegmentLayer3.afterDigit ls).world := rfl + +/-- Lightweight entry state bindings shape. -/ +private theorem probe_light_bindings (ls : RuntimeState) : + (c13BeforeWotsPkLightState ls).bindings = + bindValue + (bindValue (SegmentLayer3.afterDigit ls).bindings "wotsPtr" + ((evalExpr [] (SegmentLayer3.afterDigit ls) + (.add (.localVar "sigBase") (.localVar "sigOff"))).getD 0)) + "i" (wordNormalize 0) := rfl + +/-- The two trailing `letVar`s of the pre-checksum prefix (`"d"`, `"digitSum"`) +preserve every other binding from the pre-digest cutpoint. -/ +private theorem probe_beforeDigitLoop_lookup_eq_beforeDigest_of_ne + (ls : RuntimeState) (key : String) + (hneD : "d" ≠ key) (hneSum : "digitSum" ≠ key) : + lookupValue (SegmentLayer3.beforeDigitLoop ls).bindings key = + lookupValue (SegmentLayer3.beforeDigest ls).bindings key := by + have h : execStmtList [] ls + (SegmentLayer3.prefixBeforeDigest ++ + [ Compiler.CompilationModel.Stmt.letVar "d" + (.keccak256 (.literal 0x00) (.literal 0x80)) + , Compiler.CompilationModel.Stmt.letVar "digitSum" (.literal 0) ]) = + .continue (SegmentLayer3.beforeDigitLoop ls) := + SegmentLayer3.beforeDigitLoop_eq ls + rw [MemoryKit.execStmtList_append_continue _ _ _ _ + (SegmentLayer3.beforeDigest_eq ls)] at h + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "d" _ _ rfl)] at h + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "digitSum" _ _ rfl)] at h + have hnil : ∀ (s : RuntimeState), execStmtList [] s [] = StmtResult.continue s := + fun _ => rfl + rw [hnil] at h + have he := StmtResult.continue.inj h + rw [← he] + rw [MemoryKit.lookupValue_bindValue_ne _ "digitSum" key _ hneSum] + rw [MemoryKit.lookupValue_bindValue_ne _ "d" key _ hneD] + +/-- The pre-checksum prefix does not rebind `"sigOff"`. -/ +private theorem probe_beforeDigitLoop_preserves_sigOff (ls : RuntimeState) : + lookupValue (SegmentLayer3.beforeDigitLoop ls).bindings "sigOff" = + lookupValue ls.bindings "sigOff" := by + refine BindingFrame.execStmtList_preserves_lookup "sigOff" + SegmentLayer3.prefixBeforeDigitLoop + ls (SegmentLayer3.beforeDigitLoop ls) ?_ (SegmentLayer3.beforeDigitLoop_eq ls) + intro s s'' stmt hmem hexec + simp [SegmentLayer3.prefixBeforeDigitLoop] at hmem + rcases hmem with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "idxLeaf" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_assignVar_preserves_lookup _ _ "idxTree" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "wotsAdrs" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "countOff" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "count" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "d" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "digitSum" "sigOff" _ (by decide) hexec + +set_option maxHeartbeats 2000000 in +/-- Seed cell at the lightweight entry state. -/ +private theorem probe_seed0 (pkSeed pkRoot message sig : Bytes) : + ((c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := by + rw [probe_light_world] + rw [SegmentLayer3.afterDigit_preserves_memory_zero] + exact c13FirstLayerGuardState_seed_slot pkSeed pkRoot message sig + +set_option maxHeartbeats 2000000 in +/-- `"d"` binding at the lightweight entry state. -/ +private theorem probe_d0 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) (forsPk : Bytes) (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hFors : C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk) + (hLayer0 : sigParsed.layers[0]? = some lsig) : + lookupValue + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings "d" = + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) + lsig.wots.count (C13Concrete.wordOfHash16 forsPk) := by + rw [probe_light_bindings] + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "d" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "d" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "d" + (by decide) (by decide)] + exact SegmentLayer3.beforeDigitLoop_d_eq_wotsDigest_of_scratch + (c13FirstLayerGuardState pkSeed pkRoot message sig) + (C13Concrete.wordOfHash16 pkSeed) 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) + lsig.wots.count + (C13Concrete.wordOfHash16 forsPk) + (c13FirstLayerBeforeDigest_seed_slot pkSeed pkRoot message sig) + (c13FirstLayerBeforeDigest_wotsAdrs_slot_hyperIndex + pkSeed pkRoot message sig sigParsed hParse) + (c13FirstLayerBeforeDigest_currentNode_slot + pkSeed pkRoot message sig forsPk + (c13AfterFinalize_forsPk_of_parse_fors + pkSeed pkRoot message sig sigParsed forsPk hParse hFors)) + (c13FirstLayerBeforeDigest_count_slot_hyperIndex + pkSeed pkRoot message sig sigParsed lsig hParse hLayer0) + +set_option maxHeartbeats 2000000 in +/-- `"wotsAdrs"` binding at the lightweight entry state. -/ +private theorem probe_adrs0 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + lookupValue + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings "wotsAdrs" = + C13Concrete.adrsWotsHashBase 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) := by + rw [probe_light_bindings] + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsAdrs" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "wotsAdrs" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + rw [probe_beforeDigitLoop_lookup_eq_beforeDigest_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + exact c13FirstLayerBeforeDigest_wotsAdrs_hyperIndex + pkSeed pkRoot message sig sigParsed hParse + +set_option maxHeartbeats 2000000 in +/-- `"wotsPtr"` value at the lightweight entry state. -/ +private theorem probe_wptr0 (pkSeed pkRoot message sig : Bytes) : + lookupValue + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings "wotsPtr" = + sigDataOffset + 1952 := by + rw [probe_light_bindings] + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsPtr" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_self] + have hSigBase : evalExpr [] + (SegmentLayer3.afterDigit + (c13FirstLayerGuardState pkSeed pkRoot message sig)) + (.localVar "sigBase") = some sigDataOffset := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings + "sigBase") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "sigBase" + (by decide) (by decide)] + rw [SegmentLayer3.beforeDigitLoop_preserves_sigBase] + rw [c13FirstLayerGuardState_sigBase] + have hSigOff : evalExpr [] + (SegmentLayer3.afterDigit + (c13FirstLayerGuardState pkSeed pkRoot message sig)) + (.localVar "sigOff") = some 1952 := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings + "sigOff") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "sigOff" + (by decide) (by decide)] + rw [probe_beforeDigitLoop_preserves_sigOff] + rw [c13FirstLayerGuardState_sigOff] + rw [SegmentS2.wordNormalize_of_lt (by decide : 1952 < 2 ^ 256)] + rw [SphincsMinusVerifiers.ClimbKeccakStep.evalExpr_add_bounded + _ _ _ _ _ hSigBase hSigOff + (by decide) (by decide) (by decide)] + rfl + +set_option maxHeartbeats 2000000 in +/-- Frozen calldata at the lightweight entry state. -/ +private theorem probe_cd0 (pkSeed pkRoot message sig : Bytes) : + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).world.calldata = + headWords pkSeed pkRoot message sig.size ++ bytesToWords sig := by + rw [probe_light_world] + rw [(SegmentLayer3.afterDigit_preserves_selector_calldata + (c13FirstLayerGuardState pkSeed pkRoot message sig)).2] + exact c13FirstLayerGuardState_calldata pkSeed pkRoot message sig + +set_option maxHeartbeats 2000000 in +/-- Probe twin of the axiom `c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0`. -/ +theorem probe_c13_inputs_layer0 : + ∀ pkSeed pkRoot message sig sigParsed forsPk specRoot, + C13Concrete.parseSignatureC13 c13 sig = some sigParsed → + forcedZeroOk c13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) = true → + C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk → + foldHypertree C13Concrete.c13PrimitivesConcrete c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers = .ok specRoot → + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + ∀ d : C13Concrete.FoldHypertreeC13OkTwoLayerData + pk digest forsPk sigParsed.layers specRoot, + let st := + c13BeforeWotsPkLightState + (CurrentNodeFrame.c13LayerLoopState0 + (mkC13State pkSeed pkRoot message sig)) + let wotsPtr := lookupValue st.bindings "wotsPtr" + C13WotsOuterExactInputs pkSeed pkRoot message sig st + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk) wotsPtr 1952 := by + intro pkSeed pkRoot message sig sigParsed forsPk specRoot + hParse _hZero hFors _hFold pk digest d + rw [← c13FirstLayerGuardState_eq_c13LayerLoopState0 pkSeed pkRoot message sig] + intro st wotsPtr + have hWPtrVal : wotsPtr = sigDataOffset + 1952 := + probe_wptr0 pkSeed pkRoot message sig + have hCdSt : st.world.calldata = + headWords pkSeed pkRoot message sig.size ++ bytesToWords sig := + probe_cd0 pkSeed pkRoot message sig + refine + { hSeed := ?_, hD := ?_, hAdrs := ?_, hWPtr := ?_, hCdLoad := ?_ } + · intro j hj + rw [wotsOuterFold_preserves_seed_cell st j (by omega)] + exact probe_seed0 pkSeed pkRoot message sig + · intro j _hj + rw [wotsOuterFold_preserves_binding st "d" + (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) j] + exact probe_d0 pkSeed pkRoot message sig sigParsed forsPk d.lsig0 + hParse hFors d.hLayer0 + · intro j _hj + rw [wotsOuterFold_preserves_binding st "wotsAdrs" + (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) j] + exact probe_adrs0 pkSeed pkRoot message sig sigParsed hParse + · intro j _hj + rw [wotsOuterFold_preserves_binding st "wotsPtr" + (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) j] + rfl + · intro j hj s h1 h2 h3 + exact wotsOuterFold_cdload_raw pkSeed pkRoot message sig st 1952 + (by decide) hCdSt j hj s (h1.trans hWPtrVal) h2 h3 + +#print axioms probe_c13_inputs_layer0 + +end SphincsMinusVerifiers diff --git a/verity/probes/probe_layer1.lean b/verity/probes/probe_layer1.lean new file mode 100644 index 0000000..263efef --- /dev/null +++ b/verity/probes/probe_layer1.lean @@ -0,0 +1,475 @@ +/- + Probe v2: discharge of the + `c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1` + axiom (Proofs.lean:11607). Layer-1 twin of the ok-path layer-0 probes. + The entry scalar facts at `c13BeforeWotsPkLightState (c13SecondLayerGuardState …)` + feed the verified closure `c13Layer1_copyFold43_wotsChainsEnd_cells_of_inputs`. + + The layer-1 `"currentNode"` fact (the heavy lemma `probe_current0Root`) is + derived through the LAYER-0-ONLY residual + `c13_ok_afterMerkle_initial_wotsPk_residual_layer0`, NOT through the layer-1 + afterMerkle residual (which itself depends on the axiom being discharged). + When folding into Proofs.lean the discharged theorem must therefore MOVE + after line 11812 (`c13_ok_afterMerkle_initial_wotsPk_residual_layer0`) and + its consumers (11645+) reorder below it. + + Split into per-fact lemmas so each declaration gets a fresh heartbeat budget + and any divergence is localized. +-/ +import SphincsMinusVerifiers.Proofs + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State +open SphincsMinusVerifiers.SegmentCompose + +/-- Lightweight entry state world projection (bindings-only updates). -/ +private theorem probe_light_world (ls : RuntimeState) : + (c13BeforeWotsPkLightState ls).world = (SegmentLayer3.afterDigit ls).world := rfl + +/-- Lightweight entry state bindings shape. -/ +private theorem probe_light_bindings (ls : RuntimeState) : + (c13BeforeWotsPkLightState ls).bindings = + bindValue + (bindValue (SegmentLayer3.afterDigit ls).bindings "wotsPtr" + ((evalExpr [] (SegmentLayer3.afterDigit ls) + (.add (.localVar "sigBase") (.localVar "sigOff"))).getD 0)) + "i" (wordNormalize 0) := rfl + +/-- The two trailing `letVar`s of the pre-checksum prefix (`"d"`, `"digitSum"`) +preserve every other binding from the pre-digest cutpoint. -/ +private theorem probe_beforeDigitLoop_lookup_eq_beforeDigest_of_ne + (ls : RuntimeState) (key : String) + (hneD : "d" ≠ key) (hneSum : "digitSum" ≠ key) : + lookupValue (SegmentLayer3.beforeDigitLoop ls).bindings key = + lookupValue (SegmentLayer3.beforeDigest ls).bindings key := by + have h : execStmtList [] ls + (SegmentLayer3.prefixBeforeDigest ++ + [ Compiler.CompilationModel.Stmt.letVar "d" + (.keccak256 (.literal 0x00) (.literal 0x80)) + , Compiler.CompilationModel.Stmt.letVar "digitSum" (.literal 0) ]) = + .continue (SegmentLayer3.beforeDigitLoop ls) := + SegmentLayer3.beforeDigitLoop_eq ls + rw [MemoryKit.execStmtList_append_continue _ _ _ _ + (SegmentLayer3.beforeDigest_eq ls)] at h + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "d" _ _ rfl)] at h + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "digitSum" _ _ rfl)] at h + have hnil : ∀ (s : RuntimeState), execStmtList [] s [] = StmtResult.continue s := + fun _ => rfl + rw [hnil] at h + have he := StmtResult.continue.inj h + rw [← he] + rw [MemoryKit.lookupValue_bindValue_ne _ "digitSum" key _ hneSum] + rw [MemoryKit.lookupValue_bindValue_ne _ "d" key _ hneD] + +/-- The pre-checksum prefix does not rebind `"sigOff"`. -/ +private theorem probe_beforeDigitLoop_preserves_sigOff (ls : RuntimeState) : + lookupValue (SegmentLayer3.beforeDigitLoop ls).bindings "sigOff" = + lookupValue ls.bindings "sigOff" := by + refine BindingFrame.execStmtList_preserves_lookup "sigOff" + SegmentLayer3.prefixBeforeDigitLoop + ls (SegmentLayer3.beforeDigitLoop ls) ?_ (SegmentLayer3.beforeDigitLoop_eq ls) + intro s s'' stmt hmem hexec + simp [SegmentLayer3.prefixBeforeDigitLoop] at hmem + rcases hmem with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "idxLeaf" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_assignVar_preserves_lookup _ _ "idxTree" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "wotsAdrs" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "countOff" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "count" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "d" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "digitSum" "sigOff" _ (by decide) hexec + +set_option maxHeartbeats 2000000 in +/-- Seed cell at the layer-1 lightweight entry state. -/ +private theorem probe_seed1 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + ((c13BeforeWotsPkLightState + (c13SecondLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := by + rw [probe_light_world] + rw [SegmentLayer3.afterDigit_preserves_memory_zero] + unfold c13SecondLayerGuardState + rw [ClimbLoopGuarded.loopState_preserves_memory_val] + exact c13FirstStepLayer_seed_slot_of_memory_zero pkSeed pkRoot message sig + (by + simpa [c13FirstLayerGuardState_eq_c13LayerLoopState0] using + c13FirstLayerStep_preserves_memory_zero_of_parse + pkSeed pkRoot message sig sigParsed hParse) + +set_option maxHeartbeats 2000000 in +/-- The layer-1 guard-state `"currentNode"` binding is the layer-0 spec root, +derived through the LAYER-0-ONLY afterMerkle WOTS-PK residual. -/ +private theorem probe_current0Root (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) (forsPk specRoot : Bytes) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hZero : forcedZeroOk c13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) = true) + (hFors : C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk) + (hFold : foldHypertree C13Concrete.c13PrimitivesConcrete c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers = .ok specRoot) + (d : C13Concrete.FoldHypertreeC13OkTwoLayerData + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers specRoot) : + lookupValue (c13SecondLayerGuardState pkSeed pkRoot message sig).bindings + "currentNode" = C13Concrete.wordOfHash16 d.root0 := by + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + have hWotsPk0 : + C13FoldOkAfterMerkleRawXmssClimbInitialWotsPkDataLayer0 + pkSeed pkRoot message sig sigParsed forsPk specRoot := + c13_ok_afterMerkle_initial_wotsPk_residual_layer0 + pkSeed pkRoot message sig sigParsed forsPk specRoot hParse hZero hFors hFold + have hInit0 : + C13FoldOkAfterMerkleNormalizedXmssClimbInitialFrameDataLayer0 + pkSeed pkRoot message sig sigParsed forsPk specRoot := + c13FoldOkAfterMerkleNormalizedXmssClimbInitialFrameDataLayer0_of_wotsPk + pkSeed pkRoot message sig sigParsed forsPk specRoot hParse hWotsPk0 + have hRawInit0 : + C13FoldOkAfterMerkleRawXmssClimbInitialFrameDataLayer0 + pkSeed pkRoot message sig sigParsed forsPk specRoot := + c13FoldOkAfterMerkleRawXmssClimbInitialFrameDataLayer0_of_wotsPk + pkSeed pkRoot message sig sigParsed forsPk specRoot hParse hWotsPk0 + have hD0 : + ∀ i, i < 11 → + SphincsMinusVerifiers.ClimbMemFrameMerkle.MerkleClimbData + d.lsig0.authPath + (c13XmssAuthCdAt pkSeed pkRoot message sig + (sigDataOffset + (1952 + 868 * 0 + 692))) i := by + simpa [pk, c13XmssAuthCdAt] using + SphincsMinusVerifiers.ClimbMemFrameMerkle.xmss_climb_data_range + pkSeed pkRoot message sig c13 sigParsed d.lsig0 0 + (sigDataOffset + (1952 + 868 * 0 + 692)) + hParse (by decide : 0 < 2) d.hLayer0 rfl + have hTreeLt0 : + C13Concrete.adrsXmssTree 0 (digest.hyperIndex / 2048) < 2 ^ 256 := + c13_adrsXmssTree_lt_of_bounds 0 (digest.hyperIndex / 2048) + (by decide : 0 < 2 ^ 32) + (lt_of_le_of_lt (Nat.div_le_self _ _) + (C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message)) + have hMIdxNorm0 : + wordNormalize (digest.hyperIndex % 2048) = digest.hyperIndex % 2048 := + wordNormalize_mod_2048 digest.hyperIndex + have hAfterRaw : + lookupValue + (SegmentLayer3.afterMerkle + (CurrentNodeFrame.c13LayerLoopState0 + (mkC13State pkSeed pkRoot message sig))).bindings + "merkleNode" + = + C13Concrete.xmssClimb (C13Concrete.wordOfHash16 pkSeed) + (C13Concrete.adrsXmssTree 0 (digest.hyperIndex / 2048)) + 11 0 (digest.hyperIndex % 2048) + (C13Concrete.wordOfHash16 d.wotsPk0) d.lsig0.authPath := by + simpa [pk, digest] using + c13AfterMerkleRawXmssClimb_of_layer_site_bounded + pkSeed pkRoot message sig + (C13Concrete.wordOfHash16 pkSeed) + (C13Concrete.adrsXmssTree 0 (digest.hyperIndex / 2048)) + 0 d.lsig0.authPath + (by decide : 0 < 2) hTreeLt0 + (CurrentNodeFrame.c13LayerLoopState0 + (mkC13State pkSeed pkRoot message sig)) + (digest.hyperIndex % 2048) + (C13Concrete.wordOfHash16 d.wotsPk0) + hD0 + (by simpa [pk, digest] using hInit0 d) + (by simpa [pk, digest] using hRawInit0 d) + hMIdxNorm0 + have hRawStep : + lookupValue + (SegmentLayer3.stepLayer + (CurrentNodeFrame.c13LayerLoopState0 + (mkC13State pkSeed pkRoot message sig))).bindings + "merkleNode" + = + C13Concrete.xmssClimb (C13Concrete.wordOfHash16 pkSeed) + (C13Concrete.adrsXmssTree 0 (digest.hyperIndex / 2048)) + 11 0 (digest.hyperIndex % 2048) + (C13Concrete.wordOfHash16 d.wotsPk0) d.lsig0.authPath := + c13_stepLayer_merkleNode_eq_xmssClimb_of_afterMerkle + (CurrentNodeFrame.c13LayerLoopState0 + (mkC13State pkSeed pkRoot message sig)) + _ _ _ _ _ hAfterRaw + have hMerkle0Root : + lookupValue + (SegmentLayer3.stepLayer + (CurrentNodeFrame.c13LayerLoopState0 + (mkC13State pkSeed pkRoot message sig))).bindings + "merkleNode" + = C13Concrete.wordOfHash16 d.root0 := + SegmentAcceptSpec.stepLayer_merkleNode_eq_wordOfHash16_root_of_xmssClimb_wots_success + pk (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + forsPk d.wotsPk0 d.root0 d.lsig0.wots d.lsig0.authPath + (CurrentNodeFrame.c13LayerLoopState0 + (mkC13State pkSeed pkRoot message sig)) + (by + simpa [pk, digest, C13Concrete.c13PrimitivesConcrete, + C13Concrete.wotsPkFromSigC13AtLayer_zero] using d.hWots0) + (by + simpa [pk, digest, C13Concrete.c13PrimitivesConcrete, + C13Concrete.xmssRootFromSigC13AtLayer_zero] using d.hXmss0) + (by simpa [pk, digest] using hRawStep) + unfold c13SecondLayerGuardState ClimbLoopGuarded.loopState + rw [MemoryKit.lookupValue_bindValue_ne _ "layer" "currentNode" _ (by decide)] + rw [SegmentLayer3.stepLayer_currentNode_eq_merkleNode] + simpa [pk, digest] using hMerkle0Root + +set_option maxHeartbeats 2000000 in +/-- `"d"` binding at the layer-1 lightweight entry state, given the seed-cell +step fact and the layer-0 root `"currentNode"` fact. -/ +private theorem probe_d1 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) (root0 : Bytes) (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hLayer1 : sigParsed.layers[1]? = some lsig) + (hStepSeed : + ((SegmentLayer3.stepLayer + (c13FirstLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed) + (hCurrent : + lookupValue (c13SecondLayerGuardState pkSeed pkRoot message sig).bindings + "currentNode" = C13Concrete.wordOfHash16 root0) : + lookupValue + (c13BeforeWotsPkLightState + (c13SecondLayerGuardState pkSeed pkRoot message sig)).bindings "d" = + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 1 + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) / 2048) + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) % 2048) + lsig.wots.count (C13Concrete.wordOfHash16 root0) := by + rw [probe_light_bindings] + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "d" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "d" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13SecondLayerGuardState pkSeed pkRoot message sig) "d" + (by decide) (by decide)] + exact SegmentLayer3.beforeDigitLoop_d_eq_wotsDigest_of_scratch + (c13SecondLayerGuardState pkSeed pkRoot message sig) + (C13Concrete.wordOfHash16 pkSeed) 1 + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) / 2048) + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) % 2048) + lsig.wots.count + (C13Concrete.wordOfHash16 root0) + (c13SecondLayerBeforeDigest_seed_slot_of_first_step_seed_slot + pkSeed pkRoot message sig hStepSeed) + (c13SecondLayerBeforeDigest_wotsAdrs_slot_hyperIndex + pkSeed pkRoot message sig sigParsed hParse) + (c13SecondLayerBeforeDigest_currentNode_slot + pkSeed pkRoot message sig root0 hCurrent) + (c13SecondLayerBeforeDigest_count_slot_hyperIndex + pkSeed pkRoot message sig sigParsed lsig hParse hLayer1) + +set_option maxHeartbeats 2000000 in +/-- `"wotsAdrs"` binding at the layer-1 lightweight entry state. -/ +private theorem probe_adrs1 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + lookupValue + (c13BeforeWotsPkLightState + (c13SecondLayerGuardState pkSeed pkRoot message sig)).bindings "wotsAdrs" = + C13Concrete.adrsWotsHashBase 1 + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) / 2048) + (((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) % 2048) := by + rw [probe_light_bindings] + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsAdrs" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "wotsAdrs" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13SecondLayerGuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + rw [probe_beforeDigitLoop_lookup_eq_beforeDigest_of_ne + (c13SecondLayerGuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + exact c13SecondLayerBeforeDigest_wotsAdrs_hyperIndex + pkSeed pkRoot message sig sigParsed hParse + +set_option maxHeartbeats 2000000 in +/-- `"wotsPtr"` value at the layer-1 lightweight entry state. -/ +private theorem probe_wptr1 (pkSeed pkRoot message sig : Bytes) : + lookupValue + (c13BeforeWotsPkLightState + (c13SecondLayerGuardState pkSeed pkRoot message sig)).bindings "wotsPtr" = + sigDataOffset + (1952 + 868) := by + rw [probe_light_bindings] + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsPtr" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_self] + have hSigBase : evalExpr [] + (SegmentLayer3.afterDigit + (c13SecondLayerGuardState pkSeed pkRoot message sig)) + (.localVar "sigBase") = some sigDataOffset := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13SecondLayerGuardState pkSeed pkRoot message sig)).bindings + "sigBase") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13SecondLayerGuardState pkSeed pkRoot message sig) "sigBase" + (by decide) (by decide)] + rw [SegmentLayer3.beforeDigitLoop_preserves_sigBase] + rw [c13SecondLayerGuardState_sigBase] + have hSigOff : evalExpr [] + (SegmentLayer3.afterDigit + (c13SecondLayerGuardState pkSeed pkRoot message sig)) + (.localVar "sigOff") = some 2820 := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13SecondLayerGuardState pkSeed pkRoot message sig)).bindings + "sigOff") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13SecondLayerGuardState pkSeed pkRoot message sig) "sigOff" + (by decide) (by decide)] + rw [probe_beforeDigitLoop_preserves_sigOff] + rw [c13SecondLayerGuardState_sigOff] + rw [SphincsMinusVerifiers.ClimbKeccakStep.evalExpr_add_bounded + _ _ _ _ _ hSigBase hSigOff + (by decide) (by decide) (by decide)] + rfl + +set_option maxHeartbeats 2000000 in +/-- Frozen calldata at the layer-1 lightweight entry state. -/ +private theorem probe_cd1 (pkSeed pkRoot message sig : Bytes) : + (c13BeforeWotsPkLightState + (c13SecondLayerGuardState pkSeed pkRoot message sig)).world.calldata = + headWords pkSeed pkRoot message sig.size ++ bytesToWords sig := by + rw [probe_light_world] + rw [(SegmentLayer3.afterDigit_preserves_selector_calldata + (c13SecondLayerGuardState pkSeed pkRoot message sig)).2] + exact c13SecondLayerGuardState_calldata pkSeed pkRoot message sig + +set_option maxHeartbeats 2000000 in +/-- Probe twin of the axiom +`c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1`. -/ +theorem probe_c13_layer1 : + ∀ pkSeed pkRoot message sig sigParsed forsPk specRoot, + C13Concrete.parseSignatureC13 c13 sig = some sigParsed → + forcedZeroOk c13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) = true → + C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk → + foldHypertree C13Concrete.c13PrimitivesConcrete c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers = .ok specRoot → + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + ∀ d : C13Concrete.FoldHypertreeC13OkTwoLayerData + pk digest forsPk sigParsed.layers specRoot, + ∀ j, (h : j < 43) → + ((ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.copyStep + (ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep + (c13BeforeWotsPkLightState + (CurrentNodeFrame.c13LayerLoopState1 + (mkC13State pkSeed pkRoot message sig))) + 0 43) + 0 43).world.memory (0x40 + 32 * j)).val = + (InitialNodeKeccak.wotsChainsEnd + (C13Concrete.wordOfHash16 pkSeed) 1 + ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048) + (C13Concrete.wordOfHash16 d.root0) d.lsig1.wots)[j]'(by + rw [InitialNodeKeccak.wotsChainsEnd_length] + omega) := by + intro pkSeed pkRoot message sig sigParsed forsPk specRoot + hParse hZero hFors hFold pk digest d + rw [← c13SecondLayerGuardState_eq_c13LayerLoopState1 pkSeed pkRoot message sig] + have hStepSeed : + ((SegmentLayer3.stepLayer + (c13FirstLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := + c13FirstStepLayer_seed_slot_of_memory_zero pkSeed pkRoot message sig + (by + simpa [c13FirstLayerGuardState_eq_c13LayerLoopState0] using + c13FirstLayerStep_preserves_memory_zero_of_parse + pkSeed pkRoot message sig sigParsed hParse) + have hSeed1 := probe_seed1 pkSeed pkRoot message sig sigParsed hParse + have hCurrent0Root := + probe_current0Root pkSeed pkRoot message sig sigParsed forsPk specRoot + hParse hZero hFors hFold d + have hD1 := probe_d1 pkSeed pkRoot message sig sigParsed d.root0 d.lsig1 + hParse d.hLayer1 hStepSeed hCurrent0Root + have hAdrs1 := probe_adrs1 pkSeed pkRoot message sig sigParsed hParse + have hWPtrVal := probe_wptr1 pkSeed pkRoot message sig + have hCdSt := probe_cd1 pkSeed pkRoot message sig + have hHyLt : + (C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message).hyperIndex + < 2 ^ 22 := + C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message + have hDigestLt : + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 1 ((digest.hyperIndex / 2048) / 2048) ((digest.hyperIndex / 2048) % 2048) + d.lsig1.wots.count (C13Concrete.wordOfHash16 d.root0) < 2 ^ 256 := + c13_wotsDigest_lt (C13Concrete.wordOfHash16 pkSeed) + 1 ((digest.hyperIndex / 2048) / 2048) ((digest.hyperIndex / 2048) % 2048) + d.lsig1.wots.count (C13Concrete.wordOfHash16 d.root0) + have hAdrsLt : + C13Concrete.adrsWotsHashBase 1 + ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048) < 2 ^ 256 := by + have hT : ((digest.hyperIndex / 2048) / 2048) <<< 128 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + ((digest.hyperIndex / 2048) / 2048) * 2 ^ 128 ≤ 2 ^ 22 * 2 ^ 128 := + Nat.mul_le_mul_right _ + (le_of_lt (Nat.lt_of_le_of_lt (Nat.div_le_self _ _) + (Nat.lt_of_le_of_lt (Nat.div_le_self _ _) hHyLt))) + _ < 2 ^ 256 := by decide + have hL : ((digest.hyperIndex / 2048) % 2048) <<< 64 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + ((digest.hyperIndex / 2048) % 2048) * 2 ^ 64 ≤ 2047 * 2 ^ 64 := + Nat.mul_le_mul_right _ + (Nat.le_of_lt_succ (Nat.mod_lt _ (by decide : 0 < 2048))) + _ < 2 ^ 256 := by decide + have h224 : (1 : Nat) <<< 224 < 2 ^ 256 := by decide + exact Nat.bitwise_lt_two_pow + (Nat.bitwise_lt_two_pow h224 hT) hL + have e : C13WotsOuterEntry pkSeed + (c13BeforeWotsPkLightState + (c13SecondLayerGuardState pkSeed pkRoot message sig)) + (C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 1 ((digest.hyperIndex / 2048) / 2048) ((digest.hyperIndex / 2048) % 2048) + d.lsig1.wots.count (C13Concrete.wordOfHash16 d.root0)) + (C13Concrete.adrsWotsHashBase 1 + ((digest.hyperIndex / 2048) / 2048) + ((digest.hyperIndex / 2048) % 2048)) + (sigDataOffset + (1952 + 868)) := + { seed0 := hSeed1, d0 := hD1, adrs0 := hAdrs1, wptr0 := hWPtrVal } + exact + c13Layer1_copyFold43_wotsChainsEnd_cells_of_inputs + pkSeed pkRoot message sig sigParsed + (c13BeforeWotsPkLightState + (c13SecondLayerGuardState pkSeed pkRoot message sig)) + ((digest.hyperIndex / 2048) / 2048) ((digest.hyperIndex / 2048) % 2048) + (C13Concrete.wordOfHash16 d.root0) + d.lsig1 hParse d.hLayer1 hDigestLt hAdrsLt e hCdSt + +#print axioms probe_c13_layer1 + +end SphincsMinusVerifiers diff --git a/verity/probes/probe_reverted_layer0.lean b/verity/probes/probe_reverted_layer0.lean new file mode 100644 index 0000000..d7f6e35 --- /dev/null +++ b/verity/probes/probe_reverted_layer0.lean @@ -0,0 +1,311 @@ +/- + Probe v2: discharge of the + `c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual` + axiom (Proofs.lean:12014). Same concrete entry state as the ok-path + layer-0 inputs obligation; the entry scalar facts feed the verified + reverted closure `c13RevertedLayer0_copyFold43_wotsChainsEnd_cells_of_inputs`. + Split into per-fact lemmas so each declaration gets a fresh heartbeat + budget and any divergence is localized. +-/ +import SphincsMinusVerifiers.Proofs + +namespace SphincsMinusVerifiers + +open SphincsMinusVerifierSpec +open Compiler.Proofs.IRGeneration.SourceSemantics +open SphincsMinusVerifiers.MkC13State +open SphincsMinusVerifiers.SegmentCompose + +/-- Lightweight entry state world projection (bindings-only updates). -/ +private theorem probe_light_world (ls : RuntimeState) : + (c13BeforeWotsPkLightState ls).world = (SegmentLayer3.afterDigit ls).world := rfl + +/-- Lightweight entry state bindings shape. -/ +private theorem probe_light_bindings (ls : RuntimeState) : + (c13BeforeWotsPkLightState ls).bindings = + bindValue + (bindValue (SegmentLayer3.afterDigit ls).bindings "wotsPtr" + ((evalExpr [] (SegmentLayer3.afterDigit ls) + (.add (.localVar "sigBase") (.localVar "sigOff"))).getD 0)) + "i" (wordNormalize 0) := rfl + +/-- The two trailing `letVar`s of the pre-checksum prefix (`"d"`, `"digitSum"`) +preserve every other binding from the pre-digest cutpoint. -/ +private theorem probe_beforeDigitLoop_lookup_eq_beforeDigest_of_ne + (ls : RuntimeState) (key : String) + (hneD : "d" ≠ key) (hneSum : "digitSum" ≠ key) : + lookupValue (SegmentLayer3.beforeDigitLoop ls).bindings key = + lookupValue (SegmentLayer3.beforeDigest ls).bindings key := by + have h : execStmtList [] ls + (SegmentLayer3.prefixBeforeDigest ++ + [ Compiler.CompilationModel.Stmt.letVar "d" + (.keccak256 (.literal 0x00) (.literal 0x80)) + , Compiler.CompilationModel.Stmt.letVar "digitSum" (.literal 0) ]) = + .continue (SegmentLayer3.beforeDigitLoop ls) := + SegmentLayer3.beforeDigitLoop_eq ls + rw [MemoryKit.execStmtList_append_continue _ _ _ _ + (SegmentLayer3.beforeDigest_eq ls)] at h + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "d" _ _ rfl)] at h + rw [SphincsMinusVerifiers.ClimbKit.execStmtList_cons_continue _ _ _ _ + (MemoryKit.execStmt_letVar_continue _ "digitSum" _ _ rfl)] at h + have hnil : ∀ (s : RuntimeState), execStmtList [] s [] = StmtResult.continue s := + fun _ => rfl + rw [hnil] at h + have he := StmtResult.continue.inj h + rw [← he] + rw [MemoryKit.lookupValue_bindValue_ne _ "digitSum" key _ hneSum] + rw [MemoryKit.lookupValue_bindValue_ne _ "d" key _ hneD] + +/-- The pre-checksum prefix does not rebind `"sigOff"`. -/ +private theorem probe_beforeDigitLoop_preserves_sigOff (ls : RuntimeState) : + lookupValue (SegmentLayer3.beforeDigitLoop ls).bindings "sigOff" = + lookupValue ls.bindings "sigOff" := by + refine BindingFrame.execStmtList_preserves_lookup "sigOff" + SegmentLayer3.prefixBeforeDigitLoop + ls (SegmentLayer3.beforeDigitLoop ls) ?_ (SegmentLayer3.beforeDigitLoop_eq ls) + intro s s'' stmt hmem hexec + simp [SegmentLayer3.prefixBeforeDigitLoop] at hmem + rcases hmem with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "idxLeaf" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_assignVar_preserves_lookup _ _ "idxTree" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "wotsAdrs" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "countOff" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "count" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_mstore_preserves_lookup _ _ "sigOff" _ _ hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "d" "sigOff" _ (by decide) hexec + · exact BindingFrame.execStmt_letVar_preserves_lookup _ _ "digitSum" "sigOff" _ (by decide) hexec + +set_option maxHeartbeats 2000000 in +/-- Seed cell at the lightweight entry state. -/ +private theorem probe_seed0 (pkSeed pkRoot message sig : Bytes) : + ((c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).world.memory 0x00).val = + C13Concrete.wordOfHash16 pkSeed := by + rw [probe_light_world] + rw [SegmentLayer3.afterDigit_preserves_memory_zero] + exact c13FirstLayerGuardState_seed_slot pkSeed pkRoot message sig + +set_option maxHeartbeats 2000000 in +/-- `"d"` binding at the lightweight entry state. -/ +private theorem probe_d0 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) (forsPk : Bytes) (lsig : XmssLayerSig) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) + (hFors : C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk) + (hLayer0 : sigParsed.layers[0]? = some lsig) : + lookupValue + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings "d" = + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) + lsig.wots.count (C13Concrete.wordOfHash16 forsPk) := by + rw [probe_light_bindings] + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "d" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "d" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "d" + (by decide) (by decide)] + exact SegmentLayer3.beforeDigitLoop_d_eq_wotsDigest_of_scratch + (c13FirstLayerGuardState pkSeed pkRoot message sig) + (C13Concrete.wordOfHash16 pkSeed) 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) + lsig.wots.count + (C13Concrete.wordOfHash16 forsPk) + (c13FirstLayerBeforeDigest_seed_slot pkSeed pkRoot message sig) + (c13FirstLayerBeforeDigest_wotsAdrs_slot_hyperIndex + pkSeed pkRoot message sig sigParsed hParse) + (c13FirstLayerBeforeDigest_currentNode_slot + pkSeed pkRoot message sig forsPk + (c13AfterFinalize_forsPk_of_parse_fors + pkSeed pkRoot message sig sigParsed forsPk hParse hFors)) + (c13FirstLayerBeforeDigest_count_slot_hyperIndex + pkSeed pkRoot message sig sigParsed lsig hParse hLayer0) + +set_option maxHeartbeats 2000000 in +/-- `"wotsAdrs"` binding at the lightweight entry state. -/ +private theorem probe_adrs0 (pkSeed pkRoot message sig : Bytes) + (sigParsed : Signature) + (hParse : C13Concrete.parseSignatureC13 c13 sig = some sigParsed) : + lookupValue + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings "wotsAdrs" = + C13Concrete.adrsWotsHashBase 0 + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex / 2048) + ((C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message).hyperIndex % 2048) := by + rw [probe_light_bindings] + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsAdrs" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_ne _ "wotsPtr" "wotsAdrs" _ (by decide)] + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + rw [probe_beforeDigitLoop_lookup_eq_beforeDigest_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "wotsAdrs" + (by decide) (by decide)] + exact c13FirstLayerBeforeDigest_wotsAdrs_hyperIndex + pkSeed pkRoot message sig sigParsed hParse + +set_option maxHeartbeats 2000000 in +/-- `"wotsPtr"` value at the lightweight entry state. -/ +private theorem probe_wptr0 (pkSeed pkRoot message sig : Bytes) : + lookupValue + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings "wotsPtr" = + sigDataOffset + 1952 := by + rw [probe_light_bindings] + rw [MemoryKit.lookupValue_bindValue_ne _ "i" "wotsPtr" _ (by decide)] + rw [MemoryKit.lookupValue_bindValue_self] + have hSigBase : evalExpr [] + (SegmentLayer3.afterDigit + (c13FirstLayerGuardState pkSeed pkRoot message sig)) + (.localVar "sigBase") = some sigDataOffset := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings + "sigBase") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "sigBase" + (by decide) (by decide)] + rw [SegmentLayer3.beforeDigitLoop_preserves_sigBase] + rw [c13FirstLayerGuardState_sigBase] + have hSigOff : evalExpr [] + (SegmentLayer3.afterDigit + (c13FirstLayerGuardState pkSeed pkRoot message sig)) + (.localVar "sigOff") = some 1952 := by + show some (lookupValue + (SegmentLayer3.afterDigit + (c13FirstLayerGuardState pkSeed pkRoot message sig)).bindings + "sigOff") = _ + rw [SegmentLayer3.afterDigit_preserves_lookup_of_ne + (c13FirstLayerGuardState pkSeed pkRoot message sig) "sigOff" + (by decide) (by decide)] + rw [probe_beforeDigitLoop_preserves_sigOff] + rw [c13FirstLayerGuardState_sigOff] + rw [SegmentS2.wordNormalize_of_lt (by decide : 1952 < 2 ^ 256)] + rw [SphincsMinusVerifiers.ClimbKeccakStep.evalExpr_add_bounded + _ _ _ _ _ hSigBase hSigOff + (by decide) (by decide) (by decide)] + rfl + +set_option maxHeartbeats 2000000 in +/-- Frozen calldata at the lightweight entry state. -/ +private theorem probe_cd0 (pkSeed pkRoot message sig : Bytes) : + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)).world.calldata = + headWords pkSeed pkRoot message sig.size ++ bytesToWords sig := by + rw [probe_light_world] + rw [(SegmentLayer3.afterDigit_preserves_selector_calldata + (c13FirstLayerGuardState pkSeed pkRoot message sig)).2] + exact c13FirstLayerGuardState_calldata pkSeed pkRoot message sig + +set_option maxHeartbeats 2000000 in +/-- Probe twin of the axiom +`c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual`. -/ +theorem probe_c13_reverted_layer0 : + ∀ pkSeed pkRoot message sig sigParsed forsPk, + C13Concrete.parseSignatureC13 c13 sig = some sigParsed → + forcedZeroOk c13 + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) = true → + C13Concrete.c13PrimitivesConcrete.forsPkFromSig c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + sigParsed.fors = some forsPk → + foldHypertree C13Concrete.c13PrimitivesConcrete c13 + { pkSeed := pkSeed, pkRoot := pkRoot } + (C13Concrete.c13PrimitivesConcrete.hMsg c13 + { pkSeed := pkSeed, pkRoot := pkRoot } sigParsed.R message) + forsPk sigParsed.layers = .reverted → + let pk : PublicKey := { pkSeed := pkSeed, pkRoot := pkRoot } + let digest := C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message + ∀ d : C13Concrete.FoldHypertreeC13RevertedLayer1Data + pk digest forsPk sigParsed.layers, + ∀ j, (h : j < 43) → + ((ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.copyStep + (ClimbLoop.foldLoop "i" SegmentLayer3CopyCells.wotsOuterStep + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)) + 0 43) + 0 43).world.memory (0x40 + 32 * j)).val = + (InitialNodeKeccak.wotsChainsEnd + (C13Concrete.wordOfHash16 pkSeed) 0 + (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + (C13Concrete.wordOfHash16 forsPk) d.lsig0.wots)[j]'(by + rw [InitialNodeKeccak.wotsChainsEnd_length] + omega) := by + intro pkSeed pkRoot message sig sigParsed forsPk + hParse _hZero hFors _hFold pk digest d + have hSeed0 := probe_seed0 pkSeed pkRoot message sig + have hD0 := probe_d0 pkSeed pkRoot message sig sigParsed forsPk d.lsig0 + hParse hFors d.hLayer0 + have hAdrs0 := probe_adrs0 pkSeed pkRoot message sig sigParsed hParse + have hWPtrVal := probe_wptr0 pkSeed pkRoot message sig + have hCdSt := probe_cd0 pkSeed pkRoot message sig + have hHyLt : + (C13Concrete.c13PrimitivesConcrete.hMsg c13 pk sigParsed.R message).hyperIndex + < 2 ^ 22 := + C13Concrete.hMsgC13_hyperIndex_lt pk sigParsed.R message + have hDigestLt : + C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk) < 2 ^ 256 := + c13_wotsDigest_lt (C13Concrete.wordOfHash16 pkSeed) + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk) + have hAdrsLt : + C13Concrete.adrsWotsHashBase 0 + (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) < 2 ^ 256 := by + have hT : (digest.hyperIndex / 2048) <<< 128 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + (digest.hyperIndex / 2048) * 2 ^ 128 ≤ 2 ^ 22 * 2 ^ 128 := + Nat.mul_le_mul_right _ + (le_of_lt (Nat.lt_of_le_of_lt (Nat.div_le_self _ _) hHyLt)) + _ < 2 ^ 256 := by decide + have hL : (digest.hyperIndex % 2048) <<< 64 < 2 ^ 256 := by + rw [Nat.shiftLeft_eq] + calc + (digest.hyperIndex % 2048) * 2 ^ 64 ≤ 2047 * 2 ^ 64 := + Nat.mul_le_mul_right _ + (Nat.le_of_lt_succ (Nat.mod_lt _ (by decide : 0 < 2048))) + _ < 2 ^ 256 := by decide + have h224 : (0 : Nat) <<< 224 < 2 ^ 256 := by decide + exact Nat.bitwise_lt_two_pow + (Nat.bitwise_lt_two_pow h224 hT) hL + have e : C13WotsOuterEntry pkSeed + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)) + (C13Concrete.wotsDigest (C13Concrete.wordOfHash16 pkSeed) + 0 (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + d.lsig0.wots.count (C13Concrete.wordOfHash16 forsPk)) + (C13Concrete.adrsWotsHashBase 0 + (digest.hyperIndex / 2048) (digest.hyperIndex % 2048)) + (sigDataOffset + 1952) := + { seed0 := hSeed0, d0 := hD0, adrs0 := hAdrs0, wptr0 := hWPtrVal } + exact + c13RevertedLayer0_copyFold43_wotsChainsEnd_cells_of_inputs + pkSeed pkRoot message sig sigParsed + (c13BeforeWotsPkLightState + (c13FirstLayerGuardState pkSeed pkRoot message sig)) + (digest.hyperIndex / 2048) (digest.hyperIndex % 2048) + (C13Concrete.wordOfHash16 forsPk) + pk digest forsPk d hParse hDigestLt hAdrsLt e hCdSt + +#print axioms probe_c13_reverted_layer0 + +end SphincsMinusVerifiers