PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Model.Composition

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Relations.
From Coq Require Import RelationPairs.
From Coq Require Import Bool.
From Coq Require Import Wellfounded.

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import ListUtils.
From Padec Require Import OptionUtil.
From Padec Require Import WellfoundedUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Self_Stabilization.
From Padec Require Import Stream.
From Padec Require Import Simulation.
From Padec Require Import Exec.
From Padec Require Import Fairness.

Open Scope signature_scope.
Set Implicit Arguments.

Section Composition.

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

Algorithm 1

Definitions and Notations.
  Variable (Algo1: Algorithm).
  Notation S1 := (@State Chans Algo1).
  Notation Env1:= (Env (Algo := Algo1)).
  Notation Exec1 := (Exec (Algo:=Algo1)).

  Variable Assumption1: Stable_Assumption (Algo := Algo1).
  Notation Assume1 := (Assume (Stable_Assumption := Assumption1)).
  Notation Assume1_RO := (Assume_RO (Stable_Assumption := Assumption1)).
  Instance Assume1_RO_compat: Proper fequiv Assume1_RO
    := (Assume_RO_compat (Stable_Assumption := Assumption1)).
  Notation RO1 := (ROType (Stable_Assumption := Assumption1)).
  Notation RO1_part := (getRO (Stable_Assumption := Assumption1)).

  Instance RO1_Stable: Stable_Variable Algo1 RO1_part
    := (ROstable (Stable_Assumption := Assumption1)).
  Instance RO1_part_compat: Proper fequiv RO1_part
    := (GetVar_compat (Stable_Variable := RO1_Stable)).
  Instance RO1_Psetoid: PartialSetoid RO1
    := (VarType_setoid (Stable_Variable := RO1_Stable)).
  Notation RO1_part_stable := (GetVar_stable (Stable_Variable := RO1_Stable)).

Algorithm 2

Definitions and Notations.
  Variable (Algo2: Algorithm).
  Notation S2 := (@State Chans Algo2).
  Notation Env2:= (Env (Algo := Algo2)).
  Notation Exec2 := (Exec (Algo:=Algo2)).

  Variable Assumption2: Stable_Assumption (Algo := Algo2).
  Notation Assume2 := (Assume (Stable_Assumption := Assumption2)).
  Notation Assume2_RO := (Assume_RO (Stable_Assumption := Assumption2)).
  Instance Assume2_RO_compat: Proper fequiv Assume2_RO
    := (Assume_RO_compat (Stable_Assumption := Assumption2)).
  Notation RO2 := (ROType (Stable_Assumption := Assumption2)).
  Notation RO2_part := (getRO (Stable_Assumption := Assumption2)).

  Instance RO2_Stable: Stable_Variable Algo2 RO2_part
    := (ROstable (Stable_Assumption := Assumption2)).
  Instance RO2_part_compat: Proper fequiv RO2_part
    := (GetVar_compat (Stable_Variable := RO2_Stable)).
  Instance RO2_Psetoid: PartialSetoid RO2
    := (VarType_setoid (Stable_Variable := RO2_Stable)).
  Notation RO2_part_stable := (GetVar_stable (Stable_Variable := RO2_Stable)).

Algorithm 3 (Composite Algorithm)

Definitions and Notations.
We build the third algorithm as the composition of Algo1 and Algo2 as follows.
S3 is the state type for Algo3.

  Class Composition_State: Type:=
    {
      S3: Type;
      setoid:> Setoid S3;
      S3_dec: Decider (equiv (A:=S3));

      read1: S3 -> S1;
      write1: S3 -> S1 -> S3;
      read2: S3 -> S2;
      write2: S3 -> S2 -> S3;

      read1_compat: Proper fequiv read1;
      write1_compat: Proper fequiv write1;
      read2_compat: Proper fequiv read2;
      write2_compat: Proper fequiv write2;

      
Guarantees that write1 actually writes the S1 part of the state, since the projection of the modified state on the result allows to get back what was written. (same for S2)
      stabRW1: forall (s1: S1) (s3: S3), read1 (write1 s3 s1) == s1;
      stabRW2: forall (s2: S2) (s3: S3), read2 (write2 s3 s2) == s2;

      
Apart from the read-only part of S2, write2 cannot modified the S1 part of the state. The idea behind this constraint is that Algo2 cannot modify the (S2-writtable part of the) data computed by Algo1. (Algo2 cannot either modify the (S2-read-only part) because it is read-only).
      stabRO12: forall (s2: S2) (s3: S3),
          RO2_part s2 =~= RO2_part (read2 s3)
          -> read1 (write2 s3 s2) == read1 s3
    }.

  Context `{CS: Composition_State}.


projection on S1 of a configuration
  Notation lenv1 := (fun sn: Channel -> option S3 =>
                       (fun c => option_map read1 (sn c))).

projection on S2 of a configuration
  Notation lenv2 := (fun sn: Channel -> option S3 =>
                       (fun c => option_map read2 (sn c))).

  Instance lenv1_compat: Proper fequiv lenv1.

  Instance lenv2_compat: Proper fequiv lenv2.

RUN function of Algo3

Now, Algo3 is the hierarchical composition of Algo1 and Algo2: for any node, p, it is enabled either if Algo1 or Algo2 is enabled The function run on p returns
Namely, at each process, Algo1 has priority over Algo2.
  Definition composition_run (s: S3) (sn: Channel -> option S3):
    S3 :=
    if State_dec (run (read1 s) (lenv1 sn)) (read1 s)
    then
      if State_dec (run (read2 s) (lenv2 sn)) (read2 s)
      then s
      else write2 s (run (read2 s) (lenv2 sn))
    else write1 s (run (read1 s) (lenv1 sn)).

  Instance composition_run_compat: Proper fequiv composition_run.

Definition of Algo3

Definition of read-only variables and Assumption
  Instance Collateral_composition: Algorithm :=
    {| State_dec := S3_dec; run_compat := composition_run_compat |}.

  Notation Algo3 := Collateral_composition.
  Notation Env3 := (Env (Algo := Algo3)).
  Notation Exec3 := (Exec (Algo:=Algo3)).

The read-only part of Algo3 is made of the read-only variables of Algo1
  Let RO3 := RO1.
  Instance RO3_Psetoid: PartialSetoid RO3 := RO1_Psetoid.
  Notation RO3_part := (fun s: S3 => RO1_part (read1 s)).
  Instance RO3_part_compat: Proper fequiv RO3_part.

  Lemma RO3_part_stable: forall s sn,
      RO3_part (run s sn) =~= RO3_part s.

  Instance RO3_Stable: Stable_Variable Algo3 RO3_part.

The read-only Assumption for Algo3 is given by the read-only assumption of Algo1
  Definition Assume3_RO: (Node -> RO3) -> Prop :=
    (fun r => Assume1_RO (fun n => (r n))).

  Instance Assume3_RO_compat: Proper fequiv Assume3_RO.

  Instance Assumption3: Stable_Assumption (Algo := Algo3).

  Notation Assume3 := (Assume (Stable_Assumption := Assumption3)).

Projections from 3 to 1

  Definition envread1 (g: Env3): Env1 := fun n => read1 (g n).

  Lemma envread1_compat: Proper fequiv envread1.

  Lemma envread1_prop:
    forall g1 g2 n, g1 =~= g2 ->
                    (local_env (envread1 g1) n)
                      =~=
                      fun c => option_map read1 (local_env g2 n c) .

  Lemma Assume_31:
    forall g, Proper pequiv g ->
              (Assume3 g <-> Assume1 (envread1 g)).

Projections from 3 to 2

  Definition envread2 (g: Env3): Env2 := fun n => read2 (g n).

  Lemma envread2_compat: Proper fequiv envread2.

  Lemma envread2_prop:
    forall g1 g2 n, g1 =~= g2 ->
                    (local_env (envread2 g1) n)
                      =~=
                      fun c => option_map read2 (local_env g2 n c) .

Technical Tools about RUN for Algo1, Algo2 and Algo3


  Lemma run1_rewrite:
    forall g g': Env3,
      g =~= g' ->
      forall n n', n == n' ->
                   run (read1 (g n)) (lenv1 (local_env g n))
                   == RUN (envread1 g') n'.

  Lemma run2_rewrite:
    forall g g': Env3,
      g =~= g' -> forall n n', n == n' ->
                               run (read2 (g n)) (lenv2 (local_env g n))
                               == RUN (envread2 g') n'.

Alternative definition for RUN3
  Definition composition_RUN_alt_def (g: Env3) (n: Node): S3 :=
    if enabled_b (envread1 g) n then
      write1 (g n) (RUN (envread1 g) n)
    else if enabled_b (envread2 g) n then
           write2 (g n) (RUN (envread2 g) n)
         else (g n).

  Lemma composition_RUN_alt:
    fequiv RUN composition_RUN_alt_def.

  Lemma RUN_31_enabled:
    forall (g: Env3) (n: Node),
      Proper fequiv g ->
      enabled_b (envread1 g) n = true ->
      read1 (RUN g n) == (RUN (envread1 g) n).

  Lemma RUN_31_disabled:
    forall (g: Env3) (n: Node),
      Proper fequiv g ->
      enabled_b (envread1 g) n = false ->
      read1 (RUN g n) == (envread1 g) n.

  Lemma RUN_32_enabled:
    forall (g: Env3) (n: Node),
      Proper fequiv g ->
      enabled_b (envread1 g) n = false ->
      enabled_b (envread2 g) n = true ->
      read2 (RUN g n) == (RUN (envread2 g) n).

  Lemma RUN_32_disabled:
    forall (g: Env3) (n: Node),
      Proper fequiv g ->
      enabled_b (envread1 g) n = false ->
      enabled_b (envread2 g) n = false ->
      read2 (RUN g n) == (envread2 g) n.

  Lemma RUN_3_disabled:
    forall (g: Env3) (n: Node),
      Proper fequiv g ->
      enabled_b (envread1 g) n = false ->
      enabled_b (envread2 g) n = false ->
      RUN g n == g n.

Technical Tools about enabled_b for Algo1, Algo2, Algo3

  Lemma enabled_12_3:
    forall g n, Proper pequiv g ->
                (enabled_b g n = true <-> enabled_b (envread1 g) n = true
                                          \/
                                          enabled_b (envread2 g) n = true).

  Lemma enabled_12_3_alt:
    forall g n, Proper pequiv g ->
                enabled_b g n = enabled_b (envread1 g) n
                                || enabled_b (envread2 g) n.

  Lemma enabled_13:
    forall g3 n, Proper fequiv g3 ->
                 enabled_b (envread1 g3) n = true -> enabled_b g3 n = true.

  Lemma enabled_23:
    forall g3 n,
      Proper fequiv g3 ->
      enabled_b (envread2 g3) n = true ->
      enabled_b g3 n = true.

  Lemma enabled_32:
    forall g3 n,
      Proper fequiv g3 ->
      enabled_b (envread1 g3) n = false ->
      enabled_b g3 n = true ->
      enabled_b (envread2 g3) n = true.

  Lemma disabled_12_3:
    forall g n, Proper pequiv g ->
                enabled_b g n = false <-> enabled_b (envread1 g) n = false
                                          /\
                                          enabled_b (envread2 g) n = false.

  Lemma Step_disabled1_unchanged1:
    forall (g' g: Env3), Step g' g ->
                         forall n, enabled_b (envread1 g) n = false ->
                                   read1 (g' n) == read1 (g n).

Technical Tools about has_moved_b for Algo1, Algo2, Algo3

  Lemma has_moved_12_3_all:
    forall g' g n,
      Step g' g ->
      has_moved_b g' g n = true <->
      enabled_b (envread1 g) n = true /\
      has_moved_b (envread1 g') (envread1 g) n = true
      \/
      enabled_b (envread1 g) n = false /\
      has_moved_b (envread1 g') (envread1 g) n = false /\
      enabled_b (envread2 g) n = true /\
      has_moved_b (envread2 g') (envread2 g) n = true.

  Lemma has_moved_12_3_true:
    forall g' g n,
      Step g' g ->
      has_moved_b g' g n = true <->
      has_moved_b (envread1 g') (envread1 g) n = true \/
      has_moved_b (envread2 g') (envread2 g) n = true.

  Lemma has_moved_12_3_true_alt:
    forall g' g n, Step g' g ->
                   has_moved_b g' g n =
                   has_moved_b (envread1 g') (envread1 g) n
                   || has_moved_b (envread2 g') (envread2 g) n.

  Lemma has_moved_12_3_false:
    forall g' g n, Step g' g ->
                   has_moved_b g' g n = false <->
                   has_moved_b (envread1 g') (envread1 g) n = false
                   /\ has_moved_b (envread2 g') (envread2 g) n = false.

  Lemma has_moved_13:
    forall g3' g3 n,
      has_moved_b (envread1 g3') (envread1 g3) n = true ->
      has_moved_b g3' g3 n = true.

  Lemma has_moved_31:
    forall g3' g3 n,
      Step g3' g3 ->
      enabled_b (envread1 g3) n = true ->
      has_moved_b g3' g3 n = true ->
      has_moved_b (envread1 g3') (envread1 g3) n = true.

  Lemma has_moved_23:
    forall g3' g3 n,
      has_moved_b (envread2 g3') (envread2 g3) n = true ->
      has_moved_b g3' g3 n = true.

  Lemma has_moved_32:
    forall g3' g3 n,
      Step g3' g3 ->
      enabled_b (envread1 g3) n = false ->
      has_moved_b g3' g3 n = true ->
      has_moved_b (envread2 g3') (envread2 g3) n = true.

Projection of an execution from Algo3 to Algo1

  CoFixpoint execread1 (e3: Exec3): Exec1 :=
    match e3 with
    | s_one g3 => s_one (envread1 g3)
    | s_cons g3 e3' => s_cons (envread1 g3) (execread1 e3')
    end.


  Lemma execread1_unfold:
    forall e3,
      execread1 e3 =
      match e3 with
      | s_one g3 => s_one (envread1 g3)
      | s_cons g3 e3' => s_cons (envread1 g3) (execread1 e3')
      end.

  Lemma execread1_fold_cons:
    forall g3 e3, execread1 (s_cons g3 e3) =
                  (s_cons (envread1 g3) (execread1 e3)).

  Lemma execread1_fold_one:
    forall g3, execread1 (s_one g3) = (s_one (envread1 g3)).

  Instance execread1_compat: Proper fequiv execread1.

  Lemma s_hd_read1: forall e3,
      envread1 (s_hd e3) = s_hd (execread1 e3).

Projection of an execution from Algo3 to Algo2

  CoFixpoint execread2 (e3: Exec3): Exec2 :=
    match e3 with
    | s_one g3 => s_one (envread2 g3)
    | s_cons g3 e3' => s_cons (envread2 g3) (execread2 e3')
    end.


  Lemma execread2_unfold:
    forall e3,
      execread2 e3 =
      match e3 with
      | s_one g3 => s_one (envread2 g3)
      | s_cons g3 e3' => s_cons (envread2 g3) (execread2 e3')
      end.

  Lemma execread2_fold_cons:
    forall g3 e3, execread2 (s_cons g3 e3) =
                  (s_cons (envread2 g3) (execread2 e3)).

  Lemma execread2_fold_one:
    forall g3, execread2 (s_one g3) = (s_one (envread2 g3)).

  Instance execread2_compat: Proper fequiv execread2.

  Lemma s_hd_read2: forall e3,
      envread2 (s_hd e3) = s_hd (execread2 e3).

Terminal Configurations:

A configuration is terminal for Algo3 iff its projections on Algo1 and Algo2 are also terminal.
  Lemma terminal_31:
    forall (g: Env3), terminal g -> terminal (envread1 g).

  Lemma terminal_32:
    forall (g: Env3), terminal g -> terminal (envread2 g).

  Lemma terminal_12_3:
    forall g, Proper fequiv g ->
              terminal (envread1 g) /\ terminal (envread2 g) ->
              terminal g.

Once Algo1 has reached a terminal configuration, it remains in the same terminal configuration
  Lemma terminal1_continued':
    forall g' g,
      Step g' g -> terminal (envread1 g) -> envread1 g =~= envread1 g'.

  Lemma terminal1_continued:
    forall g' g,
      Step g' g ->
      terminal (envread1 g) -> terminal (envread1 g').

  Lemma terminal1_continued'_bis_:
    forall e3 g1,
      is_exec e3 -> terminal (envread1 (s_hd e3)) ->
      g1 =~= envread1 (s_hd e3) ->
      Always (fun e => s_hd e =~= g1) (execread1 e3).

  Lemma terminal1_continued'_bis:
    forall e3,
      is_exec e3 -> terminal (envread1 (s_hd e3)) ->
      Always (fun e => s_hd e =~= envread1 (s_hd e3)) (execread1 e3).

  Lemma terminal1_continued_bis:
    forall e3,
      is_exec e3 -> terminal (envread1 (s_hd e3)) ->
      Always (fun e => terminal (envread1 (s_hd e))) e3.

  Lemma terminal1_continued_bis'':
    forall e3,
      is_exec e3 ->
      Eventually (fun e => terminal (envread1 (s_hd e))) e3 ->
      Eventually (Always (fun e => terminal (envread1 (s_hd e)))) e3.

Technical Tools about EN, AN, NEUT for Algo1, Algo2, Algo3


  Lemma EN_1_3: forall e3 n,
      Proper fequiv (s_hd e3) ->
      EN n (execread1 e3) ->
      EN n e3.

  Lemma EN_2_3: forall e3 n,
      Proper fequiv (s_hd e3) ->
      EN n (execread2 e3) ->
      EN n e3.

  Lemma ACT_1_3: forall g3 e3 n,
      Step (s_hd e3) g3 ->
      ACT n (execread1 (s_cons g3 e3)) ->
      ACT n (s_cons g3 e3).

  Lemma ACT_3_1:
    forall g e n,
      Step (s_hd e) g ->
      EN n (execread1 (s_cons g e)) ->
      ACT n (s_cons g e) ->
      ACT n (execread1 (s_cons g e)).

  Lemma NEUT_3_1':
    forall g e n,
      Step (s_hd e) g ->
      EN n (execread1 (s_cons g e)) ->
      NEUT n (s_cons g e) ->
      NEUT n (execread1 (s_cons g e)).

  Lemma NEUT_3_1:
    forall e n,
      is_exec e ->
      EN n (execread1 e) ->
      NEUT n e ->
      NEUT n (execread1 e).

  Lemma EN_AN_1_3:
    forall e n,
      is_exec e ->
      EN n (execread1 e) -> AN n e ->
      AN n (execread1 e).

  Lemma E_AN_3_1:
    forall e3 n,
      is_exec e3 ->
      EN n (execread1 e3) ->
      Eventually (AN n) e3 ->
      Eventually (AN n) (execread1 e3).

  Lemma ACT_3_2:
    forall e n, is_exec e ->
                enabled_b (envread1 (s_hd e)) n = false ->
                ACT n e ->
                ACT n (execread2 e).

  Lemma NEUT_3_2:
    forall e n, is_exec e -> terminal (envread1 (s_hd e)) ->
                NEUT n e ->
                NEUT n (execread2 e).

  Lemma term_EN_AN_3_2:
    forall e n, is_exec e ->
                terminal (envread1 (s_hd e)) ->
                EN n (execread2 e) ->
                AN n e ->
                AN n (execread2 e).

  Lemma E_AN_3_2:
    forall e3 n,
      is_exec e3 ->
      terminal (envread1 (s_hd e3)) ->
      EN n (execread2 e3) ->
      Eventually (AN n) e3 ->
      Eventually (AN n) (execread2 e3).

Once Algo1 has reached a terminal configuration, the

projection of an execution on Algo2 is actually an execution of Algo2.
  Lemma Step_32:
    forall g' g,
      Step g' g ->
      (forall n, enabled_b (envread1 g) n = false \/
                 has_moved_b g' g n = false) ->
      Step (envread2 g') (envread2 g).

  Lemma is_exec_3_2:
    forall e3, is_exec e3 -> terminal (envread1 (s_hd e3)) ->
               is_exec (execread2 e3).

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

Checking the Specication of Algo3

  Section Spec_OK.

Algo1 is silent, hence its spec can be reduced to a predicate SPEC1 on Env1
    Variable (SPEC1: Env1 -> Prop)
             (P_correct1: P_correctness Assumption1 SPEC1).

Algo2 is self-stabilizing for its specification SPEC2, under the daemon LS2, with legitimate states LS2
    Variable (SPEC2: Exec2 -> Prop)
             (LS2: Env2 -> Prop)
             (DF2: Exec2 -> Prop)
             (spec_ok2: spec_ok Assumption2 DF2 LS2 SPEC2).

Assumption between 1 and 2: once Algo1 has stabilized into SPEC1, Assume2 should hold.
    Variable (SPEC1_Assume2:
                forall (g: Env3),
                  Proper fequiv g -> Assume3 g -> SPEC1 (envread1 g) ->
                  Assume2 (envread2 g)).

Algo3: an execution meets the specification for Algo3, SPEC3, if its projection on Algo2 meets SPEC2 and if it verifies SPEC1 on each of its configurations.
    Definition Compo_SPEC SPEC_env1 SPEC2 :=
      fun e => Always (fun ex => SPEC_env1 (envread1 (s_hd ex))) e /\
               SPEC2 (execread2 e).
    Notation SPEC3 := (Compo_SPEC SPEC1 SPEC2).

    Notation LS3 := (fun g3 => terminal (envread1 g3) /\ LS2 (envread2 g3)).

    Theorem composition_spec_ok:
      forall DF3: Exec3 -> Prop,
        (forall e, is_exec e -> DF3 e ->
                   terminal (s_hd (execread1 e))->
                   DF2 (execread2 e)) ->
        spec_ok Assumption3 DF3 LS3 SPEC3.

  End Spec_OK.

Checking the Partial Correctness of Algo3 in case Algo2 is

silent
  Section Partial_Correctness.

Algo1 is silent, hence its spec can be reduced to a predicate SPEC1 on Env1
    Variable (SPEC1: Env1 -> Prop)
             (P_correct1: P_correctness Assumption1 SPEC1).

Assumption between 1 and 2: once Algo1 has stabilized into SPEC1, Assume2 should hold.
    Variable (SPEC1_Assume2:
                forall (g: Env3),
                  Proper fequiv g -> Assume3 g -> SPEC1 (envread1 g) ->
                  Assume2 (envread2 g)).

Algo2 is silent:
    Variable (SPEC2: Env2 -> Prop)
             (P_correct2: P_correctness Assumption2 SPEC2).

Algo3
    Notation SPEC3 := (fun g => SPEC1 (envread1 g) /\
                                SPEC2 (envread2 g)).

    Theorem composition_P_correctness:
      P_correctness Assumption3 SPEC3.

  End Partial_Correctness.

Checking the Closure of Algo3

  Section Closure.

Legitimate states for Algo1: terminal states Legitimate states for Algo2:
    Variable (LS2: Env2 -> Prop) (LS2_compat: Proper pequiv LS2).

    Notation LS3 := (fun g3 => terminal (envread1 g3) /\ LS2 (envread2 g3)).

Assumption between 1 and 2: once Algo1 has stabilized Assume2 should hold.
    Variable (Term1_Assume2:
                forall (g: Env3),
                  Proper fequiv g -> Assume3 g -> terminal (envread1 g) ->
                  Assume2 (envread2 g)).

Daemon fairness
    Variable (DF2: Exec2 -> Prop) (DF3: Exec3 -> Prop)
             (hDF3: forall e, is_exec e -> DF3 e ->
                              terminal (s_hd (execread1 e))->
                              DF2 (execread2 e)).

    Theorem composition_closure:
      closure Assumption2 DF2 LS2 -> closure Assumption3 DF3 LS3.

  End Closure.

Termination:

Termination of Composition requires additionnal hypothesis.
Discussion from J. Lefrere internship report:
A good argument for additional hypotheses is to prevent the asynchronous daemon from postponing the execution of A1 steps indefinitely. This may be possible if that at some point of the program, there are some rules in A2 that enable divergent behaviors.
Theses two solutions are not comparable, there may be cases where will be applicable and not the other.

Termination: Case A

  Section A.


    Variable (Hterm1: (termination (Algo := Algo1) Assumption1)).
    Variable (Hterm2: forall (g: Env2),
                 Proper fequiv g ->
                 Acc (Step (Algo := Algo2)) g).

    Lemma Hterm2_alt: well_founded (Step (Algo := Algo2)).

****
We show first termination for the lexicographic order: this order is a relation on pairs (Env1, Env2) built by:
****
We show Acc for this order (see Lemma term_lexico_pairs_Acc):

    Lemma term_lexico_pairs:
      forall g, Assume3 g -> Proper fequiv g ->
                Acc (lexico_pairs fequiv (Step (Algo := Algo1))
                                   (Step (Algo := Algo2)))
                     (envread1 g, envread2 g).

****
We then need to show that Step is included into this order in some sense:
See Lemma incl_lexp.
We introduce a Boolean predicate step1_b that allows to decide wether a step from Algo3 is to take into account for Algo1 or for Algo2 (remember that within a step, some nodes may have performed a step from Algo1 while others from Algo2).
The proof of Lemma incl_lexp is divided on two cases. For a step of Algo3 between g and g', we split the proof into the case when (step1_b g' g) is true and the case when it is false.

    Definition step1_b (g' g: Env3): bool :=
      existsb
        (fun (n: Node) =>
           andb (enabled_b (envread1 g) n)
                (has_moved_b g' g n))
        all_nodes.

    Lemma step1_b_true:
      forall g' g, Proper fequiv g -> Proper fequiv g' ->
                   (step1_b g' g = true <->
                    exists n, enabled_b (envread1 g) n = true /\
                              has_moved_b g' g n = true).

    Lemma step1_b_false:
      forall g' g, Proper fequiv g -> Proper fequiv g' ->
                   (step1_b g' g = false <->
                    forall n, enabled_b (envread1 g) n = false \/
                              has_moved_b g' g n = false).

    Lemma Step1_is_Step_Algo1:
      forall g' g, step1_b g' g = true -> Step g' g ->
                   Step (envread1 g') (envread1 g).

    Lemma Step2_is_Step_Algo2:
      forall g' g, step1_b g' g = false -> Step g' g ->
                   Step (envread2 g') (envread2 g).

    Lemma incl_lexico_pairs:
      inclusion (Step (Algo := Algo3))
                (RelCompFun
                   (lexico_pairs fequiv (Step (Algo := Algo1))
                                 (Step (Algo := Algo2)))
                   (fun (g: Env3) => (envread1 g, envread2 g))).

    Theorem termination_A: termination Assumption3.

  End A.


Termination: Case B

  Section B.

Algo1 is silent under weakly fair daemon
    Variable (Hterm1: silence Assumption1 weakly_fair).

Algo2 converges to some legitimate states LS2, under weakly faire daemon
    Variable (LS2: Env2 -> Prop)
             (LS2_compat: Proper pequiv LS2)
             (Conv2: convergence Assumption2 weakly_fair LS2).

Assumption between 1 and 2: once Algo1 has stabilized, Assume2 should hold.
    Variable (assume_32:
                forall g3, Proper fequiv g3 -> Assume3 g3 ->
                           terminal (envread1 g3) ->
                           Assume2 (envread2 g3)).

Legitimate States for Algo3
    Notation LS3 := (fun g3 => terminal (envread1 g3) /\ LS2 (envread2 g3)).

Weakly Fair from 3 to 1

    Lemma WF_exec_3_1:
      forall (e3: Exec3),
        is_exec e3 ->
        weakly_fair e3 ->
        weakly_fair (execread1 e3).

Weakly Fair from 3 to 2

    Lemma WF_exec_3_2:
      forall (e3: Exec3),
        is_exec e3 ->
        terminal (envread1 (s_hd e3)) ->
        weakly_fair e3 ->
        weakly_fair (execread2 e3).

    Section With_Squeeze.

      Lemma move1_en_an_neq:
        forall g3 e3 n,
          Step (s_hd e3) g3 ->
          enabled_b (envread1 g3) n = true ->
          AN n (s_cons g3 e3) ->
          ~ (envread1 g3) =~= (envread1 (s_hd e3)).

      Lemma move1_term_en_neq:
        forall g3' g3 n,
          Step g3' g3 ->
          terminal g3' ->
          enabled_b (envread1 g3) n = true ->
          ~(envread1 g3') =~= (envread1 g3).

      Lemma execread1_all_compat:
        forall e3, is_exec e3 -> Proper pequiv (execread1 e3).

      Lemma non_terminal1_Skippable:
        forall g3 e3, is_exec (s_cons g3 e3) ->
                      weakly_fair (s_cons g3 e3) ->
                      ~ terminal (envread1 g3) ->
                      Skippable (envread1 g3)
                                (s_cons (envread1 g3) (execread1 e3)).

      Lemma exec_can_collapse:
        forall e3, is_exec e3 -> weakly_fair e3 ->
                   Squeezable (execread1 e3).


      Lemma is_constant_terminal:
        forall e3 g1, is_exec e3 -> weakly_fair e3 ->
                      is_constant g1 (execread1 e3) -> terminal g1.

      Lemma Step_31_neq:
        forall g3' g3,
          Step g3' g3 ->
          ~ (envread1 g3') =~= (envread1 g3) ->
          Step (envread1 g3') (envread1 g3).

      Lemma suffix_13:
        forall e1 e3, Proper pequiv e3 -> is_suffix (execread1 e3) e1 ->
                      exists e3', is_suffix e3 e3' /\ (execread1 e3') =~= e1.

      Lemma is_exec_simu':
        forall (e3: Exec3) (e1: Exec1),
          is_exec e3 ->
          Always (fun e =>
                    forall g1, is_constant g1 (execread1 e)
                               -> terminal g1) e3 ->
          Simulation e1 (execread1 e3) ->
          Always moves e1 -> is_exec e1.

      Lemma is_exec_simu:
        forall (e3: Exec3) (e1: Exec1),
          is_exec e3 -> weakly_fair e3 ->
          Simulation e1 (execread1 e3) -> Always moves e1 ->
          is_exec e1.


      Lemma collapse_is_exec:
        forall e3 (ise: is_exec e3) (wf: weakly_fair e3),
          is_exec (@Squeeze
                     _ _ Env_dec
                     _ (execread1_all_compat ise)
                     (exec_can_collapse ise wf)).

      Lemma weakly_fair_monotonic:
        Simulation_monotonic (A := Env1) weakly_fair.

      Lemma weakly_fair_simu:
        forall (e3: Exec3) (e1: Exec1),
          is_exec e3 -> weakly_fair e3 ->
          Simulation e1 (execread1 e3) ->
          weakly_fair e1.

      Lemma collapse_weakly_fair:
        forall e3 (ise: is_exec e3) (wf: weakly_fair e3),
          weakly_fair (@Squeeze
                         _ _ Env_dec _
                         (execread1_all_compat ise)
                         (exec_can_collapse ise wf)).

    End With_Squeeze.

    Lemma E_term1:
      forall e3,
        Assume3 (s_hd e3) -> is_exec e3 -> weakly_fair e3 ->
        Eventually (fun e => terminal (envread1 (s_hd e))) e3.

    Lemma assume_suffix:
      forall e, Assume3 (s_hd e) -> is_exec e ->
                forall e_suf, is_suffix e e_suf -> Assume3 (s_hd e_suf).

    Theorem composition_convergence: convergence Assumption3 weakly_fair LS3.
  End B.

  Section Results.

    Theorem Compo_B_Self_Stab (SPEC_env1: Env1 -> Prop) SPEC2:
      (forall g, Proper fequiv g -> SPEC_env1 (envread1 g) ->
                 Assume2 (envread2 g)) ->
      silence Assumption1 weakly_fair ->
      self_stabilization Assumption1 weakly_fair (only_one SPEC_env1) ->
      self_stabilization Assumption2 weakly_fair SPEC2 ->
      self_stabilization Assumption3 weakly_fair (Compo_SPEC SPEC_env1 SPEC2).

    Theorem Compo_Silent_Silent_B_Silent:
      (forall g, Proper fequiv g ->
                 Assume3 g -> terminal (envread1 g) ->
                 Assume2 (envread2 g)) ->
      silence Assumption1 weakly_fair ->
      silence Assumption2 weakly_fair ->
      silence Assumption3 weakly_fair.

  End Results.

End Composition.

Close Scope signature_scope.
Unset Implicit Arguments.