diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
index 0ce89b4..0213011 100644
--- a/.github/workflows/hax.yml
+++ b/.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
 
diff --git a/Cargo.lock b/Cargo.lock
index dbf8c4f..0465b61 100644
--- a/Cargo.lock
+++ b/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",
diff --git a/Cargo.toml b/Cargo.toml
index a7d4447..ce84d7b 100644
--- a/Cargo.toml
+++ b/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"
diff --git a/proofs/fstar/extraction/Makefile b/proofs/fstar/extraction/Makefile
index 9b0bfab..5cafb58 100644
--- a/proofs/fstar/extraction/Makefile
+++ b/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
diff --git a/proofs/fstar/models/BitVecEq.fsti b/proofs/fstar/models/BitVecEq.fsti
index 6792f2b..fe3eb8f 100644
--- a/proofs/fstar/models/BitVecEq.fsti
+++ b/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
diff --git a/proofs/fstar/models/Bytes.Buf.Buf_impl.fsti b/proofs/fstar/models/Bytes.Buf.Buf_impl.fsti
index b7b63cf..7fc82b3 100644
--- a/proofs/fstar/models/Bytes.Buf.Buf_impl.fsti
+++ b/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))
diff --git a/proofs/fstar/models/Bytes.Buf.Buf_mut.fsti b/proofs/fstar/models/Bytes.Buf.Buf_mut.fsti
index ad058b2..d34341b 100644
--- a/proofs/fstar/models/Bytes.Buf.Buf_mut.fsti
+++ b/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
 
 
diff --git a/proofs/fstar/models/Libcrux_hmac.fsti b/proofs/fstar/models/Libcrux_hmac.fsti
index 360154c..00c22a2 100644
--- a/proofs/fstar/models/Libcrux_hmac.fsti
+++ b/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
 }
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Constants.fst b/proofs/fstar/models/Libcrux_ml_kem.Constants.fst
index 7c5e8e9..190f02c 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Constants.fst
+++ b/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
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Hash_functions.Portable.fsti b/proofs/fstar/models/Libcrux_ml_kem.Hash_functions.Portable.fsti
index d495f00..f1206c6 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Hash_functions.Portable.fsti
+++ b/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.
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Hash_functions.fsti b/proofs/fstar/models/Libcrux_ml_kem.Hash_functions.fsti
index c3d7278..65f725a 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Hash_functions.fsti
+++ b/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.
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Ind_cca.Incremental.Types.fsti b/proofs/fstar/models/Libcrux_ml_kem.Ind_cca.Incremental.Types.fsti
index 8c244e5..5e0385e 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Ind_cca.Incremental.Types.fsti
+++ b/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)
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Ind_cca.Unpacked.fsti b/proofs/fstar/models/Libcrux_ml_kem.Ind_cca.Unpacked.fsti
index 3c7c1ee..a42326a 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Ind_cca.Unpacked.fsti
+++ b/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
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Ind_cpa.Unpacked.fsti b/proofs/fstar/models/Libcrux_ml_kem.Ind_cpa.Unpacked.fsti
index 6fb0726..76f756f 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Ind_cpa.Unpacked.fsti
+++ b/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)
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Mlkem768.Incremental.fsti b/proofs/fstar/models/Libcrux_ml_kem.Mlkem768.Incremental.fsti
index 65121da..e0a988e 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Mlkem768.Incremental.fsti
+++ b/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.
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Mlkem768.fsti b/proofs/fstar/models/Libcrux_ml_kem.Mlkem768.fsti
index 9b40612..c912e27 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Mlkem768.fsti
+++ b/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
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Polynomial.fsti b/proofs/fstar/models/Libcrux_ml_kem.Polynomial.fsti
index 9d96686..437906f 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Polynomial.fsti
+++ b/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)
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Serialize.fsti b/proofs/fstar/models/Libcrux_ml_kem.Serialize.fsti
index 0afb383..167a462 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Serialize.fsti
+++ b/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
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Types.fst b/proofs/fstar/models/Libcrux_ml_kem.Types.fst
index e8d7d87..d4b08f9 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Types.fst
+++ b/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
   <:
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Variant.fsti b/proofs/fstar/models/Libcrux_ml_kem.Variant.fsti
index cd3d4d2..1d34b3f 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Variant.fsti
+++ b/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 ->
diff --git a/proofs/fstar/models/Libcrux_ml_kem.Vector.Traits.fsti b/proofs/fstar/models/Libcrux_ml_kem.Vector.Traits.fsti
index 456bbf1..9d20fd1 100644
--- a/proofs/fstar/models/Libcrux_ml_kem.Vector.Traits.fsti
+++ b/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:
diff --git a/proofs/fstar/models/MkSeq.fst b/proofs/fstar/models/MkSeq.fst
index 89c8e02..b2ccec5 100644
--- a/proofs/fstar/models/MkSeq.fst
+++ b/proofs/fstar/models/MkSeq.fst
@@ -1,5 +1,5 @@
 module MkSeq
-open Core
+open Core_models
 
 open FStar.Tactics.V2
 
diff --git a/proofs/fstar/models/Num_enum.fsti b/proofs/fstar/models/Num_enum.fsti
index fb51014..856089c 100644
--- a/proofs/fstar/models/Num_enum.fsti
+++ b/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)
diff --git a/proofs/fstar/models/Prost.Encoding.Wire_type.fsti b/proofs/fstar/models/Prost.Encoding.Wire_type.fsti
index 5fc5a40..ce71b6e 100644
--- a/proofs/fstar/models/Prost.Encoding.Wire_type.fsti
+++ b/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 =
diff --git a/proofs/fstar/models/Prost.Encoding.fsti b/proofs/fstar/models/Prost.Encoding.fsti
index fa534a8..f23c2f4 100644
--- a/proofs/fstar/models/Prost.Encoding.fsti
+++ b/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 }
diff --git a/proofs/fstar/models/Prost.Error.fsti b/proofs/fstar/models/Prost.Error.fsti
index 8415161..367b24c 100644
--- a/proofs/fstar/models/Prost.Error.fsti
+++ b/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
diff --git a/proofs/fstar/models/Prost.Message.fsti b/proofs/fstar/models/Prost.Message.fsti
index adac437..2e8c8fa 100644
--- a/proofs/fstar/models/Prost.Message.fsti
+++ b/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;
diff --git a/proofs/fstar/models/Rand.Rng.fsti b/proofs/fstar/models/Rand.Rng.fsti
index 72b92e5..eaf02ea 100644
--- a/proofs/fstar/models/Rand.Rng.fsti
+++ b/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) = {
diff --git a/proofs/fstar/models/Sorted_vec.fsti b/proofs/fstar/models/Sorted_vec.fsti
index e689452..d19f9bf 100644
--- a/proofs/fstar/models/Sorted_vec.fsti
+++ b/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
   } *)
diff --git a/proofs/fstar/models/Spec.GF16.fst b/proofs/fstar/models/Spec.GF16.fst
index 8bd583f..2f4055f 100644
--- a/proofs/fstar/models/Spec.GF16.fst
+++ b/proofs/fstar/models/Spec.GF16.fst
@@ -1,5 +1,5 @@
 module Spec.GF16
-open Core
+open Core_models
 
 (** Boolean Operations **)
 
diff --git a/proofs/fstar/models/Spec.MLKEM.Instances.fst b/proofs/fstar/models/Spec.MLKEM.Instances.fst
index 8a4168d..a952dad 100644
--- a/proofs/fstar/models/Spec.MLKEM.Instances.fst
+++ b/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
diff --git a/proofs/fstar/models/Spec.MLKEM.Math.fst b/proofs/fstar/models/Spec.MLKEM.Math.fst
index 9a4aff2..c3f224c 100644
--- a/proofs/fstar/models/Spec.MLKEM.Math.fst
+++ b/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
diff --git a/proofs/fstar/models/Spec.MLKEM.fst b/proofs/fstar/models/Spec.MLKEM.fst
index 8d4ed7f..38efa21 100644
--- a/proofs/fstar/models/Spec.MLKEM.fst
+++ b/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
diff --git a/proofs/fstar/models/Spec.Utils.fsti b/proofs/fstar/models/Spec.Utils.fsti
index a6a5f38..fcef039 100644
--- a/proofs/fstar/models/Spec.Utils.fsti
+++ b/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))
diff --git a/src/chain.rs b/src/chain.rs
index d9693fc..9f3f368 100644
--- a/src/chain.rs
+++ b/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())
diff --git a/src/encoding/gf.rs b/src/encoding/gf.rs
index 31e349d..3d78854 100644
--- a/src/encoding/gf.rs
+++ b/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
diff --git a/src/encoding/polynomial.rs b/src/encoding/polynomial.rs
index 7db0d35..03315cd 100644
--- a/src/encoding/polynomial.rs
+++ b/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 {
diff --git a/src/incremental_mlkem768.rs b/src/incremental_mlkem768.rs
index 2d7ad9b..bbdb7af 100644
--- a/src/incremental_mlkem768.rs
+++ b/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);
diff --git a/src/v1/chunked/send_ct.rs b/src/v1/chunked/send_ct.rs
index a67a43a..66f0040 100644
--- a/src/v1/chunked/send_ct.rs
+++ b/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 {
diff --git a/src/v1/chunked/send_ct/serialize.rs b/src/v1/chunked/send_ct/serialize.rs
index 45f2229..1da63b4 100644
--- a/src/v1/chunked/send_ct/serialize.rs
+++ b/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()),
diff --git a/src/v1/chunked/send_ek.rs b/src/v1/chunked/send_ek.rs
index 10e5694..742c9d3 100644
--- a/src/v1/chunked/send_ek.rs
+++ b/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,
diff --git a/src/v1/chunked/send_ek/serialize.rs b/src/v1/chunked/send_ek/serialize.rs
index af2734f..5e8f9dd 100644
--- a/src/v1/chunked/send_ek/serialize.rs
+++ b/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(
diff --git a/src/v1/unchunked/send_ct.rs b/src/v1/unchunked/send_ct.rs
index 470b18d..a568ef0 100644
--- a/src/v1/unchunked/send_ct.rs
+++ b/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,
diff --git a/src/v1/unchunked/send_ek.rs b/src/v1/unchunked/send_ek.rs
index fa9b4a8..cb3d9aa 100644
--- a/src/v1/unchunked/send_ek.rs
+++ b/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,