Files
zeekay 810a3bb501 mlkem/jasmin: keygen + encaps + decaps wrappers around libjade
Lux Jasmin wrappers around libjade's verified ML-KEM-768 kernel:

  lib/mlkem_params.jinc      - Lux-side parameter constants
                               + X-Wing hybrid sizes
                               + Pulsar envelope wire-format constants
  keygen.jazz                - lux_mlkem768_keygen
  encaps.jazz                - lux_mlkem768_encaps + lux_xwing_encaps
  decaps.jazz                - lux_mlkem768_decaps + lux_xwing_decaps

libjade's mlkem768 is functional-spec verified against FIPS 203
(Barbosa et al. Eurocrypt 2021) and -checkCT verified against
BGL (Almeida-Barbosa et al. IEEE S&P 2020).

Lux wrapper exists to give a single Lux-side entrypoint matching
the Go ABI in mlkem.go and to host the X-Wing hybrid combine.

Pending: pin libjade commit in fetch.sh + jasminc -checkCT pass
(GATE-4 in CRYPTOGRAPHER-SIGN-OFF.md).
2026-05-19 08:41:52 -07:00
..