Coq Library
Tools

#### Global Import

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

#### Local Import

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

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

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

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

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 :=

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