PADEC - Coq Library

Library Padec.MessagePassing.DecrMP

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 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 PeanoNat.
From Coq Require Import Lia.
From Coq Require Import Streams.

Local imports

From Padec Require Import NatUtils.
From Padec Require Import AlgorithmMP.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import RelModelMP.
From Padec Require Import Self_StabilizationMP.
From Padec Require Import FairnessMP.
From Padec Require Import ExecMP.
From Padec Require Import Fair_convergence.

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

Section Decr_Generic_Net.

Context {InChans: InChannels} {OutChans: OutChannels} {DNet: DirNetwork}.

(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: MPAlgorithm :=
    {|
      State_setoid := Setoid_nat;
      State_dec := eq_nat_dec;
      Msg := unit;
      Msg_setoid := Setoid_unit;
      run := fun n _ => (pred n , nil );

    |}.

End Decr_Generic_Net.

Section Decr.

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

  Context {InChans: InChannels} {OutChans: OutChannels}.

  Hint Resolve is_exec_cons is_exec_tl : core.
  Variable K: N.

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

  Program Instance NetK: DirNetwork:=
    {| Node_dec := ltK_dec (K := K);
       inLink := fun _ => None;
       outLink := fun _ => None;
       all_nodes := Kenum K
    |}.

Configurations

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

#[refine] Instance Env_partial_setoid:
    PartialSetoid EnvD:=
    {| pequiv:=eqEnv |}.
  Defined.

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

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

  Instance potential_compat : Proper fequiv potential.

  Lemma potential_nonzero : forall (env: EnvD), potential env <> 0
          -> exists n : Node , Node_env env n <> 0.

  Lemma potential_zero : forall (env: EnvD), Proper eqEnv env ->
    potential env = 0 <-> forall n, Node_env env n = 0.

Terminal Configuration to reach

Definition target (env: EnvD) := potential env = 0.

Lemmas for pot_decreases

  Lemma value_non_increasing: forall (p p': EnvD *Event), Step p' p -> forall n,
    Node_env (fst p') n <= Node_env (fst p) n.

  Lemma pot_non_increasing: forall e, is_exec e ->
      pot_decreases Setoid_nat lt (fun p => potential (fst p)) e.

Lemmas for pot_fairly_decreases_until

  Lemma value_nonactive_equal: forall (p p': EnvD *Event), Step p' p -> forall n,
    ~ active_node (snd p) == n ->
    Node_env (fst p') n = Node_env (fst p) n.

  Lemma value_nonzero_active_decreasing: forall (p p': EnvD *Event), Step p' p -> forall n,
    active_node (snd p) == n ->
    Node_env (fst p) n <> 0 ->
    Node_env (fst p') n < Node_env (fst p) n.

  Lemma potential_nonzero_active_decreasing: forall (p p': EnvD *Event), Step p' p -> forall n,
    active_node (snd p) == n ->
    Node_env (fst p) n <> 0 ->
    potential (fst p') < potential (fst p).

  Lemma potential_ev_decreases:
    forall (e: Exec), is_exec e -> potential (fst (hd e)) <> 0 ->
      Exists (fun e' => potential (fst (hd (tl e'))) < potential (fst (hd e'))) e.

  Lemma potential_fairly_decreases_until : forall e, is_exec e ->
      pot_fairly_decreases_until lt (fun p : EnvD * Event => potential (fst p))
        (fun suf : Exec => target (fst (hd suf))) e.

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

  Lemma EqSt_reflex_DI : forall s:Stream nat, EqSt s s.

  Lemma SS_decr:
    self_stabilization Null_Assumption unfair_daemon
                       (fun e => target (fst (hd e))).

End Decr.

Close Scope signature_scope.
Unset Implicit Arguments.