PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_worst_case

A Framework for Certified Self-Stabilization
PADEC Coq Library

March 2017

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

Local Imports

From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.
From Padec Require Import Ring_topology.
From Padec Require Import Dijkstra_algo.
From Padec Require Import Dijkstra_common.
From Padec Require Import Dijkstra_specifications.
From Padec Require Import Self_Stabilization.
From Padec Require Import Dijkstra_specifications_proved.
From Padec Require Import Steps.
From Padec Require Import NatUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import Count.
From Padec Require All_In.
From Padec Require FoldRight.
From Padec Require Import ListUtils.

Set Implicit Arguments.
Open Scope nat_scope.

Diskstra's first token ring algorithm

Proof of self-stabilization and specification
Proof of a complexity bound in steps
Proof that this complexity bound is exact (by building a worst case prefix of execution)

Worst Case Stabilization Time

/assumes:/ Parameter k>1; the network is a unidirectional rooted ring; N <= k; N >= 4

/contains:/ Builds a prefix of execution which reaches a legitimate configuration using exactly the number of steps announced by the bound in Dijkstra_complexity

Section Simple.

simple_env is the list of values for all nodes in a ring (see mkEnv which turns a simple_env into an Env) First value is the counter at Root, followed by the values of counters at its Succ nodes.

Definition simple_env := list nat.

simple_step se n performs a step for node number n (= power Succ n Root) in simple env se. It is only correct for a node n that is enabled, i.e. holds a token). Note that a step, here, executes only one node.

  Fixpoint simple_step_Succ (ilast: nat) (se: simple_env) (n: nat):
    simple_env :=
    match se with
      nil => ilast :: nil
    | i::q =>
      match n with
        0 => ilast :: ilast :: q
      | S m => ilast :: simple_step_Succ i q m
      end
    end.

  Definition simple_step (se: simple_env) (n: nat): simple_env :=
    match se with
      nil => se
    | iroot::q =>
      match n with
        0 => S iroot :: q
      | S m => simple_step_Succ iroot q m
      end
    end.

Properties for simple_step_Succ

  Lemma simple_step_Succ_spec:
    forall i q n, n <length q ->
                  nth (S n) (simple_step_Succ i q n) 0 =
                  nth n (simple_step_Succ i q n) 0.

  Lemma simple_step_Succ_spec2:
    forall i q n, n <length q ->
                  nth (S n) (simple_step_Succ i q n) 0 = nth n (i ::q) 0.

  Lemma simple_step_Succ_spec3:
    forall i q n p, p <>S n ->
                    nth p (simple_step_Succ i q n) 0 = nth p (i ::q) 0.

Properties for simple_step

  Lemma simple_step_spec:
    forall se n, nth (S n) (simple_step se 0) 0 = nth (S n) se 0.

  Lemma simple_step_spec2:
    forall se n p, p <>n -> nth p (simple_step se n) 0 = nth p se 0.

simple_token se n states that a Token is present at position n (node power Succ n Root is enabled)

  Definition simple_token (se: simple_env) (n: nat): Prop :=
    n < length se /\
    match n with
      0 => List.hd 0 se = List.last se 0 /\ S (List.hd 0 se) < length se
    | S m => List.nth (S m) se 0 <> List.nth m se 0
    end.

  Lemma simple_token_lt_N: forall se n,
      simple_token se n -> n <length se.

simple_env_valid N se states that se represents a valid environment on a size N ring: it contains N values, all less than N

Definition simple_env_valid (N: nat) (se: simple_env): Prop :=
length se = N /\ Forall (gt N) se.

Given a valid simple env and a node with a token, the simple env then produced by simple step is still valid

  Lemma simple_step_valid: forall N se n,
      simple_env_valid N se -> simple_token se n ->
      simple_env_valid N (simple_step se n).

simple_sched: central scheduler presented by the list of nodes to be executed at each step

Definition simple_sched := list nat.

From a simple env se and a simple sched tr, run_simple_sched se tr builds the simple env which is reached after the execution of tr from se.

  Fixpoint run_simple_sched (se: simple_env) (tr: simple_sched): simple_env :=
    match tr with
    | nil => se
    | n :: q => run_simple_sched (simple_step se n) q
    end.

  Lemma run_simple_sched_app (se:simple_env) (tr1 tr2:simple_sched) :
    run_simple_sched se (tr1 ++ tr2) =
    run_simple_sched (run_simple_sched se tr1) tr2.

Illegitimate simple env (two token exist).

  Definition simple_non_leg (se: simple_env): Prop :=
    exists i , exists j , simple_token se i /\ i <> j /\
                        simple_token se j.

simple_sched_has_tokens se tr checks that all steps (from se and obtained using tr) are enabled

  Fixpoint simple_sched_has_tokens (se: simple_env) (tr: simple_sched): Prop :=
    match tr with
      nil => True
    | i :: q => simple_token se i /\
                simple_sched_has_tokens (simple_step se i) q
    end.

simple_sched_valid se tr checks that all steps (from se and obtained using tr) are enabled and the final env is illegitimate i.e., it checks simple_sched_has_tokens se tr and that the simple env reached after executing tr from se is not legitimate.

  Fixpoint simple_sched_valid (se: simple_env) (tr: simple_sched): Prop :=
    match tr with
      nil => simple_non_leg se
    | i :: q => simple_token se i /\
                simple_sched_valid (simple_step se i) q
    end.

  Lemma simple_sched_valid_alt (se:simple_env) (tr:simple_sched) :
    simple_sched_valid se tr <->
    (simple_sched_has_tokens se tr /\ simple_non_leg (run_simple_sched se tr)).

  Lemma simple_sched_app_valid (se:simple_env) (tr1 tr2:simple_sched) :
    simple_sched_has_tokens se tr1 ->
    simple_sched_valid (run_simple_sched se tr1) tr2 ->
    simple_sched_valid se (tr1 ++ tr2).

  Lemma simple_sched_app_tokens (se:simple_env) (tr1 tr2:simple_sched) :
    simple_sched_has_tokens se tr1 ->
    simple_sched_has_tokens (run_simple_sched se tr1) tr2 ->
    simple_sched_has_tokens se (tr1 ++ tr2).

  Lemma stutter_token_le: forall se j n,
      0 < n -> n <= j ->
      simple_token se n ->
      simple_token (stutter j se) n.

  Lemma stutter_token_gt: forall se j n,
      j + 2 <= n -> n < length se ->
      simple_token se (n - 1) ->
      simple_token (stutter j se) n.

  Lemma stutter_step:
    forall se j, 0 < j -> j < length se ->
                 simple_step (stutter j se) j =
                 stutter (j -1) se.

  Section Simple_Worst_Case.

N represents the number of nodes in the ring.

Variable N: nat.

building blocks for simple_envs and simple execs.

initial simple env for worst case execution For N=6, my_se = 0 :: 4 :: 3 :: 2 :: 1 :: 0 :: nil

Definition my_se: simple_env := 0 :: dc 0 (N -1).

simple scheduler for worst case execution For N=6, my_sched = 0 :: 5 :: 4 :: 3 :: 2 :: 1 :: 0 :: 5 :: 4 :: 3 :: 2 :: 1 :: 0 :: 5 :: 4 :: 3 :: 2 :: 1 :: 0 :: 5 :: 4 :: 3 :: 2 :: 1 :: 0 :: 5 :: 4 :: 3 :: 2 :: 1 ::

5 :: 4 :: 3 :: 2 :: 5 :: 4 :: 3 :: nil

    Definition my_sched: simple_sched := 0 :: repl (dc 0 N) (N -2) ++
                                           flatmap (fun p => dc p (N -p))
                                           (uc 1 (N -3)) .

    Hypothesis hN4: N >=4.

    Lemma Nsimpl: exists n , N = 4+n.

my_se has size N

Lemma my_se_length: length my_se = N.

and my_sched has size Dijkstra_exact_bound N - 1

Lemma my_sched_length: length my_sched = Dijkstra_exact_bound N - 1.

Lemma my_se_valid: simple_env_valid N my_se.

simple env definitions at various steps of the execution

    Definition se_NC0 iroot:= dc 1 iroot ++ dc (iroot -1) (N -iroot).
    Definition se_NC iroot j:= stutter j (se_NC0 iroot).
    Definition se_C0 lastconvex := rep (N -1) lastconvex ++ dc
                                       lastconvex (N -lastconvex).
    Definition se_C lastconvex j := stutter j (se_C0 lastconvex).

    Lemma se_NC0_length: forall iroot, iroot < N -> length (se_NC0 iroot) = N.

    Lemma se_NC_length:
      forall iroot j, iroot < N -> length (se_NC iroot j) = N.

    Lemma se_C0_length: forall lastconvex, lastconvex < N ->
                                           length (se_C0 lastconvex) = N.

    Lemma se_C_length: forall lastconvex j, lastconvex < N ->
                                            length (se_C lastconvex j) = N.

    Lemma my_se_step: simple_step my_se 0 = se_NC0 1.

    Lemma se_NC0_NC: forall i, i < N ->
                               (se_NC0 i ) = se_NC i (N -1).

    Lemma se_NC_middle_step:
      forall i j, i < N -> 0 < j -> j < N ->
                  simple_step (se_NC i j) j = se_NC i (j -1).

    Lemma se_NC_last_step: forall i,
        0 < i -> i <=N -2 ->
        simple_step (se_NC i 0) 0 = se_NC0 (i +1).

    Lemma se_NC0_big_step:
      forall i, 0 < i -> i <= N -2 ->
                run_simple_sched (se_NC0 i) (dc 0 N) = se_NC0 (i +1).

    Lemma se_NC_all_steps:
      run_simple_sched (se_NC0 1) (repl (dc 0 N) (N -2)) = se_NC0 (N -1).

    Lemma se_NC_C_step: simple_step (se_NC0 (N -1)) (N -1) = se_C 0 (N -2).

    Lemma se_C0_C: forall i,
        i <N -> se_C0 i = se_C i (N -1).

    Lemma se_C_middle_step: forall lc j,
        lc < j -> j < N ->
        simple_step (se_C lc j) j = se_C lc (j -1).

    Lemma se_C_C0: forall lc,
        lc < N -1 -> se_C lc lc = se_C0 (lc +1).

    Lemma se_NC_C_big_step:
      run_simple_sched (se_NC0 (N -1)) (dc 1 (N -1)) = se_C0 1.

    Lemma se_C0_big_step: forall lc,
        0 <= lc -> lc < N -1 ->
        run_simple_sched (se_C0 lc) (dc (lc +1) (N -(lc +1))) = se_C0 (lc +1).

    Lemma se_C_all_steps:
      run_simple_sched (se_NC0 (N -1)) (flatmap (fun p => dc p (N -p))
                                               (uc 1 (N -3))) =
      (se_C0 (N -3)).

    Lemma my_se_token: simple_token my_se 0.

    Lemma se_NC0_tokens: forall i j,
        1<=i -> i <N ->
        1<=j -> j <N ->
        simple_token (se_NC0 i) j.

    Lemma se_NC_root_token : forall i, 0<i -> i <=N -2 ->
                                       simple_token (se_NC i 0) 0.

    Lemma se_C0_tokens : forall lc n,
        lc < n -> n < N ->
        simple_token (se_C0 lc) n.

    Lemma se_NC0_has_tokens_all_steps :
      simple_sched_has_tokens (se_NC0 1) (repl (dc 0 N) (N - 2)).

    Lemma se_C0_has_tokens_all_steps :
      simple_sched_has_tokens (se_NC0 (N -1)) (flatmap (fun p => dc p (N -p))
                                                      (uc 1 (N -3))).

    Lemma last_se_nonleg: simple_non_leg (se_C0 (N -3)).

my_sched is a valid scheduler (i.e. at each step the node which is executed holds a token and the execution ends at a illegitimate configuration).

    Lemma my_sched_valid : simple_sched_valid my_se my_sched.

  End Simple_Worst_Case.

  Lemma worst_case:
    forall n, n >=4 -> exists se , length se = n /\ simple_env_valid n se /\
                                 exists st ,
                                   (length st ) = (Dijkstra_exact_bound n - 1)
                                   /\ simple_sched_valid se st.

End Simple.

Section Dijkstra_wc.

  Context {Chans: Channels}
          {Net: Network}
          {RURN: Rooted_Unidirectional_Ring_Network Net}
          {DP: Dijkstra_parameters}.

  Notation Algo := Dijkstra_algo.
  Notation Root := (RURN_root (Net := Net)).
  Notation Ring := (URN_topo (Net := Net)).

  Existing Instance Dijkstra_RO_assumption.

  Notation N := (Ring_size Root).

  Hypothesis HNk: N <= k.

mkEnv se builds an Env from a simple env (invalid or absent values are set to 0)

  Definition ROEnv :=
    fun n => mkROState (URN_pred_channel n)
                       (if Node_dec n Root then true else false).

  Definition mkEnv (se: simple_env): Env (Algo := Dijkstra_algo) :=
    fun n => mkState (ltk_inj k (List.nth (Dist Root n) se 0)) (ROEnv n).

  Instance mkEnv_compat:Proper fequiv mkEnv.

Link between the value of an Env and the list access

  Lemma mkEnv_value: forall se n,
      simple_env_valid N se -> v (mkEnv se n) = (List.nth (Dist Root n) se 0).

  Lemma mkEnv_ROPart: forall se n, Dijkstra_ROpart (mkEnv se n) = ROEnv n.

simple token actually specifies Token for simple env

  Lemma simple_token_Token: forall se n,
      simple_env_valid N se ->
      simple_token se (Dist Root n) -> Token (mkEnv se) n.

  Lemma Assume_RO_mkEnv: forall se, Assume_RO (ROEnv_part (mkEnv se)).

simple step actually builds an env that is a Step-successor

  Lemma simple_step_Step:
    forall se n, simple_env_valid N se -> simple_token se n ->
                 Step (mkEnv (simple_step se n)) (mkEnv se).

  Lemma simple_sched_valid_Non_leg : forall se sched,
      simple_env_valid N se -> simple_sched_valid se sched ->
      ~ Leg_state (mkEnv se).

For every simple env se and scheduler st, as far as they are valid, we can build an execution with first configuration se and such that at each step one node executes as specified by st. As we already prove convergence towards legitimate, this execution converges, but in more steps than the number of steps specified by st (since st is satisfied meaning that the last configuration reached using st is not legitimate.

  Lemma simple_sched_valid_min_steps : forall se st,
      simple_env_valid N se ->
      simple_sched_valid se st ->
      exists exec ,
        ((s_hd exec = mkEnv se ) /\ is_exec exec ) /\
        exists nn ,
          length st < nn /\
          At_N_steps nn (fun e => Leg_state (s_hd e)) exec.

  Theorem Dijkstra_min_bound:
    N >= 4 -> forall bound, bound < Dijkstra_exact_bound N ->
                            ~ Steps_complexity bound
                              (fun e => Leg_state (s_hd e))
                              (fun e => Assume (s_hd e) /\ is_exec e).

End Dijkstra_wc.

Unset Implicit Arguments.
Close Scope nat_scope.