cleanup

cryspen · Jan 29, 2025 · f24b1be · f24b1be
1 parent 9bbaa3c
commit f24b1be
Showing 1 changed file with 3 additions and 16 deletions.
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Encoding.Commitment.fst
@@ -118,29 +118,16 @@ let serialize_4_
               inp (v i * 8 + n);
               == {}
               get_bit (Seq.index simd_unit.f_values ((v i * 8 + n) / 4)) (sz ((v i * 8 + n) % 4));
-              == {
-                Math.Lemmas.division_addition_lemma n 4 (v i * 2);
-                assert ((n + (v i * 2) * 4) / 4 == n / 4 + v i * 2);
-                assert_spinoff ((v i * 8 + n) % 4 == n % 4)
-              }
+              == { Math.Lemmas.division_addition_lemma n 4 (v i * 2) }
               get_bit (Seq.index simd_unit.f_values (v i * 2 + n / 4)) (sz (n % 4));
-              == {
-                assert (coefficients == Seq.slice simd_unit.f_values (v i * 2) (v i * 2 + 2))
-              }
+              == {}
               get_bit (Seq.index coefficients (n / 4)) (sz (n % 4));
               == {}
               bit_vec_of_int_t_array #I32 #(mk_usize 2) coefficients 4 n;
-              == {}
-              get_bit r0 (mk_int n);
-              == {
-                lemma_small_div_add (v i) 8 n; lemma_small_mod_add (v i) 8 n;
-                assert (out (v i * 8 + n) == get_bit (Seq.index serialized (v i)) (sz n))
-              }
+              == {lemma_small_div_add (v i) 8 n; lemma_small_mod_add (v i) 8 n}
               out (v i * 8 + n);
             });
-
             assert (forall (n: nat {n < v i * 8 + 8}). out n == inp n);
-            assert ((Core.Slice.impl__len #u8 serialized <: usize) =. mk_usize 4);
           serialized)
   in
   let _:Prims.unit = () <: Prims.unit in