From 7df5033c871aef6172d4e98d42ce00005e24f73e Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 14 May 2017 15:52:56 -0400 Subject: add wrapper for add_get_carry and proofs for add_get_carry and zselect --- src/Util/ZUtil/Definitions.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/Util/ZUtil/Definitions.v') 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. -- cgit v1.2.3