Guruswami-Sudan Executable Decoder

Top-level executable API for the packed CompPoly Guruswami-Sudan decoder.

structure CompPoly.GuruswamiSudan.GSFilteredCoreContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] : Type u_1

Backend-parametric filtered core exposed as a reusable executable context.

The context packages an executable filtered decoder together with its CompPoly soundness and completeness contracts.

• run : Array (F × F) → GSInterpParams → ℕ → Array (CPolynomial F)
• sound {points : Array (F × F)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial F} : p ∈ (self.run points params radius).toList → ∃ (Q : CBivariate F), ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0 ∧ candidateMismatchCount points p ≤ radius
• complete {points : Array (F × F)} {params : GSInterpParams} {radius : ℕ} {p : CPolynomial F} : (∃ (Q : CBivariate F), ValidInterpolationWitness points params Q) → DistinctXCoordinates points → degreeLt p params.messageDegree → params.weightedDegreeBound < params.multiplicity * matchingPointCount points p → passesCandidateDistance points radius p = true → p ∈ (self.run points params radius).toList

def CompPoly.GuruswamiSudan.filteredCoreContextOfInterpRootContexts {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (interp : GSInterpContext F) (roots : GSRootContext F) : GSFilteredCoreContext F

Filtered-core context assembled from CompPoly interpolation and root backends.

structure CompPoly.GuruswamiSudan.GSReceivedWord (F : Type u_1) : Type u_1

Packed received word accepted by the executable decoder.

• points : Array (F × F)

@[instance_reducible]

instance CompPoly.GuruswamiSudan.instReprGSReceivedWord {F✝ : Type u_1} [Repr F✝] : Repr (GSReceivedWord F✝)

def CompPoly.GuruswamiSudan.instReprGSReceivedWord.repr {F✝ : Type u_1} [Repr F✝] : GSReceivedWord F✝ → ℕ → Std.Format

def CompPoly.GuruswamiSudan.GSReceivedWord.length {F : Type u_1} (w : GSReceivedWord F) : ℕ

Runtime length of a packed received word.

structure CompPoly.GuruswamiSudan.GSExecParams : Type

Explicit executable parameters for the parameterized decoder.

• interp : GSInterpParams
• radius : ℕ

def CompPoly.GuruswamiSudan.instReprGSExecParams.repr : GSExecParams → ℕ → Std.Format

@[instance_reducible]

instance CompPoly.GuruswamiSudan.instReprGSExecParams : Repr GSExecParams

@[instance_reducible]

instance CompPoly.GuruswamiSudan.instBEqGSExecParams : BEq GSExecParams

def CompPoly.GuruswamiSudan.instBEqGSExecParams.beq : GSExecParams → GSExecParams → Bool

@[instance_reducible]

instance CompPoly.GuruswamiSudan.instDecidableEqGSExecParams : DecidableEq GSExecParams

def CompPoly.GuruswamiSudan.instDecidableEqGSExecParams.decEq (x✝ x✝¹ : GSExecParams) : Decidable (x✝ = x✝¹)

def CompPoly.GuruswamiSudan.decodeWithParams {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (ctx : GSFilteredCoreContext F) (params : GSExecParams) (w : GSReceivedWord F) : Array (CPolynomial F)

Computable executable decoder with caller-supplied parameters.

structure CompPoly.GuruswamiSudan.GSParamSelector : Type

Parameter selector for the selector-backed executable decoder.

• choose : ℕ → ℕ → ℕ → Option GSExecParams

def CompPoly.GuruswamiSudan.decode {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (ctx : GSFilteredCoreContext F) (selector : GSParamSelector) (k e : ℕ) (w : GSReceivedWord F) : Array (CPolynomial F)

Selector-backed executable decoder with parameters selected from (k, w.length, e).