PADEC - Coq Library

Library Padec.MessagePassing.FairLossyTest

A Framework for Certified Self-Stabilization
PADEC Coq Library

June 2019

Global imports

From Coq Require Import PeanoNat.
From Coq Require Import Arith.
From Coq Require Import NArith.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import RelationPairs.
From Coq Require Import Morphisms.
From Coq Require Import List.
From Coq Require Import Lia.
From Coq Require Import Streams.

Local imports

From Padec Require Import NatUtils.
From Padec Require Import AlgorithmMP.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import RelModelMP.
From Padec Require Import Self_StabilizationMP.
From Padec Require Import FairnessMP.
From Padec Require Import ExecMP.
From Padec Require Import Fair_convergence.

Open Scope signature_scope.
Set Implicit Arguments.

Until: P P P P Q ...

  Inductive Until (A : Type) (P Q: Stream A -> Prop) (x : Stream A) : Prop :=
  | until_now: Q x -> Until P Q x
  | until_later: P x -> Until P Q (tl x) -> Until P Q x.

Weak Until: P P P P Q ... or P P P P P P ...

  CoInductive WUntil (A : Type) (P Q: Stream A -> Prop) (x : Stream A) : Prop :=
  | wuntil_now: Q x -> WUntil P Q x
  | wuntil_later: P x -> WUntil P Q (tl x) -> WUntil P Q x.

First Weak Until Included:

  Definition FWUntilI (A : Type) (P Q: Stream A -> Prop) (x : Stream A) : Prop :=
    WUntil (fun e => (P e /\ ~Q e))
           (fun e => (P e /\ Q e)) x.

  Lemma temporal_prop1 (A : Type) (P Q R: Stream A -> Prop)
          (Q_dec: forall x, {Q x } + {~ Q x }) (x : Stream A):
    FWUntilI P Q x ->
    Exists R x ->
    (Exists Q x ) \/ (Exists (fun x0 => R x0 /\ FWUntilI P Q x0) x ).

  Definition indices_list (A: Type) (P_dec: A -> bool) (l: list A):=
    map_filter (fun n => n) (fold_left
      (fun l' a => if (P_dec a) then (Some (length l'))::l' else None ::l')
      l
      nil).

  Definition indices_list' (A: Type) (P: A -> Prop) (P_dec: forall a, {P a } + {~ P a }) (l: list A):=
    map_filter (fun n => n) (fold_right
      (fun a l' => if (P_dec a) then (Some (minus (length l) (S (length l'))))::l' else None ::l')
      nil
      l).

  Lemma indices_fold_length' (A: Type) (P: A -> Prop) (P_dec: forall a, {P a } + {~ P a }) (l: list A):
    length l = length (fold_right
      (fun a l' => if (P_dec a) then (Some (minus (length l) (S (length l'))))::l' else None ::l')
      nil
      l).

  Lemma correct_indices_list' (A: Type) (P: A -> Prop) (P_dec: forall a, {P a } + {~ P a }) (l: list A):
    forall msgId, In msgId (indices_list' P P_dec l) <-> PoptionA P (nth_error l msgId).

  Lemma map_filter_app:
    forall (A B: Type) (f : A -> option B) (l m : list A),
      map_filter f (l ++ m) = map_filter f l ++ map_filter f m.

Section Tools.

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

  Lemma indices_list_lem (P: Message -> Prop) (P_dec: forall m, {P m } + {~ P m }) (env: Env):
    exists l', forall msgId, In msgId l' <-> PoptionA P (getMessage env msgId).

End Tools.

Section HighLevel.

If a message is sent as long as it is not received, then it will be received.

#[refine] Instance unitIn : InChannels := {| InChannel := unit ; InChannel_setoid := Setoid_unit |}.

#[refine] Instance unitOut : OutChannels := {| OutChannel := unit ; OutChannel_setoid := Setoid_unit |}.

Soit et deux processus reliés par des canaux.

  Program Instance edgeNet : DirNetwork :=
    {| Node_setoid := Setoid_bool;
       Node_dec := Bool.bool_dec;
       inLink := fun p => Some (negb (fst p), tt );
       outLink := fun p => Some (negb (fst p), tt );
       all_nodes := true :: false :: nil
    |}.

  Variables (A: Node).
  Definition B := negb A.

Soit un algorithme distribué pour et .

Context {Algo: MPAlgorithm}.

Si est initialement activé, envoie à uniquement des messages de type .

  Definition only_T_sent T exec :=
    forall msgId, is_sent' exec (B ,tt ) msgId ->
        PoptionA (fun m : Message => contents m == T) (getMessage (fst (hd (tl exec))) msgId).

reçoit intialement un message de type .

  Definition T_recvd T exec:=
    exists msgId ,
      is_received exec (B ,tt ) msgId
        /\
      PoptionA (fun m => contents m == T) (getMessage (fst (hd exec)) msgId).

reçoit une infinité de messages.

Definition recvd exec :=
FExists (fun e => exists msgId : nat , is_received e (B ,tt ) msgId) exec.

Tous les messages initiaux du canal sont de type .

  Definition only_T_channel (T: Msg) (exec: Exec) :=
    forall msgId,
      match getMessage (fst (hd exec)) msgId with
      | None => True
      | Some m => (status m = pending /\ destination m == (B ,tt )) -> contents m == T
      end.

Soit un type de message.

Variable (T: Msg).

Soit reçoit , soit le canal ne contient que du tant que ne reçoit pas de message de type .

  Lemma recvd_or_clean:
    forall exec, is_exec exec ->
      MessageTransmission exec ->
      FWUntilI (only_T_sent T) (T_recvd T) exec ->
        Exists (fun e => T_recvd T e \/ FWUntilI (only_T_channel T) (T_recvd T) e) exec.

Tant que ne reçoit pas de message de type , à chaque activation envoie à uniquement des messages de type et au moins un.

  Lemma clean_implies_recvd:
    forall exec, is_exec exec ->
      ForAll recvd exec ->
      FWUntilI (only_T_channel T) (T_recvd T) exec ->
        Exists (T_recvd T) exec.

Tant que ne reçoit pas de message de type , à chaque activation envoie à uniquement des messages de type et au moins un.

  Lemma ArecvsT:
    forall exec, is_exec exec ->
      MessageTransmission exec ->
      ForAll recvd exec ->
      FWUntilI (only_T_sent T) (T_recvd T) exec ->
        Exists (T_recvd T) exec.

Toute activation de entraîne l'envoi d'exactement un message.

Hypothesis HatLeastOneMsg:
forall env o, exists msg , snd (run (Node_env env A) o) == (tt , msg ) :: nil.

Soit un état possible de . Soit un ensemble de types de messages. Pour toute exécution exec,

Variables (sA: State) (Sbad: Msg -> Prop).

Si , dans l'état , est activé sur timeout ou reçoit un message de type non inclus dans , alors qui exécute reste dans l'état et envoie à uniquement des messages de type et au moins un.

  Hypothesis HAsendT:
    forall exec msgId,
      is_exec exec ->
      Node_env (fst (hd exec)) A == sA ->
      active_node (snd (hd exec)) == A ->
      recv_id (snd (hd exec)) == msgId ->
      ~PoptionA (fun m : Message => Sbad (contents m)) (getMessage (fst (hd exec)) msgId) ->
      (Node_env (fst (hd (tl exec))) A == sA /\ forall dest msgId',
        is_sent' exec dest msgId' ->
          PoptionA (fun m : Message => contents m == T) (getMessage (fst (hd (tl exec))) msgId')).

On suppose que est dans un état tel que, s'il n'est pas activé sur réception d'un message de type , alors qui exécute n'envoie pas à de messages de type inclus dans et reste dans l'état .

Hypothesis HnoBad: True.

Variable (exec: Exec).

est initialement dans l'état .

  Hypothesis HinitStatus:
    Node_env (fst (hd exec)) A == sA.

  Definition cleanChannel env:=
    forall msgId, PoptionA (fun m : Message => status m = pending) (getMessage env msgId) ->
      ~PoptionA (fun m : Message => Sbad (contents m)) (getMessage env msgId).

On suppose que, initialement, le canal ne contient pas de messages de type inclus dans .

Hypothesis HcleanChannel:
cleanChannel (fst (hd exec)).

Alors, au bout d'un temps fini, reçoit un message de type .

Lemma HhighLevel: True.

End HighLevel.

Section Hello.

(Simple) Example

  Existing Instance unitIn.
  Existing Instance unitOut.

  Inductive stateHello : Set :=
    | Init : stateHello
    | Happy : stateHello.

  Instance Setoid_stateHello: Setoid stateHello := {| equiv:=eq |}.

  Inductive MsgHello : Set :=
    | Hello : MsgHello
    | Done : MsgHello.

  Instance Setoid_MsgHello: Setoid MsgHello := {| equiv:=eq |}.

  Program Instance HelloAlg: MPAlgorithm :=
    {|
      State_setoid := Setoid_stateHello;
      Msg_setoid := Setoid_MsgHello;
      run := fun s om => match s with
        | Init => match om with
            | None => (Init , (tt , Hello )::nil )
            | Some (cin,Hello ) => (Happy , (tt , Done )::nil )
            | Some (cin,Done ) => (Init , (tt , Done )::nil )
          end
        | Happy => (Happy , (tt , Done )::nil )
      end;
    |}.

  Existing Instance edgeNet.

  Lemma run_always_sends :
    forall env b o, exists msg , snd (run (Node_env env b) o) = (tt , msg ) :: nil.

  Lemma active_node_sends :
    forall exec, is_exec exec ->
      forall b, active_node (snd (hd exec)) == negb b ->
        exists msgId : nat , is_sent' exec (b , tt ) msgId.

  Lemma FairLossyTest (exec: Exec):
    is_exec exec ->
    forall dest,
      (ForAll (Exists (fun e => exists msgId , is_sent' e dest msgId)) exec).

  Definition emptyChannels (env: Env):=
    forall msgId, getMessage env msgId == None \/
      PoptionA (fun m : Message => status m <> pending) (getMessage env msgId).

  Lemma aFaire:
    forall e,
      { (fun e => exists msgId dest , is_received e dest msgId /\
            PoptionA(fun m => contents m == Hello) (getMessage (fst (hd e)) msgId)) e } +
      {~ (fun e => exists msgId dest , is_received e dest msgId /\
            PoptionA(fun m => contents m == Hello) (getMessage (fst (hd e)) msgId)) e }.

  Lemma aFaire':
    forall (exec: Exec) msgId,
      PoptionA (fun m => contents m == Hello) (getMessage (fst (hd exec)) msgId) ->
      PoptionA (fun m => contents m == Hello) (getMessage (fst (hd (tl exec))) msgId).

  Lemma step0 (exec: Exec):
    is_exec exec ->
    (forall b, Node_env (fst (hd exec)) b = Init ) ->
      WUntil (fun e => (forall b, Node_env (fst (hd e)) b = Init))
             (fun e => (forall b, Node_env (fst (hd e)) b = Init ) /\
              exists msgId dest , is_received e dest msgId /\
                PoptionA(fun m => contents m == Hello) (getMessage (fst (hd e)) msgId)
             ) exec.

  Lemma aFaire2:
    forall exec,
    { exists (msgId : nat) (dest : Node * InChannel ), is_received exec dest msgId } +
    {~ (exists (msgId : nat) (dest : Node * InChannel ), is_received exec dest msgId )}.

  Lemma step1_1 (exec: Exec):
    is_exec exec -> FairLossy' exec ->
      FExists (fun e => exists msgId dest , is_received e dest msgId) exec.

  Lemma step1_2 (exec: Exec):
    is_exec exec ->
    (forall b, Node_env (fst (hd exec)) b = Init ) ->
      WUntil (fun e => ~ (exists msgId dest , is_received e dest msgId /\
                PoptionA(fun m => contents m == Hello) (getMessage (fst (hd (tl e))) msgId)) ->
                (forall msgId dest, is_sent' e dest msgId ->
                  PoptionA(fun m => contents m == Hello) (getMessage (fst (hd (tl e))) msgId))
             )
             (fun e => (forall b, Node_env (fst (hd e)) b = Init ) /\
              exists msgId dest , is_received e dest msgId /\
                PoptionA(fun m => contents m == Hello) (getMessage (fst (hd (tl e))) msgId)
             ) exec.

  Lemma step1 (exec: Exec):
    is_exec exec -> FairLossy' exec ->
    (forall b, Node_env (fst (hd exec)) b = Init ) ->
    (emptyChannels (fst (hd exec))) ->
      FExists (fun e => exists msgId dest , is_received e dest msgId /\
                PoptionA(fun m => contents m == Hello) (getMessage (fst (hd e)) msgId)
              ) exec.

  Lemma step2 (exec: Exec):
    is_exec exec ->
    (forall b, Node_env (fst (hd exec)) b = Init ) ->
    (exists msgId dest , is_received exec dest msgId /\
        PoptionA(fun m => contents m == Hello) (getMessage (fst (hd exec)) msgId)) ->
      exists b , Node_env (fst (hd (tl exec))) b = Happy.

Au bout d'un temps fini, au moins l'un des deux processus passe dans l'état Happy. Tout les processus sont dans l'état Init. Tout les canaux sont vides.

  Lemma EventuallyHappyFromInit (exec: Exec):
    is_exec exec -> FairLossy' exec ->
    (forall b, Node_env (fst (hd exec)) b = Init ) ->
    (emptyChannels (fst (hd exec))) ->
      Exists (fun e => exists b , Node_env (fst (hd e)) b = Happy) exec.

Au bout d'un temps fini, au moins l'un des deux processus passe dans l'état Happy.

  Lemma EventuallyHappy (exec: Exec):
    is_exec exec -> FairLossy' exec ->
    (emptyChannels (fst (hd exec))) ->
    Exists (fun e => exists b , Node_env (fst (hd e)) b = Happy) exec.

End Hello.

Close Scope signature_scope.
Unset Implicit Arguments.