diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-01 23:00:15 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-01 23:00:15 -0400 |
| commit | 68aca8687cd62127eb1dafa2029e59d38db68f3d (patch) | |
| tree | cdfcf85f2ffafea1dda2bf6ba26ab00ec4a48d3c /src | |
| parent | d4f6f7373fc1f3a0ba1d1c17547f6d5b556bea5b (diff) | |
Fix definition of BoundedWord
We need to take log2, because wordT takes lg(wordsize). We need to pass
None rather than Some, because None means "the original output type of
the function we're reifying is a tuple of Z" (as opposed to a tuple of
words), which is the situation we're in.
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/IntegrationTest.v | 2 | ||||
| -rw-r--r-- | src/Util/BoundedWord.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/Specific/IntegrationTest.v b/src/Specific/IntegrationTest.v index 49fb55969..e37dacdb7 100644 --- a/src/Specific/IntegrationTest.v +++ b/src/Specific/IntegrationTest.v @@ -7,7 +7,7 @@ Require Import Crypto.NewBaseSystem. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Specific.NewBaseSystemTest. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. +Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. Import ListNotations. Section BoundedField25p5. diff --git a/src/Util/BoundedWord.v b/src/Util/BoundedWord.v index cfd27a231..e5c3720fe 100644 --- a/src/Util/BoundedWord.v +++ b/src/Util/BoundedWord.v @@ -5,8 +5,8 @@ Require Import Crypto.Util.FixedWordSizes. Definition BoundedWord n (bitwidth : nat) (bounds : tuple zrange n) : Type := - { x : tuple (wordT bitwidth) n - | is_bounded_by (Some (Z.of_nat bitwidth)) bounds + { x : tuple (wordT (Nat.log2 bitwidth)) n + | is_bounded_by None bounds (map wordToZ x)}. Definition BoundedWordToZ n w b (BW :BoundedWord n w b) |