Commit efbc0fdb by Ralf Jung

### make wp_apply not call wp_pures

parent 1346311d
 ... ... @@ -111,7 +111,7 @@ Section tests. Lemma Pred_spec n E Φ : Φ #(n - 1) -∗ WP Pred #n @ E [{ Φ }]. Proof. iIntros "HΦ". wp_lam. wp_op. case_bool_decide. wp_op. case_bool_decide; wp_pures. - wp_apply FindPred_spec; first lia. wp_pures. by replace (n - 1)%Z with (- (-n + 2 - 1))%Z by lia. - wp_apply FindPred_spec; eauto with lia. ... ... @@ -119,7 +119,7 @@ Section tests. Lemma Pred_user E : ⊢ WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }]. Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed. Proof. iIntros "". wp_apply Pred_spec. wp_pures. by wp_apply Pred_spec. Qed. Definition Id : val := rec: "go" "x" := ... ...
 ... ... @@ -47,7 +47,7 @@ Section tests. Resolve (Resolve (#n - #n) ((λ: "x", "x") #p2) (#0 + #2)) ((λ: "x", "x") #p1) (#0 + #1) @ s; E {{{ RET #0 ; ∃ vs1' vs2', ⌜vs1 = (#0, #1)::vs1' ∧ vs2 = (#0, #2)::vs2'⌝ ∗ proph p1 vs1' ∗ proph p2 vs2' }}}. Proof. iIntros (Φ) "[Hp1 Hp2] HΦ". iIntros (Φ) "[Hp1 Hp2] HΦ". wp_pures. wp_apply (wp_resolve with "Hp1"); first done. wp_apply (wp_resolve with "Hp2"); first done. wp_op. ... ...
 ... ... @@ -84,7 +84,7 @@ Proof. iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; subst. iModIntro. iSplitL "Hl". { iNext; iRight; by eauto. } wp_apply wp_assert. wp_pures. by case_bool_decide. wp_pures. wp_apply wp_assert. wp_pures. by case_bool_decide. Qed. Lemma ht_one_shot (Φ : val → iProp Σ) : ... ... @@ -95,8 +95,8 @@ Lemma ht_one_shot (Φ : val → iProp Σ) : }}. Proof. iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit. - iIntros (n) "!> _". wp_apply "Hf1". - iIntros "!> _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _". - iIntros (n) "!> _". wp_pures. wp_apply "Hf1". - iIntros "!> _". wp_pures. wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _". Qed. End proof. ... ... @@ -111,8 +111,8 @@ Section client. Lemma client_safe : ⊢ WP client {{ _, True }}. Proof using Type*. rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]". wp_let. wp_apply wp_par. - wp_apply "Hf1". wp_let. wp_pures. wp_apply wp_par. - wp_pures. wp_apply "Hf1". - wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2". iIntros (check) "Hcheck". wp_pures. iApply "Hcheck". - auto. ... ...
 ... ... @@ -113,8 +113,8 @@ Lemma ht_one_shot (Φ : val → iProp Σ) : Proof. iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)". iExists T. iFrame "HT". iSplit. - iIntros (n) "!> HT". wp_apply "Hf1". done. - iIntros "!> _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _". - iIntros (n) "!> HT". wp_pures. wp_apply "Hf1". done. - iIntros "!> _". wp_pures. wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _". Qed. End proof. ... ... @@ -129,8 +129,8 @@ Section client. Lemma client_safe : ⊢ WP client {{ _, True }}. Proof using Type*. rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)". wp_let. wp_apply (wp_par with "[HT]"). - wp_apply "Hf1". done. wp_let. wp_pures. wp_apply (wp_par with "[HT]"). - wp_pures. wp_apply "Hf1". done. - wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2". iIntros (check) "Hcheck". wp_pures. iApply "Hcheck". - auto. ... ...
 ... ... @@ -56,7 +56,7 @@ Lemma sum_wp `{!heapG Σ} v t : [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]]. Proof. iIntros (Φ) "Ht HΦ". rewrite /sum' /=. wp_lam. wp_alloc l as "Hl". wp_lam. wp_alloc l as "Hl". wp_pures. wp_apply (sum_loop_wp with "[\$Hl \$Ht]"). rewrite Z.add_0_r. iIntros "[Hl Ht]". wp_load. by iApply "HΦ". ... ...
 ... ... @@ -82,7 +82,7 @@ Section proof. { iApply "HΦ". iFrame. } iDestruct (array_cons with "Hdst") as "[Hv1 Hdst]". iDestruct (array_cons with "Hsrc") as "[Hv2 Hsrc]". wp_load; wp_store. wp_load; wp_store. wp_pures. wp_apply ("IH" with "[%] [%] Hdst Hsrc"); [ lia .. | ]. iIntros "[Hvdst Hvsrc]". iApply "HΦ"; by iFrame. ... ... @@ -106,7 +106,7 @@ Section proof. Proof. iIntros (Hvl Hn Φ) "Hvl HΦ". wp_lam. wp_alloc dst as "Hdst"; first by auto. wp_alloc dst as "Hdst"; first by auto. wp_pures. wp_apply (twp_array_copy_to with "[\$Hdst \$Hvl]"). - rewrite replicate_length Z2Nat.id; lia. - auto. ... ... @@ -146,7 +146,7 @@ Section proof. wp_pures. iApply ("HΦ" \$! []). auto. } rewrite bool_decide_eq_false_2; last naive_solver lia. iDestruct (array_cons with "Hl") as "[Hl HSl]". iDestruct "Hf" as "[Hf HSf]". iDestruct "Hf" as "[Hf HSf]". wp_pures. wp_apply (wp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures. rewrite Z.add_1_r -Nat2Z.inj_succ. iApply ("IH" with "[%] [HSl] HSf"); first lia. ... ... @@ -173,7 +173,7 @@ Section proof. wp_pures. iApply ("HΦ" \$! []). auto. } rewrite bool_decide_eq_false_2; last naive_solver lia. iDestruct (array_cons with "Hl") as "[Hl HSl]". iDestruct "Hf" as "[Hf HSf]". iDestruct "Hf" as "[Hf HSf]". wp_pures. wp_apply (twp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures. rewrite Z.add_1_r -Nat2Z.inj_succ. iApply ("IH" with "[%] [HSl] HSf"); first lia. ... ... @@ -194,7 +194,7 @@ Section proof. ⌜Z.of_nat (length vs) = n⌝ ∗ l ↦∗ vs ∗ [∗ list] k↦v ∈ vs, Q k v }}}. Proof. iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done. iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done. wp_pures. wp_apply (wp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl \$Hf] [HΦ]"). { by rewrite /= Z2Nat.id; last lia. } { by rewrite loc_add_0. } ... ... @@ -213,7 +213,7 @@ Section proof. ⌜Z.of_nat (length vs) = n⌝ ∗ l ↦∗ vs ∗ [∗ list] k↦v ∈ vs, Q k v }]]. Proof. iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done. iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done. wp_pures. wp_apply (twp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl \$Hf] [HΦ]"). { by rewrite /= Z2Nat.id; last lia. } { by rewrite loc_add_0. } ... ...
 ... ... @@ -14,7 +14,7 @@ Lemma twp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e : WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗ WP (assert: e)%V @ E [{ Φ }]. Proof. iIntros "HΦ". wp_lam. iIntros "HΦ". wp_lam. wp_pures. wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if. Qed. ... ... @@ -22,6 +22,6 @@ Lemma wp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e : WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP (assert: e)%V @ E {{ Φ }}. Proof. iIntros "HΦ". wp_lam. iIntros "HΦ". wp_lam. wp_pures. wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if. Qed.
 ... ... @@ -63,7 +63,7 @@ Section increment. { (* abort case *) done. } iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iModIntro. (* Now go on *) awp_apply cas_spec; first done. wp_pures. awp_apply cas_spec; first done. (* Prove the atomic update for CAS *) rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]". iModIntro. iExists _. iFrame "Hl". iSplit. ... ... @@ -87,7 +87,7 @@ Section increment. iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame. iIntros "\$ !> AU !>". (* Now go on *) awp_apply cas_spec; first done. wp_pures. awp_apply cas_spec; first done. (* Prove the atomic update for CAS *) iApply (aacc_aupd with "AU"); first done. iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame. ... ... @@ -118,7 +118,7 @@ Section increment. Proof. iIntros "Hl" (Φ) "AU". wp_lam. wp_apply (atomic_wp_seq \$! (load_spec _) with "Hl"). iIntros "Hl". awp_apply store_spec. iIntros "Hl". wp_pures. awp_apply store_spec. (* Prove the atomic update for store *) iApply (aacc_aupd_commit with "AU"); first done. iIntros (x) "H↦". ... ... @@ -155,7 +155,7 @@ Section increment_client. (* The continuation: From after the atomic triple to the postcondition of the WP *) done. } wp_apply wp_par. wp_pures. wp_apply wp_par. - iAssumption. - iAssumption. - iIntros (??) "_ !>". done. ... ...
 ... ... @@ -52,7 +52,7 @@ Proof. iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?". { iNext. iExists NONEV. iFrame; eauto. } wp_apply (wp_fork with "[Hf]"). wp_pures. wp_apply (wp_fork with "[Hf]"). - iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv". wp_inj. iInv N as (v') "[Hl _]". wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto. ... ... @@ -66,7 +66,7 @@ Proof. iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]". wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst. - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|]. wp_apply ("IH" with "Hγ [HΦ]"). auto. wp_pures. wp_apply ("IH" with "Hγ [HΦ]"). auto. - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']". + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|]. wp_pures. by iApply "HΦ". ... ...
 ... ... @@ -483,7 +483,6 @@ End heap. [iApplyHyp H] to actually apply the hypothesis. TC resolution of [lem] premises happens *after* [tac H] got executed. *) Tactic Notation "wp_apply_core" open_constr(lem) tactic3(tac) := wp_pures; iPoseProofCore lem as false (fun H => lazymatch goal with | |- envs_entails _ (wp ?s ?E ?e ?Q) => ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!