Commit e6c82af6 authored by Ralf Jung's avatar Ralf Jung

Add poison

parent 6096219f
......@@ -297,19 +297,18 @@ Section heap.
- rewrite is_Some_alt inter_lookup_None; lia.
Qed.
Lemma heap_freeable_rel_init_mem l h vl σ:
vl []
Lemma heap_freeable_rel_init_mem l h n σ:
n O
( m : Z, σ !! (l + m) = None)
heap_freeable_rel σ h
heap_freeable_rel (init_mem l vl σ)
(<[l.1 := (1%Qp, inter (l.2) (length vl))]> h).
heap_freeable_rel (init_mem l n σ)
(<[l.1 := (1%Qp, inter (l.2) n)]> h).
Proof.
move=> Hvlnil FRESH REL blk qs /lookup_insert_Some [[<- <-]|[??]].
- split.
{ destruct vl as [|v vl]; simpl in *; [done|]. apply: insert_non_empty. }
intros i. destruct (decide (l.2 i i < l.2 + length vl)).
+ rewrite inter_lookup_Some //.
destruct (lookup_init_mem_Some σ l (l.1, i) vl); naive_solver.
{ destruct n as [|n]; simpl in *; [done|]. apply: insert_non_empty. }
intros i. destruct (decide (l.2 i i < l.2 + n)).
+ rewrite inter_lookup_Some // lookup_init_mem; naive_solver.
+ rewrite inter_lookup_None; last lia. rewrite lookup_init_mem_ne /=; last lia.
replace (l.1,i) with (l + (i - l.2)) by (rewrite /shift_loc; f_equal; lia).
by rewrite FRESH !is_Some_alt.
......@@ -337,15 +336,15 @@ Section heap.
Qed.
(** Weakest precondition *)
Lemma heap_alloc_vs σ l vl :
Lemma heap_alloc_vs σ l n :
( m : Z, σ !! (l + m) = None)
own heap_name ( to_heap σ)
== own heap_name ( to_heap (init_mem l vl σ))
own heap_name ( [^op list] i v vl,
== own heap_name ( to_heap (init_mem l n σ))
own heap_name ( [^op list] i v (repeat (LitV LitPoison) n),
{[l + i := (1%Qp, Cinr 0%nat, to_agree v)]}).
Proof.
intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
revert l FREE. induction vl as [|v vl IH]=> l FRESH; [done|].
revert l FREE. induction n as [|n IH]=> l FRESH; [done|].
rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
etrans; first apply (IH (l + 1)).
{ intros. by rewrite shift_loc_assoc. }
......@@ -357,16 +356,16 @@ Section heap.
rewrite lookup_init_mem_ne /=; last lia. by rewrite -(shift_loc_0 l) FRESH.
Qed.
Lemma heap_alloc σ l n vl :
Lemma heap_alloc σ l n :
0 < n
( m, σ !! (l + m) = None)
Z.of_nat (length vl) = n
heap_ctx σ ==
heap_ctx (init_mem l vl σ) l(Z.to_nat n) l ↦∗ vl.
heap_ctx (init_mem l (Z.to_nat n) σ) l(Z.to_nat n)
l ↦∗ repeat (LitV LitPoison) (Z.to_nat n).
Proof.
intros ?? HvlLen; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
assert (vl []) by (intros ->; simpl in *; lia).
iMod (heap_alloc_vs _ _ vl with "[$Hvalσ]") as "[Hvalσ Hmapsto]"; first done.
intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
assert (Z.to_nat n O). { rewrite -(Nat2Z.id 0)=>/Z2Nat.inj. lia. }
iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ Hmapsto]"; first done.
iMod (own_update _ ( hF) with "HhF") as "[HhF Hfreeable]".
{ apply auth_update_alloc,
(alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
......@@ -374,9 +373,9 @@ Section heap.
- split. done. apply inter_valid. }
iModIntro. iSplitL "Hvalσ HhF".
{ iExists _. iFrame. iPureIntro.
rewrite -HvlLen Nat2Z.id. auto using heap_freeable_rel_init_mem. }
auto using heap_freeable_rel_init_mem. }
rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //.
iFrame.
iFrame. destruct (Z.to_nat n); done.
Qed.
Lemma heap_free_vs σ l vl :
......
......@@ -14,7 +14,7 @@ Delimit Scope loc_scope with L.
Open Scope loc_scope.
Inductive base_lit : Set :=
| LitUnit | LitLoc (l : loc) | LitInt (n : Z).
| LitPoison | LitLoc (l : loc) | LitInt (n : Z).
Inductive bin_op : Set :=
| PlusOp | MinusOp | LeOp | EqOp | OffsetOp.
Inductive order : Set :=
......@@ -190,6 +190,8 @@ Proof.
Qed.
(** The stepping relation *)
(* Be careful to make sure that poison is always stuck when used for anything
except for reading from or writing to memory! *)
Definition Z_of_bool (b : bool) : Z :=
if b then 1 else 0.
......@@ -201,10 +203,10 @@ Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
Notation "l +ₗ z" := (shift_loc l%L z%Z)
(at level 50, left associativity) : loc_scope.
Fixpoint init_mem (l:loc) (init:list val) (σ:state) : state :=
match init with
| [] => σ
| inith :: initq => <[l:=(RSt 0, inith)]>(init_mem (l + 1) initq σ)
Fixpoint init_mem (l:loc) (n:nat) (σ:state) : state :=
match n with
| O => σ
| S n => <[l:=(RSt 0, LitV LitPoison)]>(init_mem (l + 1) n σ)
end.
Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
......@@ -214,6 +216,7 @@ Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
end.
Inductive lit_eq (σ : state) : base_lit base_lit Prop :=
(* No refl case for poison *)
| IntRefl z : lit_eq σ (LitInt z) (LitInt z)
| LocRefl l : lit_eq σ (LitLoc l) (LitLoc l)
(* Comparing unallocated pointers can non-deterministically say they are equal
......@@ -282,7 +285,7 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
to_val e = Some v
σ !! l = Some (RSt 0, v')
head_step (Write ScOrd (Lit $ LitLoc l) e) σ
(Lit LitUnit) (<[l:=(RSt 0, v)]>σ)
(Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
[]
| WriteNa1S l e v v' σ:
to_val e = Some v
......@@ -294,7 +297,7 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
to_val e = Some v
σ !! l = Some (WSt, v')
head_step (Write Na2Ord (Lit $ LitLoc l) e) σ
(Lit LitUnit) (<[l:=(RSt 0, v)]>σ)
(Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
[]
| CasFailS l n e1 lit1 e2 lit2 litl σ :
to_val e1 = Some $ LitV lit1 to_val e2 = Some $ LitV lit2
......@@ -329,24 +332,23 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
head_step (CAS (Lit $ LitLoc l) e1 e2) σ
stuck_term σ
[]
| AllocS n l init σ :
| AllocS n l σ :
0 < n
( m, σ !! (l + m) = None)
Z.of_nat (length init) = n
head_step (Alloc $ Lit $ LitInt n) σ
(Lit $ LitLoc l) (init_mem l init σ) []
(Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) []
| FreeS n l σ :
0 < n
( m, is_Some (σ !! (l + m)) 0 m < n)
head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
(Lit LitUnit) (free_mem l (Z.to_nat n) σ)
(Lit LitPoison) (free_mem l (Z.to_nat n) σ)
[]
| CaseS i el e σ :
0 i
el !! (Z.to_nat i) = Some e
head_step (Case (Lit $ LitInt i) el) σ e σ []
| ForkS e σ:
head_step (Fork e) σ (Lit LitUnit) σ [e].
head_step (Fork e) σ (Lit LitPoison) σ [e].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......@@ -421,35 +423,23 @@ Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
Lemma shift_loc_block l n : (l + n).1 = l.1.
Proof. done. Qed.
Lemma lookup_init_mem σ (l l' : loc) vl :
l.1 = l'.1 l.2 l'.2 < l.2 + length vl
init_mem l vl σ !! l' = (RSt 0,) <$> vl !! Z.to_nat (l'.2 - l.2).
Lemma lookup_init_mem σ (l l' : loc) (n : nat) :
l.1 = l'.1 l.2 l'.2 < l.2 + n
init_mem l n σ !! l' = Some (RSt 0, LitV LitPoison).
Proof.
intros ?. destruct l' as [? n]; simplify_eq/=.
revert n l. induction vl as [|v vl IH]=> /= n l Hl; [lia|].
assert (n = l.2 l.2 + 1 n) as [->|?] by lia.
{ by rewrite -surjective_pairing lookup_insert Z.sub_diag. }
intros ?. destruct l' as [? l']; simplify_eq/=.
revert l. induction n as [|n IH]=> /= l Hl; [lia|].
assert (l' = l.2 l.2 + 1 l') as [->|?] by lia.
{ by rewrite -surjective_pairing lookup_insert. }
rewrite lookup_insert_ne; last by destruct l; intros ?; simplify_eq/=; lia.
rewrite -(shift_loc_block l 1) IH /=; last lia.
cut (Z.to_nat (n - l.2) = S (Z.to_nat (n - (l.2 + 1)))); [by intros ->|].
rewrite -Z2Nat.inj_succ; last lia. f_equal; lia.
Qed.
Lemma lookup_init_mem_Some σ (l l' : loc) vl :
l.1 = l'.1 l.2 l'.2 < l.2 + length vl v,
vl !! Z.to_nat (l'.2 - l.2) = Some v
init_mem l vl σ !! l' = Some (RSt 0,v).
Proof.
intros. destruct (lookup_lt_is_Some_2 vl (Z.to_nat (l'.2 - l.2))) as [v Hv].
{ rewrite -(Nat2Z.id (length vl)). apply Z2Nat.inj_lt; lia. }
exists v. by rewrite lookup_init_mem ?Hv.
rewrite -(shift_loc_block l 1) IH /=; last lia. done.
Qed.
Lemma lookup_init_mem_ne σ (l l' : loc) vl :
l.1 l'.1 l'.2 < l.2 l.2 + length vl l'.2
init_mem l vl σ !! l' = σ !! l'.
Lemma lookup_init_mem_ne σ (l l' : loc) (n : nat) :
l.1 l'.1 l'.2 < l.2 l.2 + n l'.2
init_mem l n σ !! l' = σ !! l'.
Proof.
revert l. induction vl as [|v vl IH]=> /= l Hl; auto.
revert l. induction n as [|n IH]=> /= l Hl; auto.
rewrite -(IH (l + 1)); last (simpl; intuition lia).
apply lookup_insert_ne. intros ->; intuition lia.
Qed.
......@@ -472,11 +462,10 @@ Lemma alloc_fresh n σ :
let l := (fresh_block σ, 0) in
let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in
0 < n
head_step (Alloc $ Lit $ LitInt n) σ (Lit $ LitLoc l) (init_mem l init σ) [].
head_step (Alloc $ Lit $ LitInt n) σ (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
Proof.
intros l init Hn. apply AllocS. auto.
- intros i. apply (is_fresh_block _ i).
- rewrite repeat_length Z2Nat.id; lia.
Qed.
Lemma lookup_free_mem_ne σ l l' n : l.1 l'.1 free_mem l n σ !! l' = σ !! l'.
......@@ -622,8 +611,8 @@ Proof.
refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
......@@ -657,8 +646,8 @@ Notation Seq e1 e2 := (Let BAnon e1 e2).
Notation LamV xl e := (RecV BAnon xl e).
Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Skip := (Seq (Lit LitPoison) (Lit LitPoison)).
Coercion lit_of_bool : bool >-> base_lit.
Notation If e0 e1 e2 := (Case e0 (@cons expr e2 (@cons expr e1 (@nil expr)))).
Notation Newlft := (Lit LitUnit) (only parsing).
Notation Newlft := (Lit LitPoison) (only parsing).
Notation Endlft := Skip (only parsing).
......@@ -38,12 +38,12 @@ Definition weak_count : val :=
Definition clone_arc : val :=
rec: "clone" ["l"] :=
let: "strong" := !ˢᶜ"l" in
if: CAS "l" "strong" ("strong" + #1) then #() else "clone" ["l"].
if: CAS "l" "strong" ("strong" + #1) then # else "clone" ["l"].
Definition clone_weak : val :=
rec: "clone" ["l"] :=
let: "weak" := !ˢᶜ("l" + #1) in
if: CAS ("l" + #1) "weak" ("weak" + #1) then #() else "clone" ["l"].
if: CAS ("l" + #1) "weak" ("weak" + #1) then # else "clone" ["l"].
Definition downgrade : val :=
rec: "downgrade" ["l"] :=
......@@ -52,7 +52,7 @@ Definition downgrade : val :=
(* -1 in weak indicates that somebody locked the counts; let's spin. *)
"downgrade" ["l"]
else
if: CAS ("l" + #1) "weak" ("weak" + #1) then #()
if: CAS ("l" + #1) "weak" ("weak" + #1) then #
else "downgrade" ["l"].
Definition upgrade : val :=
......@@ -151,7 +151,7 @@ Section def.
( (P ={E,}= weak_tok γ (weak_tok γ ={,E}= P)))%I.
Definition drop_spec (drop : val) P : iProp Σ :=
({{{ P P1 1 }}} drop [] {{{ RET #(); P P2 }}})%I.
({{{ P P1 1 }}} drop [] {{{ RET #; P P2 }}})%I.
End def.
Section arc.
......@@ -255,7 +255,7 @@ Section arc.
Lemma clone_arc_spec (γ : gname) (l : loc) (P : iProp Σ) :
is_arc P1 P2 N γ l - arc_tok_acc γ P ( N) -
{{{ P }}} clone_arc [ #l]
{{{ q', RET #(); P arc_tok γ q' P1 q' }}}.
{{{ q', RET #; P arc_tok γ q' P1 q' }}}.
Proof using HP1.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
iInv N as (st) "[>H● H]" "Hclose1".
......@@ -291,7 +291,7 @@ Section arc.
Lemma downgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
is_arc P1 P2 N γ l - arc_tok_acc γ P ( N) -
{{{ P }}} downgrade [ #l] {{{ RET #(); P weak_tok γ }}}.
{{{ P }}} downgrade [ #l] {{{ RET #; P weak_tok γ }}}.
Proof.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iInv N as (st) "[>H● H]" "Hclose1".
......@@ -342,7 +342,7 @@ Section arc.
Lemma clone_weak_spec (γ : gname) (l : loc) (P : iProp Σ) :
is_arc P1 P2 N γ l - weak_tok_acc γ P ( N) -
{{{ P }}} clone_weak [ #l] {{{ RET #(); P weak_tok γ }}}.
{{{ P }}} clone_weak [ #l] {{{ RET #; P weak_tok γ }}}.
Proof.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iAssert ( (P ={,⊤∖↑N}= w : Z, (l + 1) #w
......
......@@ -8,7 +8,7 @@ Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
Definition mklock_locked : val := λ: ["l"], "l" <- #true.
Definition try_acquire : val := λ: ["l"], CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" ["l"] := if: try_acquire ["l"] then #() else "acquire" ["l"].
rec: "acquire" ["l"] := if: try_acquire ["l"] then # else "acquire" ["l"].
Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
(* It turns out that we need an accessor-based spec so that we can put the
......@@ -53,7 +53,7 @@ Section proof.
Qed.
Lemma mklock_unlocked_spec (R : iProp Σ) (l : loc) v :
{{{ l v R }}} mklock_unlocked [ #l ] {{{ RET #(); lock_proto l R }}}.
{{{ l v R }}} mklock_unlocked [ #l ] {{{ RET #; lock_proto l R }}}.
Proof.
iIntros (Φ) "[Hl HR] HΦ". wp_lam. rewrite -wp_fupd. wp_write.
iMod (lock_proto_create with "Hl HR") as "Hproto".
......@@ -61,7 +61,7 @@ Section proof.
Qed.
Lemma mklock_locked_spec (R : iProp Σ) (l : loc) v :
{{{ l v }}} mklock_locked [ #l ] {{{ RET #(); lock_proto l R }}}.
{{{ l v }}} mklock_locked [ #l ] {{{ RET #; lock_proto l R }}}.
Proof.
iIntros (Φ) "Hl HΦ". wp_lam. rewrite -wp_fupd. wp_write.
iMod (lock_proto_create with "Hl [//]") as "Hproto".
......@@ -88,7 +88,7 @@ Section proof.
Lemma acquire_spec E l R P :
(P ={E,}= lock_proto l R ( lock_proto l R ={,E}= P)) -
{{{ P }}} acquire [ #l ] @ E {{{ RET #(); R P }}}.
{{{ P }}} acquire [ #l ] @ E {{{ RET #; R P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
......@@ -98,7 +98,7 @@ Section proof.
Lemma release_spec E l R P :
(P ={E,}= lock_proto l R ( lock_proto l R ={,E}= P)) -
{{{ R P }}} release [ #l ] @ E {{{ RET #(); P }}}.
{{{ R P }}} release [ #l ] @ E {{{ RET #; P }}}.
Proof.
iIntros "#Hproto !# * (HR & HP) HΦ". wp_let.
iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
......
......@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
Definition memcpy : val :=
rec: "memcpy" ["dst";"len";"src"] :=
if: "len" #0 then #()
if: "len" #0 then #
else "dst" <- !"src";;
"memcpy" ["dst" + #1 ; "len" - #1 ; "src" + #1].
......@@ -24,7 +24,7 @@ Lemma wp_memcpy `{lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
Z.of_nat (length vl1) = n Z.of_nat (length vl2) = n
{{{ l1 ↦∗ vl1 l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
{{{ RET #(); l1 ↦∗ vl2 l2 ↦∗{q} vl2 }}}.
{{{ RET #; l1 ↦∗ vl2 l2 ↦∗{q} vl2 }}}.
Proof.
iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
......
......@@ -10,7 +10,7 @@ Definition new : val :=
Definition delete : val :=
λ: ["n"; "loc"],
if: "n" #0 then #()
if: "n" #0 then #
else Free "n" "loc".
Section specs.
......@@ -19,21 +19,21 @@ Section specs.
Lemma wp_new E n:
0 n
{{{ True }}} new [ #n ] @ E
{{{ l vl, RET LitV $ LitLoc l;
n = length vl (l(Z.to_nat n) n = 0) l ↦∗ vl }}}.
{{{ l, RET LitV $ LitLoc l;
(l(Z.to_nat n) n = 0) l ↦∗ repeat (LitV LitPoison) (Z.to_nat n) }}}.
Proof.
iIntros (? Φ) "_ HΦ". wp_lam. wp_op; intros ?.
- wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
- wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
rewrite heap_mapsto_vec_nil. auto.
- wp_if. wp_alloc l vl as "H↦" "H†". iApply ("HΦ" $! _ vl).
rewrite vec_to_list_length -{2}Hsz Z2Nat.id //. iFrame. auto.
- wp_if. wp_alloc l as "H↦" "H†". iApply "HΦ". subst sz.
iFrame. auto.
Qed.
Lemma wp_delete E (n:Z) l vl :
n = length vl
{{{ l ↦∗ vl (l(length vl) n = 0) }}}
delete [ #n; #l] @ E
{{{ RET LitV LitUnit; True }}}.
{{{ RET #; True }}}.
Proof.
iIntros (? Φ) "(H↦ & [H†|%]) HΦ";
wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
......
......@@ -16,7 +16,7 @@ Definition finish : val :=
λ: ["c"; "v"],
"c" + #1 <- "v";; (* Store data (non-atomically). *)
"c" <-ˢᶜ #1;; (* Signal that we finished (atomically!) *)
#().
#.
Definition join : val :=
rec: "join" ["c"] :=
if: !ˢᶜ"c" then
......@@ -67,11 +67,11 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
spawn [e] {{{ c, RET #c; join_handle c Ψ }}}.
Proof.
iIntros (<-%of_to_val Φ) "Hf HΦ". rewrite /spawn /=.
wp_let. wp_alloc l vl as "Hl" "H†". wp_let. inv_vec vl=>v0 v1.
wp_let. wp_alloc l as "Hl" "H†". wp_let.
iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done.
iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hl" as "[Hc Hd]". wp_write. clear v0.
iDestruct "Hl" as "[Hc Hd]". wp_write.
iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".
{ iNext. iRight. iExists false. auto. }
wp_apply (wp_fork with "[Hγf Hf Hd]").
......@@ -81,7 +81,7 @@ Proof.
Qed.
Lemma finish_spec (Ψ : val iProp Σ) c v :
{{{ finish_handle c Ψ Ψ v }}} finish [ #c; v] {{{ RET #(); True }}}.
{{{ finish_handle c Ψ Ψ v }}} finish [ #c; v] {{{ RET #; True }}}.
Proof.
iIntros (Φ) "[Hfin HΨ] HΦ". iDestruct "Hfin" as (γf γj v0) "(Hf & Hd & #?)".
wp_lam. wp_op. wp_write.
......
......@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
Definition swap : val :=
rec: "swap" ["p1";"p2";"len"] :=
if: "len" #0 then #()
if: "len" #0 then #
else let: "x" := !"p1" in
"p1" <- !"p2";;
"p2" <- "x";;
......@@ -15,7 +15,7 @@ Lemma wp_swap `{lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
Z.of_nat (length vl1) = n Z.of_nat (length vl2) = n
{{{ l1 ↦∗ vl1 l2 ↦∗ vl2 }}}
swap [ #l1; #l2; #n] @ E
{{{ RET #(); l1 ↦∗ vl2 l2 ↦∗ vl1 }}}.
{{{ RET #; l1 ↦∗ vl2 l2 ↦∗ vl1 }}}.
Proof.
iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
......
......@@ -44,22 +44,21 @@ Proof. exact: weakestpre.wp_bind. Qed.
Lemma wp_alloc E (n : Z) :
0 < n
{{{ True }}} Alloc (Lit $ LitInt n) @ E
{{{ l sz (vl : vec val sz), RET LitV $ LitLoc l; n = sz l(Z.to_nat n) l ↦∗ vl }}}.
{{{ l (sz: nat), RET LitV $ LitLoc l; n = sz lsz l ↦∗ repeat (LitV LitPoison) sz }}}.
Proof.
iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
iModIntro; iSplit=> //. iFrame.
iApply ("HΦ" $! _ _ (list_to_vec init)).
rewrite vec_to_list_of_list. auto.
iApply ("HΦ" $! _ (Z.to_nat n)). iFrame. iPureIntro. rewrite Z2Nat.id; lia.
Qed.
Lemma wp_free E (n:Z) l vl :
n = length vl
{{{ l ↦∗ vl l(length vl) }}}
Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
{{{ RET LitV LitUnit; True }}}.
{{{ RET LitV LitPoison; True }}}.
Proof.
iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ".
......@@ -101,7 +100,7 @@ Qed.
Lemma wp_write_sc E l e v v' :
to_val e = Some v
{{{ l v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
{{{ RET LitV LitUnit; l v }}}.
{{{ RET LitV LitPoison; l v }}}.
Proof.
iIntros (<-%of_to_val Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
......@@ -114,7 +113,7 @@ Qed.
Lemma wp_write_na E l e v v' :
to_val e = Some v
{{{ l v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
{{{ RET LitV LitUnit; l v }}}.
{{{ RET LitV LitPoison; l v }}}.
Proof.
iIntros (<-%of_to_val Φ) ">Hv HΦ".
iApply wp_lift_head_step; auto. iIntros (σ1) "Hσ".
......@@ -145,7 +144,7 @@ Proof.
Qed.
Lemma wp_cas_suc E l lit1 e2 lit2 :
to_val e2 = Some (LitV lit2) lit1 LitUnit
to_val e2 = Some (LitV lit2) lit1 LitPoison
{{{ l LitV lit1 }}}
CAS (Lit $ LitLoc l) (Lit lit1) e2 @ E
{{{ RET LitV (LitInt 1); l LitV lit2 }}}.
......@@ -211,7 +210,7 @@ Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e :
{{{ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitUnit; True }}}.
{{{ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
Proof.
iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
by intros; inv_head_step; eauto. iApply step_fupd_intro; first done. iNext.
......@@ -446,7 +445,7 @@ Lemma wp_seq E e1 e2 v Φ :
WP e2 @ E {{ Φ }} - WP Seq e1 e2 @ E {{ Φ }}.
Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
Lemma wp_skip E Φ : Φ (LitV LitUnit) - WP Skip @ E {{ Φ }}.
Lemma wp_skip E Φ : Φ (LitV LitPoison) - WP Skip @ E {{ Φ }}.
Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
End lifting.
......@@ -29,7 +29,7 @@ Notation "'case:' e0 'of' el" := (Case e0%E el%E)
(at level 102, e0, el at level 150) : expr_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(only parsing, at level 102, e1, e2, e3 at level 150) : expr_scope.
Notation "()" := LitUnit : val_scope.
Notation "☠" := LitPoison : val_scope.
Notation "! e" := (Read Na1Ord e%E) (at level 9, format "! e") : expr_scope.
Notation "!ˢᶜ e" := (Read ScOrd e%E) (at level 9, format "!ˢᶜ e") : expr_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
......
......@@ -154,8 +154,8 @@ Implicit Types Δ : envs (iResUR Σ).
Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
0 < n
IntoLaterNEnvs 1 Δ Δ'
( l sz (vl : vec val sz), n = sz Δ'',
envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (l(Z.to_nat n))) Δ'
( l (sz: nat), n = sz Δ'',
envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ repeat (LitV LitPoison) sz)) j2 (lsz)) Δ'
= Some Δ''
(Δ'' Φ (LitV $ LitLoc l)))
Δ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
......@@ -163,9 +163,9 @@ Proof.
intros ?? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
rewrite -and_sep_l. apply and_intro; first done.
rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
apply forall_intro=>sz. apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
destruct (HΔ l _ vl) as (Δ''&?&HΔ'); first done.
destruct (HΔ l sz) as (Δ''&?&HΔ'); first done.
rewrite envs_app_sound //; simpl. by rewrite right_id HΔ' -fupd_intro.
Qed.
......@@ -177,7 +177,7 @@ Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
envs_lookup i2 Δ'' = Some (false, ln')%I
envs_delete i2 false Δ'' = Δ'''
n' = length vl
(Δ''' Φ (LitV LitUnit))
(Δ''' Φ (LitV LitPoison))
Δ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
Proof.
intros -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
......@@ -209,7 +209,7 @@ Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
(Δ'' Φ (LitV LitUnit))
(Δ'' Φ (LitV LitPoison))
Δ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
Proof.
intros ? [->| ->] ????.
......@@ -230,7 +230,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
| _ => fail "wp_apply: not a 'wp'"
end.
Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q =>
......@@ -242,7 +242,7 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
[try fast_done
|apply _
|let sz := fresh "sz" in let Hsz := fresh "Hsz" in
first [intros l sz vl Hsz | fail 1 "wp_alloc:" l "or" vl "not fresh"];
first [intros l sz Hsz | fail 1 "wp_alloc:" l "not fresh"];
(* If Hsz is "constant Z = nat", change that to an equation on nat and
potentially substitute away the sz. *)
try (match goal with Hsz : ?x = _ |- _ => rewrite <-(Z2Nat.id x) in Hsz; last done end;
......@@ -257,8 +257,8 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
| _ => fail "wp_alloc: not a 'wp'"
end.
Tactic Notation "wp_alloc" ident(l) ident(vl) :=
let H := iFresh in let Hf := iFresh in wp_alloc l vl as H Hf.
Tactic Notation "wp_alloc" ident(l) :=
let H := iFresh in let Hf := iFresh in wp_alloc l as H Hf.
Tactic Notation "wp_free" :=
iStartProof;
......
......@@ -258,7 +258,7 @@ Section typing.
Proof.
iIntros (HE [k' Hk']) "#LFT #HE Htl HL Hκs Hf Hargs Hk". rewrite -(of_to_val k k') //.
clear dependent k. wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
iApply (wp_app_vec _ _ (_::_) ((λ v, v = (λ: ["_r"], (#() ;; #()) ;; k' ["_r"])%V):::
iApply (wp_app_vec _ _ (_::_) ((λ v, v = (λ: ["_r"], (# ;; #) ;; k' ["_r"])%V):::
vmap (λ ty (v : val), tctx_elt_interp tid (v box ty)) (fp x).(fp_tys))%I
with "[Hargs]"); first wp_done.
- rewrite /=. iSplitR "Hargs".
......@@ -385,8 +385,8 @@ Section typing.
intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
- iIntros (k).
(* TODO : make [simpl_subst] work here. *)
change (subst' "_k" k (p ((λ: ["_r"], (#() ;; #()) ;; "_k" ["_r"])%E :: ps))) with
((subst "_k" k p) ((λ: ["_r"], (#() ;; #()) ;; k ["_r"])%E :: map (subst "_k" k) ps)).
change (subst' "_k" k (p ((λ: ["_r"], (# ;; #) ;; "_k" ["_r"])%E :: ps))) with
((subst "_k" k p) ((λ: ["_r"], (# ;; #) ;; k ["_r"])%E :: map (subst "_k" k) ps)).
rewrite is_closed_nil_subst //.
assert (map (subst "_k" k) ps = ps) as ->.
{ clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
......
......@@ -738,8 +738,8 @@ Section arc.
"r" <-{ty.(ty_size),Σ some} !("arc'" + #2);;
if: drop_weak ["arc'"] then
delete [ #(2 + ty.(ty_size)); "arc'" ]
else #()
else #());;
else #
else #);;
delete [ #1; "arc"];; return: ["r"].
Lemma arc_drop_type ty `{!TyWf ty} :
......@@ -800,7 +800,7 @@ Section arc.
let: "r" := new [ #0] in
let: "arc'" := !"arc" in
(if: drop_weak ["arc'"] then delete [ #(2 + ty.(ty_size)); "arc'" ]
else #());;
else #);;
delete [ #1; "arc"];; return: ["r"].
Lemma weak_drop_type ty `{!TyWf ty} :
......@@ -840,7 +840,7 @@ Section arc.
"r" <-{ty.(ty_size),Σ 0} !("arc'" + #2);;
(* Decrement the "strong weak reference" *)
(if: drop_weak ["arc'"] then delete [ #(2 + ty.(ty_size)); "arc'" ]