Updates the HACL* implementation used by hashlib from upstream sources.
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
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)
#########################################################################
--- /dev/null
+Update the vendored HACL* library to fix build issues with older clang
+compilers.
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "1cd3cda98e0e6882a13a59268b88640c542350fd"
+ "checksumValue": "4b6e7696e8d84f322fb24b1fbb08ccb9b0e7d51b"
},
{
"algorithm": "SHA256",
- "checksumValue": "41a420bc9355e451720e60e9536e66f04dc6e416ca9217c4ab18d827887a2e08"
+ "checksumValue": "50a65a34a7a7569eedf7fa864a7892eeee5840a7fdf6fa8f1e87d42c65f6c877"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2b.c"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "b0b3ae92d6aee7b52bacfdf02409d8d7e23701ee"
+ "checksumValue": "7c66ac004a1dcf3fee0ab9aa62d61972f029de3a"
},
{
"algorithm": "SHA256",
- "checksumValue": "95d1dd4097a706b0719610da674297fa253b30d03a6ead4685ed648e20cb51a2"
+ "checksumValue": "9a7239a01a4ee8defbe3ebd9f0d12c873a1dd8e0659070380b2eab3ab0177333"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2b.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "0ceef306590ec12251db03a31fc08ecba697486d"
+ "checksumValue": "0f75e44a42775247a46acc2beaa6bae8f199a3d9"
},
{
"algorithm": "SHA256",
- "checksumValue": "1575a23b21319e55e670f74194fc2dfd1777eb5a3816cad43750e03da6e44db9"
+ "checksumValue": "03b612c24193464ed6848aeebbf44f9266b78ec6eed2486056211cde8992c49a"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2b_Simd256.c"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "a5011646670c4f51368aca661e458e4c7f1d88e0"
+ "checksumValue": "7f273d26942233e5dcdfb4c1a16ff2486b15f899"
},
{
"algorithm": "SHA256",
- "checksumValue": "f00c1fe8e774c7ec65f6c5a8efa43ce180a17fc80ed6119ada8c4022d058b6e2"
+ "checksumValue": "dbc0dacc68ed52dbf1b7d6fba2c87870317998bc046e65f6deaaa150625432f8"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2b_Simd256.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "9616a9f8d795d64487bf86a96719f943729621e2"
+ "checksumValue": "65bf44140691b046dcfed3ab1576dbf8bbf96dc5"
},
{
"algorithm": "SHA256",
- "checksumValue": "5ecde5ddc8ec073cffe64d60e868535d995f33fb0f87f9b50e68bd2a694b7434"
+ "checksumValue": "0f98959dafffce039ade9d296f7a05bed151c9c512498f48e4b326a5523a240b"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2s.c"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "0328172a62507a051cd60ff9603710ed5aea1bc8"
+ "checksumValue": "2120c8c467aeebcc7c8b9678c15e79648433b91a"
},
{
"algorithm": "SHA256",
- "checksumValue": "9f3c8ef615c9fbc59ef796d0ad2a7a76a7e55dc8939077b44ca538cbf8889a8c"
+ "checksumValue": "45735f7fe2dbbad7656d07854e9ec8176ad26c79f90dcc0fec0b9a59a6311ba7"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2s.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "5b950ce0a5c8f0c2c56b4ac96e1943b504255d45"
+ "checksumValue": "0da9782455923aede8d8dce9dfdc38f4fc1de572"
},
{
"algorithm": "SHA256",
- "checksumValue": "5a5f5d8e376dc30d89fd6c6c435157fe9ffa5308030e7abb1256afaee0765536"
+ "checksumValue": "2d17ae768fd3d7d6decddd8b4aaf23ce02a809ee62bb98da32c8a7f54acf92d0"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2s_Simd128.c"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "32f35c173c10a2c49ac53c839cfbccd8a147274d"
+ "checksumValue": "9028e24c9876d9d16b2435ec29240c6b57bfe2a0"
},
{
"algorithm": "SHA256",
- "checksumValue": "8734879b551f0fa860002ae81c0d0cfbade561007d9c26ad18c5a221e239237e"
+ "checksumValue": "062e3b856acac4f929c1e04b8264a754cad21ca6580215f7094a3f0a04edb912"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2s_Simd128.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "f8ba39b46ebdfa7d031d9c33130c6ded680a8120"
+ "checksumValue": "38e8d96ef1879480780494058a93cec181f8d6d7"
},
{
"algorithm": "SHA256",
- "checksumValue": "f71cf6a0e8f09354c2af2c785a1d36e0cba7613a589be01ca8a3d8478f4c8874"
+ "checksumValue": "61e77d2063cf60c96e9ce06af215efe5d42c43026833bffed5732326fe97ed1e"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_MD5.c"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "eaaab54cea2b0bb8ec0eedf0b373d42f1a0f8f6c"
+ "checksumValue": "e67a9bc18358c57afaeff3a174893ddfdb52dfc6"
},
{
"algorithm": "SHA256",
- "checksumValue": "9a02e2a6e163515ea0228a859d5e55c1f57b11fae5908c42f9f9814ce9bca230"
+ "checksumValue": "16e982081f6c2fd03ea751fcc64f5a835c94652841836e231fe562b9e287f4bc"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_MD5.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "f4f42faf8da78a230199f649c0f2a1b865799a31"
+ "checksumValue": "986dd5ba0b34d15f3e5e5c656979aea1b502e8aa"
},
{
"algorithm": "SHA256",
- "checksumValue": "5b29bd9951646861e0e19427be5d923a5bab7a4516824ccc068f696469195eec"
+ "checksumValue": "38d5f1f2e67a0eb30789f81fc56c07a6e7246e2b1be6c65485bcca1dcd0e0806"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA1.c"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "722b57139737ceeb88e41d3839e6f7d70578741b"
+ "checksumValue": "f1ca21f1ee8b15ad9ccfbda72165b9d86912166c"
},
{
"algorithm": "SHA256",
- "checksumValue": "5640295c790d56b1b4df147d6a6c58803b1845cd7d93365bf7cc7b75ba3cacd5"
+ "checksumValue": "4b2ad9ea93fdd9c2fdc521fc4e14e02550666c2717a23b85819db2e07ea555f3"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA1.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "b0aa8810339adb09623ffa429246b4324fac4565"
+ "checksumValue": "f732a6710fe3e13cd28130f0f20504e347d1c412"
},
{
"algorithm": "SHA256",
- "checksumValue": "2288f8f860efe80eed4f1e14ef570079b7459aeb41f87e94e691d7cf5e0e7adb"
+ "checksumValue": "86cf32e4d1f3ba93a94108271923fdafe2204447792a918acf4a2250f352dbde"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA2.c"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "4903e10291d07367be3bc283935bc52926e57ba1"
+ "checksumValue": "f38cebeeca40a83aeb2cf5dfce578ffefe176d84"
},
{
"algorithm": "SHA256",
- "checksumValue": "093d7693084af0999d2a13d207311d74b5bdfdc9c08447ed4a979e3f7505ae6b"
+ "checksumValue": "ee03bf9368d1a3a3c70cfd4e9391b2485466404db4a60bfc5319630cc314b590"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA2.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "ef374b9d0951ebb38006af944dd4b38a6cf3abb2"
+ "checksumValue": "50f75337b31f509b5bfcc7ebb3d066b82a0f1b33"
},
{
"algorithm": "SHA256",
- "checksumValue": "164df19f229143006c5f9a3c0bd771415f152bfbc7efb61c337fa0f903003eb3"
+ "checksumValue": "c9e1442899e5b902fa39f413f1a3131f7ab5c2283d5100dc8ac675a7d5ebbdf1"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA3.c"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "7d78e6844dde1f9b5e68f58ca105a4c330461ff6"
+ "checksumValue": "01717207aef77174e328186d48c27517f6644c15"
},
{
"algorithm": "SHA256",
- "checksumValue": "231d9bc13190be4b6821acb518194f32f4a3c04f1c034b3118f6db0bab2debe3"
+ "checksumValue": "620dded172e94cb3f25f9904b44977d91f2cc9573e41b38f19e929d083ae0308"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA3.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "ab7b4d9465a2765a07f8d5bccace7182b28ed1b8"
+ "checksumValue": "372448599774a98e5c5d083e91f301ed1c4b822e"
},
{
"algorithm": "SHA256",
- "checksumValue": "26913613f3b4f8ffff0a3e211a5ebc849159094e5e11de0a31fcb95b6105b74c"
+ "checksumValue": "95d8e70ca4bc6aa98f6d2435ceb6410ead299b1f700fae1f5c603ec3f57ea551"
}
],
"fileName": "Modules/_hacl/Hacl_Streaming_Types.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "118dc712780ea680affa8d9794470440eb87ff10"
+ "checksumValue": "80dae56879ed9bace476362ef251de48ce055a20"
},
{
"algorithm": "SHA256",
- "checksumValue": "b017e7d5662a308c938cf4e4b919680c8f3e27f42975ca152b62fe65c5f7fb0c"
+ "checksumValue": "da84b6287e9aa1fc52e819a8ca10e79b51263f1dda6b4528ed8c0c74a11fb0ea"
}
],
"fileName": "Modules/_hacl/Lib_Memzero0.c"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "7665829b9396f72e7f8098080d6d6773565468e9"
+ "checksumValue": "eaa543c778300238dc23034aafeada0951154af1"
},
{
"algorithm": "SHA256",
- "checksumValue": "ca7357ee70365c690664a44f6522e526636151d9ed2da8d0d29da15bb8556530"
+ "checksumValue": "3fd2552d527a23110d61ad2811c774810efb1eaee008f136c2a0d609daa77f5b"
}
],
"fileName": "Modules/_hacl/include/krml/FStar_UInt128_Verified.h"
"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"
],
"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"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "3f4fdfdaef97a2cbac5ec091c91ede18d4b33f92"
+ "checksumValue": "878ae284c93824b80b1763e8b3e6be3c410777a8"
},
{
"algorithm": "SHA256",
- "checksumValue": "96b1c77860f12bcadad0caca77a5a1649a840ad9989d97984a3b51bb98c80e2f"
+ "checksumValue": "49df6223f6403daf503a1af1a3d2f943d30b5889fe7ed20299c3df24c1e3853d"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "9efd61f6ba8d126e98abd83679a5ed5954278c31"
+ "checksumValue": "25552d8cbf8aa345907635b38f284eec9075301e"
},
{
"algorithm": "SHA256",
- "checksumValue": "143f58f033786173501a72ac302e435963fdce6c2cc38eef6d6adeb3cdc1bb9c"
+ "checksumValue": "a3424cf4c5518654908086bbbf5d465715ec3b23625ef0cadc29492d1f90366c"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2s.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "3f984829465285283b03b1111b4918cfb48b8031"
+ "checksumValue": "54a712fc3ed5a817288351cbac5b7d9afa7e379f"
},
{
"algorithm": "SHA256",
- "checksumValue": "cd24038fdd617edc65e472496b0d58f23ff312f81f9244c3e7893fdc9a1b2977"
+ "checksumValue": "c6abae648b8a1e9d5631c0a959620cad1f7e92ce522e07c3416199fe51debef6"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "60f02d21f045c8a4c2b6b84a8f7e023d9490c8e5"
+ "checksumValue": "c15c5f83bbb9f62611c49f0f8f723eaab1a27488"
},
{
"algorithm": "SHA256",
- "checksumValue": "370d8ef9c48cb55472ece11e12eaf94c58118de3f5515b6df1c130b696597828"
+ "checksumValue": "95cd5d91c4a9217901d0b3395dcd8881e62e2055d723b532ec5176386a636d22"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_MD5.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "6346c30a140e7d3010c98fe19d14fa229a54eb16"
+ "checksumValue": "7b8717e3a24e7e16a34b251d0d02da6f68439695"
},
{
"algorithm": "SHA256",
- "checksumValue": "ab52c6092bdbbfc9884f841bf4824016792ffa96167577cbe0df00dd96f56a34"
+ "checksumValue": "9473d8bc9506fe0053d7d98c225d4873011329863f1c4a8e93e43fc71bd1f314"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_SHA1.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "2e9ae174142fc491f20567ab8b5c08cef9b07cfe"
+ "checksumValue": "e319c949f5a2dd765be2c8c7ff77bfe52ee6c7da"
},
{
"algorithm": "SHA256",
- "checksumValue": "07100964adcf4b5f8bd4773e25f475b34cd180b90df8b1c0052e55c008b7cc49"
+ "checksumValue": "75261448e51c3eb1ba441e973b193e23570b167f67743942ee2ee57417491c9f"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_SHA2.h"
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "39ba6e8959e44ae956a640d3a1fb3ef60de8a9e5"
+ "checksumValue": "dbd92415c31606804102b79d5ba3d1752fe03887"
},
{
"algorithm": "SHA256",
- "checksumValue": "dbf4b86a04b4d8716976f8c023cccbfe174435dbec3bc00fc1f066fb52c4e341"
+ "checksumValue": "5d74a76a0ac3659a1ae1276c3ca55521f09e83d2f0039f5c519a76f8f3c76a8e"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_SHA3.h"
"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": [
"checksums": [
{
"algorithm": "SHA1",
- "checksumValue": "f4a33ad535768b860362ab0bd033a70da0b524b7"
+ "checksumValue": "63e47cc290c4ec887dca708000876ac37ee75ba0"
},
{
"algorithm": "SHA256",
- "checksumValue": "433cdf4ba80bc72e0cea5d4b420ff18676baeafdb5ba19adf5b7fb33e90b424b"
+ "checksumValue": "d09a6196d65c2645974100eb922002bd387d3ae13f2653780f82ed97a79af635"
}
],
"fileName": "Modules/_hacl/libintvector.h"
"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"
}
],
"name": "hacl-star",
"originator": "Organization: HACL* Developers",
"primaryPackagePurpose": "SOURCE",
- "versionInfo": "f218923ef2417d963d7efc7951593ae6aef613f7"
+ "versionInfo": "322f6d58290e0ed7f4ecb84fcce12917aa0f594b"
},
{
"SPDXID": "SPDXRef-PACKAGE-macholib",
"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"
},
"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",
#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"
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);
}
/**
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;
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;
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;
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;
}
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;
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;
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);
}
/**
#include <string.h>
#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;
#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
#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"
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);
}
/**
*/
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 };
*/
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)
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;
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;
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;
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;
}
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;
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;
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);
}
/**
#include <string.h>
#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)
#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
*/
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
#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"
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);
}
/**
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);
}
/**
#include <string.h>
#include "python_hacl_namespaces.h"
-#include "krml/types.h"
+#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"
#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
#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"
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);
}
/**
*/
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 };
*/
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)
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;
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;
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;
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;
}
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;
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);
}
/**
#include <string.h>
#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)
#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
*/
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
#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
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)
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)
#include <string.h>
#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 "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)
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)
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)
#include <string.h>
#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 "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)
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);
}
/**
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);
}
/**
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)
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);
}
/**
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)
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)
#include <string.h>
#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;
#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] =
}
}
+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,
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;
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)
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)
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;
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
#include <string.h>
#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);
#endif
#include <string.h>
-#include "krml/types.h"
+#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"
#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)
}
#include <AvailabilityMacros.h>
#endif
-#if (defined(__APPLE__) && defined(__MACH__)) || defined(__linux__)
+#if (defined(__APPLE__) && defined(__MACH__)) || defined(__linux__) || defined(__OpenBSD__)
#define __STDC_WANT_LIB_EXT1__ 1
#include <string.h>
#endif
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_);
#include "FStar_UInt_8_16_32_64.h"
#include <inttypes.h>
#include <stdbool.h>
-#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)
#include <inttypes.h>
#include <stdbool.h>
-
+#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;
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;
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;
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;
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
--- /dev/null
+/* 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 <inttypes.h>
+
+/* 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
#endif
#ifndef KRML_MAYBE_UNUSED
-# if defined(__GNUC__)
+# if defined(__GNUC__) || defined(__clang__)
# define KRML_MAYBE_UNUSED __attribute__((unused))
# else
# define KRML_MAYBE_UNUSED
#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)
#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
# endif
#endif
+#ifndef KRML_HOST_TIME
+
+# include <time.h>
+
+/* 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).
*/
} \
} 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 \
--- /dev/null
+/* 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 <inttypes.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+/* 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 <emmintrin.h>
+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
+++ /dev/null
-#pragma once
-
-#include <inttypes.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"
#endif
#include <string.h>
-#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
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
#endif
#include <string.h>
-#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"
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)
}
#endif
#include <string.h>
-#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);
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
#endif
#include <string.h>
-#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"
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)
}
#endif
#include <string.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_MD5.h"
void Hacl_Hash_MD5_init(uint32_t *s);
#endif
#include <string.h>
-#include "krml/types.h"
+#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"
#endif
#include <string.h>
-#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
#endif
#include <string.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_SHA3.h"
extern const uint32_t Hacl_Hash_SHA3_keccak_rotc[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,
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
#endif
#include <string.h>
-#include "krml/types.h"
+#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"
--- /dev/null
+/* 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 <string.h>
+#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
#include <sys/types.h>
+#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. */
#endif
#endif
+#endif // HACL_INTRINSICS_SHIMMED
+
#endif // __Vec_Intrin_H
# 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")"
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
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
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 <<EOF
-#pragma once
-
-#include <inttypes.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
$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 <string.h>\n!#include <string.h>\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 <string.h>!#include <string.h>\n#include "python_hacl_namespaces.h"!' Hacl_Hash_*.h
# Step 3: trim whitespace (for the linter)
<ItemDefinitionGroup>
<ClCompile>
<AdditionalOptions>/Zm200 %(AdditionalOptions)</AdditionalOptions>
- <AdditionalIncludeDirectories>$(PySourcePath)Modules\_hacl\include;$(PySourcePath)Modules\_hacl\internal;$(PySourcePath)Python;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
+ <AdditionalIncludeDirectories>$(PySourcePath)Modules\_hacl;$(PySourcePath)Modules\_hacl\include;$(PySourcePath)Python;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
<AdditionalIncludeDirectories Condition="$(IncludeExternals)">$(zlibDir);%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
<PreprocessorDefinitions>_USRDLL;Py_BUILD_CORE;Py_BUILD_CORE_BUILTIN;Py_ENABLE_SHARED;MS_DLL_ID="$(SysWinVer)";%(PreprocessorDefinitions)</PreprocessorDefinitions>
<PreprocessorDefinitions Condition="$(IncludeExternals)">_Py_HAVE_ZLIB;%(PreprocessorDefinitions)</PreprocessorDefinitions>
projects / thirdparty / Python / cpython.git / commitdiff
