diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 4616ed4b84e6cd0b67fb9c3336b92f092c2d7067..252ca6ec1fa9b86251c58ab816adcedee9b1ce6c 100644
--- a/src/correct_store_buffer.v
+++ b/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. *)