PADEC - Coq Library

Library Padec.Model.RelModel

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016 - updated (change-run) April 2018

Global imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.

Local imports

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import ZUtils.
From Padec Require Import All_In.
From Padec Require Import Algorithm.

Open Scope signature_scope.
Set Implicit Arguments.

Relational Model

Semantics of the model (Algorithm, Network, Channels) using relations. Mainly, we express the fact that a configuration g can be followed by another one g' in an execution, i.e. that g -> g' is a (valid) step of the execution.

The relational semantics does not use any notion of daemon (scheduler) but consider all possible valid steps of the algorithm.

Section RelModel.

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

Environment

a.k.a. configuration (global state of the system)

Definition Env := Node -> State.

Equivalence of Environments is (weakly-)decidable

  Program Definition Env_dec (g g': Env):
    {Proper pequiv g -> Proper pequiv g' -> g =~= g' } + {~ (g =~= g')}

    :=
      let test := forallb (fun n => if State_dec (g n) (g' n)
                                    then true else false)
                          all_nodes in
      match Bool.bool_dec test true with
      | left h => left (fun pf => _)
      | right h => right (fun hh => h _)
      end.
  Obligation 1.
  Qed.
  Obligation 2.
  Qed.

Function which represents the local env of a node into a given configuration.

Precisely, given a node n and a configuration env and a channel c, (local_env env n c) returns

None if c is not a channel from n
and otherwise, Some s with s the state of the neighbor of n reached via c, in env

This relation

is compatible and also
provides the same information as neighbourhood_state_rel, above

  Definition local_env (g: Env) (n: Node) (c: Channel): option State
    := option_map g (peer n c).

  Global Instance local_env_compat: Proper fequiv local_env.

RUN: running the algorithm (function `run`) on straightforward

parameters The function is compatible.

  Definition RUN (env: Env) (n: Node): State :=
    run (env n) (local_env env n).

  Global Instance RUN_compat: Proper fequiv RUN.

Steps of the algorithm

During a step, several nodes may update their own state at the same time.

Valid step

A step is called valid when

at least one node actually moves and
every update corresponds to the algorithm execution

This relation

is compatible

NB: step from g to g'

  Record Step (g':Env) (g: Env): Prop :=
    {

these 2 coercions are ambiguous in coq 8.15

      Step_proper_r:> Proper pequiv g;

      Step_proper_l: Proper pequiv g';
      Step_progress: ~ g' =~= g;
      Step_correct: forall n, g' n == RUN g n \/ g' n == g n
    }.

  Global Instance Step_compat: Proper fequiv Step.

  Global Instance Step_Proper_r:
    forall (g' g: Env), Step g' g -> Proper fequiv g.

  Global Instance Step_Proper_l:
    forall (g' g: Env), Step g' g -> Proper fequiv g'.

Enabled

A node is said to be enabled in the current configuration when it can execute some action.

  Definition enabled_b (env: Env) (n: Node): bool :=
    if State_dec (RUN env n) (env n) then false else true.

  Global Instance enabled_b_compat: Proper fequiv enabled_b.

    Lemma enabled_b_true:
    forall (g: Env) p, enabled_b g p = true -> ~ RUN g p == g p.

  Lemma enabled_b_false:
    forall (g: Env) p, enabled_b g p = false -> RUN g p == g p.

  Definition enabled (env: Env) (n: Node): Prop := (enabled_b env n = true).

  Global Instance enabled_compat: Proper fequiv enabled.

  Lemma enabled_prop:
    forall (env: Env) (n: Node), enabled env n <-> ~ RUN env n == env n.

If a node is enabled then the system may performe a step.

  Lemma enabled_Step:
    forall (env: Env) (n: Node), Proper pequiv env ->
                                 enabled env n -> exists env', Step env' env.

has_moved_b tests if a node has moved between two environments

  Definition has_moved_b (g' g: Env) (p: Node): bool :=
    if State_dec (g' p) (g p) then false else true.

  Global Instance has_moved_b_compat: Proper fequiv has_moved_b.

  Lemma has_moved_progress:
    forall g' g p, has_moved_b g' g p = true <-> ~ g' p == g p.

  Lemma has_moved_false:
    forall g' g p, has_moved_b g' g p = false <-> g' p == g p.

  Lemma eqE_has_moved_b_false:
    forall g g', g =~= g' -> forall n, has_moved_b g g' n = false.

  Lemma has_moved_true:
    forall g' g p, Step g' g -> has_moved_b g' g p = true ->
                   g' p == RUN g p.

  Lemma Step_one_has_moved_true:
    forall g g', Step g' g -> exists n , has_moved_b g' g n = true.

  Lemma has_moved_b_enabled_b:
    forall (g' g: Env), Step g' g ->
                        forall n,
                          has_moved_b g' g n = true -> enabled_b g n = true.

  Section with_Stable_Var.

Read-Only States and Configurations

The read-only part of a configuration is always kept unchanged,

whatever be the step.

This is, henceforth, also true for valid traces
Any true property on the read only part of the initial

configuration keeps being true all along the trace.

    Variable VarType: Type.
    Variable getVar: State -> VarType.
    Variable SV: Stable_Variable _ getVar.

    Notation EnvVar := (Node -> VarType).

    Notation getVarPart :=
      (fun env: Env => fun n => getVar (env n)).

    Instance getVarPart_compat: Proper fequiv getVarPart.

    Lemma Stable_Variable_RUN:
      forall (env: Env) (n: Node), getVar (RUN env n) =~= getVar (env n).

    Lemma Stable_Variable_step:
      forall (env' env: Env),
        Step env' env -> getVarPart env' =~= getVarPart env.

    Lemma step_assume:
      forall (g g': Env) P,
        Proper (pequiv ==> iff) P ->
        P (getVarPart g) -> Step g' g -> P (getVarPart g').

  End with_Stable_Var.

Assumptions on inputs of the algorithm

  Class Stable_Assumption: Type :=
    {
      ROType: Type;
      getRO: State -> ROType;
      ROstable:> Stable_Variable _ getRO;
      Assume_RO: (Node -> ROType ) -> Prop;
      Assume_RO_compat: Proper fequiv Assume_RO;

      ROEnv := Node -> ROType;
      ROEnv_part := (fun env: Env => fun n => getRO (env n));
      Assume := (fun g: Env => Assume_RO (ROEnv_part g));
    }.

  Global Instance ROEnv_part_compat {SA: Stable_Assumption}:
    Proper pequiv ROEnv_part.

  Global Instance Assume_compat {SA: Stable_Assumption}:
    Proper pequiv Assume.

Build a Trivial assumption on the same stable variable as an exisitng one Should not be an instance -> loop

  Definition Trivial_Assumption (StA:Stable_Assumption) : Stable_Assumption :=
    @Build_Stable_Assumption
      _ _ ROstable (fun _ => True) (fun _ _ _ => conj (fun _ => I) (fun _ => I)).

  Lemma step_Assume:
    forall {SA: Stable_Assumption} (g g': Env),
      Assume g -> Step g' g -> Assume g'.

Terminal configuration

A terminal configuration is a compatible configuration from which no more step is allowed

  Definition terminal (g: Env): Prop :=
    Proper pequiv g /\ forall g', ~Step g' g.

  Definition terminal_alt (g: Env): Prop := RUN g =~= g.

  Lemma terminal_def_equiv:
    forall (g: Env), terminal g <-> terminal_alt g.

  Global Instance terminal_alt_compat: Proper fequiv terminal_alt.

  Global Instance terminal_compat: Proper fequiv terminal.

  Lemma terminal_alt_dec:
    forall g, { Proper pequiv g -> terminal_alt g } + { ~ terminal_alt g }.

  Lemma terminal_dec:
    forall g, { Proper pequiv g -> terminal g } + { ~ terminal g }.

  Lemma terminal_all_disabled:
    forall g, terminal g -> forall n, ~enabled g n.

  Lemma terminal_all_disabled_reverse:
    forall g, Proper pequiv g -> (forall n, ~enabled g n ) -> terminal g.

  Lemma terminal_dec_bis:
    forall (g: Env), Proper pequiv g -> { n | enabled g n } + { terminal g }.

  Lemma Step_not_terminal:
    forall g g', Step g' g -> ~ terminal g.

  Lemma RUN_Step: forall g, Proper pequiv g -> ~terminal g -> Step (RUN g) g.

End RelModel.

Close Scope signature_scope.
Unset Implicit Arguments.