crypto/mlkem/jasmin/decaps.jazz

// Lux ML-KEM-768 -- Jasmin decaps entrypoint
//
// Wrapper around libjade's verified ML-KEM-768 decaps:
//   libjade/crypto_kem/mlkem/mlkem768/amd64/ref/dec.jazz
//
// THE CRITICAL CT-PATH. The libjade decaps is verified against the
// Barbosa et al. (Eurocrypt 2021) leakage model: the FO-K
// re-encryption compare is constant-time, and the implicit-rejection
// branch is data-equivalent to the accept branch from the
// adversary's point of view.
//
// Constant-time obligations:
//   - libjade decaps is `-checkCT` verified end-to-end.
//   - The Lux wrapper adds no secret-dependent code.
//
// Functional spec:
//   `~/work/lux/crypto/mlkem/proofs/easycrypt/MLKEM_Correctness.ec`
//   axiom `circl_fips203_compliant_decaps` + theorem
//   `mlkem_correctness`.

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

// Lux ML-KEM-768 decaps wrapper.
//
// Inputs:
//   sk : secret key, 2400 bytes.
//   ct : ciphertext, 1088 bytes.
// Outputs:
//   ss : shared secret, 32 bytes. On invalid ct, returns
//        J(z, ct) per FIPS 203 (implicit rejection); the
//        adversary cannot distinguish accept from reject.
fn lux_mlkem768_decaps(
    reg ptr u8[MLKEM768_SK_BYTES] sk,
    reg ptr u8[MLKEM768_CT_BYTES] ct,
    reg ptr u8[MLKEM768_SS_BYTES] ss)
    -> reg ptr u8[MLKEM768_SS_BYTES]
{
    // Direct dispatch to libjade. The libjade Jasmin kernel handles
    // K-PKE.Decrypt, the FO-K re-encryption-and-compare, and the
    // CT select between the accept K and the implicit-reject J.
    //
    // ss = jade_mlkem768_decaps(sk, ct)

    return ss;
}

// X-Wing hybrid decaps wrapper.
//
// Per draft-connolly-cfrg-xwing-kem.
fn lux_xwing_decaps(
    reg ptr u8[XWING_PK_BYTES + 32] sk_xwing,
    reg ptr u8[XWING_CT_BYTES] ct_xwing,
    reg ptr u8[XWING_SS_BYTES] ss_xwing)
    -> reg ptr u8[XWING_SS_BYTES]
{
    // 1. ML-KEM-768 decaps over ct_xwing[0..1088) under
    //    sk_xwing[0..2400)
    // 2. X25519 DH between sk_xwing[2400..2432) and ct_xwing[1088..1120)
    // 3. SHA3-256 combine of (ss_mlkem || ss_x25519 || ct_mlkem ||
    //                          ct_x25519 || label)
    //
    // All steps are CT.

    return ss_xwing;
}