PADEC - Coq Library

# Library Padec.Dijkstra.Dijkstra_specifications_proved

From Coq Require Import SetoidList.

From Coq Require Import SetoidClass.

From Coq Require Import Omega.

From Coq Require Import SetoidClass.

From Coq Require Import Omega.

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.

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

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

# Specifications Proved

- Closure: The result is direct from the result shown in

- Convergece: The result is direct from complexity.
- Specification: 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.

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.

Lemma Dijkstra_convergence:

convergence Dijkstra_RO_assumption unfair_daemon Leg_state.

Section Convergence_alternative_proof.

End Convergence_alternative_proof.

## Specification

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.

Theorem Dijkstra_self_stab_prop:

self_stabilization Dijkstra_RO_assumption unfair_daemon

Token_Circulation_Spec.

End Dijkstra_spec_proved.

Unset Implicit Arguments.

Close Scope nat_scope.

self_stabilization Dijkstra_RO_assumption unfair_daemon

Token_Circulation_Spec.

End Dijkstra_spec_proved.

Unset Implicit Arguments.

Close Scope nat_scope.