correct_store_buffer: specify how the store buffer can evolve

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

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.