Improve Hax proofs.

This PR improves the hax proofs by removing some admitted parts. It focuses on the v1 module and chain.rs. The main improvements come from the use of refinement types, and from some hax improvements around loops and more (not released yet which is why this is a draft PR for now).

Co-authored-by: Maxime Buyse <maxime@cryspen.com>
Co-authored-by: maximebuyse <45398004+maximebuyse@users.noreply.github.com>

.github/workflows/hax.yml

@@ -13,8 +13,8 @@ jobs:
       - name: ⤵ Install and configure hax
         uses: hacspec/hax-actions@main
         with:
-          fstar: v2025.02.17
-          hax_reference: hax-lib-v0.3.5
+          fstar: v2025.10.06
+          hax_reference: hax-lib-v0.3.6 
 
       - run: sudo apt-get install protobuf-compiler
 

Cargo.lock

@@ -132,9 +132,9 @@ checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75"
 
 [[package]]
 name = "core-models"
-version = "0.0.4"
+version = "0.0.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0940496e5c83c54f3b753d5317daec82e8edac71c33aaa1f666d76f518de2444"
+checksum = "657f625ff361906f779745d08375ae3cc9fef87a35fba5f22874cf773010daf4"
 dependencies = [
  "hax-lib",
  "pastey",
@@ -328,9 +328,9 @@ checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289"
 
 [[package]]
 name = "hax-lib"
-version = "0.3.5"
+version = "0.3.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "74d9ba66d1739c68e0219b2b2238b5c4145f491ebf181b9c6ab561a19352ae86"
+checksum = "543f93241d32b3f00569201bfce9d7a93c92c6421b23c77864ac929dc947b9fc"
 dependencies = [
  "hax-lib-macros",
  "num-bigint",
@@ -339,9 +339,9 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros"
-version = "0.3.5"
+version = "0.3.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "24ba777a231a58d1bce1d68313fa6b6afcc7966adef23d60f45b8a2b9b688bf1"
+checksum = "f8755751e760b11021765bb04cb4a6c4e24742688d9f3aa14c2079638f537b0f"
 dependencies = [
  "hax-lib-macros-types",
  "proc-macro-error2",
@@ -352,9 +352,9 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros-types"
-version = "0.3.5"
+version = "0.3.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "867e19177d7425140b417cd27c2e05320e727ee682e98368f88b7194e80ad515"
+checksum = "f177c9ae8ea456e2f71ff3c1ea47bf4464f772a05133fcbba56cd5ba169035a2"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -465,9 +465,9 @@ dependencies = [
 
 [[package]]
 name = "libcrux-hmac"
-version = "0.0.4"
+version = "0.0.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9f0e8011bfcdb6059127e673ec0e1fc7b2a3705c683ade9d708875ed4c26cd8d"
+checksum = "8a7a242707d65960770bd7e14e4f18a92bdf0b967777dd404887db8d087a643b"
 dependencies = [
  "libcrux-hacl-rs",
  "libcrux-macros",
@@ -476,9 +476,9 @@ dependencies = [
 
 [[package]]
 name = "libcrux-intrinsics"
-version = "0.0.4"
+version = "0.0.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bc9ee7ef66569dd7516454fe26de4e401c0c62073929803486b96744594b9632"
+checksum = "b1b5db005ff8001e026b73a6842ee81bbef8ec5ff0e1915a67ae65fd2a9fafa5"
 dependencies = [
  "core-models",
  "hax-lib",
@@ -496,9 +496,9 @@ dependencies = [
 
 [[package]]
 name = "libcrux-ml-kem"
-version = "0.0.5"
+version = "0.0.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "22a36f21056e552438dbe6ce413b6682001795e53bd1f0e2c941d7e231238e5a"
+checksum = "aca7de713c6dddcf7aaf76e8ef9dc0097c8d7ce23a8eadf04c8761734714e184"
 dependencies = [
  "hax-lib",
  "libcrux-intrinsics",
@@ -519,18 +519,18 @@ dependencies = [
 
 [[package]]
 name = "libcrux-secrets"
-version = "0.0.4"
+version = "0.0.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6e4dbbf6bc9f2bc0f20dc3bea3e5c99adff3bdccf6d2a40488963da69e2ec307"
+checksum = "1ce650f3041b44ba40d4263852347d007cd2cd9d1cc856a6f6c8b2e10c3fd40b"
 dependencies = [
  "hax-lib",
 ]
 
 [[package]]
 name = "libcrux-sha2"
-version = "0.0.4"
+version = "0.0.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "649d9401e6e1954f58531b8eb13b12c800f85bbadc93362871b63a1f8a8d6d32"
+checksum = "e9d253473f259fc74a280c43f29c464f7e374abdf28b4942234dc707f529d4b7"
 dependencies = [
  "libcrux-hacl-rs",
  "libcrux-macros",
@@ -539,9 +539,9 @@ dependencies = [
 
 [[package]]
 name = "libcrux-sha3"
-version = "0.0.5"
+version = "0.0.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "18e869fdeb9af62c55c3fcd60ce407552eb282d727550ce986abac94a3474479"
+checksum = "8c50f6e04a184511b782c5cc1eb6a227c6d36f2c935e93d698655a93a99696b5"
 dependencies = [
  "hax-lib",
  "libcrux-intrinsics",
@@ -551,9 +551,9 @@ dependencies = [
 
 [[package]]
 name = "libcrux-traits"
-version = "0.0.4"
+version = "0.0.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9adfd58e79d860f6b9e40e35127bfae9e5bd3ade33201d1347459011a2add034"
+checksum = "812e4fa89f3f5e34b47f928b22b1b78395a0d4ec23b1f583db635f128159d65f"
 dependencies = [
  "libcrux-secrets",
  "rand 0.9.1",
@@ -665,9 +665,9 @@ checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
 
 [[package]]
 name = "pastey"
-version = "0.1.1"
+version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "35fb2e5f958ec131621fdd531e9fc186ed768cbe395337403ae56c17a74c68ec"
+checksum = "b867cad97c0791bbd3aaa6472142568c6c9e8f71937e98379f584cfb0cf35bec"
 
 [[package]]
 name = "petgraph"
@@ -1075,7 +1075,7 @@ checksum = "d372029cb5195f9ab4e4b9aef550787dce78b124fcaee8d82519925defcd6f0d"
 
 [[package]]
 name = "spqr"
-version = "1.4.0"
+version = "1.5.0"
 dependencies = [
  "cpufeatures",
  "curve25519-dalek",

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "spqr"
-version = "1.4.0"
+version = "1.5.0"
 edition = "2021"
 license = "AGPL-3.0-only"
 rust-version = "1.83.0"
@@ -10,10 +10,10 @@ rust-version = "1.83.0"
 [dependencies]
 curve25519-dalek = { version = "4.1.3", features = ["rand_core"] }
 displaydoc = "0.2"
-hax-lib = "0.3.5"
+hax-lib = "0.3.6"
 hkdf = "0.12"
-libcrux-hmac = "0.0.4"
-libcrux-ml-kem = { version = "0.0.5", default-features = false, features = ["incremental", "mlkem768"] }
+libcrux-hmac = "0.0.6"
+libcrux-ml-kem = { version = "0.0.7", default-features = false, features = ["incremental", "mlkem768"] }
 log = "0.4.21"
 num_enum = "0.7.3"
 prost = "0.14.1"

proofs/fstar/extraction/Makefile

@@ -70,40 +70,22 @@ endif
 
 # The following is a bash script that discovers F* libraries.
 # Due to incompatibilities with make 4.3, I had to make a "oneliner" bash script...
-define FINDLIBS
-    : "Prints a path if and only if it exists. Takes one argument: the path."; \
-    function print_if_exists() { \
-        if [ -d "$$1" ]; then \
-            echo "$$1"; \
-        fi; \
-    } ; \
-    : "Asks Cargo all the dependencies for the current crate or workspace,"; \
-    : "and extract all "root" directories for each. Takes zero argument."; \
-    function dependencies() { \
-        cargo metadata --format-version 1 | \
-            jq -r ".packages | .[] | .manifest_path | split(\"/\") | .[:-1] | join(\"/\")"; \
-    } ; \
-    : "Find hax libraries *around* a given path. Takes one argument: the"; \
-    : "path."; \
-    function find_hax_libraries_at_path() { \
-        path="$$1" ; \
-        : "if there is a [proofs/fstar/extraction] subfolder, then that s a F* library" ; \
-        print_if_exists "$$path/proofs/fstar/extraction" ; \
-        : "Maybe the [proof-libs] folder of hax is around?" ; \
-        MAYBE_PROOF_LIBS=$$(realpath -q "$$path/proof-libs/fstar" || realpath -q "$$path/../proof-libs/fstar") ; \
-        if [ -n "$$MAYBE_PROOF_LIBS" ]; then \
-            print_if_exists "$$MAYBE_PROOF_LIBS/core" ; \
-            print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" ; \
-        fi ; \
-    } ; \
-    { while IFS= read path; do \
-          find_hax_libraries_at_path "$$path"; \
-      done < <(dependencies) ; } | sort -u
-endef
-export FINDLIBS
+FINDLIBS_OUTPUT := $(shell \
+	MANIFEST=$$(cargo metadata --format-version 1 | jq -r '.resolve.root as $$root | .packages as $$pkgs | .resolve.nodes[] | select(.id == $$root) | .dependencies[] as $$dep | select($$dep | contains("hax-lib")) | $$pkgs[] | select(.id == $$dep) | .manifest_path' 2>/dev/null); \
+	if [ -n "$$MANIFEST" ] && [ "$$MANIFEST" != "null" ]; then \
+		DIR=$$(dirname "$$MANIFEST"); \
+		[ -d "$$DIR/proofs/fstar/extraction" ] && echo "$$DIR/proofs/fstar/extraction"; \
+		for p in "$$DIR/proof-libs/fstar" "$$DIR/../proof-libs/fstar"; do \
+			if [ -d "$$p" ]; then \
+				echo "$$p/core"; \
+				echo "$$p/rust_primitives"; \
+				break; \
+			fi; \
+		done; \
+	fi | sort -u)
+
 
 FSTAR_INCLUDE_DIRS_EXTRA ?=
-FINDLIBS_OUTPUT := $(shell bash -c '${FINDLIBS}')
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(FSTAR_INCLUDE_DIRS_EXTRA) $(FINDLIBS_OUTPUT) ../models
 
 # Make sure FSTAR_INCLUDE_DIRS has the `proof-libs`, print hints and

proofs/fstar/models/BitVecEq.fsti

@@ -1,6 +1,6 @@
 module BitVecEq
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
-open Core
+open Core_models
 open FStar.Mul
 open MkSeq
 open FStar.FunctionalExtensionality

proofs/fstar/models/Bytes.Buf.Buf_impl.fsti

@@ -1,6 +1,6 @@
 module Bytes.Buf.Buf_impl
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 val sign_extend (v_val: u64) (nbytes: usize) : Prims.Pure i64 Prims.l_True (fun _ -> Prims.l_True)
@@ -251,7 +251,7 @@ val impl_1 (#v_T: Type0) {| i0: t_Buf v_T |} : t_Buf (Alloc.Boxed.t_Box v_T Allo
 val impl_2:t_Buf (t_Slice u8)
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_3 (#v_T: Type0) {| i1: Core.Convert.t_AsRef v_T (t_Slice u8) |}
+val impl_3 (#v_T: Type0) {| i1: Core_models.Convert.t_AsRef v_T (t_Slice u8) |}
     : t_Buf (Std.Io.Cursor.t_Cursor v_T) 
 
 val v__assert_trait_object (v__b: dyn 1 (fun z -> t_Buf z))

proofs/fstar/models/Bytes.Buf.Buf_mut.fsti

@@ -1,6 +1,6 @@
 module Bytes.Buf.Buf_mut
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 

proofs/fstar/models/Libcrux_hmac.fsti

@@ -1,6 +1,6 @@
 module Libcrux_hmac
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 /// The HMAC algorithm defining the used hash function.
@@ -14,19 +14,19 @@ val t_Algorithm_cast_to_repr (x: t_Algorithm)
     : Prims.Pure isize Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_1:Core.Clone.t_Clone t_Algorithm
+val impl_1:Core_models.Clone.t_Clone t_Algorithm
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl:Core.Marker.t_Copy t_Algorithm
+val impl:Core_models.Marker.t_Copy t_Algorithm
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_2:Core.Fmt.t_Debug t_Algorithm
+val impl_2:Core_models.Fmt.t_Debug t_Algorithm
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_3:Core.Marker.t_StructuralPartialEq t_Algorithm
+val impl_3:Core_models.Marker.t_StructuralPartialEq t_Algorithm
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_4:Core.Cmp.t_PartialEq t_Algorithm t_Algorithm
+val impl_4:Core_models.Cmp.t_PartialEq t_Algorithm t_Algorithm
 
 /// Get the tag size for a given algorithm.
 val tag_size (alg: t_Algorithm) : Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
@@ -35,7 +35,7 @@ val tag_size (alg: t_Algorithm) : Prims.Pure usize Prims.l_True (fun _ -> Prims.
 /// output tag length of `tag_length`.
 /// Returns a vector of length `tag_length`.
 /// Panics if either `key` or `data` are longer than `u32::MAX`.
-val hmac (alg: t_Algorithm) (key data: t_Slice u8) (tag_length: Core.Option.t_Option usize)
+val hmac (alg: t_Algorithm) (key data: t_Slice u8) (tag_length: Core_models.Option.t_Option usize)
     : Prims.Pure (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
       Prims.l_True
       (ensures
@@ -49,21 +49,21 @@ val hmac (alg: t_Algorithm) (key data: t_Slice u8) (tag_length: Core.Option.t_Op
             | Algorithm_Sha512  -> mk_usize 64
           in
           match
-            (match tag_length <: Core.Option.t_Option usize with
-              | Core.Option.Option_Some l ->
+            (match tag_length <: Core_models.Option.t_Option usize with
+              | Core_models.Option.Option_Some l ->
                 (match l <=. native_tag_length <: bool with
                   | true ->
-                    Core.Option.Option_Some
+                    Core_models.Option.Option_Some
                     ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global result <: usize) =. l)
                     <:
-                    Core.Option.t_Option bool
-                  | _ -> Core.Option.Option_None <: Core.Option.t_Option bool)
-              | _ -> Core.Option.Option_None <: Core.Option.t_Option bool)
+                    Core_models.Option.t_Option bool
+                  | _ -> Core_models.Option.Option_None <: Core_models.Option.t_Option bool)
+              | _ -> Core_models.Option.Option_None <: Core_models.Option.t_Option bool)
             <:
-            Core.Option.t_Option bool
+            Core_models.Option.t_Option bool
           with
-          | Core.Option.Option_Some x -> x
-          | Core.Option.Option_None  ->
+          | Core_models.Option.Option_Some x -> x
+          | Core_models.Option.Option_None  ->
             (Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global result <: usize) =. native_tag_length)
 
 (* item error backend: (DirectAndMut) The mutation of this &mut is not allowed here.
@@ -76,8 +76,8 @@ Last available AST for this item:
 #[register_tool(_hax)]
 fn wrap_bufalloc<const N: int, F>(f: F) -> alloc::vec::t_Vec<int, alloc::alloc::t_Global>
 where
-    _: core::ops::function::t_Fn<F, tuple1<&mut [int; N]>>,
-    F: core::ops::function::t_FnOnce<f_Output = tuple0>,
+    _: core_models::ops::function::t_Fn<F, tuple1<&mut [int; N]>>,
+    F: core_models::ops::function::t_FnOnce<f_Output = tuple0>,
 {
     rust_primitives::hax::dropped_body
 }

proofs/fstar/models/Libcrux_ml_kem.Constants.fst

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Constants
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 /// Each field element needs floor(log_2(FIELD_MODULUS)) + 1 = 12 bits to represent

proofs/fstar/models/Libcrux_ml_kem.Hash_functions.Portable.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Hash_functions.Portable
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 /// The state.

proofs/fstar/models/Libcrux_ml_kem.Hash_functions.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Hash_functions
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 /// The SHA3 block size.

proofs/fstar/models/Libcrux_ml_kem.Ind_cca.Incremental.Types.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Ind_cca.Incremental.Types
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 let _ =
@@ -20,30 +20,30 @@ type t_Error =
 val t_Error_cast_to_repr (x: t_Error) : Prims.Pure isize Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_15:Core.Fmt.t_Debug t_Error
+val impl_15:Core_models.Fmt.t_Debug t_Error
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_16:Core.Clone.t_Clone t_Error
+val impl_16:Core_models.Clone.t_Clone t_Error
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_17:Core.Marker.t_Copy t_Error
+val impl_17:Core_models.Marker.t_Copy t_Error
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_18:Core.Marker.t_StructuralPartialEq t_Error
+val impl_18:Core_models.Marker.t_StructuralPartialEq t_Error
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_19:Core.Cmp.t_PartialEq t_Error t_Error
+val impl_19:Core_models.Cmp.t_PartialEq t_Error t_Error
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_20:Core.Cmp.t_Eq t_Error
+val impl_20:Core_models.Cmp.t_Eq t_Error
 
 /// Incremental trait for unpacked key pairs.
 class t_IncrementalKeyPair (v_Self: Type0) = {
   f_pk1_bytes_pre:v_Self -> t_Slice u8 -> Type0;
-  f_pk1_bytes_post:v_Self -> t_Slice u8 -> (t_Slice u8 & Core.Result.t_Result Prims.unit t_Error)
+  f_pk1_bytes_post:v_Self -> t_Slice u8 -> (t_Slice u8 & Core_models.Result.t_Result Prims.unit t_Error)
     -> Type0;
   f_pk1_bytes:x0: v_Self -> x1: t_Slice u8
-    -> Prims.Pure (t_Slice u8 & Core.Result.t_Result Prims.unit t_Error)
+    -> Prims.Pure (t_Slice u8 & Core_models.Result.t_Result Prims.unit t_Error)
         (f_pk1_bytes_pre x0 x1)
         (fun result -> f_pk1_bytes_post x0 x1 result);
   f_pk2_bytes_pre:v_Self -> t_Slice u8 -> Type0;
@@ -66,55 +66,55 @@ type t_PublicKey1 = {
 }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_21:Core.Default.t_Default t_PublicKey1
+val impl_21:Core_models.Default.t_Default t_PublicKey1
 
 /// Get the size of the first public key in bytes.
 val impl_PublicKey1__len: Prims.unit -> Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_2: Core.Convert.t_TryFrom t_PublicKey1 (t_Slice u8) =
+let impl_2: Core_models.Convert.t_TryFrom t_PublicKey1 (t_Slice u8) =
   {
     f_Error = t_Error;
     f_try_from_pre = (fun (value: t_Slice u8) -> true);
     f_try_from_post
     =
-    (fun (value: t_Slice u8) (out: Core.Result.t_Result t_PublicKey1 t_Error) -> true);
+    (fun (value: t_Slice u8) (out: Core_models.Result.t_Result t_PublicKey1 t_Error) -> true);
     f_try_from
     =
     fun (value: t_Slice u8) ->
-      if (Core.Slice.impl__len #u8 value <: usize) <. mk_usize 64
+      if (Core_models.Slice.impl__len #u8 value <: usize) <. mk_usize 64
       then
-        Core.Result.Result_Err (Error_InvalidInputLength <: t_Error)
+        Core_models.Result.Result_Err (Error_InvalidInputLength <: t_Error)
         <:
-        Core.Result.t_Result t_PublicKey1 t_Error
+        Core_models.Result.t_Result t_PublicKey1 t_Error
       else
         let seed:t_Array u8 (mk_usize 32) = Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 32) in
         let seed:t_Array u8 (mk_usize 32) =
-          Core.Slice.impl__copy_from_slice #u8
+          Core_models.Slice.impl__copy_from_slice #u8
             seed
-            (value.[ { Core.Ops.Range.f_start = mk_usize 0; Core.Ops.Range.f_end = mk_usize 32 }
+            (value.[ { Core_models.Ops.Range.f_start = mk_usize 0; Core_models.Ops.Range.f_end = mk_usize 32 }
                 <:
-                Core.Ops.Range.t_Range usize ]
+                Core_models.Ops.Range.t_Range usize ]
               <:
               t_Slice u8)
         in
         let hash:t_Array u8 (mk_usize 32) = Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 32) in
         let hash:t_Array u8 (mk_usize 32) =
-          Core.Slice.impl__copy_from_slice #u8
+          Core_models.Slice.impl__copy_from_slice #u8
             hash
-            (value.[ { Core.Ops.Range.f_start = mk_usize 32; Core.Ops.Range.f_end = mk_usize 64 }
+            (value.[ { Core_models.Ops.Range.f_start = mk_usize 32; Core_models.Ops.Range.f_end = mk_usize 64 }
                 <:
-                Core.Ops.Range.t_Range usize ]
+                Core_models.Ops.Range.t_Range usize ]
               <:
               t_Slice u8)
         in
-        Core.Result.Result_Ok ({ f_seed = seed; f_hash = hash } <: t_PublicKey1)
+        Core_models.Result.Result_Ok ({ f_seed = seed; f_hash = hash } <: t_PublicKey1)
         <:
-        Core.Result.t_Result t_PublicKey1 t_Error
+        Core_models.Result.t_Result t_PublicKey1 t_Error
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_3:Core.Convert.t_From t_PublicKey1 (t_Array u8 (mk_usize 64))
+val impl_3:Core_models.Convert.t_From t_PublicKey1 (t_Array u8 (mk_usize 64))
 
 /// The incremental public key that allows generating [`Ciphertext2`].
 /// This public key is serialized to safe bytes on the wire.
@@ -137,7 +137,8 @@ val impl_4__deserialize
 type t_Ciphertext1 (v_LEN: usize) = { f_value:t_Array u8 v_LEN }
 
 /// The size of the ciphertext.
-val impl_5__len: v_LEN: usize -> Prims.unit -> Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
+val impl_5__len: v_LEN: usize -> Prims.unit -> Prims.Pure usize Prims.l_True 
+  (ensures fun res -> let res:usize = res in res =. v_LEN)
 
 /// The partial ciphertext c2 - second part.
 type t_Ciphertext2 (v_LEN: usize) = { f_value:t_Array u8 v_LEN }
@@ -170,7 +171,7 @@ val impl_7__to_bytes
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (self: t_EncapsState v_K v_Vector)
       (state: t_Slice u8)
-    : Prims.Pure (t_Slice u8 & Core.Result.t_Result Prims.unit t_Error)
+    : Prims.Pure (t_Slice u8 & Core_models.Result.t_Result Prims.unit t_Error)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
@@ -180,7 +181,7 @@ val impl_7__try_from_bytes
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (bytes: t_Slice u8)
-    : Prims.Pure (Core.Result.t_Result (t_EncapsState v_K v_Vector) t_Error)
+    : Prims.Pure (Core_models.Result.t_Result (t_EncapsState v_K v_Vector) t_Error)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
@@ -199,7 +200,7 @@ val impl_8
       (v_K: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-    : Core.Convert.t_From t_PublicKey1
+    : Core_models.Convert.t_From t_PublicKey1
       (Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K v_Vector)
 
 /// Convert [`MlKemPublicKeyUnpacked`] to a [`PublicKey2`].
@@ -208,45 +209,45 @@ val impl_9
       (v_K v_LEN: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-    : Core.Convert.t_From (t_PublicKey2 v_LEN)
+    : Core_models.Convert.t_From (t_PublicKey2 v_LEN)
       (Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemPublicKeyUnpacked v_K v_Vector)
 
 /// Convert a byte slice `&[u8]` to a [`PublicKey2`].
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_10 (v_LEN: usize) : Core.Convert.t_TryFrom (t_PublicKey2 v_LEN) (t_Slice u8) =
+let impl_10 (v_LEN: usize) : Core_models.Convert.t_TryFrom (t_PublicKey2 v_LEN) (t_Slice u8) =
   {
     f_Error = t_Error;
     f_try_from_pre = (fun (value: t_Slice u8) -> true);
     f_try_from_post
     =
-    (fun (value: t_Slice u8) (out: Core.Result.t_Result (t_PublicKey2 v_LEN) t_Error) -> true);
+    (fun (value: t_Slice u8) (out: Core_models.Result.t_Result (t_PublicKey2 v_LEN) t_Error) -> true);
     f_try_from
     =
     fun (value: t_Slice u8) ->
-      if (Core.Slice.impl__len #u8 value <: usize) <. v_LEN
+      if (Core_models.Slice.impl__len #u8 value <: usize) <. v_LEN
       then
-        Core.Result.Result_Err (Error_InvalidInputLength <: t_Error)
+        Core_models.Result.Result_Err (Error_InvalidInputLength <: t_Error)
         <:
-        Core.Result.t_Result (t_PublicKey2 v_LEN) t_Error
+        Core_models.Result.t_Result (t_PublicKey2 v_LEN) t_Error
       else
         let tt_as_ntt:t_Array u8 v_LEN = Rust_primitives.Hax.repeat (mk_u8 0) v_LEN in
         let tt_as_ntt:t_Array u8 v_LEN =
-          Core.Slice.impl__copy_from_slice #u8
+          Core_models.Slice.impl__copy_from_slice #u8
             tt_as_ntt
-            (value.[ { Core.Ops.Range.f_start = mk_usize 0; Core.Ops.Range.f_end = v_LEN }
+            (value.[ { Core_models.Ops.Range.f_start = mk_usize 0; Core_models.Ops.Range.f_end = v_LEN }
                 <:
-                Core.Ops.Range.t_Range usize ]
+                Core_models.Ops.Range.t_Range usize ]
               <:
               t_Slice u8)
         in
-        Core.Result.Result_Ok ({ f_tt_as_ntt = tt_as_ntt } <: t_PublicKey2 v_LEN)
+        Core_models.Result.Result_Ok ({ f_tt_as_ntt = tt_as_ntt } <: t_PublicKey2 v_LEN)
         <:
-        Core.Result.t_Result (t_PublicKey2 v_LEN) t_Error
+        Core_models.Result.t_Result (t_PublicKey2 v_LEN) t_Error
   }
 
 /// Convert bytes `&[u8; LEN]` to a [`PublicKey2`].
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_11 (v_LEN: usize) : Core.Convert.t_From (t_PublicKey2 v_LEN) (t_Array u8 v_LEN)
+val impl_11 (v_LEN: usize) : Core_models.Convert.t_From (t_PublicKey2 v_LEN) (t_Array u8 v_LEN)
 
 type t_KeyPair
   (v_K: usize) (v_PK2_LEN: usize) (v_Vector: Type0)
@@ -263,7 +264,7 @@ val impl_12
       (v_K v_PK2_LEN: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-    : Core.Convert.t_From (t_KeyPair v_K v_PK2_LEN v_Vector)
+    : Core_models.Convert.t_From (t_KeyPair v_K v_PK2_LEN v_Vector)
       (Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K v_Vector)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
@@ -271,7 +272,7 @@ val impl_13
       (v_K v_PK2_LEN: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-    : Core.Convert.t_From (Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K v_Vector)
+    : Core_models.Convert.t_From (Libcrux_ml_kem.Ind_cca.Unpacked.t_MlKemKeyPairUnpacked v_K v_Vector)
       (t_KeyPair v_K v_PK2_LEN v_Vector)
 
 /// Write `value` into `out` at `offset`.
@@ -285,7 +286,7 @@ val impl_14__pk1_bytes
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (self: t_KeyPair v_K v_PK2_LEN v_Vector)
       (pk1: t_Slice u8)
-    : Prims.Pure (t_Slice u8 & Core.Result.t_Result Prims.unit t_Error)
+    : Prims.Pure (t_Slice u8 & Core_models.Result.t_Result Prims.unit t_Error)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
@@ -296,7 +297,7 @@ val impl_14__pk2_bytes
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (self: t_KeyPair v_K v_PK2_LEN v_Vector)
       (pk2: t_Slice u8)
-    : Prims.Pure (t_Slice u8 & Core.Result.t_Result Prims.unit t_Error)
+    : Prims.Pure (t_Slice u8 & Core_models.Result.t_Result Prims.unit t_Error)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
@@ -317,7 +318,7 @@ val impl_14__to_bytes
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (self: t_KeyPair v_K v_PK2_LEN v_Vector)
       (key: t_Slice u8)
-    : Prims.Pure (t_Slice u8 & Core.Result.t_Result Prims.unit t_Error)
+    : Prims.Pure (t_Slice u8 & Core_models.Result.t_Result Prims.unit t_Error)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
@@ -341,6 +342,6 @@ val impl_14__from_bytes
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (key: t_Slice u8)
-    : Prims.Pure (Core.Result.t_Result (t_KeyPair v_K v_PK2_LEN v_Vector) t_Error)
+    : Prims.Pure (Core_models.Result.t_Result (t_KeyPair v_K v_PK2_LEN v_Vector) t_Error)
       Prims.l_True
       (fun _ -> Prims.l_True)

proofs/fstar/models/Libcrux_ml_kem.Ind_cca.Unpacked.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Ind_cca.Unpacked
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 let _ =
@@ -34,11 +34,11 @@ type t_MlKemPublicKeyUnpacked
 let impl_2
       (v_K: usize)
       (#v_Vector: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_Vector)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core_models.Clone.t_Clone v_Vector)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
           i2:
           Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector)
-    : Core.Clone.t_Clone (t_MlKemPublicKeyUnpacked v_K v_Vector) = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
+    : Core_models.Clone.t_Clone (t_MlKemPublicKeyUnpacked v_K v_Vector) = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
 
 /// An unpacked ML-KEM KeyPair
 type t_MlKemKeyPairUnpacked
@@ -149,7 +149,7 @@ val impl
       (v_K: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-    : Core.Default.t_Default (t_MlKemPublicKeyUnpacked v_K v_Vector)
+    : Core_models.Default.t_Default (t_MlKemPublicKeyUnpacked v_K v_Vector)
 
 /// Take a serialized private key and generate an unpacked key pair from it.
 val keys_from_private_key
@@ -277,7 +277,7 @@ val impl_1
       (v_K: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-    : Core.Default.t_Default (t_MlKemKeyPairUnpacked v_K v_Vector)
+    : Core_models.Default.t_Default (t_MlKemKeyPairUnpacked v_K v_Vector)
 
 /// Create a new empty unpacked key pair.
 val impl_4__new:
@@ -358,8 +358,8 @@ val encaps_prepare
       (randomness pk_hash: t_Slice u8)
     : Prims.Pure (t_Array u8 (mk_usize 64))
       (requires
-        (Core.Slice.impl__len #u8 randomness <: usize) =. mk_usize 32 &&
-        (Core.Slice.impl__len #u8 pk_hash <: usize) =. mk_usize 32)
+        (Core_models.Slice.impl__len #u8 randomness <: usize) =. mk_usize 32 &&
+        (Core_models.Slice.impl__len #u8 pk_hash <: usize) =. mk_usize 32)
       (ensures
         fun result ->
           let result:t_Array u8 (mk_usize 64) = result in

proofs/fstar/models/Libcrux_ml_kem.Ind_cpa.Unpacked.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Ind_cpa.Unpacked
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 let _ =
@@ -19,7 +19,7 @@ val impl
       (v_K: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-    : Core.Default.t_Default (t_IndCpaPrivateKeyUnpacked v_K v_Vector)
+    : Core_models.Default.t_Default (t_IndCpaPrivateKeyUnpacked v_K v_Vector)
 
 /// An unpacked ML-KEM IND-CPA Public Key
 type t_IndCpaPublicKeyUnpacked
@@ -33,15 +33,15 @@ type t_IndCpaPublicKeyUnpacked
 let impl_2
       (v_K: usize)
       (#v_Vector: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_Vector)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core_models.Clone.t_Clone v_Vector)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
           i2:
           Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector)
-    : Core.Clone.t_Clone (t_IndCpaPublicKeyUnpacked v_K v_Vector) = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
+    : Core_models.Clone.t_Clone (t_IndCpaPublicKeyUnpacked v_K v_Vector) = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_1
       (v_K: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-    : Core.Default.t_Default (t_IndCpaPublicKeyUnpacked v_K v_Vector)
+    : Core_models.Default.t_Default (t_IndCpaPublicKeyUnpacked v_K v_Vector)

proofs/fstar/models/Libcrux_ml_kem.Mlkem768.Incremental.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Mlkem768.Incremental
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 let _ =
@@ -15,7 +15,7 @@ val pk1_len: Prims.unit -> Prims.Pure usize Prims.l_True
   (ensures fun res -> let res:usize = res in res =. mk_usize 64)
 
 /// Get the size of the second public key in bytes.
-val pk2_len: Prims.unit -> Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
+val pk2_len: Prims.unit -> Prims.Pure usize Prims.l_True (ensures fun res -> res =. mk_usize 1152)
 
 /// The size of a compressed key pair in bytes.
 let v_COMPRESSED_KEYPAIR_LEN: usize = Libcrux_ml_kem.Mlkem768.v_SECRET_KEY_SIZE
@@ -48,7 +48,7 @@ val impl_KeyPairBytes__pk2 (self: t_KeyPairBytes)
     : Prims.Pure (t_Array u8 (mk_usize 1152)) Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_1:Core.Convert.t_AsRef t_KeyPairBytes (t_Slice u8)
+val impl_1:Core_models.Convert.t_AsRef t_KeyPairBytes (t_Slice u8)
 
 /// Generate a key pair and write it into `key_pair`.
 /// This uses unpacked keys and does not compress the keys.
@@ -56,7 +56,7 @@ val impl_1:Core.Convert.t_AsRef t_KeyPairBytes (t_Slice u8)
 /// The function returns an error if this is not the case.
 val generate_key_pair (randomness: t_Array u8 (mk_usize 64)) (key_pair: t_Slice u8)
     : Prims.Pure
-      (t_Slice u8 & Core.Result.t_Result Prims.unit Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Error
+      (t_Slice u8 & Core_models.Result.t_Result Prims.unit Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Error
       ) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Generate a new key pair.
@@ -100,7 +100,7 @@ val impl_KeyPairCompressedBytes__pk2 (self: t_KeyPairCompressedBytes)
     : Prims.Pure (t_Array u8 (mk_usize 1152)) Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_3:Core.Convert.t_AsRef t_KeyPairCompressedBytes (t_Slice u8)
+val impl_3:Core_models.Convert.t_AsRef t_KeyPairCompressedBytes (t_Slice u8)
 
 /// Generate a key pair and write it into `key_pair`.
 /// This compresses the keys.
@@ -133,13 +133,13 @@ val pk2 (keypair: t_Array u8 (mk_usize 7392))
 
 /// Validate that the two parts `pk1` and `pk2` are consistent.
 val validate_pk (pk1: Libcrux_ml_kem.Ind_cca.Incremental.Types.t_PublicKey1) (pk2: t_Slice u8)
-    : Prims.Pure (Core.Result.t_Result Prims.unit Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Error)
+    : Prims.Pure (Core_models.Result.t_Result Prims.unit Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Error)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
 /// Validate that the two parts `pk1` and `pk2` are consistent.
 val validate_pk_bytes (pk1 pk2: t_Slice u8)
-    : Prims.Pure (Core.Result.t_Result Prims.unit Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Error)
+    : Prims.Pure (Core_models.Result.t_Result Prims.unit Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Error)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
@@ -152,7 +152,7 @@ val encapsulate1
       (state shared_secret: t_Slice u8)
     : Prims.Pure
       (t_Slice u8 & t_Slice u8 &
-        Core.Result.t_Result (Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Ciphertext1 (mk_usize 960))
+        Core_models.Result.t_Result (Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Ciphertext1 (mk_usize 960))
           Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Error) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Encapsulate the second part of the ciphertext.
@@ -170,7 +170,7 @@ val decapsulate_incremental_key
       (ciphertext1: Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Ciphertext1 (mk_usize 960))
       (ciphertext2: Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Ciphertext2 (mk_usize 128))
     : Prims.Pure
-      (Core.Result.t_Result (t_Array u8 (mk_usize 32))
+      (Core_models.Result.t_Result (t_Array u8 (mk_usize 32))
           Libcrux_ml_kem.Ind_cca.Incremental.Types.t_Error) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Decapsulate incremental ciphertexts.

proofs/fstar/models/Libcrux_ml_kem.Mlkem768.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Mlkem768
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 let v_RANK: usize = mk_usize 3

proofs/fstar/models/Libcrux_ml_kem.Polynomial.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Polynomial
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 let _ =
@@ -71,18 +71,18 @@ let to_spec_matrix_t (#r:Spec.MLKEM.rank) (#v_Vector: Type0)
 
 let impl
       (#v_Vector: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_Vector)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core_models.Clone.t_Clone v_Vector)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
           i2:
           Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector)
-    : Core.Clone.t_Clone (t_PolynomialRingElement v_Vector) = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
+    : Core_models.Clone.t_Clone (t_PolynomialRingElement v_Vector) = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_1
       (#v_Vector: Type0)
-      {| i1: Core.Marker.t_Copy v_Vector |}
+      {| i1: Core_models.Marker.t_Copy v_Vector |}
       {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-    : Core.Marker.t_Copy (t_PolynomialRingElement v_Vector)
+    : Core_models.Marker.t_Copy (t_PolynomialRingElement v_Vector)
 
 val v_ZERO:
     #v_Vector: Type0 ->
@@ -97,7 +97,7 @@ val from_i16_array
     : Prims.Pure (t_PolynomialRingElement v_Vector)
       (requires
         (v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize) <=.
-        (Core.Slice.impl__len #i16 a <: usize))
+        (Core_models.Slice.impl__len #i16 a <: usize))
       (fun _ -> Prims.l_True)
 
 val to_i16_array
@@ -107,7 +107,7 @@ val to_i16_array
       (out: t_Slice i16)
     : Prims.Pure (t_Slice i16)
       (requires
-        (Core.Slice.impl__len #i16 out <: usize) >=.
+        (Core_models.Slice.impl__len #i16 out <: usize) >=.
         (v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize))
       (fun _ -> Prims.l_True)
 
@@ -118,7 +118,7 @@ val from_bytes
     : Prims.Pure (t_PolynomialRingElement v_Vector)
       (requires
         ((v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize) *! mk_usize 2 <: usize) <=.
-        (Core.Slice.impl__len #u8 bytes <: usize))
+        (Core_models.Slice.impl__len #u8 bytes <: usize))
       (fun _ -> Prims.l_True)
 
 val to_bytes
@@ -129,7 +129,7 @@ val to_bytes
     : Prims.Pure (t_Slice u8)
       (requires
         ((v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize) *! mk_usize 2 <: usize) <=.
-        (Core.Slice.impl__len #u8 out <: usize))
+        (Core_models.Slice.impl__len #u8 out <: usize))
       (fun _ -> Prims.l_True)
 
 /// Given two polynomial ring elements `lhs` and `rhs`, compute the pointwise
@@ -275,7 +275,7 @@ val impl_2__from_i16_array
     : Prims.Pure (t_PolynomialRingElement v_Vector)
       (requires
         (v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize) <=.
-        (Core.Slice.impl__len #i16 a <: usize))
+        (Core_models.Slice.impl__len #i16 a <: usize))
       (fun _ -> Prims.l_True)
 
 val impl_2__to_i16_array
@@ -286,7 +286,7 @@ val impl_2__to_i16_array
     : Prims.Pure (t_Slice i16)
       (requires
         (v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize) <=.
-        (Core.Slice.impl__len #i16 out <: usize))
+        (Core_models.Slice.impl__len #i16 out <: usize))
       (fun _ -> Prims.l_True)
 
 val impl_2__from_bytes
@@ -296,7 +296,7 @@ val impl_2__from_bytes
     : Prims.Pure (t_PolynomialRingElement v_Vector)
       (requires
         ((v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize) *! mk_usize 2 <: usize) <=.
-        (Core.Slice.impl__len #u8 bytes <: usize))
+        (Core_models.Slice.impl__len #u8 bytes <: usize))
       (fun _ -> Prims.l_True)
 
 /// Build a vector of ring elements from `bytes`.
@@ -307,12 +307,12 @@ val vec_from_bytes
       (out: t_Slice (t_PolynomialRingElement v_Vector))
     : Prims.Pure (t_Slice (t_PolynomialRingElement v_Vector))
       (requires
-        (Core.Slice.impl__len #(t_PolynomialRingElement v_Vector) out <: usize) <=. mk_usize 4 &&
+        (Core_models.Slice.impl__len #(t_PolynomialRingElement v_Vector) out <: usize) <=. mk_usize 4 &&
         (((v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize) *! mk_usize 2 <: usize) *!
-          (Core.Slice.impl__len #(t_PolynomialRingElement v_Vector) out <: usize)
+          (Core_models.Slice.impl__len #(t_PolynomialRingElement v_Vector) out <: usize)
           <:
           usize) <=.
-        (Core.Slice.impl__len #u8 bytes <: usize))
+        (Core_models.Slice.impl__len #u8 bytes <: usize))
       (fun _ -> Prims.l_True)
 
 val impl_2__to_bytes
@@ -323,7 +323,7 @@ val impl_2__to_bytes
     : Prims.Pure (t_Slice u8)
       (requires
         ((v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize) *! mk_usize 2 <: usize) <=.
-        (Core.Slice.impl__len #u8 out <: usize))
+        (Core_models.Slice.impl__len #u8 out <: usize))
       (fun _ -> Prims.l_True)
 
 /// Get the bytes of the vector of ring elements in `re` and write them to `out`.
@@ -334,10 +334,10 @@ val vec_to_bytes
       (out: t_Slice u8)
     : Prims.Pure (t_Slice u8)
       (requires
-        (Core.Slice.impl__len #(t_PolynomialRingElement v_Vector) re <: usize) <=. mk_usize 4 &&
+        (Core_models.Slice.impl__len #(t_PolynomialRingElement v_Vector) re <: usize) <=. mk_usize 4 &&
         (((v_VECTORS_IN_RING_ELEMENT *! mk_usize 16 <: usize) *! mk_usize 2 <: usize) *!
-          (Core.Slice.impl__len #(t_PolynomialRingElement v_Vector) re <: usize)
+          (Core_models.Slice.impl__len #(t_PolynomialRingElement v_Vector) re <: usize)
           <:
           usize) <=.
-        (Core.Slice.impl__len #u8 out <: usize))
+        (Core_models.Slice.impl__len #u8 out <: usize))
       (fun _ -> Prims.l_True)

proofs/fstar/models/Libcrux_ml_kem.Serialize.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Serialize
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 let _ =
@@ -81,7 +81,7 @@ val deserialize_to_uncompressed_ring_element
       (serialized: t_Slice u8)
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (requires
-        (Core.Slice.impl__len #u8 serialized <: usize) =.
+        (Core_models.Slice.impl__len #u8 serialized <: usize) =.
         Libcrux_ml_kem.Constants.v_BYTES_PER_RING_ELEMENT)
       (ensures
         fun result ->
@@ -97,7 +97,7 @@ val deserialize_to_reduced_ring_element
       (serialized: t_Slice u8)
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (requires
-        (Core.Slice.impl__len #u8 serialized <: usize) =.
+        (Core_models.Slice.impl__len #u8 serialized <: usize) =.
         Libcrux_ml_kem.Constants.v_BYTES_PER_RING_ELEMENT)
       (fun _ -> Prims.l_True)
 
@@ -182,7 +182,7 @@ val compress_then_serialize_4_
       (ensures
         fun serialized_future ->
           let serialized_future:t_Slice u8 = serialized_future in
-          Core.Slice.impl__len #u8 serialized_future == Core.Slice.impl__len #u8 serialized)
+          Core_models.Slice.impl__len #u8 serialized_future == Core_models.Slice.impl__len #u8 serialized)
 
 val compress_then_serialize_5_
       (#v_Vector: Type0)
@@ -190,11 +190,11 @@ val compress_then_serialize_5_
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (serialized: t_Slice u8)
     : Prims.Pure (t_Slice u8)
-      (requires (Core.Slice.impl__len #u8 serialized <: usize) =. mk_usize 160)
+      (requires (Core_models.Slice.impl__len #u8 serialized <: usize) =. mk_usize 160)
       (ensures
         fun serialized_future ->
           let serialized_future:t_Slice u8 = serialized_future in
-          Core.Slice.impl__len #u8 serialized_future == Core.Slice.impl__len #u8 serialized)
+          Core_models.Slice.impl__len #u8 serialized_future == Core_models.Slice.impl__len #u8 serialized)
 
 val compress_then_serialize_ring_element_v
       (v_K v_COMPRESSION_FACTOR v_OUT_LEN: usize)
@@ -211,7 +211,7 @@ val compress_then_serialize_ring_element_v
       (ensures
         fun out_future ->
           let out_future:t_Slice u8 = out_future in
-          Core.Slice.impl__len #u8 out_future == Core.Slice.impl__len #u8 out /\
+          Core_models.Slice.impl__len #u8 out_future == Core_models.Slice.impl__len #u8 out /\
           out_future ==
           Spec.MLKEM.compress_then_encode_v #v_K
             (Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector re))
@@ -221,7 +221,7 @@ val deserialize_then_decompress_10_
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (serialized: t_Slice u8)
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
-      (requires (Core.Slice.impl__len #u8 serialized <: usize) =. mk_usize 320)
+      (requires (Core_models.Slice.impl__len #u8 serialized <: usize) =. mk_usize 320)
       (fun _ -> Prims.l_True)
 
 val deserialize_then_decompress_11_
@@ -229,7 +229,7 @@ val deserialize_then_decompress_11_
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (serialized: t_Slice u8)
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
-      (requires (Core.Slice.impl__len #u8 serialized <: usize) =. mk_usize 352)
+      (requires (Core_models.Slice.impl__len #u8 serialized <: usize) =. mk_usize 352)
       (fun _ -> Prims.l_True)
 
 val deserialize_then_decompress_ring_element_u
@@ -240,7 +240,7 @@ val deserialize_then_decompress_ring_element_u
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (requires
         (v_COMPRESSION_FACTOR =. mk_usize 10 || v_COMPRESSION_FACTOR =. mk_usize 11) &&
-        (Core.Slice.impl__len #u8 serialized <: usize) =.
+        (Core_models.Slice.impl__len #u8 serialized <: usize) =.
         (mk_usize 32 *! v_COMPRESSION_FACTOR <: usize))
       (ensures
         fun result ->
@@ -253,7 +253,7 @@ val deserialize_then_decompress_4_
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (serialized: t_Slice u8)
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
-      (requires (Core.Slice.impl__len #u8 serialized <: usize) =. mk_usize 128)
+      (requires (Core_models.Slice.impl__len #u8 serialized <: usize) =. mk_usize 128)
       (fun _ -> Prims.l_True)
 
 val deserialize_then_decompress_5_
@@ -261,7 +261,7 @@ val deserialize_then_decompress_5_
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (serialized: t_Slice u8)
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
-      (requires (Core.Slice.impl__len #u8 serialized <: usize) =. mk_usize 160)
+      (requires (Core_models.Slice.impl__len #u8 serialized <: usize) =. mk_usize 160)
       (fun _ -> Prims.l_True)
 
 val deserialize_then_decompress_ring_element_v

proofs/fstar/models/Libcrux_ml_kem.Types.fst

@@ -1,13 +1,13 @@
 module Libcrux_ml_kem.Types
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 ///An ML-KEM Ciphertext
 type t_MlKemCiphertext (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl (v_SIZE: usize) : Core.Default.t_Default (t_MlKemCiphertext v_SIZE) =
+let impl (v_SIZE: usize) : Core_models.Default.t_Default (t_MlKemCiphertext v_SIZE) =
   {
     f_default_pre = (fun (_: Prims.unit) -> true);
     f_default_post = (fun (_: Prims.unit) (out: t_MlKemCiphertext v_SIZE) -> true);
@@ -18,7 +18,7 @@ let impl (v_SIZE: usize) : Core.Default.t_Default (t_MlKemCiphertext v_SIZE) =
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_4 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemCiphertext v_SIZE) (t_Slice u8) =
+let impl_4 (v_SIZE: usize) : Core_models.Convert.t_AsRef (t_MlKemCiphertext v_SIZE) (t_Slice u8) =
   {
     f_as_ref_pre = (fun (self: t_MlKemCiphertext v_SIZE) -> true);
     f_as_ref_post
@@ -28,7 +28,7 @@ let impl_4 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemCiphertext v_SIZE) (t_
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_5 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
+let impl_5 (v_SIZE: usize) : Core_models.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
   {
     f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
     f_from_post
@@ -38,20 +38,20 @@ let impl_5 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_A
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
+let impl_1 (v_SIZE: usize) : Core_models.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
   {
     f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
     f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemCiphertext v_SIZE) -> true);
     f_from
     =
     fun (value: t_Array u8 v_SIZE) ->
-      { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
+      { f_value = Core_models.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
       <:
       t_MlKemCiphertext v_SIZE
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemCiphertext v_SIZE) =
+let impl_2 (v_SIZE: usize) : Core_models.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemCiphertext v_SIZE) =
   {
     f_from_pre = (fun (value: t_MlKemCiphertext v_SIZE) -> true);
     f_from_post = (fun (value: t_MlKemCiphertext v_SIZE) (out: t_Array u8 v_SIZE) -> true);
@@ -59,36 +59,36 @@ let impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemCip
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_3 (v_SIZE: usize) : Core.Convert.t_TryFrom (t_MlKemCiphertext v_SIZE) (t_Slice u8) =
+let impl_3 (v_SIZE: usize) : Core_models.Convert.t_TryFrom (t_MlKemCiphertext v_SIZE) (t_Slice u8) =
   {
-    f_Error = Core.Array.t_TryFromSliceError;
+    f_Error = Core_models.Array.t_TryFromSliceError;
     f_try_from_pre = (fun (value: t_Slice u8) -> true);
     f_try_from_post
     =
     (fun
         (value: t_Slice u8)
-        (out: Core.Result.t_Result (t_MlKemCiphertext v_SIZE) Core.Array.t_TryFromSliceError)
+        (out: Core_models.Result.t_Result (t_MlKemCiphertext v_SIZE) Core_models.Array.t_TryFromSliceError)
         ->
         true);
     f_try_from
     =
     fun (value: t_Slice u8) ->
       match
-        Core.Convert.f_try_into #(t_Slice u8)
+        Core_models.Convert.f_try_into #(t_Slice u8)
           #(t_Array u8 v_SIZE)
           #FStar.Tactics.Typeclasses.solve
           value
         <:
-        Core.Result.t_Result (t_Array u8 v_SIZE) Core.Array.t_TryFromSliceError
+        Core_models.Result.t_Result (t_Array u8 v_SIZE) Core_models.Array.t_TryFromSliceError
       with
-      | Core.Result.Result_Ok value ->
-        Core.Result.Result_Ok ({ f_value = value } <: t_MlKemCiphertext v_SIZE)
+      | Core_models.Result.Result_Ok value ->
+        Core_models.Result.Result_Ok ({ f_value = value } <: t_MlKemCiphertext v_SIZE)
         <:
-        Core.Result.t_Result (t_MlKemCiphertext v_SIZE) Core.Array.t_TryFromSliceError
-      | Core.Result.Result_Err e ->
-        Core.Result.Result_Err e
+        Core_models.Result.t_Result (t_MlKemCiphertext v_SIZE) Core_models.Array.t_TryFromSliceError
+      | Core_models.Result.Result_Err e ->
+        Core_models.Result.Result_Err e
         <:
-        Core.Result.t_Result (t_MlKemCiphertext v_SIZE) Core.Array.t_TryFromSliceError
+        Core_models.Result.t_Result (t_MlKemCiphertext v_SIZE) Core_models.Array.t_TryFromSliceError
   }
 
 /// The number of bytes
@@ -107,7 +107,7 @@ let impl_6__as_slice (v_SIZE: usize) (self: t_MlKemCiphertext v_SIZE)
 type t_MlKemPrivateKey (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_7 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPrivateKey v_SIZE) =
+let impl_7 (v_SIZE: usize) : Core_models.Default.t_Default (t_MlKemPrivateKey v_SIZE) =
   {
     f_default_pre = (fun (_: Prims.unit) -> true);
     f_default_post = (fun (_: Prims.unit) (out: t_MlKemPrivateKey v_SIZE) -> true);
@@ -118,7 +118,7 @@ let impl_7 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPrivateKey v_SIZE) =
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_11 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPrivateKey v_SIZE) (t_Slice u8) =
+let impl_11 (v_SIZE: usize) : Core_models.Convert.t_AsRef (t_MlKemPrivateKey v_SIZE) (t_Slice u8) =
   {
     f_as_ref_pre = (fun (self: t_MlKemPrivateKey v_SIZE) -> true);
     f_as_ref_post
@@ -128,7 +128,7 @@ let impl_11 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPrivateKey v_SIZE) (t
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_12 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) =
+let impl_12 (v_SIZE: usize) : Core_models.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) =
   {
     f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
     f_from_post
@@ -138,20 +138,20 @@ let impl_12 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_8 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) =
+let impl_8 (v_SIZE: usize) : Core_models.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) =
   {
     f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
     f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPrivateKey v_SIZE) -> true);
     f_from
     =
     fun (value: t_Array u8 v_SIZE) ->
-      { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
+      { f_value = Core_models.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
       <:
       t_MlKemPrivateKey v_SIZE
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_9 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPrivateKey v_SIZE) =
+let impl_9 (v_SIZE: usize) : Core_models.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPrivateKey v_SIZE) =
   {
     f_from_pre = (fun (value: t_MlKemPrivateKey v_SIZE) -> true);
     f_from_post = (fun (value: t_MlKemPrivateKey v_SIZE) (out: t_Array u8 v_SIZE) -> true);
@@ -159,36 +159,36 @@ let impl_9 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPri
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_10 (v_SIZE: usize) : Core.Convert.t_TryFrom (t_MlKemPrivateKey v_SIZE) (t_Slice u8) =
+let impl_10 (v_SIZE: usize) : Core_models.Convert.t_TryFrom (t_MlKemPrivateKey v_SIZE) (t_Slice u8) =
   {
-    f_Error = Core.Array.t_TryFromSliceError;
+    f_Error = Core_models.Array.t_TryFromSliceError;
     f_try_from_pre = (fun (value: t_Slice u8) -> true);
     f_try_from_post
     =
     (fun
         (value: t_Slice u8)
-        (out: Core.Result.t_Result (t_MlKemPrivateKey v_SIZE) Core.Array.t_TryFromSliceError)
+        (out: Core_models.Result.t_Result (t_MlKemPrivateKey v_SIZE) Core_models.Array.t_TryFromSliceError)
         ->
         true);
     f_try_from
     =
     fun (value: t_Slice u8) ->
       match
-        Core.Convert.f_try_into #(t_Slice u8)
+        Core_models.Convert.f_try_into #(t_Slice u8)
           #(t_Array u8 v_SIZE)
           #FStar.Tactics.Typeclasses.solve
           value
         <:
-        Core.Result.t_Result (t_Array u8 v_SIZE) Core.Array.t_TryFromSliceError
+        Core_models.Result.t_Result (t_Array u8 v_SIZE) Core_models.Array.t_TryFromSliceError
       with
-      | Core.Result.Result_Ok value ->
-        Core.Result.Result_Ok ({ f_value = value } <: t_MlKemPrivateKey v_SIZE)
+      | Core_models.Result.Result_Ok value ->
+        Core_models.Result.Result_Ok ({ f_value = value } <: t_MlKemPrivateKey v_SIZE)
         <:
-        Core.Result.t_Result (t_MlKemPrivateKey v_SIZE) Core.Array.t_TryFromSliceError
-      | Core.Result.Result_Err e ->
-        Core.Result.Result_Err e
+        Core_models.Result.t_Result (t_MlKemPrivateKey v_SIZE) Core_models.Array.t_TryFromSliceError
+      | Core_models.Result.Result_Err e ->
+        Core_models.Result.Result_Err e
         <:
-        Core.Result.t_Result (t_MlKemPrivateKey v_SIZE) Core.Array.t_TryFromSliceError
+        Core_models.Result.t_Result (t_MlKemPrivateKey v_SIZE) Core_models.Array.t_TryFromSliceError
   }
 
 /// The number of bytes
@@ -207,7 +207,7 @@ let impl_13__as_slice (v_SIZE: usize) (self: t_MlKemPrivateKey v_SIZE)
 type t_MlKemPublicKey (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_14 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPublicKey v_SIZE) =
+let impl_14 (v_SIZE: usize) : Core_models.Default.t_Default (t_MlKemPublicKey v_SIZE) =
   {
     f_default_pre = (fun (_: Prims.unit) -> true);
     f_default_post = (fun (_: Prims.unit) (out: t_MlKemPublicKey v_SIZE) -> true);
@@ -218,7 +218,7 @@ let impl_14 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPublicKey v_SIZE) =
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_18 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPublicKey v_SIZE) (t_Slice u8) =
+let impl_18 (v_SIZE: usize) : Core_models.Convert.t_AsRef (t_MlKemPublicKey v_SIZE) (t_Slice u8) =
   {
     f_as_ref_pre = (fun (self: t_MlKemPublicKey v_SIZE) -> true);
     f_as_ref_post
@@ -228,7 +228,7 @@ let impl_18 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPublicKey v_SIZE) (t_
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_19 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) =
+let impl_19 (v_SIZE: usize) : Core_models.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) =
   {
     f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
     f_from_post
@@ -238,20 +238,20 @@ let impl_19 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_A
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_15 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) =
+let impl_15 (v_SIZE: usize) : Core_models.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) =
   {
     f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
     f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPublicKey v_SIZE) -> true);
     f_from
     =
     fun (value: t_Array u8 v_SIZE) ->
-      { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
+      { f_value = Core_models.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
       <:
       t_MlKemPublicKey v_SIZE
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_16 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPublicKey v_SIZE) =
+let impl_16 (v_SIZE: usize) : Core_models.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPublicKey v_SIZE) =
   {
     f_from_pre = (fun (value: t_MlKemPublicKey v_SIZE) -> true);
     f_from_post = (fun (value: t_MlKemPublicKey v_SIZE) (out: t_Array u8 v_SIZE) -> true);
@@ -259,36 +259,36 @@ let impl_16 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPu
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_17 (v_SIZE: usize) : Core.Convert.t_TryFrom (t_MlKemPublicKey v_SIZE) (t_Slice u8) =
+let impl_17 (v_SIZE: usize) : Core_models.Convert.t_TryFrom (t_MlKemPublicKey v_SIZE) (t_Slice u8) =
   {
-    f_Error = Core.Array.t_TryFromSliceError;
+    f_Error = Core_models.Array.t_TryFromSliceError;
     f_try_from_pre = (fun (value: t_Slice u8) -> true);
     f_try_from_post
     =
     (fun
         (value: t_Slice u8)
-        (out: Core.Result.t_Result (t_MlKemPublicKey v_SIZE) Core.Array.t_TryFromSliceError)
+        (out: Core_models.Result.t_Result (t_MlKemPublicKey v_SIZE) Core_models.Array.t_TryFromSliceError)
         ->
         true);
     f_try_from
     =
     fun (value: t_Slice u8) ->
       match
-        Core.Convert.f_try_into #(t_Slice u8)
+        Core_models.Convert.f_try_into #(t_Slice u8)
           #(t_Array u8 v_SIZE)
           #FStar.Tactics.Typeclasses.solve
           value
         <:
-        Core.Result.t_Result (t_Array u8 v_SIZE) Core.Array.t_TryFromSliceError
+        Core_models.Result.t_Result (t_Array u8 v_SIZE) Core_models.Array.t_TryFromSliceError
       with
-      | Core.Result.Result_Ok value ->
-        Core.Result.Result_Ok ({ f_value = value } <: t_MlKemPublicKey v_SIZE)
+      | Core_models.Result.Result_Ok value ->
+        Core_models.Result.Result_Ok ({ f_value = value } <: t_MlKemPublicKey v_SIZE)
         <:
-        Core.Result.t_Result (t_MlKemPublicKey v_SIZE) Core.Array.t_TryFromSliceError
-      | Core.Result.Result_Err e ->
-        Core.Result.Result_Err e
+        Core_models.Result.t_Result (t_MlKemPublicKey v_SIZE) Core_models.Array.t_TryFromSliceError
+      | Core_models.Result.Result_Err e ->
+        Core_models.Result.Result_Err e
         <:
-        Core.Result.t_Result (t_MlKemPublicKey v_SIZE) Core.Array.t_TryFromSliceError
+        Core_models.Result.t_Result (t_MlKemPublicKey v_SIZE) Core_models.Array.t_TryFromSliceError
   }
 
 /// The number of bytes
@@ -318,13 +318,13 @@ let impl_21__new
   {
     f_sk
     =
-    Core.Convert.f_into #(t_Array u8 v_PRIVATE_KEY_SIZE)
+    Core_models.Convert.f_into #(t_Array u8 v_PRIVATE_KEY_SIZE)
       #(t_MlKemPrivateKey v_PRIVATE_KEY_SIZE)
       #FStar.Tactics.Typeclasses.solve
       sk;
     f_pk
     =
-    Core.Convert.f_into #(t_Array u8 v_PUBLIC_KEY_SIZE)
+    Core_models.Convert.f_into #(t_Array u8 v_PUBLIC_KEY_SIZE)
       #(t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
       #FStar.Tactics.Typeclasses.solve
       pk
@@ -409,13 +409,13 @@ let unpack_private_key (v_CPA_SECRET_KEY_SIZE v_PUBLIC_KEY_SIZE: usize) (private
           (v v_CPA_SECRET_KEY_SIZE + v v_PUBLIC_KEY_SIZE +
             v Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE)) =
   let ind_cpa_secret_key, secret_key:(t_Slice u8 & t_Slice u8) =
-    Core.Slice.impl__split_at #u8 private_key v_CPA_SECRET_KEY_SIZE
+    Core_models.Slice.impl__split_at #u8 private_key v_CPA_SECRET_KEY_SIZE
   in
   let ind_cpa_public_key, secret_key:(t_Slice u8 & t_Slice u8) =
-    Core.Slice.impl__split_at #u8 secret_key v_PUBLIC_KEY_SIZE
+    Core_models.Slice.impl__split_at #u8 secret_key v_PUBLIC_KEY_SIZE
   in
   let ind_cpa_public_key_hash, implicit_rejection_value:(t_Slice u8 & t_Slice u8) =
-    Core.Slice.impl__split_at #u8 secret_key Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE
+    Core_models.Slice.impl__split_at #u8 secret_key Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE
   in
   ind_cpa_secret_key, ind_cpa_public_key, ind_cpa_public_key_hash, implicit_rejection_value
   <:

proofs/fstar/models/Libcrux_ml_kem.Variant.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Variant
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 let _ =
@@ -21,7 +21,7 @@ class t_Variant (v_Self: Type0) = {
       {| i1: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
       shared_secret: t_Slice u8 ->
       ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE
-    -> pred: Type0{(Core.Slice.impl__len #u8 shared_secret <: usize) =. mk_usize 32 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 shared_secret <: usize) =. mk_usize 32 ==> pred};
   f_kdf_post:
       v_K: usize ->
       v_CIPHERTEXT_SIZE: usize ->
@@ -46,7 +46,7 @@ class t_Variant (v_Self: Type0) = {
       #v_Hasher: Type0 ->
       {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
       randomness: t_Slice u8
-    -> pred: Type0{(Core.Slice.impl__len #u8 randomness <: usize) =. mk_usize 32 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 randomness <: usize) =. mk_usize 32 ==> pred};
   f_entropy_preprocess_post:
       v_K: usize ->
       #v_Hasher: Type0 ->
@@ -67,7 +67,7 @@ class t_Variant (v_Self: Type0) = {
       #v_Hasher: Type0 ->
       {| 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) =. mk_usize 32 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 seed <: usize) =. mk_usize 32 ==> pred};
   f_cpa_keygen_seed_post:
       v_K: usize ->
       #v_Hasher: Type0 ->

proofs/fstar/models/Libcrux_ml_kem.Vector.Traits.fsti

@@ -1,6 +1,6 @@
 module Libcrux_ml_kem.Vector.Traits
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
-open Core
+open Core_models
 open FStar.Mul
 
 let v_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS: i16 = mk_i16 1353
@@ -16,8 +16,8 @@ let v_BARRETT_SHIFT: i32 = mk_i32 26
 let v_BARRETT_R: i32 = mk_i32 1 <<! v_BARRETT_SHIFT
 
 class t_Repr (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_5883514518384729217:Core.Marker.t_Copy v_Self;
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_16027770981543256320:Core.Clone.t_Clone v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_5883514518384729217:Core_models.Marker.t_Copy v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_16027770981543256320:Core_models.Clone.t_Clone v_Self;
   f_repr_pre:x: v_Self -> pred: Type0{true ==> pred};
   f_repr_post:v_Self -> t_Array i16 (mk_usize 16) -> Type0;
   f_repr:x0: v_Self
@@ -25,8 +25,8 @@ class t_Repr (v_Self: Type0) = {
 }
 
 class t_Operations (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_5883514518384729217:Core.Marker.t_Copy v_Self;
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_16027770981543256320:Core.Clone.t_Clone v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_5883514518384729217:Core_models.Marker.t_Copy v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_16027770981543256320:Core_models.Clone.t_Clone v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_15138760880757129450:t_Repr v_Self;
   f_ZERO_pre:x: Prims.unit
     -> pred:
@@ -42,7 +42,7 @@ class t_Operations (v_Self: Type0) = {
             f_repr result == Seq.create 16 (mk_i16 0)) };
   f_ZERO:x0: Prims.unit -> Prims.Pure v_Self (f_ZERO_pre x0) (fun result -> f_ZERO_post x0 result);
   f_from_i16_array_pre:array: t_Slice i16
-    -> pred: Type0{(Core.Slice.impl__len #i16 array <: usize) =. mk_usize 16 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #i16 array <: usize) =. mk_usize 16 ==> pred};
   f_from_i16_array_post:array: t_Slice i16 -> result: v_Self
     -> pred: Type0{pred ==> f_repr result == array};
   f_from_i16_array:x0: t_Slice i16
@@ -55,12 +55,12 @@ class t_Operations (v_Self: Type0) = {
         (f_to_i16_array_pre x0)
         (fun result -> f_to_i16_array_post x0 result);
   f_from_bytes_pre:array: t_Slice u8
-    -> pred: Type0{(Core.Slice.impl__len #u8 array <: usize) >=. mk_usize 32 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 array <: usize) >=. mk_usize 32 ==> pred};
   f_from_bytes_post:t_Slice u8 -> v_Self -> Type0;
   f_from_bytes:x0: t_Slice u8
     -> Prims.Pure v_Self (f_from_bytes_pre x0) (fun result -> f_from_bytes_post x0 result);
   f_to_bytes_pre:x: v_Self -> bytes: t_Slice u8
-    -> pred: Type0{(Core.Slice.impl__len #u8 bytes <: usize) >=. mk_usize 32 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 bytes <: usize) >=. mk_usize 32 ==> pred};
   f_to_bytes_post:v_Self -> t_Slice u8 -> t_Slice u8 -> Type0;
   f_to_bytes:x0: v_Self -> x1: t_Slice u8
     -> Prims.Pure (t_Slice u8) (f_to_bytes_pre x0 x1) (fun result -> f_to_bytes_post x0 x1 result);
@@ -324,7 +324,7 @@ class t_Operations (v_Self: Type0) = {
         (f_serialize_1__pre x0)
         (fun result -> f_serialize_1__post x0 result);
   f_deserialize_1__pre:a: t_Slice u8
-    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. mk_usize 2 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 a <: usize) =. mk_usize 2 ==> pred};
   f_deserialize_1__post:a: t_Slice u8 -> result: v_Self
     -> pred:
       Type0{pred ==> sz (Seq.length a) =. sz 2 ==> Spec.MLKEM.deserialize_post 1 a (f_repr result)};
@@ -341,7 +341,7 @@ class t_Operations (v_Self: Type0) = {
         (f_serialize_4__pre x0)
         (fun result -> f_serialize_4__post x0 result);
   f_deserialize_4__pre:a: t_Slice u8
-    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. mk_usize 8 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 a <: usize) =. mk_usize 8 ==> pred};
   f_deserialize_4__post:a: t_Slice u8 -> result: v_Self
     -> pred:
       Type0{pred ==> sz (Seq.length a) =. sz 8 ==> Spec.MLKEM.deserialize_post 4 a (f_repr result)};
@@ -354,7 +354,7 @@ class t_Operations (v_Self: Type0) = {
         (f_serialize_5__pre x0)
         (fun result -> f_serialize_5__post x0 result);
   f_deserialize_5__pre:a: t_Slice u8
-    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. mk_usize 10 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 a <: usize) =. mk_usize 10 ==> pred};
   f_deserialize_5__post:t_Slice u8 -> v_Self -> Type0;
   f_deserialize_5_:x0: t_Slice u8
     -> Prims.Pure v_Self (f_deserialize_5__pre x0) (fun result -> f_deserialize_5__post x0 result);
@@ -370,7 +370,7 @@ class t_Operations (v_Self: Type0) = {
         (f_serialize_10__pre x0)
         (fun result -> f_serialize_10__post x0 result);
   f_deserialize_10__pre:a: t_Slice u8
-    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. mk_usize 20 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 a <: usize) =. mk_usize 20 ==> pred};
   f_deserialize_10__post:a: t_Slice u8 -> result: v_Self
     -> pred:
       Type0
@@ -384,7 +384,7 @@ class t_Operations (v_Self: Type0) = {
         (f_serialize_11__pre x0)
         (fun result -> f_serialize_11__post x0 result);
   f_deserialize_11__pre:a: t_Slice u8
-    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. mk_usize 22 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 a <: usize) =. mk_usize 22 ==> pred};
   f_deserialize_11__post:t_Slice u8 -> v_Self -> Type0;
   f_deserialize_11_:x0: t_Slice u8
     -> Prims.Pure v_Self (f_deserialize_11__pre x0) (fun result -> f_deserialize_11__post x0 result);
@@ -400,7 +400,7 @@ class t_Operations (v_Self: Type0) = {
         (f_serialize_12__pre x0)
         (fun result -> f_serialize_12__post x0 result);
   f_deserialize_12__pre:a: t_Slice u8
-    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. mk_usize 24 ==> pred};
+    -> pred: Type0{(Core_models.Slice.impl__len #u8 a <: usize) =. mk_usize 24 ==> pred};
   f_deserialize_12__post:a: t_Slice u8 -> result: v_Self
     -> pred:
       Type0
@@ -410,8 +410,8 @@ class t_Operations (v_Self: Type0) = {
   f_rej_sample_pre:a: t_Slice u8 -> out: t_Slice i16
     -> pred:
       Type0
-        { (Core.Slice.impl__len #u8 a <: usize) =. mk_usize 24 &&
-          (Core.Slice.impl__len #i16 out <: usize) =. mk_usize 16 ==>
+        { (Core_models.Slice.impl__len #u8 a <: usize) =. mk_usize 24 &&
+          (Core_models.Slice.impl__len #i16 out <: usize) =. mk_usize 16 ==>
           pred };
   f_rej_sample_post:a: t_Slice u8 -> out: t_Slice i16 -> x: (t_Slice i16 & usize)
     -> pred:

proofs/fstar/models/MkSeq.fst

@@ -1,5 +1,5 @@
 module MkSeq
-open Core
+open Core_models
 
 open FStar.Tactics.V2
 

proofs/fstar/models/Num_enum.fsti

@@ -1,6 +1,6 @@
 module Num_enum
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 (* item error backend: (reject_TraitItemDefault) ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
@@ -42,8 +42,8 @@ class t_CannotDeriveBothFromPrimitiveAndTryFromPrimitive (v_Self: Type0) = {
 
 (* class t_FromPrimitive (v_Self: Type0) = {
   f_Primitive:Type0;
-  f_Primitive_8876061459599834537:Core.Marker.t_Copy f_Primitive;
-  f_Primitive_17391871992276743015:Core.Cmp.t_Eq f_Primitive;
+  f_Primitive_8876061459599834537:Core_models.Marker.t_Copy f_Primitive;
+  f_Primitive_17391871992276743015:Core_models.Cmp.t_Eq f_Primitive;
   f_from_primitive_pre:f_Primitive -> Type0;
   f_from_primitive_post:f_Primitive -> v_Self -> Type0;
   f_from_primitive:x0: f_Primitive
@@ -52,15 +52,15 @@ class t_CannotDeriveBothFromPrimitiveAndTryFromPrimitive (v_Self: Type0) = {
 
 class t_TryFromPrimitive (v_Self: Type0) = {
   f_Primitive:Type0;
-  (* f_Primitive_12399228673407067350:Core.Marker.t_Copy f_Primitive;
-  f_Primitive_5629480169667985622:Core.Cmp.t_Eq f_Primitive;
-  f_Primitive_10837566226016321784:Core.Fmt.t_Debug f_Primitive; *)
+  (* f_Primitive_12399228673407067350:Core_models.Marker.t_Copy f_Primitive;
+  f_Primitive_5629480169667985622:Core_models.Cmp.t_Eq f_Primitive;
+  f_Primitive_10837566226016321784:Core_models.Fmt.t_Debug f_Primitive; *)
   f_Error:Type0;
   f_NAME:string;
   f_try_from_primitive_pre:f_Primitive -> Type0;
-  f_try_from_primitive_post:f_Primitive -> Core.Result.t_Result v_Self f_Error -> Type0;
+  f_try_from_primitive_post:f_Primitive -> Core_models.Result.t_Result v_Self f_Error -> Type0;
   f_try_from_primitive:x0: f_Primitive
-    -> Prims.Pure (Core.Result.t_Result v_Self f_Error)
+    -> Prims.Pure (Core_models.Result.t_Result v_Self f_Error)
         (f_try_from_primitive_pre x0)
         (fun result -> f_try_from_primitive_post x0 result)
 }
@@ -72,50 +72,50 @@ type t_TryFromPrimitiveError (v_Enum: Type0) (* {| i1: t_TryFromPrimitive v_Enum
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_5
       (#v_Enum: Type0)
-      {| i1: Core.Clone.t_Clone v_Enum |}
+      {| i1: Core_models.Clone.t_Clone v_Enum |}
       {| i2: t_TryFromPrimitive v_Enum |}
-      {| i3: Core.Clone.t_Clone i2.f_Primitive |}
-    : Core.Clone.t_Clone (t_TryFromPrimitiveError v_Enum)
+      {| i3: Core_models.Clone.t_Clone i2.f_Primitive |}
+    : Core_models.Clone.t_Clone (t_TryFromPrimitiveError v_Enum)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_4
       (#v_Enum: Type0)
-      {| i1: Core.Marker.t_Copy v_Enum |}
+      {| i1: Core_models.Marker.t_Copy v_Enum |}
       {| i2: t_TryFromPrimitive v_Enum |}
-      {| i3: Core.Marker.t_Copy i2.f_Primitive |}
-    : Core.Marker.t_Copy (t_TryFromPrimitiveError v_Enum)
+      {| i3: Core_models.Marker.t_Copy i2.f_Primitive |}
+    : Core_models.Marker.t_Copy (t_TryFromPrimitiveError v_Enum)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_6 (#v_Enum: Type0) {| i1: t_TryFromPrimitive v_Enum |}
-    : Core.Marker.t_StructuralPartialEq (t_TryFromPrimitiveError v_Enum)
+    : Core_models.Marker.t_StructuralPartialEq (t_TryFromPrimitiveError v_Enum)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_7
       (#v_Enum: Type0)
-      {| i1: Core.Cmp.t_PartialEq v_Enum v_Enum |}
+      {| i1: Core_models.Cmp.t_PartialEq v_Enum v_Enum |}
       {| i2: t_TryFromPrimitive v_Enum |}
-      {| i3: Core.Cmp.t_PartialEq i2.f_Primitive i2.f_Primitive |}
-    : Core.Cmp.t_PartialEq (t_TryFromPrimitiveError v_Enum) (t_TryFromPrimitiveError v_Enum)
+      {| i3: Core_models.Cmp.t_PartialEq i2.f_Primitive i2.f_Primitive |}
+    : Core_models.Cmp.t_PartialEq (t_TryFromPrimitiveError v_Enum) (t_TryFromPrimitiveError v_Enum)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_8
       (#v_Enum: Type0)
-      {| i1: Core.Cmp.t_Eq v_Enum |}
+      {| i1: Core_models.Cmp.t_Eq v_Enum |}
       {| i2: t_TryFromPrimitive v_Enum |}
-      {| i3: Core.Cmp.t_Eq i2.f_Primitive |}
-    : Core.Cmp.t_Eq (t_TryFromPrimitiveError v_Enum)
+      {| i3: Core_models.Cmp.t_Eq i2.f_Primitive |}
+    : Core_models.Cmp.t_Eq (t_TryFromPrimitiveError v_Enum)
 
 val impl__new (#v_Enum: Type0) {| i1: t_TryFromPrimitive v_Enum |} (number: i1.f_Primitive)
     : Prims.Pure (t_TryFromPrimitiveError v_Enum) Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_1 (#v_Enum: Type0) {| i1: t_TryFromPrimitive v_Enum |}
-    : Core.Fmt.t_Debug (t_TryFromPrimitiveError v_Enum)
+    : Core_models.Fmt.t_Debug (t_TryFromPrimitiveError v_Enum)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_2 (#v_Enum: Type0) {| i1: t_TryFromPrimitive v_Enum |}
-    : Core.Fmt.t_Display (t_TryFromPrimitiveError v_Enum)
+    : Core_models.Fmt.t_Display (t_TryFromPrimitiveError v_Enum)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_3 (#v_Enum: Type0) {| i1: t_TryFromPrimitive v_Enum |}
-    : Core.Error.t_Error (t_TryFromPrimitiveError v_Enum)
+    : Core_models.Error.t_Error (t_TryFromPrimitiveError v_Enum)

proofs/fstar/models/Prost.Encoding.Wire_type.fsti

@@ -1,6 +1,6 @@
 module Prost.Encoding.Wire_type
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 type t_WireType =

proofs/fstar/models/Prost.Encoding.fsti

@@ -1,6 +1,6 @@
 module Prost.Encoding
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 type t_DecodeContext = { f_recurse_count:u32 }

proofs/fstar/models/Prost.Error.fsti

@@ -1,6 +1,6 @@
 module Prost.Error
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 type t_Inner = {
@@ -14,33 +14,33 @@ type t_Inner = {
 /// general it is not possible to exactly pinpoint why data is malformed.
 type t_DecodeError = { f_inner:Alloc.Boxed.t_Box t_Inner Alloc.Alloc.t_Global }
 
-let impl_6: Core.Clone.t_Clone t_DecodeError = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
+let impl_6: Core_models.Clone.t_Clone t_DecodeError = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_7:Core.Marker.t_StructuralPartialEq t_DecodeError
+val impl_7:Core_models.Marker.t_StructuralPartialEq t_DecodeError
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_8:Core.Cmp.t_PartialEq t_DecodeError t_DecodeError
+val impl_8:Core_models.Cmp.t_PartialEq t_DecodeError t_DecodeError
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_9:Core.Cmp.t_Eq t_DecodeError
+val impl_9:Core_models.Cmp.t_Eq t_DecodeError
 
-let impl_10: Core.Clone.t_Clone t_Inner = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
+let impl_10: Core_models.Clone.t_Clone t_Inner = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_11:Core.Marker.t_StructuralPartialEq t_Inner
+val impl_11:Core_models.Marker.t_StructuralPartialEq t_Inner
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_12:Core.Cmp.t_PartialEq t_Inner t_Inner
+val impl_12:Core_models.Cmp.t_PartialEq t_Inner t_Inner
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_13:Core.Cmp.t_Eq t_Inner
+val impl_13:Core_models.Cmp.t_Eq t_Inner
 
 /// Creates a new `DecodeError` with a 'best effort' root cause description.
 /// Meant to be used only by `Message` implementations.
 val impl_DecodeError__new
       (#iimpl_270350286_: Type0)
-      {| i1: Core.Convert.t_Into iimpl_270350286_ (Alloc.Borrow.t_Cow string) |}
+      {| i1: Core_models.Convert.t_Into iimpl_270350286_ (Alloc.Borrow.t_Cow string) |}
       (description: iimpl_270350286_)
     : Prims.Pure t_DecodeError Prims.l_True (fun _ -> Prims.l_True)
 
@@ -50,10 +50,10 @@ val impl_DecodeError__push (self: t_DecodeError) (message field: string)
     : Prims.Pure t_DecodeError Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_1:Core.Fmt.t_Debug t_DecodeError
+val impl_1:Core_models.Fmt.t_Debug t_DecodeError
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_2:Core.Fmt.t_Display t_DecodeError
+val impl_2:Core_models.Fmt.t_Display t_DecodeError
 
 /// A Protobuf message encoding error.
 /// `EncodeError` always indicates that a message failed to encode because the
@@ -64,22 +64,22 @@ type t_EncodeError = {
   f_remaining:usize
 }
 
-let impl_15: Core.Clone.t_Clone t_EncodeError = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
+let impl_15: Core_models.Clone.t_Clone t_EncodeError = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_14:Core.Marker.t_Copy t_EncodeError
+val impl_14:Core_models.Marker.t_Copy t_EncodeError
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_16:Core.Fmt.t_Debug t_EncodeError
+val impl_16:Core_models.Fmt.t_Debug t_EncodeError
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_17:Core.Marker.t_StructuralPartialEq t_EncodeError
+val impl_17:Core_models.Marker.t_StructuralPartialEq t_EncodeError
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_18:Core.Cmp.t_PartialEq t_EncodeError t_EncodeError
+val impl_18:Core_models.Cmp.t_PartialEq t_EncodeError t_EncodeError
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_19:Core.Cmp.t_Eq t_EncodeError
+val impl_19:Core_models.Cmp.t_Eq t_EncodeError
 
 /// Creates a new `EncodeError`.
 val impl_EncodeError__new (required remaining: usize)
@@ -94,7 +94,7 @@ val impl_EncodeError__remaining (self: t_EncodeError)
     : Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_4:Core.Fmt.t_Display t_EncodeError
+val impl_4:Core_models.Fmt.t_Display t_EncodeError
 
 /// An error indicating that an unknown enumeration value was encountered.
 /// The Protobuf spec mandates that enumeration value sets are ‘open’, so this
@@ -102,22 +102,22 @@ val impl_4:Core.Fmt.t_Display t_EncodeError
 /// presently used enum definition.
 type t_UnknownEnumValue = | UnknownEnumValue : i32 -> t_UnknownEnumValue
 
-let impl_21: Core.Clone.t_Clone t_UnknownEnumValue = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
+let impl_21: Core_models.Clone.t_Clone t_UnknownEnumValue = { f_clone = (fun x -> x); f_clone_pre = (fun _ -> True); f_clone_post = (fun _ _ -> True) }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_20:Core.Marker.t_Copy t_UnknownEnumValue
+val impl_20:Core_models.Marker.t_Copy t_UnknownEnumValue
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_22:Core.Fmt.t_Debug t_UnknownEnumValue
+val impl_22:Core_models.Fmt.t_Debug t_UnknownEnumValue
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_23:Core.Marker.t_StructuralPartialEq t_UnknownEnumValue
+val impl_23:Core_models.Marker.t_StructuralPartialEq t_UnknownEnumValue
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_24:Core.Cmp.t_PartialEq t_UnknownEnumValue t_UnknownEnumValue
+val impl_24:Core_models.Cmp.t_PartialEq t_UnknownEnumValue t_UnknownEnumValue
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_25:Core.Cmp.t_Eq t_UnknownEnumValue
+val impl_25:Core_models.Cmp.t_Eq t_UnknownEnumValue
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_5:Core.Fmt.t_Display t_UnknownEnumValue
+val impl_5:Core_models.Fmt.t_Display t_UnknownEnumValue

proofs/fstar/models/Prost.Message.fsti

@@ -1,6 +1,6 @@
 module Prost.Message
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 let _ =
@@ -12,9 +12,9 @@ let _ =
 
 /// A Protocol Buffers message.
 class t_Message (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_7459769351467436346:Core.Fmt.t_Debug v_Self;
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_10374730180605511532:Core.Marker.t_Send v_Self;
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_6360119584534035317:Core.Marker.t_Sync v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_7459769351467436346:Core_models.Fmt.t_Debug v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_10374730180605511532:Core_models.Marker.t_Send v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_6360119584534035317:Core_models.Marker.t_Sync v_Self;
   f_encode_pre:
       #impl_806524398_: Type0 ->
       {| i2: Bytes.Buf.Buf_mut.t_BufMut impl_806524398_ |} ->
@@ -26,7 +26,7 @@ class t_Message (v_Self: Type0) = {
       {| i2: Bytes.Buf.Buf_mut.t_BufMut impl_806524398_ |} ->
       v_Self ->
       impl_806524398_ ->
-      (impl_806524398_ & Core.Result.t_Result Prims.unit Prost.Error.t_EncodeError)
+      (impl_806524398_ & Core_models.Result.t_Result Prims.unit Prost.Error.t_EncodeError)
     -> Type0;
   f_encode:
       #impl_806524398_: Type0 ->
@@ -34,7 +34,7 @@ class t_Message (v_Self: Type0) = {
       x0: v_Self ->
       x1: impl_806524398_
     -> Prims.Pure
-        (impl_806524398_ & Core.Result.t_Result Prims.unit Prost.Error.t_EncodeError)
+        (impl_806524398_ & Core_models.Result.t_Result Prims.unit Prost.Error.t_EncodeError)
         (f_encode_pre #impl_806524398_ #i2 x0 x1)
         (fun result -> f_encode_post #impl_806524398_ #i2 x0 x1 result);
   f_encode_to_vec_pre:v_Self -> res:Type0 {true ==> res};
@@ -45,23 +45,23 @@ class t_Message (v_Self: Type0) = {
         (fun result -> f_encode_to_vec_post x0 result);
   f_decode_pre:
       #impl_75985673_: Type0 ->
-      {| i4: Core.Default.t_Default v_Self |} ->
+      {| i4: Core_models.Default.t_Default v_Self |} ->
       {| i5: Bytes.Buf.Buf_impl.t_Buf impl_75985673_ |} ->
       impl_75985673_
     -> res:Type0 {true ==> res};
   f_decode_post:
       #impl_75985673_: Type0 ->
-      {| i4: Core.Default.t_Default v_Self |} ->
+      {| i4: Core_models.Default.t_Default v_Self |} ->
       {| i5: Bytes.Buf.Buf_impl.t_Buf impl_75985673_ |} ->
       impl_75985673_ ->
-      Core.Result.t_Result v_Self Prost.Error.t_DecodeError
+      Core_models.Result.t_Result v_Self Prost.Error.t_DecodeError
     -> Type0;
   f_decode:
       #impl_75985673_: Type0 ->
-      {| i4: Core.Default.t_Default v_Self |} ->
+      {| i4: Core_models.Default.t_Default v_Self |} ->
       {| i5: Bytes.Buf.Buf_impl.t_Buf impl_75985673_ |} ->
       x0: impl_75985673_
-    -> Prims.Pure (Core.Result.t_Result v_Self Prost.Error.t_DecodeError)
+    -> Prims.Pure (Core_models.Result.t_Result v_Self Prost.Error.t_DecodeError)
         (f_decode_pre #impl_75985673_ #i4 #i5 x0)
         (fun result -> f_decode_post #impl_75985673_ #i4 #i5 x0 result);
   f_clear_pre:v_Self -> Type0;

proofs/fstar/models/Rand.Rng.fsti

@@ -1,6 +1,6 @@
 module Rand.Rng
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 class t_Rng (t: Type) = {

proofs/fstar/models/Sorted_vec.fsti

@@ -1,69 +1,69 @@
 module Sorted_vec
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
+open Core_models
 open FStar.Mul
 
 /// Forward sorted vector
-type t_SortedVec (v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} = {
+type t_SortedVec (v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} = {
   f_vec:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global
 }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_18 (#v_T: Type0) {| i1: Core.Clone.t_Clone v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Clone.t_Clone (t_SortedVec v_T)
+val impl_18 (#v_T: Type0) {| i1: Core_models.Clone.t_Clone v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Clone.t_Clone (t_SortedVec v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_19 (#v_T: Type0) {| i1: Core.Fmt.t_Debug v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Fmt.t_Debug (t_SortedVec v_T)
+val impl_19 (#v_T: Type0) {| i1: Core_models.Fmt.t_Debug v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Fmt.t_Debug (t_SortedVec v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_22 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |}
-    : Core.Marker.t_StructuralPartialEq (t_SortedVec v_T)
+val impl_22 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Marker.t_StructuralPartialEq (t_SortedVec v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_23 (#v_T: Type0) {| i1: Core.Cmp.t_PartialEq v_T v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Cmp.t_PartialEq (t_SortedVec v_T) (t_SortedVec v_T)
+val impl_23 (#v_T: Type0) {| i1: Core_models.Cmp.t_PartialEq v_T v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Cmp.t_PartialEq (t_SortedVec v_T) (t_SortedVec v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_20 (#v_T: Type0) {| i1: Core.Cmp.t_Eq v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Cmp.t_Eq (t_SortedVec v_T)
+val impl_20 (#v_T: Type0) {| i1: Core_models.Cmp.t_Eq v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Cmp.t_Eq (t_SortedVec v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_24 (#v_T: Type0) {| i1: Core.Cmp.t_PartialOrd v_T v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Cmp.t_PartialOrd (t_SortedVec v_T) (t_SortedVec v_T)
+val impl_24 (#v_T: Type0) {| i1: Core_models.Cmp.t_PartialOrd v_T v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Cmp.t_PartialOrd (t_SortedVec v_T) (t_SortedVec v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_21 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} : Core.Cmp.t_Ord (t_SortedVec v_T)
+val impl_21 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} : Core_models.Cmp.t_Ord (t_SortedVec v_T)
 
 /// Forward sorted set
-type t_SortedSet (v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} = { f_set:t_SortedVec v_T }
+type t_SortedSet (v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} = { f_set:t_SortedVec v_T }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_25 (#v_T: Type0) {| i1: Core.Clone.t_Clone v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Clone.t_Clone (t_SortedSet v_T)
+val impl_25 (#v_T: Type0) {| i1: Core_models.Clone.t_Clone v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Clone.t_Clone (t_SortedSet v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_26 (#v_T: Type0) {| i1: Core.Fmt.t_Debug v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Fmt.t_Debug (t_SortedSet v_T)
+val impl_26 (#v_T: Type0) {| i1: Core_models.Fmt.t_Debug v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Fmt.t_Debug (t_SortedSet v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_29 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |}
-    : Core.Marker.t_StructuralPartialEq (t_SortedSet v_T)
+val impl_29 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Marker.t_StructuralPartialEq (t_SortedSet v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_30 (#v_T: Type0) {| i1: Core.Cmp.t_PartialEq v_T v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Cmp.t_PartialEq (t_SortedSet v_T) (t_SortedSet v_T)
+val impl_30 (#v_T: Type0) {| i1: Core_models.Cmp.t_PartialEq v_T v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Cmp.t_PartialEq (t_SortedSet v_T) (t_SortedSet v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_27 (#v_T: Type0) {| i1: Core.Cmp.t_Eq v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Cmp.t_Eq (t_SortedSet v_T)
+val impl_27 (#v_T: Type0) {| i1: Core_models.Cmp.t_Eq v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Cmp.t_Eq (t_SortedSet v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_31 (#v_T: Type0) {| i1: Core.Cmp.t_PartialOrd v_T v_T |} {| i2: Core.Cmp.t_Ord v_T |}
-    : Core.Cmp.t_PartialOrd (t_SortedSet v_T) (t_SortedSet v_T)
+val impl_31 (#v_T: Type0) {| i1: Core_models.Cmp.t_PartialOrd v_T v_T |} {| i2: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Cmp.t_PartialOrd (t_SortedSet v_T) (t_SortedSet v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_28 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} : Core.Cmp.t_Ord (t_SortedSet v_T)
+val impl_28 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} : Core_models.Cmp.t_Ord (t_SortedSet v_T)
 
 /// Value returned when find_or_insert is used.
 type t_FindOrInsert =
@@ -71,29 +71,29 @@ type t_FindOrInsert =
   | FindOrInsert_Inserted : usize -> t_FindOrInsert
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_32:Core.Marker.t_StructuralPartialEq t_FindOrInsert
+val impl_32:Core_models.Marker.t_StructuralPartialEq t_FindOrInsert
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_33:Core.Cmp.t_PartialEq t_FindOrInsert t_FindOrInsert
+val impl_33:Core_models.Cmp.t_PartialEq t_FindOrInsert t_FindOrInsert
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_34:Core.Cmp.t_PartialOrd t_FindOrInsert t_FindOrInsert
+val impl_34:Core_models.Cmp.t_PartialOrd t_FindOrInsert t_FindOrInsert
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_35:Core.Cmp.t_Eq t_FindOrInsert
+val impl_35:Core_models.Cmp.t_Eq t_FindOrInsert
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_36:Core.Cmp.t_Ord t_FindOrInsert
+val impl_36:Core_models.Cmp.t_Ord t_FindOrInsert
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_37:Core.Fmt.t_Debug t_FindOrInsert
+val impl_37:Core_models.Fmt.t_Debug t_FindOrInsert
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_38:Core.Hash.t_Hash t_FindOrInsert *)
+val impl_38:Core_models.Hash.t_Hash t_FindOrInsert *)
 
 /// Converts from the binary_search result type into the FindOrInsert type
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl:Core.Convert.t_From t_FindOrInsert (Core.Result.t_Result usize usize)
+val impl:Core_models.Convert.t_From t_FindOrInsert (Core_models.Result.t_Result usize usize)
 
 /// Get the index of the element that was either found or inserted.
 val impl_FindOrInsert__index (self: t_FindOrInsert)
@@ -102,12 +102,12 @@ val impl_FindOrInsert__index (self: t_FindOrInsert)
 /// If an equivalent element was found in the container, get the value of
 /// its index. Otherwise get None.
 val impl_FindOrInsert__found (self: t_FindOrInsert)
-    : Prims.Pure (Core.Option.t_Option usize) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (Core_models.Option.t_Option usize) Prims.l_True (fun _ -> Prims.l_True)
 
 /// If the provided element was inserted into the container, get the value
 /// of its index. Otherwise get None.
 val impl_FindOrInsert__inserted (self: t_FindOrInsert)
-    : Prims.Pure (Core.Option.t_Option usize) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (Core_models.Option.t_Option usize) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Returns true if the element was found.
 val impl_FindOrInsert__is_found (self: t_FindOrInsert)
@@ -117,29 +117,29 @@ val impl_FindOrInsert__is_found (self: t_FindOrInsert)
 val impl_FindOrInsert__is_inserted (self: t_FindOrInsert)
     : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 
-val impl_2__new: #v_T: Type0 -> {| i1: Core.Cmp.t_Ord v_T |} -> Prims.unit
+val impl_2__new: #v_T: Type0 -> {| i1: Core_models.Cmp.t_Ord v_T |} -> Prims.unit
   -> Prims.Pure (t_SortedVec v_T) Prims.l_True (fun _ -> Prims.l_True)
 
-val impl_2__with_capacity (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (capacity: usize)
+val impl_2__with_capacity (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (capacity: usize)
     : Prims.Pure (t_SortedVec v_T) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Uses `sort_unstable()` to sort in place.
 val impl_2__from_unsorted
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (vec: Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
     : Prims.Pure (t_SortedVec v_T) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Insert an element into sorted position, returning the order index at which
 /// it was placed.
-val impl_2__insert (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedVec v_T) (element: v_T)
+val impl_2__insert (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedVec v_T) (element: v_T)
     : Prims.Pure (t_SortedVec v_T & usize) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Find the element and return the index with `Ok`, otherwise insert the
 /// element and return the new element index with `Err`.
 val impl_2__find_or_insert
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedVec v_T)
       (element: v_T)
     : Prims.Pure (t_SortedVec v_T & t_FindOrInsert) Prims.l_True (fun _ -> Prims.l_True)
@@ -147,14 +147,14 @@ val impl_2__find_or_insert
 /// Same as insert, except performance is O(1) when the element belongs at the
 /// back of the container. This avoids an O(log(N)) search for inserting
 /// elements at the back.
-val impl_2__push (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedVec v_T) (element: v_T)
+val impl_2__push (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedVec v_T) (element: v_T)
     : Prims.Pure (t_SortedVec v_T & usize) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Reserves additional capacity in the underlying vector.
 /// See std::vec::Vec::reserve.
 val impl_2__reserve
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedVec v_T)
       (additional: usize)
     : Prims.Pure (t_SortedVec v_T) Prims.l_True (fun _ -> Prims.l_True)
@@ -163,33 +163,33 @@ val impl_2__reserve
 /// belongs at the back of the container.
 val impl_2__find_or_push
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedVec v_T)
       (element: v_T)
     : Prims.Pure (t_SortedVec v_T & t_FindOrInsert) Prims.l_True (fun _ -> Prims.l_True)
 
 val impl_2__remove_item
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedVec v_T)
       (item: v_T)
-    : Prims.Pure (t_SortedVec v_T & Core.Option.t_Option v_T) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (t_SortedVec v_T & Core_models.Option.t_Option v_T) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Panics if index is out of bounds
 val impl_2__remove_index
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedVec v_T)
       (index: usize)
     : Prims.Pure (t_SortedVec v_T & v_T) Prims.l_True (fun _ -> Prims.l_True)
 
-val impl_2__pop (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
-    : Prims.Pure (t_SortedVec v_T & Core.Option.t_Option v_T) Prims.l_True (fun _ -> Prims.l_True)
+val impl_2__pop (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
+    : Prims.Pure (t_SortedVec v_T & Core_models.Option.t_Option v_T) Prims.l_True (fun _ -> Prims.l_True)
 
-val impl_2__clear (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
+val impl_2__clear (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
     : Prims.Pure (t_SortedVec v_T) Prims.l_True (fun _ -> Prims.l_True)
 
-val impl_2__dedup (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
+val impl_2__dedup (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
     : Prims.Pure (t_SortedVec v_T) Prims.l_True (fun _ -> Prims.l_True)
 
 (* item error backend: (DirectAndMut) The mutation of this &mut is not allowed here.
@@ -251,8 +251,8 @@ const _: () = ();
 
 (* val impl_2__drain
       (#v_T #v_R: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
-      {| i7: Core.Ops.Range.t_RangeBounds v_R usize |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
+      {| i7: Core_models.Ops.Range.t_RangeBounds v_R usize |}
       (self: t_SortedVec v_T)
       (range: v_R)
     : Prims.Pure (t_SortedVec v_T & Alloc.Vec.Drain.t_Drain v_T Alloc.Alloc.t_Global)
@@ -261,15 +261,15 @@ const _: () = ();
 
 (* val impl_2__retain
       (#v_T #v_F: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
-      {| i8: Core.Ops.Function.t_FnMut v_F v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
+      {| i8: Core_models.Ops.Function.t_FnMut v_F v_T |}
       (self: t_SortedVec v_T)
       (f: v_F)
     : Prims.Pure (t_SortedVec v_T) Prims.l_True (fun _ -> Prims.l_True) *)
 
 /// NOTE: to_vec() is a slice method that is accessible through deref, use
 /// this instead to avoid cloning
-val impl_2__into_vec (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
+val impl_2__into_vec (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
     : Prims.Pure (Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global) Prims.l_True (fun _ -> Prims.l_True)
 
 (* item error backend: (DirectAndMut) The mutation of this &mut is not allowed here.
@@ -335,26 +335,26 @@ const _: () = ();
 /// The caller must ensure that the provided vector is already sorted.
 val impl_2__from_sorted
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (vec: Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
     : Prims.Pure (t_SortedVec v_T) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Unsafe access to the underlying vector. The caller must ensure that any
 /// changes to the values in the vector do not impact the ordering of the
 /// elements inside, or else this container will misbehave.
-(* val impl_2__get_unchecked_mut_vec (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
+(* val impl_2__get_unchecked_mut_vec (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedVec v_T)
     : Prims.Pure Rust_primitives.Hax.failure Prims.l_True (fun _ -> Prims.l_True) *)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_3 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} : Core.Default.t_Default (t_SortedVec v_T)
+val impl_3 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} : Core_models.Default.t_Default (t_SortedVec v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_4 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |}
-    : Core.Convert.t_From (t_SortedVec v_T) (Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
+val impl_4 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Convert.t_From (t_SortedVec v_T) (Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_5 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cmp.t_Ord v_T)
-    : Core.Ops.Deref.t_Deref (t_SortedVec v_T) =
+let impl_5 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core_models.Cmp.t_Ord v_T)
+    : Core_models.Ops.Deref.t_Deref (t_SortedVec v_T) =
   {
     f_Target = Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global;(* 
     f_deref_pre = (fun (self: t_SortedVec v_T) -> true);
@@ -365,24 +365,24 @@ let impl_5 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cmp
   }
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_6 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |}
-    : Core.Iter.Traits.Collect.t_Extend (t_SortedVec v_T) v_T *)
+val impl_6 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Iter.Traits.Collect.t_Extend (t_SortedVec v_T) v_T *)
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_7 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} {| i2: Core.Hash.t_Hash v_T |}
-    : Core.Hash.t_Hash (t_SortedVec v_T) *)
+val impl_7 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} {| i2: Core_models.Hash.t_Hash v_T |}
+    : Core_models.Hash.t_Hash (t_SortedVec v_T) *)
 
-val impl_10__new: #v_T: Type0 -> {| i1: Core.Cmp.t_Ord v_T |} -> Prims.unit
+val impl_10__new: #v_T: Type0 -> {| i1: Core_models.Cmp.t_Ord v_T |} -> Prims.unit
   -> Prims.Pure (t_SortedSet v_T) Prims.l_True (fun _ -> Prims.l_True)
 
-val impl_10__with_capacity (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (capacity: usize)
+val impl_10__with_capacity (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (capacity: usize)
     : Prims.Pure (t_SortedSet v_T) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Uses `sort_unstable()` to sort in place and `dedup()` to remove
 /// duplicates.
 val impl_10__from_unsorted
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (vec: Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
     : Prims.Pure (t_SortedSet v_T) Prims.l_True (fun _ -> Prims.l_True)
 
@@ -390,10 +390,10 @@ val impl_10__from_unsorted
 /// it was placed. If an existing item was found it will be returned.
 val impl_10__replace
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedSet v_T)
       (element: v_T)
-    : Prims.Pure (t_SortedSet v_T & (usize & Core.Option.t_Option v_T))
+    : Prims.Pure (t_SortedSet v_T & (usize & Core_models.Option.t_Option v_T))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
@@ -401,7 +401,7 @@ val impl_10__replace
 /// element and return the new element index with `Err`.
 val impl_10__find_or_insert
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedSet v_T)
       (element: v_T)
     : Prims.Pure (t_SortedSet v_T & t_FindOrInsert) Prims.l_True (fun _ -> Prims.l_True)
@@ -409,8 +409,8 @@ val impl_10__find_or_insert
 /// Same as replace, except performance is O(1) when the element belongs at
 /// the back of the container. This avoids an O(log(N)) search for inserting
 /// elements at the back.
-val impl_10__push (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedSet v_T) (element: v_T)
-    : Prims.Pure (t_SortedSet v_T & (usize & Core.Option.t_Option v_T))
+val impl_10__push (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedSet v_T) (element: v_T)
+    : Prims.Pure (t_SortedSet v_T & (usize & Core_models.Option.t_Option v_T))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
@@ -418,7 +418,7 @@ val impl_10__push (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedSet
 /// See std::vec::Vec::reserve.
 val impl_10__reserve
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedSet v_T)
       (additional: usize)
     : Prims.Pure (t_SortedSet v_T) Prims.l_True (fun _ -> Prims.l_True)
@@ -427,36 +427,36 @@ val impl_10__reserve
 /// belongs at the back of the container.
 val impl_10__find_or_push
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedSet v_T)
       (element: v_T)
     : Prims.Pure (t_SortedSet v_T & t_FindOrInsert) Prims.l_True (fun _ -> Prims.l_True)
 
 val impl_10__remove_item
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedSet v_T)
       (item: v_T)
-    : Prims.Pure (t_SortedSet v_T & Core.Option.t_Option v_T) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (t_SortedSet v_T & Core_models.Option.t_Option v_T) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Panics if index is out of bounds
 val impl_10__remove_index
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedSet v_T)
       (index: usize)
     : Prims.Pure (t_SortedSet v_T & v_T) Prims.l_True (fun _ -> Prims.l_True)
 
-val impl_10__pop (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedSet v_T)
-    : Prims.Pure (t_SortedSet v_T & Core.Option.t_Option v_T) Prims.l_True (fun _ -> Prims.l_True)
+val impl_10__pop (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedSet v_T)
+    : Prims.Pure (t_SortedSet v_T & Core_models.Option.t_Option v_T) Prims.l_True (fun _ -> Prims.l_True)
 
-val impl_10__clear (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedSet v_T)
+val impl_10__clear (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedSet v_T)
     : Prims.Pure (t_SortedSet v_T) Prims.l_True (fun _ -> Prims.l_True)
 
 (* val impl_10__drain
       (#v_T #v_R: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
-      {| i3: Core.Ops.Range.t_RangeBounds v_R usize |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
+      {| i3: Core_models.Ops.Range.t_RangeBounds v_R usize |}
       (self: t_SortedSet v_T)
       (range: v_R)
     : Prims.Pure (t_SortedSet v_T & Alloc.Vec.Drain.t_Drain v_T Alloc.Alloc.t_Global)
@@ -465,15 +465,15 @@ val impl_10__clear (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedSet
 
 (* val impl_10__retain
       (#v_T #v_F: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
-      {| i5: Core.Ops.Function.t_FnMut v_F v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
+      {| i5: Core_models.Ops.Function.t_FnMut v_F v_T |}
       (self: t_SortedSet v_T)
       (f: v_F)
     : Prims.Pure (t_SortedSet v_T) Prims.l_True (fun _ -> Prims.l_True) *)
 
 /// NOTE: to_vec() is a slice method that is accessible through deref, use
 /// this instead to avoid cloning
-val impl_10__into_vec (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} (self: t_SortedSet v_T)
+val impl_10__into_vec (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} (self: t_SortedSet v_T)
     : Prims.Pure (Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global) Prims.l_True (fun _ -> Prims.l_True)
 
 (* item error backend: (DirectAndMut) The mutation of this &mut is not allowed here.
@@ -541,7 +541,7 @@ const _: () = ();
 /// deduped.
 val impl_10__from_sorted
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (vec: Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
     : Prims.Pure (t_SortedSet v_T) Prims.l_True (fun _ -> Prims.l_True)
 
@@ -550,20 +550,20 @@ val impl_10__from_sorted
 /// elements inside, or else this container will misbehave.
 (* val impl_10__get_unchecked_mut_vec
       (#v_T: Type0)
-      {| i1: Core.Cmp.t_Ord v_T |}
+      {| i1: Core_models.Cmp.t_Ord v_T |}
       (self: t_SortedSet v_T)
     : Prims.Pure Rust_primitives.Hax.failure Prims.l_True (fun _ -> Prims.l_True) *)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_11 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} : Core.Default.t_Default (t_SortedSet v_T)
+val impl_11 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} : Core_models.Default.t_Default (t_SortedSet v_T)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_12 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |}
-    : Core.Convert.t_From (t_SortedSet v_T) (Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
+val impl_12 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Convert.t_From (t_SortedSet v_T) (Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_13 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cmp.t_Ord v_T)
-    : Core.Ops.Deref.t_Deref (t_SortedSet v_T) =
+let impl_13 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core_models.Cmp.t_Ord v_T)
+    : Core_models.Ops.Deref.t_Deref (t_SortedSet v_T) =
   {
     f_Target = t_SortedVec v_T;
     (* f_deref_pre = (fun (self: t_SortedSet v_T) -> true);
@@ -572,16 +572,16 @@ let impl_13 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cm
   }
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_14 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |}
-    : Core.Iter.Traits.Collect.t_Extend (t_SortedSet v_T) v_T *)
+val impl_14 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |}
+    : Core_models.Iter.Traits.Collect.t_Extend (t_SortedSet v_T) v_T *)
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_15 (#v_T: Type0) {| i1: Core.Cmp.t_Ord v_T |} {| i2: Core.Hash.t_Hash v_T |}
-    : Core.Hash.t_Hash (t_SortedSet v_T) *)
+val impl_15 (#v_T: Type0) {| i1: Core_models.Cmp.t_Ord v_T |} {| i2: Core_models.Hash.t_Hash v_T |}
+    : Core_models.Hash.t_Hash (t_SortedSet v_T) *)
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_8 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cmp.t_Ord v_T)
-    : Core.Iter.Traits.Collect.t_IntoIterator (t_SortedVec v_T) =
+let impl_8 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core_models.Cmp.t_Ord v_T)
+    : Core_models.Iter.Traits.Collect.t_IntoIterator (t_SortedVec v_T) =
   {
     f_Item = v_T;
     f_IntoIter = Alloc.Vec.Into_iter.t_IntoIter v_T Alloc.Alloc.t_Global;
@@ -594,25 +594,25 @@ let impl_8 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cmp
     f_into_iter
     =
     fun (self: t_SortedVec v_T) ->
-      Core.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
+      Core_models.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
         #FStar.Tactics.Typeclasses.solve
         self.f_vec
   } *)
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_9 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cmp.t_Ord v_T)
-    : Core.Iter.Traits.Collect.t_IntoIterator (t_SortedVec v_T) =
+let impl_9 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core_models.Cmp.t_Ord v_T)
+    : Core_models.Iter.Traits.Collect.t_IntoIterator (t_SortedVec v_T) =
   {
     f_Item = v_T;
-    f_IntoIter = Core.Slice.Iter.t_Iter v_T;
+    f_IntoIter = Core_models.Slice.Iter.t_Iter v_T;
     f_IntoIter_8492263130362933403 = FStar.Tactics.Typeclasses.solve;
     f_into_iter_pre = (fun (self: t_SortedVec v_T) -> true);
-    f_into_iter_post = (fun (self: t_SortedVec v_T) (out: Core.Slice.Iter.t_Iter v_T) -> true);
+    f_into_iter_post = (fun (self: t_SortedVec v_T) (out: Core_models.Slice.Iter.t_Iter v_T) -> true);
     f_into_iter
     =
     fun (self: t_SortedVec v_T) ->
-      Core.Slice.impl__iter #v_T
-        (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
+      Core_models.Slice.impl__iter #v_T
+        (Core_models.Ops.Deref.f_deref #(Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
             #FStar.Tactics.Typeclasses.solve
             self.f_vec
           <:
@@ -620,21 +620,21 @@ let impl_9 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cmp
   } *)
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_17 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cmp.t_Ord v_T)
-    : Core.Iter.Traits.Collect.t_IntoIterator (t_SortedSet v_T) =
+let impl_17 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core_models.Cmp.t_Ord v_T)
+    : Core_models.Iter.Traits.Collect.t_IntoIterator (t_SortedSet v_T) =
   {
     f_Item = v_T;
-    f_IntoIter = Core.Slice.Iter.t_Iter v_T;
+    f_IntoIter = Core_models.Slice.Iter.t_Iter v_T;
     f_IntoIter_8492263130362933403 = FStar.Tactics.Typeclasses.solve;
     f_into_iter_pre = (fun (self: t_SortedSet v_T) -> true);
-    f_into_iter_post = (fun (self: t_SortedSet v_T) (out: Core.Slice.Iter.t_Iter v_T) -> true);
+    f_into_iter_post = (fun (self: t_SortedSet v_T) (out: Core_models.Slice.Iter.t_Iter v_T) -> true);
     f_into_iter
     =
     fun (self: t_SortedSet v_T) ->
-      Core.Slice.impl__iter #v_T
-        (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
+      Core_models.Slice.impl__iter #v_T
+        (Core_models.Ops.Deref.f_deref #(Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
             #FStar.Tactics.Typeclasses.solve
-            (Core.Ops.Deref.f_deref #(t_SortedVec v_T) #FStar.Tactics.Typeclasses.solve self.f_set
+            (Core_models.Ops.Deref.f_deref #(t_SortedVec v_T) #FStar.Tactics.Typeclasses.solve self.f_set
               <:
               Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global)
           <:
@@ -642,8 +642,8 @@ let impl_17 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cm
   } *)
 
 (* [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_16 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cmp.t_Ord v_T)
-    : Core.Iter.Traits.Collect.t_IntoIterator (t_SortedSet v_T) =
+let impl_16 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core_models.Cmp.t_Ord v_T)
+    : Core_models.Iter.Traits.Collect.t_IntoIterator (t_SortedSet v_T) =
   {
     f_Item = v_T;
     f_IntoIter = Alloc.Vec.Into_iter.t_IntoIter v_T Alloc.Alloc.t_Global;
@@ -656,7 +656,7 @@ let impl_16 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Cm
     f_into_iter
     =
     fun (self: t_SortedSet v_T) ->
-      Core.Iter.Traits.Collect.f_into_iter #(t_SortedVec v_T)
+      Core_models.Iter.Traits.Collect.f_into_iter #(t_SortedVec v_T)
         #FStar.Tactics.Typeclasses.solve
         self.f_set
   } *)

proofs/fstar/models/Spec.GF16.fst

@@ -1,5 +1,5 @@
 module Spec.GF16
-open Core
+open Core_models
 
 (** Boolean Operations **)
 

proofs/fstar/models/Spec.MLKEM.Instances.fst

@@ -1,7 +1,7 @@
 module Spec.MLKEM.Instances
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 30"
 open FStar.Mul
-open Core
+open Core_models
 open Spec.Utils
 open Spec.MLKEM.Math
 open Spec.MLKEM

proofs/fstar/models/Spec.MLKEM.Math.fst

@@ -2,7 +2,7 @@ module Spec.MLKEM.Math
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 
 open FStar.Mul
-open Core
+open Core_models
 open Spec.Utils
 
 let v_FIELD_MODULUS: i32 = mk_i32 3329

proofs/fstar/models/Spec.MLKEM.fst

@@ -1,7 +1,7 @@
 module Spec.MLKEM
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open FStar.Mul
-open Core
+open Core_models
 
 include Spec.Utils
 include Spec.MLKEM.Math

proofs/fstar/models/Spec.Utils.fsti

@@ -1,7 +1,7 @@
 module Spec.Utils
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
 open FStar.Mul
-open Core
+open Core_models
 
 (** Utils *)
 let map_slice #a #b
@@ -92,7 +92,7 @@ val v_XOF (v_LEN: usize{v v_LEN < pow2 32}) (input: t_Slice u8) : t_Array u8 v_L
 
 val update_at_range_lemma #n
   (s: t_Slice 't)
-  (i: Core.Ops.Range.t_Range (int_t n) {(Core.Ops.Range.impl_index_range_slice 't n).f_index_pre s i}) 
+  (i: Core_models.Ops.Range.t_Range (int_t n) {(Core_models.Ops.Range.impl_index_range_slice 't n).f_index_pre s i}) 
   (x: t_Slice 't)
   : Lemma
     (requires (Seq.length x == v i.f_end - v i.f_start))

src/chain.rs

@@ -224,6 +224,7 @@ impl ChainEpochDirection {
     }
 
     #[hax_lib::requires(next.len() > 0 && *ctr < u32::MAX)]
+    #[hax_lib::ensures(|_| *future(ctr) == ctr + 1)]
     fn next_key_internal(next: &mut [u8], ctr: &mut u32) -> (u32, [u8; 32]) {
         assert!(!next.is_empty());
         *ctr += 1;
@@ -231,11 +232,12 @@ impl ChainEpochDirection {
         kdf::hkdf_to_slice(
             &[0u8; 32], // 32 is the hash output length
             &*next,
-            &[
+            [
                 ctr.to_be_bytes().as_slice(),
                 b"Signal PQ Ratchet V1 Chain Next",
             ]
-            .concat(),
+            .concat()
+            .as_slice(),
             &mut genr8r,
         );
         next.copy_from_slice(&genr8r[..32]);
@@ -265,11 +267,20 @@ impl ChainEpochDirection {
             // them all.
             self.prev.clear();
         }
-        hax_lib::fstar!("admit ()"); // potential overflows in condition and body of the loop
         while at > self.ctr + 1 {
+            hax_lib::loop_invariant!(self.ctr < u32::MAX);
+            hax_lib::loop_decreases!(u32::MAX - self.ctr);
+            hax_lib::assume!(self.next.len() > 0);
             let k = Self::next_key_internal(&mut self.next, &mut self.ctr);
+            hax_lib::assume!(
+                params.max_ooo_keys_or_default() < 390451572 && self.ctr <= u32::MAX - 390451572
+            );
             // Only add keys into our history if we're not going to immediately GC them.
             if self.ctr + params.max_ooo_keys_or_default() >= at {
+                hax_lib::assume!(
+                    params.trim_size() < 119304647
+                        && self.prev.data.len() <= KeyHistory::KEY_SIZE * params.trim_size()
+                );
                 self.prev.add(k, params);
             }
         }
@@ -277,6 +288,8 @@ impl ChainEpochDirection {
         // want to throw away.
         self.prev.gc(self.ctr, params);
 
+        hax_lib::assume!(self.next.len() > 0);
+
         Ok(Self::next_key_internal(&mut self.next, &mut self.ctr)
             .1
             .to_vec())

src/encoding/gf.rs

@@ -196,11 +196,15 @@ impl ops::Div<&GF16> for GF16 {
 }
 
 #[inline]
-#[hax_lib::fstar::verification_status(lax)] // proving absence of overflow in loop condition is tricky
+#[hax_lib::requires(into.len() <= usize::MAX - 2)]
+#[hax_lib::ensures(|_| future(into).len() == into.len())]
 pub fn parallel_mult(a: GF16, into: &mut [GF16]) {
-    let mut i = 0;
+    let mut i: usize = 0;
+    #[cfg(hax)]
+    let l = into.len();
     while i + 2 <= into.len() {
-        hax_lib::loop_decreases!(into.len() - i);
+        hax_lib::loop_decreases!(l - i);
+        hax_lib::loop_invariant!(into.len() == l && i <= l);
         (into[i].value, into[i + 1].value) = mul2_u16(a.value, into[i].value, into[i + 1].value);
         i += 2;
     }
@@ -267,7 +271,7 @@ mod accelerated {
     }
 
     #[inline]
-    #[target_feature(enable = "neon")]
+    #[target_feature(enable = "neon,aes")]
     unsafe fn mul2_unreduced(a: u16, b1: u16, b2: u16) -> u128 {
         aarch64::vmull_p64(a as u64, ((b1 as u64) << 32) | (b2 as u64))
     }
@@ -587,8 +591,8 @@ impl GF16 {
 #[cfg(test)]
 mod test {
     use super::*;
-    use galois_field_2pm::gf2::GFu16;
     use galois_field_2pm::GaloisField;
+    use galois_field_2pm::gf2::GFu16;
     use rand::RngCore;
 
     // https://web.eecs.utk.edu/~jplank/plank/papers/CS-07-593/primitive-polynomial-table.txt

src/encoding/polynomial.rs

@@ -75,6 +75,7 @@ pub const MAX_STORED_POLYNOMIAL_DEGREE_V1: usize = 35;
 pub const MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1: usize = 36;
 
 #[derive(Clone, PartialEq)]
+#[hax_lib::attributes]
 pub(crate) struct Poly {
     // For Protocol V1 we interpolate at most 36 values, which produces a
     // degree 35 polynomial (with 36 coefficients). In an intermediate calculation
@@ -82,6 +83,7 @@ pub(crate) struct Poly {
     // higher, thus we get the following constraint:
     //
     // coefficients.len() <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1 + 1
+    #[hax_lib::refine(coefficients.len() <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1 + 1)]
     pub coefficients: Vec<GF16>,
 }
 
@@ -249,6 +251,7 @@ impl Poly {
         gf::parallel_mult(m, &mut self.coefficients);
     }
 
+    #[hax_lib::opaque] // zip
     fn compute_at(&self, x: GF16) -> GF16 {
         // Compute x^0 .. x^N
         let mut xs = Vec::with_capacity(self.coefficients.len());
@@ -269,6 +272,7 @@ impl Poly {
     }
 
     /// Internal function for lagrange_polynomial_from_complete_points.
+    #[hax_lib::opaque] // zip
     fn lagrange_sum(pts: &[Pt], polys: &[Poly]) -> Poly {
         let mut out = Poly::zero(pts.len());
         for (pt, poly) in pts.iter().zip(polys.iter()) {
@@ -283,6 +287,7 @@ impl Poly {
     /// range [0..pts.len()), return a polynomial that computes those points.
     #[hax_lib::requires(pts.len() == 0 || pts.len() == 1 || pts.len() == 3 || pts.len() == 5
     || pts.len() == 30 || pts.len() == 34 || pts.len() == 36)]
+    #[hax_lib::opaque] // iterators
     fn from_complete_points(pts: &[Pt]) -> Result<Poly, ()> {
         for (i, pt) in pts.iter().enumerate() {
             if pt.x.value != i as u16 {
@@ -318,7 +323,6 @@ impl Poly {
         Ok(Self::lagrange_sum(pts, &polys))
     }
 
-    #[hax_lib::requires(self.coefficients.len() <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1)]
     pub fn serialize(&self) -> Vec<u8> {
         // For Protocol V1 the polynomials that get serialized will always have
         // coefficients.len() <= MAX_STORED_POLYNOMIAL_DEGREE_V1 + 1
@@ -340,6 +344,7 @@ impl Poly {
         for coeff in serialized.chunks_exact(2) {
             coefficients.push(GF16::new(u16::from_be_bytes(coeff.try_into().unwrap())));
         }
+        hax_lib::assume!(coefficients.len() <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1 + 1);
         Ok(Self { coefficients })
     }
 }
@@ -445,6 +450,7 @@ impl<const N: usize> PolyConst<N> {
     }
 
     fn to_poly(&self) -> Poly {
+        hax_lib::assume!(N <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1 + 1);
         Poly {
             coefficients: self.coefficients.to_vec(),
         }
@@ -499,11 +505,18 @@ const CHUNK_SIZE: usize = 32;
 // Number of polys or points that need to be tracked when using GF(2^16) with 2-byte elements
 pub const NUM_POLYS: usize = CHUNK_SIZE / 2;
 
+#[derive(Clone)]
+#[hax_lib::attributes]
+pub struct Point {
+    #[hax_lib::refine(value.len() <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1)]
+    pub value: Vec<GF16>,
+}
+
 #[cfg_attr(test, derive(Clone))]
 pub(crate) enum EncoderState {
     // For 32B chunks the outer vector has length 16.
     // Using MLKEM-768 the inner vector has length <= MAX_STORED_POLYNOMIAL_DEGREE_V1 + 1
-    Points([Vec<GF16>; NUM_POLYS]),
+    Points([Point; NUM_POLYS]),
     // For 32B chunks this vector has length 16.
     Polys([Poly; NUM_POLYS]),
 }
@@ -521,13 +534,7 @@ impl PolyEncoder {
         &self.s
     }
 
-    #[hax_lib::requires(match self.s {
-        EncoderState::Points(points) => hax_lib::Prop::from(points.len() == 16).and(hax_lib::prop::forall(|pts: &Vec<GF16>|
-            hax_lib::prop::implies(points.contains(pts), pts.len() <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1))),
-        EncoderState::Polys(polys) => hax_lib::Prop::from(polys.len() == 16).and(hax_lib::prop::forall(|poly: &Poly|
-            hax_lib::prop::implies(polys.contains(poly), poly.coefficients.len() <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1)))
-    })]
-    pub(crate) fn into_pb(self) -> proto::pq_ratchet::PolynomialEncoder {
+    pub fn into_pb(self) -> proto::pq_ratchet::PolynomialEncoder {
         let mut out = proto::pq_ratchet::PolynomialEncoder {
             idx: self.idx,
             pts: Vec::with_capacity(16),
@@ -539,7 +546,7 @@ impl PolyEncoder {
                 #[allow(clippy::needless_range_loop)]
                 for j in 0..points.len() {
                     hax_lib::loop_invariant!(|j: usize| out.pts.len() == j);
-                    let pts = &points[j];
+                    let pts = &points[j].value;
                     let mut v = Vec::<u8>::with_capacity(2 * pts.len());
                     #[allow(clippy::needless_range_loop)]
                     for i in 0..pts.len() {
@@ -569,16 +576,12 @@ impl PolyEncoder {
             if pb.pts.len() != NUM_POLYS {
                 return Err(PolynomialError::SerializationInvalid);
             }
-            let mut out = core::array::from_fn(|_| Vec::<GF16>::new());
+            let mut out = core::array::from_fn(|_| Point {
+                value: Vec::<GF16>::new(),
+            });
 
             #[allow(clippy::needless_range_loop)]
             for i in 0..NUM_POLYS {
-                hax_lib::loop_invariant!(|_: usize| hax_lib::prop::forall(|pts: &Vec<GF16>| {
-                    hax_lib::prop::implies(
-                        out.contains(pts),
-                        pts.len() <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1,
-                    )
-                }));
                 let pts = &pb.pts[i];
                 if pts.len() % 2 != 0 {
                     return Err(PolynomialError::SerializationInvalid);
@@ -587,7 +590,8 @@ impl PolyEncoder {
                 for pt in pts.chunks_exact(2) {
                     v.push(GF16::new(u16::from_be_bytes(pt.try_into().unwrap())));
                 }
-                out[i] = v;
+                hax_lib::assume!(v.len() <= MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1);
+                out[i] = Point { value: v };
             }
             EncoderState::Points(out)
         } else if pb.polys.len() == NUM_POLYS {
@@ -603,11 +607,12 @@ impl PolyEncoder {
     }
 
     #[requires(poly < 16)]
+    #[hax_lib::opaque] // iterators
     fn point_at(&mut self, poly: usize, idx: usize) -> GF16 {
         if let EncoderState::Points(ref pts) = self.s {
             hax_lib::assume!(pts.len() == 16);
-            if idx < pts[poly].len() {
-                return pts[poly][idx];
+            if idx < pts[poly].value.len() {
+                return pts[poly].value[idx];
             }
             // If we reach here, we've come to the first point we want to
             // find that wasn't part of the original set of points.  We
@@ -617,6 +622,7 @@ impl PolyEncoder {
             let mut polys: [Poly; NUM_POLYS] = core::array::from_fn(|_| Poly::zero(1));
             for i in 0..NUM_POLYS {
                 let pt_vec = pts[i]
+                    .value
                     .iter()
                     .enumerate()
                     .map(|(x, y)| Pt {
@@ -654,12 +660,16 @@ impl PolyEncoder {
         } else if msg.len() > (1 << 16) * NUM_POLYS {
             return Err(PolynomialError::MessageLengthTooLong.into());
         }
-        let mut pts: [Vec<GF16>; NUM_POLYS] =
-            core::array::from_fn(|_| Vec::<GF16>::with_capacity(msg.len() / 2));
+        let mut pts: [Point; NUM_POLYS] = core::array::from_fn(|_| Point {
+            value: Vec::<GF16>::with_capacity(msg.len() / 2),
+        });
         for (i, c) in msg.chunks_exact(2).enumerate() {
             hax_lib::loop_invariant!(|_: usize| pts.len() >= NUM_POLYS);
             let poly = i % pts.len();
-            pts[poly].push(GF16::new(((c[0] as u16) << 8) + (c[1] as u16)));
+            hax_lib::assume!(pts[poly].value.len() < MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1);
+            pts[poly]
+                .value
+                .push(GF16::new(((c[0] as u16) << 8) + (c[1] as u16)));
         }
         Ok(Self {
             idx: 0,
@@ -755,6 +765,7 @@ impl PolyDecoder {
         }
     }
 
+    #[hax_lib::ensures(|res| hax_lib::implies(len_bytes % 2 == 0, res.is_ok() && res.unwrap().pts_needed == len_bytes / 2))]
     fn new_with_poly_count(len_bytes: usize, _polys: usize) -> Result<Self, super::EncodingError> {
         if len_bytes % 2 != 0 {
             return Err(PolynomialError::MessageLengthEven.into());
@@ -786,17 +797,16 @@ impl PolyDecoder {
         out
     }
 
+    #[hax_lib::ensures(|res| hax_lib::implies(res.is_ok(), res.unwrap().pts_needed == pb.pts_needed as usize))]
+    #[hax_lib::opaque] // return in loop
     pub(crate) fn from_pb(
         pb: proto::pq_ratchet::PolynomialDecoder,
     ) -> Result<Self, PolynomialError> {
         if pb.pts.len() != 16 {
             return Err(PolynomialError::SerializationInvalid);
         }
-        let mut out = Self {
-            pts_needed: pb.pts_needed as usize,
-            is_complete: pb.is_complete,
-            pts: core::array::from_fn(|_| SortedSet::new()),
-        };
+        let mut out_pts = core::array::from_fn(|_| SortedSet::new());
+        #[allow(clippy::needless_range_loop)]
         for i in 0..16 {
             let pts = &pb.pts[i];
             if pts.len() % 4 != 0 {
@@ -806,9 +816,13 @@ impl PolyDecoder {
             for pt in pts.chunks_exact(4) {
                 v.push(Pt::deserialize(pt.try_into().unwrap()));
             }
-            out.pts[i] = v;
+            out_pts[i] = v;
         }
-        Ok(out)
+        Ok(Self {
+            pts_needed: pb.pts_needed as usize,
+            is_complete: pb.is_complete,
+            pts: out_pts,
+        })
     }
 
     /// Public wrapper for test utilities and benchmarks.
@@ -828,14 +842,19 @@ impl PolyDecoder {
 
 #[hax_lib::attributes]
 impl Decoder for PolyDecoder {
+    #[hax_lib::ensures(|res| hax_lib::implies(len_bytes % 2 == 0, res.is_ok() && res.unwrap().pts_needed == len_bytes / 2))]
     fn new(len_bytes: usize) -> Result<Self, super::EncodingError> {
         Self::new_with_poly_count(len_bytes, 16)
     }
 
-    #[hax_lib::requires(self.pts.len() == 16)]
+    #[hax_lib::ensures(|_| future(self).pts_needed == self.pts_needed)]
     fn add_chunk(&mut self, chunk: &Chunk) {
+        #[cfg(hax)]
+        let initial_pts_needed = self.pts_needed;
         for i in 0usize..16 {
-            hax_lib::loop_invariant!(|_: usize| self.pts.len() == 16);
+            hax_lib::loop_invariant!(
+                |_: usize| self.pts.len() == 16 && self.pts_needed == initial_pts_needed
+            );
             let total_idx = (chunk.index as usize) * 16 + i;
             let poly = total_idx % 16;
             let poly_idx = total_idx / 16;
@@ -856,20 +875,28 @@ impl Decoder for PolyDecoder {
         }
     }
 
-    #[hax_lib::requires(self.pts_needed < MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1)]
+    #[hax_lib::requires(self.pts_needed < usize::MAX / 2)]
+    #[hax_lib::ensures(|res| match res {
+        Some(v) => v.len() / 2 == self.pts_needed,
+        None => true
+    })]
     fn decoded_message(&self) -> Option<Vec<u8>> {
         if self.is_complete {
             return None;
         }
         let mut points_vecs = Vec::with_capacity(self.pts.len());
+        let mut ret_none = false;
         for i in 0..(self.pts.len()) {
             let pts = &self.pts[i];
             if pts.len() < self.necessary_points(i) {
-                return None;
+                ret_none = true;
             } else {
                 points_vecs.push(&pts[..self.necessary_points(i)]);
             }
         }
+        if ret_none {
+            return None;
+        }
         // We may or may not need these vectors of points (only if we need
         // to do a lagrange_interpolate call).  For now, we just create
         // them regardless.  However, we could optimize to lazily create them
@@ -877,6 +904,7 @@ impl Decoder for PolyDecoder {
         let mut polys: [Option<Poly>; 16] = core::array::from_fn(|_| None);
         let mut out: Vec<u8> = Vec::with_capacity(self.pts_needed * 2);
         for i in 0..self.pts_needed {
+            hax_lib::loop_invariant!(|i: usize| out.len() == i * 2);
             let poly = i % 16;
             let poly_idx = i / 16;
             let pt = Pt {

src/incremental_mlkem768.rs

@@ -30,7 +30,7 @@ pub fn ek_matches_header(ek: &EncapsulationKey, hdr: &Header) -> bool {
 }
 
 /// Generate a new keypair and associated header.
-#[hax_lib::ensures(|result| result.hdr.len() == 64 && result.ek.len() == 1152 && result.dk.len() == 2400)]
+#[hax_lib::ensures(|result| result.hdr.len() == HEADER_SIZE && result.ek.len() == ENCAPSULATION_KEY_SIZE && result.dk.len() == 2400)]
 pub fn generate<R: Rng + CryptoRng>(rng: &mut R) -> Keys {
     let mut randomness = [0u8; libcrux_ml_kem::KEY_GENERATION_SEED_SIZE];
     rng.fill_bytes(&mut randomness);

src/v1/chunked/send_ct.rs

@@ -12,24 +12,30 @@ use crate::{Epoch, EpochSecret, Error};
 use rand::{CryptoRng, Rng};
 
 #[cfg_attr(test, derive(Clone))]
+#[hax_lib::attributes]
 pub struct NoHeaderReceived {
     pub(super) uc: unchunked::NoHeaderReceived,
     // `receiving_hdr` only decodes messages of length `incremental_mlkem768::HEADER_SIZE + authenticator::Authenticator::MACSIZE`
+    #[hax_lib::refine(receiving_hdr.get_pts_needed() == (incremental_mlkem768::HEADER_SIZE + authenticator::Authenticator::MACSIZE) / 2)]
     pub(super) receiving_hdr: polynomial::PolyDecoder,
 }
 
 #[cfg_attr(test, derive(Clone))]
+#[hax_lib::attributes]
 pub struct HeaderReceived {
     uc: unchunked::HeaderReceived,
     // `receiving_ek` only decodes messages of length `incremental_mlkem768::ENCAPSULATION_KEY_SIZE`
+    #[hax_lib::refine(receiving_ek.get_pts_needed() == incremental_mlkem768::ENCAPSULATION_KEY_SIZE / 2)]
     receiving_ek: polynomial::PolyDecoder,
 }
 
 #[cfg_attr(test, derive(Clone))]
+#[hax_lib::attributes]
 pub struct Ct1Sampled {
     uc: unchunked::Ct1Sent,
     sending_ct1: polynomial::PolyEncoder,
     // `receiving_ek` only decodes messages of length `incremental_mlkem768::ENCAPSULATION_KEY_SIZE`
+    #[hax_lib::refine(receiving_ek.get_pts_needed() == incremental_mlkem768::ENCAPSULATION_KEY_SIZE / 2)]
     receiving_ek: polynomial::PolyDecoder,
 }
 
@@ -40,9 +46,11 @@ pub struct EkReceivedCt1Sampled {
 }
 
 #[cfg_attr(test, derive(Clone))]
+#[hax_lib::attributes]
 pub struct Ct1Acknowledged {
     uc: unchunked::Ct1Sent,
     // `receiving_ek` only decodes messages of length `incremental_mlkem768::ENCAPSULATION_KEY_SIZE`
+    #[hax_lib::refine(receiving_ek.get_pts_needed() == incremental_mlkem768::ENCAPSULATION_KEY_SIZE / 2)]
     receiving_ek: polynomial::PolyDecoder,
 }
 
@@ -64,7 +72,6 @@ impl NoHeaderReceived {
         let decoder = polynomial::PolyDecoder::new(
             incremental_mlkem768::HEADER_SIZE + authenticator::Authenticator::MACSIZE,
         );
-        hax_lib::assume!(decoder.is_ok());
         NoHeaderReceived {
             uc: unchunked::NoHeaderReceived::new(auth_key),
             receiving_hdr: decoder.expect("should be able to decode header size"),
@@ -83,15 +90,10 @@ impl NoHeaderReceived {
             mut receiving_hdr,
         } = self;
         receiving_hdr.add_chunk(chunk);
-        hax_lib::assume!(
-            receiving_hdr.get_pts_needed() <= polynomial::MAX_STORED_POLYNOMIAL_DEGREE_V1
-        );
         if let Some(mut hdr) = receiving_hdr.decoded_message() {
-            let mac: authenticator::Mac = hdr.drain(incremental_mlkem768::HEADER_SIZE..).collect();
-            hax_lib::assume!(hdr.len() == 64 && mac.len() == authenticator::Authenticator::MACSIZE);
+            let mac: authenticator::Mac = hdr.split_off(incremental_mlkem768::HEADER_SIZE);
             let receiving_ek =
                 polynomial::PolyDecoder::new(incremental_mlkem768::ENCAPSULATION_KEY_SIZE);
-            hax_lib::assume!(receiving_ek.is_ok());
             Ok(NoHeaderReceivedRecvChunk::Done(HeaderReceived {
                 uc: uc.recv_header(epoch, hdr, &mac)?,
                 receiving_ek: receiving_ek.expect("should be able to decode EncapsulationKey size"),
@@ -123,7 +125,6 @@ impl HeaderReceived {
 
         let (uc, ct1, epoch_secret) = uc.send_ct1(rng);
         let encoder = polynomial::PolyEncoder::encode_bytes(&ct1);
-        hax_lib::assume!(encoder.is_ok());
         let mut sending_ct1 = encoder.expect("should be able to send CTSIZE");
         let chunk = sending_ct1.next_chunk();
         (
@@ -151,12 +152,11 @@ pub enum Ct1SampledRecvChunk {
     Done(Ct2Sampled),
 }
 
+#[hax_lib::requires(ct2.len() == 128 && mac.len() == authenticator::Authenticator::MACSIZE)]
 fn send_ct2_encoder(ct2: &[u8], mac: &[u8]) -> polynomial::PolyEncoder {
-    hax_lib::assume!(
-        [ct2, mac].concat().len() % 2 == 0
-            && [ct2, mac].concat().len() <= (1 << 16) * crate::encoding::polynomial::NUM_POLYS
-    );
-    polynomial::PolyEncoder::encode_bytes(&[ct2, mac].concat()).expect("should be able to send ct2")
+    let mut msg = ct2.to_vec();
+    msg.extend_from_slice(mac);
+    polynomial::PolyEncoder::encode_bytes(&msg).expect("should be able to send ct2")
 }
 
 #[hax_lib::attributes]
@@ -174,19 +174,10 @@ impl Ct1Sampled {
             sending_ct1,
         } = self;
         receiving_ek.add_chunk(chunk);
-        hax_lib::assume!(
-            receiving_ek.get_pts_needed() <= polynomial::MAX_STORED_POLYNOMIAL_DEGREE_V1
-        );
         Ok(if let Some(decoded) = receiving_ek.decoded_message() {
-            hax_lib::assume!(decoded.len() == 1152);
             let uc = uc.recv_ek(epoch, decoded)?;
             if ct1_ack {
                 let (uc, ct2, mac) = uc.send_ct2();
-                hax_lib::assume!(
-                    [ct2.clone(), mac.clone()].concat().len() % 2 == 0
-                        && [ct2.clone(), mac.clone()].concat().len()
-                            <= (1 << 16) * crate::encoding::polynomial::NUM_POLYS
-                );
                 Ct1SampledRecvChunk::Done(Ct2Sampled {
                     uc,
                     sending_ct2: send_ct2_encoder(&ct2, &mac),
@@ -272,11 +263,7 @@ impl Ct1Acknowledged {
             mut receiving_ek,
         } = self;
         receiving_ek.add_chunk(chunk);
-        hax_lib::assume!(
-            receiving_ek.get_pts_needed() <= polynomial::MAX_STORED_POLYNOMIAL_DEGREE_V1
-        );
         Ok(if let Some(decoded) = receiving_ek.decoded_message() {
-            hax_lib::assume!(decoded.len() == 1152);
             let uc = uc.recv_ek(epoch, decoded)?;
             let (uc, ct2, mac) = uc.send_ct2();
             Ct1AcknowledgedRecvChunk::Done(Ct2Sampled {

src/v1/chunked/send_ct/serialize.rs

@@ -6,6 +6,7 @@ use crate::encoding::polynomial;
 use crate::proto::pq_ratchet as pqrpb;
 use crate::v1::unchunked;
 
+#[hax_lib::attributes]
 impl NoHeaderReceived {
     pub fn into_pb(self) -> pqrpb::v1_state::chunked::NoHeaderReceived {
         pqrpb::v1_state::chunked::NoHeaderReceived {
@@ -15,6 +16,15 @@ impl NoHeaderReceived {
     }
 
     pub fn from_pb(pb: pqrpb::v1_state::chunked::NoHeaderReceived) -> Result<Self, Error> {
+        if let Some(rhdr) = &pb.receiving_hdr {
+            if rhdr.pts_needed
+                != ((crate::incremental_mlkem768::HEADER_SIZE
+                    + crate::authenticator::Authenticator::MACSIZE)
+                    / 2) as u32
+            {
+                return Err(Error::MsgDecode);
+            }
+        }
         Ok(Self {
             uc: unchunked::send_ct::NoHeaderReceived::from_pb(pb.uc.ok_or(Error::StateDecode)?)?,
             receiving_hdr: polynomial::PolyDecoder::from_pb(
@@ -34,6 +44,11 @@ impl HeaderReceived {
     }
 
     pub fn from_pb(pb: pqrpb::v1_state::chunked::HeaderReceived) -> Result<Self, Error> {
+        if let Some(d) = &pb.receiving_ek {
+            if d.pts_needed as usize != crate::incremental_mlkem768::ENCAPSULATION_KEY_SIZE / 2 {
+                return Err(Error::MsgDecode);
+            }
+        }
         Ok(Self {
             uc: unchunked::send_ct::HeaderReceived::from_pb(pb.uc.ok_or(Error::StateDecode)?)?,
             receiving_ek: polynomial::PolyDecoder::from_pb(
@@ -46,19 +61,6 @@ impl HeaderReceived {
 
 impl Ct1Sampled {
     pub fn into_pb(self) -> pqrpb::v1_state::chunked::Ct1Sampled {
-        hax_lib::assume!(match self.sending_ct1.get_encoder_state() {
-            polynomial::EncoderState::Points(points) => hax_lib::prop::forall(
-                |pts: &Vec<crate::encoding::gf::GF16>| hax_lib::prop::implies(
-                    points.contains(pts),
-                    pts.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )
-            ),
-            polynomial::EncoderState::Polys(polys) =>
-                hax_lib::prop::forall(|poly: &polynomial::Poly| hax_lib::prop::implies(
-                    polys.contains(poly),
-                    poly.coefficients.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )),
-        });
         pqrpb::v1_state::chunked::Ct1Sampled {
             uc: Some(self.uc.into_pb()),
             sending_ct1: Some(self.sending_ct1.into_pb()),
@@ -67,6 +69,11 @@ impl Ct1Sampled {
     }
 
     pub fn from_pb(pb: pqrpb::v1_state::chunked::Ct1Sampled) -> Result<Self, Error> {
+        if let Some(d) = &pb.receiving_ek {
+            if d.pts_needed as usize != crate::incremental_mlkem768::ENCAPSULATION_KEY_SIZE / 2 {
+                return Err(Error::MsgDecode);
+            }
+        }
         Ok(Self {
             uc: unchunked::send_ct::Ct1Sent::from_pb(pb.uc.ok_or(Error::StateDecode)?)?,
             sending_ct1: polynomial::PolyEncoder::from_pb(
@@ -83,19 +90,6 @@ impl Ct1Sampled {
 
 impl EkReceivedCt1Sampled {
     pub fn into_pb(self) -> pqrpb::v1_state::chunked::EkReceivedCt1Sampled {
-        hax_lib::assume!(match self.sending_ct1.get_encoder_state() {
-            polynomial::EncoderState::Points(points) => hax_lib::prop::forall(
-                |pts: &Vec<crate::encoding::gf::GF16>| hax_lib::prop::implies(
-                    points.contains(pts),
-                    pts.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )
-            ),
-            polynomial::EncoderState::Polys(polys) =>
-                hax_lib::prop::forall(|poly: &polynomial::Poly| hax_lib::prop::implies(
-                    polys.contains(poly),
-                    poly.coefficients.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )),
-        });
         pqrpb::v1_state::chunked::EkReceivedCt1Sampled {
             uc: Some(self.uc.into_pb()),
             sending_ct1: Some(self.sending_ct1.into_pb()),
@@ -122,6 +116,11 @@ impl Ct1Acknowledged {
     }
 
     pub fn from_pb(pb: pqrpb::v1_state::chunked::Ct1Acknowledged) -> Result<Self, Error> {
+        if let Some(d) = &pb.receiving_ek {
+            if d.pts_needed as usize != crate::incremental_mlkem768::ENCAPSULATION_KEY_SIZE / 2 {
+                return Err(Error::MsgDecode);
+            }
+        }
         Ok(Self {
             uc: unchunked::send_ct::Ct1Sent::from_pb(pb.uc.ok_or(Error::StateDecode)?)?,
             receiving_ek: polynomial::PolyDecoder::from_pb(
@@ -134,19 +133,6 @@ impl Ct1Acknowledged {
 
 impl Ct2Sampled {
     pub fn into_pb(self) -> pqrpb::v1_state::chunked::Ct2Sampled {
-        hax_lib::assume!(match self.sending_ct2.get_encoder_state() {
-            polynomial::EncoderState::Points(points) => hax_lib::prop::forall(
-                |pts: &Vec<crate::encoding::gf::GF16>| hax_lib::prop::implies(
-                    points.contains(pts),
-                    pts.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )
-            ),
-            polynomial::EncoderState::Polys(polys) =>
-                hax_lib::prop::forall(|poly: &polynomial::Poly| hax_lib::prop::implies(
-                    polys.contains(poly),
-                    poly.coefficients.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )),
-        });
         pqrpb::v1_state::chunked::Ct2Sampled {
             uc: Some(self.uc.into_pb()),
             sending_ct2: Some(self.sending_ct2.into_pb()),

src/v1/chunked/send_ek.rs

@@ -24,10 +24,12 @@ pub struct KeysSampled {
 }
 
 #[cfg_attr(test, derive(Clone))]
+#[hax_lib::attributes]
 pub struct HeaderSent {
     uc: unchunked::EkSent,
     sending_ek: polynomial::PolyEncoder,
     // `receiving_ct1` only decodes messages of length `incremental_mlkem768::CIPHERTEXT1_SIZE`
+    #[hax_lib::refine(receiving_ct1.pts_needed == incremental_mlkem768::CIPHERTEXT1_SIZE / 2)]
     receiving_ct1: polynomial::PolyDecoder,
 }
 
@@ -38,9 +40,11 @@ pub struct Ct1Received {
 }
 
 #[cfg_attr(test, derive(Clone))]
+#[hax_lib::attributes]
 pub struct EkSentCt1Received {
     uc: unchunked::EkSentCt1Received,
     // `receiving_ct2` only decodes messages of length `incremental_mlkem768::CIPHERTEXT2_SIZE + authenticator::Authenticator::MACSIZE`
+    #[hax_lib::refine(receiving_ct2.pts_needed == (incremental_mlkem768::CIPHERTEXT2_SIZE + authenticator::Authenticator::MACSIZE) / 2)]
     receiving_ct2: polynomial::PolyDecoder,
 }
 
@@ -52,10 +56,9 @@ impl KeysUnsampled {
     }
 
     pub fn send_hdr_chunk<R: Rng + CryptoRng>(self, rng: &mut R) -> (KeysSampled, Chunk) {
-        let (uc, hdr, mac) = self.uc.send_header(rng);
-        let to_send = [hdr, mac].concat();
+        let (uc, mut to_send, mut mac) = self.uc.send_header(rng);
+        to_send.append(&mut mac);
         let encoder = polynomial::PolyEncoder::encode_bytes(&to_send);
-        hax_lib::assume!(encoder.is_ok());
         let mut sending_hdr = encoder.expect("should be able to encode header size");
         let chunk = sending_hdr.next_chunk();
         (KeysSampled { uc, sending_hdr }, chunk)
@@ -81,13 +84,10 @@ impl KeysSampled {
     pub fn recv_ct1_chunk(self, epoch: Epoch, chunk: &Chunk) -> HeaderSent {
         assert_eq!(epoch, self.uc.epoch);
         let decoder = polynomial::PolyDecoder::new(incremental_mlkem768::CIPHERTEXT1_SIZE);
-        hax_lib::assume!(decoder.is_ok());
         let mut receiving_ct1 = decoder.expect("should be able to decode header size");
         receiving_ct1.add_chunk(chunk);
         let (uc, ek) = self.uc.send_ek();
-
         let encoder = polynomial::PolyEncoder::encode_bytes(&ek);
-        hax_lib::assume!(encoder.is_ok());
         let sending_ek = encoder.expect("should be able to send ek");
         HeaderSent {
             uc,
@@ -135,11 +135,7 @@ impl HeaderSent {
             mut receiving_ct1,
         } = self;
         receiving_ct1.add_chunk(chunk);
-        hax_lib::assume!(
-            receiving_ct1.get_pts_needed() <= polynomial::MAX_STORED_POLYNOMIAL_DEGREE_V1
-        );
         if let Some(decoded) = receiving_ct1.decoded_message() {
-            hax_lib::assume!(decoded.len() == 960);
             let uc = uc.recv_ct1(epoch, decoded);
             HeaderSentRecvChunk::Done(Ct1Received { uc, sending_ek })
         } else {
@@ -167,10 +163,13 @@ impl Ct1Received {
     #[hax_lib::requires(epoch == self.uc.epoch)]
     pub fn recv_ct2_chunk(self, epoch: Epoch, chunk: &Chunk) -> EkSentCt1Received {
         assert_eq!(epoch, self.uc.epoch);
+        hax_lib::assert!(
+            (incremental_mlkem768::CIPHERTEXT2_SIZE + authenticator::Authenticator::MACSIZE) % 2
+                == 0
+        );
         let decoder = polynomial::PolyDecoder::new(
             incremental_mlkem768::CIPHERTEXT2_SIZE + authenticator::Authenticator::MACSIZE,
         );
-        hax_lib::assume!(decoder.is_ok());
         let mut receiving_ct2 = decoder.expect("should be able to decode ct2+mac size");
         receiving_ct2.add_chunk(chunk);
         EkSentCt1Received {
@@ -203,22 +202,12 @@ impl EkSentCt1Received {
             mut receiving_ct2,
         } = self;
         receiving_ct2.add_chunk(chunk);
-        hax_lib::assume!(
-            receiving_ct2.get_pts_needed() <= polynomial::MAX_STORED_POLYNOMIAL_DEGREE_V1
-        );
         if let Some(mut ct2) = receiving_ct2.decoded_message() {
-            let mac: authenticator::Mac = ct2
-                .drain(incremental_mlkem768::CIPHERTEXT2_SIZE..)
-                .collect();
-            hax_lib::assume!(
-                ct2.len() == incremental_mlkem768::CIPHERTEXT2_SIZE
-                    && mac.len() == authenticator::Authenticator::MACSIZE
-            );
+            let mac: authenticator::Mac = ct2.split_off(incremental_mlkem768::CIPHERTEXT2_SIZE);
             let (uc, sec) = uc.recv_ct2(ct2, mac)?;
             let decoder = polynomial::PolyDecoder::new(
                 incremental_mlkem768::HEADER_SIZE + authenticator::Authenticator::MACSIZE,
             );
-            hax_lib::assume!(decoder.is_ok());
             Ok(EkSentCt1ReceivedRecvChunk::Done((
                 send_ct::NoHeaderReceived {
                     uc,

src/v1/chunked/send_ek/serialize.rs

@@ -22,19 +22,6 @@ impl KeysUnsampled {
 
 impl KeysSampled {
     pub fn into_pb(self) -> pqrpb::v1_state::chunked::KeysSampled {
-        hax_lib::assume!(match self.sending_hdr.get_encoder_state() {
-            polynomial::EncoderState::Points(points) => hax_lib::prop::forall(
-                |pts: &Vec<crate::encoding::gf::GF16>| hax_lib::prop::implies(
-                    points.contains(pts),
-                    pts.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )
-            ),
-            polynomial::EncoderState::Polys(polys) =>
-                hax_lib::prop::forall(|poly: &polynomial::Poly| hax_lib::prop::implies(
-                    polys.contains(poly),
-                    poly.coefficients.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )),
-        });
         pqrpb::v1_state::chunked::KeysSampled {
             uc: Some(self.uc.into_pb()),
             sending_hdr: Some(self.sending_hdr.into_pb()),
@@ -52,21 +39,9 @@ impl KeysSampled {
     }
 }
 
+#[hax_lib::attributes]
 impl HeaderSent {
     pub fn into_pb(self) -> pqrpb::v1_state::chunked::HeaderSent {
-        hax_lib::assume!(match self.sending_ek.get_encoder_state() {
-            polynomial::EncoderState::Points(points) => hax_lib::prop::forall(
-                |pts: &Vec<crate::encoding::gf::GF16>| hax_lib::prop::implies(
-                    points.contains(pts),
-                    pts.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )
-            ),
-            polynomial::EncoderState::Polys(polys) =>
-                hax_lib::prop::forall(|poly: &polynomial::Poly| hax_lib::prop::implies(
-                    polys.contains(poly),
-                    poly.coefficients.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )),
-        });
         pqrpb::v1_state::chunked::HeaderSent {
             uc: Some(self.uc.into_pb()),
             sending_ek: Some(self.sending_ek.into_pb()),
@@ -75,6 +50,11 @@ impl HeaderSent {
     }
 
     pub fn from_pb(pb: pqrpb::v1_state::chunked::HeaderSent) -> Result<Self, Error> {
+        if let Some(d) = &pb.receiving_ct1 {
+            if d.pts_needed as usize != crate::incremental_mlkem768::CIPHERTEXT1_SIZE / 2 {
+                return Err(Error::MsgDecode);
+            }
+        }
         Ok(Self {
             uc: unchunked::send_ek::EkSent::from_pb(pb.uc.ok_or(Error::StateDecode)?)?,
             sending_ek: polynomial::PolyEncoder::from_pb(pb.sending_ek.ok_or(Error::StateDecode)?)
@@ -89,19 +69,6 @@ impl HeaderSent {
 
 impl Ct1Received {
     pub fn into_pb(self) -> pqrpb::v1_state::chunked::Ct1Received {
-        hax_lib::assume!(match self.sending_ek.get_encoder_state() {
-            polynomial::EncoderState::Points(points) => hax_lib::prop::forall(
-                |pts: &Vec<crate::encoding::gf::GF16>| hax_lib::prop::implies(
-                    points.contains(pts),
-                    pts.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )
-            ),
-            polynomial::EncoderState::Polys(polys) =>
-                hax_lib::prop::forall(|poly: &polynomial::Poly| hax_lib::prop::implies(
-                    polys.contains(poly),
-                    poly.coefficients.len() <= polynomial::MAX_INTERMEDIATE_POLYNOMIAL_DEGREE_V1
-                )),
-        });
         pqrpb::v1_state::chunked::Ct1Received {
             uc: Some(self.uc.into_pb()),
             sending_ek: Some(self.sending_ek.into_pb()),
@@ -126,6 +93,14 @@ impl EkSentCt1Received {
     }
 
     pub fn from_pb(pb: pqrpb::v1_state::chunked::EkSentCt1Received) -> Result<Self, Error> {
+        if let Some(d) = &pb.receiving_ct2 {
+            if d.pts_needed as usize
+                != (incremental_mlkem768::CIPHERTEXT2_SIZE + authenticator::Authenticator::MACSIZE)
+                    / 2
+            {
+                return Err(Error::MsgDecode);
+            }
+        }
         Ok(Self {
             uc: unchunked::send_ek::EkSentCt1Received::from_pb(pb.uc.ok_or(Error::StateDecode)?)?,
             receiving_ct2: polynomial::PolyDecoder::from_pb(

src/v1/unchunked/send_ct.rs

@@ -116,6 +116,7 @@ impl NoHeaderReceived {
 #[hax_lib::attributes]
 impl HeaderReceived {
     #[hax_lib::requires(self.hdr.len() == 64)]
+    #[hax_lib::ensures(|(_, ct1, _)| ct1.len() == 960)]
     pub fn send_ct1<R: Rng + CryptoRng>(
         self,
         rng: &mut R,

src/v1/unchunked/send_ek.rs

@@ -71,6 +71,7 @@ pub struct EkSentCt1Received {
     ct1: incremental_mlkem768::Ciphertext1,
 }
 
+#[hax_lib::attributes]
 impl KeysUnsampled {
     pub fn new(auth_key: &[u8]) -> Self {
         Self {
@@ -79,6 +80,7 @@ impl KeysUnsampled {
         }
     }
 
+    #[hax_lib::ensures(|(_, hdr, mac)| hdr.len() == incremental_mlkem768::HEADER_SIZE && mac.len() == authenticator::Authenticator::MACSIZE)]
     pub fn send_header<R: Rng + CryptoRng>(
         self,
         rng: &mut R,
@@ -98,7 +100,9 @@ impl KeysUnsampled {
     }
 }
 
+#[hax_lib::attributes]
 impl HeaderSent {
+    #[hax_lib::ensures(|(_, ek)| ek.len() == 1152)]
     pub fn send_ek(self) -> (EkSent, incremental_mlkem768::EncapsulationKey) {
         (
             EkSent {
@@ -131,7 +135,7 @@ impl EkSent {
 
 #[hax_lib::attributes]
 impl EkSentCt1Received {
-    #[hax_lib::requires(ct2.len() == 128 && mac.len() == authenticator::Authenticator::MACSIZE)]
+    #[hax_lib::requires(ct2.len() == incremental_mlkem768::CIPHERTEXT2_SIZE && mac.len() == authenticator::Authenticator::MACSIZE)]
     pub fn recv_ct2(
         self,
         ct2: incremental_mlkem768::Ciphertext2,