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 +++++-------- src/translation/HTLgenspec.v | 65 ++++++++++++++++++++++--------------------- 2 files changed, 41 insertions(+), 43 deletions(-) (limited to 'src/translation') 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. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index ae2a58e..ca069c1 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -293,46 +293,49 @@ Proof. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. destruct (peq pc pc1). + subst. - destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor. - * assumption. + destruct instr1 eqn:?; try discriminate; + try destruct_optional; inv_add_instr; econstructor; try assumption. * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; [ discriminate | apply H9 ]. -(* * inversion H1. inversion H9. rewrite H. apply tr_instr_Inop. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. + eapply in_map with (f := fst) in H9. contradiction. - * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor. + * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. unfold nonblock. rewrite <- e2. rewrite H. constructor. eapply translate_instr_tr_op. apply EQ1. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + eapply in_map with (f := fst) in H9. contradiction. - * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor. apply EQ1. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. rewrite <- e2. rewrite H. econstructor. apply EQ1. + eapply in_map with (f := fst) in H9. contradiction. - * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * inversion H1. inversion H7. constructor. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. constructor. + eapply in_map with (f := fst) in H9. contradiction. - * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * inversion H1. inversion H7. constructor. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. + * inversion H2. inversion H9. constructor. + eapply in_map with (f := fst) in H9. contradiction. + eapply IHl. apply EQ0. assumption. - destruct H1. inversion H1. subst. contradiction. - assumption.*) -Admitted. + destruct H2. inversion H2. subst. contradiction. + intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. + destruct H2. inv H2. contradiction. assumption. assumption. +Qed. Hint Resolve iter_expand_instr_spec : htlspec. Theorem transl_module_correct : -- cgit