Commit 11719e83 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak stuff.

parent e98404cb
......@@ -6,7 +6,6 @@ theories/lib/flock.v
theories/lib/locking_heap.v
theories/lib/U.v
theories/c_translation/monad.v
theories/c_translation/lifting.v
theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/tests/test1.v
From iris.heap_lang Require Export proofmode notation.
From iris_c.lib Require Export locking_heap flock.
From iris_c.c_translation Require Export monad.
Section lifting.
Context `{locking_heapG Σ, heapG Σ, flockG Σ}.
Lemma awp_value (ve : expr) (v : val) R Φ :
IntoVal ve v
Φ v -
awp (λ: <> <>, ve) R Φ.
Proof.
intros ?. rewrite -(of_to_val ve v); last done.
iIntros "HΦ". rewrite /awp. wp_value_head.
iIntros (γ π env lk) "Hfl Hunfl".
do 2 wp_rec. by iFrame.
Qed.
Lemma awp_pure K φ e1 e2 R Φ :
PureExec φ e1 e2
φ
awp (fill K e2) R Φ -
awp (fill K e1) R Φ.
Proof.
iIntros (? Hφ) "Hawp".
rewrite /awp.
wp_pure _.
done.
Qed.
Lemma awp_wand e (Φ Ψ : val iProp Σ) R :
awp e R Φ -
( v, Φ v - Ψ v) -
awp e R Ψ.
Proof.
iIntros "HAWP Hv".
rewrite /awp.
iApply (wp_wand with "HAWP").
iIntros (v) "HΦ".
iIntros (γ π env l) "#Hflock Hunfl".
iApply (wp_wand with "[HΦ Hunfl]"); first by iApply "HΦ".
iIntros (w) "[HΦ $]". by iApply "Hv".
Qed.
End lifting.
Notation "a ;;; b" := (a_bind (λ: <>, b) a)%E (at level 80, right associativity).
......@@ -13,6 +13,8 @@ Definition a_bind : val := λ: "f" "x" "env" "l",
let: "a" := "x" "env" "l" in
"f" "a" "env" "l".
Notation "a ;;; b" := (a_bind (λ: <>, b) a)%E (at level 80, right associativity).
(* M A → A *)
Definition a_run : val := λ: "x",
let: "env" := mset_create #() in
......@@ -56,11 +58,11 @@ Section a_wp.
Definition awp (e : expr)
(R : iProp Σ) (Φ : val iProp Σ) : iProp Σ :=
WP e {{ ev, (γ : flock_name) (π : frac) (env : val) (l : val),
tc_opaque (WP e {{ ev, (γ : flock_name) (π : frac) (env : val) (l : val),
is_flock amonadN γ l (env_inv env R) -
unflocked γ π -
WP ev env l {{ v, Φ v unflocked γ π }}
}}%I.
}})%I.
End a_wp.
Section a_wp_rules.
......@@ -68,7 +70,7 @@ Section a_wp_rules.
Lemma a_wp_awp R Φ Ψ e : awp e R Φ - ( v : val, awp v R Φ - Ψ v) - WP e {{ Ψ }}.
Proof.
iIntros "Hwp H". iApply (wp_wand with "Hwp").
iIntros "Hwp H". rewrite /awp /=. iApply (wp_wand with "Hwp").
iIntros (v) "Hwp". iApply "H". by iApply wp_value'.
Qed.
......@@ -76,10 +78,37 @@ Section a_wp_rules.
WP e {{ v, awp (fill K (of_val v)) R Φ }} awp (fill K e) R Φ.
Proof. by apply: wp_bind. Qed.
Lemma wp_awp_bind_inv R Φ K e :
awp (fill K e) R Φ WP e {{ v, awp (fill K (of_val v)) R Φ }}.
Proof. by apply: wp_bind_inv. Qed.
Lemma awp_wand e (Φ Ψ : val iProp Σ) R :
awp e R Φ -
( v, Φ v - Ψ v) -
awp e R Ψ.
Proof.
iIntros "HAWP Hv". rewrite /awp /=.
iApply (wp_wand with "HAWP").
iIntros (v) "HΦ".
iIntros (γ π env l) "#Hflock Hunfl".
iApply (wp_wand with "[HΦ Hunfl]"); first by iApply "HΦ".
iIntros (w) "[HΦ $]". by iApply "Hv".
Qed.
Lemma awp_pure K φ e1 e2 R Φ :
PureExec φ e1 e2
φ
awp (fill K e2) R Φ -
awp (fill K e1) R Φ.
Proof.
iIntros (? Hφ) "Hawp". iApply wp_awp_bind. wp_pure _.
by iApply wp_awp_bind_inv.
Qed.
Lemma awp_ret e R Φ :
WP e {{ Φ }} - awp (a_ret e) R Φ.
Proof.
iIntros "Hwp". rewrite /awp /a_ret. wp_apply (wp_wand with "Hwp").
iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp").
iIntros (v) "HΦ". wp_lam.
iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam. iFrame.
Qed.
......@@ -90,7 +119,7 @@ Section a_wp_rules.
awp e R (λ ev, awp (fv ev) R Φ) -
awp (a_bind f e) R Φ.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_bind. wp_lam. wp_bind e.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam. wp_bind (ev env l).
iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
......@@ -103,7 +132,7 @@ Section a_wp_rules.
(R - R', R' awp (ev #()) R' (λ w, R' - R Φ w)) -
awp (a_atomic e) R Φ.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic. wp_lam.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
iIntros (γ π env l) "#Hlock1 Hunfl1". do 2 wp_let.
wp_apply (acquire_cancel_spec with "[$]").
iIntros "[Hflkd [Henv HR]] /=". wp_seq.
......@@ -125,7 +154,7 @@ Section a_wp_rules.
WP ev env {{ w, env_inv env R Φ w }}) -
awp (a_atomic_env e) R Φ.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env. wp_lam.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam.
wp_apply (acquire_cancel_spec with "[$]").
iIntros "[Hflkd [Henv HR]] /=". wp_seq.
......@@ -145,7 +174,7 @@ Section a_wp_rules.
awp (a_par e1 e2) R Φ.
Proof.
iIntros (<-%of_to_val <-%of_to_val) "Hwp1 Hwp2 HΦ".
rewrite /awp /a_par. do 2 wp_lam.
rewrite /awp /a_par /=. do 2 wp_lam.
iIntros (γ π env l) "#Hlock [Hunfl1 Hunfl2]". do 2 wp_lam.
iApply (par_spec (λ v, Ψ1 v unflocked _ (π/2))%I
(λ v, Ψ2 v unflocked _ (π/2))%I
......@@ -166,7 +195,7 @@ Section a_wp_run.
R - ( `{locking_heapG Σ}, awp v R (λ w, R ={}= Φ w)) -
WP a_run v {{ Φ }}.
Proof.
iIntros "HR Hwp". rewrite /a_run /=. wp_let.
iIntros "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σ".
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris_c.lib Require Import locking_heap mset flock.
From iris_c.c_translation Require Export monad lifting.
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 :
......
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
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 monad lifting proofmode.
From iris_c.c_translation Require Import proofmode.
Definition a_alloc : val := λ: "x",
a_bind (λ: "v", a_atomic_env (λ: <>, ref "v")) "x".
......
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
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 monad lifting proofmode translation.
From iris_c.c_translation Require Import proofmode translation.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
......@@ -125,7 +125,7 @@ Section test.
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
iIntros (? ? ->) "[% Hr]"; subst.
Opaque awp.
iExists _; iFrame. iIntros "Hl2".
awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
Qed.
......@@ -137,67 +137,5 @@ Section test.
l U #n -
awp (incr1 #l) R (λ _, l L #(n+1)).
Proof.
iIntros "Hl". awp_lam.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
awp_pure _.
iApply awp_bind.
iApply (awp_par (λ v, v = #l) (λ v, v = #(n+1) l U #n) with "[] [Hl]")%I.
- by iApply awp_value.
- Transparent awp. rewrite /awp.
iApply wp_value.
iIntros (γ π env lk) "#Hlock1 Hunfl1". do 2 wp_let.
Opaque par.
repeat wp_pure _.
admit.
- iNext. iIntros (? ?) "% [% Hl]"; simplify_eq.
iNext. awp_lam.
(* a_store_spec copypasta ahead *)
iApply awp_atomic_env.
iIntros (env) "Henv HR". wp_lam.
{ rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
assert (#l X).
{ unfold correct_locks in *. intros Hx. apply Hl.
destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
wp_proj.
wp_apply (mset_add_spec with "[$HX]"); eauto.
iIntros "HX". wp_seq.
iAssert (⌜σ !! l = Some ULvl%I) with "[Hσ Hl]" as %?.
{ rewrite mapsto_eq /mapsto_def.
iDestruct "Hl" as "[Hv Hl]".
by iDestruct (own_valid_2 with "Hσ Hl")
as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hl") as "[Hσ Hl]".
do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
iDestruct "Hl" as "[Hv Hl]".
rewrite (bi.big_sepM_lookup_acc _ _ l ULvl); last done.
iDestruct "Hls" as "[Hl' Hls]".
iDestruct "Hl'" as (?) "Hl'".
iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->.
iCombine "Hv Hl'" as "Hv".
wp_store.
iDestruct "Hv" as "[Hv Hl']".
iSpecialize ("Hls" with "[Hl']"); eauto.
wp_proj. iFrame "HR". iSplitR "Hl Hv".
- iExists ({[#l]} X),(<[l:=LLvl]> σ). iFrame. iSplitL.
+ rewrite -bi.big_sepM_insert_override; eauto.
+ (* TODO: a separate lemma somewhere *)
iPureIntro. rewrite locked_locs_lock.
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
- iFrame. }
Admitted.
End test.
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