diff --git a/DesignDocument.md b/DesignDocument.md
new file mode 100644
index 0000000..e69de29
diff --git a/src/plutarch-onchain-lib/lib/Plutarch/Core/Eval.hs b/src/plutarch-onchain-lib/lib/Plutarch/Core/Eval.hs
index 690c349..c6fb26c 100644
--- a/src/plutarch-onchain-lib/lib/Plutarch/Core/Eval.hs
+++ b/src/plutarch-onchain-lib/lib/Plutarch/Core/Eval.hs
@@ -18,6 +18,7 @@ module Plutarch.Core.Eval(
   writePlutusScriptTraceBind,
   writePlutusScriptTrace,
   writePlutusScriptNoTrace,
+  calcBudgetNoTraces,
   ) where
 
 import qualified Cardano.Binary              as CBOR
@@ -61,6 +62,15 @@ evalWithArgsT cfg x args = do
   scr <- first (pack . show) escr
   pure (scr, budg, trc)
 
+calcBudgetNoTraces :: ClosedTerm a -> [Data] -> ExBudget
+calcBudgetNoTraces x args =
+  let cmp = compile NoTracing x
+  in  case cmp of 
+        Left e -> error $ "Failed to compile term: " <> show e
+        Right scr -> 
+          let (_, budg, _) = evalScript $ applyArguments scr args
+          in budg 
+
 writePlutusScript :: Config -> String -> FilePath -> ClosedTerm a -> IO ()
 writePlutusScript cfg title filepath term = do
   case evalT cfg term of
diff --git a/src/plutarch-onchain-lib/lib/Plutarch/Core/Time.hs b/src/plutarch-onchain-lib/lib/Plutarch/Core/Time.hs
index 5fc877a..23d7455 100644
--- a/src/plutarch-onchain-lib/lib/Plutarch/Core/Time.hs
+++ b/src/plutarch-onchain-lib/lib/Plutarch/Core/Time.hs
@@ -62,4 +62,14 @@ ptoCustomFiniteRangeH timeRange = do
   PFinite ((pfield @"_0" #) -> start) <- pmatchC (pfield @"_0" # lb)
   PUpperBound ub <- pmatchC timeRangeF.to
   PFinite ((pfield @"_0" #) -> end) <- pmatchC (pfield @"_0" # ub)
-  pure (pnonew $ pfromData start, pnonew $ pfromData end)
\ No newline at end of file
+  pure (pnonew $ pfromData start, pnonew $ pfromData end)
+
+pisFinite :: Term s (PInterval PPosixTime :--> PBool)
+pisFinite = plam $ \i ->
+  let isFiniteFrom = pmatch (pfield @"_0" # (pfield @"from" # i)) $ \case
+        PFinite _ -> pconstant True
+        _ -> pconstant False
+      isFiniteTo = pmatch (pfield @"_0" # (pfield @"to" # i)) $ \case
+        PFinite _ -> pconstant True
+        _ -> pconstant False
+   in pand' # isFiniteFrom # isFiniteTo
\ No newline at end of file
diff --git a/src/plutarch-onchain-lib/lib/Plutarch/Core/Unroll.hs b/src/plutarch-onchain-lib/lib/Plutarch/Core/Unroll.hs
new file mode 100644
index 0000000..2a02600
--- /dev/null
+++ b/src/plutarch-onchain-lib/lib/Plutarch/Core/Unroll.hs
@@ -0,0 +1,53 @@
+{- |
+Unrolling a recursive function involves explicitly laying out some or all of the recursive steps, rather than relying on recursion via a fixed-point combinator.
+In UPLC, the typical `pfix` implementation uses a Y-combinator under the hood. Each recursive step incurs additional evaluation costs (CPU and memory) due to
+the execution of the Y-combinator. By eliminating these costs in each recursive step, unrolled functions reduce execution overhead. However, since each recursive
+step is explicitly laid out, unrolled functions consume more script size.
+
+There are various unrolling strategies available. It is important to carefully study the implications of each strategy, as they may impose different requirements,
+such as hard limit on recursion depth.
+-}
+module Plutarch.Core.Unroll (punrollBound, punrollUnbound, punrollUnboundWhole) where
+
+import Plutarch.Internal.Fix (pfix)
+import Plutarch.Internal.PLam (plam)
+import Plutarch.Internal.Term (Term, (#$), (:-->))
+
+{- |
+The first argument specifies the unrolling depth.
+The second argument defines the fallback behavior when the recursion depth exceeds the provided unrolling depth.
+
+The fixed-point implementation provided requires a Haskell-level value @c@ and a Plutarch function of type `Term s (a :--> b)`. The functional for the recursion is passed as a Haskell function.
+The inclusion of the additional, arbitrary Haskell value (typed @c@) enables further optimization by allowing pre-computation of constant values that depend only on the recursion depth.
+
+@since WIP
+-}
+punrollBound ::
+  forall a b c s.
+  Integer ->
+  (c -> Term s (a :--> b)) ->
+  ((c -> Term s (a :--> b)) -> c -> Term s (a :--> b)) ->
+  c ->
+  Term s (a :--> b)
+punrollBound 0 def _ c = def c
+punrollBound d def f c = f (punrollBound (d - 1) def f) c
+
+{- |
+Unroll given amount of steps, and for rest, uses `pfix` to support unbound recursion.
+
+@since WIP
+-}
+punrollUnbound :: forall a b s. Integer -> (Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
+punrollUnbound 0 f = pfix #$ plam f
+punrollUnbound d f = f (punrollUnbound (d - 1) f)
+
+{- |
+Uses `pfix` to recurse unrolled function itself. Unlike @punrollUnbound@, this function uses unrolled instructions
+within `pfix` recursions.
+
+This should perform better than @punrollUnbound@ when a function requires a large recursion depth.
+
+@since WIP
+-}
+punrollUnboundWhole :: forall a b s. Integer -> (Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
+punrollUnboundWhole d f = pfix #$ plam $ \r -> punrollBound d (const r) (\g () -> f (g ())) ()
\ No newline at end of file
diff --git a/src/plutarch-onchain-lib/lib/Plutarch/Core/Utils.hs b/src/plutarch-onchain-lib/lib/Plutarch/Core/Utils.hs
index 401f5bb..a026a61 100644
--- a/src/plutarch-onchain-lib/lib/Plutarch/Core/Utils.hs
+++ b/src/plutarch-onchain-lib/lib/Plutarch/Core/Utils.hs
@@ -26,7 +26,6 @@ module Plutarch.Core.Utils(
   ppair,
   passert,
   pcheck,
-  pcountScriptInputs,
   pfoldl2,
   pelemAtWithRest',
   pmapIdxs,
@@ -45,19 +44,12 @@ module Plutarch.Core.Utils(
   ptxSignedByPkh,
   (#-),
   pfindWithRest,
-  pcountCS,
-  pcountNonAdaCS,
-  pfirstTokenName,
-  ptryLookupValue,
-  pfilterCSFromValue,
   phasUTxO,
-  pvalueContains,
   pand'List,
   pcond,
   (#>=),
   (#>),
   (#/=),
-  pisFinite,
   pmapAndConvertList,
   pintToByteString,
   punwrapPosixTime,
@@ -73,36 +65,27 @@ module Plutarch.Core.Utils(
 import qualified Data.Text                        as T
 import           Plutarch.Prelude                 
 
-import qualified Plutarch.LedgerApi.AssocMap      as AssocMap
 import Plutarch.LedgerApi.V3
     ( KeyGuarantees(Sorted),
-      PMap(..),
-      PExtended(PFinite),
-      PInterval,
       PMaybeData,
       PAddress,
       PCredential(..),
       PPubKeyHash,
       PDatum,
-      PRedeemer,
       PScriptHash,
       PPosixTime(..),
       POutputDatum(POutputDatum),
       PTxOut,
       PScriptInfo,
-      PScriptPurpose,
       PTxInInfo,
       PTxOutRef,
       AmountGuarantees(Positive),
-      PCurrencySymbol,
-      PTokenName,
       PValue(..) )            
-import           Plutarch.LedgerApi.Value         (padaSymbol,
-                                                   pvalueOf)
 import qualified Plutarch.Monadic                 as P
                                          
 import           Prelude
 import           Plutarch.Internal.Term ( PType ) 
+import Plutarch.Core.Value (pvalueContains)
 
 pfail ::
   forall (s :: S) a.
@@ -194,21 +177,6 @@ passert longErrorMsg b inp = pif b inp $ ptraceInfoError (pconstant longErrorMsg
 pcheck :: forall (s :: S) (a :: PType). Term s PBool -> Term s a -> Term s (PMaybe a)
 pcheck b inp = pif b (pcon $ PJust inp) (pcon PNothing)
 
-pcountScriptInputs :: Term s (PBuiltinList PTxInInfo :--> PInteger)
-pcountScriptInputs =
-  phoistAcyclic $
-    let go :: Term s (PInteger :--> PBuiltinList PTxInInfo :--> PInteger)
-        go = pfix #$ plam $ \self n ->
-              pelimList
-                (\x xs ->
-                  let cred = pfield @"credential" # (pfield @"address" # (pfield @"resolved" # x))
-                   in pmatch cred $ \case
-                        PScriptCredential _ -> self # (n + 1) # xs
-                        _ -> self # n # xs
-                )
-                n
-     in go # 0
-
 pfoldl2 ::
   (PListLike listA, PListLike listB, PElemConstraint listA a, PElemConstraint listB b) =>
   Term s ((acc :--> a :--> b :--> acc) :--> acc :--> listA a :--> listB b :--> acc)
@@ -384,92 +352,6 @@ pfindWithRest = phoistAcyclic $
         mnil = const (ptraceInfoError "Find")
      in precList mcons mnil # ys # pnil
 
-pcountCS ::
-  forall
-    (keys :: KeyGuarantees)
-    (amounts :: AmountGuarantees)
-    (s :: S).
-  Term s (PValue keys amounts :--> PInteger)
-pcountCS = phoistAcyclic $
-  plam $ \val ->
-    pmatch val $ \(PValue val') ->
-      pmatch val' $ \(PMap csPairs) ->
-        plength # csPairs
-
-pcountNonAdaCS ::
-  forall
-    (keys :: KeyGuarantees)
-    (amounts :: AmountGuarantees)
-    (s :: S).
-  Term s (PValue keys amounts :--> PInteger)
-pcountNonAdaCS =
-  phoistAcyclic $
-    let go :: Term (s2 :: S) (PInteger :--> PBuiltinList (PBuiltinPair (PAsData PCurrencySymbol) (PAsData (PMap keys PTokenName PInteger))) :--> PInteger)
-        go = plet (pdata padaSymbol) $ \padaSymbolD ->
-          pfix #$ plam $ \self n ->
-            pelimList (\x xs -> pif (pfstBuiltin # x #== padaSymbolD) (self # n # xs) (self # (n + 1) # xs)) n
-     in plam $ \val ->
-          pmatch val $ \(PValue val') ->
-            pmatch val' $ \(PMap csPairs) ->
-              go # 0 # csPairs
-
-pfirstTokenName ::
-  forall
-    (keys :: KeyGuarantees)
-    (amounts :: AmountGuarantees)
-    (s :: S).
-  Term s (PValue keys amounts :--> PTokenName)
-pfirstTokenName = phoistAcyclic $
-  plam $ \val ->
-    pmatch val $ \(PValue val') ->
-      pmatch val' $ \(PMap csPairs) ->
-        pmatch (pfromData (psndBuiltin # (phead # csPairs))) $ \(PMap tokens) ->
-          pfromData $ pfstBuiltin # (phead # tokens)
-
-ptryLookupValue ::
-  forall
-    (keys :: KeyGuarantees)
-    (amounts :: AmountGuarantees)
-    (s :: S).
-  Term
-    s
-    ( PAsData PCurrencySymbol
-        :--> PValue keys amounts
-        :--> PBuiltinList (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
-    )
-ptryLookupValue = phoistAcyclic $
-  plam $ \policyId val ->
-    pmatch val $ \(PValue val') ->
-      precList
-        ( \self x xs ->
-            pif
-              (pfstBuiltin # x #== policyId)
-              ( pmatch (pfromData (psndBuiltin # x)) $ \(PMap tokens) ->
-                  tokens
-              )
-              (self # xs)
-        )
-        (const perror)
-        # pto val'
-
-{- | Removes a currency symbol from a value
--}
-pfilterCSFromValue ::
-  forall
-    (anyOrder :: KeyGuarantees)
-    (anyAmount :: AmountGuarantees).
-  ClosedTerm
-    ( PValue anyOrder anyAmount
-        :--> PAsData PCurrencySymbol
-        :--> PValue anyOrder anyAmount
-    )
-pfilterCSFromValue = phoistAcyclic $
-  plam $ \value policyId ->
-      let mapVal = pto (pto value)
-          go = pfix #$ plam $ \self ys ->
-                pelimList (\x xs -> pif (pfstBuiltin # x #== policyId) xs (pcons # x # (self # xs))) pnil ys
-       in pcon (PValue $ pcon $ PMap $ go # mapVal)
-
 {- | @phasUTxO # oref # inputs@
   ensures that in @inputs@ there is an input having @TxOutRef@ @oref@ .
 -}
@@ -483,24 +365,6 @@ phasUTxO = phoistAcyclic $
   plam $ \oref inInputs ->
     pany @PBuiltinList # plam (\input -> oref #== (pfield @"outRef" # input)) # inInputs
 
-pvalueContains ::
-  ClosedTerm
-    ( PValue 'Sorted 'Positive
-        :--> PValue 'Sorted 'Positive
-        :--> PBool
-    )
-pvalueContains = phoistAcyclic $
-  plam $ \superset subset ->
-    let forEachTN cs = plam $ \tnPair ->
-          let tn = pfromData $ pfstBuiltin # tnPair
-              amount = pfromData $ psndBuiltin # tnPair
-           in amount #<= pvalueOf # superset # cs # tn
-        forEachCS = plam $ \csPair ->
-          let cs = pfromData $ pfstBuiltin # csPair
-              tnMap = pto $ pfromData $ psndBuiltin # csPair
-           in pall # forEachTN cs # tnMap
-     in pall # forEachCS #$ pto $ pto subset
-
 pand'List :: [Term s PBool] -> Term s PBool
 pand'List ts' =
   case ts' of
@@ -515,16 +379,6 @@ pand'List ts' =
 a #/= b = pnot # (a #== b)
 infix 4 #/=
 
-pisFinite :: Term s (PInterval PPosixTime :--> PBool)
-pisFinite = plam $ \i ->
-  let isFiniteFrom = pmatch (pfield @"_0" # (pfield @"from" # i)) $ \case
-        PFinite _ -> pconstant True
-        _ -> pconstant False
-      isFiniteTo = pmatch (pfield @"_0" # (pfield @"to" # i)) $ \case
-        PFinite _ -> pconstant True
-        _ -> pconstant False
-   in pand' # isFiniteFrom # isFiniteTo
-
 pmapAndConvertList :: (PIsListLike listA a, PIsListLike listB b) => Term s ((a :--> b) :--> listA a :--> listB b)
 pmapAndConvertList = phoistAcyclic $
   plam $ \f ->
diff --git a/src/plutarch-onchain-lib/lib/Plutarch/Core/Value.hs b/src/plutarch-onchain-lib/lib/Plutarch/Core/Value.hs
index 8d7f60a..3c44a4f 100644
--- a/src/plutarch-onchain-lib/lib/Plutarch/Core/Value.hs
+++ b/src/plutarch-onchain-lib/lib/Plutarch/Core/Value.hs
@@ -282,3 +282,136 @@ psingletonOfCS = phoistAcyclic $
         )
         (const perror)
         # pto val'
+
+{- | Lookup the list of token-quantity pairs for a given currency symbol in a value.
+     If the currency symbol is not found, the function will throw an error.
+
+     This function takes a currency symbol and a value, and returns the list of token-quantity pairs
+     associated with that currency symbol. The value is represented as a `PValue` which is a map of
+     currency symbols to lists of token-quantity pairs. The function traverses this map to find the
+     matching currency symbol and returns the associated list of token-quantity pairs.
+
+     If the currency symbol is not found in the value, the function will throw an error using `perror`.
+
+     Example usage:
+
+     @
+     let currencySymbol = ...
+         value = ...
+     in ptryLookupValue # currencySymbol # value
+     @
+
+     This will return the list of token-quantity pairs for the given currency symbol, or throw an error
+     if the currency symbol is not found.
+
+     Arguments:
+     * `policyId` - The currency symbol to look up.
+     * `val` - The value to search within.
+
+     Returns:
+     * A builtin list of token-quantity pairs associated with the given currency symbol.
+
+-}
+ptryLookupValue ::
+  forall
+    (keys :: KeyGuarantees)
+    (amounts :: AmountGuarantees)
+    (s :: S).
+  Term
+    s
+    ( PAsData PCurrencySymbol
+        :--> PValue keys amounts
+        :--> PBuiltinList (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
+    )
+ptryLookupValue = phoistAcyclic $
+  plam $ \policyId val ->
+    pmatch val $ \(PValue val') ->
+      precList
+        ( \self x xs ->
+            pif
+              (pfstBuiltin # x #== policyId)
+              ( pmatch (pfromData (psndBuiltin # x)) $ \(PMap tokens) ->
+                  tokens
+              )
+              (self # xs)
+        )
+        (const perror)
+        # pto val'
+
+{- | Removes a currency symbol from a value
+-}
+pfilterCSFromValue ::
+  forall
+    (anyOrder :: KeyGuarantees)
+    (anyAmount :: AmountGuarantees).
+  ClosedTerm
+    ( PValue anyOrder anyAmount
+        :--> PAsData PCurrencySymbol
+        :--> PValue anyOrder anyAmount
+    )
+pfilterCSFromValue = phoistAcyclic $
+  plam $ \value policyId ->
+      let mapVal = pto (pto value)
+          go = pfix #$ plam $ \self ys ->
+                pelimList (\x xs -> pif (pfstBuiltin # x #== policyId) xs (pcons # x # (self # xs))) pnil ys
+       in pcon (PValue $ pcon $ PMap $ go # mapVal)
+
+pvalueContains ::
+  ClosedTerm
+    ( PValue 'Sorted 'Positive
+        :--> PValue 'Sorted 'Positive
+        :--> PBool
+    )
+pvalueContains = phoistAcyclic $
+  plam $ \superset subset ->
+    let forEachTN cs = plam $ \tnPair ->
+          let tn = pfromData $ pfstBuiltin # tnPair
+              amount = pfromData $ psndBuiltin # tnPair
+           in amount #<= pvalueOf # superset # cs # tn
+        forEachCS = plam $ \csPair ->
+          let cs = pfromData $ pfstBuiltin # csPair
+              tnMap = pto $ pfromData $ psndBuiltin # csPair
+           in pall # forEachTN cs # tnMap
+     in pall # forEachCS #$ pto $ pto subset
+
+pfirstTokenName ::
+  forall
+    (keys :: KeyGuarantees)
+    (amounts :: AmountGuarantees)
+    (s :: S).
+  Term s (PValue keys amounts :--> PTokenName)
+pfirstTokenName = phoistAcyclic $
+  plam $ \val ->
+    pmatch val $ \(PValue val') ->
+      pmatch val' $ \(PMap csPairs) ->
+        pmatch (pfromData (psndBuiltin # (phead # csPairs))) $ \(PMap tokens) ->
+          pfromData $ pfstBuiltin # (phead # tokens)
+
+pcountCS ::
+  forall
+    (keys :: KeyGuarantees)
+    (amounts :: AmountGuarantees)
+    (s :: S).
+  Term s (PValue keys amounts :--> PInteger)
+pcountCS = phoistAcyclic $
+  plam $ \val ->
+    pmatch val $ \(PValue val') ->
+      pmatch val' $ \(PMap csPairs) ->
+        plength # csPairs
+
+pcountNonAdaCS ::
+  forall
+    (keys :: KeyGuarantees)
+    (amounts :: AmountGuarantees)
+    (s :: S).
+  Term s (PValue keys amounts :--> PInteger)
+pcountNonAdaCS =
+  phoistAcyclic $
+    let go :: Term (s2 :: S) (PInteger :--> PBuiltinList (PBuiltinPair (PAsData PCurrencySymbol) (PAsData (PMap keys PTokenName PInteger))) :--> PInteger)
+        go = plet (pdata padaSymbol) $ \padaSymbolD ->
+          pfix #$ plam $ \self n ->
+            pelimList (\x xs -> pif (pfstBuiltin # x #== padaSymbolD) (self # n # xs) (self # (n + 1) # xs)) n
+     in plam $ \val ->
+          pmatch val $ \(PValue val') ->
+            pmatch val' $ \(PMap csPairs) ->
+              go # 0 # csPairs
\ No newline at end of file
diff --git a/src/plutarch-onchain-lib/plutarch-onchain-lib.cabal b/src/plutarch-onchain-lib/plutarch-onchain-lib.cabal
index b7a54c4..001c6b1 100644
--- a/src/plutarch-onchain-lib/plutarch-onchain-lib.cabal
+++ b/src/plutarch-onchain-lib/plutarch-onchain-lib.cabal
@@ -59,6 +59,7 @@ library
     Plutarch.Core.PByteString
     Plutarch.Core.Scripts
     Plutarch.Core.Time
+    Plutarch.Core.Unroll
     Plutarch.Core.Utils
     Plutarch.Core.ValidationLogic
     Plutarch.Core.Value
diff --git a/src/plutarch-onchain-lib/test/Bench.hs b/src/plutarch-onchain-lib/test/Bench.hs
index 540df1c..cc7435b 100644
--- a/src/plutarch-onchain-lib/test/Bench.hs
+++ b/src/plutarch-onchain-lib/test/Bench.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE QualifiedDo #-}
 {-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE CPP                  #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 
 module Main (main) where
@@ -13,6 +16,7 @@ import Plutarch.LedgerApi.V3
 import Plutarch.Core.List
 import Plutarch.Core.FieldBinds
 import Plutarch.Core.ValidationLogic
+import Plutarch.Core.Unroll
 import Plutarch.Maybe
 import Plutarch.Internal.Term
 import Test.Tasty (TestTree, testGroup)
@@ -91,11 +95,9 @@ main =
       , testGroup "Find" findBenches
       , testGroup "Count Spend Scripts" countSpendBenches
       , testGroup "Elem At" elemAtBenches
-      --, testGroup "Spending Purpose" spendingPurposeBenches
+      , testGroup "Unroll" unrollBench
       ]
 
--- Suites
-
 dropBenches :: [TestTree]
 dropBenches =
   [ bench "recursive" (pdropR # 500 # pconstant @(PBuiltinList PInteger) [1..500])
@@ -134,26 +136,17 @@ elemAtBenches =
   , bench "fast" $ pelemAtFast # pconstant @(PBuiltinList PInteger) [1..200] # 199 
   ]
 
-
-spendingPurposeBenches :: [TestTree]
-spendingPurposeBenches =
-  [ bench "generic"
-      (mkValidatorGeneric # pconstant (mkScriptContext 2))
-  , bench "specialized"
-      (mkValidatorSpecialized # pconstant (mkScriptContext 2))
-  ]
-
-mkValidatorGeneric :: ClosedTerm (PScriptContext :--> PUnit)
-mkValidatorGeneric = plam $ \ctx -> P.do
-  ctxF <- pletFields @'["txInfo", "redeemer", "scriptInfo"] ctx
-  PSpendingScript scriptInfo <- pmatch ctxF.scriptInfo
-  scriptInfoF <- pletFields @'["_1"] scriptInfo
-  PDJust ownInDat <- pmatch scriptInfoF._1
-  pif (pfromData (punsafeCoerce @(PAsData PInteger) (pto ownInDat)) #> 0) (pconstant ()) perror
-
-mkValidatorSpecialized :: ClosedTerm (PScriptContext :--> PUnit)
-mkValidatorSpecialized = plam $ \ctx -> P.do
-  ctxF <- pletFields @'["txInfo", "redeemer", "scriptInfo"] ctx
-  scriptInfoF <- pletFieldsSpending ctxF.scriptInfo
-  PDJust ownInDat <- pmatch scriptInfoF._1
-  pif (pfromData (punsafeCoerce @(PAsData PInteger) (pto ownInDat)) #> 0) (pconstant ()) perror
\ No newline at end of file
+unrollLengthBound :: forall list a s. PIsListLike list a => Term s (list a :--> PInteger)
+unrollLengthBound = punrollBound 200 (const $ plam $ \_ -> pconstant (-1)) go 0
+  where
+    go ::
+      (Integer -> Term s (list a :--> PInteger)) ->
+      Integer ->
+      Term s (list a :--> PInteger)
+    go self n = plam $ pelimList (\_ xs -> self (n + 1) # xs) (pconstant n)
+
+unrollBench :: [TestTree]
+unrollBench =
+  [ bench "unroll length bound" $ unrollLengthBound # pconstant @(PBuiltinList PInteger) [1..200]
+  , bench "no-unroll recursion" $ plength # pconstant @(PBuiltinList PInteger) [1..200]
+  ]
\ No newline at end of file