PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_complexity_degenerated

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.

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_Z.
From Padec Require Import Dijkstra_sum_dist.
From Padec Require Import Self_Stabilization.
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)

Complexity Bounds for N= 1 to 3 nodes

/contains:/ I - Proof of the complexity bound (0 steps) for N=1 or 2 II - Proof of the complexity bound (3 maximum steps) for N=3

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

Part I: DTRC Complexity for N=1 or 2 is 0 step obtained directly since every configuration is legitimate

Part II: DTRC complexity for N=3 is 3 steps at most

Basic facts about the 3-ring (nodes N0(Root) N1 N2)
Elementary characterization of DTRC states for N=3 * L3_state : 3 non-legitimate steps may be performed (but no more) * L2_state : 2 non-legitimate steps may be performed (but no more) * L1_state : 1 non-legitimate step may be performed (but no more) * L0_state : no non-legitimate step may be performed <-> Leg_state
These predicates form a partition of DTRC state for N=3
Characterization of available transitions: * L3_Step_L2_L0 : A L3_state leads to either a L2_state or a L0_state * L2_Step_L1_L0 : A L2_state leads to either a L1_state or a L0_state * L1_Step_L0 : A L1_state leads to either a L0_state
Decomposition of possible trace based of the above partition and transition graph

Detailled transition table: (!) means node moves (.) means no move L3State == ABA+ (+) means A+1 mod k == B

transitions : 3 tokens -> 7 choices !!! BAB- !!. BAA !.! BBB !.. BBA .!! AAB .!. AAA ..! ABB

L2State == ABA- (-) means A+1 mod k <> B

transitions : 3 tokens -> 7 choices !!! CAB !!. CAA !.! CBB !.. CBA .!! AAB .!. AAA ..! ABB

L1State == ABC Transitions: 2 tokens -> 3 choices .!! AAB .!. AAC ..! ABB L0State == Leg_state /ABB : 1 token -> .!. ABB 3 subcase { AAB : 1 token -> ..! AAA \AAA : 1 token -> !.. BAA

Notation Decidable A:= ({A} + {~A}) (only parsing).

Lemma or_dec: forall A B, Decidable A -> Decidable B -> Decidable (A \/ B).
Lemma and_dec: forall A B, Decidable A -> Decidable B -> Decidable (A /\ B).
Lemma not_dec: forall A, Decidable A -> Decidable (~A).

Lemma ITE_bool_f : forall A B (f:A -> B) (b:bool) a1 a2,
    f (if b then a1 else a2) = if b then (f a1) else (f a2).

Lemma ITE_sumbool_f : forall PA PB A B (f:A -> B) (sb:{PA }+{PB }) a1 a2,
    f (if sb then a1 else a2) = if sb then (f a1) else (f a2).

Lemma Smod3: forall p n : nat, 3 <= p -> S n mod p <> n.

Lemma SSmod3: forall p n : nat, 3 <= p -> S (S n mod p) mod p <> n.

Section Dijkstra_complexity_1_2_3.

  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.

Proof for degenerated case (N = 1 or 2)

  Section Degenerated_1_2.

    Hypothesis Nis1or2: N = 1 \/ N = 2.

    Theorem Dijkstra_bound_n_is_1_or_2:
      Steps_complexity 0
                       (fun e => Leg_state (s_hd e))
                       (fun e => Assume (s_hd e) /\ is_exec e).

  End Degenerated_1_2.

Proof for degenerated case (N = 3)

  Section Degenerated_3.

    Hypothesis Nis3: N = 3.

    Notation N0:=Root (only parsing).
    Definition N1:=Succ Root.
    Definition N2:=Succ N1.

    Lemma Succ0: Succ N0 == N1.
    Lemma Succ1: Succ N1 == N2.
    Lemma Succ2: Succ N2 == N0.

    Lemma Pred0: Pred N0 == N2.
    Lemma Pred1: Pred N1 == N0.
    Lemma Pred2: Pred N2 == N1.

    Lemma N0notN1: ~N0 ==N1.
    Lemma N1notN2: ~N1 ==N2.
    Lemma N0notN2: ~N0 ==N2.

    Lemma Ring3: forall n:Node,n ==N0 \/n ==N1 \/n ==N2.

    Lemma DistN0: Dist Root N0 = 0.

    Lemma DistN1: Dist Root N1 = 1.

    Lemma DistN2: Dist Root N2 = 2.

Values of predecessors

    Lemma vPred0: forall g, Proper fequiv g -> v (g (Pred N0)) = v (g N2).

    Lemma vPred1: forall g, Proper fequiv g -> v (g (Pred N1)) = v (g N0).

    Lemma vPred2: forall g, Proper fequiv g -> v (g (Pred N2)) = v (g N1).

Elementary characterization of Tokens presence/absence for each node

    Lemma Token_N0: forall g, Proper fequiv g ->
                              (v (g N0) = v (g N2)) -> Token g N0.

    Lemma no_Token_N0: forall g, Proper fequiv g ->
                                 (v (g N0) <> v (g N2)) -> ~Token g N0.

    Lemma Token_N1: forall g, Proper fequiv g ->
                              (v (g N0) <> v (g N1)) -> Token g N1.

    Lemma no_Token_N1: forall g, Proper fequiv g ->
                                 (v (g N0) = v (g N1)) -> ~Token g N1.

    Lemma Token_N2: forall g, Proper fequiv g ->
                              (v (g N1) <> v (g N2)) -> Token g N2.

    Lemma no_Token_N2: forall g, Proper fequiv g ->
                                 (v (g N1) = v (g N2)) -> ~Token g N2.

Caracterization of configs by possible exec length (see file header)

L3_state is ABA with (A+1) mod k = B

    Definition L3_state (g:Env (Algo:=Dijkstra_algo)) : Prop :=
      v (g N0) = v (g N2) /\
      ~ (v (g N0) = v (g N1)) /\
      S (v (g N0)) mod k = v (g N1).

L2_state is ABA with (A+1) mod k <> B

    Definition L2_state (g:Env (Algo:=Dijkstra_algo)):=
      v (g N0) = v (g N2) /\
      ~ (v (g N0) = v (g N1)) /\
      ~ S (v (g N0)) mod k = v (g N1).

L1_state is ABC

    Definition L1_state (g:Env (Algo:=Dijkstra_algo)):=
      ~ (v (g N0) = v (g N2)) /\
      ~ (v (g N0) = v (g N1)) /\
      ~ (v (g N1) = v (g N2)).

L0_state subcase : ABB - N1 has the token

    Definition L0_state_ABB (g:Env (Algo:=Dijkstra_algo)):=
      ~ (v (g N0) = v (g N2)) /\
      ~ (v (g N0) = v (g N1)) /\
      (v (g N1) = v (g N2)).

L0_state subcase : AAB - N2 has the token

    Definition L0_state_AAB (g:Env (Algo:=Dijkstra_algo)):=
      ~ (v (g N0) = v (g N2)) /\
      (v (g N0) = v (g N1)) /\
      ~ (v (g N1) = v (g N2)).

L0_state subcase : AAA - N0 has the token

    Definition L0_state_AAA (g:Env (Algo:=Dijkstra_algo)):=
      (v (g N0) = v (g N2)) /\
      (v (g N0) = v (g N1)) /\
      (v (g N1) = v (g N2)).

L0_state is ABB, AAB, or AAA

Definition L0_state (g:Env (Algo:=Dijkstra_algo)):=
L0_state_ABB g \/ L0_state_AAB g \/ L0_state_AAA g.

Tactic to prove decidability of formulas with integer equalities

Ltac decidability_tac:=
repeat (apply or_dec || apply and_dec || apply not_dec || apply eq_nat_dec).

Decidability results

    Lemma L3_dec: forall g, Decidable (L3_state g).
    Lemma L2_dec: forall g, Decidable (L2_state g).
    Lemma L1_dec: forall g, Decidable (L1_state g).
    Lemma L0_dec: forall g, Decidable (L0_state g).
    Lemma Leg_dec: forall g, Proper pequiv g -> Decidable (Leg_state g).

Tacttic to prove Proper for predicates with integer equalities

    Ltac compat_tac pg:=
      repeat (apply or_compat||apply and_compat||apply not_compat);
      apply eq_compat;
      repeat (apply v_compat||apply pg||apply (f_equal2 Nat.modulo)||apply (f_equal S));
      reflexivity.

Proper results

    Instance L3_compat: Proper fequiv L3_state.
    Instance L2_compat: Proper fequiv L2_state.
    Instance L1_compat: Proper fequiv L1_state.
    Instance L0_compat: Proper fequiv L0_state.

Tactic to decompose state g based on equalities between node values:

uses fresh names so we can call it twice in the same proof
all known token properties are inferred
uses congruence to prune absurd cases

    Ltac destruct_state g pg:=
      let T0 := fresh "T0_" in
      let T1 := fresh "T1_" in
      let T2 := fresh "T2_" in
      let nT0 := fresh "nT0_" in
      let nT1 := fresh "nT1_" in
      let nT2 := fresh "nT2_" in
      let EQ02 := fresh "EQ02_" in
      let EQ01 := fresh "EQ01_" in
      let EQ12 := fresh "EQ12_" in
      let NE02 := fresh "NE02_" in
      let NE01 := fresh "NE01_" in
      let NE12 := fresh "NE12_" in
      destruct (eq_nat_dec (v (g N0)) (v (g N2))) as [EQ02|NE02];
      [assert (T0:=Token_N0 pg EQ02)|assert (nT0:=no_Token_N0 pg NE02)];
      (destruct (eq_nat_dec (v (g N0)) (v (g N1))) as [EQ01|NE01];
       [assert (nT1:=no_Token_N1 pg EQ01)|assert (T1:=Token_N1 pg NE01)]);
      (destruct (eq_nat_dec (v (g N1)) (v (g N2))) as [EQ12|NE12];
       [assert (nT2:=no_Token_N2 pg EQ12)|assert (T2:=Token_N2 pg NE12)]);
      try congruence.

    Lemma Leg_state_L0:
      forall g, Proper pequiv g -> (Leg_state g <-> L0_state g ).

    Lemma state_decomp: forall g,
        Proper fequiv g -> (L3_state g \/ L2_state g \/ L1_state g \/ L0_state g ).

    Lemma disjoint_L3_L2 : forall g, L3_state g -> L2_state g -> False.

    Lemma disjoint_L3_L1 : forall g, L3_state g -> L1_state g -> False.

    Lemma disjoint_L3_L0 : forall g, L3_state g -> L0_state g -> False.

    Lemma disjoint_L2_L1 : forall g, L2_state g -> L1_state g -> False.

    Lemma disjoint_L2_L0 : forall g, L2_state g -> L0_state g -> False.

    Lemma disjoint_L1_L0 : forall g, L1_state g -> L0_state g -> False.

    Lemma Step_has_to_move: forall (g:Env) (g':Env),
        Step (Algo:=Algo) g' g ->
        has_moved_b g' g N0 = false ->
        has_moved_b g' g N1 = false ->
        has_moved_b g' g N2 = false ->
        False.

Tactic to decompose step cases based on who has moved

all known token properties are inferred
all node value (dis)equalities are inferred
the absurd case with no move is pruned
tauto may be appended to prune moves at disabled nodes

    Lemma HN1: N > 1.

    Ltac destruct_step g g' pg assume hstep :=
      let mov0 := fresh "mov0_" in
      let mov1 := fresh "mov1_" in
      let mov2 := fresh "mov2_" in
      let nop0 := fresh "nop0_" in
      let nop1 := fresh "nop1_" in
      let nop2 := fresh "nop2_" in
      let movT0 := fresh "movT0_" in
      let movT1 := fresh "movT1_" in
      let movT2 := fresh "movT2_" in
      let movN0 := fresh "movN0_" in
      let movN1 := fresh "movN1_" in
      let movN2 := fresh "movN2_" in
      let nopN0 := fresh "nopN0_" in
      let nopN1 := fresh "nopN1_" in
      let nopN2 := fresh "nopN2_" in
        (destruct (Sumbool.sumbool_of_bool (has_moved_b g' g N0)) as [mov0|nop0];
         [ assert(movT0:=has_moved_true_Token HNk HN1 assume hstep _ mov0);
           assert(movN0:=has_moved_v_Root HNk assume hstep _ (reflexivity Root) mov0);
           rewrite (vPred0 pg),Nat.add_1_r in movN0
         | assert (nopN0:= v_compat (proj1 (has_moved_false _ _ N0) nop0));
           hnf in nopN0 ]);
        (destruct (Sumbool.sumbool_of_bool (has_moved_b g' g N1)) as [mov1|nop1];
         [ assert(movT1:=has_moved_true_Token HNk HN1 assume hstep _ mov1);
           assert(movN1:=has_moved_v_non_Root assume hstep _ (N0notN1) mov1);
           rewrite (vPred1 pg) in movN1
         | assert (nopN1:= v_compat (proj1 (has_moved_false _ _ N1) nop1));
           hnf in nopN1 ]);
        (destruct (Sumbool.sumbool_of_bool (has_moved_b g' g N2)) as [mov2|nop2];
         [ assert(movT2:=has_moved_true_Token HNk HN1 assume hstep _ mov2);
           assert(movN2:=has_moved_v_non_Root assume hstep _ N0notN2 mov2);
           rewrite (vPred2 pg) in movN2
         | assert (nopN2:= v_compat (proj1 (has_moved_false _ _ N2) nop2));
           hnf in nopN2 ]);[ .. |destruct (Step_has_to_move hstep nop0 nop1 nop2)].

    Lemma L3_Step_L2_L0: forall (g:Env) (g':Env),
        Assume g -> Step g' g ->
        L3_state g -> L2_state g' \/ L0_state g'.

    Lemma L2_Step_L1_L0: forall (g:Env) (g':Env),
        Assume g -> Step g' g ->
        L2_state g -> L1_state g' \/ L0_state g'.

    Lemma L1_Step_L0: forall (g:Env) (g':Env),
        Assume g -> Step g' g ->
        L1_state g -> L0_state g'.

    Lemma exec_no_end: forall g, Assume g ->
                                 is_exec (s_one g) -> False.

    Theorem Dijkstra_bound_n_is_3:
      Steps_complexity 3
                       (fun e => Leg_state (s_hd e))
                       (fun e => Assume (s_hd e) /\ is_exec e).

  End Degenerated_3.

End Dijkstra_complexity_1_2_3.

Unset Implicit Arguments.
Close Scope nat_scope.