Skip to content

LinearCodes

Directory actions

More options

Directory actions

More options

Latest commit

 

History

History

LinearCodes

README.md

LinearCodes

A Lean 4 library for linear codes and the BCGM25 mutual correlated-agreement (MCA) framework, including a runnable Reed-Solomon encoder and machine-checked security bounds for the IOP-based SNARK family (FRI, STIR, WHIR, WARP).

import LinearCodes

A three-snippet tour (encode a message, read security bounds, plug into a STIR profiler) lives at doc/getting-started.md.

What's in the box

  • LinearCode typeclass (LinearCode.lean) — encode, messageLen, codeLen, minimumDistance, johnsonRadius, mcaProximityGapError (gated by a ProximityRegime: .proven or .conjectured). Every instance must discharge a typeclass-level mcaProximityGapError_in_unit_interval obligation — instances cannot return garbage.
  • Reed-Solomon code (ReedSolomon.lean) — Horner-loop encoder, fully computable, no FftField requirement. Seven formal properties proved in ReedSolomonProperties.lean: encode_size, encode_add, encode_smul, encode_min_distance, encode_injective, johnson_list_decoding_radius, plus the keystone bridge to Polynomial.eval.
  • BCGM25 MCA framework (MCA/) — Theorems 6.1 (unique decoding), 6.2 (list decoding), and 9.2 (Reed-Solomon, Johnson regime) proved end-to-end at the integer-tight BCH+25 bound.
  • GS-sharpened RS bridge (MCA/RS/) — Array F ↔ Submodule F (Fin n → F) plumbing, squared-Johnson list-decoding certificate, and the canonical case-(a) MCA theorem rs_MCA_caseA matching BCIKS18 Thm 1.2 / BCGM25 Thm 9.2.
  • STIR / WHIR / WARP application bridges in MCA/Applications/.

BCGM25 Mutual Correlated Agreement

The MCA/ tree formalizes the linear-code mutual correlated agreement (MCA) framework of Bordage, Chiesa, Guan, and Manzur (2025), Correlated agreement, revisited, IACR ePrint 2025/2051. BCGM25 unifies the correlated-agreement (CA) and mutual-correlated-agreement (MCA) bounds used by modern IOP-based SNARKs by reducing them to a single generator-level seed-probability bound, parameterized by a relaxation parameter γ and the minimum distance δ_C of the underlying linear code.

Status

  • Core BCGM25 + RS bridge: build clean, 0 sorry, 0 axioms across LinearCodes/ and Upstream/, enforced by CI. All Phase A (Theorem 6.1) and Phase B (Theorem 6.2) capstones are proved end-to-end, and the GS-sharpened Reed-Solomon bridge has landed.
  • Theorem map: see doc/paper-to-lean-map.md for the full paper-to-Lean correspondence.

Capstones

  • Phase A — unique-decoding regime (Theorem 6.1): MCA/Case2Capstone.lean → MCA_unique_decoding_bound. Bounds the seed probability of the MCA bad event by (max{n·γ, 1} + 1)·(ℓ−1) / |S| for any generator over a code with MinDistAtLeast c δ_C and γ·(ℓ+1) < δ_C / n. This is the integer-tight lossless bound of BCH+25 (eprint 2025/2055) Theorem 4.1, which Remark 2.5 proves matches an explicit adversarial saturation; BCGM25's stated max{n·γ, 1}·(ℓ−1) / |S| is the real-number form (sufficient only for the strict bad-seed shape Δ_x = 0, not the Lean shape Δ_x ≤ nγ). See doc/literature-survey-lemma-5-3.md and the concrete counterexample MCA/Lemma53Examples.lean.
  • Phase B — list-decoding regime (Theorem 6.2): MCA/ListDecoding/MCA.lean → MCA_list_decoding_bound. Strengthens the bound to L · (max{n·γ, 1} + 1)·(ℓ−1) / |S|, where each bad seed may admit up to L candidate codewords agreeing on the witness set.
  • Concrete application — STIR: MCA/Applications/STIR.lean → STIR_MCA_unique_decoding_bound, STIR_MutualCorrelatedAgreement, STIR_zeroEvading. Specializes the abstract MCA capstones to the univariate-powers generator G(x) = (1, x, x², …, xᵈ) used by STIR.

GS-sharpened Reed-Solomon bridge

MCA/RS/ is the bridge from the Array F-shaped Reed-Solomon implementation to the abstract Submodule F (Fin n → F) view used throughout the MCA capstones. It packages:

  • A function-form RS encoder (reedSolomonLinearMap, reedSolomonSubmodule) with min-distance, injectivity, dimension, and IsMDS proofs.
  • A squared-Johnson list-decodability witness: reedSolomonSubmodule_isListDecodable_johnson gives (τ, n²)-list- decodability whenever (n − τ)² > n · k.
  • The case-(a) combination generator rsGenerator F l = (1, α, α², …, αˡ) and a combine ↔ linComb bridge between the abstract Generator.combine and the concrete array-form linear combination.

The headline result is the sharper RS-MCA bound

theorem rs_MCA_list_decoding_bound :
  seedProb (fun α => MCA_bad_event α)
    ≤ (n² · (max (n·γ) 1 + 1) · l) / |F|

i.e. specializing Theorem 6.2 to RS replaces the abstract list size L with the Johnson list size n². As a consequence, the case-(a) field-size requirement sharpens from the loose (ℓ + 1) · 2^n (used when bounding L by the trivial 2^n) to (ℓ + 1) · n², which is the right order for realistic STIR/WHIR/WARP parameter regimes. The case-(a) RS-MCA theorem under this sharper hypothesis is rs_MCA_caseA in MCA/RS/, also discoverable as ReedSolomon.MCA.caseA.

For the full theorem-by-theorem map (including which sub-targets are landed and which are still in progress for the bridge), see doc/paper-to-lean-map.md.

Stability

The LinearCodes tree is in active development. Stability tiers for downstream consumers:

  • Stable (safe to depend on; breaking changes will be flagged in PRs): the LinearCode typeclass interface, the Reed-Solomon encoder (reedSolomonEncode), the seven proved RS properties (encode_size, encode_add, encode_smul, encode_min_distance, encode_injective, johnson_list_decoding_radius, plus the encoder ↔ Polynomial.eval bridge), and the BCGM25 capstones (MCA_unique_decoding_bound, MCA_list_decoding_bound, rs_MCA_caseA, rs_MCA_list_decoding_bound).
  • Recently landed (may evolve): theorem aliases (correlatedAgreement_*, reedSolomon_correlatedAgreement_*, ReedSolomon.MCA.*); the GS-sharpened RS-MCA bridge (MCA/RS/); the JohnsonListSize vs JohnsonListSizeWithSlack split. Public names are unlikely to change but exact theorem locations may move as the tree gets reorganised.
  • Research / not for downstream use: Research/ (capstone smoke-test scratch); the .conjectured branch of mcaProximityGapError (a capacity-regime placeholder, not machine-checked, gated on the open capacity-achieving proximity-gap conjecture); Generator.affineSpace general s ≥ 2 MDS proofs (the structural special cases for s ∈ {0, 1} and s = 2 ∧ |F| = 2 are landed; the general case is mathematically false in the current parameterisation — see MCA/ConcreteMDS.lean for discussion).

Module structure

Docs