Skip to content

I
iris
Commit 25ed5c9c authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

generalize to lists of observations per program step

parent fc59d6d0
Hide whitespace changes
Inline Side-by-side
Showing with 83 additions and 87 deletions
theories/heap_lang/lang.v
View file @ 25ed5c9c
......@@ -448,82 +448,83 @@ Definition state_upd_used_proph (f: gset proph → gset proph) (σ: state) :=
{| heap := σ.(heap); used_proph := f σ.(used_proph) |}.
Arguments state_upd_used_proph _ !_ /.
Inductive head_step : expr → state → option observation → expr → state → list (expr) → Prop :=
Inductive head_step : expr → state → list observation → expr → state → list (expr) → Prop :=
| BetaS f x e1 e2 v2 e' σ :
to_val e2 = Some v2 →
Closed (f :b: x :b: []) e1 →
e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) →
head_step (App (Rec f x e1) e2) σ None e' σ []
head_step (App (Rec f x e1) e2) σ [] e' σ []
| UnOpS op e v v' σ :
to_val e = Some v →
un_op_eval op v = Some v' →
head_step (UnOp op e) σ None (of_val v') σ []
head_step (UnOp op e) σ [] (of_val v') σ []
| BinOpS op e1 e2 v1 v2 v' σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
bin_op_eval op v1 v2 = Some v' →
head_step (BinOp op e1 e2) σ None (of_val v') σ []
head_step (BinOp op e1 e2) σ [] (of_val v') σ []
| IfTrueS e1 e2 σ :
head_step (If (Lit $ LitBool true) e1 e2) σ None e1 σ []
head_step (If (Lit $ LitBool true) e1 e2) σ [] e1 σ []
| IfFalseS e1 e2 σ :
head_step (If (Lit $ LitBool false) e1 e2) σ None e2 σ []
head_step (If (Lit $ LitBool false) e1 e2) σ [] e2 σ []
| FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
head_step (Fst (Pair e1 e2)) σ None e1 σ []
head_step (Fst (Pair e1 e2)) σ [] e1 σ []
| SndS e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
head_step (Snd (Pair e1 e2)) σ None e2 σ []
head_step (Snd (Pair e1 e2)) σ [] e2 σ []
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
head_step (Case (InjL e0) e1 e2) σ None (App e1 e0) σ []
head_step (Case (InjL e0) e1 e2) σ [] (App e1 e0) σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
head_step (Case (InjR e0) e1 e2) σ None (App e2 e0) σ []
head_step (Case (InjR e0) e1 e2) σ [] (App e2 e0) σ []
| ForkS e σ:
head_step (Fork e) σ None (Lit LitUnit) σ [e]
head_step (Fork e) σ [] (Lit LitUnit) σ [e]
| AllocS e v σ l :
to_val e = Some v → σ.(heap) !! l = None →
head_step (Alloc e) σ
None (Lit $ LitLoc l) (state_upd_heap <[l:=v]> σ)
[]
(Lit $ LitLoc l) (state_upd_heap <[l:=v]> σ)
[]
| LoadS l v σ :
σ.(heap) !! l = Some v →
head_step (Load (Lit $ LitLoc l)) σ None (of_val v) σ []
head_step (Load (Lit $ LitLoc l)) σ [] (of_val v) σ []
| StoreS l e v σ :
to_val e = Some v → is_Some (σ.(heap) !! l) →
head_step (Store (Lit $ LitLoc l) e) σ
None
[]
(Lit LitUnit) (state_upd_heap <[l:=v]> σ)
[]
| CasFailS l e1 v1 e2 v2 vl σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
σ.(heap) !! l = Some vl → vl ≠ v1 →
vals_cas_compare_safe vl v1 →
head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool false) σ []
head_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ LitBool false) σ []
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
σ.(heap) !! l = Some v1 →
vals_cas_compare_safe v1 v1 →
head_step (CAS (Lit $ LitLoc l) e1 e2) σ
None
[]
(Lit $ LitBool true) (state_upd_heap <[l:=v2]> σ)
[]
| FaaS l i1 e2 i2 σ :
to_val e2 = Some (LitV (LitInt i2)) →
σ.(heap) !! l = Some (LitV (LitInt i1)) →
head_step (FAA (Lit $ LitLoc l) e2) σ
None
[]
(Lit $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]> σ)
[]
| NewProphS σ p :
p ∉ σ.(used_proph) →
head_step NewProph σ
None
[]
(Lit $ LitProphecy p) (state_upd_used_proph ({[ p ]} ∪) σ)
[]
| ResolveProphS e1 p e2 v σ :
to_val e1 = Some (LitV $ LitProphecy p) →
to_val e2 = Some v →
head_step (ResolveProph e1 e2) σ (Some (p, v)) (Lit LitUnit) σ [].
head_step (ResolveProph e1 e2) σ [(p, v)] (Lit LitUnit) σ [].
(** Basic properties about the language *)
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
......@@ -553,12 +554,12 @@ Qed.
Lemma alloc_fresh e v σ :
let l := fresh (dom (gset loc) σ.(heap)) in
to_val e = Some v →
head_step (Alloc e) σ None (Lit (LitLoc l)) (state_upd_heap <[l:=v]> σ) [].
head_step (Alloc e) σ [] (Lit (LitLoc l)) (state_upd_heap <[l:=v]> σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
Lemma new_proph_fresh σ :
let p := fresh σ.(used_proph) in
head_step NewProph σ None (Lit $ LitProphecy p) (state_upd_used_proph ({[ p ]} ∪) σ) [].
head_step NewProph σ [] (Lit $ LitProphecy p) (state_upd_used_proph ({[ p ]} ∪) σ) [].
Proof. constructor. apply is_fresh. Qed.
(* Misc *)
......
theories/heap_lang/lifting.v
View file @ 25ed5c9c
......@@ -292,7 +292,6 @@ Lemma wp_resolve_proph e1 e2 p v w:
{{{ p ⥱ v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}.
Proof.
iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
unfold cons_obs. simpl.
iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
iSplit; first by eauto.
......
theories/program_logic/adequacy.v
View file @ 25ed5c9c
......@@ -73,7 +73,7 @@ Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
prim_step e1 σ1 κ e2 σ2 efs →
world' E σ1 (cons_obs κ κs) ∗ WP e1 @ s; E {{ Φ }}
world' E σ1 (κ ++ κs) ∗ WP e1 @ s; E {{ Φ }}
==∗ ▷ |==> ◇ (world' E σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
......@@ -85,7 +85,7 @@ Qed.
Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
step (e1 :: t1,σ1) κ (t2, σ2) →
world σ1 (cons_obs κ κs) ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
world σ1 (κ ++ κs) ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
==∗ ∃ e2 t2',
⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 κs ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
Proof.
......@@ -107,7 +107,7 @@ Proof.
revert e1 t1 κs κs' t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
{ inversion_clear 1; iIntros "?"; eauto 10. }
iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
rewrite /cons_obs. rewrite <- app_assoc.
rewrite <- app_assoc.
iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first by eauto; simplify_eq.
subst. iModIntro; iNext; iMod "H" as ">H". by iApply IH.
Qed.
......@@ -145,7 +145,7 @@ Proof.
rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
destruct (to_val e) as [v|] eqn:?.
{ iIntros "!> !> !%". left. by exists v. }
rewrite uPred_fupd_eq. iMod ("H" $! _ None with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
rewrite uPred_fupd_eq. iMod ("H" $! _ [] with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
iIntros "!> !> !%". by right.
Qed.
......
theories/program_logic/ectx_language.v
View file @ 25ed5c9c
......@@ -16,7 +16,7 @@ Section ectx_language_mixin.
Context (empty_ectx : ectx).
Context (comp_ectx : ectx → ectx → ectx).
Context (fill : ectx → expr → expr).
Context (head_step : expr → state → option observation → expr → state → list expr → Prop).
Context (head_step : expr → state → list observation → expr → state → list expr → Prop).
Record EctxLanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
......@@ -55,7 +55,7 @@ Structure ectxLanguage := EctxLanguage {
empty_ectx : ectx;
comp_ectx : ectx → ectx → ectx;
fill : ectx → expr → expr;
head_step : expr → state → option observation → expr → state → list expr → Prop;
head_step : expr → state → list observation → expr → state → list expr → Prop;
ectx_language_mixin :
EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
......@@ -100,7 +100,7 @@ Section ectx_language.
Definition head_reducible (e : expr Λ) (σ : state Λ) :=
∃ κ e' σ' efs, head_step e σ κ e' σ' efs.
Definition head_reducible_no_obs (e : expr Λ) (σ : state Λ) :=
∃ e' σ' efs, head_step e σ None e' σ' efs.
∃ e' σ' efs, head_step e σ [] e' σ' efs.
Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
∀ κ e' σ' efs, ¬head_step e σ κ e' σ' efs.
Definition head_stuck (e : expr Λ) (σ : state Λ) :=
......@@ -111,7 +111,7 @@ Section ectx_language.
Definition sub_redexes_are_values (e : expr Λ) :=
∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx.
Inductive prim_step (e1 : expr Λ) (σ1 : state Λ) (κ : option (observation Λ))
Inductive prim_step (e1 : expr Λ) (σ1 : state Λ) (κ : list (observation Λ))
(e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
Ectx_step K e1' e2' :
e1 = fill K e1' → e2 = fill K e2' →
......@@ -217,7 +217,7 @@ Section ectx_language.
Record pure_head_step (e1 e2 : expr Λ) := {
pure_head_step_safe σ1 : head_reducible_no_obs e1 σ1;
pure_head_step_det σ1 κ e2' σ2 efs :
head_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
head_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
}.
Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2 → pure_step e1 e2.
......
theories/program_logic/ectx_lifting.v
View file @ 25ed5c9c
......@@ -16,7 +16,7 @@ Hint Resolve head_stuck_stuck.
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
⌜head_reducible e1 σ1⌝ ∗
∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
......@@ -30,7 +30,7 @@ Qed.
Lemma wp_lift_head_step {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
......@@ -52,7 +52,7 @@ Qed.
Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
(∀ σ1, head_reducible e1 σ1) →
(∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
(∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
(|={E,E'}▷=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
......@@ -76,7 +76,7 @@ Qed.
Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=∗
⌜head_reducible e1 σ1⌝ ∗
∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
state_interp σ2 κs ∗
......@@ -91,7 +91,7 @@ Qed.
Lemma wp_lift_atomic_head_step {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
state_interp σ2 κs ∗
......@@ -106,7 +106,7 @@ Qed.
Lemma wp_lift_atomic__head_step_no_fork_fupd {s E1 E2 Φ} e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=∗
⌜head_reducible e1 σ1⌝ ∗
∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
......@@ -121,7 +121,7 @@ Qed.
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
......@@ -136,7 +136,7 @@ Qed.
Lemma wp_lift_pure_det_head_step {s E E' Φ} e1 e2 efs :
(∀ σ1, head_reducible e1 σ1) →
(∀ σ1 κ e2' σ2 efs',
head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
(|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
......@@ -148,7 +148,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
to_val e1 = None →
(∀ σ1, head_reducible e1 σ1) →
(∀ σ1 κ e2' σ2 efs',
head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
(|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
......@@ -159,7 +159,7 @@ Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
to_val e1 = None →
(∀ σ1, head_reducible e1 σ1) →
(∀ σ1 κ e2' σ2 efs',
head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
......
theories/program_logic/ectxi_language.v
View file @ 25ed5c9c
......@@ -31,7 +31,7 @@ Section ectxi_language_mixin.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (fill_item : ectx_item → expr → expr).
Context (head_step : expr → state → option observation → expr → state → list expr → Prop).
Context (head_step : expr → state → list observation → expr → state → list expr → Prop).
Record EctxiLanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
......@@ -59,7 +59,7 @@ Structure ectxiLanguage := EctxiLanguage {
of_val : val → expr;
to_val : expr → option val;
fill_item : ectx_item → expr → expr;
head_step : expr → state → option observation → expr → state → list expr → Prop;
head_step : expr → state → list observation → expr → state → list expr → Prop;
ectxi_language_mixin :
EctxiLanguageMixin of_val to_val fill_item head_step
......
theories/program_logic/language.v
View file @ 25ed5c9c
......@@ -8,7 +8,7 @@ Section language_mixin.
(** We annotate the reduction relation with observations [κ], which we will
use in the definition of weakest preconditions to predict future
observations and assert correctness of the predictions. *)
Context (prim_step : expr → state → option observation → expr → state → list expr → Prop).
Context (prim_step : expr → state → list observation → expr → state → list expr → Prop).
Record LanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
......@@ -24,7 +24,7 @@ Structure language := Language {
observation : Type;
of_val : val → expr;
to_val : expr → option val;
prim_step : expr → state → option observation → expr → state → list expr → Prop;
prim_step : expr → state → list observation → expr → state → list expr → Prop;
language_mixin : LanguageMixin of_val to_val prim_step
}.
Delimit Scope expr_scope with E.
......@@ -75,7 +75,7 @@ Section language.
∃ κ e' σ' efs, prim_step e σ κ e' σ' efs.
(* Total WP only permits reductions without observations *)
Definition reducible_no_obs (e : expr Λ) (σ : state Λ) :=
∃ e' σ' efs, prim_step e σ None e' σ' efs.
∃ e' σ' efs, prim_step e σ [] e' σ' efs.
Definition irreducible (e : expr Λ) (σ : state Λ) :=
∀ κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
Definition stuck (e : expr Λ) (σ : state Λ) :=
......@@ -97,7 +97,7 @@ Section language.
prim_step e σ κ e' σ' efs →
if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
Inductive step (ρ1 : cfg Λ) (κ : option (observation Λ)) (ρ2 : cfg Λ) : Prop :=
Inductive step (ρ1 : cfg Λ) (κ : list (observation Λ)) (ρ2 : cfg Λ) : Prop :=
| step_atomic e1 σ1 e2 σ2 efs t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1) →
ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) →
......@@ -105,17 +105,13 @@ Section language.
step ρ1 κ ρ2.
Hint Constructors step.
(* TODO (MR) introduce notation ::? for cons_obs and suggest for inclusion to stdpp? *)
Definition cons_obs {A} (x : option A) (xs : list A) :=
option_list x ++ xs.
Inductive nsteps : nat → cfg Λ → list (observation Λ) → cfg Λ → Prop :=
| nsteps_refl ρ :
nsteps 0 ρ [] ρ
| nsteps_l n ρ1 ρ2 ρ3 κ κs :
step ρ1 κ ρ2 →
nsteps n ρ2 κs ρ3 →
nsteps (S n) ρ1 (cons_obs κ κs) ρ3.
nsteps (S n) ρ1 (κ ++ κs) ρ3.
Hint Constructors nsteps.
Definition erased_step (ρ1 ρ2 : cfg Λ) := ∃ κ, step ρ1 κ ρ2.
......@@ -180,7 +176,7 @@ Section language.
Record pure_step (e1 e2 : expr Λ) := {
pure_step_safe σ1 : reducible_no_obs e1 σ1;
pure_step_det σ1 κ e2' σ2 efs :
prim_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
prim_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
}.
(* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
......
theories/program_logic/lifting.v
View file @ 25ed5c9c
......@@ -15,7 +15,7 @@ Hint Resolve reducible_no_obs_reducible.
Lemma wp_lift_step_fupd s E Φ e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
......@@ -39,7 +39,7 @@ Qed.
(** Derived lifting lemmas. *)
Lemma wp_lift_step s E Φ e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
......@@ -51,7 +51,7 @@ Qed.
Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
(∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
(∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
(|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
......@@ -82,7 +82,7 @@ Qed.
use the generic lemmas here. *)
Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
state_interp σ2 κs ∗
......@@ -102,7 +102,7 @@ Qed.
Lemma wp_lift_atomic_step {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
(∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
state_interp σ2 κs ∗
......@@ -117,7 +117,7 @@ Qed.
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
(∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
(∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
(|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
......
theories/program_logic/ownp.v
View file @ 25ed5c9c
......@@ -118,7 +118,7 @@ Section lifting.
Lemma ownP_lift_step s E Φ e1 :
(|={E,∅}=> ∃ σ1 κs, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗
▷ ownP_state σ1 ∗ ▷ ownP_obs κs ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗
▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = κ ++ κs'⌝ -∗
ownP_state σ2 ∗ ownP_obs κs'
={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
......@@ -158,7 +158,7 @@ Section lifting.
Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
(∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
(∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
(▷ ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
......@@ -176,7 +176,7 @@ Section lifting.
Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 κs :
(if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(▷ (ownP_state σ1 ∗ ownP_obs κs) ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗
▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = κ ++ κs'⌝ -∗
ownP_state σ2 -∗ ownP_obs κs' -∗
from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
......@@ -194,7 +194,7 @@ Section lifting.
(if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' →
κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
▷ (ownP_state σ1 ∗ ownP_obs (κ ++ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
......@@ -208,7 +208,7 @@ Section lifting.
(if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' →
κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
{{{ ▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs}}}.
{{{ ▷ (ownP_state σ1 ∗ ownP_obs (κ ++ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs}}}.
Proof.
intros. rewrite -(ownP_lift_atomic_det_step σ1 κ κs v2 σ2 []); [|done..].
rewrite big_sepL_nil right_id. apply bi.wand_intro_r. iIntros "[Hs Hs']".
......@@ -217,7 +217,7 @@ Section lifting.
Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
(∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
(∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤{{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
......@@ -227,7 +227,7 @@ Section lifting.
Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
(∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
(∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
......@@ -246,7 +246,7 @@ Section ectx_lifting.
Lemma ownP_lift_head_step s E Φ e1 :
(|={E,∅}=> ∃ σ1 κs, ⌜head_reducible e1 σ1⌝ ∗ ▷ (ownP_state σ1 ∗ ownP_obs κs) ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗
▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = κ ++ κs'⌝ -∗
ownP_state σ2 -∗ ownP_obs κs'
={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
......@@ -269,7 +269,7 @@ Section ectx_lifting.
Lemma ownP_lift_pure_head_step s E Φ e1 :
(∀ σ1, head_reducible e1 σ1) →
(∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
(∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
(▷ ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
......@@ -282,7 +282,7 @@ Section ectx_lifting.
Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 κs :
head_reducible e1 σ1 →
▷ (ownP_state σ1 ∗ ownP_obs κs) ∗ ▷ (∀ κ κs' e2 σ2 efs,
⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗ ownP_state σ2 -∗ ownP_obs κs' -∗
⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = κ ++ κs'⌝ -∗ ownP_state σ2 -∗ ownP_obs κs' -∗
from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
......@@ -296,7 +296,7 @@ Section ectx_lifting.
head_reducible e1 σ1 →
(∀ κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' →
κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
▷ (ownP_state σ1 ∗ ownP_obs (κ ++ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
......@@ -307,7 +307,7 @@ Section ectx_lifting.
head_reducible e1 σ1 →
(∀ κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' →
κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
{{{ ▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs }}}.
{{{ ▷ (ownP_state σ1 ∗ ownP_obs (κ ++ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs }}}.
Proof.
intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
by destruct s; eauto using reducible_not_val.
......@@ -315,7 +315,7 @@ Section ectx_lifting.
Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
(∀ σ1, head_reducible e1 σ1) →
(∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
(∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
......@@ -325,7 +325,7 @@ Section ectx_lifting.
Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
(∀ σ1, head_reducible e1 σ1) →
(∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
(∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
......
theories/program_logic/total_adequacy.v
View file @ 25ed5c9c
......@@ -13,7 +13,7 @@ Implicit Types e : expr Λ.
Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
(t1 : list (expr Λ)) : iProp Σ :=
(∀ t2 σ1 κ κs σ2, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
state_interp σ1 κs