From d4f6f7373fc1f3a0ba1d1c17547f6d5b556bea5b Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 1 Apr 2017 22:58:27 -0400
Subject: Split off BoundedWord.v from IntegrationTest.v

---
 src/Util/BoundedWord.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 src/Util/BoundedWord.v

(limited to 'src/Util/BoundedWord.v')

diff --git a/src/Util/BoundedWord.v b/src/Util/BoundedWord.v
new file mode 100644
index 000000000..cfd27a231
--- /dev/null
+++ b/src/Util/BoundedWord.v
@@ -0,0 +1,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 bitwidth) n
+  | is_bounded_by (Some (Z.of_nat bitwidth)) bounds
+                  (map wordToZ x)}.
+
+Definition BoundedWordToZ n w b (BW :BoundedWord n w b)
+  : tuple Z n :=  map wordToZ (proj1_sig BW).
-- 
cgit v1.2.3