merge filter24 proofs

proof/correctness/avx2/MLKEM_genmatrix_avx2.ec

@@ -509,7 +509,7 @@ hoare gen_matrix_buf_rejection_h _pol _ctr _buf _buf_offset:
    let l = take (256-to_uint _ctr) (rejection16 (buf_subl _buf (to_uint _buf_offset) 504))
    in plist res.`1 (to_uint _ctr + size l)
       = plist _pol (to_uint _ctr) ++ l
-      /\ to_uint _ctr + size l = min 256 (W64.to_uint res.`2).
+      /\ to_uint _ctr + size l = min 256 (to_uint res.`2).
 proof.
 proc; simplify.
 while ( buf=_buf /\ 24 %| to_uint buf_offset /\ 3 %| to_uint _buf_offset /\
@@ -537,7 +537,6 @@ while ( buf=_buf /\ 24 %| to_uint buf_offset /\ 3 %| to_uint _buf_offset /\
   split; first by rewrite !modz_small 1:// /= /#.
   by move=> *; rewrite !modz_small 1:// /= /#.
  split; first smt(size_ge0). 
-(* by rewrite size_take_min 1:/# modz_small; smt(size_ge0). *)
  rewrite modz_small; first smt(size_ge0 size_take_min).
  rewrite Hc'.
  rewrite Hstep H -catA; congr.
@@ -551,7 +550,7 @@ while ( buf=_buf /\ 24 %| to_uint buf_offset /\ 3 %| to_uint _buf_offset /\
         0 <= to_uint _buf_offset <= to_uint buf_offset <= 504 /\
         0 <= to_uint _ctr <= to_uint counter <= 256 /\
         auxdata_ok load_shuffle mask bounds ones sst /\
-        plist pol (to_uint counter)
+        plist pol (min 256 (to_uint counter))
         = plist _pol (to_uint _ctr)
            ++ rejection16 (buf_subl _buf (to_uint _buf_offset) (to_uint buf_offset)) /\
         to_uint _ctr + size (rejection16 (buf_subl _buf (to_uint _buf_offset) (to_uint buf_offset))) <= 256 /\
@@ -561,18 +560,20 @@ while ( buf=_buf /\ 24 %| to_uint buf_offset /\ 3 %| to_uint _buf_offset /\
  ecall (conditionloop_h buf_offset (3 * 168 - 48) counter (256-32+1)); simplify.
  wp; ecall (buf_rejection_filter48_h pol counter buf buf_offset).
  auto => &m />.
- move => Hdvd1 Hdvd2 Ho1 Ho2 Ho3 Hctr1 Hctr2 Hctr3 H Hbo Hctr4 Hbo4.
+ move => Hdvd1 Hdvd2 Ho1 Ho2 Ho3 Hctr1 Hctr2 Hctr3 + Hbo Hctr4 Hbo4.
+ have -> : (min 256 (to_uint counter{m})) = to_uint counter{m} by smt().
+ move => H.
  split;1:smt().
  move => ? [p c'] /= /> Hstep. 
  rewrite !to_uintD_small 1:/# !of_uintK; split; first smt().
- split.
-  by rewrite !modz_small 1:// /= /#.
+ split;1: by rewrite !modz_small 1:// /= /#.
  pose R:= rejection16 _.
  have ?: 0 <= size R <= 32.
   rewrite /rejection16 size_map; split; first smt(size_ge0).
   move=> _; apply (size_rejection_le' 48); 1:done => /=.
   by rewrite /buf_subl !size_take 1:/# !size_drop /#.
  rewrite !modz_small 1..2:/#.
+  have -> : (min 256 (to_uint counter{m} + size R)) = to_uint counter{m} + size R by smt().
  split; first smt().
  rewrite -andaE; split.
   rewrite -(buf_subl_cat _ (to_uint _buf_offset) (to_uint buf_offset{m}) (to_uint buf_offset{m} + 48)) 1:/#.
@@ -589,11 +590,10 @@ wp; skip => &m /> Hctr1 Hctr2 Hbo; split.
  split; first smt().
  split; first smt().
  split; first smt().
- split.
-  by rewrite pack32_sample_load_shuffle.
- split.
-  by rewrite buf_subl0 1:/# /rejection16 rejection0 cats0.
- split; last smt().
+ split; 1:  by rewrite pack32_sample_load_shuffle.
+ have -> : (min 256 (to_uint counter{m})) = to_uint counter{m} by smt().
+ split; 1: by rewrite buf_subl0 1:/# /rejection16 rejection0 cats0.
+ split; last  by smt().
  by rewrite buf_subl0 1:/# /rejection16 rejection0 /#.
 move => buf_o cond ctr pol Hcond Hdvd1 Hdvd2 Hbo1 Hbo2 Hbo3 Hctr3 Hctr4 _ H Hsz Hterm; split.
  by rewrite take_oversize /#. 
@@ -879,8 +879,6 @@ lemma sub_gen_matrix_indexes idxs _pos _t _k (_a:WArray8.t):
    (get8
       (set64_direct _a 0
          (pack8 (sub gen_matrix_indexes (2 * _pos + 16 * b2i _t) 8)))) =>
-(*
- idxs = Array8.of_list witness (sub gen_matrix_indexes (2*_pos + 16 * b2i _t) 8) =>*)
  sub idxs (2*_k) 2 = [(pos2ji (_pos+_k) _t).`1; (pos2ji (_pos+_k) _t).`2].
 proof.
 move=> Hpos Hk ->.

proof/correctness/avx2/mlkem_filters_bridge.ec

@@ -1000,7 +1000,7 @@ conseq  (bridge24 (to_uint _ctr) (to_uint _buf_offset) _pol)(filter24P (Array32.
     + rewrite /Mlkem_filters.load_shuffle /Mlkem_filters.load_shuffle /u8_256_32.
       rewrite wordP => i ib;rewrite pack32wE 1:/# of_listK /= 1:/# initiE 1:/# /=;do      congr;rewrite /Mlkem_filters.sample_load_shuffle.
       rewrite !get_of_list 1,2:/#. 
-      by smt(@List).
+      by smt().
   + by move => *; rewrite initiE /#. 
 + move => &1 &2 /=.
   rewrite /rejection16 /buf_subl /rejection /= -map_comp /(\o) /=.
@@ -1011,16 +1011,16 @@ conseq  (bridge24 (to_uint _ctr) (to_uint _buf_offset) _pol)(filter24P (Array32.
   have ? : map W12.to_uint xx = map W16.to_uint yy; last first.
   move => /= ? [# Hs1 Hs2] [# Hl1 Hl2] .
   split; last first. 
-  + rewrite Hs2 Hl2  /yy; smt(@List take_oversize size_ge0 count_size size_filter size_bytes2coeffs W64.to_uint_cmp size_drop Array536.size_to_list).
+  + rewrite Hs2 Hl2 /yy; smt(@List size_map take_oversize size_ge0 count_size size_filter size_bytes2coeffs W64.to_uint_cmp size_drop Array536.size_to_list).
   + move :Hs1.
-    have ->: (min 256 (to_uint res{1}.`2)) = to_uint _ctr + size (take (256 - to_uint _ctr) yy) by smt(@List take_oversize size_ge0 count_size size_filter size_bytes2coeffs W64.to_uint_cmp size_drop Array536.size_to_list).
+    have ->: (min 256 (to_uint res{1}.`2)) = to_uint _ctr + size (take (256 - to_uint _ctr) yy) by smt(size_take size_map take_oversize size_ge0 count_size size_filter size_bytes2coeffs W64.to_uint_cmp size_drop Array536.size_to_list).
     move => ->.
     congr. 
     apply (eq_from_nth witness).
-    + rewrite size_mkseq. smt(size_ge0).
+    + rewrite size_mkseq;1: smt(size_ge0).
     rewrite size_mkseq => i ib.
     rewrite nth_mkseq;1:smt(size_ge0).
-    rewrite Hl1;1:smt(size_ge0 @List).   
+    rewrite Hl1;1:smt(size_ge0 size_map size_take).   
     rewrite to_uint_eq.
     rewrite -BVA_zextend_Top_Bindings_W12_t_Top_JWord_W16_t.bvzextendP.
     have : nth witness (map W12.to_uint xx) i  = nth witness (map W16.to_uint yy) i by smt().