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

1 files changed, 100 insertions, 8 deletions

diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v
index c478f70b..f08c1157 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.
@@ -816,6 +816,98 @@ Definition my_div (a b : val) :=
   let x := fmaddf invb_d alpha invb_d in
   Val.mulf (Val.maketotal (Val.floatofintu a)) x.
 
-(*
-Compute (my_div (Vint (Int.repr 3)) (Vint (Int.repr 5))).
-*)
+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.