diff options
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index a8177cf..e719070 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -107,11 +107,6 @@ Lemma assumption_32bit : valueToPos (posToValue 32 v) = v. Admitted. -Lemma assumption_32bit_bool : - forall b, - valueToBool (boolToValue 32 b) = b. -Admitted. - Lemma st_greater_than_res : forall m res : positive, m <> res. @@ -127,6 +122,11 @@ Lemma finish_not_res : f <> r. Admitted. +Lemma greater_than_max_func : + forall f st, + Plt (RTL.max_reg_function f) st. +Proof. Admitted. + Ltac inv_state := match goal with MSTATE : match_states _ _ |- _ => @@ -239,11 +239,6 @@ Section CORRECTNESS. exists assoc', HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc'). - Lemma greater_than_max_func : - forall f st, - Plt (RTL.max_reg_function f) st. - Proof. Admitted. - Theorem transl_step_correct: forall (S1 : RTL.state) t S2, RTL.step ge S1 t S2 -> @@ -358,11 +353,11 @@ Section CORRECTNESS. eapply Verilog.erun_Vternary_true. eapply eval_cond_correct; eauto. constructor. - apply assumption_32bit_bool. + apply boolToValue_ValueToBool. eapply Verilog.erun_Vternary_false. eapply eval_cond_correct; eauto. constructor. - apply assumption_32bit_bool. + apply boolToValue_ValueToBool. trivial. constructor. trivial. |