From 971b35fd4af24cfffc462df13f8c5b9be982858e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 3 Jun 2020 19:36:50 +0100 Subject: Uncomment proof --- src/translation/HTLgenproof.v | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) (limited to 'src/translation/HTLgenproof.v') 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. -- cgit