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/Util/BoundedWord.v | |
| 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/Util/BoundedWord.v')
| -rw-r--r-- | src/Util/BoundedWord.v | 4 |
1 files changed, 2 insertions, 2 deletions
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) |