PADEC - Coq Library

Library Padec.Model.Decr

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global imports

From Coq Require Import Arith.
From Coq Require Import NArith.
From Coq Require Import Setoid.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import RelationPairs.
From Coq Require Import Morphisms.
From Coq Require Import List.
From Coq Require Import Lia.

Local imports

From Padec Require Import NatUtils.
From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import FoldRight.
From Padec Require Import SetoidUtil.
From Padec Require Import NatBuild.
From Padec Require Import RelModel.
From Padec Require Import P_Q_Termination.
From Padec Require Import Self_Stabilization.
From Padec Require Import Fairness.
From Padec Require Import Exec.

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

Section Decr_Generic_Net.

Context {Chans: Channels}
{Net: Network}.

(Very Simple) Example

The state of the nodes are natural numbers.

This algorithm does not use neighborhood: At each step, the node decreases its state.

  Program Instance Decr: Algorithm :=
    {|
      State_setoid := Setoid_nat;
      State_dec := eq_nat_dec;
      run := fun n _ => pred n;

    |}.

End Decr_Generic_Net.

Section Decr.

Nodes are also natural numbers, labeled from 0 to K-1.

Context {Chans:Channels}.

Variable K: N.

The network is made of K nodes, with no edge.

  Program Instance NetK: Network:=
    {| Node_dec := ltK_dec (K := K);
       peer := fun _ _ => None;
       link := fun _ _ => None;
       all_nodes := Kenum K
    |}.

Configurations

Notation env := (@Env _ NetK Decr).

Terminal Configuration to reach

Definition target (g: env ) := forall n , g n = 0.

target is indeed a terminal configuration, i.e. no more valid step can be executed from it.

Theorem final: forall e, target e <-> terminal e.

Potential is defined as the sum of the states on all nodes.

Definition potential g :=
List.fold_right plus 0 (List.map g (@all_nodes _ NetK)).

Any valid step decreases the global potential

Theorem potential_decreases:
forall (g g': env), Step g' g -> potential g' < potential g.

Steps of this algorithm on this network are well founded

  Lemma WF_decr: well_founded (@Step _ NetK Decr).

  Program Instance Null_Assumption: Stable_Assumption (Algo:= Decr) :=
    {|
      getRO:= fun _ => tt;
      Assume_RO:= fun _ => True;
    |}.

  Lemma SS_decr:
    self_stabilization Null_Assumption unfair_daemon
                       (fun e => target (Stream.s_hd e)).

End Decr.

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