PADEC - Coq Library

Library Padec.Model.Rounds

*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 Lia.

Local Imports

From Padec Require Import Algorithm.
From Padec Require Import BoolSet.
From Padec Require Import SetoidUtil.
From Padec Require Import RelModel. From Padec Require Import Stream.
From Padec Require Import Exec.
From Padec Require Import ListUtils.
From Padec Require Import Fairness.

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

Rounds

In this section, we give tools to compute time complexity of an algorithm in terms of rounds.

Section Rounds.

  Context {Chans: Channels} {Net: Network} {Algo: Algorithm}
          {SA: Stable_Assumption}.

  Notation zerob := (Nat.eqb 0).
  Notation not_zerob := (fun n => negb (Nat.eqb 0 n)).

Tools

The definitions for rounds use

sets of nodes that we model as Boolean set (see BoolSet)
activated nodes (i.e., nodes that execute during a step) and neutralized nodes (i.e., nodes that becomes disabled during a step without executing).

We first introduce tools about Boolean node sets and activated and neutralized nodes.

Tools to describe Node set as Boolean sets

This type will be used to represent the set of unsatisfied nodes while computing a round. A set of unsatisfied nodes is initialized by the set of enabled nodes. It then decreases at each step by the nodes which are activated or neutralized during the step.

  Notation NodeSet := (BoolSet (A:=Node)).
  Notation eqNodeSet := (eqBoolSet (eqA := (equiv (A:=Node)))).
  Notation leNodeSet := (leBoolSet (eqA := (equiv (A:=Node)))).
  Notation is_empty := (fun S => EMPTY all_nodes S).

  Lemma eqNodeSet_dec: forall A B,
      Proper pequiv A -> Proper pequiv B ->
      {eqNodeSet A B }+{~eqNodeSet A B }.

  Definition UNSAT_init g := enabled_b g.
  Instance UNSAT_init_compat: Proper pequiv UNSAT_init.

  Definition UNSAT_update U e := diffBoolSet U (act_neut_b e).
  Instance UNSAT_update_compat: Proper pequiv UNSAT_update.

  Lemma UNSAT_shrinks (g: Env) (e: Exec) (U U': NodeSet)
        (pU: Proper fequiv U) (pg: Proper fequiv g)
        (pe: Proper pequiv e):
    eqNodeSet U' (UNSAT_update U (s_cons g e)) ->
    forall n, U' n = true -> U n = true.

  Lemma UNSAT_enabled (g: Env) (e: Exec) (U U': NodeSet)
        (pU: Proper fequiv U) (pg: Proper fequiv g)
        (pe: Proper pequiv e):
    eqNodeSet U' (UNSAT_update U (s_cons g e)) ->
    leNodeSet U (UNSAT_init g) ->
    leNodeSet U' (UNSAT_init (s_hd e)).

  Lemma UNSAT_update_incr:
    forall U U' e,
      Proper pequiv e -> leNodeSet U U' ->
      leNodeSet (UNSAT_update U e) (UNSAT_update U' e).

  Lemma UNSAT_are_enabled:
    forall U (pu: Proper pequiv U) g (pg: Proper pequiv g)
           e (pe: Proper pequiv e),
      leNodeSet U (UNSAT_init (s_hd (s_cons g e))) ->
      leNodeSet (UNSAT_update U (s_cons g e))
                (UNSAT_init (s_hd e)).

  Instance negb_compat: Proper fequiv negb.

  Lemma diff_not_empty:
    forall (s s': NodeSet),
      Proper eqNodeSet s -> Proper eqNodeSet s' ->
      ~ eqNodeSet (diffBoolSet s s') empty_BoolSet
      -> ~ eqNodeSet s empty_BoolSet.

  Lemma le_empty:
    forall U U', leNodeSet U U' ->
                 eqNodeSet U' empty_BoolSet ->
                 eqNodeSet U empty_BoolSet.

  Lemma is_empty_true:
    forall S, Proper pequiv S ->
              is_empty S = true <-> eqNodeSet S empty_BoolSet.

  Lemma is_empty_false:
    forall S, Proper pequiv S ->
              is_empty S = false <-> ~ eqNodeSet S empty_BoolSet.

  Lemma le_U_enabled:
    forall e U p,
      U p = true -> leNodeSet U (UNSAT_init (s_hd e)) ->
      enabled_b (s_hd e) p = true.

  Lemma empty_act_neut:
    forall e U p,
      U p = true -> eqNodeSet (UNSAT_update U e) empty_BoolSet
      -> act_neut_b e p = true.

  Lemma in_diff_act_neut:
    forall e U p,
      U p = true -> UNSAT_update U e p = false ->
        act_neut_b e p = true.

  Lemma in_diff_not_act_neut:
    forall e U p,
      U p = true -> UNSAT_update U e p = true ->
        act_neut_b e p = false.

Round Definition

  CoInductive at_most_rounds_aux (P: Exec -> Prop):
    NodeSet -> nat -> Exec -> Prop :=
  | rnd_here: forall U n e, P e -> at_most_rounds_aux P U n e
  | rnd_in: forall U n g e,
      at_most_rounds_aux P (UNSAT_update U (s_cons g e)) n e ->
      n > 0 ->
      ~eqNodeSet (UNSAT_update U (s_cons g e)) empty_BoolSet ->
      at_most_rounds_aux P U n (s_cons g e)
  | rnd_chge: forall U n g e,
      at_most_rounds_aux P (UNSAT_init (s_hd e)) n e ->
      eqNodeSet (UNSAT_update U (s_cons g e)) empty_BoolSet ->
      at_most_rounds_aux P U (S n) (s_cons g e).

  Definition at_most_rounds (P: Exec -> Prop) (n: nat) (e: Exec): Prop :=
    at_most_rounds_aux P (UNSAT_init (s_hd e)) n e.

  Lemma at_most_rounds_aux_incr:
    forall P U n e, at_most_rounds_aux P U n e ->
                    forall n', n' >= n ->
                               at_most_rounds_aux P U n' e.

  Lemma at_most_rounds_incr:
    forall P n e, at_most_rounds P n e ->
                  forall n', n' >= n -> at_most_rounds P n' e.

  Instance at_most_rounds_aux_compat:
    Proper pequiv at_most_rounds_aux.

  Instance at_most_rounds_compat: Proper pequiv at_most_rounds.

  Lemma at_most_rounds_equiv_context:
    forall (P1: Exec -> Prop) (P2: Exec -> Prop)
           Q e (pe: Proper pequiv e) k,
      (Always Q) e -> Always (fun e => P1 e -> P2 e) e ->
      at_most_rounds P1 k e -> at_most_rounds P2 k e.

  Lemma at_most_rounds_cov:
    forall (P1: Exec -> Prop) (P2: Exec -> Prop)
           e (pe: Proper pequiv e) k
           (impl2: Always (fun e => P1 e -> P2 e) e),
      at_most_rounds P1 k e -> at_most_rounds P2 k e.

Function Round Definition as long as one can compute the reachability of the predicate.

count_rounds_aux assumes Finally P e (i.e. reachability of P can be computed); it uses a set of unsatisfied nodes.

Either Finally tells that P is reached, hence one round
Or the set of unsatisfied is refreshed by removing moving or neutralized nodes. If this new set is empty, this starts a new round (add 1 and initialize the new set of unsatisfied with the enabled nodes of the current configuration) otherwise we go on the current round.

  Fixpoint count_rounds_aux (P: Exec -> Prop) (g: Env) (e: Exec)
           (U: NodeSet) (F: Finally P e): nat :=
    match F with
    | finally_now _ _ _ => 1

    | @finally_not_yet _ _ g' e' _ F' =>
      if is_empty (UNSAT_update U (s_cons g e))
      then 1 + count_rounds_aux g' (UNSAT_init g') F'
      else count_rounds_aux g' (UNSAT_update U (s_cons g e)) F'
    end.

count_rounds provides the number of rounds to reach P. It compute the 0 case separately. Otherwise it uses count_rounds_aux and initialize the new set of unsatisfied with the enabled nodes of the initial configuration.

  Definition count_rounds
             (P: Exec -> Prop) (P_dec: Weak_Dec pequiv P)
             (e: Exec) (pe: Proper pequiv e)
             (he: Eventually P e): nat :=
    match (Eventually_Dec_Finally' P_dec pe he) in
          Finally _ e_ return nat with
    | finally_now _ _ _ => 0
    | finally_not_yet g' e' F' =>
      count_rounds_aux g' (UNSAT_init g') F'
    end.

  Lemma count_rounds_aux_S: forall P g e U (F: Finally P e),
      count_rounds_aux g U F <> 0.

Progress Towards P

Simplfied assumption about an execution converging towards a goal P; if not yet reached, then there should be some enabled node(s).

  Definition progress_P (P: Exec -> Prop) (e: Exec): Prop :=
    Eventually P e ->
    Until (fun e => ~ eqNodeSet (UNSAT_init (s_hd e))
                      empty_BoolSet) P e.

  Lemma progress_P_is_exec:
    forall P (P_dec: Weak_Dec pequiv P) e,
      is_exec e -> progress_P P e.
  Lemma progress_P_contd:
    forall P e g, progress_P P (s_cons g e)
                  -> ~ P (s_cons g e) -> progress_P P e.

  Lemma progress_P_now:
    forall P e, progress_P P e -> Eventually P e -> ~ P e ->
                ~ eqNodeSet (UNSAT_init (s_hd e)) empty_BoolSet.

  Theorem round_functional_equivalence:
    forall P (P_dec: Weak_Dec pequiv P)
           (P_compat: Proper pequiv P)
           e (pe: Proper pequiv e) (he: Eventually P e)
           (pP: progress_P P e) n,
      at_most_rounds P n e <->
      exists n', n' <= n /\ count_rounds P_dec pe he = n'.

  Lemma round_functional_equivalence':
    forall P (P_dec: Weak_Dec pequiv P)
           (P_compat: Proper pequiv P)
           e (pe: Proper pequiv e) (he: Eventually P e)
           (pP: progress_P P e) n',
      count_rounds P_dec pe he = n' ->
        forall n, n' <= n -> at_most_rounds P n e.

Induction Schema - Usual Proof Pattern to prove Round Complexity

  Lemma rnd_glue0:
    forall P (pc: Proper pequiv P) e (pe: Proper pequiv e)
           U U' (pu': Proper pequiv U'),
      leNodeSet U U' ->
      at_most_rounds_aux P U 1 e ->
      at_most_rounds_aux P U' 1 e.

  Lemma rnd_glue:
    forall P (pc: Proper pequiv P) e (pe: Proper pequiv e)
           U (pu: Proper pequiv U) U' (pu': Proper pequiv U'),
      leNodeSet U U' -> leNodeSet U' (UNSAT_init (s_hd e)) ->
      at_most_rounds_aux P U' 1 e ->
      at_most_rounds_aux P U 2 e.

  Lemma schema_round_step:
    forall (P1 P2: Exec -> Prop) (P1c: Proper pequiv P1)
           (P2c: Proper pequiv P2)
           (n: nat) (e: Exec) (pe: Proper pequiv e),
      Always (fun e => P1 e -> at_most_rounds P2 1 e) e ->
      at_most_rounds P1 n e -> at_most_rounds P2 (S n) e.

  Lemma schema_round_induction:
    forall (P: nat -> Exec -> Prop) (Pc: Proper pequiv P)
           (B: nat) (e: Exec) (pe: Proper pequiv e),
      P 0 e ->
      Always (fun e => forall k,
                  k < B -> P k e ->
                  at_most_rounds (P (S k)) 1 e) e ->
      at_most_rounds (P B) B e.
  Lemma at_most_rounds_forall:
    forall (P: Node -> Exec -> Prop) k e (pe: Proper pequiv e),
      (forall p,
          at_most_rounds (Always (P p)) k e ) <->
      at_most_rounds (fun e => forall p, Always (P p) e) k e.

  Lemma at_most_rounds_forall':
    forall (P: Node -> Exec -> Prop) (pc: Proper pequiv P)
           k e (pe: Proper pequiv e),
      (forall p,
          at_most_rounds (Always (P p)) k e ) <->
      at_most_rounds (Always (fun e => forall p, (P p) e)) k e.

  Definition Round_complexity (Q P: Exec -> Prop) (k: nat) :=
    forall exec, Q exec -> at_most_rounds P k exec.

Compatibility for Round_complexity requires more assumption:

  Lemma Round_complexity_compat:
    forall n1 n2 (en: n1 == n2)
           P1 P2 (eP: fequiv P1 P2)
           (Q1 Q2: Exec -> Prop) (eQ: fequiv Q1 Q2)
           (hp1: forall e, Q1 e -> Proper pequiv e)
           (hp2: forall e, Q2 e -> Proper pequiv e),
      Round_complexity Q1 P1 n1 == Round_complexity Q2 P2 n2.

Compatibility for Round_complexity with implies:

  Lemma Round_complexity_compat_cov:
    forall n1 n2 (en: n1 == n2)
           (P1: Exec -> Prop) (P1c: Proper pequiv P1)
           (P2: Exec -> Prop) (P2c: Proper pequiv P2)
           (Q1: Exec -> Prop) (Q1c: Proper pequiv Q1)
           (Q2: Exec -> Prop) (Q2c: Proper pequiv Q2)
           (eQ: (pequiv ==> impl ) Q2 Q1)
           (eP: forall e, Q2 e -> Always (fun e => P1 e -> P2 e) e)
           (hp2: forall e, Q2 e -> Proper pequiv e),
      Round_complexity Q1 P1 n1 -> Round_complexity Q2 P2 n2.

  Lemma at_most_rounds_scheme_per_node:
    forall e (ise: is_exec e) (ass: Assume (s_hd e))
           (P: Node -> Exec -> Prop) p
           (cnd_here: enabled_b (s_hd e) p = false -> P p e)
           (cnd_act:
              Always (fun e =>
                        act_neut_b e p = true ->
                        match e with
                          s_one _ => True
                        | s_cons g e' => P p e' end) e) k,
      at_most_rounds (P p) (S k) e.

Results with weakly fair daemon

weakly_fair e -> forall U included in (enabled e), Eventually (U becomes empty) nb: this requires to define a new Eventually property, with accumulator how to prove this??? coind prop ---> ind prop

prove that: wf e -> forall node n, Eventually (n is not in U) uses the Eventually part in the weakly_fair definition -- ok

lemma above should be provable using induction on Eventually (U becomes empty)

  Lemma UNSAT_update_le:
    forall U (pu: Proper pequiv U) e (pe: Proper pequiv e),
      leNodeSet (UNSAT_update U e) U.

  Lemma UNSAT_update_empty:
    forall U e, eqNodeSet U empty_BoolSet ->
                eqNodeSet (UNSAT_update U e) empty_BoolSet.

  CoFixpoint build_pair_U_e U e :=
    match e with
    | s_one g => s_one (U , g)
    | s_cons g e => s_cons (U , g) (build_pair_U_e (UNSAT_update U (s_cons g e)) e)
    end.

  Lemma build_pair_U_e_s_hd:
    forall U e, s_hd (build_pair_U_e U e) = (U , s_hd e ).

  Lemma build_pair_U_e_s_one:
    forall U g, build_pair_U_e U (s_one g) = s_one (U , g ).

  Lemma build_pair_U_e_s_cons:
    forall U g e, build_pair_U_e U (s_cons g e) =
                  s_cons (U , g )
                         (build_pair_U_e (UNSAT_update U (s_cons g e)) e).

  Instance build_pair_U_e_compat: Proper pequiv build_pair_U_e.

  Lemma build_pair_U_e_not_increasing_1:
    forall U (pU: Proper pequiv U) e (pe: Proper pequiv e) n,
      U n = false ->
      Always (fun x => fst (s_hd x) n = false)
             (build_pair_U_e U e).

  Lemma build_pair_U_e_not_increasing:
    forall U (pU: Proper pequiv U)
           e (pe: Proper pequiv e)
           (hU: leNodeSet U (UNSAT_init (s_hd e))),
    forall n,
      Always
        (fun x =>
           fst (s_hd x) n = false ->
           Always (fun x' => fst (s_hd x') n = false) x)
        (build_pair_U_e U e).

  Lemma Eventually_forall:
    forall A (PSA: PartialSetoid A)
           (x: Stream (A := A)) (px: Proper pequiv x)
           (P: Node -> Stream (A := A) -> Prop) (pP: Proper pequiv P),
      (forall n, Eventually (P n) x ) ->
      (forall n, Always (fun x' => P n x' -> Always (P n) x') x ) ->
      Eventually (fun x' => forall n, P n x') x.

  Lemma weakly_fair_enabled_becomes_empty:
    forall e (pe: Proper pequiv e),
      weakly_fair e ->
      forall U, Proper pequiv U ->
                leNodeSet U (UNSAT_init (s_hd e)) ->
                Eventually (fun x => eqNodeSet (fst (s_hd x)) empty_BoolSet)
                           (build_pair_U_e U e).

  Lemma at_most_rounds_weakly_fair:
    forall e, Proper pequiv e -> weakly_fair e ->
              forall P n,
                at_most_rounds P n e -> Eventually P e.

End Rounds.

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