Link 5 & 6 of skeleton: lemma 10 of Hachi by ErVinuelas · Pull Request #656 · Verified-zkEVM/ArkLib

ErVinuelas · 2026-07-17T12:46:26Z

Building on top of the skeleton. This PR should provide formalization for lemma 10 of the Hachi paper, which translates to links 5 and 6 of the artifact.

…i-polynomial-quadratic-eq

…ratic-eq # Conflicts: # ArkLib/Commitments/Functional/Hachi/Gadget.lean

…ratic-eq # Conflicts: # ArkLib/Commitments/Functional/Hachi/GadgetNorms.lean

Bring in the 6 base-branch updates: - add paper def for relout Fig. 3 (1998bc3) - merge origin/main (478f69b) - address PR review (4a10a65) - chore(kb): refresh generated files (Verified-zkEVM#648) - fix(ProtocolSpec): prove partial-transcript splitters for seqCompose (Verified-zkEVM#641) - Refactor/small clean up (Verified-zkEVM#629)

github-actions · 2026-07-17T12:54:05Z

🤖 PR Summary

ℹ️ Some sections were omitted to fit GitHub's comment size limit.

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Link 5 & 6 of skeleton: lemma 10 of Hachi

sorry delta: +28 (1 removed, 29 added) — proof obligations increased

Mathematical Formalization

Core Change: Formal proof of Lemma 10 (NOZ26, Figure 5) for the Hachi opening chain in ArkLib. The lemma is a uniform-vector challenge argument; the original paper proof is invalid for multivariate multilinear polynomials. The repair restricts evaluation points to Kronecker curves (Kronecker), uses univariate interpolation, and adopts resolution option 2: adding a liftShort conjunct to relZeroCheck to enable weak-binding escape.
Key Declarations:
- zeroCheck_coordinateWiseSpecialSound (CWSS) — sorry-free, axiom-clean.
- relZeroCheck — modified with liftShort conjunct.
- LiftCom — norm-conditioned collision used to discharge the weak-binding disjunct.
- evalSplit_eq_eval, splitForm_monomialBasis_eq_eval, Lemma 8 (quadEval_coordinateWiseSpecialSound).
- Composition.lean: evalChain, eval_coordinateWiseSpecialSound — escape-threaded opening chain via LiftCom.
Remaining Gaps:
- Sumcheck bridge pull-back is a skeleton sorry (noted in audit doc).
- Other residual gaps: F5 range-side soundness, constructivity, sumcheck seam.
- Repository open gaps documented: HACHI_LEMMA10_GAP.md, HACHI_RECURSION_GAP.md.

Proof Completion (sorries removed)

zeroCheck_coordinateWiseSpecialSound is now sorry-free and axiom-clean. This is the only completed proof in this PR; all other soundness proofs remain partial.

Protocols / Soundness

New CWSS Utilities (detailed in docs/wiki/repo-map.md):
- NoChallenge: provides CWSSStructure.ofIsEmpty.
- SingleRound: generic single-challenge-round machinery.
- ScalarRound: skeletonized scalar-challenge twin.
- Escape: escape-threading via Set.withEscape.
- Guarded: B4 skeleton with GCWSSPackage and sorried guarded append.
These utilities are introduced across multiple files under CoordinateWiseSpecialSoundness/ (ChallengeRound, Escape, Guarded, NoChallenge, Package, ScalarRound, SeqCompose, SingleRound) and are imported project-wide via ArkLib.lean.

Refactoring

Gadget split: The Hachi.Gadget module has been reorganized, splitting parts into separate files.
File renames: Several files in the Hachi directory have been renamed or restructured to better reflect the module hierarchy.

Documentation

New Audit Document (docs/kb/audits/noz26-zero-check-lemma10.md): Records specification boundary, formalization status, paper-to-Lean ledger, repair details, current status of key declarations, residual gaps, and resolution options considered.
Updated Paper Status (docs/kb/papers/NOZ26.md): Changed from "seeded" to "active-audit"; added related module ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean; noted Lemma 10 CWSS argument fix and cross-reference to audit note.
Updated Repo Map (docs/wiki/repo-map.md): Rewritten Hachi section to organize modules by paper section; enumerates specific definitions/theorems; documents open gaps and skeletonized subprotocols; clarifies which components are complete vs. with sorries.
Minor Updates: docs/kb/audits/README.md, docs/kb/index.md, docs/skills/README.md, docs/skills/make-pr-ready.md.

Discrepancy Note

The PR body is empty, but the actual changes (new audit doc, updated paper status and repo map, and the core formalization effort) are substantive and accurately described in the per-file summaries. The overview above is based on the actual code and documentation changes.

CRITICAL: REMAINING SORRIES

Sumcheck bridge pull-back: skeleton sorry (documented in audit doc).
Guarded module: sorried guarded append.
Commitment.lean Proof: sorry-ridden (per repo map).
A large portion of the soundness proofs in the Hachi directory remain as sorry placeholders, marking the current state as a structural skeleton rather than a complete formalization.

Statistics

Metric	Count
📝 Files Changed	62
✅ Lines Added	9524
❌ Lines Removed	661

Lean Declarations

✏️ Removed: 22 declaration(s)

ArkLib/Commitments/Functional/Hachi/Gadget.lean (12)

def IsLawfulGadgetDecomposition (base : R) {rows digits : Nat}
def gadgetDecompose {rows digits : Nat} (dd : DigitDecomposition base digits)
def gadgetEntry (base : R) {rows digits : Nat} (i : Fin rows) (j : Fin (rows * digits)) : Rq Φ
def gadgetMatrix (base : R) (rows digits : Nat) : PolyMatrix (Rq Φ) rows (rows * digits)
def gadgetMul (base : R) {rows digits : Nat} (v : PolyVec (Rq Φ) (rows * digits)) :
def zmodDigitDecomposition (b digits : ℕ) (hb : 1 < b) (hq : q ≤ b ^ digits) :
private theorem ofDigits_eq_sum_range {α : Type*} [CommSemiring α] (β : α) (L : List ℕ) :
private theorem ofDigits_eq_sum_range_of_len_le {α : Type*} [CommSemiring α] (β : α) (L : List ℕ)
theorem gadgetDecompose_apply {rows digits : Nat} (dd : DigitDecomposition base digits)
theorem gadgetDecompose_lawful {rows digits : Nat} (hd : 0 < digits) (h1 : 1 ≤ Φ.φ.natDegree)
theorem gadgetEntry_finProdFinEquiv (base : R) {rows digits : Nat} (hd : 0 < digits)
theorem gadgetMul_apply (base : R) {rows digits : Nat} (hd : 0 < digits)

ArkLib/Commitments/Functional/Hachi/GadgetNorms.lean (6)

theorem gadgetDecompose_coeff {base : ZMod q} {rows digits : ℕ}
theorem gadgetDecompose_zmod_l2NormSq_le {b digits rows : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)
theorem gadgetDecompose_zmod_lInftyNorm_le {b digits rows : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)
theorem gadgetDecompose_zmod_vecL2NormSq_le {b digits rows : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)
theorem gadgetDecompose_zmod_vecLInftyNorm_le {b digits rows : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)
theorem zmodDigit_natAbs_le {b digits : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)

ArkLib/ProofSystem/Component/SendClaim.lean (2)

def relOut : Set ((Unit × (∀ i, (Sum.elim OStatement OStatement) i)) × Unit)
theorem completeness [Nonempty σ] :

ArkLib/ProofSystem/Component/SendWitness.lean (2)

theorem oracleReduction_rbr_knowledge_soundness : True
theorem reduction_rbr_knowledge_soundness : True

✏️ Added: 347 declaration(s)

ArkLib/Commitments/Functional/Hachi/Commitment.lean (4)

def commit [DecidableEq (ZMod q)] (hb : 1 < b)
def hachi [DecidableEq (ZMod q)] (hb : 1 < b) :
def keygen :
instance multilinearEvalOracleInterface {n : ℕ} :

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

@[reducible] def openCoreSpecSampleable (ω : ℕ) (TCom F : Type) [SampleableType F]
abbrev openCoreSpec (ω : ℕ) (TCom F : Type)
def evalChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
theorem eval_coordinateWiseSpecialSound (init : 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/EvalSplit.lean (5)

@[simp] theorem toMatrix_toPolynomial (M : PolyMatrix R (2 ^ nl) (2 ^ nh)) :
@[simp] theorem toPolynomial_get (M : PolyMatrix R (2 ^ nl) (2 ^ nh))
@[simp] theorem toPolynomial_toMatrix (p : CMlPolynomial R (nl + nh)) :
def toPolynomial (M : PolyMatrix R (2 ^ nl) (2 ^ nh)) : CMlPolynomial R (nl + nh)
theorem splitForm_monomialBasis_eq_eval (M : PolyMatrix R (2 ^ nl) (2 ^ nh))

ArkLib/Commitments/Functional/Hachi/Gadget/Basic.lean (12)

def IsLawfulGadgetDecomposition (base : R) {rows digits : Nat}
def gadgetDecompose {rows digits : Nat} (dd : DigitDecomposition base digits)
def gadgetEntry (base : R) {rows digits : Nat} (i : Fin rows) (j : Fin (rows * digits)) : Rq Φ
def gadgetMatrix (base : R) (rows digits : Nat) : PolyMatrix (Rq Φ) rows (rows * digits)
def gadgetMul (base : R) {rows digits : Nat} (v : PolyVec (Rq Φ) (rows * digits)) :
def zmodDigitDecomposition (b digits : ℕ) (hb : 1 < b) (hq : q ≤ b ^ digits) :
private theorem ofDigits_eq_sum_range {α : Type*} [CommSemiring α] (β : α) (L : List ℕ) :
private theorem ofDigits_eq_sum_range_of_len_le {α : Type*} [CommSemiring α] (β : α) (L : List ℕ)
theorem gadgetDecompose_apply {rows digits : Nat} (dd : DigitDecomposition base digits)
theorem gadgetDecompose_lawful {rows digits : Nat} (hd : 0 < digits) (h1 : 1 ≤ Φ.φ.natDegree)
theorem gadgetEntry_finProdFinEquiv (base : R) {rows digits : Nat} (hd : 0 < digits)
theorem gadgetMul_apply (base : R) {rows digits : Nat} (hd : 0 < digits)

ArkLib/Commitments/Functional/Hachi/Gadget/Norms.lean (11)

theorem gadgetDecompose_coeff {base : ZMod q} {rows digits : ℕ}
theorem gadgetDecompose_zmod_l2NormSq_le {b digits rows : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)
theorem gadgetDecompose_zmod_lInftyNorm_le {b digits rows : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)
theorem gadgetDecompose_zmod_vecL2NormSq_le {b digits rows : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)
theorem gadgetDecompose_zmod_vecLInftyNorm_le {b digits rows : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)
theorem gadgetMul_zmod_coeff_natAbs_le {b rows digits : ℕ} (hd : 0 < digits)
theorem gadgetMul_zmod_lInftyNorm_le {b rows digits : ℕ} (hd : 0 < digits)
theorem gadgetMul_zmod_sub_l2NormSq_le {b rows digits : ℕ} (hd : 0 < digits)
theorem gadgetMul_zmod_vecL2NormSq_le {b rows digits : ℕ} (hd : 0 < digits)
theorem gadgetMul_zmod_vecLInftyNorm_le {b rows digits : ℕ} (hd : 0 < digits)
theorem zmodDigit_natAbs_le {b digits : ℕ} (hb : 1 < b) (hq : q ≤ b ^ digits)

ArkLib/Commitments/Functional/Hachi/QuadEval/Bridge.lean (8)

@[simp] theorem toMatrix_extractedPoly (base : ZMod q)
def bridgePackage {σ : Type} (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
def bridgeVerifier :
def extractedPoly (base : ZMod q)
def relPolyEval (base : ZMod q) (βSq γ κ : ℕ) :
def toQuadEvalStatement
theorem bridge_coordinateWiseSpecialSound {σ : Type}
theorem mem_relPolyEval_of_relIn (base : ZMod q) (βSq γ κ : ℕ)

ArkLib/Commitments/Functional/Hachi/QuadEval/Gadgets.lean (14)

def carrier (a : PolyVec (Rq Φ) messageRows)
def carrierCommit {dRows : Nat} (D : Simple.PublicParams Φ dRows (blocks * messageDigits))
def carrierDecomp {base : R} (ddCarrier : DigitDecomposition base messageDigits)
def carrierEntry (a : PolyVec (Rq Φ) messageRows)
def jMatrix (base : R) (n zDigits : Nat) : PolyMatrix (Rq Φ) n (n * zDigits)
def tensorG (base : R) (k digits : Nat) (c : PolyVec (Rq Φ) blocks)
def tensorG1 (base : R) (digits : Nat) (c : PolyVec (Rq Φ) blocks)
def zDecomp {n zDigits : Nat} {base : R} (ddZ : DigitDecomposition base zDigits)
theorem carrier_eq_gadget {base : R} (hd : 0 < messageDigits) (h1 : 1 ≤ Φ.φ.natDegree)
theorem tensorG1_coord_diff (base : R) (digits : Nat)
theorem tensorG1_sub_challenge (base : R) (digits : Nat) (c c' : PolyVec (Rq Φ) blocks)
theorem tensorG_coord_diff (base : R) (k digits : Nat)
theorem tensorG_sub_challenge (base : R) (k digits : Nat) (c c' : PolyVec (Rq Φ) blocks)
theorem z_eq_jMatrix {n zDigits : Nat} {base : R} (hd : 0 < zDigits)

ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean (19)

abbrev CarrierCom (Φ : CyclotomicModulus R) (dRows : Nat)
def InSb (β : ℕ) (a : Rq Φ) : Prop
def ShortChallenge (Φ : CyclotomicModulus (ZMod q)) (ω : ℕ) : Type
def dShort (γ : ℕ) : ModuleSIS.Solution Φ (blocks * messageDigits) → Bool
def derivedMsgMatrix (base : ZMod q)
def evalConsistency (base : ZMod q) (a : PolyVec (Rq Φ) (2 ^ m)) (b : PolyVec (Rq Φ) (2 ^ r))
def paperRelOut (base : ZMod q) (ω b : ℕ) :
def prover (WitIn : Type)
def relIn (base : ZMod q) (βSq γ κ : ℕ) :
def relOut (base : ZMod q) (ω γ : ℕ) :
def val (c : ShortChallenge Φ ω) : Rq Φ
def vecInSb (β : ℕ) {cols : ℕ} (z : PolyVec (Rq Φ) cols) : Prop
def verifier :
theorem l1Norm_le (c : ShortChallenge Φ ω) : ‖c.val‖₁ ≤ ω
theorem l1Norm_val_sub_le (c c' : ShortChallenge Φ ω) : ‖c.val - c'.val‖₁ ≤ 2 * ω
theorem lInftyNorm_le_of_InSb {β γ : ℕ} (hγ : β / 2 ≤ γ) {a : Rq Φ} (h : InSb Φ β a) :
theorem paperRelOut_subset_relOut (base : ZMod q) (ω : ℕ) {b γ : ℕ} (hγ : b / 2 ≤ γ) :
theorem val_ne_of_ne {c c' : ShortChallenge Φ ω} (h : c ≠ c') : c.val ≠ c'.val
theorem vecLInftyNorm_le_of_vecInSb {β γ cols : ℕ} (hγ : β / 2 ≤ γ)

ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean (15)

def quadEvalBetaSq (γ b τ d m δ : ℕ) : ℕ
def quadEvalPackage {ι : Type} {oSpec : OracleSpec ι} {σ : Type}
def quadEvalZL2SqBound (γ b τ d m δ : ℕ) : ℕ
noncomputable def buildWitness (base : ZMod q)
noncomputable def extractedOpening (base : ZMod q)
theorem ShortChallenge.coordEq_val {ℓ : ℕ} {i : Fin ℓ} {x y : Fin ℓ → ShortChallenge Φ ω}
theorem buildWitness_mem_relIn (hq5 : q % 8 = 5) {b ω γ : ℕ} (hκ : (2 * ω) ^ 2 < q)
theorem evalConsistency_of_relOut_star (hq5 : q % 8 = 5) {b ω γ : ℕ} (hκ : (2 * ω) ^ 2 < q)
theorem evalConsistency_of_star (base : ZMod q) (a : PolyVec (Rq Φ) (2 ^ m))
theorem inner_eq_of_chain {base : ZMod q} {cols : Nat}
theorem msis_of_commit_eq {rows cols γ : ℕ}
theorem quadEval_coordinateWiseSpecialSound {ι : Type} {oSpec : OracleSpec ι} {σ : Type}
theorem quadEval_coordinateWiseSpecialSound_paperParams {ι : Type} {oSpec : OracleSpec ι} {σ : Type}
theorem slack_isUnit (hq5 : q % 8 = 5) {ω : ℕ} (hκ : (2 * ω) ^ 2 < q)
theorem verifiedOpening_of_star (hq5 : q % 8 = 5) {b ω γ : ℕ} (hκ : (2 * ω) ^ 2 < q)

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 rBound))
def relPartialEvalE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
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 liftPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
def liftProver (WitIn : Type)
def liftShort (bound rBound : ℕ) (w : LiftedWitness Φ μ n) : Prop
def liftVerifier :
def rShort (rBound : ℕ) (r : Fin n → Polynomial (ZMod q)) : Prop
def relLift (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
def relLiftE (K : LiftCom (LiftedWitness Φ μ n) E (liftShort Φ bound rBound))
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)

…and 197 more not listed.

✏️ Affected: 4 declaration(s) (line number changed)

def oracleProver : OracleProver oSpec in ArkLib/ProofSystem/Component/SendClaim.lean moved from L36 to L70
def oracleReduction : OracleReduction oSpec in ArkLib/ProofSystem/Component/SendClaim.lean moved from L92 to L98
def oracleVerifier : OracleVerifier oSpec in ArkLib/ProofSystem/Component/SendClaim.lean moved from L63 to L84
def pSpec : ProtocolSpec 1 in ArkLib/ProofSystem/Component/SendClaim.lean moved from L31 to L58

sorry Tracking

✅ Removed: 1 `sorry`(s)

ArkLib/ProofSystem/Component/SendWitness.lean (1)

theorem oracleVerifier_toVerifier_run {stmt : Statement} {oStmt : ∀ i, OStatement i} (L248)

❌ Added: 29 `sorry`(s)

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

def hachi [DecidableEq (ZMod q)] (hb : 1 < b) : (L151)

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/Constraints.lean (6)

def hypercubeSum (H : MvPolynomial (Fin m₀) F) (i : ℕ) (cs : Fin i → F) : F (L258)
def sumcheckPolyAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (α : F) (L247)
def sumcheckPolyZero (φF : ZMod q →+* F) (b : ℕ) (τ₀ : Fin m₀ → F) (L240)
def zcTargetAlpha (φF : ZMod q →+* F) (s : RlinStatement Φ n μ) (α : F) (L253)
theorem sum_sumcheckPolyAlpha (φF : ZMod q →+* F) (b : ℕ) (s : RlinStatement Φ n μ) (α : F) (L272)
theorem sum_sumcheckPolyZero (φF : ZMod q →+* F) (b : ℕ) (τ₀ : Fin m₀ → F) (L265)

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

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

Last updated: 2026-07-17 17:32 UTC.

tobias-rothmann and others added 27 commits July 1, 2026 16:30

CWSS protocol infrastructure

6a60715

qudaratic eq messy

14acadf

clean up

63c9242

Merge branch 'main' into cwss-components-infra

a763723

Merge branch 'cwss-components-infra' into hachi-polynomial-quadratic-eq

a6b2eed

Merge remote-tracking branch 'origin/cwss-components-infra' into hach…

7cda2e3

…i-polynomial-quadratic-eq

remove classical

c33ad9a

Merge remote-tracking branch 'origin/cwss-components-infra' into hach…

6ac3bfa

…i-polynomial-quadratic-eq

CWSSPackage for (more) readble CWSS composition

f6fbf03

huge commit

1f0bfcc

merge

4224003

Merge remote-tracking branch 'origin/main' into hachi-polynomial-quad…

acf104f

…ratic-eq # Conflicts: # ArkLib/Commitments/Functional/Hachi/Gadget.lean

Merge branch 'main' into hachi-polynomial-quadratic-eq

4df3bbf

composition plan

f8eca05

merge

bef1984

initial skeleton

59c9af8

address PR review

4a10a65

Merge remote-tracking branch 'origin/main' into hachi-polynomial-quad…

478f69b

…ratic-eq # Conflicts: # ArkLib/Commitments/Functional/Hachi/GadgetNorms.lean

add paper def for relout Fig. 3

1998bc3

skeleton

1a648d9

skeleton site

c8ed741

move hachi artifact

7501ae8

Merge branch 'main' into hachi-skeleton

733fb21

prove milestone skill

f5135e2

update hachi plan

5c2f128

Towards the formalization of lemma 10: link 6 of artifact

2927997

ErVinuelas added 2 commits July 17, 2026 16:18

lemma 5 and wTable def

63a3be2

variable renaming and documentation

34f7318

ErVinuelas changed the title ~~Link 6 of skeleton: lemma 10 of hachi~~ Link 5 & 6 of skeleton: lemma 10 of Hachi Jul 17, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Link 5 & 6 of skeleton: lemma 10 of Hachi#656

Link 5 & 6 of skeleton: lemma 10 of Hachi#656
ErVinuelas wants to merge 29 commits into
Verified-zkEVM:mainfrom
ErVinuelas:lemma10-on-650

ErVinuelas commented Jul 17, 2026

Uh oh!

github-actions Bot commented Jul 17, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

ErVinuelas commented Jul 17, 2026

Uh oh!

github-actions Bot commented Jul 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Mathematical Formalization

Proof Completion (sorries removed)

Protocols / Soundness

Refactoring

Documentation

Discrepancy Note

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented Jul 17, 2026 •

edited

Loading