PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.KDomSet.KDomSet_correctness_tree_topology

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 Tree_topology.
From Padec Require Import KDomSet_algo_tree_topology.
From Padec Require Import KDomSet_specification_tree_topology.
From Padec Require Import Self_Stabilization.

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}
          {DTN: Down_Tree_Network Net}
          {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

  Notation Tree := (DTN_topo (Net := Net)).
  Context {SPAN: is_spanning _ Tree}.

  Notation Algo := KDom_algo.
  Notation Env := (Env (Net := Net) (Algo := KDom_algo)).


  Notation alphas_ :=
    (fun (env: Env) n => alphas (children_states (env n) (local_env env n))).

  Notation new_alpha_ := (fun env n => new_alpha (alphas_ env n)).

Correctness

  Section Final_kDomSet.

Assumptions on Inputs
    Variable (env: Env)
             (env_compat: Proper pequiv env)
             (hassume: Assume env).

    Variable (final: forall (n: Node), enabled_b env n = false).

    Lemma same: forall (n: Node), alpha (env n) = new_alpha_ env n.

    Definition is_kDom_path := chain (is_kDom_edge env).

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

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

    Lemma tall_is_kDominated:
      forall (n: Node) (i: nat),
        alpha (env 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 (env n)) = true ->
        exists (i: nat), alpha (env n) = k + Z.of_nat i.

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

    Lemma alpha_monotonic_small:
      forall (n m: Node),
        isParent m n ->
        _IsShort (alpha (env n)) = true ->
        alpha (env m) >= alpha (env n) + 1.

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

    Lemma short_is_kDominated:
      forall (i: nat) (n: Node),
        alpha (env 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 env 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 env 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.

Correctness

    Section Correctness.

    Definition kDominator_ (g: Env) (n: Node): Prop :=
      kDominator g n = true.

    Theorem kdom_set_at_terminal:
      forall (g: Env),
        Assume g -> terminal g -> kDOM kDominator_ g (k := k).

    Lemma kDOM_partial_correctness:
      P_correctness KDom_RO_assumption (kDOM kDominator_ (k := k)).

  End Correctness.

End KDomSet_Correctness.

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