Commit f73cd1e9 authored by Dan Frumin's avatar Dan Frumin

Do some cleanup

parent 168ad45e
......@@ -223,6 +223,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
End R.
Ltac solve_to_val :=
rewrite /IntoVal;
try match goal with
| |- context E [language.to_val ?e] =>
let X := context E [to_val e] in change X
......@@ -231,9 +232,6 @@ Ltac solve_to_val :=
| |- to_val ?e = Some ?v =>
let e' := R.of_expr e in change (to_val (R.to_expr e') = Some v);
apply R.to_val_Some; simpl; unfold R.to_expr; unlock; reflexivity
| |- IntoVal ?e ?v =>
let e' := R.of_expr e in change (to_val (R.to_expr e') = Some v);
apply R.to_val_Some; simpl; unfold R.to_expr; reflexivity
| |- is_Some (to_val ?e) =>
let e' := R.of_expr e in change (is_Some (to_val (R.to_expr e')));
apply R.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
......
......@@ -99,34 +99,6 @@ Section lang_rules.
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
(** Helper Lemmas for weakestpre. *)
Lemma wp_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. exact: wp_ectx_bind. Qed.
Lemma wp_pure E e1 e2 φ Φ :
PureExec φ e1 e2
φ
WP e2 @ E {{ Φ }} WP e1 @ E {{ Φ }}.
Proof. apply wp_pure_step_later. Qed.
Lemma wp_rec E f x erec e1 e2 Φ :
e1 = Rec f x erec
is_Some (to_val e2)
Closed (x :b: f :b: ) erec
WP subst' f e1 (subst' x e2 erec) @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
Proof.
iIntros (? [v ?] ?) "HWP". subst.
iApply (wp_pure with "HWP"); eauto.
Qed.
Lemma wp_tlam E e Φ {Hcl: Closed e} : WP e @ E {{ Φ }} WP TApp (TLam e) @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step_no_fork (TApp _) e); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_fork E e Φ :
(|={E}=> Φ #()) WP e {{ _, True }} WP Fork e @ E {{ Φ }}.
Proof.
......@@ -137,4 +109,10 @@ Section lang_rules.
- intros; inv_head_step; eauto.
Qed.
(** Helper Lemmas for weakestpre. *)
Lemma wp_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. exact: wp_ectx_bind. Qed.
End lang_rules.
......@@ -116,6 +116,8 @@ Proof.
eapply ectx_lang_ctx. }
Qed.
Ltac wp_value := etrans; [|eapply wp_value; apply _]; simpl.
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
......@@ -125,7 +127,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
[apply _ (* PureExec *)
|try (exact I || reflexivity || tac_rel_done)
|apply _ (* IntoLaters *)
|simpl_subst/= (* new goal *)])
|simpl_subst/=; try wp_value (* new goal *)])
end.
Tactic Notation "wp_rec" := wp_pure (App (Rec _ _ _) _) || wp_pure (App _ _).
......@@ -148,8 +150,6 @@ Tactic Notation "wp_tlam" := wp_pure (TApp (TLam _)).
Tactic Notation "wp_unpack" := wp_pure (Unpack (Pack _) _).
Tactic Notation "wp_pack" := wp_unpack.
Ltac wp_value := etrans; [| eapply wp_value; tac_rel_done]; lazy beta.
(** ** Stateful reductions *)
(* WARNING: Most of the code below is copypasta from heap_lang *)
......
......@@ -84,24 +84,15 @@ Section CG_Counter.
iApply bin_log_related_wp_l.
wp_bind (FG_increment #x).
unfold FG_increment. unlock.
iApply wp_rec; eauto.
iNext. simpl.
iApply wp_value; eauto.
iApply wp_rec; eauto.
iNext. simpl.
wp_bind (Load (# x)).
iApply (wp_load with "[Hx]"); auto. iNext.
iIntros "Hx".
iApply wp_rec; eauto.
iNext. simpl.
wp_bind (BinOp _ _ _).
wp_rec.
wp_rec.
wp_load.
wp_rec.
wp_binop.
iApply wp_value.
wp_bind (CAS _ _ _).
iApply (wp_cas_suc with "[Hx]"); auto.
iNext. iIntros "Hx".
wp_if.
iApply wp_value; auto.
by iApply "Hlog".
Qed.
......
......@@ -23,13 +23,13 @@ Section Refinement.
(WP rand #() {{ v, v = #true v = #false}})%I.
Proof.
unfold rand. unlock.
iApply wp_rec; eauto. iNext. simpl.
wp_bind (Alloc _). iApply wp_alloc; auto. iNext. iIntros (y) "Hy".
wp_rec.
wp_alloc y as "Hy".
iMod (inv_alloc choiceN _ (y ↦ᵢ #false y ↦ᵢ #true)%I with "[Hy]") as "#Hinv"; eauto.
iApply wp_rec; eauto. iNext. simpl.
wp_rec.
wp_bind (Fork _). iApply wp_fork. iNext.
iSplitL.
- iModIntro. iApply wp_rec; eauto. iNext; simpl.
- iModIntro. wp_rec.
iInv choiceN as "[Hy | Hy]" "Hcl"; iApply (wp_load with "Hy"); eauto; iNext;
iIntros "Hy"; iMod ("Hcl" with "[Hy]"); eauto.
- iInv choiceN as "[Hy | Hy]" "Hcl"; iApply (wp_store with "Hy"); eauto; iNext;
......
......@@ -496,7 +496,7 @@ Section refinement.
iMod ("Hcl" with "[-Hj]").
{ iNext. iExists _,_,_; subst; iFrame; eauto. }
iModIntro.
wp_if. iApply wp_value.
wp_if.
iExists #(); iFrame; eauto.
** (** CAS FAILS *)
wp_cas_fail.
......@@ -525,7 +525,7 @@ Section refinement.
iRight. iLeft. iSplit; eauto. }
iModIntro. wp_if.
wp_case.
wp_seq. iApply wp_value. iExists #(); eauto. }
wp_seq. iExists #(); eauto. }
(* * Pop refinement *)
{ iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
......@@ -625,4 +625,3 @@ Section refinement.
Qed.
End refinement.
......@@ -99,7 +99,6 @@ Section side_channel.
iModIntro.
wp_if.
wp_proj.
iApply wp_value.
iLeft.
iExists v'; iSplit; auto.
- wp_cas_fail.
......@@ -107,7 +106,6 @@ Section side_channel.
iRight; iLeft; auto.
iModIntro.
wp_if.
iApply wp_value.
iRight; auto.
- iDestruct "H" as "[Hl H]".
wp_cas_fail.
......@@ -134,22 +132,19 @@ Section side_channel.
iModIntro.
wp_if.
wp_proj.
iApply wp_value.
iLeft.
auto.
- wp_cas_fail.
iMod ("Hclose" with "[H]").
iRight; iLeft; done.
iModIntro.
wp_if.
iApply wp_value; auto.
wp_if; eauto.
- iDestruct "H" as "[Hl Hγ]".
wp_cas_fail.
iMod ("Hclose" with "[Hl Hγ]").
iRight; iRight; iFrame.
iModIntro.
wp_if.
iApply wp_value; auto.
wp_if; eauto.
Qed.
Lemma mk_offer_works P (v : val) :
......@@ -244,7 +239,6 @@ Section mailbox.
iModIntro.
wp_case_inl.
wp_seq.
iApply wp_value.
iApply "HΦ"; auto.
+ iDestruct "H" as (v' γ) "[Hl' #Hoffer]".
wp_load.
......
......@@ -177,7 +177,7 @@ Section masked.
iExists (RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e')). iIntros "{$Hj} !#".
iLöb as "IH". iIntros ([v v']) "#Hiv". simpl. iIntros (j' K') "Hj".
iModIntro. simpl.
iApply (wp_rec _ f x (subst_p _ e)); eauto 2 using to_of_val. iNext.
wp_rec.
iApply fupd_wp.
tp_rec j'.
pose (vvs':=(<[x:=(v,v')]>(<[f:=(RecV f x (subst_p (delete f (delete x (fst <$> vvs))) e), RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e'))]>vvs))).
......@@ -308,7 +308,8 @@ Section masked.
iExists (TLamV (env_subst (snd <$> vvs) e')). cbn.
iFrame "Hj". iAlways.
iIntros (τi ? j' K') "Hv /=".
iApply wp_tlam; eauto. iModIntro; iNext; iApply fupd_wp.
iModIntro. wp_tlam.
iApply fupd_wp.
tp_tlam j'; eauto.
iSpecialize ("IH" $! τi with "[] Hs [HΓ]"); auto.
{ by rewrite interp_env_ren. }
......
......@@ -9,7 +9,7 @@ Proof.
wp_rec.
wp_rec.
wp_op.
by wp_value.
done.
Qed.
Lemma wp_proj2 `{heapG Σ} Φ :
......@@ -19,5 +19,5 @@ Proof.
iIntros "HΦ".
wp_proj.
wp_proj.
by wp_value.
done.
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