PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_Global_Thm

A Framework for Certified Self-Stabilization
PADEC Coq Library

March 2017

Global Imports

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

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.
From Padec Require Import Ring_topology.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import Dijkstra_algo.
From Padec Require Import Dijkstra_common.
From Padec Require Import Dijkstra_specifications.
From Padec Require Import Dijkstra_specifications_proved.
From Padec Require Import Dijkstra_complexity.
From Padec Require Import Dijkstra_complexity_degenerated.
From Padec Require Import Dijkstra_worst_case.
From Padec Require Import Dijkstra_worst_case_degenerated.
From Padec Require Import Steps.

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)

This file adds nothing but gathers every important results, namely the results in Theorem 1. Meanwhile, it checks that no additionnal assumption has been introduced in the development.

Theorem 1:

(B.G) Provided that , the stabilization time of Algorithm DTR is at most \DTCExact steps.
(B.1-2) If or , the stabilization time is 0 step.
(B.3) If , the stabilization time is at most 3 steps.
(S) Algorithm \DTR is a self-stabilizing token circulation in any unidirectional rooted ring of size such that under the distributed unfair daemon.
(T.G)] Provided that , this bound is tight, {\em i.e.}, it can be reached. In other words, for any ring of size at least 4, there exists an execution whose stabilization time exactly matches the bound.
(T.3) For , the bound of steps is also tight.

Section Dijkstra_Global_Thm.

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

  Existing Instance Dijkstra_RO_assumption.

  Notation N := (Ring_size Root).
  Hypothesis HNk: N <= k.

(B.G) Provided that , the stabilization time of Algorithm DTR is at most \DTCExact steps.

  Theorem BdotG:
    4 <= N -> N <= k ->
    Steps_complexity (Dijkstra_exact_bound N)
                     (fun e => Leg_state (s_hd e))
                     (fun e => Assume (s_hd e) /\ is_exec e).

(B.1-2) If or , the stabilization time is 0 step.

  Theorem Bdot1minus2:
    N = 1 \/ N = 2 ->
    Steps_complexity 0
                     (fun e => Leg_state (s_hd e))
                     (fun e => Assume (s_hd e) /\ is_exec e).

(B.3) If , the stabilization time is at most 3 steps.

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

(S) Algorithm \DTR is a self-stabilizing token circulation in any unidirectional rooted ring of size such that under the distributed unfair daemon.

  Theorem S:
    self_stabilization Dijkstra_RO_assumption unfair_daemon
                       Token_Circulation_Spec.

(T.G) Provided that , this bound is tight, {\em i.e.}, it can be reached. In other words, for any ring of size at least 4, there exists an execution whose stabilization time exactly matches the bound.

  Theorem TdotG:
    4 <= N -> N <= k ->
    exists e , Assume (s_hd e) /\ is_exec e /\
              At_N_steps (Dijkstra_exact_bound N)
                         (fun e => Leg_state (s_hd e)) e.

(T.3) For , the bound of steps is also tight.

  Theorem Tdot3:
    N = 3 ->
    exists e , Assume (s_hd e) /\ is_exec e /\
              At_N_steps 3 (fun e => Leg_state (s_hd e)) e.

End Dijkstra_Global_Thm.

Unset Implicit Arguments.
Close Scope nat_scope.