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 list. From iris_c.c_translation Require Import proofmode. Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l"). Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope. Definition a_alloc : val := λ: "n" "x", "v" ←ᶜ "x" ;;ᶜ a_atomic_env (λ: <>, lreplicate "n" "v"). Notation "'allocᶜ' e1" := (a_alloc e1%E) (at level 80) : expr_scope. Definition a_store : val := λ: "x1" "x2", "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ a_atomic_env (λ: "env", let: "l" := Fst (Fst "vv") in let: "i" := Snd (Fst "vv") in let: "v" := Snd "vv" in mset_add ("l", "i") "env" ;; let: "ll" := !"l" in "l" <- linsert "i" "v" "ll" ;; "v" ). Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope. Definition a_load : val := λ: "x", "v" ←ᶜ "x";;ᶜ a_atomic_env (λ: "env", let: "l" := Fst "v" in let: "i" := Snd "v" in assert: (mset_member ("l", "i") "env" = #false);; let: "ll" := !"l" in llookup "i" "ll" ). Notation "∗ᶜ e" := (a_load e)%E (at level 9, right associativity) : expr_scope. Definition a_un_op (op : un_op) : val := λ: "x", "v" ←ᶜ "x" ;;ᶜ a_ret (UnOp op "v"). (*Definition a_pre_un_op (op : un_op) : val := λ: "x", "l" ←ᶜ "x" ;;ᶜ a_atomic (λ: <>, a_store (a_ret "l") (a_un_op op (∗ᶜ (a_ret "l")))).*) Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2", "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ a_ret (BinOp op (Fst "vv") (Snd "vv")). Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope. Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope. Notation "e1 *ᶜ e2" := (a_bin_op MultOp e1%E e2%E) (at level 80) : expr_scope. Notation "e1 ≤ᶜ e2" := (a_bin_op LeOp e1%E e2%E) (at level 80) : expr_scope. Notation "e1 <ᶜ e2" := (a_bin_op LtOp e1%E e2%E) (at level 80) : expr_scope. Notation "e1 ==ᶜ e2" := (a_bin_op EqOp e1%E e2%E) (at level 80) : expr_scope. Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op EqOp e1%E e2%E)) (at level 80): expr_scope. Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope. Definition a_pre_bin_op (op : bin_op) : val := λ: "x" "y", "lv" ←ᶜ ("x" |||ᶜ "y");;ᶜ a_atomic (λ: <>, "ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;ᶜ a_ret (Fst "lv") =ᶜ a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;ᶜ a_ret "ov"). Notation "e1 +=ᶜ e2" := (a_pre_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope. (* M () *) (* The eta expansion is used to turn it into a value *) Definition a_seq : val := λ: <>, a_atomic_env (λ: "env", mset_clear "env"). Definition a_seq_bind : val := λ: "f" "x", "a" ←ᶜ "x" ;;ᶜ a_seq #() ;;ᶜ "f" "a". Notation "e1 ;ᶜ e2" := (a_seq_bind (λ: <>, e2) e1)%E (at level 100, e2 at level 200, format "'[' '[hv' '[' e1 ']' ;ᶜ ']' '/' e2 ']'") : expr_scope. Definition a_if : val := λ: "cnd" "e1" "e2", "c" ←ᶜ "cnd" ;;ᶜ if: "c" then "e1" #() else "e2" #(). Notation "'ifᶜ' ( e1 ) { e2 } 'elseᶜ' { e3 }" := (a_if e1%E (λ:<>, e2)%E (λ:<>, e3)%E) (at level 200, e1, e2, e3 at level 200, format "'ifᶜ' ( e1 ) { e2 } 'elseᶜ' { e3 }") : expr_scope. Definition a_while: val := rec: "while" "cnd" "bdy" := a_if ("cnd" #()) (λ: <>, "bdy" #() ;ᶜ "while" "cnd" "bdy") a_seq%E. Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ:<>, e1)%E (λ:<>, e2)%E) (at level 200, e1, e2 at level 200, format "'whileᶜ' ( e1 ) { e2 }") : expr_scope. Definition a_invoke: val := λ: "f" "arg", a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg". Section proofs. Context `{amonadG Σ}. (* Lemma a_alloc_spec R Φ e : AWP e @ R {{ v, ∀ l : loc, l ↦C v -∗ Φ #l }} -∗ AWP allocᶜ e @ R {{ Φ }}. Proof. iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. iApply awp_bind. iApply (awp_wand with "H"). clear v. iIntros (v) "H". awp_lam. iApply awp_atomic_env. iIntros (env) "Henv HR". rewrite {2}/env_inv. iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)". iDestruct "Hlocks" as %Hlocks. iApply wp_fupd. wp_let. wp_alloc l as "Hl". iAssert ⌜σ !! l = None⌝%I with "[Hl Hσ]" as %Hl. { remember (σ !! l) as σl. destruct σl as [[? ?]|]; simplify_eq; eauto. iDestruct "Hσ" as "[_ Hls]". iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto. by iDestruct (mapsto_valid_2 l with "Hl Hls") as %[]. } iMod (locking_heap_alloc σ l ULvl v with "Hl Hσ") as "[Hσ Hl']"; eauto. iModIntro. iFrame "HR". iSplitR "H Hl'". - iExists X,(<[l:=(ULvl,v)]>σ). iFrame. iPureIntro. by rewrite locked_locs_alloc_unlocked. - iApply ("H" with "Hl'"). Qed. *) Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 : AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ w, v1 ↦C w ∗ (v1 ↦C[LLvl] v2 -∗ Φ v2)) -∗ AWP e1 =ᶜ e2 @ R {{ Φ }}. Proof. iIntros "H1 H2 HΦ". awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam. awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam. iApply awp_bind. iApply (awp_par with "H1 H2"). iIntros "!>" (w1 w2) "H1 H2 !>". awp_lam. iDestruct ("HΦ" with "H1 H2") as (w) "[Hl HΦ]". iApply awp_atomic_env. iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR". iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hw1. iMod (locking_heap_store with "Hσ Hl") as (l i ll vs -> Hl Hi) "[Hl Hclose]". wp_let. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let. wp_apply (mset_add_spec with "[$]"); [set_solver|]; iIntros "Hlocks /="; wp_seq. wp_load; wp_let. wp_apply (linsert_spec with "[//]"); [eauto|]; iIntros (ll' Hl'). iApply wp_fupd. wp_store. iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]". iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ". iExists ({[(#l, #i)%V]} ∪ X), _. iFrame "Hσ". rewrite locked_locs_lock. iIntros "{$Hlocks} !%". set_solver. Qed. Lemma a_load_spec_exists_frac R Φ e : AWP e @ R {{ v, ∃ q w, v ↦C{q} w ∗ (v ↦C{q} w -∗ Φ w) }} -∗ AWP ∗ᶜe @ R {{ Φ }}. Proof. iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. iApply awp_bind. iApply (awp_wand with "H"). clear v. iIntros (v). iDestruct 1 as (q w) "[Hl HΦ]". awp_lam. iApply awp_atomic_env. iIntros (env) "Henv HR". iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]". iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hv. iMod (locking_heap_load with "Hσ Hl") as (l i ll vs -> Hl Hi) "[Hl Hclose]". wp_let. wp_proj; wp_let. wp_proj; wp_let. wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=". rewrite bool_decide_false; last set_solver. wp_op. iSplit; first done. iNext; wp_seq. wp_load; wp_let. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_". iDestruct ("Hclose" with "Hl") as "[Hσ Hl]". iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ". iExists X, _. by iFrame. Qed. Lemma a_load_spec R Φ q e : AWP e @ R {{ v, ∃ w, v ↦C{q} w ∗ (v ↦C{q} w -∗ Φ w) }} -∗ AWP ∗ᶜe @ R {{ Φ }}. Proof. iIntros "H". iApply a_load_spec_exists_frac. awp_apply (awp_wand with "H"). iIntros (v). iDestruct 1 as (w) "[H1 H2]"; eauto with iFrame. Qed. Lemma a_un_op_spec R Φ e op: AWP e @ R {{ v, ∃ w : val, ⌜un_op_eval op v = Some w⌝ ∧ Φ w }} -∗ AWP a_un_op op e @ R {{ Φ }}. Proof. iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "HΦ"; awp_lam. iApply awp_bind. iApply (awp_wand with "HΦ"); iIntros (w) "HΦ"; awp_lam. iDestruct "HΦ" as (w0) "[% H]". iApply awp_ret. by wp_op. Qed. (* Lemma a_pre_un_op_spec R Φ e op : AWP e @ R {{ vl, R -∗ ∃ l v w, l ↦C v ∗ ⌜vl = #l⌝ ∗ ⌜un_op_eval op v = Some w⌝ ∗ (l ↦C[LLvl] w -∗ R ∗ Φ w) }} -∗ AWP a_pre_un_op op e @ R {{ Φ }}. Proof. iIntros "He". rewrite /a_pre_un_op. awp_apply (a_wp_awp with "He"); iIntros (?) "HΦ"; awp_lam. iApply awp_bind. iApply (awp_wand with "HΦ"). iIntros (vl) "H". awp_lam. iApply awp_atomic. iNext. iIntros "R". iDestruct ("H" with "R") as (l v w) "(Hl & % & % & HΦ)". simplify_eq/=. iExists True%I. rewrite left_id. awp_lam. iApply (a_store_spec _ _ (λ v', ⌜v' = #l⌝)%I (λ v', ⌜v' = w⌝ ∗ l ↦C v)%I with "[] [Hl] [-]"). - iApply awp_ret. by wp_value_head. - iApply a_un_op_spec. iApply a_load_spec. iApply awp_ret. wp_value_head. iExists _,_; iFrame. iSplit; eauto. - iNext. iIntros (? ? ->) "[% Hl]". simplify_eq/=. iExists _,_; iFrame. iSplit; eauto. iIntros "? _". by iApply "HΦ". Qed. *) Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) : AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ w, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w)-∗ AWP a_bin_op op e1 e2 @ R {{ Φ }}. Proof. iIntros "H1 H2 HΦ". awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam. awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam. iApply awp_bind. iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2"). iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst. iNext. awp_lam. iApply awp_ret. do 2 wp_proj. iSpecialize ("HΦ" with "HΨ1 HΨ2"). iDestruct "HΦ" as (w0) "[% H]". by wp_pure _. Qed. Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op : AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ R -∗ ∃ v w, v1 ↦C v ∗ ⌜ bin_op_eval op v v2 = Some w ⌝ ∗ (v1 ↦C[LLvl] w -∗ R ∗ Φ v)) -∗ AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}. Proof. iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op. awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam. awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam. iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext. iIntros (v1 v2) "Hv1 Hv2 !>". awp_let. iApply awp_atomic. iNext. iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (v w) "(Hl & % & HΦ)". simplify_eq/=. iExists True%I. rewrite left_id. awp_lam. iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head. iExists v; iFrame. iIntros "Hl". awp_let. iApply awp_bind. iApply (a_store_spec _ _ (λ v', ⌜v' = v1⌝)%I (λ v', ⌜v' = w⌝)%I with "[] [] [-]"). - awp_proj. iApply awp_ret; by wp_value_head. - iApply (a_bin_op_spec _ _ (λ v', ⌜v' = v⌝)%I (λ v', ⌜v' = v2⌝)%I); try (try awp_proj; iApply awp_ret; by wp_value_head). iNext. iIntros (? ? -> ->). eauto. - iNext. iIntros (? ? -> ->). iExists _; iFrame. iIntros "?". awp_seq. iApply awp_ret; wp_value_head. iIntros "_". by iApply "HΦ". Qed. Lemma a_seq_spec R Φ : U (Φ #()) -∗ AWP (a_seq #()) @ R {{ Φ }}. Proof. iIntros "HΦ". rewrite /a_seq. awp_lam. iApply awp_atomic_env. iIntros (env) "Henv $". iApply wp_fupd. iDestruct "Henv" as (X σ _) "[Hlocks Hσ]". wp_lam. wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks". iDestruct "HΦ" as (us) "[Hus HΦ]". iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl. - iModIntro. iSplitR "HΦ". + iExists ∅, σ. by iFrame. + by iApply "HΦ". - iDestruct "Hus" as "[Hu Hus]". iDestruct (full_locking_heap_present with "Hu Hσ") as %[z Hz]. iMod (locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]". iApply ("IH" with "Hus [HΦ Hu] Hσ Hlocks"). iIntros "Hus". iApply "HΦ". by iFrame. Qed. Lemma a_sequence_spec R Φ (f e : expr) : AsVal f → ▷ AWP e @ R {{ v, U (AWP (f v) @ R {{ Φ }}) }} -∗ AWP a_seq_bind f e @ R {{ Φ }}. Proof. iIntros ([fv <-]) "H". rewrite /a_seq_bind /=. awp_lam. awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H". awp_lam. iApply awp_bind. iApply a_seq_spec. iModIntro. by awp_lam. Qed. Lemma a_sequence_spec' R Φ (e e' : expr) : Closed [] e' → ▷ AWP e @ R {{ v, U (AWP e' @ R {{ Φ }}) }} -∗ AWP a_seq_bind (λ: <>, e') e @ R {{ Φ }}. Proof. iIntros (?) "He". iApply a_sequence_spec. iApply (awp_wand with "He"). iNext. iIntros (?) "He'". iModIntro. by awp_lam. Qed. Lemma a_while_spec R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : ▷ AWP a_if c (λ: <>, (λ: <>, b) #() ;ᶜ whileᶜ (c) { b }) a_seq @ R {{ Φ }} -∗ AWP whileᶜ (c) { b } @ R {{ Φ }}. Proof. iIntros "H". awp_lam. awp_lam. awp_seq. iApply "H". Qed. Lemma a_if_spec R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} : AsVal e1 → AsVal e2 → AWP e @ R {{ v, (⌜v = #true⌝ ∧ AWP e1 #() @ R {{ Φ }}) ∨ (⌜v = #false⌝ ∧ AWP e2 #() @ R {{ Φ }}) }} -∗ AWP a_if e e1 e2 @ R {{ Φ }}. Proof. iIntros ([v1 <-] [v2 <-]) "H". awp_apply (a_wp_awp with "H"). iIntros (v) "H". do 3 awp_lam. iApply awp_bind. iApply (awp_wand with "H"). clear v. iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if. Qed. Lemma a_if_spec' R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} : AWP e @ R {{ v, (⌜v = #true⌝ ∧ AWP e1 @ R {{ Φ }}) ∨ (⌜v = #false⌝ ∧ AWP e2 @ R {{ Φ }}) }} -∗ AWP ifᶜ (e) { e1 } elseᶜ { e2 } @ R {{ Φ }}. Proof. iIntros "He". iApply a_if_spec. iApply (awp_wand with "He"). iIntros (v) "[[% Hv] | [% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto; by awp_lam. Qed. Lemma a_while_spec' R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : ▷ AWP c @ R {{ v, ⌜v = #true⌝ ∧ AWP b @ R {{ _, U (AWP whileᶜ (c) { b } @ R {{ Φ }}) }} ∨ ⌜v = #false⌝ ∧ AWP a_seq #() @ R {{ Φ }} }} -∗ AWP whileᶜ (c) { b } @ R {{ Φ }}. Proof. iIntros "H". awp_lam. awp_lam. awp_seq. iApply a_if_spec. iApply (awp_wand with "H"). iIntros (v) "[[% Hv]|[% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto. awp_seq. iApply a_sequence_spec'. iNext. awp_seq. done. Qed. Lemma a_invoke_spec (ef ea : expr) (R : iProp Σ) Ψ Φ (f : val) : IntoVal ef f → AWP ea @ R {{ Ψ }} -∗ (∀ a, Ψ a -∗ U (R -∗ ∃ R', R' ∗ (AWP ef a @ R' {{ v, R' -∗ R ∗ Φ v }}))) -∗ AWP a_invoke ef ea @ R {{ Φ }}. Proof. rewrite /IntoVal. iIntros (<-) "Ha Hfa". rewrite /a_invoke. awp_lam. awp_apply (a_wp_awp R with "Ha"). iIntros (a) "Ha". awp_let. iApply a_sequence_spec. iApply (awp_wand with "Ha"). clear a. iNext. iIntros (a) "HΨ". iSpecialize ("Hfa" with "HΨ"). iModIntro. awp_let. iApply awp_atomic. iNext. iIntros "HR". iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]". iExists R'. iFrame. by awp_let. Qed. Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ : AWP e1 @ R {{ Φ }} -∗ AWP ifᶜ (♯true) { e1 } elseᶜ { e2 } @ R {{ Φ }}. Proof. iIntros "HΦ". iApply a_if_spec. iApply awp_ret. iApply wp_value. iLeft. iSplit; eauto. by awp_seq. Qed. Lemma a_if_false_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ : AWP e2 @ R {{ Φ }} -∗ AWP ifᶜ (♯false) { e1 } elseᶜ { e2 } @ R {{ Φ }}. Proof. iIntros "HΦ". iApply a_if_spec. iApply awp_ret. iApply wp_value. iRight. iSplit; eauto. by awp_seq. Qed. Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : I -∗ □ (I -∗ AWP c @ R {{ v, (⌜v = #false⌝ ∧ U (Φ #())) ∨ (⌜v = #true⌝ ∧ ▷ (AWP b @ R {{ _, U I }})) }}) -∗ AWP whileᶜ (c) { b } @ R {{ Φ }}. Proof. iIntros "Hi #Hinv". iLöb as "IH". iApply a_while_spec. iNext. iApply a_if_spec. iSpecialize ("Hinv" with "Hi"). iApply (awp_wand with "Hinv"). iIntros (v) "[(% & H) | (% & H)] //="; subst. - iRight. iSplit; by eauto; iApply a_seq_spec. - iLeft. iSplit; first eauto. awp_seq. iApply a_sequence_spec. iNext. awp_seq. iApply (awp_wand with "H"). iIntros (v) "Hi !>". awp_seq. by iApply ("IH" with "Hi"). Qed. End proofs. (* Make sure that we only use the provided rules and don't break the abstraction *) Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke. Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret.