lint: remove proof-system hotspot debt

[quangvdao]

Result

Removes real linter debt from six proof-system hotspots without suppressing diagnostics or weakening protocol/security statements:

• Batched FRI security
• FRIBinius core interaction
• Binary Basefold core interaction and steps
• Packing sumcheck and composed protocol security

The changes remove unused section/typeclass premises, replace proof-only Fintype assumptions with weaker Finite assumptions plus local instances, simplify dead proof branches, and make tactic dependencies explicit.

Validation

• guarded exact builds pass for all six changed targets
• target non-sorry lint diagnostics: 0 / 0 / 0 / 0 / 3 / 1
• the four residual diagnostics are the existing structurally captured [Nontrivial L] plus [IsDomain L] overlap; none are suppressed
• source admission-token count: 185 -> 184, solely because two nested sorry tokens in one already-unfinished declaration become one; the kernel-tainted declaration set is unchanged at 43, so this is not a closed proof gap
• examples remain 125; explicit axioms and native trust remain 0
• independent review-lean-formalization hard gate: no correctness or trust blocker

Exact guarded timings on the reviewed head were 1.60s, 1.67s, 1.73s, 1.51s, 2.17s, and 4.05s for the six targets respectively.

API note

Three packing security theorem types are logically generalized from proof-only Fintype/DecidableEq premises to Finite; ordinary callers are source-compatible because Fintype synthesizes Finite. Explicit @ or named-instance callers may need adjustment. No in-tree caller breaks.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: lint: remove proof-system hotspot debt

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

The PR reduces linter debt by removing unused typeclass assumptions and simplifying proofs across six proof-system hotspots, but also introduces several new sorry placeholders, which contradicts the PR body's claim of a net decrease in admissions. The overview below details the changes, including the new sorries, and notes the discrepancy.

---

Statistics

Metric	Count
📝 Files Changed	6
✅ Lines Added	170
❌ Lines Removed	165

---

Lean Declarations

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

• theorem finalSumcheckOracleVerifier_rbrKnowledgeSoundness {σ : Type} in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean moved from L1122 to L1104
• def finalSumcheckKStateProp {m : Fin (1 + 1)} in ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean moved from L650 to L671
• theorem finalSumcheckOracleVerifier_rbrKnowledgeSoundness {σ : Type} in ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean moved from L714 to L734
• theorem sumcheckFoldOracleVerifier_rbrKnowledgeSoundness : in ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean moved from L431 to L447
• lemma batchingCore_perfectCompleteness [Finite L] [Finite K] : in ArkLib/ProofSystem/RingSwitching/Packing/General.lean moved from L123 to L124
• theorem fullOracleReduction_perfectCompleteness [Finite L] [Finite K] : in ArkLib/ProofSystem/RingSwitching/Packing/General.lean moved from L136 to L141
• theorem fullOracleVerifier_rbrKnowledgeSoundness [Finite K] [IsDomain L] : in ArkLib/ProofSystem/RingSwitching/Packing/General.lean moved from L164 to L171
• theorem finalSumcheckOracleVerifier_rbrKnowledgeSoundness [IsDomain L] {σ : Type} in ArkLib/ProofSystem/RingSwitching/Packing/SumcheckPhase.lean moved from L478 to L475

---

sorry Tracking

✅ Removed: 1 `sorry`(s)

ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean (1)

• def foldKnowledgeStateFunction (i : Fin ℓ) : (L404)

---

📋 **Additional Analysis**

The diff makes several stylistic improvements but still contains significant violations of the ArkLib style guide. The most pervasive issues are the use of camelCase in theorem names (should be snake_case), missing docstrings on new definitions/theorems, and the use of fun ... => instead of fun ... ↦. Additional violations include inconsistent naming (e.g., fullInputRelation starts with uppercase), empty lines inside proofs/definitions, and failure to use where syntax for instances. Below is an exhaustive list organized by category.

---

📄 **Per-File Summaries**

• ArkLib/ProofSystem/BatchedFri/Security.lean: Removed [Fintype 𝔽] and [Nontrivial 𝔽] from the enclosing variable block, and eliminated the redundant [Fintype 𝔽] parameter from correlated_agreement_density. Added omit [Fintype 𝔽] in annotations before εC and fri_soundness to avoid carrying the now‑unused instance into those local contexts. Cleaned up the proofs of fin_equiv_coset, invertibleDomain, and f_succ' by removing unneeded simp invocations (finRangeTo.eq_1, Fin.ofNat_eq_cast, etc.) and reformatting some by blocks. The fullChallengeProtocol abbreviation was also reformatted for readability.
• ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean: This diff refines the simp invocations used in proof blocks throughout CoreInteractionPhase.lean, replacing broad simp [stmt, oStmt, Nat.zero_mod] calls with targeted simp only lists (e.g., adding Fin.coe_ofNat_eq_mod, add_zero, Fin.val_last, Fin.castSucc_mk, Fin.succ_mk, zero_mul, Fin.zero_eta, Message). These changes affect the two main theorem proofs—foldRelayOracleVerifier_rbrKnowledgeSoundness and foldCommitOracleVerifier_rbrKnowledgeSoundness—and the definitions nonLastBlockOracleVerifier, lastBlockOracleVerifier, sumcheckFoldOracleVerifier, nonLastBlockOracleReduction, lastBlockOracleReduction, and sumcheckFoldOracleReduction. In foldCommitOracleVerifier_rbrKnowledgeSoundness the simp block is simplified by removing Direction.not_P_to_V_eq_V_to_P and the subsequent omega call. Several all_goals try rfl lines are removed, and a case-by-case (have hi : … ; rw! … ; rfl) block is replaced with a direct apply OracleInterface.ext (or eliminated). No sorry or admit are introduced.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean: Several theorems had their typeclass requirements weakened: commitOracleVerifier_rbrKnowledgeSoundness now omits [CharP L 2] and [SampleableType L], relayOracleVerifier_rbrKnowledgeSoundness omits [SampleableType L], and finalSumcheckOracleVerifier_rbrKnowledgeSoundness omits [CharP L 2] and no longer requires [Fintype L]. In foldKnowledgeStateFunction, the toFun_full body was replaced with a single sorry, undoing a previous partial proof. The proof of an equality in commitOracleVerifier was refined to use simp with explicit lemmas (Sum.inl.injEq, Fin.mk.injEq) instead of a larger simp. The file also includes several cosmetic cleanups—removing blank lines, simplifying comments, and reformatting—that do not affect semantics.
• ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean: The diff reformats long type signatures across multiple declarations in CoreInteractionPhase.lean to break lines at consistent column positions, improving readability without changing any semantics. The affected items are def/instance/theorem headers and their associated type-parameter blocks for sumcheckFoldCtxLens, sumcheckFoldExtractorLens, sumcheckFoldCtxLens_complete, sumcheckFoldOracleReduction_perfectCompleteness, sumcheckFoldExtractorLens_rbr_knowledge_soundness, sumcheckFoldOracleVerifier_rbrKnowledgeSoundness, finalSumcheckProver, finalSumcheckVerifier, finalSumcheckOracleReduction, finalSumcheckRbrExtractor, finalSumcheckKStateProp, finalSumcheckKnowledgeStateFunction, finalSumcheckOracleVerifier_rbrKnowledgeSoundness, coreInteractionOracleVerifier, and coreInteractionOracleReduction. Additionally, the finalSumcheckVerifier implementation now removes two blank lines around intermediate let-bindings (let s'..., let eq_tilde_eval...). No sorry or admit is present in the diff.
• ArkLib/ProofSystem/RingSwitching/Packing/General.lean: The proof of batchingCore_perfectCompleteness and fullOracleReduction_perfectCompleteness were strengthened by adding [Finite L] [Finite K] typeclass hypotheses and deriving Fintype instances via Fintype.ofFinite, wrapping the proof body in classical blocks. The fullOracleVerifier_rbrKnowledgeSoundness theorem replaced the [SampleableType L] hypothesis with [Finite K] (keeping [IsDomain L]), added a Fintype instance derivation and classical block, and introduced a sorry in the proof, specifically in the second · branch of the batchInteractionRBRKS application, where the simp invocation was also simplified. The omit clauses were updated to include the new Fintype/DecidableEq requirements.
• ArkLib/ProofSystem/RingSwitching/Packing/SumcheckPhase.lean: The diff adds sorry placeholders for toFun_full in both iteratedSumcheckKnowledgeStateFunction and finalSumcheckKnowledgeStateFunction, and for the proofs of iteratedSumcheckOracleVerifier_rbrKnowledgeSoundness, finalSumcheckOracleVerifier_rbrKnowledgeSoundness, and coreInteraction_rbrKnowledgeSoundness. It also relaxes typeclass assumptions: [Fintype L], [Fintype K], and [DecidableEq K] are removed as assumptions from several theorems, using classical and local DecidableEq K instances to replace them. Additionally, the diff makes minor simplifications to simp sets and removes some blank lines.

---

Last updated: 2026-09-01 01:29 UTC.

[github-actions]

Build Timing Report

• PR head: baf9bde
• Message: lint: remove proof-system hotspot debt
• Ref: lint/proof-system-hotspots-round2
• Measured checkout: 8ff278e (workflow head baf9bde).
• Comparison baseline: 5b263f4 from exact PR base on main.
• Runner: current ubuntu24 20260823.283.1, X64, 4 cores.
• Dependency cache: current exact hit (Linux-lean-ci-81c9e391567908d0b6843f0e97e3c9c3b2a3300432c3223762c9257acdda85b7); manifest 01cba20b029e.
• Baseline environment: runner ubuntu24 20260823.283.1, X64, 4 cores; dependency cache exact hit (Linux-lean-ci-81c9e391567908d0b6843f0e97e3c9c3b2a3300432c3223762c9257acdda85b7); manifest 01cba20b029e.
• Measured on the pinned ubuntu-24.04 runner with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; native build lake build toyproblem-runtime hachi-runtime; validation wrapper ./scripts/validate.sh.
• The rows run in order against one tree, so native build and validation wrapper both measure an already-built project: validation wrapper is the cost of the gate itself, not of a cold ./scripts/validate.sh. CI passes it no flags, so --lint, --docs, --site and --axioms contribute nothing.

Measurement	Base wall (s)	Current wall (s)	Wall change	Base CPU (s)	Current CPU (s)	CPU change	Status
Clean build	898.65	894.97	-3.68 (-0.4%)	3480.41	3478.07	-2.34 (-0.1%)	ok
Warm rebuild	2.51	2.39	-0.12 (-4.8%)	3.99	3.14	-0.85 (-21.3%)	ok
Native build	29.61	27.78	-1.83 (-6.2%)	94.65	87.90	-6.75 (-7.1%)	ok
Validation wrapper	13.10	11.98	-1.12 (-8.5%)	17.83	15.17	-2.66 (-14.9%)	ok

CPU work is user + sys. Compare it with wall time to distinguish changed compilation work from runner scheduling noise; neither metric is a standalone performance verdict.

Incremental Rebuild Signal

• Warm rebuild saved 892.58s vs clean (374.46x 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
45	41	+4	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
39	37	+2	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
38	40	-2	ArkLib/Data/CodingTheory/ProximityGap/CapacityBounds/Frs.lean
37	33	+4	ArkLib/Data/CodingTheory/SubspaceDesign.lean
34	35	-1	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
33	30	+3	ArkLib/Data/CodingTheory/ProximityGap/CapacityBounds/Subfield.lean
32	31	+1	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
31	28	+3	ArkLib/Data/CodingTheory/JohnsonBound/Family.lean
30	27	+3	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
30	27	+3	ArkLib/Data/CodingTheory/ProximityGap/CapacityBounds/Entropy.lean
30	30	+0	ArkLib/Data/CodingTheory/ProximityGap/CapacityBounds/Powers.lean
30	29	+1	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
29	26	+3	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
29	25	+4	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
28	28	+0	ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
26	27	-1	ArkLib/ProofSystem/Stir/Combine.lean
25	19	+6	ArkLib/ProofSystem/Fri/Spec/SingleRound.lean
24	23	+1	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/JointAgreement.lean
23	23	+0	ArkLib/Data/CodingTheory/ListDecodability/Bounds/KKH26.lean
23	20	+3	ArkLib/Data/CodingTheory/ListDecodability/Bounds/LargeAlphabet/Basic.lean