Skip to content

GitLab

Commit 53e1539f authored by Michael Sammler's avatar Michael Sammler
Browse files

extracted atomic bool

parent 3d86bbbf
Hide whitespace changes
Inline Side-by-side
theories/examples/spinlock/spinlock_def.v
View file @ 53e1539f
......@@ -24,39 +24,10 @@ Section type.
Definition spinlock_token (γ : lock_id) (l : list string) : iProp Σ :=
∃ s : gset string, ⌜l ≡ₚ elements s⌝ ∗ own γ (● GSet s).
Program Definition spinlock (γ : lock_id) : type := {|
ty_own β l := (match β return _ with
| Own => ∃ b, l ◁ₗ struct struct_spinlock [b @ boolean u8] ∗ if b then True else spinlock_token γ []
| Shr => ⌜l at{struct_spinlock}ₗ "lock" `has_layout_loc` bool_it⌝ ∗
l ◁ₗ{Shr} struct struct_spinlock [ singleton_place (l at{struct_spinlock}ₗ "lock")] ∗
inv lockN (∃ b, l at{struct_spinlock}ₗ "lock" ↦ i2v (Z_of_bool b) u8 ∗
if b then True else spinlock_token γ [])
end)%I
|}.
Next Obligation.
iIntros (γ l E HE) => /=. rewrite /ty_own/=. iDestruct 1 as (b) "[[$ [% [Hs _]]] Hown]".
iDestruct (ty_aligned with "Hs") as %?. iSplitR => //. iSplitR => //.
iApply inv_alloc. iIntros "!#". iExists b. iFrame.
(* TODO: don't unfold here *)
rewrite /boolean/boolean_inner_type/int_inner_type.
iDestruct "Hs" as (v Hv ?) "Hv" => /=. rewrite /GetMemberLoc/= /val_of_bool/i2v Hv. iFrame.
Qed.
Global Program Instance movable_spinlock γ : Movable (spinlock γ) := {|
ty_layout := u8;
ty_own_val v := (∃ b, v ◁ᵥ struct struct_spinlock [b @ boolean u8] ∗ if b then True else spinlock_token γ [])%I;
|}.
Next Obligation. iIntros (γ l) "?". iPureIntro. by apply has_layout_loc_1. Qed.
Next Obligation. iIntros (γ v). iDestruct 1 as (b) "[Hs _]". by iDestruct (ty_size_eq with "Hs") as %?. Qed.
Next Obligation.
iIntros (γ l). iDestruct 1 as (b) "[Hs ?]". iDestruct (ty_deref with "Hs") as (v) "[? ?]".
eauto with iFrame.
Qed.
Next Obligation.
iIntros (γ l v ?) "Hl". iDestruct 1 as (b) "[Hs ?]". iDestruct (ty_ref with "[] Hl Hs") as "?" => //.
iExists _. iFrame.
Qed.
Definition spinlock (γ : lock_id) : type :=
struct struct_spinlock [atomic_bool bool_it True (spinlock_token γ [])].
Global Program Instance movable_spinlock γ : Movable (spinlock γ) := ltac:(apply: movable_struct).
Program Definition spinlocked_ex {A} (γ : lock_id) (n : string) (x : A) (ty : A → type) : type := {|
ty_own β l := (match β return _ with
......
theories/examples/spinlock/spinlock_proof.v
View file @ 53e1539f
From iris.algebra Require Import csum excl auth cmra_big_op.
From iris.algebra Require Import big_op gset frac agree.
From refinedc.typing Require Import typing.
From refinedc.examples.spinlock Require Import spinlock_def.
From refinedc.examples.spinlock Require Import spinlock_spec.
From refinedc.examples.spinlock Require Import spinlock_code.
From iris.algebra Require Import csum excl auth cmra_big_op.
From iris.algebra Require Import big_op gset frac agree.
Set Default Proof Using "Type".
Section type.
Context `{!typeG Σ} `{!lockG Σ}.
Typeclasses Transparent spinlock spinlocked_ex spinlock_token spinlocked_ex_token.
Lemma type_sl_init:
⊢ typed_function impl_sl_init type_of_sl_init.
Proof.
......@@ -17,13 +18,12 @@ Section type.
iApply fupd_typed_stmt.
iMod (own_alloc (● GSet ∅)) as (γ) "Hown". by apply auth_auth_valid.
iAssert (spinlock_token γ []) with "[Hown]" as "?". iExists _. by iFrame.
iModIntro.
repeat liRStep; liShow.
iIntros "?". rewrite /(ty_own (spinlock _))/=.
liInst Hevar γ.
repeat liRStep; liShow.
iSplitL => //. iExists _. by iFrame.
Unshelve. all: prepare_sideconditions; solve_goal.
Qed.
......@@ -35,63 +35,8 @@ Section type.
- repeat liRStep; liShow.
- repeat liRStep; liShow.
iApply typed_place_subsume'.
destruct β.
+ iDestruct 1 as (b) "[? ?]".
repeat liRStep; liShow.
iIntros "H1 H2 H3" (Φ) "HΦ".
iDestruct "H1" as (_) "H1".
iDestruct "H2" as (_) "H2".
(* TODO: don't unfold here *)
rewrite {2 3}/boolean/boolean_inner_type/int_inner_type/=.
iDestruct "H1" as (vo Hvo Hlo) "Ho" => /=. iDestruct "H2" as (ve Hve Hle) "He" => /=.
destruct b.
* iApply (wp_cas_fail with "Ho He"); try by [apply val_to_of_loc]; try by [apply val_to_of_int].
all: try by rewrite // /loc_size/loc_size_log/it_length/it_size/=; lia.
iIntros "!# Hvo Hve".
iApply ("HΦ" $! _ (t2mt (Z_of_bool false @ int bool_it))%I with "[]") => //.
iAssert (p at{struct_spinlock}ₗ "lock" ◁ₗ true @ boolean u8)%I with "[Hvo]" as "Hp". by iExists _; iFrame.
iAssert (vexpected ◁ₗ true @ boolean u8)%I with "[Hve]" as "He". by iExists _; iFrame.
repeat liRStep; liShow.
iIntros "?". rewrite /(ty_own (spinlock _))/=.
repeat liRStep; liShow.
* iApply (wp_cas_suc with "Ho He"); try by [apply val_to_of_loc]; try by [apply val_to_of_int].
all: try by rewrite // /loc_size/loc_size_log/it_length/it_size/=; lia.
iIntros "!# Hvo Hve".
iApply ("HΦ" $! _ (t2mt (Z_of_bool true @ int bool_it))%I with "[]") => //.
iAssert (p at{struct_spinlock}ₗ "lock" ◁ₗ true @ boolean u8)%I with "[Hvo]" as "Hp". by iExists _; iFrame.
iAssert (vexpected ◁ₗ false @ boolean u8)%I with "[Hve]" as "He". by iExists _; iFrame.
repeat liRStep; liShow.
iIntros "?". rewrite /(ty_own (spinlock _))/=.
repeat liRStep; liShow.
+ iIntros "[% [#? #Hinv]]".
repeat liRStep; liShow.
iIntros "H1 H2 H3" (Φ) "HΦ". iDestruct "H2" as (_) "H2".
(* TODO: don't unfold here *)
rewrite {2}/boolean/boolean_inner_type/int_inner_type/=. iDestruct "H2" as (ve Hve Hle) "He" => /=.
iApply (@wp_atomic).
iMod (inv_acc with "Hinv") as "[Hb Hc]" => //. iModIntro.
iDestruct "Hb" as (b) "[>Hmt Hown]".
destruct b.
* iApply (wp_cas_fail with "Hmt He"); try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply val_to_int_bool].
all: try by rewrite // /loc_size/loc_size_log/it_length/it_size/=; lia.
iIntros "!# Hl He".
iMod ("Hc" with "[Hl]") as "_"; iModIntro. by iExists _; iFrame.
iApply ("HΦ" $! _ (t2mt (Z_of_bool false @ int bool_it))%I with "[]") => //.
iAssert (vexpected ◁ₗ true @ boolean u8)%I with "[He]" as "He". by iExists _; iFrame.
repeat liRStep; liShow.
iIntros "?". rewrite /(ty_own (spinlock _))/=.
repeat liRStep; liShow.
* iApply (wp_cas_suc with "Hmt He"); try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply val_to_int_bool].
all: try by rewrite // /loc_size/loc_size_log/it_length/it_size/=; lia.
iIntros "!# Hl He".
iMod ("Hc" with "[Hl]") as "_"; iModIntro. rewrite/val_of_bool. by iExists true => /=; iFrame.
iApply ("HΦ" $! _ (t2mt (Z_of_bool true @ int bool_it))%I with "[]") => //.
iAssert (vexpected ◁ₗ false @ boolean u8)%I with "[He]" as "He". by iExists _; iFrame.
repeat liRStep; liShow.
iIntros "?". rewrite /(ty_own (spinlock _))/=.
repeat liRStep; liShow.
Unshelve. all: prepare_sideconditions; solve_goal.
Unshelve. all: prepare_sideconditions; try solve_goal.
rewrite /it_length/=. have ->: loc_size = 8%nat; solve_goal.
Qed.
Lemma type_sl_unlock:
......@@ -100,27 +45,7 @@ Section type.
start_function "sl_unlock" ([[p γ] β]) => vl. split_blocks (∅ : gmap block_id (iProp Σ)) (∅ : gmap block_id (iProp Σ)).
repeat liRStep; liShow.
iApply typed_place_subsume'.
destruct β.
- iDestruct 1 as (b) "[? ?]".
repeat liRStep; liShow.
iIntros "?". rewrite /(ty_own (spinlock _))/=.
repeat liRStep; liShow.
- iIntros "[% [#? #Hinv]]".
repeat liRStep; liShow.
iExists (_, singleton_place _)%I => /=. iSplit => //.
iIntros "_" => /=.
iMod (inv_acc with "Hinv") as "[Hl Hc]" => //.
iDestruct "Hl" as (b) "[>Hb Hown]".
iMod (fupd_intro_mask') as "Hmask". 2: iModIntro. solve_ndisj.
iSplitL "Hb". by iExists _; iFrame; iPureIntro; destruct b.
iIntros "!# Hp _".
iMod "Hmask" as "_". iMod ("Hc" with "[-]"). rewrite /val_of_bool. by iModIntro; iExists false; iFrame.
iIntros "!#". iExists (singleton_place (p at{struct_spinlock}ₗ "lock"))%I. iSplit => //.
repeat liRStep; liShow.
iIntros "?". rewrite /(ty_own (spinlock _))/=.
repeat liRStep; liShow.
Unshelve. all: prepare_sideconditions; solve_goal.
Unshelve. all: prepare_sideconditions; solve_goal.
Qed.
End type.
theories/lang/base.v
View file @ 53e1539f
......@@ -74,6 +74,15 @@ Existing Class TCOneIsSome.
Global Existing Instance tc_one_is_some_left.
Global Existing Instance tc_one_is_some_right.
Inductive TCOneIsSome3 {A} : option A → option A → option A → Prop :=
| tc_one_is_some3_left n1 o2 o3 : TCOneIsSome3 (Some n1) o2 o3
| tc_one_is_some3_middle o1 n2 o3 : TCOneIsSome3 o1 (Some n2) o3
| tc_one_is_some3_right o1 o2 n3 : TCOneIsSome3 o1 o2 (Some n3).
Existing Class TCOneIsSome3.
Global Existing Instance tc_one_is_some3_left.
Global Existing Instance tc_one_is_some3_middle.
Global Existing Instance tc_one_is_some3_right.
Lemma take_elem_of {A} (x : A) n l:
x ∈ take n l ↔ ∃ i, (i < n)%nat ∧ l !! i = Some x.
Proof.
......
theories/typing/atomic_bool.v 0 → 100644
View file @ 53e1539f
From refinedc.typing Require Export type.
From refinedc.typing Require Import programs int.
Set Default Proof Using "Type".
Definition atomic_boolN : namespace := nroot.@"atomic_boolN".
Section atomic_bool.
Context `{!typeG Σ}.
Program Definition atomic_bool (it : int_type) (PT PF : iProp Σ) : type := {|
ty_own β l := (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)
end)%I
|}.
Next Obligation.
iIntros (PT PF l E HE) => /=. iDestruct 1 as (b) "[Hb Hown]".
iDestruct (ty_aligned with "Hb") as %?. iSplitR => //.
iApply inv_alloc. iIntros "!#". iExists b. iFrame.
iDestruct (ty_deref with "Hb") as (v) "[Hl Hb]".
(* TODO: don't unfold here *)
rewrite /i2v. by iDestruct "Hb" as %->.
Qed.
Global Program Instance movable_atomic_bool it PT PF : Movable (atomic_bool it PT PF) := {|
ty_layout := it_layout it;
ty_own_val v := ∃ b, v ◁ᵥ b @ boolean it ∗ if b then PT else PF;
|}%I.
Next Obligation. iIntros (it PT PF l). iDestruct 1 as (?) "[Hb _]". by iApply (ty_aligned with "Hb"). Qed.
Next Obligation. iIntros (it PT PF v). iDestruct 1 as (?) "[Hb _]". by iApply (ty_size_eq with "Hb"). Qed.
Next Obligation.
iIntros (it PT PF v). iDestruct 1 as (?) "[Hb ?]".
iDestruct (ty_deref with "Hb") as (?) "[? ?]". eauto with iFrame.
Qed.
Next Obligation.
iIntros (it PT PF l v ?) "Hl". iDestruct 1 as (?) "[Hb ?]".
iDestruct (ty_ref with "[] Hl Hb") as "?" => //. iExists _. iFrame.
Qed.
End atomic_bool.
Section programs.
Context `{!typeG Σ}.
Lemma subsume_atomic_bool_own_int l n it PT PF T:
(∃ b, subsume (l ◁ₗ n @ int it) (l ◁ₗ b @ boolean it) ((if b then PT else PF) ∗ T)) -∗
subsume (l ◁ₗ n @ int it) (l ◁ₗ atomic_bool it PT PF) T.
Proof.
iDestruct 1 as (b) "Hsub". iIntros "Hl".
iDestruct ("Hsub" with "Hl") as "[? [? $]]".
iExists _. by iFrame.
Qed.
Global Instance subsume_atomic_bool_own_int_inst l n it PT PF:
Subsume (l ◁ₗ n @ int it)%I (l ◁ₗ atomic_bool it PT PF) :=
λ T, i2p (subsume_atomic_bool_own_int l n it PT PF T).
Lemma i2v_bool_length b it:
length (i2v (Z_of_bool b) it) = it_length it.
Proof. by have /val_of_int_length -> := val_of_int_bool b it. Qed.
Lemma i2v_bool_Some b it:
val_to_int (i2v (Z_of_bool b) it) it = Some (Z_of_bool b).
Proof. apply val_to_of_int. apply val_of_int_bool. Qed.
Lemma type_write_atomic_bool l β it PT PF v ty `{!Movable ty} T:
(∃ b, subsume (v ◁ᵥ ty) (v ◁ᵥ b @ boolean it) (⌜ty.(ty_layout) = it⌝ ∗ (if b then PT else PF) ∗ T (atomic_bool it PT PF))) -∗
typed_write_end true v ty l β (atomic_bool it PT PF) T.
Proof.
iIntros "HT Hl Hv". iDestruct "HT" as (bnew) "Hsub".
iDestruct ("Hsub" with "Hv") as "(Hnew&->&Hif'&HT)".
destruct β.
- iDestruct "Hl" as (bold) "[Hl Hif]".
iMod (fupd_intro_mask' _ ∅) as "Hc" => //. iModIntro.
iDestruct (ty_aligned with "Hl") as %?.
iDestruct (ty_deref with "Hl") as (vb) "[Hmt Hold]".
iDestruct (ty_size_eq with "Hold") as %?.
iSplitL "Hmt". by iExists _; iFrame.
iIntros "!# Hl". iMod "Hc". iModIntro.
iExists _. iFrame. iExists bnew. iFrame.
iApply (@ty_ref with "[] Hl") => //. done.
- iDestruct "Hl" as (?) "#Hinv".
iInv "Hinv" as (b) "[>Hmt Hif]" "Hc".
iMod (fupd_intro_mask' _ ∅) as "Hc2". solve_ndisj. iModIntro.
iSplitL "Hmt".
{ iExists _; iFrame; iPureIntro; split => //. apply i2v_bool_length. }
iIntros "!# Hl". iMod "Hc2".
iMod ("Hc" with "[Hif' Hl Hnew]").
{ iModIntro. iExists bnew. iFrame. rewrite /i2v. by iDestruct "Hnew" as %->. }
iModIntro. iExists _. iFrame. by iSplit.
Qed.
Global Instance type_write_atomic_bool_inst l β it PT PF v ty `{!Movable ty}:
TypedWriteEnd true v ty l β (atomic_bool it PT PF) | 10 :=
λ T, i2p (type_write_atomic_bool l β it PT PF v ty T).
Lemma type_cas_atomic_bool (l : loc) β it PT PF lexp Pexp vnew Pnew T:
(∃ bexp bnew, subsume Pexp (lexp ◁ₗ bexp @ boolean it) (
subsume Pnew (vnew ◁ᵥ bnew @ boolean it) ( ⌜it_length it ≤ loc_size⌝%nat ∗ (
((if bexp then PT else PF) -∗ (if bnew then PT else PF) ∗ (
l ◁ₗ{β} atomic_bool it PT PF -∗ lexp ◁ₗ bexp @ boolean it -∗
T (val_of_bool true) (t2mt (true @ boolean bool_it)))) ∧
(l ◁ₗ{β} atomic_bool it PT PF -∗ lexp ◁ₗ negb bexp @ boolean it -∗
T (val_of_bool false) (t2mt (false @ boolean bool_it)))
)))) -∗
typed_cas (IntOp it) l (l ◁ₗ{β} (atomic_bool it PT PF))%I lexp Pexp vnew Pnew T.
Proof.
iDestruct 1 as (bexp bnew) "Hsub". iIntros "Hl Hlexp Hvnew".
iDestruct ("Hsub" with "Hlexp") as "[Hlexp Hsub]".
iDestruct ("Hsub" with "Hvnew") as "[Hvnew [% Hsub]]".
iIntros (Φ) "HΦ".
(* TODO: don't unfold here *)
rewrite {1 2}/boolean/boolean_inner_type/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_inner_type/=.
iDestruct "Hb" as (vb Hvb Hlb) "Hb" => /=.
destruct (decide (b = bexp)); subst.
+ iApply (wp_cas_suc with "Hb He") => //; try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply: val_of_int_length].
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") => //; try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply: val_of_int_length]; try by [destruct b,bexp].
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.
- iDestruct "Hl" as (?) "#Hinv".
iApply (@wp_atomic).
iMod (inv_acc with "Hinv") as "[Hb Hc]" => //. iModIntro.
iDestruct "Hb" as (b) "[>Hmt Hif]".
destruct (decide (b = bexp)); subst.
+ iApply (wp_cas_suc with "Hmt He") => //; try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply: val_of_int_length]; try by [apply i2v_bool_Some].
iIntros "!# Hb Hexp".
iDestruct "Hsub" as "[Hsub _]". iDestruct ("Hsub" with "Hif") as "[Hif HT]".
iMod ("Hc" with "[Hb Hif]") as "_"; iModIntro. by iExists bnew; iFrame; rewrite /i2v Hvnew.
iApply "HΦ". 2: iApply ("HT" with "[]"). done.
* by iSplit.
* iExists _. by iFrame.
+ iApply (wp_cas_fail with "Hmt He") => //; try by [apply val_to_of_loc]; try by [apply val_to_of_int]; try by [apply i2v_bool_Some]; try by [apply: val_of_int_length]; try by [destruct b,bexp].
iIntros "!# Hb Hexp".
iDestruct "Hsub" as "[_ HT]".
iMod ("Hc" with "[Hb Hif]") as "_"; iModIntro. by iExists b; iFrame; rewrite /i2v Hvnew.
iApply "HΦ". 2: iApply ("HT" with "[]"). done.
* by iSplit.
* iExists _. iFrame. rewrite val_of_int_bool. 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 :=
λ T, i2p (type_cas_atomic_bool l β it PT PF lexp Pexp vnew Pnew T).
End programs.
Typeclasses Opaque atomic_bool.
theories/typing/automation.v
View file @ 53e1539f
......@@ -48,6 +48,7 @@ Ltac convert_to_i2p_tac P ::=
| typed_read_end ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _) _).(i2p_proof))
| typed_write_end ?a ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T => uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _) _).(i2p_proof))
| typed_addr_of_end ?l ?β ?ty ?T => uconstr:(((_ : TypedAddrOfEnd _ _ _) _).(i2p_proof))
| typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T => uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _).(i2p_proof))
| typed_annot_expr ?n ?a ?v ?ty ?T => uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) .(i2p_proof))
| typed_annot_stmt ?a ?l ?β ?ty ?T => uconstr:(((_ : TypedAnnotStmt _ _ _ _) _).(i2p_proof))
end.
......
theories/typing/int.v
View file @ 53e1539f
......@@ -80,6 +80,7 @@ End bool.
Section programs.
Context `{!typeG Σ}.
(*** int *)
Lemma type_val_int n it T:
(⌜it_in_range it n⌝ ∗ T (t2mt (n @ (int it)))) -∗ typed_value (i2v n it) T.
Proof. iDestruct 1 as ([v Hv]%val_of_int_is_some) "HT". iExists _. iFrame. by rewrite /i2v Hv. Qed.
......@@ -264,6 +265,7 @@ Section programs.
TypedUnOpVal v (n @ int it1)%I (CastOp (IntOp it2)) (IntOp it1) :=
λ T, i2p (type_cast_int n it1 it2 v T).
(*** bool *)
Lemma type_val_bool b T:
(T (t2mt (b @ boolean bool_it))) -∗ typed_value (val_of_bool b) T.
Proof. iIntros "HT". iExists _. iFrame. by destruct b. Qed.
......@@ -327,6 +329,7 @@ Section programs.
TypedUnOpVal v (b @ boolean it1)%I (CastOp (IntOp it2)) (IntOp it1) :=
λ T, i2p (type_cast_bool b it1 it2 v T).
(*** int <-> bool *)
Lemma subsume_int_bool_place l β n b it T:
⌜n = Z_of_bool b⌝ ∗ T -∗
subsume (l ◁ₗ{β} n @ int it) (l ◁ₗ{β} b @ boolean it) T.
......@@ -343,6 +346,23 @@ Section programs.
SubsumeVal v (n @ int it) (b @ boolean it) :=
λ T, i2p (subsume_int_bool_val v n b it T).
Lemma type_binop_bool_int it1 it2 it3 it4 v1 b1 v2 n2 T op:
typed_bin_op v1 (v1 ◁ᵥ (Z_of_bool b1) @ int it1) v2 (v2 ◁ᵥ n2 @ int it2) op (IntOp it3) (IntOp it4) T -∗
typed_bin_op v1 (v1 ◁ᵥ b1 @ boolean it1) v2 (v2 ◁ᵥ n2 @ int it2) op (IntOp it3) (IntOp it4) T.
Proof. iIntros "HT". iApply "HT". Qed.
Global Instance type_binop_bool_int_inst it1 it2 it3 it4 v1 b1 v2 n2 op:
TypedBinOp v1 (v1 ◁ᵥ b1 @ boolean it1)%I v2 (v2 ◁ᵥ n2 @ int it2)%I op (IntOp it3) (IntOp it4) :=
λ T, i2p (type_binop_bool_int it1 it2 it3 it4 v1 b1 v2 n2 T op).
Lemma type_binop_int_bool it1 it2 it3 it4 v1 b1 v2 n2 T op:
typed_bin_op v1 (v1 ◁ᵥ n2 @ int it2) v2 (v2 ◁ᵥ (Z_of_bool b1) @ int it1) op (IntOp it3) (IntOp it4) T -∗
typed_bin_op v1 (v1 ◁ᵥ n2 @ int it2) v2 (v2 ◁ᵥ b1 @ boolean it1) op (IntOp it3) (IntOp it4) T.
Proof. iIntros "HT". iApply "HT". Qed.
Global Instance type_binop_int_bool_inst it1 it2 it3 it4 v1 b1 v2 n2 op:
TypedBinOp v1 (v1 ◁ᵥ n2 @ int it2)%I v2 (v2 ◁ᵥ b1 @ boolean it1)%I op (IntOp it3) (IntOp it4) :=
λ T, i2p (type_binop_int_bool it1 it2 it3 it4 v1 b1 v2 n2 T op).
End programs.
Typeclasses Opaque int_inner_type boolean_inner_type.
......
theories/typing/programs.v
View file @ 53e1539f
......@@ -122,15 +122,16 @@ Section judgements.
Class TypedUnOpVal (v : val) (ty : type) `{!Movable ty} (o : un_op) (ot : op_type) : Type :=
typed_un_op_val :> TypedUnOp v (v ◁ᵥ ty) o ot.
(* No corresponding typeclass as this should not be necessary often *)
Definition typed_cas (ot : op_type) (v1 : val) (P1 : iProp Σ) (v2 : val) (P2 : iProp Σ) (v3 : val) (P3 : iProp Σ) (T : val → mtype → iProp Σ) : iProp Σ :=
(P1 -∗ P2 -∗ P3 -∗ typed_val_expr (CAS ot v1 v2 v3) T).
Class TypedCas (ot : op_type) (v1 : val) (P1 : iProp Σ) (v2 : val) (P2 : iProp Σ) (v3 : val) (P3 : iProp Σ) : Type :=
typed_cas_proof T : iProp_to_Prop (typed_cas ot v1 P1 v2 P2 v3 P3 T).
(*** places *)
Definition typed_write (atomic : bool) (e : expr) (v : val) (ty : type) `{!Movable ty} (T : iProp Σ) : iProp Σ :=
let E := if atomic then ∅ else ⊤ in
(∀ Φ,
(∀ (l : loc), (|={⊤, E}=> l↦|ty.(ty_layout)| ∗ ▷ (l ↦ v -∗ v ◁ᵥ ty ={E, ⊤}=∗ T)) -∗ Φ (val_of_loc l)) -∗
(∀ (l : loc), (v ◁ᵥ ty ={⊤, E}=∗ l↦|ty.(ty_layout)| ∗ ▷ (l ↦ v ={E, ⊤}=∗ T)) -∗ Φ (val_of_loc l)) -∗
WP e {{ Φ }}).
Definition typed_read (e : expr) (ly : layout) (T : val → mtype → iProp Σ) : iProp Σ :=
......@@ -151,7 +152,7 @@ Section judgements.
Definition typed_write_end (atomic : bool) (v1 : val) (ty1 : type) `{!Movable ty1} (l2 : loc) (β2 : own_state) (ty2 : type) (T : type → iProp Σ) : iProp Σ :=
let E := if atomic then ∅ else ⊤ in
l2 ◁ₗ{β2} ty2 ={⊤, E}=∗ l2↦|ty1.(ty_layout)| ∗ ▷ (l2↦v1 -∗ v1 ◁ᵥ ty1 ={E, ⊤}=∗ ∃ ty3, l2 ◁ₗ{β2} ty3 ∗ T ty3).
l2 ◁ₗ{β2} ty2 -∗ v1 ◁ᵥ ty1 ={⊤, E}=∗ l2↦|ty1.(ty_layout)| ∗ ▷ (l2↦v1 ={E, ⊤}=∗ ∃ ty3, l2 ◁ₗ{β2} ty3 ∗ T ty3).
Class TypedWriteEnd (atomic : bool) (v1 : val) (ty1 : type) `{!Movable ty1} (l2 : loc) (β2 : own_state) (ty2 : type) : Type :=
typed_write_end_proof T : iProp_to_Prop (typed_write_end atomic v1 ty1 l2 β2 ty2 T).
......@@ -537,6 +538,30 @@ Section typing.
TypedUnOp v P op ot | 1000 :=
λ T, i2p (typed_unop_simplify v P T n ot op).
Lemma typed_cas_simplify v1 P1 v2 P2 v3 P3 T ot o1 o2 o3 {SH1 : SimplifyHyp P1 o1} {SH2 : SimplifyHyp P2 o2} {SH3 : SimplifyHyp P3 o3}:
let G1 := (SH1 (find_in_context (FindValP v1) (λ P, typed_cas ot v1 P v2 P2 v3 P3 T))).(i2p_P) in
let G2 := (SH2 (find_in_context (FindValP v2) (λ P, typed_cas ot v1 P1 v2 P v3 P3 T))).(i2p_P) in
let G3 := (SH3 (find_in_context (FindValP v3) (λ P, typed_cas ot v1 P1 v2 P2 v3 P T))).(i2p_P) in
let min o1 o2 :=
match o1.1, o2.1 with
| Some n1, Some n2 => if (n2 ?= n1)%N is Lt then o2 else o1
| Some n1, _ => o1
| _, _ => o2
end in
let G := (min (o1, G1) (min (o2, G2) (o3, G3))).2 in
G -∗ typed_cas ot v1 P1 v2 P2 v3 P3 T.
Proof.
iIntros "Hs Hv1 Hv2 Hv3".
destruct o1 as [n1|], o2 as [n2|], o3 as [n3|] => //=; repeat case_match => /=.
all: try iDestruct (i2p_proof with "Hs Hv1") as (P) "[Hv Hsub]".
all: try iDestruct (i2p_proof with "Hs Hv2") as (P) "[Hv Hsub]".
all: try iDestruct (i2p_proof with "Hs Hv3") as (P) "[Hv Hsub]".
all: by simpl in *; iApply ("Hsub" with "[$] [$]").
Qed.
Global Instance typed_cas_simplify_inst v1 P1 v2 P2 v3 P3 ot o1 o2 o3 {SH1 : SimplifyHyp P1 o1} {SH2 : SimplifyHyp P2 o2} {SH3 : SimplifyHyp P3 o3} `{!TCOneIsSome3 o1 o2 o3} :
TypedCas ot v1 P1 v2 P2 v3 P3 | 1000 :=
λ T, i2p (typed_cas_simplify v1 P1 v2 P2 v3 P3 T ot o1 o2 o3).
Lemma typed_annot_stmt_simplify A (a : A) l β ty T n {SH : SimplifyHyp (l ◁ₗ{β} ty) (Some n)}:
(SH (find_in_context (FindLoc l) (λ '(β1, ty1),
typed_annot_stmt a l β1 ty1 T))).(i2p_P) -∗
......@@ -582,8 +607,8 @@ Section typing.
wps_bind. iApply "He1". iIntros (l) "HT".
iDestruct (ty_size_eq with "Hv") as %?.
iApply wps_assign; rewrite ?val_to_of_loc //. destruct o; naive_solver.
iMod "HT" as "[$ HT]". destruct o; iIntros "!# !# Hl".
all: by iApply ("HT" with "Hl Hv").
iMod ("HT" with "Hv") as "[$ HT]". destruct o; iIntros "!# !# Hl".
all: by iApply ("HT" with "Hl").
Qed.
Lemma type_if {B} Q e s1 s2 fn ls (fr : B → _):
......@@ -817,9 +842,9 @@ Section typing.
iIntros (HT') "HT'". iIntros (Φ) "HΦ".
iApply (HT' with "HT'"). iIntros (K l). iDestruct 1 as ([β1 ty1]) "[Hl HK]".
iApply ("HK" with "Hl"). iIntros (l2 β2 ty2 typ R) "Hl' Hc He".
iApply "HΦ". iMod ("He" with "Hl'") as "[$ Hc2]". iModIntro.
iIntros "!# Hl Hv".
iMod ("Hc2" with "Hl Hv") as (ty3) "[Hl HT]".
iApply "HΦ". iIntros "Hv". iMod ("He" with "Hl' Hv") as "[$ Hc2]". iModIntro.
iIntros "!# Hl".
iMod ("Hc2" with "Hl") as (ty3) "[Hl HT]".
iMod ("Hc" with "Hl") as "[? ?]". by iApply ("HT" with "[$]").
Qed.
......@@ -829,13 +854,13 @@ Section typing.
⌜ty2.(ty_layout) = ty.(ty_layout)⌝ ∗ (v ◁ᵥ ty -∗ T ty) -∗
typed_write_end a v ty l2 Own ty2 T.
Proof.
iDestruct 1 as (Heq) "HT". iIntros "Hl".
iDestruct 1 as (Heq) "HT". iIntros "Hl #Hv".
iDestruct (ty_aligned with "Hl") as %?.
iDestruct (ty_deref with "Hl") as (v') "[Hl Hv']".
iDestruct (ty_size_eq with "Hv'") as %?.
iMod (fupd_intro_mask' _ (if a then ∅ else ⊤)) as "Hmask" => //. iModIntro.
iSplitL "Hl". by iExists _; iFrame; rewrite -Heq.
iIntros "!# Hl #Hv". iMod "Hmask". iModIntro.
iIntros "!# Hl". iMod "Hmask". iModIntro.
iDestruct (ty_size_eq with "Hv") as %?.
iExists _. iDestruct ("HT" with "Hv") as "$".
iApply (ty_ref with "[] Hl Hv"). by rewrite -Heq.
......