Merge pull request #40 from sertel/mathcomp.2.1.0

Mathcomp 2.1.0 support

.github/workflows/build.yml

@@ -35,7 +35,7 @@ jobs:
       - name: Install OCaml
         uses: avsm/setup-ocaml@v1
         with:
-          ocaml-version: 4.09.1
+          ocaml-version: 4.14.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.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 install coq.8.18.0 coq-equations.1.3+8.18 coq-mathcomp-ssreflect.2.1.0 coq-mathcomp-analysis.1.0.0 coq-extructures.0.4.0 coq-deriving.0.2.0
           opam exec -- make -j4
 

_CoqProject

@@ -22,6 +22,7 @@ theories/Relational/Commutativity.v
 
 theories/Crypt/Prelude.v
 theories/Crypt/Axioms.v
+theories/Crypt/Casts.v
 theories/Crypt/choice_type.v
 
 # Categorical semantics
@@ -89,7 +90,7 @@ theories/Crypt/examples/KEMDEM.v
 theories/Crypt/examples/RandomOracle.v
 theories/Crypt/examples/SigmaProtocol.v
 theories/Crypt/examples/Schnorr.v
-theories/Crypt/examples/OVN.v
+# theories/Crypt/examples/OVN.v
 theories/Crypt/examples/Executor.v
 
 # Examples from https://github.com/Som1Lse/joy-of-ssprove

flake.nix

@@ -0,0 +1,52 @@
+{
+  inputs = {
+    nixpkgs.url        = github:nixos/nixpkgs;
+    flake-utils.url    = github:numtide/flake-utils;
+  };
+  outputs = { self, nixpkgs, flake-utils }:
+    let
+      mkDrv = { stdenv, which, coqPackages, coq } :
+           let
+             extructures' = coqPackages.extructures.override { version = "0.4.0"; };
+           in
+            stdenv.mkDerivation {
+              pname = "ssprove";
+              version = "0.0.1";
+              src = ./.;
+              nativeBuildInputs = [ which coq.ocamlPackages.findlib ] ++
+                                  (with coqPackages; [
+                                    equations
+                                    mathcomp-analysis
+                                    mathcomp-ssreflect
+                                    deriving
+                                  ])
+                                  ++ [extructures'];
+              buildInputs = [ coq ];
+            };
+    in { inherit mkDrv; } //
+      flake-utils.lib.eachDefaultSystem (system:
+        let
+          pkgs = nixpkgs.legacyPackages.${system};
+        in
+         rec {
+            devShell =
+              let
+                args = {
+                  inherit (pkgs) stdenv which;
+                  coq = pkgs.coq_8_18;
+                  coqPackages = pkgs.coqPackages_8_18.overrideScope
+                    (self: super: {
+                      mathcomp = super.mathcomp.override { version = "2.1.0"; };
+                      mathcomp-analysis = super.mathcomp-analysis.override { version = "1.0.0"; };
+                    });
+                };
+                ssprove' = mkDrv args;
+              in
+                pkgs.mkShell {
+                  packages =
+                    (with pkgs; [ coq gnumake ])
+                    ++
+                    (with ssprove';  nativeBuildInputs);
+                };
+         });
+}

ssprove.opam

@@ -8,12 +8,12 @@ homepage: "https://github.com/SSProve/ssprove"
 bug-reports: "https://github.com/SSProve/ssprove/issues"
 license: "MIT"
 depends: [
-  "coq" {(>= "8.16" & < "8.18~")}
-  "coq-equations" {>= "1.3"}
-  "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")}
+  "coq" {(>= "8.18~")}
+  "coq-equations" {(>= "1.3+8.18")}
+  "coq-mathcomp-ssreflect" {(>= "2.1.0")}
+  "coq-mathcomp-analysis" {>= "1.0.0"}
+  "coq-extructures" {(>= "0.4.0" & < "dev")}
+  "coq-deriving" {(>= "0.2.0" & < "dev")}
 ]
 build: [
   [make "-j%{jobs}%"]

theories/Crypt/Casts.v

@@ -0,0 +1,37 @@
+Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format".
+From mathcomp Require Import ssreflect ssrbool ssrnat choice fintype.
+Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
+
+From extructures Require Import ord fmap.
+From Crypt Require Import Prelude.
+
+From HB Require Import structures.
+
+
+(**
+  Note for any of these types it would also be okay to write the cast, e.g., [(nat:choiceType)%type],
+  directly in the term.
+  This (backward-compatibility) file just made porting to mathcomp 2.1.0 easier.
+  Just delete as soon as all references to the below casts are gone from the code base.
+ *)
+
+Definition unit_choiceType : choiceType := Datatypes.unit.
+Definition nat_choiceType : choiceType := nat.
+Definition bool_choiceType : choiceType := bool.
+Definition prod_choiceType (A B: choiceType) : choiceType := prod A B.
+Definition fmap_choiceType (A: ordType) (B: choiceType) : choiceType := {fmap A -> B}.
+Definition option_choiceType (A: choiceType) : choiceType := option A.
+Definition fin_choiceType (p: positive) : choiceType := ordinal p.(pos).
+Definition sum_choiceType (A B: choiceType) : choiceType := (A + B)%type.
+
+Definition unit_ordType: ordType := Datatypes.unit.
+Definition nat_ordType: ordType := nat.
+Definition bool_ordType: ordType := bool.
+Definition prod_ordType (A B: ordType) : ordType := prod A B.
+Definition fmap_ordType (A B: ordType) : ordType := {fmap A -> B}.
+Definition option_ordType (A: ordType) : ordType := option A.
+Definition fin_ordType (p: positive) : ordType := ordinal p.(pos).
+Definition sum_ordType (A B: ordType) : ordType := (A + B)%type.
+
+
+Definition prod_finType (A B: finType) : finType := prod A B.

theories/Crypt/Prelude.v

@@ -5,6 +5,7 @@ From Coq Require Import Utf8 Lia.
 Set Warnings "-notation-overridden".
 From mathcomp Require Import ssreflect eqtype ssrbool ssrnat.
 Set Warnings "notation-overridden".
+From HB Require Import structures.
 From extructures Require Import ord fset.
 From Equations Require Import Equations.
 From Mon Require SPropBase.
@@ -180,9 +181,7 @@ Proof.
     intro h. apply e. inversion h. reflexivity.
 Qed.
 
-Canonical positive_eqMixin := EqMixin positive_eqP.
-  Canonical positive_eqType :=
-    Eval hnf in EqType positive positive_eqMixin.
+HB.instance Definition _ := hasDecEq.Build _ positive_eqP.
 
 (** Lt class, for finite types  *)
 
@@ -314,4 +313,4 @@ Definition testSome {A} (P : A → bool) (o : option A) : bool :=
   match o with
   | Some a => P a
   | None => false
-  end.
+  end.