diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 921df5cb9b38f34ee0d2555965562e501eae9a15..08afe789b94b71b56a6d15238cecfdabea57f1b6 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -107,6 +107,28 @@ Section can_advance.
   Qed.
 End can_advance.
 
+Definition legal_sb_transitions st sbState sbState' :=
+  match st, sbState with
+  | Su, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
+  | Su, Empty => sbState' = Empty
+  | _, _ => 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 constrained.
   Variable opc : opcode.
   Variable e d : instr_kind.