@[extern lean_hexlll_provider_available]

opaque Hex.Internal.ExternalReducer.externalReducerAvailable : Unit → Bool

Report whether an external reduction function is installed.

@[extern lean_hexlll_provider_reduce]

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

Ask the installed external function for a reduced basis and transformation data.

@[extern lean_hexlll_load_provider]

opaque Hex.Internal.ExternalReducer.loadExternalReducerImpl (path : String) : IO Bool

Install the external reducer from the shared library at path: dlopen the library, resolve lean_fplll_lll_reduce from it, and set the process reducer 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.loadExternalReducer.

structure Hex.Internal.ExternalReducer.Candidate : Type

Decoded result returned by the external LLL reducer.

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

  The proposed reduced basis in row-major order.

• transform : Array Int

  A proposed transformation mapping the input basis to reduced.

• inverse? : Option (Array Int)

  An optional proposed inverse transformation.

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

Equations

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

@[instance_reducible]

instance Hex.Internal.ExternalReducer.instReprCandidate : Repr Candidate

Equations

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

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

Equations

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

@[instance_reducible]

instance Hex.Internal.ExternalReducer.instBEqCandidate : BEq Candidate

Equations

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

structure Hex.Internal.ExternalReducer.Diagnostics : Type

Diagnostic counters for attempts to use the external LLL reducer.

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

• absent : Nat

  Calls made without an installed external reducer.

• reductionError : Nat

  Calls for which the external reducer reported an error.

• rejected : Nat

  Candidates rejected because their shape or arithmetic certificate failed.

• accepted : Nat

  Candidates decoded successfully for later certification.

@[instance_reducible]

instance Hex.Internal.ExternalReducer.instReprDiagnostics : Repr Diagnostics

Equations

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

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

Equations

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

@[instance_reducible]

instance Hex.Internal.ExternalReducer.instBEqDiagnostics : BEq Diagnostics

Equations

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

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

Equations

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

@[instance_reducible]

instance Hex.Internal.ExternalReducer.instInhabitedDiagnostics : Inhabited Diagnostics

Equations

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

inductive Hex.Internal.ExternalReducer.Outcome : Type

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

• absent : Outcome

  No external reduction function was installed.

• reductionError : Outcome

  The external reduction function reported an error.

• rejected : Outcome

  The returned arrays could not form a valid candidate.

• accepted : Outcome

  The returned arrays formed a candidate ready for certification.

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

Equations

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

@[instance_reducible]

instance Hex.Internal.ExternalReducer.instReprOutcome : Repr Outcome

Equations

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

@[instance_reducible]

instance Hex.Internal.ExternalReducer.instBEqOutcome : BEq Outcome

Equations

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

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

Equations

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

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

Increment the diagnostic counter matching outcome.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Internal.ExternalReducer.bump d Hex.Internal.ExternalReducer.Outcome.absent = { absent := d.absent + 1, reductionError := d.reductionError, rejected := d.rejected, accepted := d.accepted }
• Hex.Internal.ExternalReducer.bump d Hex.Internal.ExternalReducer.Outcome.rejected = { absent := d.absent, reductionError := d.reductionError, rejected := d.rejected + 1, accepted := d.accepted }
• Hex.Internal.ExternalReducer.bump d Hex.Internal.ExternalReducer.Outcome.accepted = { absent := d.absent, reductionError := d.reductionError, rejected := d.rejected, accepted := d.accepted + 1 }

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

def Hex.Internal.ExternalReducer.resetDiagnostics : IO Unit

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

Equations

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

def Hex.Internal.ExternalReducer.diagnostics : IO Diagnostics

Read the external-reducer 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.ExternalReducer.diagnostics = ST.Ref.get Hex.Internal.ExternalReducer.diagnosticsRef

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

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

Equations

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

def Hex.Internal.ExternalReducer.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 external reducer output cannot enter the certified path.

Equations

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

def Hex.Internal.ExternalReducer.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 reducer. The call records why no candidate was used (absent, external reducer error, or rejected flat payload) and returns some candidate only after validateFlat accepts the external reducer's response shape.

Equations

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

unsafe def Hex.Internal.ExternalReducer.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, providing the diagnostic tally without forcing lll into IO. The pattern mirrors Init.Util.withPtrEq.

Equations

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

@[implemented_by Hex.Internal.ExternalReducer.withRecordOutcomeImpl]

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

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

Equations

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

def Hex.Internal.ExternalReducer.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.ExternalReducer.ratToFloat r = Float.ofInt r.num / Float.ofNat r.den

def Hex.Internal.ExternalReducer.requestedEta : Rat

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

The selection 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.ExternalReducer.requestedEta = 107 / 200

def Hex.Internal.ExternalReducer.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 selection 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.ExternalReducer.requestedDelta δ = min (δ + 1 / 100) ((δ + 1) / 2)

def Hex.Internal.ExternalReducer.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 reducer expects.

Equations

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

def Hex.Internal.ExternalReducer.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.ExternalReducer.CertifiedTriple {n m : Nat} (B : Matrix Int n m) (δ : Rat) : Type

Bundled output of the shape/cert computation: 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.ExternalReducer.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.ExternalReducer.certifyFlat {n m : Nat} (B : Matrix Int n m) (δ : Rat) (flat : Array Int) : Option (CertifiedTriple B δ)

Pure shape/cert computation run on a flat external reducer 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.ExternalReducer.certifiedReduction {n m : Nat} (B : Matrix Int n m) (δ : Rat) : Option (Matrix Int n m)

Pure certified reduction. Checks externalReducerAvailable () first so the native path pays only the cached trial; marshals input and certifies the candidate when the external reducer is present; updates the diagnostic tally via withRecordOutcome on each outcome.

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

Equations

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

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

An accepted certifiedReduction 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.