Library RobustReconfiguration


Modelisation of robust reconfiguration protocols

Require Import Common.
Set Implicit Arguments.

Modelisation: architectures, invariants, algorithms


possible states for components

Inductive Status :=
| Started
| Stopped
| Failed.

Section s.

we assume a set of components, a set of import names, and a function indicating which import is mandatory for each component

 Variable Component: FSet.
 Variable Imports: FSet.
 Variable is_mandatory: Component -> Imports -> bool.

 Notation mandatory c i := (is_mandatory c i = true).
 Notation optional c i := (is_mandatory c i = false).

an architecture is represented by:
  • a function associating a status to all components
  • a partial function representing existing wires

 Record arch := mk_arch {
   status: Component -> Status;
   wires: Component * Imports -> option Component
 }.

the empty architecture: no wires, all components stopped

 Definition empty_arch := {|
   status := fun _ => Stopped;
   wires := fun _ => None
 |}.

the five kinds of reconfiguration operations

 Inductive down_op :=
 | Unwire(c: Component)(i: Imports)
 | Stop(c: Component)
 | Fail(c: Component).

 Inductive up_op :=
 | Wire(c: Component)(i: Imports)(d: Component)
 | Start(c: Component).

 Inductive op :=
 | down(o: down_op)
 | up(o: up_op).

 Coercion down: down_op >-> op.
 Coercion up: up_op >-> op.

 Section d.

  Variable s: arch.

  Notation started c := (status s c = Started).
  Notation stopped c := (status s c = Stopped).
  Notation failed c := (status s c = Failed).

  Notation wired c i d := (wires s (c,i) = Some d).
  Notation notwired c i := (wires s (c,i) = None).

  Definition needs c d := exists_ (fun i => is_mandatory c i && (wires s (c,i) ?= Some d)).
  Definition acyclic := acyclic needs.
  Definition rank := rank needs.

architectural invariants, to be preserved


  Record consistent := {
    AI1: forall c i, started c -> mandatory c i -> exists d, wired c i d;
    AI2: forall c i d, started c -> wired c i d -> started d;
    AI3: forall c i d, wired c i d -> ~failed c /\ ~failed d;
    AI4: forall c i d, stopped c -> wired c i d -> mandatory c i;
    AI5:> acyclic
  }.

  Lemma AI4': consistent -> forall c i d, wired c i d -> optional c i -> started c.
  Proof.
    intros H c i d Hcid Hci. destruct (AI3 H _ _ Hcid) as [? _].
    case_eq (status s c); auto; intro Hc.
    rewrite (AI4 H c i Hc Hcid) in Hci. discriminate.
    congruence.
  Qed.

lifecycle FSM



the following predicate specifies when an operation is allowed; it corresponds to the lifecycle FSM of the paper.

  Inductive allowed: op -> Prop :=
  | wire_m: forall c i d, notwired c i -> mandatory c i -> stopped c -> allowed (Wire c i d)
  | wire_o: forall c i d, notwired c i -> optional c i -> started c -> allowed (Wire c i d)
  | unwire_m: forall c i, ~notwired c i -> mandatory c i -> stopped c -> allowed (Unwire c i)
  | unwire_o: forall c i, ~notwired c i -> optional c i -> started c -> allowed (Unwire c i)
  | start: forall c, stopped c -> allowed (Start c)
  | stop: forall c, started c -> allowed (Stop c)
  | fail: forall c, allowed (Fail c).

applying atomic reconfiguration operations to an architecture

  Definition down_apply (o: down_op): arch :=
    match o with
      | Unwire c i => mk_arch (status s) (set (c,i) None (wires s))
      | Stop c => mk_arch (set c Stopped (status s)) (wires s)
      | Fail c => mk_arch (set c Failed (status s)) (wires s)
    end.

  Definition up_apply (o: up_op): arch :=
    match o with
      | Wire c i d => mk_arch (status s) (set (c,i) (Some d) (wires s))
      | Start c => mk_arch (set c Started (status s)) (wires s)
    end.

  Definition apply (o: op): arch :=
    match o with
      | down o => down_apply o
      | up o => up_apply o
    end.

comparison functions for operations

  Definition cmp_down_op o1 o2 :=
    match o1,o2 with
      | Unwire c i, Unwire d j => cmp (c,i) (d,j) | Unwire _ _, _ => Lt | _, Unwire _ _ => Gt
      | Stop c, Stop d => cmp c d | Stop _, _ => Lt | _, Stop _ => Gt
      | Fail c, Fail d => cmp c d
    end.
  Instance Cmp_down_op: Cmp cmp_down_op | 2.
  Proof.
    constructor.
     destruct x; destruct y; simpl; rewrite ?cmp_eq; intuition congruence.
     destruct x; destruct y; simpl; trivial; apply cmp_sym.
     destruct x; destruct y; destruct z; simpl; trivial; try discriminate; apply cmp_trans.
  Qed.

  Definition cmp_up_op o1 o2 :=
    match o1,o2 with
      | Wire c i c', Wire d j d' => cmp (c,i,c') (d,j,d') | Wire _ _ _, _ => Lt | _, Wire _ _ _ => Gt
      | Start c, Start d => cmp c d
    end.
  Instance Cmp_up_op: Cmp cmp_up_op | 2.
  Proof.
    constructor.
     destruct x; destruct y; simpl; rewrite ?cmp_eq; intuition congruence.
     destruct x; destruct y; simpl; trivial; apply cmp_sym.
     destruct x; destruct y; destruct z; simpl; trivial; try discriminate; apply cmp_trans.
  Qed.

V-ordering of reconfiguration operations


auxiliary functions

  Variable rank: Component -> nat.
  Inductive down_kop := kUnwire_o | kStop(rank: nat) | kUnwire_m | kFail.
  Inductive up_kop := kWire_m | kStart(rank: nat) | kWire_o.
  Definition kind_of_down_op o :=
    match o with
      | Unwire c i => if is_mandatory c i then kUnwire_m else kUnwire_o
      | Stop c => kStop (rank c)
      | Fail _ => kFail
    end.
  Definition kind_of_up_op o :=
    match o with
      | Wire c i _ => if is_mandatory c i then kWire_m else kWire_o
      | Start c => kStart (rank c)
    end.
  Definition cmp_down_kop o1 o2 :=
    match o1,o2 with
      | kUnwire_o, kUnwire_o => Eq | kUnwire_o, _ => Lt | _, kUnwire_o => Gt
      | kStop r, kStop s => nat_compare r s | kStop _, _ => Lt | _, kStop _ => Gt
      | kUnwire_m, kUnwire_m => Eq | kUnwire_m, _ => Lt | _, kUnwire_m => Gt
      | kFail, kFail => Eq
    end.
  Definition cmp_up_kop o1 o2 :=
    match o1,o2 with
      | kWire_m, kWire_m => Eq | kWire_m, _ => Lt | _, kWire_m => Gt
      | kStart r, kStart s => nat_compare s r | kStart _, _ => Lt | _, kStart _ => Gt
      | kWire_o, kWire_o => Eq
    end.
  Instance Cmp_down_kop: Cmp cmp_down_kop.
  Proof.
    constructor.
     destruct x; destruct y; simpl; rewrite ?cmp_eq; intuition congruence.
     destruct x; destruct y; simpl; trivial; apply cmp_sym.
     destruct x; destruct y; destruct z; simpl; trivial; try discriminate; apply cmp_trans.
  Qed.
  Instance Cmp_up_kop: Cmp cmp_up_kop.
  Proof.
    constructor.
     destruct x; destruct y; simpl; rewrite ?cmp_eq; intuition congruence.
     destruct x; destruct y; simpl; trivial; apply cmp_sym.
     destruct x; destruct y; destruct z; simpl; trivial; try discriminate.
     intros A B. revert B A. apply cmp_trans.
  Qed.

final V-ordering functions

  Definition order_down_op o1 o2 := lex (cmp_down_kop (kind_of_down_op o1) (kind_of_down_op o2)) (cmp_down_op o1 o2).
  Definition order_up_op o1 o2 := lex (cmp_up_kop (kind_of_up_op o1) (kind_of_up_op o2)) (cmp_up_op o1 o2).

  Instance Cmp_order_down_op: Cmp order_down_op.
  Proof.
    unfold order_down_op. constructor.
     intros x y. rewrite lex_eq, 2cmp_eq. intuition congruence.
     intros x y. rewrite lex_sym. f_equal. f_equal; symmetry; apply cmp_sym.
     intros x y z. rewrite 3lex_lt, 3cmp_eq. intuition try congruence.
      left. eapply cmp_trans; eauto.
      right. split. congruence. eapply cmp_trans; eauto.
  Qed.

  Instance Cmp_order_up_op: Cmp order_up_op.
  Proof.
    unfold order_up_op. constructor.
     intros x y. rewrite lex_eq, 2cmp_eq. intuition congruence.
     intros x y. rewrite lex_sym. f_equal. f_equal; symmetry; apply cmp_sym.
     intros x y z. rewrite 3lex_lt, 3cmp_eq. intuition try congruence.
      left. eapply cmp_trans; eauto.
      right. split. congruence. eapply cmp_trans; eauto.
  Qed.

 End d.
 Existing Instance Cmp_order_down_op.
 Existing Instance Cmp_order_up_op.

applying sequences of operations

 Definition apply_down_seq s (l: list down_op) := fold_left down_apply l s.
 Definition apply_up_seq s (l: list up_op) := fold_left up_apply l s.
 Definition apply_seq s (l: list op) := fold_left apply l s.

Incrementally Consistent Sequences (ICS)


 Inductive ics: arch -> list op -> Prop :=
 | as_nil: forall s, consistent s -> ics s nil
 | as_cons: forall s o q, allowed s o -> consistent s -> ics (apply s o) q -> ics s (o::q).

 Lemma apply_ics_consistent: forall s l, ics s l -> consistent (apply_seq s l).
 Proof. induction 1; auto. Qed.

 Lemma ics_comp: forall s h k, ics s h -> ics (apply_seq s h) k -> ics s (h++k).
 Proof. induction 1; trivial; constructor; auto. Qed.

 Lemma ics_prefix s h k: ics s (h++k) -> ics s h.
 Proof. revert s. induction h; intros s Hhk; inversion_clear Hhk; constructor; auto. Qed.

 Lemma ics_suffix s h k: ics s (h++k) -> ics (apply_seq s h) k.
 Proof.
   revert s. induction h; simpl; trivial. intros s Hhk.
   inversion_clear Hhk. auto.
 Qed.

propagation algorithm, to saturate "apply down sets"


auxiliary functions to fold through wires

 Definition fold_wires s A c (f: Imports -> list A) :=
   fold (fun i a =>
     match wires s (c,i) with
       | Some _ => f i ++ a
       | None => a
     end) nil.

 Definition fold_optional_wires s A c (f: Imports -> list A) :=
   fold_wires s c (fun i => if is_mandatory c i then nil else f i).

 Definition fold_pointing_wires s A c (f: Component -> Imports -> list A) :=
   fold (fun di a => if wires s di ?= Some c then f (fst di) (snd di) ++ a else a) nil.

 Definition fold_optional_pointing_wires s A c (f: Component -> Imports -> list A) :=
   fold_pointing_wires s c (fun d i => if is_mandatory d i then nil else f d i).

 Definition fold_mandatory_pointing_components s A c (f: Component -> list A) :=
   fold_pointing_wires s c (fun d i => if is_mandatory d i then f d else nil).

propagating stopped goals (unlike in the paper, we unfold the recursive calls to unwire optional imports: this allows us to get a simply recursive function rather than mutually recursive functions)

 Fixpoint xpropagate_stop n s c :=
   match status s c with
     | Started =>
       (match n with O => nil | S n => fold_mandatory_pointing_components s c (xpropagate_stop n s) end) ++
       (fold_optional_pointing_wires s c (fun d i => Unwire d i::nil)) ++
       (fold_optional_wires s c (fun i => Unwire c i::nil)) ++
       (Stop c) :: nil
     | _ => nil
   end.
 Definition propagate_stop := xpropagate_stop (cardinal Component).

propagating unwired goals

 Definition propagate_unwire s c i :=
   match wires s (c,i) with
     | Some _ =>
       if is_mandatory c i then propagate_stop s c ++ Unwire c i :: nil
       else Unwire c i :: nil
     | _ => nil
   end.

propagating failed goals

 Definition propagate_fail s c :=
   match status s c with
     | Failed => nil
     | _ =>
       fold_pointing_wires s c (propagate_unwire s) ++
       fold_wires s c (propagate_unwire s c) ++
       Fail c :: nil
   end.

architectural diff to generate apply up/down sets


generating saturated apply down sets by architectural diff and propagation (we assume that the source does not contain more failed components than the target)

 Definition needs_unwire c d :=
   match c,d with
     | Some _,None => true
     | Some c, Some d => negb (c?=d)
     | _,_ => false
   end.

 Definition down_diff e t :=
   fold (fun c l =>
     match status e c, status t c with
       | _, Failed => propagate_fail e c ++ l
       | Started, Stopped => propagate_stop e c ++ l
       | _,_ => l
     end) nil
   ++
   fold (fun di l =>
     if needs_unwire (wires e di) (wires t di)
       then propagate_unwire e (fst di) (snd di) ++ l
       else l)
   nil.

generating up sets: just architectural diff (we assume that the target is reachable by up operations only, i.e., that the down phase succeeded)

 Definition up_diff e t :=
   fold (fun c l =>
     match status e c, status t c with
       | Stopped, Started => Start c :: l
       | _,_ => l
     end) nil
   ++
   fold (fun di l =>
     match wires e di, wires t di with
       | None, Some c => Wire (fst di) (snd di) c :: l
       | _,_ => l
     end) nil.

final commit session algorithm, without considering failures


(returns the sequence of operations to apply)

 Definition commit_seq e t :=
   let d := sort (order_down_op (rank e)) (down_diff e t) in
   let e := apply_down_seq e d in
   let u := sort (order_up_op (rank t)) (up_diff e t) in
     map down d ++ map up u.

Proofs


comparing architecures


 Inductive les: relation Status :=
 | les_refl: forall x, les x x
 | les_ur: les Stopped Started
 | les_f: forall x, les Failed x.
 Lemma les_r: forall x, les x Started.
 Proof. destruct x; constructor. Qed.

 Hint Constructors les. Hint Resolve les_r.

e<=t holds when e is less functional than t, and when wires from e are wired like in t

 Record le (e t: arch): Prop := mk_le {
   le_status: forall c, les (status e c) (status t c);
   le_wires: forall ci, wires e ci = None \/ wires t ci = wires e ci
 }.
 Infix "<=" := le.

isomorphism of architectures

 Record isomorph (e t: arch): Prop := mk_eq {
   iso_status: forall c, status e c = status t c;
   iso_wires: forall ci, wires t ci = wires e ci
 }.
 Infix "==" := isomorph (at level 80).

 Lemma ge_wires e t: e <= t -> forall ci, wires t ci = None -> wires e ci = None.
 Proof. intros [_ H] ci. destruct (H ci); congruence. Qed.

 Instance les_preorder: PreOrder les.
 Proof.
   constructor.
    constructor.
    intros ? ? ? H1 H2. destruct H1; inversion_clear H2; constructor.
 Qed.

 Instance le_preorder: PreOrder le.
 Proof.
   constructor. intro. constructor. reflexivity. intro. auto.
   intros ? ? ? H1 H2. constructor.
    intro. eapply les_preorder. apply H1. apply H2.
    intro. edestruct (le_wires H1) as [-> | <-]; auto. apply H2.
 Qed.
 Hint Extern 0 (?x <= ?x) => apply le_preorder.

 Instance eq_equivalence: Equivalence isomorph.
 Proof.
   constructor.
    intro. constructor; reflexivity.
    intros ? ? [? ?]. split; auto.
    intros ? ? ? [? ?] [? ?]. split; congruence.
 Qed.

 Instance le_PartialOrder: PartialOrder isomorph le.
 Proof.
   intros e t. split.
   intros [Hs Hw]; split; split; auto; intro; rewrite Hs; trivial.
   intros [[Hs1 Hw1] [Hs2 Hw2]]. split.
    intro c. generalize (Hs1 c) (Hs2 c). inversion 1; trivial. inversion 1. inversion 1; trivial.
    intros ci. destruct (Hw1 ci) as [H|]; trivial. destruct (Hw2 ci); congruence.
 Qed.

has an architecture less failed components than another one ?

 Definition less_failures e t := forall c, status e c = Failed -> status t c = Failed.
 Infix "<<" := less_failures (at level 80).

 Instance less_failures_preorder: PreOrder less_failures.
 Proof. constructor; firstorder. Qed.

conjunction of <= and <<

 Definition le_and_less_failures e t :=
   (forall c, status e c = status t c \/ status e c = Stopped /\ status t c = Started) /\
   (forall ci, wires e ci = None \/ wires t ci = wires e ci).
 Infix "<<=" := le_and_less_failures (at level 80).

 Lemma leless_le_less e t: e <<= t <-> (e<=t /\ e<<t).
 Proof.
   split.
    intros [Hs Hw]. split. split; trivial.
     intro c. destruct (Hs c) as [->|[-> ->]]; trivial.
     intro c. destruct (Hs c) as [->|[-> ->]]; congruence.
   intros [[Hs Hw] Hf]. split; trivial.
    intro c. specialize (Hs c). inversion Hs; auto. subst.
    left. symmetry. apply Hf. auto.
 Qed.

miscellaneous lemmas


 Lemma consistent_empty: consistent empty_arch.
 Proof.
   constructor; intros; try discriminate.
   intro. constructor. intros ?. unfold needs. case exists_spec; try discriminate.
   intros (?&H). rewrite andb_comm in H. discriminate.
 Qed.

 Lemma apply_down_seq_map s l: apply_down_seq s l = apply_seq s (map down l).
 Proof. revert s. induction l; simpl; auto. Qed.

 Lemma apply_up_seq_map s l: apply_up_seq s l = apply_seq s (map up l).
 Proof. revert s. induction l; simpl; auto. Qed.

 Lemma apply_seq_app s h k: apply_seq s (h++k) = apply_seq (apply_seq s h) k.
 Proof. revert s. induction h; simpl; auto. Qed.

 Lemma le_acyclic s t: acyclic t -> s <= t -> acyclic s.
 Proof.
   intros Ht Hst. eapply subrelation_acyclic. eassumption.
   intros x y. unfold needs. rewrite 2exists_iff.
   intros [i Hi]. exists i.
   destruct (is_mandatory x i). 2: discriminate.
   destruct (le_wires Hst (x,i)) as [H|H].
    rewrite H in Hi. discriminate.
    rewrite H. assumption.
 Qed.

 Lemma wires_rank s (Hs: acyclic s) d i c: mandatory d i -> wires s (d,i) = Some c -> rank s d < rank s c.
 Proof.
   intros H1 H2. apply rank_spec. assumption.
   unfold needs. rewrite exists_iff.
   exists i. rewrite H1, H2. simpl. case eq_spec; auto.
 Qed.

 Lemma apply_allowed_down_op_le s (o: down_op): allowed s o -> apply s o <= s.
 Proof.
   destruct s as [s w]. inversion_clear 1; split; intros; simpl in *; auto.
   set_case; auto.
   set_case; auto.
   set_case. rewrite H0. constructor.
   set_case.
 Qed.

 Lemma apply_down_ics_le s l: ics s (map down l) -> apply_down_seq s l <= s.
 Proof.
   revert s. induction l; intros s Hl; inversion_clear Hl; simpl; trivial.
   etransitivity. apply IHl. assumption.
   apply apply_allowed_down_op_le. assumption.
 Qed.

 Lemma apply_allowed_less_failures s o: allowed s o -> s << apply s o.
 Proof. destruct s as [s w]; destruct 1; intro; simpl in *; trivial; set_case. Qed.

 Lemma apply_ics_less_failures s l: ics s l -> s << apply_seq s l.
 Proof.
   revert s; induction 1 as [|s' o q Ho Hs Hq IH]; simpl.
    intro. trivial.
    intros c H. eapply apply_allowed_less_failures, IH in H; assumption.
 Qed.

 Lemma nofail_less_failures s o: (forall c, o<>down (Fail c)) -> apply s o << s.
 Proof.
   intro H. destruct s; destruct o as [o|o]; destruct o; intro x; simpl; trivial.
   set_case.
   eelim H. reflexivity.
   set_case.
 Qed.

 Lemma nofail_seq_less_failures s l: (forall c, ~In (down (Fail c)) l) -> apply_seq s l << s.
 Proof.
   revert s. induction l; simpl; intros s Hl.
    reflexivity.
    rewrite IHl. apply nofail_less_failures. firstorder.
    firstorder.
 Qed.

sufficient conditions for operations to preserve consistency


 Lemma consistent_unwire_notstarted s c i: consistent s ->
   status s c <> Started -> consistent (apply s (Unwire c i)).
 Proof.
   destruct s as [s w]. intros [H1 H2 H3 H4 H5] Hc. constructor; simpl in *.
    intros d j Hd Hdj. destruct (H1 d j) as [e ?]; trivial. exists e. set_case.
    intros d j d' Hd. set_case. apply H2, Hd.
    intros d j d'. set_case. apply H3.
    intros d j d' Hd. set_case. apply H4, Hd.
    eapply subrelation_acyclic. apply H5.
    intros x y; unfold needs. rewrite 2exists_iff.
    intros [j H]. exists j. revert H. simpl. set_case. rewrite andb_comm. discriminate.
 Qed.

 Lemma consistent_unwire_optional s c i: consistent s ->
   optional c i -> consistent (apply s (Unwire c i)).
 Proof.
   destruct s as [s w]. intros [H1 H2 H3 H4 H5] Hci. constructor; simpl in *.
    intros d j Hd Hdj. destruct (H1 d j) as [e ?]; trivial. exists e. set_case.
    intros d j d' Hd. set_case. apply H2, Hd.
    intros d j d'. set_case. apply H3.
    intros d j d' Hd. set_case. apply H4, Hd.
    eapply subrelation_acyclic. apply H5.
    intros x y; unfold needs. rewrite 2exists_iff.
    intros [j H]. exists j. revert H. simpl. set_case. rewrite andb_comm. discriminate.
 Qed.

 Lemma consistent_stop s c: consistent s ->
   (forall i, optional c i -> wires s (c,i) = None) ->
   (forall d i, wires s (d,i) = Some c -> status s d <> Started) ->
   consistent (apply s (Stop c)).
 Proof.
   destruct s as [s w]. intros [H1 H2 H3 H4 H5] Ho Hw. constructor; simpl in *.
    intros d j. set_case. apply H1.
    intros d j d'. set_case. intros Hd Hdj. specialize (H2 _ _ _ Hd Hdj). set_case. eelim Hw; eauto.
    intros d j d' Hd. split.
     set_case. apply (H3 _ _ _ Hd).
     set_case. apply (H3 _ _ _ Hd).
    intros d j d'. set_case; intros Hd Hdj.
     case_eq (is_mandatory d j); trivial. intro Hj. specialize (Ho _ Hj). congruence.
     eapply H4; eassumption.
    apply H5.
 Qed.

 Lemma consistent_fail s c: consistent s ->
   (forall i, wires s (c,i) = None) ->
   (forall d i, wires s (d,i) <> Some c) ->
   consistent (apply s (Fail c)).
 Proof.
   destruct s as [s w]. intros [H1 H2 H3 H4 H5] He Hi. constructor; simpl in *.
    intros d j. set_case. apply H1.
    intros d j d'. set_case. intros Hd Hdj. specialize (H2 _ _ _ Hd Hdj). set_case.
    intros d j d' Hd. destruct (H3 _ _ _ Hd) as [? ?]. pose proof (Hi d j). split; set_case.
    intros d j d'. set_case. apply H4.
    apply H5.
 Qed.

 Lemma consistent_start s c: consistent s ->
   status s c <> Failed ->
   (forall i, mandatory c i -> exists d, wires s (c,i) = Some d /\ status s d = Started) ->
   (forall i, optional c i -> wires s (c,i) = None) ->
   consistent (apply s (Start c)).
 Proof.
   intro Hs. assert (H4' := AI4' Hs). revert Hs.
   destruct s as [s w]. intros [H1 H2 H3 H4 H5] Hc Hm Ho. constructor; simpl in *.
    intros d j. set_case.
     intros _ Hdj. destruct (Hm _ Hdj) as (?&?&?). eauto.
     apply H1.
    intros d j d' H Hdjd'. case_eq (is_mandatory d j); intro Hdj.
     revert H. set_case.
     intros _. set_case. destruct (Hm _ Hdj) as (?&?&?). congruence.
     set_case. intro. eapply H2; eauto.
     revert H. set_case. apply Ho in Hdj. congruence.
     intro H'. set_case. eapply H4' in Hdj; eauto.
    intros d j d' Hdjd'. apply H3 in Hdjd' as [? ?]. split; set_case.
    intros d j d'. set_case. apply H4.
    apply H5.
 Qed.

 Lemma consistent_wire_mandatory s c i d t: consistent s ->
   status s c = Stopped -> status s d <> Failed -> mandatory c i ->
   acyclic t -> s <= t -> wires t (c,i) = Some d ->
   consistent (apply s (Wire c i d)).
 Proof.
   destruct s as [s w]. intros [H1 H2 H3 H4 H5] Hc Hd Hci Ht Hst Htw. constructor; simpl in *.
    intros e j. set_case. apply H1.
    intros e j d'. set_case. apply H2.
    intros e j d'. set_case. split; congruence. eauto.
    intros e j d'. set_case. apply H4.
    eapply le_acyclic. apply Ht. constructor.
     apply Hst.
     intros ci. generalize (le_wires Hst ci). simpl. set_case. intuition congruence.
 Qed.

 Lemma consistent_wire_optional s c i d t: consistent s ->
   status s c = Started -> status s d = Started -> optional c i ->
   acyclic t -> s <= t -> wires t (c,i) = Some d ->
   consistent (apply s (Wire c i d)).
 Proof.
   destruct s as [s w]. intros [H1 H2 H3 H4 H5] Hc Hd Hci Ht Hst Htw. constructor; simpl in *.
    intros e j. set_case. eauto.
    intros e j d'. set_case. apply H2.
    intros e j d'. set_case. split; congruence. eauto.
    intros e j d'. set_case. apply H4.
    eapply le_acyclic. apply Ht. constructor.
     apply Hst.
     intros ci. generalize (le_wires Hst ci). simpl. set_case. intuition congruence.
 Qed.

applying consistent down sequences containing particular operations actually perform these operations


 Lemma apply_down_ics_unwires s l c i: In (Unwire c i) l -> ics s (map down l) ->
   wires (apply_down_seq s l) (c,i) = None.  Proof.
   intro H. revert s. induction l; intros s Hl; simpl in *. tauto.
   destruct H as [->|H]; inversion_clear Hl.
   apply apply_down_ics_le in H1.
   destruct (le_wires H1 (c,i)) as [?|H']; trivial.
   simpl in *. rewrite <- H'. apply set_idem.
   apply IHl; assumption.
 Qed.

 Lemma apply_down_ics_fails s l c: In (Fail c) l -> ics s (map down l) ->
   status (apply_down_seq s l) c = Failed.
 Proof.
   intro H. revert s. induction l; intros s Hl; simpl in *. tauto.
   destruct H as [->|H]; inversion_clear Hl.
   apply apply_down_ics_le in H1.
   assert (H' := le_status H1 c). simpl in *. rewrite set_idem in H'. inversion H'; congruence.
   apply IHl; assumption.
 Qed.

 Lemma apply_down_ics_nofail s l c: status s c <> Failed -> ~In (Fail c) l -> ics s (map down l) ->
   status (apply_down_seq s l) c <> Failed.
 Proof.
   intros H1 H2. revert s H1. induction l; intros s H1 Hl; simpl in *. tauto.
   inversion_clear Hl. destruct a as [d j|d|d].
    apply IHl; intuition.
    apply IHl. intuition. destruct s; simpl; set_case. assumption.
    case (eq_spec c d). intuition congruence.
    intro. apply IHl. intuition. destruct s; simpl; set_case. assumption.
 Qed.

 Lemma apply_down_ics_stops s l c: In (Stop c) l -> ~In (Fail c) l -> ics s (map down l) ->
   status (apply_down_seq s l) c = Stopped.
 Proof.
   intros H1 H2. revert s. induction l; intros s Hl; simpl in *. tauto.
   destruct H1 as [->|H1]; inversion_clear Hl.
   unfold apply in H1. set (s' := down_apply s (Stop c)) in *.
   assert (H' := le_status (apply_down_ics_le _ H1) c). simpl in H'. rewrite set_idem in H'.
   inversion H'; trivial.
   eelim (apply_down_ics_nofail l c). 2: intuition. 2: eassumption. 2: congruence.
   simpl. rewrite set_idem. discriminate.
   apply IHl; intuition.
 Qed.

abstract characterisation of saturated down sets

(generated by the propagation algorithms, represented by unsorted lists, with possible duplicates)

 Definition xsaturated_down_set s l l' :=
   (forall c, In (Stop c) l ->
     (forall d i, mandatory d i -> wires s (d,i) = Some c -> status s d = Started -> In (Stop d) l') /\
     (forall d i, optional d i -> wires s (d,i) = Some c -> In (Unwire d i) l') /\
     (forall i, optional c i -> wires s (c,i) <> None -> In (Unwire c i) l') /\
     (status s c = Started)) /\
   (forall c i, In (Unwire c i) l ->
     (mandatory c i -> status s c = Started -> In (Stop c) l') /\
     wires s (c,i) <> None) /\
   (forall c, In (Fail c) l ->
     (forall d i, wires s (d,i) = Some c -> In (Unwire d i) l') /\
     (forall i, wires s (c,i) <> None -> In (Unwire c i) l')
   ).
 Definition saturated_down_set s l := xsaturated_down_set s l l.

auxiliary lemmas about saturated down sets

 Lemma xsaturated_down_set_app s l1 l2 l':
   xsaturated_down_set s l1 l' ->
   xsaturated_down_set s l2 l' ->
   xsaturated_down_set s (l1++l2) l'.
 Proof.
   intros H1 H2.
   split; [intro c|split;[intros c i|intro c]];
     rewrite in_app_iff; intros [H|H];
       repeat split; intros; eapply H1 in H || eapply H2 in H; intuition eauto.
 Qed.

 Lemma xsaturated_down_set_incr s l l' l'':
   (forall o, In o l' -> In o l'') ->
   xsaturated_down_set s l l' ->
   xsaturated_down_set s l l''.
 Proof.
   intros H1 H.
   split;[intros c H'|split;[intros c i H'|intros c H']];
   repeat split; intros; eapply H in H'; intuition eauto.
 Qed.

 Lemma saturated_down_set_compat s h k: (forall o, In o h <-> In o k) ->
   (saturated_down_set s h <-> saturated_down_set s k).
 Proof. intro H. unfold saturated_down_set, xsaturated_down_set at 1. repeat setoid_rewrite H. reflexivity. Qed.

merging two saturated down sets gives a saturated down set

 Lemma merge_saturated_down_sets s h k:
   saturated_down_set s h -> saturated_down_set s k -> saturated_down_set s (h++k).
 Proof.
   intros. apply xsaturated_down_set_app; eapply xsaturated_down_set_incr;
   try eassumption; intros; rewrite in_app_iff; auto.
 Qed.

the empty set is saturated

 Lemma saturated_down_set_empty s: saturated_down_set s nil.
 Proof. split; simpl; tauto. Qed.

key lemma: sorting a saturated down set results in an incrementally consistent sequence


 Lemma sorted_saturated_down_set_ics s l: consistent s ->
   sorted (order_down_op (rank s)) l -> saturated_down_set s l -> ics s (map down l).
 Proof.
   intro Hs.
   generalize (wires_rank Hs). generalize (rank s).
   intros rnk Hrnk Hsorted. revert s Hrnk Hs.
   induction Hsorted; simpl; intros s Hrnk Hs Hl. constructor; assumption.
   destruct Hl as (Rl&Wl&Fl). constructor; trivial.

    destruct x as [c i|c|c].
     destruct (Wl c i) as [H1 H2]. left; trivial.
     case_eq (is_mandatory c i); intro Hi.
     constructor 3; trivial. case_eq (status s c); trivial; intro Hc.
      specialize (H1 Hi Hc). simpl in H1. destruct H1 as [?|H1]. discriminate. apply H in H1.
      revert H1. unfold order_down_op. simpl. rewrite Hi. discriminate.
      revert H2. case_eq (wires s (c,i)). intros d Hd. apply (AI3 Hs) in Hd as [? _]. tauto. congruence.
     constructor 4; trivial. revert H2. case_eq (wires s (c,i)).
      intros. eapply AI4'; eauto.
      congruence.
     constructor. apply Rl; left; trivial.
     constructor.

    apply IHHsorted.

     intros d i c. destruct x as [e j|e|e]; try apply Hrnk.
     simpl. set_case. apply Hrnk.

     destruct x as [c i|c|c]. case_eq (is_mandatory c i); intro Hi.
      apply consistent_unwire_notstarted; trivial. intro Hc; trivial. eapply Wl in Hc; simpl; eauto.
      simpl in Hc. destruct Hc as [?|Hq]. discriminate. apply H in Hq.
      cbv in Hq. rewrite Hi in Hq. discriminate.
      apply consistent_unwire_optional; trivial.
      destruct (Rl c) as (H1&H2&H3&H4). left; trivial.
      apply consistent_stop; trivial.
      intros i Hi. case_eq (wires s (c,i)); trivial. intros d Hci. exfalso.
      destruct (H3 i) as [?|H']; trivial. congruence. discriminate.
      apply H in H'. cbv in H'. rewrite Hi in H'. discriminate.
      intros d i Hdi Hd. case_eq (is_mandatory d i); intro Hi.
       destruct (H1 d i) as [H'|H']; trivial; exfalso.
        injection H'; intros; subst; clear H'.
        apply wires_rank in Hdi; trivial. elim (Lt.lt_irrefl _ Hdi). apply Hs.
        apply H in H'. unfold order_down_op in H'. simpl in H'.
        specialize (Hrnk _ _ _ Hi Hdi).
        revert H'. case nat_compare_spec; intro H'.
         rewrite H' in Hrnk. elim (Lt.lt_irrefl _ Hrnk).
         elim (Lt.lt_irrefl _ (Lt.lt_trans _ _ _ H' Hrnk)).
         discriminate.
       destruct (H2 d i) as [?|H']; trivial. discriminate.
       apply H in H'. cbv in H'. rewrite Hi in H'. discriminate.
      destruct (Fl c) as [H1 H2]. left; trivial.
      apply consistent_fail; trivial.
      intros i. case_eq (wires s (c,i)); trivial; intros d Hcid. exfalso.
      destruct (H2 i) as [?|H']. congruence. discriminate. apply H in H'. revert H'.
      cbv. case is_mandatory; discriminate.
      intros d i Hdi. apply H1 in Hdi as [?|H']. discriminate.
      apply H in H'. revert H'. cbv. case is_mandatory; discriminate.

     clear Hsorted IHHsorted. destruct s as [s w].
     destruct x as [c i|c|c]; simpl in *.
      split; simpl. 2: split.
      intros d Hd. destruct (Rl d) as (R1&R2&R3&R4); auto. split. 2: split. 3: split.
       intros e j Hdj. set_case. intros Hej He. destruct (R1 _ _ Hdj Hej He); congruence.
       intros e j Hdj. set_case. intros Hej. destruct (R2 _ _ Hdj Hej); congruence.
       intros j Hdj. set_case. intros Hej. destruct (R3 _ Hdj Hej); congruence.
       assumption.
      intros d j Hdj. destruct (Wl d j) as (W1&W2); auto. split.
       intuition congruence.
       set_case. apply H in Hdj. apply cmp_irrefl in Hdj. congruence.
      intros d Hd. destruct (Fl d) as [F1 F2]; auto. split.
       intros e j. set_case. intro Hej. destruct (F1 _ _ Hej); trivial. congruence.
       intros j. set_case. intro Hej. destruct (F2 _ Hej); trivial. congruence.
      split; simpl. 2: split.
      intros d Hd. destruct (Rl d) as (R1&R2&R3&R4); auto. split. 2: split. 3: split.
       intros e j Hdj. set_case. intros Hej He. destruct (R1 _ _ Hdj Hej He); congruence.
       intros e j Hdj Hej. destruct (R2 _ _ Hdj Hej); congruence.
       intros j Hdj Hej. destruct (R3 _ Hdj Hej); congruence.
       set_case. apply H in Hd. apply cmp_irrefl in Hd. congruence.
      intros d j Hdj. destruct (Wl d j) as (W1&W2); auto. split; trivial.
       set_case. intros Hdj' Hd. destruct (W1 Hdj' Hd); trivial. congruence.
      intros d Hd. destruct (Fl d) as [F1 F2]; auto; firstorder discriminate.
      split; simpl. 2: split.
      intros d Hd. destruct (Rl d) as (R1&R2&R3&R4); auto. split. 2: split. 3: split.
       intros e j Hdj. set_case. intros Hej He. destruct (R1 _ _ Hdj Hej He); congruence.
       intros e j Hdj Hej. destruct (R2 _ _ Hdj Hej); congruence.
       intros j Hdj Hej. destruct (R3 _ Hdj Hej); congruence.
       set_case. apply H in Hd. discriminate.
      intros d j Hdj. destruct (Wl d j) as (W1&W2); auto. split; trivial.
       set_case. intros Hdj' Hd. destruct (W1 Hdj' Hd); trivial. congruence.
      intros d Hd. destruct (Fl d) as [F1 F2]; auto; firstorder discriminate.
 Qed.

the propagation algorithms produce saturated down sets


auxiliary lemmas to reason about wires folding functions

 Lemma fold_wires_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), wires s (c,i) = Some d -> P l -> P (f i++l)) ->
   P nil -> P (fold_wires s c f).
 Proof.
   intro H. apply fold_wspec. intros i l Hl.
   case_eq (wires s (c,i)); eauto.
 Qed.

 Lemma fold_optional_wires_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), optional c i -> wires s (c,i) = Some d -> P l -> P (f i++l)) ->
   P nil -> P (fold_optional_wires s c f).
 Proof.
   intro H. apply fold_wires_wspec. intros.
   case_eq (is_mandatory c i); eauto.
 Qed.

 Lemma fold_pointing_wires_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), wires s (d,i) = Some c -> P l -> P (f d i++l)) ->
   P nil -> P (fold_pointing_wires s c f).
 Proof.
   intro H. apply fold_wspec. intros [d i] l Hl.
   case eq_spec; auto.
 Qed.

 Lemma fold_optional_pointing_wires_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), optional d i -> wires s (d,i) = Some c -> P l -> P (f d i++l)) ->
   P nil -> P (fold_optional_pointing_wires s c f).
 Proof.
   intro H. apply fold_pointing_wires_wspec. intros.
   case_eq (is_mandatory d i); auto.
 Qed.

 Lemma fold_mandatory_pointing_components_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), mandatory d i -> wires s (d,i) = Some c -> P l -> P (f d++l)) ->
   P nil -> P (fold_mandatory_pointing_components s c f).
 Proof.
   intro H. apply fold_pointing_wires_wspec. intros.
   case_eq (is_mandatory d i); eauto.
 Qed.

 Section down.
  Variable s: arch.
  Hypothesis Hs: acyclic s.

analysis of the xpropagate_stop function


  Lemma xpropagate_stop_doesnotfail n:
    forall c d, ~In (Fail d) (xpropagate_stop n s c).
  Proof.
    induction n; intros c d; simpl.
     case status; try tauto.
     rewrite 2 in_app_iff. intros [|[|[|]]]; trivial.
     apply fold_optional_pointing_wires_wspec; firstorder congruence.
     apply fold_optional_wires_wspec; firstorder congruence.
     discriminate.

     case status; try tauto.
     rewrite 3 in_app_iff. intros [|[|[|[|]]]]; trivial.
     apply fold_mandatory_pointing_components_wspec.
      intros ? ? ?. rewrite in_app_iff. firstorder congruence.
      intros [].
     apply fold_optional_pointing_wires_wspec; firstorder congruence.
     apply fold_optional_wires_wspec; firstorder congruence.
     discriminate.
  Qed.

  Lemma xpropagate_stop_unwire n:
    forall c, rank s c < n ->
      let l := xpropagate_stop n s c in
        forall d i, In (Unwire d i) l ->
          (mandatory d i -> status s d = Started -> In (Stop d) l) /\
          (wires s (d,i) <> None).
  Proof.
    induction n; intros c Hn l d i. inversion Hn. simpl in l. revert l.
    case status; try (simpl; tauto).

    apply fold_mandatory_pointing_components_wspec.
    intros d' i' l M W Hl. rewrite app_ass. simpl. rewrite in_app_iff. intros [Hl'|Hl'].
    apply IHn in Hl'. intuition. pose proof (wires_rank Hs M W). eauto with arith.
    apply Hl in Hl'. intuition.

    apply fold_optional_pointing_wires_wspec.
    intros d' i' l M W Hl.
    simpl. rewrite in_app_iff. simpl in Hl. intros [Hl'|Hl'].
    injection Hl'; intros; subst. intuition congruence.
    rewrite in_app_iff in Hl. apply Hl in Hl'. intuition.

    apply fold_optional_wires_wspec.
    intros d' i' l M W Hl. simpl. intros [H|H].
    injection H; intros; subst. intuition congruence.
    apply Hl in H. intuition.

    simpl. intuition discriminate.
  Qed.

  Lemma xpropagate_stop_stops n:
    forall c, status s c = Started -> In (Stop c) (xpropagate_stop n s c).
  Proof.
    destruct n; intros c Hc; simpl; rewrite Hc, !in_app_iff.
     right. right. left. reflexivity.
     right. right. right. left. reflexivity.
  Qed.

  Lemma no_stop_in_fold_optional_pwires c d:
    In (Stop d) (fold_optional_pointing_wires s c (fun d i => Unwire d i::nil)) <-> False.
  Proof. apply fold_optional_pointing_wires_wspec; simpl; intuition discriminate. Qed.

  Lemma no_stop_in_fold_optional_wires c d:
    In (Stop d) (fold_optional_wires s c (fun i => Unwire c i::nil)) <-> False.
  Proof. apply fold_optional_wires_wspec; simpl; intuition discriminate. Qed.

  Lemma xpropagate_stop_only_stops_started n:
    forall c d, rank s c < n -> In (Stop d) (xpropagate_stop n s c) -> status s d = Started.
  Proof.
    induction n; intros c d Hn; simpl. inversion Hn.
    case_eq (status s c); intro Hc; try (simpl; tauto).

    apply fold_mandatory_pointing_components_wspec.
    intros d' i' l M W Hl. rewrite app_ass. rewrite in_app_iff. intros [H|H].
    apply IHn in H. intuition. pose proof (wires_rank Hs M W). eauto with arith.
    apply Hl in H. intuition.

    simpl. rewrite in_app_iff, no_stop_in_fold_optional_pwires.
    rewrite in_app_iff, no_stop_in_fold_optional_wires.

    simpl. intuition congruence.
  Qed.

  Lemma xpropagate_stop_stops_mandatory_pointing n:
    forall c, rank s c < n ->
      forall e i d, In (Stop d) (xpropagate_stop n s c) ->
        mandatory e i -> wires s (e,i) = Some d -> status s e = Started ->
        In (Stop e) (xpropagate_stop n s c).
  Proof.
    induction n; intros c Hn e i d Hd Hei Heid Her. inversion Hn. revert Hd. simpl.
    case status; try (simpl; tauto).
    rewrite 6in_app_iff, 2no_stop_in_fold_optional_wires, 2no_stop_in_fold_optional_pwires.
    intros [Hd|[[]|[[]|[Hd|[]]]]]; left.

     revert Hei Heid Her Hd.
     apply fold_mandatory_pointing_components_wspec; auto.
     intros d' j l Hd'j Hd'jc Hl Hei Heid Her. rewrite 2 in_app_iff. intros [H|H]; eauto.
     left. eapply IHn; eauto. pose proof (wires_rank Hs Hd'j Hd'jc). eauto with arith.

     injection Hd; intros; subst; clear Hd.
     revert Hei Heid Her.
     fold_spec (fun done l => forall e i, done (e,i) -> mandatory e i -> wires s (e,i) = Some d -> status s e = Started -> In (Stop e) l).
     clear i. intros [d' i] done l Hl Htd'i c j H Hcj Hcjd Hc.
     case eq_spec; intro Hdic. simpl. case_eq (is_mandatory d' i); intro Hd'i.
      rewrite in_app_iff. destruct H as [H'|H'].
       injection H'; intros; subst. left. apply xpropagate_stop_stops; trivial.
       right. eapply Hl; eauto.
      eapply Hl; eauto. intuition congruence.
      eapply Hl; eauto. intuition congruence.
  Qed.

  Lemma xpropagate_stop_unwires_optional_pointing n:
    forall c, rank s c < n ->
      forall e i d, In (Stop d) (xpropagate_stop n s c) ->
        optional e i -> wires s (e,i) = Some d -> In (Unwire e i) (xpropagate_stop n s c).
  Proof.
   induction n; intros c Hn e i d Hd Hei Heid. inversion Hn. revert Hd. simpl.
    case status; try (simpl; tauto).
    rewrite 3in_app_iff, no_stop_in_fold_optional_wires, no_stop_in_fold_optional_pwires.
    intros [Hd|[[]|[[]|[Hd|[]]]]].

     rewrite in_app_iff. left. revert Hei Heid Hd.
     apply fold_mandatory_pointing_components_wspec; auto.
     intros d' j l Hd'j Hd'jc Hl Hei Heid. rewrite 2 in_app_iff. intros [H|H]; eauto.
     left. eapply IHn; eauto. pose proof (wires_rank Hs Hd'j Hd'jc). eauto with arith.

     injection Hd; intros; subst; clear Hd.
     rewrite 2in_app_iff. right; left. revert Hei Heid.
     fold_spec (fun done l => forall e i, done (e,i) -> optional e i -> wires s (e,i) = Some d -> In (Unwire e i) l).
     clear i. intros [d' i] done l Hl Hdoned'i c j H Hcj Hcjd.
     case eq_spec; intro Hdic. simpl. case_eq (is_mandatory d' i); intro Hd'i.
      apply Hl; intuition congruence.
      simpl. destruct H. left. congruence.
      right. apply Hl; intuition congruence.
      apply Hl; intuition congruence.
  Qed.

  Lemma xpropagate_stop_unwires_optional n:
    forall c, rank s c < n ->
      forall i d, In (Stop d) (xpropagate_stop n s c) ->
        optional d i -> wires s (d,i) <> None -> In (Unwire d i) (xpropagate_stop n s c).
  Proof.
   induction n; intros c Hn i d Hd Hdi Hdin. inversion Hn. revert Hd. simpl.
    case status; try (simpl; tauto).
    rewrite 3in_app_iff, no_stop_in_fold_optional_wires, no_stop_in_fold_optional_pwires.
    intros [Hd|[[]|[[]|[Hd|[]]]]].

     rewrite in_app_iff. left. revert Hdi Hdin Hd.
     apply fold_mandatory_pointing_components_wspec; auto.
     intros d' j l Hd'j Hd'jc Hl Hei Heid. rewrite 2in_app_iff. intros [H|H]; eauto.
     left. eapply IHn; eauto. pose proof (wires_rank Hs Hd'j Hd'jc). eauto with arith.

     injection Hd; intros; subst; clear Hd.
     rewrite <-2app_ass, 2in_app_iff. left; right. revert Hdi Hdin.
     fold_spec (fun done l => forall i, done i -> optional d i -> wires s (d,i) <> None -> In (Unwire d i) l).
     clear i. intros i done l Hl Hti j Htj Htdj Hdjn.
     case_eq (wires s (d,i)). intros c Hdic. case_eq (is_mandatory d i); intro Hdi.
      apply Hl; intuition congruence.
      simpl. case Htj; intro H'. left. congruence. right. apply Hl; intuition congruence.
      intro. apply Hl; intuition congruence.
  Qed.

  Lemma propagate_stop_stops c: status s c = Started -> In (Stop c) (propagate_stop s c).
  Proof. apply xpropagate_stop_stops. Qed.

  Lemma propagate_stop_doesnotfail c d: ~In (Fail d) (propagate_stop s c).
  Proof. apply xpropagate_stop_doesnotfail. Qed.

propagate_stop is correct

  Theorem propagate_stop_saturated c: saturated_down_set s (propagate_stop s c).
  Proof.
    assert(R:=rank_cardinal Hs: forall x, rank s x < _).
     split. intros d Hd. split. 2: split. 3: split. 5: split.
     intros e i. apply xpropagate_stop_stops_mandatory_pointing; auto.
     intros e i. apply xpropagate_stop_unwires_optional_pointing; auto.
     intro i. apply xpropagate_stop_unwires_optional; auto.
     eapply xpropagate_stop_only_stops_started; eauto.
     apply xpropagate_stop_unwire; auto.
     intros d Hd. eelim xpropagate_stop_doesnotfail; eauto.
  Qed.

  Lemma propagate_unwire_unwires c i: wires s (c,i) <> None -> In (Unwire c i) (propagate_unwire s c i).
  Proof.
    unfold propagate_unwire.
    case wires. 2: congruence. intros d _.
    case is_mandatory. rewrite in_app_iff. right; left; trivial. left; trivial.
  Qed.

  Lemma propagate_unwire_doesnotfail c i d: ~In (Fail d) (propagate_unwire s c i).
  Proof.
    unfold propagate_unwire. case wires. 2: simpl; tauto.
    intros _. case is_mandatory. 2: simpl; intuition discriminate.
    rewrite in_app_iff. intros [H|H]; simpl in *. 2: intuition discriminate.
    eapply propagate_stop_doesnotfail, H.
  Qed.

propagate_unwire is correct

  Theorem propagate_unwire_saturated c i: saturated_down_set s (propagate_unwire s c i).
  Proof.
    unfold propagate_unwire. case_eq (wires s (c,i)).
    intros d Hcid. case_eq (is_mandatory c i); intro Hci.
    apply xsaturated_down_set_app.
     eapply xsaturated_down_set_incr. 2: apply propagate_stop_saturated. intros. rewrite in_app_iff. auto.
     split. simpl. intuition discriminate.
     split. intros e j [E|[]]. injection E; intros; subst; clear E. split.
      intros _ He. rewrite in_app_iff. left. apply propagate_stop_stops, He.
      congruence.
     simpl. intuition discriminate.
    firstorder congruence.
    intros _. apply saturated_down_set_empty.
  Qed.

  Lemma propagate_fail_fails c: status s c <> Failed -> In (Fail c) (propagate_fail s c).
  Proof.
    unfold propagate_fail.
    case status; try congruence; rewrite 2in_app_iff; right; right; left; trivial.
  Qed.

  Lemma propagate_fail_case c:
    propagate_fail s c = fold_pointing_wires s c (propagate_unwire s)++
                         fold_wires s c (propagate_unwire s c)++Fail c::nil
    \/ propagate_fail s c = nil.
  Proof. unfold propagate_fail. case status; auto. Qed.

  Lemma propagate_fail_fails_once c d: In (Fail d) (propagate_fail s c) -> c=d.
  Proof.
    destruct (propagate_fail_case c) as [->| ->].
    rewrite 2in_app_iff; simpl. intros [H|[H|H]].
     revert H. apply fold_pointing_wires_wspec. intros ? ? ?. rewrite in_app_iff. intuition.
     eelim propagate_unwire_doesnotfail; eassumption.
     simpl; tauto.
     revert H. apply fold_wires_wspec. intros ? ? ?. rewrite in_app_iff. intuition.
     eelim propagate_unwire_doesnotfail; eassumption.
     simpl; tauto.
     intuition congruence.
    simpl; tauto.
  Qed.

propagate_fail is correct

  Theorem propagate_fail_saturated c: saturated_down_set s (propagate_fail s c).
  Proof.
    destruct (propagate_fail_case c) as [->| ->].
     apply xsaturated_down_set_app. eapply xsaturated_down_set_incr.
      intros. rewrite in_app_iff. left. eassumption.
      apply fold_pointing_wires_wspec.
       intros. apply merge_saturated_down_sets.
        apply propagate_unwire_saturated. assumption.
       apply saturated_down_set_empty.
     apply xsaturated_down_set_app. eapply xsaturated_down_set_incr.
      intros. rewrite 2in_app_iff. right. left. eassumption.
      apply fold_wires_wspec.
       intros. apply merge_saturated_down_sets.
        apply propagate_unwire_saturated. assumption.
       apply saturated_down_set_empty.
     split. simpl; intuition discriminate.
     split. simpl; intuition discriminate.
     intros d [E|[]]. injection E; intros <-; clear E. split.
      intros e j Hej. rewrite in_app_iff. left. revert Hej.
      fold_spec (fun done l => forall e j, done (e,j) -> wires s (e,j) = Some c -> In (Unwire e j) l).
      clear e j. intros [d i] done l Hl Htdi e j Htej Hej.
       destruct Htej as [E|Htej]. injection E; intros; subst; clear E. rewrite Hej, eqc_refl.
       rewrite in_app_iff. left. apply propagate_unwire_unwires. simpl. congruence.
       case eq_spec; intros. simpl. rewrite in_app_iff. right. apply Hl; intuition congruence.
       apply Hl; intuition congruence.
      intros j Hj. rewrite 2in_app_iff. right. left. revert Hj.
      fold_spec (fun done l => forall j, done j -> wires s (c,j) <> None -> In (Unwire c j) l).
      clear j. intros j done l Hl Htj i Hi Hce.
       case_eq (wires s (c,j)). intros d Hd.
       rewrite in_app_iff. destruct Hi as [<-|Hi].
       left. apply propagate_unwire_unwires; trivial.
       right. apply Hl; intuition congruence.
       firstorder congruence.
     apply saturated_down_set_empty.
  Qed.

analysis of the down_diff function


  Lemma down_diff_saturated t: saturated_down_set s (down_diff s t).
  Proof.
    unfold down_diff. apply merge_saturated_down_sets.
     apply fold_wspec. 2: apply saturated_down_set_empty.
     intros; case status; case status;
      auto using merge_saturated_down_sets, propagate_fail_saturated, propagate_stop_saturated.
     apply fold_wspec. 2: apply saturated_down_set_empty.
    intros; case needs_unwire;
      auto using merge_saturated_down_sets, propagate_unwire_saturated.
  Qed.

  Lemma down_diff_stops t c:
    status s c = Started -> status t c = Stopped -> In (Stop c) (down_diff s t).
  Proof.
    intros Hsc Htc. unfold down_diff. rewrite in_app_iff. left. revert Hsc Htc.
    fold_spec (fun done l => forall c, done c -> status s c = Started -> status t c = Stopped -> In (Stop c) l).
    clear c. intros c done l Hl Hdonec d [<-|D] Hsd Htd.
     rewrite Hsd, Htd. rewrite in_app_iff. left. apply propagate_stop_stops, Hsd.
     apply (Hl d) in Hsd; trivial.
     case status; case status; trivial; rewrite in_app_iff; right; trivial.
  Qed.

  Lemma down_diff_fails t c:
    status s c <> Failed -> status t c = Failed -> In (Fail c) (down_diff s t).
  Proof.
    intros Hsc Htc. unfold down_diff. rewrite in_app_iff. left. revert Hsc Htc.
    fold_spec (fun done l => forall c, done c -> status s c <> Failed -> status t c = Failed -> In (Fail c) l).
    clear c. intros c done l Hl Hdonec d [<-|D] Hsd Htd.
     rewrite Htd. revert Hsd. case_eq (status s c); try congruence;
     rewrite in_app_iff; left; apply propagate_fail_fails; congruence.
     apply (Hl d) in Hsd; trivial.
     case status; case status; trivial; rewrite in_app_iff; right; trivial.
  Qed.

  Lemma down_diff_doesnotfailtoomuch t c: In (Fail c) (down_diff s t) -> status t c = Failed.
  Proof.
    unfold down_diff. rewrite in_app_iff. intros [H|H].
     revert H. apply fold_wspec. 2: simpl; tauto. intros d l Hl.
     case_eq (status s d); case_eq (status t d); trivial; intros Htd Hsd; rewrite in_app_iff; intros [H|H]; auto.
      eelim propagate_stop_doesnotfail; eassumption.
      apply propagate_fail_fails_once in H. congruence.
      apply propagate_fail_fails_once in H. congruence.
      apply propagate_fail_fails_once in H. congruence.
     exfalso. revert H. apply fold_wspec. 2: simpl; tauto. intros d l Hl.
     case needs_unwire; trivial. rewrite in_app_iff. intuition.
     eelim propagate_unwire_doesnotfail; eassumption.
  Qed.

  Lemma down_diff_unwires t ci:
    needs_unwire (wires s ci) (wires t ci) = true -> In (Unwire (fst ci) (snd ci)) (down_diff s t).
  Proof.
    intros Hci. unfold down_diff. rewrite in_app_iff. right. revert Hci.
    fold_spec (fun done l =>
      forall ci, done ci -> needs_unwire (wires s ci) (wires t ci) = true -> In (Unwire (fst ci) (snd ci)) l).
    clear ci. intros ci done l Hl Hdonec dj [<-|D] Hdj.
     rewrite Hdj. rewrite in_app_iff; left; apply propagate_unwire_unwires.
     destruct ci as [c i]; simpl. intro H. unfold needs_unwire in Hdj. rewrite H in Hdj. discriminate.
     apply (Hl dj) in Hdj; trivial.
     case needs_unwire; trivial; rewrite in_app_iff; right; trivial.
  Qed.

 End down.
 Implicit Arguments sorted_sort [[X] [cmp] [H]].
 Implicit Arguments In_sort [[X] [cmp] [H]].

down_diff generates ICSs

 Lemma down_diff_ics e t: consistent e -> ics e (map down (sort (order_down_op (rank e)) (down_diff e t))).
 Proof.
   intro Hs.
   apply sorted_saturated_down_set_ics; trivial.
   apply sorted_sort.
   eapply saturated_down_set_compat. 2: apply down_diff_saturated.
   intro. apply In_sort.
   apply Hs.
 Qed.

the ICS obtained by down_diff brings the effective system to a state where the target can be reached by up operations only

 Theorem down_diff_leless e t: consistent e -> e << t -> apply_down_seq e (sort (order_down_op (rank e)) (down_diff e t)) <<= t.
 Proof.
   intros Hs Hst.
   cut (forall l, (forall o, In o l <-> In o (down_diff e t)) -> ics e (map down l) ->
     apply_down_seq e l <<= t).
   intro H. apply H. intro. apply In_sort. apply down_diff_ics, Hs.
   intros l Hl Hl'. apply leless_le_less. destruct (apply_down_ics_le _ Hl') as [Hls Hlw]. split. split.
    intro c. case_eq (status e c); intro Hsc; case_eq (status t c); intro Htc; auto.
     rewrite apply_down_ics_stops; auto.
      rewrite Hl. apply down_diff_stops; assumption.
      rewrite Hl. intro H. apply down_diff_doesnotfailtoomuch in H. congruence.
     rewrite apply_down_ics_fails; trivial.
      rewrite Hl. apply down_diff_fails; congruence.
     rewrite Hls, Hsc. reflexivity.
     rewrite apply_down_ics_fails; trivial.
      rewrite Hl. apply down_diff_fails; congruence.
     rewrite (Hst _ Hsc) in Htc. discriminate.
     rewrite Hls, Hsc. reflexivity.

    intro di. destruct (Hlw di) as [?|H']. auto.
    case_eq (needs_unwire (wires e di) (wires t di)); intro H.
     apply down_diff_unwires in H. rewrite <- Hl in H. destruct di as [d i].
     rewrite apply_down_ics_unwires; auto.
     rewrite <- H'. revert H. unfold needs_unwire.
     case wires; auto. intro. case wires. intro. case eq_spec; simpl; intuition congruence. discriminate.

   intros c Hc. case_eq (status e c); intro Hsc; case_eq (status t c); intro Htc; trivial; exfalso.
    apply apply_down_ics_nofail in Hc; trivial. elim Hc. congruence.
     rewrite Hl. intro H. eapply down_diff_doesnotfailtoomuch in H. congruence.
    apply apply_down_ics_nofail in Hc; trivial. elim Hc. congruence.
     rewrite Hl. intro H. eapply down_diff_doesnotfailtoomuch in H. congruence.
    apply apply_down_ics_nofail in Hc; trivial. elim Hc. congruence.
     rewrite Hl. intro H. eapply down_diff_doesnotfailtoomuch in H. congruence.
    apply apply_down_ics_nofail in Hc; trivial. elim Hc. congruence.
     rewrite Hl. intro H. eapply down_diff_doesnotfailtoomuch in H. congruence.
    rewrite (Hst _ Hsc) in Htc. discriminate.
    rewrite (Hst _ Hsc) in Htc. discriminate.
 Qed.

correctness of the up phase


 Lemma in_up_diff_wire e t c i d: In (Wire c i d) (up_diff e t) -> wires e (c,i) = None /\ wires t (c,i) = Some d.
 Proof.
   unfold up_diff. rewrite in_app_iff. intros [H|H].
    exfalso. revert H. apply fold_wspec; trivial.
    intros ? ? ?. case status; trivial. case status; trivial. simpl; intuition discriminate.

    revert H. apply fold_wspec. 2: simpl; intuition discriminate.
    intros [c' j] l Hl.
    case_eq (wires e (c',j)); auto. intro.
    case_eq (wires t (c',j)); auto. intros f ?.
    simpl. intuition congruence.
 Qed.

 Lemma up_diff_wire e t c i d: wires e (c,i) = None -> wires t (c,i) = Some d -> In (Wire c i d) (up_diff e t).
 Proof.
   intros H1 H2. unfold up_diff. rewrite in_app_iff. right.
   revert H1 H2. fold_spec (fun done l =>
     forall c i, done (c,i) -> wires e (c,i) = None -> wires t (c,i) = Some d -> In (Wire c i d) l).
   clear c i. intros [c i] done l Hl _ d' j Hdonedj Hsn Hts.
    case_eq (wires e (c,i)). intros c' H'. eapply Hl; eauto. intuition congruence. intro H'.
    case_eq (wires t (c,i)). intros c' H''. simpl. destruct Hdonedj.
     left. congruence. right. eapply Hl; eauto.
     intro. eapply Hl; eauto. intuition congruence.
 Qed.

 Lemma in_up_diff_start e t c: In (Start c) (up_diff e t) -> status e c = Stopped /\ status t c = Started.
 Proof.
   unfold up_diff. rewrite in_app_iff. intros [H|H].
    revert H. apply fold_wspec. 2: simpl; intuition discriminate.
    intros d l Hl.
    case_eq (status e d); auto. intro Hsd.
    case_eq (status t d); auto. intros Htd.
    simpl. intuition congruence.

    exfalso. revert H. apply fold_wspec; trivial.
    intros ? ? ?. case wires; trivial. case wires; trivial. simpl; intuition discriminate.
 Qed.

 Lemma up_diff_start e t c: status e c = Stopped -> status t c = Started -> In (Start c) (up_diff e t).
 Proof.
   intros H1 H2. unfold up_diff. rewrite in_app_iff. left.
   revert H1 H2. fold_spec (fun done l =>
     forall c, done c -> status e c = Stopped -> status t c = Started -> In (Start c) l).
   clear c. intros c done l Hl _ c' Hdonee Hsn Hts.
    case_eq (status e c); intro H'. eapply Hl; eauto. intuition congruence.
    case_eq (status t c); intro H''. simpl. destruct Hdonee.
     left. congruence. right. eapply Hl; eauto.
     eapply Hl; eauto. intuition congruence.
     eapply Hl; eauto. intuition congruence.
     eapply Hl; eauto. intuition congruence.
 Qed.

 Lemma up_step_consistent e t q x:
   (forall y : up_op, In y q -> order_up_op (rank t) x y = Lt) ->
   consistent e ->
   consistent t ->
   e <<= t ->
   (forall o : up_op, In o (x :: q) <-> In o (up_diff e t)) ->
   In x (up_diff e t) -> consistent (up_apply e x).
 Proof.
   intros H Hs Ht Hst Hl Hx. destruct x as [c i d|c].
   destruct (in_up_diff_wire _ _ _ _ _ Hx) as [Hsci Htci].
    case_eq (is_mandatory c i); intro Hci.
     apply consistent_wire_mandatory with t; trivial.
     case_eq (status e c); trivial; intro Hsc.
     edestruct (AI1 Hs Hsc); eauto. congruence.
     apply leless_le_less in Hst. apply Hst in Hsc. apply (AI3 Ht) in Htci. intuition congruence.
     intro Hd. apply leless_le_less in Hst. apply Hst in Hd. apply (AI3 Ht) in Htci. intuition congruence.
     apply Ht. apply leless_le_less, Hst.
     assert (Htc: status t c = Started). eapply AI4'; eauto.
     assert (Htd: status t d = Started). eapply AI2; eauto.
     apply consistent_wire_optional with t; trivial.
     case_eq (status e c); trivial; intro Hsc.
     eapply up_diff_start in Hsc; eauto.
     rewrite <- Hl in Hsc. simpl in Hsc. destruct Hsc as [?|Hsc]. discriminate.
     apply H in Hsc. revert Hsc. cbv. rewrite Hci. discriminate.
     apply leless_le_less in Hst. apply Hst in Hsc. congruence.
     case_eq (status e d); trivial; intro Hsd.
     eapply up_diff_start in Htd; eauto.
     rewrite <- Hl in Htd. simpl in Htd. destruct Htd as [?|Htd]. discriminate.
     apply H in Htd. revert Htd. cbv. rewrite Hci. discriminate.
     apply leless_le_less in Hst. apply Hst in Hsd. congruence.
     apply Ht. apply leless_le_less, Hst.
     apply in_up_diff_start in Hx as [Hsc Htc].
     apply consistent_start; trivial. congruence.
     intros i Hci. destruct (AI1 Ht Htc Hci) as (d&Hcid). assert (Hd := AI2 Ht _ _ Htc Hcid).
     exists d. destruct(proj2 Hst (c,i)) as [H'|H'].
      eapply up_diff_wire in H'; eauto. rewrite <- Hl in H'. simpl in H'.
      destruct H' as [?|H']. discriminate.
      apply H in H'. unfold order_up_op in H'. simpl in H'. rewrite Hci in H'. discriminate.
      split. congruence. destruct (proj1 Hst d) as [?|[? _]]. congruence.
       eapply up_diff_start in Hd; eauto. rewrite <-Hl in Hd. simpl in Hd.
       apply wires_rank in Hcid; trivial. 2: apply Ht.
       destruct Hd as [?|Hd]. elim (Lt.lt_irrefl (rank t c)). congruence.
       apply H in Hd. revert Hd. unfold order_up_op. simpl. case nat_compare_spec.
        intro. elim (Lt.lt_irrefl (rank t c)). congruence.
        intro. elim (Lt.lt_irrefl (rank t c)). eauto with arith.
        discriminate.
     intros i Hci. case_eq (wires e (c,i)); trivial. intros d Hcid.
     eapply AI4' in Hcid; trivial. congruence.
 Qed.

 Lemma up_step_below e t x: e <<= t -> In x (up_diff e t) -> (up_apply e x) <<= t.
 Proof.
   intros Hst Hx. destruct x as [c i d|c].
    split. apply Hst. intro ci. generalize (proj2 Hst ci). simpl. set_case.
    right. eapply in_up_diff_wire, Hx.
    split. 2:apply Hst. intro d. generalize (proj1 Hst d). simpl. set_case.
    left. symmetry. eapply in_up_diff_start, Hx.
 Qed.

 Lemma up_step_diff e t q x:
   (forall y : up_op, In y q -> order_up_op (rank t) x y = Lt) ->
   (forall o : up_op, In o (x :: q) <-> In o (up_diff e t)) ->
   In x (up_diff e t) ->
   forall o : up_op, In o q <-> In o (up_diff (apply e x) t).
 Proof.
   intros H Hl Hx o. split; intro Ho.
     assert (Hq := proj1 (Hl o) (or_intror _ Ho)).
     destruct o as [c i d|c].
      apply in_up_diff_wire in Hq as [Hsci Htci].
      apply up_diff_wire; trivial. destruct x; simpl; trivial.
      set_case. apply in_up_diff_wire in Hx as [_ Hci].
      apply H in Ho. apply cmp_irrefl in Ho. congruence.
      apply in_up_diff_start in Hq as [Hsc Htc].
      apply up_diff_start; trivial. destruct x; simpl; trivial.
      set_case. apply H in Ho. apply cmp_irrefl in Ho. congruence.
     cut (x<>o /\ In o (up_diff e t)). rewrite <- Hl. simpl. intuition.
     destruct o as [c i d|d].
      apply in_up_diff_wire in Ho as [Hsci Htci]. split.
       intro H'. revert Hsci. rewrite H'. simpl. set_case.
       apply up_diff_wire; trivial. revert Hsci. destruct x; simpl; trivial.
       set_case.
      apply in_up_diff_start in Ho as [Hsc Htc]. split.
       intro H'. revert Hsc. rewrite H'. simpl. set_case.
       apply up_diff_start; trivial. revert Hsc. destruct x; simpl; trivial.
       set_case.
 Qed.

up_diff generates ICSs

 Theorem up_diff_ics e t: consistent e -> consistent t -> e <<= t ->
   ics e (map up (sort (order_up_op (rank t)) (up_diff e t))).
 Proof.
   intros Hs Ht Hst.
   cut (forall l, (forall o, In o l <-> In o (up_diff e t)) ->
     sorted (order_up_op (rank t)) l -> ics e (map up l)).
    intros H. apply H. intro. apply In_sort. apply sorted_sort.
   intros l Hl Hsorted. revert e Hs Hst Hl.
   induction Hsorted; intros e Hs Hst Hl. constructor; trivial.
   assert (Hx := proj1 (Hl x) (or_introl _ (eq_refl _))).
   simpl; constructor; trivial.

   destruct x as [c i d|c]. destruct (in_up_diff_wire _ _ _ _ _ Hx) as [Hsci Htci].
   case_eq (is_mandatory c i); intro Hci.
    constructor 1; trivial. case_eq (status e c); trivial; intro Hsc.
     eapply (AI1 Hs) in Hsc as [? ?]; eauto. congruence.
     apply leless_le_less in Hst. apply Hst in Hsc. apply (AI3 Ht) in Htci. intuition congruence.
    constructor 2; trivial. apply (AI4' Ht) in Htci; trivial.
    case_eq (status e c); trivial; intro Hsc.
     eapply up_diff_start in Hsc; eauto.
     rewrite <- Hl in Hsc. simpl in Hsc. destruct Hsc as [?|Hsc]. discriminate.
     apply H in Hsc. revert Hsc. cbv. rewrite Hci. discriminate.
     apply leless_le_less in Hst. apply Hst in Hsc. congruence.
    constructor. eapply in_up_diff_start, Hx.

   apply IHHsorted.
    eapply up_step_consistent; eauto.
    eapply up_step_below; eauto.
    eapply up_step_diff; eauto.
 Qed.

up_diff brings the effective system to the target architecture

 Theorem up_diff_complete e t: e <<= t -> apply_up_seq e (sort (order_up_op (rank t)) (up_diff e t)) == t.
 Proof.
   intro Hst.
   cut (forall l, (forall o, In o l <-> In o (up_diff e t)) ->
     sorted (order_up_op (rank t)) l -> apply_up_seq e l == t).
    intros H. apply H. intro. apply In_sort. apply sorted_sort.
   intros l Hl Hsorted. revert e Hst Hl.
   induction Hsorted; intros e Hst Hl.

   split.
    intro c. simpl. destruct (proj1 Hst c) as [H|[H1 H2]]; trivial.
    assert (H3 := up_diff_start _ _ _ H1 H2). rewrite <-Hl in H3. elim H3.
    intros [c i]. simpl. destruct (proj2 Hst (c,i)) as [H1|H1]; auto. case_eq (wires t (c,i)); auto; intros d H2.
    assert (H3 := up_diff_wire _ _ _ _ H1 H2). rewrite <-Hl in H3. elim H3.

   assert (Hx := proj1 (Hl x) (or_introl _ (eq_refl _))).
   simpl. apply IHHsorted.
    eapply up_step_below; eauto.
    eapply up_step_diff; eauto.
 Qed.

correctness of the session commit algorithm, in the failure free case


the hypothesis e << t ensures that all failed components in e remain failed in t. In other words, we do not automatically repair failed components.

 Theorem commit_seq_ics e t: consistent e -> consistent t -> e << t -> ics e (commit_seq e t).
 Proof.
   intros Hs Ht Hst.
   pose proof (down_diff_ics t Hs).
   apply ics_comp; trivial.
   rewrite <- apply_down_seq_map. apply up_diff_ics; trivial.
   rewrite apply_down_seq_map. apply apply_ics_consistent. trivial.
   apply down_diff_leless; assumption.
 Qed.

 Theorem commit_seq_complete e t: consistent e -> consistent t -> e << t -> apply_seq e (commit_seq e t) == t.
 Proof.
   intros Hs Ht Hst.
   pose proof (down_diff_ics t Hs).
   unfold commit_seq.
   rewrite apply_seq_app, apply_down_seq_map, <- apply_up_seq_map.
   apply up_diff_complete; trivial.
   rewrite <- apply_down_seq_map. apply down_diff_leless; assumption.
 Qed.


Handling failures



To model failures in Coq, which is a strongly deterministic system, we assume an arbitratry eapply function, that may return an exception. This function is specified by saying that:
  • either it returns a new architecture, in which case this architecture should be the one returned by our deterministic and failure-free apply function,
  • or it returns an exception concerning a component, which should not belong to the set of "already known to be failed components".
The remaining results are parametrised by this eapply function, which means that they hold for all such functions, i.e., for arbitrary sequences of failures.

 Variable eapply: arch -> op -> list Component -> arch + Component.

 Inductive eapply_ind e o fs: arch + Component -> Prop :=
 | ei_nofailure: eapply_ind e o fs (inl _ (apply e o))
 | ei_failure: forall c, ~In c fs -> eapply_ind e o fs (inr _ c).
 Hypothesis eapply_spec: forall e o fs, eapply_ind e o fs (eapply e o fs).

applying a sequence of operations, until a potential failure occurs

 Fixpoint eapply_seq e l fs :=
   match l with
     | nil => (e,None)
     | o::q =>
       match eapply e o fs with
         | inl e' => eapply_seq e' q fs
         | inr c => (e,Some c)
       end
   end.

 Lemma eapply_seq_nofailure e e' l fs: eapply_seq e l fs = (e',None) -> e' = apply_seq e l.
 Proof.
  revert e e'. induction l; simpl; intros e e'. congruence.
  case eapply_spec. apply IHl. intros. discriminate.
 Qed.

 Lemma eapply_seq_failure e e' l c fs: eapply_seq e l fs = (e',Some c) ->
   ~In c fs /\ exists h, exists k, l=h++k /\ e' = apply_seq e h.
 Proof.
  revert e e' c. induction l as [|x q IH]; simpl; intros e e' c. discriminate.
  case eapply_spec.
   intro H. destruct (IH _ _ _ H) as (Hc&h&k&Hl&E).
   split; trivial. exists (x::h), k. split; trivial. rewrite Hl. trivial.
   intros d Hd E. split. congruence. injection E. intros <- <-. clear E.
   exists nil, (x::q). split; trivial.
 Qed.

 Inductive eapply_seq_ind e l fs: arch*option Component -> Prop :=
 | esi_nofailure: eapply_seq_ind e l fs (apply_seq e l, None)
 | esi_failure: forall h k c, l=h++k -> ~In c fs -> eapply_seq_ind e l fs (apply_seq e h, Some c).

 Lemma eapply_seq_spec: forall e l fs, eapply_seq_ind e l fs (eapply_seq e l fs).
 Proof.
   intros e l fs. case_eq (eapply_seq e l fs). intros e' [o|] H.
   apply eapply_seq_failure in H as (Hc&h&k&->&->). econstructor; auto.
   rewrite (eapply_seq_nofailure _ _ _ H). constructor.
 Qed.

applying an ICS always returns a consistent architecture, even when interrupted by a failure

 Lemma eapply_seq_consistent e l fs: ics e l -> consistent (fst (eapply_seq e l fs)).
 Proof.
   induction 1; simpl; trivial.
   case eapply_spec; trivial.
 Qed.

propagating failures and producing recovery ICSs


 Definition recover_failures_set e :=
   fold_right (fun c acc => propagate_fail e c ++ acc) nil.
 Definition recover_failures_seq e fs :=
   map down (sort (order_down_op (rank e)) (recover_failures_set e fs)).

recovering a target is a single pass process

 Definition recover_target t fs := apply_seq t (recover_failures_seq t fs).

on the contrary, we need a fixpoint to recover the effective system

 Fixpoint xrecover_effective n e fs :=
   match n with O => (e,fs) | S n =>
     let ics := recover_failures_seq e fs in
     match eapply_seq e ics fs with
       | (e',None) => (e',fs)
       | (e',Some c) => xrecover_effective n e' (c::fs)
     end
   end.
 Definition recover_effective := xrecover_effective (S (cardinal Component)).

robust / roll-forward / roll-back algorithms


robust commit: in case of failures, we recover the effective system and stop

 Definition robust_commit e t :=
   let ics := commit_seq e t in
   match eapply_seq e ics nil with
     | (e',None) => (e',nil)
     | (e',Some c) => recover_effective e' (c::nil)
   end.

RFP commit: in case of failures, we recover both effective system and the target architecture, and we loop

 Fixpoint xrfp_commit n e t :=
   match n with O => e | S n =>
     match robust_commit e t with
       | (e',nil) => e'
       | (e',fs) =>
         let t' := recover_target t fs in
         xrfp_commit n e' t'
     end
   end.
 Definition rfp_commit := xrfp_commit (cardinal Component).

RBP commit: in case of failures, we switch to RFP with the recovered inital architecture

 Definition rbp_commit e t :=
   match robust_commit e t with
     | (e',nil) => e'
     | (e',fs) =>
       let e0 := recover_target e fs in
         rfp_commit e' e0
   end.

correctness of the recovery phase


 Lemma recover_failures_saturated s fs: consistent s -> saturated_down_set s (recover_failures_set s fs).
 Proof.
   intro Hs. induction fs; simpl.
    apply saturated_down_set_empty.
    auto using merge_saturated_down_sets, (propagate_fail_saturated Hs).
 Qed.

 Lemma recover_failures_ics s fs: consistent s -> ics s (recover_failures_seq s fs).
 Proof.
   intro Hs. apply sorted_saturated_down_set_ics.
   apply Hs.
   apply sorted_sort.
   eapply saturated_down_set_compat. 2: apply recover_failures_saturated; trivial.
   intro. apply In_sort.
 Qed.

 Lemma recover_failures_failed e fs: consistent e -> forall c,
   status (apply_seq e (recover_failures_seq e fs)) c = Failed ->
   status e c = Failed \/ In c fs.
 Proof.
   intros He c.
   unfold recover_failures_seq. rewrite <- apply_down_seq_map.
   set (l := (sort (order_down_op (rank e)) (recover_failures_set e fs))).
   assert (H := @apply_down_ics_nofail e l c).
   assert (C: status e c = Failed \/ status e c <> Failed). case status; intuition congruence.
   destruct C as [C|C]; auto. specialize (H C). intro H'. right.
   assert (C': In c fs \/ ~In c fs). clear. induction fs; simpl. tauto. case (eq_spec a c); tauto.
   destruct C' as [C'|C']; trivial.
   elim H; auto. unfold l. rewrite In_sort. intro F. apply C'. revert F.
   clear. induction fs; simpl. trivial. rewrite in_app_iff. intros [H|H]; auto.
   apply propagate_fail_fails_once in H. auto.
   apply recover_failures_ics, He.
 Qed.

recover target


 Lemma recover_target_consistent t fs: consistent t -> consistent (recover_target t fs).
 Proof. intro Ht. apply apply_ics_consistent, recover_failures_ics, Ht. Qed.

 Lemma recover_target_fails t fs c: consistent t -> In c fs -> status (recover_target t fs) c = Failed.
 Proof.
   intro Ht.
   unfold recover_target, recover_failures_seq. rewrite <- apply_down_seq_map.
   assert (H: status t c = Failed \/ status t c <> Failed). case status; intuition congruence.
   destruct H as [Hc|Hc].
    intros _. apply (recover_failures_ics fs), apply_down_ics_le in Ht as [Ht _].
    specialize (Ht c). rewrite Hc in Ht. inversion Ht; trivial.
   intro H. apply apply_down_ics_fails.
   rewrite In_sort. revert H. induction fs; simpl; trivial.
   rewrite in_app_iff. intros [<-|H]; auto. left. apply propagate_fail_fails. assumption.
   apply recover_failures_ics, Ht.
 Qed.

recover effective


 Lemma xrecover_effective_consistent n: forall e fs, consistent e -> consistent (fst (xrecover_effective n e fs)).
 Proof.
   induction n; intros e fs He; simpl; trivial.
   generalize (eapply_seq_consistent fs (recover_failures_ics fs He)).
   case eapply_seq. intros e' [c|] H; auto.
 Qed.

 Lemma recover_effective_consistent: forall e fs, consistent e -> consistent (fst (recover_effective e fs)).
 Proof. apply xrecover_effective_consistent. Qed.

 Lemma xrecover_effective_fails n e fs c: In c fs -> In c (snd (xrecover_effective n e fs)).
 Proof.
   revert e fs. induction n; simpl; intros e fs. trivial.
   case eapply_seq. intros e' [o|]. intro. apply IHn. right. trivial.
   trivial.
 Qed.

 Lemma recover_effective_fails e fs c: In c fs -> In c (snd (recover_effective e fs)).
 Proof. apply xrecover_effective_fails. Qed.

 Lemma xrecover_effective_failed n e fs: consistent e ->
   forall c, status (fst (xrecover_effective n e fs)) c = Failed ->
     status e c = Failed \/ In c (snd (xrecover_effective n e fs)).
 Proof.
   revert e fs. induction n; simpl; intros e fs He c. auto.
   case eapply_seq_spec; simpl.
    apply recover_failures_failed, He.
    intros h k d Hl Hc H. apply IHn in H as [H|H]; auto.
    assert (H': status (apply_seq e (recover_failures_seq e fs)) c = Failed).
     rewrite Hl, apply_seq_app. apply apply_ics_less_failures; trivial.
     apply ics_suffix. rewrite <- Hl. apply recover_failures_ics; assumption.
     apply recover_failures_failed in H' as [|]; auto. right. apply xrecover_effective_fails. right. trivial.
    apply apply_ics_consistent. apply ics_prefix with k. rewrite <- Hl.
    apply recover_failures_ics, He.
 Qed.

 Lemma recover_effective_failed e fs: consistent e ->
   forall c, status (fst (recover_effective e fs)) c = Failed ->
     status e c = Failed \/ In c (snd (recover_effective e fs)).
 Proof. apply xrecover_effective_failed. Qed.

 Definition xre_size fs := fold (fun c n => if mem c fs then n else S n) O.

 Lemma xre_size_cons d fs:
   xre_size fs = if mem d fs || negb (mem d Component) then xre_size (d::fs) else S (xre_size (d::fs)).
 Proof.
  unfold xre_size, fold. induction sorted_elements as [|x q Hx Hq IH]; simpl.
  rewrite orb_comm. reflexivity.
  assert (Hdq: ~In x q). intro. apply Hx in H. rewrite cmp_refl in H. discriminate.
  rewrite IH. clear IH.
  rewrite eqc_comm. case eq_spec; simpl.
   intros <-. case mem; simpl.
    reflexivity.
    case mem_spec; simpl.
     intro H. apply Hx in H. rewrite cmp_refl in H. discriminate.
     reflexivity.
   intro D.
    case mem_spec; intro Hx'.
     reflexivity.
     case orb; reflexivity.
 Qed.

 Lemma xre_size_incr d fs: ~In d fs -> xre_size fs = S (xre_size (d::fs)).
 Proof.
  rewrite (xre_size_cons d).
  generalize (all_elements d).
  rewrite 2mem_in. case mem; case mem; intuition congruence.
 Qed.

 Lemma xre_size_cardinal fs: xre_size fs < S (cardinal Component).
 Proof.
   unfold xre_size, cardinal, fold. induction elements; simpl.
    auto with arith.
    case mem; simpl; auto with arith.
 Qed.

 Lemma xrecover_effective_complete n e fs: xre_size fs < n -> consistent e ->
   forall c, In c (snd (xrecover_effective n e fs)) -> status (fst (xrecover_effective n e fs)) c = Failed.
 Proof.
   revert e fs. induction n; simpl; intros e fs Hn He c. inversion Hn.
   case eapply_seq_spec. simpl. apply recover_target_fails, He.
   intros h k d Hl Hd H. apply IHn; trivial.
   rewrite (xre_size_incr _ _ Hd) in Hn. auto with arith.
   apply apply_ics_consistent. apply ics_prefix with k. rewrite <- Hl.
   apply recover_failures_ics, He.
 Qed.

 Theorem recover_effective_complete e fs: consistent e ->
   forall c, In c (snd (recover_effective e fs)) -> status (fst (recover_effective e fs)) c = Failed.
 Proof. apply xrecover_effective_complete, xre_size_cardinal. Qed.

correctness of the robust commit algorithm


we always get a consistent architecture
 Theorem robust_commit_consistent e t:
   consistent e -> consistent t -> e << t -> consistent (fst (robust_commit e t)).
 Proof.
   intros He Ht Het.
   unfold robust_commit.
   generalize (eapply_seq_consistent nil (commit_seq_ics He Ht Het)).
   case eapply_seq. intros e' [c|] H; trivial.
   apply recover_effective_consistent, H.
 Qed.

at the end, failed components are declared in the failed set unless they were already failed in the target
 Theorem robust_commit_failed e t: consistent e -> consistent t -> e << t ->
   forall c, status (fst (robust_commit e t)) c = Failed ->
     status t c = Failed \/ In c (snd (robust_commit e t)).
 Proof.
   intros He Ht Het c. unfold robust_commit.
   case eapply_seq_spec; simpl.
    intro H. left. rewrite <- (iso_status (commit_seq_complete He Ht Het)). trivial.
    intros h k d Hl _ H'. apply recover_effective_failed in H' as [H'|H']; auto.
    left. rewrite <- (iso_status (commit_seq_complete He Ht Het)), Hl.
    rewrite apply_seq_app. eapply apply_ics_less_failures; trivial.
    apply ics_suffix. rewrite <- Hl. apply commit_seq_ics; assumption.
    apply apply_ics_consistent. apply ics_prefix with k. rewrite <- Hl.
    apply commit_seq_ics; assumption.
 Qed.

moreover, all components declared in the failed set are properly accounted as failed in the architecture
 Theorem robust_commit_complete e t: consistent e -> consistent t -> e << t ->
   forall c, In c (snd (robust_commit e t)) -> status (fst (robust_commit e t)) c = Failed.
 Proof.
   intros He Ht Het c. unfold robust_commit.
   case eapply_seq_spec. intros []. intros h k d Hl Hd Hc.
   apply recover_effective_complete; trivial.
    apply apply_ics_consistent. apply ics_prefix with k. rewrite <- Hl.
    apply commit_seq_ics; assumption.
 Qed.

correctness of the RFP algorithm


 Theorem rfp_commit_consistent e t:
   consistent e -> consistent t -> e << t -> consistent (rfp_commit e t).
 Proof.
   unfold rfp_commit. revert e t.
   induction (cardinal _); simpl; trivial. intros e t He Ht Het.
   generalize (robust_commit_consistent He Ht Het).
   generalize (robust_commit_failed He Ht Het).
   case robust_commit.
   intros e' [|c q]; simpl; trivial. intros Hcom Hcon.
   apply IHn; trivial.
   apply recover_target_consistent, Ht.
   intros d Hd. apply Hcom in Hd as [Hd|Hd].
    unfold recover_target. apply apply_ics_less_failures.
    apply recover_failures_ics, Ht.
    apply Hd.
    apply recover_target_fails; assumption.
 Qed.

correctness of the RBP algorithm


Note the additional hypothesis t << e, which means with e << t than e and t have the same sets of failed components This is required with this policy: if t contains more failed components, then we cannot roll-back to the initial architecture if a failure occurs after these components have been marked as failed. This is not a real restriction since it seems strange to have more failed components in the target architecture.

 Theorem rbp_commit_consistent e t:
   consistent e -> consistent t -> e << t -> t << e -> consistent (rbp_commit e t).
 Proof.
   unfold rbp_commit. intros He Ht Het Hte.
   generalize (robust_commit_consistent He Ht Het).
   generalize (robust_commit_failed He Ht Het).
   case robust_commit.
   intros e' [|c q]; simpl; trivial. intros Hcom Hcon.
   apply rfp_commit_consistent; trivial.
   apply recover_target_consistent, He.
   intros d Hd. apply Hcom in Hd as [Hd|Hd].
    apply apply_ics_less_failures.
    apply recover_failures_ics, He.
    apply Hte, Hd.
    apply recover_target_fails; assumption.
 Qed.

End s.

This page has been generated by coqdoc