Began proofs of extensions

parent 0e3b8477
Pipeline #6114 failed with stages
in 0 seconds
......@@ -4,7 +4,7 @@ From stdpp Require Export strings.
From stdpp Require Import gmap.
Set Default Proof Using "Type".
Module heap_lang.
Module dist_lang.
Open Scope Z_scope.
(** Expressions and vals. *)
......@@ -329,7 +329,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| FaaLCtx e2 => FAA e e2
| FaaRCtx v1 => FAA (of_val v1) e
| StartCtx => Start e
| SendLCtx e2 => Send (e) (e2)
| SendLCtx e2 => Send e e2
| SendRCtx v1 => Send (of_val v1) e
| RecvCtx => Recv e
end.
......@@ -469,7 +469,7 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop
| FaaS l i1 e2 i2 σ :
to_val e2 = Some (LitV (LitInt i2))
σ !! l = Some (LitV (LitInt i1))
head_step (FAA (Lit $ LitLoc l) e2) σ (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) []
head_step (FAA (Lit $ LitLoc l) e2) σ (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
(* | NewChanS' l σ : *)
(* σ !! l = None → *)
(* head_step NewChan σ (Pair (Lit $ LitChan l Left) (Lit $ LitChan l Right)) (<[l:=LitV $ LitBuf [] []]>σ) [] *)
......@@ -482,7 +482,7 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop
(* to_val e = Some v → *)
(* rval::rs = r' → *)
(* rexpr = of_val (LitV $ LitInt $ rval) → *)
(* head_step (Recv (Lit $ LitChan l Left)) σ (rexpr) (<[l:= LitV $ LitBuf (l') (rs)]>σ) [] *).
(* head_step (Recv (Lit $ LitChan l Left)) σ (rexpr) (<[l:= LitV $ LitBuf (l') (rs)]>σ) []. *)
(** Work done here *)
Inductive buffer : Set :=
......@@ -502,24 +502,36 @@ Inductive head_step' : expr → state' → expr → state' → list (expr) → P
snd σ = σc
σc !! l = None
head_step' NewChan σ (Pair (Lit $ LitChan l Left) (Lit $ LitChan l Right)) (σs, <[l:=Buffer [] []]>σc) []
| SendLeftS σ σs σc l l' r' e v:
| SendLS σ σs σc l l' r' e v:
fst σ = σs
snd σ = σc
σc !! l = Some (Buffer l' r')
to_val e = Some $ v
head_step' (Send (Lit $ LitChan l Left) e) σ (Lit $ LitUnit) (σs, <[l:=Buffer (l' ++ [v]) r']>σc) []
| RecvLeftSucS l l' r' rval rs rexpr σ σs σc :
| SendRS σ σs σc l l' r' e v:
fst σ = σs
snd σ = σc
σc !! l = Some (Buffer l' r')
r' = rval::rs
rexpr = of_val rval
head_step' (Recv (Lit $ LitChan l Left)) σ rexpr (σs, <[l:= Buffer l' rs]>σc) []
| RecvLeftFailS l l' r' σ σc :
to_val e = Some $ v
head_step' (Send (Lit $ LitChan l Right) e) σ (Lit $ LitUnit) (σs, <[l:=Buffer l' (r' ++ [v])]>σc) []
| RecvLSucS l l' r' rv σ σs σc :
fst σ = σs
snd σ = σc
σc !! l = Some (Buffer l' r')
r' = []
head_step' (Recv (Lit $ LitChan l Left)) σ (Recv (Lit $ LitChan l Left)) σ [].
σc !! l = Some (Buffer l' (rv::r'))
head_step' (Recv (Lit $ LitChan l Left)) σ (of_val rv) (σs, <[l:= Buffer l' r']>σc) []
| RecvRSucS l l' r' lv σ σs σc :
fst σ = σs
snd σ = σc
σc !! l = Some (Buffer (lv::l') r')
head_step' (Recv (Lit $ LitChan l Right)) σ (of_val lv) (σs, <[l:= Buffer l' r']>σc) []
| RecvLFailS l l' σ σc :
snd σ = σc
σc !! l = Some (Buffer l' [])
head_step' (Recv (Lit $ LitChan l Left)) σ (Recv (Lit $ LitChan l Left)) σ []
| RecvRFailS l r' σ σc :
snd σ = σc
σc !! l = Some (Buffer [] r')
head_step' (Recv (Lit $ LitChan l Right)) σ (Recv (Lit $ LitChan l Right)) σ [].
Definition processes := gmap loc heap.
Definition state'' := prod processes channels.
......@@ -529,10 +541,10 @@ Inductive pval := PVal (l: loc) (v : val).
(* Definition lift_expr (i : loc) (e : expr) : pexpr := PExpr i e. *)
(* Definition unpack_expr (e:pexpr) : (loc * expr) := *)
(* match e with *)
(* | PExpr i e => (i,e) *)
(* end. *)
Definition unpack_expr (e:pexpr) : expr :=
match e with
| PExpr i e => e
end.
(* Definition unpack_state (s:processes) (i:loc) : heap := *)
(* match s !! i with *)
......@@ -564,10 +576,11 @@ Inductive head_step'' : pexpr → state'' → pexpr → state'' → list (pexpr)
forPairs p pes es
head_step' e (σ,pσc) e' (σ',pσc') es
head_step'' pe pσ pe' pσ' pes
| StartS p e σ σp σc p' :
| StartS p e σ σp σc p' v :
fst σ = σp
snd σ = σc
σp !! p' = None
to_val e = Some $ v
head_step'' (PExpr p (Start e)) σ (PExpr p (Lit $ LitUnit)) (<[p':=]>σp, σc) [PExpr p' e].
(** Basic properties about the language *)
......@@ -581,10 +594,36 @@ Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma val_head_stuck' e1 σ1 e2 σ2 efs : head_step' e1 σ1 e2 σ2 efs to_val e1 = None.
Proof.
destruct 1; try naive_solver. generalize H1. apply val_head_stuck.
Qed.
Lemma val_head_stuck'' e1 σ1 e2 σ2 efs : head_step'' e1 σ1 e2 σ2 efs to_val (unpack_expr e1) = None.
Proof.
destruct 1; try naive_solver. rewrite H. simpl. generalize H8. apply val_head_stuck'.
Qed.
Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
head_step (fill_item Ki e) σ1 e2 σ2 efs is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
Lemma head_ctx_step_val' Ki e σ1 e2 σ2 efs :
head_step' (fill_item Ki e) σ1 e2 σ2 efs is_Some (to_val e).
Proof.
inversion 1;
first (generalize dependent H2; apply head_ctx_step_val);
repeat (generalize dependent H; destruct Ki; inversion_clear 1; simplify_option_eq; by eauto).
Qed.
Lemma head_ctx_step_val'' Ki p e σ1 e2 σ2 efs :
head_step'' (PExpr p (fill_item Ki e)) σ1 e2 σ2 efs is_Some (to_val e).
Proof.
inversion 1;
first (generalize dependent H9; subst; assert (e0 = fill_item Ki e) by (by inversion H0); rewrite H1; apply head_ctx_step_val');
repeat (generalize dependent H; destruct Ki; inversion_clear 1; simplify_option_eq; by eauto).
Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None to_val e2 = None
fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2.
......@@ -672,20 +711,20 @@ Lemma subst_rec_ne' f y e x es :
subst' x es (Rec f y e) = Rec f y (subst' x es e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Lemma dist_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Proof.
split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
End heap_lang.
End dist_lang.
(** Language *)
Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
Canonical Structure dist_ectxi_lang := EctxiLanguage dist_lang.dist_lang_mixin.
Canonical Structure dist_ectx_lang := EctxLanguageOfEctxi dist_ectxi_lang.
Canonical Structure dist_lang := LanguageOfEctx dist_ectx_lang.
(* Prefer heap_lang names over ectx_language names. *)
Export heap_lang.
(* Prefer dist_lang names over ectx_language names. *)
Export dist_lang.
(** Define some derived forms *)
Notation Lam x e := (Rec BAnon x e).
......
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