correct_store_buffer.v

Require Import Bool Lia List Nat PeanoNat.
From StoreBuffer Require Import definitions utils.
Import ListNotations.

Variant sbStateT :=
  | Empty
  | NotEmpty
  | Full.

Scheme Equality for sbStateT.

(* free and cycle functions. *)
Definition busFree isSuUsed sbState :=
  (sbStateT_beq sbState Empty) && (negb isSuUsed).

Definition ready isSuUsed sbState (elt : instr_kind) :=
  match elt with
  | (Load, (Lsu, 0)) => busFree isSuUsed sbState
  | (_, (Su, 0)) => negb (sbStateT_beq sbState Full)
  | (_, (_, 0)) => true
  | _ => false
  end.

Definition luFree isSuUsed sbState trace :=
  let instr := get_instr_in_stage trace Lu in
  match instr with
  | Some elt => ready isSuUsed sbState elt
  | None => true
  end.

Definition suFree isSuUsed sbState trace :=
  let instr := get_instr_in_stage trace Su in
  match instr with
  | Some elt => ready isSuUsed sbState elt
  | None => true
  end.

Definition lsuFree isSuUsed sbState trace :=
  let instr := get_instr_in_stage trace Lsu in
  match instr with
  | Some elt => ready isSuUsed sbState elt
  | None => true
  end.

Definition free isSuUsed sbState trace (elt : instr_kind) :=
  let (opc, state) := elt in
  let (st, _) := state in
  match nstg st opc with
  | Lu => luFree isSuUsed sbState trace
  | Su => suFree isSuUsed sbState trace
  | Lsu => lsuFree isSuUsed sbState trace
  | _ => true
  end.

Definition cycle_elt isSuUsed sbState trace elt :=
  match elt with
  | (opc, (st, S n)) => (opc, (st, n))
  | (opc, (st, 0)) =>
      if ready isSuUsed sbState elt && free isSuUsed sbState trace elt then
        (opc, (nstg st opc, 0))
      else
        elt
  end.

Definition cycle sbState trace :=
  let isSuUsed := List.existsb is_in_su trace in
  List.map (cycle_elt isSuUsed sbState trace) trace.

Section can_advance.
  Variable isSuUsed : bool.
  Variable sbState : sbStateT.
  Variable n : nat.
  Variable t : trace_kind.

  Theorem instruction_never_regresses :
    forall t' e1, t' = cycle sbState t ->
             List.nth_error t n = Some e1 ->
             compare_two (List.nth_error t n) (List.nth_error t' n) = true.
  Proof.
    intros t' e1 Ht' He1.

    rewrite Ht', He1.
    unfold cycle.
    rewrite (map_nth_error _ _ _ He1).

    unfold compare_two.
    destruct e1.
    unfold cycle_elt.
    destruct s, n0.
    - destruct (ready _ _ _ && free _ _ _ _);
        destruct s, o;
        reflexivity.
    - destruct s;
        simpl;
        rewrite Nat.leb_le;
        lia.
  Qed.
End can_advance.