mirrors/cpython
1
0
Fork 0
mirror of https://github.com/python/cpython.git synced 2025-07-07 19:35:27 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 8

gh-130213: update hacl_star_rev to 322f6d58290e0ed7f4ecb84fcce12917aa0f594b (GH-130960)

Browse source 
Updates the HACL* implementation used by hashlib from upstream sources.
This commit is contained in:
Chris Eibl 2025-03-15 18:42:27 +01:00 • committed by GitHub
parent 7ae9c5dd25
commit 0ce056d265
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
40 changed files with 2899 additions and 1072 deletions
Download patch file Download diff file Expand all files Collapse all files

4
Makefile.pre.in
View file

@ -669,9 +669,10 @@ LIBHACL_HEADERS= \
Modules/_hacl/include/krml/FStar_UInt128_Verified.h \
Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h \
Modules/_hacl/include/krml/fstar_uint128_struct_endianness.h \
Modules/_hacl/include/krml/internal/compat.h \
Modules/_hacl/include/krml/internal/target.h \
Modules/_hacl/include/krml/internal/types.h \
Modules/_hacl/include/krml/lowstar_endianness.h \
Modules/_hacl/include/krml/types.h \
Modules/_hacl/Hacl_Streaming_Types.h \
Modules/_hacl/python_hacl_namespaces.h
@ -690,6 +691,7 @@ LIBHACL_BLAKE2_HEADERS= \
Modules/_hacl/internal/Hacl_Impl_Blake2_Constants.h \
Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h \
Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h \
Modules/_hacl/internal/Hacl_Streaming_Types.h \
$(LIBHACL_HEADERS)
#########################################################################

2
Misc/NEWS.d/next/Build/2025-03-11-19-06-50.gh-issue-130213._eQr0g.rst Normal file
View file

@ -0,0 +1,2 @@
Update the vendored HACL* library to fix build issues with older clang
compilers.

202
Misc/sbom.spdx.json generated
View file

@ -300,11 +300,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "1cd3cda98e0e6882a13a59268b88640c542350fd"
"checksumValue": "4b6e7696e8d84f322fb24b1fbb08ccb9b0e7d51b"
},
{
"algorithm": "SHA256",
"checksumValue": "41a420bc9355e451720e60e9536e66f04dc6e416ca9217c4ab18d827887a2e08"
"checksumValue": "50a65a34a7a7569eedf7fa864a7892eeee5840a7fdf6fa8f1e87d42c65f6c877"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2b.c"
@ -314,11 +314,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "b0b3ae92d6aee7b52bacfdf02409d8d7e23701ee"
"checksumValue": "7c66ac004a1dcf3fee0ab9aa62d61972f029de3a"
},
{
"algorithm": "SHA256",
"checksumValue": "95d1dd4097a706b0719610da674297fa253b30d03a6ead4685ed648e20cb51a2"
"checksumValue": "9a7239a01a4ee8defbe3ebd9f0d12c873a1dd8e0659070380b2eab3ab0177333"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2b.h"
@ -328,11 +328,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "0ceef306590ec12251db03a31fc08ecba697486d"
"checksumValue": "0f75e44a42775247a46acc2beaa6bae8f199a3d9"
},
{
"algorithm": "SHA256",
"checksumValue": "1575a23b21319e55e670f74194fc2dfd1777eb5a3816cad43750e03da6e44db9"
"checksumValue": "03b612c24193464ed6848aeebbf44f9266b78ec6eed2486056211cde8992c49a"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2b_Simd256.c"
@ -342,11 +342,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "a5011646670c4f51368aca661e458e4c7f1d88e0"
"checksumValue": "7f273d26942233e5dcdfb4c1a16ff2486b15f899"
},
{
"algorithm": "SHA256",
"checksumValue": "f00c1fe8e774c7ec65f6c5a8efa43ce180a17fc80ed6119ada8c4022d058b6e2"
"checksumValue": "dbc0dacc68ed52dbf1b7d6fba2c87870317998bc046e65f6deaaa150625432f8"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2b_Simd256.h"
@ -370,11 +370,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "9616a9f8d795d64487bf86a96719f943729621e2"
"checksumValue": "65bf44140691b046dcfed3ab1576dbf8bbf96dc5"
},
{
"algorithm": "SHA256",
"checksumValue": "5ecde5ddc8ec073cffe64d60e868535d995f33fb0f87f9b50e68bd2a694b7434"
"checksumValue": "0f98959dafffce039ade9d296f7a05bed151c9c512498f48e4b326a5523a240b"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2s.c"
@ -384,11 +384,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "0328172a62507a051cd60ff9603710ed5aea1bc8"
"checksumValue": "2120c8c467aeebcc7c8b9678c15e79648433b91a"
},
{
"algorithm": "SHA256",
"checksumValue": "9f3c8ef615c9fbc59ef796d0ad2a7a76a7e55dc8939077b44ca538cbf8889a8c"
"checksumValue": "45735f7fe2dbbad7656d07854e9ec8176ad26c79f90dcc0fec0b9a59a6311ba7"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2s.h"
@ -398,11 +398,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "5b950ce0a5c8f0c2c56b4ac96e1943b504255d45"
"checksumValue": "0da9782455923aede8d8dce9dfdc38f4fc1de572"
},
{
"algorithm": "SHA256",
"checksumValue": "5a5f5d8e376dc30d89fd6c6c435157fe9ffa5308030e7abb1256afaee0765536"
"checksumValue": "2d17ae768fd3d7d6decddd8b4aaf23ce02a809ee62bb98da32c8a7f54acf92d0"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2s_Simd128.c"
@ -412,11 +412,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "32f35c173c10a2c49ac53c839cfbccd8a147274d"
"checksumValue": "9028e24c9876d9d16b2435ec29240c6b57bfe2a0"
},
{
"algorithm": "SHA256",
"checksumValue": "8734879b551f0fa860002ae81c0d0cfbade561007d9c26ad18c5a221e239237e"
"checksumValue": "062e3b856acac4f929c1e04b8264a754cad21ca6580215f7094a3f0a04edb912"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_Blake2s_Simd128.h"
@ -440,11 +440,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "f8ba39b46ebdfa7d031d9c33130c6ded680a8120"
"checksumValue": "38e8d96ef1879480780494058a93cec181f8d6d7"
},
{
"algorithm": "SHA256",
"checksumValue": "f71cf6a0e8f09354c2af2c785a1d36e0cba7613a589be01ca8a3d8478f4c8874"
"checksumValue": "61e77d2063cf60c96e9ce06af215efe5d42c43026833bffed5732326fe97ed1e"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_MD5.c"
@ -454,11 +454,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "eaaab54cea2b0bb8ec0eedf0b373d42f1a0f8f6c"
"checksumValue": "e67a9bc18358c57afaeff3a174893ddfdb52dfc6"
},
{
"algorithm": "SHA256",
"checksumValue": "9a02e2a6e163515ea0228a859d5e55c1f57b11fae5908c42f9f9814ce9bca230"
"checksumValue": "16e982081f6c2fd03ea751fcc64f5a835c94652841836e231fe562b9e287f4bc"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_MD5.h"
@ -468,11 +468,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "f4f42faf8da78a230199f649c0f2a1b865799a31"
"checksumValue": "986dd5ba0b34d15f3e5e5c656979aea1b502e8aa"
},
{
"algorithm": "SHA256",
"checksumValue": "5b29bd9951646861e0e19427be5d923a5bab7a4516824ccc068f696469195eec"
"checksumValue": "38d5f1f2e67a0eb30789f81fc56c07a6e7246e2b1be6c65485bcca1dcd0e0806"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA1.c"
@ -482,11 +482,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "722b57139737ceeb88e41d3839e6f7d70578741b"
"checksumValue": "f1ca21f1ee8b15ad9ccfbda72165b9d86912166c"
},
{
"algorithm": "SHA256",
"checksumValue": "5640295c790d56b1b4df147d6a6c58803b1845cd7d93365bf7cc7b75ba3cacd5"
"checksumValue": "4b2ad9ea93fdd9c2fdc521fc4e14e02550666c2717a23b85819db2e07ea555f3"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA1.h"
@ -496,11 +496,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "b0aa8810339adb09623ffa429246b4324fac4565"
"checksumValue": "f732a6710fe3e13cd28130f0f20504e347d1c412"
},
{
"algorithm": "SHA256",
"checksumValue": "2288f8f860efe80eed4f1e14ef570079b7459aeb41f87e94e691d7cf5e0e7adb"
"checksumValue": "86cf32e4d1f3ba93a94108271923fdafe2204447792a918acf4a2250f352dbde"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA2.c"
@ -510,11 +510,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "4903e10291d07367be3bc283935bc52926e57ba1"
"checksumValue": "f38cebeeca40a83aeb2cf5dfce578ffefe176d84"
},
{
"algorithm": "SHA256",
"checksumValue": "093d7693084af0999d2a13d207311d74b5bdfdc9c08447ed4a979e3f7505ae6b"
"checksumValue": "ee03bf9368d1a3a3c70cfd4e9391b2485466404db4a60bfc5319630cc314b590"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA2.h"
@ -524,11 +524,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "ef374b9d0951ebb38006af944dd4b38a6cf3abb2"
"checksumValue": "50f75337b31f509b5bfcc7ebb3d066b82a0f1b33"
},
{
"algorithm": "SHA256",
"checksumValue": "164df19f229143006c5f9a3c0bd771415f152bfbc7efb61c337fa0f903003eb3"
"checksumValue": "c9e1442899e5b902fa39f413f1a3131f7ab5c2283d5100dc8ac675a7d5ebbdf1"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA3.c"
@ -538,11 +538,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "7d78e6844dde1f9b5e68f58ca105a4c330461ff6"
"checksumValue": "01717207aef77174e328186d48c27517f6644c15"
},
{
"algorithm": "SHA256",
"checksumValue": "231d9bc13190be4b6821acb518194f32f4a3c04f1c034b3118f6db0bab2debe3"
"checksumValue": "620dded172e94cb3f25f9904b44977d91f2cc9573e41b38f19e929d083ae0308"
}
],
"fileName": "Modules/_hacl/Hacl_Hash_SHA3.h"
@ -552,11 +552,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "ab7b4d9465a2765a07f8d5bccace7182b28ed1b8"
"checksumValue": "372448599774a98e5c5d083e91f301ed1c4b822e"
},
{
"algorithm": "SHA256",
"checksumValue": "26913613f3b4f8ffff0a3e211a5ebc849159094e5e11de0a31fcb95b6105b74c"
"checksumValue": "95d8e70ca4bc6aa98f6d2435ceb6410ead299b1f700fae1f5c603ec3f57ea551"
}
],
"fileName": "Modules/_hacl/Hacl_Streaming_Types.h"
@ -566,11 +566,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "118dc712780ea680affa8d9794470440eb87ff10"
"checksumValue": "80dae56879ed9bace476362ef251de48ce055a20"
},
{
"algorithm": "SHA256",
"checksumValue": "b017e7d5662a308c938cf4e4b919680c8f3e27f42975ca152b62fe65c5f7fb0c"
"checksumValue": "da84b6287e9aa1fc52e819a8ca10e79b51263f1dda6b4528ed8c0c74a11fb0ea"
}
],
"fileName": "Modules/_hacl/Lib_Memzero0.c"
@ -580,11 +580,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "7665829b9396f72e7f8098080d6d6773565468e9"
"checksumValue": "eaa543c778300238dc23034aafeada0951154af1"
},
{
"algorithm": "SHA256",
"checksumValue": "ca7357ee70365c690664a44f6522e526636151d9ed2da8d0d29da15bb8556530"
"checksumValue": "3fd2552d527a23110d61ad2811c774810efb1eaee008f136c2a0d609daa77f5b"
}
],
"fileName": "Modules/_hacl/include/krml/FStar_UInt128_Verified.h"
@ -594,11 +594,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "a2db924d0e8f7df3139e9a20355ffa520aded479"
"checksumValue": "41ee1e34ede7ef5b24b87d4ca816fd6d9fac8010"
},
{
"algorithm": "SHA256",
"checksumValue": "f1de79fb4c763b215c823f44471bbae6b65e6bb533eb52a5863d551d5e2e6748"
"checksumValue": "d48ed03e504cb87793a310a9552fb3ba2ebd6fe90127b7d642c8740fba1b9748"
}
],
"fileName": "Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h"
@ -617,20 +617,48 @@
],
"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-internal-types.h",
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "3f66313d16891f43b21c1a736081c2c6d46bf370"
},
{
"algorithm": "SHA256",
"checksumValue": "78e9bff9124968108e1699e1c6388e3d4ec9bd72dd8adff49734a69ab380ee5c"
}
],
"fileName": "Modules/_hacl/include/krml/internal/types.h"
},
{
"SPDXID": "SPDXRef-FILE-Modules-hacl-include-krml-lowstar-endianness.h",
"checksums": [
@ -645,30 +673,16 @@
],
"fileName": "Modules/_hacl/include/krml/lowstar_endianness.h"
},
{
"SPDXID": "SPDXRef-FILE-Modules-hacl-include-krml-types.h",
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "df8e0ed74a5970d09d3cc4c6e7c6c7a4c4e5015c"
},
{
"algorithm": "SHA256",
"checksumValue": "de7444c345caa4c47902c4380500356a3ee7e199d2aab84fd8c4960410154f3d"
}
],
"fileName": "Modules/_hacl/include/krml/types.h"
},
{
"SPDXID": "SPDXRef-FILE-Modules-hacl-internal-Hacl-Hash-Blake2b.h",
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "31b329bd39ff72ed25086e2afe7875949003c140"
"checksumValue": "0741cb8497309d648428be1e7b5944b1fc167187"
},
{
"algorithm": "SHA256",
"checksumValue": "16df6cf240ee99aade0fd11d5cc7573c201c7589d8325a5c95c7670c531e1518"
"checksumValue": "f9b923a566d62de047c753637143d439ca1c25221c08352ddc1738ff4a6ac721"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2b.h"
@ -678,11 +692,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "3f4fdfdaef97a2cbac5ec091c91ede18d4b33f92"
"checksumValue": "878ae284c93824b80b1763e8b3e6be3c410777a8"
},
{
"algorithm": "SHA256",
"checksumValue": "96b1c77860f12bcadad0caca77a5a1649a840ad9989d97984a3b51bb98c80e2f"
"checksumValue": "49df6223f6403daf503a1af1a3d2f943d30b5889fe7ed20299c3df24c1e3853d"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h"
@ -692,11 +706,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "9efd61f6ba8d126e98abd83679a5ed5954278c31"
"checksumValue": "25552d8cbf8aa345907635b38f284eec9075301e"
},
{
"algorithm": "SHA256",
"checksumValue": "143f58f033786173501a72ac302e435963fdce6c2cc38eef6d6adeb3cdc1bb9c"
"checksumValue": "a3424cf4c5518654908086bbbf5d465715ec3b23625ef0cadc29492d1f90366c"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2s.h"
@ -706,11 +720,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "3f984829465285283b03b1111b4918cfb48b8031"
"checksumValue": "54a712fc3ed5a817288351cbac5b7d9afa7e379f"
},
{
"algorithm": "SHA256",
"checksumValue": "cd24038fdd617edc65e472496b0d58f23ff312f81f9244c3e7893fdc9a1b2977"
"checksumValue": "c6abae648b8a1e9d5631c0a959620cad1f7e92ce522e07c3416199fe51debef6"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h"
@ -720,11 +734,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "60f02d21f045c8a4c2b6b84a8f7e023d9490c8e5"
"checksumValue": "c15c5f83bbb9f62611c49f0f8f723eaab1a27488"
},
{
"algorithm": "SHA256",
"checksumValue": "370d8ef9c48cb55472ece11e12eaf94c58118de3f5515b6df1c130b696597828"
"checksumValue": "95cd5d91c4a9217901d0b3395dcd8881e62e2055d723b532ec5176386a636d22"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_MD5.h"
@ -734,11 +748,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "6346c30a140e7d3010c98fe19d14fa229a54eb16"
"checksumValue": "7b8717e3a24e7e16a34b251d0d02da6f68439695"
},
{
"algorithm": "SHA256",
"checksumValue": "ab52c6092bdbbfc9884f841bf4824016792ffa96167577cbe0df00dd96f56a34"
"checksumValue": "9473d8bc9506fe0053d7d98c225d4873011329863f1c4a8e93e43fc71bd1f314"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_SHA1.h"
@ -748,11 +762,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "2e9ae174142fc491f20567ab8b5c08cef9b07cfe"
"checksumValue": "e319c949f5a2dd765be2c8c7ff77bfe52ee6c7da"
},
{
"algorithm": "SHA256",
"checksumValue": "07100964adcf4b5f8bd4773e25f475b34cd180b90df8b1c0052e55c008b7cc49"
"checksumValue": "75261448e51c3eb1ba441e973b193e23570b167f67743942ee2ee57417491c9f"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_SHA2.h"
@ -762,11 +776,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "39ba6e8959e44ae956a640d3a1fb3ef60de8a9e5"
"checksumValue": "dbd92415c31606804102b79d5ba3d1752fe03887"
},
{
"algorithm": "SHA256",
"checksumValue": "dbf4b86a04b4d8716976f8c023cccbfe174435dbec3bc00fc1f066fb52c4e341"
"checksumValue": "5d74a76a0ac3659a1ae1276c3ca55521f09e83d2f0039f5c519a76f8f3c76a8e"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Hash_SHA3.h"
@ -776,15 +790,29 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "c3ae35ed5bf70cf011b2732df011231528b9111c"
"checksumValue": "ad788265f8e1b078c4d1cb6e90b8c031590e6baf"
},
{
"algorithm": "SHA256",
"checksumValue": "c381fea7b8b505a7c7ce27231a36751add6b184b204132935c5faaba4fce8ba1"
"checksumValue": "d8354a9b75e2470085fa7e538493130e81fa23a804a6a69d34da8fdcc941c038"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Impl_Blake2_Constants.h"
},
{
"SPDXID": "SPDXRef-FILE-Modules-hacl-internal-Hacl-Streaming-Types.h",
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "4e6b098e89fd447bd03f47b55208208456b20966"
},
{
"algorithm": "SHA256",
"checksumValue": "d54d947968ca125978d61fea844711b990f0a18ab0fbca87e41029004d9d04b6"
}
],
"fileName": "Modules/_hacl/internal/Hacl_Streaming_Types.h"
},
{
"SPDXID": "SPDXRef-FILE-Modules-hacl-lib-memzero0.h",
"checksums": [
@ -804,11 +832,11 @@
"checksums": [
{
"algorithm": "SHA1",
"checksumValue": "f4a33ad535768b860362ab0bd033a70da0b524b7"
"checksumValue": "63e47cc290c4ec887dca708000876ac37ee75ba0"
},
{
"algorithm": "SHA256",
"checksumValue": "433cdf4ba80bc72e0cea5d4b420ff18676baeafdb5ba19adf5b7fb33e90b424b"
"checksumValue": "d09a6196d65c2645974100eb922002bd387d3ae13f2653780f82ed97a79af635"
}
],
"fileName": "Modules/_hacl/libintvector.h"
@ -1640,14 +1668,14 @@
"checksums": [
{
"algorithm": "SHA256",
"checksumValue": "40de5297b032d2676fc0039049b4e8dab1f2730eebb5ecff6a40c04fa0356339"
"checksumValue": "502a0250fa08d2cbcc8b9e43831235a2c075de2eb180e7381ecb5d10b181971e"
}
],
"downloadLocation": "https://github.com/hacl-star/hacl-star/archive/f218923ef2417d963d7efc7951593ae6aef613f7.zip",
"downloadLocation": "https://github.com/hacl-star/hacl-star/archive/322f6d58290e0ed7f4ecb84fcce12917aa0f594b.zip",
"externalRefs": [
{
"referenceCategory": "SECURITY",
"referenceLocator": "cpe:2.3:a:hacl-star:hacl-star:f218923ef2417d963d7efc7951593ae6aef613f7:*:*:*:*:*:*:*",
"referenceLocator": "cpe:2.3:a:hacl-star:hacl-star:322f6d58290e0ed7f4ecb84fcce12917aa0f594b:*:*:*:*:*:*:*",
"referenceType": "cpe23Type"
}
],
@ -1655,7 +1683,7 @@
"name": "hacl-star",
"originator": "Organization: HACL* Developers",
"primaryPackagePurpose": "SOURCE",
"versionInfo": "f218923ef2417d963d7efc7951593ae6aef613f7"
"versionInfo": "322f6d58290e0ed7f4ecb84fcce12917aa0f594b"
},
{
"SPDXID": "SPDXRef-PACKAGE-macholib",
@ -1923,18 +1951,23 @@
"relationshipType": "CONTAINS",
"spdxElementId": "SPDXRef-PACKAGE-hacl-star"
},
{
"relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-internal-compat.h",
"relationshipType": "CONTAINS",
"spdxElementId": "SPDXRef-PACKAGE-hacl-star"
},
{
"relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-internal-target.h",
"relationshipType": "CONTAINS",
"spdxElementId": "SPDXRef-PACKAGE-hacl-star"
},
{
"relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-lowstar-endianness.h",
"relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-internal-types.h",
"relationshipType": "CONTAINS",
"spdxElementId": "SPDXRef-PACKAGE-hacl-star"
},
{
"relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-types.h",
"relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-include-krml-lowstar-endianness.h",
"relationshipType": "CONTAINS",
"spdxElementId": "SPDXRef-PACKAGE-hacl-star"
},
@ -1983,6 +2016,11 @@
"relationshipType": "CONTAINS",
"spdxElementId": "SPDXRef-PACKAGE-hacl-star"
},
{
"relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-internal-Hacl-Streaming-Types.h",
"relationshipType": "CONTAINS",
"spdxElementId": "SPDXRef-PACKAGE-hacl-star"
},
{
"relatedSpdxElement": "SPDXRef-FILE-Modules-hacl-lib-memzero0.h",
"relationshipType": "CONTAINS",

435
Modules/_hacl/Hacl_Hash_Blake2b.c
View file

@ -25,6 +25,9 @@
#include "internal/Hacl_Hash_Blake2b.h"
#include "Hacl_Streaming_Types.h"
#include "internal/Hacl_Streaming_Types.h"
#include "internal/Hacl_Impl_Blake2_Constants.h"
#include "lib_memzero0.h"
@ -697,127 +700,215 @@ void Hacl_Hash_Blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash)
Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
}
typedef struct option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t____s
{
Hacl_Streaming_Types_optional tag;
Hacl_Hash_Blake2b_block_state_t v;
}
option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___;
static Hacl_Hash_Blake2b_state_t
*malloc_raw(Hacl_Hash_Blake2b_index kk, Hacl_Hash_Blake2b_params_and_key key)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t));
uint64_t *wv = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t));
uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t));
Hacl_Hash_Blake2b_block_state_t
block_state =
{
.fst = kk.key_length,
.snd = kk.digest_length,
.thd = kk.last_node,
.f3 = { .fst = wv, .snd = b }
};
uint8_t kk10 = kk.key_length;
uint32_t ite;
if (kk10 != 0U)
if (buf == NULL)
{
ite = 128U;
return NULL;
}
uint8_t *buf1 = buf;
uint64_t *wv0 = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t));
option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___ block_state;
if (wv0 == NULL)
{
block_state =
(
(option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
ite = 0U;
uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t));
if (b == NULL)
{
KRML_HOST_FREE(wv0);
block_state =
(
(option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
block_state =
(
(option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){
.tag = Hacl_Streaming_Types_Some,
.v = {
.fst = kk.key_length,
.snd = kk.digest_length,
.thd = kk.last_node,
.f3 = { .fst = wv0, .snd = b }
}
}
);
}
}
Hacl_Hash_Blake2b_state_t
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)ite };
Hacl_Hash_Blake2b_state_t
*p = (Hacl_Hash_Blake2b_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2b_state_t));
p[0U] = s;
Hacl_Hash_Blake2b_blake2_params *p1 = key.fst;
uint8_t kk1 = p1->key_length;
uint8_t nn = p1->digest_length;
bool last_node = block_state.thd;
Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
uint64_t *h = block_state.f3.snd;
uint32_t kk20 = (uint32_t)i.key_length;
uint8_t *k_1 = key.snd;
if (!(kk20 == 0U))
if (block_state.tag == Hacl_Streaming_Types_None)
{
uint8_t *sub_b = buf + kk20;
memset(sub_b, 0U, (128U - kk20) * sizeof (uint8_t));
memcpy(buf, k_1, kk20 * sizeof (uint8_t));
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_Blake2b_blake2_params pv = p1[0U];
uint64_t tmp[8U] = { 0U };
uint64_t *r0 = h;
uint64_t *r1 = h + 4U;
uint64_t *r2 = h + 8U;
uint64_t *r3 = h + 12U;
uint64_t iv0 = Hacl_Hash_Blake2b_ivTable_B[0U];
uint64_t iv1 = Hacl_Hash_Blake2b_ivTable_B[1U];
uint64_t iv2 = Hacl_Hash_Blake2b_ivTable_B[2U];
uint64_t iv3 = Hacl_Hash_Blake2b_ivTable_B[3U];
uint64_t iv4 = Hacl_Hash_Blake2b_ivTable_B[4U];
uint64_t iv5 = Hacl_Hash_Blake2b_ivTable_B[5U];
uint64_t iv6 = Hacl_Hash_Blake2b_ivTable_B[6U];
uint64_t iv7 = Hacl_Hash_Blake2b_ivTable_B[7U];
r2[0U] = iv0;
r2[1U] = iv1;
r2[2U] = iv2;
r2[3U] = iv3;
r3[0U] = iv4;
r3[1U] = iv5;
r3[2U] = iv6;
r3[3U] = iv7;
uint8_t kk2 = pv.key_length;
uint8_t nn1 = pv.digest_length;
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint64_t *os = tmp + 4U;
uint8_t *bj = pv.salt + i0 * 8U;
uint64_t u = load64_le(bj);
uint64_t r4 = u;
uint64_t x = r4;
os[i0] = x;);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint64_t *os = tmp + 6U;
uint8_t *bj = pv.personal + i0 * 8U;
uint64_t u = load64_le(bj);
uint64_t r4 = u;
uint64_t x = r4;
os[i0] = x;);
tmp[0U] =
(uint64_t)nn1
^
((uint64_t)kk2
<< 8U
^ ((uint64_t)pv.fanout << 16U ^ ((uint64_t)pv.depth << 24U ^ (uint64_t)pv.leaf_length << 32U)));
tmp[1U] = pv.node_offset;
tmp[2U] = (uint64_t)pv.node_depth ^ (uint64_t)pv.inner_length << 8U;
tmp[3U] = 0ULL;
uint64_t tmp0 = tmp[0U];
uint64_t tmp1 = tmp[1U];
uint64_t tmp2 = tmp[2U];
uint64_t tmp3 = tmp[3U];
uint64_t tmp4 = tmp[4U];
uint64_t tmp5 = tmp[5U];
uint64_t tmp6 = tmp[6U];
uint64_t tmp7 = tmp[7U];
uint64_t iv0_ = iv0 ^ tmp0;
uint64_t iv1_ = iv1 ^ tmp1;
uint64_t iv2_ = iv2 ^ tmp2;
uint64_t iv3_ = iv3 ^ tmp3;
uint64_t iv4_ = iv4 ^ tmp4;
uint64_t iv5_ = iv5 ^ tmp5;
uint64_t iv6_ = iv6 ^ tmp6;
uint64_t iv7_ = iv7 ^ tmp7;
r0[0U] = iv0_;
r0[1U] = iv1_;
r0[2U] = iv2_;
r0[3U] = iv3_;
r1[0U] = iv4_;
r1[1U] = iv5_;
r1[2U] = iv6_;
r1[3U] = iv7_;
return p;
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_Blake2b_block_state_t block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
uint8_t kk10 = kk.key_length;
uint32_t ite;
if (kk10 != 0U)
{
ite = 128U;
}
else
{
ite = 0U;
}
Hacl_Hash_Blake2b_state_t
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)ite };
Hacl_Hash_Blake2b_state_t
*p = (Hacl_Hash_Blake2b_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2b_state_t));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
uint64_t *b = block_state1.f3.snd;
uint64_t *wv = block_state1.f3.fst;
KRML_HOST_FREE(wv);
KRML_HOST_FREE(b);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_Blake2b_blake2_params *p1 = key.fst;
uint8_t kk1 = p1->key_length;
uint8_t nn = p1->digest_length;
bool last_node = block_state1.thd;
Hacl_Hash_Blake2b_index
i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
uint64_t *h = block_state1.f3.snd;
uint32_t kk20 = (uint32_t)i.key_length;
uint8_t *k_2 = key.snd;
if (!(kk20 == 0U))
{
uint8_t *sub_b = buf1 + kk20;
memset(sub_b, 0U, (128U - kk20) * sizeof (uint8_t));
memcpy(buf1, k_2, kk20 * sizeof (uint8_t));
}
Hacl_Hash_Blake2b_blake2_params pv = p1[0U];
uint64_t tmp[8U] = { 0U };
uint64_t *r0 = h;
uint64_t *r1 = h + 4U;
uint64_t *r2 = h + 8U;
uint64_t *r3 = h + 12U;
uint64_t iv0 = Hacl_Hash_Blake2b_ivTable_B[0U];
uint64_t iv1 = Hacl_Hash_Blake2b_ivTable_B[1U];
uint64_t iv2 = Hacl_Hash_Blake2b_ivTable_B[2U];
uint64_t iv3 = Hacl_Hash_Blake2b_ivTable_B[3U];
uint64_t iv4 = Hacl_Hash_Blake2b_ivTable_B[4U];
uint64_t iv5 = Hacl_Hash_Blake2b_ivTable_B[5U];
uint64_t iv6 = Hacl_Hash_Blake2b_ivTable_B[6U];
uint64_t iv7 = Hacl_Hash_Blake2b_ivTable_B[7U];
r2[0U] = iv0;
r2[1U] = iv1;
r2[2U] = iv2;
r2[3U] = iv3;
r3[0U] = iv4;
r3[1U] = iv5;
r3[2U] = iv6;
r3[3U] = iv7;
uint8_t kk2 = pv.key_length;
uint8_t nn1 = pv.digest_length;
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint64_t *os = tmp + 4U;
uint8_t *bj = pv.salt + i0 * 8U;
uint64_t u = load64_le(bj);
uint64_t r4 = u;
uint64_t x = r4;
os[i0] = x;);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint64_t *os = tmp + 6U;
uint8_t *bj = pv.personal + i0 * 8U;
uint64_t u = load64_le(bj);
uint64_t r4 = u;
uint64_t x = r4;
os[i0] = x;);
tmp[0U] =
(uint64_t)nn1
^
((uint64_t)kk2
<< 8U
^
((uint64_t)pv.fanout
<< 16U
^ ((uint64_t)pv.depth << 24U ^ (uint64_t)pv.leaf_length << 32U)));
tmp[1U] = pv.node_offset;
tmp[2U] = (uint64_t)pv.node_depth ^ (uint64_t)pv.inner_length << 8U;
tmp[3U] = 0ULL;
uint64_t tmp0 = tmp[0U];
uint64_t tmp1 = tmp[1U];
uint64_t tmp2 = tmp[2U];
uint64_t tmp3 = tmp[3U];
uint64_t tmp4 = tmp[4U];
uint64_t tmp5 = tmp[5U];
uint64_t tmp6 = tmp[6U];
uint64_t tmp7 = tmp[7U];
uint64_t iv0_ = iv0 ^ tmp0;
uint64_t iv1_ = iv1 ^ tmp1;
uint64_t iv2_ = iv2 ^ tmp2;
uint64_t iv3_ = iv3 ^ tmp3;
uint64_t iv4_ = iv4 ^ tmp4;
uint64_t iv5_ = iv5 ^ tmp5;
uint64_t iv6_ = iv6 ^ tmp6;
uint64_t iv7_ = iv7 ^ tmp7;
r0[0U] = iv0_;
r0[1U] = iv1_;
r0[2U] = iv2_;
r0[3U] = iv3_;
r1[0U] = iv4_;
r1[1U] = iv5_;
r1[2U] = iv6_;
r1[3U] = iv7_;
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**
@ -1137,7 +1228,7 @@ Hacl_Hash_Blake2b_update(Hacl_Hash_Blake2b_state_t *state, uint8_t *chunk, uint3
if (!(sz1 == 0U))
{
uint64_t prevlen = total_len1 - (uint64_t)sz1;
K____uint64_t___uint64_t_ acc = block_state1.f3;
Hacl_Streaming_Types_two_pointers acc = block_state1.f3;
uint64_t *wv = acc.fst;
uint64_t *hash = acc.snd;
uint32_t nb = 1U;
@ -1162,7 +1253,7 @@ Hacl_Hash_Blake2b_update(Hacl_Hash_Blake2b_state_t *state, uint8_t *chunk, uint3
uint32_t data2_len = chunk_len - data1_len;
uint8_t *data1 = chunk;
uint8_t *data2 = chunk + data1_len;
K____uint64_t___uint64_t_ acc = block_state1.f3;
Hacl_Streaming_Types_two_pointers acc = block_state1.f3;
uint64_t *wv = acc.fst;
uint64_t *hash = acc.snd;
uint32_t nb = data1_len / 128U;
@ -1230,7 +1321,7 @@ Hacl_Hash_Blake2b_update(Hacl_Hash_Blake2b_state_t *state, uint8_t *chunk, uint3
if (!(sz1 == 0U))
{
uint64_t prevlen = total_len1 - (uint64_t)sz1;
K____uint64_t___uint64_t_ acc = block_state1.f3;
Hacl_Streaming_Types_two_pointers acc = block_state1.f3;
uint64_t *wv = acc.fst;
uint64_t *hash = acc.snd;
uint32_t nb = 1U;
@ -1256,7 +1347,7 @@ Hacl_Hash_Blake2b_update(Hacl_Hash_Blake2b_state_t *state, uint8_t *chunk, uint3
uint32_t data2_len = chunk_len - diff - data1_len;
uint8_t *data1 = chunk2;
uint8_t *data2 = chunk2 + data1_len;
K____uint64_t___uint64_t_ acc = block_state1.f3;
Hacl_Streaming_Types_two_pointers acc = block_state1.f3;
uint64_t *wv = acc.fst;
uint64_t *hash = acc.snd;
uint32_t nb = data1_len / 128U;
@ -1339,7 +1430,7 @@ uint8_t Hacl_Hash_Blake2b_digest(Hacl_Hash_Blake2b_state_t *s, uint8_t *dst)
}
uint8_t *buf_last = buf_1 + r - ite;
uint8_t *buf_multi = buf_1;
K____uint64_t___uint64_t_ acc0 = tmp_block_state.f3;
Hacl_Streaming_Types_two_pointers acc0 = tmp_block_state.f3;
uint64_t *wv1 = acc0.fst;
uint64_t *hash0 = acc0.snd;
uint32_t nb = 0U;
@ -1350,7 +1441,7 @@ uint8_t Hacl_Hash_Blake2b_digest(Hacl_Hash_Blake2b_state_t *s, uint8_t *dst)
buf_multi,
nb);
uint64_t prev_len_last = total_len - (uint64_t)r;
K____uint64_t___uint64_t_ acc = tmp_block_state.f3;
Hacl_Streaming_Types_two_pointers acc = tmp_block_state.f3;
bool last_node1 = tmp_block_state.thd;
uint64_t *wv = acc.fst;
uint64_t *hash = acc.snd;
@ -1411,26 +1502,102 @@ Hacl_Hash_Blake2b_state_t *Hacl_Hash_Blake2b_copy(Hacl_Hash_Blake2b_state_t *sta
uint8_t kk1 = block_state0.fst;
Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
memcpy(buf, buf0, 128U * sizeof (uint8_t));
uint64_t *wv = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t));
uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t));
Hacl_Hash_Blake2b_block_state_t
block_state =
uint64_t *wv0 = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t));
option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___ block_state;
if (wv0 == NULL)
{
block_state =
(
(option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(16U, sizeof (uint64_t));
if (b == NULL)
{
.fst = i.key_length,
.snd = i.digest_length,
.thd = i.last_node,
.f3 = { .fst = wv, .snd = b }
};
uint64_t *src_b = block_state0.f3.snd;
uint64_t *dst_b = block_state.f3.snd;
memcpy(dst_b, src_b, 16U * sizeof (uint64_t));
Hacl_Hash_Blake2b_state_t
s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
Hacl_Hash_Blake2b_state_t
*p = (Hacl_Hash_Blake2b_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2b_state_t));
p[0U] = s;
return p;
KRML_HOST_FREE(wv0);
block_state =
(
(option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
block_state =
(
(option___uint8_t___uint8_t___bool_____uint64_t_____uint64_t___){
.tag = Hacl_Streaming_Types_Some,
.v = {
.fst = i.key_length,
.snd = i.digest_length,
.thd = i.last_node,
.f3 = { .fst = wv0, .snd = b }
}
}
);
}
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_Blake2b_block_state_t block_state1 = block_state.v;
uint64_t *src_b = block_state0.f3.snd;
uint64_t *dst_b = block_state1.f3.snd;
memcpy(dst_b, src_b, 16U * sizeof (uint64_t));
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Hash_Blake2b_state_t
s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 };
Hacl_Hash_Blake2b_state_t
*p = (Hacl_Hash_Blake2b_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2b_state_t));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
uint64_t *b = block_state1.f3.snd;
uint64_t *wv = block_state1.f3.fst;
KRML_HOST_FREE(wv);
KRML_HOST_FREE(b);
KRML_HOST_FREE(buf);
return NULL;
}
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**

27
Modules/_hacl/Hacl_Hash_Blake2b.h
View file

@ -32,13 +32,12 @@ extern "C" {
#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;
@ -72,29 +71,9 @@ Hacl_Hash_Blake2b_index;
#define HACL_HASH_BLAKE2B_PERSONAL_BYTES (16U)
typedef struct K____uint64_t___uint64_t__s
{
uint64_t *fst;
uint64_t *snd;
}
K____uint64_t___uint64_t_;
typedef struct Hacl_Hash_Blake2b_block_state_t_s Hacl_Hash_Blake2b_block_state_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_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

511
Modules/_hacl/Hacl_Hash_Blake2b_Simd256.c
View file

@ -25,6 +25,10 @@
#include "internal/Hacl_Hash_Blake2b_Simd256.h"
#include "Hacl_Streaming_Types.h"
#include "Hacl_Hash_Blake2b.h"
#include "internal/Hacl_Streaming_Types.h"
#include "internal/Hacl_Impl_Blake2_Constants.h"
#include "internal/Hacl_Hash_Blake2b.h"
#include "lib_memzero0.h"
@ -523,136 +527,268 @@ Hacl_Hash_Blake2b_Simd256_store_state256b_to_state32(
os[i] = x;);
}
Lib_IntVector_Intrinsics_vec256 *Hacl_Hash_Blake2b_Simd256_malloc_with_key(void)
Lib_IntVector_Intrinsics_vec256 *Hacl_Hash_Blake2b_Simd256_malloc_internal_state_with_key(void)
{
Lib_IntVector_Intrinsics_vec256
*buf =
(Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32,
sizeof (Lib_IntVector_Intrinsics_vec256) * 4U);
memset(buf, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
if (buf != NULL)
{
memset(buf, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
}
return buf;
}
void
Hacl_Hash_Blake2b_Simd256_update_multi_no_inline(
Lib_IntVector_Intrinsics_vec256 *s,
FStar_UInt128_uint128 ev,
uint8_t *blocks,
uint32_t n
)
{
KRML_PRE_ALIGN(32) Lib_IntVector_Intrinsics_vec256 wv[4U] KRML_POST_ALIGN(32) = { 0U };
Hacl_Hash_Blake2b_Simd256_update_multi(n * 128U, wv, s, ev, blocks, n);
}
void
Hacl_Hash_Blake2b_Simd256_update_last_no_inline(
Lib_IntVector_Intrinsics_vec256 *s,
FStar_UInt128_uint128 prev,
uint8_t *input,
uint32_t input_len
)
{
KRML_PRE_ALIGN(32) Lib_IntVector_Intrinsics_vec256 wv[4U] KRML_POST_ALIGN(32) = { 0U };
Hacl_Hash_Blake2b_Simd256_update_last(input_len, wv, s, false, prev, input_len, input);
}
void
Hacl_Hash_Blake2b_Simd256_copy_internal_state(
Lib_IntVector_Intrinsics_vec256 *src,
Lib_IntVector_Intrinsics_vec256 *dst
)
{
memcpy(dst, src, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
}
typedef struct
option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256____s
{
Hacl_Streaming_Types_optional tag;
Hacl_Hash_Blake2b_Simd256_block_state_t v;
}
option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___;
static Hacl_Hash_Blake2b_Simd256_state_t
*malloc_raw(Hacl_Hash_Blake2b_index kk, Hacl_Hash_Blake2b_params_and_key key)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t));
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 =
(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 (buf == NULL)
{
ite = 128U;
return NULL;
}
uint8_t *buf1 = buf;
Lib_IntVector_Intrinsics_vec256
*wv0 =
(Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32,
sizeof (Lib_IntVector_Intrinsics_vec256) * 4U);
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
{
ite = 0U;
Lib_IntVector_Intrinsics_vec256
*b =
(Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32,
sizeof (Lib_IntVector_Intrinsics_vec256) * 4U);
if (b != NULL)
{
memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
}
if (b == NULL)
{
KRML_ALIGNED_FREE(wv0);
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){
.tag = Hacl_Streaming_Types_Some,
.v = {
.fst = kk.key_length,
.snd = kk.digest_length,
.thd = kk.last_node,
.f3 = { .fst = wv0, .snd = b }
}
}
);
}
}
Hacl_Hash_Blake2b_Simd256_state_t
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)ite };
Hacl_Hash_Blake2b_Simd256_state_t
*p =
(Hacl_Hash_Blake2b_Simd256_state_t *)KRML_HOST_MALLOC(sizeof (
Hacl_Hash_Blake2b_Simd256_state_t
));
p[0U] = s;
Hacl_Hash_Blake2b_blake2_params *p1 = key.fst;
uint8_t kk1 = p1->key_length;
uint8_t nn = p1->digest_length;
bool last_node = block_state.thd;
Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
Lib_IntVector_Intrinsics_vec256 *h = block_state.f3.snd;
uint32_t kk20 = (uint32_t)i.key_length;
uint8_t *k_1 = key.snd;
if (!(kk20 == 0U))
if (block_state.tag == Hacl_Streaming_Types_None)
{
uint8_t *sub_b = buf + kk20;
memset(sub_b, 0U, (128U - kk20) * sizeof (uint8_t));
memcpy(buf, k_1, kk20 * sizeof (uint8_t));
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_Blake2b_blake2_params pv = p1[0U];
uint64_t tmp[8U] = { 0U };
Lib_IntVector_Intrinsics_vec256 *r0 = h;
Lib_IntVector_Intrinsics_vec256 *r1 = h + 1U;
Lib_IntVector_Intrinsics_vec256 *r2 = h + 2U;
Lib_IntVector_Intrinsics_vec256 *r3 = h + 3U;
uint64_t iv0 = Hacl_Hash_Blake2b_ivTable_B[0U];
uint64_t iv1 = Hacl_Hash_Blake2b_ivTable_B[1U];
uint64_t iv2 = Hacl_Hash_Blake2b_ivTable_B[2U];
uint64_t iv3 = Hacl_Hash_Blake2b_ivTable_B[3U];
uint64_t iv4 = Hacl_Hash_Blake2b_ivTable_B[4U];
uint64_t iv5 = Hacl_Hash_Blake2b_ivTable_B[5U];
uint64_t iv6 = Hacl_Hash_Blake2b_ivTable_B[6U];
uint64_t iv7 = Hacl_Hash_Blake2b_ivTable_B[7U];
r2[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0, iv1, iv2, iv3);
r3[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7);
uint8_t kk2 = pv.key_length;
uint8_t nn1 = pv.digest_length;
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint64_t *os = tmp + 4U;
uint8_t *bj = pv.salt + i0 * 8U;
uint64_t u = load64_le(bj);
uint64_t r4 = u;
uint64_t x = r4;
os[i0] = x;);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint64_t *os = tmp + 6U;
uint8_t *bj = pv.personal + i0 * 8U;
uint64_t u = load64_le(bj);
uint64_t r4 = u;
uint64_t x = r4;
os[i0] = x;);
tmp[0U] =
(uint64_t)nn1
^
((uint64_t)kk2
<< 8U
^ ((uint64_t)pv.fanout << 16U ^ ((uint64_t)pv.depth << 24U ^ (uint64_t)pv.leaf_length << 32U)));
tmp[1U] = pv.node_offset;
tmp[2U] = (uint64_t)pv.node_depth ^ (uint64_t)pv.inner_length << 8U;
tmp[3U] = 0ULL;
uint64_t tmp0 = tmp[0U];
uint64_t tmp1 = tmp[1U];
uint64_t tmp2 = tmp[2U];
uint64_t tmp3 = tmp[3U];
uint64_t tmp4 = tmp[4U];
uint64_t tmp5 = tmp[5U];
uint64_t tmp6 = tmp[6U];
uint64_t tmp7 = tmp[7U];
uint64_t iv0_ = iv0 ^ tmp0;
uint64_t iv1_ = iv1 ^ tmp1;
uint64_t iv2_ = iv2 ^ tmp2;
uint64_t iv3_ = iv3 ^ tmp3;
uint64_t iv4_ = iv4 ^ tmp4;
uint64_t iv5_ = iv5 ^ tmp5;
uint64_t iv6_ = iv6 ^ tmp6;
uint64_t iv7_ = iv7 ^ tmp7;
r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1_, iv2_, iv3_);
r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4_, iv5_, iv6_, iv7_);
return p;
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_Blake2b_Simd256_block_state_t block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
uint8_t kk10 = kk.key_length;
uint32_t ite;
if (kk10 != 0U)
{
ite = 128U;
}
else
{
ite = 0U;
}
Hacl_Hash_Blake2b_Simd256_state_t
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)ite };
Hacl_Hash_Blake2b_Simd256_state_t
*p =
(Hacl_Hash_Blake2b_Simd256_state_t *)KRML_HOST_MALLOC(sizeof (
Hacl_Hash_Blake2b_Simd256_state_t
));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
Lib_IntVector_Intrinsics_vec256 *b = block_state1.f3.snd;
Lib_IntVector_Intrinsics_vec256 *wv = block_state1.f3.fst;
KRML_ALIGNED_FREE(wv);
KRML_ALIGNED_FREE(b);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_Blake2b_blake2_params *p1 = key.fst;
uint8_t kk1 = p1->key_length;
uint8_t nn = p1->digest_length;
bool last_node = block_state1.thd;
Hacl_Hash_Blake2b_index
i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
Lib_IntVector_Intrinsics_vec256 *h = block_state1.f3.snd;
uint32_t kk20 = (uint32_t)i.key_length;
uint8_t *k_2 = key.snd;
if (!(kk20 == 0U))
{
uint8_t *sub_b = buf1 + kk20;
memset(sub_b, 0U, (128U - kk20) * sizeof (uint8_t));
memcpy(buf1, k_2, kk20 * sizeof (uint8_t));
}
Hacl_Hash_Blake2b_blake2_params pv = p1[0U];
uint64_t tmp[8U] = { 0U };
Lib_IntVector_Intrinsics_vec256 *r0 = h;
Lib_IntVector_Intrinsics_vec256 *r1 = h + 1U;
Lib_IntVector_Intrinsics_vec256 *r2 = h + 2U;
Lib_IntVector_Intrinsics_vec256 *r3 = h + 3U;
uint64_t iv0 = Hacl_Hash_Blake2b_ivTable_B[0U];
uint64_t iv1 = Hacl_Hash_Blake2b_ivTable_B[1U];
uint64_t iv2 = Hacl_Hash_Blake2b_ivTable_B[2U];
uint64_t iv3 = Hacl_Hash_Blake2b_ivTable_B[3U];
uint64_t iv4 = Hacl_Hash_Blake2b_ivTable_B[4U];
uint64_t iv5 = Hacl_Hash_Blake2b_ivTable_B[5U];
uint64_t iv6 = Hacl_Hash_Blake2b_ivTable_B[6U];
uint64_t iv7 = Hacl_Hash_Blake2b_ivTable_B[7U];
r2[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0, iv1, iv2, iv3);
r3[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7);
uint8_t kk2 = pv.key_length;
uint8_t nn1 = pv.digest_length;
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint64_t *os = tmp + 4U;
uint8_t *bj = pv.salt + i0 * 8U;
uint64_t u = load64_le(bj);
uint64_t r4 = u;
uint64_t x = r4;
os[i0] = x;);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint64_t *os = tmp + 6U;
uint8_t *bj = pv.personal + i0 * 8U;
uint64_t u = load64_le(bj);
uint64_t r4 = u;
uint64_t x = r4;
os[i0] = x;);
tmp[0U] =
(uint64_t)nn1
^
((uint64_t)kk2
<< 8U
^
((uint64_t)pv.fanout
<< 16U
^ ((uint64_t)pv.depth << 24U ^ (uint64_t)pv.leaf_length << 32U)));
tmp[1U] = pv.node_offset;
tmp[2U] = (uint64_t)pv.node_depth ^ (uint64_t)pv.inner_length << 8U;
tmp[3U] = 0ULL;
uint64_t tmp0 = tmp[0U];
uint64_t tmp1 = tmp[1U];
uint64_t tmp2 = tmp[2U];
uint64_t tmp3 = tmp[3U];
uint64_t tmp4 = tmp[4U];
uint64_t tmp5 = tmp[5U];
uint64_t tmp6 = tmp[6U];
uint64_t tmp7 = tmp[7U];
uint64_t iv0_ = iv0 ^ tmp0;
uint64_t iv1_ = iv1 ^ tmp1;
uint64_t iv2_ = iv2 ^ tmp2;
uint64_t iv3_ = iv3 ^ tmp3;
uint64_t iv4_ = iv4 ^ tmp4;
uint64_t iv5_ = iv5 ^ tmp5;
uint64_t iv6_ = iv6 ^ tmp6;
uint64_t iv7_ = iv7 ^ tmp7;
r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1_, iv2_, iv3_);
r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4_, iv5_, iv6_, iv7_);
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**
@ -695,7 +831,7 @@ The caller must satisfy the following requirements.
*/
Hacl_Hash_Blake2b_Simd256_state_t
*Hacl_Hash_Blake2b_Simd256_malloc_with_key0(uint8_t *k, uint8_t kk)
*Hacl_Hash_Blake2b_Simd256_malloc_with_key(uint8_t *k, uint8_t kk)
{
uint8_t nn = 64U;
Hacl_Hash_Blake2b_index i = { .key_length = kk, .digest_length = nn, .last_node = false };
@ -721,7 +857,7 @@ use Blake2 as a hash function. Further resettings of the state SHALL be done wit
*/
Hacl_Hash_Blake2b_Simd256_state_t *Hacl_Hash_Blake2b_Simd256_malloc(void)
{
return Hacl_Hash_Blake2b_Simd256_malloc_with_key0(NULL, 0U);
return Hacl_Hash_Blake2b_Simd256_malloc_with_key(NULL, 0U);
}
static Hacl_Hash_Blake2b_index index_of_state(Hacl_Hash_Blake2b_Simd256_state_t *s)
@ -967,7 +1103,7 @@ Hacl_Hash_Blake2b_Simd256_update(
if (!(sz1 == 0U))
{
uint64_t prevlen = total_len1 - (uint64_t)sz1;
K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ acc = block_state1.f3;
Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = block_state1.f3;
Lib_IntVector_Intrinsics_vec256 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec256 *hash = acc.snd;
uint32_t nb = 1U;
@ -992,7 +1128,7 @@ Hacl_Hash_Blake2b_Simd256_update(
uint32_t data2_len = chunk_len - data1_len;
uint8_t *data1 = chunk;
uint8_t *data2 = chunk + data1_len;
K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ acc = block_state1.f3;
Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = block_state1.f3;
Lib_IntVector_Intrinsics_vec256 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec256 *hash = acc.snd;
uint32_t nb = data1_len / 128U;
@ -1060,7 +1196,7 @@ Hacl_Hash_Blake2b_Simd256_update(
if (!(sz1 == 0U))
{
uint64_t prevlen = total_len1 - (uint64_t)sz1;
K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ acc = block_state1.f3;
Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = block_state1.f3;
Lib_IntVector_Intrinsics_vec256 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec256 *hash = acc.snd;
uint32_t nb = 1U;
@ -1086,7 +1222,7 @@ Hacl_Hash_Blake2b_Simd256_update(
uint32_t data2_len = chunk_len - diff - data1_len;
uint8_t *data1 = chunk2;
uint8_t *data2 = chunk2 + data1_len;
K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ acc = block_state1.f3;
Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = block_state1.f3;
Lib_IntVector_Intrinsics_vec256 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec256 *hash = acc.snd;
uint32_t nb = data1_len / 128U;
@ -1169,8 +1305,7 @@ uint8_t Hacl_Hash_Blake2b_Simd256_digest(Hacl_Hash_Blake2b_Simd256_state_t *s, u
}
uint8_t *buf_last = buf_1 + r - ite;
uint8_t *buf_multi = buf_1;
K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_
acc0 = tmp_block_state.f3;
Hacl_Hash_Blake2b_Simd256_two_2b_256 acc0 = tmp_block_state.f3;
Lib_IntVector_Intrinsics_vec256 *wv1 = acc0.fst;
Lib_IntVector_Intrinsics_vec256 *hash0 = acc0.snd;
uint32_t nb = 0U;
@ -1181,8 +1316,7 @@ uint8_t Hacl_Hash_Blake2b_Simd256_digest(Hacl_Hash_Blake2b_Simd256_state_t *s, u
buf_multi,
nb);
uint64_t prev_len_last = total_len - (uint64_t)r;
K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_
acc = tmp_block_state.f3;
Hacl_Hash_Blake2b_Simd256_two_2b_256 acc = tmp_block_state.f3;
bool last_node1 = tmp_block_state.thd;
Lib_IntVector_Intrinsics_vec256 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec256 *hash = acc.snd;
@ -1244,37 +1378,120 @@ Hacl_Hash_Blake2b_Simd256_state_t
uint8_t kk1 = block_state0.fst;
Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
memcpy(buf, buf0, 128U * sizeof (uint8_t));
Lib_IntVector_Intrinsics_vec256
*wv =
*wv0 =
(Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32,
sizeof (Lib_IntVector_Intrinsics_vec256) * 4U);
memset(wv, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
Lib_IntVector_Intrinsics_vec256
*b =
(Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32,
sizeof (Lib_IntVector_Intrinsics_vec256) * 4U);
memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
Hacl_Hash_Blake2b_Simd256_block_state_t
block_state =
if (wv0 != NULL)
{
memset(wv0, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
}
option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___
block_state;
if (wv0 == NULL)
{
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
Lib_IntVector_Intrinsics_vec256
*b =
(Lib_IntVector_Intrinsics_vec256 *)KRML_ALIGNED_MALLOC(32,
sizeof (Lib_IntVector_Intrinsics_vec256) * 4U);
if (b != NULL)
{
.fst = i.key_length,
.snd = i.digest_length,
.thd = i.last_node,
.f3 = { .fst = wv, .snd = b }
};
Lib_IntVector_Intrinsics_vec256 *src_b = block_state0.f3.snd;
Lib_IntVector_Intrinsics_vec256 *dst_b = block_state.f3.snd;
memcpy(dst_b, src_b, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
Hacl_Hash_Blake2b_Simd256_state_t
s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
Hacl_Hash_Blake2b_Simd256_state_t
*p =
(Hacl_Hash_Blake2b_Simd256_state_t *)KRML_HOST_MALLOC(sizeof (
Hacl_Hash_Blake2b_Simd256_state_t
));
p[0U] = s;
return p;
memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
}
if (b == NULL)
{
KRML_ALIGNED_FREE(wv0);
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec256_____Lib_IntVector_Intrinsics_vec256___){
.tag = Hacl_Streaming_Types_Some,
.v = {
.fst = i.key_length,
.snd = i.digest_length,
.thd = i.last_node,
.f3 = { .fst = wv0, .snd = b }
}
}
);
}
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_Blake2b_Simd256_block_state_t block_state1 = block_state.v;
Lib_IntVector_Intrinsics_vec256 *src_b = block_state0.f3.snd;
Lib_IntVector_Intrinsics_vec256 *dst_b = block_state1.f3.snd;
memcpy(dst_b, src_b, 4U * sizeof (Lib_IntVector_Intrinsics_vec256));
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Hash_Blake2b_Simd256_state_t
s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 };
Hacl_Hash_Blake2b_Simd256_state_t
*p =
(Hacl_Hash_Blake2b_Simd256_state_t *)KRML_HOST_MALLOC(sizeof (
Hacl_Hash_Blake2b_Simd256_state_t
));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
Lib_IntVector_Intrinsics_vec256 *b = block_state1.f3.snd;
Lib_IntVector_Intrinsics_vec256 *wv = block_state1.f3.fst;
KRML_ALIGNED_FREE(wv);
KRML_ALIGNED_FREE(b);
KRML_HOST_FREE(buf);
return NULL;
}
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**

27
Modules/_hacl/Hacl_Hash_Blake2b_Simd256.h
View file

@ -32,14 +32,12 @@ extern "C" {
#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)
@ -51,29 +49,10 @@ extern "C" {
#define HACL_HASH_BLAKE2B_SIMD256_PERSONAL_BYTES (16U)
typedef struct K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256__s
{
Lib_IntVector_Intrinsics_vec256 *fst;
Lib_IntVector_Intrinsics_vec256 *snd;
}
K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_;
typedef struct Hacl_Hash_Blake2b_Simd256_block_state_t_s
{
uint8_t fst;
uint8_t snd;
bool thd;
K____Lib_IntVector_Intrinsics_vec256___Lib_IntVector_Intrinsics_vec256_ f3;
}
Hacl_Hash_Blake2b_Simd256_block_state_t;
typedef struct Hacl_Hash_Blake2b_Simd256_state_t_s
{
Hacl_Hash_Blake2b_Simd256_block_state_t block_state;
uint8_t *buf;
uint64_t total_len;
}
Hacl_Hash_Blake2b_Simd256_state_t;
typedef struct Hacl_Hash_Blake2b_Simd256_state_t_s Hacl_Hash_Blake2b_Simd256_state_t;
/**
General-purpose allocation function that gives control over all
@ -109,7 +88,7 @@ The caller must satisfy the following requirements.
*/
Hacl_Hash_Blake2b_Simd256_state_t
*Hacl_Hash_Blake2b_Simd256_malloc_with_key0(uint8_t *k, uint8_t kk);
*Hacl_Hash_Blake2b_Simd256_malloc_with_key(uint8_t *k, uint8_t kk);
/**
Specialized allocation function that picks default values for all

417
Modules/_hacl/Hacl_Hash_Blake2s.c
View file

@ -25,6 +25,9 @@
#include "internal/Hacl_Hash_Blake2s.h"
#include "Hacl_Streaming_Types.h"
#include "Hacl_Hash_Blake2b.h"
#include "internal/Hacl_Streaming_Types.h"
#include "internal/Hacl_Impl_Blake2_Constants.h"
#include "internal/Hacl_Hash_Blake2b.h"
#include "lib_memzero0.h"
@ -685,124 +688,212 @@ void Hacl_Hash_Blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash)
Lib_Memzero0_memzero(b, 32U, uint8_t, void *);
}
typedef struct option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t____s
{
Hacl_Streaming_Types_optional tag;
Hacl_Hash_Blake2s_block_state_t v;
}
option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___;
static Hacl_Hash_Blake2s_state_t
*malloc_raw(Hacl_Hash_Blake2b_index kk, Hacl_Hash_Blake2b_params_and_key key)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
uint32_t *wv = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t));
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t));
Hacl_Hash_Blake2s_block_state_t
block_state =
{
.fst = kk.key_length,
.snd = kk.digest_length,
.thd = kk.last_node,
.f3 = { .fst = wv, .snd = b }
};
uint8_t kk10 = kk.key_length;
uint32_t ite;
if (kk10 != 0U)
if (buf == NULL)
{
ite = 64U;
return NULL;
}
uint8_t *buf1 = buf;
uint32_t *wv0 = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t));
option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___ block_state;
if (wv0 == NULL)
{
block_state =
(
(option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
ite = 0U;
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t));
if (b == NULL)
{
KRML_HOST_FREE(wv0);
block_state =
(
(option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
block_state =
(
(option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){
.tag = Hacl_Streaming_Types_Some,
.v = {
.fst = kk.key_length,
.snd = kk.digest_length,
.thd = kk.last_node,
.f3 = { .fst = wv0, .snd = b }
}
}
);
}
}
Hacl_Hash_Blake2s_state_t
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)ite };
Hacl_Hash_Blake2s_state_t
*p = (Hacl_Hash_Blake2s_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2s_state_t));
p[0U] = s;
Hacl_Hash_Blake2b_blake2_params *p1 = key.fst;
uint8_t kk1 = p1->key_length;
uint8_t nn = p1->digest_length;
bool last_node = block_state.thd;
Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
uint32_t *h = block_state.f3.snd;
uint32_t kk2 = (uint32_t)i.key_length;
uint8_t *k_1 = key.snd;
if (!(kk2 == 0U))
if (block_state.tag == Hacl_Streaming_Types_None)
{
uint8_t *sub_b = buf + kk2;
memset(sub_b, 0U, (64U - kk2) * sizeof (uint8_t));
memcpy(buf, k_1, kk2 * sizeof (uint8_t));
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_Blake2b_blake2_params pv = p1[0U];
uint32_t tmp[8U] = { 0U };
uint32_t *r0 = h;
uint32_t *r1 = h + 4U;
uint32_t *r2 = h + 8U;
uint32_t *r3 = h + 12U;
uint32_t iv0 = Hacl_Hash_Blake2b_ivTable_S[0U];
uint32_t iv1 = Hacl_Hash_Blake2b_ivTable_S[1U];
uint32_t iv2 = Hacl_Hash_Blake2b_ivTable_S[2U];
uint32_t iv3 = Hacl_Hash_Blake2b_ivTable_S[3U];
uint32_t iv4 = Hacl_Hash_Blake2b_ivTable_S[4U];
uint32_t iv5 = Hacl_Hash_Blake2b_ivTable_S[5U];
uint32_t iv6 = Hacl_Hash_Blake2b_ivTable_S[6U];
uint32_t iv7 = Hacl_Hash_Blake2b_ivTable_S[7U];
r2[0U] = iv0;
r2[1U] = iv1;
r2[2U] = iv2;
r2[3U] = iv3;
r3[0U] = iv4;
r3[1U] = iv5;
r3[2U] = iv6;
r3[3U] = iv7;
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint32_t *os = tmp + 4U;
uint8_t *bj = pv.salt + i0 * 4U;
uint32_t u = load32_le(bj);
uint32_t r4 = u;
uint32_t x = r4;
os[i0] = x;);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint32_t *os = tmp + 6U;
uint8_t *bj = pv.personal + i0 * 4U;
uint32_t u = load32_le(bj);
uint32_t r4 = u;
uint32_t x = r4;
os[i0] = x;);
tmp[0U] =
(uint32_t)pv.digest_length
^ ((uint32_t)pv.key_length << 8U ^ ((uint32_t)pv.fanout << 16U ^ (uint32_t)pv.depth << 24U));
tmp[1U] = pv.leaf_length;
tmp[2U] = (uint32_t)pv.node_offset;
tmp[3U] =
(uint32_t)(pv.node_offset >> 32U)
^ ((uint32_t)pv.node_depth << 16U ^ (uint32_t)pv.inner_length << 24U);
uint32_t tmp0 = tmp[0U];
uint32_t tmp1 = tmp[1U];
uint32_t tmp2 = tmp[2U];
uint32_t tmp3 = tmp[3U];
uint32_t tmp4 = tmp[4U];
uint32_t tmp5 = tmp[5U];
uint32_t tmp6 = tmp[6U];
uint32_t tmp7 = tmp[7U];
uint32_t iv0_ = iv0 ^ tmp0;
uint32_t iv1_ = iv1 ^ tmp1;
uint32_t iv2_ = iv2 ^ tmp2;
uint32_t iv3_ = iv3 ^ tmp3;
uint32_t iv4_ = iv4 ^ tmp4;
uint32_t iv5_ = iv5 ^ tmp5;
uint32_t iv6_ = iv6 ^ tmp6;
uint32_t iv7_ = iv7 ^ tmp7;
r0[0U] = iv0_;
r0[1U] = iv1_;
r0[2U] = iv2_;
r0[3U] = iv3_;
r1[0U] = iv4_;
r1[1U] = iv5_;
r1[2U] = iv6_;
r1[3U] = iv7_;
return p;
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_Blake2s_block_state_t block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
uint8_t kk10 = kk.key_length;
uint32_t ite;
if (kk10 != 0U)
{
ite = 64U;
}
else
{
ite = 0U;
}
Hacl_Hash_Blake2s_state_t
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)ite };
Hacl_Hash_Blake2s_state_t
*p = (Hacl_Hash_Blake2s_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2s_state_t));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
uint32_t *b = block_state1.f3.snd;
uint32_t *wv = block_state1.f3.fst;
KRML_HOST_FREE(wv);
KRML_HOST_FREE(b);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_Blake2b_blake2_params *p1 = key.fst;
uint8_t kk1 = p1->key_length;
uint8_t nn = p1->digest_length;
bool last_node = block_state1.thd;
Hacl_Hash_Blake2b_index
i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
uint32_t *h = block_state1.f3.snd;
uint32_t kk2 = (uint32_t)i.key_length;
uint8_t *k_2 = key.snd;
if (!(kk2 == 0U))
{
uint8_t *sub_b = buf1 + kk2;
memset(sub_b, 0U, (64U - kk2) * sizeof (uint8_t));
memcpy(buf1, k_2, kk2 * sizeof (uint8_t));
}
Hacl_Hash_Blake2b_blake2_params pv = p1[0U];
uint32_t tmp[8U] = { 0U };
uint32_t *r0 = h;
uint32_t *r1 = h + 4U;
uint32_t *r2 = h + 8U;
uint32_t *r3 = h + 12U;
uint32_t iv0 = Hacl_Hash_Blake2b_ivTable_S[0U];
uint32_t iv1 = Hacl_Hash_Blake2b_ivTable_S[1U];
uint32_t iv2 = Hacl_Hash_Blake2b_ivTable_S[2U];
uint32_t iv3 = Hacl_Hash_Blake2b_ivTable_S[3U];
uint32_t iv4 = Hacl_Hash_Blake2b_ivTable_S[4U];
uint32_t iv5 = Hacl_Hash_Blake2b_ivTable_S[5U];
uint32_t iv6 = Hacl_Hash_Blake2b_ivTable_S[6U];
uint32_t iv7 = Hacl_Hash_Blake2b_ivTable_S[7U];
r2[0U] = iv0;
r2[1U] = iv1;
r2[2U] = iv2;
r2[3U] = iv3;
r3[0U] = iv4;
r3[1U] = iv5;
r3[2U] = iv6;
r3[3U] = iv7;
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint32_t *os = tmp + 4U;
uint8_t *bj = pv.salt + i0 * 4U;
uint32_t u = load32_le(bj);
uint32_t r4 = u;
uint32_t x = r4;
os[i0] = x;);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint32_t *os = tmp + 6U;
uint8_t *bj = pv.personal + i0 * 4U;
uint32_t u = load32_le(bj);
uint32_t r4 = u;
uint32_t x = r4;
os[i0] = x;);
tmp[0U] =
(uint32_t)pv.digest_length
^
((uint32_t)pv.key_length
<< 8U
^ ((uint32_t)pv.fanout << 16U ^ (uint32_t)pv.depth << 24U));
tmp[1U] = pv.leaf_length;
tmp[2U] = (uint32_t)pv.node_offset;
tmp[3U] =
(uint32_t)(pv.node_offset >> 32U)
^ ((uint32_t)pv.node_depth << 16U ^ (uint32_t)pv.inner_length << 24U);
uint32_t tmp0 = tmp[0U];
uint32_t tmp1 = tmp[1U];
uint32_t tmp2 = tmp[2U];
uint32_t tmp3 = tmp[3U];
uint32_t tmp4 = tmp[4U];
uint32_t tmp5 = tmp[5U];
uint32_t tmp6 = tmp[6U];
uint32_t tmp7 = tmp[7U];
uint32_t iv0_ = iv0 ^ tmp0;
uint32_t iv1_ = iv1 ^ tmp1;
uint32_t iv2_ = iv2 ^ tmp2;
uint32_t iv3_ = iv3 ^ tmp3;
uint32_t iv4_ = iv4 ^ tmp4;
uint32_t iv5_ = iv5 ^ tmp5;
uint32_t iv6_ = iv6 ^ tmp6;
uint32_t iv7_ = iv7 ^ tmp7;
r0[0U] = iv0_;
r0[1U] = iv1_;
r0[2U] = iv2_;
r0[3U] = iv3_;
r1[0U] = iv4_;
r1[1U] = iv5_;
r1[2U] = iv6_;
r1[3U] = iv7_;
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**
@ -1362,26 +1453,102 @@ Hacl_Hash_Blake2s_state_t *Hacl_Hash_Blake2s_copy(Hacl_Hash_Blake2s_state_t *sta
uint8_t kk1 = block_state0.fst;
Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
memcpy(buf, buf0, 64U * sizeof (uint8_t));
uint32_t *wv = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t));
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t));
Hacl_Hash_Blake2s_block_state_t
block_state =
uint32_t *wv0 = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t));
option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___ block_state;
if (wv0 == NULL)
{
block_state =
(
(option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(16U, sizeof (uint32_t));
if (b == NULL)
{
.fst = i.key_length,
.snd = i.digest_length,
.thd = i.last_node,
.f3 = { .fst = wv, .snd = b }
};
uint32_t *src_b = block_state0.f3.snd;
uint32_t *dst_b = block_state.f3.snd;
memcpy(dst_b, src_b, 16U * sizeof (uint32_t));
Hacl_Hash_Blake2s_state_t
s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
Hacl_Hash_Blake2s_state_t
*p = (Hacl_Hash_Blake2s_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2s_state_t));
p[0U] = s;
return p;
KRML_HOST_FREE(wv0);
block_state =
(
(option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
block_state =
(
(option___uint8_t___uint8_t___bool_____uint32_t_____uint32_t___){
.tag = Hacl_Streaming_Types_Some,
.v = {
.fst = i.key_length,
.snd = i.digest_length,
.thd = i.last_node,
.f3 = { .fst = wv0, .snd = b }
}
}
);
}
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_Blake2s_block_state_t block_state1 = block_state.v;
uint32_t *src_b = block_state0.f3.snd;
uint32_t *dst_b = block_state1.f3.snd;
memcpy(dst_b, src_b, 16U * sizeof (uint32_t));
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Hash_Blake2s_state_t
s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 };
Hacl_Hash_Blake2s_state_t
*p = (Hacl_Hash_Blake2s_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_Blake2s_state_t));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
uint32_t *b = block_state1.f3.snd;
uint32_t *wv = block_state1.f3.fst;
KRML_HOST_FREE(wv);
KRML_HOST_FREE(b);
KRML_HOST_FREE(buf);
return NULL;
}
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**

26
Modules/_hacl/Hacl_Hash_Blake2s.h
View file

@ -32,7 +32,7 @@ extern "C" {
#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"
@ -49,29 +49,9 @@ extern "C" {
#define HACL_HASH_BLAKE2S_PERSONAL_BYTES (8U)
typedef struct K____uint32_t___uint32_t__s
{
uint32_t *fst;
uint32_t *snd;
}
K____uint32_t___uint32_t_;
typedef struct Hacl_Hash_Blake2s_block_state_t_s Hacl_Hash_Blake2s_block_state_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;
typedef struct Hacl_Hash_Blake2s_state_t_s Hacl_Hash_Blake2s_state_t;
/**
General-purpose allocation function that gives control over all

504
Modules/_hacl/Hacl_Hash_Blake2s_Simd128.c
View file

@ -25,6 +25,9 @@
#include "internal/Hacl_Hash_Blake2s_Simd128.h"
#include "Hacl_Streaming_Types.h"
#include "Hacl_Hash_Blake2b.h"
#include "internal/Hacl_Streaming_Types.h"
#include "internal/Hacl_Impl_Blake2_Constants.h"
#include "internal/Hacl_Hash_Blake2b.h"
#include "lib_memzero0.h"
@ -516,133 +519,265 @@ Hacl_Hash_Blake2s_Simd128_load_state128s_from_state32(
r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(b3[0U], b3[1U], b3[2U], b3[3U]);
}
Lib_IntVector_Intrinsics_vec128 *Hacl_Hash_Blake2s_Simd128_malloc_with_key(void)
Lib_IntVector_Intrinsics_vec128 *Hacl_Hash_Blake2s_Simd128_malloc_internal_state_with_key(void)
{
Lib_IntVector_Intrinsics_vec128
*buf =
(Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16,
sizeof (Lib_IntVector_Intrinsics_vec128) * 4U);
memset(buf, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
if (buf != NULL)
{
memset(buf, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
}
return buf;
}
void
Hacl_Hash_Blake2s_Simd128_update_multi_no_inline(
Lib_IntVector_Intrinsics_vec128 *s,
uint64_t ev,
uint8_t *blocks,
uint32_t n
)
{
KRML_PRE_ALIGN(16) Lib_IntVector_Intrinsics_vec128 wv[4U] KRML_POST_ALIGN(16) = { 0U };
Hacl_Hash_Blake2s_Simd128_update_multi(n * 64U, wv, s, ev, blocks, n);
}
void
Hacl_Hash_Blake2s_Simd128_update_last_no_inline(
Lib_IntVector_Intrinsics_vec128 *s,
uint64_t prev,
uint8_t *input,
uint32_t input_len
)
{
KRML_PRE_ALIGN(16) Lib_IntVector_Intrinsics_vec128 wv[4U] KRML_POST_ALIGN(16) = { 0U };
Hacl_Hash_Blake2s_Simd128_update_last(input_len, wv, s, false, prev, input_len, input);
}
void
Hacl_Hash_Blake2s_Simd128_copy_internal_state(
Lib_IntVector_Intrinsics_vec128 *src,
Lib_IntVector_Intrinsics_vec128 *dst
)
{
memcpy(dst, src, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
}
typedef struct
option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128____s
{
Hacl_Streaming_Types_optional tag;
Hacl_Hash_Blake2s_Simd128_block_state_t v;
}
option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___;
static Hacl_Hash_Blake2s_Simd128_state_t
*malloc_raw(Hacl_Hash_Blake2b_index kk, Hacl_Hash_Blake2b_params_and_key key)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
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 =
(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 (buf == NULL)
{
ite = 64U;
return NULL;
}
uint8_t *buf1 = buf;
Lib_IntVector_Intrinsics_vec128
*wv0 =
(Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16,
sizeof (Lib_IntVector_Intrinsics_vec128) * 4U);
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
{
ite = 0U;
Lib_IntVector_Intrinsics_vec128
*b =
(Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16,
sizeof (Lib_IntVector_Intrinsics_vec128) * 4U);
if (b != NULL)
{
memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
}
if (b == NULL)
{
KRML_ALIGNED_FREE(wv0);
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){
.tag = Hacl_Streaming_Types_Some,
.v = {
.fst = kk.key_length,
.snd = kk.digest_length,
.thd = kk.last_node,
.f3 = { .fst = wv0, .snd = b }
}
}
);
}
}
Hacl_Hash_Blake2s_Simd128_state_t
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)ite };
Hacl_Hash_Blake2s_Simd128_state_t
*p =
(Hacl_Hash_Blake2s_Simd128_state_t *)KRML_HOST_MALLOC(sizeof (
Hacl_Hash_Blake2s_Simd128_state_t
));
p[0U] = s;
Hacl_Hash_Blake2b_blake2_params *p1 = key.fst;
uint8_t kk1 = p1->key_length;
uint8_t nn = p1->digest_length;
bool last_node = block_state.thd;
Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
Lib_IntVector_Intrinsics_vec128 *h = block_state.f3.snd;
uint32_t kk2 = (uint32_t)i.key_length;
uint8_t *k_1 = key.snd;
if (!(kk2 == 0U))
if (block_state.tag == Hacl_Streaming_Types_None)
{
uint8_t *sub_b = buf + kk2;
memset(sub_b, 0U, (64U - kk2) * sizeof (uint8_t));
memcpy(buf, k_1, kk2 * sizeof (uint8_t));
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_Blake2b_blake2_params pv = p1[0U];
uint32_t tmp[8U] = { 0U };
Lib_IntVector_Intrinsics_vec128 *r0 = h;
Lib_IntVector_Intrinsics_vec128 *r1 = h + 1U;
Lib_IntVector_Intrinsics_vec128 *r2 = h + 2U;
Lib_IntVector_Intrinsics_vec128 *r3 = h + 3U;
uint32_t iv0 = Hacl_Hash_Blake2b_ivTable_S[0U];
uint32_t iv1 = Hacl_Hash_Blake2b_ivTable_S[1U];
uint32_t iv2 = Hacl_Hash_Blake2b_ivTable_S[2U];
uint32_t iv3 = Hacl_Hash_Blake2b_ivTable_S[3U];
uint32_t iv4 = Hacl_Hash_Blake2b_ivTable_S[4U];
uint32_t iv5 = Hacl_Hash_Blake2b_ivTable_S[5U];
uint32_t iv6 = Hacl_Hash_Blake2b_ivTable_S[6U];
uint32_t iv7 = Hacl_Hash_Blake2b_ivTable_S[7U];
r2[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0, iv1, iv2, iv3);
r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint32_t *os = tmp + 4U;
uint8_t *bj = pv.salt + i0 * 4U;
uint32_t u = load32_le(bj);
uint32_t r4 = u;
uint32_t x = r4;
os[i0] = x;);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint32_t *os = tmp + 6U;
uint8_t *bj = pv.personal + i0 * 4U;
uint32_t u = load32_le(bj);
uint32_t r4 = u;
uint32_t x = r4;
os[i0] = x;);
tmp[0U] =
(uint32_t)pv.digest_length
^ ((uint32_t)pv.key_length << 8U ^ ((uint32_t)pv.fanout << 16U ^ (uint32_t)pv.depth << 24U));
tmp[1U] = pv.leaf_length;
tmp[2U] = (uint32_t)pv.node_offset;
tmp[3U] =
(uint32_t)(pv.node_offset >> 32U)
^ ((uint32_t)pv.node_depth << 16U ^ (uint32_t)pv.inner_length << 24U);
uint32_t tmp0 = tmp[0U];
uint32_t tmp1 = tmp[1U];
uint32_t tmp2 = tmp[2U];
uint32_t tmp3 = tmp[3U];
uint32_t tmp4 = tmp[4U];
uint32_t tmp5 = tmp[5U];
uint32_t tmp6 = tmp[6U];
uint32_t tmp7 = tmp[7U];
uint32_t iv0_ = iv0 ^ tmp0;
uint32_t iv1_ = iv1 ^ tmp1;
uint32_t iv2_ = iv2 ^ tmp2;
uint32_t iv3_ = iv3 ^ tmp3;
uint32_t iv4_ = iv4 ^ tmp4;
uint32_t iv5_ = iv5 ^ tmp5;
uint32_t iv6_ = iv6 ^ tmp6;
uint32_t iv7_ = iv7 ^ tmp7;
r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1_, iv2_, iv3_);
r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4_, iv5_, iv6_, iv7_);
return p;
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_Blake2s_Simd128_block_state_t block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
uint8_t kk10 = kk.key_length;
uint32_t ite;
if (kk10 != 0U)
{
ite = 64U;
}
else
{
ite = 0U;
}
Hacl_Hash_Blake2s_Simd128_state_t
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)ite };
Hacl_Hash_Blake2s_Simd128_state_t
*p =
(Hacl_Hash_Blake2s_Simd128_state_t *)KRML_HOST_MALLOC(sizeof (
Hacl_Hash_Blake2s_Simd128_state_t
));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
Lib_IntVector_Intrinsics_vec128 *b = block_state1.f3.snd;
Lib_IntVector_Intrinsics_vec128 *wv = block_state1.f3.fst;
KRML_ALIGNED_FREE(wv);
KRML_ALIGNED_FREE(b);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_Blake2b_blake2_params *p1 = key.fst;
uint8_t kk1 = p1->key_length;
uint8_t nn = p1->digest_length;
bool last_node = block_state1.thd;
Hacl_Hash_Blake2b_index
i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
Lib_IntVector_Intrinsics_vec128 *h = block_state1.f3.snd;
uint32_t kk2 = (uint32_t)i.key_length;
uint8_t *k_2 = key.snd;
if (!(kk2 == 0U))
{
uint8_t *sub_b = buf1 + kk2;
memset(sub_b, 0U, (64U - kk2) * sizeof (uint8_t));
memcpy(buf1, k_2, kk2 * sizeof (uint8_t));
}
Hacl_Hash_Blake2b_blake2_params pv = p1[0U];
uint32_t tmp[8U] = { 0U };
Lib_IntVector_Intrinsics_vec128 *r0 = h;
Lib_IntVector_Intrinsics_vec128 *r1 = h + 1U;
Lib_IntVector_Intrinsics_vec128 *r2 = h + 2U;
Lib_IntVector_Intrinsics_vec128 *r3 = h + 3U;
uint32_t iv0 = Hacl_Hash_Blake2b_ivTable_S[0U];
uint32_t iv1 = Hacl_Hash_Blake2b_ivTable_S[1U];
uint32_t iv2 = Hacl_Hash_Blake2b_ivTable_S[2U];
uint32_t iv3 = Hacl_Hash_Blake2b_ivTable_S[3U];
uint32_t iv4 = Hacl_Hash_Blake2b_ivTable_S[4U];
uint32_t iv5 = Hacl_Hash_Blake2b_ivTable_S[5U];
uint32_t iv6 = Hacl_Hash_Blake2b_ivTable_S[6U];
uint32_t iv7 = Hacl_Hash_Blake2b_ivTable_S[7U];
r2[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0, iv1, iv2, iv3);
r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint32_t *os = tmp + 4U;
uint8_t *bj = pv.salt + i0 * 4U;
uint32_t u = load32_le(bj);
uint32_t r4 = u;
uint32_t x = r4;
os[i0] = x;);
KRML_MAYBE_FOR2(i0,
0U,
2U,
1U,
uint32_t *os = tmp + 6U;
uint8_t *bj = pv.personal + i0 * 4U;
uint32_t u = load32_le(bj);
uint32_t r4 = u;
uint32_t x = r4;
os[i0] = x;);
tmp[0U] =
(uint32_t)pv.digest_length
^
((uint32_t)pv.key_length
<< 8U
^ ((uint32_t)pv.fanout << 16U ^ (uint32_t)pv.depth << 24U));
tmp[1U] = pv.leaf_length;
tmp[2U] = (uint32_t)pv.node_offset;
tmp[3U] =
(uint32_t)(pv.node_offset >> 32U)
^ ((uint32_t)pv.node_depth << 16U ^ (uint32_t)pv.inner_length << 24U);
uint32_t tmp0 = tmp[0U];
uint32_t tmp1 = tmp[1U];
uint32_t tmp2 = tmp[2U];
uint32_t tmp3 = tmp[3U];
uint32_t tmp4 = tmp[4U];
uint32_t tmp5 = tmp[5U];
uint32_t tmp6 = tmp[6U];
uint32_t tmp7 = tmp[7U];
uint32_t iv0_ = iv0 ^ tmp0;
uint32_t iv1_ = iv1 ^ tmp1;
uint32_t iv2_ = iv2 ^ tmp2;
uint32_t iv3_ = iv3 ^ tmp3;
uint32_t iv4_ = iv4 ^ tmp4;
uint32_t iv5_ = iv5 ^ tmp5;
uint32_t iv6_ = iv6 ^ tmp6;
uint32_t iv7_ = iv7 ^ tmp7;
r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1_, iv2_, iv3_);
r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4_, iv5_, iv6_, iv7_);
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**
@ -685,7 +820,7 @@ The caller must satisfy the following requirements.
*/
Hacl_Hash_Blake2s_Simd128_state_t
*Hacl_Hash_Blake2s_Simd128_malloc_with_key0(uint8_t *k, uint8_t kk)
*Hacl_Hash_Blake2s_Simd128_malloc_with_key(uint8_t *k, uint8_t kk)
{
uint8_t nn = 32U;
Hacl_Hash_Blake2b_index i = { .key_length = kk, .digest_length = nn, .last_node = false };
@ -711,7 +846,7 @@ use Blake2 as a hash function. Further resettings of the state SHALL be done wit
*/
Hacl_Hash_Blake2s_Simd128_state_t *Hacl_Hash_Blake2s_Simd128_malloc(void)
{
return Hacl_Hash_Blake2s_Simd128_malloc_with_key0(NULL, 0U);
return Hacl_Hash_Blake2s_Simd128_malloc_with_key(NULL, 0U);
}
static Hacl_Hash_Blake2b_index index_of_state(Hacl_Hash_Blake2s_Simd128_state_t *s)
@ -954,7 +1089,7 @@ Hacl_Hash_Blake2s_Simd128_update(
if (!(sz1 == 0U))
{
uint64_t prevlen = total_len1 - (uint64_t)sz1;
K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ acc = block_state1.f3;
Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = block_state1.f3;
Lib_IntVector_Intrinsics_vec128 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec128 *hash = acc.snd;
uint32_t nb = 1U;
@ -974,7 +1109,7 @@ Hacl_Hash_Blake2s_Simd128_update(
uint32_t data2_len = chunk_len - data1_len;
uint8_t *data1 = chunk;
uint8_t *data2 = chunk + data1_len;
K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ acc = block_state1.f3;
Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = block_state1.f3;
Lib_IntVector_Intrinsics_vec128 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec128 *hash = acc.snd;
uint32_t nb = data1_len / 64U;
@ -1037,7 +1172,7 @@ Hacl_Hash_Blake2s_Simd128_update(
if (!(sz1 == 0U))
{
uint64_t prevlen = total_len1 - (uint64_t)sz1;
K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ acc = block_state1.f3;
Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = block_state1.f3;
Lib_IntVector_Intrinsics_vec128 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec128 *hash = acc.snd;
uint32_t nb = 1U;
@ -1058,7 +1193,7 @@ Hacl_Hash_Blake2s_Simd128_update(
uint32_t data2_len = chunk_len - diff - data1_len;
uint8_t *data1 = chunk2;
uint8_t *data2 = chunk2 + data1_len;
K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ acc = block_state1.f3;
Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = block_state1.f3;
Lib_IntVector_Intrinsics_vec128 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec128 *hash = acc.snd;
uint32_t nb = data1_len / 64U;
@ -1136,15 +1271,13 @@ uint8_t Hacl_Hash_Blake2s_Simd128_digest(Hacl_Hash_Blake2s_Simd128_state_t *s, u
}
uint8_t *buf_last = buf_1 + r - ite;
uint8_t *buf_multi = buf_1;
K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_
acc0 = tmp_block_state.f3;
Hacl_Hash_Blake2s_Simd128_two_2s_128 acc0 = tmp_block_state.f3;
Lib_IntVector_Intrinsics_vec128 *wv1 = acc0.fst;
Lib_IntVector_Intrinsics_vec128 *hash0 = acc0.snd;
uint32_t nb = 0U;
Hacl_Hash_Blake2s_Simd128_update_multi(0U, wv1, hash0, prev_len, buf_multi, nb);
uint64_t prev_len_last = total_len - (uint64_t)r;
K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_
acc = tmp_block_state.f3;
Hacl_Hash_Blake2s_Simd128_two_2s_128 acc = tmp_block_state.f3;
bool last_node1 = tmp_block_state.thd;
Lib_IntVector_Intrinsics_vec128 *wv = acc.fst;
Lib_IntVector_Intrinsics_vec128 *hash = acc.snd;
@ -1200,37 +1333,120 @@ Hacl_Hash_Blake2s_Simd128_state_t
uint8_t kk1 = block_state0.fst;
Hacl_Hash_Blake2b_index i = { .key_length = kk1, .digest_length = nn, .last_node = last_node };
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
memcpy(buf, buf0, 64U * sizeof (uint8_t));
Lib_IntVector_Intrinsics_vec128
*wv =
*wv0 =
(Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16,
sizeof (Lib_IntVector_Intrinsics_vec128) * 4U);
memset(wv, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
Lib_IntVector_Intrinsics_vec128
*b =
(Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16,
sizeof (Lib_IntVector_Intrinsics_vec128) * 4U);
memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
Hacl_Hash_Blake2s_Simd128_block_state_t
block_state =
if (wv0 != NULL)
{
memset(wv0, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
}
option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___
block_state;
if (wv0 == NULL)
{
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
Lib_IntVector_Intrinsics_vec128
*b =
(Lib_IntVector_Intrinsics_vec128 *)KRML_ALIGNED_MALLOC(16,
sizeof (Lib_IntVector_Intrinsics_vec128) * 4U);
if (b != NULL)
{
.fst = i.key_length,
.snd = i.digest_length,
.thd = i.last_node,
.f3 = { .fst = wv, .snd = b }
};
Lib_IntVector_Intrinsics_vec128 *src_b = block_state0.f3.snd;
Lib_IntVector_Intrinsics_vec128 *dst_b = block_state.f3.snd;
memcpy(dst_b, src_b, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
Hacl_Hash_Blake2s_Simd128_state_t
s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
Hacl_Hash_Blake2s_Simd128_state_t
*p =
(Hacl_Hash_Blake2s_Simd128_state_t *)KRML_HOST_MALLOC(sizeof (
Hacl_Hash_Blake2s_Simd128_state_t
));
p[0U] = s;
return p;
memset(b, 0U, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
}
if (b == NULL)
{
KRML_ALIGNED_FREE(wv0);
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){
.tag = Hacl_Streaming_Types_None
}
);
}
else
{
block_state =
(
(option___uint8_t___uint8_t___bool_____Lib_IntVector_Intrinsics_vec128_____Lib_IntVector_Intrinsics_vec128___){
.tag = Hacl_Streaming_Types_Some,
.v = {
.fst = i.key_length,
.snd = i.digest_length,
.thd = i.last_node,
.f3 = { .fst = wv0, .snd = b }
}
}
);
}
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_Blake2s_Simd128_block_state_t block_state1 = block_state.v;
Lib_IntVector_Intrinsics_vec128 *src_b = block_state0.f3.snd;
Lib_IntVector_Intrinsics_vec128 *dst_b = block_state1.f3.snd;
memcpy(dst_b, src_b, 4U * sizeof (Lib_IntVector_Intrinsics_vec128));
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Hash_Blake2s_Simd128_state_t
s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 };
Hacl_Hash_Blake2s_Simd128_state_t
*p =
(Hacl_Hash_Blake2s_Simd128_state_t *)KRML_HOST_MALLOC(sizeof (
Hacl_Hash_Blake2s_Simd128_state_t
));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
Lib_IntVector_Intrinsics_vec128 *b = block_state1.f3.snd;
Lib_IntVector_Intrinsics_vec128 *wv = block_state1.f3.fst;
KRML_ALIGNED_FREE(wv);
KRML_ALIGNED_FREE(b);
KRML_HOST_FREE(buf);
return NULL;
}
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**

26
Modules/_hacl/Hacl_Hash_Blake2s_Simd128.h
View file

@ -32,13 +32,12 @@ extern "C" {
#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)
@ -50,29 +49,10 @@ extern "C" {
#define HACL_HASH_BLAKE2S_SIMD128_PERSONAL_BYTES (8U)
typedef struct K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128__s
{
Lib_IntVector_Intrinsics_vec128 *fst;
Lib_IntVector_Intrinsics_vec128 *snd;
}
K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_;
typedef struct Hacl_Hash_Blake2s_Simd128_block_state_t_s
{
uint8_t fst;
uint8_t snd;
bool thd;
K____Lib_IntVector_Intrinsics_vec128___Lib_IntVector_Intrinsics_vec128_ f3;
}
Hacl_Hash_Blake2s_Simd128_block_state_t;
typedef struct Hacl_Hash_Blake2s_Simd128_state_t_s
{
Hacl_Hash_Blake2s_Simd128_block_state_t block_state;
uint8_t *buf;
uint64_t total_len;
}
Hacl_Hash_Blake2s_Simd128_state_t;
typedef struct Hacl_Hash_Blake2s_Simd128_state_t_s Hacl_Hash_Blake2s_Simd128_state_t;
/**
General-purpose allocation function that gives control over all
@ -108,7 +88,7 @@ The caller must satisfy the following requirements.
*/
Hacl_Hash_Blake2s_Simd128_state_t
*Hacl_Hash_Blake2s_Simd128_malloc_with_key0(uint8_t *k, uint8_t kk);
*Hacl_Hash_Blake2s_Simd128_malloc_with_key(uint8_t *k, uint8_t kk);
/**
Specialized allocation function that picks default values for all

140
Modules/_hacl/Hacl_Hash_MD5.c
View file

@ -25,6 +25,9 @@
#include "internal/Hacl_Hash_MD5.h"
#include "Hacl_Streaming_Types.h"
#include "internal/Hacl_Streaming_Types.h"
static uint32_t _h0[4U] = { 0x67452301U, 0xefcdab89U, 0x98badcfeU, 0x10325476U };
static uint32_t
@ -1166,14 +1169,67 @@ void Hacl_Hash_MD5_hash_oneshot(uint8_t *output, uint8_t *input, uint32_t input_
Hacl_Streaming_MD_state_32 *Hacl_Hash_MD5_malloc(void)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t));
Hacl_Streaming_MD_state_32
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
p[0U] = s;
Hacl_Hash_MD5_init(block_state);
return p;
if (buf == NULL)
{
return NULL;
}
uint8_t *buf1 = buf;
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t));
Hacl_Streaming_Types_optional_32 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf1);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint32_t *block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_32
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_MD5_init(block_state1);
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
void Hacl_Hash_MD5_reset(Hacl_Streaming_MD_state_32 *state)
@ -1412,15 +1468,67 @@ Hacl_Streaming_MD_state_32 *Hacl_Hash_MD5_copy(Hacl_Streaming_MD_state_32 *state
uint8_t *buf0 = scrut.buf;
uint64_t total_len0 = scrut.total_len;
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
memcpy(buf, buf0, 64U * sizeof (uint8_t));
uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t));
memcpy(block_state, block_state0, 4U * sizeof (uint32_t));
Hacl_Streaming_MD_state_32
s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
p[0U] = s;
return p;
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(4U, sizeof (uint32_t));
Hacl_Streaming_Types_optional_32 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint32_t *block_state1 = block_state.v;
memcpy(block_state1, block_state0, 4U * sizeof (uint32_t));
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_32
s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf);
return NULL;
}
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
void Hacl_Hash_MD5_hash(uint8_t *output, uint8_t *input, uint32_t input_len)

2
Modules/_hacl/Hacl_Hash_MD5.h
View file

@ -32,7 +32,7 @@ extern "C" {
#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"

140
Modules/_hacl/Hacl_Hash_SHA1.c
View file

@ -25,6 +25,9 @@
#include "internal/Hacl_Hash_SHA1.h"
#include "Hacl_Streaming_Types.h"
#include "internal/Hacl_Streaming_Types.h"
static uint32_t _h0[5U] = { 0x67452301U, 0xefcdab89U, 0x98badcfeU, 0x10325476U, 0xc3d2e1f0U };
void Hacl_Hash_SHA1_init(uint32_t *s)
@ -199,14 +202,67 @@ void Hacl_Hash_SHA1_hash_oneshot(uint8_t *output, uint8_t *input, uint32_t input
Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA1_malloc(void)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(5U, sizeof (uint32_t));
Hacl_Streaming_MD_state_32
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
p[0U] = s;
Hacl_Hash_SHA1_init(block_state);
return p;
if (buf == NULL)
{
return NULL;
}
uint8_t *buf1 = buf;
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(5U, sizeof (uint32_t));
Hacl_Streaming_Types_optional_32 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf1);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint32_t *block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_32
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_SHA1_init(block_state1);
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
void Hacl_Hash_SHA1_reset(Hacl_Streaming_MD_state_32 *state)
@ -445,15 +501,67 @@ Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA1_copy(Hacl_Streaming_MD_state_32 *stat
uint8_t *buf0 = scrut.buf;
uint64_t total_len0 = scrut.total_len;
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
memcpy(buf, buf0, 64U * sizeof (uint8_t));
uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(5U, sizeof (uint32_t));
memcpy(block_state, block_state0, 5U * sizeof (uint32_t));
Hacl_Streaming_MD_state_32
s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
p[0U] = s;
return p;
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(5U, sizeof (uint32_t));
Hacl_Streaming_Types_optional_32 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint32_t *block_state1 = block_state.v;
memcpy(block_state1, block_state0, 5U * sizeof (uint32_t));
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_32
s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf);
return NULL;
}
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
void Hacl_Hash_SHA1_hash(uint8_t *output, uint8_t *input, uint32_t input_len)

2
Modules/_hacl/Hacl_Hash_SHA1.h
View file

@ -32,7 +32,7 @@ extern "C" {
#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"

415
Modules/_hacl/Hacl_Hash_SHA2.c
View file

@ -25,6 +25,9 @@
#include "internal/Hacl_Hash_SHA2.h"
#include "Hacl_Streaming_Types.h"
#include "internal/Hacl_Streaming_Types.h"
void Hacl_Hash_SHA2_sha256_init(uint32_t *hash)
@ -447,14 +450,67 @@ calling `free_256`.
Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA2_malloc_256(void)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t));
Hacl_Streaming_MD_state_32
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
p[0U] = s;
Hacl_Hash_SHA2_sha256_init(block_state);
return p;
if (buf == NULL)
{
return NULL;
}
uint8_t *buf1 = buf;
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t));
Hacl_Streaming_Types_optional_32 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf1);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint32_t *block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_32
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_SHA2_sha256_init(block_state1);
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**
@ -470,15 +526,67 @@ Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA2_copy_256(Hacl_Streaming_MD_state_32 *
uint8_t *buf0 = scrut.buf;
uint64_t total_len0 = scrut.total_len;
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
memcpy(buf, buf0, 64U * sizeof (uint8_t));
uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t));
memcpy(block_state, block_state0, 8U * sizeof (uint32_t));
Hacl_Streaming_MD_state_32
s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
p[0U] = s;
return p;
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t));
Hacl_Streaming_Types_optional_32 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint32_t *block_state1 = block_state.v;
memcpy(block_state1, block_state0, 8U * sizeof (uint32_t));
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_32
s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf);
return NULL;
}
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**
@ -760,14 +868,67 @@ void Hacl_Hash_SHA2_hash_256(uint8_t *output, uint8_t *input, uint32_t input_len
Hacl_Streaming_MD_state_32 *Hacl_Hash_SHA2_malloc_224(void)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(64U, sizeof (uint8_t));
uint32_t *block_state = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t));
Hacl_Streaming_MD_state_32
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
p[0U] = s;
Hacl_Hash_SHA2_sha224_init(block_state);
return p;
if (buf == NULL)
{
return NULL;
}
uint8_t *buf1 = buf;
uint32_t *b = (uint32_t *)KRML_HOST_CALLOC(8U, sizeof (uint32_t));
Hacl_Streaming_Types_optional_32 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_32){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf1);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint32_t *block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_32
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_32
*p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_SHA2_sha224_init(block_state1);
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
void Hacl_Hash_SHA2_reset_224(Hacl_Streaming_MD_state_32 *state)
@ -858,14 +1019,67 @@ void Hacl_Hash_SHA2_hash_224(uint8_t *output, uint8_t *input, uint32_t input_len
Hacl_Streaming_MD_state_64 *Hacl_Hash_SHA2_malloc_512(void)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t));
uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t));
Hacl_Streaming_MD_state_64
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_64
*p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
p[0U] = s;
Hacl_Hash_SHA2_sha512_init(block_state);
return p;
if (buf == NULL)
{
return NULL;
}
uint8_t *buf1 = buf;
uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t));
Hacl_Streaming_Types_optional_64 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf1);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint64_t *block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_64
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_64
*p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_SHA2_sha512_init(block_state1);
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
/**
@ -881,15 +1095,67 @@ Hacl_Streaming_MD_state_64 *Hacl_Hash_SHA2_copy_512(Hacl_Streaming_MD_state_64 *
uint8_t *buf0 = scrut.buf;
uint64_t total_len0 = scrut.total_len;
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
memcpy(buf, buf0, 128U * sizeof (uint8_t));
uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t));
memcpy(block_state, block_state0, 8U * sizeof (uint64_t));
Hacl_Streaming_MD_state_64
s = { .block_state = block_state, .buf = buf, .total_len = total_len0 };
Hacl_Streaming_MD_state_64
*p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
p[0U] = s;
return p;
uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t));
Hacl_Streaming_Types_optional_64 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint64_t *block_state1 = block_state.v;
memcpy(block_state1, block_state0, 8U * sizeof (uint64_t));
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_64
s = { .block_state = block_state1, .buf = buf, .total_len = total_len0 };
Hacl_Streaming_MD_state_64
*p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf);
return NULL;
}
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
void Hacl_Hash_SHA2_reset_512(Hacl_Streaming_MD_state_64 *state)
@ -1172,14 +1438,67 @@ void Hacl_Hash_SHA2_hash_512(uint8_t *output, uint8_t *input, uint32_t input_len
Hacl_Streaming_MD_state_64 *Hacl_Hash_SHA2_malloc_384(void)
{
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(128U, sizeof (uint8_t));
uint64_t *block_state = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t));
Hacl_Streaming_MD_state_64
s = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_64
*p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
p[0U] = s;
Hacl_Hash_SHA2_sha384_init(block_state);
return p;
if (buf == NULL)
{
return NULL;
}
uint8_t *buf1 = buf;
uint64_t *b = (uint64_t *)KRML_HOST_CALLOC(8U, sizeof (uint64_t));
Hacl_Streaming_Types_optional_64 block_state;
if (b == NULL)
{
block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state = ((Hacl_Streaming_Types_optional_64){ .tag = Hacl_Streaming_Types_Some, .v = b });
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf1);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
uint64_t *block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Streaming_MD_state_64
s = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U };
Hacl_Streaming_MD_state_64
*p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
if (p != NULL)
{
p[0U] = s;
}
if (p == NULL)
{
KRML_HOST_FREE(block_state1);
KRML_HOST_FREE(buf1);
return NULL;
}
Hacl_Hash_SHA2_sha384_init(block_state1);
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
void Hacl_Hash_SHA2_reset_384(Hacl_Streaming_MD_state_64 *state)

3
Modules/_hacl/Hacl_Hash_SHA2.h
View file

@ -32,13 +32,12 @@ extern "C" {
#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;

402
Modules/_hacl/Hacl_Hash_SHA3.c
View file

@ -25,6 +25,9 @@
#include "internal/Hacl_Hash_SHA3.h"
#include "Hacl_Streaming_Types.h"
#include "internal/Hacl_Streaming_Types.h"
const
uint32_t
Hacl_Hash_SHA3_keccak_rotc[24U] =
@ -234,6 +237,12 @@ static uint32_t hash_len(Spec_Hash_Definitions_hash_alg a)
}
}
void Hacl_Hash_SHA3_init_(Spec_Hash_Definitions_hash_alg a, uint64_t *s)
{
KRML_MAYBE_UNUSED_VAR(a);
memset(s, 0U, 25U * sizeof (uint64_t));
}
void
Hacl_Hash_SHA3_update_multi_sha3(
Spec_Hash_Definitions_hash_alg a,
@ -545,6 +554,74 @@ Hacl_Hash_SHA3_update_last_sha3(
absorb_inner_32(b3, s);
}
static void squeeze(uint64_t *s, uint32_t rateInBytes, uint32_t outputByteLen, uint8_t *b)
{
for (uint32_t i0 = 0U; i0 < outputByteLen / rateInBytes; i0++)
{
uint8_t hbuf[256U] = { 0U };
uint64_t ws[32U] = { 0U };
memcpy(ws, s, 25U * sizeof (uint64_t));
for (uint32_t i = 0U; i < 32U; i++)
{
store64_le(hbuf + i * 8U, ws[i]);
}
uint8_t *b0 = b;
memcpy(b0 + i0 * rateInBytes, hbuf, rateInBytes * sizeof (uint8_t));
for (uint32_t i1 = 0U; i1 < 24U; i1++)
{
uint64_t _C[5U] = { 0U };
KRML_MAYBE_FOR5(i,
0U,
5U,
1U,
_C[i] = s[i + 0U] ^ (s[i + 5U] ^ (s[i + 10U] ^ (s[i + 15U] ^ s[i + 20U]))););
KRML_MAYBE_FOR5(i2,
0U,
5U,
1U,
uint64_t uu____0 = _C[(i2 + 1U) % 5U];
uint64_t _D = _C[(i2 + 4U) % 5U] ^ (uu____0 << 1U | uu____0 >> 63U);
KRML_MAYBE_FOR5(i, 0U, 5U, 1U, s[i2 + 5U * i] = s[i2 + 5U * i] ^ _D;););
uint64_t x = s[1U];
uint64_t current = x;
for (uint32_t i = 0U; i < 24U; i++)
{
uint32_t _Y = Hacl_Hash_SHA3_keccak_piln[i];
uint32_t r = Hacl_Hash_SHA3_keccak_rotc[i];
uint64_t temp = s[_Y];
uint64_t uu____1 = current;
s[_Y] = uu____1 << r | uu____1 >> (64U - r);
current = temp;
}
KRML_MAYBE_FOR5(i,
0U,
5U,
1U,
uint64_t v0 = s[0U + 5U * i] ^ (~s[1U + 5U * i] & s[2U + 5U * i]);
uint64_t v1 = s[1U + 5U * i] ^ (~s[2U + 5U * i] & s[3U + 5U * i]);
uint64_t v2 = s[2U + 5U * i] ^ (~s[3U + 5U * i] & s[4U + 5U * i]);
uint64_t v3 = s[3U + 5U * i] ^ (~s[4U + 5U * i] & s[0U + 5U * i]);
uint64_t v4 = s[4U + 5U * i] ^ (~s[0U + 5U * i] & s[1U + 5U * i]);
s[0U + 5U * i] = v0;
s[1U + 5U * i] = v1;
s[2U + 5U * i] = v2;
s[3U + 5U * i] = v3;
s[4U + 5U * i] = v4;);
uint64_t c = Hacl_Hash_SHA3_keccak_rndc[i1];
s[0U] = s[0U] ^ c;
}
}
uint32_t remOut = outputByteLen % rateInBytes;
uint8_t hbuf[256U] = { 0U };
uint64_t ws[32U] = { 0U };
memcpy(ws, s, 25U * sizeof (uint64_t));
for (uint32_t i = 0U; i < 32U; i++)
{
store64_le(hbuf + i * 8U, ws[i]);
}
memcpy(b + outputByteLen - remOut, hbuf, remOut * sizeof (uint8_t));
}
typedef struct hash_buf2_s
{
Hacl_Hash_SHA3_hash_buf fst;
@ -558,20 +635,88 @@ Spec_Hash_Definitions_hash_alg Hacl_Hash_SHA3_get_alg(Hacl_Hash_SHA3_state_t *s)
return block_state.fst;
}
typedef struct option___Spec_Hash_Definitions_hash_alg____uint64_t___s
{
Hacl_Streaming_Types_optional tag;
Hacl_Hash_SHA3_hash_buf v;
}
option___Spec_Hash_Definitions_hash_alg____uint64_t__;
Hacl_Hash_SHA3_state_t *Hacl_Hash_SHA3_malloc(Spec_Hash_Definitions_hash_alg a)
{
KRML_CHECK_SIZE(sizeof (uint8_t), block_len(a));
uint8_t *buf0 = (uint8_t *)KRML_HOST_CALLOC(block_len(a), sizeof (uint8_t));
uint64_t *buf = (uint64_t *)KRML_HOST_CALLOC(25U, sizeof (uint64_t));
Hacl_Hash_SHA3_hash_buf block_state = { .fst = a, .snd = buf };
Hacl_Hash_SHA3_state_t
s = { .block_state = block_state, .buf = buf0, .total_len = (uint64_t)0U };
Hacl_Hash_SHA3_state_t
*p = (Hacl_Hash_SHA3_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_SHA3_state_t));
p[0U] = s;
uint64_t *s1 = block_state.snd;
memset(s1, 0U, 25U * sizeof (uint64_t));
return p;
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(block_len(a), sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
uint8_t *buf1 = buf;
uint64_t *s = (uint64_t *)KRML_HOST_CALLOC(25U, sizeof (uint64_t));
option___Spec_Hash_Definitions_hash_alg____uint64_t__ block_state;
if (s == NULL)
{
block_state =
((option___Spec_Hash_Definitions_hash_alg____uint64_t__){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state =
(
(option___Spec_Hash_Definitions_hash_alg____uint64_t__){
.tag = Hacl_Streaming_Types_Some,
.v = { .fst = a, .snd = s }
}
);
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf1);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_SHA3_hash_buf block_state1 = block_state.v;
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Hash_SHA3_state_t
s0 = { .block_state = block_state1, .buf = buf1, .total_len = (uint64_t)0U };
Hacl_Hash_SHA3_state_t
*p = (Hacl_Hash_SHA3_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_SHA3_state_t));
if (p != NULL)
{
p[0U] = s0;
}
if (p == NULL)
{
uint64_t *s1 = block_state1.snd;
KRML_HOST_FREE(s1);
KRML_HOST_FREE(buf1);
return NULL;
}
Spec_Hash_Definitions_hash_alg a1 = block_state1.fst;
uint64_t *s1 = block_state1.snd;
Hacl_Hash_SHA3_init_(a1, s1);
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
void Hacl_Hash_SHA3_free(Hacl_Hash_SHA3_state_t *state)
@ -593,20 +738,79 @@ Hacl_Hash_SHA3_state_t *Hacl_Hash_SHA3_copy(Hacl_Hash_SHA3_state_t *state)
uint64_t total_len0 = scrut0.total_len;
Spec_Hash_Definitions_hash_alg i = block_state0.fst;
KRML_CHECK_SIZE(sizeof (uint8_t), block_len(i));
uint8_t *buf1 = (uint8_t *)KRML_HOST_CALLOC(block_len(i), sizeof (uint8_t));
memcpy(buf1, buf0, block_len(i) * sizeof (uint8_t));
uint64_t *buf = (uint64_t *)KRML_HOST_CALLOC(25U, sizeof (uint64_t));
Hacl_Hash_SHA3_hash_buf block_state = { .fst = i, .snd = buf };
hash_buf2 scrut = { .fst = block_state0, .snd = block_state };
uint64_t *s_dst = scrut.snd.snd;
uint64_t *s_src = scrut.fst.snd;
memcpy(s_dst, s_src, 25U * sizeof (uint64_t));
Hacl_Hash_SHA3_state_t
s = { .block_state = block_state, .buf = buf1, .total_len = total_len0 };
Hacl_Hash_SHA3_state_t
*p = (Hacl_Hash_SHA3_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_SHA3_state_t));
p[0U] = s;
return p;
uint8_t *buf = (uint8_t *)KRML_HOST_CALLOC(block_len(i), sizeof (uint8_t));
if (buf == NULL)
{
return NULL;
}
memcpy(buf, buf0, block_len(i) * sizeof (uint8_t));
uint64_t *s = (uint64_t *)KRML_HOST_CALLOC(25U, sizeof (uint64_t));
option___Spec_Hash_Definitions_hash_alg____uint64_t__ block_state;
if (s == NULL)
{
block_state =
((option___Spec_Hash_Definitions_hash_alg____uint64_t__){ .tag = Hacl_Streaming_Types_None });
}
else
{
block_state =
(
(option___Spec_Hash_Definitions_hash_alg____uint64_t__){
.tag = Hacl_Streaming_Types_Some,
.v = { .fst = i, .snd = s }
}
);
}
if (block_state.tag == Hacl_Streaming_Types_None)
{
KRML_HOST_FREE(buf);
return NULL;
}
if (block_state.tag == Hacl_Streaming_Types_Some)
{
Hacl_Hash_SHA3_hash_buf block_state1 = block_state.v;
hash_buf2 scrut = { .fst = block_state0, .snd = block_state1 };
uint64_t *s_dst = scrut.snd.snd;
uint64_t *s_src = scrut.fst.snd;
memcpy(s_dst, s_src, 25U * sizeof (uint64_t));
Hacl_Streaming_Types_optional k_ = Hacl_Streaming_Types_Some;
switch (k_)
{
case Hacl_Streaming_Types_None:
{
return NULL;
}
case Hacl_Streaming_Types_Some:
{
Hacl_Hash_SHA3_state_t
s0 = { .block_state = block_state1, .buf = buf, .total_len = total_len0 };
Hacl_Hash_SHA3_state_t
*p = (Hacl_Hash_SHA3_state_t *)KRML_HOST_MALLOC(sizeof (Hacl_Hash_SHA3_state_t));
if (p != NULL)
{
p[0U] = s0;
}
if (p == NULL)
{
uint64_t *s1 = block_state1.snd;
KRML_HOST_FREE(s1);
KRML_HOST_FREE(buf);
return NULL;
}
return p;
}
default:
{
KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
KRML_HOST_EXIT(253U);
}
}
}
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
__FILE__,
__LINE__,
"unreachable (pattern matches are exhaustive in F*)");
KRML_HOST_EXIT(255U);
}
void Hacl_Hash_SHA3_reset(Hacl_Hash_SHA3_state_t *state)
@ -616,8 +820,9 @@ void Hacl_Hash_SHA3_reset(Hacl_Hash_SHA3_state_t *state)
Hacl_Hash_SHA3_hash_buf block_state = scrut.block_state;
Spec_Hash_Definitions_hash_alg i = block_state.fst;
KRML_MAYBE_UNUSED_VAR(i);
Spec_Hash_Definitions_hash_alg a1 = block_state.fst;
uint64_t *s = block_state.snd;
memset(s, 0U, 25U * sizeof (uint64_t));
Hacl_Hash_SHA3_init_(a1, s);
Hacl_Hash_SHA3_state_t
tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)0U };
state[0U] = tmp;
@ -849,141 +1054,30 @@ digest_(
Hacl_Hash_SHA3_update_last_sha3(a10, s1, buf_last, r);
Spec_Hash_Definitions_hash_alg a11 = tmp_block_state.fst;
uint64_t *s = tmp_block_state.snd;
if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256)
bool sw;
switch (a11)
{
for (uint32_t i0 = 0U; i0 < l / block_len(a11); i0++)
{
uint8_t hbuf[256U] = { 0U };
uint64_t ws[32U] = { 0U };
memcpy(ws, s, 25U * sizeof (uint64_t));
for (uint32_t i = 0U; i < 32U; i++)
case Spec_Hash_Definitions_Shake128:
{
store64_le(hbuf + i * 8U, ws[i]);
sw = true;
break;
}
uint8_t *b0 = output;
uint8_t *uu____0 = hbuf;
memcpy(b0 + i0 * block_len(a11), uu____0, block_len(a11) * sizeof (uint8_t));
for (uint32_t i1 = 0U; i1 < 24U; i1++)
case Spec_Hash_Definitions_Shake256:
{
uint64_t _C[5U] = { 0U };
KRML_MAYBE_FOR5(i,
0U,
5U,
1U,
_C[i] = s[i + 0U] ^ (s[i + 5U] ^ (s[i + 10U] ^ (s[i + 15U] ^ s[i + 20U]))););
KRML_MAYBE_FOR5(i2,
0U,
5U,
1U,
uint64_t uu____1 = _C[(i2 + 1U) % 5U];
uint64_t _D = _C[(i2 + 4U) % 5U] ^ (uu____1 << 1U | uu____1 >> 63U);
KRML_MAYBE_FOR5(i, 0U, 5U, 1U, s[i2 + 5U * i] = s[i2 + 5U * i] ^ _D;););
uint64_t x = s[1U];
uint64_t current = x;
for (uint32_t i = 0U; i < 24U; i++)
{
uint32_t _Y = Hacl_Hash_SHA3_keccak_piln[i];
uint32_t r1 = Hacl_Hash_SHA3_keccak_rotc[i];
uint64_t temp = s[_Y];
uint64_t uu____2 = current;
s[_Y] = uu____2 << r1 | uu____2 >> (64U - r1);
current = temp;
}
KRML_MAYBE_FOR5(i,
0U,
5U,
1U,
uint64_t v0 = s[0U + 5U * i] ^ (~s[1U + 5U * i] & s[2U + 5U * i]);
uint64_t v1 = s[1U + 5U * i] ^ (~s[2U + 5U * i] & s[3U + 5U * i]);
uint64_t v2 = s[2U + 5U * i] ^ (~s[3U + 5U * i] & s[4U + 5U * i]);
uint64_t v3 = s[3U + 5U * i] ^ (~s[4U + 5U * i] & s[0U + 5U * i]);
uint64_t v4 = s[4U + 5U * i] ^ (~s[0U + 5U * i] & s[1U + 5U * i]);
s[0U + 5U * i] = v0;
s[1U + 5U * i] = v1;
s[2U + 5U * i] = v2;
s[3U + 5U * i] = v3;
s[4U + 5U * i] = v4;);
uint64_t c = Hacl_Hash_SHA3_keccak_rndc[i1];
s[0U] = s[0U] ^ c;
sw = true;
break;
}
}
uint32_t remOut = l % block_len(a11);
uint8_t hbuf[256U] = { 0U };
uint64_t ws[32U] = { 0U };
memcpy(ws, s, 25U * sizeof (uint64_t));
for (uint32_t i = 0U; i < 32U; i++)
{
store64_le(hbuf + i * 8U, ws[i]);
}
memcpy(output + l - remOut, hbuf, remOut * sizeof (uint8_t));
default:
{
sw = false;
}
}
if (sw)
{
squeeze(s, block_len(a11), l, output);
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++)
{
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;
}
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++)
{
store64_le(hbuf + i * 8U, ws[i]);
}
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

17
Modules/_hacl/Hacl_Hash_SHA3.h
View file

@ -32,26 +32,13 @@ extern "C" {
#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);

19
Modules/_hacl/Hacl_Streaming_Types.h
View file

@ -31,7 +31,7 @@ extern "C" {
#endif
#include <string.h>
#include "krml/types.h"
#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"
@ -56,24 +56,13 @@ typedef uint8_t Spec_Hash_Definitions_hash_alg;
#define Hacl_Streaming_Types_InvalidAlgorithm 1
#define Hacl_Streaming_Types_InvalidLength 2
#define Hacl_Streaming_Types_MaximumLengthExceeded 3
#define Hacl_Streaming_Types_OutOfMemory 4
typedef uint8_t Hacl_Streaming_Types_error_code;
typedef struct Hacl_Streaming_MD_state_32_s
{
uint32_t *block_state;
uint8_t *buf;
uint64_t total_len;
}
Hacl_Streaming_MD_state_32;
typedef struct Hacl_Streaming_MD_state_32_s Hacl_Streaming_MD_state_32;
typedef struct Hacl_Streaming_MD_state_64_s
{
uint64_t *block_state;
uint8_t *buf;
uint64_t total_len;
}
Hacl_Streaming_MD_state_64;
typedef struct Hacl_Streaming_MD_state_64_s Hacl_Streaming_MD_state_64;
#if defined(__cplusplus)
}

4
Modules/_hacl/Lib_Memzero0.c
View file

@ -12,7 +12,7 @@
#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
@ -43,7 +43,7 @@ void Lib_Memzero0_memzero0(void *dst, uint64_t len) {
SecureZeroMemory(dst, len_);
#elif defined(__APPLE__) && defined(__MACH__) && defined(MAC_OS_X_VERSION_MIN_REQUIRED) && (MAC_OS_X_VERSION_MIN_REQUIRED >= 1090)
memset_s(dst, len_, 0, len_);
#elif (defined(__linux__) && !defined(LINUX_NO_EXPLICIT_BZERO)) || defined(__FreeBSD__)
#elif (defined(__linux__) && !defined(LINUX_NO_EXPLICIT_BZERO)) || defined(__FreeBSD__) || defined(__OpenBSD__)
explicit_bzero(dst, len_);
#elif defined(__NetBSD__)
explicit_memset(dst, 0, len_);

2
Modules/_hacl/include/krml/FStar_UInt128_Verified.h
View file

@ -10,7 +10,7 @@
#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)

118
Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h
View file

@ -9,11 +9,31 @@
#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;
@ -36,6 +56,34 @@ static KRML_NOINLINE uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b)
return x_xor_q_ - 1ULL;
}
extern Prims_string FStar_UInt64_to_string(uint64_t uu___);
extern Prims_string FStar_UInt64_to_string_hex(uint64_t uu___);
extern Prims_string FStar_UInt64_to_string_hex_pad(uint64_t uu___);
extern uint64_t FStar_UInt64_of_string(Prims_string uu___);
extern krml_checked_int_t FStar_UInt32_n;
extern bool FStar_UInt32_uu___is_Mk(uint32_t projectee);
extern krml_checked_int_t FStar_UInt32___proj__Mk__item__v(uint32_t projectee);
extern krml_checked_int_t FStar_UInt32_v(uint32_t x);
typedef void *FStar_UInt32_fits;
extern uint32_t FStar_UInt32_uint_to_t(krml_checked_int_t x);
extern uint32_t FStar_UInt32_zero;
extern uint32_t FStar_UInt32_one;
extern uint32_t FStar_UInt32_minus(uint32_t a);
extern uint32_t FStar_UInt32_n_minus_one;
static KRML_NOINLINE uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b)
{
uint32_t x = a ^ b;
@ -58,6 +106,34 @@ static KRML_NOINLINE uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b)
return x_xor_q_ - 1U;
}
extern Prims_string FStar_UInt32_to_string(uint32_t uu___);
extern Prims_string FStar_UInt32_to_string_hex(uint32_t uu___);
extern Prims_string FStar_UInt32_to_string_hex_pad(uint32_t uu___);
extern uint32_t FStar_UInt32_of_string(Prims_string uu___);
extern krml_checked_int_t FStar_UInt16_n;
extern bool FStar_UInt16_uu___is_Mk(uint16_t projectee);
extern krml_checked_int_t FStar_UInt16___proj__Mk__item__v(uint16_t projectee);
extern krml_checked_int_t FStar_UInt16_v(uint16_t x);
typedef void *FStar_UInt16_fits;
extern uint16_t FStar_UInt16_uint_to_t(krml_checked_int_t x);
extern uint16_t FStar_UInt16_zero;
extern uint16_t FStar_UInt16_one;
extern uint16_t FStar_UInt16_minus(uint16_t a);
extern uint32_t FStar_UInt16_n_minus_one;
static KRML_NOINLINE uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b)
{
uint16_t x = (uint32_t)a ^ (uint32_t)b;
@ -80,6 +156,34 @@ static KRML_NOINLINE uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b)
return (uint32_t)x_xor_q_ - 1U;
}
extern Prims_string FStar_UInt16_to_string(uint16_t uu___);
extern Prims_string FStar_UInt16_to_string_hex(uint16_t uu___);
extern Prims_string FStar_UInt16_to_string_hex_pad(uint16_t uu___);
extern uint16_t FStar_UInt16_of_string(Prims_string uu___);
extern krml_checked_int_t FStar_UInt8_n;
extern bool FStar_UInt8_uu___is_Mk(uint8_t projectee);
extern krml_checked_int_t FStar_UInt8___proj__Mk__item__v(uint8_t projectee);
extern krml_checked_int_t FStar_UInt8_v(uint8_t x);
typedef void *FStar_UInt8_fits;
extern uint8_t FStar_UInt8_uint_to_t(krml_checked_int_t x);
extern uint8_t FStar_UInt8_zero;
extern uint8_t FStar_UInt8_one;
extern uint8_t FStar_UInt8_minus(uint8_t a);
extern uint32_t FStar_UInt8_n_minus_one;
static KRML_NOINLINE uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b)
{
uint8_t x = (uint32_t)a ^ (uint32_t)b;
@ -102,6 +206,16 @@ static KRML_NOINLINE uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b)
return (uint32_t)x_xor_q_ - 1U;
}
extern Prims_string FStar_UInt8_to_string(uint8_t uu___);
extern Prims_string FStar_UInt8_to_string_hex(uint8_t uu___);
extern Prims_string FStar_UInt8_to_string_hex_pad(uint8_t uu___);
extern uint8_t FStar_UInt8_of_string(Prims_string uu___);
typedef uint8_t FStar_UInt8_byte;
#define __FStar_UInt_8_16_32_64_H_DEFINED
#endif

32
Modules/_hacl/include/krml/internal/compat.h Normal file
View file

@ -0,0 +1,32 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 and MIT Licenses. */
#ifndef KRML_COMPAT_H
#define KRML_COMPAT_H
#include <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

54
Modules/_hacl/include/krml/internal/target.h
View file

@ -76,7 +76,7 @@
#endif
#ifndef KRML_MAYBE_UNUSED
# if defined(__GNUC__)
# if defined(__GNUC__) || defined(__clang__)
# define KRML_MAYBE_UNUSED __attribute__((unused))
# else
# define KRML_MAYBE_UNUSED
@ -84,7 +84,7 @@
#endif
#ifndef KRML_ATTRIBUTE_TARGET
# if defined(__GNUC__)
# if defined(__GNUC__) || defined(__clang__)
# define KRML_ATTRIBUTE_TARGET(x) __attribute__((target(x)))
# else
# define KRML_ATTRIBUTE_TARGET(x)
@ -92,10 +92,10 @@
#endif
#ifndef KRML_NOINLINE
# if defined(_MSC_VER)
# define KRML_NOINLINE __declspec(noinline)
# elif defined (__GNUC__)
# if defined (__GNUC__) || defined (__clang__)
# define KRML_NOINLINE __attribute__((noinline,unused))
# elif defined(_MSC_VER)
# define KRML_NOINLINE __declspec(noinline)
# elif defined (__SUNPRO_C)
# define KRML_NOINLINE __attribute__((noinline))
# else
@ -173,6 +173,32 @@
# endif
#endif
#ifndef KRML_HOST_TIME
# include <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).
*/
@ -195,6 +221,24 @@
} \
} while (0)
#if defined(_MSC_VER) && _MSC_VER < 1900
# define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) \
_snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
#else
# define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg)
#endif
#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4))
# define KRML_DEPRECATED(x) __attribute__((deprecated(x)))
#elif defined(__GNUC__)
/* deprecated attribute is not defined in GCC < 4.5. */
# define KRML_DEPRECATED(x)
#elif defined(__SUNPRO_C)
# define KRML_DEPRECATED(x) __attribute__((deprecated(x)))
#elif defined(_MSC_VER)
# define KRML_DEPRECATED(x) __declspec(deprecated(x))
#endif
/* Macros for prettier unrolling of loops */
#define KRML_LOOP1(i, n, x) { \
x \

106
Modules/_hacl/include/krml/internal/types.h Normal file
View file

@ -0,0 +1,106 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 and MIT Licenses. */
#ifndef KRML_TYPES_H
#define KRML_TYPES_H
#define KRML_VERIFIED_UINT128
#include <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

14
Modules/_hacl/include/krml/types.h
View file

@ -1,14 +0,0 @@
#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"

21
Modules/_hacl/internal/Hacl_Hash_Blake2b.h
View file

@ -31,11 +31,11 @@ extern "C" {
#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
@ -70,6 +70,23 @@ Hacl_Hash_Blake2b_update_last(
void Hacl_Hash_Blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash);
typedef struct Hacl_Hash_Blake2b_block_state_t_s
{
uint8_t fst;
uint8_t snd;
bool thd;
Hacl_Streaming_Types_two_pointers f3;
}
Hacl_Hash_Blake2b_block_state_t;
typedef struct Hacl_Hash_Blake2b_state_t_s
{
Hacl_Hash_Blake2b_block_state_t block_state;
uint8_t *buf;
uint64_t total_len;
}
Hacl_Hash_Blake2b_state_t;
#if defined(__cplusplus)
}
#endif

53
Modules/_hacl/internal/Hacl_Hash_Blake2b_Simd256.h
View file

@ -31,12 +31,10 @@ extern "C" {
#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"
@ -83,7 +81,54 @@ Hacl_Hash_Blake2b_Simd256_store_state256b_to_state32(
Lib_IntVector_Intrinsics_vec256 *st
);
Lib_IntVector_Intrinsics_vec256 *Hacl_Hash_Blake2b_Simd256_malloc_with_key(void);
Lib_IntVector_Intrinsics_vec256
*Hacl_Hash_Blake2b_Simd256_malloc_internal_state_with_key(void);
void
Hacl_Hash_Blake2b_Simd256_update_multi_no_inline(
Lib_IntVector_Intrinsics_vec256 *s,
FStar_UInt128_uint128 ev,
uint8_t *blocks,
uint32_t n
);
void
Hacl_Hash_Blake2b_Simd256_update_last_no_inline(
Lib_IntVector_Intrinsics_vec256 *s,
FStar_UInt128_uint128 prev,
uint8_t *input,
uint32_t input_len
);
void
Hacl_Hash_Blake2b_Simd256_copy_internal_state(
Lib_IntVector_Intrinsics_vec256 *src,
Lib_IntVector_Intrinsics_vec256 *dst
);
typedef struct Hacl_Hash_Blake2b_Simd256_two_2b_256_s
{
Lib_IntVector_Intrinsics_vec256 *fst;
Lib_IntVector_Intrinsics_vec256 *snd;
}
Hacl_Hash_Blake2b_Simd256_two_2b_256;
typedef struct Hacl_Hash_Blake2b_Simd256_block_state_t_s
{
uint8_t fst;
uint8_t snd;
bool thd;
Hacl_Hash_Blake2b_Simd256_two_2b_256 f3;
}
Hacl_Hash_Blake2b_Simd256_block_state_t;
typedef struct Hacl_Hash_Blake2b_Simd256_state_t_s
{
Hacl_Hash_Blake2b_Simd256_block_state_t block_state;
uint8_t *buf;
uint64_t total_len;
}
Hacl_Hash_Blake2b_Simd256_state_t;
#if defined(__cplusplus)
}

28
Modules/_hacl/internal/Hacl_Hash_Blake2s.h
View file

@ -31,12 +31,10 @@ extern "C" {
#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);
@ -64,6 +62,30 @@ Hacl_Hash_Blake2s_update_last(
void Hacl_Hash_Blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash);
typedef struct K____uint32_t___uint32_t__s
{
uint32_t *fst;
uint32_t *snd;
}
K____uint32_t___uint32_t_;
typedef struct Hacl_Hash_Blake2s_block_state_t_s
{
uint8_t fst;
uint8_t snd;
bool thd;
K____uint32_t___uint32_t_ f3;
}
Hacl_Hash_Blake2s_block_state_t;
typedef struct Hacl_Hash_Blake2s_state_t_s
{
Hacl_Hash_Blake2s_block_state_t block_state;
uint8_t *buf;
uint64_t total_len;
}
Hacl_Hash_Blake2s_state_t;
#if defined(__cplusplus)
}
#endif

53
Modules/_hacl/internal/Hacl_Hash_Blake2s_Simd128.h
View file

@ -31,12 +31,10 @@ extern "C" {
#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"
@ -83,7 +81,54 @@ Hacl_Hash_Blake2s_Simd128_load_state128s_from_state32(
uint32_t *st32
);
Lib_IntVector_Intrinsics_vec128 *Hacl_Hash_Blake2s_Simd128_malloc_with_key(void);
Lib_IntVector_Intrinsics_vec128
*Hacl_Hash_Blake2s_Simd128_malloc_internal_state_with_key(void);
void
Hacl_Hash_Blake2s_Simd128_update_multi_no_inline(
Lib_IntVector_Intrinsics_vec128 *s,
uint64_t ev,
uint8_t *blocks,
uint32_t n
);
void
Hacl_Hash_Blake2s_Simd128_update_last_no_inline(
Lib_IntVector_Intrinsics_vec128 *s,
uint64_t prev,
uint8_t *input,
uint32_t input_len
);
void
Hacl_Hash_Blake2s_Simd128_copy_internal_state(
Lib_IntVector_Intrinsics_vec128 *src,
Lib_IntVector_Intrinsics_vec128 *dst
);
typedef struct Hacl_Hash_Blake2s_Simd128_two_2s_128_s
{
Lib_IntVector_Intrinsics_vec128 *fst;
Lib_IntVector_Intrinsics_vec128 *snd;
}
Hacl_Hash_Blake2s_Simd128_two_2s_128;
typedef struct Hacl_Hash_Blake2s_Simd128_block_state_t_s
{
uint8_t fst;
uint8_t snd;
bool thd;
Hacl_Hash_Blake2s_Simd128_two_2s_128 f3;
}
Hacl_Hash_Blake2s_Simd128_block_state_t;
typedef struct Hacl_Hash_Blake2s_Simd128_state_t_s
{
Hacl_Hash_Blake2s_Simd128_block_state_t block_state;
uint8_t *buf;
uint64_t total_len;
}
Hacl_Hash_Blake2s_Simd128_state_t;
#if defined(__cplusplus)
}

3
Modules/_hacl/internal/Hacl_Hash_MD5.h
View file

@ -31,10 +31,11 @@ extern "C" {
#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);

2
Modules/_hacl/internal/Hacl_Hash_SHA1.h
View file

@ -31,7 +31,7 @@ extern "C" {
#endif
#include <string.h>
#include "krml/types.h"
#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"

3
Modules/_hacl/internal/Hacl_Hash_SHA2.h
View file

@ -31,11 +31,10 @@ extern "C" {
#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

20
Modules/_hacl/internal/Hacl_Hash_SHA3.h
View file

@ -31,10 +31,11 @@ extern "C" {
#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];
@ -43,6 +44,8 @@ extern const uint32_t Hacl_Hash_SHA3_keccak_piln[24U];
extern const uint64_t Hacl_Hash_SHA3_keccak_rndc[24U];
void Hacl_Hash_SHA3_init_(Spec_Hash_Definitions_hash_alg a, uint64_t *s);
void
Hacl_Hash_SHA3_update_multi_sha3(
Spec_Hash_Definitions_hash_alg a,
@ -59,6 +62,21 @@ Hacl_Hash_SHA3_update_last_sha3(
uint32_t input_len
);
typedef struct Hacl_Hash_SHA3_hash_buf_s
{
Spec_Hash_Definitions_hash_alg fst;
uint64_t *snd;
}
Hacl_Hash_SHA3_hash_buf;
typedef struct Hacl_Hash_SHA3_state_t_s
{
Hacl_Hash_SHA3_hash_buf block_state;
uint8_t *buf;
uint64_t total_len;
}
Hacl_Hash_SHA3_state_t;
#if defined(__cplusplus)
}
#endif

2
Modules/_hacl/internal/Hacl_Impl_Blake2_Constants.h
View file

@ -31,7 +31,7 @@ extern "C" {
#endif
#include <string.h>
#include "krml/types.h"
#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"

87
Modules/_hacl/internal/Hacl_Streaming_Types.h Normal file
View file

@ -0,0 +1,87 @@
/* MIT License
*
* Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
* Copyright (c) 2022-2023 HACL* Contributors
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*/
#ifndef __internal_Hacl_Streaming_Types_H
#define __internal_Hacl_Streaming_Types_H
#if defined(__cplusplus)
extern "C" {
#endif
#include <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

4
Modules/_hacl/libintvector.h
View file

@ -3,6 +3,8 @@
#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. */
@ -933,4 +935,6 @@ typedef vector128_8 vector128;
#endif
#endif
#endif // HACL_INTRINSICS_SHIMMED
#endif // __Vec_Intrin_H

42
Modules/_hacl/refresh.sh
View file

@ -22,7 +22,7 @@ fi
# Update this when updating to a new version after verifying that the changes
# the update brings in are good.
expected_hacl_star_rev=f218923ef2417d963d7efc7951593ae6aef613f7
expected_hacl_star_rev=322f6d58290e0ed7f4ecb84fcce12917aa0f594b
hacl_dir="$(realpath "$1")"
cd "$(dirname "$0")"
@ -58,6 +58,7 @@ dist_files=(
internal/Hacl_Hash_Blake2b_Simd256.h
internal/Hacl_Hash_Blake2s_Simd128.h
internal/Hacl_Impl_Blake2_Constants.h
internal/Hacl_Streaming_Types.h
Hacl_Hash_MD5.c
Hacl_Hash_SHA1.c
Hacl_Hash_SHA2.c
@ -74,7 +75,9 @@ dist_files=(
declare -a include_files
include_files=(
include/krml/lowstar_endianness.h
include/krml/internal/compat.h
include/krml/internal/target.h
include/krml/internal/types.h
)
declare -a lib_files
@ -110,32 +113,12 @@ fi
readarray -t all_files < <(find . -name '*.h' -or -name '*.c')
# types.h originally contains a complex series of if-defs and auxiliary type
# definitions; here, we just need a proper uint128 type in scope
# is a simple wrapper that defines the uint128 type
cat > include/krml/types.h <<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
@ -143,14 +126,7 @@ $sed -i -z 's!\(extern\|typedef\)[^;]*;\n\n!!g' include/krml/FStar_UInt_8_16_32_
$sed -i 's!#include.*Hacl_Krmllib.h"!!g' "${all_files[@]}"
# Use globally unique names for the Hacl_ C APIs to avoid linkage conflicts.
$sed -i -z 's!#include <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)

2
PCbuild/pythoncore.vcxproj
View file

@ -100,7 +100,7 @@
<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>