From Coq Require Import ZArith.
From Coq Require Import Lia.
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.

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.

Section KClustering_Specification_Proved.

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

  Existing Instance KC_Stable.
  Existing Instance OrdChans.

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

  Let k_pos := k_pos.

  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).

      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.

  Section Correctness.

    Section Counting.

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

    End Counting.

    Notation kClustering_SPEC_strong :=
      (kClustering_SPEC_strong kCluster
                               

                               id
                               

                               clusterHeadID
                               

                               clusterParent).

    Lemma kClustering_partial_correctness:
      P_correctness KC_Assumption kClustering_SPEC_strong.

  End Correctness.

  Section Silent_Self_Stabilization.

    Notation kClustering_SPEC_strong :=
      (kClustering_SPEC_strong kCluster
                               

                               id
                               

                               clusterHeadID
                               

                               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.