The public LLL entry points. lll keeps two paths: the certified external-candidate dispatch (provider → certCheck) and, when no provider candidate certifies, the exact lllNative. Both satisfy the same (δ, 11/20) contract. lll.firstShortVector / lll.shortVectors expose the reduced rows for downstream consumers.

def Hex.lll {n m : Nat} (b : Matrix Int n m) (δ : Rat) (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (_hind : b.independent) : Matrix Int n m

Top-level LLL entry point. Dispatches first to the certified-external path: if LLLProvider.providerAvailable () is true and the candidate passes certCheck B B' U V δ (11/20), the certified B' is returned; otherwise the exact lllNative runs. Both paths satisfy the identical post-condition (isLLLReduced (lll …) δ (11/20), same lattice, the public short-vector bound), so dispatch is invisible to callers and to proofs.

Equations

• Hex.lll b δ hδ hδ' hn _hind = match Hex.Internal.LLLProvider.dispatch b δ with | some B' => B' | none => Hex.lllNative b δ ⋯ hδ' hn

def Hex.lll.loadProvider (path : System.FilePath) : IO Bool

Install an external LLL acceleration provider from the shared library at path for the rest of this process, returning whether the load succeeded.

The library must export lean_fplll_lll_reduce (the fpLLL-ffi shim built by scripts/oracle/setup_fplll_ffi.sh); loadProvider dlopens it, resolves that symbol, and points the dispatch at it. Once installed, a lll call whose provider candidate certifies under Hex.certCheck returns the accelerated basis; an absent provider, a load failure, or a rejected candidate all fall through to the exact lllNative. Loading is an explicit action — there is no environment-variable read and no implicit load — and the trust boundary is unchanged: every provider candidate is still checked before use.

A later successful load replaces the current provider; a failed load leaves the existing state untouched and returns false (writing the dlopen/dlsym diagnostic to stderr) when the library cannot be loaded or does not export the expected symbol.

Equations

• Hex.lll.loadProvider path = Hex.Internal.LLLProvider.loadProviderImpl path.toString

def Hex.lll.providerActive : IO Bool

Whether an external LLL acceleration provider is currently installed in this process (via Hex.lll.loadProvider or a statically-linked provider symbol). When this is false, lll runs the exact lllNative; when it is true, lll attempts the certified external path first. Querying availability is side-effect-free apart from the one-shot static-symbol probe it may trigger.

Equations

• Hex.lll.providerActive = pure (Hex.Internal.LLLProvider.providerAvailable ())

def Hex.lllNative.firstShortVector {n m : Nat} (b : Matrix Int n m) (δ : Rat) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) : Vector Int m

First row of lllNative's output: the lll.firstShortVector counterpart on the exact native path. It never consults an external provider and takes no b.independent hypothesis, so Mathlib-free callers can use it directly; its short-vector guarantee is lllNative_first_row_norm_sq_le at η = 1/2.

Equations

• Hex.lllNative.firstShortVector b δ hδ hδ' hn = (Hex.lllNative b δ hδ hδ' hn).getRow ⟨0, hn⟩

def Hex.lll.firstShortVector {n m : Nat} (b : Matrix Int n m) (δ : Rat) (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hind : b.independent) : Vector Int m

The first row of the reduced basis: a provably short vector, bounded by the LLL approximation factor relative to any nonzero lattice vector (see lll_first_row_norm_sq_le), not necessarily the shortest lattice vector. Canonical short-vector entry point for downstream callers such as hex-berlekamp-zassenhaus recombination.

Equations

• Hex.lll.firstShortVector b δ hδ hδ' hn hind = (Hex.lll b δ hδ hδ' hn hind).getRow ⟨0, hn⟩

def Hex.lllNative.shortVectors {n m : Nat} (b : Matrix Int n m) (δ : Rat) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) : Array (Vector Int m)

Full lllNative output as an ordered array of candidate short vectors: the lll.shortVectors counterpart on the exact native path, forgoing the external provider and the b.independent hypothesis.

Equations

• Hex.lllNative.shortVectors b δ hδ hδ' hn = (Hex.lllNative b δ hδ hδ' hn).rows.toArray

def Hex.lll.shortVectors {n m : Nat} (b : Matrix Int n m) (δ : Rat) (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hind : b.independent) : Array (Vector Int m)

The full reduced basis viewed as an ordered array of candidate short vectors.

Equations

• Hex.lll.shortVectors b δ hδ hδ' hn hind = (Hex.lll b δ hδ hδ' hn hind).rows.toArray