From 2bbe1f0c46fee47e8864384e375fd327d652ab67 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Tue, 12 May 2026 04:44:43 +0100 Subject: [PATCH] CBMC: Add disjoint() and slices() to compact memory annotations CBMC contracts in this repo currently require one instance of requires(memory_no_alias(...)) per pointer argument and a parallel set of memory_slice(...) targets in assigns(...). For functions dealing with multiple pointers, this quickly bloats and thereby impedes the readability of the CBMC specs. Introduce two variadic preprocessor macros in mldsa/src/cbmc.h that unfold a list of regions into the corresponding memory_no_alias / memory_slice calls, joined as required by their containing clause: ``` requires(disjoint(arg, ...)) -- AND-joined memory_no_alias checks assigns(..., slices(arg, ...)) -- comma-joined memory_slice targets ``` Each arg is either a bare object x (size sizeof(*x)) or a pair (x, N) where N is an element count (size sizeof(*x) * N). The pair form covers byte buffers like uint8_t seed[CRHBYTES] and typed arrays where the count comes from a parameter rather than the type. Implementation uses the standard C99 variadic-preprocessor toolkit (arg counting, IS_PAIR probe via parenthesis detection, per-arity map/join dispatch) capped at 16 arguments. The macros are defined only inside the existing #ifdef CBMC block, so the C90 build path is unaffected. Signed-off-by: Hanno Becker --- dev/aarch64_clean/src/arith_native_aarch64.h | 69 ++++----- dev/aarch64_opt/src/arith_native_aarch64.h | 69 ++++----- .../aarch64/src/fips202_native_aarch64.h | 20 +-- .../x86_64/src/fips202_native_x86_64.h | 4 +- dev/x86_64/src/arith_native_x86_64.h | 35 ++--- mldsa/src/cbmc.h | 88 ++++++++++++ mldsa/src/ct.h | 3 +- mldsa/src/fips202/fips202.c | 24 ++-- mldsa/src/fips202/fips202.h | 51 +++---- mldsa/src/fips202/fips202x4.c | 35 ++--- mldsa/src/fips202/fips202x4.h | 56 ++++---- mldsa/src/fips202/keccakf1600.h | 38 +++-- .../aarch64/src/fips202_native_aarch64.h | 20 +-- mldsa/src/fips202/native/api.h | 27 ++-- .../native/x86_64/src/fips202_native_x86_64.h | 4 +- .../native/aarch64/src/arith_native_aarch64.h | 69 ++++----- mldsa/src/native/api.h | 88 +++++------- .../native/x86_64/src/arith_native_x86_64.h | 35 ++--- mldsa/src/packing.c | 4 +- mldsa/src/packing.h | 62 +++----- mldsa/src/poly.c | 51 +++---- mldsa/src/poly.h | 79 ++++------- mldsa/src/poly_kl.c | 38 ++--- mldsa/src/poly_kl.h | 73 ++++------ mldsa/src/polyvec.c | 26 ++-- mldsa/src/polyvec.h | 71 ++++------ mldsa/src/polyvec_lazy.c | 25 ++-- mldsa/src/polyvec_lazy.h | 132 +++++++----------- mldsa/src/randombytes.h | 4 +- mldsa/src/rounding.h | 12 +- mldsa/src/sign.c | 87 +++++------- mldsa/src/sign.h | 109 ++++++--------- 32 files changed, 656 insertions(+), 852 deletions(-) diff --git a/dev/aarch64_clean/src/arith_native_aarch64.h b/dev/aarch64_clean/src/arith_native_aarch64.h index 2d5910601..1b75cf305 100644 --- a/dev/aarch64_clean/src/arith_native_aarch64.h +++ b/dev/aarch64_clean/src/arith_native_aarch64.h @@ -66,11 +66,11 @@ void mld_ntt_aarch64_asm(int32_t *r, const int32_t *zetas_l123456, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(zetas_l123456 == mld_aarch64_ntt_zetas_layer123456) requires(zetas_l78 == mld_aarch64_ntt_zetas_layer78) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 75423753)) /* check-magic: on */ @@ -82,11 +82,11 @@ void mld_intt_aarch64_asm(int32_t *r, const int32_t *zetas_l78, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/intt_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(zetas_l78 == mld_aarch64_intt_zetas_layer78) requires(zetas_l123456 == mld_aarch64_intt_zetas_layer123456) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ @@ -120,11 +120,9 @@ void mld_poly_decompose_32_aarch64_asm(int32_t *a1, int32_t *a0) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_decompose_32_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) /* check-magic: 16 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 32)) */ ensures(array_bound(a1, 0, MLDSA_N, 0, 16)) /* check-magic: 261889 == (MLDSA_Q - 1) / 32 + 1 */ @@ -137,11 +135,9 @@ void mld_poly_decompose_88_aarch64_asm(int32_t *a1, int32_t *a0) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_decompose_88_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) /* check-magic: 44 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 88)) */ ensures(array_bound(a1, 0, MLDSA_N, 0, 44)) /* check-magic: 95233 == (MLDSA_Q - 1) / 88 + 1 */ @@ -154,9 +150,9 @@ void mld_poly_caddq_aarch64_asm(int32_t *a) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_caddq_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((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)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) ); @@ -167,11 +163,10 @@ void mld_poly_use_hint_32_aarch64_asm(int32_t *a, const int32_t *h) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (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(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(a, 0, MLDSA_N, 0, 16)) ); @@ -181,11 +176,10 @@ void mld_poly_use_hint_88_aarch64_asm(int32_t *a, const int32_t *h) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (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(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(a, 0, MLDSA_N, 0, 44)) ); #endif /* !MLD_CONFIG_NO_VERIFY_API */ @@ -196,7 +190,7 @@ int mld_poly_chknorm_aarch64_asm(const int32_t *a, int32_t B) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_chknorm_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N))) /* HOL Light precondition: abs(ival(x i)) < 2^31, i.e., a[i] != INT32_MIN */ requires(forall(k0, 0, MLDSA_N, a[k0] > INT32_MIN)) ensures(return_value == 0 || return_value == 1) @@ -212,10 +206,9 @@ void mld_polyz_unpack_17_aarch64_asm(int32_t *r, const uint8_t *buf, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/polyz_unpack_17_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(buf, 576)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (buf, 576))) requires(indices == mld_polyz_unpack_17_indices) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(r, 0, MLDSA_N, -((1 << 17) - 1), (1 << 17) + 1)) ); #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \ @@ -230,10 +223,9 @@ void mld_polyz_unpack_19_aarch64_asm(int32_t *r, const uint8_t *buf, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/polyz_unpack_19_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(buf, 640)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (buf, 640))) requires(indices == mld_polyz_unpack_19_indices) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(r, 0, MLDSA_N, -((1 << 19) - 1), (1 << 19) + 1)) ); #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \ @@ -248,12 +240,11 @@ void mld_poly_pointwise_montgomery_aarch64_asm(int32_t *a, const int32_t *b) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/pointwise_montgomery_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (b, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ requires(array_abs_bound(a, 0, MLDSA_N, 75423753)) requires(array_abs_bound(b, 0, MLDSA_N, 75423753)) - assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(a, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -269,13 +260,11 @@ void mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm( * proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 4), (b, sizeof(*b) * 4))) /* check-magic: off */ requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -289,13 +278,11 @@ void mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm( * proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 5), (b, sizeof(*b) * 5))) /* check-magic: off */ requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -309,13 +296,11 @@ void mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm( * proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 7), (b, sizeof(*b) * 7))) /* check-magic: off */ requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); diff --git a/dev/aarch64_opt/src/arith_native_aarch64.h b/dev/aarch64_opt/src/arith_native_aarch64.h index 2d5910601..1b75cf305 100644 --- a/dev/aarch64_opt/src/arith_native_aarch64.h +++ b/dev/aarch64_opt/src/arith_native_aarch64.h @@ -66,11 +66,11 @@ void mld_ntt_aarch64_asm(int32_t *r, const int32_t *zetas_l123456, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(zetas_l123456 == mld_aarch64_ntt_zetas_layer123456) requires(zetas_l78 == mld_aarch64_ntt_zetas_layer78) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 75423753)) /* check-magic: on */ @@ -82,11 +82,11 @@ void mld_intt_aarch64_asm(int32_t *r, const int32_t *zetas_l78, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/intt_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(zetas_l78 == mld_aarch64_intt_zetas_layer78) requires(zetas_l123456 == mld_aarch64_intt_zetas_layer123456) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ @@ -120,11 +120,9 @@ void mld_poly_decompose_32_aarch64_asm(int32_t *a1, int32_t *a0) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_decompose_32_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) /* check-magic: 16 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 32)) */ ensures(array_bound(a1, 0, MLDSA_N, 0, 16)) /* check-magic: 261889 == (MLDSA_Q - 1) / 32 + 1 */ @@ -137,11 +135,9 @@ void mld_poly_decompose_88_aarch64_asm(int32_t *a1, int32_t *a0) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_decompose_88_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) /* check-magic: 44 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 88)) */ ensures(array_bound(a1, 0, MLDSA_N, 0, 44)) /* check-magic: 95233 == (MLDSA_Q - 1) / 88 + 1 */ @@ -154,9 +150,9 @@ void mld_poly_caddq_aarch64_asm(int32_t *a) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_caddq_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((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)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) ); @@ -167,11 +163,10 @@ void mld_poly_use_hint_32_aarch64_asm(int32_t *a, const int32_t *h) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (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(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(a, 0, MLDSA_N, 0, 16)) ); @@ -181,11 +176,10 @@ void mld_poly_use_hint_88_aarch64_asm(int32_t *a, const int32_t *h) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (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(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(a, 0, MLDSA_N, 0, 44)) ); #endif /* !MLD_CONFIG_NO_VERIFY_API */ @@ -196,7 +190,7 @@ int mld_poly_chknorm_aarch64_asm(const int32_t *a, int32_t B) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_chknorm_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N))) /* HOL Light precondition: abs(ival(x i)) < 2^31, i.e., a[i] != INT32_MIN */ requires(forall(k0, 0, MLDSA_N, a[k0] > INT32_MIN)) ensures(return_value == 0 || return_value == 1) @@ -212,10 +206,9 @@ void mld_polyz_unpack_17_aarch64_asm(int32_t *r, const uint8_t *buf, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/polyz_unpack_17_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(buf, 576)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (buf, 576))) requires(indices == mld_polyz_unpack_17_indices) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(r, 0, MLDSA_N, -((1 << 17) - 1), (1 << 17) + 1)) ); #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \ @@ -230,10 +223,9 @@ void mld_polyz_unpack_19_aarch64_asm(int32_t *r, const uint8_t *buf, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/polyz_unpack_19_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(buf, 640)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (buf, 640))) requires(indices == mld_polyz_unpack_19_indices) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(r, 0, MLDSA_N, -((1 << 19) - 1), (1 << 19) + 1)) ); #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \ @@ -248,12 +240,11 @@ void mld_poly_pointwise_montgomery_aarch64_asm(int32_t *a, const int32_t *b) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/pointwise_montgomery_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (b, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ requires(array_abs_bound(a, 0, MLDSA_N, 75423753)) requires(array_abs_bound(b, 0, MLDSA_N, 75423753)) - assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(a, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -269,13 +260,11 @@ void mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm( * proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 4), (b, sizeof(*b) * 4))) /* check-magic: off */ requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -289,13 +278,11 @@ void mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm( * proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 5), (b, sizeof(*b) * 5))) /* check-magic: off */ requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -309,13 +296,11 @@ void mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm( * proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 7), (b, sizeof(*b) * 7))) /* check-magic: off */ requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); diff --git a/dev/fips202/aarch64/src/fips202_native_aarch64.h b/dev/fips202/aarch64/src/fips202_native_aarch64.h index 3939c2359..00c066d24 100644 --- a/dev/fips202/aarch64/src/fips202_native_aarch64.h +++ b/dev/fips202/aarch64/src/fips202_native_aarch64.h @@ -21,9 +21,9 @@ MLD_INTERNAL_DATA_DECLARATION const uint64_t void mld_keccak_f1600_x1_scalar_aarch64_asm(uint64_t state[25], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 1))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + assigns(slices((state, sizeof(uint64_t) * 25 * 1))) ); #define mld_keccak_f1600_x1_v84a_aarch64_asm \ @@ -31,9 +31,9 @@ __contract__( void mld_keccak_f1600_x1_v84a_aarch64_asm(uint64_t state[25], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 1))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + assigns(slices((state, sizeof(uint64_t) * 25 * 1))) ); #define mld_keccak_f1600_x2_v84a_aarch64_asm \ @@ -41,9 +41,9 @@ __contract__( void mld_keccak_f1600_x2_v84a_aarch64_asm(uint64_t state[50], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 2))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2)) + assigns(slices((state, sizeof(uint64_t) * 25 * 2))) ); #define mld_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm \ @@ -51,9 +51,9 @@ __contract__( void mld_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm(uint64_t state[100], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 4))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + assigns(slices((state, sizeof(uint64_t) * 25 * 4))) ); #define mld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm \ @@ -61,9 +61,9 @@ __contract__( void mld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm( uint64_t state[100], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 4))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + assigns(slices((state, sizeof(uint64_t) * 25 * 4))) ); #endif /* !MLD_DEV_FIPS202_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H */ diff --git a/dev/fips202/x86_64/src/fips202_native_x86_64.h b/dev/fips202/x86_64/src/fips202_native_x86_64.h index 7eb83d035..844f9c775 100644 --- a/dev/fips202/x86_64/src/fips202_native_x86_64.h +++ b/dev/fips202/x86_64/src/fips202_native_x86_64.h @@ -34,11 +34,11 @@ void mld_keccak_f1600_x4_avx2_asm(uint64_t states[100], const uint64_t rc[24], /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml */ __contract__( - requires(memory_no_alias(states, sizeof(uint64_t) * 25 * 4)) + requires(disjoint((states, sizeof(uint64_t) * 25 * 4))) requires(rc == mld_keccakf1600_round_constants) requires(rho8 == mld_keccak_rho8) requires(rho56 == mld_keccak_rho56) - assigns(memory_slice(states, sizeof(uint64_t) * 25 * 4)) + assigns(slices((states, sizeof(uint64_t) * 25 * 4))) ); #endif /* !MLD_DEV_FIPS202_X86_64_SRC_FIPS202_NATIVE_X86_64_H */ diff --git a/dev/x86_64/src/arith_native_x86_64.h b/dev/x86_64/src/arith_native_x86_64.h index 7c2975e5e..751a78fcc 100644 --- a/dev/x86_64/src/arith_native_x86_64.h +++ b/dev/x86_64/src/arith_native_x86_64.h @@ -36,10 +36,10 @@ void mld_ntt_avx2_asm(int32_t *r, const int32_t *qdata) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/ntt_avx2_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(qdata == mld_qdata) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 42035262)) /* check-magic: on */ @@ -50,10 +50,10 @@ void mld_invntt_avx2_asm(int32_t *r, const int32_t *qdata) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/intt_avx2_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(qdata == mld_qdata) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 6285313)) /* check-magic: on */ @@ -64,9 +64,9 @@ void mld_nttunpack_avx2_asm(int32_t *r) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/nttunpack_avx2_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* Output is a permutation of input: every output coefficient * is some input coefficient */ ensures(forall(i, 0, MLDSA_N, exists(j, 0, MLDSA_N, @@ -126,13 +126,12 @@ void mld_pointwise_avx2_asm(int32_t *a, const int32_t *b, const int32_t *qdata) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/pointwise_avx2_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (b, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ requires(array_abs_bound(a, 0, MLDSA_N, 75423753)) requires(array_abs_bound(b, 0, MLDSA_N, 75423753)) requires(qdata == mld_qdata) - assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(a, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -145,14 +144,12 @@ void mld_pointwise_acc_l4_avx2_asm(int32_t c[MLDSA_N], /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/pointwise_acc_l4_avx2_asm.ml */ __contract__( - requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N)) + requires(disjoint((c, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 4), (b, sizeof(*b) * 4))) /* check-magic: off */ requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) requires(qdata == mld_qdata) - assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N)) + assigns(slices((c, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(c, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -165,14 +162,12 @@ void mld_pointwise_acc_l5_avx2_asm(int32_t c[MLDSA_N], /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/pointwise_acc_l5_avx2_asm.ml */ __contract__( - requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N)) + requires(disjoint((c, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 5), (b, sizeof(*b) * 5))) /* check-magic: off */ requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) requires(qdata == mld_qdata) - assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N)) + assigns(slices((c, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(c, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -185,14 +180,12 @@ void mld_pointwise_acc_l7_avx2_asm(int32_t c[MLDSA_N], /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/pointwise_acc_l7_avx2_asm.ml */ __contract__( - requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N)) + requires(disjoint((c, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 7), (b, sizeof(*b) * 7))) /* check-magic: off */ requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) requires(qdata == mld_qdata) - assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N)) + assigns(slices((c, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(c, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); diff --git a/mldsa/src/cbmc.h b/mldsa/src/cbmc.h index d1be71971..c08b444e6 100644 --- a/mldsa/src/cbmc.h +++ b/mldsa/src/cbmc.h @@ -161,6 +161,94 @@ array_unchanged_u64_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), 0, (N), (array_var)) /* clang-format on */ +/*************************************************** + * Variadic compaction of memory annotations + * + * disjoint(arg, ...) -- inside requires(...): expands each arg to a + * memory_no_alias(...) check and AND-joins them. + * slices(arg, ...) -- inside assigns(...): expands each arg to a + * memory_slice(...) target, comma-joined. + * + * Each arg is either: + * - a bare object x -> size is sizeof(*(x)) + * - a pair (x, N) -> size is N (interpreted as a byte count) + * + * Requires a C99 preprocessor; only seen by the compiler in CBMC + * builds. Capped at 16 args per call. + ***************************************************/ + +#define MLD_CBMC_NARGS(...) \ + MLD_CBMC_NARGS_(__VA_ARGS__, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, \ + 3, 2, 1) +#define MLD_CBMC_NARGS_(_1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, \ + _13, _14, _15, _16, N, ...) \ + N + +#define MLD_CBMC_PROBE_(...) ~, 1 +#define MLD_CBMC_CHECK_(...) MLD_CBMC_CHECK_N_(__VA_ARGS__, 0) +#define MLD_CBMC_CHECK_N_(_a, _b, ...) _b +#define MLD_CBMC_IS_PAIR(x) MLD_CBMC_CHECK_(MLD_CBMC_PROBE_ x) + +#define MLD_CBMC_NA(x) MLD_CBMC_NA_(MLD_CBMC_IS_PAIR(x), x) +#define MLD_CBMC_NA_(t, x) MLD_CBMC_NA__(t, x) +#define MLD_CBMC_NA__(t, x) MLD_CBMC_NA_##t(x) +#define MLD_CBMC_NA_0(x) memory_no_alias((x), sizeof(*(x))) +#define MLD_CBMC_NA_1(x) MLD_CBMC_NA_PAIR_ x +#define MLD_CBMC_NA_PAIR_(p, n) memory_no_alias((p), (n)) + +#define MLD_CBMC_SL(x) MLD_CBMC_SL_(MLD_CBMC_IS_PAIR(x), x) +#define MLD_CBMC_SL_(t, x) MLD_CBMC_SL__(t, x) +#define MLD_CBMC_SL__(t, x) MLD_CBMC_SL_##t(x) +#define MLD_CBMC_SL_0(x) memory_slice((x), sizeof(*(x))) +#define MLD_CBMC_SL_1(x) MLD_CBMC_SL_PAIR_ x +#define MLD_CBMC_SL_PAIR_(p, n) memory_slice((p), (n)) + +#define MLD_CBMC_AND_1(M, a) M(a) +#define MLD_CBMC_AND_2(M, a, ...) M(a) && MLD_CBMC_AND_1(M, __VA_ARGS__) +#define MLD_CBMC_AND_3(M, a, ...) M(a) && MLD_CBMC_AND_2(M, __VA_ARGS__) +#define MLD_CBMC_AND_4(M, a, ...) M(a) && MLD_CBMC_AND_3(M, __VA_ARGS__) +#define MLD_CBMC_AND_5(M, a, ...) M(a) && MLD_CBMC_AND_4(M, __VA_ARGS__) +#define MLD_CBMC_AND_6(M, a, ...) M(a) && MLD_CBMC_AND_5(M, __VA_ARGS__) +#define MLD_CBMC_AND_7(M, a, ...) M(a) && MLD_CBMC_AND_6(M, __VA_ARGS__) +#define MLD_CBMC_AND_8(M, a, ...) M(a) && MLD_CBMC_AND_7(M, __VA_ARGS__) +#define MLD_CBMC_AND_9(M, a, ...) M(a) && MLD_CBMC_AND_8(M, __VA_ARGS__) +#define MLD_CBMC_AND_10(M, a, ...) M(a) && MLD_CBMC_AND_9(M, __VA_ARGS__) +#define MLD_CBMC_AND_11(M, a, ...) M(a) && MLD_CBMC_AND_10(M, __VA_ARGS__) +#define MLD_CBMC_AND_12(M, a, ...) M(a) && MLD_CBMC_AND_11(M, __VA_ARGS__) +#define MLD_CBMC_AND_13(M, a, ...) M(a) && MLD_CBMC_AND_12(M, __VA_ARGS__) +#define MLD_CBMC_AND_14(M, a, ...) M(a) && MLD_CBMC_AND_13(M, __VA_ARGS__) +#define MLD_CBMC_AND_15(M, a, ...) M(a) && MLD_CBMC_AND_14(M, __VA_ARGS__) +#define MLD_CBMC_AND_16(M, a, ...) M(a) && MLD_CBMC_AND_15(M, __VA_ARGS__) + +#define MLD_CBMC_COMMA_1(M, a) M(a) +#define MLD_CBMC_COMMA_2(M, a, ...) M(a), MLD_CBMC_COMMA_1(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_3(M, a, ...) M(a), MLD_CBMC_COMMA_2(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_4(M, a, ...) M(a), MLD_CBMC_COMMA_3(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_5(M, a, ...) M(a), MLD_CBMC_COMMA_4(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_6(M, a, ...) M(a), MLD_CBMC_COMMA_5(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_7(M, a, ...) M(a), MLD_CBMC_COMMA_6(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_8(M, a, ...) M(a), MLD_CBMC_COMMA_7(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_9(M, a, ...) M(a), MLD_CBMC_COMMA_8(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_10(M, a, ...) M(a), MLD_CBMC_COMMA_9(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_11(M, a, ...) M(a), MLD_CBMC_COMMA_10(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_12(M, a, ...) M(a), MLD_CBMC_COMMA_11(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_13(M, a, ...) M(a), MLD_CBMC_COMMA_12(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_14(M, a, ...) M(a), MLD_CBMC_COMMA_13(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_15(M, a, ...) M(a), MLD_CBMC_COMMA_14(M, __VA_ARGS__) +#define MLD_CBMC_COMMA_16(M, a, ...) M(a), MLD_CBMC_COMMA_15(M, __VA_ARGS__) + +#define MLD_CBMC_DISPATCH_(prefix, n, M, ...) prefix##n(M, __VA_ARGS__) +#define MLD_CBMC_DISPATCH(prefix, n, M, ...) \ + MLD_CBMC_DISPATCH_(prefix, n, M, __VA_ARGS__) + +#define disjoint(...) \ + (MLD_CBMC_DISPATCH(MLD_CBMC_AND_, MLD_CBMC_NARGS(__VA_ARGS__), MLD_CBMC_NA, \ + __VA_ARGS__)) + +#define slices(...) \ + MLD_CBMC_DISPATCH(MLD_CBMC_COMMA_, MLD_CBMC_NARGS(__VA_ARGS__), MLD_CBMC_SL, \ + __VA_ARGS__) + /* Wrapper around array_bound operating on absolute values. * * The absolute value bound `k` is exclusive. diff --git a/mldsa/src/ct.h b/mldsa/src/ct.h index f7953b3b0..e42574750 100644 --- a/mldsa/src/ct.h +++ b/mldsa/src/ct.h @@ -293,8 +293,7 @@ static MLD_INLINE uint8_t mld_ct_memcmp(const uint8_t *a, const uint8_t *b, const size_t len) __contract__( requires(len <= UINT16_MAX) - requires(memory_no_alias(a, len)) - requires(memory_no_alias(b, len)) + requires(disjoint((a, len), (b, len))) ensures((return_value == 0) || (return_value == 0xFF)) ensures((return_value == 0) == forall(i, 0, len, (a[i] == b[i])))) { diff --git a/mldsa/src/fips202/fips202.c b/mldsa/src/fips202/fips202.c index fa7f682b5..25d23d767 100644 --- a/mldsa/src/fips202/fips202.c +++ b/mldsa/src/fips202/fips202.c @@ -46,8 +46,8 @@ */ static void keccak_init(uint64_t s[MLD_KECCAK_LANES]) __contract__( - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(disjoint((s, sizeof(uint64_t) * MLD_KECCAK_LANES))) + assigns(slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES))) ) { mld_memset(s, 0, sizeof(uint64_t) * MLD_KECCAK_LANES); @@ -72,15 +72,13 @@ __contract__( requires(r > 0) requires(r < sizeof(uint64_t) * MLD_KECCAK_LANES) requires(pos <= r) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - requires(memory_no_alias(in, inlen)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(disjoint((s, sizeof(uint64_t) * MLD_KECCAK_LANES), (in, inlen))) + assigns(slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES))) ensures(return_value < r)) { while (inlen >= r - pos) __loop__( - assigns(pos, in, inlen, - memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) + assigns(pos, in, inlen, slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES))) invariant(inlen <= loop_entry(inlen)) invariant(pos <= r) invariant(in == loop_entry(in) + (loop_entry(inlen) - inlen)) @@ -113,8 +111,8 @@ static void keccak_finalize(uint64_t s[MLD_KECCAK_LANES], unsigned int pos, __contract__( requires(pos <= r && r < sizeof(uint64_t) * MLD_KECCAK_LANES) requires((r / 8) >= 1) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(disjoint((s, sizeof(uint64_t) * MLD_KECCAK_LANES))) + assigns(slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES))) ) { uint8_t b = 0x80; @@ -143,10 +141,8 @@ __contract__( (r == SHAKE256_RATE && pos <= SHAKE256_RATE) || (r == SHA3_512_RATE && pos <= SHA3_512_RATE)) requires(outlen <= 8 * r /* somewhat arbitrary bound */) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - requires(memory_no_alias(out, outlen)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) - assigns(memory_slice(out, outlen)) + requires(disjoint((s, sizeof(uint64_t) * MLD_KECCAK_LANES), (out, outlen))) + assigns(slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES), (out, outlen))) ensures(return_value <= r)) { unsigned int i; @@ -162,7 +158,7 @@ __contract__( while (bytes_to_go > 0) __loop__( - assigns(i, bytes_to_go, pos, out_offset, memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES), memory_slice(out, outlen)) + assigns(i, bytes_to_go, pos, out_offset, slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES), (out, outlen))) invariant(bytes_to_go <= outlen) invariant(out_offset == outlen - bytes_to_go) invariant(pos <= r) diff --git a/mldsa/src/fips202/fips202.h b/mldsa/src/fips202/fips202.h index c97628e28..32f3def97 100644 --- a/mldsa/src/fips202/fips202.h +++ b/mldsa/src/fips202/fips202.h @@ -41,8 +41,8 @@ typedef struct MLD_INTERNAL_API void mld_shake128_init(mld_shake128ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) + requires(disjoint(state)) + assigns(slices(state)) ensures(state->pos == 0) ); @@ -60,10 +60,9 @@ void mld_shake128_absorb(mld_shake128ctx *state, const uint8_t *in, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) - requires(memory_no_alias(in, inlen)) + requires(disjoint(state, (in, inlen))) requires(state->pos <= SHAKE128_RATE) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) + assigns(slices(state)) ensures(state->pos <= SHAKE128_RATE) ); @@ -76,9 +75,9 @@ __contract__( MLD_INTERNAL_API void mld_shake128_finalize(mld_shake128ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) + requires(disjoint(state)) requires(state->pos <= SHAKE128_RATE) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) + assigns(slices(state)) ensures(state->pos <= SHAKE128_RATE) ); @@ -95,11 +94,9 @@ MLD_INTERNAL_API void mld_shake128_squeeze(uint8_t *out, size_t outlen, mld_shake128ctx *state) __contract__( requires(outlen <= 8 * SHAKE128_RATE /* somewhat arbitrary bound */) - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) - requires(memory_no_alias(out, outlen)) + requires(disjoint(state, (out, outlen))) requires(state->pos <= SHAKE128_RATE) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) - assigns(memory_slice(out, outlen)) + assigns(slices(state, (out, outlen))) ensures(state->pos <= SHAKE128_RATE) ); @@ -112,8 +109,8 @@ __contract__( MLD_INTERNAL_API void mld_shake128_release(mld_shake128ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake128ctx))) - assigns(memory_slice(state, sizeof(mld_shake128ctx))) + requires(disjoint(state)) + assigns(slices(state)) ); #define mld_shake256_init MLD_NAMESPACE(shake256_init) @@ -125,8 +122,8 @@ __contract__( MLD_INTERNAL_API void mld_shake256_init(mld_shake256ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) + requires(disjoint(state)) + assigns(slices(state)) ensures(state->pos == 0) ); @@ -144,10 +141,9 @@ void mld_shake256_absorb(mld_shake256ctx *state, const uint8_t *in, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) - requires(memory_no_alias(in, inlen)) + requires(disjoint(state, (in, inlen))) requires(state->pos <= SHAKE256_RATE) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) + assigns(slices(state)) ensures(state->pos <= SHAKE256_RATE) ); @@ -160,9 +156,9 @@ __contract__( MLD_INTERNAL_API void mld_shake256_finalize(mld_shake256ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) + requires(disjoint(state)) requires(state->pos <= SHAKE256_RATE) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) + assigns(slices(state)) ensures(state->pos <= SHAKE256_RATE) ); @@ -179,11 +175,9 @@ MLD_INTERNAL_API void mld_shake256_squeeze(uint8_t *out, size_t outlen, mld_shake256ctx *state) __contract__( requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */) - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) - requires(memory_no_alias(out, outlen)) + requires(disjoint(state, (out, outlen))) requires(state->pos <= SHAKE256_RATE) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) - assigns(memory_slice(out, outlen)) + assigns(slices(state, (out, outlen))) ensures(state->pos <= SHAKE256_RATE) ); @@ -196,8 +190,8 @@ __contract__( MLD_INTERNAL_API void mld_shake256_release(mld_shake256ctx *state) __contract__( - requires(memory_no_alias(state, sizeof(mld_shake256ctx))) - assigns(memory_slice(state, sizeof(mld_shake256ctx))) + requires(disjoint(state)) + assigns(slices(state)) ); #if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_CORE_API_ONLY) @@ -215,9 +209,8 @@ void mld_shake256(uint8_t *out, size_t outlen, const uint8_t *in, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */) - requires(memory_no_alias(in, inlen)) - requires(memory_no_alias(out, outlen)) - assigns(memory_slice(out, outlen)) + requires(disjoint((in, inlen), (out, outlen))) + assigns(slices((out, outlen))) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_CORE_API_ONLY */ diff --git a/mldsa/src/fips202/fips202x4.c b/mldsa/src/fips202/fips202x4.c index 97fbd6a48..b3e914a25 100644 --- a/mldsa/src/fips202/fips202x4.c +++ b/mldsa/src/fips202/fips202x4.c @@ -30,18 +30,15 @@ static void mld_keccak_absorb_once_x4(uint64_t *s, uint32_t r, size_t inlen, uint8_t p) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) + requires(disjoint((s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) requires(r > 0) requires(r <= sizeof(uint64_t) * MLD_KECCAK_LANES) - requires(memory_no_alias(in0, inlen)) - requires(memory_no_alias(in1, inlen)) - requires(memory_no_alias(in2, inlen)) - requires(memory_no_alias(in3, inlen)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) + requires(disjoint((in0, inlen), (in1, inlen), (in2, inlen), (in3, inlen))) + assigns(slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)))) { while (inlen >= r) __loop__( - assigns(inlen, in0, in1, in2, in3, memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) + assigns(inlen, in0, in1, in2, in3, slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) invariant(inlen <= loop_entry(inlen)) invariant(in0 == loop_entry(in0) + (loop_entry(inlen) - inlen)) invariant(in1 == loop_entry(in1) + (loop_entry(inlen) - inlen)) @@ -85,26 +82,20 @@ static void mld_keccak_squeezeblocks_x4(uint8_t *out0, uint8_t *out1, __contract__( requires(r <= sizeof(uint64_t) * MLD_KECCAK_LANES) requires(nblocks <= 8 /* somewhat arbitrary bound */) - requires(memory_no_alias(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - requires(memory_no_alias(out0, nblocks * r)) - requires(memory_no_alias(out1, nblocks * r)) - requires(memory_no_alias(out2, nblocks * r)) - requires(memory_no_alias(out3, nblocks * r)) - assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - assigns(memory_slice(out0, nblocks * r)) - assigns(memory_slice(out1, nblocks * r)) - assigns(memory_slice(out2, nblocks * r)) - assigns(memory_slice(out3, nblocks * r))) + requires(disjoint((s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY), + (out0, nblocks * r), (out1, nblocks * r), + (out2, nblocks * r), (out3, nblocks * r))) + assigns(slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY), + (out0, nblocks * r), (out1, nblocks * r), + (out2, nblocks * r), (out3, nblocks * r)))) { size_t current_offset = 0; while (nblocks > 0) __loop__( assigns(nblocks, current_offset, - memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY), - memory_slice(out0, nblocks * r), - memory_slice(out1, nblocks * r), - memory_slice(out2, nblocks * r), - memory_slice(out3, nblocks * r)) + slices((s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY), + (out0, nblocks * r), (out1, nblocks * r), + (out2, nblocks * r), (out3, nblocks * r))) invariant(nblocks <= loop_entry(nblocks)) invariant(current_offset == (loop_entry(nblocks) - nblocks) * r) decreases(nblocks)) diff --git a/mldsa/src/fips202/fips202x4.h b/mldsa/src/fips202/fips202x4.h index 2f5db18e6..0d882eaeb 100644 --- a/mldsa/src/fips202/fips202x4.h +++ b/mldsa/src/fips202/fips202x4.h @@ -38,12 +38,8 @@ void mld_shake128x4_absorb_once(mld_shake128x4ctx *state, const uint8_t *in0, const uint8_t *in3, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(state, sizeof(mld_shake128x4ctx))) - requires(memory_no_alias(in0, inlen)) - requires(memory_no_alias(in1, inlen)) - requires(memory_no_alias(in2, inlen)) - requires(memory_no_alias(in3, inlen)) - assigns(memory_slice(state, sizeof(mld_shake128x4ctx))) + requires(disjoint(state, (in0, inlen), (in1, inlen), (in2, inlen), (in3, inlen))) + assigns(slices(state)) ); #define mld_shake128x4_squeezeblocks MLD_NAMESPACE(shake128x4_squeezeblocks) @@ -53,16 +49,16 @@ void mld_shake128x4_squeezeblocks(uint8_t *out0, uint8_t *out1, uint8_t *out2, mld_shake128x4ctx *state) __contract__( requires(nblocks <= 8 /* somewhat arbitrary bound */) - requires(memory_no_alias(state, sizeof(mld_shake128x4ctx))) - requires(memory_no_alias(out0, nblocks * SHAKE128_RATE)) - requires(memory_no_alias(out1, nblocks * SHAKE128_RATE)) - requires(memory_no_alias(out2, nblocks * SHAKE128_RATE)) - requires(memory_no_alias(out3, nblocks * SHAKE128_RATE)) - assigns(memory_slice(out0, nblocks * SHAKE128_RATE), - memory_slice(out1, nblocks * SHAKE128_RATE), - memory_slice(out2, nblocks * SHAKE128_RATE), - memory_slice(out3, nblocks * SHAKE128_RATE), - memory_slice(state, sizeof(mld_shake128x4ctx))) + requires(disjoint(state, + (out0, nblocks * SHAKE128_RATE), + (out1, nblocks * SHAKE128_RATE), + (out2, nblocks * SHAKE128_RATE), + (out3, nblocks * SHAKE128_RATE))) + assigns(slices((out0, nblocks * SHAKE128_RATE), + (out1, nblocks * SHAKE128_RATE), + (out2, nblocks * SHAKE128_RATE), + (out3, nblocks * SHAKE128_RATE), + state)) ); #define mld_shake128x4_init MLD_NAMESPACE(shake128x4_init) @@ -84,12 +80,8 @@ void mld_shake256x4_absorb_once(mld_shake256x4ctx *state, const uint8_t *in0, const uint8_t *in3, size_t inlen) __contract__( requires(inlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(state, sizeof(mld_shake256x4ctx))) - requires(memory_no_alias(in0, inlen)) - requires(memory_no_alias(in1, inlen)) - requires(memory_no_alias(in2, inlen)) - requires(memory_no_alias(in3, inlen)) - assigns(memory_slice(state, sizeof(mld_shake256x4ctx))) + requires(disjoint(state, (in0, inlen), (in1, inlen), (in2, inlen), (in3, inlen))) + assigns(slices(state)) ); #define mld_shake256x4_squeezeblocks MLD_NAMESPACE(shake256x4_squeezeblocks) @@ -99,16 +91,16 @@ void mld_shake256x4_squeezeblocks(uint8_t *out0, uint8_t *out1, uint8_t *out2, mld_shake256x4ctx *state) __contract__( requires(nblocks <= 8 /* somewhat arbitrary bound */) - requires(memory_no_alias(state, sizeof(mld_shake256x4ctx))) - requires(memory_no_alias(out0, nblocks * SHAKE256_RATE)) - requires(memory_no_alias(out1, nblocks * SHAKE256_RATE)) - requires(memory_no_alias(out2, nblocks * SHAKE256_RATE)) - requires(memory_no_alias(out3, nblocks * SHAKE256_RATE)) - assigns(memory_slice(out0, nblocks * SHAKE256_RATE), - memory_slice(out1, nblocks * SHAKE256_RATE), - memory_slice(out2, nblocks * SHAKE256_RATE), - memory_slice(out3, nblocks * SHAKE256_RATE), - memory_slice(state, sizeof(mld_shake256x4ctx))) + requires(disjoint(state, + (out0, nblocks * SHAKE256_RATE), + (out1, nblocks * SHAKE256_RATE), + (out2, nblocks * SHAKE256_RATE), + (out3, nblocks * SHAKE256_RATE))) + assigns(slices((out0, nblocks * SHAKE256_RATE), + (out1, nblocks * SHAKE256_RATE), + (out2, nblocks * SHAKE256_RATE), + (out3, nblocks * SHAKE256_RATE), + state)) ); #define mld_shake256x4_init MLD_NAMESPACE(shake256x4_init) diff --git a/mldsa/src/fips202/keccakf1600.h b/mldsa/src/fips202/keccakf1600.h index c0875f4a6..798c95bc2 100644 --- a/mldsa/src/fips202/keccakf1600.h +++ b/mldsa/src/fips202/keccakf1600.h @@ -26,9 +26,8 @@ void mld_keccakf1600_extract_bytes(uint64_t *state, unsigned char *data, __contract__( requires(0 <= offset && offset <= MLD_KECCAK_LANES * sizeof(uint64_t) && 0 <= length && length <= MLD_KECCAK_LANES * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) - requires(memory_no_alias(data, length)) - assigns(memory_slice(data, length)) + requires(disjoint((state, sizeof(uint64_t) * MLD_KECCAK_LANES), (data, length))) + assigns(slices((data, length))) ); #define mld_keccakf1600_xor_bytes MLD_NAMESPACE(keccakf1600_xor_bytes) @@ -38,9 +37,8 @@ void mld_keccakf1600_xor_bytes(uint64_t *state, const unsigned char *data, __contract__( requires(0 <= offset && offset <= MLD_KECCAK_LANES * sizeof(uint64_t) && 0 <= length && length <= MLD_KECCAK_LANES * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) - requires(memory_no_alias(data, length)) - assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(disjoint((state, sizeof(uint64_t) * MLD_KECCAK_LANES), (data, length))) + assigns(slices((state, sizeof(uint64_t) * MLD_KECCAK_LANES))) ); #if (!defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_REDUCE_RAM) || \ @@ -56,15 +54,11 @@ void mld_keccakf1600x4_extract_bytes(uint64_t *state, unsigned char *data0, __contract__( requires(0 <= offset && offset <= MLD_KECCAK_LANES * sizeof(uint64_t) && 0 <= length && length <= MLD_KECCAK_LANES * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - requires(memory_no_alias(data0, length)) - requires(memory_no_alias(data1, length)) - requires(memory_no_alias(data2, length)) - requires(memory_no_alias(data3, length)) - assigns(memory_slice(data0, length)) - assigns(memory_slice(data1, length)) - assigns(memory_slice(data2, length)) - assigns(memory_slice(data3, length)) + requires(disjoint((state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY), + (data0, length), (data1, length), + (data2, length), (data3, length))) + assigns(slices((data0, length), (data1, length), + (data2, length), (data3, length))) ); #define mld_keccakf1600x4_xor_bytes MLD_NAMESPACE(keccakf1600x4_xor_bytes) @@ -77,8 +71,8 @@ void mld_keccakf1600x4_xor_bytes(uint64_t *state, const unsigned char *data0, __contract__( requires(0 <= offset && offset <= MLD_KECCAK_LANES * sizeof(uint64_t) && 0 <= length && length <= MLD_KECCAK_LANES * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - requires(memory_no_alias(data0, length)) + requires(disjoint((state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY), + (data0, length))) /* Case 1: all input buffers are distinct; Case 2: All input buffers are the same */ requires((data0 == data1 && data0 == data2 && @@ -86,15 +80,15 @@ __contract__( (memory_no_alias(data1, length) && memory_no_alias(data2, length) && memory_no_alias(data3, length))) - assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) + assigns(slices((state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) ); #define mld_keccakf1600x4_permute MLD_NAMESPACE(keccakf1600x4_permute) MLD_INTERNAL_API void mld_keccakf1600x4_permute(uint64_t *state) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) - assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) + requires(disjoint((state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) + assigns(slices((state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) ); #endif /* (!MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_REDUCE_RAM || \ MLD_UNIT_TEST) && !MLD_CONFIG_SERIAL_FIPS202_ONLY */ @@ -103,8 +97,8 @@ __contract__( MLD_INTERNAL_API void mld_keccakf1600_permute(uint64_t *state) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) - assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES)) + requires(disjoint((state, sizeof(uint64_t) * MLD_KECCAK_LANES))) + assigns(slices((state, sizeof(uint64_t) * MLD_KECCAK_LANES))) ); #endif /* !MLD_FIPS202_KECCAKF1600_H */ diff --git a/mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h b/mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h index ff6d963ef..7f0120448 100644 --- a/mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h +++ b/mldsa/src/fips202/native/aarch64/src/fips202_native_aarch64.h @@ -21,9 +21,9 @@ MLD_INTERNAL_DATA_DECLARATION const uint64_t void mld_keccak_f1600_x1_scalar_aarch64_asm(uint64_t state[25], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 1))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + assigns(slices((state, sizeof(uint64_t) * 25 * 1))) ); #define mld_keccak_f1600_x1_v84a_aarch64_asm \ @@ -31,9 +31,9 @@ __contract__( void mld_keccak_f1600_x1_v84a_aarch64_asm(uint64_t state[25], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 1))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + assigns(slices((state, sizeof(uint64_t) * 25 * 1))) ); #define mld_keccak_f1600_x2_v84a_aarch64_asm \ @@ -41,9 +41,9 @@ __contract__( void mld_keccak_f1600_x2_v84a_aarch64_asm(uint64_t state[50], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 2))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2)) + assigns(slices((state, sizeof(uint64_t) * 25 * 2))) ); #define mld_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm \ @@ -51,9 +51,9 @@ __contract__( void mld_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm(uint64_t state[100], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 4))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + assigns(slices((state, sizeof(uint64_t) * 25 * 4))) ); #define mld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm \ @@ -61,9 +61,9 @@ __contract__( void mld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm( uint64_t state[100], const uint64_t rc[24]) __contract__( - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 4))) requires(rc == mld_keccakf1600_round_constants) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + assigns(slices((state, sizeof(uint64_t) * 25 * 4))) ); #endif /* !MLD_FIPS202_NATIVE_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H */ diff --git a/mldsa/src/fips202/native/api.h b/mldsa/src/fips202/native/api.h index 3b5b61afc..ccc2746fb 100644 --- a/mldsa/src/fips202/native/api.h +++ b/mldsa/src/fips202/native/api.h @@ -49,8 +49,8 @@ MLD_MUST_CHECK_RETURN_VALUE 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)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 1))) + assigns(slices((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)) ); @@ -59,8 +59,8 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE 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)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 4))) + assigns(slices((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)) ); @@ -92,15 +92,14 @@ static MLD_INLINE int mld_keccakf1600_xor_bytes_x4_native( __contract__( requires(0 <= offset && offset <= 25 * sizeof(uint64_t) && 0 <= length && length <= 25 * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) - requires(memory_no_alias(data0, length)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 4), (data0, length))) requires((data0 == data1 && data0 == data2 && data0 == data3) || (memory_no_alias(data1, length) && memory_no_alias(data2, length) && memory_no_alias(data3, length))) - assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + assigns(slices((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_XOR_BYTES_NATIVE */ @@ -114,15 +113,11 @@ static MLD_INLINE int mld_keccakf1600_extract_bytes_x4_native( __contract__( requires(0 <= offset && offset <= 25 * sizeof(uint64_t) && 0 <= length && length <= 25 * sizeof(uint64_t) - offset) - requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) - requires(memory_no_alias(data0, length)) - requires(memory_no_alias(data1, length)) - requires(memory_no_alias(data2, length)) - requires(memory_no_alias(data3, length)) - assigns(memory_slice(data0, length)) - assigns(memory_slice(data1, length)) - assigns(memory_slice(data2, length)) - assigns(memory_slice(data3, length)) + requires(disjoint((state, sizeof(uint64_t) * 25 * 4), + (data0, length), (data1, length), + (data2, length), (data3, length))) + assigns(slices((data0, length), (data1, length), + (data2, length), (data3, length))) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)); #endif /* MLD_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE */ diff --git a/mldsa/src/fips202/native/x86_64/src/fips202_native_x86_64.h b/mldsa/src/fips202/native/x86_64/src/fips202_native_x86_64.h index 8a64206f1..503ab92b9 100644 --- a/mldsa/src/fips202/native/x86_64/src/fips202_native_x86_64.h +++ b/mldsa/src/fips202/native/x86_64/src/fips202_native_x86_64.h @@ -34,11 +34,11 @@ void mld_keccak_f1600_x4_avx2_asm(uint64_t states[100], const uint64_t rc[24], /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml */ __contract__( - requires(memory_no_alias(states, sizeof(uint64_t) * 25 * 4)) + requires(disjoint((states, sizeof(uint64_t) * 25 * 4))) requires(rc == mld_keccakf1600_round_constants) requires(rho8 == mld_keccak_rho8) requires(rho56 == mld_keccak_rho56) - assigns(memory_slice(states, sizeof(uint64_t) * 25 * 4)) + assigns(slices((states, sizeof(uint64_t) * 25 * 4))) ); #endif /* !MLD_FIPS202_NATIVE_X86_64_SRC_FIPS202_NATIVE_X86_64_H */ diff --git a/mldsa/src/native/aarch64/src/arith_native_aarch64.h b/mldsa/src/native/aarch64/src/arith_native_aarch64.h index 2d5910601..1b75cf305 100644 --- a/mldsa/src/native/aarch64/src/arith_native_aarch64.h +++ b/mldsa/src/native/aarch64/src/arith_native_aarch64.h @@ -66,11 +66,11 @@ void mld_ntt_aarch64_asm(int32_t *r, const int32_t *zetas_l123456, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(zetas_l123456 == mld_aarch64_ntt_zetas_layer123456) requires(zetas_l78 == mld_aarch64_ntt_zetas_layer78) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 75423753)) /* check-magic: on */ @@ -82,11 +82,11 @@ void mld_intt_aarch64_asm(int32_t *r, const int32_t *zetas_l78, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/intt_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(zetas_l78 == mld_aarch64_intt_zetas_layer78) requires(zetas_l123456 == mld_aarch64_intt_zetas_layer123456) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ @@ -120,11 +120,9 @@ void mld_poly_decompose_32_aarch64_asm(int32_t *a1, int32_t *a0) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_decompose_32_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) /* check-magic: 16 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 32)) */ ensures(array_bound(a1, 0, MLDSA_N, 0, 16)) /* check-magic: 261889 == (MLDSA_Q - 1) / 32 + 1 */ @@ -137,11 +135,9 @@ void mld_poly_decompose_88_aarch64_asm(int32_t *a1, int32_t *a0) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_decompose_88_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) /* check-magic: 44 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 88)) */ ensures(array_bound(a1, 0, MLDSA_N, 0, 44)) /* check-magic: 95233 == (MLDSA_Q - 1) / 88 + 1 */ @@ -154,9 +150,9 @@ void mld_poly_caddq_aarch64_asm(int32_t *a) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_caddq_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((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)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) ); @@ -167,11 +163,10 @@ void mld_poly_use_hint_32_aarch64_asm(int32_t *a, const int32_t *h) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (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(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(a, 0, MLDSA_N, 0, 16)) ); @@ -181,11 +176,10 @@ void mld_poly_use_hint_88_aarch64_asm(int32_t *a, const int32_t *h) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (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(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(a, 0, MLDSA_N, 0, 44)) ); #endif /* !MLD_CONFIG_NO_VERIFY_API */ @@ -196,7 +190,7 @@ int mld_poly_chknorm_aarch64_asm(const int32_t *a, int32_t B) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/poly_chknorm_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N))) /* HOL Light precondition: abs(ival(x i)) < 2^31, i.e., a[i] != INT32_MIN */ requires(forall(k0, 0, MLDSA_N, a[k0] > INT32_MIN)) ensures(return_value == 0 || return_value == 1) @@ -212,10 +206,9 @@ void mld_polyz_unpack_17_aarch64_asm(int32_t *r, const uint8_t *buf, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/polyz_unpack_17_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(buf, 576)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (buf, 576))) requires(indices == mld_polyz_unpack_17_indices) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(r, 0, MLDSA_N, -((1 << 17) - 1), (1 << 17) + 1)) ); #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \ @@ -230,10 +223,9 @@ void mld_polyz_unpack_19_aarch64_asm(int32_t *r, const uint8_t *buf, /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/polyz_unpack_19_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(buf, 640)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (buf, 640))) requires(indices == mld_polyz_unpack_19_indices) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(r, 0, MLDSA_N, -((1 << 19) - 1), (1 << 19) + 1)) ); #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \ @@ -248,12 +240,11 @@ void mld_poly_pointwise_montgomery_aarch64_asm(int32_t *a, const int32_t *b) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/aarch64/proofs/pointwise_montgomery_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (b, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ requires(array_abs_bound(a, 0, MLDSA_N, 75423753)) requires(array_abs_bound(b, 0, MLDSA_N, 75423753)) - assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(a, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -269,13 +260,11 @@ void mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm( * proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 4), (b, sizeof(*b) * 4))) /* check-magic: off */ requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -289,13 +278,11 @@ void mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm( * proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 5), (b, sizeof(*b) * 5))) /* check-magic: off */ requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -309,13 +296,11 @@ void mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm( * proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 7), (b, sizeof(*b) * 7))) /* check-magic: off */ requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 2b603b387..5d6211cc0 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -85,9 +85,9 @@ MLD_MUST_CHECK_RETURN_VALUE static MLD_INLINE int mld_ntt_native(int32_t p[MLDSA_N]) __contract__( - requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((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)) + assigns(slices((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)) @@ -123,9 +123,9 @@ __contract__( * that it does not change the bound established at the end of * mld_polyvec_matrix_expand. */ - requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((p, sizeof(int32_t) * MLDSA_N))) requires(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N)) + assigns(slices((p, sizeof(int32_t) * MLDSA_N))) ensures(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q))); #endif /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ @@ -143,9 +143,9 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE static MLD_INLINE int mld_intt_native(int32_t p[MLDSA_N]) __contract__( - requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((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)) + assigns(slices((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)) @@ -177,9 +177,8 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len, __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)) + requires(disjoint((r, sizeof(int32_t) * len), (buf, buflen))) + assigns(slices((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)) ); @@ -211,9 +210,8 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len, __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)) + requires(disjoint((r, sizeof(int32_t) * len), (buf, buflen))) + assigns(slices((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))) ); @@ -245,9 +243,8 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len, __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)) + requires(disjoint((r, sizeof(int32_t) * len), (buf, buflen))) + assigns(slices((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))) ); @@ -274,11 +271,9 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE static MLD_INLINE int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0) __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a1, sizeof(int32_t) * MLDSA_N), (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)) @@ -306,11 +301,9 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE static MLD_INLINE int mld_poly_decompose_88_native(int32_t *a1, int32_t *a0) __contract__( - requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a1, sizeof(int32_t) * MLDSA_N), (a0, sizeof(int32_t) * MLDSA_N))) requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) - assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a1, sizeof(int32_t) * MLDSA_N), (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)) @@ -331,9 +324,9 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE 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(disjoint((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)) + assigns(slices((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)) @@ -356,11 +349,10 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h) __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (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(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((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-1)/(2*MLDSA_GAMMA2))) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N)) @@ -382,11 +374,10 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h) __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (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(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((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-1)/(2*MLDSA_GAMMA2))) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N)) @@ -414,7 +405,7 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE 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(disjoint((a, sizeof(int32_t) * MLDSA_N))) requires(0 <= B && B <= MLDSA_Q - MLD_REDUCE32_RANGE_MAX) requires(array_bound(a, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX)) ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == 0 || @@ -439,9 +430,8 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE 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)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, MLDSA_POLYZ_PACKEDBYTES))) + assigns(slices((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)) @@ -465,9 +455,8 @@ __contract__( MLD_MUST_CHECK_RETURN_VALUE 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)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N), (a, MLDSA_POLYZ_PACKEDBYTES))) + assigns(slices((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)) @@ -493,11 +482,10 @@ MLD_MUST_CHECK_RETURN_VALUE static MLD_INLINE int mld_poly_pointwise_montgomery_native( 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(disjoint((a, sizeof(int32_t) * MLDSA_N), (b, 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(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((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_abs_bound(a, 0, MLDSA_N, MLDSA_Q)) ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(a, 0, MLDSA_N, MLD_NTT_BOUND)) @@ -525,14 +513,12 @@ 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]) __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(disjoint((w, sizeof(int32_t) * MLDSA_N), (u, sizeof(*u) * 4), (v, sizeof(*v) * 4))) 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)) + assigns(slices((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)) @@ -558,14 +544,12 @@ 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]) __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(disjoint((w, sizeof(int32_t) * MLDSA_N), (u, sizeof(*u) * 5), (v, sizeof(*v) * 5))) 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)) + assigns(slices((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)) @@ -591,14 +575,12 @@ 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]) __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(disjoint((w, sizeof(int32_t) * MLDSA_N), (u, sizeof(*u) * 7), (v, sizeof(*v) * 7))) 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)) + assigns(slices((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)) diff --git a/mldsa/src/native/x86_64/src/arith_native_x86_64.h b/mldsa/src/native/x86_64/src/arith_native_x86_64.h index 7c2975e5e..751a78fcc 100644 --- a/mldsa/src/native/x86_64/src/arith_native_x86_64.h +++ b/mldsa/src/native/x86_64/src/arith_native_x86_64.h @@ -36,10 +36,10 @@ void mld_ntt_avx2_asm(int32_t *r, const int32_t *qdata) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/ntt_avx2_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(qdata == mld_qdata) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 42035262)) /* check-magic: on */ @@ -50,10 +50,10 @@ void mld_invntt_avx2_asm(int32_t *r, const int32_t *qdata) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/intt_avx2_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) requires(qdata == mld_qdata) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ ensures(array_abs_bound(r, 0, MLDSA_N, 6285313)) /* check-magic: on */ @@ -64,9 +64,9 @@ void mld_nttunpack_avx2_asm(int32_t *r) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/nttunpack_avx2_asm.ml */ __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, MLDSA_N, 8380417)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) /* Output is a permutation of input: every output coefficient * is some input coefficient */ ensures(forall(i, 0, MLDSA_N, exists(j, 0, MLDSA_N, @@ -126,13 +126,12 @@ void mld_pointwise_avx2_asm(int32_t *a, const int32_t *b, const int32_t *qdata) /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/pointwise_avx2_asm.ml */ __contract__( - requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((a, sizeof(int32_t) * MLDSA_N), (b, sizeof(int32_t) * MLDSA_N))) /* check-magic: off */ requires(array_abs_bound(a, 0, MLDSA_N, 75423753)) requires(array_abs_bound(b, 0, MLDSA_N, 75423753)) requires(qdata == mld_qdata) - assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N)) + assigns(slices((a, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(a, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -145,14 +144,12 @@ void mld_pointwise_acc_l4_avx2_asm(int32_t c[MLDSA_N], /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/pointwise_acc_l4_avx2_asm.ml */ __contract__( - requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N)) + requires(disjoint((c, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 4), (b, sizeof(*b) * 4))) /* check-magic: off */ requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) requires(qdata == mld_qdata) - assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N)) + assigns(slices((c, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(c, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -165,14 +162,12 @@ void mld_pointwise_acc_l5_avx2_asm(int32_t c[MLDSA_N], /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/pointwise_acc_l5_avx2_asm.ml */ __contract__( - requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N)) + requires(disjoint((c, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 5), (b, sizeof(*b) * 5))) /* check-magic: off */ requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) requires(qdata == mld_qdata) - assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N)) + assigns(slices((c, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(c, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); @@ -185,14 +180,12 @@ void mld_pointwise_acc_l7_avx2_asm(int32_t c[MLDSA_N], /* This must be kept in sync with the HOL-Light specification * in proofs/hol_light/x86_64/proofs/pointwise_acc_l7_avx2_asm.ml */ __contract__( - requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N)) - requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N)) - requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N)) + requires(disjoint((c, sizeof(int32_t) * MLDSA_N), (a, sizeof(*a) * 7), (b, sizeof(*b) * 7))) /* check-magic: off */ requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417))) requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753))) requires(qdata == mld_qdata) - assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N)) + assigns(slices((c, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(c, 0, MLDSA_N, 8380417)) /* check-magic: on */ ); diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c index 6d2c47909..116d739e1 100644 --- a/mldsa/src/packing.c +++ b/mldsa/src/packing.c @@ -118,14 +118,14 @@ int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0, * before the call), so a data-dependent early return is fine. */ for (k = 0; k < MLDSA_K; k++) __loop__( - assigns(k, j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES)) + assigns(k, j, n, slices((sig_h, MLDSA_POLYVECH_PACKEDBYTES))) invariant(k <= MLDSA_K && n <= MLDSA_OMEGA) decreases(MLDSA_K - k) ) { for (j = 0; j < MLDSA_N; j++) __loop__( - assigns(j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES)) + assigns(j, n, slices((sig_h, MLDSA_POLYVECH_PACKEDBYTES))) invariant(j <= MLDSA_N && n <= MLDSA_OMEGA) decreases(MLDSA_N - j) ) diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h index 023998018..f5282559c 100644 --- a/mldsa/src/packing.h +++ b/mldsa/src/packing.h @@ -20,11 +20,10 @@ MLD_INTERNAL_API void mld_pack_sk_s1(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES], const mld_polyvecl *s1) __contract__( - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - requires(memory_no_alias(s1, sizeof(mld_polyvecl))) + requires(disjoint((sk, MLDSA_CRYPTO_SECRETKEYBYTES), s1)) requires(forall(k1, 0, MLDSA_L, array_abs_bound(s1->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) - assigns(memory_slice(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + assigns(slices((sk, MLDSA_CRYPTO_SECRETKEYBYTES))) ); #define mld_pack_sk_rho_key_tr_s2 MLD_NAMESPACE_KL(pack_sk_rho_key_tr_s2) @@ -47,14 +46,11 @@ void mld_pack_sk_rho_key_tr_s2(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES], const uint8_t key[MLDSA_SEEDBYTES], const mld_polyveck *s2) __contract__( - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - requires(memory_no_alias(tr, MLDSA_TRBYTES)) - requires(memory_no_alias(key, MLDSA_SEEDBYTES)) - requires(memory_no_alias(s2, sizeof(mld_polyveck))) + requires(disjoint((sk, MLDSA_CRYPTO_SECRETKEYBYTES), (rho, MLDSA_SEEDBYTES), + (tr, MLDSA_TRBYTES), (key, MLDSA_SEEDBYTES), s2)) requires(forall(k2, 0, MLDSA_K, array_abs_bound(s2->vec[k2].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) - assigns(memory_slice(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + assigns(slices((sk, MLDSA_CRYPTO_SECRETKEYBYTES))) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API */ @@ -71,9 +67,8 @@ MLD_INTERNAL_API void mld_pack_sig_c(uint8_t sig[MLDSA_CRYPTO_BYTES], const uint8_t c[MLDSA_CTILDEBYTES]) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(c, MLDSA_CTILDEBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), (c, MLDSA_CTILDEBYTES))) + assigns(slices((sig, MLDSA_CRYPTO_BYTES))) ); #define mld_pack_sig_h MLD_NAMESPACE_KL(pack_sig_h) @@ -95,12 +90,10 @@ MLD_MUST_CHECK_RETURN_VALUE int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0, const mld_polyveck *w1) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(w0, sizeof(mld_polyveck))) - requires(memory_no_alias(w1, sizeof(mld_polyveck))) - assigns(memory_slice( - sig + MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES, - MLDSA_POLYVECH_PACKEDBYTES)) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), w0, w1)) + assigns(slices( + (sig + MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES, + MLDSA_POLYVECH_PACKEDBYTES))) ensures(return_value == 0 || return_value == MLD_ERR_FAIL) ); @@ -119,11 +112,10 @@ MLD_INTERNAL_API void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi, unsigned i) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(zi, sizeof(mld_poly))) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), zi)) requires(i < MLDSA_L) requires(array_bound(zi->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns(slices((sig, MLDSA_CRYPTO_BYTES))) ); #endif /* !MLD_CONFIG_NO_SIGN_API */ @@ -142,10 +134,9 @@ void mld_unpack_pk_t1(mld_poly *t1, const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], unsigned int i) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(t1, sizeof(mld_poly))) + requires(disjoint((pk, MLDSA_CRYPTO_PUBLICKEYBYTES), t1)) requires(i < MLDSA_K) - assigns(memory_slice(t1, sizeof(mld_poly))) + assigns(slices(t1)) ensures(array_bound(t1->coeffs, 0, MLDSA_N, 0, 1 << 10)) ); #endif /* !MLD_CONFIG_NO_VERIFY_API */ @@ -171,19 +162,11 @@ void mld_unpack_sk(uint8_t rho[MLDSA_SEEDBYTES], uint8_t tr[MLDSA_TRBYTES], mld_sk_s1hat *s1, mld_sk_s2hat *s2, const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES]) __contract__( - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - requires(memory_no_alias(tr, MLDSA_TRBYTES)) - requires(memory_no_alias(key, MLDSA_SEEDBYTES)) - requires(memory_no_alias(t0, sizeof(mld_sk_t0hat))) - requires(memory_no_alias(s1, sizeof(mld_sk_s1hat))) - requires(memory_no_alias(s2, sizeof(mld_sk_s2hat))) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(rho, MLDSA_SEEDBYTES)) - assigns(memory_slice(tr, MLDSA_TRBYTES)) - assigns(memory_slice(key, MLDSA_SEEDBYTES)) - assigns(memory_slice(t0, sizeof(mld_sk_t0hat))) - assigns(memory_slice(s1, sizeof(mld_sk_s1hat))) - assigns(memory_slice(s2, sizeof(mld_sk_s2hat))) + requires(disjoint((rho, MLDSA_SEEDBYTES), (tr, MLDSA_TRBYTES), + (key, MLDSA_SEEDBYTES), t0, s1, s2, + (sk, MLDSA_CRYPTO_SECRETKEYBYTES))) + assigns(slices((rho, MLDSA_SEEDBYTES), (tr, MLDSA_TRBYTES), + (key, MLDSA_SEEDBYTES), t0, s1, s2)) MLD_IF_NOT_REDUCE_RAM( ensures(forall(k0, 0, MLDSA_K, array_abs_bound(t0->vec.vec[k0].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) @@ -231,10 +214,9 @@ MLD_MUST_CHECK_RETURN_VALUE int mld_sig_unpack_hints(mld_poly *h, const uint8_t sig[MLDSA_CRYPTO_BYTES], unsigned int i) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(h, sizeof(mld_poly))) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), h)) requires(i < MLDSA_K) - assigns(memory_slice(h, sizeof(mld_poly))) + assigns(slices(h)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL) ensures(return_value == 0 ==> array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) ); diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index 09f3ab00b..a34ba0da5 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -52,9 +52,9 @@ void mld_poly_reduce(mld_poly *a) MLD_STATIC_TESTABLE void mld_poly_caddq_c(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ) { @@ -101,7 +101,7 @@ void mld_poly_add(mld_poly *r, const mld_poly *b) unsigned int i; for (i = 0; i < MLDSA_N; ++i) __loop__( - assigns(i, memory_slice(r, sizeof(mld_poly))) + assigns(i, slices(r)) invariant(i <= MLDSA_N) invariant(forall(k0, i, MLDSA_N, r->coeffs[k0] == loop_entry(*r).coeffs[k0])) invariant(forall(k1, 0, i, r->coeffs[k1] == loop_entry(*r).coeffs[k1] + b->coeffs[k1])) @@ -221,10 +221,10 @@ __contract__( requires(1 <= len && len <= MLDSA_N / 2 && start + 2 * len <= MLDSA_N) requires(0 <= bound && bound < INT32_MAX - MLDSA_Q) requires(-MLDSA_Q_HALF < zeta && zeta < MLDSA_Q_HALF) - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(array_abs_bound(r, 0, start, bound + MLDSA_Q)) requires(array_abs_bound(r, start, MLDSA_N, bound)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, start + 2*len, bound + MLDSA_Q)) ensures(array_abs_bound(r, start + 2 * len, MLDSA_N, bound))) { @@ -263,10 +263,10 @@ __contract__( /* Reference: Embedded in `ntt()` in the reference implementation @[REF]. */ static MLD_INLINE void mld_ntt_layer(int32_t r[MLDSA_N], const unsigned layer) __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(1 <= layer && layer <= 8) requires(array_abs_bound(r, 0, MLDSA_N, layer * MLDSA_Q)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, (layer + 1) * MLDSA_Q))) { unsigned start, k, len; @@ -289,9 +289,9 @@ __contract__( MLD_STATIC_TESTABLE void mld_poly_ntt_c(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ) { @@ -357,10 +357,10 @@ __contract__( * @[REF] */ static MLD_INLINE void mld_invntt_layer(int32_t r[MLDSA_N], unsigned layer) __contract__( - requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(disjoint((r, sizeof(int32_t) * MLDSA_N))) requires(1 <= layer && layer <= 8) requires(array_abs_bound(r, 0, MLDSA_N, (MLDSA_N >> layer) * MLDSA_Q)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + assigns(slices((r, sizeof(int32_t) * MLDSA_N))) ensures(array_abs_bound(r, 0, MLDSA_N, (MLDSA_N >> (layer - 1)) * MLDSA_Q))) { unsigned start, k, len; @@ -396,9 +396,9 @@ __contract__( MLD_STATIC_TESTABLE void mld_poly_invntt_tomont_c(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_INTT_BOUND)) ) { @@ -461,11 +461,10 @@ void mld_poly_invntt_tomont(mld_poly *a) MLD_STATIC_TESTABLE void mld_poly_pointwise_montgomery_c(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(disjoint(a, b)) 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(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) ) { @@ -514,7 +513,7 @@ void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a) for (i = 0; i < MLDSA_N; ++i) __loop__( - assigns(i, memory_slice(a0, sizeof(mld_poly)), memory_slice(a1, sizeof(mld_poly))) + assigns(i, slices(a0, a1)) invariant(i <= MLDSA_N) invariant(forall(k0, i, MLDSA_N, a->coeffs[k0] == loop_entry(*a).coeffs[k0])) invariant(array_bound(a0->coeffs, 0, i, -(MLD_2_POW_D/2)+1, (MLD_2_POW_D/2)+1)) @@ -548,10 +547,9 @@ MLD_STATIC_TESTABLE unsigned int mld_rej_uniform_c(int32_t *a, __contract__( requires(offset <= target && target <= MLDSA_N) requires(buflen <= (MLD_POLY_UNIFORM_NBLOCKS * MLD_STREAM128_BLOCKBYTES) && buflen % 3 == 0) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) + requires(disjoint((a, sizeof(int32_t) * target), (buf, buflen))) requires(array_bound(a, 0, offset, 0, MLDSA_Q)) - assigns(memory_slice(a, sizeof(int32_t) * target)) + assigns(slices((a, sizeof(int32_t) * target))) ensures(offset <= return_value && return_value <= target) ensures(array_bound(a, 0, return_value, 0, MLDSA_Q)) ) @@ -610,10 +608,9 @@ static unsigned int mld_rej_uniform(int32_t *a, unsigned int target, __contract__( requires(offset <= target && target <= MLDSA_N) requires(buflen <= (MLD_POLY_UNIFORM_NBLOCKS * MLD_STREAM128_BLOCKBYTES) && buflen % 3 == 0) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) + requires(disjoint((a, sizeof(int32_t) * target), (buf, buflen))) requires(array_bound(a, 0, offset, 0, MLDSA_Q)) - assigns(memory_slice(a, sizeof(int32_t) * target)) + assigns(slices((a, sizeof(int32_t) * target))) ensures(offset <= return_value && return_value <= target) ensures(array_bound(a, 0, return_value, 0, MLDSA_Q)) ) @@ -660,7 +657,7 @@ void mld_poly_uniform(mld_poly *a, const uint8_t seed[MLDSA_SEEDBYTES + 2]) buflen = MLD_STREAM128_BLOCKBYTES; while (ctr < MLDSA_N) __loop__( - assigns(ctr, state, memory_slice(a, sizeof(mld_poly)), object_whole(buf)) + assigns(ctr, state, object_whole(buf), slices(a)) invariant(ctr <= MLDSA_N) invariant(array_bound(a->coeffs, 0, ctr, 0, MLDSA_Q)) invariant(state.pos <= SHAKE128_RATE) @@ -715,9 +712,7 @@ void mld_poly_uniform_4x(mld_poly *vec0, mld_poly *vec1, mld_poly *vec2, while (ctr[0] < MLDSA_N || ctr[1] < MLDSA_N || ctr[2] < MLDSA_N || ctr[3] < MLDSA_N) __loop__( - assigns(ctr, state, object_whole(buf), - memory_slice(vec0, sizeof(mld_poly)), memory_slice(vec1, sizeof(mld_poly)), - memory_slice(vec2, sizeof(mld_poly)), memory_slice(vec3, sizeof(mld_poly))) + assigns(ctr, state, object_whole(buf), slices(vec0, vec1, vec2, vec3)) invariant(ctr[0] <= MLDSA_N && ctr[1] <= MLDSA_N) invariant(ctr[2] <= MLDSA_N && ctr[3] <= MLDSA_N) invariant(array_bound(vec0->coeffs, 0, ctr[0], 0, MLDSA_Q)) @@ -913,7 +908,7 @@ void mld_polyt0_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYT0_PACKEDBYTES]) 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(disjoint(a)) requires(0 <= B && B <= MLDSA_Q - MLD_REDUCE32_RANGE_MAX) requires(array_bound(a->coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX)) ensures(return_value == 0 || return_value == 0xFFFFFFFF) diff --git a/mldsa/src/poly.h b/mldsa/src/poly.h index ddde0f054..36f96f154 100644 --- a/mldsa/src/poly.h +++ b/mldsa/src/poly.h @@ -34,9 +34,9 @@ typedef struct MLD_INTERNAL_API void mld_poly_reduce(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint(a)) requires(array_bound(a->coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_bound(a->coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX)) ); @@ -50,9 +50,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_caddq(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ); @@ -74,11 +74,10 @@ __contract__( MLD_INTERNAL_API void mld_poly_add(mld_poly *r, const mld_poly *b) __contract__( - requires(memory_no_alias(b, sizeof(mld_poly))) - requires(memory_no_alias(r, sizeof(mld_poly))) + requires(disjoint(b, r)) requires(forall(k0, 0, MLDSA_N, (int64_t) r->coeffs[k0] + b->coeffs[k0] < MLD_REDUCE32_DOMAIN_MAX)) requires(forall(k1, 0, MLDSA_N, (int64_t) r->coeffs[k1] + b->coeffs[k1] >= INT32_MIN)) - assigns(memory_slice(r, sizeof(mld_poly))) + assigns(slices(r)) ensures(forall(k2, 0, MLDSA_N, r->coeffs[k2] == old(*r).coeffs[k2] + b->coeffs[k2])) ensures(forall(k3, 0, MLDSA_N, r->coeffs[k3] < MLD_REDUCE32_DOMAIN_MAX)) ensures(forall(k4, 0, MLDSA_N, r->coeffs[k4] >= INT32_MIN)) @@ -102,11 +101,10 @@ __contract__( MLD_INTERNAL_API void mld_poly_sub(mld_poly *r, const mld_poly *b) __contract__( - requires(memory_no_alias(b, sizeof(mld_poly))) - requires(memory_no_alias(r, sizeof(mld_poly))) + requires(disjoint(b, r)) requires(array_abs_bound(r->coeffs, 0, MLDSA_N, MLDSA_Q)) requires(array_abs_bound(b->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(r, sizeof(mld_poly))) + assigns(slices(r)) ensures(array_bound(r->coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX)) ); #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */ @@ -122,9 +120,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_shiftl(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint(a)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, 1 << 10)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ); #endif /* !MLD_CONFIG_NO_VERIFY_API */ @@ -138,9 +136,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_ntt(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ); @@ -157,9 +155,9 @@ __contract__( MLD_INTERNAL_API void mld_poly_invntt_tomont(mld_poly *a) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint(a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_INTT_BOUND)) ); @@ -179,11 +177,10 @@ __contract__( MLD_INTERNAL_API void mld_poly_pointwise_montgomery(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(disjoint(a, b)) 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(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q)) ); #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API || \ @@ -204,14 +201,12 @@ __contract__( MLD_INTERNAL_API void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a) __contract__( - requires(memory_no_alias(a0, sizeof(mld_poly))) - requires(memory_no_alias(a1, sizeof(mld_poly))) + requires(disjoint(a0, a1)) /* The implementation does not require a0 == a, but the single call site * aliases them and asserting equality simplifies the proof. */ requires(a0 == a) 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))) + assigns(slices(a1, a0)) ensures(array_bound(a0->coeffs, 0, MLDSA_N, -(MLD_2_POW_D/2)+1, (MLD_2_POW_D/2)+1)) ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1)) ); @@ -229,9 +224,8 @@ __contract__( MLD_INTERNAL_API void mld_poly_uniform(mld_poly *a, const uint8_t seed[MLDSA_SEEDBYTES + 2]) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_SEEDBYTES + 2)) - assigns(memory_slice(a, sizeof(mld_poly))) + requires(disjoint(a, (seed, MLDSA_SEEDBYTES + 2))) + assigns(slices(a)) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ); @@ -254,15 +248,8 @@ void mld_poly_uniform_4x(mld_poly *vec0, mld_poly *vec1, mld_poly *vec2, mld_poly *vec3, uint8_t seed[4][MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)]) __contract__( - requires(memory_no_alias(vec0, sizeof(mld_poly))) - requires(memory_no_alias(vec1, sizeof(mld_poly))) - requires(memory_no_alias(vec2, sizeof(mld_poly))) - requires(memory_no_alias(vec3, sizeof(mld_poly))) - requires(memory_no_alias(seed, 4 * MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2))) - assigns(memory_slice(vec0, sizeof(mld_poly))) - assigns(memory_slice(vec1, sizeof(mld_poly))) - assigns(memory_slice(vec2, sizeof(mld_poly))) - assigns(memory_slice(vec3, sizeof(mld_poly))) + requires(disjoint(vec0, vec1, vec2, vec3, (seed, 4 * MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)))) + assigns(slices(vec0, vec1, vec2, vec3)) ensures(array_bound(vec0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ensures(array_bound(vec1->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ensures(array_bound(vec2->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) @@ -284,10 +271,9 @@ __contract__( MLD_INTERNAL_API void mld_polyt1_pack(uint8_t r[MLDSA_POLYT1_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYT1_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint((r, MLDSA_POLYT1_PACKEDBYTES), a)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, 1 << 10)) - assigns(memory_slice(r, MLDSA_POLYT1_PACKEDBYTES)) + assigns(slices((r, MLDSA_POLYT1_PACKEDBYTES))) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API */ @@ -303,9 +289,8 @@ __contract__( MLD_INTERNAL_API void mld_polyt1_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYT1_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(a, MLDSA_POLYT1_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(disjoint(r, (a, MLDSA_POLYT1_PACKEDBYTES))) + assigns(slices(r)) ensures(array_bound(r->coeffs, 0, MLDSA_N, 0, 1 << 10)) ); #endif /* !MLD_CONFIG_NO_VERIFY_API */ @@ -322,10 +307,9 @@ __contract__( MLD_INTERNAL_API void mld_polyt0_pack(uint8_t r[MLDSA_POLYT0_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYT0_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint((r, MLDSA_POLYT0_PACKEDBYTES), a)) requires(array_bound(a->coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)) - assigns(memory_slice(r, MLDSA_POLYT0_PACKEDBYTES)) + assigns(slices((r, MLDSA_POLYT0_PACKEDBYTES))) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API */ @@ -340,9 +324,8 @@ __contract__( MLD_INTERNAL_API void mld_polyt0_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYT0_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(a, MLDSA_POLYT0_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(disjoint(r, (a, MLDSA_POLYT0_PACKEDBYTES))) + assigns(slices(r)) ensures(array_bound(r->coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)) ); #endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */ @@ -368,7 +351,7 @@ MLD_INTERNAL_API MLD_MUST_CHECK_RETURN_VALUE uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint(a)) requires(0 <= B && B <= MLDSA_Q - MLD_REDUCE32_RANGE_MAX) requires(array_bound(a->coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX)) ensures(return_value == 0 || return_value == 0xFFFFFFFF) diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index 4ce6ac7a6..5bd297612 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -41,11 +41,9 @@ MLD_STATIC_TESTABLE void mld_poly_decompose_c(mld_poly *a1, mld_poly *a0) __contract__( - requires(memory_no_alias(a1, sizeof(mld_poly))) - requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(disjoint(a1, a0)) requires(array_bound(a0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(mld_poly))) - assigns(memory_slice(a0, sizeof(mld_poly))) + assigns(slices(a1, a0)) 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)) ) @@ -54,7 +52,7 @@ __contract__( mld_assert_bound(a0->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))) + assigns(i, slices(a0, a1)) invariant(i <= MLDSA_N) invariant(array_bound(a0->coeffs, i, MLDSA_N, 0, MLDSA_Q)) invariant(array_bound(a1->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) @@ -106,11 +104,10 @@ void mld_poly_decompose(mld_poly *a1, mld_poly *a0) #if !defined(MLD_CONFIG_NO_VERIFY_API) MLD_STATIC_TESTABLE void mld_poly_use_hint_c(mld_poly *a, const mld_poly *h) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(h, sizeof(mld_poly))) + requires(disjoint(a, h)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ) { @@ -208,10 +205,9 @@ MLD_STATIC_TESTABLE unsigned int mld_rej_eta_c(int32_t *a, unsigned int target, __contract__( requires(offset <= target && target <= MLDSA_N) requires(buflen <= (MLD_POLY_UNIFORM_ETA_NBLOCKS * MLD_STREAM256_BLOCKBYTES)) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) + requires(disjoint((a, sizeof(int32_t) * target), (buf, buflen))) requires(array_abs_bound(a, 0, offset, MLDSA_ETA + 1)) - assigns(memory_slice(a, sizeof(int32_t) * target)) + assigns(slices((a, sizeof(int32_t) * target))) ensures(offset <= return_value && return_value <= target) ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) ) @@ -281,10 +277,9 @@ static unsigned int mld_rej_eta(int32_t *a, unsigned int target, __contract__( requires(offset <= target && target <= MLDSA_N) requires(buflen <= (MLD_POLY_UNIFORM_ETA_NBLOCKS * MLD_STREAM256_BLOCKBYTES)) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) + requires(disjoint((a, sizeof(int32_t) * target), (buf, buflen))) requires(array_abs_bound(a, 0, offset, MLDSA_ETA + 1)) - assigns(memory_slice(a, sizeof(int32_t) * target)) + assigns(slices((a, sizeof(int32_t) * target))) ensures(offset <= return_value && return_value <= target) ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) ) @@ -375,11 +370,9 @@ void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, while (ctr[0] < MLDSA_N || ctr[1] < MLDSA_N || ctr[2] < MLDSA_N || ctr[3] < MLDSA_N) __loop__( - assigns(ctr, state, memory_slice(r0, sizeof(mld_poly)), - memory_slice(r1, sizeof(mld_poly)), memory_slice(r2, sizeof(mld_poly)), - memory_slice(r3, sizeof(mld_poly)), object_whole(buf[0]), + assigns(ctr, state, object_whole(buf[0]), object_whole(buf[1]), object_whole(buf[2]), - object_whole(buf[3])) + object_whole(buf[3]), slices(r0, r1, r2, r3)) invariant(ctr[0] <= MLDSA_N && ctr[1] <= MLDSA_N) invariant(ctr[2] <= MLDSA_N && ctr[3] <= MLDSA_N) invariant(array_abs_bound(r0->coeffs, 0, ctr[0], MLDSA_ETA + 1)) @@ -445,7 +438,7 @@ void mld_poly_uniform_eta(mld_poly *r, const uint8_t seed[MLDSA_CRHBYTES], while (ctr < MLDSA_N) __loop__( assigns(ctr, object_whole(&state), - object_whole(buf), memory_slice(r, sizeof(mld_poly))) + object_whole(buf), slices(r)) invariant(ctr <= MLDSA_N) invariant(state.pos <= SHAKE256_RATE) invariant(array_abs_bound(r->coeffs, 0, ctr, MLDSA_ETA + 1))) @@ -591,7 +584,7 @@ void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES]) for (i = MLDSA_N - MLDSA_TAU; i < MLDSA_N; ++i) __loop__( - assigns(i, j, object_whole(buf), state, pos, memory_slice(c, sizeof(mld_poly)), signs) + assigns(i, j, object_whole(buf), state, pos, signs, slices(c)) invariant(i >= MLDSA_N - MLDSA_TAU) invariant(i <= MLDSA_N) invariant(pos >= 1) @@ -803,9 +796,8 @@ void mld_polyz_pack(uint8_t r[MLDSA_POLYZ_PACKEDBYTES], const mld_poly *a) 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))) + requires(disjoint(r, (a, MLDSA_POLYZ_PACKEDBYTES))) + assigns(slices(r)) ensures(array_bound(r->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ) { diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h index 2e5163ce1..8d04a89bc 100644 --- a/mldsa/src/poly_kl.h +++ b/mldsa/src/poly_kl.h @@ -29,11 +29,9 @@ MLD_INTERNAL_API void mld_poly_decompose(mld_poly *a1, mld_poly *a0) __contract__( - requires(memory_no_alias(a1, sizeof(mld_poly))) - requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(disjoint(a1, a0)) requires(array_bound(a0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(mld_poly))) - assigns(memory_slice(a0, sizeof(mld_poly))) + assigns(slices(a1, a0)) 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)) ); @@ -51,11 +49,10 @@ __contract__( MLD_INTERNAL_API void mld_poly_use_hint(mld_poly *a, const mld_poly *h) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(h, sizeof(mld_poly))) + requires(disjoint(a, h)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) - assigns(memory_slice(a, sizeof(mld_poly))) + assigns(slices(a)) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ); #endif /* !MLD_CONFIG_NO_VERIFY_API */ @@ -84,15 +81,8 @@ void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, uint8_t nonce3) __contract__( - requires(memory_no_alias(r0, sizeof(mld_poly))) - requires(memory_no_alias(r1, sizeof(mld_poly))) - requires(memory_no_alias(r2, sizeof(mld_poly))) - requires(memory_no_alias(r3, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) - assigns(memory_slice(r0, sizeof(mld_poly))) - assigns(memory_slice(r1, sizeof(mld_poly))) - assigns(memory_slice(r2, sizeof(mld_poly))) - assigns(memory_slice(r3, sizeof(mld_poly))) + requires(disjoint(r0, r1, r2, r3, (seed, MLDSA_CRHBYTES))) + assigns(slices(r0, r1, r2, r3)) ensures(array_abs_bound(r0->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) ensures(array_abs_bound(r1->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) ensures(array_abs_bound(r2->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) @@ -115,9 +105,8 @@ MLD_INTERNAL_API void mld_poly_uniform_eta(mld_poly *r, const uint8_t seed[MLDSA_CRHBYTES], uint8_t nonce) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(disjoint(r, (seed, MLDSA_CRHBYTES))) + assigns(slices(r)) ensures(array_abs_bound(r->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) ); #endif /* MLD_CONFIG_SERIAL_FIPS202_ONLY */ @@ -141,9 +130,8 @@ MLD_INTERNAL_API void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES], uint16_t nonce) __contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) - assigns(memory_slice(a, sizeof(mld_poly))) + requires(disjoint(a, (seed, MLDSA_CRHBYTES))) + assigns(slices(a)) ensures(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ); #endif /* MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_SERIAL_FIPS202_ONLY || \ @@ -174,15 +162,8 @@ void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, uint16_t nonce0, uint16_t nonce1, uint16_t nonce2, uint16_t nonce3) __contract__( - requires(memory_no_alias(r0, sizeof(mld_poly))) - requires(memory_no_alias(r1, sizeof(mld_poly))) - requires(memory_no_alias(r2, sizeof(mld_poly))) - requires(memory_no_alias(r3, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) - assigns(memory_slice(r0, sizeof(mld_poly))) - assigns(memory_slice(r1, sizeof(mld_poly))) - assigns(memory_slice(r2, sizeof(mld_poly))) - assigns(memory_slice(r3, sizeof(mld_poly))) + requires(disjoint(r0, r1, r2, r3, (seed, MLDSA_CRHBYTES))) + assigns(slices(r0, r1, r2, r3)) ensures(array_bound(r0->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ensures(array_bound(r1->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ensures(array_bound(r2->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) @@ -204,9 +185,8 @@ __contract__( MLD_INTERNAL_API void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES]) __contract__( - requires(memory_no_alias(c, sizeof(mld_poly))) - requires(memory_no_alias(seed, MLDSA_CTILDEBYTES)) - assigns(memory_slice(c, sizeof(mld_poly))) + requires(disjoint(c, (seed, MLDSA_CTILDEBYTES))) + assigns(slices(c)) /* All coefficients of c are -1, 0 or +1 */ ensures(array_bound(c->coeffs, 0, MLDSA_N, -1, 2)) ); @@ -224,10 +204,9 @@ __contract__( MLD_INTERNAL_API void mld_polyeta_pack(uint8_t r[MLDSA_POLYETA_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint((r, MLDSA_POLYETA_PACKEDBYTES), a)) requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) - assigns(memory_slice(r, MLDSA_POLYETA_PACKEDBYTES)) + assigns(slices((r, MLDSA_POLYETA_PACKEDBYTES))) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API */ @@ -258,9 +237,8 @@ __contract__( MLD_INTERNAL_API void mld_polyeta_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, sizeof(mld_poly))) - requires(memory_no_alias(a, MLDSA_POLYETA_PACKEDBYTES)) - assigns(memory_slice(r, sizeof(mld_poly))) + requires(disjoint(r, (a, MLDSA_POLYETA_PACKEDBYTES))) + assigns(slices(r)) ensures(array_bound(r->coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1)) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_SIGN_API */ @@ -278,10 +256,9 @@ __contract__( MLD_INTERNAL_API void mld_polyz_pack(uint8_t r[MLDSA_POLYZ_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYZ_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint((r, MLDSA_POLYZ_PACKEDBYTES), a)) requires(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) - assigns(memory_slice(r, MLDSA_POLYZ_PACKEDBYTES)) + assigns(slices((r, MLDSA_POLYZ_PACKEDBYTES))) ); #endif /* !MLD_CONFIG_NO_SIGN_API */ @@ -297,9 +274,8 @@ __contract__( MLD_INTERNAL_API void mld_polyz_unpack(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))) + requires(disjoint(r, (a, MLDSA_POLYZ_PACKEDBYTES))) + assigns(slices(r)) ensures(array_bound(r->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ); @@ -315,10 +291,9 @@ __contract__( MLD_INTERNAL_API void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) __contract__( - requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES)) - requires(memory_no_alias(a, sizeof(mld_poly))) + requires(disjoint((r, MLDSA_POLYW1_PACKEDBYTES), a)) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) - assigns(memory_slice(r, MLDSA_POLYW1_PACKEDBYTES)) + assigns(slices((r, MLDSA_POLYW1_PACKEDBYTES))) ); #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */ diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index e02fc07db..0b82117a4 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -84,7 +84,7 @@ void mld_polyvecl_ntt(mld_polyvecl *v) for (i = 0; i < MLDSA_L; ++i) __loop__( - assigns(i, memory_slice(v, sizeof(mld_polyvecl))) + assigns(i, slices(v)) invariant(i <= MLDSA_L) invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) @@ -103,14 +103,12 @@ void mld_polyvecl_ntt(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(disjoint(w, u, v)) 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))) + assigns(slices(w)) ensures(array_abs_bound(w->coeffs, 0, MLDSA_N, MLDSA_Q)) ) { @@ -119,7 +117,7 @@ __contract__( mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND); for (i = 0; i < MLDSA_N; i++) __loop__( - assigns(i, j, memory_slice(w, sizeof(mld_poly))) + assigns(i, j, slices(w)) invariant(i <= MLDSA_N) invariant(array_abs_bound(w->coeffs, 0, i, MLDSA_Q)) decreases(MLDSA_N - i) @@ -251,7 +249,7 @@ void mld_polyveck_reduce(mld_polyveck *v) for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(i, memory_slice(v, sizeof(mld_polyveck))) + assigns(i, slices(v)) invariant(i <= MLDSA_K) invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) invariant(forall(k2, 0, i, @@ -277,7 +275,7 @@ void mld_polyveck_caddq(mld_polyveck *v) for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(i, memory_slice(v, sizeof(mld_polyveck))) + assigns(i, slices(v)) invariant(i <= MLDSA_K) invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) invariant(forall(k1, 0, i, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) @@ -300,7 +298,7 @@ void mld_polyveck_ntt(mld_polyveck *v) for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(i, memory_slice(v, sizeof(mld_polyveck))) + assigns(i, slices(v)) invariant(i <= MLDSA_K) invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) @@ -322,7 +320,7 @@ void mld_polyveck_invntt_tomont(mld_polyveck *v) for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(i, memory_slice(v, sizeof(mld_polyveck))) + assigns(i, slices(v)) invariant(i <= MLDSA_K) invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) @@ -373,7 +371,7 @@ void mld_polyveck_decompose(mld_polyveck *v1, mld_polyveck *v0) for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(i, memory_slice(v0, sizeof(mld_polyveck)), memory_slice(v1, sizeof(mld_polyveck))) + assigns(i, slices(v0, v1)) invariant(i <= MLDSA_K) invariant(forall(k1, 0, i, array_bound(v1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))) @@ -404,7 +402,7 @@ void mld_polyveck_pack_w1(uint8_t r[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES], for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(i, memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES)) + assigns(i, slices((r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))) invariant(i <= MLDSA_K) decreases(MLDSA_K - i) ) @@ -423,7 +421,7 @@ void mld_polyveck_pack_eta(uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES], mld_assert_abs_bound_2d(p->vec, MLDSA_K, MLDSA_N, MLDSA_ETA + 1); for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(i, memory_slice(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) + assigns(i, slices((r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES))) invariant(i <= MLDSA_K) decreases(MLDSA_K - i) ) @@ -440,7 +438,7 @@ void mld_polyvecl_pack_eta(uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES], mld_assert_abs_bound_2d(p->vec, MLDSA_L, MLDSA_N, MLDSA_ETA + 1); for (i = 0; i < MLDSA_L; ++i) __loop__( - assigns(i, memory_slice(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) + assigns(i, slices((r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES))) invariant(i <= MLDSA_L) decreases(MLDSA_L - i) ) diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h index 68cc71f75..c47358081 100644 --- a/mldsa/src/polyvec.h +++ b/mldsa/src/polyvec.h @@ -42,10 +42,9 @@ void mld_polyvecl_uniform_gamma1(mld_polyvecl *v, const uint8_t seed[MLDSA_CRHBYTES], uint16_t nonce) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) + requires(disjoint(v, (seed, MLDSA_CRHBYTES))) requires(nonce <= (UINT16_MAX - MLDSA_L) / MLDSA_L) - assigns(memory_slice(v, sizeof(mld_polyvecl))) + assigns(slices(v)) ensures(forall(k0, 0, MLDSA_L, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ); @@ -66,9 +65,9 @@ __contract__( MLD_INTERNAL_API void mld_polyvecl_ntt(mld_polyvecl *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(disjoint(v)) requires(forall(k0, 0, MLDSA_L, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyvecl))) + assigns(slices(v)) ensures(forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API || \ @@ -97,14 +96,12 @@ MLD_INTERNAL_API void mld_polyvecl_pointwise_acc_montgomery(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(disjoint(w, u, v)) 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))) + assigns(slices(w)) ensures(array_abs_bound(w->coeffs, 0, MLDSA_N, MLDSA_Q)) ); #endif /* !MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */ @@ -125,7 +122,7 @@ MLD_INTERNAL_API MLD_MUST_CHECK_RETURN_VALUE uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t B) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(disjoint(v)) requires(0 <= B && B <= (MLDSA_Q - 1) / 8) requires(forall(k0, 0, MLDSA_L, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))) @@ -152,10 +149,10 @@ typedef struct MLD_INTERNAL_API void mld_polyveck_reduce(mld_polyveck *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(disjoint(v)) requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX))) - assigns(memory_slice(v, sizeof(mld_polyveck))) + assigns(slices(v)) ensures(forall(k1, 0, MLDSA_K, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))) ); @@ -173,10 +170,10 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_caddq(mld_polyveck *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(disjoint(v)) requires(forall(k0, 0, MLDSA_K, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyveck))) + assigns(slices(v)) ensures(forall(k1, 0, MLDSA_K, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) ); @@ -194,9 +191,9 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_ntt(mld_polyveck *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(disjoint(v)) requires(forall(k0, 0, MLDSA_K, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyveck))) + assigns(slices(v)) ensures(forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ); #endif /* (!MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST) && \ @@ -216,9 +213,9 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_invntt_tomont(mld_polyveck *v) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(disjoint(v)) requires(forall(k0, 0, MLDSA_K, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyveck))) + assigns(slices(v)) ensures(forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) ); #endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */ @@ -239,7 +236,7 @@ MLD_INTERNAL_API MLD_MUST_CHECK_RETURN_VALUE uint32_t mld_polyveck_chknorm(const mld_polyveck *v, int32_t B) __contract__( - requires(memory_no_alias(v, sizeof(mld_polyveck))) + requires(disjoint(v)) requires(0 <= B && B <= (MLDSA_Q - 1) / 8) requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, @@ -271,12 +268,10 @@ __contract__( MLD_INTERNAL_API void mld_polyveck_decompose(mld_polyveck *v1, mld_polyveck *v0) __contract__( - requires(memory_no_alias(v1, sizeof(mld_polyveck))) - requires(memory_no_alias(v0, sizeof(mld_polyveck))) + requires(disjoint(v1, v0)) requires(forall(k0, 0, MLDSA_K, array_bound(v0->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) - assigns(memory_slice(v1, sizeof(mld_polyveck))) - assigns(memory_slice(v0, sizeof(mld_polyveck))) + assigns(slices(v1, v0)) ensures(forall(k1, 0, MLDSA_K, array_bound(v1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))) ensures(forall(k2, 0, MLDSA_K, @@ -298,11 +293,10 @@ MLD_INTERNAL_API void mld_polyveck_pack_w1(uint8_t r[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES], const mld_polyveck *w1) __contract__( - requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES)) - requires(memory_no_alias(w1, sizeof(mld_polyveck))) + requires(disjoint((r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES), w1)) requires(forall(k1, 0, MLDSA_K, array_bound(w1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))) - assigns(memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES)) + assigns(slices((r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))) ); #endif /* !MLD_CONFIG_NO_SIGN_API */ @@ -319,11 +313,10 @@ MLD_INTERNAL_API void mld_polyveck_pack_eta(uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES], const mld_polyveck *p) __contract__( - requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyveck))) + requires(disjoint((r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES), p)) requires(forall(k1, 0, MLDSA_K, array_abs_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) - assigns(memory_slice(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) + assigns(slices((r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES))) ); #define mld_polyvecl_pack_eta MLD_NAMESPACE_KL(polyvecl_pack_eta) @@ -338,11 +331,10 @@ MLD_INTERNAL_API void mld_polyvecl_pack_eta(uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES], const mld_polyvecl *p) __contract__( - requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyvecl))) + requires(disjoint((r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES), p)) requires(forall(k1, 0, MLDSA_L, array_abs_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) - assigns(memory_slice(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) + assigns(slices((r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES))) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API */ @@ -361,9 +353,8 @@ MLD_INTERNAL_API void mld_polyvecl_unpack_eta( mld_polyvecl *p, const uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyvecl))) - assigns(memory_slice(p, sizeof(mld_polyvecl))) + requires(disjoint((r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES), p)) + assigns(slices(p)) ensures(forall(k1, 0, MLDSA_L, array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) ); @@ -383,9 +374,8 @@ MLD_INTERNAL_API void mld_polyvecl_unpack_z(mld_polyvecl *z, const uint8_t r[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) - requires(memory_no_alias(z, sizeof(mld_polyvecl))) - assigns(memory_slice(z, sizeof(mld_polyvecl))) + requires(disjoint((r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES), z)) + assigns(slices(z)) ensures(forall(k1, 0, MLDSA_L, array_bound(z->vec[k1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ); @@ -405,9 +395,8 @@ MLD_INTERNAL_API void mld_polyveck_unpack_eta( mld_polyveck *p, const uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyveck))) - assigns(memory_slice(p, sizeof(mld_polyveck))) + requires(disjoint((r, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES), p)) + assigns(slices(p)) ensures(forall(k1, 0, MLDSA_K, array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) ); diff --git a/mldsa/src/polyvec_lazy.c b/mldsa/src/polyvec_lazy.c index 6e0971fb6..21c0b19e1 100644 --- a/mldsa/src/polyvec_lazy.c +++ b/mldsa/src/polyvec_lazy.c @@ -40,10 +40,8 @@ static MLD_INLINE void mld_polymat_expand_entry( mld_poly *p, uint8_t seed_ext[MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)], uint8_t l, uint8_t k) __contract__( - requires(memory_no_alias(p, sizeof(mld_poly))) - requires(memory_no_alias(seed_ext, MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2))) - assigns(memory_slice(p, sizeof(mld_poly))) - assigns(memory_slice(seed_ext, MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2))) + requires(disjoint(p, (seed_ext, MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)))) + assigns(slices(p, (seed_ext, MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)))) ensures(array_bound(p->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ) { @@ -76,7 +74,7 @@ void mld_polyvec_matrix_expand_eager(mld_polymat_eager *mat, /* Sample 4 matrix entries a time. */ for (i = 0; i < (MLDSA_K * MLDSA_L / 4) * 4; i += 4) __loop__( - assigns(i, j, object_whole(seed_ext), memory_slice(mat, sizeof(mld_polymat_eager))) + assigns(i, j, object_whole(seed_ext), slices(mat)) invariant(i <= (MLDSA_K * MLDSA_L / 4) * 4 && i % 4 == 0) /* vectors 0 .. i / MLDSA_L are completely sampled */ invariant(forall(k1, 0, i / MLDSA_L, forall(l1, 0, MLDSA_L, @@ -122,7 +120,7 @@ void mld_polyvec_matrix_expand_eager(mld_polymat_eager *mat, /* Entries omitted by the batch-sampling are sampled individually. */ while (i < MLDSA_K * MLDSA_L) __loop__( - assigns(i, object_whole(seed_ext), memory_slice(mat, sizeof(mld_polymat_eager))) + assigns(i, object_whole(seed_ext), slices(mat)) invariant(i <= MLDSA_K * MLDSA_L) /* vectors 0 .. i / MLDSA_L are completely sampled */ invariant(forall(k1, 0, i / MLDSA_L, forall(l1, 0, MLDSA_L, @@ -165,7 +163,7 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_eager(mld_polyveck *w, for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(i, memory_slice(w, sizeof(mld_polyveck))) + assigns(i, slices(w)) invariant(i <= MLDSA_K) invariant(forall(k0, 0, i, array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) @@ -207,9 +205,7 @@ void mld_polyvec_matrix_pointwise_montgomery_row_lazy(mld_poly *t_row, for (l = 1; l < MLDSA_L; ++l) __loop__( - assigns(l, object_whole(seed_ext), - memory_slice(t_row, sizeof(mld_poly)), - memory_slice(mat, sizeof(mld_polymat_lazy))) + assigns(l, object_whole(seed_ext), slices(t_row, mat)) invariant(l >= 1 && l <= MLDSA_L) invariant(array_abs_bound(t_row->coeffs, 0, MLDSA_N, l * MLDSA_Q)) decreases(MLDSA_L - l) @@ -246,10 +242,7 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(mld_polyveck *w, /* Column-by-column: sample y[l], NTT, accumulate column l of A into w. */ for (l = 0; l < MLDSA_L; l++) __loop__( - assigns(k, l, object_whole(seed_ext), - memory_slice(w, sizeof(mld_polyveck)), - memory_slice(mat, sizeof(mld_polymat_lazy)), - memory_slice(scratch, sizeof(mld_polyvecl))) + assigns(k, l, object_whole(seed_ext), slices(w, mat, scratch)) invariant(l <= MLDSA_L) invariant(l == 0 || forall(k0, 0, MLDSA_K, @@ -262,9 +255,7 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(mld_polyveck *w, mld_poly_ntt(y_ntt); for (k = 0; k < MLDSA_K; k++) __loop__( - assigns(k, object_whole(seed_ext), - memory_slice(w, sizeof(mld_polyveck)), - memory_slice(mat, sizeof(mld_polymat_lazy))) + assigns(k, object_whole(seed_ext), slices(w, mat)) invariant(k <= MLDSA_K) invariant(l != 0 || forall(k1, 0, k, diff --git a/mldsa/src/polyvec_lazy.h b/mldsa/src/polyvec_lazy.h index 8149220bc..71d9f31f2 100644 --- a/mldsa/src/polyvec_lazy.h +++ b/mldsa/src/polyvec_lazy.h @@ -142,9 +142,8 @@ static MLD_INLINE void mld_unpack_sk_s1hat_eager( mld_sk_s1hat_eager *s1, const uint8_t packed_s1[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(s1, sizeof(mld_sk_s1hat_eager))) - requires(memory_no_alias(packed_s1, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) - assigns(memory_slice(s1, sizeof(mld_sk_s1hat_eager))) + requires(disjoint(s1, (packed_s1, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES))) + assigns(slices(s1)) ensures(forall(k1, 0, MLDSA_L, array_abs_bound(s1->vec.vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ) @@ -158,11 +157,10 @@ static MLD_INLINE void mld_sk_s1hat_get_poly_eager(mld_poly *buf, const mld_sk_s1hat_eager *s1, unsigned int i) __contract__( - requires(memory_no_alias(buf, sizeof(mld_poly))) - requires(memory_no_alias(s1, sizeof(mld_sk_s1hat_eager))) + requires(disjoint(buf, s1)) requires(i < MLDSA_L) requires(array_abs_bound(s1->vec.vec[i].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) - assigns(memory_slice(buf, sizeof(mld_poly))) + assigns(slices(buf)) ensures(array_abs_bound(buf->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ) { *buf = s1->vec.vec[i]; } #endif /* !MLD_CONFIG_NO_SIGN_API */ @@ -172,8 +170,8 @@ static MLD_INLINE void mld_unpack_sk_s1hat_lazy( mld_sk_s1hat_lazy *s1, const uint8_t packed_s1[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(s1, sizeof(mld_sk_s1hat_lazy))) - assigns(memory_slice(s1, sizeof(mld_sk_s1hat_lazy))) + requires(disjoint(s1)) + assigns(slices(s1)) ensures(s1->packed == old(packed_s1)) ) { s1->packed = packed_s1; } @@ -182,11 +180,10 @@ static MLD_INLINE void mld_sk_s1hat_get_poly_lazy(mld_poly *buf, const mld_sk_s1hat_lazy *s1, unsigned int i) __contract__( - requires(memory_no_alias(buf, sizeof(mld_poly))) - requires(memory_no_alias(s1, sizeof(mld_sk_s1hat_lazy))) + requires(disjoint(buf, s1)) requires(i < MLDSA_L) - requires(memory_no_alias(s1->packed, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) - assigns(memory_slice(buf, sizeof(mld_poly))) + requires(disjoint((s1->packed, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES))) + assigns(slices(buf)) ensures(array_abs_bound(buf->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ) { @@ -204,9 +201,8 @@ static MLD_INLINE void mld_unpack_sk_s2hat_eager( mld_sk_s2hat_eager *s2, const uint8_t packed_s2[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(s2, sizeof(mld_sk_s2hat_eager))) - requires(memory_no_alias(packed_s2, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) - assigns(memory_slice(s2, sizeof(mld_sk_s2hat_eager))) + requires(disjoint(s2, (packed_s2, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES))) + assigns(slices(s2)) ensures(forall(k1, 0, MLDSA_K, array_abs_bound(s2->vec.vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ) @@ -220,11 +216,10 @@ static MLD_INLINE void mld_sk_s2hat_get_poly_eager(mld_poly *buf, const mld_sk_s2hat_eager *s2, unsigned int i) __contract__( - requires(memory_no_alias(buf, sizeof(mld_poly))) - requires(memory_no_alias(s2, sizeof(mld_sk_s2hat_eager))) + requires(disjoint(buf, s2)) requires(i < MLDSA_K) requires(array_abs_bound(s2->vec.vec[i].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) - assigns(memory_slice(buf, sizeof(mld_poly))) + assigns(slices(buf)) ensures(array_abs_bound(buf->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ) { *buf = s2->vec.vec[i]; } #endif /* !MLD_CONFIG_NO_SIGN_API */ @@ -235,8 +230,8 @@ static MLD_INLINE void mld_unpack_sk_s2hat_lazy( mld_sk_s2hat_lazy *s2, const uint8_t packed_s2[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES]) __contract__( - requires(memory_no_alias(s2, sizeof(mld_sk_s2hat_lazy))) - assigns(memory_slice(s2, sizeof(mld_sk_s2hat_lazy))) + requires(disjoint(s2)) + assigns(slices(s2)) ensures(s2->packed == old(packed_s2)) ) { s2->packed = packed_s2; } @@ -245,11 +240,10 @@ static MLD_INLINE void mld_sk_s2hat_get_poly_lazy(mld_poly *buf, const mld_sk_s2hat_lazy *s2, unsigned int i) __contract__( - requires(memory_no_alias(buf, sizeof(mld_poly))) - requires(memory_no_alias(s2, sizeof(mld_sk_s2hat_lazy))) + requires(disjoint(buf, s2)) requires(i < MLDSA_K) - requires(memory_no_alias(s2->packed, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) - assigns(memory_slice(buf, sizeof(mld_poly))) + requires(disjoint((s2->packed, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES))) + assigns(slices(buf)) ensures(array_abs_bound(buf->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ) { @@ -267,9 +261,8 @@ static MLD_INLINE void mld_unpack_sk_t0hat_eager( mld_sk_t0hat_eager *t0, const uint8_t packed_t0[MLDSA_K * MLDSA_POLYT0_PACKEDBYTES]) __contract__( - requires(memory_no_alias(t0, sizeof(mld_sk_t0hat_eager))) - requires(memory_no_alias(packed_t0, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) - assigns(memory_slice(t0, sizeof(mld_sk_t0hat_eager))) + requires(disjoint(t0, (packed_t0, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES))) + assigns(slices(t0)) ensures(forall(k1, 0, MLDSA_K, array_abs_bound(t0->vec.vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ) @@ -277,7 +270,7 @@ __contract__( unsigned int i; for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(i, memory_slice(t0, sizeof(mld_sk_t0hat_eager))) + assigns(i, slices(t0)) invariant(i <= MLDSA_K) invariant(forall(k0, 0, i, array_bound(t0->vec.vec[k0].coeffs, 0, MLDSA_N, @@ -296,11 +289,10 @@ static MLD_INLINE void mld_sk_t0hat_get_poly_eager(mld_poly *buf, const mld_sk_t0hat_eager *t0, unsigned int i) __contract__( - requires(memory_no_alias(buf, sizeof(mld_poly))) - requires(memory_no_alias(t0, sizeof(mld_sk_t0hat_eager))) + requires(disjoint(buf, t0)) requires(i < MLDSA_K) requires(array_abs_bound(t0->vec.vec[i].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) - assigns(memory_slice(buf, sizeof(mld_poly))) + assigns(slices(buf)) ensures(array_abs_bound(buf->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ) { *buf = t0->vec.vec[i]; } #endif /* !MLD_CONFIG_NO_SIGN_API */ @@ -311,8 +303,8 @@ static MLD_INLINE void mld_unpack_sk_t0hat_lazy( mld_sk_t0hat_lazy *t0, const uint8_t packed_t0[MLDSA_K * MLDSA_POLYT0_PACKEDBYTES]) __contract__( - requires(memory_no_alias(t0, sizeof(mld_sk_t0hat_lazy))) - assigns(memory_slice(t0, sizeof(mld_sk_t0hat_lazy))) + requires(disjoint(t0)) + assigns(slices(t0)) ensures(t0->packed == old(packed_t0)) ) { t0->packed = packed_t0; } @@ -321,11 +313,10 @@ static MLD_INLINE void mld_sk_t0hat_get_poly_lazy(mld_poly *buf, const mld_sk_t0hat_lazy *t0, unsigned int i) __contract__( - requires(memory_no_alias(buf, sizeof(mld_poly))) - requires(memory_no_alias(t0, sizeof(mld_sk_t0hat_lazy))) + requires(disjoint(buf, t0)) requires(i < MLDSA_K) - requires(memory_no_alias(t0->packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) - assigns(memory_slice(buf, sizeof(mld_poly))) + requires(disjoint((t0->packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES))) + assigns(slices(buf)) ensures(array_abs_bound(buf->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ) { @@ -343,10 +334,9 @@ __contract__( static MLD_INLINE void mld_yvec_init_eager( mld_yvec_eager *y, const uint8_t rhoprime[MLDSA_CRHBYTES], uint16_t nonce) __contract__( - requires(memory_no_alias(y, sizeof(mld_yvec_eager))) - requires(memory_no_alias(rhoprime, MLDSA_CRHBYTES)) + requires(disjoint(y, (rhoprime, MLDSA_CRHBYTES))) requires(nonce <= (UINT16_MAX - MLDSA_L) / MLDSA_L) - assigns(memory_slice(y, sizeof(mld_yvec_eager))) + assigns(slices(y)) ensures(forall(k1, 0, MLDSA_L, array_bound(y->vec.vec[k1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ) @@ -358,11 +348,10 @@ static MLD_INLINE void mld_yvec_get_poly_eager(mld_poly *buf, const mld_yvec_eager *y, unsigned int i) __contract__( - requires(memory_no_alias(buf, sizeof(mld_poly))) - requires(memory_no_alias(y, sizeof(mld_yvec_eager))) + requires(disjoint(buf, y)) requires(i < MLDSA_L) requires(array_bound(y->vec.vec[i].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) - assigns(memory_slice(buf, sizeof(mld_poly))) + assigns(slices(buf)) ensures(array_bound(buf->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ) { *buf = y->vec.vec[i]; } #endif /* !MLD_CONFIG_NO_SIGN_API && (!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST) \ @@ -372,8 +361,8 @@ __contract__( static MLD_INLINE void mld_yvec_init_lazy( mld_yvec_lazy *y, const uint8_t rhoprime[MLDSA_CRHBYTES], uint16_t nonce) __contract__( - requires(memory_no_alias(y, sizeof(mld_yvec_lazy))) - assigns(memory_slice(y, sizeof(mld_yvec_lazy))) + requires(disjoint(y)) + assigns(slices(y)) ensures(y->rhoprime == old(rhoprime)) ensures(y->nonce == old(nonce)) ) @@ -386,12 +375,11 @@ static MLD_INLINE void mld_yvec_get_poly_lazy(mld_poly *buf, const mld_yvec_lazy *y, unsigned int i) __contract__( - requires(memory_no_alias(buf, sizeof(mld_poly))) - requires(memory_no_alias(y, sizeof(mld_yvec_lazy))) + requires(disjoint(buf, y)) requires(i < MLDSA_L) - requires(memory_no_alias(y->rhoprime, MLDSA_CRHBYTES)) + requires(disjoint((y->rhoprime, MLDSA_CRHBYTES))) requires(y->nonce <= ((UINT16_MAX - MLDSA_L) / MLDSA_L)) - assigns(memory_slice(buf, sizeof(mld_poly))) + assigns(slices(buf)) ensures(array_bound(buf->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) ) { @@ -426,9 +414,9 @@ __contract__( /* We don't specify that this is a permutation, only that it preserves * the bounds. * When the native NTT backend does not use the custom order, this is a no-op. */ - requires(memory_no_alias(p, sizeof(mld_poly))) + requires(disjoint(p)) requires(array_bound(p->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(p, sizeof(mld_poly))) + assigns(slices(p)) ensures(array_bound(p->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ) { @@ -452,9 +440,8 @@ MLD_INTERNAL_API void mld_polyvec_matrix_expand_eager(mld_polymat_eager *mat, const uint8_t rho[MLDSA_SEEDBYTES]) __contract__( - requires(memory_no_alias(mat, sizeof(mld_polymat_eager))) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - assigns(memory_slice(mat, sizeof(mld_polymat_eager))) + requires(disjoint(mat, (rho, MLDSA_SEEDBYTES))) + assigns(slices(mat)) ensures(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) ); @@ -477,15 +464,13 @@ void mld_polyvec_matrix_pointwise_montgomery_row_eager(mld_poly *t_row, const mld_polyvecl *v, unsigned int i) __contract__( - requires(memory_no_alias(t_row, sizeof(mld_poly))) - requires(memory_no_alias(mat, sizeof(mld_polymat_eager))) - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(disjoint(t_row, mat, v)) requires(i < MLDSA_K) requires(forall(l1, 0, MLDSA_L, array_bound(mat->vec[i].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) requires(forall(l2, 0, MLDSA_L, array_abs_bound(v->vec[l2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(t_row, sizeof(mld_poly))) + assigns(slices(t_row)) ensures(array_abs_bound(t_row->coeffs, 0, MLDSA_N, MLDSA_Q)) ); @@ -508,16 +493,12 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_eager(mld_polyveck *w, const mld_yvec_eager *y, mld_polyvecl *scratch) __contract__( - requires(memory_no_alias(w, sizeof(mld_polyveck))) - requires(memory_no_alias(mat, sizeof(mld_polymat_eager))) - requires(memory_no_alias(y, sizeof(mld_yvec_eager))) - requires(memory_no_alias(scratch, sizeof(mld_polyvecl))) + requires(disjoint(w, mat, y, scratch)) requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) requires(forall(l2, 0, MLDSA_L, array_bound(y->vec.vec[l2].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - assigns(memory_slice(w, sizeof(mld_polyveck))) - assigns(memory_slice(scratch, sizeof(mld_polyvecl))) + assigns(slices(w, scratch)) ensures(forall(k0, 0, MLDSA_K, array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) ); @@ -529,9 +510,8 @@ MLD_INTERNAL_API void mld_polyvec_matrix_expand_lazy(mld_polymat_lazy *mat, const uint8_t rho[MLDSA_SEEDBYTES]) __contract__( - requires(memory_no_alias(mat, sizeof(mld_polymat_lazy))) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) - assigns(memory_slice(mat, sizeof(mld_polymat_lazy))) + requires(disjoint(mat, (rho, MLDSA_SEEDBYTES))) + assigns(slices(mat)) ); #if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) @@ -554,14 +534,11 @@ void mld_polyvec_matrix_pointwise_montgomery_row_lazy(mld_poly *t_row, const mld_polyvecl *v, unsigned int i) __contract__( - requires(memory_no_alias(t_row, sizeof(mld_poly))) - requires(memory_no_alias(mat, sizeof(mld_polymat_lazy))) - requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(disjoint(t_row, mat, v)) requires(i < MLDSA_K) requires(forall(l1, 0, MLDSA_L, array_abs_bound(v->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(t_row, sizeof(mld_poly))) - assigns(memory_slice(mat, sizeof(mld_polymat_lazy))) + assigns(slices(t_row, mat)) ensures(array_abs_bound(t_row->coeffs, 0, MLDSA_N, MLDSA_Q)) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API */ @@ -588,15 +565,10 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(mld_polyveck *w, const mld_yvec_lazy *y, mld_polyvecl *scratch) __contract__( - requires(memory_no_alias(w, sizeof(mld_polyveck))) - requires(memory_no_alias(mat, sizeof(mld_polymat_lazy))) - requires(memory_no_alias(y, sizeof(mld_yvec_lazy))) - requires(memory_no_alias(scratch, sizeof(mld_polyvecl))) - requires(memory_no_alias(y->rhoprime, MLDSA_CRHBYTES)) + requires(disjoint(w, mat, y, scratch)) + requires(disjoint((y->rhoprime, MLDSA_CRHBYTES))) requires(y->nonce <= ((UINT16_MAX - MLDSA_L) / MLDSA_L)) - assigns(memory_slice(w, sizeof(mld_polyveck))) - assigns(memory_slice(mat, sizeof(mld_polymat_lazy))) - assigns(memory_slice(scratch, sizeof(mld_polyvecl))) + assigns(slices(w, mat, scratch)) ensures(forall(k0, 0, MLDSA_K, array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) ); diff --git a/mldsa/src/randombytes.h b/mldsa/src/randombytes.h index ee34dc9b4..fc1a44d66 100644 --- a/mldsa/src/randombytes.h +++ b/mldsa/src/randombytes.h @@ -18,8 +18,8 @@ int randombytes(uint8_t *out, size_t outlen); MLD_MUST_CHECK_RETURN_VALUE static MLD_INLINE int mld_randombytes(uint8_t *out, size_t outlen) __contract__( - requires(memory_no_alias(out, outlen)) - assigns(memory_slice(out, outlen)) + requires(disjoint((out, outlen))) + assigns(slices((out, outlen))) ) { return randombytes(out, outlen); } #endif /* !MLD_CONFIG_CUSTOM_RANDOMBYTES */ #endif /* !MLD_CONFIG_NO_RANDOMIZED_API */ diff --git a/mldsa/src/rounding.h b/mldsa/src/rounding.h index 21fae3c98..7d1284c07 100644 --- a/mldsa/src/rounding.h +++ b/mldsa/src/rounding.h @@ -47,11 +47,9 @@ */ static MLD_INLINE void mld_power2round(int32_t *a0, int32_t *a1, int32_t a) __contract__( - requires(memory_no_alias(a0, sizeof(int32_t))) - requires(memory_no_alias(a1, sizeof(int32_t))) + requires(disjoint(a0, a1)) requires(a >= 0 && a < MLDSA_Q) - assigns(memory_slice(a0, sizeof(int32_t))) - assigns(memory_slice(a1, sizeof(int32_t))) + assigns(slices(a0, a1)) ensures(*a0 > -(MLD_2_POW_D/2) && *a0 <= (MLD_2_POW_D/2)) ensures(*a1 >= 0 && *a1 <= (MLDSA_Q - 1) / MLD_2_POW_D) ensures((*a1 * MLD_2_POW_D + *a0 - a) % MLDSA_Q == 0) @@ -78,11 +76,9 @@ __contract__( */ static MLD_INLINE void mld_decompose(int32_t *a0, int32_t *a1, int32_t a) __contract__( - requires(memory_no_alias(a0, sizeof(int32_t))) - requires(memory_no_alias(a1, sizeof(int32_t))) + requires(disjoint(a0, a1)) requires(a >= 0 && a < MLDSA_Q) - assigns(memory_slice(a0, sizeof(int32_t))) - assigns(memory_slice(a1, sizeof(int32_t))) + assigns(slices(a0, a1)) /* a0 = -MLDSA_GAMMA2 can only occur when (q-1) = a - (a mod MLDSA_GAMMA2), * then a1=1; and a0 = a - (a mod MLDSA_GAMMA2) - 1 (@[FIPS204, Algorithm 36 (Decompose)]) */ ensures(*a0 >= -MLDSA_GAMMA2 && *a0 <= MLDSA_GAMMA2) diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 05643e20e..14c2cf63f 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -58,8 +58,8 @@ static int mld_check_pct(uint8_t const pk[MLDSA_CRYPTO_PUBLICKEYBYTES], uint8_t const sk[MLDSA_CRYPTO_SECRETKEYBYTES], MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires(disjoint((pk, MLDSA_CRYPTO_PUBLICKEYBYTES), + (sk, MLDSA_CRYPTO_SECRETKEYBYTES))) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY @@ -153,9 +153,7 @@ static int mld_check_pct(uint8_t const pk[MLDSA_CRYPTO_PUBLICKEYBYTES], static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2, const uint8_t seed[MLDSA_CRHBYTES]) __contract__( - requires(memory_no_alias(s1, sizeof(mld_polyvecl))) - requires(memory_no_alias(s2, sizeof(mld_polyveck))) - requires(memory_no_alias(seed, MLDSA_CRHBYTES)) + requires(disjoint(s1, s2, (seed, MLDSA_CRHBYTES))) assigns(object_whole(s1), object_whole(s2)) ensures(forall(l0, 0, MLDSA_L, array_abs_bound(s1->vec[l0].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) ensures(forall(k0, 0, MLDSA_K, array_abs_bound(s2->vec[k0].coeffs, 0, MLDSA_N, MLDSA_ETA + 1))) @@ -232,18 +230,16 @@ static int mld_compute_pack_t0_t1( const uint8_t rho[MLDSA_SEEDBYTES], MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( - requires(memory_no_alias(pk_t1, MLDSA_K * MLDSA_POLYT1_PACKEDBYTES)) - requires(memory_no_alias(t0_packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) - requires(memory_no_alias(s1hat, sizeof(mld_polyvecl))) - requires(memory_no_alias(s2, sizeof(mld_polyveck))) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) + requires(disjoint((pk_t1, MLDSA_K * MLDSA_POLYT1_PACKEDBYTES), + (t0_packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES), + s1hat, s2, (rho, MLDSA_SEEDBYTES))) requires(forall(l1, 0, MLDSA_L, array_abs_bound(s1hat->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) requires(forall(k2, 0, MLDSA_K, array_bound(s2->vec[k2].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) - assigns(memory_slice(pk_t1, MLDSA_K * MLDSA_POLYT1_PACKEDBYTES)) - assigns(memory_slice(t0_packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) + assigns(slices((pk_t1, MLDSA_K * MLDSA_POLYT1_PACKEDBYTES), + (t0_packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES))) ensures(return_value == 0 || return_value == MLD_ERR_OUT_OF_MEMORY)) { unsigned int k; @@ -263,11 +259,10 @@ __contract__( for (k = 0; k < MLDSA_K; k++) __loop__( - assigns(k, memory_slice(pk_t1, MLDSA_K * MLDSA_POLYT1_PACKEDBYTES), - memory_slice(t0_packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES), - memory_slice(t0k, sizeof(mld_poly)), - memory_slice(t1k, sizeof(mld_poly)) - MLD_IF_REDUCE_RAM(, memory_slice(mat, sizeof(mld_polymat)))) + assigns(k, slices((pk_t1, MLDSA_K * MLDSA_POLYT1_PACKEDBYTES), + (t0_packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES), + t0k, t1k) + MLD_IF_REDUCE_RAM(, slices(mat))) invariant(k <= MLDSA_K) decreases(MLDSA_K - k) ) @@ -456,11 +451,11 @@ __contract__( requires(in2len <= MLD_MAX_BUFFER_SIZE) requires(in3len <= MLD_MAX_BUFFER_SIZE) requires(outlen <= 8 * SHAKE256_RATE /* somewhat arbitrary bound */) - requires(memory_no_alias(in1, in1len)) + requires(disjoint((in1, in1len))) requires(in2len == 0 || memory_no_alias(in2, in2len)) requires(in3len == 0 || memory_no_alias(in3, in3len)) - requires(memory_no_alias(out, outlen)) - assigns(memory_slice(out, outlen)) + requires(disjoint((out, outlen))) + assigns(slices((out, outlen))) ) { mld_shake256ctx state; @@ -517,12 +512,7 @@ static int mld_compute_pack_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *cp, const mld_sk_s1hat *s1hat, const mld_yvec *y, mld_poly *z, mld_poly *tmp) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(cp, sizeof(mld_poly))) - requires(memory_no_alias(s1hat, sizeof(mld_sk_s1hat))) - requires(memory_no_alias(y, sizeof(mld_yvec))) - requires(memory_no_alias(z, sizeof(mld_poly))) - requires(memory_no_alias(tmp, sizeof(mld_poly))) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), cp, s1hat, y, z, tmp)) requires(array_abs_bound(cp->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) MLD_IF_NOT_REDUCE_RAM( requires(forall(k0, 0, MLDSA_L, @@ -530,13 +520,11 @@ __contract__( requires(forall(k1, 0, MLDSA_L, array_abs_bound(s1hat->vec.vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ) MLD_IF_REDUCE_RAM( - requires(memory_no_alias(s1hat->packed, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(y->rhoprime, MLDSA_CRHBYTES)) + requires(disjoint((s1hat->packed, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES), + (y->rhoprime, MLDSA_CRHBYTES))) requires(y->nonce <= MLD_NONCE_UB) ) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) - assigns(memory_slice(z, sizeof(mld_poly))) - assigns(memory_slice(tmp, sizeof(mld_poly))) + assigns(slices((sig, MLDSA_CRYPTO_BYTES), z, tmp)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ) @@ -545,9 +533,7 @@ __contract__( uint32_t z_invalid; for (i = 0; i < MLDSA_L; i++) __loop__( - assigns(i, memory_slice(z, sizeof(mld_poly)), - memory_slice(tmp, sizeof(mld_poly)), - memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns(i, slices(z, tmp, (sig, MLDSA_CRYPTO_BYTES))) invariant(i <= MLDSA_L) decreases(MLDSA_L - i) ) @@ -649,13 +635,8 @@ static int mld_attempt_signature_generation( const mld_sk_s1hat *s1hat, const mld_sk_s2hat *s2hat, const mld_sk_t0hat *t0hat, MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(mu, MLDSA_CRHBYTES)) - requires(memory_no_alias(rhoprime, MLDSA_CRHBYTES)) - requires(memory_no_alias(mat, sizeof(mld_polymat))) - requires(memory_no_alias(s1hat, sizeof(mld_sk_s1hat))) - requires(memory_no_alias(s2hat, sizeof(mld_sk_s2hat))) - requires(memory_no_alias(t0hat, sizeof(mld_sk_t0hat))) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), (mu, MLDSA_CRHBYTES), + (rhoprime, MLDSA_CRHBYTES), mat, s1hat, s2hat, t0hat)) requires(nonce <= MLD_NONCE_UB) MLD_IF_NOT_REDUCE_RAM( requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, @@ -665,13 +646,13 @@ __contract__( requires(forall(k4, 0, MLDSA_K, array_abs_bound(s2hat->vec.vec[k4].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ) MLD_IF_REDUCE_RAM( - requires(memory_no_alias(s1hat->packed, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(s2hat->packed, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES)) - requires(memory_no_alias(t0hat->packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES)) + requires(disjoint((s1hat->packed, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES), + (s2hat->packed, MLDSA_K * MLDSA_POLYETA_PACKEDBYTES), + (t0hat->packed, MLDSA_K * MLDSA_POLYT0_PACKEDBYTES))) ) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns(slices((sig, MLDSA_CRYPTO_BYTES))) MLD_IF_REDUCE_RAM( - assigns(memory_slice(mat, sizeof(mld_polymat))) + assigns(slices(mat)) ) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) @@ -884,11 +865,11 @@ int mld_sign_signature_internal(uint8_t sig[MLDSA_CRYPTO_BYTES], size_t *siglen, while (1) __loop__( MLD_IF_NOT_REDUCE_RAM( - assigns(nonce, ret, object_whole(siglen), memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns(nonce, ret, object_whole(siglen), slices((sig, MLDSA_CRYPTO_BYTES))) ) MLD_IF_REDUCE_RAM( - assigns(nonce, ret, object_whole(siglen), memory_slice(sig, MLDSA_CRYPTO_BYTES), - memory_slice(mat, sizeof(mld_polymat))) + assigns(nonce, ret, object_whole(siglen), + slices((sig, MLDSA_CRYPTO_BYTES), mat)) ) invariant(nonce <= nonce_limit) @@ -1157,11 +1138,9 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen, for (i = 0; i < MLDSA_K; ++i) __loop__( - assigns(MLD_IF_REDUCE_RAM(memory_slice(mat, sizeof(mld_polymat)),) + assigns(MLD_IF_REDUCE_RAM(slices(mat),) i, ret, - memory_slice(w1, sizeof(mld_poly)), - memory_slice(tmp, sizeof(mld_poly)), - memory_slice(buf, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES) + slices(w1, tmp, (buf, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES)) ) invariant(i <= MLDSA_K) decreases(MLDSA_K - i) @@ -1284,7 +1263,7 @@ int mld_sign_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen, /* All good, copy msg, return 0 */ for (i = 0; i < *mlen; ++i) __loop__( - assigns(i, memory_slice(m, *mlen)) + assigns(i, slices((m, *mlen))) invariant(i <= *mlen) decreases(*mlen - i) ) diff --git a/mldsa/src/sign.h b/mldsa/src/sign.h index 6a2643abb..78d3238e8 100644 --- a/mldsa/src/sign.h +++ b/mldsa/src/sign.h @@ -122,9 +122,9 @@ int mld_sign_keypair_internal(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], const uint8_t seed[MLDSA_SEEDBYTES], MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - requires(memory_no_alias(seed, MLDSA_SEEDBYTES)) + requires(disjoint((pk, MLDSA_CRYPTO_PUBLICKEYBYTES), + (sk, MLDSA_CRYPTO_SECRETKEYBYTES), + (seed, MLDSA_SEEDBYTES))) assigns(object_whole(pk)) assigns(object_whole(sk)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || @@ -166,8 +166,8 @@ int mld_sign_keypair(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES], MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires(disjoint((pk, MLDSA_CRYPTO_PUBLICKEYBYTES), + (sk, MLDSA_CRYPTO_SECRETKEYBYTES))) assigns(object_whole(pk)) assigns(object_whole(sk)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || @@ -226,14 +226,12 @@ int mld_sign_signature_internal(uint8_t sig[MLDSA_CRYPTO_BYTES], size_t *siglen, __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(prelen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(m, mlen)) - requires(memory_no_alias(rnd, MLDSA_RNDBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), siglen, (m, mlen), + (rnd, MLDSA_RNDBYTES), + (sk, MLDSA_CRYPTO_SECRETKEYBYTES))) requires((externalmu == 0) ==> ((prelen == 0) || memory_no_alias(pre, prelen))) requires((externalmu != 0) ==> (mlen == MLDSA_CRHBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns(slices((sig, MLDSA_CRYPTO_BYTES))) assigns(object_whole(siglen)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY || @@ -280,13 +278,11 @@ int mld_sign_signature(uint8_t sig[MLDSA_CRYPTO_BYTES], size_t *siglen, MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(m, mlen)) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), siglen, (m, mlen))) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + requires(disjoint((sk, MLDSA_CRYPTO_SECRETKEYBYTES))) + assigns(slices((sig, MLDSA_CRYPTO_BYTES))) assigns(object_whole(siglen)) ensures((return_value == 0 && *siglen == MLDSA_CRYPTO_BYTES) || ((return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY || return_value == MLD_ERR_RNG_FAIL || return_value == MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED) && *siglen == 0)) @@ -327,11 +323,10 @@ int mld_sign_signature_extmu(uint8_t sig[MLDSA_CRYPTO_BYTES], size_t *siglen, const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES], MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(mu, MLDSA_CRHBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), siglen, + (mu, MLDSA_CRHBYTES), + (sk, MLDSA_CRYPTO_SECRETKEYBYTES))) + assigns(slices((sig, MLDSA_CRYPTO_BYTES))) assigns(object_whole(siglen)) ensures((return_value == 0 && *siglen == MLDSA_CRYPTO_BYTES) || ((return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY || return_value == MLD_ERR_RNG_FAIL || return_value == MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED) && *siglen == 0)) @@ -369,13 +364,11 @@ int mld_sign(uint8_t *sm, size_t *smlen, const uint8_t *m, size_t mlen, MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sm, MLDSA_CRYPTO_BYTES + mlen)) - requires(memory_no_alias(smlen, sizeof(size_t))) + requires(disjoint((sm, MLDSA_CRYPTO_BYTES + mlen), smlen)) requires(m == sm || memory_no_alias(m, mlen)) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sm, MLDSA_CRYPTO_BYTES + mlen)) + requires(disjoint((ctx, ctxlen), (sk, MLDSA_CRYPTO_SECRETKEYBYTES))) + assigns(slices((sm, MLDSA_CRYPTO_BYTES + mlen))) assigns(object_whole(smlen)) ensures((return_value == 0 && *smlen == MLDSA_CRYPTO_BYTES + mlen) || ((return_value == MLD_ERR_FAIL @@ -427,11 +420,10 @@ __contract__( requires(prelen <= MLD_MAX_BUFFER_SIZE) requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(siglen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(m, mlen)) + requires(disjoint((sig, siglen), (m, mlen))) requires((externalmu == 0) ==> ((prelen == 0) || memory_no_alias(pre, prelen))) requires((externalmu != 0) ==> (mlen == MLDSA_CRHBYTES)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(disjoint((pk, MLDSA_CRYPTO_PUBLICKEYBYTES))) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); @@ -467,10 +459,9 @@ __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(siglen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(m, mlen)) + requires(disjoint((sig, siglen), (m, mlen))) requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(disjoint((pk, MLDSA_CRYPTO_PUBLICKEYBYTES))) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); @@ -504,9 +495,8 @@ int mld_sign_verify_extmu(const uint8_t *sig, size_t siglen, MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( requires(siglen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(mu, MLDSA_CRHBYTES)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(disjoint((sig, siglen), (mu, MLDSA_CRHBYTES), + (pk, MLDSA_CRYPTO_PUBLICKEYBYTES))) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); @@ -538,14 +528,11 @@ int mld_sign_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen, MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( requires(smlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(m, smlen)) - requires(memory_no_alias(mlen, sizeof(size_t))) + requires(disjoint((m, smlen), mlen)) requires(m == sm || memory_no_alias(sm, smlen)) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - assigns(memory_slice(m, smlen)) - assigns(memory_slice(mlen, sizeof(size_t))) + requires(disjoint((ctx, ctxlen), (pk, MLDSA_CRYPTO_PUBLICKEYBYTES))) + assigns(slices((m, smlen), mlen)) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); #endif /* !MLD_CONFIG_CORE_API_ONLY */ @@ -599,13 +586,11 @@ int mld_sign_signature_pre_hash_internal( __contract__( requires(ctxlen <= MLD_MAX_BUFFER_SIZE) requires(phlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(ph, phlen)) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), siglen, (ph, phlen))) requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(rnd, MLDSA_RNDBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + requires(disjoint((rnd, MLDSA_RNDBYTES), + (sk, MLDSA_CRYPTO_SECRETKEYBYTES))) + assigns(slices((sig, MLDSA_CRYPTO_BYTES))) assigns(object_whole(siglen)) ensures((return_value == 0 && *siglen == MLDSA_CRYPTO_BYTES) || ((return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY || return_value == MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED) && *siglen == 0)) @@ -654,10 +639,9 @@ __contract__( requires(phlen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen <= MLD_MAX_BUFFER_SIZE - 77) requires(siglen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(ph, phlen)) + requires(disjoint((sig, siglen), (ph, phlen))) requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(disjoint((pk, MLDSA_CRYPTO_PUBLICKEYBYTES))) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); #endif /* !MLD_CONFIG_NO_VERIFY_API */ @@ -701,13 +685,11 @@ int mld_sign_signature_pre_hash_shake256( __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(siglen, sizeof(size_t))) - requires(memory_no_alias(m, mlen)) + requires(disjoint((sig, MLDSA_CRYPTO_BYTES), siglen, (m, mlen))) requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(rnd, MLDSA_RNDBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + requires(disjoint((rnd, MLDSA_RNDBYTES), + (sk, MLDSA_CRYPTO_SECRETKEYBYTES))) + assigns(slices((sig, MLDSA_CRYPTO_BYTES))) assigns(object_whole(siglen)) ensures((return_value == 0 && *siglen == MLDSA_CRYPTO_BYTES) || ((return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY || return_value == MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED) && *siglen == 0)) @@ -748,10 +730,9 @@ __contract__( requires(mlen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen <= MLD_MAX_BUFFER_SIZE - 77) requires(siglen <= MLD_MAX_BUFFER_SIZE) - requires(memory_no_alias(sig, siglen)) - requires(memory_no_alias(m, mlen)) + requires(disjoint((sig, siglen), (m, mlen))) requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(disjoint((pk, MLDSA_CRYPTO_PUBLICKEYBYTES))) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); #endif /* !MLD_CONFIG_NO_VERIFY_API */ @@ -805,8 +786,8 @@ __contract__( requires(phlen <= MLD_MAX_BUFFER_SIZE) requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen)) requires(hashalg == MLD_PREHASH_NONE || memory_no_alias(ph, phlen)) - requires(memory_no_alias(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES)) - assigns(memory_slice(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES)) + requires(disjoint((prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES))) + assigns(slices((prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES))) ensures(return_value <= MLD_DOMAIN_SEPARATION_MAX_BYTES) ); #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */ @@ -841,9 +822,9 @@ int mld_sign_pk_from_sk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES], MLD_CONFIG_CONTEXT_PARAMETER_TYPE context) __contract__( - requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES)) - assigns(memory_slice(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) + requires(disjoint((pk, MLDSA_CRYPTO_PUBLICKEYBYTES), + (sk, MLDSA_CRYPTO_SECRETKEYBYTES))) + assigns(slices((pk, MLDSA_CRYPTO_PUBLICKEYBYTES))) ensures(return_value == 0 || return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY) ); #endif /* !MLD_CONFIG_NO_KEYPAIR_API */