Coq Library
Tools

#### Global Imports

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

#### Local Imports

Open Scope nat_scope.
Open Scope signature_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)

# The Algorithm

/contains:/ Dijkstra first algorithm for token circulation on a rooted ring
/assume:/ Parameter k>1
• Definition of the state of a process (ROState and State, equivalence, decidability, getter, compatibility)
• Definition of the algorithm:
• > function *simple_run* contains the algorithm as written in the original paper, using two arguments (the current state of the node and the current state of its predecessor);
• > function *run* calls simple_run with the proper arguments, as awaited by PADEC in class Algorithm.

Section Dijkstra_algo.

Context {Chans: Channels}.

Class Dijkstra_parameters :=
{

## Parameter k of the algoritm: node values are incremented

modulo k
k: nat;
H_k: k > 1
}.

Assuming the Dijkstra parameter and hypothesis:
Context {DP: Dijkstra_parameters}.
Let H_k := H_k.

## State of a Node in the Algorithm

### Read Only Part of a State; local topology information

• the channel to the predecessor node and
• a Boolean value meaning that the node is a root in the ring
Record Dijkstra_ROState := mkROState {
predc: Channel;
root: bool
}.

Notation eqROS := (fun (x y: Dijkstra_ROState) =>
predc x == predc y /\ root x = root y).

Instance eqROS_equiv: Equivalence eqROS.

Global Instance Dijkstra_ROState_setoid: Setoid Dijkstra_ROState :=
{|equiv := eqROS|}.

### State of a node

• a natural counter, v, smaller than k
• the local topology read-only part as defined above

Record Dijkstra_State := mkState {
vltk: { n: nat | n <= k-1};
Dijkstra_ROpart :> Dijkstra_ROState
}.

Notation eqS := (fun (x y: Dijkstra_State) =>
vltk x == vltk y /\ Dijkstra_ROpart x == Dijkstra_ROpart y).

Instance eqS_equiv: Equivalence eqS.

Global Instance State_setoid :Setoid Dijkstra_State := {|equiv := eqS|}.

### Getter for vltk

Definition v (s: Dijkstra_State): nat := proj1_sig (vltk s).

Lemma v_ltk: forall (s: Dijkstra_State), v s < k.

Lemma v_plus_0: forall (s: Dijkstra_State), (v s + 0) mod k = v s.

### Equality and Compatibility properties on State

Lemma Dijkstra_ROState_dec: Decider (equiv (A := Dijkstra_ROState)).

Lemma Dijkstra_State_dec: Decider (equiv (A := Dijkstra_State)).

Instance v_compat: Proper fequiv v.

Instance predc_compat_RO: Proper fequiv predc.

Instance root_compat_RO: Proper fequiv root.

Instance Dijkstra_ROpart_compat: Proper fequiv Dijkstra_ROpart.

Instance predc_compat: Proper (equiv (A:=Dijkstra_State) ==> equiv) predc.

Instance root_compat: Proper (equiv (A:=Dijkstra_State) ==> equiv) root.

Section Run_definition.

"+1" on natural modulo k
Program Definition Smod (nltk: {n: nat| n <= k-1}):
{n: nat| n <= k-1} := (S (proj1_sig nltk) mod k).

Global Instance Smod_compat: Proper fequiv Smod.

Lemma Smod_neq: forall (v: {n: nat| n <= k-1}), ~v == (Smod v).

## Run Function for the Algorithm

• when the root value is equal to the value of its predecessor, its value increments modulo k
• when the value of a non-root node is different from that of its predecessor, the node gets the value of its predecessor
Function simple_run contains the algorithm as written in papers, using two arguments (the current state of the node and the current state of its predecessor).
Function run_algorithm calls simple_run with the arguments, as awaited by PADEC in class Algorithm.

Definition simple_run (s s_pred: Dijkstra_State): Dijkstra_State :=
if root s then
if Nat.eq_dec (v s) (v s_pred) then
{| vltk := Smod (vltk s); Dijkstra_ROpart := s |}
else
s
else
if Nat.eq_dec (v s) (v s_pred) then
s
else
{| vltk := vltk s_pred; Dijkstra_ROpart := s |}.

Definition run_algorithm
(s: Dijkstra_State)
(peer_state: Channel -> option Dijkstra_State)
: Dijkstra_State :=
match peer_state (predc s) with
None => s
| Some s_pred => simple_run s s_pred
end.

End Run_definition.

## Definition of The Algorithm

Instance Dijkstra_algo: Algorithm :=
{| State := Dijkstra_State; run := run_algorithm; |}.

### Stability for the Read-Only Part of the Run Function

Lemma ROpart_stable:
forall s sn, Dijkstra_ROpart (run_algorithm s sn) =~= Dijkstra_ROpart s.

Global Instance Dijkstra_Stable:
Stable_Variable Dijkstra_algo Dijkstra_ROpart.

End Dijkstra_algo.

Unset Implicit Arguments.
Close Scope nat_scope.
Close Scope signature_scope.