diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/rv.cabal b/rv.cabal
--- a/rv.cabal
+++ b/rv.cabal
@@ -1,5 +1,5 @@
 name:                rv
-version:             0.0.0.0
+version:             0.0.1.0
 synopsis:            RISC-V
 -- description:
 license:             BSD3
@@ -13,11 +13,15 @@
 cabal-version:       >=1.10
 
 library
-  hs-source-dirs:      .
-  exposed-modules:     
-  build-depends:       base >= 4.7 && < 5
+  hs-source-dirs:      src
+  exposed-modules:     Data.RiscV.Reg
+                     , Data.RiscV.I
+  build-depends:       Fin
+                     , base >= 4.7 && < 5
                      , base-unicode-symbols
+                     , peano
                      , util
+                     , word
   default-language:    Haskell2010
   default-extensions:  UnicodeSyntax
                      , LambdaCase
diff --git a/src/Data/RiscV/I.hs b/src/Data/RiscV/I.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/RiscV/I.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Data.RiscV.I where
+
+import Prelude hiding (Word)
+import Data.Fin (Fin)
+import Data.Functor.Const
+import Data.Peano
+import Data.Word.General
+
+import Data.RiscV.Reg
+
+data Instruction
+  = LUI Reg Word20
+  | AUIPC Reg Word20
+  | JAL Reg Word20
+  | JALR Reg Reg Word12
+  | RegImmed IMinor Reg Reg Word12
+  | RegReg IOp Reg Reg Reg
+  | Branch BranchCmp Reg Reg Word12
+  | Load Reg LogNumBytes Signedness
+  | Stor Reg LogNumBytes
+  | Fence FenceSpec FenceSpec
+  | IFence
+  | Trap Bool
+  | CsrOp CsrOp Reg Reg Csr
+  | CsrOpI CsrOp Reg Word5 Csr
+
+data BranchCmp = EQ | NE | LT | LTU | GE | GEU
+  deriving (Eq, Show, Enum)
+
+newtype LogNumBytes = LogNumBytes (Fin (Succ (Succ (Succ (Succ Zero)))))
+  deriving (Eq, Ord, Show, Enum)
+
+data IOp = ∀ op . IOp (Const (ISubminor op) op)
+
+data IMinor = Add | Slt | Sltu | Xor | Or | And | Shl | Shr
+  deriving (Eq, Show, Enum)
+
+type family ISubminor (op :: IMinor) where
+    ISubminor Add = Signedness
+    ISubminor Shr = Signedness
+    ISubminor _ = ()
+
+newtype Signedness = Signedness Bool
+  deriving (Eq)
+
+data FenceSpec = FenceSpec
+  { fenceI, fenceO, fenceR, fenceW :: Bool }
+  deriving (Eq, Show)
+
+newtype Csr = Csr Word12
+  deriving (Eq, Ord)
+
+data CsrOp = RW | RS | RC
+  deriving (Eq, Show, Enum)
+
+type Word5  = Word (Succ (Succ (Succ (Succ (Succ Zero)))))
+type Word12 = Word (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))
+type Word20 = Word (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))
diff --git a/src/Data/RiscV/Reg.hs b/src/Data/RiscV/Reg.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/RiscV/Reg.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DataKinds #-}
+
+module Data.RiscV.Reg where
+
+import Prelude hiding (Word)
+import Data.Peano
+import Data.Word.General
+
+newtype Reg = Reg (Word (Succ (Succ (Succ (Succ (Succ Zero))))))
+  deriving (Eq, Ord)