diff --git a/fstar-helpers/Makefile.base b/fstar-helpers/Makefile.base
index f74723cd2..d3ae5b5dd 100644
--- a/fstar-helpers/Makefile.base
+++ b/fstar-helpers/Makefile.base
@@ -10,6 +10,4 @@ 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
-FSTAR_INCLUDE_DIRS_EXTRA += $(shell git rev-parse --show-toplevel)/fstar-helpers/tactics
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic
diff --git a/fstar-helpers/Makefile.generic b/fstar-helpers/Makefile.generic
index 07aa2023c..820d219b5 100644
--- a/fstar-helpers/Makefile.generic
+++ b/fstar-helpers/Makefile.generic
@@ -174,6 +174,7 @@ 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 "check/${ANSI_COLOR_TONE}<MyModule.fst>  " 'Typecheck up to `MyModule.fst`'
 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'
@@ -216,6 +217,9 @@ run/%: | .depend $(HINT_DIR) $(CACHE_DIR)
 	${HEADER}
 	$(Q)$(FSTAR) $(OTHERFLAGS) $(@:run/%=%)
 
+check/%: | .depend $(HINT_DIR) $(CACHE_DIR) $(HACL_HOME)
+	$(Q)$(MAKE) "${CACHE_DIR}/$(@:check/%=%).checked"
+
 VERIFIED_CHECKED = $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
 ADMIT_CHECKED = $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ADMIT_MODULES)))
 
diff --git a/fstar-helpers/core-models/Cargo.toml b/fstar-helpers/core-models/Cargo.toml
index 3a4719ce4..b064e4061 100644
--- a/fstar-helpers/core-models/Cargo.toml
+++ b/fstar-helpers/core-models/Cargo.toml
@@ -12,6 +12,7 @@ publish = false
 [dependencies]
 rand = "0.9"
 hax-lib.workspace = true
+pastey = "0.1.0"
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)'] }
diff --git a/fstar-helpers/core-models/proofs/fstar/extraction/Makefile b/fstar-helpers/core-models/proofs/fstar/extraction/Makefile
new file mode 100644
index 000000000..02d380cf8
--- /dev/null
+++ b/fstar-helpers/core-models/proofs/fstar/extraction/Makefile
@@ -0,0 +1,2 @@
+include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.base
+
diff --git a/fstar-helpers/tactics/Tactics.Circuits.fst b/fstar-helpers/core-models/proofs/fstar/extraction/Tactics.Circuits.fst
similarity index 74%
rename from fstar-helpers/tactics/Tactics.Circuits.fst
rename to fstar-helpers/core-models/proofs/fstar/extraction/Tactics.Circuits.fst
index e28a4ba80..a53be8ba9 100644
--- a/fstar-helpers/tactics/Tactics.Circuits.fst
+++ b/fstar-helpers/core-models/proofs/fstar/extraction/Tactics.Circuits.fst
@@ -201,11 +201,12 @@ let mk_app_bs (t: term) (bs: list binder): Tac term
     mk_app t args
 
 /// Given a lemma `i1 -> ... -> iN -> Lemma (lhs == rhs)`, this tactic
-/// produces a lemma `i1 -> ... -> iN -> Lemma (lhs == rhs')` where
-/// `rhs'` is given by the tactic call `f <rhs>`.
-let map_lemma_rhs (f: term -> Tac term) (lemma: term) (d: dbg): Tac term
+/// produces a lemma `i1 -> ... -> iN -> ...extra_args... -> Lemma (lhs' == rhs')` where
+/// `lhs'` and `rhs'` are given by the tactic call `f <rhs>`.
+let edit_lemma (extra_args: list binder) (f_lhs g_rhs: term -> Tac term) (lemma: term) (d: dbg): Tac term
   = let typ = tc (top_env ()) lemma in
-    let inputs, comp = collect_arr_bs typ in
+    let inputs0, comp = collect_arr_bs typ in
+    let inputs = List.Tot.append inputs0 extra_args in
     let post =
       match inspect_comp comp with
       | C_Lemma pre post _ ->
@@ -221,18 +222,95 @@ let map_lemma_rhs (f: term -> Tac term) (lemma: term) (d: dbg): Tac term
       | _, [_; (lhs, _); (rhs, _)] -> (lhs, rhs)
       | _ -> d.fail "expected lhs == rhs"
     in
-    let lemma_body = mk_abs inputs (mk_app_bs lemma inputs) in
-    let post = mk_abs [post_bd] (mk_e_app (`eq2) [lhs; f rhs]) in
+    let lemma_body = mk_abs inputs (mk_app_bs lemma inputs0) in
+    let post = mk_abs [post_bd] (mk_e_app (`eq2) [f_lhs lhs; g_rhs rhs]) in
     let lemma_typ = mk_arr inputs (pack_comp (C_Lemma (`True) post (`[]))) in
     let lemma = pack (Tv_AscribedT lemma_body lemma_typ None false) in
     lemma
 
+/// Specialize a lemma `lhs == rhs` into `lhs x == rhs x` if possible.
+let specialize_lemma_apply (lemma: term): Tac (option term)
+  = let x: binder = fresh_binder_named "arg0" (`_) in
+    let f t: Tac _ = mk_e_app t [binder_to_term x] in
+    let h = edit_lemma [x] f f lemma (mk_dbg "") in
+    trytac (fun _ -> norm_term [] h)
+
+let rec flatten_options (l: list (option 't)): list 't
+  = match l with
+  | Some hd::tl -> hd::flatten_options tl
+  | None   ::tl -> flatten_options tl
+  | []         -> []
+
+/// Given a lemma `i1 -> ... -> iN -> Lemma (lhs == rhs)`, this tactic
+/// produces a lemma `i1 -> ... -> iN -> Lemma (lhs == rhs')` where
+/// `rhs'` is given by the tactic call `f <rhs>`.
+let map_lemma_rhs (f: term -> Tac term) (lemma: term) (d: dbg): Tac term
+  = edit_lemma [] (fun t -> t) f lemma d
+
 /// Helper to mark terms. This is an identity function.
 /// It is used to normalize terms selectively in two passes:
 ///  1. browse the term, mark the subterms you want to target
 ///  2. use `ctrl_rewrite`, doing something only for `mark_to_normalize_here #_ _` terms.
 private let mark_to_normalize_here #t (x: t): t = x
 
+/// Unapplies a function named `f_name` of arity `arity`.
+let mk_unapply_lemma (f_name: string) (arity: nat): Tac term =
+  let f = pack (Tv_FVar (pack_fv (explode_qn f_name))) in
+  let bds =
+    let rec aux (n: nat): Tac _ = match n with | 0 -> [] | _ -> fresh_binder (`_) :: aux (n - 1) in
+    aux arity
+  in
+  let applied_f = mk_app_bs f bds in
+  let rhs = norm_term [delta_only [f_name]] f in
+  let rhs = mk_app_bs rhs bds in
+  let post = mk_e_app (`(==)) [rhs; applied_f] in
+  let typ = mk_arr bds (pack_comp (C_Lemma (`True) (mk_abs [fresh_binder (`_)] post) (`[]))) in
+  let body = mk_abs bds (`()) in
+  let lemma = `(`#body <: `#typ) in
+  norm_term [] lemma
+
+let (let??) (x: option 'a) (f: 'a -> Tac (option 'b)): Tac (option 'b)
+  = match x with
+  | Some x -> f x
+  | None   -> None
+
+let expect_const_int (t: term): Tac (option int)
+  = match t with
+  | Tv_Const (C_Int n) -> Some n
+  | _ -> None
+
+let expect_fvar (f: string) (t: term): Tac (option unit)
+  = match t with
+  | Tv_UInst fv _ | Tv_FVar fv ->
+    if implode_qn (inspect_fv fv) = f
+    then Some ()
+    else None
+  | _ -> None
+
+let expect_app (f: string) (arity: nat) (t: term): Tac (option (l: list term {List.Tot.length l = arity}))
+  = let hd, args = collect_app t in
+    let?? () = expect_fvar f hd in
+    let args = List.Tot.map fst args in
+    if List.Tot.length args = arity
+    then let args: l: list term {List.Tot.length l = arity} = args in
+         Some args
+    else None
+
+let auto_unapply (arity: int) = ()
+
+let get_unapply_auto_lemmas ()
+  = filter_map
+        (fun f ->
+          let name = inspect_fv f in
+          let?? sg = lookup_typ (top_env ()) name in
+          let attrs = sigelt_attrs sg in
+          let?? [arity] = tryPick (expect_app (`%auto_unapply) 1) attrs in
+          let?? arity = expect_const_int arity in
+          if arity < 0 then fail "negative arity";
+          Some (mk_unapply_lemma (implode_qn name) arity)
+        )
+        (lookup_attr (`auto_unapply) (top_env ()))
+
 let flatten_circuit_aux
   (namespace_always_norm: list string)
   (lift_lemmas: list term) (simpl_lemmas: list term)
@@ -240,9 +318,19 @@ let flatten_circuit_aux
   d
   =
     d.sub "postprocess_tactic" (fun d ->
-        norm [primops; iota; delta_namespace ["Libcrux_intrinsics"]; zeta_full];
+        let namespaces_to_unfold =
+          let crate = match cur_module () with | crate::_ -> crate | _ -> fail "Empty module name" in
+          [crate; "Libcrux_intrinsics"]
+        in
+        d.dump ("will unfold namespaces [" ^ FStar.String.concat ";" namespaces_to_unfold ^ "]");
+        norm [primops; iota; delta_namespace namespaces_to_unfold; zeta_full];
         d.dump "definitions unfolded";
 
+
+        let simpl_lemmas = simpl_lemmas
+          `List.Tot.append` flatten_options (map specialize_lemma_apply simpl_lemmas)
+        in
+
         rewrite_with_lifts lift_lemmas simpl_lemmas d;
 
         let eta_match_lemmas =
@@ -278,10 +366,19 @@ let flatten_circuit_aux
         d.dump "after full normalization";
         set_smt_goals sgs;
 
+
+        d.print "unapply functions";
+        let unapply_lemmas = get_unapply_auto_lemmas () in
+        l_to_r unapply_lemmas;
+
+        let sgs = smt_goals () in
+        set_smt_goals [];
+        d.dump "after unapply";
+        set_smt_goals sgs;
+
         ()
     )
 
-
 /// `flatten_circuit` works on a goal `squash (c == ?u)` such that `c`
 /// is a circuit.
 ///
@@ -333,6 +430,15 @@ let flatten_circuit
         eta_match_lemmas d;
     trefl ()
   in
-  if lax_on ()
+  let disable_ext_flag =
+    // Disabling the flatten circuit tactic in lax/admit mode is usually a bad idea:
+    //  - if there are no checked file, dependencies will be checked in lax mode
+    //  - then, if we want to apply the circuit flattening tactic on a function `A.f`
+    //    that happens to use a function `B.g` and expect it to be flattened,
+    //    then `B.g` actually not be flattened since it was lax checked
+    FStar.Stubs.Tactics.V2.Builtins.ext_enabled "disable_circuit_norm"
+  in
+  let is_lax_on = lax_on () in
+  if is_lax_on && disable_ext_flag
   then trefl ()
   else run (mk_dbg "")
diff --git a/fstar-helpers/core-models/src/abstractions/bitvec.rs b/fstar-helpers/core-models/src/abstractions/bitvec.rs
index 8c60a9ad3..159f1a309 100644
--- a/fstar-helpers/core-models/src/abstractions/bitvec.rs
+++ b/fstar-helpers/core-models/src/abstractions/bitvec.rs
@@ -59,11 +59,11 @@ impl<const N: u64> core::ops::Index<u64> for BitVec<N> {
 
 /// Convert a bit slice into an unsigned number.
 #[hax_lib::exclude]
-fn u64_int_from_bit_slice(bits: &[Bit]) -> u64 {
+fn u128_int_from_bit_slice(bits: &[Bit]) -> u128 {
     bits.iter()
         .enumerate()
-        .map(|(i, bit)| u64::from(*bit) << i)
-        .sum::<u64>()
+        .map(|(i, bit)| u128::from(*bit) << i)
+        .sum::<u128>()
 }
 
 /// Convert a bit slice into a machine integer of type `T`.
@@ -72,14 +72,14 @@ fn int_from_bit_slice<T: TryFrom<i128> + MachineInteger + Copy>(bits: &[Bit]) ->
     debug_assert!(bits.len() <= T::bits() as usize);
     let result = if T::SIGNED {
         let is_negative = matches!(bits[T::bits() as usize - 1], Bit::One);
-        let s = u64_int_from_bit_slice(&bits[0..T::bits() as usize - 1]) as i128;
+        let s = u128_int_from_bit_slice(&bits[0..T::bits() as usize - 1]) as i128;
         if is_negative {
-            -2i128.pow(T::bits() - 1) + s
+            s + (-2i128).pow(T::bits() - 1)
         } else {
             s
         }
     } else {
-        u64_int_from_bit_slice(bits) as i128
+        u128_int_from_bit_slice(bits) as i128
     };
     let Ok(n) = result.try_into() else {
         // Conversion must succeed as `result` is guaranteed to be in range due to the bit-length check.
@@ -173,15 +173,15 @@ open FStar.Tactics.V2
 #push-options "--z3rlimit 80 --admit_smt_queries true"
 let bitvec_rewrite_lemma_128 (x: $:{BitVec<128>})
 : Lemma (x == mark_to_normalize (${BitVec::<128>::pointwise} x)) =
-    let a = x._0 in
-    let b = (${BitVec::<128>::pointwise} x)._0 in
+    let a = x._0._0 in
+    let b = (${BitVec::<128>::pointwise} x)._0._0 in
     assert_norm (FStar.FunctionalExtensionality.feq a b);
     extensionality' a b
 
 let bitvec_rewrite_lemma_256 (x: $:{BitVec<256>})
 : Lemma (x == mark_to_normalize (${BitVec::<256>::pointwise} x)) =
-    let a = x._0 in
-    let b = (${BitVec::<256>::pointwise} x)._0 in
+    let a = x._0._0 in
+    let b = (${BitVec::<256>::pointwise} x)._0._0 in
     assert_norm (FStar.FunctionalExtensionality.feq a b);
     extensionality' a b
 #pop-options
@@ -281,6 +281,15 @@ impl<const N: u64> BitVec<N> {
         }
         chunked_shift::<N, CHUNK, SHIFTS>(self, shl)
     }
+
+    /// Folds over the array, accumulating a result.
+    ///
+    /// # Arguments
+    /// * `init` - The initial value of the accumulator.
+    /// * `f` - A function combining the accumulator and each element.
+    pub fn fold<A>(&self, init: A, f: fn(A, Bit) -> A) -> A {
+        self.0.fold(init, f)
+    }
 }
 
 pub mod int_vec_interp {
@@ -300,43 +309,53 @@ pub mod int_vec_interp {
                 #[doc = concat!(stringify!($ty), " vectors of size ", stringify!($m))]
                 #[allow(non_camel_case_types)]
                 pub type $name = FunArray<$m, $ty>;
-                const _: ()  = {
-                    #[doc = concat!("Conversion from bit vectors of size ", stringify!($n), " to ", stringify!($ty), " vectors of size ", stringify!($m))]
-                    #[hax_lib::opaque]
-                    impl From<BitVec<$n>> for $name {
-                        fn from(bv: BitVec<$n>) -> Self {
-                            let vec: Vec<$ty> = bv.to_vec();
-                            Self::from_fn(|i| vec[i as usize])
+                pastey::paste! {
+                    const _: ()  = {
+                        #[hax_lib::opaque]
+                        impl BitVec<$n> {
+                            #[doc = concat!("Conversion from ", stringify!($ty), " vectors of size ", stringify!($m), "to  bit vectors of size ", stringify!($n))]
+                            pub fn [< from_ $name >](iv: $name) -> BitVec<$n> {
+                                let vec: Vec<$ty> = iv.as_vec();
+                                Self::from_slice(&vec[..], <$ty>::bits() as u64)
+                            }
+                            #[doc = concat!("Conversion from bit vectors of size ", stringify!($n), " to ", stringify!($ty), " vectors of size ", stringify!($m))]
+                            pub fn [< to_ $name >](bv: BitVec<$n>) -> $name {
+                                let vec: Vec<$ty> = bv.to_vec();
+                                $name::from_fn(|i| vec[i as usize])
+                            }
+                        }
+
+                        #[cfg(test)]
+                        impl From<BitVec<$n>> for $name {
+                            fn from(bv: BitVec<$n>) -> Self {
+                                BitVec::[< to_ $name >](bv)
+                            }
                         }
-                    }
-
-                    #[doc = concat!("Conversion from ", stringify!($ty), " vectors of size ", stringify!($m), "to  bit vectors of size ", stringify!($n))]
-                    #[hax_lib::opaque]
-                    impl From<$name> for BitVec<$n> {
-                        fn from(iv: $name) -> Self {
-                            let vec: Vec<$ty> = iv.as_vec();
-                            Self::from_slice(&vec[..], u64::MAX)
+                        #[cfg(test)]
+                        impl From<$name> for BitVec<$n> {
+                            fn from(iv: $name) -> Self {
+                                BitVec::[< from_ $name >](iv)
+                            }
                         }
-                    }
-
-
-                    #[doc = concat!("Lemma that asserts that applying ", stringify!(BitVec::<$n>::from)," and then ", stringify!($name::from), " is the identity.")]
-                    #[hax_lib::fstar::before("[@@ $SIMPLIFICATION_LEMMA ]")]
-                    #[hax_lib::opaque]
-                    #[hax_lib::lemma]
-                    #[hax_lib::fstar::smt_pat($name::from(BitVec::<$n>::from(x)))]
-                    pub fn lemma_cancel_iv(x: $name) -> Proof<{
-                        hax_lib::eq($name::from(BitVec::<$n>::from(x)), x)
-                    }> {}
-                    #[doc = concat!("Lemma that asserts that applying ", stringify!($name::from)," and then ", stringify!(BitVec::<$n>::from), " is the identity.")]
-                    #[hax_lib::fstar::before("[@@ $SIMPLIFICATION_LEMMA ]")]
-                    #[hax_lib::opaque]
-                    #[hax_lib::lemma]
-                    #[hax_lib::fstar::smt_pat(BitVec::<$n>::from($name::from(x)))]
-                    pub fn lemma_cancel_bv(x: BitVec<$n>) -> Proof<{
-                        hax_lib::eq(BitVec::<$n>::from($name::from(x)), x)
-                    }> {}
-                };
+
+                        #[doc = concat!("Lemma that asserts that applying ", stringify!(BitVec::<$n>::from)," and then ", stringify!($name::from), " is the identity.")]
+                        #[hax_lib::fstar::before("[@@ $SIMPLIFICATION_LEMMA ]")]
+                        #[hax_lib::opaque]
+                        #[hax_lib::lemma]
+                        #[hax_lib::fstar::smt_pat(BitVec::[< to_ $name >](BitVec::[<from_ $name>](x)))]
+                        pub fn lemma_cancel_iv(x: $name) -> Proof<{
+                            hax_lib::eq(BitVec::[< to_ $name >](BitVec::[<from_ $name>](x)), x)
+                        }> {}
+                        #[doc = concat!("Lemma that asserts that applying ", stringify!($name::from)," and then ", stringify!(BitVec::<$n>::from), " is the identity.")]
+                        #[hax_lib::fstar::before("[@@ $SIMPLIFICATION_LEMMA ]")]
+                        #[hax_lib::opaque]
+                        #[hax_lib::lemma]
+                        #[hax_lib::fstar::smt_pat(BitVec::[< from_ $name >](BitVec::[<to_ $name>](x)))]
+                        pub fn lemma_cancel_bv(x: BitVec<$n>) -> Proof<{
+                            hax_lib::eq(BitVec::[< from_ $name >](BitVec::[<to_ $name>](x)), x)
+                        }> {}
+                    };
+                }
             )*
         };
     }
@@ -347,7 +366,10 @@ pub mod int_vec_interp {
     // We will need more such interpreations in the future to handle more avx2
     // intrinsics (e.g. `_mm256_add_epi16` works on 16 bits integers, not on i32
     // or i64).
-    interpretations!(256; i32x8 [i32; 8], i64x4 [i64; 4]);
+    interpretations!(256; i32x8 [i32; 8], i64x4 [i64; 4], i16x16 [i16; 16], i128x2 [i128; 2], i8x32 [i8; 32],
+		     u32x8 [u32; 8], u64x4 [u64; 4], u16x16 [u16; 16]);
+    interpretations!(128; i32x4 [i32; 4], i64x2 [i64; 2], i16x8 [i16; 8], i128x1 [i128; 1], i8x16 [i8; 16],
+		     u32x4 [u32; 4], u64x2 [u64; 2], u16x8 [u16; 8]);
 
     impl i64x4 {
         pub fn into_i32x8(self) -> i32x8 {
@@ -358,6 +380,16 @@ pub mod int_vec_interp {
         }
     }
 
+    impl i32x8 {
+        pub fn into_i64x4(self) -> i64x4 {
+            i64x4::from_fn(|i| {
+                let low = *self.get(2 * i) as u32 as u64;
+                let high = *self.get(2 * i + 1) as i32 as i64;
+                (high << 32) | low as i64
+            })
+        }
+    }
+
     impl From<i64x4> for i32x8 {
         fn from(vec: i64x4) -> Self {
             vec.into_i32x8()
@@ -369,8 +401,50 @@ pub mod int_vec_interp {
     #[hax_lib::fstar::before("[@@ $SIMPLIFICATION_LEMMA ]")]
     #[hax_lib::opaque]
     #[hax_lib::lemma]
-    fn lemma_rewrite_i64x4_bv_i32x8(
+    pub fn lemma_rewrite_i64x4_bv_i32x8(
         bv: i64x4,
-    ) -> Proof<{ hax_lib::eq(i32x8::from(BitVec::<256>::from(bv)), bv.into_i32x8()) }> {
+    ) -> Proof<{ hax_lib::eq(BitVec::to_i32x8(BitVec::from_i64x4(bv)), bv.into_i32x8()) }> {
+    }
+
+    /// Lemma stating that converting an `i64x4` vector to a `BitVec<256>` and then into an `i32x8`
+    /// yields the same result as directly converting the `i64x4` into an `i32x8`.
+    #[hax_lib::fstar::before("[@@ $SIMPLIFICATION_LEMMA ]")]
+    #[hax_lib::opaque]
+    #[hax_lib::lemma]
+    pub fn lemma_rewrite_i32x8_bv_i64x4(
+        bv: i32x8,
+    ) -> Proof<{ hax_lib::eq(BitVec::to_i64x4(BitVec::from_i32x8(bv)), bv.into_i64x4()) }> {
+    }
+
+    /// Normalize `from` calls that convert from one type to itself
+    #[hax_lib::fstar::replace(
+        r#"
+        [@@ $SIMPLIFICATION_LEMMA ]
+        let lemma (t: Type) (i: Core.Convert.t_From t t) (x: t)
+            : Lemma (Core.Convert.f_from #t #t #i x == (norm [primops; iota; delta; zeta] i.f_from) x)
+            = ()
+    "#
+    )]
+    const _: () = ();
+
+    #[cfg(test)]
+    mod direct_convertions_tests {
+        use super::*;
+        use crate::helpers::test::HasRandom;
+
+        #[test]
+        fn into_i32x8() {
+            for _ in 0..10000 {
+                let x: i64x4 = i64x4::random();
+                let y = x.into_i32x8();
+                assert_eq!(BitVec::from_i64x4(x), BitVec::from_i32x8(y));
+            }
+        }
+        #[test]
+        fn into_i64x4() {
+            let x: i32x8 = i32x8::random();
+            let y = x.into_i64x4();
+            assert_eq!(BitVec::from_i32x8(x), BitVec::from_i64x4(y));
+        }
     }
 }
diff --git a/fstar-helpers/core-models/src/abstractions/funarr.rs b/fstar-helpers/core-models/src/abstractions/funarr.rs
index 0853bf38a..71e3c9736 100644
--- a/fstar-helpers/core-models/src/abstractions/funarr.rs
+++ b/fstar-helpers/core-models/src/abstractions/funarr.rs
@@ -9,28 +9,28 @@
 
 #[hax_lib::fstar::replace(
     r#"
-open FStar.FunctionalExtensionality    
-type t_FunArray (n: u64) (t: Type0) = i:u64 {v i < v n} ^-> t
+open FStar.FunctionalExtensionality
+noeq type t_FunArray (n: u64) (t: Type0) = | FunArray : (i:u64 {v i < v n} ^-> t) -> t_FunArray n t
 
 let ${FunArray::<0, ()>::get} (v_N: u64) (#v_T: Type0) (self: t_FunArray v_N v_T) (i: u64 {v i < v v_N}) : v_T = 
-    self i
+    self._0 i
 
 let ${FunArray::<0, ()>::from_fn::<fn(u64)->()>}
     (v_N: u64)
     (#v_T: Type0)
     (f: (i: u64 {v i < v v_N}) -> v_T)
-    : t_FunArray v_N v_T = on (i: u64 {v i < v v_N}) f
+    : t_FunArray v_N v_T = FunArray (on (i: u64 {v i < v v_N}) f)
 
-let ${FunArray::<0, ()>::as_vec} n #t (self: t_FunArray n t) = FStar.Seq.init (v n) (fun i -> self (mk_u64 i))
+let ${FunArray::<0, ()>::as_vec} n #t (self: t_FunArray n t) = FStar.Seq.init (v n) (fun i -> self._0 (mk_u64 i))
 
 let rec ${FunArray::<0, ()>::fold::<()>} n #t #a (arr: t_FunArray n t) (init: a) (f: a -> t -> a): Tot a (decreases (v n)) = 
     match n with
     | MkInt 0 -> init
-    | MkInt n -> 
-        let acc: a = f init (arr (mk_u64 0)) in 
+    | MkInt n ->
+        let acc: a = f init (arr._0 (mk_u64 0)) in
         let n = MkInt (n - 1) in
         ${FunArray::<0, ()>::fold::<()>}  n #t #a
-                      (${FunArray::<0, ()>::from_fn::<fn(u64)->()>} n (fun i -> arr (i +. mk_u64 1)))
+                      (${FunArray::<0, ()>::from_fn::<fn(u64)->()>} n (fun i -> arr._0 (i +. mk_u64 1)))
                       acc f
 "#
 )]
@@ -43,7 +43,7 @@ impl<const N: u64, T> FunArray<N, T> {
     pub fn get(&self, i: u64) -> &T {
         self.0[i as usize].as_ref().unwrap()
     }
-    /// Constructor for FunArray. `FunArray::<N,T>::from_fn` constructs a FunArray out of a function that takes usizes smaller than `N` and produces values of type T.
+    /// Constructor for FunArray. `FunArray<N,T>::from_fn` constructs a funarray out of a function that takes usizes smaller than `N` and produces an element of type T.
     pub fn from_fn<F: Fn(u64) -> T>(f: F) -> Self {
         // let vec = (0..N).map(f).collect();
         let arr = core::array::from_fn(|i| {
diff --git a/fstar-helpers/core-models/src/abstractions/mod.rs b/fstar-helpers/core-models/src/abstractions/mod.rs
index 4408679e0..c67a17bba 100644
--- a/fstar-helpers/core-models/src/abstractions/mod.rs
+++ b/fstar-helpers/core-models/src/abstractions/mod.rs
@@ -1,5 +1,5 @@
 //! This module provides abstractions that are useful for writting
-//! specifications in core_models. Currently it provides two abstractions: bits and
+//! specifications in minicore. Currently it provides two abstractions: bits and
 //! bit vectors.
 //!
 //! # Examples
diff --git a/fstar-helpers/core-models/src/core_arch/x86.rs b/fstar-helpers/core-models/src/core_arch/x86.rs
index 11d6840d1..aa4740856 100644
--- a/fstar-helpers/core-models/src/core_arch/x86.rs
+++ b/fstar-helpers/core-models/src/core_arch/x86.rs
@@ -50,7 +50,7 @@
 //! ```
 //!
 //! ### (step 4) Integer‑Vector Interpretation & Lift Lemma (if needed)
-//! In `core_models::core_arch::x86::interpretations::int_vec`, we add the following model:
+//! In `minicore::core_arch::x86::interpretations::int_vec`, we add the following model:
 //!
 //! ```compile_fail
 //! pub fn _mm256_mul_epi32(x: i32x8, y: i32x8) -> i64x4 {
@@ -58,7 +58,7 @@
 //! }
 //! ```
 //!
-//! And a lift lemma in `core_models::core_arch::x86::interpretations::int_vec::lemmas`:
+//! And a lift lemma in `minicore::core_arch::x86::interpretations::int_vec::lemmas`:
 //! ```compile_fail
 //! mk_lift_lemma!(
 //!     _mm256_mul_epi32(x: __m256i, y: __m256i) ==
@@ -67,7 +67,7 @@
 //! ```
 //!
 //! ### (step 5) Unit Test
-//! In `core_models::core_arch::x86::interpretations::int_vec::tests`:
+//! In `minicore::core_arch::x86::interpretations::int_vec::tests`:
 //! ```compile_fail
 //! mk!(_mm256_mul_epi32(x: BitVec, y: BitVec));
 //! ```
@@ -86,16 +86,13 @@ pub(crate) mod upstream {
     pub use core::arch::x86_64::*;
 }
 
-pub mod opaque;
-pub use opaque::*;
-
 /// Conversions impls between `BitVec<N>` and `__mNi` types.
 #[hax_lib::exclude]
 #[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
 mod conversions {
     use super::upstream::{
-        __m128i, __m256i, _mm256_loadu_si256, _mm256_storeu_si256, _mm_loadu_si128,
-        _mm_storeu_si128,
+        __m128i, __m256, __m256i, _mm256_castps_si256, _mm256_castsi256_ps, _mm256_loadu_si256,
+        _mm256_storeu_si256, _mm_loadu_si128, _mm_storeu_si128,
     };
     use super::BitVec;
 
@@ -105,6 +102,12 @@ mod conversions {
             unsafe { _mm256_loadu_si256(bv.as_ptr() as *const _) }
         }
     }
+    impl From<BitVec<256>> for __m256 {
+        fn from(bv: BitVec<256>) -> __m256 {
+            let bv: &[u8] = &bv.to_vec()[..];
+            unsafe { _mm256_castsi256_ps(_mm256_loadu_si256(bv.as_ptr() as *const _)) }
+        }
+    }
 
     impl From<BitVec<128>> for __m128i {
         fn from(bv: BitVec<128>) -> __m128i {
@@ -123,6 +126,16 @@ mod conversions {
         }
     }
 
+    impl From<__m256> for BitVec<256> {
+        fn from(vec: __m256) -> BitVec<256> {
+            let mut v = [0u8; 32];
+            unsafe {
+                _mm256_storeu_si256(v.as_mut_ptr() as *mut _, _mm256_castps_si256(vec));
+            }
+            BitVec::from_slice(&v[..], 8)
+        }
+    }
+
     impl From<__m128i> for BitVec<128> {
         fn from(vec: __m128i) -> BitVec<128> {
             let mut v = [0u8; 16];
@@ -142,10 +155,6 @@ mod conversions {
 )]
 const _: () = {};
 
-#[allow(non_camel_case_types)]
-#[hax_lib::opaque]
-pub struct __m256(());
-
 /// 256-bit wide integer vector type.
 /// Models `core::arch::x86::__m256i` or `core::arch::x86_64::__m256i` (the __m256i type defined by Intel, representing a 256-bit SIMD register).
 #[allow(non_camel_case_types)]
@@ -156,6 +165,11 @@ pub type __m256i = BitVec<256>;
 #[allow(non_camel_case_types)]
 pub type __m128i = BitVec<128>;
 
+/// 256-bit wide vector type, which can be interpreted as 8 32 bit floating point values.
+/// Models `core::arch::x86::__m256` or `core::arch::x86_64::__m256`, but since we do not have use and fully support floating points yet, it is treated the same as __m256i.
+#[allow(non_camel_case_types)]
+pub type __m256 = __m256i;
+
 pub use ssse3::*;
 pub mod ssse3 {
     use super::*;
@@ -167,6 +181,19 @@ pub mod ssse3 {
 }
 pub use sse2::*;
 pub mod sse2 {
+    /// This intrinsics is not extracted via hax currently since it cannot hanlde raw pointers.
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_loadu_si128&ig_expand=4106)
+    #[hax_lib::exclude]
+    pub unsafe fn _mm_loadu_si128(_mem_addr: *const __m128i) -> __m128i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_packs_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm_packs_epi16(_: __m128i, _: __m128i) -> __m128i {
+        unimplemented!()
+    }
+
     use super::*;
     #[hax_lib::opaque]
     pub fn _mm_set_epi8(
@@ -189,10 +216,121 @@ pub mod sse2 {
     ) -> __m128i {
         todo!()
     }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_set1_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm_set1_epi16(_: i16) -> __m128i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_set_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm_set_epi32(_: i32, _: i32, _: i32, _: i32) -> __m128i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_add_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm_add_epi16(_: __m128i, _: __m128i) -> __m128i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_sub_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm_sub_epi16(_: __m128i, _: __m128i) -> __m128i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_mullo_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm_mullo_epi16(_: __m128i, _: __m128i) -> __m128i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_mulhi_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm_mulhi_epi16(_: __m128i, _: __m128i) -> __m128i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_srli_epi64)
+    #[hax_lib::opaque]
+    pub fn _mm_srli_epi64<const IMM8: i32>(_: __m128i) -> __m128i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_movemask_epi8)
+    #[hax_lib::opaque]
+    pub fn _mm_movemask_epi8(_: __m128i) -> i32 {
+        unimplemented!()
+    }
 }
 
 pub use avx::*;
 pub mod avx {
+    /// This intrinsics is not extracted via hax currently since it cannot hanlde raw pointers.
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_storeu_si256)
+    #[hax_lib::exclude]
+    pub unsafe fn _mm256_storeu_si256(_mem_addr: *mut __m256i, _a: __m256i) {
+        unimplemented!()
+    }
+
+    /// This intrinsics is not extracted via hax currently since it cannot hanlde raw pointers.
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_loadu_si256)
+    #[hax_lib::exclude]
+    pub unsafe fn _mm256_loadu_si256(_mem_addr: *const __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_set1_epi64x)
+    #[hax_lib::opaque]
+    pub fn _mm256_set1_epi64x(_: i64) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_set_epi64x)
+    #[hax_lib::opaque]
+    pub fn _mm256_set_epi64x(_: i64, _: i64, _: i64, _: i64) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_blendv_ps)
+    #[hax_lib::opaque]
+    pub fn _mm256_blendv_ps(_: __m256, _: __m256, _: __m256) -> __m256 {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_castsi128_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_castsi128_si256(_: __m128i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_testz_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_testz_si256(_: __m256i, _: __m256i) -> i32 {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_castsi256_ps)
+    #[hax_lib::opaque]
+    pub fn _mm256_castsi256_ps(_: __m256i) -> __m256 {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_castps_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_castps_si256(_: __m256) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_movemask_ps)
+    #[hax_lib::opaque]
+    pub fn _mm256_movemask_ps(_: __m256) -> i32 {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_setzero_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_setzero_si256() -> __m256i {
+        BitVec::from_fn(|_| Bit::Zero)
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_set_m128i)
+    #[hax_lib::opaque]
+    pub fn _mm256_set_m128i(hi: __m128i, lo: __m128i) -> __m256i {
+        BitVec::from_fn(|i| if i < 128 { lo[i] } else { hi[i - 128] })
+    }
+
     pub use super::*;
     pub fn _mm256_castsi256_si128(vector: __m256i) -> __m128i {
         BitVec::from_fn(|i| vector[i])
@@ -284,31 +422,231 @@ pub mod avx {
     ) -> __m256i {
         todo!()
     }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_set1_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_set1_epi16(_: i16) -> __m256i {
+        unimplemented!()
+    }
 }
 pub use avx2::*;
 pub mod avx2 {
     use super::*;
 
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_blend_epi32)
     #[hax_lib::opaque]
     pub fn _mm256_blend_epi32<const IMM8: i32>(_: __m256i, _: __m256i) -> __m256i {
         unimplemented!()
     }
-
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_shuffle_epi32)
     #[hax_lib::opaque]
     pub fn _mm256_shuffle_epi32<const MASK: i32>(_: __m256i) -> __m256i {
         unimplemented!()
     }
-
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_sub_epi32)
     #[hax_lib::opaque]
     pub fn _mm256_sub_epi32(_: __m256i, _: __m256i) -> __m256i {
         unimplemented!()
     }
-
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_mul_epi32)
     #[hax_lib::opaque]
     pub fn _mm256_mul_epi32(_: __m256i, _: __m256i) -> __m256i {
         unimplemented!()
     }
 
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_add_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_add_epi16(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_madd_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_madd_epi16(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_add_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_add_epi32(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_add_epi64)
+    #[hax_lib::opaque]
+    pub fn _mm256_add_epi64(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_abs_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_abs_epi32(_: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_sub_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_sub_epi16(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_cmpgt_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_cmpgt_epi16(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_cmpgt_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_cmpgt_epi32(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_cmpeq_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_cmpeq_epi32(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_sign_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_sign_epi32(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_mullo_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_mullo_epi32(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_mulhi_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_mulhi_epi16(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_mul_epu32)
+    #[hax_lib::opaque]
+    pub fn _mm256_mul_epu32(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_and_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_and_si256(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_or_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_or_si256(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_xor_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_xor_si256(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_srai_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_srai_epi16<const IMM8: i32>(_: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_srai_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_srai_epi32<const IMM8: i32>(_: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_srli_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_srli_epi16<const IMM8: i32>(_: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_srli_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_srli_epi32<const IMM8: i32>(_: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_slli_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_slli_epi32<const IMM8: i32>(_: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_permute4x64_epi64)
+    #[hax_lib::opaque]
+    pub fn _mm256_permute4x64_epi64<const IMM8: i32>(_: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_unpackhi_epi64)
+    #[hax_lib::opaque]
+    pub fn _mm256_unpackhi_epi64(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_unpacklo_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_unpacklo_epi32(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_unpackhi_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_unpackhi_epi32(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_cvtepi16_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_cvtepi16_epi32(_: __m128i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_packs_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm256_packs_epi32(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_inserti128_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_inserti128_si256<const IMM8: i32>(_: __m256i, _: __m128i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_blend_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_blend_epi16<const IMM8: i32>(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_srlv_epi64)
+    #[hax_lib::opaque]
+    pub fn _mm256_srlv_epi64(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_sllv_epi32)
+    #[hax_lib::opaque]
+    pub fn _mm_sllv_epi32(_: __m128i, _: __m128i) -> __m128i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_slli_epi64)
+    #[hax_lib::opaque]
+    pub fn _mm256_slli_epi64<const IMM8: i32>(_: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_bsrli_epi128)
+    /// NOTE: the bsrli here is different from intel specification. In the intel specification, if an IMM8 is given whose first 8 bits are higher than 15, it fixes it to 16.
+    /// However, the Rust implementation erroneously takes the input modulo 16. Thus, instead of shifting by 16 bits at an input of 16, it shifts by 0.
+    /// We are currently modelling the Rust implementation.
+    #[hax_lib::opaque]
+    pub fn _mm256_bsrli_epi128<const IMM8: i32>(_: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_andnot_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_andnot_si256(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_unpacklo_epi64)
+    #[hax_lib::opaque]
+    pub fn _mm256_unpacklo_epi64(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_permute2x128_si256)
+    #[hax_lib::opaque]
+    pub fn _mm256_permute2x128_si256<const IMM8: i32>(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_storeu_si128)
     #[hax_lib::exclude]
     pub fn _mm_storeu_si128(output: *mut __m128i, a: __m128i) {
         // This is equivalent to `*output = a`
@@ -318,41 +656,39 @@ pub mod avx2 {
             *(output.as_mut().unwrap()) = BitVec::from_slice(&out, 8);
         }
     }
-
-    #[hax_lib::requires(SHIFT_BY >= 0 && SHIFT_BY < 16)]
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_slli_epi16)
     pub fn _mm256_slli_epi16<const SHIFT_BY: i32>(vector: __m256i) -> __m256i {
         vector.chunked_shift::<16, 16>(FunArray::from_fn(|_| SHIFT_BY as i128))
     }
-
-    #[hax_lib::requires(SHIFT_BY >= 0 && SHIFT_BY < 64)]
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_srli_epi64)
     pub fn _mm256_srli_epi64<const SHIFT_BY: i32>(vector: __m256i) -> __m256i {
         vector.chunked_shift::<64, 4>(FunArray::from_fn(|_| -(SHIFT_BY as i128)))
     }
-
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_mullo_epi16)
     #[hax_lib::opaque]
     pub fn _mm256_mullo_epi16(_vector: __m256i, _shifts: __m256i) -> __m256i {
         todo!()
     }
-
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_sllv_epi32)
     #[hax_lib::opaque]
     pub fn _mm256_sllv_epi32(vector: __m256i, counts: __m256i) -> __m256i {
         extra::mm256_sllv_epi32_u32_array(vector, counts.to_vec().try_into().unwrap())
     }
-
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_srlv_epi32)
     #[hax_lib::opaque]
     pub fn _mm256_srlv_epi32(vector: __m256i, counts: __m256i) -> __m256i {
         extra::mm256_srlv_epi32_u32_array(vector, counts.to_vec().try_into().unwrap())
     }
-
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_permutevar8x32_epi32)
     #[hax_lib::opaque]
     pub fn _mm256_permutevar8x32_epi32(a: __m256i, b: __m256i) -> __m256i {
         extra::mm256_permutevar8x32_epi32_u32_array(a, b.to_vec().try_into().unwrap())
     }
-
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_extracti128_si256)
     pub fn _mm256_extracti128_si256<const IMM8: i32>(vector: __m256i) -> __m128i {
         BitVec::from_fn(|i| vector[i + if IMM8 == 0 { 0 } else { 128 }])
     }
-
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_shuffle_epi8)
     #[hax_lib::opaque]
     pub fn _mm256_shuffle_epi8(vector: __m256i, indexes: __m256i) -> __m256i {
         let indexes = indexes.to_vec().try_into().unwrap();
diff --git a/fstar-helpers/core-models/src/core_arch/x86/interpretations.rs b/fstar-helpers/core-models/src/core_arch/x86/interpretations.rs
index e952a72b1..1cadf4c5e 100644
--- a/fstar-helpers/core-models/src/core_arch/x86/interpretations.rs
+++ b/fstar-helpers/core-models/src/core_arch/x86/interpretations.rs
@@ -1,7 +1,11 @@
 pub mod int_vec {
     //! Provides a machine integer vectors intepretation for AVX2 intrinsics.
 
-    use crate::abstractions::{bitvec::int_vec_interp::*, funarr::FunArray};
+    use crate::abstractions::{
+        bit::Bit,
+        bitvec::{int_vec_interp::*, BitVec},
+        funarr::FunArray,
+    };
     #[allow(unused)]
     use crate::core_arch::x86;
 
@@ -9,8 +13,12 @@ pub mod int_vec {
         i32x8::from_fn(|_| x)
     }
 
+    pub fn i32_extended64_mul(x: i32, y: i32) -> i64 {
+        (x as i64) * (y as i64)
+    }
+
     pub fn _mm256_mul_epi32(x: i32x8, y: i32x8) -> i64x4 {
-        i64x4::from_fn(|i| (x[i * 2] as i64) * (y[i * 2] as i64))
+        i64x4::from_fn(|i| i32_extended64_mul(x[i * 2], y[i * 2]))
     }
     pub fn _mm256_sub_epi32(x: i32x8, y: i32x8) -> i32x8 {
         i32x8::from_fn(|i| x[i].wrapping_sub(y[i]))
@@ -28,18 +36,509 @@ pub mod int_vec {
     }
 
     pub fn _mm256_blend_epi32<const CONTROL: i32>(x: i32x8, y: i32x8) -> i32x8 {
-        FunArray::from_fn(|i| if (CONTROL >> i) % 2 == 0 { x[i] } else { y[i] })
+        i32x8::from_fn(|i| if (CONTROL >> i) % 2 == 0 { x[i] } else { y[i] })
+    }
+
+    pub fn _mm256_setzero_si256() -> BitVec<256> {
+        BitVec::from_fn(|_| Bit::Zero)
+    }
+    pub fn _mm256_set_m128i(hi: BitVec<128>, lo: BitVec<128>) -> BitVec<256> {
+        BitVec::from_fn(|i| if i < 128 { lo[i] } else { hi[i - 128] })
+    }
+
+    pub fn _mm256_set1_epi16(a: i16) -> i16x16 {
+        i16x16::from_fn(|_| a)
+    }
+
+    pub fn _mm_set1_epi16(a: i16) -> i16x8 {
+        i16x8::from_fn(|_| a)
+    }
+
+    pub fn _mm_set_epi32(e3: i32, e2: i32, e1: i32, e0: i32) -> i32x4 {
+        i32x4::from_fn(|i| match i {
+            0 => e0,
+            1 => e1,
+            2 => e2,
+            3 => e3,
+            _ => unreachable!(),
+        })
+    }
+    pub fn _mm_add_epi16(a: i16x8, b: i16x8) -> i16x8 {
+        i16x8::from_fn(|i| a[i].wrapping_add(b[i]))
+    }
+    pub fn _mm256_add_epi16(a: i16x16, b: i16x16) -> i16x16 {
+        i16x16::from_fn(|i| a[i].wrapping_add(b[i]))
+    }
+
+    pub fn _mm256_add_epi32(a: i32x8, b: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| a[i].wrapping_add(b[i]))
+    }
+
+    pub fn _mm256_add_epi64(a: i64x4, b: i64x4) -> i64x4 {
+        i64x4::from_fn(|i| a[i].wrapping_add(b[i]))
+    }
+
+    pub fn _mm256_abs_epi32(a: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| {
+            // See `_mm256_abs_epi32_min`: if the item is `i32::MIN`, the intrinsics returns `i32::MIN`, untouched.
+            if a[i] == i32::MIN {
+                a[i]
+            } else {
+                a[i].abs()
+            }
+        })
+    }
+
+    pub fn _mm256_sub_epi16(a: i16x16, b: i16x16) -> i16x16 {
+        i16x16::from_fn(|i| a[i].wrapping_sub(b[i]))
+    }
+
+    pub fn _mm_sub_epi16(a: i16x8, b: i16x8) -> i16x8 {
+        i16x8::from_fn(|i| a[i].wrapping_sub(b[i]))
+    }
+
+    pub fn _mm_mullo_epi16(a: i16x8, b: i16x8) -> i16x8 {
+        i16x8::from_fn(|i| (a[i].overflowing_mul(b[i]).0))
+    }
+
+    pub fn _mm256_cmpgt_epi16(a: i16x16, b: i16x16) -> i16x16 {
+        i16x16::from_fn(|i| if a[i] > b[i] { -1 } else { 0 })
+    }
+
+    pub fn _mm256_cmpgt_epi32(a: i32x8, b: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| if a[i] > b[i] { -1 } else { 0 })
+    }
+
+    pub fn _mm256_cmpeq_epi32(a: i32x8, b: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| if a[i] == b[i] { -1 } else { 0 })
+    }
+
+    pub fn _mm256_sign_epi32(a: i32x8, b: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| {
+            if b[i] < 0 {
+                // See `_mm256_sign_epi32_min`: if the item is `i32::MIN`, the intrinsics returns `i32::MIN`, untouched.
+                if a[i] == i32::MIN {
+                    a[i]
+                } else {
+                    -a[i]
+                }
+            } else if b[i] > 0 {
+                a[i]
+            } else {
+                0
+            }
+        })
+    }
+
+    pub fn _mm256_castsi256_ps(a: BitVec<256>) -> BitVec<256> {
+        a
+    }
+
+    pub fn _mm256_castps_si256(a: BitVec<256>) -> BitVec<256> {
+        a
+    }
+
+    pub fn _mm256_movemask_ps(a: i32x8) -> i32 {
+        let a0: i32 = if a[0] < 0 { 1 } else { 0 };
+        let a1 = if a[1] < 0 { 2 } else { 0 };
+        let a2 = if a[2] < 0 { 4 } else { 0 };
+        let a3 = if a[3] < 0 { 8 } else { 0 };
+        let a4 = if a[4] < 0 { 16 } else { 0 };
+        let a5 = if a[5] < 0 { 32 } else { 0 };
+        let a6 = if a[6] < 0 { 64 } else { 0 };
+        let a7 = if a[7] < 0 { 128 } else { 0 };
+        a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7
+    }
+
+    #[hax_lib::fstar::options("--z3rlimit 200")]
+    pub fn _mm_mulhi_epi16(a: i16x8, b: i16x8) -> i16x8 {
+        i16x8::from_fn(|i| (((a[i] as i32) * (b[i] as i32) >> 16) as i16))
+    }
+
+    pub fn _mm256_mullo_epi32(a: i32x8, b: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| (a[i].overflowing_mul(b[i]).0))
+    }
+
+    #[hax_lib::fstar::verification_status(lax)]
+    pub fn _mm256_mulhi_epi16(a: i16x16, b: i16x16) -> i16x16 {
+        i16x16::from_fn(|i| (((a[i] as i32) * (b[i] as i32) >> 16) as i16))
+    }
+
+    pub fn _mm256_mul_epu32(a: u32x8, b: u32x8) -> u64x4 {
+        u64x4::from_fn(|i| (a[i * 2] as u64) * (b[i * 2] as u64))
+    }
+
+    pub fn _mm256_and_si256(a: BitVec<256>, b: BitVec<256>) -> BitVec<256> {
+        BitVec::from_fn(|i| match (a[i], b[i]) {
+            (Bit::One, Bit::One) => Bit::One,
+            _ => Bit::Zero,
+        })
+    }
+
+    pub fn _mm256_or_si256(a: BitVec<256>, b: BitVec<256>) -> BitVec<256> {
+        BitVec::from_fn(|i| match (a[i], b[i]) {
+            (Bit::Zero, Bit::Zero) => Bit::Zero,
+            _ => Bit::One,
+        })
+    }
+
+    pub fn _mm256_testz_si256(a: BitVec<256>, b: BitVec<256>) -> i32 {
+        let c = BitVec::<256>::from_fn(|i| match (a[i], b[i]) {
+            (Bit::One, Bit::One) => Bit::One,
+            _ => Bit::Zero,
+        });
+        let all_zero = c.fold(true, |acc, bit| acc && bit == Bit::Zero);
+        if all_zero {
+            1
+        } else {
+            0
+        }
+    }
+
+    pub fn _mm256_xor_si256(a: BitVec<256>, b: BitVec<256>) -> BitVec<256> {
+        BitVec::from_fn(|i| match (a[i], b[i]) {
+            (Bit::Zero, Bit::Zero) => Bit::Zero,
+            (Bit::One, Bit::One) => Bit::Zero,
+            _ => Bit::One,
+        })
+    }
+
+    pub fn _mm256_srai_epi16<const IMM8: i32>(a: i16x16) -> i16x16 {
+        i16x16::from_fn(|i| {
+            let imm8 = IMM8.rem_euclid(256);
+            if imm8 > 15 {
+                if a[i] < 0 {
+                    -1
+                } else {
+                    0
+                }
+            } else {
+                a[i] >> imm8
+            }
+        })
+    }
+
+    pub fn _mm256_srai_epi32<const IMM8: i32>(a: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| {
+            let imm8 = IMM8.rem_euclid(256);
+            if imm8 > 31 {
+                if a[i] < 0 {
+                    -1
+                } else {
+                    0
+                }
+            } else {
+                a[i] >> imm8
+            }
+        })
+    }
+
+    pub fn _mm256_srli_epi16<const IMM8: i32>(a: i16x16) -> i16x16 {
+        i16x16::from_fn(|i| {
+            let imm8 = IMM8.rem_euclid(256);
+            if imm8 > 15 {
+                0
+            } else {
+                ((a[i] as u16) >> imm8) as i16
+            }
+        })
+    }
+
+    pub fn _mm256_srli_epi32<const IMM8: i32>(a: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| {
+            let imm8 = IMM8.rem_euclid(256);
+            if imm8 > 31 {
+                0
+            } else {
+                ((a[i] as u32) >> imm8) as i32
+            }
+        })
+    }
+
+    pub fn _mm_srli_epi64<const IMM8: i32>(a: i64x2) -> i64x2 {
+        i64x2::from_fn(|i| {
+            let imm8 = IMM8.rem_euclid(256);
+            if imm8 > 63 {
+                0
+            } else {
+                ((a[i] as u64) >> imm8) as i64
+            }
+        })
+    }
+
+    pub fn _mm256_slli_epi32<const IMM8: i32>(a: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| {
+            let imm8 = IMM8.rem_euclid(256);
+            if imm8 > 31 {
+                0
+            } else {
+                ((a[i] as u32) << imm8) as i32
+            }
+        })
+    }
+
+    pub fn _mm256_permute4x64_epi64<const IMM8: i32>(a: i64x4) -> i64x4 {
+        let indexes: FunArray<4, u64> = FunArray::from_fn(|i| ((IMM8 >> i * 2) % 4) as u64);
+        i64x4::from_fn(|i| a[indexes[i]])
+    }
+
+    pub fn _mm256_unpackhi_epi64(a: i64x4, b: i64x4) -> i64x4 {
+        i64x4::from_fn(|i| match i {
+            0 => a[1],
+            1 => b[1],
+            2 => a[3],
+            3 => b[3],
+            _ => unreachable!(),
+        })
+    }
+
+    pub fn _mm256_unpacklo_epi32(a: i32x8, b: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| match i {
+            0 => a[0],
+            1 => b[0],
+            2 => a[1],
+            3 => b[1],
+            4 => a[4],
+            5 => b[4],
+            6 => a[5],
+            7 => b[5],
+            _ => unreachable!(),
+        })
+    }
+
+    pub fn _mm256_unpackhi_epi32(a: i32x8, b: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| match i {
+            0 => a[2],
+            1 => b[2],
+            2 => a[3],
+            3 => b[3],
+            4 => a[6],
+            5 => b[6],
+            6 => a[7],
+            7 => b[7],
+            _ => unreachable!(),
+        })
+    }
+
+    pub fn _mm256_castsi128_si256(a: BitVec<128>) -> BitVec<256> {
+        BitVec::from_fn(|i| if i < 128 { a[i] } else { Bit::Zero })
+    }
+
+    pub fn _mm256_cvtepi16_epi32(a: i16x8) -> i32x8 {
+        i32x8::from_fn(|i| a[i] as i32)
+    }
+
+    pub fn _mm_packs_epi16(a: i16x8, b: i16x8) -> i8x16 {
+        i8x16::from_fn(|i| {
+            if i < 8 {
+                if a[i] > (i8::MAX as i16) {
+                    i8::MAX
+                } else if a[i] < (i8::MIN as i16) {
+                    i8::MIN
+                } else {
+                    a[i] as i8
+                }
+            } else {
+                if b[i - 8] > (i8::MAX as i16) {
+                    i8::MAX
+                } else if b[i - 8] < (i8::MIN as i16) {
+                    i8::MIN
+                } else {
+                    b[i - 8] as i8
+                }
+            }
+        })
+    }
+
+    pub fn _mm256_packs_epi32(a: i32x8, b: i32x8) -> i16x16 {
+        i16x16::from_fn(|i| {
+            if i < 4 {
+                if a[i] > (i16::MAX as i32) {
+                    i16::MAX
+                } else if a[i] < (i16::MIN as i32) {
+                    i16::MIN
+                } else {
+                    a[i] as i16
+                }
+            } else if i < 8 {
+                if b[i - 4] > (i16::MAX as i32) {
+                    i16::MAX
+                } else if b[i - 4] < (i16::MIN as i32) {
+                    i16::MIN
+                } else {
+                    b[i - 4] as i16
+                }
+            } else if i < 12 {
+                if a[i - 4] > (i16::MAX as i32) {
+                    i16::MAX
+                } else if a[i - 4] < (i16::MIN as i32) {
+                    i16::MIN
+                } else {
+                    a[i - 4] as i16
+                }
+            } else {
+                if b[i - 8] > (i16::MAX as i32) {
+                    i16::MAX
+                } else if b[i - 8] < (i16::MIN as i32) {
+                    i16::MIN
+                } else {
+                    b[i - 8] as i16
+                }
+            }
+        })
+    }
+
+    pub fn _mm256_inserti128_si256<const IMM8: i32>(a: i128x2, b: i128x1) -> i128x2 {
+        i128x2::from_fn(|i| {
+            if IMM8 % 2 == 0 {
+                match i {
+                    0 => b[0],
+                    1 => a[1],
+                    _ => unreachable!(),
+                }
+            } else {
+                match i {
+                    0 => a[0],
+                    1 => b[0],
+                    _ => unreachable!(),
+                }
+            }
+        })
+    }
+
+    pub fn _mm256_blend_epi16<const IMM8: i32>(a: i16x16, b: i16x16) -> i16x16 {
+        i16x16::from_fn(|i| {
+            if (IMM8 >> (i % 8)) % 2 == 0 {
+                a[i]
+            } else {
+                b[i]
+            }
+        })
+    }
+
+    pub fn _mm256_blendv_ps(a: i32x8, b: i32x8, mask: i32x8) -> i32x8 {
+        i32x8::from_fn(|i| if mask[i] < 0 { b[i] } else { a[i] })
+    }
+
+    #[hax_lib::fstar::verification_status(lax)]
+    pub fn _mm_movemask_epi8(a: i8x16) -> i32 {
+        let a0 = if a[0] < 0 { 1 } else { 0 };
+        let a1 = if a[1] < 0 { 2 } else { 0 };
+        let a2 = if a[2] < 0 { 4 } else { 0 };
+        let a3 = if a[3] < 0 { 8 } else { 0 };
+        let a4 = if a[4] < 0 { 16 } else { 0 };
+        let a5 = if a[5] < 0 { 32 } else { 0 };
+        let a6 = if a[6] < 0 { 64 } else { 0 };
+        let a7 = if a[7] < 0 { 128 } else { 0 };
+        let a8 = if a[8] < 0 { 256 } else { 0 };
+        let a9 = if a[9] < 0 { 512 } else { 0 };
+        let a10 = if a[10] < 0 { 1024 } else { 0 };
+        let a11 = if a[11] < 0 { 2048 } else { 0 };
+        let a12 = if a[12] < 0 { 4096 } else { 0 };
+        let a13 = if a[13] < 0 { 8192 } else { 0 };
+        let a14 = if a[14] < 0 { 16384 } else { 0 };
+        let a15 = if a[15] < 0 { 32768 } else { 0 };
+
+        a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7 + a8 + a9 + a10 + a11 + a12 + a13 + a14 + a15
+    }
+
+    pub fn _mm256_srlv_epi64(a: i64x4, b: i64x4) -> i64x4 {
+        i64x4::from_fn(|i| {
+            if b[i] > 63 || b[i] < 0 {
+                0
+            } else {
+                ((a[i] as u64) >> b[i]) as i64
+            }
+        })
+    }
+
+    pub fn _mm_sllv_epi32(a: i32x4, b: i32x4) -> i32x4 {
+        i32x4::from_fn(|i| {
+            if b[i] > 31 || b[i] < 0 {
+                0
+            } else {
+                ((a[i] as u32) << b[i]) as i32
+            }
+        })
+    }
+
+    pub fn _mm256_slli_epi64<const IMM8: i32>(a: i64x4) -> i64x4 {
+        i64x4::from_fn(|i| {
+            let imm8 = IMM8 % 256;
+            if imm8 > 63 {
+                0
+            } else {
+                ((a[i] as u64) << imm8) as i64
+            }
+        })
+    }
+
+    pub fn _mm256_bsrli_epi128<const IMM8: i32>(a: i128x2) -> i128x2 {
+        i128x2::from_fn(|i| {
+            let tmp = IMM8 % 256;
+            let tmp = tmp % 16;
+            ((a[i] as u128) >> (tmp * 8)) as i128
+        })
+    }
+
+    pub fn _mm256_andnot_si256(a: BitVec<256>, b: BitVec<256>) -> BitVec<256> {
+        BitVec::from_fn(|i| match (a[i], b[i]) {
+            (Bit::Zero, Bit::One) => Bit::One,
+            _ => Bit::Zero,
+        })
+    }
+
+    pub fn _mm256_set1_epi64x(a: i64) -> i64x4 {
+        i64x4::from_fn(|_| a)
+    }
+
+    pub fn _mm256_set_epi64x(e3: i64, e2: i64, e1: i64, e0: i64) -> i64x4 {
+        i64x4::from_fn(|i| match i {
+            0 => e0,
+            1 => e1,
+            2 => e2,
+            3 => e3,
+            _ => unreachable!(),
+        })
+    }
+
+    pub fn _mm256_unpacklo_epi64(a: i64x4, b: i64x4) -> i64x4 {
+        i64x4::from_fn(|i| match i {
+            0 => a[0],
+            1 => b[0],
+            2 => a[2],
+            3 => b[2],
+            _ => unreachable!(),
+        })
+    }
+
+    pub fn _mm256_permute2x128_si256<const IMM8: i32>(a: i128x2, b: i128x2) -> i128x2 {
+        i128x2::from_fn(|i| {
+            let control = IMM8 >> (i * 4);
+            if (control >> 3) % 2 == 1 {
+                0
+            } else {
+                match control % 4 {
+                    0 => a[0],
+                    1 => a[1],
+                    2 => b[0],
+                    3 => b[1],
+                    _ => unreachable!(),
+                }
+            }
+        })
     }
 
     pub use lemmas::flatten_circuit;
-    // ! This module provides lemmas allowing to lift the intrinsics modeled in `super` from their version operating on AVX2 vectors to functions operating on machine integer vectors (e.g. on `i32x8`).
     pub mod lemmas {
+        //! This module provides lemmas allowing to lift the intrinsics modeled in `super` from their version operating on AVX2 vectors to functions operating on machine integer vectors (e.g. on `i32x8`).
+        #[cfg(hax)]
         use super::*;
 
-        #[allow(unused)]
+        #[cfg(hax)]
         use crate::core_arch::x86 as upstream;
-        #[allow(unused)]
-        use crate::core_arch::x86::__m256i;
+        #[cfg(hax)]
+        use crate::core_arch::x86::{__m128i, __m256, __m256i};
 
         /// An F* attribute that marks an item as being an lifting lemma.
         #[allow(dead_code)]
@@ -61,6 +560,21 @@ pub mod int_vec {
         #[hax_lib::fstar::before("irreducible")]
         pub const LIFT_LEMMA: () = ();
 
+        #[hax_lib::fstar::replace(r#"
+[@@ v_LIFT_LEMMA ]
+assume val _mm256_set_epi32_interp: e7: i32 -> e6: i32 -> e5: i32 -> e4: i32 -> e3: i32 -> e2: i32 -> e1: i32 -> e0: i32 -> (i: u64 {v i < 8})
+  -> Lemma
+        (
+            (
+                Core_models.Abstractions.Bitvec.Int_vec_interp.e_ee_1__impl__to_i32x8
+                    (Core_models.Core_arch.X86.Avx.e_mm256_set_epi32 e7 e6 e5 e4 e3 e2 e1 e0)
+            ).[ i ]
+         == ( match i with
+            | MkInt 0 -> e0 | MkInt 1 -> e1 | MkInt 2 -> e2 | MkInt 3 -> e3
+            | MkInt 4 -> e4 | MkInt 5 -> e5 | MkInt 6 -> e6 | MkInt 7 -> e7 )
+        )"#)]
+        const _: () = ();
+
         /// Derives automatically a lift lemma for a given function
         macro_rules! mk_lift_lemma {
             ($name:ident$(<$(const $c:ident : $cty:ty),*>)?($($x:ident : $ty:ty),*) == $lhs:expr) => {
@@ -77,23 +591,109 @@ pub mod int_vec {
         }
         mk_lift_lemma!(
             _mm256_set1_epi32(x: i32) ==
-            __m256i::from(super::_mm256_set1_epi32(x))
+            __m256i::from_i32x8(super::_mm256_set1_epi32(x))
         );
         mk_lift_lemma!(
             _mm256_mul_epi32(x: __m256i, y: __m256i) ==
-            __m256i::from(super::_mm256_mul_epi32(super::i32x8::from(x), super::i32x8::from(y)))
+            __m256i::from_i64x4(super::_mm256_mul_epi32(BitVec::to_i32x8(x), BitVec::to_i32x8(y)))
         );
         mk_lift_lemma!(
             _mm256_sub_epi32(x: __m256i, y: __m256i) ==
-            __m256i::from(super::_mm256_sub_epi32(super::i32x8::from(x), super::i32x8::from(y)))
+            __m256i::from_i32x8(super::_mm256_sub_epi32(BitVec::to_i32x8(x), BitVec::to_i32x8(y)))
         );
         mk_lift_lemma!(
             _mm256_shuffle_epi32<const CONTROL: i32>(x: __m256i) ==
-            __m256i::from(super::_mm256_shuffle_epi32::<CONTROL>(super::i32x8::from(x)))
+            __m256i::from_i32x8(super::_mm256_shuffle_epi32::<CONTROL>(BitVec::to_i32x8(x)))
         );
         mk_lift_lemma!(_mm256_blend_epi32<const CONTROL: i32>(x: __m256i, y: __m256i) ==
-            __m256i::from(super::_mm256_blend_epi32::<CONTROL>(super::i32x8::from(x), super::i32x8::from(y)))
+            __m256i::from_i32x8(super::_mm256_blend_epi32::<CONTROL>(BitVec::to_i32x8(x), BitVec::to_i32x8(y)))
         );
+        mk_lift_lemma!(_mm256_set1_epi16(x: i16) ==
+		       __m256i::from_i16x16(super::_mm256_set1_epi16(x)));
+        mk_lift_lemma!(_mm_set1_epi16(x: i16) ==
+		       __m128i::from_i16x8(super::_mm_set1_epi16(x)));
+        mk_lift_lemma!(_mm_set_epi32(e3: i32, e2: i32, e1: i32, e0: i32) ==
+               __m128i::from_i32x4(super::_mm_set_epi32(e3, e2, e1, e0)));
+        mk_lift_lemma!(_mm_add_epi16(a: __m128i, b: __m128i) ==
+               __m128i::from_i16x8(super::_mm_add_epi16(BitVec::to_i16x8(a), BitVec::to_i16x8(b))));
+        mk_lift_lemma!(_mm256_add_epi16(a: __m256i, b: __m256i) ==
+		       __m256i::from_i16x16(super::_mm256_add_epi16(BitVec::to_i16x16(a), BitVec::to_i16x16(b))));
+        mk_lift_lemma!(_mm256_add_epi32(a: __m256i, b: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_add_epi32(BitVec::to_i32x8(a), BitVec::to_i32x8(b))));
+        mk_lift_lemma!(_mm256_add_epi64(a: __m256i, b: __m256i) ==
+		       __m256i::from_i64x4(super::_mm256_add_epi64(BitVec::to_i64x4(a), BitVec::to_i64x4(b))));
+        mk_lift_lemma!(_mm256_abs_epi32(a: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_abs_epi32(BitVec::to_i32x8(a))));
+        mk_lift_lemma!(_mm256_sub_epi16(a: __m256i, b: __m256i) ==
+		       __m256i::from_i16x16(super::_mm256_sub_epi16(BitVec::to_i16x16(a), BitVec::to_i16x16(b))));
+        mk_lift_lemma!(_mm_mullo_epi16(a: __m128i, b: __m128i) ==
+		       __m128i::from_i16x8(super::_mm_mullo_epi16(BitVec::to_i16x8(a), BitVec::to_i16x8(b))));
+        mk_lift_lemma!(_mm256_cmpgt_epi16(a: __m256i, b: __m256i) ==
+		       __m256i::from_i16x16(super::_mm256_cmpgt_epi16(BitVec::to_i16x16(a), BitVec::to_i16x16(b))));
+        mk_lift_lemma!(_mm256_cmpgt_epi32(a: __m256i, b: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_cmpgt_epi32(BitVec::to_i32x8(a), BitVec::to_i32x8(b))));
+        mk_lift_lemma!(_mm256_sign_epi32(a: __m256i, b: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_sign_epi32(BitVec::to_i32x8(a), BitVec::to_i32x8(b))));
+        mk_lift_lemma!(_mm256_movemask_ps(a: __m256) ==
+               super::_mm256_movemask_ps(BitVec::to_i32x8(a)));
+        mk_lift_lemma!(_mm_mulhi_epi16(a: __m128i, b: __m128i) ==
+		       __m128i::from_i16x8(super::_mm_mulhi_epi16(BitVec::to_i16x8(a), BitVec::to_i16x8(b))));
+        mk_lift_lemma!(_mm256_mullo_epi32(a: __m256i, b: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_mullo_epi32(BitVec::to_i32x8(a), BitVec::to_i32x8(b))));
+        mk_lift_lemma!(_mm256_mulhi_epi16(a: __m256i, b: __m256i) ==
+		       __m256i::from_i16x16(super::_mm256_mulhi_epi16(BitVec::to_i16x16(a), BitVec::to_i16x16(b))));
+        mk_lift_lemma!(_mm256_mul_epu32(a: __m256i, b: __m256i) ==
+		       __m256i::from_u64x4(super::_mm256_mul_epu32(BitVec::to_u32x8(a), BitVec::to_u32x8(b))));
+        mk_lift_lemma!(_mm256_srai_epi16<const IMM8: i32>(a: __m256i) ==
+		       __m256i::from_i16x16(super::_mm256_srai_epi16::<IMM8>(BitVec::to_i16x16(a))));
+        mk_lift_lemma!(_mm256_srai_epi32<const IMM8: i32>(a: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_srai_epi32::<IMM8>(BitVec::to_i32x8(a))));
+        mk_lift_lemma!(_mm256_srli_epi16<const IMM8: i32>(a: __m256i) ==
+		       __m256i::from_i16x16(super::_mm256_srli_epi16::<IMM8>(BitVec::to_i16x16(a))));
+        mk_lift_lemma!(_mm256_srli_epi32<const IMM8: i32>(a: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_srli_epi32::<IMM8>(BitVec::to_i32x8(a))));
+        mk_lift_lemma!(_mm_srli_epi64<const IMM8: i32>(a: __m128i) ==
+		       __m128i::from_i64x2(super::_mm_srli_epi64::<IMM8>(BitVec::to_i64x2(a))));
+        mk_lift_lemma!(_mm256_slli_epi32<const IMM8: i32>(a: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_slli_epi32::<IMM8>(BitVec::to_i32x8(a))));
+        mk_lift_lemma!(_mm256_permute4x64_epi64<const IMM8: i32>(a: __m256i) ==
+		       __m256i::from_i64x4(super::_mm256_permute4x64_epi64::<IMM8>(BitVec::to_i64x4(a))));
+        mk_lift_lemma!(_mm256_unpackhi_epi64(a: __m256i, b: __m256i) ==
+		       __m256i::from_i64x4(super::_mm256_unpackhi_epi64(BitVec::to_i64x4(a), BitVec::to_i64x4(b))));
+        mk_lift_lemma!(_mm256_unpacklo_epi32(a: __m256i, b: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_unpacklo_epi32(BitVec::to_i32x8(a), BitVec::to_i32x8(b))));
+        mk_lift_lemma!(_mm256_unpackhi_epi32(a: __m256i, b: __m256i) ==
+		       __m256i::from_i32x8(super::_mm256_unpackhi_epi32(BitVec::to_i32x8(a), BitVec::to_i32x8(b))));
+        mk_lift_lemma!(_mm256_cvtepi16_epi32(a: __m128i) ==
+		       __m256i::from_i32x8(super::_mm256_cvtepi16_epi32(BitVec::to_i16x8(a))));
+        mk_lift_lemma!(_mm_packs_epi16(a: __m128i, b: __m128i) ==
+		       __m128i::from_i8x16(super::_mm_packs_epi16(BitVec::to_i16x8(a), BitVec::to_i16x8(b))));
+        mk_lift_lemma!(_mm256_packs_epi32(a: __m256i, b: __m256i) ==
+               __m256i::from_i16x16(super::_mm256_packs_epi32(BitVec::to_i32x8(a), BitVec::to_i32x8(b))));
+        mk_lift_lemma!(_mm256_inserti128_si256<const IMM8: i32>(a: __m256i, b: __m128i) ==
+		       __m256i::from_i128x2(super::_mm256_inserti128_si256::<IMM8>(BitVec::to_i128x2(a),BitVec::to_i128x1(b))));
+        mk_lift_lemma!(_mm256_blend_epi16<const IMM8: i32>(a: __m256i, b: __m256i) ==
+		       __m256i::from_i16x16(super::_mm256_blend_epi16::<IMM8>(BitVec::to_i16x16(a),BitVec::to_i16x16(b))));
+        mk_lift_lemma!(_mm256_blendv_ps(a: __m256, b: __m256, c: __m256) ==
+		       __m256::from_i32x8(super::_mm256_blendv_ps(BitVec::to_i32x8(a),BitVec::to_i32x8(b),BitVec::to_i32x8(c))));
+        mk_lift_lemma!(_mm_movemask_epi8(a: __m128i) ==
+		       super::_mm_movemask_epi8(BitVec::to_i8x16(a)));
+        mk_lift_lemma!(_mm256_srlv_epi64(a: __m256i, b: __m256i) ==
+		       __m256i::from_i64x4(super::_mm256_srlv_epi64(BitVec::to_i64x4(a), BitVec::to_i64x4(b))));
+        mk_lift_lemma!(_mm_sllv_epi32(a: __m128i, b: __m128i) ==
+		       __m128i::from_i32x4(super::_mm_sllv_epi32(BitVec::to_i32x4(a), BitVec::to_i32x4(b))));
+        mk_lift_lemma!(_mm256_slli_epi64<const IMM8: i32>(a: __m256i) ==
+               __m256i::from_i64x4(super::_mm256_slli_epi64::<IMM8>(BitVec::to_i64x4(a))));
+        mk_lift_lemma!(_mm256_bsrli_epi128<const IMM8: i32>(a: __m256i) ==
+               __m256i::from_i128x2(super::_mm256_bsrli_epi128::<IMM8>(BitVec::to_i128x2(a))));
+        mk_lift_lemma!(_mm256_set1_epi64x(a: i64) ==
+		       __m256i::from_i64x4(super::_mm256_set1_epi64x(a)));
+        mk_lift_lemma!(_mm256_set_epi64x(e3: i64, e2: i64, e1: i64, e0: i64) ==
+		       __m256i::from_i64x4(super::_mm256_set_epi64x(e3, e2, e1, e0)));
+        mk_lift_lemma!(_mm256_unpacklo_epi64(a: __m256i, b: __m256i) ==
+		       __m256i::from_i64x4(super::_mm256_unpacklo_epi64(BitVec::to_i64x4(a), BitVec::to_i64x4(b))));
+        mk_lift_lemma!(_mm256_permute2x128_si256<const IMM8: i32>(a: __m256i, b: __m256i) ==
+		       __m256i::from_i128x2(super::_mm256_permute2x128_si256::<IMM8>(BitVec::to_i128x2(a), BitVec::to_i128x2(b))));
 
         #[hax_lib::fstar::replace(
             r#"
@@ -105,6 +705,8 @@ pub mod int_vec {
                     "FStar.FunctionalExtensionality";
                     `%Rust_primitives.cast_tc; `%Rust_primitives.unsize_tc;
                     "Core.Ops"; `%(.[]);
+                    `%${i64x4::into_i32x8};
+                    `%${i32x8::into_i64x4};
                 ]
                 (top_levels_of_attr (` $LIFT_LEMMA ))
                 (top_levels_of_attr (` $SIMPLIFICATION_LEMMA ))
@@ -119,25 +721,7 @@ pub mod int_vec {
     mod tests {
         use crate::abstractions::bitvec::BitVec;
         use crate::core_arch::x86::upstream;
-
-        /// Helper trait to generate random values
-        pub trait HasRandom {
-            fn random() -> Self;
-        }
-
-        impl HasRandom for i32 {
-            fn random() -> Self {
-                use rand::prelude::*;
-                let mut rng = rand::rng();
-                rng.random()
-            }
-        }
-
-        impl<const N: u64> HasRandom for BitVec<N> {
-            fn random() -> Self {
-                BitVec::rand()
-            }
-        }
+        use crate::helpers::test::HasRandom;
 
         /// Derives tests for a given intrinsics. Test that a given intrisics and its model compute the same thing over random values (1000 by default).
         macro_rules! mk {
@@ -175,5 +759,117 @@ pub mod int_vec {
         mk!(_mm256_mul_epi32(x: BitVec, y: BitVec));
         mk!(_mm256_shuffle_epi32{<0b01_00_10_11>, <0b01_11_01_10>}(x: BitVec));
         mk!([100]_mm256_blend_epi32{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(x: BitVec, y: BitVec));
+        mk!(_mm256_setzero_si256());
+        mk!(_mm256_set_m128i(x: BitVec, y: BitVec));
+        mk!(_mm256_set1_epi16(x: i16 ));
+        mk!(_mm_set1_epi16(x: i16));
+        mk!(_mm_set_epi32(e3: i32, e2: i32, e1: i32, e0: i32));
+
+        mk!(_mm_add_epi16(a: BitVec, b: BitVec));
+        mk!(_mm256_add_epi16(a: BitVec, b: BitVec));
+        mk!(_mm256_add_epi32(a: BitVec, b: BitVec));
+        mk!(_mm256_add_epi64(a: BitVec, b: BitVec));
+        mk!(_mm256_abs_epi32(a: BitVec));
+        #[test]
+        fn _mm256_abs_epi32_min() {
+            let a: BitVec<256> = BitVec::from_slice(&[i32::MIN; 8], 32);
+            assert_eq!(
+                BitVec::from(super::_mm256_abs_epi32(a.into())),
+                BitVec::from(unsafe { upstream::_mm256_abs_epi32(a.into()) })
+            );
+        }
+        mk!(_mm256_sub_epi16(a: BitVec, b: BitVec));
+
+        mk!(_mm_mullo_epi16(a: BitVec, b: BitVec));
+        mk!(_mm256_cmpgt_epi16(a: BitVec, b: BitVec));
+        mk!(_mm256_cmpgt_epi32(a: BitVec, b: BitVec));
+        mk!(_mm256_sign_epi32(a: BitVec, b: BitVec));
+        #[test]
+        fn _mm256_sign_epi32_min() {
+            let a: BitVec<256> = BitVec::from_slice(&[i32::MIN; 8], 32);
+            let b: BitVec<256> = BitVec::from_slice(&[-1; 8], 32);
+            assert_eq!(
+                BitVec::from(super::_mm256_sign_epi32(a.into(), b.into())),
+                BitVec::from(unsafe { upstream::_mm256_sign_epi32(a.into(), b.into()) })
+            );
+        }
+        mk!(_mm256_castsi256_ps(a: BitVec));
+        mk!(_mm256_castps_si256(a: BitVec));
+
+        #[test]
+        fn _mm256_movemask_ps() {
+            let n = 1000;
+
+            for _ in 0..n {
+                let a: BitVec<256> = BitVec::random();
+                assert_eq!(super::_mm256_movemask_ps(a.into()), unsafe {
+                    upstream::_mm256_movemask_ps(a.into())
+                });
+            }
+        }
+        mk!(_mm_mulhi_epi16(a: BitVec, b: BitVec));
+        mk!(_mm256_mullo_epi32(a: BitVec, b: BitVec));
+
+        mk!(_mm256_and_si256(a: BitVec, b: BitVec));
+        mk!(_mm256_or_si256(a: BitVec, b: BitVec));
+        #[test]
+        fn _mm256_testz_si256() {
+            let n = 1000;
+
+            for _ in 0..n {
+                let a: BitVec<256> = BitVec::random();
+                let b: BitVec<256> = BitVec::random();
+                assert_eq!(super::_mm256_testz_si256(a.into(), b.into()), unsafe {
+                    upstream::_mm256_testz_si256(a.into(), b.into())
+                });
+            }
+        }
+        mk!(_mm256_xor_si256(a: BitVec, b: BitVec));
+
+        mk!([100]_mm256_srai_epi16{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec));
+
+        mk!([100]_mm256_srai_epi32{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec));
+
+        mk!([100]_mm256_srli_epi16{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec));
+
+        mk!([100]_mm256_srli_epi32{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec));
+
+        mk!([100]_mm_srli_epi64{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec));
+
+        mk!([100]_mm256_slli_epi32{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec));
+
+        mk!(_mm256_castsi128_si256(a: BitVec));
+
+        mk!(_mm256_cvtepi16_epi32(a: BitVec));
+        mk!(_mm_packs_epi16(a: BitVec, b: BitVec));
+        mk!(_mm256_packs_epi32(a: BitVec, b: BitVec));
+        mk!([100]_mm256_inserti128_si256{<0>,<1>}(a: BitVec, b: BitVec));
+        mk!([100]_mm256_blend_epi16{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec, b: BitVec));
+        mk!(_mm256_blendv_ps(a: BitVec, b: BitVec, mask: BitVec));
+
+        #[test]
+        fn _mm_movemask_epi8() {
+            let n = 1000;
+
+            for _ in 0..n {
+                let a: BitVec<128> = BitVec::random();
+                assert_eq!(super::_mm_movemask_epi8(a.into()), unsafe {
+                    upstream::_mm_movemask_epi8(a.into())
+                });
+            }
+        }
+        mk!(_mm256_srlv_epi64(a: BitVec, b: BitVec));
+        mk!(_mm_sllv_epi32(a: BitVec, b: BitVec));
+
+        mk!([100]_mm256_slli_epi64{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec));
+
+        mk!([100]_mm256_bsrli_epi128{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec));
+
+        mk!(_mm256_andnot_si256(a: BitVec, b: BitVec));
+        mk!(_mm256_set1_epi64x(a: i64));
+        mk!(_mm256_set_epi64x(e3: i64, e2: i64, e1: i64, e0: i64));
+        mk!(_mm256_unpacklo_epi64(a: BitVec, b: BitVec));
+
+        mk!([100]_mm256_permute2x128_si256{<0>,<1>,<2>,<3>,<4>,<5>,<6>,<7>,<8>,<9>,<10>,<11>,<12>,<13>,<14>,<15>,<16>,<17>,<18>,<19>,<20>,<21>,<22>,<23>,<24>,<25>,<26>,<27>,<28>,<29>,<30>,<31>,<32>,<33>,<34>,<35>,<36>,<37>,<38>,<39>,<40>,<41>,<42>,<43>,<44>,<45>,<46>,<47>,<48>,<49>,<50>,<51>,<52>,<53>,<54>,<55>,<56>,<57>,<58>,<59>,<60>,<61>,<62>,<63>,<64>,<65>,<66>,<67>,<68>,<69>,<70>,<71>,<72>,<73>,<74>,<75>,<76>,<77>,<78>,<79>,<80>,<81>,<82>,<83>,<84>,<85>,<86>,<87>,<88>,<89>,<90>,<91>,<92>,<93>,<94>,<95>,<96>,<97>,<98>,<99>,<100>,<101>,<102>,<103>,<104>,<105>,<106>,<107>,<108>,<109>,<110>,<111>,<112>,<113>,<114>,<115>,<116>,<117>,<118>,<119>,<120>,<121>,<122>,<123>,<124>,<125>,<126>,<127>,<128>,<129>,<130>,<131>,<132>,<133>,<134>,<135>,<136>,<137>,<138>,<139>,<140>,<141>,<142>,<143>,<144>,<145>,<146>,<147>,<148>,<149>,<150>,<151>,<152>,<153>,<154>,<155>,<156>,<157>,<158>,<159>,<160>,<161>,<162>,<163>,<164>,<165>,<166>,<167>,<168>,<169>,<170>,<171>,<172>,<173>,<174>,<175>,<176>,<177>,<178>,<179>,<180>,<181>,<182>,<183>,<184>,<185>,<186>,<187>,<188>,<189>,<190>,<191>,<192>,<193>,<194>,<195>,<196>,<197>,<198>,<199>,<200>,<201>,<202>,<203>,<204>,<205>,<206>,<207>,<208>,<209>,<210>,<211>,<212>,<213>,<214>,<215>,<216>,<217>,<218>,<219>,<220>,<221>,<222>,<223>,<224>,<225>,<226>,<227>,<228>,<229>,<230>,<231>,<232>,<233>,<234>,<235>,<236>,<237>,<238>,<239>,<240>,<241>,<242>,<243>,<244>,<245>,<246>,<247>,<248>,<249>,<250>,<251>,<252>,<253>,<254>,<255>}(a: BitVec, b: BitVec));
     }
 }
diff --git a/fstar-helpers/core-models/src/core_arch/x86/opaque.rs b/fstar-helpers/core-models/src/core_arch/x86/opaque.rs
deleted file mode 100644
index 62bae90f8..000000000
--- a/fstar-helpers/core-models/src/core_arch/x86/opaque.rs
+++ /dev/null
@@ -1,248 +0,0 @@
-#![allow(unused_variables)]
-
-//! A module providing a opaque interfaces to intrinsics.
-//! Those functions are not intended to be used in F*: they are useful only for Rust typoechecking.
-
-use super::*;
-
-pub type Vec128 = __m128i;
-pub type Vec256 = __m256i;
-pub type Vec256Float = __m256;
-
-#[hax_lib::opaque]
-pub unsafe fn _mm256_setzero_si256() -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_set_m128i(hi: __m128i, lo: __m128i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_set1_epi16(a: i16) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_set1_epi16(a: i16) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_set_epi32(e3: i32, e2: i32, e1: i32, e0: i32) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_add_epi16(a: __m128i, b: __m128i) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_add_epi16(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_madd_epi16(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_add_epi32(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_add_epi64(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_abs_epi32(a: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_sub_epi16(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_sub_epi16(a: __m128i, b: __m128i) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_mullo_epi16(a: __m128i, b: __m128i) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_cmpgt_epi16(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_cmpgt_epi32(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_cmpeq_epi32(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_sign_epi32(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_castsi256_ps(a: __m256i) -> __m256 {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_castps_si256(a: __m256) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_movemask_ps(a: __m256) -> i32 {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_mulhi_epi16(a: __m128i, b: __m128i) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_mullo_epi32(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_mulhi_epi16(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_mul_epu32(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_and_si256(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_or_si256(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_testz_si256(a: __m256i, b: __m256i) -> i32 {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_xor_si256(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_srai_epi16<const IMM8: i32>(a: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_srai_epi32<const IMM8: i32>(a: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_srli_epi16<const IMM8: i32>(a: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_srli_epi32<const IMM8: i32>(a: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_srli_epi64<const IMM8: i32>(a: __m128i) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_slli_epi32<const IMM8: i32>(a: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_permute4x64_epi64<const IMM8: i32>(a: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_unpackhi_epi64(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_unpacklo_epi32(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_unpackhi_epi32(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_castsi128_si256(a: __m128i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_cvtepi16_epi32(a: __m128i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_packs_epi16(a: __m128i, b: __m128i) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_packs_epi32(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_inserti128_si256<const IMM8: i32>(a: __m256i, b: __m128i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_blend_epi16<const IMM8: i32>(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_blendv_ps(a: __m256, b: __m256, mask: __m256) -> __m256 {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_movemask_epi8(a: __m128i) -> i32 {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_srlv_epi64(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm_sllv_epi32(a: __m128i, b: __m128i) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_slli_epi64<const IMM8: i32>(a: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_bsrli_epi128<const IMM8: i32>(a: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_andnot_si256(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_set1_epi64x(a: i64) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_set_epi64x(e3: i64, e2: i64, e1: i64, e0: i64) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_unpacklo_epi64(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-#[hax_lib::opaque]
-pub unsafe fn _mm256_permute2x128_si256<const IMM8: i32>(a: __m256i, b: __m256i) -> __m256i {
-    unimplemented!()
-}
-
-#[hax_lib::exclude]
-pub unsafe fn _mm256_storeu_si256(mem_addr: *mut __m256i, a: __m256i) {
-    unimplemented!()
-}
-#[hax_lib::exclude]
-pub unsafe fn _mm_loadu_si128(mem_addr: *const __m128i) -> __m128i {
-    unimplemented!()
-}
-#[hax_lib::exclude]
-pub unsafe fn _mm256_loadu_si256(mem_addr: *const __m256i) -> __m256i {
-    unimplemented!()
-}
diff --git a/fstar-helpers/core-models/src/helpers.rs b/fstar-helpers/core-models/src/helpers.rs
new file mode 100644
index 000000000..6c5e84e2a
--- /dev/null
+++ b/fstar-helpers/core-models/src/helpers.rs
@@ -0,0 +1,55 @@
+#[cfg(test)]
+pub mod test {
+    use crate::abstractions::{bit::Bit, bitvec::BitVec, funarr::FunArray};
+    use rand::prelude::*;
+
+    /// Helper trait to generate random values
+    pub trait HasRandom {
+        fn random() -> Self;
+    }
+    macro_rules! mk_has_random {
+        ($($ty:ty),*) => {
+            $(impl HasRandom for $ty {
+                fn random() -> Self {
+                    let mut rng = rand::rng();
+                    rng.random()
+                }
+            })*
+        };
+    }
+
+    mk_has_random!(bool);
+    mk_has_random!(i8, i16, i32, i64, i128);
+    mk_has_random!(u8, u16, u32, u64, u128);
+
+    impl HasRandom for isize {
+        fn random() -> Self {
+            i128::random() as isize
+        }
+    }
+    impl HasRandom for usize {
+        fn random() -> Self {
+            i128::random() as usize
+        }
+    }
+
+    impl HasRandom for Bit {
+        fn random() -> Self {
+            crate::abstractions::bit::Bit::from(bool::random())
+        }
+    }
+    impl<const N: u64> HasRandom for BitVec<N> {
+        fn random() -> Self {
+            Self::from_fn(|_| Bit::random())
+        }
+    }
+
+    impl<const N: u64, T: HasRandom> HasRandom for FunArray<N, T> {
+        fn random() -> Self {
+            FunArray::from_fn(|_| T::random())
+        }
+    }
+}
+
+#[cfg(test)]
+pub use test::*;
diff --git a/fstar-helpers/core-models/src/lib.rs b/fstar-helpers/core-models/src/lib.rs
index 742775ebb..9fbd0738b 100644
--- a/fstar-helpers/core-models/src/lib.rs
+++ b/fstar-helpers/core-models/src/lib.rs
@@ -1,34 +1,36 @@
-//! `core_models`: A Rust Model for the `core` Library
+//! `core-models`: A Rust Model for the `core` Library
 //!
-//! `core_models` is a simplified, self-contained model of Rust’s `core` library. It aims to provide
+//! `core-models` is a simplified, self-contained model of Rust’s `core` library. It aims to provide
 //! a purely Rust-based specification of `core`'s fundamental operations, making them easier to
 //! understand, analyze, and formally verify. Unlike `core`, which may rely on platform-specific
-//! intrinsics and compiler magic, `core_models` expresses everything in plain Rust, prioritizing
+//! intrinsics and compiler magic, `core-models` expresses everything in plain Rust, prioritizing
 //! clarity and explicitness over efficiency.
 //!
 //! ## Key Features
 //!
-//! - **Partial Modeling**: `core_models` includes only a subset of `core`, focusing on modeling
+//! - **Partial Modeling**: `core-models` includes only a subset of `core`, focusing on modeling
 //!   fundamental operations rather than providing a complete replacement.
-//! - **Exact Signatures**: Any item that exists in both `core_models` and `core` has the same type signature,
+//! - **Exact Signatures**: Any item that exists in both `core-models` and `core` has the same type signature,
 //!   ensuring compatibility with formal verification efforts.
-//! - **Purely Functional Approach**: Where possible, `core_models` favors functional programming principles,
+//! - **Purely Functional Approach**: Where possible, `core-models` favors functional programming principles,
 //!   avoiding unnecessary mutation and side effects to facilitate formal reasoning.
 //! - **Explicit Implementations**: Even low-level operations, such as SIMD, are modeled explicitly using
 //!   Rust constructs like bit arrays and partial maps.
-//! - **Extra Abstractions**: `core_models` includes additional helper types and functions to support
+//! - **Extra Abstractions**: `core-models` includes additional helper types and functions to support
 //!   modeling. These extra items are marked appropriately to distinguish them from `core` definitions.
 //!
 //! ## Intended Use
 //!
-//! `core_models` is designed as a reference model for formal verification and reasoning about Rust programs.
+//! `core-models` is designed as a reference model for formal verification and reasoning about Rust programs.
 //! By providing a readable, well-specified version of `core`'s behavior, it serves as a foundation for
 //! proof assistants and other verification tools.
 
-// This recursion limit is necessary for macro `core_models::core_arch::x86::interpretations::int_vec::tests::mk!`.
+// This recursion limit is necessary for macro `core-models::core_arch::x86::interpretations::int_vec::tests::mk!`.
 // We test functions with const generics, the macro generate a test per possible (const generic) control value.
-#![recursion_limit = "512"]
+#![recursion_limit = "2048"]
 pub mod abstractions;
 pub mod core_arch;
 
 pub use core_arch as arch;
+
+pub mod helpers;
diff --git a/libcrux-intrinsics/src/avx2.rs b/libcrux-intrinsics/src/avx2.rs
index 8bb3863f2..52a2fa826 100644
--- a/libcrux-intrinsics/src/avx2.rs
+++ b/libcrux-intrinsics/src/avx2.rs
@@ -108,13 +108,11 @@ pub fn mm256_loadu_si256_i32(input: &[i32]) -> Vec256 {
     unsafe { _mm256_loadu_si256(input.as_ptr() as *const Vec256) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_setzero_si256() -> Vec256 {
     unsafe { _mm256_setzero_si256() }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_set_m128i(hi: Vec128, lo: Vec128) -> Vec256 {
     unsafe { _mm256_set_m128i(hi, lo) }
@@ -205,7 +203,6 @@ pub fn mm256_set_epi8(
     }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_set1_epi16(constant: i16) -> Vec256 {
     unsafe { _mm256_set1_epi16(constant) }
@@ -238,7 +235,6 @@ pub fn mm256_set_epi16(
     }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_set1_epi16(constant: i16) -> Vec128 {
     unsafe { _mm_set1_epi16(constant) }
@@ -249,7 +245,6 @@ pub fn mm256_set1_epi32(constant: i32) -> Vec256 {
     unsafe { _mm256_set1_epi32(constant) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_set_epi32(input3: i32, input2: i32, input1: i32, input0: i32) -> Vec128 {
     unsafe { _mm_set_epi32(input3, input2, input1, input0) }
@@ -273,43 +268,36 @@ pub fn mm256_set_epi32(
     }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_add_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_add_epi16(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_add_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_add_epi16(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_madd_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_madd_epi16(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_add_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_add_epi32(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_add_epi64(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_add_epi64(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_abs_epi32(a: Vec256) -> Vec256 {
     unsafe { _mm256_abs_epi32(a) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_sub_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_sub_epi16(lhs, rhs) }
@@ -320,7 +308,6 @@ pub fn mm256_sub_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_sub_epi32(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_sub_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_sub_epi16(lhs, rhs) }
@@ -331,73 +318,61 @@ pub fn mm256_mullo_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mullo_epi16(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_mullo_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_mullo_epi16(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_cmpgt_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_cmpgt_epi16(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_cmpgt_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_cmpgt_epi32(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_cmpeq_epi32(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_cmpeq_epi32(a, b) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_sign_epi32(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_sign_epi32(a, b) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_castsi256_ps(a: Vec256) -> Vec256Float {
     unsafe { _mm256_castsi256_ps(a) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_castps_si256(a: Vec256Float) -> Vec256 {
     unsafe { _mm256_castps_si256(a) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_movemask_ps(a: Vec256Float) -> i32 {
     unsafe { _mm256_movemask_ps(a) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_mulhi_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_mulhi_epi16(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_mullo_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mullo_epi32(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_mulhi_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mulhi_epi16(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_mul_epu32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mul_epu32(lhs, rhs) }
@@ -408,25 +383,21 @@ pub fn mm256_mul_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mul_epi32(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_and_si256(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_and_si256(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_or_si256(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_or_si256(a, b) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_testz_si256(lhs: Vec256, rhs: Vec256) -> i32 {
     unsafe { _mm256_testz_si256(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_xor_si256(lhs: Vec256, rhs: Vec256) -> Vec256 {
     // This floating point xor may or may not be faster than regular xor.
@@ -445,7 +416,6 @@ pub fn mm256_xor_si256(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_xor_si256(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_srai_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     #[cfg(not(hax))]
@@ -453,7 +423,6 @@ pub fn mm256_srai_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srai_epi16::<SHIFT_BY>(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_srai_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     #[cfg(not(hax))]
@@ -461,7 +430,6 @@ pub fn mm256_srai_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srai_epi32::<SHIFT_BY>(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_srli_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     #[cfg(not(hax))]
@@ -469,7 +437,6 @@ pub fn mm256_srli_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srli_epi16::<SHIFT_BY>(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_srli_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     #[cfg(not(hax))]
@@ -477,7 +444,6 @@ pub fn mm256_srli_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srli_epi32::<SHIFT_BY>(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_srli_epi64<const SHIFT_BY: i32>(vector: Vec128) -> Vec128 {
     #[cfg(not(hax))]
@@ -493,7 +459,6 @@ pub fn mm256_srli_epi64<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srli_epi64::<SHIFT_BY>(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_slli_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     #[cfg(not(hax))]
@@ -501,7 +466,6 @@ pub fn mm256_slli_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_slli_epi16::<SHIFT_BY>(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_slli_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     #[cfg(not(hax))]
@@ -526,7 +490,6 @@ pub fn mm256_shuffle_epi32<const CONTROL: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_shuffle_epi32::<CONTROL>(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_permute4x64_epi64<const CONTROL: i32>(vector: Vec256) -> Vec256 {
     #[cfg(not(hax))]
@@ -534,19 +497,16 @@ pub fn mm256_permute4x64_epi64<const CONTROL: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_permute4x64_epi64::<CONTROL>(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_unpackhi_epi64(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_unpackhi_epi64(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_unpacklo_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_unpacklo_epi32(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_unpackhi_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_unpackhi_epi32(lhs, rhs) }
@@ -557,25 +517,21 @@ pub fn mm256_castsi256_si128(vector: Vec256) -> Vec128 {
     unsafe { _mm256_castsi256_si128(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_castsi128_si256(vector: Vec128) -> Vec256 {
     unsafe { _mm256_castsi128_si256(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_cvtepi16_epi32(vector: Vec128) -> Vec256 {
     unsafe { _mm256_cvtepi16_epi32(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_packs_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_packs_epi16(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_packs_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_packs_epi32(lhs, rhs) }
@@ -588,7 +544,6 @@ pub fn mm256_extracti128_si256<const CONTROL: i32>(vector: Vec256) -> Vec128 {
     unsafe { _mm256_extracti128_si256::<CONTROL>(vector) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_inserti128_si256<const CONTROL: i32>(vector: Vec256, vector_i128: Vec128) -> Vec256 {
     #[cfg(not(hax))]
@@ -596,7 +551,6 @@ pub fn mm256_inserti128_si256<const CONTROL: i32>(vector: Vec256, vector_i128: V
     unsafe { _mm256_inserti128_si256::<CONTROL>(vector, vector_i128) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_blend_epi16<const CONTROL: i32>(lhs: Vec256, rhs: Vec256) -> Vec256 {
     #[cfg(not(hax))]
@@ -613,7 +567,7 @@ pub fn mm256_blend_epi32<const CONTROL: i32>(lhs: Vec256, rhs: Vec256) -> Vec256
 
 // This is essentially _mm256_blendv_ps adapted for use with the Vec256 type.
 // It is not offered by the AVX2 instruction set.
-#[hax_lib::opaque]
+
 #[inline(always)]
 pub fn vec256_blendv_epi32(a: Vec256, b: Vec256, mask: Vec256) -> Vec256 {
     unsafe {
@@ -625,7 +579,6 @@ pub fn vec256_blendv_epi32(a: Vec256, b: Vec256, mask: Vec256) -> Vec256 {
     }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_movemask_epi8(vector: Vec128) -> i32 {
     unsafe { _mm_movemask_epi8(vector) }
@@ -641,13 +594,11 @@ pub fn mm256_srlv_epi32(vector: Vec256, counts: Vec256) -> Vec256 {
     unsafe { _mm256_srlv_epi32(vector, counts) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_srlv_epi64(vector: Vec256, counts: Vec256) -> Vec256 {
     unsafe { _mm256_srlv_epi64(vector, counts) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_sllv_epi32(vector: Vec128, counts: Vec128) -> Vec128 {
     unsafe { _mm_sllv_epi32(vector, counts) }
@@ -658,13 +609,11 @@ pub fn mm256_sllv_epi32(vector: Vec256, counts: Vec256) -> Vec256 {
     unsafe { _mm256_sllv_epi32(vector, counts) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_slli_epi64<const LEFT: i32>(x: Vec256) -> Vec256 {
     unsafe { _mm256_slli_epi64::<LEFT>(x) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_bsrli_epi128<const SHIFT_BY: i32>(x: Vec256) -> Vec256 {
     #[cfg(not(hax))]
@@ -672,31 +621,26 @@ pub fn mm256_bsrli_epi128<const SHIFT_BY: i32>(x: Vec256) -> Vec256 {
     unsafe { _mm256_bsrli_epi128::<SHIFT_BY>(x) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_andnot_si256(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_andnot_si256(a, b) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_set1_epi64x(a: i64) -> Vec256 {
     unsafe { _mm256_set1_epi64x(a) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_set_epi64x(input3: i64, input2: i64, input1: i64, input0: i64) -> Vec256 {
     unsafe { _mm256_set_epi64x(input3, input2, input1, input0) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_unpacklo_epi64(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_unpacklo_epi64(lhs, rhs) }
 }
 
-#[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_permute2x128_si256<const IMM8: i32>(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_permute2x128_si256::<IMM8>(a, b) }
diff --git a/libcrux-ml-dsa/src/simd/avx2/arithmetic.rs b/libcrux-ml-dsa/src/simd/avx2/arithmetic.rs
index dff3fceda..9fd9cf354 100644
--- a/libcrux-ml-dsa/src/simd/avx2/arithmetic.rs
+++ b/libcrux-ml-dsa/src/simd/avx2/arithmetic.rs
@@ -56,6 +56,22 @@ pub(super) fn montgomery_multiply_by_constant(lhs: Vec256, constant: i32) -> Vec
     res
 }
 
+// TODO: prove equivalence to our specification of `montgomery_multiply`.
+#[cfg(hax)]
+#[hax_lib::fstar::before("[@@ Tactics.Circuits.auto_unapply 2 ]")]
+pub fn montgomery_multiply_spec(x: i32, y: i32) -> i32 {
+    pub fn i32_extended64_mul(x: i32, y: i32) -> i64 {
+        (x as i64) * (y as i64)
+    }
+    let x_mul_y = i32_extended64_mul(x, y);
+    let lhs = (x_mul_y >> 32i32) as i32;
+    let rhs = ((((i32_extended64_mul(x_mul_y as i32, INVERSE_OF_MODULUS_MOD_MONTGOMERY_R as i32)
+        as i32) as i64)
+        * (FIELD_MODULUS as i64))
+        >> 32i32) as i32;
+    lhs.wrapping_sub(rhs)
+}
+
 #[hax_lib::fstar::postprocess_with(
     core_models::arch::x86::interpretations::int_vec::flatten_circuit
 )]
@@ -82,6 +98,23 @@ pub(super) fn montgomery_multiply(lhs: &mut Vec256, rhs: &Vec256) {
     *lhs = mm256_blend_epi32::<0b10101010>(res02_shifted, res13);
 }
 
+#[hax_lib::fstar::replace(
+    r#"
+let montgomery_multiply_lemma lhs rhs (i: u64 {v i < 8}): squash (
+     (Core_models.Abstractions.Bitvec.Int_vec_interp.e_ee_1__impl__to_i32x8 (montgomery_multiply lhs rhs)).[i]
+  == (montgomery_multiply_spec
+        ((Core_models.Abstractions.Bitvec.Int_vec_interp.e_ee_1__impl__to_i32x8 lhs).[i])
+        ((Core_models.Abstractions.Bitvec.Int_vec_interp.e_ee_1__impl__to_i32x8 rhs).[i])
+    )
+) = _ by (
+  let open FStar.Tactics in
+  norm [iota; primops; delta_only [`%montgomery_multiply]; zeta];
+  l_to_r [`Core_models.Abstractions.Bitvec.Int_vec_interp.e_ee_1__lemma_cancel_iv]
+)
+"#
+)]
+const _: () = ();
+
 #[inline(always)]
 pub(super) fn shift_left_then_reduce<const SHIFT_BY: i32>(simd_unit: &mut Vec256) {
     let shifted = mm256_slli_epi32::<SHIFT_BY>(*simd_unit);