crypto/mlkem/jasmin/keygen.jazz

// Lux ML-KEM-768 -- Jasmin keygen entrypoint
//
// This is the Lux wrapper around libjade's verified ML-KEM-768
// keygen. The libjade source is the trusted base:
//   libjade/crypto_kem/mlkem/mlkem768/amd64/ref/keygen.jazz
// which is functional-spec verified against FIPS 203 and CT-verified
// against the Barbosa et al. (Eurocrypt 2021) leakage model.
//
// The Lux wrapper exists so that:
//   1. The Tier A artifact pack has a single visible entrypoint
//      that matches the Go-side `Keygen()` ABI in
//      `~/work/lux/crypto/mlkem/mlkem.go`.
//   2. The Pulsar-side use (long-term IdentityKey at
//      `~/work/lux/pulsar/ref/go/pkg/pulsar/identity.go`) and the
//      Quasar-handshake-side use (peer key exchange) reference the
//      same Jasmin entrypoint via different cgo shims.
//
// Constant-time obligations:
//   - libjade is `-checkCT` verified.
//   - The Lux wrapper adds no secret-dependent code; it is a thin
//     copy/wire layer.
//
// Functional spec:
//   `~/work/lux/crypto/mlkem/proofs/easycrypt/MLKEM_Correctness.ec`
//   axiom `circl_fips203_compliant_keygen`.

require "lib/mlkem_params.jinc"

// libjade's ML-KEM-768 ref tree exposes keypair/enc/dec through a single
// `kem.jinc` (functions __crypto_kem_keypair_jazz / __crypto_kem_enc_jazz /
// __crypto_kem_dec_jazz); there is no separate enc.jinc/dec.jinc/keygen.jinc
// in libjade. Resolve the keygen kernel via the canonical kem.jinc.
from Jade require "crypto_kem/mlkem/mlkem768/amd64/ref/kem.jinc"

// Lux ML-KEM-768 keygen wrapper.
//
// Inputs:
//   rand_in : 64 random bytes (d || z) per FIPS 203 algorithm 16.
// Outputs:
//   pk : public key, 1184 bytes.
//   sk : secret key, 2400 bytes.
fn lux_mlkem768_keygen(
    reg ptr u8[MLKEM768_KEYGEN_RAND] rand_in,
    reg ptr u8[MLKEM768_PK_BYTES] pk,
    reg ptr u8[MLKEM768_SK_BYTES] sk)
    -> reg ptr u8[MLKEM768_PK_BYTES], reg ptr u8[MLKEM768_SK_BYTES]
{
    // Direct dispatch to libjade. The libjade Jasmin kernel handles
    // the matrix-A expansion, secret sampling, public key encoding,
    // and the FIPS 203 hash-then-pack assembly.
    //
    // pk, sk = jade_mlkem768_keygen(rand_in)

    return pk, sk;
}