PADEC - Coq Library

Library Padec.Model.P_Q_Termination

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global imports

From Coq Require Import Arith.
From Coq Require Import List.
From Coq Require Import Relations.
From Coq Require Import Wellfounded.
From Coq Require Import Setoid.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Basics.
From Coq Require Import RelationPairs.
From Coq Require Import Lia.

Local imports

From CoLoR Require MultisetNat.

From Padec Require Import SetoidUtil.
From Padec Require Import ListUtils.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import WellfoundedUtil.

Open Scope signature_scope.
Set Implicit Arguments.

Core Results for Proving Termination

We show a sufficient condition based on some potential function. Each node in a given configuration provides a local potential. Usual termination proofs are based on some global potential based on the local ones. For instance, potentials can be natural numbers, the global potential can be the sum of the local potentials and the argument for termination might be based on the fact that the global potential strictly decreases each step of the algorithm.

Instead, we build the global potential as the multiset containing the local potential of every nodes. Our sufficient condition for termination uses the Dershowitz-Manna order on finite multi-sets and defines two criteria:

Local criterion expresses that given a step, for any node, if its local potential has not decreased, there exists another node (typically one of its neighbors) for which the potential actually decreased.
- Global criterion exhibits, at any step, a node whose potential decreased.

The result can be used for any Steps of the model, or for subrelations on it. We allow conditionned transitions such that:

1) the algorithm is initialized in some stable set of configurations. - in this set, every configuations should be proper (mandatory) - there might be no more constraints (proper self-stabilization) - but in case of composed algorithms, it can also express the fact that a first algorithm has stabilized (into this stable set) and that a second algorithm composed to the first one stabilizes provided that the first one stabilized in this set. This condition might be necessary to be able to define potentials.

2) we may need to study a particular classes of transitions (characterized by the firing condition). This might be useful to cut the termination proof in different classes of converging transitions.

Section P_Q_Termination.

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

  Section Multiset_Criterion.

    Variable (safe: Env -> Prop).

    Notation safeEnv := (sig safe).

    Notation getEnv := (@proj1_sig Env safe).
    Notation getSafe := (@proj2_sig Env safe).

Assumptions on safe configurations in which the algorithm is initialized.

should be stable against valid_diff
should be compatible

Variable (safe_compat: Proper fequiv safe)
(stable_safe: forall (g g': Env), safe g -> Step g' g -> safe g').

Safe Steps (from safeEnv to safeEnv) NB: transition from g to g'

    Definition safeStep (g' g: safeEnv): Prop := Step (getEnv g') (getEnv g).

    Global Instance safeStep_compat: Proper fequiv safeStep.

    Variable (QTrans: safeEnv -> safeEnv -> Prop).

    Definition safeQStep (g' g: safeEnv): Prop := safeStep g' g /\ QTrans g' g.

    Instance safeQStep_compat: Proper fequiv QTrans -> Proper fequiv safeQStep.

Mnat is the type of potential values endowed with

equality (decidable equivalence): eqP
strict order: gtP, compatible w.r.t. eqP

It stands for natural numbers in multisets.

    Notation Mnat := MultisetNat.MSetCore.Sid.Eq.A.

    Notation eqP := MultisetNat.MSetCore.Sid.Eq.eqA.
    Notation eqP_dec := MultisetNat.MSetCore.Sid.eqA_dec.
    Instance eqP_equiv: Equivalence eqP :=
      MultisetNat.MSetCore.Sid.Eq.eqA_Equivalence.

    Notation gtP := gt.

    Instance gtP_so: StrictOrder gtP.

    Instance gtP_compat: Proper (eqP ==> eqP ==> iff) gtP.

    Lemma classical_gtP: forall x y, gtP x y \/ ~ gtP x y.

pot is the potential function for local nodes

It should be compatible. It only needs to be defined on the set of safe configurations.

Variable (pot: safeEnv -> Node -> Mnat).
Context {pot_compat: Proper fequiv pot}.

Global Potential

Definition Pot (g: safeEnv): list nat := List.map (pot g) all_nodes.

Local Criterion (see above)

    Hypothesis local_crit:
      forall (g g': safeEnv),
        safeQStep g' g ->
        forall (n: Node),
          gtP (pot g' n) (pot g n) ->
          exists (n': Node ),
            ~ (pot g n') == (pot g' n') /\ gtP (pot g n') (pot g' n).

Global Criterion (see above)

    Hypothesis global_crit:
      forall (g g': safeEnv),
        safeQStep g' g -> exists (n: Node ), ~ (pot g' n ) == (pot g n ).

Core Result: safeQStep decreases Pot

Tools on multisets

    Notation Mset := (MultisetNat.MSetCore.Multiset).
    Notation gtM := (@MultisetNat.MSetOrd.MultisetGT gt).
    Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).
    Notation eqM := MultisetNat.MSetCore.meq.
    Notation Mempty := MultisetNat.MSetCore.empty.
    Notation Munion := MultisetNat.MSetCore.union.
    Notation Msingleton := MultisetNat.MSetCore.singleton.
    Notation MIn := MultisetNat.MSetOrd.MSet.member.

    Lemma cons_union:
      forall (x: nat) (q: Mset), eqM (x ::q) (Munion (Msingleton x) q).

    Lemma nil_empty: @eqM nil Mempty.

    Lemma eq_meq:
      forall l1 l2 : Mset, l1 == l2 -> eqM l2 l1.

    Lemma MIn_empty: forall x, MIn x Mempty <-> False.

    Lemma MIn_union:
      forall x P Q, MIn x (Munion P Q) <-> MIn x P \/ MIn x Q.

    Lemma MIn_InA: forall x MS, MIn x MS <-> InA equiv x MS.

Core Theorem

safe_incl := (forall g g', safeQStep g' g -> ltM (Pot g') (Pot g)

Lemma Step_decreases_pot:
inclusion safeQStep (ltM @@ Pot)%signature.

The main theorem: applied to prove that algorithm terminates!

Conditionned transitions are well founded.

Lemma Wf_safeQAlgo_Multiset: well_founded safeQStep.

Section No_QTrans.

Once proven that safe transitions are well founded, it can be easily deduced that any execution terminates provided that it starts in a safe configuration.

      Lemma Acc_Algo_Multiset:
        well_founded safeStep -> forall g: Env, safe g -> Acc Step g.

      Lemma NoQTrans_Wf_Multiset:
        well_founded safeQStep -> (forall x x', QTrans x x') -> well_founded safeStep.

    End No_QTrans.

  End Multiset_Criterion.

Lexicographic orders on safeEnv

  Section Lexico.

    Variable (safe: Env -> Prop).
    Notation safeEnv := (sig safe).

    Section Lexico_core.

Trans1 has priority on Trans 2

      Variable QTrans1: relation safeEnv.
      Variable QTrans2: relation safeEnv.
      Notation step1 := (safeQStep QTrans1).
      Notation step2 := (safeQStep QTrans2).

Relations abstracting step1

      Variable (S1: relation safeEnv)
               (HS1: inclusion step1 S1) (WF1: well_founded S1)
               (E1: relation safeEnv) (TE1: Transitive E1)
               (CE1: forall g' g, (exists gg , S1 g' gg /\ E1 gg g )
                                  -> S1 g' g).

      Variable (WF2: well_founded step2).

      Variable (Disjoint: forall e e',
                   step2 e' e -> E1 e' e \/ S1 e' e).

      Lemma Wf_lexico:
        well_founded (safeQStep (union QTrans1 QTrans2)).

    End Lexico_core.

    Import MultisetNat.MSetOrd.
    Notation Mnat := MultisetNat.MSetCore.Sid.Eq.A.
    Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).
    Notation eqM := MultisetNat.MSetCore.meq.

    Lemma ltM_wf: well_founded ltM.

    Lemma ltM_comp_wf:
      forall A (f: A -> MultisetNat.MSetCore.Multiset),
        well_founded (ltM @@ f).

    Instance ltM_compat: Proper (eqM ==> eqM ==> iff) ltM.

    Lemma ltM_comp_trans:
      forall A (f: A -> MultisetNat.MSetCore.Multiset),
        Transitive (eqM @@ f).

    Lemma ltM_eqM_comp_commut:
      forall A (f: A -> MultisetNat.MSetCore.Multiset),
      forall a b, (exists c , ltM (f a) (f c) /\ eqM (f c) (f b)) ->
                  ltM (f a) (f b).

Union of two classes of converging transitions

composed using priorities, i.e. lexicographic order.

    Section Lexico_MultiSet2.

      Variable (pot1: safeEnv -> Node -> Mnat).
      Notation Pot1 := (@Pot safe pot1).

Trans1 has priority on Trans 2

      Variable QTrans1: relation safeEnv.
      Variable QTrans2: relation safeEnv.
      Notation Trans1 := (safeQStep QTrans1).
      Notation Trans2 := (safeQStep QTrans2).
      Variable (Hterm1: inclusion Trans1 (ltM @@ Pot1)%signature).
      Variable (Hterm2: well_founded Trans2).
      Variable (Hdisjoint1: forall e e', Trans2 e' e -> eqM (Pot1 e') (Pot1 e) \/ ltM (Pot1 e') (Pot1 e)).

      Lemma union_lex_wf2:
        well_founded (safeQStep (union QTrans1 QTrans2)).

    End Lexico_MultiSet2.

Union of three classes of converging transitions

composed using priorities, i.e. lexicographic order.

    Section Lexico_MultiSet3.

      Variable (pot1 pot2: safeEnv -> Node -> Mnat).
      Notation Pot1 := (@Pot safe pot1).
      Notation Pot2 := (@Pot safe pot2).

      Variable QTrans1 QTrans2 QTrans3: relation safeEnv.
      Notation Trans1 := (safeQStep QTrans1).
      Notation Trans2 := (safeQStep QTrans2).
      Notation Trans3 := (safeQStep QTrans3).
      Variable (Hterm1: inclusion Trans1 (ltM @@ Pot1)%signature).
      Variable (Hterm2: inclusion Trans2 (ltM @@ Pot2)%signature).
      Variable (Hterm3: well_founded Trans3).
      Variable (Hdisjoint1: forall e e', Trans2 e' e \/ Trans3 e' e -> eqM (Pot1 e') (Pot1 e) \/ ltM (Pot1 e') (Pot1 e)).
      Variable (Hdisjoint2: forall e e', Trans3 e' e -> eqM (Pot2 e') (Pot2 e) \/ ltM (Pot2 e') (Pot2 e)).

      Lemma union_lex_wf3:
        well_founded (safeQStep (union QTrans1
                                       (union QTrans2 QTrans3))).

    End Lexico_MultiSet3.

Union of four classes of converging transitions

composed using priorities, i.e. lexicographic order.

    Section Lexico_MultiSet4.

      Variable (pot1 pot2 pot3: safeEnv -> Node -> Mnat).
      Notation Pot1 := (@Pot safe pot1).
      Notation Pot2 := (@Pot safe pot2).
      Notation Pot3 := (@Pot safe pot3).

      Variable (QTrans1 QTrans2 QTrans3 QTrans4: relation safeEnv).
      Notation Trans1 := (safeQStep QTrans1).
      Notation Trans2 := (safeQStep QTrans2).
      Notation Trans3 := (safeQStep QTrans3).
      Notation Trans4 := (safeQStep QTrans4).

      Variable (Hterm1: inclusion Trans1 (ltM @@ Pot1)%signature).
      Variable (Hterm2: inclusion Trans2 (ltM @@ Pot2)%signature).
      Variable (Hterm3: inclusion Trans3 (ltM @@ Pot3)%signature).
      Variable (Hterm4: well_founded Trans4).

      Variable (Hdisjoint1:
                  forall e e', Trans2 e' e \/ Trans3 e' e \/ Trans4 e' e ->
                               eqM (Pot1 e') (Pot1 e) \/
                               ltM (Pot1 e') (Pot1 e)).
      Variable (Hdisjoint2:
                  forall e e', Trans3 e' e \/ Trans4 e' e ->
                               eqM (Pot2 e') (Pot2 e) \/
                               ltM (Pot2 e') (Pot2 e)).
      Variable (Hdisjoint3:
                  forall e e', Trans4 e' e ->
                               eqM (Pot3 e') (Pot3 e) \/
                               ltM (Pot3 e') (Pot3 e)).

      Lemma union_lex_wf4:
        well_founded
          (safeQStep (union QTrans1 (union QTrans2 (union QTrans3 QTrans4)))).

    End Lexico_MultiSet4.
  End Lexico.

End P_Q_Termination.

Unset Implicit Arguments.
Close Scope signature_scope.