diff --git a/_CoqProject b/_CoqProject
index cd6ca145b88ab6ad97b83d19aaaa1f530e3f288e..acf17cdb922c3150dc58ad290989d26c0990fff6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,5 @@
-R src/ StoreBuffer
-src/definitions.v
src/utils.v
-src/store_buffer.v
-src/correct_store_buffer.v
+src/modular_definitions.v
+src/fivestage.v
+src/modular_store_buffer.v
diff --git a/src/definitions.v b/src/definitions.v
index 69261dfdd96f094fb165e5c44601c7de295fdbbf..122ca502c4af00283ee818cec3951597ee369f9d 100644
--- a/src/definitions.v
+++ b/src/definitions.v
@@ -3,6 +3,7 @@
(* They may or may not be useful… *)
Require Import Bool List Nat PeanoNat.
+From Coq.Arith Require Import Plus.
Import ListNotations.
(* Basic definitions: opcodes, stages, store buffer state. *)
@@ -12,18 +13,6 @@ Variant opcode :=
Scheme Equality for opcode.
-Definition is_load opc :=
- match opc with
- | Load _ => True
- | Store => False
- end.
-
-Definition is_store opc :=
- match opc with
- | Load _ => False
- | Store => True
- end.
-
Variant stage :=
| Sp
| Lsu
@@ -46,17 +35,7 @@ Definition nstg s opc :=
| _, _ => Sn
end.
-(* Specification for stage comparison. Sp < Lsu < (Lu, Su) < Sn. *)
-Inductive le : stage -> stage -> Prop :=
-| le_refl : forall x, le x x
-| le_trans : forall x y z, le x y -> le y z -> le x z
-| le_Sp_Lsu : le Sp Lsu
-| le_Lsu_Lu : le Lsu Lu
-| le_Lsu_Su : le Lsu Su
-| le_Lu_Sn : le Lu Sn
-| le_Su_Sn : le Su Sn.
-
-(* Should be the same, but with booleans this time. *)
+(* Boolean stage comparison. Sp < Lsu < (Lu, Su) < Sn. *)
Definition leb x y :=
match x, y with
| Sp, _ => true
@@ -70,51 +49,6 @@ Definition leb x y :=
| Su, _ => false
end.
-Ltac destruct_stages :=
- repeat match goal with
- | [ x : stage |- _ ] => destruct x
- end.
-
-(* Prove that le and leb are the same. *)
-Theorem le_iff_leb : forall x y, le x y <-> leb x y = true.
-Proof.
- intros x y.
- split;
- intro H.
-
- (* le implies leb *)
- - induction H;
- destruct_stages;
- (reflexivity || discriminate).
-
- (* leb implies le *)
- - destruct_stages;
- try discriminate;
- eauto using le.
-Qed.
-
-Theorem le_antisym : forall x y, le x y -> le y x -> x = y.
-Proof.
- intros x y H1 H2.
- rewrite le_iff_leb in H1, H2.
- destruct x, y;
- reflexivity || discriminate.
-Qed.
-
-(* nstg yields a better stage. *)
-Theorem nstg_is_leb : forall s o, leb s (nstg s o) = true.
-Proof.
- intros s o.
-
- (* Enumerate all stages *)
- destruct s eqn:Hs;
- match goal with
- (* Trivial for all cases, except Lsu: depends on the opcode *)
- | [ _ : s = Lsu |- _ ] => destruct o; reflexivity
- | _ => reflexivity
- end.
-Qed.
-
Variant sbStateT :=
| Empty
| NotEmpty
@@ -168,205 +102,117 @@ Definition compare_two (e1 e2 : option instr_kind) :=
Lemma compare_two_eq_true : forall e, e <> None -> compare_two e e = true.
Proof.
intros e Hn.
- destruct e.
- - destruct i.
+ destruct e as [i |].
+ - (* e = Some i *)
+ destruct i as [o s].
simpl.
+ (* state_leb s s = true, we have a lemma for this. *)
now rewrite state_leb_eq_true.
- - contradiction.
-Qed.
-
-Definition get_opc (trace : trace_kind) :=
- fst (List.split trace).
-
-Definition get_stg (trace : trace_kind) :=
- fst (List.split (snd (List.split trace))).
-
-Definition get_cyc (trace : trace_kind) :=
- snd (List.split (snd (List.split trace))).
-
-Lemma opc_length : forall t, List.length (get_opc t) = List.length t.
-Proof.
- intro t.
- unfold get_opc.
- apply List.split_length_l.
-Qed.
-
-Lemma stg_length : forall t, List.length (get_stg t) = List.length t.
-Proof.
- intro t.
- unfold get_stg.
- rewrite List.split_length_l.
- apply List.split_length_r.
-Qed.
-
-Lemma cyc_length : forall t, List.length (get_cyc t) = List.length t.
-Proof.
- intro t.
- unfold get_cyc.
- rewrite List.split_length_r.
- apply List.split_length_r.
-Qed.
-
-Lemma kind_is_valid :
- forall t i, i < List.length t -> List.nth_error (get_opc t) i <> None.
-Proof.
- intros t i Hl.
- assert (Hl' := Hl).
- now rewrite <- opc_length, <- (nth_error_Some (get_opc t) i) in Hl.
-Qed.
-
-Lemma stage_is_valid :
- forall t i, i < List.length t -> List.nth_error (get_stg t) i <> None.
-Proof.
- intros t i Hl.
- assert (Hl' := Hl).
- now rewrite <- stg_length, <- (nth_error_Some (get_stg t) i) in Hl.
-Qed.
-
-Lemma cycle_is_valid :
- forall t i, i < List.length t -> List.nth_error (get_cyc t) i <> None.
-Proof.
- intros t i Hl.
- assert (Hl' := Hl).
- now rewrite <- cyc_length, <- (nth_error_Some (get_cyc t) i) in Hl.
-Qed.
-
-Lemma not_some_0_is_some_n :
- forall i t, i < List.length t ->
- List.nth_error (get_cyc t) i <> Some 0 ->
- exists n, List.nth_error (get_cyc t) i = Some n.
-Proof.
- intros i t Hi Hzero.
-
- assert (nth_error (get_cyc t) i <> None) as Hnone.
- - now apply cycle_is_valid.
-
- - destruct nth_error.
- + exists n.
- reflexivity.
- + contradiction.
+ - (* None <> None. *)
+ contradiction.
Qed.
(* Pipeline comparison. *)
+Definition instrs_leb (instrs : (instr_kind * instr_kind)) :=
+ match instrs with
+ | ((_, st1), (_, st2)) => state_leb st1 st2
+ (* | ((o1, st1), (o2, st2)) => opcode_beq o1 o2 && state_leb st1 st2 *)
+ end.
+
Definition pipeline_leb p1 p2 :=
let comb := List.combine p1 p2 in
- Nat.eqb (List.length p1) (List.length p2)
- && List.forallb (fun instrs =>
- match instrs with
- | ((o1, st1), (o2, st2)) => opcode_beq o1 o2 && state_leb st1 st2
- end) comb.
-
-(* Pipeline validity. *)
-Definition single_in_stage trace st :=
- List.count_occ stage_eq_dec (get_stg trace) st <=? 1.
-
-Definition check_latencies trace :=
- List.forallb (fun (elt : instr_kind) =>
- match elt with
- | (_, (_, 0))
- | (_, (Lu, S _)) => true
- | (_, (_, S _)) => false
- end) trace.
-
-Definition check_loads_and_stores trace :=
- List.forallb (fun (elt : instr_kind) =>
- match elt with
- | (Load _, (Su, _))
- | (Store, (Lu, _)) => false
- | _ => true
- end) trace.
-
-Lemma check_latencies_is_correct_v0 :
- forall t t1 t2, t = t1 ++ t2 ->
- check_latencies t = (check_latencies t1 && check_latencies t2).
-Proof.
- intros t t1 t2 Ht.
- unfold check_latencies.
- rewrite Ht.
- apply forallb_app.
-Qed.
-
-Lemma check_loads_and_stores_is_correct_v0 :
- forall t t1 t2, t = t1 ++ t2 ->
- check_loads_and_stores t = (check_loads_and_stores t1 && check_loads_and_stores t2).
-Proof.
- intros t t1 t2 Ht.
- unfold check_loads_and_stores.
- rewrite Ht.
- apply forallb_app.
-Qed.
-
-Section check_correctness.
- Variable t t1 t2 tstep : trace_kind.
- Variable e : instr_kind.
- Variable opc : opcode.
- Variable lat : nat.
-
- Hypothesis Ht : t = t1 ++ e :: t2.
- Hypothesis Htstep : tstep = e :: t2.
-
- Lemma check_latencies_is_correct_v1 :
- e = (opc, (Lu, lat)) -> check_latencies t = (check_latencies t1 && check_latencies t2).
- Proof.
- intro He.
-
- rewrite <- Htstep in Ht.
- rewrite (check_latencies_is_correct_v0 _ t1 tstep).
- - rewrite (check_latencies_is_correct_v0 tstep [e] t2).
- + rewrite He.
- now destruct lat.
- + exact Htstep.
- - exact Ht.
+ Nat.eqb (List.length p1) (List.length p2) && List.forallb instrs_leb comb.
+
+Section pipeline_comparison.
+ Variable t t' : trace_kind.
+ Variable i : nat.
+ Variable d : instr_kind.
+
+ Hypothesis Hct : compare_two (List.nth_error t i) (List.nth_error t' i) = true.
+
+ Lemma compare_two_true_means_exists :
+ (exists e, List.nth_error t i = Some e)
+ /\ (exists e, List.nth_error t' i = Some e).
+ split.
+ - (* First case. *)
+ destruct (nth_error t _).
+ + now exists i0. (* Some i0 = Some e -> i0 = e. *)
+ + discriminate. (* compare_two None ... = true is a contradiction. *)
+
+ - (* Second case. *)
+ destruct (nth_error t' _).
+ + now exists i0. (* Some i0 = Some e -> i0 = e. *)
+ + (* compare_two ... None = true is a contradiction, with extra steps. *)
+ destruct (nth_error t _).
+ * simpl in Hct.
+ destruct i0.
+ discriminate.
+ * discriminate.
Qed.
- Lemma check_latencies_is_correct_v2 :
- forall stage n, stage <> Lu -> e = (opc, (stage, S n)) -> check_latencies t = false.
+ Lemma compare_two_true_means_instrs_leb :
+ instrs_leb (List.nth i t d, List.nth i t' d) = true.
Proof.
- intros stage n Hs He.
-
- rewrite <- Htstep in Ht.
- rewrite (check_latencies_is_correct_v0 _ t1 tstep).
- - rewrite (check_latencies_is_correct_v0 tstep [e] t2).
- + rewrite He.
- destruct stage;
- contradiction || (rewrite andb_comm; apply andb_false_l).
- + exact Htstep.
- - exact Ht.
- Qed.
+ destruct compare_two_true_means_exists as [Hec Hec'].
+ destruct Hec as [ec Hnth], Hec' as [ec' Hnth'].
+ rewrite Hnth, Hnth' in Hct.
- Lemma check_loads_and_stores_is_correct_v1 :
- forall n, e = (Load n, (Su, lat)) -> check_loads_and_stores t = false.
- Proof.
- intros n He.
-
- rewrite <- Htstep in Ht.
- rewrite (check_loads_and_stores_is_correct_v0 t t1 tstep).
- - rewrite (check_loads_and_stores_is_correct_v0 tstep [e] t2).
- + now rewrite He, andb_comm.
- + exact Htstep.
- - exact Ht.
+ now rewrite (nth_error_nth t i d Hnth), (nth_error_nth t' i d Hnth').
Qed.
-
- Lemma check_loads_and_stores_is_correct_v2 :
- e = (Store, (Lu, lat)) -> check_loads_and_stores t = false.
- Proof.
- intro He.
-
- rewrite <- Htstep in Ht.
- rewrite (check_loads_and_stores_is_correct_v0 t t1 tstep).
- - rewrite (check_loads_and_stores_is_correct_v0 tstep [e] t2).
- + now rewrite He, andb_comm.
- + exact Htstep.
- - exact Ht.
- Qed.
-End check_correctness.
-
-Definition valid trace :=
- single_in_stage trace Lsu
- && single_in_stage trace Lu
- && single_in_stage trace Su
- && check_latencies trace
- && check_loads_and_stores trace.
+End pipeline_comparison.
+
+Lemma combine_app :
+ forall (A B : Type) (l1 l2 : list A) (l1' l2' : list B),
+ length l1 = length l1' ->
+ combine (l1 ++ l2) (l1' ++ l2') = combine l1 l1' ++ combine l2 l2'.
+Proof.
+ intros A B l1 l2.
+
+ induction l1 as [| a l1 IHl1];
+ destruct l1'.
+ - reflexivity.
+ - discriminate.
+ - discriminate.
+ - simpl.
+ intros l2' Hlength.
+ rewrite IHl1.
+ + reflexivity.
+ + now apply eq_add_S.
+Qed.
+
+Lemma pipeline_sub_is_leb :
+ forall (t t' tpre tpre' tpost tpost' : trace_kind) (e e' : instr_kind),
+ List.length t = List.length t' -> List.length tpre = List.length tpre' ->
+ t = tpre ++ e :: tpost -> t' = tpre' ++ e' :: tpost' ->
+ pipeline_leb t t' = true ->
+ pipeline_leb tpre tpre' = true /\ pipeline_leb tpost tpost' = true /\
+ (let (_, st1) := e in let (_, st2) := e' in state_leb st1 st2) = true.
+Proof.
+ intros t t' tpre tpre' tpost tpost' e e' Hlength Hlength' Ht Ht' Hleb.
+
+ unfold pipeline_leb in Hleb |- *.
+ rewrite andb_true_iff, Nat.eqb_eq in Hleb |- *.
+ destruct Hleb as [_ Hforall].
+ rewrite Ht, Ht', combine_app, forallb_app, andb_true_iff in Hforall;
+ [| exact Hlength'].
+
+ destruct Hforall as [Hfpre Hfpost].
+ simpl in Hfpost.
+ rewrite andb_true_iff in Hfpost.
+ destruct Hfpost as [He Hfpost].
+
+ split.
+ - now split.
+ - rewrite andb_true_iff, Nat.eqb_eq.
+ split;
+ try split;
+ try assumption.
+
+ rewrite Ht, Ht', app_length, app_length, Hlength' in Hlength.
+ apply plus_reg_l in Hlength.
+ simpl in Hlength.
+ auto.
+Qed.
(* Helper functions, may be useful to all implementations. *)
(* Check if an instruction is in a stage. *)
@@ -376,8 +222,6 @@ Definition is_in_stage st (instr : instr_kind) :=
end.
(* Ready-to-use functions. *)
-Definition is_in_lsu := is_in_stage Lsu.
-Definition is_in_lu := is_in_stage Lu.
Definition is_in_su := is_in_stage Su.
Definition get_instr_in_stage trace st := List.find (is_in_stage st) trace.
diff --git a/src/fivestage.v b/src/fivestage.v
new file mode 100644
index 0000000000000000000000000000000000000000..5926e9f6cc7e73ed41caf1bc2a9801bef72234fb
--- /dev/null
+++ b/src/fivestage.v
@@ -0,0 +1,423 @@
+Require Import Bool Lia List Nat PeanoNat.
+From StoreBuffer Require Import utils modular_definitions.
+Import ListNotations.
+
+Module FiveStageSig <: Sig.
+ Variant opcode_fs :=
+ | Load (dlat : nat) (id : nat)
+ | Store (id : nat)
+ | Other (id : nat).
+
+ Variant stage_fs :=
+ | Pre
+ | Ex
+ | Mem
+ | Wb
+ | Post.
+
+ Definition first_stage := Pre.
+
+ Scheme Equality for opcode_fs.
+ Definition opcode := opcode_fs.
+ Definition opcode_beq := opcode_fs_beq.
+ Definition opcode_eq_dec := opcode_fs_eq_dec.
+
+ Scheme Equality for stage_fs.
+ Definition stage := stage_fs.
+ Definition stage_beq := stage_fs_beq.
+ Definition stage_eq_dec := stage_fs_eq_dec.
+
+ Lemma stage_beq_eq_true : forall s, stage_beq s s = true.
+ Proof.
+ now destruct s.
+ Qed.
+
+ (* Boolean stage comparison. Pre < Ex < Mem < Wb < Post. *)
+ Definition leb x y :=
+ match x, y with
+ | Pre, _ => true
+ | Ex, Pre => false
+ | Ex, _ => true
+ | Mem, Pre => false
+ | Mem, Ex => false
+ | Mem, _ => true
+ | Wb, Wb => true
+ | Wb, Post => true
+ | Wb, _ => false
+ | Post, Post => true
+ | Post, _ => false
+ end.
+End FiveStageSig.
+
+Module FiveStage := Pipeline FiveStageSig.
+Export FiveStage.
+
+Definition nstg s :=
+ match s with
+ | Pre => Ex
+ | Ex => Mem
+ | Mem => Wb
+ | _ => Post
+ end.
+
+Definition busFree := sbStateT_beq Empty.
+
+(* ready, free, and cycle functions. *)
+Definition ready next_id sbState (elt : instr_kind) :=
+ match elt with
+ | (_, (_, S _)) => false
+ | (Store _, (Mem, 0)) => negb (sbStateT_beq Full sbState)
+ | (Load _ _, (Ex, 0)) => busFree sbState
+ | (opc, (Pre, 0)) => idx opc =? next_id
+ | _ => true
+ end.
+
+Definition memFree next_id sbState trace :=
+ let instr := get_instr_in_stage trace Mem in
+ match instr with
+ | Some elt => ready next_id sbState elt
+ | None => true
+ end.
+
+Definition exFree next_id sbState trace :=
+ let instr := get_instr_in_stage trace Ex in
+ match instr with
+ | Some elt => ready next_id sbState elt && memFree next_id sbState trace
+ | None => true
+ end.
+
+Definition free next_id sbState trace (elt : instr_kind) :=
+ let (opc, state) := elt in
+ let (st, _) := state in
+ match nstg st with
+ | Mem => memFree next_id sbState trace
+ | Ex => exFree next_id sbState trace
+ | _ => true
+ end.
+
+Definition get_latency opc st :=
+ match opc, st with
+ | Load n _, Mem => n
+ | _, _ => 0
+ end.
+
+Definition cycle_elt next_id sbState trace elt :=
+ match elt with
+ | (opc, (st, S n)) => (opc, (st, n))
+ | (opc, (st, 0)) =>
+ if ready next_id sbState elt && free next_id sbState trace elt then
+ let nstg := nstg st in
+ (opc, (nstg, get_latency opc nstg))
+ else
+ elt
+ end.
+
+Definition cycle sbState trace :=
+ List.map (cycle_elt (next_id trace) sbState trace) trace.
+
+Definition legal_sb_transitions st sbState sbState' :=
+ match st, sbState with
+ | Mem, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
+ | Mem, Empty => sbState' = Empty
+ | _, _ => sbState' = Full \/ sbState' = NotEmpty \/ sbState' = Empty
+ end.
+
+Lemma next_stage_is_higher : forall opc st st',
+ st' = nstg st ->
+ compare_two (Some (opc, (st, 0)))
+ (Some (opc, (st', get_latency opc st'))) = true.
+Proof.
+ intros opc st st' Hst'.
+ rewrite Hst'.
+ now destruct st;
+ [..| destruct opc].
+Qed.
+
+Lemma opc_match_case_identical : forall (A : Type) (a : A) opc,
+ match opc with | Load _ _ | _ => a end = a.
+Proof.
+ intros A a opc.
+ now destruct opc.
+Qed.
+
+Section monotonicity.
+ Variable opc : opcode.
+ Variable d : instr_kind.
+ Variable st st' : stage.
+ Variable t tpre tpost t' tpre' tpost' tc tc' : trace_kind.
+ Variable sbState sbState' : sbStateT.
+
+ Hypothesis Hleb : pipeline_leb t t' = true.
+ 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 HnId : next_id t <= next_id t'.
+
+ Hypothesis HnIdLow : forall t (e : instr_kind),
+ match e with
+ | (opc, (st, _)) => idx opc < next_id t <-> st <> Pre
+ end.
+ Hypothesis HnIdHigh : forall t (e : instr_kind),
+ match e with
+ | (opc, (st, _)) => idx opc >= next_id t <-> st = Pre
+ end.
+
+ Hypothesis HfreePersists :
+ forall (st : stage), free (next_id t) sbState t (opc, (st, 0)) = true ->
+ free (next_id t') sbState' t' (opc, (st, 0)) = true.
+
+ Hypothesis HbusFree :
+ forall st, st = Ex -> busFree sbState = true -> busFree sbState' = true.
+
+ Hypothesis HvalidLat : forall (e : instr_kind),
+ match e with
+ | (_, (st, 0)) => True
+ | (Load dlat _, (st, n)) => st = Mem /\ n <= dlat
+ | (_, (st, S _)) => False
+ end.
+
+ 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 type of He' with
+ | e = e' =>
+ rewrite Ht', <- He' in HfreePersists, HnId |- *
+ | 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 type of He' 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, n)) ->
+ List.nth_error tc' i = Some (opc, (nstg st, n)).
+ Proof.
+ intros He He' n.
+ specialize (HfreePersists st).
+ specialize (HbusFree st).
+ specialize (HnIdLow t' e').
+ specialize (HnIdHigh t' e').
+
+ rewrite Ht', <- He' in HnIdLow, HnIdHigh.
+
+ (* Delve onto e, then handle stages on a case-by-case basis. *)
+ work_on_e He'.
+ destruct st;
+ (* Solve Wb and Post automatically. *)
+ [..| auto | auto].
+
+ (* Pre. *)
+ - destruct free.
+ + destruct free;
+ [| now discriminate HfreePersists].
+
+ simpl.
+ repeat rewrite opc_match_case_identical.
+
+ destruct (_ =? _) eqn:Hidx.
+ * rewrite Nat.eqb_eq in Hidx.
+ rewrite <- Hidx in HnId.
+ destruct HnIdHigh as [_ HnIdHigh'].
+ pose proof (n_le_he_eq _ _ HnId (HnIdHigh' eq_refl)) as HnIdEq.
+ rewrite <- Nat.eqb_eq in HnIdEq.
+ now rewrite HnIdEq.
+ * discriminate.
+
+ (* + (* Ex is free in t. *) *)
+ (* now destruct (free _ _ _) in HfreePersists |- *; *)
+ (* [| discriminate HfreePersists]. *)
+ + rewrite andb_false_r.
+ discriminate.
+
+ (* Ex. *)
+ - destruct free.
+ + (* Case where e can progress in t. *)
+ rewrite (HfreePersists eq_refl).
+ destruct opc;
+ (* Stores and others are trivial. *)
+ [| auto..].
+
+ (* Loads *)
+ unfold ready.
+ destruct busFree.
+ * now rewrite HbusFree.
+ * discriminate.
+
+ + (* Case where e cannot progress in t. *)
+ (* This is irrelevant, eliminate it. *)
+ rewrite andb_false_r.
+ discriminate.
+
+ (* Mem. *)
+ - now destruct opc; [
+ (* Loads and stores are trivial; stores are trickier. *)
+ | destruct sbState, sbState', Hlsbt;
+ try discriminate |].
+ 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 (_ && _).
+ + (* If e (in t) can progress. *)
+ (* e' (in t') can progress to. We have a lemma for this. *)
+ rewrite (Huca eq_refl eq_refl (get_latency opc (nstg st)) eq_refl).
+ now apply compare_two_eq_true.
+
+ + (* If e (in t) cannot progress. *)
+ destruct (_ && _).
+ * now apply next_stage_is_higher.
+ * 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.
+ clear HfreePersists Hlsbt.
+
+ (* Goal transformation: show exactly how e and e' are modified by the
+ * cycle function. *)
+ work_on_e Hed.
+
+ destruct st, st';
+ try contradiction;
+ try discriminate;
+ destruct (_ && _);
+ match goal with
+ | [|- context[if ?X then _ else _]] =>
+ now destruct X
+ | [|- context[get_latency ?opc _]] =>
+ now destruct opc
+ | _ =>
+ reflexivity
+ end.
+ 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.
+ clear HfreePersists Hlsbt.
+
+ pose proof (HvalidLat e') as HvalidLat'.
+ specialize (HvalidLat e).
+
+ rewrite He in HvalidLat.
+ rewrite He' in HvalidLat'.
+
+ destruct n, n'; [
+ now apply moved_no_lat_is_monotonic |
+ work_on_e Hed;
+ destruct opc;
+ [| contradiction..]..
+ ].
+
+ (* From there, opc = Load. *)
+ - (* n = 0 and n' <> 0. *)
+ destruct HvalidLat' as [Hst' Hn'].
+ rewrite Hst' in Hsl, Hed |- *.
+ destruct st;
+ try discriminate.
+ + now destruct (_ && _).
+ + destruct (_ && _).
+ * simpl.
+ rewrite Nat.leb_le.
+ lia.
+ * reflexivity.
+
+ - (* n <> 0 and n' = 0. *)
+ destruct HvalidLat as [Hst _].
+ rewrite Hst in Hsl, Hed |- *.
+ destruct st';
+ discriminate || reflexivity.
+
+ - (* n and n' <> 0. *)
+ exact Hsl.
+ 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.
+
+ Let tc_and_tc' :=
+ tc_tc'_length_eq (cycle_elt (next_id t) sbState t) (cycle_elt (next_id t') sbState' t')
+ t t' tc tc' Hleb Htc Htc'.
+
+ Variable e e' : instr_kind.
+ Variable n n' : nat.
+
+ 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 He : e = (opc, (st, n)).
+ Hypothesis He' : e' = (opc, (st', n')).
+ Hypothesis Hsl : state_leb (st, n) (st', n') = true.
+
+ Let is_monotonic' ni :=
+ is_monotonic e e' ni Ht Ht' (Hi ni) (Hi' ni) n n' He He' Hsl.
+
+ Let cycled_instrs_are_leb' :=
+ cycled_instrs_are_leb d tc tc' is_monotonic' tc_and_tc'.
+
+ Theorem is_fully_monotonic : pipeline_leb tc tc' = true.
+ Proof.
+ now apply is_pipeline_fully_monotonic.
+ Qed.
+End monotonicity.
diff --git a/src/modular_definitions.v b/src/modular_definitions.v
new file mode 100644
index 0000000000000000000000000000000000000000..bbe116a6ecaffca4e20f9dc461828ddc5097a373
--- /dev/null
+++ b/src/modular_definitions.v
@@ -0,0 +1,204 @@
+Require Import Bool List Nat PeanoNat.
+Import ListNotations.
+
+Module Type Sig.
+ Parameter opcode : Set.
+ Axiom opcode_beq : opcode -> opcode -> bool.
+ Axiom opcode_eq_dec : forall (o o' : opcode), {o = o'} + {o <> o'}.
+
+ Parameter stage : Set.
+ Axiom first_stage : stage.
+ Axiom stage_beq : stage -> stage -> bool.
+ Axiom stage_eq_dec : forall (s s' : stage), {s = s'} + {s <> s'}.
+ Axiom stage_beq_eq_true : forall s, stage_beq s s = true.
+
+ Axiom leb : stage -> stage -> bool.
+ Axiom idx : opcode -> nat.
+End Sig.
+
+Module Pipeline (Def : Sig).
+ Import Def.
+ Export Def.
+
+ Definition state := (stage * nat)%type.
+ Definition instr_kind := (opcode * state)%type.
+ Definition trace_kind := list instr_kind.
+
+ Definition is_in_stage st (instr : instr_kind) :=
+ match instr with
+ | (_, (st', _)) => stage_beq st st'
+ end.
+
+ Definition get_instr_in_stage trace st := List.find (is_in_stage st) trace.
+
+ Definition state_leb st1 st2 :=
+ match st1, st2 with
+ | (s1, n1), (s2, n2) =>
+ if stage_beq s1 s2 then
+ Nat.leb n2 n1
+ else
+ leb s1 s2
+ end.
+
+ Definition next_id (trace : trace_kind) :=
+ match trace with
+ | [] => 0
+ | (opc, _) :: r =>
+ let id := idx opc in
+ List.fold_left (fun cid (elt : instr_kind) =>
+ let (opc, st) := elt in
+ let (s, _) := st in
+ if stage_beq s first_stage then
+ Nat.min cid (idx opc)
+ else
+ cid) r id
+ end.
+
+ Lemma state_leb_eq_true : forall st, state_leb st st = true.
+ Proof.
+ intro st.
+ destruct st.
+ simpl.
+ now rewrite stage_beq_eq_true, Nat.leb_le.
+ Qed.
+
+ Lemma instr_kind_is_comparable : forall (e e' : instr_kind), {e = e'} + {e <> e'}.
+ Proof.
+ repeat decide equality.
+ - apply stage_eq_dec.
+ - apply opcode_eq_dec.
+ Qed.
+
+ Definition compare_two (e1 e2 : option instr_kind) :=
+ match e1, e2 with
+ | None, _
+ | _, None => false
+ | Some (_, st1), Some (_, st2) => state_leb st1 st2
+ end.
+
+ Lemma compare_two_eq_true : forall e, e <> None -> compare_two e e = true.
+ Proof.
+ intros e Hn.
+ destruct e as [[o s] |].
+ - (* e = Some (o, s) *)
+ simpl.
+ now rewrite state_leb_eq_true.
+ - (* None <> None *)
+ contradiction.
+ Qed.
+
+ Definition instrs_leb (instrs : (instr_kind * instr_kind)) :=
+ match instrs with
+ | ((_, st1), (_, st2)) => state_leb st1 st2
+ end.
+
+ Definition pipeline_leb p1 p2 :=
+ let comb := List.combine p1 p2 in
+ Nat.eqb (List.length p1) (List.length p2) && List.forallb instrs_leb comb.
+
+ Section comparison.
+ Variable t t' : trace_kind.
+ Variable i : nat.
+ Variable d : instr_kind.
+
+ Hypothesis Hct : compare_two (List.nth_error t i) (List.nth_error t' i) = true.
+
+ Lemma compare_two_true_means_exists :
+ (exists e, List.nth_error t i = Some e)
+ /\ (exists e, List.nth_error t' i = Some e).
+ split.
+ - (* First case. *)
+ destruct (nth_error t _).
+ + now exists i0. (* Some i0 = Some e -> i0 = e. *)
+ + discriminate. (* compare_two None ... = true is a contradiction. *)
+
+ - (* Second case. *)
+ destruct (nth_error t' _).
+ + now exists i0. (* Some i0 = Some e -> i0 = e. *)
+ + (* compare_two ... None = true is a contradiction, with extra steps. *)
+ destruct (nth_error t _).
+ * simpl in Hct.
+ destruct i0.
+ discriminate.
+ * discriminate.
+ Qed.
+
+ Lemma compare_two_true_means_instrs_leb :
+ instrs_leb (List.nth i t d, List.nth i t' d) = true.
+ Proof.
+ destruct compare_two_true_means_exists as [Hec Hec'].
+ destruct Hec as [ec Hnth], Hec' as [ec' Hnth'].
+ rewrite Hnth, Hnth' in Hct.
+
+ now rewrite (nth_error_nth t i d Hnth), (nth_error_nth t' i d Hnth').
+ Qed.
+ End comparison.
+
+ Lemma tc_tc'_length_eq :
+ forall (f f' : instr_kind -> instr_kind) (t t' tc tc' : trace_kind),
+ pipeline_leb t t' = true ->
+ tc = map f t -> tc' = map f' t' -> length tc = length tc'.
+ Proof.
+ intros f f' t t' tc tc' Hleb Htc Htc'.
+
+ (* length t = length t'. *)
+ (* length (map ... t) = length t. *)
+ rewrite Htc, Htc'.
+ repeat rewrite map_length.
+ unfold pipeline_leb in Hleb.
+ now rewrite andb_true_iff, Nat.eqb_eq in Hleb.
+ Qed.
+
+ Lemma cycled_instrs_are_leb :
+ forall (d : instr_kind) (tc tc' : trace_kind),
+ (forall i, compare_two (nth_error tc i) (nth_error tc' i) = true) ->
+ List.length tc = List.length tc' ->
+ 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 d tc tc' Hct Hlength instrs HIn.
+ destruct (In_nth (combine tc tc') instrs (d, d) HIn) as [i [Hil HInth]].
+
+ (* since nth i (combine tc tc') = instrs,
+ * instrs = (nth i tc d, nth i tc' d). *)
+ rewrite combine_nth in HInth.
+ - (* 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 <- HInth.
+ apply (compare_two_true_means_instrs_leb tc tc' i d), (Hct i).
+ - exact Hlength.
+ Qed.
+
+ Lemma is_pipeline_fully_monotonic :
+ forall (tc tc' : trace_kind),
+ List.length tc = List.length tc' ->
+ (forall instrs, In instrs (combine tc tc') -> instrs_leb instrs = true) ->
+ pipeline_leb tc tc' = true.
+ Proof.
+ intros tc tc' Hlength Hleb.
+
+ unfold pipeline_leb.
+ rewrite andb_true_iff.
+ now split; [
+ (* First, length tc = length tc'. We have a hypothesis for this. *)
+ rewrite Nat.eqb_eq |
+ (* Now, forallb instrs_leb (combine tc tc') = true. *)
+ (* Transform the goal into
+ * forall instrs, In instrs (combine ...) -> instrs_leb instrs = true.
+ * Directly apply Hleb. *)
+ rewrite forallb_forall
+ ].
+ Qed.
+End Pipeline.
+
+Variant sbStateT :=
+ | Empty
+ | NotEmpty
+ | Full.
+
+Scheme Equality for sbStateT.
diff --git a/src/modular_store_buffer.v b/src/modular_store_buffer.v
new file mode 100644
index 0000000000000000000000000000000000000000..6fe24efa33dd5b90b5bd28bab0af2108266f9b6f
--- /dev/null
+++ b/src/modular_store_buffer.v
@@ -0,0 +1,512 @@
+Require Import Bool Lia List Nat PeanoNat.
+From StoreBuffer Require Import modular_definitions utils.
+Import ListNotations.
+
+Module StoreBufferSig <: Sig.
+ Variant opcode_sb :=
+ | Load (dlat : nat) (id : nat)
+ | Store (id : nat).
+
+ Variant stage_sb :=
+ | Sp
+ | Lsu
+ | Lu
+ | Su
+ | Sn.
+
+ Definition first_stage := Sp.
+
+ Scheme Equality for opcode_sb.
+ Definition opcode := opcode_sb.
+ Definition opcode_beq := opcode_sb_beq.
+ Definition opcode_eq_dec := opcode_sb_eq_dec.
+
+ Scheme Equality for stage_sb.
+ Definition stage := stage_sb.
+ Definition stage_beq := stage_sb_beq.
+ Definition stage_eq_dec := stage_sb_eq_dec.
+
+ Lemma stage_beq_eq_true : forall s, stage_beq s s = true.
+ Proof.
+ now destruct s.
+ Qed.
+
+ (* Boolean stage comparison. Sp < Lsu < (Lu, Su) < Sn. *)
+ Definition leb x y :=
+ match x, y with
+ | Sp, _ => true
+ | _, Sn => true
+ | Sn, _ => false
+ | Lsu, Sp => false
+ | Lsu, _ => true
+ | Lu, Lu => true
+ | Lu, _ => false
+ | Su, Su => true
+ | Su, _ => false
+ end.
+
+ Definition idx opc :=
+ match opc with
+ | Load _ id | Store id => id
+ end.
+End StoreBufferSig.
+
+Module StoreBuffer := Pipeline StoreBufferSig.
+Export StoreBuffer.
+
+Definition nstg s opc :=
+ match s, opc with
+ | Sp, _ => Lsu
+ | Lsu, Load _ _ => Lu
+ | Lsu, Store _ => Su
+ | _, _ => Sn
+ end.
+
+Definition sbEmpty := sbStateT_beq Empty.
+
+(* ready, free and cycle functions. *)
+Definition ready next_id sbState (elt : instr_kind) :=
+ match elt with
+ | (Load _ _, (Lsu, _)) => sbEmpty sbState
+ | (_, (Su, _)) => negb (sbStateT_beq sbState Full)
+ | (_, (Lu, S _)) => false
+ | (opc, (Sp, 0)) => idx opc =? next_id
+ | _ => true
+ end.
+
+Definition luFree next_id sbState trace :=
+ let instr := get_instr_in_stage trace Lu in
+ match instr with
+ | Some elt => ready next_id sbState elt (* Sn is always free *)
+ | None => true
+ end.
+
+Definition suFree next_id sbState trace :=
+ let instr := get_instr_in_stage trace Su in
+ match instr with
+ | Some elt => ready next_id sbState elt (* Sn is always free *)
+ | None => true
+ end.
+
+Definition lsuFree next_id sbState trace :=
+ let instr := get_instr_in_stage trace Lsu in
+ match instr with
+ | Some (opcode, (stg, lat)) => ready next_id sbState (opcode, (stg, lat)) &&
+ if stage_beq (nstg stg opcode) Lu then
+ luFree next_id sbState trace
+ else
+ suFree next_id sbState trace
+ | None => true
+ end.
+
+Definition free next_id sbState trace (elt : instr_kind) :=
+ let (opc, state) := elt in
+ let (st, _) := state in
+ match nstg st opc with
+ | Lu => luFree next_id sbState trace
+ | Su => suFree next_id sbState trace
+ | Lsu => lsuFree next_id sbState trace
+ | _ => true
+ end.
+
+Definition get_latency opc st :=
+ match opc, st with
+ | Load n _, Lu => n
+ | _, _ => 0
+ end.
+
+Definition cycle_elt next_id (busTaken : bool) sbState trace elt :=
+ match elt with
+ | (opc, (st, S n)) =>
+ if busTaken then
+ (opc, (st, n))
+ else
+ elt
+ | (opc, (st, 0)) =>
+ if ready next_id sbState elt && free next_id sbState trace elt then
+ let nstg := nstg st opc in
+ (opc, (nstg, get_latency opc nstg))
+ else
+ elt
+ end.
+
+Definition cycle sbState busTaken trace :=
+ List.map (cycle_elt (next_id trace) busTaken sbState trace) trace.
+
+Definition legal_sb_transitions st sbState sbState' :=
+ match st, sbState with
+ | Su, Empty => sbState' = Empty
+ | Su, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
+ | _, _ => sbState' = Full \/ sbState' = NotEmpty \/ sbState' = Empty
+ end.
+
+Lemma next_stage_is_higher :
+ forall opc st st', st' = nstg st opc ->
+ compare_two (Some (opc, (st, 0)))
+ (Some (opc, (st', get_latency opc st'))) = true.
+Proof.
+ intros opc st st' Hst'.
+ rewrite Hst'.
+ destruct st;
+ try reflexivity;
+ now destruct opc.
+Qed.
+
+Lemma opc_match_case_identical : forall (A : Type) (a : A) opc,
+ match opc with | Load _ _ | _ => a end = a.
+Proof.
+ intros A a opc.
+ now destruct opc.
+Qed.
+
+Section monotonicity.
+ Variable opc : opcode.
+ Variable d : instr_kind.
+ Variable st st' : stage.
+ Variable t tpre tpost t' tpre' tpost' tc tc' : trace_kind.
+ Variable busTaken busTaken' : bool.
+ Variable sbState sbState' : sbStateT.
+
+ Hypothesis Hleb : pipeline_leb t t' = true.
+ Hypothesis Hl : pipeline_leb tpre tpre' = true.
+ Hypothesis Hl' : pipeline_leb tpost tpost' = true.
+ Hypothesis Htc : tc = cycle sbState busTaken t.
+ Hypothesis Htc' : tc' = cycle sbState' busTaken' t'.
+ Hypothesis Hlsbt : legal_sb_transitions st sbState sbState'.
+ Hypothesis HnId : next_id t <= next_id t'.
+
+ Hypothesis HnIdLow : forall t (e : instr_kind),
+ match e with
+ | (opc, (st, _)) => idx opc < next_id t <-> st <> Sp
+ end.
+
+ Hypothesis HnIdHigh : forall t (e : instr_kind),
+ match e with
+ | (opc, (st, _)) => idx opc >= next_id t <-> st = Sp
+ end.
+
+ Hypothesis Hlu : forall st opc n, st = Lu -> exists id, opc = Load n id.
+ Hypothesis Hsu : forall st opc, st = Su -> exists id, opc = Store id.
+
+ (* Long hypotheses related to stage occupation. *)
+ Hypothesis HfreeLsuPersists :
+ free (next_id t) sbState t (opc, (Sp, 0)) = true ->
+ free (next_id t') sbState' t' (opc, (Sp, 0)) = true.
+
+ Hypothesis HfreeFromLsuPersists :
+ free (next_id t) sbState t (opc, (Lsu, 0)) = true ->
+ free (next_id t') sbState' t' (opc, (Lsu, 0)) = true.
+
+ Hypothesis HbusTakenPersists : busTaken = true -> busTaken' = true.
+
+ Hypothesis HsbRemainsEmpty :
+ forall st, st = Lsu -> sbEmpty sbState = true -> sbEmpty sbState' = true.
+
+ Hypothesis HvalidLat : forall (e : instr_kind) (busTaken : bool),
+ match e with
+ | (_, (st, 0)) => True
+ | (Load dlat _, (st, n)) => st = Lu /\ n <= dlat /\ (busTaken = false -> n = dlat)
+ | (_, (st, S _)) => False
+ end.
+
+ 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 type of He' with
+ | e = e' =>
+ rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HnId |- *
+ | 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 type of He' with
+ | e = e' =>
+ subst e
+ | e <> e' =>
+ rewrite <- Ht';
+ subst e;
+ subst e'
+ end.
+
+ Ltac stage_opc Hyp :=
+ destruct (Hyp eq_refl) as [sopc_internal_id sopc_internal_Hopc];
+ (discriminate sopc_internal_Hopc ||
+ rewrite sopc_internal_Hopc;
+ auto).
+
+ 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 (HsbRemainsEmpty st).
+ specialize (HnIdLow t' e').
+ specialize (HnIdHigh t' e').
+
+ rewrite Ht', <- He' in HnIdLow, HnIdHigh.
+
+ (* 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 in HfreeLsuPersists |- *.
+ + (* LSU is free in t. *)
+ setoid_rewrite (HfreeLsuPersists eq_refl).
+ unfold ready.
+ repeat rewrite opc_match_case_identical.
+
+ destruct (_ =? _) eqn:Hidx.
+ * rewrite Nat.eqb_eq in Hidx.
+ rewrite <- Hidx in HnId.
+ destruct HnIdHigh as [_ HnIdHigh'].
+ pose proof (n_le_he_eq _ _ HnId (HnIdHigh' eq_refl)) as HnIdEq.
+ rewrite <- Nat.eqb_eq in HnIdEq.
+ now rewrite HnIdEq.
+ * discriminate.
+
+ + (* LSU is not free in t: this is irrelevant. *)
+ rewrite andb_false_r.
+ discriminate.
+
+ (* Lsu *)
+ - destruct free, opc.
+ (* Cases where e progressed in t. *)
+ + (* Loads *)
+ unfold ready.
+ destruct sbEmpty.
+ * simpl in HfreeFromLsuPersists |- *.
+ now rewrite HsbRemainsEmpty, HfreeFromLsuPersists.
+ * discriminate.
+ + (* Stores *)
+ simpl in HfreeFromLsuPersists |- *.
+ now rewrite HfreeFromLsuPersists.
+
+ (* Cases where e did not progress in t. *)
+ (* Irrelevant, exclude them. *)
+ + rewrite andb_false_r.
+ discriminate.
+ + discriminate.
+
+ (* Lu: instructions without latency (this is the case here) move to Sn. *)
+ - stage_opc (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. *)
+ - stage_opc Hsu.
+ now 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 (_ && _).
+ + (* If e (in t) can progress. *)
+ (* e' (in t') can progress to. We have a lemma for this. *)
+ rewrite (Huca eq_refl eq_refl (get_latency _ _) eq_refl).
+ now 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 apply next_stage_is_higher.
+ * (* 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. *)
+ destruct busTaken.
+ + rewrite (HbusTakenPersists eq_refl).
+ now apply compare_two_eq_true.
+ + destruct busTaken'.
+ * simpl.
+
+ rewrite stage_beq_eq_true, Nat.leb_le.
+ auto.
+ * 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.
+ clear HfreeFromLsuPersists HfreeLsuPersists Hlsbt.
+ 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 (_ && _), (_ && _), opc.
+ - now destruct (_ && _), opc.
+ - now destruct (_ && _), (_ && _).
+ - now destruct (_ && _), opc.
+
+ (* st = Lsu, st' = Lu, Su, Sn *)
+ - now destruct (_ && _), opc.
+ - destruct (_ && _), (_ && _);
+ try reflexivity;
+ stage_opc Hsu'.
+ - now destruct (_ && _), opc.
+
+ (* st = Lu, st' = Sn *)
+ - (* Trivial when opc = Load, eliminate the case where opc = Store. *)
+ stage_opc Hlu.
+
+ (* st = Su, st' = Sn *)
+ - (* Eliminate the case where opc = Load. *)
+ stage_opc Hsu.
+ (* Either the instruction remains in Su, or it progresses in Sn. *)
+ (* Both cases are trivial. *)
+ now 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.
+ clear HfreeFromLsuPersists HfreeLsuPersists Hlsbt.
+ pose proof (HvalidLat e' busTaken') as HvalidLat'.
+ specialize (HvalidLat e busTaken).
+
+ 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;
+ [| contradiction] ..
+ ].
+
+ (* From there, opc = Load. *)
+ (* n = 0 and n' <> 0. *)
+ - (* st' = Lu. *)
+ destruct HvalidLat' 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 (_ && _), busTaken'.
+ + (* st = Lsu. In this case, the next stage is either Lsu or Lu. *)
+ destruct (_ && _).
+ * simpl.
+ destruct busTaken';
+ rewrite Nat.leb_le;
+ lia.
+ * now destruct busTaken'.
+
+ (* n <> 0 and n' = 0. *)
+ - (* st = Lu. *)
+ destruct HvalidLat 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. *)
+ || now destruct busTaken.
+
+ (* n and n' <> 0. *)
+ - destruct busTaken.
+ + now rewrite HbusTakenPersists.
+ + destruct HvalidLat as [Hst [_ Hdlat]], HvalidLat' as [Hst' [Hlat' Hdlat']].
+ rewrite (Hdlat eq_refl), Hst, Hst' in Hed |- *.
+ destruct busTaken'.
+ * simpl.
+ rewrite Nat.leb_le.
+ lia.
+ * now rewrite Hdlat' in Hed |- *.
+ 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.
+
+ Let tc_and_tc' :=
+ tc_tc'_length_eq (cycle_elt (next_id t) busTaken sbState t)
+ (cycle_elt (next_id t') busTaken' sbState' t')
+ t t' tc tc' Hleb Htc Htc'.
+
+ Variable e e' : instr_kind.
+ Variable n n' : nat.
+
+ 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 He : e = (opc, (st, n)).
+ Hypothesis He' : e' = (opc, (st', n')).
+ Hypothesis Hsl : state_leb (st, n) (st', n') = true.
+
+ Let is_monotonic' ni :=
+ is_monotonic e e' ni Ht Ht' (Hi ni) (Hi' ni) n n' He He' Hsl.
+
+ Let cycled_instrs_are_leb' :=
+ cycled_instrs_are_leb d tc tc' is_monotonic' tc_and_tc'.
+
+ Theorem is_fully_monotonic : pipeline_leb tc tc' = true.
+ Proof.
+ now apply is_pipeline_fully_monotonic.
+ Qed.
+End monotonicity.
diff --git a/src/utils.v b/src/utils.v
index f8244f17f168b773a6b850b9c6441601c0874af3..19d6b321b3303958c444f063f1a75561b5e4ab9e 100644
--- a/src/utils.v
+++ b/src/utils.v
@@ -1,54 +1,85 @@
Require Import Lia List Nat.
Import ListNotations.
-Lemma not_existsb_means_cannot_find :
- forall (T : Type) (f : T -> bool) (l : list T),
- List.existsb f l = false -> List.find f l = None.
+Scheme Equality for list.
+
+Lemma list_elt_exists :
+ forall (A : Type) (l : list A) (d : A) i,
+ i < List.length l -> (exists a, List.nth_error l i = Some a).
Proof.
- intros T f l.
- induction l.
- - reflexivity.
- - simpl.
- now destruct f.
+ intros A l d i Hi.
+ destruct nth_error eqn:Hnth.
+ - now exists a.
+ - pose proof (nth_error_nth' l d Hi) as Hnth'.
+ rewrite Hnth in Hnth'.
+ discriminate.
Qed.
-Lemma nth_error_on_composed_list :
- forall (T : Type) (a d : T) (l lpre lpost : list T) i,
- l = lpre ++ a :: lpost -> i = List.length lpre ->
- List.nth_error l i = Some a.
-Proof.
- intros T a d l lpre lpost i Hl Hi.
+Section list_utils.
+ Variable A B : Type.
+ Variable a d : A.
+ Variable f : A -> B.
+ Variable l lpre lpost : list A.
+ Variable i : nat.
+
+ Hypothesis Hl : l = lpre ++ a :: lpost.
+ Hypothesis Hi : i = List.length lpre.
- assert (i < List.length l) as Hlength.
- - rewrite Hl, app_length, Hi.
+ Lemma i_lt_length_l : i < List.length l.
+ Proof.
+ rewrite Hl, app_length, Hi.
simpl.
lia.
+ Qed.
- - now rewrite (nth_error_nth' _ d Hlength), Hl, Hi, nth_middle.
-Qed.
+ Lemma nth_error_on_composed_list : List.nth_error l i = Some a.
+ Proof.
+ now rewrite (nth_error_nth' _ d i_lt_length_l), Hl, Hi, nth_middle.
+ Qed.
+
+ Lemma map_in_the_middle : List.nth_error (List.map f l) i = Some (f a).
+ Proof.
+ apply map_nth_error, nth_error_on_composed_list.
+ Qed.
+
+ Lemma list_is_composed :
+ forall (l' : list A), List.length l = List.length l' ->
+ (exists a' lpre' lpost', l' = lpre' ++ a' :: lpost' /\ i = List.length lpre').
+ Proof.
+ intros l' Hlength.
-Lemma map_in_the_middle :
- forall (A B : Type) (a d : A) (f : A -> B) l lpre lpost i,
- l = lpre ++ a :: lpost -> i = List.length lpre ->
- List.nth_error (List.map f l) i = Some (f a).
+ pose proof i_lt_length_l as Hlength'.
+ rewrite Hlength in Hlength'.
+
+ pose proof (list_elt_exists A l' d i Hlength') as Hle.
+ destruct Hle as [a' Hle].
+
+ pose proof (nth_error_split l' i Hle) as Hnes.
+ destruct Hnes as [lpre' [lpost' [Hnes Hi']]].
+ exists a', lpre', lpost'.
+ split.
+ - exact Hnes.
+ - now apply eq_sym in Hi'.
+ Qed.
+End list_utils.
+
+Lemma list_is_empty_or_composed :
+ forall (A : Type) (l : list A),
+ l = [] \/ (exists (a : A) (lpre lpost : list A) (i : nat), l = lpre ++ a :: lpost /\ i = List.length lpre).
Proof.
- intros A B a d f l lpre lpost i Hl Hi.
- now apply map_nth_error, (nth_error_on_composed_list _ _ d _ lpre lpost).
+ intros A l.
+
+ induction l.
+ - now left.
+ - right.
+ destruct IHl as [IHl | IHl].
+ + exists a, [], [], 0.
+ now rewrite IHl.
+ + destruct IHl as [a0 [lpre [lpost IHl]]].
+ now exists a, [], l, 0.
Qed.
-Section ListCustomBool.
- Variable A : Type.
- Variable f : A -> bool.
-
- Definition nth_at :=
- let fix aux i (l : list A) {struct l} :=
- match l with
- | [] => None
- | x :: tl =>
- if f x then
- Some i
- else
- aux (S i) tl
- end in
- aux 0.
-End ListCustomBool.
+Lemma n_le_he_eq : forall (n m : nat), n <= m -> n >= m -> n = m.
+Proof.
+ lia.
+Qed.