...
 
Commits (52)
Arthur Charguéraud
with contributions from:
François Pottier
Armaël Guéneau
# -------------------------------------------------------------------------
# Private Makefile for package maintenance.
SHELL := bash
export CDPATH=
.PHONY: package export opam submit pin unpin
# -------------------------------------------------------------------------
include Makefile
# -------------------------------------------------------------------------
# Distribution.
# The version number is automatically set to the current date,
# unless DATE is defined on the command line.
DATE := $(shell /bin/date +%Y%m%d)
# The project name on gitlab.
PROJECT := cfml
# The opam package name.
PACKAGE := coq-$(PROJECT)
# The repository URL (https).
REPO := https://gitlab.inria.fr/charguer/$(PROJECT)
# The archive URL (https).
ARCHIVE := $(REPO)/repository/$(DATE)/archive.tar.gz
# The local repository directory.
PWD := $(shell pwd)
# -------------------------------------------------------------------------
# Prepare a release.
package:
# Make sure the correct version can be installed.
@ make reinstall
# -------------------------------------------------------------------------
# Publish a release. (Remember to commit everything first!)
export:
# Check if everything has been committed.
@ if [ -n "$$(git status --porcelain)" ] ; then \
echo "Error: there remain uncommitted changes." ; \
git status ; \
exit 1 ; \
else \
echo "Now making a release..." ; \
fi
# Create a git tag.
@ git tag -a $(DATE) -m "Release $(DATE)."
# Upload. (This automatically makes a .tar.gz archive available on gitlab.)
@ git push
@ git push --tags
# -------------------------------------------------------------------------
# Updating the opam package.
# This entry assumes that "make package" and "make export"
# have just been run (on the same day).
# You need opam-publish:
# sudo apt-get install libssl-dev
# opam install tls opam-publish
# In fact, you need a version of opam-publish that supports --subdirectory:
# git clone git@github.com:fpottier/opam-publish.git
# cd opam-publish
# git checkout 1.3
# opam pin add opam-publish `pwd` -k git
# The following command should have been run once:
# opam-publish repo add opam-coq-archive coq/opam-coq-archive
PUBLISH_OPTIONS := \
--repo opam-coq-archive \
--subdirectory released \
opam:
@ opam lint
@ opam-publish prepare $(PUBLISH_OPTIONS) $(PACKAGE).$(DATE) $(ARCHIVE)
submit:
@ opam-publish submit $(PUBLISH_OPTIONS) $(PACKAGE).$(DATE)
# -------------------------------------------------------------------------
# Pinning.
pin:
opam pin add $(PACKAGE) `pwd` -k git
unpin:
opam pin remove $(PACKAGE)
MIT X11 LICENSE
---------------
Copyright (c) 2018 Arthur Charguéraud
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
Except as contained in this notice, the name of the copyright holders shall not
be used in advertising or otherwise to promote the sale, use or other dealings
in this Software without prior written authorization from the copyright holders.
\ No newline at end of file
......@@ -15,6 +15,9 @@ PREFIX ?= $(DEFAULT_PREFIX)
BINDIR ?= $(PREFIX)/bin
LIBDIR ?= $(PREFIX)/lib/cfml
COQ_WHERE ?= $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib
##############################################################################
# Targets.
......@@ -26,9 +29,7 @@ coqlib:
generator:
rm -f generator/cfml_config.ml
sed -e 's|@@PREFIX@@|$(PREFIX)|' \
-e 's|@@BINDIR@@|$(BINDIR)|' \
-e 's|@@LIBDIR@@|$(LIBDIR)|' \
sed -e 's|@@LIBDIR@@|$(LIBDIR)|' \
generator/cfml_config.ml.in > generator/cfml_config.ml
$(MAKE) -C generator
......@@ -58,13 +59,6 @@ clean:
##############################################################################
# Installation.
# If ARTHUR is defined, create a symbolic link from Coq's user-contrib
# directory to this directory (cfml). Otherwise, perform a copy.
# TEMPORARY, this is TODO
COQ_WHERE := $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib
# As install depends on all, the file generator/cfml_config.ml is regenerated
# when `make install` is run; this ensures LIBDIR cannot be inconsistent.
......@@ -102,7 +96,7 @@ uninstall:
rm -f $(BINDIR)/cfmlc
# rm -f $(BINDIR)/cfml_cmj
rm -rf $(LIBDIR)
rm -rf $(DOCDIR)
# rm -rf $(DOCDIR)
rm -rf $(COQ_CONTRIB)/CFML
reinstall: uninstall
......
# CFML : a characteristic formula generator for OCaml
# CFML : a tool for proving OCaml programs in Separation Logic
Description
===========
CFML is a tool for carrying out proofs of correctness of OCaml programs with
respect to specifications expressed in higher-order Separation Logic.
CFML consists of two parts:
- a tool, implemented in OCaml, which parses OCaml source code
and generates Coq files containing characteristic formulae;
- a Coq library, which exports definitions, lemmas and tactics
used to manipulate characteristic formulae.
Status:
- The current version of CFML is known to work with Coq 8.6
- a tool, implemented in OCaml, parses OCaml source code and generates Coq
files that contain characteristic formulae, that is, logical descriptions
of the behavior of the OCaml code.
- a Coq library exports definitions, lemmas, and tactics that are used
to reason inside Coq about the code. In short, these tactics allow
the reasoning rules of Separation Logic to be applied to the OCaml code.
Compilation
Installation
============
The recommended way is by using `opam` to pin the repository:
The current version of CFML requires Coq 8.6 or newer.
opam pin add coq-cfml https://gitlab.inria.fr/charguer/cfml
The simplest way of installing the *latest released version* of CFML is via `opam`.
Note that you will need in particular a working installation
of [TLC](https://gitlab.inria.fr/charguer/tlc/).
```sh
# This only needs to be done once, to add the opam repository with coq packages
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-cfml
```
If instead you wish to use *the development version* of CFML,
then the last line above should be replaced by the following:
```sh
opam pin add coq-cfml https://gitlab.inria.fr/charguer/cfml.git
```
Getting started
============
......@@ -35,7 +50,7 @@ make
coqide Tuto_proof.v
```
- Use [cfml-skeleton](https://gitlab.inria.fr/agueneau/cfml-skeleton) to setup a
- Use [cfml-skeleton](https://gitlab.inria.fr/agueneau/cfml-skeleton) to set up a
new project that uses CFML.
Documentation
......
Set Implicit Arguments.
Require Export LibInt FuncDefs FuncPrint.
Require Export LibInt FuncDefs FuncPrint.
Hint Resolve (0%nat) : typeclass_instances.
Hint Resolve (0%Z) : typeclass_instances.
......
......@@ -27,10 +27,10 @@ struct
let bucket h k =
(H.hash k) mod (Array.length h)
let create n =
Array.create n []
let create n =
Array.make n []
let rem h k =
let rem h k =
let b = bucket h k in
h.(b) <- List.filter (fun (k',_) -> not (H.equal k k')) h.(b)
......@@ -42,7 +42,7 @@ struct
let b = bucket h k in
snd (List.find (fun (k',_) -> H.equal k k') h.(b))
let add h k x =
let add h k x =
if not (mem h k) then begin
let b = bucket h k in
h.(b) <- (k,x)::h.(b)
......
(** Representation of fixed-size circular buffers. *)
module Make (Capa : CapacitySig.S) (Item : InhabType.S) =
module Make (Capa : CapacitySig.S) (Item : InhabType.S) =
struct
(*--------------------------------------------------------------------------*)
......@@ -24,7 +23,7 @@ type t = {
(** Builds a new queue *)
let create () =
let create () =
{ head = 0;
size = 0;
data = Array.make capacity Item.inhab; }
......@@ -59,15 +58,15 @@ let wrap_down i =
(** Pop an element from the front (assumes non-empty queue) *)
let pop_front q =
let pop_front q =
let x = Array.get q.data q.head in
q.head <- wrap_up (q.head + 1);
q.size <- q.size - 1;
x
(** Pop an element from the back (assumes non-empty queue) *)
let pop_back q =
let pop_back q =
q.size <- q.size - 1;
let i = wrap_up (q.head + q.size) in
Array.get q.data i
......@@ -92,12 +91,12 @@ let push_back x q =
let debug = false
(** Internal: copy n elements from an array t1 of size capacity,
starting at index i1 and possibly wrapping around, into an
starting at index i1 and possibly wrapping around, into an
array t2 starting at index i2 and not wrapping around. *)
let copy_data_wrap_src t1 i1 t2 i2 n =
if (debug && (i1 < 0 || i1 > capacity || i2 < 0 || i2 + n > capacity || n < 0))
then failwith (Printf.sprintf "copy_data_wrap_src error: %d %d %d" i1 i2 n);
then failwith (Printf.sprintf "copy_data_wrap_src error: %d %d %d" i1 i2 n);
let j1 = i1 + n in
if j1 <= capacity then begin
Array.blit t1 i1 t2 i2 n
......@@ -107,7 +106,7 @@ let copy_data_wrap_src t1 i1 t2 i2 n =
Array.blit t1 i1 t2 i2 na;
Array.blit t1 0 t2 i2' (n - na);
end
(** Internal: copy n elements from an array t1 starting at index i1
and not wrapping around, into an array t2 of size capacity,
starting at index i2 and possibly wrapping around. *)
......@@ -126,7 +125,7 @@ let copy_data_wrap_dst t1 i1 t2 i2 n =
end
(** Internal: copy n elements from an array t1 starting at index i1
and possibly wrapping around, into an array t2 starting at index
and possibly wrapping around, into an array t2 starting at index
i2 and possibly wrapping around. Both arrays are assumed to be
of size capacity. *)
......@@ -149,7 +148,7 @@ let copy_data_wrap_src_and_dst t1 i1 t2 i2 n =
(** Transfer N items from the back of a buffer to the front of another buffer *)
let transfer_back_to_front n q1 q2 =
if n < 0 || n > q1.size || n + q2.size > capacity
if n < 0 || n > q1.size || n + q2.size > capacity
then invalid_arg "CircularArray.transfer_back_to_front";
let h1 = wrap_down (wrap_up (q1.head + q1.size) - n) in
let h2 = wrap_down (q2.head - n) in
......@@ -161,7 +160,7 @@ let transfer_back_to_front n q1 q2 =
(** Transfer N items from the front of a buffer to the back of another buffer *)
let transfer_front_to_back n q1 q2 =
if n < 0 || n > q1.size || n + q2.size > capacity
if n < 0 || n > q1.size || n + q2.size > capacity
then invalid_arg "CircularArray.transfer_front_to_back";
let h1 = q1.head in
let h2 = wrap_up (q2.head + q2.size) in
......@@ -187,8 +186,8 @@ let transfer_all_to_back q1 q2 =
(** Pop N elements from the front into an array *)
let popn_front_to_array n q =
if n < 0 || n > q.size
let popn_front_to_array n q =
if n < 0 || n > q.size
then invalid_arg "CircularArray.popn_front_to_array";
if n = 0 then [||] else begin
let h = q.head in
......@@ -201,7 +200,7 @@ let popn_front_to_array n q =
(** Pop N elements from the back into an array *)
let popn_back_to_array n q =
let popn_back_to_array n q =
if n < 0 || n > q.size then invalid_arg "CircularArray.popn_back_to_array";
if n = 0 then [||] else begin
let h = wrap_down (wrap_up (q.head + q.size) - n) in
......@@ -281,7 +280,7 @@ let to_list q =
let cell_at q i =
wrap_up (q.head + i)
let get q i =
let get q i =
q.data.(cell_at q i)
let set q i v =
......
(*************************************************************************)
(** Graph representation by adjacency lists *)
module Graph = struct
type t = (int list) array
type t = (int list) array
let nb_nodes (g:t) =
let nb_nodes (g:t) =
Array.length g
let iter_edges (f:int->unit) (g:t) (i:int) =
let iter_edges (g:t) (i:int) (f:int->unit) =
List.iter (fun j -> f j) g.(i)
end
......@@ -28,15 +23,60 @@ type color = White | Gray | Black
let rec dfs_from g c i =
c.(i) <- Gray;
Graph.iter_edges (fun j ->
if c.(j) = White
then dfs_from g c j) g i;
Graph.iter_edges g i (fun j ->
if c.(j) = White
then dfs_from g c j);
c.(i) <- Black
let dfs_main g rs =
let n = Graph.nb_nodes g in
let c = Array.make n White in
List.iter (fun i ->
List.iter (fun i ->
if c.(i) = White then
dfs_from g c i) rs;
c
(*************************************************************************)
(** Minimal stack structure *)
module Stack = struct
type 'a t = ('a list) ref
let create () : 'a t =
ref []
let is_empty (s : 'a t) =
!s = []
let pop (s : 'a t) =
match !s with
| [] -> assert false
| x::n -> s := n; x
let push (x : 'a) (s : 'a t) =
s := x::!s
end
(*************************************************************************)
(** DFS Algorithm, using two colors and a stack *)
let reachable_imperative g a b =
let n = Graph.nb_nodes g in
let c = Array.make n false in
let s = Stack.create() in
c.(a) <- true;
Stack.push a s;
while not (Stack.is_empty s) do
let i = Stack.pop s in
Graph.iter_edges g i (fun j ->
if not c.(j) then begin
c.(j) <- true;
Stack.push j s;
end);
done;
c.(b)
Set Implicit Arguments.
Require Import CFLib.
Require Import CFML.CFLib.
Require Import DFS_ml.
Require Import Stdlib.
Require Import LibListZ.
Require Import TLC.LibListZ.
Require Import Array_proof.
Require Import List_proof.
Open Scope tag_scope.
Ltac auto_star ::=
(*************************************************************************)
(* TLC BUFFER *)
Lemma remove_empty : forall A (E: set A),
E \- \{} = E.
Proof. intros. rew_set. intros. rew_set. tauto. Qed.
Lemma remove_all : forall A (E: set A),
E \- E = \{}.
Proof. intros. rew_set. intros. rew_set. tauto. Qed.
(* TODO: "rew_set*" *)
(*************************************************************************)
(** Automation *)
Ltac auto_star ::=
try solve [ subst; intuition eauto with maths ].
......@@ -21,49 +37,89 @@ Definition heap_contains H1 H2 :=
Global Instance incl_inst : BagIncl hprop.
Proof. constructor. applys heap_contains. Defined.
Lemma heap_contains_intro : forall (H H1 H2 : hprop),
Lemma heap_contains_intro : forall (H H1 H2 : hprop),
(H2 ==> H1 \* H) ->
(H1 \* H ==> H2) ->
(H1 \c H2).
Proof using. introv M1 M2. hnf. exists H. apply* pred_le_extens. Qed.
Proof using. introv M1 M2. hnf. exists H. apply* antisym_pred_incl. Qed.
Lemma heap_contains_elim : forall (H1 H2 : hprop),
Lemma heap_contains_elim : forall (H1 H2 : hprop),
(H1 \c H2) -> exists H,
(H2 ==> H1 \* H)
(H2 ==> H1 \* H)
/\ (H1 \* H ==> H2).
Proof using. introv (H&M). exists H. split*. Qed.
Global Opaque heap_contains.
Lemma No_duplicates_app_inv : forall A (L1 L2 : list A),
No_duplicates (L1 ++ L2) ->
No_duplicates L1
/\ No_duplicates L2
/\ (~ exists x, Mem x L1 /\ Mem x L2).
(* Future work:
Lemma heap_contains_intro_hexists_1 : forall A (J:A->hprop) H,
H \c (Hexists x, H \* J x).
Proof using.
intros. applys heap_contains_intro (Hexists x, J x); hsimpl.
Qed.
Lemma heap_contains_intro_hexists_2 : forall A1 A2 (J:A1->A2->hprop) H,
H \c (Hexists x y, H \* J x y).
Proof using.
intros. applys heap_contains_intro (Hexists x1 x2, J x1 x2); hsimpl.
Qed.
Lemma heap_contains_hexists : forall (H1 : hprop) A (J J2:A->hprop),
(forall x, (J x ==> H1 \* J2 x)) ->
(forall x, (H1 \* J2 x ==> J x)) -> (* or just, [forall x, J x = H1 \* J2 x] *)
(H1 \c (Hexists x, J x)).
Proof using.
introv M1 M2. hnf. exists (Hexists x, J2 x). applys antisym_pred_incl.
{ hpull ;=> x. hchanges (M1 x). }
{ hpull ;=> x. hchanges (M2 x). }
Qed.
Lemma heap_contains_hexists2 : forall (H1 : hprop) A1 A2 (J J2:A1->A2->hprop),
(forall x1 x2, (J x1 x2 ==> H1 \* J2 x1 x2)) ->
(forall x1 x2, (H1 \* J2 x1 x2 ==> J x1 x2)) -> (* or just, [forall x, J x = H1 \* J2 x] *)
(H1 \c (Hexists x1 x2, J x1 x2)).
Proof using.
introv M1 M2. hnf. exists (Hexists x1 x2, J2 x1 x2). applys antisym_pred_incl.
{ hpull ;=> x1 x2. hchanges (M1 x1 x2). }
{ hpull ;=> x1 x2. hchanges (M2 x1 x2). }
Qed.
*)
(*
Search noduplicates.
Lemma noduplicates_app_inv : forall A (L1 L2 : list A),
noduplicates (L1 ++ L2) ->
noduplicates L1
/\ noduplicates L2
/\ (~ exists x, mem x L1 /\ mem x L2).
Proof using.
introv ND. splits.
induction L1.
constructors.
rew_list in ND. inverts ND as ND1 ND2. rewrite Mem_app_or_eq in ND1. rew_logic* in ND1.
rew_list in ND. inverts ND as ND1 ND2. rewrite mem_app_or_eq in ND1. rew_logic* in ND1.
induction L1.
rew_list~ in ND.
rew_list in ND. inverts~ ND.
introv (x&I1&I2). induction I1; rew_list in ND.
inverts ND as ND1 ND2. false ND1. apply* Mem_app_or.
inverts ND as ND1 ND2. false ND1. apply* mem_app_or.
apply IHI1. inverts~ ND.
Qed.
*)
(*************************************************************************)
(** Set of list predicate : TODO: move *)
Definition set_of_list_monoid A :=
(monoid_ (union : _ -> _ -> set A) (\{}:set A)).
(monoid_make (union : _ -> _ -> set A) (\{}:set A)).
Definition set_of_list A (L : list A) :=
LibList.fold (@set_of_list_monoid A) (fun x => \{x}) L.
Section SetOfList.
Variables (A:Type).
Implicit Types l : list A.
......@@ -76,7 +132,7 @@ Proof using.
apply union_empty_r.
Qed.
Local Hint Resolve set_of_list_monoid_Monoid.
Lemma set_of_list_nil :
Lemma set_of_list_nil :
set_of_list (@nil A) = \{}.
Proof using. auto. Qed.
Lemma set_of_list_cons : forall x l,
......@@ -89,12 +145,12 @@ Lemma set_of_list_app : forall l1 l2,
set_of_list (l1 ++ l2) = (set_of_list l1) \u (set_of_list l2).
Proof using. intros. unfold set_of_list. rewrite~ fold_app. Qed.
Lemma set_of_list_Mem : forall l x,
x \in set_of_list l -> Mem x l.
Lemma set_of_list_mem : forall l x,
x \in set_of_list l -> mem x l.
Proof using.
introv. induction l; introv M.
{ false. }
{ rewrite set_of_list_cons in M. set_in M; eauto. }
{ rewrite set_of_list_cons in M. rew_set in M. destruct* M. }
Qed.
End SetOfList.
......@@ -137,7 +193,7 @@ Parameter edges_in_nodes : forall (G : graph) x y,
(** Derived definition for working with graphs *)
Definition out_edges G i :=
Definition out_edges G i :=
set_st (fun j => (i,j) \in edges G).
Definition has_edge (G:graph) x y :=
......@@ -146,7 +202,7 @@ Definition has_edge (G:graph) x y :=
Definition path := list (int*int).
Inductive is_path (G:graph) : int -> int -> path -> Prop :=
| is_path_nil : forall x,
| is_path_nil : forall x,
x \in nodes G ->
is_path G x x nil
| is_path_cons : forall x y z p,
......@@ -162,10 +218,10 @@ Definition reachable (G:graph) (i j:int) :=
(********************************************************************)
(* ** Basic well-formedness facts on graphs *)
Lemma out_edges_has_edge : forall G i j,
Lemma out_edges_has_edge : forall G i j,
j \in out_edges G i <-> has_edge G i j.
Proof using.
intros. unfold has_edge, out_edges. rewrite~ in_set_st_eq.
Proof using.
intros. unfold has_edge, out_edges. rewrite* in_set_st_eq.
Qed.
Lemma has_edge_nodes : forall (G : graph) x y,
......@@ -182,29 +238,31 @@ Lemma has_edge_in_nodes_r : forall (G : graph) x y,
has_edge G x y -> y \in nodes G. (* trivial *)
Proof using. intros. forwards*: has_edge_nodes. Qed.
Hint Resolve has_edge_in_nodes_l has_edge_in_nodes_r.
Lemma reachable_in_nodes_l : forall (G : graph) x y,
reachable G x y -> x \in nodes G.
Proof using.
=>> (p&M). destruct M. auto. applys* has_edge_in_nodes_l.
=>> (p&M). destruct M. auto. applys* has_edge_in_nodes_l.
Qed.
Lemma reachable_in_nodes_r : forall (G : graph) x y,
reachable G x y -> y \in nodes G.
Proof using. =>> (p&M). induction* M. Qed.
Lemma reachable_self : forall G i,
Lemma reachable_self : forall G i,
i \in nodes G ->
reachable G i i.
Proof using. intros. exists (nil:path). constructor~. Qed.
Proof using. intros. exists (nil:path). constructor~. Qed.
Lemma reachable_edge : forall G i j,
has_edge G i j ->
has_edge G i j ->
reachable G i j.
Proof using. (* trivial *)
=>> M. exists ((i,j)::nil). constructor~. constructor~.
applys* has_edge_in_nodes_r.
Qed.
Lemma reachable_trans : forall G i j k,
reachable G i j ->
reachable G j k ->
......@@ -213,42 +271,42 @@ Proof using. (* basic induction *)
=>> (p1&M1) (p2&M2). exists (p1++p2).
induction M1; rew_list.
{ auto. }
{ constructor~. }
{ constructor~. }
Qed.
Lemma reachable_trans_edge : forall G i j k,
reachable G i j ->
has_edge G j k ->
has_edge G j k ->
reachable G i k.
Proof using. (* trivial *)
=>> M1 M2. applys* reachable_trans. applys* reachable_edge.
=>> M1 M2. applys* reachable_trans. applys* reachable_edge.
Qed.
(********************************************************************)
(* ** Graph representation predicate in Separation Logic: [g ~> RGraph G]*)
(** [nodes_index G n] asserts that the nodes in [G] are indexed
(** [nodes_index G n] asserts that the nodes in [G] are indexed
from [0] inclusive to [n] exclusive. *)
Definition nodes_index (G:graph) (n:int) :=
n >= 0 /\ (forall i, i \in nodes G <-> index n i).
(** [nodes_edges G N] asserts that [N] describes the adjacency
(** [nodes_edges G N] asserts that [N] describes the adjacency
lists of [G], in the sense that [N[i]] gives the list of
neighbors of node [i] in [G]. *)
Definition nodes_edges (G:graph) (N:list(list int)) :=
forall i, i \in nodes G ->
forall i, i \in nodes G ->
set_of_list (N[i]) = out_edges G i
/\ No_duplicates (N[i]).
/\ noduplicates (N[i]).
(** [g ~> RGraph G] asserts that at pointer [g] is an imperative
array of pure lists that represents the adjacency lists of [G]. *)
Definition RGraph (G:graph) (g:loc) :=
Hexists N, g ~> Array N
\* \[ nodes_index G (LibListZ.length N)
\* \[ nodes_index G (LibListZ.length N)
/\ nodes_edges G N].
......@@ -256,9 +314,9 @@ Definition RGraph (G:graph) (g:loc) :=
(** Basic lemmas about [RGraph] -- TODO: will be generated *)
Lemma RGraph_open : forall (g:loc) (G:graph),
g ~> RGraph G ==>
g ~> RGraph G ==>
Hexists N, g ~> Array N
\* \[nodes_index G (LibListZ.length N)
\* \[nodes_index G (LibListZ.length N)
/\ nodes_edges G N].
Proof using. intros. xunfolds~ RGraph. Qed.
......@@ -266,15 +324,15 @@ Lemma RGraph_close : forall (g:loc) (G:graph) N,
nodes_index G (LibListZ.length N) ->
nodes_edges G N ->
g ~> Array N
==>
==>
g ~> RGraph G.
Proof using. intros. xunfolds~ RGraph. Qed.
Implicit Arguments RGraph_close [].
Arguments RGraph_close : clear implicits.
Hint Extern 1 (RegisterOpen (RGraph _)) =>
Hint Extern 1 (RegisterOpen (RGraph _)) =>
Provide RGraph_open.
Hint Extern 1 (RegisterClose (Array _)) =>
Hint Extern 1 (RegisterClose (Array _)) =>
Provide RGraph_close.
......@@ -291,25 +349,33 @@ Implicit Types R E F : set int.
(** Hints for indices *)
Lemma nodes_index_index : forall G n m x,
nodes_index G n -> x \in nodes G -> n = m -> index m x.
Proof. introv (E&N) Nx L. subst. rewrite~ <- N. Qed.
Hint Extern 1 (index ?n ?x) => skip.
(* TODO: for now, we skip these trivial goals
about indices being in the bounds of the array *)
(* Hints for solving [index n x] goals automatically
Hint Resolve @index_array_length_eq @index_make @index_update.
Hint Immediate has_edge_in_nodes_l has_edge_in_nodes_r.
Hint Extern 1 (nodes_index _ _) => congruence.
Hint Extern 1 (index ?n ?x) =>
eapply nodes_index_index;
[ try eassumption
| instantiate; try eassumption
| instantiate; try congruence ].
*)
Lemma nodes_index_index : forall G n x,
nodes_index G n -> x \in nodes G -> index n x.
Proof. introv (E&N) Nx. subst. rewrite~ <- N. Qed.
Lemma nodes_index_length_index : forall A G (L: list A) x,
nodes_index G (length L) -> x \in nodes G -> index L x.
Proof. introv (E&N) Nx. subst. apply index_of_index_length. rewrite~ <- N. Qed.
Lemma index_same_length_eq : forall A (L1 L2: list A) x,
length L1 = length L2 ->
index L1 x = index L2 x.
Proof.
introv HL. rewrite !index_eq_index_length, HL. auto.
Qed.
Lemma index_same_length : forall A (L1 L2: list A) x,
length L1 = length L2 ->
index L1 x ->
index L2 x.
Proof.
introv HL I. rewrite !index_eq_index_length, HL in *. auto.
Qed.
Hint Resolve
index_update index_make
index_same_length
nodes_index_index nodes_index_length_index.
(*************************************************************************)
......@@ -317,9 +383,9 @@ Hint Extern 1 (index ?n ?x) =>
Lemma nb_nodes_spec : forall (G:graph) g,
app Graph_ml.nb_nodes [g]
PRE (g ~> RGraph G)
PRE (g ~> RGraph G)
POST (fun n => g ~> RGraph G \* \[nodes_index G n]).
Proof using.
Proof using.
xcf. xunfold RGraph. xpull ;=> N (HN1&HN2).
xapp. xsimpl*.
Qed.
......@@ -329,52 +395,77 @@ Hint Extern 1 (RegisterSpec Graph_ml.nb_nodes) => Provide nb_nodes_spec.
Lemma iter_edges_spec : forall (I:set int->hprop) (G:graph) g f i,
i \in nodes G ->
(forall L, (g ~> RGraph G) \c (I L)) ->
(forall j E, j \notin E -> has_edge G i j ->
(app f [j] (I E) (# I (\{j} \u E)))) ->
app Graph_ml.iter_edges [f g i]
PRE (I \{})
(forall j E, j \notin E -> has_edge G i j ->
(app f [j] (I E) (# I (\{j} \u E)))) ->
app Graph_ml.iter_edges [g i f]
PRE (I \{})
POST (# I (out_edges G i)).
Proof.
introv Gi Ginc Sf. xcf.
forwards (H&HO&HC): heap_contains_elim ((rm Ginc) \{}).
xchange (rm HO). xopen g. xpull ;=> N (GI&GN).
forwards (GNE&GND): GN Gi. xapps~. xclose* g. xchange (rm HC).
forwards (GNE&GND): GN Gi. xapps~.
(* unfold nodes_index in *. unpack. apply index_of_index_length. rewrite <-H1. *)
skip.
xclose* g. xchange (rm HC).
xfun. xapp_no_simpl (fun (L:list int) => I (set_of_list L)).
{ introv EN. rewrite set_of_list_last. xapp. xapp.
{ introv EN. rewrite set_of_list_last. xapp.
xapp_spec Sf. (* TODO: xapp *)
{ intros M. rewrite EN in GND. (* trivial *)
lets (_&_&N3): No_duplicates_app_inv GND. applys (rm N3). (* trivial *)
exists x. forwards*: set_of_list_Mem M. } (* trivial *)
lets (_&_&N3): noduplicates_app_inv GND. applys (rm N3). (* trivial *)
exists x. forwards*: set_of_list_mem M. } (* trivial *)
{ rewrite <- out_edges_has_edge. rewrite <- GNE. rewrite EN. (* trivial *)
rew_set_of_list. eauto. } (* trivial *)
{ xsimpl. }
rew_set_of_list. rew_set; eauto. } (* trivial *)
{ rewrite union_comm. xsimpl. } }
{ rew_set_of_list. xsimpl. }
{ rewrite GNE. xsimpl. }
Qed.
Qed.
Hint Extern 1 (RegisterSpec Graph_ml.iter_edges) => Provide iter_edges_spec.
Lemma iter_edges_remaining_spec : forall (I:set int->hprop) (G:graph) g f i,
i \in nodes G ->
(forall L, (g ~> RGraph G) \c (I L)) ->
(forall j E, j \notin E -> has_edge G i j ->
(app f [j] (I (E \u \{j})) (# I E))) ->
app Graph_ml.iter_edges [g i f]
PRE (I (out_edges G i))
POST (# I \{}).
Proof.
intros. xapp_spec~ iter_edges_spec (>> (fun E => I (out_edges G i \- E)) G).
{ introv Hj Hij. xapp~.
{ intro HH. rew_set in HH. tauto. }
{ hsimpl. match goal with |- I ?x ==> I ?y \* _ => asserts_rewrite (x = y) end.
{ rew_set. intro x. rew_set. rew_logic. iff; unpack.
{ tests~: (x = j). }
{ tests~: (x = j). branches; [| now false]. tauto. } }
hsimpl. } }
{ rewrite remove_empty. hsimpl. }
{ rewrite remove_all. hsimpl. }
Qed.
(********************************************************************)
(* ** Auxiliary definitions for the invariants of DFS *)
Definition evolution C C' :=
(forall i, index C i -> C[i] = Black -> C'[i] = Black)
length C = length C'
/\ (forall i, index C i -> C[i] = Black -> C'[i] = Black)
/\ (forall i, index C i -> (C[i] = Gray <-> C'[i] = Gray)).
Definition no_white_in E C :=
forall i, i \in E -> C[i] <> White.
forall i, i \in E -> index C i /\ C[i] <> White.
Definition all_black_in E C :=
forall i, i \in E -> C[i] = Black.
forall i, i \in E -> index C i /\ C[i] = Black.
Definition no_gray C :=
forall i, index C i -> C[i] <> Gray.
Definition no_black_to_white G C :=
forall i j,
has_edge G i j ->
Definition no_black_to_white G C :=
forall i j,
has_edge G i j ->
C[i] = Black ->
C[j] <> White.
......@@ -385,12 +476,12 @@ Definition inv G R C :=
(nodes_index G (length C))
/\ (no_black_to_white G C)
/\ (forall j, j \in nodes G -> C[j] = Black -> reachable_from G R j).
(* TODO: above, might need to maintain that [R \c nodes G]
in order to prove facts of the form [r \in nodes G] *)
(* TODO: above, might need to maintain that [R \c nodes G]
in order to prove facts of the form [r \in nodes G] *)
Definition hinv G R C g c :=
g ~> RGraph G
g ~> RGraph G
\* c ~> Array C
\* \[ inv G R C ].
......@@ -400,14 +491,27 @@ Definition hinv G R C g c :=
Lemma evolution_refl : refl evolution.
Proof using. (* trivial *)
=> C. splits*.
Qed.
=> C. splits*.
Qed.
Lemma evolution_index_fwd : forall C C' x,
evolution C C' ->
index C x ->
index C' x.
Proof. introv E I. destructs* E. Qed.
Lemma evolution_index_bwd : forall C C' x,
evolution C C' ->
index C' x ->
index C x.
Proof. introv E I. destructs* E. Qed.
Hint Resolve evolution_index_fwd evolution_index_bwd.
Lemma evolution_trans : trans evolution.
Proof using. (* trivial *)
=>> (F1&G1) (F2&G2). unfolds evolution. splits.
autos*.
intros. rewrite~ G1.
=>> (L1&F1&G1) (L2&F2&G2). unfolds evolution. splits*.
intros. rewrite* G1. rewrite* G2.
Qed.
Lemma evolution_write_black : forall G i C C',
......@@ -416,23 +520,25 @@ Lemma evolution_write_black : forall G i C C',
no_white_in (out_edges G i) C' ->
evolution C C'[i := Black].
Proof using. (* trivial *)
=>> (E1&E2) Ci HN. split.
{ => j Hj Ej. rew_array~. case_if~.
{ apply~ E1. rew_array~. case_if~. } }
{ => j Hj. rew_array~. case_if.
{ rename j into i. iff; auto_false. }
{ rewrite~ <- E2. rew_array~. case_if*. } }
Qed.
=>> (L1&E1&E2) Ci HN. splits.
{ rew_array~ in *. }
{ => j Hj Ej. rew_array*. case_if~.
{ apply* E1. rew_array~. case_if~. } }
{ => j Hj. rew_array*. case_if.
{ subst. rename j into i. iff; auto_false. }
{ rewrite* <- E2. rew_array~. case_if*. } }
Qed.
Lemma no_white_in_evolution : forall C C' E,
no_white_in E C ->
evolution C C' ->
no_white_in E C'.
Proof using. (* trivial *)
=>> N (H1&H2) i Hi. cases (C[i]) as Ci.
{ false* N. }
{ forwards~ (H2a&_): H2 i. rewrite~ H2a. auto_false. }
rewrite~ H1. auto_false.
=>> N (L1&H1&H2) i Hi.
forwards~ (Ii&Ci'): N Hi. cases (C[i]) as Ci.
{ false. }
{ splits*. forwards~ (H2a&_): H2 i. rewrite~ H2a. }
splits*. rewrite~ H1.
Qed.
Lemma no_gray_evolution : forall C C',
......@@ -440,17 +546,18 @@ Lemma no_gray_evolution : forall C C',
evolution C C' ->
no_gray C'.
Proof using. (* trivial *)
=>> N (H1&H2) i Hi Ci. forwards~ (_&HR): H2 i. applys~ N i.
Qed.
=>> N (L1&H1&H2) i Hi Ci. forwards* (_&HR): H2 i. applys* N i.
Qed.
Lemma no_black_to_white_no_gray_elim : forall G C i j,
nodes_index G (length C) ->
no_black_to_white G C ->
no_gray C ->
reachable G i j ->
C[i] = Black ->
C[j] = Black.
Proof using.
=>> HW HG (p&HP). induction HP; => Ci.
Proof using.
=>> I HW HG (p&HP). induction HP; => Ci.
(* trivial after induction *)
{ auto. }
{ applys IHHP. cases (C[y]).
......@@ -464,9 +571,9 @@ Lemma inv_empty : forall G n,
inv G \{} (make n White).
Proof using. (* trivial *)
=>> Hn. splits.
{ hnf in Hn. rew_arr*. }
{ =>> Hi Ci. false. rew_arr~ in Ci. false. }
{ => i Hi Ci. false. rew_arr~ in Ci. false. }
{ hnf in Hn. rew_array*. auto. (* TODO: fix tactic *) }
{ =>> Hi Ci. false. rew_array* in Ci. false. }
{ => i Hi Ci. false. rew_array* in Ci. false. }
Qed.
Lemma inv_add_root : forall G L C i,
......@@ -476,7 +583,8 @@ Proof using. (* trivial *)
=>> (I1&I2&I3). splits.
{ auto. }
{ auto. }
{ => j Hj Cj. forwards~ (r&Hr&Pr): I3 j. exists* r. }
{ => j Hj Cj. forwards~ (r&Hr&Pr): I3 j.
exists* r. splits*. rew_set. eauto. (* TODO: tactic *) }
Qed.
Lemma inv_gray_root : forall G R C i,
......@@ -486,10 +594,10 @@ Lemma inv_gray_root : forall G R C i,
inv G R (C[i := Gray]).
Proof using. (* trivial *)
=>> Ci Hi (I1&I2&I3). splits.
{ rew_arr~. }
{ => j k Hjk. rew_array~. => Cjk. case_if; auto_false.
case_if. applys* I2. }
{ => j Hj. rew_array~. case_if; auto_false. }
{ rew_array~. }
{ => j k Hjk. rew_array*. => Cjk. case_if; auto_false.
case_if. applys* I2. }
{ => j Hj. rew_array*. case_if; auto_false. }
Qed.
Lemma inv_evolution_black : forall G R C' i,
......@@ -499,14 +607,21 @@ Lemma inv_evolution_black : forall G R C' i,
inv G R (C'[i := Black]).
Proof using. (* trivial *)
=>> (I1&I2&I3) Ri Wi. splits.
{ rew_arr~. }
{ => j k Hjk. rew_array~. => M. case_if; auto_false. case_if.
{ applys Wi. rewrite~ out_edges_has_edge. }
{ rew_array~. }
{ => j k Hjk. rew_array*. => M. case_if; auto_false. case_if.
{ subst. applys Wi. rewrite~ out_edges_has_edge. }
{ applys* I2. } }
{ => j Hj. rew_array~. case_if; [|auto].
=> _. rename j into i. eauto. }
{ => j Hj. rew_array*. case_if; [subst|auto].
=> _. rename j into i. eauto. }
Qed.
Lemma inv_index : forall G R C i,
i \in nodes G ->
inv G R C ->
index C i.
Proof. introv I Inv. destructs* Inv. Qed.
Hint Resolve inv_index.
(*************************************************************************)
(** Verification of DFS *)
......@@ -515,7 +630,7 @@ Lemma dfs_from_spec : forall G R C g c i,
reachable_from G R i ->
C[i] = White ->
app dfs_from [g c i]
PRE (hinv G R C g c)
PRE (hinv G R C g c)
POST (# Hexists C', hinv G R C' g c
\* \[ evolution C C' /\ C'[i] = Black ]).
Proof using.
......@@ -523,127 +638,115 @@ Proof using.
=> G R C0. =>> Ri Wi.
asserts Hi: (i \in nodes G).
{ destruct Ri as (r&Hr&Mr). applys* reachable_in_nodes_r. } (* trivial *)
xcf. unfold hinv. xpull ;=> HI. xapps~. sets_eq C1: (C0[i:=Gray]).
xfun as f. set (loop_inv := fun L C => hinv G R C g c
xcf. unfold hinv. xpull ;=> HI. xapps*. sets_eq C1: (C0[i:=Gray]).
xfun as f. set (loop_inv := fun L C => hinv G R C g c
\* \[ evolution C1 C /\ no_white_in L C ]).
xseq. xapp_no_simpl (>> (fun L => Hexists C, loop_inv L C) G).
{ auto. }
{ => L. unfold loop_inv, hinv. applys heap_contains_intro
(Hexists C, c ~> Array C \* \[ inv G R C] \* (* ideally, should be computed *)
\[ evolution C1 C /\ no_white_in L C]); xsimpl~. }
{ => j js Hj Eij. unfold loop_inv, hinv.
{ => j js Hj Eij. unfold loop_inv, hinv.
xpull ;=> C I0 (H1&H2). xapp. clears f.
xapps~. xapps~. xpolymorphic_eq.
xapps*. xapps~. xpolymorphic_eq.
xpost (Hexists C', hinv G R C' g c
\* \[ evolution C1 C' /\ no_white_in js C' /\ C'[j] <> White ]).
{ xif.
{ show IH. xapply (>> IH G R C).
{ show IH. xapply (>> IH G R C).
{ destruct Ri as (r&Pr&Mr). exists r. split~. (* trivial *)
applys* reachable_trans_edge. } (* trivial *)
{ auto. } (* trivial *)
{ auto. } (* trivial *)
{ unfold hinv. xsimpl~. }
unfold hinv. xpull ;=> C' I1 (F1&F2). xsimpl. splits.
unfold hinv. xpull ;=> C' I1 (F1&F2). xsimpl. splits.
{ applys* evolution_trans. }
{ applys* no_white_in_evolution. } (* trivial *)
{ auto_false. } (* trivial *)
{ auto. } } (* trivial *)
{ applys* no_white_in_evolution. } (* trivial *)
{ auto_false. } (* trivial *)
{ auto. } } (* trivial *)
{ xret. unfold hinv. xsimpl~. } }
{ unfold hinv. xpull ;=> C' I1 (F1&F2&F3). xsimpl. splits.
{ auto. } (* trivial *)
{ => k Hk. set_in Hk; auto. } (* trivial *)
{ auto. } } } (* trivial *)
{ auto. } (* trivial *)
{ => k Hk. rew_set in Hk. destruct~ Hk. subst*. } (* trivial *)
{ auto. } } } (* trivial *)
{ clears f. unfold loop_inv, hinv. xsimpl. split.
{ applys evolution_refl. }
{ => j Hj. rew_array~. } (* trivial *)
{ => j Hj. rew_set in Hj. false. } (* trivial *)
{ subst C1. applys* inv_gray_root. } }
{ unfold loop_inv, hinv. xpull ;=> C' I1 (F1&F2).
xapps~. xsimpl. split.
xapps*. xsimpl. split.
{ subst C1. applys* evolution_write_black. }
{ rew_arr~. } (* trivial *)
{ rew_array*. case_if~. } (* trivial *)
{ applys* inv_evolution_black. } }
Qed.
Hint Extern 1 (RegisterSpec dfs_from) => Provide dfs_from_spec.
Lemma dfs_main_spec : forall (G:graph) g (rs:list int),
app dfs_main [g rs]
PRE (g ~> RGraph G)
Forall (fun i => i \in nodes G) rs ->
app dfs_main [g rs]
PRE (g ~> RGraph G)
POST (fun c => Hexists C,
c ~> Array C \*
c ~> Array C \*
g ~> RGraph G \*
\[ forall i, i \in nodes G ->
\[ forall i, i \in nodes G ->
(C[i] = Black <-> exists r, r \in set_of_list rs /\ reachable G r i)]).
Proof using.
xcf. xapp. => Hn. xapp.
Proof using.
introv Hrs. xcf. xapp. => Hn. xapp.
{ applys (proj1 Hn). } (* trivial *)
=> C0 HC0.
asserts N0: (no_gray C0). { subst. => i Hi. rew_arr; auto_false. } (* trivial *)
asserts N0: (no_gray C0).
{ subst. => i Hi. rew_array; auto_false.
rewrite index_eq_index_length in Hi. rew_array~ in Hi.
unfolds* nodes_index. } (* trivial *)
xfun as f.
set (loop_inv := fun L C => hinv G (set_of_list L) C g c
\* \[ evolution C0 C /\ all_black_in (set_of_list L) C ]).
xapp (fun L => Hexists C, loop_inv L C).
{ => i L T HL. lets (_&Hi): (proj2 Hn) i.
{ => i L T HL.
assert (i \in nodes G).
{ forwards~: Forall_mem_inv i Hrs. subst rs. rew_listx~. }
unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2).
xapp. clears f. xapps~. xapps~. xpolymorphic_eq. xif.
xapp. clears f. xapps*. xapps~. xpolymorphic_eq. xif.
{ xapp G (\{i} \u set_of_list L) C.
{ exists i. split~. applys* reachable_self. } (* trivial *)
{ auto. } (* trivial *)
{ exists i. split.
{ rew_set; eauto. } (* TODO: tactic *)
{ applys* reachable_self. } } (* trivial *)
{ auto. } (* trivial *)
{ unfold hinv. xsimpl*. applys* inv_add_root. }
{ unfold loop_inv, hinv. intros u. xpull ;=> C' I1 (F1&F2).
rew_set_of_list. xsimpl.
{ splits. (* trivial *)
{ applys~ evolution_trans F1. } (* trivial *)
{ => j Hj. set_in Hj; eauto. applys~ (proj1 F1). } } (* trivial *)
{ => j Hj.
assert (index C j).
{ rew_set in Hj. destruct Hj as [| ->]; [| now autos*].
forwards* (?&?): HC2. }
splits*. rew_set in Hj. destruct Hj. (* trivial *)
{ applys* F1. applys~ HC2. } { subst~. } } } (* trivial *)
{ rewrite~ union_comm. } } } (* trivial *)
{ xret. unfold loop_inv, hinv. rew_set_of_list. xsimpl~. split.
{ auto. } (* trivial *)
{ => j Hj. set_in Hj; eauto. cases (C[i]); auto_false. (* trivial *)
false~ N0 i. forwards~ (_&?): (proj2 HC1). } (* trivial *)