Library iris.tests.heap_lang
This file is essentially a bunch of testcases.
From iris.program_logic Require Import ownership hoare auth.
From iris.heap_lang Require Import proofmode refine_proofmode notation.
Import uPred.
Section LangTests.
Definition add : expr := (#21 + #21)%E.
Goal ∀ σ, head_step add σ (#42) σ None.
Proof. intros; do_head_step done. Qed.
Definition rec_app : expr := ((rec: "f" "x" := "f" "x") #0)%E.
Goal ∀ σ, head_step rec_app σ rec_app σ None.
Proof. intros. rewrite /rec_app. do_head_step done. Qed.
Definition lam : expr := (λ: "x", "x" + #21)%E.
Goal ∀ σ, head_step (lam #21)%E σ add σ None.
Proof. intros. rewrite /lam. do_head_step done. Qed.
End LangTests.
Section LiftingTests.
Context {Σ : gFunctors}.
Context `{refineG heap_lang Σ (delayed_lang (heap_lang) O O) (S O × (O + 3))}.
Context `{heapG Σ}.
Context `{sheapG heap_lang Σ}.
Local Notation iProp := (iPropG heap_lang Σ).
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
Lemma heap_e_spec E i K :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e K O)
⊢ WP heap_e @ E {{ v, ⧆(v = #2) ★ ownT i (of_val (#2)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e.
wp_alloc l. refine_alloc O l'.
wp_let. refine_let O.
wp_load. refine_load O.
wp_op. refine_op O.
wp_store. refine_store O.
wp_seq. refine_seq O.
wp_load. refine_load O.
iSplitL ""; auto.
Qed.
Definition heap_e_hostore : expr :=
let: "x" := ref (λ: "_", heap_e) in
(!"x") #().
Lemma heap_e_hostore_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e_hostore K O)
⊢ WP heap_e_hostore @ E {{ v, ⧆(v = #2) ★ ownT i (of_val (#2)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_hostore /heap_e.
wp_alloc l. refine_alloc O l'.
wp_let. refine_let O.
wp_load. refine_load O.
wp_let. refine_let O.
iPoseProof (heap_e_spec E i K); eauto.
iApply "~4". iFrame "~". iFrame "~1". auto.
Qed.
Definition heap_e2 : expr :=
let: "x" := ref #1 in
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e2 K O)
⊢ WP heap_e2 @ E {{ v, ⧆(v = #2) ★ ownT i (of_val (#2)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e2.
wp_alloc l1. refine_alloc O l1'.
wp_let. refine_let O.
wp_alloc l2. refine_alloc O l2'.
wp_let. refine_let O.
wp_load. refine_load O.
wp_op. refine_op O.
wp_store. refine_store O.
wp_seq. refine_seq O.
wp_load. refine_load O.
by iFrame "Hown".
Qed.
Definition heap_e_fork : expr :=
let: "x" := ref #1 in Fork ("x" <- !"x" + #1) ;; #2.
Lemma heap_e_fork_spec E i K :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e_fork K O)
⊢ WP heap_e_fork @ E {{ v, ⧆(v = #2 ∨ v = #1) ★ ownT i (of_val (v)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_fork.
wp_alloc l. refine_alloc O l'.
wp_let. refine_let O.
wp_apply wp_fork.
refine_fork O i' as "Hown'".
iSplitL "Hown".
- wp_seq. refine_seq O. wp_value. iPvsIntro.
iFrame "Hown". iIntros "@". by iLeft.
- wp_load. refine_load O.
{ rewrite /fresh_delay //=. }
wp_op. refine_op O.
wp_store. refine_store O.
refine_stopped.
Qed.
Definition fork123 e1 e2 e3 : expr :=
Fork (Fork (#();; e1) ;; e2) ;; e3.
Lemma fork_siblings P1 P2 P3 (Q1 Q2 Q3: val → iProp) (e1 e2 e3: expr)
`{!Closed [] e1} `{!Closed [] e2} `{!Closed [] e3}:
(∀ i, {{ ⧆P1 ★ ownT i e1 [] O}} e1 {{v, ⧆ Q1 v ★ ownT i (of_val v) [] O}}) →
(∀ i, {{ ⧆P2 ★ ownT i e2 [] O}} e2 {{v, ⧆ Q2 v ★ ownT i (of_val v) [] O}}) →
(∀ i, {{ ⧆P3 ★ ownT i e3 [] O}} e3 {{v, ⧆ Q3 v ★ ownT i (of_val v) [] O}}) →
{{ sheap_ctx ★ ⧆P1 ★ ⧆P2 ★ ⧆P3 ★ ownT 0 (fork123 e1 e2 e3) [] O}}
fork123 e2 e1 e3
{{ v, ⧆ Q3 v ★ ownT 0 (of_val v) [] O}}.
Proof.
intros Ht1 Ht2 Ht3.
rewrite /ht. iIntros "_".
apply affine_intro; first apply _.
iIntros "! (#Hinv&P1&P2&P3&Hown)".
rewrite /fork123.
wp_apply wp_fork.
refine_fork O t' as "Hown'".
iSplitL "P3 Hown".
- wp_seq. refine_seq O.
iCombine "P3" "Hown" as "HP".
iPoseProof (Ht3 0%nat) as "Ht".
rewrite /ht.
rewrite affine_elim.
iClear "Hinv".
by iApply ("Ht").
- wp_apply wp_fork.
refine_fork O t'' as "Hown''".
{ rewrite /fresh_delay //=. }
iSplitL "P1 Hown''".
× wp_seq. refine_seq O.
{ rewrite /fresh_delay //=. }
iPoseProof (Ht1 t''%nat) as "Ht".
rewrite /ht.
rewrite affine_elim.
iClear "Hinv".
iCombine "P1" "Hown''" as "HP".
etransitivity; first by iApply ("Ht").
apply wp_mono. iIntros (v) "(?&?)". refine_stopped.
× wp_seq. refine_seq O.
iPoseProof (Ht2 t'%nat) as "Ht".
rewrite /ht.
rewrite affine_elim.
iClear "Hinv".
iCombine "P2" "Hown'" as "HP".
etransitivity; first by iApply "Ht".
apply wp_mono. iIntros (v) "(?&?)". refine_stopped.
Qed.
Definition do_while : expr :=
rec: "do_while" "x" :=
(if: "x" #() then "do_while" "x" else #()).
Lemma do_while_spec K E P Q (e e': expr) i `{!Closed [] e} `{!Closed [] e'} :
nclose sheapN ⊆ E →
(∀ K , (sheap_ctx ★ ownT i e' K O ★ ⧆ P)
⊢ WP e @ E {{ v, (⧆ (v = #true) ★ ⧆ P ∨ ⧆ (v = #false) ★ ⧆ Q)
★ ownT i (of_val v) K O}}) →
(sheap_ctx ★ ownT i (do_while (λ: "_", e'))%E K O ★ ⧆ P)
⊢ WP (do_while (λ: "_", e)) @ E {{ v, ⧆ (v = #()) ★ ⧆ Q ★ ownT i (of_val v) K O }}.
Proof.
iIntros (HN Hwp) "(#Hsheap&Hown&HP)".
iLob as "IH".
iIntros "@ ! Hown HP".
rewrite /do_while.
wp_rec. refine_rec O.
wp_let. refine_let O.
refine_focus e'.
iPoseProof (Hwp _) as "Hwp'".
iCombine "Hsheap" "Hown" as "H1".
iCombine "H1" "HP" as "H2".
rewrite assoc.
iSpecialize ("Hwp'" with "H2").
iApply wp_wand_l. iFrame "Hwp'".
apply affine_intro; first apply _.
iIntros (v) "(Hcase&Hown0)".
iDestruct "Hcase" as "[(%&HP)|(%&HQ)]"; subst.
- wp_if.
refine_unfocus.
refine_if_true O.
by iApply ("IH" with "Hown0").
- wp_if. refine_unfocus. refine_if_false O.
wp_value. iPvsIntro. iFrame "HQ". iFrame "Hown0".
done.
Qed.
Definition do_while_1 : expr :=
let: "l" := ref #0 in
(do_while (λ: "_", "l" <- !"l" + #1 ;; (!"l") < #3) ;; !"l").
Lemma do_while_1_spec K E i :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i do_while_1 K O)
⊢ WP do_while_1 @ E {{ v, v = #3 ★ ownT i (of_val (v)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e.
rewrite /do_while_1 /do_while.
wp_alloc l. refine_alloc O l'.
wp_let. refine_let O.
wp_focus ((rec: "do_while" "x" := _) _)%E.
refine_focus ((rec: "do_while" "x" := _) _)%E.
iPoseProof (do_while_spec (comp_ectx K (reverse [SeqCtx ! #l'])) E
(heap_ctx ★ ∃ (z: Z), ⧆■ (z < 3) ★ l' ↦s #z ★ l ↦ #z)%I
(l' ↦s #3 ★ l ↦ #3)%I
(#l <- ! #l + #1 ;; !#l < #3)%E
(#l' <- ! #l' + #1 ;; !#l' < #3)%E
i); eauto; last first.
- iCombine "~1" "Hown" as "Hfoo".
iCombine "~3" "~2" as "Hpt".
assert ((l' ↦s #0 ★ l ↦ #0) ⊢ (∃ (z: Z), ⧆■ (z < 3) ★ l' ↦s #z ★ l ↦ #z)) as →.
{ rewrite -(exist_intro 0).
rewrite pure_equiv; last omega.
rewrite -emp_True left_id. auto.
}
iCombine "~" "Hpt" as "Hpt'".
rewrite -{2}(affine_affine (heap_ctx ★ ∃ z: Z, _ ★ _)) .
iCombine "Hfoo" "Hpt'" as "Hfoo'".
rewrite -assoc. iSpecialize ("~4" with "Hfoo'").
iApply wp_wand_l. iFrame "~4".
apply affine_intro; first apply _. iIntros (v) "(%&Hpt&?)".
rewrite affine_elim.
iDestruct "Hpt" as "(Hpt1&Hpt2)".
wp_seq. refine_unfocus. refine_seq O.
wp_load. refine_load O. iFrame "~2". auto.
- intros K'; iProof.
iIntros "(#?&?&?)".
rewrite {1}affine_elim.
iDestruct "~2" as "(#?&?)".
iDestruct "~3" as (n) "(%&?&?)".
wp_load. refine_load O.
wp_op. refine_op O.
wp_store. refine_store O.
wp_seq. refine_seq O.
wp_load. refine_load O.
wp_op; intros.
× refine_op O; auto.
case_bool_decide; last exfalso; eauto.
iFrame "~1".
iLeft. rewrite affine_affine. iFrame "~2".
iSplitL ""; first done.
iExists (n+1).
iFrame "~3". iFrame "~4". rewrite pure_equiv; auto.
× refine_op O; auto.
case_bool_decide; first (exfalso; omega).
iFrame "~1".
iRight. rewrite affine_affine.
assert (n + 1 = 3) as →.
{ omega. }
iFrame "~3". iFrame "~4". rewrite pure_equiv; auto.
Qed.
Lemma do_while_hoist_read K E (P Q: val → iProp) (e e': expr) (l: loc) q u0 i
`{!Closed ["x"] e} `{!Closed ["x"] e'}:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(∀ K u, (sheap_ctx ★ ownT i (subst "x" (of_val u) e') K O ★ ⧆ (P u))
⊢ WP subst "x" (of_val u) e @ E {{ v, (⧆ (v = #true) ★ ⧆ (P u)
∨ ⧆ (v = #false) ★ ⧆ (Q u))
★ ownT i (of_val v) K O }}) →
(sheap_ctx ★ ownT i ((do_while (λ: "_", (let: "x" := ! #l in e'))))%E K O ★ ⧆ (P u0)
★ l↦s{q} u0)
⊢ WP (do_while (λ: "_", (Skip ;; (subst "x" (of_val u0) e))))%E
@ E {{ v, ⧆ (v = #()) ★ ⧆ (Q u0) ★ l↦s{q} u0 ★ ownT i (of_val v) K O }}.
Proof.
intros.
rewrite -{1}(affine_affine (l ↦s{q} u0)).
rewrite -(affine_affine (⧆ (P u0))).
rewrite sep_affine_distrib.
assert (Closed [] (subst "x" u0 e))%E.
{ apply is_closed_subst_remove; auto using is_closed_of_val. }
assert (Closed [] (subst "x" u0 e'))%E.
{ apply is_closed_subst_remove; auto using is_closed_of_val. }
assert (Closed [] (#() ;; #() ;; subst "x" u0 e))%E.
{ solve_closed. }
pose (e'' := (Lam "x" e')).
assert (Closed [] e'').
{ induction e'; try naive_solver. }
assert (Closed [] (let: "x" := ! #l in e'))%E.
{ fold e''. solve_closed. }
erewrite (do_while_spec K E (⧆P u0 ★ l↦s{q} u0)%I (Q u0 ★ l↦s{q} u0)%I
((#() ;; #()) ;; (subst "x" u0 e)) _ i); auto.
- apply wp_mono; intros; rewrite assoc.
rewrite -(affine_affine (l ↦s{q} u0)).
rewrite (comm _ (Q u0)).
rewrite -sep_affine_3.
rewrite -(comm _ (⧆ (Q u0))%I).
rewrite ?assoc. auto.
- intros. iProof. iIntros "(#?&Hown&Hinv)".
rewrite {1}affine_elim.
iDestruct "Hinv" as "(?&?)".
wp_seq. refine_load O.
wp_value. iPvsIntro. wp_seq. refine_seq O.
iPoseProof (H4 K0 u0).
iCombine "~" "Hown" as "Hfoo".
iCombine "Hfoo" "Hinv" as "Hfoo".
rewrite assoc.
iSpecialize ("~2" with "Hfoo").
iApply wp_wand_l; iFrame "~2".
apply affine_intro; first apply _.
iIntros (v) "([(%&HP)|(%&HQ)]&Hown)"; iFrame "Hown".
× iLeft. rewrite pure_equiv // -emp_True ?left_id.
apply affine_intro; first apply _.
iFrame "HP". iClear "~". auto.
× iRight. rewrite pure_equiv // -emp_True ?left_id.
apply affine_intro; first apply _.
rewrite affine_elim.
iFrame "HQ". iClear "~". auto.
Qed.
Lemma reorder_writes E vold1 vold2 (l1 l1': loc) (v1: val) (l2 l2': loc) (v2: val) i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i ( #l1' <- v1 ;; #l2' <- v2)%E K O
★ l1 ↦ vold1 ★ l1' ↦s vold1 ★ l2 ↦ vold2 ★ l2' ↦s vold2)%I
⊢ WP ( #l2 <- v2 ;; #l1 <- v1) @ E
{{ v, ⧆(v = #()) ★ l1 ↦ v1 ★ l1' ↦s v1 ★ l2 ↦ v2 ★ l2' ↦s v2
★ ownT i (of_val #()) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown&Hpt1&Hpts1&Hpt2&Hpts2)". rewrite /heap_e.
wp_store. refine_store O.
wp_seq. refine_seq O.
wp_store. refine_store O.
iFrame. done.
Qed.
End LiftingTests.
Section ClosedProofs.
Definition Σ : gFunctors := #[ heapGF ; sheapGF ;
refineGF (delayed_lang (heap_lang) O O)
(S O × (O + 3))].
Import heap_lang.
Notation iProp := (iPropG heap_lang Σ).
Lemma Σ_len: projT1 Σ = 3%nat.
Proof. auto. Qed.
Ltac gid_destruct g1 g2 :=
match type of g1 with
| fin ?T ⇒
refine
(match g1 as g' in fin n return ∀ (pf: n = T),
eq_rect n fin g' T pf = g1 →
_ with
| Fin.F1 _ ⇒ _
| FS _ g2 ⇒ _
end Init.Logic.eq_refl Init.Logic.eq_refl);
let pf := fresh "pf" in
intros pf ?; inversion pf; subst; simpl;
rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec; clear pf
| _ ⇒ fail g1 "is not a fin."
end.
Tactic Notation "gid_destruct" constr(g1) "as" simple_intropattern(g2) :=
gid_destruct g1 g2.
Instance inGF_refineG : refineG heap_lang Σ (delayed_lang (heap_lang) O O) (S O × (O + 3)).
Proof. eapply inGF_refineG. intros g A.
rewrite /gid in g ×.
assert (fin (projT1 Σ) = fin 3) as Hlen.
{ rewrite Σ_len. auto. }
rewrite /projT2 /Σ.
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
exfalso; eauto. }
inversion g.
Grab Existential Variables.
omega.
Qed.
Instance inGF_heapG: heapG Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 2%positive. Qed.
Instance inGF_scheapG: sheapG heap_lang Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 1%positive. Qed.
Definition lit_refine (l l': base_lit) :=
match l, l' with
| LitInt n, LitInt n' ⇒ n = n'
| LitBool b, LitBool b' ⇒ b = b'
| LitUnit, LitUnit ⇒ True
| LitLoc l, LitLoc l' ⇒ True
| _, _ ⇒ False
end.
Fixpoint val_refine (v v': val) :=
match v, v' with
| RecV _ _ _ _, RecV _ _ _ _ ⇒ True
| LitV l, LitV l' ⇒ lit_refine l l'
| PairV v1 v2, PairV v1' v2' ⇒ val_refine v1 v1' ∧ val_refine v2 v2'
| InjLV v, InjLV v' ⇒ val_refine v v'
| InjRV v, InjRV v' ⇒ val_refine v v'
| _, _ ⇒ False
end.
Lemma heap_e_refine σ:
safe_refine val_refine heap_e σ heap_e σ.
Proof.
eapply ht_safe_refine with (d := O).
- apply head_step_det_prim_det.
apply head_step_det.
- intros. edestruct (ClassicalEpsilon.excluded_middle_informative
((∃ (e' : language.expr (ectx_lang expr))
(σ' : language.state (ectx_lang expr ))
(ef' : option (language.expr (ectx_lang expr))),
language.prim_step e σ0 e' σ' ef'))).
× apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (e'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (σ'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (ef'&e0).
left. ∃ (e', σ', ef'). eauto.
× right. auto.
- rewrite comm -assoc.
rewrite /ht. iIntros "_".
apply affine_intro; first apply _.
iIntros "! (Hσ&Hsσ&Hown)".
iPvs (heap_alloc with "Hσ") as (h) "[Hheap ?]"; first by done.
iPvs (sheap_alloc with "Hsσ") as (h') "[Hsheap ?]"; first by done.
iPoseProof (heap_e_spec with "[Hheap Hsheap Hown]") as "Hspec"; eauto.
{ by iFrame. }
iApply wp_wand_l. iFrame "Hspec".
iIntros "@". iIntros (v) "(%&?)".
iExists #2.
iSplitR ""; first by iFrame.
iPureIntro. subst. econstructor.
Qed.
Print Assumptions heap_e_refine.
End ClosedProofs.
From iris.heap_lang Require Import proofmode refine_proofmode notation.
Import uPred.
Section LangTests.
Definition add : expr := (#21 + #21)%E.
Goal ∀ σ, head_step add σ (#42) σ None.
Proof. intros; do_head_step done. Qed.
Definition rec_app : expr := ((rec: "f" "x" := "f" "x") #0)%E.
Goal ∀ σ, head_step rec_app σ rec_app σ None.
Proof. intros. rewrite /rec_app. do_head_step done. Qed.
Definition lam : expr := (λ: "x", "x" + #21)%E.
Goal ∀ σ, head_step (lam #21)%E σ add σ None.
Proof. intros. rewrite /lam. do_head_step done. Qed.
End LangTests.
Section LiftingTests.
Context {Σ : gFunctors}.
Context `{refineG heap_lang Σ (delayed_lang (heap_lang) O O) (S O × (O + 3))}.
Context `{heapG Σ}.
Context `{sheapG heap_lang Σ}.
Local Notation iProp := (iPropG heap_lang Σ).
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
Lemma heap_e_spec E i K :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e K O)
⊢ WP heap_e @ E {{ v, ⧆(v = #2) ★ ownT i (of_val (#2)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e.
wp_alloc l. refine_alloc O l'.
wp_let. refine_let O.
wp_load. refine_load O.
wp_op. refine_op O.
wp_store. refine_store O.
wp_seq. refine_seq O.
wp_load. refine_load O.
iSplitL ""; auto.
Qed.
Definition heap_e_hostore : expr :=
let: "x" := ref (λ: "_", heap_e) in
(!"x") #().
Lemma heap_e_hostore_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e_hostore K O)
⊢ WP heap_e_hostore @ E {{ v, ⧆(v = #2) ★ ownT i (of_val (#2)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_hostore /heap_e.
wp_alloc l. refine_alloc O l'.
wp_let. refine_let O.
wp_load. refine_load O.
wp_let. refine_let O.
iPoseProof (heap_e_spec E i K); eauto.
iApply "~4". iFrame "~". iFrame "~1". auto.
Qed.
Definition heap_e2 : expr :=
let: "x" := ref #1 in
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e2 K O)
⊢ WP heap_e2 @ E {{ v, ⧆(v = #2) ★ ownT i (of_val (#2)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e2.
wp_alloc l1. refine_alloc O l1'.
wp_let. refine_let O.
wp_alloc l2. refine_alloc O l2'.
wp_let. refine_let O.
wp_load. refine_load O.
wp_op. refine_op O.
wp_store. refine_store O.
wp_seq. refine_seq O.
wp_load. refine_load O.
by iFrame "Hown".
Qed.
Definition heap_e_fork : expr :=
let: "x" := ref #1 in Fork ("x" <- !"x" + #1) ;; #2.
Lemma heap_e_fork_spec E i K :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e_fork K O)
⊢ WP heap_e_fork @ E {{ v, ⧆(v = #2 ∨ v = #1) ★ ownT i (of_val (v)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_fork.
wp_alloc l. refine_alloc O l'.
wp_let. refine_let O.
wp_apply wp_fork.
refine_fork O i' as "Hown'".
iSplitL "Hown".
- wp_seq. refine_seq O. wp_value. iPvsIntro.
iFrame "Hown". iIntros "@". by iLeft.
- wp_load. refine_load O.
{ rewrite /fresh_delay //=. }
wp_op. refine_op O.
wp_store. refine_store O.
refine_stopped.
Qed.
Definition fork123 e1 e2 e3 : expr :=
Fork (Fork (#();; e1) ;; e2) ;; e3.
Lemma fork_siblings P1 P2 P3 (Q1 Q2 Q3: val → iProp) (e1 e2 e3: expr)
`{!Closed [] e1} `{!Closed [] e2} `{!Closed [] e3}:
(∀ i, {{ ⧆P1 ★ ownT i e1 [] O}} e1 {{v, ⧆ Q1 v ★ ownT i (of_val v) [] O}}) →
(∀ i, {{ ⧆P2 ★ ownT i e2 [] O}} e2 {{v, ⧆ Q2 v ★ ownT i (of_val v) [] O}}) →
(∀ i, {{ ⧆P3 ★ ownT i e3 [] O}} e3 {{v, ⧆ Q3 v ★ ownT i (of_val v) [] O}}) →
{{ sheap_ctx ★ ⧆P1 ★ ⧆P2 ★ ⧆P3 ★ ownT 0 (fork123 e1 e2 e3) [] O}}
fork123 e2 e1 e3
{{ v, ⧆ Q3 v ★ ownT 0 (of_val v) [] O}}.
Proof.
intros Ht1 Ht2 Ht3.
rewrite /ht. iIntros "_".
apply affine_intro; first apply _.
iIntros "! (#Hinv&P1&P2&P3&Hown)".
rewrite /fork123.
wp_apply wp_fork.
refine_fork O t' as "Hown'".
iSplitL "P3 Hown".
- wp_seq. refine_seq O.
iCombine "P3" "Hown" as "HP".
iPoseProof (Ht3 0%nat) as "Ht".
rewrite /ht.
rewrite affine_elim.
iClear "Hinv".
by iApply ("Ht").
- wp_apply wp_fork.
refine_fork O t'' as "Hown''".
{ rewrite /fresh_delay //=. }
iSplitL "P1 Hown''".
× wp_seq. refine_seq O.
{ rewrite /fresh_delay //=. }
iPoseProof (Ht1 t''%nat) as "Ht".
rewrite /ht.
rewrite affine_elim.
iClear "Hinv".
iCombine "P1" "Hown''" as "HP".
etransitivity; first by iApply ("Ht").
apply wp_mono. iIntros (v) "(?&?)". refine_stopped.
× wp_seq. refine_seq O.
iPoseProof (Ht2 t'%nat) as "Ht".
rewrite /ht.
rewrite affine_elim.
iClear "Hinv".
iCombine "P2" "Hown'" as "HP".
etransitivity; first by iApply "Ht".
apply wp_mono. iIntros (v) "(?&?)". refine_stopped.
Qed.
Definition do_while : expr :=
rec: "do_while" "x" :=
(if: "x" #() then "do_while" "x" else #()).
Lemma do_while_spec K E P Q (e e': expr) i `{!Closed [] e} `{!Closed [] e'} :
nclose sheapN ⊆ E →
(∀ K , (sheap_ctx ★ ownT i e' K O ★ ⧆ P)
⊢ WP e @ E {{ v, (⧆ (v = #true) ★ ⧆ P ∨ ⧆ (v = #false) ★ ⧆ Q)
★ ownT i (of_val v) K O}}) →
(sheap_ctx ★ ownT i (do_while (λ: "_", e'))%E K O ★ ⧆ P)
⊢ WP (do_while (λ: "_", e)) @ E {{ v, ⧆ (v = #()) ★ ⧆ Q ★ ownT i (of_val v) K O }}.
Proof.
iIntros (HN Hwp) "(#Hsheap&Hown&HP)".
iLob as "IH".
iIntros "@ ! Hown HP".
rewrite /do_while.
wp_rec. refine_rec O.
wp_let. refine_let O.
refine_focus e'.
iPoseProof (Hwp _) as "Hwp'".
iCombine "Hsheap" "Hown" as "H1".
iCombine "H1" "HP" as "H2".
rewrite assoc.
iSpecialize ("Hwp'" with "H2").
iApply wp_wand_l. iFrame "Hwp'".
apply affine_intro; first apply _.
iIntros (v) "(Hcase&Hown0)".
iDestruct "Hcase" as "[(%&HP)|(%&HQ)]"; subst.
- wp_if.
refine_unfocus.
refine_if_true O.
by iApply ("IH" with "Hown0").
- wp_if. refine_unfocus. refine_if_false O.
wp_value. iPvsIntro. iFrame "HQ". iFrame "Hown0".
done.
Qed.
Definition do_while_1 : expr :=
let: "l" := ref #0 in
(do_while (λ: "_", "l" <- !"l" + #1 ;; (!"l") < #3) ;; !"l").
Lemma do_while_1_spec K E i :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i do_while_1 K O)
⊢ WP do_while_1 @ E {{ v, v = #3 ★ ownT i (of_val (v)) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e.
rewrite /do_while_1 /do_while.
wp_alloc l. refine_alloc O l'.
wp_let. refine_let O.
wp_focus ((rec: "do_while" "x" := _) _)%E.
refine_focus ((rec: "do_while" "x" := _) _)%E.
iPoseProof (do_while_spec (comp_ectx K (reverse [SeqCtx ! #l'])) E
(heap_ctx ★ ∃ (z: Z), ⧆■ (z < 3) ★ l' ↦s #z ★ l ↦ #z)%I
(l' ↦s #3 ★ l ↦ #3)%I
(#l <- ! #l + #1 ;; !#l < #3)%E
(#l' <- ! #l' + #1 ;; !#l' < #3)%E
i); eauto; last first.
- iCombine "~1" "Hown" as "Hfoo".
iCombine "~3" "~2" as "Hpt".
assert ((l' ↦s #0 ★ l ↦ #0) ⊢ (∃ (z: Z), ⧆■ (z < 3) ★ l' ↦s #z ★ l ↦ #z)) as →.
{ rewrite -(exist_intro 0).
rewrite pure_equiv; last omega.
rewrite -emp_True left_id. auto.
}
iCombine "~" "Hpt" as "Hpt'".
rewrite -{2}(affine_affine (heap_ctx ★ ∃ z: Z, _ ★ _)) .
iCombine "Hfoo" "Hpt'" as "Hfoo'".
rewrite -assoc. iSpecialize ("~4" with "Hfoo'").
iApply wp_wand_l. iFrame "~4".
apply affine_intro; first apply _. iIntros (v) "(%&Hpt&?)".
rewrite affine_elim.
iDestruct "Hpt" as "(Hpt1&Hpt2)".
wp_seq. refine_unfocus. refine_seq O.
wp_load. refine_load O. iFrame "~2". auto.
- intros K'; iProof.
iIntros "(#?&?&?)".
rewrite {1}affine_elim.
iDestruct "~2" as "(#?&?)".
iDestruct "~3" as (n) "(%&?&?)".
wp_load. refine_load O.
wp_op. refine_op O.
wp_store. refine_store O.
wp_seq. refine_seq O.
wp_load. refine_load O.
wp_op; intros.
× refine_op O; auto.
case_bool_decide; last exfalso; eauto.
iFrame "~1".
iLeft. rewrite affine_affine. iFrame "~2".
iSplitL ""; first done.
iExists (n+1).
iFrame "~3". iFrame "~4". rewrite pure_equiv; auto.
× refine_op O; auto.
case_bool_decide; first (exfalso; omega).
iFrame "~1".
iRight. rewrite affine_affine.
assert (n + 1 = 3) as →.
{ omega. }
iFrame "~3". iFrame "~4". rewrite pure_equiv; auto.
Qed.
Lemma do_while_hoist_read K E (P Q: val → iProp) (e e': expr) (l: loc) q u0 i
`{!Closed ["x"] e} `{!Closed ["x"] e'}:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(∀ K u, (sheap_ctx ★ ownT i (subst "x" (of_val u) e') K O ★ ⧆ (P u))
⊢ WP subst "x" (of_val u) e @ E {{ v, (⧆ (v = #true) ★ ⧆ (P u)
∨ ⧆ (v = #false) ★ ⧆ (Q u))
★ ownT i (of_val v) K O }}) →
(sheap_ctx ★ ownT i ((do_while (λ: "_", (let: "x" := ! #l in e'))))%E K O ★ ⧆ (P u0)
★ l↦s{q} u0)
⊢ WP (do_while (λ: "_", (Skip ;; (subst "x" (of_val u0) e))))%E
@ E {{ v, ⧆ (v = #()) ★ ⧆ (Q u0) ★ l↦s{q} u0 ★ ownT i (of_val v) K O }}.
Proof.
intros.
rewrite -{1}(affine_affine (l ↦s{q} u0)).
rewrite -(affine_affine (⧆ (P u0))).
rewrite sep_affine_distrib.
assert (Closed [] (subst "x" u0 e))%E.
{ apply is_closed_subst_remove; auto using is_closed_of_val. }
assert (Closed [] (subst "x" u0 e'))%E.
{ apply is_closed_subst_remove; auto using is_closed_of_val. }
assert (Closed [] (#() ;; #() ;; subst "x" u0 e))%E.
{ solve_closed. }
pose (e'' := (Lam "x" e')).
assert (Closed [] e'').
{ induction e'; try naive_solver. }
assert (Closed [] (let: "x" := ! #l in e'))%E.
{ fold e''. solve_closed. }
erewrite (do_while_spec K E (⧆P u0 ★ l↦s{q} u0)%I (Q u0 ★ l↦s{q} u0)%I
((#() ;; #()) ;; (subst "x" u0 e)) _ i); auto.
- apply wp_mono; intros; rewrite assoc.
rewrite -(affine_affine (l ↦s{q} u0)).
rewrite (comm _ (Q u0)).
rewrite -sep_affine_3.
rewrite -(comm _ (⧆ (Q u0))%I).
rewrite ?assoc. auto.
- intros. iProof. iIntros "(#?&Hown&Hinv)".
rewrite {1}affine_elim.
iDestruct "Hinv" as "(?&?)".
wp_seq. refine_load O.
wp_value. iPvsIntro. wp_seq. refine_seq O.
iPoseProof (H4 K0 u0).
iCombine "~" "Hown" as "Hfoo".
iCombine "Hfoo" "Hinv" as "Hfoo".
rewrite assoc.
iSpecialize ("~2" with "Hfoo").
iApply wp_wand_l; iFrame "~2".
apply affine_intro; first apply _.
iIntros (v) "([(%&HP)|(%&HQ)]&Hown)"; iFrame "Hown".
× iLeft. rewrite pure_equiv // -emp_True ?left_id.
apply affine_intro; first apply _.
iFrame "HP". iClear "~". auto.
× iRight. rewrite pure_equiv // -emp_True ?left_id.
apply affine_intro; first apply _.
rewrite affine_elim.
iFrame "HQ". iClear "~". auto.
Qed.
Lemma reorder_writes E vold1 vold2 (l1 l1': loc) (v1: val) (l2 l2': loc) (v2: val) i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i ( #l1' <- v1 ;; #l2' <- v2)%E K O
★ l1 ↦ vold1 ★ l1' ↦s vold1 ★ l2 ↦ vold2 ★ l2' ↦s vold2)%I
⊢ WP ( #l2 <- v2 ;; #l1 <- v1) @ E
{{ v, ⧆(v = #()) ★ l1 ↦ v1 ★ l1' ↦s v1 ★ l2 ↦ v2 ★ l2' ↦s v2
★ ownT i (of_val #()) K O}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown&Hpt1&Hpts1&Hpt2&Hpts2)". rewrite /heap_e.
wp_store. refine_store O.
wp_seq. refine_seq O.
wp_store. refine_store O.
iFrame. done.
Qed.
End LiftingTests.
Section ClosedProofs.
Definition Σ : gFunctors := #[ heapGF ; sheapGF ;
refineGF (delayed_lang (heap_lang) O O)
(S O × (O + 3))].
Import heap_lang.
Notation iProp := (iPropG heap_lang Σ).
Lemma Σ_len: projT1 Σ = 3%nat.
Proof. auto. Qed.
Ltac gid_destruct g1 g2 :=
match type of g1 with
| fin ?T ⇒
refine
(match g1 as g' in fin n return ∀ (pf: n = T),
eq_rect n fin g' T pf = g1 →
_ with
| Fin.F1 _ ⇒ _
| FS _ g2 ⇒ _
end Init.Logic.eq_refl Init.Logic.eq_refl);
let pf := fresh "pf" in
intros pf ?; inversion pf; subst; simpl;
rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec; clear pf
| _ ⇒ fail g1 "is not a fin."
end.
Tactic Notation "gid_destruct" constr(g1) "as" simple_intropattern(g2) :=
gid_destruct g1 g2.
Instance inGF_refineG : refineG heap_lang Σ (delayed_lang (heap_lang) O O) (S O × (O + 3)).
Proof. eapply inGF_refineG. intros g A.
rewrite /gid in g ×.
assert (fin (projT1 Σ) = fin 3) as Hlen.
{ rewrite Σ_len. auto. }
rewrite /projT2 /Σ.
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
exfalso; eauto. }
inversion g.
Grab Existential Variables.
omega.
Qed.
Instance inGF_heapG: heapG Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 2%positive. Qed.
Instance inGF_scheapG: sheapG heap_lang Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 1%positive. Qed.
Definition lit_refine (l l': base_lit) :=
match l, l' with
| LitInt n, LitInt n' ⇒ n = n'
| LitBool b, LitBool b' ⇒ b = b'
| LitUnit, LitUnit ⇒ True
| LitLoc l, LitLoc l' ⇒ True
| _, _ ⇒ False
end.
Fixpoint val_refine (v v': val) :=
match v, v' with
| RecV _ _ _ _, RecV _ _ _ _ ⇒ True
| LitV l, LitV l' ⇒ lit_refine l l'
| PairV v1 v2, PairV v1' v2' ⇒ val_refine v1 v1' ∧ val_refine v2 v2'
| InjLV v, InjLV v' ⇒ val_refine v v'
| InjRV v, InjRV v' ⇒ val_refine v v'
| _, _ ⇒ False
end.
Lemma heap_e_refine σ:
safe_refine val_refine heap_e σ heap_e σ.
Proof.
eapply ht_safe_refine with (d := O).
- apply head_step_det_prim_det.
apply head_step_det.
- intros. edestruct (ClassicalEpsilon.excluded_middle_informative
((∃ (e' : language.expr (ectx_lang expr))
(σ' : language.state (ectx_lang expr ))
(ef' : option (language.expr (ectx_lang expr))),
language.prim_step e σ0 e' σ' ef'))).
× apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (e'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (σ'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (ef'&e0).
left. ∃ (e', σ', ef'). eauto.
× right. auto.
- rewrite comm -assoc.
rewrite /ht. iIntros "_".
apply affine_intro; first apply _.
iIntros "! (Hσ&Hsσ&Hown)".
iPvs (heap_alloc with "Hσ") as (h) "[Hheap ?]"; first by done.
iPvs (sheap_alloc with "Hsσ") as (h') "[Hsheap ?]"; first by done.
iPoseProof (heap_e_spec with "[Hheap Hsheap Hown]") as "Hspec"; eauto.
{ by iFrame. }
iApply wp_wand_l. iFrame "Hspec".
iIntros "@". iIntros (v) "(%&?)".
iExists #2.
iSplitR ""; first by iFrame.
iPureIntro. subst. econstructor.
Qed.
Print Assumptions heap_e_refine.
End ClosedProofs.