Coq Library
PADEC - Coq Library

Library Padec.KDomSet.KDomSet_specification_proved

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Import

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

Local Import

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import P_Q_Termination.
From Padec Require Import Count.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import KDomSet_specification.
From Padec Require Import KDomSet_alpha.
From Padec Require Import KDomSet_correctness.
From Padec Require Import KDomSet_termination.
From Padec Require Import KDomSet_count.
From Padec Require Import Spanning_Tree.
From Padec Require Import ZUtils.

Open Scope Z_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Definition of the algorithm and proof

Section KDomSet_Specification_Proved.


  Context {Chans: Channels}.

K-Dominating Set Algorithm

  Context {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

  Section Algo.

Algorithm definitions

State of node for the algorithm
    Record KDROState :=
      mkROState {
          Par: option Channel;

          KDpeers_reverse: list (Channel * Channel);
          KDpr_assume: lpeers_reverse_assume KDpeers_reverse

    Definition KDpeers :=
      (fun ro: KDROState => llpeers (KDpeers_reverse ro)).
    Definition KDreverse :=
      (fun ro: KDROState => llreverse (KDpeers_reverse ro)).

    Instance KDreverse_local_compat:
      forall ro, Proper fequiv (KDreverse ro).

    Notation eqROS :=
      (fun (x y: KDROState) =>
         Par x == Par y /\
         equivlistA equiv (KDpeers_reverse x) (KDpeers_reverse y)).

    Instance eqROS_equiv: Equivalence eqROS.

    Global Instance KDROState_setoid: Setoid KDROState :=
      {| equiv := eqROS |}.

    Record KDState := mkState {
                          alpha: Z;
                          KDROpart :> KDROState

    Notation eqS :=
      (fun (x y: KDState) =>
         alpha x == alpha y /\ KDROpart x == KDROpart y).

    Instance eqS_equiv: Equivalence eqS.

    Global Instance KDState_setoid: Setoid KDState :=
      {| equiv := eqS |}.

    Lemma KDROState_dec: Decider (equiv (A := KDROState)).

    Lemma KDState_dec: Decider (equiv (A := KDState)).

Compatibility on states

    Instance alpha_compat: Proper fequiv alpha.

    Instance Par_compat: Proper fequiv Par.

    Instance KDpeers_reverse_compat:
      Proper (equiv ==> equivlistA equiv) KDpeers_reverse.

    Instance KDpeers_compat: Proper (equiv ==> equivlistA equiv) KDpeers.

    Definition lPar state (peer_state: Channel -> option KDState) c :=
      if InA_dec Channel_dec c (KDpeers state) then
        match peer_state c with
        | None => None | Some x => Par x end
      else None.

    Definition lalpha state (peer_state: Channel -> option KDState) c :=
      if InA_dec Channel_dec c (KDpeers state) then
        option_map alpha (peer_state c)
      else None.

    Instance lPar_compat: Proper fequiv lPar.

    Instance lalpha_compat: Proper fequiv lalpha.

    Instance KDROpart_compat: Proper fequiv KDROpart.

    Lemma KDreverse_compat:
      forall sx sy: KDROState,
        sx == sy ->
        forall c, InA equiv c (KDpeers sx) -> KDreverse sx c == KDreverse sy c.

Function run

    Definition run (state: KDState)
               (peer_state: Channel -> option KDState)
      : KDState :=
        alpha := Local_NewAlpha (KDpeers state)
                                (lPar state peer_state)
                                (KDreverse state)
                                (lalpha state peer_state);
        KDROpart := KDROpart state

    Lemma Local_NewAlpha_locality:
      forall ps1 ps2 lPar1 lPar2 rev1 rev2 lalpha1 lalpha2,
        Proper fequiv lPar1 -> Proper fequiv lPar2 ->
        Proper fequiv lalpha1 -> Proper fequiv lalpha2 ->
        Proper fequiv rev1 -> Proper fequiv rev2 ->
        equivlistA equiv ps1 ps2 ->
        (forall c, InA equiv c ps1 -> lPar1 c == lPar2 c /\
                                      lalpha1 c == lalpha2 c /\
                                      rev1 c == rev2 c) ->
        Local_NewAlpha ps1 lPar1 rev1 lalpha1 =
        Local_NewAlpha ps2 lPar2 rev2 lalpha2.

Compatibility of definitions used in run_algorithm

    Instance run_compat: Proper fequiv run.

    Lemma ROpart_stable: forall s sn, KDROpart (run s sn) =~= KDROpart s.

The Algorihtm

    Instance KDomSet_algo: Algorithm.

    Global Instance KDomSet_Stable:
      Stable_Variable KDomSet_algo KDROpart.

  End Algo.

  Context {Net: Symmetric_Network}.

Input Assumptions:

Finite symmetric topology from Net and Spanning tree assumption
  Definition assumptions_RO roenv: Prop :=
    (forall n, equivlistA equiv (KDpeers_reverse (roenv n))
                          (build_symlinks Net n)) /\
      net (fun n => Par (roenv n)).

  Lemma assumptions_RO_compat: Proper fequiv assumptions_RO.

  Lemma assume_ensures_Symmetric_Network:
    forall roenv,
      assumptions_RO roenv ->
        Net (fun n => KDpeers (roenv n))
        (fun n => KDreverse (roenv n)).

  Instance KDom_Stable: Stable_Variable KDomSet_algo KDROpart.

  Instance KDom_Assumption:
    Stable_Assumption (Algo := KDomSet_algo) (Net := net).

  Notation Env := (Env (Algo := KDomSet_algo)).

  Notation ROEnv := (ROEnv (Stable_Assumption := KDom_Assumption)).

  Notation Par_part := (fun (g: Env) n => Par (g n)).

  Notation alpha_part := (fun (g: Env) n => alpha (g n)).

  Instance Par_part_compat: Proper fequiv Par_part.

  Instance alpha_part_compat: Proper fequiv alpha_part.

  Notation lenv_Par :=
    (fun (g: Env) n c =>
       match local_env g n c with | Some x => Par x | None => None end).

  Notation lenv_alpha :=
    (fun (g: Env) n c => option_map alpha (local_env g n c)).

  Instance lenv_Par_compat: Proper fequiv lenv_Par.

  Instance lenv_alpha_compat: Proper fequiv lenv_alpha.

  Lemma NewAlpha_equiv_KDom:
    forall g,
      Proper pequiv g ->
        Net (fun n => KDpeers (ROEnv_part g n))
        (fun n => KDreverse (ROEnv_part g n)) ->
      forall n,
        NewAlpha (Par_part g) (alpha_part g) n =
        Local_NewAlpha (KDpeers (g n)) (lPar (g n) (local_env g n))
                       (KDreverse (g n))
                          (g n) (local_env g n)).


  Section Correctness.

    Lemma final:
      forall (g: Env),
          Net (fun n => KDpeers (g n)) (fun n => KDreverse (g n))
        terminal g ->
        forall n: Node, ~ enabled_alpha (Par_part g) (alpha_part g) n.

    Definition kDominator_ (g: Env) (n: Node): Prop :=
      kDominator (Par_part g) (alpha_part g) n = true.

    Theorem kdom_set_at_terminal:
      forall (g: Env),
        Assume g -> terminal g -> (kDOM kDominator_ g).

    Lemma kDOM_partial_correctness:
      P_correctness KDom_Assumption (kDOM kDominator_).

  End Correctness.

  Section Termination.

    Section With_root_sym.
      Variable (root: Node).

      Theorem k_dom_set_terminates:
        forall (g: Env), Proper pequiv g /\
                           Net (fun n => KDpeers (ROEnv_part g n))
                           (fun n => KDreverse (ROEnv_part g n)) /\
                         spanning_tree root (Par_part g)
                         -> Acc Step g.

    End With_root_sym.

    Lemma kDOM_termination: termination KDom_Assumption.

  End Termination.

  Section Silent_Self_Stabilization.

    Theorem kdom_silent_self_stabilization:
      silence KDom_Assumption unfair_daemon /\
      self_stabilization KDom_Assumption
                         unfair_daemon (only_one (kDOM kDominator_)).

  End Silent_Self_Stabilization.

  Section Counting.

    Definition Dominators (g: Env) := { n: Node | kDominator_ g n }.

    Theorem counting:
      forall (g: Env),
        Assume g -> terminal g ->
        exists N D: nat,
          Num_Card Same Node N /\ Num_Card Same (Dominators g) D /\
          (N - 1 >= S (Z.to_nat k) * (D - 1))%nat.

  End Counting.

End KDomSet_Specification_Proved.

Close Scope Z_scope.
Close Scope signature_scope.
Unset Implicit Arguments.