diff --git a/Makefile.pre.in b/Makefile.pre.in index 7ac301c82678aa..fa26828e9fc789 100644 --- a/Makefile.pre.in +++ b/Makefile.pre.in @@ -669,9 +669,10 @@ LIBHACL_HEADERS= \ Modules/_hacl/include/krml/FStar_UInt128_Verified.h \ Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h \ Modules/_hacl/include/krml/fstar_uint128_struct_endianness.h \ + Modules/_hacl/include/krml/internal/compat.h \ Modules/_hacl/include/krml/internal/target.h \ + Modules/_hacl/include/krml/internal/types.h \ Modules/_hacl/include/krml/lowstar_endianness.h \ - Modules/_hacl/include/krml/types.h \ Modules/_hacl/Hacl_Streaming_Types.h \ Modules/_hacl/python_hacl_namespaces.h @@ -690,6 +691,7 @@ LIBHACL_BLAKE2_HEADERS= \ Modules/_hacl/internal/Hacl_Impl_Blake2_Constants.h \ Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h \ Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h \ + Modules/_hacl/internal/Hacl_Streaming_Types.h \ $(LIBHACL_HEADERS) ######################################################################### diff --git a/Misc/NEWS.d/next/Build/2025-03-11-19-06-50.gh-issue-130213._eQr0g.rst b/Misc/NEWS.d/next/Build/2025-03-11-19-06-50.gh-issue-130213._eQr0g.rst new file mode 100644 index 00000000000000..5dba4ff64f39b1 --- /dev/null +++ b/Misc/NEWS.d/next/Build/2025-03-11-19-06-50.gh-issue-130213._eQr0g.rst @@ -0,0 +1,2 @@ +Update the vendored HACL* library to fix build issues with older clang +compilers. diff --git a/Misc/sbom.spdx.json b/Misc/sbom.spdx.json index 316c266b7e4fd6..2bfe2a33fd1b1b 100644 --- a/Misc/sbom.spdx.json +++ b/Misc/sbom.spdx.json @@ -300,11 +300,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "1cd3cda98e0e6882a13a59268b88640c542350fd" + "checksumValue": "4b6e7696e8d84f322fb24b1fbb08ccb9b0e7d51b" }, { "algorithm": "SHA256", - "checksumValue": "41a420bc9355e451720e60e9536e66f04dc6e416ca9217c4ab18d827887a2e08" + "checksumValue": "50a65a34a7a7569eedf7fa864a7892eeee5840a7fdf6fa8f1e87d42c65f6c877" } ], "fileName": "Modules/_hacl/Hacl_Hash_Blake2b.c" @@ -314,11 +314,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "b0b3ae92d6aee7b52bacfdf02409d8d7e23701ee" + "checksumValue": "7c66ac004a1dcf3fee0ab9aa62d61972f029de3a" }, { "algorithm": "SHA256", - "checksumValue": "95d1dd4097a706b0719610da674297fa253b30d03a6ead4685ed648e20cb51a2" + "checksumValue": "9a7239a01a4ee8defbe3ebd9f0d12c873a1dd8e0659070380b2eab3ab0177333" } ], "fileName": "Modules/_hacl/Hacl_Hash_Blake2b.h" @@ -328,11 +328,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "0ceef306590ec12251db03a31fc08ecba697486d" + "checksumValue": "0f75e44a42775247a46acc2beaa6bae8f199a3d9" }, { "algorithm": "SHA256", - "checksumValue": "1575a23b21319e55e670f74194fc2dfd1777eb5a3816cad43750e03da6e44db9" + "checksumValue": "03b612c24193464ed6848aeebbf44f9266b78ec6eed2486056211cde8992c49a" } ], "fileName": "Modules/_hacl/Hacl_Hash_Blake2b_Simd256.c" @@ -342,11 +342,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "a5011646670c4f51368aca661e458e4c7f1d88e0" + "checksumValue": "7f273d26942233e5dcdfb4c1a16ff2486b15f899" }, { "algorithm": "SHA256", - "checksumValue": "f00c1fe8e774c7ec65f6c5a8efa43ce180a17fc80ed6119ada8c4022d058b6e2" + "checksumValue": "dbc0dacc68ed52dbf1b7d6fba2c87870317998bc046e65f6deaaa150625432f8" } ], "fileName": "Modules/_hacl/Hacl_Hash_Blake2b_Simd256.h" @@ -370,11 +370,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "9616a9f8d795d64487bf86a96719f943729621e2" + "checksumValue": "65bf44140691b046dcfed3ab1576dbf8bbf96dc5" }, { "algorithm": "SHA256", - "checksumValue": "5ecde5ddc8ec073cffe64d60e868535d995f33fb0f87f9b50e68bd2a694b7434" + "checksumValue": "0f98959dafffce039ade9d296f7a05bed151c9c512498f48e4b326a5523a240b" } ], "fileName": "Modules/_hacl/Hacl_Hash_Blake2s.c" @@ -384,11 +384,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "0328172a62507a051cd60ff9603710ed5aea1bc8" + "checksumValue": "2120c8c467aeebcc7c8b9678c15e79648433b91a" }, { "algorithm": "SHA256", - "checksumValue": "9f3c8ef615c9fbc59ef796d0ad2a7a76a7e55dc8939077b44ca538cbf8889a8c" + "checksumValue": "45735f7fe2dbbad7656d07854e9ec8176ad26c79f90dcc0fec0b9a59a6311ba7" } ], "fileName": "Modules/_hacl/Hacl_Hash_Blake2s.h" @@ -398,11 +398,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "5b950ce0a5c8f0c2c56b4ac96e1943b504255d45" + "checksumValue": "0da9782455923aede8d8dce9dfdc38f4fc1de572" }, { "algorithm": "SHA256", - "checksumValue": "5a5f5d8e376dc30d89fd6c6c435157fe9ffa5308030e7abb1256afaee0765536" + "checksumValue": "2d17ae768fd3d7d6decddd8b4aaf23ce02a809ee62bb98da32c8a7f54acf92d0" } ], "fileName": "Modules/_hacl/Hacl_Hash_Blake2s_Simd128.c" @@ -412,11 +412,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "32f35c173c10a2c49ac53c839cfbccd8a147274d" + "checksumValue": "9028e24c9876d9d16b2435ec29240c6b57bfe2a0" }, { "algorithm": "SHA256", - "checksumValue": "8734879b551f0fa860002ae81c0d0cfbade561007d9c26ad18c5a221e239237e" + "checksumValue": "062e3b856acac4f929c1e04b8264a754cad21ca6580215f7094a3f0a04edb912" } ], "fileName": "Modules/_hacl/Hacl_Hash_Blake2s_Simd128.h" @@ -440,11 +440,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "f8ba39b46ebdfa7d031d9c33130c6ded680a8120" + "checksumValue": "38e8d96ef1879480780494058a93cec181f8d6d7" }, { "algorithm": "SHA256", - "checksumValue": "f71cf6a0e8f09354c2af2c785a1d36e0cba7613a589be01ca8a3d8478f4c8874" + "checksumValue": "61e77d2063cf60c96e9ce06af215efe5d42c43026833bffed5732326fe97ed1e" } ], "fileName": "Modules/_hacl/Hacl_Hash_MD5.c" @@ -454,11 +454,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "eaaab54cea2b0bb8ec0eedf0b373d42f1a0f8f6c" + "checksumValue": "e67a9bc18358c57afaeff3a174893ddfdb52dfc6" }, { "algorithm": "SHA256", - "checksumValue": "9a02e2a6e163515ea0228a859d5e55c1f57b11fae5908c42f9f9814ce9bca230" + "checksumValue": "16e982081f6c2fd03ea751fcc64f5a835c94652841836e231fe562b9e287f4bc" } ], "fileName": "Modules/_hacl/Hacl_Hash_MD5.h" @@ -468,11 +468,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "f4f42faf8da78a230199f649c0f2a1b865799a31" + "checksumValue": "986dd5ba0b34d15f3e5e5c656979aea1b502e8aa" }, { "algorithm": "SHA256", - "checksumValue": "5b29bd9951646861e0e19427be5d923a5bab7a4516824ccc068f696469195eec" + "checksumValue": "38d5f1f2e67a0eb30789f81fc56c07a6e7246e2b1be6c65485bcca1dcd0e0806" } ], "fileName": "Modules/_hacl/Hacl_Hash_SHA1.c" @@ -482,11 +482,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "722b57139737ceeb88e41d3839e6f7d70578741b" + "checksumValue": "f1ca21f1ee8b15ad9ccfbda72165b9d86912166c" }, { "algorithm": "SHA256", - "checksumValue": "5640295c790d56b1b4df147d6a6c58803b1845cd7d93365bf7cc7b75ba3cacd5" + "checksumValue": "4b2ad9ea93fdd9c2fdc521fc4e14e02550666c2717a23b85819db2e07ea555f3" } ], "fileName": "Modules/_hacl/Hacl_Hash_SHA1.h" @@ -496,11 +496,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "b0aa8810339adb09623ffa429246b4324fac4565" + "checksumValue": "f732a6710fe3e13cd28130f0f20504e347d1c412" }, { "algorithm": "SHA256", - "checksumValue": "2288f8f860efe80eed4f1e14ef570079b7459aeb41f87e94e691d7cf5e0e7adb" + "checksumValue": "86cf32e4d1f3ba93a94108271923fdafe2204447792a918acf4a2250f352dbde" } ], "fileName": "Modules/_hacl/Hacl_Hash_SHA2.c" @@ -510,11 +510,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "4903e10291d07367be3bc283935bc52926e57ba1" + "checksumValue": "f38cebeeca40a83aeb2cf5dfce578ffefe176d84" }, { "algorithm": "SHA256", - "checksumValue": "093d7693084af0999d2a13d207311d74b5bdfdc9c08447ed4a979e3f7505ae6b" + "checksumValue": "ee03bf9368d1a3a3c70cfd4e9391b2485466404db4a60bfc5319630cc314b590" } ], "fileName": "Modules/_hacl/Hacl_Hash_SHA2.h" @@ -524,11 +524,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "ef374b9d0951ebb38006af944dd4b38a6cf3abb2" + "checksumValue": "50f75337b31f509b5bfcc7ebb3d066b82a0f1b33" }, { "algorithm": "SHA256", - "checksumValue": "164df19f229143006c5f9a3c0bd771415f152bfbc7efb61c337fa0f903003eb3" + "checksumValue": "c9e1442899e5b902fa39f413f1a3131f7ab5c2283d5100dc8ac675a7d5ebbdf1" } ], "fileName": "Modules/_hacl/Hacl_Hash_SHA3.c" @@ -538,11 +538,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "7d78e6844dde1f9b5e68f58ca105a4c330461ff6" + "checksumValue": "01717207aef77174e328186d48c27517f6644c15" }, { "algorithm": "SHA256", - "checksumValue": "231d9bc13190be4b6821acb518194f32f4a3c04f1c034b3118f6db0bab2debe3" + "checksumValue": "620dded172e94cb3f25f9904b44977d91f2cc9573e41b38f19e929d083ae0308" } ], "fileName": "Modules/_hacl/Hacl_Hash_SHA3.h" @@ -552,11 +552,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "ab7b4d9465a2765a07f8d5bccace7182b28ed1b8" + "checksumValue": "372448599774a98e5c5d083e91f301ed1c4b822e" }, { "algorithm": "SHA256", - "checksumValue": "26913613f3b4f8ffff0a3e211a5ebc849159094e5e11de0a31fcb95b6105b74c" + "checksumValue": "95d8e70ca4bc6aa98f6d2435ceb6410ead299b1f700fae1f5c603ec3f57ea551" } ], "fileName": "Modules/_hacl/Hacl_Streaming_Types.h" @@ -566,11 +566,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "118dc712780ea680affa8d9794470440eb87ff10" + "checksumValue": "80dae56879ed9bace476362ef251de48ce055a20" }, { "algorithm": "SHA256", - "checksumValue": "b017e7d5662a308c938cf4e4b919680c8f3e27f42975ca152b62fe65c5f7fb0c" + "checksumValue": "da84b6287e9aa1fc52e819a8ca10e79b51263f1dda6b4528ed8c0c74a11fb0ea" } ], "fileName": "Modules/_hacl/Lib_Memzero0.c" @@ -580,11 +580,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "7665829b9396f72e7f8098080d6d6773565468e9" + "checksumValue": "eaa543c778300238dc23034aafeada0951154af1" }, { "algorithm": "SHA256", - "checksumValue": "ca7357ee70365c690664a44f6522e526636151d9ed2da8d0d29da15bb8556530" + "checksumValue": "3fd2552d527a23110d61ad2811c774810efb1eaee008f136c2a0d609daa77f5b" } ], "fileName": "Modules/_hacl/include/krml/FStar_UInt128_Verified.h" @@ -594,11 +594,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "a2db924d0e8f7df3139e9a20355ffa520aded479" + "checksumValue": "41ee1e34ede7ef5b24b87d4ca816fd6d9fac8010" }, { "algorithm": "SHA256", - "checksumValue": "f1de79fb4c763b215c823f44471bbae6b65e6bb533eb52a5863d551d5e2e6748" + "checksumValue": "d48ed03e504cb87793a310a9552fb3ba2ebd6fe90127b7d642c8740fba1b9748" } ], "fileName": "Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h" @@ -617,58 +617,72 @@ ], "fileName": "Modules/_hacl/include/krml/fstar_uint128_struct_endianness.h" }, + { + "SPDXID": "SPDXRef-FILE-Modules-hacl-include-krml-internal-compat.h", + "checksums": [ + { + "algorithm": "SHA1", + "checksumValue": "b901e914ce57063f0ad2d113af4fca5761031d3b" + }, + { + "algorithm": "SHA256", + "checksumValue": "c5a04a1f99807cea29ac1832ba17d8a3d3805862d3a713642583be2106e04edb" + } + ], + "fileName": "Modules/_hacl/include/krml/internal/compat.h" + }, { "SPDXID": "SPDXRef-FILE-Modules-hacl-include-krml-internal-target.h", "checksums": [ { "algorithm": "SHA1", - "checksumValue": "9c5cac1582dcd6e0d0a4142e6e8b285b4cb7d9e6" + "checksumValue": "e01d7d493fbaceeedc4b1c6451d8240bcb9c903a" }, { "algorithm": "SHA256", - "checksumValue": "b1e32138ac8c262e872f7da43ec80c1e54c08bcbdec4b7be17117aa25807f87e" + "checksumValue": "c2f0a43884771f24d7cb744b79818b160020d2739b2881b2054cfc97fb2e7b4a" } ], "fileName": "Modules/_hacl/include/krml/internal/target.h" }, { - "SPDXID": "SPDXRef-FILE-Modules-hacl-include-krml-lowstar-endianness.h", + "SPDXID": "SPDXRef-FILE-Modules-hacl-include-krml-internal-types.h", "checksums": [ { "algorithm": "SHA1", - "checksumValue": "e18efc9239a5df0f222b5f7b0a65f72509d7e304" + "checksumValue": "3f66313d16891f43b21c1a736081c2c6d46bf370" }, { "algorithm": "SHA256", - "checksumValue": "47dd5a7d21b5302255f9fff28884f65d3056fc3f54471ed62ec85fa1904f8aa5" + "checksumValue": "78e9bff9124968108e1699e1c6388e3d4ec9bd72dd8adff49734a69ab380ee5c" } ], - "fileName": "Modules/_hacl/include/krml/lowstar_endianness.h" + "fileName": "Modules/_hacl/include/krml/internal/types.h" }, { - "SPDXID": "SPDXRef-FILE-Modules-hacl-include-krml-types.h", + "SPDXID": "SPDXRef-FILE-Modules-hacl-include-krml-lowstar-endianness.h", "checksums": [ { "algorithm": "SHA1", - "checksumValue": "df8e0ed74a5970d09d3cc4c6e7c6c7a4c4e5015c" + "checksumValue": "e18efc9239a5df0f222b5f7b0a65f72509d7e304" }, { "algorithm": "SHA256", - "checksumValue": "de7444c345caa4c47902c4380500356a3ee7e199d2aab84fd8c4960410154f3d" + "checksumValue": "47dd5a7d21b5302255f9fff28884f65d3056fc3f54471ed62ec85fa1904f8aa5" } ], - "fileName": "Modules/_hacl/include/krml/types.h" + "fileName": "Modules/_hacl/include/krml/lowstar_endianness.h" }, { "SPDXID": "SPDXRef-FILE-Modules-hacl-internal-Hacl-Hash-Blake2b.h", "checksums": [ { "algorithm": "SHA1", - "checksumValue": "31b329bd39ff72ed25086e2afe7875949003c140" + "checksumValue": "0741cb8497309d648428be1e7b5944b1fc167187" }, { "algorithm": "SHA256", - "checksumValue": "16df6cf240ee99aade0fd11d5cc7573c201c7589d8325a5c95c7670c531e1518" + "checksumValue": "f9b923a566d62de047c753637143d439ca1c25221c08352ddc1738ff4a6ac721" } ], "fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2b.h" @@ -678,11 +692,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "3f4fdfdaef97a2cbac5ec091c91ede18d4b33f92" + "checksumValue": "878ae284c93824b80b1763e8b3e6be3c410777a8" }, { "algorithm": "SHA256", - "checksumValue": "96b1c77860f12bcadad0caca77a5a1649a840ad9989d97984a3b51bb98c80e2f" + "checksumValue": "49df6223f6403daf503a1af1a3d2f943d30b5889fe7ed20299c3df24c1e3853d" } ], "fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h" @@ -692,11 +706,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "9efd61f6ba8d126e98abd83679a5ed5954278c31" + "checksumValue": "25552d8cbf8aa345907635b38f284eec9075301e" }, { "algorithm": "SHA256", - "checksumValue": "143f58f033786173501a72ac302e435963fdce6c2cc38eef6d6adeb3cdc1bb9c" + "checksumValue": "a3424cf4c5518654908086bbbf5d465715ec3b23625ef0cadc29492d1f90366c" } ], "fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2s.h" @@ -706,11 +720,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "3f984829465285283b03b1111b4918cfb48b8031" + "checksumValue": "54a712fc3ed5a817288351cbac5b7d9afa7e379f" }, { "algorithm": "SHA256", - "checksumValue": "cd24038fdd617edc65e472496b0d58f23ff312f81f9244c3e7893fdc9a1b2977" + "checksumValue": "c6abae648b8a1e9d5631c0a959620cad1f7e92ce522e07c3416199fe51debef6" } ], "fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h" @@ -720,11 +734,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "60f02d21f045c8a4c2b6b84a8f7e023d9490c8e5" + "checksumValue": "c15c5f83bbb9f62611c49f0f8f723eaab1a27488" }, { "algorithm": "SHA256", - "checksumValue": "370d8ef9c48cb55472ece11e12eaf94c58118de3f5515b6df1c130b696597828" + "checksumValue": "95cd5d91c4a9217901d0b3395dcd8881e62e2055d723b532ec5176386a636d22" } ], "fileName": "Modules/_hacl/internal/Hacl_Hash_MD5.h" @@ -734,11 +748,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "6346c30a140e7d3010c98fe19d14fa229a54eb16" + "checksumValue": "7b8717e3a24e7e16a34b251d0d02da6f68439695" }, { "algorithm": "SHA256", - "checksumValue": "ab52c6092bdbbfc9884f841bf4824016792ffa96167577cbe0df00dd96f56a34" + "checksumValue": "9473d8bc9506fe0053d7d98c225d4873011329863f1c4a8e93e43fc71bd1f314" } ], "fileName": "Modules/_hacl/internal/Hacl_Hash_SHA1.h" @@ -748,11 +762,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "2e9ae174142fc491f20567ab8b5c08cef9b07cfe" + "checksumValue": "e319c949f5a2dd765be2c8c7ff77bfe52ee6c7da" }, { "algorithm": "SHA256", - "checksumValue": "07100964adcf4b5f8bd4773e25f475b34cd180b90df8b1c0052e55c008b7cc49" + "checksumValue": "75261448e51c3eb1ba441e973b193e23570b167f67743942ee2ee57417491c9f" } ], "fileName": "Modules/_hacl/internal/Hacl_Hash_SHA2.h" @@ -762,11 +776,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "39ba6e8959e44ae956a640d3a1fb3ef60de8a9e5" + "checksumValue": "dbd92415c31606804102b79d5ba3d1752fe03887" }, { "algorithm": "SHA256", - "checksumValue": "dbf4b86a04b4d8716976f8c023cccbfe174435dbec3bc00fc1f066fb52c4e341" + "checksumValue": "5d74a76a0ac3659a1ae1276c3ca55521f09e83d2f0039f5c519a76f8f3c76a8e" } ], "fileName": "Modules/_hacl/internal/Hacl_Hash_SHA3.h" @@ -776,15 +790,29 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "c3ae35ed5bf70cf011b2732df011231528b9111c" + "checksumValue": "ad788265f8e1b078c4d1cb6e90b8c031590e6baf" }, { "algorithm": "SHA256", - "checksumValue": "c381fea7b8b505a7c7ce27231a36751add6b184b204132935c5faaba4fce8ba1" + "checksumValue": "d8354a9b75e2470085fa7e538493130e81fa23a804a6a69d34da8fdcc941c038" } ], "fileName": "Modules/_hacl/internal/Hacl_Impl_Blake2_Constants.h" }, + { + "SPDXID": "SPDXRef-FILE-Modules-hacl-internal-Hacl-Streaming-Types.h", + "checksums": [ + { + "algorithm": "SHA1", + "checksumValue": "4e6b098e89fd447bd03f47b55208208456b20966" + }, + { + "algorithm": "SHA256", + "checksumValue": "d54d947968ca125978d61fea844711b990f0a18ab0fbca87e41029004d9d04b6" + } + ], + "fileName": "Modules/_hacl/internal/Hacl_Streaming_Types.h" + }, { "SPDXID": "SPDXRef-FILE-Modules-hacl-lib-memzero0.h", "checksums": [ @@ -804,11 +832,11 @@ "checksums": [ { "algorithm": "SHA1", - "checksumValue": "f4a33ad535768b860362ab0bd033a70da0b524b7" + "checksumValue": "63e47cc290c4ec887dca708000876ac37ee75ba0" }, { "algorithm": "SHA256", - "checksumValue": "433cdf4ba80bc72e0cea5d4b420ff18676baeafdb5ba19adf5b7fb33e90b424b" + "checksumValue": "d09a6196d65c2645974100eb922002bd387d3ae13f2653780f82ed97a79af635" } ], "fileName": "Modules/_hacl/libintvector.h" @@ -1640,14 +1668,14 @@ "checksums": [ { "algorithm": "SHA256", - "checksumValue": "40de5297b032d2676fc0039049b4e8dab1f2730eebb5ecff6a40c04fa0356339" + "checksumValue": "502a0250fa08d2cbcc8b9e43831235a2c075de2eb180e7381ecb5d10b181971e" } ], - "downloadLocation": "https://github.com/hacl-star/hacl-star/archive/f218923ef2417d963d7efc7951593ae6aef613f7.zip", + "downloadLocation": "https://github.com/hacl-star/hacl-star/archive/322f6d58290e0ed7f4ecb84fcce12917aa0f594b.zip", "externalRefs": [ { "referenceCategory": "SECURITY", - "referenceLocator": "cpe:2.3:a:hacl-star:hacl-star:f218923ef2417d963d7efc7951593ae6aef613f7:*:*:*:*:*:*:*", + "referenceLocator": "cpe:2.3:a:hacl-star:hacl-star:322f6d58290e0ed7f4ecb84fcce12917aa0f594b:*:*:*:*:*:*:*", "referenceType": "cpe23Type" } ], @@ -1655,7 +1683,7 @@ "name": "hacl-star", "originator": "Organization: HACL* Developers", "primaryPackagePurpose": "SOURCE", - "versionInfo": "f218923ef2417d963d7efc7951593ae6aef613f7" + "versionInfo": "322f6d58290e0ed7f4ecb84fcce12917aa0f594b" }, { "SPDXID": "SPDXRef-PACKAGE-macholib", @@ -1923,18 +1951,23 @@ "relationshipType": "CONTAINS", "spdxElementId": "SPDXRef-PACKAGE-hacl-star" }, + { + "relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-internal-compat.h", + "relationshipType": "CONTAINS", + "spdxElementId": "SPDXRef-PACKAGE-hacl-star" + }, { "relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-internal-target.h", "relationshipType": "CONTAINS", "spdxElementId": "SPDXRef-PACKAGE-hacl-star" }, { - "relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-lowstar-endianness.h", + "relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-internal-types.h", "relationshipType": "CONTAINS", "spdxElementId": "SPDXRef-PACKAGE-hacl-star" }, { - "relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-types.h", + "relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-lowstar-endianness.h", "relationshipType": "CONTAINS", "spdxElementId": "SPDXRef-PACKAGE-hacl-star" }, @@ -1983,6 +2016,11 @@ "relationshipType": "CONTAINS", "spdxElementId": "SPDXRef-PACKAGE-hacl-star" }, + { + "relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-internal-Hacl-Streaming-Types.h", + "relationshipType": "CONTAINS", + "spdxElementId": "SPDXRef-PACKAGE-hacl-star" + }, { "relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-lib-memzero0.h", "relationshipType": "CONTAINS", diff --git a/Modules/_hacl/Hacl_Hash_Blake2b.c b/Modules/_hacl/Hacl_Hash_Blake2b.c index 1bab75e6aaf2ab..21ab2b88c799a6 100644 --- a/Modules/_hacl/Hacl_Hash_Blake2b.c +++ b/Modules/_hacl/Hacl_Hash_Blake2b.c @@ -25,6 +25,9 @@ #include "internal/Hacl_Hash_Blake2b.h" +#include "Hacl_Streaming_Types.h" + +#include "internal/Hacl_Streaming_Types.h" #include "internal/Hacl_Impl_Blake2_Constants.h" #include "lib_memzero0.h" @@ -697,127 +700,215 @@ void Hacl_Hash_Blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash) Lib_Memzero0_memzero(b, 64U, uint8_t, void *); } +typedef struct option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t____s +{ + Hacl_Streaming_Types_optional tag; + Hacl_Hash_Blake2b_block_state_t v; +} +option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___; + static Hacl_Hash_Blake2b_state_t *malloc_raw(Hacl_Hash_Blake2b_index kk, Hacl_Hash_Blake2b_params_and_key key) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t)); - uint64_t *wv = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t)); - uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t)); - Hacl_Hash_Blake2b_block_state_t - block_state = - { - .fst = kk.key_length, - .snd = kk.digest_length, - .thd = kk.last_node, - .f3 = { .fst = wv, .snd = b } - }; - uint8_t kk10 = kk.key_length; - uint32_t ite; - if (kk10 != 0U) + if (buf == NULL) { - ite = 128U; + return NULL; + } + uint8_t *buf1 = buf; + uint64_t *wv0 = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t)); + option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___ block_state; + if (wv0 == NULL) + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){ + .tag = Hacl_Streaming_Types_None + } + ); } else { - ite = 0U; + uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t)); + if (b == NULL) + { + KRML_HOST_FREE(wv0); + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){ + .tag = Hacl_Streaming_Types_Some, + .v = { + .fst = kk.key_length, + .snd = kk.digest_length, + .thd = kk.last_node, + .f3 = { .fst = wv0, .snd = b } + } + } + ); + } } - Hacl_Hash_Blake2b_state_t - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)ite }; - Hacl_Hash_Blake2b_state_t - *p = (Hacl_Hash_Blake2b_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2b_state_t)); - p[0U] = s; - Hacl_Hash_Blake2b_blake2_params *p1 = key.fst; - uint8_t kk1 = p1->key_length; - uint8_t nn = p1->digest_length; - bool last_node = block_state.thd; - Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; - uint64_t *h = block_state.f3.snd; - uint32_t kk20 = (uint32_t)i.key_length; - uint8_t *k_1 = key.snd; - if (!(kk20 == 0U)) + if (block_state.tag == Hacl_Streaming_Types_None) { - uint8_t *sub_b = buf + kk20; - memset(sub_b, 0U, (128U - kk20) * sizeof (uint8_t)); - memcpy(buf, k_1, kk20 * sizeof (uint8_t)); + KRML_HOST_FREE(buf1); + return NULL; } - Hacl_Hash_Blake2b_blake2_params pv = p1[0U]; - uint64_t tmp[8U] = { 0U }; - uint64_t *r0 = h; - uint64_t *r1 = h + 4U; - uint64_t *r2 = h + 8U; - uint64_t *r3 = h + 12U; - uint64_t iv0 = Hacl_Hash_Blake2b_ivTable_B[0U]; - uint64_t iv1 = Hacl_Hash_Blake2b_ivTable_B[1U]; - uint64_t iv2 = Hacl_Hash_Blake2b_ivTable_B[2U]; - uint64_t iv3 = Hacl_Hash_Blake2b_ivTable_B[3U]; - uint64_t iv4 = Hacl_Hash_Blake2b_ivTable_B[4U]; - uint64_t iv5 = Hacl_Hash_Blake2b_ivTable_B[5U]; - uint64_t iv6 = Hacl_Hash_Blake2b_ivTable_B[6U]; - uint64_t iv7 = Hacl_Hash_Blake2b_ivTable_B[7U]; - r2[0U] = iv0; - r2[1U] = iv1; - r2[2U] = iv2; - r2[3U] = iv3; - r3[0U] = iv4; - r3[1U] = iv5; - r3[2U] = iv6; - r3[3U] = iv7; - uint8_t kk2 = pv.key_length; - uint8_t nn1 = pv.digest_length; - KRML_MAYBE_FOR2(i0, - 0U, - 2U, - 1U, - uint64_t *os = tmp + 4U; - uint8_t *bj = pv.salt + i0 * 8U; - uint64_t u = load64_le(bj); - uint64_t r4 = u; - uint64_t x = r4; - os[i0] = x;); - KRML_MAYBE_FOR2(i0, - 0U, - 2U, - 1U, - uint64_t *os = tmp + 6U; - uint8_t *bj = pv.personal + i0 * 8U; - uint64_t u = load64_le(bj); - uint64_t r4 = u; - uint64_t x = r4; - os[i0] = x;); - tmp[0U] = - (uint64_t)nn1 - ^ - ((uint64_t)kk2 - << 8U - ^ ((uint64_t)pv.fanout << 16U ^ ((uint64_t)pv.depth << 24U ^ (uint64_t)pv.leaf_length << 32U))); - tmp[1U] = pv.node_offset; - tmp[2U] = (uint64_t)pv.node_depth ^ (uint64_t)pv.inner_length << 8U; - tmp[3U] = 0ULL; - uint64_t tmp0 = tmp[0U]; - uint64_t tmp1 = tmp[1U]; - uint64_t tmp2 = tmp[2U]; - uint64_t tmp3 = tmp[3U]; - uint64_t tmp4 = tmp[4U]; - uint64_t tmp5 = tmp[5U]; - uint64_t tmp6 = tmp[6U]; - uint64_t tmp7 = tmp[7U]; - uint64_t iv0_ = iv0 ^ tmp0; - uint64_t iv1_ = iv1 ^ tmp1; - uint64_t iv2_ = iv2 ^ tmp2; - uint64_t iv3_ = iv3 ^ tmp3; - uint64_t iv4_ = iv4 ^ tmp4; - uint64_t iv5_ = iv5 ^ tmp5; - uint64_t iv6_ = iv6 ^ tmp6; - uint64_t iv7_ = iv7 ^ tmp7; - r0[0U] = iv0_; - r0[1U] = iv1_; - r0[2U] = iv2_; - r0[3U] = iv3_; - r1[0U] = iv4_; - r1[1U] = iv5_; - r1[2U] = iv6_; - r1[3U] = iv7_; - return p; + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_Blake2b_block_state_t block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + uint8_t kk10 = kk.key_length; + uint32_t ite; + if (kk10 != 0U) + { + ite = 128U; + } + else + { + ite = 0U; + } + Hacl_Hash_Blake2b_state_t + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)ite }; + Hacl_Hash_Blake2b_state_t + *p = (Hacl_Hash_Blake2b_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2b_state_t)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + uint64_t *b = block_state1.f3.snd; + uint64_t *wv = block_state1.f3.fst; + KRML_HOST_FREE(wv); + KRML_HOST_FREE(b); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_Blake2b_blake2_params *p1 = key.fst; + uint8_t kk1 = p1->key_length; + uint8_t nn = p1->digest_length; + bool last_node = block_state1.thd; + Hacl_Hash_Blake2b_index + i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; + uint64_t *h = block_state1.f3.snd; + uint32_t kk20 = (uint32_t)i.key_length; + uint8_t *k_2 = key.snd; + if (!(kk20 == 0U)) + { + uint8_t *sub_b = buf1 + kk20; + memset(sub_b, 0U, (128U - kk20) * sizeof (uint8_t)); + memcpy(buf1, k_2, kk20 * sizeof (uint8_t)); + } + Hacl_Hash_Blake2b_blake2_params pv = p1[0U]; + uint64_t tmp[8U] = { 0U }; + uint64_t *r0 = h; + uint64_t *r1 = h + 4U; + uint64_t *r2 = h + 8U; + uint64_t *r3 = h + 12U; + uint64_t iv0 = Hacl_Hash_Blake2b_ivTable_B[0U]; + uint64_t iv1 = Hacl_Hash_Blake2b_ivTable_B[1U]; + uint64_t iv2 = Hacl_Hash_Blake2b_ivTable_B[2U]; + uint64_t iv3 = Hacl_Hash_Blake2b_ivTable_B[3U]; + uint64_t iv4 = Hacl_Hash_Blake2b_ivTable_B[4U]; + uint64_t iv5 = Hacl_Hash_Blake2b_ivTable_B[5U]; + uint64_t iv6 = Hacl_Hash_Blake2b_ivTable_B[6U]; + uint64_t iv7 = Hacl_Hash_Blake2b_ivTable_B[7U]; + r2[0U] = iv0; + r2[1U] = iv1; + r2[2U] = iv2; + r2[3U] = iv3; + r3[0U] = iv4; + r3[1U] = iv5; + r3[2U] = iv6; + r3[3U] = iv7; + uint8_t kk2 = pv.key_length; + uint8_t nn1 = pv.digest_length; + KRML_MAYBE_FOR2(i0, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 4U; + uint8_t *bj = pv.salt + i0 * 8U; + uint64_t u = load64_le(bj); + uint64_t r4 = u; + uint64_t x = r4; + os[i0] = x;); + KRML_MAYBE_FOR2(i0, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 6U; + uint8_t *bj = pv.personal + i0 * 8U; + uint64_t u = load64_le(bj); + uint64_t r4 = u; + uint64_t x = r4; + os[i0] = x;); + tmp[0U] = + (uint64_t)nn1 + ^ + ((uint64_t)kk2 + << 8U + ^ + ((uint64_t)pv.fanout + << 16U + ^ ((uint64_t)pv.depth << 24U ^ (uint64_t)pv.leaf_length << 32U))); + tmp[1U] = pv.node_offset; + tmp[2U] = (uint64_t)pv.node_depth ^ (uint64_t)pv.inner_length << 8U; + tmp[3U] = 0ULL; + uint64_t tmp0 = tmp[0U]; + uint64_t tmp1 = tmp[1U]; + uint64_t tmp2 = tmp[2U]; + uint64_t tmp3 = tmp[3U]; + uint64_t tmp4 = tmp[4U]; + uint64_t tmp5 = tmp[5U]; + uint64_t tmp6 = tmp[6U]; + uint64_t tmp7 = tmp[7U]; + uint64_t iv0_ = iv0 ^ tmp0; + uint64_t iv1_ = iv1 ^ tmp1; + uint64_t iv2_ = iv2 ^ tmp2; + uint64_t iv3_ = iv3 ^ tmp3; + uint64_t iv4_ = iv4 ^ tmp4; + uint64_t iv5_ = iv5 ^ tmp5; + uint64_t iv6_ = iv6 ^ tmp6; + uint64_t iv7_ = iv7 ^ tmp7; + r0[0U] = iv0_; + r0[1U] = iv1_; + r0[2U] = iv2_; + r0[3U] = iv3_; + r1[0U] = iv4_; + r1[1U] = iv5_; + r1[2U] = iv6_; + r1[3U] = iv7_; + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** @@ -1137,7 +1228,7 @@ Hacl_Hash_Blake2b_update(Hacl_Hash_Blake2b_state_t *state, uint8_t *chunk, uint3 if (!(sz1 == 0U)) { uint64_t prevlen = total_len1 - (uint64_t)sz1; - K____uint64_t___uint64_t_ acc = block_state1.f3; + Hacl_Streaming_Types_two_pointers acc = block_state1.f3; uint64_t *wv = acc.fst; uint64_t *hash = acc.snd; uint32_t nb = 1U; @@ -1162,7 +1253,7 @@ Hacl_Hash_Blake2b_update(Hacl_Hash_Blake2b_state_t *state, uint8_t *chunk, uint3 uint32_t data2_len = chunk_len - data1_len; uint8_t *data1 = chunk; uint8_t *data2 = chunk + data1_len; - K____uint64_t___uint64_t_ acc = block_state1.f3; + Hacl_Streaming_Types_two_pointers acc = block_state1.f3; uint64_t *wv = acc.fst; uint64_t *hash = acc.snd; uint32_t nb = data1_len / 128U; @@ -1230,7 +1321,7 @@ Hacl_Hash_Blake2b_update(Hacl_Hash_Blake2b_state_t *state, uint8_t *chunk, uint3 if (!(sz1 == 0U)) { uint64_t prevlen = total_len1 - (uint64_t)sz1; - K____uint64_t___uint64_t_ acc = block_state1.f3; + Hacl_Streaming_Types_two_pointers acc = block_state1.f3; uint64_t *wv = acc.fst; uint64_t *hash = acc.snd; uint32_t nb = 1U; @@ -1256,7 +1347,7 @@ Hacl_Hash_Blake2b_update(Hacl_Hash_Blake2b_state_t *state, uint8_t *chunk, uint3 uint32_t data2_len = chunk_len - diff - data1_len; uint8_t *data1 = chunk2; uint8_t *data2 = chunk2 + data1_len; - K____uint64_t___uint64_t_ acc = block_state1.f3; + Hacl_Streaming_Types_two_pointers acc = block_state1.f3; uint64_t *wv = acc.fst; uint64_t *hash = acc.snd; uint32_t nb = data1_len / 128U; @@ -1339,7 +1430,7 @@ uint8_t Hacl_Hash_Blake2b_digest(Hacl_Hash_Blake2b_state_t *s, uint8_t *dst) } uint8_t *buf_last = buf_1 + r - ite; uint8_t *buf_multi = buf_1; - K____uint64_t___uint64_t_ acc0 = tmp_block_state.f3; + Hacl_Streaming_Types_two_pointers acc0 = tmp_block_state.f3; uint64_t *wv1 = acc0.fst; uint64_t *hash0 = acc0.snd; uint32_t nb = 0U; @@ -1350,7 +1441,7 @@ uint8_t Hacl_Hash_Blake2b_digest(Hacl_Hash_Blake2b_state_t *s, uint8_t *dst) buf_multi, nb); uint64_t prev_len_last = total_len - (uint64_t)r; - K____uint64_t___uint64_t_ acc = tmp_block_state.f3; + Hacl_Streaming_Types_two_pointers acc = tmp_block_state.f3; bool last_node1 = tmp_block_state.thd; uint64_t *wv = acc.fst; uint64_t *hash = acc.snd; @@ -1411,26 +1502,102 @@ Hacl_Hash_Blake2b_state_t *Hacl_Hash_Blake2b_copy(Hacl_Hash_Blake2b_state_t *sta uint8_t kk1 = block_state0.fst; Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } memcpy(buf, buf0, 128U * sizeof (uint8_t)); - uint64_t *wv = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t)); - uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t)); - Hacl_Hash_Blake2b_block_state_t - block_state = + uint64_t *wv0 = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t)); + option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___ block_state; + if (wv0 == NULL) + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t)); + if (b == NULL) { - .fst = i.key_length, - .snd = i.digest_length, - .thd = i.last_node, - .f3 = { .fst = wv, .snd = b } - }; - uint64_t *src_b = block_state0.f3.snd; - uint64_t *dst_b = block_state.f3.snd; - memcpy(dst_b, src_b, 16U * sizeof (uint64_t)); - Hacl_Hash_Blake2b_state_t - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Hash_Blake2b_state_t - *p = (Hacl_Hash_Blake2b_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2b_state_t)); - p[0U] = s; - return p; + KRML_HOST_FREE(wv0); + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){ + .tag = Hacl_Streaming_Types_Some, + .v = { + .fst = i.key_length, + .snd = i.digest_length, + .thd = i.last_node, + .f3 = { .fst = wv0, .snd = b } + } + } + ); + } + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_Blake2b_block_state_t block_state1 = block_state.v; + uint64_t *src_b = block_state0.f3.snd; + uint64_t *dst_b = block_state1.f3.snd; + memcpy(dst_b, src_b, 16U * sizeof (uint64_t)); + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Hash_Blake2b_state_t + s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 }; + Hacl_Hash_Blake2b_state_t + *p = (Hacl_Hash_Blake2b_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2b_state_t)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + uint64_t *b = block_state1.f3.snd; + uint64_t *wv = block_state1.f3.fst; + KRML_HOST_FREE(wv); + KRML_HOST_FREE(b); + KRML_HOST_FREE(buf); + return NULL; + } + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** diff --git a/Modules/_hacl/Hacl_Hash_Blake2b.h b/Modules/_hacl/Hacl_Hash_Blake2b.h index 5b5b037bcdc8a4..3a73f358c98cc3 100644 --- a/Modules/_hacl/Hacl_Hash_Blake2b.h +++ b/Modules/_hacl/Hacl_Hash_Blake2b.h @@ -32,13 +32,12 @@ extern "C" { #include #include "python_hacl_namespaces.h" -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" #include "Hacl_Streaming_Types.h" - typedef struct Hacl_Hash_Blake2b_blake2_params_s { uint8_t digest_length; @@ -72,29 +71,9 @@ Hacl_Hash_Blake2b_index; #define HACL_HASH_BLAKE2B_PERSONAL_BYTES (16U) -typedef struct K____uint64_t___uint64_t__s -{ - uint64_t *fst; - uint64_t *snd; -} -K____uint64_t___uint64_t_; - -typedef struct Hacl_Hash_Blake2b_block_state_t_s -{ - uint8_t fst; - uint8_t snd; - bool thd; - K____uint64_t___uint64_t_ f3; -} -Hacl_Hash_Blake2b_block_state_t; +typedef struct Hacl_Hash_Blake2b_block_state_t_s Hacl_Hash_Blake2b_block_state_t; -typedef struct Hacl_Hash_Blake2b_state_t_s -{ - Hacl_Hash_Blake2b_block_state_t block_state; - uint8_t *buf; - uint64_t total_len; -} -Hacl_Hash_Blake2b_state_t; +typedef struct Hacl_Hash_Blake2b_state_t_s Hacl_Hash_Blake2b_state_t; /** General-purpose allocation function that gives control over all diff --git a/Modules/_hacl/Hacl_Hash_Blake2b_Simd256.c b/Modules/_hacl/Hacl_Hash_Blake2b_Simd256.c index 19234ab9d7f9b2..c4d9b4a689d28f 100644 --- a/Modules/_hacl/Hacl_Hash_Blake2b_Simd256.c +++ b/Modules/_hacl/Hacl_Hash_Blake2b_Simd256.c @@ -25,6 +25,10 @@ #include "internal/Hacl_Hash_Blake2b_Simd256.h" +#include "Hacl_Streaming_Types.h" + +#include "Hacl_Hash_Blake2b.h" +#include "internal/Hacl_Streaming_Types.h" #include "internal/Hacl_Impl_Blake2_Constants.h" #include "internal/Hacl_Hash_Blake2b.h" #include "lib_memzero0.h" @@ -523,136 +527,268 @@ Hacl_Hash_Blake2b_Simd256_store_state256b_to_state32( os[i] = x;); } -Lib_IntVector_Intrinsics_vec256 *Hacl_Hash_Blake2b_Simd256_malloc_with_key(void) +Lib_IntVector_Intrinsics_vec256 *Hacl_Hash_Blake2b_Simd256_malloc_internal_state_with_key(void) { Lib_IntVector_Intrinsics_vec256 *buf = (Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32, sizeof (Lib_IntVector_Intrinsics_vec256) * 4U); - memset(buf, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); + if (buf != NULL) + { + memset(buf, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); + } return buf; } +void +Hacl_Hash_Blake2b_Simd256_update_multi_no_inline( + Lib_IntVector_Intrinsics_vec256 *s, + FStar_UInt128_uint128 ev, + uint8_t *blocks, + uint32_t n +) +{ + KRML_PRE_ALIGN(32) Lib_IntVector_Intrinsics_vec256 wv[4U] KRML_POST_ALIGN(32) = { 0U }; + Hacl_Hash_Blake2b_Simd256_update_multi(n * 128U, wv, s, ev, blocks, n); +} + +void +Hacl_Hash_Blake2b_Simd256_update_last_no_inline( + Lib_IntVector_Intrinsics_vec256 *s, + FStar_UInt128_uint128 prev, + uint8_t *input, + uint32_t input_len +) +{ + KRML_PRE_ALIGN(32) Lib_IntVector_Intrinsics_vec256 wv[4U] KRML_POST_ALIGN(32) = { 0U }; + Hacl_Hash_Blake2b_Simd256_update_last(input_len, wv, s, false, prev, input_len, input); +} + +void +Hacl_Hash_Blake2b_Simd256_copy_internal_state( + Lib_IntVector_Intrinsics_vec256 *src, + Lib_IntVector_Intrinsics_vec256 *dst +) +{ + memcpy(dst, src, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); +} + +typedef struct +option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256____s +{ + Hacl_Streaming_Types_optional tag; + Hacl_Hash_Blake2b_Simd256_block_state_t v; +} +option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___; + static Hacl_Hash_Blake2b_Simd256_state_t *malloc_raw(Hacl_Hash_Blake2b_index kk, Hacl_Hash_Blake2b_params_and_key key) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } + uint8_t *buf1 = buf; Lib_IntVector_Intrinsics_vec256 - *wv = - (Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32, - sizeof (Lib_IntVector_Intrinsics_vec256) * 4U); - memset(wv, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); - Lib_IntVector_Intrinsics_vec256 - *b = + *wv0 = (Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32, sizeof (Lib_IntVector_Intrinsics_vec256) * 4U); - memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); - Hacl_Hash_Blake2b_Simd256_block_state_t - block_state = - { - .fst = kk.key_length, - .snd = kk.digest_length, - .thd = kk.last_node, - .f3 = { .fst = wv, .snd = b } - }; - uint8_t kk10 = kk.key_length; - uint32_t ite; - if (kk10 != 0U) + if (wv0 != NULL) { - ite = 128U; + memset(wv0, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); + } + option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___ + block_state; + if (wv0 == NULL) + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){ + .tag = Hacl_Streaming_Types_None + } + ); } else { - ite = 0U; + Lib_IntVector_Intrinsics_vec256 + *b = + (Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32, + sizeof (Lib_IntVector_Intrinsics_vec256) * 4U); + if (b != NULL) + { + memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); + } + if (b == NULL) + { + KRML_ALIGNED_FREE(wv0); + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){ + .tag = Hacl_Streaming_Types_Some, + .v = { + .fst = kk.key_length, + .snd = kk.digest_length, + .thd = kk.last_node, + .f3 = { .fst = wv0, .snd = b } + } + } + ); + } } - Hacl_Hash_Blake2b_Simd256_state_t - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)ite }; - Hacl_Hash_Blake2b_Simd256_state_t - *p = - (Hacl_Hash_Blake2b_Simd256_state_t *)KRML_HOST_MALLOC(sizeof ( - Hacl_Hash_Blake2b_Simd256_state_t - )); - p[0U] = s; - Hacl_Hash_Blake2b_blake2_params *p1 = key.fst; - uint8_t kk1 = p1->key_length; - uint8_t nn = p1->digest_length; - bool last_node = block_state.thd; - Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; - Lib_IntVector_Intrinsics_vec256 *h = block_state.f3.snd; - uint32_t kk20 = (uint32_t)i.key_length; - uint8_t *k_1 = key.snd; - if (!(kk20 == 0U)) + if (block_state.tag == Hacl_Streaming_Types_None) { - uint8_t *sub_b = buf + kk20; - memset(sub_b, 0U, (128U - kk20) * sizeof (uint8_t)); - memcpy(buf, k_1, kk20 * sizeof (uint8_t)); + KRML_HOST_FREE(buf1); + return NULL; } - Hacl_Hash_Blake2b_blake2_params pv = p1[0U]; - uint64_t tmp[8U] = { 0U }; - Lib_IntVector_Intrinsics_vec256 *r0 = h; - Lib_IntVector_Intrinsics_vec256 *r1 = h + 1U; - Lib_IntVector_Intrinsics_vec256 *r2 = h + 2U; - Lib_IntVector_Intrinsics_vec256 *r3 = h + 3U; - uint64_t iv0 = Hacl_Hash_Blake2b_ivTable_B[0U]; - uint64_t iv1 = Hacl_Hash_Blake2b_ivTable_B[1U]; - uint64_t iv2 = Hacl_Hash_Blake2b_ivTable_B[2U]; - uint64_t iv3 = Hacl_Hash_Blake2b_ivTable_B[3U]; - uint64_t iv4 = Hacl_Hash_Blake2b_ivTable_B[4U]; - uint64_t iv5 = Hacl_Hash_Blake2b_ivTable_B[5U]; - uint64_t iv6 = Hacl_Hash_Blake2b_ivTable_B[6U]; - uint64_t iv7 = Hacl_Hash_Blake2b_ivTable_B[7U]; - r2[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0, iv1, iv2, iv3); - r3[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7); - uint8_t kk2 = pv.key_length; - uint8_t nn1 = pv.digest_length; - KRML_MAYBE_FOR2(i0, - 0U, - 2U, - 1U, - uint64_t *os = tmp + 4U; - uint8_t *bj = pv.salt + i0 * 8U; - uint64_t u = load64_le(bj); - uint64_t r4 = u; - uint64_t x = r4; - os[i0] = x;); - KRML_MAYBE_FOR2(i0, - 0U, - 2U, - 1U, - uint64_t *os = tmp + 6U; - uint8_t *bj = pv.personal + i0 * 8U; - uint64_t u = load64_le(bj); - uint64_t r4 = u; - uint64_t x = r4; - os[i0] = x;); - tmp[0U] = - (uint64_t)nn1 - ^ - ((uint64_t)kk2 - << 8U - ^ ((uint64_t)pv.fanout << 16U ^ ((uint64_t)pv.depth << 24U ^ (uint64_t)pv.leaf_length << 32U))); - tmp[1U] = pv.node_offset; - tmp[2U] = (uint64_t)pv.node_depth ^ (uint64_t)pv.inner_length << 8U; - tmp[3U] = 0ULL; - uint64_t tmp0 = tmp[0U]; - uint64_t tmp1 = tmp[1U]; - uint64_t tmp2 = tmp[2U]; - uint64_t tmp3 = tmp[3U]; - uint64_t tmp4 = tmp[4U]; - uint64_t tmp5 = tmp[5U]; - uint64_t tmp6 = tmp[6U]; - uint64_t tmp7 = tmp[7U]; - uint64_t iv0_ = iv0 ^ tmp0; - uint64_t iv1_ = iv1 ^ tmp1; - uint64_t iv2_ = iv2 ^ tmp2; - uint64_t iv3_ = iv3 ^ tmp3; - uint64_t iv4_ = iv4 ^ tmp4; - uint64_t iv5_ = iv5 ^ tmp5; - uint64_t iv6_ = iv6 ^ tmp6; - uint64_t iv7_ = iv7 ^ tmp7; - r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1_, iv2_, iv3_); - r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4_, iv5_, iv6_, iv7_); - return p; + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_Blake2b_Simd256_block_state_t block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + uint8_t kk10 = kk.key_length; + uint32_t ite; + if (kk10 != 0U) + { + ite = 128U; + } + else + { + ite = 0U; + } + Hacl_Hash_Blake2b_Simd256_state_t + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)ite }; + Hacl_Hash_Blake2b_Simd256_state_t + *p = + (Hacl_Hash_Blake2b_Simd256_state_t *)KRML_HOST_MALLOC(sizeof ( + Hacl_Hash_Blake2b_Simd256_state_t + )); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + Lib_IntVector_Intrinsics_vec256 *b = block_state1.f3.snd; + Lib_IntVector_Intrinsics_vec256 *wv = block_state1.f3.fst; + KRML_ALIGNED_FREE(wv); + KRML_ALIGNED_FREE(b); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_Blake2b_blake2_params *p1 = key.fst; + uint8_t kk1 = p1->key_length; + uint8_t nn = p1->digest_length; + bool last_node = block_state1.thd; + Hacl_Hash_Blake2b_index + i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; + Lib_IntVector_Intrinsics_vec256 *h = block_state1.f3.snd; + uint32_t kk20 = (uint32_t)i.key_length; + uint8_t *k_2 = key.snd; + if (!(kk20 == 0U)) + { + uint8_t *sub_b = buf1 + kk20; + memset(sub_b, 0U, (128U - kk20) * sizeof (uint8_t)); + memcpy(buf1, k_2, kk20 * sizeof (uint8_t)); + } + Hacl_Hash_Blake2b_blake2_params pv = p1[0U]; + uint64_t tmp[8U] = { 0U }; + Lib_IntVector_Intrinsics_vec256 *r0 = h; + Lib_IntVector_Intrinsics_vec256 *r1 = h + 1U; + Lib_IntVector_Intrinsics_vec256 *r2 = h + 2U; + Lib_IntVector_Intrinsics_vec256 *r3 = h + 3U; + uint64_t iv0 = Hacl_Hash_Blake2b_ivTable_B[0U]; + uint64_t iv1 = Hacl_Hash_Blake2b_ivTable_B[1U]; + uint64_t iv2 = Hacl_Hash_Blake2b_ivTable_B[2U]; + uint64_t iv3 = Hacl_Hash_Blake2b_ivTable_B[3U]; + uint64_t iv4 = Hacl_Hash_Blake2b_ivTable_B[4U]; + uint64_t iv5 = Hacl_Hash_Blake2b_ivTable_B[5U]; + uint64_t iv6 = Hacl_Hash_Blake2b_ivTable_B[6U]; + uint64_t iv7 = Hacl_Hash_Blake2b_ivTable_B[7U]; + r2[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0, iv1, iv2, iv3); + r3[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7); + uint8_t kk2 = pv.key_length; + uint8_t nn1 = pv.digest_length; + KRML_MAYBE_FOR2(i0, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 4U; + uint8_t *bj = pv.salt + i0 * 8U; + uint64_t u = load64_le(bj); + uint64_t r4 = u; + uint64_t x = r4; + os[i0] = x;); + KRML_MAYBE_FOR2(i0, + 0U, + 2U, + 1U, + uint64_t *os = tmp + 6U; + uint8_t *bj = pv.personal + i0 * 8U; + uint64_t u = load64_le(bj); + uint64_t r4 = u; + uint64_t x = r4; + os[i0] = x;); + tmp[0U] = + (uint64_t)nn1 + ^ + ((uint64_t)kk2 + << 8U + ^ + ((uint64_t)pv.fanout + << 16U + ^ ((uint64_t)pv.depth << 24U ^ (uint64_t)pv.leaf_length << 32U))); + tmp[1U] = pv.node_offset; + tmp[2U] = (uint64_t)pv.node_depth ^ (uint64_t)pv.inner_length << 8U; + tmp[3U] = 0ULL; + uint64_t tmp0 = tmp[0U]; + uint64_t tmp1 = tmp[1U]; + uint64_t tmp2 = tmp[2U]; + uint64_t tmp3 = tmp[3U]; + uint64_t tmp4 = tmp[4U]; + uint64_t tmp5 = tmp[5U]; + uint64_t tmp6 = tmp[6U]; + uint64_t tmp7 = tmp[7U]; + uint64_t iv0_ = iv0 ^ tmp0; + uint64_t iv1_ = iv1 ^ tmp1; + uint64_t iv2_ = iv2 ^ tmp2; + uint64_t iv3_ = iv3 ^ tmp3; + uint64_t iv4_ = iv4 ^ tmp4; + uint64_t iv5_ = iv5 ^ tmp5; + uint64_t iv6_ = iv6 ^ tmp6; + uint64_t iv7_ = iv7 ^ tmp7; + r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1_, iv2_, iv3_); + r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4_, iv5_, iv6_, iv7_); + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** @@ -695,7 +831,7 @@ The caller must satisfy the following requirements. */ Hacl_Hash_Blake2b_Simd256_state_t -*Hacl_Hash_Blake2b_Simd256_malloc_with_key0(uint8_t *k, uint8_t kk) +*Hacl_Hash_Blake2b_Simd256_malloc_with_key(uint8_t *k, uint8_t kk) { uint8_t nn = 64U; Hacl_Hash_Blake2b_index i = { .key_length = kk, .digest_length = nn, .last_node = false }; @@ -721,7 +857,7 @@ use Blake2 as a hash function. Further resettings of the state SHALL be done wit */ Hacl_Hash_Blake2b_Simd256_state_t *Hacl_Hash_Blake2b_Simd256_malloc(void) { - return Hacl_Hash_Blake2b_Simd256_malloc_with_key0(NULL, 0U); + return Hacl_Hash_Blake2b_Simd256_malloc_with_key(NULL, 0U); } static Hacl_Hash_Blake2b_index index_of_state(Hacl_Hash_Blake2b_Simd256_state_t *s) @@ -967,7 +1103,7 @@ Hacl_Hash_Blake2b_Simd256_update( if (!(sz1 == 0U)) { uint64_t prevlen = total_len1 - (uint64_t)sz1; - K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ acc = block_state1.f3; + Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = block_state1.f3; Lib_IntVector_Intrinsics_vec256 *wv = acc.fst; Lib_IntVector_Intrinsics_vec256 *hash = acc.snd; uint32_t nb = 1U; @@ -992,7 +1128,7 @@ Hacl_Hash_Blake2b_Simd256_update( uint32_t data2_len = chunk_len - data1_len; uint8_t *data1 = chunk; uint8_t *data2 = chunk + data1_len; - K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ acc = block_state1.f3; + Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = block_state1.f3; Lib_IntVector_Intrinsics_vec256 *wv = acc.fst; Lib_IntVector_Intrinsics_vec256 *hash = acc.snd; uint32_t nb = data1_len / 128U; @@ -1060,7 +1196,7 @@ Hacl_Hash_Blake2b_Simd256_update( if (!(sz1 == 0U)) { uint64_t prevlen = total_len1 - (uint64_t)sz1; - K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ acc = block_state1.f3; + Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = block_state1.f3; Lib_IntVector_Intrinsics_vec256 *wv = acc.fst; Lib_IntVector_Intrinsics_vec256 *hash = acc.snd; uint32_t nb = 1U; @@ -1086,7 +1222,7 @@ Hacl_Hash_Blake2b_Simd256_update( uint32_t data2_len = chunk_len - diff - data1_len; uint8_t *data1 = chunk2; uint8_t *data2 = chunk2 + data1_len; - K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ acc = block_state1.f3; + Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = block_state1.f3; Lib_IntVector_Intrinsics_vec256 *wv = acc.fst; Lib_IntVector_Intrinsics_vec256 *hash = acc.snd; uint32_t nb = data1_len / 128U; @@ -1169,8 +1305,7 @@ uint8_t Hacl_Hash_Blake2b_Simd256_digest(Hacl_Hash_Blake2b_Simd256_state_t *s, u } uint8_t *buf_last = buf_1 + r - ite; uint8_t *buf_multi = buf_1; - K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ - acc0 = tmp_block_state.f3; + Hacl_Hash_Blake2b_Simd256_two_2b_256 acc0 = tmp_block_state.f3; Lib_IntVector_Intrinsics_vec256 *wv1 = acc0.fst; Lib_IntVector_Intrinsics_vec256 *hash0 = acc0.snd; uint32_t nb = 0U; @@ -1181,8 +1316,7 @@ uint8_t Hacl_Hash_Blake2b_Simd256_digest(Hacl_Hash_Blake2b_Simd256_state_t *s, u buf_multi, nb); uint64_t prev_len_last = total_len - (uint64_t)r; - K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ - acc = tmp_block_state.f3; + Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = tmp_block_state.f3; bool last_node1 = tmp_block_state.thd; Lib_IntVector_Intrinsics_vec256 *wv = acc.fst; Lib_IntVector_Intrinsics_vec256 *hash = acc.snd; @@ -1244,37 +1378,120 @@ Hacl_Hash_Blake2b_Simd256_state_t uint8_t kk1 = block_state0.fst; Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } memcpy(buf, buf0, 128U * sizeof (uint8_t)); Lib_IntVector_Intrinsics_vec256 - *wv = + *wv0 = (Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32, sizeof (Lib_IntVector_Intrinsics_vec256) * 4U); - memset(wv, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); - Lib_IntVector_Intrinsics_vec256 - *b = - (Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32, - sizeof (Lib_IntVector_Intrinsics_vec256) * 4U); - memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); - Hacl_Hash_Blake2b_Simd256_block_state_t - block_state = + if (wv0 != NULL) + { + memset(wv0, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); + } + option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___ + block_state; + if (wv0 == NULL) + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + Lib_IntVector_Intrinsics_vec256 + *b = + (Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32, + sizeof (Lib_IntVector_Intrinsics_vec256) * 4U); + if (b != NULL) { - .fst = i.key_length, - .snd = i.digest_length, - .thd = i.last_node, - .f3 = { .fst = wv, .snd = b } - }; - Lib_IntVector_Intrinsics_vec256 *src_b = block_state0.f3.snd; - Lib_IntVector_Intrinsics_vec256 *dst_b = block_state.f3.snd; - memcpy(dst_b, src_b, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); - Hacl_Hash_Blake2b_Simd256_state_t - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Hash_Blake2b_Simd256_state_t - *p = - (Hacl_Hash_Blake2b_Simd256_state_t *)KRML_HOST_MALLOC(sizeof ( - Hacl_Hash_Blake2b_Simd256_state_t - )); - p[0U] = s; - return p; + memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); + } + if (b == NULL) + { + KRML_ALIGNED_FREE(wv0); + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){ + .tag = Hacl_Streaming_Types_Some, + .v = { + .fst = i.key_length, + .snd = i.digest_length, + .thd = i.last_node, + .f3 = { .fst = wv0, .snd = b } + } + } + ); + } + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_Blake2b_Simd256_block_state_t block_state1 = block_state.v; + Lib_IntVector_Intrinsics_vec256 *src_b = block_state0.f3.snd; + Lib_IntVector_Intrinsics_vec256 *dst_b = block_state1.f3.snd; + memcpy(dst_b, src_b, 4U * sizeof (Lib_IntVector_Intrinsics_vec256)); + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Hash_Blake2b_Simd256_state_t + s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 }; + Hacl_Hash_Blake2b_Simd256_state_t + *p = + (Hacl_Hash_Blake2b_Simd256_state_t *)KRML_HOST_MALLOC(sizeof ( + Hacl_Hash_Blake2b_Simd256_state_t + )); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + Lib_IntVector_Intrinsics_vec256 *b = block_state1.f3.snd; + Lib_IntVector_Intrinsics_vec256 *wv = block_state1.f3.fst; + KRML_ALIGNED_FREE(wv); + KRML_ALIGNED_FREE(b); + KRML_HOST_FREE(buf); + return NULL; + } + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** diff --git a/Modules/_hacl/Hacl_Hash_Blake2b_Simd256.h b/Modules/_hacl/Hacl_Hash_Blake2b_Simd256.h index 6c11a4ba32134a..0271ab8e024e51 100644 --- a/Modules/_hacl/Hacl_Hash_Blake2b_Simd256.h +++ b/Modules/_hacl/Hacl_Hash_Blake2b_Simd256.h @@ -32,14 +32,12 @@ extern "C" { #include #include "python_hacl_namespaces.h" -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" #include "Hacl_Streaming_Types.h" - #include "Hacl_Hash_Blake2b.h" -#include "libintvector.h" #define HACL_HASH_BLAKE2B_SIMD256_BLOCK_BYTES (128U) @@ -51,29 +49,10 @@ extern "C" { #define HACL_HASH_BLAKE2B_SIMD256_PERSONAL_BYTES (16U) -typedef struct K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256__s -{ - Lib_IntVector_Intrinsics_vec256 *fst; - Lib_IntVector_Intrinsics_vec256 *snd; -} -K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_; - typedef struct Hacl_Hash_Blake2b_Simd256_block_state_t_s -{ - uint8_t fst; - uint8_t snd; - bool thd; - K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ f3; -} Hacl_Hash_Blake2b_Simd256_block_state_t; -typedef struct Hacl_Hash_Blake2b_Simd256_state_t_s -{ - Hacl_Hash_Blake2b_Simd256_block_state_t block_state; - uint8_t *buf; - uint64_t total_len; -} -Hacl_Hash_Blake2b_Simd256_state_t; +typedef struct Hacl_Hash_Blake2b_Simd256_state_t_s Hacl_Hash_Blake2b_Simd256_state_t; /** General-purpose allocation function that gives control over all @@ -109,7 +88,7 @@ The caller must satisfy the following requirements. */ Hacl_Hash_Blake2b_Simd256_state_t -*Hacl_Hash_Blake2b_Simd256_malloc_with_key0(uint8_t *k, uint8_t kk); +*Hacl_Hash_Blake2b_Simd256_malloc_with_key(uint8_t *k, uint8_t kk); /** Specialized allocation function that picks default values for all diff --git a/Modules/_hacl/Hacl_Hash_Blake2s.c b/Modules/_hacl/Hacl_Hash_Blake2s.c index ceb7385072e048..730ba135afb2fb 100644 --- a/Modules/_hacl/Hacl_Hash_Blake2s.c +++ b/Modules/_hacl/Hacl_Hash_Blake2s.c @@ -25,6 +25,9 @@ #include "internal/Hacl_Hash_Blake2s.h" +#include "Hacl_Streaming_Types.h" +#include "Hacl_Hash_Blake2b.h" +#include "internal/Hacl_Streaming_Types.h" #include "internal/Hacl_Impl_Blake2_Constants.h" #include "internal/Hacl_Hash_Blake2b.h" #include "lib_memzero0.h" @@ -685,124 +688,212 @@ void Hacl_Hash_Blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash) Lib_Memzero0_memzero(b, 32U, uint8_t, void *); } +typedef struct option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t____s +{ + Hacl_Streaming_Types_optional tag; + Hacl_Hash_Blake2s_block_state_t v; +} +option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___; + static Hacl_Hash_Blake2s_state_t *malloc_raw(Hacl_Hash_Blake2b_index kk, Hacl_Hash_Blake2b_params_and_key key) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); - uint32_t *wv = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t)); - uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t)); - Hacl_Hash_Blake2s_block_state_t - block_state = - { - .fst = kk.key_length, - .snd = kk.digest_length, - .thd = kk.last_node, - .f3 = { .fst = wv, .snd = b } - }; - uint8_t kk10 = kk.key_length; - uint32_t ite; - if (kk10 != 0U) + if (buf == NULL) { - ite = 64U; + return NULL; + } + uint8_t *buf1 = buf; + uint32_t *wv0 = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t)); + option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___ block_state; + if (wv0 == NULL) + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){ + .tag = Hacl_Streaming_Types_None + } + ); } else { - ite = 0U; + uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t)); + if (b == NULL) + { + KRML_HOST_FREE(wv0); + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){ + .tag = Hacl_Streaming_Types_Some, + .v = { + .fst = kk.key_length, + .snd = kk.digest_length, + .thd = kk.last_node, + .f3 = { .fst = wv0, .snd = b } + } + } + ); + } } - Hacl_Hash_Blake2s_state_t - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)ite }; - Hacl_Hash_Blake2s_state_t - *p = (Hacl_Hash_Blake2s_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2s_state_t)); - p[0U] = s; - Hacl_Hash_Blake2b_blake2_params *p1 = key.fst; - uint8_t kk1 = p1->key_length; - uint8_t nn = p1->digest_length; - bool last_node = block_state.thd; - Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; - uint32_t *h = block_state.f3.snd; - uint32_t kk2 = (uint32_t)i.key_length; - uint8_t *k_1 = key.snd; - if (!(kk2 == 0U)) + if (block_state.tag == Hacl_Streaming_Types_None) { - uint8_t *sub_b = buf + kk2; - memset(sub_b, 0U, (64U - kk2) * sizeof (uint8_t)); - memcpy(buf, k_1, kk2 * sizeof (uint8_t)); + KRML_HOST_FREE(buf1); + return NULL; } - Hacl_Hash_Blake2b_blake2_params pv = p1[0U]; - uint32_t tmp[8U] = { 0U }; - uint32_t *r0 = h; - uint32_t *r1 = h + 4U; - uint32_t *r2 = h + 8U; - uint32_t *r3 = h + 12U; - uint32_t iv0 = Hacl_Hash_Blake2b_ivTable_S[0U]; - uint32_t iv1 = Hacl_Hash_Blake2b_ivTable_S[1U]; - uint32_t iv2 = Hacl_Hash_Blake2b_ivTable_S[2U]; - uint32_t iv3 = Hacl_Hash_Blake2b_ivTable_S[3U]; - uint32_t iv4 = Hacl_Hash_Blake2b_ivTable_S[4U]; - uint32_t iv5 = Hacl_Hash_Blake2b_ivTable_S[5U]; - uint32_t iv6 = Hacl_Hash_Blake2b_ivTable_S[6U]; - uint32_t iv7 = Hacl_Hash_Blake2b_ivTable_S[7U]; - r2[0U] = iv0; - r2[1U] = iv1; - r2[2U] = iv2; - r2[3U] = iv3; - r3[0U] = iv4; - r3[1U] = iv5; - r3[2U] = iv6; - r3[3U] = iv7; - KRML_MAYBE_FOR2(i0, - 0U, - 2U, - 1U, - uint32_t *os = tmp + 4U; - uint8_t *bj = pv.salt + i0 * 4U; - uint32_t u = load32_le(bj); - uint32_t r4 = u; - uint32_t x = r4; - os[i0] = x;); - KRML_MAYBE_FOR2(i0, - 0U, - 2U, - 1U, - uint32_t *os = tmp + 6U; - uint8_t *bj = pv.personal + i0 * 4U; - uint32_t u = load32_le(bj); - uint32_t r4 = u; - uint32_t x = r4; - os[i0] = x;); - tmp[0U] = - (uint32_t)pv.digest_length - ^ ((uint32_t)pv.key_length << 8U ^ ((uint32_t)pv.fanout << 16U ^ (uint32_t)pv.depth << 24U)); - tmp[1U] = pv.leaf_length; - tmp[2U] = (uint32_t)pv.node_offset; - tmp[3U] = - (uint32_t)(pv.node_offset >> 32U) - ^ ((uint32_t)pv.node_depth << 16U ^ (uint32_t)pv.inner_length << 24U); - uint32_t tmp0 = tmp[0U]; - uint32_t tmp1 = tmp[1U]; - uint32_t tmp2 = tmp[2U]; - uint32_t tmp3 = tmp[3U]; - uint32_t tmp4 = tmp[4U]; - uint32_t tmp5 = tmp[5U]; - uint32_t tmp6 = tmp[6U]; - uint32_t tmp7 = tmp[7U]; - uint32_t iv0_ = iv0 ^ tmp0; - uint32_t iv1_ = iv1 ^ tmp1; - uint32_t iv2_ = iv2 ^ tmp2; - uint32_t iv3_ = iv3 ^ tmp3; - uint32_t iv4_ = iv4 ^ tmp4; - uint32_t iv5_ = iv5 ^ tmp5; - uint32_t iv6_ = iv6 ^ tmp6; - uint32_t iv7_ = iv7 ^ tmp7; - r0[0U] = iv0_; - r0[1U] = iv1_; - r0[2U] = iv2_; - r0[3U] = iv3_; - r1[0U] = iv4_; - r1[1U] = iv5_; - r1[2U] = iv6_; - r1[3U] = iv7_; - return p; + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_Blake2s_block_state_t block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + uint8_t kk10 = kk.key_length; + uint32_t ite; + if (kk10 != 0U) + { + ite = 64U; + } + else + { + ite = 0U; + } + Hacl_Hash_Blake2s_state_t + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)ite }; + Hacl_Hash_Blake2s_state_t + *p = (Hacl_Hash_Blake2s_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2s_state_t)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + uint32_t *b = block_state1.f3.snd; + uint32_t *wv = block_state1.f3.fst; + KRML_HOST_FREE(wv); + KRML_HOST_FREE(b); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_Blake2b_blake2_params *p1 = key.fst; + uint8_t kk1 = p1->key_length; + uint8_t nn = p1->digest_length; + bool last_node = block_state1.thd; + Hacl_Hash_Blake2b_index + i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; + uint32_t *h = block_state1.f3.snd; + uint32_t kk2 = (uint32_t)i.key_length; + uint8_t *k_2 = key.snd; + if (!(kk2 == 0U)) + { + uint8_t *sub_b = buf1 + kk2; + memset(sub_b, 0U, (64U - kk2) * sizeof (uint8_t)); + memcpy(buf1, k_2, kk2 * sizeof (uint8_t)); + } + Hacl_Hash_Blake2b_blake2_params pv = p1[0U]; + uint32_t tmp[8U] = { 0U }; + uint32_t *r0 = h; + uint32_t *r1 = h + 4U; + uint32_t *r2 = h + 8U; + uint32_t *r3 = h + 12U; + uint32_t iv0 = Hacl_Hash_Blake2b_ivTable_S[0U]; + uint32_t iv1 = Hacl_Hash_Blake2b_ivTable_S[1U]; + uint32_t iv2 = Hacl_Hash_Blake2b_ivTable_S[2U]; + uint32_t iv3 = Hacl_Hash_Blake2b_ivTable_S[3U]; + uint32_t iv4 = Hacl_Hash_Blake2b_ivTable_S[4U]; + uint32_t iv5 = Hacl_Hash_Blake2b_ivTable_S[5U]; + uint32_t iv6 = Hacl_Hash_Blake2b_ivTable_S[6U]; + uint32_t iv7 = Hacl_Hash_Blake2b_ivTable_S[7U]; + r2[0U] = iv0; + r2[1U] = iv1; + r2[2U] = iv2; + r2[3U] = iv3; + r3[0U] = iv4; + r3[1U] = iv5; + r3[2U] = iv6; + r3[3U] = iv7; + KRML_MAYBE_FOR2(i0, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 4U; + uint8_t *bj = pv.salt + i0 * 4U; + uint32_t u = load32_le(bj); + uint32_t r4 = u; + uint32_t x = r4; + os[i0] = x;); + KRML_MAYBE_FOR2(i0, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 6U; + uint8_t *bj = pv.personal + i0 * 4U; + uint32_t u = load32_le(bj); + uint32_t r4 = u; + uint32_t x = r4; + os[i0] = x;); + tmp[0U] = + (uint32_t)pv.digest_length + ^ + ((uint32_t)pv.key_length + << 8U + ^ ((uint32_t)pv.fanout << 16U ^ (uint32_t)pv.depth << 24U)); + tmp[1U] = pv.leaf_length; + tmp[2U] = (uint32_t)pv.node_offset; + tmp[3U] = + (uint32_t)(pv.node_offset >> 32U) + ^ ((uint32_t)pv.node_depth << 16U ^ (uint32_t)pv.inner_length << 24U); + uint32_t tmp0 = tmp[0U]; + uint32_t tmp1 = tmp[1U]; + uint32_t tmp2 = tmp[2U]; + uint32_t tmp3 = tmp[3U]; + uint32_t tmp4 = tmp[4U]; + uint32_t tmp5 = tmp[5U]; + uint32_t tmp6 = tmp[6U]; + uint32_t tmp7 = tmp[7U]; + uint32_t iv0_ = iv0 ^ tmp0; + uint32_t iv1_ = iv1 ^ tmp1; + uint32_t iv2_ = iv2 ^ tmp2; + uint32_t iv3_ = iv3 ^ tmp3; + uint32_t iv4_ = iv4 ^ tmp4; + uint32_t iv5_ = iv5 ^ tmp5; + uint32_t iv6_ = iv6 ^ tmp6; + uint32_t iv7_ = iv7 ^ tmp7; + r0[0U] = iv0_; + r0[1U] = iv1_; + r0[2U] = iv2_; + r0[3U] = iv3_; + r1[0U] = iv4_; + r1[1U] = iv5_; + r1[2U] = iv6_; + r1[3U] = iv7_; + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** @@ -1362,26 +1453,102 @@ Hacl_Hash_Blake2s_state_t *Hacl_Hash_Blake2s_copy(Hacl_Hash_Blake2s_state_t *sta uint8_t kk1 = block_state0.fst; Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } memcpy(buf, buf0, 64U * sizeof (uint8_t)); - uint32_t *wv = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t)); - uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t)); - Hacl_Hash_Blake2s_block_state_t - block_state = + uint32_t *wv0 = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t)); + option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___ block_state; + if (wv0 == NULL) + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t)); + if (b == NULL) { - .fst = i.key_length, - .snd = i.digest_length, - .thd = i.last_node, - .f3 = { .fst = wv, .snd = b } - }; - uint32_t *src_b = block_state0.f3.snd; - uint32_t *dst_b = block_state.f3.snd; - memcpy(dst_b, src_b, 16U * sizeof (uint32_t)); - Hacl_Hash_Blake2s_state_t - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Hash_Blake2s_state_t - *p = (Hacl_Hash_Blake2s_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2s_state_t)); - p[0U] = s; - return p; + KRML_HOST_FREE(wv0); + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){ + .tag = Hacl_Streaming_Types_Some, + .v = { + .fst = i.key_length, + .snd = i.digest_length, + .thd = i.last_node, + .f3 = { .fst = wv0, .snd = b } + } + } + ); + } + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_Blake2s_block_state_t block_state1 = block_state.v; + uint32_t *src_b = block_state0.f3.snd; + uint32_t *dst_b = block_state1.f3.snd; + memcpy(dst_b, src_b, 16U * sizeof (uint32_t)); + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Hash_Blake2s_state_t + s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 }; + Hacl_Hash_Blake2s_state_t + *p = (Hacl_Hash_Blake2s_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2s_state_t)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + uint32_t *b = block_state1.f3.snd; + uint32_t *wv = block_state1.f3.fst; + KRML_HOST_FREE(wv); + KRML_HOST_FREE(b); + KRML_HOST_FREE(buf); + return NULL; + } + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** diff --git a/Modules/_hacl/Hacl_Hash_Blake2s.h b/Modules/_hacl/Hacl_Hash_Blake2s.h index 5c01da144018e3..fbf8cff5cd1073 100644 --- a/Modules/_hacl/Hacl_Hash_Blake2s.h +++ b/Modules/_hacl/Hacl_Hash_Blake2s.h @@ -32,7 +32,7 @@ extern "C" { #include #include "python_hacl_namespaces.h" -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" @@ -49,29 +49,9 @@ extern "C" { #define HACL_HASH_BLAKE2S_PERSONAL_BYTES (8U) -typedef struct K____uint32_t___uint32_t__s -{ - uint32_t *fst; - uint32_t *snd; -} -K____uint32_t___uint32_t_; - -typedef struct Hacl_Hash_Blake2s_block_state_t_s -{ - uint8_t fst; - uint8_t snd; - bool thd; - K____uint32_t___uint32_t_ f3; -} -Hacl_Hash_Blake2s_block_state_t; +typedef struct Hacl_Hash_Blake2s_block_state_t_s Hacl_Hash_Blake2s_block_state_t; -typedef struct Hacl_Hash_Blake2s_state_t_s -{ - Hacl_Hash_Blake2s_block_state_t block_state; - uint8_t *buf; - uint64_t total_len; -} -Hacl_Hash_Blake2s_state_t; +typedef struct Hacl_Hash_Blake2s_state_t_s Hacl_Hash_Blake2s_state_t; /** General-purpose allocation function that gives control over all diff --git a/Modules/_hacl/Hacl_Hash_Blake2s_Simd128.c b/Modules/_hacl/Hacl_Hash_Blake2s_Simd128.c index 3b68783bfad9b4..7e9cd79544f8f1 100644 --- a/Modules/_hacl/Hacl_Hash_Blake2s_Simd128.c +++ b/Modules/_hacl/Hacl_Hash_Blake2s_Simd128.c @@ -25,6 +25,9 @@ #include "internal/Hacl_Hash_Blake2s_Simd128.h" +#include "Hacl_Streaming_Types.h" +#include "Hacl_Hash_Blake2b.h" +#include "internal/Hacl_Streaming_Types.h" #include "internal/Hacl_Impl_Blake2_Constants.h" #include "internal/Hacl_Hash_Blake2b.h" #include "lib_memzero0.h" @@ -516,133 +519,265 @@ Hacl_Hash_Blake2s_Simd128_load_state128s_from_state32( r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(b3[0U], b3[1U], b3[2U], b3[3U]); } -Lib_IntVector_Intrinsics_vec128 *Hacl_Hash_Blake2s_Simd128_malloc_with_key(void) +Lib_IntVector_Intrinsics_vec128 *Hacl_Hash_Blake2s_Simd128_malloc_internal_state_with_key(void) { Lib_IntVector_Intrinsics_vec128 *buf = (Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16, sizeof (Lib_IntVector_Intrinsics_vec128) * 4U); - memset(buf, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); + if (buf != NULL) + { + memset(buf, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); + } return buf; } +void +Hacl_Hash_Blake2s_Simd128_update_multi_no_inline( + Lib_IntVector_Intrinsics_vec128 *s, + uint64_t ev, + uint8_t *blocks, + uint32_t n +) +{ + KRML_PRE_ALIGN(16) Lib_IntVector_Intrinsics_vec128 wv[4U] KRML_POST_ALIGN(16) = { 0U }; + Hacl_Hash_Blake2s_Simd128_update_multi(n * 64U, wv, s, ev, blocks, n); +} + +void +Hacl_Hash_Blake2s_Simd128_update_last_no_inline( + Lib_IntVector_Intrinsics_vec128 *s, + uint64_t prev, + uint8_t *input, + uint32_t input_len +) +{ + KRML_PRE_ALIGN(16) Lib_IntVector_Intrinsics_vec128 wv[4U] KRML_POST_ALIGN(16) = { 0U }; + Hacl_Hash_Blake2s_Simd128_update_last(input_len, wv, s, false, prev, input_len, input); +} + +void +Hacl_Hash_Blake2s_Simd128_copy_internal_state( + Lib_IntVector_Intrinsics_vec128 *src, + Lib_IntVector_Intrinsics_vec128 *dst +) +{ + memcpy(dst, src, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); +} + +typedef struct +option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128____s +{ + Hacl_Streaming_Types_optional tag; + Hacl_Hash_Blake2s_Simd128_block_state_t v; +} +option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___; + static Hacl_Hash_Blake2s_Simd128_state_t *malloc_raw(Hacl_Hash_Blake2b_index kk, Hacl_Hash_Blake2b_params_and_key key) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } + uint8_t *buf1 = buf; Lib_IntVector_Intrinsics_vec128 - *wv = - (Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16, - sizeof (Lib_IntVector_Intrinsics_vec128) * 4U); - memset(wv, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); - Lib_IntVector_Intrinsics_vec128 - *b = + *wv0 = (Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16, sizeof (Lib_IntVector_Intrinsics_vec128) * 4U); - memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); - Hacl_Hash_Blake2s_Simd128_block_state_t - block_state = - { - .fst = kk.key_length, - .snd = kk.digest_length, - .thd = kk.last_node, - .f3 = { .fst = wv, .snd = b } - }; - uint8_t kk10 = kk.key_length; - uint32_t ite; - if (kk10 != 0U) + if (wv0 != NULL) { - ite = 64U; + memset(wv0, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); + } + option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___ + block_state; + if (wv0 == NULL) + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){ + .tag = Hacl_Streaming_Types_None + } + ); } else { - ite = 0U; + Lib_IntVector_Intrinsics_vec128 + *b = + (Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16, + sizeof (Lib_IntVector_Intrinsics_vec128) * 4U); + if (b != NULL) + { + memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); + } + if (b == NULL) + { + KRML_ALIGNED_FREE(wv0); + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){ + .tag = Hacl_Streaming_Types_Some, + .v = { + .fst = kk.key_length, + .snd = kk.digest_length, + .thd = kk.last_node, + .f3 = { .fst = wv0, .snd = b } + } + } + ); + } } - Hacl_Hash_Blake2s_Simd128_state_t - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)ite }; - Hacl_Hash_Blake2s_Simd128_state_t - *p = - (Hacl_Hash_Blake2s_Simd128_state_t *)KRML_HOST_MALLOC(sizeof ( - Hacl_Hash_Blake2s_Simd128_state_t - )); - p[0U] = s; - Hacl_Hash_Blake2b_blake2_params *p1 = key.fst; - uint8_t kk1 = p1->key_length; - uint8_t nn = p1->digest_length; - bool last_node = block_state.thd; - Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; - Lib_IntVector_Intrinsics_vec128 *h = block_state.f3.snd; - uint32_t kk2 = (uint32_t)i.key_length; - uint8_t *k_1 = key.snd; - if (!(kk2 == 0U)) + if (block_state.tag == Hacl_Streaming_Types_None) { - uint8_t *sub_b = buf + kk2; - memset(sub_b, 0U, (64U - kk2) * sizeof (uint8_t)); - memcpy(buf, k_1, kk2 * sizeof (uint8_t)); + KRML_HOST_FREE(buf1); + return NULL; } - Hacl_Hash_Blake2b_blake2_params pv = p1[0U]; - uint32_t tmp[8U] = { 0U }; - Lib_IntVector_Intrinsics_vec128 *r0 = h; - Lib_IntVector_Intrinsics_vec128 *r1 = h + 1U; - Lib_IntVector_Intrinsics_vec128 *r2 = h + 2U; - Lib_IntVector_Intrinsics_vec128 *r3 = h + 3U; - uint32_t iv0 = Hacl_Hash_Blake2b_ivTable_S[0U]; - uint32_t iv1 = Hacl_Hash_Blake2b_ivTable_S[1U]; - uint32_t iv2 = Hacl_Hash_Blake2b_ivTable_S[2U]; - uint32_t iv3 = Hacl_Hash_Blake2b_ivTable_S[3U]; - uint32_t iv4 = Hacl_Hash_Blake2b_ivTable_S[4U]; - uint32_t iv5 = Hacl_Hash_Blake2b_ivTable_S[5U]; - uint32_t iv6 = Hacl_Hash_Blake2b_ivTable_S[6U]; - uint32_t iv7 = Hacl_Hash_Blake2b_ivTable_S[7U]; - r2[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0, iv1, iv2, iv3); - r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7); - KRML_MAYBE_FOR2(i0, - 0U, - 2U, - 1U, - uint32_t *os = tmp + 4U; - uint8_t *bj = pv.salt + i0 * 4U; - uint32_t u = load32_le(bj); - uint32_t r4 = u; - uint32_t x = r4; - os[i0] = x;); - KRML_MAYBE_FOR2(i0, - 0U, - 2U, - 1U, - uint32_t *os = tmp + 6U; - uint8_t *bj = pv.personal + i0 * 4U; - uint32_t u = load32_le(bj); - uint32_t r4 = u; - uint32_t x = r4; - os[i0] = x;); - tmp[0U] = - (uint32_t)pv.digest_length - ^ ((uint32_t)pv.key_length << 8U ^ ((uint32_t)pv.fanout << 16U ^ (uint32_t)pv.depth << 24U)); - tmp[1U] = pv.leaf_length; - tmp[2U] = (uint32_t)pv.node_offset; - tmp[3U] = - (uint32_t)(pv.node_offset >> 32U) - ^ ((uint32_t)pv.node_depth << 16U ^ (uint32_t)pv.inner_length << 24U); - uint32_t tmp0 = tmp[0U]; - uint32_t tmp1 = tmp[1U]; - uint32_t tmp2 = tmp[2U]; - uint32_t tmp3 = tmp[3U]; - uint32_t tmp4 = tmp[4U]; - uint32_t tmp5 = tmp[5U]; - uint32_t tmp6 = tmp[6U]; - uint32_t tmp7 = tmp[7U]; - uint32_t iv0_ = iv0 ^ tmp0; - uint32_t iv1_ = iv1 ^ tmp1; - uint32_t iv2_ = iv2 ^ tmp2; - uint32_t iv3_ = iv3 ^ tmp3; - uint32_t iv4_ = iv4 ^ tmp4; - uint32_t iv5_ = iv5 ^ tmp5; - uint32_t iv6_ = iv6 ^ tmp6; - uint32_t iv7_ = iv7 ^ tmp7; - r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1_, iv2_, iv3_); - r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4_, iv5_, iv6_, iv7_); - return p; + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_Blake2s_Simd128_block_state_t block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + uint8_t kk10 = kk.key_length; + uint32_t ite; + if (kk10 != 0U) + { + ite = 64U; + } + else + { + ite = 0U; + } + Hacl_Hash_Blake2s_Simd128_state_t + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)ite }; + Hacl_Hash_Blake2s_Simd128_state_t + *p = + (Hacl_Hash_Blake2s_Simd128_state_t *)KRML_HOST_MALLOC(sizeof ( + Hacl_Hash_Blake2s_Simd128_state_t + )); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + Lib_IntVector_Intrinsics_vec128 *b = block_state1.f3.snd; + Lib_IntVector_Intrinsics_vec128 *wv = block_state1.f3.fst; + KRML_ALIGNED_FREE(wv); + KRML_ALIGNED_FREE(b); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_Blake2b_blake2_params *p1 = key.fst; + uint8_t kk1 = p1->key_length; + uint8_t nn = p1->digest_length; + bool last_node = block_state1.thd; + Hacl_Hash_Blake2b_index + i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; + Lib_IntVector_Intrinsics_vec128 *h = block_state1.f3.snd; + uint32_t kk2 = (uint32_t)i.key_length; + uint8_t *k_2 = key.snd; + if (!(kk2 == 0U)) + { + uint8_t *sub_b = buf1 + kk2; + memset(sub_b, 0U, (64U - kk2) * sizeof (uint8_t)); + memcpy(buf1, k_2, kk2 * sizeof (uint8_t)); + } + Hacl_Hash_Blake2b_blake2_params pv = p1[0U]; + uint32_t tmp[8U] = { 0U }; + Lib_IntVector_Intrinsics_vec128 *r0 = h; + Lib_IntVector_Intrinsics_vec128 *r1 = h + 1U; + Lib_IntVector_Intrinsics_vec128 *r2 = h + 2U; + Lib_IntVector_Intrinsics_vec128 *r3 = h + 3U; + uint32_t iv0 = Hacl_Hash_Blake2b_ivTable_S[0U]; + uint32_t iv1 = Hacl_Hash_Blake2b_ivTable_S[1U]; + uint32_t iv2 = Hacl_Hash_Blake2b_ivTable_S[2U]; + uint32_t iv3 = Hacl_Hash_Blake2b_ivTable_S[3U]; + uint32_t iv4 = Hacl_Hash_Blake2b_ivTable_S[4U]; + uint32_t iv5 = Hacl_Hash_Blake2b_ivTable_S[5U]; + uint32_t iv6 = Hacl_Hash_Blake2b_ivTable_S[6U]; + uint32_t iv7 = Hacl_Hash_Blake2b_ivTable_S[7U]; + r2[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0, iv1, iv2, iv3); + r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7); + KRML_MAYBE_FOR2(i0, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 4U; + uint8_t *bj = pv.salt + i0 * 4U; + uint32_t u = load32_le(bj); + uint32_t r4 = u; + uint32_t x = r4; + os[i0] = x;); + KRML_MAYBE_FOR2(i0, + 0U, + 2U, + 1U, + uint32_t *os = tmp + 6U; + uint8_t *bj = pv.personal + i0 * 4U; + uint32_t u = load32_le(bj); + uint32_t r4 = u; + uint32_t x = r4; + os[i0] = x;); + tmp[0U] = + (uint32_t)pv.digest_length + ^ + ((uint32_t)pv.key_length + << 8U + ^ ((uint32_t)pv.fanout << 16U ^ (uint32_t)pv.depth << 24U)); + tmp[1U] = pv.leaf_length; + tmp[2U] = (uint32_t)pv.node_offset; + tmp[3U] = + (uint32_t)(pv.node_offset >> 32U) + ^ ((uint32_t)pv.node_depth << 16U ^ (uint32_t)pv.inner_length << 24U); + uint32_t tmp0 = tmp[0U]; + uint32_t tmp1 = tmp[1U]; + uint32_t tmp2 = tmp[2U]; + uint32_t tmp3 = tmp[3U]; + uint32_t tmp4 = tmp[4U]; + uint32_t tmp5 = tmp[5U]; + uint32_t tmp6 = tmp[6U]; + uint32_t tmp7 = tmp[7U]; + uint32_t iv0_ = iv0 ^ tmp0; + uint32_t iv1_ = iv1 ^ tmp1; + uint32_t iv2_ = iv2 ^ tmp2; + uint32_t iv3_ = iv3 ^ tmp3; + uint32_t iv4_ = iv4 ^ tmp4; + uint32_t iv5_ = iv5 ^ tmp5; + uint32_t iv6_ = iv6 ^ tmp6; + uint32_t iv7_ = iv7 ^ tmp7; + r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1_, iv2_, iv3_); + r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4_, iv5_, iv6_, iv7_); + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** @@ -685,7 +820,7 @@ The caller must satisfy the following requirements. */ Hacl_Hash_Blake2s_Simd128_state_t -*Hacl_Hash_Blake2s_Simd128_malloc_with_key0(uint8_t *k, uint8_t kk) +*Hacl_Hash_Blake2s_Simd128_malloc_with_key(uint8_t *k, uint8_t kk) { uint8_t nn = 32U; Hacl_Hash_Blake2b_index i = { .key_length = kk, .digest_length = nn, .last_node = false }; @@ -711,7 +846,7 @@ use Blake2 as a hash function. Further resettings of the state SHALL be done wit */ Hacl_Hash_Blake2s_Simd128_state_t *Hacl_Hash_Blake2s_Simd128_malloc(void) { - return Hacl_Hash_Blake2s_Simd128_malloc_with_key0(NULL, 0U); + return Hacl_Hash_Blake2s_Simd128_malloc_with_key(NULL, 0U); } static Hacl_Hash_Blake2b_index index_of_state(Hacl_Hash_Blake2s_Simd128_state_t *s) @@ -954,7 +1089,7 @@ Hacl_Hash_Blake2s_Simd128_update( if (!(sz1 == 0U)) { uint64_t prevlen = total_len1 - (uint64_t)sz1; - K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ acc = block_state1.f3; + Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = block_state1.f3; Lib_IntVector_Intrinsics_vec128 *wv = acc.fst; Lib_IntVector_Intrinsics_vec128 *hash = acc.snd; uint32_t nb = 1U; @@ -974,7 +1109,7 @@ Hacl_Hash_Blake2s_Simd128_update( uint32_t data2_len = chunk_len - data1_len; uint8_t *data1 = chunk; uint8_t *data2 = chunk + data1_len; - K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ acc = block_state1.f3; + Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = block_state1.f3; Lib_IntVector_Intrinsics_vec128 *wv = acc.fst; Lib_IntVector_Intrinsics_vec128 *hash = acc.snd; uint32_t nb = data1_len / 64U; @@ -1037,7 +1172,7 @@ Hacl_Hash_Blake2s_Simd128_update( if (!(sz1 == 0U)) { uint64_t prevlen = total_len1 - (uint64_t)sz1; - K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ acc = block_state1.f3; + Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = block_state1.f3; Lib_IntVector_Intrinsics_vec128 *wv = acc.fst; Lib_IntVector_Intrinsics_vec128 *hash = acc.snd; uint32_t nb = 1U; @@ -1058,7 +1193,7 @@ Hacl_Hash_Blake2s_Simd128_update( uint32_t data2_len = chunk_len - diff - data1_len; uint8_t *data1 = chunk2; uint8_t *data2 = chunk2 + data1_len; - K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ acc = block_state1.f3; + Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = block_state1.f3; Lib_IntVector_Intrinsics_vec128 *wv = acc.fst; Lib_IntVector_Intrinsics_vec128 *hash = acc.snd; uint32_t nb = data1_len / 64U; @@ -1136,15 +1271,13 @@ uint8_t Hacl_Hash_Blake2s_Simd128_digest(Hacl_Hash_Blake2s_Simd128_state_t *s, u } uint8_t *buf_last = buf_1 + r - ite; uint8_t *buf_multi = buf_1; - K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ - acc0 = tmp_block_state.f3; + Hacl_Hash_Blake2s_Simd128_two_2s_128 acc0 = tmp_block_state.f3; Lib_IntVector_Intrinsics_vec128 *wv1 = acc0.fst; Lib_IntVector_Intrinsics_vec128 *hash0 = acc0.snd; uint32_t nb = 0U; Hacl_Hash_Blake2s_Simd128_update_multi(0U, wv1, hash0, prev_len, buf_multi, nb); uint64_t prev_len_last = total_len - (uint64_t)r; - K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ - acc = tmp_block_state.f3; + Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = tmp_block_state.f3; bool last_node1 = tmp_block_state.thd; Lib_IntVector_Intrinsics_vec128 *wv = acc.fst; Lib_IntVector_Intrinsics_vec128 *hash = acc.snd; @@ -1200,37 +1333,120 @@ Hacl_Hash_Blake2s_Simd128_state_t uint8_t kk1 = block_state0.fst; Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node }; uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } memcpy(buf, buf0, 64U * sizeof (uint8_t)); Lib_IntVector_Intrinsics_vec128 - *wv = + *wv0 = (Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16, sizeof (Lib_IntVector_Intrinsics_vec128) * 4U); - memset(wv, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); - Lib_IntVector_Intrinsics_vec128 - *b = - (Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16, - sizeof (Lib_IntVector_Intrinsics_vec128) * 4U); - memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); - Hacl_Hash_Blake2s_Simd128_block_state_t - block_state = + if (wv0 != NULL) + { + memset(wv0, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); + } + option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___ + block_state; + if (wv0 == NULL) + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + Lib_IntVector_Intrinsics_vec128 + *b = + (Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16, + sizeof (Lib_IntVector_Intrinsics_vec128) * 4U); + if (b != NULL) { - .fst = i.key_length, - .snd = i.digest_length, - .thd = i.last_node, - .f3 = { .fst = wv, .snd = b } - }; - Lib_IntVector_Intrinsics_vec128 *src_b = block_state0.f3.snd; - Lib_IntVector_Intrinsics_vec128 *dst_b = block_state.f3.snd; - memcpy(dst_b, src_b, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); - Hacl_Hash_Blake2s_Simd128_state_t - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Hash_Blake2s_Simd128_state_t - *p = - (Hacl_Hash_Blake2s_Simd128_state_t *)KRML_HOST_MALLOC(sizeof ( - Hacl_Hash_Blake2s_Simd128_state_t - )); - p[0U] = s; - return p; + memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); + } + if (b == NULL) + { + KRML_ALIGNED_FREE(wv0); + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){ + .tag = Hacl_Streaming_Types_None + } + ); + } + else + { + block_state = + ( + (option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){ + .tag = Hacl_Streaming_Types_Some, + .v = { + .fst = i.key_length, + .snd = i.digest_length, + .thd = i.last_node, + .f3 = { .fst = wv0, .snd = b } + } + } + ); + } + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_Blake2s_Simd128_block_state_t block_state1 = block_state.v; + Lib_IntVector_Intrinsics_vec128 *src_b = block_state0.f3.snd; + Lib_IntVector_Intrinsics_vec128 *dst_b = block_state1.f3.snd; + memcpy(dst_b, src_b, 4U * sizeof (Lib_IntVector_Intrinsics_vec128)); + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Hash_Blake2s_Simd128_state_t + s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 }; + Hacl_Hash_Blake2s_Simd128_state_t + *p = + (Hacl_Hash_Blake2s_Simd128_state_t *)KRML_HOST_MALLOC(sizeof ( + Hacl_Hash_Blake2s_Simd128_state_t + )); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + Lib_IntVector_Intrinsics_vec128 *b = block_state1.f3.snd; + Lib_IntVector_Intrinsics_vec128 *wv = block_state1.f3.fst; + KRML_ALIGNED_FREE(wv); + KRML_ALIGNED_FREE(b); + KRML_HOST_FREE(buf); + return NULL; + } + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** diff --git a/Modules/_hacl/Hacl_Hash_Blake2s_Simd128.h b/Modules/_hacl/Hacl_Hash_Blake2s_Simd128.h index cd1654c9726dc0..56456e6fbb3df8 100644 --- a/Modules/_hacl/Hacl_Hash_Blake2s_Simd128.h +++ b/Modules/_hacl/Hacl_Hash_Blake2s_Simd128.h @@ -32,13 +32,12 @@ extern "C" { #include #include "python_hacl_namespaces.h" -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" #include "Hacl_Streaming_Types.h" #include "Hacl_Hash_Blake2b.h" -#include "libintvector.h" #define HACL_HASH_BLAKE2S_SIMD128_BLOCK_BYTES (64U) @@ -50,29 +49,10 @@ extern "C" { #define HACL_HASH_BLAKE2S_SIMD128_PERSONAL_BYTES (8U) -typedef struct K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128__s -{ - Lib_IntVector_Intrinsics_vec128 *fst; - Lib_IntVector_Intrinsics_vec128 *snd; -} -K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_; - typedef struct Hacl_Hash_Blake2s_Simd128_block_state_t_s -{ - uint8_t fst; - uint8_t snd; - bool thd; - K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ f3; -} Hacl_Hash_Blake2s_Simd128_block_state_t; -typedef struct Hacl_Hash_Blake2s_Simd128_state_t_s -{ - Hacl_Hash_Blake2s_Simd128_block_state_t block_state; - uint8_t *buf; - uint64_t total_len; -} -Hacl_Hash_Blake2s_Simd128_state_t; +typedef struct Hacl_Hash_Blake2s_Simd128_state_t_s Hacl_Hash_Blake2s_Simd128_state_t; /** General-purpose allocation function that gives control over all @@ -108,7 +88,7 @@ The caller must satisfy the following requirements. */ Hacl_Hash_Blake2s_Simd128_state_t -*Hacl_Hash_Blake2s_Simd128_malloc_with_key0(uint8_t *k, uint8_t kk); +*Hacl_Hash_Blake2s_Simd128_malloc_with_key(uint8_t *k, uint8_t kk); /** Specialized allocation function that picks default values for all diff --git a/Modules/_hacl/Hacl_Hash_MD5.c b/Modules/_hacl/Hacl_Hash_MD5.c index ed294839ed8dc0..75ce8d2926e6e1 100644 --- a/Modules/_hacl/Hacl_Hash_MD5.c +++ b/Modules/_hacl/Hacl_Hash_MD5.c @@ -25,6 +25,9 @@ #include "internal/Hacl_Hash_MD5.h" +#include "Hacl_Streaming_Types.h" +#include "internal/Hacl_Streaming_Types.h" + static uint32_t _h0[4U] = { 0x67452301U, 0xefcdab89U, 0x98badcfeU, 0x10325476U }; static uint32_t @@ -1166,14 +1169,67 @@ void Hacl_Hash_MD5_hash_oneshot(uint8_t *output, uint8_t *input, uint32_t input_ Hacl_Streaming_MD_state_32 *Hacl_Hash_MD5_malloc(void) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - Hacl_Hash_MD5_init(block_state); - return p; + if (buf == NULL) + { + return NULL; + } + uint8_t *buf1 = buf; + uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t)); + Hacl_Streaming_Types_optional_32 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf1); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint32_t *block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_32 + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U }; + Hacl_Streaming_MD_state_32 + *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_MD5_init(block_state1); + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } void Hacl_Hash_MD5_reset(Hacl_Streaming_MD_state_32 *state) @@ -1412,15 +1468,67 @@ Hacl_Streaming_MD_state_32 *Hacl_Hash_MD5_copy(Hacl_Streaming_MD_state_32 *state uint8_t *buf0 = scrut.buf; uint64_t total_len0 = scrut.total_len; uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } memcpy(buf, buf0, 64U * sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t)); - memcpy(block_state, block_state0, 4U * sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - return p; + uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t)); + Hacl_Streaming_Types_optional_32 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint32_t *block_state1 = block_state.v; + memcpy(block_state1, block_state0, 4U * sizeof (uint32_t)); + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_32 + s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 }; + Hacl_Streaming_MD_state_32 + *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf); + return NULL; + } + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } void Hacl_Hash_MD5_hash(uint8_t *output, uint8_t *input, uint32_t input_len) diff --git a/Modules/_hacl/Hacl_Hash_MD5.h b/Modules/_hacl/Hacl_Hash_MD5.h index f69d6e5a81d63a..521c2addc50289 100644 --- a/Modules/_hacl/Hacl_Hash_MD5.h +++ b/Modules/_hacl/Hacl_Hash_MD5.h @@ -32,7 +32,7 @@ extern "C" { #include #include "python_hacl_namespaces.h" -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" diff --git a/Modules/_hacl/Hacl_Hash_SHA1.c b/Modules/_hacl/Hacl_Hash_SHA1.c index 1a8b09b1711894..508e447bf275da 100644 --- a/Modules/_hacl/Hacl_Hash_SHA1.c +++ b/Modules/_hacl/Hacl_Hash_SHA1.c @@ -25,6 +25,9 @@ #include "internal/Hacl_Hash_SHA1.h" +#include "Hacl_Streaming_Types.h" +#include "internal/Hacl_Streaming_Types.h" + static uint32_t _h0[5U] = { 0x67452301U, 0xefcdab89U, 0x98badcfeU, 0x10325476U, 0xc3d2e1f0U }; void Hacl_Hash_SHA1_init(uint32_t *s) @@ -199,14 +202,67 @@ void Hacl_Hash_SHA1_hash_oneshot(uint8_t *output, uint8_t *input, uint32_t input Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA1_malloc(void) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(5U, sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - Hacl_Hash_SHA1_init(block_state); - return p; + if (buf == NULL) + { + return NULL; + } + uint8_t *buf1 = buf; + uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(5U, sizeof (uint32_t)); + Hacl_Streaming_Types_optional_32 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf1); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint32_t *block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_32 + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U }; + Hacl_Streaming_MD_state_32 + *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_SHA1_init(block_state1); + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } void Hacl_Hash_SHA1_reset(Hacl_Streaming_MD_state_32 *state) @@ -445,15 +501,67 @@ Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA1_copy(Hacl_Streaming_MD_state_32 *stat uint8_t *buf0 = scrut.buf; uint64_t total_len0 = scrut.total_len; uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } memcpy(buf, buf0, 64U * sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(5U, sizeof (uint32_t)); - memcpy(block_state, block_state0, 5U * sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - return p; + uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(5U, sizeof (uint32_t)); + Hacl_Streaming_Types_optional_32 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint32_t *block_state1 = block_state.v; + memcpy(block_state1, block_state0, 5U * sizeof (uint32_t)); + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_32 + s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 }; + Hacl_Streaming_MD_state_32 + *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf); + return NULL; + } + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } void Hacl_Hash_SHA1_hash(uint8_t *output, uint8_t *input, uint32_t input_len) diff --git a/Modules/_hacl/Hacl_Hash_SHA1.h b/Modules/_hacl/Hacl_Hash_SHA1.h index ad1e8e72a739ec..63ac83f9dce018 100644 --- a/Modules/_hacl/Hacl_Hash_SHA1.h +++ b/Modules/_hacl/Hacl_Hash_SHA1.h @@ -32,7 +32,7 @@ extern "C" { #include #include "python_hacl_namespaces.h" -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" diff --git a/Modules/_hacl/Hacl_Hash_SHA2.c b/Modules/_hacl/Hacl_Hash_SHA2.c index cc930bbc89e8ad..d612bafa72cdc4 100644 --- a/Modules/_hacl/Hacl_Hash_SHA2.c +++ b/Modules/_hacl/Hacl_Hash_SHA2.c @@ -25,6 +25,9 @@ #include "internal/Hacl_Hash_SHA2.h" +#include "Hacl_Streaming_Types.h" + +#include "internal/Hacl_Streaming_Types.h" void Hacl_Hash_SHA2_sha256_init(uint32_t *hash) @@ -447,14 +450,67 @@ calling `free_256`. Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA2_malloc_256(void) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - Hacl_Hash_SHA2_sha256_init(block_state); - return p; + if (buf == NULL) + { + return NULL; + } + uint8_t *buf1 = buf; + uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t)); + Hacl_Streaming_Types_optional_32 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf1); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint32_t *block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_32 + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U }; + Hacl_Streaming_MD_state_32 + *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_SHA2_sha256_init(block_state1); + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** @@ -470,15 +526,67 @@ Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA2_copy_256(Hacl_Streaming_MD_state_32 * uint8_t *buf0 = scrut.buf; uint64_t total_len0 = scrut.total_len; uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } memcpy(buf, buf0, 64U * sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t)); - memcpy(block_state, block_state0, 8U * sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - return p; + uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t)); + Hacl_Streaming_Types_optional_32 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint32_t *block_state1 = block_state.v; + memcpy(block_state1, block_state0, 8U * sizeof (uint32_t)); + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_32 + s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 }; + Hacl_Streaming_MD_state_32 + *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf); + return NULL; + } + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** @@ -760,14 +868,67 @@ void Hacl_Hash_SHA2_hash_256(uint8_t *output, uint8_t *input, uint32_t input_len Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA2_malloc_224(void) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t)); - uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t)); - Hacl_Streaming_MD_state_32 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U }; - Hacl_Streaming_MD_state_32 - *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); - p[0U] = s; - Hacl_Hash_SHA2_sha224_init(block_state); - return p; + if (buf == NULL) + { + return NULL; + } + uint8_t *buf1 = buf; + uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t)); + Hacl_Streaming_Types_optional_32 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf1); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint32_t *block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_32 + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U }; + Hacl_Streaming_MD_state_32 + *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_SHA2_sha224_init(block_state1); + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } void Hacl_Hash_SHA2_reset_224(Hacl_Streaming_MD_state_32 *state) @@ -858,14 +1019,67 @@ void Hacl_Hash_SHA2_hash_224(uint8_t *output, uint8_t *input, uint32_t input_len Hacl_Streaming_MD_state_64 *Hacl_Hash_SHA2_malloc_512(void) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t)); - uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t)); - Hacl_Streaming_MD_state_64 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U }; - Hacl_Streaming_MD_state_64 - *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); - p[0U] = s; - Hacl_Hash_SHA2_sha512_init(block_state); - return p; + if (buf == NULL) + { + return NULL; + } + uint8_t *buf1 = buf; + uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t)); + Hacl_Streaming_Types_optional_64 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf1); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint64_t *block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_64 + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U }; + Hacl_Streaming_MD_state_64 + *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_SHA2_sha512_init(block_state1); + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } /** @@ -881,15 +1095,67 @@ Hacl_Streaming_MD_state_64 *Hacl_Hash_SHA2_copy_512(Hacl_Streaming_MD_state_64 * uint8_t *buf0 = scrut.buf; uint64_t total_len0 = scrut.total_len; uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } memcpy(buf, buf0, 128U * sizeof (uint8_t)); - uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t)); - memcpy(block_state, block_state0, 8U * sizeof (uint64_t)); - Hacl_Streaming_MD_state_64 - s = { .block_state = block_state, .buf = buf, .total_len = total_len0 }; - Hacl_Streaming_MD_state_64 - *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); - p[0U] = s; - return p; + uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t)); + Hacl_Streaming_Types_optional_64 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint64_t *block_state1 = block_state.v; + memcpy(block_state1, block_state0, 8U * sizeof (uint64_t)); + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_64 + s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 }; + Hacl_Streaming_MD_state_64 + *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf); + return NULL; + } + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } void Hacl_Hash_SHA2_reset_512(Hacl_Streaming_MD_state_64 *state) @@ -1172,14 +1438,67 @@ void Hacl_Hash_SHA2_hash_512(uint8_t *output, uint8_t *input, uint32_t input_len Hacl_Streaming_MD_state_64 *Hacl_Hash_SHA2_malloc_384(void) { uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t)); - uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t)); - Hacl_Streaming_MD_state_64 - s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U }; - Hacl_Streaming_MD_state_64 - *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); - p[0U] = s; - Hacl_Hash_SHA2_sha384_init(block_state); - return p; + if (buf == NULL) + { + return NULL; + } + uint8_t *buf1 = buf; + uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t)); + Hacl_Streaming_Types_optional_64 block_state; + if (b == NULL) + { + block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_Some, .v = b }); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf1); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + uint64_t *block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Streaming_MD_state_64 + s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U }; + Hacl_Streaming_MD_state_64 + *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64)); + if (p != NULL) + { + p[0U] = s; + } + if (p == NULL) + { + KRML_HOST_FREE(block_state1); + KRML_HOST_FREE(buf1); + return NULL; + } + Hacl_Hash_SHA2_sha384_init(block_state1); + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } void Hacl_Hash_SHA2_reset_384(Hacl_Streaming_MD_state_64 *state) diff --git a/Modules/_hacl/Hacl_Hash_SHA2.h b/Modules/_hacl/Hacl_Hash_SHA2.h index d8204b504baf82..a93138fb7ee7a7 100644 --- a/Modules/_hacl/Hacl_Hash_SHA2.h +++ b/Modules/_hacl/Hacl_Hash_SHA2.h @@ -32,13 +32,12 @@ extern "C" { #include #include "python_hacl_namespaces.h" -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" #include "Hacl_Streaming_Types.h" - typedef Hacl_Streaming_MD_state_32 Hacl_Hash_SHA2_state_t_224; typedef Hacl_Streaming_MD_state_32 Hacl_Hash_SHA2_state_t_256; diff --git a/Modules/_hacl/Hacl_Hash_SHA3.c b/Modules/_hacl/Hacl_Hash_SHA3.c index b964e1d9c0aa69..87638df9549fbb 100644 --- a/Modules/_hacl/Hacl_Hash_SHA3.c +++ b/Modules/_hacl/Hacl_Hash_SHA3.c @@ -25,6 +25,9 @@ #include "internal/Hacl_Hash_SHA3.h" +#include "Hacl_Streaming_Types.h" +#include "internal/Hacl_Streaming_Types.h" + const uint32_t Hacl_Hash_SHA3_keccak_rotc[24U] = @@ -234,6 +237,12 @@ static uint32_t hash_len(Spec_Hash_Definitions_hash_alg a) } } +void Hacl_Hash_SHA3_init_(Spec_Hash_Definitions_hash_alg a, uint64_t *s) +{ + KRML_MAYBE_UNUSED_VAR(a); + memset(s, 0U, 25U * sizeof (uint64_t)); +} + void Hacl_Hash_SHA3_update_multi_sha3( Spec_Hash_Definitions_hash_alg a, @@ -545,6 +554,74 @@ Hacl_Hash_SHA3_update_last_sha3( absorb_inner_32(b3, s); } +static void squeeze(uint64_t *s, uint32_t rateInBytes, uint32_t outputByteLen, uint8_t *b) +{ + for (uint32_t i0 = 0U; i0 < outputByteLen / rateInBytes; i0++) + { + uint8_t hbuf[256U] = { 0U }; + uint64_t ws[32U] = { 0U }; + memcpy(ws, s, 25U * sizeof (uint64_t)); + for (uint32_t i = 0U; i < 32U; i++) + { + store64_le(hbuf + i * 8U, ws[i]); + } + uint8_t *b0 = b; + memcpy(b0 + i0 * rateInBytes, hbuf, rateInBytes * sizeof (uint8_t)); + for (uint32_t i1 = 0U; i1 < 24U; i1++) + { + uint64_t _C[5U] = { 0U }; + KRML_MAYBE_FOR5(i, + 0U, + 5U, + 1U, + _C[i] = s[i + 0U] ^ (s[i + 5U] ^ (s[i + 10U] ^ (s[i + 15U] ^ s[i + 20U])));); + KRML_MAYBE_FOR5(i2, + 0U, + 5U, + 1U, + uint64_t uu____0 = _C[(i2 + 1U) % 5U]; + uint64_t _D = _C[(i2 + 4U) % 5U] ^ (uu____0 << 1U | uu____0 >> 63U); + KRML_MAYBE_FOR5(i, 0U, 5U, 1U, s[i2 + 5U * i] = s[i2 + 5U * i] ^ _D;);); + uint64_t x = s[1U]; + uint64_t current = x; + for (uint32_t i = 0U; i < 24U; i++) + { + uint32_t _Y = Hacl_Hash_SHA3_keccak_piln[i]; + uint32_t r = Hacl_Hash_SHA3_keccak_rotc[i]; + uint64_t temp = s[_Y]; + uint64_t uu____1 = current; + s[_Y] = uu____1 << r | uu____1 >> (64U - r); + current = temp; + } + KRML_MAYBE_FOR5(i, + 0U, + 5U, + 1U, + uint64_t v0 = s[0U + 5U * i] ^ (~s[1U + 5U * i] & s[2U + 5U * i]); + uint64_t v1 = s[1U + 5U * i] ^ (~s[2U + 5U * i] & s[3U + 5U * i]); + uint64_t v2 = s[2U + 5U * i] ^ (~s[3U + 5U * i] & s[4U + 5U * i]); + uint64_t v3 = s[3U + 5U * i] ^ (~s[4U + 5U * i] & s[0U + 5U * i]); + uint64_t v4 = s[4U + 5U * i] ^ (~s[0U + 5U * i] & s[1U + 5U * i]); + s[0U + 5U * i] = v0; + s[1U + 5U * i] = v1; + s[2U + 5U * i] = v2; + s[3U + 5U * i] = v3; + s[4U + 5U * i] = v4;); + uint64_t c = Hacl_Hash_SHA3_keccak_rndc[i1]; + s[0U] = s[0U] ^ c; + } + } + uint32_t remOut = outputByteLen % rateInBytes; + uint8_t hbuf[256U] = { 0U }; + uint64_t ws[32U] = { 0U }; + memcpy(ws, s, 25U * sizeof (uint64_t)); + for (uint32_t i = 0U; i < 32U; i++) + { + store64_le(hbuf + i * 8U, ws[i]); + } + memcpy(b + outputByteLen - remOut, hbuf, remOut * sizeof (uint8_t)); +} + typedef struct hash_buf2_s { Hacl_Hash_SHA3_hash_buf fst; @@ -558,20 +635,88 @@ Spec_Hash_Definitions_hash_alg Hacl_Hash_SHA3_get_alg(Hacl_Hash_SHA3_state_t *s) return block_state.fst; } +typedef struct option___Spec_Hash_Definitions_hash_alg____uint64_t___s +{ + Hacl_Streaming_Types_optional tag; + Hacl_Hash_SHA3_hash_buf v; +} +option___Spec_Hash_Definitions_hash_alg____uint64_t__; + Hacl_Hash_SHA3_state_t *Hacl_Hash_SHA3_malloc(Spec_Hash_Definitions_hash_alg a) { KRML_CHECK_SIZE(sizeof (uint8_t), block_len(a)); - uint8_t *buf0 = (uint8_t *)KRML_HOST_CALLOC(block_len(a), sizeof (uint8_t)); - uint64_t *buf = (uint64_t *)KRML_HOST_CALLOC(25U, sizeof (uint64_t)); - Hacl_Hash_SHA3_hash_buf block_state = { .fst = a, .snd = buf }; - Hacl_Hash_SHA3_state_t - s = { .block_state = block_state, .buf = buf0, .total_len = (uint64_t)0U }; - Hacl_Hash_SHA3_state_t - *p = (Hacl_Hash_SHA3_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_SHA3_state_t)); - p[0U] = s; - uint64_t *s1 = block_state.snd; - memset(s1, 0U, 25U * sizeof (uint64_t)); - return p; + uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(block_len(a), sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } + uint8_t *buf1 = buf; + uint64_t *s = (uint64_t *)KRML_HOST_CALLOC(25U, sizeof (uint64_t)); + option___Spec_Hash_Definitions_hash_alg____uint64_t__ block_state; + if (s == NULL) + { + block_state = + ((option___Spec_Hash_Definitions_hash_alg____uint64_t__){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = + ( + (option___Spec_Hash_Definitions_hash_alg____uint64_t__){ + .tag = Hacl_Streaming_Types_Some, + .v = { .fst = a, .snd = s } + } + ); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf1); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_SHA3_hash_buf block_state1 = block_state.v; + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Hash_SHA3_state_t + s0 = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U }; + Hacl_Hash_SHA3_state_t + *p = (Hacl_Hash_SHA3_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_SHA3_state_t)); + if (p != NULL) + { + p[0U] = s0; + } + if (p == NULL) + { + uint64_t *s1 = block_state1.snd; + KRML_HOST_FREE(s1); + KRML_HOST_FREE(buf1); + return NULL; + } + Spec_Hash_Definitions_hash_alg a1 = block_state1.fst; + uint64_t *s1 = block_state1.snd; + Hacl_Hash_SHA3_init_(a1, s1); + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } void Hacl_Hash_SHA3_free(Hacl_Hash_SHA3_state_t *state) @@ -593,20 +738,79 @@ Hacl_Hash_SHA3_state_t *Hacl_Hash_SHA3_copy(Hacl_Hash_SHA3_state_t *state) uint64_t total_len0 = scrut0.total_len; Spec_Hash_Definitions_hash_alg i = block_state0.fst; KRML_CHECK_SIZE(sizeof (uint8_t), block_len(i)); - uint8_t *buf1 = (uint8_t *)KRML_HOST_CALLOC(block_len(i), sizeof (uint8_t)); - memcpy(buf1, buf0, block_len(i) * sizeof (uint8_t)); - uint64_t *buf = (uint64_t *)KRML_HOST_CALLOC(25U, sizeof (uint64_t)); - Hacl_Hash_SHA3_hash_buf block_state = { .fst = i, .snd = buf }; - hash_buf2 scrut = { .fst = block_state0, .snd = block_state }; - uint64_t *s_dst = scrut.snd.snd; - uint64_t *s_src = scrut.fst.snd; - memcpy(s_dst, s_src, 25U * sizeof (uint64_t)); - Hacl_Hash_SHA3_state_t - s = { .block_state = block_state, .buf = buf1, .total_len = total_len0 }; - Hacl_Hash_SHA3_state_t - *p = (Hacl_Hash_SHA3_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_SHA3_state_t)); - p[0U] = s; - return p; + uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(block_len(i), sizeof (uint8_t)); + if (buf == NULL) + { + return NULL; + } + memcpy(buf, buf0, block_len(i) * sizeof (uint8_t)); + uint64_t *s = (uint64_t *)KRML_HOST_CALLOC(25U, sizeof (uint64_t)); + option___Spec_Hash_Definitions_hash_alg____uint64_t__ block_state; + if (s == NULL) + { + block_state = + ((option___Spec_Hash_Definitions_hash_alg____uint64_t__){ .tag = Hacl_Streaming_Types_None }); + } + else + { + block_state = + ( + (option___Spec_Hash_Definitions_hash_alg____uint64_t__){ + .tag = Hacl_Streaming_Types_Some, + .v = { .fst = i, .snd = s } + } + ); + } + if (block_state.tag == Hacl_Streaming_Types_None) + { + KRML_HOST_FREE(buf); + return NULL; + } + if (block_state.tag == Hacl_Streaming_Types_Some) + { + Hacl_Hash_SHA3_hash_buf block_state1 = block_state.v; + hash_buf2 scrut = { .fst = block_state0, .snd = block_state1 }; + uint64_t *s_dst = scrut.snd.snd; + uint64_t *s_src = scrut.fst.snd; + memcpy(s_dst, s_src, 25U * sizeof (uint64_t)); + Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some; + switch (k_) + { + case Hacl_Streaming_Types_None: + { + return NULL; + } + case Hacl_Streaming_Types_Some: + { + Hacl_Hash_SHA3_state_t + s0 = { .block_state = block_state1, .buf = buf, .total_len = total_len0 }; + Hacl_Hash_SHA3_state_t + *p = (Hacl_Hash_SHA3_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_SHA3_state_t)); + if (p != NULL) + { + p[0U] = s0; + } + if (p == NULL) + { + uint64_t *s1 = block_state1.snd; + KRML_HOST_FREE(s1); + KRML_HOST_FREE(buf); + return NULL; + } + return p; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); } void Hacl_Hash_SHA3_reset(Hacl_Hash_SHA3_state_t *state) @@ -616,8 +820,9 @@ void Hacl_Hash_SHA3_reset(Hacl_Hash_SHA3_state_t *state) Hacl_Hash_SHA3_hash_buf block_state = scrut.block_state; Spec_Hash_Definitions_hash_alg i = block_state.fst; KRML_MAYBE_UNUSED_VAR(i); + Spec_Hash_Definitions_hash_alg a1 = block_state.fst; uint64_t *s = block_state.snd; - memset(s, 0U, 25U * sizeof (uint64_t)); + Hacl_Hash_SHA3_init_(a1, s); Hacl_Hash_SHA3_state_t tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U }; state[0U] = tmp; @@ -849,141 +1054,30 @@ digest_( Hacl_Hash_SHA3_update_last_sha3(a10, s1, buf_last, r); Spec_Hash_Definitions_hash_alg a11 = tmp_block_state.fst; uint64_t *s = tmp_block_state.snd; - if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256) + bool sw; + switch (a11) { - for (uint32_t i0 = 0U; i0 < l / block_len(a11); i0++) - { - uint8_t hbuf[256U] = { 0U }; - uint64_t ws[32U] = { 0U }; - memcpy(ws, s, 25U * sizeof (uint64_t)); - for (uint32_t i = 0U; i < 32U; i++) + case Spec_Hash_Definitions_Shake128: { - store64_le(hbuf + i * 8U, ws[i]); + sw = true; + break; } - uint8_t *b0 = output; - uint8_t *uu____0 = hbuf; - memcpy(b0 + i0 * block_len(a11), uu____0, block_len(a11) * sizeof (uint8_t)); - for (uint32_t i1 = 0U; i1 < 24U; i1++) + case Spec_Hash_Definitions_Shake256: { - uint64_t _C[5U] = { 0U }; - KRML_MAYBE_FOR5(i, - 0U, - 5U, - 1U, - _C[i] = s[i + 0U] ^ (s[i + 5U] ^ (s[i + 10U] ^ (s[i + 15U] ^ s[i + 20U])));); - KRML_MAYBE_FOR5(i2, - 0U, - 5U, - 1U, - uint64_t uu____1 = _C[(i2 + 1U) % 5U]; - uint64_t _D = _C[(i2 + 4U) % 5U] ^ (uu____1 << 1U | uu____1 >> 63U); - KRML_MAYBE_FOR5(i, 0U, 5U, 1U, s[i2 + 5U * i] = s[i2 + 5U * i] ^ _D;);); - uint64_t x = s[1U]; - uint64_t current = x; - for (uint32_t i = 0U; i < 24U; i++) - { - uint32_t _Y = Hacl_Hash_SHA3_keccak_piln[i]; - uint32_t r1 = Hacl_Hash_SHA3_keccak_rotc[i]; - uint64_t temp = s[_Y]; - uint64_t uu____2 = current; - s[_Y] = uu____2 << r1 | uu____2 >> (64U - r1); - current = temp; - } - KRML_MAYBE_FOR5(i, - 0U, - 5U, - 1U, - uint64_t v0 = s[0U + 5U * i] ^ (~s[1U + 5U * i] & s[2U + 5U * i]); - uint64_t v1 = s[1U + 5U * i] ^ (~s[2U + 5U * i] & s[3U + 5U * i]); - uint64_t v2 = s[2U + 5U * i] ^ (~s[3U + 5U * i] & s[4U + 5U * i]); - uint64_t v3 = s[3U + 5U * i] ^ (~s[4U + 5U * i] & s[0U + 5U * i]); - uint64_t v4 = s[4U + 5U * i] ^ (~s[0U + 5U * i] & s[1U + 5U * i]); - s[0U + 5U * i] = v0; - s[1U + 5U * i] = v1; - s[2U + 5U * i] = v2; - s[3U + 5U * i] = v3; - s[4U + 5U * i] = v4;); - uint64_t c = Hacl_Hash_SHA3_keccak_rndc[i1]; - s[0U] = s[0U] ^ c; + sw = true; + break; } - } - uint32_t remOut = l % block_len(a11); - uint8_t hbuf[256U] = { 0U }; - uint64_t ws[32U] = { 0U }; - memcpy(ws, s, 25U * sizeof (uint64_t)); - for (uint32_t i = 0U; i < 32U; i++) - { - store64_le(hbuf + i * 8U, ws[i]); - } - memcpy(output + l - remOut, hbuf, remOut * sizeof (uint8_t)); - return; - } - for (uint32_t i0 = 0U; i0 < hash_len(a11) / block_len(a11); i0++) - { - uint8_t hbuf[256U] = { 0U }; - uint64_t ws[32U] = { 0U }; - memcpy(ws, s, 25U * sizeof (uint64_t)); - for (uint32_t i = 0U; i < 32U; i++) - { - store64_le(hbuf + i * 8U, ws[i]); - } - uint8_t *b0 = output; - uint8_t *uu____3 = hbuf; - memcpy(b0 + i0 * block_len(a11), uu____3, block_len(a11) * sizeof (uint8_t)); - for (uint32_t i1 = 0U; i1 < 24U; i1++) - { - uint64_t _C[5U] = { 0U }; - KRML_MAYBE_FOR5(i, - 0U, - 5U, - 1U, - _C[i] = s[i + 0U] ^ (s[i + 5U] ^ (s[i + 10U] ^ (s[i + 15U] ^ s[i + 20U])));); - KRML_MAYBE_FOR5(i2, - 0U, - 5U, - 1U, - uint64_t uu____4 = _C[(i2 + 1U) % 5U]; - uint64_t _D = _C[(i2 + 4U) % 5U] ^ (uu____4 << 1U | uu____4 >> 63U); - KRML_MAYBE_FOR5(i, 0U, 5U, 1U, s[i2 + 5U * i] = s[i2 + 5U * i] ^ _D;);); - uint64_t x = s[1U]; - uint64_t current = x; - for (uint32_t i = 0U; i < 24U; i++) + default: { - uint32_t _Y = Hacl_Hash_SHA3_keccak_piln[i]; - uint32_t r1 = Hacl_Hash_SHA3_keccak_rotc[i]; - uint64_t temp = s[_Y]; - uint64_t uu____5 = current; - s[_Y] = uu____5 << r1 | uu____5 >> (64U - r1); - current = temp; + sw = false; } - KRML_MAYBE_FOR5(i, - 0U, - 5U, - 1U, - uint64_t v0 = s[0U + 5U * i] ^ (~s[1U + 5U * i] & s[2U + 5U * i]); - uint64_t v1 = s[1U + 5U * i] ^ (~s[2U + 5U * i] & s[3U + 5U * i]); - uint64_t v2 = s[2U + 5U * i] ^ (~s[3U + 5U * i] & s[4U + 5U * i]); - uint64_t v3 = s[3U + 5U * i] ^ (~s[4U + 5U * i] & s[0U + 5U * i]); - uint64_t v4 = s[4U + 5U * i] ^ (~s[0U + 5U * i] & s[1U + 5U * i]); - s[0U + 5U * i] = v0; - s[1U + 5U * i] = v1; - s[2U + 5U * i] = v2; - s[3U + 5U * i] = v3; - s[4U + 5U * i] = v4;); - uint64_t c = Hacl_Hash_SHA3_keccak_rndc[i1]; - s[0U] = s[0U] ^ c; - } } - uint32_t remOut = hash_len(a11) % block_len(a11); - uint8_t hbuf[256U] = { 0U }; - uint64_t ws[32U] = { 0U }; - memcpy(ws, s, 25U * sizeof (uint64_t)); - for (uint32_t i = 0U; i < 32U; i++) + if (sw) { - store64_le(hbuf + i * 8U, ws[i]); + squeeze(s, block_len(a11), l, output); + return; } - uint8_t *uu____6 = hbuf; - memcpy(output + hash_len(a11) - remOut, uu____6, remOut * sizeof (uint8_t)); + squeeze(s, block_len(a11), hash_len(a11), output); } Hacl_Streaming_Types_error_code diff --git a/Modules/_hacl/Hacl_Hash_SHA3.h b/Modules/_hacl/Hacl_Hash_SHA3.h index 4d85bb6902cc5b..65ec99ee3a3ac9 100644 --- a/Modules/_hacl/Hacl_Hash_SHA3.h +++ b/Modules/_hacl/Hacl_Hash_SHA3.h @@ -32,26 +32,13 @@ extern "C" { #include #include "python_hacl_namespaces.h" -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" #include "Hacl_Streaming_Types.h" -typedef struct Hacl_Hash_SHA3_hash_buf_s -{ - Spec_Hash_Definitions_hash_alg fst; - uint64_t *snd; -} -Hacl_Hash_SHA3_hash_buf; - -typedef struct Hacl_Hash_SHA3_state_t_s -{ - Hacl_Hash_SHA3_hash_buf block_state; - uint8_t *buf; - uint64_t total_len; -} -Hacl_Hash_SHA3_state_t; +typedef struct Hacl_Hash_SHA3_state_t_s Hacl_Hash_SHA3_state_t; Spec_Hash_Definitions_hash_alg Hacl_Hash_SHA3_get_alg(Hacl_Hash_SHA3_state_t *s); diff --git a/Modules/_hacl/Hacl_Streaming_Types.h b/Modules/_hacl/Hacl_Streaming_Types.h index 15ef16ba6075a9..5c497750793720 100644 --- a/Modules/_hacl/Hacl_Streaming_Types.h +++ b/Modules/_hacl/Hacl_Streaming_Types.h @@ -31,7 +31,7 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" @@ -56,24 +56,13 @@ typedef uint8_t Spec_Hash_Definitions_hash_alg; #define Hacl_Streaming_Types_InvalidAlgorithm 1 #define Hacl_Streaming_Types_InvalidLength 2 #define Hacl_Streaming_Types_MaximumLengthExceeded 3 +#define Hacl_Streaming_Types_OutOfMemory 4 typedef uint8_t Hacl_Streaming_Types_error_code; -typedef struct Hacl_Streaming_MD_state_32_s -{ - uint32_t *block_state; - uint8_t *buf; - uint64_t total_len; -} -Hacl_Streaming_MD_state_32; +typedef struct Hacl_Streaming_MD_state_32_s Hacl_Streaming_MD_state_32; -typedef struct Hacl_Streaming_MD_state_64_s -{ - uint64_t *block_state; - uint8_t *buf; - uint64_t total_len; -} -Hacl_Streaming_MD_state_64; +typedef struct Hacl_Streaming_MD_state_64_s Hacl_Streaming_MD_state_64; #if defined(__cplusplus) } diff --git a/Modules/_hacl/Lib_Memzero0.c b/Modules/_hacl/Lib_Memzero0.c index f01568a138648f..4dbf55eef58231 100644 --- a/Modules/_hacl/Lib_Memzero0.c +++ b/Modules/_hacl/Lib_Memzero0.c @@ -12,7 +12,7 @@ #include #endif -#if (defined(__APPLE__) && defined(__MACH__)) || defined(__linux__) +#if (defined(__APPLE__) && defined(__MACH__)) || defined(__linux__) || defined(__OpenBSD__) #define __STDC_WANT_LIB_EXT1__ 1 #include #endif @@ -43,7 +43,7 @@ void Lib_Memzero0_memzero0(void *dst, uint64_t len) { SecureZeroMemory(dst, len_); #elif defined(__APPLE__) && defined(__MACH__) && defined(MAC_OS_X_VERSION_MIN_REQUIRED) && (MAC_OS_X_VERSION_MIN_REQUIRED >= 1090) memset_s(dst, len_, 0, len_); - #elif (defined(__linux__) && !defined(LINUX_NO_EXPLICIT_BZERO)) || defined(__FreeBSD__) + #elif (defined(__linux__) && !defined(LINUX_NO_EXPLICIT_BZERO)) || defined(__FreeBSD__) || defined(__OpenBSD__) explicit_bzero(dst, len_); #elif defined(__NetBSD__) explicit_memset(dst, 0, len_); diff --git a/Modules/_hacl/include/krml/FStar_UInt128_Verified.h b/Modules/_hacl/include/krml/FStar_UInt128_Verified.h index 659745b24265cb..d4a90220beafb5 100644 --- a/Modules/_hacl/include/krml/FStar_UInt128_Verified.h +++ b/Modules/_hacl/include/krml/FStar_UInt128_Verified.h @@ -10,7 +10,7 @@ #include "FStar_UInt_8_16_32_64.h" #include #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/internal/target.h" static inline uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b) diff --git a/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h b/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h index 68bac0b3f0aab1..00be80836574af 100644 --- a/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h +++ b/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h @@ -9,11 +9,31 @@ #include #include - +#include "krml/internal/compat.h" #include "krml/lowstar_endianness.h" -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/internal/target.h" +extern krml_checked_int_t FStar_UInt64_n; + +extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee); + +extern krml_checked_int_t FStar_UInt64___proj__Mk__item__v(uint64_t projectee); + +extern krml_checked_int_t FStar_UInt64_v(uint64_t x); + +typedef void *FStar_UInt64_fits; + +extern uint64_t FStar_UInt64_uint_to_t(krml_checked_int_t x); + +extern uint64_t FStar_UInt64_zero; + +extern uint64_t FStar_UInt64_one; + +extern uint64_t FStar_UInt64_minus(uint64_t a); + +extern uint32_t FStar_UInt64_n_minus_one; + static KRML_NOINLINE uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b) { uint64_t x = a ^ b; @@ -36,6 +56,34 @@ static KRML_NOINLINE uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b) return x_xor_q_ - 1ULL; } +extern Prims_string FStar_UInt64_to_string(uint64_t uu___); + +extern Prims_string FStar_UInt64_to_string_hex(uint64_t uu___); + +extern Prims_string FStar_UInt64_to_string_hex_pad(uint64_t uu___); + +extern uint64_t FStar_UInt64_of_string(Prims_string uu___); + +extern krml_checked_int_t FStar_UInt32_n; + +extern bool FStar_UInt32_uu___is_Mk(uint32_t projectee); + +extern krml_checked_int_t FStar_UInt32___proj__Mk__item__v(uint32_t projectee); + +extern krml_checked_int_t FStar_UInt32_v(uint32_t x); + +typedef void *FStar_UInt32_fits; + +extern uint32_t FStar_UInt32_uint_to_t(krml_checked_int_t x); + +extern uint32_t FStar_UInt32_zero; + +extern uint32_t FStar_UInt32_one; + +extern uint32_t FStar_UInt32_minus(uint32_t a); + +extern uint32_t FStar_UInt32_n_minus_one; + static KRML_NOINLINE uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b) { uint32_t x = a ^ b; @@ -58,6 +106,34 @@ static KRML_NOINLINE uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b) return x_xor_q_ - 1U; } +extern Prims_string FStar_UInt32_to_string(uint32_t uu___); + +extern Prims_string FStar_UInt32_to_string_hex(uint32_t uu___); + +extern Prims_string FStar_UInt32_to_string_hex_pad(uint32_t uu___); + +extern uint32_t FStar_UInt32_of_string(Prims_string uu___); + +extern krml_checked_int_t FStar_UInt16_n; + +extern bool FStar_UInt16_uu___is_Mk(uint16_t projectee); + +extern krml_checked_int_t FStar_UInt16___proj__Mk__item__v(uint16_t projectee); + +extern krml_checked_int_t FStar_UInt16_v(uint16_t x); + +typedef void *FStar_UInt16_fits; + +extern uint16_t FStar_UInt16_uint_to_t(krml_checked_int_t x); + +extern uint16_t FStar_UInt16_zero; + +extern uint16_t FStar_UInt16_one; + +extern uint16_t FStar_UInt16_minus(uint16_t a); + +extern uint32_t FStar_UInt16_n_minus_one; + static KRML_NOINLINE uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b) { uint16_t x = (uint32_t)a ^ (uint32_t)b; @@ -80,6 +156,34 @@ static KRML_NOINLINE uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b) return (uint32_t)x_xor_q_ - 1U; } +extern Prims_string FStar_UInt16_to_string(uint16_t uu___); + +extern Prims_string FStar_UInt16_to_string_hex(uint16_t uu___); + +extern Prims_string FStar_UInt16_to_string_hex_pad(uint16_t uu___); + +extern uint16_t FStar_UInt16_of_string(Prims_string uu___); + +extern krml_checked_int_t FStar_UInt8_n; + +extern bool FStar_UInt8_uu___is_Mk(uint8_t projectee); + +extern krml_checked_int_t FStar_UInt8___proj__Mk__item__v(uint8_t projectee); + +extern krml_checked_int_t FStar_UInt8_v(uint8_t x); + +typedef void *FStar_UInt8_fits; + +extern uint8_t FStar_UInt8_uint_to_t(krml_checked_int_t x); + +extern uint8_t FStar_UInt8_zero; + +extern uint8_t FStar_UInt8_one; + +extern uint8_t FStar_UInt8_minus(uint8_t a); + +extern uint32_t FStar_UInt8_n_minus_one; + static KRML_NOINLINE uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b) { uint8_t x = (uint32_t)a ^ (uint32_t)b; @@ -102,6 +206,16 @@ static KRML_NOINLINE uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b) return (uint32_t)x_xor_q_ - 1U; } +extern Prims_string FStar_UInt8_to_string(uint8_t uu___); + +extern Prims_string FStar_UInt8_to_string_hex(uint8_t uu___); + +extern Prims_string FStar_UInt8_to_string_hex_pad(uint8_t uu___); + +extern uint8_t FStar_UInt8_of_string(Prims_string uu___); + +typedef uint8_t FStar_UInt8_byte; + #define __FStar_UInt_8_16_32_64_H_DEFINED #endif diff --git a/Modules/_hacl/include/krml/internal/compat.h b/Modules/_hacl/include/krml/internal/compat.h new file mode 100644 index 00000000000000..f206520fc0f4a4 --- /dev/null +++ b/Modules/_hacl/include/krml/internal/compat.h @@ -0,0 +1,32 @@ +/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 and MIT Licenses. */ + +#ifndef KRML_COMPAT_H +#define KRML_COMPAT_H + +#include + +/* A series of macros that define C implementations of types that are not Low*, + * to facilitate porting programs to Low*. */ + +typedef struct { + uint32_t length; + const char *data; +} FStar_Bytes_bytes; + +typedef int32_t Prims_pos, Prims_nat, Prims_nonzero, Prims_int, + krml_checked_int_t; + +#define RETURN_OR(x) \ + do { \ + int64_t __ret = x; \ + if (__ret < INT32_MIN || INT32_MAX < __ret) { \ + KRML_HOST_PRINTF( \ + "Prims.{int,nat,pos} integer overflow at %s:%d\n", __FILE__, \ + __LINE__); \ + KRML_HOST_EXIT(252); \ + } \ + return (int32_t)__ret; \ + } while (0) + +#endif diff --git a/Modules/_hacl/include/krml/internal/target.h b/Modules/_hacl/include/krml/internal/target.h index 9b403c36ceca19..c592214634a3bd 100644 --- a/Modules/_hacl/include/krml/internal/target.h +++ b/Modules/_hacl/include/krml/internal/target.h @@ -76,7 +76,7 @@ #endif #ifndef KRML_MAYBE_UNUSED -# if defined(__GNUC__) +# if defined(__GNUC__) || defined(__clang__) # define KRML_MAYBE_UNUSED __attribute__((unused)) # else # define KRML_MAYBE_UNUSED @@ -84,7 +84,7 @@ #endif #ifndef KRML_ATTRIBUTE_TARGET -# if defined(__GNUC__) +# if defined(__GNUC__) || defined(__clang__) # define KRML_ATTRIBUTE_TARGET(x) __attribute__((target(x))) # else # define KRML_ATTRIBUTE_TARGET(x) @@ -92,10 +92,10 @@ #endif #ifndef KRML_NOINLINE -# if defined(_MSC_VER) -# define KRML_NOINLINE __declspec(noinline) -# elif defined (__GNUC__) +# if defined (__GNUC__) || defined (__clang__) # define KRML_NOINLINE __attribute__((noinline,unused)) +# elif defined(_MSC_VER) +# define KRML_NOINLINE __declspec(noinline) # elif defined (__SUNPRO_C) # define KRML_NOINLINE __attribute__((noinline)) # else @@ -173,6 +173,32 @@ # endif #endif +#ifndef KRML_HOST_TIME + +# include + +/* Prims_nat not yet in scope */ +inline static int32_t krml_time(void) { + return (int32_t)time(NULL); +} + +# define KRML_HOST_TIME krml_time +#endif + +/* In statement position, exiting is easy. */ +#define KRML_EXIT \ + do { \ + KRML_HOST_PRINTF("Unimplemented function at %s:%d\n", __FILE__, __LINE__); \ + KRML_HOST_EXIT(254); \ + } while (0) + +/* In expression position, use the comma-operator and a malloc to return an + * expression of the right size. KaRaMeL passes t as the parameter to the macro. + */ +#define KRML_EABORT(t, msg) \ + (KRML_HOST_PRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, msg), \ + KRML_HOST_EXIT(255), *((t *)KRML_HOST_MALLOC(sizeof(t)))) + /* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of * *elements*. Do an ugly, run-time check (some of which KaRaMeL can eliminate). */ @@ -195,6 +221,24 @@ } \ } while (0) +#if defined(_MSC_VER) && _MSC_VER < 1900 +# define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) \ + _snprintf_s(buf, sz, _TRUNCATE, fmt, arg) +#else +# define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg) +#endif + +#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4)) +# define KRML_DEPRECATED(x) __attribute__((deprecated(x))) +#elif defined(__GNUC__) +/* deprecated attribute is not defined in GCC < 4.5. */ +# define KRML_DEPRECATED(x) +#elif defined(__SUNPRO_C) +# define KRML_DEPRECATED(x) __attribute__((deprecated(x))) +#elif defined(_MSC_VER) +# define KRML_DEPRECATED(x) __declspec(deprecated(x)) +#endif + /* Macros for prettier unrolling of loops */ #define KRML_LOOP1(i, n, x) { \ x \ diff --git a/Modules/_hacl/include/krml/internal/types.h b/Modules/_hacl/include/krml/internal/types.h new file mode 100644 index 00000000000000..2280dfad48db1e --- /dev/null +++ b/Modules/_hacl/include/krml/internal/types.h @@ -0,0 +1,106 @@ +/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 and MIT Licenses. */ + +#ifndef KRML_TYPES_H +#define KRML_TYPES_H +#define KRML_VERIFIED_UINT128 + +#include +#include +#include +#include + +/* Types which are either abstract, meaning that have to be implemented in C, or + * which are models, meaning that they are swapped out at compile-time for + * hand-written C types (in which case they're marked as noextract). */ + +typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_; +typedef int64_t FStar_Int64_t, FStar_Int64_t_; +typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_; +typedef int32_t FStar_Int32_t, FStar_Int32_t_; +typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_; +typedef int16_t FStar_Int16_t, FStar_Int16_t_; +typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_; +typedef int8_t FStar_Int8_t, FStar_Int8_t_; + +/* Only useful when building krmllib, because it's in the dependency graph of + * FStar.Int.Cast. */ +typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_; +typedef int64_t FStar_Int63_t, FStar_Int63_t_; + +typedef double FStar_Float_float; +typedef uint32_t FStar_Char_char; +typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write; + +typedef void *FStar_Dyn_dyn; + +typedef const char *C_String_t, *C_String_t_, *C_Compat_String_t, *C_Compat_String_t_; + +typedef int exit_code; +typedef FILE *channel; + +typedef unsigned long long TestLib_cycles; + +typedef uint64_t FStar_Date_dateTime, FStar_Date_timeSpan; + +/* Now Prims.string is no longer illegal with the new model in LowStar.Printf; + * it's operations that produce Prims_string which are illegal. Bring the + * definition into scope by default. */ +typedef const char *Prims_string; + +#if (defined(_MSC_VER) && defined(_M_X64) && !defined(__clang__)) +#define IS_MSVC64 1 +#endif + +/* This code makes a number of assumptions and should be refined. In particular, + * it assumes that: any non-MSVC amd64 compiler supports int128. Maybe it would + * be easier to just test for defined(__SIZEOF_INT128__) only? */ +#if (defined(__x86_64__) || \ + defined(__x86_64) || \ + defined(__aarch64__) || \ + (defined(__powerpc64__) && defined(__LITTLE_ENDIAN__)) || \ + defined(__s390x__) || \ + (defined(_MSC_VER) && defined(_M_X64) && defined(__clang__)) || \ + (defined(__mips__) && defined(__LP64__)) || \ + (defined(__riscv) && __riscv_xlen == 64) || \ + defined(__SIZEOF_INT128__)) +#define HAS_INT128 1 +#endif + +/* The uint128 type is a special case since we offer several implementations of + * it, depending on the compiler and whether the user wants the verified + * implementation or not. */ +#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64) +# include +typedef __m128i FStar_UInt128_uint128; +#elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128) +typedef unsigned __int128 FStar_UInt128_uint128; +#else +typedef struct FStar_UInt128_uint128_s { + uint64_t low; + uint64_t high; +} FStar_UInt128_uint128; +#endif + +/* The former is defined once, here (otherwise, conflicts for test-c89. The + * latter is for internal use. */ +typedef FStar_UInt128_uint128 FStar_UInt128_t, uint128_t; + +#include "krml/lowstar_endianness.h" + +#endif + +/* Avoid a circular loop: if this header is included via FStar_UInt8_16_32_64, + * then don't bring the uint128 definitions into scope. */ +#ifndef __FStar_UInt_8_16_32_64_H + +#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64) +#include "fstar_uint128_msvc.h" +#elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128) +#include "fstar_uint128_gcc64.h" +#else +#include "krml/FStar_UInt128_Verified.h" +#include "krml/fstar_uint128_struct_endianness.h" +#endif + +#endif diff --git a/Modules/_hacl/include/krml/types.h b/Modules/_hacl/include/krml/types.h deleted file mode 100644 index 509f555536e4c6..00000000000000 --- a/Modules/_hacl/include/krml/types.h +++ /dev/null @@ -1,14 +0,0 @@ -#pragma once - -#include - -typedef struct FStar_UInt128_uint128_s { - uint64_t low; - uint64_t high; -} FStar_UInt128_uint128, uint128_t; - -#define KRML_VERIFIED_UINT128 - -#include "krml/lowstar_endianness.h" -#include "krml/fstar_uint128_struct_endianness.h" -#include "krml/FStar_UInt128_Verified.h" diff --git a/Modules/_hacl/internal/Hacl_Hash_Blake2b.h b/Modules/_hacl/internal/Hacl_Hash_Blake2b.h index 8ee70282f4e4de..e74c320e073f4b 100644 --- a/Modules/_hacl/internal/Hacl_Hash_Blake2b.h +++ b/Modules/_hacl/internal/Hacl_Hash_Blake2b.h @@ -31,11 +31,11 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" -#include "internal/Hacl_Impl_Blake2_Constants.h" +#include "internal/Hacl_Streaming_Types.h" #include "../Hacl_Hash_Blake2b.h" typedef struct Hacl_Hash_Blake2b_params_and_key_s @@ -70,6 +70,23 @@ Hacl_Hash_Blake2b_update_last( void Hacl_Hash_Blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash); +typedef struct Hacl_Hash_Blake2b_block_state_t_s +{ + uint8_t fst; + uint8_t snd; + bool thd; + Hacl_Streaming_Types_two_pointers f3; +} +Hacl_Hash_Blake2b_block_state_t; + +typedef struct Hacl_Hash_Blake2b_state_t_s +{ + Hacl_Hash_Blake2b_block_state_t block_state; + uint8_t *buf; + uint64_t total_len; +} +Hacl_Hash_Blake2b_state_t; + #if defined(__cplusplus) } #endif diff --git a/Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h b/Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h index ab329b92c3630c..27633f22b24f0d 100644 --- a/Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h +++ b/Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h @@ -31,12 +31,10 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" -#include "internal/Hacl_Impl_Blake2_Constants.h" -#include "internal/Hacl_Hash_Blake2b.h" #include "../Hacl_Hash_Blake2b_Simd256.h" #include "libintvector.h" @@ -83,7 +81,54 @@ Hacl_Hash_Blake2b_Simd256_store_state256b_to_state32( Lib_IntVector_Intrinsics_vec256 *st ); -Lib_IntVector_Intrinsics_vec256 *Hacl_Hash_Blake2b_Simd256_malloc_with_key(void); +Lib_IntVector_Intrinsics_vec256 +*Hacl_Hash_Blake2b_Simd256_malloc_internal_state_with_key(void); + +void +Hacl_Hash_Blake2b_Simd256_update_multi_no_inline( + Lib_IntVector_Intrinsics_vec256 *s, + FStar_UInt128_uint128 ev, + uint8_t *blocks, + uint32_t n +); + +void +Hacl_Hash_Blake2b_Simd256_update_last_no_inline( + Lib_IntVector_Intrinsics_vec256 *s, + FStar_UInt128_uint128 prev, + uint8_t *input, + uint32_t input_len +); + +void +Hacl_Hash_Blake2b_Simd256_copy_internal_state( + Lib_IntVector_Intrinsics_vec256 *src, + Lib_IntVector_Intrinsics_vec256 *dst +); + +typedef struct Hacl_Hash_Blake2b_Simd256_two_2b_256_s +{ + Lib_IntVector_Intrinsics_vec256 *fst; + Lib_IntVector_Intrinsics_vec256 *snd; +} +Hacl_Hash_Blake2b_Simd256_two_2b_256; + +typedef struct Hacl_Hash_Blake2b_Simd256_block_state_t_s +{ + uint8_t fst; + uint8_t snd; + bool thd; + Hacl_Hash_Blake2b_Simd256_two_2b_256 f3; +} +Hacl_Hash_Blake2b_Simd256_block_state_t; + +typedef struct Hacl_Hash_Blake2b_Simd256_state_t_s +{ + Hacl_Hash_Blake2b_Simd256_block_state_t block_state; + uint8_t *buf; + uint64_t total_len; +} +Hacl_Hash_Blake2b_Simd256_state_t; #if defined(__cplusplus) } diff --git a/Modules/_hacl/internal/Hacl_Hash_Blake2s.h b/Modules/_hacl/internal/Hacl_Hash_Blake2s.h index 6494075b60a25b..0c5781df8cea81 100644 --- a/Modules/_hacl/internal/Hacl_Hash_Blake2s.h +++ b/Modules/_hacl/internal/Hacl_Hash_Blake2s.h @@ -31,12 +31,10 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" -#include "internal/Hacl_Impl_Blake2_Constants.h" -#include "internal/Hacl_Hash_Blake2b.h" #include "../Hacl_Hash_Blake2s.h" void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn); @@ -64,6 +62,30 @@ Hacl_Hash_Blake2s_update_last( void Hacl_Hash_Blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash); +typedef struct K____uint32_t___uint32_t__s +{ + uint32_t *fst; + uint32_t *snd; +} +K____uint32_t___uint32_t_; + +typedef struct Hacl_Hash_Blake2s_block_state_t_s +{ + uint8_t fst; + uint8_t snd; + bool thd; + K____uint32_t___uint32_t_ f3; +} +Hacl_Hash_Blake2s_block_state_t; + +typedef struct Hacl_Hash_Blake2s_state_t_s +{ + Hacl_Hash_Blake2s_block_state_t block_state; + uint8_t *buf; + uint64_t total_len; +} +Hacl_Hash_Blake2s_state_t; + #if defined(__cplusplus) } #endif diff --git a/Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h b/Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h index 60c09a67b445b6..0f5db552d6cfed 100644 --- a/Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h +++ b/Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h @@ -31,12 +31,10 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" -#include "internal/Hacl_Impl_Blake2_Constants.h" -#include "internal/Hacl_Hash_Blake2b.h" #include "../Hacl_Hash_Blake2s_Simd128.h" #include "libintvector.h" @@ -83,7 +81,54 @@ Hacl_Hash_Blake2s_Simd128_load_state128s_from_state32( uint32_t *st32 ); -Lib_IntVector_Intrinsics_vec128 *Hacl_Hash_Blake2s_Simd128_malloc_with_key(void); +Lib_IntVector_Intrinsics_vec128 +*Hacl_Hash_Blake2s_Simd128_malloc_internal_state_with_key(void); + +void +Hacl_Hash_Blake2s_Simd128_update_multi_no_inline( + Lib_IntVector_Intrinsics_vec128 *s, + uint64_t ev, + uint8_t *blocks, + uint32_t n +); + +void +Hacl_Hash_Blake2s_Simd128_update_last_no_inline( + Lib_IntVector_Intrinsics_vec128 *s, + uint64_t prev, + uint8_t *input, + uint32_t input_len +); + +void +Hacl_Hash_Blake2s_Simd128_copy_internal_state( + Lib_IntVector_Intrinsics_vec128 *src, + Lib_IntVector_Intrinsics_vec128 *dst +); + +typedef struct Hacl_Hash_Blake2s_Simd128_two_2s_128_s +{ + Lib_IntVector_Intrinsics_vec128 *fst; + Lib_IntVector_Intrinsics_vec128 *snd; +} +Hacl_Hash_Blake2s_Simd128_two_2s_128; + +typedef struct Hacl_Hash_Blake2s_Simd128_block_state_t_s +{ + uint8_t fst; + uint8_t snd; + bool thd; + Hacl_Hash_Blake2s_Simd128_two_2s_128 f3; +} +Hacl_Hash_Blake2s_Simd128_block_state_t; + +typedef struct Hacl_Hash_Blake2s_Simd128_state_t_s +{ + Hacl_Hash_Blake2s_Simd128_block_state_t block_state; + uint8_t *buf; + uint64_t total_len; +} +Hacl_Hash_Blake2s_Simd128_state_t; #if defined(__cplusplus) } diff --git a/Modules/_hacl/internal/Hacl_Hash_MD5.h b/Modules/_hacl/internal/Hacl_Hash_MD5.h index a50ec407f53e39..7fe71a49c6df85 100644 --- a/Modules/_hacl/internal/Hacl_Hash_MD5.h +++ b/Modules/_hacl/internal/Hacl_Hash_MD5.h @@ -31,10 +31,11 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" +#include "Hacl_Streaming_Types.h" #include "../Hacl_Hash_MD5.h" void Hacl_Hash_MD5_init(uint32_t *s); diff --git a/Modules/_hacl/internal/Hacl_Hash_SHA1.h b/Modules/_hacl/internal/Hacl_Hash_SHA1.h index b39bad3f3b93e8..ed53be559fe465 100644 --- a/Modules/_hacl/internal/Hacl_Hash_SHA1.h +++ b/Modules/_hacl/internal/Hacl_Hash_SHA1.h @@ -31,7 +31,7 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" diff --git a/Modules/_hacl/internal/Hacl_Hash_SHA2.h b/Modules/_hacl/internal/Hacl_Hash_SHA2.h index cb60f9e9bd4df6..98498ee9376996 100644 --- a/Modules/_hacl/internal/Hacl_Hash_SHA2.h +++ b/Modules/_hacl/internal/Hacl_Hash_SHA2.h @@ -31,11 +31,10 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" - #include "../Hacl_Hash_SHA2.h" static const diff --git a/Modules/_hacl/internal/Hacl_Hash_SHA3.h b/Modules/_hacl/internal/Hacl_Hash_SHA3.h index 0a152b4c622533..e653c73b1d03f7 100644 --- a/Modules/_hacl/internal/Hacl_Hash_SHA3.h +++ b/Modules/_hacl/internal/Hacl_Hash_SHA3.h @@ -31,10 +31,11 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" +#include "Hacl_Streaming_Types.h" #include "../Hacl_Hash_SHA3.h" extern const uint32_t Hacl_Hash_SHA3_keccak_rotc[24U]; @@ -43,6 +44,8 @@ extern const uint32_t Hacl_Hash_SHA3_keccak_piln[24U]; extern const uint64_t Hacl_Hash_SHA3_keccak_rndc[24U]; +void Hacl_Hash_SHA3_init_(Spec_Hash_Definitions_hash_alg a, uint64_t *s); + void Hacl_Hash_SHA3_update_multi_sha3( Spec_Hash_Definitions_hash_alg a, @@ -59,6 +62,21 @@ Hacl_Hash_SHA3_update_last_sha3( uint32_t input_len ); +typedef struct Hacl_Hash_SHA3_hash_buf_s +{ + Spec_Hash_Definitions_hash_alg fst; + uint64_t *snd; +} +Hacl_Hash_SHA3_hash_buf; + +typedef struct Hacl_Hash_SHA3_state_t_s +{ + Hacl_Hash_SHA3_hash_buf block_state; + uint8_t *buf; + uint64_t total_len; +} +Hacl_Hash_SHA3_state_t; + #if defined(__cplusplus) } #endif diff --git a/Modules/_hacl/internal/Hacl_Impl_Blake2_Constants.h b/Modules/_hacl/internal/Hacl_Impl_Blake2_Constants.h index f4cf516124aabb..fb3a045cd5c608 100644 --- a/Modules/_hacl/internal/Hacl_Impl_Blake2_Constants.h +++ b/Modules/_hacl/internal/Hacl_Impl_Blake2_Constants.h @@ -31,7 +31,7 @@ extern "C" { #endif #include -#include "krml/types.h" +#include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" diff --git a/Modules/_hacl/internal/Hacl_Streaming_Types.h b/Modules/_hacl/internal/Hacl_Streaming_Types.h new file mode 100644 index 00000000000000..fed3cbd425917c --- /dev/null +++ b/Modules/_hacl/internal/Hacl_Streaming_Types.h @@ -0,0 +1,87 @@ +/* MIT License + * + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ + + +#ifndef __internal_Hacl_Streaming_Types_H +#define __internal_Hacl_Streaming_Types_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "../Hacl_Streaming_Types.h" + +#define Hacl_Streaming_Types_None 0 +#define Hacl_Streaming_Types_Some 1 + +typedef uint8_t Hacl_Streaming_Types_optional; + +typedef struct Hacl_Streaming_Types_optional_32_s +{ + Hacl_Streaming_Types_optional tag; + uint32_t *v; +} +Hacl_Streaming_Types_optional_32; + +typedef struct Hacl_Streaming_Types_optional_64_s +{ + Hacl_Streaming_Types_optional tag; + uint64_t *v; +} +Hacl_Streaming_Types_optional_64; + +typedef struct Hacl_Streaming_Types_two_pointers_s +{ + uint64_t *fst; + uint64_t *snd; +} +Hacl_Streaming_Types_two_pointers; + +typedef struct Hacl_Streaming_MD_state_32_s +{ + uint32_t *block_state; + uint8_t *buf; + uint64_t total_len; +} +Hacl_Streaming_MD_state_32; + +typedef struct Hacl_Streaming_MD_state_64_s +{ + uint64_t *block_state; + uint8_t *buf; + uint64_t total_len; +} +Hacl_Streaming_MD_state_64; + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Streaming_Types_H_DEFINED +#endif diff --git a/Modules/_hacl/libintvector.h b/Modules/_hacl/libintvector.h index 11e914f7e1650a..6db5253eee4f24 100644 --- a/Modules/_hacl/libintvector.h +++ b/Modules/_hacl/libintvector.h @@ -3,6 +3,8 @@ #include +#ifndef HACL_INTRINSICS_SHIMMED + /* We include config.h here to ensure that the various feature-flags are * properly brought into scope. Users can either run the configure script, or * write a config.h themselves and put it under version control. */ @@ -933,4 +935,6 @@ typedef vector128_8 vector128; #endif #endif +#endif // HACL_INTRINSICS_SHIMMED + #endif // __Vec_Intrin_H diff --git a/Modules/_hacl/refresh.sh b/Modules/_hacl/refresh.sh index 4147ab302fe146..86e5b4b0161072 100755 --- a/Modules/_hacl/refresh.sh +++ b/Modules/_hacl/refresh.sh @@ -22,7 +22,7 @@ fi # Update this when updating to a new version after verifying that the changes # the update brings in are good. -expected_hacl_star_rev=f218923ef2417d963d7efc7951593ae6aef613f7 +expected_hacl_star_rev=322f6d58290e0ed7f4ecb84fcce12917aa0f594b hacl_dir="$(realpath "$1")" cd "$(dirname "$0")" @@ -58,6 +58,7 @@ dist_files=( internal/Hacl_Hash_Blake2b_Simd256.h internal/Hacl_Hash_Blake2s_Simd128.h internal/Hacl_Impl_Blake2_Constants.h + internal/Hacl_Streaming_Types.h Hacl_Hash_MD5.c Hacl_Hash_SHA1.c Hacl_Hash_SHA2.c @@ -74,7 +75,9 @@ dist_files=( declare -a include_files include_files=( include/krml/lowstar_endianness.h + include/krml/internal/compat.h include/krml/internal/target.h + include/krml/internal/types.h ) declare -a lib_files @@ -110,32 +113,12 @@ fi readarray -t all_files < <(find . -name '*.h' -or -name '*.c') -# types.h originally contains a complex series of if-defs and auxiliary type -# definitions; here, we just need a proper uint128 type in scope -# is a simple wrapper that defines the uint128 type -cat > include/krml/types.h < - -typedef struct FStar_UInt128_uint128_s { - uint64_t low; - uint64_t high; -} FStar_UInt128_uint128, uint128_t; - -#define KRML_VERIFIED_UINT128 - -#include "krml/lowstar_endianness.h" -#include "krml/fstar_uint128_struct_endianness.h" -#include "krml/FStar_UInt128_Verified.h" -EOF # Adjust the include path to reflect the local directory structure -$sed -i 's!#include.*types.h"!#include "krml/types.h"!g' "${all_files[@]}" -$sed -i 's!#include.*compat.h"!!g' "${all_files[@]}" +$sed -i 's!#include "FStar_UInt128_Verified.h"!#include "krml/FStar_UInt128_Verified.h"!g' include/krml/internal/types.h +$sed -i 's!#include "fstar_uint128_struct_endianness.h"!#include "krml/fstar_uint128_struct_endianness.h"!g' include/krml/internal/types.h -# FStar_UInt_8_16_32_64 contains definitions useful in the general case, but not -# for us; trim! -$sed -i -z 's!\(extern\|typedef\)[^;]*;\n\n!!g' include/krml/FStar_UInt_8_16_32_64.h +# use KRML_VERIFIED_UINT128 +$sed -i -z 's!#define KRML_TYPES_H!#define KRML_TYPES_H\n#define KRML_VERIFIED_UINT128!g' include/krml/internal/types.h # This contains static inline prototypes that are defined in # FStar_UInt_8_16_32_64; they are by default repeated for safety of separate @@ -143,14 +126,7 @@ $sed -i -z 's!\(extern\|typedef\)[^;]*;\n\n!!g' include/krml/FStar_UInt_8_16_32_ $sed -i 's!#include.*Hacl_Krmllib.h"!!g' "${all_files[@]}" # Use globally unique names for the Hacl_ C APIs to avoid linkage conflicts. -$sed -i -z 's!#include \n!#include \n#include "python_hacl_namespaces.h"\n!' Hacl_Hash_*.h - -# Finally, we remove a bunch of ifdefs from target.h that are, again, useful in -# the general case, but not exercised by the subset of HACL* that we vendor. -$sed -z -i 's!#ifndef KRML_\(HOST_TIME\)\n\(\n\|# [^\n]*\n\|[^#][^\n]*\n\)*#endif\n\n!!g' include/krml/internal/target.h -$sed -z -i 's!\n\n\([^#][^\n]*\n\)*#define KRML_\(EABORT\|EXIT\)[^\n]*\(\n [^\n]*\)*!!g' include/krml/internal/target.h -$sed -z -i 's!\n\n\([^#][^\n]*\n\)*#if [^\n]*\n\( [^\n]*\n\)*#define KRML_\(EABORT\|EXIT\|CHECK_SIZE\)[^\n]*\(\n [^\n]*\)*!!g' include/krml/internal/target.h -$sed -z -i 's!\n\n\([^#][^\n]*\n\)*#if [^\n]*\n\( [^\n]*\n\)*# define _\?KRML_\(DEPRECATED\|HOST_SNPRINTF\)[^\n]*\n\([^#][^\n]*\n\|#el[^\n]*\n\|# [^\n]*\n\)*#endif!!g' include/krml/internal/target.h +$sed -i -z 's!#include !#include \n#include "python_hacl_namespaces.h"!' Hacl_Hash_*.h # Step 3: trim whitespace (for the linter) diff --git a/PCbuild/pythoncore.vcxproj b/PCbuild/pythoncore.vcxproj index 3b3c3972987db8..5175b1b2e76244 100644 --- a/PCbuild/pythoncore.vcxproj +++ b/PCbuild/pythoncore.vcxproj @@ -100,7 +100,7 @@ /Zm200 %(AdditionalOptions) - $(PySourcePath)Modules\_hacl\include;$(PySourcePath)Modules\_hacl\internal;$(PySourcePath)Python;%(AdditionalIncludeDirectories) + $(PySourcePath)Modules\_hacl;$(PySourcePath)Modules\_hacl\include;$(PySourcePath)Python;%(AdditionalIncludeDirectories) $(zlibDir);%(AdditionalIncludeDirectories) _USRDLL;Py_BUILD_CORE;Py_BUILD_CORE_BUILTIN;Py_ENABLE_SHARED;MS_DLL_ID="$(SysWinVer)";%(PreprocessorDefinitions) _Py_HAVE_ZLIB;%(PreprocessorDefinitions)