diff options
Diffstat (limited to 'kvx/SelectOpproof.v')
-rw-r--r-- | kvx/SelectOpproof.v | 54 |
1 files changed, 53 insertions, 1 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index cffa2583..a45d367f 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1883,6 +1883,57 @@ Proof. destruct v2; simpl; trivial. Qed. +Lemma eval_abs: + forall al a vl v le, + gen_abs al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem BI_abs vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + unfold gen_abs. + intros until le. + intros SELECT Heval BUILTIN. + inv Heval. discriminate. + inv H0. 2: discriminate. + cbn in BUILTIN. + inv BUILTIN. + inv SELECT. + econstructor; split. + { repeat (econstructor + eassumption). + } + destruct v1; try constructor. + cbn. + unfold int_abs, int_absdiff, Z_abs_diff. + change (Int.signed Int.zero) with 0%Z. + rewrite Z.sub_0_r. + constructor. +Qed. + +Lemma eval_absl: + forall al a vl v le, + gen_absl al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem BI_absl vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + unfold gen_abs. + intros until le. + intros SELECT Heval BUILTIN. + inv Heval. discriminate. + inv H0. 2: discriminate. + cbn in BUILTIN. + inv BUILTIN. + inv SELECT. + econstructor; split. + { repeat (econstructor + eassumption). + } + destruct v1; try constructor. + cbn. + unfold long_abs, long_absdiff, Z_abs_diff. + change (Int64.signed Int64.zero) with 0%Z. + rewrite Z.sub_0_r. + constructor. +Qed. Require FPDivision32. @@ -1995,6 +2046,7 @@ Proof. } inv EVAL. constructor. + - apply eval_abs; assumption. + - apply eval_absl; assumption. Qed. - End CMCONSTR. |