PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_complexity

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 Bool.
From Coq Require Import ZArith.
From Coq Require Import Lia.

Local Imports

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 Dijkstra_algo.
From Padec Require Import Dijkstra_common.
From Padec Require Import Dijkstra_Z.
From Padec Require Import Dijkstra_sum_dist.
From Padec Require Import Self_Stabilization.
From Padec Require Import Steps.
From Padec Require Import NatUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import Count.
From Padec Require All_In.
From Padec Require FoldRight.
From Padec Require Import ListUtils.

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 Bound

/contains:/ Proof of the complexity bound

gathers previous results from sum_dist, Z

/assumes:/ Parameter k>1; the network is a unidirectional rooted ring; N <= k

Case N >= 4

Definition of the cost using sum_dist and Z
Cost 0 means legitimate configuration
Cost bound
Cost decreasing

General case

Section Dijkstra_complexity.

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

  Existing Instance Dijkstra_RO_assumption.

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

Proof for non-degenerated cases (N >= 4)

  Section Non_Degenerated.

    Hypothesis HN4: N >= 4.

    Lemma HN1: N > 1.

Cost

The cost of a configuration:

Definition cost (g: Env): nat := sum_dist g + (Z g ) * N - 2.

sum_dist g + (Z g) * N < 3 implies a legitimate configuration

    Lemma cost_0_leg_state:
      forall g, Proper pequiv g -> Assume g ->
                sum_dist g + (Z g ) * N < 3 -> Leg_state g.

Cost is bounded, using bounds for Z and sum_dist

    Lemma cost_bound:
      forall g, Assume g -> Proper pequiv g ->
                Z g <= N - 2 ->
                cost g <= Dijkstra_exact_bound N - 1.

Cost decreases

    Lemma cost_decreases:
      forall g, Assume g -> ~Leg_state g ->
                forall g', Step g' g -> cost g' < cost g.

    Lemma Dijkstra_exact_bound_g0: Dijkstra_exact_bound N > 0.

    Theorem Dijkstra_bound_non_degenerated_cases:
      Steps_complexity (Dijkstra_exact_bound N)
                       (fun e => Leg_state (s_hd e))
                       (fun e => Assume (s_hd e) /\ is_exec e).
  End Non_Degenerated.

End Dijkstra_complexity.

Unset Implicit Arguments.
Close Scope nat_scope.