Commit 19d36a41 by Dan Frumin

### Reorganize lemmas in translation.v

parent 6d35edfe
 ... @@ -46,7 +46,6 @@ Notation "e1 ;;;; e2" := ... @@ -46,7 +46,6 @@ Notation "e1 ;;;; e2" := Definition a_if : val := λ: "cnd" "e1" "e2", Definition a_if : val := λ: "cnd" "e1" "e2", a_bind (λ: "c", if: "c" then "e1" #() else "e2" #()) "cnd". a_bind (λ: "c", if: "c" then "e1" #() else "e2" #()) "cnd". Definition a_while: val := Definition a_while: val := rec: "while" "cnd" "bdy" := rec: "while" "cnd" "bdy" := a_if ("cnd" #()) (λ:<>, "bdy" #() ;;;; "while" "cnd" "bdy") a_seq%E. a_if ("cnd" #()) (λ:<>, "bdy" #() ;;;; "while" "cnd" "bdy") a_seq%E. ... @@ -54,110 +53,84 @@ Definition a_while: val := ... @@ -54,110 +53,84 @@ Definition a_while: val := Section proofs. Section proofs. Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}. Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}. Lemma a_alloc_spec R Φ e : Lemma a_while_spec R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : awp e R (λ v, ∀ l, l ↦U v -∗ Φ #l) -∗ ▷ awp (a_if c awp (a_alloc e) R Φ. (λ:<>, (#() ;; 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. Proof. iIntros "HΦ". iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. iApply a_if_spec. iApply awp_bind. iApply awp_ret. iApply wp_value. iApply (awp_wand with "H"). clear v. iRight. iSplit; eauto. by awp_seq. iIntros (v) "H". 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. iApply wp_fupd. wp_let. wp_alloc l as "Hl". iAssert (⌜σ !! l = None⌝)%I with "[Hl Hls]" as %Hl. { remember (σ !! l) as σl. destruct σl; simplify_eq; eauto. iExFalso. rewrite (bi.big_sepM_lookup _ σ l _); last eauto. iDestruct "Hls" as (v') "Hl'". by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. } iDestruct "Hl" as "[Hl Hl']". iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto. iModIntro. iFrame "HR". iSplitR "H Hl'". - iExists X,(<[l:=ULvl]>σ). iFrame. iSplit. + rewrite bi.big_sepM_insert; eauto. iFrame. eauto. + iPureIntro. by rewrite locked_locs_alloc_unlocked. - iApply ("H" with "Hl'"). Qed. Qed. Lemma a_seq_spec R Φ : Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 : U (Φ #()) -∗ awp e1 R (λ v, ∃ l : loc, ⌜v = #l⌝ ∧ Ψ1 l)-∗ awp (a_seq #()) R Φ. awp e2 R Ψ2 -∗ (∀ (l : loc) w, Ψ1 l -∗ Ψ2 w -∗ (∃ v, l ↦U v ∗ (l ↦L w -∗ Φ w))) -∗ awp (a_store e1 e2) R Φ. Proof. Proof. iIntros "HΦ". rewrite /a_seq. awp_lam. 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 !>". iDestruct "H1" as (l ->) "H1". awp_lam. iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]". iApply awp_atomic_env. iApply awp_atomic_env. iIntros (env) "Henv HR". iIntros (env) "Henv HR". iApply wp_fupd. rewrite {2}/env_inv. rewrite {2}/env_inv. iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Hlocks" as %Hlocks. iDestruct "Hlocks" as %Hlocks. wp_let. iApply (mset_clear_spec with "HX"). iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl. iNext. iIntros "HX". assert (#l ∉ X). iDestruct "HΦ" as (us) "[Hus HΦ]". { unfold correct_locks in *. intros Hx. apply Hl. clear Hlocks. destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. } iInduction us as [|u us] "IH" forall (σ); simpl. wp_let. wp_proj. - iModIntro. iFrame "HR". iSplitR "HΦ". wp_apply (mset_add_spec with "[\$HX]"); eauto. + iExists ∅, σ. iFrame. iPureIntro. iIntros "HX". wp_seq. rewrite /correct_locks /set_Forall. set_solver. iAssert (⌜σ !! l = Some ULvl⌝%I) with "[Hσ Hv]" as %?. + by iApply "HΦ". - iDestruct "Hus" as "[Hu Hus]". iAssert (⌜σ !! u.1 = Some LLvl⌝%I) with "[Hσ Hu]" as %?. { rewrite mapsto_eq /mapsto_def. { rewrite mapsto_eq /mapsto_def. iDestruct "Hu" as "[Hu Hl]". iDestruct "Hv" as "[Hv Hl]". by iDestruct (own_valid_2 with "Hσ Hl") by iDestruct (own_valid_2 with "Hσ Hl") as %[?%heap_singleton_included _]%auth_valid_discrete_2. } as %[?%heap_singleton_included _]%auth_valid_discrete_2. } iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]". iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hv") as "[Hσ Hv]". iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX"). do 2 wp_proj. rewrite mapsto_eq /mapsto_def. { iIntros "Hus". iApply "HΦ". by iFrame. } iDestruct "Hv" as "[Hv Hl]". { rewrite -bi.big_sepM_insert_override; eauto. } rewrite (bi.big_sepM_lookup_acc _ _ l ULvl); last done. Qed. iDestruct "Hls" as "[Hl' Hls]". iDestruct "Hl'" as (?) "Hl'". Lemma a_sequence_spec R Φ (f e : expr) : rewrite Qp_mult_1_l. AsVal f → iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->. awp e R (λ v, U (awp (f v) R Φ)) -∗ iCombine "Hv Hl'" as "Hv". awp (a_seq_bind f e) R Φ. wp_store. Proof. iDestruct "Hv" as "[Hv Hl']". iIntros ([fv <-%of_to_val]) "H". rewrite /a_seq_bind /=. awp_lam. iSpecialize ("Hls" with "[Hl']"); eauto. awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. wp_proj. iFrame "HR". iSplitR "HΦ Hl Hv". iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H". - iExists ({[#l]} ∪ X),(<[l:=LLvl]> σ). iFrame. iSplitL. awp_lam. iApply awp_bind. iApply a_seq_spec. + rewrite -bi.big_sepM_insert_override; eauto. iModIntro. by awp_lam. + (* TODO: a separate lemma somewhere *) Qed. iPureIntro. rewrite locked_locs_lock. revert Hlocks. rewrite /correct_locks /set_Forall. set_solver. Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : - iApply "HΦ". iFrame. 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. Qed. Lemma a_load_spec R Φ q e : Lemma a_load_spec R Φ q e : ... @@ -190,35 +163,6 @@ Section proofs. ... @@ -190,35 +163,6 @@ Section proofs. - by iApply "HΦ". - by iApply "HΦ". Qed. Qed. Lemma a_alloc_spec R Φ e : awp e R (λ v, ∀ l, l ↦U v -∗ Φ #l) -∗ awp (a_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σ & Hls & Hlocks)". iDestruct "Hlocks" as %Hlocks. iApply wp_fupd. wp_let. wp_alloc l as "Hl". iAssert (⌜σ !! l = None⌝)%I with "[Hl Hls]" as %Hl. { remember (σ !! l) as σl. destruct σl; simplify_eq; eauto. iExFalso. rewrite (bi.big_sepM_lookup _ σ l _); last eauto. iDestruct "Hls" as (v') "Hl'". by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. } iDestruct "Hl" as "[Hl Hl']". iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto. iModIntro. iFrame "HR". iSplitR "H Hl'". - iExists X,(<[l:=ULvl]>σ). iFrame. iSplit. + rewrite bi.big_sepM_insert; eauto. iFrame. eauto. + iPureIntro. by rewrite locked_locs_alloc_unlocked. - iApply ("H" with "Hl'"). Qed. Lemma a_un_op_spec R Φ e op: Lemma a_un_op_spec R Φ e op: awp e R (λ v, ∃ w, ⌜un_op_eval op v = Some w⌝ ∧ Φ w) -∗ awp e R (λ v, ∃ w, ⌜un_op_eval op v = Some w⌝ ∧ Φ w) -∗ awp (a_un_op op e) R Φ. awp (a_un_op op e) R Φ. ... @@ -248,56 +192,108 @@ Section proofs. ... @@ -248,56 +192,108 @@ Section proofs. iDestruct "HΦ" as (w0) "[% H]". by wp_pure _. iDestruct "HΦ" as (w0) "[% H]". by wp_pure _. Qed. Qed. Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 : Lemma a_seq_spec R Φ : awp e1 R (λ v, ∃ l : loc, ⌜v = #l⌝ ∧ Ψ1 l)-∗ U (Φ #()) -∗ awp e2 R Ψ2 -∗ awp (a_seq #()) R Φ. (∀ (l : loc) w, Ψ1 l -∗ Ψ2 w -∗ (∃ v, l ↦U v ∗ (l ↦L w -∗ Φ w))) -∗ awp (a_store e1 e2) R Φ. Proof. Proof. iIntros "H1 H2 HΦ". iIntros "HΦ". rewrite /a_seq. awp_lam. 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 !>". iDestruct "H1" as (l ->) "H1". awp_lam. iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]". iApply awp_atomic_env. iApply awp_atomic_env. iIntros (env) "Henv HR". iIntros (env) "Henv HR". iApply wp_fupd. rewrite {2}/env_inv. rewrite {2}/env_inv. iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Hlocks" as %Hlocks. iDestruct "Hlocks" as %Hlocks. iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl. wp_let. iApply (mset_clear_spec with "HX"). assert (#l ∉ X). iNext. iIntros "HX". { unfold correct_locks in *. intros Hx. apply Hl. iDestruct "HΦ" as (us) "[Hus HΦ]". destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. } clear Hlocks. wp_let. wp_proj. iInduction us as [|u us] "IH" forall (σ); simpl. wp_apply (mset_add_spec with "[\$HX]"); eauto. - iModIntro. iFrame "HR". iSplitR "HΦ". iIntros "HX". wp_seq. + iExists ∅, σ. iFrame. iPureIntro. iAssert (⌜σ !! l = Some ULvl⌝%I) with "[Hσ Hv]" as %?. 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. { rewrite mapsto_eq /mapsto_def. iDestruct "Hv" as "[Hv Hl]". iDestruct "Hu" as "[Hu Hl]". by iDestruct (own_valid_2 with "Hσ Hl") by iDestruct (own_valid_2 with "Hσ Hl") as %[?%heap_singleton_included _]%auth_valid_discrete_2. } as %[?%heap_singleton_included _]%auth_valid_discrete_2. } iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hv") as "[Hσ Hv]". iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]". do 2 wp_proj. rewrite mapsto_eq /mapsto_def. iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX"). iDestruct "Hv" as "[Hv Hl]". { iIntros "Hus". iApply "HΦ". by iFrame. } rewrite (bi.big_sepM_lookup_acc _ _ l ULvl); last done. { rewrite -bi.big_sepM_insert_override; eauto. } iDestruct "Hls" as "[Hl' Hls]". Qed. iDestruct "Hl'" as (?) "Hl'". rewrite Qp_mult_1_l. Lemma a_sequence_spec R Φ (f e : expr) : iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->. AsVal f → iCombine "Hv Hl'" as "Hv". awp e R (λ v, U (awp (f v) R Φ)) -∗ wp_store. awp (a_seq_bind f e) R Φ. iDestruct "Hv" as "[Hv Hl']". Proof. iSpecialize ("Hls" with "[Hl']"); eauto. iIntros ([fv <-%of_to_val]) "H". rewrite /a_seq_bind /=. awp_lam. wp_proj. iFrame "HR". iSplitR "HΦ Hl Hv". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. - iExists ({[#l]} ∪ X),(<[l:=LLvl]> σ). iFrame. iSplitL. iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H". + rewrite -bi.big_sepM_insert_override; eauto. awp_lam. iApply awp_bind. iApply a_seq_spec. + (* TODO: a separate lemma somewhere *) iModIntro. by awp_lam. iPureIntro. rewrite locked_locs_lock. Qed. revert Hlocks. rewrite /correct_locks /set_Forall. set_solver. - iApply "HΦ". iFrame. 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. 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. End proofs.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!