PADEC - Coq Library

Library Padec.Model.Rounds_Slices

A Framework for Certified Self-Stabilization
PADEC Coq Library

Jun 2017

Global Imports

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

Local Imports

From Padec Require Import WellfoundedUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Stream.
From Padec Require Import Simulation.
From Padec Require Import Exec.
From Padec Require Import Fairness.
From Padec Require Import ZUtils.
From Padec Require Import BoolSet.
From Padec Require Import RelationA.
From Padec Require Import ListUtils.
From Padec Require Import Rounds_inductive_def.

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

Section Round.

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

  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

  Notation NodeSet := (BoolSet (A:=Node)).
  Notation eqNodeSet := (eqBoolSet (eqA := (equiv (A:=Node)))).
  Notation leNodeSet := (leBoolSet (eqA := (equiv (A:=Node)))).
  Notation epsilon_NodeSet:=
    (epsilon_BoolSet (eqA := (equiv (A:=Node))) all_nodes_prop).

Slices and Weights

A new characterization of rounds

We consider weighted slices for the execution so that the minimum weight provides the exact number of rounds.

The execution should reach the goal predicate P; A slice is a list of nodes; we even say witness nodes since the node in the slice witnesses the way rounds are shaped. We define the weight of a slice, inductively at each step of the execution before reaching P. Any witness node has to be enabled at the considered step: when it is replaced by another node in the list for next step, it costs 1; when it moves, this cost 1; otherwise it costs 0.

TODO expliquer l'intuition, faire des exemples

Weight for non-P step and two witness nodes transition_weight g g' n n'

is 0 when n == n' and n has not moved
is 1 otherwise,

meaning there is a weight when the node executes or the slice changes node.

  Definition transition_weight (g g': Env) (n n': Node): nat :=
    if (Node_dec n n') then


      (if has_moved_b g' g n then 1 else 0) else 1.

  Instance transition_weight_compat: Proper fequiv transition_weight.

Weight for non-empty non-P slice non_empty_slice_weight e n l

n is the first element of the slice and is used for the first step of e
at each step in e, the current transition_weight is added
when the slice is empty, it costs 1
when the slice is longer than the execution, it costs the length of the remaining slice.

  Fixpoint non_empty_slice_weight
           (e: Exec) (n: Node) (l: list Node): nat :=
    match e with
    | s_one g => match l with
                  | nil => 1
                  | n'::q => 1 + non_empty_slice_weight e n' q
                  end
    | s_cons g e' => match l with
                      | nil => 1
                      | n'::q =>
                        transition_weight g (s_hd e') n n' +
                        non_empty_slice_weight e' n' q
                      end
    end.

  Instance non_empty_slice_weight_compat:
    Proper fequiv non_empty_slice_weight.

Weight for non-P slice

0 when the slice is empty, non_empty_slice_weight otherwise

  Definition slice_weight (e: Exec) (l: list Node) : nat :=
    match l with
    | nil => 0
    | n::l => non_empty_slice_weight e n l
    end.

  Instance slice_weight_compat: Proper fequiv slice_weight.

Test that a slice is actually a list of witness nodes:

when the slice is empty, the execution should satisfy the goal predicate P
for every step of the execution before the reach of P, the corresponding witness node should be enabled.

  Fixpoint enabled_until (P: Exec -> Prop) (e: Exec) (l:list Node):
    Prop :=
    match l with
    | nil => P e
    | n::q =>
      match e with
        s_one g => False
      | s_cons g e' =>
        ~ P e /\ enabled_b g n = true /\ enabled_until P e' q
      end
    end.

  Instance enabled_until_compat: Proper fequiv enabled_until.

  Lemma enabled_until_progress:
    forall P l e, Proper pequiv e ->
                  enabled_until P e l -> progress_P P e.

The minimum weighted slice until reaching P

  Inductive minimal_slice_weight_until
            (P: Exec -> Prop) (e: Exec) (N: nat): Prop :=
    mkMSWUP : forall
      (slice: list Node)
      (slice_P: enabled_until P e slice)
      (slice_rounds: slice_weight e slice = N)
      (slice_minimal: forall l, enabled_until P e l ->
                                slice_weight e l >= N),
      minimal_slice_weight_until P e N.

Getter for slice_minimal

  Definition slice_minimal (P: Exec -> Prop) (e: Exec) (N: nat)
             (MSWUP: minimal_slice_weight_until P e N) :=
    let (_, _, _, m) := MSWUP in m.

  Instance minimal_slice_weight_until_P_compat:
    Proper fequiv minimal_slice_weight_until.

Technical (direct) lemmas about the definition

  Lemma transition_weight_zero_one:
    forall (g g':Env) (n:Node) (n':Node),
      transition_weight g g' n n' = 0 \/
      transition_weight g g' n n' = 1.

minimal_slice_weight_until defines a unique weight

  Lemma minimal_slice_weight_until_P_unique:
    forall P e N1 N2,
      minimal_slice_weight_until P e N1 ->
      minimal_slice_weight_until P e N2 -> N1 = N2.

enabled_until means P is eventually reached

  Lemma enabled_until_Eventually:
    forall P e sl, enabled_until P e sl -> Eventually P e.

  Lemma non_empty_slice_weight_S:
    forall l e n, exists N , non_empty_slice_weight e n l = S N.

  Lemma non_empty_slice_weight_ge_one:
    forall e n l, non_empty_slice_weight e n l >= 1.

  Lemma minimal_slice_weight_until_P_0:
    forall (P: Exec -> Prop) e,
      P e -> minimal_slice_weight_until P e 0.

  Lemma minimal_progress:
    forall P e N, Proper pequiv e ->
                  minimal_slice_weight_until P e N -> progress_P P e.

ROUND and Weighted Slice Equivalence

  Section Round_Weighted_slice_Equivalence.

    Variable (P: Exec -> Prop)
             (P_compat: Proper fequiv P)
             (P_dec: Weak_Dec pequiv P).

Technical result for one subcase

    Lemma round_equivalence_l_subcase:
      forall N e (pe: Proper pequiv e),
        (if (zerob N) then True else
           forall e,
             Proper pequiv e ->
             At_N_rounds N P e -> minimal_slice_weight_until P e N )
        -> When_SAT (not_zerob N) P (At_N_rounds N P)
                    (enabled_b (s_hd e)) e ->
        minimal_slice_weight_until P e (1+N).

    Lemma round_equivalence_l:
      forall N e (pe: Proper pequiv e),
        At_N_rounds N P e -> minimal_slice_weight_until P e N.

    Lemma round_equivalence_r:
      forall e N (pe: Proper pequiv e),
        minimal_slice_weight_until P e N -> At_N_rounds N P e.

    Theorem round_equivalence:
      forall e N (pe: Proper pequiv e),
        At_N_rounds N P e <-> minimal_slice_weight_until P e N.

  End Round_Weighted_slice_Equivalence.

Having a weighted slice uses the equivalence above

  Definition some_slice_weight_until P e N :=
    exists slice ,
      enabled_until P e slice /\ slice_weight e slice = N.

  Lemma some_minimal_slice:
    forall P e N, minimal_slice_weight_until P e N ->
                  some_slice_weight_until P e N.

  Lemma minimal_slice_minimal:
    forall P (P_dec: Weak_Dec pequiv P) (P_compat: Proper pequiv P)
           e N,
      Proper pequiv e -> some_slice_weight_until P e N ->
      exists M , minimal_slice_weight_until P e M /\ N >= M.

  Section Round_concat.

    Variable (P: Exec -> Prop) (P_compat: Proper fequiv P).
    Variable (Q: Exec -> Prop) (Q_compat: Proper fequiv Q).

    Hypothesis Q_incl_P: forall e, Proper pequiv e -> Q e -> P e.

    Lemma enabled_until_concat:
      forall sliceP sliceQ
             e (pe: Proper pequiv e) (W: Finally P e),
        enabled_until P e sliceP ->
        enabled_until Q (@When _ P e W) sliceQ ->
        enabled_until Q e (sliceP ++ sliceQ).

    Lemma When_nth:
      forall sliceP e (pe:Proper pequiv e) (W: Finally P e),
        enabled_until P e sliceP ->
        pequiv (s_nth (length sliceP) e) (@When _ P e W).

    Lemma enabled_until_concat_nth:
      forall sliceP sliceQ eP (pe: Proper pequiv eP),
        let eQ := s_nth (length sliceP) eP in
        enabled_until P eP sliceP -> enabled_until Q eQ sliceQ ->
        enabled_until Q eP (sliceP ++ sliceQ).

    Lemma slice_weight_concat:
      forall sliceP sliceQ eP,
        let eQ := s_nth (length sliceP) eP in
        slice_weight eP (sliceP ++ sliceQ) =
        slice_weight eP sliceP + slice_weight eQ sliceQ \/
        slice_weight eP (sliceP ++ sliceQ) =
        pred (slice_weight eP sliceP + slice_weight eQ sliceQ).

    Lemma enabled_PQ_split:
      forall (P_dec: Weak_Dec pequiv P) e slicePQ,
        Proper pequiv e -> enabled_until Q e slicePQ ->
        exists sliceP sliceQ ,
          slicePQ = sliceP ++sliceQ /\
          enabled_until P e sliceP /\
          enabled_until Q (s_nth (length sliceP) e) sliceQ.

    Lemma progress_PQ:
          forall e (w: Finally P e),
            Proper pequiv e ->
            progress_P Q e -> progress_P Q (When w).

    Lemma Until_impl:
      forall (X U V: Exec -> Prop) e
             (incl: Always (fun ee => U ee -> V ee) e),
        Until X U e -> Until X V e.

    Lemma progress_PQ':
      forall e, Proper pequiv e -> Eventually Q e ->
                progress_P Q e -> progress_P P e.

    Lemma Eventually_When:
      forall (e: Exec) U (w: Finally U e) V,
        Eventually V (When w) -> Eventually V e.

    Theorem rounds_concat:
      forall (P_dec: Weak_Dec pequiv P)
             (Q_dec: Weak_Dec pequiv Q) e np nq,
        Proper pequiv e -> At_N_rounds np P e ->
        (forall w: Finally P e, At_N_rounds nq Q (@When _ P e w)) ->
        At_N_rounds (np +nq) Q e \/
        At_N_rounds (pred (np +nq)) Q e.

  End Round_concat.

used in round composition

  Section Round_simulation.

    Variable (P: Exec -> Prop) (P_compat: Proper fequiv P).

    Hypothesis P_hd: forall e e', fequiv (s_hd e) (s_hd e') -> P e <-> P e'.

    Remark P_sim_stable : forall e e', Simulation e e' -> P e <-> P e'.

    Notation same_head l1 l2 := ((hd_error l1) == (hd_error l2)).

    Lemma parcimonious_minorant:
      forall slice e,
        Proper pequiv e ->
        enabled_until P e slice ->
        exists pslice ,
          enabled_until P e pslice /\
          slice_weight e pslice <= slice_weight e slice /\
          parcimonious e pslice .

    Theorem rounds_simulation:
      forall (P_dec: Weak_Dec pequiv P) e1 e2 n,
        Simulation e1 e2 ->
        progress_P P e1 -> progress_P P e2 ->
        At_N_rounds n P e1 <-> At_N_rounds n P e2.

  End Round_simulation.

End Round.

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