Skip to content

Reintroduce struct definitions for mlk_poly{mat,vec} #1263

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Reintroduce struct definitions for mlk_poly{mat,vec} #1263

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
193 changes: 115 additions & 78 deletions mlkem/src/indcpa.c
View file
Open in desktop

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions mlkem/src/indcpa.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,15 +39,15 @@
*
**************************************************/
MLK_INTERNAL_API
void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES],
void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES],
int transposed)
__contract__(
requires(memory_no_alias(a, sizeof(mlk_polymat)))
requires(memory_no_alias(seed, MLKEM_SYMBYTES))
requires(transposed == 0 || transposed == 1)
assigns(object_whole(a))
ensures(forall(x, 0, MLKEM_K * MLKEM_K,
array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
);

#define mlk_indcpa_keypair_derand MLK_NAMESPACE_K(indcpa_keypair_derand)
Expand Down
6 changes: 3 additions & 3 deletions mlkem/src/kem.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,9 @@ int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
mlk_polyvec p;
uint8_t p_reencoded[MLKEM_POLYVECBYTES];

mlk_polyvec_frombytes(p, pk);
mlk_polyvec_reduce(p);
mlk_polyvec_tobytes(p_reencoded, p);
mlk_polyvec_frombytes(&p, pk);
mlk_polyvec_reduce(&p);
mlk_polyvec_tobytes(p_reencoded, &p);

/* We use a constant-time memcmp here to avoid having to
* declassify the PK before the PCT has succeeded. */
Expand Down
76 changes: 38 additions & 38 deletions mlkem/src/poly_k.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,29 +47,29 @@
* in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
MLK_INTERNAL_API
void mlk_polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU],
const mlk_polyvec a)
const mlk_polyvec *a)
{
unsigned i;
mlk_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q);

for (i = 0; i < MLKEM_K; i++)
{
mlk_poly_compress_du(r + i * MLKEM_POLYCOMPRESSEDBYTES_DU, &a[i]);
mlk_poly_compress_du(r + i * MLKEM_POLYCOMPRESSEDBYTES_DU, &a->vec[i]);
}
}

/* Reference: `polyvec_decompress()` in the reference implementation @[REF]. */
MLK_INTERNAL_API
void mlk_polyvec_decompress_du(mlk_polyvec r,
void mlk_polyvec_decompress_du(mlk_polyvec *r,
const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES_DU])
{
unsigned i;
for (i = 0; i < MLKEM_K; i++)
{
mlk_poly_decompress_du(&r[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU);
mlk_poly_decompress_du(&r->vec[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU);
}

mlk_assert_bound_2d(r, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
}

/* Reference: `polyvec_tobytes()` in the reference implementation @[REF].
Expand All @@ -78,45 +78,45 @@ void mlk_polyvec_decompress_du(mlk_polyvec r,
* The reference implementation works with coefficients
* in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
MLK_INTERNAL_API
void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec a)
void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec *a)
{
unsigned i;
mlk_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q);

for (i = 0; i < MLKEM_K; i++)
__loop__(
assigns(i, object_whole(r))
invariant(i <= MLKEM_K)
)
{
mlk_poly_tobytes(&r[i * MLKEM_POLYBYTES], &a[i]);
mlk_poly_tobytes(&r[i * MLKEM_POLYBYTES], &a->vec[i]);
}
}

/* Reference: `polyvec_frombytes()` in the reference implementation @[REF]. */
MLK_INTERNAL_API
void mlk_polyvec_frombytes(mlk_polyvec r, const uint8_t a[MLKEM_POLYVECBYTES])
void mlk_polyvec_frombytes(mlk_polyvec *r, const uint8_t a[MLKEM_POLYVECBYTES])
{
unsigned i;
for (i = 0; i < MLKEM_K; i++)
{
mlk_poly_frombytes(&r[i], a + i * MLKEM_POLYBYTES);
mlk_poly_frombytes(&r->vec[i], a + i * MLKEM_POLYBYTES);
}

mlk_assert_bound_2d(r, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT);
mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT);
}

/* Reference: `polyvec_ntt()` in the reference implementation @[REF]. */
MLK_INTERNAL_API
void mlk_polyvec_ntt(mlk_polyvec r)
void mlk_polyvec_ntt(mlk_polyvec *r)
{
unsigned i;
for (i = 0; i < MLKEM_K; i++)
{
mlk_poly_ntt(&r[i]);
mlk_poly_ntt(&r->vec[i]);
}

mlk_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, MLK_NTT_BOUND);
mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLK_NTT_BOUND);
}

/* Reference: `polyvec_invntt_tomont()` in the reference implementation @[REF].
Expand All @@ -125,15 +125,15 @@ void mlk_polyvec_ntt(mlk_polyvec r)
* the end. This allows us to drop a call to `poly_reduce()`
* from the base multiplication. */
MLK_INTERNAL_API
void mlk_polyvec_invntt_tomont(mlk_polyvec r)
void mlk_polyvec_invntt_tomont(mlk_polyvec *r)
{
unsigned i;
for (i = 0; i < MLKEM_K; i++)
{
mlk_poly_invntt_tomont(&r[i]);
mlk_poly_invntt_tomont(&r->vec[i]);
}

mlk_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, MLK_INVNTT_BOUND);
mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLK_INVNTT_BOUND);
}

/* Reference: `polyvec_basemul_acc_montgomery()` in the
Expand All @@ -148,20 +148,20 @@ void mlk_polyvec_invntt_tomont(mlk_polyvec r)
* more modular reductions since it reduces after every modular
* multiplication. */
MLK_STATIC_TESTABLE void mlk_polyvec_basemul_acc_montgomery_cached_c(
mlk_poly *r, const mlk_polyvec a, const mlk_polyvec b,
const mlk_polyvec_mulcache b_cache)
mlk_poly *r, const mlk_polyvec *a, const mlk_polyvec *b,
const mlk_polyvec_mulcache *b_cache)
__contract__(
requires(memory_no_alias(r, sizeof(mlk_poly)))
requires(memory_no_alias(a, sizeof(mlk_polyvec)))
requires(memory_no_alias(b, sizeof(mlk_polyvec)))
requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache)))
requires(forall(k1, 0, MLKEM_K,
array_bound(a[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
assigns(object_whole(r))
)
{
unsigned i;
mlk_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT);
mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT);

for (i = 0; i < MLKEM_N / 2; i++)
__loop__(invariant(i <= MLKEM_N / 2))
Expand All @@ -176,10 +176,10 @@ __contract__(
t[1] <= ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) &&
t[1] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768)))
{
t[0] += (int32_t)a[k].coeffs[2 * i + 1] * b_cache[k].coeffs[i];
t[0] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i];
t[1] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i + 1];
t[1] += (int32_t)a[k].coeffs[2 * i + 1] * b[k].coeffs[2 * i];
t[0] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i];
t[0] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i];
t[1] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i + 1];
t[1] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b->vec[k].coeffs[2 * i];
}
r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]);
r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]);
Expand All @@ -188,8 +188,8 @@ __contract__(

MLK_INTERNAL_API
void mlk_polyvec_basemul_acc_montgomery_cached(
mlk_poly *r, const mlk_polyvec a, const mlk_polyvec b,
const mlk_polyvec_mulcache b_cache)
mlk_poly *r, const mlk_polyvec *a, const mlk_polyvec *b,
const mlk_polyvec_mulcache *b_cache)
{
#if defined(MLK_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED)
{
Expand Down Expand Up @@ -225,12 +225,12 @@ void mlk_polyvec_basemul_acc_montgomery_cached(
* multiplication cache ('mulcache'). This idea originates
* from @[NeonNTT] and is used at the C level here. */
MLK_INTERNAL_API
void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache x, const mlk_polyvec a)
void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache *x, const mlk_polyvec *a)
{
unsigned i;
for (i = 0; i < MLKEM_K; i++)
{
mlk_poly_mulcache_compute(&x[i], &a[i]);
mlk_poly_mulcache_compute(&x->vec[i], &a->vec[i]);
}
}

Expand All @@ -242,41 +242,41 @@ void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache x, const mlk_polyvec a)
* This conditional addition is then dropped from all
* polynomial compression functions instead (see `compress.c`). */
MLK_INTERNAL_API
void mlk_polyvec_reduce(mlk_polyvec r)
void mlk_polyvec_reduce(mlk_polyvec *r)
{
unsigned i;
for (i = 0; i < MLKEM_K; i++)
{
mlk_poly_reduce(&r[i]);
mlk_poly_reduce(&r->vec[i]);
}

mlk_assert_bound_2d(r, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
}

/* Reference: `polyvec_add()` in the reference implementation @[REF].
* - We use destructive version (output=first input) to avoid
* reasoning about aliasing in the CBMC specification */
MLK_INTERNAL_API
void mlk_polyvec_add(mlk_polyvec r, const mlk_polyvec b)
void mlk_polyvec_add(mlk_polyvec *r, const mlk_polyvec *b)
{
unsigned i;
for (i = 0; i < MLKEM_K; i++)
{
mlk_poly_add(&r[i], &b[i]);
mlk_poly_add(&r->vec[i], &b->vec[i]);
}
}

/* Reference: `polyvec_tomont()` in the reference implementation @[REF]. */
MLK_INTERNAL_API
void mlk_polyvec_tomont(mlk_polyvec r)
void mlk_polyvec_tomont(mlk_polyvec *r)
{
unsigned i;
for (i = 0; i < MLKEM_K; i++)
{
mlk_poly_tomont(&r[i]);
mlk_poly_tomont(&r->vec[i]);
}

mlk_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, MLKEM_Q);
mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLKEM_Q);
}


Expand Down
Loading