From 19d36a4158f66abe426c7b9f149633b264f0e9e8 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Sun, 20 May 2018 16:08:12 +0200 Subject: [PATCH] Reorganize lemmas in translation.v --- theories/c_translation/translation.v | 328 +++++++++++++-------------- 1 file changed, 162 insertions(+), 166 deletions(-) diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v index 0156f38..2ade3aa 100644 --- a/theories/c_translation/translation.v +++ b/theories/c_translation/translation.v @@ -46,7 +46,6 @@ Notation "e1 ;;;; e2" := Definition a_if : val := λ: "cnd" "e1" "e2", a_bind (λ: "c", if: "c" then "e1" #() else "e2" #()) "cnd". - Definition a_while: val := rec: "while" "cnd" "bdy" := a_if ("cnd" #()) (λ:<>, "bdy" #() ;;;; "while" "cnd" "bdy") a_seq%E. @@ -54,142 +53,6 @@ Definition a_while: val := Section proofs. Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}. - - Lemma a_while_spec R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : - ▷ awp (a_if c - (λ:<>, (#() ;; b) ;;;; a_while (λ:<>, c) (λ:<>, b)) - a_seq)%E R Φ -∗ - awp (a_while (λ:<>, c) (λ:<>, b))%E 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 <-%of_to_val] [v2 <-%of_to_val]) "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_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ : - awp e1 R Φ -∗ awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E 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 (a_if (a_ret #false) (λ: <>, e1) (λ: <>, e2))%E R Φ. - Proof. - iIntros "HΦ". - iApply a_if_spec. - iApply awp_ret. iApply wp_value. - iRight. iSplit; eauto. by awp_seq. - 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 HR". - iApply wp_fupd. - rewrite {2}/env_inv. - iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". - iDestruct "Hlocks" as %Hlocks. - wp_let. iApply (mset_clear_spec with "HX"). - iNext. iIntros "HX". - iDestruct "HΦ" as (us) "[Hus HΦ]". - clear Hlocks. - iInduction us as [|u us] "IH" forall (σ); simpl. - - iModIntro. iFrame "HR". iSplitR "HΦ". - + iExists ∅, σ. iFrame. iPureIntro. - rewrite /correct_locks /set_Forall. set_solver. - + by iApply "HΦ". - - iDestruct "Hus" as "[Hu Hus]". - iAssert (⌜σ !! u.1 = Some LLvl⌝%I) with "[Hσ Hu]" as %?. - { rewrite mapsto_eq /mapsto_def. - iDestruct "Hu" as "[Hu Hl]". - by iDestruct (own_valid_2 with "Hσ Hl") - as %[?%heap_singleton_included _]%auth_valid_discrete_2. } - iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]". - iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX"). - { iIntros "Hus". iApply "HΦ". by iFrame. } - { rewrite -bi.big_sepM_insert_override; eauto. } - 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 <-%of_to_val]) "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_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))))%I) -∗ - awp (a_while (λ:<>, c) (λ:<>, b))%E 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. awp_seq. - iApply (awp_wand with "H"). - iIntros (v) "Hi". iModIntro. awp_seq. - by iApply ("IH" with "Hi"). - Qed. - - Lemma a_load_spec R Φ q e : - awp e R (λ v, ∃ (l : loc) (w : val), ⌜v = #l⌝ ∗ l ↦U{q} w ∗ (l ↦U{q} w -∗ Φ w)) -∗ - awp (a_load 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 (l w) "(% & Hl & HΦ)". subst. - awp_lam. - iApply awp_atomic_env. - iIntros (env) "Henv HR". - 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_let. - wp_apply wp_assert. - wp_apply (mset_member_spec #l env with "HX"). - iIntros "Henv /=". case_decide; first by exfalso. simpl. - wp_op. iSplit; eauto. iNext. wp_seq. - rewrite mapsto_eq /mapsto_def. iDestruct "Hl" as "[Hv Hl]". wp_load. - iCombine "Hv Hl" as "Hv". iFrame "HR". - iSplitR "HΦ Hv". - - iExists X,σ. by iFrame. - - by iApply "HΦ". - Qed. - Lemma a_alloc_spec R Φ e : awp e R (λ v, ∀ l, l ↦U v -∗ Φ #l) -∗ awp (a_alloc e) R Φ. @@ -219,35 +82,6 @@ Section proofs. - iApply ("H" with "Hl'"). Qed. - Lemma a_un_op_spec R Φ e op: - awp e R (λ v, ∃ w, ⌜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_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_store_spec R Φ Ψ1 Ψ2 e1 e2 : awp e1 R (λ v, ∃ l : loc, ⌜v = #l⌝ ∧ Ψ1 l)-∗ awp e2 R Ψ2 -∗ @@ -299,5 +133,167 @@ Section proofs. - iApply "HΦ". iFrame. Qed. + Lemma a_load_spec R Φ q e : + awp e R (λ v, ∃ (l : loc) (w : val), ⌜v = #l⌝ ∗ l ↦U{q} w ∗ (l ↦U{q} w -∗ Φ w)) -∗ + awp (a_load 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 (l w) "(% & Hl & HΦ)". subst. + awp_lam. + iApply awp_atomic_env. + iIntros (env) "Henv HR". + 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_let. + wp_apply wp_assert. + wp_apply (mset_member_spec #l env with "HX"). + iIntros "Henv /=". case_decide; first by exfalso. simpl. + wp_op. iSplit; eauto. iNext. wp_seq. + rewrite mapsto_eq /mapsto_def. iDestruct "Hl" as "[Hv Hl]". wp_load. + iCombine "Hv Hl" as "Hv". iFrame "HR". + iSplitR "HΦ Hv". + - iExists X,σ. by iFrame. + - by iApply "HΦ". + Qed. + + Lemma a_un_op_spec R Φ e op: + awp e R (λ v, ∃ w, ⌜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_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_seq_spec R Φ : + U (Φ #()) -∗ + awp (a_seq #()) R Φ. + Proof. + iIntros "HΦ". rewrite /a_seq. awp_lam. + iApply awp_atomic_env. + iIntros (env) "Henv HR". + iApply wp_fupd. + rewrite {2}/env_inv. + iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". + iDestruct "Hlocks" as %Hlocks. + wp_let. iApply (mset_clear_spec with "HX"). + iNext. iIntros "HX". + iDestruct "HΦ" as (us) "[Hus HΦ]". + clear Hlocks. + iInduction us as [|u us] "IH" forall (σ); simpl. + - iModIntro. iFrame "HR". iSplitR "HΦ". + + iExists ∅, σ. iFrame. iPureIntro. + rewrite /correct_locks /set_Forall. set_solver. + + by iApply "HΦ". + - iDestruct "Hus" as "[Hu Hus]". + iAssert (⌜σ !! u.1 = Some LLvl⌝%I) with "[Hσ Hu]" as %?. + { rewrite mapsto_eq /mapsto_def. + iDestruct "Hu" as "[Hu Hl]". + by iDestruct (own_valid_2 with "Hσ Hl") + as %[?%heap_singleton_included _]%auth_valid_discrete_2. } + iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]". + iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX"). + { iIntros "Hus". iApply "HΦ". by iFrame. } + { rewrite -bi.big_sepM_insert_override; eauto. } + 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 <-%of_to_val]) "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_while_spec R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : + ▷ awp (a_if c + (λ:<>, (#() ;; b) ;;;; a_while (λ:<>, c) (λ:<>, b)) + a_seq)%E R Φ -∗ + awp (a_while (λ:<>, c) (λ:<>, b))%E 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 <-%of_to_val] [v2 <-%of_to_val]) "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_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ : + awp e1 R Φ -∗ awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E 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 (a_if (a_ret #false) (λ: <>, e1) (λ: <>, e2))%E 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))))%I) -∗ + awp (a_while (λ:<>, c) (λ:<>, b))%E 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. awp_seq. + iApply (awp_wand with "H"). + iIntros (v) "Hi". iModIntro. awp_seq. + by iApply ("IH" with "Hi"). + Qed. End proofs. -- GitLab