17.5. Certified external reduction🔗

By default Hex.lll runs the exact Hex.lllNative. To let it accelerate through the external fpLLL reducer instead, call Hex.lll.loadExternalReducer with the path to a built fpLLL-ffi shared library (scripts/oracle/setup_fplll_ffi.sh builds one and prints its path); it dlopens the library, installs it as the process reducer, and returns true on success. Hex.lll.externalReducerActive reports whether one is installed. This is a runtime switch, not a matter of importing a different module; HexLLL always links its small reducer shim, and the same Hex.lll call takes the certified path exactly when a reducer is installed. Loading is an explicit, discoverable Lean action next to Hex.lll: there is no environment variable read on the Hex.lll path and no implicit dlopen.

Either way the result is (δ, 11/20)-reduced. When the reducer is in use, Hex.lll asks it for a reduced basis and re-checks the candidate with Hex.certCheck before returning it; a candidate the checker rejects, or an absent reducer, falls straight through to the native reducer. The foreign numerics can therefore speed things up but can never affect correctness: nothing the reducer returns is trusted until the verified integer checker has accepted it.

def

Hex.lll.loadExternalReducer (path : System.FilePath) : IO Bool
Hex.lll.loadExternalReducer
  (path : System.FilePath) : IO Bool

Install an external LLL reducer 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); the loader calls dlopen, resolves that symbol, and records the reduction function. Once installed, a Hex.lll call whose candidate certifies under Hex.certCheck returns the accelerated basis; an absent reducer, a load failure, or a rejected candidate all fall through to the exact Hex.lllNative. Loading is an explicit action; there is no environment-variable read and no implicit load; and the trust boundary is unchanged: every external candidate is checked before use.

A later successful load replaces the current reducer; 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.

def

Hex.lll.externalReducerActive : IO Bool
Hex.lll.externalReducerActive : IO Bool

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