#include <stddef.h>
#include "../common.h"
#include "../ct.h"
#include "fips202.h"
#include "keccakf1600.h"
#if !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
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))
)
{
mld_memset(s, 0, sizeof(uint64_t) * MLD_KECCAK_LANES);
}
static unsigned int keccak_absorb(uint64_t s[MLD_KECCAK_LANES],
unsigned int pos, unsigned int r,
const uint8_t *in, size_t inlen)
__contract__(
requires(inlen <= MLD_MAX_BUFFER_SIZE)
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))
ensures(return_value < r))
{
while (inlen >= r - pos)
__loop__(
assigns(pos, in, inlen,
memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
invariant(inlen <= loop_entry(inlen))
invariant(pos <= r)
invariant(in == loop_entry(in) + (loop_entry(inlen) - inlen))
decreases(inlen + pos))
{
mld_keccakf1600_xor_bytes(s, in, pos, r - pos);
inlen -= r - pos;
in += r - pos;
mld_keccakf1600_permute(s);
pos = 0;
}
mld_keccakf1600_xor_bytes(s, in, pos, (unsigned)inlen);
return (unsigned)(pos + inlen);
}
static void keccak_finalize(uint64_t s[MLD_KECCAK_LANES], unsigned int pos,
unsigned int r, uint8_t p)
__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))
)
{
uint8_t b = 0x80;
mld_keccakf1600_xor_bytes(s, &p, pos, 1);
mld_keccakf1600_xor_bytes(s, &b, r - 1, 1);
}
static unsigned int keccak_squeeze(uint8_t *out, size_t outlen,
uint64_t s[MLD_KECCAK_LANES],
unsigned int pos, unsigned int r)
__contract__(
requires((r == SHAKE128_RATE && pos <= SHAKE128_RATE) ||
(r == SHAKE256_RATE && pos <= SHAKE256_RATE) ||
(r == SHA3_512_RATE && pos <= SHA3_512_RATE))
requires(outlen <= 8 * r )
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))
ensures(return_value <= r))
{
unsigned int i;
size_t out_offset = 0;
size_t bytes_to_go = outlen;
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))
invariant(bytes_to_go <= outlen)
invariant(out_offset == outlen - bytes_to_go)
invariant(pos <= r)
decreases(bytes_to_go)
)
{
if (pos == r)
{
mld_keccakf1600_permute(s);
pos = 0;
}
i = bytes_to_go < r - pos ? (unsigned)bytes_to_go : r - pos;
mld_keccakf1600_extract_bytes(s, out + out_offset, pos, i);
bytes_to_go -= i;
pos += i;
out_offset += i;
}
return pos;
}
MLD_INTERNAL_API
void mld_shake128_init(mld_shake128ctx *state)
{
keccak_init(state->s);
state->pos = 0;
}
MLD_INTERNAL_API
void mld_shake128_absorb(mld_shake128ctx *state, const uint8_t *in,
size_t inlen)
{
state->pos = keccak_absorb(state->s, state->pos, SHAKE128_RATE, in, inlen);
}
MLD_INTERNAL_API
void mld_shake128_finalize(mld_shake128ctx *state)
{
keccak_finalize(state->s, state->pos, SHAKE128_RATE, 0x1F);
state->pos = SHAKE128_RATE;
}
MLD_INTERNAL_API
void mld_shake128_squeeze(uint8_t *out, size_t outlen, mld_shake128ctx *state)
{
state->pos = keccak_squeeze(out, outlen, state->s, state->pos, SHAKE128_RATE);
}
MLD_INTERNAL_API
void mld_shake128_release(mld_shake128ctx *state)
{
mld_zeroize(state, sizeof(mld_shake128ctx));
}
MLD_INTERNAL_API
void mld_shake256_init(mld_shake256ctx *state)
{
keccak_init(state->s);
state->pos = 0;
}
MLD_INTERNAL_API
void mld_shake256_absorb(mld_shake256ctx *state, const uint8_t *in,
size_t inlen)
{
state->pos = keccak_absorb(state->s, state->pos, SHAKE256_RATE, in, inlen);
}
MLD_INTERNAL_API
void mld_shake256_finalize(mld_shake256ctx *state)
{
keccak_finalize(state->s, state->pos, SHAKE256_RATE, 0x1F);
state->pos = SHAKE256_RATE;
}
MLD_INTERNAL_API
void mld_shake256_squeeze(uint8_t *out, size_t outlen, mld_shake256ctx *state)
{
state->pos = keccak_squeeze(out, outlen, state->s, state->pos, SHAKE256_RATE);
}
MLD_INTERNAL_API
void mld_shake256_release(mld_shake256ctx *state)
{
mld_zeroize(state, sizeof(mld_shake256ctx));
}
#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_CORE_API_ONLY)
MLD_INTERNAL_API
void mld_shake256(uint8_t *out, size_t outlen, const uint8_t *in, size_t inlen)
{
mld_shake256ctx state;
mld_shake256_init(&state);
mld_shake256_absorb(&state, in, inlen);
mld_shake256_finalize(&state);
mld_shake256_squeeze(out, outlen, &state);
mld_shake256_release(&state);
}
#endif
#endif