PADEC - Coq Library

Library Padec.BFS.BFS_correctness

*Certified Round Complexity of Self-Stabilizing Algorithms*

Global Imports

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

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import NatUtils.
From Padec Require Import ListUtils.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import BFS_algo.
From Padec Require Import BFS_common.
From Padec Require Import BFS_specification.
From Padec Require Import Graph_Diameter.
From Padec Require Import Tree_topology_ALT.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

BFS Spanning Tree Under a Distributed Unfair Daemon: Correctness

This proof shows that every terminal configuration satisfies the predicate: BFS_Spannig_Tree_spec meaning that the par variables design a BFS spanning tree.

Section BFS_correctness.

  Context {Chans: Channels}
          {Net: Network}
          {Graph_assumption: BFS_Assume}
          {Graph_network_assumption: Graph_Network_matching}
          {D_Assumption: BFS_D}.
  Existing Instance G_compat.

  Notation Algo := (BFS_algo D).
  Notation Env := (Env (Net := Net) (Algo := Algo)).
  Notation terminal := (terminal (Net := Net) (Algo := Algo)).

  Notation dist := (dist G_compat G_dec Connected all_nodes_prop (DA := Node_dec)).

We consider a terminal configuration, g

Variable (g: Env) (term: terminal g) (pg: Proper pequiv g)
(ass: Input_Assume g).

Variables d are not underestimated in g

  Lemma d_not_underestimated: forall p, d (g p) >= dist p Root.

  Lemma d_is_dist: forall p, d (g p) = dist p Root.

  Lemma DistOK_true:
    forall p, ~ p == Root ->
              d (g p) = Dist_p (map S (dist_Neigh g p)).

  Lemma parOK:
    forall p, ~ p == Root -> d (g p) = S (d (g (Par g p))) /\
                             G p (Par g p).

About BFS TREE

  Lemma path_Par_ex:
    forall p, ~ p == Root ->
              exists pt , is_path (Par_Rel g) p pt Root /\
                         S (length pt) = dist p Root.

  Lemma path_Par:
    forall p pt, is_path (Par_Rel g) p pt Root ->
                 S (length pt) = dist p Root.

  Lemma Par_Rel_dist_decreases:
    forall p q pt, is_path (Par_Rel g) p pt q ->
                   dist p Root > dist q Root.

  Lemma Par_Rel_is_dag: is_dag (Par_Rel g).

  Lemma Par_Rel_single_parent: single_parent (Par_Rel g).

  Lemma Par_Rel_subgraph_G:
    is_subgraph (Par_Rel g) G.

  Lemma G_is_R_Net:
    G =~= fun n n' => exists c , is_channel n c n'.

  Lemma Par_Rel_path_to_root: forall x : Node,
      ~ x == Root ->
      exists p : list Node , is_path (Par_Rel g) x p Root.

  Lemma Par_Rel_BFS: is_BFS (Par_Rel g) G Root.

Correctness

Theorem BFS_correctness:
(BFS_Spanning_Tree_spec (Net := Net)) Root Par_Rel g.

End BFS_correctness.

Close Scope signature_scope.
Close Scope nat_scope.
Unset Implicit Arguments.