Mefresa.Examples.ThesisRunningExample
Require Import Mefresa.GCM.GCMWellFormedness.
Parameter p : path.
Parameter iclC : implementationClass.
Parameter sigS1 : signature.
Parameter sigC2 : signature.
Definition cpath : path := (app p (Ident "Component N"::nil)).
Definition C : component :=
Component (Ident "C") cpath iclC Configuration
nil
(Interface (Ident "s1") sigS1 (app cpath (Ident "C"::nil))
External Server Functional Mandatory Singleton ::
Interface (Ident "c2") sigC2 (app cpath (Ident "C"::nil))
External Client Functional Mandatory Singleton :: nil)
nil.
Parameter iclS : implementationClass.
Parameter sigS2 : signature.
Parameter sigC3 : signature.
Definition spath : path := cpath.
Definition S : component :=
Component (Ident "S") spath iclS Configuration
nil
(Interface (Ident "s2") sigS2 (app spath (Ident "S"::nil))
External Server Functional Mandatory Singleton ::
Interface (Ident "c3") sigC3 (app spath (Ident "S"::nil))
External Client Functional Optional Singleton :: nil)
nil.
Parameter sigC1 : signature.
Parameter sigS3 : signature.
Definition pN : path := cpath.
Definition N : component :=
Component (Ident "Component N") p "_blank" Configuration
(C :: S :: nil)
(Interface (Ident "c1") sigC1 pN
External Server Functional Mandatory Singleton ::
Interface (Ident "c1") sigC1 pN
Internal Client Functional Mandatory Singleton ::
Interface (Ident "s3") sigS3 pN
Internal Server Functional Optional Singleton ::
Interface (Ident "s3") sigS3 pN
External Client Functional Optional Singleton :: nil
)
(Export pN (Ident "c1") (Ident "C") (Ident "s1") ::
Normal pN (Ident "C") (Ident "c2") (Ident "S") (Ident "s2") ::
Import pN (Ident "s3") (Ident "S") (Ident "c3") :: nil
).
Lemma C_is_well_formed:
well_formed_component C.
Proof.
apply WellFormedComponent.
Case "1/4 : C's subcomponents are well-formed".
intros. simpl in H. fromfalse.
Case "2/4 : C's subcomponents possess unique id's".
simpl. apply Unique_Base. reflexivity.
Case "3/4 : C's interfaces are well-formed".
simpl.
eapply WellFormedInterfaces_Step; auto.
eapply UniquePairs_Step; auto.
eapply NotInPairStep; auto;
eapply NotInPair_Nil; auto.
eapply UniquePairs_Step; auto.
eapply NotInPair_Nil; auto.
apply UniquePairs_Base; auto.
eapply WellFormedInterfaces_Step; auto.
eapply UniquePairs_Step; auto.
eapply NotInPair_Nil; auto.
apply UniquePairs_Base; auto.
Case "4/4 : C's bindings are well-formed".
intuition.
Qed.
Lemma S_is_well_formed:
well_formed_component S.
Proof.
apply WellFormedComponent.
Case "1/4 : S's subcomponents are well-formed".
intros. simpl in H. fromfalse.
Case "2/4 : S's subcomponents possess unique id's".
simpl. apply Unique_Base. reflexivity.
Case "3/4 : S's interfaces are well-formed".
simpl.
eapply WellFormedInterfaces_Step; auto.
eapply UniquePairs_Step; auto.
eapply NotInPairStep; auto;
eapply NotInPair_Nil; auto.
eapply UniquePairs_Step; auto.
eapply NotInPair_Nil; auto.
apply UniquePairs_Base; auto.
eapply WellFormedInterfaces_Step; auto.
eapply UniquePairs_Step; auto.
eapply NotInPair_Nil; auto.
apply UniquePairs_Base; auto.
Case "4/4 : S's bindings are well-formed".
intuition.
Qed.
Lemma first_well_formedness_proof:
well_formed_component N.
Proof.
apply WellFormedComponent.
Case "1/4 : N's subcomponents are well-formed". Focus.
simpl; intros.
destruct H as [Hc | [Hs | Hf]]; subst;
[apply C_is_well_formed |
apply S_is_well_formed |
fromfalse
].
Case "2/4 : N's subcomponents possess unique id's".
simpl.
eapply Unique_Step; auto.
eapply NotInStep; auto.
Case "3/4 : N's interface are well-formed".
simpl.
eapply WellFormedInterfaces_Step; auto.
eapply UniquePairs_Step; auto.
do 3 (eapply NotInPairStep; auto).
eapply NotInPair_Nil; auto.
eapply UniquePairs_Step; auto.
do 2 (eapply NotInPairStep; auto).
eapply NotInPair_Nil; auto.
eapply UniquePairs_Step; auto.
eapply NotInPairStep; auto.
eapply NotInPair_Nil; auto.
eapply UniquePairs_Step; auto.
eapply NotInPair_Nil; auto.
eapply UniquePairs_Base; auto.
eapply WellFormedInterfaces_Step; auto.
eapply UniquePairs_Step; auto.
do 2 (eapply NotInPairStep; auto).
eapply NotInPair_Nil; auto.
eapply UniquePairs_Step; auto.
eapply NotInPairStep; auto.
eapply NotInPair_Nil; auto.
eapply UniquePairs_Step; auto.
eapply NotInPair_Nil; auto.
eapply UniquePairs_Base; auto.
eapply WellFormedInterfaces_Step; auto.
eapply UniquePairs_Step; auto.
eapply NotInPairStep; auto.
eapply NotInPair_Nil; auto.
eapply UniquePairs_Step; auto.
eapply NotInPair_Nil; auto.
eapply UniquePairs_Base; auto.
eapply WellFormedInterfaces_Step; auto.
eapply UniquePairs_Step; auto.
eapply NotInPair_Nil; auto.
eapply UniquePairs_Base; auto.
Case "4/4 : N's bindings are well-formed".
simpl. intro. intro.
destruct H as [He | [ Hn | Hi]]; subst.
compute; intuition.
compute; intuition.
inversion Hi; subst.
compute; intuition. fromfalse.
Qed.
Require Import GCMTyping.
Lemma N_has_sound_cardinality:
sound_cardinality N.
Proof.
split.
Case "Dealing with Export bindings". Focus.
split; intros.
SCase "At least bound once".
simpl in *.
destruct H as [Hc1e | [Hc1i | [Hs3e | [ Hs3i | Hf]]]];
subst; simpl in *; try fromfalse; try congruence; auto.
SCase "Recursion on inner levels".
simpl in *.
destruct H as [Hc | [Hs | Hf]]; subst; try fromfalse.
SSCase "Subcomponent C".
split; simpl; intros; auto; try fromfalse.
SSCase "Subcomponent S".
split; simpl; intros; auto; try fromfalse.
Case "Dealing wth Normal/Import bindings".
split; intros.
SCase "At least bound once". Focus.
destruct H as [Hc | [Hs | Hf]]; subst; try fromfalse.
destruct H0 as [Hc1 | [Hc2 | Hf]];
subst; simpl in *; try fromfalse; auto.
destruct H0 as [Hc1 | [Hc2 | Hf]];
subst; simpl in *; try fromfalse; auto.
SCase "Recursion on inner levels".
destruct H as [Hc | [Hs | Hf]]; subst; try fromfalse.
SSCase "Subcomponent C".
split; simpl; intros; try fromfalse; auto.
SSCase "Subcomponent S".
split; simpl; intros; try fromfalse; auto.
Qed.
Lemma N_has_sound_contingency:
sound_contingency N.
Proof.
split.
Case "Subcomponents external interfaces are bound". Focus.
apply CEMI_Bound; intros.
SCase "Interfaces are bound". Focus.
destruct H as [Hs | [Hc | Hf]]; subst; try fromfalse;
simpl in *.
SSCase "Subcomponent C". Focus.
destruct H0 as [Hs1 | [ Hc2 | Hf]]; subst; try fromfalse;
simpl in *; try congruence.
split; try congruence. intros.
destruct H as [Hs2 | Hf]; try fromfalse; subst; auto.
SSCase "Subcomponent S".
destruct H0 as [Hs1 | [ Hc2 | Hf]]; subst; try fromfalse;
simpl in *; try congruence.
SCase "Recursion on inner levels".
destruct H as [Hs | [Hc | Hf]]; try fromfalse; subst.
SSCase "Subcomponent C".
split; simpl; intros; try fromfalse.
SSCase "Subcomponent S".
split; simpl; intros; try fromfalse.
Case "Internal interfaces are bound".
apply CIMI_Bound.
SCase "1/2 : interfaces at level n are bound".
intros.
split.
SSCase "1/2 : recipients cannot be 0".
simpl in H.
destruct H as [Hc1e | [Hc1i | [ Hs3i | [ Hs3e | Hf ]]]];
subst; simpl in *; try congruence.
unfold get_export_binding_recipients.
simpl.
congruence.
SSCase "2/2 : All recipients are of mandatory contingency".
intros.
simpl in H.
destruct H as [Hc1e | [Hc1i | [ Hs3i | [ Hs3e | Hf ]]]];
subst; simpl in *; try congruence.
destruct H3 as [H3i | H3f]; subst; try fromfalse.
simpl. refl.
fromfalse.
SCase "2/2 : Inner hierarchical levels also meet property".
intros.
simpl in H.
destruct H as [Hc | [Hs | Hf]]; subst; try fromfalse.
SSCase "Subcomponent C case". Focus.
apply CIMI_Bound; simpl; intros.
SSSCase "C's internal interfaces are bound".
destruct H as [Hs1 | [ Hc2 | Hf]];
subst; simpl in *; try fromfalse; try congruence.
SSSCase "Inner hierarchical levels of C".
fromfalse.
SSCase "Subcomponent S case".
apply CIMI_Bound; simpl; intros; try fromfalse.
destruct H as [Hs1 | [ Hc2 | Hf]];
subst; simpl in *; try fromfalse; try congruence.
Qed.
Lemma first_well_typedness_proof:
well_typed N.
Proof.
split.
Case "Sound Cardinality".
apply N_has_sound_cardinality.
Case "Sound contingency".
apply N_has_sound_contingency.
Qed.
Require Import Semantics.
Require Import Reductions.
Notation " [ ] " := nil.
Notation " [ x ] " := (cons x nil).
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..).
Definition root : path := nil.
Definition build_N (id: ident) : operation :=
Mk_component id root "null" Configuration [] [] [];
Mk_interface (Ident "c1") sigC1 [id] External
Server Functional Mandatory Singleton;
Mk_interface (Ident "c1") sigC1 [id] Internal
Client Functional Mandatory Singleton;
Mk_interface (Ident "s3") sigS3 [id] Internal
Server Functional Optional Singleton;
Mk_interface (Ident "s3") sigS3 [id] External
Client Functional Optional Singleton.
Definition build_C (id:ident) (pN:path) : operation :=
Mk_component id pN iclC Configuration [] [] [];
Mk_interface (Ident "s1") sigS1 (app pN [id])
External Server Functional Mandatory Singleton;
Mk_interface (Ident "c2") sigC2 (app pN [id])
External Client Functional Mandatory Singleton.
Definition build_S (id:ident) (pN:path) : operation :=
Mk_component id pN iclS Configuration [] [] [];
Mk_interface (Ident "s2") sigS2 (app pN [id])
External Server Functional Mandatory Singleton;
Mk_interface (Ident "c3") sigC3 (app pN [id])
External Client Functional Optional Singleton.
Definition bind_system (pN:path) : operation :=
Mk_binding (Export pN (Ident "c1") (Ident "C") (Ident "s1"));
Mk_binding (Normal pN (Ident "C") (Ident "c2") (Ident "S") (Ident "s2"));
Mk_binding (Import pN (Ident "s3") (Ident "S") (Ident "c3")).
Definition build_running_example : operation :=
let idN := Ident "Component N" in
let idC := Ident "C" in
let idS := Ident "S" in
build_N idN; build_C idC [idN]; build_S idS [idN]; bind_system [idN].
Lemma reduction_example':
let idN := Ident "Component N" in
let idC := Ident "C" in
let idS := Ident "S" in
exists s, build_N idN / empty_state ~~~>* Done / s /\
exists s', build_C idC [idN] / s ~~~>* Done /s' /\
exists s'', build_S idS [idN] / s' ~~~>* Done / s'' /\
exists s''', bind_system [idN] / s'' ~~~>* Done / s'''.
Proof.
intros.
eexists.
split.
Case "Build N".
unfold build_N.
mstep; compute; intuition.
apply WellFormedComponent; simpl; intros; auto. fromfalse.
inversion H; subst; auto.
eapply ValidInterfacePath_Base; auto. eexists.
simpl; auto. inversion H; subst.
apply NotInPair_Nil; auto.
eapply ValidInterfacePath_Base; auto. eexists.
simpl; auto. inversion H; subst.
eapply NotInPairStep; simpl; auto.
apply NotInPair_Nil; auto.
eapply ValidInterfacePath_Base; auto. eexists.
simpl; auto. inversion H; subst.
eapply NotInPairStep; simpl; auto.
eapply NotInPairStep; simpl; auto.
apply NotInPair_Nil; auto.
eapply rsc_step.
apply SMakeInterface.
eapply ValidInterfacePath_Base; auto. eexists.
split; simpl; auto.
intro. simpl. intros. inversion H; subst.
simpl.
do 3 (eapply NotInPairStep; auto).
apply NotInPair_Nil; auto.
refl. auto.
eexists. split.
Case "Build C".
unfold build_C. mstep.
unfold valid_component_path. simpl.
subst idN.
eapply ValidN. refl.
exists (Component (Ident "Component N") [] "null" Configuration []
(Interface (Ident "s3") sigS3 [Ident "Component N"] External Client
Functional Optional Singleton ::
Interface (Ident "s3") sigS3 [Ident "Component N"] Internal Server
Functional Optional Singleton ::
Interface (Ident "c1") sigC1 [Ident "Component N"] Internal Client
Functional Mandatory Singleton ::
Interface (Ident "c1") sigC1 [Ident "Component N"] External Server
Functional Mandatory Singleton :: nil) []). intro.
simpl. auto.
refl.
simpl. apply Valid0; auto.
apply WellFormedComponent; simpl; intros; auto. fromfalse.
intro. simpl. intro. inversion H; subst.
apply NotInNil; auto.
refl.
unfold valid_interface_path. simpl.
eapply ValidInterfacePath_Step; auto.
exists (Component (Ident "Component N") [] "null" Configuration
[Component idC [idN] iclC Configuration [] [] []]
(Interface (Ident "s3") sigS3 [Ident "Component N"] External Client
Functional Optional Singleton ::
Interface (Ident "s3") sigS3 [Ident "Component N"] Internal Server
Functional Optional Singleton ::
Interface (Ident "c1") sigC1 [Ident "Component N"] Internal Client
Functional Mandatory Singleton ::
Interface (Ident "c1") sigC1 [Ident "Component N"] External Server
Functional Mandatory Singleton :: nil) []).
simpl. split; auto.
eapply ValidInterfacePath_Base; auto.
eexists; auto. refl.
intro. simpl. intro.
inversion H; subst. simpl.
apply NotInPair_Nil; auto.
refl.
eapply rsc_step.
apply SMakeInterface.
eapply ValidInterfacePath_Step. refl.
simpl. eexists. split; auto.
simpl.
eapply ValidInterfacePath_Base; auto.
eexists. simpl. refl.
intro. simpl. intro. inversion H; subst.
simpl.
eapply NotInPairStep; auto.
eapply NotInPair_Nil; auto.
refl.
auto.
eexists; split.
Case "Build S".
unfold build_S.
mstep.
unfold valid_component_path.
eapply ValidN. refl.
simpl. exists (Component (Ident "Component N") [] "null" Configuration
[Component idC [idN] iclC Configuration []
(Interface (Ident "c2") sigC2 (idN:: idC::nil) External Client Functional
Mandatory Singleton ::
Interface (Ident "s1") sigS1 (idN :: idC :: nil) External Server Functional
Mandatory Singleton :: nil) []]
(Interface (Ident "s3") sigS3 [Ident "Component N"] External Client
Functional Optional Singleton ::
Interface (Ident "s3") sigS3 [Ident "Component N"] Internal Server
Functional Optional Singleton ::
Interface (Ident "c1") sigC1 [Ident "Component N"] Internal Client
Functional Mandatory Singleton ::
Interface (Ident "c1") sigC1 [Ident "Component N"] External Server
Functional Mandatory Singleton :: nil) []).
simpl. intro. refl.
simpl. refl.
eapply Valid0; auto.
apply WellFormedComponent; simpl; intros; auto. fromfalse.
intro. simpl. intro. inversion H; subst.
eapply NotInStep; auto. refl.
unfold valid_interface_path. simpl.
eapply ValidInterfacePath_Step. refl.
exists (Component (Ident "Component N") [] "null" Configuration
((Component idS (idN :: nil) iclS Configuration [] [] []) ::
(Component idC (idN :: nil) iclC Configuration []
(Interface (Ident "c2") sigC2 (idN :: idC :: nil) External Client Functional
Mandatory Singleton ::
Interface (Ident "s1") sigS1 (idN :: idC :: nil) External Server Functional
Mandatory Singleton ::nil) []) :: nil)
(Interface (Ident "s3") sigS3 (Ident "Component N" :: nil) External Client
Functional Optional Singleton ::
Interface (Ident "s3") sigS3 (Ident "Component N" :: nil) Internal Server
Functional Optional Singleton ::
Interface (Ident "c1") sigC1 (Ident "Component N" :: nil) Internal Client
Functional Mandatory Singleton ::
Interface (Ident "c1") sigC1 (Ident "Component N" :: nil) External Server
Functional Mandatory Singleton :: nil) []).
simpl. split; auto.
eapply ValidInterfacePath_Base; auto.
eexists. simpl. refl.
intro. simpl; intro. inversion H; subst; simpl.
apply NotInPair_Nil; auto. refl.
eapply rsc_step.
apply SMakeInterface.
eapply ValidInterfacePath_Step; auto. refl.
simpl. eexists. split; auto.
eapply ValidInterfacePath_Base; auto.
simpl. eexists. refl.
intro. simpl. intro. inversion H; subst.
simpl.
eapply NotInPairStep; auto.
apply NotInPair_Nil; auto. refl.
auto.
Case "Bind system".
eexists.
unfold bind_system.
mstep.
unfold valid_component_binding.
simpl.
eapply ValidComponentBinding_Step; simpl.
eexists. split. refl. simpl.
compute; auto.
compute. intro; fromfalse. refl.
compute.
eapply ValidComponentBinding_Step; simpl.
eexists. split. refl. compute; auto.
compute. intro. inversion H. congruence. fromfalse.
refl.
eapply rsc_step.
mstep.
compute.
eapply ValidComponentBinding_Step; simpl.
eexists. split. refl. compute; auto.
compute. intro. inversion H. congruence.
inversion H0; [congruence | fromfalse].
refl. auto.
Qed.
Lemma reduction_example:
exists s, build_running_example / empty_state ~~~>* Done / s.
Proof.
assert(He := reduction_example').
destruct He as
(s, (Hs, (s', (Hs', (s'', (Hs'', (s''', Hs'''))))))).
exists s'''.
unfold build_running_example.
apply op_sequence_reduction with (s':=s); auto.
apply op_sequence_reduction with (s':=s'); auto.
apply op_sequence_reduction with (s':=s''); auto.
Qed.