correct_store_buffer: remove unused definitions

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

src/correct_store_buffer.v

@@ -63,53 +63,6 @@ Definition cycle sbState trace :=
   let isSuUsed := List.existsb is_in_su trace in
   List.map (cycle_elt isSuUsed sbState trace) trace.
 
-Definition is_constrained (elt : instr_kind) trace sbState :=
-  match elt, sbState with
-  | (_, (Sp, _)), _ => List.existsb is_in_lsu trace
-  | (Load _, (Lsu, _)), Empty => List.existsb is_in_lu trace || List.existsb is_in_su trace
-  | (Load _, (Lsu, _)), _ => true
-  | (Store, (Lsu, _)), _ => List.existsb is_in_su trace
-  | _, _ => false
-  end.
-
-Definition cycle_on_more_advanced (t : trace_kind) (instr : instr_kind) sbState :=
-  let (_, state) := instr in
-  let isSuUsed := List.existsb is_in_su t in
-  List.map (fun (elt : instr_kind) =>
-              let (_, state') := elt in
-              if state_leb state state' && negb (state_leb state' state) then
-                cycle_elt isSuUsed sbState t elt
-              else
-                elt) t.
-
-Section can_advance.
-  Variable isSuUsed : bool.
-  Variable sbState : sbStateT.
-  Variable n : nat.
-  Variable t : trace_kind.
-
-  Theorem instruction_never_regresses :
-    forall t' e1, t' = cycle sbState t ->
-             List.nth_error t n = Some e1 ->
-             compare_two (List.nth_error t n) (List.nth_error t' n) = true.
-  Proof.
-    intros t' e1 Ht' He1.
-
-    rewrite Ht', He1.
-    unfold cycle.
-    rewrite (map_nth_error _ _ _ He1).
-
-    unfold compare_two.
-    destruct e1.
-    unfold cycle_elt.
-    destruct s, n0.
-    - now destruct (ready _ _ _ && free _ _ _ _), s, o.
-    - simpl.
-      rewrite stage_beq_eq_true, Nat.leb_le.
-      lia.
-  Qed.
-End can_advance.
-
 Definition legal_sb_transitions st sbState sbState' :=
   match st, sbState with
   | Su, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
@@ -117,40 +70,19 @@ Definition legal_sb_transitions st sbState sbState' :=
   | _, _ => sbState' = Full \/ sbState' = NotEmpty \/ sbState' = Empty
   end.
 
-Definition legal_sb_transitions_P suE suE' sbState sbState' :=
-  match suE, suE', sbState with
-  | true, true, Full => sbState' = Full
-  | true, true, _ => sbState' = NotEmpty \/ sbState' = Full
-  | true, false, Full => True
-  | true, false, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
-  | true, false, Empty => sbState' = Empty
-  | false, true, Empty => sbState' = Empty
-  | false, true, Full => sbState' = Full
-  | false, true, _ => sbState' = NotEmpty \/ sbState' = Full
-  | false, false, Full => True
-  | false, false, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
-  | false, false, Empty => sbState' = Empty
-  end.
-
 Section monotonicity.
   Variable opc : opcode.
-  Variable st : stage.
-  Variable e e' d : instr_kind.
+  Variable d : instr_kind.
+  Variable st st' : stage.
   Variable t tpre tpost t' tpre' tpost' tc tc' : trace_kind.
-  Variable i : nat.
   Variable sbState sbState' : sbStateT.
 
-  Hypothesis Ht : t = tpre ++ e :: tpost.
-  Hypothesis Ht' : t' = tpre' ++ e' :: tpost'.
   Hypothesis Hleb : pipeline_leb t t' = true.
-  Hypothesis Hi : i = List.length tpre.
-  Hypothesis Hi' : i = List.length tpre'.
   Hypothesis Hl : pipeline_leb tpre tpre' = true.
   Hypothesis Hl' : pipeline_leb tpost tpost' = true.
   Hypothesis Htc : tc = cycle sbState t.
   Hypothesis Htc' : tc' = cycle sbState' t'.
   Hypothesis Hlsbt : legal_sb_transitions st sbState sbState'.
-  Hypothesis HlsbtP : legal_sb_transitions_P (existsb is_in_su t) (existsb is_in_su t') sbState sbState'.
   Hypothesis Hlu : forall st opc n, st = Lu -> opc = Load n.
   Hypothesis Hsu : forall st opc, st = Su -> opc = Store.
 
@@ -168,236 +100,420 @@ Section monotonicity.
     busFree (existsb is_in_su t) sbState = true ->
     busFree (existsb is_in_su t') sbState' = true.
 
-  Ltac work_on_e He' :=
-    rewrite Htc, Htc', Ht;
-      match goal with
-      | [ _ : e = e' |- _ ] =>
-          rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HbusFree |- *
-      | [ _ : e <> e' |- _ ] =>
-          rewrite Ht'
-      end;
-      unfold cycle;
-      rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi),
-        (map_in_the_middle _ _ _ d _ _ tpre' tpost' _ (eq_refl _) Hi');
-      unfold cycle_elt;
-      rewrite <- Ht;
-      match goal with
-      | [ _ : e = e' |- _ ] =>
-          subst e
-      | [ _ : e <> e' |- _ ] =>
-          rewrite <- Ht';
-            subst e;
-            subst e'
-      end.
-
-  Lemma unmoved_no_lat_can_advance :
-    e = (opc, (st, 0)) -> e = e' -> forall n,
-    List.nth_error tc i = Some (opc, (nstg st opc, n)) ->
-    List.nth_error tc' i = Some (opc, (nstg st opc, n)).
-  Proof.
-    intros He He' n.
-    specialize (Hlu st opc).
-    specialize (Hsu st opc).
-    specialize (HbusFree st).
-
-    (* Delve onto e, then handle stages on a case-by-case basis. *)
-    work_on_e He'.
-    destruct st.
-
-    (* Sp.  The proof does not rely on the kind of instruction. *)
-    - destruct (free _ _ t _) in HfreeLsuPersists |- *.
-      + (* LSU is free in t. *)
-        now destruct (free _ _ _ _) in HfreeLsuPersists |- *;
-          (* Either the next stage is also free in t': trivial. *)
-          (* Otherwise, the next stage is not free in t':
+  Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0.
+  Hypothesis HvalidLdLat : forall (e : instr_kind) st n dlat, e = (Load dlat, (st, n)) -> 0 <> n -> st = Lu /\ n <= dlat.
+
+  Section simple_monotonicity.
+    Variable e e' : instr_kind.
+    Variable i : nat.
+
+    Hypothesis Ht : t = tpre ++ e :: tpost.
+    Hypothesis Ht' : t' = tpre' ++ e' :: tpost'.
+    Hypothesis Hi : i = List.length tpre.
+    Hypothesis Hi' : i = List.length tpre'.
+
+    Ltac work_on_e He' :=
+      rewrite Htc, Htc', Ht;
+        match goal with
+        | [ _ : e = e' |- _ ] =>
+            rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HbusFree |- *
+        | [ _ : e <> e' |- _ ] =>
+            rewrite Ht'
+        end;
+        unfold cycle;
+        rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ eq_refl Hi),
+          (map_in_the_middle _ _ _ d _ _ tpre' tpost' _ eq_refl Hi');
+        unfold cycle_elt;
+        rewrite <- Ht;
+        match goal with
+        | [ _ : e = e' |- _ ] =>
+            subst e
+        | [ _ : e <> e' |- _ ] =>
+            rewrite <- Ht';
+              subst e;
+              subst e'
+        end.
+
+    Lemma unmoved_no_lat_can_advance :
+      e = (opc, (st, 0)) -> e = e' -> forall n,
+      List.nth_error tc i = Some (opc, (nstg st opc, n)) ->
+      List.nth_error tc' i = Some (opc, (nstg st opc, n)).
+    Proof.
+      intros He He' n.
+      specialize (Hlu st opc).
+      specialize (Hsu st opc).
+      specialize (HbusFree st).
+
+      (* Delve onto e, then handle stages on a case-by-case basis. *)
+      work_on_e He'.
+      destruct st.
+
+      (* Sp.  The proof does not rely on the kind of instruction. *)
+      - destruct (free _ _ t _) in HfreeLsuPersists |- *.
+        + (* LSU is free in t. *)
+          now destruct (free _ _ _ _) in HfreeLsuPersists |- *;
+            (* Either the next stage is also free in t': trivial. *)
+            (* Otherwise, the next stage is not free in t':
              this is impossible per HfreeLsuPersists. *)
-          [| discriminate HfreeLsuPersists].
-      + (* LSU is not free in t: this is irrelevant. *)
-        rewrite andb_false_r.
-        discriminate.
-
-    (* Lsu *)
-    - destruct opc, (free _ _ t _) in HfreeFromLsuPersists |- *.
-
-      (* Loads *)
-      + unfold ready.
-        destruct (busFree _ sbState).
-        * now destruct (busFree _ _); [
-              destruct (free _ _ _ _) in HfreeFromLsuPersists |- *;
-                try discriminate HfreeFromLsuPersists |
-              discriminate HbusFree
-            ].
-        * discriminate.
-      + rewrite andb_false_r.
-        discriminate.
-
-      (* Stores *)
-      + now destruct (free _ _ _ _) in HfreeFromLsuPersists |- *;
-          [| discriminate HfreeFromLsuPersists].
-      + discriminate.
-
-    (* Lu: instructions without latency (this is the case here) move to Sn. *)
-    - now rewrite (Hlu n).
-
-    (* Su: if there is space in the store buffer, move to Sn, otherwise, remain
+            [| discriminate HfreeLsuPersists].
+        + (* LSU is not free in t: this is irrelevant. *)
+          rewrite andb_false_r.
+          discriminate.
+
+      (* Lsu *)
+      - destruct opc, (free _ _ t _) in HfreeFromLsuPersists |- *.
+
+        (* Loads *)
+        + unfold ready.
+          destruct (busFree _ sbState).
+          * now destruct (busFree _ _); [
+                destruct (free _ _ _ _) in HfreeFromLsuPersists |- *;
+                  try discriminate HfreeFromLsuPersists |
+                  discriminate HbusFree
+              ].
+          * discriminate.
+        + rewrite andb_false_r.
+          discriminate.
+
+        (* Stores *)
+        + now destruct (free _ _ _ _) in HfreeFromLsuPersists |- *;
+            [| discriminate HfreeFromLsuPersists].
+        + discriminate.
+
+      (* Lu: instructions without latency (this is the case here) move to Sn. *)
+      - now rewrite (Hlu n).
+
+      (* Su: if there is space in the store buffer, move to Sn, otherwise, remain
        in Su.  Eliminate cases where sbState/sbState' are inconsistent. *)
-    - now rewrite Hsu;
-        destruct sbState, sbState', Hlsbt.
+      - now rewrite Hsu; [
+          destruct sbState, sbState', Hlsbt;
+            try discriminate
+        |].
+
+      (* Sn: instructions remains in Sn. *)
+      - auto.
+    Qed.
+
+    Lemma unmoved_is_monotonic :
+      forall n, e = (opc, (st, n)) -> e = e' ->
+                compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+    Proof.
+      intros n He He'.
+
+      (* Extract e. *)
+      pose proof unmoved_no_lat_can_advance as Huca.
+      revert Huca.
+      work_on_e He'.
+      intro Huca.
+
+      destruct n.
+      - (* Case where an instruction has a latency of 0. *)
+        destruct (ready _ _ _ && free _ _ t _).
+        + (* If e (in t) can progress. *)
+          (* apply unmoved_no_lat_can_advance, with all relevant parameters. *)
+          specialize (Huca eq_refl eq_refl).
+          now destruct opc, (nstg _ _);
+            rewrite (Huca 0 eq_refl)
+            || (rewrite (Huca n eq_refl);
+                 apply compare_two_eq_true).
+        + (* If e (in t) cannot progress. *)
+          destruct (_ && _).
+          * (* If e (in t') can progress. cycle_elt e t' > cycle_elt e t.  This
+             * is trivial, but each case must be analysed separately. *)
+            now destruct st, opc.
+          * (* If e (in t') cannot progress. cycle_elt e t' = cycle e  t. This
+             * is also trivial. *)
+            now apply compare_two_eq_true.
+
+      - (* Case where an instruction has a latency higher than 0. *)
+        (* cycle_elt ... e = cycle_elt ... e'.  Then, compare_two ... = true. *)
+        now apply compare_two_eq_true.
+    Qed.
+
+    Lemma moved_no_lat_is_monotonic :
+      e = (opc, (st, 0)) -> e' = (opc, (st', 0)) -> e <> e' ->
+      state_leb (st, 0) (st', 0) = true ->
+      compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+    Proof.
+      intros He He' Hed Hsl.
+      specialize (Hlu st opc 0).
+      pose proof (Hsu st' opc) as Hsu'.
+      specialize (Hsu st opc).
+
+      (* Goal transformation: show exactly how e and e' are modified by the
+       * cycle function. *)
+      work_on_e Hed.
+
+      (* Case-by-case analysis *)
+      destruct st, st';
+        try contradiction;
+        try discriminate.
 
-    (* Sn: instructions remains in Sn. *)
-    - auto.
-  Qed.
+      (* st = Sp, st' = Lsu, Lu, Su, Sn *)
+      - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc.
+      - now destruct (ready _ _ _ && free _ _ _ _), opc.
+      - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc.
+      - now destruct (ready _ _ _ && free _ _ _ _), opc.
+
+      (* st = Lsu, st' = Lu, Su, Sn *)
+      - now destruct (ready _ _ _ && free _ _ _ _), opc.
+      - destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc;
+          try reflexivity.
+        now discriminate Hsu'.
+      - now destruct (ready _ _ _ && free _ _ _ _), opc.
+
+      (* st = Lu, st' = Sn *)
+      - now destruct opc;
+          (* Trivial when opc = Load, eliminate the case where opc = Store. *)
+          [| discriminate Hlu].
+
+      (* st = Su, st' = Sn *)
+      - now destruct opc; [
+          (* Eliminate the case where opc = Load. *)
+          discriminate Hsu |
+            (* Either the instruction remains in Su, or it progresses in Sn. *)
+            (* Both cases are trivial. *)
+            destruct (_ && _)
+        ].
+    Qed.
+
+    Lemma moved_lat_is_monotonic :
+      forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) -> e <> e' ->
+                   state_leb (st, n) (st', n') = true ->
+                   compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+    Proof.
+      intros n n' He He' Hed Hsl.
+      pose proof (HvalidStLat e' st' n') as HvalidStLat'.
+      specialize (HvalidStLat e st n).
+      pose proof (HvalidLdLat e' st' n') as HvalidLdLat'.
+      specialize (HvalidLdLat e st n).
+
+      destruct n, n'; [
+          (* n and n' are = 0.  We have a lemma for that. *)
+          now apply moved_no_lat_is_monotonic |
+            (* Other cases: rewrite the goal to make cycle appear. *)
+            work_on_e Hed;
+              (* Since n or n' is not equal to 0, opc is a load.  Remove other cases. *)
+              destruct opc;
+              [| discriminate (HvalidStLat eq_refl)
+                 || discriminate (HvalidStLat' eq_refl)] ..
+        ].
 
-  Lemma unmoved_is_monotonic :
-    forall n, e = (opc, (st, n)) -> e = e' ->
-         compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+      (* From there, opc = Load. *)
+      (* n = 0 and n' <> 0. *)
+      - (* st' = Lu. *)
+        destruct (HvalidLdLat' n eq_refl (O_S n')) as [Hst' Hlat'].
+        rewrite Hst' in Hsl, Hed |- *.
+        destruct st;
+          try discriminate.
+        + (* st = Sp.  In this case, the next stage is either Sp or Lsu, which are
+           * both lower than Lu. *)
+          now destruct (_ && _).
+        + (* st = Lsu.  In this case, the next stage is either Lsu or Lu. *)
+          destruct (_ && _).
+          * simpl.
+            rewrite Nat.leb_le.
+            lia.
+          * reflexivity.
+
+      (* n <> 0 and n' = 0. *)
+      - (* st = Lu. *)
+        destruct (HvalidLdLat n0 eq_refl (O_S n)) as [Hst Hlat].
+        rewrite Hst in Hsl, Hed |- *.
+        destruct st';
+          (* Sp, Lsu: impossible since e' would be lower than e. *)
+          (* Su: impossible since loads cannot be in Su. *)
+          discriminate
+          (* Lu: since n' = 0, e' will be in Sn in the next cycle, e will still be
+           * in Lu. *)
+          (* Sn: e' will remain in Sn, e will still be in Lu. *)
+          || reflexivity.
+
+      (* n and n' <> 0. *)
+      - destruct (HvalidLdLat n0 eq_refl (O_S n)) as [Hst Hlat].
+        rewrite Hst in Hsl, Hed |- *.
+        (* e is lower than e', hence n > n'. *)
+        now destruct (HvalidLdLat' n0 eq_refl (O_S n')).
+    Qed.
+
+    Theorem is_monotonic :
+      forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) ->
+                   state_leb (st, n) (st', n') = true ->
+                   compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+    Proof.
+      intros n n' He He' Hsl.
+      pose proof (instr_kind_is_comparable e e') as Heqd.
+
+      (* e = e' or e <> e'. *)
+      destruct Heqd as [Heq | Hdiff].
+      - (* If e = e', we have a lemma for this. *)
+        now apply (unmoved_is_monotonic n).
+      - (* If e <> e', we have a lemma for this. *)
+        now apply (moved_lat_is_monotonic n n').
+    Qed.
+  End simple_monotonicity.
+
+  Lemma tc_and_tc' : List.length tc = List.length tc'.
   Proof.
-    intros n He He'.
-
-    pose proof (unmoved_no_lat_can_advance) as Huca.
-    revert Huca.
-    work_on_e He'.
-    intro Huca.
-
-    destruct n.
-    - destruct (ready _ _ _ && free _ _ t _).
-      + specialize (Huca (eq_refl _) (eq_refl _)).
-        now destruct opc, (nstg _ _);
-          rewrite (Huca 0 (eq_refl _))
-          || (rewrite (Huca n (eq_refl _));
-               apply compare_two_eq_true).
-      + destruct (ready _ _ _ && free _ _ _ _), st;
-          try reflexivity;
-          now destruct opc.
-
-    - apply compare_two_eq_true.
-      discriminate.
+    (* i = length tpre = length tpre'. *)
+    (* length t = length t'. *)
+    (* cycle t = map ... t. *)
+    (* length (map ... t) = length t. *)
+    rewrite Htc, Htc'.
+    unfold cycle.
+    repeat rewrite map_length.
+    unfold pipeline_leb in Hleb.
+    now rewrite andb_true_iff, Nat.eqb_eq in Hleb.
   Qed.
 
-  Variable st' : stage.
+  Variable e e' : instr_kind.
+  Variable n n' : nat.
 
-  Lemma moved_no_lat_is_monotonic :
-    e = (opc, (st, 0)) -> e' = (opc, (st', 0)) -> e <> e' ->
-    state_leb (st, 0) (st', 0) = true ->
-    compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
-  Proof.
-    intros He He' Hed Hsl.
-    specialize (Hlu st opc 0).
-    pose proof (Hsu st' opc) as Hsu'.
-    specialize (Hsu st opc).
-
-    (* Goal transformation: show exactly how e and e' are modified by the
-     * cycle function. *)
-    work_on_e Hed.
-
-    (* Case-by-case analysis *)
-    destruct st, st';
-      try contradiction;
-      try discriminate.
-
-    (* st = Sp, st' = Lsu, Lu, Su, Sn *)
-    - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc.
-    - now destruct (ready _ _ _ && free _ _ _ _), opc.
-    - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc.
-    - now destruct (ready _ _ _ && free _ _ _ _), opc.
-
-    (* st = Lsu, st' = Lu, Su, Sn *)
-    - now destruct (ready _ _ _ && free _ _ _ _), opc.
-    - destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc;
-        try reflexivity.
-      now discriminate Hsu'.
-    - now destruct (ready _ _ _ && free _ _ _ _), opc.
-
-    (* st = Lu, st' = Sn *)
-    - now destruct opc;
-        (* Trivial when opc = Load, eliminate the case where opc = Store. *)
-        [| discriminate Hlu].
-
-    (* st = Su, st' = Sn *)
-    - now destruct opc; [
-          (* Eliminate the case where opc = Load. *)
-          discriminate Hsu |
-          (* Either the instruction remains in Su, or it progresses in Sn. *)
-          (* Both cases are trivial. *)
-          destruct (_ && _)
-        ].
-  Qed.
+  Hypothesis Ht : t = tpre ++ e :: tpost.
+  Hypothesis Ht' : t' = tpre' ++ e' :: tpost'.
+  Hypothesis Hi : forall i, i = List.length tpre.
+  Hypothesis Hi' : forall i, i = List.length tpre'.
 
-  Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0.
-  Hypothesis HvalidLdLat : forall (e : instr_kind) st n dlat, e = (Load dlat, (st, n)) -> 0 <> n -> st = Lu /\ n <= dlat.
+  Hypothesis He : e = (opc, (st, n)).
+  Hypothesis He' : e' = (opc, (st', n')).
+  Hypothesis Hsl : state_leb (st, n) (st', n') = true.
 
-  Lemma moved_lat_is_monotonic :
-    forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) -> e <> e' ->
-                 state_leb (st, n) (st', n') = true ->
-                 compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
-  Proof.
-    intros n n' He He' Hed Hsl.
-    pose proof (HvalidStLat e' st' n') as HvalidStLat'.
-    specialize (HvalidStLat e st n).
-    pose proof (HvalidLdLat e' st' n') as HvalidLdLat'.
-    specialize (HvalidLdLat e st n).
-
-    destruct n, n'; [
-        (* n and n' are = 0.  We have a lemma for that. *)
-        now apply moved_no_lat_is_monotonic |
-        (* Other cases: rewrite the goal to make cycle appear. *)
-        work_on_e Hed;
-          (* Since n or n' is not equal to 0, opc is a load.  Remove other cases. *)
-          destruct opc;
-          [| discriminate (HvalidStLat (eq_refl _))
-             || discriminate (HvalidStLat' (eq_refl _))] ..
-      ].
-
-    (* From there, opc = Load. *)
-    (* n = 0 and n' <> 0. *)
-    - (* st' = Lu. *)
-      destruct (HvalidLdLat' n (eq_refl _) (O_S n')) as [Hst' Hlat'].
-      rewrite Hst' in Hsl, Hed |- *.
-      destruct st;
-        try discriminate.
-      + (* st = Sp.  In this case, the next stage is either Sp or Lsu, which are
-         * both lower than Lu. *)
-        now destruct (_ && _).
-      + (* st = Lsu.  In this case, the next stage is either Lsu or Lu. *)
-        destruct (_ && _).
-        * simpl.
-          rewrite Nat.leb_le.
-          lia.
-        * reflexivity.
-
-    (* n <> 0 and n' = 0. *)
-    - (* st = Lu. *)
-      destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat].
-      rewrite Hst in Hsl, Hed |- *.
-      destruct st';
-        (* Sp, Lsu: impossible since e' would be lower than e. *)
-        (* Su: impossible since loads cannot be in Su. *)
-        discriminate
-        (* Lu: since n' = 0, e' will be in Sn in the next cycle, e will still be
-         * in Lu. *)
-        (* Sn: e' will remain in Sn, e will still be in Lu. *)
-          || reflexivity.
+  Let is_monotonic' ni :=
+        is_monotonic e e' ni Ht Ht' (Hi ni) (Hi' ni) n n' He He' Hsl.
 
-    (* n and n' <> 0. *)
-    - destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat].
-      rewrite Hst in Hsl, Hed |- *.
-      (* e is lower than e', hence n > n'. *)
-      now destruct (HvalidLdLat' n0 (eq_refl _) (O_S n')).
+  Lemma cycled_instrs_are_leb :
+    forall instrs, In instrs (combine tc tc') -> instrs_leb instrs = true.
+  Proof.
+    (* Since instrs is in (combine tc tc'), there is a
+     * i' < length (combine tc tc') and
+     * nth i' (combine tc tc') (d, d)) = instrs. *)
+    intros instrs HIn.
+    destruct (In_nth (combine tc tc') instrs (d, d) HIn) as [i HInth].
+    destruct HInth as [Hil Hinstrs].
+
+    (* since nth i (combine tc tc') = instrs,
+     * instrs = (nth i tc d, nth i tc' d). *)
+    rewrite combine_nth in Hinstrs.
+    - (* instrs_leb instrs = true means
+       * compare_two (nth_error tc i) (nth_error tc' i) = true.
+       * We have a lemma for this. *)
+      (* Then, compare_two (nth_error tc i) (nth_error tc' i) = true.
+       * We have a theorem for this. *)
+      rewrite <- Hinstrs.
+      apply (compare_two_true_means_instrs_leb tc tc' i d), (is_monotonic' i).
+    - (* length tc = length tc'.  We have a lemma for this. *)
+      apply tc_and_tc'.
   Qed.
 
-  Theorem is_monotonic :
-    forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) ->
-                 state_leb (st, n) (st', n') = true ->
-                 compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+  Theorem is_fully_monotonic : pipeline_leb tc tc' = true.
   Proof.
-    intros n n' He He' Hsl.
-    pose proof (instr_kind_is_comparable e e') as Heqd.
-
-    (* e = e' or e <> e'. *)
-    destruct Heqd as [Heq | Hdiff].
-    - (* If e = e', we have a lemma for this. *)
-      now apply (unmoved_is_monotonic n).
-    - (* If e <> e', we have a lemma for this. *)
-      now apply (moved_lat_is_monotonic n n').
+    unfold pipeline_leb.
+    rewrite andb_true_iff.
+
+    split.
+    - (* First, length tc = length tc'.  We have a lemma for this. *)
+      rewrite Nat.eqb_eq.
+      apply tc_and_tc'.
+    - (* Now, forallb instrs_leb (combine tc tc') = true. *)
+      (* Transform the goal into
+       * forall instrs, In instrs (combine ...) -> instrs_leb instrs = true. *)
+      rewrite forallb_forall.
+      intros instrs HIn.
+      (* We have a lemma for this. *)
+      now rewrite cycled_instrs_are_leb.
   Qed.
 End monotonicity.
+
+Section monotonicity_everywhere.
+  Variable opc : opcode.
+  Variable d : instr_kind.
+  Variable t t' tc tc' : trace_kind.
+  Variable sbState sbState' : sbStateT.
+
+  Hypothesis Hleb : pipeline_leb t t' = true.
+  Hypothesis Htc : tc = cycle sbState t.
+  Hypothesis Htc' : tc' = cycle sbState' t'.
+
+  Hypothesis Hlsbt : forall st, legal_sb_transitions st sbState sbState'.
+
+  (* Hypothesis Hl : forall tpre tpre', pipeline_leb tpre tpre' = true. *)
+  (* Hypothesis Hl' : forall tpost tpost', pipeline_leb tpost tpost' = true. *)
+
+  Hypothesis Hlu : forall st opc n, st = Lu -> opc = Load n.
+  Hypothesis Hsu : forall st opc, st = Su -> opc = Store.
+
+  (* Long hypotheses related to stage occupation. *)
+  Hypothesis HfreeLsuPersists : forall opc,
+    free (existsb is_in_su t) sbState t (opc, (Sp, 0)) = true ->
+    free (existsb is_in_su t') sbState' t' (opc, (Sp, 0)) = true.
+
+  Hypothesis HfreeFromLsuPersists : forall opc,
+    free (existsb is_in_su t) sbState t (opc, (Lsu, 0)) = true ->
+    free (existsb is_in_su t') sbState' t' (opc, (Lsu, 0)) = true.
+
+  Hypothesis HbusFree :
+    forall st, st = Lsu ->
+    busFree (existsb is_in_su t) sbState = true ->
+    busFree (existsb is_in_su t') sbState' = true.
+
+  Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0.
+  Hypothesis HvalidLdLat : forall (e : instr_kind) st n dlat, e = (Load dlat, (st, n)) -> 0 <> n -> st = Lu /\ n <= dlat.
+
+  Ltac destruct_lieoc H e tpre tpost i H' :=
+    destruct H as [e H], H as [tpre H], H as [tpost H], H as [i H], H as [H H'].
+
+  Theorem monotonicity_everywhere : pipeline_leb tc tc' = true.
+  Proof.
+    pose proof (tc_and_tc' t t' tc tc' sbState sbState' Hleb Htc Htc') as Hlength'.
+    pose proof Hleb as Htpre.
+    unfold pipeline_leb in Hleb.
+    rewrite andb_true_iff, Nat.eqb_eq in Hleb.
+    destruct Hleb as [Hlength _].
+
+    destruct (list_is_empty_or_composed _ t) as [Ht | Ht].
+    - apply eq_sym in Hlength.
+      rewrite Ht, length_zero_iff_nil in Hlength.
+      rewrite Ht in Htc.
+      rewrite Hlength in Htc'.
+      compute in Htc, Htc'.
+      now rewrite Htc, Htc'.
+
+    - destruct Ht as [e Ht], Ht as [tpre Ht], Ht as [tpost Ht], Ht as [i Ht], Ht as [Ht Hi].
+      pose proof (list_is_composed instr_kind e d t tpre tpost i Ht Hi t' Hlength) as Hlic.
+      destruct Hlic as [e' Hlic], Hlic as [tpre' Hlic], Hlic as [tpost' Ht'], Ht' as [Ht' Hi'].
+      assert (List.length tpre = List.length tpre') as HHH.
+      now rewrite Hi' in Hi.
+      apply (pipeline_sub_is_leb _ _ tpre tpre' tpost tpost' e e' Hlength HHH Ht Ht') in Htpre.
+      destruct Htpre as [Htpre Htpost], Htpost as [Htpost Hte].
+
+      destruct e eqn:He, e' eqn:He'.
+      destruct s, s0.
+
+      assert (o = o0).
+      admit.
+      Check is_fully_monotonic.
+      admit.
+  Admitted.
+End monotonicity_everywhere.
+
+    (* - rewrite Ht in Hlength. *)
+    (*   simpl in Hlength. *)
+    (*   apply eq_sym in Hlength. *)
+    (*   rewrite length_zero_iff_nil in Hlength. *)
+    (*   now rewrite Hlength, Htcd. *)
+    (* - destruct Htcd as [e Htcd], Htcd as [tpre Htcd], Htcd as [tpost Htcd], Htcd as [i Htcd], Htcd as [Htcd Hi]. *)
+    (* destruct (list_is_empty_or_composed _ tc) as [Htcd | Htcd], (list_is_empty_or_composed _ tc') as [Htcd' | Htcd']; *)
+    (*   match goal with *)
+    (*   | [Ha : _ = [], Hb : (exists _, _) |- _] => *)
+    (*       destruct_lieoc Hb e tpre tpost i Hb'; *)
+    (*         rewrite Ha, Hb, app_length, <- Hb' in Hlength; *)
+    (*         simpl in Hlength; *)
+    (*         lia *)
+    (*   | [_ : _ = [] |- _] => now rewrite Htcd, Htcd' *)
+    (*   | _ => idtac *)
+    (*   end. *)
+    (* destruct_lieoc Htcd e tpre tpost i Htcd_. *)
+    (* destruct Htcd' as [e' Htcd'], Htcd' as [tpre' Htcd'], Htcd' as [tpost' Htcd']. *)
+    (* inversion Htcd'. *)
+    (* exists i in Htcd'. *)
+    (* Check is_fully_monotonic. *)