PADEC - Coq Library

Library Padec.KClustering.KClustering_specification

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Import

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

Local Import

From Padec Require Import SetoidUtil.
From Padec Require Import RelationA.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Count.

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

Specification for a k-clustering algorithm

Section KClustering_Specification.

Problem Definition

Let assume an algorithm and a positive number k

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

  Class KClustering_parameters :=
    {

The parameter K itself (from K-Clustering)

      k: Z;
      k_pos: k > 0
    }.
  Context {KCP: KClustering_parameters}.

Every terminal configuration of the system should contain a

k-clustering defined as follows:

Predicate that defines a k-cluster and a cluster head

(kCluster h n) means that node n is the cluster of node h,

h is a clusterhead, precisely, it is the clusterhead of the k-cluster { n | kCluster h n }. We can derive the predicate clusterHead h that defines: (exists n, kCluster h n), hence (kCluster h h)

Variable (kCluster: Env -> Node -> Node -> Prop).
Notation clusterHead g h := (kCluster g h h).

Definition of a path in the network (using existing channels)

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

  Definition is_path := chain is_neighbor_of.

First part of the specification:

The predicate kCluster actually designs a k-Clustering when

for any cluster head h, ie, such that (clusterHead h), the set of nodes n such that (kcluster h n) represents a k-cluster, namely,

forall n, kCluster h n -> exists p, p is a path from h to n and (length p) <= k, any element in this path being in the k-cluster of h (see kCluster_OK)
the set of sets { kCluster h | h, clusterHead h } is a partition of the set of nodes, namely,

forall n, exists h, kCluster h n /\ forall n h h', kCluster h n
- > kCluster h' n -> eqN h h' (see partition_OK)
  
  The complete check is performed using kClustering_SPEC.

kCluster actually definies a k-cluster:

  Definition kCluster_OK (g: Env): Prop :=
    forall (h: Node),
      clusterHead g h ->
      forall (n: Node), kCluster g h n ->
                        exists (p: list Node ),
                          is_path h p n /\
                          (forall q, InA equiv q p -> kCluster g h q ) /\
                          (Z_of_nat (length p) <= k)%Z.

The set of k-clusters is a partition on the set of nodes:

  Definition partition_OK (g: Env): Prop :=
    forall (n: Node), (exists (h: Node ), kCluster g h n ) /\
                      forall (h h': Node), kCluster g h n -> kCluster g h' n -> h == h'.

  Definition kClustering_SPEC (g: Env): Prop :=
    kCluster_OK g /\ partition_OK g.

Second part of the specification:

the k-clustering contains no more than floor((n-1)/(k+1))+1 k-clusters

Section Count.

The set of clusterheads

    Definition ClusterHeads (g: Env) := { n : Node | clusterHead g n }.

    Definition counting_OK (g: Env): Prop :=
      exists (N C: nat ),
        Num_Card Same Node N /\ Num_Card Same (ClusterHeads g) C /\
        (N - 1 >= S (Z.to_nat k) * (C - 1))%nat.

n.b.: N stands for the number of nodes in the network, C stands for the number of clusterheads, hence for the number of k-clusters.

End Count.

Section With_ID.

Third part of the specification:

We require that each node is locally aware of its clusterhead and has a way to route to it

there exists a local function (on state of a node) clusterHeadID: State -> ID which represents the clusterhead of the node (n.b.: it requires a fully identified network)
there exists a local function (on a state of a node) clusterParent: State -> Channel which allows to build path in the cluster from the node to its clusterhead (with length smaller or equal to k)

Identities on nodes: local and unique id

    Context {IDType: Type} `{ID_setoid: Setoid IDType}.
    Variable (ID: State -> IDType)
             (uniqueID:
                forall (g: Env),
                  Proper pequiv g ->
                  forall n1 n2, ID (g n1) == ID (g n2) -> n1 == n2).

Identity of the cluster head on each (local) node

    Variable (clusterHeadID: State -> IDType).

    Definition clusterHeadID_OK (g: Env): Prop :=
      forall (h n: Node), kCluster g h n <-> ID (g h) == clusterHeadID (g n).

Route to cluster head

Variable (clusterParent: State -> option Channel).

Definition of a route using cluster parent:

    Definition is_cluster_parent (g: Env) (y x: Node): Prop :=
      match (clusterParent (g x))
      with None => False
      | Some c => peer x c == Some y end.

A route from a node to its clusterhead is a path made of clusterParent pointers (cluster_path') such that any intermediate node remains in the same k-cluster (agreed_cluster_path).

    Definition cluster_path (g: Env) := (chain (is_cluster_parent g)).

    Definition agreed_cluster_path
               (g: Env) (n': Node) (p: list Node) (n: Node): Prop :=
      cluster_path g n' p n /\
      forall (q: Node), InA equiv q p ->
                        clusterHeadID (g n') == clusterHeadID (g q).

    Lemma cluster_path_is_path:
      forall (g: Env) (x y: Node) (p: list Node),
        agreed_cluster_path g x p y -> is_path x p y.

Any node has a route that reaches its clusterhead in at most k hops, staying in the cluster all along the route.

    Definition cluster_path_OK (g: Env): Prop :=
      forall (h: Node), clusterHead g h ->
                        forall (n: Node),
                          kCluster g h n ->
                          exists (p: list Node ), agreed_cluster_path g h p n /\
                                                 (Z_of_nat (length p) <= k)%Z.

Third part of the specification

Definition kClustering_ID_SPEC (g: Env): Prop :=
clusterHeadID_OK g /\ cluster_path_OK g.

Complete Stronger Specification

    Definition kClustering_SPEC_strong (g: Env): Prop :=
      kClustering_SPEC g /\ counting_OK g /\ kClustering_ID_SPEC g.

    Lemma kClustering_ID_SPEC_stronger:
      forall (g: Env), kClustering_ID_SPEC g -> kCluster_OK g.

Alternative complete specification

    Lemma kClustering_SPEC_strong_alt:
      forall (g: Env), kClustering_SPEC_strong g <->
                       kClustering_ID_SPEC g /\
                       partition_OK g /\ counting_OK g.

  End With_ID.

End KClustering_Specification.

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