Skip to content
Snippets Groups Projects
Commit 952daeb9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'speedup-lifting' into 'master' 

heap_lang/lifting.v: Don't run auto on hopeless goals

See merge request iris/iris!369
parents 87e4f965 9dc1d480
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/heap_lang/lifting.v
+ 15
− 17
View file @ 952daeb9
...@@ -277,7 +277,7 @@ Lemma wp_allocN_seq s E v n : ...@@ -277,7 +277,7 @@ Lemma wp_allocN_seq s E v n :
{{{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n), {{{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
(l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }}}. (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }}}.
Proof. Proof.
iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by auto with lia. iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by auto with lia.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (gen_heap_alloc_gen _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ") iMod (gen_heap_alloc_gen _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
...@@ -295,7 +295,7 @@ Lemma twp_allocN_seq s E v n : ...@@ -295,7 +295,7 @@ Lemma twp_allocN_seq s E v n :
[[{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n), [[{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
(l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }]]. (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }]].
Proof. Proof.
iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia. iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
iIntros (κ v2 σ2 efs Hstep); inv_head_step. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (gen_heap_alloc_gen _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ") iMod (gen_heap_alloc_gen _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
...@@ -311,20 +311,20 @@ Qed. ...@@ -311,20 +311,20 @@ Qed.
Lemma wp_alloc s E v : Lemma wp_alloc s E v :
{{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }}}. {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }}}.
Proof. Proof.
iIntros (Φ) "_ HΦ". iApply wp_allocN_seq; auto with lia. iIntros (Φ) "_ HΦ". iApply wp_allocN_seq; [auto with lia..|].
iIntros "!>" (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame. iIntros "!>" (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
Qed. Qed.
Lemma twp_alloc s E v : Lemma twp_alloc s E v :
[[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }]]. [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }]].
Proof. Proof.
iIntros (Φ) "_ HΦ". iApply twp_allocN_seq; auto with lia. iIntros (Φ) "_ HΦ". iApply twp_allocN_seq; [auto with lia..|].
iIntros (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame. iIntros (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
Qed. Qed.
Lemma wp_load s E l q v : Lemma wp_load s E l q v :
{{{ ▷ l ↦{q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{q} v }}}. {{{ ▷ l ↦{q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{q} v }}}.
Proof. Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ". iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
...@@ -332,7 +332,7 @@ Qed. ...@@ -332,7 +332,7 @@ Qed.
Lemma twp_load s E l q v : Lemma twp_load s E l q v :
[[{ l ↦{q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{q} v }]]. [[{ l ↦{q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{q} v }]].
Proof. Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ". iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
...@@ -342,8 +342,7 @@ Lemma wp_store s E l v' v : ...@@ -342,8 +342,7 @@ Lemma wp_store s E l v' v :
{{{ ▷ l ↦ v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E {{{ ▷ l ↦ v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
{{{ RET LitV LitUnit; l ↦ v }}}. {{{ RET LitV LitUnit; l ↦ v }}}.
Proof. Proof.
iIntros (Φ) ">Hl HΦ". iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]". iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
...@@ -353,8 +352,7 @@ Lemma twp_store s E l v' v : ...@@ -353,8 +352,7 @@ Lemma twp_store s E l v' v :
[[{ l ↦ v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E [[{ l ↦ v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E
[[{ RET LitV LitUnit; l ↦ v }]]. [[{ RET LitV LitUnit; l ↦ v }]].
Proof. Proof.
iIntros (Φ) "Hl HΦ". iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]". iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
...@@ -366,7 +364,7 @@ Lemma wp_cmpxchg_fail s E l q v' v1 v2 : ...@@ -366,7 +364,7 @@ Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
{{{ ▷ l ↦{q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E {{{ ▷ l ↦{q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }}}. {{{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }}}.
Proof. Proof.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
rewrite bool_decide_false //. rewrite bool_decide_false //.
...@@ -377,7 +375,7 @@ Lemma twp_cmpxchg_fail s E l q v' v1 v2 : ...@@ -377,7 +375,7 @@ Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
[[{ l ↦{q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E [[{ l ↦{q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }]]. [[{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }]].
Proof. Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
rewrite bool_decide_false //. rewrite bool_decide_false //.
...@@ -389,7 +387,7 @@ Lemma wp_cmpxchg_suc s E l v1 v2 v' : ...@@ -389,7 +387,7 @@ Lemma wp_cmpxchg_suc s E l v1 v2 v' :
{{{ ▷ l ↦ v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E {{{ ▷ l ↦ v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }}}. {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }}}.
Proof. Proof.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
rewrite bool_decide_true //. rewrite bool_decide_true //.
...@@ -401,7 +399,7 @@ Lemma twp_cmpxchg_suc s E l v1 v2 v' : ...@@ -401,7 +399,7 @@ Lemma twp_cmpxchg_suc s E l v1 v2 v' :
[[{ l ↦ v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E [[{ l ↦ v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }]]. [[{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }]].
Proof. Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
rewrite bool_decide_true //. rewrite bool_decide_true //.
...@@ -413,7 +411,7 @@ Lemma wp_faa s E l i1 i2 : ...@@ -413,7 +411,7 @@ Lemma wp_faa s E l i1 i2 :
{{{ ▷ l ↦ LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E {{{ ▷ l ↦ LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
{{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }}}. {{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }}}.
Proof. Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]". iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
...@@ -423,7 +421,7 @@ Lemma twp_faa s E l i1 i2 : ...@@ -423,7 +421,7 @@ Lemma twp_faa s E l i1 i2 :
[[{ l ↦ LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E [[{ l ↦ LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
[[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]]. [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
Proof. Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]". iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
...@@ -435,7 +433,7 @@ Lemma wp_new_proph s E : ...@@ -435,7 +433,7 @@ Lemma wp_new_proph s E :
NewProph @ s; E NewProph @ s; E
{{{ pvs p, RET (LitV (LitProphecy p)); proph p pvs }}}. {{{ pvs p, RET (LitV (LitProphecy p)); proph p pvs }}}.
Proof. Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto. iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep). inv_head_step. iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done. iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment