Finish top-level of proof

2 files changed, 23 insertions, 22 deletions

diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index a8da344..be57e7f 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -1354,15 +1354,7 @@ Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :
   else
     Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
 
-Definition transl_function_temp (f: RTLBlock.function) : Errors.res RTLPar.function :=
-  let tfcode := fn_code (schedule f) in
-    Errors.OK (mkfunction f.(fn_sig)
-                          f.(fn_params)
-                          f.(fn_stacksize)
-                          tfcode
-                          f.(fn_entrypoint)).
-
-Definition transl_fundef := transf_partial_fundef transl_function_temp.
+Definition transl_fundef := transf_partial_fundef transl_function.
 
 Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
   transform_partial_program transl_fundef p.
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 9cfee3a..119ed59 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -313,20 +313,29 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
 
     induction 1; repeat semantics_simpl.
 
-    { destruct bb as [bbc bbe]; destruct x as [bbc' bbe'].
-      assert (bbe = bbe') by admit.
-      rewrite H3 in H5.
-      exploit abstract_execution_correct. eauto. apply ge_preserved_lem.
-      eauto.
-      eapply abstract_execution_correct in H5; eauto with rtlgp.
-      repeat econstructor; eauto with rtlgp. simplify.
-      exploit step_cf_instr_correct. eauto.
-      econstructor; eauto with rtlgp.
+    { destruct bb; destruct x.
+      assert (bb_exit = bb_exit0) by admit; subst.
+
+      exploit abstract_execution_correct; try eassumption. eapply ge_preserved_lem.
+      econstructor; eauto.
+      inv_simp. destruct x. inv H7.
+
+      exploit step_cf_instr_correct; try eassumption. econstructor; eauto.
+      inv_simp.
+
+      econstructor. econstructor. eapply Smallstep.plus_one. econstructor.
+      eauto. eauto. simplify. eauto. eauto.
+    }
+    { unfold bind in *. inv TRANSL0. clear Learn. inv H0. destruct_match; crush.
+      inv H2. unfold transl_function in Heqr. destruct_match; crush.
+      inv Heqr. 
+      repeat econstructor; eauto.
+      unfold bind in *. destruct_match; crush.
     }
-    { unfold bind in *. destruct_match; try discriminate. repeat semantics_simpl. inv TRANSL0.
-      repeat econstructor; eauto. }
     { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. }
-    { inv STACKS. inv H2. repeat econstructor; eauto. }
-  Qed.
+    { inv STACKS. inv H2. repeat econstructor; eauto.
+      intros. admit.
+    }
+    Admitted.
 
 End CORRECTNESS.