Coq Library
PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_specifications_proved

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.

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_complexity.
From Padec Require Import Dijkstra_complexity_degenerated.
From Padec Require Import Steps.

Open Scope nat_scope.
Set Implicit Arguments.

Diskstra's first token ring algorithm

Specifications Proved

/contains:/ Proof that the algorithm is self-stabilizing wrt token ring circulation
/assumes:/ Parameter k>1; the network is a unidirectional rooted ring; N <= k
Dijkstra_common, in particular, Lemmas token_obtained and two_tokens_move.

Section Dijkstra_spec_proved.

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

  Hypothesis HNk: Ring_size Root <= k.


i.e. Step preserves legitimate configurations
  Lemma Dijkstra_closure_small:
    forall g g', Assume g -> Leg_state g -> Step g' g -> Leg_state g'.

Closure Lemma

  Lemma Dijkstra_closure: closure Dijkstra_RO_assumption
                                  unfair_daemon Leg_state.

Convergence: eventually a legitimate configuration is

reached Obtained from complexity

  Lemma Dijkstra_convergence:
    convergence Dijkstra_RO_assumption unfair_daemon Leg_state.
  Section Convergence_alternative_proof.

  End Convergence_alternative_proof.


As we have (Always Leg_State), (Always is_exec) and (Always Assume_RO), we have to prove that for every node, for every execution beginning in Assume_RO and Leg_State, it eventually reaches a configuration where the node holds the token. This proof is done by induction on the Ring traversal (using Succ), starting from the token holder. The step of induction relies on Lemma token_passes_to_Succ: after a step, a node that move transmits its token to its successor.

  Lemma token_passes_to_Succ:
    forall g g', Assume g -> Leg_state g -> Step g' g ->
                 forall n, Token g n -> Token g' (Succ n).

  Lemma Dijkstra_spec_ok:
    forall (e: Exec) (assume: Assume (s_hd e))
           (ise: is_exec e) (legit: Leg_state (s_hd e)),
    forall n, Always (Eventually (fun e => Token (s_hd e) n)) e.

Functional Specification of the Algorithm.

  Theorem Dijkstra_self_stab_prop:
    self_stabilization Dijkstra_RO_assumption unfair_daemon

End Dijkstra_spec_proved.

Unset Implicit Arguments.
Close Scope nat_scope.