diff options
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 26b5bae6..a3be20b5 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -112,6 +112,31 @@ Theorem plus_simulation s1 t s1': exists s2', plus RTL.step tge s2 t s2' /\ match_states s1' s2'. +Proof. + induction 1; intros; inv MS. + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (ib' & FNC & MIB). + inv H0. destruct H1 as (m' & fin & IBIS & FS). + admit. + (* Définir une relation inductive qui provient du MS, + et qui relie le iblock_istep avec le RTL. Il faut prendre en compte + le "isfst" pour savoir si on doit avoir du "stuttering" côté RTL. *) + (* exec_function_internal *) + - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split. + + eapply plus_one. apply RTL.exec_function_internal. + erewrite <- preserv_fnstacksize; eauto. + + erewrite <- preserv_fnparams; eauto. + eapply match_states_intro; eauto. + apply dupmap_entrypoint. assumption. + (* exec_function_external *) + - inversion TRANSF as [|]; subst. eexists. split. + + eapply plus_one. econstructor. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor. assumption. + (* exec_return *) + - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split. + + eapply plus_one. constructor. + + inv H1. econstructor; eauto. Admitted. (* TODO: première étape *) Theorem transf_program_correct: |