diff options
Diffstat (limited to 'kvx/lib/RTLpathSchedulerproof.v')
| -rw-r--r-- | kvx/lib/RTLpathSchedulerproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kvx/lib/RTLpathSchedulerproof.v b/kvx/lib/RTLpathSchedulerproof.v index 5c32847e..437f1e0a 100644 --- a/kvx/lib/RTLpathSchedulerproof.v +++ b/kvx/lib/RTLpathSchedulerproof.v @@ -215,6 +215,8 @@ Proof. intros (path & PATH). eexists; split; econstructor; eauto. + eapply seval_builtin_args_preserved; eauto. + eapply seval_list_builtin_sval_correct; eauto. + admit. (* something like seval_list_builtin_sval_preserved *) + eapply external_call_symbols_preserved; eauto. + eapply eqlive_reg_refl. - (* Sjumptable *) @@ -229,7 +231,7 @@ Proof. + erewrite <- preserv_fnstacksize; eauto. + destruct os; auto. erewrite <- seval_preserved; eauto. -Qed. +Admitted. (* The main theorem on simulation of symbolic states ! *) Theorem ssem_sstate_simu dm f f' stk stk' sp st st' rs m t s: |