PADEC - Coq Library

# Library Padec.Dijkstra.Dijkstra_Z

From Coq Require Import SetoidList.

From Coq Require Import SetoidClass.

From Coq Require Import ZArith.

From Coq Require Import Lia.

From Coq Require Import Bool.

From Coq Require Import SetoidClass.

From Coq Require Import ZArith.

From Coq Require Import Lia.

From Coq Require Import Bool.

From Padec Require Import SetoidUtil.

From Padec Require Import NatUtils.

From Padec Require Import ListUtils.

From Padec Require Import Count.

From Padec Require Import All_In.

From Padec Require Import Algorithm.

From Padec Require Import RelModel.

From Padec Require Import Exec.

From Padec Require Import P_Q_Termination.

From Padec Require Import Fairness.

From Padec Require Import Self_Stabilization.

From Padec Require Import Ring_topology.

From Padec Require Import Dijkstra_algo.

From Padec Require Import Dijkstra_common.

Open Scope nat_scope.

Set Implicit Arguments.

From Padec Require Import NatUtils.

From Padec Require Import ListUtils.

From Padec Require Import Count.

From Padec Require Import All_In.

From Padec Require Import Algorithm.

From Padec Require Import RelModel.

From Padec Require Import Exec.

From Padec Require Import P_Q_Termination.

From Padec Require Import Fairness.

From Padec Require Import Self_Stabilization.

From Padec Require Import Ring_topology.

From Padec Require Import Dijkstra_algo.

From Padec Require Import Dijkstra_common.

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

- 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

- 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

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

Existing Instance Dijkstra_RO_assumption.

This part of the proof requires the additional property that
the number of nodes in the ring is smaller than or equal to 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.

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

forall n n', Between Root n' n -> v (g n) = vr -> v (g n') = vr.

The convex predicate is weakly-decidable

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.

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

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

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

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

## Non-convex properties

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

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

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

Notation Conv g := (fun j => convex_b g ((v (g Root) + j) mod k)).

Definition Z (g: Env): nat := min_below (Conv g) 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
The potential Z is always smaller than k since there
always exists a value < k, such that convex holds
(see Lemma convex_exists above).

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

forall (g: Env) (pg: Proper fequiv g) (assume: Assume g) (p: nat),

Z g = p <-> is_minimum (Conv g) p.

## When Z is zero...

Lemma pot_0_equiv:

forall (g: Env) (pg: Proper fequiv g) (assume: Assume g),

Z g = 0 <-> convex g (v (g Root)).

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.

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

Lemma Z_0_Token_Root_Leg_state:

forall g, Assume g -> Proper fequiv g ->

Z g = 0 -> Token g Root -> Leg_state g.

forall g, Assume g -> Proper fequiv g ->

Z g = 0 -> Token g Root -> Leg_state g.

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

- 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

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.

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.

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

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.

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

- 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

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

configuration, it decreases whatever be the node which moves.- 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)

- the root still holds vR
- its successort may also holds vR if it has moved

- vR < vn < vR+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'.

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

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.

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.

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.

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.

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

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.

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.