Require Import Relations.
Require Import List.
Require Import Utils.
Require Import Semantics.
Require TINI.


Set Implicit Arguments.
Hint Constructors TINI.exec.

Definition of refinement

Section Refinement.

Variable S1 : semantics.
Let trace1 := list (event S1).

Variable S2 : semantics.
Let trace2 := list (event S2).

Inductive match_traces (match_events : event S1 -> event S2 -> Prop)
  : trace1 -> trace2 -> Prop :=
| mt_nil : match_traces match_events nil nil
| mt_cons : forall e1 t1 e2 t2,
              match_events e1 e2 ->
              match_traces match_events t1 t2 ->
              match_traces match_events (e1 :: t1) (e2 :: t2).
Hint Constructors match_traces.

Lemma match_traces_no_filter:
  forall (match_events: event S1 -> event S2 -> Prop) tr1 tr2,
    match_traces match_events tr1 tr2 ->
      length tr1 = length tr2.

Definition refinement_statement match_init_data
                                match_events :=
  forall i1 i2 t2 s2,
    match_init_data i1 i2 ->
    @TINI.exec S2 (init_state S2 i2) t2 s2 ->
    exists t1 s1,
      @TINI.exec S1 (init_state S1 i1) t1 s1 /\
      match_traces match_events t1 t2.

Record refinement := {
  ref_match_init_data : init_data S1 -> init_data S2 -> Prop;
  ref_match_events : event S1 -> event S2 -> Prop;
  ref_prop : refinement_statement ref_match_init_data
                                  ref_match_events
}.

Definition state_refinement_statement match_states
                                      match_events :=
  forall s1 s2 t2 s2',
    match_states s1 s2 ->
    @TINI.exec S2 s2 t2 s2' ->
    exists t1 s1',
      @TINI.exec S1 s1 t1 s1' /\
      match_traces match_events t1 t2.

Record state_refinement := {
  sref_match_states : state S1 -> state S2 -> Prop;
  sref_match_events : event S1 -> event S2 -> Prop;
  sref_prop : state_refinement_statement sref_match_states
                                         sref_match_events
}.

Refinement from state

Section RefinementFromStateRefinement.

Variable SR : state_refinement.

Variable match_init_data : init_data S1 -> init_data S2 -> Prop.

Hypothesis match_init_data_match_states :
  forall i1 i2,
    match_init_data i1 i2 ->
    sref_match_states SR (init_state _ i1) (init_state _ i2).

Lemma refinement_from_state_refinement_prop :
  refinement_statement match_init_data
                       (sref_match_events SR).

Definition refinement_from_state_refinement : refinement :=
  {| ref_match_init_data := match_init_data
   ; ref_match_events := sref_match_events SR
   ; ref_prop := refinement_from_state_refinement_prop |}.

End RefinementFromStateRefinement.

Refinement preserves tini

Section NI.

Context {O1 : TINI.Observation S1}
        {O2 : TINI.Observation S2}.


Variable R : refinement.

Hypothesis noninterference1 : TINI.tini O1.

Let low_compatible o1 o2 :=
  forall e1 e2,
    ref_match_events R e1 e2 ->
    (TINI.e_low o1 e1 <-> TINI.e_low o2 e2).

Let i_equiv1_i_equiv2 o1 o2 :=
  forall i21 i22,
    TINI.i_equiv o2 i21 i22 ->
    exists i11 i12,
      TINI.i_equiv o1 i11 i12 /\
      ref_match_init_data R i11 i21 /\
      ref_match_init_data R i12 i22.

Let a_equiv1_a_equiv2 o1 o2 :=
  forall e11 e12 e21 e22,
    TINI.a_equiv _ o1 (E e11) (E e12) ->
    ref_match_events R e11 e21 ->
    ref_match_events R e12 e22 ->
    TINI.a_equiv _ o2 (E e21) (E e22).

Lemma match_traces_match_observations :
  forall o1 o2 t1 t2
         (COMP : low_compatible o1 o2)
         (TRACES : match_traces (ref_match_events R) t1 t2),
    match_traces (ref_match_events R)
                 (TINI.observe O1 o1 t1) (TINI.observe O2 o2 t2).

Definition tini_preservation_hypothesis :=
  forall o2, exists o1,
    low_compatible o1 o2 /\
    i_equiv1_i_equiv2 o1 o2 /\
    a_equiv1_a_equiv2 o1 o2.

Hypothesis compatibility : tini_preservation_hypothesis.

Theorem refinement_preserves_noninterference : TINI.tini O2.

End NI.

Section Strong.

Variable match_events : event S1 -> event S2 -> Prop.
Variable match_states : state S1 -> state S2 -> Prop.

Inductive match_actions : (event S1)+τ -> (event S2)+τ -> Prop :=
| match_actions_silent : match_actions Silent Silent
| match_actions_event : forall e1 e2,
  match_events e1 e2 -> match_actions (E e1) (E e2).

Hypothesis lockstep : forall s11 s21 a2 s22,
                        match_states s11 s21 ->
                        step S2 s21 a2 s22 ->
                        exists a1 s12,
                          step S1 s11 a1 s12 /\ match_actions a1 a2 /\ match_states s12 s22.

Theorem strong_refinement_prop :
  state_refinement_statement match_states
                             match_events.

Definition strong_refinement : state_refinement :=
  {| sref_prop := strong_refinement_prop |}.

End Strong.

End Refinement.

Composition of refinements

Section Composition.

Variable S1 : semantics.
Variable S2 : semantics.
Variable S3 : semantics.

Variable R12 : refinement S1 S2.
Variable R23 : refinement S2 S3.

Variable match_init_data : init_data S1 -> init_data S3 -> Prop.
Variable match_events : event S1 -> event S3 -> Prop.

Hypothesis mid13 : forall s1 s3,
                     match_init_data s1 s3 ->
                     exists s2,
                       ref_match_init_data R12 s1 s2 /\
                       ref_match_init_data R23 s2 s3.
Hypothesis me13 : forall e1 e2 e3,
                    ref_match_events R12 e1 e2 ->
                    ref_match_events R23 e2 e3 ->
                    match_events e1 e3.

Lemma match_events_composition : forall t1 t2 t3,
                                   match_traces S1 S2
                                                (ref_match_events R12) t1 t2 ->
                                   match_traces S2 S3
                                                (ref_match_events R23) t2 t3 ->
                                   match_traces S1 S3 match_events t1 t3.

Lemma ref_composition_prop : refinement_statement S1 S3 match_init_data match_events.

Definition ref_composition :=
  {| ref_prop := ref_composition_prop |}.

End Composition.