diff --git a/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec b/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec index 36285bc8..c0a300ce 100644 --- a/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec +++ b/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 ->. diff --git a/proof/correctness/avx2/mlkem_filters_bridge.ec b/proof/correctness/avx2/mlkem_filters_bridge.ec index ab29dd1f..8ea0587c 100644 --- a/proof/correctness/avx2/mlkem_filters_bridge.ec +++ b/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().