Guruswami-Sudan Concrete Implementations

Named concrete dense-interpolation/Roth-Ruckenstein implementations and correctness theorem specializations for the implementations exercised by the benchmark suite.

def CompPoly.GuruswamiSudan.koalaBearDenseInterpContext : GSInterpContext KoalaBear.Field

Dense interpolation backend over canonical KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearDenseInterpContext : GSInterpContext KoalaBear.Fast.Field

Dense interpolation backend over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearNttFastMulContext : CPolynomial.MulContext KoalaBear.Field

NTTFast-backed univariate multiplication over canonical KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearNttFastLowMulContext : PolynomialMatrix.MulLowContext KoalaBear.Field

NTTFast-backed low univariate multiplication over canonical KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearNttFastModContext : CPolynomial.ModContext KoalaBear.Field

NTTFast-backed univariate monic remainders over canonical KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearNttFastBatchEvalContext : CPolynomial.BatchEvalContext KoalaBear.Field

NTTFast-backed subproduct batch evaluation over canonical KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearNttFastMulContext : CPolynomial.MulContext KoalaBear.Fast.Field

NTTFast-backed univariate multiplication over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearNttFastLowMulContext : PolynomialMatrix.MulLowContext KoalaBear.Fast.Field

NTTFast-backed low univariate multiplication over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearNttFastModContext : CPolynomial.ModContext KoalaBear.Fast.Field

NTTFast-backed univariate monic remainders over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearNttFastBatchEvalContext : CPolynomial.BatchEvalContext KoalaBear.Fast.Field

NTTFast-backed subproduct batch evaluation over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearLeeDirectInterpContext : GSInterpContext KoalaBear.Field

Lee-O'Sullivan interpolation over canonical KoalaBear with direct vanishing setup.

def CompPoly.GuruswamiSudan.koalaBearLeeSubproductInterpContext : GSInterpContext KoalaBear.Field

Lee-O'Sullivan interpolation over canonical KoalaBear with subproduct-tree vanishing setup.

def CompPoly.GuruswamiSudan.fastKoalaBearLeeDirectInterpContext : GSInterpContext KoalaBear.Fast.Field

Lee-O'Sullivan interpolation over native-word fast KoalaBear with direct vanishing setup.

def CompPoly.GuruswamiSudan.fastKoalaBearLeeSubproductInterpContext : GSInterpContext KoalaBear.Fast.Field

Lee-O'Sullivan interpolation over native-word fast KoalaBear with subproduct-tree vanishing setup.

def CompPoly.GuruswamiSudan.approximantPMBasisLeafCutoff : ℕ

PM-basis scalar-kernel cutoff for the approximant-basis interpolation backend.

The recursive solver handles all larger orders with low-product residuals and block matrix composition; dense scalar linear algebra is reserved for small bounded leaves.

def CompPoly.GuruswamiSudan.approximantPMBasisComposeLeafCutoff : ℕ

Polynomial-matrix basis-composition cutoff for the approximant backend. The current GS interpolation shapes are narrow enough that direct bounded composition is faster than recursing Strassen down to unit blocks.

def CompPoly.GuruswamiSudan.koalaBearApproximantPMBasisContext : PolynomialMatrix.Approximant.PMBasisContext KoalaBear.Field

Recursive approximant-basis PM-basis context over canonical KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearApproximantSolutionContext : PolynomialMatrix.Approximant.ModularSolutionBasisContext KoalaBear.Field

Diagonal modular-equation solution context over canonical KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearApproximantBasisDirectInterpContext : GSInterpContext KoalaBear.Field

Approximant-basis interpolation over canonical KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearApproximantBasisSubproductInterpContext : GSInterpContext KoalaBear.Field

Approximant-basis interpolation over canonical KoalaBear with subproduct-tree vanishing setup.

def CompPoly.GuruswamiSudan.koalaBearApproximantBasisInterpContext : GSInterpContext KoalaBear.Field

Default approximant-basis interpolation over canonical KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearApproximantPMBasisContext : PolynomialMatrix.Approximant.PMBasisContext KoalaBear.Fast.Field

Recursive approximant-basis PM-basis context over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearApproximantSolutionContext : PolynomialMatrix.Approximant.ModularSolutionBasisContext KoalaBear.Fast.Field

Diagonal modular-equation solution context over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearApproximantBasisDirectInterpContext : GSInterpContext KoalaBear.Fast.Field

Approximant-basis interpolation over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearApproximantBasisSubproductInterpContext : GSInterpContext KoalaBear.Fast.Field

Approximant-basis interpolation over native-word fast KoalaBear with subproduct-tree vanishing setup.

def CompPoly.GuruswamiSudan.fastKoalaBearApproximantBasisInterpContext : GSInterpContext KoalaBear.Fast.Field

Default approximant-basis interpolation over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.hybridReductionStepBudget (params : GSInterpParams) : ℕ

Mulders-Storjohann step budget for the hybrid interpolation backend: the ski-rental rent/buy break-even, set near the cost ratio between one approximant-fallback solve and one reduction step. Both scale with the input mass, so the ratio is proportional to ℓ^(ω−1) (with ℓ + 1 the module width) and independent of n and m under softly-linear multiplication; the constant is calibrated from the n = 5040 long-code benchmark shape.

def CompPoly.GuruswamiSudan.koalaBearHybridInterpContext : GSInterpContext KoalaBear.Field

Hybrid interpolation (budgeted Lee-O'Sullivan reduction with approximant fallback) over canonical KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearHybridInterpContext : GSInterpContext KoalaBear.Fast.Field

Hybrid interpolation (budgeted Lee-O'Sullivan reduction with approximant fallback) over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearRothRootContext : GSRootContext KoalaBear.Field

Roth-Ruckenstein root backend over canonical KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearRothNttFastRootContext : GSRootContext KoalaBear.Field

Roth-Ruckenstein root backend over canonical KoalaBear with NTTFast field roots.

def CompPoly.GuruswamiSudan.fastKoalaBearRothRootContext : GSRootContext KoalaBear.Fast.Field

Roth-Ruckenstein root backend over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearRothNttFastRootContext : GSRootContext KoalaBear.Fast.Field

Roth-Ruckenstein root backend over native-word fast KoalaBear with NTTFast field roots.

def CompPoly.GuruswamiSudan.koalaBearAlekhnovichRootContext : GSRootContext KoalaBear.Field

Alekhnovich root backend over canonical KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearAlekhnovichNttFastRootContext : GSRootContext KoalaBear.Field

Alekhnovich root backend over canonical KoalaBear with NTTFast field roots.

def CompPoly.GuruswamiSudan.fastKoalaBearAlekhnovichRootContext : GSRootContext KoalaBear.Fast.Field

Alekhnovich root backend over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearAlekhnovichNttFastRootContext : GSRootContext KoalaBear.Fast.Field

Alekhnovich root backend over native-word fast KoalaBear with NTTFast field roots.

def CompPoly.GuruswamiSudan.koalaBearDenseRothContext : GSFilteredCoreContext KoalaBear.Field

Filtered dense/Roth context over canonical KoalaBear.

def CompPoly.GuruswamiSudan.koalaBearDenseRothNttFastContext : GSFilteredCoreContext KoalaBear.Field

Filtered dense/Roth context over canonical KoalaBear with NTTFast field roots.

def CompPoly.GuruswamiSudan.fastKoalaBearDenseRothContext : GSFilteredCoreContext KoalaBear.Fast.Field

Filtered dense/Roth context over native-word fast KoalaBear.

def CompPoly.GuruswamiSudan.fastKoalaBearDenseRothNttFastContext : GSFilteredCoreContext KoalaBear.Fast.Field

Filtered dense/Roth context over native-word fast KoalaBear with NTTFast field roots.

theorem CompPoly.GuruswamiSudan.koalaBearDenseRothGsCore_sound {points : Array (KoalaBear.Field × KoalaBear.Field)} {params : GSInterpParams} {p : CPolynomial KoalaBear.Field} (hp : p ∈ (gsCore points koalaBearDenseInterpContext koalaBearRothRootContext params).toList) : ∃ (Q : CBivariate KoalaBear.Field), koalaBearDenseInterpContext.interpolate points params = some Q ∧ ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0

Concrete soundness for the canonical KoalaBear dense/Roth core.

theorem CompPoly.GuruswamiSudan.koalaBearDenseRothGsCore_complete_of_enough_matches {points : Array (KoalaBear.Field × KoalaBear.Field)} {params : GSInterpParams} {p : CPolynomial KoalaBear.Field} (hInterpExists : ∃ (Q : CBivariate KoalaBear.Field), ValidInterpolationWitness points params Q) (hpdeg : degreeLt p params.messageDegree) (hdistinct : DistinctXCoordinates points) (hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p) : p ∈ (gsCore points koalaBearDenseInterpContext koalaBearRothRootContext params).toList

Concrete completeness for the canonical KoalaBear dense/Roth core.

theorem CompPoly.GuruswamiSudan.koalaBearDenseRothGsFilteredCore_sound {points : Array (KoalaBear.Field × KoalaBear.Field)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial KoalaBear.Field} (hp : p ∈ (gsFilteredCore points koalaBearDenseInterpContext koalaBearRothRootContext params radius).toList) : ∃ (Q : CBivariate KoalaBear.Field), koalaBearDenseInterpContext.interpolate points params = some Q ∧ ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0 ∧ candidateMismatchCount points p ≤ radius

Concrete soundness for the canonical KoalaBear dense/Roth filtered core.

theorem CompPoly.GuruswamiSudan.koalaBearDenseRothGsFilteredCore_complete_of_enough_matches {points : Array (KoalaBear.Field × KoalaBear.Field)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial KoalaBear.Field} (hInterpExists : ∃ (Q : CBivariate KoalaBear.Field), ValidInterpolationWitness points params Q) (hpdeg : degreeLt p params.messageDegree) (hdistinct : DistinctXCoordinates points) (hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p) (hpass : passesCandidateDistance points radius p = true) : p ∈ (gsFilteredCore points koalaBearDenseInterpContext koalaBearRothRootContext params radius).toList

Concrete completeness for the canonical KoalaBear dense/Roth filtered core.

theorem CompPoly.GuruswamiSudan.koalaBearDenseRothNttFastGsCore_sound {points : Array (KoalaBear.Field × KoalaBear.Field)} {params : GSInterpParams} {p : CPolynomial KoalaBear.Field} (hp : p ∈ (gsCore points koalaBearDenseInterpContext koalaBearRothNttFastRootContext params).toList) : ∃ (Q : CBivariate KoalaBear.Field), koalaBearDenseInterpContext.interpolate points params = some Q ∧ ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0

Concrete soundness for the canonical KoalaBear dense/Roth-NTTFast core.

theorem CompPoly.GuruswamiSudan.koalaBearDenseRothNttFastGsCore_complete_of_enough_matches {points : Array (KoalaBear.Field × KoalaBear.Field)} {params : GSInterpParams} {p : CPolynomial KoalaBear.Field} (hInterpExists : ∃ (Q : CBivariate KoalaBear.Field), ValidInterpolationWitness points params Q) (hpdeg : degreeLt p params.messageDegree) (hdistinct : DistinctXCoordinates points) (hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p) : p ∈ (gsCore points koalaBearDenseInterpContext koalaBearRothNttFastRootContext params).toList

Concrete completeness for the canonical KoalaBear dense/Roth-NTTFast core.

theorem CompPoly.GuruswamiSudan.koalaBearDenseRothNttFastGsFilteredCore_sound {points : Array (KoalaBear.Field × KoalaBear.Field)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial KoalaBear.Field} (hp : p ∈ (gsFilteredCore points koalaBearDenseInterpContext koalaBearRothNttFastRootContext params radius).toList) : ∃ (Q : CBivariate KoalaBear.Field), koalaBearDenseInterpContext.interpolate points params = some Q ∧ ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0 ∧ candidateMismatchCount points p ≤ radius

Concrete soundness for the canonical KoalaBear dense/Roth-NTTFast filtered core.

theorem CompPoly.GuruswamiSudan.koalaBearDenseRothNttFastGsFilteredCore_complete_of_enough_matches {points : Array (KoalaBear.Field × KoalaBear.Field)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial KoalaBear.Field} (hInterpExists : ∃ (Q : CBivariate KoalaBear.Field), ValidInterpolationWitness points params Q) (hpdeg : degreeLt p params.messageDegree) (hdistinct : DistinctXCoordinates points) (hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p) (hpass : passesCandidateDistance points radius p = true) : p ∈ (gsFilteredCore points koalaBearDenseInterpContext koalaBearRothNttFastRootContext params radius).toList

Concrete completeness for the canonical KoalaBear dense/Roth-NTTFast filtered core.

theorem CompPoly.GuruswamiSudan.fastKoalaBearDenseRothGsCore_sound {points : Array (KoalaBear.Fast.Field × KoalaBear.Fast.Field)} {params : GSInterpParams} {p : CPolynomial KoalaBear.Fast.Field} (hp : p ∈ (gsCore points fastKoalaBearDenseInterpContext fastKoalaBearRothRootContext params).toList) : ∃ (Q : CBivariate KoalaBear.Fast.Field), fastKoalaBearDenseInterpContext.interpolate points params = some Q ∧ ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0

Concrete soundness for the fast KoalaBear dense/Roth core.

theorem CompPoly.GuruswamiSudan.fastKoalaBearDenseRothGsCore_complete_of_enough_matches {points : Array (KoalaBear.Fast.Field × KoalaBear.Fast.Field)} {params : GSInterpParams} {p : CPolynomial KoalaBear.Fast.Field} (hInterpExists : ∃ (Q : CBivariate KoalaBear.Fast.Field), ValidInterpolationWitness points params Q) (hpdeg : degreeLt p params.messageDegree) (hdistinct : DistinctXCoordinates points) (hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p) : p ∈ (gsCore points fastKoalaBearDenseInterpContext fastKoalaBearRothRootContext params).toList

Concrete completeness for the fast KoalaBear dense/Roth core.

theorem CompPoly.GuruswamiSudan.fastKoalaBearDenseRothGsFilteredCore_sound {points : Array (KoalaBear.Fast.Field × KoalaBear.Fast.Field)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial KoalaBear.Fast.Field} (hp : p ∈ (gsFilteredCore points fastKoalaBearDenseInterpContext fastKoalaBearRothRootContext params radius).toList) : ∃ (Q : CBivariate KoalaBear.Fast.Field), fastKoalaBearDenseInterpContext.interpolate points params = some Q ∧ ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0 ∧ candidateMismatchCount points p ≤ radius

Concrete soundness for the fast KoalaBear dense/Roth filtered core.

theorem CompPoly.GuruswamiSudan.fastKoalaBearDenseRothGsFilteredCore_complete_of_enough_matches {points : Array (KoalaBear.Fast.Field × KoalaBear.Fast.Field)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial KoalaBear.Fast.Field} (hInterpExists : ∃ (Q : CBivariate KoalaBear.Fast.Field), ValidInterpolationWitness points params Q) (hpdeg : degreeLt p params.messageDegree) (hdistinct : DistinctXCoordinates points) (hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p) (hpass : passesCandidateDistance points radius p = true) : p ∈ (gsFilteredCore points fastKoalaBearDenseInterpContext fastKoalaBearRothRootContext params radius).toList

Concrete completeness for the fast KoalaBear dense/Roth filtered core.

theorem CompPoly.GuruswamiSudan.fastKoalaBearDenseRothNttFastGsCore_sound {points : Array (KoalaBear.Fast.Field × KoalaBear.Fast.Field)} {params : GSInterpParams} {p : CPolynomial KoalaBear.Fast.Field} (hp : p ∈ (gsCore points fastKoalaBearDenseInterpContext fastKoalaBearRothNttFastRootContext params).toList) : ∃ (Q : CBivariate KoalaBear.Fast.Field), fastKoalaBearDenseInterpContext.interpolate points params = some Q ∧ ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0

Concrete soundness for the fast KoalaBear dense/Roth-NTTFast core.

theorem CompPoly.GuruswamiSudan.fastKoalaBearDenseRothNttFastGsCore_complete_of_enough_matches {points : Array (KoalaBear.Fast.Field × KoalaBear.Fast.Field)} {params : GSInterpParams} {p : CPolynomial KoalaBear.Fast.Field} (hInterpExists : ∃ (Q : CBivariate KoalaBear.Fast.Field), ValidInterpolationWitness points params Q) (hpdeg : degreeLt p params.messageDegree) (hdistinct : DistinctXCoordinates points) (hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p) : p ∈ (gsCore points fastKoalaBearDenseInterpContext fastKoalaBearRothNttFastRootContext params).toList

Concrete completeness for the fast KoalaBear dense/Roth-NTTFast core.

theorem CompPoly.GuruswamiSudan.fastKoalaBearDenseRothNttFastGsFilteredCore_sound {points : Array (KoalaBear.Fast.Field × KoalaBear.Fast.Field)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial KoalaBear.Fast.Field} (hp : p ∈ (gsFilteredCore points fastKoalaBearDenseInterpContext fastKoalaBearRothNttFastRootContext params radius).toList) : ∃ (Q : CBivariate KoalaBear.Fast.Field), fastKoalaBearDenseInterpContext.interpolate points params = some Q ∧ ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0 ∧ candidateMismatchCount points p ≤ radius

Concrete soundness for the fast KoalaBear dense/Roth-NTTFast filtered core.

theorem CompPoly.GuruswamiSudan.fastKoalaBearDenseRothNttFastGsFilteredCore_complete_of_enough_matches {points : Array (KoalaBear.Fast.Field × KoalaBear.Fast.Field)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial KoalaBear.Fast.Field} (hInterpExists : ∃ (Q : CBivariate KoalaBear.Fast.Field), ValidInterpolationWitness points params Q) (hpdeg : degreeLt p params.messageDegree) (hdistinct : DistinctXCoordinates points) (hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p) (hpass : passesCandidateDistance points radius p = true) : p ∈ (gsFilteredCore points fastKoalaBearDenseInterpContext fastKoalaBearRothNttFastRootContext params radius).toList

Concrete completeness for the fast KoalaBear dense/Roth-NTTFast filtered core.