From cd6bf14e8f5ce68624ba20a33b8278c78cb632fb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 29 Jan 2021 15:42:34 +0000 Subject: Fix the proof for RTLPargen --- src/hls/RTLPargenproof.v | 65 ++++++++++++++++++++++++------------------------ 1 file changed, 33 insertions(+), 32 deletions(-) (limited to 'src/hls') diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 0ff2312..157d734 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -24,8 +24,8 @@ Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlock. -Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLPar. +Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLPargen. Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) := @@ -35,34 +35,27 @@ Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: forall f tf res sp pc rs, transl_function f = OK tf -> - match_stackframes (RTLBlock.Stackframe res f sp pc rs) - (RTLPar.Stackframe res tf sp pc rs). + match_stackframes (Stackframe res f sp pc rs) + (Stackframe res tf sp pc rs). Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := | match_state: forall sf f sp pc rs mem sf' tf (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf'), - match_states (RTLBlock.State sf f sp pc rs mem) - (RTLPar.State sf' tf sp pc rs mem) -| match_block: - forall sf f sp bb bb' rs mem sf' tf - (TRANSL: transl_function f = OK tf) - (STACKS: list_forall2 match_stackframes sf sf') - (BB: schedule_oracle bb bb' = true), - match_states (RTLBlock.Block sf f sp bb rs mem) - (RTLPar.Block sf' tf sp bb' rs mem) + match_states (State sf f sp pc rs mem) + (State sf' tf sp pc rs mem) | match_returnstate: forall stack stack' v mem (STACKS: list_forall2 match_stackframes stack stack'), - match_states (RTLBlock.Returnstate stack v mem) - (RTLPar.Returnstate stack' v mem) + match_states (Returnstate stack v mem) + (Returnstate stack' v mem) | match_initial_call: forall stack stack' f tf args m (TRANSL: transl_fundef f = OK tf) (STACKS: list_forall2 match_stackframes stack stack'), - match_states (RTLBlock.Callstate stack f args m) - (RTLPar.Callstate stack' tf args m). + match_states (Callstate stack f args m) + (Callstate stack' tf args m). Section CORRECTNESS. @@ -103,7 +96,7 @@ Section CORRECTNESS. Lemma sig_transl_function: forall (f: RTLBlock.fundef) (tf: RTLPar.fundef), transl_fundef f = OK tf -> - RTLPar.funsig tf = RTLBlock.funsig f. + funsig tf = funsig f. Proof. unfold transl_fundef, transf_partial_fundef, transl_function; intros; repeat destruct_match; crush; @@ -112,8 +105,8 @@ Section CORRECTNESS. Lemma find_function_translated: forall ros rs f, - RTLBlock.find_function ge ros rs = Some f -> - exists tf, RTLPar.find_function tge ros rs = Some tf + find_function ge ros rs = Some f -> + exists tf, find_function tge ros rs = Some tf /\ transl_fundef f = OK tf. Proof. destruct ros; simplify; @@ -125,12 +118,28 @@ Section CORRECTNESS. Lemma schedule_oracle_nil: forall bb cfi, schedule_oracle {| bb_body := nil; bb_exit := cfi |} bb = true -> - is_empty (bb_body bb) /\ bb_exit bb = cfi. + bb_body bb = nil /\ bb_exit bb = cfi. + Proof. + unfold schedule_oracle, check_control_flow_instr. + simplify; repeat destruct_match; crush. + Qed. + + Lemma schedule_oracle_nil2: + forall cfi, + schedule_oracle {| bb_body := nil; bb_exit := cfi |} + {| bb_body := nil; bb_exit := cfi |} = true. Proof. - unfold schedule_oracle, check_control_flow_instr, is_empty. + unfold schedule_oracle, check_control_flow_instr. simplify; repeat destruct_match; crush. Qed. + Lemma schedule_sem_correct: + forall bb bb' cfi sp rs m rs' m', + schedule_oracle {| bb_body := bb; bb_exit := cfi |} {| bb_body := bb'; bb_exit := cfi |} = true -> + step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') -> + step_instr_block tge sp (InstrState rs m) bb' (InstrState rs' m'). + Proof. Admitted. + Theorem transl_step_correct : forall (S1 : RTLBlock.state) t S2, RTLBlock.step ge S1 t S2 -> @@ -145,7 +154,7 @@ Section CORRECTNESS. let H2 := fresh "TRANSL" in learn H as H2; unfold transl_function in H2; - destruct (check_scheduled_trees (RTLBlock.fn_code f) (fn_code (schedule f))) eqn:?; + destruct (check_scheduled_trees (fn_code f) (fn_code (schedule f))) eqn:?; [| discriminate ]; inv H2 | [ H: context[check_scheduled_trees] |- _ ] => let H2 := fresh "CHECK" in @@ -161,17 +170,9 @@ Section CORRECTNESS. induction 1; repeat t. - { repeat econstructor; eauto. } - { admit. } - { destruct bb'; exploit find_function_translated; simplify; - repeat econstructor; eauto using sig_transl_function. } - { destruct bb'; exploit find_function_translated; simplify; - repeat econstructor; eauto using sig_transl_function. } - { destruct bb'; simplify; subst; repeat econstructor; eauto using Events.eval_builtin_args_preserved, Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } - { destruct bb'; simplify; subst; repeat econstructor; eauto. } - { destruct bb'; simplify; subst; repeat econstructor; eauto. } - { destruct bb'; simplify; subst; repeat econstructor; eauto. } + admit. { unfold bind in *. destruct_match; try discriminate. repeat t. 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 H1. repeat econstructor; eauto. } + Qed. -- cgit