Merge branch 'main' into feature-micromega

.github/workflows/ci.yml

@@ -8,8 +8,22 @@ env:
   OPAMJOBS: 2
 
 jobs:
+  pre_job:
+    name: Check for Duplicates Jobs
+    runs-on: ubuntu-20.04
+    outputs:
+      should_skip: ${{ steps.skip_check.outputs.should_skip }}
+    steps:
+    - uses: fkirc/skip-duplicate-actions@v5
+      id: skip_check
+      with:
+        concurrent_skipping: 'same_content_newer'
+        skip_after_successful_duplicate: 'false'
+
   compile-opam:
     name: EasyCrypt compilation (opam)
+    needs: pre_job
+    if: needs.pre_job.outputs.should_skip != 'true'
     runs-on: ubuntu-20.04
     container:
       image: ghcr.io/easycrypt/ec-build-box
@@ -25,6 +39,8 @@ jobs:
 
   compile-nix:
     name: EasyCrypt compilation (nix)
+    needs: pre_job
+    if: needs.pre_job.outputs.should_skip != 'true'
     env:
       HOME: /home/runner
     runs-on: ubuntu-20.04
@@ -45,14 +61,15 @@ jobs:
 
   check:
     name: Check EasyCrypt Libraries
-    needs: compile-opam
+    needs: [pre_job, compile-opam]
+    if: needs.pre_job.outputs.should_skip != 'true'
     runs-on: ubuntu-20.04
     container:
       image: ghcr.io/easycrypt/ec-build-box
     strategy:
       fail-fast: false
       matrix:
-        target: [stdlib, examples]
+        target: [unit, stdlib, examples]
     steps:
     - uses: actions/checkout@v3
     - name: Update OPAM & EasyCrypt dependencies
@@ -80,7 +97,8 @@ jobs:
 
   external:
     name: Check EasyCrypt External Projects
-    needs: compile-opam
+    needs: [pre_job, compile-opam]
+    if: needs.pre_job.outputs.should_skip != 'true'
     runs-on: ubuntu-20.04
     container:
       image: ghcr.io/easycrypt/ec-build-box

Makefile

@@ -6,7 +6,7 @@ ECARGS    ?=
 ECTOUT    ?= 10
 ECJOBS    ?= 0
 ECEXTRA   ?= --report=report.log
-ECPROVERS ?= [email protected] Z3@4.8 CVC4@1.8
+ECPROVERS ?= [email protected] Z3@4.12 CVC5@1.0
 CHECKPY   ?=
 CHECK     := $(CHECKPY) scripts/testing/runtest
 CHECK     += --bin=./ec.native --bin-args="$(ECARGS)"
@@ -27,7 +27,7 @@ default: build
 
 build:
 	rm -f src/ec.exe ec.native
-	dune build -p easycrypt
+	dune build
 	ln -sf src/ec.exe ec.native
 ifeq ($(UNAME_P)-$(UNAME_S),arm-Darwin)
 	-codesign -f -s - src/ec.exe
@@ -39,15 +39,16 @@ install: build
 uninstall:
 	$(DUNE) uninstall
 
-check: stdlib examples
+unit: build
+	$(CHECK) unit
 
 stdlib: build
 	$(CHECK) prelude stdlib
 
 examples: build
 	$(CHECK) examples mee-cbc
 
-check: stdlib examples
+check: unit stdlib examples
 	@true
 
 clean:

config/tests.config

@@ -12,3 +12,6 @@ exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomple
 
 [test-mee-cbc]
 okdirs = examples/MEE-CBC
+
+[test-unit]
+okdirs = tests

default.nix

@@ -10,16 +10,6 @@ let provers =
     z3
   ] else []; in
 
-let why3-pin =
-  why3.overrideAttrs (o : rec {
-    version = "1.6.0";
-    src = fetchurl {
-      url = "https://why3.gitlabpages.inria.fr/releases/${o.pname}-${version}.tar.gz";
-      sha256 = "sha256-hFvM6kHScaCtcHCc6Vezl9CR7BFbiKPoTEh7kj0ZJxw=";
-    };
-  });
-in
-
 stdenv.mkDerivation {
   pname = "easycrypt";
   version = "git";
@@ -37,12 +27,11 @@ stdenv.mkDerivation {
     menhir
     menhirLib
     yojson
+    why3
     zarith
   ]);
 
-  propagatedBuildInputs = [ why3-pin ]
-    ++ devDeps
-    ++ provers;
+  propagatedBuildInputs = devDeps ++ provers;
 
   installPhase = ''
     runHook preInstall

examples/ChaChaPoly/chacha_poly.ec

@@ -1130,8 +1130,7 @@ section PROOFS.
       + by proc; inline *; auto => /> &2; case: (p{2}).
       + by proc; auto.
       by auto; conseq (_: ={RO.m}) => //; sim.
-    transitivity*{1} { r <@ G3(GenChaChaPoly(OCC(IFinRO))).main(); } => //;1:smt().
-    + by symmetry; call (CCP_OCCP IFinRO G3).
+    rewrite equiv[{1} 1 -(CCP_OCCP IFinRO G3)].
     inline *; sim (_: ={Mem.lc, Mem.log, Mem.k} /\ OCC.gs{1} = RO.m{2}).
     proc; inline *;auto.
   qed.

examples/Dice4_6.ec

@@ -69,12 +69,11 @@ transitivity D4.sample (true ==> res{1} = finv res{2})
     by apply: dinter_uni; rewrite supp_dinter /#.
   by rewrite !supp_dinter /#.
 proc *.
-rewrite equiv [{1} D4_Sample () r () r].
-rewrite equiv [{1} D4_6.sampleE_sampleWi () r ((), 5) r].
-+ by auto=> />; exact: dinter_ll.
-rewrite equiv [{2} D6_Sample () r ((), 5) r]; sim.
+rewrite equiv[{1} 1 D4_Sample].
+rewrite equiv[{1} 1 D4_6.sampleE_sampleWi ((), 5 :@ r)].
++ by auto; rewrite dinter_ll.
+rewrite equiv[{1} 1 -D6_Sample ( :@ r)]; sim.
 qed.
-
 lemma prD6 : forall k &m, Pr[D6.sample() @ &m : res = k] =
       if 1 <= k <= 4 then 1%r/4%r else 0%r.
 proof.

examples/MEE-CBC/CBC.eca

@@ -187,9 +187,9 @@ section Random_Ideal.
   equiv Random_Ideal: Random.enc ~ Ideal.enc: size p{1} = size p{2} ==> ={res}.
   proof.
   proc.
-  rewrite equiv [{2} Sampling.Sample_LoopSnoc_eq (size p + 1)  r (size p + 1) c].
-  + auto=> /#.
-  by wp; while (i0{1} = i{2} /\ c{2} = l{1} /\ size p{2} + 1 = n{1}); auto=> /#.
+  outline {2} [1] { r <@ Sampling.Sample.sample(size p + 1); }.
+  rewrite equiv[{2} 1 Sampling.Sample_LoopSnoc_eq].
+  by inline; wp; while (={i} /\ c{1} = l{2} /\ size p{1} + 1 = n{2}); auto=> /#.
   qed.
 end section Random_Ideal.
 

examples/UC/RndO.ec

@@ -84,6 +84,7 @@ abstract theory Ideal.
 type from, to.
 
 op sampleto : from -> to distr.
+axiom sampleto_ll : forall x, Distr.weight (sampleto x) = 1%r.
 
 module type RO = {
   proc init  ()                  : unit
@@ -233,8 +234,6 @@ proof. by proc; auto. qed.
 lemma FRO_set_ll : islossless FRO.set.
 proof. by proc; auto. qed.
 
-axiom sampleto_ll : forall x, Distr.weight (sampleto x) = 1%r.
-
 lemma RO_get_ll : islossless RO.get.
 proof. by proc; auto; progress; apply sampleto_ll. qed.
 

examples/WF-examp.ec

@@ -0,0 +1,66 @@
+(* example use of well-founded recursion and induction
+   (theories/structures/WF.ec) *)
+
+require import AllCore List IntDiv StdOrder.
+import IntOrder.
+
+require import WF.
+
+(* define well-founded relation on lists: lt_list_size xs ys <=>
+   size xs < size ys *)
+
+op lt_list_size : 'a list rel = wf_pre size lt_nat.
+
+lemma wf_lt_list_size ['a] : wf lt_list_size<:'a>.
+proof.
+rewrite wf_pre wf_lt_nat.
+qed.
+
+lemma lt_list_sizeP (xs ys : 'a list) :
+  lt_list_size xs ys <=> size xs < size ys.
+proof.
+by rewrite /lt_list_size /wf_pre /lt_nat size_ge0.
+qed.
+
+(* body of well-founded recursive definition that "chunkifies" an 'a
+   list into an 'a list list: the first n elements, then the next n
+   elements, etc., where if at the end there are < n elements left,
+   they are discarded *)
+
+op chunkify_wf_rec_def (n : int) : ('a list, 'a list list) wf_rec_def =
+  fun (xs : 'a list,                     (* input list *)
+       f : 'a list -> 'a list list) =>   (* for recursive calls on
+                                            strictly shorter lists *)
+  if n <= size xs
+  then take n xs :: f (drop n xs)
+  else [].
+
+(* the actual recursive definition: *)
+
+op chunkify (n : int) : 'a list -> 'a list list =
+  wf_recur
+  lt_list_size              (* well-founded relation being used *)
+  []                        (* element to be returned if recursive calls
+                               don't respect well-founded relation *)
+  (chunkify_wf_rec_def n).  (* body of recursive definition *)
+
+lemma chunkify_size (n : int, xs : 'a list) :
+  1 <= n => size (chunkify n xs) = size xs %/ n.
+proof.
+move => ge1_n; move : xs.
+apply (wf_ind lt_list_size).  (* use well-founded induction on lt_list_size *)
+apply wf_lt_list_size.
+rewrite /chunkify => /= xs IH.
+rewrite wf_recur 1:wf_lt_list_size.
+rewrite {1}/chunkify_wf_rec_def.  (* only need to rewrite at top-level *)
+case (n <= size xs) => [le_n_size_xs | not_le_n_size_xs].
+(* first case *)
+rewrite lt_list_sizeP.
+have lt_size_drop : size (drop n xs) < size xs by rewrite size_drop /#.
+rewrite lt_size_drop /= IH 1:lt_list_sizeP //.
+rewrite size_drop 1:/# ler_maxr 1:/#.
+have {2}-> : size xs = n + (size xs - n) by smt().
+rewrite (divzDl n) 1:dvdzz divzz /#.
+(* second case *)
+smt(size_ge0 ltr_normr).
+qed.