Mefresa.Dec.Eval

Evaluation for Well Formed and Well Typed Architectures

Here we build our sound and complete decision procedure for well formed and well typed architectures.

Require Import Mefresa.Operation.Compliance.
Require Import Mefresa.Operation.Reductions.
Require Import Mefresa.Dec.WellFormednessDecidability.
Require Import Mefresa.Dec.WellTypedDecidability.

Require Import Coq.Bool.Bool.

Running our 'Programs': Reducing Operations to Done

Being able to decide whether a state is well_formed gives us the ability to refuse non-compliant GCM architectures statically. However, we stil need to reduce operations in order to obtain our state structure. As such, we also need to do some work at the operation level.
Let us start by defining an ErrorState that is provably ill_formed.
As we procedeed for the component's and state's decision procedure we shall also define computational counterparts of the involved predicates.

Function valid_component_path_bool (p:path) (s:component) : bool :=
  match p with
    nil => true
  | id :: r => match (s->subComponents%comp)[id] with
                 None => false
               | Some c => valid_component_path_bool r c
               end
  end.

Lemma valid_component_path_bool_correctness:
  forall p s, valid_component_path_bool p s = true <-> valid_component_path p s.
Proof.
  split; intro.
  Case "Function Entails Predicate".
    functional induction valid_component_path_bool p s; auto;
    try congruence.
    assert (valid_component_path r c); auto.
    clear IHb.
    unfold valid_component_path.
    apply ValidN with (i:=id) (r:=r) (s':=c); auto.
    exists c; intro; eauto.
  Case "Predicate Entails Function".
    functional induction valid_component_path_bool p s; auto.
    SCase "1/2".
      inversion H; inversion H0; subst. clear H0.
      clear -H2 e0.
      destruct s; simpl in *.
      congruence.
    SCase "2/2".
      apply IHb. clear IHb.
      unfold valid_component_path in *.
      inversion H; inversion H0; subst. clear H0.
      assert (c = s').
        clear -H2 e0.
        replace (s->components)%st with (s->subComponents%comp) in H2; auto.
        functional induction ((s ->subComponents)%comp [i]); try congruence.
      subst; auto.
Qed.

Hint Resolve valid_component_path_bool_correctness.

Function no_id_clash_bool id p s : bool :=
  match get_scope p s with
    None => true
  | Some lc => not_in_bool id lc
  end.

Lemma no_id_clash_bool_correctness:
  forall id p s, no_id_clash_bool id p s = true <-> no_id_clash id p s.
Proof.
  split; intro.
  Case "Function Entails Predicate".
    Focus.
    functional induction no_id_clash_bool id p s; try congruence.
    unfold no_id_clash; intros.
    assert (scope = lc).
      destruct (get_scope p s); inversion e; auto.
      inversion H0; auto.
    subst; apply not_in_bool_correctness; auto.
  Case "Predicate Entails Function".
    unfold no_id_clash_bool.
    unfold no_id_clash in H.
    destruct (get_scope p s); auto.
    assert (not_in_l id l); auto.
    apply not_in_bool_correctness; auto.
Qed.

Hint Resolve no_id_clash_bool_correctness.

Function no_interference_bool b id : bool :=
  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.

Lemma no_interference_bool_correctness:
  forall b id, no_interference_bool b id = true <-> no_interference b id.
Proof.
  intros.
  split; intro.
  Case "Function Entails Predicate". Focus.
    unfold no_interference;
    unfold no_interference_bool in H.
    destruct (b->idcc)%bind;
    destruct (b ->idcs)%bind; auto.
    SCase "1/3".
      destruct ((i == id) || (i0 == id)); [congruence | auto].
    SCase "2/3".
      destruct (i == id); [congruence | auto].
    SCase "3/3".
      destruct (i == id); [congruence | auto].
  Case "Predicate Entails Function".
    unfold no_interference_bool;
    unfold no_interference in H.
    destruct (b->idcc)%bind;
    destruct (b ->idcs)%bind; auto.
     SCase "1/3".
      destruct ((i == id) || (i0 == id)); [fromfalse | auto].
    SCase "2/3".
      destruct (i == id); [fromfalse | auto].
    SCase "3/3".
      destruct (i == id); [fromfalse | auto].
Qed.

Function not_binded_bool id lb : bool :=
  match lb with
    nil => true
  | b :: r => if no_interference_bool b id then not_binded_bool id r else false
  end.

Lemma not_binded_bool_correctness:
  forall id lb, not_binded_bool id lb = true <-> not_binded id lb.
Proof.
  intros.
  split; intro.
  Case "Function Entails Predicate".
    unfold not_binded_bool in H;
    unfold not_binded.
    intros.
    apply no_interference_bool_correctness.
    induction lb. inversion H0.
    inversion H0; subst; clear H0.
    destruct (no_interference_bool b id ); auto.
    destruct (no_interference_bool a id).
    apply IHlb; auto.
    congruence.
  Case "Predicate Entails Function".
    unfold not_binded_bool;
    unfold not_binded in H.
    induction lb; auto.
    assert (no_interference a id).
      apply H; left; auto.
    rewrite <- no_interference_bool_correctness in H0.
    destruct (no_interference_bool a id).
    apply IHlb; intros.
    apply H. right; auto.
    congruence.
Qed.

Function get_component_with_given_path (p : path) (lc : list component) {struct p} :
  option component :=
  match p with
  | nil => None
  | i :: nil => lc [i]
  | i :: (_ :: _) as rp =>
      match lc [i] with
      | Some c => get_component_with_given_path rp (c ->subComponents)%comp
      | None => None
      end
  end.

Lemma get_component_path_eq:
  forall p lc, get_component_with_given_path p lc =
               get_component_with_path_aux p lc.
Proof.
  induction p; intros; simpl; auto.
  destruct p; auto.
  assert ((forall c r, lookup lc a = Some (c, r) -> lc [a] = Some c) /\
                      (forall acc, lookup_aux lc a acc = None -> lc [a] = None) ).
    split.
    apply lookup_get_comp.
    intros.
    clear -H.
    functional induction lookup_aux lc a acc; auto.
    congruence.
    simpl.
    rewrite e0.
    apply IHo;auto.
  destruct H.
  unfold lookup in *.
  assert ( (lookup_aux lc a nil = None -> lc [a] = None)).
    apply H0; auto.
  destruct (lc [a]);
  destruct (lookup_aux lc a nil); auto.
  Case "1/3 Both Found it". Focus.
    destruct p0 as (c0, r).
    assert (Some c = Some c0).
      apply (H c0 r); auto.
    inversion H2; subst; auto.
  Case "2/3 Found it, Not Found".
    assert (Some c = None); auto.
    congruence.
  Case "3/3".
    destruct p0.
    assert (None = Some c).
      apply (H c l); auto.
    congruence.
Qed.

Function get_parent_component (p : list ident) (lc : list component) :=
  match p with
    | nil => None
    | _ :: _ => get_component_with_given_path p lc
  end.

Lemma get_parent_eq:
  forall p lc, get_parent_component p lc = get_parent p lc.
Proof.
  induction p; intros.
  simpl. auto.
  unfold get_parent_component.
  unfold get_parent.
  apply get_component_path_eq.
Qed.

Function component_is_not_connected_bool_aux (p:path) (id:ident) lc : bool :=
  match get_parent_component p lc with
    None => false
  | Some c => not_binded_bool id (c->bindings%comp)
  end.

Function component_is_not_connected_bool (p : list ident) (id : ident) (s : state) : bool :=
  match p with
    nil => not_binded_bool id (s ->bindings)%st
    | _ :: _ => component_is_not_connected_bool_aux p id (s ->components)%st
  end.

Lemma component_is_not_connected_bool_soundness:
  forall p id s, component_is_not_connected_bool p id s = true ->
                 component_is_not_connected p id s.
Proof.
  intros.
  Case "Function Entails Predicate".
    unfold component_is_not_connected;
    unfold component_is_not_connected_bool in H.
    destruct p.
    SCase "Path is nil".
      apply not_binded_bool_correctness; auto.
    SCase "Path is not nil".
      apply NotConnected_Step.
      discriminate.
      intros.
      unfold component_is_not_connected_bool_aux in H.
      rewrite get_parent_eq in H.
      rewrite <- H0 in H.
      apply not_binded_bool_correctness; auto.
Qed.

Lemma valid_path_fact':
forall (p : path) s,
       p <> nil ->
       valid_component_path p s ->
       exists c, Some c = get_component_with_path p s.
Proof.
  induction p; intros.
  congruence.
  inversion H0; inversion H1; subst. clear H1 H H0.
  destruct r. clear IHp.
  simpl. exists s'. destruct s. simpl in *; auto.
  assert (exists c, Some c = get_component_with_path (i0 :: r) s').
    apply IHp.
    discriminate.
    eauto.
  clear IHp.
  destruct H.
  exists x.
  unfold get_component_with_path.
  destruct s.
  rewrite <- get_component_path_eq.
  unfold get_component_with_given_path.
  simpl in H3.
  rewrite H3.
  fold get_component_with_given_path.
  clear -H.
  unfold get_component_with_path in H.
  destruct s'.
  rewrite <- get_component_path_eq in H.
  simpl.
  exact H.
Qed.

Lemma component_is_not_connected_bool_completeness:
  forall p id s, valid_component_path p s ->
                 component_is_not_connected p id s ->
                 component_is_not_connected_bool p id s = true.
Proof.
  intros.
  unfold component_is_not_connected_bool;
  unfold component_is_not_connected in H0.
  destruct p.
  apply not_binded_bool_correctness; auto.
  unfold component_is_not_connected_bool_aux.
  rewrite get_parent_eq.
  inversion H0.
  clear H0.
  assert (get_parent (i :: p) (s ->components)%st <> None). Focus.
    inversion H; inversion H0; subst.
    clear H1 H0.
    unfold get_parent.
    destruct (valid_path_fact' (i0::r) s). discriminate.
    auto. unfold get_component_with_path in H0.
    destruct s.
    replace (Component i p i1 c l l0 l1 ->components)%st with l; auto.
    rewrite <- H0. discriminate.
  destruct (get_parent (i :: p) (s ->components)%st).
  apply not_binded_bool_correctness.
  apply H2; auto.
  congruence.
Qed.

Function valid_interface_path_bool p s : bool :=
  match p with
    nil => false
  | id :: nil => match (s->subComponents%comp)[id] with
                   None => false
                 | _ => true
                 end
  | id :: r => match (s->subComponents%comp)[id] with
                   None => false
                 | Some c => valid_interface_path_bool r c
                  end
  end.

Lemma valid_interface_path_bool_correctness:
  forall p s, valid_interface_path_bool p s = true <-> valid_interface_path p s.
Proof.
  split; intro.
  Case "Function Entails Predicate".
    functional induction valid_interface_path_bool p s; auto;
    try congruence.
    SCase "Just one Step".
      apply ValidInterfacePath_Base with (id:=id); auto.
      replace ((s ->components)%st) with (s ->subComponents)%comp; auto.
      destruct ((s ->subComponents)%comp [id]).
      exists c; auto.
      fromfalse.
    SCase "More than one Step".
      apply ValidInterfacePath_Step with (id:=id) (r:=r); auto.
      exists c.
      split; auto.
      apply IHb; auto.
  Case "Predicate Entails Function".
    unfold valid_interface_path in H.
    functional induction valid_interface_path_bool p s;
    try thus inversion H; inversion H0.
    SCase "1/3".
      inversion H; inversion H0; subst. clear H0.
      destruct H1.
      replace ((s ->components)%st) with ((s ->subComponents)%comp) in H0; auto.
      congruence.
      destruct H1. destruct H1.
      replace ((s ->components)%st) with ((s ->subComponents)%comp) in H1; auto.
      congruence.
    SCase "2/3".
      clear y.
      inversion H; inversion H0; subst. clear H0.
      destruct H1.
      replace ((s ->components)%st) with ((s ->subComponents)%comp) in H0; auto.
      congruence.
      destruct H1. destruct H1.
      replace ((s ->components)%st) with ((s ->subComponents)%comp) in H1; auto.
      congruence.
    SCase "3/3".
      apply IHb.
      clear IHb.
      inversion H; inversion H0; subst.
      inversion y.
      clear H0.
      destruct H1. destruct H0.
      assert (x = c).
        replace ((s ->components)%st) with ((s ->subComponents)%comp) in H0; auto.
        rewrite H0 in e0.
        inversion e0; auto.
      subst; auto.
Qed.

Lemma valid_interface_path_fact:
    forall p s, valid_interface_path p s ->
            get_component_with_path p s <> None.
Proof.
  intros.
  destruct s.
  unfold get_component_with_path.
  destruct p. inversion H; inversion H0.
  functional induction get_component_with_path_aux (i1::p) l.
  Case "1/4".
    inversion H; inversion H0.
  Case "2/4".
    inversion H; inversion H0; subst. clear H0.
    destruct H1.
    simpl in H0.
    rewrite H0. discriminate.
    clear H0.
    destruct H1. destruct H0.
    simpl in H0.
    rewrite H0. discriminate.
  Case "3/4".
    clear -e0 H Case.
    inversion H; inversion H0; subst. clear H0.
    destruct H1.
    simpl in H0.
    assert (forall acc, (lookup_aux li id0 acc = None -> li [id0] = None)). Focus.
      intros.
      clear -H1 Case.
      functional induction lookup_aux li id0 acc; auto.
      congruence.
      simpl.
      rewrite e0.
      apply IHo;auto.
    assert (li [id0] = None).
      apply (H1 nil); auto.
    congruence.
    inversion H; inversion H0; subst. clear H0.
    destruct H1.
    destruct H0.
    simpl in H0.
    assert (forall acc, (lookup_aux li id0 acc = None -> li [id0] = None)).
      intros.
      clear -H4 Case.
      functional induction lookup_aux li id0 acc; auto.
      congruence.
      simpl.
      rewrite e0.
      apply IHo;auto.
    assert (li [id0] = None).
      apply (H4 nil); auto.
    congruence.
    destruct H1.
    destruct H1.
    simpl in H1.
    assert (forall acc, (lookup_aux li id0 acc = None -> li [id0] = None)).
      intros.
      clear -H5 Case.
      functional induction lookup_aux li id0 acc; auto.
      congruence.
      simpl.
      rewrite e0.
      apply IHo;auto.
    assert (li [id0] = None).
      apply (H5 nil); auto.
    congruence.
  Case "4/4".
    apply IHo.
    clear IHo.
    inversion H; inversion H0; subst.
    fromfalse.
    clear H0.
    destruct H1. destruct H0.
    simpl in *.
     assert ((forall c r, lookup li id0 = Some (c, r) -> li [id0] = Some c)).
       apply lookup_get_comp.
     assert (li [id0] = Some c0).
       apply (H2 c0 r); auto.
     rewrite H0 in H3.
     inversion H3; subst; auto.
Qed.

Function no_id_acc_clash_bool id acc p s : bool :=
  match get_component_with_path p s with
    None => false
  | Some c => not_in_l_pairs_bool id acc (c->interfaces%comp)
  end.

Lemma no_id_acc_clash_bool_soundness:
  forall id acc p s,
    no_id_acc_clash_bool id acc p s = true -> no_id_acc_clash id acc p s.
Proof.
  intros.
  unfold no_id_acc_clash_bool in H.
  intro. intros.
  rewrite <- H0 in H.
  apply not_in_l_pairs_bool_correctness; auto.
Qed.

Lemma no_id_acc_clash_bool_completeness:
  forall id acc p s,
    valid_interface_path p s ->
    no_id_acc_clash id acc p s -> no_id_acc_clash_bool id acc p s = true.
Proof.
  intros.
  destruct s.
  unfold no_id_acc_clash_bool.
  unfold no_id_acc_clash in *.
  assert (get_component_with_path p (Component i p0 i0 c l l0 l1) <> None).
    apply valid_interface_path_fact; auto.
  destruct (get_component_with_path p (Component i p0 i0 c l l0 l1)); try congruence.
  apply not_in_l_pairs_bool_correctness.
  apply H0; auto.
Qed.

Function valid_component_binding_bool b s : bool :=
  match (b->path%bind) with
    nil => valid_binding_bool b (s->components%st) nil
  | _ => match get_component_with_path_aux (b->path%bind) (s->components%st) with
             None => false
           | Some c => valid_binding_bool b (c->subComponents%comp) (c ->interfaces)%comp
           end
  end.

Lemma valid_component_binding_bool_correctness:
  forall b s,
    valid_component_binding_bool b s = true <-> valid_component_binding b s.
Proof.
  split; intros.
  Case "Function Entails Predicate".
    unfold valid_component_binding.
    unfold valid_component_binding_bool in H.
    destruct ((b ->path)%bind).
    SCase "Path is nil".
      apply ValidComponentBinding_Base; auto.
      apply valid_bindings_correctness; auto.
    SCase "Path is not nil".
      apply ValidComponentBinding_Step.
      destruct (get_component_with_path_aux (i :: p) (s ->components)%st).
      SSCase "1/2".
        exists c.
        split; auto.
        apply valid_bindings_correctness; auto.
      SSCase "2/2".
        congruence.
  Case "Predicate Entails Function".
    unfold valid_component_binding in H.
    unfold valid_component_binding_bool.
    destruct ((b ->path)%bind ).
    SCase "Path is Nil".
      inversion H.
      apply valid_bindings_correctness; auto.
      destruct H0 as (x, (H1, H2)).
      simpl in H1. congruence.
    SCase "Path is not Nil".
      inversion H; subst. congruence.
      destruct H0 as (x, (H1, H2)).
      rewrite <- H1.
      apply valid_bindings_correctness; auto.
Qed.

Function binding_exists (b:binding) lb : bool :=
  match lb with
    nil => false
  | b' :: r => if (b' == b)%bind then true else binding_exists b r
  end.

Lemma binding_exists_correctness:
  forall b lb, binding_exists b lb = true <-> In b lb.
Proof.
  split;intros.
  Case "Function Entails Predicate". Focus.
    induction lb; simpl in *.
    congruence.
    assert ((a == b)%bind=true -> a=b).
      intro; eauto.
    destruct ((a == b)%bind).
    left; auto.
    right; auto.
  Case "Predicate Entails Function".
     induction lb. inversion H.
     assert ({b=a} + {b<>a}).
       repeat decide equality.
     destruct H0; subst.
     SCase "They are Equal".
       assert (a=a->(a == a)%bind=true).
           intro; auto.
       destruct H.
       SSCase "Is the Head of the list".
         simpl.
         rewrite H0; simpl; auto.
       SSCase "In the Tail of the List".
         simpl.
         rewrite H0; simpl; auto.
    SCase "They are not Equal".
      destruct H; subst.
      SSCase "Head of the List".
        congruence.
      SSCase "In the Tail of the List".
        simpl.
        replace ((a == b)%bind) with false.
        apply IHlb; auto.
        assert ((a == b)%bind=true -> b=a).
          intro; symmetry; auto.
        destruct ((a == b)%bind); auto.
Qed.

Function binding_is_not_a_duplicate_bool b s : bool :=
  match (b ->path)%bind with
    | nil => negb (binding_exists b (s ->bindings)%st)
    | _ :: _ =>
      match get_component_with_path_aux (b ->path)%bind (s ->components)%st with
        | Some c => negb (binding_exists b (c ->bindings)%st)
        | None => true
      end
end.

Lemma binding_is_not_a_duplicate_bool_correctness:
  forall b s,
    binding_is_not_a_duplicate_bool b s = true <-> binding_is_not_a_duplicate b s.
Proof.
  split; intros.
  Case "Function Entails Predicate".
    unfold binding_is_not_a_duplicate_bool in H;
    unfold binding_is_not_a_duplicate.
    destruct ((b ->path)%bind).
    SCase "Path is Nil".
      destruct (binding_exists_correctness b (s ->bindings)%st).
      destruct ((binding_exists b (s ->bindings)%st)).
      simpl in H. congruence.
      intro.
      assert (false=true); auto.
      congruence.
    SCase "Path is not Nil".
      destruct (get_component_with_path_aux (i :: p) (s ->components)%st); auto.
      intro.
      replace (c ->bindings)%st with (c ->bindings)%comp in * ;auto.
      destruct (binding_exists_correctness b (c ->bindings)%comp).
      assert (binding_exists b (c ->bindings)%comp = true); auto.
      destruct (binding_exists b (c ->bindings)%comp);
      simpl in H; congruence.
  Case "Predicate Entails Function".
    unfold binding_is_not_a_duplicate_bool;
    unfold binding_is_not_a_duplicate in H.
    destruct ((b ->path)%bind).
    SCase "Path is Nil".
      destruct (binding_exists_correctness b (s ->bindings)%st).
      destruct ((binding_exists b (s ->bindings)%st)); simpl; auto.
    SCase "Path is not Nil".
      destruct (get_component_with_path_aux (i :: p) (s ->components)%st ); auto.
      replace (c ->bindings)%st with (c ->bindings)%comp in * ;auto.
      destruct (binding_exists_correctness b (c ->bindings)%comp).
      destruct ((binding_exists b (c ->bindings)%comp)); simpl; auto.
Qed.

Function build_state (op:operation) (init:state) : option state :=
  match op with
    | Mk_component i p ic cl lc li lb =>
              if beq_bool ( valid_component_path_bool p init &&
                            no_id_clash_bool i p init &&
                            dec_component (Component i p ic cl lc li lb)) false then
                    None
              else
                    add_component init p i ic cl lc li lb

    | Rm_component p i =>
              if beq_bool ( valid_component_path_bool p init &&
                            component_is_not_connected_bool p i init ) false then
                    None
              else
                    remove_component init p i
     
    | Mk_interface i sign p a c f ct cd =>
          if beq_bool ( valid_interface_path_bool p init &&
                            no_id_acc_clash_bool i a p init ) false then
                    None
              else
                    add_interface init p i sign a c f ct cd

    | Mk_binding b =>

          if beq_bool ( valid_component_binding_bool b init &&
                        binding_is_not_a_duplicate_bool b init ) false then
                    None
              else
                    add_binding init b

    | Rm_binding b =>
           if beq_bool ( valid_component_binding_bool b init ) false then
                    None
              else
                    remove_binding init b

    | Seq a1 a2 =>
       let s := build_state a1 init in
       match s with
         | None => None
         | Some s => build_state a2 s
       end
    | Done => Some init
  end.
A simple shorthand
Definition eval op := build_state op empty_state.

Lemma build_state_fact:
  forall op1 op2 s s',
                  forall conf, conf = (op1; op2) ->
                  build_state conf s = Some s' ->
                  exists x, build_state op1 s = Some x /\
                            build_state op2 x = Some s'.
Proof.
  intros op1 op2 s s' conf Hc Hb.
  functional induction build_state conf s; try congruence.
  clear IHo IHo0.
  inversion Hc; subst.
  clear Hc.
  exists s0.
  split; auto.
Qed.

Lemma build_state_fact':
    forall op1 s x op2 s',
      build_state op1 s = Some x ->
      well_formed x ->
      build_state op2 x = Some s' ->
      build_state (op1; op2) s = Some s'.
Proof.
  intros.
  simpl.
  rewrite H; auto.
Qed.

Lemma seq_fact':
    forall op1 s s' op2,
    (refl_step_closure step (op1, s) (Done, s')) ->
    (op1 ; op2) / s ~~~>* (Done ; op2) / s'.
Proof.
  intros.
  assert (forall x x' d,
    (refl_step_closure step x x') ->
    (fst x ; d) / (snd x) ~~~>* (fst x' ; d) / (snd x')).
    auto.
  assert (step * ((fst (op1, s); op2, snd (op1, s)), (fst (Done, s'); op2, snd (Done, s')))).
    apply H0; auto.
  simpl in H1.
  exact H1.
Qed.

Theorem build_state_soundness:
  forall op s s',
    build_state op s = Some s' -> op / s ~~~>* Done / s'.
Proof.
  induction op; intros.
   Case "Function Entails Predicate".
    SCase "Making Components". Focus.
      eapply rsc_step; eauto.
      unfold build_state in H.
      apply SMakeComponent.
      SSCase "Valid Path".
        apply valid_component_path_bool_correctness.
        destruct (valid_component_path_bool p s); auto.
        simpl in H. congruence.
      SSCase "Well Formed Component".
        apply dec_component_correctness.
        destruct (dec_component (Component i p i0 c l l0 l1)); auto.
        rewrite andb_false_r in H.
        simpl in H.
        congruence.
      SSCase "No id Clash".
        apply no_id_clash_bool_correctness.
        destruct (no_id_clash_bool i p s); auto.
        rewrite andb_false_r in H.
        simpl in H.
        congruence.
      SSCase "add component function".
        destruct ((valid_component_path_bool p s && no_id_clash_bool i p s &&
                   dec_component (Component i p i0 c l l0 l1)) );
        simpl in H.
        SSSCase "True Branch".
          destruct (add_component s p i i0 c l l0 l1); subst; auto.
        SSSCase "False Branch".
         congruence.
    SCase "Removing Components".
      Focus.
      eapply rsc_step; eauto.
      unfold build_state in H.
      apply SRemoveComponent.
      SSCase "Valid Path".
        apply valid_component_path_bool_correctness.
        destruct (valid_component_path_bool p s); auto.
        simpl in H.
        congruence.
      SSCase "Component is not Connected".
        apply component_is_not_connected_bool_soundness.
        destruct (valid_component_path_bool p s);
        try thus simpl in H; congruence.
        destruct (component_is_not_connected_bool p i s); auto.
        simpl in H. congruence.
      SSCase "Remove Component Function".
        destruct (valid_component_path_bool p s &&
            component_is_not_connected_bool p i s); simpl in H.
        SSSCase "True Branch".
          destruct (remove_component s p i); subst; auto.
        SSSCase "False Branch".
          congruence.
    SCase "Making Interfaces".
      Focus.
      eapply rsc_step; eauto.
      unfold build_state in H.
      apply SMakeInterface.
      SSCase "Valid Path".
        apply valid_interface_path_bool_correctness.
        destruct (valid_interface_path_bool p s0);auto.
        simpl in H. congruence.
      SSCase "No id/Acc Clash".
        apply no_id_acc_clash_bool_soundness.
        destruct (no_id_acc_clash_bool);auto.
        destruct (valid_interface_path_bool); auto.
        simpl in H; congruence.
        simpl in H;congruence.
      SSCase "Add Interface Function".
        destruct ((valid_interface_path_bool p s0 && no_id_acc_clash_bool i v p s0));
          simpl in *; auto; congruence.
    SCase "Making Bindings".
      Focus.
      eapply rsc_step; eauto.
      unfold build_state in H.
      apply SMakeBinding.
      SSCase "Valid Component Binding".
        apply valid_component_binding_bool_correctness.
        destruct (valid_component_binding_bool b s); auto;
        simpl in H; congruence.
      SSCase "Binding is not Duplicate".
        apply binding_is_not_a_duplicate_bool_correctness.
        destruct (binding_is_not_a_duplicate_bool b s); auto.
        destruct (valid_component_binding_bool b s ); auto;
        simpl in H; congruence.
      SSCase "Add Binding Function".
        destruct ((valid_component_binding_bool b s &&
            binding_is_not_a_duplicate_bool b s) ); simpl in *; congruence.
      SCase "Removing Bindings".
      Focus.
      eapply rsc_step; eauto.
      unfold build_state in H.
      apply SRemoveBinding.
      SSCase "Valid Component Binding".
        apply valid_component_binding_bool_correctness.
        destruct (valid_component_binding_bool b s); auto;
        simpl in H; congruence.
      SSCase "Remove Binding Function".
        destruct ((valid_component_binding_bool b s)); simpl in *; congruence.
      SCase "Seq #1".
      assert (build_state (op1; op2) s = Some s' ->
                  exists x, build_state op1 s = Some x /\
                            build_state op2 x = Some s').
        intros.
        apply build_state_fact with (conf:=(op1; op2)); auto.
      destruct H0; auto.
      destruct H0 as (Ha, Hb).
      assert (step * ((op1, s), (Done, x))).
        apply IHop1; auto.
      clear IHop1.
      assert (step * ((op2, x), (Done, s'))).
        apply IHop2; auto.
      assert ((op1 ; op2) / s ~~~>* (Done ; op2) / x).
        apply seq_fact'; auto.
      apply rsc_trans with (y:=((Done;op2), x)).
      auto.
      mstep. auto.
      exact H1.
    SCase "Done".
      simpl in H. inversion H; subst.
      apply rsc_base.
Qed.

Lemma build_state_completeness:
  forall op s s',
   well_formed s ->
   op / s ~~~>* Done / s' -> build_state op s = Some s'.
Proof.
  induction op; intros.
  Case "Predicate entails Function".
    SCase "Making Components". Focus.
      inversion H0; subst. inversion H1; subst.
      unfold build_state.
       assert ( ((valid_component_path_bool p s && no_id_clash_bool i p s &&
                 dec_component (Component i p i0 c l l0 l1) ) = true)).
         repeat rewrite andb_true_iff.
         repeat split.
         apply valid_component_path_bool_correctness;auto.
         apply no_id_clash_bool_correctness; auto.
         apply dec_component_correctness; auto.
       rewrite H3; simpl.
       rewrite <- H15; auto.
       apply f_equal; auto.
    SCase "Removing Components". Focus.
      inversion H0; subst.
      inversion H1; subst.
      unfold build_state.
      assert ( (valid_component_path_bool p s && component_is_not_connected_bool p i s) = true).
        repeat rewrite andb_true_iff.
        repeat split.
        apply valid_component_path_bool_correctness;auto.
        apply component_is_not_connected_bool_completeness;auto.
      rewrite H3; simpl.
      rewrite <- H9.
      apply f_equal; auto.
    SCase "Making Interfaces".
      Focus.
      inversion H0; subst.
      inversion H1; subst.
      unfold build_state.
      assert ( (valid_interface_path_bool p s0 && no_id_acc_clash_bool i v p s0) = true).
        repeat rewrite andb_true_iff.
        repeat split.
        apply valid_interface_path_bool_correctness;auto.
        apply no_id_acc_clash_bool_completeness;auto.
      rewrite H3; simpl.
      rewrite <- H15.
      apply f_equal; auto.
    SCase "Making Bindings".
      Focus.
      inversion H0; subst.
      inversion H1; subst.
      unfold build_state.
      assert ( (valid_component_binding_bool b s &&
                binding_is_not_a_duplicate_bool b s) = true).
        repeat rewrite andb_true_iff.
        repeat split.
        apply valid_component_binding_bool_correctness;auto.
        apply binding_is_not_a_duplicate_bool_correctness;auto.
      rewrite H3; simpl.
      rewrite <- H8.
      apply f_equal; auto.
    SCase "Removing Bindings".
      Focus.
      inversion H0; subst.
      inversion H1; subst.
      unfold build_state.
      assert ( (valid_component_binding_bool b s) = true).
        apply valid_component_binding_bool_correctness;auto.
      rewrite H3; simpl.
      rewrite <- H7.
      apply f_equal; auto.
    SCase "Seq #1". Focus.
      destruct sequence_completion_gen with (a1:=op1) (a2:=op2)
                                          (s:=s) (s'':=s'); auto.
      destruct H1.
      assert (build_state op1 s = Some x).
        apply IHop1; auto.
      clear IHop1.
      assert (build_state op2 x = Some s').
        apply IHop2;auto.
        apply validity with (s:=s) (a:=op1); auto.
      apply build_state_fact' with (x:=x); auto.
      apply validity with (s:=s) (a:=op1); auto.
    SCase "Done".
      simpl.
      inversion H0; subst; auto.
      apply f_equal; auto.
Qed.

Lemma build_state_correctness:
  forall op s s',
    well_formed s ->
    (op / s ~~~>* Done / s' <-> build_state op s = Some s').
Proof.
  split.
  apply build_state_completeness; auto.
  apply build_state_soundness; auto.
Qed.

Theorem build_state_reduction_fact:
  forall op s s',
    well_formed s ->
    build_state op s = Some s' ->
    
    well_formed s'.
Proof.
  intros.
  rewrite <- build_state_correctness in H0; auto.
  apply validity with (s:=s) (a:=op); auto.
Qed.

Lemma eval_reduction_fact:
  forall op s',
    eval op = Some s' ->
    well_formed s'.
Proof.
  intros.
  eapply build_state_reduction_fact; eauto.
Qed.

Lemma errorState_means_stuck_reduction:
  forall op s,
    well_formed s ->
    build_state op s = None ->
    ~ (exists s', op / s ~~~>* Done/ s').
Proof.
  intros.
  intro.
  destruct H1.

  assert (well_formed x).
    eapply validity; eauto.
  assert (build_state op s = Some x).
    apply build_state_completeness; auto.
  rewrite H3 in H0.
  congruence.
Qed.

Lemma errorState_means_stuck_reduction':
  forall op,
    eval op = None ->
    ~ (exists s, op / empty_state ~~~>* Done/ s).
Proof.
  intros.
  apply errorState_means_stuck_reduction; auto.
Qed.
An application can be considered to be ready to start if is well-formed and well-typed.
However, we know that starting from a well_formed state, if we are able to reduce op to Done, then we know we reached a well-formed state. This is given by the build_state_reduction_fact theorem. However, we still need to check if it is well-typed.
Thus, we can conclude that an application is ready to start if we can reduce its operations to Done, and we reach a well_typed state.

Definition ready_to_start s :=
  well_formed s /\ well_typed s.

Lemma ready_to_start_fact:
  forall op s s',
    well_formed s ->
    build_state op s = Some s' ->
    well_typed s' ->
    ready_to_start s'.
Proof.
  intros.
  split; auto.
  eapply build_state_reduction_fact; eauto.
Qed.