From ed6e20995761614ee7ea6235b978a463f071c123 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 14 Feb 2022 17:49:40 +0100
Subject: abs builtins

---
 kvx/SelectOpproof.v | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 54 insertions(+), 1 deletion(-)

(limited to 'kvx/SelectOpproof.v')

diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 0ede1e2d..4ddf6ece 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1883,6 +1883,58 @@ 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.
+
 Theorem eval_platform_builtin:
   forall bf al a vl v le,
   platform_builtin bf al = Some a ->
@@ -1896,6 +1948,7 @@ Proof.
        repeat (try econstructor; try eassumption)).
   - apply eval_fma; assumption.
   - apply eval_fmaf; assumption.
+  - apply eval_abs; assumption.
+  - apply eval_absl; assumption.
 Qed.
-
 End CMCONSTR.
-- 
cgit