(296) * Warning 296 at Libcrux_ml_kem.Vector.Portable.Serialize.fst(508,5-512,4): - Tactics admitted goal. - Goal : (v: Rust_primitives.Arrays.t_Array Rust_primitives.Integers.u8 (Rust_primitives.Integers.sz 8)) |- _ : Prims.squash (forall (i: Prims.nat{i < 64}). Rust_primitives.BitVectors.bit_vec_of_int_t_array v 8 i == Rust_primitives.BitVectors.bit_vec_of_int_t_array (Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_4_ v) .f_elements 4 i)

(296) * Warning 296 at Libcrux_ml_kem.Vector.Portable.Serialize.fst(408,5-412,4): - Tactics admitted goal. - Goal : (v: Rust_primitives.Arrays.t_Array Rust_primitives.Integers.i16 (Rust_primitives.Integers.sz 16)), (_: Prims.squash (forall (i: Prims.nat{i < FStar.Seq.Base.length v}). Rust_primitives.BitVectors.bounded (FStar.Seq.Base.index v i) 4)) |- _ : Prims.squash (forall (i: Prims.nat{i < 64}). Rust_primitives.BitVectors.bit_vec_of_int_t_array v 4 i == Rust_primitives.BitVectors.bit_vec_of_int_t_array (Libcrux_ml_kem.Vector.Portable.Serialize.serialize_4_ (Libcrux_ml_kem.Vector.Portable.Vector_type.Mkt_PortableVector v)) 8 i)

(296) * Warning 296 at Libcrux_ml_kem.Vector.Portable.Serialize.fst(302,5-307,4): - Tactics admitted goal. - Goal : (inp: Rust_primitives.Arrays.t_Array Rust_primitives.Integers.u8 (Rust_primitives.Integers.sz 2)) |- _ : Prims.squash (forall (i: Prims.nat{i < 16}). Rust_primitives.BitVectors.bit_vec_of_int_t_array inp 8 i == Rust_primitives.BitVectors.bit_vec_of_int_t_array (Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_ inp) .f_elements 1 i /\ Rust_primitives.BitVectors.bounded (FStar.Seq.Base.index (Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_ inp) .f_elements i) 1)

(296) * Warning 296 at Libcrux_ml_kem.Vector.Portable.Serialize.fst(185,5-189,4): - Tactics admitted goal. - Goal : (v: Rust_primitives.Arrays.t_Array Rust_primitives.Integers.i16 (Rust_primitives.Integers.sz 16)), (_: Prims.squash (forall (i: Prims.nat{i < FStar.Seq.Base.length v}). Rust_primitives.BitVectors.bounded (FStar.Seq.Base.index v i) 1)) |- _ : Prims.squash (forall (i: Prims.nat{i < 16}). Rust_primitives.BitVectors.bit_vec_of_int_t_array v 1 i == Rust_primitives.BitVectors.bit_vec_of_int_t_array (Libcrux_ml_kem.Vector.Portable.Serialize.serialize_1_ (Libcrux_ml_kem.Vector.Portable.Vector_type.Mkt_PortableVector v)) 8 i)

(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(424,8-424,67): - Definitions of inner let-rec h and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(225,12-225,13) -

(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(223,0-229,12): - Definitions of inner let-rec h and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(225,12-225,13) -

(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(328,0-328,12): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15) -

(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(74,0-80,10): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15) -

(242) * Warning 242 at /home/runner/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/hax-lib-0.3.2/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst(87,0-87,81): - Definitions of inner let-rec while_loop_internal and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/hax-lib-0.3.2/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst(74,10-74,29) -