PADEC
Coq Library
Toc
Tools
PADEC - Coq Library

Library Padec.KDomSet.KDomSet_algo_tree_topology

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Lia.

Local Imports

From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import FoldRight.
From Padec Require Import Tree_topology.
From Padec Require Import Algorithm.

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

Definition of alpha and its computation

Section KDomSet_Algo.

  Context {Chans: Channels}.

  Class KDomSet_parameters :=
    {
      

The parameter K itself (from K-Dominating-Set)

      k: Z;
      k_pos: k > 0
    }.
  Context {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

State of a Node in the Algorithm

Read Only Part of a State

It stores local information about the tree topology:
  Record KDom_ROState := mkROState {
                             is_root: bool;
                             children_c: list Channel;
                           }.

  Notation eqROS := (fun (x y: KDom_ROState) =>
                       is_root x == is_root y /\
                       equivlistA equiv (children_c x) (children_c y)).

  Instance eqROS_equiv: Equivalence eqROS.

  Global Instance KDom_ROState_setoid: Setoid KDom_ROState :=
    {| equiv := eqROS |}.

State of a Node


  Record KDom_State := mkState {
                           alpha: Z;
                           KDom_ROpart:> KDom_ROState;
                         }.

  Notation eqS := (fun (x y: KDom_State) =>
                     alpha x == alpha y /\
                     KDom_ROpart x == KDom_ROpart y).

  Instance eqS_equiv: Equivalence eqS.

  Global Instance KDom_State_setoid: Setoid KDom_State :=
    {| equiv := eqS |}.

Equality and Compatibility properties on State


  Lemma KDom_ROState_dec: Decider (equiv (A := KDom_ROState)).

  Lemma KDom_State_dec: Decider (equiv (A := KDom_State)).

  Instance alpha_compat: Proper fequiv alpha.

  Instance is_root_compat_RO: Proper fequiv is_root.

  Instance children_c_compat_RO:
    Proper (equiv ==> equivlistA equiv) children_c.

  Instance KDom_ROpart_compat: Proper fequiv KDom_ROpart.

  Instance is_root_compat:
    Proper (equiv (A := KDom_State) ==> equiv) is_root.

  Instance children_c_compat:
    Proper (equiv (A := KDom_State) ==> equivlistA equiv) children_c.

  Section Run_definition.

Run Function for the Algorithm


    Definition _IsShort _alpha := (_alpha <? k).

    Instance _IsShort_compat: Proper fequiv _IsShort.

    Definition _IsTall _alpha := (_alpha >=? k).

    Instance _IsTall_compat: Proper fequiv _IsTall.

    Definition min_Atall l :=
      List.fold_right Z.min (2 * k + 1) (List.filter _IsTall l).

    Instance min_Atall_compat:
      Proper (equivlistA equiv ==> equiv) min_Atall.

    Definition max_Ashort l :=
      List.fold_right Z.max (-1) (List.filter _IsShort l).

    Instance max_Ashort_compat:
      Proper (equivlistA equiv ==> equiv) max_Ashort.

    Definition new_alpha (alpha_children: list Z): Z :=
      let max := max_Ashort alpha_children in
      let min := min_Atall alpha_children in
      if Z_le_gt_dec (max + min + 2) (2 * k)
      then min + 1 else max + 1.

    Instance new_alpha_compat:
      Proper (equivlistA equiv ==> equiv) new_alpha.

    Definition alphas (s_children: list KDom_State): list Z := map alpha s_children.

    Instance alphas_compat: Proper (equivlistA equiv ==> equivlistA equiv) alphas.

    Definition children_states (s: KDom_ROState)
               (peer_state: Channel -> option KDom_State): list KDom_State :=
      map_filter peer_state (children_c s).

    Instance children_states_compat: Proper (equiv ==> fequiv ==> equivlistA equiv) children_states.

    Lemma children_states_depends:
      forall s1 s2,
        equivlistA equiv (children_c s1) (children_c s2) ->
        forall ps1 ps2,
          Proper pequiv ps1 -> Proper pequiv ps2 ->
          (forall c, InA equiv c (children_c s1) -> ps1 c == ps2 c) ->
          equivlistA equiv (children_states s1 ps1) (children_states s2 ps2).

    Definition run_algorithm
               (s: KDom_State)
               (peer_state: Channel -> option KDom_State)
      : KDom_State :=
      {| alpha := new_alpha (alphas (children_states s peer_state));
         KDom_ROpart := s |}.

  End Run_definition.

Properties of the Algorithm

Compatibility of the Run Function


  Instance run_algorithm_compat: Proper fequiv run_algorithm.

Stability for the Read-Only Part of the Run Function

  Lemma ROpart_stable:
    forall s sn, KDom_ROpart (run_algorithm s sn) =~= KDom_ROpart s.

Definition of The Algorithm

  Instance KDom_algo: Algorithm :=
    {| State := KDom_State; State_dec := KDom_State_dec; run := run_algorithm; |}.

  Global Instance KDom_Stable: Stable_Variable KDom_algo KDom_ROpart.

  Section Short_Or_Tall.

    Lemma short_or_tall: forall alpha,
      {_IsShort alpha = true} + {_IsTall alpha = true}.

  End Short_Or_Tall.

alpha is always between 0 and 2k

  Section Range_of_alpha.

    Lemma new_alpha_0_2k:
      forall alphas, 0 <= new_alpha alphas <= 2 * k.

  End Range_of_alpha.

End KDomSet_Algo.

Common definitions and results ******************

From Padec Require Import RelModel.
*****************************************************

Section KDom_Assume.

  Context {Chans: Channels}.

  Context {Net: Network}
          {DTN: Down_Tree_Network Net}.

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

  Global Instance KDom_RO_assumption:
    Stable_Assumption (Algo := KDom_algo) (Net := Net).

  Notation Env := (Env (Net := Net) (Algo := KDom_algo)).

  Lemma children_c_equiv: forall (env: Env) (n: Node),
      Assume env ->
      equivlistA equiv (children_c (env n)) (DTN_children n).

  Lemma is_root_equiv: forall (env: Env) n,
      Assume env -> is_root (env n) == DTN_root n.

  Notation alphas_ :=
    (fun (env: Env) n => alphas (children_states (env n) (local_env env n))).

  Notation new_alpha_ := (fun env n => new_alpha (alphas_ env n)).

  Section KDom_Graph.

kDomSet definitions

    Definition is_kDom_edge (env: Env) (x y: Node): Prop :=
      match alpha (env y) ?= k with
      | Lt => (isParent x y)
      | Eq => False
      | Gt => (isParent y x) /\ alpha (env x) = alpha (env y) - 1
      end.

    Global Instance is_kDom_edge_compat: Proper fequiv is_kDom_edge.

    Definition kDominator (env: Env) (p: Node) :=
      orb (Z.eqb (alpha (env p)) k)
          (andb (_IsShort (alpha (env p))) (is_root (env p))).

    Global Instance kDominator_compat: Proper fequiv kDominator.

  End KDom_Graph.

Assume that the computation of alpha provides no new value

relation on the values of alpha between children and parent
  Section Alpha_child_parent.

Assumptions on Inputs
    Variable (env: Env)
             (env_compat: Proper pequiv env)
             (hassume: Assume env).

Local properties of alpha, based on is_tree_parent
    Lemma InA_alphas:
      forall (n: Node) (a: Z),
        (exists (m: Node), isParent n m /\ alpha (env m) = a)
        <-> InA equiv a (alphas_ env n).
    Lemma new_alpha_inv:
      forall (n: Node),
        alpha (env n) = new_alpha_ env n ->
        alpha (env n) > 0 ->
        exists m, isParent n m /\ alpha (env n) = alpha (env m) + 1.

  End Alpha_child_parent.

End KDom_Assume.

Close Scope signature_scope.
Close Scope Z_scope.
Unset Implicit Arguments.
You can change colors, if you wish ;)