PADEC - Coq Library

Library Padec.MessagePassing.RelModelMP

A Framework for Certified Self-Stabilization
PADEC Coq Library

Jan 2019 (Description of steps for message-passing systems)

Global imports

From Coq Require Import PeanoNat.
From Coq Require Import Lia.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.
From Coq Require Import Streams.

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 AlgorithmMP.

Open Scope signature_scope.
Set Implicit Arguments.

Relational Model

Semantics of the model (AlgorithmMP, DirNetwork, *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 RelModelMP.

Context {InChans: InChannels} {OutChans: OutChannels} {DNet: DirNetwork} {Algo: MPAlgorithm}.

Message tags

For ease of manipulation, a message existing at some point will never be removed from the configuration. In order to keep track of its status however, a message tag is attached to it.

Inductive MsgTag : Type :=
| lost : MsgTag

The message has been lost, i.e. deleted by the adversary.

| rejected : MsgTag

The message has been rejected by the channel, due to its limited capacity.

| received : MsgTag

The message has been received, i.e. read, at the destination.

| pending : MsgTag.

The message is still in the channel.

Type Message

The type Message is used to store all the information about a message: its destination, its contents, and its current status.

  Record Message :Type :=
    {
      destination: Node *InChannel;
      contents: Msg;
      status: MsgTag
    }.

  Definition eqMessage: relation Message :=
    fun m1 m2 =>
      destination m1 == destination m2 /\
      contents m1 == contents m2 /\
      status m1 = status m2.

  Instance eqMessage_equiv: Equivalence eqMessage.

  Global Instance Message_Setoid : Setoid Message:= {|equiv:=eqMessage |}.

  Instance Build_Message_compat:
    Proper ((RelationPairs.RelProd equiv equiv ) ==> equiv ==> eq ==> equiv) Build_Message.

  Instance destination_compat:
    Proper fequiv destination.

  Instance contents_compat:
    Proper fequiv contents.

  Instance status_compat:
    Proper (equiv ==> eq) status.

  Instance consA_compat {A:Type} {SA:Setoid A}:
    Proper fequiv (@cons A).

Some properties enabling to easily manipulate options

property strongly holds on an option

  Definition PoptionA {A: Type} (P: A -> Prop) (optA: option A) : Prop :=
    match optA with
      | Some a => P a
      | None => False
      end.

  Lemma PoptionA_and {A: Type} (optA: option A) (P P': A -> Prop):
      PoptionA (fun a => P a /\ P' a) optA
        <->
      PoptionA P optA /\ PoptionA P' optA.

  Lemma PoptionA_decidable {A: Type} (P: A -> Prop):
    (forall a, {P a } + {~ P a })
      ->
    (forall o, {PoptionA P o } + {~ PoptionA P o }).

count_tag is a small function allowing to count the number of messages sent to a given destination and having the appropriate MsgTags.

  Fixpoint count_tag (l: list Message) (dest: (Node *InChannel))
                     (tag_wt: MsgTag -> nat): nat :=
    match l with
    | nil => O
    | m::ll =>
        if dest_dec (destination m) dest then
          (tag_wt (status m)) + count_tag ll dest tag_wt
        else count_tag ll dest tag_wt
        end.

  Instance count_tag_compat:
    Proper (equiv ==> equiv ==> eq ==> eq) count_tag.

count_tag is non-decreasing w.r.t. cons

  Lemma count_tag_cons_remove (l: list Message) (dest: (Node *InChannel))
                       (m: Message) (tag_wt: MsgTag -> nat):
    count_tag l dest tag_wt <= count_tag (m :: l) dest tag_wt.

count_tag comparisons with le can ignore identical heads

  Lemma count_tag_cons_le (l l': list Message) (dest: (Node *InChannel))
                       (m: Message) (tag_wt: MsgTag -> nat):
    count_tag l dest tag_wt <= count_tag l' dest tag_wt
      <->
    count_tag (m :: l) dest tag_wt <= count_tag (m :: l') dest tag_wt.

count_tag is linear w.r.t. cons

  Lemma count_tag_cons_dest (l: list Message) (dest: (Node *InChannel))
                       (m: Message) (tag_wt: MsgTag -> nat):
    destination m == dest ->
      count_tag (m :: l) dest tag_wt = tag_wt (status m) + count_tag l dest tag_wt.

count_tag is linear w.r.t. ++

  Lemma count_tag_app (l1 l2: list Message) (dest: (Node *InChannel))
                     (tag_wt: MsgTag -> nat):
    count_tag (l1 ++ l2) dest tag_wt = count_tag l1 dest tag_wt + count_tag l2 dest tag_wt.

Some weight functions to be used with count_tag

  Definition rejected_wt (t: MsgTag): nat :=
    match t with
      rejected => 1
    | _ => 0
    end.

  Definition pending_wt (t: MsgTag): nat :=
    match t with
      pending => 1
    | _ => 0
    end.

An obvious equivalence between count_tag pending_wt being positive and the existence of a pending message.

  Lemma count_tag_pending (dest : Node * InChannel) (m : Message):
    status m = pending -> destination m == dest ->
      forall l : list Message, In m l -> count_tag l dest pending_wt > 0.

  Lemma count_tag_pending' (dest : Node * InChannel) (l : list Message):
    count_tag l dest pending_wt > 0 ->
    exists msgId : nat ,
      PoptionA (fun m => destination m == dest /\ status m = pending) (nth_error l msgId).

Environment

a.k.a. configuration (global state of the system). This corresponds to the states of the nodes and the messages in the channels. As pointed out before, even old messages that are not anymore in the channels are stored. Moreover, all messages from the different channels are stored in a unique list.

  Record Env : Type :=
    {
      Node_env : Node -> State ;
      Channel_env : list Message
    }.

  Definition eqEnv: relation Env := fun g1 g2 =>
      (Node_env g1 =~= Node_env g2 ) /\
      (Channel_env g1 == Channel_env g2 ).

  Instance eqEnv_per: PER eqEnv.

  Instance Env_partial_setoid:
    PartialSetoid Env:=
    {| pequiv:=eqEnv |}.

  Global Instance Node_env_compat:
    Proper fequiv Node_env.

  Global Instance Channel_env_compat:
    Proper fequiv Channel_env.

Event

An event corresponds to the activation of a node, and possibly the reception of an incoming message (given by its position in the global list). A step will be basically the change from an environment to another, caused by an event.

  Record Event: Type :=
    {
      active_node: Node;
      recv_id: nat

    }.

  Definition eqEvent: relation Event :=
    fun ev1 ev2 =>
      (active_node ev1 == active_node ev2 ) /\
      (recv_id ev1 == recv_id ev2 ).

  Instance eqEvent_equiv: Equivalence eqEvent.

  Instance Event_setoid:
    Setoid Event:=
    {| equiv:=eqEvent |}.

  Instance active_node_compat:
    Proper fequiv active_node.

  Instance nth_error_compat: forall (A:Type) (SA: PartialSetoid A),
      Proper fequiv (nth_error (A:=A)).

  Lemma nth_error_equiv_eq: forall (A:Type) (S: Setoid A) l n,
    nth_error l n == None -> nth_error l n = None.

  Lemma nth_error_app {A} (P: A -> Prop) (l l' : list A):
    forall (n: nat),
      match nth_error l n with
      | Some a => P a
      | None => False
      end ->
      match nth_error (l ++ l') n with
      | Some a => P a
      | None => False
      end.

  Lemma nth_error_Forall {A} {P P': A -> Prop} {n: nat} {l : list A}:
    PoptionA P' (nth_error l n)
      ->
    Forall P l
      ->
    PoptionA P (nth_error l n).

Function getMessage

This function retrieves a message of given ID in an environment. The output is an option Message because the function outputs None when the message ID does not exist in the provided environment.

  Definition getMessage (env: Env) (msgid: nat):
    option Message := nth_error (Channel_env env) msgid.

  Instance getMessage_compat:
    Proper fequiv getMessage.

Function tag_Msg

This function constructs a complete pending message (including the correct destination) from a sender, and a pair consisting of an outcoming channel and a message contents. The output is an option Message because the function outputs None when the outcoming channel does not exist at the sender.

  Definition tag_Msg (sender:Node)
             (pmsg: OutChannel * Msg) :
    option Message :=
    option_map (fun dest => {|
      destination := dest;
      contents := snd pmsg;
      status := pending;
                  |}) (inLink (sender ,fst pmsg )).

  Instance tag_Msg_compat:
    Proper fequiv tag_Msg.

A message produced by tag_Msg is pending

Lemma tag_Msg_pending_one (sender:Node) (pmsg: OutChannel * Msg):
forall m, Some m = tag_Msg sender pmsg -> status m = pending.

Messages produced by tag_Msg are pending

  Lemma tag_Msg_pending_list (sender: Node) (dest: Node * InChannel) (m: Message):
    forall l, In m (ListUtils.map_filter (tag_Msg sender) l)
        -> status m = pending.

No messages produced by tag_Msg are rejected

  Lemma count_tag_tag_Msg (sender: Node) (dest: Node * InChannel):
    forall (l : list (OutChannel * Msg)),
      count_tag (ListUtils.map_filter (tag_Msg sender) l) dest rejected_wt = 0.

Function append_new_messages

This function appends to a list of (complete) messages a list of somehow local messages sent by some sender node. All the new messages are considered pending

  Definition append_new_messages
             (CE:list Message) (sender:Node)
             (sent: list (OutChannel *Msg)) :=
    CE ++ map_filter (tag_Msg sender) sent.

  Instance append_new_messages_compat:
    Proper fequiv append_new_messages.

Function mark_as_read

Gives the received status to the message of the given ID in the given global list of messages.

  Fixpoint mark_as_read (CE:list Message) (msgid:nat) :=
    match CE with
    | nil => nil
    | cons mesg q =>
      match msgid with
        O => cons {| destination:=destination mesg;
                     contents:=contents mesg;
                     status:=received |} q
      | S id' => cons mesg (mark_as_read q id')
      end
    end.

  Instance mark_as_read_compat:
    Proper fequiv mark_as_read.

mark_as_read does not modify the length of the list

Lemma mark_as_read_length (l: list Message) :
forall msgid, length l = length (mark_as_read l msgid).

mark_as_read does not modify the destination of the messages

  Lemma mark_as_read_destination (dest : Node * InChannel) (msgId msgId': nat):
    forall l : list Message,
      PoptionA (fun m => destination m == dest) (nth_error l msgId)
        ->
      PoptionA (fun m => destination m == dest) (nth_error (mark_as_read l msgId') msgId).

mark_as_read does not make increase the number of pending messages

Lemma mark_as_read_pending (l: list Message) (dest: Node * InChannel):
forall msgId, count_tag (mark_as_read l msgId) dest pending_wt <= count_tag l dest pending_wt.

mark_as_read decreases the number of pending messages if the read message exists and has the studied destination

  Lemma mark_as_read_pending_decr l dest msgId msgId':
    PoptionA (fun m => destination m == dest /\ status m = pending) (nth_error l msgId)
      ->
    PoptionA (fun m => ~ status m = pending) (nth_error (mark_as_read l msgId') msgId)
      ->
    count_tag (mark_as_read l msgId') dest pending_wt < count_tag l dest pending_wt.

  Definition update_pfun (A B:Type) (SA:PartialSetoid A)
             (Adec:Decider (pequiv (A:=A))) (F:A -> B) (a:A) (b:B) : A -> B :=
    fun a_ => if Adec a a_ then b else F a_.

  Definition update_fun (A B:Type) (SA:Setoid A)
             (Adec:Decider (equiv (A:=A))) (F:A -> B) (a:A) (b:B) : A -> B :=
    fun a_ => if Adec a a_ then b else F a_.

  Instance update_fun_compat: forall (A B:Type)
                                     (SA: Setoid A) (SB: PartialSetoid B)
                                     (Adec:Decider (equiv (A:=A))),
      Proper fequiv (@update_fun A B SA Adec ).

Function update_env

Fully transforms the environment according to the event and the other inputs:

change of state
a message is marked as read, if relevant
sent messages are stored in the channel

  Definition update_env
             (g:Env) (ev:Event)
             (output: State *(list (OutChannel *Msg)))
    : Env := {|
              Node_env:=
                update_fun _ (Node_dec) (Node_env g) (active_node ev) (fst output);
              Channel_env:=
                append_new_messages (mark_as_read (Channel_env g) (recv_id ev))
                  (active_node ev) (snd output)
            |}.

  Instance update_env_compat:
    Proper fequiv update_env.

Function read_mesg

Gets from the environment the incoming channel and the contents of the message specified in the event. It returns none if the message ID in the event does not correspond to an existing message. (The function does not check whether the message is indeed intended to the active node.)

  Definition read_mesg
             (g:Env) (ev:Event ) : option (InChannel *Msg) :=
    match getMessage g (recv_id ev) with
    | None => None
    | Some mesg =>

      Some (snd (destination mesg),contents mesg)
    end.

  Instance read_mesg_compat:
    Proper fequiv read_mesg.

Relation RchangeTag

States that the only difference between m1 and m2 is that the status may have changed from pending to rejected or lost, i.e., the message is removed from the channel because of the channel capacity or because of the adversary.

  Definition RchangeTag : relation Message := fun m1 m2 =>
    (m1 == m2 ) \/ (status m1 = pending /\
                          (status m2 = rejected \/ status m2 = lost ) /\
                          destination m1 == destination m2 /\
                          contents m1 == contents m2 ).

  Instance RchangeTag_compat:
    Proper fequiv RchangeTag.

RchangeTag remains true on sublists of the same size

  Lemma RchangeTag_app:
    forall l1 l2 l1' l2', length l1' = length l1 ->
      eqlistA RchangeTag (l1 ++ l2) (l1' ++ l2')
        <->
      eqlistA RchangeTag l1 l1' /\ eqlistA RchangeTag l2 l2'.

RchangeTag does not modify the length of the list

  Lemma RchangeTag_length:
    forall l l', eqlistA RchangeTag l l' ->
      length l = length l'.

RchangeTag does not modify the destination of a message

  Lemma RchangeTag_destination_one (dest: Node * InChannel):
    forall m m', RchangeTag m m' ->
    destination m == dest <-> destination m' == dest.

RchangeTag does not modify the destination of the messages

  Lemma RchangeTag_destination_list (dest: Node * InChannel):
    forall l l', eqlistA RchangeTag l l'
      ->
    forall msgId,
      PoptionA (fun m => destination m == dest) (nth_error l msgId)
        <->
      PoptionA (fun m => destination m == dest) (nth_error l' msgId).

RchangeTag does not make decrease the number of rejected messages

  Lemma RchangeTag_rejected (l l': list Message) (dest: Node * InChannel):
    eqlistA RchangeTag l l' ->
        count_tag l' dest rejected_wt >= count_tag l dest rejected_wt.

RchangeTag does not make increase the number of pending messages

  Lemma RchangeTag_pending (l l': list Message) (dest: Node * InChannel):
    eqlistA RchangeTag l l' ->
        count_tag l' dest pending_wt <= count_tag l dest pending_wt.

RchangeTag decreases the number of pending messages if a pending message with the studied destination is lost or rejected

  Lemma RchangeTag_pending_decr (l l': list Message) (dest: Node * InChannel):
    eqlistA RchangeTag l l' ->
    forall msgId,
      PoptionA (fun m => destination m == dest /\ status m = pending) (nth_error l msgId)
        ->
      PoptionA (fun m => ~ status m = pending) (nth_error l' msgId)
        ->
      count_tag l' dest pending_wt < count_tag l dest pending_wt.

if not all pending messages are rejected by RchangeTag, then there exists some non-rejected message after RchangeTag has been applied

  Lemma RchangeTag_rejected_few (l l': list Message) (dest: Node * InChannel):
    eqlistA RchangeTag l l' ->
    count_tag l' dest rejected_wt < count_tag l dest pending_wt ->
      exists msgId : nat ,
        PoptionA (fun m => destination m == dest /\ ~ status m = rejected) (nth_error l' msgId).

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

parameters The function is compatible.

  Definition RUN (p:Env *Event) :=
    update_env (fst p) (snd p)
               (run
                  (Node_env (fst p) (active_node (snd p)))
                  (read_mesg (fst p) (snd p))).

  Instance RUN_compat:
    Proper fequiv RUN.

RUN does not modify the destination of any message

  Lemma RUN_destination (dest : Node * InChannel) (msgId : nat):
    forall p : Env * Event,
      PoptionA (fun m => destination m == dest) (getMessage (fst p) msgId)
        ->
      PoptionA (fun m => destination m == dest) (getMessage (RUN p) msgId).

Steps of the algorithm

A step corresponds to the legal application of an event to an environment, i.e.,

the received message, if it exists, is a valid message for the active node
the new environment simply corresponds to the application of the algorithm triggered by the event (snd p1) on the environment (fst p1), with possibly some pending messages being lost or rejected.

This relation

is compatible

NB: step from p1 to p2

  Record Step
         (p2:Env *Event)
         (p1:Env *Event): Prop :=
    {
      Step_proper_r:> Proper pequiv p1;
      Step_proper_l: Proper pequiv p2;

The message ID in the event (snd p1) either does not correspond to a message, or it does correpond to a message actually in the channel (pending), intended to the target specified in (snd p1), and coming from a valid channel.

      h_msg_select:
        match getMessage (fst p1) (recv_id (snd p1)) with
        | None => True
        | Some message =>
          status message = pending
          /\
          fst (destination message) == (active_node (snd p1))
          /\
          is_valid_dest (destination message)
        end;

The only difference between (RUN p1) and the new environment (fst p2) is that some pending messages may have been lost or rejected.

      h_change_tag: (Node_env (RUN p1) =~= Node_env (fst p2)) /\
          eqlistA RchangeTag (Channel_env (RUN p1)) (Channel_env (fst p2));
   }.

  Lemma eqlistA_rel (A: Type) (SA: Setoid A) (rel : relation A) (rel_compat : Proper fequiv rel)
    (l1 l1' l2 l2': list A) :
        eqlistA equiv l1 l1' -> eqlistA equiv l2 l2' -> eqlistA rel l1 l2 -> eqlistA rel l1' l2'.

  Global Instance Step_compat:
    Proper fequiv Step.

Since messages are never removed from the environment, the list lenght cannot decrease

  Lemma Step_length:
    forall p1 p2 : Env * Event, Step p2 p1 ->
      length (Channel_env (fst p1)) <= length (Channel_env (fst p2)).

A simple consequence of the lemma Step_length using getMessage

  Lemma Step_none:
    forall (p1 p2 : Env * Event) (msgId: nat), Step p2 p1 ->
      None = getMessage (fst p2) msgId
        ->
      None = getMessage (fst p1) msgId.

The destination of an existing message is nod modified through a step

  Lemma Step_destination (dest : Node * InChannel) (msgId : nat):
    forall p1 p2 : Env * Event, Step p2 p1 ->
      PoptionA (fun m => destination m == dest) (getMessage (fst p1) msgId)
        ->
      PoptionA (fun m => destination m == dest) (getMessage (fst p2) msgId).

Conservation of the status and the destination through a step under a certain condition

  Lemma Step_destination_pending (dest : Node * InChannel) (msgId : nat):
    forall p1 p2 : Env * Event, Step p2 p1 ->
      PoptionA (fun m => destination m == dest /\ status m = pending) (getMessage (fst p1) msgId)
        ->
      ~ PoptionA (fun m => ~ status m = pending) (getMessage (fst p2) msgId)
        ->
      PoptionA (fun m => destination m == dest /\ status m = pending) (getMessage (fst p2) msgId).

  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 (Node_env env n)).

    Instance getVarPart_compat: Proper fequiv getVarPart.

The stable part of the state indeed remains stable through RUN

    Lemma Stable_Variable_RUN:
      forall (p: Env *Event) (n: Node), Proper pequiv p ->
          getVar (Node_env (RUN p) n) =~= getVar (Node_env (fst p) n).

The stable part of the state indeed remains stable through a step

    Lemma Stable_Variable_step:
      forall (p' p: Env *Event),
        Step p' p -> getVarPart (fst p') =~= getVarPart (fst p).

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 (Node_env env n));
        Assume := (fun env: Env => Assume_RO (ROEnv_part env));
      }.

    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)).

  End with_Stable_Var.

End RelModelMP.

Close Scope signature_scope.
Unset Implicit Arguments.