Commit 5d7ef74f authored by Ralf Jung's avatar Ralf Jung

Turn master into Iris 2.0

Everything has been re-written from scratch
parents 50738b0e 4a272286
;;; Directory Local Variables
;;; See Info node `(emacs) Directory Variables' for more information.
((coq-mode
(coq-load-path
(rec "." "_"))))
*.v~
*.vo
*.v.d
*.glob
guide
html
*.cache
*.aux
\#*\#
*~
*.bak
.coq-native/
Makefile
All files in this development, excluding those in docs/, are distributed
under the terms of the BSD license, included below.
------------------------------------------------------------------------------
BSD LICENCE
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
* Neither the name of the <organization> nor the
names of its contributors may be used to endorse or promote products
derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
# This Makefile started being auto-generated, but now it's hand-crafted and automatically finds all the files.
# YOU SHOULD NOT HAVE TO EDIT THIS FILE.
.DEFAULT_GOAL := all
#
# This Makefile may take arguments passed as environment variables:
# COQBIN to specify the directory where Coq binaries resides;
# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
# DSTROOT to specify a prefix to install path.
# Here is a hack to make $(eval $(shell works:
define donewline
endef
includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
$(call includecmdwithout@,$(COQBIN)coqtop -config)
##########################
# #
# Libraries definitions. #
# #
##########################
COQLIBS?=-I . -R . _
COQDOCLIBS?=-I lib
##########################
# #
# Variables definitions. #
# #
##########################
OPT?=
COQDEP?="$(COQBIN)coqdep" -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8
COQC?="$(COQBIN)coqc"
GALLINA?="$(COQBIN)gallina"
COQDOC?="$(COQBIN)coqdoc"
COQCHK?="$(COQBIN)coqchk"
##################
# #
# Install Paths. #
# #
##################
ifdef USERINSTALL
XDG_DATA_HOME?="$(HOME)/.local/share"
COQLIBINSTALL=$(XDG_DATA_HOME)/coq
COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
else
COQLIBINSTALL="${COQLIB}user-contrib"
COQDOCINSTALL="${DOCDIR}user-contrib"
endif
######################
# #
# Files dispatching. #
# #
######################
LIBVFILES:=$(wildcard lib/*/*.v)
VFILES:=$(wildcard *.v) $(LIBVFILES)
-include $(addsuffix .d,$(VFILES))
.SECONDARY: $(addsuffix .d,$(VFILES))
VOFILES:=$(VFILES:.v=.vo)
LIBVOFILES:=$(LIBVFILES:.v=.vo)
VOFILESINC=$(filter $(wildcard ./*),$(VOFILES))
GLOBFILES:=$(VFILES:.v=.glob)
VIFILES:=$(VFILES:.v=.vi)
GFILES:=$(VFILES:.v=.g)
HTMLFILES:=$(VFILES:.v=.html)
GHTMLFILES:=$(VFILES:.v=.g.html)
ifeq '$(HASNATDYNLINK)' 'true'
HASNATDYNLINK_OR_EMPTY := yes
else
HASNATDYNLINK_OR_EMPTY :=
endif
#######################################
# #
# Definition of the toplevel targets. #
# #
#######################################
all: $(VOFILES)
lib: $(LIBVOFILES)
spec: $(VIFILES)
gallina: $(GFILES)
html: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
gallinahtml: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
all.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
validate: $(VOFILES)
$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
beautify: $(VFILES:=.beautified)
for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
@echo 'Do not do "make clean" until you are sure that everything went well!'
@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
.PHONY: all lib opt byte archclean clean install userinstall depend html validate
####################
# #
# Special targets. #
# #
####################
byte:
$(MAKE) all "OPT:=-byte"
opt:
$(MAKE) all "OPT:=-opt"
userinstall:
+$(MAKE) USERINSTALL=true install
clean:
rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
- rm -rf html mlihtml
archclean:
rm -f *.cmx *.o
printenv:
@"$(COQBIN)coqtop" -config
@echo 'CAMLC = $(CAMLC)'
@echo 'CAMLOPTC = $(CAMLOPTC)'
@echo 'PP = $(PP)'
@echo 'COQFLAGS = $(COQFLAGS)'
@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
###################
# #
# Implicit rules. #
# #
###################
%.vo %.glob: %.v
$(COQC) $(COQDEBUG) $(COQFLAGS) $*
%.vi: %.v
$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
%.g: %.v
$(GALLINA) $<
%.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
%.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
%.g.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
%.g.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@
%.v.d: %.v Makefile
$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
%.v.beautified:
$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
PREREQUISITES
-------------
This version is known to compile with:
- Coq 8.5
- Ssreflect 1.6
- Autosubst 1.4
For development, better make sure you have a version of Ssreflect that includes
commit be724937 (no such version has been released so far, you will have to
fetch the development branch yourself). Iris compiles fine even without this
patch, but proof bullets will only be in 'strict' (enforcing) mode with the
fixed version of Ssreflect.
BUILDING INSTRUCTIONS
---------------------
Run the following commands to build the full development:
./configure
make
DESCRIPTION
This folder contains the Coq development for
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
by
Ralf Jung <jung@mpi-sws.org>
David Swasey <swasey@mpi-sws.org>
Filip Sieczkowski <filips@cs.au.dk>
Kasper Svendsen <ksvendsen@cs.au.dk>
Aaron Turon <turon@mpi-sws.org>
Lars Birkedal <birkedal@cs.au.dk>
Derek Dreyer <dreyer@mpi-sws.org>
CONTENTS
Our artifact is a Coq formalization of the model of our Iris logic,
together with a proof of adequacy (establishing that the model is
faithful wrt the operational semantics) and a proof of soundness of
the primitive rules of the logic wrt the model.
NOTE: We have just mechanized the *soundness* of the *primitive*
rules of Iris in Coq. We have not mechanized the proofs of derived
rules (i.e. those derivable from the primitive rules), nor have we
mechanized the case study or other examples that are proven within
the logic. Proof outlines for the latter are given in the appendix
that accompanied the POPL submission, and will be fleshed out even
further for the final version of the appendix.
The reason we focused on the primitive rules is that those are the
rules whose soundness is proven by direct appeal to the semantic
model of Iris. For space reasons, we did not want to present the
semantic model of Iris in any detail in the paper, but we still
wanted to give the reader confidence in the results of the paper.
With our Coq mechanization in hand, the reader can safely ignore the
semantic model and instead focus on how to *use* the primitive rules
of the logic (to derive more sophisticated rules or prove
interesting examples).
Mechanizing Iris proofs is a very interesting and important
direction for future work, but it is beyond the scope of the paper.
The folder is organized as follows:
* core_lang.v contains the axioms about the language
* lang.v defines the threadpool reduction and derives some lemmas
from core_lang.v
* world_prop_recdom.v uses the ModuRes Coq library to construct the domain
for Iris propositions, satisfying the interface to the Iris domain
defined in world_prop.v
* iris_core.v constructs the BI structure on the Iris domain, and defines
some additional connectives (box, later, ownership).
* iris_plog.v adds the programming logic: World satisfaction, primitive view shifts,
weakest precondition.
* iris_vs_rules.v and iris_wp_rules.v contain proofs of the primitive proof
rules for primitive view shifts and weakest precondition, respectively.
* iris_derived_rules.v derives rules for Hoare triples and view shifts
(as presented in the appendix).
* iris_meta.v proves adequacy and the lifting lemmas
The development uses ModuRes, a Coq library by Sieczkowski et al. to
solve the recursive domain equation (see the paper for a reference)
and prove some of the standard separation logic rules. It is located
in the lib/ subdirectory.
REQUIREMENTS
Coq
We have tested the development using Coq 8.4pl4 on Linux and Mac
machines. The entire compilation took less than 15 minutes.
HOW TO COMPILE
To compile the development, run
> make -j
in the folder containing this README.
OVERVIEW OF LEMMAS
Below we give a mapping from proof rules in the paper to Coq lemma's.
RULE Coq lemma
-----------------------
VSTimeless iris_derived_rules.v:vsTimeless
NewInv iris_derived_rules.v:vsNewInv
InvOpen iris_derived_rules.v:vsOpen
InvClose iris_derived_rules.v:vsClose
VSTrans iris_derived_rules.v:vsTrans
VSImp iris_derived_rules.v:vsEnt
VSFrame iris_derived_rules.v:vsFrame
FpUpd iris_derived_rules.v:vsGhostUpd
Ret iris_derived_rules.v:htRet
Bind iris_derived_rules.v:htBind
Frame iris_derived_rules.v:htFrame
AFrame iris_derived_rules.v:htAFrame
Csq iris_derived_rules.v:htCons
ACSQ iris_derived_rules.v:htACons
Fork iris_derived_rules.v:htFork
The main adequacy result is expressed by Theorem
iris_meta.v:adequacy_obs.
-Q . ""
prelude/option.v
prelude/fin_map_dom.v
prelude/bsets.v
prelude/fin_maps.v
prelude/vector.v
prelude/pmap.v
prelude/stringmap.v
prelude/fin_collections.v
prelude/mapset.v
prelude/proof_irrel.v
prelude/hashset.v
prelude/pretty.v
prelude/countable.v
prelude/orders.v
prelude/natmap.v
prelude/strings.v
prelude/relations.v
prelude/collections.v
prelude/listset.v
prelude/streams.v
prelude/gmap.v
prelude/base.v
prelude/tactics.v
prelude/prelude.v
prelude/listset_nodup.v
prelude/finite.v
prelude/numbers.v
prelude/nmap.v
prelude/zmap.v
prelude/co_pset.v
prelude/lexico.v
prelude/sets.v
prelude/decidable.v
prelude/list.v
prelude/error.v
algebra/option.v
algebra/cmra.v
algebra/cmra_big_op.v
algebra/cmra_tactics.v
algebra/sts.v
algebra/auth.v
algebra/fin_maps.v
logic/upred.v
algebra/cofe.v
algebra/base.v
algebra/dra.v
algebra/cofe_solver.v
algebra/agree.v
algebra/excl.v
program_logic/model.v
program_logic/adequacy.v
program_logic/hoare_lifting.v
program_logic/lifting.v
program_logic/namespace.v
program_logic/viewshifts.v
program_logic/wsat.v
program_logic/ownership.v
program_logic/weakestpre.v
program_logic/pviewshifts.v
program_logic/resources.v
program_logic/hoare.v
program_logic/language.v
program_logic/functor.v
program_logic/tests.v
heap_lang/heap_lang.v
heap_lang/heap_lang_tactics.v
heap_lang/lifting.v
heap_lang/sugar.v
heap_lang/tests.v
Require Export algebra.cmra.
Local Hint Extern 10 (_ _) => omega.
Record agree (A : Type) : Type := Agree {
agree_car :> nat A;
agree_is_valid : nat Prop;
agree_valid_0 : agree_is_valid 0;
agree_valid_S n : agree_is_valid (S n) agree_is_valid n
}.
Arguments Agree {_} _ _ _ _.
Arguments agree_car {_} _ _.
Arguments agree_is_valid {_} _ _.
Section agree.
Context {A : cofeT}.
Instance agree_validN : ValidN (agree A) := λ n x,
agree_is_valid x n n', n' n x n' ={n'}= x n.
Lemma agree_valid_le (x : agree A) n n' :
agree_is_valid x n n' n agree_is_valid x n'.
Proof. induction 2; eauto using agree_valid_S. Qed.
Instance agree_equiv : Equiv (agree A) := λ x y,
( n, agree_is_valid x n agree_is_valid y n)
( n, agree_is_valid x n x n ={n}= y n).
Instance agree_dist : Dist (agree A) := λ n x y,
( n', n' n agree_is_valid x n' agree_is_valid y n')
( n', n' n agree_is_valid x n' x n' ={n'}= y n').
Program Instance agree_compl : Compl (agree A) := λ c,
{| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}.
Next Obligation. intros; apply agree_valid_0. Qed.
Next Obligation.
intros c n ?; apply (chain_cauchy c n (S n)), agree_valid_S; auto.
Qed.
Definition agree_cofe_mixin : CofeMixin (agree A).
Proof.
split.
* intros x y; split.
+ by intros Hxy n; split; intros; apply Hxy.
+ by intros Hxy; split; intros; apply Hxy with n.
* split.
+ by split.
+ by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
+ intros x y z Hxy Hyz; split; intros n'; intros.
- transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz.
- transitivity (y n'). by apply Hxy. by apply Hyz, Hxy.
* intros n x y Hxy; split; intros; apply Hxy; auto.
* intros x y; split; intros n'; rewrite Nat.le_0_r; intros ->; [|done].
by split; intros; apply agree_valid_0.
* by intros c n; split; intros; apply (chain_cauchy c).
Qed.
Canonical Structure agreeC := CofeT agree_cofe_mixin.
Lemma agree_car_ne (x y : agree A) n : {n} x x ={n}= y x n ={n}= y n.
Proof. by intros [??] Hxy; apply Hxy. Qed.
Lemma agree_cauchy (x : agree A) n i : {n} x i n x i ={i}= x n.
Proof. by intros [? Hx]; apply Hx. Qed.
Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x;
agree_is_valid n := agree_is_valid x n agree_is_valid y n x ={n}= y |}.
Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Instance agree_unit : Unit (agree A) := id.
Instance agree_minus : Minus (agree A) := λ x y, x.
Instance: Commutative () (@op (agree A) _).
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
Definition agree_idempotent (x : agree A) : x x x.
Proof. split; naive_solver. Qed.
Instance: n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n).
Proof.
intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?].
rewrite -(proj2 Hxy n') 1?(Hx n'); eauto using agree_valid_le.
by apply dist_le with n; try apply Hxy.
Qed.
Instance: x : agree A, Proper (dist n ==> dist n) (op x).
Proof.
intros n x y1 y2 [Hy' Hy]; split; [|done].
split; intros (?&?&Hxy); repeat (intro || split);
try apply Hy'; eauto using agree_valid_le.
* etransitivity; [apply Hxy|apply Hy]; eauto using agree_valid_le.
* etransitivity; [apply Hxy|symmetry; apply Hy, Hy'];
eauto using agree_valid_le.
Qed.
Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(commutative _ _ y2) Hx. Qed.
Instance: Proper (() ==> () ==> ()) op := ne_proper_2 _.
Instance: Associative () (@op (agree A) _).
Proof.
intros x y z; split; simpl; intuition;
repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
by cofe_subst; rewrite !agree_idempotent.
Qed.
Lemma agree_includedN (x y : agree A) n : x {n} y y ={n}= x y.
Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz (associative _) agree_idempotent.
Qed.
Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
split; try (apply _ || done).
* by intros n x1 x2 Hx y1 y2 Hy.
* intros x; split; [apply agree_valid_0|].
by intros n'; rewrite Nat.le_0_r; intros ->.
* intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
rewrite (Hx n'); last auto.
symmetry; apply dist_le with n; try apply Hx; auto.
* intros x; apply agree_idempotent.
* by intros x y n [(?&?&?) ?].
* by intros x y n; rewrite agree_includedN.
Qed.
Lemma agree_op_inv (x1 x2 : agree A) n : {n} (x1 x2) x1 ={n}= x2.
Proof. intros Hxy; apply Hxy. Qed.
Lemma agree_valid_includedN (x y : agree A) n : {n} y x {n} y x ={n}= y.
Proof.
move=> Hval [z Hy]; move: Hval; rewrite Hy.
by move=> /agree_op_inv->; rewrite agree_idempotent.
Qed.
Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A).
Proof.
intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
* by rewrite agree_idempotent.
* by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idempotent.
Qed.
Canonical Structure agreeRA : cmraT :=
CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin.
Program Definition to_agree (x : A) : agree A :=
{| agree_car n := x; agree_is_valid n := True |}.
Solve Obligations with done.
Global Instance to_agree_ne