From dbb8a3a88acd9591ffa1bdf30a5018911b731ffd Mon Sep 17 00:00:00 2001 From: Aleksandar Nanevski Date: Tue, 17 Mar 2026 17:14:19 +0100 Subject: [PATCH] Adapting to math-comp/math-comp#1545. Adding docker image 2.5.0-rocq-prover-9.1. --- .github/workflows/docker-action.yml | 1 + README.md | 9 +++++++-- coq-htt-core.opam | 6 +++--- coq-htt.opam | 4 ++-- examples/array.v | 2 +- examples/bubblesort.v | 3 +++ examples/congmath.v | 3 +++ examples/congprog.v | 3 +++ examples/hashtab.v | 3 +++ examples/kvmaps.v | 3 +++ examples/quicksort.v | 3 +++ examples/union_find.v | 3 +++ htt/domain.v | 11 +++++++---- meta.yml | 8 +++++--- 14 files changed, 47 insertions(+), 15 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index c9cc9b5..157b274 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -18,6 +18,7 @@ jobs: matrix: image: - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0' + - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1' - 'mathcomp/mathcomp-dev:rocq-prover-dev' fail-fast: false steps: diff --git a/README.md b/README.md index ce25e6d..59515d1 100644 --- a/README.md +++ b/README.md @@ -10,8 +10,6 @@ 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. @@ -130,3 +128,10 @@ The original version of HTT can be found [here](https://software.imdea.org/~alek Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski. TLCA 2011. 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) + + Marcos Grandury, Aleksandar Nanevski and Alexander Gryzlov. ICFP 2025. + + The paper on verifying graphs algorithms using PCMs and their morphism. \ No newline at end of file diff --git a/coq-htt-core.opam b/coq-htt-core.opam index 550550b..6a5ab2d 100644 --- a/coq-htt-core.opam +++ b/coq-htt-core.opam @@ -35,9 +35,9 @@ build: [make "-C" "htt" "-j%{jobs}%"] install: [make "-C" "htt" "install"] depends: [ "dune" {>= "3.6"} - "coq" { (>= "9.0" & < "9.1~") | (= "dev") } - "coq-hierarchy-builder" { (>= "1.7.0" & < "1.10~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") } + "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") } diff --git a/coq-htt.opam b/coq-htt.opam index 34f4c55..5033cae 100644 --- a/coq-htt.opam +++ b/coq-htt.opam @@ -32,8 +32,8 @@ build: [make "-C" "examples" "-j%{jobs}%"] install: [make "-C" "examples" "install"] depends: [ "dune" {>= "3.6"} - "coq" { (>= "9.0" & < "9.1~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") } + "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") } diff --git a/examples/array.v b/examples/array.v index 2eef1df..3235aed 100644 --- a/examples/array.v +++ b/examples/array.v @@ -27,7 +27,7 @@ From htt Require Import options model heapauto. Record array (I : finType) (T : Type) : Set := Array {orig :> ptr}. Arguments Array {I T}. -Definition array_for (I : finType) (T : Type) of phant (I -> T) := array I T. +Definition array_for (I : finType) (T : Type) & phant (I -> T) := array I T. Identity Coercion array_for_array : array_for >-> array. Notation "{ 'array' aT }" := (array_for (Phant aT)) (at level 0, format "{ 'array' '[hv' aT ']' }") : type_scope. diff --git a/examples/bubblesort.v b/examples/bubblesort.v index 205d72b..751be67 100644 --- a/examples/bubblesort.v +++ b/examples/bubblesort.v @@ -22,6 +22,9 @@ 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. *) diff --git a/examples/congmath.v b/examples/congmath.v index 76124cf..329a197 100644 --- a/examples/congmath.v +++ b/examples/congmath.v @@ -16,6 +16,9 @@ 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. +(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *) +Set SsrOldRewriteGoalsOrder. + (**********************) (* Congruence closure *) (**********************) diff --git a/examples/congprog.v b/examples/congprog.v index 31f0328..7731441 100644 --- a/examples/congprog.v +++ b/examples/congprog.v @@ -19,6 +19,9 @@ From pcm Require Import unionmap heap autopcm automap. From htt Require Import options model heapauto llist array. From htt Require Import kvmaps hashtab congmath. +(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *) +Set SsrOldRewriteGoalsOrder. + (***********************************) (* Congruence closure verification *) (***********************************) diff --git a/examples/hashtab.v b/examples/hashtab.v index 9830206..a3b6448 100644 --- a/examples/hashtab.v +++ b/examples/hashtab.v @@ -19,6 +19,9 @@ From pcm Require Import pcm unionmap heap autopcm. From htt Require Import options model heapauto. From htt Require Import array kvmaps. +(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *) +Set SsrOldRewriteGoalsOrder. + (* hash table is array of buckets, i.e. KV maps *) (* bucket indices are provided by the hash function *) (* using dynaming kv-maps for buckets *) diff --git a/examples/kvmaps.v b/examples/kvmaps.v index 859b51b..384e6c3 100644 --- a/examples/kvmaps.v +++ b/examples/kvmaps.v @@ -22,6 +22,9 @@ From pcm Require Import options axioms pred ordtype finmap seqext. From pcm Require Import pcm unionmap heap autopcm automap. From htt Require Import options model heapauto. +(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *) +Set SsrOldRewriteGoalsOrder. + (* Dynamic KV map is determined by its root pointer(s). *) (* Functions such insert and remove may modify *) (* the root, and will correspondingly return the new one. *) diff --git a/examples/quicksort.v b/examples/quicksort.v index 06bd998..b07be05 100644 --- a/examples/quicksort.v +++ b/examples/quicksort.v @@ -21,6 +21,9 @@ 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 quickorting *) (* There is some overlap with mathematics developed for bubblesort *) (* but the development is repeated here to make the files *) diff --git a/examples/union_find.v b/examples/union_find.v index 27041ea..9626df3 100644 --- a/examples/union_find.v +++ b/examples/union_find.v @@ -17,6 +17,9 @@ From pcm Require Import options axioms pred seqext. From pcm Require Import prelude pcm unionmap natmap heap autopcm automap. From htt Require Import options model heapauto tree. +(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *) +Set SsrOldRewriteGoalsOrder. + (**************) (**************) (* Union-find *) diff --git a/htt/domain.v b/htt/domain.v index 700fca5..78338b7 100644 --- a/htt/domain.v +++ b/htt/domain.v @@ -16,6 +16,9 @@ From Stdlib Require Import ssreflect ssrbool ssrfun. From mathcomp Require Import ssrnat eqtype. From pcm Require Import options axioms pred prelude. +(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *) +Set SsrOldRewriteGoalsOrder. + (**************************************************) (* This file develops some basic domain theory of *) (* posets, complete lattices, complete partial *) @@ -208,7 +211,7 @@ Definition lattice_axiom (T : poset) (sup : Pred T -> T) := forall (s : Pred T) x, (forall y, y \In s -> y <== x) -> sup s <== x]. -HB.mixin Record isLattice T of Poset T := { +HB.mixin Record isLattice T & Poset T := { sup : Pred T -> T; lattice_subproof : lattice_axiom sup}. @@ -602,7 +605,7 @@ Definition cpo_axiom (T : poset) (bot : T) (lim : chain T -> T) := forall (s : chain T) x, (forall y, y \In s -> y <== x) -> lim s <== x]. -HB.mixin Record isCPO T of Poset T := { +HB.mixin Record isCPO T & Poset T := { bot : T; lim_op : chain T -> T; cpo_subproof: cpo_axiom bot lim_op}. @@ -610,7 +613,7 @@ HB.mixin Record isCPO T of Poset T := { #[short(type="cpo")] HB.structure Definition CPO := {T of Poset T & isCPO T}. -Definition limx (D : cpo) (s : chain D) of phantom (Pred _) s := lim_op s. +Definition limx (D : cpo) (s : chain D) & phantom (Pred _) s := lim_op s. Notation lim s := (limx (Phantom (Pred _) s)). Section Repack. @@ -854,7 +857,7 @@ Definition contfun_axiom (D1 D2 : cpo) (f : mono_fun D1 D2) := forall s : chain D1, f (lim s) <== lim (Image f s). HB.mixin Record isContFun (D1 D2 : cpo) (f : D1 -> D2) - of @MonoFun D1 D2 f := {contfun_subproof : contfun_axiom f}. + & @MonoFun D1 D2 f := {contfun_subproof : contfun_axiom f}. #[short(type="cont_fun")] HB.structure Definition ContFun (D1 D2 : cpo) := diff --git a/meta.yml b/meta.yml index 7c5b946..a069912 100644 --- a/meta.yml +++ b/meta.yml @@ -81,11 +81,13 @@ license: supported_coq_versions: text: 9.0 or later - opam: '{ (>= "9.0" & < "9.1~") | (= "dev") }' + opam: '{ (>= "9.0" & < "9.2~") | (= "dev") }' tested_coq_opam_versions: - version: '2.4.0-rocq-prover-9.0' repo: 'mathcomp/mathcomp' +- version: '2.5.0-rocq-prover-9.1' + repo: 'mathcomp/mathcomp' - version: 'rocq-prover-dev' repo: 'mathcomp/mathcomp-dev' @@ -93,12 +95,12 @@ tested_coq_opam_versions: dependencies: - opam: name: coq-hierarchy-builder - version: '{ (>= "1.7.0" & < "1.10~") | (= "dev") }' + version: '{ (>= "1.7.0" & < "1.11~") | (= "dev") }' description: |- [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder) - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "2.4.0" & < "2.5~") | (= "dev") }' + version: '{ (>= "2.4.0" & < "2.6~") | (= "dev") }' description: |- [MathComp ssreflect 2.4 or later](https://math-comp.github.io) - opam: