Mefresa.Operation.Semantics
In this section we define our operation language that will
allow us to build GCM Architectures. An operational semantics
is discussed along with some of its preserved properties.role
Require Export Mefresa.GCM.CoreElementsFacts.
Require Export Mefresa.GCM.GCMWellFormedness.
Require Import List.
Basic Definitions
Defining this empty state can be achieved as follows:
Definition root := nil : list ident.
Definition empty_state : state := Component (Ident "Root") root "null" Configuration nil nil nil.
Definition empty_state : state := Component (Ident "Root") root "null" Configuration nil nil nil.
Short hand for state
Here, the definition of root is just to give some emphasis on the fact
that we will be building an hierarchy of components, and the empty state
is at the root of this hierarchy.
Projections on state
Definition projStateComponents (s:state) : list component :=
match s with
| Component _ _ _ _ lc _ lb => lc
end.
Definition projStateBindings (s:state) : list binding :=
match s with
| Component _ _ _ _ lc _ lb => lb
end.
Notation "s '->components' " := (projStateComponents s) (at level 80, right associativity) : state_scope.
Notation "s '->bindings' " := (projStateBindings s) (at level 80, right associativity) : state_scope.
Bind Scope state_scope with state.
Delimit Scope state_scope with st.
A Few More Words on State
Function lookup_aux (l:list component)
(id:ident) (acc:list component)
{struct l} : option (component * list component) :=
match l with
| nil => None
| c :: r => if (c->id)%comp == id then Some ((c, app r acc)) else lookup_aux r id (c :: acc)
end.
Function lookup (l:list component) (id:ident)
: option (component * list component) := lookup_aux l id nil.
Lemma lookup_solution_fact:
forall l id c r,
Some (c, r) = lookup l id ->
In c l.
Proof.
intros.
unfold lookup in H.
functional induction (lookup_aux l id nil).
Case "Exit Branch 1/3".
thus inversion H.
Case "Exit Branch 2/3".
inversion H; subst.
thus intuition.
Case "Exit Branch 3/3".
assert (In c r0).
apply IHo; auto.
thus auto with *.
Qed.
Lemma lookup'_id_fact:
forall lc id c r X,
lookup_aux lc id X = Some (c,r) ->
(c->id%comp =id).
Proof.
intros.
functional induction (lookup_aux lc id X).
Case "Branch 1/3".
thus inversion H.
Case "Branch 2/3".
inversion H; subst. clear H.
auto.
Case "Branch 3/3".
apply IHo.
thus exact H.
Qed.
Lemma lookup_id_fact:
forall l id c r,
Some (c, r) = lookup l id ->
(c->id%comp =id).
Proof.
intros.
unfold lookup in H.
apply lookup'_id_fact with (lc:=l) (r:=r) (X:=nil).
symmetry;auto.
Qed.
Hint Resolve lookup_solution_fact lookup_id_fact.
Lemma lookup_get_comp:
forall lc id c r,
lookup lc id = Some (c, r) ->
lc [id] = Some c.
Proof.
intros.
unfold lookup in H.
functional induction lookup_aux lc id (nil:list component);
inversion H; subst; clear H.
Case "1/2".
unfold get_component.
rewrite e0; auto.
Case "2/2".
unfold get_component.
rewrite e0; auto.
Qed.
Hint Resolve lookup_get_comp.
Lemma lookup_congruence_fact:
forall lc id c,
lc [id] = Some c ->
lookup lc id = None ->
False.
Proof.
intros.
unfold lookup in H0.
functional induction lookup_aux lc id (nil:list component).
Case "Exit Branch 1/3".
inversion H.
Case "Exit Branch 2/3".
inversion H0.
Case "Exit Branch 3/3".
apply IHo; auto.
unfold get_component in H;
rewrite e0 in H; auto.
Qed.
Hint Resolve lookup_congruence_fact.
Lemma lookup_mem_fact':
forall l acc id c r,
lookup_aux l id acc = Some (c,r) ->
forall x, In x (l ++ acc) <-> In x (c :: r).
Proof.
intros l acc id c r Hf x.
functional induction lookup_aux l id acc ; inversion Hf ; subst.
reflexivity.
rewrite in_app_cons_fact ; apply IHo ; assumption.
Qed.
Lemma lookup_mem_fact:
forall lc id X c r,
lookup_aux lc id X = Some (c,r) ->
X = nil ->
forall x, In x lc <-> In x (c :: r).
Proof.
intros l id X c r Hf H x ; subst ;
rewrite (app_nil_end l) ;
eapply lookup_mem_fact' ; eassumption.
Qed.
Hint Resolve lookup_mem_fact.
Lemma lookup_get_comp_fact:
forall lc id c r X,
lookup_aux lc id X = Some (c, r) ->
X = nil ->
(c :: r) [id] = Some c.
Proof.
intros.
assert (c->id%comp = id).
symmetry in H.
apply lookup_id_fact with (l:=lc) (r:=r);auto.
unfold lookup; subst; auto.
functional induction lookup_aux lc id X.
Case "Exit Branch 1/3".
inversion H.
Case "Exit Branch 2/3".
inversion H; subst; clear H.
unfold get_component;
rewrite e0; auto.
Case "Exit Branch 3/3".
clear e0.
unfold get_component.
assert (c->id%comp = (c->id)%comp).
auto.
clear IHo.
assert ((c->id%comp == (c->id)%comp) = true).
auto.
rewrite H1;auto.
Qed.
Hint Resolve lookup_get_comp_fact.
Lemma lookup_backup_fact:
forall lc id X c r,
lookup_aux lc id X = Some (c, r) ->
X = nil ->
(forall x, In x r -> In x lc).
Proof.
intros.
destruct lookup_mem_fact' with (l:=lc) (acc:=X) (id:=id) (c:=c) (r:=r) (x:=x); auto.
subst.
assert (lc ++ nil = lc).
apply app_nil_r.
rewrite H0 in *.
apply H3.
right;auto.
Qed.
Hint Resolve lookup_backup_fact.
Lemma lookup_get_fact:
forall lc id c c' r X,
lookup_aux lc id X = Some (c, r) ->
lc[id] = Some c' ->
(c::r)[id] = Some c'.
Proof.
intros.
assert((c->id%comp) = id).
apply lookup'_id_fact with (lc:=lc) (r:=r) (X:=X);auto.
assert(((c->id%comp) == id) = true).
eauto.
unfold get_component; rewrite H2.
functional induction lookup_aux lc id X.
Case "Exit Branch 1/3".
inversion H.
Case "Exit Branch 2/3".
inversion H; subst. clear H.
unfold get_component in H0 ; rewrite e0 in H0;
auto.
Case "Exit Branch 3/3".
apply IHo; auto.
unfold get_component in H0; rewrite e0 in H0; auto.
Qed.
Hint Resolve lookup_get_fact.
Lemma in_entailment:
forall c l,
In c l ->
in_l (c->id%comp) l.
Proof.
intros.
induction l.
Case "List is Nil".
inversion H.
Case "List is not Nil".
destruct ident_dec with (id1:=c->id%comp) (id2:=a->id%comp).
SCase "Ids are Equal".
unfold in_l. rewrite e.
left; refl.
SCase "Ids are not Equal".
right.
apply IHl.
destruct H; subst.
congruence.
auto.
Qed.
Lemma in_get_component_fact:
forall c l id,
In c l ->
unique_ids l ->
c->id%comp = id ->
l [id] = Some c.
Proof.
intros.
functional induction get_component id l.
Case "Exit Branch 1/3".
inversion H.
Case "Exit Branch 2/3".
destruct H; subst. refl.
assert ((e ->id)%comp = (c ->id)%comp ).
eauto.
inversion H0; inversion H2; subst.
clear H2 e1.
rewrite H1 in *.
clear H1.
assert (False).
apply not_in_congruence with (c:=c) (l:=r0); auto.
inversion H1.
Case "Exit Branch 3/3".
apply IHo.
destruct H; subst; auto.
assert ((c ->id)%comp <> (c ->id)%comp).
eauto.
congruence.
inversion H0 ; inversion H1; auto.
Qed.
Lemma get_component_commutes_on_l:
forall l l' id c,
(forall x, In x l <-> In x l') ->
l[id] = Some c ->
unique_ids l ->
unique_ids l' ->
l'[id] = Some c.
Proof.
intros l l' id c H H0 H1 H2.
destruct l.
Case "List is Nil".
inversion H0.
Case "List is not Nil".
destruct H with (x:=c0).
assert (In c0 l').
apply H3;left;auto.
clear H4 H3.
assert (c->id%comp= id).
eauto.
assert (In c (c0 :: l)).
eauto.
apply in_get_component_fact; auto.
destruct H4; subst; auto.
destruct H with (x:=c).
apply H3; eauto.
Qed.
Function get_component_with_path_aux (p:path) (li:list component) {struct p} : option component :=
match p with
| nil => None
| id :: nil => li[id]
| id :: rp => match lookup li id with
| None => None
| Some (c, r) => get_component_with_path_aux rp (c->subComponents%comp)
end
end.
Lemma get_component_on_empty_components_entails_false:
forall c p,
Some c = get_component_with_path_aux p nil ->
False.
Proof.
intros.
destruct p.
Case "Empty Path".
simpl in H.
inversion H.
Case "Path is not Empty".
simpl in H.
destruct p; inversion H.
Qed.
Function get_scope_aux (p:path) (lc:list component) {struct p}: option (list component) :=
match p with
| nil => None
| _ =>
match (get_component_with_path_aux p lc) with
| None => None
| Some c => Some (c->subComponents)%comp
end
end.
Function get_scope (p:path) (s:state) : option (list component) :=
match p, s with
| nil, _ => Some (s->components)%st
| p, Component _ _ _ _ lc _ lb => get_scope_aux p lc
end.
Definition get_component_with_path p (s:state) : option component :=
match p, s with
| nil, _ => None
| p, Component _ _ _ _ lc _ lb => get_component_with_path_aux p lc
end.
Function update_sub_components (c:component) (lc: list component) : component :=
match c with
| Component id p iclass cl lc' li lb => Component id p iclass cl lc li lb
end.
Function add_component_aux (comp_list:list component) (id_list:path) (c:component) {struct id_list} : list component :=
match id_list with
| nil => c :: comp_list
| id :: r => let s := lookup comp_list id in
match s with
| None => nil
| Some (c', backup) =>
let x := add_component_aux (c'->subComponents)%comp r c in
match x with
| nil => nil
| x' => ((update_sub_components c' x') :: backup)
end
end
end.
Function add_component (s:state) (id_list:path) (c_id:ident) (ic:implementationClass)
(cl:controlLevel) (lc:list component)
(li:list interface) (lb:list binding): option state :=
match s with
| Component state_id state_p state_class state_cl state_lc state_li state_lb =>
match add_component_aux state_lc id_list (Component c_id id_list ic cl lc li lb) with
| nil => None
| updated_hierarchy =>
Some (Component state_id state_p state_class state_cl updated_hierarchy state_li state_lb)
end
end.
Function remove_component_aux (comp_list:list component) (p:path) (idComponent:ident) : list component :=
match p with
| nil => remove_component_from_list idComponent comp_list
| idp :: r => let s := lookup comp_list idp in
match s with
| None => nil
| Some (c', backup) =>
let x := remove_component_aux (c'->subComponents)%comp r idComponent in
((update_sub_components c' x) :: backup)
end
end.
Function remove_component (s:state) (p:path) (id:ident) : option state :=
match s with
| Component state_id state_p state_class state_cl state_lc state_li state_lb =>
match remove_component_aux state_lc p id with
| updated_hierarchy =>
Some (Component state_id state_p state_class state_cl updated_hierarchy state_li state_lb)
end
end.
Function add_interface_in_component (c:component) (int: interface) : component :=
match c with
| Component id p ic cl lc li lb => Component id p ic cl lc (int::li) lb
end.
Function add_interface_aux (comp_list:list component) (p:path) (int: interface) {struct p} : list component :=
match p with
| nil => nil
| c_id :: nil =>
let x := lookup comp_list c_id in
match x with
| None => nil
| Some (c, r) =>
let c' := add_interface_in_component c int in
(c' :: r)
end
| id :: r =>
let loo := lookup comp_list id in
match loo with
| None => nil
| Some (c', backup) =>
let x := add_interface_aux (c'->subComponents)%comp r int in
match x with
| nil => nil
| x' => ((update_sub_components c' x') :: backup)
end
end
end.
Definition add_interface (s:state) p int_id t a co f ct cd: option state :=
match s with
| Component state_id state_path state_class state_cl state_lc state_li state_lb =>
match add_interface_aux state_lc p (Interface int_id t p a co f ct cd) with
| nil => None
| updated_hierarchy => Some (Component state_id state_path state_class state_cl updated_hierarchy state_li state_lb)
end
end.
Function add_binding_in_component (c:component) (b: binding) : component :=
match c with
| Component id p ic cl lc li lb => Component id p ic cl lc li (b :: lb)
end.
Function add_binding_aux (lc:list component) (p:path) (b:binding)
{struct p} : (list component) :=
match p with
| nil => nil
| c_id :: nil =>
let x := lookup lc c_id in
match x with
| None => nil
| Some (c, r) =>
let c' := add_binding_in_component c b in
(c' :: r)
end
| id :: r =>
let loo := lookup lc id in
match loo with
| None => nil
| Some (c', backup) =>
let x := add_binding_aux (c'->subComponents)%comp r b in
match x with
| nil => nil
| x' => ((update_sub_components c' x') :: backup)
end
end
end.
Definition add_binding (s:state) b : option state :=
match s with
| Component i p ic cl state_lc li state_lb =>
match add_binding_aux state_lc (b->path%bind) b, (b->path%bind) with
| _, nil => Some (Component i p ic cl state_lc li (b :: state_lb))
| nil, _ => None
| updated_hierarchy, _ => Some (Component i p ic cl updated_hierarchy li state_lb)
end
end.
Function remove_binding_from_list (b:binding) (lb:list binding) {struct lb}: list binding :=
match lb with
nil => nil
| b' :: r => if beq_binding b b' then (remove_binding_from_list b r) else b' :: (remove_binding_from_list b r)
end.
Function remove_binding_from_component (c:component) (b:binding) : component :=
match c with
Component id p ic cl lc li lb => Component id p ic cl lc li (remove_binding_from_list b lb)
end.
Function remove_binding_aux (lc:list component) (p:path) (b:binding)
{struct p} : (list component) :=
match p with
| nil => nil
| c_id :: nil =>
let x := lookup lc c_id in
match x with
| None => nil
| Some (c, r) =>
let c' := remove_binding_from_component c b in
(c' :: r)
end
| id :: r =>
let loo := lookup lc id in
match loo with
| None => nil
| Some (c', backup) =>
let x := remove_binding_aux (c'->subComponents)%comp r b in
match x with
| nil => nil
| x' => ((update_sub_components c' x') :: backup)
end
end
end.
Definition remove_binding (s:state) (b:binding) : option state :=
match s with
| Component i p ic cl state_lc li state_lb =>
match (b->path%bind) with
nil => Some (Component i p ic cl state_lc li (remove_binding_from_list b state_lb))
| _ => Some (Component i p ic cl (remove_binding_aux state_lc (b->path%bind) b) li state_lb)
end
end.
match c with
| Component id p ic cl lc li lb => Component id p ic cl lc li (b :: lb)
end.
Function add_binding_aux (lc:list component) (p:path) (b:binding)
{struct p} : (list component) :=
match p with
| nil => nil
| c_id :: nil =>
let x := lookup lc c_id in
match x with
| None => nil
| Some (c, r) =>
let c' := add_binding_in_component c b in
(c' :: r)
end
| id :: r =>
let loo := lookup lc id in
match loo with
| None => nil
| Some (c', backup) =>
let x := add_binding_aux (c'->subComponents)%comp r b in
match x with
| nil => nil
| x' => ((update_sub_components c' x') :: backup)
end
end
end.
Definition add_binding (s:state) b : option state :=
match s with
| Component i p ic cl state_lc li state_lb =>
match add_binding_aux state_lc (b->path%bind) b, (b->path%bind) with
| _, nil => Some (Component i p ic cl state_lc li (b :: state_lb))
| nil, _ => None
| updated_hierarchy, _ => Some (Component i p ic cl updated_hierarchy li state_lb)
end
end.
Function remove_binding_from_list (b:binding) (lb:list binding) {struct lb}: list binding :=
match lb with
nil => nil
| b' :: r => if beq_binding b b' then (remove_binding_from_list b r) else b' :: (remove_binding_from_list b r)
end.
Function remove_binding_from_component (c:component) (b:binding) : component :=
match c with
Component id p ic cl lc li lb => Component id p ic cl lc li (remove_binding_from_list b lb)
end.
Function remove_binding_aux (lc:list component) (p:path) (b:binding)
{struct p} : (list component) :=
match p with
| nil => nil
| c_id :: nil =>
let x := lookup lc c_id in
match x with
| None => nil
| Some (c, r) =>
let c' := remove_binding_from_component c b in
(c' :: r)
end
| id :: r =>
let loo := lookup lc id in
match loo with
| None => nil
| Some (c', backup) =>
let x := remove_binding_aux (c'->subComponents)%comp r b in
match x with
| nil => nil
| x' => ((update_sub_components c' x') :: backup)
end
end
end.
Definition remove_binding (s:state) (b:binding) : option state :=
match s with
| Component i p ic cl state_lc li state_lb =>
match (b->path%bind) with
nil => Some (Component i p ic cl state_lc li (remove_binding_from_list b state_lb))
| _ => Some (Component i p ic cl (remove_binding_aux state_lc (b->path%bind) b) li state_lb)
end
end.
Inductive valid_path (p:path) (lc:list component) : Prop :=
| Valid0 : p = nil ->
valid_path p lc
| ValidN : forall i r s',
p = i :: r ->
(exists c, In c lc -> (c->id%comp) = i) ->
lc[i] = Some s' ->
valid_path r (s'->subComponents%comp) ->
valid_path p lc.
Definition valid_component_path p (s:state) := valid_path p (s->components%st).
Inductive valid_interface_path' (p:path) (lc:list component) : Prop :=
| ValidInterfacePath_Base: forall id,
p = id :: nil ->
(exists c, lc[id] = Some c) ->
valid_interface_path' p lc
| ValidInterfacePath_Step: forall id r,
p = id :: r ->
(exists c, lc[id] = Some c /\
valid_interface_path' r (c->subComponents)%comp) ->
valid_interface_path' p lc.
Definition valid_interface_path p (s:state) := valid_interface_path' p (s->components%st).
Lemma nil_is_valid_path':
forall s, valid_path nil s.
Proof.
intro.
thus apply Valid0; reflexivity.
Qed.
Lemma nil_is_valid_path:
forall s, valid_component_path nil s.
Proof.
intros; apply nil_is_valid_path'.
Qed.
Hint Resolve nil_is_valid_path nil_is_valid_path'.
Definition binding_exists (b:binding) (s:state) : Prop :=
forall c, Some c = get_component_with_path (b->path)%bind s ->
exists b', In b' (c->bindings%comp) -> b' = b.
Definition no_id_clash id p s :=
forall scope, Some scope = get_scope p s ->
not_in_l id scope.
Function get_scope2 (p:path) (lc:list component) : option (list component) :=
match p with
| nil => Some lc
| _ => get_scope_aux p lc
end.
Definition no_id_clash' id p s :=
forall scope, Some scope = get_scope2 p s ->
not_in_l id scope.
Lemma no_id_clash_step:
forall id' id r r' lc c,
unique_ids lc ->
lookup lc id = Some (c, r') ->
no_id_clash' id' (id :: r) lc ->
no_id_clash' id' r (c->subComponents)%comp.
Proof.
intros.
unfold no_id_clash' in *; intros.
apply H1. clear H1.
unfold get_scope2 in *.
unfold get_scope_aux.
assert (lc[id] = Some c).
eauto.
unfold get_component_with_path_aux.
rewrite H1.
fold get_component_with_path_aux.
destruct r; auto.
rewrite H0; auto.
Qed.
Hint Resolve no_id_clash_step.
Inductive valid_component_binding' (b:binding) (p:path) lc : Prop :=
| ValidComponentBinding_Base: p = nil ->
valid_binding b lc nil ->
valid_component_binding' b p lc
| ValidComponentBinding_Step: (exists c,
Some c = get_component_with_path_aux p lc /\
valid_binding b (c->subComponents)%comp (c->interfaces)%comp) ->
valid_component_binding' (b:binding) p lc .
Definition valid_component_binding (b:binding) (s:state) : Prop :=
valid_component_binding' b (b->path)%bind (s->components)%st .
Definition no_id_acc_clash' id acc p lc :=
forall c, Some c = get_component_with_path_aux p lc ->
not_in_l_pairs id acc (c->interfaces)%comp.
Definition no_id_acc_clash id acc p s :=
forall c, Some c = get_component_with_path p s ->
not_in_l_pairs id acc (c->interfaces)%comp.
Lemma lookup_unique_ids_gen2:
forall lc id c r,
unique_ids lc ->
forall X, lookup_aux lc id X = Some (c, r) ->
unique_ids X ->
unique_ids (app lc X) ->
unique_ids (c::r).
Proof.
intros.
functional induction lookup_aux lc id X.
Case "1/3".
inversion H0.
Case "2/3".
inversion H0; subst; auto.
Case "3/3".
apply IHo; eauto; clear IHo.
Qed.
Lemma lookup_unique_ids_gen:
forall lc id c r,
well_formed_components lc ->
forall X, lookup_aux lc id X = Some (c, r) ->
well_formed_components X ->
well_formed_components (app lc X) ->
unique_ids (c::r).
Proof.
intros.
functional induction lookup_aux lc id X.
Case "1/3".
inversion H0.
Case "2/3".
inversion H0; subst.
clear H0.
inversion H2;auto.
Case "3/3".
apply IHo; eauto; clear IHo.
Qed.
Lemma lookup_unique_ids:
forall lc id c r,
well_formed_components lc ->
lookup lc id = Some (c, r) ->
unique_ids (c::r).
Proof.
intros.
unfold lookup in H0.
destruct lookup_unique_ids_gen with
(lc:=lc) (id:=id) (c:=c) (r:=r) (X:=nil:list component); auto.
assert (lc ++ nil = lc).
apply app_nil_r.
rewrite H1;auto.
inversion H1.
inversion H1; subst.
apply Unique_Step with (c:=c0) (r:=r0); auto.
Qed.
Hint Resolve lookup_unique_ids.
Lemma lookup_unique_ids_backup:
forall lc id c r,
well_formed_components lc ->
lookup lc id = Some (c, r) ->
unique_ids r.
Proof.
intros.
assert (unique_ids (c::r)).
eauto.
inversion H1; inversion H2; auto.
Qed.
Hint Resolve lookup_unique_ids_backup.
Lemma lookup_unique_ids_gen':
forall lc id c r,
well_formed_components lc ->
lookup lc id = Some (c, r) ->
not_in_l id r.
Proof.
intros.
assert (unique_ids (c::r)).
eauto.
inversion H1.
Case "List is Nil".
inversion H2.
Case "List is not Nil".
inversion H2; subst.
assert (c0->id%comp = id).
eauto.
rewrite <- H5; auto.
Qed.
Hint Resolve lookup_unique_ids lookup_unique_ids.
Lemma lookup_get_fact_gen':
forall lc id i c c' r X,
well_formed_components lc ->
lookup_aux lc id X = Some (c, r) ->
X = nil ->
lc[i] = Some c' ->
(c::r)[i] = Some c'.
Proof.
intros.
inversion H.
apply get_component_commutes_on_l with (l:=lc); eauto.
apply lookup_unique_ids_gen with (lc:=lc) (id:=id) (X:=X); subst; auto.
rewrite app_nil_r; auto.
Qed.
Lemma lookup_get_fact':
forall lc id i c c' r ,
lookup lc id = Some (c, r) ->
well_formed_components lc ->
lc[i] = Some c' ->
(c::r)[i] = Some c'.
Proof.
intros.
apply lookup_get_fact_gen' with (lc:=lc) (id:=id) (X:=nil); auto.
Qed.
Hint Resolve lookup_get_fact'.
Lemma valid_path_fact:
forall c p lc, Some c = get_component_with_path_aux p lc ->
valid_path p lc.
Proof.
intros.
functional induction get_component_with_path_aux p lc.
inversion H.
eapply ValidN; eauto.
inversion H.
apply ValidN with (i:=id) (r:=rp) (s':=c0); auto.
exists c0; intro; eauto.
eauto.
Qed.
Lemma well_formed_lookup_split:
forall id c lc backup,
well_formed_components lc ->
lookup lc id = Some (c, backup) ->
well_formed_components (c :: backup).
Proof.
intros.
assert (forall x, In x lc <-> In x (c :: backup)).
eauto.
inversion H.
split.
Case "Unique Ids".
destruct H1 with (x:=c).
assert (In c lc).
apply H5. left;auto.
assert (In c (c::backup)).
left;auto.
clear H4 H5.
inversion H.
apply lookup_unique_ids with (lc:=lc) (id:=id); auto.
Case "Well Formed Component".
intros.
apply H3; auto.
destruct H4; subst.
SCase "It is the Head of the list".
eauto.
SCase "It is in the tail of the list".
eauto.
Qed.
Hint Resolve well_formed_lookup_split.
Definition well_formed (s:state) : Prop :=
match s with
| Component id p ic cl lc li lb =>
id = Ident "Root" /\
p = root /\
ic = "null" /\
cl = Configuration /\
li = nil /\
well_formed_component (Component (Ident "Root") root ic Configuration lc nil lb)
end.
Lets start with something easy. We shall prove
that an empty state, i.e. without any components,
is indeed well formed.
Lemma empty_state_is_well_formed:
well_formed empty_state.
Proof.
firstorder.
apply WellFormedComponent; intros; firstorder.
Qed.
Hint Resolve empty_state_is_well_formed.
well_formed empty_state.
Proof.
firstorder.
apply WellFormedComponent; intros; firstorder.
Qed.
Hint Resolve empty_state_is_well_formed.
Inductive operation : Type :=
| Mk_component : ident -> path -> implementationClass -> controlLevel ->
list component -> list interface ->
list binding -> operation
| Rm_component : path -> ident -> operation
| Mk_interface : ident -> signature -> path -> visibility ->
role -> functionality -> contingency -> cardinality -> operation
| Mk_binding : binding -> operation
| Rm_binding : binding -> operation
| Seq : operation -> operation -> operation
| Done : operation.
Lemma operation_dec:
forall a a' : operation, {a = a'} + {a <> a'}.
Proof.
intros.
decide equality; decide equality.
apply component_dec.
Qed.
We need to define the precise meaning for each constructor of our
operation language defined above, i.e., a semantics. This is
defined as follows.
Inductive binding_exists' b s : Prop :=
| BindingExists_Root: (b->path)%bind = nil ->
(exists b', In b' (s->bindings%comp) -> b' = b) ->
binding_exists' b s
| BindingExists_Step: forall c,
Some c = get_component_with_path (b ->path)%bind s ->
(exists b', In b' (c->bindings%comp) -> b' = b) ->
binding_exists' b s.
Definition get_parent p (lc:list component) : option component :=
match p with
| nil => None
| _ => get_component_with_path_aux p lc
end.
Definition get_binding_client_id b : option ident :=
match b with
| Normal p idc1 idi1 idc2 idi2 => Some idc1
| Export p idInt1 idSubComp idInt2 => None
| Import p idInt1 idSubComp idInt2 => Some idSubComp
end.
Definition get_binding_server_id b : option ident :=
match b with
| Normal p idc1 idi1 idc2 idi2 => Some idc2
| Export p idInt1 idSubComp idInt2 => Some idSubComp
| Import p idInt1 idSubComp idInt2 => None
end.
Notation "b '->idcc'" := (get_binding_client_id b) (at level 80) : binding_scope.
Notation "b '->idcs'" := (get_binding_server_id b) (at level 80) : binding_scope.
Function no_interference b id : Prop :=
match (b->idcc)%bind, (b->idcs)%bind with
| None, None => True
| Some idC, Some idS =>
if (idC == id) ||
(idS == id) then False else True
| _, Some idS => if (idS == id) then False else True
| Some idC, _ => if (idC == id) then False else True
end.
Notation "b '~~' c" := (no_interference b c) (at level 80, right associativity) : binding_scope.
Definition not_binded id lb :=
forall b, In b lb -> no_interference b id.
Inductive component_is_not_connected' (p:path) (id:ident) lc : Prop :=
| NotConnected_Step: p <> nil ->
(forall c,
Some c = get_parent p lc ->
not_binded id (c->bindings%comp)) ->
component_is_not_connected' p id lc.
Definition component_is_not_connected p id (s:state) : Prop :=
match p with
nil => not_binded id (s->bindings%st)
| _ => component_is_not_connected' p id (s->components%st)
end.
Definition binding_is_not_a_duplicate b s :=
match (b->path%bind) with
nil => ~ In b (s->bindings%st)
| _ => match get_component_with_path_aux (b->path%bind) (s->components%st) with
None => True
| Some c => ~ In b (c->bindings%comp)
end
end.
Notation "a1 ; a2" := (Seq a1 a2) (at level 80, right associativity).
Reserved Notation "a '/' s '~~~>' a' '/' s'" (at level 40, s at level 39, a' at level 39).
Inductive step : (operation * state) -> (operation * state) -> Prop :=
| SSeq1: forall a1 a1' a2 s s',
a1 / s ~~~> a1' / s' ->
(a1;a2) / s ~~~> (a1';a2) / s'
| SSeqFinish: forall s a2,
(Done;a2) / s ~~~> a2 / s
| SSeq2: forall a1 a2 s s',
a1 / s ~~~> Done / s' ->
(a1 ; a2) / s ~~~> a2 / s'
| SDoneRefl: forall s, Done / s ~~~> Done / s
| SMakeComponent: forall (id:ident) (ic:implementationClass) (cl:controlLevel) (lc: list component)
(li: list interface) (lb: list binding) (s:state) (p:path) (s':state),
valid_component_path p s ->
well_formed_component (Component id p ic cl lc li lb) ->
no_id_clash id p s ->
Some s' = add_component s p id ic cl lc li lb ->
Mk_component id p ic cl lc li lb / s ~~~> Done / s'
| SRemoveComponent: forall (p:path) (id:ident) (s s':state),
valid_component_path p s ->
component_is_not_connected p id s ->
Some s' = remove_component s p id ->
Rm_component p id / s ~~~> Done / s'
| SMakeInterface: forall (id:ident) (sig:signature) (acc:visibility)
(co:role) (f:functionality) (ct:contingency)
(cd:cardinality)
(s:state) (p:path) (s':state),
valid_interface_path p s ->
no_id_acc_clash id acc p s ->
Some s' = add_interface s p id sig acc co f ct cd ->
Mk_interface id sig p acc co f ct cd / s ~~~> Done / s'
| SMakeBinding : forall b (s s':state),
valid_component_binding b s ->
binding_is_not_a_duplicate b s ->
Some s' = add_binding s b ->
Mk_binding b / s ~~~> Done / s'
| SRemoveBinding : forall b (s s':state),
valid_component_binding b s ->
Some s' = remove_binding s b ->
Rm_binding b / s ~~~> Done / s'
where "a '/' s '~~~>' a' '/' s'" := (step (a,s) (a',s')).
Hint Constructors step.
So far, we defined our formal model of the GCM Component Model, and a semantics
for an operation language allowing to build GCM Architectures.
The defined semantics rigorously stipulates how each operation construct
can behave, making each transition between states without
Definition relation (X:Type) := X -> X -> Prop.
Set Implicit Arguments.
Inductive refl_step_closure (X:Type) (R: relation X) (x:X) : X -> Prop :=
| rsc_base : refl_step_closure R x x
| rsc_step : forall (y z : X),
R x y ->
refl_step_closure R y z ->
refl_step_closure R x z.
Hint Constructors refl_step_closure.
Notation " operation '/' s '~~~>*' operation' '/' s' " :=
(refl_step_closure step (operation,s) (operation',s'))
(at level 40, s at level 39, operation' at level 39, s' at level 39).
Lemma valid_component_binding_has_valid_component_path:
forall b s, valid_component_binding b s ->
valid_component_path (b->path)%bind s.
Proof.
intros.
inversion H.
Case "Path is nil".
rewrite H0.
unfold valid_component_path.
apply Valid0; auto.
Case "Path is not Nil".
unfold valid_component_path.
destruct H0 as (x, (H2, H3)).
functional induction get_component_with_path_aux (b->path%bind) (s->components%st); auto.
eapply ValidN; eauto.
congruence.
assert (valid_path rp (c ->subComponents)%comp); auto.
eapply ValidN; eauto.
Qed.
Lets begin by proving an intuitive fact about the transitive
closure: if I can go there in one step, then it means I can
go there in n steps
Lemma one_step_entails_n_steps:
forall a a' s s',
a / s ~~~> a' / s' ->
a / s ~~~>* a' / s'.
Proof.
intros.
eapply rsc_step; eauto.
Qed.
Hint Resolve one_step_entails_n_steps.
Definition is_normal_form a := a = Done.
Definition is_one_step_from_normal_form a :=
match a with
Mk_component _ _ _ _ _ _ _ => True
| Rm_component _ _ => True
| Mk_interface _ _ _ _ _ _ _ _ => True
| Mk_binding _ => True
| Rm_binding _ => True
| _ => False
end.
Definition is_seq a :=
match a with
Seq _ _ => True
| _ => False
end.
Lemma seq_fact:
forall a s a' s',
a / s ~~~> a' / s' ->
is_one_step_from_normal_form a ->
is_normal_form a'.
Proof.
intros.
induction a;
try thus (inversion H; subst; refl).
inversion H0.
Qed.
Lemma seq_lemma:
forall x x' d,
(refl_step_closure step x x') ->
(fst x ; d) / (snd x) ~~~>* (fst x' ; d) / (snd x').
Proof.
intros. induction H.
apply rsc_base.
apply rsc_step with (fst y;d, snd y); auto.
apply SSeq1;auto.
destruct x; destruct y; auto.
Qed.
Hint Resolve seq_lemma.
Notation "r '*' '(' s ',' s' ')' " :=
(refl_step_closure r s s') (at level 40, s at next level, s' at next level).
Lemma rsc_trans:
forall (X : Type) (R : relation X) (x y z : X),
R* (x, y) -> R * (y, z) -> R * (x, z).
Proof.
intros. induction H; auto.
apply rsc_step with y; auto.
Qed.
Lemma op_sequence_reduction:
forall op1 op2 s s' s'',
op1 / s ~~~>* Done / s' ->
op2 / s' ~~~>* Done / s'' ->
(op1;op2) / s ~~~>* Done / s''.
Proof.
intros op1 op2 s s' s'' Hop1 Hop2.
inversion Hop1; subst.
Case "1/2".
eapply rsc_step; auto.
Case "2/2".
apply rsc_trans with (y:=(Done;op2, s')).
assert (Hseq := seq_lemma (x:=(op1, s)) (x':=(Done, s')) op2).
simpl in Hseq.
apply Hseq. exact Hop1.
apply rsc_trans with (y:=(op2, s')).
apply rsc_step with (y:=(op2, s')).
apply SSeqFinish.
apply rsc_base.
clear H H0.
inversion Hop2; subst.
eapply rsc_step; auto.
auto.
Qed.
Lemma seq_reduction_aux:
forall z z',
(refl_step_closure step z z') ->
forall c d,
(fst z) = (c;d) ->
fst z' = Done ->
(exists s', c / (snd z) ~~~>* Done / s' /\
d / s' ~~~>* Done / (snd z')).
Proof.
induction 1; intros; subst.
congruence.
destruct x as (x,s).
simpl in *. subst x.
inversion H; subst; auto.
Case "1/3".
elim (IHrefl_step_closure a1' d); auto.
intro x; simpl in *.
intros (H', H'').
exists x.
split; auto.
apply rsc_trans with (a1', s'); auto.
Case "2/3".
exists s; split; auto.
destruct z as (z, x); simpl in *; auto.
subst z; auto.
Case "3/3".
exists s'; split; auto.
destruct z; subst.
simpl in *; subst; auto.
Qed.
Lemma sequence_completion_gen:
forall a1 a2 s s'',
(a1; a2) / s ~~~>* Done / s'' ->
exists s', a1 / s ~~~>* Done / s' /\
a2 / s' ~~~>* Done / s''.
Proof.
intros.
destruct seq_reduction_aux with
(z:=((a1; a2), s)) (z':=(Done, s''))
(c:=a1) (d:=a2); auto.
destruct H0.
exists x; split ;auto.
Qed.
Hint Resolve one_step_entails_n_steps.
Lemma done_is_quiet':
forall x y, fst x = Done -> fst y = Done ->
(refl_step_closure step x y) ->
snd x = snd y.
Proof.
intros.
induction H1. auto.
destruct x; destruct y; destruct z.
simpl in *; subst.
inversion H1; subst.
apply IHrefl_step_closure; auto.
Qed.
Lemma done_is_quiet:
forall s s', Done / s ~~~>* Done / s' -> s = s'.
Proof.
intros.
assert (snd (Done, s) = snd (Done, s')).
apply done_is_quiet'; auto.
simpl in H0; auto.
Qed.
Hint Resolve done_is_quiet.
forall a a' s s',
a / s ~~~> a' / s' ->
a / s ~~~>* a' / s'.
Proof.
intros.
eapply rsc_step; eauto.
Qed.
Hint Resolve one_step_entails_n_steps.
Definition is_normal_form a := a = Done.
Definition is_one_step_from_normal_form a :=
match a with
Mk_component _ _ _ _ _ _ _ => True
| Rm_component _ _ => True
| Mk_interface _ _ _ _ _ _ _ _ => True
| Mk_binding _ => True
| Rm_binding _ => True
| _ => False
end.
Definition is_seq a :=
match a with
Seq _ _ => True
| _ => False
end.
Lemma seq_fact:
forall a s a' s',
a / s ~~~> a' / s' ->
is_one_step_from_normal_form a ->
is_normal_form a'.
Proof.
intros.
induction a;
try thus (inversion H; subst; refl).
inversion H0.
Qed.
Lemma seq_lemma:
forall x x' d,
(refl_step_closure step x x') ->
(fst x ; d) / (snd x) ~~~>* (fst x' ; d) / (snd x').
Proof.
intros. induction H.
apply rsc_base.
apply rsc_step with (fst y;d, snd y); auto.
apply SSeq1;auto.
destruct x; destruct y; auto.
Qed.
Hint Resolve seq_lemma.
Notation "r '*' '(' s ',' s' ')' " :=
(refl_step_closure r s s') (at level 40, s at next level, s' at next level).
Lemma rsc_trans:
forall (X : Type) (R : relation X) (x y z : X),
R* (x, y) -> R * (y, z) -> R * (x, z).
Proof.
intros. induction H; auto.
apply rsc_step with y; auto.
Qed.
Lemma op_sequence_reduction:
forall op1 op2 s s' s'',
op1 / s ~~~>* Done / s' ->
op2 / s' ~~~>* Done / s'' ->
(op1;op2) / s ~~~>* Done / s''.
Proof.
intros op1 op2 s s' s'' Hop1 Hop2.
inversion Hop1; subst.
Case "1/2".
eapply rsc_step; auto.
Case "2/2".
apply rsc_trans with (y:=(Done;op2, s')).
assert (Hseq := seq_lemma (x:=(op1, s)) (x':=(Done, s')) op2).
simpl in Hseq.
apply Hseq. exact Hop1.
apply rsc_trans with (y:=(op2, s')).
apply rsc_step with (y:=(op2, s')).
apply SSeqFinish.
apply rsc_base.
clear H H0.
inversion Hop2; subst.
eapply rsc_step; auto.
auto.
Qed.
Lemma seq_reduction_aux:
forall z z',
(refl_step_closure step z z') ->
forall c d,
(fst z) = (c;d) ->
fst z' = Done ->
(exists s', c / (snd z) ~~~>* Done / s' /\
d / s' ~~~>* Done / (snd z')).
Proof.
induction 1; intros; subst.
congruence.
destruct x as (x,s).
simpl in *. subst x.
inversion H; subst; auto.
Case "1/3".
elim (IHrefl_step_closure a1' d); auto.
intro x; simpl in *.
intros (H', H'').
exists x.
split; auto.
apply rsc_trans with (a1', s'); auto.
Case "2/3".
exists s; split; auto.
destruct z as (z, x); simpl in *; auto.
subst z; auto.
Case "3/3".
exists s'; split; auto.
destruct z; subst.
simpl in *; subst; auto.
Qed.
Lemma sequence_completion_gen:
forall a1 a2 s s'',
(a1; a2) / s ~~~>* Done / s'' ->
exists s', a1 / s ~~~>* Done / s' /\
a2 / s' ~~~>* Done / s''.
Proof.
intros.
destruct seq_reduction_aux with
(z:=((a1; a2), s)) (z':=(Done, s''))
(c:=a1) (d:=a2); auto.
destruct H0.
exists x; split ;auto.
Qed.
Hint Resolve one_step_entails_n_steps.
Lemma done_is_quiet':
forall x y, fst x = Done -> fst y = Done ->
(refl_step_closure step x y) ->
snd x = snd y.
Proof.
intros.
induction H1. auto.
destruct x; destruct y; destruct z.
simpl in *; subst.
inversion H1; subst.
apply IHrefl_step_closure; auto.
Qed.
Lemma done_is_quiet:
forall s s', Done / s ~~~>* Done / s' -> s = s'.
Proof.
intros.
assert (snd (Done, s) = snd (Done, s')).
apply done_is_quiet'; auto.
simpl in H0; auto.
Qed.
Hint Resolve done_is_quiet.