feat(Hachi): make extractors computable

ArkLib.lean

@@ -1,6 +1,6 @@
 import ArkLib.AGM.Basic
 import ArkLib.Commitments.Functional.Basic
-import ArkLib.Commitments.Functional.Hachi
+import ArkLib.Commitments.Functional.Hachi.Basic
 import ArkLib.Commitments.Functional.Hachi.Commitment
 import ArkLib.Commitments.Functional.Hachi.Composition
 import ArkLib.Commitments.Functional.Hachi.EvalSplit
@@ -179,6 +179,7 @@ import ArkLib.Data.Lattices.CyclotomicRing.Galois.FixedSubring
 import ArkLib.Data.Lattices.CyclotomicRing.Galois.Group
 import ArkLib.Data.Lattices.CyclotomicRing.Galois.Order
 import ArkLib.Data.Lattices.CyclotomicRing.Galois.Trace
+import ArkLib.Data.Lattices.CyclotomicRing.Inverse
 import ArkLib.Data.Lattices.CyclotomicRing.NormBounds
 import ArkLib.Data.Lattices.CyclotomicRing.NormBounds.Basic
 import ArkLib.Data.Lattices.CyclotomicRing.NormBounds.LsCore

ArkLib/Commitments/Functional/Hachi.lean → ArkLib/Commitments/Functional/Hachi/Basic.lean

@@ -25,7 +25,8 @@ proofs and the completeness layer — the honest-prover `opening` (`hachi.openin
 ## Folder structure
 
 The folder `Hachi/` is organized by paper section. Each subfolder carries a `Basic.lean`
-umbrella re-export inside the folder (as this file does for the whole Hachi development):
+umbrella re-export inside the folder, and this file is that umbrella for the whole Hachi
+development:
 
 * `Gadget/` (§2.1) — the base-`b` Ajtai gadget matrix `G` and its digit-decomposition inverse
   `G⁻¹` (`Core`), with centered `ℓ∞` / `ℓ₂²` norm bounds for both directions (`Norms`).

ArkLib/Commitments/Functional/Hachi/Composition.lean

@@ -14,28 +14,28 @@ import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Guarded
 /-!
 # Hachi — the CWSS composition home
 
-This is the designated home of the growing n-ary composition of the subprotocols of Hachi [NOZ26],
-a lattice-based multilinear polynomial commitment scheme. Each subprotocol is formalized in its own
+This is the designated home of the growing n-ary composition of the subprotocols of Hachi [NOZ26], a
+lattice-based multilinear polynomial commitment scheme. Each subprotocol is formalized in its own
 file and exported as a CWSS *package* in the weakest of the four kinds it honestly lives in —
-`CWSSPackage`, `GCWSSPackage` (guarded verifier: may `failure` at runtime), `EscapeCWSSPackage`
-(extraction may exhibit a cryptographic escape), `EscapeGCWSSPackage` (both) — bundling the verifier
-with its proof of coordinate-wise special soundness (CWSS), the knowledge-soundness notion under
-which a witness is extracted from a suitably structured tree of accepting transcripts. This file
-only **imports those packages and chains them** with the universal append `▷`, which dispatches on
-the factors' package kinds and lifts each to the join automatically (both lifts are lossless). Only
-the ordinary relation seam has to match — escape events compose without a seam. The guarded
-composition theorem lives in
+`CWSSPackage`, `GCWSSPackage` (guarded verifier: may `failure` at runtime),
+`EscapeCWSSPackage` (extraction may exhibit a cryptographic escape),
+`EscapeGCWSSPackage` (both) — bundling the verifier with its proof of coordinate-wise
+special soundness (CWSS), the knowledge-soundness notion under which a witness is extracted from a
+suitably structured tree of accepting transcripts. This file only **imports those packages and
+chains them** with the universal append `▷`, which dispatches on the factors' package kinds and
+lifts each to the join automatically (both lifts are lossless). Only the ordinary relation seam has
+to match — escape events compose without a seam. The guarded composition theorem lives in
 `OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean`. The composed chain's
 `isCWSS` field is the CWSS certificate for the whole reduction. (Hachi as a `Commitment.Scheme` —
-the honest committer `keygen`/`commit` and the `hachi` functional commitment — lives in the
-sibling `Commitment.lean`.)
+the honest committer `keygen`/`commit` and the `hachi` functional commitment — lives in the sibling
+`Commitment.lean`.)
 
 ## The three layers of this file
 
 1. **`evalChain`** (sorry-free, finished): the polynomial-level bridge ▷ `QuadEval`
    (§4.2 / Figure 3 / Lemma 8) — an escape-aware package whose event is `QuadEval`'s.
 2. **`openCore`** (skeleton, pure links): the escape-aware `evalChain` extended by the
-   §4.3 stages up to the sumcheck bridge — R^lin adapter (F2) ▷ HMZ25 lift (Figure 4 / Lemma 9)
+   §4.3 stages up to the sumcheck bridge — R^lin adapter ▷ HMZ25 lift (Figure 4 / Lemma 9)
    ▷ batching bridge (Eqs. (22)–(23)) ▷ zero-check (Figure 5 / **corrected** Lemma 10) ▷
    sumcheck bridge.
 3. **`openingChain`** (skeleton, guarded tail): the pure `openCore` ▷ the paired sumcheck loop
@@ -82,10 +82,10 @@ match their relation seam.
 
 **Which rows carry an escape event.** Row 2 carries `QuadEval`'s Module-SIS(B/D) break of the fixed
 key (`quadEvalEscLocal`); rows 4, 6 and 8 carry the weak-binding collision of the `w̃`-commitment
-(`LiftCom.Collision`, via `Lift.escEvent` / `zeroCheckEsc` / `roundEsc`). Those four are
+(`LiftCom.Collision`, via `Lift.escEvent` / `nestedZeroCheckEsc` / `roundEsc`). Those four are
 `EscapeCWSSPackage`/`EscapeGCWSSPackage`s; every other row is escape-free
-(`CWSSPackage`/`GCWSSPackage`) and enters the chain at the never-firing event through the universal
-`▷`'s lossless lift.
+(`CWSSPackage`/`GCWSSPackage`) and enters the chain at the never-firing event
+through the universal `▷`'s lossless lift.
 
 - Rows 1–7 have **pure** verifiers: every check constrains either retained statement data or the
   never-sent witness, so it lives in the output relation (the `QuadEval` precedent). Rows 8, 9,
@@ -96,10 +96,14 @@ key (`quadEvalEscLocal`); rows 4, 6 and 8 carry the weak-binding collision of th
 - Row 6 implements the **corrected Lemma 10**: the paper's uniform-vector star extraction is not
   provable (axis-cross counterexample). Each coordinate of `τ₀` and `τα` is instead sampled in a
   separate scalar round, so the accepting transcript tree becomes a path-dependent complete
-  binary evaluation tree — `k = 2` at every round, and the multilinear identity test extraction
-  needs. Since no prover message separates the rounds, the *interactive* protocol is unchanged
-  from Figure 5; what changes is the tree shape the extractor is handed. The counterexample, the
-  repair and their costs are spelled out in `ZeroCheck/Reduction.lean`; the full analysis is
+  binary evaluation tree with `2 ^ (m₀ + m₁)` leaves — `k = 2` at every round, as the multilinear
+  identity test extraction needs. `ChallengeTree.LeafWitnesses` supplies one candidate output
+  witness at every leaf, and the ordinary `nestedZeroCheckExtractor` directly returns the all-left
+  entry; it neither searches the output relation nor uses a classical witness at runtime. Any
+  `Classical.choice` is proof-local when the certificate assembles response data. Since no prover
+  message separates the rounds, the *interactive* protocol is unchanged from Figure 5; what
+  changes is the tree shape the extractor is handed. The counterexample, repair, and concrete cost
+  are spelled out in `ZeroCheck/Reduction.lean`; the full analysis is
   `docs/kb/audits/noz26-zero-check-lemma10.md`.
 - Row 11 isolates the **§4.5/§3.2 partial-evaluation gap** found while auditing this skeleton:
   the packed claim of Eq. (26) pins only one `F`-linear functional of the per-slice values, so
@@ -115,21 +119,24 @@ key (`quadEvalEscLocal`); rows 4, 6 and 8 carry the weak-binding collision of th
 
 ## Sorry inventory of the composed chain (provenance of the certificate)
 
-*Generic machinery*: `Verifier.IsGuarded.append` and
-`Verifier.append_coordinateWiseSpecialSoundWithEscape_of_guardedLeft` (`Guarded.lean`; the latter is
-the fundamental obligation, stated escape-threaded at explicit guard data — the plain guarded
-append is *proven* from it at the never-firing events). The two scalar-round assemblies
-`coordinateWiseSpecialSoundWith(Escape)_of_mkWitness_scalar` (`ScalarRound.lean`) are proven, as
-are their readers, shape recovery, extractor and escape event. The escape
-layer (`TranscriptTree/Basic.lean`, `CWSS/{Basic,Composition}.lean`, `Escape.lean`) with its append
+*Generic machinery*: `Verifier.GuardedForm.append`'s `verify_eq` (`Guarded.lean`) — the one
+remaining generic obligation, and the only `sorry` left on the composition path now that both
+guarded append theorems are proved. The two scalar-round assemblies
+`coordinateWiseSpecialSoundWith(Escape)_of_mkWitness_scalar` (`ScalarRound.lean`) are
+proven, as are their readers, shape recovery, extractor and escape event. The escape layer
+(`TranscriptTree/Basic.lean`, `CoordinateWiseSpecialSoundness/{Basic,Composition,Escape}.lean`)
+with its append
 theorem, the single-round escape assembly and `quadEval_coordinateWiseSpecialSoundWithEscape` are
 proven (`sorryAx`-free). Each sorried row carries its extraction *algorithm* as an explicitly
-sorried `Extractor.TreeBased`.
+sorried `Extractor.TreeBased`. Row 6 has a named, executable, witness-fed
+`nestedZeroCheckExtractor` that returns the supplied all-left leaf entry directly;
+`nestedZeroCheckEsc` remains a statement/tree escape event independent of the caller's leaf
+witnessing.
 
 **Rows 1–7 carry no sorried certificate.** The `R^lin` adapter
 (`rlinStmt`/`unstack`/`mem_relOut_of_relRlin`) and the HMZ25 lift (Lemma 9, `liftPackage.isCWSS`,
 via the generic `Lift` layer on the proven scalar-round engine and the `QuotientLift` algebra)
-are sorry-free and axiom-clean (rows 3–4). So are, on this branch:
+are sorry-free and axiom-clean (rows 3–4). The following links are as well:
 
 * row 5, the batching pull-back `mem_relLift_of_relBatched` — including the range-side soundness
   `H₀ ≡ 0 ⇒ liftShort` (`hZero_eq_zero_imp_liftShort`), so shortness is **derived**, not assumed,
@@ -139,7 +146,7 @@ are sorry-free and axiom-clean (rows 3–4). So are, on this branch:
   `CMlPolynomialEval` encodings `hZero`/`hAlpha` and the evaluation-tree zero test;
 * row 7, the sum-to-point bridge `mem_relNestedZeroCheck_of_nestedRoundRel`.
 
-*Per-link math still sorried*: two F5 sumcheck identities in `Constraints.lean`
+*Per-link math still sorried*: two sumcheck identities in `Constraints.lean`
 (`sum_sumcheckPolyZero`, `sum_sumcheckPolyAlpha` — rows 7–9 depend on them transitively),
 Lemma 11 (`round_coordinateWiseSpecialSoundWithEscape` + `roundExtractor`), the final evaluation
 (`finalEval_coordinateWiseSpecialSoundWith` + `finalEvalExtractor` + the `finalCheck` encoding),
@@ -179,7 +186,7 @@ variable {σ : Type}
 /-- The polynomial bridge followed by `QuadEval`, along a single relation seam. The bridge is
 escape-free and `QuadEval` escape-aware, so the universal `▷` lifts the bridge at the never-firing
 event and the composed event fires exactly when `QuadEval`'s own event fires on the suffix tree. -/
-noncomputable def evalChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
+def evalChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
     (hq5 : q % 8 = 5) {b ω γ : ℕ} (hκ : (2 * ω) ^ 2 < q) (hτ : 0 < zDigits)
     (pp : Hachi.PublicParamsD 𝓜(q, α) innerRows (2 ^ m) messageDigits outerRows (2 ^ r)
       innerDigits dRows) :
@@ -281,11 +288,11 @@ same workaround as `roundsSpecSampleable`). Requires a sampler for the fold chal
 escape-aware evaluation front (`evalChain` = bridge ▷ `QuadEval`) extended by the §4.3 stages
 with pure verifiers — the `R^lin` adapter, the HMZ25 lift, the batching bridge, the
 (corrected-Lemma-10) zero-check, and the sumcheck bridge. Every relation seam is definitional
-(`rfl`). The public result reduces `relPolyEval` to the round-`0` `nestedRoundRel`; the composite's escape
-event is the `EscapeEvent.append`-nesting of the honest factor events (`QuadEval`'s Module-SIS break
-in row 2, the lift's weak-binding collision in row 4, the zero-check's in row 6), each on its own
-subtree. -/
-noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
+(`rfl`). The public result reduces `relPolyEval` to the round-`0` `nestedRoundRel`; the
+composite's escape event is the `EscapeEvent.append`-nesting of the honest factor events:
+`QuadEval`'s Module-SIS break in row 2, the lift's weak-binding collision in row 4, and the
+zero-check's in row 6, each on its own subtree. -/
+def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
     (hq5 : q % 8 = 5) {b ω γ ρBound m₀ m₁ : ℕ} (hκ : (2 * ω) ^ 2 < q) (hτ : 0 < zDigits)
     [SampleableType (ShortChallenge 𝓜(q, α) ω)]
     (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) (liftShort 𝓜(q, α) γ ρBound))
@@ -315,23 +322,23 @@ noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT
     nestedSumcheckBridgePackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b
 
 /-- **One full Hachi opening iteration** (rows 1–12 of the chain table): the pure prefix
-`openCore` composed with the guarded tail: the `m₀` paired sumcheck rounds (Lemma 11, guarded on
-the round checks), the final-evaluation step (guarded on the target checks), and the §4.5
-recursion adapters (the pure partial-evaluation head, the ⚠ `Z`-packing bridge with the open
-row-11 soundness question, and the guarded trace handoff). Pure factors (`openCore`,
-`partialEvalPackage`, `zBatchPackage`) stay pure escape packages and are lifted into the
-escape-guarded world by the mixed appends behind the universal `▷` (the two head seams, whose
-relation identifications are the named `roundsChain_relIn`/`roundsChain_relOut` lemmas rather than
-`rfl`, use `EscapeCWSSPackage.appendEscapeGuarded` / `EscapeGCWSSPackage.appendGuarded`
+`openCore` composed with the guarded tail: the `m₀` paired sumcheck rounds (Lemma 11, guarded on the
+round checks), the final-evaluation step (guarded on the target checks), and the §4.5 recursion
+adapters (the pure partial-evaluation head, the ⚠ `Z`-packing bridge with the open row-11 soundness
+question, and the guarded trace handoff). Pure factors (`openCore`, `partialEvalPackage`,
+`zBatchPackage`) stay pure escape packages and are lifted into the escape-guarded world by the mixed
+appends behind the universal `▷` (the two head seams, whose relation identifications are the named
+`roundsChain_relIn`/`roundsChain_relOut` lemmas rather than `rfl`, use
+`EscapeCWSSPackage.appendEscapeGuarded` / `EscapeGCWSSPackage.appendGuarded`
 explicitly). The chain lands on the plain `relIn Φ'` relation — closing the recursion loop:
-iteration `i+1` is this chain re-instantiated at `Φ'` (entering at `quadEvalPackage`, without
-row 1).
+iteration `i+1` is this chain re-instantiated at `Φ'` (entering at `quadEvalPackage`, without row
+1).
 
 The certificate `openingChain.isCWSS` is the one-iteration CWSS statement; its provenance (which
 links are finished, skeleton-sorried, or gap-flagged) is inventoried in the module header. The
 sumcheck arity is pinned to `m₀ := mLow + κ` so the recursion adapters can peel the top `κ`
 variables. -/
-noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
+def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
     (hq5 : q % 8 = 5) {b ω γ ρBound m₁ mLow κ : ℕ} (hκ : (2 * ω) ^ 2 < q) (hτ : 0 < zDigits)
     [SampleableType (ShortChallenge 𝓜(q, α) ω)]
     (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) (liftShort 𝓜(q, α) γ ρBound))