blob: e5c3720fe60e6a213baea7ad35477bbf46c32b85 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.FixedWordSizes.
Definition BoundedWord n (bitwidth : nat)
(bounds : tuple zrange n) : Type :=
{ 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)
: tuple Z n := map wordToZ (proj1_sig BW).
|
