Compatibility with 8.16 and beyond, external zify (#6)

* port to external zify and latest MathComp

* rely on zify package, update for 8.16 and beyond, generate boilerplate

* use [fsfun f with ...] from finmap, purge local setfs extension

* adjust lower bound and generate boilerplate

* compatibility with dev version of dependencies

* restrict uses of intuition tactic for compatibility

* fix duplicate-clear warnings

* avoid needless warning supression

.github/workflows/coq-ci.yml → .github/workflows/docker-action.yml

@@ -1,4 +1,6 @@
-name: CI
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
 
 on:
   push:
@@ -15,15 +17,19 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-algorand.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -1,9 +1,12 @@
 # Algorand Verification
 
-[![CI][action-shield]][action-link]
+[![Docker CI][docker-action-shield]][docker-action-link]
+
+[docker-action-shield]: https://github.com/runtimeverification/algorand-verification/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/runtimeverification/algorand-verification/actions?query=workflow:"Docker%20CI"
+
+
 
-[action-shield]: https://github.com/runtimeverification/algorand-verification/workflows/CI/badge.svg?branch=master
-[action-link]: https://github.com/runtimeverification/algorand-verification/actions?query=workflow%3ACI
 
 The Algorand consensus protocol is the foundation of a decentralized
 digital currency and transactions platform. This project provides a
@@ -14,12 +17,13 @@ a formal proof of safety for the transition system.
 ## Meta
 
 - License: [University of Illinois/NCSA Open Source License](LICENSE.md)
-- Compatible Coq versions: 8.12
+- Compatible Coq versions: 8.14 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.11.0](https://math-comp.github.io)
+  - [MathComp ssreflect 1.14.0 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
-  - [MathComp finmap 1.5.0](https://github.com/math-comp/finmap)
-  - [MathComp analysis 0.3.2](https://github.com/math-comp/analysis)
+  - [MathComp finmap 1.5.1 or later](https://github.com/math-comp/finmap)
+  - [MathComp analysis 0.5.0 or later](https://github.com/math-comp/analysis)
+  - [Mczify](https://github.com/math-comp/mczify)
   - [Coq record update](https://github.com/tchajed/coq-record-update)
 - Coq namespace: `Algorand`
 - Related publication(s):
@@ -28,12 +32,12 @@ a formal proof of safety for the transition system.
 ## Building
 
 We recommend installing the dependencies of the project via
-[OPAM](http://opam.ocaml.org/doc/Install.html), for example:
+[opam](http://opam.ocaml.org/doc/Install.html), for example:
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq.8.12.0 coq-mathcomp-ssreflect.1.11.0 \
-  coq-mathcomp-algebra coq-mathcomp-finmap.1.5.0 \
-  coq-mathcomp-analysis.0.3.2 coq-record-update
+opam install coq.8.16.0 coq-mathcomp-ssreflect.1.15.0 \
+ coq-mathcomp-algebra coq-mathcomp-finmap.1.5.2 \
+ coq-mathcomp-analysis.0.5.4 coq-mathcomp-zify coq-record-update
 ```
 
 Then, run `make` in the project root directory. This will check all the definitions and proofs.
@@ -52,7 +56,6 @@ Statements of some _liveness_ properties for the transition system are also prov
 
 All Coq source files can be found under the `theories` directory, and their content is as follows:
 
-- `zify.v`: definitions for using the `lia` arithmetic tactic for MathComp from [mczify](https://github.com/pi8027/mczify)
 - `fmap_ext.v`: auxiliary definitions and results on finite maps
 - `algorand_model.v`: definition of the Algorand local state, global state, and transition system, along with helper functions and facts
 - `safety_helpers.v`: helper functions and lemmas used when proving safety of the transition system

_CoqProject

@@ -1,13 +1,7 @@
 -Q theories Algorand
 
--arg -w -arg -notation-incompatible-format
 -arg -w -arg -notation-overridden
--arg -w -arg -projection-no-head-constant
--arg -w -arg -redundant-canonical-projection
--arg -w -arg -duplicate-clear
--arg -w -arg -ambiguous-paths
 
-theories/zify.v
 theories/fmap_ext.v
 theories/algorand_model.v
 theories/safety_helpers.v

coq-algorand.opam

@@ -18,11 +18,12 @@ a formal proof of safety for the transition system."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {>= "8.12" & < "8.13~"}
-  "coq-mathcomp-ssreflect" {>= "1.11" & < "1.12~"}
+  "coq" {>= "8.14"}
+  "coq-mathcomp-ssreflect" {>= "1.14"}
   "coq-mathcomp-algebra" 
-  "coq-mathcomp-finmap" {>= "1.5"}
-  "coq-mathcomp-analysis" {>= "0.3.2"}
+  "coq-mathcomp-finmap" {>= "1.5.1"}
+  "coq-mathcomp-analysis" {>= "0.5.0"}
+  "coq-mathcomp-zify" 
   "coq-record-update" 
 ]
 

meta.yml

@@ -40,33 +40,43 @@ license:
   file: LICENSE.md
 
 supported_coq_versions:
-  text: '8.12'
-  opam: '{>= "8.12" & < "8.13~"}'
+  text: '8.14 or later'
+  opam: '{>= "8.14"}'
 
 tested_coq_opam_versions:
-- version: '1.11.0-coq-8.12'
+- version: '1.15.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.11" & < "1.12~"}'
+    version: '{>= "1.14"}'
   description: |-
-    [MathComp ssreflect 1.11.0](https://math-comp.github.io)
+    [MathComp ssreflect 1.14.0 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-finmap
-    version: '{>= "1.5"}'
+    version: '{>= "1.5.1"}'
   description: |-
-    [MathComp finmap 1.5.0](https://github.com/math-comp/finmap)
+    [MathComp finmap 1.5.1 or later](https://github.com/math-comp/finmap)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{>= "0.3.2"}'
+    version: '{>= "0.5.0"}'
+  description: |-
+    [MathComp analysis 0.5.0 or later](https://github.com/math-comp/analysis)
+- opam:
+    name: coq-mathcomp-zify
   description: |-
-    [MathComp analysis 0.3.2](https://github.com/math-comp/analysis)
+    [Mczify](https://github.com/math-comp/mczify)
 - opam:
     name: coq-record-update
   description: |-
@@ -87,12 +97,12 @@ build: |-
   ## Building
   
   We recommend installing the dependencies of the project via
-  [OPAM](http://opam.ocaml.org/doc/Install.html), for example:
+  [opam](http://opam.ocaml.org/doc/Install.html), for example:
   ```shell
   opam repo add coq-released https://coq.inria.fr/opam/released
-  opam install coq.8.12.0 coq-mathcomp-ssreflect.1.11.0 \
-    coq-mathcomp-algebra coq-mathcomp-finmap.1.5.0 \
-    coq-mathcomp-analysis.0.3.2 coq-record-update
+  opam install coq.8.16.0 coq-mathcomp-ssreflect.1.15.0 \
+   coq-mathcomp-algebra coq-mathcomp-finmap.1.5.2 \
+   coq-mathcomp-analysis.0.5.4 coq-mathcomp-zify coq-record-update
   ```
 
   Then, run `make` in the project root directory. This will check all the definitions and proofs.
@@ -112,7 +122,6 @@ documentation: |-
 
   All Coq source files can be found under the `theories` directory, and their content is as follows:
 
-  - `zify.v`: definitions for using the `lia` arithmetic tactic for MathComp from [mczify](https://github.com/pi8027/mczify)
   - `fmap_ext.v`: auxiliary definitions and results on finite maps
   - `algorand_model.v`: definition of the Algorand local state, global state, and transition system, along with helper functions and facts
   - `safety_helpers.v`: helper functions and lemmas used when proving safety of the transition system

theories/algorand_model.v

@@ -1,22 +1,11 @@
-From mathcomp.ssreflect
-Require Import all_ssreflect.
-
-From mathcomp.finmap
-Require Import finmap multiset.
-
-From Coq
-Require Import Reals Relation_Definitions Relation_Operators.
-
-From mathcomp.analysis
-Require Import boolp Rstruct.
-
-From RecordUpdate
-Require Import RecordSet.
+From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import finmap multiset.
+From Coq Require Import Reals Relation_Definitions Relation_Operators.
+From mathcomp Require Import boolp Rstruct.
+From RecordUpdate Require Import RecordSet.
+From Algorand Require Import fmap_ext.
 Import RecordSetNotations.
 
-From Algorand
-Require Import fmap_ext.
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -236,7 +225,7 @@ Record UState :=
     nextvotes_val : {fsfun nat * nat * nat -> seq Vote with [::]} (**r a sequence of value-nextvotes seen for the given round/period/step *)
    }.
 
-Instance UState_Settable : Settable _ :=
+#[export] Instance UState_Settable : Settable _ :=
   settable! mkUState <corrupt;round;period;step;timer;deadline;p_start;
    proposals;stv;blocks;softvotes;certvotes;nextvotes_open;nextvotes_val>.
 
@@ -263,22 +252,28 @@ Canonical UState_choiceType := ChoiceType UState (PcanChoiceMixin cancelUState).
 
 (** Update functions for sequences maintained in the user state. *)
 Definition set_proposals u r' p' prop : UState :=
-  u <| proposals := setfs u.(proposals) (r', p') (undup (prop :: u.(proposals) (r', p'))) |>.
+  u <| proposals := [fsfun u.(proposals) with
+   (r', p') |-> (undup (prop :: u.(proposals) (r', p')))] |>.
 
 Definition set_blocks (u : UState) (r':nat) block : UState :=
-  u <| blocks := setfs u.(blocks) r' (undup (block :: u.(blocks) r')) |>.
+  u <| blocks := [fsfun u.(blocks) with
+   r' |-> (undup (block :: u.(blocks) r'))] |>.
 
 Definition set_softvotes (u : UState) r' p' sv : UState :=
-  u <| softvotes := setfs u.(softvotes) (r', p') (undup (sv :: u.(softvotes) (r', p'))) |>.
+  u <| softvotes := [fsfun u.(softvotes) with
+   (r', p') |-> (undup (sv :: u.(softvotes) (r', p')))] |>.
 
 Definition set_certvotes (u : UState) r' p' sv : UState :=
-  u <| certvotes := setfs u.(certvotes) (r', p') (undup (sv :: u.(certvotes) (r', p'))) |>.
+  u <| certvotes := [fsfun u.(certvotes) with
+   (r', p') |-> (undup (sv :: u.(certvotes) (r', p')))] |>.
 
 Definition set_nextvotes_open (u : UState) r' p' s' nvo : UState :=
-  u <| nextvotes_open := setfs u.(nextvotes_open) (r', p', s') (undup (nvo :: u.(nextvotes_open) (r', p', s'))) |>.
+  u <| nextvotes_open := [fsfun u.(nextvotes_open) with
+   (r', p', s') |-> (undup (nvo :: u.(nextvotes_open) (r', p', s')))] |>.
 
 Definition set_nextvotes_val (u : UState) r' p' s' nvv : UState :=
-  u <| nextvotes_val := setfs u.(nextvotes_val) (r', p', s') (undup (nvv :: u.(nextvotes_val) (r', p', s'))) |>.
+  u <| nextvotes_val := [fsfun u.(nextvotes_val) with
+   (r', p', s') |-> (undup (nvv :: u.(nextvotes_val) (r', p', s')))] |>.
 
 (** Update function for advancing the period of a user state. *)
 Definition advance_period (u : UState) : UState :=
@@ -310,7 +305,7 @@ Record GState :=
     msg_history : {mset Msg} (**r the history of all broadcasted messages as a multiset of messages *)
   }.
 
-Instance GState_Settable : Settable _ :=
+#[export] Instance GState_Settable : Settable _ :=
  settable! mkGState <now;network_partition;users;msg_in_transit;msg_history>.
 
 (** State with empty maps, unpartitioned, at global time 0. *)

theories/dune

@@ -1,5 +1,5 @@
 (coq.theory
  (name Algorand)
  (package coq-algorand)
- (synopsis "A verified model of Algorand in Coq")
- (flags -w -notation-overridden -w -projection-no-head-constant -w -redundant-canonical-projection -w -duplicate-clear -w -ambiguous-paths -w -notation-incompatible-format))
+ (synopsis "A verified model of the Algorand consensus protocol in Coq")
+ (flags :standard -w -notation-overridden))