diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v index 47598bb8e61c674640ed640d6dae78d8c4c63c21..e375b48f8a5add3f83d78662d178410df0776551 100644 --- a/src/correct_store_buffer.v +++ b/src/correct_store_buffer.v @@ -164,6 +164,7 @@ Section monotonicity. free (existsb is_in_su t') sbState' t' (opc, (Lsu, 0)) = true. Hypothesis HbusFree : + forall st, st = Lsu -> busFree (existsb is_in_su t) sbState = true -> busFree (existsb is_in_su t') sbState' = true. @@ -197,6 +198,7 @@ Section monotonicity. intros He He' n. specialize (Hlu st opc). specialize (Hsu st opc). + specialize (HbusFree st). (* Delve onto e, then handle stages on a case-by-case basis. *) work_on_e He'. @@ -220,8 +222,7 @@ Section monotonicity. (* Loads *) + unfold ready. destruct (busFree _ sbState). - * now destruct (busFree _ _); - [ + * now destruct (busFree _ _); [ destruct (free _ _ _ _) in HfreeFromLsuPersists |- *; try discriminate HfreeFromLsuPersists | discriminate HbusFree