Commit 13acc121 authored by Michael Sammler's avatar Michael Sammler
Browse files

Don't use val_to_Z_Some_inj and add wp cas rules for int and bool

parent 813d3206
Pipeline #45213 passed with stage
in 17 minutes and 32 seconds
......@@ -144,24 +144,10 @@ Section proofs.
iIntros "???" (Φ) "HΦ".
destruct (decide (next = i)) as [<-|] .
** iRename select (_ ◁ₗ next @ int u16)%I into "Hnext".
iDestruct (ty_aligned with "Hnext") as %?.
iDestruct (ty_deref with "Hnext") as (?) "[Hnext Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iRename select (_ ◁ₗ (next + 1) @ int u16)%I into "Hnext+1".
iDestruct (ty_aligned with "Hnext+1") as %?.
iDestruct (ty_deref with "Hnext+1") as (?) "[Hnext+1 Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (_ ◁ᵥ (next + 1) @ int u16)%I as "Hv".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (local_ticket ◁ᵥ _)%I as "[_ Hticket]".
iDestruct (ty_aligned with "Hticket") as %?.
iDestruct (ty_deref with "Hticket") as (?) "[Hticket Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (p at{_} _ ◁ᵥ _)%I as "[_ ->]".
iApply (wp_cas_suc _ _ _ v2 v4 next next _ _ _ u16 _ _ with "Hnext Hticket") => //.
{ by rewrite val_to_of_loc. }
{ by rewrite val_to_of_loc. }
{ cbv. lia. }
iApply (wp_cas_suc_int with "Hnext Hticket [$]"). { cbv. lia. } done.
iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (true @ boolean bool_it))%I) => //.
repeat liRStep; liShow.
rewrite /hyp_spinlock_t_invariant.
......@@ -171,44 +157,19 @@ Section proofs.
liInst Hevar2 (next + 1).
liInst Hevar0 next.
repeat liRStep; liShow.
iRename select (p at{struct_hyp_spinlock} _ _)%I into "Hnext".
iSplitL "Hnext".
{ iDestruct (ty_ref (t := (next + 1) @ int u16)%I with "[] Hnext []") as "$" => //. }
iDestruct select (owner_frag _ _) as "$".
iDestruct select (ticket_range _ 0 _) as "$".
iRename select (ticket_range _ _ _) into "Htks".
iDestruct (split_first_ticket with "Htks") as "[$$]".
iDestruct (split_first_ticket with "Htks") as "[Hnext $]".
{ split; last by lia. by transitivity (min_int u16) => //. }
iRename select (_ _)%I into "Hcases".
iSplitL "Hcases".
{ iDestruct "Hcases" as "[[H %]|H]"; [iLeft | iRight] => //. iSplitL => //. iPureIntro. lia. }
iDestruct (ty_ref (t := uninit u16) with "[] Hnext+1 []") as "$" => //.
{ iPureIntro. split => //. by apply Forall_forall. }
iRename select (local_ticket _)%I into "Hticket".
iRename select (local_got_it ◁ₗ _)%I into "Hgot_it".
iDestruct (ty_ref (t := next @ int u16) with "[] Hticket []") as "$" => //.
iDestruct (ty_aligned with "Hgot_it") as %?.
iDestruct (ty_deref with "Hgot_it") as (?) "[Hgot_it [% ->]]".
iDestruct (ty_ref (t := true @ boolean bool_it) with "[] Hgot_it []") as "$" => //.
repeat liRStep; liShow.
** iRename select (_ ◁ₗ next @ int u16)%I into "Hnext".
iDestruct (ty_aligned with "Hnext") as %?.
iDestruct (ty_deref with "Hnext") as (?) "[Hnext Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iRename select (_ ◁ₗ (i + 1) @ int u16)%I into "Hi+1".
iDestruct (ty_aligned with "Hi+1") as %?.
iDestruct (ty_deref with "Hi+1") as (?) "[Hi+1 Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (_ ◁ᵥ (i + 1) @ int u16)%I as "Hv".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (local_ticket ◁ᵥ _)%I as "[_ Hticket]".
iDestruct (ty_aligned with "Hticket") as %?.
iDestruct (ty_deref with "Hticket") as (?) "[Hticket Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (p at{_} _ ◁ᵥ _)%I as "[_ ->]".
iApply (wp_cas_fail _ _ _ v2 v4 next i _ _ _ u16 _ _ with "Hnext Hticket") => //.
{ by rewrite val_to_of_loc. }
{ by rewrite val_to_of_loc. }
{ cbv. lia. }
iApply (wp_cas_fail_int with "Hnext Hticket [$]"). { cbv. lia. } done.
iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (false @ boolean bool_it))%I) => //.
repeat liRStep; liShow.
rewrite /hyp_spinlock_t_invariant.
......@@ -218,21 +179,6 @@ Section proofs.
liInst Hevar2 next.
liInst Hevar0 next.
repeat liRStep; liShow.
iRename select (p at{struct_hyp_spinlock} _ _)%I into "Hnext".
iSplitL "Hnext".
{ iDestruct (ty_ref (t := next @ int u16)%I with "[] Hnext []") as "$" => //. }
iDestruct select (owner_frag _ _) as "$".
iDestruct select (ticket_range _ 0 _) as "$".
iDestruct select (ticket_range _ _ _) as "$".
iDestruct select (_ _)%I as "$".
iDestruct (ty_ref (t := uninit u16) with "[] Hi+1 []") as "$" => //.
{ iPureIntro. split => //. by apply Forall_forall. }
iRename select (local_ticket _)%I into "Hticket".
iDestruct (ty_ref (t := next @ int u16) with "[] Hticket []") as "$" => //.
iRename select (local_got_it ◁ₗ _)%I into "Hgot_it".
iDestruct (ty_aligned with "Hgot_it") as %?.
iDestruct (ty_deref with "Hgot_it") as (?) "[Hgot_it [% ->]]".
iDestruct (ty_ref (t := false @ boolean bool_it) with "[] Hgot_it []") as "$" => //.
+ liRStepUntil typed_if. do 2 liRStep; liShow.
* repeat liRStep; liShow.
iExists (Shr, place _); iSplitR; first by simpl.
......@@ -259,27 +205,13 @@ Section proofs.
iDestruct "Inv" as (owner next) "([%%]&Howner&Hnext&Hrest)".
destruct (decide (next = i)) as [<-|] .
** iRename select (_ ◁ₗ next @ int u16)%I into "Hnext".
iDestruct (ty_aligned with "Hnext") as %?.
iDestruct (ty_deref with "Hnext") as (?) "[Hnext Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iRename select (_ ◁ₗ (next + 1) @ int u16)%I into "Hnext+1".
iDestruct (ty_aligned with "Hnext+1") as %?.
iDestruct (ty_deref with "Hnext+1") as (?) "[Hnext+1 Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (_ ◁ᵥ (next + 1) @ int u16)%I as "Hv".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (local_ticket ◁ᵥ _)%I as "[_ Hticket]".
iDestruct (ty_aligned with "Hticket") as %?.
iDestruct (ty_deref with "Hticket") as (?) "[Hticket Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (p at{_} _ ◁ᵥ _)%I as "[_ ->]".
iApply (wp_cas_suc _ _ _ v2 v4 next next _ _ _ u16 _ _ with "Hnext Hticket") => //.
{ by rewrite val_to_of_loc. }
{ by rewrite val_to_of_loc. }
{ cbv. lia. }
iApply (wp_cas_suc_int with "Hnext Hticket [$]"). { cbv. lia. } done.
iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (true @ boolean bool_it))%I) => //.
iRename select (p at{struct_hyp_spinlock} _ _)%I into "Hnext".
iDestruct (ty_ref (t := (next + 1) @ int u16)%I with "[] Hnext []") as "Hnext" => //.
iRename select (p at{struct_hyp_spinlock} "next" ◁ₗ _)%I into "Hnext".
iDestruct "Hrest" as "(Hfrag&Hr1&Hr2&Hcases)".
iDestruct (split_first_ticket with "Hr2") as "[Hticket Hr2]".
{ split; last by lia. by transitivity (min_int u16). }
......@@ -290,44 +222,18 @@ Section proofs.
iSplitL => //. iPureIntro. lia. }
iModIntro.
repeat liRStep; liShow.
liInst Hevar0 next. iFrame.
iRename select (local_ticket _)%I into "Hlocal_ticket".
iRename select (local_next _)%I into "Hlocal_next".
iDestruct (ty_ref (t := next @ int u16) with "[] Hlocal_ticket []") as "$" => //.
iDestruct (ty_ref (t := uninit u16) with "[] Hlocal_next []") as "$" => //.
{ iPureIntro. split => //. by apply Forall_forall. }
** iRename select (_ ◁ₗ next @ int u16)%I into "Hnext".
iDestruct (ty_aligned with "Hnext") as %?.
iDestruct (ty_deref with "Hnext") as (?) "[Hnext Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iRename select (_ ◁ₗ (i + 1) @ int u16)%I into "Hi+1".
iDestruct (ty_aligned with "Hi+1") as %?.
iDestruct (ty_deref with "Hi+1") as (?) "[Hi+1 Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (_ ◁ᵥ (i + 1) @ int u16)%I as "Hv".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (local_ticket ◁ᵥ _)%I as "[_ Hticket]".
iDestruct (ty_aligned with "Hticket") as %?.
iDestruct (ty_deref with "Hticket") as (?) "[Hticket Hv]".
iDestruct (ty_size_eq with "Hv") as %?. iDestruct "Hv" as "%".
iDestruct select (p at{_} _ ◁ᵥ _)%I as "[_ ->]".
iApply (wp_cas_fail _ _ _ v2 v4 next i _ _ _ u16 _ _ with "Hnext Hticket") => //.
{ by rewrite val_to_of_loc. }
{ by rewrite val_to_of_loc. }
{ cbv. lia. }
iApply (wp_cas_fail_int with "Hnext Hticket [$]"). { cbv. lia. } done.
iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (false @ boolean bool_it))%I) => //.
iRename select (p at{struct_hyp_spinlock} _ _)%I into "Hnext".
iDestruct (ty_ref (t := next @ int u16)%I with "[] Hnext []") as "Hnext" => //.
iRename select (p at{struct_hyp_spinlock} _ ◁ₗ _)%I into "Hnext".
iMod ("Hclose_inv" with "[Howner Hnext Hrest]") as "_".
{ iNext. iExists owner, next. iFrame "Howner". iFrame "Hnext". iFrame "Hrest". done. }
iModIntro.
repeat liRStep; liShow.
liInst Hevar0 next.
iRename select (local_ticket _)%I into "Hlocal_ticket".
iRename select (local_next _)%I into "Hlocal_next".
iDestruct (ty_ref (t := next @ int u16) with "[] Hlocal_ticket []") as "$" => //.
iDestruct (ty_ref (t := uninit u16) with "[] Hlocal_next []") as "$" => //.
{ iPureIntro. split => //. by apply Forall_forall. }
- (* #4 Final loop: checking if we are the owner. *)
destruct s.
+ repeat liRStep; liShow.
......
......@@ -11,15 +11,13 @@ Section atomic_bool.
match β return _ with
| Own => b, l ◁ₗ b @ boolean it if b then PT else PF
| Shr => l `has_layout_loc` it
inv atomic_boolN ( b, l i2v (Z_of_bool b) it if b then PT else PF)
inv atomic_boolN ( b, l ◁ₗ b @ boolean it if b then PT else PF)
end;
|}%I.
Next Obligation.
iIntros "%it %PT %PF %l %E %HE (%b&Hb&Hown)".
iDestruct (ty_aligned with "Hb") as %?. iSplitR => //.
iApply inv_alloc. iNext. iExists b. iFrame.
iDestruct (ty_deref with "Hb") as "(%v&Hl&Hb)".
by iDestruct (boolean_own_val_eq with "Hb") as %<-.
Qed.
Global Program Instance movable_atomic_bool it PT PF : Movable (atomic_bool it PT PF) := {|
......@@ -82,12 +80,14 @@ Section programs.
- iDestruct "Hl" as (Hly) "#Hinv".
iInv "Hinv" as (b) "[>Hl Hif]" "Hclose".
iApply fupd_mask_intro. set_solver. iIntros "Hclose2".
iExists _, _, _, (t2mt (b @ boolean it)). iFrame.
rewrite /has_layout_val i2v_bool_length.
do 2 iSplitR => //=. iSplitR; first by iApply boolean_own_val_eq.
iDestruct (ty_aligned with "Hl") as %?.
iDestruct (ty_deref with "Hl") as (?) "[Hmt #Hv]".
iDestruct (ty_size_eq with "Hv") as %?.
iExists _, _, _, (t2mt (b @ boolean it)). iFrame "Hmt Hv".
iSplit; [done|]. iSplit; [done|].
iIntros "!# Hl". iDestruct ("HT" with "Hif") as "[Hif $]".
iMod "Hclose2" as "_".
iMod ("Hclose" with "[-]"). { iExists _. by iFrame. }
iMod ("Hclose" with "[-]"). { iExists b. iModIntro. iFrame. by iApply (ty_ref with "[] Hl Hv"). }
iModIntro. by iSplitR.
Qed.
Global Instance type_read_atomic_bool_inst l β it PT PF:
......@@ -105,7 +105,7 @@ Section programs.
typed_write_end true v ty l β (atomic_bool it PT PF) T.
Proof.
iIntros "[%bnew Hsub] Hl Hv".
iDestruct ("Hsub" with "Hv") as "(Hnew&->&Hif_new&HT)".
iDestruct ("Hsub" with "Hv") as "(#Hnew&->&Hif_new&HT)".
destruct β.
- iDestruct "Hl" as "[%bold [Hl Hif_old]]".
iApply fupd_mask_intro => //. iIntros "Hc".
......@@ -119,12 +119,14 @@ Section programs.
- iDestruct "Hl" as (?) "#Hinv".
iInv "Hinv" as (b) "[>Hmt Hif]" "Hc".
iApply fupd_mask_intro; first solve_ndisj.
iIntros "Hc2". iSplitL "Hmt".
{ iExists _; iFrame; iPureIntro; split => //. apply i2v_bool_length. }
iIntros "Hc2".
iDestruct (ty_aligned with "Hmt") as %?.
iDestruct (ty_deref with "Hmt") as (?) "[Hmt #Hv]".
iDestruct (ty_size_eq with "Hv") as %?.
iSplitL "Hmt". { iExists _; by iFrame. }
iIntros "!# Hl". iMod "Hc2".
iDestruct (boolean_own_val_eq with "Hnew") as %->.
iMod ("Hc" with "[Hif_new Hl]").
{ iModIntro. iExists bnew. iFrame. }
{ iModIntro. iExists bnew. iFrame. by iApply (@ty_ref with "[] Hl Hnew"). }
iModIntro. iExists _. iFrame. by iSplit.
Qed.
Global Instance type_write_atomic_bool_inst l β it PT PF v ty `{!Movable ty}:
......@@ -151,77 +153,39 @@ Section programs.
Proof.
iIntros "(%bexp&%bnew&Hsub) Hl Hlexp Hvnew".
iDestruct ("Hsub" with "Hlexp") as "[Hlexp Hsub]".
iDestruct ("Hsub" with "Hvnew") as "[Hvnew [% Hsub]]".
iDestruct ("Hsub" with "Hvnew") as "[#Hvnew [% Hsub]]".
iIntros (Φ) "HΦ".
(* TODO: don't unfold here *)
rewrite {1 2}/boolean/boolean_inner_type/int/int_inner_type/=.
iDestruct "Hlexp" as (ve Hve Hle) "He" => /=.
iDestruct "Hvnew" as %Hvnew.
destruct β.
- iDestruct "Hl" as (b) "[Hb Hif]".
(* TODO: don't unfold here *)
rewrite {1}/boolean/boolean_inner_type/int/int_inner_type/=.
iDestruct "Hb" as (vb Hvb Hlb) "Hb" => /=.
destruct (decide (b = bexp)); subst.
+ iApply (wp_cas_suc with "Hb He") => //.
{ by apply val_to_of_loc. }
{ by apply val_to_of_loc. }
{ by eapply val_to_Z_length. }
+ iApply (wp_cas_suc_bool with "Hb Hlexp") => //.
iIntros "!# Hb Hexp".
iDestruct "Hsub" as "[Hsub _]". iDestruct ("Hsub" with "Hif") as "[Hif HT]".
iApply "HΦ". 2: iApply ("HT" with "[Hb Hif]"). done.
* iExists bnew. iFrame "Hif". iExists _. by iFrame.
* iExists _. by iFrame.
+ iApply (wp_cas_fail with "Hb He") => //.
{ by apply val_to_of_loc. }
{ by apply val_to_of_loc. }
{ by eapply val_to_Z_length. }
{ by destruct b, bexp. }
iApply "HΦ". 2: iApply ("HT" with "[Hb Hif] Hexp"). done.
iExists bnew. by iFrame.
+ iApply (wp_cas_fail_bool with "Hb Hlexp") => //.
iIntros "!# Hb Hexp".
iDestruct "Hsub" as "[_ HT]".
iApply "HΦ". 2: iApply ("HT" with "[Hb Hif]"). done.
* iExists b. iFrame "Hif". iExists _. by iFrame.
* iExists _. iFrame. by destruct b, bexp.
* iExists b. iFrame.
* by destruct b, bexp.
- iDestruct "Hl" as (?) "#Hinv".
iInv "Hinv" as "Hb".
iDestruct "Hb" as (b) "[>Hmt Hif]".
destruct (decide (b = bexp)); subst.
+ iApply (wp_cas_suc with "Hmt He") => //.
{ by apply val_to_of_loc. }
{ by apply val_to_of_loc. }
{ apply val_to_of_int. rewrite /i2v.
have Hin: Z_of_bool bexp it by apply Z_of_bool_elem_of_int_type.
apply val_of_Z_is_some in Hin. destruct Hin as [? ->]. done. }
{ by eapply val_to_Z_length. }
+ iApply (wp_cas_suc_bool with "Hmt Hlexp") => //.
iIntros "!# Hb Hexp".
iDestruct "Hsub" as "[Hsub _]". iDestruct ("Hsub" with "Hif") as "[Hif HT]".
iModIntro. iSplitL "Hb Hif".
{ iExists bnew. iFrame.
assert (vnew = i2v (Z_of_bool bnew) it) as ->; last done.
rewrite /i2v.
have Hin: Z_of_bool bnew it by apply Z_of_bool_elem_of_int_type.
apply val_of_Z_is_some in Hin. destruct Hin as [? Heq]. rewrite Heq /=.
apply val_to_of_int in Heq. by eapply val_to_Z_Some_inj. }
iApply "HΦ". 2: iApply ("HT" with "[]"). done.
* by iSplit.
* iExists _. by iFrame.
+ iApply (wp_cas_fail with "Hmt He") => //.
{ by apply val_to_of_loc. }
{ by apply val_to_of_loc. }
{ apply val_to_of_int. rewrite /i2v.
have Hin: Z_of_bool b it by apply Z_of_bool_elem_of_int_type.
apply val_of_Z_is_some in Hin. destruct Hin as [? ->]. done. }
{ by eapply val_to_Z_length. }
{ by destruct b, bexp. }
iModIntro. iSplitL "Hb Hif". { iExists bnew. iFrame. }
iApply "HΦ". 2: iApply ("HT" with "[] Hexp"). done.
by iSplit.
+ iApply (wp_cas_fail_bool with "Hmt Hlexp") => //.
iIntros "!# Hb Hexp".
iDestruct "Hsub" as "[_ HT]".
iModIntro. iSplitL "Hb Hif". { by iExists b; iFrame; rewrite /i2v Hvnew. }
iApply "HΦ". 2: iApply ("HT" with "[]"). done.
* by iSplit.
* iExists _. iFrame. iSplit; last done. iPureIntro. rewrite /i2v.
have Hin: Z_of_bool b it by apply Z_of_bool_elem_of_int_type.
apply val_of_Z_is_some in Hin. destruct Hin as [? Heq]. rewrite Heq /=.
apply val_to_of_int in Heq. rewrite Heq. by destruct b, bexp.
* by destruct b, bexp.
Qed.
Global Instance type_cas_atomic_bool_inst (l : loc) β it PT PF (lexp : loc) Pexp vnew Pnew:
TypedCas (IntOp it) l (l ◁ₗ{β} (atomic_bool it PT PF))%I lexp Pexp vnew Pnew :=
......
......@@ -63,6 +63,10 @@ Section int.
iSplitR => //. iExists q, v. iFrame. iModIntro. eauto with iFrame.
Qed.
Global Instance int_timeless l z it:
Timeless (l ◁ₗ z @ int it)%I.
Proof. apply _. Qed.
End int.
(* Typeclasses Opaque int. *)
Notation "int< it >" := (int it) (only printing, format "'int<' it '>'") : printing_sugar.
......@@ -86,17 +90,12 @@ Section boolean.
Next Obligation. iIntros (???). done. Qed.
Lemma boolean_own_val_eq v b it:
(v ◁ᵥ b @ boolean it)%I v = i2v (Z_of_bool b) it%I.
Proof.
iSplit.
- iIntros "%Hv !%". rewrite /i2v.
have [v' Hv']: is_Some (val_of_Z (Z_of_bool b) it).
{ apply val_of_Z_is_some. apply elem_of_int_type_0_to_127.
destruct b => /=; lia. }
rewrite Hv'. simpl. apply val_to_of_int in Hv'.
by eapply val_to_Z_Some_inj.
- iIntros "-> !%". by rewrite i2v_bool_Some.
Qed.
(v ◁ᵥ b @ boolean it)%I val_to_Z v it = Some (Z_of_bool b)%I.
Proof. done. Qed.
Global Instance boolean_timeless l b it:
Timeless (l ◁ₗ b @ boolean it)%I.
Proof. apply _. Qed.
End boolean.
Notation "boolean< it >" := (boolean it) (only printing, format "'boolean<' it '>'") : printing_sugar.
......@@ -412,6 +411,31 @@ Section programs.
TypedUnOpVal v (n @ int it)%I NotIntOp (IntOp it) :=
λ T, i2p (type_not_int n it v T).
(* TODO: replace this with a typed_cas once it is refactored to take E as an argument. *)
Lemma wp_cas_suc_int it z1 z2 zd l1 l2 vd Φ E:
(bytes_per_int it bytes_per_addr)%nat
z1 = z2
l1 ◁ₗ z1 @ int it - l2 ◁ₗ z2 @ int it - vd ◁ᵥ zd @ int it -
(l1 ◁ₗ zd @ int it - l2 ◁ₗ z2 @ int it - Φ (val_of_bool true)) -
wp NotStuck E (CAS (IntOp it) (Val l1) (Val l2) (Val vd)) Φ.
Proof.
iIntros (? ->) "(%v1&%&%&Hl1) (%v2&%&%&Hl2) % HΦ/=".
iApply (wp_cas_suc with "Hl1 Hl2"); try done; try by [apply: val_to_of_loc]; try by [apply: val_to_Z_length].
iIntros "!# Hl1 Hl2". iApply ("HΦ" with "[Hl1] [Hl2]"); iExists _; by iFrame.
Qed.
Lemma wp_cas_fail_int it z1 z2 zd l1 l2 vd Φ E:
(bytes_per_int it bytes_per_addr)%nat
z1 z2
l1 ◁ₗ z1 @ int it - l2 ◁ₗ z2 @ int it - vd ◁ᵥ zd @ int it -
(l1 ◁ₗ z1 @ int it - l2 ◁ₗ z1 @ int it - Φ (val_of_bool false)) -
wp NotStuck E (CAS (IntOp it) (Val l1) (Val l2) (Val vd)) Φ.
Proof.
iIntros (? ?) "(%v1&%&%&Hl1) (%v2&%&%&Hl2) % HΦ/=".
iApply (wp_cas_fail with "Hl1 Hl2"); try done; try by [apply: val_to_of_loc]; try by [apply: val_to_Z_length].
iIntros "!# Hl1 Hl2". iApply ("HΦ" with "[Hl1] [Hl2]"); iExists _; by iFrame.
Qed.
(*** bool *)
Lemma type_val_bool' b:
(val_of_bool b) ◁ᵥ (b @ boolean bool_it).
......@@ -481,6 +505,27 @@ Section programs.
TypedUnOpVal v (b @ boolean it1)%I (CastOp (IntOp it2)) (IntOp it1) :=
λ T, i2p (type_cast_bool b it1 it2 v T).
(* TODO: replace this with a typed_cas once it is refactored to take E as an argument. *)
Lemma wp_cas_suc_bool it b1 b2 bd l1 l2 vd Φ E:
(bytes_per_int it bytes_per_addr)%nat
b1 = b2
l1 ◁ₗ b1 @ boolean it - l2 ◁ₗ b2 @ boolean it - vd ◁ᵥ bd @ boolean it -
(l1 ◁ₗ bd @ boolean it - l2 ◁ₗ b2 @ boolean it - Φ (val_of_bool true)) -
wp NotStuck E (CAS (IntOp it) (Val l1) (Val l2) (Val vd)) Φ.
Proof. iIntros (? ->) "Hl1 Hl2 Hv HΦ/=". iApply (wp_cas_suc_int with "Hl1 Hl2 Hv"); done. Qed.
Lemma wp_cas_fail_bool it b1 b2 bd l1 l2 vd Φ E:
(bytes_per_int it bytes_per_addr)%nat
b1 b2
l1 ◁ₗ b1 @ boolean it - l2 ◁ₗ b2 @ boolean it - vd ◁ᵥ bd @ boolean it -
(l1 ◁ₗ b1 @ boolean it - l2 ◁ₗ b1 @ boolean it - Φ (val_of_bool false)) -
wp NotStuck E (CAS (IntOp it) (Val l1) (Val l2) (Val vd)) Φ.
Proof.
iIntros (? ?) "Hl1 Hl2 Hv HΦ/=". iApply (wp_cas_fail_int with "Hl1 Hl2 Hv"); try done.
by destruct b1, b2.
Qed.
(*** int <-> bool *)
Lemma subsume_int_bool_place l β n b it T:
n = Z_of_bool b T -
......
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