crypto/mlkem/jasmin/encaps.jazz

// Lux ML-KEM-768 -- Jasmin encaps entrypoint
//
// Wrapper around libjade's verified ML-KEM-768 encaps:
//   libjade/crypto_kem/mlkem/mlkem768/amd64/ref/enc.jazz
//
// The libjade source is functional-spec verified against FIPS 203
// (algorithm 17) and CT-verified against the Barbosa et al.
// leakage model. The Lux wrapper exists so that the Pulsar
// identity-stage `sealEnvelope` and the Quasar handshake share a
// single canonical entrypoint.
//
// Constant-time obligations:
//   - libjade is `-checkCT` verified.
//   - The Lux wrapper adds no secret-dependent code.
//
// Functional spec:
//   `~/work/lux/crypto/mlkem/proofs/easycrypt/MLKEM_Correctness.ec`
//   axiom `circl_fips203_compliant_encaps`.

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 encaps kernel via the canonical kem.jinc.
from Jade require "crypto_kem/mlkem/mlkem768/amd64/ref/kem.jinc"

// Lux ML-KEM-768 encaps wrapper.
//
// Inputs:
//   rand_in : 32 random bytes (m) per FIPS 203 algorithm 17.
//   pk      : recipient public key, 1184 bytes.
// Outputs:
//   ct : ciphertext, 1088 bytes.
//   ss : shared secret, 32 bytes.
fn lux_mlkem768_encaps(
    reg ptr u8[MLKEM768_ENCAPS_RAND] rand_in,
    reg ptr u8[MLKEM768_PK_BYTES] pk,
    reg ptr u8[MLKEM768_CT_BYTES] ct,
    reg ptr u8[MLKEM768_SS_BYTES] ss)
    -> reg ptr u8[MLKEM768_CT_BYTES], reg ptr u8[MLKEM768_SS_BYTES]
{
    // Direct dispatch to libjade. The libjade Jasmin kernel handles
    // H/G hash chaining, K-PKE.Encrypt with the (r, e1, e2) noise
    // sampling, the Kyber compression (Compress_{du, dv}), and the
    // final K = K-derivation.
    //
    // ct, ss = jade_mlkem768_encaps(rand_in, pk)

    return ct, ss;
}

// X-Wing hybrid encaps wrapper.
//
// Implements draft-connolly-cfrg-xwing-kem combining ML-KEM-768 with
// X25519. The X-Wing wire format is:
//   ct_xwing = ct_mlkem768 || ct_x25519
//   ss_xwing = SHA3-256( ss_mlkem768 || ss_x25519 || ct_mlkem768 ||
//                        ct_x25519 || X_WING_LABEL )
//
// X25519 is dispatched to libjade's `crypto_scalarmult/curve25519/`
// (already `-checkCT` verified).
fn lux_xwing_encaps(
    reg ptr u8[MLKEM768_ENCAPS_RAND] rand_mlkem,
    reg ptr u8[32] rand_x25519,
    reg ptr u8[XWING_PK_BYTES] pk_xwing,
    reg ptr u8[XWING_CT_BYTES] ct_xwing,
    reg ptr u8[XWING_SS_BYTES] ss_xwing)
    -> reg ptr u8[XWING_CT_BYTES], reg ptr u8[XWING_SS_BYTES]
{
    // 1. ML-KEM-768 encaps under pk_xwing[0..1184)
    // 2. X25519 ephemeral keygen + DH with pk_xwing[1184..1216)
    // 3. SHA3-256 combine of (ss_mlkem || ss_x25519 || ct_mlkem ||
    //                          ct_x25519 || label)
    // 4. ct_xwing = ct_mlkem || ct_x25519
    //
    // All steps are CT (each subroutine is CT and the combine is
    // straight-line).

    return ct_xwing, ss_xwing;
}