Discharge the three C13 residual assembly axioms (issue #7)

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

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

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

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

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