PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.KDomSet.KDomSet_correctness

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 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 KDomSet_specification.
From Padec Require Import KDomSet_alpha.

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

Correctness of the K-Dominating Set algorithm

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

  Context {Chans: Channels} {Net: Symmetric_Network}.
  Context {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

  Section KDom_Graph.

kDomSet definitions

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

    Global Instance is_kDom_edge_compat: Proper fequiv is_kDom_edge.

  End KDom_Graph.

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 (Par: Node -> option Channel)
             (Par_compat: Proper fequiv Par)
             (alpha: Node -> Z)
             (alpha_compat: Proper fequiv alpha).

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

  End Alpha_child_parent.

Correctness

  Section Final_kDomSet.

Assumptions on Inputs
    Variable (Par: Node -> option Channel)
             (Par_compat: Proper fequiv Par)
             (alpha: Node -> Z)
             (alpha_compat: Proper fequiv alpha).

    Variable (root: Node)
             (span_tree: spanning_tree root Par).

    Variable (final: forall (n: Node), ~enabled_alpha Par alpha n).

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

    Definition is_kDom_path := chain (is_kDom_edge alpha Par).

    Lemma tall_has_path_to_root:
      forall (n: Node) (i: nat),
        alpha n = k + Z_of_nat i ->
        exists (r: Node),
          kDominator Par alpha r = true /\
          exists (p: list Node), (is_kDom_path r p n).

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

    Lemma tall_is_kDominated:
      forall (n: Node) (i: nat),
        alpha n = k + Z_of_nat i ->
        forall r p, is_kDom_path r p n -> (length p <= i)%nat.

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

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

    Lemma alpha_monotonic_small:
      forall (n m: Node),
        is_tree_parent_of Par m n ->
        IsShort alpha n = true -> alpha m >= alpha n + 1.

    Lemma short_is_linked:
      forall (i: nat) (n: Node),
        alpha n = k - Z.of_nat i ->
        (exists (r: Node),
            kDominator Par alpha r = true /\
            exists (p: list Node), (is_kDom_path r p n)).

    Lemma short_is_kDominated:
      forall (i: nat) (n: Node),
        alpha n = k - Z.of_nat i ->
        forall r p, is_kDom_path r p n -> (length p <= i)%nat.

    Lemma any_is_linked:
      forall (n: Node), exists (r: Node),
          kDominator Par alpha r = true /\
          exists (p: list Node), (is_kDom_path r p n).

    Lemma any_is_kDominated:
      forall (n: Node),
      forall r p, is_kDom_path r p n -> Z.of_nat (length p) <= k.

Lemma that proves correctness: Any node is linked to dom_set head through a path of length smaller than k
    Definition IsInkDomSet (k: Z) (root: Node) (n: Node): Prop :=
      kDominator Par alpha root = true /\
      exists p, (is_kDom_path root p n) /\ (Z_of_nat (length p) <= k)%Z.

    Lemma any_is_in_kDom_set:
      forall (n: Node), exists (r: Node), IsInkDomSet k r n.

  End Final_kDomSet.

End KDomSet_Correctness.

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