PADEC - Coq Library

Library Padec.MessagePassing.ExecMP

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2019

Global Imports

From Coq Require Import Lia.
From Coq Require Import PeanoNat.
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 AlgorithmMP.
From Padec Require Import RelModelMP.

Open Scope signature_scope.
Set Implicit Arguments.

Section Exec.

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

Execution

An execution describes an infinite sequence of steps of the algorithm.

Type Exec:

An Exec is an infinite list of interleaved Env and Event. More precisely, an Exec is an infinite list of pairs (Env, Event), where the Event in the pair is the event occuring from the Env.

Definition Exec: Type := Stream (Env *Event).

Under the FIFO hypothesis, a received message from an incoming channel must be the oldest pending message of this particular channel.

  Definition h_fifo_step (g:Env) (ev:Event) :=
    match getMessage g (recv_id ev) with
    | None => True
    | Some message =>
      Forall (fun m => ~(status m = pending /\
                         destination m == destination message))
             (firstn (recv_id ev) (Channel_env g))
    end.
  Definition h_fifo_exec (exec : Exec) :=
    ForAll (fun e => h_fifo_step (fst (hd e)) (snd (hd e))) exec.

If channels have unbounded capacity, then no messages are rejected.

  Definition h_non_bounded_step (env : Env) :=
    Forall (fun m => ~(status m = rejected )) (Channel_env env).
  Definition h_non_bounded_exec (exec : Exec) :=
    ForAll (fun e => h_non_bounded_step (fst (hd e))) exec.

Messages are rejected before they are potentially lost, i.e., ((RUN p1) -> g2, Pending -> Rejected) = (RUN p1,Pending) - capa

  Definition h_bounded_init (capa : nat) (g1 : Env) :=
    forall dest, count_tag (Channel_env g1) dest pending_wt <= capa.
  Definition h_bounded_step (capa : nat) (gg : Env) (g2 : Env) :=
    forall dest, count_tag (Channel_env g2) dest rejected_wt
               - count_tag (Channel_env gg) dest rejected_wt
                 =
                 count_tag (Channel_env gg) dest pending_wt
               - capa.
  Definition h_bounded_exec (capa : nat) (exec : Exec) :=
    ForAll (fun e => h_bounded_init capa (fst (hd e)) /\
              h_bounded_step capa (RUN (hd e)) (fst (hd (tl e)))) exec.

Process fairness: Every node is activated infinitely often.

  Definition ProcessFairness (exec: Exec): Prop :=
    forall n, ForAll (Exists (fun e => active_node (snd (hd e)) == n)) exec.

  Lemma ProcessFairness_always: forall p e, ProcessFairness (Cons p e) -> ProcessFairness e.

Message transmission: Every pending message is eventually lost, rejected, or received.

  Definition MessageTransmission (exec: Exec): Prop :=
    ForAll (fun e =>
              forall msgId, ~(getMessage (fst (hd e)) msgId == None ) ->
                Exists (fun ee =>
                          match getMessage (fst (hd ee)) msgId with
                          | None => False
                          | Some message => ~(status message = pending )
                          end) e
           ) exec.

is_exec: an infinite sequence such that any two consecutive configurations in the sequence actually form a Step of the algorithm

  Definition is_exec (e: Exec) : Prop :=
    ForAll (fun e' => Step (hd (tl e')) (hd e')) e
      /\
    ProcessFairness e.

  Lemma is_exec_cons: forall p e, is_exec (Cons p e) -> is_exec e.

  Lemma is_exec_tl: forall e, is_exec e -> is_exec (tl e).

Under the non-lossy hypothesis, no messages are lost.

  Definition h_non_lossy_step (env : Env) :=
    Forall (fun m => ~(status m = lost )) (Channel_env env).
  Definition h_non_lossy_exec (exec : Exec) :=
    ForAll (fun e => h_non_lossy_step (fst (hd e))) exec.

Fair lossy channels: for every channel, if infinitely many messages are inserted in the channel, then infinitely many messages are received by the destination node of the channel.

The message msgId is sent at the beginning of the execution and is not immediately rejected.

  Definition is_sent (exec: Exec) (dest: Node * InChannel) (msgId:nat) : Prop :=
    let env1 := fst (hd exec) in
      let env2 := fst (hd (tl exec)) in
        getMessage env1 msgId == None
          /\
        PoptionA (fun m => destination m == dest /\ status m <> rejected) (getMessage env2 msgId).

The message msgId has been received.

  Definition is_received (exec: Exec) (dest: Node * InChannel) (msgId:nat) : Prop :=
    (active_node (snd (hd exec)) == fst dest ) /\
    (recv_id (snd (hd exec)) == msgId ) /\
    ~(getMessage (fst (hd exec)) msgId == None ).

For every destination, if infinitely messages are sent and not immediately rejected, then infinitely messages are received.

  Definition FairLossy (exec: Exec): Prop :=
    forall dest,
      (ForAll (Exists (fun e => exists msgId , is_sent e dest msgId)) exec )
        ->
      (ForAll (Exists (fun e => exists msgId , is_received e dest msgId)) exec ).

The message msgId is sent at the beginning of the execution (and might be immediately rejected).

  Definition is_sent' (exec: Exec) (dest: Node * InChannel) (msgId:nat) : Prop :=
    let env1 := fst (hd exec) in
      let env2 := fst (hd (tl exec)) in
        getMessage env1 msgId == None
          /\
        PoptionA (fun m => destination m == dest) (getMessage env2 msgId).

For every destination, if infinitely messages are sent, then infinitely messages are received.

  Definition FairLossy' (exec: Exec): Prop :=
    forall dest,
      (ForAll (Exists (fun e => exists msgId , is_sent' e dest msgId)) exec )
        ->
      (ForAll (Exists (fun e => exists msgId , is_received e dest msgId)) exec ).

  Lemma FairLossy'_tl (e : Exec) :
    FairLossy' e -> FairLossy' (tl e).

Stronger Exists (for the first time)

Inductive FExists (A : Type) (P : Stream A -> Prop) (x : Stream A) : Prop :=
FHere : P x -> FExists P x | FFurther : ~(P x ) -> FExists P (tl x) -> FExists P x.

If the property is always decidable, then Exists implies FEexists.

  Lemma first_exists:
    forall (A : Type) (P : Stream A -> Prop) (x : Stream A),
    (forall (y : Stream A), {P y } + {~(P y )}) -> Exists P x -> FExists P x.

"tl" can be transferred from the second argument of FExists to inside the first

  Lemma tl_FExists_comm:
    forall (A : Type) (P : Stream A -> Prop) (x : Stream A),
          (FExists (fun y : Stream A => P y) (tl x))
            ->
          (FExists (fun y : Stream A => P (tl y)) x ).

Small tool to make "\/" and "Exists" commute

  Lemma exists_or:
    forall (A : Type) (P P' : Stream A -> Prop) (x : Stream A),
      Exists (fun y => P y \/ P' y) x <-> Exists P x \/ Exists P' x.

By definition, is_sent implies is_sent' in all models

  Lemma is_sent_is_sent' :
    forall e dest,
        ForAll (Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent e' dest msgId)) e
          ->
        ForAll (Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent' e' dest msgId)) e.

For unbounded channels, is_sent' implies is_sent (now)

  Lemma is_sent'_is_sent_unbounded_now :
    forall e, h_non_bounded_exec e ->
      forall dest,
        (exists msgId : nat , is_sent' e dest msgId )
          ->
        (exists msgId : nat , is_sent e dest msgId ).

For unbounded channels, is_sent' implies is_sent (eventually)

  Lemma is_sent'_is_sent_unbounded_eventually :
    forall e, h_non_bounded_exec e ->
      forall dest,
        Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent' e' dest msgId) e
          ->
        Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent e' dest msgId) e.

For unbounded channels, is_sent' implies is_sent (always eventually)

  Lemma is_sent'_is_sent_unbounded :
    forall e, h_non_bounded_exec e ->
      forall dest,
        ForAll (Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent' e' dest msgId)) e
          ->
        ForAll (Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent e' dest msgId)) e.

If a pending message becomes non pending during a step, then the number of pending messages in the initial list of messages decreases

  Lemma step_pending_decr (msgId msgId': nat) (l0 l1 l1': list Message) (dest: Node * InChannel):
    l1 = mark_as_read l0 msgId'
      ->
    eqlistA RchangeTag l1 l1'
      ->
    PoptionA (fun m => destination m == dest /\ status m = pending) (nth_error l0 msgId)
      ->
    PoptionA (fun m => ~ status m = pending) (nth_error l1' msgId)
      ->
    count_tag l1' dest pending_wt < count_tag l0 dest pending_wt.

If a pending message becomes non-pending in a step but the total number of pending messages does not decrease, then a message has been sent during the step and is still pending at the end of the step.

  Lemma non_decr_sent (capa_1 : nat) (e: Exec) (dest: Node * InChannel) (msgId: nat):
    is_exec e
      ->
    PoptionA (fun m => destination m == dest /\ status m = pending) (getMessage (fst (hd e)) msgId)
      ->
    PoptionA (fun m => ~ status m = pending) (getMessage (fst (hd (tl e))) msgId)
      ->
    count_tag (Channel_env (fst (hd e))) dest pending_wt
        <= count_tag (Channel_env (fst (hd (tl e)))) dest pending_wt
      ->
    exists msgId', is_sent e dest msgId'.

Under bounded capacity, in any execution and for any dest, there exists a point in time when the channel is not full or a message has just been sent (without being immediately rejected)

  Lemma under_capa (capa_1 : nat) (e: Exec) (dest: Node * InChannel):
    is_exec e -> MessageTransmission e -> h_bounded_exec (S capa_1) e ->
        Exists (fun e' : Exec =>
          count_tag (Channel_env (fst (hd e'))) dest pending_wt < S capa_1
            \/
          exists msgId : nat , is_sent e' dest msgId) e.

Given a destination, it is decidable whether a message has been sent to this destination

  Lemma is_sent'_dec (dest : Node * InChannel) (e : Exec):
    {exists msgId : nat , is_sent' e dest msgId }
       +
    {~ (exists msgId : nat , is_sent' e dest msgId )}.

If not full capacity, next is_sent' implies is_sent

  Lemma is_sent'_is_sent_bounded_now :
    forall capa_1 e, is_exec e -> h_bounded_exec (S capa_1) e ->
      forall dest,
        count_tag (Channel_env (fst (hd e))) dest pending_wt < S capa_1 ->
          (exists msgId : nat , is_sent' e dest msgId )
            ->
          exists msgId : nat , is_sent e dest msgId.

If not full capacity, next is_sent' implies is_sent

  Lemma capacity_not_full_stable :
    forall capa_1 e, is_exec e -> h_bounded_exec (S capa_1) e ->
      forall dest,
        count_tag (Channel_env (fst (hd e))) dest pending_wt < S capa_1 ->
          ~ (exists msgId : nat , is_sent' e dest msgId )
            ->
          count_tag (Channel_env (fst (hd (tl e)))) dest pending_wt < S capa_1.

If not full capacity, next is_sent' implies is_sent

  Lemma is_sent'_is_sent_bounded_exists :
    forall capa_1 e, is_exec e -> h_bounded_exec (S capa_1) e ->
      forall dest,
        count_tag (Channel_env (fst (hd e))) dest pending_wt < S capa_1 ->
          Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent' e' dest msgId) e
            ->
          Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent e' dest msgId) e.

Under bounded capacity, is_sent' implies is_sent

  Lemma is_sent'_is_sent_bounded :
    forall capa_1 e, is_exec e -> MessageTransmission e -> h_bounded_exec (S capa_1) e ->
      forall dest,
        ForAll (Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent' e' dest msgId)) e
          ->
        ForAll (Exists (fun e' : Stream (Env * Event) => exists msgId : nat , is_sent e' dest msgId)) e.

  Lemma fairlossy'_equiv :
    forall capa_1 e, is_exec e -> MessageTransmission e -> (h_bounded_exec (S capa_1) e \/ h_non_bounded_exec e ) ->
      FairLossy e <-> FairLossy' e.

End Exec.

Close Scope signature_scope.
Unset Implicit Arguments.