diff --git a/mldsa/mldsa_native.S b/mldsa/mldsa_native.S index cfed7a76c..7b895a4a5 100644 --- a/mldsa/mldsa_native.S +++ b/mldsa/mldsa_native.S @@ -547,9 +547,12 @@ #endif /* MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 */ #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) /* mldsa/src/native/api.h */ +#undef MLD_INTT_BOUND #undef MLD_NATIVE_API_H #undef MLD_NATIVE_FUNC_FALLBACK #undef MLD_NATIVE_FUNC_SUCCESS +#undef MLD_NTT_BOUND +#undef REDUCE32_RANGE_MAX /* mldsa/src/native/meta.h */ #undef MLD_NATIVE_META_H #if defined(MLD_SYS_AARCH64) diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 9a5e2f318..79661a7ff 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -544,9 +544,12 @@ #endif /* MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 */ #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) /* mldsa/src/native/api.h */ +#undef MLD_INTT_BOUND #undef MLD_NATIVE_API_H #undef MLD_NATIVE_FUNC_FALLBACK #undef MLD_NATIVE_FUNC_SUCCESS +#undef MLD_NTT_BOUND +#undef REDUCE32_RANGE_MAX /* mldsa/src/native/meta.h */ #undef MLD_NATIVE_META_H #if defined(MLD_SYS_AARCH64) diff --git a/mldsa/src/cbmc.h b/mldsa/src/cbmc.h index 72b8538f0..b1208440b 100644 --- a/mldsa/src/cbmc.h +++ b/mldsa/src/cbmc.h @@ -8,7 +8,6 @@ /*************************************************** * Basic replacements for __CPROVER_XXX contracts ***************************************************/ - #ifndef CBMC #define __contract__(x) @@ -16,6 +15,7 @@ #define cassert(x) #else /* !CBMC */ + #include #define __contract__(x) x @@ -128,6 +128,28 @@ #define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \ array_bound_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), (qvar_lb), \ (qvar_ub), (array_var), (value_lb), (value_ub)) + +#define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var) \ + __CPROVER_forall \ + { \ + unsigned qvar; \ + ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + ((array_var)[(qvar)]) == (old(* (int16_t (*)[(qvar_ub)])(array_var)))[(qvar)] \ + } + +#define array_unchanged(array_var, N) \ + array_unchanged_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), 0, (N), (array_var)) + +#define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var) \ + __CPROVER_forall \ + { \ + unsigned qvar; \ + ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + ((array_var)[(qvar)]) == (old(* (uint64_t (*)[(qvar_ub)])(array_var)))[(qvar)] \ + } + +#define array_unchanged_u64(array_var, N) \ + array_unchanged_u64_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), 0, (N), (array_var)) /* clang-format on */ /* Wrapper around array_bound operating on absolute values. diff --git a/mldsa/src/fips202/native/api.h b/mldsa/src/fips202/native/api.h index c527b6a26..4625c9a1a 100644 --- a/mldsa/src/fips202/native/api.h +++ b/mldsa/src/fips202/native/api.h @@ -46,10 +46,22 @@ */ #if defined(MLD_USE_FIPS202_X1_NATIVE) -static MLD_INLINE int mld_keccak_f1600_x1_native(uint64_t *state); -#endif +static MLD_INLINE int mld_keccak_f1600_x1_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 1)) +); +#endif /* MLD_USE_FIPS202_X1_NATIVE */ #if defined(MLD_USE_FIPS202_X4_NATIVE) -static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state); -#endif +static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 4)) +); +#endif /* MLD_USE_FIPS202_X4_NATIVE */ #endif /* !MLD_FIPS202_NATIVE_API_H */ diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 333bb0c7b..c52d345d9 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -38,6 +38,24 @@ */ #define MLD_NATIVE_FUNC_FALLBACK (-1) +/* Bound on absolute value of coefficients after NTT. + * + * NOTE: This is the same bound as in ntt.h and has to be kept + * in sync. */ +#define MLD_NTT_BOUND (9 * MLDSA_Q) + +/* Absolute exclusive upper bound for the output of the inverse NTT + * + * NOTE: This is the same bound as in ntt.h and has to be kept + * in sync. */ +#define MLD_INTT_BOUND MLDSA_Q + +/* Absolute bound for range of mld_reduce32() + * + * NOTE: This is the same bound as in reduce.h and has to be kept + * in sync. */ +/* check-magic: 6283009 == (REDUCE32_DOMAIN_MAX - 255 * MLDSA_Q + 1) */ +#define REDUCE32_RANGE_MAX 6283009 /* * This is the C<->native interface allowing for the drop-in of * native code for performance critical arithmetic components of ML-DSA. @@ -67,7 +85,16 @@ * * Arguments: - int32_t p[MLDSA_N]: pointer to in/output polynomial **************************************************/ -static MLD_INLINE int mld_ntt_native(int32_t p[MLDSA_N]); +static MLD_INLINE int mld_ntt_native(int32_t p[MLDSA_N]) +__contract__( + requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) + assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(p, 0, MLDSA_N, MLD_NTT_BOUND)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(p, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_NTT */ @@ -111,7 +138,16 @@ static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t p[MLDSA_N]); * * Arguments: - uint32_t p[MLDSA_N]: pointer to in/output polynomial **************************************************/ -static MLD_INLINE int mld_intt_native(int32_t p[MLDSA_N]); +static MLD_INLINE int mld_intt_native(int32_t p[MLDSA_N]) +__contract__( + requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) + assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(p, 0, MLDSA_N, MLD_INTT_BOUND)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(p, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_INTT */ #if defined(MLD_USE_NATIVE_REJ_UNIFORM) @@ -134,7 +170,16 @@ static MLD_INLINE int mld_intt_native(int32_t p[MLDSA_N]); **************************************************/ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len, const uint8_t *buf, - unsigned buflen); + unsigned buflen) +__contract__( + requires(len <= MLDSA_N) + requires(buflen <= ( 5 * 168) && buflen % 3 == 0) + requires(memory_no_alias(r, sizeof(int32_t) * len)) + requires(memory_no_alias(buf, buflen)) + assigns(memory_slice(r, sizeof(int32_t) * len)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len)) + ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> array_bound(r, 0, (unsigned) return_value, 0, MLDSA_Q)) +); #endif /* MLD_USE_NATIVE_REJ_UNIFORM */ #if defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2) @@ -157,7 +202,16 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len, **************************************************/ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len, const uint8_t *buf, - unsigned buflen); + unsigned buflen) +__contract__( + requires(len <= MLDSA_N) + requires(buflen <= (2 * 136)) + requires(memory_no_alias(r, sizeof(int32_t) * len)) + requires(memory_no_alias(buf, buflen)) + assigns(memory_slice(r, sizeof(int32_t) * len)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len)) + ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))) +); #endif /* MLD_USE_NATIVE_REJ_UNIFORM_ETA2 */ #if defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA4) @@ -180,7 +234,16 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len, **************************************************/ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len, const uint8_t *buf, - unsigned buflen); + unsigned buflen) +__contract__( + requires(len <= MLDSA_N) + requires(buflen <= (2 * 136)) + requires(memory_no_alias(r, sizeof(int32_t) * len)) + requires(memory_no_alias(buf, buflen)) + assigns(memory_slice(r, sizeof(int32_t) * len)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len)) + ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))) +); #endif /* MLD_USE_NATIVE_REJ_UNIFORM_ETA4 */ #if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_32) @@ -201,7 +264,20 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len, * - const int32_t *a: input polynomial **************************************************/ static MLD_INLINE int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0, - const int32_t *a); + const int32_t *a) +__contract__( + requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) + assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a1, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(a0, 0, MLDSA_N, MLDSA_GAMMA2+1)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_DECOMPOSE_32 */ #if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_88) @@ -222,7 +298,20 @@ static MLD_INLINE int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0, * - const int32_t *a: input polynomial **************************************************/ static MLD_INLINE int mld_poly_decompose_88_native(int32_t *a1, int32_t *a0, - const int32_t *a); + const int32_t *a) +__contract__( + requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) + assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a1, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(a0, 0, MLDSA_N, MLDSA_GAMMA2+1)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_DECOMPOSE_88 */ #if defined(MLD_USE_NATIVE_POLY_CADDQ) @@ -234,7 +323,16 @@ static MLD_INLINE int mld_poly_decompose_88_native(int32_t *a1, int32_t *a0, * * Arguments: - int32_t *a: pointer to input/output polynomial **************************************************/ -static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N]); +static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N]) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(array_abs_bound(a, 0, MLDSA_N, MLDSA_Q)) + assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(a, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_CADDQ */ #if defined(MLD_USE_NATIVE_POLY_USE_HINT_32) @@ -250,7 +348,18 @@ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N]); * - const int32_t *h: pointer to input hint polynomial **************************************************/ static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a, - const int32_t *h); + const int32_t *h) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + requires(array_bound(h, 0, MLDSA_N, 0, 2)) + assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(b, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(b, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_USE_HINT_32 */ #if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) @@ -266,7 +375,18 @@ static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a, * - const int32_t *h: pointer to input hint polynomial **************************************************/ static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a, - const int32_t *h); + const int32_t *h) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + requires(array_bound(h, 0, MLDSA_N, 0, 2)) + assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(b, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(b, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_USE_HINT_88 */ #if defined(MLD_USE_NATIVE_POLY_CHKNORM) @@ -282,7 +402,14 @@ static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a, * Returns 0 if the infinity norm is strictly smaller than B, and 1 * otherwise. B must not be larger than MLDSA_Q - REDUCE32_RANGE_MAX. **************************************************/ -static MLD_INLINE int mld_poly_chknorm_native(const int32_t *a, int32_t B); +static MLD_INLINE int mld_poly_chknorm_native(const int32_t *a, int32_t B) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(0 <= B && B <= MLDSA_Q - REDUCE32_RANGE_MAX) + requires(array_bound(a, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == 0) == array_abs_bound(a, 0, MLDSA_N, B)) +); #endif /* MLD_USE_NATIVE_POLY_CHKNORM */ #if defined(MLD_USE_NATIVE_POLYZ_UNPACK_17) @@ -296,7 +423,15 @@ static MLD_INLINE int mld_poly_chknorm_native(const int32_t *a, int32_t B); * Arguments: - int32_t *r: pointer to output polynomial * - const uint8_t *a: byte array with bit-packed polynomial **************************************************/ -static MLD_INLINE int mld_polyz_unpack_17_native(int32_t *r, const uint8_t *a); +static MLD_INLINE int mld_polyz_unpack_17_native(int32_t *r, const uint8_t *a) +__contract__( + requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) + assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(r, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(r, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYZ_UNPACK_17 */ #if defined(MLD_USE_NATIVE_POLYZ_UNPACK_19) @@ -310,7 +445,15 @@ static MLD_INLINE int mld_polyz_unpack_17_native(int32_t *r, const uint8_t *a); * Arguments: - int32_t *r: pointer to output polynomial * - const uint8_t *a: byte array with bit-packed polynomial **************************************************/ -static MLD_INLINE int mld_polyz_unpack_19_native(int32_t *r, const uint8_t *a); +static MLD_INLINE int mld_polyz_unpack_19_native(int32_t *r, const uint8_t *a) +__contract__( + requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) + assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(r, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(r, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYZ_UNPACK_19 */ #if defined(MLD_USE_NATIVE_POINTWISE_MONTGOMERY) @@ -328,7 +471,20 @@ static MLD_INLINE int mld_polyz_unpack_19_native(int32_t *r, const uint8_t *a); * - const int32_t b[MLDSA_N]: second input polynomial **************************************************/ static MLD_INLINE int mld_poly_pointwise_montgomery_native( - int32_t c[MLDSA_N], const int32_t a[MLDSA_N], const int32_t b[MLDSA_N]); + int32_t c[MLDSA_N], const int32_t a[MLDSA_N], const int32_t b[MLDSA_N]) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N)) + requires(array_abs_bound(a, 0, MLDSA_N, MLD_NTT_BOUND)) + requires(array_abs_bound(b, 0, MLDSA_N, MLD_NTT_BOUND)) + assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(c, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(a, 0, MLDSA_N, MLD_NTT_BOUND)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(b, 0, MLDSA_N, MLD_NTT_BOUND)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(c, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POINTWISE_MONTGOMERY */ #if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4) @@ -348,7 +504,20 @@ static MLD_INLINE int mld_poly_pointwise_montgomery_native( **************************************************/ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native( int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N], - const int32_t v[4][MLDSA_N]); + const int32_t v[4][MLDSA_N]) +__contract__( + requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(u, sizeof(int32_t) * 4 * MLDSA_N)) + requires(memory_no_alias(v, sizeof(int32_t) * 4 * MLDSA_N)) + requires(forall(l0, 0, 4, + array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q))) + requires(forall(l1, 0, 4, + array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND))) + assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 */ #if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5) @@ -368,7 +537,20 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native( **************************************************/ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native( int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N], - const int32_t v[5][MLDSA_N]); + const int32_t v[5][MLDSA_N]) +__contract__( + requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(u, sizeof(int32_t) * 5 * MLDSA_N)) + requires(memory_no_alias(v, sizeof(int32_t) * 5 * MLDSA_N)) + requires(forall(l0, 0, 5, + array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q))) + requires(forall(l1, 0, 5, + array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND))) + assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5 */ #if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7) @@ -388,7 +570,20 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native( **************************************************/ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native( int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N], - const int32_t v[7][MLDSA_N]); + const int32_t v[7][MLDSA_N]) +__contract__( + requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(u, sizeof(int32_t) * 7 * MLDSA_N)) + requires(memory_no_alias(v, sizeof(int32_t) * 7 * MLDSA_N)) + requires(forall(l0, 0, 7, + array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q))) + requires(forall(l1, 0, 7, + array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND))) + assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7 */ #endif /* !MLD_NATIVE_API_H */ diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index e60fc306b..04e402060 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -244,7 +244,6 @@ void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a, const mld_poly *b) { #if defined(MLD_USE_NATIVE_POINTWISE_MONTGOMERY) - /* TODO: proof */ int ret; mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND); mld_assert_abs_bound(b->coeffs, MLDSA_N, MLD_NTT_BOUND); @@ -368,7 +367,6 @@ __contract__( ensures(array_bound(a, 0, return_value, 0, MLDSA_Q)) ) { -/* TODO: CBMC proof based on mld_rej_uniform_native */ #if defined(MLD_USE_NATIVE_REJ_UNIFORM) int ret; mld_assert_bound(a, offset, 0, MLDSA_Q); @@ -704,7 +702,6 @@ MLD_INTERNAL_API uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B) { #if defined(MLD_USE_NATIVE_POLY_CHKNORM) - /* TODO: proof */ int ret; int success; mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX); diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index ba7ba25b2..1e1a5bf38 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -75,7 +75,6 @@ void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) #if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_88) && MLD_CONFIG_PARAMETER_SET == 44 int ret; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - /* TODO: proof */ ret = mld_poly_decompose_88_native(a1->coeffs, a0->coeffs, a->coeffs); if (ret == MLD_NATIVE_FUNC_SUCCESS) { @@ -88,7 +87,6 @@ void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) int ret; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - /* TODO: proof */ ret = mld_poly_decompose_32_native(a1->coeffs, a0->coeffs, a->coeffs); if (ret == MLD_NATIVE_FUNC_SUCCESS) { @@ -160,7 +158,6 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) int ret; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - /* TODO: proof */ ret = mld_poly_use_hint_88_native(b->coeffs, a->coeffs, h->coeffs); if (ret == MLD_NATIVE_FUNC_SUCCESS) { @@ -172,7 +169,6 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) int ret; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - /* TODO: proof */ ret = mld_poly_use_hint_32_native(b->coeffs, a->coeffs, h->coeffs); if (ret == MLD_NATIVE_FUNC_SUCCESS) { @@ -313,7 +309,6 @@ __contract__( ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) ) { -/* TODO: CBMC proof based on mld_rej_uniform_eta2_native */ #if MLDSA_ETA == 2 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2) int ret; mld_assert_abs_bound(a, offset, MLDSA_ETA + 1); @@ -327,7 +322,6 @@ __contract__( return res; } } -/* TODO: CBMC proof based on mld_rej_uniform_eta4_native */ #elif MLDSA_ETA == 4 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA4) int ret; mld_assert_abs_bound(a, offset, MLDSA_ETA + 1); @@ -867,7 +861,6 @@ MLD_INTERNAL_API void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) { #if defined(MLD_USE_NATIVE_POLYZ_UNPACK_17) && MLD_CONFIG_PARAMETER_SET == 44 - /* TODO: proof */ int ret; ret = mld_polyz_unpack_17_native(r->coeffs, a); if (ret == MLD_NATIVE_FUNC_SUCCESS) @@ -877,7 +870,6 @@ void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) } #elif defined(MLD_USE_NATIVE_POLYZ_UNPACK_19) && \ (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) - /* TODO: proof */ int ret; ret = mld_polyz_unpack_19_native(r->coeffs, a); if (ret == MLD_NATIVE_FUNC_SUCCESS) diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index 975b35b3e..13f052337 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -375,7 +375,6 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, { #if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4) && \ MLD_CONFIG_PARAMETER_SET == 44 - /* TODO: proof */ int ret; mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q); mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND); @@ -389,7 +388,6 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, } #elif defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5) && \ MLD_CONFIG_PARAMETER_SET == 65 - /* TODO: proof */ int ret; mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q); mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND); @@ -403,7 +401,6 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, } #elif defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7) && \ MLD_CONFIG_PARAMETER_SET == 87 - /* TODO: proof */ int ret; mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q); mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND); diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h new file mode 100644 index 000000000..92a11b566 --- /dev/null +++ b/proofs/cbmc/dummy_backend.h @@ -0,0 +1,30 @@ +/* + * Copyright (c) The mldsa-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + */ + +#ifndef MLD_DUMMY_ARITH_BACKEND_H +#define MLD_DUMMY_ARITH_BACKEND_H + + +#define MLD_USE_NATIVE_NTT +#define MLD_USE_NATIVE_INTT +#define MLD_USE_NATIVE_REJ_UNIFORM +#define MLD_USE_NATIVE_REJ_UNIFORM_ETA2 +#define MLD_USE_NATIVE_REJ_UNIFORM_ETA4 +#define MLD_USE_NATIVE_POLY_DECOMPOSE_32 +#define MLD_USE_NATIVE_POLY_DECOMPOSE_88 +#define MLD_USE_NATIVE_POLY_CADDQ +#define MLD_USE_NATIVE_POLY_USE_HINT_32 +#define MLD_USE_NATIVE_POLY_USE_HINT_88 +#define MLD_USE_NATIVE_POLY_CHKNORM +#define MLD_USE_NATIVE_POLYZ_UNPACK_17 +#define MLD_USE_NATIVE_POLYZ_UNPACK_19 +#define MLD_USE_NATIVE_POINTWISE_MONTGOMERY +#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 +#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5 +#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7 + +#include "../../mldsa/src/native/api.h" + +#endif /* !MLD_DUMMY_ARITH_BACKEND_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x1.h b/proofs/cbmc/dummy_backend_fips202_x1.h new file mode 100644 index 000000000..fb71bdc31 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x1.h @@ -0,0 +1,14 @@ +/* + * Copyright (c) The mldsa-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + */ + +#ifndef MLD_DUMMY_FIPS202X1_BACKEND_H +#define MLD_DUMMY_FIPS202X1_BACKEND_H + + +#define MLD_USE_FIPS202_X1_NATIVE + +#include "../../mldsa/src/fips202/native/api.h" + +#endif /* !MLD_DUMMY_FIPS202X1_BACKEND_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x4.h b/proofs/cbmc/dummy_backend_fips202_x4.h new file mode 100644 index 000000000..d84df09c5 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x4.h @@ -0,0 +1,14 @@ +/* + * Copyright (c) The mldsa-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + */ + +#ifndef MLD_DUMMY_FIPS202X4_BACKEND_H +#define MLD_DUMMY_FIPS202X4_BACKEND_H + + +#define MLD_USE_FIPS202_X4_NATIVE + +#include "../../mldsa/src/fips202/native/api.h" + +#endif /* !MLD_DUMMY_FIPS202X4_BACKEND_H */ diff --git a/proofs/cbmc/keccakf1600_permute_native/Makefile b/proofs/cbmc/keccakf1600_permute_native/Makefile new file mode 100644 index 000000000..ce5f5a76e --- /dev/null +++ b/proofs/cbmc/keccakf1600_permute_native/Makefile @@ -0,0 +1,55 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = keccakf1600_permute_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = keccakf1600_permute_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLD_CONFIG_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x1.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)keccakf1600_permute +USE_FUNCTION_CONTRACTS=mld_keccak_f1600_x1_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mld_keccakf1600_permute_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/keccakf1600_permute_native/keccakf1600_permute_native_harness.c b/proofs/cbmc/keccakf1600_permute_native/keccakf1600_permute_native_harness.c new file mode 100644 index 000000000..5647efb41 --- /dev/null +++ b/proofs/cbmc/keccakf1600_permute_native/keccakf1600_permute_native_harness.c @@ -0,0 +1,10 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include + +void harness(void) +{ + uint64_t *a; + mld_keccakf1600_permute(a); +} diff --git a/proofs/cbmc/keccakf1600x4_permute_native/Makefile b/proofs/cbmc/keccakf1600x4_permute_native/Makefile new file mode 100644 index 000000000..a0900c114 --- /dev/null +++ b/proofs/cbmc/keccakf1600x4_permute_native/Makefile @@ -0,0 +1,67 @@ +# Copyright (c) The mldsa-native project authors +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = keccakf1600x4_permute_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = keccakf1600x4_permute_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLD_CONFIG_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x4.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)keccakf1600x4_permute +USE_FUNCTION_CONTRACTS=mld_keccak_f1600_x4_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +# For this proof we tell CBMC to +# - not decompose arrays into their individual cells +# - to slice constraints that are not in the cone of influence of the proof obligations +# These options simplify them modelling of arrays and produce much more compact +# SMT files, leaving all array-type reasoning to the SMT solver. +# +# For functions that use large and multi-dimensional arrays, this yields +# a substantial improvement in proof performance. +CBMCFLAGS += --no-array-field-sensitivity +CBMCFLAGS += --slice-formula + +FUNCTION_NAME = mld_keccakf1600x4_permute_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/keccakf1600x4_permute_native/keccakf1600x4_permute_native_harness.c b/proofs/cbmc/keccakf1600x4_permute_native/keccakf1600x4_permute_native_harness.c new file mode 100644 index 000000000..ed72d896b --- /dev/null +++ b/proofs/cbmc/keccakf1600x4_permute_native/keccakf1600x4_permute_native_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mldsa-native project authors +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint64_t *s; + mld_keccakf1600x4_permute(s); +} diff --git a/proofs/cbmc/poly_caddq_native/Makefile b/proofs/cbmc/poly_caddq_native/Makefile new file mode 100644 index 000000000..94fc09e8b --- /dev/null +++ b/proofs/cbmc/poly_caddq_native/Makefile @@ -0,0 +1,55 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE =poly_caddq_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_caddq_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_caddq +USE_FUNCTION_CONTRACTS=mld_poly_caddq_native mld_poly_caddq_c +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_caddq_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_caddq_native/poly_caddq_native_harness.c b/proofs/cbmc/poly_caddq_native/poly_caddq_native_harness.c new file mode 100644 index 000000000..93de3b5b5 --- /dev/null +++ b/proofs/cbmc/poly_caddq_native/poly_caddq_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + + +void harness(void) +{ + mld_poly *a; + mld_poly_caddq(a); +} diff --git a/proofs/cbmc/poly_chknorm_native/Makefile b/proofs/cbmc/poly_chknorm_native/Makefile new file mode 100644 index 000000000..6643b2158 --- /dev/null +++ b/proofs/cbmc/poly_chknorm_native/Makefile @@ -0,0 +1,55 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE =poly_chknorm_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_chknorm_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_chknorm +USE_FUNCTION_CONTRACTS=mld_poly_chknorm_native mld_poly_chknorm_c +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_chknorm_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_chknorm_native/poly_chknorm_native_harness.c b/proofs/cbmc/poly_chknorm_native/poly_chknorm_native_harness.c new file mode 100644 index 000000000..890886154 --- /dev/null +++ b/proofs/cbmc/poly_chknorm_native/poly_chknorm_native_harness.c @@ -0,0 +1,13 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + + +void harness(void) +{ + mld_poly *a; + uint32_t r; + int32_t B; + r = mld_poly_chknorm(a, B); +} diff --git a/proofs/cbmc/poly_decompose_native/Makefile b/proofs/cbmc/poly_decompose_native/Makefile new file mode 100644 index 000000000..1f084308e --- /dev/null +++ b/proofs/cbmc/poly_decompose_native/Makefile @@ -0,0 +1,62 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_decompose_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_decompose_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_decompose +USE_FUNCTION_CONTRACTS= mld_poly_decompose_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_poly_decompose_88_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_poly_decompose_32_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_poly_decompose_32_native +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_decompose_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c b/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c new file mode 100644 index 000000000..309afec1e --- /dev/null +++ b/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + + +void harness(void) +{ + mld_poly *a0, *a1, *a; + mld_poly_decompose(a1, a0, a); +} diff --git a/proofs/cbmc/poly_invntt_tomont_native/Makefile b/proofs/cbmc/poly_invntt_tomont_native/Makefile new file mode 100644 index 000000000..fa1a0b623 --- /dev/null +++ b/proofs/cbmc/poly_invntt_tomont_native/Makefile @@ -0,0 +1,55 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_invntt_tomont_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_invntt_tomont_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_invntt_tomont +USE_FUNCTION_CONTRACTS=mld_intt_native mld_poly_invntt_tomont_c +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_invntt_tomont_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 9 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c b/proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c new file mode 100644 index 000000000..27fc2b9d6 --- /dev/null +++ b/proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c @@ -0,0 +1,10 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ + mld_poly *a; + mld_poly_invntt_tomont(a); +} diff --git a/proofs/cbmc/poly_ntt_native/Makefile b/proofs/cbmc/poly_ntt_native/Makefile new file mode 100644 index 000000000..80d47f049 --- /dev/null +++ b/proofs/cbmc/poly_ntt_native/Makefile @@ -0,0 +1,55 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_ntt_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_ntt_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_ntt +USE_FUNCTION_CONTRACTS=mld_ntt_native mld_poly_ntt_c +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_ntt + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c b/proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c new file mode 100644 index 000000000..a1720228f --- /dev/null +++ b/proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c @@ -0,0 +1,10 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ + mld_poly *a; + mld_poly_ntt(a); +} diff --git a/proofs/cbmc/poly_pointwise_montgomery_native/Makefile b/proofs/cbmc/poly_pointwise_montgomery_native/Makefile new file mode 100644 index 000000000..9e82db17c --- /dev/null +++ b/proofs/cbmc/poly_pointwise_montgomery_native/Makefile @@ -0,0 +1,55 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_pointwise_montgomery_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_pointwise_montgomery_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_pointwise_montgomery +USE_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery_native mld_poly_pointwise_montgomery_c +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_pointwise_montgomery_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 10 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_pointwise_montgomery_native/poly_pointwise_montgomery_native_harness.c b/proofs/cbmc/poly_pointwise_montgomery_native/poly_pointwise_montgomery_native_harness.c new file mode 100644 index 000000000..d885c2d5d --- /dev/null +++ b/proofs/cbmc/poly_pointwise_montgomery_native/poly_pointwise_montgomery_native_harness.c @@ -0,0 +1,10 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ + mld_poly *a, *b, *c; + mld_poly_pointwise_montgomery(c, a, b); +} diff --git a/proofs/cbmc/poly_use_hint_native/Makefile b/proofs/cbmc/poly_use_hint_native/Makefile new file mode 100644 index 000000000..800f888cd --- /dev/null +++ b/proofs/cbmc/poly_use_hint_native/Makefile @@ -0,0 +1,62 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_use_hint_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_use_hint_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_use_hint +USE_FUNCTION_CONTRACTS=mld_poly_use_hint_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_88_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_32_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_32_native +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_use_hint_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c b/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c new file mode 100644 index 000000000..360de6d3f --- /dev/null +++ b/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + + +void harness(void) +{ + mld_poly *a, *b, *h; + mld_poly_use_hint(b, a, h); +} diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/Makefile b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/Makefile new file mode 100644 index 000000000..5b507f981 --- /dev/null +++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/Makefile @@ -0,0 +1,64 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = polyvecl_pointwise_acc_montgomery_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = polyvecl_pointwise_acc_montgomery_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_acc_montgomery +USE_FUNCTION_CONTRACTS= mld_polyvecl_pointwise_acc_montgomery_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_polyvecl_pointwise_acc_montgomery_l4_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_polyvecl_pointwise_acc_montgomery_l5_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_polyvecl_pointwise_acc_montgomery_l7_native +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3 +CBMCFLAGS += --slice-formula +CBMCFLAGS += --no-array-field-sensitivity + +FUNCTION_NAME = polyvecl_pointwise_acc_montgomery_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/polyvecl_pointwise_acc_montgomery_native_harness.c b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/polyvecl_pointwise_acc_montgomery_native_harness.c new file mode 100644 index 000000000..927d5a220 --- /dev/null +++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/polyvecl_pointwise_acc_montgomery_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "polyvec.h" + +void harness(void) +{ + mld_poly *a; + mld_polyvecl *b, *c; + mld_polyvecl_pointwise_acc_montgomery(a, b, c); +} diff --git a/proofs/cbmc/polyz_unpack_native/Makefile b/proofs/cbmc/polyz_unpack_native/Makefile new file mode 100644 index 000000000..af621ba54 --- /dev/null +++ b/proofs/cbmc/polyz_unpack_native/Makefile @@ -0,0 +1,62 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = polyz_unpack_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = polyz_unpack_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_unpack +USE_FUNCTION_CONTRACTS=mld_polyz_unpack_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_polyz_unpack_17_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_polyz_unpack_19_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_polyz_unpack_19_native +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = polyz_unpack_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/polyz_unpack_native/polyz_unpack_native_harness.c b/proofs/cbmc/polyz_unpack_native/polyz_unpack_native_harness.c new file mode 100644 index 000000000..0dd46b69b --- /dev/null +++ b/proofs/cbmc/polyz_unpack_native/polyz_unpack_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + +void harness(void) +{ + mld_poly *a; + uint8_t *b; + mld_polyz_unpack(a, b); +} diff --git a/proofs/cbmc/rej_eta_native/Makefile b/proofs/cbmc/rej_eta_native/Makefile new file mode 100644 index 000000000..76fb0b117 --- /dev/null +++ b/proofs/cbmc/rej_eta_native/Makefile @@ -0,0 +1,62 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = rej_eta_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = rej_eta_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=mld_rej_eta +USE_FUNCTION_CONTRACTS= mld_rej_eta_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_rej_uniform_eta2_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_rej_uniform_eta4_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_rej_uniform_eta2_native +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = mld_rej_eta_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/rej_eta_native/rej_eta_native_harness.c b/proofs/cbmc/rej_eta_native/rej_eta_native_harness.c new file mode 100644 index 000000000..b540b7bf9 --- /dev/null +++ b/proofs/cbmc/rej_eta_native/rej_eta_native_harness.c @@ -0,0 +1,19 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +static unsigned int mld_rej_eta(int32_t *a, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen); + +void harness(void) +{ + int32_t *a; + unsigned int target; + unsigned int offset; + const uint8_t *buf; + unsigned int buflen; + + mld_rej_eta(a, target, offset, buf, buflen); +} diff --git a/proofs/cbmc/rej_uniform_native/Makefile b/proofs/cbmc/rej_uniform_native/Makefile new file mode 100644 index 000000000..15447a074 --- /dev/null +++ b/proofs/cbmc/rej_uniform_native/Makefile @@ -0,0 +1,55 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = rej_uniform_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = rej_uniform_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_rej_uniform +USE_FUNCTION_CONTRACTS=mld_rej_uniform_native mld_rej_uniform_c +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mld_rej_uniform_native_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mldsa/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c b/proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c new file mode 100644 index 000000000..e4b909748 --- /dev/null +++ b/proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c @@ -0,0 +1,19 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +static unsigned int mld_rej_uniform(int32_t *a, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen); + +void harness(void) +{ + int32_t *a; + unsigned int target; + unsigned int offset; + const uint8_t *buf; + unsigned int buflen; + + mld_rej_uniform(a, target, offset, buf, buflen); +}