From 0fc11d0192b3c434280f36914a5feeed67ae9e1e Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 15 Dec 2024 19:42:26 +0000 Subject: [PATCH] restoring F* extraction --- Cargo.lock | 88 ++++--- .../Libcrux_intrinsics.Avx2_extract.fsti | 12 + libcrux-intrinsics/src/arm64_extract.rs | 18 +- .../Libcrux_ml_kem.Hash_functions.Avx2.fsti | 2 +- .../Libcrux_ml_kem.Hash_functions.Neon.fsti | 2 +- ...ibcrux_ml_kem.Hash_functions.Portable.fsti | 2 +- .../Libcrux_ml_kem.Ind_cca.Unpacked.fst | 34 ++- .../Libcrux_ml_kem.Ind_cca.Unpacked.fsti | 24 +- .../Libcrux_ml_kem.Ind_cpa.Unpacked.fst | 18 ++ .../Libcrux_ml_kem.Ind_cpa.Unpacked.fsti | 8 + .../extraction/Libcrux_ml_kem.Polynomial.fst | 48 +++- .../extraction/Libcrux_ml_kem.Polynomial.fsti | 30 ++- .../extraction/Libcrux_ml_kem.Variant.fst | 6 +- .../extraction/Libcrux_ml_kem.Variant.fsti | 10 +- .../extraction/Libcrux_ml_kem.Vector.Avx2.fst | 12 + .../Libcrux_ml_kem.Vector.Avx2.fsti | 6 + ...Libcrux_ml_kem.Vector.Neon.Vector_type.fst | 12 + ...ibcrux_ml_kem.Vector.Neon.Vector_type.fsti | 6 + ...rux_ml_kem.Vector.Portable.Vector_type.fst | 12 + ...ux_ml_kem.Vector.Portable.Vector_type.fsti | 6 + libcrux-ml-kem/src/constant_time_ops.rs | 4 +- libcrux-ml-kem/src/hash_functions.rs | 6 +- libcrux-ml-kem/src/ind_cca.rs | 232 +++++++++--------- libcrux-ml-kem/src/ind_cpa.rs | 4 +- libcrux-ml-kem/src/invert_ntt.rs | 2 +- libcrux-ml-kem/src/ntt.rs | 20 +- libcrux-ml-kem/src/serialize.rs | 8 +- libcrux-ml-kem/src/utils.rs | 12 +- libcrux-ml-kem/src/vector/avx2.rs | 30 +-- libcrux-ml-kem/src/vector/avx2/arithmetic.rs | 8 +- libcrux-ml-kem/src/vector/portable.rs | 54 ++-- .../src/vector/portable/arithmetic.rs | 36 +-- .../src/vector/portable/compress.rs | 28 +-- libcrux-ml-kem/src/vector/portable/ntt.rs | 5 +- libcrux-ml-kem/src/vector/traits.rs | 66 ++--- libcrux-sha3/src/generic_keccak.rs | 4 +- .../extraction/Libcrux_platform.X86.fsti | 6 + 37 files changed, 525 insertions(+), 356 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 94f450b74..823e87153 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1,6 +1,6 @@ # This file is automatically @generated by Cargo. # It is not intended for manual editing. -version = 3 +version = 4 [[package]] name = "aead" @@ -191,9 +191,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.2.2" +version = "1.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f34d93e62b03caf570cccc334cbc6c2fceca82f39211051345108adcba3eebdc" +checksum = "9157bbaa6b165880c27a4293a474c91cdcf265cc68cc829bf10be0964a391caf" dependencies = [ "jobserver", "libc", @@ -290,9 +290,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.21" +version = "4.5.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fb3b4b9e5a7c7514dfa52869339ee98b3156b0bfb4e8a77c4ff4babb64b1604f" +checksum = "3135e7ec2ef7b10c6ed8950f0f792ed96ee093fa088608f1c76e569722700c84" dependencies = [ "clap_builder", "clap_derive", @@ -300,9 +300,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.21" +version = "4.5.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b17a95aa67cc7b5ebd32aa5370189aa0d79069ef1c64ce893bd30fb24bff20ec" +checksum = "30582fc632330df2bd26877bde0c1f4470d57c582bbc070376afcd04d8cb4838" dependencies = [ "anstream", "anstyle", @@ -324,9 +324,9 @@ dependencies = [ [[package]] name = "clap_lex" -version = "0.7.3" +version = "0.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "afb84c814227b90d6895e01398aee0d8033c00e7466aca416fb6a8e0eb19d8a7" +checksum = "f46ad14479a25103f283c0f10005961cf086d8dc42205bb44c46ac563475dca6" [[package]] name = "classic-mceliece-rust" @@ -698,7 +698,7 @@ dependencies = [ [[package]] name = "hax-lib" version = "0.1.0-rc.1" -source = "git+https://github.com/hacspec/hax/#de59826b832befc82905286d052c8a961c31f3cd" +source = "git+https://github.com/hacspec/hax/#62f7bfabe31ac2dcdbda867e3879b49b080fd292" dependencies = [ "hax-lib-macros", "num-bigint", @@ -708,7 +708,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" version = "0.1.0-rc.1" -source = "git+https://github.com/hacspec/hax/#de59826b832befc82905286d052c8a961c31f3cd" +source = "git+https://github.com/hacspec/hax/#62f7bfabe31ac2dcdbda867e3879b49b080fd292" dependencies = [ "hax-lib-macros-types", "paste", @@ -721,7 +721,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" version = "0.1.0-rc.1" -source = "git+https://github.com/hacspec/hax/#de59826b832befc82905286d052c8a961c31f3cd" +source = "git+https://github.com/hacspec/hax/#62f7bfabe31ac2dcdbda867e3879b49b080fd292" dependencies = [ "proc-macro2", "quote", @@ -845,9 +845,9 @@ dependencies = [ [[package]] name = "js-sys" -version = "0.3.74" +version = "0.3.76" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a865e038f7f6ed956f788f0d7d60c541fff74c7bd74272c5d4cf15c63743e705" +checksum = "6717b6b5b077764fb5966237269cb3c64edddde4b14ce42647430a78ced9e7b7" dependencies = [ "once_cell", "wasm-bindgen", @@ -886,9 +886,9 @@ dependencies = [ [[package]] name = "libc" -version = "0.2.167" +version = "0.2.168" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09d6582e104315a817dff97f75133544b2e094ee22447d2acf4a74e189ba06fc" +checksum = "5aaeb2981e0606ca11d79718f8bb01164f1d6ed75080182d3abf017e6d244b6d" [[package]] name = "libcrux" @@ -1625,15 +1625,15 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.41" +version = "0.38.42" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7f649912bc1495e167a6edee79151c84b1bad49748cb4f1f1167f459f6224f6" +checksum = "f93dc38ecbab2eb790ff964bb77fa94faf256fd3e73285fd7ba0903b76bedb85" dependencies = [ "bitflags", "errno", "libc", "linux-raw-sys", - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] @@ -1673,24 +1673,24 @@ dependencies = [ [[package]] name = "semver" -version = "1.0.23" +version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61697e0a1c7e512e84a621326239844a24d8207b4669b41bc18b32ea5cbf988b" +checksum = "3cb6eb87a131f756572d7fb904f6e7b68633f09cca868c5df1c4b8d1a694bbba" [[package]] name = "serde" -version = "1.0.215" +version = "1.0.216" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f" +checksum = "0b9781016e935a97e8beecf0c933758c97a5520d32930e460142b4cd80c6338e" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.215" +version = "1.0.216" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" +checksum = "46f859dbbf73865c6627ed570e78961cd3ac92407a2d117204c49232485da55e" dependencies = [ "proc-macro2", "quote", @@ -1894,9 +1894,9 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "wasm-bindgen" -version = "0.2.97" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d15e63b4482863c109d70a7b8706c1e364eb6ea449b201a76c5b89cedcec2d5c" +checksum = "a474f6281d1d70c17ae7aa6a613c87fce69a127e2624002df63dcb39d6cf6396" dependencies = [ "cfg-if", "once_cell", @@ -1905,13 +1905,12 @@ dependencies = [ [[package]] name = "wasm-bindgen-backend" -version = "0.2.97" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8d36ef12e3aaca16ddd3f67922bc63e48e953f126de60bd33ccc0101ef9998cd" +checksum = "5f89bb38646b4f81674e8f5c3fb81b562be1fd936d84320f3264486418519c79" dependencies = [ "bumpalo", "log", - "once_cell", "proc-macro2", "quote", "syn 2.0.90", @@ -1920,9 +1919,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-futures" -version = "0.4.47" +version = "0.4.49" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9dfaf8f50e5f293737ee323940c7d8b08a66a95a419223d9f41610ca08b0833d" +checksum = "38176d9b44ea84e9184eff0bc34cc167ed044f816accfe5922e54d84cf48eca2" dependencies = [ "cfg-if", "js-sys", @@ -1933,9 +1932,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.97" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "705440e08b42d3e4b36de7d66c944be628d579796b8090bfa3471478a2260051" +checksum = "2cc6181fd9a7492eef6fef1f33961e3695e4579b9872a6f7c83aee556666d4fe" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -1943,9 +1942,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.97" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "98c9ae5a76e46f4deecd0f0255cc223cfa18dc9b261213b8aa0c7b36f61b3f1d" +checksum = "30d7a95b763d3c45903ed6c81f156801839e5ee968bb07e534c44df0fcd330c2" dependencies = [ "proc-macro2", "quote", @@ -1956,19 +1955,18 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.97" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ee99da9c5ba11bd675621338ef6fa52296b76b83305e9b6e5c77d4c286d6d49" +checksum = "943aab3fdaaa029a6e0271b35ea10b72b943135afe9bffca82384098ad0e06a6" [[package]] name = "wasm-bindgen-test" -version = "0.3.47" +version = "0.3.49" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3d919bb60ebcecb9160afee6c71b43a58a4f0517a2de0054cd050d02cec08201" +checksum = "c61d44563646eb934577f2772656c7ad5e9c90fac78aa8013d776fcdaf24625d" dependencies = [ "js-sys", "minicov", - "once_cell", "scoped-tls", "wasm-bindgen", "wasm-bindgen-futures", @@ -1977,9 +1975,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-test-macro" -version = "0.3.47" +version = "0.3.49" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "222ebde6ea87fbfa6bdd2e9f1fd8a91d60aee5db68792632176c4e16a74fc7d8" +checksum = "54171416ce73aa0b9c377b51cc3cb542becee1cd678204812e8392e5b0e4a031" dependencies = [ "proc-macro2", "quote", @@ -1988,9 +1986,9 @@ dependencies = [ [[package]] name = "web-sys" -version = "0.3.74" +version = "0.3.76" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a98bc3c33f0fe7e59ad7cd041b89034fa82a7c2d4365ca538dda6cdaf513863c" +checksum = "04dd7223427d52553d3702c004d3b2fe07c148165faa56313cb00211e31c12bc" dependencies = [ "js-sys", "wasm-bindgen", diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti index 290b679a5..e597dd2fd 100644 --- a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti +++ b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti @@ -9,10 +9,22 @@ unfold type t_Vec128 = bit_vec 128 val vec128_as_i16x8 (x: bit_vec 128) : t_Array i16 (sz 8) let get_lane128 (v: bit_vec 128) (i:nat{i < 8}) = Seq.index (vec128_as_i16x8 v) i +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_3:Core.Clone.t_Clone t_Vec128 + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_2:Core.Marker.t_Copy t_Vec128 + unfold type t_Vec256 = bit_vec 256 val vec256_as_i16x16 (x: bit_vec 256) : t_Array i16 (sz 16) let get_lane (v: bit_vec 256) (i:nat{i < 16}) = Seq.index (vec256_as_i16x16 v) i +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl:Core.Clone.t_Clone t_Vec256 + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1:Core.Marker.t_Copy t_Vec256 + val mm256_abs_epi32 (a: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True) val mm256_add_epi16 (lhs rhs: t_Vec256) diff --git a/libcrux-intrinsics/src/arm64_extract.rs b/libcrux-intrinsics/src/arm64_extract.rs index d41241275..9f651b6c0 100644 --- a/libcrux-intrinsics/src/arm64_extract.rs +++ b/libcrux-intrinsics/src/arm64_extract.rs @@ -3,23 +3,23 @@ #![allow(non_camel_case_types, unsafe_code, unused_variables)] -#[hax_lib::opaque_type] +#[hax_lib::opaque] pub type _uint16x4_t = u8; -#[hax_lib::opaque_type] +#[hax_lib::opaque] pub type _int16x4_t = u8; -#[hax_lib::opaque_type] +#[hax_lib::opaque] pub type _int16x8_t = u8; -#[hax_lib::opaque_type] +#[hax_lib::opaque] pub type _uint8x16_t = u8; -#[hax_lib::opaque_type] +#[hax_lib::opaque] pub type _uint16x8_t = u8; -#[hax_lib::opaque_type] +#[hax_lib::opaque] pub type _uint32x4_t = u8; -#[hax_lib::opaque_type] +#[hax_lib::opaque] pub type _int32x4_t = u8; -#[hax_lib::opaque_type] +#[hax_lib::opaque] pub type _uint64x2_t = u8; -#[hax_lib::opaque_type] +#[hax_lib::opaque] pub type _int64x2_t = u8; #[inline(always)] diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti index 336b75faa..c830bb8f6 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti @@ -6,7 +6,7 @@ open FStar.Mul /// The state. /// It\'s only used for SHAKE128. /// All other functions don\'t actually use any members. -val t_Simd256Hash:Type0 +val t_Simd256Hash:eqtype [@@ FStar.Tactics.Typeclasses.tcinstance] val impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd256Hash v_K diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti index 7b7869c77..1a7c6875a 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti @@ -6,7 +6,7 @@ open FStar.Mul /// The state. /// It\'s only used for SHAKE128. /// All other functions don\'t actually use any members. -val t_Simd128Hash:Type0 +val t_Simd128Hash:eqtype [@@ FStar.Tactics.Typeclasses.tcinstance] val impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd128Hash v_K diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti index 37255d0af..661213d58 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti @@ -6,7 +6,7 @@ open FStar.Mul /// The state. /// It\'s only used for SHAKE128. /// All other functions don\'t actually use any members. -val t_PortableHash (v_K: usize) : Type0 +val t_PortableHash (v_K: usize) : eqtype [@@ FStar.Tactics.Typeclasses.tcinstance] val impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash (t_PortableHash v_K) v_K diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst index e726f4578..ed2632129 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst @@ -19,7 +19,7 @@ let impl_4__private_key (v_K: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_MlKemKeyPairUnpacked v_K v_Vector) = self.f_private_key @@ -28,11 +28,29 @@ let impl_4__public_key (v_K: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_MlKemKeyPairUnpacked v_K v_Vector) = self.f_public_key +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_2': + v_K: usize -> + #v_Vector: Type0 -> + {| i1: Core.Clone.t_Clone v_Vector |} -> + {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + -> Core.Clone.t_Clone (t_MlKemPublicKeyUnpacked v_K v_Vector) + +let impl_2 + (v_K: usize) + (#v_Vector: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_Vector) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i2: + Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) + = impl_2' v_K #v_Vector #i1 #i2 + #push-options "--z3rlimit 200" let transpose_a @@ -352,7 +370,7 @@ let impl_4__from_private_key (v_SECRET_KEY_SIZE v_CPA_SECRET_KEY_SIZE v_PUBLIC_KEY_SIZE v_BYTES_PER_RING_ELEMENT v_T_AS_NTT_ENCODED_SIZE: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (private_key: Libcrux_ml_kem.Types.t_MlKemPrivateKey v_SECRET_KEY_SIZE) = @@ -592,7 +610,7 @@ let impl_4__serialized_public_key_mut (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_MlKemKeyPairUnpacked v_K v_Vector) (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) @@ -616,7 +634,7 @@ let impl_3__serialized (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_MlKemPublicKeyUnpacked v_K v_Vector) = @@ -637,7 +655,7 @@ let impl_4__serialized_public_key (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_MlKemKeyPairUnpacked v_K v_Vector) = @@ -831,7 +849,7 @@ let impl_4__serialized_private_key_mut (v_CPA_PRIVATE_KEY_SIZE v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_RANKED_BYTES_PER_RING_ELEMENT: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_MlKemKeyPairUnpacked v_K v_Vector) (serialized: Libcrux_ml_kem.Types.t_MlKemPrivateKey v_PRIVATE_KEY_SIZE) @@ -870,7 +888,7 @@ let impl_4__serialized_private_key (v_CPA_PRIVATE_KEY_SIZE v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_RANKED_BYTES_PER_RING_ELEMENT: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_MlKemKeyPairUnpacked v_K v_Vector) = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti index 85ebcd273..a6eb033b1 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti @@ -43,7 +43,7 @@ type t_MlKemKeyPairUnpacked val impl_4__private_key (v_K: usize) (#v_Vector: Type0) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemKeyPairUnpacked v_K v_Vector) : Prims.Pure (t_MlKemPrivateKeyUnpacked v_K v_Vector) Prims.l_True (fun _ -> Prims.l_True) @@ -51,10 +51,18 @@ val impl_4__private_key val impl_4__public_key (v_K: usize) (#v_Vector: Type0) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemKeyPairUnpacked v_K v_Vector) : Prims.Pure (t_MlKemPublicKeyUnpacked v_K v_Vector) Prims.l_True (fun _ -> Prims.l_True) +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_2 + (v_K: usize) + (#v_Vector: Type0) + {| i1: Core.Clone.t_Clone v_Vector |} + {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + : Core.Clone.t_Clone (t_MlKemPublicKeyUnpacked v_K v_Vector) + val transpose_a (v_K: usize) (#v_Vector: Type0) @@ -121,7 +129,7 @@ val impl_4__from_private_key (#v_Vector: Type0) (v_SECRET_KEY_SIZE v_CPA_SECRET_KEY_SIZE v_PUBLIC_KEY_SIZE v_BYTES_PER_RING_ELEMENT v_T_AS_NTT_ENCODED_SIZE: usize) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (private_key: Libcrux_ml_kem.Types.t_MlKemPrivateKey v_SECRET_KEY_SIZE) : Prims.Pure (t_MlKemKeyPairUnpacked v_K v_Vector) (requires @@ -238,7 +246,7 @@ val impl_4__serialized_public_key_mut (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemKeyPairUnpacked v_K v_Vector) (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) @@ -269,7 +277,7 @@ val impl_3__serialized (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemPublicKeyUnpacked v_K v_Vector) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) (requires @@ -297,7 +305,7 @@ val impl_4__serialized_public_key (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemKeyPairUnpacked v_K v_Vector) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) (requires @@ -355,7 +363,7 @@ val impl_4__serialized_private_key_mut (#v_Vector: Type0) (v_CPA_PRIVATE_KEY_SIZE v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_RANKED_BYTES_PER_RING_ELEMENT: usize) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemKeyPairUnpacked v_K v_Vector) (serialized: Libcrux_ml_kem.Types.t_MlKemPrivateKey v_PRIVATE_KEY_SIZE) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPrivateKey v_PRIVATE_KEY_SIZE) @@ -372,7 +380,7 @@ val impl_4__serialized_private_key (#v_Vector: Type0) (v_CPA_PRIVATE_KEY_SIZE v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_RANKED_BYTES_PER_RING_ELEMENT: usize) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemKeyPairUnpacked v_K v_Vector) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPrivateKey v_PRIVATE_KEY_SIZE) (requires diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.Unpacked.fst index ef0c39424..1f6cee7c2 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.Unpacked.fst @@ -9,6 +9,24 @@ let _ = let open Libcrux_ml_kem.Vector.Traits in () +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_2': + v_K: usize -> + #v_Vector: Type0 -> + {| i1: Core.Clone.t_Clone v_Vector |} -> + {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + -> Core.Clone.t_Clone (t_IndCpaPublicKeyUnpacked v_K v_Vector) + +let impl_2 + (v_K: usize) + (#v_Vector: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_Vector) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i2: + Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) + = impl_2' v_K #v_Vector #i1 #i2 + [@@ FStar.Tactics.Typeclasses.tcinstance] let impl (v_K: usize) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.Unpacked.fsti index d627f74c8..1f7036f4f 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.Unpacked.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.Unpacked.fsti @@ -23,6 +23,14 @@ type t_IndCpaPublicKeyUnpacked f_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K } +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_2 + (v_K: usize) + (#v_Vector: Type0) + {| i1: Core.Clone.t_Clone v_Vector |} + {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + : Core.Clone.t_Clone (t_IndCpaPublicKeyUnpacked v_K v_Vector) + [@@ FStar.Tactics.Typeclasses.tcinstance] val impl (v_K: usize) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst index ce5d113e4..4cad63238 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst @@ -14,6 +14,38 @@ let zeta (i: usize) = let _:Prims.unit = admit () (* Panic freedom *) in result +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl': + #v_Vector: Type0 -> + {| i1: Core.Clone.t_Clone v_Vector |} -> + {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + -> Core.Clone.t_Clone (t_PolynomialRingElement v_Vector) + +let impl + (#v_Vector: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_Vector) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i2: + Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) + = impl' #v_Vector #i1 #i2 + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_1': + #v_Vector: Type0 -> + {| i1: Core.Marker.t_Copy v_Vector |} -> + {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + -> Core.Marker.t_Copy (t_PolynomialRingElement v_Vector) + +let impl_1 + (#v_Vector: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_Vector) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i2: + Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) + = impl_1' #v_Vector #i1 #i2 + #push-options "--admit_smt_queries true" let add_error_reduce @@ -71,7 +103,7 @@ let add_error_reduce let impl_2__add_error_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self error: t_PolynomialRingElement v_Vector) = @@ -141,7 +173,7 @@ let add_message_error_reduce let impl_2__add_message_error_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self message result: t_PolynomialRingElement v_Vector) = add_message_error_reduce #v_Vector self message result @@ -201,7 +233,7 @@ let add_standard_error_reduce let impl_2__add_standard_error_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self error: t_PolynomialRingElement v_Vector) = @@ -253,7 +285,7 @@ let poly_barrett_reduce let impl_2__poly_barrett_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_PolynomialRingElement v_Vector) = @@ -316,7 +348,7 @@ let subtract_reduce let impl_2__subtract_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self b: t_PolynomialRingElement v_Vector) = subtract_reduce #v_Vector self b @@ -409,7 +441,7 @@ let from_i16_array let impl_2__from_i16_array (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (a: t_Slice i16) = from_i16_array #v_Vector a @@ -464,7 +496,7 @@ let ntt_multiply let impl_2__ntt_multiply (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self rhs: t_PolynomialRingElement v_Vector) = ntt_multiply #v_Vector self rhs @@ -517,7 +549,7 @@ let impl_2__add_to_ring_element (#v_Vector: Type0) (v_K: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self rhs: t_PolynomialRingElement v_Vector) = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti index 0ddfb6ea7..7f60ace38 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti @@ -62,6 +62,20 @@ let v_VECTORS_IN_RING_ELEMENT: usize = Libcrux_ml_kem.Constants.v_COEFFICIENTS_IN_RING_ELEMENT /! Libcrux_ml_kem.Vector.Traits.v_FIELD_ELEMENTS_IN_VECTOR +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl + (#v_Vector: Type0) + {| i1: Core.Clone.t_Clone v_Vector |} + {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + : Core.Clone.t_Clone (t_PolynomialRingElement v_Vector) + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1 + (#v_Vector: Type0) + {| i1: Core.Marker.t_Copy v_Vector |} + {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + : Core.Marker.t_Copy (t_PolynomialRingElement v_Vector) + val add_error_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} @@ -70,7 +84,7 @@ val add_error_reduce val impl_2__add_error_reduce (#v_Vector: Type0) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self error: t_PolynomialRingElement v_Vector) : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) @@ -82,7 +96,7 @@ val add_message_error_reduce val impl_2__add_message_error_reduce (#v_Vector: Type0) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self message result: t_PolynomialRingElement v_Vector) : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) @@ -94,7 +108,7 @@ val add_standard_error_reduce val impl_2__add_standard_error_reduce (#v_Vector: Type0) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self error: t_PolynomialRingElement v_Vector) : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) @@ -106,7 +120,7 @@ val poly_barrett_reduce val impl_2__poly_barrett_reduce (#v_Vector: Type0) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_PolynomialRingElement v_Vector) : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) @@ -118,7 +132,7 @@ val subtract_reduce val impl_2__subtract_reduce (#v_Vector: Type0) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self b: t_PolynomialRingElement v_Vector) : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) @@ -145,7 +159,7 @@ val from_i16_array val impl_2__from_i16_array (#v_Vector: Type0) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (a: t_Slice i16) : Prims.Pure (t_PolynomialRingElement v_Vector) (requires @@ -180,7 +194,7 @@ val ntt_multiply val impl_2__ntt_multiply (#v_Vector: Type0) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self rhs: t_PolynomialRingElement v_Vector) : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) @@ -198,6 +212,6 @@ val add_to_ring_element val impl_2__add_to_ring_element (#v_Vector: Type0) (v_K: usize) - {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self rhs: t_PolynomialRingElement v_Vector) : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fst index 90987de0b..dcdeb0041 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fst @@ -96,7 +96,7 @@ let impl: t_Variant t_MlKem = (v_K: usize) (#v_Hasher: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i4: + i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) (key_generation_seed: t_Slice u8) -> @@ -107,7 +107,7 @@ let impl: t_Variant t_MlKem = (v_K: usize) (#v_Hasher: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i4: + i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) (key_generation_seed: t_Slice u8) (res: t_Array u8 (sz 64)) @@ -120,7 +120,7 @@ let impl: t_Variant t_MlKem = (v_K: usize) (#v_Hasher: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i4: + i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) (key_generation_seed: t_Slice u8) -> diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fsti index 590a79d4c..9f3dc29f3 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fsti @@ -73,13 +73,13 @@ class t_Variant (v_Self: Type0) = { f_cpa_keygen_seed_pre: v_K: usize -> #v_Hasher: Type0 -> - {| i4: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> seed: t_Slice u8 -> pred: Type0{(Core.Slice.impl__len #u8 seed <: usize) =. sz 32 ==> pred}; f_cpa_keygen_seed_post: v_K: usize -> #v_Hasher: Type0 -> - {| i4: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> seed: t_Slice u8 -> res: t_Array u8 (sz 64) -> pred: @@ -90,11 +90,11 @@ class t_Variant (v_Self: Type0) = { f_cpa_keygen_seed: v_K: usize -> #v_Hasher: Type0 -> - {| i4: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> x0: t_Slice u8 -> Prims.Pure (t_Array u8 (sz 64)) - (f_cpa_keygen_seed_pre v_K #v_Hasher #i4 x0) - (fun result -> f_cpa_keygen_seed_post v_K #v_Hasher #i4 x0 result) + (f_cpa_keygen_seed_pre v_K #v_Hasher #i3 x0) + (fun result -> f_cpa_keygen_seed_post v_K #v_Hasher #i3 x0 result) } [@@ FStar.Tactics.Typeclasses.tcinstance] diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst index a352090e8..b0b8981ad 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst @@ -158,6 +158,18 @@ let ntt_multiply (lhs rhs: t_SIMD256Vector) (zeta0 zeta1 zeta2 zeta3: i16) = #pop-options +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_1': Core.Clone.t_Clone t_SIMD256Vector + +let impl_1 = impl_1' + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_2': Core.Marker.t_Copy t_SIMD256Vector + +let impl_2 = impl_2' + #push-options "--admit_smt_queries true" let serialize_10_ (vector: t_SIMD256Vector) = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti index 952ee56eb..3ba81f3eb 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti @@ -159,6 +159,12 @@ val ntt_multiply (lhs rhs: t_SIMD256Vector) (zeta0 zeta1 zeta2 zeta3: i16) let out:t_SIMD256Vector = out in Spec.Utils.is_i16b_array 3328 (repr out)) +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1:Core.Clone.t_Clone t_SIMD256Vector + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_2:Core.Marker.t_Copy t_SIMD256Vector + val serialize_10_ (vector: t_SIMD256Vector) : Prims.Pure (t_Array u8 (sz 20)) (requires Spec.MLKEM.serialize_pre 10 (repr vector)) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Vector_type.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Vector_type.fst index 9b4625de3..761d0a4b3 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Vector_type.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Vector_type.fst @@ -47,6 +47,18 @@ let from_i16_array (array: t_Slice i16) = let _:Prims.unit = admit () (* Panic freedom *) in result +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl': Core.Clone.t_Clone t_SIMD128Vector + +let impl = impl' + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_1': Core.Marker.t_Copy t_SIMD128Vector + +let impl_1 = impl_1' + let to_i16_array (v: t_SIMD128Vector) = let out:t_Array i16 (sz 16) = Rust_primitives.Hax.repeat 0s (sz 16) in let out:t_Array i16 (sz 16) = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Vector_type.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Vector_type.fsti index 2a950fdf6..ce6c9b299 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Vector_type.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Neon.Vector_type.fsti @@ -26,6 +26,12 @@ val from_i16_array (array: t_Slice i16) let result:t_SIMD128Vector = result in repr result == array) +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl:Core.Clone.t_Clone t_SIMD128Vector + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1:Core.Marker.t_Copy t_SIMD128Vector + val to_i16_array (v: t_SIMD128Vector) : Prims.Pure (t_Array i16 (sz 16)) Prims.l_True diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Vector_type.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Vector_type.fst index 177b2fe04..70c80f4e5 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Vector_type.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Vector_type.fst @@ -25,5 +25,17 @@ let from_i16_array (array: t_Slice i16) = let to_i16_array (x: t_PortableVector) = x.f_elements +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl': Core.Clone.t_Clone t_PortableVector + +let impl = impl' + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_1': Core.Marker.t_Copy t_PortableVector + +let impl_1 = impl_1' + let zero (_: Prims.unit) = { f_elements = Rust_primitives.Hax.repeat 0s (sz 16) } <: t_PortableVector diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Vector_type.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Vector_type.fsti index 782ad70eb..0d4b6268a 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Vector_type.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Vector_type.fsti @@ -21,6 +21,12 @@ val to_i16_array (x: t_PortableVector) let result:t_Array i16 (sz 16) = result in result == x.f_elements) +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl:Core.Clone.t_Clone t_PortableVector + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1:Core.Marker.t_Copy t_PortableVector + val zero: Prims.unit -> Prims.Pure t_PortableVector Prims.l_True diff --git a/libcrux-ml-kem/src/constant_time_ops.rs b/libcrux-ml-kem/src/constant_time_ops.rs index 33c7c858f..b462a2cff 100644 --- a/libcrux-ml-kem/src/constant_time_ops.rs +++ b/libcrux-ml-kem/src/constant_time_ops.rs @@ -69,10 +69,10 @@ fn compare(lhs: &[u8], rhs: &[u8]) -> u8 { for i in 0..lhs.len() { hax_lib::loop_invariant!(|i: usize| { fstar!( - "v $i <= Seq.length $lhs /\ + r#"v $i <= Seq.length $lhs /\ (if (Seq.slice $lhs 0 (v $i) = Seq.slice $rhs 0 (v $i)) then $r == 0uy - else ~ ($r == 0uy))" + else ~ ($r == 0uy))"# ) }); let nr = r | (lhs[i] ^ rhs[i]); diff --git a/libcrux-ml-kem/src/hash_functions.rs b/libcrux-ml-kem/src/hash_functions.rs index d0acbab30..572664cff 100644 --- a/libcrux-ml-kem/src/hash_functions.rs +++ b/libcrux-ml-kem/src/hash_functions.rs @@ -78,7 +78,7 @@ pub(crate) mod portable { /// /// It's only used for SHAKE128. /// All other functions don't actually use any members. - #[cfg_attr(hax, hax_lib::opaque_type)] + #[cfg_attr(hax, hax_lib::opaque)] pub(crate) struct PortableHash { shake128_state: [KeccakState; K], } @@ -237,7 +237,7 @@ pub(crate) mod avx2 { /// /// It's only used for SHAKE128. /// All other functions don't actually use any members. - #[cfg_attr(hax, hax_lib::opaque_type)] + #[cfg_attr(hax, hax_lib::opaque)] pub(crate) struct Simd256Hash { shake128_state: KeccakState, } @@ -487,7 +487,7 @@ pub(crate) mod neon { /// /// It's only used for SHAKE128. /// All other functions don't actually use any members. - #[cfg_attr(hax, hax_lib::opaque_type)] + #[cfg_attr(hax, hax_lib::opaque)] pub(crate) struct Simd128Hash { shake128_state: [KeccakState; 2], } diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs index 843d347f2..916ff78a3 100644 --- a/libcrux-ml-kem/src/ind_cca.rs +++ b/libcrux-ml-kem/src/ind_cca.rs @@ -37,10 +37,10 @@ pub(crate) mod instantiations; #[inline(always)] #[hax_lib::fstar::options("--z3rlimit 150")] -#[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $SERIALIZED_KEY_LEN == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\\ - ${private_key.len()} == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\\ - ${public_key.len()} == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ +#[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $SERIALIZED_KEY_LEN == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\ + ${private_key.len()} == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\ + ${public_key.len()} == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ ${implicit_rejection_value.len()} == Spec.MLKEM.v_SHARED_SECRET_SIZE"#))] #[hax_lib::ensures(|result| fstar!(r#"${serialized}_future == Seq.append $private_key ( Seq.append $public_key ( @@ -67,7 +67,7 @@ fn serialize_kem_secret_key_mut< .copy_from_slice(implicit_rejection_value); hax_lib::fstar!( - r#"let open Spec.Utils in + "let open Spec.Utils in assert (Seq.slice serialized 0 (v #usize_inttype (Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K)) `Seq.equal` $private_key); assert (Seq.slice serialized (v #usize_inttype (Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K)) (v #usize_inttype (Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K +! Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K)) `Seq.equal` $public_key); @@ -85,16 +85,16 @@ fn serialize_kem_secret_key_mut< Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE +! Spec.MLKEM.v_SHARED_SECRET_SIZE)) == $implicit_rejection_value); - lemma_slice_append_4 serialized $private_key $public_key (Libcrux_ml_kem.Hash_functions.f_H #$:Hasher #$K $public_key) $implicit_rejection_value"# + lemma_slice_append_4 serialized $private_key $public_key (Libcrux_ml_kem.Hash_functions.f_H #$:Hasher #$K $public_key) $implicit_rejection_value" ); } #[inline(always)] #[hax_lib::fstar::options("--z3rlimit 150")] -#[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $SERIALIZED_KEY_LEN == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\\ - ${private_key.len()} == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\\ - ${public_key.len()} == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ +#[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $SERIALIZED_KEY_LEN == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\ + ${private_key.len()} == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\ + ${public_key.len()} == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ ${implicit_rejection_value.len()} == Spec.MLKEM.v_SHARED_SECRET_SIZE"#))] #[hax_lib::ensures(|result| fstar!(r#"$result == Seq.append $private_key ( Seq.append $public_key ( @@ -122,8 +122,8 @@ fn serialize_kem_secret_key>( private_key: &MlKemPrivateKey, @@ -192,12 +192,12 @@ fn validate_private_key_only (${result}.f_sk.f_value, ${result}.f_pk.f_value) == expected"#))] @@ -243,18 +243,18 @@ fn generate_keypair< } #[hax_lib::fstar::options("--z3rlimit 300")] -#[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\ - $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ - $T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE $K /\\ - $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\\ - $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\\ - $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\ - $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\ - $C1_BLOCK_SIZE == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\ - $ETA1 == Spec.MLKEM.v_ETA1 $K /\\ - $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\ - $ETA2 == Spec.MLKEM.v_ETA2 $K /\\ +#[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ + $T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE $K /\ + $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\ + $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\ + $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\ + $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\ + $C1_BLOCK_SIZE == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\ + $ETA1 == Spec.MLKEM.v_ETA1 $K /\ + $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\ + $ETA2 == Spec.MLKEM.v_ETA2 $K /\ $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K"#))] #[hax_lib::ensures(|result| fstar!(r#"let (expected, valid) = Spec.MLKEM.ind_cca_encapsulate $K ${public_key}.f_value $randomness in valid ==> (${result}._1.f_value, ${result}._2) == expected"#))] @@ -316,21 +316,21 @@ fn encapsulate< /// This code verifies on some machines, runs out of memory on others #[hax_lib::fstar::options("--z3rlimit 500")] -#[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $SECRET_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\\ - $CPA_SECRET_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\\ - $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ - $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\ - $T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE $K /\\ - $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\\ - $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\\ - $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\ - $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\ - $C1_BLOCK_SIZE == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\ - $ETA1 == Spec.MLKEM.v_ETA1 $K /\\ - $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\ - $ETA2 == Spec.MLKEM.v_ETA2 $K /\\ - $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\\ +#[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $SECRET_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\ + $CPA_SECRET_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ + $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\ + $T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE $K /\ + $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\ + $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\ + $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\ + $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\ + $C1_BLOCK_SIZE == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\ + $ETA1 == Spec.MLKEM.v_ETA1 $K /\ + $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\ + $ETA2 == Spec.MLKEM.v_ETA2 $K /\ + $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\ $IMPLICIT_REJECTION_HASH_INPUT_SIZE == Spec.MLKEM.v_IMPLICIT_REJECTION_HASH_INPUT_SIZE $K"#))] #[hax_lib::ensures(|result| fstar!(r#"let (expected, valid) = Spec.MLKEM.ind_cca_decapsulate $K ${private_key}.f_value ${ciphertext}.f_value in valid ==> $result == expected"#))] @@ -483,16 +483,16 @@ pub(crate) mod unpacked { /// Generate an unpacked key from a serialized key. #[hax_lib::requires( - fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + fstar!(r#"Spec.MLKEM.is_rank $K /\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ $T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE $K"#) )] #[hax_lib::ensures(|result| fstar!(r#"let (public_key_hash, (seed, (deserialized_pk, (matrix_A, valid)))) = Spec.MLKEM.ind_cca_unpack_public_key $K ${public_key}.f_value in (valid ==> - Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${unpacked_public_key}_future.f_ind_cpa_public_key.f_A == matrix_A) /\\ - Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${unpacked_public_key}_future.f_ind_cpa_public_key.f_t_as_ntt == deserialized_pk /\\ - ${unpacked_public_key}_future.f_ind_cpa_public_key.f_seed_for_A == seed /\\ + Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${unpacked_public_key}_future.f_ind_cpa_public_key.f_A == matrix_A) /\ + Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${unpacked_public_key}_future.f_ind_cpa_public_key.f_t_as_ntt == deserialized_pk /\ + ${unpacked_public_key}_future.f_ind_cpa_public_key.f_seed_for_A == seed /\ ${unpacked_public_key}_future.f_public_key_hash == public_key_hash"#)) ] #[inline(always)] @@ -531,9 +531,9 @@ pub(crate) mod unpacked { impl MlKemPublicKeyUnpacked { /// Get the serialized public key. #[inline(always)] - #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ - $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ (forall (i:nat). i < v $K ==> Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_ind_cpa_public_key.f_t_as_ntt i))"#))] @@ -560,9 +560,9 @@ pub(crate) mod unpacked { /// Get the serialized public key. #[inline(always)] - #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ - $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ (forall (i:nat). i < v $K ==> Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_ind_cpa_public_key.f_t_as_ntt i))"#))] @@ -602,11 +602,11 @@ pub(crate) mod unpacked { /// Take a serialized private key and generate an unpacked key pair from it. #[inline(always)] - #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - v_SECRET_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE v_K /\\ - v_CPA_SECRET_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE v_K /\\ - v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\\ - v_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\\ + #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + v_SECRET_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE v_K /\ + v_CPA_SECRET_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE v_K /\ + v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\ + v_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\ v_T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE v_K"#))] pub fn keys_from_private_key< const K: usize, @@ -666,11 +666,11 @@ pub(crate) mod unpacked { /// Take a serialized private key and generate an unpacked key pair from it. #[inline(always)] - #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - v_SECRET_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE v_K /\\ - v_CPA_SECRET_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE v_K /\\ - v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\\ - v_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\\ + #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + v_SECRET_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE v_K /\ + v_CPA_SECRET_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE v_K /\ + v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\ + v_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\ v_T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE v_K)"#))] pub fn from_private_key< const SECRET_KEY_SIZE: usize, @@ -696,9 +696,9 @@ pub(crate) mod unpacked { /// Get the serialized public key. #[inline(always)] - #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ - $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ (forall (i:nat). i < v $K ==> Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i))"#))] @@ -722,9 +722,9 @@ pub(crate) mod unpacked { /// Get the serialized public key. #[inline(always)] - #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ - $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ (forall (i:nat). i < v $K ==> Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i))"#))] @@ -758,10 +758,10 @@ pub(crate) mod unpacked { /// Get the serialized private key. #[inline(always)] - #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $PRIVATE_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\\ - $CPA_PRIVATE_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\\ - $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $PRIVATE_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\ + $CPA_PRIVATE_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K"#))] pub fn serialized_private_key_mut< const CPA_PRIVATE_KEY_SIZE: usize, @@ -793,10 +793,10 @@ pub(crate) mod unpacked { /// Get the serialized private key. #[inline(always)] - #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $PRIVATE_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\\ - $CPA_PRIVATE_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\\ - $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $PRIVATE_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\ + $CPA_PRIVATE_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\ $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K"#))] pub fn serialized_private_key< const CPA_PRIVATE_KEY_SIZE: usize, @@ -848,21 +848,21 @@ pub(crate) mod unpacked { for i in 0..K { hax_lib::loop_invariant!(|i: usize| { fstar!( - "forall (j: nat). j < v $i ==> + r#"forall (j: nat). j < v $i ==> (forall (k: nat). k < v $K ==> Seq.index (Seq.index $A j) k == - Seq.index (Seq.index $ind_cpa_a k) j)" + Seq.index (Seq.index $ind_cpa_a k) j)"# ) }); let _a_i = A; for j in 0..K { hax_lib::loop_invariant!(|j: usize| { fstar!( - "(forall (k: nat). k < v $i ==> - Seq.index $A k == Seq.index $_a_i k) /\\ + r#"(forall (k: nat). k < v $i ==> + Seq.index $A k == Seq.index $_a_i k) /\ (forall (k: nat). k < v $j ==> Seq.index (Seq.index $A (v $i)) k == - Seq.index (Seq.index $ind_cpa_a k) (v $i))" + Seq.index (Seq.index $ind_cpa_a k) (v $i))"# ) }); A[i][j] = ind_cpa_a[j][i].clone(); @@ -874,17 +874,17 @@ pub(crate) mod unpacked { /// Generate Unpacked Keys #[inline(always)] #[hax_lib::fstar::options("--z3rlimit 1500 --ext context_pruning --z3refresh")] - #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\ - $ETA1 == Spec.MLKEM.v_ETA1 $K /\\ - $BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ + #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\ + $ETA1 == Spec.MLKEM.v_ETA1 $K /\ + $BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\ $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K"#))] #[hax_lib::ensures(|result| fstar!(r#"let ((m_A, public_key_hash), implicit_rejection_value), valid = Spec.MLKEM.ind_cca_unpack_generate_keypair $K $randomness in valid ==> Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector - ${out}_future.f_public_key.f_ind_cpa_public_key.f_A == m_A /\\ - ${out}_future.f_public_key.f_public_key_hash == public_key_hash /\\ + ${out}_future.f_public_key.f_ind_cpa_public_key.f_A == m_A /\ + ${out}_future.f_public_key.f_public_key_hash == public_key_hash /\ ${out}_future.f_private_key.f_implicit_rejection_value == implicit_rejection_value"#)) ] pub(crate) fn generate_keypair< @@ -947,16 +947,16 @@ pub(crate) mod unpacked { // Encapsulate with Unpacked Public Key #[inline(always)] - #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $ETA1 == Spec.MLKEM.v_ETA1 $K /\\ - $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\ - $ETA2 == Spec.MLKEM.v_ETA2 $K /\\ - $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\\ - $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\\ - $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\\ - $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\ - $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\ - $VECTOR_U_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\ + #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $ETA1 == Spec.MLKEM.v_ETA1 $K /\ + $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\ + $ETA2 == Spec.MLKEM.v_ETA2 $K /\ + $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\ + $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\ + $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\ + $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\ + $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\ + $VECTOR_U_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\ $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K"#))] #[hax_lib::ensures(|(ciphertext_result, shared_secret_array)| fstar!(r#"let (ciphertext, shared_secret) = @@ -964,7 +964,7 @@ pub(crate) mod unpacked { (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key}.f_ind_cpa_public_key.f_t_as_ntt) (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key}.f_ind_cpa_public_key.f_A) $randomness in - ${ciphertext_result}.f_value == ciphertext /\\ + ${ciphertext_result}.f_value == ciphertext /\ $shared_secret_array == shared_secret"#)) ] pub(crate) fn encapsulate< @@ -1025,17 +1025,17 @@ pub(crate) mod unpacked { // Decapsulate with Unpacked Private Key #[inline(always)] #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning --z3refresh")] - #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\\ - $ETA1 == Spec.MLKEM.v_ETA1 $K /\\ - $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\ - $ETA2 == Spec.MLKEM.v_ETA2 $K /\\ - $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\\ - $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\\ - $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\\ - $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\ - $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\ - $C1_BLOCK_SIZE == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\ - $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\ + #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\ + $ETA1 == Spec.MLKEM.v_ETA1 $K /\ + $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\ + $ETA2 == Spec.MLKEM.v_ETA2 $K /\ + $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\ + $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\ + $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\ + $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\ + $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\ + $C1_BLOCK_SIZE == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\ + $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\ $IMPLICIT_REJECTION_HASH_INPUT_SIZE == Spec.MLKEM.v_IMPLICIT_REJECTION_HASH_INPUT_SIZE $K"#))] #[hax_lib::ensures(|result| fstar!(r#"$result == diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs index 5dc48d300..a552ba5dd 100644 --- a/libcrux-ml-kem/src/ind_cpa.rs +++ b/libcrux-ml-kem/src/ind_cpa.rs @@ -380,10 +380,10 @@ fn sample_vector_cbd_then_ntt< for i in 0..K { hax_lib::loop_invariant!(|i: usize| { fstar!( - "forall (j:nat). j < v $i ==> + r#"forall (j:nat). j < v $i ==> Libcrux_ml_kem.Polynomial.to_spec_poly_t #$:Vector re_as_ntt.[ sz j ] == Spec.MLKEM.poly_ntt (Spec.MLKEM.sample_poly_cbd $ETA ${prf_outputs}.[ sz j ]) /\ - Libcrux_ml_kem.Serialize.coefficients_field_modulus_range #$:Vector re_as_ntt.[ sz j ]" + Libcrux_ml_kem.Serialize.coefficients_field_modulus_range #$:Vector re_as_ntt.[ sz j ]"# ) }); re_as_ntt[i] = sample_from_binomial_distribution::(&prf_outputs[i]); diff --git a/libcrux-ml-kem/src/invert_ntt.rs b/libcrux-ml-kem/src/invert_ntt.rs index 81d9db04f..65ab81748 100644 --- a/libcrux-ml-kem/src/invert_ntt.rs +++ b/libcrux-ml-kem/src/invert_ntt.rs @@ -77,7 +77,7 @@ pub(crate) fn invert_ntt_at_layer_1( } #[inline(always)] -#[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning"#)] +#[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")] #[hax_lib::requires(fstar!(r#"v ${*zeta_i} == 64 /\ invert_ntt_re_range_2 $re "#))] #[hax_lib::ensures(|result| fstar!(r#"invert_ntt_re_range_2 ${re}_future /\ diff --git a/libcrux-ml-kem/src/ntt.rs b/libcrux-ml-kem/src/ntt.rs index 12feb2485..4446ddc64 100644 --- a/libcrux-ml-kem/src/ntt.rs +++ b/libcrux-ml-kem/src/ntt.rs @@ -8,21 +8,21 @@ use crate::{ #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")] #[hax_lib::fstar::before( interface, - "[@@ \"opaque_to_smt\"] + r#"[@@ "opaque_to_smt"] let ntt_re_range_2 (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) = forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (11207+5*3328) - (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ sz i ]))" + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ sz i ]))"# )] #[hax_lib::fstar::before( interface, - "[@@ \"opaque_to_smt\"] + r#"[@@ "opaque_to_smt"] let ntt_re_range_1 (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) = forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (11207+6*3328) - (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ sz i ]))" + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ sz i ]))"# )] #[hax_lib::requires(fstar!(r#"v ${*zeta_i} == 63 /\ ntt_re_range_2 $re"#))] @@ -81,12 +81,12 @@ pub(crate) fn ntt_at_layer_1( #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")] #[hax_lib::fstar::before( interface, - "[@@ \"opaque_to_smt\"] + r#"[@@ "opaque_to_smt"] let ntt_re_range_3 (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) = forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (11207+4*3328) - (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ sz i ]))" + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ sz i ]))"# )] #[hax_lib::requires(fstar!(r#"v ${*zeta_i} == 31 /\ ntt_re_range_3 $re"#))] @@ -140,12 +140,12 @@ pub(crate) fn ntt_at_layer_2( #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")] #[hax_lib::fstar::before( interface, - "[@@ \"opaque_to_smt\"] + r#"[@@ "opaque_to_smt"] let ntt_re_range_4 (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) = forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (11207+3*3328) - (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ sz i ]))" + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ sz i ]))"# )] #[hax_lib::requires(fstar!(r#"v ${*zeta_i} == 15 /\ ntt_re_range_4 $re"#))] @@ -263,7 +263,7 @@ pub(crate) fn ntt_at_layer_4_plus( //We should make the loops inside this function `opaque_to_smt` to get it work #[hax_lib::fstar::before( interface, - "[@@ \"opaque_to_smt\"] + r#"[@@ "opaque_to_smt"] let ntt_layer_7_pre (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (re_0 re_1: v_Vector) = @@ -278,7 +278,7 @@ pub(crate) fn ntt_at_layer_4_plus( (forall i. i < 16 ==> Spec.Utils.is_intb (pow2 15 - 1) (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_0) i) + - v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))))" + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))))"# )] #[hax_lib::requires(fstar!(r#"forall i. i < 8 ==> ntt_layer_7_pre (${re}.f_coefficients.[ sz i ]) (${re}.f_coefficients.[ sz i +! sz 8 ])"#))] diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs index 0ae669038..a3b3b2ce5 100644 --- a/libcrux-ml-kem/src/serialize.rs +++ b/libcrux-ml-kem/src/serialize.rs @@ -10,21 +10,21 @@ use crate::{ #[inline(always)] #[hax_lib::fstar::before( interface, - "[@@ \"opaque_to_smt\"] + r#"[@@ "opaque_to_smt"] let coefficients_field_modulus_range (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) = - forall (i:nat). i < 16 ==> field_modulus_range (Seq.index re.f_coefficients i)" + forall (i:nat). i < 16 ==> field_modulus_range (Seq.index re.f_coefficients i)"# )] #[hax_lib::fstar::before( interface, - "[@@ \"opaque_to_smt\"] + r#"[@@ "opaque_to_smt"] let field_modulus_range (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (a: v_Vector) = let coef = Libcrux_ml_kem.Vector.Traits.f_to_i16_array a in forall (i:nat). i < 16 ==> v (Seq.index coef i) > -(v $FIELD_MODULUS) /\ - v (Seq.index coef i) < v $FIELD_MODULUS" + v (Seq.index coef i) < v $FIELD_MODULUS"# )] #[hax_lib::fstar::verification_status(panic_free)] #[hax_lib::requires(fstar!(r#"field_modulus_range $a"#))] diff --git a/libcrux-ml-kem/src/utils.rs b/libcrux-ml-kem/src/utils.rs index f38e3c088..ece8cdabc 100644 --- a/libcrux-ml-kem/src/utils.rs +++ b/libcrux-ml-kem/src/utils.rs @@ -33,9 +33,9 @@ pub(crate) fn into_padded_array(slice: &[u8]) -> [u8; LEN] { #[hax_lib::fstar::options("--z3rlimit 200")] #[hax_lib::requires(fstar!(r#"range (v $domain_separator + v $K) u8_inttype"#))] #[hax_lib::ensures(|ds| - fstar!(r#"v $ds == v $domain_separator + v $K /\\ + fstar!(r#"v $ds == v $domain_separator + v $K /\ (forall (i:nat). i < v $K ==> - v (Seq.index (Seq.index ${prf_inputs}_future i) 32) == v $domain_separator + i /\\ + v (Seq.index (Seq.index ${prf_inputs}_future i) 32) == v $domain_separator + i /\ Seq.slice (Seq.index ${prf_inputs}_future i) 0 32 == Seq.slice (Seq.index $prf_inputs i) 0 32)"#) )] pub(crate) fn prf_input_inc( @@ -47,10 +47,10 @@ pub(crate) fn prf_input_inc( for i in 0..K { hax_lib::loop_invariant!(|i: usize| { fstar!( - r#"v $domain_separator == v $_domain_separator_init + v $i /\\ - (v $i < v $K ==> (forall (j:nat). (j >= v $i /\\ j < v $K) ==> - prf_inputs.[ sz j ] == ${_prf_inputs_init}.[ sz j ])) /\\ - (forall (j:nat). j < v $i ==> v (Seq.index (Seq.index prf_inputs j) 32) == v $_domain_separator_init + j /\\ + r#"v $domain_separator == v $_domain_separator_init + v $i /\ + (v $i < v $K ==> (forall (j:nat). (j >= v $i /\ j < v $K) ==> + prf_inputs.[ sz j ] == ${_prf_inputs_init}.[ sz j ])) /\ + (forall (j:nat). j < v $i ==> v (Seq.index (Seq.index prf_inputs j) 32) == v $_domain_separator_init + j /\ Seq.slice (Seq.index prf_inputs j) 0 32 == Seq.slice (Seq.index $_prf_inputs_init j) 0 32)"# ) }); diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs index 87d0f873b..89b1b01a4 100644 --- a/libcrux-ml-kem/src/vector/avx2.rs +++ b/libcrux-ml-kem/src/vector/avx2.rs @@ -65,15 +65,15 @@ fn compress_1(vector: SIMD256Vector) -> SIMD256Vector { #[inline(always)] #[hax_lib::fstar::verification_status(lax)] -#[hax_lib::requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ +#[hax_lib::requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ v $COEFFICIENT_BITS == 11) /\ (forall (i:nat). i < 16 ==> v (Seq.index (repr $vector) i) >= 0 /\ v (Seq.index (repr $vector) i) < 3329)"#))] -#[hax_lib::ensures(|out| fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ +#[hax_lib::ensures(|out| fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ v $COEFFICIENT_BITS == 11) ==> (forall (i:nat). i < 16 ==> bounded (Seq.index (repr $out) i) (v $COEFFICIENT_BITS))"#))] fn compress(vector: SIMD256Vector) -> SIMD256Vector { @@ -366,15 +366,15 @@ impl Operations for SIMD256Vector { compress_1(vector) } - #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ + #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ v $COEFFICIENT_BITS == 11) /\ (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $vector) i) >= 0 /\ v (Seq.index (impl.f_repr $vector) i) < 3329)"#))] - #[ensures(|out| fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ + #[ensures(|out| fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ v $COEFFICIENT_BITS == 11) ==> (forall (i:nat). i < 16 ==> bounded (Seq.index (impl.f_repr $out) i) (v $COEFFICIENT_BITS))"#))] #[inline(always)] @@ -382,9 +382,9 @@ impl Operations for SIMD256Vector { compress::(vector) } - #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ + #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ v $COEFFICIENT_BITS == 11) /\ (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $vector) i) >= 0 /\ v (Seq.index (impl.f_repr $vector) i) < pow2 (v $COEFFICIENT_BITS))"#))] diff --git a/libcrux-ml-kem/src/vector/avx2/arithmetic.rs b/libcrux-ml-kem/src/vector/avx2/arithmetic.rs index 1a46a54b6..905c5186b 100644 --- a/libcrux-ml-kem/src/vector/avx2/arithmetic.rs +++ b/libcrux-ml-kem/src/vector/avx2/arithmetic.rs @@ -105,7 +105,7 @@ pub(crate) fn shift_right(vector: Vec256) -> Vec256 { } #[inline(always)] -#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 100"#))] +#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 100"))] #[hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b_array (pow2 12 - 1) (Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 $vector)"#))] #[hax_lib::ensures(|result| fstar!(r#"forall i. i < 16 ==> get_lane $result i == @@ -146,7 +146,7 @@ const BARRETT_MULTIPLIER: i16 = 20159; /// See Section 3.2 of the implementation notes document for an explanation /// of this code. #[inline(always)] -#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 200"#))] +#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 200"))] #[cfg_attr(hax, hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b_array 28296 (Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 ${vector})"#)))] #[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b_array 3328 (Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 ${result}) /\ (forall i. i < 16 ==> v (get_lane $result i) % 3329 == @@ -235,7 +235,7 @@ pub(crate) fn montgomery_multiply_by_constant(vector: Vec256, constant: i16) -> } #[inline(always)] -#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 100"#))] +#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 100"))] #[cfg_attr(hax, hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b_array 1664 (Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 $constants))"#)))] #[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b_array 3328 (Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 ${result}) /\ (forall i. i < 16 ==> v (get_lane $result i) % 3329 == @@ -312,7 +312,7 @@ pub(crate) fn montgomery_reduce_i32s(vec: Vec256) -> Vec256 { } #[inline(always)] -#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 100"#))] +#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 100"))] #[cfg_attr(hax, hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b_array 1664 (Libcrux_intrinsics.Avx2_extract.vec128_as_i16x8 $constants))"#)))] #[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b_array 3328 (Libcrux_intrinsics.Avx2_extract.vec128_as_i16x8 ${result}) /\ (forall i. i < 8 ==> v (get_lane128 $result i) % 3329 == diff --git a/libcrux-ml-kem/src/vector/portable.rs b/libcrux-ml-kem/src/vector/portable.rs index cc997b79e..d5432c02e 100644 --- a/libcrux-ml-kem/src/vector/portable.rs +++ b/libcrux-ml-kem/src/vector/portable.rs @@ -159,7 +159,7 @@ impl Operations for PortableVector { } #[requires(SHIFT_BY >= 0 && SHIFT_BY < 16)] - #[ensures(|out| fstar!(r#"(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $v)"#))] + #[ensures(|out| fstar!(r#"(v_SHIFT_BY >=. 0l /\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $v)"#))] fn shift_right(v: Self) -> Self { shift_right::<{ SHIFT_BY }>(v) } @@ -180,85 +180,85 @@ impl Operations for PortableVector { montgomery_multiply_by_constant(v, r) } - #[requires(fstar!(r#"forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\\ + #[requires(fstar!(r#"forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\ v (Seq.index (impl.f_repr $a) i) < 3329"#))] #[ensures(|out| fstar!(r#"forall (i:nat). i < 16 ==> bounded (Seq.index (impl.f_repr $out) i) 1"#))] fn compress_1(a: Self) -> Self { compress_1(a) } - #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ - v $COEFFICIENT_BITS == 11) /\\ - (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\\ + #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ + v $COEFFICIENT_BITS == 11) /\ + (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\ v (Seq.index (impl.f_repr $a) i) < 3329)"#))] - #[ensures(|out| fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ + #[ensures(|out| fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ v $COEFFICIENT_BITS == 11) ==> (forall (i:nat). i < 16 ==> bounded (Seq.index (impl.f_repr $out) i) (v $COEFFICIENT_BITS))"#))] fn compress(a: Self) -> Self { compress::(a) } - #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ - v $COEFFICIENT_BITS == 11) /\\ - (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\\ + #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ + v $COEFFICIENT_BITS == 11) /\ + (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\ v (Seq.index (impl.f_repr $a) i) < pow2 (v $COEFFICIENT_BITS))"#))] fn decompress_ciphertext_coefficient(a: Self) -> Self { decompress_ciphertext_coefficient::(a) } - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ - Spec.Utils.is_i16b 1664 zeta2 /\\ Spec.Utils.is_i16b 1664 zeta3 /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ + Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ Spec.Utils.is_i16b_array (11207+5*3328) (impl.f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array (11207+6*3328) (impl.f_repr $out)"#))] fn ntt_layer_1_step(a: Self, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) -> Self { ntt_layer_1_step(a, zeta0, zeta1, zeta2, zeta3) } - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b_array (11207+4*3328) (impl.f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array (11207+5*3328) (impl.f_repr $out)"#))] fn ntt_layer_2_step(a: Self, zeta0: i16, zeta1: i16) -> Self { ntt_layer_2_step(a, zeta0, zeta1) } - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta /\ Spec.Utils.is_i16b_array (11207+3*3328) (impl.f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array (11207+4*3328) (impl.f_repr $out)"#))] fn ntt_layer_3_step(a: Self, zeta: i16) -> Self { ntt_layer_3_step(a, zeta) } - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ - Spec.Utils.is_i16b 1664 zeta2 /\\ Spec.Utils.is_i16b 1664 zeta3 /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ + Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ Spec.Utils.is_i16b_array (4*3328) (impl.f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (impl.f_repr $out)"#))] fn inv_ntt_layer_1_step(a: Self, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) -> Self { inv_ntt_layer_1_step(a, zeta0, zeta1, zeta2, zeta3) } - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b_array 3328 (impl.f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (impl.f_repr $out)"#))] fn inv_ntt_layer_2_step(a: Self, zeta0: i16, zeta1: i16) -> Self { inv_ntt_layer_2_step(a, zeta0, zeta1) } - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta /\ Spec.Utils.is_i16b_array 3328 (impl.f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (impl.f_repr $out)"#))] fn inv_ntt_layer_3_step(a: Self, zeta: i16) -> Self { inv_ntt_layer_3_step(a, zeta) } - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ - Spec.Utils.is_i16b 1664 zeta2 /\\ Spec.Utils.is_i16b 1664 zeta3 /\\ - Spec.Utils.is_i16b_array 3328 (impl.f_repr ${lhs}) /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ + Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ + Spec.Utils.is_i16b_array 3328 (impl.f_repr ${lhs}) /\ Spec.Utils.is_i16b_array 3328 (impl.f_repr ${rhs})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (impl.f_repr $out)"#))] fn ntt_multiply( @@ -340,7 +340,7 @@ impl Operations for PortableVector { #[requires(a.len() == 24 && out.len() == 16)] #[ensures(|result| - fstar!(r#"Seq.length $out_future == Seq.length $out /\\ v $result <= 16"#) + fstar!(r#"Seq.length $out_future == Seq.length $out /\ v $result <= 16"#) )] fn rej_sample(a: &[u8], out: &mut [i16]) -> usize { rej_sample(a, out) diff --git a/libcrux-ml-kem/src/vector/portable/arithmetic.rs b/libcrux-ml-kem/src/vector/portable/arithmetic.rs index 9e909c2b6..dabef94f6 100644 --- a/libcrux-ml-kem/src/vector/portable/arithmetic.rs +++ b/libcrux-ml-kem/src/vector/portable/arithmetic.rs @@ -58,7 +58,7 @@ pub fn add(mut lhs: PortableVector, rhs: &PortableVector) -> PortableVector { fstar!( r#" (forall j. j < v i ==> (Seq.index ${lhs}.f_elements j) == - (Seq.index ${_lhs0}.f_elements j) +! (Seq.index ${rhs}.f_elements j)) /\\ + (Seq.index ${_lhs0}.f_elements j) +! (Seq.index ${rhs}.f_elements j)) /\ (forall j. j >= v i ==> (Seq.index ${lhs}.f_elements j) == (Seq.index ${_lhs0}.f_elements j))"# ) }); @@ -84,7 +84,7 @@ pub fn sub(mut lhs: PortableVector, rhs: &PortableVector) -> PortableVector { fstar!( r#" (forall j. j < v i ==> (Seq.index ${lhs}.f_elements j) == - (Seq.index ${_lhs0}.f_elements j) -! (Seq.index ${rhs}.f_elements j)) /\\ + (Seq.index ${_lhs0}.f_elements j) -! (Seq.index ${rhs}.f_elements j)) /\ (forall j. j >= v i ==> (Seq.index ${lhs}.f_elements j) == (Seq.index ${_lhs0}.f_elements j))"# ) }); @@ -110,7 +110,7 @@ pub fn multiply_by_constant(mut vec: PortableVector, c: i16) -> PortableVector { fstar!( r#" (forall j. j < v i ==> (Seq.index ${vec}.f_elements j) == - (Seq.index ${_vec0}.f_elements j) *! c) /\\ + (Seq.index ${_vec0}.f_elements j) *! c) /\ (forall j. j >= v i ==> (Seq.index ${vec}.f_elements j) == (Seq.index ${_vec0}.f_elements j))"# ) }); @@ -132,7 +132,7 @@ pub fn bitwise_and_with_constant(mut vec: PortableVector, c: i16) -> PortableVec fstar!( r#" (forall j. j < v i ==> Seq.index ${vec}.f_elements j == - (Seq.index ${_vec0}.f_elements j &. c)) /\\ + (Seq.index ${_vec0}.f_elements j &. c)) /\ (forall j. j >= v i ==> Seq.index ${vec}.f_elements j == Seq.index ${_vec0}.f_elements j)"# ) }); @@ -146,7 +146,7 @@ pub fn bitwise_and_with_constant(mut vec: PortableVector, c: i16) -> PortableVec #[inline(always)] #[hax_lib::requires(SHIFT_BY >= 0 && SHIFT_BY < 16)] -#[hax_lib::ensures(|result| fstar!(r#"(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> +#[hax_lib::ensures(|result| fstar!(r#"(v_SHIFT_BY >=. 0l /\ v_SHIFT_BY <. 16l) ==> ${result}.f_elements == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (${vec}.f_elements)"#))] pub fn shift_right(mut vec: PortableVector) -> PortableVector { let _vec0 = vec; @@ -155,7 +155,7 @@ pub fn shift_right(mut vec: PortableVector) -> PortableVect fstar!( r#" (forall j. j < v i ==> Seq.index ${vec}.f_elements j == - (Seq.index ${_vec0}.f_elements j >>! ${SHIFT_BY})) /\\ + (Seq.index ${_vec0}.f_elements j >>! ${SHIFT_BY})) /\ (forall j. j >= v i ==> Seq.index ${vec}.f_elements j == Seq.index ${_vec0}.f_elements j)"# ) }); @@ -182,7 +182,7 @@ pub fn cond_subtract_3329(mut vec: PortableVector) -> PortableVector { r#" (forall j. j < v i ==> Seq.index ${vec}.f_elements j == (let x = Seq.index ${_vec0}.f_elements j in - if x >=. 3329s then x -! 3329s else x)) /\\ + if x >=. 3329s then x -! 3329s else x)) /\ (forall j. j >= v i ==> Seq.index ${vec}.f_elements j == Seq.index ${_vec0}.f_elements j)"# ) }); @@ -211,7 +211,7 @@ pub fn cond_subtract_3329(mut vec: PortableVector) -> PortableVector { /// #[hax_lib::fstar::options("--z3rlimit 150 --ext context_pruning")] #[cfg_attr(hax, hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b 28296 value"#)))] -#[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b 3328 result /\\ +#[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b 3328 result /\ v result % 3329 == v value % 3329"#)))] pub(crate) fn barrett_reduce_element(value: FieldElement) -> FieldElement { let t = (i32::from(value) * BARRETT_MULTIPLIER) + (BARRETT_R >> 1); @@ -244,7 +244,7 @@ pub(crate) fn barrett_reduce_element(value: FieldElement) -> FieldElement { #[inline(always)] #[hax_lib::fstar::options("--z3rlimit 150")] #[cfg_attr(hax, hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b_array 28296 ${vec}.f_elements"#)))] -#[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b_array 3328 ${result}.f_elements /\\ +#[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b_array 3328 ${result}.f_elements /\ (forall i. (v (Seq.index ${result}.f_elements i) % 3329) == (v (Seq.index ${vec}.f_elements i) % 3329))"#)))] pub(crate) fn barrett_reduce(mut vec: PortableVector) -> PortableVector { @@ -253,9 +253,9 @@ pub(crate) fn barrett_reduce(mut vec: PortableVector) -> PortableVector { hax_lib::loop_invariant!(|i: usize| { fstar!( r#" - (forall j. j < v i ==> (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements j) /\\ - v (Seq.index ${vec}.f_elements j) % 3329 == (v (Seq.index ${_vec0}.f_elements j) % 3329))) /\\ - (forall j. j >= v i ==> (Seq.index ${vec}.f_elements j == Seq.index ${_vec0}.f_elements j /\\ + (forall j. j < v i ==> (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements j) /\ + v (Seq.index ${vec}.f_elements j) % 3329 == (v (Seq.index ${_vec0}.f_elements j) % 3329))) /\ + (forall j. j >= v i ==> (Seq.index ${vec}.f_elements j == Seq.index ${_vec0}.f_elements j /\ Spec.Utils.is_i16b 28296 (Seq.index ${vec}.f_elements j)))"# ) }); @@ -287,8 +287,8 @@ pub(crate) fn barrett_reduce(mut vec: PortableVector) -> PortableVector { /// #[hax_lib::fstar::options("--z3rlimit 500 --split_queries always")] #[cfg_attr(hax, hax_lib::requires(fstar!(r#"Spec.Utils.is_i32b (3328 * pow2 16) value "#)))] -#[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b (3328 + 1665) result /\\ - (Spec.Utils.is_i32b (3328 * pow2 15) value ==> Spec.Utils.is_i16b 3328 result) /\\ +#[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b (3328 + 1665) result /\ + (Spec.Utils.is_i32b (3328 * pow2 15) value ==> Spec.Utils.is_i16b 3328 result) /\ v result % 3329 == (v value * 169) % 3329"#)))] pub(crate) fn montgomery_reduce_element(value: i32) -> MontgomeryFieldElement { // This forces hax to extract code for MONTGOMERY_R before it extracts code @@ -385,7 +385,7 @@ pub(crate) fn montgomery_reduce_element(value: i32) -> MontgomeryFieldElement { #[inline(always)] #[hax_lib::fstar::options("--z3rlimit 300")] #[cfg_attr(hax, hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b 1664 fer"#)))] -#[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b 3328 result /\\ +#[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b 3328 result /\ v result % 3329 == (v fe * v fer * 169) % 3329"#)))] pub(crate) fn montgomery_multiply_fe_by_fer( fe: FieldElement, @@ -400,7 +400,7 @@ pub(crate) fn montgomery_multiply_fe_by_fer( #[hax_lib::fstar::options("--z3rlimit 150")] #[cfg_attr(hax, hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b 1664 c"#)))] #[cfg_attr(hax, hax_lib::ensures(|result| fstar!(r#" -Spec.Utils.is_i16b_array 3328 ${result}.f_elements /\\ +Spec.Utils.is_i16b_array 3328 ${result}.f_elements /\ (forall i. i < 16 ==> (v (Seq.index ${result}.f_elements i) % 3329 == (v (Seq.index ${vec}.f_elements i) * v c * 169) %3329))"#)))] @@ -412,8 +412,8 @@ pub(crate) fn montgomery_multiply_by_constant(mut vec: PortableVector, c: i16) - r#" (forall j. j < v i ==> (let vecj = Seq.index ${vec}.f_elements j in - (Spec.Utils.is_i16b 3328 vecj /\\ - v vecj % 3329 == (v (Seq.index ${_vec0}.f_elements j) * v c * 169) % 3329))) /\\ + (Spec.Utils.is_i16b 3328 vecj /\ + v vecj % 3329 == (v (Seq.index ${_vec0}.f_elements j) * v c * 169) % 3329))) /\ (forall j. j >= v i ==> (Seq.index ${vec}.f_elements j) == (Seq.index ${_vec0}.f_elements j))"# ) }); diff --git a/libcrux-ml-kem/src/vector/portable/compress.rs b/libcrux-ml-kem/src/vector/portable/compress.rs index 3b9d946ee..7fb2bf672 100644 --- a/libcrux-ml-kem/src/vector/portable/compress.rs +++ b/libcrux-ml-kem/src/vector/portable/compress.rs @@ -156,23 +156,23 @@ pub(crate) fn compress_1(mut a: PortableVector) -> PortableVector { ); a.elements[i] = compress_message_coefficient(a.elements[i] as u16) as i16; hax_lib::fstar!( - "assert (v (${a}.f_elements.[ $i ] <: i16) >= 0 /\ - v (${a}.f_elements.[ $i ] <: i16) < 2)" + r#"assert (v (${a}.f_elements.[ $i ] <: i16) >= 0 /\ + v (${a}.f_elements.[ $i ] <: i16) < 2)"# ); } hax_lib::fstar!( - "assert (forall (i:nat). i < 16 ==> v (${a}.f_elements.[ sz i ] <: i16) >= 0 /\ - v (${a}.f_elements.[ sz i ] <: i16) < 2)" + r#"assert (forall (i:nat). i < 16 ==> v (${a}.f_elements.[ sz i ] <: i16) >= 0 /\ + v (${a}.f_elements.[ sz i ] <: i16) < 2)"# ); a } #[inline(always)] #[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 2000")] -#[hax_lib::requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ +#[hax_lib::requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ v $COEFFICIENT_BITS == 11) /\ (forall (i:nat). i < 16 ==> v (Seq.index ${a}.f_elements i) >= 0 /\ v (Seq.index ${a}.f_elements i) < 3329)"#))] @@ -200,22 +200,22 @@ pub(crate) fn compress(mut a: PortableVector) -> Po a.elements[i] = compress_ciphertext_coefficient(COEFFICIENT_BITS as u8, a.elements[i] as u16) as i16; hax_lib::fstar!( - "assert (v (${a}.f_elements.[ $i ] <: i16) >= 0 /\ - v (${a}.f_elements.[ $i ] <: i16) < pow2 (v (cast ($COEFFICIENT_BITS) <: u32)))" + r#"assert (v (${a}.f_elements.[ $i ] <: i16) >= 0 /\ + v (${a}.f_elements.[ $i ] <: i16) < pow2 (v (cast ($COEFFICIENT_BITS) <: u32)))"# ); } hax_lib::fstar!( - "assert (forall (i:nat). i < 16 ==> v (${a}.f_elements.[ sz i ] <: i16) >= 0 /\ - v (${a}.f_elements.[ sz i ] <: i16) < pow2 (v $COEFFICIENT_BITS))" + r#"assert (forall (i:nat). i < 16 ==> v (${a}.f_elements.[ sz i ] <: i16) >= 0 /\ + v (${a}.f_elements.[ sz i ] <: i16) < pow2 (v $COEFFICIENT_BITS))"# ); a } #[inline(always)] #[hax_lib::fstar::options("--z3rlimit 300 --ext context_pruning")] -#[hax_lib::requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ +#[hax_lib::requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ v $COEFFICIENT_BITS == 11) /\ (forall (i:nat). i < 16 ==> v (Seq.index ${a}.f_elements i) >= 0 /\ v (Seq.index ${a}.f_elements i) < pow2 (v $COEFFICIENT_BITS))"#))] diff --git a/libcrux-ml-kem/src/vector/portable/ntt.rs b/libcrux-ml-kem/src/vector/portable/ntt.rs index bf746901d..85d053afc 100644 --- a/libcrux-ml-kem/src/vector/portable/ntt.rs +++ b/libcrux-ml-kem/src/vector/portable/ntt.rs @@ -183,7 +183,7 @@ pub(crate) fn inv_ntt_layer_1_step( inv_ntt_step(&mut vec, zeta3, 12, 14); inv_ntt_step(&mut vec, zeta3, 13, 15); hax_lib::fstar!( - "assert (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements 13)); + r#"assert (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements 13)); assert (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements 15)); assert (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements 12)); assert (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements 14)); @@ -199,7 +199,8 @@ pub(crate) fn inv_ntt_layer_1_step( assert (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements 3)); assert (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements 0)); assert (Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements 2)); - assert (forall (i:nat). i < 16 ==> Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements i))"#); + assert (forall (i:nat). i < 16 ==> Spec.Utils.is_i16b 3328 (Seq.index ${vec}.f_elements i))"# + ); vec } diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs index 87436fcd1..9898c741c 100644 --- a/libcrux-ml-kem/src/vector/traits.rs +++ b/libcrux-ml-kem/src/vector/traits.rs @@ -58,7 +58,7 @@ pub trait Operations: Copy + Clone + Repr { fn bitwise_and_with_constant(v: Self, c: i16) -> Self; #[requires(SHIFT_BY >= 0 && SHIFT_BY < 16)] - #[ensures(|result| fstar!(r#"(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> f_repr $result == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (f_repr $v)"#))] + #[ensures(|result| fstar!(r#"(v_SHIFT_BY >=. 0l /\ v_SHIFT_BY <. 16l) ==> f_repr $result == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (f_repr $v)"#))] fn shift_right(v: Self) -> Self; // fn shift_left(v: Self) -> Self; @@ -74,62 +74,62 @@ pub trait Operations: Copy + Clone + Repr { fn montgomery_multiply_by_constant(v: Self, c: i16) -> Self; // Compression - #[requires(fstar!(r#"forall (i:nat). i < 16 ==> v (Seq.index (f_repr $a) i) >= 0 /\\ + #[requires(fstar!(r#"forall (i:nat). i < 16 ==> v (Seq.index (f_repr $a) i) >= 0 /\ v (Seq.index (f_repr $a) i) < 3329"#))] #[ensures(|result| fstar!(r#"forall (i:nat). i < 16 ==> bounded (Seq.index (f_repr $result) i) 1"#))] fn compress_1(a: Self) -> Self; - #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ - v $COEFFICIENT_BITS == 11) /\\ - (forall (i:nat). i < 16 ==> v (Seq.index (f_repr $a) i) >= 0 /\\ + #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ + v $COEFFICIENT_BITS == 11) /\ + (forall (i:nat). i < 16 ==> v (Seq.index (f_repr $a) i) >= 0 /\ v (Seq.index (f_repr $a) i) < 3329)"#))] - #[ensures(|result| fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ + #[ensures(|result| fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ v $COEFFICIENT_BITS == 11) ==> (forall (i:nat). i < 16 ==> bounded (Seq.index (f_repr $result) i) (v $COEFFICIENT_BITS))"#))] fn compress(a: Self) -> Self; - #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \\/ - v $COEFFICIENT_BITS == 5 \\/ - v $COEFFICIENT_BITS == 10 \\/ - v $COEFFICIENT_BITS == 11) /\\ - (forall (i:nat). i < 16 ==> v (Seq.index (f_repr $a) i) >= 0 /\\ + #[requires(fstar!(r#"(v $COEFFICIENT_BITS == 4 \/ + v $COEFFICIENT_BITS == 5 \/ + v $COEFFICIENT_BITS == 10 \/ + v $COEFFICIENT_BITS == 11) /\ + (forall (i:nat). i < 16 ==> v (Seq.index (f_repr $a) i) >= 0 /\ v (Seq.index (f_repr $a) i) < pow2 (v $COEFFICIENT_BITS))"#))] fn decompress_ciphertext_coefficient(a: Self) -> Self; // NTT - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ - Spec.Utils.is_i16b 1664 zeta2 /\\ Spec.Utils.is_i16b 1664 zeta3 /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ + Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ Spec.Utils.is_i16b_array (11207+5*3328) (f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array (11207+6*3328) (f_repr $out)"#))] fn ntt_layer_1_step(a: Self, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) -> Self; - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b_array (11207+4*3328) (f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array (11207+5*3328) (f_repr $out)"#))] fn ntt_layer_2_step(a: Self, zeta0: i16, zeta1: i16) -> Self; - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta /\ Spec.Utils.is_i16b_array (11207+3*3328) (f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array (11207+4*3328) (f_repr $out)"#))] fn ntt_layer_3_step(a: Self, zeta: i16) -> Self; - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ - Spec.Utils.is_i16b 1664 zeta2 /\\ Spec.Utils.is_i16b 1664 zeta3 /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ + Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ Spec.Utils.is_i16b_array (4 * 3328) (f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (f_repr $out)"#))] fn inv_ntt_layer_1_step(a: Self, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) -> Self; - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b_array 3328 (f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (f_repr $out)"#))] fn inv_ntt_layer_2_step(a: Self, zeta0: i16, zeta1: i16) -> Self; - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta/\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta/\ Spec.Utils.is_i16b_array 3328 (f_repr ${a})"#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (f_repr $out)"#))] fn inv_ntt_layer_3_step(a: Self, zeta: i16) -> Self; - #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ - Spec.Utils.is_i16b 1664 zeta2 /\\ Spec.Utils.is_i16b 1664 zeta3 /\\ - Spec.Utils.is_i16b_array 3328 (f_repr ${lhs}) /\\ + #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ + Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ + Spec.Utils.is_i16b_array 3328 (f_repr ${lhs}) /\ Spec.Utils.is_i16b_array 3328 (f_repr ${rhs}) "#))] #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (f_repr $out)"#))] fn ntt_multiply(lhs: &Self, rhs: &Self, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) @@ -174,7 +174,7 @@ pub trait Operations: Copy + Clone + Repr { #[requires(a.len() == 24 && out.len() == 16)] #[ensures(|result| - fstar!(r#"Seq.length $out_future == Seq.length $out /\\ v $result <= 16"#) + fstar!(r#"Seq.length $out_future == Seq.length $out /\ v $result <= 16"#) )] fn rej_sample(a: &[u8], out: &mut [i16]) -> usize; } @@ -236,7 +236,7 @@ pub fn to_standard_domain(v: T) -> T { #[hax_lib::ensures(|result| fstar!(r#"forall i. (let x = Seq.index (i1._super_8706949974463268012.f_repr ${a}) i in let y = Seq.index (i1._super_8706949974463268012.f_repr ${result}) i in - (v y >= 0 /\\ v y <= 3328 /\\ (v y % 3329 == v x % 3329)))"#))] + (v y >= 0 /\ v y <= 3328 /\ (v y % 3329 == v x % 3329)))"#))] #[inline(always)] pub fn to_unsigned_representative(a: T) -> T { let t = T::shift_right::<15>(a); @@ -244,9 +244,9 @@ pub fn to_unsigned_representative(a: T) -> T { T::add(a, &fm) } -#[hax_lib::fstar::options("--z3rlimit 200 --split_queries always"#)] +#[hax_lib::fstar::options("--z3rlimit 200 --split_queries always")] #[hax_lib::requires(fstar!(r#"forall i. let x = Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i in - (x == 0s \\/ x == 1s)"#))] + (x == 0s \/ x == 1s)"#))] #[inline(always)] pub fn decompress_1(vec: T) -> T { let z = T::ZERO(); @@ -254,8 +254,8 @@ pub fn decompress_1(vec: T) -> T { "assert(forall i. Seq.index (i1._super_8706949974463268012.f_repr ${z}) i == 0s)" ); hax_lib::fstar!( - "assert(forall i. let x = Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i in - ((0 - v x) == 0 \\/ (0 - v x) == -1))" + r#"assert(forall i. let x = Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i in + ((0 - v x) == 0 \/ (0 - v x) == -1))"# ); hax_lib::fstar!( r#"assert(forall i. i < 16 ==> @@ -265,7 +265,7 @@ pub fn decompress_1(vec: T) -> T { let s = T::sub(z, &vec); hax_lib::fstar!( - r#"assert(forall i. Seq.index (i1._super_8706949974463268012.f_repr ${s}) i == 0s \\/ + r#"assert(forall i. Seq.index (i1._super_8706949974463268012.f_repr ${s}) i == 0s \/ Seq.index (i1._super_8706949974463268012.f_repr ${s}) i == -1s)"# ); hax_lib::fstar!(r#"assert (i1.f_bitwise_and_with_constant_pre ${s} 1665s)"#); diff --git a/libcrux-sha3/src/generic_keccak.rs b/libcrux-sha3/src/generic_keccak.rs index 8751d95d5..ab3bd28e4 100644 --- a/libcrux-sha3/src/generic_keccak.rs +++ b/libcrux-sha3/src/generic_keccak.rs @@ -5,7 +5,7 @@ use core::ops::Index; use crate::traits::*; -#[cfg_attr(hax, hax_lib::opaque_type)] +#[cfg_attr(hax, hax_lib::opaque)] #[derive(Clone, Copy)] pub(crate) struct KeccakState> { st: [[T; 5]; 5], @@ -31,7 +31,7 @@ impl> KeccakState { /// The internal keccak state that can also buffer inputs to absorb. /// This is used in the general xof APIs. -#[cfg_attr(hax, hax_lib::opaque_type)] +#[cfg_attr(hax, hax_lib::opaque)] pub(crate) struct KeccakXofState< const PARALLEL_LANES: usize, const RATE: usize, diff --git a/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fsti b/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fsti index 0b77def1e..d7c15a880 100644 --- a/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fsti +++ b/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fsti @@ -38,6 +38,12 @@ type t_Feature = val t_Feature_cast_to_repr (x: t_Feature) : Prims.Pure isize Prims.l_True (fun _ -> Prims.l_True) +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl:Core.Clone.t_Clone t_Feature + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1:Core.Marker.t_Copy t_Feature + /// Initialize CPU detection. val init: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)