PADEC - Coq Library

Library Padec.KDomSet.KDomSet_correctness

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

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: Network}
          {KDP: KDomSet_parameters}
          {Graph_assumption: KDomSet_Assume}
          {Graph_network_assumption: Graph_Network_matching}.
  Let k_pos := k_pos.

  Existing Instance T_compat.

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

    Notation newAlpha n := (NewAlpha k (lcA alpha n)).

    Lemma NewAlpha_inv:
      forall (n: Node),
        alpha n = newAlpha n -> alpha n > 0 ->
        exists m , T n m /\ alpha n = alpha m + 1.
  End Alpha_child_parent.

Correctness

Section Final_kDomSet.

Assumptions on Inputs

    Variable (alpha: Node -> Z)
             (alpha_compat: Proper fequiv alpha).

    Notation newAlpha n := (NewAlpha k (lcA alpha n)).

    Variable (final: forall (n: Node), alpha n = newAlpha n).

    Definition is_kDom_path := chain (is_kDom_edge alpha).

    Lemma tall_has_path_to_root:
      forall (n: Node) (i: nat),
        alpha n = k + Z_of_nat i ->
        exists (r: Node ),
          kDominator alpha r /\
          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 alpha r /\
            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), alpha n >= k ->
                        exists (i: nat ), alpha n = k + Z.of_nat i.

    Lemma short_k:
      forall (n: Node),
        alpha n < k ->
        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),
        T m n -> alpha n < k -> 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 alpha r /\
            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 alpha r /\ 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 alpha root /\
      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.