From e29fc2db2a3ffe9b0589d3c0477b559ac9cdb59d Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Thu, 24 Oct 2024 20:51:03 +0100 Subject: [PATCH] Rewrites done --- easycrypt.project | 1 + proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec | 127 +++++++++++++++++- 2 files changed, 127 insertions(+), 1 deletion(-) diff --git a/easycrypt.project b/easycrypt.project index 842092c4..5a12003e 100644 --- a/easycrypt.project +++ b/easycrypt.project @@ -6,6 +6,7 @@ provers = CVC4@1.8 provers = Z3@4.8 rdirs = proof +rdirs = ../easycrypt/examples rdirs = Jasmin:jasmin/eclib idirs = code/jasmin/mlkem_ref/extraction idirs = code/jasmin/mlkem_avx2/extraction diff --git a/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec b/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec index 7ba7d70b..453f241a 100644 --- a/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec +++ b/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec @@ -30,7 +30,7 @@ import WArray512 WArray256. (* shake assumptions *) - +(* op SHAKE256_ABSORB4x_33 : W8.t Array33.t -> W8.t Array33.t -> W8.t Array33.t -> W8.t Array33.t -> W256.t Array25.t. op SHAKE256_SQUEEZENBLOCKS4x : W256.t Array25.t -> W256.t Array25.t * W8.t Array136.t * W8.t Array136.t * W8.t Array136.t * W8.t Array136.t. @@ -1267,6 +1267,7 @@ qed. (***************************************************) +*) import WArray960 WArray1536 Array4. module AuxPolyVecCompress10 = { @@ -1567,6 +1568,130 @@ lemma compress10_mr : equiv [AuxPolyVecCompress10.avx2 ~ AuxPolyVecCompress10.ref : lift_array768 bp{1} = lift_array768 bp{2}==> ={res}]. admitted. + +require import Bindings. +(* BINDINGS *) + +bind array Array256."_.[_]" Array256."_.[_<-_]" Array256.to_list Array256.of_list Array256.t 256. +realize tolistP by admit. +realize get_setP by admit. +realize eqP by admit. +realize get_out by admit. + + +bind array Array768."_.[_]" Array768."_.[_<-_]" Array768.to_list Array768.of_list Array768.t 768. +realize tolistP by admit. +realize get_setP by admit. +realize eqP by admit. +realize get_out by admit. + +bind array Array32."_.[_]" Array32."_.[_<-_]" Array32.to_list Array32.of_list Array32.t 32. +realize tolistP by admit. +realize get_setP by admit. +realize eqP by admit. +realize get_out by admit. + +bind array Array960."_.[_]" Array960."_.[_<-_]" Array960.to_list Array960.of_list Array960.t 960. +realize tolistP by admit. +realize get_setP by admit. +realize eqP by admit. +realize get_out by admit. + + +op init_256_16 (f: int -> W16.t) : W16.t Array256.t = Array256.init f. + +bind op [W16.t & Array256.t] init_256_16 "ainit". +realize bvainitP by admit. + + +op init_768_16 (f: int -> W16.t) : W16.t Array768.t = Array768.init f. + +bind op [W16.t & Array768.t] init_768_16 "ainit". +realize bvainitP by admit. + +op init_960_8 (f: int -> W8.t) : W8.t Array960.t = Array960.init f. + +bind op [W8.t & Array960.t] init_960_8 "ainit". +realize bvainitP by admit. + + +print Array768.to_list. + +op sliceget256_16_256 (arr: W16.t Array256.t) (i: int) : W256.t. + +bind op [W16.t & W256.t & Array256.t] sliceget256_16_256 "asliceget". +realize bvaslicegetP by admit. + +op sliceset256_16_256 (arr: W16.t Array256.t) (i: int) (bv: W256.t) : W16.t Array256.t. + +bind op [W16.t & W256.t & Array256.t] sliceset256_16_256 "asliceset". +realize bvaslicesetP by admit. + +op sliceget32_8_256 (arr: W8.t Array32.t) (i: int) : W256.t. + +bind op [W8.t & W256.t & Array32.t] sliceget32_8_256 "asliceget". +realize bvaslicegetP by admit. + +op sliceget768_16_256 (arr: W16.t Array768.t) (i: int) : W256.t. + +bind op [W16.t & W256.t & Array768.t] sliceget768_16_256 "asliceget". +realize bvaslicegetP by admit. + +op sliceset960_8_128 (arr: W8.t Array960.t) (i: int) (bv: W128.t) : W8.t Array960.t. + +bind op [W8.t & W128.t & Array960.t] sliceset960_8_128 "asliceset". +realize bvaslicesetP by admit. + + +op sliceset960_8_32 (arr: W8.t Array960.t) (i: int) (bv: W32.t) : W8.t Array960.t. + +bind op [W8.t & W32.t & Array960.t] sliceset960_8_32 "asliceset". +realize bvaslicesetP by admit. + +print pvc_shufbidx_s. + +op lane (w: W16.t) = w. +op pcond (w: W16.t) = true. + +lemma blah (_bp : W16.t Array768.t) : hoare [ AuxPolyVecCompress10.avx2 : true ==> false]. +proof. +proc. +inline *. +proc change 2 : (init_256_16 (fun i => r.[i])); auto. +proc change ^while.1 : (sliceget256_16_256 ap i0). by admit. +proc change ^while.11 : (sliceset256_16_256 ap i0 a1). by admit. + +proc change 9 : (init_768_16 (fun i => if 0 <= i && i < 256 then aux.[i] else r.[i])). +by auto. +proc change 10 : (init_256_16 (fun i => r.[256 + i])). by auto. +proc change ^while{2}.1 : (sliceget256_16_256 ap0 i1). by admit. +proc change ^while{2}.11 : (sliceset256_16_256 ap0 i1 a2). by admit. + +proc change 17 : (init_768_16 (fun i => if 256 <= i && i < 256 + 256 then aux.[i - 256] else r.[i])). by auto. +proc change 18 : (init_256_16 (fun i => r.[2*256 + i])). by auto. +proc change ^while{3}.1 : (sliceget256_16_256 ap1 i2). by admit. +proc change ^while{3}.11 : (sliceset256_16_256 ap1 i2 a3). by admit. + +proc change 25 : (init_768_16 (fun i => if 2 * 256 <= i < 3 * 256 then aux.[i - 2 * 256] else r.[i])). by auto. + +proc change 35 : (sliceget32_8_256 pvc_shufbidx_s 0). by admit. + +proc change ^while{4}.1 : (sliceget768_16_256 a i). by admit. + +proc change ^while{4}.25 : (init_960_8 (fun i => (sliceset960_8_128 rr0 (i * 20) lo).[i])). by admit. +proc change ^while{4}.26 : (init_960_8 (fun i => (sliceset960_8_32 rr0 (i * 20 + 16) (VPEXTR_32 hi W8.zero)).[i])).by admit. + +cfold 36. +unroll for 37. +cfold 36. unroll for 23. cfold 22. +unroll for 15. cfold 14. unroll for 7. cfold 6. + +bdep 16 16 [_bp] [bp] [ap] lane pcond. + +print get256_direct. + + + lemma compress10_equiv : equiv [ AuxPolyVecCompress10.avx2_orig ~ AuxPolyVecCompress10.ref_orig : lift_array768 bp{1} = lift_array768 bp{2} /\ valid_ptr (to_uint ctp{1}) (128 + 3 * 320) /\ ={ctp,Glob.mem} ==> ={Glob.mem}].