From 516b6f31cd2fc769cd6f301028497deee48897b6 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Tue, 29 Oct 2024 20:36:16 +0100 Subject: [PATCH] cleanup --- Cargo.lock | 189 ++++++++++-------- Cargo.toml | 3 +- libcrux-intrinsics/Cargo.toml | 3 - libcrux-ml-dsa/Cargo.toml | 2 - libcrux-sha3/proofs/fstar/extraction/Makefile | 1 - .../fstar/extraction/Libcrux_platform.X86.fst | 69 ------- 6 files changed, 107 insertions(+), 160 deletions(-) delete mode 100644 libcrux-sha3/proofs/fstar/extraction/Makefile delete mode 100644 sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fst diff --git a/Cargo.lock b/Cargo.lock index dc42f03bd..830df0dcd 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -84,9 +84,9 @@ checksum = "7d5a26814d8dcb93b0e5a0ff3c6d80a8843bafb21b39e8e18a6f05471870e110" [[package]] name = "autocfg" -version = "1.4.0" +version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" +checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" [[package]] name = "base16ct" @@ -126,9 +126,9 @@ dependencies = [ [[package]] name = "bindgen" -version = "0.69.5" +version = "0.69.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "271383c67ccabffb7381723dea0672a673f292304fcb45c01cc648c7a8d58088" +checksum = "a00dc851838a2120612785d195287475a3ac45514741da670b735818822129a0" dependencies = [ "bitflags", "cexpr", @@ -143,7 +143,7 @@ dependencies = [ "regex", "rustc-hash", "shlex", - "syn 2.0.82", + "syn 2.0.77", "which", ] @@ -191,9 +191,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.1.31" +version = "1.1.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c2e7962b54006dcfcc61cb72735f4d89bb97061dd6a7ed882ec6b8ee53714c6f" +checksum = "07b1695e2c7e8fc85310cde85aeaab7e3097f593c91d209d3f9df76c928100f0" dependencies = [ "jobserver", "libc", @@ -290,9 +290,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.20" +version = "4.5.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b97f376d85a664d5837dbae44bf546e6477a679ff6610010f17276f686d867e8" +checksum = "b0956a43b323ac1afaffc053ed5c4b7c1f1800bacd1683c353aabbb752515dd3" dependencies = [ "clap_builder", "clap_derive", @@ -300,9 +300,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.20" +version = "4.5.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "19bc80abd44e4bed93ca373a0704ccbd1b710dc5749406201bb018272808dc54" +checksum = "4d72166dd41634086d5803a47eb71ae740e61d84709c36f3c34110173db3961b" dependencies = [ "anstream", "anstyle", @@ -319,7 +319,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", ] [[package]] @@ -483,7 +483,7 @@ checksum = "f46882e17999c6cc590af592290432be3bce0428cb0d5f8b6715e4dc7b383eb3" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", ] [[package]] @@ -711,10 +711,10 @@ dependencies = [ [[package]] name = "hax-lib" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax/#001a27e20755b65d6a780243a125076fe90e6d0b" +version = "0.1.0-pre.1" +source = "git+https://github.com/hacspec/hax/#c2093b4963099522c65f5cd42b96d6433afb0617" dependencies = [ - "hax-lib-macros 0.1.0-alpha.1 (git+https://github.com/hacspec/hax/)", + "hax-lib-macros 0.1.0-pre.1", "num-bigint", "num-traits", ] @@ -729,20 +729,33 @@ dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", ] [[package]] name = "hax-lib-macros" version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax/#001a27e20755b65d6a780243a125076fe90e6d0b" +source = "git+https://github.com/hacspec/hax?branch=main#001a27e20755b65d6a780243a125076fe90e6d0b" dependencies = [ - "hax-lib-macros-types 0.1.0-alpha.1 (git+https://github.com/hacspec/hax/)", + "hax-lib-macros-types 0.1.0-alpha.1 (git+https://github.com/hacspec/hax?branch=main)", "paste", "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", +] + +[[package]] +name = "hax-lib-macros" +version = "0.1.0-pre.1" +source = "git+https://github.com/hacspec/hax/#c2093b4963099522c65f5cd42b96d6433afb0617" +dependencies = [ + "hax-lib-macros-types 0.1.0-pre.1", + "paste", + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.77", ] [[package]] @@ -760,7 +773,19 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax/#001a27e20755b65d6a780243a125076fe90e6d0b" +source = "git+https://github.com/hacspec/hax?branch=main#001a27e20755b65d6a780243a125076fe90e6d0b" +dependencies = [ + "proc-macro2", + "quote", + "serde", + "serde_json", + "uuid", +] + +[[package]] +name = "hax-lib-macros-types" +version = "0.1.0-pre.1" +source = "git+https://github.com/hacspec/hax/#c2093b4963099522c65f5cd42b96d6433afb0617" dependencies = [ "proc-macro2", "quote", @@ -884,9 +909,9 @@ dependencies = [ [[package]] name = "js-sys" -version = "0.3.72" +version = "0.3.70" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6a88f1bda2bd75b0452a14784937d796722fdebfe50df998aeb3f0b7603019a9" +checksum = "1868808506b929d7b0cfa8f75951347aa71bb21144b7791bae35d9bccfcfe37a" dependencies = [ "wasm-bindgen", ] @@ -924,9 +949,9 @@ dependencies = [ [[package]] name = "libc" -version = "0.2.161" +version = "0.2.158" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9489c2807c139ffd9c1794f4af0ebe86a828db53ecdc7fea2111d0fed085d1" +checksum = "d8adc4bb1803a324070e64a98ae98f38934d91957a99cfb3a43dcbc01bc56439" [[package]] name = "libcrux" @@ -934,6 +959,8 @@ version = "0.0.2-beta.2" dependencies = [ "clap", "getrandom", + "hax-lib 0.1.0-alpha.1", + "hax-lib-macros 0.1.0-alpha.1 (git+https://github.com/hacspec/hax?branch=main)", "hex", "libcrux", "libcrux-ecdh", @@ -1006,9 +1033,6 @@ dependencies = [ [[package]] name = "libcrux-intrinsics" version = "0.0.2-beta.2" -dependencies = [ - "hax-lib 0.1.0-alpha.1 (git+https://github.com/hacspec/hax/?branch=fstar-proof-lib-small-additions)", -] [[package]] name = "libcrux-kem" @@ -1027,7 +1051,6 @@ name = "libcrux-ml-dsa" version = "0.0.2-beta.2" dependencies = [ "criterion", - "hax-lib 0.1.0-alpha.1 (git+https://github.com/hacspec/hax/?branch=fstar-proof-lib-small-additions)", "hex", "libcrux-intrinsics", "libcrux-platform", @@ -1043,7 +1066,7 @@ name = "libcrux-ml-kem" version = "0.0.2-beta.2" dependencies = [ "criterion", - "hax-lib 0.1.0-alpha.1 (git+https://github.com/hacspec/hax/)", + "hax-lib 0.1.0-pre.1", "hex", "libcrux-intrinsics", "libcrux-platform", @@ -1089,7 +1112,7 @@ version = "0.0.2-beta.2" dependencies = [ "cavp", "criterion", - "hax-lib 0.1.0-alpha.1 (git+https://github.com/hacspec/hax/)", + "hax-lib 0.1.0-pre.1", "hex", "libcrux-intrinsics", "libcrux-platform", @@ -1202,9 +1225,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.20.2" +version = "1.19.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" +checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" [[package]] name = "oorandom" @@ -1220,9 +1243,9 @@ checksum = "c08d65885ee38876c4f86fa503fb49d7b507c2b62552df7c70b2fce627e06381" [[package]] name = "openssl" -version = "0.10.68" +version = "0.10.66" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6174bc48f102d208783c2c84bf931bb75927a617866870de8a4ea85597f871f5" +checksum = "9529f4786b70a3e8c61e11179af17ab6188ad8d0ded78c5529441ed39d4bd9c1" dependencies = [ "bitflags", "cfg-if", @@ -1241,14 +1264,14 @@ checksum = "a948666b637a0f465e8564c73e89d4dde00d72d4d473cc972f390fc3dcee7d9c" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", ] [[package]] name = "openssl-sys" -version = "0.9.104" +version = "0.9.103" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "45abf306cbf99debc8195b66b7346498d7b10c210de50418b5ccd7ceba08c741" +checksum = "7f9e8deee91df40a943c71b917e5874b951d32a802526c85721ce3b776c929d6" dependencies = [ "cc", "libc", @@ -1403,12 +1426,12 @@ dependencies = [ [[package]] name = "prettyplease" -version = "0.2.24" +version = "0.2.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "910d41a655dac3b764f1ade94821093d3610248694320cd072303a8eedcf221d" +checksum = "479cf940fbbb3426c32c5d5176f62ad57549a0bb84773423ba8be9d089f5faba" dependencies = [ "proc-macro2", - "syn 2.0.82", + "syn 2.0.77", ] [[package]] @@ -1446,9 +1469,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.88" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7c3a7fc5db1e57d5a779a352c8cdb57b29aa4c40cc69c3a68a7fedc815fbf2f9" +checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" dependencies = [ "unicode-ident", ] @@ -1536,9 +1559,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.11.0" +version = "1.10.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "38200e5ee88914975b69f657f0801b6f6dccafd44fd9326302a4aaeecfacb1d8" +checksum = "4219d74c6b67a3654a9fbebc4b419e22126d13d2f3c4a07ee0cb61ff79a79619" dependencies = [ "aho-corasick", "memchr", @@ -1548,9 +1571,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.4.8" +version = "0.4.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "368758f23274712b504848e9d5a6f010445cc8b87a7cdb4d7cbee666c1288da3" +checksum = "38caf58cc5ef2fed281f89292ef23f6365465ed9a41b7a7754eb4e26496c92df" dependencies = [ "aho-corasick", "memchr", @@ -1559,9 +1582,9 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.8.5" +version = "0.8.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2b15c43186be67a4fd63bee50d0303afffcef381492ebe2c5d87f324e1b8815c" +checksum = "7a66a03ae7c801facd77a29370b4faec201768915ac14a721ba36f20bc9c209b" [[package]] name = "rfc6979" @@ -1659,29 +1682,29 @@ checksum = "61697e0a1c7e512e84a621326239844a24d8207b4669b41bc18b32ea5cbf988b" [[package]] name = "serde" -version = "1.0.211" +version = "1.0.210" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ac55e59090389fb9f0dd9e0f3c09615afed1d19094284d0b200441f13550793" +checksum = "c8e3592472072e6e22e0a54d5904d9febf8508f65fb8552499a1abc7d1078c3a" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.211" +version = "1.0.210" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "54be4f245ce16bc58d57ef2716271d0d4519e0f6defa147f6e081005bcb278ff" +checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", ] [[package]] name = "serde_json" -version = "1.0.132" +version = "1.0.128" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d726bfaff4b320266d395898905d0eba0345aae23b54aee3a737e260fd46db03" +checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8" dependencies = [ "itoa", "memchr", @@ -1773,9 +1796,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.82" +version = "2.0.77" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "83540f837a8afc019423a8edb95b52a8effe46957ee402287f4292fae35be021" +checksum = "9f35bcdf61fd8e7be6caf75f429fdca8beb3ed76584befb503b1569faee373ed" dependencies = [ "proc-macro2", "quote", @@ -1837,9 +1860,9 @@ checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" [[package]] name = "uuid" -version = "1.11.0" +version = "1.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8c5f0a0af699448548ad1a2fbf920fb4bee257eae39953ba95cb84891a0446a" +checksum = "81dfa00651efa65069b0b6b651f4aaa31ba9e3c3ce0137aaad053604ee7e0314" dependencies = [ "getrandom", ] @@ -1874,9 +1897,9 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "wasm-bindgen" -version = "0.2.95" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "128d1e363af62632b8eb57219c8fd7877144af57558fb2ef0368d0087bddeb2e" +checksum = "a82edfc16a6c469f5f44dc7b571814045d60404b55a0ee849f9bcfa2e63dd9b5" dependencies = [ "cfg-if", "once_cell", @@ -1885,24 +1908,24 @@ dependencies = [ [[package]] name = "wasm-bindgen-backend" -version = "0.2.95" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb6dd4d3ca0ddffd1dd1c9c04f94b868c37ff5fac97c30b97cff2d74fce3a358" +checksum = "9de396da306523044d3302746f1208fa71d7532227f15e347e2d93e4145dd77b" dependencies = [ "bumpalo", "log", "once_cell", "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", "wasm-bindgen-shared", ] [[package]] name = "wasm-bindgen-futures" -version = "0.4.45" +version = "0.4.43" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cc7ec4f8827a71586374db3e87abdb5a2bb3a15afed140221307c3ec06b1f63b" +checksum = "61e9300f63a621e96ed275155c108eb6f843b6a26d053f122ab69724559dc8ed" dependencies = [ "cfg-if", "js-sys", @@ -1912,9 +1935,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.95" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e79384be7f8f5a9dd5d7167216f022090cf1f9ec128e6e6a482a2cb5c5422c56" +checksum = "585c4c91a46b072c92e908d99cb1dcdf95c5218eeb6f3bf1efa991ee7a68cccf" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -1922,28 +1945,28 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.95" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26c6ab57572f7a24a4985830b120de1594465e5d500f24afe89e16b4e833ef68" +checksum = "afc340c74d9005395cf9dd098506f7f44e38f2b4a21c6aaacf9a105ea5e1e836" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", "wasm-bindgen-backend", "wasm-bindgen-shared", ] [[package]] name = "wasm-bindgen-shared" -version = "0.2.95" +version = "0.2.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "65fc09f10666a9f147042251e0dda9c18f166ff7de300607007e96bdebc1068d" +checksum = "c62a0a307cb4a311d3a07867860911ca130c3494e8c2719593806c08bc5d0484" [[package]] name = "wasm-bindgen-test" -version = "0.3.45" +version = "0.3.43" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d381749acb0943d357dcbd8f0b100640679883fcdeeef04def49daf8d33a5426" +checksum = "68497a05fb21143a08a7d24fc81763384a3072ee43c44e86aad1744d6adef9d9" dependencies = [ "console_error_panic_hook", "js-sys", @@ -1956,20 +1979,20 @@ dependencies = [ [[package]] name = "wasm-bindgen-test-macro" -version = "0.3.45" +version = "0.3.43" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c97b2ef2c8d627381e51c071c2ab328eac606d3f69dd82bcbca20a9e389d95f0" +checksum = "4b8220be1fa9e4c889b30fd207d4906657e7e90b12e0e6b0c8b8d8709f5de021" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", ] [[package]] name = "web-sys" -version = "0.3.72" +version = "0.3.70" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f6488b90108c040df0fe62fa815cbdee25124641df01814dd7282749234c6112" +checksum = "26fdeaafd9bd129f65e7c031593c24d62186301e0c72c8978fa1678be7d532c0" dependencies = [ "js-sys", "wasm-bindgen", @@ -2120,7 +2143,7 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", ] [[package]] @@ -2140,5 +2163,5 @@ checksum = "ce36e65b0d2999d2aafac989fb249189a141aee1f53c612c1f37d72631959f69" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.77", ] diff --git a/Cargo.toml b/Cargo.toml index aef7bc2b2..561c1ce67 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -77,8 +77,7 @@ getrandom = { version = "0.2", features = ["js"], optional = true } # When using the hax toolchain, we have more dependencies. # This is only required when doing proofs. -#[target.'cfg(hax)'.dependencies] -[workspace.dependencies] +[target.'cfg(hax)'.dependencies] hax-lib-macros = { git = "https://github.com/hacspec/hax", branch = "main" } hax-lib = { git = "https://github.com/hacspec/hax/", branch = "fstar-proof-lib-small-additions" } diff --git a/libcrux-intrinsics/Cargo.toml b/libcrux-intrinsics/Cargo.toml index 5cacc5bee..144f7137d 100644 --- a/libcrux-intrinsics/Cargo.toml +++ b/libcrux-intrinsics/Cargo.toml @@ -10,9 +10,6 @@ readme.workspace = true description = "Libcrux intrinsics crate" exclude = ["/proofs"] -[dependencies] -hax-lib.workspace = true - [features] simd128 = [] simd256 = [] diff --git a/libcrux-ml-dsa/Cargo.toml b/libcrux-ml-dsa/Cargo.toml index bd57d33c7..d451f7c23 100644 --- a/libcrux-ml-dsa/Cargo.toml +++ b/libcrux-ml-dsa/Cargo.toml @@ -20,8 +20,6 @@ libcrux-sha3 = { version = "0.0.2-beta.2", path = "../libcrux-sha3" } libcrux-intrinsics = { version = "0.0.2-beta.2", path = "../libcrux-intrinsics" } libcrux-platform = { version = "0.0.2-beta.2", path = "../sys/platform" } -hax-lib.workspace = true - [dev-dependencies] rand = { version = "0.8" } hex = { version = "0.4.3", features = ["serde"] } diff --git a/libcrux-sha3/proofs/fstar/extraction/Makefile b/libcrux-sha3/proofs/fstar/extraction/Makefile deleted file mode 100644 index ec420d509..000000000 --- a/libcrux-sha3/proofs/fstar/extraction/Makefile +++ /dev/null @@ -1 +0,0 @@ -include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.template diff --git a/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fst b/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fst deleted file mode 100644 index 0e4db4e49..000000000 --- a/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fst +++ /dev/null @@ -1,69 +0,0 @@ -module Libcrux_platform.X86 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" -open Core -open FStar.Mul - -(* item error backend: (reject_Unsafe) ExplicitRejection { reason: "a node of kind [Unsafe] have been found in the AST" } -Last available AST for this item: - -#[inline(never)] -#[inline(always)] -#[cfg(any(target_arch = "x86", target_arch = "x86_64"))] -#[allow(non_upper_case_globals)] -#[no_std()] -#[feature(register_tool)] -#[register_tool(_hax)] -unsafe fn init__cpuid(leaf: int) -> core::core_arch::x86::cpuid::t_CpuidResult { - rust_primitives::hax::dropped_body -} - - -Last AST: -/** print_rust: pitem: not implemented (item: { Concrete_ident.T.def_id = - { Concrete_ident.Imported.krate = "libcrux_platform"; - path = - [{ Concrete_ident.Imported.data = (Concrete_ident.Imported.TypeNs "x86"); - disambiguator = 0 }; - { Concrete_ident.Imported.data = - (Concrete_ident.Imported.ValueNs "init"); disambiguator = 0 }; - { Concrete_ident.Imported.data = - (Concrete_ident.Imported.ValueNs "cpuid"); disambiguator = 0 } - ] - }; - kind = Concrete_ident.Kind.Value }) */ -const _: () = (); - *) - -(* item error backend: (reject_Unsafe) ExplicitRejection { reason: "a node of kind [Unsafe] have been found in the AST" } -Last available AST for this item: - -#[inline(never)] -#[inline(always)] -#[cfg(any(target_arch = "x86", target_arch = "x86_64"))] -#[allow(non_upper_case_globals)] -#[no_std()] -#[feature(register_tool)] -#[register_tool(_hax)] -unsafe fn init__cpuid_count( - leaf: int, - sub_leaf: int, -) -> core::core_arch::x86::cpuid::t_CpuidResult { - rust_primitives::hax::dropped_body -} - - -Last AST: -/** print_rust: pitem: not implemented (item: { Concrete_ident.T.def_id = - { Concrete_ident.Imported.krate = "libcrux_platform"; - path = - [{ Concrete_ident.Imported.data = (Concrete_ident.Imported.TypeNs "x86"); - disambiguator = 0 }; - { Concrete_ident.Imported.data = - (Concrete_ident.Imported.ValueNs "init"); disambiguator = 0 }; - { Concrete_ident.Imported.data = - (Concrete_ident.Imported.ValueNs "cpuid_count"); disambiguator = 0 } - ] - }; - kind = Concrete_ident.Kind.Value }) */ -const _: () = (); - *)