update to HACL* 2706a814a711b62e5b0e271b2c3c8696a6239663

cryspen · Nov 7, 2023 · 09d121e · 09d121e
1 parent dfdf26a
commit 09d121e
Show file tree

Hide file tree

Showing 22 changed files with 188 additions and 194 deletions.
diff --git a/benchmarks/sha3.cc b/benchmarks/sha3.cc
@@ -27,7 +27,7 @@ static void
 Hacl_Sha3_224(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_sha3_224(input.size(), (uint8_t*)input.data(), digest224.data());
+    Hacl_Hash_SHA3_sha3_224(digest224.data(), (uint8_t*)input.data(), input.size());
   }
   if (digest224 != expected_digest_sha3_224) {
     state.SkipWithError("Incorrect digest.");
@@ -51,7 +51,7 @@ static void
 Hacl_Sha3_256(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_sha3_256(input.size(), (uint8_t*)input.data(), digest256.data());
+    Hacl_Hash_SHA3_sha3_256(digest256.data(), (uint8_t*)input.data(), input.size());
   }
   if (digest256 != expected_digest_sha3_256) {
     state.SkipWithError("Incorrect digest.");
@@ -102,7 +102,7 @@ static void
 Hacl_Sha3_384(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_sha3_384(input.size(), (uint8_t*)input.data(), digest384.data());
+    Hacl_Hash_SHA3_sha3_384(digest384.data(), (uint8_t*)input.data(), input.size());
   }
   if (digest384 != expected_digest_sha3_384) {
     state.SkipWithError("Incorrect digest.");
@@ -126,7 +126,7 @@ static void
 Hacl_Sha3_512(benchmark::State& state)
 {
   for (auto _ : state) {
-    Hacl_Hash_SHA3_sha3_512(input.size(), (uint8_t*)input.data(), digest512.data());
+    Hacl_Hash_SHA3_sha3_512(digest512.data(), (uint8_t*)input.data(), input.size());
   }
   if (digest512 != expected_digest_sha3_512) {
     state.SkipWithError("Incorrect digest.");

diff --git a/include/Hacl_AEAD_Chacha20Poly1305.h b/include/Hacl_AEAD_Chacha20Poly1305.h
@@ -65,23 +65,22 @@ Hacl_AEAD_Chacha20Poly1305_encrypt(
 );
 
 /**
-Decrypt a ciphertext `cipher` with key `k`.
+Decrypt a ciphertext `input` with key `key`.
 
-The arguments `k`, `n`, `aadlen`, and `aad` are same in encryption/decryption.
-Note: Encryption and decryption can be executed in-place, i.e., `m` and `cipher` can point to the same memory.
-
-If decryption succeeds, the resulting plaintext is stored in `m` and the function returns the success code 0.
-If decryption fails, the array `m` remains unchanged and the function returns the error code 1.
+The arguments `key`, `nonce`, `data`, and `data_len` are same in encryption/decryption.
+Note: Encryption and decryption can be executed in-place, i.e., `output` and `input` can point to the same memory.
 
-@param k Pointer to 32 bytes of memory where the AEAD key is read from.
-@param n Pointer to 12 bytes of memory where the AEAD nonce is read from.
-@param aadlen Length of the associated data.
-@param aad Pointer to `aadlen` bytes of memory where the associated data is read from.
+If decryption succeeds, the resulting plaintext is stored in `output` and the function returns the success code 0.
+If decryption fails, the array `output` remains unchanged and the function returns the error code 1.
 
-@param mlen Length of the ciphertext.
-@param m Pointer to `mlen` bytes of memory where the message is written to.
-@param cipher Pointer to `mlen` bytes of memory where the ciphertext is read from.
-@param mac Pointer to 16 bytes of memory where the mac is read from.
+@param output Pointer to `input_len` bytes of memory where the message is written to.
+@param input Pointer to `input_len` bytes of memory where the ciphertext is read from.
+@param input_len Length of the ciphertext.
+@param data Pointer to `data_len` bytes of memory where the associated data is read from.
+@param data_len Length of the associated data.
+@param key Pointer to 32 bytes of memory where the AEAD key is read from.
+@param nonce Pointer to 12 bytes of memory where the AEAD nonce is read from.
+@param tag Pointer to 16 bytes of memory where the mac is read from.
 
 @returns 0 on succeess; 1 on failure.
 */

diff --git a/include/Hacl_Hash_SHA3.h b/include/Hacl_Hash_SHA3.h
@@ -93,13 +93,13 @@ Hacl_Hash_SHA3_shake256_hacl(
   uint8_t *output
 );
 
-void Hacl_Hash_SHA3_sha3_224(uint32_t inputByteLen, uint8_t *input, uint8_t *output);
+void Hacl_Hash_SHA3_sha3_224(uint8_t *output, uint8_t *input, uint32_t input_len);
 
-void Hacl_Hash_SHA3_sha3_256(uint32_t inputByteLen, uint8_t *input, uint8_t *output);
+void Hacl_Hash_SHA3_sha3_256(uint8_t *output, uint8_t *input, uint32_t input_len);
 
-void Hacl_Hash_SHA3_sha3_384(uint32_t inputByteLen, uint8_t *input, uint8_t *output);
+void Hacl_Hash_SHA3_sha3_384(uint8_t *output, uint8_t *input, uint32_t input_len);
 
-void Hacl_Hash_SHA3_sha3_512(uint32_t inputByteLen, uint8_t *input, uint8_t *output);
+void Hacl_Hash_SHA3_sha3_512(uint8_t *output, uint8_t *input, uint32_t input_len);
 
 void Hacl_Hash_SHA3_absorb_inner(uint32_t rateInBytes, uint8_t *block, uint64_t *s);
 

diff --git a/include/msvc/Hacl_AEAD_Chacha20Poly1305.h b/include/msvc/Hacl_AEAD_Chacha20Poly1305.h
@@ -65,23 +65,22 @@ Hacl_AEAD_Chacha20Poly1305_encrypt(
 );
 
 /**
-Decrypt a ciphertext `cipher` with key `k`.
+Decrypt a ciphertext `input` with key `key`.
 
-The arguments `k`, `n`, `aadlen`, and `aad` are same in encryption/decryption.
-Note: Encryption and decryption can be executed in-place, i.e., `m` and `cipher` can point to the same memory.
-
-If decryption succeeds, the resulting plaintext is stored in `m` and the function returns the success code 0.
-If decryption fails, the array `m` remains unchanged and the function returns the error code 1.
+The arguments `key`, `nonce`, `data`, and `data_len` are same in encryption/decryption.
+Note: Encryption and decryption can be executed in-place, i.e., `output` and `input` can point to the same memory.
 
-@param k Pointer to 32 bytes of memory where the AEAD key is read from.
-@param n Pointer to 12 bytes of memory where the AEAD nonce is read from.
-@param aadlen Length of the associated data.
-@param aad Pointer to `aadlen` bytes of memory where the associated data is read from.
+If decryption succeeds, the resulting plaintext is stored in `output` and the function returns the success code 0.
+If decryption fails, the array `output` remains unchanged and the function returns the error code 1.
 
-@param mlen Length of the ciphertext.
-@param m Pointer to `mlen` bytes of memory where the message is written to.
-@param cipher Pointer to `mlen` bytes of memory where the ciphertext is read from.
-@param mac Pointer to 16 bytes of memory where the mac is read from.
+@param output Pointer to `input_len` bytes of memory where the message is written to.
+@param input Pointer to `input_len` bytes of memory where the ciphertext is read from.
+@param input_len Length of the ciphertext.
+@param data Pointer to `data_len` bytes of memory where the associated data is read from.
+@param data_len Length of the associated data.
+@param key Pointer to 32 bytes of memory where the AEAD key is read from.
+@param nonce Pointer to 12 bytes of memory where the AEAD nonce is read from.
+@param tag Pointer to 16 bytes of memory where the mac is read from.
 
 @returns 0 on succeess; 1 on failure.
 */

diff --git a/include/msvc/Hacl_Hash_SHA3.h b/include/msvc/Hacl_Hash_SHA3.h
@@ -93,13 +93,13 @@ Hacl_Hash_SHA3_shake256_hacl(
   uint8_t *output
 );
 
-void Hacl_Hash_SHA3_sha3_224(uint32_t inputByteLen, uint8_t *input, uint8_t *output);
+void Hacl_Hash_SHA3_sha3_224(uint8_t *output, uint8_t *input, uint32_t input_len);
 
-void Hacl_Hash_SHA3_sha3_256(uint32_t inputByteLen, uint8_t *input, uint8_t *output);
+void Hacl_Hash_SHA3_sha3_256(uint8_t *output, uint8_t *input, uint32_t input_len);
 
-void Hacl_Hash_SHA3_sha3_384(uint32_t inputByteLen, uint8_t *input, uint8_t *output);
+void Hacl_Hash_SHA3_sha3_384(uint8_t *output, uint8_t *input, uint32_t input_len);
 
-void Hacl_Hash_SHA3_sha3_512(uint32_t inputByteLen, uint8_t *input, uint8_t *output);
+void Hacl_Hash_SHA3_sha3_512(uint8_t *output, uint8_t *input, uint32_t input_len);
 
 void Hacl_Hash_SHA3_absorb_inner(uint32_t rateInBytes, uint8_t *block, uint64_t *s);
 

diff --git a/info.txt b/info.txt
@@ -1,5 +1,5 @@
 The code was generated with the following toolchain.
-F* version: f3b4db2ebce90020acbbbe1b4ea0d05d3e69ad6c
-KaRaMeL version: af4acdbe2d95d4ce09e044de52fabb39d5d09766
-HACL* version: 45b18730573d3404a57fb63767570cb97897a75f
+F* version: f4cbb7a38d67eeb13fbdb2f4fb8a44a65cbcdc1f
+Karamel version: a7be2a7c43eca637ceb57fe8f3ffd16fc6627ebd
+HACL* version: 2706a814a711b62e5b0e271b2c3c8696a6239663
 Vale version: 0.3.19
diff --git a/js/api.json b/js/api.json
@@ -644,10 +644,18 @@
       "module": "Hacl_Hash_SHA3",
       "custom_module_name": true,
       "name": "Hacl_Hash_SHA3_sha3_512",
-      "args": [{
-          "name": "input_len",
-          "kind": "input",
-          "type": "uint32"
+      "args": [
+        {
+          "name": "output",
+          "kind": "output",
+          "type": "buffer",
+          "size": 64,
+          "tests": [
+              "a69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26",
+              "b751850b1a57168a5693cd924b6b096e08f621827444f70d884f5d0240d2712e10e116e9192af3c91a7ec57647e3934057340b4cf408d5a56592f8274eec53f0",
+              "04a371e84ecfb5b8b77cb48610fca8182dd457ce6f326a0fd3d7ec2f1e91636dee691fbe0c985302ba1b0d8dc78c086346b533b49c030d99a27daf1139d6e75e",
+              "afebb2ef542e6579c50cad06d2e578f9f8dd6881d7dc824d26360feebf18a4fa73e3261122948efcfd492e74e82e2189ed0fb440d187f382270cb455f21dd185"
+          ]
         }, {
           "name": "input",
           "kind": "input",
@@ -661,17 +669,10 @@
               "61626364656667686263646566676869636465666768696a6465666768696a6b65666768696a6b6c666768696a6b6c6d6768696a6b6c6d6e68696a6b6c6d6e6f696a6b6c6d6e6f706a6b6c6d6e6f70716b6c6d6e6f7071726c6d6e6f707172736d6e6f70717273746e6f707172737475"
           ]
         }, {
-          "name": "output",
-          "kind": "output",
-          "type": "buffer",
-          "size": 64,
-          "tests": [
-              "a69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26",
-              "b751850b1a57168a5693cd924b6b096e08f621827444f70d884f5d0240d2712e10e116e9192af3c91a7ec57647e3934057340b4cf408d5a56592f8274eec53f0",
-              "04a371e84ecfb5b8b77cb48610fca8182dd457ce6f326a0fd3d7ec2f1e91636dee691fbe0c985302ba1b0d8dc78c086346b533b49c030d99a27daf1139d6e75e",
-              "afebb2ef542e6579c50cad06d2e578f9f8dd6881d7dc824d26360feebf18a4fa73e3261122948efcfd492e74e82e2189ed0fb440d187f382270cb455f21dd185"
-          ]
-        }
+          "name": "input_len",
+          "kind": "input",
+          "type": "uint32"
+	}
       ],
       "return": {
         "type": "void"
@@ -681,12 +682,19 @@
       "module": "Hacl_Hash_SHA3",
       "custom_module_name": true,
       "name": "Hacl_Hash_SHA3_sha3_384",
-      "args": [{
-          "name": "input_len",
-          "kind": "input",
-          "type": "uint32"
-        },
+      "args": [
         {
+          "name": "hash",
+          "kind": "output",
+          "type": "buffer",
+          "size": 48,
+          "tests": [
+              "0c63a75b845e4f7d01107d852e4c2485c51a50aaaa94fc61995e71bbee983a2ac3713831264adb47fb6bd1e058d5f004",
+              "ec01498288516fc926459f58e2c6ad8df9b473cb0fc08c2596da7cf0e49be4b298d88cea927ac7f539f1edf228376d25",
+              "991c665755eb3a4b6bbdfb75c78a492e8c56a22c5c4d7e429bfdbc32b9d4ad5aa04a1f076e62fea19eef51acd0657c22",
+              "79407d3b5916b59c3e30b09822974791c313fb9ecc849e406f23592d04f625dc8c709b98b43b3852b337216179aa7fc7"
+          ]
+	}, {
           "name": "input",
           "kind": "input",
           "type": "buffer",
@@ -698,18 +706,10 @@
               "6162636462636465636465666465666765666768666768696768696a68696a6b696a6b6c6a6b6c6d6b6c6d6e6c6d6e6f6d6e6f706e6f7071",
               "61626364656667686263646566676869636465666768696a6465666768696a6b65666768696a6b6c666768696a6b6c6d6768696a6b6c6d6e68696a6b6c6d6e6f696a6b6c6d6e6f706a6b6c6d6e6f70716b6c6d6e6f7071726c6d6e6f707172736d6e6f70717273746e6f707172737475"
           ]
-        },
-        {
-          "name": "hash",
-          "kind": "output",
-          "type": "buffer",
-          "size": 48,
-          "tests": [
-              "0c63a75b845e4f7d01107d852e4c2485c51a50aaaa94fc61995e71bbee983a2ac3713831264adb47fb6bd1e058d5f004",
-              "ec01498288516fc926459f58e2c6ad8df9b473cb0fc08c2596da7cf0e49be4b298d88cea927ac7f539f1edf228376d25",
-              "991c665755eb3a4b6bbdfb75c78a492e8c56a22c5c4d7e429bfdbc32b9d4ad5aa04a1f076e62fea19eef51acd0657c22",
-              "79407d3b5916b59c3e30b09822974791c313fb9ecc849e406f23592d04f625dc8c709b98b43b3852b337216179aa7fc7"
-          ]
+        }, {
+          "name": "input_len",
+          "kind": "input",
+          "type": "uint32"
         }
       ],
       "return": {
@@ -720,12 +720,19 @@
       "module": "Hacl_Hash_SHA3",
       "custom_module_name": true,
       "name": "Hacl_Hash_SHA3_sha3_256",
-      "args": [{
-          "name": "input_len",
-          "kind": "input",
-          "type": "uint32"
-        },
+      "args": [
         {
+          "name": "hash",
+          "kind": "output",
+          "type": "buffer",
+          "size": 32,
+          "tests": [
+              "a7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a",
+              "3a985da74fe225b2045c172d6bd390bd855f086e3e9d525b46bfe24511431532",
+              "41c0dba2a9d6240849100376a8235e2c82e1b9998a999e21db32dd97496d3376",
+              "916f6061fe879741ca6469b43971dfdb28b1a32dc36cb3254e812be27aad1d18"
+          ]
+        }, {
           "name": "input",
           "kind": "input",
           "type": "buffer",
@@ -737,18 +744,10 @@
               "6162636462636465636465666465666765666768666768696768696a68696a6b696a6b6c6a6b6c6d6b6c6d6e6c6d6e6f6d6e6f706e6f7071",
               "61626364656667686263646566676869636465666768696a6465666768696a6b65666768696a6b6c666768696a6b6c6d6768696a6b6c6d6e68696a6b6c6d6e6f696a6b6c6d6e6f706a6b6c6d6e6f70716b6c6d6e6f7071726c6d6e6f707172736d6e6f70717273746e6f707172737475"
           ]
-        },
-        {
-          "name": "hash",
-          "kind": "output",
-          "type": "buffer",
-          "size": 32,
-          "tests": [
-              "a7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a",
-              "3a985da74fe225b2045c172d6bd390bd855f086e3e9d525b46bfe24511431532",
-              "41c0dba2a9d6240849100376a8235e2c82e1b9998a999e21db32dd97496d3376",
-              "916f6061fe879741ca6469b43971dfdb28b1a32dc36cb3254e812be27aad1d18"
-          ]
+        },{
+          "name": "input_len",
+          "kind": "input",
+          "type": "uint32"
         }
       ],
       "return": {
@@ -759,12 +758,19 @@
       "module": "Hacl_Hash_SHA3",
       "custom_module_name": true,
       "name": "Hacl_Hash_SHA3_sha3_224",
-      "args": [{
-          "name": "input_len",
-          "kind": "input",
-          "type": "uint32"
-        },
+      "args": [
         {
+          "name": "hash",
+          "kind": "output",
+          "type": "buffer",
+          "size": 28,
+          "tests": [
+              "6b4e03423667dbb73b6e15454f0eb1abd4597f9a1b078e3f5b5a6bc7",
+              "e642824c3f8cf24ad09234ee7d3c766fc9a3a5168d0c94ad73b46fdf",
+              "8a24108b154ada21c9fd5574494479ba5c7e7ab76ef264ead0fcce33",
+              "543e6868e1666c1a643630df77367ae5a62a85070a51c14cbf665cbc"
+          ]
+        }, {
           "name": "input",
           "kind": "input",
           "type": "buffer",
@@ -776,19 +782,11 @@
               "6162636462636465636465666465666765666768666768696768696a68696a6b696a6b6c6a6b6c6d6b6c6d6e6c6d6e6f6d6e6f706e6f7071",
               "61626364656667686263646566676869636465666768696a6465666768696a6b65666768696a6b6c666768696a6b6c6d6768696a6b6c6d6e68696a6b6c6d6e6f696a6b6c6d6e6f706a6b6c6d6e6f70716b6c6d6e6f7071726c6d6e6f707172736d6e6f70717273746e6f707172737475"
           ]
-        },
-        {
-          "name": "hash",
-          "kind": "output",
-          "type": "buffer",
-          "size": 28,
-          "tests": [
-              "6b4e03423667dbb73b6e15454f0eb1abd4597f9a1b078e3f5b5a6bc7",
-              "e642824c3f8cf24ad09234ee7d3c766fc9a3a5168d0c94ad73b46fdf",
-              "8a24108b154ada21c9fd5574494479ba5c7e7ab76ef264ead0fcce33",
-              "543e6868e1666c1a643630df77367ae5a62a85070a51c14cbf665cbc"
-          ]
-        }
+        }, {
+          "name": "input_len",
+          "kind": "input",
+          "type": "uint32"
+	}
       ],
       "return": {
         "type": "void"

diff --git a/ocaml/hacl-star/Hacl.ml b/ocaml/hacl-star/Hacl.ml
@@ -103,25 +103,25 @@ end)
 module SHA3_224 : HashFunction =
   Make_HashFunction (struct
     let hash_alg = SHA3_224
-    let hash output input input_len = Hacl_Hash_SHA3.hacl_Hash_SHA3_sha3_224 input_len input output
+    let hash = Hacl_Hash_SHA3.hacl_Hash_SHA3_sha3_224
 end)
 
 module SHA3_256 : HashFunction =
   Make_HashFunction (struct
     let hash_alg = SHA3_256
-    let hash output input input_len = Hacl_Hash_SHA3.hacl_Hash_SHA3_sha3_256 input_len input output
+    let hash= Hacl_Hash_SHA3.hacl_Hash_SHA3_sha3_256
 end)
 
 module SHA3_384 : HashFunction =
   Make_HashFunction (struct
     let hash_alg = SHA3_384
-    let hash output input input_len = Hacl_Hash_SHA3.hacl_Hash_SHA3_sha3_384 input_len input output
+    let hash = Hacl_Hash_SHA3.hacl_Hash_SHA3_sha3_384
 end)
 
 module SHA3_512 : HashFunction =
   Make_HashFunction (struct
     let hash_alg = SHA3_512
-    let hash output input input_len = Hacl_Hash_SHA3.hacl_Hash_SHA3_sha3_512 input_len input output
+    let hash = Hacl_Hash_SHA3.hacl_Hash_SHA3_sha3_512
 end)
 
 module Keccak = struct

diff --git a/ocaml/lib/Hacl_Hash_SHA3_bindings.ml b/ocaml/lib/Hacl_Hash_SHA3_bindings.ml
@@ -85,16 +85,16 @@ module Bindings(F:Cstubs.FOREIGN) =
            (ocaml_bytes @-> (uint32_t @-> (ocaml_bytes @-> (returning void)))))
     let hacl_Hash_SHA3_sha3_224 =
       foreign "Hacl_Hash_SHA3_sha3_224"
-        (uint32_t @-> (ocaml_bytes @-> (ocaml_bytes @-> (returning void))))
+        (ocaml_bytes @-> (ocaml_bytes @-> (uint32_t @-> (returning void))))
     let hacl_Hash_SHA3_sha3_256 =
       foreign "Hacl_Hash_SHA3_sha3_256"
-        (uint32_t @-> (ocaml_bytes @-> (ocaml_bytes @-> (returning void))))
+        (ocaml_bytes @-> (ocaml_bytes @-> (uint32_t @-> (returning void))))
     let hacl_Hash_SHA3_sha3_384 =
       foreign "Hacl_Hash_SHA3_sha3_384"
-        (uint32_t @-> (ocaml_bytes @-> (ocaml_bytes @-> (returning void))))
+        (ocaml_bytes @-> (ocaml_bytes @-> (uint32_t @-> (returning void))))
     let hacl_Hash_SHA3_sha3_512 =
       foreign "Hacl_Hash_SHA3_sha3_512"
-        (uint32_t @-> (ocaml_bytes @-> (ocaml_bytes @-> (returning void))))
+        (ocaml_bytes @-> (ocaml_bytes @-> (uint32_t @-> (returning void))))
     let hacl_Hash_SHA3_state_permute =
       foreign "Hacl_Hash_SHA3_state_permute"
         ((ptr uint64_t) @-> (returning void))