Mefresa.Operation.Reductions

GCM Architectures - Some Examples


Require Import Mefresa.Operation.Semantics.

Definition SimpleArchitecture : operation :=
  Mk_component (Ident "A") nil default_class Configuration nil nil nil;
  Mk_component (Ident "B") nil default_class Configuration nil nil nil;
  Mk_interface (Ident "X") "org.proactive.hm.HMServerManager" ((Ident "A"):: nil) External Client Control Optional Singleton;
  Mk_interface (Ident "Y") "org.proactive.hm.HMConfig" ((Ident "B"):: nil) External Server Control Optional Singleton;
  Mk_binding (Normal nil (Ident "A") (Ident "X") (Ident "B") (Ident "Y")).
Let us define a simple tactic for improving the proof automation. Ths tactic has the purpose of automatically deciding that two operations are different. Naturally, it uses the lemma operation_dec about operation's decidability proved above.
Ltac operation_ineq :=
  match goal with
    |- ?A <> ?B => destruct operation_dec with (a:=A) (a':=B);
                   [
                     match goal with
                       H:?A = ?B |- A <> B => inversion H
                     | _ => idtac
                     end
                    | auto
                     ]
  | _ => idtac
  end.

Lemma simpleProof :
  exists s,
   SimpleArchitecture / empty_state ~~~>* Done / s.
Proof.
  eexists.
  unfold SimpleArchitecture.
  eapply rsc_step.
  Case "One Step: x --> y".
    apply SSeq2.
    destruct operation_dec with (a:=(Mk_component (Ident "B") nil default_class Configuration nil nil nil;
                                  Mk_interface (Ident "X") "" (Ident "A" :: nil) External Client Control Optional Singleton;
                                  Mk_interface (Ident "Y") "" (Ident "B" :: nil) External Server Control Optional Singleton;
                                  Mk_binding (Normal nil (Ident "A") (Ident "X") (Ident "B") (Ident "Y"))) )
                             (a':=Done).
    inversion e.
    apply SMakeComponent; intuition.
    SCase "No ID Clash uppon Component Insertion".
      unfold no_id_clash.
      intros.
      inversion H; subst.
      thus apply NotInNil.
  Case "Others Steps: y -->* z".
    eapply rsc_step.
    SCase "One Step: x --> y".
      apply SSeq2.
      apply SMakeComponent; intuition.
      SSCase "No ID Clash uppon Component Insertion".
        unfold no_id_clash; intros.
        inversion H. clear H.
        thus apply NotInStep with
          (a:=Component (Ident "A") nil default_class Configuration nil nil nil) (r:=nil);
        auto.
    SCase "Others Steps: y -->* z".
      eapply rsc_step.
      SSCase "One Step: x --> y".
        apply SSeq2.
        apply SMakeInterface; intuition.
        SSSCase "Valid Path for Interface Creation".
          unfold valid_interface_path.
          simpl.
          apply ValidInterfacePath_Base with (id:=Ident "A"); auto.
          eexists; simpl; eauto.
        SSSCase "No Clash in id * visibility uppon Interface Insertion".
          unfold no_id_acc_clash; intros.
          simpl in *.
          inversion H.
          simpl.
          apply NotInPair_Nil; auto.
      SSCase "Other Steps: y -->* z".
        eapply rsc_step.
        SSSCase "One Step: x --> y".
          apply SSeq2.
          apply SMakeInterface.
          SSSSCase "Valid Path to Component".
            unfold valid_interface_path.
            apply ValidInterfacePath_Base with (id:=Ident "B"); auto.
            eexists; simpl; eauto.
          SSSSCase "No clash beetwen id*acc".
            unfold no_id_acc_clash.
            intros.
            inversion H. clear H.
            destruct c. inversion H1; subst. clear H1.
            simpl.
            apply NotInPair_Nil; auto.
          SSSSCase "adding interface went well".
            refl.
        SSSCase "Others Steps: y -->* z".
          eapply rsc_step.
          SSSSCase "One Step: x --> y".
            apply SMakeBinding;intros.
            SSSSSCase "Valid binding".
              unfold valid_component_binding.
              simpl.
              apply ValidComponentBinding_Base; auto.
              compute; intuition.
            SSSSSCase "Binding is not a Duplicate".
              compute. intro HFalse; inversion HFalse.
            SSSSSCase "adding binding".
              refl.
       SSSSCase "Last step".
         auto.
Qed.

step: a custom tactic to reason on operations


Ltac step :=
  match goal with
        
     |- ?operation / ?S ~~~>* ?operation' / ?S' =>
           
           (match operation with
                  (Seq ?A1 ?As) => eapply rsc_step
             | _ => apply rsc_base
            end)
    | |- ?operation / ?S ~~~>* ?operation / ?S => apply rsc_base
    
    | |- Seq (?A1 ; ?A2) / ?S ~~~> ?operation' / ?s' => apply SSeq2
    | |- step ((?A1 ; ?A2), ?S) ?X' => apply SSeq2
    | |- Seq (Done ; ?a) / ?s ~~~> ?a' / ?s' => apply SSeqFinish
    | |- step ((Done ; ?A2), ?S) ?X' => apply SSeqFinish
    
    | |- (Mk_component ?id ?p ?ic ?c ?lc ?li ?lb) / ?s ~~~> ?a / ?s' => apply SMakeComponent
    | |- (Rm_component ?p ?id) / ?s ~~~> ?a / ?s' => apply SRemoveComponent
    | |- (Mk_interface ?id ?sig ?p ?a ?c ?f ?ct ?cd) / ?s ~~~> ?a' / ?s' => apply SMakeInterface
    | |- (Mk_binding ?b) / ?s ~~~> ?a / ?s' => apply SMakeBinding
    | |- step ((Mk_binding ?b), ?s) ?X => apply SMakeBinding
    | |- (Rm_binding ?b) / ?s ~~~> ?a / ?s' => apply SRemoveBinding
    | |- step ((Rm_binding ?b), ?s) ?X => apply SRemoveBinding
    
    | _ => fail
  end.

Ltac mstep := repeat step.

Example simpleProof_Revisited :
  exists s,
   SimpleArchitecture / empty_state ~~~>* Done / s.
Proof.
  eexists.
  unfold SimpleArchitecture.   mstep; auto.
  Case "Make Component, No Id Clash".
    unfold no_id_clash.
    intros.
    inversion H; subst.
    thus apply NotInNil.
  Case "Make Component, Adding the Component".
    refl.
  Case "Make Component, No Id Clash".
    unfold no_id_clash.
    intros.
    inversion H; subst.
    thus apply NotInStep with
          (a:=Component (Ident "A") nil default_class Configuration nil nil nil) (r:=nil).
  Case "Make Component, Adding the Component".
    refl.
  Case "Make Interface, Valid Interface Path".
    unfold valid_interface_path.
    simpl.
    apply ValidInterfacePath_Base with (id:=Ident "A"); auto.
    eexists; simpl; eauto.
  Case "Make Interface, no clash between id and visibility value".
    unfold no_id_acc_clash.
    intros.
    inversion H. clear H.
    destruct c. inversion H1; subst. clear H1.
    simpl.
    apply NotInPair_Nil; auto.
  Case "Make Interface, Adding the Interface".
    refl.
  Case "Make Interface, Valid Interface Path".
    unfold valid_interface_path.
    simpl.
    apply ValidInterfacePath_Base with (id:=Ident "B"); auto.
    eexists; simpl; eauto.
  Case "Make Interface, no clash between id and visibility value".
    unfold no_id_acc_clash.
    intros.
    inversion H. clear H.
    destruct c. inversion H1; subst. clear H1.
    simpl.
    apply NotInPair_Nil; auto.
  Case "Make Interface, Adding the Interface".
    refl.
  Case "Make Binding, Valid Path #1".
    auto.
    eapply rsc_step.
    apply SMakeBinding.
    auto.
    unfold valid_component_binding.
     simpl.
     apply ValidComponentBinding_Base; auto.
     compute; intuition.
     compute. intro HFalse; inversion HFalse.
     refl.
     mstep.
Qed.

Testing removing of Bindings


Function execute (act:operation) (init:state) {struct act}: option state :=
  match act with
    | Mk_component i p ic cl lc li lb =>
        match add_component init p i ic cl lc li lb with
          | None => None
          | Some s => Some s
        end
    | Rm_component p i =>
      match remove_component init p i with
          | None => None
          | Some s => Some s
      end
    | Mk_interface i sig p a c f ct cd =>
        match add_interface init p i sig a c f ct cd with
          | None => None
          | Some s => Some s
        end
    | Mk_binding b =>
        match add_binding init b with
          | None => None
          | Some s => Some s
        end
    | Rm_binding b =>
        match remove_binding init b with
          | None => None
          | Some s => Some s
        end
    | Seq a1 a2 =>
       let s := execute a1 init in
       match s with
         | None => None
         | Some s' => execute a2 s'
       end
    | Done => Some init
  end.

Lemma execute_computes_the_semantics:
  forall a s s',
    a / s ~~~>* Done / s' ->
    Some s' = execute a s.
Proof.
  induction a; intros; unfold execute.
  Case "Mk Component".
    unfold add_component.
    destruct s.
    inversion H.
    inversion H0; subst.
    unfold add_component in H15.
    rewrite <- H15.
    apply f_equal. symmetry. eauto.
  Case "Rm Component".
    unfold remove_component.
    destruct s.
    inversion H.
    inversion H0; subst.
    unfold remove_component in H9.
    inversion H9; subst. clear H9.
    apply f_equal. symmetry. eauto.
  Case "Mk Interface".
    unfold add_interface.
    destruct s0.
    inversion H.
    inversion H0; subst.
    unfold add_interface in H15.
    rewrite <- H15.
    apply f_equal; symmetry; eauto.
   Case "Mk binding".
    unfold add_binding.
    destruct s.
    inversion H.
    inversion H0; subst.
    unfold add_binding in H8.
    rewrite <- H8.
    apply f_equal; symmetry; eauto.
  Case "Rm binding".
    unfold remove_binding.
    destruct s.
    inversion H.
    inversion H0; subst.
    unfold remove_binding in H7.
    rewrite <- H7. apply f_equal; symmetry; eauto.
  Case "Sequence". Focus.
    fold execute.
    destruct sequence_completion_gen with (a1:=a1) (a2:=a2)
                                          (s:=s) (s'':=s'); auto.
    destruct H0.
    assert (Some x = execute a1 s).
      apply IHa1. exact H0.
    rewrite <- H2.
    apply IHa2; auto.
  Case "Done ".
    apply f_equal; symmetry; eauto.
Qed.

Definition RemoveBinding : operation :=
  Rm_binding (Normal nil (Ident "A") (Ident "X") (Ident "B") (Ident "Y")).

Example Arch_is_Sound:
  forall s, Some s = execute SimpleArchitecture empty_state ->
  exists s', RemoveBinding / s ~~~>* Done / s'.
Proof.
  intros.
  simpl in H.
  eexists.
  unfold RemoveBinding.
  mstep.
  Focus.
  inversion H.
  clear H H1.
  unfold valid_component_binding; simpl.
  eapply rsc_step. mstep.
  apply ValidComponentBinding_Base; auto.
  simpl.
  eexists; simpl; auto.
  refl.
  mstep.
Qed.

Example Arch_is_Sound' :
  exists s,
   SimpleArchitecture / empty_state ~~~>* Done / s /\
   exists s', RemoveBinding / s ~~~>* Done / s'.
Proof.
  destruct simpleProof_Revisited .
  eexists.
  split; eauto.
  apply execute_computes_the_semantics in H.
  simpl in H.
  inversion H. clear H H1.
  apply Arch_is_Sound.
  refl.
Qed.

Definition RemoveComponent : operation := Rm_component nil (Ident "A") .

Example Arch_is_Sound_After_Removal:
  forall s, Some s = execute SimpleArchitecture empty_state ->
  forall s', Some s' = execute RemoveBinding s ->
  exists s'', RemoveComponent / s' ~~~>* Done / s''.
Proof.
  intros.
  simpl in H0.
  simpl in H.
  inversion H.
  subst.
  inversion H0; subst.
  clear H.
  clear H0.
  eexists.
  mstep.
  unfold RemoveComponent.
  mstep; auto.
  simpl.
  unfold not_binded.
  intros.
  eapply rsc_step.
  apply SRemoveComponent.
  auto.
  simpl.
  unfold not_binded. intros. inversion H.
  refl.
  apply rsc_base.
Qed.

Testing removing components


Definition AnotherSimpleArchitecture : operation :=
  Mk_component (Ident "A") nil default_class Configuration nil nil nil;
  Mk_component (Ident "Sub A") (Ident "A" :: nil) default_class Configuration nil nil nil;
  Mk_interface (Ident "X") "org.proactive.hm.HMServerManager" ((Ident "A"):: nil) Internal Client Control Optional Singleton;
  Mk_interface (Ident "Y") "org.proactive.hm.HMDbConfig" ((Ident "A") :: (Ident "Sub A") :: nil) External Server Control Optional Singleton;
  Mk_binding (Export ((Ident "A") :: nil) (Ident "X") (Ident "Sub A") (Ident "Y")).

Example Arch_is_Sound_After_Removal':
  forall s, Some s = execute AnotherSimpleArchitecture empty_state ->
  exists s', RemoveComponent / s ~~~>* Done / s'.
Proof.
  intros.
  simpl in H.
  inversion H. subst.
  clear H.
  eexists.
  unfold RemoveComponent.
  mstep.
  Case "Path is Valid".
    unfold valid_component_path.
    simpl.
Abort.

Definition AnotherSimpleArchitecture' : operation :=
  Mk_component (Ident "A") nil default_class Configuration nil nil nil;
  Mk_component (Ident "Sub A") (Ident "A" :: nil) default_class Configuration nil nil nil;
  Mk_interface (Ident "X") "org.proactive.hm.HMServerManager" ((Ident "A"):: nil) Internal Client Control Optional Singleton;
  Mk_interface (Ident "Y") "org.proactive.hm.HMDbConfig" ((Ident "A") :: (Ident "Sub A") :: nil) External Server Control Optional Singleton;
  Rm_component (Ident "A" :: nil) (Ident "Sub A").