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)

# Bounds for N = 1 to 3 are tight

We do not prove it for N=1 or 2 since this is obvious (no value smaller than 0 step). We assume N = 3
/contains:/ I - Proof that this bound is reached (synchronous execution from (0,1,0])
/assumes:/ Parameter k>1; the network is a unidirectional rooted ring; N <= k ; N = 3
Part I: DTRC complexity for N=3 is 3 steps at least
We exhibit wcExec3 := (sync_exec (mkEnv 0;1;0)) as a worst case execution.
We prove that the execution begins as follows: (mkEnv 0;1;0) -> (mkEnv 1;0;1) -> (mkEnv 2;1;0) -> (mkEnv 2;2;1) -> ... ~ Leg_state ~ Leg_state ~ Leg_state Leg_state
Main result wcLeg3 : At_N_steps 3 (fun e => Leg_state (s_hd e)) wcExec3.
Conclusion using Non_Leg_Steps_min_bound

Section Dijkstra_worst_case_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 using Type using Type for degenerated case (N = 3)
Hypothesis Nis3: N = 3.

Notation N0:=Root (only parsing).
Definition DistN1 := (DistN1 HNk Nis3).
Definition DistN2 := (DistN2 HNk Nis3).
Definition Ring3 := (Ring3 Nis3).
Definition N0notN1 := (N0notN1 HNk Nis3).
Definition N0notN2 := (N0notN2 HNk Nis3).
Definition vPred0 := (vPred0 Nis3).

Lemma kge3: k>=3.

Definition wcEnv3: Env (Algo := Dijkstra_algo) := mkEnv (0::1::0::nil).

Definition wcEnv2: Env (Algo := Dijkstra_algo) := mkEnv (1::0::1::nil).

Definition wcEnv1: Env (Algo := Dijkstra_algo) := mkEnv (2::1::0::nil).

Definition wcEnv0: Env (Algo := Dijkstra_algo) := mkEnv (2::2::1::nil).

Definition wcExec3: Exec (Algo := Dijkstra_algo) := sync_exec wcEnv3.

Instance wcEnv3_compat:Proper pequiv wcEnv3:= mkEnv_compat (reflexivity _).
Instance wcEnv2_compat:Proper pequiv wcEnv2:= mkEnv_compat (reflexivity _).
Instance wcEnv1_compat:Proper pequiv wcEnv1:= mkEnv_compat (reflexivity _).
Instance wcEnv0_compat:Proper pequiv wcEnv0:= mkEnv_compat (reflexivity _).

Ltac value_tac DistN :=
intros v0 v1 v2 h0 h1 h2;
rewrite mkEnv_value;auto;
[ rewrite DistN;reflexivity
| rewrite Nis3;hnf;simpl;
repeat split;try omega;
apply Forall_nil].

Lemma N0_value: forall (v0 v1 v2:nat),
v0 < 3 -> v1 < 3 -> v2 < 3 ->
v (mkEnv (v0::v1::v2::nil) N0) = v0.

Lemma N1_value: forall (v0 v1 v2:nat),
v0 < 3 -> v1 < 3 -> v2 < 3 ->
v (mkEnv (v0::v1::v2::nil) N1) = v1.

Lemma N2_value: forall (v0 v1 v2:nat),
v0 < 3 -> v1 < 3 -> v2 < 3 ->
v (mkEnv (v0::v1::v2::nil) N2) = v2.

Ltac simpl_value:=
(rewrite N0_value || rewrite N1_value || rewrite N2_value);[|try omega ..].

Lemma L3_wcEnv3: L3_state wcEnv3.

Lemma L2_wcEnv2: L2_state wcEnv2.

Lemma L1_wcEnv1: L1_state wcEnv1.

Lemma L0_wcEnv0: L0_state_AAB wcEnv0.

Lemma wcEnv3_non_leg: ~ Leg_state wcEnv3.

Lemma wcEnv2_non_leg: ~ Leg_state wcEnv2.

Lemma wcEnv1_non_leg: ~ Leg_state wcEnv1.

Lemma wcEnv0_leg: Leg_state wcEnv0.

Lemma v_simpl: forall s rop, v (mkState (vltk s) rop) = v s.

Lemma v_simpl_mod: forall s rop, v (mkState (Smod (vltk s)) rop) = (S (v s)) mod k.

Ltac simpl_root :=
simpl root;
match goal with
| [|- context [ Node_dec N0 N0]] =>
(destruct (Node_dec N0 N0) as [EQ|NE]; [|elim NE;reflexivity])
| [|- context [ Node_dec N1 N0]] =>
(destruct (Node_dec N1 Root) as [EQ|NE];[elim N0notN1;symmetry;apply EQ|])
| [|- context [ Node_dec N2 N0]] =>
(destruct (Node_dec N2 Root) as [EQ|NE];[elim N0notN2;symmetry;apply EQ|])
end.

Ltac uglySharedProofScript g_ g'_ pg_ pg'_:=
pose (g:=g_); pose (g':=g'_);
assert (pg:=pg_); assert (pg':=pg'_);
fold g in pg|-*; fold g' in pg'|-*;
unfold g_ in g; unfold g'_ in g';
assert (assume: Assume g) by apply Assume_RO_mkEnv;
intros n_ n en;
rewrite en;clear n_ en;
(split; [|
rewrite (Stable_Variable_RUN Dijkstra_Stable);
change (Dijkstra_ROpart (g n)) with (Dijkstra_ROpart (g' n));
apply Dijkstra_ROpart_compat,pg',reflexivity]);
change (v (RUN g n) = v (g' n));
assert (pp:Proper pequiv (fun n => (v (RUN g n) = v (g' n)))) by
(
intros n1 n2 en; apply eq_compat,v_compat;
[ apply (RUN_compat pg _ _ en)
| apply (pg' _ _ en) ]
);
destruct (Ring3 n) as [en|[en|en]];
(rewrite (pp _ _ en);clear pp en n;
rewrite (fun n => v_compat (RUN_simpl n pg assume));
unfold simple_run;
simpl_root;
rewrite ITE_sumbool_f;
repeat rewrite v_simpl;
repeat rewrite v_simpl_mod;
try rewrite (vPred0 pg);
try rewrite (vPred1 pg);
try rewrite (vPred2 pg);
unfold g,g'; repeat simpl_value;try reflexivity;
simpl;apply Nat.mod_small;try omega).

Lemma wcRUN3: (RUN wcEnv3) =~= wcEnv2.

Lemma wcRUN2: (RUN wcEnv2) =~= wcEnv1.

Lemma wcRUN1: (RUN wcEnv1) =~= wcEnv0.

Lemma wcLeg3: At_N_steps 3 (fun e => Leg_state (s_hd e)) wcExec3.

Theorem Dijkstra_min_bound_n_is_3:
forall bound, bound < 3 ->
~ Steps_complexity bound
(fun e => Leg_state (s_hd e))
(fun e => Assume (s_hd e) /\ is_exec e).

End Dijkstra_worst_case_3.

Unset Implicit Arguments.
Close Scope nat_scope.