PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.KClustering.KClustering_specification_proved

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Import

From Coq Require Import ZArith.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.
From Coq Require Import RelationPairs.
From Coq Require Import Wellfounded.Union.
From Coq Require Import Morphisms_Prop.

Local Import

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import Count.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import KClustering_specification.
From Padec Require Import KClustering_algo.
From Padec Require Import Spanning_Tree.
From Padec Require Import KClustering_def_termination.
From Padec Require Import P_Q_Termination.
From Padec Require Import KClustering_alpha_termination.
From Padec Require Import KClustering_pcl_termination.
From Padec Require Import KClustering_hd_termination.
From Padec Require Import KClustering_correctness_alpha.
From Padec Require Import KClustering_correctness.
From Padec Require Import KClustering_count.

Open Scope Z_scope.
Set Implicit Arguments.

Proof of the algorithm

Section KClustering_Specification_Proved.

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


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

  Let k_pos := k_pos.

Input Assumptions:

Finite symmetric topology and Spanning tree assumption
  Definition assumptions_RO ro: Prop :=
    (forall n, equivlistA equiv (KCpeers_reverse (ro n))
                          (build_symlinks Net n)) /\
    Spanning_Tree_Network_assumption net (fun n => Par (ro n))
    /\ forall n1 n2, id (ro n1) == id (ro n2)
                     -> n1 == n2.

  Instance assumptions_RO_compat: Proper fequiv assumptions_RO.

  Lemma assume_ensures_Symmetric_Network:
    forall roenv,
      assumptions_RO roenv ->
      Symmetric_Network_assumption
        Net (fun n => KCpeers (roenv n))
        (fun n => KCreverse (roenv n)).

  Instance KC_Assumption:
    Stable_Assumption (Algo := KC_algo) (Net := net).

  Section Termination.

    Section With_root_sym.

      Variable (root: Node).

      Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).

Global Termination

      Notation SafeStep := (safeStep (safe := Pspanning_tree root)).
      Lemma KClustering_WF: well_founded SafeStep.
        Notation Trans_union := (@Trans_union _ _ _ _ root).

    End With_root_sym.

    Lemma KClustering_termination:
      termination KC_Assumption.

  End Termination.

Correctness

  Section Correctness.

    Section Counting.

      Lemma counting_OK_OK:
        forall (g: Env), Assume g -> terminal g -> counting_OK kCluster g.

    End Counting.

The specification is proven for:
    Notation kClustering_SPEC_strong :=
      (kClustering_SPEC_strong kCluster
                               
ids in the state
                               id
                               
the local information clusterHeadID provides the identifier of the clusterhead
                               clusterHeadID
                               
the local information clusterParent provides the pointer to build a route to the clusterhead
                               clusterParent).

    Lemma kClustering_partial_correctness:
      P_correctness KC_Assumption kClustering_SPEC_strong.

  End Correctness.

The algorithm is self-stabilizing and silent

  Section Silent_Self_Stabilization.

Self Stabilization is proven for:
    Notation kClustering_SPEC_strong :=
      (kClustering_SPEC_strong kCluster
                               
ids in the state
                               id
                               
the local information clusterHeadID provides the identifier of the clusterhead
                               clusterHeadID
                               
the local information clusterParent provides the pointer to build a route to the clusterhead
                               clusterParent).

    Theorem kclustering_silent_self_stabilization:
      silence KC_Assumption unfair_daemon /\
      self_stabilization KC_Assumption unfair_daemon
                (only_one kClustering_SPEC_strong).

  End Silent_Self_Stabilization.

End KClustering_Specification_Proved.

Close Scope Z_scope.
Unset Implicit Arguments.