PADEC
Coq Library
Toc
Tools
PADEC - Coq Library

Library Padec.KClustering.KClustering_algo

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 Bool.
From Coq Require Import ZArith.

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Spanning_Tree.
From Padec Require Import FoldRight.
From Padec Require Import KClustering_specification.

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

Algorithm for KClustering:

computation of alpha, parent in cluster and cluster head
usage:
forall Channels, exists an Algorithm (the one built here) (uses Channels) forall Network using Channels, KClustering_algo meets its specification defined on (some) Network and Channels.

K-Clustering Algorithm

Section KClustering_algo.

Channel interface definitions

The algorithm requires totally ordered channels
  Context {Chans: Channels}.

  Class OrderedChannels :=
    {
      ltC: relation Channel;
      ltC_dec: Decider ltC;
      ltC_compat:> Proper fequiv ltC;
      ltC_trans: forall x y z, ltC x y -> ltC y z -> ltC x z;
      ltC_strict: forall x y, ltC x y -> ~ x == y;
      ltC_total: forall x y, x == y \/ ltC x y \/ ltC y x
    }.
  Notation minC := (min _ ltC_dec).
Definition minC x y := (if ltC_dec x y then x else y).

Algorithm definitions

The algorithm also requires identities on nodes: to refer the cluster head of the node, refer the identity of this cluster head
  Class KC_algo_tools :=
    {
      OrdChans: OrderedChannels;
      IdNode: Type;
      Id_setoid:> Setoid IdNode;
      Id_dec: Decider (equiv (A := IdNode))
    }.

  Context {KCT: KC_algo_tools}.
  Existing Instance OrdChans.

Read-only state of a node for the algorithm

  Record KCROState :=
    {
      Par: option Channel;
      id: IdNode;
      
      KCpeers_reverse: list (Channel * Channel);
      KCpr_assume: lpeers_reverse_assume KCpeers_reverse
    }.

  Definition KCpeers :=
    (fun ro: KCROState => llpeers (KCpeers_reverse ro)).
  Definition KCreverse :=
    (fun ro: KCROState => llreverse (KCpeers_reverse ro)).

  Instance KCreverse_local_compat:
    forall ro, Proper fequiv (KCreverse ro).

  Definition eqROS :=
    (fun (x y: KCROState) =>
       Par x == Par y /\ id x == id y /\
       equivlistA equiv (KCpeers_reverse x) (KCpeers_reverse y)).

  Global Instance eqROS_equiv: Equivalence eqROS.

  Global Instance KCROState_setoid: Setoid KCROState :=
    {| equiv := eqROS |}.

State of a node for the algorithm

  Lemma KCROState_dec: Decider (equiv (A := KCROState)).

  Record KCState :=
    mkState {
        alpha: Z;
        parCl: option Channel;
None means p itself
        hd: IdNode;
        KCROpart:> KCROState
      }.

Equality on states (decidable equivalence)
  Definition eqS :=
    (fun (x y: KCState) =>
       alpha x == alpha y /\ hd x == hd y /\
       parCl x == parCl y /\ KCROpart x == KCROpart y).

  Global Instance eqS_equiv: Equivalence eqS.

  Global Instance KCState_setoid: Setoid KCState := {| equiv := eqS |}.

  Lemma KCState_dec: Decider eqS.

Compatibility on states

  Global Instance alpha_compat: Proper fequiv alpha.

  Global Instance Par_compat: Proper fequiv Par.

  Global Instance id_compat: Proper fequiv id.

  Global Instance parCl_compat: Proper fequiv parCl.

  Global Instance hd_compat: Proper fequiv hd.

  Instance KCROpart_compat: Proper fequiv KCROpart.

  Instance KCpeers_reverse_compat:
    Proper (equiv ==> equivlistA equiv) KCpeers_reverse.

  Instance KCpeers_compat: Proper (equiv ==> equivlistA equiv) KCpeers.

  Lemma KCreverse_compat:
    forall sx sy: KCROState,
      sx == sy ->
      forall c, InA equiv c (KCpeers sx) -> KCreverse sx c == KCreverse sy c.

The Parameter K itself (from K-Clustering)

  Context {KCP: KClustering_parameters}.

Functions used for the definition of run

  Section Run_definition.

    Variable self_state: KCState.
    Variable peer_state: Channel -> option KCState.

Access to children in the spanning tree (made of Par)
    Definition lPar :=
      (fun c => option_rect (fun _ => option Channel)
                            (fun s: KCState => Par (KCROpart s)) None
                            (peer_state c)).

    Notation children :=
      (Local_Children (KCpeers self_state) lPar
                      (KCreverse self_state)).

Access to states of the children in the spanning tree (made of Par) -- same order as children
    Definition ChildrenStates: list KCState := map_filter peer_state children.

Access to values of alpha in the states of the children in the spanning tree (made of Par) -- same order as children
    Definition ChildrenAlphas: list Z := List.map alpha ChildrenStates.

    Definition _IsShort (_alpha: Z): bool := _alpha <? k.
    Definition _IsTall (_alpha: Z): bool := _alpha >=? k.

    Global Instance _IsShort_compat: Proper fequiv _IsShort.

    Global Instance _IsTall_compat: Proper fequiv _IsTall.

Access to short values of alpha among children
    Definition ShortAlphas: list Z := List.filter _IsShort ChildrenAlphas.

Access to tall values of alpha among children
    Definition TallAlphas: list Z := List.filter _IsTall ChildrenAlphas.

Maximum value of alpha among the short children
    Definition MaxAShort: Z := List.fold_right Z.max (-1) ShortAlphas.
Minimum value of alpha among the tall children
    Definition MinATall: Z := List.fold_right Z.min (2 * k + 1) TallAlphas.

New value for alpha
    Definition NewAlpha: Z :=
      if Z_le_gt_dec (MaxAShort + MinATall + 2) (2 * k) then
        MinATall + 1
      else
        MaxAShort + 1.

Does this channel corresponds to the tall child with minimum alpha value?
    Definition isMinATalls (c: Channel): bool :=
      option_rect (fun _ => bool)
                  (fun qs => (alpha qs) =? MinATall) false
                  (peer_state c).

Computes the minimum channel among the ones for which isMinATalls is true, i.e. among the tall children with minimum alpha value.
    Definition MinIDMinATall: option Channel :=
      match (List.filter isMinATalls children) with
      | nil => None
      | hd::tl => Some (List.fold_right minC hd tl)
      end.

New value for parCl
    Definition NewparCl: option Channel :=
      if (alpha self_state) <? k then (Par self_state)
      else if (alpha self_state) =? k then None
           else MinIDMinATall.

Is this node a cluster head (according to alpha and Par)?
    Definition IsClusterHead: bool :=
      ((alpha self_state) =? k)
      ||
      (_IsShort (alpha self_state) &&
                dec2b (A := option Channel) (eqoptionA_dec Channel_dec)
                (Par self_state) None).

New value for head
    Definition NewHead: IdNode :=
      if (IsClusterHead) then (id self_state)
      else match (parCl self_state) with
           | None => (hd self_state)
           | Some pcl =>
             match (peer_state pcl) with
             | None => (hd self_state)
             | Some ps => (hd ps)
             end
           end.

Alpha action enabled
    Definition alpha_enabled_b: bool :=
      match (Z.eq_dec (alpha self_state) NewAlpha) with
      | left _ => false
      | right _ => true
      end.
    Definition alpha_enabled: Prop := (alpha_enabled_b = true).

ParCl action enabled
    Definition parCl_enabled_b: bool :=
      match (eqoptionA_dec Channel_dec (parCl self_state) (NewparCl)) with
      | left _ => false
      | right _ => true
      end.
    Definition parCl_enabled: Prop := (parCl_enabled_b = true).

Head action enabled
    Definition hd_enabled_b: bool :=
      match (Id_dec (hd self_state) (NewHead)) with
      | left _ => false
      | right _ => true
      end.
    Definition hd_enabled: Prop := (hd_enabled_b = true).

run_algorithm
    Definition run_algorithm: KCState :=
      if alpha_enabled_b then
        mkState NewAlpha (parCl self_state) (hd self_state)
                (KCROpart self_state)
      else if parCl_enabled_b then
             mkState (alpha self_state) NewparCl (hd self_state)
                     (KCROpart self_state)
           else if hd_enabled_b then
                  mkState (alpha self_state) (parCl self_state)
                          NewHead (KCROpart self_state)
                else self_state.

  End Run_definition.

Locality and Compatibility of definitions used in run_algorithm

  Section Run_definition_Locality.

    Instance lPar_compat: Proper (fequiv ==> equiv ==> equiv) lPar.

    Lemma lPar_locality:
      forall ns1 ns2 c, ns1 c == ns2 c -> lPar ns1 c == lPar ns2 c.

    Global Instance ChildrenStates_compat:
      Proper (equiv ==> fequiv ==> equivlistA equiv) ChildrenStates.

    Lemma ChildrenStates_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        equivlistA equiv (ChildrenStates s1 ns1) (ChildrenStates s2 ns2).

    Global Instance ChildrenAlphas_compat:
      Proper (equiv ==> fequiv ==> equivlistA equiv) ChildrenAlphas.

    Lemma map_eq_locality A {SA: Setoid A} B {SB: Setoid B}:
      forall (f1 f2: A -> B) (l1 l2: list A),
        equivlistA equiv l1 l2 ->
        Proper fequiv f1 -> Proper fequiv f2 ->
        (forall a, InA equiv a l1 -> f1 a == f2 a) ->
        equivlistA equiv (map f1 l1) (map f2 l2).

    Lemma ChildrenAlphas_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        equivlistA equiv (ChildrenAlphas s1 ns1) (ChildrenAlphas s2 ns2).

    Global Instance ShortAlphas_compat:
      Proper (equiv ==> fequiv ==> equivlistA equiv) ShortAlphas.

    Lemma ShortAlphas_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        equivlistA equiv (ShortAlphas s1 ns1) (ShortAlphas s2 ns2).

    Global Instance TallAlphas_compat:
      Proper (equiv ==> fequiv ==> equivlistA equiv) TallAlphas.

    Lemma TallAlphas_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        equivlistA equiv (TallAlphas s1 ns1) (TallAlphas s2 ns2).

    Global Instance MaxAShort_compat:
      Proper (equiv ==> fequiv ==> equiv) MaxAShort.

    Lemma MaxAShort_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        MaxAShort s1 ns1 = MaxAShort s2 ns2.

    Global Instance MinATall_compat:
      Proper (equiv ==> fequiv ==> equiv) MinATall.

    Lemma MinATall_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        MinATall s1 ns1 = MinATall s2 ns2.

    Global Instance NewAlpha_compat:
      Proper (equiv ==> fequiv ==> equiv) NewAlpha.

    Lemma NewAlpha_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        NewAlpha s1 ns1 = NewAlpha s2 ns2.

    Global Instance isMinATalls_compat:
      Proper (equiv ==> fequiv ==> equiv ==> equiv) isMinATalls.

    Lemma isMinATalls_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        forall c, InA equiv c (KCpeers s1) ->
                  isMinATalls s1 ns1 c = isMinATalls s2 ns2 c.

    Global Instance MinIDMinATall_compat:
      Proper (equiv ==> fequiv ==> equiv) MinIDMinATall.

    Lemma MinIDMinATall_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        MinIDMinATall s1 ns1 == MinIDMinATall s2 ns2.

    Global Instance NewparCl_compat:
      Proper (equiv ==> fequiv ==> equiv) NewparCl.

    Lemma NewParCl_locality:
      forall (s1 s2: KCState) ns1 ns2,
        s1 == s2 ->
        Proper fequiv ns1 -> Proper fequiv ns2 ->
        (forall c, InA equiv c (KCpeers s1) -> ns1 c == ns2 c) ->
        NewparCl s1 ns1 == NewparCl s2 ns2.

    Global Instance IsClusterHead_compat: Proper fequiv IsClusterHead.

    Global Instance NewHead_compat: Proper fequiv NewHead.

    Global Instance alpha_enabled_b_compat:
      Proper fequiv alpha_enabled_b.

    Global Instance alpha_enabled_compat:
      Proper fequiv alpha_enabled.

    Global Instance parCl_enabled_b_compat:
      Proper fequiv parCl_enabled_b.

    Global Instance parCl_enabled_compat:
      Proper fequiv parCl_enabled.

    Global Instance hd_enabled_b_compat: Proper fequiv hd_enabled_b.

    Global Instance hd_enabled_compat: Proper fequiv hd_enabled.

    Global Instance run_algorithm_compat:
      Proper fequiv run_algorithm.

  End Run_definition_Locality.

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

The algorihtm!!

  Global Instance KC_algo: Algorithm.

  Global Instance KC_Stable: Stable_Variable KC_algo KCROpart.

End KClustering_algo.

Section Projections.

  Context {Chans: Channels}
          {KCP: KClustering_parameters} {KCT: KC_algo_tools}
          {Net: Symmetric_Network}.

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

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

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

  Definition id_part := (fun (g: Env) n => id (g n)).

  Instance Par_part_compat: Proper fequiv Par_part.

  Instance alpha_part_compat: Proper fequiv alpha_part.

  Instance id_part_compat: Proper fequiv id_part.

End Projections.

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