Commit 1229cc72 authored by Simon Hudon's avatar Simon Hudon
Browse files

remove unboxed assumptions

parent 78b3986b
......@@ -207,40 +207,32 @@ Qed.
Lemma twp_xchg_offset s E l off vs v v' :
vs !! off = Some v
val_is_unboxed v
val_is_unboxed v'
[[{ l ↦∗ vs }]] Xchg #(l + off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
Proof.
iIntros (Hlookup Hunboxed Hunboxed' Φ) "Hl HΦ".
iIntros (Hlookup Φ) "Hl HΦ".
iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
iApply (twp_xchg with "Hl1") => //. iIntros "Hl1".
iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
Lemma wp_xchg_offset s E l off vs v v' :
vs !! off = Some v
val_is_unboxed v
val_is_unboxed v'
{{{ l ↦∗ vs }}} Xchg #(l + off) v' @ s; E {{{ RET v; l ↦∗ <[off:=v']> vs }}}.
Proof.
iIntros (? ? ? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_xchg_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Lemma twp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
val_is_unboxed (vs !!! off)
val_is_unboxed v
[[{ l ↦∗ vs }]] Xchg #(l + off) v @ s; E [[{ RET (vs !!! off); l ↦∗ vinsert off v vs }]].
Proof.
intros ? ?. setoid_rewrite vec_to_list_insert. apply twp_xchg_offset => //.
setoid_rewrite vec_to_list_insert. apply twp_xchg_offset => //.
by apply vlookup_lookup.
Qed.
Lemma wp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
val_is_unboxed (vs !!! off)
val_is_unboxed v
{{{ l ↦∗ vs }}} Xchg #(l + off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
{{{ l ↦∗ vs }}} Xchg #(l + off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
Proof.
iIntros (? ? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_xchg_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
......
......@@ -684,8 +684,6 @@ Inductive head_step : expr → state → list observation → expr → state →
[]
| XchgS l v1 v2 σ :
σ.(heap) !! l = Some $ Some v1
val_is_unboxed v1
val_is_unboxed v2
head_step (Xchg (Val $ LitV $ LitLoc l) (Val v2)) σ
[]
(Val v1) (state_upd_heap <[l:=Some v2]> σ)
......
......@@ -313,12 +313,10 @@ Proof.
Qed.
Lemma twp_xchg s E l v' v :
val_is_unboxed v
val_is_unboxed v'
[[{ l v' }]] Xchg (Val $ LitV $ LitLoc l) (Val v) @ s; E
[[{ RET v'; l v }]].
Proof.
iIntros (Hv Hv' Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
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 %?.
iSplit; first by eauto with head_step.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
......@@ -327,12 +325,10 @@ Proof.
Qed.
Lemma wp_xchg s E l v' v :
val_is_unboxed v
val_is_unboxed v'
{{{ l v' }}} Xchg (Val $ LitV (LitLoc l)) (Val v) @ s; E
{{{ RET v'; l v }}}.
Proof.
iIntros (Hv Hv' Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_xchg with "H"); [by auto..|]. iIntros "H HΦ". by iApply "HΦ".
Qed.
......
......@@ -373,15 +373,13 @@ Qed.
Lemma tac_wp_xchg Δ Δ' s E i K l v v' Φ :
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
val_is_unboxed v'
val_is_unboxed v
match envs_simple_replace i false (Esnoc Enil i (l v')) Δ' with
| Some Δ'' => envs_entails Δ'' (WP fill K (Val $ v) @ s; E {{ Φ }})
| None => False
end
envs_entails Δ (WP fill K (Xchg (LitV l) (Val v')) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ?????.
rewrite envs_entails_eq=> ???.
destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
......@@ -390,8 +388,6 @@ Proof.
Qed.
Lemma tac_twp_xchg Δ s E i K l v v' Φ :
envs_lookup i Δ = Some (false, l v)%I
val_is_unboxed v'
val_is_unboxed v
match envs_simple_replace i false (Esnoc Enil i (l v')) Δ with
| Some Δ' => envs_entails Δ' (WP fill K (Val $ v) @ s; E [{ Φ }])
| None => False
......
......@@ -279,16 +279,13 @@ Proof.
eexists _, _, _, _; simpl; split; first econstructor; eauto.
Qed.
Lemma erased_head_step_head_step_Xchg l v w σ :
val_is_unboxed v
val_is_unboxed w
erase_heap (heap σ) !! l = Some (Some v)
head_steps_to_erasure_of (Xchg #l w) σ v
{| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ)); used_proph_id := |} [].
Proof.
intros Hv Hw Hl.
intros Hl.
rewrite lookup_erase_heap in Hl.
destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
rewrite val_is_unboxed_erased in Hv * => //; intros Hv.
eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
Qed.
......@@ -725,14 +722,11 @@ Proof.
Qed.
Lemma head_step_erased_prim_step_xchg σ l v w :
val_is_unboxed v
val_is_unboxed w
heap σ !! l = Some (Some v)
e2' σ2' ef', prim_step (Xchg #l (erase_val w)) (erase_state σ) [] e2' σ2' ef'.
Proof.
intros Hv Hw Hl. do 3 eexists; apply head_prim_step; econstructor.
1: rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl; eauto.
1,2: by rewrite val_is_unboxed_erased.
intros Hl. do 3 eexists; apply head_prim_step; econstructor.
rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl; eauto.
Qed.
Lemma head_step_erased_prim_step_store σ l v w :
......
Supports Markdown
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