Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: imdea-software/htt
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: v2.0.1
Choose a base ref
...
head repository: imdea-software/htt
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: master
Choose a head ref
  • 4 commits
  • 14 files changed
  • 3 contributors

Commits on Dec 18, 2024

  1. update ssr upper bounds

    aleksnanevski committed Dec 18, 2024
    Copy the full SHA
    eae4dc4 View commit details

Commits on Dec 19, 2024

  1. Merge pull request #33 from imdea-software/fix3

    clayrat authored Dec 19, 2024
    Copy the full SHA
    ab2d6c5 View commit details

Commits on Jan 17, 2025

  1. boilerplate for enabling packaging using coq_makefile (#34)

    palmskog authored Jan 17, 2025
    Copy the full SHA
    8ff85ab View commit details
  2. V2.1.0 (#35)

    * Preparing coq-htt v2.1.0 for release
    
    * preparing coq-htt v2.1.0 for release
    
    * Preparing coq-htt v2.1.0 for release
    
    * preparing coq-htt v2.1.0 for release
    
    * preparing coq-htt v2.1.0 for release
    aleksnanevski authored Jan 17, 2025
    Copy the full SHA
    b6c4102 View commit details
Showing with 207 additions and 36 deletions.
  1. +2 −2 .github/workflows/docker-action.yml
  2. +3 −14 Makefile
  3. +99 −0 Makefile.common
  4. +3 −3 README.md
  5. +5 −4 coq-htt-core.opam
  6. +5 −4 coq-htt.opam
  7. +29 −0 examples/Make
  8. +7 −0 examples/Makefile
  9. +1 −1 examples/llist.v
  10. +1 −0 examples/quicksort.v
  11. +14 −0 htt/Make
  12. +7 −0 htt/Makefile
  13. +23 −0 htt/model.v
  14. +8 −8 meta.yml
4 changes: 2 additions & 2 deletions .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
@@ -16,8 +16,8 @@ jobs:
matrix:
image:
- 'mathcomp/mathcomp:2.2.0-coq-8.19'
- 'mathcomp/mathcomp:2.2.0-coq-8.20'
- 'mathcomp/mathcomp:latest-coq-dev'
- 'mathcomp/mathcomp:2.3.0-coq-8.20'
- 'mathcomp/mathcomp-dev:coq-dev'
fail-fast: false
steps:
- uses: actions/checkout@v4
17 changes: 3 additions & 14 deletions Makefile
Original file line number Diff line number Diff line change
@@ -1,15 +1,4 @@
all: default doc
default: Makefile.coq
make -f Makefile.coq
# -*- Makefile -*-

clean: Makefile.coq
make -f Makefile.coq clean
rm -f Makefile.coq

install: Makefile.coq
make -f Makefile.coq install

Makefile.coq: _CoqProject
coq_makefile -f _CoqProject -o Makefile.coq

.PHONY: coq clean install doc
# --------------------------------------------------------------------
include Makefile.common
99 changes: 99 additions & 0 deletions Makefile.common
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
# -*- Makefile -*-

######################################################################
# USAGE: #
# The rules this-config::, this-build::, this-distclean::, #
# 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
COQDEP?=$(COQBIN)coqdep
COQPROJECT?=_CoqProject
COQMAKEOPTIONS?=
COQMAKEFILEOPTIONS?=
V?=
VERBOSE?=V
######################################################################

# local context: -----------------------------------------------------
.PHONY: all config build clean distclean __always__
.SUFFIXES:

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)' \
| wc -l | sed 's/ *//g')

# coq version:
ifneq "$(BRANCH_coq)" "0"
COQVVV:= dev
else
COQVVV:=$(shell $(COQBIN)coqtop --print-version | cut -d" " -f1)
endif

COQV:= $(shell echo $(COQVVV) | cut -d"." -f1)
COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2)

# all: ---------------------------------------------------------------
all: config build

# Makefile.coq: ------------------------------------------------------
.PHONY: pre-makefile

Makefile.coq: pre-makefile $(COQPROJECT) Makefile
$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq

# Global config, build, clean and distclean --------------------------
config: sub-config this-config

build: sub-build this-build

clean: sub-clean this-clean

distclean: sub-distclean this-distclean

# Local config, build, clean and distclean ---------------------------
.PHONY: this-config this-build this-distclean this-clean

this-config:: __always__

this-build:: this-config Makefile.coq
+$(COQMAKE)

this-distclean:: this-clean
rm -f Makefile.coq Makefile.coq.conf Makefile.coq

this-clean:: __always__
@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi

# Install target -----------------------------------------------------
.PHONY: install

install: __always__ Makefile.coq
$(COQMAKE) install
# counting lines of Coq code -----------------------------------------
.PHONY: count

COQFILES = $(shell grep '.v$$' $(COQPROJECT))

count:
@coqwc $(COQFILES) | tail -1 | \
awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
# Additionally cleaning backup (*~) files ----------------------------
this-distclean::
rm -f $(shell find . -name '*~')

# Make in SUBDIRS ----------------------------------------------------
ifdef SUBDIRS
sub-%: __always__
@set -e; for d in $(SUBDIRS); do +$(MAKE) -C $$d $(@:sub-%=%); done
else
sub-%: __always__
@true
endif

# Make of individual .vo ---------------------------------------------
%.vo: __always__ Makefile.coq
+$(COQMAKE) $@
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
@@ -41,11 +41,11 @@ that HTT implements Separation logic as a shallow embedding in Coq.
- License: [Apache-2.0](LICENSE)
- Compatible Coq versions: Coq 8.19 to 8.20
- Additional dependencies:
- [MathComp ssreflect 2.2](https://math-comp.github.io)
- [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)
- [Dune](https://dune.build) 2.5 or later
- [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):
- [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)
9 changes: 5 additions & 4 deletions coq-htt-core.opam
Original file line number Diff line number Diff line change
@@ -3,7 +3,7 @@

opam-version: "2.0"
maintainer: "fcsl@software.imdea.org"
version: "dev"
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.3~") | (= "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: [
9 changes: 5 additions & 4 deletions coq-htt.opam
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
opam-version: "2.0"
maintainer: "fcsl@software.imdea.org"
version: "dev"
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.3~") | (= "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}
]

29 changes: 29 additions & 0 deletions examples/Make
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
-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
7 changes: 7 additions & 0 deletions examples/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
# -*- Makefile -*-

# setting variables
COQPROJECT?=Make

# Main Makefile
include ../Makefile.common
2 changes: 1 addition & 1 deletion examples/llist.v
Original file line number Diff line number Diff line change
@@ -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 *)
1 change: 1 addition & 0 deletions examples/quicksort.v
Original file line number Diff line number Diff line change
@@ -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 *)
14 changes: 14 additions & 0 deletions htt/Make
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
-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
7 changes: 7 additions & 0 deletions htt/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
# -*- Makefile -*-

# setting variables
COQPROJECT?=Make

# Main Makefile
include ../Makefile.common
23 changes: 23 additions & 0 deletions htt/model.v
Original file line number Diff line number Diff line change
@@ -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. *)
16 changes: 8 additions & 8 deletions meta.yml
Original file line number Diff line number Diff line change
@@ -72,7 +72,7 @@ maintainers:

opam-file-maintainer: fcsl@software.imdea.org

opam-file-version: dev
opam-file-version: 2.1.0

license:
fullname: Apache-2.0
@@ -86,17 +86,17 @@ supported_coq_versions:
tested_coq_opam_versions:
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.20'
repo: 'mathcomp/mathcomp'
- version: 'latest-coq-dev'
- version: '2.3.0-coq-8.20'
repo: 'mathcomp/mathcomp'
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'

dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }'
version: '{ (>= "2.2.0" & < "2.4~") | (= "dev") }'
description: |-
[MathComp ssreflect 2.2](https://math-comp.github.io)
[MathComp ssreflect 2.2-2.3](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
description: |-
@@ -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