feat(Hachi): make extractors computable by tobias-rothmann · Pull Request #697 · Verified-zkEVM/ArkLib

tobias-rothmann · 2026-08-06T10:03:50Z

make extractors computable

github-actions · 2026-08-06T10:06:15Z

🤖 PR Summary

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

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

Hachi extractors made fully computable; documentation and axiom baseline updated accordingly.

This PR eliminates the noncomputable marker from the Hachi extractor infrastructure by replacing classical choices with data-carrying analogues and bounded search, enabling runtime extraction. It simultaneously updates the project's documentation to reflect the finalized zero-check design and adjusts the axiom baseline (the sorry inventory). The core work is concentrated in ArkLib/; the other files are documentation and baseline bookkeeping.

Mathematical Formalization

Replaced nonconstructive primitives: The Hachi chain (ArkLib/) switches from Classical.choice, Ring.inverse, and Nonempty assumptions to explicitly computable analogues:
- Verifier.PureForm and Verifier.GuardedForm now carry data instead of being classical definitions.
- Fin.find is used for bounded search in place of Exists.choose or other nonconstructive selections.
- A new computable inverse Rq.inv is added for cyclotomic rings (Data/Lattices/CyclotomicRing/Inverse), replacing the noncomputable Ring.inverse.
Definitions unmarked: Numerous definitions across Hachi lose the noncomputable marker.
New lemmas proved:
- sum_sumcheckPolyZero' and sum_sumcheckPolyAlpha' are now proved (removed from the sorry baseline).
- Both guarded binary CWSS append theorems (append_coordinateWiseSpecialSoundWithEscape_of_guardedLeft, append_coordinateWiseSpecialSoundWith_of_guardedLeft) are proved and removed from the baseline; their Verifier.GuardedForm.append variant is added to the baseline (see “Known Gaps”).
- GuardianForm.append theorems for guarded binary CWSS append are now proved.
Updated audit (docs/kb/audits/noz26-zero-check-lemma10.md): The file is rewritten to match the current zero-check formalization. Removes all references to the superseded one-round Kronecker-seed design. Marks sum_sumcheckPolyZero and sum_sumcheckPolyAlpha as done. Notes that nestedZeroCheckExtractor is now an executable function (Classical.choice is proof-local). Renames “F5 encoding” to “Constraint encoding” and “F5 gap” to “encoding gap”.

Known Gaps / Remaining `sorry`s

Several critical components remain sorry-filled and are now tracked in the axiom baseline. The PR does not claim to prove the full correctness of the extractor, only to make the core infrastructure computable. The incomplete statements are:

Verifier.GuardedForm.append (axiom-baseline entry added). This is the sole remaining sorry in the guarded binary CWSS append section.
Verifier.append_coordinateWiseSpecialSoundWithEscape_of_guardedLeft and Verifier.append_coordinateWiseSpecialSoundWith_of_guardedLeft were removed from the baseline only because they are replaced by Verifier.GuardedForm.append — the new statement is unfinished.
Ten new sorry entries were added to the axiom baseline (under ArkLib.Lattices.Ajtai.InnerOuter):
- finalEvalVerifierGuardedForm
- handoffVerifierGuardedForm
- mem_relNestedZeroCheck_of_nestedRoundRel
- nestedSumcheckBridgePackage
- partialEvalVerifierPureForm
- sum_sumcheckPolyAlpha' and sum_sumcheckPolyZero' (new variants with ' have sorrys)
- Three entries under Verifier.GuardedForm, Verifier.IsGuarded, Verifier.StateFunction.
24 existing entries were removed from the baseline because their sorrys were completed (all from ArkLib.Lattices.Ajtai.InnerOuter). This includes zeroCheckExtractor, zeroCheckPackage, batchPackage, and others.

Documentation (No code changes)

New workflow guide (docs/skills/make-computable.md): A step-by-step guide for converting noncomputable Lean definitions into executable code, classifying gaps (Sorried, Leaf, Recursor, Architectural) and prescribing a procedure (inventory, rate, probe, replace, prove agreement, #eval, clean up). Includes pitfalls (e.g., sorry bodies do not force noncomputable, noncomputable section hides regressions).
Updated checklist (docs/skills/make-pr-ready.md): Adds steps for _generated/ drift detection, improved stale-reference checking, and detection of “dead” names that still resolve but encode historical narrative (e.g., old_of_new).
Audit refactoring: docs/kb/audits/noz26-zero-check-lemma10.md is comprehensively rewritten to match the current design (see Mathematical Formalization). docs/kb/papers/NOZ26.md reflects the executable extractor.
Repo map (docs/wiki/repo-map.md): Corrects the landing page for Hachi (now Hachi/Basic.lean). Updates descriptions for ZeroCheck/ (now nestedZeroCheckExtractor), TranscriptTree/Basic (witness-only, with LeafWitnesses.IsValid). Reports Verifier.GuardedForm.append as the sole outstanding sorry.
Cross-references: docs/skills/discharge-lemmas.md and docs/skills/README.md link to make-computable.md.

Infrastructure / CI

scripts/axiom_baseline.json: Updated to reflect the new sorry inventory (see Known Gaps). The baseline explicitly tracks which theorems are unproven; this change indicates which proofs are now complete (removed) and which are unfinished (added).
scripts/arklib.lean: Import updated from ArkLib.Commitments.Functional.Hachi to its submodule ArkLib.Commitments.Functional.Hachi.Basic, and a new import ArkLib.Data.Lattices.CyclotomicRing.Inverse added to support the new computable inverse.

Architectural Note

The core change is the Hachi extractor infrastructure (replacing nonconstructive primitives with computable analogues). The documentation and baseline files are updated to match the resulting mathematical and sorry state. No new sorrys are introduced in the documentation-only files. The work is concentrated in ArkLib/; the remaining files are mechanical or bookkeeping.

Statistics

Metric	Count
📝 Files Changed	53
✅ Lines Added	3837
❌ Lines Removed	1881

Lean Declarations

✏️ Removed: 14 declaration(s)

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

noncomputable def nestedPathResponse

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

def _root_.CoordinateWise.EscapeCWSSPackage.toGuarded
def append {StmtA WitA StmtB WitB StmtC WitC : Type}
private def univAppendFn : Name → Name → Option Name

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

def onlyTranscript [IsEmpty pSpec.ChallengeIdx]
theorem onlyTranscript_mem [IsEmpty pSpec.ChallengeIdx]

ArkLib/OracleReduction/Security/TranscriptTree/Composition.lean (8)

def RightProj.src : {r : Fin (n + 1)} → RightProj arity₁ arity₂ r →
def RightProj.tree : {r : Fin (n + 1)} → RightProj arity₁ arity₂ r →
def rightProjOfTree {r : Fin (n + 1)}
def rightProjOfTreeAux : {a : Fin (m + n + 1)} →
def splitDataOfTreeAux : {a : Fin (m + n + 1)} →
theorem RightProj.mem_transcripts_append :
theorem RightProj.tree_isStructured :
theorem rightProjOfTree_src {r : Fin (n + 1)}

✏️ Added: 99 declaration(s)

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

def bridgeVerifierPureForm : (bridgeVerifier (oSpec

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

def verifierPureForm : (verifier (oSpec

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

def partialEvalVerifierPureForm {TCom : Type} :

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

def handoffVerifierGuardedForm {TCom : Type} (φF : ZMod q →+* F)

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

def zBatchVerifierPureForm {TCom : Type} (zpow : Fin (2 ^ κ) → F) :

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

def rlinVerifierPureForm

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

def nestedSumcheckBridgeVerifierPureForm

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

def finalEvalVerifierGuardedForm {TCom : Type} (φF : ZMod q →+* F) :

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

def roundVerifierGuardedForm {TCom : Type} (i : ℕ) :
def roundsBaseVerifierPureForm {TCom : Type} :

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

def batchVerifierPureForm

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

def nestedZeroCheckVerifierPureForm {TCom : Type} :

ArkLib/Data/Lattices/CyclotomicRing/Core/Basic.lean (1)

@[simp] theorem quotientHom_phi : Φ.quotientHom Φ.φ = 0

ArkLib/Data/Lattices/CyclotomicRing/Inverse.lean (6)

def Rq.inv (a : Rq Φ) : Rq Φ
theorem Rq.inv_eq_ringInverse {a : Rq Φ} (ha : IsUnit a) :
theorem Rq.inv_mul_cancel {a : Rq Φ} (ha : IsUnit a) : Rq.inv Φ a * a = 1
theorem Rq.isCoprime_of_isUnit {a : Rq Φ} (ha : IsUnit a) :
theorem Rq.mul_inv_cancel {a : Rq Φ} (ha : IsUnit a) : a * Rq.inv Φ a = 1
theorem Rq.normXgcd_fst_eq_one {a : Rq Φ} (ha : IsUnit a) :

ArkLib/OracleReduction/Basic.lean (1)

theorem Verifier.PureForm.isPure {V : Verifier oSpec StmtIn StmtOut pSpec} (P : V.PureForm) :

ArkLib/OracleReduction/Composition/Sequential/IsPure.lean (1)

def PureForm.append {V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁}

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

instance instDecidableCoordEq [DecidableEq S] {ℓ : ℕ} (i : Fin ℓ) (x y : Fin ℓ → S) :
theorem toShape_arity_pos : ∀ i, 0 < D.toShape.arity i

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

def verifierPureForm {ι : Type} {oSpec : OracleSpec ι} (K : BindingCommitment W Short) :

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

theorem append_run_outputs

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

def EscapeCWSSPackage.append
def EscapeCWSSPackage.toGuarded
def EscapeGCWSSPackage.append
private def applyAppend (fn : Name) (lE rE : Expr) : TermElabM Expr
private def canonAppendFn : Name → Name → Option Name

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

def GuardedForm.append {V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁}
def PureForm.toGuardedForm {V : Verifier oSpec StmtIn StmtOut pSpec} (P : V.PureForm) :
theorem GuardedForm.isGuarded {V : Verifier oSpec StmtIn StmtOut pSpec} (G : V.GuardedForm) :
theorem append_run_guardedLeft
theorem append_run_outputs_guardedLeft
theorem append_treeSpecialSoundWithEscape_guardedLeft
theorem append_treeSpecialSoundWith_guardedLeft
theorem guarded_accepting_of_mem
theorem guarded_verdict_mem_outputs
theorem outputs_guarded_subsingleton

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

def branchPathOf (tree : ChallengeTree (pSpecScalar Msg C) arity 0)
def chalPathAux : {a : Fin 3} → (t : ChallengeTree (pSpecScalar Msg C) arity a) →
def lastPathAux : {a : Fin 3} → (t : ChallengeTree (pSpecScalar Msg C) arity a) →
theorem collect_branch_data {k : ℕ}
theorem fullTranscript_branchPathOf (v : Msg)

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SingleRound.lean (8)

def branchPathOf (tree : ChallengeTree (pSpec CarrierCom C r) arity 0)
def chalPathAux : {a : Fin 3} → (t : ChallengeTree (pSpec CarrierCom C r) arity a) →
def collect {K : ℕ} {W : Type} (f : Fin K → Option W) : Option (Fin K → W)
def lastPathAux : {a : Fin 3} → (t : ChallengeTree (pSpec CarrierCom C r) arity a) →
instance instDecidableStarAt [DecidableEq C] {ℓ K : ℕ} (challenges : Fin K → (Fin ℓ → C))
theorem collect_branch_data
theorem collect_eq_some {K : ℕ} {W : Type} {f : Fin K → Option W} {w : Fin K → W}
theorem fullTranscript_branchPathOf (v : CarrierCom)

ArkLib/OracleReduction/Security/SpecialSoundness.lean (1)

theorem specialSound.exists_total_extractor [Inhabited WitIn] (k : pSpec.ChallengeIdx → ℕ)

ArkLib/OracleReduction/Security/TranscriptTree/Basic.lean (18)

def IsValid (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
def LeafWitnesses (tree : ChallengeTree pSpec arity 0) (WitOut : Type) : Type
def Outputs (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
def onlyPath [IsEmpty pSpec.ChallengeIdx] :
def somePath (harity : ∀ i, 0 < arity i) :
noncomputable def canonWitnesses (init : ProbComp σ)
theorem canonWitnesses_isValid {init : ProbComp σ}
theorem isValid_iff_pure (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
theorem mem_language_of_mem_outputs {init : ProbComp σ}
theorem mem_outputs_iff (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
theorem not_accepting_of_failure {init : ProbComp σ}
theorem not_isAccepting_of_no_outputs (init : ProbComp σ)
theorem outputs_nonempty_of_isAccepting {init : ProbComp σ}
theorem outputs_pure_subsingleton {Stmt₁ Stmt₂ : Type} {m : ℕ} {pSpec₁ : ProtocolSpec m}
theorem pure_verdict_mem_outputs (init : ProbComp σ)
theorem support_init_nonempty_of_accepting {init : ProbComp σ}
theorem support_init_nonempty_of_prob_one {init : ProbComp σ}
theorem treeSpecialSoundWith.mem_relIn_of_isAccepting [Inhabited WitIn]

ArkLib/OracleReduction/Security/TranscriptTree/Composition.lean (27)

def AppendSplit.gluePath
def LeafPath.embedRight : {r : Fin (n + 1)} → {t : ChallengeTree pSpec₂ arity₂ r} →
def LeafPath.transport {r : Fin (m + 1)} {T T' : ChallengeTree pSpec₁ arity₁ r}
def SplitData.gluePath : {r : Fin (m + 1)} → (S : SplitData arity₁ arity₂ r) →
def TreeBased.append (verify₁ : Stmt₁ → pSpec₁.FullTranscript → Stmt₂)
def boundaryOf {a : Fin (m + n + 1)}
def embedRight : {r : Fin (n + 1)} → ChallengeTree pSpec₂ arity₂ r →
def splitOf : {a : Fin (m + n + 1)} →
def unembedRight : {a : Fin (m + n + 1)} →
def unembedRight' {r : Fin (n + 1)}
theorem AppendSplit.fullTranscript_gluePath
theorem LeafPath.fullTranscript_transport {T T' : ChallengeTree pSpec₁ arity₁ 0}
theorem LeafPath.transcript_embedRight :
theorem SplitData.transcript_gluePath :
theorem appendArity_left {i : Fin m} {h : pSpec₁.dir i = .V_to_P}
theorem appendArity_right {i : Fin n} {h : pSpec₂.dir i = .V_to_P}
theorem appendDir_left (i : Fin m) :
theorem appendDir_right (i : Fin n) :
theorem appendType_left (i : Fin m) :
theorem appendType_right (i : Fin n) :
theorem embedRight_isStructured :
theorem embedRight_mem_transcripts_append :
theorem embedRight_unembedRight : {a : Fin (m + n + 1)} →
theorem embedRight_unembedRight' {r : Fin (n + 1)}
theorem leftSucc {i : Fin (m + n)} {rv : ℕ} (hv : (i : ℕ) = rv) (hlt : rv + 1 < m + 1) :
theorem rightSucc {i : Fin (m + n)} {rv : ℕ} (hv : (i : ℕ) = m + rv) (hlt : rv + 1 < n + 1) :
theorem src_splitOf : {a : Fin (m + n + 1)} →

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

def evalChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/Composition.lean moved from L182 to L189
def openCore (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/Composition.lean moved from L288 to L295
def openingChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/Composition.lean moved from L334 to L341
def bridgePackage {σ : Type} in ArkLib/Commitments/Functional/Hachi/QuadEval/Bridge.lean moved from L229 to L243
def buildWitness (base : ZMod q) in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L207 to L221
def extractedOpening (base : ZMod q) in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L177 to L188
def quadEvalMkWitness (base : ZMod q) in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L252 to L267
def quadEvalPackage {ι : Type} {oSpec : OracleSpec ι} {σ : Type} in ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean moved from L596 to L609
def partialEvalExtractor in ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean moved from L165 to L182
def partialEvalPackage (init : ProbComp σ) in ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean moved from L201 to L218
def handoffExtractor in ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean moved from L157 to L179
def handoffPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean moved from L225 to L248
def zBatchPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean moved from L119 to L132
def RhoShort (ρBound : ℕ) (ρ : Fin n → CPolynomial (ZMod q)) : Prop in ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean moved from L140 to L142
def cyclotomicPresentation : Lift.Presentation (ZMod q) (Rq Φ) where in ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean moved from L102 to L104
def liftPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean moved from L252 to L255
def rlinPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L469 to L483
def rlinStmt in ArkLib/Commitments/Functional/Hachi/RingSwitch/Rlin.lean moved from L273 to L274
def nestedSumcheckBridgePackage (init : ProbComp σ) in ArkLib/Commitments/Functional/Hachi/Sumcheck/Bridge.lean moved from L84 to L97
def finalEvalExtractor in ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean moved from L141 to L160
def finalEvalPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/Sumcheck/FinalEval.lean moved from L177 to L197
def roundExtractor in ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean moved from L199 to L224
def roundPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean moved from L246 to L271
def roundsChain (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean moved from L310 to L347
def roundsChainAux (init : ProbComp σ) in ArkLib/Commitments/Functional/Hachi/Sumcheck/Rounds.lean moved from L273 to L312
def batchPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Batch.lean moved from L126 to L138
def nestedZeroCheckExtractor {TCom : Type} : in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean moved from L454 to L442
def nestedZeroCheckPackage (init : ProbComp σ) in ArkLib/Commitments/Functional/Hachi/ZeroCheck/Reduction.lean moved from L622 to L619
def package {ι : Type} {oSpec : OracleSpec ι} {σ : Type} in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean moved from L261 to L273
def treeExtractor {k : ℕ} (hk : 2 ≤ k) (K : BindingCommitment W Short) (project : W → WitIn) : in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean moved from L198 to L202
theorem coordinateWiseSpecialSoundWithEscape {ι : Type} {oSpec : OracleSpec ι} in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/CommittedScalar.lean moved from L238 to L249
def CWSSPackage.toEscape (L : CWSSPackage init impl StmtIn WitIn StmtOut WitOut pSpec) : in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Escape.lean moved from L215 to L132
def GCWSSPackage.toEscape (L : GCWSSPackage init impl StmtIn WitIn StmtOut WitOut pSpec) : in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Escape.lean moved from L229 to L144
theorem IsGuarded.append (V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁) in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean moved from L113 to L156
theorem append_coordinateWiseSpecialSoundWith_of_guardedLeft in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Guarded.lean moved from L161 to L498
def append {StmtA WitA StmtB WitB StmtC WitC : Type} in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/Package.lean moved from L94 to L102
def treeExtractorScalar {k : ℕ} (hk : 2 ≤ k) in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/ScalarRound.lean moved from L336 to L385
def central [DecidableEq C] {ℓ K : ℕ} (challenges : Fin K → (Fin ℓ → C)) [Inhabited (Fin K)] : in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SingleRound.lean moved from L273 to L327
def sib [DecidableEq C] {ℓ K : ℕ} (challenges : Fin K → (Fin ℓ → C)) [Inhabited (Fin K)] in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SingleRound.lean moved from L279 to L332
def treeExtractor {StmtIn WitOut WitIn : Type} in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SingleRound.lean moved from L349 to L419
theorem sib_coordEq [DecidableEq C] {ℓ K : ℕ} (challenges : Fin K → (Fin ℓ → C)) in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SingleRound.lean moved from L296 to L349
theorem sib_coordEq_ne [DecidableEq C] {ℓ K : ℕ} (challenges : Fin K → (Fin ℓ → C)) in ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SingleRound.lean moved from L312 to L365
def TreeBased (StmtIn WitIn WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) in ArkLib/OracleReduction/Security/TranscriptTree/Basic.lean moved from L319 to L654
def treeSpecialSoundEscape (S : ChallengeTreeShape pSpec) in ArkLib/OracleReduction/Security/TranscriptTree/Basic.lean moved from L440 to L747
def treeSpecialSoundWithEscape (S : ChallengeTreeShape pSpec) in ArkLib/OracleReduction/Security/TranscriptTree/Basic.lean moved from L426 to L716
theorem treeSpecialSoundWith_congr {S S' : ChallengeTreeShape pSpec} (hS : S = S') in ArkLib/OracleReduction/Security/TranscriptTree/Basic.lean moved from L404 to L826
def chalPeelAux : {ρ : Fin (m + 1)} → {T : ChallengeTree pSpec₁ arity₁ ρ} → (p : LeafPath T) → in ArkLib/OracleReduction/Security/TranscriptTree/Composition.lean moved from L380 to L406
def peelMsgAux : {ρ : Fin (m + 1)} → {T : ChallengeTree pSpec₁ arity₁ ρ} → (p : LeafPath T) → in ArkLib/OracleReduction/Security/TranscriptTree/Composition.lean moved from L346 to L373
def oracleTreeExtractor (mapWitInv : StmtIn × (∀ i, OStmtIn i) → WitOut → WitIn) in ArkLib/ProofSystem/Component/ReduceClaim.lean moved from L407 to L409
def treeExtractor (mapWitInv : StmtIn → WitOut → WitIn) in ArkLib/ProofSystem/Component/ReduceClaim.lean moved from L187 to L190
theorem oracleVerifier_coordinateWiseSpecialSoundWith in ArkLib/ProofSystem/Component/ReduceClaim.lean moved from L421 to L420
theorem verifier_coordinateWiseSpecialSoundWith in ArkLib/ProofSystem/Component/ReduceClaim.lean moved from L199 to L204
theorem eq_of_modulus_dvd {a b : S} in ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean moved from L136 to L156
theorem eq_zero_of_modulus_dvd_of_natDegree_lt {p : Polynomial R} (h : P.modulus.toPoly ∣ p) in ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean moved from L162 to L184
theorem modulus_dvd_rep_zero : P.modulus.toPoly ∣ (P.rep 0).toPoly in ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean moved from L114 to L133
theorem natDegree_modulus_pos : 0 < P.modulus.toPoly.natDegree in ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean moved from L110 to L129
theorem rep_add (a b : S) : in ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean moved from L181 to L203
theorem rep_neg (a : S) : (P.rep (-a)).toPoly = -(P.rep a).toPoly in ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean moved from L194 to L218
theorem rep_zero : (P.rep (0 : S)).toPoly = 0 in ArkLib/ProofSystem/RingSwitching/Lift/Presentation.lean moved from L176 to L198
def escEvent [IsPresentation P] (hd : P.modulus.toPoly.natDegree = d) : in ArkLib/ProofSystem/RingSwitching/Lift/Reduction.lean moved from L165 to L170
def package [IsPresentation P] (hφF : Function.Injective φF) in ArkLib/ProofSystem/RingSwitching/Lift/Reduction.lean moved from L204 to L215
def treeExtractor [IsPresentation P] (hd : P.modulus.toPoly.natDegree = d) : in ArkLib/ProofSystem/RingSwitching/Lift/Reduction.lean moved from L174 to L183

sorry Tracking

✅ Removed: 2 `sorry`(s)

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

theorem IsGuarded.append (V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁) (L116)
theorem append_coordinateWiseSpecialSoundWithEscape_of_guardedLeft (L155)

❌ Added: 1 `sorry`(s)

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

def GuardedForm.append {V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁} (L153)

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

ArkLib/OracleReduction/Security/TranscriptTree/Composition.lean (+551/-376)

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

Last updated: 2026-08-12 10:17 UTC.

github-actions · 2026-08-06T10:18:30Z

Build Timing Report

Commit: 3c72749
Message: feat(Hachi): make extractors computable
Ref: tr/computable-extractors
Comparison baseline: b144e23 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	949.58	966.69	+17.11	ok
Warm rebuild	2.51	2.46	-0.05	ok
Validation wrapper	2.79	2.70	-0.09	ok

Incremental Rebuild Signal

Warm rebuild saved 964.23s vs clean (392.96x 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
126.00	132.00	-6.00	`ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean`
74.00	59.00	+15.00	`ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean`
71.00	76.00	-5.00	`ArkLib/ProofSystem/Stir/Combine.lean`
68.00	66.00	+2.00	`ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean`
65.00	54.00	+11.00	`ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean`
64.00	58.00	+6.00	`ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean`
60.00	64.00	-4.00	`ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean`
59.00	55.00	+4.00	`ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean`
56.00	51.00	+5.00	`ArkLib/Data/MvPolynomial/EvenAndOdd.lean`
53.00	53.00	+0.00	`ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean`
47.00	50.00	-3.00	`ArkLib/Data/CodingTheory/ProximityGap/Folding.lean`
42.00	43.00	-1.00	`ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean`
41.00	35.00	+6.00	`ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean`
39.00	36.00	+3.00	`ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/WeightedAgreement.lean`
38.00	53.00	-15.00	`ArkLib/OracleReduction/LiftContext/Reduction.lean`
37.00	39.00	-2.00	`ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean`
37.00	38.00	-1.00	`ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean`
33.00	32.00	+1.00	`ArkLib/Data/CodingTheory/DivergenceOfSets.lean`
31.00	27.00	+4.00	`ArkLib/Data/CodingTheory/PolishchukSpielman/Existence.lean`
30.00	25.00	+5.00	`ArkLib/Data/Polynomial/Indicator.lean`

…ebt only Baseline for the computable-extractor work planned in docs/plans/computable-cwss-extractors.md (milestone M0, step 1). - Tree-split rework in `TranscriptTree/Composition.lean`: all 16 `*Package.append*` operators are computable, and `TranscriptTree/Basic.lean` no longer opens a file-wide `noncomputable section`. - Drop `noncomputable` from sorried extractors and from the definitions that carried the marker only because they mentioned one, so the marker set records genuine computability debt rather than proof debt. Each such docstring now says the generated code panics until its `sorry` is filled. - `docs/skills/make-computable.md`: record the Recursor kind, the IR-presence inventory rule, and the `sorry`-does-not-force-`noncomputable` pitfall these changes rest on. - Vendor the plan and its four machine-checked prototypes under `docs/plans/`. Inventory probe (plan §9 note 2) against this tree: 20 noncomputable definitions whose type mentions `Extractor.TreeBased` or a CWSS package, 6 of them narrowly extractor-typed — exactly the population §2 counts. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Milestone M0 step 3 of docs/plans/computable-cwss-extractors.md: remove the classical root that is independent of the extractor-notion work. `onlyTranscript` selected a challenge-free tree's unique full transcript as `(fullTranscripts_eq_singleton tree).choose`, so every extractor the no-challenge bridges produced was noncomputable. It is replaced by `ChallengeTree.onlyPath`, the unique root-to-leaf *path*, read off the tree by structural recursion — and therefore computable and axiom-free. Stating the bridges at the path rather than the transcript is also the granularity a leaf-indexed extraction premise needs later in the plan. - `TranscriptTree/Basic.lean`: add `ChallengeTree.onlyPath`, beside `LeafPath`, the structure it constructs (`docs/skills/make-computable.md` step 4's placement rule). - `NoChallenge.lean`: restate the three bridges at `tree.onlyPath.fullTranscript`, delete `onlyTranscript` and `onlyTranscript_mem` (zero consumers afterwards), and drop the file's `noncomputable section`. `transcripts_eq_singleton` / `fullTranscripts_eq_singleton` stay. - `SendWitness.lean`: the two CWSS statements that apply those bridges. They are the only consumers that needed touching — the other four (`CheckClaim`, `SendClaim`, `ReduceClaim` x2) pass an `e` that ignores its transcript argument, so their applications stay definitionally equal across the swap. Gates: `./scripts/validate.sh` green over all 324 imports; `IR PRESENT: ProtocolSpec.ChallengeTree.onlyPath` and it depends on no axioms; `rg -w onlyTranscript ArkLib/` returns nothing; on a concrete one-message tree `#eval tree.onlyPath.fullTranscript 0` prints `42`, kernel-`rfl`-checked. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Session protocol step 5: fill §11's M0 row with the milestone's actual gate output (inventory probe counts and names, validate.sh lines, the IR-gate and axiom prints, the runtime `#eval`), record the `BASELINE` SHA in §1 rule 2, and note the three deviations — `onlyPath`'s home, the four bridge consumers that stayed defeq, and the deliberately untouched generated KB catalog. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…cal` (M2 step 2a) Mechanical rename per the migration shim of `docs/plans/computable-cwss-extractors.md` §4.5: `Extractor.TreeBased`, the `Verifier`/`OracleVerifier` tree- and CWSS-soundness notions with their forgetful and transport lemmas, the four `CoordinateWise` package structures with their 16 appends and lifts, and every certificate-producing append/bridge theorem gain a `Classical` suffix — which frees the canonical names for the witness-only notion. The `▷` dispatch table's constant literals are renamed, not deleted. No statement, proof or definition changes. `lake build` green (4148 jobs); the word-boundary grep over §4.5's table names is clean across every `.lean` file under `ArkLib/`. The vendored prototypes are patched in the same commit so the evidence stays runnable (§1 rule 3, "apply the rename inside `docs/plans/prototypes/`"): `Extractor.TreeBased` renamed in `CM_gates`, `nonempty_leafPath` re-proved on M0's `onlyPath`, and `CM_enginecerts`' inlined `onlyPath` dropped in favour of the in-library one. All four prototypes reproduce §6's expected output. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…2 step 2b) Lands the generic notion of `docs/plans/computable-cwss-extractors.md` §4.1 under the canonical names, additively — nothing migrates onto it yet, so every consumer stays on the `*Classical` layer and the build stays green. * `Verifier.Outputs` — the statements a verifier can output on a transcript under the fixed sampling, with the acceptance bridges (`mem_language_of_mem_outputs`, `outputs_nonempty_of_isAccepting`, `support_init_nonempty_of_accepting`) and the pure-verifier pin-down (`outputs_pure_subsingleton`, `pure_verdict_mem_outputs`). * `ChallengeTree.LeafWitnesses` / `LeafWitnesses.IsValid` — one candidate output witness per leaf, valid when each witness certifies, in `relOut`, *some* statement the verifier can output at that leaf (∃ over `Outputs`, not ∀). `LeafWitnesses.isValid_iff_pure` is the pure-case collapse. * `Extractor.TreeBased` — the witness-only extractor `StmtIn → (tree) → tree.LeafWitnesses WitOut → Option WitIn`; no `StmtOut` index, since attributing output statements is the verifier's business. * `Verifier.treeSpecialSoundWith` and its escape twin, the ∃-forms, the forgetful maps and the two shape-congruence transports, all at the widened extractor. * `ChallengeTree.canonWitnesses` (+ `canonWitnesses_isValid`: valid on every accepting tree) and `Verifier.treeSpecialSoundWith.old_of_new`, which recovers the unconditioned classical reading from a certificate and needs only `[Inhabited WitIn]`. * Purity as data: `Verifier.PureForm` (+ `isPure`, `pureFormOfIsPure`) beside `Verifier.IsPure`, the computable `Verifier.PureForm.append` beside `IsPure.append`, and `Verifier.GuardedForm` + `PureForm.toGuardedForm` beside `IsGuardedWith`. * `Security/TranscriptTree/NonVacuity.lean` — the permanent regression gates: refutability at `relIn = ∅` for every extractor, satisfiability of the validity premise, the ∀-over-outputs kill against the classical statement, the reachability-free kill on a sound forwarding engine, the constant-`none` invalidity, and the arity-0 edge. The rejected variants and the fixtures are `private`. Migration shim, deleted with the `*Classical` layer: `Extractor.TreeBased.ofClassical` and `Verifier.treeSpecialSoundWith.new_of_old`. Gates: `IR PRESENT` on `PureForm.append`, `PureForm.toGuardedForm`, `TreeBased.ofClassical`, their toy applications and the three decisive `def probe := @X` probes; `#print axioms` on all 31 new declarations free of `sorryAx`; `./scripts/validate.sh` green over 325 imports; no new build warnings. Lands after the execution-log commit rather than before it: the original handover script committed 2a and the log but dropped this step's patch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…ractor (M3 step 3a) Re-lands the CWSS notion under its canonical names at `Extractor.TreeBased`, as shape instances of step 2b's generics — so no declaration here carries a proof of its own, and nothing migrates onto them yet (`lake build` stays green on the `*Classical` layer). * `Verifier.coordinateWiseSpecialSoundWith` / `coordinateWiseSpecialSound` / `coordinateWiseSpecialSoundWithEscape` / `coordinateWiseSpecialSoundEscape`, with `coordinateWiseSpecialSound_iff_exists`, the forgetful `toCWSS` / `toEscape`, the lossless lift `coordinateWiseSpecialSoundWith.withEscape`, `coordinateWiseSpecialSoundWithEscape_false_iff` and `coordinateWiseSpecialSoundWithEscape.mono` — each defined as the corresponding `Verifier.treeSpecialSound*` at `D.toShape`. * The six `OracleVerifier` mirrors, matching the `*Classical` layer's set exactly. * `CWSSStructure.toShape_arity_pos` — every CWSS shape branches (`arity i = ℓᵢ·(kᵢ-1)+1 > 0`). Nothing needs it yet; it is what discharges the positivity hypothesis the guarded-left append theorems gain in step 4a, at every CWSS call site. There is no CWSS-level shape-congruence transport to re-land: the only two transports are tree-level, and the CWSS append theorems consume those directly. Gates: `lake build` green (4149 jobs) with this step alone applied; all 17 declarations `#check`; `#print axioms` on the eight new theorems free of `sorryAx`; `lake env lean` on the file emits no messages. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`appendSplit` cuts a tree; sequential composition of extractors needs the inverse *on paths*. This lands that glue in `TranscriptTree/Composition.lean`, transcribed verbatim from the vendored prototype: * `LeafPath.embedRight` — a suffix tree's leaf path, viewed in the embedded appended tree; * `SplitData.gluePath` — a prefix leaf path plus a suffix leaf path, glued along the certificate; * `LeafPath.transport` / `fullTranscript_transport` — moving a path along `splitDataOfTree_src`; * `AppendSplit.gluePath` + `fullTranscript_gluePath` — the path-level recombination and the fact that the glued path reads exactly `p₁.fullTranscript ++ₜ p₂.fullTranscript`, with the transcript specs `LeafPath.transcript_embedRight` / `SplitData.transcript_gluePath` behind it. The glue is needed in one direction only — nothing ever *un-glues* a path, because extractors attribute no output statements — so it stays an ordinary structural recursion and runs at runtime inside every composed extractor. `docs/plans/prototypes/CM_append.lean` loses its Part A in the same commit: the prototype imports the library, so the copy would now collide. Its Parts B–F still exercise the glue, which makes them evidence for *this* code — the 2-fold and 3-fold chain demos (`some 11`, `some 211`, kernel-`rfl`) and the prototype IR gate now run against these declarations. Gates: `lake build` green (4149 jobs); `lake env lean` on the file emits no messages; `IR PRESENT` on `LeafPath.embedRight`, `SplitData.gluePath`, `LeafPath.transport`, `AppendSplit.gluePath` and the two decisive `def probe := @X` probes; `#print axioms` on the four glue theorems free of `sorryAx`; all four vendored prototypes reproduce their expected output. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Fills the M3 row of §11 with the real gate output (entry probes, the per-step builds, the `IR PRESENT` lines and axiom prints, the four prototype re-runs, `./scripts/validate.sh`) and records four session-global facts: `linter.style.longLine` counts codepoints rather than bytes; a prototype declaration that moves into the library must lose its prototype copy in the same commit (4a will hit this for `somePath`); and M2 step 2b was still uncommitted when M3 started. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…p 4a) Compose the *named* extractors of both factors, at the witness-only notion landed in M2/M3. * `ChallengeTree.somePath` — some leaf path of any positively-branching tree, beside `onlyPath`; the guarded appends' probe for "the suffix tree is inhabited". * `Verifier.support_init_nonempty_of_prob_one` / `not_accepting_of_failure` — the transcript-level forms of the acceptance facts, so a rejecting guard branch can be refuted from one leaf. * `Extractor.TreeBased.append verify₁ E₁ E₂` — the composed extraction algorithm: the left extractor on the prefix tree, fed per prefix leaf with the right extractor's output on the suffix tree below it, at the statement the left verifier's verdict function names. `AppendSplit.gluePath` is the only path machinery on its runtime path. * `Verifier.append_run_outputs` and the five guarded seam lemmas (`append_run_guardedLeft`, `append_run_outputs_guardedLeft`, `outputs_guarded_subsingleton`, `guarded_accepting_of_mem`, `guarded_verdict_mem_outputs`) — the `Outputs`-level bridges that carry leaf-witnessing validity across a seam. * The four composition theorems — `append_treeSpecialSoundWith{,Escape}` and their `_guardedLeft` twins — with their CWSS and `OracleVerifier` wrappers. Prefix acceptance is established by running the *right* certificate at the canonical witnessing, which licenses the left one; the guarded twins add one move in front, that every prefix guard already passes. * `Verifier.GuardedForm.append` — guardedness data composes; its `verify_eq` is where `IsGuarded.append`'s `sorry` now lives, and `IsGuarded.append` is proved from it. The escape-threaded guarded append — until now the development's fundamental sorried obligation — is **proved** in its retyped form, at the unchanged `ChallengeTree.EscapeEvent.append`. The guarded theorems gain the positivity hypothesis `∀ i, 0 < S₂.arity i`, discharged at every CWSS call site by `CWSSStructure.toShape_arity_pos`. Milestone M4 step 4a of docs/plans/computable-cwss-extractors.md. Additive: the `*Classical` layer is untouched, so every consumer stays green.

Re-land the 2x2 package lattice under its canonical names, at the new extractor and notion: `CWSSPackage`, `GCWSSPackage`, `EscapeCWSSPackage`, `EscapeGCWSSPackage`, with the same field *names* as their `*Classical` predecessors and two retyped fields: * `extractor : Extractor.TreeBased …` — a leaf witnessing in, `Option` out; * `isPure : verifier.PureForm` / `isGuarded : verifier.GuardedForm` — purity and guardedness **as data**. This is the one field whose kind changes, and it is what keeps composition computable: the composed `extractor` and `esc` read the seam verdict off `L₁.isPure.verify` (resp. `L₁.isGuarded.out`) instead of laundering it out of a `Prop` with `Classical.choice`. The sixteen appends, the four lattice lifts and the `▷` elaborator follow. `▷` now carries two dispatch tables: two outgoing factors compose on the outgoing one, so an un-migrated definition keeps its ascribed type, and every other combination composes canonically, lifting an outgoing factor with `ofClassical`. That is how a half-migrated chain stays composable — at the cost of being `noncomputable`, since the lift fills the purity field with choice, which is why migrating a consumer rather than lifting it is what buys computability. The escape layer is untouched: `EscapeEvent.append` still takes the left verdict map as its index. Milestone M4 step 4b of docs/plans/computable-cwss-extractors.md.

…p 1) Replace `SingleRound.treeExtractor` with the computable witness-only engine: it reads the per-branch responses off the leaf witnessing at `branchPathOf` paths and `collect`s them into `mkWitness`, instead of inverting `relOut` by choice. No `[Nonempty WitOut]`, no relation argument, no `Classical`. New: `lastPathAux` / `chalPathAux` / `branchPathOf` (+ `fullTranscript_branchPathOf`, by bare `rfl` on the star tree), the `Option`-traverse `collect` with `collect_eq_some`, the extraction core `collect_branch_data`, and both canonical certificates `coordinateWiseSpecialSoundWith{,Escape}_of_mkWitness` at TODAY's `hpure`/`hmk` and the UNCHANGED `escEvent`. The validity premise collapses through purity (`LeafWitnesses.isValid_iff_pure`), so `hmk` is unchanged; the escape disjunction is decided before any witnessing is seen. The classical engine survives as `treeExtractorClassical` under an explicit outgoing header, carrying its two `*Classical_of_mkWitness` certificates, until M8 migrates `QuadEval`; the three sites there are repointed accordingly.

…kage (M5 steps 2-3) `ScalarRound`: the `(l = 1, k)` transplant of step 1 — the branch paths, the witness-only `treeExtractorScalar` (reusing `SingleRound.collect`), the scalar `collect_branch_data`, and both canonical certificates at the unchanged `escEventScalar`, with `hmk` at `Function.Injective fam`. The classical engine survives as `treeExtractorScalarClassical` with its two outgoing certificates. `CommittedScalar`: the delegate and the package move to the canonical types — `treeExtractor` (no longer parameterized by `checkAt`, since the openings come from the witnessing), `coordinateWiseSpecialSoundWithEscape`, `package` at `EscapeCWSSPackage` with `isPure` at the new `verifierPureForm` data. The file-wide `noncomputable section` is DELETED: the only noncomputable declarations left are the two outgoing twins `treeExtractorClassical` and `packageClassical`, which now carry per-declaration markers so no later computability sweep can miss them. `RingSwitching/Lift/Reduction.lean` is repointed at the outgoing delegate until M6 migrates it.

…implications (M5 steps 4-6) `NoChallenge`: the three bridges at the canonical notion. Their extractor `fun stmtIn tree _ => some (e stmtIn tree.onlyPath.fullTranscript)` ignores its leaf witnessing, so they carry no purity hypothesis and the validity premise is unused — this is the *closing* shape, the factor that lets a composed extractor run as a function of `(stmtIn, tree)` alone. `SpecialSoundness`: `Verifier.specialSound` / `OracleVerifier.specialSound` re-introduced with their same defining equations, now resolving to the witness-only `treeSpecialSound`, plus `Verifier.specialSound.old_of_new` — the textbook reading recovered unconditionally, with the extractor closed at `ChallengeTree.canonWitnesses` and the conclusion written out so it outlives the shim. Costs `[Inhabited WitIn]` and nothing else. `Implications`: the CWSS-generalizes-SS bridges at the canonical notions, with outgoing twins for the total-extractor forms. Both files' `noncomputable section`s are deleted; they compile clean without them.

`CM_m5demo.lean` runs entirely against the landed library: a real `CWSSPackage` at `SingleRound.treeExtractor` / `coordinateWiseSpecialSoundWith_of_mkWitness`, composed through the canonical `▷` with a synthetic zero-round closing package from `coordinateWiseSpecialSoundWith_of_isEmpty_challengeIdx`. `chain.extractor 3 T (fun _ => none)` evaluates to `some 17` — at the CONSTANT- `none` top-level witnessing, so a chain closed by a terminal link demonstrably runs as a computable function of `(stmtIn, tree)` alone — and `(3, 17) ∈ chain.relIn` holds by `rfl`. The open engine declines (`none`) rather than inventing junk; the composed seam verdict reads the transcript at runtime. All kernel-`rfl`-checked, with fourteen `IR PRESENT` gates and four decisive probes outside any `noncomputable section`.

…p 1) Transcribe `CM_enginecerts.lean` Part B (E17) into `ReduceClaim`, for both the reduction and the oracle-reduction variant: * `treeExtractor` / `oracleTreeExtractor` become the witness-only engines `fun s tree o => (o tree.onlyPath).map (mapWitInv s)` — computable and `Classical.choice`-free (`[propext, Quot.sound]`), matching the prototype's `CMEngines.rcTreeExtractor` byte-for-byte. The zero-round tree carries no information, so the output witness the classical version had to invent by inverting `relOut` now arrives on the leaf witnessing. `ReduceClaim` is an *open* link: it declines exactly when its witnessing declines. * Both certificates are proved directly at the new notion, consuming validity through `LeafWitnesses.isValid_iff_pure` at the verifier's verdict — the no-challenge bridge no longer applies, since the extractor now reads `o`. `[Nonempty WitIn]` is dropped from all four declarations. The classical pair survives as the explicitly-labelled outgoing `treeExtractorClassical` / `verifier_coordinateWiseSpecialSoundWithClassical`, because the seven Hachi package literals that name it are `*PackageClassical`- typed and so demand `Extractor.TreeBasedClassical`; those sites are repointed here and M8 retires the twins with the packages. The oracle pair needs no twin — nothing outside this file names it. IR gate: `IR PRESENT` on both engines and on the two §9-note-1 decisive probes.

Move `CheckClaim`, `SendClaim` and `SendWitness`/`SendSingleWitness`'s CWSS theorems onto the canonical no-challenge bridges. Statement-only migrations, as the plan predicts: the extractors become `fun _ _ _ => some ()` and `fun _ tree _ => some (tree.onlyPath.fullTranscript 0)`, and every proof body survives untouched — each ends `have h := …; exact h`, and `exact` absorbs the beta-redex the canonical bridge introduces. All four extractors are witnessing-agnostic: they read the transcript and never consult their leaf witnessing. That is the *closing* shape — a factor of this kind on the right of a chain is what lets the composed extractor run on `(stmtIn, tree)` alone. The docstrings now say so.

`RingSwitching.Lift.treeExtractor` and `.package` move to the canonical witness-only types and **drop their `noncomputable` markers**: both of their roots are gone — `ScalarRound`'s engine (M5) and the presentation data (M1) — so the markers come off unconditionally. `IR PRESENT` on both, and on the two §9-note-1 decisive probes. * `treeExtractor` delegates to the witness-only `CommittedScalar.treeExtractor` and therefore loses its `φF getM getY sideCond` arguments: the branch openings come from the leaf witnessing, so nothing reads `checkAt` any more. * `package`'s purity field is now `CommittedScalar.verifierPureForm K` — the verdict as data, which is what makes the composed seam computable. The classical trio survives as the explicitly-labelled outgoing `treeExtractorClassical` / `coordinateWiseSpecialSoundWithEscapeClassical` / `packageClassical`, because Hachi's `liftPackage` is still `EscapeCWSSPackageClassical`-typed; it is repointed here and M8 retires the twins with the package.

Fill §11's M6 row with the milestone's actual gate output, add the two session-global facts it established (the outgoing-twin rule, and that a witness-only retype shrinks signatures), and amend M8's entry probe: M6 could not vacate `*Classical` from `ReduceClaim.lean`, so the old probe is unsatisfiable and would have made an M8 session stop under §7 protocol step 2. M8's section now names the five twins it must delete when it repoints Hachi.

The `*Classical` layer introduced in M2 step 2a existed only to keep `lake build` green while consumers migrated to the witness-only extractor notion. M5-M8 moved every consumer onto the canonical names, so the twins are now consumer-free and D3's time-boxed removal fires. Deleted: * `Extractor.TreeBasedClassical`, the eight `Verifier.treeSpecialSound*Classical` / `coordinateWiseSpecialSound*Classical` notions, the four `OracleVerifier` mirrors and both `specialSoundClassical`s; * every forgetful/transport twin (`toCWSSClassical`, `toEscapeClassical`, `toTreeSpecialSoundClassical`, `*_iff_exists`, `*_congr`, `monoClassical`, `withEscapeClassical`, `*_false_iff`); * the four `*PackageClassical` structures with their 16 appends, `toGuardedClassical` and `toEscapeClassical`; * every certificate-producing twin, including the sorried `append_coordinateWiseSpecialSoundWithEscapeClassical_of_guardedLeft` whose canonical restatement M4 proved -- so the CWSS core comes out with one fewer `sorry`; * M5's four extra outgoing engines, both `Implications` bridges, the four `ofClassical` package lifts, `Extractor.TreeBased.ofClassical`, the two `new_of_old` shims, `Verifier.pureFormOfIsPure` and `Verifier.guardedFormOfIsGuarded` (neither had an organic use left); * the `▷` elaborator's second dispatch table and its lift machinery (`univAppendFn`, `canonLiftOf`, `liftFactor`), leaving one 16-entry `canonAppendFn` over the canonical packages. The kind-marked synonyms `▷ᵍ`, `▷ₑ`, `▷ₑᵍ` are repointed to the canonical appends. `TranscriptTree/NonVacuity.lean` keeps the total-extractor shape as a `private def TotalExtractor`: its G0 kill is a statement *about* that shape, so the shape has to outlive the shim. `docs/plans/prototypes/CM_gates.lean` gets the same treatment, per the standing rule that a milestone touching a declaration the prototypes import patches them in the same commit. Gates: `Build completed successfully (4149 jobs)`; `rg -oN '[A-Za-z_][A-Za-z_0-9.]*Classical\b' ArkLib/` returns nothing; the inventory probe logs `TOTAL noncomputable over the CWSS surface: 0` (baseline: 20); 36 `IR PRESENT` lines with `MISSING IR: 0` over the packages, engines and all 17 Hachi chains, plus 16 decisive `def probe := @X` outside any `noncomputable section`; all five vendored prototypes green with no `sorryAx`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Closes the plan's docs contract. `docs/wiki/repo-map.md`: the `TranscriptTree` entry now describes the witness-only extractor, leaf witnessings and their validity, the `canonWitnesses` closer, and `NonVacuity` as the standing regression gate; the `Guarded` entry records that both guarded binary CWSS appends are proved and that the file's one remaining `sorry` is `GuardedForm.append`'s `verify_eq`. `docs/skills/make-computable.md`: a new "Widening an interface" section carrying the durable lesson -- *architectural* means the interface is wrong, and an interface is something you can change -- with the three recurring shapes (a missing argument; a `Prop`-valued field a consumer must read as data; a kept `Type`-valued binder holding noncomputable data) and the two facts that shape such a job. `docs/plans/computable-cwss-extractors.md` and `docs/plans/README.md` flip to **landed**, and the M9 row records the gate output. `docs/plans/prototypes/README.md` notes that `TranscriptTree/NonVacuity.lean` is now the living copy of the gates. Validation: `./scripts/validate.sh --docs` passes (`All requested validation checks passed.`, 8570 jobs, 325 imports, docs integrity and KB lint green). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…gleton `Finset.prod_eq_mul_prod_diff_singleton` was deprecated in Mathlib on 2026-06-03 in favour of `Finset.prod_eq_mul_prod_sdiff_singleton`. The old name is a plain `alias`, so the rename is a drop-in with no proof changes. The deprecation warning lands under `ArkLib/Data/`, where the zero-warning budget in `scripts/check-warning-log.py` treats any non-`sorry` warning as an error. That failed the `Time validation wrapper` CI step on every branch, including `main`, from 4f38691 (#534) onward. Verified locally: `lake build` completes clean and `./scripts/validate.sh` exits 0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

make extractors computable (mostly QuadEval)

03c95a9

tobias-rothmann and others added 23 commits August 10, 2026 09:47

milestone 2

76a3d1e

docs(plans): record M2 green in the computable-extractor execution log

424eddf

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

docs(plans): record M4 green in the computable-extractor execution log

febc6c2

docs(plans): record M5 green in the computable-extractor execution log

0954e0b

milestones 7 and 8

2fbba2f

tobias-rothmann mentioned this pull request Aug 10, 2026

feat(Hachi): formalize lemma 10 of the paper #656

Merged

tobias-rothmann and others added 3 commits August 10, 2026 20:08

clean-up

06085a1

Merge branch 'main' into tr/computable-extractors

fc6b8a4

tobias-rothmann marked this pull request as ready for review August 10, 2026 18:54

tobias-rothmann requested review from ErVinuelas and alexanderlhicks August 10, 2026 19:24

tobias-rothmann and others added 4 commits August 11, 2026 16:34

Merge origin/main into tr/computable-extractors

0eacf32

clean-up

f71ce7e

Merge branch 'main' into tr/computable-extractors

b144e23

Merge branch 'main' into tr/computable-extractors

3c72749

Navigation Menu

Uh oh!

feat(Hachi): make extractors computable - #697

feat(Hachi): make extractors computable #697
tobias-rothmann wants to merge 33 commits into
mainfrom
tr/computable-extractors

tobias-rothmann commented Aug 6, 2026

Uh oh!

github-actions Bot commented Aug 6, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Aug 6, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

tobias-rothmann commented Aug 6, 2026

Uh oh!

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

Uh oh!

🤖 PR Summary

Hachi extractors made fully computable; documentation and axiom baseline updated accordingly.

Mathematical Formalization

Known Gaps / Remaining sorrys

Documentation (No code changes)

Infrastructure / CI

Architectural Note

Uh oh!

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

Uh oh!

Build Timing Report

Incremental Rebuild Signal

Slowest Current Clean-Build Files

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions Bot commented Aug 6, 2026 •

edited

Loading

Known Gaps / Remaining `sorry`s

github-actions Bot commented Aug 6, 2026 •

edited

Loading