balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
a8d2998170
ligo/vendors/ocaml-hacl/src/Hacl_SHA2_512.c

391 lines
13 KiB
C
Raw Blame History

/* MIT License
*
* Copyright (c) 2016-2017 INRIA and Microsoft Corporation
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*/
#include "Hacl_SHA2_512.h"
static void
Hacl_Hash_Lib_LoadStore_uint64s_from_be_bytes(uint64_t *output, uint8_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U)
{
uint8_t *x0 = input + (uint32_t)8U * i;
uint64_t inputi = load64_be(x0);
output[i] = inputi;
}
}
static void
Hacl_Hash_Lib_LoadStore_uint64s_to_be_bytes(uint8_t *output, uint64_t *input, uint32_t len)
{
for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U)
{
uint64_t hd1 = input[i];
uint8_t *x0 = output + (uint32_t)8U * i;
store64_be(x0, hd1);
}
}
static void Hacl_Impl_SHA2_512_init(uint64_t *state)
{
uint64_t *n1 = state + (uint32_t)168U;
uint64_t *k1 = state;
uint64_t *h_01 = state + (uint32_t)160U;
uint64_t *p10 = k1;
uint64_t *p20 = k1 + (uint32_t)16U;
uint64_t *p3 = k1 + (uint32_t)32U;
uint64_t *p4 = k1 + (uint32_t)48U;
uint64_t *p5 = k1 + (uint32_t)64U;
uint64_t *p11 = p10;
uint64_t *p21 = p10 + (uint32_t)8U;
uint64_t *p12 = p11;
uint64_t *p22 = p11 + (uint32_t)4U;
p12[0U] = (uint64_t)0x428a2f98d728ae22U;
p12[1U] = (uint64_t)0x7137449123ef65cdU;
p12[2U] = (uint64_t)0xb5c0fbcfec4d3b2fU;
p12[3U] = (uint64_t)0xe9b5dba58189dbbcU;
p22[0U] = (uint64_t)0x3956c25bf348b538U;
p22[1U] = (uint64_t)0x59f111f1b605d019U;
p22[2U] = (uint64_t)0x923f82a4af194f9bU;
p22[3U] = (uint64_t)0xab1c5ed5da6d8118U;
uint64_t *p13 = p21;
uint64_t *p23 = p21 + (uint32_t)4U;
p13[0U] = (uint64_t)0xd807aa98a3030242U;
p13[1U] = (uint64_t)0x12835b0145706fbeU;
p13[2U] = (uint64_t)0x243185be4ee4b28cU;
p13[3U] = (uint64_t)0x550c7dc3d5ffb4e2U;
p23[0U] = (uint64_t)0x72be5d74f27b896fU;
p23[1U] = (uint64_t)0x80deb1fe3b1696b1U;
p23[2U] = (uint64_t)0x9bdc06a725c71235U;
p23[3U] = (uint64_t)0xc19bf174cf692694U;
uint64_t *p14 = p20;
uint64_t *p24 = p20 + (uint32_t)8U;
uint64_t *p15 = p14;
uint64_t *p25 = p14 + (uint32_t)4U;
p15[0U] = (uint64_t)0xe49b69c19ef14ad2U;
p15[1U] = (uint64_t)0xefbe4786384f25e3U;
p15[2U] = (uint64_t)0x0fc19dc68b8cd5b5U;
p15[3U] = (uint64_t)0x240ca1cc77ac9c65U;
p25[0U] = (uint64_t)0x2de92c6f592b0275U;
p25[1U] = (uint64_t)0x4a7484aa6ea6e483U;
p25[2U] = (uint64_t)0x5cb0a9dcbd41fbd4U;
p25[3U] = (uint64_t)0x76f988da831153b5U;
uint64_t *p16 = p24;
uint64_t *p26 = p24 + (uint32_t)4U;
p16[0U] = (uint64_t)0x983e5152ee66dfabU;
p16[1U] = (uint64_t)0xa831c66d2db43210U;
p16[2U] = (uint64_t)0xb00327c898fb213fU;
p16[3U] = (uint64_t)0xbf597fc7beef0ee4U;
p26[0U] = (uint64_t)0xc6e00bf33da88fc2U;
p26[1U] = (uint64_t)0xd5a79147930aa725U;
p26[2U] = (uint64_t)0x06ca6351e003826fU;
p26[3U] = (uint64_t)0x142929670a0e6e70U;
uint64_t *p17 = p3;
uint64_t *p27 = p3 + (uint32_t)8U;
uint64_t *p18 = p17;
uint64_t *p28 = p17 + (uint32_t)4U;
p18[0U] = (uint64_t)0x27b70a8546d22ffcU;
p18[1U] = (uint64_t)0x2e1b21385c26c926U;
p18[2U] = (uint64_t)0x4d2c6dfc5ac42aedU;
p18[3U] = (uint64_t)0x53380d139d95b3dfU;
p28[0U] = (uint64_t)0x650a73548baf63deU;
p28[1U] = (uint64_t)0x766a0abb3c77b2a8U;
p28[2U] = (uint64_t)0x81c2c92e47edaee6U;
p28[3U] = (uint64_t)0x92722c851482353bU;
uint64_t *p19 = p27;
uint64_t *p29 = p27 + (uint32_t)4U;
p19[0U] = (uint64_t)0xa2bfe8a14cf10364U;
p19[1U] = (uint64_t)0xa81a664bbc423001U;
p19[2U] = (uint64_t)0xc24b8b70d0f89791U;
p19[3U] = (uint64_t)0xc76c51a30654be30U;
p29[0U] = (uint64_t)0xd192e819d6ef5218U;
p29[1U] = (uint64_t)0xd69906245565a910U;
p29[2U] = (uint64_t)0xf40e35855771202aU;
p29[3U] = (uint64_t)0x106aa07032bbd1b8U;
uint64_t *p110 = p4;
uint64_t *p210 = p4 + (uint32_t)8U;
uint64_t *p111 = p110;
uint64_t *p211 = p110 + (uint32_t)4U;
p111[0U] = (uint64_t)0x19a4c116b8d2d0c8U;
p111[1U] = (uint64_t)0x1e376c085141ab53U;
p111[2U] = (uint64_t)0x2748774cdf8eeb99U;
p111[3U] = (uint64_t)0x34b0bcb5e19b48a8U;
p211[0U] = (uint64_t)0x391c0cb3c5c95a63U;
p211[1U] = (uint64_t)0x4ed8aa4ae3418acbU;
p211[2U] = (uint64_t)0x5b9cca4f7763e373U;
p211[3U] = (uint64_t)0x682e6ff3d6b2b8a3U;
uint64_t *p112 = p210;
uint64_t *p212 = p210 + (uint32_t)4U;
p112[0U] = (uint64_t)0x748f82ee5defb2fcU;
p112[1U] = (uint64_t)0x78a5636f43172f60U;
p112[2U] = (uint64_t)0x84c87814a1f0ab72U;
p112[3U] = (uint64_t)0x8cc702081a6439ecU;
p212[0U] = (uint64_t)0x90befffa23631e28U;
p212[1U] = (uint64_t)0xa4506cebde82bde9U;
p212[2U] = (uint64_t)0xbef9a3f7b2c67915U;
p212[3U] = (uint64_t)0xc67178f2e372532bU;
uint64_t *p113 = p5;
uint64_t *p213 = p5 + (uint32_t)8U;
uint64_t *p1 = p113;
uint64_t *p214 = p113 + (uint32_t)4U;
p1[0U] = (uint64_t)0xca273eceea26619cU;
p1[1U] = (uint64_t)0xd186b8c721c0c207U;
p1[2U] = (uint64_t)0xeada7dd6cde0eb1eU;
p1[3U] = (uint64_t)0xf57d4f7fee6ed178U;
p214[0U] = (uint64_t)0x06f067aa72176fbaU;
p214[1U] = (uint64_t)0x0a637dc5a2c898a6U;
p214[2U] = (uint64_t)0x113f9804bef90daeU;
p214[3U] = (uint64_t)0x1b710b35131c471bU;
uint64_t *p114 = p213;
uint64_t *p215 = p213 + (uint32_t)4U;
p114[0U] = (uint64_t)0x28db77f523047d84U;
p114[1U] = (uint64_t)0x32caab7b40c72493U;
p114[2U] = (uint64_t)0x3c9ebe0a15c9bebcU;
p114[3U] = (uint64_t)0x431d67c49c100d4cU;
p215[0U] = (uint64_t)0x4cc5d4becb3e42b6U;
p215[1U] = (uint64_t)0x597f299cfc657e2aU;
p215[2U] = (uint64_t)0x5fcb6fab3ad6faecU;
p215[3U] = (uint64_t)0x6c44198c4a475817U;
uint64_t *p115 = h_01;
uint64_t *p2 = h_01 + (uint32_t)4U;
p115[0U] = (uint64_t)0x6a09e667f3bcc908U;
p115[1U] = (uint64_t)0xbb67ae8584caa73bU;
p115[2U] = (uint64_t)0x3c6ef372fe94f82bU;
p115[3U] = (uint64_t)0xa54ff53a5f1d36f1U;
p2[0U] = (uint64_t)0x510e527fade682d1U;
p2[1U] = (uint64_t)0x9b05688c2b3e6c1fU;
p2[2U] = (uint64_t)0x1f83d9abfb41bd6bU;
p2[3U] = (uint64_t)0x5be0cd19137e2179U;
n1[0U] = (uint64_t)0U;
}
static void Hacl_Impl_SHA2_512_update(uint64_t *state, uint8_t *data)
{
KRML_CHECK_SIZE((uint64_t)(uint32_t)0U, (uint32_t)16U);
uint64_t data_w[16U];
for (uint32_t _i = 0U; _i < (uint32_t)16U; ++_i)
data_w[_i] = (uint64_t)(uint32_t)0U;
Hacl_Hash_Lib_LoadStore_uint64s_from_be_bytes(data_w, data, (uint32_t)16U);
uint64_t *hash_w = state + (uint32_t)160U;
uint64_t *ws_w = state + (uint32_t)80U;
uint64_t *k_w = state;
uint64_t *counter_w = state + (uint32_t)168U;
for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U)
{
uint64_t b = data_w[i];
ws_w[i] = b;
}
for (uint32_t i = (uint32_t)16U; i < (uint32_t)80U; i = i + (uint32_t)1U)
{
uint64_t t16 = ws_w[i - (uint32_t)16U];
uint64_t t15 = ws_w[i - (uint32_t)15U];
uint64_t t7 = ws_w[i - (uint32_t)7U];
uint64_t t2 = ws_w[i - (uint32_t)2U];
ws_w[i] =
((t2 >> (uint32_t)19U | t2 << ((uint32_t)64U - (uint32_t)19U))
^ ((t2 >> (uint32_t)61U | t2 << ((uint32_t)64U - (uint32_t)61U)) ^ t2 >> (uint32_t)6U))
+
t7
+
((t15 >> (uint32_t)1U | t15 << ((uint32_t)64U - (uint32_t)1U))
^ ((t15 >> (uint32_t)8U | t15 << ((uint32_t)64U - (uint32_t)8U)) ^ t15 >> (uint32_t)7U))
+ t16;
}
uint64_t hash_0[8U] = { 0U };
memcpy(hash_0, hash_w, (uint32_t)8U * sizeof hash_w[0U]);
for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i = i + (uint32_t)1U)
{
uint64_t a = hash_0[0U];
uint64_t b = hash_0[1U];
uint64_t c = hash_0[2U];
uint64_t d = hash_0[3U];
uint64_t e = hash_0[4U];
uint64_t f1 = hash_0[5U];
uint64_t g = hash_0[6U];
uint64_t h = hash_0[7U];
uint64_t k_t = k_w[i];
uint64_t ws_t = ws_w[i];
uint64_t
t1 =
h
+
((e >> (uint32_t)14U | e << ((uint32_t)64U - (uint32_t)14U))
^
((e >> (uint32_t)18U | e << ((uint32_t)64U - (uint32_t)18U))
^ (e >> (uint32_t)41U | e << ((uint32_t)64U - (uint32_t)41U))))
+ ((e & f1) ^ (~e & g))
+ k_t
+ ws_t;
uint64_t
t2 =
((a >> (uint32_t)28U | a << ((uint32_t)64U - (uint32_t)28U))
^
((a >> (uint32_t)34U | a << ((uint32_t)64U - (uint32_t)34U))
^ (a >> (uint32_t)39U | a << ((uint32_t)64U - (uint32_t)39U))))
+ ((a & b) ^ ((a & c) ^ (b & c)));
uint64_t x1 = t1 + t2;
uint64_t x5 = d + t1;
uint64_t *p1 = hash_0;
uint64_t *p2 = hash_0 + (uint32_t)4U;
p1[0U] = x1;
p1[1U] = a;
p1[2U] = b;
p1[3U] = c;
p2[0U] = x5;
p2[1U] = e;
p2[2U] = f1;
p2[3U] = g;
}
for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i = i + (uint32_t)1U)
{
uint64_t xi = hash_w[i];
uint64_t yi = hash_0[i];
hash_w[i] = xi + yi;
}
uint64_t c0 = counter_w[0U];
uint64_t one1 = (uint64_t)(uint32_t)1U;
counter_w[0U] = c0 + one1;
}
static void Hacl_Impl_SHA2_512_update_multi(uint64_t *state, uint8_t *data, uint32_t n1)
{
for (uint32_t i = (uint32_t)0U; i < n1; i = i + (uint32_t)1U)
{
uint8_t *b = data + i * (uint32_t)128U;
Hacl_Impl_SHA2_512_update(state, b);
}
}
static void Hacl_Impl_SHA2_512_update_last(uint64_t *state, uint8_t *data, uint64_t len)
{
uint8_t blocks[256U] = { 0U };
uint32_t nb;
if (len < (uint64_t)112U)
nb = (uint32_t)1U;
else
nb = (uint32_t)2U;
uint8_t *final_blocks;
if (len < (uint64_t)112U)
final_blocks = blocks + (uint32_t)128U;
else
final_blocks = blocks;
memcpy(final_blocks, data, (uint32_t)len * sizeof data[0U]);
uint64_t n1 = state[168U];
uint8_t *padding = final_blocks + (uint32_t)len;
FStar_UInt128_t
encodedlen =
FStar_UInt128_shift_left(FStar_UInt128_add(FStar_UInt128_mul_wide(n1, (uint64_t)(uint32_t)128U),
FStar_UInt128_uint64_to_uint128(len)),
(uint32_t)3U);
uint32_t
pad0len = ((uint32_t)256U - ((uint32_t)len + (uint32_t)16U + (uint32_t)1U)) % (uint32_t)128U;
uint8_t *buf1 = padding;
uint8_t *buf2 = padding + (uint32_t)1U + pad0len;
buf1[0U] = (uint8_t)0x80U;
store128_be(buf2, encodedlen);
Hacl_Impl_SHA2_512_update_multi(state, final_blocks, nb);
}
static void Hacl_Impl_SHA2_512_finish(uint64_t *state, uint8_t *hash1)
{
uint64_t *hash_w = state + (uint32_t)160U;
Hacl_Hash_Lib_LoadStore_uint64s_to_be_bytes(hash1, hash_w, (uint32_t)8U);
}
static void Hacl_Impl_SHA2_512_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
{
KRML_CHECK_SIZE((uint64_t)(uint32_t)0U, (uint32_t)169U);
uint64_t state[169U];
for (uint32_t _i = 0U; _i < (uint32_t)169U; ++_i)
state[_i] = (uint64_t)(uint32_t)0U;
uint32_t n1 = len / (uint32_t)128U;
uint32_t r = len % (uint32_t)128U;
uint8_t *input_blocks = input;
uint8_t *input_last = input + n1 * (uint32_t)128U;
Hacl_Impl_SHA2_512_init(state);
Hacl_Impl_SHA2_512_update_multi(state, input_blocks, n1);
Hacl_Impl_SHA2_512_update_last(state, input_last, (uint64_t)r);
Hacl_Impl_SHA2_512_finish(state, hash1);
}
uint32_t Hacl_SHA2_512_size_word = (uint32_t)8U;
uint32_t Hacl_SHA2_512_size_hash_w = (uint32_t)8U;
uint32_t Hacl_SHA2_512_size_block_w = (uint32_t)16U;
uint32_t Hacl_SHA2_512_size_hash = (uint32_t)64U;
uint32_t Hacl_SHA2_512_size_block = (uint32_t)128U;
uint32_t Hacl_SHA2_512_size_k_w = (uint32_t)80U;
uint32_t Hacl_SHA2_512_size_ws_w = (uint32_t)80U;
uint32_t Hacl_SHA2_512_size_whash_w = (uint32_t)8U;
uint32_t Hacl_SHA2_512_size_count_w = (uint32_t)1U;
uint32_t Hacl_SHA2_512_size_len_8 = (uint32_t)16U;
uint32_t Hacl_SHA2_512_size_state = (uint32_t)169U;
uint32_t Hacl_SHA2_512_pos_k_w = (uint32_t)0U;
uint32_t Hacl_SHA2_512_pos_ws_w = (uint32_t)80U;
uint32_t Hacl_SHA2_512_pos_whash_w = (uint32_t)160U;
uint32_t Hacl_SHA2_512_pos_count_w = (uint32_t)168U;
void Hacl_SHA2_512_init(uint64_t *state)
{
Hacl_Impl_SHA2_512_init(state);
}
void Hacl_SHA2_512_update(uint64_t *state, uint8_t *data)
{
Hacl_Impl_SHA2_512_update(state, data);
}
void Hacl_SHA2_512_update_multi(uint64_t *state, uint8_t *data, uint32_t n1)
{
Hacl_Impl_SHA2_512_update_multi(state, data, n1);
}
void Hacl_SHA2_512_update_last(uint64_t *state, uint8_t *data, uint64_t len)
{
Hacl_Impl_SHA2_512_update_last(state, data, len);
}
void Hacl_SHA2_512_finish(uint64_t *state, uint8_t *hash1)
{
Hacl_Impl_SHA2_512_finish(state, hash1);
}
void Hacl_SHA2_512_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
{
Hacl_Impl_SHA2_512_hash(hash1, input, len);
}
Reference in New Issue View Git Blame Copy Permalink