Merge branch 'main' into franziskus/mldsa-cleanup

cryspen · Jan 7, 2025 · 6732091 · 6732091
2 parents 95e75ed + 8ce0529
commit 6732091
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git a/libcrux-ml-kem/src/polynomial.rs b/libcrux-ml-kem/src/polynomial.rs
@@ -55,7 +55,7 @@ pub(crate) const VECTORS_IN_RING_ELEMENT: usize =
     {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
     (p: t_PolynomialRingElement v_Vector) : Spec.MLKEM.polynomial =
     createi (sz 256) (fun i -> Spec.MLKEM.Math.to_spec_fe 
-                                (Seq.index (i2._super_8706949974463268012.f_repr 
+                                (Seq.index (i2._super_12682756204189288427.f_repr 
                                     (Seq.index p.f_coefficients (v i / 16))) (v i % 16)))"
     )
 )]

diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs
@@ -233,10 +233,10 @@ pub fn to_standard_domain<T: Operations>(v: T) -> T {
 }
 
 #[hax_lib::fstar::verification_status(lax)]
-#[hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b_array 3328 (i1._super_8706949974463268012.f_repr a)"#))]
+#[hax_lib::requires(fstar!(r#"Spec.Utils.is_i16b_array 3328 (i1._super_12682756204189288427.f_repr a)"#))]
 #[hax_lib::ensures(|result| fstar!(r#"forall i.
-                                       (let x = Seq.index (i1._super_8706949974463268012.f_repr ${a}) i in
-                                        let y = Seq.index (i1._super_8706949974463268012.f_repr ${result}) i in
+                                       (let x = Seq.index (i1._super_12682756204189288427.f_repr ${a}) i in
+                                        let y = Seq.index (i1._super_12682756204189288427.f_repr ${result}) i in
                                         (v y >= 0 /\ v y <= 3328 /\ (v y % 3329 == v x % 3329)))"#))]
 #[inline(always)]
 pub fn to_unsigned_representative<T: Operations>(a: T) -> T {
@@ -246,28 +246,28 @@ pub fn to_unsigned_representative<T: Operations>(a: T) -> T {
 }
 
 #[hax_lib::fstar::options("--z3rlimit 200 --split_queries always")]
-#[hax_lib::requires(fstar!(r#"forall i. let x = Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i in 
+#[hax_lib::requires(fstar!(r#"forall i. let x = Seq.index (i1._super_12682756204189288427.f_repr ${vec}) i in 
                                       (x == 0s \/ x == 1s)"#))]
 #[inline(always)]
 pub fn decompress_1<T: Operations>(vec: T) -> T {
     let z = T::ZERO();
     hax_lib::fstar!(
-        "assert(forall i. Seq.index (i1._super_8706949974463268012.f_repr ${z}) i == 0s)"
+        "assert(forall i. Seq.index (i1._super_12682756204189288427.f_repr ${z}) i == 0s)"
     );
     hax_lib::fstar!(
-        r#"assert(forall i. let x = Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i in 
+        r#"assert(forall i. let x = Seq.index (i1._super_12682756204189288427.f_repr ${vec}) i in 
                                       ((0 - v x) == 0 \/ (0 - v x) == -1))"#
     );
     hax_lib::fstar!(
         r#"assert(forall i. i < 16 ==>
                                       Spec.Utils.is_intb (pow2 15 - 1) 
-                                        (0 - v (Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i)))"#
+                                        (0 - v (Seq.index (i1._super_12682756204189288427.f_repr ${vec}) i)))"#
     );
 
     let s = T::sub(z, &vec);
     hax_lib::fstar!(
-        r#"assert(forall i. Seq.index (i1._super_8706949974463268012.f_repr ${s}) i == 0s \/ 
-                                      Seq.index (i1._super_8706949974463268012.f_repr ${s}) i == -1s)"#
+        r#"assert(forall i. Seq.index (i1._super_12682756204189288427.f_repr ${s}) i == 0s \/ 
+                                      Seq.index (i1._super_12682756204189288427.f_repr ${s}) i == -1s)"#
     );
     hax_lib::fstar!(r#"assert (i1.f_bitwise_and_with_constant_pre ${s} 1665s)"#);
     let res = T::bitwise_and_with_constant(s, 1665);