LCOV - code coverage report
Current view: | top level - Modules/_hacl - Hacl_Streaming_SHA2.c (source / functions) |  |  | Hit | Total | Coverage
Test: | CPython 3.12 LCOV report [commit 5e6661bce9] |  | Lines: | 0 | 614 | 0.0 %
Date: | 2023-03-20 08:15:36 |  | Functions: | 0 | 46 | 0.0 %
|  |  | Branches: | 0 | 138 | 0.0 %

               Branch data     Line data    Source code
           1                 :            : /* MIT License
           2                 :            :  *
           3                 :            :  * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
           4                 :            :  * Copyright (c) 2022-2023 HACL* Contributors
           5                 :            :  *
           6                 :            :  * Permission is hereby granted, free of charge, to any person obtaining a copy
           7                 :            :  * of this software and associated documentation files (the "Software"), to deal
           8                 :            :  * in the Software without restriction, including without limitation the rights
           9                 :            :  * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
          10                 :            :  * copies of the Software, and to permit persons to whom the Software is
          11                 :            :  * furnished to do so, subject to the following conditions:
          12                 :            :  *
          13                 :            :  * The above copyright notice and this permission notice shall be included in all
          14                 :            :  * copies or substantial portions of the Software.
          15                 :            :  *
          16                 :            :  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
          17                 :            :  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
          18                 :            :  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
          19                 :            :  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
          20                 :            :  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
          21                 :            :  * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
          22                 :            :  * SOFTWARE.
          23                 :            :  */
          24                 :            :
          25                 :            :
          26                 :            : #include "Hacl_Streaming_SHA2.h"
          27                 :            :
          28                 :            : #include "internal/Hacl_SHA2_Generic.h"
          29                 :            :
          30                 :            :
          31                 :          0 : static inline void sha256_init(uint32_t *hash)
          32                 :            : {
          33                 :          0 :   KRML_MAYBE_FOR8(i,
          34                 :            :     (uint32_t)0U,
          35                 :            :     (uint32_t)8U,
          36                 :            :     (uint32_t)1U,
          37                 :            :     uint32_t *os = hash;
          38                 :            :     uint32_t x = Hacl_Impl_SHA2_Generic_h256[i];
          39                 :            :     os[i] = x;);
          40                 :          0 : }
          41                 :            :
          42                 :          0 : static inline void sha256_update0(uint8_t *b, uint32_t *hash)
          43                 :            : {
          44                 :          0 :   uint32_t hash_old[8U] = { 0U };
          45                 :          0 :   uint32_t ws[16U] = { 0U };
          46                 :          0 :   memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint32_t));
          47                 :          0 :   uint8_t *b10 = b;
          48                 :          0 :   uint32_t u = load32_be(b10);
          49                 :          0 :   ws[0U] = u;
          50                 :          0 :   uint32_t u0 = load32_be(b10 + (uint32_t)4U);
          51                 :          0 :   ws[1U] = u0;
          52                 :          0 :   uint32_t u1 = load32_be(b10 + (uint32_t)8U);
          53                 :          0 :   ws[2U] = u1;
          54                 :          0 :   uint32_t u2 = load32_be(b10 + (uint32_t)12U);
          55                 :          0 :   ws[3U] = u2;
          56                 :          0 :   uint32_t u3 = load32_be(b10 + (uint32_t)16U);
          57                 :          0 :   ws[4U] = u3;
          58                 :          0 :   uint32_t u4 = load32_be(b10 + (uint32_t)20U);
          59                 :          0 :   ws[5U] = u4;
          60                 :          0 :   uint32_t u5 = load32_be(b10 + (uint32_t)24U);
          61                 :          0 :   ws[6U] = u5;
          62                 :          0 :   uint32_t u6 = load32_be(b10 + (uint32_t)28U);
          63                 :          0 :   ws[7U] = u6;
          64                 :          0 :   uint32_t u7 = load32_be(b10 + (uint32_t)32U);
          65                 :          0 :   ws[8U] = u7;
          66                 :          0 :   uint32_t u8 = load32_be(b10 + (uint32_t)36U);
          67                 :          0 :   ws[9U] = u8;
          68                 :          0 :   uint32_t u9 = load32_be(b10 + (uint32_t)40U);
          69                 :          0 :   ws[10U] = u9;
          70                 :          0 :   uint32_t u10 = load32_be(b10 + (uint32_t)44U);
          71                 :          0 :   ws[11U] = u10;
          72                 :          0 :   uint32_t u11 = load32_be(b10 + (uint32_t)48U);
          73                 :          0 :   ws[12U] = u11;
          74                 :          0 :   uint32_t u12 = load32_be(b10 + (uint32_t)52U);
          75                 :          0 :   ws[13U] = u12;
          76                 :          0 :   uint32_t u13 = load32_be(b10 + (uint32_t)56U);
          77                 :          0 :   ws[14U] = u13;
          78                 :          0 :   uint32_t u14 = load32_be(b10 + (uint32_t)60U);
          79                 :          0 :   ws[15U] = u14;
          80   [ #  #  #  #  :          0 :   KRML_MAYBE_FOR4(i0,
                 #  #  #  # ]
          81                 :            :     (uint32_t)0U,
          82                 :            :     (uint32_t)4U,
          83                 :            :     (uint32_t)1U,
          84                 :            :     KRML_MAYBE_FOR16(i,
          85                 :            :       (uint32_t)0U,
          86                 :            :       (uint32_t)16U,
          87                 :            :       (uint32_t)1U,
          88                 :            :       uint32_t k_t = Hacl_Impl_SHA2_Generic_k224_256[(uint32_t)16U * i0 + i];
          89                 :            :       uint32_t ws_t = ws[i];
          90                 :            :       uint32_t a0 = hash[0U];
          91                 :            :       uint32_t b0 = hash[1U];
          92                 :            :       uint32_t c0 = hash[2U];
          93                 :            :       uint32_t d0 = hash[3U];
          94                 :            :       uint32_t e0 = hash[4U];
          95                 :            :       uint32_t f0 = hash[5U];
          96                 :            :       uint32_t g0 = hash[6U];
          97                 :            :       uint32_t h02 = hash[7U];
          98                 :            :       uint32_t k_e_t = k_t;
          99                 :            :       uint32_t
         100                 :            :       t1 =
         101                 :            :         h02
         102                 :            :         +
         103                 :            :           ((e0 << (uint32_t)26U | e0 >> (uint32_t)6U)
         104                 :            :           ^
         105                 :            :             ((e0 << (uint32_t)21U | e0 >> (uint32_t)11U)
         106                 :            :             ^ (e0 << (uint32_t)7U | e0 >> (uint32_t)25U)))
         107                 :            :         + ((e0 & f0) ^ (~e0 & g0))
         108                 :            :         + k_e_t
         109                 :            :         + ws_t;
         110                 :            :       uint32_t
         111                 :            :       t2 =
         112                 :            :         ((a0 << (uint32_t)30U | a0 >> (uint32_t)2U)
         113                 :            :         ^
         114                 :            :           ((a0 << (uint32_t)19U | a0 >> (uint32_t)13U)
         115                 :            :           ^ (a0 << (uint32_t)10U | a0 >> (uint32_t)22U)))
         116                 :            :         + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0)));
         117                 :            :       uint32_t a1 = t1 + t2;
         118                 :            :       uint32_t b1 = a0;
         119                 :            :       uint32_t c1 = b0;
         120                 :            :       uint32_t d1 = c0;
         121                 :            :       uint32_t e1 = d0 + t1;
         122                 :            :       uint32_t f1 = e0;
         123                 :            :       uint32_t g1 = f0;
         124                 :            :       uint32_t h12 = g0;
         125                 :            :       hash[0U] = a1;
         126                 :            :       hash[1U] = b1;
         127                 :            :       hash[2U] = c1;
         128                 :            :       hash[3U] = d1;
         129                 :            :       hash[4U] = e1;
         130                 :            :       hash[5U] = f1;
         131                 :            :       hash[6U] = g1;
         132                 :            :       hash[7U] = h12;);
         133                 :            :     if (i0 < (uint32_t)3U)
         134                 :            :     {
         135                 :            :       KRML_MAYBE_FOR16(i,
         136                 :            :         (uint32_t)0U,
         137                 :            :         (uint32_t)16U,
         138                 :            :         (uint32_t)1U,
         139                 :            :         uint32_t t16 = ws[i];
         140                 :            :         uint32_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U];
         141                 :            :         uint32_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U];
         142                 :            :         uint32_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U];
         143                 :            :         uint32_t
         144                 :            :         s1 =
         145                 :            :           (t2 << (uint32_t)15U | t2 >> (uint32_t)17U)
         146                 :            :           ^ ((t2 << (uint32_t)13U | t2 >> (uint32_t)19U) ^ t2 >> (uint32_t)10U);
         147                 :            :         uint32_t
         148                 :            :         s0 =
         149                 :            :           (t15 << (uint32_t)25U | t15 >> (uint32_t)7U)
         150                 :            :           ^ ((t15 << (uint32_t)14U | t15 >> (uint32_t)18U) ^ t15 >> (uint32_t)3U);
         151                 :            :         ws[i] = s1 + t7 + s0 + t16;);
         152                 :            :     });
         153                 :          0 :   KRML_MAYBE_FOR8(i,
         154                 :            :     (uint32_t)0U,
         155                 :            :     (uint32_t)8U,
         156                 :            :     (uint32_t)1U,
         157                 :            :     uint32_t *os = hash;
         158                 :            :     uint32_t x = hash[i] + hash_old[i];
         159                 :            :     os[i] = x;);
         160                 :          0 : }
         161                 :            :
         162                 :          0 : static inline void sha256_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st)
         163                 :            : {
         164                 :          0 :   uint32_t blocks = len / (uint32_t)64U;
         165         [ #  # ]:          0 :   for (uint32_t i = (uint32_t)0U; i < blocks; i++)
         166                 :            :   {
         167                 :          0 :     uint8_t *b0 = b;
         168                 :          0 :     uint8_t *mb = b0 + i * (uint32_t)64U;
         169                 :          0 :     sha256_update0(mb, st);
         170                 :            :   }
         171                 :          0 : }
         172                 :            :
         173                 :            : static inline void
         174                 :          0 : sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *hash)
         175                 :            : {
         176                 :            :   uint32_t blocks;
         177         [ #  # ]:          0 :   if (len + (uint32_t)8U + (uint32_t)1U <= (uint32_t)64U)
         178                 :            :   {
         179                 :          0 :     blocks = (uint32_t)1U;
         180                 :            :   }
         181                 :            :   else
         182                 :            :   {
         183                 :          0 :     blocks = (uint32_t)2U;
         184                 :            :   }
         185                 :          0 :   uint32_t fin = blocks * (uint32_t)64U;
         186                 :          0 :   uint8_t last[128U] = { 0U };
         187                 :          0 :   uint8_t totlen_buf[8U] = { 0U };
         188                 :          0 :   uint64_t total_len_bits = totlen << (uint32_t)3U;
         189                 :          0 :   store64_be(totlen_buf, total_len_bits);
         190                 :          0 :   uint8_t *b0 = b;
         191                 :          0 :   memcpy(last, b0, len * sizeof (uint8_t));
         192                 :          0 :   last[len] = (uint8_t)0x80U;
         193                 :          0 :   memcpy(last + fin - (uint32_t)8U, totlen_buf, (uint32_t)8U * sizeof (uint8_t));
         194                 :          0 :   uint8_t *last00 = last;
         195                 :          0 :   uint8_t *last10 = last + (uint32_t)64U;
         196                 :          0 :   uint8_t *l0 = last00;
         197                 :          0 :   uint8_t *l1 = last10;
         198                 :          0 :   uint8_t *lb0 = l0;
         199                 :          0 :   uint8_t *lb1 = l1;
         200                 :          0 :   uint8_t *last0 = lb0;
         201                 :          0 :   uint8_t *last1 = lb1;
         202                 :          0 :   sha256_update0(last0, hash);
         203         [ #  # ]:          0 :   if (blocks > (uint32_t)1U)
         204                 :            :   {
         205                 :          0 :     sha256_update0(last1, hash);
         206                 :          0 :     return;
         207                 :            :   }
         208                 :            : }
         209                 :            :
         210                 :          0 : static inline void sha256_finish(uint32_t *st, uint8_t *h)
         211                 :            : {
         212                 :          0 :   uint8_t hbuf[32U] = { 0U };
         213                 :          0 :   KRML_MAYBE_FOR8(i,
         214                 :            :     (uint32_t)0U,
         215                 :            :     (uint32_t)8U,
         216                 :            :     (uint32_t)1U,
         217                 :            :     store32_be(hbuf + i * (uint32_t)4U, st[i]););
         218                 :          0 :   memcpy(h, hbuf, (uint32_t)32U * sizeof (uint8_t));
         219                 :          0 : }
         220                 :            :
         221                 :          0 : static inline void sha224_init(uint32_t *hash)
         222                 :            : {
         223                 :          0 :   KRML_MAYBE_FOR8(i,
         224                 :            :     (uint32_t)0U,
         225                 :            :     (uint32_t)8U,
         226                 :            :     (uint32_t)1U,
         227                 :            :     uint32_t *os = hash;
         228                 :            :     uint32_t x = Hacl_Impl_SHA2_Generic_h224[i];
         229                 :            :     os[i] = x;);
         230                 :          0 : }
         231                 :            :
         232                 :          0 : static inline void sha224_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st)
         233                 :            : {
         234                 :          0 :   sha256_update_nblocks(len, b, st);
         235                 :          0 : }
         236                 :            :
         237                 :          0 : static void sha224_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *st)
         238                 :            : {
         239                 :          0 :   sha256_update_last(totlen, len, b, st);
         240                 :          0 : }
         241                 :            :
         242                 :          0 : static inline void sha224_finish(uint32_t *st, uint8_t *h)
         243                 :            : {
         244                 :          0 :   uint8_t hbuf[32U] = { 0U };
         245                 :          0 :   KRML_MAYBE_FOR8(i,
         246                 :            :     (uint32_t)0U,
         247                 :            :     (uint32_t)8U,
         248                 :            :     (uint32_t)1U,
         249                 :            :     store32_be(hbuf + i * (uint32_t)4U, st[i]););
         250                 :          0 :   memcpy(h, hbuf, (uint32_t)28U * sizeof (uint8_t));
         251                 :          0 : }
         252                 :            :
         253                 :          0 : void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash)
         254                 :            : {
         255                 :          0 :   KRML_MAYBE_FOR8(i,
         256                 :            :     (uint32_t)0U,
         257                 :            :     (uint32_t)8U,
         258                 :            :     (uint32_t)1U,
         259                 :            :     uint64_t *os = hash;
         260                 :            :     uint64_t x = Hacl_Impl_SHA2_Generic_h512[i];
         261                 :            :     os[i] = x;);
         262                 :          0 : }
         263                 :            :
         264                 :          0 : static inline void sha512_update(uint8_t *b, uint64_t *hash)
         265                 :            : {
         266                 :          0 :   uint64_t hash_old[8U] = { 0U };
         267                 :          0 :   uint64_t ws[16U] = { 0U };
         268                 :          0 :   memcpy(hash_old, hash, (uint32_t)8U * sizeof (uint64_t));
         269                 :          0 :   uint8_t *b10 = b;
         270                 :          0 :   uint64_t u = load64_be(b10);
         271                 :          0 :   ws[0U] = u;
         272                 :          0 :   uint64_t u0 = load64_be(b10 + (uint32_t)8U);
         273                 :          0 :   ws[1U] = u0;
         274                 :          0 :   uint64_t u1 = load64_be(b10 + (uint32_t)16U);
         275                 :          0 :   ws[2U] = u1;
         276                 :          0 :   uint64_t u2 = load64_be(b10 + (uint32_t)24U);
         277                 :          0 :   ws[3U] = u2;
         278                 :          0 :   uint64_t u3 = load64_be(b10 + (uint32_t)32U);
         279                 :          0 :   ws[4U] = u3;
         280                 :          0 :   uint64_t u4 = load64_be(b10 + (uint32_t)40U);
         281                 :          0 :   ws[5U] = u4;
         282                 :          0 :   uint64_t u5 = load64_be(b10 + (uint32_t)48U);
         283                 :          0 :   ws[6U] = u5;
         284                 :          0 :   uint64_t u6 = load64_be(b10 + (uint32_t)56U);
         285                 :          0 :   ws[7U] = u6;
         286                 :          0 :   uint64_t u7 = load64_be(b10 + (uint32_t)64U);
         287                 :          0 :   ws[8U] = u7;
         288                 :          0 :   uint64_t u8 = load64_be(b10 + (uint32_t)72U);
         289                 :          0 :   ws[9U] = u8;
         290                 :          0 :   uint64_t u9 = load64_be(b10 + (uint32_t)80U);
         291                 :          0 :   ws[10U] = u9;
         292                 :          0 :   uint64_t u10 = load64_be(b10 + (uint32_t)88U);
         293                 :          0 :   ws[11U] = u10;
         294                 :          0 :   uint64_t u11 = load64_be(b10 + (uint32_t)96U);
         295                 :          0 :   ws[12U] = u11;
         296                 :          0 :   uint64_t u12 = load64_be(b10 + (uint32_t)104U);
         297                 :          0 :   ws[13U] = u12;
         298                 :          0 :   uint64_t u13 = load64_be(b10 + (uint32_t)112U);
         299                 :          0 :   ws[14U] = u13;
         300                 :          0 :   uint64_t u14 = load64_be(b10 + (uint32_t)120U);
         301                 :          0 :   ws[15U] = u14;
         302   [ #  #  #  #  :          0 :   KRML_MAYBE_FOR5(i0,
              #  #  #  #  #
                          # ]
         303                 :            :     (uint32_t)0U,
         304                 :            :     (uint32_t)5U,
         305                 :            :     (uint32_t)1U,
         306                 :            :     KRML_MAYBE_FOR16(i,
         307                 :            :       (uint32_t)0U,
         308                 :            :       (uint32_t)16U,
         309                 :            :       (uint32_t)1U,
         310                 :            :       uint64_t k_t = Hacl_Impl_SHA2_Generic_k384_512[(uint32_t)16U * i0 + i];
         311                 :            :       uint64_t ws_t = ws[i];
         312                 :            :       uint64_t a0 = hash[0U];
         313                 :            :       uint64_t b0 = hash[1U];
         314                 :            :       uint64_t c0 = hash[2U];
         315                 :            :       uint64_t d0 = hash[3U];
         316                 :            :       uint64_t e0 = hash[4U];
         317                 :            :       uint64_t f0 = hash[5U];
         318                 :            :       uint64_t g0 = hash[6U];
         319                 :            :       uint64_t h02 = hash[7U];
         320                 :            :       uint64_t k_e_t = k_t;
         321                 :            :       uint64_t
         322                 :            :       t1 =
         323                 :            :         h02
         324                 :            :         +
         325                 :            :           ((e0 << (uint32_t)50U | e0 >> (uint32_t)14U)
         326                 :            :           ^
         327                 :            :             ((e0 << (uint32_t)46U | e0 >> (uint32_t)18U)
         328                 :            :             ^ (e0 << (uint32_t)23U | e0 >> (uint32_t)41U)))
         329                 :            :         + ((e0 & f0) ^ (~e0 & g0))
         330                 :            :         + k_e_t
         331                 :            :         + ws_t;
         332                 :            :       uint64_t
         333                 :            :       t2 =
         334                 :            :         ((a0 << (uint32_t)36U | a0 >> (uint32_t)28U)
         335                 :            :         ^
         336                 :            :           ((a0 << (uint32_t)30U | a0 >> (uint32_t)34U)
         337                 :            :           ^ (a0 << (uint32_t)25U | a0 >> (uint32_t)39U)))
         338                 :            :         + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0)));
         339                 :            :       uint64_t a1 = t1 + t2;
         340                 :            :       uint64_t b1 = a0;
         341                 :            :       uint64_t c1 = b0;
         342                 :            :       uint64_t d1 = c0;
         343                 :            :       uint64_t e1 = d0 + t1;
         344                 :            :       uint64_t f1 = e0;
         345                 :            :       uint64_t g1 = f0;
         346                 :            :       uint64_t h12 = g0;
         347                 :            :       hash[0U] = a1;
         348                 :            :       hash[1U] = b1;
         349                 :            :       hash[2U] = c1;
         350                 :            :       hash[3U] = d1;
         351                 :            :       hash[4U] = e1;
         352                 :            :       hash[5U] = f1;
         353                 :            :       hash[6U] = g1;
         354                 :            :       hash[7U] = h12;);
         355                 :            :     if (i0 < (uint32_t)4U)
         356                 :            :     {
         357                 :            :       KRML_MAYBE_FOR16(i,
         358                 :            :         (uint32_t)0U,
         359                 :            :         (uint32_t)16U,
         360                 :            :         (uint32_t)1U,
         361                 :            :         uint64_t t16 = ws[i];
         362                 :            :         uint64_t t15 = ws[(i + (uint32_t)1U) % (uint32_t)16U];
         363                 :            :         uint64_t t7 = ws[(i + (uint32_t)9U) % (uint32_t)16U];
         364                 :            :         uint64_t t2 = ws[(i + (uint32_t)14U) % (uint32_t)16U];
         365                 :            :         uint64_t
         366                 :            :         s1 =
         367                 :            :           (t2 << (uint32_t)45U | t2 >> (uint32_t)19U)
         368                 :            :           ^ ((t2 << (uint32_t)3U | t2 >> (uint32_t)61U) ^ t2 >> (uint32_t)6U);
         369                 :            :         uint64_t
         370                 :            :         s0 =
         371                 :            :           (t15 << (uint32_t)63U | t15 >> (uint32_t)1U)
         372                 :            :           ^ ((t15 << (uint32_t)56U | t15 >> (uint32_t)8U) ^ t15 >> (uint32_t)7U);
         373                 :            :         ws[i] = s1 + t7 + s0 + t16;);
         374                 :            :     });
         375                 :          0 :   KRML_MAYBE_FOR8(i,
         376                 :            :     (uint32_t)0U,
         377                 :            :     (uint32_t)8U,
         378                 :            :     (uint32_t)1U,
         379                 :            :     uint64_t *os = hash;
         380                 :            :     uint64_t x = hash[i] + hash_old[i];
         381                 :            :     os[i] = x;);
         382                 :          0 : }
         383                 :            :
         384                 :          0 : static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
         385                 :            : {
         386                 :          0 :   uint32_t blocks = len / (uint32_t)128U;
         387         [ #  # ]:          0 :   for (uint32_t i = (uint32_t)0U; i < blocks; i++)
         388                 :            :   {
         389                 :          0 :     uint8_t *b0 = b;
         390                 :          0 :     uint8_t *mb = b0 + i * (uint32_t)128U;
         391                 :          0 :     sha512_update(mb, st);
         392                 :            :   }
         393                 :          0 : }
         394                 :            :
         395                 :            : static inline void
         396                 :          0 : sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash)
         397                 :            : {
         398                 :            :   uint32_t blocks;
         399         [ #  # ]:          0 :   if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U)
         400                 :            :   {
         401                 :          0 :     blocks = (uint32_t)1U;
         402                 :            :   }
         403                 :            :   else
         404                 :            :   {
         405                 :          0 :     blocks = (uint32_t)2U;
         406                 :            :   }
         407                 :          0 :   uint32_t fin = blocks * (uint32_t)128U;
         408                 :          0 :   uint8_t last[256U] = { 0U };
         409                 :          0 :   uint8_t totlen_buf[16U] = { 0U };
         410                 :          0 :   FStar_UInt128_uint128 total_len_bits = FStar_UInt128_shift_left(totlen, (uint32_t)3U);
         411                 :          0 :   store128_be(totlen_buf, total_len_bits);
         412                 :          0 :   uint8_t *b0 = b;
         413                 :          0 :   memcpy(last, b0, len * sizeof (uint8_t));
         414                 :          0 :   last[len] = (uint8_t)0x80U;
         415                 :          0 :   memcpy(last + fin - (uint32_t)16U, totlen_buf, (uint32_t)16U * sizeof (uint8_t));
         416                 :          0 :   uint8_t *last00 = last;
         417                 :          0 :   uint8_t *last10 = last + (uint32_t)128U;
         418                 :          0 :   uint8_t *l0 = last00;
         419                 :          0 :   uint8_t *l1 = last10;
         420                 :          0 :   uint8_t *lb0 = l0;
         421                 :          0 :   uint8_t *lb1 = l1;
         422                 :          0 :   uint8_t *last0 = lb0;
         423                 :          0 :   uint8_t *last1 = lb1;
         424                 :          0 :   sha512_update(last0, hash);
         425         [ #  # ]:          0 :   if (blocks > (uint32_t)1U)
         426                 :            :   {
         427                 :          0 :     sha512_update(last1, hash);
         428                 :          0 :     return;
         429                 :            :   }
         430                 :            : }
         431                 :            :
         432                 :          0 : static inline void sha512_finish(uint64_t *st, uint8_t *h)
         433                 :            : {
         434                 :          0 :   uint8_t hbuf[64U] = { 0U };
         435                 :          0 :   KRML_MAYBE_FOR8(i,
         436                 :            :     (uint32_t)0U,
         437                 :            :     (uint32_t)8U,
         438                 :            :     (uint32_t)1U,
         439                 :            :     store64_be(hbuf + i * (uint32_t)8U, st[i]););
         440                 :          0 :   memcpy(h, hbuf, (uint32_t)64U * sizeof (uint8_t));
         441                 :          0 : }
         442                 :            :
         443                 :          0 : static inline void sha384_init(uint64_t *hash)
         444                 :            : {
         445                 :          0 :   KRML_MAYBE_FOR8(i,
         446                 :            :     (uint32_t)0U,
         447                 :            :     (uint32_t)8U,
         448                 :            :     (uint32_t)1U,
         449                 :            :     uint64_t *os = hash;
         450                 :            :     uint64_t x = Hacl_Impl_SHA2_Generic_h384[i];
         451                 :            :     os[i] = x;);
         452                 :          0 : }
         453                 :            :
         454                 :          0 : static inline void sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
         455                 :            : {
         456                 :          0 :   sha512_update_nblocks(len, b, st);
         457                 :          0 : }
         458                 :            :
         459                 :            : static void
         460                 :          0 : sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *st)
         461                 :            : {
         462                 :          0 :   sha512_update_last(totlen, len, b, st);
         463                 :          0 : }
         464                 :            :
         465                 :          0 : static inline void sha384_finish(uint64_t *st, uint8_t *h)
         466                 :            : {
         467                 :          0 :   uint8_t hbuf[64U] = { 0U };
         468                 :          0 :   KRML_MAYBE_FOR8(i,
         469                 :            :     (uint32_t)0U,
         470                 :            :     (uint32_t)8U,
         471                 :            :     (uint32_t)1U,
         472                 :            :     store64_be(hbuf + i * (uint32_t)8U, st[i]););
         473                 :          0 :   memcpy(h, hbuf, (uint32_t)48U * sizeof (uint8_t));
         474                 :          0 : }
         475                 :            :
         476                 :            : /**
         477                 :            : Allocate initial state for the SHA2_256 hash. The state is to be freed by
         478                 :            : calling `free_256`.
         479                 :            : */
         480                 :          0 : Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void)
         481                 :            : {
         482                 :          0 :   uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t));
         483                 :          0 :   uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t));
         484                 :            :   Hacl_Streaming_MD_state_32
         485                 :          0 :   s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
         486                 :            :   Hacl_Streaming_MD_state_32
         487                 :          0 :   *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
         488                 :          0 :   p[0U] = s;
         489                 :          0 :   sha256_init(block_state);
         490                 :          0 :   return p;
         491                 :            : }
         492                 :            :
         493                 :            : /**
         494                 :            : Copies the state passed as argument into a newly allocated state (deep copy).
         495                 :            : The state is to be freed by calling `free_256`. Cloning the state this way is
         496                 :            : useful, for instance, if your control-flow diverges and you need to feed
         497                 :            : more (different) data into the hash in each branch.
         498                 :            : */
         499                 :          0 : Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0)
         500                 :            : {
         501                 :          0 :   Hacl_Streaming_MD_state_32 scrut = *s0;
         502                 :          0 :   uint32_t *block_state0 = scrut.block_state;
         503                 :          0 :   uint8_t *buf0 = scrut.buf;
         504                 :          0 :   uint64_t total_len0 = scrut.total_len;
         505                 :          0 :   uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t));
         506                 :          0 :   memcpy(buf, buf0, (uint32_t)64U * sizeof (uint8_t));
         507                 :          0 :   uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t));
         508                 :          0 :   memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint32_t));
         509                 :            :   Hacl_Streaming_MD_state_32
         510                 :          0 :   s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
         511                 :            :   Hacl_Streaming_MD_state_32
         512                 :          0 :   *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
         513                 :          0 :   p[0U] = s;
         514                 :          0 :   return p;
         515                 :            : }
         516                 :            :
         517                 :            : /**
         518                 :            : Reset an existing state to the initial hash state with empty data.
         519                 :            : */
         520                 :          0 : void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s)
         521                 :            : {
         522                 :          0 :   Hacl_Streaming_MD_state_32 scrut = *s;
         523                 :          0 :   uint8_t *buf = scrut.buf;
         524                 :          0 :   uint32_t *block_state = scrut.block_state;
         525                 :          0 :   sha256_init(block_state);
         526                 :            :   Hacl_Streaming_MD_state_32
         527                 :          0 :   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
         528                 :          0 :   s[0U] = tmp;
         529                 :          0 : }
         530                 :            :
         531                 :            : static inline uint32_t
         532                 :          0 : update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
         533                 :            : {
         534                 :          0 :   Hacl_Streaming_MD_state_32 s = *p;
         535                 :          0 :   uint64_t total_len = s.total_len;
         536         [ #  # ]:          0 :   if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len)
         537                 :            :   {
         538                 :          0 :     return (uint32_t)1U;
         539                 :            :   }
         540                 :            :   uint32_t sz;
         541   [ #  #  #  # ]:          0 :   if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
         542                 :            :   {
         543                 :          0 :     sz = (uint32_t)64U;
         544                 :            :   }
         545                 :            :   else
         546                 :            :   {
         547                 :          0 :     sz = (uint32_t)(total_len % (uint64_t)(uint32_t)64U);
         548                 :            :   }
         549         [ #  # ]:          0 :   if (len <= (uint32_t)64U - sz)
         550                 :            :   {
         551                 :          0 :     Hacl_Streaming_MD_state_32 s1 = *p;
         552                 :          0 :     uint32_t *block_state1 = s1.block_state;
         553                 :          0 :     uint8_t *buf = s1.buf;
         554                 :          0 :     uint64_t total_len1 = s1.total_len;
         555                 :            :     uint32_t sz1;
         556   [ #  #  #  # ]:          0 :     if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U)
         557                 :            :     {
         558                 :          0 :       sz1 = (uint32_t)64U;
         559                 :            :     }
         560                 :            :     else
         561                 :            :     {
         562                 :          0 :       sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U);
         563                 :            :     }
         564                 :          0 :     uint8_t *buf2 = buf + sz1;
         565                 :          0 :     memcpy(buf2, data, len * sizeof (uint8_t));
         566                 :          0 :     uint64_t total_len2 = total_len1 + (uint64_t)len;
         567                 :            :     *p
         568                 :          0 :     =
         569                 :            :       (
         570                 :            :         (Hacl_Streaming_MD_state_32){
         571                 :            :           .block_state = block_state1,
         572                 :            :           .buf = buf,
         573                 :            :           .total_len = total_len2
         574                 :            :         }
         575                 :            :       );
         576                 :            :   }
         577         [ #  # ]:          0 :   else if (sz == (uint32_t)0U)
         578                 :            :   {
         579                 :          0 :     Hacl_Streaming_MD_state_32 s1 = *p;
         580                 :          0 :     uint32_t *block_state1 = s1.block_state;
         581                 :          0 :     uint8_t *buf = s1.buf;
         582                 :          0 :     uint64_t total_len1 = s1.total_len;
         583                 :            :     uint32_t sz1;
         584   [ #  #  #  # ]:          0 :     if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U)
         585                 :            :     {
         586                 :          0 :       sz1 = (uint32_t)64U;
         587                 :            :     }
         588                 :            :     else
         589                 :            :     {
         590                 :          0 :       sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U);
         591                 :            :     }
         592         [ #  # ]:          0 :     if (!(sz1 == (uint32_t)0U))
         593                 :            :     {
         594                 :          0 :       sha256_update_nblocks((uint32_t)64U, buf, block_state1);
         595                 :            :     }
         596                 :            :     uint32_t ite;
         597   [ #  #  #  # ]:          0 :     if ((uint64_t)len % (uint64_t)(uint32_t)64U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U)
         598                 :            :     {
         599                 :          0 :       ite = (uint32_t)64U;
         600                 :            :     }
         601                 :            :     else
         602                 :            :     {
         603                 :          0 :       ite = (uint32_t)((uint64_t)len % (uint64_t)(uint32_t)64U);
         604                 :            :     }
         605                 :          0 :     uint32_t n_blocks = (len - ite) / (uint32_t)64U;
         606                 :          0 :     uint32_t data1_len = n_blocks * (uint32_t)64U;
         607                 :          0 :     uint32_t data2_len = len - data1_len;
         608                 :          0 :     uint8_t *data1 = data;
         609                 :          0 :     uint8_t *data2 = data + data1_len;
         610                 :          0 :     sha256_update_nblocks(data1_len, data1, block_state1);
         611                 :          0 :     uint8_t *dst = buf;
         612                 :          0 :     memcpy(dst, data2, data2_len * sizeof (uint8_t));
         613                 :            :     *p
         614                 :          0 :     =
         615                 :            :       (
         616                 :            :         (Hacl_Streaming_MD_state_32){
         617                 :            :           .block_state = block_state1,
         618                 :            :           .buf = buf,
         619                 :          0 :           .total_len = total_len1 + (uint64_t)len
         620                 :            :         }
         621                 :            :       );
         622                 :            :   }
         623                 :            :   else
         624                 :            :   {
         625                 :          0 :     uint32_t diff = (uint32_t)64U - sz;
         626                 :          0 :     uint8_t *data1 = data;
         627                 :          0 :     uint8_t *data2 = data + diff;
         628                 :          0 :     Hacl_Streaming_MD_state_32 s1 = *p;
         629                 :          0 :     uint32_t *block_state10 = s1.block_state;
         630                 :          0 :     uint8_t *buf0 = s1.buf;
         631                 :          0 :     uint64_t total_len10 = s1.total_len;
         632                 :            :     uint32_t sz10;
         633   [ #  #  #  # ]:          0 :     if (total_len10 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len10 > (uint64_t)0U)
         634                 :            :     {
         635                 :          0 :       sz10 = (uint32_t)64U;
         636                 :            :     }
         637                 :            :     else
         638                 :            :     {
         639                 :          0 :       sz10 = (uint32_t)(total_len10 % (uint64_t)(uint32_t)64U);
         640                 :            :     }
         641                 :          0 :     uint8_t *buf2 = buf0 + sz10;
         642                 :          0 :     memcpy(buf2, data1, diff * sizeof (uint8_t));
         643                 :          0 :     uint64_t total_len2 = total_len10 + (uint64_t)diff;
         644                 :            :     *p
         645                 :          0 :     =
         646                 :            :       (
         647                 :            :         (Hacl_Streaming_MD_state_32){
         648                 :            :           .block_state = block_state10,
         649                 :            :           .buf = buf0,
         650                 :            :           .total_len = total_len2
         651                 :            :         }
         652                 :            :       );
         653                 :          0 :     Hacl_Streaming_MD_state_32 s10 = *p;
         654                 :          0 :     uint32_t *block_state1 = s10.block_state;
         655                 :          0 :     uint8_t *buf = s10.buf;
         656                 :          0 :     uint64_t total_len1 = s10.total_len;
         657                 :            :     uint32_t sz1;
         658   [ #  #  #  # ]:          0 :     if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len1 > (uint64_t)0U)
         659                 :            :     {
         660                 :          0 :       sz1 = (uint32_t)64U;
         661                 :            :     }
         662                 :            :     else
         663                 :            :     {
         664                 :          0 :       sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U);
         665                 :            :     }
         666         [ #  # ]:          0 :     if (!(sz1 == (uint32_t)0U))
         667                 :            :     {
         668                 :          0 :       sha256_update_nblocks((uint32_t)64U, buf, block_state1);
         669                 :            :     }
         670                 :            :     uint32_t ite;
         671                 :            :     if
         672                 :          0 :     (
         673                 :          0 :       (uint64_t)(len - diff)
         674                 :            :       % (uint64_t)(uint32_t)64U
         675         [ #  # ]:          0 :       == (uint64_t)0U
         676         [ #  # ]:          0 :       && (uint64_t)(len - diff) > (uint64_t)0U
         677                 :            :     )
         678                 :            :     {
         679                 :          0 :       ite = (uint32_t)64U;
         680                 :            :     }
         681                 :            :     else
         682                 :            :     {
         683                 :          0 :       ite = (uint32_t)((uint64_t)(len - diff) % (uint64_t)(uint32_t)64U);
         684                 :            :     }
         685                 :          0 :     uint32_t n_blocks = (len - diff - ite) / (uint32_t)64U;
         686                 :          0 :     uint32_t data1_len = n_blocks * (uint32_t)64U;
         687                 :          0 :     uint32_t data2_len = len - diff - data1_len;
         688                 :          0 :     uint8_t *data11 = data2;
         689                 :          0 :     uint8_t *data21 = data2 + data1_len;
         690                 :          0 :     sha256_update_nblocks(data1_len, data11, block_state1);
         691                 :          0 :     uint8_t *dst = buf;
         692                 :          0 :     memcpy(dst, data21, data2_len * sizeof (uint8_t));
         693                 :            :     *p
         694                 :          0 :     =
         695                 :            :       (
         696                 :            :         (Hacl_Streaming_MD_state_32){
         697                 :            :           .block_state = block_state1,
         698                 :            :           .buf = buf,
         699                 :          0 :           .total_len = total_len1 + (uint64_t)(len - diff)
         700                 :            :         }
         701                 :            :       );
         702                 :            :   }
         703                 :          0 :   return (uint32_t)0U;
         704                 :            : }
         705                 :            :
         706                 :            : /**
         707                 :            : Feed an arbitrary amount of data into the hash. This function returns 0 for
         708                 :            : success, or 1 if the combined length of all of the data passed to `update_256`
         709                 :            : (since the last call to `init_256`) exceeds 2^61-1 bytes.
         710                 :            :
         711                 :            : This function is identical to the update function for SHA2_224.
         712                 :            : */
         713                 :            : uint32_t
         714                 :          0 : Hacl_Streaming_SHA2_update_256(
         715                 :            :   Hacl_Streaming_MD_state_32 *p,
         716                 :            :   uint8_t *input,
         717                 :            :   uint32_t input_len
         718                 :            : )
         719                 :            : {
         720                 :          0 :   return update_224_256(p, input, input_len);
         721                 :            : }
         722                 :            :
         723                 :            : /**
         724                 :            : Write the resulting hash into `dst`, an array of 32 bytes. The state remains
         725                 :            : valid after a call to `finish_256`, meaning the user may feed more data into
         726                 :            : the hash via `update_256`. (The finish_256 function operates on an internal copy of
         727                 :            : the state and therefore does not invalidate the client-held state `p`.)
         728                 :            : */
         729                 :          0 : void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst)
         730                 :            : {
         731                 :          0 :   Hacl_Streaming_MD_state_32 scrut = *p;
         732                 :          0 :   uint32_t *block_state = scrut.block_state;
         733                 :          0 :   uint8_t *buf_ = scrut.buf;
         734                 :          0 :   uint64_t total_len = scrut.total_len;
         735                 :            :   uint32_t r;
         736   [ #  #  #  # ]:          0 :   if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
         737                 :            :   {
         738                 :          0 :     r = (uint32_t)64U;
         739                 :            :   }
         740                 :            :   else
         741                 :            :   {
         742                 :          0 :     r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U);
         743                 :            :   }
         744                 :          0 :   uint8_t *buf_1 = buf_;
         745                 :          0 :   uint32_t tmp_block_state[8U] = { 0U };
         746                 :          0 :   memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint32_t));
         747                 :            :   uint32_t ite;
         748   [ #  #  #  # ]:          0 :   if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U)
         749                 :            :   {
         750                 :          0 :     ite = (uint32_t)64U;
         751                 :            :   }
         752                 :            :   else
         753                 :            :   {
         754                 :          0 :     ite = r % (uint32_t)64U;
         755                 :            :   }
         756                 :          0 :   uint8_t *buf_last = buf_1 + r - ite;
         757                 :          0 :   uint8_t *buf_multi = buf_1;
         758                 :          0 :   sha256_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
         759                 :          0 :   uint64_t prev_len_last = total_len - (uint64_t)r;
         760                 :          0 :   sha256_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state);
         761                 :          0 :   sha256_finish(tmp_block_state, dst);
         762                 :          0 : }
         763                 :            :
         764                 :            : /**
         765                 :            : Free a state allocated with `create_in_256`.
         766                 :            :
         767                 :            : This function is identical to the free function for SHA2_224.
         768                 :            : */
         769                 :          0 : void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s)
         770                 :            : {
         771                 :          0 :   Hacl_Streaming_MD_state_32 scrut = *s;
         772                 :          0 :   uint8_t *buf = scrut.buf;
         773                 :          0 :   uint32_t *block_state = scrut.block_state;
         774                 :          0 :   KRML_HOST_FREE(block_state);
         775                 :          0 :   KRML_HOST_FREE(buf);
         776                 :          0 :   KRML_HOST_FREE(s);
         777                 :          0 : }
         778                 :            :
         779                 :            : /**
         780                 :            : Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes.
         781                 :            : */
         782                 :          0 : void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst)
         783                 :            : {
         784                 :          0 :   uint8_t *ib = input;
         785                 :          0 :   uint8_t *rb = dst;
         786                 :          0 :   uint32_t st[8U] = { 0U };
         787                 :          0 :   sha256_init(st);
         788                 :          0 :   uint32_t rem = input_len % (uint32_t)64U;
         789                 :          0 :   uint64_t len_ = (uint64_t)input_len;
         790                 :          0 :   sha256_update_nblocks(input_len, ib, st);
         791                 :          0 :   uint32_t rem1 = input_len % (uint32_t)64U;
         792                 :          0 :   uint8_t *b0 = ib;
         793                 :          0 :   uint8_t *lb = b0 + input_len - rem1;
         794                 :          0 :   sha256_update_last(len_, rem, lb, st);
         795                 :          0 :   sha256_finish(st, rb);
         796                 :          0 : }
         797                 :            :
         798                 :          0 : Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void)
         799                 :            : {
         800                 :          0 :   uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint8_t));
         801                 :          0 :   uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint32_t));
         802                 :            :   Hacl_Streaming_MD_state_32
         803                 :          0 :   s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
         804                 :            :   Hacl_Streaming_MD_state_32
         805                 :          0 :   *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
         806                 :          0 :   p[0U] = s;
         807                 :          0 :   sha224_init(block_state);
         808                 :          0 :   return p;
         809                 :            : }
         810                 :            :
         811                 :          0 : void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s)
         812                 :            : {
         813                 :          0 :   Hacl_Streaming_MD_state_32 scrut = *s;
         814                 :          0 :   uint8_t *buf = scrut.buf;
         815                 :          0 :   uint32_t *block_state = scrut.block_state;
         816                 :          0 :   sha224_init(block_state);
         817                 :            :   Hacl_Streaming_MD_state_32
         818                 :          0 :   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
         819                 :          0 :   s[0U] = tmp;
         820                 :          0 : }
         821                 :            :
         822                 :            : uint32_t
         823                 :          0 : Hacl_Streaming_SHA2_update_224(
         824                 :            :   Hacl_Streaming_MD_state_32 *p,
         825                 :            :   uint8_t *input,
         826                 :            :   uint32_t input_len
         827                 :            : )
         828                 :            : {
         829                 :          0 :   return update_224_256(p, input, input_len);
         830                 :            : }
         831                 :            :
         832                 :            : /**
         833                 :            : Write the resulting hash into `dst`, an array of 28 bytes. The state remains
         834                 :            : valid after a call to `finish_224`, meaning the user may feed more data into
         835                 :            : the hash via `update_224`.
         836                 :            : */
         837                 :          0 : void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst)
         838                 :            : {
         839                 :          0 :   Hacl_Streaming_MD_state_32 scrut = *p;
         840                 :          0 :   uint32_t *block_state = scrut.block_state;
         841                 :          0 :   uint8_t *buf_ = scrut.buf;
         842                 :          0 :   uint64_t total_len = scrut.total_len;
         843                 :            :   uint32_t r;
         844   [ #  #  #  # ]:          0 :   if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
         845                 :            :   {
         846                 :          0 :     r = (uint32_t)64U;
         847                 :            :   }
         848                 :            :   else
         849                 :            :   {
         850                 :          0 :     r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U);
         851                 :            :   }
         852                 :          0 :   uint8_t *buf_1 = buf_;
         853                 :          0 :   uint32_t tmp_block_state[8U] = { 0U };
         854                 :          0 :   memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint32_t));
         855                 :            :   uint32_t ite;
         856   [ #  #  #  # ]:          0 :   if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U)
         857                 :            :   {
         858                 :          0 :     ite = (uint32_t)64U;
         859                 :            :   }
         860                 :            :   else
         861                 :            :   {
         862                 :          0 :     ite = r % (uint32_t)64U;
         863                 :            :   }
         864                 :          0 :   uint8_t *buf_last = buf_1 + r - ite;
         865                 :          0 :   uint8_t *buf_multi = buf_1;
         866                 :          0 :   sha224_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
         867                 :          0 :   uint64_t prev_len_last = total_len - (uint64_t)r;
         868                 :          0 :   sha224_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state);
         869                 :          0 :   sha224_finish(tmp_block_state, dst);
         870                 :          0 : }
         871                 :            :
         872                 :          0 : void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p)
         873                 :            : {
         874                 :          0 :   Hacl_Streaming_SHA2_free_256(p);
         875                 :          0 : }
         876                 :            :
         877                 :            : /**
         878                 :            : Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes.
         879                 :            : */
         880                 :          0 : void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst)
         881                 :            : {
         882                 :          0 :   uint8_t *ib = input;
         883                 :          0 :   uint8_t *rb = dst;
         884                 :          0 :   uint32_t st[8U] = { 0U };
         885                 :          0 :   sha224_init(st);
         886                 :          0 :   uint32_t rem = input_len % (uint32_t)64U;
         887                 :          0 :   uint64_t len_ = (uint64_t)input_len;
         888                 :          0 :   sha224_update_nblocks(input_len, ib, st);
         889                 :          0 :   uint32_t rem1 = input_len % (uint32_t)64U;
         890                 :          0 :   uint8_t *b0 = ib;
         891                 :          0 :   uint8_t *lb = b0 + input_len - rem1;
         892                 :          0 :   sha224_update_last(len_, rem, lb, st);
         893                 :          0 :   sha224_finish(st, rb);
         894                 :          0 : }
         895                 :            :
         896                 :          0 : Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void)
         897                 :            : {
         898                 :          0 :   uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t));
         899                 :          0 :   uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t));
         900                 :            :   Hacl_Streaming_MD_state_64
         901                 :          0 :   s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
         902                 :            :   Hacl_Streaming_MD_state_64
         903                 :          0 :   *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
         904                 :          0 :   p[0U] = s;
         905                 :          0 :   Hacl_SHA2_Scalar32_sha512_init(block_state);
         906                 :          0 :   return p;
         907                 :            : }
         908                 :            :
         909                 :            : /**
         910                 :            : Copies the state passed as argument into a newly allocated state (deep copy).
         911                 :            : The state is to be freed by calling `free_512`. Cloning the state this way is
         912                 :            : useful, for instance, if your control-flow diverges and you need to feed
         913                 :            : more (different) data into the hash in each branch.
         914                 :            : */
         915                 :          0 : Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0)
         916                 :            : {
         917                 :          0 :   Hacl_Streaming_MD_state_64 scrut = *s0;
         918                 :          0 :   uint64_t *block_state0 = scrut.block_state;
         919                 :          0 :   uint8_t *buf0 = scrut.buf;
         920                 :          0 :   uint64_t total_len0 = scrut.total_len;
         921                 :          0 :   uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t));
         922                 :          0 :   memcpy(buf, buf0, (uint32_t)128U * sizeof (uint8_t));
         923                 :          0 :   uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t));
         924                 :          0 :   memcpy(block_state, block_state0, (uint32_t)8U * sizeof (uint64_t));
         925                 :            :   Hacl_Streaming_MD_state_64
         926                 :          0 :   s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
         927                 :            :   Hacl_Streaming_MD_state_64
         928                 :          0 :   *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
         929                 :          0 :   p[0U] = s;
         930                 :          0 :   return p;
         931                 :            : }
         932                 :            :
         933                 :          0 : void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s)
         934                 :            : {
         935                 :          0 :   Hacl_Streaming_MD_state_64 scrut = *s;
         936                 :          0 :   uint8_t *buf = scrut.buf;
         937                 :          0 :   uint64_t *block_state = scrut.block_state;
         938                 :          0 :   Hacl_SHA2_Scalar32_sha512_init(block_state);
         939                 :            :   Hacl_Streaming_MD_state_64
         940                 :          0 :   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
         941                 :          0 :   s[0U] = tmp;
         942                 :          0 : }
         943                 :            :
         944                 :            : static inline uint32_t
         945                 :          0 : update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
         946                 :            : {
         947                 :          0 :   Hacl_Streaming_MD_state_64 s = *p;
         948                 :          0 :   uint64_t total_len = s.total_len;
         949         [ #  # ]:          0 :   if ((uint64_t)len > (uint64_t)18446744073709551615U - total_len)
         950                 :            :   {
         951                 :          0 :     return (uint32_t)1U;
         952                 :            :   }
         953                 :            :   uint32_t sz;
         954   [ #  #  #  # ]:          0 :   if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U)
         955                 :            :   {
         956                 :          0 :     sz = (uint32_t)128U;
         957                 :            :   }
         958                 :            :   else
         959                 :            :   {
         960                 :          0 :     sz = (uint32_t)(total_len % (uint64_t)(uint32_t)128U);
         961                 :            :   }
         962         [ #  # ]:          0 :   if (len <= (uint32_t)128U - sz)
         963                 :            :   {
         964                 :          0 :     Hacl_Streaming_MD_state_64 s1 = *p;
         965                 :          0 :     uint64_t *block_state1 = s1.block_state;
         966                 :          0 :     uint8_t *buf = s1.buf;
         967                 :          0 :     uint64_t total_len1 = s1.total_len;
         968                 :            :     uint32_t sz1;
         969   [ #  #  #  # ]:          0 :     if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U)
         970                 :            :     {
         971                 :          0 :       sz1 = (uint32_t)128U;
         972                 :            :     }
         973                 :            :     else
         974                 :            :     {
         975                 :          0 :       sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U);
         976                 :            :     }
         977                 :          0 :     uint8_t *buf2 = buf + sz1;
         978                 :          0 :     memcpy(buf2, data, len * sizeof (uint8_t));
         979                 :          0 :     uint64_t total_len2 = total_len1 + (uint64_t)len;
         980                 :            :     *p
         981                 :          0 :     =
         982                 :            :       (
         983                 :            :         (Hacl_Streaming_MD_state_64){
         984                 :            :           .block_state = block_state1,
         985                 :            :           .buf = buf,
         986                 :            :           .total_len = total_len2
         987                 :            :         }
         988                 :            :       );
         989                 :            :   }
         990         [ #  # ]:          0 :   else if (sz == (uint32_t)0U)
         991                 :            :   {
         992                 :          0 :     Hacl_Streaming_MD_state_64 s1 = *p;
         993                 :          0 :     uint64_t *block_state1 = s1.block_state;
         994                 :          0 :     uint8_t *buf = s1.buf;
         995                 :          0 :     uint64_t total_len1 = s1.total_len;
         996                 :            :     uint32_t sz1;
         997   [ #  #  #  # ]:          0 :     if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U)
         998                 :            :     {
         999                 :          0 :       sz1 = (uint32_t)128U;
        1000                 :            :     }
        1001                 :            :     else
        1002                 :            :     {
        1003                 :          0 :       sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U);
        1004                 :            :     }
        1005         [ #  # ]:          0 :     if (!(sz1 == (uint32_t)0U))
        1006                 :            :     {
        1007                 :          0 :       sha512_update_nblocks((uint32_t)128U, buf, block_state1);
        1008                 :            :     }
        1009                 :            :     uint32_t ite;
        1010   [ #  #  #  # ]:          0 :     if ((uint64_t)len % (uint64_t)(uint32_t)128U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U)
        1011                 :            :     {
        1012                 :          0 :       ite = (uint32_t)128U;
        1013                 :            :     }
        1014                 :            :     else
        1015                 :            :     {
        1016                 :          0 :       ite = (uint32_t)((uint64_t)len % (uint64_t)(uint32_t)128U);
        1017                 :            :     }
        1018                 :          0 :     uint32_t n_blocks = (len - ite) / (uint32_t)128U;
        1019                 :          0 :     uint32_t data1_len = n_blocks * (uint32_t)128U;
        1020                 :          0 :     uint32_t data2_len = len - data1_len;
        1021                 :          0 :     uint8_t *data1 = data;
        1022                 :          0 :     uint8_t *data2 = data + data1_len;
        1023                 :          0 :     sha512_update_nblocks(data1_len, data1, block_state1);
        1024                 :          0 :     uint8_t *dst = buf;
        1025                 :          0 :     memcpy(dst, data2, data2_len * sizeof (uint8_t));
        1026                 :            :     *p
        1027                 :          0 :     =
        1028                 :            :       (
        1029                 :            :         (Hacl_Streaming_MD_state_64){
        1030                 :            :           .block_state = block_state1,
        1031                 :            :           .buf = buf,
        1032                 :          0 :           .total_len = total_len1 + (uint64_t)len
        1033                 :            :         }
        1034                 :            :       );
        1035                 :            :   }
        1036                 :            :   else
        1037                 :            :   {
        1038                 :          0 :     uint32_t diff = (uint32_t)128U - sz;
        1039                 :          0 :     uint8_t *data1 = data;
        1040                 :          0 :     uint8_t *data2 = data + diff;
        1041                 :          0 :     Hacl_Streaming_MD_state_64 s1 = *p;
        1042                 :          0 :     uint64_t *block_state10 = s1.block_state;
        1043                 :          0 :     uint8_t *buf0 = s1.buf;
        1044                 :          0 :     uint64_t total_len10 = s1.total_len;
        1045                 :            :     uint32_t sz10;
        1046   [ #  #  #  # ]:          0 :     if (total_len10 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len10 > (uint64_t)0U)
        1047                 :            :     {
        1048                 :          0 :       sz10 = (uint32_t)128U;
        1049                 :            :     }
        1050                 :            :     else
        1051                 :            :     {
        1052                 :          0 :       sz10 = (uint32_t)(total_len10 % (uint64_t)(uint32_t)128U);
        1053                 :            :     }
        1054                 :          0 :     uint8_t *buf2 = buf0 + sz10;
        1055                 :          0 :     memcpy(buf2, data1, diff * sizeof (uint8_t));
        1056                 :          0 :     uint64_t total_len2 = total_len10 + (uint64_t)diff;
        1057                 :            :     *p
        1058                 :          0 :     =
        1059                 :            :       (
        1060                 :            :         (Hacl_Streaming_MD_state_64){
        1061                 :            :           .block_state = block_state10,
        1062                 :            :           .buf = buf0,
        1063                 :            :           .total_len = total_len2
        1064                 :            :         }
        1065                 :            :       );
        1066                 :          0 :     Hacl_Streaming_MD_state_64 s10 = *p;
        1067                 :          0 :     uint64_t *block_state1 = s10.block_state;
        1068                 :          0 :     uint8_t *buf = s10.buf;
        1069                 :          0 :     uint64_t total_len1 = s10.total_len;
        1070                 :            :     uint32_t sz1;
        1071   [ #  #  #  # ]:          0 :     if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len1 > (uint64_t)0U)
        1072                 :            :     {
        1073                 :          0 :       sz1 = (uint32_t)128U;
        1074                 :            :     }
        1075                 :            :     else
        1076                 :            :     {
        1077                 :          0 :       sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U);
        1078                 :            :     }
        1079         [ #  # ]:          0 :     if (!(sz1 == (uint32_t)0U))
        1080                 :            :     {
        1081                 :          0 :       sha512_update_nblocks((uint32_t)128U, buf, block_state1);
        1082                 :            :     }
        1083                 :            :     uint32_t ite;
        1084                 :            :     if
        1085                 :          0 :     (
        1086                 :          0 :       (uint64_t)(len - diff)
        1087                 :            :       % (uint64_t)(uint32_t)128U
        1088         [ #  # ]:          0 :       == (uint64_t)0U
        1089         [ #  # ]:          0 :       && (uint64_t)(len - diff) > (uint64_t)0U
        1090                 :            :     )
        1091                 :            :     {
        1092                 :          0 :       ite = (uint32_t)128U;
        1093                 :            :     }
        1094                 :            :     else
        1095                 :            :     {
        1096                 :          0 :       ite = (uint32_t)((uint64_t)(len - diff) % (uint64_t)(uint32_t)128U);
        1097                 :            :     }
        1098                 :          0 :     uint32_t n_blocks = (len - diff - ite) / (uint32_t)128U;
        1099                 :          0 :     uint32_t data1_len = n_blocks * (uint32_t)128U;
        1100                 :          0 :     uint32_t data2_len = len - diff - data1_len;
        1101                 :          0 :     uint8_t *data11 = data2;
        1102                 :          0 :     uint8_t *data21 = data2 + data1_len;
        1103                 :          0 :     sha512_update_nblocks(data1_len, data11, block_state1);
        1104                 :          0 :     uint8_t *dst = buf;
        1105                 :          0 :     memcpy(dst, data21, data2_len * sizeof (uint8_t));
        1106                 :            :     *p
        1107                 :          0 :     =
        1108                 :            :       (
        1109                 :            :         (Hacl_Streaming_MD_state_64){
        1110                 :            :           .block_state = block_state1,
        1111                 :            :           .buf = buf,
        1112                 :          0 :           .total_len = total_len1 + (uint64_t)(len - diff)
        1113                 :            :         }
        1114                 :            :       );
        1115                 :            :   }
        1116                 :          0 :   return (uint32_t)0U;
        1117                 :            : }
        1118                 :            :
        1119                 :            : /**
        1120                 :            : Feed an arbitrary amount of data into the hash. This function returns 0 for
        1121                 :            : success, or 1 if the combined length of all of the data passed to `update_512`
        1122                 :            : (since the last call to `init_512`) exceeds 2^125-1 bytes.
        1123                 :            :
        1124                 :            : This function is identical to the update function for SHA2_384.
        1125                 :            : */
        1126                 :            : uint32_t
        1127                 :          0 : Hacl_Streaming_SHA2_update_512(
        1128                 :            :   Hacl_Streaming_MD_state_64 *p,
        1129                 :            :   uint8_t *input,
        1130                 :            :   uint32_t input_len
        1131                 :            : )
        1132                 :            : {
        1133                 :          0 :   return update_384_512(p, input, input_len);
        1134                 :            : }
        1135                 :            :
        1136                 :            : /**
        1137                 :            : Write the resulting hash into `dst`, an array of 64 bytes. The state remains
        1138                 :            : valid after a call to `finish_512`, meaning the user may feed more data into
        1139                 :            : the hash via `update_512`. (The finish_512 function operates on an internal copy of
        1140                 :            : the state and therefore does not invalidate the client-held state `p`.)
        1141                 :            : */
        1142                 :          0 : void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst)
        1143                 :            : {
        1144                 :          0 :   Hacl_Streaming_MD_state_64 scrut = *p;
        1145                 :          0 :   uint64_t *block_state = scrut.block_state;
        1146                 :          0 :   uint8_t *buf_ = scrut.buf;
        1147                 :          0 :   uint64_t total_len = scrut.total_len;
        1148                 :            :   uint32_t r;
        1149   [ #  #  #  # ]:          0 :   if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U)
        1150                 :            :   {
        1151                 :          0 :     r = (uint32_t)128U;
        1152                 :            :   }
        1153                 :            :   else
        1154                 :            :   {
        1155                 :          0 :     r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U);
        1156                 :            :   }
        1157                 :          0 :   uint8_t *buf_1 = buf_;
        1158                 :          0 :   uint64_t tmp_block_state[8U] = { 0U };
        1159                 :          0 :   memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint64_t));
        1160                 :            :   uint32_t ite;
        1161   [ #  #  #  # ]:          0 :   if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U)
        1162                 :            :   {
        1163                 :          0 :     ite = (uint32_t)128U;
        1164                 :            :   }
        1165                 :            :   else
        1166                 :            :   {
        1167                 :          0 :     ite = r % (uint32_t)128U;
        1168                 :            :   }
        1169                 :          0 :   uint8_t *buf_last = buf_1 + r - ite;
        1170                 :          0 :   uint8_t *buf_multi = buf_1;
        1171                 :          0 :   sha512_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
        1172                 :          0 :   uint64_t prev_len_last = total_len - (uint64_t)r;
        1173                 :          0 :   sha512_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last),
        1174                 :            :       FStar_UInt128_uint64_to_uint128((uint64_t)r)),
        1175                 :            :     r,
        1176                 :            :     buf_last,
        1177                 :            :     tmp_block_state);
        1178                 :          0 :   sha512_finish(tmp_block_state, dst);
        1179                 :          0 : }
        1180                 :            :
        1181                 :            : /**
        1182                 :            : Free a state allocated with `create_in_512`.
        1183                 :            :
        1184                 :            : This function is identical to the free function for SHA2_384.
        1185                 :            : */
        1186                 :          0 : void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s)
        1187                 :            : {
        1188                 :          0 :   Hacl_Streaming_MD_state_64 scrut = *s;
        1189                 :          0 :   uint8_t *buf = scrut.buf;
        1190                 :          0 :   uint64_t *block_state = scrut.block_state;
        1191                 :          0 :   KRML_HOST_FREE(block_state);
        1192                 :          0 :   KRML_HOST_FREE(buf);
        1193                 :          0 :   KRML_HOST_FREE(s);
        1194                 :          0 : }
        1195                 :            :
        1196                 :            : /**
        1197                 :            : Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes.
        1198                 :            : */
        1199                 :          0 : void Hacl_Streaming_SHA2_sha512(uint8_t *input, uint32_t input_len, uint8_t *dst)
        1200                 :            : {
        1201                 :          0 :   uint8_t *ib = input;
        1202                 :          0 :   uint8_t *rb = dst;
        1203                 :          0 :   uint64_t st[8U] = { 0U };
        1204                 :          0 :   Hacl_SHA2_Scalar32_sha512_init(st);
        1205                 :          0 :   uint32_t rem = input_len % (uint32_t)128U;
        1206                 :          0 :   FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len);
        1207                 :          0 :   sha512_update_nblocks(input_len, ib, st);
        1208                 :          0 :   uint32_t rem1 = input_len % (uint32_t)128U;
        1209                 :          0 :   uint8_t *b0 = ib;
        1210                 :          0 :   uint8_t *lb = b0 + input_len - rem1;
        1211                 :          0 :   sha512_update_last(len_, rem, lb, st);
        1212                 :          0 :   sha512_finish(st, rb);
        1213                 :          0 : }
        1214                 :            :
        1215                 :          0 : Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void)
        1216                 :            : {
        1217                 :          0 :   uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC((uint32_t)128U, sizeof (uint8_t));
        1218                 :          0 :   uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC((uint32_t)8U, sizeof (uint64_t));
        1219                 :            :   Hacl_Streaming_MD_state_64
        1220                 :          0 :   s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
        1221                 :            :   Hacl_Streaming_MD_state_64
        1222                 :          0 :   *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
        1223                 :          0 :   p[0U] = s;
        1224                 :          0 :   sha384_init(block_state);
        1225                 :          0 :   return p;
        1226                 :            : }
        1227                 :            :
        1228                 :          0 : void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s)
        1229                 :            : {
        1230                 :          0 :   Hacl_Streaming_MD_state_64 scrut = *s;
        1231                 :          0 :   uint8_t *buf = scrut.buf;
        1232                 :          0 :   uint64_t *block_state = scrut.block_state;
        1233                 :          0 :   sha384_init(block_state);
        1234                 :            :   Hacl_Streaming_MD_state_64
        1235                 :          0 :   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
        1236                 :          0 :   s[0U] = tmp;
        1237                 :          0 : }
        1238                 :            :
        1239                 :            : uint32_t
        1240                 :          0 : Hacl_Streaming_SHA2_update_384(
        1241                 :            :   Hacl_Streaming_MD_state_64 *p,
        1242                 :            :   uint8_t *input,
        1243                 :            :   uint32_t input_len
        1244                 :            : )
        1245                 :            : {
        1246                 :          0 :   return update_384_512(p, input, input_len);
        1247                 :            : }
        1248                 :            :
        1249                 :            : /**
        1250                 :            : Write the resulting hash into `dst`, an array of 48 bytes. The state remains
        1251                 :            : valid after a call to `finish_384`, meaning the user may feed more data into
        1252                 :            : the hash via `update_384`.
        1253                 :            : */
        1254                 :          0 : void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst)
        1255                 :            : {
        1256                 :          0 :   Hacl_Streaming_MD_state_64 scrut = *p;
        1257                 :          0 :   uint64_t *block_state = scrut.block_state;
        1258                 :          0 :   uint8_t *buf_ = scrut.buf;
        1259                 :          0 :   uint64_t total_len = scrut.total_len;
        1260                 :            :   uint32_t r;
        1261   [ #  #  #  # ]:          0 :   if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U)
        1262                 :            :   {
        1263                 :          0 :     r = (uint32_t)128U;
        1264                 :            :   }
        1265                 :            :   else
        1266                 :            :   {
        1267                 :          0 :     r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U);
        1268                 :            :   }
        1269                 :          0 :   uint8_t *buf_1 = buf_;
        1270                 :          0 :   uint64_t tmp_block_state[8U] = { 0U };
        1271                 :          0 :   memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof (uint64_t));
        1272                 :            :   uint32_t ite;
        1273   [ #  #  #  # ]:          0 :   if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U)
        1274                 :            :   {
        1275                 :          0 :     ite = (uint32_t)128U;
        1276                 :            :   }
        1277                 :            :   else
        1278                 :            :   {
        1279                 :          0 :     ite = r % (uint32_t)128U;
        1280                 :            :   }
        1281                 :          0 :   uint8_t *buf_last = buf_1 + r - ite;
        1282                 :          0 :   uint8_t *buf_multi = buf_1;
        1283                 :          0 :   sha384_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
        1284                 :          0 :   uint64_t prev_len_last = total_len - (uint64_t)r;
        1285                 :          0 :   sha384_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last),
        1286                 :            :       FStar_UInt128_uint64_to_uint128((uint64_t)r)),
        1287                 :            :     r,
        1288                 :            :     buf_last,
        1289                 :            :     tmp_block_state);
        1290                 :          0 :   sha384_finish(tmp_block_state, dst);
        1291                 :          0 : }
        1292                 :            :
        1293                 :          0 : void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p)
        1294                 :            : {
        1295                 :          0 :   Hacl_Streaming_SHA2_free_512(p);
        1296                 :          0 : }
        1297                 :            :
        1298                 :            : /**
        1299                 :            : Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes.
        1300                 :            : */
        1301                 :          0 : void Hacl_Streaming_SHA2_sha384(uint8_t *input, uint32_t input_len, uint8_t *dst)
        1302                 :            : {
        1303                 :          0 :   uint8_t *ib = input;
        1304                 :          0 :   uint8_t *rb = dst;
        1305                 :          0 :   uint64_t st[8U] = { 0U };
        1306                 :          0 :   sha384_init(st);
        1307                 :          0 :   uint32_t rem = input_len % (uint32_t)128U;
        1308                 :          0 :   FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len);
        1309                 :          0 :   sha384_update_nblocks(input_len, ib, st);
        1310                 :          0 :   uint32_t rem1 = input_len % (uint32_t)128U;
        1311                 :          0 :   uint8_t *b0 = ib;
        1312                 :          0 :   uint8_t *lb = b0 + input_len - rem1;
        1313                 :          0 :   sha384_update_last(len_, rem, lb, st);
        1314                 :          0 :   sha384_finish(st, rb);
        1315                 :          0 : }
        1316                 :            :

Generated by: LCOV version 1.14