correct_store_buffer: add comments in luFree and suFree

This adds comment to clarify a specificity of the Sn stage, which
follows the Su and Lu stages.

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

src/correct_store_buffer.v

@@ -14,14 +14,14 @@ Definition ready isSuUsed sbState (elt : instr_kind) :=
 Definition luFree isSuUsed sbState trace :=
   let instr := get_instr_in_stage trace Lu in
   match instr with
-  | Some elt => ready isSuUsed sbState elt
+  | Some elt => ready isSuUsed sbState elt (* Sn is always free *)
   | 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
+  | Some elt => ready isSuUsed sbState elt (* Sn is always free *)
   | None => true
   end.