Coq Library
PADEC - Coq Library

Library Padec.Model.Compo_ex

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

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

Local Imports

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.

One given network

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

Algorithm 1

  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).

Assumption on Algo1: identified network

  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 |}.

Specification on Algo1: spanning tree

  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.

Algorithm 2

  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).

Assumption on Algo2: spanning tree

  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 |}.

Specification on Algo2: k-dominating set

  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.

Algo3: collateral hierarchical composition of Algo1 and Algo2

  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.