store_buffer: move compare_two to definitions

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

src/definitions.v

@@ -110,6 +110,15 @@ Definition state_leb st1 st2 :=
 Definition instr_kind := (opcode * state)%type.
 Definition trace_kind := list instr_kind.
 
+(* Compare two with options.  This will be necessary for proofs since we will
+ * make heavy use of List.nth_error. *)
+Definition compare_two (e1 e2 : option instr_kind) :=
+  match e1, e2 with
+  | None, _
+  | _, None => false
+  | Some (_, st1), Some (_, st2) => state_leb st1 st2
+  end.
+
 Definition get_opc (trace : trace_kind) :=
   fst (List.split trace).
 

src/store_buffer.v

@@ -57,13 +57,6 @@ Definition cycle dchit busTaken wbFull trace :=
   let isSuUsed := List.existsb is_in_su trace in
   List.map (cycle_elt isSuUsed dchit busTaken wbFull trace) trace.
 
-Definition compare_two (e1 e2 : option instr_kind) :=
-  match e1, e2 with
-  | None, _
-  | _, None => false
-  | Some (_, st1), Some (_, st2) => state_leb st1 st2
-  end.
-
 Section can_advance.
   Variable isSuUsed dchit busTaken wbFull : bool.
   Variable n : nat.