diff --git a/bv-sized.cabal b/bv-sized.cabal
--- a/bv-sized.cabal
+++ b/bv-sized.cabal
@@ -1,16 +1,16 @@
 name:                bv-sized
-version:             0.5.0
+version:             0.6.0
 category:            Bit Vectors
 synopsis:            a BitVector datatype that is parameterized by the vector width
 description:
   This module defines a width-parameterized 'BitVector' type and various associated
   operations that assume a 2's complement representation.
-homepage:            https://github.com/benjaminselfridge/bv-sized
+homepage:            https://github.com/GaloisInc/bv-sized
 license:             BSD3
 license-file:        LICENSE
 author:              Ben Selfridge
 maintainer:          benselfridge@galois.com
-copyright:           March 2018
+copyright:           Galois Inc., Ben Selfridge March 2018
 build-type:          Simple
 cabal-version:       >=1.10
 extra-source-files:  README.md
@@ -19,12 +19,13 @@
   exposed-modules:     Data.BitVector.Sized
                      , Data.BitVector.Sized.App
                      , Data.BitVector.Sized.BitLayout
+  other-modules:       Data.BitVector.Sized.Internal
   build-depends:       base >= 4.7 && < 5
                      , containers >= 0.5.10 && < 0.6
                      , lens >= 4 && < 5
                      , mtl >= 2 && < 3
                      , parameterized-utils
-                     , prettyclass >= 1.0 && < 2.0
+                     , pretty
                      , random >= 1.1 && < 1.2
                      , QuickCheck >= 2.11 && < 2.12
   hs-source-dirs:      src
@@ -42,6 +43,6 @@
                      , bv-sized
                      , lens >= 4 && < 5
                      , parameterized-utils
-                     , prettyclass >= 1.0 && < 2.0
+                     , pretty
                      , random >= 1.1 && < 1.2
                      , QuickCheck >= 2.11 && < 2.12
diff --git a/cabal.project b/cabal.project
new file mode 100644
--- /dev/null
+++ b/cabal.project
@@ -0,0 +1,2 @@
+packages: .
+          submodules/parameterized-utils
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -1,5 +1,15 @@
 # Changelog for [`bv-sized` package](http://hackage.haskell.org/package/bv-sized)
 
+## 0.6.0 *March 2019*
+* changed WithRepr functions to '
+* added Num, Bits instances
+* bitVector now takes arbitrary Integral argument
+* add 'bitLayoutAssignmentList' function (see haddocks for details
+* Hid BV constructor, exposed BitVector as pattern
+
+## 0.5.1 *August 2018*
+  * fixed github URL
+
 ## 0.5.0 *August 2018*
   * Added a lot of better support for the App module, including a type class for
     embedding BVApp expressions along with associated smart constructors
diff --git a/src/Data/BitVector/Sized.hs b/src/Data/BitVector/Sized.hs
--- a/src/Data/BitVector/Sized.hs
+++ b/src/Data/BitVector/Sized.hs
@@ -1,8 +1,8 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeOperators #-}
 
 {-|
@@ -19,12 +19,12 @@
 
 module Data.BitVector.Sized
   ( -- * BitVector type
-    BitVector(..)
-  , bitVector
+    BitVector, pattern BitVector
+  , bitVector, bitVector'
   , bv0
     -- * Bitwise operations (width-preserving)
-    -- | These are alternative versions of some of the 'Bits' functions where we do
-    -- not need to know the width at compile time. They are all width-preserving.
+    -- | These are alternative versions of some of the 'Data.Bits' functions where we
+    -- do not need to know the width at compile time. They are all width-preserving.
   , bvAnd, bvOr, bvXor
   , bvComplement
   , bvShift, bvShiftL, bvShiftRA, bvShiftRL, bvRotate
@@ -41,10 +41,10 @@
   , bvLTS, bvLTU
     -- * Variable-width operations
     -- | These are functions that involve bit vectors of different lengths.
-  , bvConcat, (<:>), bvConcatMany, bvConcatManyWithRepr
-  , bvExtract, bvExtractWithRepr
-  , bvZext, bvZextWithRepr
-  , bvSext, bvSextWithRepr
+  , bvConcat, (<:>), bvConcatMany, bvConcatMany'
+  , bvExtract, bvExtract'
+  , bvZext, bvZext'
+  , bvSext, bvSext'
     -- * Conversions to Integer
   , bvIntegerU
   , bvIntegerS
@@ -52,391 +52,4 @@
   , bvGetBytesU
   ) where
 
-import Data.Bits
-import Data.Ix
-import Data.Parameterized
-import GHC.TypeLits
-import Numeric
-import System.Random
-import Test.QuickCheck (Arbitrary(..), choose)
-import Text.PrettyPrint.HughesPJClass
-import Text.Printf
-import Unsafe.Coerce (unsafeCoerce)
-
-----------------------------------------
--- BitVector data type definitions
-
--- | BitVector datatype, parameterized by width.
-data BitVector (w :: Nat) :: * where
-  BV :: NatRepr w -> Integer -> BitVector w
-
--- | Construct a bit vector with a particular width, where the width is inferrable
--- from the type context. The 'Integer' input (an unbounded data type, hence with an
--- infinite-width bit representation), whether positive or negative, is silently
--- truncated to fit into the number of bits demanded by the return type.
---
--- >>> bitVector 0xA :: BitVector 4
--- 0xa
--- >>> bitVector 0xA :: BitVector 2
--- 0x2
-bitVector :: KnownNat w => Integer -> BitVector w
-bitVector x = BV wRepr (truncBits width (fromIntegral x))
-  where wRepr = knownNat
-        width = natValue wRepr
-
--- | The zero bitvector with width 0.
-bv0 :: BitVector 0
-bv0 = bitVector 0
-
-----------------------------------------
--- BitVector -> Integer functions
-
--- | Unsigned interpretation of a bit vector as a (positive) Integer.
-bvIntegerU :: BitVector w -> Integer
-bvIntegerU (BV _ x) = x
-
--- | Signed interpretation of a bit vector as an Integer.
-bvIntegerS :: BitVector w -> Integer
-bvIntegerS bv = if bvTestBit bv (width - 1)
-                then bvIntegerU bv - (1 `shiftL` width)
-                else bvIntegerU bv
-  where width = bvWidth bv
-
-----------------------------------------
--- BitVector w operations (fixed width)
-
--- | Bitwise and.
-bvAnd :: BitVector w -> BitVector w -> BitVector w
-bvAnd (BV wRepr x) (BV _ y) = BV wRepr (x .&. y)
-
--- | Bitwise or.
-bvOr :: BitVector w -> BitVector w -> BitVector w
-bvOr (BV wRepr x) (BV _ y) = BV wRepr (x .|. y)
-
--- | Bitwise xor.
-bvXor :: BitVector w -> BitVector w -> BitVector w
-bvXor (BV wRepr x) (BV _ y) = BV wRepr (x `xor` y)
-
--- | Bitwise complement (flip every bit).
-bvComplement :: BitVector w -> BitVector w
-bvComplement (BV wRepr x) = BV wRepr (truncBits width (complement x))
-  where width = natValue wRepr
-
--- | Bitwise shift. Uses an arithmetic right shift.
-bvShift :: BitVector w -> Int -> BitVector w
-bvShift bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` shf))
-  where width = natValue wRepr
-        x     = bvIntegerS bv -- arithmetic right shift when negative
-
-toPos :: Int -> Int
-toPos x | x < 0 = 0
-toPos x = x
-
--- | Left shift.
-bvShiftL :: BitVector w -> Int -> BitVector w
-bvShiftL bv shf = bvShift bv (toPos shf)
-
--- | Right arithmetic shift.
-bvShiftRA :: BitVector w -> Int -> BitVector w
-bvShiftRA bv shf = bvShift bv (- (toPos shf))
-
--- | Right logical shift.
-bvShiftRL :: BitVector w -> Int -> BitVector w
-bvShiftRL bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` (- toPos shf)))
-  where width = natValue wRepr
-        x     = bvIntegerU bv
-
--- | Bitwise rotate.
-bvRotate :: BitVector w -> Int -> BitVector w
-bvRotate bv rot' = leftChunk `bvOr` rightChunk
-  where rot = rot' `mod` bvWidth bv
-        leftChunk = bvShift bv rot
-        rightChunk = bvShift bv (rot - bvWidth bv)
-
--- | Get the width of a 'BitVector'.
-bvWidth :: BitVector w -> Int
-bvWidth (BV wRepr _) = fromIntegral (natValue wRepr)
-
--- | Test if a particular bit is set.
-bvTestBit :: BitVector w -> Int -> Bool
-bvTestBit (BV _ x) b = testBit x b
-
--- | Get the number of 1 bits in a 'BitVector'.
-bvPopCount :: BitVector w -> Int
-bvPopCount (BV _ x) = popCount x
-
--- | Truncate a bit vector to a particular width given at runtime, while keeping the
--- type-level width constant.
-bvTruncBits :: BitVector w -> Int -> BitVector w
-bvTruncBits (BV wRepr x) b = BV wRepr (truncBits b x)
-
-----------------------------------------
--- BitVector w arithmetic operations (fixed width)
-
--- | Bitwise add.
-bvAdd :: BitVector w -> BitVector w -> BitVector w
-bvAdd (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x + y))
-  where width = natValue wRepr
-
--- | Bitwise multiply.
-bvMul :: BitVector w -> BitVector w -> BitVector w
-bvMul (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x * y))
-  where width = natValue wRepr
-
--- | Bitwise division (unsigned). Rounds to zero.
-bvQuotU :: BitVector w -> BitVector w -> BitVector w
-bvQuotU (BV wRepr x) (BV _ y) = BV wRepr (x `quot` y)
-
--- | Bitwise division (signed). Rounds to zero (not negative infinity).
-bvQuotS :: BitVector w -> BitVector w -> BitVector w
-bvQuotS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `quot` y))
-  where x = bvIntegerS bv1
-        y = bvIntegerS bv2
-        width = natValue wRepr
-
--- | Bitwise remainder after division (unsigned), when rounded to zero.
-bvRemU :: BitVector w -> BitVector w -> BitVector w
-bvRemU (BV wRepr x) (BV _ y) = BV wRepr (x `rem` y)
-
--- | Bitwise remainder after  division (signed), when rounded to zero (not negative
--- infinity).
-bvRemS :: BitVector w -> BitVector w -> BitVector w
-bvRemS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `rem` y))
-  where x = bvIntegerS bv1
-        y = bvIntegerS bv2
-        width = natValue wRepr
-
--- | Bitwise absolute value.
-bvAbs :: BitVector w -> BitVector w
-bvAbs bv@(BV wRepr _) = BV wRepr abs_x
-  where width = natValue wRepr
-        x     = bvIntegerS bv
-        abs_x = truncBits width (abs x) -- this is necessary
-
--- | Bitwise negation.
-bvNegate :: BitVector w -> BitVector w
-bvNegate (BV wRepr x) = BV wRepr (truncBits width (-x))
-  where width = fromIntegral (natValue wRepr) :: Integer
-
--- | Get the sign bit as a 'BitVector'.
-bvSignum :: BitVector w -> BitVector w
-bvSignum bv@(BV wRepr _) = bvShift bv (1 - width) `bvAnd` BV wRepr 0x1
-  where width = fromIntegral (natValue wRepr)
-
--- | Signed less than.
-bvLTS :: BitVector w -> BitVector w -> Bool
-bvLTS bv1 bv2 = bvIntegerS bv1 < bvIntegerS bv2
-
--- | Unsigned less than.
-bvLTU :: BitVector w -> BitVector w -> Bool
-bvLTU bv1 bv2 = bvIntegerU bv1 < bvIntegerU bv2
-
-----------------------------------------
--- Width-changing operations
-
--- | Concatenate two bit vectors.
---
--- >>> (0xAA :: BitVector 8) `bvConcat` (0xBCDEF0 :: BitVector 24)
--- 0xaabcdef0
--- >>> :type it
--- it :: BitVector 32
---
--- Note that the first argument gets placed in the higher-order bits. The above
--- example should be illustrative enough.
-bvConcat :: BitVector v -> BitVector w -> BitVector (v+w)
-bvConcat (BV hiWRepr hi) (BV loWRepr lo) =
-  BV (hiWRepr `addNat` loWRepr) ((hi `shiftL` loWidth) .|. lo)
-  where loWidth = fromIntegral (natValue loWRepr)
-
--- | Infix 'bvConcat'.
-(<:>) :: BitVector v -> BitVector w -> BitVector (v+w)
-(<:>) = bvConcat
-
-bvConcatSome :: Some BitVector -> Some BitVector -> Some BitVector
-bvConcatSome (Some bv1) (Some bv2) = Some (bv2 <:> bv1)
-
--- | Concatenate a list of 'BitVector's into a 'BitVector' of arbitrary width. The ordering is little endian:
---
--- >>> bvConcatMany [0xAA :: BitVector 8, 0xBB] :: BitVector 16
--- 0xbbaa
--- >>> bvConcatMany [0xAA :: BitVector 8, 0xBB, 0xCC] :: BitVector 16
--- 0xbbaa
---
--- If the sum of the widths of the input 'BitVector's exceeds the output width, we
--- ignore the tail end of the list.
-bvConcatMany :: KnownNat w' => [BitVector w] -> BitVector w'
-bvConcatMany = bvConcatManyWithRepr knownNat
-
--- | 'bvConcatMany' with an explicit 'NatRepr'.
-bvConcatManyWithRepr :: NatRepr w' -> [BitVector w] -> BitVector w'
-bvConcatManyWithRepr wRepr bvs =
-  viewSome (bvZextWithRepr wRepr) $ foldl bvConcatSome (Some bv0) (Some <$> bvs)
-
-infixl 6 <:>
-
--- | Slice out a smaller bit vector from a larger one. The lowest significant bit is
--- given explicitly as an argument of type 'Int', and the length of the slice is
--- inferred from a type-level context.
---
--- >>> bvExtract 12 (0xAABCDEF0 :: BitVector 32) :: BitVector 8
--- 0xcd
---
--- Note that 'bvExtract' does not do any bounds checking whatsoever; if you try and
--- extract bits that aren't present in the input, you will get 0's.
-bvExtract :: forall w w' . (KnownNat w')
-          => Int
-          -> BitVector w
-          -> BitVector w'
-bvExtract pos bv = bitVector xShf
-  where (BV _ xShf) = bvShift bv (- pos)
-
--- | Unconstrained variant of 'bvExtract' with an explicit 'NatRepr' argument.
-bvExtractWithRepr :: NatRepr w'
-                  -> Int
-                  -> BitVector w
-                  -> BitVector w'
-bvExtractWithRepr repr pos bv = BV repr (truncBits width xShf)
-  where (BV _ xShf) = bvShift bv (- pos)
-        width = natValue repr
-
--- | Zero-extend a vector to one of greater length. If given an input of greater
--- length than the output type, this performs a truncation.
-bvZext :: forall w w' . KnownNat w'
-       => BitVector w
-       -> BitVector w'
-bvZext (BV _ x) = bitVector x
-
--- | Unconstrained variant of 'bvZext' with an explicit 'NatRepr' argument.
-bvZextWithRepr :: NatRepr w'
-               -> BitVector w
-               -> BitVector w'
-bvZextWithRepr repr (BV _ x) = BV repr (truncBits width x)
-  where width = natValue repr
-
--- | Sign-extend a vector to one of greater length. If given an input of greater
--- length than the output type, this performs a truncation.
-bvSext :: forall w w' . KnownNat w'
-       => BitVector w
-       -> BitVector w'
-bvSext bv = bitVector (bvIntegerS bv)
-
--- | Unconstrained variant of 'bvSext' with an explicit 'NatRepr' argument.
-bvSextWithRepr :: NatRepr w'
-               -> BitVector w
-               -> BitVector w'
-bvSextWithRepr repr bv = BV repr (truncBits width (bvIntegerS bv))
-  where width = natValue repr
-
-----------------------------------------
--- Byte decomposition
-
--- | Given a 'BitVector' of arbitrary length, decompose it into a list of bytes. Uses
--- an unsigned interpretation of the input vector, so if you ask for more bytes that
--- the 'BitVector' contains, you get zeros. The result is little-endian, so the first
--- element of the list will be the least significant byte of the input vector.
-bvGetBytesU :: Int -> BitVector w -> [BitVector 8]
-bvGetBytesU n _ | n <= 0 = []
-bvGetBytesU n bv = bvExtract 0 bv : bvGetBytesU (n-1) (bvShiftRL bv 8)
-
-----------------------------------------
--- Bits
-
--- | Mask for a specified number of lower bits.
-lowMask :: (Integral a, Bits b) => a -> b
-lowMask numBits = complement (complement zeroBits `shiftL` fromIntegral numBits)
-
--- | Truncate to a specified number of lower bits.
-truncBits :: (Integral a, Bits b) => a -> b -> b
-truncBits width b = b .&. lowMask width
-
-----------------------------------------
--- Class instances
-$(return [])
-
-instance Show (BitVector w) where
-  show (BV _ x) = "0x" ++ showHex x ""
-
-instance KnownNat w => Read (BitVector w) where
-  readsPrec s =
-    (fmap . fmap) (\(a,s') -> (bitVector a, s')) (readsPrec s :: ReadS Integer)
-
-instance ShowF BitVector
-
-instance Eq (BitVector w) where
-  (BV _ x) == (BV _ y) = x == y
-
-instance EqF BitVector where
-  (BV _ x) `eqF` (BV _ y) = x == y
-
-instance Ord (BitVector w) where
-  (BV _ x) `compare` (BV _ y) = x `compare` y
-
-instance OrdF BitVector where
-  (BV xRepr x) `compareF` (BV yRepr y) =
-    case xRepr `compareF` yRepr of
-      EQF -> fromOrdering (x `compare` y)
-      cmp -> cmp
-
-instance TestEquality BitVector where
-  testEquality (BV wRepr x) (BV wRepr' y) =
-    if natValue wRepr == natValue wRepr' && x == y
-    then Just (unsafeCoerce (Refl :: a :~: a))
-    else Nothing
-
-instance KnownNat w => Bits (BitVector w) where
-  (.&.)        = bvAnd
-  (.|.)        = bvOr
-  xor          = bvXor
-  complement   = bvComplement
-  shift        = bvShift
-  rotate       = bvRotate
-  bitSize      = bvWidth
-  bitSizeMaybe = Just . bvWidth
-  isSigned     = const False
-  testBit      = bvTestBit
-  bit          = bitVector . bit
-  popCount     = bvPopCount
-
-instance KnownNat w => FiniteBits (BitVector w) where
-  finiteBitSize = bvWidth
-
-instance KnownNat w => Num (BitVector w) where
-  (+)         = bvAdd
-  (*)         = bvMul
-  abs         = bvAbs
-  signum      = bvSignum
-  fromInteger = bitVector
-  negate      = bvNegate
-
-instance KnownNat w => Enum (BitVector w) where
-  toEnum   = bitVector . fromIntegral
-  fromEnum = fromIntegral . bvIntegerU
-
-instance KnownNat w => Ix (BitVector w) where
-  range (lo, hi) = bitVector <$> [bvIntegerU lo .. bvIntegerU hi]
-  index (lo, hi) bv = index (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv)
-  inRange (lo, hi) bv = inRange (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv)
-
-instance KnownNat w => Bounded (BitVector w) where
-  minBound = bitVector 0
-  maxBound = bitVector (-1)
-
-instance KnownNat w => Arbitrary (BitVector w) where
-  arbitrary = choose (minBound, maxBound)
-
-instance KnownNat w => Random (BitVector w) where
-  randomR (bvLo, bvHi) gen =
-    let (x, gen') = randomR (bvIntegerU bvLo, bvIntegerU bvHi) gen
-    in (bitVector x, gen')
-  random gen =
-    let (x, gen') = random gen
-    in (bitVector x, gen')
-
-prettyHex :: (Integral a, PrintfArg a, Show a) => a -> Integer -> String
-prettyHex width val = printf format val width
-  where numDigits = (width+3) `quot` 4
-        format = "0x%." ++ show numDigits ++ "x<%d>"
-
-instance Pretty (BitVector w) where
-  -- | Pretty print a bit vector (shows its width)
-  pPrint (BV wRepr x) = text $ prettyHex (natValue wRepr) x
+import Data.BitVector.Sized.Internal
diff --git a/src/Data/BitVector/Sized/App.hs b/src/Data/BitVector/Sized/App.hs
--- a/src/Data/BitVector/Sized/App.hs
+++ b/src/Data/BitVector/Sized/App.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
@@ -48,6 +49,9 @@
   , quotsE
   , remuE
   , remsE
+  , negateE
+  , absE
+  , signumE
   , sllE
   , srlE
   , sraE
@@ -56,9 +60,9 @@
   , ltuE
   , ltsE
   -- ** Width-changing
-  , zextE, zextEWithRepr
-  , sextE, sextEWithRepr
-  , extractE, extractEWithRepr
+  , zextE, zextE'
+  , sextE, sextE'
+  , extractE, extractE'
   , concatE
   -- ** Control
   , iteE
@@ -66,6 +70,7 @@
 
 import Control.Monad.Identity
 import Data.BitVector.Sized
+import Data.Bits
 import Data.Parameterized
 import Data.Parameterized.TH.GADT
 import Foreign.Marshal.Utils (fromBool)
@@ -96,6 +101,9 @@
   QuotSApp :: !(expr w) -> !(expr w) -> BVApp expr w
   RemUApp  :: !(expr w) -> !(expr w) -> BVApp expr w
   RemSApp  :: !(expr w) -> !(expr w) -> BVApp expr w
+  NegateApp :: !(expr w) -> BVApp expr w
+  AbsApp   :: !(expr w) -> BVApp expr w
+  SignumApp :: !(expr w) -> BVApp expr w
 
   -- Comparisons
   EqApp  :: !(expr w) -> !(expr w) -> BVApp expr 1
@@ -120,6 +128,9 @@
 instance TestEquality expr => Eq (BVApp expr w) where
   (==) = \x y -> isJust (testEquality x y)
 
+instance TestEquality expr => EqF (BVApp expr) where
+  eqF = (==)
+
 instance OrdF expr => OrdF (BVApp expr) where
   compareF = $(structuralTypeOrd [t|BVApp|]
                 [ (AnyType `TypeApp` AnyType, [|compareF|]) ])
@@ -160,12 +171,15 @@
 evalBVAppM eval (QuotUApp e1 e2) = bvQuotU  <$> eval e1 <*> eval e2
 evalBVAppM eval (RemSApp  e1 e2) = bvRemS   <$> eval e1 <*> eval e2
 evalBVAppM eval (RemUApp  e1 e2) = bvRemU   <$> eval e1 <*> eval e2
+evalBVAppM eval (NegateApp e) = bvNegate <$> eval e
+evalBVAppM eval (AbsApp e) = bvAbs <$> eval e
+evalBVAppM eval (SignumApp e) = bvSignum <$> eval e
 evalBVAppM eval (EqApp  e1 e2) = fromBool <$> ((==)  <$> eval e1 <*> eval e2)
 evalBVAppM eval (LtuApp e1 e2) = fromBool <$> (bvLTU <$> eval e1 <*> eval e2)
 evalBVAppM eval (LtsApp e1 e2) = fromBool <$> (bvLTS <$> eval e1 <*> eval e2)
-evalBVAppM eval (ZExtApp wRepr e) = bvZextWithRepr wRepr <$> eval e
-evalBVAppM eval (SExtApp wRepr e) = bvSextWithRepr wRepr <$> eval e
-evalBVAppM eval (ExtractApp wRepr base e) = bvExtractWithRepr wRepr base <$> eval e
+evalBVAppM eval (ZExtApp wRepr e) = bvZext' wRepr <$> eval e
+evalBVAppM eval (SExtApp wRepr e) = bvSext' wRepr <$> eval e
+evalBVAppM eval (ExtractApp wRepr base e) = bvExtract' wRepr base <$> eval e
 evalBVAppM eval (ConcatApp e1 e2) = do
   e1Val <- eval e1
   e2Val <- eval e2
@@ -186,6 +200,31 @@
 class BVExpr (expr :: Nat -> *) where
   appExpr :: BVApp expr w -> expr w
 
+instance (KnownNat w, BVExpr expr) => Num (BVApp expr w) where
+  app1 + app2 = AddApp (appExpr app1) (appExpr app2)
+  app1 * app2 = MulApp (appExpr app1) (appExpr app2)
+  abs app = AbsApp (appExpr app)
+  signum app = SignumApp (appExpr app)
+  fromInteger x = LitBVApp (fromInteger x)
+  negate app = NegateApp (appExpr app)
+  app1 - app2 = SubApp (appExpr app1) (appExpr app2)
+
+-- TODO: finish
+instance (KnownNat w, BVExpr expr, TestEquality expr) => Bits (BVApp expr w) where
+  app1 .&. app2 = AndApp (appExpr app1) (appExpr app2)
+  app1 .|. app2 = OrApp (appExpr app1) (appExpr app2)
+  app1 `xor` app2 = XorApp (appExpr app1) (appExpr app2)
+  complement app = NotApp (appExpr app)
+  shiftL app x = SllApp (appExpr app) (litBV (bitVector x))
+  shiftR app x = SraApp (appExpr app) (litBV (bitVector x))
+  rotate = undefined
+  bitSize = undefined
+  bitSizeMaybe = undefined
+  isSigned = undefined
+  testBit = undefined
+  bit = undefined
+  popCount = undefined
+
 -- | Literal bit vector.
 litBV :: BVExpr expr => BitVector w -> expr w
 litBV = appExpr . LitBVApp
@@ -214,27 +253,36 @@
 subE :: BVExpr expr => expr w -> expr w -> expr w
 subE e1 e2 = appExpr (SubApp e1 e2)
 
--- | Signed multiply two 'BitVectors', doubling the width of the result to hold all
+-- | Signed multiply two 'BitVector's, doubling the width of the result to hold all
 -- arithmetic overflow bits.
 mulE :: BVExpr expr => expr w -> expr w -> expr w
 mulE e1 e2 = appExpr (MulApp e1 e2)
 
--- | Signed divide two 'BitVectors', rounding to zero.
+-- | Signed divide two 'BitVector's, rounding to zero.
 quotsE :: BVExpr expr => expr w -> expr w -> expr w
 quotsE e1 e2 = appExpr (QuotSApp e1 e2)
 
--- | Unsigned divide two 'BitVectors', rounding to zero.
+-- | Unsigned divide two 'BitVector's, rounding to zero.
 quotuE :: BVExpr expr => expr w -> expr w -> expr w
 quotuE e1 e2 = appExpr (QuotUApp e1 e2)
 
--- | Remainder after signed division of two 'BitVectors', when rounded to zero.
+-- | Remainder after signed division of two 'BitVector's, when rounded to zero.
 remsE :: BVExpr expr => expr w -> expr w -> expr w
 remsE e1 e2 = appExpr (RemSApp e1 e2)
 
--- | Remainder after unsigned division of two 'BitVectors', when rounded to zero.
+-- | Remainder after unsigned division of two 'BitVector's, when rounded to zero.
 remuE :: BVExpr expr => expr w -> expr w -> expr w
 remuE e1 e2 = appExpr (RemUApp e1 e2)
 
+negateE :: BVExpr expr => expr w -> expr w
+negateE e = appExpr (NegateApp e)
+
+absE :: BVExpr expr => expr w -> expr w
+absE e = appExpr (AbsApp e)
+
+signumE :: BVExpr expr => expr w -> expr w
+signumE e = appExpr (SignumApp e)
+
 -- | Left logical shift the first expression by the second.
 sllE :: BVExpr expr => expr w -> expr w -> expr w
 sllE e1 e2 = appExpr (SllApp e1 e2)
@@ -264,24 +312,24 @@
 zextE e = appExpr (ZExtApp knownNat e)
 
 -- | Zero-extension with an explicit width argument
-zextEWithRepr :: BVExpr expr => NatRepr w' -> expr w -> expr w'
-zextEWithRepr repr e = appExpr (ZExtApp repr e)
+zextE' :: BVExpr expr => NatRepr w' -> expr w -> expr w'
+zextE' repr e = appExpr (ZExtApp repr e)
 
 -- | Sign-extension
 sextE :: (BVExpr expr, KnownNat w') => expr w -> expr w'
 sextE e = appExpr (SExtApp knownNat e)
 
 -- | Sign-extension with an explicit width argument
-sextEWithRepr :: BVExpr expr => NatRepr w' -> expr w -> expr w'
-sextEWithRepr repr e = appExpr (SExtApp repr e)
+sextE' :: BVExpr expr => NatRepr w' -> expr w -> expr w'
+sextE' repr e = appExpr (SExtApp repr e)
 
 -- | Extract bits
 extractE :: (BVExpr expr, KnownNat w') => Int -> expr w -> expr w'
 extractE base e = appExpr (ExtractApp knownNat base e)
 
 -- | Extract bits with an explicit width argument
-extractEWithRepr :: BVExpr expr => NatRepr w' -> Int -> expr w -> expr w'
-extractEWithRepr wRepr base e = appExpr (ExtractApp wRepr base e)
+extractE' :: BVExpr expr => NatRepr w' -> Int -> expr w -> expr w'
+extractE' wRepr base e = appExpr (ExtractApp wRepr base e)
 
 -- | Concatenation
 concatE :: BVExpr expr => expr w -> expr w' -> expr (w+w')
diff --git a/src/Data/BitVector/Sized/BitLayout.hs b/src/Data/BitVector/Sized/BitLayout.hs
--- a/src/Data/BitVector/Sized/BitLayout.hs
+++ b/src/Data/BitVector/Sized/BitLayout.hs
@@ -32,9 +32,11 @@
   , extract
     -- * Lenses
   , layoutLens, layoutsLens
+    -- * Utilities
+  , bitLayoutAssignmentList
   ) where
 
-import Data.BitVector.Sized
+import Data.BitVector.Sized.Internal
 import Data.Foldable
 import qualified Data.Functor.Product as P
 import Control.Lens (lens, Simple, Lens)
@@ -198,8 +200,8 @@
        -> BitVector s
        -> BitVector t
        -> BitVector t
-bvOrAt start sVec tVec@(BV tRepr _) =
-  (bvZextWithRepr tRepr sVec `bvShift` start) `bvOr` tVec
+bvOrAt start sVec tVec@(BitVector tRepr _) =
+  (bvZext' tRepr sVec `bvShift` start) `bvOr` tVec
 
 -- | Given a list of 'Chunk's, inject each chunk from a source 'BitVector' @s@ into a
 -- target 'BitVector' @t@.
@@ -230,7 +232,7 @@
              -> BitVector s
 extractChunk sRepr sStart (Some (Chunk chunkRepr chunkStart)) tVec =
   bvShift extractedChunk sStart
-  where extractedChunk = bvZextWithRepr sRepr (bvExtractWithRepr chunkRepr chunkStart tVec)
+  where extractedChunk = bvZext' sRepr (bvExtract' chunkRepr chunkStart tVec)
 
 extractAll :: NatRepr s       -- ^ determines width of output vector
            -> Int             -- ^ current position in output vector
@@ -241,7 +243,7 @@
 extractAll sRepr outStart (chk@(Some (Chunk chunkRepr _)) : chunks) tVec =
   extractChunk sRepr outStart chk tVec `bvOr`
   extractAll sRepr (outStart + chunkWidth) chunks tVec
-  where chunkWidth = fromInteger (natValue chunkRepr)
+  where chunkWidth = fromInteger (intValue chunkRepr)
 
 -- | Use a 'BitLayout' to extract a smaller vector from a larger one.
 extract :: BitLayout t s -- ^ The layout
@@ -260,3 +262,22 @@
   (\bv bvFlds -> ifoldr (\_ (P.Pair fld layout) bv' -> inject layout bv' fld)
                  bv
                  (izipWith (const P.Pair) bvFlds layouts))
+
+-- | From a `BitLayout`, get a list representing the position of each bit from the
+-- source to the target. The list
+--
+-- @
+-- [3,4,5,10,11,12,13]
+-- @
+--
+-- means that bit 0 of the source is placed in bit 3 of the target, bit 1 of the
+-- source is placed in bit 4 of the target, etc.
+
+bitLayoutAssignmentList :: BitLayout t s -> [Int]
+bitLayoutAssignmentList (BitLayout _ _ someChunks) = reverse (bitLayoutAssignmentList' (toList someChunks))
+
+bitLayoutAssignmentList' :: [Some Chunk] -> [Int]
+bitLayoutAssignmentList' [] = []
+bitLayoutAssignmentList' (Some (Chunk wRepr start):rst) =
+  reverse [start..start+w-1] ++ bitLayoutAssignmentList' rst
+  where w = fromIntegral (natValue wRepr)
diff --git a/src/Data/BitVector/Sized/Internal.hs b/src/Data/BitVector/Sized/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/BitVector/Sized/Internal.hs
@@ -0,0 +1,419 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-|
+Module      : Data.BitVector.Sized
+Copyright   : (c) Galois Inc. 2018
+License     : BSD-3
+Maintainer  : benselfridge@galois.com
+Stability   : experimental
+Portability : portable
+
+This module defines a width-parameterized 'BitVector' type and various associated
+operations that assume a 2's complement representation.
+-}
+
+module Data.BitVector.Sized.Internal where
+
+import Data.Bits
+import Data.Ix
+import Data.Parameterized
+import GHC.TypeLits
+import Numeric
+import System.Random
+import Test.QuickCheck (Arbitrary(..), choose)
+import Text.PrettyPrint.HughesPJClass
+import Text.Printf
+import Unsafe.Coerce (unsafeCoerce)
+
+----------------------------------------
+-- BitVector data type definitions
+
+-- | BitVector datatype, parameterized by width.
+data BitVector (w :: Nat) :: * where
+  BV :: NatRepr w -> Integer -> BitVector w
+
+-- | 'BitVector' can be treated as a constructor for pattern matching, but to build
+-- one you must use the smart constructor `bitVector`.
+pattern BitVector :: NatRepr w -> Integer -> BitVector w
+pattern BitVector wRepr x <- BV wRepr x
+{-# COMPLETE BitVector #-}
+
+-- | Construct a bit vector with a particular width, where the width is inferrable
+-- from the type context. The input (an unbounded data type, hence with an
+-- infinite-width bit representation), whether positive or negative, is silently
+-- truncated to fit into the number of bits demanded by the return type.
+--
+-- >>> bitVector 0xA :: BitVector 4
+-- 0xa
+-- >>> bitVector 0xA :: BitVector 2
+-- 0x2
+bitVector :: (Integral a, KnownNat w) => a -> BitVector w
+bitVector x = bitVector' knownNat x
+
+-- | Like 'bitVector', but with an explict 'NatRepr'.
+bitVector' :: Integral a => NatRepr w -> a -> BitVector w
+bitVector' wRepr x = BV wRepr (truncBits width (fromIntegral x))
+  where width = natValue wRepr
+
+-- | The zero bitvector with width 0.
+bv0 :: BitVector 0
+bv0 = bitVector (0 :: Integer)
+
+----------------------------------------
+-- BitVector -> Integer functions
+
+-- | Unsigned interpretation of a bit vector as a (positive) Integer.
+bvIntegerU :: BitVector w -> Integer
+bvIntegerU (BV _ x) = x
+
+-- | Signed interpretation of a bit vector as an Integer.
+bvIntegerS :: BitVector w -> Integer
+bvIntegerS bv = if bvTestBit bv (width - 1)
+                then bvIntegerU bv - (1 `shiftL` width)
+                else bvIntegerU bv
+  where width = bvWidth bv
+
+----------------------------------------
+-- BitVector w operations (fixed width)
+
+-- | Bitwise and.
+bvAnd :: BitVector w -> BitVector w -> BitVector w
+bvAnd (BV wRepr x) (BV _ y) = BV wRepr (x .&. y)
+
+-- | Bitwise or.
+bvOr :: BitVector w -> BitVector w -> BitVector w
+bvOr (BV wRepr x) (BV _ y) = BV wRepr (x .|. y)
+
+-- | Bitwise xor.
+bvXor :: BitVector w -> BitVector w -> BitVector w
+bvXor (BV wRepr x) (BV _ y) = BV wRepr (x `xor` y)
+
+-- | Bitwise complement (flip every bit).
+bvComplement :: BitVector w -> BitVector w
+bvComplement (BV wRepr x) = BV wRepr (truncBits width (complement x))
+  where width = natValue wRepr
+
+-- | Bitwise shift. Uses an arithmetic right shift.
+bvShift :: BitVector w -> Int -> BitVector w
+bvShift bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` shf))
+  where width = natValue wRepr
+        x     = bvIntegerS bv -- arithmetic right shift when negative
+
+toPos :: Int -> Int
+toPos x | x < 0 = 0
+toPos x = x
+
+-- | Left shift.
+bvShiftL :: BitVector w -> Int -> BitVector w
+bvShiftL bv shf = bvShift bv (toPos shf)
+
+-- | Right arithmetic shift.
+bvShiftRA :: BitVector w -> Int -> BitVector w
+bvShiftRA bv shf = bvShift bv (- (toPos shf))
+
+-- | Right logical shift.
+bvShiftRL :: BitVector w -> Int -> BitVector w
+bvShiftRL bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` (- toPos shf)))
+  where width = natValue wRepr
+        x     = bvIntegerU bv
+
+-- | Bitwise rotate.
+bvRotate :: BitVector w -> Int -> BitVector w
+bvRotate bv rot' = leftChunk `bvOr` rightChunk
+  where rot = rot' `mod` bvWidth bv
+        leftChunk = bvShift bv rot
+        rightChunk = bvShift bv (rot - bvWidth bv)
+
+-- | Get the width of a 'BitVector'.
+bvWidth :: BitVector w -> Int
+bvWidth (BV wRepr _) = fromIntegral (natValue wRepr)
+
+-- | Test if a particular bit is set.
+bvTestBit :: BitVector w -> Int -> Bool
+bvTestBit (BV _ x) b = testBit x b
+
+-- | Get the number of 1 bits in a 'BitVector'.
+bvPopCount :: BitVector w -> Int
+bvPopCount (BV _ x) = popCount x
+
+-- | Truncate a bit vector to a particular width given at runtime, while keeping the
+-- type-level width constant.
+bvTruncBits :: BitVector w -> Int -> BitVector w
+bvTruncBits (BV wRepr x) b = BV wRepr (truncBits b x)
+
+----------------------------------------
+-- BitVector w arithmetic operations (fixed width)
+
+-- | Bitwise add.
+bvAdd :: BitVector w -> BitVector w -> BitVector w
+bvAdd (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x + y))
+  where width = natValue wRepr
+
+-- | Bitwise multiply.
+bvMul :: BitVector w -> BitVector w -> BitVector w
+bvMul (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x * y))
+  where width = natValue wRepr
+
+-- | Bitwise division (unsigned). Rounds to zero.
+bvQuotU :: BitVector w -> BitVector w -> BitVector w
+bvQuotU (BV wRepr x) (BV _ y) = BV wRepr (x `quot` y)
+
+-- | Bitwise division (signed). Rounds to zero (not negative infinity).
+bvQuotS :: BitVector w -> BitVector w -> BitVector w
+bvQuotS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `quot` y))
+  where x = bvIntegerS bv1
+        y = bvIntegerS bv2
+        width = natValue wRepr
+
+-- | Bitwise remainder after division (unsigned), when rounded to zero.
+bvRemU :: BitVector w -> BitVector w -> BitVector w
+bvRemU (BV wRepr x) (BV _ y) = BV wRepr (x `rem` y)
+
+-- | Bitwise remainder after  division (signed), when rounded to zero (not negative
+-- infinity).
+bvRemS :: BitVector w -> BitVector w -> BitVector w
+bvRemS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `rem` y))
+  where x = bvIntegerS bv1
+        y = bvIntegerS bv2
+        width = natValue wRepr
+
+-- | Bitwise absolute value.
+bvAbs :: BitVector w -> BitVector w
+bvAbs bv@(BV wRepr _) = BV wRepr abs_x
+  where width = natValue wRepr
+        x     = bvIntegerS bv
+        abs_x = truncBits width (abs x) -- this is necessary
+
+-- | Bitwise negation.
+bvNegate :: BitVector w -> BitVector w
+bvNegate (BV wRepr x) = BV wRepr (truncBits width (-x))
+  where width = fromIntegral (natValue wRepr) :: Integer
+
+-- | Get the sign bit as a 'BitVector'.
+bvSignum :: BitVector w -> BitVector w
+bvSignum bv@(BV wRepr _) = bvShift bv (1 - width) `bvAnd` BV wRepr 0x1
+  where width = fromIntegral (natValue wRepr)
+
+-- | Signed less than.
+bvLTS :: BitVector w -> BitVector w -> Bool
+bvLTS bv1 bv2 = bvIntegerS bv1 < bvIntegerS bv2
+
+-- | Unsigned less than.
+bvLTU :: BitVector w -> BitVector w -> Bool
+bvLTU bv1 bv2 = bvIntegerU bv1 < bvIntegerU bv2
+
+----------------------------------------
+-- Width-changing operations
+
+-- | Concatenate two bit vectors.
+--
+-- >>> (0xAA :: BitVector 8) `bvConcat` (0xBCDEF0 :: BitVector 24)
+-- 0xaabcdef0
+-- >>> :type it
+-- it :: BitVector 32
+--
+-- Note that the first argument gets placed in the higher-order bits. The above
+-- example should be illustrative enough.
+bvConcat :: BitVector v -> BitVector w -> BitVector (v+w)
+bvConcat (BV hiWRepr hi) (BV loWRepr lo) =
+  BV (hiWRepr `addNat` loWRepr) ((hi `shiftL` loWidth) .|. lo)
+  where loWidth = fromIntegral (natValue loWRepr)
+
+-- | Infix 'bvConcat'.
+(<:>) :: BitVector v -> BitVector w -> BitVector (v+w)
+(<:>) = bvConcat
+
+bvConcatSome :: Some BitVector -> Some BitVector -> Some BitVector
+bvConcatSome (Some bv1) (Some bv2) = Some (bv2 <:> bv1)
+
+-- | Concatenate a list of 'BitVector's into a 'BitVector' of arbitrary width. The ordering is little endian:
+--
+-- >>> bvConcatMany [0xAA :: BitVector 8, 0xBB] :: BitVector 16
+-- 0xbbaa
+-- >>> bvConcatMany [0xAA :: BitVector 8, 0xBB, 0xCC] :: BitVector 16
+-- 0xbbaa
+--
+-- If the sum of the widths of the input 'BitVector's exceeds the output width, we
+-- ignore the tail end of the list.
+bvConcatMany :: KnownNat w' => [BitVector w] -> BitVector w'
+bvConcatMany = bvConcatMany' knownNat
+
+-- | 'bvConcatMany' with an explicit 'NatRepr'.
+bvConcatMany' :: NatRepr w' -> [BitVector w] -> BitVector w'
+bvConcatMany' wRepr bvs =
+  viewSome (bvZext' wRepr) $ foldl bvConcatSome (Some bv0) (Some <$> bvs)
+
+infixl 6 <:>
+
+-- | Slice out a smaller bit vector from a larger one. The lowest significant bit is
+-- given explicitly as an argument of type 'Int', and the length of the slice is
+-- inferred from a type-level context.
+--
+-- >>> bvExtract 12 (0xAABCDEF0 :: BitVector 32) :: BitVector 8
+-- 0xcd
+--
+-- Note that 'bvExtract' does not do any bounds checking whatsoever; if you try and
+-- extract bits that aren't present in the input, you will get 0's.
+bvExtract :: forall w w' . (KnownNat w')
+          => Int
+          -> BitVector w
+          -> BitVector w'
+bvExtract pos bv = bitVector xShf
+  where (BV _ xShf) = bvShift bv (- pos)
+
+-- | Unconstrained variant of 'bvExtract' with an explicit 'NatRepr' argument.
+bvExtract' :: NatRepr w'
+                  -> Int
+                  -> BitVector w
+                  -> BitVector w'
+bvExtract' repr pos bv = BV repr (truncBits width xShf)
+  where (BV _ xShf) = bvShift bv (- pos)
+        width = natValue repr
+
+-- | Zero-extend a vector to one of greater length. If given an input of greater
+-- length than the output type, this performs a truncation.
+bvZext :: forall w w' . KnownNat w'
+       => BitVector w
+       -> BitVector w'
+bvZext (BV _ x) = bitVector x
+
+-- | Unconstrained variant of 'bvZext' with an explicit 'NatRepr' argument.
+bvZext' :: NatRepr w'
+               -> BitVector w
+               -> BitVector w'
+bvZext' repr (BV _ x) = BV repr (truncBits width x)
+  where width = natValue repr
+
+-- | Sign-extend a vector to one of greater length. If given an input of greater
+-- length than the output type, this performs a truncation.
+bvSext :: forall w w' . KnownNat w'
+       => BitVector w
+       -> BitVector w'
+bvSext bv = bitVector (bvIntegerS bv)
+
+-- | Unconstrained variant of 'bvSext' with an explicit 'NatRepr' argument.
+bvSext' :: NatRepr w'
+               -> BitVector w
+               -> BitVector w'
+bvSext' repr bv = BV repr (truncBits width (bvIntegerS bv))
+  where width = natValue repr
+
+----------------------------------------
+-- Byte decomposition
+
+-- | Given a 'BitVector' of arbitrary length, decompose it into a list of bytes. Uses
+-- an unsigned interpretation of the input vector, so if you ask for more bytes that
+-- the 'BitVector' contains, you get zeros. The result is little-endian, so the first
+-- element of the list will be the least significant byte of the input vector.
+bvGetBytesU :: Int -> BitVector w -> [BitVector 8]
+bvGetBytesU n _ | n <= 0 = []
+bvGetBytesU n bv = bvExtract 0 bv : bvGetBytesU (n-1) (bvShiftRL bv 8)
+
+----------------------------------------
+-- Bits
+
+-- | Mask for a specified number of lower bits.
+lowMask :: (Integral a, Bits b) => a -> b
+lowMask numBits = complement (complement zeroBits `shiftL` fromIntegral numBits)
+
+-- | Truncate to a specified number of lower bits.
+truncBits :: (Integral a, Bits b) => a -> b -> b
+truncBits width b = b .&. lowMask width
+
+----------------------------------------
+-- Class instances
+$(return [])
+
+instance Show (BitVector w) where
+  show (BV _ x) = "0x" ++ showHex x ""
+
+instance KnownNat w => Read (BitVector w) where
+  readsPrec s =
+    (fmap . fmap) (\(a,s') -> (bitVector a, s')) (readsPrec s :: ReadS Integer)
+
+instance ShowF BitVector
+
+instance Eq (BitVector w) where
+  (BV _ x) == (BV _ y) = x == y
+
+instance EqF BitVector where
+  (BV _ x) `eqF` (BV _ y) = x == y
+
+instance Ord (BitVector w) where
+  (BV _ x) `compare` (BV _ y) = x `compare` y
+
+instance OrdF BitVector where
+  (BV xRepr x) `compareF` (BV yRepr y) =
+    case xRepr `compareF` yRepr of
+      EQF -> fromOrdering (x `compare` y)
+      cmp -> cmp
+
+instance TestEquality BitVector where
+  testEquality (BV wRepr x) (BV wRepr' y) =
+    if natValue wRepr == natValue wRepr' && x == y
+    then Just (unsafeCoerce (Refl :: a :~: a))
+    else Nothing
+
+instance KnownNat w => Bits (BitVector w) where
+  (.&.)        = bvAnd
+  (.|.)        = bvOr
+  xor          = bvXor
+  complement   = bvComplement
+  shift        = bvShift
+  rotate       = bvRotate
+  bitSize      = bvWidth
+  bitSizeMaybe = Just . bvWidth
+  isSigned     = const False
+  testBit      = bvTestBit
+  bit          = bitVector . (bit :: Int -> Integer)
+  popCount     = bvPopCount
+
+instance KnownNat w => FiniteBits (BitVector w) where
+  finiteBitSize = bvWidth
+
+instance KnownNat w => Num (BitVector w) where
+  (+)         = bvAdd
+  (*)         = bvMul
+  abs         = bvAbs
+  signum      = bvSignum
+  fromInteger = bitVector
+  negate      = bvNegate
+
+instance KnownNat w => Enum (BitVector w) where
+  toEnum   = bitVector
+  fromEnum = fromIntegral . bvIntegerU
+
+instance KnownNat w => Ix (BitVector w) where
+  range (lo, hi) = bitVector <$> [bvIntegerU lo .. bvIntegerU hi]
+  index (lo, hi) bv = index (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv)
+  inRange (lo, hi) bv = inRange (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv)
+
+instance KnownNat w => Bounded (BitVector w) where
+  minBound = bitVector (0 :: Integer)
+  maxBound = bitVector ((-1) :: Integer)
+
+instance KnownNat w => Arbitrary (BitVector w) where
+  arbitrary = choose (minBound, maxBound)
+
+instance KnownNat w => Random (BitVector w) where
+  randomR (bvLo, bvHi) gen =
+    let (x, gen') = randomR (bvIntegerU bvLo, bvIntegerU bvHi) gen
+    in (bitVector x, gen')
+  random gen =
+    let (x :: Integer, gen') = random gen
+    in (bitVector x, gen')
+
+prettyHex :: (Integral a, PrintfArg a, Show a) => a -> Integer -> String
+prettyHex width val = printf format val width
+  where numDigits = (width+3) `quot` 4
+        format = "0x%." ++ show numDigits ++ "x<%d>"
+
+instance Pretty (BitVector w) where
+  -- | Pretty print a bit vector (shows its width)
+  pPrint (BV wRepr x) = text $ prettyHex (natValue wRepr) x
diff --git a/stack.yaml b/stack.yaml
deleted file mode 100644
--- a/stack.yaml
+++ /dev/null
@@ -1,12 +0,0 @@
-resolver: lts-12.5
-
-packages:
-- .
-- submodules/parameterized-utils
-
-extra-deps:
-- containers-0.5.11.0
-- lens-4.16
-- prettyclass-1.0.0.0
-- random-1.1
-- QuickCheck-2.11.3
diff --git a/submodules/parameterized-utils/.travis.yml b/submodules/parameterized-utils/.travis.yml
new file mode 100644
--- /dev/null
+++ b/submodules/parameterized-utils/.travis.yml
@@ -0,0 +1,103 @@
+# This Travis job script has been generated by a script via
+#
+#   runghc make_travis_yml_2.hs 'parameterized-utils.cabal'
+#
+# For more information, see https://github.com/haskell-CI/haskell-ci
+#
+language: c
+sudo: false
+
+git:
+  submodules: false  # whether to recursively clone submodules
+
+cache:
+  directories:
+    - $HOME/.cabal/packages
+    - $HOME/.cabal/store
+
+before_cache:
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log
+  # remove files that are regenerated by 'cabal update'
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.*
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/*.json
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.cache
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/01-index.tar.idx
+
+  - rm -rfv $HOME/.cabal/packages/head.hackage
+
+matrix:
+  include:
+    - compiler: "ghc-8.4.3"
+    # env: TEST=--disable-tests BENCH=--disable-benchmarks
+      addons: {apt: {packages: [ghc-ppa-tools,cabal-install-2.2,ghc-8.4.3], sources: [hvr-ghc]}}
+
+before_install:
+  - HC=${CC}
+  - HCPKG=${HC/ghc/ghc-pkg}
+  - unset CC
+  - ROOTDIR=$(pwd)
+  - mkdir -p $HOME/.local/bin
+  - "PATH=/opt/ghc/bin:/opt/ghc-ppa-tools/bin:$HOME/local/bin:$PATH"
+  - HCNUMVER=$(( $(${HC} --numeric-version|sed -E 's/([0-9]+)\.([0-9]+)\.([0-9]+).*/\1 * 10000 + \2 * 100 + \3/') ))
+  - echo $HCNUMVER
+
+install:
+  - cabal --version
+  - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"
+  - BENCH=${BENCH---enable-benchmarks}
+  - TEST=${TEST---enable-tests}
+  - HADDOCK=${HADDOCK-true}
+  - UNCONSTRAINED=${UNCONSTRAINED-true}
+  - NOINSTALLEDCONSTRAINTS=${NOINSTALLEDCONSTRAINTS-false}
+  - GHCHEAD=${GHCHEAD-false}
+  - travis_retry cabal update -v
+  - "sed -i.bak 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config"
+  - rm -fv cabal.project cabal.project.local
+  - grep -Ev -- '^\s*--' ${HOME}/.cabal/config | grep -Ev '^\s*$'
+  - "printf 'packages: \".\"\\n' > cabal.project"
+  - touch cabal.project.local
+  - "if ! $NOINSTALLEDCONSTRAINTS; then for pkg in $($HCPKG list --simple-output); do echo $pkg  | grep -vw -- parameterized-utils | sed 's/^/constraints: /' | sed 's/-[^-]*$/ installed/' >> cabal.project.local; done; fi"
+  - cat cabal.project || true
+  - cat cabal.project.local || true
+  - if [ -f "./configure.ac" ]; then
+      (cd "." && autoreconf -i);
+    fi
+  - rm -f cabal.project.freeze
+  - cabal new-build -w ${HC} ${TEST} ${BENCH} --project-file="cabal.project" --dep -j2 all
+  - cabal new-build -w ${HC} --disable-tests --disable-benchmarks --project-file="cabal.project" --dep -j2 all
+  - rm -rf .ghc.environment.* "."/dist
+  - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX)
+
+# Here starts the actual work to be performed for the package under test;
+# any command which exits with a non-zero exit code causes the build to fail.
+script:
+  # test that source-distributions can be generated
+  - (cd "." && cabal sdist)
+  - mv "."/dist/parameterized-utils-*.tar.gz ${DISTDIR}/
+  - cd ${DISTDIR} || false
+  - find . -maxdepth 1 -name '*.tar.gz' -exec tar -xvf '{}' \;
+  - "printf 'packages: parameterized-utils-*/*.cabal\\n' > cabal.project"
+  - touch cabal.project.local
+  - "if ! $NOINSTALLEDCONSTRAINTS; then for pkg in $($HCPKG list --simple-output); do echo $pkg  | grep -vw -- parameterized-utils | sed 's/^/constraints: /' | sed 's/-[^-]*$/ installed/' >> cabal.project.local; done; fi"
+  - cat cabal.project || true
+  - cat cabal.project.local || true
+  # this builds all libraries and executables (without tests/benchmarks)
+  - cabal new-build -w ${HC} --disable-tests --disable-benchmarks all
+
+  # build & run tests, build benchmarks
+  - cabal new-build -w ${HC} ${TEST} ${BENCH} all
+  - if [ "x$TEST" = "x--enable-tests" ]; then cabal new-test -w ${HC} ${TEST} ${BENCH} all; fi
+
+  # cabal check
+  - (cd parameterized-utils-* && cabal check)
+
+  # haddock
+  - rm -rf ./dist-newstyle
+  - if $HADDOCK; then cabal new-haddock -w ${HC} ${TEST} ${BENCH} all; else echo "Skipping haddock generation";fi
+
+  # Build without installed constraints for packages in global-db
+  - if $UNCONSTRAINED; then rm -f cabal.project.local; echo cabal new-build -w ${HC} --disable-tests --disable-benchmarks all; else echo "Not building without installed constraints"; fi
+
+# REGENDATA ["parameterized-utils.cabal"]
+# EOF
diff --git a/submodules/parameterized-utils/parameterized-utils.cabal b/submodules/parameterized-utils/parameterized-utils.cabal
--- a/submodules/parameterized-utils/parameterized-utils.cabal
+++ b/submodules/parameterized-utils/parameterized-utils.cabal
@@ -1,5 +1,5 @@
 Name:          parameterized-utils
-Version:       1.0.0
+Version:       1.0.8
 Author:        Galois Inc.
 Maintainer:    jhendrix@galois.com
 Build-type:    Simple
@@ -14,6 +14,7 @@
   intended for things like expression libraries where one wishes
   to leverage the Haskell type-checker to improve type-safety by encoding
   the object language type system into data kinds.
+tested-with: GHC==8.4.3, GHC==8.6.1
 
 -- Many (but not all, sadly) uses of unsafe operations are
 -- controlled by this compile flag.  When this flag is set
@@ -30,8 +31,9 @@
 
 library
   build-depends:
-    base >= 4.7 && < 4.12,
+    base >= 4.7 && < 4.13,
     th-abstraction >=0.1 && <0.3,
+    constraints >= 0.10 && < 0.11,
     containers,
     deepseq,
     ghc-prim,
@@ -48,11 +50,14 @@
   exposed-modules:
     Data.Parameterized
     Data.Parameterized.Classes
+    Data.Parameterized.ClassesC
+    Data.Parameterized.Compose
     Data.Parameterized.Context
     Data.Parameterized.Context.Safe
     Data.Parameterized.Context.Unsafe
     Data.Parameterized.Ctx
     Data.Parameterized.Ctx.Proofs
+    Data.Parameterized.DecidableEq
     Data.Parameterized.HashTable
     Data.Parameterized.List
     Data.Parameterized.Map
@@ -60,13 +65,16 @@
     Data.Parameterized.Nonce
     Data.Parameterized.Nonce.Transformers
     Data.Parameterized.Nonce.Unsafe
+    Data.Parameterized.Pair
+    Data.Parameterized.Peano
     Data.Parameterized.Some
     Data.Parameterized.SymbolRepr
-    Data.Parameterized.Pair
     Data.Parameterized.TH.GADT
     Data.Parameterized.TraversableF
     Data.Parameterized.TraversableFC
     Data.Parameterized.Utils.BinTree
+    Data.Parameterized.Utils.Endian
+    Data.Parameterized.Vector
 
   ghc-options: -Wall
 
@@ -84,6 +92,7 @@
   other-modules:
     Test.Context
     Test.NatRepr
+    Test.Vector
 
   build-depends:
     base,
@@ -94,7 +103,7 @@
     mtl,
     parameterized-utils,
     tasty,
-    tasty-ant-xml,
+    tasty-ant-xml >= 1.1.0,
     tasty-hunit,
     tasty-quickcheck >= 0.8.1,
     QuickCheck >= 2.7
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Classes.hs b/submodules/parameterized-utils/src/Data/Parameterized/Classes.hs
--- a/submodules/parameterized-utils/src/Data/Parameterized/Classes.hs
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Classes.hs
@@ -37,6 +37,7 @@
   , orderingF_refl
   , toOrdering
   , fromOrdering
+  , ordFCompose
     -- * Typeclass generalizations
   , ShowF(..)
   , showsF
@@ -55,11 +56,14 @@
   ) where
 
 import Data.Functor.Const
+import Data.Functor.Compose (Compose(..))
 import Data.Hashable
 import Data.Maybe (isJust)
 import Data.Proxy
 import Data.Type.Equality as Equality
 
+import Data.Parameterized.Compose ()
+
 -- We define these type alias here to avoid importing Control.Lens
 -- modules, as this apparently causes problems with the safe Hasekll
 -- checking.
@@ -193,6 +197,23 @@
             -> (a ~ b => OrderingF c d)
             -> OrderingF c d
 lexCompareF x y = joinOrderingF (compareF x y)
+
+-- | If the \"outer\" functor has an 'OrdF' instance, then one can be generated
+-- for the \"inner\" functor. The type-level evidence of equality is deduced
+-- via generativity of @g@, e.g. the inference @g x ~ g y@ implies @x ~ y@.
+ordFCompose :: forall (f :: k -> *) (g :: l -> k) x y.
+                (forall w z. f w -> f z -> OrderingF w z)
+            -> Compose f g x
+            -> Compose f g y
+            -> OrderingF x y
+ordFCompose ordF_ (Compose x) (Compose y) =
+  case ordF_ x y of
+    LTF -> LTF
+    GTF -> GTF
+    EQF -> EQF
+
+instance OrdF f => OrdF (Compose f g) where
+  compareF x y = ordFCompose compareF x y
 
 ------------------------------------------------------------------------
 -- ShowF
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/ClassesC.hs b/submodules/parameterized-utils/src/Data/Parameterized/ClassesC.hs
new file mode 100644
--- /dev/null
+++ b/submodules/parameterized-utils/src/Data/Parameterized/ClassesC.hs
@@ -0,0 +1,52 @@
+{-|
+Copyright        : (c) Galois, Inc 2014-2015
+Maintainer       : Langston Barrett <langston@galois.com>
+
+This module declares classes for working with types with the kind
+@(k -> *) -> *@ for any kind @k@.
+
+These classes generally require type-level evidence for operations
+on their subterms, but don't actually provide it themselves (because
+their types are not themselves parameterized, unlike those in
+"Data.Parameterized.TraverableFC").
+
+Note that there is still some ambiguity around naming conventions, see
+<https://github.com/GaloisInc/parameterized-utils/issues/23 issue 23>.
+-}
+
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Parameterized.ClassesC
+  ( TestEqualityC(..)
+  , OrdC(..)
+  ) where
+
+import Data.Type.Equality ((:~:)(..))
+import Data.Maybe (isJust)
+import Data.Parameterized.Classes (OrderingF, toOrdering)
+import Data.Parameterized.Some (Some(..))
+
+class TestEqualityC (t :: (k -> *) -> *) where
+  testEqualityC :: (forall x y. f x -> f y -> Maybe (x :~: y))
+                -> t f
+                -> t f
+                -> Bool
+
+class TestEqualityC t => OrdC (t :: (k -> *) -> *) where
+  compareC :: (forall x y. f x -> g y -> OrderingF x y)
+           -> t f
+           -> t g
+           -> Ordering
+
+-- | This instance demonstrates where the above class is useful: namely, in
+-- types with existential quantification.
+instance TestEqualityC Some where
+  testEqualityC subterms (Some someone) (Some something) =
+    isJust (subterms someone something)
+
+instance OrdC Some where
+  compareC subterms (Some someone) (Some something) =
+    toOrdering (subterms someone something)
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Compose.hs b/submodules/parameterized-utils/src/Data/Parameterized/Compose.hs
new file mode 100644
--- /dev/null
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Compose.hs
@@ -0,0 +1,45 @@
+{-|
+Copyright        : (c) Galois, Inc 2014-2018
+Maintainer       : Langston Barrett <langston@galois.com
+
+Utilities for working with "Data.Functor.Compose".
+
+NB: This module contains an orphan instance. It will be included in GHC 8.10,
+see https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
+-}
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Safe #-}
+
+module Data.Parameterized.Compose
+  ( testEqualityComposeBare
+  ) where
+
+import Data.Functor.Compose
+import Data.Type.Equality
+
+-- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.
+--
+-- See https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
+testEqualityComposeBare :: forall (f :: k -> *) (g :: l -> k) x y.
+                           (forall w z. f w -> f z -> Maybe (w :~: z))
+                        -> Compose f g x
+                        -> Compose f g y
+                        -> Maybe (x :~: y)
+testEqualityComposeBare testEquality_ (Compose x) (Compose y) =
+  case (testEquality_ x y :: Maybe (g x :~: g y)) of
+    Just Refl -> Just (Refl :: x :~: y)
+    Nothing   -> Nothing
+
+testEqualityCompose :: forall (f :: k -> *) (g :: l -> k) x y. (TestEquality f)
+                    => Compose f g x
+                    -> Compose f g y
+                    -> Maybe (x :~: y)
+testEqualityCompose = testEqualityComposeBare testEquality
+
+instance (TestEquality f) => TestEquality (Compose f g) where
+  testEquality = testEqualityCompose
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Context.hs b/submodules/parameterized-utils/src/Data/Parameterized/Context.hs
--- a/submodules/parameterized-utils/src/Data/Parameterized/Context.hs
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Context.hs
@@ -33,50 +33,63 @@
 module Data.Parameterized.Context
  (
 #ifdef UNSAFE_OPS
-   module Data.Parameterized.Context.Unsafe
+    module Data.Parameterized.Context.Unsafe
 #else
-   module Data.Parameterized.Context.Safe
+    module Data.Parameterized.Context.Safe
 #endif
- , singleton
- , toVector
- , pattern (:>)
- , pattern Empty
- , decompose
- , Data.Parameterized.Context.null
- , Data.Parameterized.Context.init
- , Data.Parameterized.Context.last
- , Data.Parameterized.Context.view
- , forIndexM
- , generateSome
- , generateSomeM
- , fromList
-   -- * Context extension and embedding utilities
- , CtxEmbedding(..)
- , ExtendContext(..)
- , ExtendContext'(..)
- , ApplyEmbedding(..)
- , ApplyEmbedding'(..)
- , identityEmbedding
- , extendEmbeddingRightDiff
- , extendEmbeddingRight
- , extendEmbeddingBoth
- , ctxeSize
- , ctxeAssignment
+  , singleton
+  , toVector
+  , pattern (:>)
+  , pattern Empty
+  , decompose
+  , Data.Parameterized.Context.null
+  , Data.Parameterized.Context.init
+  , Data.Parameterized.Context.last
+  , Data.Parameterized.Context.view
+  , Data.Parameterized.Context.take
+  , forIndexM
+  , generateSome
+  , generateSomeM
+  , fromList
+  , traverseAndCollect
 
-   -- * Static indexing and lenses for assignments
- , Idx
- , field
- , natIndex
- , natIndexProxy
-   -- * Currying and uncurrying for assignments
- , CurryAssignment
- , CurryAssignmentClass(..)
- ) where
+    -- * Context extension and embedding utilities
+  , CtxEmbedding(..)
+  , ExtendContext(..)
+  , ExtendContext'(..)
+  , ApplyEmbedding(..)
+  , ApplyEmbedding'(..)
+  , identityEmbedding
+  , extendEmbeddingRightDiff
+  , extendEmbeddingRight
+  , extendEmbeddingBoth
+  , appendEmbedding
+  , ctxeSize
+  , ctxeAssignment
 
+    -- * Static indexing and lenses for assignments
+  , Idx
+  , field
+  , natIndex
+  , natIndexProxy
+    -- * Currying and uncurrying for assignments
+  , CurryAssignment
+  , CurryAssignmentClass(..)
+    -- * Size and Index values
+  , size1, size2, size3, size4, size5, size6
+  , i1of2, i2of2
+  , i1of3, i2of3, i3of3
+  , i1of4, i2of4, i3of4, i4of4
+  , i1of5, i2of5, i3of5, i4of5, i5of5
+  , i1of6, i2of6, i3of6, i4of6, i5of6, i6of6
+  ) where
+
+import           Control.Applicative (liftA2)
 import           Control.Lens hiding (Index, (:>), Empty)
 import qualified Data.Vector as V
 import qualified Data.Vector.Mutable as MV
 import           GHC.TypeLits (Nat, type (-))
+import           Data.Monoid ((<>))
 
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
@@ -152,7 +165,7 @@
 #endif
 
 --------------------------------------------------------------------------------
--- | Views
+-- Views
 
 -- | Return true if assignment is empty.
 null :: Assignment f ctx -> Bool
@@ -181,10 +194,15 @@
 view :: forall f ctx . Assignment f ctx -> AssignView f ctx
 view = viewAssign
 
+take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
+take sz sz' asgn =
+  let diff = appendDiff sz' in
+  generate sz (\i -> asgn ! extendIndex' diff i)
+
 --------------------------------------------------------------------------------
--- | Context embedding.
+-- Context embedding.
 
--- This datastructure contains a proof that the first context is
+-- | This datastructure contains a proof that the first context is
 -- embeddable in the second.  This is useful if we want to add extend
 -- an existing term under a larger context.
 
@@ -248,6 +266,11 @@
 extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
 extendEmbeddingRight = extendEmbeddingRightDiff knownDiff
 
+appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
+appendEmbedding sz sz' = CtxEmbedding (addSize sz sz') (generate sz (extendIndex' diff))
+  where
+  diff = appendDiff sz'
+
 extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
 extendEmbeddingBoth ctxe = updated & ctxeAssignment %~ flip extend (nextIndex (ctxe ^. ctxeSize))
   where
@@ -339,3 +362,102 @@
   where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)
         go prev [] = Some prev
         go prev (Some g:next) = (go $! prev `extend` g) next
+
+
+newtype Collector m w a = Collector { runCollector :: m w }
+instance Functor (Collector m w) where
+  fmap _ (Collector x) = Collector x
+instance (Applicative m, Monoid w) => Applicative (Collector m w) where
+  pure _ = Collector (pure mempty)
+  Collector x <*> Collector y = Collector (liftA2 (<>) x y)
+
+-- | Visit each of the elements in an @Assignment@ in order
+--   from left to right and collect the results using the provided @Monoid@.
+traverseAndCollect ::
+  (Monoid w, Applicative m) =>
+  (forall tp. Index ctx tp -> f tp -> m w) ->
+  Assignment f ctx ->
+  m w
+traverseAndCollect f =
+  runCollector . traverseWithIndex (\i x -> Collector (f i x))
+
+--------------------------------------------------------------------------------
+-- Size and Index values
+
+size1 :: Size (EmptyCtx ::> a)
+size1 = incSize zeroSize
+
+size2 :: Size (EmptyCtx ::> a ::> b)
+size2 = incSize size1
+
+size3 :: Size (EmptyCtx ::> a ::> b ::> c)
+size3 = incSize size2
+
+size4 :: Size (EmptyCtx ::> a ::> b ::> c ::> d)
+size4 = incSize size3
+
+size5 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e)
+size5 = incSize size4
+
+size6 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f)
+size6 = incSize size5
+
+i1of2 :: Index (EmptyCtx ::> a ::> b) a
+i1of2 = skipIndex baseIndex
+
+i2of2 :: Index (EmptyCtx ::> a ::> b) b
+i2of2 = nextIndex size1
+
+i1of3 :: Index (EmptyCtx ::> a ::> b ::> c) a
+i1of3 = skipIndex i1of2
+
+i2of3 :: Index (EmptyCtx ::> a ::> b ::> c) b
+i2of3 = skipIndex i2of2
+
+i3of3 :: Index (EmptyCtx ::> a ::> b ::> c) c
+i3of3 = nextIndex size2
+
+i1of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) a
+i1of4 = skipIndex i1of3
+
+i2of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) b
+i2of4 = skipIndex i2of3
+
+i3of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) c
+i3of4 = skipIndex i3of3
+
+i4of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) d
+i4of4 = nextIndex size3
+
+i1of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) a
+i1of5 = skipIndex i1of4
+
+i2of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) b
+i2of5 = skipIndex i2of4
+
+i3of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) c
+i3of5 = skipIndex i3of4
+
+i4of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) d
+i4of5 = skipIndex i4of4
+
+i5of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) e
+i5of5 = nextIndex size4
+
+i1of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) a
+i1of6 = skipIndex i1of5
+
+i2of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) b
+i2of6 = skipIndex i2of5
+
+i3of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) c
+i3of6 = skipIndex i3of5
+
+i4of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) d
+i4of6 = skipIndex i4of5
+
+i5of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) e
+i5of6 = skipIndex i5of5
+
+i6of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) f
+i6of6 = nextIndex size5
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Context/Safe.hs b/submodules/parameterized-utils/src/Data/Parameterized/Context/Safe.hs
--- a/submodules/parameterized-utils/src/Data/Parameterized/Context/Safe.hs
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Context/Safe.hs
@@ -60,6 +60,7 @@
   , Diff
   , noDiff
   , extendRight
+  , appendDiff
   , DiffView(..)
   , viewDiff
   , KnownDiff(..)
@@ -120,7 +121,7 @@
 ------------------------------------------------------------------------
 -- Size
 
--- | A  indexed singleton type representing the size of a context.
+-- | An indexed singleton type representing the size of a context.
 data Size (ctx :: Ctx k) where
   SizeZero :: Size 'EmptyCtx
   SizeSucc :: !(Size ctx) -> Size (ctx '::> tp)
@@ -185,6 +186,10 @@
 -- | Extend the difference to a sub-context of the right side.
 extendRight :: Diff l r -> Diff l (r '::> tp)
 extendRight diff = DiffThere diff
+
+appendDiff :: Size r -> Diff l (l <+> r)
+appendDiff SizeZero = DiffHere
+appendDiff (SizeSucc sz) = DiffThere (appendDiff sz)
 
 composeDiff :: Diff a b -> Diff b c -> Diff a c
 composeDiff x DiffHere = x
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Context/Unsafe.hs b/submodules/parameterized-utils/src/Data/Parameterized/Context/Unsafe.hs
--- a/submodules/parameterized-utils/src/Data/Parameterized/Context/Unsafe.hs
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Context/Unsafe.hs
@@ -32,6 +32,7 @@
   , Diff
   , noDiff
   , extendRight
+  , appendDiff
   , DiffView(..)
   , viewDiff
   , KnownDiff(..)
@@ -97,10 +98,14 @@
 -- Size
 
 -- | Represents the size of a context.
-newtype Size (ctx :: Ctx k) = Size { sizeInt :: Int }
+newtype Size (ctx :: Ctx k) = Size Int
 
 type role Size nominal
 
+-- | Convert a context size to an 'Int'.
+sizeInt :: Size ctx -> Int
+sizeInt (Size n) = n
+
 -- | The size of an empty context.
 zeroSize :: Size 'EmptyCtx
 zeroSize = Size 0
@@ -143,6 +148,8 @@
 newtype Diff (l :: Ctx k) (r :: Ctx k)
       = Diff { _contextExtSize :: Int }
 
+type role Diff nominal nominal
+
 -- | The identity difference.
 noDiff :: Diff l l
 noDiff = Diff 0
@@ -150,6 +157,9 @@
 -- | Extend the difference to a sub-context of the right side.
 extendRight :: Diff l r -> Diff l (r '::> tp)
 extendRight (Diff i) = Diff (i+1)
+
+appendDiff :: Size r -> Diff l (l <+> r)
+appendDiff (Size r) = Diff r
 
 instance Cat.Category Diff where
   id = Diff 0
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/DecidableEq.hs b/submodules/parameterized-utils/src/Data/Parameterized/DecidableEq.hs
new file mode 100644
--- /dev/null
+++ b/submodules/parameterized-utils/src/Data/Parameterized/DecidableEq.hs
@@ -0,0 +1,37 @@
+{-|
+Copyright        : (c) Galois, Inc 2014-2018
+Maintainer       : Langston Barrett <langston@galois.com>
+
+This defines a class @DecidableEq@, which represents decidable equality on a
+type family.
+
+This is different from GHC's @TestEquality@ in that it provides evidence
+of non-equality. In fact, it is a superclass of @TestEquality@.
+-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Safe #-}
+module Data.Parameterized.DecidableEq
+  ( DecidableEq(..)
+  ) where
+
+import Data.Void (Void)
+import Data.Type.Equality ((:~:))
+
+-- | Decidable equality.
+class DecidableEq f where
+  decEq :: f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)
+
+-- TODO: instances for sums, products of types with decidable equality
+
+-- import Data.Type.Equality ((:~:), TestEquality(..))
+-- instance (DecidableEq f) => TestEquality f where
+--   testEquality a b =
+--     case decEq a b of
+--       Left  prf -> Just prf
+--       Right _   -> Nothing
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Map.hs b/submodules/parameterized-utils/src/Data/Parameterized/Map.hs
--- a/submodules/parameterized-utils/src/Data/Parameterized/Map.hs
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Map.hs
@@ -45,13 +45,21 @@
   , fromKeys
   , fromKeysM
    -- * Filter
+  , filter
+  , filterWithKey
   , filterGt
   , filterLt
     -- * Folds
+  , foldlWithKey
+  , foldlWithKey'
   , foldrWithKey
+  , foldrWithKey'
+  , foldMapWithKey
     -- * Traversal
   , map
+  , mapWithKey
   , mapMaybe
+  , mapMaybeWithKey
   , traverseWithKey
   , traverseWithKey_
     -- * Complex interface.
@@ -65,18 +73,18 @@
   , Pair(..)
   ) where
 
-import Control.Applicative hiding (empty)
-import Control.Lens (Traversal', Lens')
-import Control.Monad.Identity
-import Data.List (intercalate, foldl')
-import Data.Maybe ()
-import Data.Kind(Type)
+import           Control.Applicative hiding (empty)
+import           Control.Lens (Traversal', Lens')
+import           Control.Monad.Identity
+import           Data.Kind (Type)
+import           Data.List (intercalate, foldl')
+import           Data.Monoid
 
-import Data.Parameterized.Classes
-import Data.Parameterized.Some
-import Data.Parameterized.Pair ( Pair(..) )
-import Data.Parameterized.TraversableF
-import Data.Parameterized.Utils.BinTree
+import           Data.Parameterized.Classes
+import           Data.Parameterized.Some
+import           Data.Parameterized.Pair ( Pair(..) )
+import           Data.Parameterized.TraversableF
+import           Data.Parameterized.Utils.BinTree
   ( MaybeS(..)
   , fromMaybeS
   , Updated(..)
@@ -91,9 +99,9 @@
 import qualified Data.Parameterized.Utils.BinTree as Bin
 
 #if MIN_VERSION_base(4,8,0)
-import Prelude hiding (lookup, map, traverse, null)
+import           Prelude hiding (filter, lookup, map, traverse, null)
 #else
-import Prelude hiding (lookup, map, null)
+import           Prelude hiding (filter, lookup, map, null)
 #endif
 
 ------------------------------------------------------------------------
@@ -106,7 +114,7 @@
 ------------------------------------------------------------------------
 -- MapF
 
--- | A map from parameterized keys to values with the same paramter type.
+-- | A map from parameterized keys to values with the same parameter type.
 data MapF (k :: v -> Type) (a :: v -> Type) where
   Bin :: {-# UNPACK #-}
          !Size -- Number of elements in tree.
@@ -165,18 +173,30 @@
  #-}
 #endif
 
+
+-- | Apply function to all elements in map.
+mapWithKey
+  :: (forall tp . ktp tp -> f tp -> g tp)
+  -> MapF ktp f
+  -> MapF ktp g
+mapWithKey _ Tip = Tip
+mapWithKey f (Bin sx kx x l r) = Bin sx kx (f kx x) (mapWithKey f l) (mapWithKey f r)
+
 -- | Modify elements in a map
 map :: (forall tp . f tp -> g tp) -> MapF ktp f -> MapF ktp g
-map _ Tip = Tip
-map f (Bin sx kx x l r) = Bin sx kx (f x) (map f l) (map f r)
+map f = mapWithKey (\_ x -> f x)
 
--- | Run partial map over elements.
+-- | Map keys and elements and collect `Just` results.
+mapMaybeWithKey :: (forall tp . k tp -> f tp -> Maybe (g tp)) -> MapF k f -> MapF k g
+mapMaybeWithKey _ Tip = Tip
+mapMaybeWithKey f (Bin _ k x l r) =
+  case f k x of
+    Just y -> Bin.link (Pair k y) (mapMaybeWithKey f l) (mapMaybeWithKey f r)
+    Nothing -> Bin.merge (mapMaybeWithKey f l) (mapMaybeWithKey f r)
+
+-- | Map elements and collect `Just` results.
 mapMaybe :: (forall tp . f tp -> Maybe (g tp)) -> MapF ktp f -> MapF ktp g
-mapMaybe _ Tip = Tip
-mapMaybe f (Bin _ k x l r) =
-  case f x of
-    Just y -> Bin.link (Pair k y) (mapMaybe f l) (mapMaybe f r)
-    Nothing -> Bin.merge (mapMaybe f l) (mapMaybe f r)
+mapMaybe f = mapMaybeWithKey (\_ x -> f x)
 
 -- | Traverse elements in a map
 traverse :: Applicative m => (forall tp . f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g)
@@ -270,13 +290,43 @@
 elems :: MapF k a -> [Some a]
 elems = foldrF (\e l -> Some e : l) []
 
--- | Perform a fold with the key also provided.
+-- | Perform a left fold with the key also provided.
+foldlWithKey :: (forall s . b -> k s -> a s -> b) -> b -> MapF k a -> b
+foldlWithKey _ z Tip = z
+foldlWithKey f z (Bin _ kx x l r) =
+  let lz = foldlWithKey f z l
+      kz = f lz kx x
+   in foldlWithKey f kz r
+
+-- | Perform a strict left fold with the key also provided.
+foldlWithKey' :: (forall s . b -> k s -> a s -> b) -> b -> MapF k a -> b
+foldlWithKey' _ z Tip = z
+foldlWithKey' f z (Bin _ kx x l r) =
+  let lz = foldlWithKey f z l
+      kz = seq lz $ f lz kx x
+   in seq kz $ foldlWithKey f kz r
+
+-- | Perform a right fold with the key also provided.
 foldrWithKey :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b
-foldrWithKey f z = go z
-  where
-    go z' Tip = z'
-    go z' (Bin _ kx x l r) = go (f kx x (go z' r)) l
+foldrWithKey _ z Tip = z
+foldrWithKey f z (Bin _ kx x l r) =
+  let rz = foldrWithKey f z r
+      kz = f kx x rz
+   in foldrWithKey f kz l
 
+-- | Perform a strict right fold with the key also provided.
+foldrWithKey' :: (forall s . k s -> a s -> b -> b) -> b -> MapF k a -> b
+foldrWithKey' _ z Tip = z
+foldrWithKey' f z (Bin _ kx x l r) =
+  let rz = foldrWithKey f z r
+      kz = seq rz $ f kx x rz
+   in seq kz $ foldrWithKey f kz l
+
+-- | Fold the keys and values using the given monoid.
+foldMapWithKey :: Monoid m => (forall s . k s -> a s -> m) -> MapF k a -> m
+foldMapWithKey _ Tip = mempty
+foldMapWithKey f (Bin _ kx x l r) = foldMapWithKey f l <> f kx x <> foldMapWithKey f r
+
 showMap :: (forall tp . ktp tp -> String)
         -> (forall tp . rtp tp -> String)
         -> MapF ktp rtp
@@ -286,6 +336,17 @@
 
 ------------------------------------------------------------------------
 -- filter
+
+-- | Return entries with values that satisfy predicate.
+filter :: (forall tp . f tp -> Bool) -> MapF k f -> MapF k f
+filter f = filterWithKey (\_ v -> f v)
+
+-- | Return key-value pairs that satisfy predicate.
+filterWithKey :: (forall tp . k tp -> f tp -> Bool) -> MapF k f -> MapF k f
+filterWithKey _ Tip = Tip
+filterWithKey f (Bin _ k x l r)
+  | f k x     = Bin.link (Pair k x) (filterWithKey f l) (filterWithKey f r)
+  | otherwise = Bin.merge (filterWithKey f l) (filterWithKey f r)
 
 compareKeyPair :: OrdF k => k tp -> Pair k a -> Ordering
 compareKeyPair k = \(Pair x _) -> toOrdering (compareF k x)
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/NatRepr.hs b/submodules/parameterized-utils/src/Data/Parameterized/NatRepr.hs
--- a/submodules/parameterized-utils/src/Data/Parameterized/NatRepr.hs
+++ b/submodules/parameterized-utils/src/Data/Parameterized/NatRepr.hs
@@ -1,5 +1,5 @@
 {-|
-Copyright        : (c) Galois, Inc 2014-2015
+Copyright        : (c) Galois, Inc 2014-2018
 Maintainer       : Joe Hendrix <jhendrix@galois.com>
 
 This defines a type 'NatRepr' for representing a type-level natural
@@ -8,14 +8,17 @@
 @n@.  This can be used to help use type-level variables on code
 with data dependendent types.
 
-The 'TestEquality' instance for 'NatRepr' is implemented using
-'unsafeCoerce', as is the `isZeroNat` function. This should be
-typesafe because we maintain the invariant that the integer value
+The @TestEquality@ and @DecidableEq@ instances for 'NatRepr'
+are implemented using 'unsafeCoerce', as is the `isZeroNat` function. This
+should be typesafe because we maintain the invariant that the integer value
 contained in a NatRepr value matches its static type.
 -}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
@@ -24,19 +27,25 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeApplications #-}
 #if MIN_VERSION_base(4,9,0)
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 #endif
+#if __GLASGOW_HASKELL__ >= 805
+{-# LANGUAGE NoStarIsType #-}
+#endif
 module Data.Parameterized.NatRepr
   ( NatRepr
   , natValue
+  , intValue
   , knownNat
   , withKnownNat
   , IsZeroNat(..)
   , isZeroNat
+  , isZeroOrGT1
   , NatComparison(..)
   , compareNat
   , decNat
@@ -49,11 +58,18 @@
   , withDivModNat
   , natMultiply
   , someNat
+  , mkNatRepr
   , maxNat
   , natRec
+  , natRecStrong
+  , natRecBounded
   , natForEach
+  , natFromZero
   , NatCases(..)
   , testNatCases
+    -- * Strict order
+  , lessThanIrreflexive
+  , lessThanAsymmetric
     -- * Bitvector utilities
   , widthVal
   , minUnsigned
@@ -66,6 +82,7 @@
   , signedClamp
     -- * LeqProof
   , LeqProof(..)
+  , decideLeq
   , testLeq
   , testStrictLeq
   , leqRefl
@@ -98,6 +115,7 @@
   , withSubMulDistribRight
   , mulCancelR
   , mul2Plus
+  , lemmaMul
     -- * Re-exports typelists basics
 --  , NatK
   , type (+)
@@ -107,20 +125,25 @@
   , Equality.TestEquality(..)
   , (Equality.:~:)(..)
   , Data.Parameterized.Some.Some
+    -- * Backdoor, no touchy
+  , activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing
   ) where
 
-import Data.Bits ((.&.))
+import Data.Bits ((.&.), bit)
 import Data.Hashable
 import Data.Proxy as Proxy
 import Data.Type.Equality as Equality
-import GHC.TypeLits as TypeLits
+import Data.Void as Void
+import Numeric.Natural
+import GHC.TypeNats as TypeNats
 import Unsafe.Coerce
 
 import Data.Parameterized.Classes
+import Data.Parameterized.DecidableEq
 import Data.Parameterized.Some
 
-maxInt :: Integer
-maxInt = toInteger (maxBound :: Int)
+maxInt :: Natural
+maxInt = fromIntegral (maxBound :: Int)
 
 ------------------------------------------------------------------------
 -- Nat
@@ -129,15 +152,27 @@
 --
 -- This can be used for performing dynamic checks on a type-level natural
 -- numbers.
-newtype NatRepr (n::Nat) = NatRepr { natValue :: Integer
-                                     -- ^ The underlying integer value of the number.
+newtype NatRepr (n::Nat) = NatRepr { natValue :: Natural
+                                     -- ^ The underlying natural value of the number.
                                    }
   deriving (Hashable)
 
+type role NatRepr nominal
+
+intValue :: NatRepr n -> Integer
+intValue n = toInteger (natValue n)
+{-# INLINE intValue #-}
+
+-- | If you are not 110% sure what the consequences of using this are and
+--   how to use it, don't.
+activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing :: ((Natural -> NatRepr n) -> a) -> a
+activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing k = k NatRepr
+{-# INLINE activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing #-}
+
 -- | Return the value of the nat representation.
 widthVal :: NatRepr n -> Int
-widthVal (NatRepr i) | i < maxInt = fromInteger i
-                     | otherwise = error "Width is too large."
+widthVal (NatRepr i) | i <= maxInt = fromIntegral i
+                     | otherwise   = error ("Width is too large: " ++ show i)
 
 instance Eq (NatRepr m) where
   _ == _ = True
@@ -147,20 +182,26 @@
     | m == n = Just (unsafeCoerce Refl)
     | otherwise = Nothing
 
+instance DecidableEq NatRepr where
+  decEq (NatRepr m) (NatRepr n)
+    | m == n    = Left $ unsafeCoerce Refl
+    | otherwise = Right $
+        \x -> seq x $ error "Impossible [DecidableEq on NatRepr]"
+
 -- | Result of comparing two numbers.
 data NatComparison m n where
   -- First number is less than second.
-  NatLT :: !(NatRepr y) -> NatComparison x (x+(y+1))
+  NatLT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison x (x+(y+1))
   NatEQ :: NatComparison x x
   -- First number is greater than second.
-  NatGT :: !(NatRepr y) -> NatComparison (x+(y+1)) x
+  NatGT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison (x+(y+1)) x
 
 compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
 compareNat m n =
   case compare (natValue m) (natValue n) of
-    LT -> unsafeCoerce $ NatLT (NatRepr (natValue n - natValue m - 1))
-    EQ -> unsafeCoerce $ NatEQ
-    GT -> unsafeCoerce $ NatGT (NatRepr (natValue m - natValue n - 1))
+    LT -> unsafeCoerce (NatLT @0 @0) (NatRepr (natValue n - natValue m - 1))
+    EQ -> unsafeCoerce  NatEQ
+    GT -> unsafeCoerce (NatGT @0 @0) (NatRepr (natValue m - natValue n - 1))
 
 instance OrdF NatRepr where
   compareF x y =
@@ -187,14 +228,12 @@
 instance (KnownNat n) => KnownRepr NatRepr n where
   knownRepr = knownNat
 
-{-# DEPRECATED withKnownNat "This function is potentially unsafe and is schedueled to be removed." #-}
 withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
 withKnownNat (NatRepr nVal) v =
   case someNatVal nVal of
-    Just (SomeNat (Proxy :: Proxy n')) ->
-      case unsafeCoerce (Refl :: 0 :~: 0) :: n :~: n' of
+    SomeNat (Proxy :: Proxy n') ->
+      case unsafeCoerce (Refl :: n :~: n) :: n :~: n' of
         Refl -> v
-    Nothing -> error "withKnownNat: inner value in NatRepr is not a natural"
 
 data IsZeroNat n where
   ZeroNat    :: IsZeroNat 0
@@ -204,11 +243,35 @@
 isZeroNat (NatRepr 0) = unsafeCoerce ZeroNat
 isZeroNat (NatRepr _) = unsafeCoerce NonZeroNat
 
+-- | Every nat is either zero or >= 1.
+isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
+isZeroOrGT1 n =
+  case isZeroNat n of
+    ZeroNat    -> Left Refl
+    NonZeroNat -> Right $
+      -- We have n = m + 1 for some m.
+      let
+        -- | x <= x + 1
+        leqSucc:: forall x. LeqProof x (x+1)
+        leqSucc = leqAdd2 (LeqProof :: LeqProof x x) (LeqProof :: LeqProof 0 1)
+        leqPlus :: forall f x y. ((x + 1) ~ y) => f x ->  LeqProof 1 y
+        leqPlus fx =
+          case (plusComm fx (knownNat @1) :: x + 1 :~: 1 + x)    of { Refl ->
+          case (plusMinusCancel (knownNat @1) fx :: 1+x-x :~: 1) of { Refl ->
+          case (LeqProof :: LeqProof (x+1) y)                    of { LeqProof ->
+          case (LeqProof :: LeqProof (1+x-x) (y-x))              of { LeqProof ->
+            leqTrans (LeqProof :: LeqProof 1 (y-x))
+                     (leqSub (LeqProof :: LeqProof y y)
+                             (leqTrans (leqSucc :: LeqProof x (x+1))
+                                       (LeqProof) :: LeqProof x y) :: LeqProof (y - x) y)
+          }}}}
+      in leqPlus (predNat n)
+
 -- | Decrement a @NatRepr@
 decNat :: (1 <= n) => NatRepr n -> NatRepr (n-1)
 decNat (NatRepr i) = NatRepr (i-1)
 
--- | Get the predicessor of a nat
+-- | Get the predecessor of a nat
 predNat :: NatRepr (n+1) -> NatRepr n
 predNat (NatRepr i) = NatRepr (i-1)
 
@@ -254,15 +317,15 @@
 
 -- | Return maximum unsigned value for bitvector with given width.
 maxUnsigned :: NatRepr w -> Integer
-maxUnsigned w = 2^(natValue w) - 1
+maxUnsigned w = bit (widthVal w) - 1
 
 -- | Return minimum value for bitvector in 2s complement with given width.
 minSigned :: (1 <= w) => NatRepr w -> Integer
-minSigned w = negate (2^(natValue w - 1))
+minSigned w = negate (bit (widthVal w - 1))
 
 -- | Return maximum value for bitvector in 2s complement with given width.
 maxSigned :: (1 <= w) => NatRepr w -> Integer
-maxSigned w = 2^(natValue w - 1) - 1
+maxSigned w = bit (widthVal w - 1) - 1
 
 -- | @toUnsigned w i@ maps @i@ to a @i `mod` 2^w@.
 toUnsigned :: NatRepr w -> Integer -> Integer
@@ -272,7 +335,7 @@
 -- signed number in two's complement notation and returns that value.
 toSigned :: (1 <= w) => NatRepr w -> Integer -> Integer
 toSigned w i0
-    | i > maxSigned w = i - 2^(natValue w)
+    | i > maxSigned w = i - bit (widthVal w)
     | otherwise       = i
   where i = i0 .&. maxUnsigned w
 
@@ -295,10 +358,16 @@
 ------------------------------------------------------------------------
 -- Some NatRepr
 
-someNat :: Integer -> Maybe (Some NatRepr)
-someNat n | 0 <= n && n <= toInteger maxInt = Just (Some (NatRepr (fromInteger n)))
-          | otherwise = Nothing
+-- | Turn an @Integral@ value into a @NatRepr@.  Returns @Nothing@
+--   if the given value is negative.
+someNat :: Integral a => a -> Maybe (Some NatRepr)
+someNat x | x >= 0 = Just . Some . NatRepr $! fromIntegral x
+someNat _ = Nothing
 
+-- | Turn a @Natural@ into the corresponding @NatRepr@
+mkNatRepr :: Natural -> Some NatRepr
+mkNatRepr n = Some (NatRepr n)
+
 -- | Return the maximum of two nat representations.
 maxNat :: NatRepr m -> NatRepr n -> Some NatRepr
 maxNat x y
@@ -345,8 +414,6 @@
   case unsafeCoerce (Refl :: 0 :~: 0) of
     (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> f
 
-
-
 ------------------------------------------------------------------------
 -- LeqProof
 
@@ -355,6 +422,13 @@
 data LeqProof m n where
   LeqProof :: (m <= n) => LeqProof m n
 
+-- | (<=) is a decidable relation on nats.
+decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) ((LeqProof a b) -> Void)
+decideLeq (NatRepr m) (NatRepr n)
+  | m <= n    = Left $ unsafeCoerce (LeqProof :: LeqProof 0 0)
+  | otherwise = Right $
+      \x -> seq x $ error "Impossible [decidable <= on NatRepr]"
+
 testStrictLeq :: forall m n
                . (m <= n)
               => NatRepr m
@@ -384,6 +458,31 @@
     GT -> NatCaseGT (unsafeCoerce (LeqProof :: LeqProof 0 0))
 {-# NOINLINE testNatCases #-}
 
+-- | The strict order (<), defined by n < m <-> n + 1 <= m, is irreflexive.
+lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void
+lessThanIrreflexive a prf =
+  let prf1 :: LeqProof (1 + a - a) (a - a)
+      prf1 = leqSub2 prf (LeqProof :: LeqProof a a)
+      prf2 :: 1 + a - a :~: 1
+      prf2 = plusMinusCancel (knownNat @1) a
+      prf3 :: a - a :~: 0
+      prf3 = plusMinusCancel (knownNat @0) a
+      prf4 :: LeqProof 1 0
+      prf4 = case prf2 of Refl -> case prf3 of { Refl -> prf1 }
+  in case prf4 of {}
+
+-- | The strict order on the naturals is irreflexive.
+lessThanAsymmetric :: forall m f n
+                    . LeqProof (n+1) m
+                   -> LeqProof (m+1) n
+                   -> f n
+                   -> Void
+lessThanAsymmetric nLTm mLTn n =
+  case plusComm n (knownNat @1) :: n + 1 :~: 1 + n of { Refl ->
+  case leqAdd (LeqProof :: LeqProof m m) (knownNat @1) :: LeqProof m (m+1) of
+    LeqProof -> lessThanIrreflexive n $ leqTrans (leqTrans nLTm LeqProof) mLTn
+  }
+
 -- | @x `testLeq` y@ checks whether @x@ is less than or equal to @y@.
 testLeq :: forall m n . NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
 testLeq (NatRepr m) (NatRepr n)
@@ -395,7 +494,6 @@
 leqRefl :: forall f n . f n -> LeqProof n n
 leqRefl _ = LeqProof
 
-
 -- | Apply transitivity to LeqProof
 leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
 leqTrans LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)
@@ -509,19 +607,84 @@
            -> [a]
 natForEach l h f = natForEach' l h (\LeqProof LeqProof -> f)
 
+-- | Apply a function to each element in a range starting at zero;
+-- return the list of values obtained.
+natFromZero :: forall h a
+            . NatRepr h
+           -> (forall n. (n <= h) => NatRepr n -> a)
+           -> [a]
+natFromZero = natForEach (knownNat @0)
+
 -- | Recursor for natural numbeers.
-natRec :: forall m f
-       .  NatRepr m
-       -> f 0
+natRec :: forall p f
+       .  NatRepr p
+       -> f 0 {- ^ base case -}
        -> (forall n. NatRepr n -> f n -> f (n + 1))
-       -> f m
-natRec n f0 ih = go n
-  where
-    go :: forall n'. NatRepr n' -> f n'
-    go n' = case isZeroNat n' of
-              ZeroNat    -> f0
-              NonZeroNat -> let n'' = predNat n' in ih n'' (go n'')
+       -> f p
+natRec n base ind =
+  case isZeroNat n of
+    ZeroNat    -> base
+    NonZeroNat -> let n' = predNat n
+                  in ind n' (natRec n' base ind)
 
+-- | Strong induction variant of the recursor.
+natRecStrong :: forall p f
+             .  NatRepr p
+             -> f 0 {- ^ base case -}
+             -> (forall n.
+                  NatRepr n ->
+                  (forall m. (m <= n) => NatRepr m -> f m) ->
+                  f (n + 1)) {- ^ inductive step -}
+             -> f p
+natRecStrong p base ind = natRecStrong' base ind p
+  where -- We can't use use "flip" or some other basic combinator
+        -- because type variables can't be instantiated to contain "forall"s.
+        natRecStrong' :: forall p' f'
+                      .  f' 0 {- ^ base case -}
+                      -> (forall n.
+                            NatRepr n ->
+                            (forall m. (m <= n) => NatRepr m -> f' m) ->
+                            f' (n + 1)) {- ^ inductive step -}
+                      -> NatRepr p'
+                      -> f' p'
+        natRecStrong' base' ind' n =
+          case isZeroNat n of
+            ZeroNat    -> base'
+            NonZeroNat -> ind' (predNat n) (natRecStrong' base' ind')
+
+-- | Bounded recursor for natural numbers.
+--
+-- If you can prove:
+-- - Base case: f 0
+-- - Inductive step: if n <= h and (f n) then (f (n + 1))
+-- You can conclude: for all n <= h, (f (n + 1)).
+natRecBounded :: forall m h f. (m <= h)
+              => NatRepr m
+              -> NatRepr h
+              -> f 0
+              -> (forall n. (n <= h) => NatRepr n -> f n -> f (n + 1))
+              -> f (m + 1)
+natRecBounded m h base indH =
+  case isZeroOrGT1 m of
+    Left Refl      -> indH (knownNat @0) base
+    Right LeqProof ->
+      case decideLeq m h of
+        Left LeqProof {- :: m <= h -} ->
+          let -- Since m is non-zero, it is n + 1 for some n.
+              lemma :: LeqProof (m-1) h
+              lemma = leqSub (LeqProof :: LeqProof m h) (LeqProof :: LeqProof 1 m)
+          in indH m $
+            case lemma of { LeqProof ->
+            case minusPlusCancel m (knownNat @1) of { Refl ->
+              natRecBounded @(m - 1) @h @f (predNat m) h base indH
+            }}
+        Right f {- :: (m <= h) -> Void -} ->
+          absurd $ f (LeqProof :: LeqProof m h)
+
 mulCancelR ::
   (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)
 mulCancelR _ _ _ = unsafeCoerce Refl
+
+-- | Used in @Vector@
+lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)
+lemmaMul = unsafeCoerce Refl
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Nonce.hs b/submodules/parameterized-utils/src/Data/Parameterized/Nonce.hs
--- a/submodules/parameterized-utils/src/Data/Parameterized/Nonce.hs
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Nonce.hs
@@ -16,6 +16,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
@@ -29,6 +30,7 @@
   ( -- * NonceGenerator
     NonceGenerator
   , freshNonce
+  , countNoncesGenerated
   , Nonce
   , indexValue
     -- * Accessing a nonce generator
@@ -53,7 +55,7 @@
 import Data.Parameterized.Classes
 import Data.Parameterized.Some
 
-#if MIN_VERSION_base(4,9,0)
+#if MIN_VERSION_base(4,9,0) && __GLASGOW_HASKELL__ < 805
 import Data.Kind
 #endif
 
@@ -61,47 +63,53 @@
 --
 -- The first type parameter @m@ is the monad used for generating names, and
 -- the second parameter @s@ is used for the counter.
-data NonceGenerator (m :: * -> *) (s :: *) = NonceGenerator {
+data NonceGenerator (m :: * -> *) (s :: *) where
+  STNG :: !(STRef t Word64) -> NonceGenerator (ST t) s
+  IONG :: !(IORef Word64) -> NonceGenerator IO s
+
 #if MIN_VERSION_base(4,9,0)
 -- We have to make the k explicit in GHC 8.0 to avoid a warning.
-    freshNonce :: forall k (tp :: k) . m (Nonce s tp)
+freshNonce :: forall m s k (tp :: k) . NonceGenerator m s -> m (Nonce s tp)
 #else
-    freshNonce :: forall (tp :: k) . m (Nonce s tp)
+freshNonce :: forall m s (tp :: k) . NonceGenerator m s -> m (Nonce s tp)
 #endif
-  }
+freshNonce (IONG r) =
+  atomicModifyIORef' r $ \n -> (n+1, Nonce n)
+freshNonce (STNG r) = do
+  i <- readSTRef r
+  writeSTRef r $! i+1
+  return $ Nonce i
+  -- (Weirdly, there's no atomicModifySTRef'.  Yes, only the IO monad
+  -- does concurrency, but the ST monad is part of the IO monad via
+  -- stToIO, so there's no guarantee that ST code won't be run in
+  -- multiple threads.)
 
+{-# INLINE freshNonce #-}
+  -- Inlining is particularly necessary since there's no @Monad m@
+  -- constraint on 'freshNonce', so SPECIALIZE doesn't work on it.  In
+  -- this case, though, we get specialization for free from inlining.
+  -- For instance, a @NonceGenerator IO s@ must be an @IONG@, so the
+  -- simplifier eliminates the STNG branch.
+
+-- | The number of nonces generated so far by this generator.  Only
+-- really useful for profiling.
+countNoncesGenerated :: NonceGenerator m s -> m Integer
+countNoncesGenerated (IONG r) = toInteger <$> readIORef r
+countNoncesGenerated (STNG r) = toInteger <$> readSTRef r
+
 -- | Create a new counter.
 withGlobalSTNonceGenerator :: (forall t . NonceGenerator (ST t) t -> ST t r) -> r
 withGlobalSTNonceGenerator f = runST $ do
   r <- newSTRef (toEnum 0)
-  f $! NonceGenerator {
-      freshNonce = do
-          i <- readSTRef r
-          writeSTRef r $! succ i
-          return $! Nonce i
-    }
+  f $! STNG r
 
 -- | Create a new nonce generator in the ST monad.
 newSTNonceGenerator :: ST t (Some (NonceGenerator (ST t)))
-newSTNonceGenerator = g <$> newSTRef (toEnum 0)
-  where g r = Some $!
-          NonceGenerator {
-              freshNonce = do
-                i <- readSTRef r
-                writeSTRef r $! succ i
-                return $! Nonce i
-            }
+newSTNonceGenerator = Some . STNG <$> newSTRef (toEnum 0)
 
 -- | Create a new nonce generator in the ST monad.
 newIONonceGenerator :: IO (Some (NonceGenerator IO))
-newIONonceGenerator = g <$> newIORef (toEnum 0)
-  where g r = Some $!
-          NonceGenerator {
-              freshNonce = do
-                  i <- readIORef r
-                  writeIORef r $! succ i
-                  return $! Nonce i
-            }
+newIONonceGenerator = Some . IONG <$> newIORef (toEnum 0)
 
 -- | Run a ST computation with a new nonce generator in the ST monad.
 withSTNonceGenerator :: (forall s . NonceGenerator (ST t) s -> (ST t) r) -> ST t r
@@ -152,7 +160,4 @@
 
 -- | A nonce generator that uses a globally-defined counter.
 globalNonceGenerator :: NonceGenerator IO GlobalNonceGenerator
-globalNonceGenerator =
-  NonceGenerator
-  { freshNonce = Nonce <$> atomicModifyIORef' globalNonceIORef (\n -> (n+1, n))
-  }
+globalNonceGenerator = IONG globalNonceIORef
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Peano.hs b/submodules/parameterized-utils/src/Data/Parameterized/Peano.hs
new file mode 100644
--- /dev/null
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Peano.hs
@@ -0,0 +1,285 @@
+{-|
+
+This defines a type 'Peano' and 'PeanoRepr' for representing a
+type-level natural at runtime. These type-level numbers are defined
+inductively instead of using GHC.TypeLits.
+
+As a result, type-level computation defined recursively over these
+numbers works more smoothly. (For example, see the type-level
+function Repeatn below.)
+
+Note: as in NatRepr, the runtime representation of these type-level
+natural numbers is an Int.
+
+-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if MIN_VERSION_base(4,9,0)
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+#endif
+#if __GLASGOW_HASKELL__ >= 805
+{-# LANGUAGE NoStarIsType #-}
+#endif
+module Data.Parameterized.Peano
+   ( Peano
+     , Z , S
+     , Plus, Minus, Mul, Le, Lt, Gt, Ge, Max, Min, Repeat
+     , plusP, minusP, mulP, maxP, minP, repeatP
+     , zeroP, succP, predP
+
+     , KnownPeano
+     , withKnownPeano
+
+     , PeanoRepr, peanoValue
+     , PeanoView(..), peanoView
+     , viewRepr
+
+     , somePeano
+     , mkPeanoRepr
+     , maxPeano
+     , minPeano
+
+     -- * Re-exports
+     , TestEquality(..)
+     , (:~:)(..)
+     , Data.Parameterized.Some.Some
+
+     ) where
+
+import           Data.Parameterized.Classes
+import           Data.Parameterized.DecidableEq
+import           Data.Parameterized.Some
+
+import           Data.Hashable
+import           Data.Constraint
+import           Data.Word
+
+import           Unsafe.Coerce(unsafeCoerce)
+
+------------------------------------------------------------------------
+-- ** Peano - a unary representation of natural numbers
+
+data Peano = Z | S Peano
+-- | Peano zero
+type Z = 'Z
+-- | Peano successor
+type S = 'S
+
+-- Peano numbers are more about *counting* than arithmetic.
+-- They are most useful as iteration arguments and list indices
+-- However, for completeness, we define a few standard
+-- operations.
+
+type family Plus (a :: Peano) (b :: Peano) :: Peano where
+  Plus Z     b = b
+  Plus (S a) b = S (Plus a b)
+
+type family Minus (a :: Peano) (b :: Peano) :: Peano where
+  Minus Z     b     = Z
+  Minus (S a) (S b) = Minus a b
+  Minus a    Z      = a
+
+type family Mul (a :: Peano) (b :: Peano) :: Peano where
+  Mul Z     b = Z
+  Mul (S a) b = Plus a (Mul a b)
+
+type family Le  (a :: Peano) (b :: Peano) :: Bool where
+  Le  a  a        = 'True
+  Le  Z  b        = 'True
+  Le  a  Z        = 'False
+  Le  (S a) (S b) = Le a b
+
+type family Lt  (a :: Peano) (b :: Peano) :: Bool where
+  Lt a b = Le (S a) b
+
+type family Gt  (a :: Peano) (b :: Peano) :: Bool where
+  Gt a b = Lt b a
+
+type family Ge  (a :: Peano) (b :: Peano) :: Bool where
+  Ge a b = Le b a
+
+type family Max (a :: Peano) (b :: Peano) :: Peano where
+  Max Z b = b
+  Max a Z = a
+  Max (S a) (S b) = S (Max a b)
+
+type family Min (a :: Peano) (b :: Peano) :: Peano where
+  Min Z b = Z
+  Min a Z = Z
+  Min (S a) (S b) = S (Min a b)
+
+-- Apply a constructor 'f' n-times to an argument 's'
+type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where
+  Repeat Z f s     = s
+  Repeat (S m) f s = f (Repeat m f s)
+
+
+------------------------------------------------------------------------
+-- ** Run time representation of Peano numbers
+
+-- | The run time value, stored as an Word64
+-- As these are unary numbers, we don't worry about overflow.
+newtype PeanoRepr (n :: Peano) =
+  PeanoRepr { peanoValue :: Word64 }
+
+-- n is Phantom in the definition, but we don't want to allow coerce
+type role PeanoRepr nominal
+
+----------------------------------------------------------
+
+-- | Because we have optimized the runtime representation,
+-- we need to have a "view" that decomposes the representation
+-- into the standard form.
+data PeanoView (n :: Peano) where
+  ZRepr :: PeanoView Z
+  SRepr :: PeanoRepr n -> PeanoView (S n)
+
+-- | Test whether a number is Zero or Successor
+peanoView :: PeanoRepr n -> PeanoView n
+peanoView (PeanoRepr i) =
+  if i == 0 then unsafeCoerce ZRepr else unsafeCoerce (SRepr (PeanoRepr (i-1)))
+
+-- | convert the view back to the runtime representation
+viewRepr :: PeanoView n -> PeanoRepr n
+viewRepr ZRepr     = PeanoRepr 0
+viewRepr (SRepr n) = PeanoRepr (peanoValue n + 1)
+
+----------------------------------------------------------
+
+instance Hashable (PeanoRepr n) where
+  hashWithSalt i (PeanoRepr x) = hashWithSalt i x
+
+instance Eq (PeanoRepr m) where
+  _ == _ = True
+
+instance TestEquality PeanoRepr where
+  testEquality (PeanoRepr m) (PeanoRepr n)
+    | m == n = Just (unsafeCoerce Refl)
+    | otherwise = Nothing
+
+instance DecidableEq PeanoRepr where
+  decEq (PeanoRepr m) (PeanoRepr n)
+    | m == n    = Left $ unsafeCoerce Refl
+    | otherwise = Right $
+        \x -> seq x $ error "Impossible [DecidableEq on PeanoRepr]"
+
+instance OrdF PeanoRepr where
+  compareF (PeanoRepr m) (PeanoRepr n)
+    | m < n     = unsafeCoerce LTF
+    | m == n    = unsafeCoerce EQF
+    | otherwise = unsafeCoerce GTF
+
+instance PolyEq (PeanoRepr m) (PeanoRepr n) where
+  polyEqF x y = (\Refl -> Refl) <$> testEquality x y
+
+-- Display as digits, not in unary
+instance Show (PeanoRepr p) where
+  show p = show (peanoValue p)
+
+instance ShowF PeanoRepr
+
+instance HashableF PeanoRepr where
+  hashWithSaltF = hashWithSalt
+
+----------------------------------------------------------
+-- * Implicit runtime Peano numbers
+
+type KnownPeano = KnownRepr PeanoRepr
+
+instance KnownRepr PeanoRepr Z where
+  knownRepr = viewRepr ZRepr
+instance (KnownRepr PeanoRepr n) => KnownRepr PeanoRepr (S n) where
+  knownRepr = viewRepr (SRepr knownRepr)
+
+newtype DI a = Don'tInstantiate (KnownPeano a => Dict (KnownPeano a))
+
+peanoInstance :: forall a . PeanoRepr a -> Dict (KnownPeano a)
+peanoInstance s = with_sing_i Dict
+  where
+    with_sing_i :: (KnownPeano a => Dict (KnownPeano a)) -> Dict (KnownPeano a)
+    with_sing_i si = unsafeCoerce (Don'tInstantiate si) s
+
+-- | convert an explicit number to an implicit number
+withKnownPeano :: forall n r. PeanoRepr n -> (KnownPeano n => r) -> r
+withKnownPeano si r = case peanoInstance si of
+                        Dict -> r
+
+----------------------------------------------------------
+-- * Operations on runtime numbers
+
+-- | zero
+zeroP :: PeanoRepr Z
+zeroP = PeanoRepr 0
+
+-- | Successor, Increment
+succP :: PeanoRepr n -> PeanoRepr (S n)
+succP (PeanoRepr i) = PeanoRepr (i+1)
+
+-- | Get the predecessor (decrement)
+predP :: PeanoRepr (S n) -> PeanoRepr n
+predP (PeanoRepr i) = PeanoRepr (i-1)
+
+
+plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)
+plusP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a + b)
+
+minusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)
+minusP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a - b)
+
+mulP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)
+mulP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a * b)
+
+maxP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)
+maxP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (max a b)
+
+minP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)
+minP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (min a b)
+
+repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)
+repeatP n f s = case peanoView n of
+  ZRepr   -> s
+  SRepr m -> f (repeatP m f s)
+
+------------------------------------------------------------------------
+-- * Some PeanoRepr
+
+-- | Convert a Word64 to a PeanoRepr
+mkPeanoRepr :: Word64 -> Some PeanoRepr
+mkPeanoRepr n = Some (PeanoRepr n)
+
+-- | Turn an @Integral@ value into a @PeanoRepr@.  Returns @Nothing@
+--   if the given value is negative.
+somePeano :: Integral a => a -> Maybe (Some PeanoRepr)
+somePeano x | x >= 0 = Just . Some . PeanoRepr $! fromIntegral x
+somePeano _ = Nothing
+
+-- | Return the maximum of two representations.
+maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
+maxPeano x y
+  | peanoValue x >= peanoValue y = Some x
+  | otherwise = Some y
+
+-- | Return the minimum of two representations.
+minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
+minPeano x y
+  | peanoValue y >= peanoValue x = Some x
+  | otherwise = Some y
+
+------------------------------------------------------------------------
+--  LocalWords:  PeanoRepr withKnownPeano runtime Peano unary
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/TestEquality.hs b/submodules/parameterized-utils/src/Data/Parameterized/TestEquality.hs
new file mode 100644
--- /dev/null
+++ b/submodules/parameterized-utils/src/Data/Parameterized/TestEquality.hs
@@ -0,0 +1,36 @@
+{-|
+Copyright        : (c) Galois, Inc 2014-2018
+Maintainer       : Langston Barrett <langston@galois.com
+
+Utilities for working with "Data.Type.TestEquality".
+
+NB: This module contains an orphan instance.
+-}
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+
+import Data.Functor.Compose
+import Data.Type.Equality
+
+testEqualityComposeBare :: forall f g x y.
+                           (forall w z. f w -> f z -> Maybe (w :~: z))
+                        -> Compose f g x
+                        -> Compose f g y
+                        -> Maybe (x :~: y)
+testEqualityComposeBare testEquality_ (Compose x) (Compose y) =
+  case (testEquality_ x y :: Maybe (g x :~: g y)) of
+    Just Refl -> Just (Refl :: x :~: y)
+    Nothing   -> Nothing
+
+testEqualityCompose :: forall f g x y. (TestEquality f)
+                    => Compose f g x
+                    -> Compose f g y
+                    -> Maybe (x :~: y)
+testEqualityCompose = testEqualityComposeBare testEquality
+
+-- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.
+instance (TestEquality f) => TestEquality (Compose f g) where
+  testEquality = testEqualityCompose
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/TraversableF.hs b/submodules/parameterized-utils/src/Data/Parameterized/TraversableF.hs
--- a/submodules/parameterized-utils/src/Data/Parameterized/TraversableF.hs
+++ b/submodules/parameterized-utils/src/Data/Parameterized/TraversableF.hs
@@ -7,8 +7,10 @@
 -- This module declares classes for working with structures that accept
 -- a single parametric type parameter.
 ------------------------------------------------------------------------
+{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE Trustworthy #-}
 module Data.Parameterized.TraversableF
   ( FunctorF(..)
@@ -24,10 +26,13 @@
 import Control.Applicative
 import Control.Monad.Identity
 import Data.Coerce
+import Data.Functor.Compose (Compose(..))
 import Data.Monoid
 import GHC.Exts (build)
 
--- | A parameterized type that is a function on all instances.
+import Data.Parameterized.TraversableFC
+
+-- | A parameterized type that is a functor on all instances.
 class FunctorF m where
   fmapF :: (forall x . f x -> g x) -> m f -> m g
 
@@ -37,7 +42,7 @@
 ------------------------------------------------------------------------
 -- FoldableF
 
--- | This is a coercision used to avoid overhead associated
+-- | This is a coercion used to avoid overhead associated
 -- with function composition.
 (#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c)
 (#.) _f = coerce
@@ -112,5 +117,30 @@
 
 -- | Map each element of a structure to an action, evaluate
 -- these actions from left to right, and ignore the results.
-traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f ()) -> t e -> f ()
+traverseF_ :: (FoldableF t, Applicative f) => (forall s . e s  -> f a) -> t e -> f ()
 traverseF_ f = foldrF (\e r -> f e *> r) (pure ())
+
+------------------------------------------------------------------------
+-- TraversableF (Compose s t)
+
+instance ( FunctorF (s :: (k -> *) -> *)
+         , FunctorFC (t :: (l -> *) -> (k -> *))
+         ) =>
+         FunctorF (Compose s t) where
+  fmapF f (Compose v) = Compose $ fmapF (fmapFC f) v
+
+instance ( TraversableF (s :: (k -> *) -> *)
+         , TraversableFC (t :: (l -> *) -> (k -> *))
+         ) =>
+         FoldableF (Compose s t) where
+  foldMapF = foldMapFDefault
+
+-- | Traverse twice over: go under the @t@, under the @s@ and lift @m@ out.
+instance ( TraversableF (s :: (k -> *) -> *)
+         , TraversableFC (t :: (l -> *) -> (k -> *))
+         ) =>
+         TraversableF (Compose s t) where
+  traverseF :: forall (f :: l -> *) (g :: l -> *) m. (Applicative m) =>
+               (forall (u :: l). f u -> m (g u))
+            -> Compose s t f -> m (Compose s t g)
+  traverseF f (Compose v) = Compose <$> traverseF (traverseFC f) v
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/TraversableFC.hs b/submodules/parameterized-utils/src/Data/Parameterized/TraversableFC.hs
--- a/submodules/parameterized-utils/src/Data/Parameterized/TraversableFC.hs
+++ b/submodules/parameterized-utils/src/Data/Parameterized/TraversableFC.hs
@@ -150,12 +150,12 @@
 
 -- | Map each element of a structure to an action, evaluate
 -- these actions from left to right, and ignore the results.
-traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m ()) -> (forall x. t f x -> m ())
+traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m a) -> (forall x. t f x -> m ())
 traverseFC_ f = foldrFC (\e r -> f e *> r) (pure ())
 {-# INLINE traverseFC_ #-}
 
 -- | Map each element of a structure to an action, evaluate
 -- these actions from left to right, and ignore the results.
-forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m ()) -> m ()
+forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m ()
 forMFC_ v f = traverseFC_ f v
 {-# INLINE forMFC_ #-}
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Utils/Endian.hs b/submodules/parameterized-utils/src/Data/Parameterized/Utils/Endian.hs
new file mode 100644
--- /dev/null
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Utils/Endian.hs
@@ -0,0 +1,3 @@
+module Data.Parameterized.Utils.Endian where
+
+data Endian = LittleEndian | BigEndian deriving (Eq,Show,Ord)
diff --git a/submodules/parameterized-utils/src/Data/Parameterized/Vector.hs b/submodules/parameterized-utils/src/Data/Parameterized/Vector.hs
new file mode 100644
--- /dev/null
+++ b/submodules/parameterized-utils/src/Data/Parameterized/Vector.hs
@@ -0,0 +1,507 @@
+{-# Language GADTs, DataKinds, TypeOperators, BangPatterns #-}
+{-# Language PatternGuards #-}
+{-# Language TypeApplications, ScopedTypeVariables #-}
+{-# Language Rank2Types, RoleAnnotations #-}
+{-# Language CPP #-}
+#if __GLASGOW_HASKELL__ >= 805
+{-# Language NoStarIsType #-}
+#endif
+-- | A vector fixed-size vector of typed elements.
+module Data.Parameterized.Vector
+  ( Vector
+    -- * Lists
+  , fromList
+  , toList
+
+    -- * Length
+  , length
+  , nonEmpty
+  , lengthInt
+
+  -- * Indexing
+  , elemAt
+  , elemAtMaybe
+  , elemAtUnsafe
+
+  -- * Update
+  , insertAt
+  , insertAtMaybe
+
+    -- * Sub sequences
+  , uncons
+  , slice
+  , Data.Parameterized.Vector.take
+
+    -- * Zipping
+  , zipWith
+  , zipWithM
+  , zipWithM_
+  , interleave
+
+    -- * Reorder
+  , shuffle
+  , reverse
+  , rotateL
+  , rotateR
+  , shiftL
+  , shiftR
+
+    -- * Construction
+  , singleton
+  , cons
+  , snoc
+  , generate
+  , generateM
+
+    -- * Splitting and joining
+    -- ** General
+  , joinWithM
+  , joinWith
+  , splitWith
+  , splitWithA
+
+    -- ** Vectors
+  , split
+  , join
+  , append
+
+  ) where
+
+import qualified Data.Vector as Vector
+import Data.Functor.Compose
+import Data.Coerce
+import Data.Vector.Mutable (MVector)
+import qualified Data.Vector.Mutable as MVector
+import Control.Monad.ST
+import Data.Functor.Identity
+import Data.Parameterized.NatRepr
+import Data.Proxy
+import Prelude hiding (length,reverse,zipWith)
+import Numeric.Natural
+
+import Data.Parameterized.Utils.Endian
+
+-- | Fixed-size non-empty vectors.
+data Vector n a where
+  Vector :: (1 <= n) => !(Vector.Vector a) -> Vector n a
+
+type role Vector nominal representational
+
+instance Eq a => Eq (Vector n a) where
+  (Vector x) == (Vector y) = x == y
+
+instance Show a => Show (Vector n a) where
+  show (Vector x) = show x
+
+-- | Get the elements of the vector as a list, lowest index first.
+toList :: Vector n a -> [a]
+toList (Vector v) = Vector.toList v
+{-# Inline toList #-}
+
+-- | Length of the vector.
+-- @O(1)@
+length :: Vector n a -> NatRepr n
+length (Vector xs) =
+  activateNatReprCoercionBackdoor_IPromiseIKnowWhatIAmDoing $ \mk ->
+    mk (fromIntegral (Vector.length xs) :: Natural)
+{-# INLINE length #-}
+
+-- | The length of the vector as an "Int".
+lengthInt :: Vector n a -> Int
+lengthInt (Vector xs) = Vector.length xs
+{-# Inline lengthInt #-}
+
+elemAt :: ((i+1) <= n) => NatRepr i -> Vector n a -> a
+elemAt n (Vector xs) = xs Vector.! widthVal n
+
+-- | Get the element at the given index.
+-- @O(1)@
+elemAtMaybe :: Int -> Vector n a -> Maybe a
+elemAtMaybe n (Vector xs) = xs Vector.!? n
+{-# INLINE elemAt #-}
+
+-- | Get the element at the given index.
+-- Raises an exception if the element is not in the vector's domain.
+-- @O(1)@
+elemAtUnsafe :: Int -> Vector n a -> a
+elemAtUnsafe n (Vector xs) = xs Vector.! n
+{-# INLINE elemAtUnsafe #-}
+
+
+-- | Insert an element at the given index.
+-- @O(n)@.
+insertAt :: ((i + 1) <= n) => NatRepr i -> a -> Vector n a -> Vector n a
+insertAt n a (Vector xs) = Vector (Vector.unsafeUpd xs [(widthVal n,a)])
+
+-- | Insert an element at the given index.
+-- Return 'Nothing' if the element is outside the vector bounds.
+-- @O(n)@.
+insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a)
+insertAtMaybe n a (Vector xs)
+  | 0 <= n && n < Vector.length xs = Just (Vector (Vector.unsafeUpd xs [(n,a)]))
+  | otherwise = Nothing
+
+
+-- | Proof that the length of this vector is not 0.
+nonEmpty :: Vector n a -> LeqProof 1 n
+nonEmpty (Vector _) = LeqProof
+{-# Inline nonEmpty #-}
+
+
+-- | Remove the first element of the vector, and return the rest, if any.
+uncons :: forall n a.  Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))
+uncons v@(Vector xs) = (Vector.head xs, mbTail)
+  where
+  mbTail :: Either (n :~: 1) (Vector (n - 1) a)
+  mbTail = case testStrictLeq (knownNat @1) (length v) of
+             Left n2_leq_n ->
+               do LeqProof <- return (leqSub2 n2_leq_n (leqRefl (knownNat @1)))
+                  return (Vector (Vector.tail xs))
+             Right Refl    -> Left Refl
+{-# Inline uncons #-}
+
+
+--------------------------------------------------------------------------------
+
+-- | Make a vector of the given length and element type.
+-- Returns "Nothing" if the input list does not have the right number of
+-- elements.
+-- @O(n)@.
+fromList :: (1 <= n) => NatRepr n -> [a] -> Maybe (Vector n a)
+fromList n xs
+  | widthVal n == Vector.length v = Just (Vector v)
+  | otherwise                     = Nothing
+  where
+  v = Vector.fromList xs
+{-# INLINE fromList #-}
+
+
+-- | Extract a subvector of the given vector.
+slice :: (i + w <= n, 1 <= w) =>
+            NatRepr i {- ^ Start index -} ->
+            NatRepr w {- ^ Width of sub-vector -} ->
+            Vector n a -> Vector w a
+slice i w (Vector xs) = Vector (Vector.slice (widthVal i) (widthVal w) xs)
+{-# INLINE slice #-}
+
+-- | Take the front (lower-indexes) part of the vector.
+take :: forall n x a. (1 <= n) => NatRepr n -> Vector (n + x) a -> Vector n a
+take | LeqProof <- prf = slice (knownNat @0)
+  where
+  prf = leqAdd (leqRefl (Proxy @n)) (Proxy @x)
+
+--------------------------------------------------------------------------------
+
+instance Functor (Vector n) where
+  fmap f (Vector xs) = Vector (Vector.map f xs)
+  {-# Inline fmap #-}
+
+instance Foldable (Vector n) where
+  foldMap f (Vector xs) = foldMap f xs
+
+instance Traversable (Vector n) where
+  traverse f (Vector xs) = Vector <$> traverse f xs
+  {-# Inline traverse #-}
+
+-- | Zip two vectors, potentially changing types.
+-- @O(n)@
+zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
+zipWith f (Vector xs) (Vector ys) = Vector (Vector.zipWith f xs ys)
+{-# Inline zipWith #-}
+
+zipWithM :: Monad m => (a -> b -> m c) ->
+                       Vector n a -> Vector n b -> m (Vector n c)
+zipWithM f (Vector xs) (Vector ys) = Vector <$> Vector.zipWithM f xs ys
+{-# Inline zipWithM #-}
+
+zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()
+zipWithM_ f (Vector xs) (Vector ys) = Vector.zipWithM_ f xs ys
+{-# Inline zipWithM_ #-}
+
+{- | Interleave two vectors.  The elements of the first vector are
+at even indexes in the result, the elements of the second are at odd indexes. -}
+interleave ::
+  forall n a. (1 <= n) => Vector n a -> Vector n a -> Vector (2 * n) a
+interleave (Vector xs) (Vector ys)
+  | LeqProof <- leqMulPos (Proxy @2) (Proxy @n) = Vector zs
+  where
+  len = Vector.length xs + Vector.length ys
+  zs  = Vector.generate len (\i -> let v = if even i then xs else ys
+                                   in v Vector.! (i `div` 2))
+
+
+--------------------------------------------------------------------------------
+
+{- | Move the elements around, as specified by the given function.
+  * Note: the reindexing function says where each of the elements
+          in the new vector come from.
+  * Note: it is OK for the same input element to end up in mulitple places
+          in the result.
+@O(n)@
+-}
+shuffle :: (Int -> Int) -> Vector n a -> Vector n a
+shuffle f (Vector xs) = Vector ys
+  where
+  ys = Vector.generate (Vector.length xs) (\i -> xs Vector.! f i)
+{-# Inline shuffle #-}
+
+-- | Reverse the vector.
+reverse :: forall a n. (1 <= n) => Vector n a -> Vector n a
+reverse x = shuffle (\i -> lengthInt x - i - 1) x
+
+-- | Rotate "left".  The first element of the vector is on the "left", so
+-- rotate left moves all elemnts toward the corresponding smaller index.
+-- Elements that fall off the beginning end up at the end.
+rotateL :: Int -> Vector n a -> Vector n a
+rotateL !n xs = shuffle rotL xs
+  where
+  !len   = lengthInt xs
+  rotL i = (i + n) `mod` len          -- `len` is known to be >= 1
+{-# Inline rotateL #-}
+
+-- | Rotate "right".  The first element of the vector is on the "left", so
+-- rotate right moves all elemnts toward the corresponding larger index.
+-- Elements that fall off the end, end up at the beginning.
+rotateR :: Int -> Vector n a -> Vector n a
+rotateR !n xs = shuffle rotR xs
+  where
+  !len   = lengthInt xs
+  rotR i = (i - n) `mod` len        -- `len` is known to be >= 1
+{-# Inline rotateR #-}
+
+{- | Move all elements towards smaller indexes.
+Elements that fall off the front are ignored.
+Empty slots are filled in with the given element.
+@O(n)@. -}
+shiftL :: Int -> a -> Vector n a -> Vector n a
+shiftL !x a (Vector xs) = Vector ys
+  where
+  !len = Vector.length xs
+  ys   = Vector.generate len (\i -> let j = i + x
+                                    in if j >= len then a else xs Vector.! j)
+{-# Inline shiftL #-}
+
+{- | Move all elements towards the larger indexes.
+Elements that "fall" off the end are ignored.
+Empty slots are filled in with the given element.
+@O(n)@. -}
+shiftR :: Int -> a -> Vector n a -> Vector n a
+shiftR !x a (Vector xs) = Vector ys
+  where
+  !len = Vector.length xs
+  ys   = Vector.generate len (\i -> let j = i - x
+                                    in if j < 0 then a else xs Vector.! j)
+{-# Inline shiftR #-}
+
+-------------------------------------------------------------------------------i
+
+-- | Append two vectors. The first one is at lower indexes in the result.
+append :: Vector m a -> Vector n a -> Vector (m + n) a
+append v1@(Vector xs) v2@(Vector ys) =
+  case leqAddPos (length v1) (length v2) of { LeqProof ->
+    Vector (xs Vector.++ ys)
+  }
+{-# Inline append #-}
+
+--------------------------------------------------------------------------------
+-- Constructing Vectors
+
+-- | Vector with exactly one element
+singleton :: forall a. a -> Vector 1 a
+singleton a = Vector (Vector.singleton a)
+
+leqLen :: forall n a. Vector n a -> LeqProof 1 (n + 1)
+leqLen v =
+  let leqSucc :: forall f z. f z -> LeqProof z (z + 1)
+      leqSucc fz = leqAdd (leqRefl fz :: LeqProof z z) (knownNat @1)
+  in leqTrans (nonEmpty v :: LeqProof 1 n) (leqSucc (length v))
+
+-- | Add an element to the head of a vector
+cons :: forall n a. a -> Vector n a -> Vector (n+1) a
+cons a v@(Vector x) = case leqLen v of LeqProof -> (Vector (Vector.cons a x))
+
+-- | Add an element to the tail of a vector
+snoc :: forall n a. Vector n a -> a -> Vector (n+1) a
+snoc v@(Vector x) a = case leqLen v of LeqProof -> (Vector (Vector.snoc x a))
+
+-- | This newtype wraps Vector so that we can curry it in the call to
+-- @natRecBounded@. It adds 1 to the length so that the base case is
+-- a @Vector@ of non-zero length.
+newtype Vector' a n = MkVector' (Vector (n+1) a)
+
+unVector' :: Vector' a n -> Vector (n+1) a
+unVector' (MkVector' v) = v
+
+snoc' :: forall a m. Vector' a m -> a -> Vector' a (m+1)
+snoc' v = MkVector' . snoc (unVector' v)
+
+generate' :: forall h a
+           . NatRepr h
+          -> (forall n. (n <= h) => NatRepr n -> a)
+          -> Vector' a h
+generate' h gen =
+  case isZeroOrGT1 h of
+    Left Refl -> base
+    Right LeqProof ->
+      case (minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h) of { Refl ->
+      natRecBounded (decNat h) (decNat h) base step
+      }
+  where base :: Vector' a 0
+        base = MkVector' $ singleton (gen (knownNat @0))
+        step :: forall m. (1 <= h, m <= h - 1)
+             => NatRepr m -> Vector' a m -> Vector' a (m + 1)
+        step m v =
+          case minusPlusCancel h (knownNat @1) :: h - 1 + 1 :~: h of { Refl ->
+          case (leqAdd2 (LeqProof :: LeqProof m (h-1))
+                        (LeqProof :: LeqProof 1 1) :: LeqProof (m+1) h) of { LeqProof ->
+            snoc' v (gen (incNat m))
+          }}
+
+-- | Apply a function to each element in a range starting at zero;
+-- return the a vector of values obtained.
+-- cf. both @natFromZero@ and @Data.Vector.generate@
+generate :: forall h a
+          . NatRepr h
+         -> (forall n. (n <= h) => NatRepr n -> a)
+         -> Vector (h + 1) a
+generate h gen = unVector' (generate' h gen)
+
+-- | Since @Vector@ is traversable, we can pretty trivially sequence
+-- @natFromZeroVec@ inside a monad.
+generateM :: forall m h a. (Monad m)
+          => NatRepr h
+          -> (forall n. (n <= h) => NatRepr n -> m a)
+          -> m (Vector (h + 1) a)
+generateM h gen = sequence $ generate h gen
+
+--------------------------------------------------------------------------------
+
+coerceVec :: Coercible a b => Vector n a -> Vector n b
+coerceVec = coerce
+
+-- | Monadically join a vector of values, using the given function.
+-- This functionality can sometimes be reproduced by creating a newtype
+-- wrapper and using @joinWith@, this implementation is provided for
+-- convenience.
+joinWithM ::
+  forall m f n w.
+  (1 <= w, Monad m) =>
+  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> m (f (w + l)))
+  {- ^ A function for appending contained elements.
+       Earlier vector indexes are the first argument of the join function.
+       Pass a different function to implmenet little/big endian behaviors -} ->
+  NatRepr w -> Vector n (f w) -> m (f (n * w))
+
+joinWithM jn w = fmap fst . go
+  where
+  go :: forall l. Vector l (f w) -> m (f (l * w), NatRepr (l * w))
+  go exprs =
+    case uncons exprs of
+      (a, Left Refl) -> return (a, w)
+      (a, Right rest) ->
+        case nonEmpty rest                of { LeqProof ->
+        case leqMulPos (length rest) w    of { LeqProof ->
+        case nonEmpty exprs               of { LeqProof ->
+        case lemmaMul w (length exprs)    of { Refl -> do
+          -- @siddharthist: This could probably be written applicatively?
+          (res, sz) <- go rest
+          joined <- jn sz a res
+          return (joined, addNat w sz)
+        }}}}
+
+-- | Join a vector of values, using the given function.
+joinWith ::
+  forall f n w.
+  (1 <= w) =>
+  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> f (w + l))
+  {- ^ A function for appending contained elements.
+       Earlier vector indexes are the first argument of the join function.
+       Pass a different function to implmenet little/big endian behaviors -} ->
+  NatRepr w -> Vector n (f w) -> f (n * w)
+joinWith jn w v = runIdentity $ joinWithM (\n x -> pure . (jn n x)) w v
+{-# Inline joinWith #-}
+
+-- | Split a bit-vector into a vector of bit-vectors.
+-- If "LittleEndian", then less significant bits go into smaller indexes.
+-- If "BigEndian", then less significant bits go into larger indexes.
+splitWith :: forall f w n.
+  (1 <= w, 1 <= n) =>
+  Endian ->
+  (forall i. (i + w <= n * w) =>
+             NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)
+  {- ^ A function for slicing out a chunk of length @w@, starting at @i@ -} ->
+  NatRepr n -> NatRepr w -> f (n * w) -> Vector n (f w)
+splitWith endian select n w val = Vector (Vector.create initializer)
+  where
+  len          = widthVal n
+  start :: Int
+  next :: Int -> Int
+  (start,next) = case endian of
+                   LittleEndian -> (0, succ)
+                   BigEndian    -> (len - 1, pred)
+
+  initializer :: forall s. ST s (MVector s (f w))
+  initializer =
+    do LeqProof <- return (leqMulPos n w)
+       LeqProof <- return (leqMulMono n w)
+
+       v <- MVector.new len
+       let fill :: Int -> NatRepr i -> ST s ()
+           fill loc i =
+             let end = addNat i w in
+             case testLeq end inLen of
+               Just LeqProof ->
+                 do MVector.write v loc (select inLen i val)
+                    fill (next loc) end
+               Nothing -> return ()
+
+
+       fill start (knownNat @0)
+       return v
+
+  inLen :: NatRepr (n * w)
+  inLen = natMultiply n w
+{-# Inline splitWith #-}
+
+-- We can sneakily put our functor in the parameter "f" of @splitWith@ using the
+-- @Compose@ newtype.
+-- | An applicative version of @splitWith@.
+splitWithA :: forall f g w n. (Applicative f, 1 <= w, 1 <= n) =>
+  Endian ->
+  (forall i. (i + w <= n * w) =>
+             NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w))
+  {- ^ f function for slicing out f chunk of length @w@, starting at @i@ -} ->
+  NatRepr n -> NatRepr w -> g (n * w) -> f (Vector n (g w))
+splitWithA e select n w val = traverse getCompose $
+  splitWith @(Compose f g) e select' n w $ Compose (pure val)
+  where -- Wrap everything in Compose
+        select' :: (forall i. (i + w <= n * w)
+                => NatRepr (n * w) -> NatRepr i -> Compose f g (n * w) -> Compose f g w)
+        -- Whatever we pass in as "val" is what's passed to select anyway,
+        -- so there's no need to examine the argument. Just use "val" directly here.
+        select' nw i _ = Compose $ select nw i val
+
+newtype Vec a n = Vec (Vector n a)
+
+vSlice :: (i + w <= l, 1 <= w) =>
+  NatRepr w -> NatRepr l -> NatRepr i -> Vec a l -> Vec a w
+vSlice w _ i (Vec xs) = Vec (slice i w xs)
+{-# Inline vSlice #-}
+
+-- | Append the two bit vectors.  The first argument is
+-- at the lower indexes of the resulting vector.
+vAppend :: NatRepr n -> Vec a m -> Vec a n -> Vec a (m + n)
+vAppend _ (Vec xs) (Vec ys) = Vec (append xs ys)
+{-# Inline vAppend #-}
+
+-- | Split a vector into a vector of vectors.
+split :: (1 <= w, 1 <= n) =>
+        NatRepr n -> NatRepr w -> Vector (n * w) a -> Vector n (Vector w a)
+split n w xs = coerceVec (splitWith LittleEndian (vSlice w) n w (Vec xs))
+{-# Inline split #-}
+
+-- | Join a vector of vectors into a single vector.
+join :: (1 <= w) => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a
+join w xs = ys
+  where Vec ys = joinWith vAppend w (coerceVec xs)
+{-# Inline join #-}
diff --git a/submodules/parameterized-utils/test/Test/Context.hs b/submodules/parameterized-utils/test/Test/Context.hs
--- a/submodules/parameterized-utils/test/Test/Context.hs
+++ b/submodules/parameterized-utils/test/Test/Context.hs
@@ -16,6 +16,7 @@
 import Data.Parameterized.TraversableFC
 import Data.Parameterized.Some
 
+import qualified Data.Parameterized.Context as C
 import qualified Data.Parameterized.Context.Safe as S
 import qualified Data.Parameterized.Context.Unsafe as U
 
@@ -167,4 +168,11 @@
          case testEquality x y of
            Just Refl -> return $ vals1 == vals2
            Nothing   -> return $ vals1 /= vals2
+
+   , testProperty "append_take" $ \vals1 vals2 -> ioProperty $ do
+         Some x <- return $ mkUAsgn vals1
+         Some y <- return $ mkUAsgn vals2
+         let z = x U.<++> y
+         let x' = C.take (U.size x) (U.size y) z
+         return $ isJust $ testEquality x x'
    ]
diff --git a/submodules/parameterized-utils/test/Test/Vector.hs b/submodules/parameterized-utils/test/Test/Vector.hs
new file mode 100644
--- /dev/null
+++ b/submodules/parameterized-utils/test/Test/Vector.hs
@@ -0,0 +1,67 @@
+{-# Language DataKinds #-}
+{-# Language ExplicitForAll #-}
+{-# Language TypeOperators #-}
+{-# Language TypeFamilies #-}
+{-# Language FlexibleInstances #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language StandaloneDeriving #-}
+{-# Language CPP #-}
+#if __GLASGOW_HASKELL__ >= 805
+{-# Language NoStarIsType #-}
+#endif
+module Test.Vector
+( vecTests
+) where
+
+import Test.Tasty
+import Test.Tasty.QuickCheck (Arbitrary(..), Gen, testProperty)
+
+import Data.Parameterized.NatRepr
+import Data.Parameterized.Vector
+import GHC.TypeLits
+import Prelude hiding (reverse)
+
+instance KnownNat n => Arbitrary (NatRepr n) where
+  arbitrary = return knownNat
+
+-- GHC thinks that this instances overlaps with the
+-- "Arbitrary a => Arbitrary (Maybe a)" instance from QuickCheck, but it doesn't:
+-- there is no "Arbitrary a => Arbitrary (Vector n a)".
+--
+-- While it might seem like this would just successfully generate a lot
+-- of "Nothing", it does a pretty good job. Just try changing one of the tests!
+instance {-# OVERLAPS #-} forall a n. (1 <= n, Arbitrary a, KnownNat n)
+    => Arbitrary (Maybe (Vector n a)) where
+  arbitrary = do
+    n <- (arbitrary :: Gen (NatRepr n))
+    l <- (arbitrary :: Gen [a])
+    return $ fromList n l
+
+instance Show (Int -> Ordering) where
+  show _ = "unshowable"
+
+-- We use @Ordering@ just because it's simple
+vecTests :: IO TestTree
+vecTests = testGroup "Vector" <$> return
+  [ testProperty "reverse100" $
+      \n v -> fromList (n :: NatRepr 100) (v :: [Ordering]) ==
+              (reverse <$> (reverse <$> (fromList n v)))
+  , testProperty "reverseSingleton" $
+      \n v -> fromList (n :: NatRepr 1) (v :: [Ordering]) ==
+              (reverse <$> (fromList n v))
+  , testProperty "split-join" $
+      \n w v -> (v :: Maybe (Vector (5 * 5) Ordering)) ==
+                (join (n :: NatRepr 5) . split n (w :: NatRepr 5) <$> v)
+  -- @cons@ is the same for vectors or lists
+  , testProperty "cons" $
+      \n v x -> (cons x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==
+                (fromList (incNat n) (x:v))
+  -- @snoc@ is like appending to a list
+  , testProperty "snoc" $
+      \n v x -> (flip snoc x <$> fromList (n :: NatRepr 20) (v :: [Ordering])) ==
+                (fromList (incNat n) (v ++ [x]))
+  -- @generate@ is like mapping a function over indices
+  , testProperty "generate" $
+      \n f -> Just (generate (n :: NatRepr 55) ((f :: Int -> Ordering) . widthVal)) ==
+              (fromList (incNat n) (map f [0..widthVal n]) :: Maybe (Vector 56 Ordering))
+  ]
diff --git a/submodules/parameterized-utils/test/UnitTest.hs b/submodules/parameterized-utils/test/UnitTest.hs
--- a/submodules/parameterized-utils/test/UnitTest.hs
+++ b/submodules/parameterized-utils/test/UnitTest.hs
@@ -4,6 +4,7 @@
 
 import qualified Test.Context
 import qualified Test.NatRepr
+import qualified Test.Vector
 
 main :: IO ()
 main = tests >>= defaultMainWithIngredients ingrs
@@ -19,4 +20,5 @@
 tests = testGroup "ParameterizedUtils" <$> sequence
   [ Test.Context.contextTests
   , Test.NatRepr.natTests
+  , Test.Vector.vecTests
   ]