PADEC - Coq Library

Library Padec.KClustering.KClustering_correctness_alpha

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.

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 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.

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

Correctness of the K-Clustering algorithm: alpha-variables

Once a terminal configuration is reached, we prove that the alpha-variables draw a k-dominating set

Section KClustering_Correctness_Alpha.

Channel interface definitions

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

  Existing Instance KC_Stable.

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

  Let k_pos := k_pos.

Definition for kdom-graph

Section KDom_Graph.

kDomSet definitions

    Definition is_kDom_edge (g: Env) (x y: Node): Prop :=
      match alpha (g y) ?= k with
        | Lt => (is_tree_parent_of (Par_part g) x y)
        | Eq => False
        | Gt => (is_tree_parent_of (Par_part g) y x ) /\
                alpha (g x) = alpha (g y) - 1
      end.

    Global Instance is_kDom_edge_compat: Proper fequiv is_kDom_edge.

  End KDom_Graph.

alpha is always between 0 and 2k

  Section Range_of_alpha_Preserved.

    Lemma MinATall_range:
      forall (g: Env) (n: Node),
        k <= MinATall (g n) (local_env g n) <= 2*k +1.

    Lemma MaxAShort_range:
      forall (g: Env) (n: Node),
        -1 <= MaxAShort (g n) (local_env g n) <= k -1.

    Lemma new_alpha_0_2k :
      forall (g: Env) (n: Node),
        0 <= NewAlpha (g n) (local_env g n) <= 2*k.

  End Range_of_alpha_Preserved.

Assume that the computation of alpha provides no new value

relation on the values of alpha between children and parent

Section Alpha_child_parent.

Assumptions on Inputs

    Variable (g: Env) (pg: Proper pequiv g)
             (symm: Symmetric_Network_assumption
                      Net (fun n => KCpeers (g n))
                      (fun n => KCreverse (g n))).

    Lemma ChildrenAlphas_inv:
      forall n a,
        InA equiv a (ChildrenAlphas (g n) (local_env g n) ) ->
        exists m c , is_channel n c m /\
                    alpha (g m) = a /\
                    is_tree_parent_of (Par_part g) n m.

    Lemma NewAlpha_inv:
      forall (n: Node),
        alpha (g n) = NewAlpha (g n) (local_env g n) -> alpha (g n) > 0 ->
        exists m , is_tree_parent_of (Par_part g) n m /\ alpha (g n) =
                                                        alpha (g m) + 1.

  End Alpha_child_parent.

Correctness

Section Final_kDomSet.

Assumptions on Inputs

    Variable (g: Env) (pg: Proper pequiv g).

    Variable (root: Node)
             (span_tree: spanning_tree root (Par_part g))
             (sym: Symmetric_Network_assumption
                     Net (fun n => KCpeers (g n)) (fun n => KCreverse (g n))).

    Variable (final_alpha:
                forall (n: Node), alpha_enabled_bb g n = false).

    Lemma same:
      forall (n: Node), alpha (g n) = NewAlpha (g n) (local_env g n).

    Definition is_kDom_path := chain (is_kDom_edge g).

    Notation eqCob := (dec2b (A := option Channel) (eqoptionA_dec Channel_dec)).
    Definition IsRoot (g: Env) (p: Node) := eqCob (Par_part g p) None.

    Lemma IsRoot_is_root_equiv:
      forall n1 n2 (en: n1 == n2) g1 g2 (eg: g1 =~= g2),
        is_root (Par_part g1) n1 <-> IsRoot g2 n2 = true.

    Global Instance IsRoot_compat: Proper fequiv IsRoot.

      Definition kDominator (g: Env) (p: Node) :=
        orb (Z.eqb (alpha (g p)) k) (andb
                                       (_IsShort (alpha (g p))) (IsRoot g p)).

      Global Instance kDominator_compat: Proper fequiv kDominator.

Tall nodes

    Lemma tall_is_linked:
      forall (n: Node) (i: nat),
        alpha (g n) = k + Z_of_nat i ->
        (exists (r: Node ),
          kDominator g r = true /\
          exists (p: list Node ), (is_kDom_path r p n ))
        /\
        forall r p, is_kDom_path r p n -> (length p <= i)%nat.

    Lemma tall_k:
      forall (n: Node), _IsTall (alpha (g n)) = true ->
                        exists (i: nat ), alpha (g n) = k + Z.of_nat i.

    Lemma short_k:
      forall (n: Node),
        _IsShort (alpha (g n)) = true ->
        exists (i: nat ), (Z.of_nat i < k)%Z /\ alpha (g n) = k - 1 - Z.of_nat i.

    Lemma short_or_tall:
      forall (n: Node), {_IsShort (alpha (g n)) = true } +
                        {_IsTall (alpha (g n)) = true }.

    Lemma alpha_monotonic_small:
      forall (n m: Node),
        is_tree_parent_of (Par_part g) m n ->
        _IsShort (alpha (g n)) = true -> alpha (g m) >= alpha (g n) + 1.

    Lemma short_is_linked:
      forall (i: nat) (p: Node),
        alpha (g p) = k - Z.of_nat i ->
        (exists (kdom: Node ),
           kDominator g kdom = true /\
           exists (path: list Node ), (is_kDom_path kdom path p ))
        /\
        forall kdom path, is_kDom_path kdom path p -> (length path <= i)%nat.

    Lemma any_is_linked:
      forall (n: Node),
        (exists (r: Node ), kDominator g r = true /\
                           exists (p: list Node ), (is_kDom_path r p n ))
        /\
        forall r p, is_kDom_path r p n -> Z.of_nat (length p) <= k.

  End Final_kDomSet.

End KClustering_Correctness_Alpha.

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