diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index cb1399b..0ba560f 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,7 +17,7 @@ jobs: image: - 'mathcomp/mathcomp:2.2.0-coq-8.19' - 'mathcomp/mathcomp:2.3.0-coq-8.20' - - 'mathcomp/mathcomp:latest-coq-dev' + - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: - uses: actions/checkout@v4 diff --git a/README.md b/README.md index 3d79121..e0c132c 100644 --- a/README.md +++ b/README.md @@ -44,7 +44,7 @@ that HTT implements Separation logic as a shallow embedding in Coq. - [MathComp ssreflect 2.2-2.3](https://math-comp.github.io) - [MathComp algebra](https://math-comp.github.io) - [MathComp fingroup](https://math-comp.github.io) - - [FCSL-PCM 2.0](https://github.com/imdea-software/fcsl-pcm) + - [FCSL-PCM 2.1](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 74837d7..e342fd1 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.0.1" +version: "2.1.0" homepage: "https://github.com/imdea-software/htt" dev-repo: "git+https://github.com/imdea-software/htt.git" @@ -31,14 +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: ["dune" "build" "-p" name "-j" jobs] +build: [make "-C" "htt" "-j%{jobs}%"] +install: [make "-C" "htt" "install"] depends: [ "dune" {>= "3.6"} "coq" { (>= "8.19" & < "8.21~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } "coq-mathcomp-algebra" "coq-mathcomp-fingroup" - "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") } + "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") } ] tags: [ diff --git a/coq-htt.opam b/coq-htt.opam index 56ea4f2..4265e46 100644 --- a/coq-htt.opam +++ b/coq-htt.opam @@ -1,6 +1,6 @@ opam-version: "2.0" maintainer: "fcsl@software.imdea.org" -version: "2.0.1" +version: "2.1.0" homepage: "https://github.com/imdea-software/htt" dev-repo: "git+https://github.com/imdea-software/htt.git" @@ -28,14 +28,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: ["dune" "build" "-p" name "-j" jobs] +build: [make "-C" "examples" "-j%{jobs}%"] +install: [make "-C" "examples" "install"] depends: [ "dune" {>= "3.6"} "coq" { (>= "8.19" & < "8.21~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } "coq-mathcomp-algebra" "coq-mathcomp-fingroup" - "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") } + "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") } "coq-htt-core" {= version} ] diff --git a/examples/llist.v b/examples/llist.v index 95682de..1adba0f 100644 --- a/examples/llist.v +++ b/examples/llist.v @@ -64,7 +64,7 @@ Lemma lseg_empty (xs : seq A) p q : Unit \In lseg p q xs -> p = q /\ xs = [::]. Proof. -by case: xs=>[|x xs][] //= r [h][/esym/umap0E][/unitbP]; rewrite um_unitbU. +by case: xs=>[|x xs][] //= r [h][/esym/join0I][/unitbP]; rewrite um_unitbU. Qed. (* reformulation of the specification *) diff --git a/examples/quicksort.v b/examples/quicksort.v index d405474..c6530e0 100644 --- a/examples/quicksort.v +++ b/examples/quicksort.v @@ -23,6 +23,7 @@ From mathcomp Require order. Import order.Order.NatOrder order.Order.TTheory. Local Open Scope order_scope. + (* Brief mathematics of quickorting *) (* There is some overlap with mathematics developed for bubblesort *) (* but the development is repeated here to make the files *) diff --git a/htt/model.v b/htt/model.v index a2c66e4..29663ca 100644 --- a/htt/model.v +++ b/htt/model.v @@ -1233,6 +1233,29 @@ Notation "[ 'tryE' x1 , .. , xn ]" := (tryE (existT _ x1 .. (existT _ xn tt) ..)) (at level 0, format "[ 'tryE' x1 , .. , xn ]"). +(* backward symbolic execution by one step *) +Lemma bnd_vrf G A B (pq : A -> spec G B) (g : G) (e1 : ST A) + (e2 : forall x, STspec G (pq x)) (Q : post B) i : + vrf i e1 (fun x m => + match x with + Val v => (pq v g).1 m + | Exn e => valid m -> Q (Exn e) m + end) -> + (forall v y m, (pq v g).2 y m -> valid m -> Q y m) -> + vrf i (bnd e1 e2) Q. +Proof. +move=>H1 H2; apply/vrf_bnd/vrf_post/H1=>/= y m V. +by case: y=>// y H; apply: gE H _ _ => v h; apply: H2. +Qed. + +Arguments bnd_vrf {G A B pq} g {e1 e2 Q}. + +Notation "[bnd_vrf]" := (bnd_vrf tt) (at level 0). +Notation "[ 'bnd_vrf' x1 , .. , xn ]" := + (bnd_vrf (existT _ x1 .. (existT _ xn tt) ..)) +(at level 0, format "[ 'bnd_vrf' x1 , .. , xn ]"). + + (* Common special case for framing on `Unit`, i.e. passing an *) (* empty heap to the routine. For more sophisticated framing *) (* variants see the `heapauto` module. *) diff --git a/meta.yml b/meta.yml index 63d75fc..7c13da7 100644 --- a/meta.yml +++ b/meta.yml @@ -72,7 +72,7 @@ maintainers: opam-file-maintainer: fcsl@software.imdea.org -opam-file-version: 2.0.1 +opam-file-version: 2.1.0 license: fullname: Apache-2.0 @@ -88,8 +88,8 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '2.3.0-coq-8.20' repo: 'mathcomp/mathcomp' -- version: 'latest-coq-dev' - repo: 'mathcomp/mathcomp' +- version: 'coq-dev' + repo: 'mathcomp/mathcomp-dev' dependencies: - opam: @@ -107,9 +107,9 @@ dependencies: [MathComp fingroup](https://math-comp.github.io) - opam: name: coq-fcsl-pcm - version: '{ (>= "2.0.0" & < "2.1~") | (= "dev") }' + version: '{ (>= "2.1.0" & < "2.2~") | (= "dev") }' description: |- - [FCSL-PCM 2.0](https://github.com/imdea-software/fcsl-pcm) + [FCSL-PCM 2.1](https://github.com/imdea-software/fcsl-pcm) namespace: htt