PADEC - Coq Library

Library Padec.KClustering.KClustering_hd_termination

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Lia.
From Coq Require Import Bool.
From Coq Require Import Inclusion.
From Coq Require Import RelationPairs.

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 RelationA.
From Padec Require Import FoldRight.
From Padec Require Import All_In.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Spanning_Tree.
From Padec Require Import KClustering_specification.
From Padec Require Import KClustering_algo.
From Padec Require Import KClustering_def_termination.
From Padec Require Import KClustering_alpha_termination.
From Padec Require Import KClustering_pcl_termination.
From Padec Require Import P_Q_Termination.

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

Termination for KClustering Algorithm: Head Steps Only

This part shows termination of the algorithm when considering Head safe steps only. Actually, it shows safe inclusion required by the rest of the proof:

hd_safe_incl := (forall g g', Head_SafeStep g' g -> ltM (Pot_hd g') (Pot_hd g)

Section KClustering_Hd_Termination.

Channel and network

  Context {Chans: Channels} {Net: Symmetric_Network}
          {KCP: KClustering_parameters} {KCT: KC_algo_tools}.

  Variable (root: Node).
  Existing Instance KC_Stable.

  Notation Env := (Env (Algo := KC_algo)).

  Let k_pos := k_pos.

Roadmap

define the well founded relation which corresponds to the chain of pcl pointers when alpha_disabled and pcl_disabled (show that it is actually well founded)
define dist_hd (structural induction on the above well founded order)
define potential ( = N+1 - dist_hd )
prove criteria

Chain Of Pcl Pointers Defines the well founded relation which

corresponds to the chain of pcl pointers when alpha_disabled and pcl_disabled (show that it is actually well founded)

  Section Chain_Of_Pcl_Pointers.

    Definition get_pcl (g: Env) (n: Node): option Node :=
      match parCl (g n) with
        None => None
      | Some p =>
        match (peer n p) with None => None
                         | Some pn => if andb (negb (alpha_enabled_bb g n))
                                              (negb (pcl_enabled_bb g n))
                                      then (peer n p)
                                      else None
        end
      end.

    Instance get_pcl_compat: Proper fequiv get_pcl.

Well founded order

    Definition pcl_chain (g: Env): relation Node :=
      fun pn n => Some pn == get_pcl g n.

    Instance pcl_chain_compat: Proper fequiv pcl_chain.

    Lemma pcl_chain_dec:
      forall g n1 n2, {pcl_chain g n1 n2 } + {~pcl_chain g n1 n2 }.

    Lemma pcl_unique:
      forall env1 env2 n1 n2 p1 p2,
        env1 =~= env2 -> n1 == n2 ->
        pcl_chain env1 p1 n1 -> pcl_chain env2 p2 n2 -> p1 == p2.

    Lemma ap_disabled:
      forall n pn env, pcl_chain env pn n
                       -> alpha_enabled_bb env n = false /\
                          pcl_enabled_bb env n = false.

    Lemma _noclusterhead:
      forall n pn env, pcl_chain env pn n
                       -> IsClusterHead (env n) = false.

    Lemma noclusterhead_:
      forall n env, IsClusterHead (env n) = true
                    -> forall pn, ~pcl_chain env pn n.

    Lemma MinIDMinATall_IsChild:
      forall n (env: Env) (c: Channel),
        Symmetric_Network_assumption
          Net (fun n => KCpeers (env n)) (fun n => KCreverse (env n))
        -> Proper pequiv env ->
        Some c == MinIDMinATall (env n) (local_env env n) ->
        InA equiv c (Children (Par_part env) n).

    Lemma same_par_pcl:
      forall n pn (env: Env),
        Proper pequiv env ->
        Symmetric_Network_assumption
          Net (fun n => KCpeers (env n)) (fun n => KCreverse (env n)) ->
        pcl_chain env pn n
        ->
        ((alpha (env n) <? k ) = true /\
         (is_tree_parent_of (Par_part env) pn n ))
        \/
        ((alpha (env n) <? k ) = false /\
         (alpha (env n) =? k ) = false /\
         (is_tree_parent_of (Par_part env) n pn )).

    Lemma preserved_ge_alpha:
      forall env n pn, Proper pequiv env ->
                       pcl_chain env pn n -> (alpha (env n) >=? k ) = true
                       -> (alpha (env pn) >=? k ) = true.

    Lemma Acc_Tall:
      forall (n: Node) (env: Env),
        Proper pequiv env ->
        Symmetric_Network_assumption
          Net (fun n => KCpeers (env n)) (fun n => KCreverse (env n)) ->

        (alpha (env n) >=? k ) = true ->
        Acc (flip (is_tree_parent_of (Par_part env))) n ->
        Acc (pcl_chain env) n.

    Lemma Acc_Short:
      forall (n: Node) (env: Env),
        Proper pequiv env ->
        Symmetric_Network_assumption
          Net (fun n => KCpeers (env n)) (fun n => KCreverse (env n)) ->
        (alpha (env n) <=? k ) = true ->
        Acc (is_tree_parent_of (Par_part env)) n ->
        well_founded (flip(is_tree_parent_of (Par_part env))) ->
        Acc (pcl_chain env) n.

well founded

    Lemma pcl_chain_wf:
      forall (env: Env),
        Symmetric_Network_assumption
          Net (fun n => KCpeers (env n)) (fun n => KCreverse (env n)) ->
        Proper pequiv env -> spanning_tree root (Par_part env)
        -> well_founded (pcl_chain env).

  End Chain_Of_Pcl_Pointers.

Head Potentila

define dist_hd (structural induction on the above well founded order)
define potential ( = N+1 - dist_hd )

Section Hd_Potential.

Head-Distance

    Fixpoint dist_hd (env: Env) (n: Node)
             (W: Acc (pcl_chain env) n): Z :=
      match get_pcl env n as x0
            return (x0 == (get_pcl env n ) -> Z)
      with
      | Some px => fun heq => 1 + dist_hd (Acc_inv W px heq)
      | None => fun _ => 0
      end (Equivalence_Reflexive (get_pcl env n)).

    Lemma dist_hd_compat:
      forall env1 env2 n1 n2
             (A1: Acc (pcl_chain env1) n1)
             (A2: Acc (pcl_chain env2) n2),
        env1 =~= env2 -> n1 == n2 -> dist_hd A1 = dist_hd A2.

    Lemma dist_hd_cluster_head:
      forall (n: Node) (env: Env) (A: Acc (pcl_chain env) n)
             (PE: Proper pequiv env),
        IsClusterHead (env n) = true -> dist_hd A = 0.

    Lemma dist_hd_pcl:
      forall n pn env (An: Acc (pcl_chain env) n) (Apn: Acc (pcl_chain env) pn)
             (PE: Proper pequiv env),
        pcl_chain env pn n -> dist_hd An = 1+ dist_hd Apn.

    Lemma hd_pcl_chain_wf:
      forall (env: sig (Pspanning_tree root)),
        well_founded (pcl_chain (proj1_sig env)).

    Definition dist_hd' (env: sig (Pspanning_tree root)) (n: Node): Z :=
      dist_hd (hd_pcl_chain_wf env n).

    Instance dist_hd'_compat: Proper fequiv dist_hd'.

Head Potential

    Variable (NN: Z)
             (HNN: forall (env: sig (Pspanning_tree root))
                          (n: Node), NN > dist_hd' env n).

    Definition hd_potential (env: sig (Pspanning_tree root)) (n: Node): Z :=
      if andb
           (andb (negb (alpha_enabled_bb (proj1_sig env) n))
                 (negb (pcl_enabled_bb (proj1_sig env) n)))
           (hd_enabled_bb (proj1_sig env) n) then NN - dist_hd' env n
      else 0.

    Instance hd_potential_compat: Proper fequiv hd_potential.

    Lemma hd_potential_pos:
      forall env n, hd_potential env n >= 0.

  End Hd_Potential.

Results with a Head Step

  Section With_Hd_Step.

    Variable (g g': Env)
             (step: Step g' g)
             (hd_step: hd_step_b g' g = true)
             (span_tree_env: Pspanning_tree root g)
             (span_tree_env': Pspanning_tree root g').

    Variable (NN: Z)
             (HNN: forall (env: sig (Pspanning_tree root)) (n: Node),
                 NN > dist_hd' env n).

Head Global Cirteria

    Lemma hd_no_alpha_pcl_enabled_when_move:
      forall n, has_moved_b g' g n = true
                -> alpha_enabled_bb g n = false /\
                   pcl_enabled_bb g n = false.

    Lemma hd_enabled_when_move:
      forall n, has_moved_b g' g n = true
                -> hd_enabled_bb g n = true.

    Lemma hd_alpha_pcl_unchanged:
      forall n, alpha (g n) = alpha (g' n) /\ (parCl (g n)) == (parCl (g' n)).

    Lemma cluster_head_unchanged:
      forall n, IsClusterHead (g n) = IsClusterHead (g' n).

    Lemma exists_hd_move:
      exists n , has_moved_b g' g n = true /\
                hd_enabled_bb g n = true.

    Lemma hd_still_enabled:
      forall n, hd_enabled_bb g n = true ->
                hd_enabled_bb g' n = true -> has_moved_b g' g n = true
                -> exists pn , pcl_chain g pn n /\
                              hd_enabled_bb g pn = true /\
                              has_moved_b g' g pn = true.

    Lemma exists_hd_move_disabled:
      exists n , hd_enabled_bb g n = true /\
                hd_enabled_bb g' n = false /\
                has_moved_b g' g n = true.

    Lemma alpha_enabled_unchanged_hd:
      forall n, alpha_enabled_bb g n = alpha_enabled_bb g' n.

    Lemma pcl_enabled_unchanged:
      forall n, pcl_enabled_bb g n = pcl_enabled_bb g' n.

    Lemma Sg: Pspanning_tree root g.
    Lemma Sg': Pspanning_tree root g'.

    Notation sg := (exist Sg).
    Notation sg' := (exist Sg').

    Section Global_criterium.

      Lemma global_hd_criterium:
        exists n , hd_potential NN sg n <> hd_potential NN sg' n.

    End Global_criterium.

Head Local Criteria

    Lemma get_pcl_unchanged:
      forall n, (get_pcl g n ) == (get_pcl g' n ).

    Lemma dist_hd_unchanged:
      forall n, dist_hd (hd_pcl_chain_wf sg n) =
                dist_hd (hd_pcl_chain_wf sg' n).

    Lemma dist_hd'_unchanged:
      forall n, dist_hd' sg n = dist_hd' sg' n.

    Lemma hd_dont_move:
      forall n, hd_enabled_bb g n = false -> eqS (g n) (g' n).

    Section Local_criterium.

      Lemma local_crit_next_steps:
        forall n, hd_enabled_bb g n = true -> hd_enabled_bb g' n = true ->
                  has_moved_b g' g n = true ->
                  exists n', hd_enabled_bb g n' = true /\
                             hd_enabled_bb g' n' = false /\
                             has_moved_b g' g n' = true /\
                             dist_hd' sg n' < dist_hd' sg' n.

      Lemma local_hd_criterium:
        forall n,
          (hd_potential NN sg n ) < (hd_potential NN sg' n ) ->
          exists n', (hd_potential NN sg n') > (hd_potential NN sg' n )
                     /\
                     (hd_potential NN sg n') <> (hd_potential NN sg' n').

    End Local_criterium.

  End With_Hd_Step.

  Section Hd_Termination.

    Variable (NN: Z)
             (HNN: forall (env: sig (Pspanning_tree root)) (n: Node),
                 NN > dist_hd' env n).

    Definition hd_pot (sg: sig (Pspanning_tree root)) (n: Node) :=
      Z.to_nat (hd_potential NN sg n).
    Instance hd_pot_compat: Proper fequiv hd_pot.

    Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).
    Notation Pot_hd := (Pot hd_pot).

Head Termination

    Lemma hd_safe_inclusion:
      inclusion (Head_SafeStep (root := root)) (ltM @@ Pot_hd).

  End Hd_Termination.

End KClustering_Hd_Termination.

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