Commit 1754bf9c authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Finishing up synchronization soundness.

parent d6842e2a
......@@ -3268,8 +3268,6 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
intros l1 d l2 R1 R2 R mtchd; induction mtchd; cbn; ProjectChorDestructor; auto.
Qed.
Lemma LocalSyncSoundness' : forall C1 l1 d l2 E11 E12 E21 E22 R1 R2 R,
ProjectChor C1 l1 = Some E11 ->
ProjectChor C1 l2 = Some E21 ->
......@@ -3416,16 +3414,6 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
end; auto]]]];
repeat (cbn in *; ProjectChorDestructor; eauto); fail).
(* 8: { *)
(* inversion step1; subst. inversion H3. *)
(* inversion mtchd; subst. inversion step2; subst. *)
(* -- destruct (IHC0 _ _ _ _ _ _ _ _ _ _ eq1 eq H3 H5 H4) *)
(* as [C1 [projp2 [projl2 [projR1' [projR2' step]]]]]. *)
(* exists (C.DefLocal l C1 C2); repeat split; cbn; ProjectChorDestructor; *)
(* auto with ConExpr Chor. *)
(* -- inversion mtchd. *)
(* } *)
1:{ pose proof (MatchedSyncRedicesNotAllowChoice _ _ _ _ _ _ mtchd) as nac.
destruct (UnmergeRelStep' _ _ _ _ _ step1 nac (ConExprMergeRelSpec2 _ _ _ projp1))
as [E11' [E12' [merge1 [step3 step4]]]].
......@@ -3498,6 +3486,54 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
all: try (inversion step2; subst; inversion mtchd; subst; inversion step1; subst;
exists C1; repeat split; auto with ConExpr Chor; destruct (neq0 eq_refl); fail).
Qed.
Lemma ChoiceLabelPairToRedices : forall l1 d l2 L1 L2 R1 R2,
l1 <> l2 ->
ChoiceLabelPair l1 d l2 L1 L2 ->
ConExprRedexToLabel R1 = L1 ->
ConExprRedexToLabel R2 = L2 ->
exists R, MatchedSyncRedices l1 d l2 R1 R2 R.
Proof using.
intros l1 d l2 L1 L2 R1 R2 neq pr; revert R1 R2 neq; induction pr;
cbn; intros R1 R2 neq eq1 eq2; destruct R1; destruct R2; cbn in *;
ProjectChorDestructor; try discriminate.
- inversion eq1; clear eq1; subst; inversion eq2; clear eq2; subst;
eexists; econstructor; eauto.
- inversion eq1; clear eq1; subst; inversion eq2; clear eq2; subst;
eexists; econstructor; eauto.
- inversion eq1; clear eq1; subst; inversion eq2; clear eq2; subst.
destruct (IHpr R1 R2 neq eq_refl eq_refl) as [R mtchd];
exists (C.RFun R); constructor; auto.
- inversion eq1; clear eq1; subst; inversion eq2; clear eq2; subst.
destruct (IHpr R1 R2 neq eq_refl eq_refl) as [R mtchd];
exists (C.RArg R); constructor; auto.
Qed.
Corollary LocalSyncSoundness : forall C1 l1 d l2 E11 E12 E21 E22 L1 L2,
l1 <> l2 ->
ProjectChor C1 l1 = Some E11 ->
ProjectChor C1 l2 = Some E21 ->
ConExprStep E11 L1 E12 ->
ConExprStep E21 L2 E22 ->
ChoiceLabelPair l1 d l2 L1 L2 ->
exists R C2, ProjectChor C2 l1 = Some E12
/\ ProjectChor C2 l2 = Some E22
/\ ProjectRedex R l1 = Some L1
/\ ProjectRedex R l2 = Some L2
/\ C.ChorStep R [] C1 C2.
Proof using.
intros C1 l1 d l2 E11 E12 E21 E22 L1 L2 H H0 H1 H2 H3 H4.
destruct (ConExprStepToPrime H2) as [R1 [eq1 step1]];
destruct (ConExprStepToPrime H3) as [R2 [eq2 step2]].
destruct (ChoiceLabelPairToRedices l1 d l2 L1 L2 R1 R2 H H4 eq1 eq2)
as [R mtchd].
destruct (LocalSyncSoundness' C1 l1 d l2 E11 E12 E21 E22 R1 R2 R
H0 H1 step1 step2 mtchd)
as [C2 [proj21 [proj22 [projR1 [projR2 step]]]]].
exists R; exists C2; split; [|split; [|split; [|split]]]; auto.
rewrite <- eq1; apply ProjectRedexTriangle1; auto.
rewrite <- eq2; apply ProjectRedexTriangle1; auto.
Qed.
Theorem SysTauSoundness : forall C1 nms Π1 Π2,
SystemOfNames C1 nms = Some Π1 ->
......@@ -3599,7 +3635,6 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
try discriminate; auto with ConExpr; try (constructor; auto; fail).
all: rewrite H0 in eq0; auto; inversion eq0.
Qed.
Theorem CommSoundness : forall C1 nms Π1 Π2 l v l',
SystemOfNames C1 nms = Some Π1 ->
......@@ -3659,6 +3694,119 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
exists E2' ;split; auto.
Qed.
Theorem ProjectChoiceSystem : forall R l d l' L1 L2,
ProjectRedex R l = Some L1 ->
ProjectRedex R l' = Some L2 ->
ChoiceLabelPair l d l' L1 L2 ->
RedexToSystemLabel R = ChoiceLabel l d l'.
Proof using.
intros R; induction R; intros p v q L1 L2; cbn;
intros eq1 eq2 pr; ProjectChorDestructor; inversion pr; subst; try discriminate;
try match goal with
| [ H : ?a <> ?a |- _] => destruct (H eq_refl)
end; try (eapply IHR; eauto); reflexivity.
Qed.
Theorem ChoiceRedexPair : forall R l d l',
RedexToSystemLabel R = ChoiceLabel l d l' ->
l <> l' ->
exists L1 L2, ProjectRedex R l = Some L1 /\
ProjectRedex R l' = Some L2 /\
ChoiceLabelPair l d l' L1 L2 /\
(forall l'', l'' <> l -> l'' <> l' -> ProjectRedex R l'' = None).
Proof using.
intros R; induction R; intros p v q eq neq; cbn in *;
ProjectChorDestructor; try discriminate;
repeat match goal with
| [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
| [ H : ChoiceLabel ?a ?b ?c = ChoiceLabel ?d ?e ?f |- _ ] =>
inversion H; clear H; subst
| [ |- exists L1 L2, Some ?L1' = Some L1 /\ Some ?L2' = Some L2 /\ _ /\ _ ] =>
exists L1'; exists L2'; split; [reflexivity|split; [reflexivity|split]]
| [ IH : forall l v l', RedexToSystemLabel ?R = ChoiceLabel l v l' ->
l <> l' ->
exists L1 L2,
ProjectRedex R l = Some L1 /\
ProjectRedex R l' = Some L2 /\
ChoiceLabelPair l v l' L1 L2 /\
(forall l'', l'' <> l -> l'' <> l' -> ProjectRedex R l'' = None),
H1 : RedexToSystemLabel ?R = ChoiceLabel ?l ?v ?l',
H2 : ?l <> ?l' |- _ ] =>
specialize (IH l v l' H1 H2);
let L1 := fresh "L" in
let L2 := fresh "L" in
let eq1 := fresh "eq" in
let eq2 := fresh "eq" in
let neq := fresh "neq" in
destruct IH as [L1 [L2 [eq1 [eq2 neq]]]]
| [H1 : ?a = ?b, H2 : ?a = ?c |- _ ] =>
tryif unify b c
then fail
else assert (b = c) by (rewrite H1 in H2; exact H2); clear H2; subst
end; eauto with ConExpr; try intros; ProjectChorDestructor;
try discriminate; auto with ConExpr; try (constructor; auto; fail).
all: rewrite H0 in eq0; auto; inversion eq0.
Qed.
Theorem ChoiceSoundness : forall C1 nms Π1 Π2 l d l',
SystemOfNames C1 nms = Some Π1 ->
SystemStep Π1 (ChoiceLabel l d l') Π2 ->
exists C2 Π2' R, SystemOfNames C2 nms = Some Π2'
/\ C.ChorStep R [] C1 C2
/\ LessNondetSystem Π2' Π2
/\ RedexToSystemLabel R = ChoiceLabel l d l'.
Proof using.
intros C1 nms Π1 Π2 p d q 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 H1; destruct H1; auto).
assert (In q nms)
by (apply (SystemOfNamesLookup C1 nms Π1 eq) in H2; destruct H2; auto).
assert (ProjectChor C1 p = Some pE1)
by (apply (SystemOfNamesLookup C1 nms Π1 eq) in H1; destruct H1; auto).
assert (ProjectChor C1 q = Some qE1)
by (apply (SystemOfNamesLookup C1 nms Π1 eq) in H2; destruct H2; auto).
destruct (LocalSyncSoundness C1 p d q pE1 pE2 qE1 qE2 L1 L2 H H10 H11 H3 H4 H0)
as [R [C2 [proj_l1_2 [proj_l2_2 [proj_r1 [proj_r2 step]]]]]].
pose proof (ProjectChoiceSystem R p d q L1 L2 proj_r1 proj_r2 H0).
destruct (ChoiceRedexPair R p d q H12 H) as [L1' [L2' [proj_r1' [proj_r2' [_ eq_none]]]]].
rewrite proj_r1 in proj_r1'; rewrite proj_r2 in proj_r2';
inversion proj_r1'; inversion proj_r2'; clear proj_r1' proj_r2'; subst;
rename L1' into L1; rename L2' into L2.
destruct (SystemOfNamesCompletenessExists _ _ _ _ _ _ eq step) as [Π2' eq'].
pose proof (proj2 (SystemOfNamesLookup _ _ _ eq' p pE2) ltac:(split; auto)).
pose proof (proj2 (SystemOfNamesLookup _ _ _ eq' q qE2) ltac:(split; auto)).
exists C2; exists Π2'; exists R; split; [|split; [|split]]; auto.
unfold LessNondetSystem; split.
- intros l E1 mt.
destruct (L.eq_dec l p); subst; [|destruct (L.eq_dec l q); subst].
-- exists pE2; split; auto.
pose proof (LMF.MapsToUnique mt H13); subst; auto with ConExpr.
-- exists qE2; split; auto.
pose proof (LMF.MapsToUnique mt H14); subst; auto with ConExpr.
-- assert (ProjectRedex R l = None) by (apply eq_none; auto).
destruct (proj1 (SystemOfNamesLookup _ _ _ eq' l E1) mt) as [i proj_l2].
destruct (ProjectChor C1 l) as [E1'|] eqn:proj_l1;
[|rewrite (SystemOfNamesLookupNone _ _ _ i proj_l1) in eq; inversion eq].
pose proof (ProjectChorRedex _ _ _ _ _ _ _ proj_l1 proj_l2 H15 step).
exists E1'; split; auto.
apply H7; auto.
apply (proj2 (SystemOfNamesLookup _ _ _ eq l E1') ltac:(split; auto)).
- intros l E2 mt; right.
destruct (L.eq_dec l p); subst; [|destruct (L.eq_dec l q); subst].
-- exists pE2; split; auto. pose proof (LMF.MapsToUnique mt H5); subst; reflexivity.
-- exists qE2; split; auto. pose proof (LMF.MapsToUnique mt H6); subst; reflexivity.
-- apply H7 in mt; auto.
destruct (proj1 (SystemOfNamesLookup _ _ _ eq l E2) mt) as [i proj_l_1].
destruct (ProjectChor C2 l) as [E2'|] eqn:proj_l2;
[|rewrite (SystemOfNamesLookupNone _ _ _ i proj_l2) in eq'; inversion eq'].
assert (ProjectRedex R l = None) by (apply eq_none; auto).
pose proof (ProjectChorRedex _ _ _ _ _ _ _ proj_l_1 proj_l2 H15 step).
pose proof (proj2 (SystemOfNamesLookup _ _ _ eq' l E2') ltac:(split; auto)).
exists E2' ;split; auto.
Qed.
(* Theorem Soundness : forall C1 nms Π1 L Π2 r, *)
(* In r nms -> *)
(* SystemOfNames C1 nms = Some Π1 -> *)
......
......@@ -1247,8 +1247,6 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
Inductive ChoiceLabelPair : Loc -> LRChoice -> Loc -> Label -> Label -> Prop :=
BaseChoiceLabelPair : forall l1 d l2,
ChoiceLabelPair l1 d l2 (ChooseLabel l2 d) (AllowChoiceLabel l1 d)
| BaseChoiceLabelPair' : forall l1 d l2,
ChoiceLabelPair l1 d l2 (AllowChoiceLabel l1 d) (ChooseLabel l2 d)
| FunChoiceLabelPair : forall l1 d l2 L1 L2,
ChoiceLabelPair l1 d l2 L1 L2 -> ChoiceLabelPair l1 d l2 (FunLabel L1) (FunLabel L2)
| ArgChoiceLabelPair : forall l1 d l2 L1 L2,
......
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