preparing V2.3.0

.github/workflows/docker-action.yml

@@ -9,6 +9,7 @@ on:
   pull_request:
     branches:
       - '**'
+  workflow_dispatch:
 
 jobs:
   build:
@@ -17,8 +18,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
-          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
+          - 'mathcomp/mathcomp:2.6.0-rocq-prover-9.2'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:

Makefile.common

@@ -6,8 +6,8 @@
 # pre-makefile::, this-clean:: and __always__:: may be extended      #
 # Additionally, the following variables may be customized:           #
 SUBDIRS?=
-COQBIN?=$(dir $(shell which coqtop))
-COQMAKEFILE?=$(COQBIN)coq_makefile
+COQBIN?=$(dir $(shell which rocq))
+COQMAKEFILE?=$(COQBIN)rocq makefile
 COQDEP?=$(COQBIN)coqdep
 COQPROJECT?=_CoqProject
 COQMAKEOPTIONS?=
@@ -23,14 +23,14 @@ VERBOSE?=V
 H:= $(if $(VERBOSE),,@)  # not used yet
 TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
 COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
-BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
+BRANCH_coq:= $(shell $(COQBIN)rocq top -v | head -1 | grep -E '(trunk|master)' \
 	      | wc -l | sed 's/ *//g')
 
 # coq version:
 ifneq "$(BRANCH_coq)" "0"
 COQVVV:= dev
 else
-COQVVV:=$(shell $(COQBIN)coqtop --print-version | cut -d" " -f1)
+COQVVV:=$(shell $(COQBIN)rocq top --print-version | cut -d" " -f1)
 endif
 
 COQV:= $(shell echo $(COQVVV) | cut -d"." -f1)

README.md

@@ -10,6 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [docker-action-link]: https://github.com/imdea-software/htt/actions/workflows/docker-action.yml
 
 
+
+
 Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating
 programs based on Separation logic.
 
@@ -27,7 +29,7 @@ sequential composition, and the type for monadic unit combines the Hoare rules f
 program (in a small-footprint variant) and for variable assignment (adapted for functional
 variables). The connection reconciles dependent types with effects of state and exceptions 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.
+that HTT implements Separation logic as a shallow embedding in Rocq.
 
 ## Meta
 
@@ -37,15 +39,17 @@ that HTT implements Separation logic as a shallow embedding in Coq.
   - Alexander Gryzlov
   - Marcos Grandury
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: 9.0 or later
+- Compatible Rocq/Coq versions: 9.2
 - Additional dependencies:
+  - Rocq Core compiler engine
+  - Rocq Standard Library components
+  - [MathComp ssreflect 2.6 or later](https://math-comp.github.io)
   - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
-  - [MathComp ssreflect 2.4 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
-  - [FCSL-PCM 2.2](https://github.com/imdea-software/fcsl-pcm)
+  - [FCSL-PCM 2.3 or later](https://github.com/imdea-software/fcsl-pcm)
   - [Dune](https://dune.build) 3.6 or later
-- Coq namespace: `htt`
+- Rocq/Coq namespace: `htt`
 - Related publication(s):
   - [Structuring the verification of heap-manipulating programs](https://software.imdea.org/~aleks/papers/reflect/reflect.pdf) doi:[10.1145/1706299.1706331](https://doi.org/10.1145/1706299.1706331)
 
@@ -129,9 +133,9 @@ The original version of HTT can be found [here](https://software.imdea.org/~alek
 
   A semantic model for HTT, with large sigma types.
 
-* [Verifying Graph Algorithms in Separation Logic: A Case for an
-  Algebraic Approach](https://software.imdea.org/~aleks/icfp25/paper-sub.pdf)
+* [Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach](https://software.imdea.org/~aleks/icfp25/paper-sub.pdf)
 
   Marcos Grandury, Aleksandar Nanevski and Alexander Gryzlov. ICFP 2025.
 
-  The paper on verifying graphs algorithms using PCMs and their morphism.
+  Development of PCM of graphs and their morphisms. 
+  Concise verification of Schorr-Waite graph algorith, and union-find datastructure.

_CoqProject

@@ -4,17 +4,14 @@
 
 -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 
+-arg -w -arg -HB.no-new-instance
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -register-all
 
 htt/options.v
 htt/domain.v
 htt/model.v
 htt/heapauto.v
-examples/exploit.v
 examples/gcd.v
 examples/counter.v
 examples/llist.v
@@ -32,4 +29,7 @@ examples/quicksort.v
 examples/congmath.v
 examples/congprog.v
 examples/tree.v	
+examples/graph.v
+examples/schorr.v
 examples/union_find.v
+

coq-htt-core.opam

@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "fcsl@software.imdea.org"
-version: "2.2.0"
+version: "2.3.0"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -29,18 +29,19 @@ sequential composition, and the type for monadic unit combines the Hoare rules f
 program (in a small-footprint variant) and for variable assignment (adapted for functional
 variables). The connection reconciles dependent types with effects of state and exceptions 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."""
+that HTT implements Separation logic as a shallow embedding in Rocq."""
 
 build: [make "-C" "htt" "-j%{jobs}%"]
 install: [make "-C" "htt" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
-  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
-  "coq-mathcomp-algebra" 
-  "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }
+  "rocq-core" { (>= "9.2" & < "9.3~") | (= "dev") }
+  "rocq-stdlib" 
+  "rocq-mathcomp-ssreflect" { (>= "2.6.0" & < "2.7~") | (= "dev") }
+  "rocq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
+  "rocq-mathcomp-algebra" 
+  "rocq-mathcomp-fingroup" 
+  "coq-fcsl-pcm" { (>= "2.3.0" & < "2.4~") | (= "dev") }
 ]
 
 tags: [

coq-htt.opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 maintainer: "fcsl@software.imdea.org"
-version: "2.2.0"
+version: "2.3.0"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -26,17 +26,19 @@ sequential composition, and the type for monadic unit combines the Hoare rules f
 program (in a small-footprint variant) and for variable assignment (adapted for functional
 variables). The connection reconciles dependent types with effects of state and exceptions 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."""
+that HTT implements Separation logic as a shallow embedding in Rcoq."""
 
 build: [make "-C" "examples" "-j%{jobs}%"]
 install: [make "-C" "examples" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
-  "coq-mathcomp-algebra" 
-  "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }
+  "rocq-core" { (>= "9.2" & < "9.3~") | (= "dev") }
+  "rocq-stdlib"
+  "rocq-mathcomp-ssreflect" { (>= "2.6.0" & < "2.7~") | (= "dev") }
+  "rocq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
+  "rocq-mathcomp-algebra" 
+  "rocq-mathcomp-fingroup" 
+  "coq-fcsl-pcm" { (>= "2.3.0" & < "2.4~") | (= "dev") }
   "coq-htt-core" {= version}
 ]
 

examples/Make

@@ -2,13 +2,10 @@
 
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
+-arg -w -arg -HB.no-new-instance
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -register-all
 
-# 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
@@ -26,4 +23,6 @@ quicksort.v
 congmath.v
 congprog.v
 tree.v	
+graph.v
+schorr.v
 union_find.v

examples/array.v

@@ -63,7 +63,7 @@ End ArraySig.
 Module Array : ArraySig.
 Section Array.
 Context {I : finType} {T : Type}.
-Notation array := {array I -> T}.
+Abbreviation array := {array I -> T}.
 
 (* array is specified by finite function *)
 Definition shape (a : array) (f : {ffun I -> T}) : Pred heap :=

examples/bubblesort.v

@@ -22,9 +22,6 @@ Import Order.NatOrder Order.TTheory.
 Local Open Scope order_scope.
 Local Open Scope nat_scope.
 
-(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
-Set SsrOldRewriteGoalsOrder.  
-
 (* Brief mathematics of (bubble) array sorting: *)
 (* Theory of permutations built out of (adjacent-element) swaps acting on *)
 (* finite functions from bounded nats to ordered values. *)
@@ -128,7 +125,7 @@ Lemma codom1_ax_rcons2 (f : {ffun 'I_n.+1 -> A}) (a : itv_bound nat) (i : 'I_n)
         rcons (rcons (&:(fgraph f) (Interval a (BLeft (i : nat)))) 
               (f (Wo i))) (f (So i)).
 Proof.
-move=>H; rewrite slice_xR; last first.
+move=>H; rewrite slice_xR.
 - by apply: ltW; case: a H=>[[] ax|ab] //; rewrite !bnd_simp ltEnat /= =>/ltnW.
 by rewrite onth_codom1S /= slice_oSR codom1_ax_rcons.
 Qed.
@@ -194,7 +191,7 @@ Proof.
 move=>Hx0 Hx1.
 suff E: {in &:(enum 'I_n.+1) i, f =1 pffun (swnx x) f}.
 - by rewrite !fgraph_codom /= !codomE /= -2!slice_map /=; move/eq_in_map: E.
-move=>/= y; rewrite slice_uniq_memE /=; last by exact: enum_uniq.
+move=>/= y; rewrite slice_uniq_memE /=; first by exact: enum_uniq.
 case: i Hx0 Hx1=>i j Hx0 Hx1 /=.
 case/and3P=>_; rewrite /swnx size_enum_ord index_enum_ord =>Hy1 Hy2.
 rewrite ffunE; case: tpermP=>// Ey; move: Hy1 Hy2; rewrite {y}Ey /=.
@@ -282,7 +279,7 @@ Proof.
 move=>H; move: (perm_swnx f i).
 set f' : {ffun 'I_n.+1 -> A} := pffun (swnx i) f.
 rewrite {1}(slice_uxou (fgraph f) k.+1) {1}(slice_uxou (fgraph f') k.+1).
-by rewrite swnx_oa /=; [rewrite perm_cat2r | rewrite ltnS].
+by rewrite swnx_oa /=; [rewrite ltnS|rewrite perm_cat2r].
 Qed.
 End SwapNextEq.
 
@@ -728,13 +725,13 @@ apply: [stepE f]=>//= sw m [p][Hm Hsw]; case: decP=>H.
   - rewrite Sbo_eq.
     case: sw Hsw=>/=; case=>Ep Hf; rewrite {p}Ep ?pffunE1 in Hm *.
     (* swap happened before the call *)
-    - rewrite So_eq swnx_oa; last by rewrite ltnS; apply: ltnW.
+    - rewrite So_eq swnx_oa; first by rewrite ltnS; apply: ltnW.
       rewrite swnx_Skk /=; split=>//.
       - rewrite (@allrel_in_l _ _ _ _ &:(codom f) `]-oo, k.+1]) //.
         by apply/perm_mem; rewrite perm_sym; apply: perm_swnx_ux.
       - by rewrite ltnS leqnn.
-      rewrite allrel1r slice_oSR (slice_split (x:=ls) _ true); 
-        last by rewrite in_itv.
+      rewrite allrel1r slice_oSR (slice_split (x:=ls) _ true).
+      - by rewrite in_itv.
       rewrite /= all_cat; apply/andP; split.
       - rewrite swnx_ao //; move: Hai.
         by rewrite codom1_ax_rcons // allrel_rconsr; case/andP.
@@ -777,13 +774,13 @@ step=>Vm; exists p; case: sw Hsw=>/=; case=>Ep Hf.
     move: Hsi; rewrite codom1_ax_rcons // sorted_rconsE //=. 
     case/andP => Halsi _.
     move: Hils; rewrite leq_eqVlt; case/orP=>[/eqP <-|Hlsi] //.
-    rewrite (slice_split (x:=ls) _ true); last by rewrite in_itv.
+    rewrite (slice_split (x:=ls) _ true); first by rewrite in_itv.
     by rewrite /= all_cat Hals.
   rewrite Ep swnx_xu_cons /= (path_sortedE (@otrans A)) Hsk andbT.
   by move: Hak; rewrite codom1_ax_rcons2 // !allrel_rconsl -!andbA; case/and3P.
 (* swap didn't happen on last iteration *)
 rewrite {p}Ep pffunE1 /= in Hm *.
-rewrite (slice_split (x:=i) (i:=`[ls:nat, +oo[) _ false); last first. 
+rewrite (slice_split (x:=i) (i:=`[ls:nat, +oo[) _ false).
 - by rewrite in_itv /= andbT.
 split=>//=.
 - rewrite allrel_catr Hai /= -slice_oSL codom1_xu_cons allrel_consr.
@@ -860,7 +857,7 @@ Qed.
 Next Obligation.
 move=>a [f][] h /= E.
 apply: [gE f]=>//=.
-rewrite (@itv_overL _ _ _ +oo) /=; first by split=>//; exact: allrel0r.
+rewrite (@itv_overL _ _ _ +oo) /=; last by split=>//; exact: allrel0r.
 by rewrite leEnat addn1 size_codom /= card_ord.
 Qed.