The optional external LLL provider. lll probes an @[extern] hook for an independent native reducer, marshals the basis, and certifies the returned candidate with certCheck; absence or rejection falls through to the exact lllNative path. The provider is acceleration only.

External LLL provider

Optional runtime hook for an external reducer (e.g. fpLLL) reached through the C FFI shim in HexLLL/ffi/. A provider is installed either by the explicit Lean loader Hex.lll.loadProvider (which dlopens a named shared library) or, for a provider linked into the process, by a one-shot static-symbol probe; there is no environment-variable read and no implicit dlopen. providerAvailable reports whether a provider is currently installed; when none is present, or a returned candidate fails validation, callers fall back to the verified native reducer lllNative. The provider is acceleration only and is never part of the trusted path — every candidate it returns is checked before use. See SPEC/hex-lll.md for the dispatch and certification details.

@[extern lean_hexlll_provider_available]

opaque Hex.Internal.LLLProvider.providerAvailable : Unit → Bool

@[extern lean_hexlll_provider_reduce]

opaque Hex.Internal.LLLProvider.providerReduce (rows cols : USize) (entries : Array String) (delta eta : Float) (method : UInt8) (withInverse : Bool) : Except String (Array Int)

@[extern lean_hexlll_load_provider]

opaque Hex.Internal.LLLProvider.loadProviderImpl (path : String) : IO Bool

Install the external provider from the shared library at path: dlopen the library, resolve lean_fplll_lll_reduce from it, and set the process provider slot. Returns true on success and false when the library cannot be loaded or the symbol is missing (the loader diagnostic is written to stderr). This is the raw FFI entry point behind the public Hex.lll.loadProvider.

structure Hex.Internal.LLLProvider.Candidate : Type

Decoded result returned by the external LLL provider.

reduced is the row-major reduced basis, transform is the row-major unimodular transformation matrix with transform * input = reduced, and inverse? is the optional row-major inverse transformation when the caller requested it.

• reduced : Array Int
• transform : Array Int
• inverse? : Option (Array Int)

def Hex.Internal.LLLProvider.instReprCandidate.repr : Candidate → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Hex.Internal.LLLProvider.instReprCandidate : Repr Candidate

Equations

• Hex.Internal.LLLProvider.instReprCandidate = { reprPrec := Hex.Internal.LLLProvider.instReprCandidate.repr }

def Hex.Internal.LLLProvider.instBEqCandidate.beq : Candidate → Candidate → Bool

Equations

• Hex.Internal.LLLProvider.instBEqCandidate.beq { reduced := a, transform := a_1, inverse? := a_2 } { reduced := b, transform := b_1, inverse? := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Hex.Internal.LLLProvider.instBEqCandidate.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Hex.Internal.LLLProvider.instBEqCandidate : BEq Candidate

Equations

• Hex.Internal.LLLProvider.instBEqCandidate = { beq := Hex.Internal.LLLProvider.instBEqCandidate.beq }

structure Hex.Internal.LLLProvider.Diagnostics : Type

Diagnostic counters for attempts to use the external LLL provider.

absent counts calls made when the provider is unavailable, providerError counts provider-level failures, rejected counts structurally invalid provider responses, and accepted counts responses decoded into a Candidate.

• absent : Nat
• providerError : Nat
• rejected : Nat
• accepted : Nat

def Hex.Internal.LLLProvider.instReprDiagnostics.repr : Diagnostics → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Hex.Internal.LLLProvider.instReprDiagnostics : Repr Diagnostics

Equations

• Hex.Internal.LLLProvider.instReprDiagnostics = { reprPrec := Hex.Internal.LLLProvider.instReprDiagnostics.repr }

def Hex.Internal.LLLProvider.instBEqDiagnostics.beq : Diagnostics → Diagnostics → Bool

Equations

• One or more equations did not get rendered due to their size.
• Hex.Internal.LLLProvider.instBEqDiagnostics.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Hex.Internal.LLLProvider.instBEqDiagnostics : BEq Diagnostics

Equations

• Hex.Internal.LLLProvider.instBEqDiagnostics = { beq := Hex.Internal.LLLProvider.instBEqDiagnostics.beq }

@[implicit_reducible]

instance Hex.Internal.LLLProvider.instInhabitedDiagnostics : Inhabited Diagnostics

Equations

• Hex.Internal.LLLProvider.instInhabitedDiagnostics = { default := Hex.Internal.LLLProvider.instInhabitedDiagnostics.default }

inductive Hex.Internal.LLLProvider.Outcome : Type

Classification of one external-provider attempt: unavailable provider, provider error, rejected response, or accepted candidate.

• absent : Outcome
• providerError : Outcome
• rejected : Outcome
• accepted : Outcome

@[implicit_reducible]

instance Hex.Internal.LLLProvider.instReprOutcome : Repr Outcome

Equations

• Hex.Internal.LLLProvider.instReprOutcome = { reprPrec := Hex.Internal.LLLProvider.instReprOutcome.repr }

def Hex.Internal.LLLProvider.instReprOutcome.repr : Outcome → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Hex.Internal.LLLProvider.instBEqOutcome : BEq Outcome

Equations

• Hex.Internal.LLLProvider.instBEqOutcome = { beq := Hex.Internal.LLLProvider.instBEqOutcome.beq }

def Hex.Internal.LLLProvider.instBEqOutcome.beq : Outcome → Outcome → Bool

Equations

• Hex.Internal.LLLProvider.instBEqOutcome.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Hex.Internal.LLLProvider.bump (d : Diagnostics) : Outcome → Diagnostics

Increment the diagnostic counter matching outcome.

Equations

• Hex.Internal.LLLProvider.bump d Hex.Internal.LLLProvider.Outcome.absent = { absent := d.absent + 1, providerError := d.providerError, rejected := d.rejected, accepted := d.accepted }
• Hex.Internal.LLLProvider.bump d Hex.Internal.LLLProvider.Outcome.providerError = { absent := d.absent, providerError := d.providerError + 1, rejected := d.rejected, accepted := d.accepted }
• Hex.Internal.LLLProvider.bump d Hex.Internal.LLLProvider.Outcome.rejected = { absent := d.absent, providerError := d.providerError, rejected := d.rejected + 1, accepted := d.accepted }
• Hex.Internal.LLLProvider.bump d Hex.Internal.LLLProvider.Outcome.accepted = { absent := d.absent, providerError := d.providerError, rejected := d.rejected, accepted := d.accepted + 1 }

opaque Hex.Internal.LLLProvider.diagnosticsRef : IO.Ref Diagnostics

def Hex.Internal.LLLProvider.resetDiagnostics : IO Unit

Reset the external-provider diagnostics counters to zero. Test and bench harnesses use this to isolate one run's provider availability, rejection, and acceptance counts.

Equations

• Hex.Internal.LLLProvider.resetDiagnostics = ST.Ref.set Hex.Internal.LLLProvider.diagnosticsRef { }

def Hex.Internal.LLLProvider.diagnostics : IO Diagnostics

Read the external-provider diagnostics accumulated since the last resetDiagnostics. The snapshot is the observability hook for deciding whether the external reducer was absent, failed, returned malformed data, or supplied a candidate accepted by the decoder.

Equations

• Hex.Internal.LLLProvider.diagnostics = ST.Ref.get Hex.Internal.LLLProvider.diagnosticsRef

def Hex.Internal.LLLProvider.recordOutcome (outcome : Outcome) : IO Unit

Increment the external-provider diagnostic counter for outcome. This is the IO entry point used by provider calls; pure LLL code uses withRecordOutcome to record the same classifications without changing its surface type.

Equations

• Hex.Internal.LLLProvider.recordOutcome outcome = ST.Ref.modify Hex.Internal.LLLProvider.diagnosticsRef fun (d : Hex.Internal.LLLProvider.Diagnostics) => Hex.Internal.LLLProvider.bump d outcome

def Hex.Internal.LLLProvider.validateFlat (rows cols : Nat) (withInverse : Bool) (flat : Array Int) : Option Candidate

Decode the external reducer's flat integer response into a structured Candidate. The decoder checks the status word, row/column headers, inverse flag, and total payload length before slicing out the reduced basis, transformation, and optional inverse; any mismatch returns none, so malformed provider output cannot enter the certified path.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Internal.LLLProvider.tryReduce (rows cols : USize) (entries : Array String) (delta eta : Float) (method : UInt8) (withInverse : Bool) : IO (Option Candidate)

Try to obtain an LLL candidate from the external provider. The call records why no candidate was used (absent, provider error, or rejected flat payload) and returns some candidate only after validateFlat accepts the provider's response shape.

Equations

• One or more equations did not get rendered due to their size.

unsafe def Hex.Internal.LLLProvider.withRecordOutcomeImpl {α : Sort u} (o : Outcome) (k : α) : α

Side-effecting companion of recordOutcome callable from pure code.

Definitionally k, so kernel reduction and proofs treat it as identity on the continuation. The @[implemented_by] attribute redirects compiled code to a side-effecting implementation that bumps diagnosticsRef via unsafeBaseIO before returning k, giving us the diagnostic tally that the SPEC requires without forcing lll into IO. The pattern mirrors Init.Util.withPtrEq.

Equations

• Hex.Internal.LLLProvider.withRecordOutcomeImpl o k = k

@[implemented_by Hex.Internal.LLLProvider.withRecordOutcomeImpl]

def Hex.Internal.LLLProvider.withRecordOutcome {α : Sort u} (_o : Outcome) (k : α) : α

Pure-facing wrapper that records one external-provider outcome in compiled code and otherwise returns k. This lets the public reducer stay pure while compiled runs still populate diagnosticsRef for provider observability.

Equations

• Hex.Internal.LLLProvider.withRecordOutcome _o k = k

def Hex.Internal.LLLProvider.ratToFloat (r : Rat) : Float

Approximate Rat → Float conversion used to forward the requested δ to the external reducer. Precision of the forwarded value is not part of correctness: the candidate is certified by integer arithmetic against the exact δ.

Equations

• Hex.Internal.LLLProvider.ratToFloat r = Float.ofInt r.num / Float.ofNat r.den

def Hex.Internal.LLLProvider.requestedEta : Rat

Size-reduction bound requested from the external reducer, strictly stronger than the η = 11/20 the checker certifies.

The dispatch asks the reducer for a (requestedDelta δ, requestedEta)-reduced basis but certifies it against the public (δ, 11/20). The two differ on purpose. certCheck's reducedness clause is decided by a fixed-precision enclosure pass that resolves open inequalities only by margin; a candidate whose |μ| sits arbitrarily close to 11/20 would leave the enclosure straddling its threshold and force the exact fallback. Requesting requestedEta < 11/20 instead guarantees a correctly-functioning reducer lands every size-reduction inequality a macroscopic 11/20 − requestedEta clear of the certified bound, so the enclosure decides it.

requestedEta must stay > 1/2 (the reducer's hard floor) and < 11/20. Its exact value is untrusted: certification is against the exact (δ, 11/20), so the requested bound is outside the trusted story entirely (the "reliability is empirical, soundness is not" clause). Varying it within (1/2, 11/20) only trades reducer work against enclosure margin; it cannot make a non-reduced basis certify. The value 107/200 sits a gap of 3/200 below 11/20 and 7/200 above 1/2: a narrow gap from the certified bound keeps the small amount of extra work the stronger request costs the reducer inside measurement noise, while still clearing the bound by a margin the enclosure resolves. It is a Rat, forwarded to the reducer through ratToFloat like requestedDelta, so the design constant and the certified bound are comparable rationals.

Equations

• Hex.Internal.LLLProvider.requestedEta = 107 / 200

def Hex.Internal.LLLProvider.requestedDelta (δ : Rat) : Rat

Lovász parameter requested from the external reducer: a fixed 1/100 margin above the caller's δ, but never past the midpoint (δ + 1)/2 between δ and 1.

Mirrors requestedEta: the dispatch certifies the candidate against the caller's exact δ but asks the reducer for the stronger requestedDelta δ, so a correctly-functioning reducer clears every Lovász inequality by a positive margin (requestedDelta δ − δ)·d[i+1]² and the enclosure decides it rather than straddling.

The midpoint cap is what keeps the request strictly between δ and 1 over the whole public surface δ ≤ 1. For δ ≤ 49/50 the 1/100 term wins and the margin is the full 1/100; for 49/50 < δ < 1 the midpoint wins and the margin is (1 − δ)/2, still positive, so δ < requestedDelta δ < 1 holds for every δ < 1. At the boundary δ = 1 the midpoint is 1: no value is both > δ and < 1, so the request equals the certified δ and the prophylactic gap is unavoidably lost — a candidate the reducer cannot strengthen there falls back through certification to the native path, which stays sound.

The Lovász condition governs how many swaps the reducer performs, so the requested δ drives the extra work the stronger request costs; the small 1/100 margin keeps that cost inside measurement noise while still giving the enclosure a decisive gap.

Untrusted, exactly as requestedEta: the certificate is checked against the exact δ, never against this value, so the margin may vary without touching soundness.

Equations

• Hex.Internal.LLLProvider.requestedDelta δ = min (δ + 1 / 100) ((δ + 1) / 2)

def Hex.Internal.LLLProvider.matrixToEntries {n m : Nat} (B : Matrix Int n m) : Array String

Row-major marshalling of an integer matrix into the Array String payload the external provider expects.

Equations

• Hex.Internal.LLLProvider.matrixToEntries B = Array.flatMap (fun (row : Vector Int m) => Array.map toString row.toArray) B.rows.toArray

def Hex.Internal.LLLProvider.matrixFromArray (rows cols : Nat) (a : Array Int) : Option (Matrix Int rows cols)

Reshape a flat row-major Array Int of length rows * cols into a Matrix Int rows cols. Returns none on length mismatch.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Internal.LLLProvider.CertifiedTriple {n m : Nat} (B : Matrix Int n m) (δ : Rat) : Type

Bundled output of the shape/cert pipeline: the reduced basis B', the two integer transforms, and a proof that they pass Hex.certCheck at (δ, 11/20). Bundling the proof inside the option lets the extraction lemma read it off as a projection.

Equations

• Hex.Internal.LLLProvider.CertifiedTriple B δ = ((B' : Hex.Matrix Int n m) ×' (U : Hex.Matrix Int n n) ×' (V : Hex.Matrix Int n n) ×' Hex.certCheck B B' U V δ (11 / 20) = true)

def Hex.Internal.LLLProvider.certifyFlat {n m : Nat} (B : Matrix Int n m) (δ : Rat) (flat : Array Int) : Option (CertifiedTriple B δ)

Pure shape/cert pipeline run on a flat provider payload. Validates the header, reshapes the reduced basis and the two transforms, and runs Hex.certCheck at η = 11/20. Returns the bundled certified triple on acceptance and none on any failure.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Internal.LLLProvider.dispatch {n m : Nat} (B : Matrix Int n m) (δ : Rat) : Option (Matrix Int n m)

Pure certified-dispatch core. Gates on providerAvailable () first so the native path pays only the cached probe; marshals input and certifies the candidate when the provider is present; updates the diagnostic tally via withRecordOutcome on each outcome.

Returns the certified reduced basis B' on acceptance and none on absent / provider error / shape rejection / certificate rejection. The Mathlib-free correctness hook is dispatch_some_certCheck.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Internal.LLLProvider.dispatch_some_certCheck {n m : Nat} {B : Matrix Int n m} {δ : Rat} {B' : Matrix Int n m} (h : dispatch B δ = some B') : ∃ (U : Matrix Int n n), ∃ (V : Matrix Int n n), certCheck B B' U V δ (11 / 20) = true

An accepted dispatch result exhibits the integer transforms witnessing certCheck B B' U V δ (11/20) = true. The property-level extraction ((same lattice, B'.independent, isLLLReduced B' δ (11/20))) is certCheck's soundness theorem in HexLLLMathlib.