PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_Z

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

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

Local Imports

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.

Diskstra's first token ring algorithm

Potential Z

/contains:/ Definitions and results about Z and convexity
/assumes:/ Parameter k>1; the network is a unidirectional rooted ring; assumption: N <= k

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
For example,
  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
  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:
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.
  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 i.e. Z g = min { z < k | convex g ((v g Root + z) mod k) }
For example, with k=7,
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
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).
  Lemma Z_0_Token_Root_Leg_state:
    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 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:
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)).
  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).
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 value of n is vR, then this vR disappears: In both cases, we get a convex configuration hence Z g' = 0.
If the value vn of n is not vR, then we have 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.