PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.KClustering.KClustering_specification

A Framework for Certified Self-Stabilization
PADEC Coq Library

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