1 files changed, 101 insertions, 5 deletions
diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v
index b4e14898..c493f708 100644
--- a/kvx/ExtValues.v
+++ b/kvx/ExtValues.v
@@ -21,14 +21,14 @@ Require Import Lia.
 
 Open Scope Z_scope.
 
-Definition abs_diff (x y : Z) := Z.abs (x - y).
-Definition 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 abs_diff2_correct :
-  forall x y : Z, (abs_diff x y) = (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 abs_diff, abs_diff2.
+  unfold Z_abs_diff, Z_abs_diff2.
   unfold Z.leb.
   pose proof (Z.compare_spec x y) as Hspec.
   inv Hspec.
@@ -754,3 +754,99 @@ 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 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 (f i1 i2)
+  |  _, _ => Vundef
+  end.
+
+Definition double_op_long f v1 v2 :=
+  match v1, v2 with
+  | (Vlong i1), (Vlong i2) => Vlong (f i1 i2)
+  | _, _ => Vundef
+  end.
+
+Definition absdiff := double_op_int int_absdiff.
+Definition absdiffl := double_op_long long_absdiff.
+
+Definition abs v1 :=
+  match v1 with
+  | Vint x => Vint (Int.repr (Z.abs (Int.signed x)))
+  | _ => Vundef
+  end.
+
+Definition absl v1 :=
+  match v1 with
+  | Vlong x => Vlong (Int64.repr (Z.abs (Int64.signed x)))
+  | _ => Vundef
+  end.
+
+Lemma absdiff_zero_correct:
+  forall v, abs v = absdiff v (Vint Int.zero).
+Proof.
+  intro. destruct v; cbn; try reflexivity.
+  f_equal. unfold int_absdiff, Z_abs_diff.
+  change (Int.unsigned Int.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  reflexivity.
+Qed.
+
+Lemma absdiffl_zero_correct:
+  forall v, absl v = absdiffl v (Vlong Int64.zero).
+Proof.
+  intro. destruct v; cbn; try reflexivity.
+  f_equal. unfold long_absdiff, Z_abs_diff.
+  change (Int64.unsigned Int64.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  reflexivity.
+Qed.
+
+Remark absdiff_inject:
+  forall f v1 v1' v2 v2'
+  (INJ1 : Val.inject f v1 v1')
+  (INJ2 : Val.inject f v2 v2'),
+  Val.inject f (absdiff v1 v2) (absdiff v1' v2').
+Proof.
+  intros.
+  inv INJ1; cbn; try constructor.
+  inv INJ2; cbn; constructor.
+Qed.
+
+Remark absdiffl_inject:
+  forall f v1 v1' v2 v2'
+  (INJ1 : Val.inject f v1 v1')
+  (INJ2 : Val.inject f v2 v2'),
+  Val.inject f (absdiffl v1 v2) (absdiffl v1' v2').
+Proof.
+  intros.
+  inv INJ1; cbn; try constructor.
+  inv INJ2; cbn; constructor.
+Qed.