Update files in proofs/security to verify with newest EC and provers

easycrypt.project

@@ -1,14 +1,14 @@
 [general]
 timeout = 30
 
-provers = [email protected]
-provers = CVC4@1.8
-provers = Z3@4.8
+provers = [email protected].2
+provers = CVC5@1.2.0
+provers = Z3@4.13.3
 
 rdirs = proof
 rdirs = Jasmin:jasmin/eclib
 idirs = code/jasmin/mlkem_ref/extraction
 idirs = code/jasmin/mlkem_avx2/extraction
 idirs = crypto-specs/common
 rdirs = crypto-specs/fips202
-rdirs = crypto-specs/ml-kem
+rdirs = crypto-specs/ml-kem

proof/security/FO_MLKEM.ec

@@ -1,4 +1,4 @@
-require import AllCore Distr List Real SmtMap FSet DInterval FinType KEM_ROM.
+require import AllCore Distr List Real FMap FSet DInterval FinType KEM_ROM.
 require (****) PKE_ROM PlugAndPray Hybrid FelTactic. 
 
 require FO_UU.
@@ -238,7 +238,7 @@ seq 6 5 : (#pre /\ m0{1} = m{2} /\ pk1{1} = pk0{2} /\
         dkey `*` randd; last by smt().
     rewrite dprod_dlet; congr;apply fun_ext => r.
     by rewrite dlet_dunit.
-  by auto => />;smt(get_setE mem_set mem_empty @SmtMap @FSet).
+  by auto => />;smt(get_setE mem_set mem_empty @FMap @FSet).
 
 seq 1 1 : (#pre /\ c1{1} = c0{2}); 1: by auto => /#.
 
@@ -395,7 +395,8 @@ have -> : Pr[KEMROMx2.RO2.MainD(DKK2(A),RO2.RO).distinguish() @ &m : res] =
           ={res} /\
           (CCA.sk{1}, CCA.cstar{1}, RO1.RO.m{1}, (glob A){1}) =
           (CCA.sk{2}, CCA.cstar{2}, RO1.RO.m{2}, (glob A){2})) => //.
-  apply(RO2.FullEager.RO_LRO (DKK2(A)) _).
+  conseq (: ={glob DKK2(A), arg} ==> ={res, glob DKK2(A)}) => //. 
+  apply (RO2.FullEager.RO_LRO (DKK2(A)) _).
   by move => *;rewrite dkey_ll.
 
 have <- : Pr[KEMROMx2.RO1.MainD(DKK1(A),RO1.RO).distinguish() @ &m : res] =
@@ -405,7 +406,8 @@ have <- : Pr[KEMROMx2.RO1.MainD(DKK1(A),RO1.RO).distinguish() @ &m : res] =
           ={res} /\
           (CCA.sk{1}, CCA.cstar{1}, RO2.RO.m{1}, (glob A){1}) =
           (CCA.sk{2}, CCA.cstar{2}, RO2.RO.m{2}, (glob A){2})) => //.
-  apply(RO1.FullEager.RO_LRO (DKK1(A)) _).
+  conseq (: ={glob DKK1(A), arg} ==> ={res, glob DKK1(A)}) => //. 
+  apply (RO1.FullEager.RO_LRO (DKK1(A)) _).
   by move => *;rewrite randd_ll.
 
 byequiv => //;proc;inline {1} 2; inline {2} 2. 
@@ -456,7 +458,8 @@ call(: ={glob CCA} /\ B1x2._pk{1} = CCA.sk{2}.`1.`1 /\
   case (m'{1} = None).
   + rcondf{1} 8; 1: by auto.
     rcondt{1} 8; 1: by auto.
-    by auto => />;smt(get_setE). 
+    auto => />.
+    by do ? (move=> *; split); smt(get_setE).
   rcondt{1} 8; 1: by auto.
   inline *.
   rcondf{1} 10; 1: by auto;smt(mem_set).
@@ -480,7 +483,7 @@ call(: ={glob CCA} /\ B1x2._pk{1} = CCA.sk{2}.`1.`1 /\
     by auto => />;smt(get_setE).  
 
     rcondf{1} 2;1: by move => *;inline *;auto => />.
-    by inline *;auto => /> *; do split;move => *;do split;move => *;1:do split;smt(@SmtMap).
+    by inline *;auto => /> *; do split;move => *;do split;move => *;1:do split;smt(@FMap).
 
 inline *. 
 swap {1} 14 -13. swap {1} 20 -18. swap {2} 11 -10.

proof/security/FO_TT.ec

@@ -1,4 +1,4 @@
-require import AllCore Distr List Real SmtMap FSet DInterval FinType.
+require import AllCore Distr List Real FMap FSet DInterval FinType.
 require (****) PKE_ROM PlugAndPray Hybrid FelTactic. 
 
 (******************************************************************)
@@ -664,13 +664,12 @@ lemma corr_pnp &m :
     (qHC+1)%r * Pr[PKE.Correctness_Adv(BasePKE, B(A,RO.RO)).main() @ &m : res]. 
   move => qHC_small A_count A_ll.
   rewrite RField.mulrC -StdOrder.RealOrder.ler_pdivr_mulr; 1: smt (ge0_qHC).
-(* print glob Correctness_Adv1(RO.RO,A). *)
   pose phi := fun (g: (glob Correctness_Adv1(RO.RO,A))) (_:unit) => 
       has (fun m =>
-        Some m <> dec g.`1 (enc (oget g.`7.[m]) g.`2 m)) g.`6.
+        Some m <> dec g.`7 (enc (oget g.`8.[m]) g.`5 m)) g.`6. 
   pose psi := fun (g: (glob Correctness_Adv1(RO.RO,A))) (_:unit) => 
     let i = find 
-      (fun m => Some m <> dec g.`1 (enc (oget g.`7.[m]) g.`2 m)) g.`6
+      (fun m => Some m <> dec g.`7 (enc (oget g.`8.[m]) g.`5 m)) g.`6
     in if 0 <= i < qHC + 1 then i else 0.
   have := PAPC.PBound (Correctness_Adv1(RO.RO,A)) phi psi tt &m _.
   + smt (ge0_qHC mem_iota).
@@ -1814,10 +1813,9 @@ proof.
 
   move => qHPn0.
   rewrite RField.mulrC -StdOrder.RealOrder.ler_pdivr_mulr; 1: smt (ge0_qH ge0_qP).
-(* print glob G3. *)
-  pose phi := fun (g:glob G3) (b:bool) => dec g.`7.`2 g.`8 = Some g.`2 /\ g.`2 \in g.`9.
+  pose phi := fun (g:glob G3) (b:bool) => dec g.`9.`2 g.`8 = Some g.`5 /\ g.`5 \in g.`10.
   pose psi := fun (g:glob G3) (_:bool) => 
-    let i = find (pred1 g.`2) (elems (fdom g.`9)) in
+    let i = find (pred1 g.`5) (elems (fdom g.`10)) in
     if 0 <= i < qH + qP then i else 0.
   have := PAP1.PBound G3 phi psi tt &m _. 
   + smt (ge0_qH ge0_qP mem_iota).

proof/security/FO_UU.ec

@@ -1,4 +1,4 @@
-require import AllCore Distr List Real SmtMap FSet DInterval FinType KEM_ROM.
+require import AllCore Distr List Real FMap FSet DInterval FinType KEM_ROM.
 require (****) PKE_ROM PlugAndPray Hybrid FelTactic. 
 
 (* This will be the underlying scheme resulting 
@@ -963,7 +963,7 @@ seq 32 19 : (={glob A,k1,pk,b,cm,CCA.sk,CCA.cstar, H2.invert, H2.mtgt, H1.bad, H
   (forall m, m <> H2.mtgt{2} => RO2.RO.m{1}.[m] = RO2.RO.m{2}.[m]) /\
   (!H1.bad{2} <=> 
              Some H2.mtgt{2} = dec  CCA.sk{2}.`1.`2 (oget CCA.cstar{2})));
-    1: by auto => />; smt(mem_empty get_setE fdom_set @SmtMap @FSet @List).
+    1: by auto => />; smt(mem_empty get_setE fdom_set @FMap @FSet @List).
 
 case (H1.bad{1}).
 rnd;wp;call(:H1.bad,false,CCA.cstar{2} <> None /\ 
@@ -1180,9 +1180,9 @@ proc.
     + by islossless.
   + case (H1.bad). 
     + conseq(:nobias); 1: smt().
-      by rnd;rnd;auto => /> *;rewrite DBool.dbool_ll /=;smt(DBool.dbool1E).
+      rnd;rnd;auto => /> *;rewrite DBool.dbool_ll /=; smt(DBool.dboolE).
     conseq(: b' = b); 1:smt(). 
-    by rnd;rnd;auto => /> *;rewrite DBool.dbool_ll /=;smt(DBool.dbool1E).
+    by rnd;rnd;auto => /> *;rewrite DBool.dbool_ll /=;smt(DBool.dboolE).
   + by hoare; trivial.
 by done.
 qed.

proof/security/MLWE.ec

@@ -1,4 +1,4 @@
-require import AllCore Ring SmtMap Distr PROM.
+require import AllCore Ring FMap Distr PROM.
 require (****) Matrix.
 
 clone import Matrix as Matrix_.
@@ -261,7 +261,7 @@ swap {1} 5 -2.
 seq 3 6 : (#pre /\ ={b,_A,sd} /\ (RO.m{1}.[B._sd{2}] = Some B.__A{2}) /\ 
           B.__A{2} = _A{2} /\ B._sd{2} = sd{2} /\ 
           (forall x, x <> B._sd{2} => RO.m{1}.[x] = RO.m{2}.[x]));
- first by inline *; auto => />; smt(@SmtMap).
+ first by inline *; auto => />; smt(@FMap).
 wp;call(: (RO.m{1}.[B._sd{2}] = Some B.__A{2}) /\ 
             forall x, x <> B._sd{2} => RO.m{1}.[x] = RO.m{2}.[x]).
 proc;inline *.
@@ -290,7 +290,7 @@ seq 3 6 : (#pre /\ ={b,sd} /\ _A{1} = m_transpose _A{2} /\
            Bt.__A{2} = m_transpose _A{2} /\ Bt._sd{2} = sd{2} /\ 
            (forall x, x <> Bt._sd{2} => RO.m{1}.[x] = RO.m{2}.[x])).
 + inline *; wp; rnd (fun m => m_transpose m) (fun m => m_transpose m).
-  by auto => />;   smt(@SmtMap trmxK duni_matrix_funi). 
+  by auto => />;   smt(@FMap trmxK duni_matrix_funi). 
 wp;call(: (RO.m{1}.[Bt._sd{2}] = Some Bt.__A{2}) /\ 
             forall x, x <> Bt._sd{2} => RO.m{1}.[x] = RO.m{2}.[x]).
 proc;inline *.
@@ -658,7 +658,7 @@ seq 4 0 : (#pre /\ (_A = oget RO.m.[sd]){1}); 1:
 seq 1 1 : #pre; last by auto => /> &1 ?; rewrite /dout duni_matrix_ll.
 exists* _A{1}, sd{1}; elim * => _A1 sd1.
 call(: ={RO.m} /\ sd1 \in RO.m{1} /\ _A1 = oget RO.m{1}.[sd1]).
-+ proc; auto => /> &2 rl ??; 1:smt(@SmtMap).
++ proc; auto => /> &2 rl ??; 1:smt(@FMap).
 by auto => />.
 qed.
 
@@ -694,7 +694,7 @@ seq 4 0 : (#pre /\ (_A = oget RO.m.[sd]){1}); 1:
 seq 1 1 : #pre; last by auto => /> &1 ?; rewrite /dout duni_matrix_ll.
 exists* _A{1}, sd{1}; elim * => _A1 sd1.
 call(: ={RO.m} /\ sd1 \in RO.m{1} /\ _A1 = oget RO.m{1}.[sd1]).
-+ proc; auto => /> &2 rl ??; 1:smt(@SmtMap).
++ proc; auto => /> &2 rl ??; 1:smt(@FMap).
 by auto => />.
 qed.
 
@@ -1060,7 +1060,7 @@ seq 2 2 : #pre; last by auto => /> &1 ?; rewrite /dout duni_matrix_ll.
 exists* _A{1}, sd{1}; elim * => _A1 sd1.
 call(: ={RO.m, glob Sim} /\ sd1 \in RO.m{1} /\ _A1 = oget RO.m{1}.[sd1]); last by call(_:true); auto => />.
 proc*;call(: ={RO.m} /\ sd1 \in RO.m{1} /\ _A1 = oget RO.m{1}.[sd1]); last by auto => />.
-by proc; inline *; auto => />; smt(@SmtMap).
+by proc; inline *; auto => />; smt(@FMap).
 qed.
 
 lemma MLWE_SMP_equiv_t _b &m  (S <: Sampler {-LRO, -RO, -FRO, -RO_SMP.LRO, -D}) 
@@ -1122,7 +1122,7 @@ seq 2 2 : #pre; last by auto => /> &1 ?; rewrite /dout duni_matrix_ll.
 exists* _A{1}, sd{1}; elim * => _A1 sd1.
 call(: ={RO.m, glob Sim} /\ sd1 \in RO.m{1} /\ _A1 = oget RO.m{1}.[sd1]); last by call(_: true);auto => />.
 proc*;call(: ={RO.m} /\ sd1 \in RO.m{1} /\ _A1 = oget RO.m{1}.[sd1]); last by auto => />.
-by proc; inline *; auto => />; smt(@SmtMap).
+by proc; inline *; auto => />; smt(@FMap).
 qed.
 
 end SMP_vs_ROM_IND.

proof/security/MLWE_PKE.ec

@@ -1,4 +1,4 @@
-require import AllCore Distr List SmtMap Dexcepted PKE_ROM.
+require import AllCore Distr List FMap Dexcepted PKE_ROM.
 require (****) RndExcept StdOrder MLWE.
 
 theory MLWE_PKE.
@@ -606,7 +606,8 @@ seq 14 9 : ((tr{1}, b{1}) = witness /\
     by auto => />; smt(get_setE sk_encodeK pk_encodeK).
   by auto => />; smt(sk_encodeK get_setE pk_encodeK).
 
-inline *; auto => />;1:by smt(sk_encodeK get_setE pk_encodeK).
+inline *; auto => />.
++ by do ? (move => *; split); smt(sk_encodeK get_setE pk_encodeK). 
 by call(_: true); auto => />; smt(get_set_eqE).
 qed.
 
@@ -717,7 +718,8 @@ rcondt{1}6; 1: by move => *; auto;call(_: true); auto => />;smt(mem_empty).
 rcondt{2}6; 1: by move => *; auto;call(_: true); auto => />;smt(mem_empty).
 wp;call(_: ={glob RO_H.RO, glob Sim});1: by sim.
 conseq />;1:by smt(). 
-auto => />; 1: by smt(parts_work noise_commutes noise_preserved).
+auto => />. 
++ by do ? (move => *; split); smt(parts_work noise_commutes noise_preserved).
 by call(_: true); auto => />;  smt(parts_work noise_commutes noise_preserved).
 qed.
 
@@ -873,7 +875,7 @@ byequiv => //; proc; inline *.
 wp;call(_: ={glob RO_H.RO, glob Sim}); 1: by sim.
 rcondt{1}6; 1: by move => *; auto => />;call(_: true); auto => />;smt(mem_empty). 
 rcondt{2}6; 1: by move => *; auto => />;call(_: true); auto => />;smt(mem_empty). 
-auto => />;1: by smt(). 
+auto => /> *; 1: smt().
 by call(_: true); auto => />;smt(get_set_sameE).
 qed.
 

proof/security/MLWE_PKE_Basic.ec

@@ -1,4 +1,4 @@
-require import AllCore Distr List SmtMap Dexcepted PKE_ROM.
+require import AllCore Distr List FMap Dexcepted PKE_ROM.
 require (****) RndExcept StdOrder MLWE.
 
 theory MLWE_PKE_Basic.

proof/security/MLWE_PKE_Hash.ec

@@ -1,4 +1,4 @@
-require import AllCore Distr List SmtMap Dexcepted PKE_ROM StdOrder.
+require import AllCore Distr List FMap Dexcepted PKE_ROM StdOrder.
 require (**RndExcept **) MLWE FLPRG.
 
 theory MLWE_PKE_Hash.