Library Padec.Model.Compo_ex

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.

From Padec Require Import Algorithm.
From Padec Require Import Composition.
From Padec Require Import Spanning_Tree.
From Padec Require Import RelModel.
From Padec Require Import Fairness.
From Padec Require Import Stream.
From Padec Require Import Exec.
From Padec Require Import Self_Stabilization.
From Padec Require Import OptionUtil.
From Padec Require Import RelationA.
From Padec Require Import SetoidUtil.


Section kDomSet.

  Context {Chans: Channels}
          {Net: Network}.

  Variable (Algo1: Algorithm).
  Notation S1:= (@State Chans Algo1).
  Notation Env1:= (@Env Chans Net Algo1).

  Variable (ROS1: Type) (getRO1: S1 -> ROS1).
  Variable RO1_Stable: Stable_Variable Algo1 getRO1.

  Notation ROEnv1 := (Node -> ROS1).

  Context {IDType: Type} `{ID_setoid: Setoid IDType}.
  Variable (ID1: ROS1 -> IDType) (ID1_compat: Proper fequiv ID1).

  Definition UniqueID1 (rog: ROEnv1): Prop:=
    Proper fequiv rog -> forall n1 n2, (ID1 (rog n1)) == (ID1 (rog n2)) ->
                                       n1 == n2.

  Instance UniqueID1_compat: Proper fequiv UniqueID1.

  Instance Assumption1: Stable_Assumption :=
    {| Assume_RO := UniqueID1 |}.

  Variable (root1: Node)
           (Par1: S1 -> option Channel) (Par1_compat: Proper fequiv Par1).
  Definition SPAN_TREE1 (g: Env1): Prop:=
    (spanning_tree root1 (fun n => Par1 (g n))).

  Hypothesis PCorrectness1: P_correctness Assumption1 SPAN_TREE1.
  Hypothesis WFtermination1: silence Assumption1 weakly_fair.

  Variable (Algo2: Algorithm).
  Notation S2:= (@State Chans Algo2).
  Notation Env2:= (@Env Chans Net Algo2).

  Variable (ROS2: Type) (getRO2: S2 -> ROS2).
  Variable RO2_Stable: Stable_Variable Algo2 getRO2.

  Notation ROEnv2:= (Node -> ROS2).

  Variable (root2: Node)
           (Par2: ROS2 -> option Channel)
           (Par2_compat: Proper fequiv Par2).

  Definition SPAN_TREE2 (rog: ROEnv2): Prop:=
    spanning_tree root2 (fun n => Par2 (rog n)).

  Instance SPAN_TREE2_compat: Proper pequiv SPAN_TREE2.

  Instance Assumption2: Stable_Assumption :=
    {| Assume_RO := SPAN_TREE2 |}.

  Variable (k: nat).
  Variable (kDominator: Env2 -> Node -> Prop).

  Definition is_neighbor_of (x y: Node): Prop:=
    exists (c: Channel), (peer x c) == (Some y).
  Definition is_path:= chain is_neighbor_of.

  Definition kDOM (g: Env2): Prop:=
    forall (n: Node),
    exists (d: Node), kDominator g d /\
                      exists path, (is_path d path n) /\
                                   (length path) <= k.

  Hypothesis PCorrectness2: P_correctness Assumption2 kDOM.
  Hypothesis WFtermination2: silence Assumption2 weakly_fair.

  Context (C3: Composition_State Algo1 Assumption2).
  Notation Compo := (Collateral_composition (Assumption2:=Assumption2)).

  Notation S3:= (S3 (Assumption2:=Assumption2)).
  Notation read1:= (read1 (Assumption2:=Assumption2)).
  Notation read2:= (read2 (Assumption2:=Assumption2)).
  Notation Env3 := (@Env Chans Net Compo).
  Notation envread1 := (envread1 (Assumption2:=Assumption2)).
  Notation envread2 := (envread2 (Assumption2:=Assumption2)).

  Variable (samePar: forall s3: S3,
               (Par1 (read1 s3)) == (Par2 (getRO2 (read2 s3)))).
  Variable (sameRoot: root1 == root2).

  Lemma ASSUMES: forall g : Env, Proper fequiv g -> SPAN_TREE1 (envread1 g) ->
                                 SPAN_TREE2 (ROEnv_part (envread2 g)).

  Instance Assumption3: Stable_Assumption (Algo := Compo) :=
    Assumption3 Assumption1 (Assumption2 := Assumption2).

  Lemma PCorrectness_Compo:
    exists (kDominator3: Env3 -> Node -> Prop),
      P_correctness (Algo := Compo) Assumption3
                    (fun (g: Env3) =>
                       forall (n: Node),
                       exists (d: Node), kDominator3 g d /\
                                         exists path, (is_path d path n) /\
                                                      (length path) <= k).

  Lemma WF_Termination_Compo:
    silence Assumption3 weakly_fair.

End kDomSet.