PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_worst_case_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 Dijkstra_complexity_degenerated.
From Padec Require Import Dijkstra_worst_case.
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)

Bounds for N = 1 to 3 are tight

We do not prove it for N=1 or 2 since this is obvious (no value smaller than 0 step). We assume N = 3

/contains:/ I - Proof that this bound is reached (synchronous execution from (0,1,0])

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

Part I: DTRC complexity for N=3 is 3 steps at least

We exhibit wcExec3 := (sync_exec (mkEnv 0;1;0)) as a worst case execution.

We prove that the execution begins as follows: (mkEnv 0;1;0) -> (mkEnv 1;0;1) -> (mkEnv 2;1;0) -> (mkEnv 2;2;1) -> ... ~ Leg_state ~ Leg_state ~ Leg_state Leg_state

Main result wcLeg3 : At_N_steps 3 (fun e => Leg_state (s_hd e)) wcExec3.

Conclusion using Non_Leg_Steps_min_bound

Section Dijkstra_worst_case_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 using Type using Type for degenerated case (N = 3)

  Hypothesis Nis3: N = 3.

  Notation N0:=Root (only parsing).
  Definition DistN1 := (DistN1 HNk Nis3).
  Definition DistN2 := (DistN2 HNk Nis3).
  Definition Ring3 := (Ring3 Nis3).
  Definition N0notN1 := (N0notN1 HNk Nis3).
  Definition N0notN2 := (N0notN2 HNk Nis3).
  Definition vPred0 := (vPred0 Nis3).

  Lemma kge3: k >=3.

  Definition wcEnv3: Env (Algo := Dijkstra_algo) := mkEnv (0::1::0::nil).

  Definition wcEnv2: Env (Algo := Dijkstra_algo) := mkEnv (1::0::1::nil).

  Definition wcEnv1: Env (Algo := Dijkstra_algo) := mkEnv (2::1::0::nil).

  Definition wcEnv0: Env (Algo := Dijkstra_algo) := mkEnv (2::2::1::nil).

  Definition wcExec3: Exec (Algo := Dijkstra_algo) := sync_exec wcEnv3.

  Instance wcEnv3_compat:Proper pequiv wcEnv3:= mkEnv_compat (reflexivity _).
  Instance wcEnv2_compat:Proper pequiv wcEnv2:= mkEnv_compat (reflexivity _).
  Instance wcEnv1_compat:Proper pequiv wcEnv1:= mkEnv_compat (reflexivity _).
  Instance wcEnv0_compat:Proper pequiv wcEnv0:= mkEnv_compat (reflexivity _).

  Ltac value_tac DistN :=
        intros v0 v1 v2 h0 h1 h2;
        rewrite mkEnv_value;auto;
        [ rewrite DistN;reflexivity
        | rewrite Nis3;hnf;simpl;
          repeat rewrite Forall_head_and_tail;
          repeat split;try lia;
          apply Forall_nil].

      Lemma N0_value: forall (v0 v1 v2:nat),
          v0 < 3 -> v1 < 3 -> v2 < 3 ->
          v (mkEnv (v0 ::v1 ::v2 ::nil) N0) = v0.

      Lemma N1_value: forall (v0 v1 v2:nat),
          v0 < 3 -> v1 < 3 -> v2 < 3 ->
          v (mkEnv (v0 ::v1 ::v2 ::nil) N1) = v1.

      Lemma N2_value: forall (v0 v1 v2:nat),
          v0 < 3 -> v1 < 3 -> v2 < 3 ->
          v (mkEnv (v0 ::v1 ::v2 ::nil) N2) = v2.

      Ltac simpl_value:=
        (rewrite N0_value || rewrite N1_value || rewrite N2_value);[|try lia ..].

      Lemma L3_wcEnv3: L3_state wcEnv3.

      Lemma L2_wcEnv2: L2_state wcEnv2.

      Lemma L1_wcEnv1: L1_state wcEnv1.

      Lemma L0_wcEnv0: L0_state_AAB wcEnv0.

      Lemma wcEnv3_non_leg: ~ Leg_state wcEnv3.

      Lemma wcEnv2_non_leg: ~ Leg_state wcEnv2.

      Lemma wcEnv1_non_leg: ~ Leg_state wcEnv1.

      Lemma wcEnv0_leg: Leg_state wcEnv0.

      Lemma v_simpl: forall s rop, v (mkState (vltk s) rop) = v s.

      Lemma v_simpl_mod: forall s rop, v (mkState (Smod (vltk s)) rop) = (S (v s)) mod k.

      Ltac simpl_root :=
          simpl root;
          match goal with
        | [|- context [ Node_dec N0 N0]] =>
          (destruct (Node_dec N0 N0) as [EQ|NE]; [|elim NE;reflexivity])
        | [|- context [ Node_dec N1 N0]] =>
          (destruct (Node_dec N1 Root) as [EQ|NE];[elim N0notN1;symmetry;apply EQ|])
        | [|- context [ Node_dec N2 N0]] =>
          (destruct (Node_dec N2 Root) as [EQ|NE];[elim N0notN2;symmetry;apply EQ|])
        end.

      Ltac uglySharedProofScript g_ g'_ pg_ pg'_:=
        pose (g:=g_); pose (g':=g'_);
        assert (pg:=pg_); assert (pg':=pg'_);
        fold g in pg|-*; fold g' in pg'|-*;
        unfold g_ in g; unfold g'_ in g';
        assert (assume: Assume g) by apply Assume_RO_mkEnv;
        intros n_ n en;
        rewrite en;clear n_ en;
          (split; [|
                   rewrite (Stable_Variable_RUN Dijkstra_Stable);
                   change (Dijkstra_ROpart (g n)) with (Dijkstra_ROpart (g' n));
                   apply Dijkstra_ROpart_compat,pg',reflexivity]);
        change (v (RUN g n) = v (g' n));
        assert (pp:Proper pequiv (fun n => (v (RUN g n) = v (g' n)))) by
        (
          intros n1 n2 en; apply eq_compat,v_compat;
          [ apply (RUN_compat pg _ _ en)
          | apply (pg' _ _ en) ]
        );
        destruct (Ring3 n) as [en|[en|en]];
        (rewrite (pp _ _ en);clear pp en n;
         rewrite (fun n => v_compat (RUN_simpl n pg assume));
         unfold simple_run;
         simpl_root;
         rewrite ITE_sumbool_f;
         repeat rewrite v_simpl;
         repeat rewrite v_simpl_mod;
         try rewrite (vPred0 pg);
         try rewrite (vPred1 pg);
         try rewrite (vPred2 pg);
         unfold g,g'; repeat simpl_value;try reflexivity;
         simpl;apply PeanoNat.Nat.mod_small;try lia).

      Lemma wcRUN3: (RUN wcEnv3 ) =~= wcEnv2.

      Lemma wcRUN2: (RUN wcEnv2 ) =~= wcEnv1.

      Lemma wcRUN1: (RUN wcEnv1 ) =~= wcEnv0.

      Lemma wcLeg3: At_N_steps 3 (fun e => Leg_state (s_hd e)) wcExec3.

      Theorem Dijkstra_min_bound_n_is_3:
        forall bound, bound < 3 ->
                      ~ Steps_complexity bound
                        (fun e => Leg_state (s_hd e))
                        (fun e => Assume (s_hd e) /\ is_exec e).

End Dijkstra_worst_case_3.

Unset Implicit Arguments.
Close Scope nat_scope.