PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.KDomSet.KDomSet_termination

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 SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import FoldRight.
From Padec Require Import Algorithm.
From Padec Require Import Spanning_Tree.
From Padec Require Import KDomSet_specification.
From Padec Require Import KDomSet_alpha.

Open Scope Z_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Termination for K-Dominating Set Algorithm

Roadmap
1) Define Potential of a node: 0 if not enabled, else tree depth signature: node->env -> nat
NB: depth for root == 1
2) Proof: if a node becomes enabled, one of its child has moved
3) Proof (down path induction + 2)): if a node becomes enabled, one of its descendant has become disabled
assumption: downpaths are finite (to be proved elsewhere)
4) Proof: there is always a node whose activation has changed (potential of this node passed from >0 to 0) (induction on down path)
5) Using 3) and multiset theorem (P_Q_Termination.v) concludes that the algorithm terminates
=> Use results from P_Q_Termination
Section KDomSet_Termination.

Channel and Network definitions
  Context {Chans: Channels} {Net: Symmetric_Network}.
  Context {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

  Section Potential_Definition.

Potential of a node:

0 if not enabled, else depth of the node in the spanning tree.
Note that this definition requires that the spanning tree exists. This is the reason why termination cannot be shown without the assumption on safe configurations.

    Variable (root: Node).
    Variable (Par: Node -> option Channel).
    Variable (span_tree: spanning_tree root Par)
             (Par_compat: Proper fequiv Par).

depth in the tree
    Definition depth_ (n: Node)
               (W: Acc (is_tree_parent_of Par) n): nat :=
      @Fix_F Node (is_tree_parent_of Par) (fun _ => nat)
             (fun (x: Node)
                  (f_rec: forall y: Node, is_tree_parent_of Par y x -> nat) =>
                Datatypes.S
                  (match (tree_parent Par x) as op return
                         (op == (tree_parent Par x)) -> nat
                   with
                   | None => fun _ => 0%nat
                   | Some y => fun e => (f_rec y e)
                   end (Equivalence_Reflexive (tree_parent Par x)))
             ) n W.

    Definition depth (n: Node): nat := depth_ (WF_par Par_compat span_tree n).

Potential of a node: 0 if not enabled, else depth
    Definition potential (alpha: Node -> Z) (n: Node): nat :=
      if (enabled_alpha_b Par alpha n) then (depth n) else 0%nat.

  End Potential_Definition.

  Section Potential_Compatibility.

    Lemma depth__compat:
      (Proper (respectful_dep_param (equiv (A:=nat))
                                    ((Node -> option Channel)::Node::nil)
                                    (pequiv,(equiv,tt))
                                    (inl (fun par n => Acc (is_tree_parent_of par) n)::nil)) depth_).

    Lemma depth_compat:
      Proper (respectful_dep_param pequiv
                                   (Node::(Node -> option Channel)::nil)
                                   (equiv,(pequiv,tt))
                                   ( inl (fun r p => spanning_tree r p)
                                          ::
                                          inl (fun r p => Proper fequiv p)
                                          ::
                                          nil)) depth.

    Lemma potential_compat:
      Proper (respectful_dep_param pequiv
                                   (Node::(Node -> option Channel)::nil)
                                   (equiv,(pequiv,tt))
                                   ( inl (fun r p => spanning_tree r p)
                                          ::
                                          inl (fun r p => Proper fequiv p)
                                          ::
                                          nil)) potential.

  End Potential_Compatibility.

  Section Potential_Properties.

    Variable (root: Node).
    Variable (Par: Node -> option Channel).
    Variable (span_tree: spanning_tree root Par)
             (Par_compat: Proper fequiv Par).

    Lemma depth_gt_0: forall (n: Node), gt (depth span_tree Par_compat n) 0.

Any node which is down-linked to another has smaller depth than the first one.
    Lemma deeper_depth_step:
      forall (n: Node) (child: Node),
        is_tree_parent_of Par n child ->
        depth span_tree
              Par_compat child = Datatypes.S (depth span_tree Par_compat n).

    Lemma deeper_depth:
      forall (p: list Node) (n: Node) (d: Node),
        ~ (n == d) -> directed_tree_path Par n p d ->
        (depth span_tree Par_compat n < depth span_tree Par_compat d)%nat.

  End Potential_Properties.

Results for one step of execution

  Section With_Step.

    Variable (root: Node).

    Variable (Par: Node -> option Channel) (Par': Node -> option Channel).
    Variable (Par_same: Par =~= Par') (span: spanning_tree root Par).
    Variable (Par_compat: Proper fequiv Par)
             (Par'_compat: Proper fequiv Par')
             (span': spanning_tree root Par').
    Variable (alpha: Node -> Z) (alpha': Node -> Z).
    Variable (alpha_compat: Proper fequiv alpha)
             (alpha'_compat: Proper fequiv alpha')
             (step_ok: forall n, alpha' n = NewAlpha Par alpha n \/
                                 alpha' n = alpha n)
             (progress: exists n, alpha n <> alpha' n).

New Children alphas only depends on children moves
    Lemma ChildrenAlphas_only_depends_on_children:
      forall (n: Node),
        (forall (child: Node),
            is_tree_parent_of Par n child -> alpha child = alpha' child)
        ->
        ChildrenAlphas Par alpha n == ChildrenAlphas Par' alpha' n.

New Alphas only depends on children moves
    Lemma NewAlpha_only_depends_on_children:
      forall (n: Node),
        (forall (child: Node),
            is_tree_parent_of Par n child -> (alpha child) = (alpha' child)) ->
        NewAlpha Par alpha n = NewAlpha Par' alpha' n.

When a node that was disabled becomes enabled, one of its child has actually moved.
    Lemma enabled_child_has_moved:
      forall (n: Node) (H: ~ enabled_alpha Par alpha n)
             (H': enabled_alpha Par' alpha' n),
      exists (child: Node),
        (is_tree_parent_of Par n child) /\ (alpha child) <> (alpha' child).

When a node has actually moved while none of its children moved, it is no more enabled at next configuration.
    Lemma node_has_moved_but_no_child:
      forall n, alpha n <> alpha' n
                -> (forall child, is_tree_parent_of Par n child
                                  -> alpha child = alpha' child)
                -> ~enabled_alpha Par' alpha' n.

When a node has moved, but is still enabled at next configuration, it has a child that actually also moved.
    Lemma node_has_moved:
      forall (n: Node),
        alpha n <> alpha' n -> enabled_alpha Par' alpha' n ->
        exists (child: Node),
          (is_tree_parent_of Par n child) /\ (alpha child <> alpha' child).

When a node actually moved, it is down-linked (in the spanning tree) to a node which was enabled and became disabled.
    Lemma moving_node_has_disabled_desc:
      forall (n: Node),
        alpha n <> alpha' n ->
        exists (descendant: Node),
          (exists p, directed_tree_path Par n p descendant) /\
          (enabled_alpha Par alpha descendant) /\
          not (enabled_alpha Par' alpha' descendant).

When a node that was disabled becomes enabled at next configuration, it is down-linked (in the spanning tree) to a node which was enabled and becomes disabled.
    Lemma new_enabled_node_has_disabled_descendant:
      forall (n: Node),
        not (enabled_alpha Par alpha n) ->
        (enabled_alpha Par' alpha' n) ->
        exists (descendant: Node),
          (exists p, directed_tree_path Par n p descendant) /\
          enabled_alpha Par alpha descendant /\
          ~enabled_alpha Par' alpha' descendant.

4) Proof:

there is always a node that becomes disabled after a step (potential of this node passed from >0 to 0) (induction on down path)
Within a valid step, there exists a node that was enabled but becomes disabled
    Lemma one_disabled:
      exists (n: Node), enabled_alpha Par alpha n
                        /\ ~enabled_alpha Par' alpha' n.

5) Using 3) and multiset theorem (Termination.v,

Wf_Algo_Multiset) conclude that the algorithm terminates

Termination Criteria

    Section Potential_termination_criteria.

      Lemma diff_pot:
        forall n, potential span' Par'_compat alpha' n <>
                  potential span Par_compat alpha n
                  <->
                  (~enabled_alpha Par alpha n <-> enabled_alpha Par' alpha' n).

Local Criterion
      Lemma kHopDom_local_criterion:
        forall (n: Node),
          gt (potential span' Par'_compat alpha' n)
             (potential span Par_compat alpha n)
          -> exists (n': Node),
            potential span Par_compat alpha n' <>
            potential span' Par'_compat alpha' n'
            /\
            gt (potential span Par_compat alpha n')
               (potential span' Par'_compat alpha' n).

Global Criterion

      Lemma kHopDom_global_criterion:
        exists n, potential span' Par'_compat alpha' n <>
                  potential span Par_compat alpha n.

    End Potential_termination_criteria.
  End With_Step.

End KDomSet_Termination.

Close Scope signature_scope.
Close Scope Z_scope.
Unset Implicit Arguments.