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

Misc big op tweaks.

parent 02924947
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/typing/int.v
+ 3
− 6
View file @ 3e9074b9
...@@ -39,8 +39,7 @@ Section typing. ...@@ -39,8 +39,7 @@ Section typing.
Lemma type_plus_instr E L p1 p2 : Lemma type_plus_instr E L p1 p2 :
typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int. typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
Proof. Proof.
iIntros (tid) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton. iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
iIntros "[Hp1 Hp2]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done. wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done. wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //. wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
...@@ -56,8 +55,7 @@ Section typing. ...@@ -56,8 +55,7 @@ Section typing.
Lemma type_minus_instr E L p1 p2 : Lemma type_minus_instr E L p1 p2 :
typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int. typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
Proof. Proof.
iIntros (tid) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton. iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
iIntros "[Hp1 Hp2]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done. wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done. wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //. wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
...@@ -73,8 +71,7 @@ Section typing. ...@@ -73,8 +71,7 @@ Section typing.
Lemma type_le_instr E L p1 p2 : Lemma type_le_instr E L p1 p2 :
typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool. typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
Proof. Proof.
iIntros (tid) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton. iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
iIntros "[Hp1 Hp2]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done. wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done. wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op; intros _; by rewrite tctx_interp_singleton tctx_hasty_val' //. wp_op; intros _; by rewrite tctx_interp_singleton tctx_hasty_val' //.
......
theories/typing/lib/spawn.v
+ 2
− 3
View file @ 3e9074b9
...@@ -81,9 +81,8 @@ Section spawn. ...@@ -81,9 +81,8 @@ Section spawn.
iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _]%TC) iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _]%TC)
(λ j, [j ◁ join_handle retty]%TC)); try solve_typing; [|]. (λ j, [j ◁ join_handle retty]%TC)); try solve_typing; [|].
{ (* The core of the proof: showing that spawn is safe. *) { (* The core of the proof: showing that spawn is safe. *)
iIntros (tid) "#LFT #HE $ $". iIntros (tid) "#LFT #HE $ $ [Hf' [Henv _]]".
rewrite tctx_interp_cons tctx_interp_singleton. iApply (spawn_spec _ (join_inv tid retty) with "[-]");
iIntros "[Hf' Henv]". iApply (spawn_spec _ (join_inv tid retty) with "[-]");
first solve_to_val; last first; last simpl_subst. first solve_to_val; last first; last simpl_subst.
{ iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val. { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
iIntros "?". iExists retty. iFrame. iApply type_incl_refl. } iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
......
theories/typing/programs.v
+ 3
− 5
View file @ 3e9074b9
...@@ -99,8 +99,7 @@ Section typing_rules. ...@@ -99,8 +99,7 @@ Section typing_rules.
typed_body ((κ1 ⊑ κ2) :: (κ2 ⊑ κ1) :: E) L C T e → typed_body ((κ1 ⊑ κ2) :: (κ2 ⊑ κ1) :: E) L C T e →
typed_body E ((κ1 ⊑ [κ2]%list) :: L) C T e. typed_body E ((κ1 ⊑ [κ2]%list) :: L) C T e.
Proof. Proof.
iIntros (He tid) "#LFT #HE Htl HL HC HT". iIntros (He tid) "#LFT #HE Htl [Hκ HL] HC HT".
rewrite /llctx_interp big_sepL_cons. iDestruct "HL" as "[Hκ HL]".
iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]". iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
iApply (He with "LFT [Hκ1 Hκ2 HE] Htl HL HC HT"). iApply (He with "LFT [Hκ1 Hκ2 HE] Htl HL HC HT").
rewrite /elctx_interp /=. by iFrame. rewrite /elctx_interp /=. by iFrame.
...@@ -163,8 +162,7 @@ Section typing_rules. ...@@ -163,8 +162,7 @@ Section typing_rules.
Closed [] e → UnblockTctx κ T1 T2 → Closed [] e → UnblockTctx κ T1 T2 →
typed_body E L C T2 e -∗ typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e). typed_body E L C T2 e -∗ typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
Proof. Proof.
iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl". iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
rewrite /llctx_interp big_sepL_cons. iIntros "[Hκ HL] HC HT".
iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)". iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft. iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
iApply (wp_mask_mono (↑lftN)); first done. iApply (wp_mask_mono (↑lftN)); first done.
...@@ -176,7 +174,7 @@ Section typing_rules. ...@@ -176,7 +174,7 @@ Section typing_rules.
Lemma type_path_instr {E L} p ty : Lemma type_path_instr {E L} p ty :
typed_instruction_ty E L [p ◁ ty] p ty. typed_instruction_ty E L [p ◁ ty] p ty.
Proof. Proof.
iIntros (?) "_ _ $$ ?". rewrite tctx_interp_singleton. iIntros (?) "_ _ $$ [? _]".
iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv". iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv".
rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val. rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val.
Qed. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment