diff options
Diffstat (limited to 'src/hls/GiblePargenproof.v')
-rw-r--r-- | src/hls/GiblePargenproof.v | 51 |
1 files changed, 33 insertions, 18 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index caad4b5..c48e5f3 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -2023,8 +2023,8 @@ all be evaluable. Lemma step_instr_lessdef_term : forall sp a i i' ti cf, step_instr ge sp (Iexec i) a (Iterm i' cf) -> - state_lessdef i ti -> - exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ state_lessdef i' ti'. + Abstr.match_states i ti -> + exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ Abstr.match_states i' ti'. Proof. inversion 1; intros; subst. econstructor. split; eauto. constructor. @@ -2042,11 +2042,11 @@ all be evaluable. constructor. auto. Qed. - Lemma state_lessdef_sem : + Lemma Abstr_match_states_sem : forall i sp f i' ti cf, sem (mk_ctx i sp ge) f (i', cf) -> - state_lessdef i ti -> - exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ state_lessdef i' ti'. + Abstr.match_states i ti -> + exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ Abstr.match_states i' ti'. Proof. Admitted. (* This needs a bit more in Abstr.v *) Lemma mfold_left_update_Some : @@ -2183,7 +2183,7 @@ all be evaluable. Lemma eval_predf_lessdef : forall p a b, - state_lessdef a b -> + Abstr.match_states a b -> eval_predf (is_ps a) p = eval_predf (is_ps b) p. Proof using. induction p; crush. @@ -2228,9 +2228,9 @@ execution, the values in the register map do not continue to change. eval_predf (is_ps i') curr_p = true -> mfold_left update x (Some (curr_p, f)) = Some (p, f') -> forall ti, - state_lessdef i ti -> + Abstr.match_states i ti -> exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf) - /\ state_lessdef i'' ti' + /\ Abstr.match_states i'' ti' /\ valid_mem (is_mem i) (is_mem i''). Proof. induction x as [| x xs IHx ]; intros; cbn -[update] in *; inv H; cbn [fst snd] in *. @@ -2248,7 +2248,7 @@ execution, the values in the register map do not continue to change. - (* terminal case *) exploit mfold_left_update_Some; eauto; intros Hexists; inversion Hexists as [[curr_p_inter f_inter] EXEQ]; clear Hexists. rewrite EXEQ in H2. - exploit state_lessdef_sem; (* TODO *) + exploit Abstr_match_states_sem; (* TODO *) eauto; intros H; inversion H as [v [Hi LESSDEF]]; clear H. exploit step_instr_lessdef_term; eauto; intros H; inversion H as [v2 [Hi2 LESSDEF2]]; clear H. @@ -2293,9 +2293,9 @@ execution, the values in the register map do not continue to change. SeqBB.step ge sp (Iexec i) x (Iterm i'' cf) -> abstract_sequence x = Some x' -> forall ti, - state_lessdef i ti -> + Abstr.match_states i ti -> exists ti', sem (mk_ctx ti sp ge) x' (ti', Some cf) - /\ state_lessdef i'' ti'. + /\ Abstr.match_states i'' ti'. Proof. unfold abstract_sequence. intros. unfold Option.map in H0. destruct_match; try easy. @@ -2309,9 +2309,9 @@ execution, the values in the register map do not continue to change. forall sp x i i' ti cf x', abstract_sequence x = Some x' -> sem (mk_ctx i sp ge) x' (i', (Some cf)) -> - state_lessdef i ti -> + Abstr.match_states i ti -> exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) - /\ state_lessdef i' ti'. + /\ Abstr.match_states i' ti'. Proof. (*| @@ -2355,18 +2355,33 @@ square: clock cycles. |*) + Definition local_abstr_check_correct := + @abstr_check_correct GibleSeq.fundef GiblePar.fundef. + + Definition local_abstr_check_correct2 := + @abstr_check_correct GibleSeq.fundef GibleSeq.fundef. + + Lemma ge_preserved_local : + ge_preserved ge tge. + Proof. + unfold ge_preserved; + eauto using Op.eval_operation_preserved, Op.eval_addressing_preserved. + Qed. + Lemma schedule_oracle_correct : forall x y sp i i' ti cf, schedule_oracle x y = true -> SeqBB.step ge sp (Iexec i) x (Iterm i' cf) -> - state_lessdef i ti -> + Abstr.match_states i ti -> exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf) - /\ state_lessdef i' ti'. + /\ Abstr.match_states i' ti'. Proof. unfold schedule_oracle; intros. repeat (destruct_match; try discriminate). simplify. exploit abstr_sequence_correct; eauto; simplify. - exploit abstr_check_correct; eauto. apply state_lessdef_refl. simplify. - exploit abstr_seq_reverse_correct; eauto. apply state_lessdef_refl. simplify. + exploit local_abstr_check_correct2; eauto. + { constructor. eapply ge_preserved_refl. reflexivity. } + simplify. + exploit abstr_seq_reverse_correct; eauto. reflexivity. simplify. exploit seqbb_step_parbb_step; eauto; intros. econstructor; split; eauto. etransitivity; eauto. @@ -2390,7 +2405,7 @@ Proof Sketch: Trivial because of structural equality. Lemma match_states_stepBB : forall s f sp pc rs pr m sf' f' trs tps tm rs' pr' m' trs' tpr' tm', match_states (GibleSeq.State s f sp pc rs pr m) (State sf' f' sp pc trs tps tm) -> - state_lessdef (mk_instr_state rs' pr' m') (mk_instr_state trs' tpr' tm') -> + Abstr.match_states (mk_instr_state rs' pr' m') (mk_instr_state trs' tpr' tm') -> match_states (GibleSeq.State s f sp pc rs' pr' m') (State sf' f' sp pc trs' tpr' tm'). Proof. inversion 1; subst; simplify. |