(242) * Warning 242 at /home/runner/work/hax/hax/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/hax/hax/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15) -

(242) * Warning 242 at /home/runner/work/hax/hax/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/hax/hax/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15) -

(242) * Warning 242 at /home/runner/work/hax/hax/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/hax/hax/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(225,12-225,13) -

(242) * Warning 242 at /home/runner/work/hax/hax/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/hax/hax/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(225,12-225,13) -

(361) * Warning 361 at /home/runner/work/hax/hax/hacl-star/lib/Lib.IntTypes.fsti(988,0-988,21): - Some #push-options have not been popped. Current depth is 1.

(361) * Warning 361 at /home/runner/work/hax/hax/hacl-star/lib/Lib.Sequence.fsti(599,0-613,142): - Some #push-options have not been popped. Current depth is 1.

(296) * Warning 296 at Libcrux_ml_kem.Vector.Portable.Serialize.fst(129,5-133,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)

(296) * Warning 296 at Libcrux_ml_kem.Vector.Portable.Serialize.fst(182,5-186,4): - Tactics admitted goal. - Goal : (v: 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 v 8 i == Rust_primitives.BitVectors.bit_vec_of_int_t_array (Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_ v) .f_elements 1 i)

(296) * Warning 296 at Libcrux_ml_kem.Vector.Portable.Serialize.fst(262,5-266,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)