hex

6.5. Certified external dispatch🔗

When an external fpLLL provider is linked in, Hex.Internal.LLLProvider.dispatch asks it for a reduced basis and validates the answer with Hex.certCheck before trusting it. A rejected or absent provider yields none, and the caller falls through to the native path, so the foreign reducer can speed things up but can never compromise correctness.

🔗def
Hex.Internal.LLLProvider.dispatch {n m : Nat} (B : Hex.Matrix Int n m)
  (δ : Rat) : Option (Hex.Matrix Int n m)
Hex.Internal.LLLProvider.dispatch
  {n m : Nat} (B : Hex.Matrix Int n m)
  (δ : Rat) : Option (Hex.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.

An accepted dispatch result comes with the integer transforms witnessing its certificate, the single fact the certified-dispatch path of Hex.lll depends on.

🔗theorem
Hex.Internal.LLLProvider.dispatch_some_certCheck {n m : Nat}
  {B : Hex.Matrix Int n m} {δ : Rat} {B' : Hex.Matrix Int n m}
  (h : Hex.Internal.LLLProvider.dispatch B δ = some B') :
  ∃ U V, Hex.certCheck B B' U V δ (11 / 20) = true
Hex.Internal.LLLProvider.dispatch_some_certCheck
  {n m : Nat} {B : Hex.Matrix Int n m}
  {δ : Rat} {B' : Hex.Matrix Int n m}
  (h :
    Hex.Internal.LLLProvider.dispatch B
        δ =
      some B') :
  ∃ U V,
    Hex.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.