From iris.heap_lang Require Export proofmode notation. From iris.heap_lang Require Import adequacy spin_lock assert par. From iris.algebra Require Import frac. From iris_c.lib Require Import mset flock locking_heap. (* M A := ref (list loc) → Mutex → A *) (* A → M A *) Definition a_ret : val := λ: "a" <> <>, "a". (* (A → M B) → M A → M B *) 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 let: "l" := newlock #() in "x" "env" "l". (* M A → M A *) Definition a_atomic : val := λ: "x" "env" "l", acquire "l";; let: "k" := newlock #() in let: "a" := "x" #() "env" "k" in release "l";; "a". (* (ref (list loc) → A) → M A *) Definition a_atomic_env : val := λ: "f" "env" "l", acquire "l";; let: "a" := "f" "env" in release "l";; "a". (* M A → M B → M (A * B) *) Definition a_par : val := λ: "x" "y" "env" "l", "x" "env" "l" ||| "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 `{amonadG Σ}. (* X ⊆ σ^{-1}(L) *) Definition correct_locks (X : gset val) (preσ : gset loc) : Prop := set_Forall (λ v, ∃ l : loc, v = #l ∧ l ∈ preσ) X. Definition env_inv (env : val) : iProp Σ := (∃ (X : gset val) (σ : gmap loc level), is_set_mut env X ∗ full_locking_heap σ ∗ ([∗ map] l ↦ _ ∈ σ, ∃ v', l ↦{1/2} v') ∗ ⌜correct_locks X (locked_locs σ)⌝)%I. Definition awp (e : expr) (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ := tc_opaque (WP e {{ ev, ∀ (γ : flock_name) (π : frac) (env : val) (l : val) s, is_flock amonadN γ l -∗ flock_res γ s (env_inv env ∗ R) -∗ unflocked γ π -∗ WP ev env l {{ v, Φ v ∗ unflocked γ π }} }})%I. Global Instance elim_bupd_awp p e Φ : ElimModal True p false (|==> P) P (awp e R Φ) (awp e R Φ). Proof. iIntros (P R _) "[HP HA]". rewrite /awp /tc_opaque. destruct p; simpl; [ iDestruct "HP" as "#HP" | ]; iMod "HP"; by iApply "HA". Qed. End a_wp. Section a_wp_rules. Context `{amonadG Σ}. Lemma a_wp_awp R Φ Ψ e : awp e R Φ -∗ (∀ v : val, awp v R Φ -∗ Ψ v) -∗ WP e {{ Ψ }}. Proof. iIntros "Hwp H". rewrite /awp /=. iApply (wp_wand with "Hwp"). iIntros (v) "Hwp". iApply "H". by iApply wp_value'. Qed. Lemma wp_awp_bind R Φ K e : 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 s) "#Hflock #Hres 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 (v) "HΦ". wp_lam. iIntros (γ π env l s) "#Hlock #Hres Hunfl". do 2 wp_lam. iFrame. Qed. Lemma awp_bind (f e : expr) R Φ : AsVal f → awp e R (λ ev, awp (f ev) R Φ) -∗ awp (a_bind f e) R Φ. Proof. iIntros ([fv <-%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 s) "#Hlock #Hres Hunfl". do 2 wp_lam. wp_bind (ev env l). iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp". iIntros (w) "[Hwp Hunfl]". wp_let. wp_apply (wp_wand with "Hwp"). iIntros (v) "H". by iApply ("H" with "[\$]"). Qed. Lemma awp_atomic (e : expr) (ev : val) R Φ : IntoVal e ev → (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 (γ π env l s) "#Hlock1 #Hres Hunfl1". do 2 wp_let. wp_apply (acquire_cancel_spec with "[\$]"). iIntros (f) "([Henv HR] & Hcl)". wp_seq. iDestruct ("Hwp" with "HR") as (R') "[HR' Hwp]". wp_apply (newlock_cancel_spec amonadN); first done. iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let. iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env ∗ R')%I with "Hlock2 Hunfl2 [\$Henv \$HR']") as (s') "[#Hres2 Hunfl2]". wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _). iApply (wp_wand with "[Hwp Hunfl2]"); first by iApply "Hwp". iIntros (w) "[HR Hunfl2]". iMod (cancel_lock with "Hlock2 Hres2 Hunfl2") as "[Henv HR']". wp_let. iDestruct ("HR" with "HR'") as "[HR HΦ]". wp_apply (release_cancel_spec with "[\$Hlock1 Hcl Henv HR]"). { iApply "Hcl". by iNext; iFrame. } iIntros "Hunfl1". wp_seq. iFrame. Qed. Lemma awp_atomic_env (e : expr) (ev : val) R Φ : IntoVal e ev → (∀ env, env_inv env -∗ R -∗ 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 (γ π env l s) "#Hlock #Hres Hunfl". do 2 wp_lam. wp_apply (acquire_cancel_spec with "[\$]"). iIntros (f) "([Henv HR] & Hcl)". wp_seq. iDestruct ("Hwp" with "Henv HR") as "Hwp". wp_apply (wp_wand with "Hwp"). iIntros (w) "[Henv [HR HΦ]]". wp_let. wp_apply (release_cancel_spec with "[\$Hlock Hcl Henv HR]"). { iApply "Hcl". by iNext; iFrame. } iIntros "Hunfl". wp_seq. iFrame. Qed. Lemma awp_par (Ψ1 Ψ2 : val → iProp Σ) e1 e2 (ev1 ev2 : val) R (Φ : val → iProp Σ) : IntoVal e1 ev1 → IntoVal e2 ev2 → awp ev1 R Ψ1 -∗ awp ev2 R Ψ2 -∗ ▷ (∀ w1 w2, Ψ1 w1 -∗ Ψ2 w2 -∗ ▷ Φ (w1,w2)%V) -∗ 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. iIntros (γ π env l s) "#Hlock #Hres [Hunfl1 Hunfl2]". do 2 wp_lam. iApply (par_spec (λ v, Ψ1 v ∗ unflocked _ (π/2))%I (λ v, Ψ2 v ∗ unflocked _ (π/2))%I with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]"). - wp_lam. wp_apply (wp_wand with "Hwp1"). iIntros (v) "Hwp1". by iApply "Hwp1". - wp_lam. wp_apply (wp_wand with "Hwp2"). iIntros (v) "Hwp2". by iApply "Hwp2". - iNext. iIntros (w1 w2) "[[HΨ1 \$] [HΨ2 \$]]". iApply ("HΦ" with "[\$] [\$]"). Qed. End a_wp_rules. Section a_wp_run. Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}. Lemma awp_run (e : expr) R Φ : AsVal e → 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); first done. iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd. iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env ∗ R)%I with "Hlock Hunfl [Henv Hσ \$HR]") as (s) "[#Hres Hunfl]". { iNext. iExists ∅, ∅. iFrame. eauto. } 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]". iMod (cancel_lock with "Hlock Hres Hunfl") as "[HEnv HR]". by iApply "HΦ". Qed. End a_wp_run. (* Make sure that we only use the provided rules and don't break the abstraction *) Opaque a_ret a_bind (* a_run *) a_atomic a_atomic_env a_par. (* Definition locking_heapΣ : gFunctors := *) (* #[heapΣ; GFunctor (auth.authR locking_heapUR)]. *) (* Instance subG_locking_heapG {Σ} : subG locking_heapΣ Σ → locking_heapPreG Σ. *) (* Proof. solve_inG. Qed. *) (* Definition awp_adequacy Σ R s v σ φ : *) (* (R -∗ (∀ `{locking_heapG Σ}, awp (of_val v) R (λ w, R -∗ ⌜φ w⌝)))%I → *) (* adequate MaybeStuck (a_run v) σ φ. *) (* (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) → *) (* Proof. *) (* intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "". *) (* iMod (gen_heap_init σ) as (?) "Hh". *) (* iModIntro. iExists gen_heap_ctx. iFrame "Hh". *) (* iApply (Hwp (HeapG _ _ _)). *) (* Qed. *)