hex

17.6. Performance comparison🔗

HexLLL is benchmarked against the verified Isabelle LLL_Basis_Reduction extraction and the unverified floating-point fpLLL, across six input families that each stress a different cost. Here is harsh-cubic, where the entry bit-length grows with the dimension:

HexLLL harsh-cubic comparator

17.6.1. The five curves🔗

Each plot is log-scale wall-time per reduction against the family dimension:

  • fpLLL: the raw floating-point reducer, unverified; the speed baseline.

  • Lean native: Hex.lllNative, the exact all-integer d/ν reducer. Correct by construction, but its exact arithmetic pays for wide operands and high swap counts.

  • Lean certified: an fpLLL candidate checked by the verified Lean checker Hex.certCheck. It inherits floating-point speed and adds only a cheap integer check, so it stays close to the fpLLL curve while remaining fully verified.

  • verified Isabelle native: the Isabelle extraction's own reducer; the independent verified point of comparison.

  • verified Isabelle certified: the same fpLLL candidate checked by the Isabelle checker instead of the Lean one; the apples-to-apples yardstick for the Lean certified path.

17.6.2. The six input families🔗

Each family is a faithful port of an fplll generator, and stresses a different part of the algorithm:

  • random-bounded: near-orthogonal random bases; the easy baseline, few swaps.

  • harsh-cubic: entries of bit-length about 3.3·n; exact-integer operand-width growth (shown above).

  • ajtai: fplll gen_trg worst-case triangular bases; the swap / iteration count Θ(d² log B) (shown in the introduction).

  • q-ary: LWE/SIS bases [[I, H], [0, qI]]; the cryptographic Z-shape.

  • ntru: bases [[I, Rot h], [0, qI]]; a planted dense sublattice plus a q-block.

  • knapsack: the rectangular d × (d+1) integer-relation form; the only family with more columns than rows, using the m > n construction.

Across every family the exact reducers are correct but climb steeply on the hard bases, while Lean certified stays within about 1.2 to 2.5 times raw fpLLL: verified output at close to floating-point cost. Selecting the certified versus native path is the runtime switch described under Certified external reduction; the η = 11/20 constants both paths report are explained under the size-reduction bound.

17.6.3. The other families🔗

The remaining comparator plots, for reference:

ajtai

q-ary

ntru

knapsack

random-bounded