diff options
Diffstat (limited to 'src/hls/CondElimproof.v')
-rw-r--r-- | src/hls/CondElimproof.v | 179 |
1 files changed, 179 insertions, 0 deletions
diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v new file mode 100644 index 0000000..f16a710 --- /dev/null +++ b/src/hls/CondElimproof.v @@ -0,0 +1,179 @@ +(*| +.. + Vericert: Verified high-level synthesis. + Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see <https://www.gnu.org/licenses/>. + +================ +RTLBlockgenproof +================ + +.. coq:: none +|*) + +Require Import compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Globalenvs. +Require Import compcert.lib.Maps. +Require Import compcert.backend.Registers. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Events. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. + +Require Import vericert.common.Vericertlib. +Require Import vericert.common.DecEq. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.CondElim. + +#[local] Open Scope positive. + +Lemma cf_in_step : + forall A B ge sp is_ is_' bb cf, + @SeqBB.step A B ge sp (Iexec is_) bb (Iterm is_' cf) -> + exists p, In (RBexit p cf) bb + /\ Option.default true (Option.map (eval_predf (is_ps is_')) p) = true. + Proof. Admitted. + +Lemma forbidden_term_trans : + forall A B ge sp i c b i' c', + ~ @SeqBB.step A B ge sp (Iterm i c) b (Iterm i' c'). +Proof. induction b; unfold not; intros; inv H. Qed. + +Lemma random1 : + forall A B ge sp is_ b is_' cf, + @SeqBB.step A B ge sp (Iexec is_) b (Iterm is_' cf) -> + exists p b', SeqBB.step ge sp (Iexec is_) (b' ++ (RBexit p cf) :: nil) (Iterm is_' cf) + /\ Forall2 eq (b' ++ (RBexit p cf) :: nil) b. +Proof. +Admitted. + +Lemma replace_section_spec : + forall A B ge sp is_ is_' bb cf, + @SeqBB.step A B ge sp (Iexec is_) bb (Iterm is_' cf) -> + exists p, + @SeqBB.step A B ge sp (Iexec is_) + (snd (replace_section elim_cond_s p bb)) + (Iterm is_' cf). Admitted. + +Lemma transf_block_spec : + forall f pc b, + f.(fn_code) ! pc = Some b -> + exists p, + (transf_function f).(fn_code) ! pc + = Some (snd (replace_section elim_cond_s p b)). Admitted. + +Variant match_stackframe : stackframe -> stackframe -> Prop := + | match_stackframe_init : + forall res f tf sp pc rs p p' + (TF: transf_function f = tf), + match_stackframe (Stackframe res f sp pc rs p) (Stackframe res tf sp pc rs p'). + +Variant match_states : state -> state -> Prop := + | match_state : + forall stk stk' f tf sp pc rs p p0 m + (TF: transf_function f = tf) + (STK: Forall2 match_stackframe stk stk'), + match_states (State stk f sp pc rs p m) (State stk' tf sp pc rs p0 m) + | match_callstate : + forall cs cs' f tf args m + (TF: transf_fundef f = tf) + (STK: Forall2 match_stackframe cs cs'), + match_states (Callstate cs f args m) (Callstate cs' tf args m) + | match_returnstate : + forall cs cs' v m + (STK: Forall2 match_stackframe cs cs'), + match_states (Returnstate cs v m) (Returnstate cs' v m) +. + +Definition match_prog (p: program) (tp: program) := + Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp. + +Section CORRECTNESS. + + Context (prog tprog : program). + + Let ge : genv := Globalenvs.Genv.globalenv prog. + Let tge : genv := Globalenvs.Genv.globalenv tprog. + + Context (TRANSL : match_prog prog tprog). + + Lemma symbols_preserved: + forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. + Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed. + + Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). + Proof using TRANSL. intros; eapply (Genv.senv_transf TRANSL). Qed. + + Lemma function_ptr_translated: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + Genv.find_funct_ptr tge b = Some (transf_fundef f). + Proof (Genv.find_funct_ptr_transf TRANSL). + + Lemma sig_transf_function: + forall (f tf: fundef), + funsig (transf_fundef f) = funsig f. + Proof using. + unfold transf_fundef. unfold AST.transf_fundef; intros. destruct f. + unfold transf_function. auto. auto. + Qed. + + Lemma transf_initial_states : + forall s1, + initial_state prog s1 -> + exists s2, initial_state tprog s2 /\ match_states s1 s2. + Proof using TRANSL. + induction 1. + exploit function_ptr_translated; eauto; intros. + do 2 econstructor; simplify. econstructor. + apply (Genv.init_mem_transf TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto. + symmetry; eapply Linking.match_program_main; eauto. eauto. + erewrite sig_transf_function; eauto. constructor. auto. auto. + Qed. + + Lemma transf_final_states : + forall s1 s2 r, + match_states s1 s2 -> final_state s1 r -> final_state s2 r. + Proof using. + inversion 2; crush. subst. inv H. inv STK. econstructor. + Qed. + + Lemma transf_step_correct: + forall (s1 : state) (t : trace) (s1' : state), + step ge s1 t s1' -> + forall s2 : state, + match_states s1 s2 -> + exists s2' : state, step tge s2 t s2' /\ match_states s1' s2'. + Proof. + induction 1; intros. + + inv H2. eapply cf_in_step in H0; simplify. + do 2 econstructor. econstructor; eauto. admit. Admitted. + + Theorem transf_program_correct: + forward_simulation (semantics prog) (semantics tprog). + Proof using TRANSL. + eapply forward_simulation_step. + + apply senv_preserved. + + apply transf_initial_states. + + apply transf_final_states. + + apply transf_step_correct. + Qed. + + +End CORRECTNESS. |