From e03f62ff78491cb8dee76a015ea2c55de8ce0e19 Mon Sep 17 00:00:00 2001 From: Manuel Barbosa Date: Mon, 17 Feb 2025 19:41:26 +0000 Subject: [PATCH 1/4] stronger contract --- .../correctness/avx2/mlkem_filters_bridge.ec | 31 ++++++++++--------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/proof/correctness/avx2/mlkem_filters_bridge.ec b/proof/correctness/avx2/mlkem_filters_bridge.ec index 614f17fa..191956e8 100644 --- a/proof/correctness/avx2/mlkem_filters_bridge.ec +++ b/proof/correctness/avx2/mlkem_filters_bridge.ec @@ -260,7 +260,7 @@ rewrite /plist !nth_mkseq 1:/# => ->. rewrite (nth_cat witness) ifF; 1: smt(size_mkseq). smt(nth_mkseq size_mkseq). qed. -(* + lemma bridge48 _ctr _offset _p : equiv [ Jkem_avx2.M(Jkem_avx2.Syscall).__gen_matrix_buf_rejection_filter48 ~ Filters.filter48 : @@ -759,7 +759,6 @@ proof. conseq buf_rejection_filter48_ll (buf_rejection_filter48_h _pol _ctr _buf _buf_offset). smt(). qed. -*) from JazzEC require import Array16. @@ -965,10 +964,11 @@ hoare buf_rejection_filter24_h _pol _ctr _buf _buf_offset: /\ buf_offset = _buf_offset /\ auxdata_ok load_shuffle mask bounds ones sst ==> - let l = take (256-to_uint _ctr) (rejection16 (buf_subl _buf (to_uint _buf_offset) (to_uint _buf_offset + 24))) - in plist res.`1 (to_uint _ctr + size l) - = plist _pol (to_uint _ctr) ++ l - /\ to_uint _ctr + size l <= to_uint res.`2. + let l = rejection16 (buf_subl _buf (to_uint _buf_offset) (to_uint _buf_offset + 24)) in + let lused = take (256-to_uint _ctr) l + in plist res.`1 (to_uint _ctr + size lused) + = plist _pol (to_uint _ctr) ++ lused + /\ to_uint res.`2 = to_uint _ctr + size l. proof. conseq (bridge24 (to_uint _ctr) (to_uint _buf_offset) _pol)(filter24P (Array32.init (fun i => _buf.[to_uint _buf_offset+i]))). + move => &1 [#] ??????;rewrite /auxdata_ok => [#] ->->->->->. @@ -977,7 +977,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) /=. @@ -988,16 +988,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(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(). @@ -1106,10 +1106,11 @@ phoare buf_rejection_filter24_ph _pol _ctr _buf _buf_offset: /\ buf_offset = _buf_offset /\ auxdata_ok load_shuffle mask bounds ones sst ==> - let l = take (256-to_uint _ctr) (rejection16 (buf_subl _buf (to_uint _buf_offset) (to_uint _buf_offset + 24))) - in plist res.`1 (to_uint _ctr + size l) - = plist _pol (to_uint _ctr) ++ l - /\ to_uint _ctr + size l <= to_uint res.`2] = 1%r. + let l = rejection16 (buf_subl _buf (to_uint _buf_offset) (to_uint _buf_offset + 24)) in + let lused = take (256-to_uint _ctr) l + in plist res.`1 (to_uint _ctr + size lused) + = plist _pol (to_uint _ctr) ++ lused + /\ to_uint res.`2 = to_uint _ctr + size l] = 1%r. proof. by conseq buf_rejection_filter24_ll (buf_rejection_filter24_h _pol _ctr _buf _buf_offset). qed. From fa025f41e5144ea33986b874ba6aa72550cbee3d Mon Sep 17 00:00:00 2001 From: Manuel Barbosa Date: Mon, 17 Feb 2025 21:40:07 +0000 Subject: [PATCH 2/4] some progress --- jasmin | 2 +- .../correctness/avx2/MLKEM_genmatrix_avx2.ec | 81 ++++++++++--------- 2 files changed, 43 insertions(+), 40 deletions(-) diff --git a/jasmin b/jasmin index f6eca756..b46561be 160000 --- a/jasmin +++ b/jasmin @@ -1 +1 @@ -Subproject commit f6eca756f16538217e9af7d46952c43f26546a09 +Subproject commit b46561bea9ba1ff66cbc78835f6fa2e04622cc56 diff --git a/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec b/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec index abd41160..9ed090dd 100644 --- a/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec +++ b/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec @@ -509,14 +509,14 @@ 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 - /\ res.`2 = W64.of_int (to_uint _ctr + size l). + /\ 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 /\ 0 <= to_uint _buf_offset <= to_uint buf_offset <= 504 /\ - 0 <= to_uint _ctr <= to_uint counter <= 256 /\ + 0 <= to_uint _ctr <= min 256 (to_uint counter) /\ 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) ++ take (256-to_uint _ctr) (rejection16 (buf_subl _buf (to_uint _buf_offset) (to_uint buf_offset))) ) /\ @@ -525,20 +525,26 @@ while ( buf=_buf /\ 24 %| to_uint buf_offset /\ 3 %| to_uint _buf_offset /\ /\ to_uint buf_offset <= 504-24))). ecall (conditionloop_h buf_offset (3 * 168 - 24) counter 256); simplify. wp; ecall (buf_rejection_filter24_h pol counter buf buf_offset). - auto => &m /> Hdvd1 Hdvd2 Ho1 Ho2 Ho3 Hctr1 Hctr2 Hctr3 H Hcond1 Hcond2. + auto => &m /> Hdvd1 Hdvd2 Ho1 Ho2 Ho3 Hctr1 + + Hcond1 Hcond2. + have -> : min 256 (to_uint counter{m}) = to_uint counter{m} by smt(). + move => Hctr2 H. have Hsz: to_uint counter{m} = to_uint _ctr + min (256-to_uint _ctr) (size (rejection16 (buf_subl buf{m} (to_uint _buf_offset) (to_uint buf_offset{m})))). rewrite -(size_plist pol{m} (to_uint counter{m})) 1:/# H size_cat size_plist 1:/#; congr. by rewrite size_take_min /#. - move: H; rewrite take_oversize 1:/# => H [p c' ms'] /= />. - rewrite !of_uintK => Hstep. + split;1:smt(). + move => Ho4 Hctr4. + move: H; rewrite take_oversize 1:/# => H [p c' ms'] /= /> + Hsizecp. + have -> : (to_uint counter{m} + + size + (take (256 - to_uint counter{m}) + (rejection16 (buf_subl buf{m} (to_uint buf_offset{m}) (to_uint buf_offset{m} + 24))))) = min 256 (to_uint c') by smt(@List). + move => Hstep. rewrite !to_uintD_small 1:/# !of_uintK; split; first smt(). split. split; first by rewrite !modz_small 1:// /= /#. by move=> *; rewrite !modz_small 1:// /= /#. split. - by rewrite size_take_min 1:/# modz_small; smt(size_ge0). - rewrite modz_small; first smt(size_ge0 size_take_min). - rewrite modz_small 1:/#. + by smt(size_ge0). rewrite Hstep H -catA; congr. rewrite -(buf_subl_cat _ (to_uint _buf_offset) (to_uint buf_offset{m}) (to_uint buf_offset{m} + 24)) 1:/#. rewrite rejection16_cat. @@ -550,7 +556,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 /\ @@ -560,18 +566,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:/#. @@ -588,36 +596,31 @@ 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 /#. -move=> buf_o2 cond2 ctr2 pol2 HC2 Hdvd3 Hbo4 Hbo5 Hctr5 Hctr6 HH. -case: (to_uint ctr2 < 256) => /= C1. +move => buf_o cond ctr ppol Hcond Hdvd1 Hdvd2 Hbo1 Hbo2 Hbo3 Hctr3 Hctr4 ? H Hsz Hterm; split;1: by rewrite take_oversize /#. +move=> buf_o2 cond2 ctr2 pol2 HC2 Hdvd3 Hbo4 Hbo5 Hctr5 HH. + +case: ((min 256 (to_uint ctr2)) < 256) => /= C1. move=> C2; move: HH; have ->: to_uint buf_o2 = 504 by smt(). - move => HH; rewrite andbC -andaE to_uint_eq of_uintK modz_small. - split=> *; first smt(size_ge0). - by rewrite size_take /#. - split. - rewrite -(size_plist pol2 (to_uint ctr2)) 1:/#. - by rewrite HH size_cat size_plist 1:/#. - by move => E; move: HH; rewrite E => ->. -have E: to_uint ctr2 = 256 by smt(). -rewrite to_uint_eq andbC -andaE. -have HHsz: 256 = to_uint counter{m} + min (256 - to_uint counter{m}) - (size (rejection16 (buf_subl buf{m} (to_uint buf_offset{m}) (to_uint buf_o2)))). - rewrite -(size_plist pol2 256) 1:/#. - by rewrite -E HH size_cat size_plist 1:/# size_take_min /#. -rewrite size_take_min 1:/#. -rewrite of_uintK modz_small; first smt(size_ge0). -split; first smt(size_rejection16_le). + move => HH; rewrite andbC -andaE. + split; 1: + rewrite -(size_plist pol2 (to_uint ctr2)) 1:/#; + by smt(size_take size_ge0 size_map size_cat size_plist). +move => ?; move: HH; have ->: (min 256 (to_uint ctr2)) = 256 by smt(). + move => HH; rewrite andbC -andaE. +??? +(* +split; 1: admit. +move => ->. + smt(size_rejection16_le take_rejection16_done size_take @List). move => <-; rewrite HH; congr. apply take_rejection16_done; first 3 smt(). -by rewrite size_take_min /#. +by rewrite size_take_min /#. *) + qed. lemma gen_matrix_buf_rejection_ll: From 840aee3cb4da1b6d3327a3eb82e00149ed3550a9 Mon Sep 17 00:00:00 2001 From: Manuel Barbosa Date: Mon, 17 Feb 2025 23:15:37 +0000 Subject: [PATCH 3/4] progress --- .../correctness/avx2/MLKEM_genmatrix_avx2.ec | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec b/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec index 9ed090dd..53a0ec04 100644 --- a/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec +++ b/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec @@ -605,21 +605,21 @@ move => buf_o cond ctr ppol Hcond Hdvd1 Hdvd2 Hbo1 Hbo2 Hbo3 Hctr3 Hctr4 ? H Hsz move=> buf_o2 cond2 ctr2 pol2 HC2 Hdvd3 Hbo4 Hbo5 Hctr5 HH. case: ((min 256 (to_uint ctr2)) < 256) => /= C1. - move=> C2; move: HH; have ->: to_uint buf_o2 = 504 by smt(). + move=> C2; move: HH; have ->: to_uint buf_o2 = 504; + by smt(size_take size_ge0 size_map size_cat size_plist). +move => C2; move: HH; have ->: (min 256 (to_uint ctr2)) = 256 by smt(). move => HH; rewrite andbC -andaE. - split; 1: - rewrite -(size_plist pol2 (to_uint ctr2)) 1:/#; - by smt(size_take size_ge0 size_map size_cat size_plist). -move => ?; move: HH; have ->: (min 256 (to_uint ctr2)) = 256 by smt(). - move => HH; rewrite andbC -andaE. -??? -(* -split; 1: admit. -move => ->. - smt(size_rejection16_le take_rejection16_done size_take @List). -move => <-; rewrite HH; congr. -apply take_rejection16_done; first 3 smt(). -by rewrite size_take_min /#. *) + have ? : size (plist pol2 256) = 256 by smt(size_mkseq). + have? := size_rejection16_le buf{m} (to_uint buf_offset{m}) (to_uint buf_o2) 504 _ _ _ _ ;1..4: smt(). + split. + + have : size(plist pol{m} (to_uint counter{m}) ++ + take (256 - to_uint counter{m}) (rejection16 (buf_subl buf{m} (to_uint buf_offset{m}) (to_uint buf_o2)))) = to_uint counter{m} + size (take (256 - to_uint counter{m}) (rejection16 (buf_subl buf{m} (to_uint buf_offset{m}) 504))); last by + smt(). + rewrite size_cat; congr; 1: by smt(size_plist). + by smt(@List size_plist). + have := take_rejection16_done (256 - to_uint counter{m}) buf{m} (to_uint buf_offset{m}) (to_uint buf_o2) _ _ _ _ ;1..3: smt(). +smt(size_plist size_take @List). +by smt(). qed. From e5a489bc3ee86ca8d111c84d052e33e3edab3549 Mon Sep 17 00:00:00 2001 From: Manuel Barbosa Date: Tue, 18 Feb 2025 00:05:04 +0000 Subject: [PATCH 4/4] progress --- proof/correctness/avx2/MLKEM_genmatrix_avx2.ec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec b/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec index 53a0ec04..c2b6848d 100644 --- a/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec +++ b/proof/correctness/avx2/MLKEM_genmatrix_avx2.ec @@ -677,7 +677,7 @@ phoare gen_matrix_buf_rejection_ph _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 - /\ res.`2 = W64.of_int (to_uint _ctr + size l) + /\ to_uint _ctr + size l = min 256 (to_uint res.`2) ] = 1%r. proof. by conseq gen_matrix_buf_rejection_ll (gen_matrix_buf_rejection_h _pol _ctr _buf _buf_offset).