From 59babfef1fb5b268c6d4b8b2abbd80ef944e63dc Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 17 Nov 2025 20:16:03 -0800
Subject: [PATCH 1/4] saw-central/Yosys: Specialize functions from MonadIO
 class to IO.

This greatly reduces the number of needed uses of liftIO.
---
 saw-central/src/SAWCentral/Yosys.hs           |  42 ++--
 saw-central/src/SAWCentral/Yosys/Cell.hs      | 218 +++++++++---------
 saw-central/src/SAWCentral/Yosys/IR.hs        |   5 +-
 saw-central/src/SAWCentral/Yosys/Netgraph.hs  |  39 ++--
 saw-central/src/SAWCentral/Yosys/State.hs     |  91 ++++----
 saw-central/src/SAWCentral/Yosys/Theorem.hs   |  55 ++---
 .../src/SAWCentral/Yosys/TransitionSystem.hs  |  37 ++-
 saw-central/src/SAWCentral/Yosys/Utils.hs     |  94 ++++----
 saw-server/src/SAWServer/Yosys.hs             |   4 +-
 9 files changed, 270 insertions(+), 315 deletions(-)

diff --git a/saw-central/src/SAWCentral/Yosys.hs b/saw-central/src/SAWCentral/Yosys.hs
index 1961174271..db01bec9c1 100644
--- a/saw-central/src/SAWCentral/Yosys.hs
+++ b/saw-central/src/SAWCentral/Yosys.hs
@@ -90,10 +90,9 @@ yosysIRModgraph ir =
 
 -- | Given a Yosys IR, construct a map from module names to SAWCore terms alongside SAWCore and Cryptol types
 convertYosysIR ::
-  MonadIO m =>
   SC.SharedContext ->
   YosysIR ->
-  m (Map Text ConvertedModule)
+  IO (Map Text ConvertedModule)
 convertYosysIR sc ir = do
   let mg = yosysIRModgraph ir
   let sorted = reverseTopSort $ mg ^. modgraphGraph
@@ -102,7 +101,7 @@ convertYosysIR sc ir = do
         let (m, nm, _) = mg ^. modgraphNodeFromVertex $ v
         cm <- convertModule sc env m
         _ <- validateTerm sc ("translating the combinational circuit \"" <> nm <> "\"") $ cm ^. convertedModuleTerm
-        n <- liftIO $ Nonce.freshNonce Nonce.globalNonceGenerator
+        n <- Nonce.freshNonce Nonce.globalNonceGenerator
         let frag = Text.pack . show $ Nonce.indexValue n
         let uri = URI.URI
               { URI.uriScheme = URI.mkScheme "yosys"
@@ -112,7 +111,7 @@ convertYosysIR sc ir = do
               , URI.uriFragment = URI.mkFragment frag
               }
         let ni = SC.ImportedName uri [nm]
-        tc <- liftIO $ SC.scDefineConstant sc ni (cm ^. convertedModuleTerm) (cm ^. convertedModuleType)
+        tc <- SC.scDefineConstant sc ni (cm ^. convertedModuleTerm) (cm ^. convertedModuleType)
         let cm' = cm { _convertedModuleTerm = tc }
         pure $ Map.insert nm cm' env
     )
@@ -121,10 +120,9 @@ convertYosysIR sc ir = do
 
 -- | Given a Yosys IR, construct a map from module names to TypedTerms
 yosysIRToTypedTerms ::
-  MonadIO m =>
   SC.SharedContext ->
   YosysIR ->
-  m (Map Text SC.TypedTerm)
+  IO (Map Text SC.TypedTerm)
 yosysIRToTypedTerms sc ir = do
   env <- convertYosysIR sc ir
   pure . flip fmap env $ \cm ->
@@ -134,10 +132,9 @@ yosysIRToTypedTerms sc ir = do
 
 -- | Given a Yosys IR, construct a SAWCore record containing terms for each module
 yosysIRToRecordTerm ::
-  MonadIO m =>
   SC.SharedContext ->
   YosysIR ->
-  m SC.TypedTerm
+  IO SC.TypedTerm
 yosysIRToRecordTerm sc ir = do
   env <- convertYosysIR sc ir
   record <- cryptolRecord sc $ view convertedModuleTerm <$> env
@@ -147,11 +144,10 @@ yosysIRToRecordTerm sc ir = do
 
 -- | Given a Yosys IR, construct a value representing a specific module with all submodules inlined
 yosysIRToSequential ::
-  MonadIO m =>
   SC.SharedContext ->
   YosysIR ->
   Text ->
-  m YosysSequential
+  IO YosysSequential
 yosysIRToSequential sc ir nm = do
   case Map.lookup nm $ ir ^. yosysModules of
     Nothing -> throw . YosysError $ mconcat
@@ -173,9 +169,9 @@ yosysIRToSequential sc ir nm = do
 yosys_import :: FilePath -> TopLevel SC.TypedTerm
 yosys_import path = do
   sc <- getSharedContext
-  ir <- loadYosysIR path
-  tt <- yosysIRToRecordTerm sc ir
-  _ <- validateTerm sc "translating combinational circuits" $ SC.ttTerm tt
+  ir <- liftIO $ loadYosysIR path
+  tt <- liftIO $ yosysIRToRecordTerm sc ir
+  _ <- liftIO $ validateTerm sc "translating combinational circuits" $ SC.ttTerm tt
   pure tt
 
 -- | Proves equality between a combinational HDL module and a
@@ -193,7 +189,7 @@ yosys_verify ::
   TopLevel YosysTheorem
 yosys_verify ymod preconds other specs tactic = do
   sc <- getSharedContext
-  newmod <- foldM (flip $ applyOverride sc)
+  newmod <- liftIO $ foldM (flip $ applyOverride sc)
     (SC.ttTerm ymod)
     specs
   mpc <- case preconds of
@@ -201,8 +197,8 @@ yosys_verify ymod preconds other specs tactic = do
     (pc:pcs) -> do
       t <- foldM (\a b -> liftIO $ SC.scAnd sc a b) (SC.ttTerm pc) (SC.ttTerm <$> pcs)
       pure . Just $ SC.TypedTerm (SC.ttType pc) t
-  thm <- buildTheorem sc ymod newmod mpc other
-  prop <- theoremProp sc thm
+  thm <- liftIO $ buildTheorem sc ymod newmod mpc other
+  prop <- liftIO $ theoremProp sc thm
   _ <- Builtins.provePrintPrim tactic prop
   pure thm
 
@@ -214,8 +210,8 @@ yosys_import_sequential ::
   TopLevel YosysSequential
 yosys_import_sequential nm path = do
   sc <- getSharedContext
-  ir <- loadYosysIR path
-  yosysIRToSequential sc ir nm
+  ir <- liftIO $ loadYosysIR path
+  liftIO $ yosysIRToSequential sc ir nm
 
 -- | Extracts a term from the given sequential module with the state
 -- eliminated by iterating the term over the given concrete number of
@@ -229,8 +225,8 @@ yosys_extract_sequential ::
   TopLevel SC.TypedTerm
 yosys_extract_sequential s n = do
   sc <- getSharedContext
-  tt <- composeYosysSequential sc s n
-  _ <- validateTerm sc "composing a sequential term" $ SC.ttTerm tt
+  tt <- liftIO $ composeYosysSequential sc s n
+  _ <- liftIO $ validateTerm sc "composing a sequential term" $ SC.ttTerm tt
   pure tt
 
 -- | Like `yosys_extract_sequential`, but the resulting term has an
@@ -241,8 +237,8 @@ yosys_extract_sequential_with_state ::
   TopLevel SC.TypedTerm
 yosys_extract_sequential_with_state s n = do
   sc <- getSharedContext
-  tt <- composeYosysSequentialWithState sc s n
-  _ <- validateTerm sc "composing a sequential term with state" $ SC.ttTerm tt
+  tt <- liftIO $ composeYosysSequentialWithState sc s n
+  _ <- liftIO $ validateTerm sc "composing a sequential term with state" $ SC.ttTerm tt
   pure tt
 
 -- | Extracts a term from the given sequential module. This term has
@@ -261,4 +257,4 @@ yosys_verify_sequential_sally ::
 yosys_verify_sequential_sally s path q fixed = do
   sc <- getSharedContext
   sym <- liftIO $ Common.newSAWCoreExprBuilder sc False
-  queryModelChecker sym sc s path q $ Set.fromList fixed
+  liftIO $ queryModelChecker sym sc s path q $ Set.fromList fixed
diff --git a/saw-central/src/SAWCentral/Yosys/Cell.hs b/saw-central/src/SAWCentral/Yosys/Cell.hs
index 387852689f..2ae01d2b2e 100644
--- a/saw-central/src/SAWCentral/Yosys/Cell.hs
+++ b/saw-central/src/SAWCentral/Yosys/Cell.hs
@@ -13,7 +13,6 @@ Stability   : experimental
 module SAWCentral.Yosys.Cell where
 
 import Control.Lens ((^.))
-import Control.Monad.IO.Class (MonadIO(..))
 
 import Data.Char (digitToInt)
 import Data.Map (Map)
@@ -38,31 +37,31 @@ data CellTerm = CellTerm
   , cellTermSigned :: Bool
   }
 
-cellTermNat :: forall m. MonadIO m => SC.SharedContext -> CellTerm -> m SC.Term
-cellTermNat sc (CellTerm { cellTermTerm = t, cellTermWidth = w }) = liftIO $ SC.scBvToNat sc w t
+cellTermNat :: SC.SharedContext -> CellTerm -> IO SC.Term
+cellTermNat sc (CellTerm { cellTermTerm = t, cellTermWidth = w }) = SC.scBvToNat sc w t
 
 -- | Apply the appropriate (possibly signed) extension or truncation to make the given bitvector
 -- match the given width.
-extTrunc :: forall m. MonadIO m => SC.SharedContext -> Natural -> CellTerm -> m CellTerm
+extTrunc :: SC.SharedContext -> Natural -> CellTerm -> IO CellTerm
 extTrunc sc width (CellTerm { cellTermTerm = t, cellTermWidth = bvw, cellTermSigned = signed}) = do
-  wterm <- liftIO $ SC.scNat sc width
-  bvwterm <- liftIO $ SC.scNat sc bvw
+  wterm <- SC.scNat sc width
+  bvwterm <- SC.scNat sc bvw
   res <- if
     | bvw > width -> do
-        diffterm <- liftIO . SC.scNat sc $ bvw - width
-        liftIO $ SC.scBvTrunc sc diffterm wterm t
+        diffterm <- SC.scNat sc $ bvw - width
+        SC.scBvTrunc sc diffterm wterm t
     | width > bvw && signed -> do
-        bvwpredterm <- liftIO . SC.scNat sc $ bvw - 1
-        diffterm <- liftIO . SC.scNat sc $ width - bvw
-        liftIO $ SC.scBvSExt sc diffterm bvwpredterm t
+        bvwpredterm <- SC.scNat sc $ bvw - 1
+        diffterm <- SC.scNat sc $ width - bvw
+        SC.scBvSExt sc diffterm bvwpredterm t
     | width > bvw && not signed -> do
-        diffterm <- liftIO . SC.scNat sc $ width - bvw
-        liftIO $ SC.scBvUExt sc diffterm bvwterm t
+        diffterm <- SC.scNat sc $ width - bvw
+        SC.scBvUExt sc diffterm bvwterm t
     | otherwise -> pure t
   pure $ CellTerm res width signed
 
 -- | Given two bitvectors, extend the narrower bitvector to match the wider.
-extMax :: forall m. MonadIO m => SC.SharedContext -> CellTerm -> CellTerm -> m (CellTerm, CellTerm)
+extMax :: SC.SharedContext -> CellTerm -> CellTerm -> IO (CellTerm, CellTerm)
 extMax sc c1 c2 = do
   let
     w1 = cellTermWidth c1
@@ -72,45 +71,41 @@ extMax sc c1 c2 = do
   res2 <- extTrunc sc w c2
   pure (res1, res2)
 
-liftUnary :: forall m.
-  MonadIO m =>
+liftUnary ::
   SC.SharedContext ->
   (SC.Term -> SC.Term -> IO SC.Term) -> -- (w : Nat) -> [w] -> [w]
-  CellTerm -> m CellTerm
+  CellTerm -> IO CellTerm
 liftUnary sc f c@(CellTerm { cellTermTerm = t }) = do
-  wt <- liftIO . SC.scNat sc $ cellTermWidth c
-  res <- liftIO $ f wt t
+  wt <- SC.scNat sc $ cellTermWidth c
+  res <- f wt t
   pure $ c { cellTermTerm = res }
 
-liftBinary :: forall m.
-  MonadIO m =>
+liftBinary ::
   SC.SharedContext ->
   (SC.Term -> SC.Term -> SC.Term -> IO SC.Term) -> -- (w : Nat) -> [w] -> [w] -> [w]
-  CellTerm -> CellTerm -> m CellTerm
+  CellTerm -> CellTerm -> IO CellTerm
 liftBinary sc f c1@(CellTerm { cellTermTerm = t1 }) (CellTerm { cellTermTerm = t2 }) = do
-  wt <- liftIO . SC.scNat sc $ cellTermWidth c1
-  res <- liftIO $ f wt t1 t2
+  wt <- SC.scNat sc $ cellTermWidth c1
+  res <- f wt t1 t2
   pure $ c1 { cellTermTerm = res }
 
-liftBinaryCmp :: forall m.
-  MonadIO m =>
+liftBinaryCmp ::
   SC.SharedContext ->
   (SC.Term -> SC.Term -> SC.Term -> IO SC.Term) -> -- (w : Nat) -> [w] -> [w] -> Bool
-  CellTerm -> CellTerm -> m SC.Term
+  CellTerm -> CellTerm -> IO SC.Term
 liftBinaryCmp sc f c1@(CellTerm { cellTermTerm = t1 }) (CellTerm { cellTermTerm = t2 }) = do
-  wt <- liftIO . SC.scNat sc $ cellTermWidth c1
-  liftIO $ f wt t1 t2
+  wt <- SC.scNat sc $ cellTermWidth c1
+  f wt t1 t2
 
 -- | Given a primitive Yosys cell and a map of terms for its
 -- arguments, construct a record term representing the output. If the
 -- provided cell is not a primitive, return Nothing.
 primCellToTerm ::
-  forall m b.
-  MonadIO m =>
+  forall b.
   SC.SharedContext ->
   Cell [b] {- ^ Cell type -} ->
   Map Text SC.Term {- ^ Mapping of input names to input terms -} ->
-  m (Maybe SC.Term)
+  IO (Maybe SC.Term)
 primCellToTerm sc c args = do
   mm <- primCellToMap sc c args
   mt <- traverse (cryptolRecord sc) mm
@@ -124,12 +119,11 @@ primCellToTerm sc c args = do
       ]
 
 primCellToMap ::
-  forall m b.
-  MonadIO m =>
+  forall b.
   SC.SharedContext ->
   Cell [b] {- ^ Cell type -} ->
   Map Text SC.Term {- ^ Mapping of input names to input terms -} ->
-  m (Maybe (Map Text SC.Term))
+  IO (Maybe (Map Text SC.Term))
 primCellToMap sc c args = case c ^. cellType of
   CellTypeNot -> bvUnaryOp . liftUnary sc $ SC.scBvNot sc
   CellTypePos -> do
@@ -143,60 +137,60 @@ primCellToMap sc c args = case c ^. cellType of
     r <- SC.scBvXor sc w x y
     SC.scBvNot sc w r
   CellTypeReduceAnd -> bvReduce True =<< do
-    liftIO . SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "and"
+    SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "and"
   CellTypeReduceOr -> bvReduce False =<< do
-    liftIO . SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "or"
+    SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "or"
   CellTypeReduceXor -> bvReduce False =<< do
-    liftIO . SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "xor"
+    SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "xor"
   CellTypeReduceXnor -> bvReduce True =<< do
-    boolTy <- liftIO $ SC.scBoolType sc
-    x <- liftIO $ SC.scFreshVariable sc "x" boolTy
-    y <- liftIO $ SC.scFreshVariable sc "y" boolTy
-    r <- liftIO $ SC.scXor sc x y
-    res <- liftIO $ SC.scNot sc r
-    liftIO $ SC.scAbstractTerms sc [x, y] res
+    boolTy <- SC.scBoolType sc
+    x <- SC.scFreshVariable sc "x" boolTy
+    y <- SC.scFreshVariable sc "y" boolTy
+    r <- SC.scXor sc x y
+    res <- SC.scNot sc r
+    SC.scAbstractTerms sc [x, y] res
   CellTypeReduceBool -> bvReduce False =<< do
-    liftIO . SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "or"
+    SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "or"
   CellTypeShl -> do
     ta <- fmap cellTermTerm $ input "A"
     nb <- cellTermNat sc =<< input "B"
     w <- outputWidth
-    res <- liftIO $ SC.scBvShl sc w ta nb
+    res <- SC.scBvShl sc w ta nb
     output (CellTerm res (connWidthNat "A") (connSigned "A"))
   CellTypeShr -> do
     ta <- fmap cellTermTerm $ input "A"
     nb <- cellTermNat sc =<< input "B"
     w <- outputWidth
-    res <- liftIO $ SC.scBvShr sc w ta nb
+    res <- SC.scBvShr sc w ta nb
     output (CellTerm res (connWidthNat "A") (connSigned "A"))
   CellTypeSshl -> do
     ta <- fmap cellTermTerm $ input "A"
     nb <- cellTermNat sc =<< input "B"
     w <- outputWidth
-    res <- liftIO $ SC.scBvShl sc w ta nb
+    res <- SC.scBvShl sc w ta nb
     output (CellTerm res (connWidthNat "A") (connSigned "A"))
   CellTypeSshr -> do
     ta <- fmap cellTermTerm $ input "A"
     nb <- cellTermNat sc =<< input "B"
     w <- outputWidth
-    res <- liftIO $ SC.scBvSShr sc w ta nb
+    res <- SC.scBvSShr sc w ta nb
     output (CellTerm res (connWidthNat "A") (connSigned "A"))
   -- "$shift" -> _
   CellTypeShiftx -> do
     let w = max (connWidthNat "A") (connWidthNat "B")
-    wt <- liftIO $ SC.scNat sc w
+    wt <- SC.scNat sc w
     CellTerm ta _ _ <- extTrunc sc w =<< input "A"
     CellTerm tb _ _ <- extTrunc sc w =<< input "B"
-    zero <- liftIO $ SC.scBvConst sc w 0
-    tbn <- liftIO $ SC.scBvToNat sc w tb
-    tbneg <- liftIO $ SC.scBvNeg sc wt tb
-    tbnegn <- liftIO $ SC.scBvToNat sc w tbneg
-    cond <- liftIO $ SC.scBvSGe sc wt tb zero
-    tcase <- liftIO $ SC.scBvShr sc wt ta tbn
-    ecase <- liftIO $ SC.scBvShl sc wt ta tbnegn
-    ty <- liftIO . SC.scBitvector sc $ connWidthNat "A"
+    zero <- SC.scBvConst sc w 0
+    tbn <- SC.scBvToNat sc w tb
+    tbneg <- SC.scBvNeg sc wt tb
+    tbnegn <- SC.scBvToNat sc w tbneg
+    cond <- SC.scBvSGe sc wt tb zero
+    tcase <- SC.scBvShr sc wt ta tbn
+    ecase <- SC.scBvShl sc wt ta tbnegn
+    ty <- SC.scBitvector sc $ connWidthNat "A"
     res <- if connSigned "B"
-      then liftIO $ SC.scIte sc ty cond tcase ecase
+      then SC.scIte sc ty cond tcase ecase
       else pure tcase
     output (CellTerm res (connWidthNat "A") (connSigned "A"))
   CellTypeLt -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvULt sc
@@ -220,26 +214,26 @@ primCellToMap sc c args = case c ^. cellType of
   CellTypeLogicNot -> do
     w <- connWidth "A"
     ta <- cellTermTerm <$> input "A"
-    anz <- liftIO $ SC.scBvNonzero sc w ta
-    res <- liftIO $ SC.scNot sc anz
+    anz <- SC.scBvNonzero sc w ta
+    res <- SC.scNot sc anz
     outputBit res
   CellTypeLogicAnd -> bvBinaryCmp . liftBinaryCmp sc $ \w x y -> do
-    xnz <- liftIO $ SC.scBvNonzero sc w x
-    ynz <- liftIO $ SC.scBvNonzero sc w y
-    liftIO $ SC.scAnd sc xnz ynz
+    xnz <- SC.scBvNonzero sc w x
+    ynz <- SC.scBvNonzero sc w y
+    SC.scAnd sc xnz ynz
   CellTypeLogicOr -> bvBinaryCmp . liftBinaryCmp sc $ \w x y -> do
-    xnz <- liftIO $ SC.scBvNonzero sc w x
-    ynz <- liftIO $ SC.scBvNonzero sc w y
-    liftIO $ SC.scOr sc xnz ynz
+    xnz <- SC.scBvNonzero sc w x
+    ynz <- SC.scBvNonzero sc w y
+    SC.scOr sc xnz ynz
   CellTypeMux -> do
     ta <- cellTermTerm <$> input "A"
     tb <- cellTermTerm <$> input "B"
     ts <- cellTermTerm <$> input "S"
     swidth <- connWidth "S"
-    snz <- liftIO $ SC.scBvNonzero sc swidth ts
+    snz <- SC.scBvNonzero sc swidth ts
     let width = connWidthNat "Y"
-    ty <- liftIO $ SC.scBitvector sc width
-    res <- liftIO $ SC.scIte sc ty snz tb ta
+    ty <- SC.scBitvector sc width
+    res <- SC.scIte sc ty snz tb ta
     output $ CellTerm res (connWidthNat "A") (connSigned "A")
   CellTypePmux -> do
     ta <- cellTermTerm <$> input "A"
@@ -247,28 +241,28 @@ primCellToMap sc c args = case c ^. cellType of
     ts <- cellTermTerm <$> input "S"
 
     width <- connWidth "A"
-    widthBv <- liftIO . SC.scBitvector sc $ connWidthNat "A"
+    widthBv <- SC.scBitvector sc $ connWidthNat "A"
     swidth <- connWidth "S"
-    bool <- liftIO $ SC.scBoolType sc
-    nat <- liftIO $ SC.scNatType sc
-    splitb <- liftIO $ SC.scSplit sc swidth width bool tb
-    zero <- liftIO $ SC.scNat sc 0
-    accTy <- liftIO $ SC.scPairType sc nat widthBv
-    defaultAcc <- liftIO $ SC.scPairValue sc zero ta
+    bool <- SC.scBoolType sc
+    nat <- SC.scNatType sc
+    splitb <- SC.scSplit sc swidth width bool tb
+    zero <- SC.scNat sc 0
+    accTy <- SC.scPairType sc nat widthBv
+    defaultAcc <- SC.scPairValue sc zero ta
 
-    bit <- liftIO $ SC.scFreshVariable sc "bit" bool
-    acc <- liftIO $ SC.scFreshVariable sc "acc" accTy
-    fun <- liftIO . SC.scAbstractTerms sc [bit, acc] =<< do
-      idx <- liftIO $ SC.scPairLeft sc acc
-      aval <- liftIO $ SC.scPairRight sc acc
-      bval <- liftIO $ SC.scAtWithDefault sc swidth widthBv aval splitb idx
-      newidx <- liftIO $ SC.scAddNat sc idx width
-      newval <- liftIO $ SC.scIte sc widthBv bit bval aval
-      liftIO $ SC.scPairValue sc newidx newval
+    bit <- SC.scFreshVariable sc "bit" bool
+    acc <- SC.scFreshVariable sc "acc" accTy
+    fun <- SC.scAbstractTerms sc [bit, acc] =<< do
+      idx <- SC.scPairLeft sc acc
+      aval <- SC.scPairRight sc acc
+      bval <- SC.scAtWithDefault sc swidth widthBv aval splitb idx
+      newidx <- SC.scAddNat sc idx width
+      newval <- SC.scIte sc widthBv bit bval aval
+      SC.scPairValue sc newidx newval
 
-    scFoldr <- liftIO . SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "foldr"
-    resPair <- liftIO $ SC.scApplyAll sc scFoldr [bool, accTy, swidth, fun, defaultAcc, ts]
-    res <- liftIO $ SC.scPairRight sc resPair
+    scFoldr <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "foldr"
+    resPair <- SC.scApplyAll sc scFoldr [bool, accTy, swidth, fun, defaultAcc, ts]
+    res <- SC.scPairRight sc resPair
     output $ CellTerm res (connWidthNat "A") (connSigned "Y")
   CellTypeBmux -> do
     ia <- input "A"
@@ -276,16 +270,16 @@ primCellToMap sc c args = case c ^. cellType of
     let swidth = cellTermWidth is
     let ywidth = connWidthNat "Y"
     -- Split input A into chunks
-    chunks <- liftIO (SC.scNat sc (2 ^ swidth))
-    ywidth' <- liftIO (SC.scNat sc ywidth)
-    bool <- liftIO (SC.scBoolType sc)
-    splitA <- liftIO (SC.scSplit sc chunks ywidth' bool (cellTermTerm ia))
+    chunks <- SC.scNat sc (2 ^ swidth)
+    ywidth' <- SC.scNat sc ywidth
+    bool <- SC.scBoolType sc
+    splitA <- SC.scSplit sc chunks ywidth' bool (cellTermTerm ia)
     -- reverse to put index 0 on the left
-    outputType <- liftIO (SC.scBitvector sc ywidth)
-    revA <- liftIO (SC.scGlobalApply sc "Prelude.reverse" [chunks, outputType, splitA])
+    outputType <- SC.scBitvector sc ywidth
+    revA <- SC.scGlobalApply sc "Prelude.reverse" [chunks, outputType, splitA]
     -- Select chunk from output
-    ixWidth <- liftIO (SC.scNat sc swidth)
-    elt <- liftIO (SC.scBvAt sc chunks outputType ixWidth revA (cellTermTerm is))
+    ixWidth <- SC.scNat sc swidth
+    elt <- SC.scBvAt sc chunks outputType ixWidth revA (cellTermTerm is)
     output (CellTerm elt ywidth (connSigned "Y"))
   -- "$demux" -> _
   -- "$lut" -> _
@@ -311,16 +305,16 @@ primCellToMap sc c args = case c ^. cellType of
       case Map.lookup onm $ c ^. cellConnections of
         Nothing -> panic "cellToTerm" ["Missing expected output name for " <> nm <> " cell"]
         Just bits -> fromIntegral $ length bits
-    connWidth :: Text -> m SC.Term
-    connWidth onm = liftIO . SC.scNat sc $ connWidthNat onm
+    connWidth :: Text -> IO SC.Term
+    connWidth onm = SC.scNat sc $ connWidthNat onm
     outputWidth = connWidth "Y"
 
-    input :: Text -> m CellTerm
+    input :: Text -> IO CellTerm
     input inpNm = case Map.lookup inpNm args of
       Nothing -> panic "cellToTerm" [nm <> " missing input " <> inpNm]
       Just a -> pure $ CellTerm a (connWidthNat inpNm) (connSigned inpNm)
 
-    output :: CellTerm -> m (Maybe (Map Text SC.Term))
+    output :: CellTerm -> IO (Maybe (Map Text SC.Term))
     output (CellTerm ct cw _) = do
       let res = CellTerm ct cw (connSigned "Y")
       CellTerm t _ _ <- extTrunc sc (connWidthNat "Y") res
@@ -328,22 +322,22 @@ primCellToMap sc c args = case c ^. cellType of
         [ ("Y", t)
         ]
 
-    outputBit :: SC.Term -> m (Maybe (Map Text SC.Term))
+    outputBit :: SC.Term -> IO (Maybe (Map Text SC.Term))
     outputBit res = do
-      bool <- liftIO $ SC.scBoolType sc
-      vres <- liftIO $ SC.scSingle sc bool res
+      bool <- SC.scBoolType sc
+      vres <- SC.scSingle sc bool res
       pure . Just $ Map.fromList
         [ ("Y", vres)
         ]
 
     -- convert input to big endian
-    bvUnaryOp :: (CellTerm -> m CellTerm) -> m (Maybe (Map Text SC.Term))
+    bvUnaryOp :: (CellTerm -> IO CellTerm) -> IO (Maybe (Map Text SC.Term))
     bvUnaryOp f = do
       t <- input "A"
       res <- f t
       output res
     -- extend inputs to output width
-    bvBinaryOp :: (CellTerm -> CellTerm -> m CellTerm) -> m (Maybe (Map Text SC.Term))
+    bvBinaryOp :: (CellTerm -> CellTerm -> IO CellTerm) -> IO (Maybe (Map Text SC.Term))
     bvBinaryOp f = do
       let w = connWidthNat "Y"
       ta <- extTrunc sc w =<< input "A"
@@ -351,18 +345,18 @@ primCellToMap sc c args = case c ^. cellType of
       res <- f ta tb
       output res
     -- extend inputs to max input width, output is a single bit
-    bvBinaryCmp :: (CellTerm -> CellTerm -> m SC.Term) -> m (Maybe (Map Text SC.Term))
+    bvBinaryCmp :: (CellTerm -> CellTerm -> IO SC.Term) -> IO (Maybe (Map Text SC.Term))
     bvBinaryCmp f = do
       ta <- input "A"
       tb <- input "B"
       res <- uncurry f =<< extMax sc ta tb
       outputBit res
-    bvReduce :: Bool -> SC.Term -> m (Maybe (Map Text SC.Term))
+    bvReduce :: Bool -> SC.Term -> IO (Maybe (Map Text SC.Term))
     bvReduce boolIdentity boolFun = do
       CellTerm t _ _ <- input "A"
       w <- connWidth "A"
-      boolTy <- liftIO $ SC.scBoolType sc
-      identity <- liftIO $ SC.scBool sc boolIdentity
-      scFoldr <- liftIO . SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "foldr"
-      bit <- liftIO $ SC.scApplyAll sc scFoldr [boolTy, boolTy, w, boolFun, identity, t]
+      boolTy <- SC.scBoolType sc
+      identity <- SC.scBool sc boolIdentity
+      scFoldr <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "foldr"
+      bit <- SC.scApplyAll sc scFoldr [boolTy, boolTy, w, boolFun, identity, t]
       outputBit bit
diff --git a/saw-central/src/SAWCentral/Yosys/IR.hs b/saw-central/src/SAWCentral/Yosys/IR.hs
index b519f5b8da..32fef57ab5 100644
--- a/saw-central/src/SAWCentral/Yosys/IR.hs
+++ b/saw-central/src/SAWCentral/Yosys/IR.hs
@@ -19,7 +19,6 @@ module SAWCentral.Yosys.IR where
 import Control.Lens.TH (makeLenses)
 
 import Control.Lens ((^.))
-import Control.Monad.IO.Class (MonadIO(..))
 import Control.Exception (throw)
 
 import qualified Data.Maybe as Maybe
@@ -305,8 +304,8 @@ instance Aeson.FromJSON YosysIR where
     pure YosysIR{..}
 
 -- | Read a collection of HDL modules from a file produced by Yosys' write_json command.
-loadYosysIR :: MonadIO m => FilePath -> m YosysIR
-loadYosysIR p = liftIO $ Aeson.eitherDecodeFileStrict p >>= \case
+loadYosysIR :: FilePath -> IO YosysIR
+loadYosysIR p = Aeson.eitherDecodeFileStrict p >>= \case
   Left err -> throw . YosysError $ Text.pack err
   Right ir -> pure ir
 
diff --git a/saw-central/src/SAWCentral/Yosys/Netgraph.hs b/saw-central/src/SAWCentral/Yosys/Netgraph.hs
index ae76ec73e2..06fc7db9e0 100644
--- a/saw-central/src/SAWCentral/Yosys/Netgraph.hs
+++ b/saw-central/src/SAWCentral/Yosys/Netgraph.hs
@@ -21,7 +21,6 @@ import Control.Lens.TH (makeLenses)
 
 import Control.Lens ((^.))
 import Control.Monad (forM, foldM)
-import Control.Monad.IO.Class (MonadIO(..))
 import Control.Exception (throw)
 
 import qualified Data.Maybe as Maybe
@@ -93,15 +92,15 @@ data ConvertedModule = ConvertedModule
 makeLenses ''ConvertedModule
 
 lookupPatternTerm ::
-  (MonadIO m, Ord b, Show b) =>
+  (Ord b, Show b) =>
   SC.SharedContext ->
   YosysBitvecConsumer ->
   [b] ->
   Map [b] Preterm ->
-  m SC.Term
+  IO SC.Term
 lookupPatternTerm sc loc pat ts =
   case Map.lookup pat ts of
-    Just t -> liftIO $ scPreterm sc t
+    Just t -> scPreterm sc t
     Nothing -> do
       bits <- forM pat $ \b -> do
         case Map.lookup [b] ts of
@@ -109,17 +108,16 @@ lookupPatternTerm sc loc pat ts =
           Nothing -> throw $ YosysErrorNoSuchOutputBitvec (Text.pack $ show b) loc
       -- Yosys lists bits in little-endian order, while scVector expects big-endian, so reverse
       let ps = fusePreterms (reverse bits)
-      liftIO $ scPreterms sc ps
+      scPreterms sc ps
 
 -- | Given a netgraph and an initial map from bit patterns to terms, populate that map with terms
 -- generated from the rest of the netgraph.
 netgraphToTerms ::
-  (MonadIO m) =>
   SC.SharedContext ->
   Map Text ConvertedModule ->
   Netgraph ->
   Map [Bitrep] Preterm ->
-  m (Map [Bitrep] Preterm)
+  IO (Map [Bitrep] Preterm)
 netgraphToTerms sc env ng inputs
   | length (Graph.scc $ ng ^. netgraphGraph) /= length (ng ^. netgraphGraph)
   = do
@@ -155,7 +153,7 @@ netgraphToTerms sc env ng inputs
                       case Map.lookup submoduleName env of
                         Just cm -> do
                           r <- cryptolRecord sc args
-                          liftIO $ SC.scApply sc (cm ^. convertedModuleTerm) r
+                          SC.scApply sc (cm ^. convertedModuleTerm) r
                         Nothing ->
                             throw $ YosysErrorNoSuchSubmodule  submoduleName cnm
 
@@ -169,11 +167,10 @@ netgraphToTerms sc env ng inputs
         sorted
 
 convertModule ::
-  MonadIO m =>
   SC.SharedContext ->
   Map Text ConvertedModule ->
   Module ->
-  m ConvertedModule
+  IO ConvertedModule
 convertModule sc env m = do
   let ng = moduleNetgraph m
 
@@ -182,25 +179,25 @@ convertModule sc env m = do
 
   inputFields <- forM inputPorts
     (\inp -> do
-        liftIO . SC.scBitvector sc . fromIntegral $ length inp
+        SC.scBitvector sc . fromIntegral $ length inp
     )
   outputFields <- forM outputPorts
     (\out -> do
-        liftIO . SC.scBitvector sc . fromIntegral $ length out
+        SC.scBitvector sc . fromIntegral $ length out
     )
   inputRecordType <- cryptolRecordType sc inputFields
   outputRecordType <- cryptolRecordType sc outputFields
-  inputRecord <- liftIO $ SC.scFreshVariable sc "input" inputRecordType
+  inputRecord <- SC.scFreshVariable sc "input" inputRecordType
 
   derivedInputs <- forM (Map.assocs inputPorts) $ \(nm, inp) -> do
-    t <- liftIO $ cryptolRecordSelect sc inputFields inputRecord nm
+    t <- cryptolRecordSelect sc inputFields inputRecord nm
     deriveTermsByIndices sc inp t
 
-  oneBitType <- liftIO $ SC.scBitvector sc 1
-  xMsg <- liftIO $ SC.scString sc "Attempted to read X bit"
-  xTerm <- liftIO $ SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, xMsg]
-  zMsg <- liftIO $ SC.scString sc "Attempted to read Z bit"
-  zTerm <- liftIO $ SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, zMsg]
+  oneBitType <- SC.scBitvector sc 1
+  xMsg <- SC.scString sc "Attempted to read X bit"
+  xTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, xMsg]
+  zMsg <- SC.scString sc "Attempted to read Z bit"
+  zTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, zMsg]
   let inputs = Map.unions $ mconcat
         [ [ Map.fromList
             [ ( [BitrepZero], PretermBvNat 1 0 )
@@ -216,8 +213,8 @@ convertModule sc env m = do
   outputRecord <- cryptolRecord sc =<< mapForWithKeyM outputPorts
     (\onm out -> lookupPatternTerm sc (YosysBitvecConsumerOutputPort onm) out terms)
 
-  t <- liftIO $ SC.scAbstractTerms sc [inputRecord] outputRecord
-  ty <- liftIO $ SC.scFun sc inputRecordType outputRecordType
+  t <- SC.scAbstractTerms sc [inputRecord] outputRecord
+  ty <- SC.scFun sc inputRecordType outputRecordType
 
   let toCryptol (nm, rep) = (C.mkIdent nm, C.tWord . C.tNum $ length rep)
   let cty = C.tFun
diff --git a/saw-central/src/SAWCentral/Yosys/State.hs b/saw-central/src/SAWCentral/Yosys/State.hs
index ec99699dff..8f0c474589 100644
--- a/saw-central/src/SAWCentral/Yosys/State.hs
+++ b/saw-central/src/SAWCentral/Yosys/State.hs
@@ -20,7 +20,6 @@ import Control.Lens.TH (makeLenses)
 
 import Control.Lens ((^.))
 import Control.Monad (forM, foldM)
-import Control.Monad.IO.Class (MonadIO(..))
 import Control.Exception (throw)
 
 import Data.Map (Map)
@@ -66,11 +65,10 @@ makeLenses ''YosysSequential
 -- | Add a record-typed field named __states__ to the given mapping of
 -- field names to types.
 insertStateField ::
-  MonadIO m =>
   SC.SharedContext ->
   Map Text (SC.Term, C.Type) {- ^ The field types of "__states__" -} ->
   Map Text (SC.Term, C.Type) {- ^ The mapping to update -} ->
-  m (Map Text (SC.Term, C.Type))
+  IO (Map Text (SC.Term, C.Type))
 insertStateField sc stateFields fields = do
   stateRecordType <- fieldsToType sc stateFields
   stateRecordCryptolType <- fieldsToCryptolType stateFields
@@ -78,10 +76,9 @@ insertStateField sc stateFields fields = do
 
 -- | Translate a stateful HDL module into SAWCore
 convertModuleInline ::
-  MonadIO m =>
   SC.SharedContext ->
   Module ->
-  m YosysSequential
+  IO YosysSequential
 convertModuleInline sc m = do
   let ng = moduleNetgraph m
 
@@ -106,18 +103,18 @@ convertModuleInline sc m = do
       Just b -> pure . fromIntegral $ length b
 
   stateFields <- forM stateWidths $ \w -> do
-    t <- liftIO $ SC.scBitvector sc w
+    t <- SC.scBitvector sc w
     let cty = C.tWord $ C.tNum w
     pure (t, cty)
 
   let inputPorts = moduleInputPorts m
   let outputPorts = moduleOutputPorts m
   inputFields <- forM inputPorts $ \inp -> do
-    ty <- liftIO . SC.scBitvector sc . fromIntegral $ length inp
+    ty <- SC.scBitvector sc . fromIntegral $ length inp
     let cty = C.tWord . C.tNum $ length inp
     pure (ty, cty)
   outputFields <- forM outputPorts $ \out -> do
-    ty <- liftIO . SC.scBitvector sc . fromIntegral $ length out
+    ty <- SC.scBitvector sc . fromIntegral $ length out
     let cty = C.tWord . C.tNum $ length out
     pure (ty, cty)
 
@@ -130,25 +127,25 @@ convertModuleInline sc m = do
   codomainCryptolRecordType <- fieldsToCryptolType codomainFields
 
   -- convert module into term
-  domainRecord <- liftIO $ SC.scFreshVariable sc "input" domainRecordType
+  domainRecord <- SC.scFreshVariable sc "input" domainRecordType
 
   derivedInputs <- forM (Map.assocs inputPorts) $ \(nm, inp) -> do
-    t <- liftIO $ cryptolRecordSelect sc domainFields domainRecord nm
+    t <- cryptolRecordSelect sc domainFields domainRecord nm
     deriveTermsByIndices sc inp t
 
-  preStateRecord <- liftIO $ cryptolRecordSelect sc domainFields domainRecord "__state__"
+  preStateRecord <- cryptolRecordSelect sc domainFields domainRecord "__state__"
   derivedPreState <- forM (Map.assocs dffs) $ \(cnm, c) ->
     case Map.lookup "Q" $ c ^. cellConnections of
       Nothing -> panic "convertModuleInline" ["Missing expected output name for $dff cell"]
       Just b -> do
-        t <- liftIO $ cryptolRecordSelect sc stateFields preStateRecord cnm
+        t <- cryptolRecordSelect sc stateFields preStateRecord cnm
         deriveTermsByIndices sc b t
 
-  oneBitType <- liftIO $ SC.scBitvector sc 1
-  xMsg <- liftIO $ SC.scString sc "Attempted to read X bit"
-  xTerm <- liftIO $ SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, xMsg]
-  zMsg <- liftIO $ SC.scString sc "Attempted to read Z bit"
-  zTerm <- liftIO $ SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, zMsg]
+  oneBitType <- SC.scBitvector sc 1
+  xMsg <- SC.scString sc "Attempted to read X bit"
+  xTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, xMsg]
+  zMsg <- SC.scString sc "Attempted to read Z bit"
+  zTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, zMsg]
   let inputs = Map.unions $ mconcat
         [ [ Map.fromList
             [ ( [BitrepZero], PretermBvNat 1 0 )
@@ -175,8 +172,8 @@ convertModuleInline sc m = do
     (\onm out -> lookupPatternTerm sc (YosysBitvecConsumerOutputPort onm) out terms)
 
   -- construct result
-  t <- liftIO $ SC.scAbstractTerms sc [domainRecord] outputRecord
-  -- ty <- liftIO $ SC.scFun sc domainRecordType codomainRecordType
+  t <- SC.scAbstractTerms sc [domainRecord] outputRecord
+  -- ty <- SC.scFun sc domainRecordType codomainRecordType
   _ <- validateTerm sc "translating a sequential circuit" t
   let cty = C.tFun domainCryptolRecordType codomainCryptolRecordType
   pure YosysSequential
@@ -193,78 +190,76 @@ convertModuleInline sc m = do
 -- given number of times. The resulting term has a parameter for the
 -- initial state, the resulting Cryptol types does not.
 composeYosysSequentialHelper ::
-  forall m.
-  MonadIO m =>
   SC.SharedContext ->
   YosysSequential ->
   Integer ->
-  m (SC.Term, C.Type)
+  IO (SC.Term, C.Type)
 composeYosysSequentialHelper sc s n = do
   let t = SC.ttTerm $ s ^. yosysSequentialTerm
 
-  width <- liftIO . SC.scNat sc $ fromIntegral n
+  width <- SC.scNat sc $ fromIntegral n
   extendedInputFields <- forM (s ^. yosysSequentialInputFields) $ \(ty, cty) -> do
-    exty <- liftIO $ SC.scVecType sc width ty
+    exty <- SC.scVecType sc width ty
     let excty = C.tSeq (C.tNum n) cty
     pure (exty, excty)
   extendedOutputFields <- forM (s ^. yosysSequentialOutputFields) $ \(ty, cty) -> do
-    exty <- liftIO $ SC.scVecType sc width ty
+    exty <- SC.scVecType sc width ty
     let excty = C.tSeq (C.tNum n) cty
     pure (exty, excty)
   extendedInputType <- fieldsToType sc extendedInputFields
   extendedInputCryptolType <- fieldsToCryptolType extendedInputFields
-  extendedInputRecord <- liftIO $ SC.scFreshVariable sc "input" extendedInputType
+  extendedInputRecord <- SC.scFreshVariable sc "input" extendedInputType
   extendedOutputCryptolType <- fieldsToCryptolType extendedOutputFields
 
   allInputs <- fmap Map.fromList . forM (Map.keys extendedInputFields) $ \nm -> do
-    inp <- liftIO $ cryptolRecordSelect sc extendedInputFields extendedInputRecord nm
+    inp <- cryptolRecordSelect sc extendedInputFields extendedInputRecord nm
     pure (nm, inp)
 
   codomainFields <- insertStateField sc (s ^. yosysSequentialStateFields) $ s ^. yosysSequentialOutputFields
 
   let
-    buildIntermediateInput :: Integer -> SC.Term -> m SC.Term
+    buildIntermediateInput :: Integer -> SC.Term -> IO SC.Term
     buildIntermediateInput i st = do
       inps <- fmap Map.fromList . forM (Map.assocs allInputs) $ \(nm, inp) -> do
         case Map.lookup nm $ s ^. yosysSequentialInputFields of
           Nothing -> throw . YosysError $ "Invalid input: " <> nm
           Just (elemty, _) -> do
-            idx <- liftIO . SC.scNat sc $ fromIntegral i
-            idxed <- liftIO $ SC.scAt sc width elemty inp idx
+            idx <- SC.scNat sc $ fromIntegral i
+            idxed <- SC.scAt sc width elemty inp idx
             pure (nm, idxed)
       let inpsWithSt = Map.insert "__state__" st inps
       cryptolRecord sc inpsWithSt
 
-    summarizeOutput :: SC.Term -> m (SC.Term, Map Text SC.Term)
+    summarizeOutput :: SC.Term -> IO (SC.Term, Map Text SC.Term)
     summarizeOutput outrec = do
-      outstate <- liftIO $ cryptolRecordSelect sc codomainFields outrec "__state__"
+      outstate <- cryptolRecordSelect sc codomainFields outrec "__state__"
       outputs <- fmap Map.fromList . forM (Map.assocs $ s ^. yosysSequentialOutputFields) $ \(nm, (ty, _)) -> do
-        out <- liftIO $ cryptolRecordSelect sc codomainFields outrec nm
-        wrapped <- liftIO $ SC.scSingle sc ty out
+        out <- cryptolRecordSelect sc codomainFields outrec nm
+        wrapped <- SC.scSingle sc ty out
         pure (nm, wrapped)
       pure (outstate, outputs)
 
-    compose1 :: Integer -> (SC.Term, Map Text SC.Term) -> m (SC.Term, Map Text SC.Term)
+    compose1 :: Integer -> (SC.Term, Map Text SC.Term) -> IO (SC.Term, Map Text SC.Term)
     compose1 i (st, outs) = do
       inprec <- buildIntermediateInput i st
-      outrec <- liftIO $ SC.scApply sc t inprec
+      outrec <- SC.scApply sc t inprec
       (st', outs') <- summarizeOutput outrec
       mergedOuts <- fmap Map.fromList . forM (Map.assocs outs') $ \(nm, arr) -> do
         case (Map.lookup nm $ s ^. yosysSequentialOutputFields, Map.lookup nm outs) of
           (Just (ty, _), Just rest) -> do
-            restlen <- liftIO . SC.scNat sc $ fromIntegral i
-            arrlen <- liftIO $ SC.scNat sc 1
-            appended <- liftIO $ SC.scAppend sc restlen arrlen ty rest arr
+            restlen <- SC.scNat sc $ fromIntegral i
+            arrlen <- SC.scNat sc 1
+            appended <- SC.scAppend sc restlen arrlen ty rest arr
             pure (nm, appended)
           _ -> pure (nm, arr)
       pure (st', mergedOuts)
 
   stateType <- fieldsToType sc $ s ^. yosysSequentialStateFields
-  initialState <- liftIO $ SC.scFreshVariable sc "initial_state" stateType
+  initialState <- SC.scFreshVariable sc "initial_state" stateType
   (_, outputs) <- foldM (\acc i -> compose1 i acc) (initialState, Map.empty) [0..n-1]
 
   outputRecord <- cryptolRecord sc outputs
-  res <- liftIO $ SC.scAbstractTerms sc [initialState, extendedInputRecord] outputRecord
+  res <- SC.scAbstractTerms sc [initialState, extendedInputRecord] outputRecord
   let cty = C.tFun extendedInputCryptolType extendedOutputCryptolType
 
   pure (res, cty)
@@ -273,30 +268,26 @@ composeYosysSequentialHelper sc s n = do
 -- given number of times. Accessing the initial state produces an
 -- error.
 composeYosysSequential ::
-  forall m.
-  MonadIO m =>
   SC.SharedContext ->
   YosysSequential ->
   Integer ->
-  m SC.TypedTerm
+  IO SC.TypedTerm
 composeYosysSequential sc s n = do
   (t, cty) <- composeYosysSequentialHelper sc s n
   stateType <- fieldsToType sc $ s ^. yosysSequentialStateFields
-  initialStateMsg <- liftIO $ SC.scString sc "Attempted to read initial state of sequential circuit"
-  initialState <- liftIO $ SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [stateType, initialStateMsg]
-  res <- liftIO $ SC.scApply sc t initialState
+  initialStateMsg <- SC.scString sc "Attempted to read initial state of sequential circuit"
+  initialState <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [stateType, initialStateMsg]
+  res <- SC.scApply sc t initialState
   pure $ SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) res
 
 -- | Given a SAWCore term with an explicit state, iterate the term the
 -- given number of times. The resulting term has a parameter for the
 -- initial state.
 composeYosysSequentialWithState ::
-  forall m.
-  MonadIO m =>
   SC.SharedContext ->
   YosysSequential ->
   Integer ->
-  m SC.TypedTerm
+  IO SC.TypedTerm
 composeYosysSequentialWithState sc s n = do
   (t, cty) <- composeYosysSequentialHelper sc s n
   scty <- fieldsToCryptolType $ s ^. yosysSequentialStateFields
diff --git a/saw-central/src/SAWCentral/Yosys/Theorem.hs b/saw-central/src/SAWCentral/Yosys/Theorem.hs
index 92384a1fc6..e150998091 100644
--- a/saw-central/src/SAWCentral/Yosys/Theorem.hs
+++ b/saw-central/src/SAWCentral/Yosys/Theorem.hs
@@ -18,9 +18,7 @@ module SAWCentral.Yosys.Theorem where
 import Control.Lens.TH (makeLenses)
 
 import Control.Lens ((^.))
-import Control.Monad.IO.Class (MonadIO(..))
 import Control.Exception (throw)
-import Control.Monad.Catch (MonadThrow)
 
 import Data.Text (Text)
 import Data.Map (Map)
@@ -58,21 +56,20 @@ makeLenses ''YosysTheorem
 -- | Construct a SAWCore proposition for the given theorem.
 -- In pseudo-Cryptol, this looks like {{ \r -> precond r ==> (module r == body r) }}
 theoremProp ::
-  (MonadIO m, MonadThrow m) =>
   SC.SharedContext ->
   YosysTheorem ->
-  m SC.TypedTerm
+  IO SC.TypedTerm
 theoremProp sc thm = do
-  r <- liftIO $ SC.scFreshVariable sc "r" $ thm ^. theoremInputType
-  modr <- liftIO $ SC.scApply sc (thm ^. theoremModule) r
-  bodyr <- liftIO $ SC.scApply sc (thm ^. theoremBody) r
-  equality <- liftIO $ eqBvRecords sc (thm ^. theoremOutputCryptolType) modr bodyr
+  r <- SC.scFreshVariable sc "r" $ thm ^. theoremInputType
+  modr <- SC.scApply sc (thm ^. theoremModule) r
+  bodyr <- SC.scApply sc (thm ^. theoremBody) r
+  equality <- eqBvRecords sc (thm ^. theoremOutputCryptolType) modr bodyr
   res <- case thm ^. theoremPrecond of
     Nothing -> pure equality
     Just pc -> do
-      pcr <- liftIO $ SC.scApply sc pc r
-      liftIO $ SC.scImplies sc pcr equality
-  func <- liftIO $ SC.scAbstractTerms sc [r] res
+      pcr <- SC.scApply sc pc r
+      SC.scImplies sc pcr equality
+  func <- SC.scAbstractTerms sc [r] res
   let cty = C.tFun (thm ^. theoremInputCryptolType) C.tBit
   SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty)
     <$> validateTerm sc
@@ -82,20 +79,19 @@ theoremProp sc thm = do
 -- | Construct a SAWCore proposition for the given theorem.
 -- In pseudo-Cryptol, this looks like {{ \r -> if precond r then body r else module r }}
 theoremReplacement ::
-  (MonadIO m, MonadThrow m) =>
   SC.SharedContext ->
   YosysTheorem ->
-  m SC.Term
+  IO SC.Term
 theoremReplacement sc thm = do
-  r <- liftIO $ SC.scFreshVariable sc "r" $ thm ^. theoremInputType
+  r <- SC.scFreshVariable sc "r" $ thm ^. theoremInputType
   body <- case thm ^. theoremPrecond of
-    Nothing -> liftIO $ SC.scApply sc (thm ^. theoremBody) r
+    Nothing -> SC.scApply sc (thm ^. theoremBody) r
     Just pc -> do
-      precond <- liftIO $ SC.scApply sc pc r
-      thenCase <- liftIO $ SC.scApply sc (thm ^. theoremBody) r
-      elseCase <- liftIO $ SC.scApply sc (thm ^. theoremModule) r
-      liftIO $ SC.scIte sc (thm ^. theoremOutputType) precond thenCase elseCase
-  ft <- liftIO $ SC.scAbstractTerms sc [r] body
+      precond <- SC.scApply sc pc r
+      thenCase <- SC.scApply sc (thm ^. theoremBody) r
+      elseCase <- SC.scApply sc (thm ^. theoremModule) r
+      SC.scIte sc (thm ^. theoremOutputType) precond thenCase elseCase
+  ft <- SC.scAbstractTerms sc [r] body
   validateTerm sc
     ("constructing an override replacement for " <> URI.render (thm ^. theoremURI))
     ft
@@ -103,13 +99,12 @@ theoremReplacement sc thm = do
 -- | Given a SAWCore term corresponding to an HDL module, a specification, and a precondition:
 -- Construct a theorem summarizing the relationship between the module and the specification.
 buildTheorem ::
-  (MonadIO m, MonadThrow m) =>
   SC.SharedContext ->
   SC.TypedTerm ->
   SC.Term ->
   Maybe SC.TypedTerm ->
   SC.TypedTerm ->
-  m YosysTheorem
+  IO YosysTheorem
 buildTheorem sc ymod newmod precond body = do
   cty <- case SC.ttType ymod of
     SC.TypedTermSchema (C.Forall [] [] cty) -> pure cty
@@ -117,8 +112,8 @@ buildTheorem sc ymod newmod precond body = do
   (cinpTy, coutTy) <- case cty of
     C.TCon (C.TC C.TCFun) [ci, co] -> pure (ci, co)
     _ -> throw YosysErrorInvalidOverrideTarget
-  inpTy <- liftIO $ CSC.importType sc CSC.emptyEnv cinpTy
-  outTy <- liftIO $ CSC.importType sc CSC.emptyEnv coutTy
+  inpTy <- CSC.importType sc CSC.emptyEnv cinpTy
+  outTy <- CSC.importType sc CSC.emptyEnv coutTy
   nmi <- case reduceSelectors (SC.ttTerm ymod) of
     (R.asConstant -> Just (SC.Name _ nmi)) -> pure nmi
     _ -> throw YosysErrorInvalidOverrideTarget
@@ -161,22 +156,20 @@ reduceSelectors t =
 --     {{ \r -> if thm.theoremPrecond r then thm.theoremBody r else thm.theoremURI r }}
 --     in the presence of a precondition
 applyOverride ::
-  forall m.
-  (MonadIO m, MonadThrow m) =>
   SC.SharedContext ->
   YosysTheorem ->
   SC.Term ->
-  m SC.Term
+  IO SC.Term
 applyOverride sc thm t = do
-  tidx <- liftIO (SC.scResolveNameByURI sc $ thm ^. theoremURI) >>= \case
+  tidx <- (SC.scResolveNameByURI sc $ thm ^. theoremURI) >>= \case
     Nothing -> throw . YosysErrorOverrideNameNotFound . URI.render $ thm ^. theoremURI
     Just i -> pure i
   -- unfold everything except for theoremURI and prelude constants
   let isPreludeName (SC.ModuleIdentifier ident) = SC.identModule ident == SC.preludeModuleName
       isPreludeName _ = False
   let unfold nm = SC.nameIndex nm /= tidx && not (isPreludeName (SC.nameInfo nm))
-  unfolded <- liftIO $ SC.scUnfoldConstants sc unfold t
-  cache <- liftIO SC.newCache
+  unfolded <- SC.scUnfoldConstants sc unfold t
+  cache <- SC.newCache
   let
     go :: SC.Term -> IO SC.Term
     go s@SC.STApp { SC.stAppIndex = aidx, SC.stAppTermF = tf } = SC.useCache cache aidx $ case tf of
@@ -184,7 +177,7 @@ applyOverride sc thm t = do
         | idx == tidx -> theoremReplacement sc thm
         | otherwise -> pure s
       _ -> SC.scTermF sc =<< traverse go tf
-  ft <- liftIO $ go unfolded
+  ft <- go unfolded
   validateTerm sc
     ("applying an override for " <> URI.render (thm ^. theoremURI))
     ft
diff --git a/saw-central/src/SAWCentral/Yosys/TransitionSystem.hs b/saw-central/src/SAWCentral/Yosys/TransitionSystem.hs
index 5a47e2978f..be625c6afb 100644
--- a/saw-central/src/SAWCentral/Yosys/TransitionSystem.hs
+++ b/saw-central/src/SAWCentral/Yosys/TransitionSystem.hs
@@ -22,7 +22,6 @@ import Control.Lens.TH (makeLenses)
 
 import Control.Lens ((^.), view, at)
 import Control.Monad (forM, foldM)
-import Control.Monad.IO.Class (MonadIO(..))
 import Control.Exception (throw)
 
 import Data.Functor.Const (Const(..))
@@ -80,10 +79,8 @@ makeLenses ''SequentialFields
 -- | Convert a mapping from names to widths into a typed mapping from
 -- those names to What4 bitvectors of those widths.
 sequentialReprs ::
-  forall m.
-  MonadIO m =>
   Map Text Natural ->
-  m (Some SequentialFields)
+  IO (Some SequentialFields)
 sequentialReprs fs = do
   let assocs = Map.assocs fs
   Some fields <- go assocs
@@ -94,7 +91,7 @@ sequentialReprs fs = do
     , _sequentialFieldsIndex = Map.fromList index
     }
   where
-    go :: [(Text, Natural)] -> m (Some (Ctx.Assignment SequentialField))
+    go :: [(Text, Natural)] -> IO (Some (Ctx.Assignment SequentialField))
     go [] = pure $ Some Ctx.empty
     go ((nm, n):ns) = case someNat n of
       Just (Some nr) | Just LeqProof <- testLeq (knownNat @1) nr -> do
@@ -113,23 +110,22 @@ sequentialReprs fs = do
 -- struct into a representation that is more convenient to manipulate
 -- in SAWCore.)
 ecBindingsOfFields ::
-  MonadIO m =>
   W4.B.ExprBuilder n st fs ->
   SC.SharedContext ->
   Text {- ^ Prefix to prepend to all field names -} ->
   Map Text SC.Term {- ^ Mapping from field names to SAWCore types -} ->
   SequentialFields ctx {- ^ Mapping from field names to What4 base types -} ->
   W4.SymStruct (W4.B.ExprBuilder n st fs) ctx {- ^ What4 record to deconstruct -} ->
-  m (Map Text (SC.VarName, SC.Term, SimW4.SValue (W4.B.ExprBuilder n st fs)))
+  IO (Map Text (SC.VarName, SC.Term, SimW4.SValue (W4.B.ExprBuilder n st fs)))
 ecBindingsOfFields sym sc pfx fs s inp = fmap Map.fromList . forM (Map.assocs fs) $ \(baseName, ty) -> do
   let nm = pfx <> baseName
-  vn <- liftIO $ SC.scFreshVarName sc nm
+  vn <- SC.scFreshVarName sc nm
   val <- case s ^. sequentialFieldsIndex . at nm of
     Just (Some idx)
       | sf <- s ^. sequentialFields . ixF' idx
       , W4.BaseBVRepr _nr <- sf ^. sequentialFieldTypeRepr
         -> do
-          inpExpr <- liftIO $ W4.structField sym inp idx
+          inpExpr <- W4.structField sym inp idx
           pure . Sim.VWord $ W4.DBV inpExpr
     _ -> throw $ YosysErrorTransitionSystemMissingField nm
   pure (baseName, (vn, ty, val))
@@ -137,14 +133,13 @@ ecBindingsOfFields sym sc pfx fs s inp = fmap Map.fromList . forM (Map.assocs fs
 -- | Given a sequential circuit and a query, construct and write to
 -- disk a Sally transition system encoding that query.
 queryModelChecker ::
-  MonadIO m =>
   W4.B.ExprBuilder n st fs ->
   SC.SharedContext ->
   YosysSequential ->
   FilePath {- ^ Path to write the resulting Sally input -} ->
   SC.TypedTerm {- ^ A boolean function of three parameters: an 8-bit cycle counter, a record of "fixed" inputs, and a record of circuit outputs -} ->
   Set Text {- ^ Names of circuit inputs that are fixed -}->
-  m ()
+  IO ()
 queryModelChecker sym sc sequential path query fixedInputs = do
   -- there are 5 classes of field:
   --  - fixed inputs (inputs from the circuit named in the fixed set, assumed to be constant across cycles
@@ -155,7 +150,7 @@ queryModelChecker sym sc sequential path query fixedInputs = do
   let (fixedInputWidths, variableInputWidths) = Map.partitionWithKey (\nm _ -> Set.member nm fixedInputs) $ sequential ^. yosysSequentialInputWidths
   let (fixedInputFields, variableInputFields) = Map.partitionWithKey (\nm _ -> Set.member nm fixedInputs) $ sequential ^. yosysSequentialInputFields
   let internalWidths = Map.singleton "cycle" 8
-  internalFields <- forM internalWidths $ \w -> liftIO $ SC.scBitvector sc w
+  internalFields <- forM internalWidths $ \w -> SC.scBitvector sc w
 
   -- the "inputs" for our transition system are exclusively the circuit's variable inputs
   Some inputFields <- sequentialReprs variableInputWidths
@@ -217,31 +212,31 @@ queryModelChecker sym sc sequential path query fixedInputs = do
             states <- forM curBindings $ \(vn, tp, _) -> SC.scVariable sc vn tp
             inpst <- cryptolRecord sc states
             domainRec <- cryptolRecord sc $ Map.insert "__state__" inpst inps
-            codomainRec <- liftIO $ SC.scApply sc (sequential ^. yosysSequentialTerm . SC.ttTermLens) domainRec
+            codomainRec <- SC.scApply sc (sequential ^. yosysSequentialTerm . SC.ttTermLens) domainRec
             codomainFields <- insertStateField sc (sequential ^. yosysSequentialStateFields) $ sequential ^. yosysSequentialOutputFields
             outst <- cryptolRecordSelect sc codomainFields codomainRec "__state__"
             stPreds <- forM (Map.assocs $ sequential ^. yosysSequentialStateWidths) $ \(nm, w) -> do
               val <- cryptolRecordSelect sc (sequential ^. yosysSequentialStateFields) outst nm
               wnat <- SC.scNat sc w
               new <- lookupBinding nm nextBindings
-              liftIO $ SC.scBvEq sc wnat new val
+              SC.scBvEq sc wnat new val
             outputPreds <- forM (Map.assocs $ sequential ^. yosysSequentialOutputWidths) $ \(nm, w) -> do
               val <- cryptolRecordSelect sc codomainFields codomainRec nm
               wnat <- SC.scNat sc w
               new <- lookupBinding nm nextOutputBindings
-              liftIO $ SC.scBvEq sc wnat new val
+              SC.scBvEq sc wnat new val
             fixedInputPreds <- forM (Map.assocs fixedInputWidths) $ \(nm, w) -> do
               wnat <- SC.scNat sc w
               val <- lookupBinding nm curFixedInputBindings
               new <- lookupBinding nm nextFixedInputBindings
-              liftIO $ SC.scBvEq sc wnat new val
+              SC.scBvEq sc wnat new val
             cycleIncrement <- do
               wnat <- SC.scNat sc 8
               val <- lookupBinding "cycle" curInternalBindings
               one <- SC.scBvConst sc 8 1
               incremented <- SC.scBvAdd sc wnat val one
               new <- lookupBinding "cycle" nextInternalBindings
-              liftIO $ SC.scBvEq sc wnat new incremented
+              SC.scBvEq sc wnat new incremented
             identity <- SC.scBool sc True
             conj <- foldM (SC.scAnd sc) identity $ stPreds <> outputPreds <> fixedInputPreds <> [cycleIncrement]
             ref <- IORef.newIORef Map.empty
@@ -278,7 +273,7 @@ queryModelChecker sym sc sequential path query fixedInputs = do
             cycleVal <- lookupBinding "cycle" curInternalBindings
             fixedInputRec <- cryptolRecord sc fixedInps
             outputRec <- cryptolRecord sc outputs
-            result <- liftIO $ SC.scApplyAll sc (query ^. SC.ttTermLens) [cycleVal, fixedInputRec, outputRec]
+            result <- SC.scApplyAll sc (query ^. SC.ttTermLens) [cycleVal, fixedInputRec, outputRec]
             ref <- IORef.newIORef Map.empty
             let args = Map.unions $ fmap (Map.fromList . fmap (\(vn, _ty, x) -> (SC.vnIndex vn, x)) . Map.elems)
                   [ curOutputBindings
@@ -291,7 +286,7 @@ queryModelChecker sym sc sequential path query fixedInputs = do
               _ -> throw . YosysError $ "Invalid type when converting predicate to What4: " <> Text.pack (show sval)
             pure [w4Pred]
         }
-  sts <- liftIO $ Sally.exportTransitionSystem sym Sally.mySallyNames ts
-  sexp <- liftIO $ Sally.sexpOfSally sym sts
-  liftIO . BS.writeFile path . encodeUtf8 . Text.pack . show $ Sally.sexpToDoc sexp
+  sts <- Sally.exportTransitionSystem sym Sally.mySallyNames ts
+  sexp <- Sally.sexpOfSally sym sts
+  BS.writeFile path . encodeUtf8 . Text.pack . show $ Sally.sexpToDoc sexp
   pure ()
diff --git a/saw-central/src/SAWCentral/Yosys/Utils.hs b/saw-central/src/SAWCentral/Yosys/Utils.hs
index 2abfa372aa..998771d7d6 100644
--- a/saw-central/src/SAWCentral/Yosys/Utils.hs
+++ b/saw-central/src/SAWCentral/Yosys/Utils.hs
@@ -16,9 +16,7 @@ Stability   : experimental
 module SAWCentral.Yosys.Utils where
 
 import Control.Monad (forM, foldM)
-import Control.Monad.IO.Class (MonadIO(..))
-import Control.Exception (Exception, throw)
-import Control.Monad.Catch (MonadThrow)
+import Control.Exception (Exception, throwIO)
 
 import Data.Bifunctor (bimap)
 import qualified Data.List as List
@@ -140,60 +138,57 @@ reverseTopSort =
 #endif
 
 -- | Check that a SAWCore term is well-typed, throwing an exception otherwise.
-validateTerm :: MonadIO m => SC.SharedContext -> Text -> SC.Term -> m SC.Term
-validateTerm sc msg t = liftIO (SC.TC.scTypeCheck sc t) >>= \case
-  Right _ -> pure t
-  Left err ->
-    throw
-    . YosysErrorTypeError msg
-    . Text.pack
-    . unlines
-    $ SC.TC.prettyTCError err
+validateTerm :: SC.SharedContext -> Text -> SC.Term -> IO SC.Term
+validateTerm sc msg t =
+  do result <- SC.TC.scTypeCheck sc t
+     case result of
+       Right _ -> pure t
+       Left err ->
+         throwIO $
+         YosysErrorTypeError msg $
+         Text.pack $ unlines $ SC.TC.prettyTCError err
 
 -- | Check that a SAWCore term is well-typed and has a specific type
-validateTermAtType :: MonadIO m => SC.SharedContext -> Text ->
-                      SC.Term -> SC.Term -> m ()
+validateTermAtType :: SC.SharedContext -> Text -> SC.Term -> SC.Term -> IO ()
 validateTermAtType sc msg trm tp =
-  liftIO (SC.TC.runTCM (SC.TC.typeInferComplete trm >>= \tp_trm ->
-                         SC.TC.checkSubtype tp_trm tp) sc) >>= \case
-  Right _ -> return ()
-  Left err ->
-    throw
-    . YosysErrorTypeError msg
-    . Text.pack
-    . unlines
-    $ SC.TC.prettyTCError err
+  do let check =
+           do tp_trm <- SC.TC.typeInferComplete trm
+              SC.TC.checkSubtype tp_trm tp
+     result <- SC.TC.runTCM check sc
+     case result of
+       Right _ -> pure ()
+       Left err ->
+         throwIO $
+         YosysErrorTypeError msg $
+         Text.pack $ unlines $ SC.TC.prettyTCError err
 
 -- | Produce a SAWCore tuple type corresponding to a Cryptol record type with the given fields.
 cryptolRecordType ::
-  MonadIO m =>
   SC.SharedContext ->
   Map Text SC.Term ->
-  m SC.Term
+  IO SC.Term
 cryptolRecordType sc fields =
-  liftIO $ SC.scTupleType sc (fmap snd . C.canonicalFields . C.recordFromFields $ Map.assocs fields)
+  SC.scTupleType sc (fmap snd . C.canonicalFields . C.recordFromFields $ Map.assocs fields)
 
 -- | Produce a SAWCore tuple corresponding to a Cryptol record with the given fields.
 cryptolRecord ::
-  MonadIO m =>
   SC.SharedContext ->
   Map Text SC.Term ->
-  m SC.Term
+  IO SC.Term
 cryptolRecord sc fields =
-  liftIO $ SC.scTuple sc (fmap snd . C.canonicalFields . C.recordFromFields $ Map.assocs fields)
+  SC.scTuple sc (fmap snd . C.canonicalFields . C.recordFromFields $ Map.assocs fields)
 
 -- | Produce a SAWCore tuple index corresponding to a lookup in a Cryptol record with the given fields.
 cryptolRecordSelect ::
-  MonadIO m =>
   SC.SharedContext ->
   Map Text a ->
   SC.Term ->
   Text ->
-  m SC.Term
+  IO SC.Term
 cryptolRecordSelect sc fields r nm =
   case List.elemIndex nm ord of
-    Just i -> liftIO $ SC.scTupleSelector sc r (i + 1) (length ord)
-    Nothing -> throw . YosysError $ mconcat
+    Just i -> SC.scTupleSelector sc r (i + 1) (length ord)
+    Nothing -> throwIO $ YosysError $ mconcat
       [ "Could not build record selector term for field name \""
       , nm
       , "\" on record term: "
@@ -207,22 +202,21 @@ cryptolRecordSelect sc fields r nm =
 -- Cryptol record. The record fields are inferred from the Cryptol
 -- type attached to the `TypedTerm`.
 cryptolRecordSelectTyped ::
-  MonadIO m =>
   SC.SharedContext ->
   SC.TypedTerm ->
   Text ->
-  m SC.TypedTerm
+  IO SC.TypedTerm
 cryptolRecordSelectTyped sc r nm = do
   fields <- Map.mapKeys C.identText . Map.fromList . C.canonicalFields <$> case SC.ttType r of
     SC.TypedTermSchema (C.Forall [] [] (C.TRec fs)) -> pure fs
-    _ -> throw . YosysError $ mconcat
+    _ -> throwIO $ YosysError $ mconcat
       [ "Type\n"
       , Text.pack . show $ SC.ttType r
       , "\nis not a record type"
       ]
   cty <- case Map.lookup nm fields of
     Just cty -> pure cty
-    _ -> throw . YosysError $ mconcat
+    _ -> throwIO $ YosysError $ mconcat
       [ "Record type\n"
       , Text.pack . show $ SC.ttType r
       , "\ndoes not have field "
@@ -235,16 +229,15 @@ cryptolRecordSelectTyped sc r nm = do
 -- field of two records. Both records should be tuples corresponding
 -- to the specified Cryptol record type.
 eqBvRecords ::
-  (MonadIO m, MonadThrow m) =>
   SC.SharedContext ->
   C.Type ->
   SC.Term ->
   SC.Term ->
-  m SC.Term
+  IO SC.Term
 eqBvRecords sc cty a b = do
   fields <- Map.mapKeys C.identText . Map.fromList . C.canonicalFields <$> case cty of
     C.TRec fs -> pure fs
-    _ -> throw . YosysError $ mconcat
+    _ -> throwIO $ YosysError $ mconcat
       [ "Type\n"
       , Text.pack $ show cty
       , "\nis not a record type"
@@ -252,22 +245,22 @@ eqBvRecords sc cty a b = do
   eqs <- forM (Map.assocs fields) $ \(nm, fcty) -> do
     w <- case fcty of
       C.TCon (C.TC C.TCSeq) [C.TCon (C.TC (C.TCNum wint)) [], C.TCon (C.TC C.TCBit) []] ->
-        liftIO . SC.scNat sc $ fromIntegral wint
-      _ -> throw . YosysError $ mconcat
+        SC.scNat sc $ fromIntegral wint
+      _ -> throwIO $  YosysError $ mconcat
         [ "Type\n"
         , Text.pack $ show fcty
         , "\nis not a bitvector type"
         ]
     fa <- cryptolRecordSelect sc fields a nm
     fb <- cryptolRecordSelect sc fields b nm
-    liftIO $ SC.scBvEq sc w fa fb
+    SC.scBvEq sc w fa fb
   case eqs of
-    [] -> throw . YosysError $ mconcat
+    [] -> throwIO $ YosysError $ mconcat
       [ "Record type\n"
       , Text.pack $ show cty
       , "\nhas no fields"
       ]
-    (e:es) -> foldM (\x y -> liftIO $ SC.scAnd sc x y) e es
+    (e:es) -> foldM (\x y -> SC.scAnd sc x y) e es
 
 -- | Encode the given string such that is a valid Cryptol identifier.
 -- Since Yosys cell names often look like "\42", this makes it much
@@ -278,23 +271,20 @@ cellIdentifier = Text.pack . zEncodeString . Text.unpack
 -- | Build a SAWCore type corresponding to the Cryptol record type
 -- with the given field types.
 fieldsToType ::
-  MonadIO m =>
   SC.SharedContext ->
   Map Text (SC.Term, C.Type) ->
-  m SC.Term
+  IO SC.Term
 fieldsToType sc = cryptolRecordType sc . fmap fst
 
 -- | Build a Cryptol record type with the given field types
 fieldsToCryptolType ::
-  MonadIO m =>
-  Map Text (SC.Term, C.Type) ->
-  m C.Type
+  Map Text (SC.Term, C.Type) -> IO C.Type
 fieldsToCryptolType fields = pure . C.tRec . C.recordFromFields $ bimap C.mkIdent snd <$> Map.assocs fields
 
 -- | Given a bit pattern ([b]) and a term, construct a map associating
 -- that output pattern with the term, and each bit of that pattern
 -- with the corresponding bit of the term.
-deriveTermsByIndices :: (MonadIO m, Ord b) => SC.SharedContext -> [b] -> SC.Term -> m (Map [b] Preterm)
+deriveTermsByIndices :: (Ord b) => SC.SharedContext -> [b] -> SC.Term -> IO (Map [b] Preterm)
 deriveTermsByIndices _sc rep t = do
   let len = length rep
   let bit i = PretermSlice (fromIntegral (len - 1 - i)) 1 (fromIntegral i) t
@@ -365,7 +355,7 @@ scPreterm sc p =
          i' <- SC.scNat sc i
          SC.scSingle sc boolty =<< SC.scAt sc n' boolty t i'
     PretermSlice i j k t ->
-      do boolty <- liftIO $ SC.scBoolType sc
+      do boolty <- SC.scBoolType sc
          i' <- SC.scNat sc i
          j' <- SC.scNat sc j
          k' <- SC.scNat sc k
diff --git a/saw-server/src/SAWServer/Yosys.hs b/saw-server/src/SAWServer/Yosys.hs
index 158e3d527d..e09ee3aded 100644
--- a/saw-server/src/SAWServer/Yosys.hs
+++ b/saw-server/src/SAWServer/Yosys.hs
@@ -60,8 +60,8 @@ yosysImport params = do
     [] -> do
       imp <- tl $ do
         sc <- getSharedContext
-        ir <- loadYosysIR $ yosysImportPath params
-        YosysImport <$> yosysIRToTypedTerms sc ir
+        ir <- liftIO $ loadYosysIR $ yosysImportPath params
+        liftIO $ YosysImport <$> yosysIRToTypedTerms sc ir
       setServerVal (yosysImportServerName params) imp
       ok
 

From ac8c52bb67c871a9e6dc4a17f0e848f61f8ae31a Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 17 Nov 2025 21:04:46 -0800
Subject: [PATCH 2/4] saw-central/Yosys: Reindent and lay out code.

For readability, 'do' and 'case' go on the left.
---
 saw-central/src/SAWCentral/Yosys.hs           | 152 +++---
 saw-central/src/SAWCentral/Yosys/Cell.hs      | 492 +++++++++---------
 saw-central/src/SAWCentral/Yosys/Netgraph.hs  | 197 +++----
 saw-central/src/SAWCentral/Yosys/State.hs     | 390 +++++++-------
 saw-central/src/SAWCentral/Yosys/Theorem.hs   | 108 ++--
 .../src/SAWCentral/Yosys/TransitionSystem.hs  | 369 ++++++-------
 saw-central/src/SAWCentral/Yosys/Utils.hs     | 114 ++--
 7 files changed, 941 insertions(+), 881 deletions(-)

diff --git a/saw-central/src/SAWCentral/Yosys.hs b/saw-central/src/SAWCentral/Yosys.hs
index db01bec9c1..29a70beccd 100644
--- a/saw-central/src/SAWCentral/Yosys.hs
+++ b/saw-central/src/SAWCentral/Yosys.hs
@@ -10,7 +10,6 @@ Stability   : experimental
 {-# Language OverloadedStrings #-}
 {-# Language RecordWildCards #-}
 {-# Language ViewPatterns #-}
-{-# Language LambdaCase #-}
 {-# Language MultiWayIf #-}
 {-# Language TupleSections #-}
 {-# Language ScopedTypeVariables #-}
@@ -93,54 +92,54 @@ convertYosysIR ::
   SC.SharedContext ->
   YosysIR ->
   IO (Map Text ConvertedModule)
-convertYosysIR sc ir = do
-  let mg = yosysIRModgraph ir
-  let sorted = reverseTopSort $ mg ^. modgraphGraph
-  foldM
-    (\env v -> do
-        let (m, nm, _) = mg ^. modgraphNodeFromVertex $ v
-        cm <- convertModule sc env m
-        _ <- validateTerm sc ("translating the combinational circuit \"" <> nm <> "\"") $ cm ^. convertedModuleTerm
-        n <- Nonce.freshNonce Nonce.globalNonceGenerator
-        let frag = Text.pack . show $ Nonce.indexValue n
-        let uri = URI.URI
-              { URI.uriScheme = URI.mkScheme "yosys"
-              , URI.uriAuthority = Left True
-              , URI.uriPath = (False,) <$> mapM URI.mkPathPiece (nm NE.:| [])
-              , URI.uriQuery = []
-              , URI.uriFragment = URI.mkFragment frag
-              }
-        let ni = SC.ImportedName uri [nm]
-        tc <- SC.scDefineConstant sc ni (cm ^. convertedModuleTerm) (cm ^. convertedModuleType)
-        let cm' = cm { _convertedModuleTerm = tc }
-        pure $ Map.insert nm cm' env
-    )
-    Map.empty
-    sorted
+convertYosysIR sc ir =
+  do let mg = yosysIRModgraph ir
+     let sorted = reverseTopSort $ mg ^. modgraphGraph
+     foldM
+       (\env v ->
+          do let (m, nm, _) = mg ^. modgraphNodeFromVertex $ v
+             cm <- convertModule sc env m
+             _ <- validateTerm sc ("translating the combinational circuit \"" <> nm <> "\"") $ cm ^. convertedModuleTerm
+             n <- Nonce.freshNonce Nonce.globalNonceGenerator
+             let frag = Text.pack . show $ Nonce.indexValue n
+             let uri = URI.URI
+                   { URI.uriScheme = URI.mkScheme "yosys"
+                   , URI.uriAuthority = Left True
+                   , URI.uriPath = (False,) <$> mapM URI.mkPathPiece (nm NE.:| [])
+                   , URI.uriQuery = []
+                   , URI.uriFragment = URI.mkFragment frag
+                   }
+             let ni = SC.ImportedName uri [nm]
+             tc <- SC.scDefineConstant sc ni (cm ^. convertedModuleTerm) (cm ^. convertedModuleType)
+             let cm' = cm { _convertedModuleTerm = tc }
+             pure $ Map.insert nm cm' env
+       )
+       Map.empty
+       sorted
 
 -- | Given a Yosys IR, construct a map from module names to TypedTerms
 yosysIRToTypedTerms ::
   SC.SharedContext ->
   YosysIR ->
   IO (Map Text SC.TypedTerm)
-yosysIRToTypedTerms sc ir = do
-  env <- convertYosysIR sc ir
-  pure . flip fmap env $ \cm ->
-    SC.TypedTerm
-    (SC.TypedTermSchema $ C.tMono $ cm ^. convertedModuleCryptolType)
-    $ cm ^. convertedModuleTerm
+yosysIRToTypedTerms sc ir =
+  do env <- convertYosysIR sc ir
+     pure $ flip fmap env $ \cm ->
+       SC.TypedTerm
+       (SC.TypedTermSchema $ C.tMono $ cm ^. convertedModuleCryptolType)
+       $ cm ^. convertedModuleTerm
 
 -- | Given a Yosys IR, construct a SAWCore record containing terms for each module
 yosysIRToRecordTerm ::
   SC.SharedContext ->
   YosysIR ->
   IO SC.TypedTerm
-yosysIRToRecordTerm sc ir = do
-  env <- convertYosysIR sc ir
-  record <- cryptolRecord sc $ view convertedModuleTerm <$> env
-  let cty = C.tRec . C.recordFromFields $ (\(nm, cm) -> (C.mkIdent nm, cm ^. convertedModuleCryptolType)) <$> Map.assocs env
-  let tt = SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) record
-  pure tt
+yosysIRToRecordTerm sc ir =
+  do env <- convertYosysIR sc ir
+     record <- cryptolRecord sc $ view convertedModuleTerm <$> env
+     let cty = C.tRec . C.recordFromFields $ (\(nm, cm) -> (C.mkIdent nm, cm ^. convertedModuleCryptolType)) <$> Map.assocs env
+     let tt = SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) record
+     pure tt
 
 -- | Given a Yosys IR, construct a value representing a specific module with all submodules inlined
 yosysIRToSequential ::
@@ -148,7 +147,7 @@ yosysIRToSequential ::
   YosysIR ->
   Text ->
   IO YosysSequential
-yosysIRToSequential sc ir nm = do
+yosysIRToSequential sc ir nm =
   case Map.lookup nm $ ir ^. yosysModules of
     Nothing -> throw . YosysError $ mconcat
       [ "Could not find module: "
@@ -167,12 +166,12 @@ yosysIRToSequential sc ir nm = do
 -- Each HDL module is in turn represented by a function from a record
 -- of input port values to a record of output port values.
 yosys_import :: FilePath -> TopLevel SC.TypedTerm
-yosys_import path = do
-  sc <- getSharedContext
-  ir <- liftIO $ loadYosysIR path
-  tt <- liftIO $ yosysIRToRecordTerm sc ir
-  _ <- liftIO $ validateTerm sc "translating combinational circuits" $ SC.ttTerm tt
-  pure tt
+yosys_import path =
+  do sc <- getSharedContext
+     ir <- liftIO $ loadYosysIR path
+     tt <- liftIO $ yosysIRToRecordTerm sc ir
+     _ <- liftIO $ validateTerm sc "translating combinational circuits" $ SC.ttTerm tt
+     pure tt
 
 -- | Proves equality between a combinational HDL module and a
 -- specification. Note that terms derived from HDL modules are first
@@ -187,20 +186,21 @@ yosys_verify ::
   [YosysTheorem] {- ^ Overrides to apply -} ->
   ProofScript () ->
   TopLevel YosysTheorem
-yosys_verify ymod preconds other specs tactic = do
-  sc <- getSharedContext
-  newmod <- liftIO $ foldM (flip $ applyOverride sc)
-    (SC.ttTerm ymod)
-    specs
-  mpc <- case preconds of
-    [] -> pure Nothing
-    (pc:pcs) -> do
-      t <- foldM (\a b -> liftIO $ SC.scAnd sc a b) (SC.ttTerm pc) (SC.ttTerm <$> pcs)
-      pure . Just $ SC.TypedTerm (SC.ttType pc) t
-  thm <- liftIO $ buildTheorem sc ymod newmod mpc other
-  prop <- liftIO $ theoremProp sc thm
-  _ <- Builtins.provePrintPrim tactic prop
-  pure thm
+yosys_verify ymod preconds other specs tactic =
+  do sc <- getSharedContext
+     newmod <- liftIO $ foldM (flip $ applyOverride sc)
+       (SC.ttTerm ymod)
+       specs
+     mpc <-
+       case preconds of
+         [] -> pure Nothing
+         (pc:pcs) ->
+           do t <- foldM (\a b -> liftIO $ SC.scAnd sc a b) (SC.ttTerm pc) (SC.ttTerm <$> pcs)
+              pure . Just $ SC.TypedTerm (SC.ttType pc) t
+     thm <- liftIO $ buildTheorem sc ymod newmod mpc other
+     prop <- liftIO $ theoremProp sc thm
+     _ <- Builtins.provePrintPrim tactic prop
+     pure thm
 
 -- | Import a single sequential HDL module. N.B. SAW expects the
 -- sequential module to exist entirely within a single Yosys module.
@@ -208,10 +208,10 @@ yosys_import_sequential ::
   Text {- ^ Name of the HDL module -} ->
   FilePath {- ^ Path to the Yosys JSON file -} ->
   TopLevel YosysSequential
-yosys_import_sequential nm path = do
-  sc <- getSharedContext
-  ir <- liftIO $ loadYosysIR path
-  liftIO $ yosysIRToSequential sc ir nm
+yosys_import_sequential nm path =
+  do sc <- getSharedContext
+     ir <- liftIO $ loadYosysIR path
+     liftIO $ yosysIRToSequential sc ir nm
 
 -- | Extracts a term from the given sequential module with the state
 -- eliminated by iterating the term over the given concrete number of
@@ -223,11 +223,11 @@ yosys_extract_sequential ::
   YosysSequential ->
   Integer {- ^ Number of cycles to iterate term -} ->
   TopLevel SC.TypedTerm
-yosys_extract_sequential s n = do
-  sc <- getSharedContext
-  tt <- liftIO $ composeYosysSequential sc s n
-  _ <- liftIO $ validateTerm sc "composing a sequential term" $ SC.ttTerm tt
-  pure tt
+yosys_extract_sequential s n =
+  do sc <- getSharedContext
+     tt <- liftIO $ composeYosysSequential sc s n
+     _ <- liftIO $ validateTerm sc "composing a sequential term" $ SC.ttTerm tt
+     pure tt
 
 -- | Like `yosys_extract_sequential`, but the resulting term has an
 -- additional parameter to specify the initial state.
@@ -235,11 +235,11 @@ yosys_extract_sequential_with_state ::
   YosysSequential ->
   Integer {- ^ Number of cycles to iterate term -} ->
   TopLevel SC.TypedTerm
-yosys_extract_sequential_with_state s n = do
-  sc <- getSharedContext
-  tt <- liftIO $ composeYosysSequentialWithState sc s n
-  _ <- liftIO $ validateTerm sc "composing a sequential term with state" $ SC.ttTerm tt
-  pure tt
+yosys_extract_sequential_with_state s n =
+  do sc <- getSharedContext
+     tt <- liftIO $ composeYosysSequentialWithState sc s n
+     _ <- liftIO $ validateTerm sc "composing a sequential term with state" $ SC.ttTerm tt
+     pure tt
 
 -- | Extracts a term from the given sequential module. This term has
 -- explicit fields for the state of the circuit in the input and
@@ -254,7 +254,7 @@ yosys_verify_sequential_sally ::
   SC.TypedTerm {- ^ A boolean function of three parameters: an 8-bit cycle counter, a record of "fixed" inputs, and a record of circuit outputs -} ->
   [Text] {- ^ Names of circuit inputs that are fixed -} ->
   TopLevel ()
-yosys_verify_sequential_sally s path q fixed = do
-  sc <- getSharedContext
-  sym <- liftIO $ Common.newSAWCoreExprBuilder sc False
-  liftIO $ queryModelChecker sym sc s path q $ Set.fromList fixed
+yosys_verify_sequential_sally s path q fixed =
+  do sc <- getSharedContext
+     sym <- liftIO $ Common.newSAWCoreExprBuilder sc False
+     liftIO $ queryModelChecker sym sc s path q $ Set.fromList fixed
diff --git a/saw-central/src/SAWCentral/Yosys/Cell.hs b/saw-central/src/SAWCentral/Yosys/Cell.hs
index 2ae01d2b2e..d06ea44bd6 100644
--- a/saw-central/src/SAWCentral/Yosys/Cell.hs
+++ b/saw-central/src/SAWCentral/Yosys/Cell.hs
@@ -43,59 +43,59 @@ cellTermNat sc (CellTerm { cellTermTerm = t, cellTermWidth = w }) = SC.scBvToNat
 -- | Apply the appropriate (possibly signed) extension or truncation to make the given bitvector
 -- match the given width.
 extTrunc :: SC.SharedContext -> Natural -> CellTerm -> IO CellTerm
-extTrunc sc width (CellTerm { cellTermTerm = t, cellTermWidth = bvw, cellTermSigned = signed}) = do
-  wterm <- SC.scNat sc width
-  bvwterm <- SC.scNat sc bvw
-  res <- if
-    | bvw > width -> do
-        diffterm <- SC.scNat sc $ bvw - width
-        SC.scBvTrunc sc diffterm wterm t
-    | width > bvw && signed -> do
-        bvwpredterm <- SC.scNat sc $ bvw - 1
-        diffterm <- SC.scNat sc $ width - bvw
-        SC.scBvSExt sc diffterm bvwpredterm t
-    | width > bvw && not signed -> do
-        diffterm <- SC.scNat sc $ width - bvw
-        SC.scBvUExt sc diffterm bvwterm t
-    | otherwise -> pure t
-  pure $ CellTerm res width signed
+extTrunc sc width (CellTerm { cellTermTerm = t, cellTermWidth = bvw, cellTermSigned = signed}) =
+  do wterm <- SC.scNat sc width
+     bvwterm <- SC.scNat sc bvw
+     res <- if
+       | bvw > width ->
+           do diffterm <- SC.scNat sc $ bvw - width
+              SC.scBvTrunc sc diffterm wterm t
+       | width > bvw && signed ->
+           do bvwpredterm <- SC.scNat sc $ bvw - 1
+              diffterm <- SC.scNat sc $ width - bvw
+              SC.scBvSExt sc diffterm bvwpredterm t
+       | width > bvw && not signed ->
+           do diffterm <- SC.scNat sc $ width - bvw
+              SC.scBvUExt sc diffterm bvwterm t
+       | otherwise -> pure t
+     pure $ CellTerm res width signed
 
 -- | Given two bitvectors, extend the narrower bitvector to match the wider.
 extMax :: SC.SharedContext -> CellTerm -> CellTerm -> IO (CellTerm, CellTerm)
-extMax sc c1 c2 = do
-  let
-    w1 = cellTermWidth c1
-    w2 = cellTermWidth c2
-    w = max w1 w2
-  res1 <- extTrunc sc w c1
-  res2 <- extTrunc sc w c2
-  pure (res1, res2)
+extMax sc c1 c2 =
+  do let
+       w1 = cellTermWidth c1
+       w2 = cellTermWidth c2
+       w = max w1 w2
+     res1 <- extTrunc sc w c1
+     res2 <- extTrunc sc w c2
+     pure (res1, res2)
 
 liftUnary ::
   SC.SharedContext ->
   (SC.Term -> SC.Term -> IO SC.Term) -> -- (w : Nat) -> [w] -> [w]
   CellTerm -> IO CellTerm
-liftUnary sc f c@(CellTerm { cellTermTerm = t }) = do
-  wt <- SC.scNat sc $ cellTermWidth c
-  res <- f wt t
-  pure $ c { cellTermTerm = res }
+liftUnary sc f c@(CellTerm { cellTermTerm = t }) =
+  do wt <- SC.scNat sc $ cellTermWidth c
+     res <- f wt t
+     pure $ c { cellTermTerm = res }
 
 liftBinary ::
   SC.SharedContext ->
   (SC.Term -> SC.Term -> SC.Term -> IO SC.Term) -> -- (w : Nat) -> [w] -> [w] -> [w]
   CellTerm -> CellTerm -> IO CellTerm
-liftBinary sc f c1@(CellTerm { cellTermTerm = t1 }) (CellTerm { cellTermTerm = t2 }) = do
-  wt <- SC.scNat sc $ cellTermWidth c1
-  res <- f wt t1 t2
-  pure $ c1 { cellTermTerm = res }
+liftBinary sc f c1@(CellTerm { cellTermTerm = t1 }) (CellTerm { cellTermTerm = t2 }) =
+  do wt <- SC.scNat sc $ cellTermWidth c1
+     res <- f wt t1 t2
+     pure $ c1 { cellTermTerm = res }
 
 liftBinaryCmp ::
   SC.SharedContext ->
   (SC.Term -> SC.Term -> SC.Term -> IO SC.Term) -> -- (w : Nat) -> [w] -> [w] -> Bool
   CellTerm -> CellTerm -> IO SC.Term
-liftBinaryCmp sc f c1@(CellTerm { cellTermTerm = t1 }) (CellTerm { cellTermTerm = t2 }) = do
-  wt <- SC.scNat sc $ cellTermWidth c1
-  f wt t1 t2
+liftBinaryCmp sc f c1@(CellTerm { cellTermTerm = t1 }) (CellTerm { cellTermTerm = t2 }) =
+  do wt <- SC.scNat sc $ cellTermWidth c1
+     f wt t1 t2
 
 -- | Given a primitive Yosys cell and a map of terms for its
 -- arguments, construct a record term representing the output. If the
@@ -106,10 +106,10 @@ primCellToTerm ::
   Cell [b] {- ^ Cell type -} ->
   Map Text SC.Term {- ^ Mapping of input names to input terms -} ->
   IO (Maybe SC.Term)
-primCellToTerm sc c args = do
-  mm <- primCellToMap sc c args
-  mt <- traverse (cryptolRecord sc) mm
-  traverse (validateTerm sc typeCheckMsg) mt
+primCellToTerm sc c args =
+  do mm <- primCellToMap sc c args
+     mt <- traverse (cryptolRecord sc) mm
+     traverse (validateTerm sc typeCheckMsg) mt
   where
     typeCheckMsg :: Text
     typeCheckMsg = mconcat
@@ -124,171 +124,184 @@ primCellToMap ::
   Cell [b] {- ^ Cell type -} ->
   Map Text SC.Term {- ^ Mapping of input names to input terms -} ->
   IO (Maybe (Map Text SC.Term))
-primCellToMap sc c args = case c ^. cellType of
-  CellTypeNot -> bvUnaryOp . liftUnary sc $ SC.scBvNot sc
-  CellTypePos -> do
-    res <- input "A"
-    output res
-  CellTypeNeg -> bvUnaryOp . liftUnary sc $ SC.scBvNeg sc
-  CellTypeAnd -> bvBinaryOp . liftBinary sc $ SC.scBvAnd sc
-  CellTypeOr -> bvBinaryOp . liftBinary sc $ SC.scBvOr sc
-  CellTypeXor -> bvBinaryOp . liftBinary sc $ SC.scBvXor sc
-  CellTypeXnor -> bvBinaryOp . liftBinary sc $ \w x y -> do
-    r <- SC.scBvXor sc w x y
-    SC.scBvNot sc w r
-  CellTypeReduceAnd -> bvReduce True =<< do
-    SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "and"
-  CellTypeReduceOr -> bvReduce False =<< do
-    SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "or"
-  CellTypeReduceXor -> bvReduce False =<< do
-    SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "xor"
-  CellTypeReduceXnor -> bvReduce True =<< do
-    boolTy <- SC.scBoolType sc
-    x <- SC.scFreshVariable sc "x" boolTy
-    y <- SC.scFreshVariable sc "y" boolTy
-    r <- SC.scXor sc x y
-    res <- SC.scNot sc r
-    SC.scAbstractTerms sc [x, y] res
-  CellTypeReduceBool -> bvReduce False =<< do
-    SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "or"
-  CellTypeShl -> do
-    ta <- fmap cellTermTerm $ input "A"
-    nb <- cellTermNat sc =<< input "B"
-    w <- outputWidth
-    res <- SC.scBvShl sc w ta nb
-    output (CellTerm res (connWidthNat "A") (connSigned "A"))
-  CellTypeShr -> do
-    ta <- fmap cellTermTerm $ input "A"
-    nb <- cellTermNat sc =<< input "B"
-    w <- outputWidth
-    res <- SC.scBvShr sc w ta nb
-    output (CellTerm res (connWidthNat "A") (connSigned "A"))
-  CellTypeSshl -> do
-    ta <- fmap cellTermTerm $ input "A"
-    nb <- cellTermNat sc =<< input "B"
-    w <- outputWidth
-    res <- SC.scBvShl sc w ta nb
-    output (CellTerm res (connWidthNat "A") (connSigned "A"))
-  CellTypeSshr -> do
-    ta <- fmap cellTermTerm $ input "A"
-    nb <- cellTermNat sc =<< input "B"
-    w <- outputWidth
-    res <- SC.scBvSShr sc w ta nb
-    output (CellTerm res (connWidthNat "A") (connSigned "A"))
-  -- "$shift" -> _
-  CellTypeShiftx -> do
-    let w = max (connWidthNat "A") (connWidthNat "B")
-    wt <- SC.scNat sc w
-    CellTerm ta _ _ <- extTrunc sc w =<< input "A"
-    CellTerm tb _ _ <- extTrunc sc w =<< input "B"
-    zero <- SC.scBvConst sc w 0
-    tbn <- SC.scBvToNat sc w tb
-    tbneg <- SC.scBvNeg sc wt tb
-    tbnegn <- SC.scBvToNat sc w tbneg
-    cond <- SC.scBvSGe sc wt tb zero
-    tcase <- SC.scBvShr sc wt ta tbn
-    ecase <- SC.scBvShl sc wt ta tbnegn
-    ty <- SC.scBitvector sc $ connWidthNat "A"
-    res <- if connSigned "B"
-      then SC.scIte sc ty cond tcase ecase
-      else pure tcase
-    output (CellTerm res (connWidthNat "A") (connSigned "A"))
-  CellTypeLt -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvULt sc
-  CellTypeLe -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvULe sc
-  CellTypeGt -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvUGt sc
-  CellTypeGe -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvUGe sc
-  CellTypeEq -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvEq sc
-  CellTypeNe -> bvBinaryCmp . liftBinaryCmp sc $ \w x y -> do
-    r <- SC.scBvEq sc w x y
-    SC.scNot sc r
-  CellTypeEqx -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvEq sc
-  CellTypeNex -> bvBinaryCmp . liftBinaryCmp sc $ \w x y -> do
-    r <- SC.scBvEq sc w x y
-    SC.scNot sc r
-  CellTypeAdd -> bvBinaryOp . liftBinary sc $ SC.scBvAdd sc
-  CellTypeSub -> bvBinaryOp . liftBinary sc $ SC.scBvSub sc
-  CellTypeMul -> bvBinaryOp . liftBinary sc $ SC.scBvMul sc
-  CellTypeDiv -> bvBinaryOp . liftBinary sc $ SC.scBvUDiv sc
-  CellTypeMod -> bvBinaryOp . liftBinary sc $ SC.scBvURem sc
-  -- "$modfloor" -> _
-  CellTypeLogicNot -> do
-    w <- connWidth "A"
-    ta <- cellTermTerm <$> input "A"
-    anz <- SC.scBvNonzero sc w ta
-    res <- SC.scNot sc anz
-    outputBit res
-  CellTypeLogicAnd -> bvBinaryCmp . liftBinaryCmp sc $ \w x y -> do
-    xnz <- SC.scBvNonzero sc w x
-    ynz <- SC.scBvNonzero sc w y
-    SC.scAnd sc xnz ynz
-  CellTypeLogicOr -> bvBinaryCmp . liftBinaryCmp sc $ \w x y -> do
-    xnz <- SC.scBvNonzero sc w x
-    ynz <- SC.scBvNonzero sc w y
-    SC.scOr sc xnz ynz
-  CellTypeMux -> do
-    ta <- cellTermTerm <$> input "A"
-    tb <- cellTermTerm <$> input "B"
-    ts <- cellTermTerm <$> input "S"
-    swidth <- connWidth "S"
-    snz <- SC.scBvNonzero sc swidth ts
-    let width = connWidthNat "Y"
-    ty <- SC.scBitvector sc width
-    res <- SC.scIte sc ty snz tb ta
-    output $ CellTerm res (connWidthNat "A") (connSigned "A")
-  CellTypePmux -> do
-    ta <- cellTermTerm <$> input "A"
-    tb <- cellTermTerm <$> input "B"
-    ts <- cellTermTerm <$> input "S"
+primCellToMap sc c args =
+  case c ^. cellType of
+    CellTypeNot -> bvUnaryOp . liftUnary sc $ SC.scBvNot sc
+    CellTypePos ->
+      do res <- input "A"
+         output res
+    CellTypeNeg -> bvUnaryOp . liftUnary sc $ SC.scBvNeg sc
+    CellTypeAnd -> bvBinaryOp . liftBinary sc $ SC.scBvAnd sc
+    CellTypeOr -> bvBinaryOp . liftBinary sc $ SC.scBvOr sc
+    CellTypeXor -> bvBinaryOp . liftBinary sc $ SC.scBvXor sc
+    CellTypeXnor ->
+      bvBinaryOp $ liftBinary sc $ \w x y ->
+      do r <- SC.scBvXor sc w x y
+         SC.scBvNot sc w r
+    CellTypeReduceAnd ->
+      do r <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "and"
+         bvReduce True r
+    CellTypeReduceOr ->
+      do r <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "or"
+         bvReduce False r
+    CellTypeReduceXor ->
+      do r <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "xor"
+         bvReduce False r
+    CellTypeReduceXnor ->
+      do boolTy <- SC.scBoolType sc
+         x <- SC.scFreshVariable sc "x" boolTy
+         y <- SC.scFreshVariable sc "y" boolTy
+         r <- SC.scXor sc x y
+         res <- SC.scNot sc r
+         t <- SC.scAbstractTerms sc [x, y] res
+         bvReduce True t
+    CellTypeReduceBool ->
+      do r <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "or"
+         bvReduce False r
+    CellTypeShl ->
+      do ta <- fmap cellTermTerm $ input "A"
+         nb <- cellTermNat sc =<< input "B"
+         w <- outputWidth
+         res <- SC.scBvShl sc w ta nb
+         output (CellTerm res (connWidthNat "A") (connSigned "A"))
+    CellTypeShr ->
+      do ta <- fmap cellTermTerm $ input "A"
+         nb <- cellTermNat sc =<< input "B"
+         w <- outputWidth
+         res <- SC.scBvShr sc w ta nb
+         output (CellTerm res (connWidthNat "A") (connSigned "A"))
+    CellTypeSshl ->
+      do ta <- fmap cellTermTerm $ input "A"
+         nb <- cellTermNat sc =<< input "B"
+         w <- outputWidth
+         res <- SC.scBvShl sc w ta nb
+         output (CellTerm res (connWidthNat "A") (connSigned "A"))
+    CellTypeSshr ->
+      do ta <- fmap cellTermTerm $ input "A"
+         nb <- cellTermNat sc =<< input "B"
+         w <- outputWidth
+         res <- SC.scBvSShr sc w ta nb
+         output (CellTerm res (connWidthNat "A") (connSigned "A"))
+    -- "$shift" -> _
+    CellTypeShiftx ->
+      do let w = max (connWidthNat "A") (connWidthNat "B")
+         wt <- SC.scNat sc w
+         CellTerm ta _ _ <- extTrunc sc w =<< input "A"
+         CellTerm tb _ _ <- extTrunc sc w =<< input "B"
+         zero <- SC.scBvConst sc w 0
+         tbn <- SC.scBvToNat sc w tb
+         tbneg <- SC.scBvNeg sc wt tb
+         tbnegn <- SC.scBvToNat sc w tbneg
+         cond <- SC.scBvSGe sc wt tb zero
+         tcase <- SC.scBvShr sc wt ta tbn
+         ecase <- SC.scBvShl sc wt ta tbnegn
+         ty <- SC.scBitvector sc $ connWidthNat "A"
+         res <-
+           if connSigned "B"
+           then SC.scIte sc ty cond tcase ecase
+           else pure tcase
+         output (CellTerm res (connWidthNat "A") (connSigned "A"))
+    CellTypeLt -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvULt sc
+    CellTypeLe -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvULe sc
+    CellTypeGt -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvUGt sc
+    CellTypeGe -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvUGe sc
+    CellTypeEq -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvEq sc
+    CellTypeNe ->
+      bvBinaryCmp $ liftBinaryCmp sc $ \w x y ->
+      do r <- SC.scBvEq sc w x y
+         SC.scNot sc r
+    CellTypeEqx -> bvBinaryCmp . liftBinaryCmp sc $ SC.scBvEq sc
+    CellTypeNex ->
+      bvBinaryCmp $ liftBinaryCmp sc $ \w x y ->
+      do r <- SC.scBvEq sc w x y
+         SC.scNot sc r
+    CellTypeAdd -> bvBinaryOp . liftBinary sc $ SC.scBvAdd sc
+    CellTypeSub -> bvBinaryOp . liftBinary sc $ SC.scBvSub sc
+    CellTypeMul -> bvBinaryOp . liftBinary sc $ SC.scBvMul sc
+    CellTypeDiv -> bvBinaryOp . liftBinary sc $ SC.scBvUDiv sc
+    CellTypeMod -> bvBinaryOp . liftBinary sc $ SC.scBvURem sc
+    -- "$modfloor" -> _
+    CellTypeLogicNot ->
+      do w <- connWidth "A"
+         ta <- cellTermTerm <$> input "A"
+         anz <- SC.scBvNonzero sc w ta
+         res <- SC.scNot sc anz
+         outputBit res
+    CellTypeLogicAnd ->
+      bvBinaryCmp $ liftBinaryCmp sc $ \w x y ->
+      do xnz <- SC.scBvNonzero sc w x
+         ynz <- SC.scBvNonzero sc w y
+         SC.scAnd sc xnz ynz
+    CellTypeLogicOr ->
+      bvBinaryCmp $ liftBinaryCmp sc $ \w x y ->
+      do xnz <- SC.scBvNonzero sc w x
+         ynz <- SC.scBvNonzero sc w y
+         SC.scOr sc xnz ynz
+    CellTypeMux ->
+      do ta <- cellTermTerm <$> input "A"
+         tb <- cellTermTerm <$> input "B"
+         ts <- cellTermTerm <$> input "S"
+         swidth <- connWidth "S"
+         snz <- SC.scBvNonzero sc swidth ts
+         let width = connWidthNat "Y"
+         ty <- SC.scBitvector sc width
+         res <- SC.scIte sc ty snz tb ta
+         output $ CellTerm res (connWidthNat "A") (connSigned "A")
+    CellTypePmux ->
+      do ta <- cellTermTerm <$> input "A"
+         tb <- cellTermTerm <$> input "B"
+         ts <- cellTermTerm <$> input "S"
 
-    width <- connWidth "A"
-    widthBv <- SC.scBitvector sc $ connWidthNat "A"
-    swidth <- connWidth "S"
-    bool <- SC.scBoolType sc
-    nat <- SC.scNatType sc
-    splitb <- SC.scSplit sc swidth width bool tb
-    zero <- SC.scNat sc 0
-    accTy <- SC.scPairType sc nat widthBv
-    defaultAcc <- SC.scPairValue sc zero ta
+         width <- connWidth "A"
+         widthBv <- SC.scBitvector sc $ connWidthNat "A"
+         swidth <- connWidth "S"
+         bool <- SC.scBoolType sc
+         nat <- SC.scNatType sc
+         splitb <- SC.scSplit sc swidth width bool tb
+         zero <- SC.scNat sc 0
+         accTy <- SC.scPairType sc nat widthBv
+         defaultAcc <- SC.scPairValue sc zero ta
 
-    bit <- SC.scFreshVariable sc "bit" bool
-    acc <- SC.scFreshVariable sc "acc" accTy
-    fun <- SC.scAbstractTerms sc [bit, acc] =<< do
-      idx <- SC.scPairLeft sc acc
-      aval <- SC.scPairRight sc acc
-      bval <- SC.scAtWithDefault sc swidth widthBv aval splitb idx
-      newidx <- SC.scAddNat sc idx width
-      newval <- SC.scIte sc widthBv bit bval aval
-      SC.scPairValue sc newidx newval
+         bit <- SC.scFreshVariable sc "bit" bool
+         acc <- SC.scFreshVariable sc "acc" accTy
+         body <-
+           do idx <- SC.scPairLeft sc acc
+              aval <- SC.scPairRight sc acc
+              bval <- SC.scAtWithDefault sc swidth widthBv aval splitb idx
+              newidx <- SC.scAddNat sc idx width
+              newval <- SC.scIte sc widthBv bit bval aval
+              SC.scPairValue sc newidx newval
+         fun <- SC.scAbstractTerms sc [bit, acc] body
 
-    scFoldr <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "foldr"
-    resPair <- SC.scApplyAll sc scFoldr [bool, accTy, swidth, fun, defaultAcc, ts]
-    res <- SC.scPairRight sc resPair
-    output $ CellTerm res (connWidthNat "A") (connSigned "Y")
-  CellTypeBmux -> do
-    ia <- input "A"
-    is <- input "S"
-    let swidth = cellTermWidth is
-    let ywidth = connWidthNat "Y"
-    -- Split input A into chunks
-    chunks <- SC.scNat sc (2 ^ swidth)
-    ywidth' <- SC.scNat sc ywidth
-    bool <- SC.scBoolType sc
-    splitA <- SC.scSplit sc chunks ywidth' bool (cellTermTerm ia)
-    -- reverse to put index 0 on the left
-    outputType <- SC.scBitvector sc ywidth
-    revA <- SC.scGlobalApply sc "Prelude.reverse" [chunks, outputType, splitA]
-    -- Select chunk from output
-    ixWidth <- SC.scNat sc swidth
-    elt <- SC.scBvAt sc chunks outputType ixWidth revA (cellTermTerm is)
-    output (CellTerm elt ywidth (connSigned "Y"))
-  -- "$demux" -> _
-  -- "$lut" -> _
-  -- "$slice" -> _
-  -- "$concat" -> _
-  CellTypeDff -> pure Nothing
-  CellTypeFf -> pure Nothing
-  CellTypeUnsupportedPrimitive _ -> pure Nothing
-  CellTypeUserType _ -> pure Nothing
+         scFoldr <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "foldr"
+         resPair <- SC.scApplyAll sc scFoldr [bool, accTy, swidth, fun, defaultAcc, ts]
+         res <- SC.scPairRight sc resPair
+         output $ CellTerm res (connWidthNat "A") (connSigned "Y")
+    CellTypeBmux ->
+      do ia <- input "A"
+         is <- input "S"
+         let swidth = cellTermWidth is
+         let ywidth = connWidthNat "Y"
+         -- Split input A into chunks
+         chunks <- SC.scNat sc (2 ^ swidth)
+         ywidth' <- SC.scNat sc ywidth
+         bool <- SC.scBoolType sc
+         splitA <- SC.scSplit sc chunks ywidth' bool (cellTermTerm ia)
+         -- reverse to put index 0 on the left
+         outputType <- SC.scBitvector sc ywidth
+         revA <- SC.scGlobalApply sc "Prelude.reverse" [chunks, outputType, splitA]
+         -- Select chunk from output
+         ixWidth <- SC.scNat sc swidth
+         elt <- SC.scBvAt sc chunks outputType ixWidth revA (cellTermTerm is)
+         output (CellTerm elt ywidth (connSigned "Y"))
+    -- "$demux" -> _
+    -- "$lut" -> _
+    -- "$slice" -> _
+    -- "$concat" -> _
+    CellTypeDff -> pure Nothing
+    CellTypeFf -> pure Nothing
+    CellTypeUnsupportedPrimitive _ -> pure Nothing
+    CellTypeUserType _ -> pure Nothing
   where
     nm :: Text
     nm = Text.pack $ show $ c ^. cellType
@@ -310,53 +323,54 @@ primCellToMap sc c args = case c ^. cellType of
     outputWidth = connWidth "Y"
 
     input :: Text -> IO CellTerm
-    input inpNm = case Map.lookup inpNm args of
-      Nothing -> panic "cellToTerm" [nm <> " missing input " <> inpNm]
-      Just a -> pure $ CellTerm a (connWidthNat inpNm) (connSigned inpNm)
+    input inpNm =
+      case Map.lookup inpNm args of
+        Nothing -> panic "cellToTerm" [nm <> " missing input " <> inpNm]
+        Just a -> pure $ CellTerm a (connWidthNat inpNm) (connSigned inpNm)
 
     output :: CellTerm -> IO (Maybe (Map Text SC.Term))
-    output (CellTerm ct cw _) = do
-      let res = CellTerm ct cw (connSigned "Y")
-      CellTerm t _ _ <- extTrunc sc (connWidthNat "Y") res
-      pure . Just $ Map.fromList
-        [ ("Y", t)
-        ]
+    output (CellTerm ct cw _) =
+      do let res = CellTerm ct cw (connSigned "Y")
+         CellTerm t _ _ <- extTrunc sc (connWidthNat "Y") res
+         pure . Just $ Map.fromList
+           [ ("Y", t)
+           ]
 
     outputBit :: SC.Term -> IO (Maybe (Map Text SC.Term))
-    outputBit res = do
-      bool <- SC.scBoolType sc
-      vres <- SC.scSingle sc bool res
-      pure . Just $ Map.fromList
-        [ ("Y", vres)
-        ]
+    outputBit res =
+      do bool <- SC.scBoolType sc
+         vres <- SC.scSingle sc bool res
+         pure . Just $ Map.fromList
+           [ ("Y", vres)
+           ]
 
     -- convert input to big endian
     bvUnaryOp :: (CellTerm -> IO CellTerm) -> IO (Maybe (Map Text SC.Term))
-    bvUnaryOp f = do
-      t <- input "A"
-      res <- f t
-      output res
+    bvUnaryOp f =
+      do t <- input "A"
+         res <- f t
+         output res
     -- extend inputs to output width
     bvBinaryOp :: (CellTerm -> CellTerm -> IO CellTerm) -> IO (Maybe (Map Text SC.Term))
-    bvBinaryOp f = do
-      let w = connWidthNat "Y"
-      ta <- extTrunc sc w =<< input "A"
-      tb <- extTrunc sc w =<< input "B"
-      res <- f ta tb
-      output res
+    bvBinaryOp f =
+      do let w = connWidthNat "Y"
+         ta <- extTrunc sc w =<< input "A"
+         tb <- extTrunc sc w =<< input "B"
+         res <- f ta tb
+         output res
     -- extend inputs to max input width, output is a single bit
     bvBinaryCmp :: (CellTerm -> CellTerm -> IO SC.Term) -> IO (Maybe (Map Text SC.Term))
-    bvBinaryCmp f = do
-      ta <- input "A"
-      tb <- input "B"
-      res <- uncurry f =<< extMax sc ta tb
-      outputBit res
+    bvBinaryCmp f =
+      do ta <- input "A"
+         tb <- input "B"
+         res <- uncurry f =<< extMax sc ta tb
+         outputBit res
     bvReduce :: Bool -> SC.Term -> IO (Maybe (Map Text SC.Term))
-    bvReduce boolIdentity boolFun = do
-      CellTerm t _ _ <- input "A"
-      w <- connWidth "A"
-      boolTy <- SC.scBoolType sc
-      identity <- SC.scBool sc boolIdentity
-      scFoldr <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "foldr"
-      bit <- SC.scApplyAll sc scFoldr [boolTy, boolTy, w, boolFun, identity, t]
-      outputBit bit
+    bvReduce boolIdentity boolFun =
+      do CellTerm t _ _ <- input "A"
+         w <- connWidth "A"
+         boolTy <- SC.scBoolType sc
+         identity <- SC.scBool sc boolIdentity
+         scFoldr <- SC.scGlobalDef sc $ SC.mkIdent SC.preludeName "foldr"
+         bit <- SC.scApplyAll sc scFoldr [boolTy, boolTy, w, boolFun, identity, t]
+         outputBit bit
diff --git a/saw-central/src/SAWCentral/Yosys/Netgraph.hs b/saw-central/src/SAWCentral/Yosys/Netgraph.hs
index 06fc7db9e0..2d0832ad10 100644
--- a/saw-central/src/SAWCentral/Yosys/Netgraph.hs
+++ b/saw-central/src/SAWCentral/Yosys/Netgraph.hs
@@ -101,14 +101,15 @@ lookupPatternTerm ::
 lookupPatternTerm sc loc pat ts =
   case Map.lookup pat ts of
     Just t -> scPreterm sc t
-    Nothing -> do
-      bits <- forM pat $ \b -> do
-        case Map.lookup [b] ts of
-          Just t -> pure t
-          Nothing -> throw $ YosysErrorNoSuchOutputBitvec (Text.pack $ show b) loc
-      -- Yosys lists bits in little-endian order, while scVector expects big-endian, so reverse
-      let ps = fusePreterms (reverse bits)
-      scPreterms sc ps
+    Nothing ->
+      do bits <-
+           forM pat $ \b ->
+           case Map.lookup [b] ts of
+             Just t -> pure t
+             Nothing -> throw $ YosysErrorNoSuchOutputBitvec (Text.pack $ show b) loc
+         -- Yosys lists bits in little-endian order, while scVector expects big-endian, so reverse
+         let ps = fusePreterms (reverse bits)
+         scPreterms sc ps
 
 -- | Given a netgraph and an initial map from bit patterns to terms, populate that map with terms
 -- generated from the rest of the netgraph.
@@ -120,48 +121,51 @@ netgraphToTerms ::
   IO (Map [Bitrep] Preterm)
 netgraphToTerms sc env ng inputs
   | length (Graph.scc $ ng ^. netgraphGraph) /= length (ng ^. netgraphGraph)
-  = do
-      throw $ YosysError "Network graph contains a cycle after splitting on DFFs; SAW does not currently support analysis of this circuit"
-  | otherwise = do
+  = throw $ YosysError "Network graph contains a cycle after splitting on DFFs; SAW does not currently support analysis of this circuit"
+  | otherwise =
+      do
       let sorted = reverseTopSort $ ng ^. netgraphGraph
       foldM
-        ( \acc v -> do
+        ( \acc v ->
+            do
             let (c, cnm, _deps) = ng ^. netgraphNodeFromVertex $ v
             let outputFields = Map.filter (\d -> d == DirectionOutput || d == DirectionInout) $ c ^. cellPortDirections
             if
               -- special handling for $dff/$ff nodes - we read their /output/ from the inputs map, and later detect and write their /input/ to the state
               | c ^. cellType == CellTypeDff
-              , Just dffout <- Map.lookup "Q" $ c ^. cellConnections -> do
-                  r <- lookupPatternTerm sc (YosysBitvecConsumerCell cnm "Q") dffout acc
-                  ts <- deriveTermsByIndices sc dffout r
-                  pure $ Map.union ts acc
+              , Just dffout <- Map.lookup "Q" $ c ^. cellConnections ->
+                  do r <- lookupPatternTerm sc (YosysBitvecConsumerCell cnm "Q") dffout acc
+                     ts <- deriveTermsByIndices sc dffout r
+                     pure $ Map.union ts acc
               | c ^. cellType == CellTypeFf
-              , Just ffout <- Map.lookup "Q" $ c ^. cellConnections -> do
-                  r <- lookupPatternTerm sc (YosysBitvecConsumerCell cnm "Q") ffout acc
-                  ts <- deriveTermsByIndices sc ffout r
-                  pure $ Map.union ts acc
-              | otherwise -> do
-                  args <- fmap Map.fromList . forM (Map.assocs $ cellInputConnections c) $ \(inm, i) -> do -- for each input bit pattern
-                    -- if we can find that pattern exactly, great! use that term
-                    -- otherwise, find each individual bit and append the terms
-                    (inm,) <$> lookupPatternTerm sc (YosysBitvecConsumerCell cnm inm) i acc
-
-                  r <- primCellToTerm sc c args >>= \case
-                    Just r -> pure r
-                    Nothing ->
-                      let submoduleName = asUserType $ c ^. cellType in
-                      case Map.lookup submoduleName env of
-                        Just cm -> do
-                          r <- cryptolRecord sc args
-                          SC.scApply sc (cm ^. convertedModuleTerm) r
-                        Nothing ->
-                            throw $ YosysErrorNoSuchSubmodule  submoduleName cnm
-
-                  -- once we've built a term, insert it along with each of its bits
-                  ts <- forM (Map.assocs $ cellOutputConnections c) $ \(o, out) -> do
-                    t <- cryptolRecordSelect sc outputFields r o
-                    deriveTermsByIndices sc out t
-                  pure $ Map.union (Map.unions ts) acc
+              , Just ffout <- Map.lookup "Q" $ c ^. cellConnections ->
+                  do r <- lookupPatternTerm sc (YosysBitvecConsumerCell cnm "Q") ffout acc
+                     ts <- deriveTermsByIndices sc ffout r
+                     pure $ Map.union ts acc
+              | otherwise ->
+                  do args <- fmap Map.fromList . forM (Map.assocs $ cellInputConnections c) $ \(inm, i) ->
+                       -- for each input bit pattern
+                       -- if we can find that pattern exactly, great! use that term
+                       -- otherwise, find each individual bit and append the terms
+                       (inm,) <$> lookupPatternTerm sc (YosysBitvecConsumerCell cnm inm) i acc
+
+                     r <- primCellToTerm sc c args >>= \case
+                       Just r -> pure r
+                       Nothing ->
+                         let submoduleName = asUserType $ c ^. cellType in
+                         case Map.lookup submoduleName env of
+                           Just cm ->
+                             do r <- cryptolRecord sc args
+                                SC.scApply sc (cm ^. convertedModuleTerm) r
+                           Nothing ->
+                             throw $ YosysErrorNoSuchSubmodule submoduleName cnm
+
+                     -- once we've built a term, insert it along with each of its bits
+                     ts <-
+                       forM (Map.assocs $ cellOutputConnections c) $ \(o, out) ->
+                       do t <- cryptolRecordSelect sc outputFields r o
+                          deriveTermsByIndices sc out t
+                     pure $ Map.union (Map.unions ts) acc
         )
         inputs
         sorted
@@ -171,57 +175,58 @@ convertModule ::
   Map Text ConvertedModule ->
   Module ->
   IO ConvertedModule
-convertModule sc env m = do
-  let ng = moduleNetgraph m
-
-  let inputPorts = moduleInputPorts m
-  let outputPorts = moduleOutputPorts m
-
-  inputFields <- forM inputPorts
-    (\inp -> do
-        SC.scBitvector sc . fromIntegral $ length inp
-    )
-  outputFields <- forM outputPorts
-    (\out -> do
-        SC.scBitvector sc . fromIntegral $ length out
-    )
-  inputRecordType <- cryptolRecordType sc inputFields
-  outputRecordType <- cryptolRecordType sc outputFields
-  inputRecord <- SC.scFreshVariable sc "input" inputRecordType
-
-  derivedInputs <- forM (Map.assocs inputPorts) $ \(nm, inp) -> do
-    t <- cryptolRecordSelect sc inputFields inputRecord nm
-    deriveTermsByIndices sc inp t
-
-  oneBitType <- SC.scBitvector sc 1
-  xMsg <- SC.scString sc "Attempted to read X bit"
-  xTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, xMsg]
-  zMsg <- SC.scString sc "Attempted to read Z bit"
-  zTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, zMsg]
-  let inputs = Map.unions $ mconcat
-        [ [ Map.fromList
-            [ ( [BitrepZero], PretermBvNat 1 0 )
-            , ( [BitrepOne], PretermBvNat 1 1 )
-            , ( [BitrepX], PretermSlice 0 1 0 xTerm )
-            , ( [BitrepZ], PretermSlice 0 1 0 zTerm )
-            ]
-          ]
-        , derivedInputs
-        ]
-
-  terms <- netgraphToTerms sc env ng inputs
-  outputRecord <- cryptolRecord sc =<< mapForWithKeyM outputPorts
-    (\onm out -> lookupPatternTerm sc (YosysBitvecConsumerOutputPort onm) out terms)
-
-  t <- SC.scAbstractTerms sc [inputRecord] outputRecord
-  ty <- SC.scFun sc inputRecordType outputRecordType
-
-  let toCryptol (nm, rep) = (C.mkIdent nm, C.tWord . C.tNum $ length rep)
-  let cty = C.tFun
-        (C.tRec . C.recordFromFields $ toCryptol <$> Map.assocs inputPorts)
-        (C.tRec . C.recordFromFields $ toCryptol <$> Map.assocs outputPorts)
-  pure ConvertedModule
-    { _convertedModuleTerm = t
-    , _convertedModuleType = ty
-    , _convertedModuleCryptolType = cty
-    }
+convertModule sc env m =
+  do let ng = moduleNetgraph m
+
+     let inputPorts = moduleInputPorts m
+     let outputPorts = moduleOutputPorts m
+
+     inputFields <- forM inputPorts
+       (\inp ->
+           SC.scBitvector sc . fromIntegral $ length inp
+       )
+     outputFields <- forM outputPorts
+       (\out ->
+           SC.scBitvector sc . fromIntegral $ length out
+       )
+     inputRecordType <- cryptolRecordType sc inputFields
+     outputRecordType <- cryptolRecordType sc outputFields
+     inputRecord <- SC.scFreshVariable sc "input" inputRecordType
+
+     derivedInputs <-
+       forM (Map.assocs inputPorts) $ \(nm, inp) ->
+       do t <- cryptolRecordSelect sc inputFields inputRecord nm
+          deriveTermsByIndices sc inp t
+
+     oneBitType <- SC.scBitvector sc 1
+     xMsg <- SC.scString sc "Attempted to read X bit"
+     xTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, xMsg]
+     zMsg <- SC.scString sc "Attempted to read Z bit"
+     zTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, zMsg]
+     let inputs = Map.unions $ mconcat
+           [ [ Map.fromList
+               [ ( [BitrepZero], PretermBvNat 1 0 )
+               , ( [BitrepOne], PretermBvNat 1 1 )
+               , ( [BitrepX], PretermSlice 0 1 0 xTerm )
+               , ( [BitrepZ], PretermSlice 0 1 0 zTerm )
+               ]
+             ]
+           , derivedInputs
+           ]
+
+     terms <- netgraphToTerms sc env ng inputs
+     outputRecord <- cryptolRecord sc =<< mapForWithKeyM outputPorts
+       (\onm out -> lookupPatternTerm sc (YosysBitvecConsumerOutputPort onm) out terms)
+
+     t <- SC.scAbstractTerms sc [inputRecord] outputRecord
+     ty <- SC.scFun sc inputRecordType outputRecordType
+
+     let toCryptol (nm, rep) = (C.mkIdent nm, C.tWord . C.tNum $ length rep)
+     let cty = C.tFun
+           (C.tRec . C.recordFromFields $ toCryptol <$> Map.assocs inputPorts)
+           (C.tRec . C.recordFromFields $ toCryptol <$> Map.assocs outputPorts)
+     pure ConvertedModule
+       { _convertedModuleTerm = t
+       , _convertedModuleType = ty
+       , _convertedModuleCryptolType = cty
+       }
diff --git a/saw-central/src/SAWCentral/Yosys/State.hs b/saw-central/src/SAWCentral/Yosys/State.hs
index 8f0c474589..190e01017c 100644
--- a/saw-central/src/SAWCentral/Yosys/State.hs
+++ b/saw-central/src/SAWCentral/Yosys/State.hs
@@ -69,122 +69,126 @@ insertStateField ::
   Map Text (SC.Term, C.Type) {- ^ The field types of "__states__" -} ->
   Map Text (SC.Term, C.Type) {- ^ The mapping to update -} ->
   IO (Map Text (SC.Term, C.Type))
-insertStateField sc stateFields fields = do
-  stateRecordType <- fieldsToType sc stateFields
-  stateRecordCryptolType <- fieldsToCryptolType stateFields
-  pure $ Map.insert "__state__" (stateRecordType, stateRecordCryptolType) fields
+insertStateField sc stateFields fields =
+  do stateRecordType <- fieldsToType sc stateFields
+     stateRecordCryptolType <- fieldsToCryptolType stateFields
+     pure $ Map.insert "__state__" (stateRecordType, stateRecordCryptolType) fields
 
 -- | Translate a stateful HDL module into SAWCore
 convertModuleInline ::
   SC.SharedContext ->
   Module ->
   IO YosysSequential
-convertModuleInline sc m = do
-  let ng = moduleNetgraph m
-
-  let netnames =
-        Map.fromList
-        [ (n ^. netnameBits, t)
-        | (t, n) <- Map.assocs (m ^. moduleNetnames), not (n ^. netnameHideName) ]
-
-  let bestName t c =
-        fromMaybe (cellIdentifier t) $
-        do bs <- Map.lookup "Q" (c ^. cellConnections)
-           Map.lookup bs netnames
-
-  -- construct SAWCore and Cryptol types
-  let dffs =
-        Map.fromList
-        [ (bestName t c, c) | (t, c) <- Map.assocs (m ^. moduleCells), cellIsRegister c ]
-
-  stateWidths <- forM dffs $ \c ->
-    case Map.lookup "Q" $ c ^. cellConnections of
-      Nothing -> panic "convertModuleInline" ["Missing expected output name for $dff cell"]
-      Just b -> pure . fromIntegral $ length b
-
-  stateFields <- forM stateWidths $ \w -> do
-    t <- SC.scBitvector sc w
-    let cty = C.tWord $ C.tNum w
-    pure (t, cty)
-
-  let inputPorts = moduleInputPorts m
-  let outputPorts = moduleOutputPorts m
-  inputFields <- forM inputPorts $ \inp -> do
-    ty <- SC.scBitvector sc . fromIntegral $ length inp
-    let cty = C.tWord . C.tNum $ length inp
-    pure (ty, cty)
-  outputFields <- forM outputPorts $ \out -> do
-    ty <- SC.scBitvector sc . fromIntegral $ length out
-    let cty = C.tWord . C.tNum $ length out
-    pure (ty, cty)
-
-  domainFields <- insertStateField sc stateFields inputFields
-  codomainFields <- insertStateField sc stateFields outputFields
-
-  domainRecordType <- fieldsToType sc domainFields
-  domainCryptolRecordType <- fieldsToCryptolType domainFields
-  -- codomainRecordType <- fieldsToType sc codomainFields
-  codomainCryptolRecordType <- fieldsToCryptolType codomainFields
-
-  -- convert module into term
-  domainRecord <- SC.scFreshVariable sc "input" domainRecordType
-
-  derivedInputs <- forM (Map.assocs inputPorts) $ \(nm, inp) -> do
-    t <- cryptolRecordSelect sc domainFields domainRecord nm
-    deriveTermsByIndices sc inp t
-
-  preStateRecord <- cryptolRecordSelect sc domainFields domainRecord "__state__"
-  derivedPreState <- forM (Map.assocs dffs) $ \(cnm, c) ->
-    case Map.lookup "Q" $ c ^. cellConnections of
-      Nothing -> panic "convertModuleInline" ["Missing expected output name for $dff cell"]
-      Just b -> do
-        t <- cryptolRecordSelect sc stateFields preStateRecord cnm
-        deriveTermsByIndices sc b t
-
-  oneBitType <- SC.scBitvector sc 1
-  xMsg <- SC.scString sc "Attempted to read X bit"
-  xTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, xMsg]
-  zMsg <- SC.scString sc "Attempted to read Z bit"
-  zTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, zMsg]
-  let inputs = Map.unions $ mconcat
-        [ [ Map.fromList
-            [ ( [BitrepZero], PretermBvNat 1 0 )
-            , ( [BitrepOne], PretermBvNat 1 1 )
-            , ( [BitrepX], PretermSlice 0 1 0 xTerm )
-            , ( [BitrepZ], PretermSlice 0 1 0 zTerm )
-            ]
-          ]
-        , derivedInputs
-        , derivedPreState
-        ]
-
-  terms <- netgraphToTerms sc Map.empty ng inputs
-
-  postStateFields <- mapForWithKeyM dffs $ \cnm c ->
-    case Map.lookup "D" $ c ^. cellConnections of
-      Nothing -> panic "convertModuleInline" ["Missing expected input name for $dff cell"]
-      Just b -> do
-        t <- lookupPatternTerm sc (YosysBitvecConsumerCell cnm "D") b terms
-        pure t
-  postStateRecord <- cryptolRecord sc postStateFields
-
-  outputRecord <- cryptolRecord sc . Map.insert "__state__" postStateRecord =<< mapForWithKeyM outputPorts
-    (\onm out -> lookupPatternTerm sc (YosysBitvecConsumerOutputPort onm) out terms)
-
-  -- construct result
-  t <- SC.scAbstractTerms sc [domainRecord] outputRecord
-  -- ty <- SC.scFun sc domainRecordType codomainRecordType
-  _ <- validateTerm sc "translating a sequential circuit" t
-  let cty = C.tFun domainCryptolRecordType codomainCryptolRecordType
-  pure YosysSequential
-    { _yosysSequentialTerm = SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) t
-    , _yosysSequentialStateFields = stateFields
-    , _yosysSequentialInputFields = inputFields
-    , _yosysSequentialOutputFields = outputFields
-    , _yosysSequentialInputWidths = fromIntegral . length <$> inputPorts
-    , _yosysSequentialOutputWidths = fromIntegral . length <$> outputPorts
-    , _yosysSequentialStateWidths = stateWidths
-    }
+convertModuleInline sc m =
+  do let ng = moduleNetgraph m
+
+     let netnames =
+           Map.fromList
+           [ (n ^. netnameBits, t)
+           | (t, n) <- Map.assocs (m ^. moduleNetnames), not (n ^. netnameHideName) ]
+
+     let bestName t c =
+           fromMaybe (cellIdentifier t) $
+           do bs <- Map.lookup "Q" (c ^. cellConnections)
+              Map.lookup bs netnames
+
+     -- construct SAWCore and Cryptol types
+     let dffs =
+           Map.fromList
+           [ (bestName t c, c) | (t, c) <- Map.assocs (m ^. moduleCells), cellIsRegister c ]
+
+     stateWidths <- forM dffs $ \c ->
+       case Map.lookup "Q" $ c ^. cellConnections of
+         Nothing -> panic "convertModuleInline" ["Missing expected output name for $dff cell"]
+         Just b -> pure . fromIntegral $ length b
+
+     stateFields <-
+       forM stateWidths $ \w ->
+       do t <- SC.scBitvector sc w
+          let cty = C.tWord $ C.tNum w
+          pure (t, cty)
+
+     let inputPorts = moduleInputPorts m
+     let outputPorts = moduleOutputPorts m
+     inputFields <-
+       forM inputPorts $ \inp ->
+       do ty <- SC.scBitvector sc . fromIntegral $ length inp
+          let cty = C.tWord . C.tNum $ length inp
+          pure (ty, cty)
+     outputFields <-
+       forM outputPorts $ \out ->
+       do ty <- SC.scBitvector sc . fromIntegral $ length out
+          let cty = C.tWord . C.tNum $ length out
+          pure (ty, cty)
+
+     domainFields <- insertStateField sc stateFields inputFields
+     codomainFields <- insertStateField sc stateFields outputFields
+
+     domainRecordType <- fieldsToType sc domainFields
+     domainCryptolRecordType <- fieldsToCryptolType domainFields
+     -- codomainRecordType <- fieldsToType sc codomainFields
+     codomainCryptolRecordType <- fieldsToCryptolType codomainFields
+
+     -- convert module into term
+     domainRecord <- SC.scFreshVariable sc "input" domainRecordType
+
+     derivedInputs <-
+       forM (Map.assocs inputPorts) $ \(nm, inp) ->
+       do t <- cryptolRecordSelect sc domainFields domainRecord nm
+          deriveTermsByIndices sc inp t
+
+     preStateRecord <- cryptolRecordSelect sc domainFields domainRecord "__state__"
+     derivedPreState <-
+       forM (Map.assocs dffs) $ \(cnm, c) ->
+       case Map.lookup "Q" $ c ^. cellConnections of
+         Nothing -> panic "convertModuleInline" ["Missing expected output name for $dff cell"]
+         Just b ->
+           do t <- cryptolRecordSelect sc stateFields preStateRecord cnm
+              deriveTermsByIndices sc b t
+
+     oneBitType <- SC.scBitvector sc 1
+     xMsg <- SC.scString sc "Attempted to read X bit"
+     xTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, xMsg]
+     zMsg <- SC.scString sc "Attempted to read Z bit"
+     zTerm <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [oneBitType, zMsg]
+     let inputs = Map.unions $ mconcat
+           [ [ Map.fromList
+               [ ( [BitrepZero], PretermBvNat 1 0 )
+               , ( [BitrepOne], PretermBvNat 1 1 )
+               , ( [BitrepX], PretermSlice 0 1 0 xTerm )
+               , ( [BitrepZ], PretermSlice 0 1 0 zTerm )
+               ]
+             ]
+           , derivedInputs
+           , derivedPreState
+           ]
+
+     terms <- netgraphToTerms sc Map.empty ng inputs
+
+     postStateFields <-
+       mapForWithKeyM dffs $ \cnm c ->
+       case Map.lookup "D" $ c ^. cellConnections of
+         Nothing -> panic "convertModuleInline" ["Missing expected input name for $dff cell"]
+         Just b -> lookupPatternTerm sc (YosysBitvecConsumerCell cnm "D") b terms
+     postStateRecord <- cryptolRecord sc postStateFields
+
+     outputRecord <- cryptolRecord sc . Map.insert "__state__" postStateRecord =<< mapForWithKeyM outputPorts
+       (\onm out -> lookupPatternTerm sc (YosysBitvecConsumerOutputPort onm) out terms)
+
+     -- construct result
+     t <- SC.scAbstractTerms sc [domainRecord] outputRecord
+     -- ty <- SC.scFun sc domainRecordType codomainRecordType
+     _ <- validateTerm sc "translating a sequential circuit" t
+     let cty = C.tFun domainCryptolRecordType codomainCryptolRecordType
+     pure YosysSequential
+       { _yosysSequentialTerm = SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) t
+       , _yosysSequentialStateFields = stateFields
+       , _yosysSequentialInputFields = inputFields
+       , _yosysSequentialOutputFields = outputFields
+       , _yosysSequentialInputWidths = fromIntegral . length <$> inputPorts
+       , _yosysSequentialOutputWidths = fromIntegral . length <$> outputPorts
+       , _yosysSequentialStateWidths = stateWidths
+       }
 
 -- | Given a SAWCore term with an explicit state, iterate the term the
 -- given number of times. The resulting term has a parameter for the
@@ -194,75 +198,81 @@ composeYosysSequentialHelper ::
   YosysSequential ->
   Integer ->
   IO (SC.Term, C.Type)
-composeYosysSequentialHelper sc s n = do
-  let t = SC.ttTerm $ s ^. yosysSequentialTerm
-
-  width <- SC.scNat sc $ fromIntegral n
-  extendedInputFields <- forM (s ^. yosysSequentialInputFields) $ \(ty, cty) -> do
-    exty <- SC.scVecType sc width ty
-    let excty = C.tSeq (C.tNum n) cty
-    pure (exty, excty)
-  extendedOutputFields <- forM (s ^. yosysSequentialOutputFields) $ \(ty, cty) -> do
-    exty <- SC.scVecType sc width ty
-    let excty = C.tSeq (C.tNum n) cty
-    pure (exty, excty)
-  extendedInputType <- fieldsToType sc extendedInputFields
-  extendedInputCryptolType <- fieldsToCryptolType extendedInputFields
-  extendedInputRecord <- SC.scFreshVariable sc "input" extendedInputType
-  extendedOutputCryptolType <- fieldsToCryptolType extendedOutputFields
-
-  allInputs <- fmap Map.fromList . forM (Map.keys extendedInputFields) $ \nm -> do
-    inp <- cryptolRecordSelect sc extendedInputFields extendedInputRecord nm
-    pure (nm, inp)
-
-  codomainFields <- insertStateField sc (s ^. yosysSequentialStateFields) $ s ^. yosysSequentialOutputFields
-
-  let
-    buildIntermediateInput :: Integer -> SC.Term -> IO SC.Term
-    buildIntermediateInput i st = do
-      inps <- fmap Map.fromList . forM (Map.assocs allInputs) $ \(nm, inp) -> do
-        case Map.lookup nm $ s ^. yosysSequentialInputFields of
-          Nothing -> throw . YosysError $ "Invalid input: " <> nm
-          Just (elemty, _) -> do
-            idx <- SC.scNat sc $ fromIntegral i
-            idxed <- SC.scAt sc width elemty inp idx
-            pure (nm, idxed)
-      let inpsWithSt = Map.insert "__state__" st inps
-      cryptolRecord sc inpsWithSt
-
-    summarizeOutput :: SC.Term -> IO (SC.Term, Map Text SC.Term)
-    summarizeOutput outrec = do
-      outstate <- cryptolRecordSelect sc codomainFields outrec "__state__"
-      outputs <- fmap Map.fromList . forM (Map.assocs $ s ^. yosysSequentialOutputFields) $ \(nm, (ty, _)) -> do
-        out <- cryptolRecordSelect sc codomainFields outrec nm
-        wrapped <- SC.scSingle sc ty out
-        pure (nm, wrapped)
-      pure (outstate, outputs)
-
-    compose1 :: Integer -> (SC.Term, Map Text SC.Term) -> IO (SC.Term, Map Text SC.Term)
-    compose1 i (st, outs) = do
-      inprec <- buildIntermediateInput i st
-      outrec <- SC.scApply sc t inprec
-      (st', outs') <- summarizeOutput outrec
-      mergedOuts <- fmap Map.fromList . forM (Map.assocs outs') $ \(nm, arr) -> do
-        case (Map.lookup nm $ s ^. yosysSequentialOutputFields, Map.lookup nm outs) of
-          (Just (ty, _), Just rest) -> do
-            restlen <- SC.scNat sc $ fromIntegral i
-            arrlen <- SC.scNat sc 1
-            appended <- SC.scAppend sc restlen arrlen ty rest arr
-            pure (nm, appended)
-          _ -> pure (nm, arr)
-      pure (st', mergedOuts)
-
-  stateType <- fieldsToType sc $ s ^. yosysSequentialStateFields
-  initialState <- SC.scFreshVariable sc "initial_state" stateType
-  (_, outputs) <- foldM (\acc i -> compose1 i acc) (initialState, Map.empty) [0..n-1]
-
-  outputRecord <- cryptolRecord sc outputs
-  res <- SC.scAbstractTerms sc [initialState, extendedInputRecord] outputRecord
-  let cty = C.tFun extendedInputCryptolType extendedOutputCryptolType
-
-  pure (res, cty)
+composeYosysSequentialHelper sc s n =
+  do let t = SC.ttTerm $ s ^. yosysSequentialTerm
+
+     width <- SC.scNat sc $ fromIntegral n
+     extendedInputFields <-
+       forM (s ^. yosysSequentialInputFields) $ \(ty, cty) ->
+       do exty <- SC.scVecType sc width ty
+          let excty = C.tSeq (C.tNum n) cty
+          pure (exty, excty)
+     extendedOutputFields <-
+       forM (s ^. yosysSequentialOutputFields) $ \(ty, cty) ->
+       do exty <- SC.scVecType sc width ty
+          let excty = C.tSeq (C.tNum n) cty
+          pure (exty, excty)
+     extendedInputType <- fieldsToType sc extendedInputFields
+     extendedInputCryptolType <- fieldsToCryptolType extendedInputFields
+     extendedInputRecord <- SC.scFreshVariable sc "input" extendedInputType
+     extendedOutputCryptolType <- fieldsToCryptolType extendedOutputFields
+
+     allInputs <-
+       fmap Map.fromList . forM (Map.keys extendedInputFields) $ \nm ->
+       do inp <- cryptolRecordSelect sc extendedInputFields extendedInputRecord nm
+          pure (nm, inp)
+
+     codomainFields <- insertStateField sc (s ^. yosysSequentialStateFields) $ s ^. yosysSequentialOutputFields
+
+     let
+       buildIntermediateInput :: Integer -> SC.Term -> IO SC.Term
+       buildIntermediateInput i st =
+         do inps <-
+              fmap Map.fromList . forM (Map.assocs allInputs) $ \(nm, inp) ->
+              case Map.lookup nm $ s ^. yosysSequentialInputFields of
+                Nothing -> throw . YosysError $ "Invalid input: " <> nm
+                Just (elemty, _) ->
+                  do idx <- SC.scNat sc $ fromIntegral i
+                     idxed <- SC.scAt sc width elemty inp idx
+                     pure (nm, idxed)
+            let inpsWithSt = Map.insert "__state__" st inps
+            cryptolRecord sc inpsWithSt
+
+       summarizeOutput :: SC.Term -> IO (SC.Term, Map Text SC.Term)
+       summarizeOutput outrec =
+         do outstate <- cryptolRecordSelect sc codomainFields outrec "__state__"
+            outputs <-
+              fmap Map.fromList . forM (Map.assocs $ s ^. yosysSequentialOutputFields) $ \(nm, (ty, _)) ->
+              do out <- cryptolRecordSelect sc codomainFields outrec nm
+                 wrapped <- SC.scSingle sc ty out
+                 pure (nm, wrapped)
+            pure (outstate, outputs)
+
+       compose1 :: Integer -> (SC.Term, Map Text SC.Term) -> IO (SC.Term, Map Text SC.Term)
+       compose1 i (st, outs) =
+         do inprec <- buildIntermediateInput i st
+            outrec <- SC.scApply sc t inprec
+            (st', outs') <- summarizeOutput outrec
+            mergedOuts <-
+              fmap Map.fromList . forM (Map.assocs outs') $ \(nm, arr) ->
+              case (Map.lookup nm $ s ^. yosysSequentialOutputFields, Map.lookup nm outs) of
+                (Just (ty, _), Just rest) ->
+                  do restlen <- SC.scNat sc $ fromIntegral i
+                     arrlen <- SC.scNat sc 1
+                     appended <- SC.scAppend sc restlen arrlen ty rest arr
+                     pure (nm, appended)
+                _ -> pure (nm, arr)
+            pure (st', mergedOuts)
+
+     stateType <- fieldsToType sc $ s ^. yosysSequentialStateFields
+     initialState <- SC.scFreshVariable sc "initial_state" stateType
+     (_, outputs) <- foldM (\acc i -> compose1 i acc) (initialState, Map.empty) [0..n-1]
+
+     outputRecord <- cryptolRecord sc outputs
+     res <- SC.scAbstractTerms sc [initialState, extendedInputRecord] outputRecord
+     let cty = C.tFun extendedInputCryptolType extendedOutputCryptolType
+
+     pure (res, cty)
 
 -- | Given a SAWCore term with an explicit state, iterate the term the
 -- given number of times. Accessing the initial state produces an
@@ -272,13 +282,13 @@ composeYosysSequential ::
   YosysSequential ->
   Integer ->
   IO SC.TypedTerm
-composeYosysSequential sc s n = do
-  (t, cty) <- composeYosysSequentialHelper sc s n
-  stateType <- fieldsToType sc $ s ^. yosysSequentialStateFields
-  initialStateMsg <- SC.scString sc "Attempted to read initial state of sequential circuit"
-  initialState <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [stateType, initialStateMsg]
-  res <- SC.scApply sc t initialState
-  pure $ SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) res
+composeYosysSequential sc s n =
+  do (t, cty) <- composeYosysSequentialHelper sc s n
+     stateType <- fieldsToType sc $ s ^. yosysSequentialStateFields
+     initialStateMsg <- SC.scString sc "Attempted to read initial state of sequential circuit"
+     initialState <- SC.scGlobalApply sc (SC.mkIdent SC.preludeName "error") [stateType, initialStateMsg]
+     res <- SC.scApply sc t initialState
+     pure $ SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) res
 
 -- | Given a SAWCore term with an explicit state, iterate the term the
 -- given number of times. The resulting term has a parameter for the
@@ -288,7 +298,7 @@ composeYosysSequentialWithState ::
   YosysSequential ->
   Integer ->
   IO SC.TypedTerm
-composeYosysSequentialWithState sc s n = do
-  (t, cty) <- composeYosysSequentialHelper sc s n
-  scty <- fieldsToCryptolType $ s ^. yosysSequentialStateFields
-  pure $ SC.TypedTerm (SC.TypedTermSchema . C.tMono $ C.tFun scty cty) t
+composeYosysSequentialWithState sc s n =
+  do (t, cty) <- composeYosysSequentialHelper sc s n
+     scty <- fieldsToCryptolType $ s ^. yosysSequentialStateFields
+     pure $ SC.TypedTerm (SC.TypedTermSchema . C.tMono $ C.tFun scty cty) t
diff --git a/saw-central/src/SAWCentral/Yosys/Theorem.hs b/saw-central/src/SAWCentral/Yosys/Theorem.hs
index e150998091..5d9121203f 100644
--- a/saw-central/src/SAWCentral/Yosys/Theorem.hs
+++ b/saw-central/src/SAWCentral/Yosys/Theorem.hs
@@ -59,22 +59,23 @@ theoremProp ::
   SC.SharedContext ->
   YosysTheorem ->
   IO SC.TypedTerm
-theoremProp sc thm = do
-  r <- SC.scFreshVariable sc "r" $ thm ^. theoremInputType
-  modr <- SC.scApply sc (thm ^. theoremModule) r
-  bodyr <- SC.scApply sc (thm ^. theoremBody) r
-  equality <- eqBvRecords sc (thm ^. theoremOutputCryptolType) modr bodyr
-  res <- case thm ^. theoremPrecond of
-    Nothing -> pure equality
-    Just pc -> do
-      pcr <- SC.scApply sc pc r
-      SC.scImplies sc pcr equality
-  func <- SC.scAbstractTerms sc [r] res
-  let cty = C.tFun (thm ^. theoremInputCryptolType) C.tBit
-  SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty)
-    <$> validateTerm sc
-    ("constructing a proposition while verifying " <> URI.render (thm ^. theoremURI))
-    func
+theoremProp sc thm =
+  do r <- SC.scFreshVariable sc "r" $ thm ^. theoremInputType
+     modr <- SC.scApply sc (thm ^. theoremModule) r
+     bodyr <- SC.scApply sc (thm ^. theoremBody) r
+     equality <- eqBvRecords sc (thm ^. theoremOutputCryptolType) modr bodyr
+     res <-
+       case thm ^. theoremPrecond of
+         Nothing -> pure equality
+         Just pc ->
+           do pcr <- SC.scApply sc pc r
+              SC.scImplies sc pcr equality
+     func <- SC.scAbstractTerms sc [r] res
+     let cty = C.tFun (thm ^. theoremInputCryptolType) C.tBit
+     SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty)
+       <$> validateTerm sc
+       ("constructing a proposition while verifying " <> URI.render (thm ^. theoremURI))
+       func
 
 -- | Construct a SAWCore proposition for the given theorem.
 -- In pseudo-Cryptol, this looks like {{ \r -> if precond r then body r else module r }}
@@ -82,19 +83,20 @@ theoremReplacement ::
   SC.SharedContext ->
   YosysTheorem ->
   IO SC.Term
-theoremReplacement sc thm = do
-  r <- SC.scFreshVariable sc "r" $ thm ^. theoremInputType
-  body <- case thm ^. theoremPrecond of
-    Nothing -> SC.scApply sc (thm ^. theoremBody) r
-    Just pc -> do
-      precond <- SC.scApply sc pc r
-      thenCase <- SC.scApply sc (thm ^. theoremBody) r
-      elseCase <- SC.scApply sc (thm ^. theoremModule) r
-      SC.scIte sc (thm ^. theoremOutputType) precond thenCase elseCase
-  ft <- SC.scAbstractTerms sc [r] body
-  validateTerm sc
-    ("constructing an override replacement for " <> URI.render (thm ^. theoremURI))
-    ft
+theoremReplacement sc thm =
+  do r <- SC.scFreshVariable sc "r" $ thm ^. theoremInputType
+     body <-
+       case thm ^. theoremPrecond of
+          Nothing -> SC.scApply sc (thm ^. theoremBody) r
+          Just pc ->
+            do precond <- SC.scApply sc pc r
+               thenCase <- SC.scApply sc (thm ^. theoremBody) r
+               elseCase <- SC.scApply sc (thm ^. theoremModule) r
+               SC.scIte sc (thm ^. theoremOutputType) precond thenCase elseCase
+     ft <- SC.scAbstractTerms sc [r] body
+     validateTerm sc
+       ("constructing an override replacement for " <> URI.render (thm ^. theoremURI))
+       ft
 
 -- | Given a SAWCore term corresponding to an HDL module, a specification, and a precondition:
 -- Construct a theorem summarizing the relationship between the module and the specification.
@@ -106,20 +108,24 @@ buildTheorem ::
   SC.TypedTerm ->
   IO YosysTheorem
 buildTheorem sc ymod newmod precond body = do
-  cty <- case SC.ttType ymod of
-    SC.TypedTermSchema (C.Forall [] [] cty) -> pure cty
-    _ -> throw YosysErrorInvalidOverrideTarget
-  (cinpTy, coutTy) <- case cty of
-    C.TCon (C.TC C.TCFun) [ci, co] -> pure (ci, co)
-    _ -> throw YosysErrorInvalidOverrideTarget
+  cty <-
+    case SC.ttType ymod of
+      SC.TypedTermSchema (C.Forall [] [] cty) -> pure cty
+      _ -> throw YosysErrorInvalidOverrideTarget
+  (cinpTy, coutTy) <-
+    case cty of
+      C.TCon (C.TC C.TCFun) [ci, co] -> pure (ci, co)
+      _ -> throw YosysErrorInvalidOverrideTarget
   inpTy <- CSC.importType sc CSC.emptyEnv cinpTy
   outTy <- CSC.importType sc CSC.emptyEnv coutTy
-  nmi <- case reduceSelectors (SC.ttTerm ymod) of
-    (R.asConstant -> Just (SC.Name _ nmi)) -> pure nmi
-    _ -> throw YosysErrorInvalidOverrideTarget
-  uri <- case nmi of
-    SC.ImportedName uri _ -> pure uri
-    _ -> throw YosysErrorInvalidOverrideTarget
+  nmi <-
+    case reduceSelectors (SC.ttTerm ymod) of
+      (R.asConstant -> Just (SC.Name _ nmi)) -> pure nmi
+      _ -> throw YosysErrorInvalidOverrideTarget
+  uri <-
+    case nmi of
+      SC.ImportedName uri _ -> pure uri
+      _ -> throw YosysErrorInvalidOverrideTarget
   pure YosysTheorem
     { _theoremURI = uri
     , _theoremInputCryptolType = cinpTy
@@ -161,9 +167,11 @@ applyOverride ::
   SC.Term ->
   IO SC.Term
 applyOverride sc thm t = do
-  tidx <- (SC.scResolveNameByURI sc $ thm ^. theoremURI) >>= \case
-    Nothing -> throw . YosysErrorOverrideNameNotFound . URI.render $ thm ^. theoremURI
-    Just i -> pure i
+  tidx <-
+    do result <- SC.scResolveNameByURI sc $ thm ^. theoremURI
+       case result of
+         Nothing -> throw . YosysErrorOverrideNameNotFound . URI.render $ thm ^. theoremURI
+         Just i -> pure i
   -- unfold everything except for theoremURI and prelude constants
   let isPreludeName (SC.ModuleIdentifier ident) = SC.identModule ident == SC.preludeModuleName
       isPreludeName _ = False
@@ -172,11 +180,13 @@ applyOverride sc thm t = do
   cache <- SC.newCache
   let
     go :: SC.Term -> IO SC.Term
-    go s@SC.STApp { SC.stAppIndex = aidx, SC.stAppTermF = tf } = SC.useCache cache aidx $ case tf of
-      SC.Constant (SC.Name idx _)
-        | idx == tidx -> theoremReplacement sc thm
-        | otherwise -> pure s
-      _ -> SC.scTermF sc =<< traverse go tf
+    go s@SC.STApp { SC.stAppIndex = aidx, SC.stAppTermF = tf } =
+      SC.useCache cache aidx $
+      case tf of
+        SC.Constant (SC.Name idx _)
+          | idx == tidx -> theoremReplacement sc thm
+          | otherwise -> pure s
+        _ -> SC.scTermF sc =<< traverse go tf
   ft <- go unfolded
   validateTerm sc
     ("applying an override for " <> URI.render (thm ^. theoremURI))
diff --git a/saw-central/src/SAWCentral/Yosys/TransitionSystem.hs b/saw-central/src/SAWCentral/Yosys/TransitionSystem.hs
index be625c6afb..e37792b087 100644
--- a/saw-central/src/SAWCentral/Yosys/TransitionSystem.hs
+++ b/saw-central/src/SAWCentral/Yosys/TransitionSystem.hs
@@ -81,27 +81,29 @@ makeLenses ''SequentialFields
 sequentialReprs ::
   Map Text Natural ->
   IO (Some SequentialFields)
-sequentialReprs fs = do
-  let assocs = Map.assocs fs
-  Some fields <- go assocs
-  idxs <- Ctx.traverseAndCollect (\idx _ -> pure [Some idx]) fields
-  let index = zipWith (\(nm, _) idx -> (nm, idx)) assocs $ reverse idxs
-  pure $ Some SequentialFields
-    { _sequentialFields = fields
-    , _sequentialFieldsIndex = Map.fromList index
-    }
+sequentialReprs fs =
+  do let assocs = Map.assocs fs
+     Some fields <- go assocs
+     idxs <- Ctx.traverseAndCollect (\idx _ -> pure [Some idx]) fields
+     let index = zipWith (\(nm, _) idx -> (nm, idx)) assocs $ reverse idxs
+     pure $ Some SequentialFields
+       { _sequentialFields = fields
+       , _sequentialFieldsIndex = Map.fromList index
+       }
   where
     go :: [(Text, Natural)] -> IO (Some (Ctx.Assignment SequentialField))
     go [] = pure $ Some Ctx.empty
-    go ((nm, n):ns) = case someNat n of
-      Just (Some nr) | Just LeqProof <- testLeq (knownNat @1) nr -> do
-        let field = SequentialField
-              { _sequentialFieldName = nm
-              , _sequentialFieldTypeRepr = W4.BaseBVRepr nr
-              }
-        Some rest <- go ns
-        pure $ Some $ Ctx.extend rest field
-      _ -> throw $ YosysErrorInvalidStateFieldWidth nm
+    go ((nm, n):ns) =
+      case someNat n of
+        Just (Some nr)
+          | Just LeqProof <- testLeq (knownNat @1) nr ->
+              do let field = SequentialField
+                       { _sequentialFieldName = nm
+                       , _sequentialFieldTypeRepr = W4.BaseBVRepr nr
+                       }
+                 Some rest <- go ns
+                 pure $ Some $ Ctx.extend rest field
+        _ -> throw $ YosysErrorInvalidStateFieldWidth nm
 
 -- | Given information about field names and types alongside an
 -- appropriately-typed What4 struct value, explode that struct into a
@@ -117,18 +119,19 @@ ecBindingsOfFields ::
   SequentialFields ctx {- ^ Mapping from field names to What4 base types -} ->
   W4.SymStruct (W4.B.ExprBuilder n st fs) ctx {- ^ What4 record to deconstruct -} ->
   IO (Map Text (SC.VarName, SC.Term, SimW4.SValue (W4.B.ExprBuilder n st fs)))
-ecBindingsOfFields sym sc pfx fs s inp = fmap Map.fromList . forM (Map.assocs fs) $ \(baseName, ty) -> do
-  let nm = pfx <> baseName
-  vn <- SC.scFreshVarName sc nm
-  val <- case s ^. sequentialFieldsIndex . at nm of
-    Just (Some idx)
-      | sf <- s ^. sequentialFields . ixF' idx
-      , W4.BaseBVRepr _nr <- sf ^. sequentialFieldTypeRepr
-        -> do
-          inpExpr <- W4.structField sym inp idx
-          pure . Sim.VWord $ W4.DBV inpExpr
-    _ -> throw $ YosysErrorTransitionSystemMissingField nm
-  pure (baseName, (vn, ty, val))
+ecBindingsOfFields sym sc pfx fs s inp =
+  fmap Map.fromList . forM (Map.assocs fs) $ \(baseName, ty) ->
+  do let nm = pfx <> baseName
+     vn <- SC.scFreshVarName sc nm
+     val <-
+       case s ^. sequentialFieldsIndex . at nm of
+         Just (Some idx)
+           | sf <- s ^. sequentialFields . ixF' idx
+           , W4.BaseBVRepr _nr <- sf ^. sequentialFieldTypeRepr ->
+               do inpExpr <- W4.structField sym inp idx
+                  pure . Sim.VWord $ W4.DBV inpExpr
+         _ -> throw $ YosysErrorTransitionSystemMissingField nm
+     pure (baseName, (vn, ty, val))
 
 -- | Given a sequential circuit and a query, construct and write to
 -- disk a Sally transition system encoding that query.
@@ -140,153 +143,163 @@ queryModelChecker ::
   SC.TypedTerm {- ^ A boolean function of three parameters: an 8-bit cycle counter, a record of "fixed" inputs, and a record of circuit outputs -} ->
   Set Text {- ^ Names of circuit inputs that are fixed -}->
   IO ()
-queryModelChecker sym sc sequential path query fixedInputs = do
-  -- there are 5 classes of field:
-  --  - fixed inputs (inputs from the circuit named in the fixed set, assumed to be constant across cycles
-  --  - variable inputs (all other inputs from the circuit)
-  --  - outputs (all outputs from the circuit)
-  --  - state (all circuit flip-flop states)
-  --  - internal (right now, just a cycle counter)
-  let (fixedInputWidths, variableInputWidths) = Map.partitionWithKey (\nm _ -> Set.member nm fixedInputs) $ sequential ^. yosysSequentialInputWidths
-  let (fixedInputFields, variableInputFields) = Map.partitionWithKey (\nm _ -> Set.member nm fixedInputs) $ sequential ^. yosysSequentialInputFields
-  let internalWidths = Map.singleton "cycle" 8
-  internalFields <- forM internalWidths $ \w -> SC.scBitvector sc w
+queryModelChecker sym sc sequential path query fixedInputs =
+  do -- there are 5 classes of field:
+     --  - fixed inputs (inputs from the circuit named in the fixed set, assumed to be constant across cycles
+     --  - variable inputs (all other inputs from the circuit)
+     --  - outputs (all outputs from the circuit)
+     --  - state (all circuit flip-flop states)
+     --  - internal (right now, just a cycle counter)
+     let (fixedInputWidths, variableInputWidths) = Map.partitionWithKey (\nm _ -> Set.member nm fixedInputs) $ sequential ^. yosysSequentialInputWidths
+     let (fixedInputFields, variableInputFields) = Map.partitionWithKey (\nm _ -> Set.member nm fixedInputs) $ sequential ^. yosysSequentialInputFields
+     let internalWidths = Map.singleton "cycle" 8
+     internalFields <- forM internalWidths $ \w -> SC.scBitvector sc w
 
-  -- the "inputs" for our transition system are exclusively the circuit's variable inputs
-  Some inputFields <- sequentialReprs variableInputWidths
-  let inputReprs = TraversableFC.fmapFC (view sequentialFieldTypeRepr) $ inputFields ^. sequentialFields
-  let inputNames = TraversableFC.fmapFC (Const . W4.safeSymbol . Text.unpack . view sequentialFieldName) $ inputFields ^. sequentialFields
+     -- the "inputs" for our transition system are exclusively the circuit's variable inputs
+     Some inputFields <- sequentialReprs variableInputWidths
+     let inputReprs = TraversableFC.fmapFC (view sequentialFieldTypeRepr) $ inputFields ^. sequentialFields
+     let inputNames = TraversableFC.fmapFC (Const . W4.safeSymbol . Text.unpack . view sequentialFieldName) $ inputFields ^. sequentialFields
 
-  -- while the transition system "states" are everything else: flip-flop states, fixed inputs, all outputs, and the cycle counter
-  let combinedWidths = Map.unions
-        [ sequential ^. yosysSequentialStateWidths
-        , Map.mapKeys ("stateinput_"<>) fixedInputWidths
-        , Map.mapKeys ("stateoutput_"<>) $ sequential ^. yosysSequentialOutputWidths
-        , Map.mapKeys ("internal_"<>) internalWidths
-        ]
-  Some stateFields <- sequentialReprs combinedWidths
-  let stateReprs = TraversableFC.fmapFC (view sequentialFieldTypeRepr) $ stateFields ^. sequentialFields
-  let stateNames = TraversableFC.fmapFC (Const . W4.safeSymbol . Text.unpack . view sequentialFieldName) $ stateFields ^. sequentialFields
-  let lookupBinding nm bindings =
-        case Map.lookup nm bindings of
-          Just (vn, tp, _) -> SC.scVariable sc vn tp
-          Nothing -> throw $ YosysErrorTransitionSystemMissingField nm
-  let ts = W4.TransitionSystem
-        { W4.inputReprs = inputReprs
-        , W4.inputNames = inputNames
-        , W4.stateReprs = stateReprs
-        , W4.stateNames = stateNames
-        , W4.initialStatePredicate = \cur -> do
-            -- initially , we assert that cycle = 0
-            curInternalBindings <- ecBindingsOfFields sym sc "internal_" internalFields stateFields cur
-            cycleVal <- lookupBinding "cycle" curInternalBindings
-            zero <- SC.scBvConst sc 8 0
-            wnat <- SC.scNat sc 8
-            cyclePred <- SC.scBvEq sc wnat cycleVal zero
-            ref <- IORef.newIORef Map.empty
-            let args = Map.unions $ fmap (Map.fromList . fmap (\(vn, _ty, x) -> (SC.vnIndex vn, x)) . Map.elems)
-                  [ curInternalBindings
-                  ]
-            sval <- SimW4.w4SolveBasic sym sc Map.empty args ref Set.empty cyclePred
-            case sval of
-              Sim.VBool b -> pure b
-              _ -> throw YosysErrorTransitionSystemBadType
-        , W4.stateTransitions = \input cur next -> do
-            -- there is exactly one state transition, defined by the SAWCore function f representing the circuit
-            -- here, we assert that:
-            --  - the new value of each state field is equal to the same field in f(<previous state + all inputs>)
-            --  - the new value of each output is equal to the same output in f(<previous state + all inputs>)
-            --  - the new value of each fixed input is equal to the old value of that fixed input
-            --  - the new cycle counter is equal to the old cycle counter plus one
-            inputBindings <- ecBindingsOfFields sym sc "" (fst <$> variableInputFields) inputFields input
-            curBindings <- ecBindingsOfFields sym sc "" (fst <$> (sequential ^. yosysSequentialStateFields)) stateFields cur
-            curFixedInputBindings <- ecBindingsOfFields sym sc "stateinput_" (fst <$> fixedInputFields) stateFields cur
-            curInternalBindings <- ecBindingsOfFields sym sc "internal_" internalFields stateFields cur
-            nextBindings <- ecBindingsOfFields sym sc "" (fst <$> (sequential ^. yosysSequentialStateFields)) stateFields next
-            nextFixedInputBindings <- ecBindingsOfFields sym sc "stateinput_" (fst <$> fixedInputFields) stateFields next
-            nextOutputBindings <- ecBindingsOfFields sym sc "stateoutput_" (fst <$> (sequential ^. yosysSequentialOutputFields)) stateFields next
-            nextInternalBindings <- ecBindingsOfFields sym sc "internal_" internalFields stateFields next
-            inps <- fmap Map.fromList . forM (Map.assocs $ sequential ^. yosysSequentialInputWidths) $ \(nm, _) ->
-              let bindings = if Set.member nm fixedInputs then curFixedInputBindings else inputBindings
-              in (nm,) <$> lookupBinding nm bindings
-            states <- forM curBindings $ \(vn, tp, _) -> SC.scVariable sc vn tp
-            inpst <- cryptolRecord sc states
-            domainRec <- cryptolRecord sc $ Map.insert "__state__" inpst inps
-            codomainRec <- SC.scApply sc (sequential ^. yosysSequentialTerm . SC.ttTermLens) domainRec
-            codomainFields <- insertStateField sc (sequential ^. yosysSequentialStateFields) $ sequential ^. yosysSequentialOutputFields
-            outst <- cryptolRecordSelect sc codomainFields codomainRec "__state__"
-            stPreds <- forM (Map.assocs $ sequential ^. yosysSequentialStateWidths) $ \(nm, w) -> do
-              val <- cryptolRecordSelect sc (sequential ^. yosysSequentialStateFields) outst nm
-              wnat <- SC.scNat sc w
-              new <- lookupBinding nm nextBindings
-              SC.scBvEq sc wnat new val
-            outputPreds <- forM (Map.assocs $ sequential ^. yosysSequentialOutputWidths) $ \(nm, w) -> do
-              val <- cryptolRecordSelect sc codomainFields codomainRec nm
-              wnat <- SC.scNat sc w
-              new <- lookupBinding nm nextOutputBindings
-              SC.scBvEq sc wnat new val
-            fixedInputPreds <- forM (Map.assocs fixedInputWidths) $ \(nm, w) -> do
-              wnat <- SC.scNat sc w
-              val <- lookupBinding nm curFixedInputBindings
-              new <- lookupBinding nm nextFixedInputBindings
-              SC.scBvEq sc wnat new val
-            cycleIncrement <- do
-              wnat <- SC.scNat sc 8
-              val <- lookupBinding "cycle" curInternalBindings
-              one <- SC.scBvConst sc 8 1
-              incremented <- SC.scBvAdd sc wnat val one
-              new <- lookupBinding "cycle" nextInternalBindings
-              SC.scBvEq sc wnat new incremented
-            identity <- SC.scBool sc True
-            conj <- foldM (SC.scAnd sc) identity $ stPreds <> outputPreds <> fixedInputPreds <> [cycleIncrement]
-            ref <- IORef.newIORef Map.empty
-            let args = Map.unions $ fmap (Map.fromList . fmap (\(vn, _tp, x) -> (SC.vnIndex vn, x)) . Map.elems)
-                  [ inputBindings
-                  , curBindings
-                  , curFixedInputBindings
-                  , curInternalBindings
-                  , nextBindings
-                  , nextOutputBindings
-                  , nextFixedInputBindings
-                  , nextInternalBindings
-                  ]
-            sval <- SimW4.w4SolveBasic sym sc Map.empty args ref Set.empty conj
-            w4Conj <- case sval of
-              Sim.VBool b -> pure b
-              _ -> throw YosysErrorTransitionSystemBadType
-            pure
-              [ (W4.systemSymbol "default!", w4Conj)
-              ]
-        , W4.queries = \cur -> do
-            -- here we generate a single query, corresponding to the provided query term q
-            -- this is q applied to:
-            --  - the cycle counter (an 8-bit bitvector)
-            --  - a record of the fixed inputs (as usual really a SAWCore tuple, ordered per the Cryptol record type)
-            --  - a record of the outputs
-            curFixedInputBindings <- ecBindingsOfFields sym sc "stateinput_" (fst <$> fixedInputFields) stateFields cur
-            curOutputBindings <- ecBindingsOfFields sym sc "stateoutput_" (fst <$> (sequential ^. yosysSequentialOutputFields)) stateFields cur
-            curInternalBindings <- ecBindingsOfFields sym sc "internal_" internalFields stateFields cur
-            fixedInps <- fmap Map.fromList . forM (Map.assocs fixedInputWidths) $ \(nm, _) ->
-              (nm,) <$> lookupBinding nm curFixedInputBindings
-            outputs <- fmap Map.fromList . forM (Map.assocs $ sequential ^. yosysSequentialOutputWidths) $ \(nm, _) ->
-              (nm,) <$> lookupBinding nm curOutputBindings
-            cycleVal <- lookupBinding "cycle" curInternalBindings
-            fixedInputRec <- cryptolRecord sc fixedInps
-            outputRec <- cryptolRecord sc outputs
-            result <- SC.scApplyAll sc (query ^. SC.ttTermLens) [cycleVal, fixedInputRec, outputRec]
-            ref <- IORef.newIORef Map.empty
-            let args = Map.unions $ fmap (Map.fromList . fmap (\(vn, _ty, x) -> (SC.vnIndex vn, x)) . Map.elems)
-                  [ curOutputBindings
-                  , curFixedInputBindings
-                  , curInternalBindings
-                  ]
-            sval <- SimW4.w4SolveBasic sym sc Map.empty args ref Set.empty result
-            w4Pred <- case sval of
-              Sim.VBool b -> pure b
-              _ -> throw . YosysError $ "Invalid type when converting predicate to What4: " <> Text.pack (show sval)
-            pure [w4Pred]
-        }
-  sts <- Sally.exportTransitionSystem sym Sally.mySallyNames ts
-  sexp <- Sally.sexpOfSally sym sts
-  BS.writeFile path . encodeUtf8 . Text.pack . show $ Sally.sexpToDoc sexp
-  pure ()
+     -- while the transition system "states" are everything else: flip-flop states, fixed inputs, all outputs, and the cycle counter
+     let combinedWidths = Map.unions
+           [ sequential ^. yosysSequentialStateWidths
+           , Map.mapKeys ("stateinput_"<>) fixedInputWidths
+           , Map.mapKeys ("stateoutput_"<>) $ sequential ^. yosysSequentialOutputWidths
+           , Map.mapKeys ("internal_"<>) internalWidths
+           ]
+     Some stateFields <- sequentialReprs combinedWidths
+     let stateReprs = TraversableFC.fmapFC (view sequentialFieldTypeRepr) $ stateFields ^. sequentialFields
+     let stateNames = TraversableFC.fmapFC (Const . W4.safeSymbol . Text.unpack . view sequentialFieldName) $ stateFields ^. sequentialFields
+     let lookupBinding nm bindings =
+           case Map.lookup nm bindings of
+             Just (vn, tp, _) -> SC.scVariable sc vn tp
+             Nothing -> throw $ YosysErrorTransitionSystemMissingField nm
+     let ts = W4.TransitionSystem
+           { W4.inputReprs = inputReprs
+           , W4.inputNames = inputNames
+           , W4.stateReprs = stateReprs
+           , W4.stateNames = stateNames
+           , W4.initialStatePredicate = \cur ->
+               do -- initially , we assert that cycle = 0
+                  curInternalBindings <- ecBindingsOfFields sym sc "internal_" internalFields stateFields cur
+                  cycleVal <- lookupBinding "cycle" curInternalBindings
+                  zero <- SC.scBvConst sc 8 0
+                  wnat <- SC.scNat sc 8
+                  cyclePred <- SC.scBvEq sc wnat cycleVal zero
+                  ref <- IORef.newIORef Map.empty
+                  let args = Map.unions $ fmap (Map.fromList . fmap (\(vn, _ty, x) -> (SC.vnIndex vn, x)) . Map.elems)
+                        [ curInternalBindings
+                        ]
+                  sval <- SimW4.w4SolveBasic sym sc Map.empty args ref Set.empty cyclePred
+                  case sval of
+                    Sim.VBool b -> pure b
+                    _ -> throw YosysErrorTransitionSystemBadType
+           , W4.stateTransitions = \input cur next ->
+               do -- there is exactly one state transition, defined by the SAWCore function f representing the circuit
+                  -- here, we assert that:
+                  --  - the new value of each state field is equal to the same field in f(<previous state + all inputs>)
+                  --  - the new value of each output is equal to the same output in f(<previous state + all inputs>)
+                  --  - the new value of each fixed input is equal to the old value of that fixed input
+                  --  - the new cycle counter is equal to the old cycle counter plus one
+                  inputBindings <- ecBindingsOfFields sym sc "" (fst <$> variableInputFields) inputFields input
+                  curBindings <- ecBindingsOfFields sym sc "" (fst <$> (sequential ^. yosysSequentialStateFields)) stateFields cur
+                  curFixedInputBindings <- ecBindingsOfFields sym sc "stateinput_" (fst <$> fixedInputFields) stateFields cur
+                  curInternalBindings <- ecBindingsOfFields sym sc "internal_" internalFields stateFields cur
+                  nextBindings <- ecBindingsOfFields sym sc "" (fst <$> (sequential ^. yosysSequentialStateFields)) stateFields next
+                  nextFixedInputBindings <- ecBindingsOfFields sym sc "stateinput_" (fst <$> fixedInputFields) stateFields next
+                  nextOutputBindings <- ecBindingsOfFields sym sc "stateoutput_" (fst <$> (sequential ^. yosysSequentialOutputFields)) stateFields next
+                  nextInternalBindings <- ecBindingsOfFields sym sc "internal_" internalFields stateFields next
+                  inps <-
+                    fmap Map.fromList . forM (Map.assocs $ sequential ^. yosysSequentialInputWidths) $ \(nm, _) ->
+                    let bindings = if Set.member nm fixedInputs then curFixedInputBindings else inputBindings
+                    in (nm,) <$> lookupBinding nm bindings
+                  states <- forM curBindings $ \(vn, tp, _) -> SC.scVariable sc vn tp
+                  inpst <- cryptolRecord sc states
+                  domainRec <- cryptolRecord sc $ Map.insert "__state__" inpst inps
+                  codomainRec <- SC.scApply sc (sequential ^. yosysSequentialTerm . SC.ttTermLens) domainRec
+                  codomainFields <- insertStateField sc (sequential ^. yosysSequentialStateFields) $ sequential ^. yosysSequentialOutputFields
+                  outst <- cryptolRecordSelect sc codomainFields codomainRec "__state__"
+                  stPreds <-
+                    forM (Map.assocs $ sequential ^. yosysSequentialStateWidths) $ \(nm, w) ->
+                    do val <- cryptolRecordSelect sc (sequential ^. yosysSequentialStateFields) outst nm
+                       wnat <- SC.scNat sc w
+                       new <- lookupBinding nm nextBindings
+                       SC.scBvEq sc wnat new val
+                  outputPreds <-
+                    forM (Map.assocs $ sequential ^. yosysSequentialOutputWidths) $ \(nm, w) ->
+                    do val <- cryptolRecordSelect sc codomainFields codomainRec nm
+                       wnat <- SC.scNat sc w
+                       new <- lookupBinding nm nextOutputBindings
+                       SC.scBvEq sc wnat new val
+                  fixedInputPreds <-
+                    forM (Map.assocs fixedInputWidths) $ \(nm, w) ->
+                    do wnat <- SC.scNat sc w
+                       val <- lookupBinding nm curFixedInputBindings
+                       new <- lookupBinding nm nextFixedInputBindings
+                       SC.scBvEq sc wnat new val
+                  cycleIncrement <-
+                    do wnat <- SC.scNat sc 8
+                       val <- lookupBinding "cycle" curInternalBindings
+                       one <- SC.scBvConst sc 8 1
+                       incremented <- SC.scBvAdd sc wnat val one
+                       new <- lookupBinding "cycle" nextInternalBindings
+                       SC.scBvEq sc wnat new incremented
+                  identity <- SC.scBool sc True
+                  conj <- foldM (SC.scAnd sc) identity $ stPreds <> outputPreds <> fixedInputPreds <> [cycleIncrement]
+                  ref <- IORef.newIORef Map.empty
+                  let args =
+                        Map.unions $ fmap (Map.fromList . fmap (\(vn, _tp, x) -> (SC.vnIndex vn, x)) . Map.elems)
+                        [ inputBindings
+                        , curBindings
+                        , curFixedInputBindings
+                        , curInternalBindings
+                        , nextBindings
+                        , nextOutputBindings
+                        , nextFixedInputBindings
+                        , nextInternalBindings
+                        ]
+                  sval <- SimW4.w4SolveBasic sym sc Map.empty args ref Set.empty conj
+                  w4Conj <-
+                    case sval of
+                      Sim.VBool b -> pure b
+                      _ -> throw YosysErrorTransitionSystemBadType
+                  pure
+                    [ (W4.systemSymbol "default!", w4Conj)
+                    ]
+           , W4.queries = \cur ->
+               do -- here we generate a single query, corresponding to the provided query term q
+                  -- this is q applied to:
+                  --  - the cycle counter (an 8-bit bitvector)
+                  --  - a record of the fixed inputs (as usual really a SAWCore tuple, ordered per the Cryptol record type)
+                  --  - a record of the outputs
+                  curFixedInputBindings <- ecBindingsOfFields sym sc "stateinput_" (fst <$> fixedInputFields) stateFields cur
+                  curOutputBindings <- ecBindingsOfFields sym sc "stateoutput_" (fst <$> (sequential ^. yosysSequentialOutputFields)) stateFields cur
+                  curInternalBindings <- ecBindingsOfFields sym sc "internal_" internalFields stateFields cur
+                  fixedInps <-
+                    fmap Map.fromList . forM (Map.assocs fixedInputWidths) $ \(nm, _) ->
+                    (nm,) <$> lookupBinding nm curFixedInputBindings
+                  outputs <-
+                    fmap Map.fromList . forM (Map.assocs $ sequential ^. yosysSequentialOutputWidths) $ \(nm, _) ->
+                    (nm,) <$> lookupBinding nm curOutputBindings
+                  cycleVal <- lookupBinding "cycle" curInternalBindings
+                  fixedInputRec <- cryptolRecord sc fixedInps
+                  outputRec <- cryptolRecord sc outputs
+                  result <- SC.scApplyAll sc (query ^. SC.ttTermLens) [cycleVal, fixedInputRec, outputRec]
+                  ref <- IORef.newIORef Map.empty
+                  let args =
+                        Map.unions $ fmap (Map.fromList . fmap (\(vn, _ty, x) -> (SC.vnIndex vn, x)) . Map.elems)
+                        [ curOutputBindings
+                        , curFixedInputBindings
+                        , curInternalBindings
+                        ]
+                  sval <- SimW4.w4SolveBasic sym sc Map.empty args ref Set.empty result
+                  w4Pred <-
+                    case sval of
+                      Sim.VBool b -> pure b
+                      _ -> throw . YosysError $ "Invalid type when converting predicate to What4: " <> Text.pack (show sval)
+                  pure [w4Pred]
+           }
+     sts <- Sally.exportTransitionSystem sym Sally.mySallyNames ts
+     sexp <- Sally.sexpOfSally sym sts
+     BS.writeFile path . encodeUtf8 . Text.pack . show $ Sally.sexpToDoc sexp
+     pure ()
diff --git a/saw-central/src/SAWCentral/Yosys/Utils.hs b/saw-central/src/SAWCentral/Yosys/Utils.hs
index 998771d7d6..e7a0b9bfe1 100644
--- a/saw-central/src/SAWCentral/Yosys/Utils.hs
+++ b/saw-central/src/SAWCentral/Yosys/Utils.hs
@@ -206,24 +206,27 @@ cryptolRecordSelectTyped ::
   SC.TypedTerm ->
   Text ->
   IO SC.TypedTerm
-cryptolRecordSelectTyped sc r nm = do
-  fields <- Map.mapKeys C.identText . Map.fromList . C.canonicalFields <$> case SC.ttType r of
-    SC.TypedTermSchema (C.Forall [] [] (C.TRec fs)) -> pure fs
-    _ -> throwIO $ YosysError $ mconcat
-      [ "Type\n"
-      , Text.pack . show $ SC.ttType r
-      , "\nis not a record type"
-      ]
-  cty <- case Map.lookup nm fields of
-    Just cty -> pure cty
-    _ -> throwIO $ YosysError $ mconcat
-      [ "Record type\n"
-      , Text.pack . show $ SC.ttType r
-      , "\ndoes not have field "
-      , nm
-      ]
-  t <- cryptolRecordSelect sc fields (SC.ttTerm r) nm
-  pure $ SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) t
+cryptolRecordSelectTyped sc r nm =
+  do fields <-
+       Map.mapKeys C.identText . Map.fromList . C.canonicalFields <$>
+       case SC.ttType r of
+         SC.TypedTermSchema (C.Forall [] [] (C.TRec fs)) -> pure fs
+         _ -> throwIO $ YosysError $ mconcat
+           [ "Type\n"
+           , Text.pack . show $ SC.ttType r
+           , "\nis not a record type"
+           ]
+     cty <-
+       case Map.lookup nm fields of
+         Just cty -> pure cty
+         _ -> throwIO $ YosysError $ mconcat
+           [ "Record type\n"
+           , Text.pack . show $ SC.ttType r
+           , "\ndoes not have field "
+           , nm
+           ]
+     t <- cryptolRecordSelect sc fields (SC.ttTerm r) nm
+     pure $ SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) t
 
 -- | Construct a SAWCore expression asserting equality between each
 -- field of two records. Both records should be tuples corresponding
@@ -234,33 +237,38 @@ eqBvRecords ::
   SC.Term ->
   SC.Term ->
   IO SC.Term
-eqBvRecords sc cty a b = do
-  fields <- Map.mapKeys C.identText . Map.fromList . C.canonicalFields <$> case cty of
-    C.TRec fs -> pure fs
-    _ -> throwIO $ YosysError $ mconcat
-      [ "Type\n"
-      , Text.pack $ show cty
-      , "\nis not a record type"
-      ]
-  eqs <- forM (Map.assocs fields) $ \(nm, fcty) -> do
-    w <- case fcty of
-      C.TCon (C.TC C.TCSeq) [C.TCon (C.TC (C.TCNum wint)) [], C.TCon (C.TC C.TCBit) []] ->
-        SC.scNat sc $ fromIntegral wint
-      _ -> throwIO $  YosysError $ mconcat
-        [ "Type\n"
-        , Text.pack $ show fcty
-        , "\nis not a bitvector type"
-        ]
-    fa <- cryptolRecordSelect sc fields a nm
-    fb <- cryptolRecordSelect sc fields b nm
-    SC.scBvEq sc w fa fb
-  case eqs of
-    [] -> throwIO $ YosysError $ mconcat
-      [ "Record type\n"
-      , Text.pack $ show cty
-      , "\nhas no fields"
-      ]
-    (e:es) -> foldM (\x y -> SC.scAnd sc x y) e es
+eqBvRecords sc cty a b =
+  do fields <-
+       Map.mapKeys C.identText . Map.fromList . C.canonicalFields <$>
+       case cty of
+         C.TRec fs -> pure fs
+         _ -> throwIO $ YosysError $ mconcat
+           [ "Type\n"
+           , Text.pack $ show cty
+           , "\nis not a record type"
+           ]
+     eqs <-
+       forM (Map.assocs fields) $ \(nm, fcty) ->
+       do w <-
+            case fcty of
+              C.TCon (C.TC C.TCSeq) [C.TCon (C.TC (C.TCNum wint)) [], C.TCon (C.TC C.TCBit) []] ->
+                SC.scNat sc $ fromIntegral wint
+              _ -> throwIO $  YosysError $ mconcat
+                [ "Type\n"
+                , Text.pack $ show fcty
+                , "\nis not a bitvector type"
+                ]
+          fa <- cryptolRecordSelect sc fields a nm
+          fb <- cryptolRecordSelect sc fields b nm
+          SC.scBvEq sc w fa fb
+     case eqs of
+       [] ->
+         throwIO $ YosysError $ mconcat
+         [ "Record type\n"
+         , Text.pack $ show cty
+         , "\nhas no fields"
+         ]
+       (e:es) -> foldM (\x y -> SC.scAnd sc x y) e es
 
 -- | Encode the given string such that is a valid Cryptol identifier.
 -- Since Yosys cell names often look like "\42", this makes it much
@@ -285,14 +293,14 @@ fieldsToCryptolType fields = pure . C.tRec . C.recordFromFields $ bimap C.mkIden
 -- that output pattern with the term, and each bit of that pattern
 -- with the corresponding bit of the term.
 deriveTermsByIndices :: (Ord b) => SC.SharedContext -> [b] -> SC.Term -> IO (Map [b] Preterm)
-deriveTermsByIndices _sc rep t = do
-  let len = length rep
-  let bit i = PretermSlice (fromIntegral (len - 1 - i)) 1 (fromIntegral i) t
-  let telems = map bit [0..len-1]
-  pure . Map.fromList $ mconcat
-    [ [(rep, PretermSlice 0 (fromIntegral len) 0 t)]
-    , zip ((:[]) <$> rep) telems
-    ]
+deriveTermsByIndices _sc rep t =
+  do let len = length rep
+     let bit i = PretermSlice (fromIntegral (len - 1 - i)) 1 (fromIntegral i) t
+     let telems = map bit [0..len-1]
+     pure . Map.fromList $ mconcat
+       [ [(rep, PretermSlice 0 (fromIntegral len) 0 t)]
+       , zip ((:[]) <$> rep) telems
+       ]
 
 --------------------------------------------------------------------------------
 -- ** Pre-terms

From 277a9063d2595416fb26d93945691efad4eb7f28 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 17 Nov 2025 21:12:18 -0800
Subject: [PATCH 3/4] saw-central/Yosys: Support "$_BUF_" cell type in yosys
 import.

Fixes #2828.
---
 saw-central/src/SAWCentral/Yosys/Cell.hs | 3 +++
 saw-central/src/SAWCentral/Yosys/IR.hs   | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/saw-central/src/SAWCentral/Yosys/Cell.hs b/saw-central/src/SAWCentral/Yosys/Cell.hs
index d06ea44bd6..7bb942939f 100644
--- a/saw-central/src/SAWCentral/Yosys/Cell.hs
+++ b/saw-central/src/SAWCentral/Yosys/Cell.hs
@@ -300,6 +300,9 @@ primCellToMap sc c args =
     -- "$concat" -> _
     CellTypeDff -> pure Nothing
     CellTypeFf -> pure Nothing
+    CellTypeBUF ->
+      do res <- input "A"
+         output res
     CellTypeUnsupportedPrimitive _ -> pure Nothing
     CellTypeUserType _ -> pure Nothing
   where
diff --git a/saw-central/src/SAWCentral/Yosys/IR.hs b/saw-central/src/SAWCentral/Yosys/IR.hs
index 32fef57ab5..2d612fbeae 100644
--- a/saw-central/src/SAWCentral/Yosys/IR.hs
+++ b/saw-central/src/SAWCentral/Yosys/IR.hs
@@ -135,6 +135,7 @@ textToPrimitiveCellType = Map.fromList
   , ("$bmux"        , CellTypeBmux)
   , ("$dff"         , CellTypeDff)
   , ("$ff"          , CellTypeFf)
+  , ("$_BUF_"       , CellTypeBUF)
   ]
 
 -- | Mapping from primitive cell types to textual representation
@@ -183,6 +184,7 @@ data CellType
   | CellTypeBmux
   | CellTypeDff
   | CellTypeFf
+  | CellTypeBUF
   | CellTypeUnsupportedPrimitive Text
   | CellTypeUserType Text
   deriving (Eq, Ord)

From 93505e7c0bd250edcaa99aedac13a56835866e66 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 21 Nov 2025 09:18:37 -0800
Subject: [PATCH 4/4] intTests: Add regression test for #2828.

---
 intTests/test2828/README.txt       |  15 +
 intTests/test2828/adder_tabby.json | 684 +++++++++++++++++++++++++++++
 intTests/test2828/adder_yosys.json | 478 ++++++++++++++++++++
 intTests/test2828/test.saw         |   6 +
 intTests/test2828/test.sh          |   1 +
 5 files changed, 1184 insertions(+)
 create mode 100644 intTests/test2828/README.txt
 create mode 100644 intTests/test2828/adder_tabby.json
 create mode 100644 intTests/test2828/adder_yosys.json
 create mode 100644 intTests/test2828/test.saw
 create mode 100644 intTests/test2828/test.sh

diff --git a/intTests/test2828/README.txt b/intTests/test2828/README.txt
new file mode 100644
index 0000000000..b1c646e45d
--- /dev/null
+++ b/intTests/test2828/README.txt
@@ -0,0 +1,15 @@
+File `adder_yosys.json` is produced using the directions in the
+"Analyzing Hardware Circuits using Yosys" section of the SAW User
+Manual.
+
+File `adder_tabby.json` is generated using the following commands in
+TabbyCAD:
+
+yosys> read -vhd adder.vhdl
+yosys> hierarchy -check -top add4
+yosys> write_json adder_tabby.json
+
+TabbyCAD/Verific insert some extra cells of type "$_BUF_" which are
+not present in `adder_yosys.json`. This proof script ensures that the
+TabbyCAD version can be read and proved equivalent to the plain Yosys
+version.
diff --git a/intTests/test2828/adder_tabby.json b/intTests/test2828/adder_tabby.json
new file mode 100644
index 0000000000..9d5ea74dfe
--- /dev/null
+++ b/intTests/test2828/adder_tabby.json
@@ -0,0 +1,684 @@
+{
+  "creator": "Yosys 0.59 (git sha1 5df4c20be, aarch64-linux-gnu-g++ 11.4.0-1ubuntu1~22.04 -fPIC -O3)",
+  "modules": {
+    "add4": {
+      "attributes": {
+        "top": "00000000000000000000000000000001",
+        "architecture": "add4arch",
+        "library": "work",
+        "hdlname": "add4",
+        "src_entity": "adder.vhd:46.8-46.12",
+        "src": "adder.vhd:54.14-54.22"
+      },
+      "ports": {
+        "a": {
+          "direction": "input",
+          "upto": 1,
+          "bits": [ 2, 3, 4, 5 ]
+        },
+        "b": {
+          "direction": "input",
+          "upto": 1,
+          "bits": [ 6, 7, 8, 9 ]
+        },
+        "res": {
+          "direction": "output",
+          "upto": 1,
+          "bits": [ 10, 11, 12, 13 ]
+        }
+      },
+      "cells": {
+        "full0": {
+          "hide_name": 0,
+          "type": "full_default(fullarch)",
+          "parameters": {
+          },
+          "attributes": {
+            "src": "adder.vhd:60.3-60.8"
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "cin": "input",
+            "cout": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 5 ],
+            "b": [ 9 ],
+            "cin": [ "0" ],
+            "cout": [ 14 ],
+            "s": [ 13 ]
+          }
+        },
+        "full1": {
+          "hide_name": 0,
+          "type": "full_default(fullarch)",
+          "parameters": {
+          },
+          "attributes": {
+            "src": "adder.vhd:61.3-61.8"
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "cin": "input",
+            "cout": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 4 ],
+            "b": [ 8 ],
+            "cin": [ 14 ],
+            "cout": [ 15 ],
+            "s": [ 12 ]
+          }
+        },
+        "full2": {
+          "hide_name": 0,
+          "type": "full_default(fullarch)",
+          "parameters": {
+          },
+          "attributes": {
+            "src": "adder.vhd:62.3-62.8"
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "cin": "input",
+            "cout": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 3 ],
+            "b": [ 7 ],
+            "cin": [ 15 ],
+            "cout": [ 16 ],
+            "s": [ 11 ]
+          }
+        },
+        "full3": {
+          "hide_name": 0,
+          "type": "full_default(fullarch)",
+          "parameters": {
+          },
+          "attributes": {
+            "src": "adder.vhd:63.3-63.8"
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "cin": "input",
+            "cout": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 2 ],
+            "b": [ 6 ],
+            "cin": [ 16 ],
+            "cout": [ 17 ],
+            "s": [ 10 ]
+          }
+        }
+      },
+      "netnames": {
+        "$verific$full0$adder.vhd:60$3": {
+          "hide_name": 1,
+          "bits": [ 18 ],
+          "attributes": {
+          }
+        },
+        "$verific$full0$adder.vhd:60$4": {
+          "hide_name": 1,
+          "bits": [ 19 ],
+          "attributes": {
+          }
+        },
+        "$verific$full0$adder.vhd:60$5": {
+          "hide_name": 1,
+          "bits": [ 20 ],
+          "attributes": {
+          }
+        },
+        "$verific$full0$adder.vhd:60$6": {
+          "hide_name": 1,
+          "bits": [ 21 ],
+          "attributes": {
+          }
+        },
+        "$verific$full0$adder.vhd:60$7": {
+          "hide_name": 1,
+          "bits": [ 22 ],
+          "attributes": {
+          }
+        },
+        "$verific$full1$adder.vhd:61$10": {
+          "hide_name": 1,
+          "bits": [ 23 ],
+          "attributes": {
+          }
+        },
+        "$verific$full1$adder.vhd:61$11": {
+          "hide_name": 1,
+          "bits": [ 24 ],
+          "attributes": {
+          }
+        },
+        "$verific$full1$adder.vhd:61$12": {
+          "hide_name": 1,
+          "bits": [ 25 ],
+          "attributes": {
+          }
+        },
+        "$verific$full1$adder.vhd:61$8": {
+          "hide_name": 1,
+          "bits": [ 26 ],
+          "attributes": {
+          }
+        },
+        "$verific$full1$adder.vhd:61$9": {
+          "hide_name": 1,
+          "bits": [ 27 ],
+          "attributes": {
+          }
+        },
+        "$verific$full2$adder.vhd:62$13": {
+          "hide_name": 1,
+          "bits": [ 28 ],
+          "attributes": {
+          }
+        },
+        "$verific$full2$adder.vhd:62$14": {
+          "hide_name": 1,
+          "bits": [ 29 ],
+          "attributes": {
+          }
+        },
+        "$verific$full2$adder.vhd:62$15": {
+          "hide_name": 1,
+          "bits": [ 30 ],
+          "attributes": {
+          }
+        },
+        "$verific$full2$adder.vhd:62$16": {
+          "hide_name": 1,
+          "bits": [ 31 ],
+          "attributes": {
+          }
+        },
+        "$verific$full2$adder.vhd:62$17": {
+          "hide_name": 1,
+          "bits": [ 32 ],
+          "attributes": {
+          }
+        },
+        "$verific$full3$adder.vhd:63$18": {
+          "hide_name": 1,
+          "bits": [ 33 ],
+          "attributes": {
+          }
+        },
+        "$verific$full3$adder.vhd:63$19": {
+          "hide_name": 1,
+          "bits": [ 34 ],
+          "attributes": {
+          }
+        },
+        "$verific$full3$adder.vhd:63$20": {
+          "hide_name": 1,
+          "bits": [ 35 ],
+          "attributes": {
+          }
+        },
+        "$verific$full3$adder.vhd:63$21": {
+          "hide_name": 1,
+          "bits": [ 36 ],
+          "attributes": {
+          }
+        },
+        "$verific$full3$adder.vhd:63$22": {
+          "hide_name": 1,
+          "bits": [ 37 ],
+          "attributes": {
+          }
+        },
+        "$verific$n1$1": {
+          "hide_name": 1,
+          "bits": [ "0" ],
+          "attributes": {
+          }
+        },
+        "a": {
+          "hide_name": 0,
+          "bits": [ 2, 3, 4, 5 ],
+          "upto": 1,
+          "attributes": {
+            "src": "adder.vhd:48.5-48.6"
+          }
+        },
+        "b": {
+          "hide_name": 0,
+          "bits": [ 6, 7, 8, 9 ],
+          "upto": 1,
+          "attributes": {
+            "src": "adder.vhd:49.5-49.6"
+          }
+        },
+        "full0cout": {
+          "hide_name": 0,
+          "bits": [ 14 ],
+          "attributes": {
+            "src": "adder.vhd:55.10-55.19"
+          }
+        },
+        "full1cout": {
+          "hide_name": 0,
+          "bits": [ 15 ],
+          "attributes": {
+            "src": "adder.vhd:56.10-56.19"
+          }
+        },
+        "full2cout": {
+          "hide_name": 0,
+          "bits": [ 16 ],
+          "attributes": {
+            "src": "adder.vhd:57.10-57.19"
+          }
+        },
+        "ignore": {
+          "hide_name": 0,
+          "bits": [ 17 ],
+          "attributes": {
+            "src": "adder.vhd:58.10-58.16"
+          }
+        },
+        "res": {
+          "hide_name": 0,
+          "bits": [ 10, 11, 12, 13 ],
+          "upto": 1,
+          "attributes": {
+            "src": "adder.vhd:50.5-50.8"
+          }
+        }
+      }
+    },
+    "full_default(fullarch)": {
+      "attributes": {
+        "architecture": "fullarch",
+        "library": "work",
+        "hdlname": "full",
+        "src_entity": "adder.vhd:22.8-22.12",
+        "src": "adder.vhd:32.14-32.22"
+      },
+      "ports": {
+        "a": {
+          "direction": "input",
+          "bits": [ 2 ]
+        },
+        "b": {
+          "direction": "input",
+          "bits": [ 3 ]
+        },
+        "cin": {
+          "direction": "input",
+          "bits": [ 4 ]
+        },
+        "cout": {
+          "direction": "output",
+          "bits": [ 5 ]
+        },
+        "s": {
+          "direction": "output",
+          "bits": [ 6 ]
+        }
+      },
+      "cells": {
+        "$verific$i4$adder.vhd:39$32": {
+          "hide_name": 1,
+          "type": "$or",
+          "parameters": {
+            "A_SIGNED": "00000000000000000000000000000000",
+            "A_WIDTH": "00000000000000000000000000000001",
+            "B_SIGNED": "00000000000000000000000000000000",
+            "B_WIDTH": "00000000000000000000000000000001",
+            "Y_WIDTH": "00000000000000000000000000000001"
+          },
+          "attributes": {
+            "src": "adder.vhd:39.11-39.27"
+          },
+          "port_directions": {
+            "A": "input",
+            "B": "input",
+            "Y": "output"
+          },
+          "connections": {
+            "A": [ 7 ],
+            "B": [ 8 ],
+            "Y": [ 9 ]
+          }
+        },
+        "$verific$i5$adder.vhd:39$33": {
+          "hide_name": 1,
+          "type": "$_BUF_",
+          "parameters": {
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "A": "input",
+            "Y": "output"
+          },
+          "connections": {
+            "A": [ 9 ],
+            "Y": [ 5 ]
+          }
+        },
+        "half0": {
+          "hide_name": 0,
+          "type": "half_default(halfarch)",
+          "parameters": {
+          },
+          "attributes": {
+            "src": "adder.vhd:37.3-37.8"
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "c": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 2 ],
+            "b": [ 3 ],
+            "c": [ 7 ],
+            "s": [ 10 ]
+          }
+        },
+        "half1": {
+          "hide_name": 0,
+          "type": "half_default(halfarch)",
+          "parameters": {
+          },
+          "attributes": {
+            "src": "adder.vhd:38.3-38.8"
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "c": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 10 ],
+            "b": [ 4 ],
+            "c": [ 8 ],
+            "s": [ 6 ]
+          }
+        }
+      },
+      "netnames": {
+        "$verific$half0$adder.vhd:37$24": {
+          "hide_name": 1,
+          "bits": [ 11 ],
+          "attributes": {
+          }
+        },
+        "$verific$half0$adder.vhd:37$25": {
+          "hide_name": 1,
+          "bits": [ 12 ],
+          "attributes": {
+          }
+        },
+        "$verific$half0$adder.vhd:37$26": {
+          "hide_name": 1,
+          "bits": [ 13 ],
+          "attributes": {
+          }
+        },
+        "$verific$half0$adder.vhd:37$27": {
+          "hide_name": 1,
+          "bits": [ 14 ],
+          "attributes": {
+          }
+        },
+        "$verific$half1$adder.vhd:38$28": {
+          "hide_name": 1,
+          "bits": [ 15 ],
+          "attributes": {
+          }
+        },
+        "$verific$half1$adder.vhd:38$29": {
+          "hide_name": 1,
+          "bits": [ 16 ],
+          "attributes": {
+          }
+        },
+        "$verific$half1$adder.vhd:38$30": {
+          "hide_name": 1,
+          "bits": [ 17 ],
+          "attributes": {
+          }
+        },
+        "$verific$half1$adder.vhd:38$31": {
+          "hide_name": 1,
+          "bits": [ 18 ],
+          "attributes": {
+          }
+        },
+        "$verific$n12$23": {
+          "hide_name": 1,
+          "bits": [ 9 ],
+          "attributes": {
+          }
+        },
+        "a": {
+          "hide_name": 0,
+          "bits": [ 2 ],
+          "attributes": {
+            "src": "adder.vhd:24.5-24.6"
+          }
+        },
+        "b": {
+          "hide_name": 0,
+          "bits": [ 3 ],
+          "attributes": {
+            "src": "adder.vhd:25.5-25.6"
+          }
+        },
+        "cin": {
+          "hide_name": 0,
+          "bits": [ 4 ],
+          "attributes": {
+            "src": "adder.vhd:26.5-26.8"
+          }
+        },
+        "cout": {
+          "hide_name": 0,
+          "bits": [ 5 ],
+          "attributes": {
+            "src": "adder.vhd:27.5-27.9"
+          }
+        },
+        "half0c": {
+          "hide_name": 0,
+          "bits": [ 7 ],
+          "attributes": {
+            "src": "adder.vhd:33.10-33.16"
+          }
+        },
+        "half0s": {
+          "hide_name": 0,
+          "bits": [ 10 ],
+          "attributes": {
+            "src": "adder.vhd:34.10-34.16"
+          }
+        },
+        "half1c": {
+          "hide_name": 0,
+          "bits": [ 8 ],
+          "attributes": {
+            "src": "adder.vhd:35.10-35.16"
+          }
+        },
+        "s": {
+          "hide_name": 0,
+          "bits": [ 6 ],
+          "attributes": {
+            "src": "adder.vhd:28.5-28.6"
+          }
+        }
+      }
+    },
+    "half_default(halfarch)": {
+      "attributes": {
+        "architecture": "halfarch",
+        "library": "work",
+        "hdlname": "half",
+        "src_entity": "adder.vhd:4.8-4.12",
+        "src": "adder.vhd:13.14-13.22"
+      },
+      "ports": {
+        "a": {
+          "direction": "input",
+          "bits": [ 2 ]
+        },
+        "b": {
+          "direction": "input",
+          "bits": [ 3 ]
+        },
+        "c": {
+          "direction": "output",
+          "bits": [ 4 ]
+        },
+        "s": {
+          "direction": "output",
+          "bits": [ 5 ]
+        }
+      },
+      "cells": {
+        "$verific$i4$adder.vhd:15$36": {
+          "hide_name": 1,
+          "type": "$and",
+          "parameters": {
+            "A_SIGNED": "00000000000000000000000000000000",
+            "A_WIDTH": "00000000000000000000000000000001",
+            "B_SIGNED": "00000000000000000000000000000000",
+            "B_WIDTH": "00000000000000000000000000000001",
+            "Y_WIDTH": "00000000000000000000000000000001"
+          },
+          "attributes": {
+            "src": "adder.vhd:15.8-15.15"
+          },
+          "port_directions": {
+            "A": "input",
+            "B": "input",
+            "Y": "output"
+          },
+          "connections": {
+            "A": [ 2 ],
+            "B": [ 3 ],
+            "Y": [ 6 ]
+          }
+        },
+        "$verific$i5$adder.vhd:15$37": {
+          "hide_name": 1,
+          "type": "$_BUF_",
+          "parameters": {
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "A": "input",
+            "Y": "output"
+          },
+          "connections": {
+            "A": [ 6 ],
+            "Y": [ 4 ]
+          }
+        },
+        "$verific$i6$adder.vhd:16$38": {
+          "hide_name": 1,
+          "type": "$xor",
+          "parameters": {
+            "A_SIGNED": "00000000000000000000000000000000",
+            "A_WIDTH": "00000000000000000000000000000001",
+            "B_SIGNED": "00000000000000000000000000000000",
+            "B_WIDTH": "00000000000000000000000000000001",
+            "Y_WIDTH": "00000000000000000000000000000001"
+          },
+          "attributes": {
+            "src": "adder.vhd:16.8-16.15"
+          },
+          "port_directions": {
+            "A": "input",
+            "B": "input",
+            "Y": "output"
+          },
+          "connections": {
+            "A": [ 2 ],
+            "B": [ 3 ],
+            "Y": [ 7 ]
+          }
+        },
+        "$verific$i7$adder.vhd:16$39": {
+          "hide_name": 1,
+          "type": "$_BUF_",
+          "parameters": {
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "A": "input",
+            "Y": "output"
+          },
+          "connections": {
+            "A": [ 7 ],
+            "Y": [ 5 ]
+          }
+        }
+      },
+      "netnames": {
+        "$verific$n4$34": {
+          "hide_name": 1,
+          "bits": [ 6 ],
+          "attributes": {
+          }
+        },
+        "$verific$n6$35": {
+          "hide_name": 1,
+          "bits": [ 7 ],
+          "attributes": {
+          }
+        },
+        "a": {
+          "hide_name": 0,
+          "bits": [ 2 ],
+          "attributes": {
+            "src": "adder.vhd:6.5-6.6"
+          }
+        },
+        "b": {
+          "hide_name": 0,
+          "bits": [ 3 ],
+          "attributes": {
+            "src": "adder.vhd:7.5-7.6"
+          }
+        },
+        "c": {
+          "hide_name": 0,
+          "bits": [ 4 ],
+          "attributes": {
+            "src": "adder.vhd:8.5-8.6"
+          }
+        },
+        "s": {
+          "hide_name": 0,
+          "bits": [ 5 ],
+          "attributes": {
+            "src": "adder.vhd:9.5-9.6"
+          }
+        }
+      }
+    }
+  }
+}
diff --git a/intTests/test2828/adder_yosys.json b/intTests/test2828/adder_yosys.json
new file mode 100644
index 0000000000..32dd977a80
--- /dev/null
+++ b/intTests/test2828/adder_yosys.json
@@ -0,0 +1,478 @@
+{
+  "creator": "Yosys 0.33 (git sha1 2584903a060)",
+  "modules": {
+    "add4": {
+      "attributes": {
+      },
+      "ports": {
+        "a": {
+          "direction": "input",
+          "bits": [ 2, 3, 4, 5 ]
+        },
+        "b": {
+          "direction": "input",
+          "bits": [ 6, 7, 8, 9 ]
+        },
+        "res": {
+          "direction": "output",
+          "bits": [ 10, 11, 12, 13 ]
+        }
+      },
+      "cells": {
+        "full0": {
+          "hide_name": 0,
+          "type": "full_Bfullarch",
+          "parameters": {
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "cin": "input",
+            "cout": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 5 ],
+            "b": [ 9 ],
+            "cin": [ "0" ],
+            "cout": [ 14 ],
+            "s": [ 13 ]
+          }
+        },
+        "full1": {
+          "hide_name": 0,
+          "type": "full_Bfullarch",
+          "parameters": {
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "cin": "input",
+            "cout": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 4 ],
+            "b": [ 8 ],
+            "cin": [ 14 ],
+            "cout": [ 15 ],
+            "s": [ 12 ]
+          }
+        },
+        "full2": {
+          "hide_name": 0,
+          "type": "full_Bfullarch",
+          "parameters": {
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "cin": "input",
+            "cout": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 3 ],
+            "b": [ 7 ],
+            "cin": [ 15 ],
+            "cout": [ 16 ],
+            "s": [ 11 ]
+          }
+        },
+        "full3": {
+          "hide_name": 0,
+          "type": "full_Bfullarch",
+          "parameters": {
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "cin": "input",
+            "cout": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 2 ],
+            "b": [ 6 ],
+            "cin": [ 16 ],
+            "cout": [ 17 ],
+            "s": [ 10 ]
+          }
+        }
+      },
+      "netnames": {
+        "$auto$ghdl.cc:827:import_module$1": {
+          "hide_name": 1,
+          "bits": [ 14 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$2": {
+          "hide_name": 1,
+          "bits": [ 13 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$3": {
+          "hide_name": 1,
+          "bits": [ 15 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$4": {
+          "hide_name": 1,
+          "bits": [ 12 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$5": {
+          "hide_name": 1,
+          "bits": [ 16 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$6": {
+          "hide_name": 1,
+          "bits": [ 11 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$7": {
+          "hide_name": 1,
+          "bits": [ 17 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$8": {
+          "hide_name": 1,
+          "bits": [ 10 ],
+          "attributes": {
+          }
+        },
+        "a": {
+          "hide_name": 0,
+          "bits": [ 2, 3, 4, 5 ],
+          "attributes": {
+          }
+        },
+        "b": {
+          "hide_name": 0,
+          "bits": [ 6, 7, 8, 9 ],
+          "attributes": {
+          }
+        },
+        "full0cout": {
+          "hide_name": 0,
+          "bits": [ 14 ],
+          "attributes": {
+          }
+        },
+        "full1cout": {
+          "hide_name": 0,
+          "bits": [ 15 ],
+          "attributes": {
+          }
+        },
+        "full2cout": {
+          "hide_name": 0,
+          "bits": [ 16 ],
+          "attributes": {
+          }
+        },
+        "res": {
+          "hide_name": 0,
+          "bits": [ 10, 11, 12, 13 ],
+          "attributes": {
+          }
+        }
+      }
+    },
+    "full_Bfullarch": {
+      "attributes": {
+      },
+      "ports": {
+        "a": {
+          "direction": "input",
+          "bits": [ 2 ]
+        },
+        "b": {
+          "direction": "input",
+          "bits": [ 3 ]
+        },
+        "cin": {
+          "direction": "input",
+          "bits": [ 4 ]
+        },
+        "cout": {
+          "direction": "output",
+          "bits": [ 5 ]
+        },
+        "s": {
+          "direction": "output",
+          "bits": [ 6 ]
+        }
+      },
+      "cells": {
+        ":25": {
+          "hide_name": 0,
+          "type": "$or",
+          "parameters": {
+            "A_SIGNED": "00000000000000000000000000000000",
+            "A_WIDTH": "00000000000000000000000000000001",
+            "B_SIGNED": "00000000000000000000000000000000",
+            "B_WIDTH": "00000000000000000000000000000001",
+            "Y_WIDTH": "00000000000000000000000000000001"
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "A": "input",
+            "B": "input",
+            "Y": "output"
+          },
+          "connections": {
+            "A": [ 7 ],
+            "B": [ 8 ],
+            "Y": [ 5 ]
+          }
+        },
+        "half0": {
+          "hide_name": 0,
+          "type": "half_Bhalfarch",
+          "parameters": {
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "c": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 2 ],
+            "b": [ 3 ],
+            "c": [ 7 ],
+            "s": [ 9 ]
+          }
+        },
+        "half1": {
+          "hide_name": 0,
+          "type": "half_Bhalfarch",
+          "parameters": {
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "a": "input",
+            "b": "input",
+            "c": "output",
+            "s": "output"
+          },
+          "connections": {
+            "a": [ 9 ],
+            "b": [ 4 ],
+            "c": [ 8 ],
+            "s": [ 6 ]
+          }
+        }
+      },
+      "netnames": {
+        "$auto$ghdl.cc:827:import_module$10": {
+          "hide_name": 1,
+          "bits": [ 9 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$11": {
+          "hide_name": 1,
+          "bits": [ 8 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$12": {
+          "hide_name": 1,
+          "bits": [ 6 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$13": {
+          "hide_name": 1,
+          "bits": [ 5 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$9": {
+          "hide_name": 1,
+          "bits": [ 7 ],
+          "attributes": {
+          }
+        },
+        "a": {
+          "hide_name": 0,
+          "bits": [ 2 ],
+          "attributes": {
+          }
+        },
+        "b": {
+          "hide_name": 0,
+          "bits": [ 3 ],
+          "attributes": {
+          }
+        },
+        "cin": {
+          "hide_name": 0,
+          "bits": [ 4 ],
+          "attributes": {
+          }
+        },
+        "cout": {
+          "hide_name": 0,
+          "bits": [ 5 ],
+          "attributes": {
+          }
+        },
+        "half0c": {
+          "hide_name": 0,
+          "bits": [ 7 ],
+          "attributes": {
+          }
+        },
+        "half0s": {
+          "hide_name": 0,
+          "bits": [ 9 ],
+          "attributes": {
+          }
+        },
+        "half1c": {
+          "hide_name": 0,
+          "bits": [ 8 ],
+          "attributes": {
+          }
+        },
+        "s": {
+          "hide_name": 0,
+          "bits": [ 6 ],
+          "attributes": {
+          }
+        }
+      }
+    },
+    "half_Bhalfarch": {
+      "attributes": {
+      },
+      "ports": {
+        "a": {
+          "direction": "input",
+          "bits": [ 2 ]
+        },
+        "b": {
+          "direction": "input",
+          "bits": [ 3 ]
+        },
+        "c": {
+          "direction": "output",
+          "bits": [ 4 ]
+        },
+        "s": {
+          "direction": "output",
+          "bits": [ 5 ]
+        }
+      },
+      "cells": {
+        ":28": {
+          "hide_name": 0,
+          "type": "$and",
+          "parameters": {
+            "A_SIGNED": "00000000000000000000000000000000",
+            "A_WIDTH": "00000000000000000000000000000001",
+            "B_SIGNED": "00000000000000000000000000000000",
+            "B_WIDTH": "00000000000000000000000000000001",
+            "Y_WIDTH": "00000000000000000000000000000001"
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "A": "input",
+            "B": "input",
+            "Y": "output"
+          },
+          "connections": {
+            "A": [ 2 ],
+            "B": [ 3 ],
+            "Y": [ 4 ]
+          }
+        },
+        ":29": {
+          "hide_name": 0,
+          "type": "$xor",
+          "parameters": {
+            "A_SIGNED": "00000000000000000000000000000000",
+            "A_WIDTH": "00000000000000000000000000000001",
+            "B_SIGNED": "00000000000000000000000000000000",
+            "B_WIDTH": "00000000000000000000000000000001",
+            "Y_WIDTH": "00000000000000000000000000000001"
+          },
+          "attributes": {
+          },
+          "port_directions": {
+            "A": "input",
+            "B": "input",
+            "Y": "output"
+          },
+          "connections": {
+            "A": [ 2 ],
+            "B": [ 3 ],
+            "Y": [ 5 ]
+          }
+        }
+      },
+      "netnames": {
+        "$auto$ghdl.cc:827:import_module$14": {
+          "hide_name": 1,
+          "bits": [ 4 ],
+          "attributes": {
+          }
+        },
+        "$auto$ghdl.cc:827:import_module$15": {
+          "hide_name": 1,
+          "bits": [ 5 ],
+          "attributes": {
+          }
+        },
+        "a": {
+          "hide_name": 0,
+          "bits": [ 2 ],
+          "attributes": {
+          }
+        },
+        "b": {
+          "hide_name": 0,
+          "bits": [ 3 ],
+          "attributes": {
+          }
+        },
+        "c": {
+          "hide_name": 0,
+          "bits": [ 4 ],
+          "attributes": {
+          }
+        },
+        "s": {
+          "hide_name": 0,
+          "bits": [ 5 ],
+          "attributes": {
+          }
+        }
+      }
+    }
+  }
+}
\ No newline at end of file
diff --git a/intTests/test2828/test.saw b/intTests/test2828/test.saw
new file mode 100644
index 0000000000..defe0b7b45
--- /dev/null
+++ b/intTests/test2828/test.saw
@@ -0,0 +1,6 @@
+enable_experimental;
+
+adder_yosys <- yosys_import "adder_yosys.json";
+adder_tabby <- yosys_import "adder_tabby.json";
+
+prove_print z3 {{ adder_yosys.add4 === adder_tabby.add4 }};
diff --git a/intTests/test2828/test.sh b/intTests/test2828/test.sh
new file mode 100644
index 0000000000..0b864017cd
--- /dev/null
+++ b/intTests/test2828/test.sh
@@ -0,0 +1 @@
+$SAW test.saw