From 20f1e50486bf3ff9b134525e93c32b1526c78e86 Mon Sep 17 00:00:00 2001 From: Aleksandar Nanevski Date: Thu, 12 Jun 2025 11:23:18 +0200 Subject: [PATCH] preparing v2.2.0 release --- .github/workflows/docker-action.yml | 2 -- README.md | 4 ++-- coq-htt-core.opam | 11 +++++------ coq-htt.opam | 8 ++++---- examples/Make | 29 ----------------------------- examples/Makefile | 7 ------- examples/array.v | 2 +- examples/bintree.v | 2 +- examples/bst.v | 2 +- examples/bubblesort.v | 3 ++- examples/congmath.v | 2 +- examples/cyclic.v | 2 +- examples/dlist.v | 2 +- examples/dune | 9 --------- examples/exploit.v | 2 +- examples/gcd.v | 2 +- examples/hashtab.v | 2 +- examples/kvmaps.v | 2 +- examples/queue.v | 2 +- examples/quicksort.v | 4 ++-- examples/stack.v | 2 +- htt/Make | 14 -------------- htt/Makefile | 7 ------- htt/domain.v | 2 +- htt/dune | 11 ----------- htt/model.v | 20 ++++++++++++++++++++ meta.yml | 16 ++++++---------- 27 files changed, 54 insertions(+), 117 deletions(-) delete mode 100644 examples/Make delete mode 100644 examples/Makefile delete mode 100644 examples/dune delete mode 100644 htt/Make delete mode 100644 htt/Makefile delete mode 100644 htt/dune diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 2aaf380..c9cc9b5 100644 --- 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 index 1099810..a4534b7 100644 --- 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 index 2d57070..1569926 100644 --- 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 index bb0c93a..34f4c55 100644 --- 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 deleted file mode 100644 index 05db16d..0000000 --- a/examples/Make +++ /dev/null @@ -1,29 +0,0 @@ --Q . htt - --arg -w -arg -notation-overridden --arg -w -arg -redundant-canonical-projection - -# release-specific arguments --arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 --arg -w -arg -deprecated-from-Coq # specific to coq8.21 --arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 - -exploit.v -gcd.v -counter.v -llist.v -dlist.v -array.v -queue.v -cyclic.v -stack.v -bintree.v -bst.v -kvmaps.v -hashtab.v -bubblesort.v -quicksort.v -congmath.v -congprog.v -tree.v -union_find.v diff --git a/examples/Makefile b/examples/Makefile deleted file mode 100644 index 103b008..0000000 --- a/examples/Makefile +++ /dev/null @@ -1,7 +0,0 @@ -# -*- Makefile -*- - -# setting variables -COQPROJECT?=Make - -# Main Makefile -include ../Makefile.common diff --git a/examples/array.v b/examples/array.v index d79fb40..2eef1df 100644 --- 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 index 81552af..ede7f40 100644 --- 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 index 3deedab..27c850e 100644 --- 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 index 5c68f47..205d72b 100644 --- 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 index fa4c2d3..76124cf 100644 --- 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 index 968ba47..47d8d78 100644 --- 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 index 72e551d..c0cf660 100644 --- 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 deleted file mode 100644 index af8c240..0000000 --- a/examples/dune +++ /dev/null @@ -1,9 +0,0 @@ -(coq.theory - (name htt) - (package coq-htt) - (synopsis "Hoare Type Theory with examples") - (flags :standard - -w -notation-overridden - -w -local-declaration - -w -redundant-canonical-projection - -w -projection-no-head-constant)) diff --git a/examples/exploit.v b/examples/exploit.v index f42ffa3..ed14cf6 100644 --- 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 index 40c39b0..526574c 100644 --- 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 index bc5e7c4..9830206 100644 --- 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 index 59a3c38..859b51b 100644 --- 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 index 2df546c..f62d6b0 100644 --- 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 index 1b8a894..06bd998 100644 --- 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 index d374dc8..fda64fa 100644 --- 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 deleted file mode 100644 index dca3ca7..0000000 --- a/htt/Make +++ /dev/null @@ -1,14 +0,0 @@ --Q . htt - --arg -w -arg -notation-overridden --arg -w -arg -redundant-canonical-projection - -# release-specific arguments --arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 --arg -w -arg -deprecated-from-Coq # specific to coq8.21 --arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 - -options.v -domain.v -model.v -heapauto.v diff --git a/htt/Makefile b/htt/Makefile deleted file mode 100644 index 103b008..0000000 --- a/htt/Makefile +++ /dev/null @@ -1,7 +0,0 @@ -# -*- Makefile -*- - -# setting variables -COQPROJECT?=Make - -# Main Makefile -include ../Makefile.common diff --git a/htt/domain.v b/htt/domain.v index 8ee1d97..700fca5 100644 --- 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 deleted file mode 100644 index a6eeaa3..0000000 --- a/htt/dune +++ /dev/null @@ -1,11 +0,0 @@ -; This file was generated from `meta.yml`, please do not edit manually. - -(coq.theory - (name htt) - (package coq-htt-core) - (synopsis "Hoare Type Theory") - (flags :standard - -w -notation-overridden - -w -local-declaration - -w -redundant-canonical-projection - -w -projection-no-head-constant)) diff --git a/htt/model.v b/htt/model.v index 854e2ad..8c1bb4a 100644 --- 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 index da7bebe..60b53b6 100644 --- a/meta.yml +++ b/meta.yml @@ -72,7 +72,7 @@ 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 @@ -80,14 +80,10 @@ license: 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