Commit bd9a61e5 authored by Ralf Jung's avatar Ralf Jung
Browse files

make inv_heapG part of heapG

parent e2407f9f
...@@ -204,7 +204,7 @@ Section tests. ...@@ -204,7 +204,7 @@ Section tests.
End tests. End tests.
Section notation_tests. Section notation_tests.
Context `{!heapG Σ, !inv_heapG Σ}. Context `{!heapG Σ}.
(* Make sure these parse and type-check. *) (* Make sure these parse and type-check. *)
Lemma inv_mapsto_own_test (l : loc) : l _(λ _, True) #5. Abort. Lemma inv_mapsto_own_test (l : loc) : l _(λ _, True) #5. Abort.
...@@ -274,4 +274,4 @@ Section error_tests. ...@@ -274,4 +274,4 @@ Section error_tests.
End error_tests. End error_tests.
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2). Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed. Proof. eapply (heap_adequacy heapΣ)=> ?. iIntros "_". by iApply heap_e_spec. Qed.
...@@ -124,7 +124,7 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ]. ...@@ -124,7 +124,7 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
(** This lemma implicitly shows that these functors are enough to meet (** This lemma implicitly shows that these functors are enough to meet
all library assumptions. *) all library assumptions. *)
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True). Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed. Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
(* Since we check the output of the test files, this means (* Since we check the output of the test files, this means
our test suite will fail if we ever accidentally add an axiom our test suite will fail if we ever accidentally add an axiom
......
...@@ -142,4 +142,4 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ]. ...@@ -142,4 +142,4 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
(** This lemma implicitly shows that these functors are enough to meet (** This lemma implicitly shows that these functors are enough to meet
all library assumptions. *) all library assumptions. *)
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True). Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed. Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
...@@ -113,7 +113,7 @@ Section to_inv_heap. ...@@ -113,7 +113,7 @@ Section to_inv_heap.
Qed. Qed.
End to_inv_heap. End to_inv_heap.
Lemma inv_heap_init {L V : Type} `{Countable L, !invG Σ, !gen_heapG L V Σ, !inv_heapPreG L V Σ} E: Lemma inv_heap_init (L V : Type) `{Countable L, !invG Σ, !gen_heapG L V Σ, !inv_heapPreG L V Σ} E :
|==> _ : inv_heapG L V Σ, |={E}=> inv_heap_inv L V. |==> _ : inv_heapG L V Σ, |={E}=> inv_heap_inv L V.
Proof. Proof.
iMod (own_alloc ( (to_inv_heap ))) as (γ) "H●". iMod (own_alloc ( (to_inv_heap ))) as (γ) "H●".
......
...@@ -7,23 +7,25 @@ Set Default Proof Using "Type". ...@@ -7,23 +7,25 @@ Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG { Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ; heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ; heap_preG_heap :> gen_heapPreG loc val Σ;
heap_preG_inv_heap :> inv_heapPreG loc val Σ;
heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ; heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ;
}. }.
Definition heapΣ : gFunctors := Definition heapΣ : gFunctors :=
#[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)]. #[invΣ; gen_heapΣ loc val; inv_heapΣ loc val; proph_mapΣ proph_id (val * val)].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ. Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ : Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
( `{!heapG Σ}, WP e @ s; {{ v, ⌜φ v }}) ( `{!heapG Σ}, inv_heap_inv - WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v). adequate s e σ (λ v _, φ v).
Proof. Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "". intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh". iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (inv_heap_init loc val) as (?) ">Hi".
iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp". iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
iModIntro. iExists iModIntro. iExists
(λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I), (λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I),
(λ _, True%I). (λ _, True%I).
iFrame. iApply (Hwp (HeapG _ _ _ _)). iFrame. iApply (Hwp (HeapG _ _ _ _ _)). done.
Qed. Qed.
...@@ -11,6 +11,7 @@ Set Default Proof Using "Type". ...@@ -11,6 +11,7 @@ Set Default Proof Using "Type".
Class heapG Σ := HeapG { Class heapG Σ := HeapG {
heapG_invG : invG Σ; heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ; heapG_gen_heapG :> gen_heapG loc val Σ;
heapG_inv_heapG :> inv_heapG loc val Σ;
heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ; heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
}. }.
...@@ -34,7 +35,6 @@ Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type) ...@@ -34,7 +35,6 @@ Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
(at level 20, format "l ↦□ I") : bi_scope. (at level 20, format "l ↦□ I") : bi_scope.
Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type) Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
(at level 20, I at level 9, format "l ↦_ I v") : bi_scope. (at level 20, I at level 9, format "l ↦_ I v") : bi_scope.
Notation inv_heapG := (inv_heapG loc val).
Notation inv_heap_inv := (inv_heap_inv loc val). Notation inv_heap_inv := (inv_heap_inv loc val).
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
......
...@@ -5,15 +5,16 @@ From iris.heap_lang Require Import proofmode notation. ...@@ -5,15 +5,16 @@ From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Definition heap_total Σ `{!heapPreG Σ} s e σ φ : Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
( `{!heapG Σ}, WP e @ s; [{ v, ⌜φ v }]) ( `{!heapG Σ}, inv_heap_inv - WP e @ s; [{ v, ⌜φ v }])
sn erased_step ([e], σ). sn erased_step ([e], σ).
Proof. Proof.
intros Hwp; eapply (twp_total _ _); iIntros (?) "". intros Hwp; eapply (twp_total _ _); iIntros (?) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh". iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (inv_heap_init loc val) as (?) ">Hi".
iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp". iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
iModIntro. iModIntro.
iExists iExists
(λ σ κs _, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I), (λ σ κs _, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I),
(λ _, True%I); iFrame. (λ _, True%I); iFrame.
iApply (Hwp (HeapG _ _ _ _)). iApply (Hwp (HeapG _ _ _ _ _)). done.
Qed. 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