Change proofs to work with most recent EC version.

MM45 · Aug 20, 2024 · 8422d56 · 8422d56
1 parent 42a2460
commit 8422d56
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 16 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -41,8 +41,10 @@ jobs:
     - name: Detect SMT provers
       run: |
         opam config exec -- easycrypt why3config -why3 ~/.why3.conf
-    - name: Compile Project
-      run: opam config exec -- easycrypt runtest -jobs 1 -report report.log -raw-args -gcstats config/tests.config xmss-acai
+    - name: Compile Project (acai)
+      run: opam config exec -- easycrypt runtest -jobs 1 -report report_acai.log -raw-args -gcstats config/tests.config xmss-acai
+    - name: Compile Project (fsai)
+      run: opam config exec -- easycrypt runtest -jobs 1 -report report_fsai.log -raw-args -gcstats config/tests.config xmss-fsai
     - uses: actions/upload-artifact@v4
       name: Upload report.log
       if: always()

diff --git a/config/tests.config b/config/tests.config
@@ -1,6 +1,3 @@
-[default]
-report = report.log
-
 [test-xmss-acai]
 okdirs  = !proofs/acai
 

diff --git a/proofs/acai/FL_XMSS_TW.ec b/proofs/acai/FL_XMSS_TW.ec
@@ -4742,7 +4742,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].
@@ -4763,7 +4763,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/acai/HashThenSign.eca b/proofs/acai/HashThenSign.eca
@@ -1323,8 +1323,8 @@ 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).
-  rewrite addrC; apply ler_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 ler_add. 
   + by rewrite EUFRMAROCCReproSample_Query EUFRMAROCCReproQuery_IEUFRMA.
   apply (ler_trans `| Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(false) @ &m : res] -
                       Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(true) @ &m : res] |).
@@ -1356,7 +1356,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] -
@@ -2035,8 +2035,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 
@@ -2066,8 +2065,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/acai/WOTS_TW.ec b/proofs/acai/WOTS_TW.ec
@@ -898,7 +898,7 @@ clone import FC.SMDTPREC as FC_PRE with
   Interpretation of arguments is, respectively, as follows:
   - Tweakable hash function to chain
   - Public seed
-  - Address (should be of chaining type (chtype))
+  - Address
   - Current position/index in chain
   - Number of times to chain the tweakable hash function
   - Input to apply the tweakable hash function on
@@ -5368,7 +5368,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 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)