From f6686d81092ccaaf3a22b4e34aecc7c5895b08ba Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 14 Feb 2022 15:48:43 +0100 Subject: begin adding abdw abdd --- kvx/ExtValues.v | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 74 insertions(+), 5 deletions(-) (limited to 'kvx/ExtValues.v') diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v index b4e14898..434d283e 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 int_abs_diff (x y : Z) := Z.abs (x - y). +Definition int_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 int_abs_diff2_correct : + forall x y : Z, (int_abs_diff x y) = (int_abs_diff2 x y). Proof. intros. - unfold abs_diff, abs_diff2. + unfold int_abs_diff, int_abs_diff2. unfold Z.leb. pose proof (Z.compare_spec x y) as Hspec. inv Hspec. @@ -754,3 +754,72 @@ 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 := + match v1, v2 with + | (Vint i1), (Vint i2) => Vint (Int.repr (f (Int.signed i1) (Int.signed i2))) + | _, _ => Vundef + end. + +Definition double_op_longZ f v1 v2 := + match v1, v2 with + | (Vlong i1), (Vlong i2) => Vlong (Int64.repr (f (Int64.signed i1) (Int64.signed i2))) + | _, _ => Vundef + end. + +Definition absdiff := double_op_intZ int_abs_diff. +Definition absdiffl := double_op_longZ int_abs_diff. + +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_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 int_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. -- cgit From ed6e20995761614ee7ea6235b978a463f071c123 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 14 Feb 2022 17:49:40 +0100 Subject: abs builtins --- kvx/ExtValues.v | 53 ++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 40 insertions(+), 13 deletions(-) (limited to 'kvx/ExtValues.v') 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. -- cgit