Coq Library
PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_algo

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

Local Imports

From Padec Require Import OptionUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import Ring_topology.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Diskstra's first token ring algorithm

The Algorithm

/contains:/ Dijkstra first algorithm for token circulation on a rooted ring
/assume:/ Parameter k>1

Section Dijkstra_algo.

  Context {Chans: Channels}.

  Class Dijkstra_parameters :=

Parameter k of the algoritm: node values are incremented

modulo k
      k: nat;
      H_k: k > 1

Assuming the Dijkstra parameter and hypothesis:
  Context {DP: Dijkstra_parameters}.
  Let H_k := H_k.

State of a Node in the Algorithm

Read Only Part of a State; local topology information

It is made of
    Record Dijkstra_ROState := mkROState {
                                   predc: Channel;
                                   root: bool

    Notation eqROS := (fun (x y: Dijkstra_ROState) =>
                         predc x == predc y /\ root x = root y).

    Instance eqROS_equiv: Equivalence eqROS.

    Global Instance Dijkstra_ROState_setoid: Setoid Dijkstra_ROState :=
      {|equiv := eqROS|}.

State of a node

    Record Dijkstra_State := mkState {
                                 vltk: { n: nat | n <= k-1};
                                 Dijkstra_ROpart :> Dijkstra_ROState

    Notation eqS := (fun (x y: Dijkstra_State) =>
      vltk x == vltk y /\ Dijkstra_ROpart x == Dijkstra_ROpart y).

    Instance eqS_equiv: Equivalence eqS.

    Global Instance State_setoid :Setoid Dijkstra_State := {|equiv := eqS|}.

Getter for vltk

    Definition v (s: Dijkstra_State): nat := proj1_sig (vltk s).

    Lemma v_ltk: forall (s: Dijkstra_State), v s < k.

    Lemma v_plus_0: forall (s: Dijkstra_State), (v s + 0) mod k = v s.

Equality and Compatibility properties on State

    Lemma Dijkstra_ROState_dec: Decider (equiv (A := Dijkstra_ROState)).

    Lemma Dijkstra_State_dec: Decider (equiv (A := Dijkstra_State)).

    Instance v_compat: Proper fequiv v.

    Instance predc_compat_RO: Proper fequiv predc.

    Instance root_compat_RO: Proper fequiv root.

    Instance Dijkstra_ROpart_compat: Proper fequiv Dijkstra_ROpart.

    Instance predc_compat: Proper (equiv (A:=Dijkstra_State) ==> equiv) predc.

    Instance root_compat: Proper (equiv (A:=Dijkstra_State) ==> equiv) root.

    Section Run_definition.

"+1" on natural modulo k
      Program Definition Smod (nltk: {n: nat| n <= k-1}):
        {n: nat| n <= k-1} := (S (proj1_sig nltk) mod k).

      Global Instance Smod_compat: Proper fequiv Smod.

      Lemma Smod_neq: forall (v: {n: nat| n <= k-1}), ~v == (Smod v).

Run Function for the Algorithm

Function simple_run contains the algorithm as written in papers, using two arguments (the current state of the node and the current state of its predecessor).
Function run_algorithm calls simple_run with the arguments, as awaited by PADEC in class Algorithm.

      Definition simple_run (s s_pred: Dijkstra_State): Dijkstra_State :=
         if root s then
           if Nat.eq_dec (v s) (v s_pred) then
             {| vltk := Smod (vltk s); Dijkstra_ROpart := s |}
           if Nat.eq_dec (v s) (v s_pred) then
             {| vltk := vltk s_pred; Dijkstra_ROpart := s |}.

      Definition run_algorithm
                 (s: Dijkstra_State)
                 (peer_state: Channel -> option Dijkstra_State)
        : Dijkstra_State :=
        match peer_state (predc s) with
          None => s
        | Some s_pred => simple_run s s_pred

    End Run_definition.

Properties of the Algorithm

Compatibility of the Run Function

    Instance simple_run_compat:
      Proper fequiv simple_run.

    Instance run_algorithm_compat: Proper fequiv run_algorithm.

Definition of The Algorithm

    Instance Dijkstra_algo: Algorithm :=
      {| State := Dijkstra_State; run := run_algorithm; |}.

Stability for the Read-Only Part of the Run Function

    Lemma ROpart_stable:
      forall s sn, Dijkstra_ROpart (run_algorithm s sn) =~= Dijkstra_ROpart s.

    Global Instance Dijkstra_Stable:
      Stable_Variable Dijkstra_algo Dijkstra_ROpart.

End Dijkstra_algo.

Unset Implicit Arguments.
Close Scope nat_scope.
Close Scope signature_scope.