From f06f87e76cee43d2a4d9b47bea758a2ed5c78bd8 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 9 Oct 2020 18:13:30 +0200 Subject: hconsing: red_PTree_set_correct --- kvx/lib/RTLpathSE_impl_junk.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'kvx') 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 -- cgit