Commit 04c5dba4 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Cleaned up CtrlLang and RestrictedSemantics. Removed closure for values.

parent 2e558915
This diff is collapsed.
......@@ -412,23 +412,23 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
match R with
| C.RDone p _ _ =>
if L.eq_dec l p
then Some Tau
then Some Iota
else None
| C.RIfE p _ _ =>
if L.eq_dec l p
then Some Tau
then Some Iota
else None
| C.RIfTT p =>
if L.eq_dec l p
then Some Tau
then Some Iota
else None
| C.RIfFF p =>
if L.eq_dec l p
then Some Tau
then Some Iota
else None
| C.RSendE p e1 e2 q =>
if L.eq_dec l p
then Some Tau
then Some Iota
else None
| C.RSendV p v q =>
if L.eq_dec l p
......@@ -446,14 +446,14 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
else if L.eq_dec l q
then Some (AllowChoiceLabel p LR)
else None
| C.RDefLocal p _ => Some SyncTau
| C.RDefLocal p _ => Some SyncIota
| C.RAppLocalE p _ _ =>
if L.eq_dec l p
then Some Tau
then Some Iota
else None
| C.RAppLocal _ _ =>
Some SyncTau
| C.RAppGlobal => Some SyncTau
Some SyncIota
| C.RAppGlobal => Some SyncIota
| C.RFun R => match ProjectRedex R l with
| Some L => Some (FunLabel L)
| None => None
......@@ -1489,17 +1489,17 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
Fixpoint RedexToSystemLabel (R : C.Redex) : SystemLabel :=
match R with
| C.RDone x x0 x1 => SysTau
| C.RIfE x x0 x1 => SysTau
| C.RIfTT x => SysTau
| C.RIfFF x => SysTau
| C.RSendE l e1 e2 l' => SysTau
| C.RDone x x0 x1 => SysIota
| C.RIfE x x0 x1 => SysIota
| C.RIfTT x => SysIota
| C.RIfFF x => SysIota
| C.RSendE l e1 e2 l' => SysIota
| C.RSendV l v l' => CommLabel l v l'
| C.RSync l ch l' => ChoiceLabel l ch l'
| C.RDefLocal x x0 => SysSyncTau
| C.RAppLocalE x x0 x1 => SysTau
| C.RAppLocal x x0 => SysSyncTau
| C.RAppGlobal => SysSyncTau
| C.RDefLocal x x0 => SysSyncIota
| C.RAppLocalE x x0 x1 => SysIota
| C.RAppLocal x x0 => SysSyncIota
| C.RAppGlobal => SysSyncIota
| C.RFun R => RedexToSystemLabel R
| C.RArg R => RedexToSystemLabel R
end.
......@@ -1822,7 +1822,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
| [ H : LM.MapsTo ?a ?b LM.empty |- _ ] =>
destruct (LM.empty_1 H)
| [ H : ?l <> ?p |- LM.MapsTo ?p ?E (LM.add ?l ?E' ?Π) ] => apply LM.add_2; auto
| [ |- UniqueLocList [?l]] => exact (SingletonUniqueLocList l)
(* | [ |- UniqueLocList [?l]] => exact (SingletonUniqueLocList l) *)
| [ eq : SystemOfNames ?C ?nms = Some ?Π,
mt : LM.MapsTo ?l ?E ?Π |- _ ] =>
lazymatch goal with
......@@ -1993,9 +1993,9 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
end.
Lemma ProjectTauSystemTau : forall R l L,
Lemma ProjectIotaSystemIota : forall R l L,
InternalLabel L ->
ProjectRedex R l = Some L -> RedexToSystemLabel R = SysTau.
ProjectRedex R l = Some L -> RedexToSystemLabel R = SysIota.
Proof using.
intro R; induction R; intros l' L; cbn; intros il eq;
ProjectPirExprDestructor; try reflexivity; try discriminate;
......@@ -2003,8 +2003,8 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
all: eapply IHR; eauto.
Qed.
Lemma ProjectSystemTauTau : forall R l L,
RedexToSystemLabel R = SysTau ->
Lemma ProjectSystemIotaIota : forall R l L,
RedexToSystemLabel R = SysIota ->
ProjectRedex R l = Some L ->
InternalLabel L.
Proof using.
......@@ -2066,7 +2066,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
end; auto.
Qed.
Lemma TauUnique : forall R, RedexToSystemLabel R = SysTau ->
Lemma IotaUnique : forall R, RedexToSystemLabel R = SysIota ->
exists l L, InternalLabel L /\ ProjectRedex R l = Some L /\
forall l', l <> l' -> ProjectRedex R l' = None.
Proof using.
......@@ -2081,7 +2081,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
all: rewrite (eq2 l' neq) in eq0; inversion eq0.
Qed.
Lemma TauUniqueInvolved : forall R, RedexToSystemLabel R = SysTau ->
Lemma IotaUniqueInvolved : forall R, RedexToSystemLabel R = SysIota ->
exists l, C.InvolvedWithRedex R l /\
forall l', l <> l' -> ~ C.InvolvedWithRedex R l'.
Proof using.
......@@ -2093,7 +2093,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
all: apply IHR; auto.
Qed.
Lemma ProjectInvolved : forall R, RedexToSystemLabel R = SysTau ->
Lemma ProjectInvolved : forall R, RedexToSystemLabel R = SysIota ->
forall l, C.InvolvedWithRedex R l <-> exists L, ProjectRedex R l = Some L.
Proof using.
intros R; induction R; cbn; ProjectPirExprDestructor;
......@@ -2108,16 +2108,16 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
- specialize (IHR eq p). apply IHR; exists l; auto.
Qed.
Theorem ProjectSystemTauStep : forall R B C1 C2 Π1 Π2 nms,
Theorem ProjectSystemIotaStep : forall R B C1 C2 Π1 Π2 nms,
SystemOfNames C1 nms = Some Π1 ->
SystemOfNames C2 nms = Some Π2 ->
RedexToSystemLabel R = SysTau ->
RedexToSystemLabel R = SysIota ->
C.PirStep R B C1 C2 ->
(forall l, C.InvolvedWithRedex R l -> In l nms) ->
exists Π2', SystemStep Π1 SysTau Π2' /\ LessNondetSystem Π2 Π2'.
exists Π2', SystemStep Π1 SysIota Π2' /\ LessNondetSystem Π2 Π2'.
Proof using.
intros R B C1 C2 Π1 Π2 nms eq1 eq2 eq3 step1 inv_R.
destruct (TauUniqueInvolved R eq3) as [l [inv_l ninv]].
destruct (IotaUniqueInvolved R eq3) as [l [inv_l ninv]].
pose proof (inv_R l inv_l) as in_l.
destruct (ProjectPirExpr C1 l) as [E1|] eqn:proj_l1;
[|rewrite (SystemOfNamesLookupNone _ _ _ in_l proj_l1) in eq1; inversion eq1].
......@@ -2127,12 +2127,12 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
pose proof (proj2 (SystemOfNamesLookup _ _ _ eq2 l E2) ltac:(split; auto)) as mt2.
destruct (proj1 (ProjectInvolved R eq3 l) inv_l) as [L proj_lR].
pose proof (LocalCompleteness C1 R B C2 l E1 E2 L proj_l1 proj_l2 proj_lR step1) as lstep.
destruct (TauUnique R eq3) as [l' [L' [il_L [eqR' neqR']]]].
destruct (IotaUnique R eq3) as [l' [L' [il_L [eqR' neqR']]]].
destruct (L.eq_dec l' l) as [ e|n]; subst;
[|apply neqR' in n; rewrite n in proj_lR; inversion proj_lR].
rewrite proj_lR in eqR'; inversion eqR'; clear eqR'; symmetry in H0; subst.
exists (LM.add l E2 Π1); split; [| unfold LessNondetSystem; split].
- eapply TauStep; eauto. apply LM.add_1.
- eapply IotaStep; eauto. apply LM.add_1.
intros q E neq; split; intro mt.
apply LM.add_2; auto.
apply LM.add_3 in mt; auto.
......@@ -2160,12 +2160,12 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
exists E''; split; auto. apply (SystemOfNamesLookup _ _ _ eq2 l' E''); split; auto.
Qed.
Lemma RedexSysSyncTauSyncTau : forall R,
RedexToSystemLabel R = SysSyncTau ->
Lemma RedexSysSyncIotaSyncIota : forall R,
RedexToSystemLabel R = SysSyncIota ->
exists L, IsSyncLabel L /\ forall l, ProjectRedex R l = Some L.
Proof using.
intros R; induction R; intros eq; cbn in *; try discriminate; try reflexivity.
1-3: exists SyncTau; split; auto; constructor.
1-3: exists SyncIota; split; auto; constructor.
all: destruct (IHR eq) as [L [eq' sync_L]]; clear eq.
exists (FunLabel L). 2: exists (ArgLabel L).
all: split; [constructor; auto|]; intro l; specialize (sync_L l); auto;
......@@ -2284,9 +2284,9 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
Proof using.
intros R B C1 C2 Π1 Π2 nms eq1 eq2 step allinvolved.
destruct (RedexToSystemLabel R) eqn:eqR.
- eapply ProjectSystemTauStep; eauto.
- eapply ProjectSystemIotaStep; eauto.
- clear allinvolved.
destruct (RedexSysSyncTauSyncTau R eqR) as [L [projl_R syncL]].
destruct (RedexSysSyncIotaSyncIota R eqR) as [L [projl_R syncL]].
exists Π2; split; [|reflexivity]; econstructor; eauto.
intros l E1 E2 mt1 mt2.
destruct (proj1 (SystemOfNamesLookup C1 nms Π1 eq1 l E1) mt1) as [i proj_l_1].
......@@ -2565,7 +2565,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
Qed.
Lemma LocalTauSoundness' : forall C1 p E1 R E2,
Lemma LocalIotaSoundness' : forall C1 p E1 R E2,
InternalLabel (CtrlExprRedexToLabel R) ->
CtrlExprStep' E1 R E2 ->
ProjectPirExpr C1 p = Some E1 ->
......@@ -2642,7 +2642,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
let merge := fresh "merge" in
let step1 := fresh "step" in
let step2 := fresh "step" in
destruct (UnmergeRelTauStep' E1 E2 E3 _ E4 H' ltac:(cbn; auto) H)
destruct (UnmergeRelIotaStep' E1 E2 E3 _ E4 H' ltac:(cbn; auto) H)
as [E1' [E2' [merge [step1 step2]]]]
end
end.
......@@ -2673,7 +2673,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
end.
Qed.
Corollary LocalTauSoundness : forall C1 p E1 E2 L,
Corollary LocalIotaSoundness : forall C1 p E1 E2 L,
ProjectPirExpr C1 p = Some E1 ->
CtrlExprStep E1 L E2 ->
InternalLabel L ->
......@@ -2683,7 +2683,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
Proof using.
intros C1 p E1 E2 L H H0 H12.
destruct (CtrlExprStepToPrime H0) as [R [pf step]]; clear H0; subst.
destruct (LocalTauSoundness' C1 p E1 R E2 H12 step H) as [C2 [eq2 step']].
destruct (LocalIotaSoundness' C1 p E1 R E2 H12 step H) as [C2 [eq2 step']].
exists (CtrlExprRedexToRedex R p); exists C2; split; [|split]; auto.
clear step' eq2 C2 step H E1 E2 C1.
induction R; cbn; ProjectPirExprDestructor; try discriminate; auto; inversion H12; subst.
......@@ -3196,7 +3196,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
inversion val.
Qed.
Lemma LocalSyncTauSoundness' : forall C1 L ls,
Lemma LocalSyncIotaSoundness' : forall C1 L ls,
ls <> [] ->
IsSyncLabel L ->
(forall l, In l (C.LocsInPirExpr C1) -> In l ls) ->
......@@ -3365,7 +3365,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
intro l; cbn; rewrite (eqs l); auto.
Qed.
Corollary LocalSyncTauSoundness : forall C1 L ls,
Corollary LocalSyncIotaSoundness : forall C1 L ls,
ls <> [] ->
IsSyncLabel L ->
(forall l, In l (C.LocsInPirExpr C1) -> In l ls) ->
......@@ -3375,7 +3375,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
exists C2 R, (forall l, ProjectRedex R l = Some L) /\ C.PirStep R [] C1 C2.
Proof using.
intros C1 L ls H H0 H1 H2.
eapply LocalSyncTauSoundness'; eauto.
eapply LocalSyncIotaSoundness'; eauto.
intros l i; destruct (H2 l i) as [E1 [E2 [eq1 step]]].
destruct (CtrlExprStepToPrime step) as [R [eq2 step']].
exists R; exists E1; exists E2; split; [|split]; auto.
......@@ -3649,7 +3649,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
let eq2 := fresh "eq" in
let neq := fresh "neq" in
let merge := fresh "merge" in
destruct (UnmergeRelACStep' E11 E12 E1 d R E2 H H' H'')
destruct (UnmergeRelACStep' E11 E12 E1 d R E2 H H'' H')
as [d1 [R1 [E21 [d2 [R2 [E22 [step1 [step2 [scrs1 [scrs2 [adcl1 [adcl2 [[eq1 [eq2 merge]] | [[eq1 neq] | [eq1 neq]]]]]]]]]]]]]]]; subst
end
| [ H : context[LetRet ?E1 ?E2], H' : CtrlExprStep' ?E1 ?R ?E1' |- _ ] =>
......@@ -3869,7 +3869,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
destruct (UnmergeRelStep' _ _ _ _ _ step1 nac (CtrlExprMergeRelSpec2 _ _ _ projp1))
as [E11' [E12' [merge1 [step3 step4]]]];
pose proof (MatchedSyncRedicesDCL _ _ _ _ _ _ mtchd) as adcl;
destruct (UnmergeRelACStep' _ _ _ _ _ _ adcl step2 (CtrlExprMergeRelSpec2 _ _ _ projp2))
destruct (UnmergeRelACStep' _ _ _ _ _ _ adcl (CtrlExprMergeRelSpec2 _ _ _ projp2) step2)
as [d1 [R1' [E21' [d2 [R2' [E22' [step5 [step6 [scrs1 [scrs2 [adcl1 [adcl2 [[eq3 [eq4 merge]] | [[eq3 neq'] | [eq3 neq']]]]]]]]]]]]]]]; subst;
repeat match goal with
| [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
......@@ -3992,22 +3992,22 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
rewrite <- eq2; apply ProjectRedexTriangle1; auto.
Qed.
Theorem SysTauSoundness : forall C1 nms Π1 Π2,
Theorem SysIotaSoundness : forall C1 nms Π1 Π2,
SystemOfNames C1 nms = Some Π1 ->
SystemStep Π1 SysTau Π2 ->
SystemStep Π1 SysIota Π2 ->
exists R C2 Π2', SystemOfNames C2 nms = Some Π2'
/\ C.PirStep R [] C1 C2
/\ LessNondetSystem Π2' Π2
/\ RedexToSystemLabel R = SysTau.
/\ RedexToSystemLabel R = SysIota.
Proof using.
intros C1 nms Π1 Π2 eq step;
revert C1 nms eq; dependent induction step; intros C1 nms eq.
assert (In p nms) by (apply (SystemOfNamesLookup C1 nms Π1 eq) in H; destruct H; auto).
assert (ProjectPirExpr C1 p = Some E1)
by (apply (SystemOfNamesLookup C1 nms Π1 eq) in H; destruct H; auto).
destruct (LocalTauSoundness C1 p E1 E2 L H5 H0 H1) as [R [C2 [eq1 [eq2 cstep]]]].
pose proof (ProjectTauSystemTau R p L H1 eq1).
destruct (TauUnique R H6) as [q [L' [iL' [eq' neq]]]].
destruct (LocalIotaSoundness C1 p E1 E2 L H5 H0 H1) as [R [C2 [eq1 [eq2 cstep]]]].
pose proof (ProjectIotaSystemIota R p L H1 eq1).
destruct (IotaUnique R H6) as [q [L' [iL' [eq' neq]]]].
destruct (L.eq_dec q p) as [e |n]; subst;
[clear eq'| apply neq in n; rewrite n in eq1; inversion eq1].
destruct (SystemOfNamesCompletenessExists R [] C1 C2 Π1 nms eq cstep) as [Π2' eq3].
......@@ -4278,16 +4278,16 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
nms <> [] ->
(forall p, In p (C.LocsInPirExpr C1) -> In p nms) ->
SystemOfNames C1 nms = Some Π1 ->
SystemStep Π1 SysSyncTau Π2 ->
SystemStep Π1 SysSyncIota Π2 ->
exists R C2 Π2', SystemOfNames C2 nms = Some Π2'
/\ C.PirStep R [] C1 C2
/\ LessNondetSystem Π2' Π2
/\ RedexToSystemLabel R = SysSyncTau.
/\ RedexToSystemLabel R = SysSyncIota.
Proof using.
intros C1 nms Π1 Π2 nempty tn eq step;
revert C1 nms nempty tn eq; dependent induction step;
intros C1 nms nempty tn eq.
destruct (LocalSyncTauSoundness C1 L nms nempty H tn) as [C2 [R [eq' step]]].
destruct (LocalSyncIotaSoundness C1 L nms nempty H tn) as [C2 [R [eq' step]]].
- intros l i;
destruct (ProjectPirExpr C1 l) as [E1|] eqn:proj_l1;
[|rewrite (SystemOfNamesLookupNone C1 nms l i proj_l1) in eq; inversion eq].
......@@ -4340,7 +4340,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
/\ RedexToSystemLabel R = L.
Proof using.
intros C1 nms Π1 L Π2 H H0 H1 H2; destruct L.
eapply SysTauSoundness; eauto.
eapply SysIotaSoundness; eauto.
eapply SyncSoundness; eauto.
eapply CommSoundness; eauto.
eapply ChoiceSoundness; eauto.
......@@ -4392,7 +4392,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
inversion iacl; subst; apply IHL; auto).
destruct (LowerStepNondet E1 L E2 E21 H0 lnd H4) as [E22 [lnd' step']].
exists (LM.add p E22 Π21); split; auto;
[|eapply TauStep; eauto;
[|eapply IotaStep; eauto;
[apply LM.add_1| intros q E neq; split; intro mt];
[apply LM.add_2; auto| apply LM.add_3 in mt; auto]].
unfold LessNondetSystem; split.
......@@ -4440,7 +4440,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
inversion iacl; subst; apply IHL; auto).
destruct (LowerListOfSteps l L H5 H3 H4) as [ [nd [nr eqv]]].
exists (OutputListToSystem ); split; [unfold LessNondetSystem; split|
eapply SyncTauStep; eauto].
eapply SyncIotaStep; eauto].
-- intros p E mt. apply OutputUniqueToSystem in mt; auto.
destruct (nd p E mt) as [E1 [E2 [E3 [i [lnd step]]]]].
exists E3; split; auto. eapply H2; eauto.
......
......@@ -46,6 +46,12 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
apply SyncLabelEqDec.
Defined.
Inductive PirExprVal : PirExpr -> Prop :=
| ReturnVal : forall (l : Loc) (v : Expr),
ExprVal v -> PirExprVal (Done l v)
| FunLocalVal : forall l C, PirExprVal (FunLocal l C)
| FunGlobalVal : forall C, PirExprVal (FunGlobal C).
(* RENAMING *)
(*
......@@ -1160,6 +1166,17 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
(* Properties of equivalence *)
(*
Values are only equivalent to values.
*)
Lemma PirExprValStableEquiv : forall C1 C2,
PirExprVal C1 -> C1 C2 -> PirExprVal C2.
Proof using.
intros C1 C2 val1 eqv; revert val1; induction eqv; intro val1; inversion val1;
subst; auto.
all: inversion val1; subst; constructor; auto; eapply PirExprClosedAboveEquiv; eauto.
Qed.
(*
Local renaming and subsitution do not affect equivalence, as long as you do the
same renamings/subsitutions on each side.
......@@ -1462,34 +1479,6 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
destruct n; auto. rewrite ExprRenameVar; auto.
Qed.
(*
We could not define Pirouette values earlier, because we require that functions be
closed to be values.
*)
Inductive PirExprVal : PirExpr -> Prop :=
| ReturnVal : forall (l : Loc) (v : Expr),
ExprVal v -> PirExprVal (Done l v)
| FunLocalVal : forall l C, (* PirExprClosedAbove (fun l' => if L.eq_dec l l' then 1 else 0) 1 C *)
(* -> *)PirExprVal (FunLocal l C)
| FunGlobalVal : forall C, (* PirExprClosedAbove (fun _ => 0) 2 C -> *)
PirExprVal (FunGlobal C).
(* Lemma PirExprValuesClosed : forall C : PirExpr, PirExprVal C -> PirExprClosed C. *)
(* Proof. *)
(* intros C H; induction H; unfold PirExprClosed. *)
(* apply DoneClosedAbove; apply ExprValuesClosed in H; unfold ExprClosed in H; exact H. *)
(* apply FunLocalClosedAbove; auto. *)
(* apply FunGlobalClosedAbove; auto. *)
(* Qed. *)
Lemma PirExprValStableEquiv : forall C1 C2,
PirExprVal C1 -> C1 C2 -> PirExprVal C2.
Proof using.
intros C1 C2 val1 eqv; revert val1; induction eqv; intro val1; inversion val1;
subst; auto.
all: inversion val1; subst; constructor; auto; eapply PirExprClosedAboveEquiv; eauto.
Qed.
(*
The labeled-transition system itself. Here, the list `B` is the set of _blocked_
locations, which are not allowed to participate in the step. Note how `B` grows
......
This diff is collapsed.
Supports Markdown
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