diff options
| author |  Rob Sloan <varomodt@google.com> | 2016-11-01 12:57:45 -0700 |
|---|---|---|
| committer | Rob Sloan <varomodt@google.com> | 2016-11-01 12:57:45 -0700 |
| commit | ea549915c168d1d4440708b75a35ec450648cf8e (patch) | |
| tree | 54d8ddedf5abb6994b68f32e5139af0d596ecc65 /src/Util/WordUtil.v | |
| parent | c9dc1e35783bdcf9e5bdeaed51c87c23f47dd448 (diff) | |
More of jgross admits, less neg and the cmovs
Diffstat (limited to 'src/Util/WordUtil.v')
| -rw-r--r-- | src/Util/WordUtil.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 5f4dc9c7a..36fd21d28 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -271,12 +271,10 @@ Proof. end. Qed. -Local Notation bounds_2statement wop Zop - := (forall {sz} (x y : word sz), - (0 <= Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y)) - -> Z.log2 (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))) < Z.of_nat sz - -> Z.of_N (wordToN (wop x y)) = (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))))%Z). - +Local Notation bounds_2statement wop Zop := (forall {sz} (x y : word sz), + (0 <= Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y)) + -> (Z.log2 (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))) < Z.of_nat sz) + -> (Z.of_N (wordToN (wop x y)) = (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y)))))%Z). Require Import Crypto.Assembly.WordizeUtil. Require Import Crypto.Assembly.Bounds. |