From 3d4f7f60b90131d8e543c1db150294362257e586 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Mon, 4 Jul 2022 16:33:03 +0200
Subject: [PATCH] store_buffer: move compare_two to definitions

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
 src/definitions.v  | 9 +++++++++
 src/store_buffer.v | 7 -------
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/definitions.v b/src/definitions.v
index ad4fe5b..3096c87 100644
--- a/src/definitions.v
+++ b/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).
 
diff --git a/src/store_buffer.v b/src/store_buffer.v
index dff98d3..dcfd33a 100644
--- a/src/store_buffer.v
+++ b/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.
-- 
GitLab