From e1d0762daf0dd4d8f826decaa4c0498c75aa9119 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 21 May 2021 18:28:58 +0100 Subject: Finish top-level of proof --- src/hls/RTLPargen.v | 10 +--------- src/hls/RTLPargenproof.v | 35 ++++++++++++++++++++++------------- 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. -- cgit