Commit e2d12989 authored by David Swasey's avatar David Swasey

Define type pbit for readable adequacy lemmas.

parent 3742f4c2
......@@ -16,7 +16,7 @@ Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
( `{heapG Σ}, WP e {{ v, ⌜φ v }}%I)
adequate true e σ φ.
adequate progress e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
......
......@@ -27,7 +27,7 @@ Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp true ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
| |- envs_entails _ (wp progress ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
unify e' efoc;
eapply (tac_wp_pure K);
[simpl; apply _ (* PureExec *)
......@@ -66,7 +66,7 @@ Ltac wp_bind_core K :=
Tactic Notation "wp_bind" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp true ?E ?e ?Q) =>
| |- envs_entails _ (wp progress ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
|| fail "wp_bind: cannot find" efoc "in" e
| _ => fail "wp_bind: not a 'wp'"
......@@ -151,7 +151,7 @@ End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
iPoseProofCore lem as false true (fun H =>
lazymatch goal with
| |- envs_entails _ (wp true ?E ?e ?Q) =>
| |- envs_entails _ (wp progress ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
lazymatch iTypeOf H with
......@@ -163,7 +163,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp true ?E ?e ?Q) =>
| |- envs_entails _ (wp progress ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
......@@ -182,7 +182,7 @@ Tactic Notation "wp_alloc" ident(l) :=
Tactic Notation "wp_load" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp true ?E ?e ?Q) =>
| |- envs_entails _ (wp progress ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K))
|fail 1 "wp_load: cannot find 'Load' in" e];
......@@ -196,7 +196,7 @@ Tactic Notation "wp_load" :=
Tactic Notation "wp_store" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp true ?E ?e ?Q) =>
| |- envs_entails _ (wp progress ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_store _ _ _ _ _ K); [apply _|..])
......@@ -212,7 +212,7 @@ Tactic Notation "wp_store" :=
Tactic Notation "wp_cas_fail" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp true ?E ?e ?Q) =>
| |- envs_entails _ (wp progress ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..])
......@@ -228,7 +228,7 @@ Tactic Notation "wp_cas_fail" :=
Tactic Notation "wp_cas_suc" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp true ?E ?e ?Q) =>
| |- envs_entails _ (wp progress ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
......
......@@ -34,24 +34,24 @@ Proof.
Qed.
(* Program logic adequacy *)
Record adequate {Λ} (p : bool) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ Prop) := {
Record adequate {Λ} (p : pbit) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ Prop) := {
adequate_result t2 σ2 v2 :
rtc step ([e1], σ1) (of_val v2 :: t2, σ2) φ v2;
adequate_safe t2 σ2 e2 :
p
p = progress
rtc step ([e1], σ1) (t2, σ2)
e2 t2 progressive e2 σ2
}.
Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
adequate true e1 σ1 φ
adequate progress e1 σ1 φ
rtc step ([e1], σ1) (t2, σ2)
Forall (λ e, is_Some (to_val e)) t2 t3 σ3, step (t2, σ2) (t3, σ3).
Proof.
intros Had ?.
destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
destruct (adequate_safe true e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
destruct (adequate_safe progress e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
rewrite ?eq_None_not_Some; auto.
{ exfalso. eauto. }
destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
......@@ -59,7 +59,7 @@ Proof.
Qed.
Section adequacy.
Context `{irisG Λ Σ} (p : bool).
Context `{irisG Λ Σ} (p : pbit).
Implicit Types e : expr Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
......@@ -187,7 +187,7 @@ Proof.
iMod wsat_alloc as (Hinv) "[Hw HE]".
rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]".
iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate) true); eauto with iFrame.
iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate) progress); eauto with iFrame.
Qed.
Theorem wp_invariance Σ Λ `{invPreG Σ} p e σ1 t2 σ2 φ :
......
......@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
Section wp.
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
Implicit Types p : bool.
Implicit Types p : pbit.
Implicit Types P : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types v : val.
......
......@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export viewshifts.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Definition ht `{irisG Λ Σ} (p : bool) (E : coPset) (P : iProp Σ)
Definition ht `{irisG Λ Σ} (p : pbit) (E : coPset) (P : iProp Σ)
(e : expr Λ) (Φ : val Λ iProp Σ) : iProp Σ :=
( (P - WP e @ p; E {{ Φ }}))%I.
Instance: Params (@ht) 5.
......@@ -11,38 +11,38 @@ Instance: Params (@ht) 5.
Notation "{{ P } } e @ p ; E {{ Φ } }" := (ht p E P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e @ p ; E {{ Φ } }") : C_scope.
Notation "{{ P } } e @ E {{ Φ } }" := (ht true E P%I e%E Φ%I)
Notation "{{ P } } e @ E {{ Φ } }" := (ht progress E P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e @ E {{ Φ } }") : C_scope.
Notation "{{ P } } e @ E ? {{ Φ } }" := (ht false E P%I e%E Φ%I)
Notation "{{ P } } e @ E ? {{ Φ } }" := (ht noprogress E P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e @ E ? {{ Φ } }") : C_scope.
Notation "{{ P } } e {{ Φ } }" := (ht true P%I e%E Φ%I)
Notation "{{ P } } e {{ Φ } }" := (ht progress P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e {{ Φ } }") : C_scope.
Notation "{{ P } } e ? {{ Φ } }" := (ht false P%I e%E Φ%I)
Notation "{{ P } } e ? {{ Φ } }" := (ht noprogress P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e ? {{ Φ } }") : C_scope.
Notation "{{ P } } e @ p ; E {{ v , Q } }" := (ht p E P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
format "{{ P } } e @ p ; E {{ v , Q } }") : C_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (ht true E P%I e%E (λ v, Q)%I)
Notation "{{ P } } e @ E {{ v , Q } }" := (ht progress E P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
format "{{ P } } e @ E {{ v , Q } }") : C_scope.
Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht false E P%I e%E (λ v, Q)%I)
Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht noprogress E P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
format "{{ P } } e @ E ? {{ v , Q } }") : C_scope.
Notation "{{ P } } e {{ v , Q } }" := (ht true P%I e%E (λ v, Q)%I)
Notation "{{ P } } e {{ v , Q } }" := (ht progress P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
format "{{ P } } e {{ v , Q } }") : C_scope.
Notation "{{ P } } e ? {{ v , Q } }" := (ht false P%I e%E (λ v, Q)%I)
Notation "{{ P } } e ? {{ v , Q } }" := (ht noprogress P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
format "{{ P } } e ? {{ v , Q } }") : C_scope.
Section hoare.
Context `{irisG Λ Σ}.
Implicit Types p : bool.
Implicit Types p : pbit.
Implicit Types P Q : iProp Σ.
Implicit Types Φ Ψ : val Λ iProp Σ.
Implicit Types v : val Λ.
......@@ -77,7 +77,7 @@ Proof.
Qed.
Lemma ht_atomic' p E1 E2 P P' Φ Φ' e :
StronglyAtomic e p Atomic e
StronglyAtomic e p = progress Atomic e
(P ={E1,E2}=> P') {{ P' }} e @ p; E2 {{ Φ' }} ( v, Φ' v ={E2,E1}=> Φ v)
{{ P }} e @ p; E1 {{ Φ }}.
Proof.
......
......@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
Section lifting.
Context `{irisG Λ Σ}.
Implicit Types p : bool.
Implicit Types p : pbit.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
......
......@@ -70,7 +70,7 @@ Qed.
(** Lifting *)
Section lifting.
Context `{ownPG Λ Σ}.
Implicit Types p : bool.
Implicit Types p : pbit.
Implicit Types e : expr Λ.
Implicit Types Φ : val Λ iProp Σ.
......@@ -197,7 +197,7 @@ Section ectx_lifting.
Import ectx_language.
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
Context `{ownPG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
Implicit Types p : bool.
Implicit Types p : pbit.
Implicit Types Φ : val iProp Σ.
Implicit Types e : expr.
Hint Resolve head_prim_reducible head_reducible_prim_step.
......
......@@ -11,7 +11,9 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
}.
Notation irisG Λ Σ := (irisG' (state Λ) Σ).
Definition wp_pre `{irisG Λ Σ} (p : bool)
CoInductive pbit := progress | noprogress.
Definition wp_pre `{irisG Λ Σ} (p : pbit)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
......@@ -41,32 +43,32 @@ Instance: Params (@wp) 6.
Notation "'WP' e @ p ; E {{ Φ } }" := (wp p E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ p ; E {{ Φ } } ']'") : uPred_scope.
Notation "'WP' e @ E {{ Φ } }" := (wp true E e%E Φ)
Notation "'WP' e @ E {{ Φ } }" := (wp progress E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ E {{ Φ } } ']'") : uPred_scope.
Notation "'WP' e @ E ? {{ Φ } }" := (wp false E e%E Φ)
Notation "'WP' e @ E ? {{ Φ } }" := (wp noprogress E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ E ? {{ Φ } } ']'") : uPred_scope.
Notation "'WP' e {{ Φ } }" := (wp true e%E Φ)
Notation "'WP' e {{ Φ } }" := (wp progress e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' {{ Φ } } ']'") : uPred_scope.
Notation "'WP' e ? {{ Φ } }" := (wp false e%E Φ)
Notation "'WP' e ? {{ Φ } }" := (wp noprogress e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' ? {{ Φ } } ']'") : uPred_scope.
Notation "'WP' e @ p ; E {{ v , Q } }" := (wp p E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' @ p ; E {{ v , Q } } ']'") : uPred_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp true E e%E (λ v, Q))
Notation "'WP' e @ E {{ v , Q } }" := (wp progress E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' @ E {{ v , Q } } ']'") : uPred_scope.
Notation "'WP' e @ E ? {{ v , Q } }" := (wp false E e%E (λ v, Q))
Notation "'WP' e @ E ? {{ v , Q } }" := (wp noprogress E e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' @ E ? {{ v , Q } } ']'") : uPred_scope.
Notation "'WP' e {{ v , Q } }" := (wp true e%E (λ v, Q))
Notation "'WP' e {{ v , Q } }" := (wp progress e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' {{ v , Q } } ']'") : uPred_scope.
Notation "'WP' e ? {{ v , Q } }" := (wp false e%E (λ v, Q))
Notation "'WP' e ? {{ v , Q } }" := (wp noprogress e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' ? {{ v , Q } } ']'") : uPred_scope.
......@@ -165,7 +167,7 @@ Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
Section wp.
Context `{irisG Λ Σ}.
Implicit Types p : bool.
Implicit Types p : pbit.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types v : val Λ.
......@@ -234,7 +236,7 @@ Lemma wp_fupd p E e Φ : WP e @ p; E {{ v, |={E}=> Φ v }} ⊢ WP e @ p; E {{ Φ
Proof. iIntros "H". iApply (wp_strong_mono p E); try iFrame; auto. Qed.
Lemma wp_atomic' p E1 E2 e Φ :
StronglyAtomic e p Atomic e
StronglyAtomic e p = progress Atomic e
(|={E1,E2}=> WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }}) WP e @ p; E1 {{ Φ }}.
Proof.
iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
......
......@@ -86,5 +86,5 @@ Section LiftingTests.
Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
End LiftingTests.
Lemma heap_e_adequate σ : adequate true heap_e σ (= #2).
Lemma heap_e_adequate σ : adequate progress heap_e σ (= #2).
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment