#include "Hacl_Chacha20_Vec32.h"
inline static void Hacl_Chacha20_Vec32_double_round_32(uint32_t *st)
{
uint32_t std0;
uint32_t std1;
uint32_t std2;
uint32_t std3;
uint32_t std4;
uint32_t std5;
uint32_t std6;
uint32_t std7;
uint32_t std8;
uint32_t std9;
uint32_t std10;
uint32_t std11;
uint32_t std12;
uint32_t std13;
uint32_t std14;
uint32_t std15;
uint32_t std16;
uint32_t std17;
uint32_t std18;
uint32_t std19;
uint32_t std20;
uint32_t std21;
uint32_t std22;
uint32_t std23;
uint32_t std24;
uint32_t std25;
uint32_t std26;
uint32_t std27;
uint32_t std28;
uint32_t std29;
uint32_t std30;
uint32_t std;
st[0U] = st[0U] + st[4U];
std0 = st[12U] ^ st[0U];
st[12U] = std0 << (uint32_t)16U | std0 >> ((uint32_t)32U - (uint32_t)16U);
st[8U] = st[8U] + st[12U];
std1 = st[4U] ^ st[8U];
st[4U] = std1 << (uint32_t)12U | std1 >> ((uint32_t)32U - (uint32_t)12U);
st[0U] = st[0U] + st[4U];
std2 = st[12U] ^ st[0U];
st[12U] = std2 << (uint32_t)8U | std2 >> ((uint32_t)32U - (uint32_t)8U);
st[8U] = st[8U] + st[12U];
std3 = st[4U] ^ st[8U];
st[4U] = std3 << (uint32_t)7U | std3 >> ((uint32_t)32U - (uint32_t)7U);
st[1U] = st[1U] + st[5U];
std4 = st[13U] ^ st[1U];
st[13U] = std4 << (uint32_t)16U | std4 >> ((uint32_t)32U - (uint32_t)16U);
st[9U] = st[9U] + st[13U];
std5 = st[5U] ^ st[9U];
st[5U] = std5 << (uint32_t)12U | std5 >> ((uint32_t)32U - (uint32_t)12U);
st[1U] = st[1U] + st[5U];
std6 = st[13U] ^ st[1U];
st[13U] = std6 << (uint32_t)8U | std6 >> ((uint32_t)32U - (uint32_t)8U);
st[9U] = st[9U] + st[13U];
std7 = st[5U] ^ st[9U];
st[5U] = std7 << (uint32_t)7U | std7 >> ((uint32_t)32U - (uint32_t)7U);
st[2U] = st[2U] + st[6U];
std8 = st[14U] ^ st[2U];
st[14U] = std8 << (uint32_t)16U | std8 >> ((uint32_t)32U - (uint32_t)16U);
st[10U] = st[10U] + st[14U];
std9 = st[6U] ^ st[10U];
st[6U] = std9 << (uint32_t)12U | std9 >> ((uint32_t)32U - (uint32_t)12U);
st[2U] = st[2U] + st[6U];
std10 = st[14U] ^ st[2U];
st[14U] = std10 << (uint32_t)8U | std10 >> ((uint32_t)32U - (uint32_t)8U);
st[10U] = st[10U] + st[14U];
std11 = st[6U] ^ st[10U];
st[6U] = std11 << (uint32_t)7U | std11 >> ((uint32_t)32U - (uint32_t)7U);
st[3U] = st[3U] + st[7U];
std12 = st[15U] ^ st[3U];
st[15U] = std12 << (uint32_t)16U | std12 >> ((uint32_t)32U - (uint32_t)16U);
st[11U] = st[11U] + st[15U];
std13 = st[7U] ^ st[11U];
st[7U] = std13 << (uint32_t)12U | std13 >> ((uint32_t)32U - (uint32_t)12U);
st[3U] = st[3U] + st[7U];
std14 = st[15U] ^ st[3U];
st[15U] = std14 << (uint32_t)8U | std14 >> ((uint32_t)32U - (uint32_t)8U);
st[11U] = st[11U] + st[15U];
std15 = st[7U] ^ st[11U];
st[7U] = std15 << (uint32_t)7U | std15 >> ((uint32_t)32U - (uint32_t)7U);
st[0U] = st[0U] + st[5U];
std16 = st[15U] ^ st[0U];
st[15U] = std16 << (uint32_t)16U | std16 >> ((uint32_t)32U - (uint32_t)16U);
st[10U] = st[10U] + st[15U];
std17 = st[5U] ^ st[10U];
st[5U] = std17 << (uint32_t)12U | std17 >> ((uint32_t)32U - (uint32_t)12U);
st[0U] = st[0U] + st[5U];
std18 = st[15U] ^ st[0U];
st[15U] = std18 << (uint32_t)8U | std18 >> ((uint32_t)32U - (uint32_t)8U);
st[10U] = st[10U] + st[15U];
std19 = st[5U] ^ st[10U];
st[5U] = std19 << (uint32_t)7U | std19 >> ((uint32_t)32U - (uint32_t)7U);
st[1U] = st[1U] + st[6U];
std20 = st[12U] ^ st[1U];
st[12U] = std20 << (uint32_t)16U | std20 >> ((uint32_t)32U - (uint32_t)16U);
st[11U] = st[11U] + st[12U];
std21 = st[6U] ^ st[11U];
st[6U] = std21 << (uint32_t)12U | std21 >> ((uint32_t)32U - (uint32_t)12U);
st[1U] = st[1U] + st[6U];
std22 = st[12U] ^ st[1U];
st[12U] = std22 << (uint32_t)8U | std22 >> ((uint32_t)32U - (uint32_t)8U);
st[11U] = st[11U] + st[12U];
std23 = st[6U] ^ st[11U];
st[6U] = std23 << (uint32_t)7U | std23 >> ((uint32_t)32U - (uint32_t)7U);
st[2U] = st[2U] + st[7U];
std24 = st[13U] ^ st[2U];
st[13U] = std24 << (uint32_t)16U | std24 >> ((uint32_t)32U - (uint32_t)16U);
st[8U] = st[8U] + st[13U];
std25 = st[7U] ^ st[8U];
st[7U] = std25 << (uint32_t)12U | std25 >> ((uint32_t)32U - (uint32_t)12U);
st[2U] = st[2U] + st[7U];
std26 = st[13U] ^ st[2U];
st[13U] = std26 << (uint32_t)8U | std26 >> ((uint32_t)32U - (uint32_t)8U);
st[8U] = st[8U] + st[13U];
std27 = st[7U] ^ st[8U];
st[7U] = std27 << (uint32_t)7U | std27 >> ((uint32_t)32U - (uint32_t)7U);
st[3U] = st[3U] + st[4U];
std28 = st[14U] ^ st[3U];
st[14U] = std28 << (uint32_t)16U | std28 >> ((uint32_t)32U - (uint32_t)16U);
st[9U] = st[9U] + st[14U];
std29 = st[4U] ^ st[9U];
st[4U] = std29 << (uint32_t)12U | std29 >> ((uint32_t)32U - (uint32_t)12U);
st[3U] = st[3U] + st[4U];
std30 = st[14U] ^ st[3U];
st[14U] = std30 << (uint32_t)8U | std30 >> ((uint32_t)32U - (uint32_t)8U);
st[9U] = st[9U] + st[14U];
std = st[4U] ^ st[9U];
st[4U] = std << (uint32_t)7U | std >> ((uint32_t)32U - (uint32_t)7U);
}
inline static void
Hacl_Chacha20_Vec32_chacha20_core_32(uint32_t *k, uint32_t *ctx, uint32_t ctr)
{
uint32_t ctr_u32;
uint32_t cv;
memcpy(k, ctx, (uint32_t)16U * sizeof ctx[0U]);
ctr_u32 = (uint32_t)1U * ctr;
cv = ctr_u32;
k[12U] = k[12U] + cv;
Hacl_Chacha20_Vec32_double_round_32(k);
Hacl_Chacha20_Vec32_double_round_32(k);
Hacl_Chacha20_Vec32_double_round_32(k);
Hacl_Chacha20_Vec32_double_round_32(k);
Hacl_Chacha20_Vec32_double_round_32(k);
Hacl_Chacha20_Vec32_double_round_32(k);
Hacl_Chacha20_Vec32_double_round_32(k);
Hacl_Chacha20_Vec32_double_round_32(k);
Hacl_Chacha20_Vec32_double_round_32(k);
Hacl_Chacha20_Vec32_double_round_32(k);
{
uint32_t i;
for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U)
{
uint32_t *os = k;
uint32_t x = k[i] + ctx[i];
os[i] = x;
}
}
k[12U] = k[12U] + cv;
}
inline static void
Hacl_Chacha20_Vec32_chacha20_init_32(uint32_t *ctx, uint8_t *k, uint8_t *n1, uint32_t ctr)
{
uint32_t ctx1[16U] = { 0U };
uint32_t *uu____0 = ctx1;
uint32_t *uu____1;
uint32_t *uu____2;
uint32_t ctr1;
uint32_t c12;
{
uint32_t i;
for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U)
{
uint32_t *os = uu____0;
uint32_t x = Hacl_Impl_Chacha20_Vec_chacha20_constants[i];
os[i] = x;
}
}
uu____1 = ctx1 + (uint32_t)4U;
{
uint32_t i;
for (i = (uint32_t)0U; i < (uint32_t)8U; i = i + (uint32_t)1U)
{
uint32_t *os = uu____1;
uint8_t *bj = k + i * (uint32_t)4U;
uint32_t u = load32_le(bj);
uint32_t r = u;
uint32_t x = r;
os[i] = x;
}
}
ctx1[12U] = ctr;
uu____2 = ctx1 + (uint32_t)13U;
{
uint32_t i;
for (i = (uint32_t)0U; i < (uint32_t)3U; i = i + (uint32_t)1U)
{
uint32_t *os = uu____2;
uint8_t *bj = n1 + i * (uint32_t)4U;
uint32_t u = load32_le(bj);
uint32_t r = u;
uint32_t x = r;
os[i] = x;
}
}
{
uint32_t i;
for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U)
{
uint32_t *os = ctx;
uint32_t x = ctx1[i];
os[i] = x;
}
}
ctr1 = (uint32_t)0U;
c12 = ctx[12U];
ctx[12U] = c12 + ctr1;
}
void
Hacl_Chacha20_Vec32_chacha20_encrypt_32(
uint32_t len,
uint8_t *out,
uint8_t *text,
uint8_t *key,
uint8_t *n1,
uint32_t ctr
)
{
uint32_t ctx[16U] = { 0U };
uint32_t rem1;
uint32_t nb;
uint32_t rem2;
Hacl_Chacha20_Vec32_chacha20_init_32(ctx, key, n1, ctr);
rem1 = len % (uint32_t)64U;
nb = len / (uint32_t)64U;
rem2 = len % (uint32_t)64U;
{
uint32_t i0;
for (i0 = (uint32_t)0U; i0 < nb; i0 = i0 + (uint32_t)1U)
{
uint8_t *uu____0 = out + i0 * (uint32_t)64U;
uint8_t *uu____1 = text + i0 * (uint32_t)64U;
uint32_t k[16U] = { 0U };
Hacl_Chacha20_Vec32_chacha20_core_32(k, ctx, i0);
{
uint32_t i;
for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U)
{
uint32_t u = load32_le(uu____1 + i * (uint32_t)4U);
uint32_t x = u;
uint32_t y = x ^ k[i];
store32_le(uu____0 + i * (uint32_t)4U, y);
}
}
}
}
if (rem2 > (uint32_t)0U)
{
uint8_t *uu____2 = out + nb * (uint32_t)64U;
uint8_t *uu____3 = text + nb * (uint32_t)64U;
uint8_t plain[64U] = { 0U };
memcpy(plain, uu____3, rem1 * sizeof uu____3[0U]);
{
uint32_t k[16U] = { 0U };
Hacl_Chacha20_Vec32_chacha20_core_32(k, ctx, nb);
{
uint32_t i;
for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U)
{
uint32_t u = load32_le(plain + i * (uint32_t)4U);
uint32_t x = u;
uint32_t y = x ^ k[i];
store32_le(plain + i * (uint32_t)4U, y);
}
}
memcpy(uu____2, plain, rem1 * sizeof plain[0U]);
}
}
}
void
Hacl_Chacha20_Vec32_chacha20_decrypt_32(
uint32_t len,
uint8_t *out,
uint8_t *cipher,
uint8_t *key,
uint8_t *n1,
uint32_t ctr
)
{
uint32_t ctx[16U] = { 0U };
uint32_t rem1;
uint32_t nb;
uint32_t rem2;
Hacl_Chacha20_Vec32_chacha20_init_32(ctx, key, n1, ctr);
rem1 = len % (uint32_t)64U;
nb = len / (uint32_t)64U;
rem2 = len % (uint32_t)64U;
{
uint32_t i0;
for (i0 = (uint32_t)0U; i0 < nb; i0 = i0 + (uint32_t)1U)
{
uint8_t *uu____0 = out + i0 * (uint32_t)64U;
uint8_t *uu____1 = cipher + i0 * (uint32_t)64U;
uint32_t k[16U] = { 0U };
Hacl_Chacha20_Vec32_chacha20_core_32(k, ctx, i0);
{
uint32_t i;
for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U)
{
uint32_t u = load32_le(uu____1 + i * (uint32_t)4U);
uint32_t x = u;
uint32_t y = x ^ k[i];
store32_le(uu____0 + i * (uint32_t)4U, y);
}
}
}
}
if (rem2 > (uint32_t)0U)
{
uint8_t *uu____2 = out + nb * (uint32_t)64U;
uint8_t *uu____3 = cipher + nb * (uint32_t)64U;
uint8_t plain[64U] = { 0U };
memcpy(plain, uu____3, rem1 * sizeof uu____3[0U]);
{
uint32_t k[16U] = { 0U };
Hacl_Chacha20_Vec32_chacha20_core_32(k, ctx, nb);
{
uint32_t i;
for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U)
{
uint32_t u = load32_le(plain + i * (uint32_t)4U);
uint32_t x = u;
uint32_t y = x ^ k[i];
store32_le(plain + i * (uint32_t)4U, y);
}
}
memcpy(uu____2, plain, rem1 * sizeof plain[0U]);
}
}
}