correct_store_buffer: new store buffer definition

This adds a new store buffer definiton, with more locking than before.
Provided are the ready and free functions, as well as a proof of
no-regression.

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

_CoqProject

@@ -2,3 +2,4 @@
 src/definitions.v
 src/utils.v
 src/store_buffer.v
+src/correct_store_buffer.v

src/correct_store_buffer.v

+Require Import Bool Lia List Nat PeanoNat.
+From StoreBuffer Require Import definitions utils.
+Import ListNotations.
+
+Variant sbStateT :=
+  | Empty
+  | NotEmpty
+  | Full.
+
+Scheme Equality for sbStateT.
+
+(* free and cycle functions. *)
+Definition busFree isSuUsed sbState :=
+  (sbStateT_beq sbState Empty) && (negb isSuUsed).
+
+Definition ready isSuUsed sbState (elt : instr_kind) :=
+  match elt with
+  | (Load, (Lsu, 0)) => busFree isSuUsed sbState
+  | (_, (Su, 0)) => negb (sbStateT_beq sbState Full)
+  | (_, (_, 0)) => true
+  | _ => false
+  end.
+
+Definition luFree isSuUsed sbState trace :=
+  let instr := get_instr_in_stage trace Lu in
+  match instr with
+  | Some elt => ready isSuUsed sbState elt
+  | None => true
+  end.
+
+Definition suFree isSuUsed sbState trace :=
+  let instr := get_instr_in_stage trace Su in
+  match instr with
+  | Some elt => ready isSuUsed sbState elt
+  | None => true
+  end.
+
+Definition lsuFree isSuUsed sbState trace :=
+  let instr := get_instr_in_stage trace Lsu in
+  match instr with
+  | Some elt => ready isSuUsed sbState elt
+  | None => true
+  end.
+
+Definition free isSuUsed sbState trace (elt : instr_kind) :=
+  let (opc, state) := elt in
+  let (st, _) := state in
+  match nstg st opc with
+  | Lu => luFree isSuUsed sbState trace
+  | Su => suFree isSuUsed sbState trace
+  | Lsu => lsuFree isSuUsed sbState trace
+  | _ => true
+  end.
+
+Definition cycle_elt isSuUsed sbState trace elt :=
+  match elt with
+  | (opc, (st, S n)) => (opc, (st, n))
+  | (opc, (st, 0)) =>
+      if ready isSuUsed sbState elt && free isSuUsed sbState trace elt then
+        (opc, (nstg st opc, 0))
+      else
+        elt
+  end.
+
+Definition cycle sbState trace :=
+  let isSuUsed := List.existsb is_in_su trace in
+  List.map (cycle_elt isSuUsed sbState trace) trace.
+
+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.
+    - destruct (ready _ _ _ && free _ _ _ _);
+        destruct s, o;
+        reflexivity.
+    - destruct s;
+        simpl;
+        rewrite Nat.leb_le;
+        lia.
+  Qed.
+End can_advance.