From 68aca8687cd62127eb1dafa2029e59d38db68f3d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 1 Apr 2017 23:00:15 -0400 Subject: 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. --- src/Util/BoundedWord.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util/BoundedWord.v') 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) -- cgit v1.2.3