Merge pull request #1136 from cryspen/frontend-upgrades-hash-fixes

chore: update hardcodeded hashes following cryspen/hax#1559

Author: karthikbhargavan

Cargo.toml

@@ -51,7 +51,7 @@ readme = "Readme.md"
 allow-branch = ["main"]
 
 [workspace.dependencies]
-hax-lib = { version = "0.3.4" }
+hax-lib = { version = "0.3.5" }
 
 [package]
 name = "libcrux"

libcrux-ml-dsa/src/arithmetic.rs

@@ -9,7 +9,7 @@ use crate::{
 #[hax_lib::requires(fstar!(r#"v $bound > 0 /\ 
         (forall i. forall j. Spec.Utils.is_i32b_array_opaque 
             (v ${crate::simd::traits::specs::FIELD_MAX}) 
-            (i0._super_4202118595671791609.f_repr (Seq.index (Seq.index vector i).f_simd_units j)))"#))]
+            (i0._super_4731626403787200903.f_repr (Seq.index (Seq.index vector i).f_simd_units j)))"#))]
 pub(crate) fn vector_infinity_norm_exceeds<SIMDUnit: Operations>(
     vector: &[PolynomialRingElement<SIMDUnit>],
     bound: i32,
@@ -25,8 +25,8 @@ pub(crate) fn vector_infinity_norm_exceeds<SIMDUnit: Operations>(
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 #[hax_lib::requires(fstar!(r#"v $SHIFT_BY == 13 /\ 
         (forall i. forall j.
-            v (Seq.index (i0._super_4202118595671791609.f_repr (Seq.index re.f_simd_units i)) j) >= 0 /\
-            v (Seq.index (i0._super_4202118595671791609.f_repr (Seq.index re.f_simd_units i)) j) <= 261631)"#))]
+            v (Seq.index (i0._super_4731626403787200903.f_repr (Seq.index re.f_simd_units i)) j) >= 0 /\
+            v (Seq.index (i0._super_4731626403787200903.f_repr (Seq.index re.f_simd_units i)) j) <= 261631)"#))]
 pub(crate) fn shift_left_then_reduce<SIMDUnit: Operations, const SHIFT_BY: i32>(
     re: &mut PolynomialRingElement<SIMDUnit>,
 ) {
@@ -49,7 +49,7 @@ pub(crate) fn shift_left_then_reduce<SIMDUnit: Operations, const SHIFT_BY: i32>(
     (forall i. forall j. 
         Spec.Utils.is_i32b_array_opaque 
         (v ${crate::simd::traits::specs::FIELD_MAX}) 
-        (i0._super_4202118595671791609.f_repr (Seq.index (Seq.index t i).f_simd_units j)))"#))]
+        (i0._super_4731626403787200903.f_repr (Seq.index (Seq.index t i).f_simd_units j)))"#))]
 pub(crate) fn power2round_vector<SIMDUnit: Operations>(
     t: &mut [PolynomialRingElement<SIMDUnit>],
     t1: &mut [PolynomialRingElement<SIMDUnit>],
@@ -100,7 +100,7 @@ pub(crate) fn power2round_vector<SIMDUnit: Operations>(
          (forall i. forall j. 
             Spec.Utils.is_i32b_array_opaque 
             (v ${crate::simd::traits::specs::FIELD_MAX}) 
-            (i0._super_4202118595671791609.f_repr (Seq.index (Seq.index t i).f_simd_units j)))"#))]
+            (i0._super_4731626403787200903.f_repr (Seq.index (Seq.index t i).f_simd_units j)))"#))]
 pub(crate) fn decompose_vector<SIMDUnit: Operations>(
     dimension: usize,
     gamma2: Gamma2,
@@ -176,7 +176,7 @@ pub(crate) fn make_hint<SIMDUnit: Operations>(
          (forall i. forall j. 
             Spec.Utils.is_i32b_array_opaque 
             (v ${crate::simd::traits::specs::FIELD_MAX}) 
-            (i0._super_4202118595671791609.f_repr (Seq.index (Seq.index re_vector i).f_simd_units j)))"#))]
+            (i0._super_4731626403787200903.f_repr (Seq.index (Seq.index re_vector i).f_simd_units j)))"#))]
 pub(crate) fn use_hint<SIMDUnit: Operations>(
     gamma2: Gamma2,
     hint: &[[i32; COEFFICIENTS_IN_RING_ELEMENT]],

libcrux-ml-dsa/src/polynomial.rs

@@ -52,7 +52,7 @@ impl<SIMDUnit: Operations> PolynomialRingElement<SIMDUnit> {
     #[hax_lib::requires(fstar!(r#"v $bound > 0 /\ 
         (forall i. Spec.Utils.is_i32b_array_opaque 
             (v ${FIELD_MAX}) 
-            (i0._super_4202118595671791609.f_repr (Seq.index self.f_simd_units i)))"#))]
+            (i0._super_4731626403787200903.f_repr (Seq.index self.f_simd_units i)))"#))]
     pub(crate) fn infinity_norm_exceeds(&self, bound: i32) -> bool {
         let mut result = false;
         for i in 0..self.simd_units.len() {
@@ -64,8 +64,8 @@ impl<SIMDUnit: Operations> PolynomialRingElement<SIMDUnit> {
 
     #[inline(always)]
     #[hax_lib::requires(fstar!(r#"forall i. 
-        add_pre (i0._super_4202118595671791609.f_repr (Seq.index self.f_simd_units i)) 
-                (i0._super_4202118595671791609.f_repr (Seq.index rhs.f_simd_units i))"#))]
+        add_pre (i0._super_4731626403787200903.f_repr (Seq.index self.f_simd_units i)) 
+                (i0._super_4731626403787200903.f_repr (Seq.index rhs.f_simd_units i))"#))]
     pub(crate) fn add(&mut self, rhs: &Self) {
         #[cfg(hax)]
         let old_self = self.clone();
@@ -83,8 +83,8 @@ impl<SIMDUnit: Operations> PolynomialRingElement<SIMDUnit> {
 
     #[inline(always)]
     #[hax_lib::requires(fstar!(r#"forall i. 
-        sub_pre (i0._super_4202118595671791609.f_repr (Seq.index self.f_simd_units i)) 
-                (i0._super_4202118595671791609.f_repr (Seq.index rhs.f_simd_units i))"#))]
+        sub_pre (i0._super_4731626403787200903.f_repr (Seq.index self.f_simd_units i)) 
+                (i0._super_4731626403787200903.f_repr (Seq.index rhs.f_simd_units i))"#))]
     pub(crate) fn subtract(&mut self, rhs: &Self) {
         #[cfg(hax)]
         let old_self = self.clone();

libcrux-ml-kem/src/polynomial.rs

@@ -34,7 +34,7 @@ pub(crate) const VECTORS_IN_RING_ELEMENT: usize = 16;
     {| 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_16084754032855797384.f_repr 
+                                (Seq.index (i2._super_6081346371236564305.f_repr 
                                     (Seq.index p.f_coefficients (v i / 16))) (v i % 16)))
 let to_spec_vector_t (#r:Spec.MLKEM.rank) (#v_Vector: Type0)
     {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
@@ -186,7 +186,7 @@ fn add_to_ring_element<Vector: Operations, const K: usize>(
     let _myself = myself.coefficients;
     hax_lib::fstar!(
         r#"assert(forall (v: v_Vector).
-        i0.f_to_i16_array v == i0._super_16084754032855797384.f_repr v)"#
+        i0.f_to_i16_array v == i0._super_6081346371236564305.f_repr v)"#
     );
 
     for i in 0..myself.coefficients.len() {