diff --git a/mldsa/mldsa_native.S b/mldsa/mldsa_native.S index 93d98326e..e8c4b9284 100644 --- a/mldsa/mldsa_native.S +++ b/mldsa/mldsa_native.S @@ -419,6 +419,7 @@ #undef MLD_INLINE #undef MLD_MUST_CHECK_RETURN_VALUE #undef MLD_RESTRICT +#undef MLD_STATIC_TESTABLE #undef MLD_SYS_AARCH64 #undef MLD_SYS_AARCH64_EB #undef MLD_SYS_APPLE diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 156a9bb3b..2972ed33d 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -416,6 +416,7 @@ #undef MLD_INLINE #undef MLD_MUST_CHECK_RETURN_VALUE #undef MLD_RESTRICT +#undef MLD_STATIC_TESTABLE #undef MLD_SYS_AARCH64 #undef MLD_SYS_AARCH64_EB #undef MLD_SYS_APPLE diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index 61405469f..e60fc306b 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -50,23 +50,17 @@ void mld_poly_reduce(mld_poly *a) mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX); } - -MLD_INTERNAL_API -void mld_poly_caddq(mld_poly *a) +MLD_STATIC_TESTABLE void mld_poly_caddq_c(mld_poly *a) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) + assigns(memory_slice(a, sizeof(mld_poly))) + ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) +) { unsigned int i; mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); -#if defined(MLD_USE_NATIVE_POLY_CADDQ) - { - int ret; - ret = mld_poly_caddq_native(a->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - return; - } - } -#endif /* MLD_USE_NATIVE_POLY_CADDQ */ + for (i = 0; i < MLDSA_N; ++i) __loop__( invariant(i <= MLDSA_N) @@ -80,6 +74,22 @@ void mld_poly_caddq(mld_poly *a) mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); } +MLD_INTERNAL_API +void mld_poly_caddq(mld_poly *a) +{ +#if defined(MLD_USE_NATIVE_POLY_CADDQ) + int ret; + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); + ret = mld_poly_caddq_native(a->coeffs); + if (ret == MLD_NATIVE_FUNC_SUCCESS) + { + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + return; + } +#endif /* MLD_USE_NATIVE_POLY_CADDQ */ + mld_poly_caddq_c(a); +} + /* Reference: We use destructive version (output=first input) to avoid * reasoning about aliasing in the CBMC specification */ MLD_INTERNAL_API @@ -142,63 +152,82 @@ void mld_poly_shiftl(mld_poly *a) mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); } +MLD_STATIC_TESTABLE void mld_poly_ntt_c(mld_poly *a) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) + assigns(memory_slice(a, sizeof(mld_poly))) + ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) +) +{ + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); + mld_ntt(a->coeffs); + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND); +} + MLD_INTERNAL_API void mld_poly_ntt(mld_poly *a) { - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); #if defined(MLD_USE_NATIVE_NTT) + int ret; + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); + ret = mld_ntt_native(a->coeffs); + if (ret == MLD_NATIVE_FUNC_SUCCESS) { - int ret; - ret = mld_ntt_native(a->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND); - return; - } + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND); + return; } #endif /* MLD_USE_NATIVE_NTT */ - mld_ntt(a->coeffs); - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND); + mld_poly_ntt_c(a); +} + +MLD_STATIC_TESTABLE void mld_poly_invntt_tomont_c(mld_poly *a) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) + assigns(memory_slice(a, sizeof(mld_poly))) + ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_INTT_BOUND)) +) +{ + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); + mld_invntt_tomont(a->coeffs); + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_INTT_BOUND); } + MLD_INTERNAL_API void mld_poly_invntt_tomont(mld_poly *a) { - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); #if defined(MLD_USE_NATIVE_INTT) + int ret; + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); + ret = mld_intt_native(a->coeffs); + if (ret == MLD_NATIVE_FUNC_SUCCESS) { - int ret; - ret = mld_intt_native(a->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_INTT_BOUND); - return; - } + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_INTT_BOUND); + return; } #endif /* MLD_USE_NATIVE_INTT */ - mld_invntt_tomont(a->coeffs); - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_INTT_BOUND); + mld_poly_invntt_tomont_c(a); } -MLD_INTERNAL_API -void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a, - const mld_poly *b) +MLD_STATIC_TESTABLE void mld_poly_pointwise_montgomery_c(mld_poly *c, + const mld_poly *a, + const mld_poly *b) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(memory_no_alias(b, sizeof(mld_poly))) + requires(memory_no_alias(c, sizeof(mld_poly))) + requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) + requires(array_abs_bound(b->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) + assigns(memory_slice(c, sizeof(mld_poly))) + ensures(array_abs_bound(c->coeffs, 0, MLDSA_N, MLDSA_Q)) +) { unsigned int i; mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND); mld_assert_abs_bound(b->coeffs, MLDSA_N, MLD_NTT_BOUND); -#if defined(MLD_USE_NATIVE_POINTWISE_MONTGOMERY) - { - /* TODO: proof */ - int ret; - ret = mld_poly_pointwise_montgomery_native(c->coeffs, a->coeffs, b->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_abs_bound(c->coeffs, MLDSA_N, MLDSA_Q); - return; - } - } -#endif /* MLD_USE_NATIVE_POINTWISE_MONTGOMERY */ + for (i = 0; i < MLDSA_N; ++i) __loop__( invariant(i <= MLDSA_N) @@ -207,10 +236,28 @@ void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a, { c->coeffs[i] = mld_montgomery_reduce((int64_t)a->coeffs[i] * b->coeffs[i]); } - mld_assert_abs_bound(c->coeffs, MLDSA_N, MLDSA_Q); } +MLD_INTERNAL_API +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); + ret = mld_poly_pointwise_montgomery_native(c->coeffs, a->coeffs, b->coeffs); + if (ret == MLD_NATIVE_FUNC_SUCCESS) + { + mld_assert_abs_bound(c->coeffs, MLDSA_N, MLDSA_Q); + return; + } +#endif /* MLD_USE_NATIVE_POINTWISE_MONTGOMERY */ + mld_poly_pointwise_montgomery_c(c, a, b); +} + MLD_INTERNAL_API void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a) { @@ -233,7 +280,57 @@ void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a) mld_assert_bound(a1->coeffs, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1); } +#define POLY_UNIFORM_NBLOCKS \ + ((768 + STREAM128_BLOCKBYTES - 1) / STREAM128_BLOCKBYTES) +/* Reference: `mld_rej_uniform()` in the reference implementation @[REF]. + * - Our signature differs from the reference implementation + * in that it adds the offset and always expects the base of the + * target buffer. This avoids shifting the buffer base in the + * caller, which appears tricky to reason about. */ +MLD_STATIC_TESTABLE unsigned int mld_rej_uniform_c(int32_t *a, + unsigned int target, + unsigned int offset, + const uint8_t *buf, + unsigned int buflen) +__contract__( + requires(offset <= target && target <= MLDSA_N) + requires(buflen <= (POLY_UNIFORM_NBLOCKS * STREAM128_BLOCKBYTES) && buflen % 3 == 0) + requires(memory_no_alias(a, sizeof(int32_t) * target)) + requires(memory_no_alias(buf, buflen)) + requires(array_bound(a, 0, offset, 0, MLDSA_Q)) + assigns(memory_slice(a, sizeof(int32_t) * target)) + ensures(offset <= return_value && return_value <= target) + ensures(array_bound(a, 0, return_value, 0, MLDSA_Q)) +) +{ + unsigned int ctr, pos; + uint32_t t; + mld_assert_bound(a, offset, 0, MLDSA_Q); + ctr = offset; + pos = 0; + /* pos + 3 cannot overflow due to the assumption + buflen <= (POLY_UNIFORM_NBLOCKS * STREAM128_BLOCKBYTES) */ + while (ctr < target && pos + 3 <= buflen) + __loop__( + invariant(offset <= ctr && ctr <= target && pos <= buflen) + invariant(array_bound(a, 0, ctr, 0, MLDSA_Q))) + { + t = buf[pos++]; + t |= (uint32_t)buf[pos++] << 8; + t |= (uint32_t)buf[pos++] << 16; + t &= 0x7FFFFF; + + if (t < MLDSA_Q) + { + a[ctr++] = (int32_t)t; + } + } + + mld_assert_bound(a, ctr, 0, MLDSA_Q); + + return ctr; +} /************************************************* * Name: mld_rej_uniform * @@ -257,8 +354,6 @@ void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a) * in that it adds the offset and always expects the base of the * target buffer. This avoids shifting the buffer base in the * caller, which appears tricky to reason about. */ -#define POLY_UNIFORM_NBLOCKS \ - ((768 + STREAM128_BLOCKBYTES - 1) / STREAM128_BLOCKBYTES) static unsigned int mld_rej_uniform(int32_t *a, unsigned int target, unsigned int offset, const uint8_t *buf, unsigned int buflen) @@ -273,15 +368,12 @@ __contract__( ensures(array_bound(a, 0, return_value, 0, MLDSA_Q)) ) { - unsigned int ctr, pos; - uint32_t t; - mld_assert_bound(a, offset, 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); if (offset == 0) { - int ret; ret = mld_rej_uniform_native(a, target, buf, buflen); if (ret != MLD_NATIVE_FUNC_FALLBACK) { @@ -292,29 +384,7 @@ __contract__( } #endif /* MLD_USE_NATIVE_REJ_UNIFORM */ - ctr = offset; - pos = 0; - /* pos + 3 cannot overflow due to the assumption - buflen <= (POLY_UNIFORM_NBLOCKS * STREAM128_BLOCKBYTES) */ - while (ctr < target && pos + 3 <= buflen) - __loop__( - invariant(offset <= ctr && ctr <= target && pos <= buflen) - invariant(array_bound(a, 0, ctr, 0, MLDSA_Q))) - { - t = buf[pos++]; - t |= (uint32_t)buf[pos++] << 8; - t |= (uint32_t)buf[pos++] << 16; - t &= 0x7FFFFF; - - if (t < MLDSA_Q) - { - a[ctr++] = (int32_t)t; - } - } - - mld_assert_bound(a, ctr, 0, MLDSA_Q); - - return ctr; + return mld_rej_uniform_c(a, target, offset, buf, buflen); } /* Reference: poly_uniform() in the reference implementation @[REF]. @@ -578,50 +648,18 @@ void mld_polyt0_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYT0_PACKEDBYTES]) (1 << (MLDSA_D - 1)) + 1); } -/* Reference: explicitly checks the bound B to be <= (MLDSA_Q - 1) / 8). - * This is unnecessary as it's always a compile-time constant. - * We instead model it as a precondition. - * Checking the bound is performed using a conditional arguing - * that it is okay to leak which coefficient violates the bound (while the - * coefficient itself must remain secret). - * We instead perform everything in constant-time. - * Also it is sufficient to check that it is smaller than - * MLDSA_Q - REDUCE32_RANGE_MAX > (MLDSA_Q - 1) / 8). - */ -MLD_INTERNAL_API -uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B) +MLD_STATIC_TESTABLE uint32_t mld_poly_chknorm_c(const mld_poly *a, int32_t B) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(0 <= B && B <= MLDSA_Q - REDUCE32_RANGE_MAX) + requires(array_bound(a->coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX)) + ensures(return_value == 0 || return_value == 0xFFFFFFFF) + ensures((return_value == 0) == array_abs_bound(a->coeffs, 0, MLDSA_N, B)) +) { unsigned int i; uint32_t t = 0; mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX); -#if defined(MLD_USE_NATIVE_POLY_CHKNORM) - { - /* TODO: proof */ - int ret; - int success; - /* The native backend returns 0 if all coefficients are within the bound, - * 1 if at least one coefficient exceeds the bound, and - * -1 (MLD_NATIVE_FUNC_FALLBACK) if the platform does not have the - * required capabilities to run the native function. - */ - ret = mld_poly_chknorm_native(a->coeffs, B); - - success = (ret != MLD_NATIVE_FUNC_FALLBACK); - /* Constant-time: It would be fine to leak the return value of chknorm - * entirely (as it is fine to leak if any coefficient exceeded the bound or - * not). However, it is cleaner to perform declassification in sign.c. - * Hence, here we only declassify if the native function returned - * MLD_NATIVE_FUNC_FALLBACK or not (which solely depends on system - * capabilities). - */ - MLD_CT_TESTING_DECLASSIFY(&success, sizeof(int)); - if (success) - { - /* Convert 0 / 1 to 0 / 0xFFFFFFFF here */ - return 0U - (uint32_t)ret; - } - } -#endif /* MLD_USE_NATIVE_POLY_CHKNORM */ for (i = 0; i < MLDSA_N; ++i) __loop__( invariant(i <= MLDSA_N) @@ -652,6 +690,49 @@ uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B) return t; } +/* Reference: explicitly checks the bound B to be <= (MLDSA_Q - 1) / 8). + * This is unnecessary as it's always a compile-time constant. + * We instead model it as a precondition. + * Checking the bound is performed using a conditional arguing + * that it is okay to leak which coefficient violates the bound (while the + * coefficient itself must remain secret). + * We instead perform everything in constant-time. + * Also it is sufficient to check that it is smaller than + * MLDSA_Q - REDUCE32_RANGE_MAX > (MLDSA_Q - 1) / 8). + */ +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); + /* The native backend returns 0 if all coefficients are within the bound, + * 1 if at least one coefficient exceeds the bound, and + * -1 (MLD_NATIVE_FUNC_FALLBACK) if the platform does not have the + * required capabilities to run the native function. + */ + ret = mld_poly_chknorm_native(a->coeffs, B); + + success = (ret != MLD_NATIVE_FUNC_FALLBACK); + /* Constant-time: It would be fine to leak the return value of chknorm + * entirely (as it is fine to leak if any coefficient exceeded the bound or + * not). However, it is cleaner to perform declassification in sign.c. + * Hence, here we only declassify if the native function returned + * MLD_NATIVE_FUNC_FALLBACK or not (which solely depends on system + * capabilities). + */ + MLD_CT_TESTING_DECLASSIFY(&success, sizeof(int)); + if (success) + { + /* Convert 0 / 1 to 0 / 0xFFFFFFFF here */ + return 0U - (uint32_t)ret; + } +#endif /* MLD_USE_NATIVE_POLY_CHKNORM */ + return mld_poly_chknorm_c(a, B); +} + #else /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */ MLD_EMPTY_CU(mld_poly) #endif /* MLD_CONFIG_MULTILEVEL_NO_SHARED */ diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index af83bbf28..ba7ba25b2 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -32,44 +32,28 @@ * of mldsa-native (e.g. with varying parameter sets) * within a single compilation unit. */ #define mld_rej_eta MLD_ADD_PARAM_SET(mld_rej_eta) +#define mld_rej_eta_c MLD_ADD_PARAM_SET(mld_rej_eta_c) +#define mld_poly_decompose_c MLD_ADD_PARAM_SET(mld_poly_decompose_c) +#define mld_poly_use_hint_c MLD_ADD_PARAM_SET(mld_poly_use_hint_c) +#define mld_polyz_unpack_c MLD_ADD_PARAM_SET(mld_polyz_unpack_c) /* End of parameter set namespacing */ -MLD_INTERNAL_API -void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) + +MLD_STATIC_TESTABLE void mld_poly_decompose_c(mld_poly *a1, mld_poly *a0, + const mld_poly *a) +__contract__( + requires(memory_no_alias(a1, sizeof(mld_poly))) + requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(a1, sizeof(mld_poly))) + assigns(memory_slice(a0, sizeof(mld_poly))) + ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1)) +) { unsigned int i; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); -#if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_88) && MLD_CONFIG_PARAMETER_SET == 44 - { - int ret; - /* TODO: proof */ - ret = mld_poly_decompose_88_native(a1->coeffs, a0->coeffs, a->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2 + 1); - mld_assert_bound(a1->coeffs, MLDSA_N, 0, - (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); - return; - } - } -#elif defined(MLD_USE_NATIVE_POLY_DECOMPOSE_32) && \ - (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) - { - int ret; - /* TODO: proof */ - ret = mld_poly_decompose_32_native(a1->coeffs, a0->coeffs, a->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2 + 1); - mld_assert_bound(a1->coeffs, MLDSA_N, 0, - (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); - return; - } - } -#endif /* !(MLD_USE_NATIVE_POLY_DECOMPOSE_88 && MLD_CONFIG_PARAMETER_SET == \ - 44) && MLD_USE_NATIVE_POLY_DECOMPOSE_32 && (MLD_CONFIG_PARAMETER_SET \ - == 65 || MLD_CONFIG_PARAMETER_SET == 87) */ - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); for (i = 0; i < MLDSA_N; ++i) __loop__( assigns(i, memory_slice(a0, sizeof(mld_poly)), memory_slice(a1, sizeof(mld_poly))) @@ -85,6 +69,40 @@ void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) mld_assert_bound(a1->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); } +MLD_INTERNAL_API +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) + { + mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2 + 1); + mld_assert_bound(a1->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); + return; + } +#elif defined(MLD_USE_NATIVE_POLY_DECOMPOSE_32) && \ + (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) + { + mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2 + 1); + mld_assert_bound(a1->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); + return; + } +#endif /* !(MLD_USE_NATIVE_POLY_DECOMPOSE_88 && MLD_CONFIG_PARAMETER_SET == \ + 44) && MLD_USE_NATIVE_POLY_DECOMPOSE_32 && (MLD_CONFIG_PARAMETER_SET \ + == 65 || MLD_CONFIG_PARAMETER_SET == 87) */ + mld_poly_decompose_c(a1, a0, a); +} + MLD_INTERNAL_API unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, const mld_poly *a1) @@ -108,40 +126,21 @@ unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, return s; } -MLD_INTERNAL_API -void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) +MLD_STATIC_TESTABLE void mld_poly_use_hint_c(mld_poly *b, const mld_poly *a, + const mld_poly *h) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(memory_no_alias(b, sizeof(mld_poly))) + requires(memory_no_alias(h, sizeof(mld_poly))) + requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) + assigns(memory_slice(b, sizeof(mld_poly))) + ensures(array_bound(b->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) +) { unsigned int i; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); -#if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) && MLD_CONFIG_PARAMETER_SET == 44 - { - int ret; - /* TODO: proof */ - ret = mld_poly_use_hint_88_native(b->coeffs, a->coeffs, h->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_bound(b->coeffs, MLDSA_N, 0, - (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); - return; - } - } -#elif defined(MLD_USE_NATIVE_POLY_USE_HINT_32) && \ - (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) - { - int ret; - /* TODO: proof */ - ret = mld_poly_use_hint_32_native(b->coeffs, a->coeffs, h->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_bound(b->coeffs, MLDSA_N, 0, - (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); - return; - } - } -#endif /* !(MLD_USE_NATIVE_POLY_USE_HINT_88 && MLD_CONFIG_PARAMETER_SET == 44) \ - && MLD_USE_NATIVE_POLY_USE_HINT_32 && (MLD_CONFIG_PARAMETER_SET == \ - 65 || MLD_CONFIG_PARAMETER_SET == 87) */ for (i = 0; i < MLDSA_N; ++i) __loop__( @@ -154,6 +153,38 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); } +MLD_INTERNAL_API +void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) +{ +#if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) && MLD_CONFIG_PARAMETER_SET == 44 + 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) + { + mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); + return; + } +#elif defined(MLD_USE_NATIVE_POLY_USE_HINT_32) && \ + (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) + 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) + { + mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); + return; + } +#endif /* !(MLD_USE_NATIVE_POLY_USE_HINT_88 && MLD_CONFIG_PARAMETER_SET == 44) \ + && MLD_USE_NATIVE_POLY_USE_HINT_32 && (MLD_CONFIG_PARAMETER_SET == \ + 65 || MLD_CONFIG_PARAMETER_SET == 87) */ + mld_poly_use_hint_c(b, a, h); +} + /************************************************* * Name: mld_rej_eta * @@ -194,9 +225,11 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) #else /* MLDSA_ETA == 4 */ #error "Invalid value of MLDSA_ETA" #endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ -static unsigned int mld_rej_eta(int32_t *a, unsigned int target, - unsigned int offset, const uint8_t *buf, - unsigned int buflen) + +MLD_STATIC_TESTABLE unsigned int mld_rej_eta_c(int32_t *a, unsigned int target, + unsigned int offset, + const uint8_t *buf, + unsigned int buflen) __contract__( requires(offset <= target && target <= MLDSA_N) requires(buflen <= (POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)) @@ -212,36 +245,6 @@ __contract__( int t_valid; uint32_t t0, t1; mld_assert_abs_bound(a, offset, MLDSA_ETA + 1); - -/* TODO: CBMC proof based on mld_rej_uniform_eta2_native */ -#if MLDSA_ETA == 2 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2) - if (offset == 0) - { - int ret; - ret = mld_rej_uniform_eta2_native(a, target, buf, buflen); - if (ret != MLD_NATIVE_FUNC_FALLBACK) - { - unsigned res = (unsigned)ret; - mld_assert_abs_bound(a, res, MLDSA_ETA + 1); - return res; - } - } -/* TODO: CBMC proof based on mld_rej_uniform_eta4_native */ -#elif MLDSA_ETA == 4 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA4) - if (offset == 0) - { - int ret; - ret = mld_rej_uniform_eta4_native(a, target, buf, buflen); - if (ret != MLD_NATIVE_FUNC_FALLBACK) - { - unsigned res = (unsigned)ret; - mld_assert_abs_bound(a, res, MLDSA_ETA + 1); - return res; - } - } -#endif /* !(MLDSA_ETA == 2 && MLD_USE_NATIVE_REJ_UNIFORM_ETA2) && MLDSA_ETA == \ - 4 && MLD_USE_NATIVE_REJ_UNIFORM_ETA4 */ - ctr = offset; pos = 0; while (ctr < target && pos < buflen) @@ -296,6 +299,54 @@ __contract__( return ctr; } +static unsigned int mld_rej_eta(int32_t *a, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen) +__contract__( + requires(offset <= target && target <= MLDSA_N) + requires(buflen <= (POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)) + requires(memory_no_alias(a, sizeof(int32_t) * target)) + requires(memory_no_alias(buf, buflen)) + requires(array_abs_bound(a, 0, offset, MLDSA_ETA + 1)) + assigns(memory_slice(a, sizeof(int32_t) * target)) + ensures(offset <= return_value && return_value <= target) + 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); + if (offset == 0) + { + ret = mld_rej_uniform_eta2_native(a, target, buf, buflen); + if (ret != MLD_NATIVE_FUNC_FALLBACK) + { + unsigned res = (unsigned)ret; + mld_assert_abs_bound(a, res, MLDSA_ETA + 1); + 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); + if (offset == 0) + { + ret = mld_rej_uniform_eta4_native(a, target, buf, buflen); + if (ret != MLD_NATIVE_FUNC_FALLBACK) + { + unsigned res = (unsigned)ret; + mld_assert_abs_bound(a, res, MLDSA_ETA + 1); + return res; + } + } +#endif /* !(MLDSA_ETA == 2 && MLD_USE_NATIVE_REJ_UNIFORM_ETA2) && MLDSA_ETA == \ + 4 && MLD_USE_NATIVE_REJ_UNIFORM_ETA4 */ + + return mld_rej_eta_c(a, target, offset, buf, buflen); +} + #if !defined(MLD_CONFIG_SERIAL_FIPS202_ONLY) MLD_INTERNAL_API void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, @@ -747,33 +798,16 @@ void mld_polyz_pack(uint8_t r[MLDSA_POLYZ_PACKEDBYTES], const mld_poly *a) #endif /* MLD_CONFIG_PARAMETER_SET != 44 */ } -MLD_INTERNAL_API -void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) +MLD_STATIC_TESTABLE void mld_polyz_unpack_c( + mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) +__contract__( + requires(memory_no_alias(r, sizeof(mld_poly))) + requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) + assigns(memory_slice(r, sizeof(mld_poly))) + ensures(array_bound(r->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) +) { unsigned int i; -#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) - { - mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); - return; - } -#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) - { - mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); - return; - } -#endif /* !(MLD_USE_NATIVE_POLYZ_UNPACK_17 && MLD_CONFIG_PARAMETER_SET == 44) \ - && MLD_USE_NATIVE_POLYZ_UNPACK_19 && (MLD_CONFIG_PARAMETER_SET == 65 \ - || MLD_CONFIG_PARAMETER_SET == 87) */ - #if MLD_CONFIG_PARAMETER_SET == 44 for (i = 0; i < MLDSA_N / 4; ++i) __loop__( @@ -829,6 +863,35 @@ void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); } +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) + { + mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); + return; + } +#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) + { + mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); + return; + } +#endif /* !(MLD_USE_NATIVE_POLYZ_UNPACK_17 && MLD_CONFIG_PARAMETER_SET == 44) \ + && MLD_USE_NATIVE_POLYZ_UNPACK_19 && (MLD_CONFIG_PARAMETER_SET == 65 \ + || MLD_CONFIG_PARAMETER_SET == 87) */ + + mld_polyz_unpack_c(r, a); +} + MLD_INTERNAL_API void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) { @@ -864,6 +927,10 @@ void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. * Don't modify by hand -- this is auto-generated by scripts/autogen. */ #undef mld_rej_eta +#undef mld_rej_eta_c +#undef mld_poly_decompose_c +#undef mld_poly_use_hint_c +#undef mld_polyz_unpack_c #undef POLY_UNIFORM_ETA_NBLOCKS #undef POLY_UNIFORM_ETA_NBLOCKS #undef POLY_UNIFORM_GAMMA1_NBLOCKS diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index aa40213c7..975b35b3e 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -25,6 +25,8 @@ * with native backends, which are currently not yet namespaced. */ #define mld_polymat_permute_bitrev_to_custom \ MLD_ADD_PARAM_SET(mld_polymat_permute_bitrev_to_custom) +#define mld_polyvecl_pointwise_acc_montgomery_c \ + MLD_ADD_PARAM_SET(mld_polyvecl_pointwise_acc_montgomery_c) /* Helper function to ensure that the polynomial entries in the output * of mld_polyvec_matrix_expand use the standard (bitreversed) ordering @@ -323,54 +325,95 @@ void mld_polyvecl_pointwise_poly_montgomery(mld_polyvecl *r, const mld_poly *a, mld_assert_abs_bound_2d(r->vec, MLDSA_L, MLDSA_N, MLDSA_Q); } -MLD_INTERNAL_API -void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, - const mld_polyvecl *v) +MLD_STATIC_TESTABLE void mld_polyvecl_pointwise_acc_montgomery_c( + mld_poly *w, const mld_polyvecl *u, const mld_polyvecl *v) +__contract__( + requires(memory_no_alias(w, sizeof(mld_poly))) + requires(memory_no_alias(u, sizeof(mld_polyvecl))) + requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(forall(l0, 0, MLDSA_L, + array_bound(u->vec[l0].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) + requires(forall(l1, 0, MLDSA_L, + array_abs_bound(v->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) + assigns(memory_slice(w, sizeof(mld_poly))) + ensures(array_abs_bound(w->coeffs, 0, MLDSA_N, MLDSA_Q)) +) { unsigned int i, j; 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); -#if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4) && \ - MLD_CONFIG_PARAMETER_SET == 44 + for (i = 0; i < MLDSA_N; i++) + __loop__( + assigns(i, j, memory_slice(w, sizeof(mld_poly))) + invariant(i <= MLDSA_N) + invariant(array_abs_bound(w->coeffs, 0, i, MLDSA_Q)) + ) { - /* TODO: proof */ - int ret; - ret = mld_polyvecl_pointwise_acc_montgomery_l4_native( - w->coeffs, (const int32_t(*)[MLDSA_N])u->vec, - (const int32_t(*)[MLDSA_N])v->vec); - if (ret == MLD_NATIVE_FUNC_SUCCESS) + int64_t t = 0; + int32_t r; + for (j = 0; j < MLDSA_L; j++) + __loop__( + assigns(j, t) + invariant(j <= MLDSA_L) + invariant(t >= -(int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1)) + invariant(t <= (int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1)) + ) { - mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q); - return; + t += (int64_t)u->vec[j].coeffs[i] * v->vec[j].coeffs[i]; } + + r = mld_montgomery_reduce(t); + w->coeffs[i] = r; + } + + mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q); +} + +MLD_INTERNAL_API +void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, + const mld_polyvecl *v) +{ +#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); + ret = mld_polyvecl_pointwise_acc_montgomery_l4_native( + w->coeffs, (const int32_t(*)[MLDSA_N])u->vec, + (const int32_t(*)[MLDSA_N])v->vec); + if (ret == MLD_NATIVE_FUNC_SUCCESS) + { + mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q); + return; } #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); + ret = mld_polyvecl_pointwise_acc_montgomery_l5_native( + w->coeffs, (const int32_t(*)[MLDSA_N])u->vec, + (const int32_t(*)[MLDSA_N])v->vec); + if (ret == MLD_NATIVE_FUNC_SUCCESS) { - /* TODO: proof */ - int ret; - ret = mld_polyvecl_pointwise_acc_montgomery_l5_native( - w->coeffs, (const int32_t(*)[MLDSA_N])u->vec, - (const int32_t(*)[MLDSA_N])v->vec); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q); - return; - } + mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q); + return; } #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); + ret = mld_polyvecl_pointwise_acc_montgomery_l7_native( + w->coeffs, (const int32_t(*)[MLDSA_N])u->vec, + (const int32_t(*)[MLDSA_N])v->vec); + if (ret == MLD_NATIVE_FUNC_SUCCESS) { - /* TODO: proof */ - int ret; - ret = mld_polyvecl_pointwise_acc_montgomery_l7_native( - w->coeffs, (const int32_t(*)[MLDSA_N])u->vec, - (const int32_t(*)[MLDSA_N])v->vec); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q); - return; - } + mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q); + return; } #endif /* !(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 && \ MLD_CONFIG_PARAMETER_SET == 44) && \ @@ -386,32 +429,7 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, * The worst case is ML-DSA-87: 7 * (9Q-1) * (Q-1) < 2**52 * (and likewise for negative values) */ - - for (i = 0; i < MLDSA_N; i++) - __loop__( - assigns(i, j, memory_slice(w, sizeof(mld_poly))) - invariant(i <= MLDSA_N) - invariant(array_abs_bound(w->coeffs, 0, i, MLDSA_Q)) - ) - { - int64_t t = 0; - int32_t r; - for (j = 0; j < MLDSA_L; j++) - __loop__( - assigns(j, t) - invariant(j <= MLDSA_L) - invariant(t >= -(int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1)) - invariant(t <= (int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1)) - ) - { - t += (int64_t)u->vec[j].coeffs[i] * v->vec[j].coeffs[i]; - } - - r = mld_montgomery_reduce(t); - w->coeffs[i] = r; - } - - mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q); + mld_polyvecl_pointwise_acc_montgomery_c(w, u, v); } MLD_INTERNAL_API @@ -864,3 +882,4 @@ void mld_polyveck_unpack_t0(mld_polyveck *p, /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. * Don't modify by hand -- this is auto-generated by scripts/autogen. */ #undef mld_polymat_permute_bitrev_to_custom +#undef mld_polyvecl_pointwise_acc_montgomery_c diff --git a/mldsa/src/sys.h b/mldsa/src/sys.h index f5f3cc4ac..815ccfaf4 100644 --- a/mldsa/src/sys.h +++ b/mldsa/src/sys.h @@ -135,6 +135,10 @@ #endif /* inline */ #endif /* !MLD_INLINE */ +#ifndef MLD_STATIC_TESTABLE +#define MLD_STATIC_TESTABLE static +#endif + /* * C90 does not have the restrict compiler directive yet. * We don't use it in C90 builds. diff --git a/proofs/cbmc/poly_caddq/Makefile b/proofs/cbmc/poly_caddq/Makefile index 5b60156dc..4639df941 100644 --- a/proofs/cbmc/poly_caddq/Makefile +++ b/proofs/cbmc/poly_caddq/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_caddq -USE_FUNCTION_CONTRACTS=mld_caddq +USE_FUNCTION_CONTRACTS=mld_poly_caddq_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_caddq_c/Makefile b/proofs/cbmc/poly_caddq_c/Makefile new file mode 100644 index 000000000..04868ff84 --- /dev/null +++ b/proofs/cbmc/poly_caddq_c/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_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_poly_caddq_c +USE_FUNCTION_CONTRACTS=mld_caddq +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_poly_caddq_c + +# 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_c/poly_caddq_c_harness.c b/proofs/cbmc/poly_caddq_c/poly_caddq_c_harness.c new file mode 100644 index 000000000..be1fa8fab --- /dev/null +++ b/proofs/cbmc/poly_caddq_c/poly_caddq_c_harness.c @@ -0,0 +1,14 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + + +// Prototype for the function under test +void mld_poly_caddq_c(mld_poly *p); + +void harness(void) +{ + mld_poly *a; + mld_poly_caddq_c(a); +} diff --git a/proofs/cbmc/poly_chknorm/Makefile b/proofs/cbmc/poly_chknorm/Makefile index a18e30904..e83362cd3 100644 --- a/proofs/cbmc/poly_chknorm/Makefile +++ b/proofs/cbmc/poly_chknorm/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_chknorm -USE_FUNCTION_CONTRACTS=mld_ct_abs_i32 mld_ct_cmask_neg_i32 +USE_FUNCTION_CONTRACTS=mld_poly_chknorm_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_chknorm_c/Makefile b/proofs/cbmc/poly_chknorm_c/Makefile new file mode 100644 index 000000000..cd9ded7d8 --- /dev/null +++ b/proofs/cbmc/poly_chknorm_c/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_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_poly_chknorm_c +USE_FUNCTION_CONTRACTS=mld_ct_abs_i32 mld_ct_cmask_neg_i32 +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_poly_chknorm_c + +# 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_c/poly_chknorm_c_harness.c b/proofs/cbmc/poly_chknorm_c/poly_chknorm_c_harness.c new file mode 100644 index 000000000..65d6e48d8 --- /dev/null +++ b/proofs/cbmc/poly_chknorm_c/poly_chknorm_c_harness.c @@ -0,0 +1,15 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + +// Prototype for the function under test +uint32_t mld_poly_chknorm_c(mld_poly *a, int32_t B); + +void harness(void) +{ + mld_poly *a; + uint32_t r; + int32_t B; + r = mld_poly_chknorm_c(a, B); +} diff --git a/proofs/cbmc/poly_decompose/Makefile b/proofs/cbmc/poly_decompose/Makefile index faf755265..ce20f3b4b 100644 --- a/proofs/cbmc/poly_decompose/Makefile +++ b/proofs/cbmc/poly_decompose/Makefile @@ -20,7 +20,7 @@ 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_decompose +USE_FUNCTION_CONTRACTS= mld_poly_decompose_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_decompose_c/Makefile b/proofs/cbmc/poly_decompose_c/Makefile new file mode 100644 index 000000000..1c4a3c31e --- /dev/null +++ b/proofs/cbmc/poly_decompose_c/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_decompose_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_c +USE_FUNCTION_CONTRACTS=mld_decompose +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_poly_decompose_c + +# 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_c/poly_decompose_c_harness.c b/proofs/cbmc/poly_decompose_c/poly_decompose_c_harness.c new file mode 100644 index 000000000..67e87f110 --- /dev/null +++ b/proofs/cbmc/poly_decompose_c/poly_decompose_c_harness.c @@ -0,0 +1,14 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + +// Prototype for the function under test +#define mld_poly_decompose_c MLD_ADD_PARAM_SET(mld_poly_decompose_c) +void mld_poly_decompose_c(mld_poly *a1, mld_poly *a0, mld_poly *a); + +void harness(void) +{ + mld_poly *a0, *a1, *a; + mld_poly_decompose_c(a1, a0, a); +} diff --git a/proofs/cbmc/poly_invntt_tomont/Makefile b/proofs/cbmc/poly_invntt_tomont/Makefile index 9b4553731..6b1f356fc 100644 --- a/proofs/cbmc/poly_invntt_tomont/Makefile +++ b/proofs/cbmc/poly_invntt_tomont/Makefile @@ -20,7 +20,7 @@ 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_NAMESPACE)invntt_tomont +USE_FUNCTION_CONTRACTS=mld_poly_invntt_tomont_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_invntt_tomont_c/Makefile b/proofs/cbmc/poly_invntt_tomont_c/Makefile new file mode 100644 index 000000000..b367b2e38 --- /dev/null +++ b/proofs/cbmc/poly_invntt_tomont_c/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_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_poly_invntt_tomont_c +USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)invntt_tomont +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_poly_invntt_tomont_c + +# 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_c/poly_invntt_tomont_c_harness.c b/proofs/cbmc/poly_invntt_tomont_c/poly_invntt_tomont_c_harness.c new file mode 100644 index 000000000..5c723c514 --- /dev/null +++ b/proofs/cbmc/poly_invntt_tomont_c/poly_invntt_tomont_c_harness.c @@ -0,0 +1,16 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include +#include "params.h" +#include "poly.h" + +// Prototype for the function under test +void mld_poly_invntt_tomont_c(mld_poly *p); + + +void harness(void) +{ + mld_poly *a; + mld_poly_invntt_tomont_c(a); +} diff --git a/proofs/cbmc/poly_ntt/Makefile b/proofs/cbmc/poly_ntt/Makefile index 751e8c5b3..d64857657 100644 --- a/proofs/cbmc/poly_ntt/Makefile +++ b/proofs/cbmc/poly_ntt/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_ntt -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)ntt +USE_FUNCTION_CONTRACTS=mld_poly_ntt_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_ntt_c/Makefile b/proofs/cbmc/poly_ntt_c/Makefile new file mode 100644 index 000000000..4b29506c1 --- /dev/null +++ b/proofs/cbmc/poly_ntt_c/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_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_poly_ntt_c +USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)ntt +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_poly_ntt_c + +# 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_c/poly_ntt_c_harness.c b/proofs/cbmc/poly_ntt_c/poly_ntt_c_harness.c new file mode 100644 index 000000000..e5e1a3c23 --- /dev/null +++ b/proofs/cbmc/poly_ntt_c/poly_ntt_c_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.h" + +// Prototype for the function under test +void mld_poly_ntt_c(mld_poly *p); + +void harness(void) +{ + mld_poly *a; + mld_poly_ntt_c(a); +} diff --git a/proofs/cbmc/poly_pointwise_montgomery/Makefile b/proofs/cbmc/poly_pointwise_montgomery/Makefile index 966afd7d4..260e07bd4 100644 --- a/proofs/cbmc/poly_pointwise_montgomery/Makefile +++ b/proofs/cbmc/poly_pointwise_montgomery/Makefile @@ -20,7 +20,7 @@ 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_montgomery_reduce +USE_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_pointwise_montgomery_c/Makefile b/proofs/cbmc/poly_pointwise_montgomery_c/Makefile new file mode 100644 index 000000000..587b45915 --- /dev/null +++ b/proofs/cbmc/poly_pointwise_montgomery_c/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_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery_c +USE_FUNCTION_CONTRACTS=mld_montgomery_reduce +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_poly_pointwise_montgomery_c + +# 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_c/poly_pointwise_montgomery_c_harness.c b/proofs/cbmc/poly_pointwise_montgomery_c/poly_pointwise_montgomery_c_harness.c new file mode 100644 index 000000000..4ff441fb6 --- /dev/null +++ b/proofs/cbmc/poly_pointwise_montgomery_c/poly_pointwise_montgomery_c_harness.c @@ -0,0 +1,14 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +// Prototype for the function under test +void mld_poly_pointwise_montgomery_c(mld_poly *c, mld_poly *a, mld_poly *b); + + +void harness(void) +{ + mld_poly *a, *b, *c; + mld_poly_pointwise_montgomery_c(c, a, b); +} diff --git a/proofs/cbmc/poly_use_hint/Makefile b/proofs/cbmc/poly_use_hint/Makefile index 9705c8ce8..d15774086 100644 --- a/proofs/cbmc/poly_use_hint/Makefile +++ b/proofs/cbmc/poly_use_hint/Makefile @@ -20,7 +20,7 @@ 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_use_hint +USE_FUNCTION_CONTRACTS=mld_poly_use_hint_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_use_hint_c/Makefile b/proofs/cbmc/poly_use_hint_c/Makefile new file mode 100644 index 000000000..188b8e705 --- /dev/null +++ b/proofs/cbmc/poly_use_hint_c/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_use_hint_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_c +USE_FUNCTION_CONTRACTS=mld_use_hint +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_poly_use_hint_c + +# 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_c/poly_use_hint_c_harness.c b/proofs/cbmc/poly_use_hint_c/poly_use_hint_c_harness.c new file mode 100644 index 000000000..0b17ee2be --- /dev/null +++ b/proofs/cbmc/poly_use_hint_c/poly_use_hint_c_harness.c @@ -0,0 +1,15 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + +// Prototype for the function under test +#define mld_poly_use_hint_c MLD_ADD_PARAM_SET(mld_poly_use_hint_c) +void mld_poly_use_hint_c(mld_poly *b, mld_poly *a, mld_poly *h); + + +void harness(void) +{ + mld_poly *a, *b, *h; + mld_poly_use_hint_c(b, a, h); +} diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile b/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile index bfef14c29..c5b81567b 100644 --- a/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile +++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile @@ -20,7 +20,7 @@ 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_montgomery_reduce +USE_FUNCTION_CONTRACTS= mld_polyvecl_pointwise_acc_montgomery_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile new file mode 100644 index 000000000..dd6ca86ce --- /dev/null +++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile @@ -0,0 +1,57 @@ +# 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_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c + +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery_c +USE_FUNCTION_CONTRACTS=mld_montgomery_reduce +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_no_bv_extract --z3 +CBMCFLAGS += --slice-formula +CBMCFLAGS += --no-array-field-sensitivity + +FUNCTION_NAME = mld_polyvecl_pointwise_acc_montgomery_c + +# 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_c/polyvecl_pointwise_acc_montgomery_c_harness.c b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/polyvecl_pointwise_acc_montgomery_c_harness.c new file mode 100644 index 000000000..7ff7073aa --- /dev/null +++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/polyvecl_pointwise_acc_montgomery_c_harness.c @@ -0,0 +1,18 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "polyvec.h" + + +// Prototype for the function under test +#define mld_polyvecl_pointwise_acc_montgomery_c \ + MLD_ADD_PARAM_SET(mld_polyvecl_pointwise_acc_montgomery_c) +void mld_polyvecl_pointwise_acc_montgomery_c(mld_poly *a, mld_polyvecl *b, + mld_polyvecl *c); + +void harness(void) +{ + mld_poly *a; + mld_polyvecl *b, *c; + mld_polyvecl_pointwise_acc_montgomery_c(a, b, c); +} diff --git a/proofs/cbmc/polyz_unpack/Makefile b/proofs/cbmc/polyz_unpack/Makefile index 4d0075518..dfe0ecff7 100644 --- a/proofs/cbmc/polyz_unpack/Makefile +++ b/proofs/cbmc/polyz_unpack/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_unpack -USE_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS=mld_polyz_unpack_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/polyz_unpack_c/Makefile b/proofs/cbmc/polyz_unpack_c/Makefile new file mode 100644 index 000000000..0a3112c17 --- /dev/null +++ b/proofs/cbmc/polyz_unpack_c/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 = polyz_unpack_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS= mld_polyz_unpack_c +USE_FUNCTION_CONTRACTS= +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_polyz_unpack_c + +# 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_c/polyz_unpack_c_harness.c b/proofs/cbmc/polyz_unpack_c/polyz_unpack_c_harness.c new file mode 100644 index 000000000..ce68d6147 --- /dev/null +++ b/proofs/cbmc/polyz_unpack_c/polyz_unpack_c_harness.c @@ -0,0 +1,17 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + + +// Prototype for the function under test +#define mld_polyz_unpack_c MLD_ADD_PARAM_SET(mld_polyz_unpack_c) +void mld_polyz_unpack_c(mld_poly *a, uint8_t *b); + + +void harness(void) +{ + mld_poly *a; + uint8_t *b; + mld_polyz_unpack_c(a, b); +} diff --git a/proofs/cbmc/rej_eta/Makefile b/proofs/cbmc/rej_eta/Makefile index 77a74ccdc..350b80ca3 100644 --- a/proofs/cbmc/rej_eta/Makefile +++ b/proofs/cbmc/rej_eta/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c CHECK_FUNCTION_CONTRACTS=mld_rej_eta -USE_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= mld_rej_eta_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/rej_eta_c/Makefile b/proofs/cbmc/rej_eta_c/Makefile new file mode 100644 index 000000000..ba0294c64 --- /dev/null +++ b/proofs/cbmc/rej_eta_c/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_eta_c_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_c + +DEFINES += +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_c +USE_FUNCTION_CONTRACTS= +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_c + +# 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_c/rej_eta_c_harness.c b/proofs/cbmc/rej_eta_c/rej_eta_c_harness.c new file mode 100644 index 000000000..7355bc6c2 --- /dev/null +++ b/proofs/cbmc/rej_eta_c/rej_eta_c_harness.c @@ -0,0 +1,20 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +#define mld_rej_eta_c MLD_ADD_PARAM_SET(mld_rej_eta_c) +static unsigned int mld_rej_eta_c(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_c(a, target, offset, buf, buflen); +} diff --git a/proofs/cbmc/rej_uniform/Makefile b/proofs/cbmc/rej_uniform/Makefile index bec260ead..12633d07d 100644 --- a/proofs/cbmc/rej_uniform/Makefile +++ b/proofs/cbmc/rej_uniform/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=mld_rej_uniform -USE_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS=mld_rej_uniform_c APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/rej_uniform_c/Makefile b/proofs/cbmc/rej_uniform_c/Makefile new file mode 100644 index 000000000..6acca2b4d --- /dev/null +++ b/proofs/cbmc/rej_uniform_c/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_c_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_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_rej_uniform_c +USE_FUNCTION_CONTRACTS= +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_c + +# 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_c/rej_uniform_c_harness.c b/proofs/cbmc/rej_uniform_c/rej_uniform_c_harness.c new file mode 100644 index 000000000..c366b8e48 --- /dev/null +++ b/proofs/cbmc/rej_uniform_c/rej_uniform_c_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_c(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_c(a, target, offset, buf, buflen); +}