V2.1.0

.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

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):

coq-htt-core.opam

@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "[email protected]"
-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: [

coq-htt.opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 maintainer: "[email protected]"
-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}
 ]
 

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 *)

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 *)

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.                        *)

meta.yml

@@ -72,7 +72,7 @@ maintainers:
 
 opam-file-maintainer: [email protected]
 
-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