Coq Library
Tools

#### Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Omega.
From Coq Require Import Bool.

#### Local Imports

Open Scope nat_scope.
Set Implicit Arguments.

# Diskstra's first token ring algorithm

• Proof of self-stabilization and specification
• Proof of a complexity bound in steps
• Proof that this complexity bound is exact (by building a worst case prefix of execution)

# Potential Z

/contains:/ Definitions and results about Z and convexity
/assumes:/ Parameter k>1; the network is a unidirectional rooted ring; assumption: N <= k
• convex: A configuration is said convex w.r.t. to a given value vr if vr is the value of Root and all the nodes holding this value vr shape a convex sequence of vr-valued nodes made of consecutive successors of the root. Convex for a value vr is equivalent to
• vr is the value of the root and it is actually convex
• otherwise, no node holds the value vr
There always exists a value that satisfies convex (This is due to the fact that N <= k).
• Z: The potential Z of a configuration g is
• 0 if g is convex for the value of the Root
• the distance to the closest absent value from the Root (modulo k), otherwise
i.e. Z g = min { z < k | convex g ((v g Root + z) mod k) }
• When Z is null: 'Z g = 0' is equivalent to 'g is convex for the root value'; and a configuration where Z is 0 and where the root holds a token is legitimate.
• Z evolution during a step from an illegitimate configuration:
• Z decreases when the root executes
• Z does not increase.
• Bound on Z: Z is upper bounded by N-1. If the configuration is convex, the result is trivial. We consider a non-convex configuration. We use counting arguments which stands on Lemma all_here (that asserts that every value between 0 and Z-1 is represented in the ring).
• When Z g is N - 1: g is of a particular shape. There exists a non-root node, which is not the successor of the root, that holds the root value; moreover, every value from (v g Root + 1) mod k to (v g Root + N-2) mod k is held by a single node. From this observation, easily follows that Z g' <= N - 2.

Section Dijkstra_Z.

Context {Chans: Channels}
{Net: Network}
{RURN: Rooted_Unidirectional_Ring_Network Net}
{DP: Dijkstra_parameters}.

Notation Algo := Dijkstra_algo.
Notation Root := (RURN_root (Net := Net)).
Notation Ring := (URN_topo (Net := Net)).
Notation Env := (Env (Net := Net) (Algo := Dijkstra_algo)).
Let H_k := H_k.

Notation N := (Ring_size Root).

This part of the proof requires the additional property that the number of nodes in the ring is smaller than or equal to k.
Hypothesis HNk: N <= k.

## Convexity

A configuration is said convex wrt to a given value vr if
• vr is the value of Root and
• all the nodes holding this value vr shape a convex sequence of vr valued nodes made of consecutive successors of the root.
For example,
• Root->5 5 5 6 3 4 0 is convex for vr = 5
• Root->5 5 5 6 3 4 0 is not convex for any vr <> 5
• Root->5 5 5 6 3 4 5 is not convex for any vr
• Root->5 5 6 2 5 3 0 is not convex for any vr
Definition convex (g: Env) (vr: nat): Prop :=
forall n n', Between Root n' n -> v (g n) = vr -> v (g n') = vr.

The convex predicate is weakly-decidable
Lemma convex_dec: forall (g: Env) (vr: nat),
{Proper fequiv g -> convex g vr} + {~convex g vr}.

Boolean getters for convex
Definition convex_b (g: Env) (vr: nat): bool :=
match convex_dec g vr with left _ => true | right _ => false end.

Lemma convex_b_true:
forall g (pg: Proper fequiv g) V, convex g V <-> convex_b g V = true.

Lemma convex_b_false:
forall g (pg: Proper fequiv g) V, ~convex g V <-> convex_b g V = false.

Convex for a value vr is equivalent to
• vr is the value of the root and it is actually convex
• otherwise, no node holds the value vr
Lemma convex_equiv:
forall (g: Env) (pg: Proper fequiv g) (V: nat),
convex g V <->
V = v (g Root) /\ convex g (v (g Root)) \/
forall n, V <> v (g n).
There always exists a value that satisfies convex.
This is due to the fact that N <= k.
Here follows the outline of the proof.
If the value of the root is convex, then we are done. Otherwise, the value we are looking for is not in the ring (see Lemma convex_equiv).
We now focus on the case when the root value is not convex. We first prove that the number of values in the ring is smaller or equal to N (the ring size), using the Library Count. present x := exists n, v (g n) = x. Num_Card Smaller (@eqSig nat eq present) N In particular, we exhibit the following injection relation:
• a present value x corresponds to a natural value (less than N) j when x is the value of the node located at j successor edges from the root.
Let nV be the number values present in the ring: Num_Card Same (eqSig present) nV In particular, we have nV <= N <= k (using transitivity of Card).
Let nP be the number of values that satisfy convex (i.e. absent from the ring). P := fun V : nat => V < k /\ convex g V Num_Card Same (eqSig P) nP We show that nV + nP = k using (disjoint union of Card).
Now comes the proof: it is split in two cases, depended if nV is less than k or equal to k.
• Case nV < k. We show that nP >0 and then pick an element V from P (i.e., such that V < k /\ convex g V].
• Case nV = k. Then the number of present is exactly N, the number of nodes in the ring: Card Same (@eqSig _ eq present) eqN From this hypothesis, we can show that convex g (v (g Root)), a contradiction.
Indeed, if the root is the unique node to hold this value, we are done. Otherwise, we count the number of values present in the ring, except the one of the root, using: present_outside_Root := fun x => exists n : Node, ~eqN n Root /\ v (g n) = x and obtain that: it is less that N and also equal to the number of values present in the ring, that is N, a contradiction.
Lemma convex_exists:
forall g, Proper fequiv g -> Assume g ->
exists V, V < k /\ convex g V.

## Non-convex properties

When the configuration is not convex, there exists a non-root node that holds the root value (this directly comes from the definition)
Lemma nonconvex_Root_direct:
forall g, Proper pequiv g ->
~ convex g (v (g Root)) ->
exists n n', Between Root n' n /\
v (g n) = v (g Root) /\
v (g n') <> v (g Root).

Lemma nonconvex_Root:
forall g, Proper pequiv g ->
~ convex g (v (g Root)) ->
exists n, ~ n == Root /\
v (g n) = v (g Root).

## Z

The potential Z of a configuration g is
• 0 if g is convex for the value of the Root
• the distance to the closest absent value from the Root (modulo k), otherwise
i.e. Z g = min { z < k | convex g ((v g Root + z) mod k) }
For example, with k=7,
• Root->5 5 5 6 3 4 0 has potential 0
• Root->5 5 5 6 3 4 5 has potential 2 (since the closest absent value is 0, at distance 2 from 5)
• Root->5 5 6 2 5 3 0 has potential 3 (since the closest absent value is 1, at distance 3 from 5)
Conv: Boolean function, (Conv g j) returns true when g is convex for the value (vR + j) mod k, where vR is the value of the root.
Notation Conv g := (fun j => convex_b g ((v (g Root) + j) mod k)).

Definition Z (g: Env): nat := min_below (Conv g) k.

n.b.: for a function f and a value k, min_below f n is specified by: min_below f n = n /\ (forall x, x < n -> f x = false) \/ min_below f n < n /\ is_minimum f (min_below f n)
where, as expected, (is_minimum f m) means: f m = true /\ (forall m', m' < m -> f m' = false)
(is_minimum f m) is hence the minimum natural value on which f returns true. (min_below f n) returns
• either n if no value above n allows f to return true
• or the minimum value above n on which f is true.
The potential Z is always smaller than k since there always exists a value < k, such that convex holds (see Lemma convex_exists above).
Lemma Z_ltk:
forall (g: Env) (pg: Proper fequiv g) (assume: Assume g),
Z g < k.

The potential Z is actually the minimum among the convex values
Lemma Z_min:
forall (g: Env) (pg: Proper fequiv g) (assume: Assume g) (p: nat),
Z g = p <-> is_minimum (Conv g) p.

## When Z is zero...

'Potential Z is 0' is equivalent to 'the configuration is convex for the root value'.
Lemma pot_0_equiv:
forall (g: Env) (pg: Proper fequiv g) (assume: Assume g),
Z g = 0 <-> convex g (v (g Root)).

In a legitimate configuration, Z is 0, since the configuration is convex. To prove this, we use the characterization of a legitimate configuration ls_charac.
Lemma Leg_state_pot_0:
forall g, Proper pequiv g -> Assume g -> Leg_state g ->
Z g = 0.
A configuration where Z is 0 and where the root holds a token is legitimate. Indeed, in such configuration, every node holds one and the same value (the root one).

## Z-evolution during a step from an illegitimate configuration

The potential Z decreases when the root executes from a illegitimate configuration.
We first show that the potential at g is not null, using Z_0_Token_Root_Leg_state. (Indeed, every value in the ring would be equal to the one of the root, hence there would be a unique token, hence this would be a legitimate configuration.)
Now, we have:
• the Root holds a Token, i.e., its value is equal to the value of its predecessor (a) Token g Root and (b) v (g Root) = v (g (Pred Root))
• the Root increments its value modulo k (c) v (g' Root) = (v (g Root) + 1) mod k
To show that the potential is g' has decreased, we rewrite potential as minimum (using Z_min) and applies Lemma is_minimum_lt that says that if M1 (resp. M2) is the minimum of some set A1 (resp. A2) and if for every value in A1, there exists a smaller value in A2, then M2 is smaller than M1. Hence, for any value x such that (x + v (g Root)) mod k is absent from the ring in configuration g, we have to build a smaller value x' such that (x + v (g Root)) mod k is absent from the ring in configuration g.
If x >= k, we just pick the value given by convex_exists in g'; as this value is smaller than k, we are done.
If x < k, x cannot be 0 (resp. 1 otherwise the potential in g (resp. in g') is null. Then the value we are looking for is (x-1), that is to say: we prove that the configuration g' is convex for value (v (g' Root) + (x - 1)) mod k = (v (g Root) + x) mod k. Namely, we prove that forall n, (v (g Root) + x) mod k <> v (g' n) since no value appears in the ring but ((v (g Root) + 1) mod k) and 1 < x < k.
Lemma Z_decreases:
forall g, Assume g -> ~Leg_state g ->
forall g', Step g' g ->
has_moved_b g' g Root = true ->
Z g' < Z g.

The potential Z does not increase from a illegitimate configuration.
We rewrite potentials as minimum (using Z_min) and applies Lemma is_minimum_le that says that if M1 (resp. M2) is minimum of some set A1 (resp. A2) and if for every value in A1, there exists a smaller or equal value in A2, then M2 is smaller than or equal to M1.
We first restrict to values smaller than k in M1 (i.e. values x such that (convex g ((v (g Root) + x) mod k)) holds). - If x is 0, we prove that (convex g' (v (g Root))): since the value is copied from the predecessor when a node moves, this cannot break the convex property for (v (g Root)).
• If x <> 0 then, no node in the ring holds value ((v (g Root) + x) mod k) = ((v (g' Root) + x) mod k). As no new value appears in the step, (convex g ((v (g Root) + x) mod k)) holds.
Lemma Z_does_not_increase:
forall g, Assume g -> ~Leg_state g ->
forall g', Step g' g ->
Z g' <= Z g.

Lemma Z_evolves:
forall g, Assume g -> ~Leg_state g ->
forall g', Step g' g ->
if has_moved_b g' g Root then Z g' < Z g
else Z g' <= Z g.

## Bound on Z

Every value between 0 and pot_with_Root-1 is present at some node in the ring. Indeed, Z is minimum among the convex values (v+j)mod k.
Lemma all_here:
forall g, Assume g -> Proper fequiv g ->
forall x, x < Z g ->
exists n, v (g n) = (v (g Root) + x) mod k.

Z is upper bounded by N-1 If the configuration is convex, the result is trivial. We consider a non convex configuration. We use counting arguments which stands on all_here (that asserts that every value between 0 and Z-1 is represented in the ring).
• presentNR are the nodes which hold a value different from the root. Cardinal = NR
• presentR are the nodes which hold the root value. Cardinal = R
We show that R >=2 due to nonconvex_Root. And that N = NR + R. Hence NR <= N - 2.
Now, Z g - 1 <= NR due to pot_with_root definition. Hence the result.
Lemma Z_lt_N:
forall g, Assume g -> Proper fequiv g -> Z g <= N - 1.

## When Z is N - 1: in a step from a non-legitimate

configuration, it decreases whatever be the node which moves.
SKETCH
Situation : (vR = value of the Root)
There exists a unique non-root node (which neither the successor of the root) which holds vR. For every value between vR+1 et vR+N-2, there exists a unique node which holds this value.
Counting arguments.
In a step of the algorithm,
• If the root moves then the value of the root becomes vR+1 as vR+1+N-2 is absent (and no value can appear) we obtain Z g' <= N-2
• Otherwise, there exists a node n which moves but whose successor does not. (induction which exhibits such a node, the closest from the root)
If the value of n is vR, then this vR disappears:
• the root still holds vR
• its successort may also holds vR if it has moved
In both cases, we get a convex configuration hence Z g' = 0.
If the value vn of n is not vR, then we have
• vR < vn < vR+N-1
n is the only node to hold vn and vn is absent from g'. Hence Z g' < N-1

Section Z_Fully_Decreases.

Variable HN4: N >= 4.
Variable (g: Env) (ass: Assume g).
Variable (g': Env) (step: Step g' g).

Variable (HZ: Z g = N - 1).

Notation pg' := (Step_Proper_l step).
Notation pg := (Step_Proper_r step).

We note presentX x n the predicate which means that node n holds present value x
Definition presentX :=
(fun x n => (v (g Root) + x) mod k = v (g n)).

Instance presentX_compat: Proper pequiv presentX.

Lemma v_inv: forall n, exists x,
x < k /\ (v (g Root) + x) mod k = v (g n) /\
forall x', x' < k -> x' <> x -> ~ presentX x' n.

Lemma v_inv_unique: forall n,
forall x x', presentX x n -> presentX x' n ->
x < k -> x' < k -> x = x'.

The number of non-root nodes is N-1.
Lemma HNR: Num_Card Same {x : Node | ~ x == Root} (N - 1).

Let Ua = { n, ~n==Root /\ exists x < a, x<N-1 /\ presentX x n } Ua_card defines the number of non-root nodes in Ua.
Lemma Ua_card:
forall a, exists Na,
Num_Card Same {n | ~ n == Root /\
(exists x, x < a /\ presentX x n)} Na.

From Lemmas all_here and nonconvex_Root, we know that for each present value in {0, ..., N-2}, there exists a non-root node which holds it.
Lemma AB:
forall x, x < N-1 ->
exists n, ~ n == Root /\ presentX x n.

Let Up_a = { n | ~ n == Root /\ presentX a n } for any value a. Up_a has a cardinality (see Upa_card) which is positive (see Upa). The results are direct from the definition of the set and from Lemma AB.
Lemma Upa_card:
forall a, a < k -> exists Na,
Num_Card Same {n | ~ n == Root /\ presentX a n} Na.

Lemma Upa:
forall a, a < N-1 ->
Num_Card Larger {n | ~ n == Root /\ presentX a n} 1.

We show that forall a in {1, ..., N-1}, |Ua| >= a Induction on a. The base case, for a=1, is provided by nonconvex_Root: this exhibits a non-root node withe the same value as the root. For induction step, we write Ua = U(a-1) Union {n, ~n==Root /\ presentX a n} (This is a disjoint union.) By induction hypothesis, |U(a-1)| >= a - 1 and we can prove that |{n, ~n==Root /\ presentX a n}| >= 1 since Lemma all_here provides a node with present value a.
Lemma Ua:
forall a, a <= N-1 ->
Num_Card Larger
{n | ~ n == Root /\
exists x, x < a /\ presentX x n} a.

The number of non-root nodes with a present value smaller than N-1 is exactly N-1.
Indeed, it is smaller than or equal to the number of non-root nodes, ie N-1 (see HNR) we use the implication of predicates and Inj_impl. It is also greater or equal due to Lemma Ua.
Lemma cc:
Num_Card Same {n | ~ n == Root /\
exists x, x < N-1 /\ presentX x n} (N-1).

Lemma interval_clas:
forall (P: nat -> Prop) (n: nat)
(P_clas: forall x, x < n -> P x \/ ~P x),
(exists x, x < n /\ P x) \/ (forall x, x < n -> ~P x).

Lemma interval_clas':
forall (P: nat -> Prop) (n: nat)
(P_clas: forall x, x < n -> ~P x \/ P x),
(exists x, x < n /\ ~P x) \/ (forall x, x < n -> P x).

Using cc above, we know that the number of non-root nodes with a present value x<N-1 is (N-1) If there exists a non-root node with a non-present value, then by disjoint union of the sets the number of non-root nodes with a present value x<N-1 would be smaller than (N-1).
This proof uses the fact that we can enumerate every natural number between 0 and N-2 in order to check if the value is present of not.
Lemma T1:
forall n, ~ n == Root -> exists x, x < N-1 /\ presentX x n.

Lemma T2:
forall x, x < N-1 -> Num_Card Same {n | ~ n == Root /\
presentX x n} 1.

Lemma S_: forall n1 n2,
~ n1 == Root -> ~ n2 == Root ->
v (g n1) = v (g n2) -> n1 == n2.

Lemma last_to_move:
has_moved_b g' g Root = false ->
exists n, has_moved_b g' g n = true /\
has_moved_b g' g (Succ n) = false.
Lemma Z_fully_decreases: Z g' <= N - 2.

End Z_Fully_Decreases.

End Dijkstra_Z.

Unset Implicit Arguments.
Close Scope nat_scope.