PADEC - Coq Library

Library Padec.Model.FunModel

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global imports

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

Local imports

From Padec Require Import OptionUtil.
From Padec Require Import Stream.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.

Open Scope signature_scope.
Set Implicit Arguments.

Functional Model

Semantics of the model (Algorithm, Network, Channels) using functions. Compared to the relational model semantics, it additionnaly uses a daemon.

Looking at an execution, next step from a configuration is computed, using the run function applied on nodes selected by the daemon.

Relational and Functional semantics are proven equivalent using the daemon.

We work on executions. The daemon, in this case, in a coninductive type Daemon (each element represents the selected nodes at the current step).

We require the daemon to be sound (namely to select next state of enabled nodes only) and to achieve progress (at least one node should be selected if possible).

And we prove,

soundness: the daemon is equipped with a function that computes an execution from an initial configuration. We prove that the result is actually an execution from the algorithm.
completeness: we prove that any execution of the algorithm is actually produce using a daemon (namely that there exists a daemon which produces an equivalent execution. This latter proof builds the daemon step by step.

Section FunModel.

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

Daemon on executions

Section Daemon_Exec.

a Daemon is given by (Daemon_Step select next).

Daemon next is the daemon for next step.

The role of function select: Diff -> Diff is to represent the enabled nodes selected by the daemon. From a difference built by the algorithm, d, (select d) is another difference: for node p such that

(d p) is None, p is disabled and (select d) is also None;
(d p) is Some s, where s is the next state of p,
- p can be chosen by the daemon: in this case, (select d) equals Some s, namely (d p);
- p is not chosen by the daemon: in this case, (select d) equals None.

We call this property: soundness of the select function. We require, futhermore, that the daemon actually selects an enabled nodes if possible: this is the progress property of the select function. Those constraints on the function select are expressed in the predicate sound_progress

The fact that the daemon satisfies sound_progress at each step is expressed in the predicate is_Daemon.

    CoInductive Daemon: Type :=
      Daemon_Step:
        (Env -> Env -> Env ) ->
        (Env -> Env -> Daemon ) ->
        Daemon.

equality (partial equivalence relation) on daemon

    CoInductive eqDaemon: relation Daemon :=
      eqDaemon_Step:
        forall f1 f2,
          fequiv f1 f2 ->
          forall dm1 dm2, (fequiv ==> fequiv ==> eqDaemon ) dm1 dm2 ->
                          eqDaemon (Daemon_Step f1 dm1) (Daemon_Step f2 dm2).

    Global Instance eqDaemon_per: PER eqDaemon.

    Global Instance Daemon_PSetoid: PartialSetoid Daemon
      := @Build_PartialSetoid _ eqDaemon _.

    Definition daemon_decompose (d: Daemon): Daemon :=
      match d with Daemon_Step select next => Daemon_Step select next end.

    Lemma daemon_decomposition_lemma:
      forall (d: Daemon), d = daemon_decompose d.

constraints on the select function of the daemon: first line expresses soundness and second line progress.

    Definition sound_progress (select: Env -> Env -> Env): Prop :=
      forall g1 g2, Proper fequiv g1 -> Proper fequiv g2 ->
                    (forall n : Node, select g1 g2 n == g2 n \/ select g1 g2 n == g1 n )
                    /\
                    (select g1 g2 =~= g1 -> (g1 =~= g2 )).
    Instance sound_progress_compat:
      Proper fequiv sound_progress.

Characterization of a daemon: we require that at each step, the select function is compatible and verifies soundness and progress.

    CoInductive is_Daemon: Daemon -> Prop :=
      is_Daemon_Step:
        forall (select: Env -> Env -> Env) (next: Env -> Env -> Daemon),
          Proper fequiv select ->
          sound_progress select ->
          Proper fequiv next ->
          (forall g1 g2, Proper fequiv g1 -> Proper fequiv g2 -> is_Daemon (next g1 g2) ) ->
          is_Daemon (Daemon_Step select next).

    Global Instance is_Daemon_compat: Proper (eqDaemon ==> iff) is_Daemon.

Daemons are compatible.

Lemma is_Daemon_proper:
forall (daem: Daemon), is_Daemon daem -> Proper eqDaemon daem.

Synchronous Daemon

Example of daemon: synchronous daemon choses every enabled nodes, at each step.

    Definition sync_select (g1 g2 : Env): Env := g2.

    Global Instance sync_select_compat: Proper fequiv sync_select.

    Lemma sync_sound_progress: sound_progress sync_select.

    CoFixpoint d_sync: Daemon := Daemon_Step sync_select (fun _ _ => d_sync).

    Lemma d_sync_unfold: d_sync = Daemon_Step sync_select (fun _ _ => d_sync).

    Lemma d_sync_compat: Proper pequiv d_sync.

    Lemma d_sync_is_daemon: is_Daemon d_sync.

Soundness (execution)

Execution built from a daemon and an initial configuration:

the select function of the daemon applies to (RUN init); next configuration is then obtained with diff_eval on the result.

    CoFixpoint build_exec (init: Env) (daem: Daemon): Exec :=
      match daem with
      | Daemon_Step select next =>
        if (terminal_dec init)
        then s_one init
        else s_cons init (build_exec (select init (RUN init)) (next init (RUN init)))
      end.

    Lemma build_exec_unfold:
      forall (init: Env) (daem: Daemon),
        build_exec init daem =
        match daem with
        | Daemon_Step select next =>
          if (terminal_dec init)
          then s_one init
          else s_cons init (build_exec (select init (RUN init)) (next init (RUN init)))
        end.

Any execution (Exec) built using a daemon is actually an exection (is_exec from relational stemantics)

    Theorem computational_soundness:
      forall daem, is_Daemon daem ->
                   forall init, Proper pequiv init ->
                                is_exec (build_exec init daem).

Completeness (execution)

To prove completeness, we have to build a daemon from an execution: we build the select function as follows. Note that the result has to verify soundness and progress.

If the parameter d of the select function does not come from the execution of the algorithm (if it is not (RUN (s_hd e)), then we return d to achieve soundness (and progress).

In either case, when the execution is over, the select function selects nothing and returns None for any parameter. When the execution is going on,

if (d p) is None, then the node is disabled: we return

None also for soundness

if (d p) is not None and equals the state of p in

the next configuration of the execution, p may have moved or may have produced the same state but not moved.

if it has moved, we return (d p) to achieve soundness and progress
otherwise, it has not moved, but its local algorithm in the current state computes exactly this same state: in this case, the daemon can select it or not without changing the computation. As we have no mean to distinguish, in our model, this case, from the previous one, we also return (d p).
in the last case, ((d p) is not None, but differs from

next state), the node has not moved and we return None.

    Definition build_select (e: Exec): Env -> Env -> Env :=
      fun g1 g2 =>
        match e with
        | s_one _ => g2
        | s_cons g e' =>
          if Env_dec g1 g then
            if Env_dec g2 (RUN g1) then
              s_hd e'
            else
              g2
          else g2
        end.

    Lemma build_select_compat: Proper fequiv build_select.

    Lemma build_select_sound_progress:
      forall e (is_e: is_exec e), sound_progress (build_select e).

The daemon built from an execution simply uses build_select.

    CoFixpoint build_daemon (e: Exec): Daemon :=
      match e with
      | s_one _ => Daemon_Step (build_select e) (fun _ _ => build_daemon e)
      | s_cons _ e' => Daemon_Step (build_select e) (fun _ _ => build_daemon e')
      end.

    Lemma build_daemon_unfold:
      forall e,
        build_daemon e =
        match e with
        | s_one _ => Daemon_Step (build_select e) (fun _ _ => build_daemon e)
        | s_cons _ e' => Daemon_Step (build_select e) (fun _ _ => build_daemon e')
        end.

    Lemma build_daemon_compat: Proper pequiv build_daemon.

The daemon built from build_daemon is actually a daemon.

Lemma build_daemon_is_Daemon:
forall e, is_exec e -> is_Daemon (build_daemon e).

Completeness: the proof uses build_daemon and shows that the daemon obtained from an execution e computes an execution with build_exec which corresponds to the initial execution e.

    Theorem computational_completeness:
      forall (init: Env) (init_compat: Proper pequiv init) (e: Exec),
        is_exec e -> pequiv (s_hd e) init ->
        exists daemon , is_Daemon daemon /\
                       e =~= build_exec init daemon.

  End Daemon_Exec.

End FunModel.

Close Scope signature_scope.
Unset Implicit Arguments.