diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,8 +1,40 @@
 # Changelog for `cuddle`
 
-## 1.1.2.0
+## 1.2.0.0
 
+* Add `Pretty` instance for `PTerm` 
+* Replace `ValidationResult` with `Evidenced ValidationTrace`
+* Move `ValidatorStageSimple` and `showSimple` to `Codec.CBOR.Cuddle.CBOR.Validator.Trace`
+* Add `Codec.CBOR.Cuddle.CBOR.Validator.Trace`
+* Add `--no-fold-valid` and `--format` options to `validate-cbor`
+* Changed `--rule` to a required argument in the `validate-cbor` subcommand
 * Export `Type0`
+* Removed `Codec.CBOR.Cuddle.Huddle.HuddleM`
+* Add `format-cbor` subcommand
+* Changed `--cbor` option of `validate` to a proper argument
+* Added `binary` and `hex` output formats. Providing an output file argument to 
+  `gen` no longer affects the output format.
+* Add `format-cbor` subcommand
+* Changed `--cbor` option of `validate` to a proper argument
+* Added `binary` and `hex` output formats. Providing an output file argument to 
+  `gen` no longer affects the output format.
+* Add `seed` and `size` options to `generate` subcommand
+* Replace `generateCBORTerm` with `generateFromName`
+* Remove `generateCBORTerm'`
+* Change the type of `withGenerator` and `CBORGenerator`
+* Change `--rule` option of `gen` to an argument
+* Add `withValidator`
+* Add `showSimple`, `ValidatorStageSimple`
+* Add `CBORValidator`, `CustomValidatorResult`, `HasValidator`
+* Add custom validator field to `XRule CTreePhase`
+* Added index type parameter to `CDDLResult`, `CBORTermResult`, `AMatchedItem`, `ANonMatchedItem`
+* Remove `CDDL` and `Rule` type synonyms from `Codec.CBOR.Cuddle.CBOR.Validator`
+* Remove `CBORTermResult`, `CDDLResult`, `AMatchedItem`, `ANonMatchedItem`, `CustomValidatorResult`
+* Add `--negative` option to `gen` for generating negative examples
+* `CBORGenerator` now uses `AntiGen` instead of `Gen`
+* Add `withAntiGen`
+* Add `GenPhase`
+* Add `MonoSimple`
 
 ## 1.1.1.0
 
diff --git a/bin/Main.hs b/bin/Main.hs
--- a/bin/Main.hs
+++ b/bin/Main.hs
@@ -1,26 +1,45 @@
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Main (main) where
 
-import Codec.CBOR.Cuddle.CBOR.Gen (generateCBORTerm)
+import Codec.CBOR.Cuddle.CBOR.Gen (generateFromName)
 import Codec.CBOR.Cuddle.CBOR.Validator
-import Codec.CBOR.Cuddle.CDDL (Name (..), fromRules, sortCDDL)
+import Codec.CBOR.Cuddle.CBOR.Validator.Trace (
+  Evidenced (..),
+  SValidity (..),
+  TraceOptions (..),
+  prettyValidationTrace,
+ )
+import Codec.CBOR.Cuddle.CDDL (CDDL, Name (..), fromRules, sortCDDL)
 import Codec.CBOR.Cuddle.CDDL.CTree (CTreeRoot)
 import Codec.CBOR.Cuddle.CDDL.Postlude (appendPostlude)
 import Codec.CBOR.Cuddle.CDDL.Resolve (
   fullResolveCDDL,
  )
 import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..), mapCDDLDropExt)
-import Codec.CBOR.Cuddle.Parser (pCDDL)
+import Codec.CBOR.Cuddle.Parser (ParserStage, pCDDL)
 import Codec.CBOR.Cuddle.Pretty (PrettyStage)
 import Codec.CBOR.FlatTerm (toFlatTerm)
 import Codec.CBOR.Pretty (prettyHexEnc)
-import Codec.CBOR.Term (encodeTerm)
+import Codec.CBOR.Read (deserialiseFromBytes)
+import Codec.CBOR.Term (Term, decodeTerm, encodeTerm)
 import Codec.CBOR.Write (toStrictByteString)
+import Control.Monad (unless)
+import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.ByteString.Base16 qualified as Base16
 import Data.ByteString.Char8 qualified as BSC
+import Data.ByteString.Lazy qualified as LBS
+import Data.Char (isSpace)
+import Data.IORef (newIORef)
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
 import Data.Text qualified as T
+import Data.Text.Encoding (encodeUtf8)
 import Data.Text.IO qualified as T
 import Options.Applicative
 import Prettyprinter (
@@ -29,20 +48,26 @@
   Pretty (pretty),
   defaultLayoutOptions,
   layoutPretty,
+  removeTrailingWhitespace,
  )
+import Prettyprinter.Render.Terminal qualified as Ansi
 import Prettyprinter.Render.Text qualified as PT
 import System.Exit (exitFailure, exitSuccess)
 import System.IO (hPutStrLn, stderr)
-import System.Random (getStdGen)
+import System.Random (newStdGen)
+import System.Random.Stateful (IOGenM (..), Uniform (..))
+import Test.AntiGen (zapAntiGen)
+import Test.QuickCheck (Gen)
+import Test.QuickCheck.Gen (Gen (..))
+import Test.QuickCheck.Random (mkQCGen)
 import Text.Megaparsec (ParseErrorBundle, Parsec, errorBundlePretty, runParser)
 
-data Opts = Opts Command String
-
 data Command
-  = Format FormatOpts
-  | Validate ValidateOpts
-  | GenerateCBOR GenOpts
-  | ValidateCBOR ValidateCBOROpts
+  = Format FormatOpts FilePath
+  | Validate ValidateOpts FilePath
+  | GenerateCBOR GenOpts FilePath
+  | ValidateCBOR ValidateCBOROpts FilePath
+  | FormatCBOR FormatCBOROpts FilePath
 
 newtype ValidateOpts = ValidateOpts {vNoPrelude :: Bool}
 
@@ -56,41 +81,49 @@
 
 -- | Various formats for outputtting CBOR
 data CBOROutputFormat
-  = AsCBOR
-  | AsPrettyCBOR
+  = AsBinary
+  | AsHex
+  | AsDiagnostic
   | AsTerm
   | AsFlatTerm
 
+outputFormatOptions :: Map String CBOROutputFormat
+outputFormatOptions =
+  Map.fromList
+    [ ("binary", AsBinary)
+    , ("hex", AsHex)
+    , ("pretty", AsDiagnostic)
+    , ("diagnostic", AsDiagnostic)
+    , ("term", AsTerm)
+    , ("flat", AsFlatTerm)
+    ]
+
 pCBOROutputFormat :: ReadM CBOROutputFormat
-pCBOROutputFormat = eitherReader $ \case
-  "cbor" -> Right AsCBOR
-  "pretty" -> Right AsPrettyCBOR
-  "term" -> Right AsTerm
-  "flat" -> Right AsFlatTerm
-  s -> Left s
+pCBOROutputFormat = eitherReader $ \k ->
+  case Map.lookup k outputFormatOptions of
+    Just x -> Right x
+    Nothing -> Left k
 
 data GenOpts = GenOpts
-  { itemName :: T.Text
-  , outputFormat :: CBOROutputFormat
+  { outputFormat :: CBOROutputFormat
   , outputTo :: Maybe String
   , gNoPrelude :: Bool
+  , goSeed :: Maybe Int
+  , goSize :: Int
+  , goNegative :: Bool
+  , itemName :: T.Text
   }
 
 pGenOpts :: Parser GenOpts
 pGenOpts =
   GenOpts
-    <$> strOption
-      ( long "rule"
-          <> short 'r'
-          <> metavar "RULE"
-          <> help "Name of the CDDL rule to generate a CBOR term for"
-      )
-    <*> option
+    <$> option
       pCBOROutputFormat
       ( long "format"
           <> short 'f'
           <> help "Output format"
-          <> value AsCBOR
+          <> value AsHex
+          <> completeWith (Map.keys outputFormatOptions)
       )
     <*> optional
       ( strOption
@@ -103,6 +136,26 @@
       ( long "no-prelude"
           <> help "Do not include the CDDL prelude."
       )
+    <*> optional
+      ( option auto $
+          long "seed"
+            <> short 's'
+            <> help "Generator seed"
+      )
+    <*> option
+      auto
+      ( long "size"
+          <> help "Generator size"
+          <> value 30
+      )
+    <*> switch
+      ( long "negative"
+          <> short 'n'
+          <> help "Generate a negative example"
+      )
+    <*> argument
+      str
+      (metavar "RULE" <> help "Name of the CDDL rule to generate a CBOR term for")
 
 newtype FormatOpts = FormatOpts
   {sort :: Bool}
@@ -116,132 +169,236 @@
       )
 
 data ValidateCBOROpts = ValidateCBOROpts
-  { vcItemName :: T.Text
+  { vcNoPrelude :: Bool
+  , vcInputFormat :: CBORInputFormat
+  , vcTraceOpts :: TraceOptions
+  , vcItemName :: T.Text
   , vcInput :: FilePath
-  , vcNoPrelude :: Bool
   }
 
+pTraceOpts :: Parser TraceOptions
+pTraceOpts =
+  TraceOptions
+    <$> flag
+      True
+      False
+      ( long "no-fold-valid"
+          <> help "Do not squash valid elements in lists/maps when printing validation trace"
+      )
+
 pValidateCBOROpts :: Parser ValidateCBOROpts
 pValidateCBOROpts =
   ValidateCBOROpts
-    <$> strOption
-      ( long "rule"
-          <> short 'r'
-          <> metavar "RULE"
+    <$> switch
+      ( long "no-prelude"
+          <> help "Do not include the CDDL prelude."
+      )
+    <*> option
+      pCBORInputFormat
+      ( long "format"
+          <> short 'f'
+          <> help "Output format"
+          <> completeWith (Map.keys inputFormatOptions)
+      )
+    <*> pTraceOpts
+    <*> argument
+      str
+      ( metavar "RULE"
           <> help "Name of the CDDL rule to validate this file with"
       )
-    <*> strOption
-      ( long "cbor"
-          <> short 'c'
-          <> help "CBOR file"
+    <*> argument str (metavar "CBOR_FILE")
+
+data CBORInputFormat
+  = FromHex
+  | FromBinary
+
+inputFormatOptions :: Map String CBORInputFormat
+inputFormatOptions =
+  Map.fromList
+    [ ("hex", FromHex)
+    , ("binary", FromBinary)
+    ]
+
+data FormatCBOROpts = FormatCBOROpts
+  { dcInputFormat :: CBORInputFormat
+  , dcOutputFormat :: CBOROutputFormat
+  , dcOutputFile :: Maybe FilePath
+  }
+
+pCBORInputFormat :: ReadM CBORInputFormat
+pCBORInputFormat = eitherReader $ \k -> case Map.lookup k inputFormatOptions of
+  Just x -> Right x
+  Nothing -> Left k
+
+pFormatCBOROpts :: Parser FormatCBOROpts
+pFormatCBOROpts =
+  FormatCBOROpts
+    <$> option
+      pCBORInputFormat
+      ( long "fin"
+          <> help "Input format"
+          <> value FromBinary
+          <> completeWith (Map.keys inputFormatOptions)
       )
-    <*> switch
-      ( long "no-prelude"
-          <> help "Do not include the CDDL prelude."
+    <*> option
+      pCBOROutputFormat
+      ( long "fout"
+          <> help "Output format"
+          <> value AsDiagnostic
+          <> completeWith (Map.keys outputFormatOptions)
       )
+    <*> optional
+      ( strOption
+          ( long "out-file"
+              <> short 'o'
+              <> help "Write to"
+          )
+      )
 
-opts :: Parser Opts
-opts =
-  Opts
-    <$> subparser
-      ( command
-          "format"
+pCommand :: Parser Command
+pCommand =
+  subparser
+    ( command
+        "format"
+        ( info
+            (Format <$> pFormatOpts <*> argument str (metavar "CDDL_FILE") <**> helper)
+            (progDesc "Format the provided CDDL file")
+        )
+        <> command
+          "validate"
           ( info
-              (Format <$> pFormatOpts <**> helper)
-              (progDesc "Format the provided CDDL file")
+              (Validate <$> pValidateOpts <*> argument str (metavar "CDDL_FILE") <**> helper)
+              (progDesc "Validate the provided CDDL file")
           )
-          <> command
-            "validate"
-            ( info
-                (Validate <$> pValidateOpts <**> helper)
-                (progDesc "Validate the provided CDDL file")
-            )
-          <> command
-            "gen"
-            ( info
-                (GenerateCBOR <$> pGenOpts <**> helper)
-                (progDesc "Generate a CBOR term matching the schema")
-            )
-          <> command
-            "validate-cbor"
-            ( info
-                (ValidateCBOR <$> pValidateCBOROpts <**> helper)
-                (progDesc "Validate a CBOR file against a schema")
-            )
-      )
-    <*> argument str (metavar "CDDL_FILE")
+        <> command
+          "gen"
+          ( info
+              (GenerateCBOR <$> pGenOpts <*> argument str (metavar "CDDL_FILE") <**> helper)
+              (progDesc "Generate a CBOR term matching the schema")
+          )
+        <> command
+          "validate-cbor"
+          ( info
+              (ValidateCBOR <$> pValidateCBOROpts <*> argument str (metavar "CDDL_FILE") <**> helper)
+              (progDesc "Validate a CBOR file against a schema")
+          )
+        <> command
+          "format-cbor"
+          ( info
+              (FormatCBOR <$> pFormatCBOROpts <*> argument str (metavar "CBOR_FILE") <**> helper)
+              (progDesc "Output a CBOR binary in diagnostic formatting")
+          )
+    )
 
 main :: IO ()
 main = do
   options <-
     execParser $
       info
-        (opts <**> helper)
+        (pCommand <**> helper)
         ( fullDesc
             <> progDesc "Manipulate CDDL files"
             <> header "cuddle"
         )
   run options
 
-run :: Opts -> IO ()
-run (Opts cmd cddlFile) = do
+tryParseFromFile :: FilePath -> IO (CDDL ParserStage)
+tryParseFromFile cddlFile =
   parseFromFile pCDDL cddlFile >>= \case
     Left err -> do
       putStrLnErr $ errorBundlePretty err
       exitFailure
-    Right res ->
-      case cmd of
-        Format fOpts ->
-          let
-            defs
-              | sort fOpts = fromRules $ sortCDDL res
-              | otherwise = res
-            layoutOptions = defaultLayoutOptions {layoutPageWidth = AvailablePerLine 80 1}
-            formattedText =
-              PT.renderStrict . layoutPretty layoutOptions . pretty $
-                mapIndex @_ @_ @PrettyStage defs
-            strippedText = T.unlines . fmap (T.dropWhileEnd (== ' ')) $ T.lines formattedText
-           in
-            T.putStr strippedText
-        Validate vOpts ->
-          let
-            cddl
-              | vNoPrelude vOpts = res
-              | otherwise = appendPostlude res
-           in
-            case fullResolveCDDL $ mapCDDLDropExt cddl of
-              Left err -> putStrLnErr (show err) >> exitFailure
-              Right _ -> exitSuccess
-        GenerateCBOR gOpts ->
-          let
-            cddl
-              | gNoPrelude gOpts = res
-              | otherwise = appendPostlude res
-           in
-            case fullResolveCDDL $ mapCDDLDropExt cddl of
-              Left err -> putStrLnErr (show err) >> exitFailure
-              Right mt -> do
-                stdGen <- getStdGen
-                let term = generateCBORTerm mt (Name $ itemName gOpts) stdGen
-                 in case outputFormat gOpts of
-                      AsTerm -> print term
-                      AsFlatTerm -> print $ toFlatTerm (encodeTerm term)
-                      AsCBOR -> case outputTo gOpts of
-                        Nothing -> BSC.putStrLn . Base16.encode . toStrictByteString $ encodeTerm term
-                        Just out -> BSC.writeFile out $ toStrictByteString $ encodeTerm term
-                      AsPrettyCBOR -> putStrLn . prettyHexEnc $ encodeTerm term
-        ValidateCBOR vcOpts ->
-          let
-            cddl
-              | vcNoPrelude vcOpts = res
-              | otherwise = res
-           in
-            case fullResolveCDDL $ mapCDDLDropExt cddl of
-              Left err -> putStrLnErr (show err) >> exitFailure
-              Right mt -> do
-                cbor <- BSC.readFile (vcInput vcOpts)
-                runValidateCBOR cbor (Name $ vcItemName vcOpts) (mapIndex mt)
+    Right res -> pure res
 
+formatTerm :: Term -> CBOROutputFormat -> ByteString
+formatTerm term = \case
+  AsTerm -> encodeUtf8 . T.pack $ show term
+  AsFlatTerm -> encodeUtf8 . T.pack . show . toFlatTerm $ encodeTerm term
+  AsBinary -> toStrictByteString $ encodeTerm term
+  AsHex -> Base16.encode . toStrictByteString $ encodeTerm term
+  AsDiagnostic -> encodeUtf8 . T.pack . prettyHexEnc $ encodeTerm term
+
+runGen :: Int -> Int -> Gen a -> a
+runGen seed size gen = unGen gen (mkQCGen seed) size
+
+tryReadCBOR :: CBORInputFormat -> FilePath -> IO ByteString
+tryReadCBOR format path = do
+  contentsRaw <- BS.readFile path
+  case format of
+    FromBinary -> pure contentsRaw
+    FromHex -> case Base16.decode . BSC.filter (not . isSpace) $ contentsRaw of
+      Right x -> pure x
+      Left err -> putStrLnErr (show err <> " when decoding hex input") >> exitFailure
+
+run :: Command -> IO ()
+run = \case
+  Format fOpts cddlFile -> do
+    res <- tryParseFromFile cddlFile
+    let
+      defs
+        | sort fOpts = fromRules $ sortCDDL res
+        | otherwise = res
+      layoutOptions = defaultLayoutOptions {layoutPageWidth = AvailablePerLine 80 1}
+      formattedText =
+        PT.renderStrict . removeTrailingWhitespace . layoutPretty layoutOptions . pretty $
+          mapIndex @_ @_ @PrettyStage defs
+    T.putStr formattedText
+  Validate vOpts cddlFile -> do
+    res <- tryParseFromFile cddlFile
+    let
+      cddl
+        | vNoPrelude vOpts = res
+        | otherwise = appendPostlude res
+    case fullResolveCDDL $ mapCDDLDropExt cddl of
+      Left err -> putStrLnErr (show err) >> exitFailure
+      Right _ -> exitSuccess
+  GenerateCBOR GenOpts {..} cddlFile -> do
+    res <- tryParseFromFile cddlFile
+    let
+      cddl
+        | gNoPrelude = res
+        | otherwise = appendPostlude res
+    case fullResolveCDDL $ mapCDDLDropExt cddl of
+      Left err -> putStrLnErr (show err) >> exitFailure
+      Right mt -> do
+        seed <- case goSeed of
+          Just s -> pure s
+          Nothing -> uniformM . IOGenM =<< newIORef =<< newStdGen
+        let
+          zapN
+            | goNegative = 1
+            | otherwise = 0
+          term = runGen seed goSize . zapAntiGen zapN $ generateFromName (mapIndex mt) (Name itemName)
+          formatted = formatTerm term outputFormat
+        case outputTo of
+          Just outputPath -> BS.writeFile outputPath formatted
+          Nothing -> BSC.putStrLn formatted
+        putStrLnErr $ "seed: " <> show seed
+  ValidateCBOR ValidateCBOROpts {..} cddlFile -> do
+    res <- tryParseFromFile cddlFile
+    let
+      cddl
+        | vcNoPrelude = res
+        | otherwise = appendPostlude res
+    case fullResolveCDDL $ mapCDDLDropExt cddl of
+      Left err -> putStrLnErr (show err) >> exitFailure
+      Right mt -> do
+        cbor <- BS.readFile vcInput
+        runValidateCBOR cbor (Name vcItemName) (mapIndex mt) vcTraceOpts
+  FormatCBOR FormatCBOROpts {..} cborFile -> do
+    contents <- tryReadCBOR dcInputFormat cborFile
+    term <- case deserialiseFromBytes decodeTerm (LBS.fromStrict contents) of
+      Right (leftover, term) -> do
+        unless (LBS.null leftover) . putStrLnErr $
+          "Warning: " <> show (LBS.length leftover) <> " leftover bytes after decoding"
+        pure term
+      Left err -> putStrLnErr (show err) >> exitFailure
+    let
+      formatted = formatTerm term dcOutputFormat
+    case dcOutputFile of
+      Just outputPath -> BS.writeFile outputPath formatted
+      Nothing -> BSC.putStrLn formatted
+
 putStrLnErr :: String -> IO ()
 putStrLnErr = hPutStrLn stderr
 
@@ -251,12 +408,17 @@
   IO (Either (ParseErrorBundle T.Text e) a)
 parseFromFile p file = runParser p file <$> T.readFile file
 
-runValidateCBOR :: BS.ByteString -> Name -> CTreeRoot ValidatorStage -> IO ()
-runValidateCBOR bs rule cddl =
+runValidateCBOR :: BS.ByteString -> Name -> CTreeRoot ValidatorStage -> TraceOptions -> IO ()
+runValidateCBOR bs rule cddl traceOpts =
   case validateCBOR bs rule cddl of
-    ok@(CBORTermResult _ (Valid _)) -> do
-      putStrLn $ "Valid " ++ show ok
-      exitSuccess
-    err -> do
-      hPutStrLn stderr $ "Invalid " ++ show err
-      exitFailure
+    Evidenced validity trc -> do
+      T.putStrLn . Ansi.renderStrict . layoutPretty defaultLayoutOptions $
+        prettyValidationTrace traceOpts trc
+      putStrLn mempty
+      case validity of
+        SValid -> do
+          putStrLn "Validation successful"
+          exitSuccess
+        SInvalid -> do
+          putStrLn "Validation failed"
+          exitFailure
diff --git a/cuddle.cabal b/cuddle.cabal
--- a/cuddle.cabal
+++ b/cuddle.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.4
 name: cuddle
-version: 1.1.2.0
+version: 1.2.0.0
 synopsis: CDDL Generator and test utilities
 description:
   Cuddle is a library for generating and manipulating [CDDL](https://datatracker.ietf.org/doc/html/rfc8610).
@@ -25,6 +25,7 @@
 data-files:
   example/cddl-files/*.cddl
   example/cddl-files/validator/negative/*.cddl
+  golden/*.txt
 
 source-repository head
   type: git
@@ -43,15 +44,16 @@
   exposed-modules:
     Codec.CBOR.Cuddle.CBOR.Gen
     Codec.CBOR.Cuddle.CBOR.Validator
+    Codec.CBOR.Cuddle.CBOR.Validator.Trace
     Codec.CBOR.Cuddle.CDDL
     Codec.CBOR.Cuddle.CDDL.CBORGenerator
     Codec.CBOR.Cuddle.CDDL.CTree
+    Codec.CBOR.Cuddle.CDDL.CTreePhase
     Codec.CBOR.Cuddle.CDDL.CtlOp
     Codec.CBOR.Cuddle.CDDL.Postlude
     Codec.CBOR.Cuddle.CDDL.Resolve
     Codec.CBOR.Cuddle.Comments
     Codec.CBOR.Cuddle.Huddle
-    Codec.CBOR.Cuddle.Huddle.HuddleM
     Codec.CBOR.Cuddle.IndexMappable
     Codec.CBOR.Cuddle.Parser
     Codec.CBOR.Cuddle.Parser.Lexer
@@ -60,6 +62,8 @@
     Codec.CBOR.Cuddle.Pretty.Utils
 
   build-depends:
+    QuickCheck >=2.14.3 && <2.18,
+    antigen >=0.3.1 && <0.4,
     base >=4.18 && <5,
     base16-bytestring >=1.0.2,
     boxes >=0.1.5,
@@ -70,6 +74,7 @@
     data-default-class >=0.2,
     foldable1-classes-compat >=0.1.1,
     generic-optics >=2.2.1,
+    half,
     hashable >=1.4,
     megaparsec >=9.5,
     mtl >=2.3.1,
@@ -78,6 +83,8 @@
     ordered-containers >=0.2.4,
     parser-combinators >=1.3,
     prettyprinter >=1.7.1,
+    prettyprinter-ansi-terminal,
+    quickcheck-transformer,
     random >=1.2,
     regex-tdfa >=1.3.2,
     scientific >=0.3.7,
@@ -104,6 +111,7 @@
   main-is: Main.hs
   build-depends:
     base,
+    bytestring,
     cuddle,
     megaparsec,
     prettyprinter,
@@ -116,15 +124,19 @@
   hs-source-dirs: ./bin/
   main-is: Main.hs
   build-depends:
+    QuickCheck,
+    antigen,
     base,
     base16-bytestring,
     bytestring,
     cborg,
+    containers,
     cuddle,
     megaparsec,
     mtl,
     optparse-applicative >=0.18,
     prettyprinter,
+    prettyprinter-ansi-terminal,
     random,
     text,
 
@@ -137,11 +149,13 @@
   other-modules:
     Paths_cuddle
     Test.Codec.CBOR.Cuddle.CDDL.Examples
+    Test.Codec.CBOR.Cuddle.CDDL.Examples.Huddle
     Test.Codec.CBOR.Cuddle.CDDL.Gen
     Test.Codec.CBOR.Cuddle.CDDL.GeneratorSpec
     Test.Codec.CBOR.Cuddle.CDDL.Parser
     Test.Codec.CBOR.Cuddle.CDDL.Pretty
     Test.Codec.CBOR.Cuddle.CDDL.Validator
+    Test.Codec.CBOR.Cuddle.CDDL.Validator.Golden
     Test.Codec.CBOR.Cuddle.Huddle
 
   type: exitcode-stdio-1.0
@@ -149,19 +163,24 @@
   main-is: Main.hs
   build-depends:
     HUnit >=1.6.2,
-    QuickCheck >=2.14,
+    QuickCheck,
+    antigen,
     base,
     bytestring,
     cborg,
     containers,
     cuddle,
     data-default-class,
+    filepath,
     generic-random,
     hspec >=2.11,
+    hspec-core,
+    hspec-golden,
     hspec-megaparsec >=2.2,
     megaparsec,
     pretty-simple,
     prettyprinter,
+    prettyprinter-ansi-terminal,
     random,
     string-qq >=0.0.6,
     text,
diff --git a/golden/choiceAlmostSecond.txt b/golden/choiceAlmostSecond.txt
new file mode 100644
--- /dev/null
+++ b/golden/choiceAlmostSecond.txt
@@ -0,0 +1,6 @@
+array
+└ app: 1
+  app: bool
+  failed to apply required rule:
+  └ failed to apply: 
+      6
diff --git a/golden/huddleRangeArrayTwoStrings.txt b/golden/huddleRangeArrayTwoStrings.txt
new file mode 100644
--- /dev/null
+++ b/golden/huddleRangeArrayTwoStrings.txt
@@ -0,0 +1,6 @@
+array
+└ app: int
+  app: int
+  app: text
+  app: text
+  not all required rules have been applied
diff --git a/golden/refTermTooLong.txt b/golden/refTermTooLong.txt
new file mode 100644
--- /dev/null
+++ b/golden/refTermTooLong.txt
@@ -0,0 +1,9 @@
+array
+└ app: 0
+  failed to apply required rule:
+  └ ref: bar
+    └ array
+      └ app: 1
+        app: 2
+        app: 3
+        leftover elements after all rules have been applied
diff --git a/src/Codec/CBOR/Cuddle/CBOR/Gen.hs b/src/Codec/CBOR/Cuddle/CBOR/Gen.hs
--- a/src/Codec/CBOR/Cuddle/CBOR/Gen.hs
+++ b/src/Codec/CBOR/Cuddle/CBOR/Gen.hs
@@ -14,66 +14,112 @@
 {-# LANGUAGE ViewPatterns #-}
 
 -- | Generate example CBOR given a CDDL specification
-module Codec.CBOR.Cuddle.CBOR.Gen (generateCBORTerm, generateCBORTerm') where
+module Codec.CBOR.Cuddle.CBOR.Gen (
+  generateFromName,
+  GenPhase,
+  GenSimple,
+  XXCTree (..),
+) where
 
 #if MIN_VERSION_random(1,3,0)
-import System.Random.Stateful (
-  SplitGen (..)
-  )
 #endif
-import Capability.Reader
-import Capability.Sink (HasSink)
-import Capability.Source (HasSource, MonadState (..))
-import Capability.State (HasState, get, modify)
 import Codec.CBOR.Cuddle.CDDL (
   Name (..),
   OccurrenceIndicator (..),
+  RangeBound (..),
   Value (..),
   ValueVariant (..),
  )
-import Codec.CBOR.Cuddle.CDDL.CBORGenerator (CBORGenerator (..), WrappedTerm (..))
+import Codec.CBOR.Cuddle.CDDL.CBORGenerator (
+  CBORGenerator (..),
+  GenPhase,
+  WrappedTerm (..),
+  XXCTree (..),
+ )
 import Codec.CBOR.Cuddle.CDDL.CTree (CTree (..), CTreeRoot (..), PTerm (..), foldCTree)
 import Codec.CBOR.Cuddle.CDDL.CTree qualified as CTree
 import Codec.CBOR.Cuddle.CDDL.CtlOp qualified as CtlOp
-import Codec.CBOR.Cuddle.CDDL.Resolve (MonoReferenced, XXCTree (..))
+import Codec.CBOR.Cuddle.CDDL.Resolve (XXCTree (..))
 import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..))
 import Codec.CBOR.Term (Term (..))
 import Codec.CBOR.Term qualified as CBOR
 import Codec.CBOR.Write qualified as CBOR
-import Control.Monad (join, replicateM, (<=<))
-import Control.Monad.Reader (Reader, runReader)
-import Control.Monad.State.Strict (StateT, runStateT)
-import Control.Monad.State.Strict qualified as MTL
-import Data.Bifunctor (second)
+import Control.Monad ((<=<))
 import Data.ByteString (ByteString)
+import Data.ByteString.Lazy qualified as BSL
+import Data.Char (chr)
+import Data.Containers.ListUtils (nubOrdOn)
 import Data.Functor ((<&>))
 import Data.List.NonEmpty qualified as NE
 import Data.Map.Strict qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.Text (Text)
 import Data.Text qualified as T
-import Data.Word (Word32)
+import Data.Text.Internal.Encoding.Utf8 (utf8Length)
+import Data.Text.Lazy qualified as LT
+import Data.Text.Lazy qualified as TL
+import Data.Text.Lazy.Builder (toLazyText)
+import Data.Text.Lazy.Builder qualified as LB
+import Data.Word (Word64, Word8)
 import GHC.Generics (Generic)
 import GHC.Stack (HasCallStack)
-import System.Random.Stateful (
-  Random,
-  RandomGen (..),
-  StateGenM (..),
-  UniformRange (uniformRM),
-  randomM,
-  uniformByteStringM,
+import Numeric.Half (Half (..), fromHalf)
+import System.Random.Stateful (Random, StatefulGen (..), runStateGen_, uniformByteStringM)
+import Test.AntiGen (
+  AntiGen,
+  antiChoose,
+  antiNonNegative,
+  antiNonPositive,
+  faultyNum,
+  runAntiGen,
+  (|!),
  )
+import Test.QuickCheck (
+  Arbitrary,
+  NonNegative (..),
+ )
+import Test.QuickCheck qualified as QC
+import Test.QuickCheck.Gen (Gen (..), getSize)
+import Test.QuickCheck.GenT (MonadGen (..), elements, listOf, oneof, suchThat, vectorOf)
 
-type data MonoDropGen
+-- TODO remove this once QuickCheck gets QC
+data QC = QC
 
-newtype instance XXCTree MonoDropGen = MDGRef Name
+instance StatefulGen QC Gen where
+  uniformWord32 QC = MkGen (\r _n -> runStateGen_ r uniformWord32)
+  uniformWord64 QC = MkGen (\r _n -> runStateGen_ r uniformWord64)
+#if MIN_VERSION_random(1,3,0)
+  uniformByteArrayM pinned sz QC = 
+    MkGen (\r _n -> runStateGen_ r (uniformByteArrayM pinned sz))
+#else
+  uniformShortByteString k QC =
+    MkGen (\r _n -> runStateGen_ r (uniformShortByteString k))
+#endif
+
+--------------------------------------------------------------------------------
+-- Lifted MonadGen utils
+--------------------------------------------------------------------------------
+
+arbitrary :: (Arbitrary a, MonadGen m) => m a
+arbitrary = liftGen QC.arbitrary
+
+scale :: MonadGen m => (Int -> Int) -> m a -> m a
+scale f m = sized $ \n -> resize (f n) m
+
+--------------------------------------------------------------------------------
+-- MonoSimple
+--------------------------------------------------------------------------------
+
+type data GenSimple
+
+newtype instance XXCTree GenSimple = GenSimpleRef Name
   deriving (Show)
 
-instance IndexMappable CTree MonoReferenced MonoDropGen where
+instance IndexMappable CTree GenPhase GenSimple where
   mapIndex = foldCTree mapExt mapIndex
     where
-      mapExt (MRuleRef n) = CTreeE $ MDGRef n
-      mapExt (MGenerator _ x) = mapIndex x
+      mapExt (GenRef n) = CTreeE $ GenSimpleRef n
+      mapExt (GenGenerator _ x) = mapIndex x
 
 --------------------------------------------------------------------------------
 -- Generator infrastructure
@@ -81,141 +127,103 @@
 
 -- | Generator context, parametrised over the type of the random seed
 newtype GenEnv = GenEnv
-  { cddl :: CTreeRoot MonoReferenced
-  }
-  deriving (Generic)
-
-data GenState g = GenState
-  { randomSeed :: g
-  -- ^ Actual seed
-  , depth :: Int
-  -- ^ Depth of the generator. This measures the number of references we
-  -- follow. As we go deeper into the tree, we try to reduce the likelihood of
-  -- following recursive paths, and generate shorter lists where allowed by
-  -- the occurrence bounds.
+  { cddl :: CTreeRoot GenPhase
   }
   deriving (Generic)
 
-instance RandomGen g => RandomGen (GenState g) where
-  genWord8 = withRandomSeed genWord8
-  genWord16 = withRandomSeed genWord16
-  genWord32 = withRandomSeed genWord32
-  genWord64 = withRandomSeed genWord64
-  split = splitGenStateWith split
-
-#if MIN_VERSION_random(1,3,0)
-instance SplitGen g => SplitGen (GenState g) where
-  splitGen = splitGenStateWith splitGen
-#endif
-
-splitGenStateWith :: (g -> (g, g)) -> GenState g -> (GenState g, GenState g)
-splitGenStateWith f s =
-  case f (randomSeed s) of
-    (gen', gen) -> (s {randomSeed = gen'}, s {randomSeed = gen})
-
-withRandomSeed :: (t -> (a, g)) -> GenState t -> (a, GenState g)
-withRandomSeed f s =
-  case f (randomSeed s) of
-    (r, gen) -> (r, s {randomSeed = gen})
-
-newtype M g a = M {runM :: StateT (GenState g) (Reader GenEnv) a}
-  deriving (Functor, Applicative, Monad, MTL.MonadState (GenState g))
-  deriving
-    (HasSource "randomSeed" g, HasSink "randomSeed" g, HasState "randomSeed" g)
-    via Field
-          "randomSeed"
-          ()
-          (MonadState (StateT (GenState g) (Reader GenEnv)))
-  deriving
-    (HasSource "depth" Int, HasSink "depth" Int, HasState "depth" Int)
-    via Field
-          "depth"
-          ()
-          (MonadState (StateT (GenState g) (Reader GenEnv)))
-  deriving
-    ( HasSource "cddl" (CTreeRoot MonoReferenced)
-    , HasReader "cddl" (CTreeRoot MonoReferenced)
-    )
-    via Field
-          "cddl"
-          ()
-          (Lift (StateT (GenState g) (MonadReader (Reader GenEnv))))
-
-runGen :: M g a -> GenEnv -> GenState g -> (a, GenState g)
-runGen m env st = runReader (runStateT (runM m) st) env
-
-evalGen :: M g a -> GenEnv -> GenState g -> a
-evalGen m env = fst . runGen m env
-
 --------------------------------------------------------------------------------
--- Wrappers around some Random function in Gen
+-- Postlude
 --------------------------------------------------------------------------------
 
-genUniformRM :: forall a g. (UniformRange a, RandomGen g) => (a, a) -> M g a
-genUniformRM r = uniformRM r (StateGenM @(GenState g))
+-- | Simple values that are either unassigned or don't have a specialized type already
+simple :: [Word8]
+simple =
+  -- TODO add the other values once they are supported
+  -- [0 .. 19] ++ [23] ++ [32 ..]
+  [23]
 
--- | Generate a random number in a given range, biased increasingly towards the
--- lower end as the depth parameter increases.
-genDepthBiasedRM ::
-  forall a g.
-  (Ord a, UniformRange a, RandomGen g) =>
-  (a, a) ->
-  M g a
-genDepthBiasedRM bounds = do
-  d <- get @"depth"
-  samples <- replicateM d (genUniformRM bounds)
-  pure $ minimum samples
+genHalf :: MonadGen m => m Float
+genHalf = do
+  half <- Half <$> arbitrary
+  if isInfinite half || isDenormalized half || isNaN half
+    then genHalf
+    else pure $ fromHalf half
 
--- | Generates a bool, increasingly likely to be 'False' as the depth increases.
-genDepthBiasedBool :: forall g. RandomGen g => M g Bool
-genDepthBiasedBool = do
-  d <- get @"depth"
-  and <$> replicateM d genRandomM
+genTerm :: AntiGen Term
+genTerm =
+  oneof
+    [ TInt <$> choose (minBound, maxBound)
+    , TInteger
+        <$> oneof
+          [ choose (toInteger (maxBound :: Int) + 1, toInteger (maxBound :: Word64))
+          , choose (negate (toInteger (maxBound :: Word64)), toInteger (minBound :: Int) - 1)
+          ]
+    , TBytes <$> (genNBytes . getNonNegative =<< arbitrary)
+    , TBytesI <$> (genNLazyBytes . getNonNegative =<< arbitrary)
+    , TString . T.pack <$> arbitrary
+    , TStringI . TL.pack <$> arbitrary
+    , TList <$> listOf smallerTerm
+    , TListI <$> listOf smallerTerm
+    , TMap <$> listOf ((,) <$> smallerTerm <*> smallerTerm)
+    , TMapI <$> listOf ((,) <$> smallerTerm <*> smallerTerm)
+    , TTagged <$> choose (6, maxBound :: Word64) <*> smallerTerm
+    , TBool <$> arbitrary
+    , pure TNull
+    , TSimple <$> elements simple
+    , THalf <$> genHalf
+    , TFloat <$> arbitrary
+    , TDouble <$> arbitrary
+    ]
+  where
+    smallerTerm :: AntiGen Term
+    smallerTerm = scale (`div` 5) genTerm
 
-genRandomM :: forall g a. (Random a, RandomGen g) => M g a
-genRandomM = randomM (StateGenM @(GenState g))
+genNBytes :: MonadGen m => Int -> m ByteString
+genNBytes n = liftGen (uniformByteStringM n QC)
 
-genBytes :: forall g. RandomGen g => Int -> M g ByteString
-genBytes n = uniformByteStringM n (StateGenM @(GenState g))
+genBytes :: MonadGen m => m ByteString
+genBytes = sized $ \sz -> do
+  numElems <- choose (0, sz)
+  genNBytes numElems
 
-genText :: forall g. RandomGen g => Int -> M g Text
-genText n = pure $ T.pack . take n . join $ repeat ['a' .. 'z']
+genNLazyBytes :: MonadGen m => Int -> m BSL.ByteString
+genNLazyBytes n = BSL.fromStrict <$> genNBytes n
 
---------------------------------------------------------------------------------
--- Postlude
---------------------------------------------------------------------------------
+genCharAtMostBytes :: MonadGen m => Int -> m Char
+genCharAtMostBytes 1 = chr <$> choose (0x00, 0x7F)
+genCharAtMostBytes 2 = chr <$> choose (0x00, 0x7FF)
+genCharAtMostBytes 3 = chr <$> oneof [choose (0x00, 0xD7FF), choose (0xE000, 0xFFFF)]
+genCharAtMostBytes n
+  | n <= 0 = error "expected positive number"
+  | otherwise = chr <$> oneof [choose (0x00, 0xD7FF), choose (0xE000, 0x10FFFF)]
 
+genNBytesText :: MonadGen m => Int -> m Text
+genNBytesText n = do
+  let
+    go m !acc
+      | m <= 0 = pure acc
+      | otherwise = do
+          c <- genCharAtMostBytes m
+          go (m - utf8Length c) (acc <> LB.singleton c)
+  builder <- go n mempty
+  pure . LT.toStrict $ toLazyText builder
+
+genText :: MonadGen m => m Text
+genText = sized $ \sz -> genNBytesText =<< choose (0, sz)
+
 -- | Primitive types defined by the CDDL specification, with their generators
-genPostlude :: RandomGen g => PTerm -> M g Term
+genPostlude :: PTerm -> AntiGen Term
 genPostlude pt = case pt of
-  PTBool ->
-    genRandomM
-      <&> TBool
-  PTUInt ->
-    genUniformRM (minBound :: Word32, maxBound)
-      <&> TInteger
-        . fromIntegral
-  PTNInt ->
-    genUniformRM
-      (minBound :: Int, 0)
-      <&> TInteger
-        . fromIntegral
-  PTInt ->
-    genUniformRM (minBound :: Int, maxBound)
-      <&> TInteger
-        . fromIntegral
-  PTHalf ->
-    genUniformRM (-65504, 65504)
-      <&> THalf
-  PTFloat ->
-    genRandomM
-      <&> TFloat
-  PTDouble ->
-    genRandomM
-      <&> TDouble
-  PTBytes -> TBytes <$> genBytes 30
-  PTText -> TString <$> genText 30
-  PTAny -> pure $ TString "Any"
+  PTBool -> TBool <$> arbitrary
+  PTUInt -> TInteger <$> antiNonNegative
+  PTNInt -> TInteger <$> antiNonPositive
+  PTInt -> TInteger . fromIntegral <$> choose (minBound :: Int, maxBound)
+  PTHalf -> THalf <$> choose (-65504, 65504)
+  PTFloat -> TFloat <$> arbitrary
+  PTDouble -> TDouble <$> arbitrary
+  PTBytes -> TBytes <$> genBytes
+  PTText -> TString <$> genText
+  PTAny -> genTerm
   PTNil -> pure TNull
   PTUndefined -> pure $ TSimple 23
 
@@ -246,18 +254,43 @@
 pairTermList (P x y : xs) = ((x, y) :) <$> pairTermList xs
 pairTermList _ = Nothing
 
-showDropGen :: CTree MonoReferenced -> String
-showDropGen = show . mapIndex @_ @_ @MonoDropGen
+showSimple :: CTree GenPhase -> String
+showSimple = show . mapIndex @_ @_ @GenSimple
 
+-- | Remove all negative generators from the `AntiGen`.
+dropNegativeGen :: AntiGen a -> AntiGen a
+dropNegativeGen = liftGen . runAntiGen
+
 --------------------------------------------------------------------------------
 -- Generator functions
 --------------------------------------------------------------------------------
 
-genForCTree :: (HasCallStack, RandomGen g) => CTree MonoReferenced -> M g WrappedTerm
-genForCTree (CTree.Literal v) = S <$> genValue v
-genForCTree (CTree.Postlude pt) = S <$> genPostlude pt
-genForCTree (CTree.Map nodes) = do
-  items <- pairTermList . flattenWrappedList <$> traverse genForCTree nodes
+genSized :: HasCallStack => Word64 -> CTree i -> AntiGen WrappedTerm
+genSized s target = do
+  case target of
+    CTree.Postlude PTText -> S . TString <$> genNBytesText (fromIntegral s)
+    CTree.Postlude PTBytes -> S . TBytes <$> genNBytes (fromIntegral s)
+    CTree.Postlude PTUInt -> S . TInteger <$> choose (0, 256 ^ s - 1)
+    _ -> error "Cannot apply size operator to target "
+
+range :: Enum a => RangeBound -> a -> a -> (a, a)
+range ClOpen x y = (x, pred y)
+range Closed x y = (x, y)
+
+genBetween :: (Integral a, Random a) => (a, a) -> AntiGen a
+genBetween rng = do
+  size <- liftGen getSize
+  let
+    sizeBounds :: Integral a => (a, a)
+    sizeBounds = (0, fromIntegral size)
+  antiChoose rng sizeBounds
+
+genForCTree ::
+  HasCallStack => CTreeRoot GenPhase -> CTree GenPhase -> AntiGen WrappedTerm
+genForCTree _ (CTree.Literal v) = pure . S $ valueToTerm v
+genForCTree _ (CTree.Postlude pt) = S <$> genPostlude pt
+genForCTree cddl (CTree.Map nodes) = do
+  items <- pairTermList . flattenWrappedList <$> traverse (genForCTree cddl) nodes
   case items of
     Just ts ->
       let
@@ -265,123 +298,116 @@
         -- Per RFC7049:
         -- >> A map that has duplicate keys may be well-formed, but it is not
         -- >> valid, and thus it causes indeterminate decoding
-        tsNodup = Map.toList $ Map.fromList ts
+        tsNodup = nubOrdOn fst ts
        in
         pure . S $ TMap tsNodup
     Nothing -> error "Single terms in map context"
-genForCTree (CTree.Array nodes) = do
-  items <- singleTermList . flattenWrappedList <$> traverse genForCTree nodes
+genForCTree cddl (CTree.Array nodes) = do
+  items <- singleTermList . flattenWrappedList <$> traverse (genForCTree cddl) nodes
   case items of
     Just ts -> pure . S $ TList ts
     Nothing -> error "Something weird happened which shouldn't be possible"
-genForCTree (CTree.Choice (NE.toList -> nodes)) = do
-  ix <- genUniformRM (0, length nodes - 1)
-  genForCTree $ nodes !! ix
-genForCTree (CTree.Group nodes) = G <$> traverse genForCTree nodes
-genForCTree (CTree.KV key value _cut) = do
-  kg <- genForCTree key
-  vg <- genForCTree value
+genForCTree cddl (CTree.Choice (NE.toList -> nodes)) = do
+  ix <- choose (0, length nodes - 1)
+  genForCTree cddl $ nodes !! ix
+genForCTree cddl (CTree.Group nodes) = G <$> traverse (genForCTree cddl) nodes
+genForCTree cddl (CTree.KV key value _cut) = do
+  kg <- genForCTree cddl key
+  vg <- genForCTree cddl value
   case (kg, vg) of
     (S k, S v) -> pure $ P k v
     _ ->
       error $
         "Non single-term generated outside of group context: "
-          <> showDropGen key
+          <> showSimple key
           <> " => "
-          <> showDropGen value
-genForCTree (CTree.Occur item occurs) =
-  applyOccurenceIndicator occurs (genForCTree item)
-genForCTree (CTree.Range from to _bounds) = do
-  -- TODO Handle bounds correctly
-  term1 <- genForCTree from
-  term2 <- genForCTree to
+          <> showSimple value
+genForCTree cddl (CTree.Occur item occurs) =
+  applyOccurenceIndicator occurs (genForCTree cddl item)
+genForCTree cddl (CTree.Range from to bounds) = do
+  term1 <- dropNegativeGen $ genForCTree cddl from
+  term2 <- dropNegativeGen $ genForCTree cddl to
   case (term1, term2) of
     (S (TInt a), S (TInt b))
-      | a <= b -> genUniformRM (a, b) <&> S . TInt
+      | a <= b -> genBetween (range bounds a b) <&> S . TInt
     (S (TInt a), S (TInteger b))
-      | fromIntegral a <= b -> genUniformRM (fromIntegral a, b) <&> S . TInteger
+      | fromIntegral a <= b ->
+          genBetween (range bounds (fromIntegral a) b) <&> S . TInteger
     (S (TInteger a), S (TInteger b))
-      | a <= b -> genUniformRM (a, b) <&> S . TInteger
+      | a <= b -> genBetween (range bounds a b) <&> S . TInteger
     (S (THalf a), S (THalf b))
-      | a <= b -> genUniformRM (a, b) <&> S . THalf
+      | a <= b -> choose (range bounds a b) <&> S . THalf
     (S (TFloat a), S (TFloat b))
-      | a <= b -> genUniformRM (a, b) <&> S . TFloat
+      | a <= b -> choose (range bounds a b) <&> S . TFloat
     (S (TDouble a), S (TDouble b))
-      | a <= b -> genUniformRM (a, b) <&> S . TDouble
+      | a <= b -> choose (range bounds a b) <&> S . TDouble
     (a, b) -> error $ "invalid range (a = " <> show a <> ", b = " <> show b <> ")"
-genForCTree (CTree.Control op target controller) = do
+genForCTree cddl (CTree.Control op target controller) = do
   resolvedController <- case controller of
-    CTreeE (MRuleRef n) -> resolveRef n
+    CTreeE (GenRef n) -> dropNegativeGen $ resolveRef cddl n
     x -> pure x
   case (op, resolvedController) of
     (CtlOp.Le, CTree.Literal (Value (VUInt n) _)) -> case target of
-      CTree.Postlude PTUInt -> S . TInteger <$> genUniformRM (0, fromIntegral n)
+      CTree.Postlude PTUInt -> S . TInteger <$> choose (0, fromIntegral n)
       _ -> error "Cannot apply le operator to target"
-    (CtlOp.Le, _) -> error $ "Invalid controller for .le operator: " <> showDropGen controller
+    (CtlOp.Le, _) -> error $ "Invalid controller for .le operator: " <> showSimple controller
     (CtlOp.Lt, CTree.Literal (Value (VUInt n) _)) -> case target of
-      CTree.Postlude PTUInt -> S . TInteger <$> genUniformRM (0, fromIntegral n - 1)
+      CTree.Postlude PTUInt -> S . TInteger <$> choose (0, fromIntegral n - 1)
       _ -> error "Cannot apply lt operator to target"
-    (CtlOp.Lt, _) -> error $ "Invalid controller for .lt operator: " <> showDropGen controller
-    (CtlOp.Size, CTree.Literal (Value (VUInt n) _)) -> case target of
-      CTree.Postlude PTText -> S . TString <$> genText (fromIntegral n)
-      CTree.Postlude PTBytes -> S . TBytes <$> genBytes (fromIntegral n)
-      CTree.Postlude PTUInt -> S . TInteger <$> genUniformRM (0, 2 ^ n - 1)
-      _ -> error "Cannot apply size operator to target "
+    (CtlOp.Lt, _) -> error $ "Invalid controller for .lt operator: " <> showSimple controller
+    (CtlOp.Size, CTree.Literal (Value (VUInt s) _)) -> do
+      s' <- pure s |! sized (\sz -> choose (0, fromIntegral sz) `suchThat` (/= s))
+      genSized s' target
     (CtlOp.Size, CTree.Range {CTree.from, CTree.to}) -> do
       case (from, to) of
-        (CTree.Literal (Value (VUInt f1) _), CTree.Literal (Value (VUInt t1) _)) -> case target of
-          CTree.Postlude PTText ->
-            genUniformRM (fromIntegral f1, fromIntegral t1)
-              >>= (fmap (S . TString) . genText)
-          CTree.Postlude PTBytes ->
-            genUniformRM (fromIntegral f1, fromIntegral t1)
-              >>= (fmap (S . TBytes) . genBytes)
-          CTree.Postlude PTUInt ->
-            S . TInteger
-              <$> genUniformRM (fromIntegral f1, fromIntegral t1)
-          _ -> error $ "Cannot apply size operator to target: " <> showDropGen target
+        (CTree.Literal (Value (VUInt f) _), CTree.Literal (Value (VUInt t) _)) -> do
+          s <- sized $ \sz ->
+            antiChoose
+              (fromIntegral f, fromIntegral t)
+              (0, max (succ t) $ fromIntegral sz)
+          genSized s target
         _ ->
           error $
             "Invalid controller for .size operator: "
-              <> showDropGen controller
+              <> showSimple controller
     (CtlOp.Size, _) ->
       error $
         "Invalid controller for .size operator: "
-          <> showDropGen controller
+          <> showSimple controller
     (CtlOp.Cbor, _) -> do
-      enc <- genForCTree controller
+      enc <- genForCTree cddl controller
       case enc of
         S x -> pure . S . TBytes . CBOR.toStrictByteString $ CBOR.encodeTerm x
         _ -> error "Controller does not correspond to a single term"
-    _ -> genForCTree target
-genForCTree (CTree.Enum tree) = do
+    (c, _) -> error $ "Controller not yet implemented: " <> show c
+genForCTree cddl (CTree.Enum tree) = do
   case tree of
     CTree.Group trees -> do
-      ix <- genUniformRM (0, length trees - 1)
-      genForCTree $ trees !! ix
+      ix <- choose (0, length trees - 1)
+      genForCTree cddl $ trees !! ix
     _ -> error "Attempt to form an enum from something other than a group"
-genForCTree (CTree.Unwrap node) = genForCTree node
-genForCTree (CTree.Tag tag node) = do
-  enc <- genForCTree node
+genForCTree cddl (CTree.Unwrap node) = genForCTree cddl node
+genForCTree cddl (CTree.Tag t node) = do
+  tag <- faultyNum t
+  enc <- genForCTree cddl node
   case enc of
     S x -> pure $ S $ TTagged tag x
     _ -> error "Tag controller does not correspond to a single term"
-genForCTree (CTree.CTreeE (MRuleRef n)) = genForNode n
-genForCTree (CTree.CTreeE (MGenerator (CBORGenerator gen) _)) = gen StateGenM
+genForCTree cddl (CTree.CTreeE (GenRef n)) = genForNode cddl n
+genForCTree cddl (CTree.CTreeE (GenGenerator (CBORGenerator gen) _)) = gen cddl
 
-genForNode :: (HasCallStack, RandomGen g) => Name -> M g WrappedTerm
-genForNode = genForCTree <=< resolveRef
+genForNode :: HasCallStack => CTreeRoot GenPhase -> Name -> AntiGen WrappedTerm
+genForNode cddl = genForCTree cddl <=< resolveRef cddl
 
 -- | Take a reference and resolve it to the relevant Tree, following multiple
 -- links if necessary.
-resolveRef :: RandomGen g => Name -> M g (CTree MonoReferenced)
-resolveRef n = do
-  (CTreeRoot cddl) <- ask @"cddl"
-  -- Since we follow a reference, we increase the 'depth' of the gen monad.
-  modify @"depth" (+ 1)
-  case Map.lookup n cddl of
-    Nothing -> error $ "Unbound reference: " <> show n
-    Just val -> pure val
+resolveRef :: MonadGen m => CTreeRoot GenPhase -> Name -> m (CTree GenPhase)
+resolveRef (CTreeRoot cddl) n = do
+  -- Since we follow a reference, we decrease the 'size' of the Gen monad.
+  scale (\x -> max 0 $ x - 1) $
+    case Map.lookup n cddl of
+      Nothing -> error $ "Unbound reference: " <> show n
+      Just val -> pure val
 
 -- | Generate a CBOR Term corresponding to a top-level name.
 --
@@ -391,13 +417,12 @@
 -- This will throw an error if the generated item does not correspond to a
 -- single CBOR term (e.g. if the name resolves to a group, which cannot be
 -- generated outside a context).
-genForName :: (HasCallStack, RandomGen g) => Name -> M g Term
-genForName n = do
-  (CTreeRoot cddl) <- ask @"cddl"
+generateFromName :: HasCallStack => CTreeRoot GenPhase -> Name -> AntiGen Term
+generateFromName root@(CTreeRoot cddl) n = do
   case Map.lookup n cddl of
     Nothing -> error $ "Unbound reference: " <> show n
     Just val ->
-      genForCTree val >>= \case
+      genForCTree root val >>= \case
         S x -> pure x
         _ ->
           error $
@@ -405,55 +430,54 @@
               <> show n
               <> ", but it does not correspond to a single term."
 
+sizeBiasedBool :: MonadGen m => m Bool
+sizeBiasedBool = sized $ \sz -> (> 1) <$> choose (0, sz)
+
+listOfScaled :: MonadGen m => m a -> m [a]
+listOfScaled g = sized $ \sz -> do
+  i <- choose (0, sz)
+  vectorOf i $ scale (`div` (i + 1)) g
+
+listOfScaled1 :: AntiGen a -> AntiGen [a]
+listOfScaled1 g = sized $ \sz -> do
+  i <- choose (1, max sz 1) |! pure 0
+  vectorOf i $ scale (`div` (i + 1)) g
+
 -- | Apply an occurence indicator to a group entry
 applyOccurenceIndicator ::
-  RandomGen g =>
   OccurrenceIndicator ->
-  M g WrappedTerm ->
-  M g WrappedTerm
+  AntiGen WrappedTerm ->
+  AntiGen WrappedTerm
 applyOccurenceIndicator OIOptional oldGen =
-  genDepthBiasedBool >>= \case
+  sizeBiasedBool >>= \case
     False -> pure $ G mempty
     True -> oldGen
 applyOccurenceIndicator OIZeroOrMore oldGen =
-  genDepthBiasedRM (0 :: Int, 10) >>= \i ->
-    G <$> replicateM i oldGen
+  G <$> listOfScaled oldGen
 applyOccurenceIndicator OIOneOrMore oldGen =
-  genDepthBiasedRM (1 :: Int, 10) >>= \i ->
-    G <$> replicateM i oldGen
+  G <$> listOfScaled1 oldGen
 applyOccurenceIndicator (OIBounded mlb mub) oldGen =
-  genDepthBiasedRM (lo, fromMaybe (max 10 lo) mub)
-    >>= \i -> G <$> replicateM (fromIntegral i) oldGen
-  where
-    lo = fromMaybe 0 mlb
-
-genValue :: RandomGen g => Value -> M g Term
-genValue (Value x _) = genValueVariant x
-
-genValueVariant :: RandomGen g => ValueVariant -> M g Term
-genValueVariant (VUInt i) = pure . TInt $ fromIntegral i
-genValueVariant (VNInt i) = pure . TInt $ fromIntegral (-i)
-genValueVariant (VBignum i) = pure $ TInteger i
-genValueVariant (VFloat16 i) = pure . THalf $ i
-genValueVariant (VFloat32 i) = pure . TFloat $ i
-genValueVariant (VFloat64 i) = pure . TDouble $ i
-genValueVariant (VText t) = pure $ TString t
-genValueVariant (VBytes b) = pure $ TBytes b
-genValueVariant (VBool b) = pure $ TBool b
-
---------------------------------------------------------------------------------
--- Generator functions
---------------------------------------------------------------------------------
+  sized $ \sz -> do
+    let
+      lb = fromMaybe 0 mlb
+      ub = fromMaybe (lb + fromIntegral sz) mub
+    i <- fromIntegral <$> genBetween (lb, ub)
+    G <$> vectorOf i (scale (`div` (i + 1)) oldGen)
 
-generateCBORTerm :: (HasCallStack, RandomGen g) => CTreeRoot MonoReferenced -> Name -> g -> Term
-generateCBORTerm cddl n stdGen =
-  let genEnv = GenEnv {cddl}
-      genState = GenState {randomSeed = stdGen, depth = 1}
-   in evalGen (genForName n) genEnv genState
+valueToTerm :: Value -> Term
+valueToTerm (Value x _) = valueVariantToTerm x
 
-generateCBORTerm' ::
-  (HasCallStack, RandomGen g) => CTreeRoot MonoReferenced -> Name -> g -> (Term, g)
-generateCBORTerm' cddl n stdGen =
-  let genEnv = GenEnv {cddl}
-      genState = GenState {randomSeed = stdGen, depth = 1}
-   in second randomSeed $ runGen (genForName n) genEnv genState
+valueVariantToTerm :: ValueVariant -> Term
+valueVariantToTerm (VUInt i)
+  | toInteger i <= toInteger (maxBound :: Int) = TInt (fromIntegral i)
+  | otherwise = TInteger (fromIntegral i)
+valueVariantToTerm (VNInt i)
+  | -toInteger i >= toInteger (minBound :: Int) = TInt (-fromIntegral i)
+  | otherwise = TInteger (-fromIntegral i)
+valueVariantToTerm (VBignum i) = TInteger i
+valueVariantToTerm (VFloat16 i) = THalf i
+valueVariantToTerm (VFloat32 i) = TFloat i
+valueVariantToTerm (VFloat64 i) = TDouble i
+valueVariantToTerm (VText t) = TString t
+valueVariantToTerm (VBytes b) = TBytes b
+valueVariantToTerm (VBool b) = TBool b
diff --git a/src/Codec/CBOR/Cuddle/CBOR/Validator.hs b/src/Codec/CBOR/Cuddle/CBOR/Validator.hs
--- a/src/Codec/CBOR/Cuddle/CBOR/Validator.hs
+++ b/src/Codec/CBOR/Cuddle/CBOR/Validator.hs
@@ -1,890 +1,997 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TypeData #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE ViewPatterns #-}
-
-module Codec.CBOR.Cuddle.CBOR.Validator (
-  validateCBOR,
-  isCBORTermResultValid,
-  CDDLResult (..),
-  CBORTermResult (..),
-  ValidatorStage,
-) where
-
-import Codec.CBOR.Cuddle.CDDL hiding (CDDL, Group, Rule)
-import Codec.CBOR.Cuddle.CDDL.CTree
-import Codec.CBOR.Cuddle.CDDL.CtlOp
-import Codec.CBOR.Cuddle.CDDL.Resolve (MonoReferenced, XXCTree (..))
-import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..))
-import Codec.CBOR.Read
-import Codec.CBOR.Term
-import Data.Bits hiding (And)
-import Data.ByteString qualified as BS
-import Data.ByteString.Lazy qualified as BSL
-import Data.IntSet qualified as IS
-import Data.List.NonEmpty qualified as NE
-import Data.Map.Strict qualified as Map
-import Data.Maybe
-import Data.Text qualified as T
-import Data.Text.Lazy qualified as TL
-import Data.Word
-import GHC.Float
-import GHC.Stack (HasCallStack)
-import Text.Regex.TDFA
-
-type data ValidatorStage
-
-data instance XTerm ValidatorStage = ValidatorXTerm
-  deriving (Show, Eq)
-
-newtype instance XXCTree ValidatorStage = VRuleRef Name
-  deriving (Show, Eq)
-
-instance IndexMappable CTreeRoot MonoReferenced ValidatorStage where
-  mapIndex (CTreeRoot m) = CTreeRoot $ mapIndex <$> m
-
-instance IndexMappable CTree MonoReferenced ValidatorStage where
-  mapIndex = foldCTree mapExt mapIndex
-    where
-      mapExt (MRuleRef n) = CTreeE $ VRuleRef n
-      mapExt (MGenerator _ x) = mapIndex x
-
-type CDDL = CTreeRoot ValidatorStage
-type Rule = CTree ValidatorStage
-
-data CBORTermResult = CBORTermResult
-  { ctrTerm :: Term
-  , ctrResult :: CDDLResult
-  }
-  deriving (Show, Eq)
-
-data CDDLResult
-  = -- | The rule was valid
-    Valid Rule
-  | -- | All alternatives failed
-    ChoiceFail
-      -- | Rule we are trying
-      Rule
-      -- | The alternatives that arise from said rule
-      (NE.NonEmpty Rule)
-      -- | For each alternative, the result
-      (NE.NonEmpty (Rule, CDDLResult))
-  | -- | All expansions failed
-    --
-    -- An expansion is: Given a CBOR @TList@ of @N@ elements, we will expand the
-    -- rules in a list spec to match the number of items in the list.
-    ListExpansionFail
-      -- | Rule we are trying
-      Rule
-      -- | List of expansions of rules
-      [[Rule]]
-      -- | For each expansion, for each of the rules in the expansion, the result
-      [[(Rule, CBORTermResult)]]
-  | -- | All expansions failed
-    --
-    -- An expansion is: Given a CBOR @TMap@ of @N@ elements, we will expand the
-    -- rules in a map spec to match the number of items in the map.
-    MapExpansionFail
-      -- | Rule we are trying
-      Rule
-      -- | List of expansions
-      [[Rule]]
-      -- | A list of matched items @(key, value, rule)@ and the unmatched item
-      [([AMatchedItem], ANonMatchedItem)]
-  | -- | The rule was valid but the control failed
-    InvalidControl
-      -- | Control we are trying
-      Rule
-      -- | If it is a .cbor, the result of the underlying validation
-      (Maybe CBORTermResult)
-  | InvalidRule Rule
-  | -- | A tagged was invalid
-    InvalidTagged
-      -- | Rule we are trying
-      Rule
-      -- | Either the tag is wrong, or the contents are wrong
-      (Either Word64 CBORTermResult)
-  | -- | The rule we are trying is not applicable to the CBOR term
-    UnapplicableRule
-      -- | Extra information
-      String
-      -- | Rule we are trying
-      Rule
-  deriving (Show, Eq)
-
-isCBORTermResultValid :: CBORTermResult -> Bool
-isCBORTermResultValid (CBORTermResult _ Valid {}) = True
-isCBORTermResultValid _ = False
-
-data ANonMatchedItem = ANonMatchedItem
-  { anmiKey :: Term
-  , anmiValue :: Term
-  , anmiResults :: [Either (Rule, CDDLResult) (Rule, CDDLResult, CDDLResult)]
-  -- ^ For all the tried rules, either the key failed or the key succeeded and
-  -- the value failed
-  }
-  deriving (Show, Eq)
-
-data AMatchedItem = AMatchedItem
-  { amiKey :: Term
-  , amiValue :: Term
-  , amiRule :: Rule
-  }
-  deriving (Show, Eq)
-
---------------------------------------------------------------------------------
--- Main entry point
-
-validateCBOR :: BS.ByteString -> Name -> CDDL -> CBORTermResult
-validateCBOR bs rule cddl@(CTreeRoot tree) =
-  case deserialiseFromBytes decodeTerm (BSL.fromStrict bs) of
-    Left e -> error $ show e
-    Right (rest, term)
-      | BSL.null rest -> validateTerm cddl term (tree Map.! rule)
-      | otherwise -> error $ "Leftover bytes in CBOR" <> show rest
-
---------------------------------------------------------------------------------
--- Terms
-
--- | Core function that validates a CBOR term to a particular rule of the CDDL
--- spec
-validateTerm :: CDDL -> Term -> Rule -> CBORTermResult
-validateTerm cddl term rule =
-  CBORTermResult term $ case term of
-    TInt i -> validateInteger cddl (fromIntegral i) rRule
-    TInteger i -> validateInteger cddl i rRule
-    TBytes b -> validateBytes cddl b rRule
-    TBytesI b -> validateBytes cddl (BSL.toStrict b) rRule
-    TString s -> validateText cddl s rRule
-    TStringI s -> validateText cddl (TL.toStrict s) rRule
-    TList ts -> validateList cddl ts rRule
-    TListI ts -> validateList cddl ts rRule
-    TMap ts -> validateMap cddl ts rRule
-    TMapI ts -> validateMap cddl ts rRule
-    TTagged w t -> validateTagged cddl w t rRule
-    TBool b -> validateBool cddl b rRule
-    TNull -> validateNull cddl rRule
-    TSimple s -> validateSimple cddl s rRule
-    THalf h -> validateHalf cddl h rRule
-    TFloat h -> validateFloat cddl h rRule
-    TDouble d -> validateDouble cddl d rRule
-  where
-    rRule = resolveIfRef cddl rule
-
---------------------------------------------------------------------------------
--- Ints and integers
-
--- | Validation of an Int or Integer. CBOR categorizes every integral in `TInt`
--- or `TInteger` but it can be the case that we are decoding something that is
--- expected to be a `Word64` even if we get a `TInt`.
---
--- > ghci> encodeWord64 15
--- > [TkInt 15]
--- > ghci> encodeWord64 maxBound
--- > [TkInteger 18446744073709551615]
---
--- For this reason, we cannot assume that bounds or literals are going to be
--- Ints, so we convert everything to Integer.
-validateInteger :: HasCallStack => CDDL -> Integer -> Rule -> CDDLResult
-validateInteger cddl i rule =
-  case resolveIfRef cddl rule of
-    -- echo "C24101" | xxd -r -p - example.cbor
-    -- echo "foo = int" > a.cddl
-    -- cddl a.cddl validate example.cbor
-    --
-    -- but
-    --
-    -- echo "C249010000000000000000"| xxd -r -p - example.cbor
-    -- echo "foo = int" > a.cddl
-    -- cddl a.cddl validate example.cbor
-    --
-    -- and they are both bigints?
-
-    -- a = any
-    Postlude PTAny -> Valid rule
-    -- a = int
-    Postlude PTInt -> Valid rule
-    -- a = uint
-    Postlude PTUInt -> check (i >= 0) rule
-    -- a = nint
-    Postlude PTNInt -> check (i <= 0) rule
-    -- a = x
-    Literal (Value (VUInt i') _) -> check (i == fromIntegral i') rule
-    -- a = -x
-    Literal (Value (VNInt i') _) -> check (-i == fromIntegral i') rule
-    -- a = <big number>
-    Literal (Value (VBignum i') _) -> check (i == i') rule
-    -- a = foo .ctrl bar
-    Control op tgt ctrl -> ctrlDispatch (validateInteger cddl i) op tgt ctrl (controlInteger cddl i) rule
-    -- a = foo / bar
-    Choice opts -> validateChoice (validateInteger cddl i) opts rule
-    -- a = x..y
-    Range low high bound ->
-      check
-        ( case (resolveIfRef cddl low, resolveIfRef cddl high) of
-            (Literal (Value (VUInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) -> n <= i && range bound i m
-            (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) -> -n <= i && range bound i m
-            (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VNInt (fromIntegral -> m)) _)) -> -n <= i && range bound i (-m)
-            (Literal (Value VUInt {} _), Literal (Value VNInt {} _)) -> False
-            (Literal (Value (VBignum n) _), Literal (Value (VUInt (fromIntegral -> m)) _)) -> n <= i && range bound i m
-            (Literal (Value (VBignum n) _), Literal (Value (VNInt (fromIntegral -> m)) _)) -> n <= i && range bound i (-m)
-            (Literal (Value (VUInt (fromIntegral -> n)) _), Literal (Value (VBignum m) _)) -> n <= i && range bound i m
-            (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VBignum m) _)) -> (-n) <= i && range bound i m
-            x -> error $ "Unable to validate range: " <> show x
-        )
-        rule
-    -- a = &(x, y, z)
-    Enum g ->
-      case resolveIfRef cddl g of
-        Group g' -> replaceRule (validateInteger cddl i (Choice (NE.fromList g'))) rule
-        _ -> error "Not yet implemented"
-    -- a = x: y
-    -- Note KV cannot appear on its own, but we will use this when validating
-    -- lists.
-    KV _ v _ -> replaceRule (validateInteger cddl i v) rule
-    Tag 2 x -> validateBigInt x
-    Tag 3 x -> validateBigInt x
-    _ -> UnapplicableRule "validateInteger" rule
-  where
-    validateBigInt x = case resolveIfRef cddl x of
-      Postlude PTBytes -> Valid rule
-      Control op tgt@(Postlude PTBytes) ctrl ->
-        ctrlDispatch (validateBytes cddl bs) op tgt ctrl (controlBytes cddl bs) rule
-        where
-          -- TODO figure out a way to turn Integer into bytes or figure out why
-          -- tagged bigints are decoded as integers in the first place
-          bs = mempty
-      e -> error $ "Not yet implemented" <> show e
-
--- | Controls for an Integer
-controlInteger ::
-  HasCallStack => CDDL -> Integer -> CtlOp -> Rule -> Either (Maybe CBORTermResult) ()
-controlInteger cddl i Size ctrl =
-  case resolveIfRef cddl ctrl of
-    Literal (Value (VUInt sz) _) ->
-      boolCtrl $ 0 <= i && i < 256 ^ sz
-    _ -> error "Not yet implemented"
-controlInteger cddl i Bits ctrl = do
-  let
-    indices = case resolveIfRef cddl ctrl of
-      Literal (Value (VUInt i') _) -> [i']
-      Choice nodes -> getIndicesOfChoice cddl nodes
-      Range ff tt incl -> getIndicesOfRange cddl ff tt incl
-      Enum g -> getIndicesOfEnum cddl g
-      _ -> error "Not yet implemented"
-  boolCtrl $ go (IS.fromList (map fromIntegral indices)) i 0
-  where
-    go _ 0 _ = True
-    go indices n idx =
-      let bitSet = testBit n 0
-          allowed = not bitSet || IS.member idx indices
-       in (allowed && go indices (shiftR n 1) (idx + 1))
-controlInteger cddl i Lt ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VUInt i') _) -> i < fromIntegral i'
-    Literal (Value (VNInt i') _) -> i < -fromIntegral i'
-    Literal (Value (VBignum i') _) -> i < i'
-    _ -> error "Not yet implemented"
-controlInteger cddl i Gt ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VUInt i') _) -> i > fromIntegral i'
-    Literal (Value (VNInt i') _) -> i > -fromIntegral i'
-    Literal (Value (VBignum i') _) -> i > i'
-    _ -> error "Not yet implemented"
-controlInteger cddl i Le ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VUInt i') _) -> i <= fromIntegral i'
-    Literal (Value (VNInt i') _) -> i <= -fromIntegral i'
-    Literal (Value (VBignum i') _) -> i <= i'
-    _ -> error "Not yet implemented"
-controlInteger cddl i Ge ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VUInt i') _) -> i >= fromIntegral i'
-    Literal (Value (VNInt i') _) -> i >= -fromIntegral i'
-    Literal (Value (VBignum i') _) -> i >= i'
-    _ -> error "Not yet implemented"
-controlInteger cddl i Eq ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VUInt i') _) -> i == fromIntegral i'
-    Literal (Value (VNInt i') _) -> i == -fromIntegral i'
-    Literal (Value (VBignum i') _) -> i == i'
-    _ -> error "Not yet implemented"
-controlInteger cddl i Ne ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VUInt i') _) -> i /= fromIntegral i'
-    Literal (Value (VNInt i') _) -> i /= -fromIntegral i'
-    Literal (Value (VBignum i') _) -> i /= i'
-    _ -> error "Not yet implemented"
-controlInteger _ _ _ _ = error "Not yet implemented"
-
---------------------------------------------------------------------------------
--- Floating point (Float16, Float32, Float64)
---
--- As opposed to Integral types, there seems to be no ambiguity when encoding
--- and decoding floating-point numbers.
-
--- | Validating a `Float16`
-validateHalf :: HasCallStack => CDDL -> Float -> Rule -> CDDLResult
-validateHalf cddl f rule =
-  case resolveIfRef cddl rule of
-    -- a = any
-    Postlude PTAny -> Valid rule
-    -- a = float16
-    Postlude PTHalf -> Valid rule
-    -- a = 0.5
-    Literal (Value (VFloat16 f') _) -> check (f == f') rule
-    -- a = foo / bar
-    Choice opts -> validateChoice (validateHalf cddl f) opts rule
-    -- a = foo .ctrl bar
-    Control op tgt ctrl -> ctrlDispatch (validateHalf cddl f) op tgt ctrl (controlHalf cddl f) rule
-    -- a = x..y
-    Range low high bound ->
-      check
-        ( case (resolveIfRef cddl low, resolveIfRef cddl high) of
-            (Literal (Value (VFloat16 n) _), Literal (Value (VFloat16 m) _)) -> n <= f && range bound f m
-            _ -> error "Not yet implemented"
-        )
-        rule
-    _ -> UnapplicableRule "validateHalf" rule
-
--- | Controls for `Float16`
-controlHalf :: HasCallStack => CDDL -> Float -> CtlOp -> Rule -> Either (Maybe CBORTermResult) ()
-controlHalf cddl f Eq ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VFloat16 f') _) -> f == f'
-    _ -> error "Not yet implemented"
-controlHalf cddl f Ne ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VFloat16 f') _) -> f /= f'
-    _ -> error "Not yet implemented"
-controlHalf _ _ _ _ = error "Not yet implemented"
-
--- | Validating a `Float32`
-validateFloat :: HasCallStack => CDDL -> Float -> Rule -> CDDLResult
-validateFloat cddl f rule =
-  ($ rule) $ do
-    case resolveIfRef cddl rule of
-      -- a = any
-      Postlude PTAny -> Valid
-      -- a = float32
-      Postlude PTFloat -> Valid
-      -- a = 0.000000005
-      -- TODO: it is unclear if smaller floats should also validate
-      Literal (Value (VFloat32 f') _) -> check $ f == f'
-      -- a = foo / bar
-      Choice opts -> validateChoice (validateFloat cddl f) opts
-      -- a = foo .ctrl bar
-      Control op tgt ctrl -> ctrlDispatch (validateFloat cddl f) op tgt ctrl (controlFloat cddl f)
-      -- a = x..y
-      -- TODO it is unclear if this should mix floating point types too
-      Range low high bound ->
-        check $ case (resolveIfRef cddl low, resolveIfRef cddl high) of
-          (Literal (Value (VFloat16 n) _), Literal (Value (VFloat16 m) _)) -> n <= f && range bound f m
-          (Literal (Value (VFloat32 n) _), Literal (Value (VFloat32 m) _)) -> n <= f && range bound f m
-          _ -> error "Not yet implemented"
-      _ -> UnapplicableRule "validateFloat"
-
--- | Controls for `Float32`
-controlFloat :: HasCallStack => CDDL -> Float -> CtlOp -> Rule -> Either (Maybe CBORTermResult) ()
-controlFloat cddl f Eq ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VFloat16 f') _) -> f == f'
-    Literal (Value (VFloat32 f') _) -> f == f'
-    _ -> error "Not yet implemented"
-controlFloat cddl f Ne ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VFloat16 f') _) -> f /= f'
-    Literal (Value (VFloat32 f') _) -> f /= f'
-    _ -> error "Not yet implemented"
-controlFloat _ _ _ _ = error "Not yet implemented"
-
--- | Validating a `Float64`
-validateDouble :: HasCallStack => CDDL -> Double -> Rule -> CDDLResult
-validateDouble cddl f rule =
-  ($ rule) $ do
-    case resolveIfRef cddl rule of
-      -- a = any
-      Postlude PTAny -> Valid
-      -- a = float64
-      Postlude PTDouble -> Valid
-      -- a = 0.0000000000000000000000000000000000000000000005
-      -- TODO: it is unclear if smaller floats should also validate
-      Literal (Value (VFloat64 f') _) -> check $ f == f'
-      -- a = foo / bar
-      Choice opts -> validateChoice (validateDouble cddl f) opts
-      -- a = foo .ctrl bar
-      Control op tgt ctrl -> ctrlDispatch (validateDouble cddl f) op tgt ctrl (controlDouble cddl f)
-      -- a = x..y
-      -- TODO it is unclear if this should mix floating point types too
-      Range low high bound ->
-        check $ case (resolveIfRef cddl low, resolveIfRef cddl high) of
-          (Literal (Value (VFloat16 (float2Double -> n)) _), Literal (Value (VFloat16 (float2Double -> m)) _)) -> n <= f && range bound f m
-          (Literal (Value (VFloat32 (float2Double -> n)) _), Literal (Value (VFloat32 (float2Double -> m)) _)) -> n <= f && range bound f m
-          (Literal (Value (VFloat64 n) _), Literal (Value (VFloat64 m) _)) -> n <= f && range bound f m
-          _ -> error "Not yet implemented"
-      _ -> UnapplicableRule "validateDouble"
-
--- | Controls for `Float64`
-controlDouble :: HasCallStack => CDDL -> Double -> CtlOp -> Rule -> Either (Maybe CBORTermResult) ()
-controlDouble cddl f Eq ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VFloat16 f') _) -> f == float2Double f'
-    Literal (Value (VFloat32 f') _) -> f == float2Double f'
-    Literal (Value (VFloat64 f') _) -> f == f'
-    _ -> error "Not yet implemented"
-controlDouble cddl f Ne ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VFloat16 f') _) -> f /= float2Double f'
-    Literal (Value (VFloat32 f') _) -> f /= float2Double f'
-    Literal (Value (VFloat64 f') _) -> f /= f'
-    _ -> error "Not yet implemented"
-controlDouble _ _ _ _ = error "Not yet implmented"
-
---------------------------------------------------------------------------------
--- Bool
-
--- | Validating a boolean
-validateBool :: CDDL -> Bool -> Rule -> CDDLResult
-validateBool cddl b rule =
-  ($ rule) $ do
-    case resolveIfRef cddl rule of
-      -- a = any
-      Postlude PTAny -> Valid
-      -- a = bool
-      Postlude PTBool -> Valid
-      -- a = true
-      Literal (Value (VBool b') _) -> check $ b == b'
-      -- a = foo .ctrl bar
-      Control op tgt ctrl -> ctrlDispatch (validateBool cddl b) op tgt ctrl (controlBool cddl b)
-      -- a = foo / bar
-      Choice opts -> validateChoice (validateBool cddl b) opts
-      _ -> UnapplicableRule "validateBool"
-
--- | Controls for `Bool`
-controlBool :: HasCallStack => CDDL -> Bool -> CtlOp -> Rule -> Either (Maybe CBORTermResult) ()
-controlBool cddl b Eq ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VBool b') _) -> b == b'
-    _ -> error "Not yet implemented"
-controlBool cddl b Ne ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VBool b') _) -> b /= b'
-    _ -> error "Not yet implemented"
-controlBool _ _ _ _ = error "Not yet implemented"
-
---------------------------------------------------------------------------------
--- Simple
-
--- | Validating a `TSimple`. It is unclear if this is used for anything else than undefined.
-validateSimple :: CDDL -> Word8 -> Rule -> CDDLResult
-validateSimple cddl 23 rule =
-  do
-    case resolveIfRef cddl rule of
-      -- a = any
-      Postlude PTAny -> Valid rule
-      -- a = undefined
-      Postlude PTUndefined -> Valid rule
-      -- a = foo / bar
-      Choice opts -> validateChoice (validateSimple cddl 23) opts rule
-      _ -> UnapplicableRule "validateSimple" rule
-validateSimple _ n _ = error $ "Found simple different to 23! please report this somewhere! Found: " <> show n
-
---------------------------------------------------------------------------------
--- Null/nil
-
--- | Validating nil
-validateNull :: CDDL -> Rule -> CDDLResult
-validateNull cddl rule =
-  case resolveIfRef cddl rule of
-    -- a = any
-    Postlude PTAny -> Valid rule
-    -- a = nil
-    Postlude PTNil -> Valid rule
-    Choice opts -> validateChoice (validateNull cddl) opts rule
-    _ -> UnapplicableRule "validateNull" rule
-
---------------------------------------------------------------------------------
--- Bytes
-
--- | Validating a byte sequence
-validateBytes :: CDDL -> BS.ByteString -> Rule -> CDDLResult
-validateBytes cddl bs rule =
-  case resolveIfRef cddl rule of
-    -- a = any
-    Postlude PTAny -> Valid rule
-    -- a = bytes
-    Postlude PTBytes -> Valid rule
-    -- a = h'123456'
-    Literal (Value (VBytes bs') _) -> check (bs == bs') rule
-    -- a = foo .ctrl bar
-    Control op tgt ctrl -> ctrlDispatch (validateBytes cddl bs) op tgt ctrl (controlBytes cddl bs) rule
-    -- a = foo / bar
-    Choice opts -> validateChoice (validateBytes cddl bs) opts rule
-    _ -> UnapplicableRule "validateBytes" rule
-
--- | Controls for byte strings
-controlBytes ::
-  HasCallStack =>
-  CDDL ->
-  BS.ByteString ->
-  CtlOp ->
-  Rule ->
-  Either (Maybe CBORTermResult) ()
-controlBytes cddl bs Size ctrl =
-  case resolveIfRef cddl ctrl of
-    Literal (Value (VUInt (fromIntegral -> sz)) _) -> boolCtrl $ BS.length bs == sz
-    Range low high bound ->
-      let i = BS.length bs
-       in boolCtrl $ case (resolveIfRef cddl low, resolveIfRef cddl high) of
-            (Literal (Value (VUInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) -> n <= i && range bound i m
-            (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) -> -n <= i && range bound i m
-            (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VNInt (fromIntegral -> m)) _)) -> -n <= i && range bound i (-m)
-            (Literal (Value VUInt {} _), Literal (Value VNInt {} _)) -> False
-            _ -> error "Not yet implemented"
-    _ -> error "Not yet implemented"
-controlBytes cddl bs Bits ctrl = do
-  let
-    indices =
-      case resolveIfRef cddl ctrl of
-        Literal (Value (VUInt i') _) -> [i']
-        Choice nodes -> getIndicesOfChoice cddl nodes
-        Range ff tt incl -> getIndicesOfRange cddl ff tt incl
-        Enum g -> getIndicesOfEnum cddl g
-        _ -> error "Not yet implemented"
-  boolCtrl $ bitsControlCheck (map fromIntegral indices)
-  where
-    bitsControlCheck :: [Int] -> Bool
-    bitsControlCheck allowedBits =
-      let allowedSet = IS.fromList allowedBits
-          totalBits = BS.length bs * 8
-          isAllowedBit n =
-            let byteIndex = n `shiftR` 3
-                bitIndex = n .&. 7
-             in case BS.indexMaybe bs byteIndex of
-                  Just byte -> not (testBit byte bitIndex) || IS.member n allowedSet
-                  Nothing -> True
-       in all isAllowedBit [0 .. totalBits - 1]
-controlBytes cddl bs Cbor ctrl =
-  case deserialiseFromBytes decodeTerm (BSL.fromStrict bs) of
-    Right (BSL.null -> True, term) ->
-      case validateTerm cddl term ctrl of
-        CBORTermResult _ (Valid _) -> Right ()
-        err -> Left $ Just err
-    _ -> error "Not yet implemented"
-controlBytes cddl bs Cborseq ctrl =
-  case deserialiseFromBytes decodeTerm (BSL.fromStrict (BS.snoc (BS.cons 0x9f bs) 0xff)) of
-    Right (BSL.null -> True, TListI terms) ->
-      case validateTerm cddl (TList terms) (Array [Occur ctrl OIZeroOrMore]) of
-        CBORTermResult _ (Valid _) -> Right ()
-        CBORTermResult _ err -> error $ show err
-    _ -> error "Not yet implemented"
-controlBytes _ _ _ _ = error "Not yet implmented"
-
---------------------------------------------------------------------------------
--- Text
-
--- | Validating text strings
-validateText :: CDDL -> T.Text -> Rule -> CDDLResult
-validateText cddl txt rule =
-  case resolveIfRef cddl rule of
-    -- a = any
-    Postlude PTAny -> Valid rule
-    -- a = text
-    Postlude PTText -> Valid rule
-    -- a = "foo"
-    Literal (Value (VText txt') _) -> check (txt == txt') rule
-    -- a = foo .ctrl bar
-    Control op tgt ctrl -> ctrlDispatch (validateText cddl txt) op tgt ctrl (controlText cddl txt) rule
-    -- a = foo / bar
-    Choice opts -> validateChoice (validateText cddl txt) opts rule
-    _ -> UnapplicableRule "validateText" rule
-
--- | Controls for text strings
-controlText :: HasCallStack => CDDL -> T.Text -> CtlOp -> Rule -> Either (Maybe CBORTermResult) ()
-controlText cddl bs Size ctrl =
-  case resolveIfRef cddl ctrl of
-    Literal (Value (VUInt (fromIntegral -> sz)) _) -> boolCtrl $ T.length bs == sz
-    Range ff tt bound ->
-      boolCtrl $ case (resolveIfRef cddl ff, resolveIfRef cddl tt) of
-        (Literal (Value (VUInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) -> n <= T.length bs && range bound (T.length bs) m
-        (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) -> -n <= T.length bs && range bound (T.length bs) m
-        (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VNInt (fromIntegral -> m)) _)) -> -n <= T.length bs && range bound (T.length bs) (-m)
-        _ -> error "Not yet implemented"
-    _ -> error "Not yet implemented"
-controlText cddl s Regexp ctrl =
-  boolCtrl $ case resolveIfRef cddl ctrl of
-    Literal (Value (VText rxp) _) -> case s =~ rxp :: (T.Text, T.Text, T.Text) of
-      ("", s', "") -> s == s'
-      _ -> error "Not yet implemented"
-    _ -> error "Not yet implemented"
-controlText _ _ _ _ = error "Not yet implemented"
-
---------------------------------------------------------------------------------
--- Tagged values
-
--- | Validating a `TTagged`
-validateTagged :: CDDL -> Word64 -> Term -> Rule -> CDDLResult
-validateTagged cddl tag term rule =
-  case resolveIfRef cddl rule of
-    Postlude PTAny -> Valid rule
-    Tag tag' rule' ->
-      -- If the tag does not match, this is a direct fail
-      if tag == tag'
-        then case validateTerm cddl term rule' of
-          CBORTermResult _ (Valid _) -> Valid rule
-          err -> InvalidTagged rule (Right err)
-        else InvalidTagged rule (Left tag)
-    Choice opts -> validateChoice (validateTagged cddl tag term) opts rule
-    _ -> UnapplicableRule "validateTagged" rule
-
--- --------------------------------------------------------------------------------
--- -- Lists
-
-isWithinBoundsInclusive :: Ord a => a -> Maybe a -> Maybe a -> Bool
-isWithinBoundsInclusive x lb ub = maybe True (x >=) lb && maybe True (x <=) ub
-
-isOptional :: CTree i -> Bool
-isOptional (Occur _ oi) = case oi of
-  OIOptional -> True
-  OIZeroOrMore -> True
-  OIBounded lb ub -> isWithinBoundsInclusive 0 lb ub
-  _ -> False
-isOptional _ = False
-
-decrementBounds :: Maybe Word64 -> Maybe Word64 -> OccurrenceIndicator
-decrementBounds lb ub = OIBounded (clampedPred <$> lb) (clampedPred <$> ub)
-  where
-    clampedPred 0 = 0
-    clampedPred x = pred x
-
-validateList :: CDDL -> [Term] -> Rule -> CDDLResult
-validateList cddl terms rule =
-  case resolveIfRef cddl rule of
-    Postlude PTAny -> Valid rule
-    Array rules -> validate terms rules
-    Choice opts -> validateChoice (validateList cddl terms) opts rule
-    r -> UnapplicableRule "validateList" r
-  where
-    validate :: [Term] -> [CTree ValidatorStage] -> CDDLResult
-    validate [] [] = Valid rule
-    validate _ [] = ListExpansionFail rule [] []
-    validate [] (r : rs)
-      | isOptional r = validate [] rs
-      | otherwise = UnapplicableRule "validateList" r
-    validate (t : ts) (r : rs) = case r of
-      Occur ct oi -> case oi of
-        OIOptional
-          | (Valid {}, leftover) <- validateTermInList (t : ts) ct
-          , res@Valid {} <- validate leftover rs ->
-              res
-          | otherwise -> validate (t : ts) rs
-        OIZeroOrMore
-          | (Valid {}, leftover) <- validateTermInList (t : ts) ct
-          , res@Valid {} <- validate leftover (r : rs) ->
-              res
-          | otherwise -> validate (t : ts) rs
-        OIOneOrMore -> case validateTermInList (t : ts) ct of
-          (Valid {}, leftover) -> validate leftover (Occur ct OIZeroOrMore : rs)
-          (err, _) -> err
-        OIBounded _ (Just ub) | ub < 0 -> ListExpansionFail rule [] []
-        OIBounded lb ub
-          | (Valid {}, leftover) <- validateTermInList (t : ts) ct ->
-              validate leftover (Occur ct (decrementBounds lb ub) : rs)
-          | isWithinBoundsInclusive 0 lb ub ->
-              validate (t : ts) rs
-          | otherwise -> UnapplicableRule "validateList" r
-      _ -> case validateTermInList (t : ts) (resolveIfRef cddl r) of
-        (Valid {}, leftover) -> validate leftover rs
-        (err, _) -> err
-
-    validateTermInList ts (KV _ v _) = validateTermInList ts v
-    validateTermInList ts (Group grp) = case grp of
-      (resolveIfRef cddl -> g) : gs
-        | (Valid {}, leftover) <- validateTermInList ts g -> validateTermInList leftover (Group gs)
-        | otherwise -> (UnapplicableRule "validateTermInList group" g, ts)
-      [] -> (Valid rule, ts)
-    validateTermInList (t : ts) r =
-      let CBORTermResult _ res = validateTerm cddl t r
-       in (res, ts)
-    validateTermInList [] g = (validate [] [g], [])
-
---------------------------------------------------------------------------------
--- Maps
-
-validateMap :: HasCallStack => CDDL -> [(Term, Term)] -> Rule -> CDDLResult
-validateMap cddl terms rule =
-  case resolveIfRef cddl rule of
-    Postlude PTAny -> Valid rule
-    Map rules -> validate [] terms rules
-    Choice opts -> validateChoice (validateMap cddl terms) opts rule
-    r -> UnapplicableRule "validateMap" r
-  where
-    validate :: [Rule] -> [(Term, Term)] -> [Rule] -> CDDLResult
-    validate [] [] [] = Valid rule
-    validate _ _ [] = MapExpansionFail rule [] []
-    validate [] [] (r : rs)
-      | isOptional r = validate [] [] rs
-      | otherwise = UnapplicableRule "validateMap" r
-    validate exhausted kvs (r : rs) = case r of
-      Occur ct oi -> case oi of
-        OIOptional
-          | (Valid {}, leftover) <- validateKVInMap kvs ct
-          , res@Valid {} <- validate [] leftover (exhausted <> rs) ->
-              res
-          | otherwise -> validate (r : exhausted) kvs rs
-        OIZeroOrMore
-          | (Valid {}, leftover) <- validateKVInMap kvs ct
-          , res@Valid {} <- validate [] leftover (r : exhausted <> rs) ->
-              res
-          | otherwise -> validate (r : exhausted) kvs rs
-        OIOneOrMore
-          | (Valid {}, leftover) <- validateKVInMap kvs ct
-          , res@Valid {} <- validate [] leftover (Occur ct OIZeroOrMore : exhausted <> rs) ->
-              res
-          | otherwise -> validate (r : exhausted) kvs rs
-        OIBounded mlb mub
-          | Just lb <- mlb, Just ub <- mub, lb > ub -> error "Unsatisfiable range encountered"
-          | otherwise -> case compare 0 <$> mub of
-              Just EQ -> validate exhausted kvs rs
-              Just GT -> error "Unsatisfiable range encountered"
-              _
-                | (Valid {}, leftover) <- validateKVInMap kvs ct
-                , res@Valid {} <-
-                    validate
-                      []
-                      leftover
-                      (Occur ct (decrementBounds mlb mub) : exhausted <> rs) ->
-                    res
-                | otherwise -> validate (r : exhausted) kvs rs
-      _ -> case validateKVInMap kvs r of
-        (Valid {}, leftover) -> validate [] leftover (exhausted <> rs)
-        _ -> validate (r : exhausted) kvs rs
-
-    validateKVInMap ((tk, tv) : ts) (KV k v _) = case (validateTerm cddl tk k, validateTerm cddl tv v) of
-      (CBORTermResult _ Valid {}, CBORTermResult _ x@Valid {}) -> (x, ts)
-      (CBORTermResult _ Valid {}, CBORTermResult _ err) -> (err, ts)
-      (CBORTermResult _ err, _) -> (err, ts)
-    validateKVInMap [] _ = error "No remaining KV pairs"
-    validateKVInMap _ x = error $ "Unexpected value in map: " <> show x
-
---------------------------------------------------------------------------------
--- Choices
-
-validateChoice :: (Rule -> CDDLResult) -> NE.NonEmpty Rule -> Rule -> CDDLResult
-validateChoice v rules = go rules
-  where
-    go :: NE.NonEmpty Rule -> Rule -> CDDLResult
-    go (choice NE.:| xs) rule = do
-      case v choice of
-        Valid _ -> Valid rule
-        err -> case NE.nonEmpty xs of
-          Nothing -> ChoiceFail rule rules ((choice, err) NE.:| [])
-          Just choices ->
-            case go choices rule of
-              Valid _ -> Valid rule
-              ChoiceFail _ _ errors -> ChoiceFail rule rules ((choice, err) NE.<| errors)
-              _ -> error "Not yet implemented"
-
---------------------------------------------------------------------------------
--- Control helpers
-
--- | Validate both rules
-ctrlAnd :: (Rule -> CDDLResult) -> Rule -> Rule -> Rule -> CDDLResult
-ctrlAnd v tgt ctrl rule =
-  case v tgt of
-    Valid _ ->
-      case v ctrl of
-        Valid _ -> Valid rule
-        _ -> InvalidControl rule Nothing
-    _ -> InvalidRule rule
-
--- | Dispatch to the appropriate control
-ctrlDispatch ::
-  (Rule -> CDDLResult) ->
-  CtlOp ->
-  Rule ->
-  Rule ->
-  (CtlOp -> Rule -> Either (Maybe CBORTermResult) ()) ->
-  Rule ->
-  CDDLResult
-ctrlDispatch v And tgt ctrl _ rule = ctrlAnd v tgt ctrl rule
-ctrlDispatch v Within tgt ctrl _ rule = ctrlAnd v tgt ctrl rule
-ctrlDispatch v op tgt ctrl vctrl rule =
-  case v tgt of
-    Valid _ ->
-      case vctrl op ctrl of
-        Left err -> InvalidControl rule err
-        Right () -> Valid rule
-    _ -> InvalidRule rule
-
--- | A boolean control
-boolCtrl :: Bool -> Either (Maybe CBORTermResult) ()
-boolCtrl c = if c then Right () else Left Nothing
-
---------------------------------------------------------------------------------
--- Bits control
-
-getIndicesOfChoice :: CDDL -> NE.NonEmpty Rule -> [Word64]
-getIndicesOfChoice cddl =
-  concatMap $ \case
-    Literal (Value (VUInt v) _) -> [fromIntegral v]
-    KV _ v _ ->
-      case resolveIfRef cddl v of
-        Literal (Value (VUInt v') _) -> [fromIntegral v']
-        somethingElse ->
-          error $
-            "Malformed value in KV in choice in .bits: "
-              <> show somethingElse
-    Range ff tt incl -> getIndicesOfRange cddl ff tt incl
-    Enum g -> getIndicesOfEnum cddl g
-    somethingElse ->
-      error $
-        "Malformed alternative in choice in .bits: "
-          <> show somethingElse
-
-getIndicesOfRange :: CDDL -> Rule -> Rule -> RangeBound -> [Word64]
-getIndicesOfRange cddl ff tt incl =
-  case (resolveIfRef cddl ff, resolveIfRef cddl tt) of
-    (Literal (Value (VUInt ff') _), Literal (Value (VUInt tt') _)) ->
-      case incl of
-        ClOpen -> init rng
-        Closed -> rng
-      where
-        rng = [ff' .. tt']
-    somethingElse -> error $ "Malformed range in .bits: " <> show somethingElse
-
-getIndicesOfEnum :: CDDL -> Rule -> [Word64]
-getIndicesOfEnum cddl g =
-  case resolveIfRef cddl g of
-    Group g' -> getIndicesOfChoice cddl (fromJust $ NE.nonEmpty g')
-    somethingElse -> error $ "Malformed enum in .bits: " <> show somethingElse
-
---------------------------------------------------------------------------------
--- Resolving rules from the CDDL spec
-
-resolveIfRef :: CDDL -> Rule -> Rule
-resolveIfRef ct@(CTreeRoot cddl) (CTreeE (VRuleRef n)) = do
-  case Map.lookup n cddl of
-    Nothing -> error $ "Unbound reference: " <> show n
-    Just val -> resolveIfRef ct val
-resolveIfRef _ r = r
-
---------------------------------------------------------------------------------
--- Utils
-
-replaceRule :: CDDLResult -> Rule -> CDDLResult
-replaceRule (ChoiceFail _ a b) r = ChoiceFail r a b
-replaceRule (ListExpansionFail _ a b) r = ListExpansionFail r a b
-replaceRule (MapExpansionFail _ a b) r = MapExpansionFail r a b
-replaceRule (InvalidTagged _ a) r = InvalidTagged r a
-replaceRule InvalidRule {} r = InvalidRule r
-replaceRule (InvalidControl _ a) r = InvalidControl r a
-replaceRule (UnapplicableRule m _) r = UnapplicableRule m r
-replaceRule Valid {} r = Valid r
-
-check :: Bool -> Rule -> CDDLResult
-check c = if c then Valid else InvalidRule
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Codec.CBOR.Cuddle.CBOR.Validator (
+  validateCBOR,
+  ValidatorStage,
+) where
+
+import Codec.CBOR.Cuddle.CBOR.Validator.Trace (
+  ControlInfo (..),
+  Evidenced (..),
+  ListValidationTrace (..),
+  MapValidationTrace (..),
+  SValidity (..),
+  ValidationTrace (..),
+  ValidatorStage,
+  XXCTree (..),
+  evidence,
+  isValid,
+  mapTrace,
+  showSimple,
+  showValidationTrace,
+ )
+import Codec.CBOR.Cuddle.CDDL hiding (CDDL, Group, Rule)
+import Codec.CBOR.Cuddle.CDDL.CBORGenerator (CBORValidator (..), CustomValidatorResult (..))
+import Codec.CBOR.Cuddle.CDDL.CTree
+import Codec.CBOR.Cuddle.CDDL.CtlOp
+import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..))
+import Codec.CBOR.Read
+import Codec.CBOR.Term
+import Data.Bifunctor (Bifunctor (..))
+import Data.Bits hiding (And)
+import Data.ByteString qualified as BS
+import Data.ByteString.Lazy qualified as BSL
+import Data.Function ((&))
+import Data.IntSet qualified as IS
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.List.NonEmpty qualified as NE
+import Data.Map.Strict qualified as Map
+import Data.Maybe
+import Data.Text qualified as T
+import Data.Text.Encoding (encodeUtf8)
+import Data.Text.Lazy qualified as TL
+import Data.Word
+import GHC.Float
+import GHC.Stack (HasCallStack)
+import Text.Regex.TDFA
+
+--------------------------------------------------------------------------------
+-- Main entry point
+
+validateCBOR ::
+  HasCallStack =>
+  BS.ByteString ->
+  Name ->
+  CTreeRoot ValidatorStage ->
+  Evidenced ValidationTrace
+validateCBOR bs rule cddl@(CTreeRoot tree) =
+  case deserialiseFromBytes decodeTerm (BSL.fromStrict bs) of
+    Left e -> error $ show e
+    Right (rest, term)
+      | BSL.null rest -> validateTerm cddl term (tree Map.! rule)
+      | otherwise -> error $ "Leftover bytes in CBOR: " <> show rest
+
+--------------------------------------------------------------------------------
+-- Terms
+
+-- | Core function that validates a CBOR term to a particular rule of the CDDL
+-- spec
+validateTerm ::
+  CTreeRoot ValidatorStage ->
+  Term ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateTerm cddl term rule
+  | CTreeE (VRuleRef n) <- rule =
+      dereferenceAndValidate cddl n (validateTerm cddl term)
+  | CTreeE (VValidator (CBORValidator validator) _) <- rule =
+      case validator term of
+        CustomValidatorSuccess -> evidence CustomSuccess
+        CustomValidatorFailure err -> evidence $ CustomFailure err
+  | otherwise =
+      case term of
+        TInt i -> validateInteger cddl (fromIntegral i) rule
+        TInteger i -> validateInteger cddl i rule
+        TBytes b -> validateBytes cddl b rule
+        TBytesI b -> validateBytes cddl (BSL.toStrict b) rule
+        TString s -> validateText cddl s rule
+        TStringI s -> validateText cddl (TL.toStrict s) rule
+        TList ts -> validateList cddl ts rule
+        TListI ts -> validateList cddl ts rule
+        TMap ts -> validateMap cddl ts rule
+        TMapI ts -> validateMap cddl ts rule
+        TTagged w t -> validateTagged cddl w t rule
+        TBool b -> validateBool cddl b rule
+        TNull -> validateNull cddl rule
+        TSimple s -> validateSimple cddl s rule
+        THalf h -> validateHalf cddl h rule
+        TFloat h -> validateFloat cddl h rule
+        TDouble d -> validateDouble cddl d rule
+
+terminal :: CTree ValidatorStage -> Evidenced ValidationTrace
+terminal = evidence . TerminalRule Nothing . mapIndex
+
+unapplicable :: CTree ValidatorStage -> Evidenced ValidationTrace
+unapplicable = evidence . UnapplicableRule . mapIndex
+
+--------------------------------------------------------------------------------
+-- Ints and integers
+
+-- | Validation of an Int or Integer. CBOR categorizes every integral in `TInt`
+-- or `TInteger` but it can be the case that we are decoding something that is
+-- expected to be a `Word64` even if we get a `TInt`.
+--
+-- > ghci> encodeWord64 15
+-- > [TkInt 15]
+-- > ghci> encodeWord64 maxBound
+-- > [TkInteger 18446744073709551615]
+--
+-- For this reason, we cannot assume that bounds or literals are going to be
+-- Ints, so we convert everything to Integer.
+validateInteger ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  Integer ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateInteger cddl i rule =
+  case rule of
+    CTreeE (VRuleRef n) -> dereferenceAndValidate cddl n $ validateInteger cddl i
+    -- echo "C24101" | xxd -r -p - example.cbor
+    -- echo "foo = int" > a.cddl
+    -- cddl a.cddl validate example.cbor
+    --
+    -- but
+    --
+    -- echo "C249010000000000000000"| xxd -r -p - example.cbor
+    -- echo "foo = int" > a.cddl
+    -- cddl a.cddl validate example.cbor
+    --
+    -- and they are both bigints?
+
+    -- a = any
+    Postlude PTAny -> terminal rule
+    -- a = int
+    Postlude PTInt -> terminal rule
+    -- a = uint
+    Postlude PTUInt
+      | i >= 0 -> terminal rule
+    -- a = nint
+    Postlude PTNInt | i <= 0 -> terminal rule
+    -- a = x
+    Literal (Value (VUInt i') _) | i == fromIntegral i' -> terminal rule
+    -- a = -x
+    Literal (Value (VNInt i') _) | -i == fromIntegral i' -> terminal rule
+    -- a = <big number>
+    Literal (Value (VBignum i') _) | i == i' -> terminal rule
+    -- a = foo .ctrl bar
+    Control op tgt ctrl -> ctrlDispatch (validateInteger cddl i) op tgt ctrl (controlInteger cddl i)
+    -- a = foo / bar
+    Choice opts -> validateChoice (validateInteger cddl i) opts
+    -- a = x..y
+    Range low high bound ->
+      case (low, high) of
+        (Literal (Value (VUInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _))
+          | n <= i && range bound i m -> terminal rule
+          | otherwise -> unapplicable rule
+        (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _))
+          | -n <= i && range bound i m -> terminal rule
+          | otherwise -> unapplicable rule
+        (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VNInt (fromIntegral -> m)) _))
+          | -n <= i && range bound i (-m) -> terminal rule
+          | otherwise -> unapplicable rule
+        (Literal (Value VUInt {} _), Literal (Value VNInt {} _)) -> error "range types mismatch"
+        (Literal (Value (VBignum n) _), Literal (Value (VUInt (fromIntegral -> m)) _))
+          | n <= i && range bound i m -> terminal rule
+          | otherwise -> unapplicable rule
+        (Literal (Value (VBignum n) _), Literal (Value (VNInt (fromIntegral -> m)) _))
+          | n <= i && range bound i (-m) -> terminal rule
+          | otherwise -> unapplicable rule
+        (Literal (Value (VUInt (fromIntegral -> n)) _), Literal (Value (VBignum m) _))
+          | n <= i && range bound i m -> terminal rule
+          | otherwise -> unapplicable rule
+        (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VBignum m) _))
+          | (-n) <= i && range bound i m -> terminal rule
+          | otherwise -> unapplicable rule
+        (CTreeE (VRuleRef n), _) ->
+          dereferenceAndValidate cddl n $ \lo -> validateInteger cddl i (Range lo high bound)
+        (_, CTreeE (VRuleRef n)) ->
+          dereferenceAndValidate cddl n $ \hi -> validateInteger cddl i (Range low hi bound)
+        (lo, hi) -> error $ "Unable to validate range: (" <> showSimple lo <> ", " <> showSimple hi <> ")"
+    -- a = &(x, y, z)
+    Enum g ->
+      case g of
+        CTreeE (VRuleRef n) -> dereferenceAndValidate cddl n $ validateInteger cddl i
+        Group g' -> validateInteger cddl i (Choice (NE.fromList g'))
+        _ -> error "Not yet implemented"
+    -- a = x: y
+    -- Note KV cannot appear on its own, but we will use this when validating
+    -- lists.
+    KV _ v _ -> validateInteger cddl i v
+    Tag 2 x -> validateBigInt x
+    Tag 3 x -> validateBigInt x
+    _ -> unapplicable rule
+  where
+    validateBigInt x = case x of
+      CTreeE (VRuleRef n) -> dereferenceAndValidate cddl n validateBigInt
+      Postlude PTBytes -> terminal rule
+      Control op tgt@(Postlude PTBytes) ctrl ->
+        ctrlDispatch (validateBytes cddl bs) op tgt ctrl (controlBytes cddl bs)
+        where
+          -- TODO figure out a way to turn Integer into bytes or figure out why
+          -- tagged bigints are decoded as integers in the first place
+          bs = mempty
+      _ -> unapplicable rule
+
+-- | Controls for an Integer
+controlInteger ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  Integer ->
+  CtlOp ->
+  CTree ValidatorStage ->
+  Bool
+controlInteger cddl i op (CTreeE (VRuleRef n)) =
+  controlInteger cddl i op $ dereference cddl n
+controlInteger _ i Size ctrl =
+  case ctrl of
+    Literal (Value (VUInt sz) _) -> 0 <= i && i < 256 ^ sz
+    _ -> False
+controlInteger cddl i Bits ctrl = do
+  let
+    indices = case ctrl of
+      Literal (Value (VUInt i') _) -> [i']
+      Choice nodes -> getIndicesOfChoice cddl nodes
+      Range ff tt incl -> getIndicesOfRange cddl ff tt incl
+      Enum g -> getIndicesOfEnum cddl g
+      _ -> error "Not yet implemented"
+  go (IS.fromList (map fromIntegral indices)) i 0
+  where
+    go _ 0 _ = True
+    go indices n idx =
+      let bitSet = testBit n 0
+          allowed = not bitSet || IS.member idx indices
+       in allowed && go indices (shiftR n 1) (idx + 1)
+controlInteger _ i Lt ctrl =
+  case ctrl of
+    Literal (Value (VUInt i') _) -> i < fromIntegral i'
+    Literal (Value (VNInt i') _) -> i < -fromIntegral i'
+    Literal (Value (VBignum i') _) -> i < i'
+    _ -> False
+controlInteger _ i Gt ctrl =
+  case ctrl of
+    Literal (Value (VUInt i') _) -> i > fromIntegral i'
+    Literal (Value (VNInt i') _) -> i > -fromIntegral i'
+    Literal (Value (VBignum i') _) -> i > i'
+    _ -> False
+controlInteger _ i Le ctrl =
+  case ctrl of
+    Literal (Value (VUInt i') _) -> i <= fromIntegral i'
+    Literal (Value (VNInt i') _) -> i <= -fromIntegral i'
+    Literal (Value (VBignum i') _) -> i <= i'
+    _ -> False
+controlInteger _ i Ge ctrl =
+  case ctrl of
+    Literal (Value (VUInt i') _) -> i >= fromIntegral i'
+    Literal (Value (VNInt i') _) -> i >= -fromIntegral i'
+    Literal (Value (VBignum i') _) -> i >= i'
+    _ -> False
+controlInteger _ i Eq ctrl =
+  case ctrl of
+    Literal (Value (VUInt i') _) -> i == fromIntegral i'
+    Literal (Value (VNInt i') _) -> i == -fromIntegral i'
+    Literal (Value (VBignum i') _) -> i == i'
+    _ -> False
+controlInteger _ i Ne ctrl =
+  case ctrl of
+    Literal (Value (VUInt i') _) -> i /= fromIntegral i'
+    Literal (Value (VNInt i') _) -> i /= -fromIntegral i'
+    Literal (Value (VBignum i') _) -> i /= i'
+    _ -> False
+controlInteger _ _ _ ctrl = error $ "unexpected control: " <> showSimple ctrl
+
+--------------------------------------------------------------------------------
+-- Floating point (Float16, Float32, Float64)
+--
+-- As opposed to Integral types, there seems to be no ambiguity when encoding
+-- and decoding floating-point numbers.
+
+-- | Validating a `Float16`
+validateHalf ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  Float ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateHalf cddl f (CTreeE (VRuleRef n)) = dereferenceAndValidate cddl n $ validateHalf cddl f
+validateHalf cddl f rule =
+  case rule of
+    -- a = any
+    Postlude PTAny -> terminal rule
+    -- a = float16
+    Postlude PTHalf -> terminal rule
+    -- a = 0.5
+    Literal (Value (VFloat16 f') _) | f == f' -> terminal rule
+    -- a = foo / bar
+    Choice opts -> validateChoice (validateHalf cddl f) opts
+    -- a = foo .ctrl bar
+    Control op tgt ctrl -> ctrlDispatch (validateHalf cddl f) op tgt ctrl (controlHalf cddl f)
+    -- a = x..y
+    Range (CTreeE (VRuleRef n)) high bound ->
+      dereferenceAndValidate cddl n $ \lo -> validateHalf cddl f $ Range lo high bound
+    Range low (CTreeE (VRuleRef n)) bound ->
+      dereferenceAndValidate cddl n $ \hi -> validateHalf cddl f $ Range low hi bound
+    Range (Literal (Value (VFloat16 n) _)) (Literal (Value (VFloat16 m) _)) bound
+      | n <= f && range bound f m -> terminal rule
+    _ -> unapplicable rule
+
+-- | Controls for `Float16`
+controlHalf ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  Float ->
+  CtlOp ->
+  CTree ValidatorStage ->
+  Bool
+controlHalf cddl f op (CTreeE (VRuleRef n)) =
+  controlHalf cddl f op $ dereference cddl n
+controlHalf _ f Eq ctrl =
+  case ctrl of
+    Literal (Value (VFloat16 f') _) -> f == f'
+    _ -> False
+controlHalf _ f Ne ctrl =
+  case ctrl of
+    Literal (Value (VFloat16 f') _) -> f /= f'
+    _ -> False
+controlHalf _ _ op _ = error $ "Not yet implemented for half: " <> show op
+
+-- | Validating a `Float32`
+validateFloat ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  Float ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateFloat cddl f (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateFloat cddl f
+validateFloat cddl f rule =
+  case rule of
+    -- a = any
+    Postlude PTAny -> terminal rule
+    -- a = float32
+    Postlude PTFloat -> terminal rule
+    -- a = 0.000000005
+    -- TODO: it is unclear if smaller floats should also validate
+    Literal (Value (VFloat32 f') _) | f == f' -> terminal rule
+    -- a = foo / bar
+    Choice opts -> validateChoice (validateFloat cddl f) opts
+    -- a = foo .ctrl bar
+    Control op tgt ctrl -> ctrlDispatch (validateFloat cddl f) op tgt ctrl (controlFloat cddl f)
+    -- a = x..y
+    -- TODO it is unclear if this should mix floating point types too
+    Range (CTreeE (VRuleRef n)) high bound ->
+      dereferenceAndValidate cddl n $ \lo -> validateFloat cddl f $ Range lo high bound
+    Range low (CTreeE (VRuleRef n)) bound ->
+      dereferenceAndValidate cddl n $ \hi -> validateFloat cddl f $ Range low hi bound
+    Range (Literal (Value nv _)) (Literal (Value mv _)) bound
+      | VFloat16 n <- nv
+      , VFloat16 m <- mv
+      , n <= f && range bound f m ->
+          terminal rule
+      | VFloat32 n <- nv
+      , VFloat32 m <- mv
+      , n <= f && range bound f m ->
+          terminal rule
+    _ -> unapplicable rule
+
+-- | Controls for `Float32`
+controlFloat ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  Float ->
+  CtlOp ->
+  CTree ValidatorStage ->
+  Bool
+controlFloat cddl f op (CTreeE (VRuleRef n)) =
+  controlFloat cddl f op $ dereference cddl n
+controlFloat _ f Eq ctrl =
+  case ctrl of
+    Literal (Value (VFloat16 f') _) -> f == f'
+    Literal (Value (VFloat32 f') _) -> f == f'
+    _ -> False
+controlFloat _ f Ne ctrl =
+  case ctrl of
+    Literal (Value (VFloat16 f') _) -> f /= f'
+    Literal (Value (VFloat32 f') _) -> f /= f'
+    _ -> False
+controlFloat _ _ op _ = error $ "Not yet implemented for float: " <> show op
+
+-- | Validating a `Float64`
+validateDouble ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  Double ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateDouble cddl f (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateDouble cddl f
+validateDouble cddl f rule =
+  case rule of
+    -- a = any
+    Postlude PTAny -> terminal rule
+    -- a = float64
+    Postlude PTDouble -> terminal rule
+    -- a = 0.0000000000000000000000000000000000000000000005
+    -- TODO: it is unclear if smaller floats should also validate
+    Literal (Value (VFloat64 f') _) | f == f' -> terminal rule
+    -- a = foo / bar
+    Choice opts -> validateChoice (validateDouble cddl f) opts
+    -- a = foo .ctrl bar
+    Control op tgt ctrl -> ctrlDispatch (validateDouble cddl f) op tgt ctrl (controlDouble cddl f)
+    -- a = x..y
+    -- TODO it is unclear if this should mix floating point types too
+    Range (CTreeE (VRuleRef n)) high bound ->
+      dereferenceAndValidate cddl n $ \lo -> validateDouble cddl f $ Range lo high bound
+    Range low (CTreeE (VRuleRef n)) bound ->
+      dereferenceAndValidate cddl n $ \hi -> validateDouble cddl f $ Range low hi bound
+    Range (Literal (Value nv _)) (Literal (Value mv _)) bound
+      | VFloat16 n <- nv
+      , VFloat16 m <- mv
+      , float2Double n <= f && range bound f (float2Double m) ->
+          terminal rule
+      | VFloat32 n <- nv
+      , VFloat32 m <- mv
+      , float2Double n <= f && range bound f (float2Double m) ->
+          terminal rule
+      | VFloat64 n <- nv
+      , VFloat64 m <- mv
+      , n <= f && range bound f m ->
+          terminal rule
+    _ -> unapplicable rule
+
+-- | Controls for `Float64`
+controlDouble ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  Double ->
+  CtlOp ->
+  CTree ValidatorStage ->
+  Bool
+controlDouble cddl f op (CTreeE (VRuleRef n)) =
+  controlDouble cddl f op $ dereference cddl n
+controlDouble _ f Eq ctrl =
+  case ctrl of
+    Literal (Value (VFloat16 f') _) -> f == float2Double f'
+    Literal (Value (VFloat32 f') _) -> f == float2Double f'
+    Literal (Value (VFloat64 f') _) -> f == f'
+    _ -> False
+controlDouble _ f Ne ctrl =
+  case ctrl of
+    Literal (Value (VFloat16 f') _) -> f /= float2Double f'
+    Literal (Value (VFloat32 f') _) -> f /= float2Double f'
+    Literal (Value (VFloat64 f') _) -> f /= f'
+    _ -> False
+controlDouble _ _ op _ = error $ "Not yet implmented for double: " <> show op
+
+--------------------------------------------------------------------------------
+-- Bool
+
+-- | Validating a boolean
+validateBool ::
+  CTreeRoot ValidatorStage ->
+  Bool ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateBool cddl b (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateBool cddl b
+validateBool cddl b rule =
+  case rule of
+    -- a = any
+    Postlude PTAny -> terminal rule
+    -- a = bool
+    Postlude PTBool -> terminal rule
+    -- a = true
+    Literal (Value (VBool b') _) | b == b' -> terminal rule
+    -- a = foo .ctrl bar
+    Control op tgt ctrl -> ctrlDispatch (validateBool cddl b) op tgt ctrl (controlBool cddl b)
+    -- a = foo / bar
+    Choice opts -> validateChoice (validateBool cddl b) opts
+    _ -> unapplicable rule
+
+-- | Controls for `Bool`
+controlBool ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  Bool ->
+  CtlOp ->
+  CTree ValidatorStage ->
+  Bool
+controlBool cddl b op (CTreeE (VRuleRef n)) =
+  controlBool cddl b op $ dereference cddl n
+controlBool _ b Eq ctrl =
+  case ctrl of
+    Literal (Value (VBool b') _) -> b == b'
+    _ -> False
+controlBool _ b Ne ctrl =
+  case ctrl of
+    Literal (Value (VBool b') _) -> b /= b'
+    _ -> False
+controlBool _ _ op _ = error $ "Not yet implemented for bool: " <> show op
+
+--------------------------------------------------------------------------------
+-- Simple
+
+-- | Validating a `TSimple`. It is unclear if this is used for anything else than `undefined`.
+validateSimple ::
+  CTreeRoot ValidatorStage ->
+  Word8 ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateSimple cddl i (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateSimple cddl i
+validateSimple cddl 23 rule =
+  case rule of
+    -- a = any
+    Postlude PTAny -> terminal rule
+    -- a = undefined
+    Postlude PTUndefined -> terminal rule
+    -- a = foo / bar
+    Choice opts -> validateChoice (validateSimple cddl 23) opts
+    _ -> unapplicable rule
+validateSimple _ n _ = error $ "Found simple different to 23! please report this somewhere! Found: " <> show n
+
+--------------------------------------------------------------------------------
+-- Null/nil
+
+-- | Validating nil
+validateNull :: CTreeRoot ValidatorStage -> CTree ValidatorStage -> Evidenced ValidationTrace
+validateNull cddl (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateNull cddl
+validateNull cddl rule =
+  case rule of
+    -- a = any
+    Postlude PTAny -> terminal rule
+    -- a = nil
+    Postlude PTNil -> terminal rule
+    Choice opts -> validateChoice (validateNull cddl) opts
+    _ -> unapplicable rule
+
+--------------------------------------------------------------------------------
+-- Bytes
+
+-- | Validating a byte sequence
+validateBytes ::
+  CTreeRoot ValidatorStage -> BS.ByteString -> CTree ValidatorStage -> Evidenced ValidationTrace
+validateBytes cddl bs (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateBytes cddl bs
+validateBytes cddl bs rule =
+  case rule of
+    -- a = any
+    Postlude PTAny -> terminal rule
+    -- a = bytes
+    Postlude PTBytes -> terminal rule
+    -- a = h'123456'
+    Literal (Value (VBytes bs') _) | bs == bs' -> terminal rule
+    -- a = foo .ctrl bar
+    Control op tgt ctrl -> ctrlDispatch (validateBytes cddl bs) op tgt ctrl (controlBytes cddl bs)
+    -- a = foo / bar
+    Choice opts -> validateChoice (validateBytes cddl bs) opts
+    _ -> unapplicable rule
+
+-- | Controls for byte strings
+controlBytes ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  BS.ByteString ->
+  CtlOp ->
+  CTree ValidatorStage ->
+  Bool
+controlBytes cddl bs op (CTreeE (VRuleRef n)) =
+  controlBytes cddl bs op $ dereference cddl n
+controlBytes cddl bs op@Size ctrl =
+  case ctrl of
+    Literal (Value (VUInt sz) _) -> fromIntegral (BS.length bs) == sz
+    Range (CTreeE (VRuleRef n)) high bound ->
+      dereference cddl n & \lo -> controlBytes cddl bs op $ Range lo high bound
+    Range low (CTreeE (VRuleRef n)) bound ->
+      dereference cddl n & \hi -> controlBytes cddl bs op $ Range low hi bound
+    Range low high bound ->
+      let i = BS.length bs
+       in case (low, high) of
+            (Literal (Value (VUInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) ->
+              boundPlacement i (Just n, Just m) bound == WithinBounds
+            (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) ->
+              boundPlacement i (Just $ -n, Just m) bound == WithinBounds
+            (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VNInt (fromIntegral -> m)) _)) ->
+              boundPlacement i (Just $ -n, Just $ -m) bound == WithinBounds
+            _ -> False
+    _ -> False
+controlBytes cddl bs Bits ctrl = do
+  let
+    indices =
+      case ctrl of
+        Literal (Value (VUInt i') _) -> [i']
+        Choice nodes -> getIndicesOfChoice cddl nodes
+        Range ff tt incl -> getIndicesOfRange cddl ff tt incl
+        Enum g -> getIndicesOfEnum cddl g
+        _ -> error "Not yet implemented"
+  bitsControlCheck (map fromIntegral indices)
+  where
+    bitsControlCheck :: [Int] -> Bool
+    bitsControlCheck allowedBits =
+      let allowedSet = IS.fromList allowedBits
+          totalBits = BS.length bs * 8
+          isAllowedBit n =
+            let byteIndex = n `shiftR` 3
+                bitIndex = n .&. 7
+             in case BS.indexMaybe bs byteIndex of
+                  Just byte -> not (testBit byte bitIndex) || IS.member n allowedSet
+                  Nothing -> True
+       in all isAllowedBit [0 .. totalBits - 1]
+controlBytes cddl bs Cbor ctrl =
+  case deserialiseFromBytes decodeTerm (BSL.fromStrict bs) of
+    Right (BSL.null -> True, term) -> isValid $ validateTerm cddl term ctrl
+    _ -> error "Not yet implemented"
+controlBytes cddl bs Cborseq ctrl =
+  case deserialiseFromBytes decodeTerm (BSL.fromStrict (BS.snoc (BS.cons 0x9f bs) 0xff)) of
+    Right (BSL.null -> True, TListI terms) -> isValid $ validateTerm cddl (TList terms) (Array [Occur ctrl OIZeroOrMore])
+    _ -> False
+controlBytes _ _ op _ = error $ "Not yet implmented for bytes: " <> show op
+
+--------------------------------------------------------------------------------
+-- Text
+
+-- | Validating text strings
+validateText ::
+  CTreeRoot ValidatorStage ->
+  T.Text ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateText cddl txt (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateText cddl txt
+validateText cddl txt rule =
+  case rule of
+    -- a = any
+    Postlude PTAny -> terminal rule
+    -- a = text
+    Postlude PTText -> terminal rule
+    -- a = "foo"
+    Literal (Value (VText txt') _) | txt == txt' -> terminal rule
+    -- a = foo .ctrl bar
+    Control op tgt ctrl -> ctrlDispatch (validateText cddl txt) op tgt ctrl (controlText cddl txt)
+    -- a = foo / bar
+    Choice opts -> validateChoice (validateText cddl txt) opts
+    _ -> unapplicable rule
+
+-- | Controls for text strings
+controlText ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  T.Text ->
+  CtlOp ->
+  CTree ValidatorStage ->
+  Bool
+controlText cddl bs op (CTreeE (VRuleRef n)) =
+  controlText cddl bs op $ dereference cddl n
+controlText cddl bs op@Size ctrl =
+  let bsSize = BS.length $ encodeUtf8 bs
+   in case ctrl of
+        Literal (Value (VUInt (fromIntegral -> sz)) _) -> bsSize == sz
+        Range (CTreeE (VRuleRef n)) high bound ->
+          dereference cddl n & \lo -> controlText cddl bs op $ Range lo high bound
+        Range low (CTreeE (VRuleRef n)) bound ->
+          dereference cddl n & \hi -> controlText cddl bs op $ Range low hi bound
+        Range ff tt bound ->
+          case (ff, tt) of
+            (Literal (Value (VUInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) ->
+              n <= T.length bs && range bound bsSize m
+            (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VUInt (fromIntegral -> m)) _)) ->
+              -n <= T.length bs && range bound bsSize m
+            (Literal (Value (VNInt (fromIntegral -> n)) _), Literal (Value (VNInt (fromIntegral -> m)) _)) ->
+              -n <= T.length bs && range bound bsSize (-m)
+            _ -> False
+        _ -> error "Invalid control value in .size"
+controlText _ s Regexp ctrl =
+  case ctrl of
+    Literal (Value (VText rxp) _) -> case s =~ rxp :: (T.Text, T.Text, T.Text) of
+      ("", s', "") -> s == s'
+      _ -> False
+    _ -> error "Invalid control value in .regexp"
+controlText _ _ op _ = error $ "Not yet implemented for text: " <> show op
+
+--------------------------------------------------------------------------------
+-- Tagged values
+
+-- | Validating a `TTagged`
+validateTagged ::
+  CTreeRoot ValidatorStage -> Word64 -> Term -> CTree ValidatorStage -> Evidenced ValidationTrace
+validateTagged cddl tag term (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateTagged cddl tag term
+validateTagged cddl tag term rule =
+  case rule of
+    Postlude PTAny -> terminal rule
+    Tag tag' rule' ->
+      -- If the tag does not match, this is a direct fail
+      if tag == tag'
+        then mapTrace (TagTrace tag) $ validateTerm cddl term rule'
+        else evidence $ InvalidTag tag
+    Choice opts -> validateChoice (validateTagged cddl tag term) opts
+    _ -> unapplicable rule
+
+-- --------------------------------------------------------------------------------
+-- -- Lists
+
+isWithinBoundsInclusive :: Ord a => a -> Maybe a -> Maybe a -> Bool
+isWithinBoundsInclusive x lb ub = maybe True (x >=) lb && maybe True (x <=) ub
+
+isOptional :: CTree i -> Bool
+isOptional (Occur _ oi) = case oi of
+  OIOptional -> True
+  OIZeroOrMore -> True
+  OIBounded lb ub -> isWithinBoundsInclusive 0 lb ub
+  _ -> False
+isOptional _ = False
+
+data BoundPlacement
+  = BelowBounds
+  | WithinBounds
+  | AboveBounds
+  deriving (Eq, Ord, Show)
+
+boundPlacement :: Ord a => a -> (Maybe a, Maybe a) -> RangeBound -> BoundPlacement
+boundPlacement _ (Nothing, Nothing) _ = WithinBounds
+boundPlacement x (Just lo, mHi) bounds
+  | lo > x = BelowBounds
+  | otherwise = boundPlacement x (Nothing, mHi) bounds
+boundPlacement x (Nothing, Just hi) bounds
+  | range bounds x hi = WithinBounds
+  | otherwise = AboveBounds
+
+decrementBounds :: (Maybe Word64, Maybe Word64) -> OccurrenceIndicator
+decrementBounds (lb, ub) = OIBounded (clampedPred <$> lb) (clampedPred <$> ub)
+  where
+    clampedPred 0 = 0
+    clampedPred x = pred x
+
+validateList ::
+  CTreeRoot ValidatorStage ->
+  [Term] ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateList cddl terms (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateList cddl terms
+validateList cddl terms rule =
+  case rule of
+    Postlude PTAny -> terminal rule
+    Array rules -> mapTrace ListTrace . fst $ validate finalize terms rules
+      where
+        finalize [] = evidence ListValidationDone
+        finalize (x : xs) = evidence . ListValidationLeftoverTerms $ x :| xs
+    Choice opts -> validateChoice (validateList cddl terms) opts
+    _ -> unapplicable rule
+  where
+    validate ::
+      ([Term] -> Evidenced ListValidationTrace) ->
+      [Term] ->
+      [CTree ValidatorStage] ->
+      (Evidenced ListValidationTrace, [Term])
+    validate f tss [] = (f tss, tss)
+    validate f [] (r : rs)
+      | isOptional r = validate f [] rs
+      | otherwise = (evidence $ ListValidationUnappliedRules (mapIndex <$> r :| rs), [])
+    validate f tss@(t : ts) (r : rs) =
+      let
+        consumeTerm ct g = case validateTerm cddl t ct of
+          Evidenced SValid trc -> first (mapTrace $ ListValidationConsume (mapIndex r) trc) $ g ts
+          Evidenced SInvalid trc -> (evidence $ ListValidationMissingRequired (mapIndex ct) trc, tss)
+
+        consumeGroup ns gp g = case validate (const $ evidence ListValidationDone) tss gp of
+          (Evidenced SValid trc, leftover) -> first (mapTrace $ ListValidationConsumeGroup (reverse ns) trc) $ g leftover
+          (Evidenced SInvalid trc, leftover) -> (evidence $ ListValidationBadGroup (reverse ns) trc, leftover)
+
+        consume ct@(CTreeE (VRuleRef n)) g = go n []
+          where
+            go name ns =
+              case dereference cddl name of
+                Group gp -> consumeGroup (name : ns) gp g
+                CTreeE (VRuleRef newName) -> go newName (name : ns)
+                _ -> consumeTerm ct g
+        consume (Group gp) g = consumeGroup [] gp g
+        consume (KV _ v _) g = consume v g
+        consume ct g = consumeTerm ct g
+        continue l = validate f l rs
+        skipRule = validate f tss rs
+        rewriteRule newRule l = validate f l (newRule : rs)
+        validateRule =
+          \case
+            Occur ct oi -> case oi of
+              OIOptional -> consume ct continue <> skipRule
+              OIZeroOrMore -> consume ct (rewriteRule r) <> skipRule
+              OIOneOrMore -> consume ct (rewriteRule (Occur ct OIZeroOrMore))
+              OIBounded lb ub ->
+                let bounds = (lb, ub)
+                 in case boundPlacement 1 bounds Closed of
+                      BelowBounds -> consume ct (rewriteRule (Occur ct $ decrementBounds bounds))
+                      WithinBounds -> consume ct (rewriteRule (Occur ct $ decrementBounds bounds)) <> skipRule
+                      AboveBounds
+                        | boundPlacement 0 (lb, ub) Closed == WithinBounds -> skipRule
+                        | otherwise -> error "Negative upper bound"
+            _ -> consume r continue
+       in
+        validateRule r
+
+--------------------------------------------------------------------------------
+-- Maps
+
+validateMap ::
+  HasCallStack =>
+  CTreeRoot ValidatorStage ->
+  [(Term, Term)] ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+validateMap cddl terms (CTreeE (VRuleRef n)) =
+  dereferenceAndValidate cddl n $ validateMap cddl terms
+validateMap cddl terms rule =
+  case rule of
+    Postlude PTAny -> terminal rule
+    Map rules -> mapTrace MapTrace $ validate [] terms rules
+    Choice opts -> validateChoice (validateMap cddl terms) opts
+    _ -> unapplicable rule
+  where
+    validate ::
+      [CTree ValidatorStage] -> [(Term, Term)] -> [CTree ValidatorStage] -> Evidenced MapValidationTrace
+    validate [] [] [] = evidence MapValidationDone
+    validate _ kvs [] = evidence $ MapValidationLeftoverKVs kvs
+    validate [] [] rs =
+      case NE.nonEmpty $ filter (not . isOptional) rs of
+        Nothing -> evidence MapValidationDone
+        Just requiredRules -> evidence $ MapValidationUnappliedRules (mapIndex <$> requiredRules)
+    validate exhausted kvs (r : rs) =
+      let
+        consume (KV k v _) f = case kvs of
+          ((tk, tv) : leftover) ->
+            case validateTerm cddl tk k of
+              Evidenced SValid kTrc ->
+                case validateTerm cddl tv v of
+                  Evidenced SValid vTrc -> mapTrace (MapValidationConsume (mapIndex r) kTrc vTrc) $ f leftover
+                  Evidenced SInvalid vTrc -> evidence $ MapValidationInvalidValue (mapIndex r) kTrc vTrc
+              Evidenced SInvalid _ -> evidence $ MapValidationUnappliedRules (NE.singleton $ mapIndex r)
+          [] -> error "No remaining KV pairs"
+        consume x _ = error $ "Unexpected value in map: " <> showSimple x
+        postponeRule l = validate (r : exhausted) l rs
+        dropRule l = validate exhausted l rs
+        resetDropRule l = validate [] l (exhausted <> rs)
+        rewriteRule newRule l = validate [] l (newRule : exhausted <> rs)
+       in
+        case r of
+          Occur ct oi ->
+            case oi of
+              OIOptional ->
+                consume ct resetDropRule <> postponeRule kvs
+              OIZeroOrMore ->
+                consume ct (rewriteRule r) <> postponeRule kvs
+              OIOneOrMore ->
+                consume ct (rewriteRule (Occur ct OIZeroOrMore)) <> postponeRule kvs
+              OIBounded mlb mub
+                | Just lb <- mlb, Just ub <- mub, lb > ub -> error "Unsatisfiable range encountered"
+                | otherwise -> case compare 0 <$> mub of
+                    Just EQ -> dropRule kvs
+                    Just GT -> error "Unsatisfiable range encountered"
+                    _ ->
+                      consume ct (rewriteRule (Occur ct $ decrementBounds (mlb, mub)))
+                        <> postponeRule kvs
+          _ -> consume r resetDropRule <> postponeRule kvs
+
+--------------------------------------------------------------------------------
+-- Choices
+
+validateChoice ::
+  (CTree ValidatorStage -> Evidenced ValidationTrace) ->
+  NE.NonEmpty (CTree ValidatorStage) ->
+  Evidenced ValidationTrace
+validateChoice v = go 0
+  where
+    go :: Int -> NE.NonEmpty (CTree ValidatorStage) -> Evidenced ValidationTrace
+    go i (choice NE.:| xs) = do
+      case v choice of
+        Evidenced SValid trc -> evidence $ ChoiceBranch i trc
+        err -> case xs of
+          [] -> err
+          y : ys -> err <> go (succ i) (y NE.:| ys)
+
+--------------------------------------------------------------------------------
+-- Control helpers
+
+-- | Validate both rules
+ctrlAnd ::
+  (CTree ValidatorStage -> Evidenced ValidationTrace) ->
+  CTree ValidatorStage ->
+  CTree ValidatorStage ->
+  Evidenced ValidationTrace
+ctrlAnd v tgt ctrl =
+  case v tgt of
+    (isValid -> True) -> v ctrl
+    err -> err
+
+-- | Dispatch to the appropriate control
+ctrlDispatch ::
+  (CTree ValidatorStage -> Evidenced ValidationTrace) ->
+  CtlOp ->
+  CTree ValidatorStage ->
+  CTree ValidatorStage ->
+  (CtlOp -> CTree ValidatorStage -> Bool) ->
+  Evidenced ValidationTrace
+ctrlDispatch v And tgt ctrl _ = ctrlAnd v tgt ctrl
+ctrlDispatch v Within tgt ctrl _ = ctrlAnd v tgt ctrl
+ctrlDispatch v op tgt ctrl vctrl =
+  case v tgt of
+    Evidenced SValid (TerminalRule _ res)
+      | vctrl op ctrl ->
+          evidence $ TerminalRule (Just (ControlInfo op (mapIndex ctrl))) res
+      | otherwise ->
+          evidence $ UnsatisfiedControl op (mapIndex ctrl)
+    Evidenced SValid trc ->
+      error $ "Unexpected trace:\n\t" <> showValidationTrace trc
+    err -> err
+
+--------------------------------------------------------------------------------
+-- Bits control
+
+getIndicesOfChoice :: CTreeRoot ValidatorStage -> NE.NonEmpty (CTree ValidatorStage) -> [Word64]
+getIndicesOfChoice cddl = concatMap go
+  where
+    go = \case
+      Literal (Value (VUInt v) _) -> [fromIntegral v]
+      KV _ v _ ->
+        case v of
+          CTreeE (VRuleRef n) -> go $ dereference cddl n
+          Literal (Value (VUInt v') _) -> [fromIntegral v']
+          somethingElse ->
+            error $
+              "Malformed value in KV in choice in .bits: "
+                <> showSimple somethingElse
+      Range ff tt incl -> getIndicesOfRange cddl ff tt incl
+      Enum g -> getIndicesOfEnum cddl g
+      somethingElse ->
+        error $
+          "Malformed alternative in choice in .bits: "
+            <> showSimple somethingElse
+
+getIndicesOfRange ::
+  CTreeRoot ValidatorStage -> CTree ValidatorStage -> CTree ValidatorStage -> RangeBound -> [Word64]
+getIndicesOfRange cddl (CTreeE (VRuleRef n)) tt incl =
+  dereference cddl n & \ff -> getIndicesOfRange cddl ff tt incl
+getIndicesOfRange cddl ff (CTreeE (VRuleRef n)) incl =
+  dereference cddl n & \tt -> getIndicesOfRange cddl ff tt incl
+getIndicesOfRange _ ff tt incl =
+  case (ff, tt) of
+    (Literal (Value (VUInt ff') _), Literal (Value (VUInt tt') _)) ->
+      case incl of
+        ClOpen -> init rng
+        Closed -> rng
+      where
+        rng = [ff' .. tt']
+    (lo, hi) -> error $ "Malformed range in .bits: (" <> showSimple lo <> ", " <> showSimple hi <> ")"
+
+getIndicesOfEnum :: CTreeRoot ValidatorStage -> CTree ValidatorStage -> [Word64]
+getIndicesOfEnum cddl (CTreeE (VRuleRef n)) = getIndicesOfEnum cddl $ dereference cddl n
+getIndicesOfEnum cddl g =
+  case g of
+    Group g' -> getIndicesOfChoice cddl (fromJust $ NE.nonEmpty g')
+    somethingElse -> error $ "Malformed enum in .bits: " <> showSimple somethingElse
+
+dereference ::
+  CTreeRoot ValidatorStage ->
+  Name ->
+  CTree ValidatorStage
+dereference (CTreeRoot m) n =
+  case Map.lookup n m of
+    Just r -> r
+    Nothing -> error $ "Nonexistent rule referenced: " <> T.unpack (unName n)
+
+dereferenceAndValidate ::
+  CTreeRoot ValidatorStage ->
+  Name ->
+  (CTree ValidatorStage -> Evidenced ValidationTrace) ->
+  Evidenced ValidationTrace
+dereferenceAndValidate cddl n f =
+  mapTrace (ReferenceRule n) . f $ dereference cddl n
+
+--------------------------------------------------------------------------------
+-- Utils
 
 range :: Ord a => RangeBound -> a -> a -> Bool
 range Closed = (<=)
diff --git a/src/Codec/CBOR/Cuddle/CBOR/Validator/Trace.hs b/src/Codec/CBOR/Cuddle/CBOR/Validator/Trace.hs
new file mode 100644
--- /dev/null
+++ b/src/Codec/CBOR/Cuddle/CBOR/Validator/Trace.hs
@@ -0,0 +1,476 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeData #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Codec.CBOR.Cuddle.CBOR.Validator.Trace (
+  ValidatorStage,
+  ValidatorStageSimple,
+  XXCTree (..),
+  SValidity (..),
+  Validity (..),
+  ValidationTrace (..),
+  ListValidationTrace (..),
+  MapValidationTrace (..),
+  Evidenced (..),
+  ControlInfo (..),
+  TraceOptions (..),
+  defaultTraceOptions,
+  showSimple,
+  traceValidity,
+  isValid,
+  prettyValidationTrace,
+  showValidationTrace,
+  mapTrace,
+  compareEvidencedProgress,
+  evidence,
+  foldEvidenced,
+) where
+
+import Codec.CBOR.Cuddle.CDDL (Name (..), OccurrenceIndicator (..), RangeBound (..), XTerm)
+import Codec.CBOR.Cuddle.CDDL.CBORGenerator (CBORValidator)
+import Codec.CBOR.Cuddle.CDDL.CTree (CTree (..), CTreeRoot (..), Node, XXCTree, foldCTree)
+import Codec.CBOR.Cuddle.CDDL.CtlOp (CtlOp)
+import Codec.CBOR.Cuddle.CDDL.Resolve (MonoReferenced, XXCTree (..))
+import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..))
+import Codec.CBOR.Term (Term)
+import Data.Foldable (Foldable (..))
+import Data.Function (on)
+import Data.Kind (Type)
+import Data.List.NonEmpty (NonEmpty)
+import Data.Text (Text)
+import Data.Text qualified as T
+import Data.Type.Equality (TestEquality (..), (:~:) (..))
+import Data.Word (Word64)
+import Prettyprinter (
+  Doc,
+  Pretty (..),
+  annotate,
+  defaultLayoutOptions,
+  encloseSep,
+  group,
+  hang,
+  indent,
+  layoutPretty,
+  list,
+  punctuate,
+  tupled,
+  vsep,
+  (<+>),
+ )
+import Prettyprinter.Render.Terminal (AnsiStyle, Color (..), color, italicized)
+import Prettyprinter.Render.Terminal qualified as Ansi
+
+--------------------------------------------------------------------------------
+-- ValidatorStage
+
+type data ValidatorStage
+
+data instance XTerm ValidatorStage = ValidatorXTerm
+  deriving (Show, Eq)
+
+data instance XXCTree ValidatorStage
+  = VRuleRef Name
+  | VValidator CBORValidator (CTree ValidatorStage)
+
+instance IndexMappable CTreeRoot MonoReferenced ValidatorStage where
+  mapIndex (CTreeRoot m) = CTreeRoot $ mapIndex <$> m
+
+instance IndexMappable CTree MonoReferenced ValidatorStage where
+  mapIndex = foldCTree mapExt mapIndex
+    where
+      mapExt (MRuleRef n) = CTreeE $ VRuleRef n
+      mapExt (MGenerator _ x) = mapIndex x
+      mapExt (MValidator v x) = CTreeE . VValidator v $ mapIndex x
+
+type data ValidatorStageSimple
+
+newtype instance XXCTree ValidatorStageSimple = VRuleRefSimple Name
+
+instance IndexMappable CTreeRoot ValidatorStage ValidatorStageSimple where
+  mapIndex (CTreeRoot m) = CTreeRoot $ mapIndex <$> m
+
+instance IndexMappable CTree ValidatorStage ValidatorStageSimple where
+  mapIndex = foldCTree mapExt mapIndex
+    where
+      mapExt (VRuleRef n) = CTreeE $ VRuleRefSimple n
+      mapExt (VValidator _ x) = mapIndex x
+
+instance Pretty (CTree ValidatorStageSimple) where
+  pretty = \case
+    Literal v -> pretty v
+    Postlude v -> pretty v
+    Range lo hi ClOpen -> pretty lo <+> "..." <+> pretty hi
+    Range lo hi Closed -> pretty lo <+> ".." <+> pretty hi
+    KV k v _ -> pretty k <+> "==>" <+> pretty v
+    CTreeE (VRuleRefSimple (Name n)) -> pretty n
+    Occur v oi ->
+      case oi of
+        OIOptional -> "?" <+> pretty v
+        OIZeroOrMore -> "*" <+> pretty v
+        OIOneOrMore -> "+" <+> pretty v
+        OIBounded lo hi -> foldMap pretty lo <> "*" <> foldMap pretty hi <+> pretty v
+    Map m -> encloseSep "{" "}" "," $ pretty <$> m
+    Array e -> list $ pretty <$> e
+    Choice c -> group . vsep . punctuate "//" $ pretty <$> toList c
+    Group g -> tupled $ pretty <$> g
+    Control op tgt ctl -> pretty tgt <+> pretty op <+> pretty ctl
+    Enum e -> "&" <> pretty e
+    Unwrap x -> "~" <> pretty x
+    Tag t x -> "#6." <> pretty t <> "(" <> pretty x <> ")"
+
+showSimple ::
+  ( IndexMappable a ValidatorStage ValidatorStageSimple
+  , Show (a ValidatorStageSimple)
+  ) =>
+  a ValidatorStage -> String
+showSimple = show . mapIndex @_ @_ @ValidatorStageSimple
+
+deriving instance Eq (Node ValidatorStageSimple)
+
+deriving instance Show (Node ValidatorStageSimple)
+
+--------------------------------------------------------------------------------
+-- Validation result
+
+type data Validity
+  = IsValid
+  | IsInvalid
+
+data SValidity (v :: Validity) where
+  SInvalid :: SValidity IsInvalid
+  SValid :: SValidity IsValid
+
+deriving instance Eq (SValidity v)
+
+deriving instance Ord (SValidity v)
+
+deriving instance Show (SValidity v)
+
+instance TestEquality SValidity where
+  testEquality SValid SValid = Just Refl
+  testEquality SInvalid SInvalid = Just Refl
+  testEquality _ _ = Nothing
+
+data ControlInfo = ControlInfo
+  { ciOp :: CtlOp
+  , ciRule :: CTree ValidatorStageSimple
+  }
+  deriving (Show)
+
+instance Pretty ControlInfo where
+  pretty ControlInfo {..} = pretty ciOp <+> pretty ciRule
+
+data ValidationTrace (v :: Validity) where
+  UnapplicableRule :: CTree ValidatorStageSimple -> ValidationTrace IsInvalid
+  TerminalRule :: Maybe ControlInfo -> CTree ValidatorStageSimple -> ValidationTrace IsValid
+  ReferenceRule :: Name -> ValidationTrace v -> ValidationTrace v
+  CustomFailure :: Text -> ValidationTrace IsInvalid
+  CustomSuccess :: ValidationTrace IsValid
+  UnsatisfiedControl :: CtlOp -> CTree ValidatorStageSimple -> ValidationTrace IsInvalid
+  ChoiceBranch :: Int -> ValidationTrace IsValid -> ValidationTrace IsValid
+  ListTrace :: ListValidationTrace v -> ValidationTrace v
+  MapTrace :: MapValidationTrace v -> ValidationTrace v
+  TagTrace :: Word64 -> ValidationTrace v -> ValidationTrace v
+  InvalidTag :: Word64 -> ValidationTrace IsInvalid
+
+deriving instance Show (ValidationTrace v)
+
+data ListValidationTrace (v :: Validity) where
+  ListValidationDone :: ListValidationTrace IsValid
+  ListValidationLeftoverTerms :: NonEmpty Term -> ListValidationTrace IsInvalid
+  ListValidationUnappliedRules ::
+    NonEmpty (CTree ValidatorStageSimple) -> ListValidationTrace IsInvalid
+  ListValidationConsume ::
+    CTree ValidatorStageSimple ->
+    ValidationTrace IsValid ->
+    ListValidationTrace v ->
+    ListValidationTrace v
+  ListValidationMissingRequired ::
+    CTree ValidatorStageSimple -> ValidationTrace IsInvalid -> ListValidationTrace IsInvalid
+  ListValidationConsumeGroup ::
+    [Name] ->
+    ListValidationTrace IsValid ->
+    ListValidationTrace v ->
+    ListValidationTrace v
+  ListValidationBadGroup ::
+    [Name] ->
+    ListValidationTrace IsInvalid ->
+    ListValidationTrace IsInvalid
+
+deriving instance Show (ListValidationTrace v)
+
+data MapValidationTrace (v :: Validity) where
+  MapValidationDone :: MapValidationTrace IsValid
+  MapValidationLeftoverKVs :: [(Term, Term)] -> MapValidationTrace IsInvalid
+  MapValidationUnappliedRules :: NonEmpty (CTree ValidatorStageSimple) -> MapValidationTrace IsInvalid
+  MapValidationInvalidValue ::
+    CTree ValidatorStageSimple ->
+    ValidationTrace IsValid ->
+    ValidationTrace IsInvalid ->
+    MapValidationTrace IsInvalid
+  MapValidationConsume ::
+    CTree ValidatorStageSimple ->
+    ValidationTrace IsValid ->
+    ValidationTrace IsValid ->
+    MapValidationTrace v ->
+    MapValidationTrace v
+
+deriving instance Show (MapValidationTrace v)
+
+mapTrace :: (forall v. Show (u v)) => (forall v. t v -> u v) -> Evidenced t -> Evidenced u
+mapTrace f (Evidenced v t) = Evidenced v $ f t
+
+data Evidenced t where
+  Evidenced ::
+    { eValidity :: SValidity v
+    , eTrace :: t v
+    } ->
+    Evidenced t
+
+foldEvidenced :: (forall v. t v -> a) -> Evidenced t -> a
+foldEvidenced f (Evidenced v t) =
+  case v of
+    SValid -> f t
+    SInvalid -> f t
+
+deriving instance (forall v. Show (t v)) => Show (Evidenced t)
+
+instance IsValidationTrace t => Semigroup (Evidenced t) where
+  x@(Evidenced SValid _) <> _ = x
+  _ <> y@(Evidenced SValid _) = y
+  Evidenced SInvalid x <> Evidenced SInvalid y =
+    Evidenced SInvalid $ case compareInvalidProgress x y of
+      GT -> x
+      _ -> y
+
+class IsValidationTrace (t :: Validity -> Type) where
+  traceValidity :: t v -> SValidity v
+  measureProgress :: t v -> Int
+
+instance IsValidationTrace ValidationTrace where
+  traceValidity = \case
+    CustomSuccess {} -> SValid
+    TerminalRule {} -> SValid
+    ChoiceBranch {} -> SValid
+    UnapplicableRule {} -> SInvalid
+    CustomFailure {} -> SInvalid
+    UnsatisfiedControl {} -> SInvalid
+    InvalidTag {} -> SInvalid
+    ReferenceRule _ x -> traceValidity x
+    ListTrace x -> traceValidity x
+    MapTrace x -> traceValidity x
+    TagTrace _ x -> traceValidity x
+
+  measureProgress = \case
+    TerminalRule {} -> 1
+    CustomSuccess -> 1
+    ChoiceBranch {} -> 1
+    UnapplicableRule {} -> 0
+    CustomFailure {} -> 0
+    UnsatisfiedControl {} -> 0
+    InvalidTag {} -> 0
+    ReferenceRule _ x -> succ $ measureProgress x
+    ListTrace x -> measureProgress x
+    MapTrace x -> measureProgress x
+    TagTrace _ x -> succ $ measureProgress x
+
+instance IsValidationTrace ListValidationTrace where
+  traceValidity = \case
+    ListValidationDone -> SValid
+    ListValidationLeftoverTerms {} -> SInvalid
+    ListValidationUnappliedRules {} -> SInvalid
+    ListValidationMissingRequired {} -> SInvalid
+    ListValidationBadGroup _ _ -> SInvalid
+    ListValidationConsume _ _ x -> traceValidity x
+    ListValidationConsumeGroup _ _ x -> traceValidity x
+
+  measureProgress = \case
+    ListValidationDone -> 10
+    ListValidationConsume _ _ x -> succ $ measureProgress x
+    ListValidationLeftoverTerms _ -> 0
+    ListValidationMissingRequired _ _ -> 0
+    ListValidationUnappliedRules _ -> 0
+    ListValidationConsumeGroup _ g x -> measureProgress g + measureProgress x
+    ListValidationBadGroup _ x -> measureProgress x
+
+instance IsValidationTrace MapValidationTrace where
+  traceValidity = \case
+    MapValidationDone -> SValid
+    MapValidationLeftoverKVs _ -> SInvalid
+    MapValidationUnappliedRules _ -> SInvalid
+    MapValidationInvalidValue {} -> SInvalid
+    MapValidationConsume _ _ _ x -> traceValidity x
+
+  measureProgress = \case
+    MapValidationDone -> 10
+    MapValidationLeftoverKVs _ -> 0
+    MapValidationUnappliedRules _ -> 0
+    MapValidationConsume _ _ _ x -> 3 + measureProgress x
+    MapValidationInvalidValue {} -> 2
+
+evidence :: (Show (t v), IsValidationTrace t) => t v -> Evidenced t
+evidence x = Evidenced (traceValidity x) x
+
+isValid :: Evidenced t -> Bool
+isValid Evidenced {eValidity = SValid} = True
+isValid _ = False
+
+compareEvidencedProgress :: IsValidationTrace t => Evidenced t -> Evidenced t -> Ordering
+compareEvidencedProgress (Evidenced SValid _) (Evidenced SValid _) = EQ
+compareEvidencedProgress (Evidenced SInvalid _) (Evidenced SValid _) = LT
+compareEvidencedProgress (Evidenced SValid _) (Evidenced SInvalid _) = GT
+compareEvidencedProgress (Evidenced SInvalid x) (Evidenced SInvalid y) =
+  x `compareInvalidProgress` y
+
+compareInvalidProgress :: IsValidationTrace t => t IsInvalid -> t IsInvalid -> Ordering
+compareInvalidProgress = compare `on` measureProgress
+
+nestContainer :: Doc AnsiStyle -> Doc AnsiStyle
+nestContainer = hang 2 . ("└ " <>)
+
+newtype TraceOptions = TraceOptions
+  { toFoldValid :: Bool
+  }
+
+defaultTraceOptions :: TraceOptions
+defaultTraceOptions = TraceOptions {toFoldValid = False}
+
+prettyListValidationResult :: TraceOptions -> ListValidationTrace v -> Doc AnsiStyle
+prettyListValidationResult opts@TraceOptions {..} = \case
+  ListValidationDone -> mempty
+  ListValidationLeftoverTerms _ -> annotate (color Red) "leftover elements after all rules have been applied"
+  ListValidationUnappliedRules _ -> annotate (color Red) "not all required rules have been applied"
+  ListValidationConsume _ t c
+    | toFoldValid -> foldValid 1 c
+    | otherwise -> vsep $ continue c [prettyValidationTrace opts t]
+  ListValidationMissingRequired _ t ->
+    vsep
+      [ annotate (color Red) "failed to apply required rule:"
+      , nestContainer $ prettyValidationTrace opts t
+      ]
+  ListValidationConsumeGroup refs x c -> vsep . continue c $ prettyGroup SValid refs x
+  ListValidationBadGroup refs x -> vsep $ prettyGroup SInvalid refs x
+  where
+    -- This prevents unnecessary empty lines
+    continue ListValidationDone l = l
+    continue x l = l <> [prettyListValidationResult opts x]
+
+    prettyGroup :: SValidity v -> [Name] -> ListValidationTrace v -> [Doc AnsiStyle]
+    prettyGroup v refs x = go refs
+      where
+        go (n : ns) =
+          [ "ref" <+> pretty n
+          , nestContainer . vsep $ go ns
+          ]
+        go [] =
+          [ case v of
+              SValid -> "grp"
+              SInvalid -> "grp" <+> annotate (color Red) "(fail)"
+          , nestContainer $ prettyListValidationResult opts x
+          ]
+
+    foldValid !n (ListValidationConsume _ _ c) = foldValid (n + 1) c
+    foldValid !n t =
+      vsep $ continue t [annotate italicized $ pretty (n :: Int) <> " valid elements"]
+
+prettyMapValidationResult :: TraceOptions -> MapValidationTrace v -> Doc AnsiStyle
+prettyMapValidationResult opts@TraceOptions {..} = \case
+  MapValidationDone -> mempty
+  MapValidationLeftoverKVs _ -> annotate (color Red) "no more rules left to apply"
+  MapValidationUnappliedRules rs ->
+    hang 2 $
+      vsep
+        [ annotate (color Red) "not all required rules have been applied:"
+        , vsep (toList $ pretty <$> rs)
+        ]
+  MapValidationConsume _ k v c
+    | toFoldValid -> foldValid 1 c
+    | otherwise ->
+        vsep $
+          continue
+            c
+            [ "key:"
+            , nestContainer $ prettyValidationTrace opts k
+            , "value:"
+            , nestContainer $ prettyValidationTrace opts v
+            ]
+  MapValidationInvalidValue _ k v ->
+    vsep
+      [ "key:"
+      , nestContainer $ prettyValidationTrace opts k
+      , "value:" <+> annotate (color Red) "(fail)"
+      , nestContainer $ prettyValidationTrace opts v
+      ]
+  where
+    foldValid !n (MapValidationConsume _ _ _ c) = foldValid (n + 1) c
+    foldValid !n t =
+      vsep . continue t $
+        [ annotate italicized $ pretty (n :: Int) <> " valid key-value pairs"
+        , "..."
+        ]
+
+    -- This prevents unnecessary empty lines
+    continue MapValidationDone l = l
+    continue x l = l <> [prettyMapValidationResult opts x]
+
+prettyValidationTrace :: TraceOptions -> ValidationTrace v -> Doc AnsiStyle
+prettyValidationTrace opts = \case
+  UnapplicableRule x -> annotate (color Red) $ vsep ["failed to apply: ", indent 2 $ pretty x]
+  TerminalRule mCi x -> case mCi of
+    Just ci ->
+      vsep
+        [ appMsg
+        , nestContainer $ "ctrl:" <+> annotate (color Yellow) ("." <> pretty ci)
+        ]
+    Nothing -> appMsg
+    where
+      appMsg = "app: " <> annotate (color Green) (pretty x)
+  ChoiceBranch i c ->
+    vsep
+      [ "choice (idx: " <> pretty i <> ")"
+      , nestContainer $ prettyValidationTrace opts c
+      ]
+  ReferenceRule (Name n) x ->
+    vsep
+      [ "ref: " <> annotate (color Blue) (pretty n)
+      , nestContainer $ prettyValidationTrace opts x
+      ]
+  CustomFailure e -> annotate (color Red) $ pretty e
+  CustomSuccess -> "<custom validator>"
+  UnsatisfiedControl op ctl ->
+    annotate (color Red) $
+      vsep
+        [ "unsatisfied control:"
+        , indent 2 $ "." <> pretty op <+> pretty ctl
+        ]
+  ListTrace l ->
+    vsep
+      [ "array"
+      , nestContainer $ prettyListValidationResult opts l
+      ]
+  MapTrace m ->
+    vsep
+      [ "map"
+      , nestContainer $ prettyMapValidationResult opts m
+      ]
+  TagTrace t x ->
+    vsep
+      [ "tag:" <+> annotate (color Green) ("#6." <> pretty t)
+      , nestContainer $ prettyValidationTrace opts x
+      ]
+  InvalidTag t ->
+    "expected tag #6." <> pretty t
+
+showValidationTrace :: ValidationTrace v -> String
+showValidationTrace =
+  T.unpack
+    . Ansi.renderStrict
+    . layoutPretty defaultLayoutOptions
+    . prettyValidationTrace defaultTraceOptions
diff --git a/src/Codec/CBOR/Cuddle/CDDL/CBORGenerator.hs b/src/Codec/CBOR/Cuddle/CDDL/CBORGenerator.hs
--- a/src/Codec/CBOR/Cuddle/CDDL/CBORGenerator.hs
+++ b/src/Codec/CBOR/Cuddle/CDDL/CBORGenerator.hs
@@ -1,13 +1,31 @@
+{-# LANGUAGE TypeData #-}
+{-# LANGUAGE TypeFamilies #-}
+
 module Codec.CBOR.Cuddle.CDDL.CBORGenerator (
   CBORGenerator (..),
   HasGenerator (..),
   WrappedTerm (..),
+  CBORValidator (..),
+  HasValidator (..),
+  GenPhase,
+  XXCTree (..),
+  CustomValidatorResult (..),
 ) where
 
+import Codec.CBOR.Cuddle.CDDL (Name)
+import Codec.CBOR.Cuddle.CDDL.CTree (CTree, CTreeRoot, XXCTree)
 import Codec.CBOR.Term (Term)
+import Data.Text (Text)
+import GHC.Generics (Generic)
 import Optics.Core (Lens')
-import System.Random.Stateful (StatefulGen)
+import Test.AntiGen (AntiGen)
 
+type data GenPhase
+
+data instance XXCTree GenPhase
+  = GenRef Name
+  | GenGenerator CBORGenerator (CTree GenPhase)
+
 data WrappedTerm
   = -- | Single term
     S Term
@@ -17,7 +35,17 @@
     G [WrappedTerm]
   deriving (Eq, Show)
 
-newtype CBORGenerator = CBORGenerator (forall g m. StatefulGen g m => g -> m WrappedTerm)
+newtype CBORGenerator = CBORGenerator (CTreeRoot GenPhase -> AntiGen WrappedTerm)
 
 class HasGenerator a where
   generatorL :: Lens' a (Maybe CBORGenerator)
+
+class HasValidator a where
+  validatorL :: Lens' a (Maybe CBORValidator)
+
+data CustomValidatorResult
+  = CustomValidatorSuccess
+  | CustomValidatorFailure Text
+  deriving (Generic, Show, Eq)
+
+newtype CBORValidator = CBORValidator (Term -> CustomValidatorResult)
diff --git a/src/Codec/CBOR/Cuddle/CDDL/CTree.hs b/src/Codec/CBOR/Cuddle/CDDL/CTree.hs
--- a/src/Codec/CBOR/Cuddle/CDDL/CTree.hs
+++ b/src/Codec/CBOR/Cuddle/CDDL/CTree.hs
@@ -1,31 +1,16 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE TypeData #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module Codec.CBOR.Cuddle.CDDL.CTree where
 
-import Codec.CBOR.Cuddle.CDDL (
-  Name,
-  OccurrenceIndicator,
-  RangeBound,
-  Value,
-  XCddl,
-  XRule,
-  XTerm,
-  XXTopLevel,
-  XXType2,
- )
-import Codec.CBOR.Cuddle.CDDL.CBORGenerator (CBORGenerator)
+import Codec.CBOR.Cuddle.CDDL (Name, OccurrenceIndicator, RangeBound, Value)
 import Codec.CBOR.Cuddle.CDDL.CtlOp
 import Control.Monad.Identity (Identity (..))
-import Data.Default.Class (Default)
 import Data.Hashable (Hashable)
 import Data.List.NonEmpty qualified as NE
 import Data.Map.Strict qualified as Map
-import Data.Void (Void)
 import Data.Word (Word64)
 import GHC.Generics (Generic)
 
@@ -40,25 +25,6 @@
 --------------------------------------------------------------------------------
 
 data family XXCTree i
-
-type data CTreePhase
-
-data instance XTerm CTreePhase = CTreeXTerm
-  deriving (Generic, Show, Eq, Ord)
-  deriving anyclass (Hashable, Default)
-
-newtype instance XXTopLevel CTreePhase = CTreeXXTopLevel Void
-  deriving (Generic, Show, Eq, Ord)
-
-data instance XCddl CTreePhase = CTreeXCddl
-  deriving (Generic, Show, Eq, Ord)
-
-newtype instance XRule CTreePhase = CTreeXRule (Maybe CBORGenerator)
-  deriving (Generic)
-
-newtype instance XXType2 CTreePhase = CTreeXXType2 Void
-  deriving (Generic, Show, Eq, Ord)
-  deriving anyclass (Hashable)
 
 data CTree i
   = Literal Value
diff --git a/src/Codec/CBOR/Cuddle/CDDL/CTreePhase.hs b/src/Codec/CBOR/Cuddle/CDDL/CTreePhase.hs
new file mode 100644
--- /dev/null
+++ b/src/Codec/CBOR/Cuddle/CDDL/CTreePhase.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE TypeData #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Codec.CBOR.Cuddle.CDDL.CTreePhase (
+  CTreePhase,
+  XTerm (..),
+  XCddl (..),
+  XRule (..),
+  XXTopLevel,
+) where
+
+import Codec.CBOR.Cuddle.CDDL (XCddl, XRule, XTerm, XXTopLevel, XXType2)
+import Codec.CBOR.Cuddle.CDDL.CBORGenerator (CBORGenerator, CBORValidator)
+import Data.Default.Class (Default)
+import Data.Hashable (Hashable)
+import GHC.Generics (Generic)
+
+type data CTreePhase
+
+data instance XTerm CTreePhase = CTreeXTerm
+  deriving (Generic, Show, Eq, Ord)
+  deriving anyclass (Hashable, Default)
+
+data instance XXTopLevel CTreePhase
+  deriving (Generic, Show, Eq, Ord)
+
+data instance XCddl CTreePhase = CTreeXCddl
+  deriving (Generic, Show, Eq, Ord)
+
+data instance XRule CTreePhase = CTreeXRule (Maybe CBORGenerator) (Maybe CBORValidator)
+  deriving (Generic)
+
+data instance XXType2 CTreePhase
+  deriving (Generic, Show, Eq, Ord)
+  deriving anyclass (Hashable)
diff --git a/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs b/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs
--- a/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs
+++ b/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TypeData #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -34,6 +35,7 @@
   fullResolveCDDL,
   NameResolutionFailure (..),
   MonoReferenced,
+  MonoSimple,
   XXCTree (..),
 )
 where
@@ -48,12 +50,9 @@
 import Codec.CBOR.Cuddle.CDDL as CDDL
 import Codec.CBOR.Cuddle.CDDL.CTree (
   CTree (..),
-  CTreePhase,
   CTreeRoot (..),
   PTerm (..),
-  XRule (..),
   XXCTree,
-  XXType2 (..),
   foldCTree,
  )
 import Codec.CBOR.Cuddle.CDDL.CTree qualified as CTree
@@ -66,12 +65,17 @@
 #if __GLASGOW_HASKELL__ < 910
 import Data.List (foldl')
 #endif
-import Codec.CBOR.Cuddle.CDDL.CBORGenerator (CBORGenerator)
+import Codec.CBOR.Cuddle.CDDL.CBORGenerator (
+  CBORGenerator,
+  CBORValidator,
+  GenPhase,
+  XXCTree (..),
+ )
+import Codec.CBOR.Cuddle.CDDL.CTreePhase (CTreePhase, XRule (..))
 import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..))
 import Data.List.NonEmpty qualified as NE
 import Data.Map.Strict qualified as Map
 import Data.Text qualified as T
-import Data.Void (absurd)
 import GHC.Generics (Generic)
 import Optics.Core
 
@@ -90,9 +94,15 @@
 newtype PartialCTreeRoot i = PartialCTreeRoot (Map.Map Name (ProvidedParameters (CTree i)))
   deriving (Generic)
 
-type CDDLMap =
-  Map.Map Name (ProvidedParameters (TypeOrGroup CTreePhase), Maybe CBORGenerator)
+data CDDLMapEntry = CDDLMapEntry
+  { cmeProvidedParameters :: ProvidedParameters (TypeOrGroup CTreePhase)
+  , cmeCustomGenerator :: Maybe CBORGenerator
+  , cmeCustomValidator :: Maybe CBORValidator
+  }
+  deriving (Generic)
 
+type CDDLMap = Map.Map Name CDDLMapEntry
+
 toParametrised ::
   TypeOrGroup CTreePhase ->
   Maybe (GenericParameters CTreePhase) ->
@@ -108,36 +118,36 @@
     go x (TopLevelRule r) = assignOrExtend x r
 
     assignOrExtend :: CDDLMap -> Rule CTreePhase -> CDDLMap
-    assignOrExtend m (Rule n gps assign tog (CTreeXRule g)) = case assign of
+    assignOrExtend m (Rule n gps assign tog (CTreeXRule g v)) = case assign of
       -- Equals assignment
-      AssignEq -> Map.insert n (toParametrised tog gps, g) m
+      AssignEq -> Map.insert n (CDDLMapEntry (toParametrised tog gps) g v) m
       AssignExt ->
         Map.alter (extend tog gps) n m
 
     extend ::
       TypeOrGroup CTreePhase ->
       Maybe (GenericParameters CTreePhase) ->
-      Maybe (ProvidedParameters (TypeOrGroup CTreePhase), Maybe CBORGenerator) ->
-      Maybe (ProvidedParameters (TypeOrGroup CTreePhase), Maybe CBORGenerator)
-    extend tog _gps (Just (existing, gen)) = case (underlying existing, tog) of
+      Maybe CDDLMapEntry ->
+      Maybe CDDLMapEntry
+    extend tog _gps (Just cme) = case (underlying $ cmeProvidedParameters cme, tog) of
       (TOGType _, TOGType (Type0 new)) ->
         Just $
-          ( existing
-              & field @"underlying"
-              % _Ctor @"TOGType"
-              % _Ctor @"Type0"
-              %~ (<> new)
-          , gen
-          )
+          cme
+            & #cmeProvidedParameters
+            % field @"underlying"
+            % _Ctor @"TOGType"
+            % _Ctor @"Type0"
+            %~ (<> new)
       -- From the CDDL spec, I don't see how one is meant to extend a group.
       -- According to the description, it's meant to add a group choice, but the
       -- assignment to a group takes a 'GrpEntry', not a Group, and there is no
       -- ability to add a choice. For now, we simply ignore attempt at
       -- extension.
-      (TOGGroup _, TOGGroup _new) -> Just (existing, gen)
+      (TOGGroup _, TOGGroup _new) -> Just cme
       (TOGType _, _) -> error "Attempting to extend a type with a group"
       (TOGGroup _, _) -> error "Attempting to extend a group with a type"
-    extend tog gps Nothing = Just (toParametrised tog gps, Nothing)
+    extend tog gps Nothing =
+      Just $ CDDLMapEntry (toParametrised tog gps) Nothing Nothing
 
 --------------------------------------------------------------------------------
 -- 2. Conversion to CTree
@@ -149,29 +159,48 @@
   = -- | Reference to another node with possible generic arguments supplied
     OrRef Name [CTree OrReferenced]
   | OGenerator CBORGenerator (CTree OrReferenced)
+  | OValidator CBORValidator (CTree OrReferenced)
 
-type data OrReferencedDropGen
+type data OrReferencedSimple
 
-data instance XXCTree OrReferencedDropGen = DGOrRef Name [CTree OrReferencedDropGen]
+data instance XXCTree OrReferencedSimple = DGOrRef Name [CTree OrReferencedSimple]
   deriving (Eq, Show)
 
-instance IndexMappable CTree OrReferenced OrReferencedDropGen where
+instance IndexMappable CTree OrReferenced OrReferencedSimple where
   mapIndex = foldCTree mapExt mapIndex
     where
       mapExt (OrRef n xs) = CTreeE . DGOrRef n $ mapIndex <$> xs
       mapExt (OGenerator _ x) = mapIndex x
+      mapExt (OValidator _ x) = mapIndex x
 
+instance IndexMappable CTree MonoReferenced GenPhase where
+  mapIndex = foldCTree mapExt mapIndex
+    where
+      mapExt (MRuleRef n) = CTreeE $ GenRef n
+      mapExt (MGenerator g x) = CTreeE . GenGenerator g $ mapIndex x
+      mapExt (MValidator _ x) = mapIndex x
+
+instance IndexMappable CTreeRoot MonoReferenced GenPhase where
+  mapIndex (CTreeRoot m) = CTreeRoot $ mapIndex <$> m
+
 -- | Build a CTree incorporating references.
 --
 -- This translation cannot fail.
 buildRefCTree :: CDDLMap -> PartialCTreeRoot OrReferenced
-buildRefCTree rules = PartialCTreeRoot $ uncurry toCTreeRule <$> rules
+buildRefCTree rules = PartialCTreeRoot $ toCTreeRule <$> rules
   where
-    toCTreeRule ::
-      ProvidedParameters (TypeOrGroup CTreePhase) ->
-      Maybe CBORGenerator ->
-      ProvidedParameters (CTree OrReferenced)
-    toCTreeRule params gen = fmap (maybe id (\g x -> CTreeE $ OGenerator g x) gen . toCTreeTOG) params
+    toCTreeRule :: CDDLMapEntry -> ProvidedParameters (CTree OrReferenced)
+    toCTreeRule CDDLMapEntry {..} =
+      fmap
+        (applyValidator . applyGenerator . toCTreeTOG)
+        cmeProvidedParameters
+      where
+        applyGenerator = case cmeCustomGenerator of
+          Just g -> CTreeE . OGenerator g
+          Nothing -> id
+        applyValidator = case cmeCustomValidator of
+          Just v -> CTreeE . OValidator v
+          Nothing -> id
 
     toCTreeTOG :: TypeOrGroup CTreePhase -> CTree OrReferenced
     toCTreeTOG (TOGType t0) = toCTreeT0 t0
@@ -222,7 +251,7 @@
       -- We don't validate numerical items yet
       CTree.Postlude PTAny
     toCTreeT2 T2Any = CTree.Postlude PTAny
-    toCTreeT2 (XXType2 (CTreeXXType2 v)) = absurd v
+    toCTreeT2 (XXType2 v) = case v of {}
 
     toCTreeDataItem 20 =
       CTree.Literal $ Value (VBool False) mempty
@@ -317,7 +346,7 @@
 data NameResolutionFailure
   = UnboundReference Name
   | MismatchingArgs Name [Name]
-  | ArgsToPostlude PTerm [CTree OrReferencedDropGen]
+  | ArgsToPostlude PTerm [CTree OrReferencedSimple]
   deriving (Show, Eq)
 
 postludeBinding :: Map.Map Name PTerm
@@ -351,9 +380,9 @@
 
 data DistRef i
   = -- | Reference to a generic parameter
-    GenericRef (Name)
+    GenericRef Name
   | -- | Reference to a rule definition, possibly with generic arguments
-    RuleRef (Name) [CTree i]
+    RuleRef Name [CTree i]
   deriving (Generic)
 
 deriving instance Eq (CTree.Node i) => Eq (DistRef i)
@@ -365,6 +394,7 @@
 data instance XXCTree DistReferenced
   = DRef (DistRef DistReferenced)
   | DGenerator CBORGenerator (CTree DistReferenced)
+  | DValidator CBORValidator (CTree DistReferenced)
 
 type data DistReferencedNoGen
 
@@ -391,6 +421,7 @@
       Just _ -> Right . CTreeE . DRef $ GenericRef n
       Nothing -> Left $ UnboundReference n
 resolveRef env (OGenerator g x) = CTreeE . DGenerator g <$> resolveCTree env x
+resolveRef env (OValidator v x) = CTreeE . DValidator v <$> resolveCTree env x
 
 resolveCTree ::
   BindingEnv OrReferenced OrReferenced ->
@@ -418,12 +449,28 @@
 data instance XXCTree MonoReferenced
   = MRuleRef Name
   | MGenerator CBORGenerator (CTree MonoReferenced)
+  | MValidator CBORValidator (CTree MonoReferenced)
 
 type MonoEnv = BindingEnv DistReferenced MonoReferenced
 
 -- | We introduce additional bindings in the state
 type MonoState = Map.Map Name (CTree MonoReferenced)
 
+type data MonoSimple
+
+instance IndexMappable CTree MonoReferenced MonoSimple where
+  mapIndex = foldCTree mapExt mapIndex
+    where
+      mapExt (MRuleRef n) = CTreeE $ MSimpleRef n
+      mapExt (MGenerator _ x) = mapIndex x
+      mapExt (MValidator _ x) = mapIndex x
+
+instance IndexMappable CTreeRoot MonoReferenced MonoSimple where
+  mapIndex (CTreeRoot m) = CTreeRoot $ mapIndex <$> m
+
+newtype instance XXCTree MonoSimple = MSimpleRef Name
+  deriving (Generic, Show, Eq)
+
 -- | Monad to run the monomorphisation process. We need some additional
 -- capabilities for this, so 'Either' doesn't fully cut it anymore.
 newtype MonoM a = MonoM
@@ -526,6 +573,7 @@
     Just node -> pure node
     Nothing -> throwNR $ UnboundReference n
 resolveGenericRef (DGenerator g x) = CTreeE . MGenerator g <$> resolveGenericCTree x
+resolveGenericRef (DValidator v x) = CTreeE . MValidator v <$> resolveGenericCTree x
 
 resolveGenericCTree ::
   CTree DistReferenced ->
@@ -570,6 +618,7 @@
     where
       mapExt (DRef x) = CTreeE . DHRef $ mapIndex x
       mapExt (DGenerator _ x) = mapIndex x
+      mapExt (DValidator _ x) = mapIndex x
 
 instance IndexMappable DistRef DistReferenced DistReferencedNoGen where
   mapIndex (GenericRef n) = GenericRef n
diff --git a/src/Codec/CBOR/Cuddle/Huddle.hs b/src/Codec/CBOR/Cuddle/Huddle.hs
--- a/src/Codec/CBOR/Cuddle/Huddle.hs
+++ b/src/Codec/CBOR/Cuddle/Huddle.hs
@@ -92,7 +92,11 @@
 
   -- * Generators
   withGenerator,
+  withAntiGen,
 
+  -- * Validators
+  withValidator,
+
   -- * Name
   HasName (..),
 
@@ -106,10 +110,20 @@
 
 import Codec.CBOR.Cuddle.CDDL (CDDL, GenericParameter (..), HasName (..), Name (..), XRule)
 import Codec.CBOR.Cuddle.CDDL qualified as C
-import Codec.CBOR.Cuddle.CDDL.CBORGenerator (CBORGenerator (..), HasGenerator (..), WrappedTerm)
+import Codec.CBOR.Cuddle.CDDL.CBORGenerator (
+  CBORGenerator (..),
+  CBORValidator (..),
+  CustomValidatorResult,
+  GenPhase,
+  HasGenerator (..),
+  HasValidator (..),
+  WrappedTerm,
+ )
+import Codec.CBOR.Cuddle.CDDL.CTree (CTreeRoot)
 import Codec.CBOR.Cuddle.CDDL.CtlOp qualified as CtlOp
 import Codec.CBOR.Cuddle.Comments (Comment (..), HasComment (..))
 import Codec.CBOR.Cuddle.Comments qualified as C
+import Codec.CBOR.Term (Term)
 import Control.Monad (when)
 import Control.Monad.State (MonadState (get), State, execState, modify)
 import Data.ByteString (ByteString)
@@ -131,7 +145,9 @@
 import GHC.Generics (Generic)
 import Optics.Core (lens, view, (%), (%~), (&))
 import Optics.Core qualified as L
-import System.Random.Stateful (StatefulGen)
+import Test.AntiGen (AntiGen)
+import Test.QuickCheck (Gen)
+import Test.QuickCheck.GenT (MonadGen (liftGen))
 import Prelude hiding ((/))
 
 type data HuddleStage
@@ -145,12 +161,19 @@
 data instance C.XRule HuddleStage = HuddleXRule
   { hxrComment :: C.Comment
   , hxrGenerator :: Maybe CBORGenerator
+  , hxrValidator :: Maybe CBORValidator
   }
   deriving (Generic)
 
 instance HasComment (C.XRule HuddleStage) where
   commentL = #hxrComment
 
+instance HasValidator (C.XRule HuddleStage) where
+  validatorL = #hxrValidator
+
+instance HasGenerator (C.XRule HuddleStage) where
+  generatorL = #hxrGenerator
+
 instance Default (XRule HuddleStage)
 
 newtype instance C.XXTopLevel HuddleStage = HuddleXXTopLevel C.Comment
@@ -159,39 +182,41 @@
 newtype instance C.XXType2 HuddleStage = HuddleXXType2 Void
   deriving (Generic, Semigroup, Show, Eq)
 
-data Named a = Named
-  { name :: Name
-  , value :: a
-  }
-  deriving (Functor, Generic, Show)
-
 -- | Add a description to a rule or group entry, to be included as a comment.
 comment :: HasComment a => Comment -> a -> a
 comment desc n = n & commentL %~ (<> desc)
 
 data Rule = Rule
-  { ruleDefinition :: Named Type0
+  { ruleName :: Name
+  , ruleDefinition :: Type0
   , ruleExtra :: XRule HuddleStage
   }
   deriving (Generic)
 
 instance HasGenerator Rule where
-  generatorL = #ruleExtra % #hxrGenerator
+  generatorL = #ruleExtra % generatorL
 
 instance HasComment Rule where
-  commentL = #ruleExtra % #hxrComment
+  commentL = #ruleExtra % commentL
 
+instance HasValidator Rule where
+  validatorL = #ruleExtra % validatorL
+
 instance HasName Rule where
-  getName = getName . ruleDefinition
+  getName = ruleName
 
-data GroupDef = GroupDef {gdNamed :: Named Group, gdExt :: XRule HuddleStage}
+data GroupDef = GroupDef
+  { gdName :: Name
+  , gdDefinition :: Group
+  , gdExt :: XRule HuddleStage
+  }
   deriving (Generic)
 
 instance HasComment GroupDef where
   commentL = #gdExt % commentL
 
 instance HasName GroupDef where
-  getName = getName . gdNamed
+  getName = gdName
 
 data HuddleItem
   = HIRule Rule
@@ -212,7 +237,7 @@
 -- definition from the `Huddle` value on the left.
 huddleAugment :: Huddle -> Huddle -> Huddle
 huddleAugment (Huddle rootsL itemsL) (Huddle rootsR itemsR) =
-  Huddle (L.nubBy ((==) `on` name . ruleDefinition) $ rootsL <> rootsR) (itemsL |<> itemsR)
+  Huddle (L.nubBy ((==) `on` ruleName) $ rootsL <> rootsR) (itemsL |<> itemsR)
 
 -- | This semigroup instance:
 --   - Takes takes the roots from the RHS unless they are empty, in which case
@@ -237,8 +262,8 @@
 instance IsList Huddle where
   type Item Huddle = Rule
   fromList [] = Huddle mempty OMap.empty
-  fromList (r@(Rule x _) : xs) =
-    (#items %~ (OMap.|> (getName x, HIRule r))) $ fromList xs
+  fromList (r@(Rule n _ _) : xs) =
+    (#items %~ (OMap.|> (n, HIRule r))) $ fromList xs
 
   toList = const []
 
@@ -454,11 +479,17 @@
 --------------------------------------------------------------------------------
 
 -- | A reference can be to any type, so we allow it to inhabit all
-type AnyRef a = Named Type0
+data AnyRef = AnyRef
+  { arName :: Name
+  , arDefinition :: Type0
+  }
 
+instance HasName AnyRef where
+  getName = arName
+
 data Constrainable a
   = CValue (Value a)
-  | CRef (AnyRef a)
+  | CRef AnyRef
   | CGRef GRef
 
 -- | Uninhabited type used as marker for the type of thing a CRef sizes
@@ -484,7 +515,7 @@
 class IsConstrainable a x | a -> x where
   toConstrainable :: a -> Constrainable x
 
-instance IsConstrainable (AnyRef a) CRefType where
+instance IsConstrainable AnyRef CRefType where
   toConstrainable = CRef
 
 instance IsConstrainable (Value a) a where
@@ -576,11 +607,11 @@
 
 class IsCborable a
 instance IsCborable ByteString
-instance IsCborable (AnyRef a)
+instance IsCborable AnyRef
 instance IsCborable GRef
 
 cbor :: (IsCborable b, IsConstrainable c b) => c -> Rule -> Constrained
-cbor v r@(Rule (Named n _) _) =
+cbor v r@(Rule n _ _) =
   Constrained
     (toConstrainable v)
     ValueConstraint
@@ -595,7 +626,7 @@
 
 class IsComparable a
 instance IsComparable Int
-instance IsComparable (AnyRef a)
+instance IsComparable AnyRef
 instance IsComparable GRef
 
 le :: (IsComparable a, IsConstrainable c a) => c -> Word64 -> Constrained
@@ -616,7 +647,7 @@
 
 data RangeBound
   = RangeBoundLiteral Literal
-  | RangeBoundRef (Named Type0)
+  | RangeBoundRef Name Type0
 
 class IsRangeBound a where
   toRangeBound :: a -> RangeBound
@@ -627,11 +658,8 @@
 instance IsRangeBound Integer where
   toRangeBound = RangeBoundLiteral . inferInteger
 
-instance IsRangeBound (Named Type0) where
-  toRangeBound = RangeBoundRef
-
 instance IsRangeBound Rule where
-  toRangeBound (Rule x _) = toRangeBound x
+  toRangeBound (Rule n x _) = RangeBoundRef n x
 
 data Ranged where
   Ranged ::
@@ -655,6 +683,9 @@
 class IsType0 a where
   toType0 :: a -> Type0
 
+instance IsType0 Type0 where
+  toType0 = id
+
 instance IsType0 Rule where
   toType0 = Type0 . NoChoice . T2Ref
 
@@ -786,12 +817,12 @@
 
 -- | Assign a rule
 (=:=) :: IsType0 a => Name -> a -> Rule
-n =:= b = Rule (Named n (toType0 b)) def
+n =:= b = Rule n (toType0 b) def
 
 infixl 1 =:=
 
 (=:~) :: Name -> Group -> GroupDef
-n =:~ b = GroupDef (Named n b) def
+n =:~ b = GroupDef n b def
 
 infixl 1 =:~
 
@@ -986,17 +1017,19 @@
   }
 
 data GRuleCall = GRuleCall
-  { grcBody :: Named (GRule Type2)
+  { grcName :: Name
+  , grcBody :: GRule Type2
   , grcExtra :: XRule HuddleStage
   }
 
 data GRuleDef = GRuleDef
-  { grdBody :: Named (GRule GRef)
+  { grdName :: Name
+  , grdBody :: GRule GRef
   , grdExtra :: XRule HuddleStage
   }
 
 instance HasName GRuleDef where
-  getName = getName . grdBody
+  getName = grdName
 
 callToDef :: GRule Type2 -> GRule GRef
 callToDef gr = gr {args = refs}
@@ -1014,13 +1047,11 @@
 binding :: IsType0 t0 => (GRef -> Rule) -> t0 -> GRuleCall
 binding fRule t0 =
   GRuleCall
-    ( Named
-        (name ruleDefinition)
-        GRule
-          { args = t2 NE.:| []
-          , body = getField @"value" ruleDefinition
-          }
-    )
+    ruleName
+    GRule
+      { args = t2 NE.:| []
+      , body = ruleDefinition
+      }
     ruleExtra
   where
     Rule {..} = fRule (freshName 0)
@@ -1032,13 +1063,11 @@
 binding2 :: (IsType0 t0, IsType0 t1) => (GRef -> GRef -> Rule) -> t0 -> t1 -> GRuleCall
 binding2 fRule t0 t1 =
   GRuleCall
-    ( Named
-        (name ruleDefinition)
-        GRule
-          { args = t02 NE.:| [t12]
-          , body = getField @"value" ruleDefinition
-          }
-    )
+    ruleName
+    GRule
+      { args = t02 NE.:| [t12]
+      , body = ruleDefinition
+      }
     ruleExtra
   where
     Rule {..} = fRule (freshName 0) (freshName 1)
@@ -1058,9 +1087,9 @@
 hiRule _ = []
 
 instance HasName HuddleItem where
-  getName (HIRule (Rule (Named n _) _)) = n
-  getName (HIGroup (GroupDef (Named n _) _)) = n
-  getName (HIGRule (GRuleDef (Named n _) _)) = n
+  getName (HIRule rule) = getName rule
+  getName (HIGroup group) = getName group
+  getName (HIGRule gRule) = getName gRule
 
 -- | Collect all rules starting from a given point. This will also insert a
 --   single pseudo-rule as the first element which references the specified
@@ -1079,9 +1108,9 @@
         }
     goHuddleItem (HIRule r) = goRule r
     goHuddleItem (HIGroup g) = goNamedGroup g
-    goHuddleItem (HIGRule (GRuleDef (Named _ (GRule _ t0)) _)) = goT0 t0
+    goHuddleItem (HIGRule (GRuleDef _ (GRule _ t0) _)) = goT0 t0
     goRule :: Rule -> State (OMap Name HuddleItem) ()
-    goRule r@(Rule (Named n t0) _) = do
+    goRule r@(Rule n t0 _) = do
       items <- get
       when (OMap.notMember n items) $ do
         modify (OMap.|> (n, HIRule r))
@@ -1089,15 +1118,15 @@
     goChoice f (NoChoice x) = f x
     goChoice f (ChoiceOf x xs) = f x >> goChoice f xs
     goT0 = goChoice goT2 . unType0
-    goNamedGroup gd@(GroupDef (Named n g) _) = do
+    goNamedGroup gd@(GroupDef n g _) = do
       items <- get
       when (OMap.notMember n items) $ do
         modify (OMap.|> (n, HIGroup gd))
         goGroup g
-    goGRule (GRuleCall r@(Named n g) extra) = do
+    goGRule (GRuleCall n g extra) = do
       items <- get
       when (OMap.notMember n items) $ do
-        modify (OMap.|> (n, HIGRule $ GRuleDef (fmap callToDef r) extra))
+        modify (OMap.|> (n, HIGRule $ GRuleDef n (callToDef g) extra))
         goT0 (body g)
       -- Note that the parameters here may be different, so this doesn't live
       -- under the guard
@@ -1112,7 +1141,7 @@
     goT2 (T2Constrained (Constrained c _ refs)) =
       ( case c of
           CValue _ -> pure ()
-          CRef r -> goRule $ Rule r def
+          CRef AnyRef {..} -> goRule $ Rule arName arDefinition def
           CGRef _ -> pure ()
       )
         >> mapM_ goRule refs
@@ -1126,7 +1155,7 @@
     goRanged (Unranged _) = pure ()
     goRanged (Ranged lb ub _) = goRangeBound lb >> goRangeBound ub
     goRangeBound (RangeBoundLiteral _) = pure ()
-    goRangeBound (RangeBoundRef r) = goRule . Rule r $ HuddleXRule mempty Nothing
+    goRangeBound (RangeBoundRef n r) = goRule . Rule n r $ HuddleXRule mempty Nothing Nothing
 
 -- | Same as `collectFrom`, but the rules passed into this function will be put
 --   at the top of the Huddle, and all of their dependencies will be added at
@@ -1196,7 +1225,7 @@
         comment "Pseudo-rule introduced by Cuddle to collect root elements" $
           "huddle_root_defs" =:= arr (fromList (fmap a topRs))
     toCDDLRule :: Rule -> C.Rule HuddleStage
-    toCDDLRule (Rule (Named n (Type0 t0)) extra) =
+    toCDDLRule (Rule n (Type0 t0) extra) =
       ( \x ->
           C.Rule n Nothing C.AssignEq x extra
       )
@@ -1248,8 +1277,8 @@
       T2Array x -> C.Type1 (C.T2Array $ arrayToCDDLGroup x) Nothing mempty
       T2Tagged (Tagged mmin x) ->
         C.Type1 (C.T2Tag mmin $ toCDDLType0 x) Nothing mempty
-      T2Ref (Rule (Named n _) _) -> C.Type1 (C.T2Name n Nothing) Nothing mempty
-      T2Group (GroupDef (Named n _) _) -> C.Type1 (C.T2Name n Nothing) Nothing mempty
+      T2Ref (Rule n _ _) -> C.Type1 (C.T2Name n Nothing) Nothing mempty
+      T2Group (GroupDef n _ _) -> C.Type1 (C.T2Name n Nothing) Nothing mempty
       T2Generic g -> C.Type1 (toGenericCall g) Nothing mempty
       T2GenericRef (GRef n) -> C.Type1 (C.T2Name (C.Name n) Nothing) Nothing mempty
 
@@ -1289,7 +1318,7 @@
 
     toCDDLConstrainable c = case c of
       CValue v -> toCDDLPostlude v
-      CRef r -> name r
+      CRef r -> getName r
       CGRef (GRef n) -> C.Name n
 
     toCDDLRanged :: Ranged -> C.Type1 HuddleStage
@@ -1303,10 +1332,10 @@
 
     toCDDLRangeBound :: RangeBound -> C.Type2 HuddleStage
     toCDDLRangeBound (RangeBoundLiteral l) = C.T2Value $ toCDDLValue l
-    toCDDLRangeBound (RangeBoundRef (Named n _)) = C.T2Name n Nothing
+    toCDDLRangeBound (RangeBoundRef n _) = C.T2Name n Nothing
 
     toCDDLGroupDef :: GroupDef -> C.Rule HuddleStage
-    toCDDLGroupDef (GroupDef (Named n (Group t0s)) extra) =
+    toCDDLGroupDef (GroupDef n (Group t0s) extra) =
       C.Rule
         n
         Nothing
@@ -1324,13 +1353,13 @@
         extra
 
     toGenericCall :: GRuleCall -> C.Type2 HuddleStage
-    toGenericCall (GRuleCall (Named n gr) _) =
+    toGenericCall (GRuleCall n gr _) =
       C.T2Name
         n
         (Just . C.GenericArg $ fmap toCDDLType1 (args gr))
 
     toGenRuleDef :: GRuleDef -> C.Rule HuddleStage
-    toGenRuleDef (GRuleDef (Named n gr) extra) =
+    toGenRuleDef (GRuleDef n gr extra) =
       C.Rule
         n
         (Just gps)
@@ -1345,8 +1374,16 @@
           C.GenericParameters $
             fmap (\(GRef t) -> GenericParameter (C.Name t) $ HuddleXTerm mempty) (args gr)
 
-withGenerator :: HasGenerator a => (forall g m. StatefulGen g m => g -> m WrappedTerm) -> a -> a
-withGenerator f = L.set generatorL (Just $ CBORGenerator f)
+-- | Use a custom `QuickCheck` generator to generate the term. Will override
+-- the generator passed via `withAntiGen`
+withGenerator :: HasGenerator a => (CTreeRoot GenPhase -> Gen WrappedTerm) -> a -> a
+withGenerator f = L.set generatorL (Just . CBORGenerator $ liftGen . f)
 
-instance HasName (Named a) where
-  getName = name
+-- | Use a custom `AntiGen` generator to generate the term. Will override
+-- the custom generator passed via `withGenerator`. The advantage of using
+-- `AntiGen` generator is that it can also be used to generate negative examples.
+withAntiGen :: HasGenerator a => (CTreeRoot GenPhase -> AntiGen WrappedTerm) -> a -> a
+withAntiGen f = L.set generatorL (Just $ CBORGenerator f)
+
+withValidator :: HasValidator a => (Term -> CustomValidatorResult) -> a -> a
+withValidator p = L.set validatorL . Just $ CBORValidator p
diff --git a/src/Codec/CBOR/Cuddle/Huddle/HuddleM.hs b/src/Codec/CBOR/Cuddle/Huddle/HuddleM.hs
deleted file mode 100644
--- a/src/Codec/CBOR/Cuddle/Huddle/HuddleM.hs
+++ /dev/null
@@ -1,106 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-
--- | Monad for declaring Huddle constructs
-module Codec.CBOR.Cuddle.Huddle.HuddleM (
-  module Huddle,
-  (=:=),
-  (=:~),
-  (=::=),
-  binding,
-  setRootRules,
-  huddleDef,
-  huddleDef',
-  include,
-  unsafeIncludeFromHuddle,
-)
-where
-
-import Codec.CBOR.Cuddle.CDDL (Name)
-import Codec.CBOR.Cuddle.Huddle hiding (binding, (=:=), (=:~))
-import Codec.CBOR.Cuddle.Huddle qualified as Huddle
-import Control.Monad.State.Strict (State, modify, runState)
-import Data.Default.Class (def)
-import Data.Generics.Product (HasField (..))
-import Data.Map.Ordered.Strict qualified as OMap
-import Optics.Core (set, (%~), (^.))
-
-type HuddleM = State Huddle
-
--- | Overridden version of assignment which also adds the rule to the state
-(=:=) :: IsType0 a => Name -> a -> HuddleM Rule
-n =:= b = let r = n Huddle.=:= b in include r
-
-infixl 1 =:=
-
--- | Overridden version of group assignment which adds the rule to the state
-(=:~) :: Name -> Group -> HuddleM GroupDef
-n =:~ b = let r = n Huddle.=:~ b in include r
-
-infixl 1 =:~
-
-binding ::
-  forall t0.
-  IsType0 t0 =>
-  (GRef -> Rule) ->
-  HuddleM (t0 -> GRuleCall)
-binding fRule = include (Huddle.binding fRule)
-
--- | Renamed version of Huddle's underlying '=:=' for use in generic bindings
-(=::=) :: IsType0 a => Name -> a -> Rule
-n =::= b = n Huddle.=:= b
-
-infixl 1 =::=
-
-setRootRules :: [Rule] -> HuddleM ()
-setRootRules = modify . set (field @"roots")
-
-huddleDef :: HuddleM a -> Huddle
-huddleDef = snd . huddleDef'
-
-huddleDef' :: HuddleM a -> (a, Huddle)
-huddleDef' mh = runState mh def
-
-class Includable a where
-  -- | Include a rule, group, or generic rule defined elsewhere
-  include :: a -> HuddleM a
-
-instance Includable Rule where
-  include r@(Rule x _) =
-    modify (field @"items" %~ (OMap.|> (getName x, HIRule r)))
-      >> pure r
-
-instance Includable GroupDef where
-  include r =
-    modify
-      ( (field @"items")
-          %~ (OMap.|> (getName r, HIGroup r))
-      )
-      >> pure r
-
-instance IsType0 t0 => Includable (t0 -> GRuleCall) where
-  include gr =
-    let fakeT0 = error "Attempting to unwrap fake value in generic call"
-        GRuleCall g extra = gr fakeT0
-        grDef = callToDef <$> g
-        n = getName grDef
-     in do
-          modify (field @"items" %~ (OMap.|> (n, HIGRule $ GRuleDef grDef extra)))
-          pure gr
-
-instance Includable HuddleItem where
-  include x@(HIRule r) = include r >> pure x
-  include x@(HIGroup g) = include g >> pure x
-  include x@(HIGRule g) =
-    do
-      modify (field @"items" %~ (OMap.|> (getName g, x)))
-      pure x
-
-unsafeIncludeFromHuddle ::
-  Huddle ->
-  Name ->
-  HuddleM HuddleItem
-unsafeIncludeFromHuddle h name =
-  let items = h ^. field @"items"
-   in case OMap.lookup name items of
-        Just v -> include v
-        Nothing -> error $ show name <> " was not found in Huddle spec"
diff --git a/src/Codec/CBOR/Cuddle/IndexMappable.hs b/src/Codec/CBOR/Cuddle/IndexMappable.hs
--- a/src/Codec/CBOR/Cuddle/IndexMappable.hs
+++ b/src/Codec/CBOR/Cuddle/IndexMappable.hs
@@ -24,12 +24,11 @@
   XXTopLevel,
   XXType2,
  )
-import Codec.CBOR.Cuddle.CDDL.CTree (
+import Codec.CBOR.Cuddle.CDDL.CTreePhase (
   CTreePhase,
   XCddl (..),
   XRule (..),
   XTerm (..),
-  XXType2 (..),
  )
 import Codec.CBOR.Cuddle.Huddle (
   HuddleStage,
@@ -225,13 +224,13 @@
   mapIndex _ = CTreeXCddl
 
 instance IndexMappable XXType2 ParserStage CTreePhase where
-  mapIndex (ParserXXType2 c) = CTreeXXType2 c
+  mapIndex (ParserXXType2 c) = case c of {}
 
 instance IndexMappable XTerm ParserStage CTreePhase where
   mapIndex _ = CTreeXTerm
 
 instance IndexMappable XRule ParserStage CTreePhase where
-  mapIndex _ = CTreeXRule Nothing
+  mapIndex _ = CTreeXRule Nothing Nothing
 
 -- ParserStage -> HuddleStage
 
@@ -253,13 +252,13 @@
   mapIndex _ = CTreeXCddl
 
 instance IndexMappable XXType2 HuddleStage CTreePhase where
-  mapIndex (HuddleXXType2 c) = CTreeXXType2 c
+  mapIndex (HuddleXXType2 c) = case c of {}
 
 instance IndexMappable XTerm HuddleStage CTreePhase where
   mapIndex _ = CTreeXTerm
 
 instance IndexMappable XRule HuddleStage CTreePhase where
-  mapIndex (HuddleXRule _ g) = CTreeXRule g
+  mapIndex (HuddleXRule _ g v) = CTreeXRule g v
 
 -- HuddleStage -> PrettyStage
 
@@ -276,7 +275,7 @@
   mapIndex (HuddleXTerm c) = PrettyXTerm c
 
 instance IndexMappable XRule HuddleStage PrettyStage where
-  mapIndex (HuddleXRule c _) = PrettyXRule c
+  mapIndex (HuddleXRule c _ _) = PrettyXRule c
 
 -- ParserStage -> ParserStage
 
diff --git a/src/Codec/CBOR/Cuddle/Parser.hs b/src/Codec/CBOR/Cuddle/Parser.hs
--- a/src/Codec/CBOR/Cuddle/Parser.hs
+++ b/src/Codec/CBOR/Cuddle/Parser.hs
@@ -300,10 +300,10 @@
     pInt =
       pSignedNum L.decimal >>= \case
         (False, val)
-          | val < fromIntegral (maxBound @Word64) -> pure . VUInt $ fromIntegral val
+          | val <= fromIntegral (maxBound @Word64) -> pure . VUInt $ fromIntegral val
           | otherwise -> pure $ VBignum val
         (True, val)
-          | val < fromIntegral (maxBound @Word64) -> pure . VNInt $ fromIntegral val
+          | val <= fromIntegral (maxBound @Word64) -> pure . VNInt $ fromIntegral val
           | otherwise -> pure . VBignum $ -val
     pFloat =
       pSignedNum L.float >>= \case
diff --git a/src/Codec/CBOR/Cuddle/Pretty.hs b/src/Codec/CBOR/Cuddle/Pretty.hs
--- a/src/Codec/CBOR/Cuddle/Pretty.hs
+++ b/src/Codec/CBOR/Cuddle/Pretty.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeData #-}
@@ -17,6 +18,7 @@
 ) where
 
 import Codec.CBOR.Cuddle.CDDL
+import Codec.CBOR.Cuddle.CDDL.CTree (PTerm (..))
 import Codec.CBOR.Cuddle.CDDL.CtlOp (CtlOp)
 import Codec.CBOR.Cuddle.Comments (CollectComments (..), Comment (..), HasComment (..), unComment)
 import Codec.CBOR.Cuddle.Pretty.Columnar (
@@ -256,3 +258,18 @@
   pretty (VBytes b) = fromString $ "h" <> "'" <> BS.unpack (B16.encode b) <> "'"
   pretty (VBool True) = "true"
   pretty (VBool False) = "false"
+
+instance Pretty PTerm where
+  pretty = \case
+    PTBool -> "bool"
+    PTUInt -> "uint"
+    PTNInt -> "nint"
+    PTInt -> "int"
+    PTHalf -> "half"
+    PTFloat -> "float"
+    PTDouble -> "double"
+    PTBytes -> "bytes"
+    PTText -> "text"
+    PTAny -> "any"
+    PTNil -> "nil"
+    PTUndefined -> "undefined"
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -5,6 +5,7 @@
 import Test.Codec.CBOR.Cuddle.CDDL.GeneratorSpec qualified as Generator
 import Test.Codec.CBOR.Cuddle.CDDL.Parser (parserSpec)
 import Test.Codec.CBOR.Cuddle.CDDL.Validator qualified as Validator
+import Test.Codec.CBOR.Cuddle.CDDL.Validator.Golden qualified as ValidatorGolden
 import Test.Codec.CBOR.Cuddle.Huddle (huddleSpec)
 import Test.Hspec
 import Test.Hspec.Runner
@@ -24,4 +25,6 @@
     describe "Huddle" huddleSpec
     describe "Examples" Examples.spec
     describe "Generator" Generator.spec
-    describe "Validator" Validator.spec
+    describe "Validator" $ do
+      describe "Properties" Validator.spec
+      describe "Golden" ValidatorGolden.spec
diff --git a/test/Test/Codec/CBOR/Cuddle/CDDL/Examples/Huddle.hs b/test/Test/Codec/CBOR/Cuddle/CDDL/Examples/Huddle.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Codec/CBOR/Cuddle/CDDL/Examples/Huddle.hs
@@ -0,0 +1,179 @@
+{-# LANGUAGE OverloadedLists #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Test.Codec.CBOR.Cuddle.CDDL.Examples.Huddle (
+  huddleRangeArray,
+  huddleArray,
+  huddleMap,
+  huddleRangeMap,
+  simpleRule,
+  simpleTermExample,
+  refTermExample,
+  bytesExample,
+  opCertExample,
+  sizeTextExample,
+  sizeBytesExample,
+  rangeListExample,
+  rangeMapExample,
+  optionalMapExample,
+  choicesExample,
+) where
+
+import Codec.CBOR.Cuddle.CDDL (Name)
+import Codec.CBOR.Cuddle.CDDL.CBORGenerator (WrappedTerm (..))
+import Codec.CBOR.Cuddle.Huddle (
+  CanQuantify (..),
+  Huddle,
+  HuddleItem (..),
+  Rule,
+  Value (..),
+  a,
+  arr,
+  asKey,
+  collectFrom,
+  idx,
+  mp,
+  opt,
+  sized,
+  withGenerator,
+  (...),
+  (=:=),
+  (==>),
+ )
+import Codec.CBOR.Cuddle.Huddle qualified as H
+import Codec.CBOR.Term qualified as C
+import Data.Word (Word64)
+import Test.QuickCheck.Gen (choose)
+
+huddleRangeArray :: Huddle
+huddleRangeArray =
+  collectFrom
+    [ HIRule $
+        "a"
+          =:= arr
+            [ opt $ a VInt
+            , 2 <+ a VInt +> 3
+            , a VBool +> 3
+            , 3 <+ a VText
+            ]
+    ]
+
+huddleArray :: Huddle
+huddleArray =
+  collectFrom
+    [ HIRule $
+        "a"
+          =:= arr
+            [ 0 <+ a VBool
+            , 1 <+ a VInt
+            , opt $ a VText
+            , a VUInt
+            ]
+    ]
+
+huddleMap :: Huddle
+huddleMap =
+  collectFrom
+    [ HIRule $
+        "a"
+          =:= mp
+            [ idx 1 ==> arr [0 <+ a VUInt]
+            , 1 <+ asKey VBytes ==> VAny
+            , opt $ idx 2 ==> VBool
+            , 0 <+ asKey VText ==> VInt
+            ]
+    ]
+
+huddleRangeMap :: Huddle
+huddleRangeMap =
+  collectFrom
+    [ HIRule $
+        "a"
+          =:= mp
+            [ 5 <+ asKey VInt ==> VBool +> 10
+            ]
+    ]
+
+simpleRule :: Name -> Rule
+simpleRule n = withGenerator (\_ -> S . C.TInt <$> choose (4, 6)) $ n =:= arr [1, 2, 3]
+
+simpleTermExample :: Huddle
+simpleTermExample =
+  collectFrom
+    [ HIRule $ simpleRule "root"
+    ]
+
+refTermExample :: Huddle
+refTermExample =
+  collectFrom
+    [ HIRule $ "root" =:= arr [0, a $ simpleRule "bar"]
+    ]
+
+bytesExample :: Huddle
+bytesExample =
+  collectFrom
+    [ HIRule $ "root" =:= H.bstr "010203ff"
+    ]
+
+opCertExample :: Huddle
+opCertExample =
+  collectFrom
+    [ HIRule $
+        "root"
+          =:= arr
+            [ a (VBytes `sized` (32 :: Word64))
+            , a VUInt
+            , a VUInt
+            , a (VBytes `sized` (64 :: Word64))
+            ]
+    ]
+
+sizeTextExample :: Huddle
+sizeTextExample =
+  collectFrom
+    [HIRule $ "root" =:= VText `sized` (0 :: Word64, 32 :: Word64)]
+
+sizeBytesExample :: Huddle
+sizeBytesExample =
+  collectFrom
+    [HIRule $ "root" =:= VBytes `sized` (0 :: Word64, 32 :: Word64)]
+
+rangeListExample :: Huddle
+rangeListExample =
+  collectFrom
+    [ HIRule $
+        "root"
+          =:= arr
+            [ 3 <+ a VInt +> 7
+            ]
+    ]
+
+rangeMapExample :: Huddle
+rangeMapExample =
+  collectFrom
+    [ HIRule $
+        "root"
+          =:= mp
+            [ 3 <+ asKey VInt ==> VBool +> 7
+            ]
+    ]
+
+optionalMapExample :: Huddle
+optionalMapExample =
+  collectFrom
+    [ HIRule $
+        "root"
+          =:= mp
+            [ 10 <+ asKey ((0 :: Integer) ... (10 :: Integer)) ==> VBool
+            ]
+    ]
+
+choicesExample :: Huddle
+choicesExample =
+  collectFrom
+    [ HIRule $
+        "root"
+          =:= arr [1, a VInt, 3]
+          H./ arr [1, a VBool, 6]
+          H./ arr [1, a VText]
+    ]
diff --git a/test/Test/Codec/CBOR/Cuddle/CDDL/GeneratorSpec.hs b/test/Test/Codec/CBOR/Cuddle/CDDL/GeneratorSpec.hs
--- a/test/Test/Codec/CBOR/Cuddle/CDDL/GeneratorSpec.hs
+++ b/test/Test/Codec/CBOR/Cuddle/CDDL/GeneratorSpec.hs
@@ -1,66 +1,97 @@
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedStrings #-}
 
 module Test.Codec.CBOR.Cuddle.CDDL.GeneratorSpec (spec) where
 
-import Codec.CBOR.Cuddle.CBOR.Gen (generateCBORTerm)
-import Codec.CBOR.Cuddle.CDDL.CBORGenerator (WrappedTerm (..))
-import Codec.CBOR.Cuddle.CDDL.Resolve (fullResolveCDDL)
-import Codec.CBOR.Cuddle.Huddle (
-  Huddle,
-  HuddleItem (..),
-  a,
-  arr,
-  collectFrom,
-  toCDDL,
-  withGenerator,
-  (=:=),
+import Codec.CBOR.Cuddle.CBOR.Gen (GenPhase, generateFromName)
+import Codec.CBOR.Cuddle.CBOR.Validator (validateCBOR)
+import Codec.CBOR.Cuddle.CDDL (Name)
+import Codec.CBOR.Cuddle.CDDL.CTree (CTreeRoot (..))
+import Codec.CBOR.Cuddle.CDDL.Resolve (MonoReferenced, MonoSimple, fullResolveCDDL)
+import Codec.CBOR.Cuddle.Huddle (Huddle, toCDDL)
+import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..), mapCDDLDropExt)
+import Codec.CBOR.Pretty (prettyHexEnc)
+import Codec.CBOR.Read (deserialiseFromBytes)
+import Codec.CBOR.Term (Term (..), decodeTerm, encodeTerm)
+import Codec.CBOR.Write (toStrictByteString)
+import Data.ByteString.Lazy qualified as LBS
+import Data.Text.Lazy qualified as TL
+import Test.AntiGen (runAntiGen, zapAntiGen)
+import Test.Codec.CBOR.Cuddle.CDDL.Examples.Huddle (
+  bytesExample,
+  opCertExample,
+  optionalMapExample,
+  rangeListExample,
+  rangeMapExample,
+  refTermExample,
+  simpleTermExample,
+  sizeBytesExample,
+  sizeTextExample,
  )
-import Codec.CBOR.Cuddle.Huddle qualified as H
-import Codec.CBOR.Cuddle.IndexMappable (mapCDDLDropExt)
-import Codec.CBOR.Term (Term)
-import Codec.CBOR.Term qualified as C
-import System.Random (mkStdGen)
-import System.Random.Stateful (UniformRange (..))
-import Test.Hspec (Expectation, Spec, describe, it, shouldBe)
-
-foo :: H.Rule
-foo = withGenerator (fmap (S . C.TInt) . uniformRM (4, 6)) $ "foo" =:= arr [1, 2, 3]
+import Test.Codec.CBOR.Cuddle.CDDL.Validator (expectInvalid)
+import Test.Hspec (HasCallStack, Spec, describe, runIO, shouldBe, shouldSatisfy)
+import Test.Hspec.Core.Spec (SpecM)
+import Test.Hspec.QuickCheck (prop)
+import Test.QuickCheck (Gen, Property, Testable (..), counterexample)
+import Text.Pretty.Simple (pShow)
 
-simpleTermExample :: Huddle
-simpleTermExample =
-  collectFrom
-    [ HIRule foo
-    ]
+generateCDDL :: CTreeRoot GenPhase -> Gen Term
+generateCDDL cddl = runAntiGen $ generateFromName cddl "root"
 
-refTermExample :: Huddle
-refTermExample =
-  collectFrom
-    [ HIRule foo
-    , HIRule $ "bar" =:= arr [0, a foo]
-    ]
+tryResolveHuddle :: HasCallStack => Huddle -> SpecM () (CTreeRoot MonoReferenced)
+tryResolveHuddle huddle = do
+  case fullResolveCDDL . mapCDDLDropExt $ toCDDL huddle of
+    Right x -> pure x
+    Left err -> runIO . fail $ "Failed to resolve CDDL:\n" <> show err
 
-bytesExample :: Huddle
-bytesExample =
-  collectFrom
-    [ HIRule $ "foo" =:= H.bstr "010203ff"
-    ]
+expectZapInvalidates :: CTreeRoot MonoReferenced -> Name -> Property
+expectZapInvalidates cddl name = property $ do
+  value <- zapAntiGen 1 $ generateFromName (mapIndex cddl) name
+  let
+    bs = toStrictByteString $ encodeTerm value
+    validationRes = validateCBOR bs name $ mapIndex cddl
+    failMsg = case deserialiseFromBytes decodeTerm (LBS.fromStrict bs) of
+      Right (_, t) -> prettyHexEnc (encodeTerm t)
+      Left _ -> mempty
+  pure . counterexample failMsg $ expectInvalid validationRes
 
-huddleShouldGenerate :: Huddle -> Term -> Expectation
-huddleShouldGenerate huddle term = do
-  let g = mkStdGen 12345
-  ct <- case fullResolveCDDL . mapCDDLDropExt $ toCDDL huddle of
-    Right x -> pure x
-    Left err -> fail $ "Failed to resolve CDDL: " <> show err
-  generateCBORTerm ct "foo" g `shouldBe` term
+zapInvalidatesHuddle :: String -> Huddle -> Spec
+zapInvalidatesHuddle n huddle = do
+  cddl <- tryResolveHuddle huddle
+  prop n . counterexample (TL.unpack . pShow $ mapIndex @_ @_ @MonoSimple cddl) $
+    expectZapInvalidates cddl "root"
 
 spec :: Spec
 spec = do
+  describe "Negative generator" $ do
+    describe "Zapped value fails to validate" $ do
+      zapInvalidatesHuddle "simpleTerm" simpleTermExample
+      zapInvalidatesHuddle "refTerm" refTermExample
+      zapInvalidatesHuddle "opCert" opCertExample
+      zapInvalidatesHuddle "sizeText" sizeTextExample
+      zapInvalidatesHuddle "sizeBytes" sizeBytesExample
+      zapInvalidatesHuddle "rangeList" rangeListExample
+      zapInvalidatesHuddle "rangeMap" rangeMapExample
+      zapInvalidatesHuddle "optionalMapExample" optionalMapExample
+
   describe "Custom generators" $ do
     describe "Huddle" $ do
-      it "If a term has a custom generator then it is used" $
-        simpleTermExample `huddleShouldGenerate` C.TInt 5
-      it "Custom generator works when called via reference" $
-        refTermExample `huddleShouldGenerate` C.TInt 5
-      it "Bytes are generated correctly" $
-        bytesExample `huddleShouldGenerate` C.TBytes "\x01\x02\x03\xff"
+      simpleTermExampleCddl <- tryResolveHuddle simpleTermExample
+      prop "If a term has a custom generator then it is used" $ do
+        res <- generateCDDL $ mapIndex simpleTermExampleCddl
+        pure $
+          res `shouldSatisfy` \case
+            TInt i -> i > 3 && i < 7
+            _ -> False
+      refTermExampleCddl <- tryResolveHuddle refTermExample
+      prop "Custom generator works when called via reference" $ do
+        res <- generateCDDL $ mapIndex refTermExampleCddl
+        pure $
+          res `shouldSatisfy` \case
+            TList [TInt 0, TInt i] -> i > 3 && i < 7
+            _ -> False
+      bytesExampleCddl <- tryResolveHuddle bytesExample
+      prop "Bytes are generated correctly" $ do
+        res <- generateCDDL $ mapIndex bytesExampleCddl
+        pure $ res `shouldBe` TBytes "\x01\x02\x03\xff"
diff --git a/test/Test/Codec/CBOR/Cuddle/CDDL/Validator.hs b/test/Test/Codec/CBOR/Cuddle/CDDL/Validator.hs
--- a/test/Test/Codec/CBOR/Cuddle/CDDL/Validator.hs
+++ b/test/Test/Codec/CBOR/Cuddle/CDDL/Validator.hs
@@ -1,17 +1,26 @@
-{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Codec.CBOR.Cuddle.CDDL.Validator (spec) where
+module Test.Codec.CBOR.Cuddle.CDDL.Validator (
+  spec,
+  expectValid,
+  expectInvalid,
+) where
 
-import Codec.CBOR.Cuddle.CBOR.Gen (generateCBORTerm)
+import Codec.CBOR.Cuddle.CBOR.Gen (generateFromName)
 import Codec.CBOR.Cuddle.CBOR.Validator (
-  CBORTermResult (..),
-  CDDLResult (..),
-  isCBORTermResultValid,
   validateCBOR,
  )
+import Codec.CBOR.Cuddle.CBOR.Validator.Trace (
+  Evidenced (..),
+  SValidity (..),
+  ValidationTrace,
+  defaultTraceOptions,
+  prettyValidationTrace,
+ )
 import Codec.CBOR.Cuddle.CDDL (Name (..))
+import Codec.CBOR.Cuddle.CDDL.CBORGenerator (CustomValidatorResult (..))
 import Codec.CBOR.Cuddle.CDDL.CTree (CTreeRoot (..))
 import Codec.CBOR.Cuddle.CDDL.CTree qualified as CTree
 import Codec.CBOR.Cuddle.CDDL.Postlude (appendPostlude)
@@ -22,19 +31,15 @@
   Value (..),
   a,
   arr,
-  asKey,
   collectFrom,
-  idx,
-  mp,
-  opt,
+  int,
   toCDDL,
-  (+>),
-  (<+),
+  withValidator,
   (=:=),
-  (==>),
  )
 import Codec.CBOR.Cuddle.IndexMappable (mapCDDLDropExt, mapIndex)
 import Codec.CBOR.Cuddle.Parser (pCDDL)
+import Codec.CBOR.Pretty (prettyHexEnc)
 import Codec.CBOR.Term (Term (..), encodeTerm)
 import Codec.CBOR.Write (toStrictByteString)
 import Control.Monad (forM_)
@@ -49,11 +54,22 @@
 import Data.Text.IO qualified as T
 import Data.Text.Lazy qualified as LT
 import Paths_cuddle (getDataFileName)
+import Prettyprinter (defaultLayoutOptions, layoutPretty)
+import Prettyprinter.Render.Terminal (renderStrict)
+import Test.AntiGen (runAntiGen)
+import Test.Codec.CBOR.Cuddle.CDDL.Examples.Huddle (
+  huddleArray,
+  huddleMap,
+  huddleRangeArray,
+  huddleRangeMap,
+ )
 import Test.Hspec (
+  Expectation,
+  HasCallStack,
   Spec,
   describe,
+  expectationFailure,
   runIO,
-  shouldSatisfy,
  )
 import Test.Hspec.QuickCheck
 import Test.QuickCheck (
@@ -67,15 +83,12 @@
   infiniteListOf,
   listOf,
   listOf1,
-  noShrinking,
   oneof,
   scale,
   shuffle,
   vectorOf,
  )
-import Test.QuickCheck.Random (mkQCGen)
 import Text.Megaparsec (runParser)
-import Text.Pretty.Simple (pShow)
 
 genAndValidateFromFile :: FilePath -> Spec
 genAndValidateFromFile path = do
@@ -89,49 +102,19 @@
         mapCDDLDropExt cddl
     isRule CTree.Group {} = False
     isRule _ = True
-  describe path $
+  describe path $ do
     forM_ (Map.keys $ Map.filter isRule m) $ \name@(Name n) ->
-      prop (T.unpack n) . noShrinking $ \seed -> do
+      prop (T.unpack n) $ do
+        cborTerm <- runAntiGen $ generateFromName (mapIndex resolvedCddl) name
         let
-          gen = mkQCGen seed
-          cborTerm = generateCBORTerm resolvedCddl name gen
           generatedCbor = toStrictByteString $ encodeTerm cborTerm
           res = validateCBOR generatedCbor name (mapIndex resolvedCddl)
           extraInfo =
             unlines
-              [ "Term result:"
-              , LT.unpack $ pShow res
-              , "====="
-              , "CBOR term:"
-              , LT.unpack $ pShow cborTerm
+              [ "CBOR term:"
+              , prettyHexEnc $ encodeTerm cborTerm
               ]
-        counterexample extraInfo $
-          res `shouldSatisfy` \case
-            CBORTermResult _ Valid {} -> True
-            _ -> False
-
-huddleMap :: Huddle
-huddleMap =
-  collectFrom
-    [ HIRule $
-        "a"
-          =:= mp
-            [ idx 1 ==> arr [0 <+ a VUInt]
-            , 1 <+ asKey VBytes ==> VAny
-            , opt $ idx 2 ==> VBool
-            , 0 <+ asKey VText ==> VInt
-            ]
-    ]
-
-huddleRangeMap :: Huddle
-huddleRangeMap =
-  collectFrom
-    [ HIRule $
-        "a"
-          =:= mp
-            [ 5 <+ asKey VInt ==> VBool +> 10
-            ]
-    ]
+        pure . counterexample extraInfo $ expectValid res
 
 genInfiniteUniqueList :: Ord a => Gen a -> Gen [a]
 genInfiniteUniqueList = fmap nubOrd . infiniteListOf
@@ -142,19 +125,6 @@
   let genKV = (,) <$> fmap TInt arbitrary <*> fmap TBool arbitrary
   genMapTerm . take n =<< scale (const $ max lo hi) (genInfiniteUniqueList genKV)
 
-huddleArray :: Huddle
-huddleArray =
-  collectFrom
-    [ HIRule $
-        "a"
-          =:= arr
-            [ 0 <+ a VBool
-            , 1 <+ a VInt
-            , opt $ a VText
-            , a VUInt
-            ]
-    ]
-
 genHuddleArrayRequiredTerms :: Gen [Term]
 genHuddleArrayRequiredTerms = do
   ints <- listOf1 $ TInt <$> arbitrary
@@ -185,19 +155,6 @@
     isNonNegativeInt (TInt x) | x >= 0 = True
     isNonNegativeInt _ = False
 
-huddleRangeArray :: Huddle
-huddleRangeArray =
-  collectFrom
-    [ HIRule $
-        "a"
-          =:= arr
-            [ opt $ a VInt
-            , 2 <+ a VInt +> 3
-            , a VBool +> 3
-            , 3 <+ a VText
-            ]
-    ]
-
 genHuddleRangeArray :: Gen Term
 genHuddleRangeArray = do
   numInts <- choose (3, 4)
@@ -223,9 +180,28 @@
 arbitraryByteString :: Gen ByteString
 arbitraryByteString = BS.pack <$> arbitrary
 
--- TODO make this complete
 arbitraryTerm :: Gen Term
-arbitraryTerm = oneof [TBool <$> arbitrary, TInt <$> arbitrary, TString . T.pack <$> arbitrary]
+arbitraryTerm =
+  oneof
+    [ TInt <$> arbitrary
+    , TInteger <$> arbitrary
+    , TBytes . BS.pack <$> arbitrary
+    , TBytesI . LBS.pack <$> arbitrary
+    , TString . T.pack <$> arbitrary
+    , TStringI . LT.pack <$> arbitrary
+    , TList <$> listOf (scale (`div` 2) arbitraryTerm)
+    , TListI <$> listOf (scale (`div` 2) arbitraryTerm)
+    , TMap <$> listOf (scale (`div` 2) $ (,) <$> arbitraryTerm <*> arbitraryTerm)
+    , TMapI <$> listOf (scale (`div` 2) $ (,) <$> arbitraryTerm <*> arbitraryTerm)
+    , -- TODO properly implement tagged generation
+      -- , TTagged <$> arbitrary <*> arbitraryTerm
+      TBool <$> arbitrary
+    , pure TNull
+    , pure $ TSimple 23 -- TODO add other values once they are supported by cuddle
+    , THalf <$> arbitrary
+    , TFloat <$> arbitrary
+    , TDouble <$> arbitrary
+    ]
 
 genFullMap :: Gen Term
 genFullMap = do
@@ -256,8 +232,13 @@
       , (TBytes "foo", TBytes "bar")
       ]
 
-validateHuddle :: Term -> Huddle -> Name -> CBORTermResult
-validateHuddle term huddle name = do
+validateHuddle ::
+  HasCallStack =>
+  Huddle ->
+  Name ->
+  Term ->
+  Evidenced ValidationTrace
+validateHuddle huddle name term = do
   let
     resolvedCddl = case fullResolveCDDL . mapCDDLDropExt $ toCDDL huddle of
       Right root -> root
@@ -265,6 +246,30 @@
     bs = toStrictByteString $ encodeTerm term
   validateCBOR bs name (mapIndex resolvedCddl)
 
+expectValid :: Evidenced ValidationTrace -> Expectation
+expectValid (Evidenced SValid _) = pure ()
+expectValid (Evidenced SInvalid t) =
+  expectationFailure . T.unpack $
+    "Expected a success, got failure:\n"
+      <> renderStrict (layoutPretty defaultLayoutOptions $ prettyValidationTrace defaultTraceOptions t)
+
+expectInvalid :: Evidenced ValidationTrace -> Expectation
+expectInvalid (Evidenced SValid t) =
+  expectationFailure . T.unpack $
+    "Expected a failure, but got success:\n"
+      <> renderStrict (layoutPretty defaultLayoutOptions $ prettyValidationTrace defaultTraceOptions t)
+expectInvalid _ = pure ()
+
+stringValidator :: Term -> CustomValidatorResult
+stringValidator (TString _) = CustomValidatorSuccess
+stringValidator (TStringI _) = CustomValidatorSuccess
+stringValidator t = CustomValidatorFailure $ "Expected a string, got\n" <> T.pack (show t)
+
+bytesValidator :: Term -> CustomValidatorResult
+bytesValidator (TBytes _) = CustomValidatorSuccess
+bytesValidator (TBytesI _) = CustomValidatorSuccess
+bytesValidator t = CustomValidatorFailure $ "Expected bytes, got\n" <> T.pack (show t)
+
 spec :: Spec
 spec = describe "Validator" $ do
   describe "Generate and validate from file" $ do
@@ -276,33 +281,73 @@
     genAndValidateFromFile "example/cddl-files/shelley.cddl"
     genAndValidateFromFile "example/cddl-files/validator.cddl"
   describe "Term tests" $ do
+    describe "Maps and arrays" $ do
+      describe "Positive" $ do
+        prop "Validates a full map" . forAll genFullMap $
+          expectValid . validateHuddle huddleMap "a"
+        prop "Validates array" . forAll genHuddleArray $
+          expectValid . validateHuddle huddleArray "a"
+        prop "Validates map with correct number of range elements"
+          . forAll (genHuddleRangeMap (5, 10))
+          $ expectValid . validateHuddle huddleRangeMap "a"
+        prop "Validates array with ranges" . forAll genHuddleRangeArray $
+          expectValid . validateHuddle huddleRangeArray "a"
+      describe "Negative" $ do
+        prop "Fails to validate a map with an unexpected index"
+          . forAll genBadMapInvalidIndex
+          $ expectInvalid . validateHuddle huddleMap "a"
+        prop "Fails to validate reversed array" . forAll genBadArrayReversed $
+          expectInvalid . validateHuddle huddleArray "a"
+        prop "Fails to validate array with missing non-negative int at the end"
+          . forAll genBadArrayMissingLastInt
+          $ expectInvalid . validateHuddle huddleArray "a"
+        prop "Fails to validate map with too few range elements"
+          . forAll (genHuddleRangeMap (0, 4))
+          $ expectInvalid . validateHuddle huddleRangeMap "a"
+        prop "Fails to validate map with too many range elements"
+          . forAll (genHuddleRangeMap (11, 20))
+          $ expectInvalid . validateHuddle huddleRangeMap "a"
+
+  describe "Custom validator" $ do
     describe "Positive" $ do
-      prop "Validates a full map" . forAll genFullMap $ \cbor ->
-        validateHuddle cbor huddleMap "a" `shouldSatisfy` isCBORTermResultValid
-      prop "Validates array" . forAll genHuddleArray $ \cbor ->
-        validateHuddle cbor huddleArray "a" `shouldSatisfy` isCBORTermResultValid
-      prop "Validates map with correct number of range elements"
-        . forAll (genHuddleRangeMap (5, 10))
-        $ \cbor ->
-          validateHuddle cbor huddleRangeMap "a" `shouldSatisfy` isCBORTermResultValid
-      prop "Validates array with ranges" . forAll genHuddleRangeArray $ \cbor ->
-        validateHuddle cbor huddleRangeArray "a" `shouldSatisfy` isCBORTermResultValid
+      prop "Validates with custom validator" $ do
+        term <- genStringTerm . T.pack =<< arbitrary
+        num <- arbitrary
+        let
+          huddle =
+            collectFrom
+              [ HIRule . withValidator stringValidator $ "a" =:= int num
+              ]
+        pure . expectValid $ validateHuddle huddle "a" term
+      prop "Validates with custom validator behind a reference" $ do
+        stringTerm <- genStringTerm . T.pack =<< arbitrary
+        arrTerm <- genArrayTerm [stringTerm]
+        num <- arbitrary
+        let
+          ruleA = withValidator stringValidator $ "a" =:= int num
+          huddle =
+            collectFrom
+              [ HIRule ruleA
+              , HIRule $ "b" =:= arr [a ruleA]
+              ]
+        pure . expectValid $ validateHuddle huddle "b" arrTerm
     describe "Negative" $ do
-      prop "Fails to validate a map with an unexpected index"
-        . forAll genBadMapInvalidIndex
-        $ \cbor ->
-          validateHuddle cbor huddleMap "a" `shouldSatisfy` not . isCBORTermResultValid
-      prop "Fails to validate reversed array" . forAll genBadArrayReversed $ \cbor ->
-        validateHuddle cbor huddleArray "a" `shouldSatisfy` not . isCBORTermResultValid
-      prop "Fails to validate array with missing non-negative int at the end"
-        . forAll genBadArrayMissingLastInt
-        $ \cbor ->
-          validateHuddle cbor huddleArray "a" `shouldSatisfy` not . isCBORTermResultValid
-      prop "Fails to validate map with too few range elements"
-        . forAll (genHuddleRangeMap (0, 4))
-        $ \cbor ->
-          validateHuddle cbor huddleRangeMap "a" `shouldSatisfy` not . isCBORTermResultValid
-      prop "Fails to validate map with too many range elements"
-        . forAll (genHuddleRangeMap (11, 20))
-        $ \cbor ->
-          validateHuddle cbor huddleRangeMap "a" `shouldSatisfy` not . isCBORTermResultValid
+      prop "Fails if term is valid against the Huddle, but not the custom validator" $ do
+        stringTerm <- genStringTerm . T.pack =<< arbitrary
+        let
+          huddle =
+            collectFrom
+              [ HIRule . withValidator bytesValidator $ "a" =:= VText
+              ]
+        pure . expectInvalid $ validateHuddle huddle "a" stringTerm
+      prop "Fails if term is valid against the Huddle, but not the custom validator, behind a reference" $ do
+        stringTerm <- genStringTerm . T.pack =<< arbitrary
+        let
+          ruleA = withValidator bytesValidator $ "a" =:= VText
+          ruleB = "b" =:= arr [a ruleA]
+          huddle =
+            collectFrom
+              [ HIRule ruleA
+              , HIRule ruleB
+              ]
+        pure . expectInvalid $ validateHuddle huddle "a" stringTerm
diff --git a/test/Test/Codec/CBOR/Cuddle/CDDL/Validator/Golden.hs b/test/Test/Codec/CBOR/Cuddle/CDDL/Validator/Golden.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Codec/CBOR/Cuddle/CDDL/Validator/Golden.hs
@@ -0,0 +1,104 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Test.Codec.CBOR.Cuddle.CDDL.Validator.Golden (spec) where
+
+import Codec.CBOR.Cuddle.CBOR.Validator (validateCBOR)
+import Codec.CBOR.Cuddle.CBOR.Validator.Trace (
+  defaultTraceOptions,
+  foldEvidenced,
+  prettyValidationTrace,
+ )
+import Codec.CBOR.Cuddle.CDDL (Name)
+import Codec.CBOR.Cuddle.CDDL.Resolve (fullResolveCDDL)
+import Codec.CBOR.Cuddle.Huddle (Huddle, toCDDL)
+import Codec.CBOR.Cuddle.IndexMappable (mapCDDLDropExt, mapIndex)
+import Codec.CBOR.Term (Term (..), encodeTerm)
+import Codec.CBOR.Write qualified as CBOR
+import Control.Monad ((<=<))
+import Data.Either (fromRight)
+import Data.Text qualified as T
+import Data.Text.IO qualified as T
+import Paths_cuddle (getDataFileName)
+import Prettyprinter (defaultLayoutOptions, layoutPretty)
+import Prettyprinter.Render.Terminal qualified as Ansi
+import System.FilePath ((</>))
+import Test.Codec.CBOR.Cuddle.CDDL.Examples.Huddle (
+  choicesExample,
+  huddleRangeArray,
+  refTermExample,
+ )
+import Test.Hspec (Spec, describe, it)
+import Test.Hspec.Golden (Golden (..))
+
+huddleRangeArrayTermTwoStrings :: Term
+huddleRangeArrayTermTwoStrings =
+  TList
+    [ TInt 0
+    , TInt 1
+    , TString "one"
+    , TString "two"
+    ]
+
+refTermTooLong :: Term
+refTermTooLong =
+  TList
+    [ TInt 0
+    , TList
+        [ TInt 1
+        , TInt 2
+        , TInt 3
+        , TInt 4
+        ]
+    ]
+
+choiceAlmostSecond :: Term
+choiceAlmostSecond =
+  TList
+    [ TInt 1
+    , TBool True
+    , TInt 1
+    ]
+
+validatorPrettyGolden :: String -> Huddle -> Name -> Term -> Spec
+validatorPrettyGolden testName huddle n term =
+  it testName $
+    Golden
+      { goldenFile = "golden" </> testName <> ".txt"
+      , readFromFile = T.readFile <=< getDataFileName
+      , writeToFile = \fp txt -> getDataFileName fp >>= (`T.writeFile` txt)
+      , actualFile = Nothing
+      , output = str
+      , encodePretty = T.unpack
+      , failFirstTime = False
+      }
+  where
+    bs = CBOR.toStrictByteString $ encodeTerm term
+    treeRoot =
+      fromRight (error "Failed to resolve CDDL") . fullResolveCDDL . mapCDDLDropExt $
+        toCDDL huddle
+    str =
+      Ansi.renderStrict
+        . layoutPretty defaultLayoutOptions
+        . foldEvidenced (prettyValidationTrace defaultTraceOptions)
+        . validateCBOR bs n
+        $ mapIndex treeRoot
+
+spec :: Spec
+spec = describe "golden" $ do
+  describe "error messages" $ do
+    validatorPrettyGolden
+      "huddleRangeArrayTwoStrings"
+      huddleRangeArray
+      "a"
+      huddleRangeArrayTermTwoStrings
+    validatorPrettyGolden
+      "refTermTooLong"
+      refTermExample
+      "root"
+      refTermTooLong
+    validatorPrettyGolden
+      "choiceAlmostSecond"
+      choicesExample
+      "root"
+      choiceAlmostSecond
diff --git a/test/Test/Codec/CBOR/Cuddle/Huddle.hs b/test/Test/Codec/CBOR/Cuddle/Huddle.hs
--- a/test/Test/Codec/CBOR/Cuddle/Huddle.hs
+++ b/test/Test/Codec/CBOR/Cuddle/Huddle.hs
@@ -48,7 +48,7 @@
   mapIndex (ParserXRule x) = TestXRule x
 
 instance IndexMappable XRule HuddleStage TestStage where
-  mapIndex (HuddleXRule x _) = TestXRule x
+  mapIndex (HuddleXRule x _ _) = TestXRule x
 
 newtype instance XXTopLevel TestStage = TestXXTopLevel Comment
   deriving (Generic, Show, Eq)