Merge pull request #37 from 4ever2/update-deps

Support Coq 8.16 and 8.17

.github/workflows/build.yml

@@ -35,7 +35,7 @@ jobs:
       - name: Install OCaml
         uses: avsm/setup-ocaml@v1
         with:
-          ocaml-version: 4.07.1
+          ocaml-version: 4.09.1
 
       # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
       - name: Checkout repo
@@ -45,6 +45,6 @@ jobs:
       - name: Build
         run: |
           opam repo add coq-released https://coq.inria.fr/opam/released
-          opam install coq.8.14.0 coq-equations.1.3+8.14 coq-mathcomp-ssreflect.1.13.0 coq-mathcomp-analysis.0.3.13 coq-extructures.0.3.1 coq-deriving.0.1.0
+          opam install coq.8.16.0 coq-equations.1.3+8.16 coq-mathcomp-ssreflect.1.15.0 coq-mathcomp-analysis.0.5.3 coq-extructures.0.3.1 coq-deriving.0.1.0
           opam exec -- make -j4
 

DOC.md

@@ -421,7 +421,7 @@ Proof.
   (* Now deal with the goals *)
 ```
 
-Finally the identity package is defined as `ID I` where `I` is an interface.
+Finally, the identity package is defined as `ID I` where `I` is an interface.
 It both imports and exports `I` by simply forwarding the calls.
 It is valid as long as `I` does not include two signatures sharing the same
 identifier, as overloading is not possible in our packages. This property is
@@ -790,7 +790,7 @@ then applying `ssprove_swap_lhs 0%N` will leave us to prove
 ```
 instead.
 
-Not any two commands are swappable however. The tactic will try to infer the
+However, not any two commands are swappable. The tactic will try to infer the
 swappability condition automatically, this is the case for sampling which can
 always be swapped (if dependencies permit), or for `get`/`put` when they talk
 about distinct locations. If automation proves insufficient, the user will have
@@ -900,7 +900,7 @@ and turn it into
 #### Remember after reading
 
 Sometimes, swapping and contracting is not possible, even when the code makes
-two reads to the same location. It can happen for instance if the the value read
+two reads to the same location. It can happen for instance if the value read
 is branched upon before being read again.
 
 For this we have several rules that will *remember* which location was read.
@@ -978,7 +978,7 @@ Dually to how we *remember* read values, we propose a way to write to a memory
 location, even when it might temporarily break the invariant. As we will se in
 [[Crafting invariants]], a lot of invariants will involve several locations at
 once, meaning the most of the time, writing a value will break them.
-Thus our machinery to write to the memory freely and then, at the user's
+Thus, our machinery to write to the memory freely and then, at the user's
 command, to restore the invariant.
 
 These debts to the precondition are incurred by using one of the following
@@ -1060,7 +1060,7 @@ where `L₀` and `L₁` represent the sets of memory locations of both programs.
 While it can be enough for a lot of examples (our own examples mostly use
 equality as an invariant), it is not always sufficient.
 
-Another invariant the we propose is called `heap_ignore` and is defined as
+Another invariant we propose is called `heap_ignore` and is defined as
 ```coq
 Definition heap_ignore (L : {fset Location}) :=
   λ '(h₀, h₁),

README.md

@@ -31,11 +31,11 @@ A documentation is available in [DOC.md].
 
 #### Prerequisites
 
-- OCaml `>=4.05.0 & <4.13.0`
-- Coq `8.14.0`
-- Equations `1.3+8.14`
-- Mathcomp `1.13.0`
-- Mathcomp analysis `0.3.13`
+- OCaml `>=4.05.0 & <5`
+- Coq `>=8.16.0 & <8.18.0`
+- Equations `1.3`
+- Mathcomp `>=1.15.0`
+- Mathcomp analysis `>=0.5.3`
 - Coq Extructures `0.3.1`
 - Coq Deriving `0.1`
 
@@ -199,7 +199,7 @@ more. Packages created through our operations always verify this property
 
 #### Interchange between sequential and parallel composition
 
-Finally we prove a law involving sequential and parallel composition
+Finally, we prove a law involving sequential and parallel composition
 stating how we can interchange them:
 ```coq
 Lemma interchange :
@@ -335,7 +335,7 @@ Theorem commitment_binding :
     ɛ_soundness A Adv.
 ```
 
-Combining the above theorems with the instatiation of Schnorr's protocol we get a commitment scheme given by:
+Combining the above theorems with the instantiation of Schnorr's protocol we get a commitment scheme given by:
 
 ```coq
 Theorem schnorr_com_hiding :
@@ -392,7 +392,7 @@ We separate by a slash (/) rule names that differ in the CSF (left) and journal
 | async-put-lhs     | `r_put_lhs`           |
 | restore-pre-lhs   | `r_restore_lhs`       |
 
-Finally the "bwhile" / "do-while" rule is proven as
+Finally, the "bwhile" / "do-while" rule is proven as
 `bounded_do_while_rule` in [rules/RulesStateProb.v].
 
 ### More Lemmas and Theorems for packages
@@ -493,7 +493,7 @@ This relational effect observation is called
 file [rhl_semantics/only_prob/ThetaDex.v] as a composition:
 FreeProb² ---`unary_theta_dens²`---> SDistr² ---`θ_morph`---> Wrelprop
 
-The first part `unary_theta_dens²` consists in intepreting pairs
+The first part `unary_theta_dens²` consists in interpreting pairs
 of probabilistic programs into pairs of actual subdistributions.
 This unary semantics for probabilistic programs `unary_theta_dens`
 is defined in [rhl_semantics/only_prob/Theta_dens.v].
@@ -516,7 +516,7 @@ It is defined in the file [rhl_semantics/only_prob/Theta_exCP.v].
 up to inequalities.
 The definition of `θ_morph` relies on the notion of couplings,
 defined in this file [rhl_semantics/only_prob/Couplings.v].
-The prove that it constitutes a lax morphism depends on lemmas
+The proof that it constitutes a lax morphism depends on lemmas
 for couplings that can be found in the same file.
 
 
@@ -589,8 +589,8 @@ a lax morphism Kl(θ) between those Kleisli adjunctions.
 Kl(θ) is a lax morphism between left relative adjunctions,
 (see [LaxMorphismOfRelAdjunctions.v]) and we can
 transform such morphisms of adjunctions using
-the theory developped in [TransformingLaxMorph.v].
-Finallly, out of this transformed morphism of adjunctions we can
+the theory developed in [TransformingLaxMorph.v].
+Finally, out of this transformed morphism of adjunctions we can
 extract a lax morphism between monads Tθ : T M1 → T M2, as expected.
 This last step is also performed in [TransformingLaxMorph.v].
 

ssprove.opam

@@ -8,10 +8,10 @@ homepage: "https://github.com/SSProve/ssprove"
 bug-reports: "https://github.com/SSProve/ssprove/issues"
 license: "MIT"
 depends: [
-  "coq" {= "8.14"}
+  "coq" {(>= "8.16" & < "8.18~")}
   "coq-equations" {>= "1.3"}
-  "coq-mathcomp-ssreflect" {(>= "1.13.0" & < "1.14~")}
-  "coq-mathcomp-analysis" {= "0.3.13"}
+  "coq-mathcomp-ssreflect" {(>= "1.15.0" & < "1.17~")}
+  "coq-mathcomp-analysis" {>= "0.5.3" & <= "0.6.1"}
   "coq-extructures" {(>= "0.3.1" & < "dev")}
   "coq-deriving" {(>= "0.1" & < "dev")}
 ]

theories/Crypt/choice_type.v

@@ -275,7 +275,7 @@ Section choice_typeTypes.
     intros x y.
     induction x as [ | | | x1 ih1 x2 ih2| x1 ih1 x2 ih2| x ih| x]
     in y |- *.
-    all: try solve [ destruct y ; intuition ; reflexivity ].
+    all: try solve [ destruct y ; auto with solve_subterm; reflexivity ].
     - destruct y. all: try (intuition; reflexivity).
       cbn.
       specialize (ih1 y1). specialize (ih2 y2).
@@ -388,7 +388,8 @@ Section choice_typeTypes.
   Proof.
     intros x y.
     destruct (choice_type_eq x y) eqn:H.
-    - intuition.
+    - apply/orP.
+      by right.
     - apply/orP.
       left.
       unfold choice_type_eq in H.

theories/Crypt/examples/AsymScheme.v

@@ -121,7 +121,7 @@ Module AsymmetricScheme (π : AsymmetricSchemeParams)
   Definition i_cipher := #|Cipher|.
   Definition i_pk := #|PubKey|.
   Definition i_sk := #|SecKey|.
-  Definition i_bool := 2.
+  Definition i_bool : nat := 2.
 
   Local Open Scope package_scope.
 

theories/Crypt/examples/ElGamal.v

@@ -134,12 +134,13 @@ Module MyAlg <: AsymmetricSchemeAlgorithms MyParam.
   Definition challenge_id : nat := 8. (*challenge for LR *)
   Definition challenge_id' : nat := 9. (*challenge for real rnd *)
   Definition getpk_id : nat := 42. (* routine to get the public key *)
+  Definition query_id : nat := 10.
 
   Definition i_plain := #|Plain|.
   Definition i_cipher := #|Cipher|.
   Definition i_pk := #|PubKey|.
   Definition i_sk := #|SecKey|.
-  Definition i_bool := 2.
+  Definition i_bool : nat := 2.
 
   (** Key Generation algorithm *)
   Definition KeyGen {L : {fset Location}} :
@@ -208,9 +209,9 @@ Definition DH_loc := fset [:: pk_loc ; sk_loc].
 
 Definition DH_real :
   package DH_loc [interface]
-    [interface #val #[10] : 'unit → 'pubkey × 'cipher ] :=
+    [interface #val #[query_id] : 'unit → 'pubkey × 'cipher ] :=
     [package
-      #def #[10] (_ : 'unit) : 'pubkey × 'cipher
+      #def #[query_id] (_ : 'unit) : 'pubkey × 'cipher
       {
         a ← sample uniform i_sk ;;
         let a := otf a in
@@ -224,9 +225,9 @@ Definition DH_real :
 
 Definition DH_rnd :
   package DH_loc [interface]
-    [interface #val #[10] : 'unit → 'pubkey × 'cipher ] :=
+    [interface #val #[query_id] : 'unit → 'pubkey × 'cipher ] :=
     [package
-      #def #[10] (_ : 'unit) : 'pubkey × 'cipher
+      #def #[query_id] (_ : 'unit) : 'pubkey × 'cipher
       {
         a ← sample uniform i_sk ;;
         let a := otf a in
@@ -242,7 +243,7 @@ Definition DH_rnd :
 
 Definition Aux :
   package (fset [:: counter_loc ; pk_loc ])
-    [interface #val #[10] : 'unit → 'pubkey × 'cipher]
+    [interface #val #[query_id] : 'unit → 'pubkey × 'cipher]
     [interface
       #val #[getpk_id] : 'unit → 'pubkey ;
       #val #[challenge_id'] : 'plain → 'cipher
@@ -257,7 +258,7 @@ Definition Aux :
 
     #def #[challenge_id'] (m : 'plain) : 'cipher
     {
-      #import {sig #[10] : 'unit → 'pubkey × 'cipher } as query ;;
+      #import {sig #[query_id] : 'unit → 'pubkey × 'cipher } as query ;;
       count ← get counter_loc ;;
       #put counter_loc := (count + 1)%N ;;
       #assert (count == 0)%N ;;

theories/Crypt/examples/OVN.v

@@ -189,8 +189,8 @@ End CDSParams.
 
 Module OVN (π2 : CDSParams) (Alg2 : SigmaProtocolAlgorithms π2).
 
-  Module Sigma1 := (Schnorr GP).
-  Module Sigma2 := (SigmaProtocol π2 Alg2).
+  Module Sigma1 := Schnorr GP.
+  Module Sigma2 := SigmaProtocol π2 Alg2.
 
   Obligation Tactic := idtac.
   Set Equations Transparent.

theories/Crypt/package/pkg_core_definition.v

@@ -551,7 +551,8 @@ Section FreeLocations.
     move /eqP => Q.
     rewrite -Q.
     rewrite in_fsetU.
-    intuition.
+    apply/orP.
+    by left.
   Defined.
 
   Let codeI locs := code locs import.
@@ -603,7 +604,8 @@ Section FreeMap.
     unfold fsubset in hs.
     move: hs. move /eqP => hs. rewrite -hs.
     rewrite in_fsetU.
-    intuition.
+    apply/orP.
+    auto.
   Defined.
 
   Let codeL I := code Locs I.

theories/Crypt/package/pkg_notation.v

@@ -328,6 +328,6 @@ Module PackageNotation.
     cbn. exists n. exact h.
   Defined.
 
-  Notation gfin n := (@give_fin n _).
+  Notation gfin n := (give_fin n).
 
 End PackageNotation.

theories/Crypt/package/pkg_rhl.v

@@ -2366,7 +2366,7 @@ Proof.
   eapply r_transR.
   - unfold fail.
     eapply rswap_cmd_eq with (c₀ := cmd_sample _) (c₁ := c).
-    eapply rsamplerC'_cmd with (c0 := c).
+    eapply rsamplerC'_cmd with (c := c).
   - simpl. unfold fail.
     eapply from_sem_jdg. intros [s₀ s₁]. hnf. intro P. hnf.
     intros [hpre hpost]. simpl.

theories/Crypt/package/pkg_tactics.v

@@ -95,6 +95,20 @@ Proof.
   f_equal. apply functional_extensionality. auto.
 Qed.
 
+#[export] Instance cmd_bind_morphism (A B : choiceType) :
+  Proper (eq ==> pointwise_relation A eq ==> eq) (@cmd_bind A B).
+Proof.
+  simpl_relation.
+  f_equal. apply functional_extensionality. auto.
+Qed.
+
+#[export] Instance bindrFree_morphism (A B : choiceType) c k :
+  Proper (eq ==> pointwise_relation A eq ==> eq) (@FreeProbProg.bindrFree c k A B).
+Proof.
+  simpl_relation.
+  f_equal. apply functional_extensionality. auto.
+Qed.
+
 (** Some validity lemmata and hints *)
 (* TODO MOVE? *)
 

theories/Crypt/rhl_semantics/state_prob/OrderEnrichedRelativeAdjunctionsExamples.v

@@ -24,10 +24,10 @@ Section ConstantFunctor.
 
   Program Definition mkConstFunc : ord_functor C D := mkOrdFunctor (fun c => d) _ _ _ _.
   Next Obligation.
-    intuition.
+    auto with solve_subterm.
   Defined.
   Next Obligation.
-    cbv. intuition.
+    cbv. auto with solve_subterm.
   Qed.
   Next Obligation.
     cbv. intuition. rewrite ord_cat_law1. reflexivity.

theories/Crypt/rules/RulesProb.v

@@ -614,7 +614,7 @@ Proof.
   rewrite HeqH11.
   assert ((fun x : X => (A x)%:R * psum (fun w : Choice.Pack chY => d (x, w))) = (fun x : X => psum (fun w : Choice.Pack chY => (A x)%:R * d (x, w)))) as H4.
   { extensionality k. rewrite -psumZ. reflexivity.
-    case (A k); intuition. by rewrite ler01. }
+    case (A k); intuition; by rewrite ler01. }
   rewrite H4.
   assert ((fun x : Y => (B x)%:R * dsnd d x) = (fun y : Y => (B y)%:R * psum (fun w => d (w, y)))) as HeqH12.
   { extensionality K. rewrite dsndE. reflexivity. }
@@ -722,7 +722,7 @@ Proof.
   rewrite HeqH11.
   assert ((fun x : X => (A x)%:R * psum (fun w : Choice.Pack chY => d (x, w))) = (fun x : X => psum (fun w : Choice.Pack chY => (A x)%:R * d (x, w)))) as H4.
   { extensionality k. rewrite -psumZ. reflexivity.
-    case (A k); intuition. by rewrite ler01. }
+    case (A k); intuition; by rewrite ler01. }
   rewrite H4.
   assert ((fun x : Y => (B x)%:R * dsnd d x) = (fun y : Y => (B y)%:R * psum (fun w => d (w, y)))) as HeqH12.
   { extensionality K. rewrite dsndE. reflexivity. }
@@ -739,7 +739,7 @@ Proof.
   - move => [x1 x2] /=.
     apply /andP. split.
     -- apply: mulr_ge0.
-       --- case: (A x1); rewrite //=. exact ler01.
+       --- case: (A x1); rewrite //=; exact ler01.
        --- by inversion d.
     -- have Hd0 : 0 <= d(x1,x2) by inversion d.
        have [Hdor1 | Hdor2]: 0 == d(x1,x2) \/ 0 < d(x1,x2).
@@ -748,13 +748,12 @@ Proof.
        --- move/eqP : Hdor1 => Hdor1.
            by rewrite -Hdor1 !GRing.mulr0.
        --- apply: ler_pmul.
-           + case: (A x1); rewrite //=. exact ler01.
+           + case: (A x1); rewrite //=; exact ler01.
            + by inversion d.
            + move:  (H2 x1 x2 Hdor2) => HAB.
              destruct (A x1) eqn: Ax1; rewrite //=;
-             destruct (B x2) eqn : Bx2; rewrite //=.
+             destruct (B x2) eqn : Bx2; rewrite //=; try exact ler01.
              exfalso. by apply: true_false_False.
-             exact ler01.
              auto.
   (* summable B *)
     assert ((fun x : (prod_choiceType (Choice.Pack chX) (Choice.Pack chY)) =>

theories/Crypt/rules/RulesStateProb.v

@@ -236,7 +236,8 @@ Proof.
   - apply bind_rule with (wf := (fun '(a1, a2) => fromPrePost (fun '(s1, s2) => middle (a1, s1) (a2, s2)) post)).
     + exact judge_wm.
     + exact judge_wf.
-  - cbv. intuition.
+  - cbv.
+    intuition auto with funelim.
 Qed.
 
 (* Pre-condition manipulating rules *)
@@ -623,7 +624,7 @@ Proof.
   rewrite HeqH11. simpl in HeqH11.
   assert ((fun x : X * S1 => (A x)%:R * psum (fun w => d (x, w))) = (fun x : X * S1 => psum (fun w => (A x)%:R * d (x, w)))) as H4.
   { extensionality k. rewrite -psumZ. reflexivity.
-    case (A k); intuition. by rewrite ler01. }
+    case (A k); intuition; by rewrite ler01. }
   rewrite H4.
   assert ((fun x : Y * S2 => (B x)%:R * dsnd d x) = (fun y : Y * S2 => (B y)%:R * psum (fun w => d (w, y)))) as HeqH12.
   { extensionality K. rewrite dsndE. reflexivity. }

theories/Crypt/rules/UniformStateProb.v

@@ -221,12 +221,12 @@ Proof.
       rewrite ler_pmul2l.
       * rewrite ler_int. auto.
       * unfold r. apply mulr_gt0.
-        -- cbn. rewrite posnum.one_pos_gt0. reflexivity.
+        -- cbn. rewrite ltr01. reflexivity.
         -- rewrite -(@pmulr_rgt0 _ #|F1|%:~R).
             ++ rewrite -(GRing.mul1r (#|F1|%:~R / #|F1|%:~R)).
               rewrite GRing.mulrA.
               rewrite GRing.Theory.mulfK.
-              ** rewrite posnum.one_pos_gt0. reflexivity.
+              ** rewrite ltr01. reflexivity.
               ** unshelve eapply card_non_zero. auto.
             ++ eapply fintype0 in w0 as h.
               destruct #|F1| eqn:e. 1: contradiction.