diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs
index 3c3305b53..e4de427c6 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Fold.hs
@@ -12,11 +12,9 @@ import           Control.Lens                                     ((^.))
 import           Data.Binary                                      (Binary)
 import           Data.Function                                    ((.))
 import           Data.Functor                                     (fmap)
-import           Data.Functor.Rep                                 (Rep, Representable)
 import           Data.Kind                                        (Type)
 import           Data.Map.Strict                                  (Map)
 import qualified Data.Map.Strict                                  as M
-import           Data.Ord                                         (Ord)
 import           Data.Proxy                                       (Proxy)
 import           GHC.Generics                                     (Generic, Par1 (..), U1 (..), type (:*:) (..),
                                                                    type (:.:) (..))
@@ -43,6 +41,7 @@ import           ZkFold.Symbolic.Data.Bool
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.FieldElement                (FieldElement)
+import           ZkFold.Symbolic.Data.Input                       (SymbolicInput)
 
 
 -- | These instances might seem off, but accumulator scheme requires this exact behaviour for ProverMessages which are Maps in this case.
@@ -118,34 +117,13 @@ ivcVerifier (i, pi_x, accTuple, acc'Tuple, pf) (a, ckTuple, dkTuple)
 ivcVerifierAc
     :: forall i f c m ctx a y t
     .  Symbolic ctx
-    => SymbolicData i
-    => SymbolicData f
-    => SymbolicData c
-    => SymbolicData m
-    => SymbolicData a
+    => SymbolicInput (i, c, (i, c, f, c, f), (i, c, f, c, f), c)
+    => SymbolicInput (a, (f, (f, f)), ((i, c, f, c, f), m))
     => SymbolicData y
-    => Context i ~ ctx
-    => Context f ~ ctx
-    => Context c ~ ctx
-    => Context m ~ ctx
     => Context a ~ ctx
+    => Context i ~ ctx
     => Context y ~ ctx
-    => Support i ~ Proxy ctx
-    => Support f ~ Proxy ctx
-    => Support c ~ Proxy ctx
-    => Support m ~ Proxy ctx
-    => Support a ~ Proxy ctx
     => Support y ~ Proxy ctx
-    => Representable (Layout i)
-    => Representable (Layout c)
-    => Representable (Layout f)
-    => Representable (Layout a)
-    => Representable (Layout m)
-    => Ord (Rep (Layout i))
-    => Ord (Rep (Layout c))
-    => Ord (Rep (Layout f))
-    => Ord (Rep (Layout a))
-    => Ord (Rep (Layout m))
     => Layout y ~ Par1
     => t ~ ((i,c,(i,c,f,c,f),(i,c,f,c,f),c),(a,(f,f,f),(i,c,f,c,f),m),Proxy ctx)
     => ctx ~ ArithmeticCircuit a (Layout t)
diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler.hs
index f82e41c12..4496dbb0f 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Compiler.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Compiler.hs
@@ -16,16 +16,19 @@ import           Data.Function                              (const, (.))
 import           Data.Functor                               (($>))
 import           Data.Functor.Rep                           (Rep, Representable)
 import           Data.Ord                                   (Ord)
-import           Data.Proxy                                 (Proxy)
+import           Data.Proxy                                 (Proxy (..))
 import           Data.Traversable                           (for)
+import           GHC.Generics                               (Par1 (Par1))
 import           Prelude                                    (FilePath, IO, Monoid (mempty), Show (..), Traversable,
-                                                             putStrLn, type (~), ($), (++))
+                                                             putStrLn, return, type (~), ($), (++))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Prelude                             (writeFileJSON)
-import           ZkFold.Symbolic.Class                      (Arithmetic, Symbolic (..))
+import           ZkFold.Symbolic.Class                      (Arithmetic, Symbolic (..), fromCircuit2F)
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit
+import           ZkFold.Symbolic.Data.Bool                  (Bool (Bool))
 import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Input
 import           ZkFold.Symbolic.MonadCircuit               (MonadCircuit (..))
 
 {-
@@ -43,21 +46,21 @@ forceOne r = fromCircuitF r (\fi -> for fi $ \i -> constraint (\x -> x i - one)
 
 -- | Arithmetizes an argument by feeding an appropriate amount of inputs.
 solder ::
-    forall a c f s l .
-    ( c ~ ArithmeticCircuit a l
+    forall a c f s .
+    ( c ~ ArithmeticCircuit a (Layout s)
     , SymbolicData f
     , Context f ~ c
     , Support f ~ s
-    , SymbolicData s
+    , SymbolicInput s
     , Context s ~ c
-    , Support s ~ Proxy c
-    , Layout s ~ l
-    , Representable l
-    , Ord (Rep l)
+    , Symbolic c
     ) => f -> c (Layout f)
-solder f = pieces f (restore @(Support f) $ const inputC)
-    where
-        inputC = mempty { acOutput = acInput }
+solder f = fromCircuit2F (pieces f input) b $ \r (Par1 i) -> do
+    constraint (\x -> one - x i)
+    return r
+  where
+    Bool b = isValid input
+    input = restore @(Support f) $ const mempty { acOutput = acInput }
 
 -- | Compiles function `f` into an arithmetic circuit with all outputs equal to 1.
 compileForceOne ::
@@ -68,9 +71,8 @@ compileForceOne ::
     , SymbolicData f
     , Context f ~ c
     , Support f ~ s
-    , SymbolicData s
+    , SymbolicInput s
     , Context s ~ c
-    , Support s ~ Proxy c
     , Layout s ~ l
     , Representable l
     , Binary (Rep l)
@@ -90,16 +92,14 @@ compile ::
     , SymbolicData f
     , Context f ~ c
     , Support f ~ s
-    , SymbolicData s
+    , SymbolicInput s
     , Context s ~ c
-    , Support s ~ Proxy c
     , Layout s ~ l
-    , Representable l
-    , Ord (Rep l)
     , SymbolicData y
     , Context y ~ c
     , Support y ~ Proxy c
     , Layout f ~ Layout y
+    , Symbolic c
     ) => f -> y
 compile = restore . const . optimize . solder @a
 
@@ -113,14 +113,12 @@ compileIO ::
     , Context f ~ c
     , Support f ~ s
     , ToJSON (Layout f (Var a l))
-    , SymbolicData s
+    , SymbolicInput s
     , Context s ~ c
-    , Support s ~ Proxy c
     , Layout s ~ l
-    , Representable l
-    , Ord (Rep l)
     , FromJSON (Rep l)
     , ToJSON (Rep l)
+    , Symbolic c
     ) => FilePath -> f -> IO ()
 compileIO scriptFile f = do
     let ac = optimize (solder @a f) :: c (Layout f)
diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs
index 4d89d09ee..55386f500 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Compiler/ArithmeticCircuit/Internal.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes  #-}
 {-# LANGUAGE DeriveAnyClass       #-}
 {-# LANGUAGE DerivingVia          #-}
 {-# LANGUAGE NoStarIsType         #-}
@@ -129,6 +130,7 @@ imapVar _ (ConstVar c) = ConstVar c
 acInput :: Representable i => i (Var a i)
 acInput = fmapRep (SysVar . InVar) (tabulate id)
 
+
 getAllVars :: forall a i o. (Representable i, Foldable i) => ArithmeticCircuit a i o -> [SysVar i]
 getAllVars ac = toList acInput0 ++ map NewVar (keys $ acWitness ac) where
   acInput0 :: i (SysVar i)
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
index 16e8538d7..17a24b360 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
@@ -26,6 +26,7 @@ import           Control.Monad                      (replicateM)
 import           Data.Aeson                         (FromJSON (..), ToJSON (..))
 import qualified Data.Bits                          as B
 import qualified Data.ByteString                    as Bytes
+import           Data.Foldable                      (foldlM)
 import           Data.Kind                          (Type)
 import           Data.List                          (reverse, unfoldr)
 import           Data.Maybe                         (Maybe (..))
@@ -34,8 +35,8 @@ import           Data.Traversable                   (for)
 import           GHC.Generics                       (Generic, Par1 (..))
 import           GHC.Natural                        (naturalFromInteger)
 import           Numeric                            (readHex, showHex)
-import           Prelude                            (Integer, drop, fmap, otherwise, pure, return, take, type (~), ($),
-                                                     (.), (<$>), (<), (<>), (==), (>=))
+import           Prelude                            (Integer, const, drop, fmap, otherwise, pure, return, take,
+                                                     type (~), ($), (.), (<$>), (<), (<>), (==), (>=))
 import qualified Prelude                            as Haskell
 import           Test.QuickCheck                    (Arbitrary (..), chooseInteger)
 
@@ -55,6 +56,7 @@ import           ZkFold.Symbolic.Data.Combinators
 import           ZkFold.Symbolic.Data.Eq            (Eq)
 import           ZkFold.Symbolic.Data.Eq.Structural
 import           ZkFold.Symbolic.Data.FieldElement  (FieldElement)
+import           ZkFold.Symbolic.Data.Input         (SymbolicInput, isValid)
 import           ZkFold.Symbolic.Interpreter        (Interpreter (..))
 import           ZkFold.Symbolic.MonadCircuit       (ClosedPoly, MonadCircuit, newAssigned)
 
@@ -265,6 +267,25 @@ instance
 
         zeroA = Haskell.replicate diff (fromConstant (0 :: Integer ))
 
+instance
+  ( Symbolic c
+  , KnownNat n
+  ) => SymbolicInput (ByteString n c) where
+  isValid (ByteString bits) = Bool $ fromCircuitF bits solve
+    where
+        solve :: MonadCircuit i (BaseField c) m => Vector n i -> m (Par1 i)
+        solve v = do
+            let vs = V.fromVector v
+            ys <- for vs $ \i -> newAssigned (\p -> p i * (one - p i))
+            us <-for ys $ \i -> isZero $ Par1 i
+            helper us
+
+        helper :: MonadCircuit i a m => [Par1 i] -> m (Par1 i)
+        helper xs = case xs of
+            []       -> Par1 <$> newAssigned (const one)
+            (b : bs) -> foldlM (\(Par1 v1) (Par1 v2) -> Par1 <$> newAssigned (($ v1) * ($ v2))) b bs
+
+
 isSet :: forall c n. Symbolic c => ByteString n c -> Natural -> Bool c
 isSet (ByteString bits) ix = Bool $ fromCircuitF bits solve
     where
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs
index 99c91135e..af364351c 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Combinators.hs
@@ -246,3 +246,6 @@ runInvert is = do
     js <- for is $ \i -> newConstrained (\x j -> x i * x j) (\x -> let xi = x i in one - xi // xi)
     ks <- for (mzipRep is js) $ \(i, j) -> newConstrained (\x k -> x i * x k + x j - one) (finv . ($ i))
     return (js, ks)
+
+isZero :: (MonadCircuit i a m, Representable f, Traversable f) => f i -> m (f i)
+isZero is = Haskell.fst <$> runInvert is
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs b/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs
index c0d6d653a..3f49dc958 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs
@@ -25,10 +25,11 @@ import           ZkFold.Base.Data.Utils           (zipWithM)
 import           ZkFold.Base.Data.Vector
 import           ZkFold.Prelude                   (iterateM, length)
 import           ZkFold.Symbolic.Class
-import           ZkFold.Symbolic.Data.Bool        (Bool)
+import           ZkFold.Symbolic.Data.Bool        (Bool, BoolType (..))
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators (expansionW, log2, maxBitsPerFieldElement, splitExpansion)
 import           ZkFold.Symbolic.Data.Eq
+import           ZkFold.Symbolic.Data.Input
 import           ZkFold.Symbolic.Data.Ord         (blueprintGE)
 import           ZkFold.Symbolic.Interpreter
 import           ZkFold.Symbolic.MonadCircuit     (MonadCircuit, newAssigned)
@@ -212,3 +213,7 @@ instance Finite (Zp p) => Finite (FFA p b) where
 
 -- FIXME: This Eq instance is wrong
 deriving newtype instance Symbolic c => Eq (Bool c) (FFA p c)
+
+-- | TODO: fix when rewrite is done
+instance (Symbolic c) => SymbolicInput (FFA p c) where
+  isValid _ = true
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
index 693b00571..2676c0451 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
@@ -19,10 +19,11 @@ import           ZkFold.Base.Data.HFunctor        (hmap)
 import           ZkFold.Base.Data.Par1            ()
 import           ZkFold.Base.Data.Vector          (Vector, fromVector, unsafeToVector)
 import           ZkFold.Symbolic.Class
-import           ZkFold.Symbolic.Data.Bool        (Bool)
+import           ZkFold.Symbolic.Data.Bool        (Bool, BoolType (true))
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators (expansion, horner, runInvert)
 import           ZkFold.Symbolic.Data.Eq          (Eq)
+import           ZkFold.Symbolic.Data.Input
 import           ZkFold.Symbolic.Data.Ord
 import           ZkFold.Symbolic.MonadCircuit     (newAssigned)
 
@@ -105,3 +106,6 @@ instance Symbolic c => BinaryExpansion (FieldElement c) where
   fromBinary bits =
     FieldElement $ symbolicF bits (Par1 . foldr (\x y -> x + y + y) zero)
       $ fmap Par1 . horner . fromVector
+
+instance (Symbolic c) => SymbolicInput (FieldElement c) where
+  isValid _ = true
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Input.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Input.hs
new file mode 100644
index 000000000..13fe161d3
--- /dev/null
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Input.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module ZkFold.Symbolic.Data.Input (
+    SymbolicInput (..)
+) where
+
+import           Control.Monad.Representable.Reader (Rep)
+import           Data.Functor.Rep                   (Representable)
+import           Data.Ord                           (Ord)
+import           Data.Type.Equality                 (type (~))
+import           Data.Typeable                      (Proxy (..))
+import           GHC.Generics                       (Par1 (..))
+import           GHC.TypeLits                       (KnownNat)
+import           Prelude                            (foldl, ($))
+
+import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Data.ByteString        (Binary)
+import           ZkFold.Base.Data.Vector            (Vector, fromVector)
+import           ZkFold.Symbolic.Class
+import           ZkFold.Symbolic.Data.Bool
+import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Combinators
+import           ZkFold.Symbolic.MonadCircuit
+
+
+-- | A class for Symbolic input.
+class
+    ( SymbolicData d
+    , Support d ~ Proxy (Context d)
+    , Representable (Layout d)
+    , Binary (Rep (Layout d))
+    , Ord (Rep (Layout d))
+    ) => SymbolicInput d where
+    isValid :: d -> Bool (Context d)
+
+
+instance Symbolic c => SymbolicInput (Bool c) where
+  isValid (Bool b) = Bool $ fromCircuitF b $
+      \(Par1 v) -> do
+        u <- newAssigned (\x -> x v * (one - x v))
+        isZero $ Par1 u
+
+
+instance
+  ( Symbolic c
+  , Binary (Rep f)
+  , Ord (Rep f)
+  , Representable f) => SymbolicInput (c f) where
+  isValid _ = true
+
+
+instance Symbolic c => SymbolicInput (Proxy c) where
+  isValid _ = true
+
+instance (
+    Symbolic (Context x)
+    , Context x ~ Context y
+    , SymbolicInput x
+    , SymbolicInput y
+    ) => SymbolicInput (x, y) where
+  isValid (l, r) = isValid l && isValid r
+
+instance (
+    Symbolic (Context x)
+    , Context x ~ Context y
+    , Context y ~ Context z
+    , SymbolicInput x
+    , SymbolicInput y
+    , SymbolicInput z
+    ) => SymbolicInput (x, y, z) where
+  isValid (l, m, r) = isValid l && isValid m && isValid r
+
+instance (
+  Symbolic (Context x)
+  , KnownNat n
+  , SymbolicInput x
+  ) => SymbolicInput (Vector n x) where
+  isValid v = foldl (\l r -> l && isValid r) true $ fromVector v
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
index 7ecb9ade3..991e43169 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
@@ -17,8 +17,8 @@ module ZkFold.Symbolic.Data.UInt (
 
 import           Control.DeepSeq
 import           Control.Monad.State                (StateT (..))
-import           Data.Aeson
-import           Data.Foldable                      (foldr, foldrM, for_)
+import           Data.Aeson                         hiding (Bool)
+import           Data.Foldable                      (foldlM, foldr, foldrM, for_)
 import           Data.Functor                       ((<$>))
 import           Data.Kind                          (Type)
 import           Data.List                          (unfoldr, zip)
@@ -28,8 +28,8 @@ import           Data.Tuple                         (swap)
 import qualified Data.Zip                           as Z
 import           GHC.Generics                       (Generic, Par1 (..))
 import           GHC.Natural                        (naturalFromInteger)
-import           Prelude                            (Integer, error, flip, otherwise, return, type (~), ($), (++), (.),
-                                                     (<>), (>>=))
+import           Prelude                            (Integer, const, error, flip, otherwise, return, type (~), ($),
+                                                     (++), (.), (<>), (>>=))
 import qualified Prelude                            as Haskell
 import           Test.QuickCheck                    (Arbitrary (..), chooseInteger)
 
@@ -48,6 +48,7 @@ import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Eq.Structural
 import           ZkFold.Symbolic.Data.FieldElement  (FieldElement)
+import           ZkFold.Symbolic.Data.Input         (SymbolicInput, isValid)
 import           ZkFold.Symbolic.Data.Ord
 import           ZkFold.Symbolic.Interpreter        (Interpreter (..))
 import           ZkFold.Symbolic.MonadCircuit       (MonadCircuit, constraint, newAssigned)
@@ -520,6 +521,29 @@ instance (Symbolic c, KnownNat n, KnownRegisterSize r) => StrictNum (UInt n r c)
                 return (p : ps <> [p'])
 
 
+instance
+  ( Symbolic c
+  , KnownNat n
+  , KnownRegisterSize r
+  , KnownNat (NumberOfRegisters (BaseField c) n r)
+  ) => SymbolicInput (UInt n r c) where
+  isValid (UInt bits) = Bool $ fromCircuitF bits solve
+    where
+        solve :: MonadCircuit i (BaseField c) m => Vector (NumberOfRegisters (BaseField c) n r) i -> m (Par1 i)
+        solve v = do
+            let vs = V.fromVector v
+            bs <- toBits (Haskell.reverse vs) (highRegisterSize @(BaseField c) @n @r) (registerSize @(BaseField c) @n @r)
+            ys <- Haskell.reverse <$> fromBits (highRegisterSize @(BaseField c) @n @r) (registerSize @(BaseField c) @n @r) bs
+            difference <- for (zip vs ys) $ \(i, j) -> newAssigned (\w -> w i - w j)
+            isZeros <- for difference $ isZero . Par1
+            helper isZeros
+
+        helper :: MonadCircuit i a m => [Par1 i] -> m (Par1 i)
+        helper xs = case xs of
+            []       -> Par1 <$> newAssigned (const one)
+            (b : bs) -> foldlM (\(Par1 v1) (Par1 v2) -> Par1 <$> newAssigned (($ v1) * ($ v2))) b bs
+
+
 --------------------------------------------------------------------------------
 
 fullAdder :: (Arithmetic a, MonadCircuit i a m) => Natural -> i -> i -> i -> m (i, i)
diff --git a/symbolic-base/symbolic-base.cabal b/symbolic-base/symbolic-base.cabal
index 228efe8a0..ccaffc30d 100644
--- a/symbolic-base/symbolic-base.cabal
+++ b/symbolic-base/symbolic-base.cabal
@@ -185,6 +185,7 @@ library
       ZkFold.Symbolic.Data.Eq
       ZkFold.Symbolic.Data.Eq.Structural
       ZkFold.Symbolic.Data.FFA
+      ZkFold.Symbolic.Data.Input
       ZkFold.Symbolic.Data.List
       ZkFold.Symbolic.Data.Maybe
       ZkFold.Symbolic.Data.Ord
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/BatchTransfer.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/BatchTransfer.hs
index 3a068a533..ee5cb80ae 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/BatchTransfer.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/BatchTransfer.hs
@@ -18,6 +18,7 @@ import           ZkFold.Symbolic.Data.Class           (SymbolicData (..))
 import           ZkFold.Symbolic.Data.Combinators
 import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.FieldElement    (fromFieldElement)
+import           ZkFold.Symbolic.Data.Input           (SymbolicInput)
 import           ZkFold.Symbolic.Data.UInt            (StrictConv (..))
 
 type Tokens = 10
@@ -42,7 +43,7 @@ verifySignature pub (pay, change) sig = (from sig * base) == (strictConv (fromFi
 batchTransfer ::
     forall context.
     ( Symbolic context
-    , SymbolicData (TxOut context)
+    , SymbolicInput (TxOut context)
     , KnownNat (NumberOfRegisters (BaseField context) 256 'Auto)
     , KnownNat (NumberOfRegisters (BaseField context) 64 'Auto)
     ) => Tx context -> Vector 5 (TxOut context, TxOut context, ByteString 256 context)-> Bool context
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
index a4a7e7bf7..92ec53745 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
@@ -12,12 +12,13 @@ import           ZkFold.Symbolic.Class               (Symbolic)
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Eq             (Eq)
 import           ZkFold.Symbolic.Data.Eq.Structural
+import           ZkFold.Symbolic.Data.Input
 
 type AddressType context = ByteString 4 context
 type PaymentCredential context = ByteString 224 context
 type StakingCredential context = ByteString 224 context
 
-data  Address context = Address {
+data Address context = Address {
         addressType       :: AddressType context,
         paymentCredential :: PaymentCredential context,
         stakingCredential :: StakingCredential context
@@ -36,3 +37,6 @@ instance HApplicative context => SymbolicData (Address context) where
   type Layout (Address context) = Layout (AddressType context, PaymentCredential context, StakingCredential context)
   pieces (Address a b c) = pieces (a, b, c)
   restore f = let (a, b, c) = restore f in Address a b c
+
+instance (Symbolic context) => SymbolicInput (Address context)  where
+    isValid (Address a p s) = isValid (a, p, s)
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs
index 3f5e13025..5194804b1 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs
@@ -14,6 +14,8 @@ import           ZkFold.Symbolic.Cardano.Types.OutputRef (OutputRef)
 import           ZkFold.Symbolic.Cardano.Types.Value     (Value)
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Combinators        (NumberOfRegisters, RegisterSize (..))
+import           ZkFold.Symbolic.Data.Input              (SymbolicInput, isValid)
 
 data Input tokens datum context = Input  {
         txiOutputRef :: OutputRef context,
@@ -33,6 +35,14 @@ instance (Symbolic context, KnownNat tokens) => SymbolicData (Input tokens datum
   pieces (Input a b) = pieces (a, b)
   restore f = let (a, b) = restore f in Input a b
 
+instance
+  ( Symbolic context
+  , KnownNat tokens
+  , KnownNat (NumberOfRegisters (BaseField context) 32 Auto)
+  , KnownNat (NumberOfRegisters (BaseField context) 64 Auto)
+  ) => SymbolicInput (Input tokens datum context) where
+  isValid (Input ior io) = isValid (ior, io)
+
 txiAddress :: Input tokens datum context -> Address context
 txiAddress (Input _ txo) = txoAddress txo
 
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
index df79b1d10..d1778aab5 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
@@ -20,6 +20,7 @@ import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators           (NumberOfRegisters, RegisterSize (..))
 import           ZkFold.Symbolic.Data.Eq                    (Eq)
 import           ZkFold.Symbolic.Data.Eq.Structural
+import           ZkFold.Symbolic.Data.Input                 (SymbolicInput (..))
 
 data Output tokens datum context = Output {
         txoAddress   :: Address context,
@@ -45,6 +46,13 @@ instance
   pieces (Output a b c) = pieces (a, b, c)
   restore f = let (a, b, c) = restore f in Output a b c
 
+instance
+    ( Symbolic context
+    , KnownNat tokens
+    , KnownNat (NumberOfRegisters (BaseField context) 64 Auto)
+    ) => SymbolicInput (Output tokens datum context) where
+    isValid (Output a t d) = isValid (a, t, d)
+
 deriving via (Structural (Output tokens datum context))
          instance
             ( Symbolic context
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
index e75177db5..7cfaf7f19 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
@@ -1,15 +1,19 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -freduction-depth=0 #-} -- Avoid reduction overflow error caused by NumberOfRegisters
+{-# LANGUAGE AllowAmbiguousTypes  #-}
 
 module ZkFold.Symbolic.Cardano.Types.OutputRef where
 
+import           GHC.TypeNats                        (KnownNat)
 import           Prelude                             hiding (Bool, Eq, length, splitAt, (*), (+))
 import qualified Prelude                             as Haskell
 
 import           ZkFold.Base.Control.HApplicative    (HApplicative)
 import           ZkFold.Symbolic.Cardano.Types.Basic
+import           ZkFold.Symbolic.Class               (Symbolic (..))
 import           ZkFold.Symbolic.Data.Class
-import           ZkFold.Symbolic.Data.Combinators    (RegisterSize (..))
+import           ZkFold.Symbolic.Data.Combinators    (NumberOfRegisters, RegisterSize (..))
+import           ZkFold.Symbolic.Data.Input          (SymbolicInput, isValid)
 
 type TxRefId context = ByteString 256 context
 type TxRefIndex context = UInt 32 Auto context
@@ -31,3 +35,10 @@ instance HApplicative context => SymbolicData (OutputRef context) where
 
   pieces (OutputRef a b) = pieces (a, b)
   restore f = let (a, b) = restore f in OutputRef a b
+
+instance
+    ( HApplicative context
+    , Symbolic context
+    , KnownNat (NumberOfRegisters (BaseField context) 32 Auto)
+    ) => SymbolicInput (OutputRef context) where
+    isValid (OutputRef orId orInd) = isValid (orId, orInd)
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Transaction.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Transaction.hs
index eda4986a1..61a01283b 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Transaction.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Transaction.hs
@@ -11,8 +11,10 @@ import           ZkFold.Symbolic.Cardano.Types.Basic
 import           ZkFold.Symbolic.Cardano.Types.Input  (Input)
 import           ZkFold.Symbolic.Cardano.Types.Output (Output)
 import           ZkFold.Symbolic.Cardano.Types.Value  (Value)
-import           ZkFold.Symbolic.Class                (Symbolic)
+import           ZkFold.Symbolic.Class                (BaseField, Symbolic)
 import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Combinators
+import           ZkFold.Symbolic.Data.Input           (SymbolicInput, isValid)
 
 data Transaction inputs rinputs outputs tokens mint datum context = Transaction {
         txRefInputs :: Vector rinputs (Input tokens datum context),
@@ -46,3 +48,16 @@ instance
   pieces (Transaction a b c d e) = pieces (a, b, c, d, e)
   restore f = let (a, b, c, d, e) = restore f in Transaction a b c d e
 
+
+instance
+    ( Symbolic context
+    , KnownNat (NumberOfRegisters (BaseField context) 32 Auto)
+    , KnownNat (NumberOfRegisters (BaseField context) 64 Auto)
+    , KnownNat (NumberOfRegisters (BaseField context) 11 Auto)
+    , KnownNat tokens
+    , KnownNat rinputs
+    , KnownNat outputs
+    , KnownNat mint
+    , KnownNat inputs
+    ) => SymbolicInput (Transaction inputs rinputs outputs tokens mint datum context) where
+  isValid (Transaction _ txI _ _ _) = isValid txI
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
index 3428f328d..048b2b355 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -freduction-depth=0 #-} -- Avoid reduction overflow error caused by NumberOfRegisters
+{-# OPTIONS_GHC -Wno-orphans #-}
 
 module ZkFold.Symbolic.Cardano.Types.Value where
 
@@ -12,9 +13,10 @@ import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number    (KnownNat)
 import           ZkFold.Base.Data.Vector
 import           ZkFold.Symbolic.Cardano.Types.Basic
-import           ZkFold.Symbolic.Class               (Symbolic)
+import           ZkFold.Symbolic.Class               (Symbolic (..))
 import           ZkFold.Symbolic.Data.Class
-import           ZkFold.Symbolic.Data.Combinators    (RegisterSize (..))
+import           ZkFold.Symbolic.Data.Combinators    (NumberOfRegisters, RegisterSize (..))
+import           ZkFold.Symbolic.Data.Input
 
 type PolicyId context    = ByteString 224 context
 type AssetName context   = ByteString 256 context
@@ -30,7 +32,15 @@ deriving instance (Haskell.Ord (ByteString 224 context), Haskell.Ord (ByteString
 
 deriving instance (Symbolic context, KnownNat n) => SymbolicData (Value n context)
 
+instance
+    ( Symbolic context
+    , KnownNat n
+    , KnownNat (NumberOfRegisters (BaseField context) 64 Auto)
+    ) => SymbolicInput (Value n context) where
+    isValid (Value v) = isValid v
+
 instance Symbolic context => Scale Natural (Value n context) where
+    scale :: Natural -> Value n context -> Value n context
     n `scale` Value v = Value $ fmap (\((pid, aname), q) -> ((pid, aname), n `scale` q)) v
 
 instance (Haskell.Ord (PolicyId context), Haskell.Ord (AssetName context), Symbolic context) => Semigroup (Value n context) where
diff --git a/symbolic-examples/src/Examples/BatchTransfer.hs b/symbolic-examples/src/Examples/BatchTransfer.hs
index 4b22c5d7f..04a964a83 100644
--- a/symbolic-examples/src/Examples/BatchTransfer.hs
+++ b/symbolic-examples/src/Examples/BatchTransfer.hs
@@ -6,12 +6,12 @@ import           ZkFold.Base.Data.Vector                         (Vector)
 import           ZkFold.Symbolic.Cardano.Contracts.BatchTransfer (Tx, TxOut, batchTransfer)
 import           ZkFold.Symbolic.Cardano.Types                   (Bool, ByteString)
 import           ZkFold.Symbolic.Class                           (Symbolic (..))
-import           ZkFold.Symbolic.Data.Class                      (SymbolicData (..))
 import           ZkFold.Symbolic.Data.Combinators                (NumberOfRegisters, RegisterSize (..))
+import           ZkFold.Symbolic.Data.Input                      (SymbolicInput)
 
 exampleBatchTransfer ::
     ( Symbolic c
-    , SymbolicData (TxOut c)
+    , SymbolicInput (TxOut c)
     , KnownNat (NumberOfRegisters (BaseField c) 64 'Auto)
     , KnownNat (NumberOfRegisters (BaseField c) 256 'Auto)
     )  => Tx c -> Vector 5 (TxOut c, TxOut c, ByteString 256 c) -> Bool c
diff --git a/symbolic-examples/src/ZkFold/Symbolic/Examples.hs b/symbolic-examples/src/ZkFold/Symbolic/Examples.hs
index 2f46b4a47..dcc84686f 100644
--- a/symbolic-examples/src/ZkFold/Symbolic/Examples.hs
+++ b/symbolic-examples/src/ZkFold/Symbolic/Examples.hs
@@ -31,6 +31,7 @@ import           ZkFold.Symbolic.Compiler.ArithmeticCircuit  (Var)
 import           ZkFold.Symbolic.Data.ByteString             (ByteString)
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators            (RegisterSize (Auto))
+import           ZkFold.Symbolic.Data.Input                  (SymbolicInput)
 
 type A = Zp BLS12_381_Scalar
 type C = ArithmeticCircuit A
@@ -46,7 +47,7 @@ exampleOutput ::
   , c ~ C i
   , Context f ~ c
   , Layout f ~ o
-  , SymbolicData (Support f)
+  , SymbolicInput (Support f)
   , Context (Support f) ~ c
   , Support (Support f) ~ Proxy c
   , Layout (Support f) ~ i
diff --git a/symbolic-examples/stats/ByteString.Add.512 b/symbolic-examples/stats/ByteString.Add.512
index f82c2c846..d6b536818 100644
--- a/symbolic-examples/stats/ByteString.Add.512
+++ b/symbolic-examples/stats/ByteString.Add.512
@@ -1,4 +1,4 @@
 ByteString.Add.512
-Number of constraints: 1542
-Number of variables: 2054
+Number of constraints: 5639
+Number of variables: 6150
 Number of range lookups: 522
\ No newline at end of file
diff --git a/symbolic-examples/stats/ByteString.And.32 b/symbolic-examples/stats/ByteString.And.32
index 45afda713..a13b27958 100644
--- a/symbolic-examples/stats/ByteString.And.32
+++ b/symbolic-examples/stats/ByteString.And.32
@@ -1,4 +1,4 @@
 ByteString.And.32
-Number of constraints: 32
-Number of variables: 32
+Number of constraints: 289
+Number of variables: 288
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/ByteString.Extend.1.512 b/symbolic-examples/stats/ByteString.Extend.1.512
index 8c14b1084..48a10bae1 100644
--- a/symbolic-examples/stats/ByteString.Extend.1.512
+++ b/symbolic-examples/stats/ByteString.Extend.1.512
@@ -1,4 +1,4 @@
 ByteString.Extend.1.512
-Number of constraints: 1
-Number of variables: 1
+Number of constraints: 6
+Number of variables: 5
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/ByteString.Or.64 b/symbolic-examples/stats/ByteString.Or.64
index 608620be1..5d36861e2 100644
--- a/symbolic-examples/stats/ByteString.Or.64
+++ b/symbolic-examples/stats/ByteString.Or.64
@@ -1,4 +1,4 @@
 ByteString.Or.64
-Number of constraints: 64
-Number of variables: 64
+Number of constraints: 577
+Number of variables: 576
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/Conditional b/symbolic-examples/stats/Conditional
index 956172591..96834bd57 100644
--- a/symbolic-examples/stats/Conditional
+++ b/symbolic-examples/stats/Conditional
@@ -1,4 +1,4 @@
 Conditional
-Number of constraints: 3
-Number of variables: 3
+Number of constraints: 10
+Number of variables: 9
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/Constant.5 b/symbolic-examples/stats/Constant.5
index 1d59a3f61..9769303f8 100644
--- a/symbolic-examples/stats/Constant.5
+++ b/symbolic-examples/stats/Constant.5
@@ -1,4 +1,4 @@
 Constant.5
-Number of constraints: 0
+Number of constraints: 1
 Number of variables: 0
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/Eq b/symbolic-examples/stats/Eq
index 73b62a0f1..c5bd64465 100644
--- a/symbolic-examples/stats/Eq
+++ b/symbolic-examples/stats/Eq
@@ -1,4 +1,4 @@
 Eq
-Number of constraints: 4
-Number of variables: 4
+Number of constraints: 7
+Number of variables: 6
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/Eq.Constant.5 b/symbolic-examples/stats/Eq.Constant.5
index 6b977fb9e..7b4f1456e 100644
--- a/symbolic-examples/stats/Eq.Constant.5
+++ b/symbolic-examples/stats/Eq.Constant.5
@@ -1,4 +1,4 @@
 Eq.Constant.5
-Number of constraints: 4
-Number of variables: 4
+Number of constraints: 6
+Number of variables: 5
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/FFA.Add.097 b/symbolic-examples/stats/FFA.Add.097
index 907bed990..e2e7cb3f8 100644
--- a/symbolic-examples/stats/FFA.Add.097
+++ b/symbolic-examples/stats/FFA.Add.097
@@ -1,4 +1,4 @@
 FFA.Add.097
-Number of constraints: 18870
-Number of variables: 23897
+Number of constraints: 18873
+Number of variables: 23899
 Number of range lookups: 11916
\ No newline at end of file
diff --git a/symbolic-examples/stats/FFA.Add.337 b/symbolic-examples/stats/FFA.Add.337
index 966776bfa..f3e0ede8e 100644
--- a/symbolic-examples/stats/FFA.Add.337
+++ b/symbolic-examples/stats/FFA.Add.337
@@ -1,4 +1,4 @@
 FFA.Add.337
-Number of constraints: 18870
-Number of variables: 23897
+Number of constraints: 18873
+Number of variables: 23899
 Number of range lookups: 11916
\ No newline at end of file
diff --git a/symbolic-examples/stats/FFA.Mul.097 b/symbolic-examples/stats/FFA.Mul.097
index 1121e6117..23a4e07c8 100644
--- a/symbolic-examples/stats/FFA.Mul.097
+++ b/symbolic-examples/stats/FFA.Mul.097
@@ -1,4 +1,4 @@
 FFA.Mul.097
-Number of constraints: 18898
-Number of variables: 23939
+Number of constraints: 18901
+Number of variables: 23941
 Number of range lookups: 11944
\ No newline at end of file
diff --git a/symbolic-examples/stats/FFA.Mul.337 b/symbolic-examples/stats/FFA.Mul.337
index ea534504b..9bd1094bd 100644
--- a/symbolic-examples/stats/FFA.Mul.337
+++ b/symbolic-examples/stats/FFA.Mul.337
@@ -1,4 +1,4 @@
 FFA.Mul.337
-Number of constraints: 18898
-Number of variables: 23939
+Number of constraints: 18901
+Number of variables: 23941
 Number of range lookups: 11944
\ No newline at end of file
diff --git a/symbolic-examples/stats/Fibonacci.100 b/symbolic-examples/stats/Fibonacci.100
index 42dc6e566..abda4d00a 100644
--- a/symbolic-examples/stats/Fibonacci.100
+++ b/symbolic-examples/stats/Fibonacci.100
@@ -1,4 +1,4 @@
 Fibonacci.100
-Number of constraints: 794
-Number of variables: 794
+Number of constraints: 796
+Number of variables: 795
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/LEQ b/symbolic-examples/stats/LEQ
index ab21b6311..86103665c 100644
--- a/symbolic-examples/stats/LEQ
+++ b/symbolic-examples/stats/LEQ
@@ -1,4 +1,4 @@
 LEQ
-Number of constraints: 3062
-Number of variables: 4080
+Number of constraints: 3065
+Number of variables: 4082
 Number of range lookups: 2040
\ No newline at end of file
diff --git a/symbolic-examples/stats/MiMCHash b/symbolic-examples/stats/MiMCHash
index 6a7770d49..b231f1413 100644
--- a/symbolic-examples/stats/MiMCHash
+++ b/symbolic-examples/stats/MiMCHash
@@ -1,4 +1,4 @@
 MiMCHash
-Number of constraints: 1760
-Number of variables: 1760
+Number of constraints: 1763
+Number of variables: 1762
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/Reverse.32.3000 b/symbolic-examples/stats/Reverse.32.3000
index 02abc4c3a..ba86e7361 100644
--- a/symbolic-examples/stats/Reverse.32.3000
+++ b/symbolic-examples/stats/Reverse.32.3000
@@ -1,4 +1,4 @@
 Reverse.32.3000
-Number of constraints: 0
-Number of variables: 0
+Number of constraints: 384002
+Number of variables: 384001
 Number of range lookups: 0
\ No newline at end of file
diff --git a/symbolic-examples/stats/SHA256.32 b/symbolic-examples/stats/SHA256.32
index b03845b66..6ebee3157 100644
--- a/symbolic-examples/stats/SHA256.32
+++ b/symbolic-examples/stats/SHA256.32
@@ -1,4 +1,4 @@
 SHA256.32
-Number of constraints: 53632
-Number of variables: 63890
+Number of constraints: 53761
+Number of variables: 64018
 Number of range lookups: 11156
\ No newline at end of file
diff --git a/symbolic-examples/stats/UInt.DivMod.32.Auto b/symbolic-examples/stats/UInt.DivMod.32.Auto
index 41abfa752..ae632d648 100644
--- a/symbolic-examples/stats/UInt.DivMod.32.Auto
+++ b/symbolic-examples/stats/UInt.DivMod.32.Auto
@@ -1,4 +1,4 @@
 UInt.DivMod.32.Auto
-Number of constraints: 11979
-Number of variables: 15209
+Number of constraints: 11988
+Number of variables: 15217
 Number of range lookups: 7488
\ No newline at end of file
diff --git a/symbolic-examples/stats/UInt.Mul.64.Auto b/symbolic-examples/stats/UInt.Mul.64.Auto
index 2281bc5a3..2e29021cf 100644
--- a/symbolic-examples/stats/UInt.Mul.64.Auto
+++ b/symbolic-examples/stats/UInt.Mul.64.Auto
@@ -1,4 +1,4 @@
 UInt.Mul.64.Auto
-Number of constraints: 2
-Number of variables: 3
-Number of range lookups: 2
\ No newline at end of file
+Number of constraints: 139
+Number of variables: 265
+Number of range lookups: 130
\ No newline at end of file
diff --git a/symbolic-examples/stats/UInt.StrictAdd.256.Auto b/symbolic-examples/stats/UInt.StrictAdd.256.Auto
index 62ae8edb2..885d14cb3 100644
--- a/symbolic-examples/stats/UInt.StrictAdd.256.Auto
+++ b/symbolic-examples/stats/UInt.StrictAdd.256.Auto
@@ -1,4 +1,4 @@
 UInt.StrictAdd.256.Auto
-Number of constraints: 10
-Number of variables: 13
-Number of range lookups: 6
\ No newline at end of file
+Number of constraints: 547
+Number of variables: 1055
+Number of range lookups: 518
\ No newline at end of file
diff --git a/symbolic-examples/stats/UInt.StrictMul.512.Auto b/symbolic-examples/stats/UInt.StrictMul.512.Auto
index aef9b4bbb..2bc24b897 100644
--- a/symbolic-examples/stats/UInt.StrictMul.512.Auto
+++ b/symbolic-examples/stats/UInt.StrictMul.512.Auto
@@ -1,4 +1,4 @@
 UInt.StrictMul.512.Auto
-Number of constraints: 143
-Number of variables: 236
-Number of range lookups: 108
\ No newline at end of file
+Number of constraints: 1208
+Number of variables: 2314
+Number of range lookups: 1132
\ No newline at end of file