correct_store_buffer: base hypothesis for monotonicity proofs

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

src/correct_store_buffer.v

@@ -129,6 +129,42 @@ Definition legal_sb_transitions_P suE suE' sbState sbState' :=
   | false, false, Empty => sbState' = Empty
   end.
 
+Section monotonicity.
+  Variable opc : opcode.
+  Variable st : stage.
+  Variable e e' d : instr_kind.
+  Variable t tpre tpost t' tpre' tpost' tc tc' : trace_kind.
+  Variable i : nat.
+  Variable sbState sbState' : sbStateT.
+
+  Hypothesis Ht : t = tpre ++ e :: tpost.
+  Hypothesis Ht' : t' = tpre' ++ e' :: tpost'.
+  Hypothesis Hleb : pipeline_leb t t' = true.
+  Hypothesis Hi : i = List.length tpre.
+  Hypothesis Hi' : i = List.length tpre'.
+  Hypothesis Hl : pipeline_leb tpre tpre' = true.
+  Hypothesis Hl' : pipeline_leb tpost tpost' = true.
+  Hypothesis Htc : tc = cycle sbState t.
+  Hypothesis Htc' : tc' = cycle sbState' t'.
+  Hypothesis Hlsbt : legal_sb_transitions st sbState sbState'.
+  Hypothesis HlsbtP : legal_sb_transitions_P (existsb is_in_su t) (existsb is_in_su t') sbState sbState'.
+  Hypothesis Hlu : forall st opc, st = Lu -> opc = Load.
+  Hypothesis Hsu : forall st opc, st = Su -> opc = Store.
+
+  (* Long hypotheses related to stage occupation. *)
+  Hypothesis HfreeLsuPersists :
+    free (existsb is_in_su t) sbState t (opc, (Sp, 0)) = true ->
+    free (existsb is_in_su t') sbState' t' (opc, (Sp, 0)) = true.
+
+  Hypothesis HfreeFromLsuPersists :
+    free (existsb is_in_su t) sbState t (opc, (Lsu, 0)) = true ->
+    free (existsb is_in_su t') sbState' t' (opc, (Lsu, 0)) = true.
+
+  Hypothesis HbusFree :
+    busFree (existsb is_in_su t) sbState = true ->
+    busFree (existsb is_in_su t') sbState' = true.
+End monotonicity.
+
 Section constrained.
   Variable opc : opcode.
   Variable e d : instr_kind.