diff options
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v index 4bf4b03a..a1bd8638 100644 --- a/kvx/lib/RTLpathSE_impl.v +++ b/kvx/lib/RTLpathSE_impl.v @@ -1066,12 +1066,9 @@ Definition ok_args ge sp rs0 m0 hst lsv sm := Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lsv sm sv': hsilocal_refines ge sp rs0 m0 hst st -> - (forall ge sp rs0 m0, - ok_args ge sp rs0 m0 hst lsv sm -> - (hsok_local ge sp rs0 m0 hst -> seval_sval ge sp sv' rs0 m0 = seval_sval ge sp (rsv lsv sm) rs0 m0) ) -> + (ok_args ge sp rs0 m0 hst lsv sm -> (hsok_local ge sp rs0 m0 hst -> seval_sval ge sp sv' rs0 m0 = seval_sval ge sp (rsv lsv sm) rs0 m0)) -> hsilocal_refines ge sp rs0 m0 (hslocal_set_sreg hst r rsv lsv sm) (slocal_set_sreg st r sv'). Admitted. - (** ** Execution of one instruction *) Definition hsiexec_inst (i: instruction) (hst: hsistate): option hsistate := @@ -1174,11 +1171,15 @@ Proof. - (* Iop *) eapply hsist_set_local_correct_dyn; eauto. eapply hslocal_set_sreg_correct; eauto. - + simpl. admit. (* TODO *) + simpl; intros. + erewrite seval_list_sval_refines; eauto. + erewrite seval_smem_refines; eauto. - (* Iload *) eapply hsist_set_local_correct_dyn; eauto. eapply hslocal_set_sreg_correct; eauto. - + simpl. admit. (* TODO *) + simpl; intros. + erewrite seval_list_sval_refines; eauto. + erewrite seval_smem_refines; eauto. - (* Istore *) eapply hsist_set_local_correct_dyn; eauto. eapply hslocal_set_mem_correct; eauto. |