Uncomment proof

3 files changed, 46 insertions, 43 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.
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 :
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index efbd99c..d527b15 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -356,3 +356,8 @@ Proof.
   unfold valToValue in H. inversion H.
   symmetry. apply valueToInt_intToValue.
 Qed.
+
+Lemma boolToValue_ValueToBool :
+  forall b,
+  valueToBool (boolToValue 32 b) = b.
+Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed.