Commit 9f34cfe5 authored by Robbert's avatar Robbert

Merge branch 'atomic_resolve' into 'master'

Resolution of prophecy variables can be attached to atomic expressions

See merge request iris/iris!244
parents 2c926d86 f87db2d2
From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.heap_lang Require Import lang adequacy proofmode notation.
From iris.heap_lang Require Import lang.
Set Default Proof Using "Type".
Section tests.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Definition CAS_resolve e1 e2 e3 p v :=
Resolve (CAS e1 e2 e3) p v.
Lemma wp_cas_suc_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v1 v2 v : val) :
vals_cas_compare_safe v1 v1
{{{ proph p vs l v1 }}}
CAS_resolve #l v1 v2 #p v @ s; E
{{{ RET #true ; vs', vs = (#true, v)::vs' proph p vs' l v2 }}}.
Proof.
iIntros (Hcmp Φ) "[Hp Hl] HΦ".
wp_apply (wp_resolve with "Hp"); first done.
assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
wp_cas_suc. iIntros (vs' ->) "Hp".
iApply "HΦ". eauto with iFrame.
Qed.
Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v' v1 v2 v : val) :
v' v1 vals_cas_compare_safe v' v1
{{{ proph p vs l v' }}}
CAS_resolve #l v1 v2 #p v @ s; E
{{{ RET #false ; vs', vs = (#false, v)::vs' proph p vs' l v' }}}.
Proof.
iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
wp_apply (wp_resolve with "Hp"); first done.
wp_cas_fail. iIntros (vs' ->) "Hp".
iApply "HΦ". eauto with iFrame.
Qed.
Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
l #n -
proph p vs -
WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, v = #true vs, proph p vs l #(n+1) }}%I.
Proof.
iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame.
Qed.
Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) :
proph p vs -
WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, v = #0 vs, proph p vs }}%I.
Proof.
iIntros "Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
wp_pures. iIntros (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame.
Qed.
Lemma test_resolve3 s E (p1 p2 : proph_id) (vs1 vs2 : list (val * val)) (n : Z) :
{{{ proph p1 vs1 proph p2 vs2 }}}
Resolve (Resolve (#n - #n) #p2 #2) #p1 #1 @ s; E
{{{ RET #0 ; vs1' vs2', vs1 = (#0, #1)::vs1' vs2 = (#0, #2)::vs2' proph p1 vs1' proph p2 vs2' }}}.
Proof.
iIntros (Φ) "[Hp1 Hp2] HΦ".
wp_apply (wp_resolve with "Hp1"); first done.
wp_apply (wp_resolve with "Hp2"); first done.
wp_op.
iIntros (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
Qed.
Lemma test_resolve4 s E (p1 p2 : proph_id) (vs1 vs2 : list (val * val)) (n : Z) :
{{{ proph p1 vs1 proph p2 vs2 }}}
Resolve (Resolve (#n - #n) ((λ: "x", "x") #p2) (#0 + #2)) ((λ: "x", "x") #p1) (#0 + #1) @ s; E
{{{ RET #0 ; vs1' vs2', vs1 = (#0, #1)::vs1' vs2 = (#0, #2)::vs2' proph p1 vs1' proph p2 vs2' }}}.
Proof.
iIntros (Φ) "[Hp1 Hp2] HΦ".
wp_apply (wp_resolve with "Hp1"); first done.
wp_apply (wp_resolve with "Hp2"); first done.
wp_op.
iIntros (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
Qed.
End tests.
......@@ -8,10 +8,10 @@ Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ;
heap_preG_proph :> proph_mapPreG proph_id val Σ
heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ
}.
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id val].
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
......
......@@ -14,13 +14,42 @@ Set Default Proof Using "Type".
useless unless the user let-expands [b].
- For prophecy variables, we annotate the reduction steps with an "observation"
and tweak adequacy such that WP knows all future observations. There is
and tweak adequacy such that WP knows all future observations. There is
another possible choice: Use non-deterministic choice when creating a prophecy
variable ([NewProph]), and when resolving it ([ResolveProph]) make the
program diverge unless the variable matches. That, however, requires an
variable ([NewProph]), and when resolving it ([Resolve]) make the
program diverge unless the variable matches. That, however, requires an
erasure proof that this endless loop does not make specifications useless.
*)
The expression [Resolve e p v] attaches a prophecy resolution (for prophecy
variable [p] to value [v]) to the top-level head-reduction step of [e]. The
prophecy resolution happens simultaneously with the head-step being taken.
Furthermore, it is required that the head-step produces a value (otherwise
the [Resolve] is stuck), and this value is also attached to the resolution.
A prophecy variable is thus resolved to a pair containing (1) the result
value of the wrapped expression (called [e] above), and (2) the value that
was attached by the [Resolve] (called [v] above). This allows, for example,
to distinguish a resolution originating from a successful [CAS] from one
originating from a failing [CAS]. For example:
- [Resolve (CAS #l #n #(n+1)) #p v] will behave as [CAS #l #n #(n+1)],
which means step to a boolean [b] while updating the heap, but in the
meantime the prophecy variable [p] will be resolved to [(#b, v)].
- [Resolve (! #l) #p v] will behave as [! #l], that is return the value
[w] pointed to by [l] on the heap (assuming it was allocated properly),
but it will additionally resolve [p] to the pair [(w,v)].
Note that the sub-expressions of [Resolve e p v] (i.e., [e], [p] and [v])
are reduced as usual, from right to left. However, the evaluation of [e]
is restricted so that the head-step to which the resolution is attached
cannot be taken by the context. For example:
- [Resolve (CAS #l #n (#n + #1)) #p v] will first be reduced (with by a
context-step) to [Resolve (CAS #l #n #(n+1) #p v], and then behave as
described above.
- However, [Resolve ((λ: "n", CAS #l "n" ("n" + #1)) #n) #p v] is stuck.
Indeed, it can only be evaluated using a head-step (it is a β-redex),
but the process does not yield a value.
The mechanism described above supports nesting [Resolve] expressions to
attach several prophecy resolutions to a head-redex. *)
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
......@@ -72,7 +101,7 @@ Inductive expr :=
| FAA (e1 : expr) (e2 : expr)
(* Prophecy *)
| NewProph
| ResolveProph (e1 : expr) (e2 : expr)
| Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *)
with val :=
| LitV (l : base_lit)
| RecV (f x : binder) (e : expr)
......@@ -83,7 +112,12 @@ with val :=
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.
Definition observation : Set := proph_id * val.
(** An observation associates a prophecy variable (identifier) to a pair of
values. The first value is the one that was returned by the (atomic) operation
during which the prophecy resolution happened (typically, a boolean when the
wrapped operation is a CAS). The second value is the one that the prophecy
variable was actually resolved to. *)
Definition observation : Set := proph_id * (val * val).
Notation of_val := Val (only parsing).
......@@ -181,8 +215,8 @@ Proof.
| FAA e1 e2, FAA e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| NewProph, NewProph => left _
| ResolveProph e1 e2, ResolveProph e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Resolve e0 e1 e2, Resolve e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| _, _ => right _
end
with gov (v1 v2 : val) {struct v1} : Decision (v1 = v2) :=
......@@ -255,7 +289,7 @@ Proof.
| CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
| FAA e1 e2 => GenNode 17 [go e1; go e2]
| NewProph => GenNode 18 []
| ResolveProph e1 e2 => GenNode 19 [go e1; go e2]
| Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
end
with gov v :=
match v with
......@@ -290,7 +324,7 @@ Proof.
| GenNode 16 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
| GenNode 17 [e1; e2] => FAA (go e1) (go e2)
| GenNode 18 [] => NewProph
| GenNode 19 [e1; e2] => ResolveProph (go e1) (go e2)
| GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
| _ => Val $ LitV LitUnit (* dummy *)
end
with gov v :=
......@@ -347,10 +381,18 @@ Inductive ectx_item :=
| CasRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
| ProphLCtx (v2 : val)
| ProphRCtx (e1 : expr).
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
| ResolveMCtx (e0 : expr) (v2 : val)
| ResolveRCtx (e0 : expr) (e1 : expr).
(** Contextual closure will only reduce [e] in [Resolve e (Val _) (Val _)] if
the local context of [e] is non-empty. As a consequence, the first argument of
[Resolve] is not completely evaluated (down to a value) by contextual closure:
no head steps (i.e., surface reductions) are taken. This means that contextual
closure will reduce [Resolve (CAS #l #n (#n + #1)) #p #v] into [Resolve (CAS
#l #n #(n+1)) #p #v], but it cannot context-step any further. *)
Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx v2 => App e (of_val v2)
| AppRCtx e1 => App e1 e
......@@ -375,8 +417,9 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| CasRCtx e0 e1 => CAS e0 e1 e
| FaaLCtx v2 => FAA e (Val v2)
| FaaRCtx e1 => FAA e1 e
| ProphLCtx v2 => ResolveProph e (of_val v2)
| ProphRCtx e1 => ResolveProph e1 e
| ResolveLCtx K v1 v2 => Resolve (fill_item K e) (Val v1) (Val v2)
| ResolveMCtx ex v2 => Resolve ex e (Val v2)
| ResolveRCtx ex e1 => Resolve ex e1 e
end.
(** Substitution *)
......@@ -403,7 +446,7 @@ Fixpoint subst (x : string) (v : val) (e : expr) : expr :=
| CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
| FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
| NewProph => NewProph
| ResolveProph e1 e2 => ResolveProph (subst x v e1) (subst x v e2)
| Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
end.
Definition subst' (mx : binder) (v : val) : expr expr :=
......@@ -595,30 +638,30 @@ Inductive head_step : expr → state → list observation → expr → state →
[]
(Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ) σ)
[]
| ResolveProphS p v σ :
head_step (ResolveProph (Val $ LitV $ LitProphecy p) (Val v)) σ
[(p, v)]
(Val $ LitV LitUnit) σ [].
| ResolveS p v e σ w σ' κs ts :
head_step e σ κs (Val v) σ' ts
head_step (Resolve e (Val $ LitV $ LitProphecy p) (Val w)) σ
(κs ++ [(p, (v, w))]) (Val v) σ' ts.
(** Basic properties about the language *)
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed.
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
head_step (fill_item Ki e) σ1 κ e2 σ2 efs is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
Proof. revert κ e2. induction Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None to_val e2 = None
fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2.
Proof. destruct Ki1, Ki2; intros; by simplify_eq. Qed.
Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
Lemma alloc_fresh v n σ :
let l := fresh_locs (dom (gset loc) σ.(heap)) n in
......@@ -652,6 +695,47 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
(* Prefer heap_lang names over ectx_language names. *)
Export heap_lang.
(* The following lemma is not provable using the axioms of [ectxi_language].
The proof requires a case analysis over context items ([destruct i] on the
last line), which in all cases yields a non-value. To prove this lemma for
[ectxi_language] in general, we would require that a term of the form
[fill_item i e] is never a value. *)
Lemma to_val_fill_some K e v : to_val (fill K e) = Some v K = [] e = Val v.
Proof.
intro H. destruct K as [|Ki K]; first by apply of_to_val in H. exfalso.
assert (to_val e None) as He.
{ intro A. by rewrite fill_not_val in H. }
assert ( w, e = Val w) as [w ->].
{ destruct e; try done; eauto. }
assert (to_val (fill (Ki :: K) (Val w)) = None).
{ destruct Ki; simpl; apply fill_not_val; done. }
by simplify_eq.
Qed.
Lemma prim_step_to_val_is_head_step e σ1 κs w σ2 efs :
prim_step e σ1 κs (Val w) σ2 efs head_step e σ1 κs (Val w) σ2 efs.
Proof.
intro H. destruct H as [K e1 e2 H1 H2].
assert (to_val (fill K e2) = Some w) as H3; first by rewrite -H2.
apply to_val_fill_some in H3 as [-> ->]. subst e. done.
Qed.
Lemma irreducible_resolve e v1 v2 σ :
irreducible e σ irreducible (Resolve e (Val v1) (Val v2)) σ.
Proof.
intros H κs ** [Ks e1' e2' Hfill -> step]. simpl in *.
induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
- subst e1'. inversion step. eapply H. by apply head_prim_step.
- rewrite fill_app /= in Hfill.
destruct K; (inversion Hfill; subst; clear Hfill; try
match goal with | H : Val ?v = fill Ks ?e |- _ =>
(assert (to_val (fill Ks e) = Some v) as HEq by rewrite -H //);
apply to_val_fill_some in HEq; destruct HEq as [-> ->]; inversion step
end).
apply (H κs (fill_item K (foldl (flip fill_item) e2' Ks)) σ' efs).
econstructor 1 with (K := Ks ++ [K]); last done; simpl; by rewrite fill_app.
Qed.
(** Define some derived forms. *)
Notation Lam x e := (Rec BAnon x e) (only parsing).
Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
......@@ -665,3 +749,5 @@ Notation Alloc e := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
(* Skip should be atomic, we sometimes open invariants around
it. Hence, we need to explicitly use LamV instead of e.g., Seq. *)
Notation Skip := (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUnit)).
Notation ResolveProph e1 e2 := (Resolve Skip e1 e2) (only parsing).
......@@ -61,10 +61,10 @@ Section coinflip.
iModIntro. wp_seq. done.
Qed.
Definition val_list_to_bool (v : list val) : bool :=
match v with
| LitV (LitBool b) :: _ => b
| _ => true
Definition extract_bool (l : list (val * val)) : bool :=
match l with
| (_, LitV (LitBool b)) :: _ => b
| _ => true
end.
Lemma lateChoice_spec (x: loc) :
......@@ -81,7 +81,7 @@ Section coinflip.
iMod "AU" as "[Hl [_ Hclose]]".
iDestruct "Hl" as (v') "Hl".
wp_store.
iMod ("Hclose" $! (val_list_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
iMod ("Hclose" $! (extract_bool v) with "[Hl]") as "HΦ"; first by eauto.
iModIntro. wp_apply rand_spec; try done.
iIntros (b') "_".
wp_apply (wp_resolve_proph with "Hp").
......
From Coq.Lists Require Import List. (* used for lemma "exists_last" *)
From iris.algebra Require Import auth gmap.
From iris.base_logic Require Export gen_heap.
From iris.base_logic.lib Require Export proph_map.
......@@ -12,7 +13,7 @@ Set Default Proof Using "Type".
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ;
heapG_proph_mapG :> proph_mapG proph_id val Σ
heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ
}.
Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
......@@ -83,9 +84,31 @@ Instance skip_atomic s : Atomic s Skip.
Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance proph_resolve_atomic s e v1 v2 :
Atomic s e Atomic s (Resolve e (Val v1) (Val v2)).
Proof.
rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
- subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
- rewrite fill_app. rewrite fill_app in Hfill.
assert ( v, Val v = fill Ks e1' False) as fill_absurd.
{ intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
destruct K; (inversion Hfill; clear Hfill; subst; try
match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
+ destruct s; intro Hs; simpl in *.
* destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
* apply irreducible_resolve. by rewrite fill_app in Hs.
+ econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
Qed.
Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
Proof. by apply proph_resolve_atomic, skip_atomic. Qed.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec :=
......@@ -396,18 +419,88 @@ Proof.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
(* In the following, strong atomicity is required due to the fact that [e] must
be able to make a head step for [Resolve e _ _] not to be (head) stuck. *)
Lemma resolve_reducible e σ p v :
Atomic StronglyAtomic e reducible e σ
reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ.
Proof.
intros A (κ & e' & σ' & efs & H).
exists (κ ++ [(p, (default v (to_val e'), v))]), e', σ', efs.
eapply Ectx_step with (K:=[]); try done.
assert (w, Val w = e') as [w <-].
{ unfold Atomic in A. apply (A σ e' κ σ' efs) in H. unfold is_Some in H.
destruct H as [w H]. exists w. simpl in H. by apply (of_to_val _ _ H). }
simpl. constructor. by apply prim_step_to_val_is_head_step.
Qed.
Lemma step_resolve e p v σ1 κ e2 σ2 efs :
Atomic StronglyAtomic e
prim_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs
head_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs.
Proof.
intros A [Ks e1' e2' Hfill -> step]. simpl in *.
induction Ks as [|K Ks _] using rev_ind.
+ simpl in *. subst. inversion step. by constructor.
+ rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
- assert (fill_item K (fill Ks e1') = fill (Ks ++ [K]) e1') as Eq1;
first by rewrite fill_app.
assert (fill_item K (fill Ks e2') = fill (Ks ++ [K]) e2') as Eq2;
first by rewrite fill_app.
rewrite fill_app /=. rewrite Eq1 in A.
assert (is_Some (to_val (fill (Ks ++ [K]) e2'))) as H.
{ apply (A σ1 _ κ σ2 efs). eapply Ectx_step with (K0 := Ks ++ [K]); done. }
destruct H as [v H]. apply to_val_fill_some in H. by destruct H, Ks.
- assert (to_val (fill Ks e1') = Some p); first by rewrite -H1 //.
apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
- assert (to_val (fill Ks e1') = Some v); first by rewrite -H2 //.
apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
Qed.
Lemma wp_resolve s E e Φ p v vs :
Atomic StronglyAtomic e
to_val e = None
proph p vs -
WP e @ s; E {{ r, vs', vs = (r, v)::vs' - proph p vs' - Φ r }} -
WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E {{ Φ }}.
Proof.
(* TODO we should try to use a generic lifting lemma (and avoid [wp_unfold])
here, since this breaks the WP abstraction. *)
iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre /= He. simpl in *.
iIntros (σ1 κ κs n) "[Hσ Hκ]". destruct (decide (κ = [])) as [->|HNeq].
- iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
{ iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
iIntros (e2 σ2 efs step). exfalso. apply step_resolve in step; last done.
inversion step. match goal with H: ?κs ++ [_] = [] |- _ => by destruct κs end.
- apply exists_last in HNeq as [κ' [[p' [w' v']] ->]]. rewrite -app_assoc.
iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
{ iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
iIntros (e2 σ2 efs step). apply step_resolve in step; last done. inversion step.
match goal with H: _ ++ _ = _ ++ _ |- _ =>
apply app_inj_2 in H; last done; destruct H as [-> [=-> -> ->]] end. subst.
iMod ("WPe" $! (Val w') σ2 efs with "[%]") as "WPe". { eexists [] _ _; try done. }
iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
iMod (proph_map_resolve_proph p' (w',v') κs with "[$Hκ $Hp]") as (vs' ->) "[$ HPost]".
iModIntro. rewrite !wp_unfold /wp_pre /=. iDestruct "WPe" as "[HΦ $]".
iMod "HΦ". iModIntro. iApply "HΦ"; [ done | iFrame ].
Qed.
Lemma wp_skip s E Φ : Φ (LitV LitUnit) - WP Skip @ s; E {{ Φ }}.
Proof.
iIntros "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "Hσ". iModIntro. iSplit.
- iPureIntro. eexists _, _, _, _. by constructor.
- iIntros (e2 σ2 efs step) "!>". inversion step. simplify_eq. by iFrame.
Qed.
Lemma wp_resolve_proph s E p vs v :
{{{ proph p vs }}}
ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
{{{ vs', RET (LitV LitUnit); vs = v::vs' proph p vs' }}}.
{{{ vs', RET (LitV LitUnit); vs = (LitV LitUnit, v)::vs' proph p vs' }}}.
Proof.
iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
iMod (proph_map_resolve_proph p v κs with "[HR Hp]") as "HPost"; first by iFrame.
iModIntro. iFrame. iSplitR; first done.
iDestruct "HPost" as (vs') "[HEq [HR Hp]]". iFrame.
iApply "HΦ". iFrame.
iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
iApply wp_skip. iNext. iIntros (vs') "HEq Hp". iApply "HΦ". iFrame.
Qed.
End lifting.
......
......@@ -12,10 +12,9 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
| Rec f x e => is_closed_expr (f :b: x :b: X) e
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Load e =>
is_closed_expr X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2
| ResolveProph e1 e2 =>
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
is_closed_expr X e1 && is_closed_expr X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 | Resolve e0 e1 e2 =>
is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
| NewProph => true
end
......@@ -130,7 +129,7 @@ Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
map_Forall (λ _ v, is_closed_val v) σ2.(heap).
Proof.
intros Cl1 Clσ1 STEP.
destruct STEP; simpl in *; split_and!;
induction STEP; simpl in *; split_and!;
try apply map_Forall_insert_2; try by naive_solver.
- subst. repeat apply is_closed_subst'; naive_solver.
- unfold un_op_eval in *. repeat case_match; naive_solver.
......@@ -173,7 +172,7 @@ Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
| CAS e0 e1 e2 => CAS (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
| FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
| NewProph => NewProph
| ResolveProph e1 e2 => ResolveProph (subst_map vs e1) (subst_map vs e2)
| Resolve e0 e1 e2 => Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
end.
Lemma subst_map_empty e : subst_map e = e.
......
......@@ -6,32 +6,48 @@ Import heap_lang.
evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
for each possible decomposition until [tac] succeeds. *)
Ltac reshape_expr e tac :=
let rec go K e :=
match e with
| _ => tac K e
| App ?e (Val ?v) => go (AppLCtx v :: K) e
| App ?e1 ?e2 => go (AppRCtx e1 :: K) e2
| UnOp ?op ?e => go (UnOpCtx op :: K) e
| BinOp ?op ?e (Val ?v) => go (BinOpLCtx op v :: K) e