diff options
author | jadep <jade.philipoom@gmail.com> | 2017-05-14 15:52:56 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2017-05-14 15:56:56 -0400 |
commit | 7df5033c871aef6172d4e98d42ce00005e24f73e (patch) | |
tree | c858b22c861885a5f76d648afb2b102f7fc89662 | |
parent | 7e3d941510ad65ea712f608a9e0b2a19437e9e84 (diff) |
add wrapper for add_get_carry and proofs for add_get_carry and zselect
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Util/ZUtil/AddGetCarry.v | 21 | ||||
-rw-r--r-- | src/Util/ZUtil/Definitions.v | 9 | ||||
-rw-r--r-- | src/Util/ZUtil/Zselect.v | 16 |
4 files changed, 47 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index f65bc9e84..4e3d52282 100644 --- a/_CoqProject +++ b/_CoqProject @@ -328,6 +328,7 @@ src/Util/ZUtil/Tactics/SimplifyFractionsLe.v src/Util/ZUtil/Tactics/ZeroBounds.v src/Util/ZUtil/Tactics/Ztestbit.v src/Util/ZUtil/Tactics/PullPush/Modulo.v +src/Util/ZUtil/Zselect.v src/Util/ZUtil/ZSimplify/Autogenerated.v src/Util/ZUtil/ZSimplify/Core.v src/Util/ZUtil/ZSimplify/Simple.v diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v index 7a38e4ba6..3c78ca280 100644 --- a/src/Util/ZUtil/AddGetCarry.v +++ b/src/Util/ZUtil/AddGetCarry.v @@ -1,6 +1,8 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.Prod Crypto.Util.Tactics. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. Require Import Crypto.Util.LetIn. @@ -49,4 +51,23 @@ Module Z. apply add_get_carry_to_add_with_get_carry_cps_gen. Qed. End with_bitwidth. + + Local Hint Unfold Z.add_get_carry_full Z.add_get_carry + Z.add_with_get_carry Z.get_carry Z.add_with_carry. + Lemma add_get_carry_full_mod s x y : + fst (Z.add_get_carry_full s x y) = (x + y) mod s. + Proof. + repeat progress autounfold. + break_match; autorewrite with cancel_pair zsimplify; + reflexivity. + Qed. + + Lemma add_get_carry_full_div s x y : + snd (Z.add_get_carry_full s x y) = (x + y) / s. + Proof. + repeat progress autounfold. + break_match; autorewrite with cancel_pair zsimplify; + reflexivity. + Qed. + End Z. diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v index a74e4b8f4..4a5d3a0ab 100644 --- a/src/Util/ZUtil/Definitions.v +++ b/src/Util/ZUtil/Definitions.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.Decidable. Require Import Crypto.Util.ZUtil.Notations. Local Open Scope Z_scope. @@ -16,4 +17,12 @@ Module Z. := get_carry bitwidth (add_with_carry c x y). Definition add_get_carry (bitwidth : Z) (x y : Z) : Z * Z := add_with_get_carry bitwidth 0 x y. + + (* splits at [bound], not [2^bitwidth]; wrapper to make add_getcarry + work if input is not known to be a power of 2 *) + Definition add_get_carry_full (bound : Z) (x y : Z) : Z * Z + := if dec (2 ^ (Z.log2 bound) = bound) + then add_get_carry (Z.log2 bound) x y + else ((x + y) mod bound, (x + y) / bound). + End Z. diff --git a/src/Util/ZUtil/Zselect.v b/src/Util/ZUtil/Zselect.v new file mode 100644 index 000000000..0166ce6f4 --- /dev/null +++ b/src/Util/ZUtil/Zselect.v @@ -0,0 +1,16 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.Tactics. +Local Open Scope Z_scope. + +Module Z. + Lemma zselect_correct cond zero_case nonzero_case : + Z.zselect cond zero_case nonzero_case = + if dec (cond = 0) then zero_case else nonzero_case. + Proof. + cbv [Z.zselect]; break_match; + try reflexivity; try discriminate. + rewrite <-Z.eqb_neq in *; congruence. + Qed. +End Z.
\ No newline at end of file |