Commit eafd77e6 authored by Ralf Jung's avatar Ralf Jung

use equality instead of let binding

parent 242cee02
...@@ -634,11 +634,11 @@ Inductive head_step : expr → state → list observation → expr → state → ...@@ -634,11 +634,11 @@ Inductive head_step : expr → state → list observation → expr → state →
[] []
(Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ) (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
[] []
| CompareExchangeS l v1 v2 vl σ : | CompareExchangeS l v1 v2 vl σ b :
vals_cas_compare_safe vl v1 vals_cas_compare_safe vl v1
σ.(heap) !! l = Some vl σ.(heap) !! l = Some vl
(* Crucially, this compares the same way as [EqOp]! *) (* Crucially, this compares the same way as [EqOp]! *)
let b := bool_decide (val_for_compare vl = val_for_compare v1) in b = bool_decide (val_for_compare vl = val_for_compare v1)
head_step (CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ head_step (CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
[] []
(Val $ PairV (LitV $ LitBool b) vl) (if b then state_upd_heap <[l:=v2]> σ else σ) (Val $ PairV (LitV $ LitBool b) vl) (if b then state_upd_heap <[l:=v2]> σ else σ)
......
...@@ -382,7 +382,7 @@ Proof. ...@@ -382,7 +382,7 @@ Proof.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) ">Hl HΦ". 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.
rewrite /b bool_decide_false //. rewrite bool_decide_false //.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ". iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed. Qed.
Lemma twp_cas_fail s E l q v' v1 v2 : Lemma twp_cas_fail s E l q v' v1 v2 :
...@@ -393,7 +393,7 @@ Proof. ...@@ -393,7 +393,7 @@ Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) "Hl HΦ". 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.
rewrite /b bool_decide_false //. rewrite bool_decide_false //.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ". iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
Qed. Qed.
...@@ -405,7 +405,7 @@ Proof. ...@@ -405,7 +405,7 @@ Proof.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) ">Hl HΦ". 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.
rewrite /b bool_decide_true //. rewrite bool_decide_true //.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]". iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ". iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed. Qed.
...@@ -417,7 +417,7 @@ Proof. ...@@ -417,7 +417,7 @@ Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto. iIntros (?? Φ) "Hl HΦ". 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.
rewrite /b bool_decide_true //. rewrite bool_decide_true //.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]". iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ". iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed. Qed.
......
Markdown is supported
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