Commit 51a28faa authored by Dan Frumin's avatar Dan Frumin

Organize all the necessary functors into a single one

- amonadG Σ
- + clean up a bit
parent 19d36a41
......@@ -4,9 +4,8 @@ From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation.
Section Derived.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Section derived.
Context `{amonadG Σ}.
Lemma a_load_ret (l: loc) (q : Qp) (w: val) R Φ:
l U{q} w (l U{q} w - Φ w) -
......@@ -59,17 +58,14 @@ Section Derived.
Qed.
Lemma a_move_spec (s t :loc) (v w: val) R Φ :
s U v t U w ( t U w - s L w - Φ w) -
s U v t U w ( t U w - s L w - Φ w) -
awp (a_store (a_ret #s) (a_load (a_ret #t))) R Φ.
Proof.
iIntros "(Hs & Ht & H)".
iApply a_store_ret. awp_load_ret t. iIntros "Ht".
iExists v. iFrame. iSpecialize ("H" with "Ht"). done.
Qed.
End Derived.
End derived.
Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.
Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
......
......@@ -42,8 +42,15 @@ Definition a_par : val := λ: "x" "y" "env" "l",
Definition amonadN := nroot .@ "amonad".
Class amonadG (Σ : gFunctors) := AMonadG {
aheapG :> heapG Σ;
aflockG :> flockG Σ;
alocking_heapG :> locking_heapG Σ;
aspawnG :> spawnG Σ
}.
Section a_wp.
Context `{heapG Σ, flockG Σ, locking_heapG Σ}.
Context `{amonadG Σ}.
(* X ⊆ σ^{-1}(L) *)
Definition correct_locks (X : gset val) (preσ : gset loc) : Prop :=
......@@ -66,7 +73,7 @@ Section a_wp.
End a_wp.
Section a_wp_rules.
Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapG Σ}.
Context `{amonadG Σ}.
Lemma a_wp_awp R Φ Ψ e : awp e R Φ - ( v : val, awp v R Φ - Ψ v) - WP e {{ Ψ }}.
Proof.
......@@ -192,16 +199,18 @@ Section a_wp_run.
Lemma awp_run (e : expr) R Φ :
AsVal e
R - ( `{locking_heapG Σ}, awp e R (λ w, R ={}= Φ w)) -
R - ( `{amonadG Σ}, awp e R (λ w, R ={}= Φ w)) -
WP a_run e {{ Φ }}.
Proof.
iIntros ([ev <-%of_to_val]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
wp_bind (mset_create #()). iApply mset_create_spec; first done.
iNext. iIntros (env) "Henv". wp_let.
iMod (locking_heap_init ) as (?) "Hσ".
pose (amg := AMonadG Σ _ _ _ _).
wp_apply (newlock_cancel_spec amonadN (env_inv env R)%I with "[Henv Hσ $HR]").
{ iExists , . iFrame. eauto. }
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
iSpecialize ("Hwp" $! amg).
wp_apply (wp_wand with "Hwp"). iIntros (v') "Hwp".
iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
iIntros (w) "[HΦ Hunfl]".
......
......@@ -4,7 +4,7 @@ From iris_c.lib Require Import locking_heap mset flock.
From iris_c.c_translation Require Export monad.
From iris.proofmode Require Import coq_tactics.
Lemma tac_awp_bind `{locking_heapG Σ, heapG Σ, flockG Σ} K Δ R Φ e f :
Lemma tac_awp_bind `{amonadG Σ} K Δ R Φ e f :
f = (λ e, fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e {{ v, awp (f (of_val v)) R Φ }})%I
envs_entails Δ (awp (fill K e) R Φ).
......@@ -28,7 +28,7 @@ Tactic Notation "awp_apply" open_constr(lem) :=
| _ => fail "awp_apply: not a 'awp'"
end).
Lemma tac_awp_pure `{locking_heapG Σ, heapG Σ, flockG Σ} Δ Δ' K e1 e2 e φ R Φ :
Lemma tac_awp_pure `{amonadG Σ} Δ Δ' K e1 e2 e φ R Φ :
e = fill K e1
PureExec φ e1 e2
φ
......
......@@ -51,7 +51,7 @@ Definition a_while: val :=
a_if ("cnd" #()) (λ:<>, "bdy" #() ;;;; "while" "cnd" "bdy") a_seq%E.
Section proofs.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Context `{amonadG Σ}.
Lemma a_alloc_spec R Φ e :
awp e R (λ v, l, l U v - Φ #l) -
......
......@@ -24,7 +24,7 @@ Definition factorial : val := λ: "n",
Section factorial_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Context `{amonadG Σ}.
Lemma incr_spec (l : loc) (n : Z) R Φ :
l U #n - (l L #(n+1) - Φ #(n+1)) -
......
......@@ -18,7 +18,7 @@ Definition gcd : val := λ: "a" "b",
Section gcd_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Context `{amonadG Σ}.
Lemma gcd_spec (a b : Z) (l r: loc) R :
0 a 0 b
......
......@@ -56,7 +56,7 @@ Definition in_place_reverse : val := λ: "hd",
Section list_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Context `{amonadG Σ}.
Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
match xs with
......@@ -86,7 +86,7 @@ Section list_spec.
End list_spec.
Section InPlaceReversal.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Context `{amonadG Σ}.
Lemma a_list_store_next_spec e1 e2 Ψ1 Ψ2 R Φ :
......
......@@ -5,8 +5,7 @@ From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Context `{amonadG Σ}.
Lemma test1 (l : loc) :
l L #1 -
......
......@@ -6,7 +6,7 @@ From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Context `{amonadG Σ}.
Lemma test_fractional (x : loc) :
x U #1 -
......
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