Receive almost done - last stable at 15-03-2019

parent e7051e41
This diff is collapsed.
......@@ -745,14 +745,17 @@ Definition val : Type := proc_id * buff_lang.val.
Definition to_buff_val (v : val) : buff_lang.val := v.2.
Coercion to_buff_val : val >-> buff_lang.val.
Definition ectx_item : Type := proc_id * buff_lang.ectx_item.
Definition to_buff_ectx_item (Ki : ectx_item) : buff_lang.ectx_item := Ki.2.
Coercion to_buff_ectx_item : ectx_item >-> buff_lang.ectx_item.
(* Definition ectx_item : Type := proc_id * buff_lang.ectx_item. *)
(* Definition to_buff_ectx_item (Ki : ectx_item) : buff_lang.ectx_item := Ki.2. *)
(* Coercion to_buff_ectx_item : ectx_item >-> buff_lang.ectx_item. *)
(* Definition fill_item : ectx_item -> _ -> expr := λ Ki e, (e.1, buff_lang.fill_item Ki.2 e.2). *)
Definition fill_item : _ -> _ -> expr := λ Ki e, (e.1, buff_lang.fill_item Ki e.2).
(* Definition ectx_item := buff_lang.ectx_item. *)
(* Definition fill_item : _ -> _ -> expr := λ Ki e, (e.1, buff_lang.fill_item Ki e.2). *)
Definition ectx_item : Type := buff_lang.ectx_item.
Definition to_buff_ectx_item (Ki : ectx_item) : buff_lang.ectx_item := Ki.
Coercion to_buff_ectx_item : ectx_item >-> buff_lang.ectx_item.
Definition fill_item : ectx_item -> _ -> expr := λ Ki e, (e.1, buff_lang.fill_item Ki e.2).
Definition of_val : val -> expr := λ v, (v.1, buff_lang.of_val v.2).
Definition to_val : expr -> option val := λ e, (λ v, (e.1, v)) <$> buff_lang.to_val (e.2).
......
......@@ -45,11 +45,41 @@ Instance distG_irisG `{distG Σ} : irisG proc_lang Σ := {
well_formed e := (mapsto (p_init e.1));
fork_post _ := True%I
}.
Instance distG_WFCtx `{distG Σ} K : WFCtx (fill_item K).
Proof. split. intros [p e]. iSplit; [eauto | by iIntros "[_ Hwf]"]. Qed.
Instance distG_WFRed `{distG Σ} : WFRed.
(* Global Instance distG_WFCtx `{distG Σ} K : WFCtx (fill_item K). *)
(* Proof. split. intros [p e]. iSplit; [eauto | by iIntros "[_ Hwf]"]. Qed. *)
Lemma lift_fill_item p e KS :
(foldl (flip fill_item) (p, e) KS) = (p, (foldl (flip fill_item) (p, e) KS).2).
Proof.
generalize dependent e.
induction KS as [|K KS]; intros e; eauto.
Qed.
Global Instance distG_WFCtx_fill_item `{distG Σ} K : WFCtx (fill_item K).
Proof. split; intros [p e]. iSplit. eauto. iIntros "[_ Hwf]". eauto. Qed.
Global Instance distG_WFCtx_fill `{distG Σ} KS : WFCtx (fill KS).
Proof.
split.
intros e.
iSplit.
- iIntros "#Hwf".
simpl. unfold fill. simpl.
iSplit.
+ iIntros (e0) "#Hp".
destruct e0.
by rewrite lift_fill_item.
+ destruct e.
by rewrite lift_fill_item.
- iIntros "[_ Hwf]".
simpl. unfold fill. simpl.
destruct e.
by rewrite lift_fill_item.
Qed.
Global Instance distG_WFRed `{distG Σ} : WFRed.
Proof.
split.
inversion 1. simpl in *.
......
This diff is collapsed.
......@@ -493,10 +493,13 @@ Module proc_lang_meta.
Lemma subst_map_is_closed_nil e vs : is_closed_expr [] e subst_map vs e = e.
Proof. frame_proc. apply buff_lang_meta.subst_map_is_closed_nil. Qed.
Lemma proc_id_preserved e1 σ1 κ e2 σ2 efs :
head_step e1 σ1 κ e2 σ2 efs ->
e1.1 = e2.1.
Proof. intros. inverse_head. Qed.
Lemma proc_id_ctx_preserved e K :
e.1 = (fill_item K e).1.
Proof. eauto. Qed.
End proc_lang_meta.
\ No newline at end of file
......@@ -213,6 +213,15 @@ Section typing.
(Some $ inl $ TrRecv (LitV $ 10) $ TrEnd).
Proof. repeat constructor. Qed.
Inductive trace_recv_only : trace -> Prop :=
| trace_recv_only_end : trace_recv_only TrEnd
| trace_recv_only_recv x tr : trace_recv_only tr -> trace_recv_only (TrRecv x tr) .
Inductive trace_send_only : trace -> Prop :=
| trace_send_only_end : trace_send_only TrEnd
| trace_send_only_recv x tr : trace_send_only tr -> trace_send_only (TrSend x tr) .
Global Instance trace_inhabited : Inhabited trace := populate (TrEnd).
Inductive sτ_eval : stype trace stype Prop :=
......@@ -304,6 +313,25 @@ Section typing.
apply sτ_eval_send => //.
apply IHtr => //.
- intros sτ0 sτ HP Hsτ.
, inversion Hsτ. subst. simpl.
apply sτ_eval_recv => //.
apply IHtr => //.
Qed.
Lemma sτ_eval_recv_step sτ0 sτ tr (P : val -> Prop) v :
P v -> sτ_eval sτ0 tr (TRecv P sτ) -> sτ_eval sτ0 (trace_app tr (TrRecv v TrEnd)) (sτ v).
Proof.
generalize dependent sτ.
generalize dependent sτ0.
induction tr.
- intros sτ0 sτ HP Hsτ.
inversion Hsτ. subst.
apply sτ_eval_recv => //.
- intros sτ0 sτ HP Hsτ.
inversion Hsτ. subst. simpl.
apply sτ_eval_send => //.
apply IHtr => //.
- intros sτ0 sτ HP Hsτ.
inversion Hsτ. subst. simpl.
apply sτ_eval_recv => //.
apply IHtr => //.
......
......@@ -125,6 +125,40 @@ Proof.
by iApply "H".
Qed.
(* Definition well_formed_red e1 e2 := *)
(* ∀ σ1 κ σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → well_formed e1 -∗ well_formed e2. *)
(* Lemma wp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E E' Φ} e1 e2 : *)
(* well_formed_red e1 e2 → *)
(* (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) → *)
(* (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → *)
(* κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) → *)
(* (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}. *)
(* Proof. *)
(* Admitted. *)
(* Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ : *)
(* relations.nsteps well_formed_red n e1 e2 → *)
(* PureExec φ n e1 e2 → *)
(* φ → *)
(* (|={E,E'}▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}. *)
(* Proof. *)
(* intro Hred. *)
(* iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ). *)
(* iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done. *)
(* iApply wp_lift_pure_det_step_no_fork. *)
(* - intros σ. eauto. *)
(* - intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val. *)
(* - intros. *)
(* specialize (pure_step_det σ1 κ e2' σ2 efs' H1) as [Hκeq [Hσeq [Heeq Hefseq]]]. *)
(* repeat split=>//. *)
(* done. *)
(* apply pure_step_det. done. *)
(* - by iApply (step_fupd_wand with "Hwp"). *)
(* Qed. *)
Lemma wp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} `{!WFRed} {s E E' Φ} e1 e2 :
( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'
......@@ -137,6 +171,7 @@ Proof.
iIntros (κ e' efs' σ (_&?&->&?)%Hpuredet); auto.
Qed.
Lemma wp_pure_step_fupd `{Inhabited (state Λ)} `{!WFRed} s E E' e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
......@@ -150,6 +185,7 @@ Proof.
- by iApply (step_fupd_wand with "Hwp").
Qed.
Lemma wp_pure_step_later `{Inhabited (state Λ)} `{!WFRed} s E e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
......@@ -185,7 +221,7 @@ Proof.
specialize (step2 step) as [Hκeq [Hσeq [Heeq Hefseq]]].
iModIntro.
iApply fupd_frame_l.
iSplitL "Hσ".
iSplitL "Hσ".
rewrite Hκeq. rewrite Hσeq. simpl. inversion Hefseq. simpl. eauto.
iNext.
iMod ("Hclose").
......
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