From 00bfef44ed5ef07c63879a10530f6333079ee6db Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 6 May 2019 18:20:03 +0200
Subject: [PATCH 01/28] Start to extend heaplang with atomic resolution.
---
theories/heap_lang/lang.v | 40 ++++++------
theories/heap_lang/lifting.v | 111 +++++++++++++++++++++++++++++++-
theories/heap_lang/metatheory.v | 9 ++-
theories/heap_lang/tactics.v | 4 +-
4 files changed, 138 insertions(+), 26 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 9edced2d4..0c5c3fbd4 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -14,13 +14,15 @@ 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.
-*)
+If [e] is an expression that executes physically atomically, then so does
+[Resolve e p v]. This second expression behaves exactly as [e], except that
+it aditionally resolves the prophecy variable [p] to the value [v]. *)
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
@@ -72,7 +74,7 @@ Inductive expr :=
| FAA (e1 : expr) (e2 : expr)
(* Prophecy *)
| NewProph
- | ResolveProph (e1 : expr) (e2 : expr)
+ | Resolve (e0 : expr) (e1 : expr) (e2 : expr)
with val :=
| LitV (l : base_lit)
| RecV (f x : binder) (e : expr)
@@ -181,8 +183,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 +257,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 +292,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,8 +349,8 @@ Inductive ectx_item :=
| CasRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
- | ProphLCtx (v2 : val)
- | ProphRCtx (e1 : expr).
+ | ResolveLCtx (e : expr) (v2 : val)
+ | ResolveRCtx (e : expr) (e1 : expr).
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
@@ -375,8 +377,8 @@ 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 ex v2 => Resolve ex e (Val v2)
+ | ResolveRCtx ex e1 => Resolve ex e1 e
end.
(** Substitution *)
@@ -403,7 +405,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 :=
@@ -587,10 +589,10 @@ 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, w)]) (Val v) σ' ts.
(** Basic properties about the language *)
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
@@ -657,3 +659,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).
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 514c533d8..78588a307 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -9,6 +9,41 @@ From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
+(* TODO: move elsewhere. *)
+Lemma app_non_empty_last A (l : list A) : l ≠ [] → ∃ l' x, l = l' ++ [x].
+Proof.
+ induction l; intro H; first by exfalso.
+ destruct (decide (l = [])) as [->|NEq].
+ + exists [], a. reflexivity.
+ + apply IHl in NEq as [l' [x IH]]. exists (a :: l'), x. by rewrite IH.
+Qed.
+
+(* TODO: move elsewhere. *)
+Lemma app_singleton_non_empty A (l : list A) x : l ++ [x] ≠ [].
+Proof. case l; discriminate. Qed.
+
+(* TODO: move elsewhere. *)
+Lemma to_val_fill_some K e v : to_val (fill K e) = Some v → K = [] ∧ e = Val v.
+Proof.
+ intro H. destruct K. { simpl in H. apply of_to_val in H. done. }
+ exfalso. assert (to_val e ≠ None) as HH.
+ { intro A. eapply (fill_not_val (e0 :: K)) in A. rewrite A in H. inversion H. }
+ unfold to_val in HH. simpl in HH. destruct e; try done. clear HH.
+ assert (to_val (fill (e0 :: K) (Val v0)) = None) as G.
+ { clear H v. rename e0 into e. rename v0 into v.
+ destruct e; simpl; apply fill_not_val; done. }
+ rewrite G in H. inversion H.
+Qed.
+
+(* TODO: move elsewhere. *)
+Lemma prim_step_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 [-> ->]. simpl in H1. subst e. done.
+Qed.
+
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ;
@@ -83,8 +118,15 @@ Instance skip_atomic s : Atomic s Skip.
Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
+Instance proph_resolve_atomic s e v1 v2 :
+ Atomic s e → Atomic s (Resolve e (Val v1) (Val v2)).
+Proof.
+ intro H. apply ectx_language_atomic.
+ - inversion 1. eapply H. apply head_prim_step. done.
+ - apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver.
+Qed.
Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
-Proof. solve_atomic. Qed.
+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.
@@ -412,6 +454,73 @@ Proof.
iApply "HΦ". iFrame.
Qed.
+(* TODO: cleanup / move elsewhere? *)
+Lemma wp_resolve_aux s E e Φ p v vs :
+ Atomic StronglyAtomic e → language.to_val e = None →
+ WP e @ s; E {{ r, Φ r }} -∗ proph p vs -∗
+ WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E
+ {{ r, Φ r ∗ ∃ vs', ⌜vs = v::vs'⌝ ∗ proph p vs' }}.
+Proof.
+ iIntros (A He) "WPe Hp". rewrite !wp_unfold /wp_pre He; simpl.
+ iIntros (σ1 κ κs n) "H". iCombine "WPe" "H" as "H".
+ iAssert (|={E}=> ⌜match s with
+ | NotStuck => reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1
+ | MaybeStuck => True
+ end⌝ ∗ _)%I with "[H]" as "XXX".
+ { iApply fupd_plain_keep_l. iSplitR "H"; last iExact "H". iIntros "[WPe [Hσ Hκ]]".
+ iApply fupd_plain_mask_empty. iMod ("WPe" $! σ1 κ κs n with "[$Hσ $Hκ]") as "[Hs WPe]".
+ iModIntro. iDestruct "Hs" as "%". iPureIntro. induction s; last done.
+ destruct H as [κs2 [e2 [σ2 [efs H]]]]. econstructor. exists e2, σ2, efs.
+ econstructor. instantiate (2 := []). reflexivity. reflexivity.
+ assert (is_Some (to_val e2)) as He2.
+ { unfold Atomic in A. specialize A with σ1 e2 κs2 σ2 efs. apply A. apply H. }
+ unfold is_Some in He2. destruct He2 as [w He2]. apply of_to_val in He2. subst e2.
+ constructor. instantiate (1 := κs2). apply prim_step_val_is_head_step. done. }
+ iMod "XXX" as "[$ [WPe [Hσ Hκ]]]".
+ destruct (decide (κ = [])) as [->|HNeq].
+ - iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro.
+ iIntros (e2 σ2 efs step). exfalso.
+ assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as HHH.
+ { exists [], e2, σ2, efs. exact step. } apply prim_head_reducible in HHH.
+ 2: { apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver. }
+ apply head_reducible_prim_step in step; last done. clear HHH. inversion step.
+ destruct κs0; simpl in H4; discriminate H4.
+ - apply app_non_empty_last in HNeq as [κs' [o ->]]. destruct o as [p' v']. rewrite -app_assoc.
+ iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]".
+ iIntros "!>" (e2 σ2 efs step).
+ assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as HHH.
+ { exists (κs' ++ [(p',v')]), e2, σ2, efs. exact step. } apply prim_head_reducible in HHH.
+ 2: { apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver. }
+ apply head_reducible_prim_step in step; last done. clear HHH. inversion step; simpl in *.
+ assert (κs0 = κs' ∧ p = p' ∧ v = v') as [W1 [W2 W3]]. { apply app_inj_2 in H4; last done.
+ destruct H4 as [H41 H42]. split; first done. inversion H42. done. }
+ subst p' v' κs0. iMod ("WPe" $! (Val v0) σ2 efs with "[%]") as "WPe".
+ { econstructor. instantiate (2 := []). reflexivity. simpl; reflexivity. done. }
+ iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
+ iMod (proph_map_resolve_proph p v κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
+ subst vs. iModIntro. simpl. rewrite !wp_unfold /wp_pre; simpl.
+ iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro.
+ iExists vs'. by iFrame.
+Qed.
+
+(*
+Lemma wp_resolve se e s E P r Q p vs v :
+ Atomic se e →
+ {{{ P }}} e @ s; E {{{ RET r; Q }}} →
+ {{{ P ∗ proph p vs }}}
+ Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E
+ {{{ vs', RET r; Q ∗ ⌜vs = v::vs'⌝ ∗ proph p vs' }}}.
+*)
+
+(*
+Lemma wp_resolve se e P vs1 r Q vs2 p v :
+ Atomic se e →
+ {{{ P ∗ proph p vs1 }}} e {{{ RET r; Q ∗ proph p vs2 }}} →
+ {{{ P ∗ proph p vs1 }}}
+ Resolve e (Val $ LitV $ LitProphecy p) (Val v)
+ {{{ vs, RET r; Q ∗ ⌜vs2 = v::vs⌝ ∗ proph p vs }}}.
+*)
+
End lifting.
Notation "l ↦∗ vs" := (array l vs)
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 523d29c75..660fbbd51 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -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.
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 400da8c11..dd586631b 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -32,6 +32,6 @@ Ltac reshape_expr e tac :=
| CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
| FAA ?e (Val ?v) => go (FaaLCtx v :: K) e
| FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
- | ResolveProph ?e (Val ?v) => go (ProphLCtx v :: K) e
- | ResolveProph ?e1 ?e2 => go (ProphRCtx e1 :: K) e2
+ | Resolve ?e (Val ?v) => go (ResolveLCtx v :: K) e
+ | Resolve ?e1 ?e2 => go (ResolveRCtx e1 :: K) e2
end in go (@nil ectx_item) e.
--
GitLab
From 867db0dda6b47942f7ac1099f3c3c587b12d0e46 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 13 May 2019 14:54:05 +0200
Subject: [PATCH 02/28] Observation with pairs of values (result, resolved).
---
theories/base_logic/lib/proph_map.v | 25 +++++++++++-----------
theories/heap_lang/lang.v | 9 +++++---
theories/heap_lang/lib/coin_flip.v | 10 ++++-----
theories/heap_lang/lifting.v | 33 +++++++++++++++++------------
4 files changed, 43 insertions(+), 34 deletions(-)
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index c1a990384..d10910666 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -4,14 +4,14 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
-Local Notation proph_map P V := (gmap P (list V)).
-Definition proph_val_list (P V : Type) := list (P * V).
+Local Notation proph_map P V := (gmap P (list (V * V))).
+Definition proph_val_list (P V : Type) := list (P * (V * V)).
Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
- gmapUR P $ exclR $ listC $ leibnizC V.
+ gmapUR P $ exclR $ listC $ prodC (leibnizC V) (leibnizC V).
Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
- fmap (λ vs, Excl (vs : list (leibnizC V))) pvs.
+ fmap (λ vs, Excl (vs : list (prodC (leibnizC V) (leibnizC V)))) pvs.
(** The CMRA we need. *)
Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
@@ -37,7 +37,7 @@ Section definitions.
Implicit Types p : P.
(** The list of resolves for [p] in [pvs]. *)
- Fixpoint proph_list_resolves pvs p : list V :=
+ Fixpoint proph_list_resolves pvs p : list (V * V) :=
match pvs with
| [] => []
| (q,v)::pvs => if decide (p = q) then v :: proph_list_resolves pvs p
@@ -52,7 +52,7 @@ Section definitions.
dom (gset _) R ⊆ ps⌝ ∗
own (proph_map_name pG) (● (to_proph_map R)))%I.
- Definition proph_def (p : P) (vs : list V) : iProp Σ :=
+ Definition proph_def (p : P) (vs : list (V * V)) : iProp Σ :=
own (proph_map_name pG) (◯ {[p := Excl vs]}).
Definition proph_aux : seal (@proph_def). by eexists. Qed.
@@ -81,14 +81,14 @@ End list_resolves.
Section to_proph_map.
Context (P V : Type) `{Countable P}.
Implicit Types p : P.
- Implicit Types vs : list V.
+ Implicit Types vs : list (V * V).
Implicit Types R : proph_map P V.
Lemma to_proph_map_valid R : ✓ to_proph_map R.
Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
- Lemma to_proph_map_insert p vs R :
- to_proph_map (<[p := vs]> R) = <[p := Excl (vs: list (leibnizC V))]> (to_proph_map R).
+ Lemma to_proph_map_insert p (vs : list (prodC (leibnizC V) (leibnizC V))) R :
+ to_proph_map (<[p := vs]> R) = <[p := Excl vs]> (to_proph_map R).
Proof. by rewrite /to_proph_map fmap_insert. Qed.
Lemma to_proph_map_delete p R :
@@ -119,8 +119,8 @@ Qed.
Section proph_map.
Context `{proph_mapG P V Σ}.
Implicit Types p : P.
- Implicit Types v : V.
- Implicit Types vs : list V.
+ Implicit Types v : V * V.
+ Implicit Types vs : list (V * V).
Implicit Types R : proph_map P V.
Implicit Types ps : gset P.
@@ -159,7 +159,8 @@ Section proph_map.
iMod (own_update_2 with "H● Hp") as "[H● H◯]".
{ eapply auth_update. apply: singleton_local_update.
- by rewrite /to_proph_map lookup_fmap HR.
- - by apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizC V)))). }
+ - by apply (exclusive_local_update _ (Excl
+ (proph_list_resolves pvs p : list (prodC (leibnizC V) (leibnizC V))))). }
rewrite /to_proph_map -fmap_insert.
iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
- iPureIntro. done.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 0c5c3fbd4..a7e28c958 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -74,7 +74,7 @@ Inductive expr :=
| FAA (e1 : expr) (e2 : expr)
(* Prophecy *)
| NewProph
- | Resolve (e0 : expr) (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)
@@ -85,7 +85,10 @@ 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 is returned by the (atomic) operation
+during which the prophecy resolution happened. *)
+Definition observation : Set := proph_id * (val * val).
Notation of_val := Val (only parsing).
@@ -592,7 +595,7 @@ Inductive head_step : expr → state → list observation → expr → state →
| 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, w)]) (Val v) σ' ts.
+ (κs ++ [(p, (v, w))]) (Val v) σ' ts.
(** Basic properties about the language *)
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index 2f76409d2..08545fa3b 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -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").
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 78588a307..c1750f0f0 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -443,12 +443,12 @@ 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.
+ iMod (proph_map_resolve_proph p (LitV LitUnit, 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.
@@ -459,7 +459,7 @@ Lemma wp_resolve_aux s E e Φ p v vs :
Atomic StronglyAtomic e → language.to_val e = None →
WP e @ s; E {{ r, Φ r }} -∗ proph p vs -∗
WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E
- {{ r, Φ r ∗ ∃ vs', ⌜vs = v::vs'⌝ ∗ proph p vs' }}.
+ {{ r, Φ r ∗ ∃ vs', ⌜vs = (r, v)::vs'⌝ ∗ proph p vs' }}.
Proof.
iIntros (A He) "WPe Hp". rewrite !wp_unfold /wp_pre He; simpl.
iIntros (σ1 κ κs n) "H". iCombine "WPe" "H" as "H".
@@ -474,8 +474,9 @@ Proof.
econstructor. instantiate (2 := []). reflexivity. reflexivity.
assert (is_Some (to_val e2)) as He2.
{ unfold Atomic in A. specialize A with σ1 e2 κs2 σ2 efs. apply A. apply H. }
- unfold is_Some in He2. destruct He2 as [w He2]. apply of_to_val in He2. subst e2.
- constructor. instantiate (1 := κs2). apply prim_step_val_is_head_step. done. }
+ unfold is_Some in He2. destruct He2 as [w He2]. apply of_to_val in He2.
+ instantiate (1 := κs2 ++ [(p, (match to_val e2 with Some w => w | _ => v end, v))]).
+ subst e2. simpl. constructor. apply prim_step_val_is_head_step. done. }
iMod "XXX" as "[$ [WPe [Hσ Hκ]]]".
destruct (decide (κ = [])) as [->|HNeq].
- iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro.
@@ -485,31 +486,35 @@ Proof.
2: { apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver. }
apply head_reducible_prim_step in step; last done. clear HHH. inversion step.
destruct κs0; simpl in H4; discriminate H4.
- - apply app_non_empty_last in HNeq as [κs' [o ->]]. destruct o as [p' v']. rewrite -app_assoc.
- iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]".
+ - apply app_non_empty_last in HNeq as [κs' [o ->]]. destruct o as [p' [w' v']].
+ rewrite -app_assoc. iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]".
iIntros "!>" (e2 σ2 efs step).
assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as HHH.
- { exists (κs' ++ [(p',v')]), e2, σ2, efs. exact step. } apply prim_head_reducible in HHH.
+ { exists (κs' ++ [(p',(w',v'))]), e2, σ2, efs. exact step. } apply prim_head_reducible in HHH.
2: { apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver. }
apply head_reducible_prim_step in step; last done. clear HHH. inversion step; simpl in *.
- assert (κs0 = κs' ∧ p = p' ∧ v = v') as [W1 [W2 W3]]. { apply app_inj_2 in H4; last done.
- destruct H4 as [H41 H42]. split; first done. inversion H42. done. }
- subst p' v' κs0. iMod ("WPe" $! (Val v0) σ2 efs with "[%]") as "WPe".
+ assert (κs0 = κs' ∧ p = p' ∧ v = v' ∧ v0 = w') as [W1 [W2 [W3 W4]]].
+ { apply app_inj_2 in H4; last done. destruct H4 as [H41 H42]. split; first done.
+ inversion H42. done. }
+ subst p' v' w' κs0. iMod ("WPe" $! (Val v0) σ2 efs with "[%]") as "WPe".
{ econstructor. instantiate (2 := []). reflexivity. simpl; reflexivity. done. }
iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
- iMod (proph_map_resolve_proph p v κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
+ iMod (proph_map_resolve_proph p (v0,v) κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
subst vs. iModIntro. simpl. rewrite !wp_unfold /wp_pre; simpl.
iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro.
iExists vs'. by iFrame.
Qed.
(*
-Lemma wp_resolve se e s E P r Q p vs v :
- Atomic se e →
+Lemma wp_resolve e s E P r Q p vs v :
+ Atomic StronglyAtomic e → language.to_val e = None →
{{{ P }}} e @ s; E {{{ RET r; Q }}} →
{{{ P ∗ proph p vs }}}
Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E
{{{ vs', RET r; Q ∗ ⌜vs = v::vs'⌝ ∗ proph p vs' }}}.
+Proof.
+ iIntros (A He TTe Φ) "[P Hp] HΦ". iDestruct TTe as "#TTe"; clear TTe.
+ iDestruct ("TTe" with "P") as "He". instantiate (1 := Φ).
*)
(*
--
GitLab
From 141baad96477d7f07aa4d2c5a90e7765e6dedaa7 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 13 May 2019 15:30:11 +0200
Subject: [PATCH 03/28] Cleaning up (unused lemma + use lemma from Coq stdlib).
---
theories/heap_lang/lifting.v | 16 ++--------------
1 file changed, 2 insertions(+), 14 deletions(-)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index c1750f0f0..1bda07cb4 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,3 +1,4 @@
+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.
@@ -9,19 +10,6 @@ From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
-(* TODO: move elsewhere. *)
-Lemma app_non_empty_last A (l : list A) : l ≠ [] → ∃ l' x, l = l' ++ [x].
-Proof.
- induction l; intro H; first by exfalso.
- destruct (decide (l = [])) as [->|NEq].
- + exists [], a. reflexivity.
- + apply IHl in NEq as [l' [x IH]]. exists (a :: l'), x. by rewrite IH.
-Qed.
-
-(* TODO: move elsewhere. *)
-Lemma app_singleton_non_empty A (l : list A) x : l ++ [x] ≠ [].
-Proof. case l; discriminate. Qed.
-
(* TODO: move elsewhere. *)
Lemma to_val_fill_some K e v : to_val (fill K e) = Some v → K = [] ∧ e = Val v.
Proof.
@@ -486,7 +474,7 @@ Proof.
2: { apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver. }
apply head_reducible_prim_step in step; last done. clear HHH. inversion step.
destruct κs0; simpl in H4; discriminate H4.
- - apply app_non_empty_last in HNeq as [κs' [o ->]]. destruct o as [p' [w' v']].
+ - apply exists_last in HNeq as [κs' [o ->]]. destruct o as [p' [w' v']].
rewrite -app_assoc. iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]".
iIntros "!>" (e2 σ2 efs step).
assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as HHH.
--
GitLab
From 567a21a6f4189453233306b43b45e34908409140 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 13 May 2019 16:21:03 +0200
Subject: [PATCH 04/28] New statement of Resolve's lifting lemma.
---
theories/heap_lang/lifting.v | 41 +++++++++---------------------------
1 file changed, 10 insertions(+), 31 deletions(-)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 1bda07cb4..3798dd3fb 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -442,14 +442,14 @@ Proof.
iApply "HΦ". iFrame.
Qed.
-(* TODO: cleanup / move elsewhere? *)
-Lemma wp_resolve_aux s E e Φ p v vs :
- Atomic StronglyAtomic e → language.to_val e = None →
- WP e @ s; E {{ r, Φ r }} -∗ proph p vs -∗
- WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E
- {{ r, Φ r ∗ ∃ vs', ⌜vs = (r, v)::vs'⌝ ∗ proph p vs' }}.
+Lemma wp_resolve s E e Φ p v vs :
+ Atomic StronglyAtomic e →
+ language.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.
- iIntros (A He) "WPe Hp". rewrite !wp_unfold /wp_pre He; simpl.
+ iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre He; simpl.
iIntros (σ1 κ κs n) "H". iCombine "WPe" "H" as "H".
iAssert (|={E}=> ⌜match s with
| NotStuck => reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1
@@ -457,7 +457,7 @@ Proof.
end⌝ ∗ _)%I with "[H]" as "XXX".
{ iApply fupd_plain_keep_l. iSplitR "H"; last iExact "H". iIntros "[WPe [Hσ Hκ]]".
iApply fupd_plain_mask_empty. iMod ("WPe" $! σ1 κ κs n with "[$Hσ $Hκ]") as "[Hs WPe]".
- iModIntro. iDestruct "Hs" as "%". iPureIntro. induction s; last done.
+ iModIntro. iDestruct "Hs" as "%". iPureIntro. destruct s; last done.
destruct H as [κs2 [e2 [σ2 [efs H]]]]. econstructor. exists e2, σ2, efs.
econstructor. instantiate (2 := []). reflexivity. reflexivity.
assert (is_Some (to_val e2)) as He2.
@@ -489,31 +489,10 @@ Proof.
iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
iMod (proph_map_resolve_proph p (v0,v) κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
subst vs. iModIntro. simpl. rewrite !wp_unfold /wp_pre; simpl.
- iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro.
- iExists vs'. by iFrame.
+ iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro. simplify_eq.
+ iApply "HΦ"; first done. iFrame.
Qed.
-(*
-Lemma wp_resolve e s E P r Q p vs v :
- Atomic StronglyAtomic e → language.to_val e = None →
- {{{ P }}} e @ s; E {{{ RET r; Q }}} →
- {{{ P ∗ proph p vs }}}
- Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E
- {{{ vs', RET r; Q ∗ ⌜vs = v::vs'⌝ ∗ proph p vs' }}}.
-Proof.
- iIntros (A He TTe Φ) "[P Hp] HΦ". iDestruct TTe as "#TTe"; clear TTe.
- iDestruct ("TTe" with "P") as "He". instantiate (1 := Φ).
-*)
-
-(*
-Lemma wp_resolve se e P vs1 r Q vs2 p v :
- Atomic se e →
- {{{ P ∗ proph p vs1 }}} e {{{ RET r; Q ∗ proph p vs2 }}} →
- {{{ P ∗ proph p vs1 }}}
- Resolve e (Val $ LitV $ LitProphecy p) (Val v)
- {{{ vs, RET r; Q ∗ ⌜vs2 = v::vs⌝ ∗ proph p vs }}}.
-*)
-
End lifting.
Notation "l ↦∗ vs" := (array l vs)
--
GitLab
From d10cbc5dac7691350d25462ccb624a783610cc90 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 13 May 2019 17:10:25 +0200
Subject: [PATCH 05/28] Use spec of Resolve for (legacy) ResolveProph.
---
theories/heap_lang/lifting.v | 36 ++++++++++++++++++++----------------
1 file changed, 20 insertions(+), 16 deletions(-)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 3798dd3fb..9d1fff0c3 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -428,20 +428,6 @@ Proof.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
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 = (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 (LitV LitUnit, 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.
-Qed.
-
Lemma wp_resolve s E e Φ p v vs :
Atomic StronglyAtomic e →
language.to_val e = None →
@@ -450,8 +436,9 @@ Lemma wp_resolve s E e Φ p v vs :
WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E {{ Φ }}.
Proof.
iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre He; simpl.
- iIntros (σ1 κ κs n) "H". iCombine "WPe" "H" as "H".
- iAssert (|={E}=> ⌜match s with
+ iIntros (σ1 κ κs n) "H".
+ (* TODO cleaning up from here. *)
+ iCombine "WPe" "H" as "H". iAssert (|={E}=> ⌜match s with
| NotStuck => reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1
| MaybeStuck => True
end⌝ ∗ _)%I with "[H]" as "XXX".
@@ -493,6 +480,23 @@ Proof.
iApply "HΦ"; first 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 S) "!>". inversion S. 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 = (LitV LitUnit, v)::vs'⌝ ∗ proph p vs' }}}.
+Proof.
+ iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
+ iApply wp_skip. iNext. iIntros (vs') "HEq Hp". iApply "HΦ". iFrame.
+Qed.
+
End lifting.
Notation "l ↦∗ vs" := (array l vs)
--
GitLab
From 296cb5b421c9577697ea30dfd737a0836ad16f11 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 13 May 2019 18:23:05 +0200
Subject: [PATCH 06/28] Cleaning up new reduction lemmas for heaplang.
---
theories/heap_lang/lang.v | 16 ++++++++++++++++
theories/heap_lang/lifting.v | 24 +-----------------------
2 files changed, 17 insertions(+), 23 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index a7e28c958..6a02d692b 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -649,6 +649,22 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
(* Prefer heap_lang names over ectx_language names. *)
Export heap_lang.
+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 [|i K]. { apply of_to_val in H. done. } exfalso.
+ assert (to_val e ≠ None) as He. { intro A. rewrite fill_not_val in H; done. }
+ destruct e; try done. assert (to_val (fill (i :: K) (Val v0)) = None) as G.
+ { clear H v. destruct i; simpl; apply fill_not_val; done. } 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.
+
(** 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).
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 9d1fff0c3..52bb69991 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -10,28 +10,6 @@ From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
-(* TODO: move elsewhere. *)
-Lemma to_val_fill_some K e v : to_val (fill K e) = Some v → K = [] ∧ e = Val v.
-Proof.
- intro H. destruct K. { simpl in H. apply of_to_val in H. done. }
- exfalso. assert (to_val e ≠ None) as HH.
- { intro A. eapply (fill_not_val (e0 :: K)) in A. rewrite A in H. inversion H. }
- unfold to_val in HH. simpl in HH. destruct e; try done. clear HH.
- assert (to_val (fill (e0 :: K) (Val v0)) = None) as G.
- { clear H v. rename e0 into e. rename v0 into v.
- destruct e; simpl; apply fill_not_val; done. }
- rewrite G in H. inversion H.
-Qed.
-
-(* TODO: move elsewhere. *)
-Lemma prim_step_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 [-> ->]. simpl in H1. subst e. done.
-Qed.
-
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ;
@@ -451,7 +429,7 @@ Proof.
{ unfold Atomic in A. specialize A with σ1 e2 κs2 σ2 efs. apply A. apply H. }
unfold is_Some in He2. destruct He2 as [w He2]. apply of_to_val in He2.
instantiate (1 := κs2 ++ [(p, (match to_val e2 with Some w => w | _ => v end, v))]).
- subst e2. simpl. constructor. apply prim_step_val_is_head_step. done. }
+ subst e2. simpl. constructor. apply prim_step_to_val_is_head_step. done. }
iMod "XXX" as "[$ [WPe [Hσ Hκ]]]".
destruct (decide (κ = [])) as [->|HNeq].
- iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro.
--
GitLab
From 44047eb0459f67adcf376a5e125afc53f8406dba Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Tue, 14 May 2019 11:43:31 +0200
Subject: [PATCH 07/28] Proof cleanup (lifting lemma for Resolve).
---
theories/heap_lang/lifting.v | 83 ++++++++++++++++++------------------
1 file changed, 41 insertions(+), 42 deletions(-)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 52bb69991..b6d529f4c 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -406,6 +406,18 @@ Proof.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
+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]]]]. econstructor. exists e', σ', efs. econstructor.
+ instantiate (2 := []). reflexivity. reflexivity. 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). }
+ instantiate (1 := κ ++ [(p, (match to_val e' with Some w => w | _ => v end, v))]).
+ simpl. constructor. by apply prim_step_to_val_is_head_step.
+Qed.
+
Lemma wp_resolve s E e Φ p v vs :
Atomic StronglyAtomic e →
language.to_val e = None →
@@ -413,49 +425,36 @@ Lemma wp_resolve s E e Φ p v 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.
- iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre He; simpl.
- iIntros (σ1 κ κs n) "H".
- (* TODO cleaning up from here. *)
- iCombine "WPe" "H" as "H". iAssert (|={E}=> ⌜match s with
- | NotStuck => reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1
- | MaybeStuck => True
- end⌝ ∗ _)%I with "[H]" as "XXX".
- { iApply fupd_plain_keep_l. iSplitR "H"; last iExact "H". iIntros "[WPe [Hσ Hκ]]".
- iApply fupd_plain_mask_empty. iMod ("WPe" $! σ1 κ κs n with "[$Hσ $Hκ]") as "[Hs WPe]".
- iModIntro. iDestruct "Hs" as "%". iPureIntro. destruct s; last done.
- destruct H as [κs2 [e2 [σ2 [efs H]]]]. econstructor. exists e2, σ2, efs.
- econstructor. instantiate (2 := []). reflexivity. reflexivity.
- assert (is_Some (to_val e2)) as He2.
- { unfold Atomic in A. specialize A with σ1 e2 κs2 σ2 efs. apply A. apply H. }
- unfold is_Some in He2. destruct He2 as [w He2]. apply of_to_val in He2.
- instantiate (1 := κs2 ++ [(p, (match to_val e2 with Some w => w | _ => v end, v))]).
- subst e2. simpl. constructor. apply prim_step_to_val_is_head_step. done. }
- iMod "XXX" as "[$ [WPe [Hσ Hκ]]]".
- destruct (decide (κ = [])) as [->|HNeq].
- - iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro.
+ iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre He. inv_head_step.
+ 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; last done. by apply resolve_reducible. }
iIntros (e2 σ2 efs step). exfalso.
- assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as HHH.
- { exists [], e2, σ2, efs. exact step. } apply prim_head_reducible in HHH.
- 2: { apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver. }
- apply head_reducible_prim_step in step; last done. clear HHH. inversion step.
- destruct κs0; simpl in H4; discriminate H4.
- - apply exists_last in HNeq as [κs' [o ->]]. destruct o as [p' [w' v']].
- rewrite -app_assoc. iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]".
- iIntros "!>" (e2 σ2 efs step).
- assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as HHH.
- { exists (κs' ++ [(p',(w',v'))]), e2, σ2, efs. exact step. } apply prim_head_reducible in HHH.
- 2: { apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver. }
- apply head_reducible_prim_step in step; last done. clear HHH. inversion step; simpl in *.
- assert (κs0 = κs' ∧ p = p' ∧ v = v' ∧ v0 = w') as [W1 [W2 [W3 W4]]].
- { apply app_inj_2 in H4; last done. destruct H4 as [H41 H42]. split; first done.
- inversion H42. done. }
- subst p' v' w' κs0. iMod ("WPe" $! (Val v0) σ2 efs with "[%]") as "WPe".
- { econstructor. instantiate (2 := []). reflexivity. simpl; reflexivity. done. }
- iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
- iMod (proph_map_resolve_proph p (v0,v) κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
- subst vs. iModIntro. simpl. rewrite !wp_unfold /wp_pre; simpl.
- iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro. simplify_eq.
- iApply "HΦ"; first done. iFrame.
+ assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as R.
+ { exists [], e2, σ2, efs. exact step. }
+ apply prim_head_reducible in R.
+ + apply head_reducible_prim_step in step; last done. inv_head_step.
+ destruct κs0; simpl in H4; discriminate H4.
+ + apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver.
+ - 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; last done. by apply resolve_reducible. }
+ iIntros (e2 σ2 efs step).
+ assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as R.
+ { exists (κ' ++ [(p',(w',v'))]), e2, σ2, efs. exact step. }
+ apply prim_head_reducible in R.
+ + apply head_reducible_prim_step in step; last done. inversion step; simpl in *.
+ assert (κs0 = κ' ∧ p = p' ∧ v = v' ∧ v0 = w') as [Eq1 [Eq2 [Eq3 Eq4]]].
+ { apply app_inj_2 in H4; last done. destruct H4 as [H41 H42].
+ split; first done. by inversion H42. }
+ subst p' v' w' κs0. iMod ("WPe" $! (Val v0) σ2 efs with "[%]") as "WPe".
+ { econstructor. instantiate (2 := []). reflexivity. simpl; reflexivity. done. }
+ iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
+ iMod (proph_map_resolve_proph p (v0,v) κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
+ subst vs. iModIntro. simpl. rewrite !wp_unfold /wp_pre; simpl.
+ iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro. simplify_eq.
+ iApply "HΦ"; first done. iFrame.
+ + apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver.
Qed.
Lemma wp_skip s E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ s; E {{ Φ }}.
--
GitLab
From 553a4c1eb37807a19d08c55da26430016a3f8b65 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Wed, 15 May 2019 10:29:27 +0200
Subject: [PATCH 08/28] Revert changes in proph_map and use parameter.
---
theories/base_logic/lib/proph_map.v | 25 ++++++++++++-------------
theories/heap_lang/adequacy.v | 4 ++--
theories/heap_lang/lifting.v | 2 +-
3 files changed, 15 insertions(+), 16 deletions(-)
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index d10910666..c1a990384 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -4,14 +4,14 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
-Local Notation proph_map P V := (gmap P (list (V * V))).
-Definition proph_val_list (P V : Type) := list (P * (V * V)).
+Local Notation proph_map P V := (gmap P (list V)).
+Definition proph_val_list (P V : Type) := list (P * V).
Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
- gmapUR P $ exclR $ listC $ prodC (leibnizC V) (leibnizC V).
+ gmapUR P $ exclR $ listC $ leibnizC V.
Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
- fmap (λ vs, Excl (vs : list (prodC (leibnizC V) (leibnizC V)))) pvs.
+ fmap (λ vs, Excl (vs : list (leibnizC V))) pvs.
(** The CMRA we need. *)
Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
@@ -37,7 +37,7 @@ Section definitions.
Implicit Types p : P.
(** The list of resolves for [p] in [pvs]. *)
- Fixpoint proph_list_resolves pvs p : list (V * V) :=
+ Fixpoint proph_list_resolves pvs p : list V :=
match pvs with
| [] => []
| (q,v)::pvs => if decide (p = q) then v :: proph_list_resolves pvs p
@@ -52,7 +52,7 @@ Section definitions.
dom (gset _) R ⊆ ps⌝ ∗
own (proph_map_name pG) (● (to_proph_map R)))%I.
- Definition proph_def (p : P) (vs : list (V * V)) : iProp Σ :=
+ Definition proph_def (p : P) (vs : list V) : iProp Σ :=
own (proph_map_name pG) (◯ {[p := Excl vs]}).
Definition proph_aux : seal (@proph_def). by eexists. Qed.
@@ -81,14 +81,14 @@ End list_resolves.
Section to_proph_map.
Context (P V : Type) `{Countable P}.
Implicit Types p : P.
- Implicit Types vs : list (V * V).
+ Implicit Types vs : list V.
Implicit Types R : proph_map P V.
Lemma to_proph_map_valid R : ✓ to_proph_map R.
Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
- Lemma to_proph_map_insert p (vs : list (prodC (leibnizC V) (leibnizC V))) R :
- to_proph_map (<[p := vs]> R) = <[p := Excl vs]> (to_proph_map R).
+ Lemma to_proph_map_insert p vs R :
+ to_proph_map (<[p := vs]> R) = <[p := Excl (vs: list (leibnizC V))]> (to_proph_map R).
Proof. by rewrite /to_proph_map fmap_insert. Qed.
Lemma to_proph_map_delete p R :
@@ -119,8 +119,8 @@ Qed.
Section proph_map.
Context `{proph_mapG P V Σ}.
Implicit Types p : P.
- Implicit Types v : V * V.
- Implicit Types vs : list (V * V).
+ Implicit Types v : V.
+ Implicit Types vs : list V.
Implicit Types R : proph_map P V.
Implicit Types ps : gset P.
@@ -159,8 +159,7 @@ Section proph_map.
iMod (own_update_2 with "H● Hp") as "[H● H◯]".
{ eapply auth_update. apply: singleton_local_update.
- by rewrite /to_proph_map lookup_fmap HR.
- - by apply (exclusive_local_update _ (Excl
- (proph_list_resolves pvs p : list (prodC (leibnizC V) (leibnizC V))))). }
+ - by apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizC V)))). }
rewrite /to_proph_map -fmap_insert.
iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
- iPureIntro. done.
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 217ca2cae..6f13fbb39 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -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.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index b6d529f4c..9d0414b59 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -13,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 Σ := {
--
GitLab
From 2da7dbef5f43feeb0f28ebae0e668129535e015d Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Wed, 15 May 2019 11:04:58 +0200
Subject: [PATCH 09/28] Add comments related to Resolve heap_lang.
---
theories/heap_lang/lang.v | 20 ++++++++++++++++++--
1 file changed, 18 insertions(+), 2 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 6a02d692b..03dadac04 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -86,8 +86,10 @@ Bind Scope expr_scope with expr.
Bind Scope val_scope with val.
(** An observation associates a prophecy variable (identifier) to a pair of
-values. The first value is the one that is returned by the (atomic) operation
-during which the prophecy resolution happened. *)
+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).
@@ -355,6 +357,15 @@ Inductive ectx_item :=
| ResolveLCtx (e : expr) (v2 : val)
| ResolveRCtx (e : expr) (e1 : expr).
+(** The first argument of [Resolve] is never evaluated through the contextual
+closure of reduction. Its evaluation (in one step, to a value) is done while
+taking a head reduction step. As a consequence, one should make sure that the
+expression [e] indeed reduces to a value atomically (i.e., in one step).
+
+Note that the expression [Resolve (CAS #l #n (#n + #1)) p v] will not reduce
+as one would expect. A workaroud it do use some let-normalization, which in
+the above case yields [let: "x" := #n + #1 in Resolve (CAS #l #n "x") p v]. *)
+
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx v2 => App e (of_val v2)
@@ -649,6 +660,11 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
(* Prefer heap_lang names over ectx_language names. *)
Export heap_lang.
+(* The following lemma does not seem to be provable using the current axioms
+of [ectxi_language]. The current 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 if [e] is not 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 [|i K]. { apply of_to_val in H. done. } exfalso.
--
GitLab
From c1f02a16751fef0ee3103a2003d1bc38c3626dea Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Wed, 15 May 2019 11:17:34 +0200
Subject: [PATCH 10/28] Say why strong atomicity is needed in the lifting lemma
of Resolve.
---
theories/heap_lang/lifting.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 9d0414b59..2126f603a 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -406,6 +406,9 @@ 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)) σ.
--
GitLab
From 5042e95106087487732c9303783e3fee2299e624 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 17 May 2019 16:59:21 +0200
Subject: [PATCH 11/28] clean up proofs a bit
---
theories/heap_lang/lifting.v | 22 +++++++++++-----------
1 file changed, 11 insertions(+), 11 deletions(-)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 2126f603a..816886a34 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -413,11 +413,12 @@ 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]]]]. econstructor. exists e', σ', efs. econstructor.
- instantiate (2 := []). reflexivity. reflexivity. assert (∃w, Val w = e') as [w <-].
+ intros A [κ [e' [σ' [efs H]]]].
+ exists (κ ++ [(p, (match to_val e' with Some w => w | _ => v end, 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). }
- instantiate (1 := κ ++ [(p, (match to_val e' with Some w => w | _ => v end, v))]).
simpl. constructor. by apply prim_step_to_val_is_head_step.
Qed.
@@ -437,7 +438,7 @@ Proof.
{ exists [], e2, σ2, efs. exact step. }
apply prim_head_reducible in R.
+ apply head_reducible_prim_step in step; last done. inv_head_step.
- destruct κs0; simpl in H4; discriminate H4.
+ match goal with H: ?κs ++ _ = [] |- _ => destruct κs; simpl in H; discriminate end.
+ apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver.
- apply exists_last in HNeq as [κ' [[p' [w' v']] ->]]. rewrite -app_assoc.
iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
@@ -446,14 +447,13 @@ Proof.
assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as R.
{ exists (κ' ++ [(p',(w',v'))]), e2, σ2, efs. exact step. }
apply prim_head_reducible in R.
- + apply head_reducible_prim_step in step; last done. inversion step; simpl in *.
- assert (κs0 = κ' ∧ p = p' ∧ v = v' ∧ v0 = w') as [Eq1 [Eq2 [Eq3 Eq4]]].
- { apply app_inj_2 in H4; last done. destruct H4 as [H41 H42].
- split; first done. by inversion H42. }
- subst p' v' w' κs0. iMod ("WPe" $! (Val v0) σ2 efs with "[%]") as "WPe".
- { econstructor. instantiate (2 := []). reflexivity. simpl; reflexivity. done. }
+ + apply head_reducible_prim_step in step; last done. inv_head_step.
+ match goal with H: _ ++ _ = _ ++ _ |- _ =>
+ apply app_inj_2 in H; last done; destruct H as [-> [=-> -> ->]] end.
+ iMod ("WPe" $! (Val w') σ2 efs with "[%]") as "WPe".
+ { eexists [] _ _. reflexivity. simpl; reflexivity. done. }
iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
- iMod (proph_map_resolve_proph p (v0,v) κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
+ iMod (proph_map_resolve_proph p' (w',v') κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
subst vs. iModIntro. simpl. rewrite !wp_unfold /wp_pre; simpl.
iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro. simplify_eq.
iApply "HΦ"; first done. iFrame.
--
GitLab
From cbc0951bf6cbf15c6f5bc8918857e570811647f3 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Wed, 29 May 2019 11:09:03 +0200
Subject: [PATCH 12/28] Implement Jacques-Henry's proposal (need cleanup)
---
theories/heap_lang/lang.v | 21 +++++---
theories/heap_lang/lifting.v | 97 +++++++++++++++++++++++++++---------
theories/heap_lang/tactics.v | 5 +-
3 files changed, 89 insertions(+), 34 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 03dadac04..290b311d6 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -354,8 +354,9 @@ Inductive ectx_item :=
| CasRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
- | ResolveLCtx (e : expr) (v2 : val)
- | ResolveRCtx (e : expr) (e1 : expr).
+ | ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
+ | ResolveMCtx (e0 : expr) (v2 : val)
+ | ResolveRCtx (e0 : expr) (e1 : expr).
(** The first argument of [Resolve] is never evaluated through the contextual
closure of reduction. Its evaluation (in one step, to a value) is done while
@@ -366,7 +367,7 @@ Note that the expression [Resolve (CAS #l #n (#n + #1)) p v] will not reduce
as one would expect. A workaroud it do use some let-normalization, which in
the above case yields [let: "x" := #n + #1 in Resolve (CAS #l #n "x") p v]. *)
-Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
+Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx v2 => App e (of_val v2)
| AppRCtx e1 => App e1 e
@@ -391,7 +392,8 @@ 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
- | ResolveLCtx ex v2 => Resolve ex e (Val v2)
+ | 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.
@@ -610,23 +612,26 @@ Inductive head_step : expr → state → list observation → expr → state →
(** 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; induction Ki1; intros; simplify_eq; try done.
+ f_equal. eapply IHKi2; done.
+Qed.
Lemma alloc_fresh v n σ :
let l := fresh_locs (dom (gset loc) σ.(heap)) n in
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 816886a34..d1433dfb3 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -84,12 +84,43 @@ Instance skip_atomic s : Atomic s Skip.
Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
+
+Lemma fill_app {Λ} Ks1 Ks2 e : @fill Λ (Ks1 ++ Ks2) e = @fill Λ Ks2 (@fill Λ Ks1 e).
+Proof. rewrite /fill foldl_app //. 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.
+ + 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.
+ + assert (to_val (fill Ks e1') = Some v1); first by rewrite -H2 //.
+ apply to_val_fill_some in H0. destruct H0 as [-> ->]. inversion step.
+ + assert (to_val (fill Ks e1') = Some v2); first by rewrite -H3 //.
+ apply to_val_fill_some in H0. destruct H0 as [-> ->]. inversion step.
+Qed.
+
Instance proph_resolve_atomic s e v1 v2 :
Atomic s e → Atomic s (Resolve e (Val v1) (Val v2)).
Proof.
- intro H. apply ectx_language_atomic.
- - inversion 1. eapply H. apply head_prim_step. done.
- - apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver.
+ 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.
+ destruct K; inversion Hfill; clear Hfill; subst.
+ + refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)); last first.
+ econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
+ destruct s; intro Hs; simpl in *.
+ * destruct Hs as [v Hs]. apply to_val_fill_some in Hs.
+ destruct Hs as [Contra _]. destruct Ks; inversion Contra.
+ * apply irreducible_resolve. rewrite fill_app in Hs. done.
+ + induction Ks as [|K Ks _] using rev_ind. { simpl in H2. subst. inversion step. }
+ rewrite fill_app in H2. simpl in H2. destruct K; inversion H2.
+ + induction Ks as [|K Ks _] using rev_ind. { simpl in H3. subst. inversion step. }
+ rewrite fill_app in H3. simpl in H3. destruct K; inversion H3.
Qed.
Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
Proof. by apply proph_resolve_atomic, skip_atomic. Qed.
@@ -422,6 +453,32 @@ Proof.
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. subst. constructor. done.
+ + rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
+ - rewrite fill_app /=.
+ 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 Eq1 in A.
+ assert (is_Some (to_val (fill (Ks ++ [K]) e2'))) as He2'. {
+ refine (A σ1 _ κ σ2 efs _).
+ refine (Ectx_step (fill (Ks ++ [K]) e1') σ1 κ
+ (fill (Ks ++ [K]) e2') σ2 efs (Ks ++ [K]) e1' e2' eq_refl eq_refl step).
+ }
+ unfold is_Some in He2'. destruct He2' as [v HEq]. apply to_val_fill_some in HEq.
+ destruct HEq as [Contra _]. destruct Ks; done.
+ - 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 →
language.to_val e = None →
@@ -433,31 +490,23 @@ Proof.
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; last done. by apply resolve_reducible. }
- iIntros (e2 σ2 efs step). exfalso.
- assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as R.
- { exists [], e2, σ2, efs. exact step. }
- apply prim_head_reducible in R.
- + apply head_reducible_prim_step in step; last done. inv_head_step.
- match goal with H: ?κs ++ _ = [] |- _ => destruct κs; simpl in H; discriminate end.
- + apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver.
+ iIntros (e2 σ2 efs step). exfalso. apply step_resolve in step; last done. inversion step.
+ destruct κs0; inversion H4.
- 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; last done. by apply resolve_reducible. }
iIntros (e2 σ2 efs step).
- assert (reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ1) as R.
- { exists (κ' ++ [(p',(w',v'))]), e2, σ2, efs. exact step. }
- apply prim_head_reducible in R.
- + apply head_reducible_prim_step in step; last done. inv_head_step.
- match goal with H: _ ++ _ = _ ++ _ |- _ =>
- apply app_inj_2 in H; last done; destruct H as [-> [=-> -> ->]] end.
- iMod ("WPe" $! (Val w') σ2 efs with "[%]") as "WPe".
- { eexists [] _ _. reflexivity. simpl; reflexivity. done. }
- iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
- iMod (proph_map_resolve_proph p' (w',v') κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
- subst vs. iModIntro. simpl. rewrite !wp_unfold /wp_pre; simpl.
- iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro. simplify_eq.
- iApply "HΦ"; first done. iFrame.
- + apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver.
+ 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 [] _ _. reflexivity. simpl; reflexivity. done. }
+ iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
+ iMod (proph_map_resolve_proph p' (w',v') κs with "[$Hκ $Hp]") as (vs') "[% [$ HPost]]".
+ subst vs. iModIntro. simpl. rewrite !wp_unfold /wp_pre; simpl.
+ iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro. simplify_eq.
+ iApply "HΦ"; first done. iFrame.
Qed.
Lemma wp_skip s E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ s; E {{ Φ }}.
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index dd586631b..36179e28b 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -32,6 +32,7 @@ Ltac reshape_expr e tac :=
| CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
| FAA ?e (Val ?v) => go (FaaLCtx v :: K) e
| FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
- | Resolve ?e (Val ?v) => go (ResolveLCtx v :: K) e
- | Resolve ?e1 ?e2 => go (ResolveRCtx e1 :: K) e2
+ | Resolve ?ex (Val ?v1) (Val ?v2) => go (ResolveLCtx v1 v2 :: K) ex
+ | Resolve ?ex ?e1 (Val ?v2) => go (ResolveMCtx ex v2 :: K) e1
+ | Resolve ?ex ?e1 ?e2 => go (ResolveRCtx ex e1 :: K) e2
end in go (@nil ectx_item) e.
--
GitLab
From e53f1992ffb01ba5f501b36f0ed3a4093043d46e Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Thu, 30 May 2019 01:26:37 +0200
Subject: [PATCH 13/28] Cleanup of proofs + failed attempt for [reshape_expr].
---
theories/heap_lang/lang.v | 28 ++++++++++-----
theories/heap_lang/lifting.v | 69 ++++++++++++------------------------
theories/heap_lang/tactics.v | 40 ++++++++++++++++++++-
3 files changed, 81 insertions(+), 56 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 290b311d6..92400c95e 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -358,14 +358,11 @@ Inductive ectx_item :=
| ResolveMCtx (e0 : expr) (v2 : val)
| ResolveRCtx (e0 : expr) (e1 : expr).
-(** The first argument of [Resolve] is never evaluated through the contextual
-closure of reduction. Its evaluation (in one step, to a value) is done while
-taking a head reduction step. As a consequence, one should make sure that the
-expression [e] indeed reduces to a value atomically (i.e., in one step).
-
-Note that the expression [Resolve (CAS #l #n (#n + #1)) p v] will not reduce
-as one would expect. A workaroud it do use some let-normalization, which in
-the above case yields [let: "x" := #n + #1 in Resolve (CAS #l #n "x") p v]. *)
+(** 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 [Resolve (CAS #l #n (#n + #1)) #p #v] will evaluate
+to [Resolve (CAS #l #n #(n + 1)) #p #v] using context steps, but no further
+step will be taken (by the contextual closure). *)
Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
@@ -686,6 +683,21 @@ Proof.
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.
+ + 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.
+ + assert (to_val (fill Ks e1') = Some v1); first by rewrite -H2 //.
+ apply to_val_fill_some in H0. destruct H0 as [-> ->]. inversion step.
+ + assert (to_val (fill Ks e1') = Some v2); first by rewrite -H3 //.
+ apply to_val_fill_some in H0. destruct H0 as [-> ->]. inversion step.
+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).
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index d1433dfb3..973ce60f4 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -85,24 +85,6 @@ Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
-Lemma fill_app {Λ} Ks1 Ks2 e : @fill Λ (Ks1 ++ Ks2) e = @fill Λ Ks2 (@fill Λ Ks1 e).
-Proof. rewrite /fill foldl_app //. 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.
- + 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.
- + assert (to_val (fill Ks e1') = Some v1); first by rewrite -H2 //.
- apply to_val_fill_some in H0. destruct H0 as [-> ->]. inversion step.
- + assert (to_val (fill Ks e1') = Some v2); first by rewrite -H3 //.
- apply to_val_fill_some in H0. destruct H0 as [-> ->]. inversion step.
-Qed.
-
Instance proph_resolve_atomic s e v1 v2 :
Atomic s e → Atomic s (Resolve e (Val v1) (Val v2)).
Proof.
@@ -114,14 +96,14 @@ Proof.
+ refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)); last first.
econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
destruct s; intro Hs; simpl in *.
- * destruct Hs as [v Hs]. apply to_val_fill_some in Hs.
- destruct Hs as [Contra _]. destruct Ks; inversion Contra.
- * apply irreducible_resolve. rewrite fill_app in Hs. done.
+ * 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.
+ induction Ks as [|K Ks _] using rev_ind. { simpl in H2. subst. inversion step. }
rewrite fill_app in H2. simpl in H2. destruct K; inversion H2.
+ induction Ks as [|K Ks _] using rev_ind. { simpl in H3. subst. inversion step. }
rewrite fill_app in H3. simpl in H3. destruct K; inversion H3.
Qed.
+
Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
Proof. by apply proph_resolve_atomic, skip_atomic. Qed.
@@ -460,19 +442,16 @@ Lemma step_resolve e p 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. subst. constructor. done.
+ + simpl in *. subst. inversion step. by constructor.
+ rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
- - rewrite fill_app /=.
- 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 Eq1 in A.
- assert (is_Some (to_val (fill (Ks ++ [K]) e2'))) as He2'. {
- refine (A σ1 _ κ σ2 efs _).
- refine (Ectx_step (fill (Ks ++ [K]) e1') σ1 κ
- (fill (Ks ++ [K]) e2') σ2 efs (Ks ++ [K]) e1' e2' eq_refl eq_refl step).
- }
- unfold is_Some in He2'. destruct He2' as [v HEq]. apply to_val_fill_some in HEq.
- destruct HEq as [Contra _]. destruct Ks; done.
+ - 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 //.
@@ -486,27 +465,23 @@ Lemma wp_resolve s E e Φ p v 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.
- iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre He. inv_head_step.
+ 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; last done. by apply resolve_reducible. }
- iIntros (e2 σ2 efs step). exfalso. apply step_resolve in step; last done. inversion step.
- destruct κs0; inversion H4.
+ { 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; last done. by apply resolve_reducible. }
- iIntros (e2 σ2 efs step).
- apply step_resolve in step; last done. inversion step.
+ { 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 [] _ _. reflexivity. simpl; reflexivity. done. }
+ 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]]".
- subst vs. iModIntro. simpl. rewrite !wp_unfold /wp_pre; simpl.
- iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iFrame. iModIntro. simplify_eq.
- iApply "HΦ"; first done. iFrame.
+ subst vs. 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 {{ Φ }}.
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 36179e28b..051901cf4 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -32,7 +32,45 @@ Ltac reshape_expr e tac :=
| CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
| FAA ?e (Val ?v) => go (FaaLCtx v :: K) e
| FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
- | Resolve ?ex (Val ?v1) (Val ?v2) => go (ResolveLCtx v1 v2 :: K) ex
+ | Resolve ?ex (Val ?v1) (Val ?v2) => fail 0 "reshape_expr: not implemented" (* FIXME *)
| Resolve ?ex ?e1 (Val ?v2) => go (ResolveMCtx ex v2 :: K) e1
| Resolve ?ex ?e1 ?e2 => go (ResolveRCtx ex e1 :: K) e2
end in go (@nil ectx_item) e.
+
+(* Failed attempt.
+Definition build_ResolveLCtx Ki pairs :=
+ fold_right (fun p i => ResolveLCtx i p.1 p.2) pairs Ki.
+
+Ltac reshape_expr e tac :=
+ let rec go K vs e :=
+ match e with
+ | _ => match vs with nil => tac K e | _ => () end
+ | App ?e (Val ?v) => go (build_ResolveLCtx (AppLCtx v) vs :: K) nil e
+ | App ?e1 ?e2 => go (build_ResolveLCtx (AppRCtx e1) vs :: K) nil e2
+ | UnOp ?op ?e => go (build_ResolveLCtx (UnOpCtx op) vs :: K) nil e
+ | BinOp ?op ?e (Val ?v) => go (build_ResolveLCtx (BinOpLCtx op v) vs :: K) nil e
+ | BinOp ?op ?e1 ?e2 => go (build_ResolveLCtx (BinOpRCtx op e1) vs :: K) nil e2
+ | If ?e0 ?e1 ?e2 => go (build_ResolveLCtx (IfCtx e1 e2) vs :: K) nil e0
+ | Pair ?e (Val ?v) => go (build_ResolveLCtx (PairLCtx v) vs :: K) nil e
+ | Pair ?e1 ?e2 => go (build_ResolveLCtx (PairRCtx e1) vs :: K) nil e2
+ | Fst ?e => go (build_ResolveLCtx FstCtx vs :: K) nil e
+ | Snd ?e => go (build_ResolveLCtx SndCtx vs :: K) nil e
+ | InjL ?e => go (build_ResolveLCtx InjLCtx vs :: K) nil e
+ | InjR ?e => go (build_ResolveLCtx InjRCtx vs :: K) nil e
+ | Case ?e0 ?e1 ?e2 => go (build_ResolveLCtx (CaseCtx e1 e2) vs :: K) nil e0
+ | Alloc ?e => go (build_ResolveLCtx AllocCtx vs :: K) nil e
+ | Load ?e => go (build_ResolveLCtx LoadCtx vs :: K) nil e
+ | Store ?e (Val ?v) => go (build_ResolveLCtx (StoreLCtx v) vs :: K) nil e
+ | Store ?e1 ?e2 => go (build_ResolveLCtx (StoreRCtx e1) vs :: K) nil e2
+ | CAS ?e0 (Val ?v1) (Val ?v2) => go (build_ResolveLCtx (CasLCtx v1 v2) vs :: K) nil e0
+ | CAS ?e0 ?e1 (Val ?v2) => go (build_ResolveLCtx (CasMCtx e0 v2) vs :: K) nil e1
+ | CAS ?e0 ?e1 ?e2 => go (build_ResolveLCtx (CasRCtx e0 e1) vs :: K) nil e2
+ | FAA ?e (Val ?v) => go (build_ResolveLCtx (FaaLCtx v) vs :: K) nil e
+ | FAA ?e1 ?e2 => go (build_ResolveLCtx (FaaRCtx e1) vs :: K) nil e2
+ | Resolve ?ex (Val ?v1) (Val ?v2) => go K ((v1,v2) :: vs) ex
+ | Resolve ?ex ?e1 (Val ?v2) => go (build_ResolveLCtx (ResolveMCtx ex v2) vs :: K) nil e1
+ | Resolve ?ex ?e1 ?e2 => go (build_ResolveLCtx (ResolveRCtx ex e1) vs :: K) nil e2
+ end
+ in
+ go (@nil ectx_item) (@nil (list (val * val))) e.
+*)
--
GitLab
From 22398d20a84bb56cce9e53d1bd8ca2f471c8b8f9 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Thu, 30 May 2019 13:11:39 +0200
Subject: [PATCH 14/28] Fix for [reshape_expr] given by Robbert.
---
theories/heap_lang/tactics.v | 95 ++++++++++++------------------------
1 file changed, 32 insertions(+), 63 deletions(-)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 051901cf4..d9597a4e4 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -5,72 +5,41 @@ Import heap_lang.
(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
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
- | BinOp ?op ?e1 ?e2 => go (BinOpRCtx op e1 :: K) e2
- | If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
- | Pair ?e (Val ?v) => go (PairLCtx v :: K) e
- | Pair ?e1 ?e2 => go (PairRCtx e1 :: K) e2
- | Fst ?e => go (FstCtx :: K) e
- | Snd ?e => go (SndCtx :: K) e
- | InjL ?e => go (InjLCtx :: K) e
- | InjR ?e => go (InjRCtx :: K) e
- | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
- | AllocN ?e (Val ?v) => go (AllocNLCtx v :: K) e
- | AllocN ?e1 ?e2 => go (AllocNRCtx e1 :: K) e2
- | Load ?e => go (LoadCtx :: K) e
- | Store ?e (Val ?v) => go (StoreLCtx v :: K) e
- | Store ?e1 ?e2 => go (StoreRCtx e1 :: K) e2
- | CAS ?e0 (Val ?v1) (Val ?v2) => go (CasLCtx v1 v2 :: K) e0
- | CAS ?e0 ?e1 (Val ?v2) => go (CasMCtx e0 v2 :: K) e1
- | CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
- | FAA ?e (Val ?v) => go (FaaLCtx v :: K) e
- | FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
- | Resolve ?ex (Val ?v1) (Val ?v2) => fail 0 "reshape_expr: not implemented" (* FIXME *)
- | Resolve ?ex ?e1 (Val ?v2) => go (ResolveMCtx ex v2 :: K) e1
- | Resolve ?ex ?e1 ?e2 => go (ResolveRCtx ex e1 :: K) e2
- end in go (@nil ectx_item) e.
-
-(* Failed attempt.
-Definition build_ResolveLCtx Ki pairs :=
- fold_right (fun p i => ResolveLCtx i p.1 p.2) pairs Ki.
-
Ltac reshape_expr e tac :=
let rec go K vs e :=
match e with
- | _ => match vs with nil => tac K e | _ => () end
- | App ?e (Val ?v) => go (build_ResolveLCtx (AppLCtx v) vs :: K) nil e
- | App ?e1 ?e2 => go (build_ResolveLCtx (AppRCtx e1) vs :: K) nil e2
- | UnOp ?op ?e => go (build_ResolveLCtx (UnOpCtx op) vs :: K) nil e
- | BinOp ?op ?e (Val ?v) => go (build_ResolveLCtx (BinOpLCtx op v) vs :: K) nil e
- | BinOp ?op ?e1 ?e2 => go (build_ResolveLCtx (BinOpRCtx op e1) vs :: K) nil e2
- | If ?e0 ?e1 ?e2 => go (build_ResolveLCtx (IfCtx e1 e2) vs :: K) nil e0
- | Pair ?e (Val ?v) => go (build_ResolveLCtx (PairLCtx v) vs :: K) nil e
- | Pair ?e1 ?e2 => go (build_ResolveLCtx (PairRCtx e1) vs :: K) nil e2
- | Fst ?e => go (build_ResolveLCtx FstCtx vs :: K) nil e
- | Snd ?e => go (build_ResolveLCtx SndCtx vs :: K) nil e
- | InjL ?e => go (build_ResolveLCtx InjLCtx vs :: K) nil e
- | InjR ?e => go (build_ResolveLCtx InjRCtx vs :: K) nil e
- | Case ?e0 ?e1 ?e2 => go (build_ResolveLCtx (CaseCtx e1 e2) vs :: K) nil e0
- | Alloc ?e => go (build_ResolveLCtx AllocCtx vs :: K) nil e
- | Load ?e => go (build_ResolveLCtx LoadCtx vs :: K) nil e
- | Store ?e (Val ?v) => go (build_ResolveLCtx (StoreLCtx v) vs :: K) nil e
- | Store ?e1 ?e2 => go (build_ResolveLCtx (StoreRCtx e1) vs :: K) nil e2
- | CAS ?e0 (Val ?v1) (Val ?v2) => go (build_ResolveLCtx (CasLCtx v1 v2) vs :: K) nil e0
- | CAS ?e0 ?e1 (Val ?v2) => go (build_ResolveLCtx (CasMCtx e0 v2) vs :: K) nil e1
- | CAS ?e0 ?e1 ?e2 => go (build_ResolveLCtx (CasRCtx e0 e1) vs :: K) nil e2
- | FAA ?e (Val ?v) => go (build_ResolveLCtx (FaaLCtx v) vs :: K) nil e
- | FAA ?e1 ?e2 => go (build_ResolveLCtx (FaaRCtx e1) vs :: K) nil e2
+ | _ => lazymatch vs with [] => tac K e | _ => fail end
+ | App ?e (Val ?v) => go_resolve (AppLCtx v) vs K e
+ | App ?e1 ?e2 => go_resolve (AppRCtx e1) vs K e2
+ | UnOp ?op ?e => go_resolve (UnOpCtx op) vs K e
+ | BinOp ?op ?e (Val ?v) => go_resolve (BinOpLCtx op v) vs K e
+ | BinOp ?op ?e1 ?e2 => go_resolve (BinOpRCtx op e1) vs K e2
+ | If ?e0 ?e1 ?e2 => go_resolve (IfCtx e1 e2) vs K e0
+ | Pair ?e (Val ?v) => go_resolve (PairLCtx v) vs K e
+ | Pair ?e1 ?e2 => go_resolve (PairRCtx e1) vs K e2
+ | Fst ?e => go_resolve FstCtx vs K e
+ | Snd ?e => go_resolve SndCtx vs K e
+ | InjL ?e => go_resolve InjLCtx vs K e
+ | InjR ?e => go_resolve InjRCtx vs K e
+ | Case ?e0 ?e1 ?e2 => go_resolve (CaseCtx e1 e2) vs K e0
+ | AllocN ?e (Val ?v) => go_resolve (AllocNLCtx v) vs K e
+ | AllocN ?e1 ?e2 => go_resolve (AllocNRCtx e1) vs K e2
+ | Load ?e => go_resolve LoadCtx vs K e
+ | Store ?e (Val ?v) => go_resolve (StoreLCtx v) vs K e
+ | Store ?e1 ?e2 => go_resolve (StoreRCtx e1) vs K e2
+ | CAS ?e0 (Val ?v1) (Val ?v2) => go_resolve (CasLCtx v1 v2) vs K e0
+ | CAS ?e0 ?e1 (Val ?v2) => go_resolve (CasMCtx e0 v2) vs K e1
+ | CAS ?e0 ?e1 ?e2 => go_resolve (CasRCtx e0 e1) vs K e2
+ | FAA ?e (Val ?v) => go_resolve (FaaLCtx v) vs K e
+ | FAA ?e1 ?e2 => go_resolve (FaaRCtx e1) vs K e2
| Resolve ?ex (Val ?v1) (Val ?v2) => go K ((v1,v2) :: vs) ex
- | Resolve ?ex ?e1 (Val ?v2) => go (build_ResolveLCtx (ResolveMCtx ex v2) vs :: K) nil e1
- | Resolve ?ex ?e1 ?e2 => go (build_ResolveLCtx (ResolveRCtx ex e1) vs :: K) nil e2
+ | Resolve ?ex ?e1 (Val ?v2) => go_resolve (ResolveMCtx ex v2) vs K e1
+ | Resolve ?ex ?e1 ?e2 => go_resolve (ResolveRCtx ex e1) vs K e2
+ end
+ with go_resolve Ki vs K e :=
+ lazymatch vs with
+ | [] => go (Ki :: K) (@nil (val * val)) e
+ | (?v1,?v2) :: ?vs => go_resolve (ResolveLCtx Ki v1 v2) vs K e
end
in
- go (@nil ectx_item) (@nil (list (val * val))) e.
-*)
+ go (@nil ectx_item) (@nil (val * val)) e.
--
GitLab
From 80ea7c7b82d7f2061f6f9361ee410bd8a8bf2ebe Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Thu, 30 May 2019 15:36:48 +0200
Subject: [PATCH 15/28] Cleanup: applying some MR comments.
---
theories/heap_lang/lang.v | 32 +++++++++++++++++---------------
theories/heap_lang/lifting.v | 6 +++---
2 files changed, 20 insertions(+), 18 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 92400c95e..3964ffa6c 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -358,13 +358,14 @@ Inductive ectx_item :=
| ResolveMCtx (e0 : expr) (v2 : val)
| ResolveRCtx (e0 : expr) (e1 : expr).
-(** 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 [Resolve (CAS #l #n (#n + #1)) #p #v] will evaluate
-to [Resolve (CAS #l #n #(n + 1)) #p #v] using context steps, but no further
-step will be taken (by the contextual closure). *)
-
-Fixpoint fill_item (Ki : ectx_item) (e : expr) : 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
@@ -625,10 +626,7 @@ Proof. revert κ e2. induction Ki; inversion_clear 1; simplify_option_eq; eauto
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.
- revert Ki1. induction Ki2; induction Ki1; intros; simplify_eq; try done.
- f_equal. eapply IHKi2; done.
-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
@@ -669,10 +667,14 @@ 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 if [e] is not 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 [|i K]. { apply of_to_val in H. done. } exfalso.
- assert (to_val e ≠ None) as He. { intro A. rewrite fill_not_val in H; done. }
- destruct e; try done. assert (to_val (fill (i :: K) (Val v0)) = None) as G.
- { clear H v. destruct i; simpl; apply fill_not_val; done. } simplify_eq.
+ intro H. destruct K as [|i 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 (i :: K) (Val w)) = None).
+ { destruct i; simpl; apply fill_not_val; done. }
+ by simplify_eq.
Qed.
Lemma prim_step_to_val_is_head_step e σ1 κs w σ2 efs :
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 973ce60f4..270f654ab 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -426,8 +426,8 @@ 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, (match to_val e' with Some w => w | _ => v end, v))]), e', σ', efs.
+ 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.
@@ -489,7 +489,7 @@ 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 S) "!>". inversion S. simplify_eq. by iFrame.
+ - iIntros (e2 σ2 efs step) "!>". inversion step. simplify_eq. by iFrame.
Qed.
Lemma wp_resolve_proph s E p vs v :
--
GitLab
From 4a6a72e708fb1724b604200177c33554290f4358 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Thu, 30 May 2019 15:41:47 +0200
Subject: [PATCH 16/28] More cleanup, avoid [language.to_val].
---
theories/heap_lang/lifting.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 270f654ab..39ae8f415 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -460,12 +460,12 @@ Qed.
Lemma wp_resolve s E e Φ p v vs :
Atomic StronglyAtomic e →
- language.to_val e = None →
+ 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.
- iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre He. simpl in *.
+ 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]. }
--
GitLab
From 3ee217df5c23138dda475dbe25fefcb6e03fb962 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Thu, 30 May 2019 15:56:34 +0200
Subject: [PATCH 17/28] Explanations in [reshape_expr].
---
theories/heap_lang/tactics.v | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index d9597a4e4..08a7d464d 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -6,6 +6,14 @@ 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 :=
+ (* Note that the current context is spread into a list of fully-constructed
+ items [K], and a list of pairs of values [vs] that is only non-empty if
+ a [ResolveLCtx] item (possibly with several levels)is in the process of
+ being constructed. The construction is trigerred by calling [go_resolve]
+ whenever a new, non-[ResolveLCtx] item is constructed. In that case, the
+ accumulated elements of [vs] (if any) can be used to produce the expected
+ [ResolveLCtx] context: a sequence of [ResolveLCtx] with elements of [vs]
+ terminated with the non-[ResolveLCtx] item initially fed to [go_resolve]. *)
let rec go K vs e :=
match e with
| _ => lazymatch vs with [] => tac K e | _ => fail end
--
GitLab
From 26243e6b9b2a6add00511008329c0f920cde44e0 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Thu, 30 May 2019 17:48:29 +0200
Subject: [PATCH 18/28] Tests for Resolve.
---
tests/heap_lang_proph.ref | 0
tests/heap_lang_proph.v | 89 +++++++++++++++++++++++++++++++++++++++
2 files changed, 89 insertions(+)
create mode 100644 tests/heap_lang_proph.ref
create mode 100644 tests/heap_lang_proph.v
diff --git a/tests/heap_lang_proph.ref b/tests/heap_lang_proph.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
new file mode 100644
index 000000000..f563d457f
--- /dev/null
+++ b/tests/heap_lang_proph.v
@@ -0,0 +1,89 @@
+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.
+
+ Instance alloc_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
+ Proof.
+ apply strongly_atomic_atomic, ectx_language_atomic.
+ - inversion 1; naive_solver.
+ - apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver.
+ 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.
--
GitLab
From 3f5f403dbad48db62fc3454aa708d1e8881192d1 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Thu, 30 May 2019 23:00:15 +0200
Subject: [PATCH 19/28] Move Atomic instance to lifting.v
---
tests/heap_lang_proph.v | 9 +--------
theories/heap_lang/lifting.v | 2 ++
2 files changed, 3 insertions(+), 8 deletions(-)
diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index f563d457f..d5e2cbbc5 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -45,14 +45,7 @@ Section tests.
wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame.
Qed.
- Instance alloc_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
- Proof.
- apply strongly_atomic_atomic, ectx_language_atomic.
- - inversion 1; naive_solver.
- - apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver.
- Qed.
-
- Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) :
+ 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.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 39ae8f415..4deb629e2 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -84,6 +84,8 @@ Instance skip_atomic s : Atomic s Skip.
Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
+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)).
--
GitLab
From d9c8aa634b5e867fe6e26c5d19bf370413807215 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Fri, 31 May 2019 10:29:03 +0200
Subject: [PATCH 20/28] Get rid of some generated hypothesis name.
---
theories/heap_lang/lang.v | 15 ++++++++-------
theories/heap_lang/lifting.v | 21 +++++++++++----------
2 files changed, 19 insertions(+), 17 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 3964ffa6c..0644ac397 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -691,13 +691,14 @@ 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.
- + 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.
- + assert (to_val (fill Ks e1') = Some v1); first by rewrite -H2 //.
- apply to_val_fill_some in H0. destruct H0 as [-> ->]. inversion step.
- + assert (to_val (fill Ks e1') = Some v2); first by rewrite -H3 //.
- apply to_val_fill_some in H0. destruct H0 as [-> ->]. inversion 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; first 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. *)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 4deb629e2..d812fcd81 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -94,16 +94,17 @@ Proof.
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.
- destruct K; inversion Hfill; clear Hfill; subst.
- + refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)); last first.
- econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
- 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.
- + induction Ks as [|K Ks _] using rev_ind. { simpl in H2. subst. inversion step. }
- rewrite fill_app in H2. simpl in H2. destruct K; inversion H2.
- + induction Ks as [|K Ks _] using rev_ind. { simpl in H3. subst. inversion step. }
- rewrite fill_app in H3. simpl in H3. destruct K; inversion H3.
+ destruct K; (inversion Hfill; clear Hfill; subst; try
+ match goal with | H : Val ?v = fill Ks ?e |- _ =>
+ induction Ks as [|K Ks _] using rev_ind;
+ [ simpl in H; subst; inversion step
+ | rewrite fill_app in H; simpl in H; destruct K; inversion H ]
+ end).
+ refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)); last first.
+ econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
+ 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.
Qed.
Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
--
GitLab
From 5f7312b531033571a2b21f1749912d55e5881be7 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Fri, 31 May 2019 13:02:29 +0200
Subject: [PATCH 21/28] Clarify comment in [theories/heap_lang/lang.v].
---
theories/heap_lang/lang.v | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 0644ac397..40928f21c 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -660,11 +660,11 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
(* Prefer heap_lang names over ectx_language names. *)
Export heap_lang.
-(* The following lemma does not seem to be provable using the current axioms
-of [ectxi_language]. The current 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 if [e] is not a value. *)
+(* 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 if [e] is not 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 [|i K]; first by apply of_to_val in H. exfalso.
--
GitLab
From f095ba930a75ba55a129f7426bf3055627ae3450 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Fri, 31 May 2019 18:58:34 +0200
Subject: [PATCH 22/28] Comment fix.
---
theories/heap_lang/lang.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 40928f21c..cff6a5ef1 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -664,7 +664,7 @@ Export heap_lang.
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 if [e] is not a value. *)
+[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 [|i K]; first by apply of_to_val in H. exfalso.
--
GitLab
From d450139f451f30cf63c11bb5dbbaec38a76de33b Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Fri, 31 May 2019 20:19:56 +0200
Subject: [PATCH 23/28] Clearer comment + some renaming.
---
theories/heap_lang/tactics.v | 68 ++++++++++++++++++------------------
1 file changed, 34 insertions(+), 34 deletions(-)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 08a7d464d..6ea6feb75 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -7,47 +7,47 @@ 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 :=
(* Note that the current context is spread into a list of fully-constructed
- items [K], and a list of pairs of values [vs] that is only non-empty if
- a [ResolveLCtx] item (possibly with several levels)is in the process of
- being constructed. The construction is trigerred by calling [go_resolve]
- whenever a new, non-[ResolveLCtx] item is constructed. In that case, the
- accumulated elements of [vs] (if any) can be used to produce the expected
- [ResolveLCtx] context: a sequence of [ResolveLCtx] with elements of [vs]
- terminated with the non-[ResolveLCtx] item initially fed to [go_resolve]. *)
+ items [K], and a list of pairs of values [vs] (prophecy identifier and
+ resolution value) that is only non-empty if a [ResolveLCtx] item (maybe
+ having several levels) is in the process of being constructed. Note that
+ a fully-constructed item is inserted into [K] by calling [add_item], and
+ that is only the case when a non-[ResolveLCtx] item is built. When [vs]
+ is non-empty, [add_item] also wraps the item under several [ResolveLCtx]
+ constructors: one for each pair in [vs]. *)
let rec go K vs e :=
match e with
| _ => lazymatch vs with [] => tac K e | _ => fail end
- | App ?e (Val ?v) => go_resolve (AppLCtx v) vs K e
- | App ?e1 ?e2 => go_resolve (AppRCtx e1) vs K e2
- | UnOp ?op ?e => go_resolve (UnOpCtx op) vs K e
- | BinOp ?op ?e (Val ?v) => go_resolve (BinOpLCtx op v) vs K e
- | BinOp ?op ?e1 ?e2 => go_resolve (BinOpRCtx op e1) vs K e2
- | If ?e0 ?e1 ?e2 => go_resolve (IfCtx e1 e2) vs K e0
- | Pair ?e (Val ?v) => go_resolve (PairLCtx v) vs K e
- | Pair ?e1 ?e2 => go_resolve (PairRCtx e1) vs K e2
- | Fst ?e => go_resolve FstCtx vs K e
- | Snd ?e => go_resolve SndCtx vs K e
- | InjL ?e => go_resolve InjLCtx vs K e
- | InjR ?e => go_resolve InjRCtx vs K e
- | Case ?e0 ?e1 ?e2 => go_resolve (CaseCtx e1 e2) vs K e0
- | AllocN ?e (Val ?v) => go_resolve (AllocNLCtx v) vs K e
- | AllocN ?e1 ?e2 => go_resolve (AllocNRCtx e1) vs K e2
- | Load ?e => go_resolve LoadCtx vs K e
- | Store ?e (Val ?v) => go_resolve (StoreLCtx v) vs K e
- | Store ?e1 ?e2 => go_resolve (StoreRCtx e1) vs K e2
- | CAS ?e0 (Val ?v1) (Val ?v2) => go_resolve (CasLCtx v1 v2) vs K e0
- | CAS ?e0 ?e1 (Val ?v2) => go_resolve (CasMCtx e0 v2) vs K e1
- | CAS ?e0 ?e1 ?e2 => go_resolve (CasRCtx e0 e1) vs K e2
- | FAA ?e (Val ?v) => go_resolve (FaaLCtx v) vs K e
- | FAA ?e1 ?e2 => go_resolve (FaaRCtx e1) vs K e2
+ | App ?e (Val ?v) => add_item (AppLCtx v) vs K e
+ | App ?e1 ?e2 => add_item (AppRCtx e1) vs K e2
+ | UnOp ?op ?e => add_item (UnOpCtx op) vs K e
+ | BinOp ?op ?e (Val ?v) => add_item (BinOpLCtx op v) vs K e
+ | BinOp ?op ?e1 ?e2 => add_item (BinOpRCtx op e1) vs K e2
+ | If ?e0 ?e1 ?e2 => add_item (IfCtx e1 e2) vs K e0
+ | Pair ?e (Val ?v) => add_item (PairLCtx v) vs K e
+ | Pair ?e1 ?e2 => add_item (PairRCtx e1) vs K e2
+ | Fst ?e => add_item FstCtx vs K e
+ | Snd ?e => add_item SndCtx vs K e
+ | InjL ?e => add_item InjLCtx vs K e
+ | InjR ?e => add_item InjRCtx vs K e
+ | Case ?e0 ?e1 ?e2 => add_item (CaseCtx e1 e2) vs K e0
+ | AllocN ?e (Val ?v) => add_item (AllocNLCtx v) vs K e
+ | AllocN ?e1 ?e2 => add_item (AllocNRCtx e1) vs K e2
+ | Load ?e => add_item LoadCtx vs K e
+ | Store ?e (Val ?v) => add_item (StoreLCtx v) vs K e
+ | Store ?e1 ?e2 => add_item (StoreRCtx e1) vs K e2
+ | CAS ?e0 (Val ?v1) (Val ?v2) => add_item (CasLCtx v1 v2) vs K e0
+ | CAS ?e0 ?e1 (Val ?v2) => add_item (CasMCtx e0 v2) vs K e1
+ | CAS ?e0 ?e1 ?e2 => add_item (CasRCtx e0 e1) vs K e2
+ | FAA ?e (Val ?v) => add_item (FaaLCtx v) vs K e
+ | FAA ?e1 ?e2 => add_item (FaaRCtx e1) vs K e2
| Resolve ?ex (Val ?v1) (Val ?v2) => go K ((v1,v2) :: vs) ex
- | Resolve ?ex ?e1 (Val ?v2) => go_resolve (ResolveMCtx ex v2) vs K e1
- | Resolve ?ex ?e1 ?e2 => go_resolve (ResolveRCtx ex e1) vs K e2
+ | Resolve ?ex ?e1 (Val ?v2) => add_item (ResolveMCtx ex v2) vs K e1
+ | Resolve ?ex ?e1 ?e2 => add_item (ResolveRCtx ex e1) vs K e2
end
- with go_resolve Ki vs K e :=
+ with add_item Ki vs K e :=
lazymatch vs with
| [] => go (Ki :: K) (@nil (val * val)) e
- | (?v1,?v2) :: ?vs => go_resolve (ResolveLCtx Ki v1 v2) vs K e
+ | (?v1,?v2) :: ?vs => add_item (ResolveLCtx Ki v1 v2) vs K e
end
in
go (@nil ectx_item) (@nil (val * val)) e.
--
GitLab
From d3e5f3c92a4df50e92add1b4775232f922ce8142 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 3 Jun 2019 16:57:07 +0200
Subject: [PATCH 24/28] Apply comments by Robbert.
---
theories/heap_lang/lang.v | 10 +++++-----
theories/heap_lang/lifting.v | 16 ++++++++--------
2 files changed, 13 insertions(+), 13 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index cff6a5ef1..0b59998ff 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -621,7 +621,7 @@ 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. revert κ e2. induction Ki; inversion_clear 1; simplify_option_eq; 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 →
@@ -667,13 +667,13 @@ last line), which in all cases yields a non-value. To prove this lemma for
[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 [|i K]; first by apply of_to_val in H. exfalso.
+ 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 (i :: K) (Val w)) = None).
- { destruct i; simpl; apply fill_not_val; done. }
+ assert (to_val (fill (Ki :: K) (Val w)) = None).
+ { destruct Ki; simpl; apply fill_not_val; done. }
by simplify_eq.
Qed.
@@ -694,7 +694,7 @@ Proof.
- 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; first by rewrite -H //);
+ (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).
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index d812fcd81..f5d9bb0a6 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -100,11 +100,11 @@ Proof.
[ simpl in H; subst; inversion step
| rewrite fill_app in H; simpl in H; destruct K; inversion H ]
end).
- refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)); last first.
- econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
- 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.
+ 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)).
@@ -482,9 +482,9 @@ Proof.
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]]".
- subst vs. iModIntro. rewrite !wp_unfold /wp_pre /=.
- iDestruct "WPe" as "[HΦ $]". iMod "HΦ". iModIntro. iApply "HΦ"; [ done | iFrame ].
+ 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 {{ Φ }}.
--
GitLab
From 827cc03e1fbff903f6816cbcfbcf0b2c871db343 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 3 Jun 2019 17:38:52 +0200
Subject: [PATCH 25/28] Avoid long tactic by using assert.
---
theories/heap_lang/lifting.v | 9 ++++-----
1 file changed, 4 insertions(+), 5 deletions(-)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index f5d9bb0a6..a7cee04a4 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -94,12 +94,11 @@ Proof.
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 ?e |- _ =>
- induction Ks as [|K Ks _] using rev_ind;
- [ simpl in H; subst; inversion step
- | rewrite fill_app in H; simpl in H; destruct K; inversion H ]
- end).
+ 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.
--
GitLab
From 78e3c54100d72de75efbfed54159cd47ad13872b Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 3 Jun 2019 18:13:38 +0200
Subject: [PATCH 26/28] Add a comment.
---
theories/heap_lang/lifting.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index a7cee04a4..ce71d9fd4 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -467,6 +467,8 @@ Lemma wp_resolve s E e Φ p v 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.
--
GitLab
From 462d6044e064372dd49aa9b8bf7c177ece8d8963 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 3 Jun 2019 20:19:38 +0200
Subject: [PATCH 27/28] Fix indentation.
---
tests/heap_lang_proph.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index d5e2cbbc5..a68a6ff2e 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -45,7 +45,7 @@ Section tests.
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)) :
+ 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.
--
GitLab
From b38b34344686293815cdf8c6bf3f94bffea8675d Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Mon, 3 Jun 2019 23:41:31 +0200
Subject: [PATCH 28/28] More precise comment for [Resolve].
---
theories/heap_lang/lang.v | 33 ++++++++++++++++++++++++++++++---
1 file changed, 30 insertions(+), 3 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 0b59998ff..3fcd37f68 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -20,9 +20,36 @@ Set Default Proof Using "Type".
program diverge unless the variable matches. That, however, requires an
erasure proof that this endless loop does not make specifications useless.
-If [e] is an expression that executes physically atomically, then so does
-[Resolve e p v]. This second expression behaves exactly as [e], except that
-it aditionally resolves the prophecy variable [p] to the value [v]. *)
+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.
--
GitLab