Merge remote-tracking branch 'origin/kvx-bits' into kvx_fp_division

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.