@@ -21,7 +21,7 @@ file and exported as a `CWSSPackage` (pure verifier) or `GCWSSPackage` (guarded
2121(CWSS), the knowledge-soundness notion under which a witness is extracted from a suitably
2222structured tree of accepting transcripts. This file only **imports those packages and chains
2323them**: pure links with `▷` (`CWSSPackage.append`, seams discharged by `rfl`), guarded links with
24- `▷ᵍ` (`GCWSSPackage.append`, the B4 skeleton in
24+ `▷ᵍ` (`GCWSSPackage.append`, the skeleton in
2525`OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean`). The composed chain's
2626`isCWSS` field is the CWSS certificate for the whole reduction. (Hachi as a `Commitment.Scheme` —
2727the honest committer `keygen`/`commit` and the `hachi` functional commitment — lives in the
@@ -31,10 +31,10 @@ sibling `Commitment.lean`.)
3131
32321. **`evalChain`** (sorry-free, finished): the polynomial-level bridge ▷ `QuadEval`
3333 (§4.2 / Figure 3 / Lemma 8).
34- 2. **`openCore`** (skeleton, pure links): the escape-threaded front `evalChainE` extended by the
35- §4.3 stages up to the sumcheck bridge — R^lin adapter (F2) ▷ HMZ25 lift (Figure 4 / Lemma 9 )
36- ▷ batching bridge (Eqs. (22)–(23)) ▷ zero-check ( Figure 5 / **corrected** Lemma 10 ) ▷
37- sumcheck bridge.
34+ 2. **`openCore`** (pure links; rows 3–4 proven, rows 5–7 skeleton ): the escape-threaded front
35+ `evalChainE` extended by the §4.3 stages up to the sumcheck bridge — R^lin adapter (proven )
36+ ▷ HMZ25 lift ( Figure 4 / Lemma 9, **proven & axiom-clean** ) ▷ batching bridge
37+ (Eqs. (22)–(23)) ▷ zero-check (Figure 5 / **corrected** Lemma 10) ▷ sumcheck bridge.
38383. **`openingChain`** (skeleton, guarded tail): `openCore` ▷ᵍ the paired sumcheck loop
3939 (Figure 6 / Lemma 11, `m₀` guarded rounds) ▷ᵍ final evaluation (Figure 7 tail) ▷ᵍ the §4.5
4040 recursion adapters (partial evaluations ▷ᵍ `Z`-packing bridge ▷ᵍ trace handoff), landing on
@@ -46,10 +46,10 @@ sibling `Commitment.lean`.)
4646Top-to-bottom is one opening iteration of the ArkLib Hachi commitment, whose committed data is an
4747`Rq`-valued multilinear polynomial. The opening starts with the Figure 3 path, not with §3: the §3
4848packing head (extension-field claims into `Rq`-claims, via the generalized `RingSwitching` packing
49- phase — see `HACHI_RING_SWITCHING_PLAN.md`, Phases B–E ) is a separate track that wraps *external*
49+ phase) is a separate track that wraps *external*
5050extension-field claims in front of `relPolyEval(E)`; the §4.5 adapters below close the recursion
5151*internally* . Witnesses in rows 3–11 are `· ⊕ E`: escape threading (`Set.withEscape`) gives every
52- seam a home for the `w̃`-commitment's weak-binding break (design G1; `E` abstract, escape set
52+ seam a home for the `w̃`-commitment's weak-binding break (`E` abstract, escape set
5353`K.esc`).
5454
5555```text
@@ -73,20 +73,20 @@ seam a home for the `w̃`-commitment's weak-binding break (design G1; `E` abstra
7373
7474- Rows 1–7 have **pure** verifiers: every check constrains either retained statement data or the
7575 never-sent witness, so it lives in the output relation (the `QuadEval` precedent). Rows 8, 9,
76- 12 are **guarded** (design D6) : their runtime check reads data the next statement type drops
76+ 12 are **guarded** : their runtime check reads data the next statement type drops
7777 (the previous sumcheck target; the final targets; the packed claim value) — exactly the paper's
78- runtime checks — and compose via `▷ᵍ`, whose composition theorem (B4) is the one sorried piece
78+ runtime checks — and compose via `▷ᵍ`, whose composition theorem is the one sorried piece
7979 of *generic* machinery.
8080- Row 6 implements the **corrected Lemma 10** : the paper's uniform-vector star extraction is not
8181 provable (axis-cross counterexample); the challenge is a pair of scalar **Kronecker seeds**
8282 with the batching points derived on the curves `κ_m(ρ) = (ρ, ρ², ρ⁴, …)`, giving genuine
83- `(ℓ, k) = (2, D)` CWSS at `D = max 2^{m₀} 2^{m₁}`. See `HACHI_LEMMA10_GAP.md`. This is the one
83+ `(ℓ, k) = (2, D)` CWSS at `D = max 2^{m₀} 2^{m₁}`. This is the one
8484 place the formalization deliberately changes the paper's protocol.
8585- Row 11 isolates the **§4.5/§3.2 partial-evaluation gap** found while auditing this skeleton:
8686 the packed claim of Eq. (26) pins only one `F`-linear functional of the per-slice values, so
8787 the paper's step is (apparently) not knowledge-sound as stated; the bridge's pull-back sorry is
8888 expected to be unprovable until a repair (batching challenge / generic §3.1 packing) is
89- adopted. See `HACHI_RECURSION_GAP.md`. All other sorries in the chain are honest skeleton work.
89+ adopted. All other sorries in the chain are honest skeleton work.
9090- Row 12 lands on `relInE Φ'` — the escape-threaded `QuadEval` input relation at the **next**
9191 ring: iteration `i+1` re-enters at `quadEvalPackageE Φ'` directly (its bases are `eq`-tensor
9292 packings, not monomial bases, so the polynomial-level bridge of row 1 is head-only).
@@ -95,18 +95,21 @@ seam a home for the `w̃`-commitment's weak-binding break (design G1; `E` abstra
9595
9696
9797
98- *Generic machinery* (B4): `Verifier.IsGuarded.append`,
99- `Verifier.append_coordinateWiseSpecialSound_of_guardedLeft` (`Guarded.lean`);
100- `coordinateWiseSpecialSound_of_mkWitness_scalar` (`ScalarRound.lean`, consumed only by future
101- proofs). *Escape threading* (F2.0): `quadEval_coordinateWiseSpecialSound_withEscape`.
102- *Per-link math* : the F2 index bookkeeping (`rlinStmt`/`unstack`/`mem_relOutE_of_relRlinE`),
103- Lemma 9 (`lift_coordinateWiseSpecialSound`), the F5 encodings (`Constraints.lean`), the
98+ *Generic machinery* : `Verifier.IsGuarded.append`,
99+ `Verifier.append_coordinateWiseSpecialSound_of_guardedLeft` (`Guarded.lean`).
100+ *Escape threading* : `quadEval_coordinateWiseSpecialSound_withEscape`.
101+ *Per-link math* (the `R^lin` adapter — `rlinStmt`/`unstack`/`mem_relOutE_of_relRlinE` — and
102+ the HMZ25 lift — Lemma 9, `liftPackage.isCWSS` (generic `Lift.coordinateWiseSpecialSound`) on the
103+ proven scalar-round engine `coordinateWiseSpecialSound_of_mkWitness_scalar` and the `QuotientLift`
104+ algebra — are now proven, sorry-free and axiom-clean; rows 1–4 of the table carry no sorries):
105+ the encodings (`Constraints.lean`), the
104106un-batching (`mem_relLiftE_of_relBatchedE`), corrected Lemma 10
105107(`zeroCheck_coordinateWiseSpecialSound`), the sum-to-point bridge, Lemma 11
106- (`round_coordinateWiseSpecialSound`), F8 (`finalEval_coordinateWiseSpecialSound` + the
107- `finalCheck` encoding), G2 (`partialEval_coordinateWiseSpecialSound` + its encoding defs), G3
108+ (`round_coordinateWiseSpecialSound`), final evaluation (`finalEval_coordinateWiseSpecialSound` +
109+ the `finalCheck` encoding), partial evaluation (`partialEval_coordinateWiseSpecialSound` + its
110+ encoding defs), and trace handoff
108111(`handoff_coordinateWiseSpecialSound` + `traceCheck`/`toNextQuadEvalStatement`/`hatEval`).
109- Every sorried encoding def carries an in-situ `**Sorried**` docstring naming its milestone .
112+ Every sorried encoding def carries an in-situ `**Sorried**` docstring.
110113*Flagged as an open gap (not merely unproven)* : `mem_relPartialEvalE_of_relHatEvalE` (row 11).
111114
112115## References
@@ -234,7 +237,9 @@ noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT
234237 [SampleableType (ShortChallenge 𝓜(q, α) ω)]
235238 (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) E (liftShort 𝓜(q, α) γ ρBound))
236239 (φF : ZMod q →+* F)
237- (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1 ) (hb : b - 1 ≤ γ) :
240+ (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1 ) (hb : b - 1 ≤ γ)
241+ (hρ : b - 1 ≤ ρBound) (hcov : (μ₀ + n₀) * (𝓜(q, α)).φ.natDegree ≤ 2 ^ m₀)
242+ (hn : n₀ ≤ 2 ^ m₁) :
238243 CWSSPackage init impl
239244 (PolyEvalStatement 𝓜(q, α) innerRows messageDigits outerRows innerDigits dRows m r)
240245 (QuadEvalWitness 𝓜(q, α) innerRows (2 ^ m) messageDigits (2 ^ r) innerDigits ⊕ E)
@@ -250,15 +255,15 @@ noncomputable def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT
250255 evalChainE (b := b) (γ := γ) init impl hq5 hκ hτ K.esc ▷
251256 rlinPackage (zDigits := zDigits) 𝓜(q, α) init impl (b : ZMod q) ω γ K.esc ▷
252257 liftPackage 𝓜(q, α) γ ρBound K φF init impl hd ▷
253- batchPackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b hq2 hb ▷
258+ batchPackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b hq2 hb hρ hcov hn ▷
254259 zeroCheckPackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b ▷
255260 sumcheckBridgePackage 𝓜(q, α) m₀ m₁ γ ρBound init impl K φF b
256261
257262/-- **One full Hachi opening iteration** (rows 1–12 of the chain table): the pure prefix
258263`openCore` composed — through the guarded append `▷ᵍ` — with the guarded tail: the `m₀` paired
259264sumcheck rounds (Lemma 11, guarded on the round checks), the final-evaluation step (guarded on
260265the target checks), and the §4.5 recursion adapters (the pure partial-evaluation head, the ⚠
261- `Z`-packing bridge of `HACHI_RECURSION_GAP.md` , and the guarded trace handoff). The chain lands
266+ `Z`-packing bridge, and the guarded trace handoff). The chain lands
262267on `relInE Φ'` — the escape-threaded `QuadEval` input relation at the next ring `Φ'` — closing
263268the recursion loop: iteration `i+1` is this chain re-instantiated at `Φ'` (entering at
264269`quadEvalPackageE`, without row 1).
@@ -273,6 +278,8 @@ noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (Sta
273278 (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) E (liftShort 𝓜(q, α) γ ρBound))
274279 (φF : ZMod q →+* F)
275280 (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1 ) (hb : b - 1 ≤ γ)
281+ (hρ : b - 1 ≤ ρBound) (hcov : (μ₀ + n₀) * (𝓜(q, α)).φ.natDegree ≤ 2 ^ (mLow + κ))
282+ (hn : n₀ ≤ 2 ^ m₁)
276283 (zpow : Fin (2 ^ κ) → F)
277284 (Φ' : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ']
278285 {innerRows' messageDigits' outerRows' innerDigits' dRows' m' r' : ℕ}
@@ -300,7 +307,8 @@ noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (Sta
300307 roundsSpec F b (mLow + κ)) ++ₚ pSpecFinalEval F).Challenge i) :=
301308 ProtocolSpec.instSampleableTypeChallengeAppend (h₁ := i₁)
302309 (h₂ := instSampleableTypeChallengePSpecFinalEval)
303- (((openCore (m₀ := mLow + κ) (m₁ := m₁) init impl hq5 hκ hτ K φF hd hq2 hb).toGuarded.append
310+ (((openCore (m₀ := mLow + κ) (m₁ := m₁) init impl hq5 hκ hτ K φF hd hq2 hb hρ hcov
311+ hn).toGuarded.append
304312 (roundsChain 𝓜(q, α) (mLow + κ) m₁ γ ρBound b init impl K φF (mLow + κ))
305313 (roundsChain_relIn 𝓜(q, α) (mLow + κ) m₁ γ ρBound b init impl K φF
306314 (mLow + κ)).symm).append
@@ -315,14 +323,16 @@ noncomputable def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (Sta
315323The composed verifier of rows 1–12 is CWSS, reducing the polynomial-level `relPolyEvalE` (over
316324the current ring `𝓜(q, α)`) to the next iteration's `relInE` (over `Φ'`). The proof term is
317325just `openingChain.isCWSS`; its assumptions are exactly the sorried links inventoried in the
318- module header (in particular the ⚠ row-11 gap and the B4 guarded-append machinery). -/
326+ module header (in particular the ⚠ row-11 gap and the guarded-append machinery). -/
319327theorem hachi_iteration_coordinateWiseSpecialSound (init : ProbComp σ)
320328 (impl : QueryImpl oSpec (StateT σ ProbComp))
321329 (hq5 : q % 8 = 5 ) {b ω γ ρBound m₁ mLow κ : ℕ} (hκ : (2 * ω) ^ 2 < q) (hτ : 0 < zDigits)
322330 [SampleableType (ShortChallenge 𝓜(q, α) ω)]
323331 (K : LiftCom (LiftedWitness 𝓜(q, α) μ₀ n₀) E (liftShort 𝓜(q, α) γ ρBound))
324332 (φF : ZMod q →+* F)
325333 (hd : 0 < (𝓜(q, α)).φ.natDegree) (hq2 : 2 * b ≤ q + 1 ) (hb : b - 1 ≤ γ)
334+ (hρ : b - 1 ≤ ρBound) (hcov : (μ₀ + n₀) * (𝓜(q, α)).φ.natDegree ≤ 2 ^ (mLow + κ))
335+ (hn : n₀ ≤ 2 ^ m₁)
326336 (zpow : Fin (2 ^ κ) → F)
327337 (Φ' : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ']
328338 {innerRows' messageDigits' outerRows' innerDigits' dRows' m' r' : ℕ}
@@ -331,15 +341,15 @@ theorem hachi_iteration_coordinateWiseSpecialSound (init : ProbComp σ)
331341 (reinterpretCom : K.TCom → Commitment Φ' outerRows')
332342 (base' : ZMod q) (βSq' γ' κ' : ℕ) :
333343 ((openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) init impl hq5 hκ
334- hτ K φF hd hq2 hb zpow Φ' pp' reinterpretCom base' βSq'
344+ hτ K φF hd hq2 hb hρ hcov hn zpow Φ' pp' reinterpretCom base' βSq'
335345 γ' κ')).verifier.coordinateWiseSpecialSound init impl
336346 (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) init impl hq5 hκ hτ
337- K φF hd hq2 hb zpow Φ' pp' reinterpretCom base' βSq' γ' κ').struct
347+ K φF hd hq2 hb hρ hcov hn zpow Φ' pp' reinterpretCom base' βSq' γ' κ').struct
338348 (relPolyEvalE 𝓜(q, α) (b : ZMod q)
339349 (quadEvalBetaSq γ b zDigits ((𝓜(q, α)).φ.natDegree) m messageDigits) γ (2 * ω) K.esc)
340350 (relInE Φ' base' βSq' γ' κ' K.esc) :=
341351 (openingChain (zDigits := zDigits) (ω := ω) (mLow := mLow) (m₁ := m₁) init impl hq5 hκ hτ
342- K φF hd hq2 hb zpow Φ' pp' reinterpretCom base' βSq' γ' κ').isCWSS
352+ K φF hd hq2 hb hρ hcov hn zpow Φ' pp' reinterpretCom base' βSq' γ' κ').isCWSS
343353
344354end OpeningChain
345355
@@ -348,16 +358,16 @@ end OpeningChain
348358* **§3 packing head (external extension-field claims).** The paper's headline
349359 multilinear-over-`F_{q^k}` interface (§3.1/§3.2) wraps an extension-field evaluation claim in
350360 front of `relPolyEvalE`; it is planned as an instance of the generalized `RingSwitching`
351- packing phase (`HACHI_RING_SWITCHING_PLAN.md`, Phases B–E) , not as a Hachi-local head.
361+ packing phase, not as a Hachi-local head.
352362* **Recursion termination.** At the row-12 seam: the §4.4 asymptotic base case (reveal the final
353363 small polynomial — a `SendWitness`-style tail) and the §4.5 concrete cutoff (switch to
354364 Greyhound/LaBRADOR, i.e. the JL projection route) are future zero-round/one-message tails.
355- * **Discharging the skeleton.** The sorry inventory in the module header, in dependency order:
356- B4 (`Guarded.lean`) → F2.0/F2 → F3/F4 → F5 → F6 → F7 → F8 → G2/G3 — plus a repair decision for
357- the row-11 gap (`HACHI_RECURSION_GAP.md`) and the Phase-G `LiftCom` instantiation (the
365+ * **Discharging the skeleton.** Work through the sorry inventory in the module header in
366+ dependency order, starting from the guarded-append machinery (`Guarded.lean`) — plus a repair
367+ decision for the row-11 gap and the `LiftCom` instantiation (the
358368 inner-outer commitment without re-decomposition, its collision escape via
359369 `outputToModuleSIS_valid_of_verified`, and the ring-dimension reinterpretation used by row 12).
360370* **Knowledge-error accounting** (FMN24 Lemma 4), `Commitment.extractability`, and Fiat–Shamir
361- (design D12/R6) . -/
371+
362372
363373end ArkLib.Lattices.Ajtai.InnerOuter
0 commit comments