correct_sb: define cycle_on_more_advanced

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

src/correct_store_buffer.v

@@ -65,6 +65,16 @@ Definition is_constrained (elt : instr_kind) trace sbState :=
   | _, _ => false
   end.
 
+Definition cycle_on_more_advanced (t : trace_kind) (instr : instr_kind) sbState :=
+  let (_, state) := instr in
+  let isSuUsed := List.existsb is_in_su t in
+  List.map (fun (elt : instr_kind) =>
+              let (_, state') := elt in
+              if state_leb state state' && negb (state_leb state' state) then
+                cycle_elt isSuUsed sbState t elt
+              else
+                elt) t.
+
 Section can_advance.
   Variable isSuUsed : bool.
   Variable sbState : sbStateT.