lib-q-ml-dsa 0.0.2

pub(crate) use lib_q_ring::constants::{
    COEFFICIENTS_IN_RING_ELEMENT,
    FIELD_MODULUS,
};

pub(crate) const FIELD_MODULUS_MINUS_ONE_BIT_LENGTH: usize = 23;

pub(crate) const BITS_IN_LOWER_PART_OF_T: usize = 13;
pub(crate) const RING_ELEMENT_OF_T0S_SIZE: usize =
    (BITS_IN_LOWER_PART_OF_T * COEFFICIENTS_IN_RING_ELEMENT) / 8;

pub(crate) const BITS_IN_UPPER_PART_OF_T: usize =
    FIELD_MODULUS_MINUS_ONE_BIT_LENGTH - BITS_IN_LOWER_PART_OF_T;
pub(crate) const RING_ELEMENT_OF_T1S_SIZE: usize =
    (BITS_IN_UPPER_PART_OF_T * COEFFICIENTS_IN_RING_ELEMENT) / 8;

pub(crate) const SEED_FOR_A_SIZE: usize = 32;
pub(crate) const SEED_FOR_ERROR_VECTORS_SIZE: usize = 64;
pub(crate) const BYTES_FOR_VERIFICATION_KEY_HASH: usize = 64;
pub(crate) const SEED_FOR_SIGNING_SIZE: usize = 32;

/// Number of bytes of entropy required for key generation.
pub const KEY_GENERATION_RANDOMNESS_SIZE: usize = 32;
/// Number of bytes of entropy required for signing.
pub const SIGNING_RANDOMNESS_SIZE: usize = 32;

pub(crate) const MESSAGE_REPRESENTATIVE_SIZE: usize = 64;
pub(crate) const MASK_SEED_SIZE: usize = 64;

pub(crate) const REJECTION_SAMPLE_BOUND_SIGN: usize = 814;

/// The length of `context` is serialized to a single `u8`.
pub(crate) const CONTEXT_MAX_LEN: usize = 255;

// Handling of enums in eurydice is very limited.
// We therefore don't sue them here in all the places we could.
// See
// - https://github.com/AeneasVerif/eurydice/issues/123
// - https://github.com/AeneasVerif/eurydice/issues/122

/// ML-DSA-44-specific parameters
#[cfg(feature = "mldsa44")]
pub(crate) mod ml_dsa_44 {
    use super::Eta;
    use crate::constants::*;

    pub(crate) const ROWS_IN_A: usize = 4;
    pub(crate) const COLUMNS_IN_A: usize = 4;

    pub(crate) const ETA: Eta = Eta::Two;

    // To sample a value in the interval [-ETA, ETA], we can sample a value (say 'v')
    // in the interval [0, 2 * ETA] and then compute ETA - v. This can be done in
    // 3 bits when ETA is 2.
    pub(crate) const BITS_PER_ERROR_COEFFICIENT: usize = 3;

    pub(crate) const GAMMA1_EXPONENT: usize = 17;
    pub(crate) const GAMMA2: i32 = (FIELD_MODULUS - 1) / 88;

    // To sample a value in the interval [-(GAMMA - 1), GAMMA], we can sample a
    // value (say 'v') in the interval [0, (2 * GAMMA) - 1] and then compute
    // GAMMA - v. This can be done in 18 bits when GAMMA is 2^{17}.
    pub(crate) const BITS_PER_GAMMA1_COEFFICIENT: usize = 18;

    pub(crate) const MAX_ONES_IN_HINT: usize = 80;

    pub(crate) const ONES_IN_VERIFIER_CHALLENGE: usize = 39;

    pub(crate) const COMMITMENT_HASH_SIZE: usize = 32;

    // Commitment coefficients are in the interval: [0, ((FIELD_MODULUS − 1)/2γ2) − 1]
    // ((FIELD_MODULUS − 1)/2γ2) − 1 = 43, which means we need 6 bits to represent a
    // coefficient.
    pub(crate) const BITS_PER_COMMITMENT_COEFFICIENT: usize = 6;

    // Type aliases for ML-DSA-44
    pub(crate) const SIGNING_KEY_SIZE: usize = signing_key_size(
        ROWS_IN_A,
        COLUMNS_IN_A,
        error_ring_element_size(BITS_PER_ERROR_COEFFICIENT),
    );
    pub(crate) const VERIFICATION_KEY_SIZE: usize = verification_key_size(ROWS_IN_A);
    pub(crate) const SIGNATURE_SIZE: usize = signature_size(
        ROWS_IN_A,
        COLUMNS_IN_A,
        MAX_ONES_IN_HINT,
        COMMITMENT_HASH_SIZE,
        BITS_PER_GAMMA1_COEFFICIENT,
    );

    pub type MLDSA44KeyPair = crate::MLDSAKeyPair<VERIFICATION_KEY_SIZE, SIGNING_KEY_SIZE>;
    pub type MLDSA44Signature = crate::MLDSASignature<SIGNATURE_SIZE>;
    pub type MLDSA44SigningKey = crate::MLDSASigningKey<SIGNING_KEY_SIZE>;
    pub type MLDSA44VerificationKey = crate::MLDSAVerificationKey<VERIFICATION_KEY_SIZE>;
}

/// ML-DSA-65-specific parameters
#[cfg(feature = "mldsa65")]
pub(crate) mod ml_dsa_65 {
    use super::Eta;
    use crate::constants::*;

    pub(crate) const ROWS_IN_A: usize = 6;
    pub(crate) const COLUMNS_IN_A: usize = 5;

    pub(crate) const ETA: Eta = Eta::Four;

    // To sample a value in the interval [-ETA, ETA], we can sample a value (say 'v')
    // in the interval [0, 2 * ETA] and then compute ETA - v. This can be done in
    // 4 bits when ETA is 4.
    pub(crate) const BITS_PER_ERROR_COEFFICIENT: usize = 4;

    pub(crate) const GAMMA1_EXPONENT: usize = 19;
    pub(crate) const GAMMA2: i32 = (FIELD_MODULUS - 1) / 32;

    // To sample a value in the interval [-(GAMMA - 1), GAMMA], we can sample a
    // value (say 'v') in the interval [0, (2 * GAMMA) - 1] and then compute
    // GAMMA - v. This can be done in 20 bits when GAMMA is 2^{19}.
    pub(crate) const BITS_PER_GAMMA1_COEFFICIENT: usize = 20;

    pub(crate) const MAX_ONES_IN_HINT: usize = 55;

    pub(crate) const ONES_IN_VERIFIER_CHALLENGE: usize = 49;

    pub(crate) const COMMITMENT_HASH_SIZE: usize = 48;

    // Commitment coefficients are in the interval: [0, ((FIELD_MODULUS − 1)/2γ2) − 1]
    // ((FIELD_MODULUS − 1)/2γ2) − 1 = 15, which means we need 4 bits to represent a
    // coefficient.
    pub(crate) const BITS_PER_COMMITMENT_COEFFICIENT: usize = 4;

    // Type aliases for ML-DSA-65
    pub(crate) const SIGNING_KEY_SIZE: usize = signing_key_size(
        ROWS_IN_A,
        COLUMNS_IN_A,
        error_ring_element_size(BITS_PER_ERROR_COEFFICIENT),
    );
    pub(crate) const VERIFICATION_KEY_SIZE: usize = verification_key_size(ROWS_IN_A);
    pub(crate) const SIGNATURE_SIZE: usize = signature_size(
        ROWS_IN_A,
        COLUMNS_IN_A,
        MAX_ONES_IN_HINT,
        COMMITMENT_HASH_SIZE,
        BITS_PER_GAMMA1_COEFFICIENT,
    );

    pub type MLDSA65KeyPair = crate::MLDSAKeyPair<VERIFICATION_KEY_SIZE, SIGNING_KEY_SIZE>;
    pub type MLDSA65Signature = crate::MLDSASignature<SIGNATURE_SIZE>;
    pub type MLDSA65SigningKey = crate::MLDSASigningKey<SIGNING_KEY_SIZE>;
    pub type MLDSA65VerificationKey = crate::MLDSAVerificationKey<VERIFICATION_KEY_SIZE>;
}

/// ML-DSA-87-specific parameters
#[cfg(feature = "mldsa87")]
pub(crate) mod ml_dsa_87 {
    use super::Eta;
    use crate::constants::*;

    pub(crate) const ROWS_IN_A: usize = 8;
    pub(crate) const COLUMNS_IN_A: usize = 7;

    pub(crate) const ETA: Eta = Eta::Two;

    // To sample a value in the interval [-ETA, ETA], we can sample a value (say 'v')
    // in the interval [0, 2 * ETA] and then compute ETA - v. This can be done in
    // 3 bits when ETA is 2.
    pub(crate) const BITS_PER_ERROR_COEFFICIENT: usize = 3;

    pub(crate) const GAMMA1_EXPONENT: usize = 19;
    // To sample a value in the interval [-(GAMMA - 1), GAMMA], we can sample a
    // value (say 'v') in the interval [0, (2 * GAMMA) - 1] and then compute
    // GAMMA - v. This can be done in 20 bits when GAMMA is 2^{19}.
    pub(crate) const BITS_PER_GAMMA1_COEFFICIENT: usize = 20;

    pub(crate) const MAX_ONES_IN_HINT: usize = 75;

    pub(crate) const ONES_IN_VERIFIER_CHALLENGE: usize = 60;

    pub(crate) const GAMMA2: i32 = (FIELD_MODULUS - 1) / 32;

    // Commitment coefficients are in the interval: [0, ((FIELD_MODULUS − 1)/2γ2) − 1]
    // ((FIELD_MODULUS − 1)/2γ2) − 1 = 15, which means we need 4 bits to represent a
    // coefficient.
    pub(crate) const BITS_PER_COMMITMENT_COEFFICIENT: usize = 4;

    pub(crate) const COMMITMENT_HASH_SIZE: usize = 64;

    // Type aliases for ML-DSA-87
    pub(crate) const SIGNING_KEY_SIZE: usize = signing_key_size(
        ROWS_IN_A,
        COLUMNS_IN_A,
        error_ring_element_size(BITS_PER_ERROR_COEFFICIENT),
    );
    pub(crate) const VERIFICATION_KEY_SIZE: usize = verification_key_size(ROWS_IN_A);
    pub(crate) const SIGNATURE_SIZE: usize = signature_size(
        ROWS_IN_A,
        COLUMNS_IN_A,
        MAX_ONES_IN_HINT,
        COMMITMENT_HASH_SIZE,
        BITS_PER_GAMMA1_COEFFICIENT,
    );

    pub type MLDSA87KeyPair = crate::MLDSAKeyPair<VERIFICATION_KEY_SIZE, SIGNING_KEY_SIZE>;
    pub type MLDSA87Signature = crate::MLDSASignature<SIGNATURE_SIZE>;
    pub type MLDSA87SigningKey = crate::MLDSASigningKey<SIGNING_KEY_SIZE>;
    pub type MLDSA87VerificationKey = crate::MLDSAVerificationKey<VERIFICATION_KEY_SIZE>;
}

/// Eta values (parameter sets use a subset; `Two` is kept for spec completeness).
#[derive(Clone, Copy)]
pub(crate) enum Eta {
    #[allow(dead_code)]
    Two = 2,
    #[allow(dead_code)]
    Four = 4,
}

/// Gamma2 values
pub(crate) type Gamma2 = i32;
pub(crate) const GAMMA2_V261_888: Gamma2 = 261_888;
pub(crate) const GAMMA2_V95_232: Gamma2 = 95_232;

#[hax_lib::requires(ones_in_verifier_challenge <= 60)]
pub(crate) const fn beta(ones_in_verifier_challenge: usize, eta: Eta) -> i32 {
    // [eurydice] can't handle conversion of enum into a usize
    let eta_val: usize = match eta {
        Eta::Two => 2,
        Eta::Four => 4,
    };
    (ones_in_verifier_challenge * eta_val) as i32
}

#[hax_lib::requires(bits_per_error_coefficient <= 4)]
pub(crate) const fn error_ring_element_size(bits_per_error_coefficient: usize) -> usize {
    (bits_per_error_coefficient * COEFFICIENTS_IN_RING_ELEMENT) / 8
}

#[hax_lib::requires(bits_per_gamma1_coefficient <= 20)]
pub(crate) const fn gamma1_ring_element_size(bits_per_gamma1_coefficient: usize) -> usize {
    (bits_per_gamma1_coefficient * COEFFICIENTS_IN_RING_ELEMENT) / 8
}

#[hax_lib::requires(bits_per_commitment_coefficient <= 6)]
pub(crate) const fn commitment_ring_element_size(bits_per_commitment_coefficient: usize) -> usize {
    (bits_per_commitment_coefficient * COEFFICIENTS_IN_RING_ELEMENT) / 8
}

#[hax_lib::requires(bits_per_commitment_coefficient <= 6 && rows_in_a <= 8)]
pub(crate) const fn commitment_vector_size(
    bits_per_commitment_coefficient: usize,
    rows_in_a: usize,
) -> usize {
    commitment_ring_element_size(bits_per_commitment_coefficient) * rows_in_a
}

#[hax_lib::requires(rows_in_a <= 8 && columns_in_a <= 7 && error_ring_element_size <= 128)]
pub(crate) const fn signing_key_size(
    rows_in_a: usize,
    columns_in_a: usize,
    error_ring_element_size: usize,
) -> usize {
    SEED_FOR_A_SIZE +
        SEED_FOR_SIGNING_SIZE +
        BYTES_FOR_VERIFICATION_KEY_HASH +
        (rows_in_a + columns_in_a) * error_ring_element_size +
        rows_in_a * RING_ELEMENT_OF_T0S_SIZE
}

#[hax_lib::requires(rows_in_a <= 8)]
pub(crate) const fn verification_key_size(rows_in_a: usize) -> usize {
    SEED_FOR_A_SIZE +
        (COEFFICIENTS_IN_RING_ELEMENT *
            rows_in_a *
            (FIELD_MODULUS_MINUS_ONE_BIT_LENGTH - BITS_IN_LOWER_PART_OF_T)) /
            8
}

#[hax_lib::requires(rows_in_a <= 8 && columns_in_a <= 7 && max_ones_in_hint <= 80 && commitment_hash_size <= 64 && bits_per_gamma1_coefficient <= 20)]
pub(crate) const fn signature_size(
    rows_in_a: usize,
    columns_in_a: usize,
    max_ones_in_hint: usize,
    commitment_hash_size: usize,
    bits_per_gamma1_coefficient: usize,
) -> usize {
    commitment_hash_size +
        (columns_in_a * gamma1_ring_element_size(bits_per_gamma1_coefficient)) +
        max_ones_in_hint +
        rows_in_a
}