feat[Hachi]: skeleton

[tobias-rothmann]

Skeleton for the Hachi opening proof with a corresponding artifact:
in Hachi/hachi-overview.html

cc @ErVinuelas

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: feat[Hachi]: skeleton

sorry delta: +36 (36 added) — proof obligations increased

This pull request introduces a large skeleton for the Hachi opening proof in Lean 4, adding extensive new files for subprotocols, infrastructure, and documentation. The core changes are in Composition.lean (restructured into three layers: evalChain, openCore, openingChain) and the new Escape.lean (escape-threaded evaluation front). Many theorems and definitions are sorried (placeholder), and several documented gaps exist (e.g., Lemma 10, Recursion). The PR body is minimal but accurate; the actual changes are far more extensive, with numerous sorries and documented protocol issues. The following overview highlights the key additions, sorries, and organizational changes.

---

Statistics

Metric	Count
📝 Files Changed	30
✅ Lines Added	8448
❌ Lines Removed	100

---

Lean Declarations

✏️ Added: 125 declaration(s)

ArkLib/Commitments/Functional/Hachi/Composition.lean (5)

• @[reducible] def openCoreSpecSampleable (ω : ℕ) (TCom F : Type) [SampleableType F]
• abbrev openCoreSpec (ω : ℕ) (TCom F : Type)
• noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• theorem hachi_iteration_coordinateWiseSpecialSound (init : ProbComp σ)

ArkLib/Commitments/Functional/Hachi/Escape.lean (8)

• def bridgePackageE (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def evalChainE (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def quadEvalPackageE (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def relInE (base : ZMod q) (βSq γ κ : ℕ) (esc : Set E) :
• def relOutE (base : ZMod q) (ω γ : ℕ) (esc : Set E) :
• def relPolyEvalE (base : ZMod q) (βSq γ κ : ℕ) (esc : Set E) :
• theorem mem_relPolyEvalE_of_relInE (base : ZMod q) (βSq γ κ : ℕ) (esc : Set E)
• theorem quadEval_coordinateWiseSpecialSound_withEscape

ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean (11)

• @[reducible] def pSpecPartialEval (F : Type) (κ : ℕ) : ProtocolSpec 1
• def deriveFamily (value : F) (pointHigh : Fin κ → F)
• def eqWeight (a₁ : Fin κ → F) (i : Fin (2 ^ κ)) : F
• def partialEvalAt (φF : ZMod q →+* F) (w : LiftedWitness Φ μ n)
• def partialEvalPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def partialEvalProver {TCom : Type}
• def partialEvalVerifier {TCom : Type} :
• def relPartialEval (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• def relPartialEvalE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• theorem partialEval_coordinateWiseSpecialSound
• theorem wTableMleEval_split (φF : ZMod q →+* F) (w : LiftedWitness Φ μ n)

ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean (8)

• @[reducible] def pSpecHandoff (Φ' : CyclotomicModulus (ZMod q)) : ProtocolSpec 1
• def handoffPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def handoffProver {TCom WitOut : Type} (φF : ZMod q →+* F)
• def handoffVerifier {TCom : Type} (φF : ZMod q →+* F)
• def toNextQuadEvalStatement {TCom : Type} (φF : ZMod q →+* F)
• def traceCheck {TCom : Type} (φF : ZMod q →+* F)
• theorem handoffVerifier_isGuarded {TCom : Type} (φF : ZMod q →+* F)
• theorem handoff_coordinateWiseSpecialSound

ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean (6)

• def hatEval (φF : ZMod q →+* F) (zpow : Fin (2 ^ κ) → F) (w : LiftedWitness Φ μ n)
• def relHatEval (zpow : Fin (2 ^ κ) → F)
• def relHatEvalE (zpow : Fin (2 ^ κ) → F)
• def toHatEvalStatement {TCom : Type} (zpow : Fin (2 ^ κ) → F)
• def zBatchPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• theorem mem_relPartialEvalE_of_relHatEvalE (zpow : Fin (2 ^ κ) → F)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean (11)

• abbrev LiftStatement (Φ : CyclotomicModulus (ZMod q)) (TCom F : Type) (n μ : ℕ) : Type
• def RhoShort (ρBound : ℕ) (ρ : Fin n → Polynomial (ZMod q)) : Prop
• def liftPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def liftProver (WitIn : Type)
• def liftShort (bound ρBound : ℕ) (w : LiftedWitness Φ μ n) : Prop
• def liftVerifier :
• def relLift (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• def relLiftE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• noncomputable def evalAt (φF : ZMod q →+* F) (a : F) : Polynomial (ZMod q) →+* F
• noncomputable def rowSum (s : RlinStatement Φ n μ) (z : PolyVec (Rq Φ) μ) (i : Fin n) :
• theorem lift_coordinateWiseSpecialSound

ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean (8)

• abbrev rlinCols (innerRows messageDigits innerDigits zDigits m r : Nat) : Nat
• abbrev rlinRows (innerRows outerRows dRows : Nat) : Nat
• def relRlin {n μ : ℕ} : Set (RlinStatement Φ n μ × PolyVec (Rq Φ) μ)
• def relRlinE {n μ : ℕ} (esc : Set E) :
• def rlinPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def rlinStmt (base : ZMod q) (ω γ : ℕ)
• def unstack
• theorem mem_relOutE_of_relRlinE (base : ZMod q) (ω γ : ℕ) (esc : Set E)

ArkLib/Commitments/Functional/Hachi/Sumcheck/Bridge.lean (3)

• noncomputable def sumcheckBridgePackage (init : ProbComp σ)
• noncomputable def toRoundStatement {TCom : Type} (φF : ZMod q →+* F)
• theorem mem_relZeroCheckE_of_roundRelE

ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean (9)

• @[reducible] def pSpecFinalEval (F : Type) : ProtocolSpec 1
• def finalCheck {TCom : Type} (m₁ bound b : ℕ) (φF : ZMod q →+* F)
• def finalEvalPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def finalEvalProver {TCom : Type}
• def finalEvalVerifier {TCom : Type} (φF : ZMod q →+* F) :
• def relWEvalClaim (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• def relWEvalClaimE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• theorem finalEvalVerifier_isGuarded {TCom : Type} (φF : ZMod q →+* F) :
• theorem finalEval_coordinateWiseSpecialSound

ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean (13)

• @[reducible] def RoundMsg : Type
• def roundCheck {TCom : Type} {i : ℕ} (stmt : RoundStatement Φ TCom F n μ i)
• def roundPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def roundProver {TCom : Type} (i : ℕ)
• def roundVerifier {TCom : Type} (i : ℕ) :
• def roundsSpec : (count : ℕ) → ProtocolSpec (2 * count)
• instance roundsSpecSampleable [SampleableType F] :
• noncomputable def roundsChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• noncomputable def roundsChainAux (init : ProbComp σ)
• theorem roundVerifier_isGuarded {TCom : Type} (i : ℕ) :
• theorem round_coordinateWiseSpecialSound
• theorem roundsChain_relIn (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• theorem roundsChain_relOut (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Batch.lean (4)

• def batchPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def relBatched (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• def relBatchedE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• theorem mem_relLiftE_of_relBatchedE

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean (17)

• def hAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F)
• def hZero (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n) :
• def hypercubeSum (H : MvPolynomial (Fin m₀) F) (i : ℕ) (cs : Fin i → F) : F
• def kroneckerPoint (m : ℕ) (ρ : F) : Fin m → F
• def roundDegAlpha : ℕ
• def roundDegZero (b : ℕ) : ℕ
• def roundRel (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• def roundRelE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• def sumcheckPolyAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F)
• def sumcheckPolyZero (φF : ZMod q →+* F) (b : ℕ) (τ₀ : Fin m₀ → F)
• def wTable (b : ℕ) (w : LiftedWitness Φ μ n) : Fin (2 ^ m₀) → ZMod q
• def wTableMleEval (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n)
• def zcTargetAlpha (φF : ZMod q →+* F) (s : RlinStatement Φ n μ) (a : F)
• theorem hAlpha_degreeOf_le (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F)
• theorem hZero_degreeOf_le (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n)
• theorem sum_sumcheckPolyAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F)
• theorem sum_sumcheckPolyZero (φF : ZMod q →+* F) (b : ℕ) (τ₀ : Fin m₀ → F)

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean (8)

• @[reducible] def pSpecZeroCheck (F : Type) : ProtocolSpec 1
• def relZeroCheck (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• def relZeroCheckE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound ρBound))
• def zeroCheckPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• def zeroCheckProver {TCom : Type} :
• def zeroCheckStructure (F : Type) (m₀ m₁ : ℕ) : CWSSStructure (pSpecZeroCheck F) where
• def zeroCheckVerifier {TCom : Type} :
• theorem zeroCheck_coordinateWiseSpecialSound

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Escape.lean (5)

• def withEscape (rel : Set (S × W)) (esc : Set E) : Set (S × (W ⊕ E))
• theorem mem_withEscape_inl (rel : Set (S × W)) (esc : Set E) (s : S) (w : W) :
• theorem mem_withEscape_inr (rel : Set (S × W)) (esc : Set E) (s : S) (e : E) :
• theorem mem_withEscape_language_iff (rel : Set (S × W)) (esc : Set E) (s : S) :
• theorem withEscape_empty_iff (rel : Set (S × W)) (s : S) (w : W ⊕ Empty) :

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean (6)

• def IsGuardedWith (V : Verifier oSpec StmtIn StmtOut pSpec)
• def _root_.CoordinateWise.CWSSPackage.toGuarded
• def append {StmtA WitA StmtB WitB StmtC WitC : Type}
• theorem IsGuarded.append (V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁)
• theorem IsGuarded.of_isPure (V : Verifier oSpec StmtIn StmtOut pSpec) (h : V.IsPure) :
• theorem append_coordinateWiseSpecialSound_of_guardedLeft

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean (3)

• @[reducible] def pSpecScalar (Msg C : Type) : ProtocolSpec 2
• @[reducible] def scalarStructure (k : ℕ) (hk : 2 ≤ k) :
• theorem coordinateWiseSpecialSound_of_mkWitness_scalar

---

sorry Tracking

❌ Added: 36 `sorry`(s)

ArkLib/Commitments/Functional/Hachi/Escape.lean (1)

• theorem quadEval_coordinateWiseSpecialSound_withEscape (L147)

ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean (5)

• def deriveFamily (value : F) (pointHigh : Fin κ → F) (L112)
• def eqWeight (a₁ : Fin κ → F) (i : Fin (2 ^ κ)) : F (L92)
• def partialEvalAt (φF : ZMod q →+* F) (w : LiftedWitness Φ μ n) (L86)
• theorem partialEval_coordinateWiseSpecialSound (L180)
• theorem wTableMleEval_split (φF : ZMod q →+* F) (w : LiftedWitness Φ μ n) (L103)

ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean (3)

• def toNextQuadEvalStatement {TCom : Type} (φF : ZMod q →+* F) (L102)
• def traceCheck {TCom : Type} (φF : ZMod q →+* F) (L88)
• theorem handoff_coordinateWiseSpecialSound (L184)

ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean (2)

• def hatEval (φF : ZMod q →+* F) (zpow : Fin (2 ^ κ) → F) (w : LiftedWitness Φ μ n) (L80)
• theorem mem_relPartialEvalE_of_relHatEvalE (zpow : Fin (2 ^ κ) → F) (L119)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean (1)

• theorem lift_coordinateWiseSpecialSound (L226)

ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean (3)

• def rlinStmt (base : ZMod q) (ω γ : ℕ) (L101)
• def unstack (L111)
• theorem mem_relOutE_of_relRlinE (base : ZMod q) (ω γ : ℕ) (esc : Set E) (L129)

ArkLib/Commitments/Functional/Hachi/Sumcheck/Bridge.lean (1)

• theorem mem_relZeroCheckE_of_roundRelE (L63)

ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean (2)

• def finalCheck {TCom : Type} (m₁ bound b : ℕ) (φF : ZMod q →+* F) (L83)
• theorem finalEval_coordinateWiseSpecialSound (L157)

ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean (1)

• theorem round_coordinateWiseSpecialSound (L183)

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Batch.lean (1)

• theorem mem_relLiftE_of_relBatchedE (L82)

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean (12)

• def hAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F) (L117)
• def hZero (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n) : (L108)
• def hypercubeSum (H : MvPolynomial (Fin m₀) F) (i : ℕ) (cs : Fin i → F) : F (L167)
• def sumcheckPolyAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F) (L155)
• def sumcheckPolyZero (φF : ZMod q →+* F) (b : ℕ) (τ₀ : Fin m₀ → F) (L147)
• def wTable (b : ℕ) (w : LiftedWitness Φ μ n) : Fin (2 ^ m₀) → ZMod q (L94)
• def wTableMleEval (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n) (L100)
• def zcTargetAlpha (φF : ZMod q →+* F) (s : RlinStatement Φ n μ) (a : F) (L161)
• theorem hAlpha_degreeOf_le (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F) (L130)
• theorem hZero_degreeOf_le (φF : ZMod q →+* F) (b : ℕ) (w : LiftedWitness Φ μ n) (L123)
• theorem sum_sumcheckPolyAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (a : F) (L183)
• theorem sum_sumcheckPolyZero (φF : ZMod q →+* F) (b : ℕ) (τ₀ : Fin m₀ → F) (L175)

ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean (1)

• theorem zeroCheck_coordinateWiseSpecialSound (L173)

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean (2)

• theorem IsGuarded.append (V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁) (L114)
• theorem append_coordinateWiseSpecialSound_of_guardedLeft (L142)

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean (1)

• theorem coordinateWiseSpecialSound_of_mkWitness_scalar (L102)

---

Coverage Notes

• AI file summarization partially analyzed 1 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

• HACHI_GENERIC_RING_SWITCH_PLAN.md (+1079/-0)

* Additional-instructions analysis was skipped because the full diff exceeded the analysis size budget, and partial results would be misleading.

---

📄 **Per-File Summaries**

• ArkLib.lean: Imports were added for several new modules in the ArkLib project. In the ArkLib/Commitments/Functional/Hachi/ directory, new imports include Escape, a Recursion subdirectory with PartialEval, TraceHandoff, and ZBatchBridge, a RingSwitch subdirectory with Reduction and Rlin, a Sumcheck subdirectory with Bridge, FinalEval, and Rounds, and a ZeroCheck subdirectory with Batch, Constraints, and Reduction. In the ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ directory, new imports include Escape, Guarded, and ScalarRound.
• ArkLib/Commitments/Functional/Hachi/Composition.lean: This file was significantly restructured and extended in three layers: the existing finished evalChain (sorry-free core of bridge ▷ QuadEval) was retained, a new openCore definition was added that chains the escape-threaded evalChainE with five §4.3 pure subprotocols (rlinPackage, liftPackage, batchPackage, zeroCheckPackage, sumcheckBridgePackage), and a new openingChain definition was added that composes openCore with the guarded tail (roundsChain, finalEvalPackage, partialEvalPackage, zBatchPackage, handoffPackage) to land on the next ring's QuadEval input. The new theorem hachi_iteration_coordinateWiseSpecialSound states that openingChain is coordinate-wise special-sound (the certificate is openingChain.isCWSS). The module header was rewritten to document the three layers, the seam table, the corrected Lemma 10 (using Kronecker seeds) and the row‑11 gap (HACHI_RECURSION_GAP.md), and a sorry inventory naming each sorried encoding and the generic B4 guarded-append machinery. New imports were added: ArkLib.Commitments.Functional.Hachi.Sumcheck.FinalEval, ArkLib.Commitments.Functional.Hachi.Recursion.TraceHandoff, and ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Guarded.
• ArkLib/Commitments/Functional/Hachi/Escape.lean: This new file threads an abstract escape budget E (with escape set esc : Set E) through the Hachi evaluation front, enabling backward flow of extraction escapes for the §4.3 opening chain. It defines the escape-threaded relations relPolyEvalE, relInE, and relOutE using Set.withEscape, a sorry-free polynomial-level bridge bridgePackageE with the pull-back theorem mem_relPolyEvalE_of_relInE, and the sorried theorem quadEval_coordinateWiseSpecialSound_withEscape that will widen Lemma 8. These are packaged into quadEvalPackageE and composed as evalChainE = bridgePackageE ▷ quadEvalPackageE, serving as the widened drop-in for evalChain. The file also provides an instance Nonempty (A ⊕ E).
• ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean: This new file (204 lines) introduces the partial-evaluation head for the Hachi recursion (Milestone G2), factoring an mle evaluation claim mle[w̃](a)=y′ into per‑index partial claims yᵢ = partialEvalAt w̃ a₀ i. It defines: pSpecPartialEval (the 1‑message protocol spec, sending the 2^κ-1 nonzero partials), PartialEvalStatement (the output statement bundling the commitment, split evaluation point (a₀,a₁), and derived family (yᵢ)ᵢ), the sorried functions partialEvalAt, eqWeight, deriveFamily, and the theorem wTableMleEval_split (the mle splitting identity underlying Eq. (24)). The file also defines a pure verifier partialEvalVerifier (no challenge round, derives y₀ via deriveFamily), a skeleton prover partialEvalProver, the residual relation relPartialEval (per‑i well‑formedness plus commitment binding), and its escaped variant relPartialEvalE. Crucially, the CWSS theorem partialEval_coordinateWiseSpecialSound is sorried, as are partialEvalAt, eqWeight, wTableMleEval_split, and deriveFamily—all marked as “Sorried (G2)”. The file concludes by packaging these pieces into partialEvalPackage, a CWSSPackage that reduces the input evaluation relation (relWEvalClaimE) to the output per‑i partial-evaluation relation (relPartialEvalE).
• ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean: This new file (TraceHandoff.lean) implements the recursion-closing adapter for the Hachi protocol (§4.5, Eqs. (27)–(28)), converting a Z-packed hatEval claim into the next iteration's QuadEvalStatement over ring Φ'. The file defines the prover message spec pSpecHandoff, the verifier handoffVerifier (guarded by the sorried traceCheck which enforces the trace equation Tr_H(p·…) = (d′/k)·value), the next-statement builder toNextQuadEvalStatement (also sorried), and the honest prover skeleton handoffProver. The sorried handoff_coordinateWiseSpecialSound theorem sketches the CWSS proof plan: using the trace guard and the ψ/Z-packing bijection to extract an opening satisfying relHatEvalE. The file also assembles the handoffPackage as a GCWSSPackage, closing the recursion loop by relating relHatEvalE to the next iteration's relInE relation.
• ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='This new file defines th... seam pending a repair.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• ArkLib/Commitments/Functional/Hachi/RingSwitch.lean: Added ArkLib/Commitments/Functional/Hachi/RingSwitch.lean, an umbrella module that re-exports Reduction (which transitively includes Rlin). The file's docstring documents the Hachi ring‑switching lift (Figure 4 / Lemma 9) and folder structure, noting that the submodules contain sorried pieces: Rlin.lean has sorried block‑matrix assembly/unstacking and block‑row equivalence pull‑back; Reduction.lean has the CWSS theorem lift_coordinateWiseSpecialSound sorried at Lemma 9's interpolation extraction.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean: This new file Reduction.lean introduces the HMZ25 lift — a two-round commit-then-challenge protocol (Hachi Figure 4 / Lemma 9) that reduces the R^lin relation relRlinE to an extended lift relation relLiftE via coordinate-wise special soundness (CWSS). It defines:

• LiftedWitness (the witness z plus per-row quotient polynomials ρ with degree bound ≤ d−2), the shortness predicates RhoShort and liftShort, and the abstract binding commitment structure LiftCom with its weak-binding axiom collision_mem.
• The output statement LiftStatement (an RlinStatement paired with a commitment t and evaluation challenge α), the row-sum computation rowSum, the evaluation embedding evalAt, and the output relation relLift (requiring t opens to a short lifted witness whose lifted rows vanish at α and bound ≤ s.bound).
• The escape-threaded variant relLiftE, the pure pass-through verifier liftVerifier, and the honest-prover skeleton liftProver.
• The core theorem lift_coordinateWiseSpecialSound (stated but sorried), which claims CWSS at k = 2d for the lift protocol, and the bundled liftPackage structure that packages it for composition.
• The module docstring contains detailed protocol commentary, soundness strategy, and references to [HMZ25] and [NOZ26]. No existing code is modified; this is a pure addition.

• ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean: This new file introduces the R^lin adapter (Hachi §4.3), a zero-round ReduceClaim bridge that reshapes a QuadEval (Eq. (20)) statement into an RlinStatement and vice versa. It defines RlinStatement (with fields M, yvec, bound) and the relation relRlin (M ζ = y and ‖ζ‖∞ ≤ bound), plus its escape-threaded variant relRlinE. The core bridge consists of three sorried definitions: rlinStmt (assembles the block matrix and right-hand side from QuadEval's output), unstack (splits the stacked witness back into the QuadEvalResponse triple), and mem_relOutE_of_relRlinE (proves the block-row equivalence pull-back). The file also provides rlinPackage, a CWSSPackage that ties these components together using ReduceClaim.verifier_coordinateWiseSpecialSound.
• ArkLib/Commitments/Functional/Hachi/Sumcheck.lean: Added a new umbrella module Sumcheck.lean for the Hachi sumcheck loop folder, which re-exports the submodules Bridge, Rounds, and FinalEval. The file documents the protocol's reduction of zero-check point-evaluation claims to hypercube-sum claims, the m₀-round paired sumcheck loop (Figure 6/Lemma 11), and the closing tail (Figure 7) that outputs an evaluation claim for the committed table w̃ consumed by recursion. It explicitly notes a TODO to rebase onto Sumcheck.Structured and states that the CWSS round verifier round_coordinateWiseSpecialSound in Rounds.lean is left sorry.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/Bridge.lean: This new file defines the zero-round sumcheck bridge in the Hachi protocol, connecting zero-check point-evaluation claims to initial sumcheck hypercube-sum claims. It introduces toRoundStatement, which installs the empty challenge prefix and the initial target pair (0, zcTargetAlpha), and the theorem mem_relZeroCheckE_of_roundRelE (marked with sorry) establishing that the hypercube-sum claims imply the point-evaluation claims via the identities ∑ F_{0,τ₀} = H₀(τ₀) and ∑ F_{α,τ_α} = H_α(τ_α) + zcTargetAlpha. The file also provides sumcheckBridgePackage, a CWSSPackage that packages the bridge as a ReduceClaim reducing relZeroCheckE to roundRelE 0 with no soundness error.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean: This new file adds the skeleton of the final-evaluation step for the Hachi sumcheck protocol (Figure 7 tail):

• Defines pSpecFinalEval, a one-message protocol spec with no challenges.
• Defines WEvalStatement (containing commitment t, point a, and claimed value y′), the output statement that serves as the recursion currency after one sumcheck pass.
• Defines finalCheck (currently sorry) and finalEvalVerifier, a guarded verifier that checks both final sumcheck targets and the bound-sanity conjunct, outputting a WEvalStatement.
• Defines finalEvalProver, an honest prover that sends the claimed evaluation y′ = mle[w̃](a).
• Defines relWEvalClaim and its escaped variant relWEvalClaimE, specifying that w̃ opens t and evaluates to y′ at a.
• States finalEval_coordinateWiseSpecialSound (currently sorry) asserting the CWSS property that ties the guarded verifier to the round-m₀ relation, and packages this as finalEvalPackage.
• All proofs (including finalCheck and the CWSS theorem) are sorried (marked with sorry), signaling that the implementation is incomplete at milestone F8.

• ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean: This new file Rounds.lean implements the paired sumcheck rounds from Hachi Figure 6 / Lemma 11 as part of the milestone F7 skeleton. It defines RoundMsg as the pair of univariate round polynomials (g_i^{(0)}, g_i^{(α)}) with degree bounds roundDegZero b = 2b and roundDegAlpha = 2, the roundCheck Bool-valued function verifying both polynomials sum to their respective targets over {0,1}, the guarded roundVerifier that returns failure on check failure (embedding the guard as a definitional condition for extractability), the roundProver skeleton parameterized by computeG, and the roundsSpec wire format composing count rounds via pSpecScalar. The central theorem round_coordinateWiseSpecialSound (Lemma 11) is explicitly sorried, with a detailed extraction plan described in the docstring; it would establish per-round CWSS at k = max (2b) 2 + 1. The roundPackage assembles the verifier, structure, and relations into a GCWSSPackage. The loop composition is built via roundsChainAux (recursive guarded append ▷ᵍ) and exposed as roundsChain, with companion lemmas roundsChain_relIn and roundsChain_relOut proving that the composite's input/output relations match the round-0 and round-count seam relations respectively.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck.lean: This diff adds a new umbrella module ArkLib/Commitments/Functional/Hachi/ZeroCheck.lean that re-exports the ZeroCheck/ subfolder (which transitively includes Batch and Constraints) and documents the overall structure of the batched-constraint encoding and zero-check subprotocol. It notes that Lemma 10 from the Hachi paper is repaired via two Kronecker seeds (ρ₀, ρ_α), and it explicitly names the three submodules: Constraints.lean (defines shared constraint encoding with sorried definitions), Batch.lean (batching bridge reinterpreting residual claims as H₀ ≡ 0 ∧ H_α ≡ 0), and Reduction.lean (corrected Lemma 10 with zeroCheck_coordinateWiseSpecialSound sorried at k = D).
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Batch.lean: This new file introduces the batching bridge for the Hachi zero-check protocol, defining the batched relation relBatched (Eqs. (22)–(23) as polynomial identities) and its escape-threaded version relBatchedE, along with the sorried theorem mem_relLiftE_of_relBatchedE which states that the batched identities (including hZero and hAlpha being zero) imply the lift's per-row and range claims (relLiftE). It also provides the batchPackage definition, a zero-round CWSSPackage that reduces relLiftE to relBatchedE with no soundness error, relying on the sorried pull-back theorem. The file depends on ZeroCheck/Constraints.lean and is part of milestone F6, isolating the batching algebra from the zero-check's Kronecker interpolation.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean: This new file adds the constraint-encoding layer for the Hachi zero-check protocol, including definitions for the Kronecker curve (kroneckerPoint), round degrees (roundDegZero, roundDegAlpha), batched constraint polynomials (hZero, hAlpha), sumcheck polynomials (sumcheckPolyZero, sumcheckPolyAlpha), and statement types (ZeroCheckStatement, RoundStatement, roundRel, roundRelE). However, the core definitions and all characterizing lemmas are sorried: wTable, wTableMleEval, hZero, hAlpha, sumcheckPolyZero, sumcheckPolyAlpha, zcTargetAlpha, hypercubeSum, and the theorems hZero_degreeOf_le, hAlpha_degreeOf_le, sum_sumcheckPolyZero, sum_sumcheckPolyAlpha are all sorry placeholders.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean: This new file ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean implements the corrected Hachi Lemma 10 (zero-check round) using a Kronecker‑curve seed pair (ρ₀, ρ_α) ∈ F × F instead of the paper’s uniform vector challenges. It defines the protocol spec pSpecZeroCheck, the CWSSStructure zeroCheckStructure (with ℓ = 2, k = D = max 2 (max 2^{m₀} 2^{m₁})), a pure‑pass‑through verifier zeroCheckVerifier, a trivial prover zeroCheckProver, the output relation relZeroCheck (and its escape‑threaded variant relZeroCheckE), and the CWSSPackage zeroCheckPackage. The central theorem zeroCheck_coordinateWiseSpecialSound (corrected Lemma 10) is sorried; the file also includes a detailed comment explaining the paper’s gap and the adopted repair.
• ArkLib/Commitments/Functional/Hachi/hachi-overview.html: This diff adds a new standalone HTML file, hachi-overview.html, which provides a visual and structural overview of the formalization of the Hachi evaluation opening for the Lean 4 proof assistant project. The file documents a nine-step reduction chain from QuadEval to the final multilinear evaluation claim, listing every protocol-bearing file in the Hachi/ directory along with its proof status (proven, work-in-progress, or planned), the number of sorry terms, and the relevant paper references. It also summarizes supporting substrate files, cross-cutting machinery, and a roadmap for remaining work, enabling reviewers to understand the current state of the formalization before inspecting individual .lean diffs.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Escape.lean: This new file adds Set.withEscape to widen a relation Set (S × W) by an escape disjunct to Set (S × (W ⊕ E)), together with the simplification lemmas mem_withEscape_inl and mem_withEscape_inr. It also provides mem_withEscape_language_iff, which characterizes the language of the widened relation as the original language or the existence of any escape, and withEscape_empty_iff, showing that widening by the empty escape set over Empty degenerates to the original relation. These definitions implement the escape-threading plumbing for composed special-soundness chains in the Hachi protocol, where a downstream extractor may produce a cryptographic escape (e.g., a binding break) instead of a real witness.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean: This file introduces the guarded verifier framework (Verifier.IsGuardedWith, Verifier.IsGuarded, and GCWSSPackage) as a skeleton for milestone B4 of the Hachi sumcheck track. It provides the guarded analogue of the existing pure CWSS composition: Verifier.IsGuarded.append (sorried – B4.4), Verifier.append_coordinateWiseSpecialSound_of_guardedLeft (sorried – B4.3), and the bundled GCWSSPackage with append/▷ᵍ defined in terms of those sorried theorems. A CWSSPackage.toGuarded conversion and the Verifier.IsGuarded instance for pure verifiers are also added.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean: This new file introduces the generic scalar-challenge round framework for coordinate-wise special soundness (CWSS) in the Hachi sumcheck track, corresponding to milestone F4.1. It defines the two-round protocol specification pSpecScalar (prover message then scalar challenge) and the CWSS structure scalarStructure k representing plain k-special soundness. Instance declarations provide SampleableType and OracleInterface for the challenge and message types. The main result is the sorried theorem coordinateWiseSpecialSound_of_mkWitness_scalar, which asserts that any pure statement-extending verifier of this shape is CWSS given a witness assembler mkWitness; this unifies the proofs of Hachi Lemma 9 (k = 2d) and Lemma 11 (k = deg + 1). The proof skeleton is described in the module docstring, relying on an injection condition rather than the star machinery used in the vector-challenge counterpart.
• HACHI_GENERIC_RING_SWITCH_PLAN.md: This new documentation file, HACHI_GENERIC_RING_SWITCH_PLAN.md, presents a detailed reconciliation and implementation plan for extending the feat/generic-ring-switch branch's RingSwitching/Generic/ layer to accommodate the Hachi protocol's §3.1 packing head. The document identifies five key necessary changes: adding a deterministic 'packed-claim' exit stage to the Generic/ layer, retracting existing docstrings that incorrectly model Hachi as a batching instance, closing gaps in the lattice layer (such as psi_smul and a bundled psiLinearEquiv), building the head reduction itself including an unpackPoly function and composed CWSS soundness proof, and composing this into the existing evalChain. The plan supersedes previous design documents, defines a 7-phase implementation roadmap (Phases 0-7) with estimated effort, documents verified 'ground truth' about the repository's current state, establishes ~9 design decisions (including the use of a guarded verifier over a pure one, and G2's decision that the wire message is untwisted), and notes that the plan deliberately does not route Hachi's proofs through the branch's MultilinearPoly-based generic lemmas due to missing eval agreement bridges. It also details specific technical specifications such as the recombineCheck and unpackPoly definitions, psiLinearEquiv bundling requirements, index convention packIndexEquiv, the traceCheck_iff_recombine equivalence, and the need for a new GuardedCWSSPackage with guarded append for left-side guard-supporting variants.
• HACHI_LEMMA10_GAP.md: Added HACHI_LEMMA10_GAP.md, a detailed analysis of a gap in Lemma 10 of Hachi (NOZ26). The file identifies that the paper's coordinate-wise special soundness claim for the zero-check challenge round is not provable as stated, provides a protocol-level counterexample that breaks the paper's extraction claim, and proposes several repair approaches. The adopted repair replaces the original unrestricted vector challenges with one-round Kronecker-curve challenges, achieving deterministic one-round CWSS with corrected parameter D = max(2^m_0, 2^m_α). The file also documents a fallback coordinate-zipped CWSS approach, discusses knowledge error, and outlines the formalization impact.
• HACHI_RECURSION_GAP.md: Added HACHI_RECURSION_GAP.md, a detailed analysis of a knowledge‑soundness gap in Hachi’s §4.5/§3.2 partial‑evaluation step (Eqs. (24)–(26)): the packed claim f′(x_rest) = ∑ᵢ yᵢ·Z^{⟨i⟩} does not force all per‑slice defects to zero when the yᵢ are in the extension field, with an explicit counterexample for κ=1. The document adopts a repair that reconstructs a tensor carrier from the already‑sent yᵢ, uses a post‑yᵢ scalar challenge and a degree‑two relocation sumcheck, and reuses Hachi’s existing Eq. (27) element p to avoid extra communication. It also corrects the dynamic‑omission rule for the derived partial (footnote 10) and outlines formalization impacts: ZBatchBridge must be replaced, PartialEval.lean updated, TraceHandoff changed to a scaled product relation, and Composition.lean updated to wire the new packages.
• HACHI_RING_SWITCHING_COMPARISON.md: This new documentation file (HACHI_RING_SWITCHING_COMPARISON.md) provides a detailed, architecturally oriented comparison between Hachi's ring-switching subprotocol and the existing ArkLib/ProofSystem/RingSwitching/ formalization (DP24/Binius). It distinguishes three different notions of “ring switching” in the project, explains why Hachi's §3 reduction is deterministic (no challenges or sumcheck rounds) while DP24's is interactive, and documents the framework mismatch (CWSS vs. RBR soundness) that prevents protocol reuse. The file also records two major structural updates as of 2026-07-17: the separation of the folder into Packing/ and Lift/ construction families, and the addition of shared verifier skeletons (RoundVerifiers.lean) and an embed-and-evaluate algebra (Transport/) that both sides consume, together with the explicit negative results on why the data layers cannot share a common parent. This document matters because it preemptively resolves recurring review questions about protocol overlap, justifies architectural decisions, and serves as living orientation for the formalization's evolving structure.
• HACHI_RING_SWITCHING_PLAN.md: This new file (HACHI_RING_SWITCHING_PLAN.md) is a detailed formalization plan for the complete interactive core of Hachi (NOZ26), covering ring switching (§3) and sumcheck (§4.3) beyond the existing Lemma 8 layer. It disambiguates three reductions called "ring switching" (Hachi packing, DP24/Binius packing, Hachi HMZ25 lift) and proposes generalizing ArkLib/ProofSystem/RingSwitching/ so one packing-phase definition serves both Binius and Hachi. The plan describes the current verified state of the repository (including two sorries in Subfield/Field.lean and Subfield/NormBound.lean), target architecture (new PackingScheme, Packing, Relocation modules), twelve design decisions (D1–D12), milestones (Phases A–H), acceptance criteria, and risks. Notably, it identifies a gap in the paper's Lemma 10 (the star extraction is insufficient) and proposes a repair using Kronecker curves (F6). The document also tracks the seam between the generic ring-switching module and Hachi-specific components, and notes that all five RingSwitching RBR soundness theorems and three completeness lemmas are currently sorried.
• HACHI_SUMCHECK_TRACK_PLAN.md: This new document (HACHI_SUMCHECK_TRACK_PLAN.md) adds a detailed implementation plan for the first four milestones (B4, F2, F3, F4) of the Hachi sumcheck track, superseding the previous v2 plan. It specifies global design decisions (G1–G6), introduces new structures such as GCWSSPackage, RlinStatement, LiftedWitness, and LiftCom, and outlines the theorems and acceptance criteria for each milestone. The plan also includes effort estimates, risk analysis, and documentation obligations, serving as a guide for implementing guarded CWSS composition, the R^lin adapter, quotient-lift algebra, and the HMZ25 lift.
• docs/skills/README.md: Added a new skills document prove-milestone.md to the skills index, describing a four-stage, paper-audited workflow for freezing and constructively proving one Hachi milestone and then improving the workflow based on run evidence.
• docs/skills/prove-milestone.md: This new docs/skills/prove-milestone.md documents a multi-stage workflow (/prove-milestone) for discharging Hachi milestones in the Lean formalization project. It defines invocation contracts, global invariants (e.g., forbidding Classical.choice, sorryAx, native_decide), required artifacts, and four explicit stages: establishing the correct formalization with paper-to-Lean correspondence and adversarial audits, developing a feasible proof architecture with a semantic freeze, discharging frozen proof obligations under strict baseline compliance, and independently verifying the result with clean-room audits. The file also includes a self-improvement pass that allows the skill to be updated based on observed failures, ensuring the workflow remains rigorous and reusable.
• docs/wiki/repo-map.md: Updated docs/wiki/repo-map.md to document the skeleton structure for §4.3 (Hachi's sumcheck-based opening), including the Escape.lean front-threading file and subprotocol folders RingSwitch, ZeroCheck, and Sumcheck, each with their respective modules and sorried CWSS theorems. Also added entries for the Recursion/ section (§4.5) and its component files (PartialEval, ZBatchBridge, TraceHandoff), noting the gap documented in HACHI_RECURSION_GAP.md. Updated the Composition.lean description to reflect composition of escape-threaded and guarded tails, and the CoordinateWiseSpecialSoundness.lean entry to note ScalarRound, Escape, and Guarded as skeletonized components with sorried assembly theorems.

---

Last updated: 2026-07-17 16:21 UTC.

[alexanderlhicks]

haven't reviewed in great detail but that seems ok for a skeleton that will likely change anyway as the formalization progresses.