diff --git a/Cargo.lock b/Cargo.lock
index 1f9f0f6d1..0da78d60b 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -702,7 +702,7 @@ dependencies = [
 [[package]]
 name = "hax-lib"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax?branch=main#6d493af879767475a269327513208d4a491c6179"
+source = "git+https://github.com/hacspec/hax?branch=main#c707da15965f76d0ee3792a96e73a46394c5e01a"
 dependencies = [
  "hax-lib-macros",
  "num-bigint",
@@ -712,7 +712,7 @@ dependencies = [
 [[package]]
 name = "hax-lib-macros"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax?branch=main#6d493af879767475a269327513208d4a491c6179"
+source = "git+https://github.com/hacspec/hax?branch=main#c707da15965f76d0ee3792a96e73a46394c5e01a"
 dependencies = [
  "hax-lib-macros-types",
  "paste",
@@ -725,7 +725,7 @@ dependencies = [
 [[package]]
 name = "hax-lib-macros-types"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax?branch=main#6d493af879767475a269327513208d4a491c6179"
+source = "git+https://github.com/hacspec/hax?branch=main#c707da15965f76d0ee3792a96e73a46394c5e01a"
 dependencies = [
  "proc-macro2",
  "quote",
diff --git a/fstar-helpers/Makefile.base b/fstar-helpers/Makefile.base
index e7c57847f..b4e0d962b 100644
--- a/fstar-helpers/Makefile.base
+++ b/fstar-helpers/Makefile.base
@@ -1,5 +1,14 @@
 # Base Makefile for F* in libcrux.
 # This inherits from Makefile.generic, and adds the `specs` folder from HACL and the `libcrux-ml-kem/proofs/fstar/spec` folder. 
 
-FSTAR_INCLUDE_DIRS_EXTRA = $(HACL_HOME)/specs $(shell git rev-parse --show-toplevel)/libcrux-ml-kem/proofs/fstar/spec $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec
+VERIFY_SLOW_MODULES ?= no
+ifeq (${VERIFY_SLOW_MODULES},no)
+	ADMIT_MODULES += ${SLOW_MODULES}
+endif
+
+EXTRA_HELPMESSAGE += printf "Libcrux specifics:\n";
+EXTRA_HELPMESSAGE += target SLOW_MODULES 'a list of modules to verify fully only when `VERIFY_SLOW_MODULES` is set to `yes`. When `VERIFY_SLOW_MODULES`, those modules are admitted.';
+EXTRA_HELPMESSAGE += target VERIFY_SLOW_MODULES '`yes` or `no`, defaults to `no`';
+
+FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs $(shell git rev-parse --show-toplevel)/libcrux-ml-kem/proofs/fstar/spec $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic
diff --git a/fstar-helpers/Makefile.generic b/fstar-helpers/Makefile.generic
index d63f08b13..a7264458b 100644
--- a/fstar-helpers/Makefile.generic
+++ b/fstar-helpers/Makefile.generic
@@ -196,6 +196,7 @@ echo "Variables:"
 target "NO_COLOR" "Set to anything to disable colors"
 target "ADMIT_MODULES" "List of modules where F* will assume every SMT query"
 target "FSTAR_INCLUDE_DIRS_EXTRA" "List of extra include F* dirs"
+${EXTRA_HELPMESSAGE}
 endef
 export HELPMESSAGE
 
@@ -215,7 +216,6 @@ describe:
 	@printf ' - ${ANSI_COLOR_BLUE}HINT_DIR${ANSI_COLOR_RESET} = %s\n' '${HINT_DIR}'
 	@printf ' - ${ANSI_COLOR_BLUE}ADMIT_MODULE_FLAGS${ANSI_COLOR_RESET} = %s\n' '${ADMIT_MODULE_FLAGS}'
 	@printf ' - ${ANSI_COLOR_BLUE}FSTAR_INCLUDE_DIRS_EXTRA${ANSI_COLOR_RESET} = %s\n' '${FSTAR_INCLUDE_DIRS_EXTRA}'
-	@printf ' - ${ANSI_COLOR_BLUE}OTHERFLAGS${ANSI_COLOR_RESET} = %s\n' '${OTHERFLAGS}'
 
 help: ;@bash -c "$$HELPMESSAGE"
 h: ;@bash -c "$$HELPMESSAGE"
diff --git a/fstar-helpers/Makefile.template b/fstar-helpers/Makefile.template
deleted file mode 100644
index 9faae3841..000000000
--- a/fstar-helpers/Makefile.template
+++ /dev/null
@@ -1,255 +0,0 @@
-# This is a generically useful Makefile for F* that is self-contained
-#
-# We expect:
-#  1. `fstar.exe` to be in PATH (alternatively, you can also set
-#     $FSTAR_HOME to be set to your F* repo/install directory)
-#
-#  2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH.
-#
-#  3. the extracted Cargo crate to have "hax-lib" as a dependency:
-#     `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}`
-#
-# Optionally, you can set `HACL_HOME`.
-#
-# ROOTS contains all the top-level F* files you wish to verify
-# The default target `verify` verified ROOTS and its dependencies
-# To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line
-#
-# To make F* emacs mode use the settings in this file, you need to
-# add the following lines to your .emacs
-#
-# (setq-default fstar-executable "<YOUR_FSTAR_HOME>/bin/fstar.exe")
-# (setq-default fstar-smt-executable "<YOUR_Z3_HOME>/bin/z3")
-#
-# (defun my-fstar-compute-prover-args-using-make ()
-#   "Construct arguments to pass to F* by calling make."
-#   (with-demoted-errors "Error when constructing arg string: %S"
-#     (let* ((fname (file-name-nondirectory buffer-file-name))
-# 	   (target (concat fname "-in"))
-# 	   (argstr (car (process-lines "make" "--quiet" target))))
-#       (split-string argstr))))
-# (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
-#
-
-HACL_HOME      ?= $(HOME)/.hax/hacl_home
-# Expand variable FSTAR_BIN_DETECT now, so that we don't run this over and over
-
-FSTAR_BIN_DETECT := $(if $(shell command -v fstar.exe), fstar.exe, $(FSTAR_HOME)/bin/fstar.exe)
-FSTAR_BIN      ?= $(FSTAR_BIN_DETECT)
-
-GIT_ROOT_DIR   := $(shell git rev-parse --show-toplevel)/
-CACHE_DIR      ?= ${GIT_ROOT_DIR}.fstar-cache/checked
-HINT_DIR       ?= ${GIT_ROOT_DIR}.fstar-cache/hints
-
-# Makes command quiet by default
-Q ?= @
-
-# Verify the required executable are in PATH
-EXECUTABLES = cargo cargo-hax jq
-K := $(foreach exec,$(EXECUTABLES),\
-        $(if $(shell which $(exec)),some string,$(error "No $(exec) in PATH")))
-
-export ANSI_COLOR_BLUE=\033[34m
-export ANSI_COLOR_RED=\033[31m
-export ANSI_COLOR_BBLUE=\033[1;34m
-export ANSI_COLOR_GRAY=\033[90m
-export ANSI_COLOR_TONE=\033[35m
-export ANSI_COLOR_RESET=\033[0m
-
-ifdef NO_COLOR
-export ANSI_COLOR_BLUE=
-export ANSI_COLOR_RED=
-export ANSI_COLOR_BBLUE=
-export ANSI_COLOR_GRAY=
-export ANSI_COLOR_BOLD_BLUE=
-export ANSI_COLOR_TONE=
-export ANSI_COLOR_RESET=
-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") ; \
-        if [ $$? -eq 0 ]; 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 bash -c '${FINDLIBS}')
-FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HACL_HOME)/specs $(FSTAR_INCLUDE_DIRS_EXTRA) $(FINDLIBS_OUTPUT)
-
-# Make sure FSTAR_INCLUDE_DIRS has the `proof-libs`, print hints and
-# an error message otherwise
-ifneq (,$(findstring proof-libs/fstar,$(FSTAR_INCLUDE_DIRS)))
-else
-	K += $(info )
-	ERROR := $(shell printf '${ANSI_COLOR_RED}Error: could not detect `proof-libs`!${ANSI_COLOR_RESET}')
-	K += $(info ${ERROR})
-	ERROR := $(shell printf '  > Do you have `${ANSI_COLOR_BLUE}hax-lib${ANSI_COLOR_RESET}` in your `${ANSI_COLOR_BLUE}Cargo.toml${ANSI_COLOR_RESET}` as a ${ANSI_COLOR_BLUE}git${ANSI_COLOR_RESET} or ${ANSI_COLOR_BLUE}path${ANSI_COLOR_RESET} dependency?')
-	K += $(info ${ERROR})
-	ERROR := $(shell printf '  ${ANSI_COLOR_BLUE}> Tip: you may want to run `cargo add --git https://github.com/hacspec/hax hax-lib`${ANSI_COLOR_RESET}')
-	K += $(info ${ERROR})
-	K += $(info )
-	K += $(error Fatal error: `proof-libs` is required.)
-endif
-
-.PHONY: all verify clean
-
-all:
-	$(Q)rm -f .depend
-	$(Q)$(MAKE) .depend vscode verify
-
-all-keep-going:
-	$(Q)rm -f .depend
-	$(Q)$(MAKE) --keep-going .depend vscode verify
-
-# If $HACL_HOME doesn't exist, clone it
-${HACL_HOME}:
-	$(Q)mkdir -p "${HACL_HOME}"
-	$(info Clonning Hacl* in ${HACL_HOME}...)
-	git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}"
-	$(info Clonning Hacl* in ${HACL_HOME}... done!)
-
-# If no any F* file is detected, we run hax
-ifeq "$(wildcard *.fst *fsti)" ""
-$(shell cargo hax into fstar)
-endif
-
-# By default, we process all the files in the current directory
-ROOTS ?= $(wildcard *.fst *fsti)
-ADMIT_MODULES ?=
-
-# Can be useful for debugging purposes
-FINDLIBS.sh:
-	$(Q)echo '${FINDLIBS}' > FINDLIBS.sh
-include-dirs:
-	$(Q)bash -c '${FINDLIBS}'
-
-FSTAR_FLAGS = --query_stats \
-  --warn_error -321-331-241-274-239-271 \
-  --cache_checked_modules --cache_dir $(CACHE_DIR) \
-  --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \
-  $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
-
-FSTAR := $(FSTAR_BIN) $(FSTAR_FLAGS)
-
-.depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(HACL_HOME)
-	@$(FSTAR) --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@
-
-include .depend
-
-$(HINT_DIR) $(CACHE_DIR):
-	$(Q)mkdir -p $@
-
-define HELPMESSAGE
-echo "hax' default Makefile for F*"
-echo ""
-echo "The available targets are:"
-echo ""
-function target() {
-  printf '  ${ANSI_COLOR_BLUE}%-20b${ANSI_COLOR_RESET} %s\n' "$$1" "$$2"
-}
-target "all" "Verify every F* files (stops whenever an F* fails first)"
-target "all-keep-going" "Verify every F* files (tries as many F* module as possible)"
-target "" ""
-target "run:${ANSI_COLOR_TONE}<MyModule.fst>  " 'Runs F* on `MyModule.fst` only'
-target "" ""
-target "vscode" 'Generates a `hax.fst.config.json` file'
-target "${ANSI_COLOR_TONE}<MyModule.fst>${ANSI_COLOR_BLUE}-in   " 'Useful for Emacs, outputs the F* prefix command to be used'
-target "" ""
-target "clean" 'Cleanup the target'
-target "include-dirs" 'List the F* include directories'
-target "" ""
-target "roots" 'List the F* root modules.'
-echo ""
-echo "Environment variables:"
-target "NO_COLOR" "Set to anything to disable colors"
-endef
-export HELPMESSAGE
-
-roots:
-	@for root in ${ROOTS}; do \
-	  filename=$$(basename -- "$$root") ;\
-	  ext="$${filename##*.}" ;\
-	  noext="$${filename%.*}" ;\
-	  printf "${ANSI_COLOR_GRAY}$$(dirname -- "$$root")/${ANSI_COLOR_RESET}%s${ANSI_COLOR_GRAY}.${ANSI_COLOR_TONE}%s${ANSI_COLOR_RESET}\n" "$$noext" "$$ext"; \
-	done
-
-help: ;@bash -c "$$HELPMESSAGE"
-h: ;@bash -c "$$HELPMESSAGE"
-
-HEADER = $(Q)printf '${ANSI_COLOR_BBLUE}[CHECK] %s ${ANSI_COLOR_RESET}\n' "$(basename $(notdir $@))"
-
-run:%: | .depend $(HINT_DIR) $(CACHE_DIR) $(HACL_HOME)
-	${HEADER}
-	$(Q)$(FSTAR) $(OTHERFLAGS) $(@:run:%=%)
-
-
-VERIFIED_CHECKED = $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
-ADMIT_CHECKED = $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,${ADMIT_MODULES}))
-
-$(ADMIT_CHECKED):
-	$(Q)printf '${ANSI_COLOR_BBLUE}[${ANSI_COLOR_TONE}ADMIT${ANSI_COLOR_BBLUE}] %s ${ANSI_COLOR_RESET}\n' "$(basename $(notdir $@))"
-	$(Q)$(FSTAR) $(OTHERFLAGS) --admit_smt_queries true $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints || { \
-	  echo "" ; \
-	  exit 1 ; \
-	}
-	$(Q)printf "\n\n"
-
-$(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR) $(HACL_HOME)
-	${HEADER}
-	$(Q)$(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints || { \
-	  echo "" ; \
-	  exit 1 ; \
-	}
-	touch $@
-	$(Q)printf "\n\n"
-
-verify: $(VERIFIED_CHECKED) $(ADMIT_CHECKED)
-
-# Targets for interactive mode
-
-%.fst-in:
-	$(info $(FSTAR_FLAGS) \
-	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints)
-%.fsti-in:
-	$(info $(FSTAR_FLAGS) \
-	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints)
-
-# Targets for VSCode
-hax.fst.config.json:
-	$(Q)echo "$(FSTAR_INCLUDE_DIRS)" | jq --arg fstar "$(FSTAR_BIN)" -R 'split(" ") | {fstar_exe: $$fstar, includes: .}' > $@
-vscode: hax.fst.config.json
-
-SHELL=bash
-
-# Clean target
-clean:
-	rm -rf $(CACHE_DIR)/*
-	rm *.fst
-
diff --git a/fstar-helpers/fstar-bitvec/Makefile b/fstar-helpers/fstar-bitvec/Makefile
index 4bddb3c33..b4ce70a38 100644
--- a/fstar-helpers/fstar-bitvec/Makefile
+++ b/fstar-helpers/fstar-bitvec/Makefile
@@ -1,33 +1 @@
-ADMIT_MODULES = Libcrux_ml_kem.Ind_cca.Unpacked.fst \
-	      Libcrux_ml_kem.Ind_cca.fst \
-              Libcrux_ml_kem.Ind_cpa.fst \
-              Libcrux_ml_kem.Ind_cpa.fsti \
-              Libcrux_ml_kem.Invert_ntt.fst \
-              Libcrux_ml_kem.Matrix.fst \
-              Libcrux_ml_kem.Ntt.fst \
-              Libcrux_ml_kem.Polynomial.fst \
-              Libcrux_ml_kem.Sampling.fst \
-              Libcrux_ml_kem.Serialize.fst \
-	      Libcrux_ml_kem.Vector.Rej_sample_table.fsti \
-              Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst \
-              Libcrux_ml_kem.Vector.Avx2.Compress.fst \
-              Libcrux_ml_kem.Vector.Avx2.fst \
-              Libcrux_ml_kem.Vector.Avx2.Ntt.fst \
-              Libcrux_ml_kem.Vector.Avx2.Portable.fst \
-              Libcrux_ml_kem.Vector.Avx2.Sampling.fst \
-              Libcrux_ml_kem.Vector.Avx2.Serialize.fst \
-              Libcrux_ml_kem.Vector.Neon.Arithmetic.fst \
-              Libcrux_ml_kem.Vector.Neon.Compress.fst \
-              Libcrux_ml_kem.Vector.Neon.fst \
-              Libcrux_ml_kem.Vector.Neon.Ntt.fst \
-              Libcrux_ml_kem.Vector.Neon.Serialize.fst \
-              Libcrux_ml_kem.Vector.Neon.Vector_type.fst \
-              Libcrux_ml_kem.Vector.Portable.Arithmetic.fst \
-              Libcrux_ml_kem.Vector.Portable.Compress.fst \
-              Libcrux_ml_kem.Vector.Portable.Ntt.fst \
-              Libcrux_ml_kem.Vector.Portable.Sampling.fst \
-              Libcrux_ml_kem.Vector.Portable.Vector_type.fst \
-              Libcrux_ml_kem.Vector.Traits.fst
-
-OTHERFLAGS += --unsafe_tactic_exec
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.base
diff --git a/fstar-helpers/fstar-bitvec/RwLemmas.fst b/fstar-helpers/fstar-bitvec/RwLemmas.fst
new file mode 100644
index 000000000..1fc1e00de
--- /dev/null
+++ b/fstar-helpers/fstar-bitvec/RwLemmas.fst
@@ -0,0 +1,71 @@
+module RwLemmas
+
+open Core
+module L = FStar.List.Tot
+open FStar.Tactics.V2
+open FStar.Tactics.V2.SyntaxHelpers
+open FStar.Class.Printable
+open FStar.Mul
+open FStar.Option
+
+open Tactics.Utils
+open Tactics.Pow2
+
+open BitVecEq {}
+
+let norm_machine_int () = Tactics.MachineInts.(transform norm_machine_int_term)
+
+#push-options "--z3rlimit 40"
+let deserialize_10_int (bytes: t_Array u8 (sz 10)) =
+  let r0:i16 =
+    (((cast (bytes.[ sz 1 ] <: u8) <: i16) &. 3s <: i16) <<! 8l <: i16) |.
+    ((cast (bytes.[ sz 0 ] <: u8) <: i16) &. 255s <: i16)
+  in
+  let r1:i16 =
+    (((cast (bytes.[ sz 2 ] <: u8) <: i16) &. 15s <: i16) <<! 6l <: i16) |.
+    ((cast (bytes.[ sz 1 ] <: u8) <: i16) >>! 2l <: i16)
+  in
+  let r2:i16 =
+    (((cast (bytes.[ sz 3 ] <: u8) <: i16) &. 63s <: i16) <<! 4l <: i16) |.
+    ((cast (bytes.[ sz 2 ] <: u8) <: i16) >>! 4l <: i16)
+  in
+  let r3:i16 =
+    ((cast (bytes.[ sz 4 ] <: u8) <: i16) <<! 2l <: i16) |.
+    ((cast (bytes.[ sz 3 ] <: u8) <: i16) >>! 6l <: i16)
+  in
+  let r4:i16 =
+    (((cast (bytes.[ sz 6 ] <: u8) <: i16) &. 3s <: i16) <<! 8l <: i16) |.
+    ((cast (bytes.[ sz 5 ] <: u8) <: i16) &. 255s <: i16)
+  in
+  let r5:i16 =
+    (((cast (bytes.[ sz 7 ] <: u8) <: i16) &. 15s <: i16) <<! 6l <: i16) |.
+    ((cast (bytes.[ sz 6 ] <: u8) <: i16) >>! 2l <: i16)
+  in
+  let r6:i16 =
+    (((cast (bytes.[ sz 8 ] <: u8) <: i16) &. 63s <: i16) <<! 4l <: i16) |.
+    ((cast (bytes.[ sz 7 ] <: u8) <: i16) >>! 4l <: i16)
+  in
+  let r7:i16 =
+    ((cast (bytes.[ sz 9 ] <: u8) <: i16) <<! 2l <: i16) |.
+    ((cast (bytes.[ sz 8 ] <: u8) <: i16) >>! 6l <: i16)
+  in
+  let result:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
+    r0, r1, r2, r3, r4, r5, r6, r7 <: (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
+  in
+  result
+#pop-options
+
+let deserialize_10_int' (bytes: t_Array u8 (sz 10)): t_Array i16 (sz 8)
+    = MkSeq.create8 (deserialize_10_int bytes)
+  
+#push-options "--compat_pre_core 0"
+#push-options "--z3rlimit 80"
+let fff_ (bytes: t_Array u8 (sz 10)) x: unit = 
+    let bv1 = bit_vec_of_int_t_array bytes 8 in
+    let out = deserialize_10_int' bytes in
+    let bv2 = bit_vec_of_int_t_array out 10 in
+    assert (forall (i: nat { i < 80 }). bv1 i == bv2 i) by (
+      Tactics.GetBit.prove_bit_vector_equality ()
+    )
+#pop-options
+
diff --git a/fstar-helpers/fstar-bitvec/Tactics.GetBit.fst b/fstar-helpers/fstar-bitvec/Tactics.GetBit.fst
index a59c72fba..abec9b4fe 100644
--- a/fstar-helpers/fstar-bitvec/Tactics.GetBit.fst
+++ b/fstar-helpers/fstar-bitvec/Tactics.GetBit.fst
@@ -16,8 +16,6 @@ open BitVecEq
 open Tactics.Seq
 
 
-let _ = Rust_primitives.Hax.array_of_list
-
 let norm_machine_int () = Tactics.MachineInts.(transform norm_machine_int_term)
 
 /// Does one round of computation
@@ -29,6 +27,7 @@ let compute_one_round (): Tac _ =
             ; implode_qn (cur_module ())
             ; "MkSeq"
             ; `%Rust_primitives.Hax.array_of_list
+            ; `%Libcrux_ml_kem.Vector.Portable.Vector_type.__proj__Mkt_PortableVector__item__f_elements
           ]
         ; primops; unmeta];
    trace "compute_one_round: norm_pow2"        norm_pow2;
@@ -39,7 +38,7 @@ let compute_one_round (): Tac _ =
 let compute': unit -> Tac unit = goal_fixpoint compute_one_round
 
 /// Proves a goal of the shape `forall (i:nat{i < N}). get_bit ... i == get_bit ... i` (`N` is expected to be a literal)
-let prove_bit_vector_equality' (): Tac unit = 
+let prove_bit_vector_equality'' (): Tac unit =
   norm [
     iota;
     primops;
@@ -58,6 +57,10 @@ let prove_bit_vector_equality' (): Tac unit =
     print ("Ask SMT: " ^ term_to_string (cur_goal ()));
     focus smt_sync
   ))
+let prove_bit_vector_equality' (): Tac unit =
+  if lax_on ()
+  then iterAll tadmit
+  else prove_bit_vector_equality'' ()
 let prove_bit_vector_equality (): Tac unit = 
   set_rlimit 100;
   with_compat_pre_core 0 prove_bit_vector_equality'
diff --git a/fstar-helpers/proofs/fstar/extraction/Makefile b/fstar-helpers/proofs/fstar/extraction/Makefile
deleted file mode 100644
index ec420d509..000000000
--- a/fstar-helpers/proofs/fstar/extraction/Makefile
+++ /dev/null
@@ -1 +0,0 @@
-include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.template
diff --git a/libcrux-ml-kem/hax.py b/libcrux-ml-kem/hax.py
index b95b864ab..8df66c304 100755
--- a/libcrux-ml-kem/hax.py
+++ b/libcrux-ml-kem/hax.py
@@ -40,6 +40,8 @@ def __call__(self, parser, args, values, option_string=None) -> None:
             "-i",
             include_str,
             "fstar",
+            "--z3rlimit",
+            "80",
             "--interfaces",
             interface_include,
         ]
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst
index a037dd8e4..2576b5c73 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst
@@ -11,6 +11,8 @@ let _ =
   let open Libcrux_ml_kem.Vector.Traits in
   ()
 
+#push-options "--z3rlimit 150"
+
 let serialize_kem_secret_key
       (v_K v_SERIALIZED_KEY_LEN: usize)
       (#v_Hasher: Type0)
@@ -157,6 +159,8 @@ let serialize_kem_secret_key
   in
   out
 
+#pop-options
+
 let validate_public_key
       (v_K v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize)
       (#v_Vector: Type0)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Portable.fsti
new file mode 100644
index 000000000..fe64003c4
--- /dev/null
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Portable.fsti
@@ -0,0 +1,30 @@
+module Libcrux_ml_kem.Vector.Avx2.Portable
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+val deserialize_11_int (bytes: t_Slice u8)
+    : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
+
+val serialize_11_int (v: t_Slice i16)
+    : Prims.Pure (u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
+
+type t_PortableVector = { f_elements:t_Array i16 (sz 16) }
+
+val from_i16_array (array: t_Array i16 (sz 16))
+    : Prims.Pure t_PortableVector Prims.l_True (fun _ -> Prims.l_True)
+
+val serialize_11_ (v: t_PortableVector)
+    : Prims.Pure (t_Array u8 (sz 22)) Prims.l_True (fun _ -> Prims.l_True)
+
+val to_i16_array (v: t_PortableVector)
+    : Prims.Pure (t_Array i16 (sz 16)) Prims.l_True (fun _ -> Prims.l_True)
+
+val zero: Prims.unit -> Prims.Pure t_PortableVector Prims.l_True (fun _ -> Prims.l_True)
+
+val deserialize_11_ (bytes: t_Slice u8)
+    : Prims.Pure t_PortableVector Prims.l_True (fun _ -> Prims.l_True)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti
index 3d329030c..2aa6f7ab9 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti
@@ -385,31 +385,57 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector =
         }
         <:
         t_SIMD256Vector);
-    f_serialize_1_pre = (fun (vector: t_SIMD256Vector) -> true);
-    f_serialize_1_post = (fun (vector: t_SIMD256Vector) (out: t_Array u8 (sz 2)) -> true);
+    f_serialize_1_pre
+    =
+    (fun (vector: t_SIMD256Vector) -> Spec.MLKEM.serialize_pre 1 (impl.f_repr vector));
+    f_serialize_1_post
+    =
+    (fun (vector: t_SIMD256Vector) (out: t_Array u8 (sz 2)) ->
+        Spec.MLKEM.serialize_pre 1 (impl.f_repr vector) ==>
+        Spec.MLKEM.serialize_post 1 (impl.f_repr vector) out);
     f_serialize_1_
     =
     (fun (vector: t_SIMD256Vector) ->
+        let _:Prims.unit = admit () in
         Libcrux_ml_kem.Vector.Avx2.Serialize.serialize_1_ vector.f_elements);
-    f_deserialize_1_pre = (fun (bytes: t_Slice u8) -> true);
-    f_deserialize_1_post = (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) -> true);
+    f_deserialize_1_pre
+    =
+    (fun (bytes: t_Slice u8) -> (Core.Slice.impl__len #u8 bytes <: usize) =. sz 2);
+    f_deserialize_1_post
+    =
+    (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) ->
+        sz (Seq.length bytes) =. sz 2 ==> Spec.MLKEM.deserialize_post 1 bytes (impl.f_repr out));
     f_deserialize_1_
     =
     (fun (bytes: t_Slice u8) ->
+        let _:Prims.unit = admit () in
         { f_elements = Libcrux_ml_kem.Vector.Avx2.Serialize.deserialize_1_ bytes }
         <:
         t_SIMD256Vector);
-    f_serialize_4_pre = (fun (vector: t_SIMD256Vector) -> true);
-    f_serialize_4_post = (fun (vector: t_SIMD256Vector) (out: t_Array u8 (sz 8)) -> true);
+    f_serialize_4_pre
+    =
+    (fun (vector: t_SIMD256Vector) -> Spec.MLKEM.serialize_pre 4 (impl.f_repr vector));
+    f_serialize_4_post
+    =
+    (fun (vector: t_SIMD256Vector) (out: t_Array u8 (sz 8)) ->
+        Spec.MLKEM.serialize_pre 4 (impl.f_repr vector) ==>
+        Spec.MLKEM.serialize_post 4 (impl.f_repr vector) out);
     f_serialize_4_
     =
     (fun (vector: t_SIMD256Vector) ->
+        let _:Prims.unit = admit () in
         Libcrux_ml_kem.Vector.Avx2.Serialize.serialize_4_ vector.f_elements);
-    f_deserialize_4_pre = (fun (bytes: t_Slice u8) -> true);
-    f_deserialize_4_post = (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) -> true);
+    f_deserialize_4_pre
+    =
+    (fun (bytes: t_Slice u8) -> (Core.Slice.impl__len #u8 bytes <: usize) =. sz 8);
+    f_deserialize_4_post
+    =
+    (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) ->
+        sz (Seq.length bytes) =. sz 8 ==> Spec.MLKEM.deserialize_post 4 bytes (impl.f_repr out));
     f_deserialize_4_
     =
     (fun (bytes: t_Slice u8) ->
+        let _:Prims.unit = admit () in
         { f_elements = Libcrux_ml_kem.Vector.Avx2.Serialize.deserialize_4_ bytes }
         <:
         t_SIMD256Vector);
@@ -419,7 +445,9 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector =
     =
     (fun (vector: t_SIMD256Vector) ->
         Libcrux_ml_kem.Vector.Avx2.Serialize.serialize_5_ vector.f_elements);
-    f_deserialize_5_pre = (fun (bytes: t_Slice u8) -> true);
+    f_deserialize_5_pre
+    =
+    (fun (bytes: t_Slice u8) -> (Core.Slice.impl__len #u8 bytes <: usize) =. sz 10);
     f_deserialize_5_post = (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) -> true);
     f_deserialize_5_
     =
@@ -427,17 +455,30 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector =
         { f_elements = Libcrux_ml_kem.Vector.Avx2.Serialize.deserialize_5_ bytes }
         <:
         t_SIMD256Vector);
-    f_serialize_10_pre = (fun (vector: t_SIMD256Vector) -> true);
-    f_serialize_10_post = (fun (vector: t_SIMD256Vector) (out: t_Array u8 (sz 20)) -> true);
+    f_serialize_10_pre
+    =
+    (fun (vector: t_SIMD256Vector) -> Spec.MLKEM.serialize_pre 10 (impl.f_repr vector));
+    f_serialize_10_post
+    =
+    (fun (vector: t_SIMD256Vector) (out: t_Array u8 (sz 20)) ->
+        Spec.MLKEM.serialize_pre 10 (impl.f_repr vector) ==>
+        Spec.MLKEM.serialize_post 10 (impl.f_repr vector) out);
     f_serialize_10_
     =
     (fun (vector: t_SIMD256Vector) ->
+        let _:Prims.unit = admit () in
         Libcrux_ml_kem.Vector.Avx2.Serialize.serialize_10_ vector.f_elements);
-    f_deserialize_10_pre = (fun (bytes: t_Slice u8) -> true);
-    f_deserialize_10_post = (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) -> true);
+    f_deserialize_10_pre
+    =
+    (fun (bytes: t_Slice u8) -> (Core.Slice.impl__len #u8 bytes <: usize) =. sz 20);
+    f_deserialize_10_post
+    =
+    (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) ->
+        sz (Seq.length bytes) =. sz 20 ==> Spec.MLKEM.deserialize_post 10 bytes (impl.f_repr out));
     f_deserialize_10_
     =
     (fun (bytes: t_Slice u8) ->
+        let _:Prims.unit = admit () in
         { f_elements = Libcrux_ml_kem.Vector.Avx2.Serialize.deserialize_10_ bytes }
         <:
         t_SIMD256Vector);
@@ -447,7 +488,9 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector =
     =
     (fun (vector: t_SIMD256Vector) ->
         Libcrux_ml_kem.Vector.Avx2.Serialize.serialize_11_ vector.f_elements);
-    f_deserialize_11_pre = (fun (bytes: t_Slice u8) -> true);
+    f_deserialize_11_pre
+    =
+    (fun (bytes: t_Slice u8) -> (Core.Slice.impl__len #u8 bytes <: usize) =. sz 22);
     f_deserialize_11_post = (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) -> true);
     f_deserialize_11_
     =
@@ -455,17 +498,30 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector =
         { f_elements = Libcrux_ml_kem.Vector.Avx2.Serialize.deserialize_11_ bytes }
         <:
         t_SIMD256Vector);
-    f_serialize_12_pre = (fun (vector: t_SIMD256Vector) -> true);
-    f_serialize_12_post = (fun (vector: t_SIMD256Vector) (out: t_Array u8 (sz 24)) -> true);
+    f_serialize_12_pre
+    =
+    (fun (vector: t_SIMD256Vector) -> Spec.MLKEM.serialize_pre 12 (impl.f_repr vector));
+    f_serialize_12_post
+    =
+    (fun (vector: t_SIMD256Vector) (out: t_Array u8 (sz 24)) ->
+        Spec.MLKEM.serialize_pre 12 (impl.f_repr vector) ==>
+        Spec.MLKEM.serialize_post 12 (impl.f_repr vector) out);
     f_serialize_12_
     =
     (fun (vector: t_SIMD256Vector) ->
+        let _:Prims.unit = admit () in
         Libcrux_ml_kem.Vector.Avx2.Serialize.serialize_12_ vector.f_elements);
-    f_deserialize_12_pre = (fun (bytes: t_Slice u8) -> true);
-    f_deserialize_12_post = (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) -> true);
+    f_deserialize_12_pre
+    =
+    (fun (bytes: t_Slice u8) -> (Core.Slice.impl__len #u8 bytes <: usize) =. sz 24);
+    f_deserialize_12_post
+    =
+    (fun (bytes: t_Slice u8) (out: t_SIMD256Vector) ->
+        sz (Seq.length bytes) =. sz 24 ==> Spec.MLKEM.deserialize_post 12 bytes (impl.f_repr out));
     f_deserialize_12_
     =
     (fun (bytes: t_Slice u8) ->
+        let _:Prims.unit = admit () in
         { f_elements = Libcrux_ml_kem.Vector.Avx2.Serialize.deserialize_12_ bytes }
         <:
         t_SIMD256Vector);
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.Edited.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.Edited.fsti
new file mode 100644
index 000000000..4ed69770d
--- /dev/null
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.Edited.fsti
@@ -0,0 +1,100 @@
+module Libcrux_ml_kem.Vector.Portable.Serialize.Edited
+// #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+// open Core
+// open FStar.Mul
+
+// val deserialize_10_int (bytes: t_Slice u8)
+//     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
+
+// val deserialize_11_int (bytes: t_Slice u8)
+//     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
+
+// val deserialize_12_int (bytes: t_Slice u8)
+//     : Prims.Pure (i16 & i16) Prims.l_True (fun _ -> Prims.l_True)
+
+// val deserialize_4_int (bytes: t_Slice u8)
+//     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
+
+// val deserialize_5_int (bytes: t_Slice u8)
+//     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
+
+// val serialize_10_int (v: t_Slice i16)
+//     : Prims.Pure (u8 & u8 & u8 & u8 & u8)
+//       (requires (Core.Slice.impl__len #i16 v <: usize) =. sz 4)
+//       (ensures
+//         fun tuple ->
+//           let tuple:(u8 & u8 & u8 & u8 & u8) = tuple in
+//           BitVecEq.int_t_array_bitwise_eq' (v <: t_Array i16 (sz 4)) 10 (MkSeq.create5 tuple) 8)
+
+// val serialize_11_int (v: t_Slice i16)
+//     : Prims.Pure (u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8)
+//       (requires Seq.length v == 8 /\ (forall i. Rust_primitives.bounded (Seq.index v i) 11))
+//       (ensures
+//         fun tuple ->
+//           let tuple:(u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8) = tuple in
+//           BitVecEq.int_t_array_bitwise_eq' (v <: t_Array i16 (sz 8)) 11 (MkSeq.create11 tuple) 8)
+
+// val serialize_12_int (v: t_Slice i16)
+//     : Prims.Pure (u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
+
+// val serialize_4_int (v: t_Slice i16)
+//     : Prims.Pure (u8 & u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
+
+// val serialize_5_int (v: t_Slice i16)
+//     : Prims.Pure (u8 & u8 & u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
+
+// val serialize_1_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+//     : Prims.Pure (t_Array u8 (sz 2)) Prims.l_True (fun _ -> Prims.l_True)
+
+// val serialize_10_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+//     : Prims.Pure (t_Array u8 (sz 20)) Prims.l_True (fun _ -> Prims.l_True)
+
+// val serialize_11_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+//     : Prims.Pure (t_Array u8 (sz 22)) Prims.l_True (fun _ -> Prims.l_True)
+
+// val serialize_12_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+//     : Prims.Pure (t_Array u8 (sz 24)) Prims.l_True (fun _ -> Prims.l_True)
+
+// val serialize_4_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+//     : Prims.Pure (t_Array u8 (sz 8)) Prims.l_True (fun _ -> Prims.l_True)
+
+// val serialize_5_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+//     : Prims.Pure (t_Array u8 (sz 10)) Prims.l_True (fun _ -> Prims.l_True)
+
+// val deserialize_1_ (v: t_Slice u8)
+//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
+
+// val deserialize_10_ (bytes: t_Slice u8)
+//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
+
+// val deserialize_11_ (bytes: t_Slice u8)
+//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
+
+// val deserialize_12_ (bytes: t_Slice u8)
+//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
+
+// val deserialize_4_ (bytes: t_Slice u8)
+//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
+
+// val deserialize_5_ (bytes: t_Slice u8)
+//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+//       Prims.l_True
+//       (fun _ -> Prims.l_True)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst
index 9a88facf7..4f479ac21 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fst
@@ -244,55 +244,430 @@ let serialize_5_int (v: t_Slice i16) =
   in
   r0, r1, r2, r3, r4 <: (u8 & u8 & u8 & u8 & u8)
 
+let deserialize_1_ (v: t_Slice u8) =
+  let result0:i16 = cast ((v.[ sz 0 ] <: u8) &. 1uy <: u8) <: i16 in
+  let result1:i16 = cast (((v.[ sz 0 ] <: u8) >>! 1l <: u8) &. 1uy <: u8) <: i16 in
+  let result2:i16 = cast (((v.[ sz 0 ] <: u8) >>! 2l <: u8) &. 1uy <: u8) <: i16 in
+  let result3:i16 = cast (((v.[ sz 0 ] <: u8) >>! 3l <: u8) &. 1uy <: u8) <: i16 in
+  let result4:i16 = cast (((v.[ sz 0 ] <: u8) >>! 4l <: u8) &. 1uy <: u8) <: i16 in
+  let result5:i16 = cast (((v.[ sz 0 ] <: u8) >>! 5l <: u8) &. 1uy <: u8) <: i16 in
+  let result6:i16 = cast (((v.[ sz 0 ] <: u8) >>! 6l <: u8) &. 1uy <: u8) <: i16 in
+  let result7:i16 = cast (((v.[ sz 0 ] <: u8) >>! 7l <: u8) &. 1uy <: u8) <: i16 in
+  let result8:i16 = cast ((v.[ sz 1 ] <: u8) &. 1uy <: u8) <: i16 in
+  let result9:i16 = cast (((v.[ sz 1 ] <: u8) >>! 1l <: u8) &. 1uy <: u8) <: i16 in
+  let result10:i16 = cast (((v.[ sz 1 ] <: u8) >>! 2l <: u8) &. 1uy <: u8) <: i16 in
+  let result11:i16 = cast (((v.[ sz 1 ] <: u8) >>! 3l <: u8) &. 1uy <: u8) <: i16 in
+  let result12:i16 = cast (((v.[ sz 1 ] <: u8) >>! 4l <: u8) &. 1uy <: u8) <: i16 in
+  let result13:i16 = cast (((v.[ sz 1 ] <: u8) >>! 5l <: u8) &. 1uy <: u8) <: i16 in
+  let result14:i16 = cast (((v.[ sz 1 ] <: u8) >>! 6l <: u8) &. 1uy <: u8) <: i16 in
+  let result15:i16 = cast (((v.[ sz 1 ] <: u8) >>! 7l <: u8) &. 1uy <: u8) <: i16 in
+  {
+    Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+    =
+    let list =
+      [
+        result0; result1; result2; result3; result4; result5; result6; result7; result8; result9;
+        result10; result11; result12; result13; result14; result15
+      ]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16);
+    Rust_primitives.Hax.array_of_list 16 list
+  }
+  <:
+  Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+
+#push-options "--compat_pre_core 2 --z3rlimit 300 --z3refresh"
+
+let deserialize_1_bit_vec_lemma (v: t_Array u8 (sz 2))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 8 in
+     let outputs = bit_vec_of_int_t_array (deserialize_1_ v).f_elements 1 in
+     (forall (i: nat {i < 16}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+
+#push-options "--z3rlimit 300"
+
+let deserialize_1_lemma inputs =
+  deserialize_1_bit_vec_lemma inputs;
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (deserialize_1_ inputs).f_elements 1) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+#pop-options
+
+let deserialize_10_ (bytes: t_Slice u8) =
+  let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
+    deserialize_10_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 10 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v8_15_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
+    deserialize_10_int (bytes.[ { Core.Ops.Range.f_start = sz 10; Core.Ops.Range.f_end = sz 20 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  {
+    Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+    =
+    let list =
+      [
+        v0_7_._1; v0_7_._2; v0_7_._3; v0_7_._4; v0_7_._5; v0_7_._6; v0_7_._7; v0_7_._8; v8_15_._1;
+        v8_15_._2; v8_15_._3; v8_15_._4; v8_15_._5; v8_15_._6; v8_15_._7; v8_15_._8
+      ]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16);
+    Rust_primitives.Hax.array_of_list 16 list
+  }
+  <:
+  Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+
+#push-options "--compat_pre_core 2 --z3rlimit 300 --z3refresh"
+
+let deserialize_10_bit_vec_lemma (v: t_Array u8 (sz 20))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 8 in
+     let outputs = bit_vec_of_int_t_array (deserialize_10_ v).f_elements 10 in
+     (forall (i: nat {i < 160}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+
+#push-options "--z3rlimit 300"
+
+let deserialize_10_lemma inputs =
+  deserialize_10_bit_vec_lemma inputs;
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (deserialize_10_ inputs).f_elements 10) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+#pop-options
+
+let deserialize_11_ (bytes: t_Slice u8) =
+  let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
+    deserialize_11_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 11 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v8_15_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
+    deserialize_11_int (bytes.[ { Core.Ops.Range.f_start = sz 11; Core.Ops.Range.f_end = sz 22 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  {
+    Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+    =
+    let list =
+      [
+        v0_7_._1; v0_7_._2; v0_7_._3; v0_7_._4; v0_7_._5; v0_7_._6; v0_7_._7; v0_7_._8; v8_15_._1;
+        v8_15_._2; v8_15_._3; v8_15_._4; v8_15_._5; v8_15_._6; v8_15_._7; v8_15_._8
+      ]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16);
+    Rust_primitives.Hax.array_of_list 16 list
+  }
+  <:
+  Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+
+let deserialize_12_ (bytes: t_Slice u8) =
+  let v0_1_:(i16 & i16) =
+    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 3 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v2_3_:(i16 & i16) =
+    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 3; Core.Ops.Range.f_end = sz 6 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v4_5_:(i16 & i16) =
+    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 6; Core.Ops.Range.f_end = sz 9 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v6_7_:(i16 & i16) =
+    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 9; Core.Ops.Range.f_end = sz 12 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v8_9_:(i16 & i16) =
+    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 12; Core.Ops.Range.f_end = sz 15 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v10_11_:(i16 & i16) =
+    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 15; Core.Ops.Range.f_end = sz 18 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v12_13_:(i16 & i16) =
+    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 18; Core.Ops.Range.f_end = sz 21 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v14_15_:(i16 & i16) =
+    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 21; Core.Ops.Range.f_end = sz 24 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  {
+    Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+    =
+    let list =
+      [
+        v0_1_._1; v0_1_._2; v2_3_._1; v2_3_._2; v4_5_._1; v4_5_._2; v6_7_._1; v6_7_._2; v8_9_._1;
+        v8_9_._2; v10_11_._1; v10_11_._2; v12_13_._1; v12_13_._2; v14_15_._1; v14_15_._2
+      ]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16);
+    Rust_primitives.Hax.array_of_list 16 list
+  }
+  <:
+  Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+
+#push-options "--compat_pre_core 2 --z3rlimit 300 --z3refresh"
+
+let deserialize_12_bit_vec_lemma (v: t_Array u8 (sz 24))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 8 in
+     let outputs = bit_vec_of_int_t_array (deserialize_12_ v).f_elements 12 in
+     (forall (i: nat {i < 192}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+
+#push-options "--z3rlimit 300"
+
+let deserialize_12_lemma inputs =
+  deserialize_12_bit_vec_lemma inputs;
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (deserialize_12_ inputs).f_elements 12) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+#pop-options
+
+let deserialize_4_ (bytes: t_Slice u8) =
+  let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
+    deserialize_4_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 4 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v8_15_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
+    deserialize_4_int (bytes.[ { Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 8 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  {
+    Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+    =
+    let list =
+      [
+        v0_7_._1; v0_7_._2; v0_7_._3; v0_7_._4; v0_7_._5; v0_7_._6; v0_7_._7; v0_7_._8; v8_15_._1;
+        v8_15_._2; v8_15_._3; v8_15_._4; v8_15_._5; v8_15_._6; v8_15_._7; v8_15_._8
+      ]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16);
+    Rust_primitives.Hax.array_of_list 16 list
+  }
+  <:
+  Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+
+#push-options "--compat_pre_core 2 --z3rlimit 300 --z3refresh"
+
+let deserialize_4_bit_vec_lemma (v: t_Array u8 (sz 8))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 8 in
+     let outputs = bit_vec_of_int_t_array (deserialize_4_ v).f_elements 4 in
+     (forall (i: nat {i < 64}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+
+#push-options "--z3rlimit 300"
+
+let deserialize_4_lemma inputs =
+  deserialize_4_bit_vec_lemma inputs;
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (deserialize_4_ inputs).f_elements 4) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+#pop-options
+
+let deserialize_5_ (bytes: t_Slice u8) =
+  let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
+    deserialize_5_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 5 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  let v8_15_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
+    deserialize_5_int (bytes.[ { Core.Ops.Range.f_start = sz 5; Core.Ops.Range.f_end = sz 10 }
+          <:
+          Core.Ops.Range.t_Range usize ]
+        <:
+        t_Slice u8)
+  in
+  {
+    Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+    =
+    let list =
+      [
+        v0_7_._1; v0_7_._2; v0_7_._3; v0_7_._4; v0_7_._5; v0_7_._6; v0_7_._7; v0_7_._8; v8_15_._1;
+        v8_15_._2; v8_15_._3; v8_15_._4; v8_15_._5; v8_15_._6; v8_15_._7; v8_15_._8
+      ]
+    in
+    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16);
+    Rust_primitives.Hax.array_of_list 16 list
+  }
+  <:
+  Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+
 let serialize_1_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
-  let result:t_Array u8 (sz 2) = Rust_primitives.Hax.repeat 0uy (sz 2) in
-  let result:t_Array u8 (sz 2) =
-    Rust_primitives.Hax.Folds.fold_range (sz 0)
-      (sz 8)
-      (fun result temp_1_ ->
-          let result:t_Array u8 (sz 2) = result in
-          let _:usize = temp_1_ in
-          true)
-      result
-      (fun result i ->
-          let result:t_Array u8 (sz 2) = result in
-          let i:usize = i in
-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result
-            (sz 0)
-            ((result.[ sz 0 ] <: u8) |.
-              ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ i ] <: i16) <: u8) <<!
-                i
+  let result0:u8 =
+    (((((((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 0 ] <: i16) <: u8) |.
+                ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 1 ] <: i16)
+                    <:
+                    u8) <<!
+                  1l
+                  <:
+                  u8)
+                <:
+                u8) |.
+              ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 2 ] <: i16) <: u8
+                ) <<!
+                2l
                 <:
                 u8)
               <:
+              u8) |.
+            ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 3 ] <: i16) <: u8) <<!
+              3l
+              <:
               u8)
+            <:
+            u8) |.
+          ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 4 ] <: i16) <: u8) <<!
+            4l
+            <:
+            u8)
+          <:
+          u8) |.
+        ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 5 ] <: i16) <: u8) <<!
+          5l
           <:
-          t_Array u8 (sz 2))
-  in
-  let result:t_Array u8 (sz 2) =
-    Rust_primitives.Hax.Folds.fold_range (sz 8)
-      (sz 16)
-      (fun result temp_1_ ->
-          let result:t_Array u8 (sz 2) = result in
-          let _:usize = temp_1_ in
-          true)
-      result
-      (fun result i ->
-          let result:t_Array u8 (sz 2) = result in
-          let i:usize = i in
-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result
-            (sz 1)
-            ((result.[ sz 1 ] <: u8) |.
-              ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ i ] <: i16) <: u8) <<!
-                (i -! sz 8 <: usize)
+          u8)
+        <:
+        u8) |.
+      ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 6 ] <: i16) <: u8) <<! 6l
+        <:
+        u8)
+      <:
+      u8) |.
+    ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 7 ] <: i16) <: u8) <<! 7l
+      <:
+      u8)
+  in
+  let result1:u8 =
+    (((((((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 8 ] <: i16) <: u8) |.
+                ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 9 ] <: i16)
+                    <:
+                    u8) <<!
+                  1l
+                  <:
+                  u8)
+                <:
+                u8) |.
+              ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 10 ] <: i16)
+                  <:
+                  u8) <<!
+                2l
                 <:
                 u8)
               <:
+              u8) |.
+            ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 11 ] <: i16) <: u8) <<!
+              3l
+              <:
               u8)
+            <:
+            u8) |.
+          ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 12 ] <: i16) <: u8) <<!
+            4l
+            <:
+            u8)
+          <:
+          u8) |.
+        ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 13 ] <: i16) <: u8) <<!
+          5l
           <:
-          t_Array u8 (sz 2))
+          u8)
+        <:
+        u8) |.
+      ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 14 ] <: i16) <: u8) <<!
+        6l
+        <:
+        u8)
+      <:
+      u8) |.
+    ((cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ sz 15 ] <: i16) <: u8) <<! 7l
+      <:
+      u8)
   in
-  result
+  let list = [result0; result1] in
+  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+  Rust_primitives.Hax.array_of_list 2 list
+
+#push-options "--compat_pre_core 2 --z3rlimit 300 --z3refresh"
+
+let serialize_1_bit_vec_lemma (v: t_Array i16 (sz 16))
+  (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 1))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 1 in
+     let outputs = bit_vec_of_int_t_array (serialize_1_ ({ f_elements = v })) 8 in
+     (forall (i: nat {i < 16}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+
+#push-options "--z3rlimit 300"
+
+let serialize_1_lemma inputs =
+  serialize_1_bit_vec_lemma inputs.f_elements ();
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (serialize_1_ inputs) 8) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 1))
+
+#pop-options
 
 let serialize_10_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
   let r0_4_:(u8 & u8 & u8 & u8 & u8) =
@@ -335,68 +710,37 @@ let serialize_10_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVecto
         <:
         t_Slice i16)
   in
-  let result:t_Array u8 (sz 20) = Rust_primitives.Hax.repeat 0uy (sz 20) in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 0) r0_4_._1
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 1) r0_4_._2
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 2) r0_4_._3
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 3) r0_4_._4
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 4) r0_4_._5
+  let list =
+    [
+      r0_4_._1; r0_4_._2; r0_4_._3; r0_4_._4; r0_4_._5; r5_9_._1; r5_9_._2; r5_9_._3; r5_9_._4;
+      r5_9_._5; r10_14_._1; r10_14_._2; r10_14_._3; r10_14_._4; r10_14_._5; r15_19_._1; r15_19_._2;
+      r15_19_._3; r15_19_._4; r15_19_._5
+    ]
   in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 5) r5_9_._1
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 6) r5_9_._2
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 7) r5_9_._3
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 8) r5_9_._4
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 9) r5_9_._5
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 10) r10_14_._1
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 11) r10_14_._2
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 12) r10_14_._3
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 13) r10_14_._4
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 14) r10_14_._5
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 15) r15_19_._1
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 16) r15_19_._2
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 17) r15_19_._3
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 18) r15_19_._4
-  in
-  let result:t_Array u8 (sz 20) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 19) r15_19_._5
-  in
-  result
+  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 20);
+  Rust_primitives.Hax.array_of_list 20 list
+
+#push-options "--compat_pre_core 2 --z3rlimit 300 --z3refresh"
+
+let serialize_10_bit_vec_lemma (v: t_Array i16 (sz 16))
+  (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 10))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 10 in
+     let outputs = bit_vec_of_int_t_array (serialize_10_ ({ f_elements = v })) 8 in
+     (forall (i: nat {i < 160}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+
+#push-options "--z3rlimit 300"
+
+let serialize_10_lemma inputs =
+  serialize_10_bit_vec_lemma inputs.f_elements ();
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (serialize_10_ inputs) 8) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 10))
+
+#pop-options
 
 let serialize_11_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
   let r0_10_:(u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8) =
@@ -419,74 +763,15 @@ let serialize_11_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVecto
         <:
         t_Slice i16)
   in
-  let result:t_Array u8 (sz 22) = Rust_primitives.Hax.repeat 0uy (sz 22) in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 0) r0_10_._1
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 1) r0_10_._2
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 2) r0_10_._3
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 3) r0_10_._4
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 4) r0_10_._5
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 5) r0_10_._6
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 6) r0_10_._7
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 7) r0_10_._8
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 8) r0_10_._9
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 9) r0_10_._10
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 10) r0_10_._11
+  let list =
+    [
+      r0_10_._1; r0_10_._2; r0_10_._3; r0_10_._4; r0_10_._5; r0_10_._6; r0_10_._7; r0_10_._8;
+      r0_10_._9; r0_10_._10; r0_10_._11; r11_21_._1; r11_21_._2; r11_21_._3; r11_21_._4; r11_21_._5;
+      r11_21_._6; r11_21_._7; r11_21_._8; r11_21_._9; r11_21_._10; r11_21_._11
+    ]
   in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 11) r11_21_._1
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 12) r11_21_._2
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 13) r11_21_._3
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 14) r11_21_._4
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 15) r11_21_._5
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 16) r11_21_._6
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 17) r11_21_._7
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 18) r11_21_._8
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 19) r11_21_._9
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 20) r11_21_._10
-  in
-  let result:t_Array u8 (sz 22) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 21) r11_21_._11
-  in
-  result
+  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 22);
+  Rust_primitives.Hax.array_of_list 22 list
 
 let serialize_12_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
   let r0_2_:(u8 & u8 & u8) =
@@ -569,80 +854,37 @@ let serialize_12_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVecto
         <:
         t_Slice i16)
   in
-  let result:t_Array u8 (sz 24) = Rust_primitives.Hax.repeat 0uy (sz 24) in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 0) r0_2_._1
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 1) r0_2_._2
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 2) r0_2_._3
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 3) r3_5_._1
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 4) r3_5_._2
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 5) r3_5_._3
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 6) r6_8_._1
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 7) r6_8_._2
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 8) r6_8_._3
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 9) r9_11_._1
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 10) r9_11_._2
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 11) r9_11_._3
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 12) r12_14_._1
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 13) r12_14_._2
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 14) r12_14_._3
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 15) r15_17_._1
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 16) r15_17_._2
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 17) r15_17_._3
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 18) r18_20_._1
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 19) r18_20_._2
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 20) r18_20_._3
+  let list =
+    [
+      r0_2_._1; r0_2_._2; r0_2_._3; r3_5_._1; r3_5_._2; r3_5_._3; r6_8_._1; r6_8_._2; r6_8_._3;
+      r9_11_._1; r9_11_._2; r9_11_._3; r12_14_._1; r12_14_._2; r12_14_._3; r15_17_._1; r15_17_._2;
+      r15_17_._3; r18_20_._1; r18_20_._2; r18_20_._3; r21_23_._1; r21_23_._2; r21_23_._3
+    ]
   in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 21) r21_23_._1
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 22) r21_23_._2
-  in
-  let result:t_Array u8 (sz 24) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 23) r21_23_._3
-  in
-  result
+  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 24);
+  Rust_primitives.Hax.array_of_list 24 list
+
+#push-options "--compat_pre_core 2 --z3rlimit 300 --z3refresh"
+
+let serialize_12_bit_vec_lemma (v: t_Array i16 (sz 16))
+  (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 12))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 12 in
+     let outputs = bit_vec_of_int_t_array (serialize_12_ ({ f_elements = v })) 8 in
+     (forall (i: nat {i < 192}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+
+#push-options "--z3rlimit 300"
+
+let serialize_12_lemma inputs =
+  serialize_12_bit_vec_lemma inputs.f_elements ();
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (serialize_12_ inputs) 8) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 12))
+
+#pop-options
 
 let serialize_4_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
   let result0_3_:(u8 & u8 & u8 & u8) =
@@ -665,32 +907,42 @@ let serialize_4_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
         <:
         t_Slice i16)
   in
-  let result:t_Array u8 (sz 8) = Rust_primitives.Hax.repeat 0uy (sz 8) in
-  let result:t_Array u8 (sz 8) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 0) result0_3_._1
-  in
-  let result:t_Array u8 (sz 8) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 1) result0_3_._2
-  in
-  let result:t_Array u8 (sz 8) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 2) result0_3_._3
-  in
-  let result:t_Array u8 (sz 8) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 3) result0_3_._4
-  in
-  let result:t_Array u8 (sz 8) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 4) result4_7_._1
-  in
-  let result:t_Array u8 (sz 8) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 5) result4_7_._2
-  in
-  let result:t_Array u8 (sz 8) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 6) result4_7_._3
-  in
-  let result:t_Array u8 (sz 8) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 7) result4_7_._4
-  in
-  result
+  let list =
+    [
+      result0_3_._1;
+      result0_3_._2;
+      result0_3_._3;
+      result0_3_._4;
+      result4_7_._1;
+      result4_7_._2;
+      result4_7_._3;
+      result4_7_._4
+    ]
+  in
+  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 8);
+  Rust_primitives.Hax.array_of_list 8 list
+
+#push-options "--compat_pre_core 2 --z3rlimit 300 --z3refresh"
+
+let serialize_4_bit_vec_lemma (v: t_Array i16 (sz 16))
+  (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 4))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 4 in
+     let outputs = bit_vec_of_int_t_array (serialize_4_ ({ f_elements = v })) 8 in
+     (forall (i: nat {i < 64}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+
+#push-options "--z3rlimit 300"
+
+let serialize_4_lemma inputs =
+  serialize_4_bit_vec_lemma inputs.f_elements ();
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (serialize_4_ inputs) 8) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 4))
+
+#pop-options
 
 let serialize_5_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
   let r0_4_:(u8 & u8 & u8 & u8 & u8) =
@@ -713,1273 +965,11 @@ let serialize_5_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
         <:
         t_Slice i16)
   in
-  let result:t_Array u8 (sz 10) = Rust_primitives.Hax.repeat 0uy (sz 10) in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 0) r0_4_._1
-  in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 1) r0_4_._2
-  in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 2) r0_4_._3
-  in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 3) r0_4_._4
-  in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 4) r0_4_._5
-  in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 5) r5_9_._1
-  in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 6) r5_9_._2
-  in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 7) r5_9_._3
-  in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 8) r5_9_._4
-  in
-  let result:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result (sz 9) r5_9_._5
-  in
-  result
-
-let deserialize_1_ (v: t_Slice u8) =
-  let result:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    Libcrux_ml_kem.Vector.Portable.Vector_type.zero ()
-  in
-  let result:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    Rust_primitives.Hax.Folds.fold_range (sz 0)
-      (sz 8)
-      (fun result temp_1_ ->
-          let result:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = result in
-          let _:usize = temp_1_ in
-          true)
-      result
-      (fun result i ->
-          let result:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = result in
-          let i:usize = i in
-          {
-            result with
-            Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-            =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result
-                .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-              i
-              (cast (((v.[ sz 0 ] <: u8) >>! i <: u8) &. 1uy <: u8) <: i16)
-            <:
-            t_Array i16 (sz 16)
-          }
-          <:
-          Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-  in
-  let result:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    Rust_primitives.Hax.Folds.fold_range (sz 8)
-      Libcrux_ml_kem.Vector.Traits.v_FIELD_ELEMENTS_IN_VECTOR
-      (fun result temp_1_ ->
-          let result:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = result in
-          let _:usize = temp_1_ in
-          true)
-      result
-      (fun result i ->
-          let result:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = result in
-          let i:usize = i in
-          {
-            result with
-            Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-            =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize result
-                .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-              i
-              (cast (((v.[ sz 1 ] <: u8) >>! (i -! sz 8 <: usize) <: u8) &. 1uy <: u8) <: i16)
-            <:
-            t_Array i16 (sz 16)
-          }
-          <:
-          Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-  in
-  result
-
-let deserialize_10_ (bytes: t_Slice u8) =
-  let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
-    deserialize_10_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 10 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v8_15_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
-    deserialize_10_int (bytes.[ { Core.Ops.Range.f_start = sz 10; Core.Ops.Range.f_end = sz 20 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    Libcrux_ml_kem.Vector.Portable.Vector_type.zero ()
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 0)
-        v0_7_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 1)
-        v0_7_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 2)
-        v0_7_._3
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 3)
-        v0_7_._4
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 4)
-        v0_7_._5
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 5)
-        v0_7_._6
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 6)
-        v0_7_._7
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 7)
-        v0_7_._8
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 8)
-        v8_15_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 9)
-        v8_15_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 10)
-        v8_15_._3
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 11)
-        v8_15_._4
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 12)
-        v8_15_._5
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 13)
-        v8_15_._6
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 14)
-        v8_15_._7
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 15)
-        v8_15_._8
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  v
-
-let deserialize_11_ (bytes: t_Slice u8) =
-  let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
-    deserialize_11_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 11 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v8_15_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
-    deserialize_11_int (bytes.[ { Core.Ops.Range.f_start = sz 11; Core.Ops.Range.f_end = sz 22 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    Libcrux_ml_kem.Vector.Portable.Vector_type.zero ()
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 0)
-        v0_7_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 1)
-        v0_7_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 2)
-        v0_7_._3
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 3)
-        v0_7_._4
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 4)
-        v0_7_._5
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 5)
-        v0_7_._6
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 6)
-        v0_7_._7
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 7)
-        v0_7_._8
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 8)
-        v8_15_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 9)
-        v8_15_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 10)
-        v8_15_._3
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 11)
-        v8_15_._4
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 12)
-        v8_15_._5
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 13)
-        v8_15_._6
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 14)
-        v8_15_._7
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 15)
-        v8_15_._8
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  v
-
-let deserialize_12_ (bytes: t_Slice u8) =
-  let v0_1_:(i16 & i16) =
-    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 3 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v2_3_:(i16 & i16) =
-    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 3; Core.Ops.Range.f_end = sz 6 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v4_5_:(i16 & i16) =
-    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 6; Core.Ops.Range.f_end = sz 9 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v6_7_:(i16 & i16) =
-    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 9; Core.Ops.Range.f_end = sz 12 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v8_9_:(i16 & i16) =
-    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 12; Core.Ops.Range.f_end = sz 15 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v10_11_:(i16 & i16) =
-    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 15; Core.Ops.Range.f_end = sz 18 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v12_13_:(i16 & i16) =
-    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 18; Core.Ops.Range.f_end = sz 21 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v14_15_:(i16 & i16) =
-    deserialize_12_int (bytes.[ { Core.Ops.Range.f_start = sz 21; Core.Ops.Range.f_end = sz 24 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    Libcrux_ml_kem.Vector.Portable.Vector_type.zero ()
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 0)
-        v0_1_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 1)
-        v0_1_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 2)
-        v2_3_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 3)
-        v2_3_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 4)
-        v4_5_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 5)
-        v4_5_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 6)
-        v6_7_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 7)
-        v6_7_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 8)
-        v8_9_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 9)
-        v8_9_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 10)
-        v10_11_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 11)
-        v10_11_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 12)
-        v12_13_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 13)
-        v12_13_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 14)
-        v14_15_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let re:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      re with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 15)
-        v14_15_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  re
-
-let deserialize_4_ (bytes: t_Slice u8) =
-  let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
-    deserialize_4_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 4 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v8_15_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
-    deserialize_4_int (bytes.[ { Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 8 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    Libcrux_ml_kem.Vector.Portable.Vector_type.zero ()
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 0)
-        v0_7_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 1)
-        v0_7_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 2)
-        v0_7_._3
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 3)
-        v0_7_._4
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 4)
-        v0_7_._5
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 5)
-        v0_7_._6
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 6)
-        v0_7_._7
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 7)
-        v0_7_._8
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 8)
-        v8_15_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 9)
-        v8_15_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 10)
-        v8_15_._3
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 11)
-        v8_15_._4
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 12)
-        v8_15_._5
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 13)
-        v8_15_._6
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 14)
-        v8_15_._7
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 15)
-        v8_15_._8
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  v
-
-let deserialize_5_ (bytes: t_Slice u8) =
-  let v0_7_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
-    deserialize_5_int (bytes.[ { Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 5 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v8_15_:(i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16) =
-    deserialize_5_int (bytes.[ { Core.Ops.Range.f_start = sz 5; Core.Ops.Range.f_end = sz 10 }
-          <:
-          Core.Ops.Range.t_Range usize ]
-        <:
-        t_Slice u8)
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    Libcrux_ml_kem.Vector.Portable.Vector_type.zero ()
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 0)
-        v0_7_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 1)
-        v0_7_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 2)
-        v0_7_._3
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 3)
-        v0_7_._4
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 4)
-        v0_7_._5
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 5)
-        v0_7_._6
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 6)
-        v0_7_._7
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 7)
-        v0_7_._8
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 8)
-        v8_15_._1
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 9)
-        v8_15_._2
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 10)
-        v8_15_._3
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 11)
-        v8_15_._4
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 12)
-        v8_15_._5
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 13)
-        v8_15_._6
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 14)
-        v8_15_._7
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-  in
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
-    {
-      v with
-      Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-          .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-        (sz 15)
-        v8_15_._8
-    }
-    <:
-    Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+  let list =
+    [
+      r0_4_._1; r0_4_._2; r0_4_._3; r0_4_._4; r0_4_._5; r5_9_._1; r5_9_._2; r5_9_._3; r5_9_._4;
+      r5_9_._5
+    ]
   in
-  v
+  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 10);
+  Rust_primitives.Hax.array_of_list 10 list
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fsti
index 978699fa8..1456b37d8 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.fsti
@@ -5,88 +5,126 @@ open FStar.Mul
 
 val deserialize_10_int (bytes: t_Slice u8)
     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 bytes =. sz 10)
       (fun _ -> Prims.l_True)
 
 val deserialize_11_int (bytes: t_Slice u8)
     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 bytes =. sz 11)
       (fun _ -> Prims.l_True)
 
 val deserialize_12_int (bytes: t_Slice u8)
-    : Prims.Pure (i16 & i16) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (i16 & i16)
+      (requires Core.Slice.impl__len #u8 bytes =. sz 3)
+      (fun _ -> Prims.l_True)
 
 val deserialize_4_int (bytes: t_Slice u8)
     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 bytes =. sz 4)
       (fun _ -> Prims.l_True)
 
 val deserialize_5_int (bytes: t_Slice u8)
     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 bytes =. sz 5)
       (fun _ -> Prims.l_True)
 
 val serialize_10_int (v: t_Slice i16)
-    : Prims.Pure (u8 & u8 & u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (u8 & u8 & u8 & u8 & u8)
+      (requires Core.Slice.impl__len #i16 v =. sz 4)
+      (fun _ -> Prims.l_True)
 
 val serialize_11_int (v: t_Slice i16)
     : Prims.Pure (u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8)
-      Prims.l_True
+      (requires Core.Slice.impl__len #i16 v =. sz 8)
       (fun _ -> Prims.l_True)
 
 val serialize_12_int (v: t_Slice i16)
-    : Prims.Pure (u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (u8 & u8 & u8)
+      (requires Core.Slice.impl__len #i16 v =. sz 2)
+      (fun _ -> Prims.l_True)
 
 val serialize_4_int (v: t_Slice i16)
-    : Prims.Pure (u8 & u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (u8 & u8 & u8 & u8)
+      (requires Core.Slice.impl__len #i16 v =. sz 8)
+      (fun _ -> Prims.l_True)
 
 val serialize_5_int (v: t_Slice i16)
-    : Prims.Pure (u8 & u8 & u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
-
-val serialize_1_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-    : Prims.Pure (t_Array u8 (sz 2)) Prims.l_True (fun _ -> Prims.l_True)
-
-val serialize_10_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-    : Prims.Pure (t_Array u8 (sz 20)) Prims.l_True (fun _ -> Prims.l_True)
-
-val serialize_11_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-    : Prims.Pure (t_Array u8 (sz 22)) Prims.l_True (fun _ -> Prims.l_True)
-
-val serialize_12_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-    : Prims.Pure (t_Array u8 (sz 24)) Prims.l_True (fun _ -> Prims.l_True)
-
-val serialize_4_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-    : Prims.Pure (t_Array u8 (sz 8)) Prims.l_True (fun _ -> Prims.l_True)
-
-val serialize_5_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-    : Prims.Pure (t_Array u8 (sz 10)) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (u8 & u8 & u8 & u8 & u8)
+      (requires Core.Slice.impl__len #i16 v =. sz 8)
+      (fun _ -> Prims.l_True)
 
 val deserialize_1_ (v: t_Slice u8)
     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 v =. sz 2)
       (fun _ -> Prims.l_True)
 
+val deserialize_1_lemma (inputs: t_Array u8 (sz 2)) : Lemma
+  (ensures bit_vec_of_int_t_array (deserialize_1_ inputs).f_elements 1 == bit_vec_of_int_t_array inputs 8)
+
 val deserialize_10_ (bytes: t_Slice u8)
     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 bytes =. sz 20)
       (fun _ -> Prims.l_True)
 
+val deserialize_10_lemma (inputs: t_Array u8 (sz 20)) : Lemma
+  (ensures bit_vec_of_int_t_array (deserialize_10_ inputs).f_elements 10 == bit_vec_of_int_t_array inputs 8)
+
 val deserialize_11_ (bytes: t_Slice u8)
     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 bytes =. sz 22)
       (fun _ -> Prims.l_True)
 
 val deserialize_12_ (bytes: t_Slice u8)
     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 bytes =. sz 24)
       (fun _ -> Prims.l_True)
 
+val deserialize_12_lemma (inputs: t_Array u8 (sz 24)) : Lemma
+  (ensures bit_vec_of_int_t_array (deserialize_12_ inputs).f_elements 12 == bit_vec_of_int_t_array inputs 8)
+
 val deserialize_4_ (bytes: t_Slice u8)
     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 bytes =. sz 8)
       (fun _ -> Prims.l_True)
 
+val deserialize_4_lemma (inputs: t_Array u8 (sz 8)) : Lemma
+  (ensures bit_vec_of_int_t_array (deserialize_4_ inputs).f_elements 4 == bit_vec_of_int_t_array inputs 8)
+
 val deserialize_5_ (bytes: t_Slice u8)
     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-      Prims.l_True
+      (requires Core.Slice.impl__len #u8 bytes =. sz 10)
       (fun _ -> Prims.l_True)
+
+val serialize_1_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+    : Prims.Pure (t_Array u8 (sz 2)) Prims.l_True (fun _ -> Prims.l_True)
+
+val serialize_1_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+  (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 1)) 
+  (ensures bit_vec_of_int_t_array (serialize_1_ inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 1)
+
+val serialize_10_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+    : Prims.Pure (t_Array u8 (sz 20)) Prims.l_True (fun _ -> Prims.l_True)
+
+val serialize_10_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+  (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 10)) 
+  (ensures bit_vec_of_int_t_array (serialize_10_ inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 10)
+
+val serialize_11_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+    : Prims.Pure (t_Array u8 (sz 22)) Prims.l_True (fun _ -> Prims.l_True)
+
+val serialize_12_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+    : Prims.Pure (t_Array u8 (sz 24)) Prims.l_True (fun _ -> Prims.l_True)
+
+val serialize_12_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+  (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 12)) 
+  (ensures bit_vec_of_int_t_array (serialize_12_ inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 12)
+
+val serialize_4_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+    : Prims.Pure (t_Array u8 (sz 8)) Prims.l_True (fun _ -> Prims.l_True)
+
+val serialize_4_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+  (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 4)) 
+  (ensures bit_vec_of_int_t_array (serialize_4_ inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 4)
+
+val serialize_5_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+    : Prims.Pure (t_Array u8 (sz 10)) Prims.l_True (fun _ -> Prims.l_True)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti
index ed7826f7a..00d0a1e3d 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti
@@ -1,5 +1,5 @@
 module Libcrux_ml_kem.Vector.Portable
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 300 --split_queries always"
 open Core
 open FStar.Mul
 
@@ -443,46 +443,58 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
         Libcrux_ml_kem.Vector.Portable.Ntt.ntt_multiply lhs rhs zeta0 zeta1 zeta2 zeta3);
     f_serialize_1_pre
     =
-    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
+    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        Spec.MLKEM.serialize_pre 1 (impl.f_repr a));
     f_serialize_1_post
     =
     (fun
         (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         (out: t_Array u8 (sz 2))
         ->
-        true);
+        Spec.MLKEM.serialize_pre 1 (impl.f_repr a) ==>
+        Spec.MLKEM.serialize_post 1 (impl.f_repr a) out);
     f_serialize_1_
     =
     (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.serialize_1_lemma a in
         Libcrux_ml_kem.Vector.Portable.Serialize.serialize_1_ a);
-    f_deserialize_1_pre = (fun (a: t_Slice u8) -> true);
+    f_deserialize_1_pre = (fun (a: t_Slice u8) -> (Core.Slice.impl__len #u8 a <: usize) =. sz 2);
     f_deserialize_1_post
     =
-    (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
+    (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        sz (Seq.length a) =. sz 2 ==> Spec.MLKEM.deserialize_post 1 a (impl.f_repr out));
     f_deserialize_1_
     =
-    (fun (a: t_Slice u8) -> Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_ a);
+    (fun (a: t_Slice u8) ->
+        let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_lemma a in
+        Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_ a);
     f_serialize_4_pre
     =
-    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
+    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        Spec.MLKEM.serialize_pre 4 (impl.f_repr a));
     f_serialize_4_post
     =
     (fun
         (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         (out: t_Array u8 (sz 8))
         ->
-        true);
+        Spec.MLKEM.serialize_pre 4 (impl.f_repr a) ==>
+        Spec.MLKEM.serialize_post 4 (impl.f_repr a) out);
     f_serialize_4_
     =
     (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.serialize_4_lemma a in
         Libcrux_ml_kem.Vector.Portable.Serialize.serialize_4_ a);
-    f_deserialize_4_pre = (fun (a: t_Slice u8) -> true);
+    f_deserialize_4_pre = (fun (a: t_Slice u8) -> (Core.Slice.impl__len #u8 a <: usize) =. sz 8);
     f_deserialize_4_post
     =
-    (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
+    (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        sz (Seq.length a) =. sz 8 ==> Spec.MLKEM.deserialize_post 4 a (impl.f_repr out));
     f_deserialize_4_
     =
-    (fun (a: t_Slice u8) -> Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_4_ a);
+    (fun (a: t_Slice u8) ->
+        let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_4_lemma a in
+        Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_4_ a);
     f_serialize_5_pre
     =
     (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
@@ -497,7 +509,7 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
     =
     (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
         Libcrux_ml_kem.Vector.Portable.Serialize.serialize_5_ a);
-    f_deserialize_5_pre = (fun (a: t_Slice u8) -> true);
+    f_deserialize_5_pre = (fun (a: t_Slice u8) -> (Core.Slice.impl__len #u8 a <: usize) =. sz 10);
     f_deserialize_5_post
     =
     (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
@@ -506,25 +518,31 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
     (fun (a: t_Slice u8) -> Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_5_ a);
     f_serialize_10_pre
     =
-    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
+    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        Spec.MLKEM.serialize_pre 10 (impl.f_repr a));
     f_serialize_10_post
     =
     (fun
         (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         (out: t_Array u8 (sz 20))
         ->
-        true);
+        Spec.MLKEM.serialize_pre 10 (impl.f_repr a) ==>
+        Spec.MLKEM.serialize_post 10 (impl.f_repr a) out);
     f_serialize_10_
     =
     (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.serialize_10_lemma a in
         Libcrux_ml_kem.Vector.Portable.Serialize.serialize_10_ a);
-    f_deserialize_10_pre = (fun (a: t_Slice u8) -> true);
+    f_deserialize_10_pre = (fun (a: t_Slice u8) -> (Core.Slice.impl__len #u8 a <: usize) =. sz 20);
     f_deserialize_10_post
     =
-    (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
+    (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        sz (Seq.length a) =. sz 20 ==> Spec.MLKEM.deserialize_post 10 a (impl.f_repr out));
     f_deserialize_10_
     =
-    (fun (a: t_Slice u8) -> Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_10_ a);
+    (fun (a: t_Slice u8) ->
+        let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_10_lemma a in
+        Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_10_ a);
     f_serialize_11_pre
     =
     (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
@@ -539,7 +557,7 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
     =
     (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
         Libcrux_ml_kem.Vector.Portable.Serialize.serialize_11_ a);
-    f_deserialize_11_pre = (fun (a: t_Slice u8) -> true);
+    f_deserialize_11_pre = (fun (a: t_Slice u8) -> (Core.Slice.impl__len #u8 a <: usize) =. sz 22);
     f_deserialize_11_post
     =
     (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
@@ -548,25 +566,31 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
     (fun (a: t_Slice u8) -> Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_11_ a);
     f_serialize_12_pre
     =
-    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
+    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        Spec.MLKEM.serialize_pre 12 (impl.f_repr a));
     f_serialize_12_post
     =
     (fun
         (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         (out: t_Array u8 (sz 24))
         ->
-        true);
+        Spec.MLKEM.serialize_pre 12 (impl.f_repr a) ==>
+        Spec.MLKEM.serialize_post 12 (impl.f_repr a) out);
     f_serialize_12_
     =
     (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.serialize_12_lemma a in
         Libcrux_ml_kem.Vector.Portable.Serialize.serialize_12_ a);
-    f_deserialize_12_pre = (fun (a: t_Slice u8) -> true);
+    f_deserialize_12_pre = (fun (a: t_Slice u8) -> (Core.Slice.impl__len #u8 a <: usize) =. sz 24);
     f_deserialize_12_post
     =
-    (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
+    (fun (a: t_Slice u8) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        sz (Seq.length a) =. sz 24 ==> Spec.MLKEM.deserialize_post 12 a (impl.f_repr out));
     f_deserialize_12_
     =
-    (fun (a: t_Slice u8) -> Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_12_ a);
+    (fun (a: t_Slice u8) ->
+        let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_12_lemma a in
+        Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_12_ a);
     f_rej_sample_pre = (fun (a: t_Slice u8) (out: t_Slice i16) -> true);
     f_rej_sample_post
     =
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti
index 155041e0a..a1de0f9af 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti
@@ -194,64 +194,98 @@ class t_Operations (v_Self: Type0) = {
     -> Prims.Pure v_Self
         (f_ntt_multiply_pre x0 x1 x2 x3 x4 x5)
         (fun result -> f_ntt_multiply_post x0 x1 x2 x3 x4 x5 result);
-  f_serialize_1_pre:a: v_Self -> pred: Type0{true ==> pred};
-  f_serialize_1_post:v_Self -> t_Array u8 (sz 2) -> Type0;
+  f_serialize_1_pre:a: v_Self -> pred: Type0{Spec.MLKEM.serialize_pre 1 (f_repr a) ==> pred};
+  f_serialize_1_post:a: v_Self -> result: t_Array u8 (sz 2)
+    -> pred:
+      Type0
+        { pred ==>
+          Spec.MLKEM.serialize_pre 1 (f_repr a) ==> Spec.MLKEM.serialize_post 1 (f_repr a) result };
   f_serialize_1_:x0: v_Self
     -> Prims.Pure (t_Array u8 (sz 2))
         (f_serialize_1_pre x0)
         (fun result -> f_serialize_1_post x0 result);
-  f_deserialize_1_pre:a: t_Slice u8 -> pred: Type0{true ==> pred};
-  f_deserialize_1_post:t_Slice u8 -> v_Self -> Type0;
+  f_deserialize_1_pre:a: t_Slice u8
+    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. sz 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)};
   f_deserialize_1_:x0: t_Slice u8
     -> Prims.Pure v_Self (f_deserialize_1_pre x0) (fun result -> f_deserialize_1_post x0 result);
-  f_serialize_4_pre:a: v_Self -> pred: Type0{true ==> pred};
-  f_serialize_4_post:v_Self -> t_Array u8 (sz 8) -> Type0;
+  f_serialize_4_pre:a: v_Self -> pred: Type0{Spec.MLKEM.serialize_pre 4 (f_repr a) ==> pred};
+  f_serialize_4_post:a: v_Self -> result: t_Array u8 (sz 8)
+    -> pred:
+      Type0
+        { pred ==>
+          Spec.MLKEM.serialize_pre 4 (f_repr a) ==> Spec.MLKEM.serialize_post 4 (f_repr a) result };
   f_serialize_4_:x0: v_Self
     -> Prims.Pure (t_Array u8 (sz 8))
         (f_serialize_4_pre x0)
         (fun result -> f_serialize_4_post x0 result);
-  f_deserialize_4_pre:a: t_Slice u8 -> pred: Type0{true ==> pred};
-  f_deserialize_4_post:t_Slice u8 -> v_Self -> Type0;
+  f_deserialize_4_pre:a: t_Slice u8
+    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. sz 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)};
   f_deserialize_4_:x0: t_Slice u8
     -> Prims.Pure v_Self (f_deserialize_4_pre x0) (fun result -> f_deserialize_4_post x0 result);
-  f_serialize_5_pre:a: v_Self -> pred: Type0{true ==> pred};
+  f_serialize_5_pre:v_Self -> Type0;
   f_serialize_5_post:v_Self -> t_Array u8 (sz 10) -> Type0;
   f_serialize_5_:x0: v_Self
     -> Prims.Pure (t_Array u8 (sz 10))
         (f_serialize_5_pre x0)
         (fun result -> f_serialize_5_post x0 result);
-  f_deserialize_5_pre:a: t_Slice u8 -> pred: Type0{true ==> pred};
+  f_deserialize_5_pre:a: t_Slice u8
+    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. sz 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);
-  f_serialize_10_pre:a: v_Self -> pred: Type0{true ==> pred};
-  f_serialize_10_post:v_Self -> t_Array u8 (sz 20) -> Type0;
+  f_serialize_10_pre:a: v_Self -> pred: Type0{Spec.MLKEM.serialize_pre 10 (f_repr a) ==> pred};
+  f_serialize_10_post:a: v_Self -> result: t_Array u8 (sz 20)
+    -> pred:
+      Type0
+        { pred ==>
+          Spec.MLKEM.serialize_pre 10 (f_repr a) ==> Spec.MLKEM.serialize_post 10 (f_repr a) result
+        };
   f_serialize_10_:x0: v_Self
     -> Prims.Pure (t_Array u8 (sz 20))
         (f_serialize_10_pre x0)
         (fun result -> f_serialize_10_post x0 result);
-  f_deserialize_10_pre:a: t_Slice u8 -> pred: Type0{true ==> pred};
-  f_deserialize_10_post:t_Slice u8 -> v_Self -> Type0;
+  f_deserialize_10_pre:a: t_Slice u8
+    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. sz 20 ==> pred};
+  f_deserialize_10_post:a: t_Slice u8 -> result: v_Self
+    -> pred:
+      Type0
+        {pred ==> sz (Seq.length a) =. sz 20 ==> Spec.MLKEM.deserialize_post 10 a (f_repr result)};
   f_deserialize_10_:x0: t_Slice u8
     -> Prims.Pure v_Self (f_deserialize_10_pre x0) (fun result -> f_deserialize_10_post x0 result);
-  f_serialize_11_pre:a: v_Self -> pred: Type0{true ==> pred};
+  f_serialize_11_pre:v_Self -> Type0;
   f_serialize_11_post:v_Self -> t_Array u8 (sz 22) -> Type0;
   f_serialize_11_:x0: v_Self
     -> Prims.Pure (t_Array u8 (sz 22))
         (f_serialize_11_pre x0)
         (fun result -> f_serialize_11_post x0 result);
-  f_deserialize_11_pre:a: t_Slice u8 -> pred: Type0{true ==> pred};
+  f_deserialize_11_pre:a: t_Slice u8
+    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. sz 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);
-  f_serialize_12_pre:a: v_Self -> pred: Type0{true ==> pred};
-  f_serialize_12_post:v_Self -> t_Array u8 (sz 24) -> Type0;
+  f_serialize_12_pre:a: v_Self -> pred: Type0{Spec.MLKEM.serialize_pre 12 (f_repr a) ==> pred};
+  f_serialize_12_post:a: v_Self -> result: t_Array u8 (sz 24)
+    -> pred:
+      Type0
+        { pred ==>
+          Spec.MLKEM.serialize_pre 12 (f_repr a) ==> Spec.MLKEM.serialize_post 12 (f_repr a) result
+        };
   f_serialize_12_:x0: v_Self
     -> Prims.Pure (t_Array u8 (sz 24))
         (f_serialize_12_pre x0)
         (fun result -> f_serialize_12_post x0 result);
-  f_deserialize_12_pre:a: t_Slice u8 -> pred: Type0{true ==> pred};
-  f_deserialize_12_post:t_Slice u8 -> v_Self -> Type0;
+  f_deserialize_12_pre:a: t_Slice u8
+    -> pred: Type0{(Core.Slice.impl__len #u8 a <: usize) =. sz 24 ==> pred};
+  f_deserialize_12_post:a: t_Slice u8 -> result: v_Self
+    -> pred:
+      Type0
+        {pred ==> sz (Seq.length a) =. sz 24 ==> Spec.MLKEM.deserialize_post 12 a (f_repr result)};
   f_deserialize_12_:x0: t_Slice u8
     -> Prims.Pure v_Self (f_deserialize_12_pre x0) (fun result -> f_deserialize_12_post x0 result);
   f_rej_sample_pre:a: t_Slice u8 -> out: t_Slice i16 -> pred: Type0{true ==> pred};
diff --git a/libcrux-ml-kem/proofs/fstar/spec/ML.KEM.Spec.fst.config.json b/libcrux-ml-kem/proofs/fstar/extraction/ML.KEM.fst.config.json
similarity index 97%
rename from libcrux-ml-kem/proofs/fstar/spec/ML.KEM.Spec.fst.config.json
rename to libcrux-ml-kem/proofs/fstar/extraction/ML.KEM.fst.config.json
index 2509bf529..d7b3a38b6 100644
--- a/libcrux-ml-kem/proofs/fstar/spec/ML.KEM.Spec.fst.config.json
+++ b/libcrux-ml-kem/proofs/fstar/extraction/ML.KEM.fst.config.json
@@ -18,6 +18,7 @@
         "${HAX_HOME}/proof-libs/fstar/rust_primitives",
         "${HAX_HOME}/proof-libs/fstar/core",
         "${HAX_HOME}/hax-lib/proofs/fstar/extraction",
+        "../spec",
         "../../../../sys/platform/proofs/fstar/extraction",
         "../../../../libcrux-sha3/proofs/fstar/extraction",
         "../../../../libcrux-intrinsics/proofs/fstar/extraction"
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Makefile b/libcrux-ml-kem/proofs/fstar/extraction/Makefile
index c51c6275e..5886525fd 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Makefile
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Makefile
@@ -1,8 +1,9 @@
-# This is the list of modules that are fully admitted.
-# All other modules have individual annotations on their functions indicating verification status
+SLOW_MODULES += Libcrux_ml_kem.Vector.Portable.Serialize.fst
+
 ADMIT_MODULES = Libcrux_ml_kem.Ind_cca.Unpacked.fst \
               Libcrux_ml_kem.Invert_ntt.fst \
               Libcrux_ml_kem.Ntt.fst \
+              Libcrux_ml_kem.Serialize.fst \
               Libcrux_ml_kem.Sampling.fst \
               Libcrux_ml_kem.Polynomial.fst \
               Libcrux_ml_kem.Vector.Avx2.fst \
@@ -11,7 +12,6 @@ ADMIT_MODULES = Libcrux_ml_kem.Ind_cca.Unpacked.fst \
               Libcrux_ml_kem.Vector.Portable.Compress.fst \
               Libcrux_ml_kem.Vector.Portable.Ntt.fst \
               Libcrux_ml_kem.Vector.Portable.Sampling.fst \
-              Libcrux_ml_kem.Vector.Portable.Serialize.fst \
               Libcrux_ml_kem.Vector.Portable.Vector_type.fst \
               Libcrux_ml_kem.Vector.Rej_sample_table.fsti \
               Libcrux_ml_kem.Vector.Neon.Arithmetic.fst \
@@ -20,6 +20,6 @@ ADMIT_MODULES = Libcrux_ml_kem.Ind_cca.Unpacked.fst \
               Libcrux_ml_kem.Vector.Neon.fst \
               Libcrux_ml_kem.Vector.Neon.Ntt.fst \
               Libcrux_ml_kem.Vector.Neon.Serialize.fst \
-              Libcrux_ml_kem.Vector.Neon.Vector_type.fst \
+              Libcrux_ml_kem.Vector.Neon.Vector_type.fst
 
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.base
diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Math.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Math.fst
index 9057da69f..dabcb0f5c 100644
--- a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Math.fst
+++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Math.fst
@@ -285,5 +285,4 @@ let deserialize_post
   (output: t_Array i16 (sz 16))
   = BitVecEq.int_t_array_bitwise_eq bytes  8
                                     output d1
-  /\ (forall i. i < 16 ==> bounded (Seq.index output i) d1)
 #pop-options
diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst
index 463bb1d5a..714882751 100644
--- a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst
+++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst
@@ -22,7 +22,7 @@ let map2 #a #b #c (#len:usize{v len < pow2 32})
 
 let repeati #acc (l:usize) (f:(i:usize{v i < v l}) -> acc -> acc) acc0 : acc = Lib.LoopCombinators.repeati (v l) (fun i acc -> f (sz i) acc) acc0
   
-#push-options "--fuel 0 --ifuel 0 --z3rlimit 500"
+#push-options "--z3rlimit 500"
 let flatten #t #n
   (#m: usize {range (v n * v m) usize_inttype})
   (x: t_Array (t_Array t m) n)
diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs
index dae6d21b5..a709a62e7 100644
--- a/libcrux-ml-kem/src/ind_cca.rs
+++ b/libcrux-ml-kem/src/ind_cca.rs
@@ -39,6 +39,7 @@ pub(crate) mod instantiations;
 
 /// Serialize the secret key.
 #[inline(always)]
+#[hax_lib::fstar::options("--z3rlimit 150")]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $SERIALIZED_KEY_LEN == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\\
     ${private_key.len()} == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\\
diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs
index 93bfca2fa..e5a205174 100644
--- a/libcrux-ml-kem/src/vector/avx2.rs
+++ b/libcrux-ml-kem/src/vector/avx2.rs
@@ -53,44 +53,44 @@ impl crate::vector::traits::Repr for SIMD256Vector {
 #[hax_lib::attributes]
 impl Operations for SIMD256Vector {
     #[inline(always)]
-    #[ensures(|result| fstar!("impl.f_repr out == Seq.create 16 0s"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Seq.create 16 0s"))]
     fn ZERO() -> Self {
         vec_zero()
     }
 
     #[requires(array.len() == 16)]
-    #[ensures(|result| fstar!("impl.f_repr out == $array"))]
+    #[ensures(|out| fstar!("impl.f_repr out == $array"))]
     fn from_i16_array(array: &[i16]) -> Self {
         vec_from_i16_array(array)
     }
 
-    #[ensures(|result| fstar!("out == impl.f_repr $x"))]
+    #[ensures(|out| fstar!("out == impl.f_repr $x"))]
     fn to_i16_array(x: Self) -> [i16; 16] {
         vec_to_i16_array(x)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map2 (+.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map2 (+.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
     fn add(lhs: Self, rhs: &Self) -> Self {
         Self {
             elements: arithmetic::add(lhs.elements, rhs.elements),
         }
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map2 (-.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map2 (-.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
     fn sub(lhs: Self, rhs: &Self) -> Self {
         Self {
             elements: arithmetic::sub(lhs.elements, rhs.elements),
         }
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x *. c) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x *. c) (impl.f_repr $v)"))]
     fn multiply_by_constant(v: Self, c: i16) -> Self {
         Self {
             elements: arithmetic::multiply_by_constant(v.elements, c),
         }
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x &. $constant) (impl.f_repr $vector)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x &. $constant) (impl.f_repr $vector)"))]
     fn bitwise_and_with_constant(vector: Self, constant: i16) -> Self {
         Self {
             elements: arithmetic::bitwise_and_with_constant(vector.elements, constant),
@@ -98,7 +98,7 @@ impl Operations for SIMD256Vector {
     }
 
     #[requires(SHIFT_BY >= 0 && SHIFT_BY < 16)]
-    #[ensures(|result| fstar!("(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $vector)"))]
+    #[ensures(|out| fstar!("(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $vector)"))]
     fn shift_right<const SHIFT_BY: i32>(vector: Self) -> Self {
         Self {
             elements: arithmetic::shift_right::<{ SHIFT_BY }>(vector.elements),
@@ -106,7 +106,7 @@ impl Operations for SIMD256Vector {
     }
 
     #[requires(true)]
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (impl.f_repr $vector)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (impl.f_repr $vector)"))]
     fn cond_subtract_3329(vector: Self) -> Self {
         Self {
             elements: arithmetic::cond_subtract_3329(vector.elements),
@@ -209,21 +209,37 @@ impl Operations for SIMD256Vector {
         }
     }
 
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 1 (impl.f_repr $vector)"))]
+    // Output name has be `out` https://github.com/hacspec/hax/issues/832
+    #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 1 (impl.f_repr $vector) ==> Spec.MLKEM.serialize_post 1 (impl.f_repr $vector) $out"))]
     fn serialize_1(vector: Self) -> [u8; 2] {
+        hax_lib::fstar!("admit()");
         serialize::serialize_1(vector.elements)
     }
 
+    #[requires(bytes.len() == 2)]
+    // Output name has be `out` https://github.com/hacspec/hax/issues/832
+    #[ensures(|out| fstar!("sz (Seq.length $bytes) =. sz 2 ==> Spec.MLKEM.deserialize_post 1 $bytes (impl.f_repr $out)"))]
     fn deserialize_1(bytes: &[u8]) -> Self {
+        hax_lib::fstar!("admit()");
         Self {
             elements: serialize::deserialize_1(bytes),
         }
     }
 
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 4 (impl.f_repr $vector)"))]
+    // Output name has be `out` https://github.com/hacspec/hax/issues/832
+    #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 4 (impl.f_repr $vector) ==> Spec.MLKEM.serialize_post 4 (impl.f_repr $vector) $out"))]
     fn serialize_4(vector: Self) -> [u8; 8] {
+        hax_lib::fstar!("admit()");
         serialize::serialize_4(vector.elements)
     }
 
+    #[requires(bytes.len() == 8)]
+    // Output name has be `out` https://github.com/hacspec/hax/issues/832
+    #[ensures(|out| fstar!("sz (Seq.length $bytes) =. sz 8 ==> Spec.MLKEM.deserialize_post 4 $bytes (impl.f_repr $out)"))]
     fn deserialize_4(bytes: &[u8]) -> Self {
+        hax_lib::fstar!("admit()");
         Self {
             elements: serialize::deserialize_4(bytes),
         }
@@ -233,17 +249,26 @@ impl Operations for SIMD256Vector {
         serialize::serialize_5(vector.elements)
     }
 
+    #[requires(bytes.len() == 10)]
     fn deserialize_5(bytes: &[u8]) -> Self {
         Self {
             elements: serialize::deserialize_5(bytes),
         }
     }
 
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 10 (impl.f_repr $vector)"))]
+    // Output name has be `out` https://github.com/hacspec/hax/issues/832
+    #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 10 (impl.f_repr $vector) ==> Spec.MLKEM.serialize_post 10 (impl.f_repr $vector) $out"))]
     fn serialize_10(vector: Self) -> [u8; 20] {
+        hax_lib::fstar!("admit()");
         serialize::serialize_10(vector.elements)
     }
 
+    #[requires(bytes.len() == 20)]
+    // Output name has be `out` https://github.com/hacspec/hax/issues/832
+    #[ensures(|out| fstar!("sz (Seq.length $bytes) =. sz 20 ==> Spec.MLKEM.deserialize_post 10 $bytes (impl.f_repr $out)"))]
     fn deserialize_10(bytes: &[u8]) -> Self {
+        hax_lib::fstar!("admit()");
         Self {
             elements: serialize::deserialize_10(bytes),
         }
@@ -253,17 +278,26 @@ impl Operations for SIMD256Vector {
         serialize::serialize_11(vector.elements)
     }
 
+    #[requires(bytes.len() == 22)]
     fn deserialize_11(bytes: &[u8]) -> Self {
         Self {
             elements: serialize::deserialize_11(bytes),
         }
     }
 
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 12 (impl.f_repr $vector)"))]
+    // Output name has be `out` https://github.com/hacspec/hax/issues/832
+    #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 12 (impl.f_repr $vector) ==> Spec.MLKEM.serialize_post 12 (impl.f_repr $vector) $out"))]
     fn serialize_12(vector: Self) -> [u8; 24] {
+        hax_lib::fstar!("admit()");
         serialize::serialize_12(vector.elements)
     }
 
+    #[requires(bytes.len() == 24)]
+    // Output name has be `out` https://github.com/hacspec/hax/issues/832
+    #[ensures(|out| fstar!("sz (Seq.length $bytes) =. sz 24 ==> Spec.MLKEM.deserialize_post 12 $bytes (impl.f_repr $out)"))]
     fn deserialize_12(bytes: &[u8]) -> Self {
+        hax_lib::fstar!("admit()");
         Self {
             elements: serialize::deserialize_12(bytes),
         }
diff --git a/libcrux-ml-kem/src/vector/neon.rs b/libcrux-ml-kem/src/vector/neon.rs
index 394434cc7..bd3be862a 100644
--- a/libcrux-ml-kem/src/vector/neon.rs
+++ b/libcrux-ml-kem/src/vector/neon.rs
@@ -26,18 +26,18 @@ impl crate::vector::traits::Repr for SIMD128Vector {
 #[hax_lib::attributes]
 impl Operations for SIMD128Vector {
     #[inline(always)]
-    #[ensures(|result| fstar!("impl.f_repr out == Seq.create 16 0s"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Seq.create 16 0s"))]
     fn ZERO() -> Self {
         ZERO()
     }
 
     #[requires(array.len() == 16)]
-    #[ensures(|result| fstar!("impl.f_repr out == $array"))]
+    #[ensures(|out| fstar!("impl.f_repr out == $array"))]
     fn from_i16_array(array: &[i16]) -> Self {
         from_i16_array(array)
     }
 
-    #[ensures(|result| fstar!("out == impl.f_repr $x"))]
+    #[ensures(|out| fstar!("out == impl.f_repr $x"))]
     fn to_i16_array(x: Self) -> [i16; 16] {
         to_i16_array(x)
     }
diff --git a/libcrux-ml-kem/src/vector/portable.rs b/libcrux-ml-kem/src/vector/portable.rs
index 452c48fbf..1b34df9bc 100644
--- a/libcrux-ml-kem/src/vector/portable.rs
+++ b/libcrux-ml-kem/src/vector/portable.rs
@@ -23,51 +23,52 @@ impl crate::vector::traits::Repr for PortableVector {
 }
 
 #[hax_lib::attributes]
+#[hax_lib::fstar::options("--z3rlimit 300")]
 impl Operations for PortableVector {
-    #[ensures(|result| fstar!("impl.f_repr out == Seq.create 16 0s"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Seq.create 16 0s"))]
     fn ZERO() -> Self {
         zero()
     }
 
     #[requires(array.len() == 16)]
-    #[ensures(|result| fstar!("impl.f_repr out == $array"))]
+    #[ensures(|out| fstar!("impl.f_repr out == $array"))]
     fn from_i16_array(array: &[i16]) -> Self {
         from_i16_array(array)
     }
 
-    #[ensures(|result| fstar!("out == impl.f_repr $x"))]
+    #[ensures(|out| fstar!("out == impl.f_repr $x"))]
     fn to_i16_array(x: Self) -> [i16; 16] {
         to_i16_array(x)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map2 (+.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map2 (+.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
     fn add(lhs: Self, rhs: &Self) -> Self {
         add(lhs, rhs)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map2 (-.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map2 (-.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
     fn sub(lhs: Self, rhs: &Self) -> Self {
         sub(lhs, rhs)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x *. c) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x *. c) (impl.f_repr $v)"))]
     fn multiply_by_constant(v: Self, c: i16) -> Self {
         multiply_by_constant(v, c)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x &. c) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x &. c) (impl.f_repr $v)"))]
     fn bitwise_and_with_constant(v: Self, c: i16) -> Self {
         bitwise_and_with_constant(v, c)
     }
 
     #[requires(SHIFT_BY >= 0 && SHIFT_BY < 16)]
-    #[ensures(|result| fstar!("(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $v)"))]
     fn shift_right<const SHIFT_BY: i32>(v: Self) -> Self {
         shift_right::<{ SHIFT_BY }>(v)
     }
 
     #[requires(true)]
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (impl.f_repr $v)"))]
     fn cond_subtract_3329(v: Self) -> Self {
         cond_subtract_3329(v)
     }
@@ -133,19 +134,31 @@ impl Operations for PortableVector {
         ntt_multiply(lhs, rhs, zeta0, zeta1, zeta2, zeta3)
     }
 
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 1 (impl.f_repr $a)"))]
+    #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 1 (impl.f_repr $a) ==> Spec.MLKEM.serialize_post 1 (impl.f_repr $a) $out"))]
     fn serialize_1(a: Self) -> [u8; 2] {
+        hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.serialize_1_lemma $a");
         serialize_1(a)
     }
 
+    #[requires(a.len() == 2)]
+    #[ensures(|out| fstar!("sz (Seq.length $a) =. sz 2 ==> Spec.MLKEM.deserialize_post 1 $a (impl.f_repr $out)"))]
     fn deserialize_1(a: &[u8]) -> Self {
+        hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_lemma $a");
         deserialize_1(a)
     }
 
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 4 (impl.f_repr $a)"))]
+    #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 4 (impl.f_repr $a) ==> Spec.MLKEM.serialize_post 4 (impl.f_repr $a) $out"))]
     fn serialize_4(a: Self) -> [u8; 8] {
+        hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.serialize_4_lemma $a");
         serialize_4(a)
     }
 
+    #[requires(a.len() == 8)]
+    #[ensures(|out| fstar!("sz (Seq.length $a) =. sz 8 ==> Spec.MLKEM.deserialize_post 4 $a (impl.f_repr $out)"))]
     fn deserialize_4(a: &[u8]) -> Self {
+        hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_4_lemma $a");
         deserialize_4(a)
     }
 
@@ -153,15 +166,22 @@ impl Operations for PortableVector {
         serialize_5(a)
     }
 
+    #[requires(a.len() == 10)]
     fn deserialize_5(a: &[u8]) -> Self {
         deserialize_5(a)
     }
 
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 10 (impl.f_repr $a)"))]
+    #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 10 (impl.f_repr $a) ==> Spec.MLKEM.serialize_post 10 (impl.f_repr $a) $out"))]
     fn serialize_10(a: Self) -> [u8; 20] {
+        hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.serialize_10_lemma $a");
         serialize_10(a)
     }
 
+    #[requires(a.len() == 20)]
+    #[ensures(|out| fstar!("sz (Seq.length $a) =. sz 20 ==> Spec.MLKEM.deserialize_post 10 $a (impl.f_repr $out)"))]
     fn deserialize_10(a: &[u8]) -> Self {
+        hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_10_lemma $a");
         deserialize_10(a)
     }
 
@@ -169,15 +189,22 @@ impl Operations for PortableVector {
         serialize_11(a)
     }
 
+    #[requires(a.len() == 22)]
     fn deserialize_11(a: &[u8]) -> Self {
         deserialize_11(a)
     }
 
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 12 (impl.f_repr $a)"))]
+    #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 12 (impl.f_repr $a) ==> Spec.MLKEM.serialize_post 12 (impl.f_repr $a) $out"))]
     fn serialize_12(a: Self) -> [u8; 24] {
+        hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.serialize_12_lemma $a");
         serialize_12(a)
     }
 
+    #[requires(a.len() == 24)]
+    #[ensures(|out| fstar!("sz (Seq.length $a) =. sz 24 ==> Spec.MLKEM.deserialize_post 12 $a (impl.f_repr $out)"))]
     fn deserialize_12(a: &[u8]) -> Self {
+        hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_12_lemma $a");
         deserialize_12(a)
     }
 
diff --git a/libcrux-ml-kem/src/vector/portable/serialize.rs b/libcrux-ml-kem/src/vector/portable/serialize.rs
index e0818dc28..e10194a40 100644
--- a/libcrux-ml-kem/src/vector/portable/serialize.rs
+++ b/libcrux-ml-kem/src/vector/portable/serialize.rs
@@ -13,33 +13,124 @@
 // and code that updates arrays (in the outer functions).
 
 use super::vector_type::*;
-use crate::vector::traits::FIELD_ELEMENTS_IN_VECTOR;
 
+#[cfg_attr(hax, hax_lib::fstar::after(interface, "
+val serialize_1_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+  (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 1)) 
+  (ensures bit_vec_of_int_t_array (${serialize_1} inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 1)
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--z3rlimit 300\"
+
+let serialize_1_lemma inputs =
+  serialize_1_bit_vec_lemma inputs.f_elements ();
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${serialize_1} inputs) 8) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 1))
+
+#pop-options
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+let serialize_1_bit_vec_lemma (v: t_Array i16 (sz 16))
+  (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 1))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 1 in
+     let outputs = bit_vec_of_int_t_array (${serialize_1} ({ f_elements = v })) 8 in
+     (forall (i: nat {i < 16}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+"))]
 #[inline(always)]
 pub(crate) fn serialize_1(v: PortableVector) -> [u8; 2] {
-    let mut result = [0u8; 2];
-    for i in 0..8 {
-        result[0] |= (v.elements[i] as u8) << i;
-    }
-    for i in 8..16 {
-        result[1] |= (v.elements[i] as u8) << (i - 8);
-    }
-    result
+    let result0 = (v.elements[0] as u8) | ((v.elements[1] as u8) << 1) |
+        ((v.elements[2] as u8) << 2) | ((v.elements[3] as u8) << 3) |
+        ((v.elements[4] as u8) << 4) | ((v.elements[5] as u8) << 5) |
+        ((v.elements[6] as u8) << 6) | ((v.elements[7] as u8) << 7);
+    let result1 = (v.elements[8] as u8) | ((v.elements[9] as u8) << 1) |
+        ((v.elements[10] as u8) << 2) | ((v.elements[11] as u8) << 3) |
+        ((v.elements[12] as u8) << 4) | ((v.elements[13] as u8) << 5) |
+        ((v.elements[14] as u8) << 6) | ((v.elements[15] as u8) << 7);
+    [
+        result0,
+        result1
+    ]
 }
 
+#[cfg_attr(hax, hax_lib::fstar::after(interface, "
+val deserialize_1_lemma (inputs: t_Array u8 (sz 2)) : Lemma
+  (ensures bit_vec_of_int_t_array (${deserialize_1} inputs).f_elements 1 == bit_vec_of_int_t_array inputs 8)
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--z3rlimit 300\"
+
+let deserialize_1_lemma inputs =
+  deserialize_1_bit_vec_lemma inputs;
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${deserialize_1} inputs).f_elements 1) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+#pop-options
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+let deserialize_1_bit_vec_lemma (v: t_Array u8 (sz 2))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 8 in
+     let outputs = bit_vec_of_int_t_array (${deserialize_1} v).f_elements 1 in
+     (forall (i: nat {i < 16}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+"))]
+#[hax_lib::requires(fstar!(r#"
+     ${v.len() == 2}
+"#))]
 #[inline(always)]
 pub(crate) fn deserialize_1(v: &[u8]) -> PortableVector {
-    let mut result = zero();
-    for i in 0..8 {
-        result.elements[i] = ((v[0] >> i) & 0x1) as i16;
-    }
-    for i in 8..FIELD_ELEMENTS_IN_VECTOR {
-        result.elements[i] = ((v[1] >> (i - 8)) & 0x1) as i16;
-    }
-    result
+    let result0 = (v[0] & 0x1) as i16;
+    let result1 = ((v[0] >> 1) & 0x1) as i16;
+    let result2 = ((v[0] >> 2) & 0x1) as i16;
+    let result3 = ((v[0] >> 3) & 0x1) as i16;
+    let result4 = ((v[0] >> 4) & 0x1) as i16;
+    let result5 = ((v[0] >> 5) & 0x1) as i16;
+    let result6 = ((v[0] >> 6) & 0x1) as i16;
+    let result7 = ((v[0] >> 7) & 0x1) as i16;
+    let result8 = (v[1] & 0x1) as i16;
+    let result9 = ((v[1] >> 1) & 0x1) as i16;
+    let result10 = ((v[1] >> 2) & 0x1) as i16;
+    let result11 = ((v[1] >> 3) & 0x1) as i16;
+    let result12 = ((v[1] >> 4) & 0x1) as i16;
+    let result13 = ((v[1] >> 5) & 0x1) as i16;
+    let result14 = ((v[1] >> 6) & 0x1) as i16;
+    let result15 = ((v[1] >> 7) & 0x1) as i16;
+    PortableVector { elements: [
+        result0,
+        result1,
+        result2,
+        result3,
+        result4,
+        result5,
+        result6,
+        result7,
+        result8,
+        result9,
+        result10,
+        result11,
+        result12,
+        result13,
+        result14,
+        result15,
+    ] }
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${v.len() == 8}
+"#))]
 pub(crate) fn serialize_4_int(v: &[i16]) -> (u8, u8, u8, u8) {
     let result0 = ((v[1] as u8) << 4) | (v[0] as u8);
     let result1 = ((v[3] as u8) << 4) | (v[2] as u8);
@@ -48,23 +139,55 @@ pub(crate) fn serialize_4_int(v: &[i16]) -> (u8, u8, u8, u8) {
     (result0, result1, result2, result3)
 }
 
+#[cfg_attr(hax, hax_lib::fstar::after(interface, "
+val serialize_4_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+  (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 4)) 
+  (ensures bit_vec_of_int_t_array (${serialize_4} inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 4)
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--z3rlimit 300\"
+
+let serialize_4_lemma inputs =
+  serialize_4_bit_vec_lemma inputs.f_elements ();
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${serialize_4} inputs) 8) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 4))
+
+#pop-options
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+let serialize_4_bit_vec_lemma (v: t_Array i16 (sz 16))
+  (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 4))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 4 in
+     let outputs = bit_vec_of_int_t_array (${serialize_4} ({ f_elements = v })) 8 in
+     (forall (i: nat {i < 64}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+"))]
 #[inline(always)]
 pub(crate) fn serialize_4(v: PortableVector) -> [u8; 8] {
     let result0_3 = serialize_4_int(&v.elements[0..8]);
     let result4_7 = serialize_4_int(&v.elements[8..16]);
-    let mut result = [0u8; 8];
-    result[0] = result0_3.0;
-    result[1] = result0_3.1;
-    result[2] = result0_3.2;
-    result[3] = result0_3.3;
-    result[4] = result4_7.0;
-    result[5] = result4_7.1;
-    result[6] = result4_7.2;
-    result[7] = result4_7.3;
-    result
+    [
+        result0_3.0,
+        result0_3.1,
+        result0_3.2,
+        result0_3.3,
+        result4_7.0,
+        result4_7.1,
+        result4_7.2,
+        result4_7.3,
+    ]
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 4}
+"#))]
 pub(crate) fn deserialize_4_int(bytes: &[u8]) -> (i16, i16, i16, i16, i16, i16, i16, i16) {
     let v0 = (bytes[0] & 0x0F) as i16;
     let v1 = ((bytes[0] >> 4) & 0x0F) as i16;
@@ -77,31 +200,64 @@ pub(crate) fn deserialize_4_int(bytes: &[u8]) -> (i16, i16, i16, i16, i16, i16,
     (v0, v1, v2, v3, v4, v5, v6, v7)
 }
 
+#[cfg_attr(hax, hax_lib::fstar::after(interface, "
+val deserialize_4_lemma (inputs: t_Array u8 (sz 8)) : Lemma
+  (ensures bit_vec_of_int_t_array (${deserialize_4} inputs).f_elements 4 == bit_vec_of_int_t_array inputs 8)
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--z3rlimit 300\"
+
+let deserialize_4_lemma inputs =
+  deserialize_4_bit_vec_lemma inputs;
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${deserialize_4} inputs).f_elements 4) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+#pop-options
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+let deserialize_4_bit_vec_lemma (v: t_Array u8 (sz 8))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 8 in
+     let outputs = bit_vec_of_int_t_array (${deserialize_4} v).f_elements 4 in
+     (forall (i: nat {i < 64}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+"))]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 8}
+"#))]
 #[inline(always)]
 pub(crate) fn deserialize_4(bytes: &[u8]) -> PortableVector {
     let v0_7 = deserialize_4_int(&bytes[0..4]);
     let v8_15 = deserialize_4_int(&bytes[4..8]);
-    let mut v = zero();
-    v.elements[0] = v0_7.0;
-    v.elements[1] = v0_7.1;
-    v.elements[2] = v0_7.2;
-    v.elements[3] = v0_7.3;
-    v.elements[4] = v0_7.4;
-    v.elements[5] = v0_7.5;
-    v.elements[6] = v0_7.6;
-    v.elements[7] = v0_7.7;
-    v.elements[8] = v8_15.0;
-    v.elements[9] = v8_15.1;
-    v.elements[10] = v8_15.2;
-    v.elements[11] = v8_15.3;
-    v.elements[12] = v8_15.4;
-    v.elements[13] = v8_15.5;
-    v.elements[14] = v8_15.6;
-    v.elements[15] = v8_15.7;
-    v
+    PortableVector { elements: [
+        v0_7.0,
+        v0_7.1,
+        v0_7.2,
+        v0_7.3,
+        v0_7.4,
+        v0_7.5,
+        v0_7.6,
+        v0_7.7,
+        v8_15.0,
+        v8_15.1,
+        v8_15.2,
+        v8_15.3,
+        v8_15.4,
+        v8_15.5,
+        v8_15.6,
+        v8_15.7,
+    ] }
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${v.len() == 8}
+"#))]
 pub(crate) fn serialize_5_int(v: &[i16]) -> (u8, u8, u8, u8, u8) {
     let r0 = (v[0] | v[1] << 5) as u8;
     let r1 = (v[1] >> 3 | v[2] << 2 | v[3] << 7) as u8;
@@ -111,25 +267,57 @@ pub(crate) fn serialize_5_int(v: &[i16]) -> (u8, u8, u8, u8, u8) {
     (r0, r1, r2, r3, r4)
 }
 
+// #[cfg_attr(hax, hax_lib::fstar::after(interface, "
+// val serialize_5_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+//   (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 5)) 
+//   (ensures bit_vec_of_int_t_array (${serialize_5} inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 5)
+// "))]
+// #[cfg_attr(hax, hax_lib::fstar::after("
+// #push-options \"--z3rlimit 300\"
+
+// let serialize_5_lemma inputs =
+//   serialize_5_bit_vec_lemma inputs.f_elements ();
+//   BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${serialize_5} inputs) 8) 
+//     (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 5))
+
+// #pop-options
+// "))]
+// #[cfg_attr(hax, hax_lib::fstar::after("
+// #push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+// let serialize_5_bit_vec_lemma (v: t_Array i16 (sz 16))
+//   (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 5))
+//    : squash (
+//      let inputs = bit_vec_of_int_t_array v 5 in
+//      let outputs = bit_vec_of_int_t_array (${serialize_5} ({ f_elements = v })) 8 in
+//      (forall (i: nat {i < 80}). inputs i == outputs i)
+//    ) =
+//   _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+// #pop-options
+// "))]
 #[inline(always)]
 pub(crate) fn serialize_5(v: PortableVector) -> [u8; 10] {
     let r0_4 = serialize_5_int(&v.elements[0..8]);
     let r5_9 = serialize_5_int(&v.elements[8..16]);
-    let mut result = [0u8; 10];
-    result[0] = r0_4.0;
-    result[1] = r0_4.1;
-    result[2] = r0_4.2;
-    result[3] = r0_4.3;
-    result[4] = r0_4.4;
-    result[5] = r5_9.0;
-    result[6] = r5_9.1;
-    result[7] = r5_9.2;
-    result[8] = r5_9.3;
-    result[9] = r5_9.4;
-    result
+    [
+        r0_4.0,
+        r0_4.1,
+        r0_4.2,
+        r0_4.3,
+        r0_4.4,
+        r5_9.0,
+        r5_9.1,
+        r5_9.2,
+        r5_9.3,
+        r5_9.4,
+    ]
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 5}
+"#))]
 pub(crate) fn deserialize_5_int(bytes: &[u8]) -> (i16, i16, i16, i16, i16, i16, i16, i16) {
     let v0 = (bytes[0] & 0x1F) as i16;
     let v1 = ((bytes[1] & 0x3) << 3 | (bytes[0] >> 5)) as i16;
@@ -142,31 +330,64 @@ pub(crate) fn deserialize_5_int(bytes: &[u8]) -> (i16, i16, i16, i16, i16, i16,
     (v0, v1, v2, v3, v4, v5, v6, v7)
 }
 
+// #[cfg_attr(hax, hax_lib::fstar::after(interface, "
+// val deserialize_5_lemma (inputs: t_Array u8 (sz 10)) : Lemma
+//   (ensures bit_vec_of_int_t_array (${deserialize_5} inputs).f_elements 5 == bit_vec_of_int_t_array inputs 8)
+// "))]
+// #[cfg_attr(hax, hax_lib::fstar::after("
+// #push-options \"--z3rlimit 300\"
+
+// let deserialize_5_lemma inputs =
+//   deserialize_5_bit_vec_lemma inputs;
+//   BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${deserialize_5} inputs).f_elements 5) 
+//     (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+// #pop-options
+// "))]
+// #[cfg_attr(hax, hax_lib::fstar::after("
+// #push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+// let deserialize_5_bit_vec_lemma (v: t_Array u8 (sz 10))
+//    : squash (
+//      let inputs = bit_vec_of_int_t_array v 8 in
+//      let outputs = bit_vec_of_int_t_array (${deserialize_5} v).f_elements 5 in
+//      (forall (i: nat {i < 80}). inputs i == outputs i)
+//    ) =
+//   _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+// #pop-options
+// "))]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 10}
+"#))]
 #[inline(always)]
 pub(crate) fn deserialize_5(bytes: &[u8]) -> PortableVector {
     let v0_7 = deserialize_5_int(&bytes[0..5]);
     let v8_15 = deserialize_5_int(&bytes[5..10]);
-    let mut v = zero();
-    v.elements[0] = v0_7.0;
-    v.elements[1] = v0_7.1;
-    v.elements[2] = v0_7.2;
-    v.elements[3] = v0_7.3;
-    v.elements[4] = v0_7.4;
-    v.elements[5] = v0_7.5;
-    v.elements[6] = v0_7.6;
-    v.elements[7] = v0_7.7;
-    v.elements[8] = v8_15.0;
-    v.elements[9] = v8_15.1;
-    v.elements[10] = v8_15.2;
-    v.elements[11] = v8_15.3;
-    v.elements[12] = v8_15.4;
-    v.elements[13] = v8_15.5;
-    v.elements[14] = v8_15.6;
-    v.elements[15] = v8_15.7;
-    v
+    PortableVector { elements: [
+        v0_7.0,
+        v0_7.1,
+        v0_7.2,
+        v0_7.3,
+        v0_7.4,
+        v0_7.5,
+        v0_7.6,
+        v0_7.7,
+        v8_15.0,
+        v8_15.1,
+        v8_15.2,
+        v8_15.3,
+        v8_15.4,
+        v8_15.5,
+        v8_15.6,
+        v8_15.7,
+    ] }
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${v.len() == 4}
+"#))]
 pub(crate) fn serialize_10_int(v: &[i16]) -> (u8, u8, u8, u8, u8) {
     let r0 = (v[0] & 0xFF) as u8;
     let r1 = ((v[1] & 0x3F) as u8) << 2 | ((v[0] >> 8) & 0x03) as u8;
@@ -176,43 +397,51 @@ pub(crate) fn serialize_10_int(v: &[i16]) -> (u8, u8, u8, u8, u8) {
     (r0, r1, r2, r3, r4)
 }
 
+#[cfg_attr(hax, hax_lib::fstar::after(interface, "
+val serialize_10_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+  (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 10)) 
+  (ensures bit_vec_of_int_t_array (${serialize_10} inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 10)
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--z3rlimit 300\"
+
+let serialize_10_lemma inputs =
+  serialize_10_bit_vec_lemma inputs.f_elements ();
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${serialize_10} inputs) 8) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 10))
+
+#pop-options
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+let serialize_10_bit_vec_lemma (v: t_Array i16 (sz 16))
+  (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 10))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 10 in
+     let outputs = bit_vec_of_int_t_array (${serialize_10} ({ f_elements = v })) 8 in
+     (forall (i: nat {i < 160}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+"))]
 #[inline(always)]
 pub(crate) fn serialize_10(v: PortableVector) -> [u8; 20] {
     let r0_4 = serialize_10_int(&v.elements[0..4]);
     let r5_9 = serialize_10_int(&v.elements[4..8]);
     let r10_14 = serialize_10_int(&v.elements[8..12]);
     let r15_19 = serialize_10_int(&v.elements[12..16]);
-    // Here we could also do, the following, but it slows F* down:
-    // [r0_4.0, r0_4.1, r0_4.2, r0_4.3, r0_4.4,
-    //  r5_9.0, r5_9.1, r5_9.2, r5_9.3, r5_9.4,
-    //  r10_14.0, r10_14.1, r10_14.2, r10_14.3, r10_14.4,
-    //  r15_19.0, r15_19.1, r15_19.2, r15_19.3, r15_19.4 ]
-    // If we can fix the F* for this, the code would be more compact.
-    let mut result = [0u8; 20];
-    result[0] = r0_4.0;
-    result[1] = r0_4.1;
-    result[2] = r0_4.2;
-    result[3] = r0_4.3;
-    result[4] = r0_4.4;
-    result[5] = r5_9.0;
-    result[6] = r5_9.1;
-    result[7] = r5_9.2;
-    result[8] = r5_9.3;
-    result[9] = r5_9.4;
-    result[10] = r10_14.0;
-    result[11] = r10_14.1;
-    result[12] = r10_14.2;
-    result[13] = r10_14.3;
-    result[14] = r10_14.4;
-    result[15] = r15_19.0;
-    result[16] = r15_19.1;
-    result[17] = r15_19.2;
-    result[18] = r15_19.3;
-    result[19] = r15_19.4;
-    result
+    [
+        r0_4.0, r0_4.1, r0_4.2, r0_4.3, r0_4.4, r5_9.0, r5_9.1, r5_9.2, r5_9.3, r5_9.4, r10_14.0,
+        r10_14.1, r10_14.2, r10_14.3, r10_14.4, r15_19.0, r15_19.1, r15_19.2, r15_19.3, r15_19.4,
+    ]
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 10}
+"#))]
 pub(crate) fn deserialize_10_int(bytes: &[u8]) -> (i16, i16, i16, i16, i16, i16, i16, i16) {
     let r0 = ((bytes[1] as i16 & 0x03) << 8 | (bytes[0] as i16 & 0xFF)) as i16;
     let r1 = ((bytes[2] as i16 & 0x0F) << 6 | (bytes[1] as i16 >> 2)) as i16;
@@ -225,31 +454,64 @@ pub(crate) fn deserialize_10_int(bytes: &[u8]) -> (i16, i16, i16, i16, i16, i16,
     (r0, r1, r2, r3, r4, r5, r6, r7)
 }
 
+#[cfg_attr(hax, hax_lib::fstar::after(interface, "
+val deserialize_10_lemma (inputs: t_Array u8 (sz 20)) : Lemma
+  (ensures bit_vec_of_int_t_array (${deserialize_10} inputs).f_elements 10 == bit_vec_of_int_t_array inputs 8)
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--z3rlimit 300\"
+
+let deserialize_10_lemma inputs =
+  deserialize_10_bit_vec_lemma inputs;
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${deserialize_10} inputs).f_elements 10) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+#pop-options
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+let deserialize_10_bit_vec_lemma (v: t_Array u8 (sz 20))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 8 in
+     let outputs = bit_vec_of_int_t_array (${deserialize_10} v).f_elements 10 in
+     (forall (i: nat {i < 160}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+"))]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 20}
+"#))]
 #[inline(always)]
 pub(crate) fn deserialize_10(bytes: &[u8]) -> PortableVector {
     let v0_7 = deserialize_10_int(&bytes[0..10]);
     let v8_15 = deserialize_10_int(&bytes[10..20]);
-    let mut v = zero();
-    v.elements[0] = v0_7.0;
-    v.elements[1] = v0_7.1;
-    v.elements[2] = v0_7.2;
-    v.elements[3] = v0_7.3;
-    v.elements[4] = v0_7.4;
-    v.elements[5] = v0_7.5;
-    v.elements[6] = v0_7.6;
-    v.elements[7] = v0_7.7;
-    v.elements[8] = v8_15.0;
-    v.elements[9] = v8_15.1;
-    v.elements[10] = v8_15.2;
-    v.elements[11] = v8_15.3;
-    v.elements[12] = v8_15.4;
-    v.elements[13] = v8_15.5;
-    v.elements[14] = v8_15.6;
-    v.elements[15] = v8_15.7;
-    v
+    PortableVector { elements: [
+        v0_7.0,
+        v0_7.1,
+        v0_7.2,
+        v0_7.3,
+        v0_7.4,
+        v0_7.5,
+        v0_7.6,
+        v0_7.7,
+        v8_15.0,
+        v8_15.1,
+        v8_15.2,
+        v8_15.3,
+        v8_15.4,
+        v8_15.5,
+        v8_15.6,
+        v8_15.7,
+    ] }
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${v.len() == 8}
+"#))]
 pub(crate) fn serialize_11_int(v: &[i16]) -> (u8, u8, u8, u8, u8, u8, u8, u8, u8, u8, u8) {
     let r0 = v[0] as u8;
     let r1 = ((v[1] & 0x1F) as u8) << 3 | ((v[0] >> 8) as u8);
@@ -265,76 +527,119 @@ pub(crate) fn serialize_11_int(v: &[i16]) -> (u8, u8, u8, u8, u8, u8, u8, u8, u8
     (r0, r1, r2, r3, r4, r5, r6, r7, r8, r9, r10)
 }
 
+// #[cfg_attr(hax, hax_lib::fstar::after(interface, "
+// val serialize_11_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+//   (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 11)) 
+//   (ensures bit_vec_of_int_t_array (${serialize_11} inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 11)
+// "))]
+// #[cfg_attr(hax, hax_lib::fstar::after("
+// #push-options \"--z3rlimit 300\"
+
+// let serialize_11_lemma inputs =
+//   serialize_11_bit_vec_lemma inputs.f_elements ();
+//   BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${serialize_11} inputs) 8) 
+//     (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 11))
+
+// #pop-options
+// "))]
+// #[cfg_attr(hax, hax_lib::fstar::after("
+// #push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+// let serialize_11_bit_vec_lemma (v: t_Array i16 (sz 16))
+//   (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 11))
+//    : squash (
+//      let inputs = bit_vec_of_int_t_array v 11 in
+//      let outputs = bit_vec_of_int_t_array (${serialize_11} ({ f_elements = v })) 8 in
+//      (forall (i: nat {i < 176}). inputs i == outputs i)
+//    ) =
+//   _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+// #pop-options
+// "))]
 #[inline(always)]
 pub(crate) fn serialize_11(v: PortableVector) -> [u8; 22] {
     let r0_10 = serialize_11_int(&v.elements[0..8]);
     let r11_21 = serialize_11_int(&v.elements[8..16]);
-    let mut result = [0u8; 22];
-    result[0] = r0_10.0;
-    result[1] = r0_10.1;
-    result[2] = r0_10.2;
-    result[3] = r0_10.3;
-    result[4] = r0_10.4;
-    result[5] = r0_10.5;
-    result[6] = r0_10.6;
-    result[7] = r0_10.7;
-    result[8] = r0_10.8;
-    result[9] = r0_10.9;
-    result[10] = r0_10.10;
-    result[11] = r11_21.0;
-    result[12] = r11_21.1;
-    result[13] = r11_21.2;
-    result[14] = r11_21.3;
-    result[15] = r11_21.4;
-    result[16] = r11_21.5;
-    result[17] = r11_21.6;
-    result[18] = r11_21.7;
-    result[19] = r11_21.8;
-    result[20] = r11_21.9;
-    result[21] = r11_21.10;
-    result
+    [
+        r0_10.0, r0_10.1, r0_10.2, r0_10.3, r0_10.4, r0_10.5, r0_10.6, r0_10.7, r0_10.8, r0_10.9, r0_10.10,
+        r11_21.0, r11_21.1, r11_21.2, r11_21.3, r11_21.4, r11_21.5, r11_21.6, r11_21.7, r11_21.8, r11_21.9, r11_21.10,
+    ]
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 11}
+"#))]
 pub(crate) fn deserialize_11_int(bytes: &[u8]) -> (i16, i16, i16, i16, i16, i16, i16, i16) {
-    let r0 = ((bytes[1] as i16 & 0x7) << 8 | bytes[0] as i16) as i16;
-    let r1 = ((bytes[2] as i16 & 0x3F) << 5 | (bytes[1] as i16 >> 3)) as i16;
-    let r2 = ((bytes[4] as i16 & 0x1) << 10 | ((bytes[3] as i16) << 2) | ((bytes[2] as i16) >> 6))
-        as i16;
-    let r3 = ((bytes[5] as i16 & 0xF) << 7 | (bytes[4] as i16 >> 1)) as i16;
-    let r4 = ((bytes[6] as i16 & 0x7F) << 4 | (bytes[5] as i16 >> 4)) as i16;
-    let r5 =
-        ((bytes[8] as i16 & 0x3) << 9 | ((bytes[7] as i16) << 1) | ((bytes[6] as i16) >> 7)) as i16;
-    let r6 = ((bytes[9] as i16 & 0x1F) << 6 | (bytes[8] as i16 >> 2)) as i16;
-    let r7 = (((bytes[10] as i16) << 3) | (bytes[9] as i16 >> 5)) as i16;
+    let r0 = (bytes[1] as i16 & 0x7) << 8 | bytes[0] as i16;
+    let r1 = (bytes[2] as i16 & 0x3F) << 5 | (bytes[1] as i16 >> 3);
+    let r2 = (bytes[4] as i16 & 0x1) << 10 | ((bytes[3] as i16) << 2) | ((bytes[2] as i16) >> 6);
+    let r3 = (bytes[5] as i16 & 0xF) << 7 | (bytes[4] as i16 >> 1);
+    let r4 = (bytes[6] as i16 & 0x7F) << 4 | (bytes[5] as i16 >> 4);
+    let r5 = (bytes[8] as i16 & 0x3) << 9 | ((bytes[7] as i16) << 1) | ((bytes[6] as i16) >> 7);
+    let r6 = (bytes[9] as i16 & 0x1F) << 6 | (bytes[8] as i16 >> 2);
+    let r7 = ((bytes[10] as i16) << 3) | (bytes[9] as i16 >> 5);
     (r0, r1, r2, r3, r4, r5, r6, r7)
 }
 
+// #[cfg_attr(hax, hax_lib::fstar::after(interface, "
+// val deserialize_11_lemma (inputs: t_Array u8 (sz 22)) : Lemma
+//   (ensures bit_vec_of_int_t_array (${deserialize_11} inputs).f_elements 11 == bit_vec_of_int_t_array inputs 8)
+// "))]
+// #[cfg_attr(hax, hax_lib::fstar::after("
+// #push-options \"--z3rlimit 300\"
+
+// let deserialize_11_lemma inputs =
+//   deserialize_11_bit_vec_lemma inputs;
+//   BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${deserialize_11} inputs).f_elements 11) 
+//     (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+// #pop-options
+// "))]
+// #[cfg_attr(hax, hax_lib::fstar::after("
+// #push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+// let deserialize_11_bit_vec_lemma (v: t_Array u8 (sz 22))
+//    : squash (
+//      let inputs = bit_vec_of_int_t_array v 8 in
+//      let outputs = bit_vec_of_int_t_array (${deserialize_11} v).f_elements 11 in
+//      (forall (i: nat {i < 176}). inputs i == outputs i)
+//    ) =
+//   _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+// #pop-options
+// "))]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 22}
+"#))]
 #[inline(always)]
 pub(crate) fn deserialize_11(bytes: &[u8]) -> PortableVector {
     let v0_7 = deserialize_11_int(&bytes[0..11]);
     let v8_15 = deserialize_11_int(&bytes[11..22]);
-    let mut v = zero();
-    v.elements[0] = v0_7.0;
-    v.elements[1] = v0_7.1;
-    v.elements[2] = v0_7.2;
-    v.elements[3] = v0_7.3;
-    v.elements[4] = v0_7.4;
-    v.elements[5] = v0_7.5;
-    v.elements[6] = v0_7.6;
-    v.elements[7] = v0_7.7;
-    v.elements[8] = v8_15.0;
-    v.elements[9] = v8_15.1;
-    v.elements[10] = v8_15.2;
-    v.elements[11] = v8_15.3;
-    v.elements[12] = v8_15.4;
-    v.elements[13] = v8_15.5;
-    v.elements[14] = v8_15.6;
-    v.elements[15] = v8_15.7;
-    v
+    PortableVector { elements: [
+        v0_7.0,
+        v0_7.1,
+        v0_7.2,
+        v0_7.3,
+        v0_7.4,
+        v0_7.5,
+        v0_7.6,
+        v0_7.7,
+        v8_15.0,
+        v8_15.1,
+        v8_15.2,
+        v8_15.3,
+        v8_15.4,
+        v8_15.5,
+        v8_15.6,
+        v8_15.7,
+    ] }
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${v.len() == 2}
+"#))]
 pub(crate) fn serialize_12_int(v: &[i16]) -> (u8, u8, u8) {
     let r0 = (v[0] & 0xFF) as u8;
     let r1 = ((v[0] >> 8) | ((v[1] & 0x0F) << 4)) as u8;
@@ -342,6 +647,35 @@ pub(crate) fn serialize_12_int(v: &[i16]) -> (u8, u8, u8) {
     (r0, r1, r2)
 }
 
+#[cfg_attr(hax, hax_lib::fstar::after(interface, "
+val serialize_12_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma
+  (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 12)) 
+  (ensures bit_vec_of_int_t_array (${serialize_12} inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 12)
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--z3rlimit 300\"
+
+let serialize_12_lemma inputs =
+  serialize_12_bit_vec_lemma inputs.f_elements ();
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${serialize_12} inputs) 8) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 12))
+
+#pop-options
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+let serialize_12_bit_vec_lemma (v: t_Array i16 (sz 16))
+  (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 12))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 12 in
+     let outputs = bit_vec_of_int_t_array (${serialize_12} ({ f_elements = v })) 8 in
+     (forall (i: nat {i < 192}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+"))]
 #[inline(always)]
 pub(crate) fn serialize_12(v: PortableVector) -> [u8; 24] {
     let r0_2 = serialize_12_int(&v.elements[0..2]);
@@ -352,35 +686,22 @@ pub(crate) fn serialize_12(v: PortableVector) -> [u8; 24] {
     let r15_17 = serialize_12_int(&v.elements[10..12]);
     let r18_20 = serialize_12_int(&v.elements[12..14]);
     let r21_23 = serialize_12_int(&v.elements[14..16]);
-    let mut result = [0u8; 24];
-    result[0] = r0_2.0;
-    result[1] = r0_2.1;
-    result[2] = r0_2.2;
-    result[3] = r3_5.0;
-    result[4] = r3_5.1;
-    result[5] = r3_5.2;
-    result[6] = r6_8.0;
-    result[7] = r6_8.1;
-    result[8] = r6_8.2;
-    result[9] = r9_11.0;
-    result[10] = r9_11.1;
-    result[11] = r9_11.2;
-    result[12] = r12_14.0;
-    result[13] = r12_14.1;
-    result[14] = r12_14.2;
-    result[15] = r15_17.0;
-    result[16] = r15_17.1;
-    result[17] = r15_17.2;
-    result[18] = r18_20.0;
-    result[19] = r18_20.1;
-    result[20] = r18_20.2;
-    result[21] = r21_23.0;
-    result[22] = r21_23.1;
-    result[23] = r21_23.2;
-    result
+    [
+        r0_2.0, r0_2.1, r0_2.2,
+        r3_5.0, r3_5.1, r3_5.2,
+        r6_8.0, r6_8.1, r6_8.2,
+        r9_11.0, r9_11.1, r9_11.2,
+        r12_14.0, r12_14.1, r12_14.2,
+        r15_17.0, r15_17.1, r15_17.2,
+        r18_20.0, r18_20.1, r18_20.2,
+        r21_23.0, r21_23.1, r21_23.2,
+    ]
 }
 
 #[inline(always)]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 3}
+"#))]
 pub(crate) fn deserialize_12_int(bytes: &[u8]) -> (i16, i16) {
     let byte0 = bytes[0] as i16;
     let byte1 = bytes[1] as i16;
@@ -390,6 +711,36 @@ pub(crate) fn deserialize_12_int(bytes: &[u8]) -> (i16, i16) {
     (r0, r1)
 }
 
+#[cfg_attr(hax, hax_lib::fstar::after(interface, "
+val deserialize_12_lemma (inputs: t_Array u8 (sz 24)) : Lemma
+  (ensures bit_vec_of_int_t_array (${deserialize_12} inputs).f_elements 12 == bit_vec_of_int_t_array inputs 8)
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--z3rlimit 300\"
+
+let deserialize_12_lemma inputs =
+  deserialize_12_bit_vec_lemma inputs;
+  BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${deserialize_12} inputs).f_elements 12) 
+    (BitVecEq.retype (bit_vec_of_int_t_array inputs 8))
+
+#pop-options
+"))]
+#[cfg_attr(hax, hax_lib::fstar::after("
+#push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\"
+
+let deserialize_12_bit_vec_lemma (v: t_Array u8 (sz 24))
+   : squash (
+     let inputs = bit_vec_of_int_t_array v 8 in
+     let outputs = bit_vec_of_int_t_array (${deserialize_12} v).f_elements 12 in
+     (forall (i: nat {i < 192}). inputs i == outputs i)
+   ) =
+  _ by (Tactics.GetBit.prove_bit_vector_equality' ())
+
+#pop-options
+"))]
+#[hax_lib::requires(fstar!(r#"
+     ${bytes.len() == 24}
+"#))]
 #[inline(always)]
 pub(crate) fn deserialize_12(bytes: &[u8]) -> PortableVector {
     let v0_1 = deserialize_12_int(&bytes[0..3]);
@@ -400,22 +751,22 @@ pub(crate) fn deserialize_12(bytes: &[u8]) -> PortableVector {
     let v10_11 = deserialize_12_int(&bytes[15..18]);
     let v12_13 = deserialize_12_int(&bytes[18..21]);
     let v14_15 = deserialize_12_int(&bytes[21..24]);
-    let mut re = zero();
-    re.elements[0] = v0_1.0;
-    re.elements[1] = v0_1.1;
-    re.elements[2] = v2_3.0;
-    re.elements[3] = v2_3.1;
-    re.elements[4] = v4_5.0;
-    re.elements[5] = v4_5.1;
-    re.elements[6] = v6_7.0;
-    re.elements[7] = v6_7.1;
-    re.elements[8] = v8_9.0;
-    re.elements[9] = v8_9.1;
-    re.elements[10] = v10_11.0;
-    re.elements[11] = v10_11.1;
-    re.elements[12] = v12_13.0;
-    re.elements[13] = v12_13.1;
-    re.elements[14] = v14_15.0;
-    re.elements[15] = v14_15.1;
-    re
+    PortableVector { elements: [
+        v0_1.0,
+        v0_1.1,
+        v2_3.0,
+        v2_3.1,
+        v4_5.0,
+        v4_5.1,
+        v6_7.0,
+        v6_7.1,
+        v8_9.0,
+        v8_9.1,
+        v10_11.0,
+        v10_11.1,
+        v12_13.0,
+        v12_13.1,
+        v14_15.0,
+        v14_15.1,
+    ] }
 }
diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs
index 006c0f188..f11137c50 100644
--- a/libcrux-ml-kem/src/vector/traits.rs
+++ b/libcrux-ml-kem/src/vector/traits.rs
@@ -91,46 +91,41 @@ pub trait Operations: Copy + Clone + Repr {
     fn ntt_multiply(lhs: &Self, rhs: &Self, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16)
         -> Self;
 
-    // #[requires(fstar!("Spec.MLKEM.serialize_pre 1 (f_repr $a)"))]
-    // #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 1 (f_repr $a) ==> Spec.MLKEM.serialize_post 1 (f_repr $a) $result"))]
-    #[requires(true)]
+    // Serialization and deserialization
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 1 (f_repr $a)"))]
+    #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 1 (f_repr $a) ==> Spec.MLKEM.serialize_post 1 (f_repr $a) $result"))]
     fn serialize_1(a: Self) -> [u8; 2];
-    #[requires(true)]
+    #[requires(a.len() == 2)]
+    #[ensures(|result| fstar!("sz (Seq.length $a) =. sz 2 ==> Spec.MLKEM.deserialize_post 1 $a (f_repr $result)"))]
     fn deserialize_1(a: &[u8]) -> Self;
 
-    // #[requires(fstar!("Spec.MLKEM.serialize_pre 4 (f_repr $a)"))]
-    // #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 4 (f_repr $a) ==> Spec.MLKEM.serialize_post 4 (f_repr $a) $result"))]
-    #[requires(true)]
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 4 (f_repr $a)"))]
+    #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 4 (f_repr $a) ==> Spec.MLKEM.serialize_post 4 (f_repr $a) $result"))]
     fn serialize_4(a: Self) -> [u8; 8];
-    #[requires(true)]
+    #[requires(a.len() == 8)]
+    #[ensures(|result| fstar!("sz (Seq.length $a) =. sz 8 ==> Spec.MLKEM.deserialize_post 4 $a (f_repr $result)"))]
     fn deserialize_4(a: &[u8]) -> Self;
 
-    // #[requires(fstar!("Spec.MLKEM.serialize_pre 5 (f_repr $a)"))]
-    // #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 5 (f_repr $a) ==> Spec.MLKEM.serialize_post 5 (f_repr $a) $result"))]
-    #[requires(true)]
     fn serialize_5(a: Self) -> [u8; 10];
-    #[requires(true)]
+    #[requires(a.len() == 10)]
     fn deserialize_5(a: &[u8]) -> Self;
 
-    // #[requires(fstar!("Spec.MLKEM.serialize_pre 10 (f_repr $a)"))]
-    // #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 10 (f_repr $a) ==> Spec.MLKEM.serialize_post 10 (f_repr $a) $result"))]
-    #[requires(true)]
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 10 (f_repr $a)"))]
+    #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 10 (f_repr $a) ==> Spec.MLKEM.serialize_post 10 (f_repr $a) $result"))]
     fn serialize_10(a: Self) -> [u8; 20];
-    #[requires(true)]
+    #[requires(a.len() == 20)]
+    #[ensures(|result| fstar!("sz (Seq.length $a) =. sz 20 ==> Spec.MLKEM.deserialize_post 10 $a (f_repr $result)"))]
     fn deserialize_10(a: &[u8]) -> Self;
 
-    // #[requires(fstar!("Spec.MLKEM.serialize_pre 11 (f_repr $a)"))]
-    // #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 11 (f_repr $a) ==> Spec.MLKEM.serialize_post 11 (f_repr $a) $result"))]
-    #[requires(true)]
     fn serialize_11(a: Self) -> [u8; 22];
-    #[requires(true)]
+    #[requires(a.len() == 22)]
     fn deserialize_11(a: &[u8]) -> Self;
 
-    // #[requires(fstar!("Spec.MLKEM.serialize_pre 12 (f_repr $a)"))]
-    // #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 12 (f_repr $a) ==> Spec.MLKEM.serialize_post 12 (f_repr $a) $result"))]
-    #[requires(true)]
+    #[requires(fstar!("Spec.MLKEM.serialize_pre 12 (f_repr $a)"))]
+    #[ensures(|result| fstar!("Spec.MLKEM.serialize_pre 12 (f_repr $a) ==> Spec.MLKEM.serialize_post 12 (f_repr $a) $result"))]
     fn serialize_12(a: Self) -> [u8; 24];
-    #[requires(true)]
+    #[requires(a.len() == 24)]
+    #[ensures(|result| fstar!("sz (Seq.length $a) =. sz 24 ==> Spec.MLKEM.deserialize_post 12 $a (f_repr $result)"))]
     fn deserialize_12(a: &[u8]) -> Self;
 
     #[requires(true)]
diff --git a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti
index e8713dad5..95dad6932 100644
--- a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti
+++ b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti
@@ -1,5 +1,5 @@
 module Libcrux_platform.Platform
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul