Also adjust fsai proofs to work with recent EC veresion.

MM45 · Aug 20, 2024 · 705bd0f · 705bd0f
1 parent 8422d56
commit 705bd0f
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 9 deletions.
diff --git a/proofs/fsai/FL_XMSS_TW.ec b/proofs/fsai/FL_XMSS_TW.ec
@@ -4109,7 +4109,7 @@ have nthxval:
     split=> [| _].
     * rewrite {2}(: i = i - 1 + 1) // (take_nth witness) 1:/# flatten_rcons size_cat.
       by rewrite ltz_add2l /#.
-    rewrite -{2}(cat_take_drop i) flatten_cat size_cat.
+    rewrite -{2}(cat_take_drop i R_SMDTTCRCTRH_EUFRMAFLXMSSTWESNOPRF.inpll{2}) flatten_cat size_cat.
     by rewrite lez_addl size_ge0.
   rewrite xval equnz2ts_flinpl nth_flatten 1,2:/#.
   case (i = 1) => [eq1_i | neq1_i].
@@ -4130,7 +4130,7 @@ have -> //=:
     split=> [| _].
     * rewrite {2}(: i = i - 1 + 1) // (take_nth witness) 1:/# flatten_rcons size_cat.
       by rewrite ltz_add2l /#.
-    rewrite -{2}(cat_take_drop i) flatten_cat size_cat.
+    rewrite -{2}(cat_take_drop i R_SMDTTCRCTRH_EUFRMAFLXMSSTWESNOPRF.adrsll{2}) flatten_cat size_cat.
     by rewrite lez_addl size_ge0.
   do 4! congr. 
   apply (eq_from_nth witness); first by rewrite 2!size_map ?size_take /#. 

diff --git a/proofs/fsai/HashThenSign.eca b/proofs/fsai/HashThenSign.eca
@@ -1355,7 +1355,7 @@ theory WithSampling.
   apply (ler_trans (`|  Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll]
                       - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] |
                     + Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll])).
-  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0] 2:&(ler_norm_add).
+  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0]; smt(ler_norm_add).
   rewrite addrC; apply ler_add.
   + by rewrite EUFRMAROCCReproSample_Query EUFRMAROCCReproQuery_IEUFRMA.
   apply (ler_trans `| Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(false) @ &m : res] -
@@ -1388,7 +1388,7 @@ theory WithSampling.
   apply (ler_trans (`|  Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll]
                       - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] |
                     + Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll])).
-  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0] 2:&(ler_norm_add).
+  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0]; smt(ler_norm_add).
   rewrite addrC; apply ler_add.
   + by rewrite EUFRMAROCCReproSample_Query EUFRMAROCCReproQuery_IEUFRMA.
   apply (ler_trans `| Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(false) @ &m : res] -
@@ -2067,8 +2067,7 @@ theory WithPRF.
   rewrite opprB (addrC Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]) addrA.
   apply (ler_trans (`| Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - 
                        Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] | +
-                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)).
-  + by apply ler_norm_add.
+                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)); 1: smt(ler_norm_add).
   rewrite -3!addrA &(ler_add) 1:ALKUDSS_EUFCMARO_PRF //.
   rewrite ger0_norm 1:Pr[mu_ge0] //.
   move: (ALKUDSS_EUFCMARO_CRRO_EUFRMA FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll A 
@@ -2098,8 +2097,7 @@ theory WithPRF.
   rewrite opprB (addrC Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]) addrA.
   apply (ler_trans (`| Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - 
                        Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] | +
-                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)).
-  + by apply ler_norm_add.
+                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)); 1: smt(ler_norm_add).
   rewrite -3!addrA &(ler_add) 1:ALKUDSS_EUFCMARO_PRF //.
   rewrite ger0_norm 1:Pr[mu_ge0] //.
   move: (ALKUDSS_EUFCMARO_METCRRO_EUFRMA FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll A 

diff --git a/proofs/fsai/WOTS_TW.ec b/proofs/fsai/WOTS_TW.ec
@@ -5616,7 +5616,7 @@ have indtelesum:
     BRA.bigi predT (fun (x : int) => Pr[DistRCHil.main(x) @ &m : res] - Pr[DistRCHil.main(x + 1) @ &m : res]) 0 i.
 + elim => [/= | i ge0_i ih]; first by rewrite range_geq.
   rewrite -addr0 (: 0%r = (- Pr[DistRCHil.main(i) @ &m : res] + Pr[DistRCHil.main(i) @ &m : res])) 1:/#.
-  by rewrite addrA ih BRA.big_int_recr //= addrA.
+  by rewrite addrA BRA.big_int_recr /#.
 rewrite (indtelesum (w - 2)); first by smt(val_w).
 have ->:
   BRA.bigi predT (fun (i : int) => Pr[DistRCHil.main(i) @ &m : res] - Pr[DistRCHil.main(i + 1) @ &m : res]) 0 (w - 2)