Link 5 & 6 of skeleton: lemma 10 of Hachi

ArkLib.lean

@@ -216,6 +216,7 @@ import ArkLib.OracleReduction.Salt
 import ArkLib.OracleReduction.Security.Basic
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Basic
+import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.ChallengeRound
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Composition
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Escape
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Guarded

ArkLib/Commitments/Functional/Hachi/Composition.lean

@@ -100,9 +100,8 @@ seam a home for the `w̃`-commitment's weak-binding break (design G1; `E` abstra
 `coordinateWiseSpecialSound_of_mkWitness_scalar` (`ScalarRound.lean`, consumed only by future
 proofs). *Escape threading* (F2.0): `quadEval_coordinateWiseSpecialSound_withEscape`.
 *Per-link math*: the F2 index bookkeeping (`rlinStmt`/`unstack`/`mem_relOutE_of_relRlinE`),
-Lemma 9 (`lift_coordinateWiseSpecialSound`), the F5 encodings (`Constraints.lean`), the
-un-batching (`mem_relLiftE_of_relBatchedE`), corrected Lemma 10
-(`zeroCheck_coordinateWiseSpecialSound`), the sum-to-point bridge, Lemma 11
+Lemma 9 (`lift_coordinateWiseSpecialSound`), the F5 encodings (`Constraints.lean`), corrected
+Lemma 10 (`zeroCheck_coordinateWiseSpecialSound`), the sum-to-point bridge, Lemma 11
 (`round_coordinateWiseSpecialSound`), F8 (`finalEval_coordinateWiseSpecialSound` + the
 `finalCheck` encoding), G2 (`partialEval_coordinateWiseSpecialSound` + its encoding defs), G3
 (`handoff_coordinateWiseSpecialSound` + `traceCheck`/`toNextQuadEvalStatement`/`hatEval`).
@@ -234,7 +233,7 @@ noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT
     [SampleableType (ShortChallenge 𝓜(q, α) ω)]
     (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) E (liftShort 𝓜(q, α) γ ρBound))
     (φF : ZMod q →+* F)
-    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1) (hb : b - 1 ≤ γ) :
+    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hn : n₀ ≤ 2 ^ m₁) :
     CWSSPackage init impl
       (PolyEvalStatement 𝓜(q, α) innerRows messageDigits outerRows innerDigits dRows m r)
       (QuadEvalWitness 𝓜(q, α) innerRows (2 ^ m) messageDigits (2 ^ r) innerDigits ⊕ E)
@@ -250,7 +249,7 @@ noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT
   evalChainE (b := b) (γ := γ) init impl hq5 hκ hτ K.esc ▷
     rlinPackage (zDigits := zDigits) 𝓜(q, α) init impl (b : ZMod q) ω γ K.esc ▷
     liftPackage 𝓜(q, α) γ ρBound K φF init impl hd ▷
-    batchPackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b hq2 hb ▷
+    batchPackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b hn ▷
     zeroCheckPackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b ▷
     sumcheckBridgePackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b
 
@@ -272,7 +271,7 @@ noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (Sta
     [SampleableType (ShortChallenge 𝓜(q, α) ω)]
     (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) E (liftShort 𝓜(q, α) γ ρBound))
     (φF : ZMod q →+* F)
-    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1) (hb : b - 1 ≤ γ)
+    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hn : n₀ ≤ 2 ^ m₁)
     (zpow : Fin (2 ^ κ) → F)
     (Φ' : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ']
     {innerRows' messageDigits' outerRows' innerDigits' dRows' m' r' : ℕ}
@@ -300,7 +299,7 @@ noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (Sta
           roundsSpec F b (mLow + κ)) ++ₚ pSpecFinalEval F).Challenge i) :=
     ProtocolSpec.instSampleableTypeChallengeAppend (h₁ := i₁)
       (h₂ := instSampleableTypeChallengePSpecFinalEval)
-  (((openCore (m₀ := mLow + κ) (m₁ := m₁) init impl hq5 hκ hτ K φF hd hq2 hb).toGuarded.append
+  (((openCore (m₀ := mLow + κ) (m₁ := m₁) init impl hq5 hκ hτ K φF hd hn).toGuarded.append
       (roundsChain 𝓜(q, α) (mLow + κ) m₁ γ ρBound b init impl K φF (mLow + κ))
       (roundsChain_relIn 𝓜(q, α) (mLow + κ) m₁ γ ρBound b init impl K φF
         (mLow + κ)).symm).append
@@ -322,24 +321,24 @@ theorem hachi_iteration_coordinateWiseSpecialSound (init : ProbComp σ)
     [SampleableType (ShortChallenge 𝓜(q, α) ω)]
     (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) E (liftShort 𝓜(q, α) γ ρBound))
     (φF : ZMod q →+* F)
-    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1) (hb : b - 1 ≤ γ)
+    (hd : 0 < (𝓜(q, α)).φ.natDegree) (hn : n₀ ≤ 2 ^ m₁)
     (zpow : Fin (2 ^ κ) → F)
     (Φ' : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ']
     {innerRows' messageDigits' outerRows' innerDigits' dRows' m' r' : ℕ}
     (pp' : Hachi.PublicParamsD Φ' innerRows' (2 ^ m') messageDigits' outerRows' (2 ^ r')
       innerDigits' dRows')
     (reinterpretCom : K.TCom → Commitment Φ' outerRows')
     (base' : ZMod q) (βSq' γ' κ' : ℕ) :
-    ((openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) init impl hq5 hκ
-        hτ K φF hd hq2 hb zpow Φ' pp' reinterpretCom base' βSq'
+    ((openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) (b := b) init impl hq5 hκ
+        hτ K φF hd hn zpow Φ' pp' reinterpretCom base' βSq'
         γ' κ')).verifier.coordinateWiseSpecialSound init impl
-      (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) init impl hq5 hκ hτ
-        K φF hd hq2 hb zpow Φ' pp' reinterpretCom base' βSq' γ' κ').struct
+      (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) (b := b) init impl
+        hq5 hκ hτ K φF hd hn zpow Φ' pp' reinterpretCom base' βSq' γ' κ').struct
       (relPolyEvalE 𝓜(q, α) (b : ZMod q)
         (quadEvalBetaSq γ b zDigits ((𝓜(q, α)).φ.natDegree) m messageDigits) γ (2 * ω) K.esc)
       (relInE Φ' base' βSq' γ' κ' K.esc) :=
-  (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) init impl hq5 hκ hτ
-    K φF hd hq2 hb zpow Φ' pp' reinterpretCom base' βSq' γ' κ').isCWSS
+  (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) (b := b) init impl hq5 hκ hτ
+    K φF hd hn zpow Φ' pp' reinterpretCom base' βSq' γ' κ').isCWSS
 
 end OpeningChain
 

ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean

@@ -75,7 +75,7 @@ section Protocol
 variable {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] [BEq (ZMod q)] [LawfulBEq (ZMod q)]
   (Φ : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ]
 variable {n μ : ℕ} {E : Type} {F : Type} [Field F]
-variable (mLow κ : ℕ) (bound ρBound : ℕ) (b : ℕ)
+variable (mLow κ : ℕ) (bound rBound : ℕ) (b : ℕ)
 variable {ι : Type} {oSpec : OracleSpec ι} {σ : Type}
 
 /-- The `i`-th true partial evaluation of the table (Eq. (24)):
@@ -145,18 +145,18 @@ def partialEvalProver {TCom : Type}
 `t` and *every* partial evaluation in the derived family is well-formed. This seam is the sound
 stopping point of the §4.5 peeling; collapsing it into the single `Z`-packed claim is the
 `Recursion/ZBatchBridge.lean` step (⚠ see there). -/
-def relPartialEval (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+def relPartialEval (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F) :
     Set (PartialEvalStatement K.TCom F mLow κ × LiftedWitness Φ μ n) :=
   {p |
     K.com p.2 = p.1.t ∧
     ∀ i, partialEvalAt Φ mLow κ φF p.2 p.1.pointLow i = p.1.partials i}
 
 /-- Escape-threaded per-`i` partial-evaluation relation. -/
-def relPartialEvalE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+def relPartialEvalE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F) :
     Set (PartialEvalStatement K.TCom F mLow κ × (LiftedWitness Φ μ n ⊕ E)) :=
-  (relPartialEval Φ mLow κ bound ρBound K φF).withEscape K.esc
+  (relPartialEval Φ mLow κ bound rBound K φF).withEscape K.esc
 
 variable [SampleableType F]
 
@@ -170,34 +170,34 @@ statement, the mle splitting identity `wTableMleEval_split` plus the derivation
 membership; escapes pass through. -/
 theorem partialEval_coordinateWiseSpecialSound
     (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
-    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F) :
     (partialEvalVerifier (oSpec := oSpec) mLow κ (TCom := K.TCom)
         (F := F)).coordinateWiseSpecialSound init impl
       CWSSStructure.ofIsEmpty
-      (relWEvalClaimE Φ (mLow + κ) bound ρBound b K φF)
-      (relPartialEvalE Φ mLow κ bound ρBound K φF) := by
+      (relWEvalClaimE Φ (mLow + κ) bound rBound b K φF)
+      (relPartialEvalE Φ mLow κ bound rBound K φF) := by
   sorry
 
 /-- **The partial-evaluation head as a `CWSSPackage`** (Hachi §4.5, Eq. (24)): the pure
 one-message derive-`y₀` head with the empty challenge structure, reducing the evaluation claim
 `relWEvalClaimE` to the per-`i` claims `relPartialEvalE`. -/
 def partialEvalPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
-    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F) :
     CWSSPackage init impl
       (WEvalStatement K.TCom F (mLow + κ)) (LiftedWitness Φ μ n ⊕ E)
       (PartialEvalStatement K.TCom F mLow κ) (LiftedWitness Φ μ n ⊕ E)
       (pSpecPartialEval F κ) where
   verifier := partialEvalVerifier (oSpec := oSpec) mLow κ (TCom := K.TCom) (F := F)
   struct := CWSSStructure.ofIsEmpty
-  relIn := relWEvalClaimE Φ (mLow + κ) bound ρBound b K φF
-  relOut := relPartialEvalE Φ mLow κ bound ρBound K φF
+  relIn := relWEvalClaimE Φ (mLow + κ) bound rBound b K φF
+  relOut := relPartialEvalE Φ mLow κ bound rBound K φF
   isPure := ⟨fun stmt tr =>
     ⟨stmt.t, fun j => stmt.point (Fin.castAdd κ j), fun j => stmt.point (Fin.natAdd mLow j),
       deriveFamily κ stmt.value (fun j => stmt.point (Fin.natAdd mLow j)) (tr 0)⟩,
     fun _ _ => rfl⟩
-  isCWSS := partialEval_coordinateWiseSpecialSound Φ mLow κ bound ρBound b init impl K φF
+  isCWSS := partialEval_coordinateWiseSpecialSound Φ mLow κ bound rBound b init impl K φF
 
 end Protocol
 

ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean

@@ -67,7 +67,7 @@ variable {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] [BEq (ZMod q)] [LawfulBEq (ZM
   (Φ : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ]
   (Φ' : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ']
 variable {n μ : ℕ} {E : Type} {F : Type} [Field F]
-variable (mLow κ : ℕ) (bound ρBound : ℕ)
+variable (mLow κ : ℕ) (bound rBound : ℕ)
 variable {innerRows' messageDigits' outerRows' innerDigits' dRows' m' r' : ℕ}
 variable {ι : Type} {oSpec : OracleSpec ι} {σ : Type}
 
@@ -170,7 +170,7 @@ instantiation obligation. -/
 theorem handoff_coordinateWiseSpecialSound
     (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
     (zpow : Fin (2 ^ κ) → F)
-    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F)
     (pp' : Hachi.PublicParamsD Φ' innerRows' (2 ^ m') messageDigits' outerRows' (2 ^ r')
       innerDigits' dRows')
@@ -179,7 +179,7 @@ theorem handoff_coordinateWiseSpecialSound
     (handoffVerifier (oSpec := oSpec) Φ' mLow φF pp'
         reinterpretCom).coordinateWiseSpecialSound init impl
       CWSSStructure.ofIsEmpty
-      (relHatEvalE Φ mLow κ bound ρBound zpow K φF)
+      (relHatEvalE Φ mLow κ bound rBound zpow K φF)
       (relInE Φ' base' βSq' γ' κ' K.esc) := by
   sorry
 
@@ -191,7 +191,7 @@ claim `relHatEvalE` to the **next iteration's** escape-threaded `QuadEval` input
 packings, not monomial bases of a point). -/
 def handoffPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
     (zpow : Fin (2 ^ κ) → F)
-    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F)
     (pp' : Hachi.PublicParamsD Φ' innerRows' (2 ^ m') messageDigits' outerRows' (2 ^ r')
       innerDigits' dRows')
@@ -205,10 +205,10 @@ def handoffPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbC
       (pSpecHandoff Φ') where
   verifier := handoffVerifier (oSpec := oSpec) Φ' mLow φF pp' reinterpretCom
   struct := CWSSStructure.ofIsEmpty
-  relIn := relHatEvalE Φ mLow κ bound ρBound zpow K φF
+  relIn := relHatEvalE Φ mLow κ bound rBound zpow K φF
   relOut := relInE Φ' base' βSq' γ' κ' K.esc
   isGuarded := handoffVerifier_isGuarded Φ' mLow φF pp' reinterpretCom
-  isCWSS := handoff_coordinateWiseSpecialSound Φ Φ' mLow κ bound ρBound init impl zpow K φF pp'
+  isCWSS := handoff_coordinateWiseSpecialSound Φ Φ' mLow κ bound rBound init impl zpow K φF pp'
     reinterpretCom base' βSq' γ' κ'
 
 end Protocol

ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean

@@ -68,7 +68,7 @@ section Bridge
 variable {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] [BEq (ZMod q)] [LawfulBEq (ZMod q)]
   (Φ : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ]
 variable {n μ : ℕ} {E : Type} {F : Type} [Field F]
-variable (mLow κ : ℕ) (bound ρBound : ℕ)
+variable (mLow κ : ℕ) (bound rBound : ℕ)
 variable {ι : Type} {oSpec : OracleSpec ι} {σ : Type}
 
 /-- The `Z`-packed table evaluation (Hachi Eqs. (25)–(26) left-hand side):
@@ -83,7 +83,7 @@ def hatEval (φF : ZMod q →+* F) (zpow : Fin (2 ^ κ) → F) (w : LiftedWitnes
 evaluates to the packed public value at the low point half. This is the claim the trace handoff
 (`Recursion/TraceHandoff.lean`) converts into the next iteration's `Rq`-statement. -/
 def relHatEval (zpow : Fin (2 ^ κ) → F)
-    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F) :
     Set (HatEvalStatement K.TCom F mLow × LiftedWitness Φ μ n) :=
   {p |
@@ -92,10 +92,10 @@ def relHatEval (zpow : Fin (2 ^ κ) → F)
 
 /-- Escape-threaded `Z`-packed claim relation. -/
 def relHatEvalE (zpow : Fin (2 ^ κ) → F)
-    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F) :
     Set (HatEvalStatement K.TCom F mLow × (LiftedWitness Φ μ n ⊕ E)) :=
-  (relHatEval Φ mLow κ bound ρBound zpow K φF).withEscape K.esc
+  (relHatEval Φ mLow κ bound rBound zpow K φF).withEscape K.esc
 
 /-- The bridge's statement map: forget the peeled point half and pack the partial evaluations
 into the public right-hand side `∑ᵢ yᵢ·zpow i` of Eq. (26). -/
@@ -111,11 +111,11 @@ the module docstring for the explicit `κ = 1` cheat). The sorry is kept — del
 in this zero-round seam — until a repair (batching challenge / generic §3.1 packing) is adopted;
 any repair changes this bridge's *protocol content*, not the surrounding seams. -/
 theorem mem_relPartialEvalE_of_relHatEvalE (zpow : Fin (2 ^ κ) → F)
-    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F)
     (s : PartialEvalStatement K.TCom F mLow κ) (w : LiftedWitness Φ μ n ⊕ E)
-    (h : (toHatEvalStatement mLow κ zpow s, w) ∈ relHatEvalE Φ mLow κ bound ρBound zpow K φF) :
-    (s, w) ∈ relPartialEvalE Φ mLow κ bound ρBound K φF := by
+    (h : (toHatEvalStatement mLow κ zpow s, w) ∈ relHatEvalE Φ mLow κ bound rBound zpow K φF) :
+    (s, w) ∈ relPartialEvalE Φ mLow κ bound rBound K φF := by
   sorry
 
 /-- **The `Z`-packing bridge as a `CWSSPackage`** (Hachi §4.5, Eqs. (25)–(26)): zero-round
@@ -124,22 +124,22 @@ theorem mem_relPartialEvalE_of_relHatEvalE (zpow : Fin (2 ^ κ) → F)
 pull-back; see the module docstring. -/
 def zBatchPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
     (zpow : Fin (2 ^ κ) → F)
-    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
+    (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
     (φF : ZMod q →+* F) :
     CWSSPackage init impl
       (PartialEvalStatement K.TCom F mLow κ) (LiftedWitness Φ μ n ⊕ E)
       (HatEvalStatement K.TCom F mLow) (LiftedWitness Φ μ n ⊕ E)
       (!p[] : ProtocolSpec 0) where
   verifier := ReduceClaim.verifier oSpec (toHatEvalStatement mLow κ zpow)
   struct := CWSSStructure.ofIsEmpty
-  relIn := relPartialEvalE Φ mLow κ bound ρBound K φF
-  relOut := relHatEvalE Φ mLow κ bound ρBound zpow K φF
+  relIn := relPartialEvalE Φ mLow κ bound rBound K φF
+  relOut := relHatEvalE Φ mLow κ bound rBound zpow K φF
   isPure := ⟨fun stmt _ => toHatEvalStatement mLow κ zpow stmt, fun _ _ => rfl⟩
   isCWSS := ReduceClaim.verifier_coordinateWiseSpecialSound
-    (relIn := relPartialEvalE Φ mLow κ bound ρBound K φF)
-    (relOut := relHatEvalE Φ mLow κ bound ρBound zpow K φF)
+    (relIn := relPartialEvalE Φ mLow κ bound rBound K φF)
+    (relOut := relHatEvalE Φ mLow κ bound rBound zpow K φF)
     (mapWitInv := fun _ w => w) (D := CWSSStructure.ofIsEmpty)
-    (mem_relPartialEvalE_of_relHatEvalE Φ mLow κ bound ρBound zpow K φF)
+    (mem_relPartialEvalE_of_relHatEvalE Φ mLow κ bound rBound zpow K φF)
 
 end Bridge