Coq Library
Tools

#### Global Imports

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

#### Local Imports

Set Implicit Arguments.
Open Scope nat_scope.

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

# Complexity Bounds for N= 1 to 3 nodes

/contains:/ I - Proof of the complexity bound (0 steps) for N=1 or 2 II - Proof of the complexity bound (3 maximum steps) for N=3
/assumes:/ Parameter k>1; the network is a unidirectional rooted ring; N <= k
Part I: DTRC Complexity for N=1 or 2 is 0 step obtained directly since every configuration is legitimate
Part II: DTRC complexity for N=3 is 3 steps at most
• Basic facts about the 3-ring (nodes N0(Root) N1 N2)
• Elementary characterization of DTRC states for N=3 * L3_state : 3 non-legitimate steps may be performed (but no more) * L2_state : 2 non-legitimate steps may be performed (but no more) * L1_state : 1 non-legitimate step may be performed (but no more) * L0_state : no non-legitimate step may be performed <-> Leg_state
• These predicates form a partition of DTRC state for N=3
• Characterization of available transitions: * L3_Step_L2_L0 : A L3_state leads to either a L2_state or a L0_state * L2_Step_L1_L0 : A L2_state leads to either a L1_state or a L0_state * L1_Step_L0 : A L1_state leads to either a L0_state
• Decomposition of possible trace based of the above partition and transition graph
Detailled transition table: (!) means node moves (.) means no move L3State == ABA+ (+) means A+1 mod k == B
• transitions : 3 tokens -> 7 choices !!! BAB- !!. BAA !.! BBB !.. BBA .!! AAB .!. AAA ..! ABB
L2State == ABA- (-) means A+1 mod k <> B
• transitions : 3 tokens -> 7 choices !!! CAB !!. CAA !.! CBB !.. CBA .!! AAB .!. AAA ..! ABB
L1State == ABC Transitions: 2 tokens -> 3 choices .!! AAB .!. AAC ..! ABB L0State == Leg_state /ABB : 1 token -> .!. ABB 3 subcase { AAB : 1 token -> ..! AAA \AAA : 1 token -> !.. BAA

Notation Decidable A:= ({A} + {~A}) (only parsing).

Lemma or_dec: forall A B, Decidable A -> Decidable B -> Decidable (A \/ B).
Lemma and_dec: forall A B, Decidable A -> Decidable B -> Decidable (A /\ B).
Lemma not_dec: forall A, Decidable A -> Decidable (~A).

Lemma ITE_bool_f : forall A B (f:A -> B) (b:bool) a1 a2,
f (if b then a1 else a2) = if b then (f a1) else (f a2).

Lemma ITE_sumbool_f : forall PA PB A B (f:A -> B) (sb:{PA}+{PB}) a1 a2,
f (if sb then a1 else a2) = if sb then (f a1) else (f a2).

Lemma Smod3: forall p n : nat, 3 <= p -> S n mod p <> n.

Lemma SSmod3: forall p n : nat, 3 <= p -> S (S n mod p) mod p <> n.

Section Dijkstra_complexity_1_2_3.

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 N := (Ring_size Root).

Hypothesis HNk: N <= k.

# Proof for degenerated case (N = 1 or 2)

Section Degenerated_1_2.

Hypothesis Nis1or2: N = 1 \/ N = 2.

Theorem Dijkstra_bound_n_is_1_or_2:
Steps_complexity 0
(fun e => Leg_state (s_hd e))
(fun e => Assume (s_hd e) /\ is_exec e).

End Degenerated_1_2.

# Proof for degenerated case (N = 3)

Section Degenerated_3.

Hypothesis Nis3: N = 3.

Notation N0:=Root (only parsing).
Definition N1:=Succ Root.
Definition N2:=Succ N1.

Lemma Succ0: Succ N0 == N1.
Lemma Succ1: Succ N1 == N2.
Lemma Succ2: Succ N2 == N0.

Lemma Pred0: Pred N0 == N2.
Lemma Pred1: Pred N1 == N0.
Lemma Pred2: Pred N2 == N1.

Lemma N0notN1: ~N0==N1.
Lemma N1notN2: ~N1==N2.
Lemma N0notN2: ~N0==N2.

Lemma Ring3: forall n:Node,n==N0\/n==N1\/n==N2.

Lemma DistN0: Dist Root N0 = 0.

Lemma DistN1: Dist Root N1 = 1.

Lemma DistN2: Dist Root N2 = 2.

## Values of predecessors

Lemma vPred0: forall g, Proper fequiv g -> v (g (Pred N0)) = v (g N2).

Lemma vPred1: forall g, Proper fequiv g -> v (g (Pred N1)) = v (g N0).

Lemma vPred2: forall g, Proper fequiv g -> v (g (Pred N2)) = v (g N1).

## Elementary characterization of Tokens presence/absence for each node

Lemma Token_N0: forall g, Proper fequiv g ->
(v (g N0) = v (g N2)) -> Token g N0.

Lemma no_Token_N0: forall g, Proper fequiv g ->
(v (g N0) <> v (g N2)) -> ~Token g N0.

Lemma Token_N1: forall g, Proper fequiv g ->
(v (g N0) <> v (g N1)) -> Token g N1.

Lemma no_Token_N1: forall g, Proper fequiv g ->
(v (g N0) = v (g N1)) -> ~Token g N1.

Lemma Token_N2: forall g, Proper fequiv g ->
(v (g N1) <> v (g N2)) -> Token g N2.

Lemma no_Token_N2: forall g, Proper fequiv g ->
(v (g N1) = v (g N2)) -> ~Token g N2.

# L3_state is ABA with (A+1) mod k = B

Definition L3_state (g:Env (Algo:=Dijkstra_algo)) : Prop :=
v (g N0) = v (g N2) /\
~ (v (g N0) = v (g N1)) /\
S (v (g N0)) mod k = v (g N1).

# L2_state is ABA with (A+1) mod k <> B

Definition L2_state (g:Env (Algo:=Dijkstra_algo)):=
v (g N0) = v (g N2) /\
~ (v (g N0) = v (g N1)) /\
~ S (v (g N0)) mod k = v (g N1).

# L1_state is ABC

Definition L1_state (g:Env (Algo:=Dijkstra_algo)):=
~ (v (g N0) = v (g N2)) /\
~ (v (g N0) = v (g N1)) /\
~ (v (g N1) = v (g N2)).

# L0_state subcase : ABB

Definition L0_state_ABB (g:Env (Algo:=Dijkstra_algo)):=
~ (v (g N0) = v (g N2)) /\
~ (v (g N0) = v (g N1)) /\
(v (g N1) = v (g N2)).

# L0_state subcase : AAB

Definition L0_state_AAB (g:Env (Algo:=Dijkstra_algo)):=
~ (v (g N0) = v (g N2)) /\
(v (g N0) = v (g N1)) /\
~ (v (g N1) = v (g N2)).

# L0_state subcase : AAA

Definition L0_state_AAA (g:Env (Algo:=Dijkstra_algo)):=
(v (g N0) = v (g N2)) /\
(v (g N0) = v (g N1)) /\
(v (g N1) = v (g N2)).

# L0_state is ABB, AAB, or AAA

Definition L0_state (g:Env (Algo:=Dijkstra_algo)):=
L0_state_ABB g \/ L0_state_AAB g \/ L0_state_AAA g.

# Tacttic to prove decidability of formulas with integer equalities

Ltac decidability_tac:=
repeat (apply or_dec || apply and_dec || apply not_dec || apply eq_nat_dec).

# Decidability results

Lemma L3_dec: forall g, Decidable (L3_state g).
Lemma L2_dec: forall g, Decidable (L2_state g).
Lemma L1_dec: forall g, Decidable (L1_state g).
Lemma L0_dec: forall g, Decidable (L0_state g).
Lemma Leg_dec: forall g, Proper pequiv g -> Decidable (Leg_state g).

# Tacttic to prove Proper for predicates with integer equalities

Ltac compat_tac pg:=
repeat (apply or_compat||apply and_compat||apply not_compat);
apply eq_compat;
repeat (apply v_compat||apply pg||apply (f_equal2 Nat.modulo)||apply (f_equal S));
reflexivity.

# Proper results

Instance L3_compat: Proper fequiv L3_state.
Instance L2_compat: Proper fequiv L2_state.
Instance L1_compat: Proper fequiv L1_state.
Instance L0_compat: Proper fequiv L0_state.

# Tactic to decompose state g based on equalities between node values:

• uses fresh names so we can call it twice in the same proof
• all known token properties are inferred
• uses congruence to prune absurd cases

Ltac destruct_state g pg:=
let T0 := fresh "T0_" in
let T1 := fresh "T1_" in
let T2 := fresh "T2_" in
let nT0 := fresh "nT0_" in
let nT1 := fresh "nT1_" in
let nT2 := fresh "nT2_" in
let EQ02 := fresh "EQ02_" in
let EQ01 := fresh "EQ01_" in
let EQ12 := fresh "EQ12_" in
let NE02 := fresh "NE02_" in
let NE01 := fresh "NE01_" in
let NE12 := fresh "NE12_" in
destruct (eq_nat_dec (v (g N0)) (v (g N2))) as [EQ02|NE02];
[assert (T0:=Token_N0 pg EQ02)|assert (nT0:=no_Token_N0 pg NE02)];
(destruct (eq_nat_dec (v (g N0)) (v (g N1))) as [EQ01|NE01];
[assert (nT1:=no_Token_N1 pg EQ01)|assert (T1:=Token_N1 pg NE01)]);
(destruct (eq_nat_dec (v (g N1)) (v (g N2))) as [EQ12|NE12];
[assert (nT2:=no_Token_N2 pg EQ12)|assert (T2:=Token_N2 pg NE12)]);
try congruence.

Lemma Leg_state_L0:
forall g, Proper pequiv g -> (Leg_state g <-> L0_state g).

Lemma state_decomp: forall g,
Proper fequiv g -> (L3_state g \/ L2_state g \/ L1_state g \/ L0_state g).

Lemma disjoint_L3_L2 : forall g, L3_state g -> L2_state g -> False.

Lemma disjoint_L3_L1 : forall g, L3_state g -> L1_state g -> False.

Lemma disjoint_L3_L0 : forall g, L3_state g -> L0_state g -> False.

Lemma disjoint_L2_L1 : forall g, L2_state g -> L1_state g -> False.

Lemma disjoint_L2_L0 : forall g, L2_state g -> L0_state g -> False.

Lemma disjoint_L1_L0 : forall g, L1_state g -> L0_state g -> False.

Lemma Step_has_to_move: forall (g:Env) (g':Env),
Step (Algo:=Algo) g' g ->
has_moved_b g' g N0 = false ->
has_moved_b g' g N1 = false ->
has_moved_b g' g N2 = false ->
False.

# Tactic to decompose step cases based on who has moved

• all known token properties are inferred
• all node value (dis)equalities are inferred
• the absurd case with no move is pruned
• tauto may be appended to prune moves at disabled nodes

Ltac destruct_step g g' pg assume hstep :=
let mov0 := fresh "mov0_" in
let mov1 := fresh "mov1_" in
let mov2 := fresh "mov2_" in
let nop0 := fresh "nop0_" in
let nop1 := fresh "nop1_" in
let nop2 := fresh "nop2_" in
let movT0 := fresh "movT0_" in
let movT1 := fresh "movT1_" in
let movT2 := fresh "movT2_" in
let movN0 := fresh "movN0_" in
let movN1 := fresh "movN1_" in
let movN2 := fresh "movN2_" in
let nopN0 := fresh "nopN0_" in
let nopN1 := fresh "nopN1_" in
let nopN2 := fresh "nopN2_" in
(destruct (Sumbool.sumbool_of_bool (has_moved_b g' g N0)) as [mov0|nop0];
[ assert(movT0:=has_moved_true_Token assume hstep _ mov0);
assert(movN0:=has_moved_v_Root assume hstep _ (reflexivity Root) mov0);
| assert (nopN0:= v_compat (proj1 (has_moved_false _ _ N0) nop0));
hnf in nopN0 ]);
(destruct (Sumbool.sumbool_of_bool (has_moved_b g' g N1)) as [mov1|nop1];
[ assert(movT1:=has_moved_true_Token assume hstep _ mov1);
assert(movN1:=has_moved_v_non_Root assume hstep _ (N0notN1) mov1);
rewrite (vPred1 pg) in movN1
| assert (nopN1:= v_compat (proj1 (has_moved_false _ _ N1) nop1));
hnf in nopN1 ]);
(destruct (Sumbool.sumbool_of_bool (has_moved_b g' g N2)) as [mov2|nop2];
[ assert(movT2:=has_moved_true_Token assume hstep _ mov2);
assert(movN2:=has_moved_v_non_Root assume hstep _ N0notN2 mov2);
rewrite (vPred2 pg) in movN2
| assert (nopN2:= v_compat (proj1 (has_moved_false _ _ N2) nop2));
hnf in nopN2 ]);[ .. |destruct (Step_has_to_move hstep nop0 nop1 nop2)].

Lemma L3_Step_L2_L0: forall (g:Env) (g':Env),
Assume g -> Step g' g ->
L3_state g -> L2_state g' \/ L0_state g'.

Lemma L2_Step_L1_L0: forall (g:Env) (g':Env),
Assume g -> Step g' g ->
L2_state g -> L1_state g' \/ L0_state g'.

Lemma L1_Step_L0: forall (g:Env) (g':Env),
Assume g -> Step g' g ->
L1_state g -> L0_state g'.

Lemma exec_no_end: forall g, Assume g ->
is_exec (s_one g) -> False.

Theorem Dijkstra_bound_n_is_3:
Steps_complexity 3
(fun e => Leg_state (s_hd e))
(fun e => Assume (s_hd e) /\ is_exec e).

End Degenerated_3.

End Dijkstra_complexity_1_2_3.

Unset Implicit Arguments.
Close Scope nat_scope.