Commit 8076fe39 authored by Robbert Krebbers's avatar Robbert Krebbers

Total weakest preconditions for heap_lang.

parent f7dc0953
......@@ -79,6 +79,7 @@ theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/counter.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
......
From iris.base_logic Require Export gen_heap.
From iris.program_logic Require Export weakestpre lifting.
From iris.program_logic Require Import ectx_lifting.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics.
From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
Import uPred.
(** Basic rules for language operations. *)
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
......@@ -39,8 +36,6 @@ Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : _ = of_val ?v |- _ =>
is_var v; destruct v; first[discriminate H|injection H as H]
| H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
......@@ -54,22 +49,6 @@ Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
Section lifting.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork s E e Φ :
Φ (LitV LitUnit) WP e @ s; {{ _, True }} WP Fork e @ s; E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
- by rewrite -step_fupd_intro // later_sep -(wp_value _ _ _ (Lit _)) // right_id.
- intros; inv_head_step; eauto.
Qed.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec :=
......@@ -79,48 +58,69 @@ Local Ltac solve_pure_exec :=
Class AsRec (e : expr) (f x : binder) (erec : expr) :=
as_rec : e = Rec f x erec.
Global Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
Global Instance AsRec_rec_locked_val v f x e :
Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
Instance AsRec_rec_locked_val v f x e :
AsRec (of_val v) f x e AsRec (of_val (locked v)) f x e.
Proof. by unlock. Qed.
Global Instance pure_rec f x (erec e1 e2 : expr)
Instance pure_rec f x (erec e1 e2 : expr)
`{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
Proof. unfold AsRec in *; solve_pure_exec. Qed.
Global Instance pure_unop op e v v' `{!IntoVal e v} :
Instance pure_unop op e v v' `{!IntoVal e v} :
PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
Proof. solve_pure_exec. Qed.
Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
Proof. solve_pure_exec. Qed.
Global Instance pure_if_true e1 e2 :
PureExec True (If (Lit (LitBool true)) e1 e2) e1.
Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
Proof. solve_pure_exec. Qed.
Global Instance pure_if_false e1 e2 :
PureExec True (If (Lit (LitBool false)) e1 e2) e2.
Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
Proof. solve_pure_exec. Qed.
Global Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
PureExec True (Fst (Pair e1 e2)) e1.
Proof. solve_pure_exec. Qed.
Global Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
PureExec True (Snd (Pair e1 e2)) e2.
Proof. solve_pure_exec. Qed.
Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
Proof. solve_pure_exec. Qed.
Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
Proof. solve_pure_exec. Qed.
Section lifting.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork s E e Φ :
Φ (LitV LitUnit) WP e @ s; {{ _, True }} WP Fork e @ s; E {{ Φ }}.
Proof.
iIntros "[HΦ He]".
iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
Qed.
Lemma twp_fork s E e Φ :
Φ (LitV LitUnit) WP e @ s; [{ _, True }] WP Fork e @ s; E [{ Φ }].
Proof.
iIntros "[HΦ He]".
iApply twp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
iIntros "!> /= {$He}". by iApply twp_value.
Qed.
(** Heap *)
Lemma wp_alloc s E e v :
IntoVal e v
......@@ -132,6 +132,16 @@ Proof.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_alloc s E e v :
IntoVal e v
[[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l v }]].
Proof.
iIntros (<-%of_to_val Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>"; iSplit; first by auto.
iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_load s E l q v :
{{{ l {q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l {q} v }}}.
......@@ -142,6 +152,15 @@ Proof.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_load s E l q v :
[[{ l {q} v }]] Load (Lit (LitLoc l)) @ s; E [[{ RET v; l {q} v }]].
Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_store s E l v' e v :
IntoVal e v
......@@ -154,6 +173,17 @@ Proof.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Lemma twp_store s E l v' e v :
IntoVal e v
[[{ l v' }]] Store (Lit (LitLoc l)) e @ s; E [[{ RET LitV LitUnit; l v }]].
Proof.
iIntros (<-%of_to_val Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Lemma wp_cas_fail s E l q v' e1 v1 e2 :
IntoVal e1 v1 AsVal e2 v' v1
......@@ -166,6 +196,17 @@ Proof.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_fail s E l q v' e1 v1 e2 :
IntoVal e1 v1 AsVal e2 v' v1
[[{ l {q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
[[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_suc s E l e1 v1 e2 v2 :
IntoVal e1 v1 IntoVal e2 v2
......@@ -179,6 +220,18 @@ Proof.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Lemma twp_cas_suc s E l e1 v1 e2 v2 :
IntoVal e1 v1 IntoVal e2 v2
[[{ l v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
[[{ RET LitV (LitBool true); l v2 }]].
Proof.
iIntros (<-%of_to_val <-%of_to_val Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Lemma wp_faa s E l i1 e2 i2 :
IntoVal e2 (LitV (LitInt i2))
......@@ -192,4 +245,16 @@ Proof.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Lemma twp_faa s E l i1 e2 i2 :
IntoVal e2 (LitV (LitInt i2))
[[{ l LitV (LitInt i1) }]] FAA (Lit (LitLoc l)) e2 @ s; E
[[{ RET LitV (LitInt i1); l LitV (LitInt (i1 + i2)) }]].
Proof.
iIntros (<-%of_to_val Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
End lifting.
This diff is collapsed.
From iris.program_logic Require Export total_adequacy.
From iris.heap_lang Require Export adequacy.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Definition heap_total Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; [{ v, ⌜φ v }]%I)
sn step ([e], σ).
Proof.
intros Hwp; eapply (twp_total _ _); iIntros (?) "".
iMod (gen_heap_init σ) as (?) "Hh".
iModIntro. iExists gen_heap_ctx; iFrame.
iApply (Hwp (HeapG _ _ _)).
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