From 5ef85ede22e98f2acceb542c2dd8d5265ff6ff98 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 6 Jan 2025 03:58:35 +0000 Subject: [PATCH] CBMC: Remove `STATIC_[INLINE_]TESTABLE` STATIC_TESTABLE and STATIC_INLINE_TESTABLE were previously used as wrappers around `static` and `static inline` that were defined as empty for a CBMC build, thereby lifting visibility of static (inline) functions so that CBMC would see them. This commit achieves the same without STATIC_TESTABLE and STATIC_INLINE_TESTABLE, both of which are removed, by defining `static` and `INLINE` as the empty string in a CBMC build. Signed-off-by: Hanno Becker --- cbmc/Makefile.common | 4 + examples/monolithic_build/mlkem_native_all.c | 112 ++++++++----------- mlkem/cbmc.h | 7 -- mlkem/fips202/fips202.c | 13 +-- mlkem/indcpa.c | 14 +-- mlkem/ntt.c | 11 +- mlkem/reduce.h | 9 +- mlkem/rej_uniform.c | 7 +- mlkem/verify.h | 36 +++--- 9 files changed, 89 insertions(+), 124 deletions(-) diff --git a/cbmc/Makefile.common b/cbmc/Makefile.common index bfff4f831..3ea48ab1e 100644 --- a/cbmc/Makefile.common +++ b/cbmc/Makefile.common @@ -535,6 +535,10 @@ ifndef MLKEM_K endif DEFINES += -DMLKEM_K=$(MLKEM_K) +# Give visibility to all static functions +DEFINES += -Dstatic= +DEFINES += -DINLINE= +DEFINES += -DALWAYS_INLINE= # CI currently assumes cbmc invocation has at most one --unwindset diff --git a/examples/monolithic_build/mlkem_native_all.c b/examples/monolithic_build/mlkem_native_all.c index 5e516a6e9..17b80ee27 100644 --- a/examples/monolithic_build/mlkem_native_all.c +++ b/examples/monolithic_build/mlkem_native_all.c @@ -80,161 +80,141 @@ #endif /* mlkem/cbmc.h:13 */ -#if defined(STATIC_INLINE_TESTABLE) -#undef STATIC_INLINE_TESTABLE -#endif - -/* mlkem/cbmc.h:14 */ -#if defined(STATIC_TESTABLE) -#undef STATIC_TESTABLE -#endif - -/* mlkem/cbmc.h:16 */ #if defined(__contract__) #undef __contract__ #endif -/* mlkem/cbmc.h:17 */ +/* mlkem/cbmc.h:14 */ #if defined(__loop__) #undef __loop__ #endif -/* mlkem/cbmc.h:18 */ +/* mlkem/cbmc.h:15 */ #if defined(cassert) #undef cassert #endif -/* mlkem/cbmc.h:23 */ -#if defined(STATIC_TESTABLE) -#undef STATIC_TESTABLE -#endif - -/* mlkem/cbmc.h:24 */ -#if defined(STATIC_INLINE_TESTABLE) -#undef STATIC_INLINE_TESTABLE -#endif - -/* mlkem/cbmc.h:26 */ +/* mlkem/cbmc.h:19 */ #if defined(__contract__) #undef __contract__ #endif -/* mlkem/cbmc.h:27 */ +/* mlkem/cbmc.h:20 */ #if defined(__loop__) #undef __loop__ #endif -/* mlkem/cbmc.h:30 */ +/* mlkem/cbmc.h:23 */ #if defined(assigns) #undef assigns #endif -/* mlkem/cbmc.h:33 */ +/* mlkem/cbmc.h:26 */ #if defined(requires) #undef requires #endif -/* mlkem/cbmc.h:34 */ +/* mlkem/cbmc.h:27 */ #if defined(ensures) #undef ensures #endif -/* mlkem/cbmc.h:36 */ +/* mlkem/cbmc.h:29 */ #if defined(invariant) #undef invariant #endif -/* mlkem/cbmc.h:37 */ +/* mlkem/cbmc.h:30 */ #if defined(decreases) #undef decreases #endif -/* mlkem/cbmc.h:39 */ +/* mlkem/cbmc.h:32 */ #if defined(cassert) #undef cassert #endif -/* mlkem/cbmc.h:40 */ +/* mlkem/cbmc.h:33 */ #if defined(assume) #undef assume #endif -/* mlkem/cbmc.h:51 */ +/* mlkem/cbmc.h:44 */ #if defined(return_value) #undef return_value #endif -/* mlkem/cbmc.h:57 */ +/* mlkem/cbmc.h:50 */ #if defined(object_whole) #undef object_whole #endif -/* mlkem/cbmc.h:58 */ +/* mlkem/cbmc.h:51 */ #if defined(memory_slice) #undef memory_slice #endif -/* mlkem/cbmc.h:59 */ +/* mlkem/cbmc.h:52 */ #if defined(same_object) #undef same_object #endif -/* mlkem/cbmc.h:65 */ +/* mlkem/cbmc.h:58 */ #if defined(memory_no_alias) #undef memory_no_alias #endif -/* mlkem/cbmc.h:66 */ +/* mlkem/cbmc.h:59 */ #if defined(readable) #undef readable #endif -/* mlkem/cbmc.h:67 */ +/* mlkem/cbmc.h:60 */ #if defined(writeable) #undef writeable #endif -/* mlkem/cbmc.h:73 */ +/* mlkem/cbmc.h:66 */ #if defined(old) #undef old #endif -/* mlkem/cbmc.h:74 */ +/* mlkem/cbmc.h:67 */ #if defined(loop_entry) #undef loop_entry #endif -/* mlkem/cbmc.h:86 */ +/* mlkem/cbmc.h:79 */ #if defined(forall) #undef forall #endif -/* mlkem/cbmc.h:93 */ +/* mlkem/cbmc.h:86 */ #if defined(EXISTS) #undef EXISTS #endif -/* mlkem/cbmc.h:119 */ +/* mlkem/cbmc.h:112 */ #if defined(CBMC_CONCAT_) #undef CBMC_CONCAT_ #endif -/* mlkem/cbmc.h:120 */ +/* mlkem/cbmc.h:113 */ #if defined(CBMC_CONCAT) #undef CBMC_CONCAT #endif -/* mlkem/cbmc.h:122 */ +/* mlkem/cbmc.h:115 */ #if defined(array_bound_core) #undef array_bound_core #endif -/* mlkem/cbmc.h:132 */ +/* mlkem/cbmc.h:125 */ #if defined(array_bound) #undef array_bound #endif -/* mlkem/cbmc.h:138 */ +/* mlkem/cbmc.h:131 */ #if defined(array_abs_bound) #undef array_abs_bound #endif @@ -479,7 +459,7 @@ #undef keccak_squeezeblocks #endif -/* mlkem/fips202/fips202.c:186 */ +/* mlkem/fips202/fips202.c:185 */ #if defined(shake256ctx) #undef shake256ctx #endif @@ -1184,7 +1164,7 @@ #undef MLKEM_GEN_MATRIX_NBLOCKS #endif -/* mlkem/indcpa.c:269 */ +/* mlkem/indcpa.c:267 */ #if defined(poly_permute_bitrev_to_custom) #undef poly_permute_bitrev_to_custom #endif @@ -2044,7 +2024,7 @@ #undef invntt_layer #endif -/* mlkem/ntt.c:165 */ +/* mlkem/ntt.c:163 */ #if defined(INVNTT_BOUND_REF) #undef INVNTT_BOUND_REF #endif @@ -2634,82 +2614,82 @@ #undef SYS_BIG_ENDIAN #endif -/* mlkem/sys.h:65 */ +/* mlkem/sys.h:66 */ #if defined(INLINE) #undef INLINE #endif -/* mlkem/sys.h:66 */ +/* mlkem/sys.h:67 */ #if defined(ALWAYS_INLINE) #undef ALWAYS_INLINE #endif -/* mlkem/sys.h:68 */ +/* mlkem/sys.h:69 */ #if defined(INLINE) #undef INLINE #endif -/* mlkem/sys.h:69 */ +/* mlkem/sys.h:70 */ #if defined(ALWAYS_INLINE) #undef ALWAYS_INLINE #endif -/* mlkem/sys.h:71 */ +/* mlkem/sys.h:72 */ #if defined(INLINE) #undef INLINE #endif -/* mlkem/sys.h:72 */ +/* mlkem/sys.h:73 */ #if defined(ALWAYS_INLINE) #undef ALWAYS_INLINE #endif -/* mlkem/sys.h:76 */ +/* mlkem/sys.h:77 */ #if defined(INLINE) #undef INLINE #endif -/* mlkem/sys.h:77 */ +/* mlkem/sys.h:78 */ #if defined(ALWAYS_INLINE) #undef ALWAYS_INLINE #endif -/* mlkem/sys.h:86 */ +/* mlkem/sys.h:88 */ #if defined(RESTRICT) #undef RESTRICT #endif -/* mlkem/sys.h:88 */ +/* mlkem/sys.h:90 */ #if defined(RESTRICT) #undef RESTRICT #endif -/* mlkem/sys.h:93 */ +/* mlkem/sys.h:95 */ #if defined(RESTRICT) #undef RESTRICT #endif -/* mlkem/sys.h:96 */ +/* mlkem/sys.h:98 */ #if defined(DEFAULT_ALIGN) #undef DEFAULT_ALIGN #endif -/* mlkem/sys.h:98 */ +/* mlkem/sys.h:100 */ #if defined(ALIGN) #undef ALIGN #endif -/* mlkem/sys.h:99 */ +/* mlkem/sys.h:101 */ #if defined(asm) #undef asm #endif -/* mlkem/sys.h:101 */ +/* mlkem/sys.h:103 */ #if defined(asm) #undef asm #endif -/* mlkem/sys.h:102 */ +/* mlkem/sys.h:104 */ #if defined(ALIGN) #undef ALIGN #endif diff --git a/mlkem/cbmc.h b/mlkem/cbmc.h index 317a26421..37636100b 100644 --- a/mlkem/cbmc.h +++ b/mlkem/cbmc.h @@ -11,19 +11,12 @@ #ifndef CBMC -#define STATIC_INLINE_TESTABLE static INLINE -#define STATIC_TESTABLE static - #define __contract__(x) #define __loop__(x) #define cassert(x, y) #else /* CBMC _is_ defined, therefore we're doing proof */ -/* expose certain procedures to CBMC proofs that are static otherwise */ -#define STATIC_TESTABLE -#define STATIC_INLINE_TESTABLE - #define __contract__(x) x #define __loop__(x) x diff --git a/mlkem/fips202/fips202.c b/mlkem/fips202/fips202.c index 124f9f4da..b145e1c69 100644 --- a/mlkem/fips202/fips202.c +++ b/mlkem/fips202/fips202.c @@ -43,9 +43,8 @@ * - uint8_t p: domain-separation byte for different * Keccak-derived functions **************************************************/ -STATIC_TESTABLE -void keccak_absorb_once(uint64_t *s, uint32_t r, const uint8_t *m, size_t mlen, - uint8_t p) +static void keccak_absorb_once(uint64_t *s, uint32_t r, const uint8_t *m, + size_t mlen, uint8_t p) __contract__( requires(r <= sizeof(uint64_t) * KECCAK_LANES) requires(memory_no_alias(s, sizeof(uint64_t) * KECCAK_LANES)) @@ -100,8 +99,8 @@ __contract__( * - uint64_t *s_inc: pointer to input/output state * - uint32_t r: rate in bytes (e.g., 168 for SHAKE128) **************************************************/ -STATIC_TESTABLE -void keccak_squeezeblocks(uint8_t *h, size_t nblocks, uint64_t *s, uint32_t r) +static void keccak_squeezeblocks(uint8_t *h, size_t nblocks, uint64_t *s, + uint32_t r) __contract__( requires(r <= sizeof(uint64_t) * KECCAK_LANES) requires(nblocks <= 8 /* somewhat arbitrary bound */) @@ -137,8 +136,8 @@ __contract__( * - uint64_t *s_inc: pointer to Keccak state * - uint32_t r: rate in bytes (e.g., 168 for SHAKE128) **************************************************/ -STATIC_TESTABLE -void keccak_squeeze_once(uint8_t *h, size_t outlen, uint64_t *s, uint32_t r) +static void keccak_squeeze_once(uint8_t *h, size_t outlen, uint64_t *s, + uint32_t r) __contract__( requires(r <= sizeof(uint64_t) * KECCAK_LANES) requires(memory_no_alias(s, sizeof(uint64_t) * KECCAK_LANES)) diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index 6a4bb1062..1c2dbad86 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -154,8 +154,7 @@ static void unpack_ciphertext(polyvec *b, poly *v, * Generate four A matrix entries from a seed, using rejection * sampling on the output of a XOF. */ -STATIC_TESTABLE -void gen_matrix_entry_x4(poly *vec, uint8_t *seed[4]) +static void gen_matrix_entry_x4(poly *vec, uint8_t *seed[4]) __contract__( requires(memory_no_alias(vec, sizeof(poly) * 4)) requires(memory_no_alias(seed, sizeof(uint8_t*) * 4)) @@ -227,8 +226,7 @@ __contract__( * Generate a single A matrix entry from a seed, using rejection * sampling on the output of a XOF. */ -STATIC_TESTABLE -void gen_matrix_entry(poly *entry, uint8_t seed[MLKEM_SYMBYTES + 2]) +static void gen_matrix_entry(poly *entry, uint8_t seed[MLKEM_SYMBYTES + 2]) __contract__( requires(memory_no_alias(entry, sizeof(poly))) requires(memory_no_alias(seed, MLKEM_SYMBYTES + 2)) @@ -270,8 +268,7 @@ __contract__( #define poly_permute_bitrev_to_custom \ MLKEM_NAMESPACE(poly_permute_bitrev_to_custom) -STATIC_INLINE_TESTABLE -void poly_permute_bitrev_to_custom(poly *data) +static INLINE void poly_permute_bitrev_to_custom(poly *data) __contract__( /* We don't specify that this should be a permutation, but only * that it does not change the bound established at the end of gen_matrix. */ @@ -386,9 +383,8 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed) * - polyvec *vc: Mulcache for v, computed via * polyvec_mulcache_compute(). **************************************************/ -STATIC_TESTABLE -void matvec_mul(polyvec *out, const polyvec a[MLKEM_K], const polyvec *v, - const polyvec_mulcache *vc) +static void matvec_mul(polyvec *out, const polyvec a[MLKEM_K], const polyvec *v, + const polyvec_mulcache *vc) __contract__( requires(memory_no_alias(out, sizeof(polyvec))) requires(memory_no_alias(a, sizeof(polyvec) * MLKEM_K)) diff --git a/mlkem/ntt.c b/mlkem/ntt.c index 93f3cdba2..83c8b2d3f 100644 --- a/mlkem/ntt.c +++ b/mlkem/ntt.c @@ -45,9 +45,8 @@ * 4 -- 6 * 5 -- 7 */ -STATIC_TESTABLE -void ntt_butterfly_block(int16_t r[MLKEM_N], int16_t zeta, int start, int len, - int bound) +static void ntt_butterfly_block(int16_t r[MLKEM_N], int16_t zeta, int start, + int len, int bound) __contract__( requires(0 <= start && start < MLKEM_N) requires(1 <= len && len <= MLKEM_N / 2 && start + 2 * len <= MLKEM_N) @@ -94,8 +93,7 @@ __contract__( * official Kyber implementation here, merely adding `layer` as * a ghost variable for the specifications. */ -STATIC_TESTABLE -void ntt_layer(int16_t r[MLKEM_N], int len, int layer) +static void ntt_layer(int16_t r[MLKEM_N], int len, int layer) __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(1 <= layer && layer <= 7 && len == (MLKEM_N >> layer)) @@ -167,8 +165,7 @@ void poly_ntt(poly *p) STATIC_ASSERT(INVNTT_BOUND_REF <= INVNTT_BOUND, invntt_bound) /* Compute one layer of inverse NTT */ -STATIC_TESTABLE -void invntt_layer(int16_t *r, int len, int layer) +static void invntt_layer(int16_t *r, int len, int layer) __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(2 <= len && len <= 128 && 1 <= layer && layer <= 7) diff --git a/mlkem/reduce.h b/mlkem/reduce.h index ec98c209f..ddbea6be5 100644 --- a/mlkem/reduce.h +++ b/mlkem/reduce.h @@ -107,8 +107,7 @@ static INLINE int16_t montgomery_reduce_generic(int32_t a) * Returns: integer congruent to a * R^-1 modulo q, * smaller than 2 * q in absolute value. **************************************************/ -STATIC_INLINE_TESTABLE -int16_t montgomery_reduce(int32_t a) +static INLINE int16_t montgomery_reduce(int32_t a) __contract__( requires(a > -(2 * 4096 * 32768)) requires(a < (2 * 4096 * 32768)) @@ -143,8 +142,7 @@ __contract__( * smaller than q in absolute value. * **************************************************/ -STATIC_INLINE_TESTABLE -int16_t fqmul(int16_t a, int16_t b) +static INLINE int16_t fqmul(int16_t a, int16_t b) __contract__( requires(b > -HALF_Q) requires(b < HALF_Q) @@ -177,8 +175,7 @@ __contract__( * * Returns: integer in {-(q-1)/2,...,(q-1)/2} congruent to a modulo q. **************************************************/ -STATIC_INLINE_TESTABLE -int16_t barrett_reduce(int16_t a) +static INLINE int16_t barrett_reduce(int16_t a) __contract__( ensures(return_value > -HALF_Q && return_value < HALF_Q) ) diff --git a/mlkem/rej_uniform.c b/mlkem/rej_uniform.c index 372196d74..88c98be25 100644 --- a/mlkem/rej_uniform.c +++ b/mlkem/rej_uniform.c @@ -42,10 +42,9 @@ * is guaranteed to have been consumed. If it is equal to len, no information * is provided on how many bytes of the input buffer have been consumed. **************************************************/ -STATIC_TESTABLE -unsigned int rej_uniform_scalar(int16_t *r, unsigned int target, - unsigned int offset, const uint8_t *buf, - unsigned int buflen) +static unsigned int rej_uniform_scalar(int16_t *r, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen) __contract__( requires(offset <= target && target <= 4096 && buflen <= 4096 && buflen % 3 == 0) requires(memory_no_alias(r, sizeof(int16_t) * target)) diff --git a/mlkem/verify.h b/mlkem/verify.h index ba17d8788..126eeb279 100644 --- a/mlkem/verify.h +++ b/mlkem/verify.h @@ -74,41 +74,41 @@ extern volatile uint64_t ct_opt_blocker_u64; /* Helper functions for obtaining masks of various sizes */ -STATIC_INLINE_TESTABLE uint8_t get_optblocker_u8(void) +static INLINE uint8_t get_optblocker_u8(void) __contract__(ensures(return_value == 0)) { return (uint8_t)ct_opt_blocker_u64; } -STATIC_INLINE_TESTABLE uint32_t get_optblocker_u32(void) +static INLINE uint32_t get_optblocker_u32(void) __contract__(ensures(return_value == 0)) { return ct_opt_blocker_u64; } -STATIC_INLINE_TESTABLE uint32_t get_optblocker_i32(void) +static INLINE uint32_t get_optblocker_i32(void) __contract__(ensures(return_value == 0)) { return ct_opt_blocker_u64; } -STATIC_INLINE_TESTABLE uint32_t value_barrier_u32(uint32_t b) +static INLINE uint32_t value_barrier_u32(uint32_t b) __contract__(ensures(return_value == b)) { return (b ^ get_optblocker_u32()); } -STATIC_INLINE_TESTABLE int32_t value_barrier_i32(int32_t b) +static INLINE int32_t value_barrier_i32(int32_t b) __contract__(ensures(return_value == b)) { return (b ^ get_optblocker_i32()); } -STATIC_INLINE_TESTABLE uint8_t value_barrier_u8(uint8_t b) +static INLINE uint8_t value_barrier_u8(uint8_t b) __contract__(ensures(return_value == b)) { return (b ^ get_optblocker_u8()); } #else /* !MLKEM_USE_ASM_VALUE_BARRIER */ -STATIC_INLINE_TESTABLE uint32_t value_barrier_u32(uint32_t b) +static INLINE uint32_t value_barrier_u32(uint32_t b) __contract__(ensures(return_value == b)) { asm("" : "+r"(b)); return b; } -STATIC_INLINE_TESTABLE int32_t value_barrier_i32(int32_t b) +static INLINE int32_t value_barrier_i32(int32_t b) __contract__(ensures(return_value == b)) { asm("" : "+r"(b)); return b; } -STATIC_INLINE_TESTABLE uint8_t value_barrier_u8(uint8_t b) +static INLINE uint8_t value_barrier_u8(uint8_t b) __contract__(ensures(return_value == b)) { asm("" : "+r"(b)); @@ -134,7 +134,7 @@ __contract__(ensures(return_value == b)) * * Arguments: uint16_t x: Value to be converted into a mask **************************************************/ -STATIC_INLINE_TESTABLE uint16_t ct_cmask_nonzero_u16(uint16_t x) +static INLINE uint16_t ct_cmask_nonzero_u16(uint16_t x) __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFFFF))) { uint32_t tmp = value_barrier_u32(-((uint32_t)x)); @@ -149,7 +149,7 @@ __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFFFF))) * * Arguments: uint8_t x: Value to be converted into a mask **************************************************/ -STATIC_INLINE_TESTABLE uint8_t ct_cmask_nonzero_u8(uint8_t x) +static INLINE uint8_t ct_cmask_nonzero_u8(uint8_t x) __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFF))) { uint32_t tmp = value_barrier_u32(-((uint32_t)x)); @@ -179,7 +179,7 @@ __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFF))) * * Arguments: uint16_t x: Value to be converted into a mask **************************************************/ -STATIC_INLINE_TESTABLE uint16_t ct_cmask_neg_i16(int16_t x) +static INLINE uint16_t ct_cmask_neg_i16(int16_t x) __contract__(ensures(return_value == ((x < 0) ? 0xFFFF : 0))) { int32_t tmp = value_barrier_i32((int32_t)x); @@ -214,7 +214,7 @@ __contract__(ensures(return_value == ((x < 0) ? 0xFFFF : 0))) * int16_t b: Second alternative * uint16_t cond: Condition variable. **************************************************/ -STATIC_INLINE_TESTABLE int16_t ct_sel_int16(int16_t a, int16_t b, uint16_t cond) +static INLINE int16_t ct_sel_int16(int16_t a, int16_t b, uint16_t cond) __contract__(ensures(return_value == (cond ? a : b))) { uint16_t au = a, bu = b; @@ -238,7 +238,7 @@ __contract__(ensures(return_value == (cond ? a : b))) * uint8_t b: Second alternative * uuint8_t cond: Condition variable. **************************************************/ -STATIC_INLINE_TESTABLE uint8_t ct_sel_uint8(uint8_t a, uint8_t b, uint8_t cond) +static INLINE uint8_t ct_sel_uint8(uint8_t a, uint8_t b, uint8_t cond) __contract__(ensures(return_value == (cond ? a : b))) { return b ^ (ct_cmask_nonzero_u8(cond) & (a ^ b)); @@ -255,8 +255,8 @@ __contract__(ensures(return_value == (cond ? a : b))) * * Returns 0 if the byte arrays are equal, a non-zero value otherwise **************************************************/ -STATIC_INLINE_TESTABLE uint8_t ct_memcmp(const uint8_t *a, const uint8_t *b, - const size_t len) +static INLINE uint8_t ct_memcmp(const uint8_t *a, const uint8_t *b, + const size_t len) __contract__( requires(memory_no_alias(a, len)) requires(memory_no_alias(b, len)) @@ -306,8 +306,8 @@ __contract__( * size_t len: Amount of bytes to be copied * uint8_t b: Condition value. **************************************************/ -STATIC_INLINE_TESTABLE -void ct_cmov_zero(uint8_t *r, const uint8_t *x, size_t len, uint8_t b) +static INLINE void ct_cmov_zero(uint8_t *r, const uint8_t *x, size_t len, + uint8_t b) __contract__( requires(memory_no_alias(r, len)) requires(memory_no_alias(x, len))