refactor(Hachi/CWSS): cwss packages with escape

[tobias-rothmann]

CWSS packages with escape threading

Adds a protocol-agnostic escape abstraction to the coordinate-wise special-soundness
(CWSS) composition machinery, and refactors the package layer into a clean 2×2 lattice
of package kinds joined by a single universal append ▷.

Motivation: escapes belong to composition, not to relations

In a composed special-soundness chain, a downstream extractor may fail to produce a real
witness and instead return a cryptographic escape — e.g. a commitment binding-break that
is a Module-SIS solution via weak binding (Hachi's w̃-commitment, [NOZ26] Remark 2 /
Lemma 7). Composed extraction feeds each extractor's output into the previous seam relation,
so every relation upstream of the escape's origin needs somewhere to put it.

The naive fix — bake an escape disjunct into each subprotocol's own relIn/relOut — pollutes
every upstream relation definition with cryptographic plumbing it shouldn't know about.

This PR keeps the subprotocol relations ordinary and threads the escape on a parallel seam
that is only widened into the relation inside the special-soundness certificate. Escape
handling shifts from relation definitions to appending / protocol composition. Because an
escape (an MSIS/collision solution) is checkable against the commitment key alone, it is
statement-independent: it passes through statement maps trivially, and the escape branch of
every seam extractor is the identity Sum.inr.

Core primitive: Set.withEscape

withEscape (rel : Set (S × W)) (esc : Set E) : Set (S × (W ⊕ E))

Widens an ordinary relation to accept escapes on the right summand (+ lemmas:
mem_withEscape_inl/inr, mem_withEscape_language_iff, withEscape_empty_iff). The widening
lives inside each package's certificate — the public relIn/relOut stay escape-free.

The four package kinds — the 2×2 lattice (escape? × guarded?)

Every kind carries verifier, struct, relIn, relOut, and an isCWSS certificate; the
escape kinds add escIn/escOut plus escape_mono : escOut ⊆ escIn (escapes may grow up the
chain but are never discarded).

Package	Escape-aware	Guarded (verifier may reject at runtime)	Certificate is over…	Native infix	File
CWSSPackage	–	– (pure)	relIn / relOut	▷	Package.lean
GCWSSPackage	–	✓	relIn / relOut	▷ᵍ	Guarded.lean
EscapeCWSSPackage	✓	– (pure)	relIn.withEscape escIn / relOut.withEscape escOut	▷ₑ	Escape.lean
EscapeGCWSSPackage	✓	✓	relIn.withEscape escIn / relOut.withEscape escOut	▷ₑᵍ	Escape.lean

The guarded axis (from the sumcheck track) models a left factor whose verifier may reject:
if check stmt tr then pure (out …) else failure. This is needed exactly where a runtime check
reads sent/input data that the downstream statement type drops (sumcheck round targets,
final-eval check, recursion handoff), which pure/relation-only verifiers cannot express.

Lifting: an escape-free / pure package enters a richer chain for free

Escape packages need only be defined for the subprotocols that genuinely produce escapes;
everything else is lifted automatically at composition time.

Lift	From → To	Semantics
CWSSPackage.toGuarded / EscapeCWSSPackage.toGuarded	pure → guarded (both escape columns)	lossless — purity is the check := true special case
CWSSPackage.withEscape / GCWSSPackage.withEscape	escape-free → escape-aware (both rows)	constant budget escIn = escOut (passes downstream escapes through unchanged)
coordinateWiseSpecialSound.withEscape	certificate-level widening to any escape set E	underpins the package lifts; treeSpecialSound.withEscape at the tree level

Composition: one universal ▷ over all 16 pairings

L₁ ▷ L₂ composes any two package kinds at the join of their kinds, inserting the
withEscape / toGuarded lifts on the fly and choosing escape budgets so the escape seam holds
definitionally (only the ordinary relation seam hRel, and between two escape-aware factors the
escape seam hEsc, remain — both discharged by rfl). Join semantics: escape-free ▷ escape-free
stays escape-free, pure ▷ pure stays pure, and a single escape-aware or guarded factor lifts the
rest of the chain.

• All 16 (4×4) appends are implemented (append, appendEscape, appendGuarded,
  appendEscapeGuarded, appendPure, …) and wired into a single dispatch table univAppendFn.
• ▷ is a single scoped elaborator that reads each factor's head constant and applies the
  unique compatible append — linear in chain length. Overloaded-notation choice nodes would
  re-elaborate nested alternatives exponentially (a 5-link Hachi chain already exhausts the
  heartbeat budget). The kind-marked ▷ₑ, ▷ᵍ, ▷ₑᵍ remain as explicit single-target synonyms;
  repo code composes with the universal ▷ throughout.

[github-actions]

🤖 PR Summary

sorry delta: -1 (1 removed) — net proof progress

This refactor PR replaces the prior escape-threaded evaluation-chain approach with a protocol-agnostic escape abstraction embedded into the CWSS composition machinery itself. It does not close any sorries; callers who rely on the old Escape.lean file must port to the new EscapeCWSSPackage / EscapeGCWSSPackage types.

---

Statistics

Metric	Count
📝 Files Changed	49
✅ Lines Added	1895
❌ Lines Removed	5175

---

Lean Declarations

✏️ Removed: 25 declaration(s)

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/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/QuadEval/Soundness.lean (1)

• theorem buildWitness_mem_relIn (hq5 : q % 8 = 5) {b ω γ : ℕ} (hκ : (2 * ω) ^ 2 < q)

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

• theorem mem_relPartialEvalE_of_relHatEvalE (zpow : Fin (2 ^ κ) → F)

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

• theorem mem_relOutE_of_relRlinE (base : ZMod q) (ω γ : ℕ) (esc : Set E)

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

• theorem mem_relZeroCheckE_of_roundRelE

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

• theorem mem_relLiftE_of_relBatchedE

✏️ Added: 44 declaration(s)

ArkLib/Commitments/Functional/Hachi/Gadget/Core.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/QuadEval/Reduction.lean (3)

• abbrev QuadEvalWitness (Φ : CyclotomicModulus R)
• def quadEvalSISSet
• def self

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

• noncomputable def buildWitnessWithEscape {E : Type} {ω γ : ℕ} (base : ZMod q)
• theorem buildWitnessWithEscape_mem (hq5 : q % 8 = 5) {E : Type} {b ω γ : ℕ}
• theorem buildWitness_mem_relIn_withEscape (hq5 : q % 8 = 5) {b ω γ : ℕ}

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

• theorem mem_relPartialEval_of_relHatEval (zpow : Fin (2 ^ κ) → F)

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

• theorem mem_relOut_of_relRlin

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

• theorem mem_relZeroCheck_of_roundRel

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

• theorem roundsChain_escIn (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• theorem roundsChain_escOut (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))

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

• theorem mem_relLift_of_relBatched

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

• def CWSSPackage.appendEscape {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def CWSSPackage.appendEscapeGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def CWSSPackage.withEscape {E StmtIn WitIn StmtOut WitOut : Type}
• def EscapeCWSSPackage.appendEscapeGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeCWSSPackage.appendGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeCWSSPackage.appendPure {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeGCWSSPackage.appendEscape {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeGCWSSPackage.appendGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeGCWSSPackage.appendPure {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def GCWSSPackage.appendEscape {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def GCWSSPackage.appendEscapeGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def GCWSSPackage.withEscape {E StmtIn WitIn StmtOut WitOut : Type}
• def _root_.CoordinateWise.EscapeCWSSPackage.toGuarded
• def append {E StmtA WitA StmtB WitB StmtC WitC : Type}
• private def packageKindOf (e : Expr) : TermElabM Name
• private def univAppendFn : Name → Name → Option Name
• theorem coordinateWiseSpecialSound.withEscape {E : Type} (esc : Set E)
• theorem treeSpecialSound.withEscape {E : Type} (esc : Set E)

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

• def CWSSPackage.appendGuarded {StmtA WitA StmtB WitB StmtC WitC : Type}
• def GCWSSPackage.appendPure {StmtA WitA StmtB WitB StmtC WitC : Type}

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

• def relPolyEval in ArkLib/Commitments/Functional/Hachi/QuadEval/Bridge.lean moved from L169 to L167
• theorem mem_relPolyEval_of_relIn in ArkLib/Commitments/Functional/Hachi/QuadEval/Bridge.lean moved from L186 to L183
• def paperRelOut in ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean moved from L277 to L349
• def relIn in ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean moved from L323 to L395
• def relOut in ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean moved from L211 to L281
• theorem paperRelOut_subset_relOut in ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean moved from L306 to L380
• def quadEvalPackage {ι : Type} {oSpec : OracleSpec ι} {σ E : Type} in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L493 to L590
• theorem quadEval_coordinateWiseSpecialSound {ι : Type} {oSpec : OracleSpec ι} {σ E : Type} in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L444 to L531
• theorem quadEval_coordinateWiseSpecialSound_paperParams in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L471 to L566
• def rlinStmt in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L95 to L98

---

sorry Tracking

✅ Removed: 1 `sorry`(s)

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

• theorem quadEval_coordinateWiseSpecialSound_withEscape (L147)

---

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 (+0/-1079)

* 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: The import structure in ArkLib.lean is refactored: top-level modules Escape, Gadget, InnerOuter, QuadEval, RingSwitch, Sumcheck, and ZeroCheck are replaced by their respective .Basic submodules (and Gadget.Core is added). A new import ArkLib.Commitments.Functional.Hachi.Recursion.Basic is introduced. These changes reflect a reorganization of the Hachi commitment scheme into finer-grained submodules, which improves modularity and may affect dependency resolution.
• ArkLib/Commitments/Functional/Hachi.lean: The file’s module‑level documentation comments were updated to reflect a reorganization of the Hachi/ subfolder structure: subfolders now use a Basic.lean umbrella re‑export (instead of a sibling .lean file), and the Gadget subfolder’s core file is renamed from Basic to Core. Three new subfolders — RingSwitch/, ZeroCheck/, and Sumcheck/ (§4.3) — and a Recursion/ subfolder (§4.5) were added to the documented structure. The description of Composition.lean was revised to mention that it now hosts the opening subprotocols in addition to the previously documented evalChain, and that packages expose a relIn/relOut flow with a parallel escape set. The existing Commitment.lean entry (including the noted sorry for the Proof type) is unchanged. No definitions, theorems, or code were added or modified; only documentation comments were updated.
• ArkLib/Commitments/Functional/Hachi/Commitment.lean: The import statement was changed from ArkLib.Commitments.Functional.Hachi.QuadEval to ArkLib.Commitments.Functional.Hachi.QuadEval.Basic, reflecting a refactor that split or renamed the QuadEval module (likely introducing QuadEval.Basic as the new home for the core definitions previously exported by QuadEval). This ensures the Commitment.lean file still has access to the required definitions after the module structure change.
• ArkLib/Commitments/Functional/Hachi/Composition.lean: The file underwent a major refactoring to unify pure and guarded composition under a universal ▷ operator, replacing the prior CWSSPackage/GCWSSPackage with EscapeCWSSPackage/EscapeGCWSSPackage and threading an explicit escape set esc (of type Set E) and a QuadEvalEscapeMap parameter Q through all core definitions and theorems: evalChain, openCore, openingChain, and their companion _coordinateWiseSpecialSound proofs now accept these new arguments along with Hachi.PublicParamsD and QuadEvalEscapeMap. The composition in openingChain no longer uses .toGuarded or the separate ▷ᵍ operator; instead it calls EscapeCWSSPackage.appendEscapeGuarded with explicit seam lemmas (roundsChain_relIn, _escIn, _relOut, _escOut) and uses the universal ▷ for all remaining links. The module docstring and the chain table were updated to drop the E suffix from relation names (e.g., relPolyEvalE → relPolyEval) and to describe the new escape-set handling. The import was changed from ArkLib.Commitments.Functional.Hachi.QuadEval to ArkLib.Commitments.Functional.Hachi.QuadEval.Basic.
• ArkLib/Commitments/Functional/Hachi/Escape.lean: This pull request deletes ArkLib/Commitments/Functional/Hachi/Escape.lean, which defined the escape-threaded Hachi evaluation chain. The file introduced escape-budget E and escape set esc abstractions into the existing polynomial evaluation and QuadEval relations, producing relPolyEvalE, relInE, and relOutE via Set.withEscape. It provided a bridgePackageE CWSS package with a sorry-free mem_relPolyEvalE_of_relInE pull-back, a quadEvalPackageE package using the sorried quadEval_coordinateWiseSpecialSound_withEscape theorem, and the composed evalChainE drop-in. Despite working towards milestone F2.0, the entire file is now removed.
• ArkLib/Commitments/Functional/Hachi/Gadget/Basic.lean: This diff replaces the entire content of ArkLib/Commitments/Functional/Hachi/Gadget/Basic.lean. It removes all the original definitions, theorems, and proofs (DigitDecomposition, zmodDigitDecomposition, gadgetEntry, gadgetMatrix, gadgetMul, IsLawfulGadgetDecomposition, gadgetDecompose, gadgetDecompose_lawful, and the supporting lemmas), and replaces them with a module-level docstring that re-exports two submodules Gadget/Core.lean and Gadget/Norms.lean, describing their contents. The original imports have been replaced with imports of those two submodules.
• ArkLib/Commitments/Functional/Hachi/Gadget/Core.lean: This new file introduces the base-b gadget matrix G = I_rows ⊗ [1, b, …, b^(digits-1)] over the cyclotomic ring Rq Φ and its norm-reducing inverse G⁻¹ (the genuine base-b digit decomposition from the Hachi commitment). Key definitions include gadgetMatrix, gadgetMul, IsLawfulGadgetDecomposition, DigitDecomposition (abstract digit map with reconstruction law), zmodDigitDecomposition (concrete digits over ZMod q, valid when 1 < b and q ≤ b ^ digits), and gadgetDecompose (the gadget inverse induced by a DigitDecomposition). The main theorem gadgetMul_apply expresses the gadget product row as a base-weighted sum of the digits slots of the corresponding block. Theorem gadgetDecompose_lawful proves that gadgetDecompose satisfies G · G⁻¹(x) = x, i.e., it is a lawful gadget decomposition, which will be used to instantiate the inner-outer correctness theorem. Two auxiliary private lemmas (ofDigits_eq_sum_range, ofDigits_eq_sum_range_of_len_le) are also added. No sorry or admit appears.
• ArkLib/Commitments/Functional/Hachi/Gadget/Norms.lean: Changes ArkLib/Commitments/Functional/Hachi/Gadget/Norms.lean to import ArkLib.Commitments.Functional.Hachi.Gadget.Core instead of the previous ..Gadget.Basic, updating the dependencies of this norms file after a likely refactor of the Gadget module structure.
• ArkLib/Commitments/Functional/Hachi/InnerOuter/Basic.lean: This change renames the file ArkLib/Commitments/Functional/Hachi/InnerOuter.lean to ArkLib/Commitments/Functional/Hachi/InnerOuter/Basic.lean (moving it into a new subdirectory) and updates its module-level docstring to clarify that it now serves as an umbrella module for the Hachi/InnerOuter/ subdirectory, while otherwise leaving the file content unchanged.
• ArkLib/Commitments/Functional/Hachi/InnerOuter/Scheme.lean: The import ArkLib.Commitments.Functional.Hachi.Gadget.Basic was replaced with ArkLib.Commitments.Functional.Hachi.Gadget.Core, updating the dependency to a different (presumably core) gadget module. No other changes were made to the file.
• ArkLib/Commitments/Functional/Hachi/QuadEval/Basic.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The file `ArkLib/Commitm... were added or removed.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• ArkLib/Commitments/Functional/Hachi/QuadEval/Bridge.lean: The file is refactored to separate the public parameters pp from the PolyEvalStatement structure (removing the pp field) and make them an explicit parameter of the relations relPolyEval and relIn and of the theorems mem_relPolyEval_of_relIn and bridge_coordinateWiseSpecialSound. The relation relPolyEval is simplified from a three‑disjunct relation (opening, MSIS for B, MSIS for D) to a single opening condition requiring a VerifiedOpening whose extracted polynomial evaluates to the claimed value. Correspondingly, mem_relPolyEval_of_relIn is rewritten to avoid pattern‑matching on witness variants. The bridgePackage is changed from a CWSSPackage to an EscapeCWSSPackage that carries a passive escape set, using .withEscape on the CWSS certificate; the import is updated to CoordinateWiseSpecialSound.Escape accordingly. The E type variable is added to the relevant sections.
• ArkLib/Commitments/Functional/Hachi/QuadEval/Gadgets.lean: The comments in ArkLib/Commitments/Functional/Hachi/QuadEval/Gadgets.lean were updated to refer to the gadget matrix definitions from Gadget/Core.lean instead of the previous Gadget/Basic.lean, reflecting a reorganization of the gadget module.
• ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean: This diff refactors the QuadEval reduction file by removing the public parameters (A, B, D) from the QuadEvalStatement structure (making them a fixed reduction parameter pp instead of adversary-chosen statement data), and correspondingly adds pp as an explicit parameter to relOut, paperRelOut, relIn, and paperRelOut_subset_relOut. The QuadEvalWitness is simplified from a three-constructor inductive (opening, msisB, msisD) to a plain abbreviation for Opening, while the Module-SIS escape outcomes are moved to a new separate QuadEvalSISBreak inductive and a new quadEvalSISSet definition that checks solutions against the fixed key pp. A new structure QuadEvalEscapeMap (with a self canonical embedding) is introduced to embed these local escapes into a common ambient type, and relIn is correspondingly simplified to no longer include the Module-SIS disjuncts (only VerifiedOpening and evalConsistency). The commit also updates several comments to explain the rationale for keeping the key out of the statement.
• ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean: The diff refactors Soundness.lean to integrate an EscapeCWSSPackage interface, adding escape-based handling of Module-SIS breaks (local QuadEvalSISBreak) to the coordinate-wise special-soundness proof. Key changes: buildWitness now returns a sum type QuadEvalWitness ⊕ QuadEvalSISBreak and its correctness lemma is replaced by buildWitness_mem_relIn_withEscape (which returns (relIn …).withEscape (quadEvalSISSet …)). New buildWitnessWithEscape and buildWitnessWithEscape_mem propagate existing branch escapes and map local SIS breaks into an ambient escape set. The theorems verifiedOpening_of_star, evalConsistency_of_relOut_star, and quadEval_coordinateWiseSpecialSound now take an explicit pp : Hachi.PublicParamsD … parameter and use relOut … pp … / relIn … pp …. The quadEval_coordinateWiseSpecialSound theorem gains esc, pp, and Q : QuadEvalEscapeMap parameters, concluding with (relIn …).withEscape (esc ∪ Q.localEsc) and (relOut …).withEscape esc. The quadEvalPackage definition is updated to an EscapeCWSSPackage with escIn, escOut, and escape_mono fields, and the import CoordinateWiseSpecialSound.Package is replaced by CoordinateWiseSpecialSound.Escape. No sorry or admit are added.
• ArkLib/Commitments/Functional/Hachi/Recursion/Basic.lean: Created ArkLib/Commitments/Functional/Hachi/Recursion/Basic.lean as the umbrella module for Hachi/Recursion/. It re-exports TraceHandoff (which transitively imports ZBatchBridge and PartialEval) and documents the folder structure: PartialEval.lean transforms the final multilinear-evaluation claim into partial evaluations; ZBatchBridge.lean packs those into relHatEval; TraceHandoff.lean performs the guarded trace handoff into the next iteration's QuadEval.relIn relation while carrying the ambient escape set separately. The full guarded chain is composed in sibling Composition.lean.
• ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean: The file refactors relPartialEvalE and partialEval_coordinateWiseSpecialSound to accept an explicit esc : Set E parameter, replacing the previous implicit use of K.esc. The partialEvalPackage is changed from CWSSPackage to EscapeCWSSPackage, now storing esc as escIn/escOut and using relWEvalClaim/relPartialEval (without the E suffix) as relIn/relOut, with an escape_mono field. The proof of partialEval_coordinateWiseSpecialSound remains sorry.
• ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean: This diff refactors the trace handoff protocol definitions to remove the pp' public-parameter argument from toNextQuadEvalStatement, handoffVerifier, handoffVerifier_isGuarded, and handoffProver, and to convert handoffPackage from a GCWSSPackage to an EscapeGCWSSPackage with an explicit escape set esc. The theorem handoff_coordinateWiseSpecialSound gains an esc : Set E parameter and changes its relation types from relHatEvalE/relInE to (relHatEval …).withEscape esc and (relIn …).withEscape esc. The comment documentation is updated accordingly: toNextQuadEvalStatement's docstring explains that pp' is no longer statement data; the soundness proof plan now mentions ambient escapes passing through independently; and the handoffPackage docstring describes it as a 'guarded escape-aware package' carrying esc unchanged between relHatEval and relIn. The toNextQuadEvalStatement itself still contains a sorry.**
• ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean: Renamed relPartialEvalE to relPartialEval and relHatEvalE to relHatEval throughout (both are relation definitions). The escape-threaded relation relHatEvalE now takes an explicit esc : Set E parameter, replacing the previous use of K.esc. The theorem mem_relPartialEvalE_of_relHatEvalE was renamed to mem_relPartialEval_of_relHatEval, its witness type changed from LiftedWitness Φ μ n ⊕ E to LiftedWitness Φ μ n, and its hypothesis/conclusion now refer to the non-E relations; the proof remains sorry. The package zBatchPackage was refactored from a CWSSPackage to an EscapeCWSSPackage, taking an additional esc : Set E parameter, using relPartialEval/relHatEval as relations (with escIn/escOut both set to esc), and the isCWSS field now uses the escape‑threaded relations with esc and splits the witness case analysis accordingly.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Basic.lean: The file was renamed from RingSwitch.lean to RingSwitch/Basic.lean, reflecting the reorganization of the RingSwitch/ folder. The module doc comment and folder-structure descriptions were updated: the output relation names relOutE and relRlinE are now relOut and relRlin, and the plain relLift replaces relLiftE. The text now notes that the package carries the parallel escape set unchanged, and the umbrella description states that relLift (rather than relLiftE) is the input to the batching bridge. These are purely documentation and naming changes; no theorems, definitions, or proofs were modified, and no sorry or admit was introduced.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean: Added an explicit esc : Set E parameter to relLiftE, lift_coordinateWiseSpecialSound, and liftPackage. The relLiftE definition now uses the passed esc rather than K.esc; lift_coordinateWiseSpecialSound’s relation statements change to use esc ∪ K.esc for the input relation and esc for the output relation (still sorried). liftPackage’s return type changes from CWSSPackage to EscapeCWSSPackage, with new fields escIn, escOut, and escape_mono := Set.subset_union_left, and its relIn/relOut now refer to the plain (non-escape) relations relRlin/relLift. The comment is updated to reflect the EscapeCWSSPackage structure and that backwards extraction grows esc by K.esc.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean: Refactored the adapter from CWSSPackage to EscapeCWSSPackage, separating the escape set from the relations. rlinStmt and mem_relOut_of_relRlin (renamed from mem_relOutE_of_relRlinE) now take an explicit pp parameter and operate on plain relOut/relRlin instead of their escape-threaded versions. The rlinPackage definition adds escIn/escOut/escape_mono fields and updates the isCWSS proof to apply ReduceClaim.verifier_coordinateWiseSpecialSound to (relOut …).withEscape esc. Imports were expanded to QuadEval.Reduction, ReduceClaim, and the coordinatewise special‑soundness escape/no‑challenge modules.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/Basic.lean: This diff renames the file from ArkLib/Commitments/Functional/Hachi/Sumcheck.lean to ArkLib/Commitments/Functional/Hachi/Sumcheck/Basic.lean, making it an umbrella module. The module-level docstring is updated to clarify it is an "Umbrella module" and to replace the output relation name relWEvalE with relWEvalClaim. Additionally, the description of the guarded append in Sumcheck/Rounds.lean is revised from "append ▷ᵍ" to "binary guarded append"; the sorried status of round_coordinateWiseSpecialSound remains unchanged.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/Bridge.lean: The theorem mem_relZeroCheckE_of_roundRelE is renamed to mem_relZeroCheck_of_roundRel and its signature changed: it now uses relZeroCheck and roundRel (without E suffix) and accepts a plain LiftedWitness (dropping the ⊕ E sum type); the theorem remains sorried. The sumcheckBridgePackage is refactored from a CWSSPackage into an EscapeCWSSPackage, adding a parameter esc : Set E and new fields escIn, escOut, escape_mono. The relIn field now uses relZeroCheck with .withEscape esc instead of relZeroCheckE, and relOut uses roundRelE with an additional escape argument. The isCWSS proof is updated to pattern-match on the witness, calling mem_relZeroCheck_of_roundRel for the inl case and using the hypothesis directly for the inr escape case.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean: Changes in ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean make the escape set an explicit parameter throughout the final-evaluation step. relWEvalClaimE and finalEval_coordinateWiseSpecialSound gain an additional esc : Set E argument; the latter passes it to both roundRelE and relWEvalClaimE. finalEvalPackage now returns an EscapeGCWSSPackage instead of GCWSSPackage, accepts esc as a parameter, and replaces roundRelE with roundRel and relWEvalClaimE with relWEvalClaim in the relation fields, adding explicit escIn, escOut, and escape_mono fields. The theorem finalEval_coordinateWiseSpecialSound remains sorried (contains sorry).
• ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean: The file refactors the sumcheck round package from GCWSSPackage to EscapeGCWSSPackage, adding an escape set parameter esc : Set E throughout. This change is applied to roundPackage, roundsChainAux, and roundsChain, which now return EscapeGCWSSPackage with escIn/escOut fields; the auxiliary roundsChainAux additionally returns proofs that these escape sets equal the ambient esc. The theorem round_coordinateWiseSpecialSound gains an esc argument, and its statement now uses roundRelE with the escape set for both input and output relations. The base case of roundsChainAux is updated to EscapeCWSSPackage.toGuarded, and roundRel (without the E suffix) replaces roundRelE in the package's relation fields, while the sorried theorem still uses roundRelE. New theorems roundsChain_escIn and roundsChain_escOut expose the escape-set properties. A comment is updated to remove the ▷ᵍ notation and to update the umbrella reference to Sumcheck/Basic.lean.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Basic.lean: The file ArkLib/Commitments/Functional/Hachi/ZeroCheck.lean was renamed to ArkLib/Commitments/Functional/Hachi/ZeroCheck/Basic.lean, moving it into a subfolder as the umbrella module for the zero-check subprotocol. The documentation comment updates the description to clarify that relZeroCheck (previously relZeroCheckE) is the plain output relation passed to the sumcheck bridge, and adjusts line wrapping in the module header.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Batch.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='This diff renames the re...itself remains sorried.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean: This commit modifies the comment on hAlpha_degreeOf_le to update the cross-reference from Sumcheck.lean to Sumcheck/Basic.lean. It also adds a new parameter esc : Set E to roundRelE, changing the function signature from 5 to 6 explicit arguments; the definition now passes esc (instead of K.esc) as the second argument to .withEscape.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean: Modified relZeroCheckE to accept an explicit escape set esc : Set E instead of using K.esc. Updated zeroCheck_coordinateWiseSpecialSound to take esc as an extra argument and pass esc to both relBatchedE and relZeroCheckE. Refactored zeroCheckPackage from a CWSSPackage to an EscapeCWSSPackage, changing the relation types to relBatched and relZeroCheck (without the E suffix), adding escIn and escOut fields set to esc, and adding escape_mono := fun _ h => h. The proof zeroCheck_coordinateWiseSpecialSound remains sorry.
• ArkLib/Commitments/Functional/Hachi/hachi-overview.html: The overview legend and spine now use the operator ▷ₑᵍ (instead of ▷ᵍ) for guarded composition and describe the escape mechanism as a parallel seam carried per‑package via EscapeCWSSPackage (replacing the earlier threaded budget notation). All relation names throughout the SPINE, SUB_CROSS, and ROADMAP data have had the trailing “E” dropped (e.g. relPolyEvalE → relPolyEval), reflecting that the ordinary relation seam no longer carries an explicit escape budget. The file index has been reorganized: umbrella entries such as QuadEval.lean and RingSwitch.lean are replaced by sub‑directory entries (QuadEval/Basic.lean, RingSwitch/Basic.lean, etc.), and a new Recursion section (with Basic.lean, PartialEval.lean, ZBatchBridge.lean, TraceHandoff.lean) has been added. The escape‑threading sub‑cross entry changed its status from wip (1 sorry) to proven (0 sorries) and its file reference from Escape.lean to CWSS/Escape.lean, while the roadmap’s first item now references relPolyEval instead of relPolyEvalE.
• ArkLib/Data/Lattices/CyclotomicRing/Rq.lean: The diff corrects an outdated module path in a documentation comment: the reference to ArkLib/Commitments/Functional/Hachi/Gadget.lean is updated to ArkLib/Commitments/Functional/Hachi/Gadget/Core.lean. No other changes are present.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Escape.lean: This commit heavily revamps Escape.lean: the module docstring is rewritten to introduce a package lattice (EscapeCWSSPackage, EscapeGCWSSPackage) and a universal append operator ▷; new theorems treeSpecialSound.withEscape and coordinateWiseSpecialSound.withEscape transport escape widening to special-soundness certificates; lifting functions such as CWSSPackage.withEscape and GCWSSPackage.withEscape let escape‑free packages enter escape chains, and the elaboration‑level dispatch unifies all sixteen ordered compositions. The import is changed from ArkLib.OracleReduction.Prelude to ArkLib.OracleReduction.Security.CoordinateWiseSpecialSound.Guarded, and no sorry or admit is introduced.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean: Updated doc comments (module header, GCWSSPackage structure, and append definition) to reflect that the infix notation is now ▷ (with explicit synonym ▷ᵍ) and added two new definitions CWSSPackage.appendGuarded and GCWSSPackage.appendPure that compose a pure package with a guarded package (in either order) by lifting the pure side via CWSSPackage.toGuarded and then using GCWSSPackage.append, with a default rfl argument for the relation seam. A new section comment explains the overall lifting scheme and the universal ▷ elaborator defined in Escape.lean. These changes enable mixed pure‑guarded composition and align the notation with the project‑wide ▷ overload.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Package.lean: This commit updates the Package.lean file's module-level docstring to note that the ▷ operator is now a single universal elaborator defined in Escape.lean (dispatching over pure, guarded, escape-aware, or both package kinds), rather than being defined locally. It also removes the scoped infixr:65 ▷ notation definition that was previously in this file, since the operator is now defined and made available elsewhere.
• HACHI_GENERIC_RING_SWITCH_PLAN.md: The file HACHI_GENERIC_RING_SWITCH_PLAN.md was deleted. It previously contained a detailed implementation plan for integrating a Hachi §3.1 packing head into a Generic/ ring-switching layer, outlining design decisions, dependency orders, and phased deliverables (phases 0–7) for modifying Lean and other source files in the project. The deletion removes this planning document from the repository.
• HACHI_LEMMA10_GAP.md: The file HACHI_LEMMA10_GAP.md was deleted. It contained a detailed analysis of a counterexample refuting Lemma 10's coordinate-wise special soundness claim in the Hachi protocol, along with repair strategies (e.g., Kronecker-curve challenges) and formalization statements. Its removal likely indicates that this analysis has been integrated into the main formalization plan or superseded by subsequent documentation.
• HACHI_RECURSION_GAP.md: The file HACHI_RECURSION_GAP.md was deleted. This document had analyzed a knowledge-soundness gap in the Hachi protocol's partial-evaluation step (§4.5/§3.2), where the packed claim f′(x_rest) = ∑ᵢ yᵢ·Z^{⟨i⟩}} fails to force all partial evaluations yᵢ to equal the honest fᵢ(x_rest), with a concrete counterexample for κ=1, k=2. It had documented an adopted CWSS-native repair using a tensor carrier reconstructed from the yᵢ, a post-yᵢ scalar challenge ρ, a degree-two relocation sumcheck, and reuse of the existing Eq. (27) element p, preserving the paper's boundary communication of (k−1) extension-field elements plus one ring element. This also included a correction for §4.5's derivation of the omitted partial, and a summary of formalization impact affecting Recursion/PartialEval.lean, ZBatchBridge, the terminal relation, and the composition file.
• HACHI_RING_SWITCHING_COMPARISON.md: This document was deleted from the repository. It contained a lengthy architectural justification explaining why the ring-switching protocol used in Hachi's system is a fundamentally different protocol from the one formalized in the ProofSystem/RingSwitching/ module (which follows DP24/Binius), despite sharing the same packing algebra. The document cataloged three distinct meanings of "ring switching" (small-to-large interactive packing vs. Hachi's two deterministic switches), detailed why Hachi's subfield-valued evaluation points eliminate the need for DP24's batching challenge and dedicated packing sumcheck, compared the two protocols' transcripts and soundness costs, and described updates to the repository's folder structure—including the addition of ProofSystem/RingSwitching/Lift/ as a generic Hachi-style abstraction separate from Packing/. It also identified specific shared layers (round-shape verifiers, embed-and-evaluate algebra) and noted two negative results that prevented merging the two data layers under a common parent structure.
• HACHI_RING_SWITCHING_PLAN.md: The file HACHI_RING_SWITCHING_PLAN.md, a comprehensive 814-line formalization plan for Hachi's ring switching and sumcheck components (Phases A–H), was deleted. This plan detailed the strategy for proving coordinate-wise special soundness, proposed module splits, and tracked sorries and dependencies. Its removal indicates that the plan is no longer current — the formalization work it outlined may have been completed or superseded.
• HACHI_SUMCHECK_TRACK_PLAN.md: The file HACHI_SUMCHECK_TRACK_PLAN.md was deleted. This document contained a 748‑line sequential implementation plan (with milestones B4, F2, F3, F4) for the sumcheck track of the Hachi project, including: guarded CWSS composition (Guarded.lean, GCWSSPackage, infix ▷ᵍ), the Eq. (20) → R^lin adapter (LinSumcheck/Escape.lean, Rlin.lean, evalRlinChain), the quotient‑lift algebra (QuotientLift.lean, theorems exists_quotient_witness_of_quotient_eq, lift_eq_of_eval_eq_at_distinct, Rq.dot_eq_iff_exists_quotient), and the HMZ25 lift (ScalarRound.lean, Lift.lean, lift_coordinateWiseSpecialSound, evalLiftChain). It also specified global design decisions (escape threading via ⊕, guard predicates, field abstraction) and included concrete proof plans, file structure, and timeline estimates. Removing this file eliminates the detailed roadmap and design rationale for these four milestones from the repository.
• blueprint/src/references.bib: Added two new BibTeX entries to the bibliography: HMZ25 (Huang, Mao, Zhang, “Sublinear Proofs over Polynomial Rings,” Cryptology ePrint Archive, 2025) and NOZ26 (Nguyen, O’Rourke, Zhang, “Hachi: Efficient Lattice-Based Multilinear Polynomial Commitments over Extension Fields,” Cryptology ePrint Archive, 2026). These references are now available for citation in the blueprint.
• docs/kb/papers/HMZ25.md: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The new documentation fi...sorry-level skeleton.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• docs/kb/papers/NOZ26.md: Two references to the Hachi gadget file were updated from Gadget.lean to Gadget/Core.lean in the related_modules frontmatter and the Ring-switching layer section. This reflects a reorganization of the ArkLib library where the gadget matrix and gadgetDecompose definitions have been moved into a new subdirectory.
• docs/kb/papers/NS24.md: Updated the related_modules list to reflect the renaming of the Gadget.lean file to Gadget/Core.lean within the Arklib/Commitments/Functional/Hachi/ directory. This ensures the documentation accurately references the current module structure.
• docs/kb/sources/HMZ25/metadata.yml: Added a new metadata file for the HMZ25 source (ePrint 2025/199), recording its bibkey, canonical URL, and a note explaining that the paper's sublinear proofs for Ring-R1CS over Z_Q[X]/(X^N+1) are used in ArkLib's ring-switching lift, as adopted by Hachi (NOZ26, Figure 4 / Lemma 9). This establishes a documentation link between the paper and the project's implementation commitments.
• docs/skills/make-pr-ready.md: The PR readiness checklist in docs/skills/make-pr-ready.md gains four new instructions: a step to detect and strip stray planning/scratch .md files (e.g. PLAN.md, scratch/*.md) from the PR, a warning against piping validate.sh (recommends redirecting to a log file instead), an explanation of the kb/lint.py severity split (missing bibkey is an Error, missing paper page is a Warning) with a fix using scaffold_paper.py, and a note that kb failures may be pre-existing on main but should still be fixed to unblock CI. These additions fill gaps in the existing workflow guidance.
• docs/wiki/repo-map.md: The docs/wiki/repo-map.md documentation was updated to reflect a structural reorganization of the Hachi commitment-scheme modules. Key changes include: renaming umbrella re-export files from ModuleName.lean to ModuleName/Basic.lean (e.g., Gadget.lean became Gadget/Basic.lean, InnerOuter.lean became InnerOuter/Basic.lean, etc.); clarifying that each subfolder carries its umbrella as Basic.lean inside that subfolder; refining the description of QuadEval/Reduction to note the addition of plain relOut, plain relIn, and a parallel QuadEvalSISBreak escape set (key-tied and validated by quadEvalSISSet); updating the §4.3 skeleton description to mention that files export EscapeCWSSPackage/EscapeGCWSSPackage with plain public relations and a parallel escape set; and expanding the Composition.lean section to describe that openCore now chains the plain relation flow and parallel escape flow through the pure §4.3 links. These changes matter because they keep the repository map accurate after the actual code’s structural reorganization, ensuring reviewers and developers have correct file paths and module descriptions.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): ArkLib/Commitments/Functional/Hachi/Gadget.lean

---

Last updated: 2026-07-24 13:46 UTC.

[github-actions]

Build Timing Report

• Commit: 74feb76
• Message: refactor(Hachi/CWSS): cwss packages with escape
• Ref: tr/cwss-packages-with-escape
• Comparison baseline: 679546f from the previous successful PR update.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	1441.04	948.37	-492.67	ok
Warm rebuild	2.63	1.95	-0.68	ok
Validation wrapper	2.78	2.31	-0.47	ok

Incremental Rebuild Signal

• Warm rebuild saved 946.42s vs clean (486.34x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
44.00	70.00	-26.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
43.00	67.00	-24.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
42.00	67.00	-25.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
42.00	66.00	-24.00	ArkLib/ProofSystem/Stir/Combine.lean
36.00	51.00	-15.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
35.00	56.00	-21.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
33.00	59.00	-26.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
32.00	57.00	-25.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
30.00	30.00	+0.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
29.00	31.00	-2.00	ArkLib/OracleReduction/Security/RoundByRound.lean
27.00	42.00	-15.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
24.00	45.00	-21.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
23.00	27.00	-4.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
21.00	35.00	-14.00	ArkLib/Commitments/Functional/KZG/Binding.lean
19.00	28.00	-9.00	ArkLib/ToCompPoly/Univariate/Basic.lean
19.00	30.00	-11.00	ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
18.00	32.00	-14.00	ArkLib/Commitments/Functional/KZG/FunctionBinding/EvaluationBindingConflict.lean
17.00	26.00	-9.00	ArkLib/Data/Polynomial/Indicator.lean
17.00	31.00	-14.00	ArkLib/Data/Polynomial/FoldingPolynomial.lean
16.00	19.00	-3.00	ArkLib/Commitments/Functional/KZG/FunctionBinding/DegreeConflict.lean

[alexanderlhicks]

🤖 AI-generated review (Claude Code). These comments were produced by an AI assistant reviewing this PR against the Hachi paper (NOZ26, ePrint 2026/156) and ArkLib conventions; claims were spot-checked in a built worktree but please verify before acting.

Additional notes (lines outside the diff hunks)

• ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean:95 — [documented deviation · no action required] For the record (already noted in the docstrings): quadEvalBetaSq is a squared-ℓ₂ over-approximation with dimensional factors, not the paper's β̄ = 2b^k (Lemma 8). This is the same quadEvalBetaSq/VerifiedOpening vs (2b^k, 2ω, b) parameter bridge owed since #626 — worth tracking as the parameter-instantiation task so the escape norm bounds eventually reconcile to the paper's constants.

[github-actions]

🤖 PR Summary

sorry delta: -1 (1 removed) — net proof progress

Generated — expertly summarize remaining output above

---

Statistics

Metric	Count
📝 Files Changed	49
✅ Lines Added	1895
❌ Lines Removed	5175

---

Lean Declarations

✏️ Removed: 25 declaration(s)

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/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/QuadEval/Soundness.lean (1)

• theorem buildWitness_mem_relIn (hq5 : q % 8 = 5) {b ω γ : ℕ} (hκ : (2 * ω) ^ 2 < q)

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

• theorem mem_relPartialEvalE_of_relHatEvalE (zpow : Fin (2 ^ κ) → F)

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

• theorem mem_relOutE_of_relRlinE (base : ZMod q) (ω γ : ℕ) (esc : Set E)

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

• theorem mem_relZeroCheckE_of_roundRelE

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

• theorem mem_relLiftE_of_relBatchedE

✏️ Added: 44 declaration(s)

ArkLib/Commitments/Functional/Hachi/Gadget/Core.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/QuadEval/Reduction.lean (3)

• abbrev QuadEvalWitness (Φ : CyclotomicModulus R)
• def quadEvalSISSet
• def self

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

• noncomputable def buildWitnessWithEscape {E : Type} {ω γ : ℕ} (base : ZMod q)
• theorem buildWitnessWithEscape_mem (hq5 : q % 8 = 5) {E : Type} {b ω γ : ℕ}
• theorem buildWitness_mem_relIn_withEscape (hq5 : q % 8 = 5) {b ω γ : ℕ}

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

• theorem mem_relPartialEval_of_relHatEval (zpow : Fin (2 ^ κ) → F)

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

• theorem mem_relOut_of_relRlin

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

• theorem mem_relZeroCheck_of_roundRel

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

• theorem roundsChain_escIn (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
• theorem roundsChain_escOut (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))

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

• theorem mem_relLift_of_relBatched

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

• def CWSSPackage.appendEscape {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def CWSSPackage.appendEscapeGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def CWSSPackage.withEscape {E StmtIn WitIn StmtOut WitOut : Type}
• def EscapeCWSSPackage.appendEscapeGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeCWSSPackage.appendGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeCWSSPackage.appendPure {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeGCWSSPackage.appendEscape {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeGCWSSPackage.appendGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def EscapeGCWSSPackage.appendPure {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def GCWSSPackage.appendEscape {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def GCWSSPackage.appendEscapeGuarded {E StmtA WitA StmtB WitB StmtC WitC : Type}
• def GCWSSPackage.withEscape {E StmtIn WitIn StmtOut WitOut : Type}
• def _root_.CoordinateWise.EscapeCWSSPackage.toGuarded
• def append {E StmtA WitA StmtB WitB StmtC WitC : Type}
• private def packageKindOf (e : Expr) : TermElabM Name
• private def univAppendFn : Name → Name → Option Name
• theorem coordinateWiseSpecialSound.withEscape {E : Type} (esc : Set E)
• theorem treeSpecialSound.withEscape {E : Type} (esc : Set E)

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

• def CWSSPackage.appendGuarded {StmtA WitA StmtB WitB StmtC WitC : Type}
• def GCWSSPackage.appendPure {StmtA WitA StmtB WitB StmtC WitC : Type}

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

• def relPolyEval in ArkLib/Commitments/Functional/Hachi/QuadEval/Bridge.lean moved from L169 to L167
• theorem mem_relPolyEval_of_relIn in ArkLib/Commitments/Functional/Hachi/QuadEval/Bridge.lean moved from L186 to L183
• def paperRelOut in ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean moved from L277 to L349
• def relIn in ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean moved from L323 to L395
• def relOut in ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean moved from L211 to L281
• theorem paperRelOut_subset_relOut in ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean moved from L306 to L380
• def quadEvalPackage {ι : Type} {oSpec : OracleSpec ι} {σ E : Type} in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L493 to L590
• theorem quadEval_coordinateWiseSpecialSound {ι : Type} {oSpec : OracleSpec ι} {σ E : Type} in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L444 to L531
• theorem quadEval_coordinateWiseSpecialSound_paperParams in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L471 to L566
• def rlinStmt in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L95 to L98

---

sorry Tracking

✅ Removed: 1 `sorry`(s)

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

• theorem quadEval_coordinateWiseSpecialSound_withEscape (L147)

---

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 (+0/-1079)

* 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: Summary unavailable — AI generation failed.
• ArkLib/Commitments/Functional/Hachi.lean: The diff updates the module-level documentation in Hachi.lean to reflect the current folder structure of the Hachi commitment scheme. Key changes: the umbrella re-export file is now Basic.lean inside each subfolder (not a standalone file); the Gadget/ subfolder’s core module is renamed from Basic to Core; three new subprotocol stage folders (RingSwitch/, ZeroCheck/, Sumcheck/) and a Recursion/ adapter folder are added to the structure listing; the description of Composition.lean is revised to note that it now hosts the evalChain composition followed by the opening subprotocols, with packages exposing a plain relIn/relOut flow alongside a parallel escape set; and the Commitment.lean note is retained but rephrased.
• ArkLib/Commitments/Functional/Hachi/Commitment.lean: The import statement in ArkLib/Commitments/Functional/Hachi/Commitment.lean was updated from ArkLib.Commitments.Functional.Hachi.QuadEval to ArkLib.Commitments.Functional.Hachi.QuadEval.Basic. This change reflects a refactoring of the QuadEval module, likely splitting it into multiple submodules, and ensures the file imports the correct entry point.
• ArkLib/Commitments/Functional/Hachi/Composition.lean: This diff transitions ArkLib/Commitments/Functional/Hachi/Composition.lean from a "pure + guarded" package composition (using CWSSPackage, GCWSSPackage, and separate ▷/▷ᵍ operators) to an escape-aware universal composition framework based on EscapeCWSSPackage and EscapeGCWSSPackage, with a single universal ▷ operator that auto-lifts pure packages into the escape-guarded world. The evalChain definition and its eval_coordinateWiseSpecialSound theorem were augmented with a new esc : Set E argument, a pp : Hachi.PublicParamsD parameter, and a Q : QuadEvalEscapeMap argument; the theorem's conclusion now wraps the endpoint relations with Set.withEscape calls. openCore was changed from returning a CWSSPackage to an EscapeCWSSPackage, dropping the ⊕ E witness sum type in favor of pure witness types, and its internal composition chain updated to use evalChain (which now accepts pp, Q, and esc) and to thread esc through all sub-protocol packages. openingChain similarly changed from GCWSSPackage to EscapeGCWSSPackage, removed the ⊕ E witness sum type, and replaced the explicit .toGuarded.append/▷ᵍ composition with a mix of appendEscapeGuarded (for the head seam) and the universal ▷ for the remaining pure and guarded factors. The hachi_iteration_coordinateWiseSpecialSound theorem signature gained the new pp, Q, and esc parameters, and its conclusion now widens the endpoint relations with Set.withEscape and nested (esc ∪ K.esc) ∪ Q.localEsc budgets. The module docstring was extensively rewritten to describe the new escape-aware package types, the universal append, the parallel ordinary/escape seams, and updated chain tables and references; the old evalChainE and relPolyEvalE/relInE escape-apostrophe naming convention was removed in favor of Set.withEscape-based widening.
• ArkLib/Commitments/Functional/Hachi/Escape.lean: The diff deletes the entire file ArkLib/Commitments/Functional/Hachi/Escape.lean, which defined an "escape-threaded" front for the Hachi polynomial commitment scheme. The file contained the widened relations relPolyEvalE, relInE, relOutE (parameterized by an escape set esc : Set E), the sorry-free escape-threaded polynomial-level bridge bridgePackageE with its pull-back theorem mem_relPolyEvalE_of_relInE, the sorried theorem quadEval_coordinateWiseSpecialSound_withEscape (a widened version of Lemma 8), the escape-threaded package quadEvalPackageE, and the composed evalChainE which was the drop-in replacement of the evalChain front. The theorem quadEval_coordinateWiseSpecialSound_withEscape is explicitly marked as sorry.
• ArkLib/Commitments/Functional/Hachi/Gadget.lean: The file ArkLib/Commitments/Functional/Hachi/Gadget.lean was deleted. This umbrella module previously re-exported ArkLib.Commitments.Functional.Hachi.Gadget.Basic and ArkLib.Commitments.Functional.Hachi.Gadget.Norms, and contained top-level documentation for the Ajtai gadget matrix and its role in the Hachi/Greyhound commitment scheme. Its removal likely indicates that the re-exports and documentation have been moved or are no longer needed, so any imports relying on this file must be updated to import the submodules directly.
• ArkLib/Commitments/Functional/Hachi/Gadget/Basic.lean: This file was restructured from a standalone module into an umbrella module that re-exports the core gadget algebra from Gadget/Core.lean and the norm analysis from Gadget/Norms.lean. All previous inline definitions and theorems (gadgetEntry, gadgetMatrix, gadgetMul, IsLawfulGadgetDecomposition, DigitDecomposition, zmodDigitDecomposition, gadgetDecompose, gadgetDecompose_apply, gadgetDecompose_lawful, and the private ofDigits_eq_sum_range lemmas) were removed from this file; they now live in the two new submodules. The module-level docstring was rewritten to describe the folder structure and to frame the gadget as the shortness workhorse of the Greyhound/Hachi inner-outer commitment, replacing the old -- Main definitions and -- Main results lists.
• ArkLib/Commitments/Functional/Hachi/Gadget/Core.lean: This new file introduces the core definitions and theorems for the Ajtai gadget matrix over the cyclotomic ring Rq Φ, used in the Hachi commitment scheme. It defines the abstract DigitDecomposition structure (with reconstruction law) and a concrete zmodDigitDecomposition over ZMod q. It defines gadgetEntry, gadgetMatrix, gadgetMul, and IsLawfulGadgetDecomposition, proves the explicit formulas gadgetEntry_finProdFinEquiv and gadgetMul_apply, and provides the gadget inverse gadgetDecompose together with the lawfulness theorem gadgetDecompose_lawful. Two private lemmas rewrite Nat.ofDigits as a finite sum over a range. No sorry or admit appear in the file.
• ArkLib/Commitments/Functional/Hachi/Gadget/Norms.lean: The import statement in Norms.lean was changed from ArkLib.Commitments.Functional.Hachi.Gadget.Basic to ArkLib.Commitments.Functional.Hachi.Gadget.Core. This updates the file to depend on the refactored core module, which likely contains the definitions that Norms.lean relies on. No other changes, such as new theorems, definitions, or sorry/admit, were introduced.
• ArkLib/Commitments/Functional/Hachi/InnerOuter/Basic.lean: Summary unavailable — AI generation failed.
• ArkLib/Commitments/Functional/Hachi/InnerOuter/Scheme.lean: The diff updates the import statement in ArkLib/Commitments/Functional/Hachi/InnerOuter/Scheme.lean to use ArkLib.Commitments.Functional.Hachi.Gadget.Core instead of ArkLib.Commitments.Functional.Hachi.Gadget.Basic. This reflects a restructuring of the Hachi gadget module, likely to split a larger Basic file into a more focused Core file. No other changes are made; no sorry or admit are introduced.
• ArkLib/Commitments/Functional/Hachi/QuadEval/Basic.lean: This commit moves ArkLib/Commitments/Functional/Hachi/QuadEval.lean into a new subdirectory as ArkLib/Commitments/Functional/Hachi/QuadEval/Basic.lean, updating the module head docstring to reflect its new role as umbrella module for the QuadEval/ folder. The docstring is also revised to clarify that the ordinary relations relIn and relOut are defined over the fixed commitment key pp, and that the parallel QuadEvalSISBreak escape set (validated by quadEvalSISSet) uses the same pp as a parameter, not as statement data. These changes improve the organization and documentation accuracy of the Hachi polynomial-evaluation reduction.
• ArkLib/Commitments/Functional/Hachi/QuadEval/Bridge.lean: The file refactors PolyEvalStatement to remove the pp field (public parameters are now a relation parameter, not statement data), and simplifies relPolyEval by dropping the two MSIS disjuncts, leaving only the VerifiedOpening condition with polynomial evaluation. Correspondingly, toQuadEvalStatement no longer copies pp, and mem_relPolyEval_of_relIn is rewritten to handle only the opening case rather than case‑splitting on the witness. The bridgePackage is changed from CWSSPackage to EscapeCWSSPackage (import updated to CoordinateWiseSpecialSoundness.Escape), adding an escape set esc : Set E and the fields escIn, escOut, escape_mono; isCWSS now uses .withEscape esc. All affected definitions and theorems (relPolyEval, relIn, bridge_coordinateWiseSpecialSound, bridgePackage) gain an explicit pp parameter.
• ArkLib/Commitments/Functional/Hachi/QuadEval/Gadgets.lean: The diff updates a documentation comment in Gadgets.lean to reflect the correct module path for the gadget matrix definition: the text previously referencing Gadget/Basic.lean now points to Gadget/Core.lean. This corrects the file path mentioned in the documentation, ensuring that readers are directed to the appropriate source for the G matrix definitions and related concepts.
• ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean: The QuadEvalStatement structure removed its pp (public parameters) field, making the commitment key a fixed parameter of the reduction rather than statement data; correspondingly, relOut, paperRelOut, relIn, and paperRelOut_subset_relOut now take pp explicitly. QuadEvalWitness was redefined from an inductive type (three cases: opening, msisB, msisD) to an abbreviation for Opening only, while the Module-SIS escape cases were moved to a new QuadEvalSISBreak inductive type with two constructors (msisB, msisD). A new quadEvalSISSet definition and QuadEvalEscapeMap structure (with self instance) were added to model the statement-independent set of valid Module-SIS escapes relative to the fixed key, enabling parallel escape accumulation without altering the core relIn/relOut relations. relIn now checks only a VerifiedOpening and evalConsistency for u, omitting the former Module-SIS disjuncts. The documentation was updated throughout to reflect that the commitment key is never statement-carried.
• ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean: This file changes Hachi's QuadEval soundness from a plain CWSS package into an escape-aware EscapeCWSSPackage, allowing local Module-SIS breaks (cases A/B) to be propagated alongside the ordinary weak-opening case (case C). The change adds buildWitnessWithEscape and its correctness theorem buildWitnessWithEscape_mem, which lift the local three-case extractor into a common ambient escape type E via a QuadEvalEscapeMap. The return type of buildWitness is changed from QuadEvalWitness to QuadEvalWitness ⊕ QuadEvalSISBreak (the inr cases now carry the fixed-key SIS breaks). The old theorem buildWitness_mem_relIn is replaced by buildWitness_mem_relIn_withEscape, which returns membership in relIn.withEscape (quadEvalSISSet ...). The main theorem quadEval_coordinateWiseSpecialSound now takes an escape set esc and an escape map Q, and the final package quadEvalPackage becomes an EscapeCWSSPackage with fields escIn, escOut, and escape_mono. All relOut and relIn references in the diff now also take an explicit pp parameter (the Hachi public key) rather than using stmt.pp. The docstrings are updated throughout to reflect the new escape semantics and the revised lemma names.
• ArkLib/Commitments/Functional/Hachi/Recursion/Basic.lean: Added a new umbrella module file ArkLib/Commitments/Functional/Hachi/Recursion/Basic.lean that documents the folder structure of the Hachi recursion adapters and re-exports the TraceHandoff module (which transitively imports ZBatchBridge and PartialEval). No theorems, definitions, or sorry/admit are present; the file is purely documentation and re-export.
• ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean: Modified relPartialEvalE to accept an explicit esc : Set E parameter instead of hardcoding K.esc, and updated its body to use esc in the call to .withEscape. Added the same esc parameter to partialEval_coordinateWiseSpecialSound, updated its premises to use relWEvalClaimE and relPartialEvalE with that esc, and adjusted its proof target to match. Replaced CWSSPackage in partialEvalPackage with EscapeCWSSPackage carrying E as the escape type, changed relIn/relOut from the escape-threaded relations relWEvalClaimE/relPartialEvalE to the plain relations relWEvalClaim/relPartialEval, added fields escIn := esc, escOut := esc, and escape_mono := fun _ h => h, and updated the isCWSS field to pass esc to the soundness theorem. The partialEval_coordinateWiseSpecialSound proof is entirely sorry.
• ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean: The pp' parameter was removed from toNextQuadEvalStatement, handoffVerifier, handoffVerifier_isGuarded, and handoffProver; the documentation now states that pp' is not statement data and enters only through the next iteration's relations. An explicit escape set esc was added to handoff_coordinateWiseSpecialSound and handoffPackage, with the relations changed from relHatEvalE/relInE to (relHatEval ...).withEscape esc/(relIn ...).withEscape esc, and the package type refactored from GCWSSPackage to EscapeGCWSSPackage carrying esc independently via escIn/escOut and adding an escape_mono field; handoffPackage's witness types were simplified accordingly. handoffVerifier_isGuarded now provides explicit implicit arguments for type parameters, and documentation comments across the file were updated to reflect the escape-aware design (e.g., relHatEvalE → relHatEval).
• ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean: The module docstring corrects two relation names — relPartialEvalE → relPartialEval and relHatEvalE → relHatEval — and updates the corresponding reference to the sorried pull-back theorem, renaming it from mem_relPartialEvalE_of_relHatEvalE to mem_relPartialEval_of_relHatEval and noting its expected unprovability. The theorem mem_relPartialEval_of_relHatEval itself is changed: its witness argument w changes from LiftedWitness Φ μ n ⊕ E to LiftedWitness Φ μ n, and its hypothesis accordingly uses relHatEval (without the E suffix) instead of relHatEvalE, while the conclusion targets relPartialEval (without the E suffix). The zBatchPackage definition is refactored from a CWSSPackage to an EscapeCWSSPackage — it now accepts an extra esc : Set E parameter and passes escIn := esc, escOut := esc, and escape_mono := fun _ h => h — and all internal relation references are updated to the non-E-suffixed versions except in the isCWSS proof, where the E-suffixed relations (relPartialEvalE, relHatEvalE) are used with the explicit escape set. The body of zBatchPackage's isCWSS argument now cases on the witness to call either the renamed mem_relPartialEval_of_relHatEval theorem (for inl w) or directly h (for inr e). The module-level comment about mem_relPartialEvalE_of_relHatEvalE being sorried is updated to reflect the new theorem name; the mem_relPartialEval_of_relHatEval theorem remains sorried.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Basic.lean: The file ArkLib/Commitments/Functional/Hachi/RingSwitch.lean was renamed to ArkLib/Commitments/Functional/Hachi/RingSwitch/Basic.lean, and its module documentation was updated. The umbrella description now clarifies that it re-exports the folder (with Reduction transitively importing Rlin), and that the plain output relation relLift (formerly relLiftE) is the input of the batching bridge in ZeroCheck/. The documentation for Rlin.lean was revised to state that it reinterprets QuadEval's Eq. (20) output relOut (instead of relOutE of Escape.lean) as relRlin (instead of relRlinE), and that the package carries the parallel escape set unchanged. The sorried block-matrix assembly/unstacking and block-row equivalence pull-back are noted as the remaining gaps. The Reduction.lean description remains consistent: it establishes the LiftCom commitment, relLift, and the sorried lift_coordinateWiseSpecialSound for k = 2d.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean: Summary unavailable — AI generation failed after retries.
• ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean: The file was refactored from a CWSSPackage to an EscapeCWSSPackage, decoupling the escape set from the relations: rlinPackage now declares relIn := relOut (plain) and relOut := relRlin (plain) with separate escIn/escOut fields, and the theorem mem_relOutE_of_relRlinE was renamed to mem_relOut_of_relRlin with its signature simplified to operate on plain relations (removing the esc parameter and changing the witness type from PolyVec … ⊕ E to PolyVec …). rlinStmt gained a pp parameter of type Hachi.PublicParamsD … to receive public parameters directly. The imports were updated to include QuadEval.Reduction, ReduceClaim, and the two CoordinateWiseSpecialSoundness.Escape/NoChallenge modules. The sorried theorem mem_relOut_of_relRlin remains, now with its new signature.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/Basic.lean: Summary unavailable — AI generation failed.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/Bridge.lean: Renamed mem_relZeroCheckE_of_roundRelE to mem_relZeroCheck_of_roundRel, simplifying its witness type from LiftedWitness Φ μ n ⊕ E to LiftedWitness Φ μ n and its conclusion from relZeroCheckE to relZeroCheck (the proof remains sorried). Refactored sumcheckBridgePackage from a CWSSPackage into an EscapeCWSSPackage parameterized by an escape set esc : Set E; the relIn now uses relZeroCheck (with withEscape esc) and relOut uses roundRelE with the escape set, witnesses are no longer the sum type ⊕ E, and the soundness argument handles both inl and inr cases (the mem_relZeroCheck_of_roundRel theorem and the inr path via the escape condition). The module docstring similarly updates relIn and relOut to drop the E suffix.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean: This diff modifies ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean to add an explicit esc : Set E parameter to relWEvalClaimE, finalEval_coordinateWiseSpecialSound, and finalEvalPackage, replacing the previously hard-coded K.esc usage and changing the latter's return type from GCWSSPackage to EscapeGCWSSPackage. Accordingly, finalEvalPackage now includes separate escIn, escOut, and escape_mono fields, and uses roundRel and relWEvalClaim (without the E suffix) for its relIn and relOut respectively. The theorem finalEval_coordinateWiseSpecialSound is still admitted via sorry.
• ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean: The file refactors the round package and chain from GCWSSPackage to EscapeGCWSSPackage, adding an esc : Set E parameter to round_coordinateWiseSpecialSound, roundPackage, roundsChainAux, roundsChain, and the associated theorems, which now carry escape set invariants (escIn/escOut). Two new theorems roundsChain_escIn and roundsChain_escOut expose the invariant that the escape set is preserved through the composition. The relIn and relOut fields of roundPackage and the chain definitions changed from roundRelE to roundRel, while the base case of the recursion uses EscapeCWSSPackage.toGuarded and the recursive append call passes the escape set proofs. Documentation comments are updated to reflect the new type and to correct a reference from Sumcheck.lean to Sumcheck/Basic.lean. The sorry in round_coordinateWiseSpecialSound remains but its signature now includes the esc parameter.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Basic.lean: This diff renames ArkLib/Commitments/Functional/Hachi/ZeroCheck.lean to ArkLib/Commitments/Functional/Hachi/ZeroCheck/Basic.lean (now the umbrella module for the ZeroCheck/ subfolder) and updates its docstring to mark the file as an umbrella that re-exports Reduction (which transitively imports Batch and Constraints). It also corrects the docstring's mention of the output relation from relZeroCheckE to relZeroCheck, noting that this plain relation feeds the sumcheck bridge in Sumcheck/, with composition handled in Composition.lean.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Batch.lean: this diff performs two main groups of changes. first, the module-level docstring is updated to rename relIn and relOut from relLiftE/relBatchedE to relLift/relBatched, and the extraction-direction theorem is renamed from mem_relLiftE_of_relBatchedE to mem_relLift_of_relBatched. second, the signature and implementation of several declarations are simplified by removing the E escape-wrapper from the base relations in batchPackage: relIn becomes relLift (no ⊕ E on the witness), relOut becomes relBatched (no ⊕ E), and the theorem mem_relLiftE_of_relBatchedE is replaced by mem_relLift_of_relBatched which drops the ⊕ E witness option and works directly with relBatched and relLift. accordingly batchPackage changes from a CWSSPackage to an EscapeCWSSPackage, gaining escIn/escOut fields set to a fresh esc : Set E parameter, an escape_mono field, and the witness handling in isCWSS is split into cases (inl w / inr e) so the LiftedWitness case uses the renamed pull-back theorem while an escape e is passed through via h. the redefined relBatchedE now takes esc as an explicit parameter and uses (relBatched …).withEscape esc. the single sorry in the file persists unchanged under the new name mem_relLift_of_relBatched.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean: The diff makes two changes in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Constraints.lean. First, the docstring of hAlpha_degreeOf_le updates a cross-reference from Sumcheck.lean to Sumcheck/Basic.lean. Second, roundRelE gains an explicit esc : Set E parameter (replacing the previous use of K.esc) and its definition now passes esc to .withEscape instead of K.esc, making the escape set an explicit argument rather than pulling it from the LiftCom structure K.
• ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean: The relZeroCheckE definition now takes an explicit (esc : Set E) argument and uses it directly to compute the escape-threaded relation, instead of implicitly using K.esc. The zeroCheck_coordinateWiseSpecialSound theorem signature gained the same esc parameter, and its statement now relates relBatchedE and relZeroCheckE with the explicit escape set; its proof remains sorry. The zeroCheckPackage definition was refactored: its return type changed from CWSSPackage to EscapeCWSSPackage, and its fields now use plain relBatched and relZeroCheck (without the E suffix) together with explicit escIn/escOut fields set to esc and an escape_mono proof fun _ h => h; the isCWSS field was updated accordingly to pass the esc argument. The docstring was also updated to reflect that the package now carries esc unchanged.
• ArkLib/Commitments/Functional/Hachi/hachi-overview.html: The Hachi overview HTML was updated to reflect a project-wide refactor: the guarded verifier composition operator changed from ▷ᵍ to ▷ₑᵍ; the escape-threading description now says “a parallel escape seam carried per-package via EscapeCWSSPackage” instead of “threaded by Escape.lean”; all relation names lost their E suffix (e.g., relPolyEvalE→relPolyEval, relInE→relIn, roundRelE→roundRel, relWEvalE→relWEvalClaim), and the escape threading sub‑cross changed status from wip (1 sorry) to proven (0 sorries) with a description mentioning the parallel seam. The file index was restructured: umbrella entries (e.g., Gadget.lean, QuadEval.lean, RingSwitch.lean, ZeroCheck.lean, Sumcheck.lean) were replaced by Basic.lean files under their respective subdirectories, and a new Recursion/ subdirectory was added with entries for Basic.lean, PartialEval.lean, ZBatchBridge.lean, and TraceHandoff.lean (all marked wip or gap).
• ArkLib/Data/Lattices/CyclotomicRing/Rq.lean: The docstring comment block for the natDegree_val_toPoly_lt theorem has been updated to correct the module path of the inner-outer gadget commitment from ArkLib/Commitments/Functional/Hachi/Gadget.lean to the more specific ArkLib/Commitments/Functional/Hachi/Gadget/Core.lean, ensuring the cross-reference accurately reflects the current file structure.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Escape.lean: The file was substantially rewritten (module docstring, new theorems, definitions, and instances, plus a universal append macro). The module-level docstring was replaced: it now describes Set.withEscape as the technical primitive for escape threading, introduces the EscapeCWSSPackage structure (which keeps escapes separate from ordinary relations), and discusses the 2×2 package lattice (escape? × guarded?) and the universal ▷ elaborator. The existing Set.withEscape and mem_withEscape_inl definitions were retained but supplemented: mem_withEscape_inr and Nonempty (W ⊕ E) instance were added, and the docstring was expanded with an architectural overview and references. The theorems treeSpecialSound.withEscape and coordinateWiseSpecialSound.withEscape were added, which transport special-soundness certificates across the escape widening. The structures EscapeCWSSPackage and EscapeGCWSSPackage (and their append compositions) were introduced, together with lifting definitions CWSSPackage.withEscape, GCWSSPackage.withEscape, EscapeCWSSPackage.toGuarded, and a series of mixed-append helpers (CWSSPackage.appendEscape, EscapeCWSSPackage.appendPure, etc.). Finally, a scoped elaborator ▷ was defined that dispatches append by the package kinds of its arguments (using a 16-entry dispatch table), and the scoped infix synonyms ▷ₑ, ▷ₑᵍ were also provided. None of the declarations are left as sorry or admit. No code was removed.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean: The diff modifies Guarded.lean to introduce two mixed-composition definitions (CWSSPackage.appendGuarded and GCWSSPackage.appendPure) that lift either a pure left or pure right CWSSPackage into the guarded world via CWSSPackage.toGuarded before delegating to GCWSSPackage.append. The docstring for GCWSSPackage is updated to reflect that its append operation is now the primary infix ▷ (with ▷ᵍ as an explicit synonym) and that its composition is extended to cover mixed pure/guarded pairs through overloads defined in this file and in Escape.lean. The module-level header comment is also revised to replace the earlier ▷ᵍ notation references with the new ▷ primary notation and to clarify that the guarded loop is built by recursion over binary guarded append rather than the specific ▷ᵍ infix.
• ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Package.lean: The diff removes the scoped infix operator ▷ for CWSSPackage.append and updates the module-level docstring to explain that the ▷ operator is now defined universally in Escape.lean, dispatching over all four package kinds (pure, guarded, escape-aware, or both). No new theorems, definitions, or sorry/admit are introduced.
• HACHI_GENERIC_RING_SWITCH_PLAN.md: The file HACHI_GENERIC_RING_SWITCH_PLAN.md has been deleted from the repository. This 1079-line document outlined a detailed reconciliation and implementation plan for extending the Generic/ ring-switching layer to support Hachi's §3.1 packing head, covering phases such as adding a deterministic packed-claim stage, lattice glue, unpack algebra, head reduction, guarded composition, and chain assembly. Its removal indicates that the plan is no longer maintained as a separate document, likely because the implementation has been completed or the approach has been superseded.
• HACHI_LEMMA10_GAP.md: The file HACHI_LEMMA10_GAP.md was deleted. It previously contained a detailed analysis of a gap in Lemma 10 of the Hachi protocol (coordinate-wise special soundness of the zero-check challenge round), including a protocol-level counterexample and evaluations of multiple repair approaches (Kronecker-curve challenges, coordinate‑zipped rounds, etc.). Its removal means that the orientation/documentation content it provided is no longer available in the repository; the formalization plan now references other files (e.g., HACHI_RING_SWITCHING_PLAN.md) for the adopted repair.
• HACHI_RECURSION_GAP.md: The file HACHI_RECURSION_GAP.md was deleted. It contained a detailed analysis of an algebraic gap in the partial-evaluation step of the Hachi protocol (NOZ26, ePrint 2026/156) along with an adopted repair involving CWSS relocation. Its removal indicates the underlying issue has been resolved, or the documentation has been integrated elsewhere, making this standalone analysis obsolete.
• HACHI_RING_SWITCHING_COMPARISON.md: The file HACHI_RING_SWITCHING_COMPARISON.md was deleted. This documentation contained a detailed analysis contrasting Hachi's ring-switching protocol (subfield-valued evaluation points, deterministic trace check, separate sumcheck for linear relations and norm bounds) with the formalized ProofSystem/RingSwitching/Packing/ module (interactive batching and sumcheck for claim relocation, round-by-round knowledge soundness). It also catalogued the shared data layers (RingSwitchingProfile, packMLE, Sumcheck/Structured), the separate Lift/ abstraction for Hachi's opposite-direction ring switch, the round-shape verifier skeletons, and the embed-and-evaluate algebra. Removing this file eliminates a comprehensive orientation resource that mapped the taxonomy of the two constructions and their compatibility.
• HACHI_RING_SWITCHING_PLAN.md: The entire HACHI_RING_SWITCHING_PLAN.md file — an 814-line formalization plan covering the Hachi ring-switching (§3) and sumcheck (§4.3) protocols, including the lattice-layer theorems, the generalization of the RingSwitching/ module, the design decisions D1–D12, and the Phases A–H milestones — has been deleted. This removal likely indicates that the plan is no longer active or has been superseded; reviewers should confirm whether the work described (e.g., the Hachi packing scheme, CWSS guarded composition, and the §4.3 sumcheck) is being tracked elsewhere or is out of scope.
• HACHI_SUMCHECK_TRACK_PLAN.md: The file HACHI_SUMCHECK_TRACK_PLAN.md was deleted (removed entirely). It contained a detailed, sequential implementation plan for the first four milestones (B4, F2, F3, F4) of the Hachi sumcheck track, including design decisions, proof sketches, file structures, acceptance criteria, and risk assessments. As a planning document, its removal indicates that the plan is no longer maintained or has been superseded, which matters for reviewers because it removes a source of implementation guidance and design context that was previously considered authoritative for these milestones.
• docs/kb/papers/HMZ25.md: Added docs/kb/papers/HMZ25.md, a new documentation page for the Huang–Mao–Zhang paper on sublinear proofs over polynomial rings. It describes the ring‑switching lift (M z = y over Rq iff M z = y + (X^N+1)·r over Zq[X]) and how Hachi uses it, lists the three related ArkLib Lean modules (Basic, Reduction, Rlin), notes that the formalization follows Hachi’s presentation rather than the original Ring‑R1CS setting, and explicitly states that the interpolation‑based extraction for Hachi’s Lemma 9 (lift_coordinateWiseSpecialSound) is currently a sorry‑level skeleton. This is a new file containing no prior content, so every line is an addition.
• 6 file(s) filtered as noise (lockfiles, generated, or trivial): blueprint/src/references.bib, docs/kb/papers/NOZ26.md, docs/kb/papers/NS24.md, docs/kb/sources/HMZ25/metadata.yml, docs/skills/make-pr-ready.md, docs/wiki/repo-map.md

---

Last updated: 2026-07-26 07:15 UTC.

[alexanderlhicks]

Part of a cross-PR review of #654, #656 and #659 read together (plus the open ring-switching PR #615), in isolated builds, against NOZ26 (ePrint 2026/156, SHA-256 c7c98591…afd5e6a15). Where a finding interacts with a sibling PR I say so explicitly.

#659 — reviewed at 74feb760

The refactor is clean and the fixed-key Module-SIS repair is genuinely sound. Escapes are now
checked against pp.outerMatrix / pp.dMatrix, the actual key from the statement's public
parameters, so a break can no longer be smuggled in by supplying a convenient matrix alongside the
solution. I also went looking for the obvious hole and it isn't there: ModuleSIS.relation is
decide (z ≠ 0) && isShort z && decide (A *ᵥ z = 0), so Definition 1's 0 < ‖z‖∞ really is
enforced.

Several paper checks came out right on independent re-derivation:

• paperRelOut_subset_relOut has the containment in the sound direction — the formalized
  relation is the weaker (larger) one, so soundness against it is at least as strong;
• the ℓ₁ invertibility criterion implies paper Lemma 3's ℓ₂ hypothesis, since ‖·‖₂ ≤ ‖·‖₁. A
  sound generalisation, not a weakening;
• SS(C, 2^r, 2) really does have ℓ(k−1)+1 = 2^r + 1 elements, as Lemma 8 states. (Pleasant
  contrast with Lemma 10, whose transcript count is wrong — see #656.)

The 14 Gadget Basic → Core declarations are body-identical moves, the five umbrella renames are
declaration-free, import integrity holds, and there is no new sorry (changed-file bodies
36 → 35). quadEval_coordinateWiseSpecialSound, paperRelOut_subset_relOut, CWSSPackage.append
and EscapeCWSSPackage.append are all axiom-clean.

Three things I'd like changed:

1. Six deleted design documents with 21 live references left behind, across 10 files. Several are
   load-bearing section pointers — ZeroCheck/Constraints.lean:45,75,188 cite
   HACHI_LEMMA10_GAP.md §3.K / §3.K.2 as the derivation of the Kronecker-seed design the code
   implements. check-docs-integrity.py doesn't see docstring paths, so CI stays green. #654
   performs the identical deletion with zero dangling references — adopt its cleanup on rebase, and
   migrate the surviving gap analyses into docs/kb/audits/ first.
2. docs/skills/make-pr-ready.md tells agents to delete untracked user files after only a
   warning. Out of scope, and hazardous in a tree that routinely carries dozens of untracked planning
   documents. (#656 edits the same file with a genuinely useful canonical-base fix — worth keeping
   theirs and dropping this addition.)
3. QuadEvalEscapeMap has no upper bound on localEsc — and the obvious fix doesn't work,
   because .self sets localEsc := quadEvalSISSet, which is nonempty for every compressing key,
   and nonemptiness alone already collapses the certificate to a constant extractor. Compiled witness
   in that comment. Pre-existing framework behaviour, so not a blocker on its own, but the
   guarded-append and package-lattice claims should be scoped accordingly.

Two smaller items: the generated overview still advertises a superseded shape — "single line of nine
reductions" (:357), "9-link opening chain" (:365), "≈24 open sorries" (:367), and generation "from
the current working tree on the hachi-skeleton branch" (:527) — against an actual 12 rows and 33
executable sorry bodies in the Hachi tree. Those lines fall outside this PR's diff hunks so I
couldn't anchor a comment; either regenerate or drop the numeric claims. And your HMZ25 bib entry is
the correct one of the two competing additions — see that comment, it's a heads-up rather than a
defect.

On #615 (open, head 68e9a752): it overlaps this PR on ArkLib.lean,
blueprint/src/references.bib and docs/wiki/repo-map.md. Worth noting it is not exposed to
item 3: #615 states security as an RBR knowledge-soundness probability bound and never uses
withEscape, so there's no constant-extractor escape hatch there. The fix I suggest above moves
these certificates toward the shape #615 already has.

Ordering: #654 → #659 → #656. Rebasing onto #654 gets you its proof of
ScalarRound.coordinateWiseSpecialSound_of_mkWitness_scalar (currently sorry here), its
HACHI_*.md reference cleanup, and a settled bib — three of the items above largely resolve
themselves that way.

Posted as a comment rather than a formal "request changes" so it doesn't block the queue.