diff options
Diffstat (limited to 'kvx')
-rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 80e8b08c..dce66a5f 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -824,6 +824,17 @@ Definition red_PTree_set (r: reg) (hsv: hsval) (hst: PTree.t hsval): PTree.t hsv | _ => PTree.set r hsv hst end. +Lemma red_PTree_set_correct (r r0:reg) hsv hst ge sp rs0 m0: + hsi_sreg_eval ge sp (red_PTree_set r hsv hst) r0 rs0 m0 = hsi_sreg_eval ge sp (PTree.set r hsv hst) r0 rs0 m0. +Proof. + destruct hsv; simpl; auto. + destruct (Pos.eq_dec r r1); auto. + subst; unfold hsi_sreg_eval. + destruct (Pos.eq_dec r0 r1); auto. + - subst; rewrite PTree.grs, PTree.gss; simpl; auto. + - rewrite PTree.gro, PTree.gso; simpl; auto. +Qed. + Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local := DO ok_lhsv <~ (if may_trap rsv lr |