abs builtins

1 files changed, 40 insertions, 13 deletions

diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v
index 434d283e..c493f708 100644
--- a/kvx/ExtValues.v
+++ b/kvx/ExtValues.v
@@ -21,14 +21,14 @@ Require Import Lia.
 
 Open Scope Z_scope.
 
-Definition int_abs_diff (x y : Z) := Z.abs (x - y).
-Definition int_abs_diff2 (x y : Z) :=
+Definition Z_abs_diff (x y : Z) := Z.abs (x - y).
+Definition Z_abs_diff2 (x y : Z) :=
   if x <=? y then y - x else x - y.
-Lemma int_abs_diff2_correct :
-  forall x y : Z, (int_abs_diff x y) = (int_abs_diff2 x y).
+Lemma Z_abs_diff2_correct :
+  forall x y : Z, (Z_abs_diff x y) = (Z_abs_diff2 x y).
 Proof.
   intros.
-  unfold int_abs_diff, int_abs_diff2.
+  unfold Z_abs_diff, Z_abs_diff2.
   unfold Z.leb.
   pose proof (Z.compare_spec x y) as Hspec.
   inv Hspec.
@@ -755,20 +755,47 @@ Definition fmaddfs := triple_op_single (fun f1 f2 f3 => Float32.fma f2 f3 f1).
 Definition fmsubf := triple_op_float (fun f1 f2 f3 => Float.fma (Float.neg f2) f3 f1).
 Definition fmsubfs := triple_op_single (fun f1 f2 f3 => Float32.fma (Float32.neg f2) f3 f1).
 
-Definition double_op_intZ f v1 v2 :=
+Definition int_abs i1 := Int.repr (Z.abs (Int.signed i1)).
+Definition long_abs i1 := Int64.repr (Z.abs (Int64.signed i1)).
+
+Definition int_absdiff i1 i2 :=
+             Int.repr (Z_abs_diff (Int.signed i1) (Int.signed i2)).
+
+Definition long_absdiff i1 i2 :=
+             Int64.repr (Z_abs_diff (Int64.signed i1) (Int64.signed i2)).
+
+Lemma int_absdiff_zero :
+  forall i, int_abs i = int_absdiff i Int.zero.
+Proof.
+  intro. unfold int_abs, int_absdiff, Z_abs_diff.
+  change (Int.signed Int.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  reflexivity.
+Qed.
+
+Lemma long_absdiff_zero :
+  forall i, long_abs i = long_absdiff i Int64.zero.
+Proof.
+  intro. unfold long_abs, long_absdiff, Z_abs_diff.
+  change (Int64.signed Int64.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  reflexivity.
+Qed.
+
+Definition double_op_int f v1 v2 :=
   match v1, v2 with
-  | (Vint i1), (Vint i2) => Vint (Int.repr (f (Int.signed i1) (Int.signed i2)))
+  | (Vint i1), (Vint i2) => Vint (f i1 i2)
   |  _, _ => Vundef
   end.
 
-Definition double_op_longZ f v1 v2 :=
+Definition double_op_long f v1 v2 :=
   match v1, v2 with
-  | (Vlong i1), (Vlong i2) => Vlong (Int64.repr (f (Int64.signed i1) (Int64.signed i2)))
+  | (Vlong i1), (Vlong i2) => Vlong (f i1 i2)
   | _, _ => Vundef
   end.
 
-Definition absdiff := double_op_intZ int_abs_diff.
-Definition absdiffl := double_op_longZ int_abs_diff.
+Definition absdiff := double_op_int int_absdiff.
+Definition absdiffl := double_op_long long_absdiff.
 
 Definition abs v1 :=
   match v1 with
@@ -786,7 +813,7 @@ Lemma absdiff_zero_correct:
   forall v, abs v = absdiff v (Vint Int.zero).
 Proof.
   intro. destruct v; cbn; try reflexivity.
-  f_equal. unfold int_abs_diff.
+  f_equal. unfold int_absdiff, Z_abs_diff.
   change (Int.unsigned Int.zero) with 0%Z.
   rewrite Z.sub_0_r.
   reflexivity.
@@ -796,7 +823,7 @@ Lemma absdiffl_zero_correct:
   forall v, absl v = absdiffl v (Vlong Int64.zero).
 Proof.
   intro. destruct v; cbn; try reflexivity.
-  f_equal. unfold int_abs_diff.
+  f_equal. unfold long_absdiff, Z_abs_diff.
   change (Int64.unsigned Int64.zero) with 0%Z.
   rewrite Z.sub_0_r.
   reflexivity.