add admits to broken proofs

formosa-crypto · Dec 2, 2024 · d06f818 · d06f818
1 parent 0504dae
commit d06f818
Show file tree

Hide file tree

Showing 5 changed files with 215 additions and 119 deletions.
diff --git a/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec b/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec
@@ -25,11 +25,15 @@ import MLKEM_PolyVec.
 import MLKEM_PolyvecAVX.
 import MLKEM_PolyAVXVec.
 import NTT_Avx2.
-import WArray136 WArray32 WArray128.
+(*import WArray136 WArray32 WArray128.*)
+import WArray32 WArray128.
 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.
@@ -111,6 +115,7 @@ unroll for ^while; auto.
 conseq => /=.
 inline *; unroll for ^while; auto.
 qed.
+*)
 
 (*
 axiom shake128_equiv_absorb : equiv [ M(Syscall)._shake128_absorb34 ~ 
@@ -782,6 +787,7 @@ proc*.
 transitivity{2} { r <@ AuxMLKEMAvx2.__poly_getnoise_eta1_4x(aux3,aux2,aux1,aux0,noiseseed,nonce); } ((r0{1}, r1{1}, r2{1}, r3{1}, seed{1}, nonce{1}) = (aux3{2}, aux2{2}, aux1{2}, aux0{2}, noiseseed{2}, nonce{2}) ==> ={r}) (={aux3,aux2,aux1,aux0,noiseseed,nonce} ==> ={r}); last first.
 symmetry. call getnoise_4x_split => />. auto => />. smt(). smt().
 (*main proof*)
+admit(*
 inline Jkem_avx2.M(Jkem_avx2.Syscall)._poly_getnoise_eta1_4x AuxMLKEMAvx2.__poly_getnoise_eta1_4x AuxMLKEMAvx2._poly_getnoise. swap{2} [30..31] 5. swap{2} [23..24] 10. swap{2} [16..17] 15.
 seq 25 30 : (
     r00{1}=rp{2}  /\ Array128.init (fun (i : int) => buf0{1}.[i]) =buf{2}
@@ -805,15 +811,19 @@ wp. call getnoise_1x_equiv_avx => />.
 wp. call getnoise_1x_equiv_avx => />.
 wp. call getnoise_1x_equiv_avx => />.
 wp. call getnoise_1x_equiv_avx => />.
-auto => />. qed.
+auto => />. 
+*).
+qed.
 
 lemma polygetnoise_ll : islossless Jkem.M(Jkem.Syscall)._poly_getnoise.
 proc. 
+admit(*
 while (0 <= to_uint i <= 128) (128 - to_uint i);
   1: by move => z; auto => />;rewrite  ultE /= => &hr ???; rewrite !to_uintD_small /=; smt(to_uint_cmp).
 wp; call sha3ll; wp; while (0<=k<=32) (32 -k); 1: by move => z; auto=> /> /#.
 auto => /> *; do split; 1:smt(). 
 by move => *; rewrite ultE /=; smt().
+*).
 qed.
 
 equiv getnoiseequiv : 
@@ -883,8 +893,9 @@ unroll for* {1} 36.
 
 sp 3 3.
 
-seq 15 17  : (#pre /\ ={publicseed, noiseseed,e,skpv,pkpv} /\ sskp{2} = skp{1} /\ spkp{2} = pkp{1}); 1: by
- sp; conseq />; sim 2 2; call( sha3equiv); conseq />; sim. 
+seq 15 17  : (#pre /\ ={publicseed, noiseseed,e,skpv,pkpv} /\ sskp{2} = skp{1} /\ spkp{2} = pkp{1}).
+ admit(* 1: by
+ sp; conseq />; sim 2 2; call( sha3equiv); conseq />; sim. *).
 
 sp 0 2.
 seq 2 2 : (#pre /\ aa{1} = nttunpackm a{2} /\
@@ -1310,14 +1321,14 @@ transitivity {1} {Jkem.M(Jkem.Syscall).__indcpa_enc(sctp,msgp,pkp,noiseseed);}
 
 inline{1} 1; inline {2} 1. wp.
 
-seq 50 59 : (={ctp,Glob.mem} /\
+seq 51 59 : (={ctp,Glob.mem} /\
      pos_bound256_cxq v{1} 0 256 2 /\
      pos_bound256_cxq v{2} 0 256 2 /\
     lift_array256 v{1} = lift_array256 v{2} /\ 
     valid_ptr (to_uint ctp{1}) 128); last by
   exists *Glob.mem{1}, (to_uint ctp{1}); elim* => memm _p; call (compressequiv memm _p); auto.
 
-seq 48 57 : (={ctp,Glob.mem} /\
+seq 49 57 : (={ctp,Glob.mem} /\
      pos_bound256_cxq v{1} 0 256 2 /\
      pos_bound256_cxq v{2} 0 256 2 /\
      pos_bound768_cxq bp{1} 0 768 2 /\
@@ -1338,7 +1349,7 @@ have H := polyvec_add2_equiv_noperm 2 2 _ _ => //.
 ecall (H (lift_array768 bp{2}) (lift_array768 ep{2})); clear H.
 
 
-unroll for* {1} 39.
+unroll for* {1} 40.
 
 swap {1} 3 -2; swap {2} 3 -2; seq 1 1: (#pre /\ ={pkp0} /\ pkp0{2}=pkp{1}); 1: by auto.
 sp 3 3.
@@ -1378,13 +1389,14 @@ seq 18 17  : (#pre /\ ={publicseed, bp,ep,epp,v,sp_0,k} /\
 sp 2 0.
 (* swap {1} [11..12] 2. *)
 
-seq 11 20 : (#{/~bp{1}=bp{2}}pre  /\
+seq 12 20 : (#{/~bp{1}=bp{2}}pre  /\
     signed_bound768_cxq sp_0{1} 0 768 1 /\
     signed_bound768_cxq ep{1} 0 768 1 /\
     signed_bound_cxq epp{1} 0 256 1 /\
     signed_bound768_cxq sp_0{2} 0 768 1 /\
     signed_bound768_cxq ep{2} 0 768 1 /\ 
     signed_bound_cxq epp{1} 0 256 1).
+admit(*
 + conseq />.
   transitivity {1} { (sp_0,ep,bp,epp) <@ GetNoiseAVX2.samplenoise_enc(sp_0,ep,bp, epp,noiseseed);} (lnoiseseed{1} = noiseseed{2} /\ ={sp_0,ep,bp,epp} ==> ={sp_0,ep,epp}) 
    (
@@ -1454,7 +1466,7 @@ seq 11 20 : (#{/~bp{1}=bp{2}}pre  /\
   case (256 <= x && x < 512); 1: by smt().
   move => *; rewrite !initiE //= fun_if. 
   by smt().
-
+*).
 swap {1} 1 2.
 seq 1 1 : (#{/~sp_0{1}}{~sp_0{2}}pre /\ 
            lift_array768 sp_0{1} = nttunpackv (lift_array768 sp_0{2}) /\
@@ -1690,13 +1702,13 @@ transitivity {1} { r <@Jkem.M(Jkem.Syscall).__iindcpa_enc(ctp,msgp,pkp,noiseseed
 
 inline{1} 1; inline {2} 1. wp.
 
-seq 49 61 : (={ctp0,Glob.mem} /\ Glob.mem{1} = mem /\
+seq 50 61 : (={ctp0,Glob.mem} /\ Glob.mem{1} = mem /\
      pos_bound256_cxq v{1} 0 256 2 /\
      pos_bound256_cxq v{2} 0 256 2 /\
     lift_array256 v{1} = lift_array256 v{2}); last by
   exists *Glob.mem{1}; elim* => memm; call (compressequiv_1 memm); auto => />; smt(Array1088.tP Array1088.initiE).
 
-seq 47  59 : (={ctp0,Glob.mem} /\ Glob.mem{1} = mem /\
+seq 48  59 : (={ctp0,Glob.mem} /\ Glob.mem{1} = mem /\
      pos_bound256_cxq v{1} 0 256 2 /\
      pos_bound256_cxq v{2} 0 256 2 /\
      pos_bound768_cxq bp{1} 0 768 2 /\
@@ -1715,7 +1727,7 @@ have H := polyvec_add2_equiv_noperm 2 2 _ _ => //.
 ecall (H (lift_array768 bp{2}) (lift_array768 ep{2})); clear H.
 
 
-unroll for* {1} 39.
+unroll for* {1} 40.
 
 swap {1} 3 -2; swap {2} 3 -2; seq 1 1: (#pre /\ ={pkp0} /\ pkp0{2} = pkp{1}); 1: by auto.
 sp 3 3.
@@ -1758,13 +1770,14 @@ seq 18 19  : (#pre /\ ={publicseed, bp,ep,epp,v,sp_0,k} /\ ctp{2} = sctp{2} /\
 sp 2 0.
 (* swap {1} [11..12] 2. *)
 
-seq 12 20 : (#{/~bp{1}=bp{2}}pre  /\
+seq 13 20 : (#{/~bp{1}=bp{2}}pre  /\
     signed_bound768_cxq sp_0{1} 0 768 1 /\
     signed_bound768_cxq ep{1} 0 768 1 /\
     signed_bound_cxq epp{1} 0 256 1 /\
     signed_bound768_cxq sp_0{2} 0 768 1 /\
     signed_bound768_cxq ep{2} 0 768 1 /\ 
     signed_bound_cxq epp{1} 0 256 1).
+admit(*
 + conseq />.
   transitivity {1} { (sp_0,ep,bp,epp) <@ GetNoiseAVX2.samplenoise_enc(sp_0,ep,bp, epp,noiseseed);} (lnoiseseed{1} = noiseseed{2} /\ ={sp_0,ep,bp,epp} ==> ={sp_0,ep,epp}) 
    (
@@ -1832,7 +1845,7 @@ seq 12 20 : (#{/~bp{1}=bp{2}}pre  /\
   case (256 <= x && x < 512); 1: by smt().
   move => *; rewrite !initiE //= fun_if. 
   by smt().
-
+*).
 seq 1 1 : (#{/~sp_0{1}}{~sp_0{2}}pre /\ 
            lift_array768 sp_0{1} = nttunpackv (lift_array768 sp_0{2}) /\
            pos_bound768_cxq sp_0{1} 0 768 2 /\

diff --git a/proof/correctness/avx2/MLKEM_KEM_avx2.ec b/proof/correctness/avx2/MLKEM_KEM_avx2.ec
@@ -8,6 +8,7 @@ import GFq Rq Sampling Serialization Symmetric VecMat InnerPKE MLKEM Fq Correctn
 import MLKEM_Poly.
 import MLKEM_PolyVec.
 
+(*
 axiom pkH_sha_avx2 mem _ptr inp: 
     phoare [Jkem_avx2.M(Jkem_avx2.Syscall)._isha3_256 :
           arg = (inp,W64.of_int _ptr,W64.of_int (3*384+32)) /\
@@ -39,7 +40,38 @@ axiom sha_g_avx2 buf inp:
           let bytes = SHA3_512_64_64 (Array32.init (fun k => buf.[k])) 
                                      (Array32.init (fun k => buf.[k+32])) in
           res = Array64.init (fun k => if k < 32 then bytes.`1.[k] else bytes.`2.[k-32])] = 1%r.
+*)
+axiom sha3_256A_M1184_ph mem _ptr inp:
+ phoare [ Jkem_avx2.M(Jkem_avx2.Syscall)._sha3_256A_M1184
+        : arg = (inp,W64.of_int _ptr) /\
+          valid_ptr _ptr 1184 /\
+          Glob.mem = mem
+          ==> 
+          Glob.mem = mem /\
+          res = SHA3_256_1184_32
+            (Array1152.init (fun k =>  mem.[_ptr+k]),
+            (Array32.init (fun k => mem.[_ptr+1152+k])))] = 1%r.
 
+axiom sha3_512A_A64_ph buf inp: 
+ phoare [ Jkem_avx2.M(Jkem_avx2.Syscall)._sha3_512A_A64
+        : arg = (inp,buf)
+        ==> 
+        let bytes = SHA3_512_64_64 (Array32.init (fun k => buf.[k])) 
+                                   (Array32.init (fun k => buf.[k+32])) in
+        res = Array64.init (fun k => if k < 32 then bytes.`1.[k] else bytes.`2.[k-32])] = 1%r.
+
+axiom shake256_M32__M32_M1088_ph mem _pout _pin1 _pin2: 
+ phoare [ Jkem_avx2.M(Jkem_avx2.Syscall)._shake256_M32__M32_M1088
+        : arg = (W64.of_int _pout,W64.of_int _pin1,W64.of_int _pin2) /\
+          valid_ptr _pout 32 /\
+          valid_ptr _pin1 32 /\
+          valid_ptr _pin2 1088 /\
+          Glob.mem = mem
+          ==> 
+          touches Glob.mem mem _pout 32 /\
+          (Array32.init (fun k =>  Glob.mem.[_pout+k])) = 
+             SHAKE_256_1120_32 (Array32.init (fun k => mem.[_pin1+k])) 
+                            (Array960.init (fun k => mem.[_pin2+k]), Array128.init (fun k => mem.[_pin2+960+k])) ] = 1%r.
 
 lemma pack_inj : injective W8u8.pack8_t by apply (can_inj W8u8.pack8_t W8u8.unpack8 W8u8.pack8K).
 
@@ -59,12 +91,12 @@ lemma mlkem_kem_correct_kg mem _pkp _skp  :
          sk.`4 = load_array32 Glob.mem{1} (_skp + 1152 + 1152 + 32 + 32) /\
          t = load_array1152 Glob.mem{1} _pkp  /\
          rho = load_array32 Glob.mem{1} (_pkp+1152)].
+proof.
 proc => /=.
-
-swap {1} [3..5] 17.
-swap {1} 1 14.
-
-seq 19 4 : (
+swap {1} 1 16.
+swap {1} [2..4] 17.
+admit(*
+seq 13 2 : (
       z{2} = Array32.init(fun i => randomnessp{1}.[32 + i]) /\ 
       to_uint skp{1} = _skp +  1152 + 1152 + 32 + 32 /\
       valid_disj_reg _pkp (384*3+32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\
@@ -309,6 +341,7 @@ do split.
 move => memL iL skL; do split; 1: by smt().
 move => *; split; 1: by smt().
 by rewrite tP => i ib; smt(Array32.initiE).
+*).
 qed.
 
 
@@ -331,7 +364,7 @@ lemma mlkem_kem_correct_enc mem _ctp _pkp _kp :
      k = load_array32 Glob.mem{1} _kp
 ].
 proc => /=.
-seq 14 4 : (#[/1:-2]post 
+seq 13 4 : (#[/1:-2]post 
       /\ valid_disj_reg _ctp 1088 _kp 32 
       /\ to_uint s_shkp{1} = _kp 
       /\ (forall k, 0<=k<32 => kr{1}.[k]=_K{2}.[k])); last first.
@@ -365,16 +398,15 @@ seq 14 4 : (#[/1:-2]post
       case (k < 8 * i{hr}).
       + move => kbb;have := H9 k _; 1: by smt().
         by rewrite initiE 1:/# /= /#. 
-      rewrite !WArray64.WArray64.get64E. search pack8_t (\bits8).
+      rewrite !WArray64.WArray64.get64E.
       by rewrite !pack8bE // !initiE //= /init8 !WArray64.WArray64.initiE /#.
     by smt().
   auto => /> &1 &2 ?????????;split;  1: by smt().
   move => mm ii;do split => ???????; 1: smt().
   by rewrite /load_array32 tP => kk kkb; smt(Array32.initiE).
-
-wp;call (mlkem_correct_enc_0_avx2 mem _ctp _pkp).
-wp;ecall {1} (sha_g_avx2 buf{1} kr{1}).
-wp;ecall {1} (pkH_sha_avx2 mem (_pkp) ((Array32.init (fun (i : int) => buf{1}.[32 + i])))).
+wp; call (mlkem_correct_enc_0_avx2 mem _ctp _pkp).
+wp; ecall {1} (sha3_512A_A64_ph buf{1} kr{1}).
+wp; ecall {1} (sha3_256A_M1184_ph mem (_pkp) ((Array32.init (fun (i : int) => buf{1}.[32 + i])))).
 seq 8 0 : (#pre /\ s_pkp{1} = pkp{1} /\ s_ctp{1} = ctp{1} /\  s_shkp{1} = shkp{1} /\ randomnessp{1} = Array32.init (fun i => buf{1}.[i])).
 + sp ; conseq />.
   while {1} (0<=i{1}<=aux{1} /\ aux{1} = 4 /\ randomnessp{1} = coins{2} /\  (forall k, 0<=k<i{1}*8 => randomnessp{1}.[k] = buf{1}.[k])) (aux{1} - i{1}); last first.
@@ -390,8 +422,7 @@ seq 8 0 : (#pre /\ s_pkp{1} = pkp{1} /\ s_ctp{1} = ctp{1} /\  s_shkp{1} = shkp{1
      rewrite WArray32.WArray32.get64E pack8bE 1:/# !initiE 1:/# /= /init8.  
      by rewrite !WArray32.WArray32.initiE /#.
   by move => *; rewrite /get8; rewrite WArray64.WArray64.initiE /#.
-
-auto  => />  &1 &2; rewrite /load_array1152 /load_array32 /load_array128 /load_array960 /touches2 /touches !tP.
+auto  => /> &1 &2; rewrite /load_array1152 /load_array32 /load_array128 /load_array960 /touches2 /touches !tP.
 move => [#] ??????? pkv1 pkv2; do split.
 + by move => i ib; rewrite !initiE /= /#.
 + move => i ib; rewrite initiE /= 1:/# initiE /= 1:/# ifF 1:/#.
@@ -658,7 +689,7 @@ seq 7 1 : (#pre /\
            (forall k, 0<=k<32 => buf{1}.[k] = m{2}.[k]) /\
            (forall k, 0<=k<32 => kr{1}.[k] = _K{2}.[k]) /\
            (forall k, 0<=k<32 => kr{1}.[k+32] = r{2}.[k])).
-ecall {1} (sha_g_avx2 buf{1} kr{1}).
+ecall {1} (sha3_512A_A64_ph buf{1} kr{1}).
 wp; conseq (_: _ ==> 
    (forall k, 0<=k<32 => buf{1}.[k] = m{2}.[k]) /\
    (forall k, 32<=k<64 => buf{1}.[k] = mem.[_skp + 2336 + k - 32]) /\
@@ -670,7 +701,6 @@ wp; conseq (_: _ ==>
   + move => k kbl kbh; rewrite initiE 1:/# /= ifF 1:/# /= /G_mhpk; congr; congr;congr.
     rewrite tP => i ib; rewrite initiE //= /#.
     by rewrite tP => i ib; rewrite !initiE  /#. 
-
 while {1} (0<=i{1}<=4 /\ aux_0{1} = 4  /\ to_uint hp{1} = _skp + 2336 /\ Glob.mem{1} = mem /\
              valid_ptr _skp (384*3 + 384*3 + 32 + 32 + 32+ 32) /\
              (forall (k : int), 32 <= k && k < 32 + 8*i{1} => buf{1}.[k] = mem.[_skp + 2336 + k - 32]) /\
@@ -749,7 +779,7 @@ sp 3 0; seq 1 0 : (#pre /\
 
 ecall {1} (cmov_correct (to_uint shkp{1}) (Array32.init (fun (i_0 : int) => kr{1}.[0 + i_0])) cnd{1} Glob.mem{1}).
 
-wp;ecall{1} (j_shake_avx2  Glob.mem{1} (to_uint shkp{1}) (to_uint zp{1}) (to_uint ctp{1})).
+wp;ecall{1} (shake256_M32__M32_M1088_ph  Glob.mem{1} (to_uint shkp{1}) (to_uint zp{1}) (to_uint ctp{1})).
 
 + auto => /> &1 &2 ???????; rewrite /load_array1152 /load_array32 !tP => ?cphv????ceq cdif.
 do split;1,2: