Commit c92854e5 authored by Robbert Krebbers's avatar Robbert Krebbers

Initial commit.

parents
*.vo
*.vio
*.v.d
.coqdeps.d
*.glob
*.cache
*.aux
\#*\#
.\#*
*~
*.bak
.coqdeps.d
.coq-native/
build-dep/
Makefile.coq
Makefile.coq.conf
*.crashcoqide
All files in this development 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.
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq
+@make -f Makefile.coq all
.PHONY: all
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
.PHONY: clean
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Install build-dependencies
build-dep/opam: opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything.
@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
@# package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
((! opam --version | grep "^1\." > /dev/null) || ( \
echo "# Reinstalling build-dep package." && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \
))
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
awk.Makefile: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
This diff is collapsed.
-Q theories iron
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/algebra/vfrac.v
theories/algebra/vfrac_auth.v
theories/bi/fracpred.v
theories/proofmode/fracpred.v
theories/iron_logic/iron.v
theories/iron_logic/fcinv.v
theories/iron_logic/weakestpre.v
theories/iron_logic/adequacy.v
theories/iron_logic/lifting.v
theories/heap_lang/lang.v
theories/heap_lang/heap.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/notation.v
theories/heap_lang/adequacy.v
theories/heap_lang/proofmode.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
theories/heap_lang/lib/spin_lock.v
theories/heap_lang/lib/spin_lock_track.v
theories/heap_lang/lib/resource_transfer_par.v
theories/heap_lang/lib/resource_transfer_fork.v
theories/heap_lang/lib/resource_transfer_sts.v
theories/heap_lang/lib/list.v
theories/heap_lang/lib/bag.v
theories/heap_lang/lib/queue.v
theories/heap_lang/lib/message_passing.v
theories/heap_lang/lib/message_passing_example.v
# awk program that patches the Makefile generated by Coq.
# Detect the name this project will be installed under.
/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
# Wow, POSIX awk is really broken. I mean, isn't it supposed to be a text processing language?
# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
# we can just split the string at '/' here.
split($0, PIECES, /\//);
PROJECT=PIECES[2];
}
# Patch the uninstall target to work properly, and to also uninstall stale files.
# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
# This (and the section above) can be removed once we no longer support Coq 8.6.
/^uninstall: / {
print "uninstall:";
print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
getline;
next
}
# This forwards all unchanged lines
1
(** This file provides a version of the fractional camera whose elements can be
between (not including) 0 and infinity. This differs from the standard
fractional camera in [algebra/frac] in the Iris repository, whose elements
be [≤ 1]. Fractions [> 1] are mainly useful in combination with the fractional
authoritative cameras, as in the file [vfrac_auth].
This file is much the same as the one in the Iris repository. The main
difference is that the validity predicate is changed (it is [True] instead of
[≤ 1]). To avoid ambiguity in the canonical structure search, we wrap the
type of fractions [vfrac] in a definition instead of a notation. *)
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
Definition vfrac := Qp.
Section vfrac.
Canonical Structure vfracC := leibnizC vfrac.
Instance vfrac_valid : Valid vfrac := λ x, True.
Instance vfrac_pcore : PCore vfrac := λ _, None.
Instance vfrac_op : Op vfrac := λ x y, (x + y)%Qp.
Lemma vfrac_included (x y : vfrac) : x y (x < y)%Qc.
Proof. by rewrite Qp_lt_sum. Qed.
Corollary vfrac_included_weak (x y : vfrac) : x y (x y)%Qc.
Proof. intros ?%vfrac_included. auto using Qclt_le_weak. Qed.
Definition vfrac_ra_mixin : RAMixin vfrac.
Proof. split; try apply _; try done. Qed.
Canonical Structure vfracR := discreteR vfrac vfrac_ra_mixin.
Global Instance vfrac_cmra_discrete : CmraDiscrete vfracR.
Proof. apply discrete_cmra_discrete. Qed.
End vfrac.
Global Instance vfrac_cancelable (q : vfrac) : Cancelable q.
Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
Global Instance vfrac_id_free (q : vfrac) : IdFree q.
Proof.
intros [q0 Hq0] ? EQ%Qp_eq. rewrite -{1}(Qcplus_0_r q) in EQ.
eapply Qclt_not_eq; first done. by apply (inj (Qcplus q)).
Qed.
Lemma vfrac_op' (q p : vfrac) : (p q) = (p + q)%Qp.
Proof. done. Qed.
Global Instance is_op_vfrac (q : vfrac) : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp vfrac_op' Qp_div_2. Qed.
(** This file provides a version of the fractional authoritative camera that
can be used with fractions [> 1]. This is useful in the state interpretation of
Iron (see the file [heap_lang/heap]), where we want to keep track of a surplus
of fragmental elements by forked-off threads.
Much of the reasoning principles for this version of the fractional
authoritative cameras are the same as for the original version. There are two
difference:
- We get the additional rule:
<<<
✓ (a ⋅ b) → ●?{p} a ~~> ●?{p + q} (a ⋅ b) ⋅ ◯?{q} b
>>>
That can be used to allocate a surplus.
- We no longer have the [◯?{1} a] is the exclusive fragmental element (cf.
[frac_auth_frag_validN_op_1_l] in Iris).
*)
From iris.algebra Require Export auth frac.
From iron.algebra Require Import vfrac.
From iris.algebra Require Export updates local_updates.
From iris.algebra Require Import proofmode_classes.
From Coq Require Import QArith Qcanon.
Definition vfrac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR vfracR A)).
Definition vfrac_authUR (A : cmraT) : ucmraT :=
authUR (optionUR (prodR vfracR A)).
Definition vfrac_auth_auth {A : cmraT} (q : Qp) (x : A) : vfrac_authR A :=
(Some (q,x)).
Definition vfrac_auth_frag {A : cmraT} (q : Qp) (x : A) : vfrac_authR A :=
(Some (q,x)).
Typeclasses Opaque vfrac_auth_auth vfrac_auth_frag.
Instance: Params (@vfrac_auth_auth) 2.
Instance: Params (@vfrac_auth_frag) 2.
Notation "●?{ q } a" := (vfrac_auth_auth q a) (at level 10, format "●?{ q } a").
Notation "◯?{ q } a" := (vfrac_auth_frag q a) (at level 10, format "◯?{ q } a").
Section vfrac_auth.
Context {A : cmraT}.
Implicit Types a b : A.
Global Instance vfrac_auth_auth_ne q : NonExpansive (@vfrac_auth_auth A q).
Proof. solve_proper. Qed.
Global Instance vfrac_auth_auth_proper q : Proper (() ==> ()) (@vfrac_auth_auth A q).
Proof. solve_proper. Qed.
Global Instance vfrac_auth_frag_ne q : NonExpansive (@vfrac_auth_frag A q).
Proof. solve_proper. Qed.
Global Instance vfrac_auth_frag_proper q : Proper (() ==> ()) (@vfrac_auth_frag A q).
Proof. solve_proper. Qed.
Global Instance vfrac_auth_auth_discrete a : Discrete a Discrete (?{q} a).
Proof. intros; apply Auth_discrete; apply _. Qed.
Global Instance vfrac_auth_frag_discrete a : Discrete a Discrete (?{q} a).
Proof. intros; apply Auth_discrete, Some_discrete; apply _. Qed.
Lemma vfrac_auth_validN n a p : {n} a {n} (?{p} a ?{p} a).
Proof. done. Qed.
Lemma vfrac_auth_valid p a : a (?{p} a ?{p} a).
Proof. done. Qed.
Lemma vfrac_auth_agreeN n p a b : {n} (?{p} a ?{p} b) a {n} b.
Proof.
rewrite auth_validN_eq /= => -[Hincl Hvalid].
move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]].
move=> /discrete_iff /leibniz_equiv_iff; rewrite vfrac_op'=> [/Qp_eq/=].
rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
Qed.
Lemma vfrac_auth_agree p a b : (?{p} a ?{p} b) a b.
Proof.
intros. apply equiv_dist=> n. by eapply vfrac_auth_agreeN, cmra_valid_validN.
Qed.
Lemma vfrac_auth_agreeL `{!LeibnizEquiv A} p a b : (?{p} a ?{p} b) a = b.
Proof. intros. by eapply leibniz_equiv, vfrac_auth_agree. Qed.
Lemma vfrac_auth_includedN n p q a b : {n} (?{p} a ?{q} b) Some b {n} Some a.
Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed.
Lemma vfrac_auth_included `{CmraDiscrete A} q p a b :
(?{p} a ?{q} b) Some b Some a.
Proof. rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _] //. Qed.
Lemma vfrac_auth_includedN_total `{CmraTotal A} n q p a b :
{n} (?{p} a ?{q} b) b {n} a.
Proof. intros. by eapply Some_includedN_total, vfrac_auth_includedN. Qed.
Lemma vfrac_auth_included_total `{CmraDiscrete A, CmraTotal A} q p a b :
(?{p} a ?{q} b) b a.
Proof. intros. by eapply Some_included_total, vfrac_auth_included. Qed.
Lemma vfrac_auth_auth_validN n q a : {n} (?{q} a) {n} a.
Proof.
split; [by intros [_ [??]]|].
repeat split; simpl; by try apply: ucmra_unit_leastN.
Qed.
Lemma vfrac_auth_auth_valid q a : (?{q} a) a.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite vfrac_auth_auth_validN. Qed.
Lemma vfrac_auth_frag_validN n q a : {n} (?{q} a) {n} a.
Proof. split. by intros [??]. by split. Qed.
Lemma vfrac_auth_frag_valid q a : (?{q} a) a.
Proof. split. by intros [??]. by split. Qed.
Lemma vfrac_auth_frag_op q1 q2 a1 a2 : ?{q1+q2} (a1 a2) ?{q1} a1 ?{q2} a2.
Proof. done. Qed.
Global Instance is_op_vfrac_auth q q1 q2 a a1 a2 :
IsOp q q1 q2 IsOp a a1 a2 IsOp' (?{q} a) (?{q1} a1) (?{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
Global Instance is_op_vfrac_auth_core_id q q1 q2 a :
CoreId a IsOp q q1 q2 IsOp' (?{q} a) (?{q1} a) (?{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
by rewrite -vfrac_auth_frag_op -core_id_dup.
Qed.
Lemma vfrac_auth_update p q a b a' b' :
(a,b) ~l~> (a',b') ?{p} a ?{q} b ~~> ?{p} a' ?{q} b'.
Proof.
intros. apply: auth_update.
apply: option_local_update. by apply: prod_local_update_2.
Qed.
Lemma vfrac_auth_update' p q a b :
(a b) ?{p} a ~~> ?{p + q} (a b) ?{q} b.
Proof.
intros Hconsistent. apply: auth_update_alloc.
intros n m; simpl; intros [Hvalid1 Hvalid2] Heq.
split.
- split; by apply cmra_valid_validN.
- rewrite -pair_op Some_op Heq comm.
destruct m; simpl; [rewrite left_id | rewrite right_id]; done.
Qed.
End vfrac_auth.
This diff is collapsed.
(** This file proves the basic and correct usage of resources adequacy
statements for [heap_lang]. It does do so by appealing to the generic results
in [iron_logic/adequacy].
Note, we only state adequacy for the lifted logic, because in the Coq
formalization we state all specifications in terms of the lifted logic. *)
From iris.algebra Require Import big_op gmap.
From iron.iron_logic Require Export weakestpre adequacy.
From iron.algebra Require Import vfrac_auth vfrac.
From iron.heap_lang Require Import heap.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> ironInvPreG Σ;
heap_preG_inG :> inG Σ (vfrac_authR heapUR);
heap_preG_fork_post_inG :> inG Σ (authR (gmapUR positive (exclR (optionC vfracC))));
}.
Definition heapΣ : gFunctors := #[
ironInvΣ;
GFunctor (vfrac_authR heapUR);
GFunctor (authR (gmapUR positive (exclR (optionC vfracC))))].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
(** A generic helper *)
Theorem heap_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ},
([ map] l v σ, l v)
WP e @ s; {{ v, |={,}=> ⎡∀ h m, heap_ctx h [] m - ⌜φ v h⌝⎤ }}%I)
adequate s e σ φ.
Proof.
(* TODO: refactor this proof so we don't have the two cases *)
destruct (decide (σ = )) as [->|Heq].
- intros Hwp; eapply (iron_wp_adequacy _ _ _ _ _ _ (1 / 2) ε); iIntros (? κs) "".
iMod (own_alloc (?{1} (?{1/2} ?{1/2} ε))) as (γ) "[Hσ [Hp Hp']]".
{ rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
by apply vfrac_auth_valid. }
iMod (own_alloc ( )) as (γf) "Hf"; first done.
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I.
iFrame "Hp". iSplitL "Hσ Hf".
{ iExists . rewrite /= to_heap_empty fmap_empty big_opM_empty. by iFrame. }
iPoseProof (Hwp _) as "Hwp"; clear Hwp.
iApply (iron_wp_wand with "[Hwp]").
{ iApply "Hwp". by rewrite fracPred_at_emp. }
iIntros (v π1) "Hupd". iExists π1, ε; repeat (iSplit || iModIntro)=> //.
iIntros (π2 π3 h2 Qs Hπ) "Hctx _ _".
iMod ("Hupd" with "Hp'") as (π4 π5 _) "[_ H]".
iModIntro. iApply ("H" with "Hctx").
- intros Hwp; eapply (iron_wp_adequacy _ _ _ _ _ _ (1 / 2 / 2) (Some (1 / 2)%Qp)).
iIntros (? κs) "".
iMod (own_alloc (?{1} (to_heap σ)
(?{1/2} (to_heap σ) ?{1/2} ε))) as (γ) "[Hσ [Hσ' [Hp Hp']]]".
{ rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
apply vfrac_auth_valid; by apply to_heap_valid. }
iMod (own_alloc ( )) as (γf) "Hf"; first done.
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I.
iFrame "Hp". iSplitL "Hσ Hf".
{ iExists . rewrite /= fmap_empty big_opM_empty. by iFrame. }
iPoseProof (Hwp _) as "Hwp"; clear Hwp.
iDestruct (big_mapsto_alt_2 with "Hσ'") as "Hσ'"; first done.
iDestruct ("Hwp" with "Hσ'") as "Hwp'".
iApply (iron_wp_wand with "Hwp'").
iIntros (v π1) "Hupd". iExists π1, ε; repeat (iSplit || iModIntro)=> //.
iIntros (π2 π3 h2 Qs Hπ) "Hctx _ _".
iMod ("Hupd" with "Hp'") as (π4 π5 _) "[_ H]".
iModIntro. iApply ("H" with "Hctx").
Qed.
(** The basic adequacy statement: the program is safe & when the main thread
terminates, the postcondition hold. *)
Theorem heap_basic_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ},
{{{ [ map] l v σ, l v }}} e @ s; {{{ v, RET v; ⌜φ v }}}%I)
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply (heap_adequacy Σ). iIntros (?) "Hall".
iApply (Hwp with "Hall"). iIntros "!>" (v) "Hφ".
iMod (fupd_intro_mask' ) as "H"; first done.
iModIntro. iDestruct "Hφ" as %Hφ. by iIntros "!>" (σ' Qs) "_".
Qed.
(** Adequacy for correct usage of resources: when all threads terminate, and the
post-condition exactly characterizes the heap, we know that the heap is in
fact of the given shape. *)
Theorem heap_all_adequacy Σ `{heapPreG Σ} s e σ1 σ2 σ2' v vs φ :
( `{heapG Σ},
([ map] l v σ1, l v)
WP e @ s; {{ v, ([ map] l v σ2, l v) ⌜φ v }}%I )
rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2')
σ2' = σ2.
Proof.
(* TODO: refactor this proof so we don't have the two cases *)
destruct (decide (σ1 = )) as [->|Heq].
- intros Hwp Hsteps.
eapply (iron_wp_all_adequacy _ heap_lang _ _ σ2' _ _ (λ _, σ2' = σ2) _ ε);
[|done]; iIntros (? κs) "".
iMod (own_alloc ( )) as (γf) "Hf"; first done.
iMod (own_alloc (?{1} (to_heap ) (?{1/2} (to_heap ) ?{1/2} ε)))
as (γ) "[Hσ [Hσ' Hp]]".
{ rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
apply vfrac_auth_valid; by apply to_heap_valid. }
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _.
iFrame "Hp"; iExists ([ map] l v σ2, l v)%I. iSplitL "Hσ Hf".
{ iExists . rewrite /= to_heap_empty fmap_empty big_opM_empty. by iFrame. }
iPoseProof (Hwp _) as "Hwp"; clear Hwp.
iDestruct ("Hwp" with "[]") as "Hwp'".
{ rewrite big_opM_empty fracPred_at_emp; auto. }
iApply (iron_wp_wand with "Hwp'"); iIntros (v' π) "[Hσ2 _] /=".
iExists π, ε; iSplit; first (by rewrite left_id_L right_id_L).
iFrame "Hσ2". iModIntro; iSplit; first done.
iIntros (π1 π2 Hπ) "Hσ2' HQs Hp' Hσ2". rewrite to_heap_empty.
iMod (heap_thread_adequacy _ _ _ (1/2 + π1)%Qp
with "Hσ2' [HQs] [Hσ' Hp'] Hσ2") as "$".
{ by rewrite -frac_op' cmra_op_opM_assoc_L -Hπ frac_op' Qp_div_2. }
{ by iApply big_sepL_replicate. }
{ by iSplitL "Hσ'". }
iMod (fupd_intro_mask' ) as "_"; auto.
- intros Hwp Hsteps.
eapply (iron_wp_all_adequacy _ heap_lang _ _ σ1 σ2' _ _ (λ _, σ2' = σ2) _
(Some (1 / 2)%Qp)); [|done]; iIntros (? κs) "".
iMod (own_alloc ( )) as (γf) "Hf"; first done.
iMod (own_alloc (?{1} (to_heap σ1) (?{1/2} (to_heap σ1) ?{1/2} ε)))
as (γ) "[Hσ [Hσ' Hp]]".
{ rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
apply vfrac_auth_valid; by apply to_heap_valid. }
iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _.
iFrame "Hp"; iExists ([ map] l v σ2, l v)%I. iSplitL "Hσ Hf".
{ iExists . rewrite /= fmap_empty big_opM_empty. by iFrame. }
iPoseProof (Hwp _) as "Hwp"; clear Hwp.
iDestruct ("Hwp" with "[Hσ']") as "Hwp'"; first by iApply big_mapsto_alt_2.
iApply (iron_wp_wand with "Hwp'"). iIntros (v' π) "[Hσ2 _]".
iExists π, ε; iSplit; first (erewrite left_id_L, right_id_L; auto; apply _).
iFrame "Hσ2". iModIntro; iSplit; first done.
iIntros (π1 π2 Hπ) "Hσ2' HQs Hp' Hσ2".
iMod (heap_thread_adequacy with "Hσ2' [HQs] Hp' Hσ2") as "$".
{ by rewrite -Hπ /= frac_op' Qp_div_2. }
{ by iApply big_sepL_replicate. }
iMod (fupd_intro_mask' ) as "_"; auto.
Qed.
This diff is collapsed.
This diff is collapsed.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma twp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E [{ v, v = #true Φ #() }] - WP assert: e @ E [{ Φ }].
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} - WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
(* bag.v: this formalizes the bag example not used in the paper.
* It, in particular, includes operations for creating a new bag, insertion,
* removal, and disposal of the entire bag. The specifications for these
* operations is given by [new_bag_spec], [insert_spec], [remove_spec],
* and [dispose_spec].
*)
From iron.heap_lang Require Export lang.
From iron.heap_lang Require Import proofmode notation.
From iron.heap_lang.lib Require Import spin_lock list.
Set Default Proof Using "Type".
Definition new_bag : val := λ: <>,
(ref (new_list #()), new_lock #()).
Definition insert : val := λ: "bag" "u",
let: "lock" := Snd "bag" in
acquire "lock";;
let: "list" := ! (Fst "bag") in
Fst "bag" <- (cons "u" "list");;
release "lock".
Definition remove : val := λ: "bag",
let: "lock" := Snd "bag" in
acquire "lock";;
let: "list" := !(Fst "bag") in
let: "p" := remove "list" in
Fst "bag" <- Snd "p";;
release "lock";;
Fst "p".
Definition dispose : val := λ: "bag" "f",
let: "lock" := Snd "bag" in
free "lock";;
let: "list" := !(Fst "bag") in
Free (Fst "bag");;
delete_all "f" "list".
Definition bag_inv `{!heapG Σ} (v : val) (Ψ : val ironProp Σ) : ironProp Σ :=
( (k : loc) (l : val) (vs : list val),
v = #k k l is_list Ψ l vs)%I.
Definition is_bag `{!heapG Σ, !lockG Σ} (N : namespace)
(γ : lock_name) (v : val) (p : frac) (Ψ : val ironProp Σ) : ironProp Σ:=
( v1 v2, v = (v1, v2)%V is_lock N γ v2 p (bag_inv v1 Ψ))%I.
Section proofs.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Context (Ψ : val ironProp Σ) `{HΨ : v : val, Uniform (Ψ v)}.
Lemma into_bag_inv l v ws : l v - is_list Ψ v ws - bag_inv #l Ψ.
Proof. iIntros "H1 H2"; iExists _, _, _; iFrame; eauto. Qed.
Global Instance is_bag_fractional γ b : Fractional (λ p, is_bag N γ b p Ψ).
Proof.
intros p1 p2. iSplit.
- iDestruct 1 as (k l ->) "[H1 H2]".
iSplitL "H1"; iExists _, _; iFrame; eauto.
- iIntros "[H1 H2]".
iDestruct "H1" as (k1 l1 ->) "H1".
iDestruct "H2" as (k2 l2 ?) "H2"; simplify_eq/=.
iExists _, _; iSplit; eauto. by iSplitL "H1".
Qed.
Global Instance is_bag_as_fractional γ b p :
AsFractional (is_bag N γ b p Ψ) (λ p, is_bag N γ b p Ψ) p.
Proof. split. done. apply _. Qed.
Local Instance bag_inv_uniform v : Uniform (bag_inv v Ψ).
Proof using HΨ. rewrite /bag_inv; apply _. Qed.
Theorem new_bag_spec :
{{{ emp }}} new_bag #() {{{ b γ, RET b; is_bag N γ b 1 Ψ }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (new_list_spec Ψ with "[//]"); iIntros (l) "Hlist".
wp_alloc k as "Hk".
iDestruct (into_bag_inv with "Hk Hlist") as "Hlist".
wp_apply (new_lock_spec with "Hlist"); iIntros (lk γ) "Hlock".
iApply iron_wp_value. iApply "HΦ". rewrite /is_bag; eauto.
Qed.
Theorem insert_spec γ b v p :
{{{ is_bag N γ b p Ψ Ψ v }}}
insert b v
{{{ RET #(); is_bag N γ b p Ψ }}}.
Proof using HΨ.
iIntros (Φ) "[Hbag HΨ] HΦ". do 2 wp_lam.
iDestruct "Hbag" as (v1 v2 ->) "Hlock".
wp_proj. wp_lam.
wp_apply (acquire_spec with "Hlock"); iIntros "(Hlock & Hlocked & Hbag)".
wp_let. wp_proj.
iDestruct "Hbag" as (k l xs ->) "[Hk Hlist]".
wp_load. wp_let. wp_proj.
wp_apply (cons_spec with "[$Hlist $HΨ]"); iIntros (l') "Hlist".
wp_store.
wp_apply (release_spec with "[$Hlock $Hlocked Hk Hlist]").
{ iApply (into_bag_inv with "Hk Hlist"). }
iIntros "Hlock". iApply "HΦ". rewrite /is_bag; auto.
Qed.
Theorem remove_spec γ b p :
{{{ is_bag N γ b p Ψ }}}
remove b
{{{ v, RET v;
(v = NONEV is_bag N γ b p Ψ)
( v', v = SOMEV v' Ψ v' is_bag N γ b p Ψ) }}}.
Proof using HΨ.
iIntros (Φ) "Hbag HΦ". wp_lam.
iDestruct "Hbag" as (v v ->) "Hlock".
wp_proj. wp_lam.
wp_apply (acquire_spec with "Hlock"); iIntros "(Hlock & Hlocked & Hbag)".
wp_let. wp_proj.
iDestruct "Hbag" as (k l xs ->) "[Hk Hlist]".
wp_load. wp_let.
destruct xs as [|xs].