#ifndef MLD_FIPS202_FIPS202_H
#define MLD_FIPS202_FIPS202_H
#include <stddef.h>
#include "../cbmc.h"
#include "../common.h"
#define SHAKE128_RATE 168
#define SHAKE256_RATE 136
#define SHA3_256_RATE 136
#define SHA3_512_RATE 72
#define MLD_KECCAK_LANES 25
#define SHA3_256_HASHBYTES 32
#define SHA3_512_HASHBYTES 64
typedef struct
{
uint64_t s[MLD_KECCAK_LANES];
unsigned int pos;
} mld_shake128ctx;
typedef struct
{
uint64_t s[MLD_KECCAK_LANES];
unsigned int pos;
} mld_shake256ctx;
#define mld_shake128_init MLD_NAMESPACE(shake128_init)
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)))
ensures(state->pos == 0)
);
#define mld_shake128_absorb MLD_NAMESPACE(shake128_absorb)
MLD_INTERNAL_API
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(state->pos <= SHAKE128_RATE)
assigns(memory_slice(state, sizeof(mld_shake128ctx)))
ensures(state->pos <= SHAKE128_RATE)
);
#define mld_shake128_finalize MLD_NAMESPACE(shake128_finalize)
MLD_INTERNAL_API
void mld_shake128_finalize(mld_shake128ctx *state)
__contract__(
requires(memory_no_alias(state, sizeof(mld_shake128ctx)))
requires(state->pos <= SHAKE128_RATE)
assigns(memory_slice(state, sizeof(mld_shake128ctx)))
ensures(state->pos <= SHAKE128_RATE)
);
#define mld_shake128_squeeze MLD_NAMESPACE(shake128_squeeze)
MLD_INTERNAL_API
void mld_shake128_squeeze(uint8_t *out, size_t outlen, mld_shake128ctx *state)
__contract__(
requires(outlen <= 8 * SHAKE128_RATE )
requires(memory_no_alias(state, sizeof(mld_shake128ctx)))
requires(memory_no_alias(out, outlen))
requires(state->pos <= SHAKE128_RATE)
assigns(memory_slice(state, sizeof(mld_shake128ctx)))
assigns(memory_slice(out, outlen))
ensures(state->pos <= SHAKE128_RATE)
);
#define mld_shake128_release MLD_NAMESPACE(shake128_release)
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)))
);
#define mld_shake256_init MLD_NAMESPACE(shake256_init)
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)))
ensures(state->pos == 0)
);
#define mld_shake256_absorb MLD_NAMESPACE(shake256_absorb)
MLD_INTERNAL_API
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(state->pos <= SHAKE256_RATE)
assigns(memory_slice(state, sizeof(mld_shake256ctx)))
ensures(state->pos <= SHAKE256_RATE)
);
#define mld_shake256_finalize MLD_NAMESPACE(shake256_finalize)
MLD_INTERNAL_API
void mld_shake256_finalize(mld_shake256ctx *state)
__contract__(
requires(memory_no_alias(state, sizeof(mld_shake256ctx)))
requires(state->pos <= SHAKE256_RATE)
assigns(memory_slice(state, sizeof(mld_shake256ctx)))
ensures(state->pos <= SHAKE256_RATE)
);
#define mld_shake256_squeeze MLD_NAMESPACE(shake256_squeeze)
MLD_INTERNAL_API
void mld_shake256_squeeze(uint8_t *out, size_t outlen, mld_shake256ctx *state)
__contract__(
requires(outlen <= 8 * SHAKE256_RATE )
requires(memory_no_alias(state, sizeof(mld_shake256ctx)))
requires(memory_no_alias(out, outlen))
requires(state->pos <= SHAKE256_RATE)
assigns(memory_slice(state, sizeof(mld_shake256ctx)))
assigns(memory_slice(out, outlen))
ensures(state->pos <= SHAKE256_RATE)
);
#define mld_shake256_release MLD_NAMESPACE(shake256_release)
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)))
);
#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_CORE_API_ONLY)
#define mld_shake256 MLD_NAMESPACE(shake256)
MLD_INTERNAL_API
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 )
requires(memory_no_alias(in, inlen))
requires(memory_no_alias(out, outlen))
assigns(memory_slice(out, outlen))
);
#endif
#endif