preparing v2.2.0 release (#44)

aleksnanevski · web-flow · commit e0d2a6c94626 · 2025-06-12T11:30:45.000+02:00
Adapting to coq-fcsl-pcm 2.2.0 along with other dependencies (coq 9.0 and mathcomp 2.4.0).
Dropped support for coq 8.0 and mathcomp 2.3.0.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,8 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
-          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
diff --git a/README.md b/README.md
@@ -39,13 +39,13 @@ that HTT implements Separation logic as a shallow embedding in Coq.
   - Alexander Gryzlov
   - Marcos Grandury
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: 8.19 or later
+- Compatible Coq versions: 9.0 or later
 - Additional dependencies:
   - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
   - [MathComp ssreflect 2.2 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
-  - [FCSL-PCM 2.1](https://github.com/imdea-software/fcsl-pcm)
+  - [FCSL-PCM 2.2](https://github.com/imdea-software/fcsl-pcm)
   - [Dune](https://dune.build) 3.6 or later
 - Coq namespace: `htt`
 - Related publication(s):
diff --git a/coq-htt-core.opam b/coq-htt-core.opam
@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "fcsl@software.imdea.org"
-version: "2.1.0"
+version: "2.2.0"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -31,16 +31,15 @@ variables). The connection reconciles dependent types with effects of state and
 establishes Separation logic as a type theory for such effects. In implementation terms, it means
 that HTT implements Separation logic as a shallow embedding in Coq."""
 
-build: [make "-C" "htt" "-j%{jobs}%"]
-install: [make "-C" "htt" "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
+  "coq" { (>= "9.0" & < "9.1~") | (= "dev") }
   "coq-hierarchy-builder" { (>= "1.7.0" & < "1.10~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }
+  "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }
 ]
 
 tags: [
diff --git a/coq-htt.opam b/coq-htt.opam
@@ -1,6 +1,6 @@
 opam-version: "2.0"
 maintainer: "fcsl@software.imdea.org"
-version: "2.1.0"
+version: "2.2.0"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -32,11 +32,11 @@ build: [make "-C" "examples" "-j%{jobs}%"]
 install: [make "-C" "examples" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") }
+  "coq" { (>= "9.0" & < "9.1~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }
+  "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }
   "coq-htt-core" {= version}
 ]
 
diff --git a/examples/Make b/examples/Make
diff --git a/examples/Makefile b/examples/Makefile
diff --git a/examples/array.v b/examples/array.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path fintype tuple finfun finset.
 From pcm Require Import options axioms prelude pred.
 From pcm Require Import pcm unionmap heap.
diff --git a/examples/bintree.v b/examples/bintree.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq ssrnat.
 From pcm Require Import options axioms pred.
 From pcm Require Import pcm unionmap heap autopcm automap.
diff --git a/examples/bst.v b/examples/bst.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype ssrnat seq path.
 From pcm Require Import options axioms pred ordtype seqext.
 From pcm Require Import pcm unionmap heap autopcm automap.
diff --git a/examples/bubblesort.v b/examples/bubblesort.v
@@ -16,7 +16,8 @@ From mathcomp Require Import ssrnat eqtype seq path fintype tuple.
 From mathcomp Require Import finfun fingroup perm order interval.
 From pcm Require Import options axioms prelude pred ordtype slice.
 From pcm Require Import seqext pcm unionmap heap.
-From htt Require Import options model heapauto array.
+From htt Require Import options model heapauto.
+From htt Require Import array.
 Import Order.NatOrder Order.TTheory.
 Local Open Scope order_scope.
 Local Open Scope nat_scope.
diff --git a/examples/congmath.v b/examples/congmath.v
@@ -12,7 +12,7 @@ limitations under the License.
 *)
 
 From HB Require Import structures.
-From Coq Require Import Recdef Setoid ssreflect ssrbool ssrfun.
+From Stdlib Require Import Recdef Setoid ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype choice ssrnat seq bigop fintype finfun.
 From pcm Require Import options prelude ordtype finmap pred seqext.
 
diff --git a/examples/cyclic.v b/examples/cyclic.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq ssrnat.
 From pcm Require Import options axioms pred seqext.
 From pcm Require Import pcm unionmap heap auto automap autopcm.
diff --git a/examples/dlist.v b/examples/dlist.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq.
 From pcm Require Import options axioms pred.
 From pcm Require Import pcm unionmap heap autopcm.
diff --git a/examples/dune b/examples/dune
diff --git a/examples/exploit.v b/examples/exploit.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool Logic.Hurkens.
+From Stdlib Require Import ssreflect ssrbool Logic.Hurkens.
 
 (* This file shows the unsoundness of the axiom pack_injective assumed in *)
 (* the implementation of Ynot2.0. The proof relies on the lemma of        *)
diff --git a/examples/gcd.v b/examples/gcd.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype div.
 From pcm Require Import axioms pred ordtype pcm heap.
 From htt Require Import options model heapauto.
diff --git a/examples/hashtab.v b/examples/hashtab.v
@@ -12,7 +12,7 @@ limitations under the License.
 *)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq fintype tuple finfun finset.
 From pcm Require Import options axioms prelude pred ordtype finmap.
 From pcm Require Import pcm unionmap heap autopcm.
diff --git a/examples/kvmaps.v b/examples/kvmaps.v
@@ -16,7 +16,7 @@ limitations under the License.
 (******************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq path ssrnat.
 From pcm Require Import options axioms pred ordtype finmap seqext.
 From pcm Require Import pcm unionmap heap autopcm automap.
diff --git a/examples/queue.v b/examples/queue.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype ssrnat seq.
 From pcm Require Import options axioms pred.
 From pcm Require Import pcm unionmap heap automap.
diff --git a/examples/quicksort.v b/examples/quicksort.v
@@ -303,8 +303,8 @@ case: oleqP=>Hfp.
   - step=>_; split.
     - rewrite Sbo_eq; apply/andP; split=>//.
       by apply/leq_ltn_trans/Hj.
-    exists (tperm i j); rewrite Sbo_eq; split=>//.
-    - rewrite -(eqP Hj1).
+    exists (tperm i j); rewrite Sbo_eq; split=>//.  
+    - rewrite -(eqP Hj1).      
       apply/(subset_trans (tperm_on i j))/subsetP=>/= x; rewrite !inE ltnS.
       by case/orP=>/eqP->; rewrite leqnn // andbT.
     - rewrite slice_oSR slice_xR; last by rewrite bnd_simp.
diff --git a/examples/stack.v b/examples/stack.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype seq.
 From pcm Require Import options axioms pred.
 From pcm Require Import pcm unionmap heap autopcm.
diff --git a/htt/Make b/htt/Make
diff --git a/htt/Makefile b/htt/Makefile
diff --git a/htt/domain.v b/htt/domain.v
@@ -12,7 +12,7 @@ limitations under the License.
 *)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype.
 From pcm Require Import options axioms pred prelude.
 
diff --git a/htt/dune b/htt/dune
diff --git a/htt/model.v b/htt/model.v
@@ -1292,13 +1292,33 @@ move=>Hp Hv Hx; apply/vrf_bnd/(gU _ Hp).
 by move=>ex m H V _; apply: Hx.
 Qed.
 
+(* variant of stepU that adds the new heap to the right *)
+Lemma stepV G A B (pq : spec G A) (e : STspec G pq) (e2 : A -> ST B)
+             i (Q : post B) g :
+        (pq g).1 Unit ->
+        (forall x m, (pq g).2 (Val x) m -> vrf (i \+ m) (e2 x) Q) ->
+        (forall x m, (pq g).2 (Exn x) m ->
+           valid (i \+ m) -> Q (Exn x) (i \+ m)) ->
+        vrf i (bnd e e2) Q.
+Proof.
+move=>H1 H2 H3; apply: stepU H1 _ _ =>x m H1; rewrite !(joinC m).
+- by apply: H2.
+by apply: H3.
+Qed.
+
 Arguments stepU {G A B pq e e2 i Q}. 
+Arguments stepV {G A B pq e e2 i Q}. 
 
 Notation "[stepU]" := (stepU tt) (at level 0).
 Notation "[ 'stepU' x1 , .. , xn ]" :=
   (stepU (existT _ x1 .. (existT _ xn tt) ..))
   (at level 0, format "[ 'stepU'  x1 ,  .. ,  xn ]").
 
+Notation "[stepV]" := (stepV tt) (at level 0).
+Notation "[ 'stepV' x1 , .. , xn ]" :=
+  (stepU (existT _ x1 .. (existT _ xn tt) ..))
+  (at level 0, format "[ 'stepV'  x1 ,  .. ,  xn ]").
+
 (* combination of gU + vrf_try *)
 Lemma tryU G A B (pq : spec G A) (e : STspec G pq)
              (e1 : A -> ST B) (e2 : exn -> ST B) i (Q : post B) g :
diff --git a/meta.yml b/meta.yml
@@ -72,22 +72,18 @@ maintainers:
 
 opam-file-maintainer: fcsl@software.imdea.org
 
-opam-file-version: 2.1.0
+opam-file-version: 2.2.0
 
 license:
   fullname: Apache-2.0
   identifier: Apache-2.0
   file: LICENSE
 
 supported_coq_versions:
-  text: 8.19 or later
-  opam: '{ (>= "8.19" & < "9.1~") | (= "dev") }'
+  text: 9.0 or later
+  opam: '{ (>= "9.0" & < "9.1~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.19'
-  repo: 'mathcomp/mathcomp'
-- version: '2.3.0-coq-8.20'
-  repo: 'mathcomp/mathcomp'
 - version: '2.4.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
 - version: 'rocq-prover-dev'
@@ -102,7 +98,7 @@ dependencies:
     [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "2.2.0" & < "2.5~") | (= "dev") }'
+    version: '{ (>= "2.4.0" & < "2.5~") | (= "dev") }'
   description: |-
     [MathComp ssreflect 2.2 or later](https://math-comp.github.io)
 - opam:
@@ -115,9 +111,9 @@ dependencies:
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-fcsl-pcm
-    version: '{ (>= "2.1.0" & < "2.2~") | (= "dev") }'
+    version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }'
   description: |-
-    [FCSL-PCM 2.1](https://github.com/imdea-software/fcsl-pcm)
+    [FCSL-PCM 2.2](https://github.com/imdea-software/fcsl-pcm)
 
 namespace: htt
 
