diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
diff --git a/app/Implicit.hs b/app/Implicit.hs
new file mode 100644
--- /dev/null
+++ b/app/Implicit.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, ImpredicativeTypes #-}
+
+-- | Testing the code about printing implicit queues.
+module Implicit where
+
+import Control.Monad.Credit
+import Test.Credit.Queue.Base
+import Test.Credit.Queue.Implicit
+
+testImplicit :: Either String (Maybe (Int, String), Ticks)
+testImplicit =
+  runCounterM $ (=<<) (traverse (traverse showImplicit)) $
+    empty >>= (`snoc` 1) >>= (`snoc` 2) >>= (`snoc` 3)
+          >>= (`snoc` 4) >>= (`snoc` 5) >>= uncons
diff --git a/app/Intro.hs b/app/Intro.hs
new file mode 100644
--- /dev/null
+++ b/app/Intro.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}
+
+-- | Testing the code in the introduction of the paper.
+module Intro where
+
+import Control.Monad
+import System.Environment (getArgs)
+import Test.QuickCheck
+
+import Control.Monad.Credit
+
+data Batched a = Batched [a] [a]
+  deriving (Eq, Ord, Show)
+
+rev :: MonadCount m => [a] -> [a] -> m [a]
+rev [] acc = pure acc
+rev (x : xs) acc = tick >> rev xs (x : acc)
+
+batched :: MonadCount m => [a] -> [a] -> m (Batched a)
+batched [] rear = do
+  front <- rev rear []
+  pure $ Batched front []
+batched front rear = pure $ Batched front rear
+
+empty :: MonadCount m => m (Batched a)
+empty = pure $ Batched [] []
+
+snoc :: MonadCount m => Batched a -> a -> m (Batched a)
+snoc   (Batched front rear) x = batched front (x : rear)
+
+uncons :: MonadCount m => Batched a -> m (Maybe (a, Batched a))
+uncons (Batched [] []) = pure Nothing
+uncons (Batched (x:front) rear) = do
+  q' <- batched front rear
+  pure $ Just (x, q')
+
+unfoldM :: Monad m => (b -> m (Maybe (a, b))) -> b -> m [a] 
+unfoldM f b = do
+  mb <- f b
+  case mb of
+    Nothing -> pure []
+    Just (x, b') -> (x :) <$> unfoldM f b'
+
+testBatched :: Either String ([Int], Ticks)
+testBatched =
+  runCounterM $ empty >>= flip (foldM snoc) [1..10]
+                      >>= unfoldM uncons
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, DerivingStrategies #-}
+
+module Main where
+
+import UnliftIO.Internals.Async
+import System.Environment (getArgs)
+import Test.QuickCheck
+import Prettyprinter
+
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Queue.Base
+import Test.Credit.Queue.Batched
+import Test.Credit.Queue.Bankers
+import Test.Credit.Queue.Physicists
+import Test.Credit.Queue.Realtime
+import Test.Credit.Queue.Bootstrapped
+import Test.Credit.Queue.Implicit
+import Test.Credit.Deque.Base
+import Test.Credit.Deque.Bankers
+import Test.Credit.Deque.Realtime
+import Test.Credit.Deque.Catenable
+import Test.Credit.Deque.SimpleCat
+import Test.Credit.Deque.ImplicitCat
+import Test.Credit.Finger
+import Test.Credit.Heap.Base
+import Test.Credit.Heap.Binomial
+import Test.Credit.Heap.LazyPairing
+import Test.Credit.Heap.Scheduled
+import Test.Credit.Sortable.Base
+import Test.Credit.Sortable.MergeSort
+import Test.Credit.Sortable.Scheduled
+import Test.Credit.RandomAccess.Base
+import Test.Credit.RandomAccess.Binary
+import Test.Credit.RandomAccess.Zeroless
+
+run :: forall t op. (MemoryStructure t, DataStructure t op) => Args -> Strategy -> IO Result
+run args strat = quickCheckWithResult args $ checkCreditsMemory @t strat
+
+newtype Alpha = Alpha Char
+  deriving (Eq, Ord)
+  deriving newtype (Pretty)
+
+instance Show Alpha where
+  show (Alpha c) = [c]
+
+instance Arbitrary Alpha where
+  arbitrary = Alpha <$> frequency
+    [ (1, choose ('a', 'z')), (1, choose ('A', 'Z')) ]
+
+benchmarks :: Args -> [(String, IO Result)]
+benchmarks args =
+  [ (benchs ++ strats ++ ":", runB args strat)
+  | (strats, strat) <-
+      [ (" (path)", Path)
+      , (" (bloom)", Bloom)
+      , (" (pennant)", Pennant)
+      , (" (random)", Random)
+      ]
+  , (benchs, runB) <- reverse
+      [ ("Batched Queue", run @(Q Batched Alpha))
+      , ("Bankers Queue", run @(Q BQueue Alpha))
+      , ("Physicists Queue", run @(Q Physicists Alpha))
+      , ("Realtime Queue", run @(Q RQueue Alpha))
+      , ("Bootstrapped Queue", run @(Q Bootstrapped Alpha))
+      , ("Implicit Queue", run @(Q Implicit Alpha))
+      , ("Bankers Deque", run @(D BDeque Alpha))
+      , ("Realtime Deque", run @(D RDeque Alpha))
+      , ("Catenable List", run @(D CatDeque Alpha))
+      , ("Simple Catenable Deque", run @(D SimpleCat Alpha))
+      , ("Implicit Catenable Deque", run @(D ImplicitCat Alpha))
+      , ("Catenable List (Concat)", run @(BD CatDeque Alpha))
+      , ("Simple Catenable Deque (Concat)", run @(BD SimpleCat Alpha))
+      , ("Implicit Catenable Deque (Concat)", run @(BD ImplicitCat Alpha))
+      , ("Binomial Heap", run @(H Binomial Alpha))
+      , ("Lazy Pairing Heap", run @(H LazyPairing Alpha))
+      , ("Scheduled Binomial Heap", run @(H Scheduled Alpha))
+      , ("Binomial Heap (Merge)", run @(BH Binomial Alpha))
+      , ("Lazy Pairing Heap (Merge)", run @(BH LazyPairing Alpha))
+      , ("Scheduled Binomial Heap (Merge)", run @(BH Scheduled Alpha))
+      , ("Mergesort", run @(S MergeSort Alpha))
+      , ("Scheduled Mergesort", run @(S SMergeSort Alpha))
+      , ("Binary Random Access List", run @(RA BinaryRA Alpha))
+      , ("Zeroless Random Access List", run @(RA ZerolessRA Alpha))
+      , ("Finger Tree (Deque)", run @(D FingerDeque Alpha))
+      , ("Finger Tree (Concat)", run @(BD FingerDeque Alpha))
+      , ("Finger Tree (Heap)", run @(H FingerHeap Alpha))
+      , ("Finger Tree (Merge)", run @(BH FingerHeap Alpha))
+      , ("Finger Tree (Random Access)", run @(RA FingerRA Alpha))
+      , ("Finger Tree (Sortable)", run @(S FingerSort Alpha))
+      ]
+  ]
+
+main :: IO ()
+main = do
+  (maxSuccess, maxSize) <- do
+    args <- getArgs
+    case args of
+      [n, s]    -> pure (read n, read s)
+      [n]       -> pure (read n, 1000)
+      _         -> pure (1000,   1000)
+  let args = stdArgs { maxSuccess, maxSize, maxShrinks = maxBound, chatty = False }
+  pooledForConcurrently_ (benchmarks args) $ \(s,r) -> do
+    res <- r
+    putStrLn $ s ++ "\n" ++ output res
+
+-- Categorization of implementations:
+
+-- Passing static credits to static reference:
+--  - Realtime Queue (Section 7.2)
+--  - Realtime Deque (Section 8.4.3)
+--  - Scheduled Binomial Heaps (Section 7.3)
+--  - Scheduled Mergesort (Section 7.4)
+
+-- Passing static credits to dynamic reference:
+--  - Implicit Queue (Section 11.1)
+--  - Binary Random Access List (Section 9.2.3)
+--  - Zeroless Random Access List (Section 9.2.3)
+--  - Finger Tree
+--  - Simple Catenable Deque (Section 11.2)
+--  - Implicit Catenable Deque (Section 11.2)
+
+-- Passing dynamic credits to static reference:
+--  - Binomial Heaps (Section 6.4.1)
+--  - Lazy Pairing Heaps (Section 6.5)
+--  - Bottom-up Mergesort (Section 6.4.3)
+
+-- Passing static credits to ghost reference:
+--  - Bootstrapped Queue (Section 10.1.3)
+--  - Physicists Queue (Section 6.4.2)
+
+-- Requires extra traversal:
+--  - Catenable List (Section 10.2.1)
+
+-- Needs Credit Inheritance:
+--  - Bankers Queue (Section 6.3.2)
+--  - Bankers Deque (Section 8.4.2)
diff --git a/app/Stack.hs b/app/Stack.hs
new file mode 100644
--- /dev/null
+++ b/app/Stack.hs
@@ -0,0 +1,61 @@
+module Stack where
+
+fn :: Int -> (a -> a) -> a -> a
+fn 0 f x = x
+fn n f x = fn (n - 1) f (f x)
+
+suc :: Int -> Int
+suc n = n + 1
+
+exp1 :: Int -> Int -> Int
+exp1 m n = fn m (fn n) suc 0
+
+--
+
+data Fun b = Unit (b -> b) | Rec (Fun b) (Fun b -> b -> b)
+
+call :: Fun b -> b -> b
+call (Unit f) x = f x
+call (Rec env f) x = f env x
+
+fn' :: Int -> Fun b -> b -> b
+fn' 0 f x = x
+fn' n f x = fn' (n - 1) f (call f x)
+
+fn1 :: Int -> Fun b -> Fun b
+fn1 n f = Rec f (fn' n)
+
+exp2 :: Int -> Int -> Int
+exp2 m n = call (fn' m (Unit (fn1 n)) (Unit suc)) 0
+
+--
+
+data Closure b where
+  Exists :: a -> (a -> b -> b) -> Closure b
+
+callC :: Closure b -> b -> b
+callC (Exists x f) y = f x y
+
+fnC :: Int -> Closure b -> b -> b
+fnC 0 c x = x
+fnC n c x = fnC (n - 1) c (callC c x)
+
+fnC1 :: Int -> Closure b -> Closure b
+fnC1 n c = Exists c (fnC n)
+
+fnC1' :: Int -> () -> Closure b -> Closure b
+fnC1' n () c = fnC1 n c
+
+sucC :: () -> Int -> Int
+sucC () n = n + 1
+
+exp3 :: Int -> Int -> Int
+exp3 m n = callC (fnC m (Exists () (fnC1' n)) (Exists () sucC)) 0
+
+--
+
+-- type Closure b c = ... | Fn (type of env) (type of env -> b -> c) | ...
+-- [[\x.^n e]] = (fn, env) where
+--   fn env x = [[e]]
+--   env = "free vars in [[e]]"
+
diff --git a/creditmonad.cabal b/creditmonad.cabal
new file mode 100644
--- /dev/null
+++ b/creditmonad.cabal
@@ -0,0 +1,103 @@
+cabal-version: 2.2
+
+-- This file has been generated from package.yaml by hpack version 0.38.1.
+--
+-- see: https://github.com/sol/hpack
+
+name:           creditmonad
+version:        1.0.0
+synopsis:       Reasoning about amortized time complexity
+description:    Persistent data structures are ubiquitous in functional
+                programming languages and their designers frequently have to
+                reason about amortized time complexity. But proving amortized
+                bounds is difficult in a persistent setting, and pen-and-paper
+                proofs give little assurance of correctness, while a full
+                mechanization in a proof assistant can be too involved for the
+                casual user. This package defines a domain specific
+                language for testing the amortized time complexity of
+                persistent data structures using QuickCheck. The DSL can
+                give strong evidence of correctness, while imposing low
+                overhead on the user. The package includes implementations
+                and tests of all lazy data structures given in Okasaki's book.
+                See the paper "Lightweight Testing of Persistent Amortized Time
+                Complexity in the Credit Monad" (2025) for a detailed description.
+category:       Development
+homepage:       https://github.com/anfelor/creditmonad#readme
+bug-reports:    https://github.com/anfelor/creditmonad/issues
+author:         Anton Lorenzen <anton.lorenzen@ed.ac.uk>
+maintainer:     Anton Lorenzen <anton.lorenzen@ed.ac.uk>
+license:        BSD-3-Clause
+build-type:     Simple
+extra-doc-files:
+    CHANGELOG.md
+
+source-repository head
+  type: git
+  location: https://github.com/anfelor/creditmonad
+
+library
+  exposed-modules:
+      Control.Monad.Credit
+      Test.Credit
+      Test.Credit.Deque.Bankers
+      Test.Credit.Deque.Base
+      Test.Credit.Deque.Catenable
+      Test.Credit.Deque.ImplicitCat
+      Test.Credit.Deque.Realtime
+      Test.Credit.Deque.SimpleCat
+      Test.Credit.Deque.Streams
+      Test.Credit.Finger
+      Test.Credit.Heap.Base
+      Test.Credit.Heap.Binomial
+      Test.Credit.Heap.LazyPairing
+      Test.Credit.Heap.Pairing
+      Test.Credit.Heap.Scheduled
+      Test.Credit.Queue.Bankers
+      Test.Credit.Queue.Base
+      Test.Credit.Queue.Batched
+      Test.Credit.Queue.Bootstrapped
+      Test.Credit.Queue.Implicit
+      Test.Credit.Queue.Physicists
+      Test.Credit.Queue.Realtime
+      Test.Credit.Queue.Streams
+      Test.Credit.RandomAccess.Base
+      Test.Credit.RandomAccess.Binary
+      Test.Credit.RandomAccess.Zeroless
+      Test.Credit.Sortable.Base
+      Test.Credit.Sortable.MergeSort
+      Test.Credit.Sortable.Scheduled
+  other-modules:
+      Control.Monad.Credit.Base
+      Control.Monad.Credit.CreditM
+      Control.Monad.Credit.CounterM
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -Wno-name-shadowing
+  build-depends:
+      QuickCheck >=2.14 && <3
+    , STMonadTrans ==0.4.*
+    , base >=4.13 && <5
+    , containers >=0.6 && <1.7
+    , mtl ==2.3.*
+    , prettyprinter ==1.7.*
+  default-language: GHC2021
+
+executable creditmonad
+  main-is: Main.hs
+  other-modules:
+      Implicit
+      Intro
+      Stack
+  hs-source-dirs:
+      app
+  ghc-options: -Wall -Wno-name-shadowing -O2 -fworker-wrapper-cbv -threaded -rtsopts
+  build-depends:
+      QuickCheck >=2.14 && <3
+    , STMonadTrans ==0.4.*
+    , base >=4.13 && <5
+    , containers >=0.6 && <1.7
+    , creditmonad
+    , mtl ==2.3.*
+    , prettyprinter ==1.7.*
+    , unliftio ==0.2.*
+  default-language: GHC2021
diff --git a/src/Control/Monad/Credit.hs b/src/Control/Monad/Credit.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Credit.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE GADTs #-}
+
+module Control.Monad.Credit 
+  (
+  -- * Computations with credits
+    Control.Monad.Credit.Base.MonadCount(..), Control.Monad.Credit.Base.MonadLazy (..), Control.Monad.Credit.Base.HasStep(..), Control.Monad.Credit.Base.Lazy(..)
+  , Control.Monad.Credit.Base.Ticks, Control.Monad.Credit.Base.Credit, Control.Monad.Credit.Base.MonadCredit(..), Control.Monad.Credit.Base.MonadInherit(..)
+  -- * Counter Monad
+  , Control.Monad.Credit.CounterM.CounterM, Control.Monad.Credit.CounterM.runCounterM, Control.Monad.Credit.CounterM.CounterT, Control.Monad.Credit.CounterM.runCounterT
+  -- * Credit Monad
+  , Control.Monad.Credit.CreditM.CreditM, Control.Monad.Credit.CreditM.runCreditM, Control.Monad.Credit.CreditM.CreditT, Control.Monad.Credit.CreditM.runCreditT
+  , Control.Monad.Credit.CreditM.Error(..), Control.Monad.Credit.Base.Cell
+  -- * Pretty-printing memory cells
+  , Control.Monad.Credit.Base.Memory, Control.Monad.Credit.Base.mkMCell, Control.Monad.Credit.Base.mkMList, linearize
+  , Control.Monad.Credit.Base.MemoryCell(..), Control.Monad.Credit.Base.MonadMemory(..), Control.Monad.Credit.Base.PrettyCell(..), Control.Monad.Credit.Base.MemoryStructure(..)
+  ) where
+
+import Control.Monad.Credit.Base
+import Control.Monad.Credit.CreditM
+import Control.Monad.Credit.CounterM
diff --git a/src/Control/Monad/Credit/Base.hs b/src/Control/Monad/Credit/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Credit/Base.hs
@@ -0,0 +1,202 @@
+{-# LANGUAGE DerivingStrategies, TypeFamilies #-}
+
+module Control.Monad.Credit.Base
+  ( Cell(..), Credit(..), Ticks(..)
+  , MonadCount(..), MonadLazy(..), MonadCredit(..), HasStep(..), Lazy(..), MonadInherit(..)
+  , MTree(..), Memory(..), MemoryCell(..), MonadMemory(..), linearize, mkMCell, mkMList
+  , MemoryStructure(..), PrettyCell(..)
+  ) where
+
+import Prettyprinter
+import Control.Monad
+import Control.Monad.State
+import Data.Char
+import Data.Maybe
+import Data.Map (Map)
+import Data.Kind (Type)
+import qualified Data.Map as Map
+
+newtype Credit = Credit Int
+  deriving (Eq, Ord, Show)
+  deriving newtype (Num, Enum, Real, Integral, Pretty)
+
+newtype Cell = Cell Int
+  deriving (Eq, Ord, Show)
+
+instance Pretty Cell where
+  pretty (Cell 0) = pretty "main thread"
+  pretty (Cell i) = pretty "thunk" <+> pretty i
+
+newtype Ticks = Ticks Int
+  deriving (Eq, Ord, Show)
+  deriving newtype (Num, Enum, Real, Integral, Pretty)
+
+class Monad m => MonadCount m where
+  tick :: m ()
+  -- ^ tick consumes one credit of the current cell
+
+class Monad m => MonadLazy m where
+  data Thunk m :: (Type -> Type) -> Type -> Type
+  delay :: t a -> m (Thunk m t a)
+  -- ^ delay creates a new cell with the given thunk
+  force :: HasStep t m => Thunk m t a -> m a
+  -- ^ force retrieves and evaluates the thunk of a cell
+  lazymatch :: Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b
+  -- ^ lazymatch can inspect the unevaluated thunk and allows us to
+  -- perform an action like forcing or assigning credits.
+
+-- | Thunks can take a step to yield a computation that evaluates to their result.
+class HasStep t m where
+  step :: t a -> m a
+
+-- | A basic thunk that contains the computation to be evaluated.
+-- This type can be used to express any thunk but its disadvantage is that
+-- it will be printed merely as "<lazy>".
+newtype Lazy m a = Lazy (m a)
+
+instance HasStep (Lazy m) m where
+  step (Lazy f) = f
+
+-- | A computation in the credit monad has a given amounts of credits,
+-- which it can spend on computation or transfer to other cells.
+class (MonadCount m, MonadLazy m, MonadFail m) => MonadCredit m where
+  creditWith :: Thunk m t a -> Credit -> m ()
+  -- ^ creditWith transfers a given amount of credits to a cell
+  hasAtLeast :: Thunk m t a -> Credit -> m ()
+  -- ^ assert that a cell has at least a given amount of credits
+
+class MonadCredit m => MonadInherit m where
+  creditAllTo :: Thunk m t a -> m ()
+  -- ^ creditAllTo transfers all credits to a cell and assigns it as heir
+
+data MTree = MCell String [MTree] | MList [MTree] (Maybe MTree) | Indirection Cell
+
+-- | A view of memory that can be pretty-printed.
+data Memory = Memory
+  { memoryTree :: MTree
+  , memoryStore :: Map Cell (MTree, Credit)
+  }
+
+-- | Make memory cell with a given tag and a list of children.
+mkMCell :: String -> [Memory] -> Memory
+mkMCell d ms = Memory (MCell d (map memoryTree ms)) (Map.unions (map memoryStore ms))
+
+-- | A special case for nicer printing of list-like datatypes.
+-- ''mkMList [m1,...,mn] Nothing'' renders as ''[m1, .., mn]'', while
+-- ''mkMList [m1,...,mn] (Just m)'' renders as ''[m1, .., mn] ++ m''.
+mkMList :: [Memory] -> Maybe Memory -> Memory
+mkMList ms mm =
+  let ms' = case mm of Nothing -> ms; Just m -> ms ++ [m] in
+  Memory (MList (map memoryTree ms) (fmap memoryTree mm)) (Map.unions (map memoryStore ms'))
+
+-- | A class for pretty-printing memory cells.
+class Monad m => MemoryCell m a where
+  prettyCell :: a -> m Memory
+
+instance Monad m => MemoryCell m Int where
+  prettyCell i = pure $ mkMCell (show i) []
+
+instance MemoryCell m a => MemoryCell m [a] where
+  prettyCell xs = flip mkMList Nothing <$> mapM prettyCell xs
+
+instance (MemoryCell m a, MemoryCell m b) => MemoryCell m (a, b) where
+  prettyCell (a, b) = mkMCell "" <$> sequence [prettyCell a, prettyCell b]
+
+instance (MemoryCell m a, MemoryCell m b, MemoryCell m c) => MemoryCell m (a, b, c) where
+  prettyCell (a, b, c) = mkMCell "" <$> sequence [prettyCell a, prettyCell b, prettyCell c]
+
+instance Monad m => MemoryCell m (Lazy m a) where
+  prettyCell (Lazy _) = pure $ mkMCell "<lazy>" []
+
+class Monad m => MonadMemory m where
+  prettyThunk :: (MemoryCell m a, MemoryCell m (t a)) => Thunk m t a -> m Memory
+
+instance (MonadMemory m, MemoryCell m a, MemoryCell m (t a)) => MemoryCell m (Thunk m t a) where
+  prettyCell t = prettyThunk t
+
+newtype PrettyCell a = PrettyCell a
+  deriving (Eq, Ord, Show)
+
+instance (Monad m, Pretty a) => MemoryCell m (PrettyCell a) where
+  prettyCell (PrettyCell a) = pure $ mkMCell (show $ pretty a) []
+
+class MemoryStructure t where
+  prettyStructure :: MonadMemory m => t m -> m Memory
+
+showCredit :: Credit -> String
+showCredit (Credit c) = map (chr . (\n -> n - 48 + 8320) . ord) $ show c
+
+annCredit :: Credit -> MTree -> MTree
+annCredit c (MCell d ms) = MCell (d ++ showCredit c) ms
+annCredit c m = m
+
+-- | Inline memory cells that are only used once and remove them from the store 
+linearize :: Memory -> Memory
+linearize mem = linearize' mem $ countUsages mem
+  where
+    countUsage :: MTree -> Map Cell Int
+    countUsage (MCell _ ms) = Map.unionsWith (+) (map countUsage ms)
+    countUsage (MList ms mm) =
+      Map.unionsWith (+) (countUsage <$> ms ++ maybeToList mm)
+    countUsage (Indirection c) = Map.singleton c 1
+
+    countUsages :: Memory -> Map Cell Int
+    countUsages (Memory mtree mstore) = Map.unionsWith (+) (countUsage mtree : map (countUsage . fst) (Map.elems mstore))
+
+    lin :: Map Cell Int -> Map Cell (MTree, Credit) -> Cell -> State (Map Cell (MTree, Credit)) ()
+    lin usages mstore c = do
+      mstore' <- get
+      when (Map.notMember c mstore') $
+        case Map.lookup c mstore of
+          Just (mtree, credit) -> do
+            mtree' <- linearizeTree usages mstore mtree
+            case Map.lookup c usages of
+              Just 1 -> modify' $ Map.insert c (annCredit credit mtree', credit)
+              _ -> modify' $ Map.insert c (mtree', credit)
+          Nothing -> pure ()
+
+    linearizeTree :: Map Cell Int -> Map Cell (MTree, Credit) -> MTree -> State (Map Cell (MTree, Credit)) MTree
+    linearizeTree usages mstore (MCell d ms) = do
+      ms' <- mapM (linearizeTree usages mstore) ms
+      pure $ MCell d ms'
+    linearizeTree usages mstore (MList ms mm) = do
+      ms' <- mapM (linearizeTree usages mstore) ms
+      mm' <- mapM (linearizeTree usages mstore) mm
+      pure $ MList ms' mm'
+    linearizeTree usages mstore (Indirection c) =
+      case Map.lookup c usages of
+        Just 1 -> do
+          lin usages mstore c
+          mstore' <- get
+          pure $ case Map.lookup c mstore' of
+            Just (mtree, _) -> mtree
+            Nothing -> Indirection c
+        _ -> pure $ Indirection c
+
+    linearizeAll :: Map Cell Int -> Map Cell (MTree, Credit) -> Map Cell (MTree, Credit)
+    linearizeAll usages mstore = Map.foldrWithKey (\k _ -> execState (lin usages mstore k)) Map.empty mstore
+
+    removeUniques :: Map Cell Int -> Map Cell (MTree, Credit) -> Map Cell (MTree, Credit)
+    removeUniques usages mstore = Map.filterWithKey (\c _ -> Map.findWithDefault 0 c usages > 1) mstore
+
+    linearize' :: Memory -> Map Cell Int -> Memory
+    linearize' (Memory mtree mstore) usages =
+      let mstore' = linearizeAll usages mstore
+          mtree' = evalState (linearizeTree usages mstore' mtree) mstore'
+      in Memory mtree' (removeUniques usages mstore')
+
+instance Pretty MTree where
+  pretty (MCell d []) = pretty d 
+  pretty (MCell d ms) = pretty d <> tupled (map pretty ms)
+  pretty (MList [] Nothing) = pretty "[]"
+  pretty (MList [] (Just m)) = pretty m
+  pretty (MList ms Nothing) = list (map pretty ms)
+  pretty (MList ms (Just m)) = tupled [list (map pretty ms) <+> pretty "++" <+> pretty m]
+  pretty (Indirection (Cell c)) = pretty "<" <> pretty c <> pretty ">"
+
+instance Pretty Memory where
+  pretty (Memory mtree mstore) =
+    let prettyStore = case Map.toList mstore of
+          [] -> mempty
+          _ -> pretty "where:" <+> align (vsep (map (\((Cell c), (m, cr)) -> pretty "<" <> pretty c <> pretty "> =>" <> pretty (showCredit cr) <+> pretty m) (Map.toList mstore)))
+    in pretty mtree <> line <> prettyStore
diff --git a/src/Control/Monad/Credit/CounterM.hs b/src/Control/Monad/Credit/CounterM.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Credit/CounterM.hs
@@ -0,0 +1,103 @@
+{-# LANGUAGE TypeFamilies, StandaloneDeriving, UndecidableInstances, OverloadedStrings, DerivingStrategies, MagicHash #-}
+
+module Control.Monad.Credit.CounterM (CounterM, runCounterM, CounterT, runCounterT) where
+
+import Prelude hiding (lookup)
+import Control.Monad.Except
+import Control.Monad.Identity
+import Control.Monad.State.Lazy
+import Control.Monad.ST.Trans
+
+import Control.Monad.Credit.Base
+
+-- Run computation in a state monad
+
+-- State of the computation
+-- credits: The total credits consumed so far
+newtype St = St Ticks
+  deriving (Eq, Ord, Show)
+
+-- | An instance of the counter monad using ST to memoize thunks.
+type CounterM s = CounterT s Identity
+
+-- | A monad transformer on the counter monad.
+-- Warning! This monad transformer includes the ST monad transformer and
+-- should not be used with monads that can contain multiple answers,
+-- like the list monad. Safe monads include the monads State, Reader, Writer,
+-- Maybe and combinations of their corresponding monad transformers.
+newtype CounterT s m a = CounterT { runT :: StateT St (ExceptT String (STT s m)) a }
+
+instance Functor m => Functor (CounterT s m) where
+  fmap f (CounterT m) = CounterT (fmap f m)
+
+instance Monad m => Applicative (CounterT s m) where
+  pure = CounterT . pure
+  CounterT f <*> CounterT x = CounterT (f <*> x)
+
+instance Monad m => Monad (CounterT s m) where
+  CounterT m >>= f = CounterT (m >>= runT . f)
+
+instance Monad m => MonadError String (CounterT s m) where
+  throwError e = CounterT (throwError e)
+  catchError (CounterT m) h = CounterT (catchError m (runT . h))
+
+instance Monad m => MonadState St (CounterT s m) where
+  get = CounterT get
+  put s = CounterT (put s)
+
+instance MonadTrans (CounterT s) where
+  lift = CounterT . lift . lift . lift
+
+liftST :: Monad m => STT s m a -> CounterT s m a
+liftST = CounterT . lift . lift
+
+instance Monad m => MonadFail (CounterT s m) where
+  fail e = throwError e
+
+instance Monad m => MonadCount (CounterT s m) where
+  tick = do
+    (St c) <- get
+    put (St (c + 1))
+
+instance Monad m => MonadLazy (CounterT s m) where
+  {-# SPECIALIZE instance MonadLazy (CounterT s Identity) #-}
+  {-# SPECIALIZE instance MonadLazy (CounterT s (State st)) #-}
+  data Thunk (CounterT s m) t b = Thunk !(STRef s (Either (t b) b))
+  delay a = do
+    s <- liftST $ newSTRef (Left a)
+    pure (Thunk s)
+  force (Thunk t) = do
+    t' <- liftST $ readSTRef t
+    case t' of
+      Left a -> do
+        b <- step a
+        liftST $ writeSTRef t (Right b)
+        pure b
+      Right b -> pure b
+  lazymatch (Thunk t) f g = do
+    t' <- liftST $ readSTRef t
+    case t' of
+      Right b -> f b
+      Left a -> g a
+
+instance Monad m => MonadCredit (CounterT s m) where
+  {-# SPECIALIZE instance MonadCredit (CounterT s Identity) #-}
+  {-# SPECIALIZE instance MonadCredit (CounterT s (State st)) #-}
+  creditWith _ _ = pure ()
+  hasAtLeast _ _ = pure ()
+
+instance Monad m => MonadInherit (CounterT s m) where
+  {-# SPECIALIZE instance MonadInherit (CounterT s Identity) #-}
+  {-# SPECIALIZE instance MonadInherit (CounterT s (State st)) #-}
+  creditAllTo _ = pure ()
+
+runStateT' :: Monad m => StateT St m a -> m (a, Ticks)
+runStateT' m = do
+  (a, St c) <- runStateT m $ St 0
+  pure (a, c)
+
+runCounterT :: Monad m => (forall s. CounterT s m a) -> m (Either String (a, Ticks))
+runCounterT m = runSTT $ runExceptT $ runStateT' $ runT m
+
+runCounterM :: (forall s. CounterM s a) -> Either String (a, Ticks)
+runCounterM m = runIdentity $ runSTT $ runExceptT $ runStateT' $ runT m
diff --git a/src/Control/Monad/Credit/CreditM.hs b/src/Control/Monad/Credit/CreditM.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Credit/CreditM.hs
@@ -0,0 +1,292 @@
+{-# LANGUAGE TypeFamilies, StandaloneDeriving, UndecidableInstances, OverloadedStrings, DerivingStrategies, MagicHash #-}
+
+module Control.Monad.Credit.CreditM (CreditM, Error(..), runCreditM, CreditT, runCreditT, resetCurrentThunk) where
+
+import Prelude hiding (lookup)
+import Control.Monad.Except
+import Control.Monad.Identity
+import Control.Monad.State.Lazy
+import Control.Monad.ST.Trans
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import GHC.Exts
+import Prettyprinter
+
+import Control.Monad.Credit.Base
+
+-- Errors
+
+data Error
+  = OutOfCredits Cell
+  | InvalidAccount Cell
+  | InvalidTick Cell
+  | ClosedCurrent Cell
+  | UserError String
+  | AssertionFailed Cell Credit Credit
+  deriving (Eq, Ord, Show)
+
+-- Each memory cell has an associated amount of credits
+-- Once it is evaluated, it chooses an heir to pass its credits on to
+
+data Account = Balance
+                 Int# -- ^ The amount of credits in the account
+                 Int# -- ^ The number of credits consumed so far
+             | Closed
+             | ClosedWithHeir {-# UNPACK #-} !Cell Int#
+  deriving (Eq, Ord, Show)
+
+newtype Credits = Credits (IntMap Account)
+  deriving (Eq, Ord, Show)
+
+open :: Cell -> Credits -> Credits
+open (Cell i) (Credits cm) = Credits (IntMap.insert i (Balance 0# 0#) cm)
+
+addCredit :: Cell -> Credit -> Credits -> Credits
+addCredit (Cell i) (Credit (I# n)) (Credits cm) = go i cm
+  where
+    go i cm =
+      case IntMap.lookup i cm of
+        Just (Balance avail burnt) -> Credits (IntMap.insert i (Balance (n +# avail) burnt) cm)
+        Just (ClosedWithHeir (Cell h) burnt) ->
+          case IntMap.lookup h cm of
+            Just (ClosedWithHeir (Cell h') burnt') -> -- path halving
+              go h' (IntMap.insert i (ClosedWithHeir (Cell h') (burnt +# burnt')) cm)
+            _ -> go h cm
+        Just Closed -> Credits cm
+        Nothing -> Credits cm
+
+subCredit :: MonadError Error m => Cell -> Credit -> Credits -> m Credits
+subCredit (Cell i) (Credit (I# n)) (Credits cm) = go i cm
+  where
+    go i cm = case IntMap.lookup i cm of
+      Just (Balance avail burnt) ->
+        if isTrue# $ avail -# n <# 0#
+          then throwError (OutOfCredits (Cell i))
+          else pure (Credits (IntMap.insert i (Balance (avail -# n) (burnt +# n)) cm))
+      Just (ClosedWithHeir (Cell h) _) -> go h cm
+      Just Closed -> throwError (InvalidTick (Cell i))
+      Nothing -> throwError (InvalidTick (Cell i))
+
+-- | Close an account
+close :: MonadError Error m => Cell -> Credits -> m Credits
+close (Cell i) (Credits cm) = do
+  case IntMap.lookup i cm of
+    Just (Balance _ _) -> pure $ Credits $ IntMap.insert i Closed cm
+    Just Closed -> pure $ Credits cm
+    Just (ClosedWithHeir _ _) -> pure $ Credits cm
+    Nothing -> throwError (InvalidAccount (Cell i))
+
+-- | Close an account and transfer its credits to the heir.
+closeWithHeir :: MonadError Error m => Cell -> Cell -> Credits -> m Credits
+closeWithHeir (Cell i) h c = do
+  (n, burnt) <- extractValue c
+  pure $ closeAccount burnt $ addCredit h n c
+  where
+    closeAccount (I# burnt) (Credits cm) = Credits $ IntMap.insert i (ClosedWithHeir h burnt) cm
+
+    extractValue (Credits cm) =
+      case IntMap.findWithDefault (Balance 0# 0#) i cm of
+        Balance a b -> pure (Credit (I# a), I# b)
+        ClosedWithHeir _ _ -> throwError (InvalidAccount (Cell i))
+        Closed -> throwError (InvalidAccount (Cell i))
+
+singleton :: Cell -> Credit -> Credits
+singleton (Cell i) (Credit (I# n)) = Credits (IntMap.singleton i (Balance n 0#))
+
+-- Run computation in a state monad
+
+-- State of the computation
+-- me: The currently evaluated cell
+-- credits: The credits of each cell
+-- next: The next free cell to be allocated
+data St = St {-# UNPACK #-} !Cell !Credits {-# UNPACK #-} !Int 
+  deriving (Eq, Ord, Show)
+
+-- | An instance of the credit monad using ST to memoize thunks.
+type CreditM s = CreditT s Identity
+
+-- | A monad transformer on the credit monad.
+-- Warning! This monad transformer includes the ST monad transformer and
+-- should not be used with monads that can contain multiple answers,
+-- like the list monad. Safe monads include the monads State, Reader, Writer,
+-- Maybe and combinations of their corresponding monad transformers.
+newtype CreditT s m a = CreditT { runT :: ExceptT Error (StateT St (STT s m)) a }
+
+instance Functor m => Functor (CreditT s m) where
+  fmap f (CreditT m) = CreditT (fmap f m)
+
+instance Monad m => Applicative (CreditT s m) where
+  pure = CreditT . pure
+  CreditT f <*> CreditT x = CreditT (f <*> x)
+
+instance Monad m => Monad (CreditT s m) where
+  CreditT m >>= f = CreditT (m >>= runT . f)
+
+instance Monad m => MonadError Error (CreditT s m) where
+  throwError e = CreditT (throwError e)
+  catchError (CreditT m) h = CreditT (catchError m (runT . h))
+
+instance Monad m => MonadState St (CreditT s m) where
+  get = CreditT get
+  put s = CreditT (put s)
+
+instance MonadTrans (CreditT s) where
+  lift = CreditT . lift . lift . lift
+
+liftST :: Monad m => STT s m a -> CreditT s m a
+liftST = CreditT . lift . lift
+
+getMe :: Monad m => CreditT s m Cell
+getMe = do
+  St me _ _ <- get
+  pure me
+
+getNext :: Monad m => CreditT s m Cell
+getNext = do
+  St _ _ nxt <- get
+  modify' $ \(St me c _) -> St me c (nxt + 1)
+  pure $ Cell nxt
+
+withCredits :: Monad m => (Credits -> CreditT s m Credits) -> CreditT s m ()
+withCredits f = do
+  St _ c _ <- get
+  c' <- f c
+  modify' $ \(St me _ nxt) -> St me c' nxt
+
+instance Monad m => MonadFail (CreditT s m) where
+  fail e = throwError (UserError e)
+
+instance Monad m => MonadCount (CreditT s m) where
+  tick = do
+    me <- getMe
+    withCredits $ subCredit me 1
+
+instance Monad m => MonadLazy (CreditT s m) where
+  {-# SPECIALIZE instance MonadLazy (CreditT s Identity) #-}
+  {-# SPECIALIZE instance MonadLazy (CreditT s (State st)) #-}
+  data Thunk (CreditT s m) t b = Thunk !Cell !(STRef s (Either (t b) b))
+  delay a = do
+    i <- getNext
+    withCredits $ pure . open i
+    s <- liftST $ newSTRef (Left a)
+    pure (Thunk i s)
+  force (Thunk i t) = do
+    t' <- liftST $ readSTRef t
+    case t' of
+      Left a -> do  -- [step] rule in the big-step semantics of the paper
+        St me _ _ <- get
+        modify' $ \(St _ c nxt) -> St i c nxt
+        b <- step a
+        modify' $ \(St _ c nxt) -> St me c nxt
+        liftST $ writeSTRef t (Right b)
+        withCredits $ close i
+        pure b
+      Right b -> pure b
+  lazymatch (Thunk _ t) f g = do
+    t' <- liftST $ readSTRef t
+    case t' of
+      Right b -> f b
+      Left a -> g a
+
+assertAtLeast :: Monad m => Cell -> Credit -> CreditT s m ()
+assertAtLeast (Cell i) n = do
+  St _ (Credits cm) _ <- get
+  case IntMap.lookup i cm of
+    Just (Balance m' _) -> do
+      let m = Credit (I# m')
+      if m >= n
+        then pure ()
+        else throwError (AssertionFailed (Cell i) n m)
+    Just Closed -> pure ()
+    Just (ClosedWithHeir i burnt) ->
+      assertAtLeast i (n - Credit (I# burnt))
+    Nothing -> throwError (InvalidAccount (Cell i))
+
+instance Monad m => MonadCredit (CreditT s m) where
+  {-# SPECIALIZE instance MonadCredit (CreditT s Identity) #-}
+  {-# SPECIALIZE instance MonadCredit (CreditT s (State st)) #-}
+  creditWith (Thunk i _) n =
+    if n > 0 then do
+      me <- getMe
+      withCredits $ subCredit me n . addCredit i n
+    else pure ()
+  hasAtLeast (Thunk i _) n =
+    assertAtLeast i n
+
+instance Monad m => MonadInherit (CreditT s m) where
+  {-# SPECIALIZE instance MonadInherit (CreditT s Identity) #-}
+  {-# SPECIALIZE instance MonadInherit (CreditT s (State st)) #-}
+  creditAllTo (Thunk i _) = do
+    me <- getMe
+    withCredits $ me `closeWithHeir` i
+
+emptyState :: Credit -> St
+emptyState n = St (Cell 0) (singleton (Cell 0) n) 1
+
+runCreditT :: Monad m => Credit -> (forall s. CreditT s m a) -> m (Either Error a)
+runCreditT n m = runSTT $ evalStateT (runExceptT (runT m)) (emptyState n)
+
+runCreditM :: Credit -> (forall s. CreditM s a) -> Either Error a
+runCreditM n m = runIdentity $ runSTT $ evalStateT (runExceptT (runT m)) (emptyState n)
+
+{-# SPECIALIZE resetCurrentThunk :: Credit -> CreditT s Identity () #-}
+{-# SPECIALIZE resetCurrentThunk :: Credit -> CreditT s (State st) () #-}
+resetCurrentThunk :: Monad m => Credit -> CreditT s m ()
+resetCurrentThunk (Credit (I# n)) = do
+  (Cell me) <- getMe
+  withCredits $ \(Credits c) -> do
+    case IntMap.lookup me c of
+      Just (Balance m b) -> pure $ Credits $ IntMap.insert me (Balance (n +# m) b) c
+      _ -> throwError $ ClosedCurrent (Cell me)
+
+-- Pretty Printing
+
+getCredit :: Monad m => Cell -> CreditT s m Credit
+getCredit (Cell i) = do
+  St _ (Credits cm) _ <- get
+  case IntMap.lookup i cm of
+    Just (Balance n _) -> pure $ Credit (I# n)
+    _ -> pure 0
+
+instance (Monad m) => MonadMemory (CreditT s m) where
+  {-# SPECIALIZE instance MonadMemory (CreditT s Identity) #-}
+  {-# SPECIALIZE instance MonadMemory (CreditT s (State st)) #-}
+  prettyThunk (Thunk c s) = do
+    e <- liftST $ readSTRef s
+    (Memory mtree mstore) <- case e of
+      Left a -> prettyCell a
+      Right b -> prettyCell b
+    cr <- getCredit c
+    pure $ Memory (Indirection c) (Map.insert c (mtree, cr) mstore)
+
+instance Pretty Error where
+  pretty (OutOfCredits i) = "Out of credits for" <+> pretty i
+  pretty (InvalidAccount i) = "Invalid account for" <+> pretty i
+  pretty (InvalidTick i) = "Invalid tick for" <+> pretty i
+  pretty (ClosedCurrent (Cell 0)) = "Closed maint thread account. Never invoke creditAllTo on main thread."
+  pretty (ClosedCurrent i) = "Closed current account" <+> pretty i
+  pretty (UserError e) = "User error:" <+> pretty e
+  pretty (AssertionFailed i n m) = pretty i <+> "should have" <+> pretty n <+> "credits but only has" <+> pretty m
+
+instance Pretty a => Pretty (Either Error a) where
+  pretty (Left e) = pretty e
+  pretty (Right a) = pretty a
+
+instance Pretty Account where
+  pretty (Balance n _) = pretty (I# n)
+  pretty Closed = "closed"
+  pretty (ClosedWithHeir h _) = "closed with heir" <+> pretty h
+
+instance Pretty Credits where
+  pretty (Credits cm) = vsep $ map prettyPair (IntMap.toList cm)
+    where
+      prettyPair (i, a) = pretty i <+> "->" <+> pretty a
+
+instance Pretty St where
+  pretty (St me c nxt) = vsep
+    [ "me:" <+> pretty me
+    , "credits:" <+> pretty c
+    , "next:" <+> pretty nxt
+    ]
diff --git a/src/Test/Credit.hs b/src/Test/Credit.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit.hs
@@ -0,0 +1,180 @@
+{-# LANGUAGE DerivingStrategies, FunctionalDependencies, AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables #-}
+
+module Test.Credit
+  (
+  -- * Common time-complexity functions
+    Size, logstar, log2, linear
+  -- * Tree shapes for testing
+  , Strategy(..), genTree
+  -- * Testing data structures on trees of operations
+  , DataStructure(..), runTree, checkCredits, runTreeMemory, checkCreditsMemory
+  ) where
+
+import Data.Either
+import Control.Monad.State
+import Data.Tree
+import Test.QuickCheck
+import Prettyprinter
+import Prettyprinter.Render.String
+
+import Control.Monad.Credit.Base
+import Control.Monad.Credit.CreditM
+
+path :: Arbitrary a => Int -> Tree a -> Gen (Tree a)
+path 0 end = pure end
+path n end = Node <$> arbitrary <*> ((:[]) <$> path (n-1) end)
+
+path' :: Arbitrary a => Int -> Gen (Tree a)
+path' n = path n =<< Node <$> arbitrary <*> pure []
+
+bloom :: Arbitrary a => Gen (Tree a)
+bloom = sized $ \n -> do
+  m <- chooseInt (0, n)
+  k <- chooseInt (0, m `div` 2)
+  ts <- mapM (\_ -> path' (m `div` k)) [1..k]
+  path (n - m) =<< Node <$> arbitrary <*> pure ts
+
+pennant :: Arbitrary a => Gen (Tree a)
+pennant = sized go
+  where
+    go n | n <= 1 = path' 0
+    go n = do
+      k <- chooseInt (n `div` 3, 2 * (n `div` 3))
+      ts <- mapM (\_ -> go ((n - k - 1) `div` 2)) [1..2]
+      path k =<< Node <$> arbitrary <*> pure ts
+
+newtype SeqTree a = SeqTree { fromSeqTree :: Tree a }
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (SeqTree a) where
+  arbitrary = sized $ \n -> SeqTree <$> path' n
+
+newtype BloomTree a = BloomTree { fromBloomTree :: Tree a }
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (BloomTree a) where
+  arbitrary = BloomTree <$> bloom
+
+newtype PennantTree a = PennantTree { fromPennantTree :: Tree a }
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (PennantTree a) where
+  arbitrary = PennantTree <$> pennant
+
+newtype PrsTree a = PrsTree { fromPrsTree :: Tree a }
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (PrsTree a) where
+  arbitrary = PrsTree <$> arbitrary
+
+data Strategy = Path | Bloom | Pennant | Random
+  deriving (Eq, Ord, Show)
+
+genTree :: Arbitrary op => Strategy -> Gen (Tree op)
+genTree Path = fromSeqTree <$> arbitrary
+genTree Bloom = fromBloomTree <$> arbitrary
+genTree Pennant = fromPennantTree <$> arbitrary
+genTree Random = fromPrsTree <$> arbitrary
+
+newtype Size = Size Int
+  deriving (Eq, Ord, Show)
+  deriving newtype (Num, Enum, Real, Integral, Pretty)
+
+instance Monad m => MemoryCell m Size where
+  prettyCell (Size i) = pure $ mkMCell (show i) []
+
+logstar :: Size -> Credit
+logstar (Size n) = fromInteger $ go n 0
+  where
+    go n acc | n < 2 = acc
+    go n acc = go (log2 n 0) (acc + 1)
+
+    log2 n acc | n < 2 = acc
+    log2 n acc = log2 (n `div` 2) (acc + 1)
+
+log2 :: Size -> Credit
+log2 (Size n) = fromInteger $ go n 0
+  where
+    go n acc | n < 2 = acc
+    go n acc = go (n `div` 2) (acc + 1)
+
+linear :: Size -> Credit
+linear (Size n) = fromInteger $ toInteger n
+
+class (Arbitrary op, Show op) => DataStructure t op | t -> op where
+  create :: forall m. MonadInherit m => t m
+  action :: forall m. MonadInherit m => t m -> op -> (Credit, m (t m))
+
+runTree :: forall t op. DataStructure t op => Tree op -> Either Error ()
+runTree tree = runCreditM 0 (go (create @t) tree)
+  where
+    go :: forall s t op. DataStructure t op => t (CreditM s) -> Tree op -> CreditM s ()
+    go a (Node op ts) = do
+      let (cr, f) = action a op
+      resetCurrentThunk cr
+      a' <- f
+      mapM_ (go a') ts
+
+isPersistent :: Tree a -> Bool
+isPersistent (Node _ ts) = length ts > 1 || any isPersistent ts
+
+-- | Evaluate the queue operations using the given strategy on the given queue
+-- Reports only if evaluation succeeded.
+checkCredits :: forall t op. DataStructure t op => Strategy -> Property
+checkCredits strat =
+  forAllShrink (genTree strat) shrink $ \t ->
+    classify (isPersistent t) "persistent" $
+      isRight $ runTree @t t
+
+data RoseZipper a = Root | Branch a [Tree a] (RoseZipper a)
+  deriving (Eq, Ord, Show)
+
+up :: RoseZipper a -> RoseZipper a
+up (Branch x ls (Branch y rs z)) = Branch y (Node x (reverse ls) : rs) z
+up z = z
+
+extend :: String -> RoseZipper String -> RoseZipper String
+extend s (Branch x ls z) = Branch (x ++ s) ls z
+extend _ Root = Root
+
+extract :: RoseZipper a -> Tree a
+extract (Branch x ls Root) = Node x (reverse ls)
+extract z = extract (up z)
+
+flattenTree :: Tree a -> Tree a
+flattenTree t = case go t of
+  Just (x:xs) -> Node x (map (\x -> Node x []) xs)
+  _ -> t
+  where
+    go (Node x []) = Just [x]
+    go (Node x [t]) = (x :) <$> go t
+    go (Node _ _) = Nothing
+
+showState :: (Either Error (), RoseZipper String) -> String
+showState (Left e, t) = drawTree $ flattenTree $ extract $ extend (show $ pretty e) t
+showState (Right (), t) = drawTree $ flattenTree $ extract t
+
+type M s = CreditT s (State (RoseZipper String))
+
+runTreeMemory :: forall t op. (MemoryStructure t, DataStructure t op) => Tree op -> String
+runTreeMemory tree = showState $ runState (runCreditT 0 (go (create @t) tree)) Root
+  where
+    go :: forall s t op. (MemoryStructure t, DataStructure t op) => t (M s) -> Tree op -> M s ()
+    go a (Node op ts) = do
+      let (cr, f) = action a op
+      resetCurrentThunk cr
+      lift $ modify' (Branch (show op ++ ": ") []) 
+      a' <- f
+      mem <- prettyStructure a'
+      let s = renderString $ layoutSmart (defaultLayoutOptions { layoutPageWidth = Unbounded }) $ nest 2 $ pretty $ mem
+      lift $ modify' (extend s)
+      mapM_ (go a') ts
+      lift $ modify' up
+
+-- | Evaluate the queue operations using the given strategy on the given queue
+-- Reports only if evaluation succeeded.
+checkCreditsMemory :: forall t op. (MemoryStructure t, DataStructure t op) => Strategy -> Property
+checkCreditsMemory strat =
+  forAllShrinkShow (genTree strat) shrink (\t -> runTreeMemory @t t) $ \t ->
+    classify (isPersistent t) "persistent" $
+      isRight $ runTree @t t
diff --git a/src/Test/Credit/Deque/Bankers.hs b/src/Test/Credit/Deque/Bankers.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Deque/Bankers.hs
@@ -0,0 +1,95 @@
+module Test.Credit.Deque.Bankers where
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Deque.Base
+import Test.Credit.Deque.Streams
+
+-- | Delay a computation, but do not consume any credits
+indirect :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)
+indirect t = delay t >>= pure . SIndirect
+
+data BDeque a m = BDeque
+  { front :: Stream m a
+  , lenf :: !Int
+  , ghostf :: Stream m a
+  , rear :: Stream m a
+  , lenr :: !Int
+  , ghostr :: Stream m a
+  }
+
+isEmpty :: BDeque a m -> Bool
+isEmpty (BDeque _ 0 _ _ 0 _) = True
+isEmpty (BDeque _ _ _ _ _ _) = False
+
+size :: BDeque a m -> Int
+size (BDeque _ lenf _ _ lenr _) = lenf + lenr
+
+-- Rough proof sketch:
+-- After rebalancing, the front and rear streams have at most lenf + lenr debits.
+-- Need (c - 1) * n/2 cons operations before rebalance, which means we have to
+-- pay off 2 / (c - 1) debits on each stream per cons operation.
+-- Need (c - 1) / c * n/2 uncons operations before rebalance, which means we have to
+-- pay off at least 2*c / (c - 1) debits on each stream per uncons operation
+-- (but also at least (c + 1) debits to be able to force on element).
+-- Not sure if the analysis above works for c < 3
+
+bdeque :: MonadInherit m => BDeque a m -> m (BDeque a m)
+bdeque (BDeque f lenf gf r lenr gr)
+  | lenf > c * lenr + 1 = do
+    let i = (lenf + lenr) `div` 2
+    let j = lenf + lenr - i
+    f' <- indirect (STake i f)
+    f'' <- indirect (SRevDrop i f SNil)
+    credit (fromIntegral c) f'' >> eval (fromIntegral c) f''
+    r' <- indirect (SAppend r f'')
+    credit 1 r'
+    pure $ BDeque f' i f' r' j r'
+  | lenr > c * lenf + 1 = do
+    let j = (lenf + lenr) `div` 2
+    let i = lenf + lenr - j
+    r' <- indirect (STake j r)
+    r'' <- indirect (SRevDrop j r SNil)
+    credit (fromIntegral c) r'' >> eval (fromIntegral c) r''
+    f' <- indirect (SAppend f r'')
+    credit 1 f'
+    pure $ BDeque f' i f' r' j r'
+  | otherwise =
+    pure $ BDeque f lenf gf r lenr gr
+
+instance Deque BDeque where
+  empty = pure $ BDeque SNil 0 SNil SNil 0 SNil
+  cons x (BDeque f fl gf r rl gr) = credit 1 gf >> credit 1 gr >>
+    bdeque (BDeque (SCons x f) (fl + 1) gf r rl gr)
+  snoc (BDeque f fl gf r rl gr) x = credit 1 gf >> credit 1 gr >>
+    bdeque (BDeque f fl gf (SCons x r) (rl + 1) gr)
+  uncons (BDeque f fl gf r rl gr) = credit (fromIntegral c + 1) gf >> credit (fromIntegral c + 1) gr >> smatch f
+    (\x f -> bdeque (BDeque f (fl - 1) gf r rl gr) >>= \q -> pure $ Just (x, q))
+    (smatch r
+      (\x _ -> empty >>= \q -> pure $ Just (x, q))
+      (pure Nothing))
+  unsnoc (BDeque f fl gf r rl gr) = credit (fromIntegral c + 1) gr >> credit (fromIntegral c + 1) gf >> smatch r
+    (\x r -> bdeque (BDeque f fl gf r (rl - 1) gr) >>= \q -> pure $ Just (q, x))
+    (smatch f
+      (\x _ -> empty >>= \q -> pure $ Just (q, x))
+      (pure Nothing))
+  concat = undefined
+
+instance BoundedDeque BDeque where
+  qcost _ (Cons _) = fromIntegral c + 3
+  qcost _ (Snoc _) = fromIntegral c + 3
+  qcost _ Uncons = 3 * fromIntegral c + 4
+  qcost _ Unsnoc = 3 * fromIntegral c + 4
+  qcost _ Concat = 0
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BDeque a m) where
+  prettyCell (BDeque f fl _ r rl _) = do
+    f' <- prettyCell f
+    fl' <- prettyCell fl
+    r' <- prettyCell r
+    rl' <- prettyCell rl
+    pure $ mkMCell "BDeque" [f', fl', r', rl']
+
+instance Pretty a => MemoryStructure (BDeque (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Deque/Base.hs b/src/Test/Credit/Deque/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Deque/Base.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}
+
+module Test.Credit.Deque.Base (DequeOp(..), Deque(..), BoundedDeque(..), D, BD) where
+
+import Prelude hiding (concat)
+import Control.Monad.Credit
+import Test.Credit
+import Test.QuickCheck
+
+data DequeOp a = Cons a | Snoc a | Uncons | Unsnoc | Concat
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (DequeOp a) where
+  arbitrary = frequency
+    [ (7, Cons <$> arbitrary)
+    , (4, Snoc <$> arbitrary)
+    , (2, pure Uncons)
+    , (6, pure Unsnoc)
+    , (1, pure Concat)
+    ]
+
+class Deque q where
+  empty :: MonadInherit m => m (q a m)
+  cons :: MonadInherit m => a -> q a m -> m (q a m)
+  snoc :: MonadInherit m => q a m -> a -> m (q a m)
+  uncons :: MonadInherit m => q a m -> m (Maybe (a, q a m))
+  unsnoc :: MonadInherit m => q a m -> m (Maybe (q a m, a))
+  concat :: MonadInherit m => q a m -> q a m -> m (q a m)
+
+class Deque q => BoundedDeque q where
+  qcost :: Size -> DequeOp a -> Credit
+
+data D q a m = E | D Size (q (PrettyCell a) m)
+
+instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (D q a m) where
+  prettyCell E = pure $ mkMCell "" []
+  prettyCell (D _ q) = prettyCell q
+
+instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (D q a) where
+  prettyStructure E = pure $ mkMCell "" []
+  prettyStructure (D _ q) = prettyStructure q
+
+act :: (MonadInherit m, Deque q) => Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)
+act sz q (Cons x) = D (sz + 1) <$> cons (PrettyCell x) q
+act sz q (Snoc x) = D (sz + 1) <$> snoc q (PrettyCell x)
+act sz q Uncons = do
+  m <- uncons q
+  case m of
+    Nothing -> pure E
+    Just (_, q') -> pure $ D (max 0 (sz - 1)) q'
+act sz q Unsnoc = do
+  m <- unsnoc q
+  case m of
+    Nothing -> pure E
+    Just (q', _) -> pure $ D (max 0 (sz - 1)) q'
+act sz q Concat = pure $ D sz q
+
+instance (Arbitrary a, BoundedDeque q, Show a) => DataStructure (D q a) (DequeOp a) where
+  create = E
+  action E op = (qcost @q 0 op, empty >>= flip (act 0) op)
+  action (D sz q) op = (qcost @q sz op, act sz q op)
+
+size :: D q a m -> Size
+size E = 0
+size (D sz _) = sz
+
+data BD q a m = BD (D q a m) (D q a m)
+
+instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (BD q a m) where
+  prettyCell (BD q1 q2) = do
+    q1' <- prettyCell q1
+    q2' <- prettyCell q2
+    pure $ mkMCell "Concat" [q1', q2']
+
+instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (BD q a) where
+  prettyStructure (BD q1 q2) = do
+    q1' <- prettyStructure q1
+    q2' <- prettyStructure q2
+    pure $ mkMCell "Concat" [q1', q2']
+
+act1 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)
+act1 op (BD q1 q2) = do
+  q1' <- case q1 of
+    E -> empty
+    D _ q -> pure q
+  q1'' <- act (size q1) q1' op 
+  pure $ BD q1'' q2
+
+act2 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)
+act2 op (BD q1 q2) = do
+  let sz = size q2
+  q2' <- case q2 of
+    E -> empty
+    D _ q -> pure q
+  q2'' <- act (size q2) q2' op 
+  pure $ BD q1 q2''
+
+concatenate :: (MonadInherit m, Deque q) => D q a m -> D q a m -> m (D q a m)
+concatenate E E = pure E
+concatenate (D sz1 q1) E = pure $ D sz1 q1
+concatenate E (D sz2 q2) = pure $ D sz2 q2
+concatenate (D sz1 q1) (D sz2 q2) = D (sz1 + sz2) <$> concat q1 q2
+
+instance (Arbitrary a, BoundedDeque q, Show a) => DataStructure (BD q a) (DequeOp a) where
+  create = BD E E
+  action (BD q1 q2) (Cons x) = (qcost @q (size q1) (Cons x), act1 (Cons x) (BD q1 q2))
+  action (BD q1 q2) (Snoc x) = (qcost @q (size q2) (Snoc x), act2 (Snoc x) (BD q1 q2))
+  action (BD q1 q2) Uncons = (qcost @q (size q1) Uncons, act1 Uncons (BD q1 q2))
+  action (BD q1 q2) Unsnoc = (qcost @q (size q2) Unsnoc, act2 Unsnoc (BD q1 q2))
+  action (BD q1 q2) Concat = (qcost @q (size q1 + size q2) Concat, BD E <$> concatenate q1 q2)
diff --git a/src/Test/Credit/Deque/Catenable.hs b/src/Test/Credit/Deque/Catenable.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Deque/Catenable.hs
@@ -0,0 +1,135 @@
+{-# LANGUAGE GADTs, LambdaCase #-}
+
+module Test.Credit.Deque.Catenable where
+
+import Prelude hiding (concat)
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit.Deque.Base
+import qualified Test.Credit.Queue.Base as Q
+import qualified Test.Credit.Queue.Bankers as Q
+
+-- | A rose tree where the elements are pre-ordered
+data CatDeque a m
+  = E
+  | C a -- ^ head
+      (Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m) -- ^ tail
+
+data CLazyCon m a where
+  Pure :: a -> CLazyCon m a
+  LinkAll :: Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m -> CLazyCon m (CatDeque a m)
+
+instance MonadInherit m => HasStep (CLazyCon m) m where
+  step (Pure xs) = pure xs
+  step (LinkAll q) = linkAll q
+
+costSnoc :: Credit
+costSnoc = Q.qcost @(Q.BQueue) undefined (Q.Snoc undefined)
+
+costUncons :: Credit
+costUncons = Q.qcost @(Q.BQueue) undefined (Q.Uncons)
+
+link :: MonadInherit m => CatDeque a m -> Thunk m (CLazyCon m) (CatDeque a m) -> m (CatDeque a m)
+link (C x q) s = C x <$> Q.snoc q s
+
+linkAll :: MonadInherit m => Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m -> m (CatDeque a m)
+linkAll q = do
+  m <- Q.uncons q
+  case m of
+    Nothing -> fail "linkAll: empty queue"
+    Just (t, q') -> do
+      t <- force t
+      if Q.isEmpty q' then pure t
+      else do
+        s <- delay $ LinkAll q'
+        creditWith s costUncons -- for the last uncons
+        link t s
+
+concat' :: MonadInherit m => CatDeque a m -> CatDeque a m -> m (CatDeque a m)
+concat' E xs = pure xs
+concat' xs E = pure xs
+concat' xs ys = do
+  ys <- delay $ Pure ys
+  link xs ys
+
+-- | Assign credits to the thunk and force it
+-- unless it is a `LinkAll(t:_)` where `t` requires credits.
+-- In the latter case, recursive until we can force a thunk.
+dischargeThunk :: MonadInherit m => Thunk m (CLazyCon m) (CatDeque a m) -> m ()
+dischargeThunk s = do
+  let assign = creditWith s (costSnoc + costUncons) >> force s >> pure ()
+  lazymatch s (\_ -> assign) $ \case
+    Pure _ -> assign
+    LinkAll q -> do
+      q' <- Q.lazyqueue q
+      case q' of
+        [] -> assign
+        t' : _ -> do
+          lazymatch t' (\_ -> assign) $ \case
+            Pure _ -> assign
+            LinkAll _ -> dischargeThunk t'
+
+findFirstThunk :: MonadInherit m => CatDeque a m -> m (Maybe (Thunk m (CLazyCon m) (CatDeque a m)))
+findFirstThunk (C _ q) = do
+  q' <- Q.lazyqueue q
+  seekFirstThunk q'
+findFirstThunk _ = pure Nothing
+
+seekFirstThunk :: MonadInherit m => [Thunk m (CLazyCon m) (CatDeque a m)] -> m (Maybe (Thunk m (CLazyCon m) (CatDeque a m)))
+seekFirstThunk [] = pure Nothing
+seekFirstThunk (t : q) = do
+  mt <- lazymatch t findFirstThunk $ \case
+    Pure q' -> findFirstThunk q'
+    LinkAll _ -> pure $ Just t
+  case mt of
+    Nothing -> seekFirstThunk q
+    Just t' -> pure $ Just t'
+
+dischargeFirst :: MonadInherit m => CatDeque a m -> m ()
+dischargeFirst q = do
+  mt <- findFirstThunk q
+  case mt of
+    Nothing -> pure ()
+    Just t -> dischargeThunk t
+
+instance Deque CatDeque where
+  empty = pure E
+  cons x q = do
+    e <- Q.empty
+    concat (C x e) q
+  snoc q x = do
+    e <- Q.empty
+    concat q (C x e)
+  uncons E = pure Nothing
+  uncons (C x q) = do
+    q' <- if Q.isEmpty q then pure E else linkAll q
+    dischargeFirst q'
+    dischargeFirst q'
+    pure $ Just (x, q')
+  unsnoc q = pure $ Just (q, undefined)
+  concat = concat'
+
+instance BoundedDeque CatDeque where
+  qcost _ (Cons _) = costSnoc
+  qcost _ (Snoc _) = costSnoc
+  qcost _ Uncons = 4 * costUncons + 3 * costSnoc
+  qcost _ Unsnoc = 0
+  qcost _ Concat = 0
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (CLazyCon m a) where
+  prettyCell (Pure x) = do
+    x' <- prettyCell x
+    pure $ mkMCell "Pure" [x']
+  prettyCell (LinkAll q) = do
+    q' <- prettyCell q
+    pure $ mkMCell "LinkAll" [q']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (CatDeque a m) where
+  prettyCell E = pure $ mkMCell "E" []
+  prettyCell (C x q) = do
+    x' <- prettyCell x
+    q' <- prettyCell q
+    pure $ mkMCell "C" [x', q']
+
+instance Pretty a => MemoryStructure (CatDeque (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Deque/ImplicitCat.hs b/src/Test/Credit/Deque/ImplicitCat.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Deque/ImplicitCat.hs
@@ -0,0 +1,404 @@
+module Test.Credit.Deque.ImplicitCat where
+
+import Prelude hiding (head, tail, concat)
+import Control.Monad (join, when)
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Deque.Base
+import qualified Test.Credit.Deque.Base as D
+import qualified Test.Credit.Deque.Bankers as D
+
+data ImplicitCat a m
+  = Shallow (D.BDeque a m)
+  | Deep (D.BDeque a m) -- ^ (>= 3 elements)
+         (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
+         (D.BDeque a m) -- ^ (>= 2 elements)
+         (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
+         (D.BDeque a m) -- ^ (>= 3 elements)
+
+data ILazyCon m a where
+  IPay :: (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)) -> m b -> ILazyCon m b
+  ILazy :: m a -> ILazyCon m a
+
+instance MonadCredit m => HasStep (ILazyCon m) m where
+  step (IPay _ m) = m
+  step (ILazy m) = m
+
+data CmpdElem a m
+  = Simple (D.BDeque a m)
+  | Cmpd (D.BDeque a m) -- ^ (>= 2 elements)
+         (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
+         (D.BDeque a m) -- ^ (>= 2 elements)
+
+-- The O(1) unshared cost of operations
+-- Each thunk in the program requires at most 5 * cost credits to run
+-- except for the thunks returned by uncons/unsnoc which require
+-- 6 * cost credits to run.
+cost :: Credit
+cost = 3 * (qcost @(D.BDeque) undefined (Cons undefined) + qcost @(D.BDeque) undefined Uncons)
+
+deepDanger :: D.BDeque a m -> Credit
+deepDanger d = if D.size d == 3 then cost else 0
+
+deep :: MonadCredit m
+     => D.BDeque a m
+     -> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
+     -> D.BDeque a m
+     -> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
+     -> D.BDeque a m
+     -> m (ImplicitCat a m)
+deep f a m b r = do
+  -- a `hasAtLeast` (4 * deepDanger f + deepDanger r)
+  -- b `hasAtLeast` (deepDanger f + 4 * deepDanger r)
+  pure $ Deep f a m b r
+
+icreditWith :: MonadCredit m => Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
+icreditWith t c = do
+  lazymatch t (\_ -> pure ()) $ \t'' -> case t'' of
+    ILazy _ ->   t  `creditWith` c
+    IPay t' _ -> t' `creditWith` c
+
+cmpdDanger :: D.BDeque a m -> Credit
+cmpdDanger d = if D.size d == 2 then cost else 0
+
+cmpd :: MonadCredit m
+     => D.BDeque a m
+     -> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
+     -> D.BDeque a m
+     -> m (CmpdElem a m)
+cmpd f c r = pure $ Cmpd f c r
+
+isEmpty :: ImplicitCat a m -> Bool
+isEmpty (Shallow d) = D.isEmpty d
+isEmpty (Deep _ _ _ _ _) = False
+
+share :: MonadInherit m => D.BDeque a m -> D.BDeque a m -> m (D.BDeque a m, D.BDeque a m, D.BDeque a m)
+share f r = do
+  fu <- D.unsnoc f
+  ru <- D.uncons r
+  case (fu, ru) of
+    (Just (fi, fl), Just (rh, rt)) -> do
+      m <- D.cons fl =<< D.cons rh =<< D.empty
+      pure $ (fi, m, rt)
+    _ -> fail "share: empty deque"
+
+dappendL :: MonadInherit m => D.BDeque a m -> D.BDeque a m -> m (D.BDeque a m)
+dappendL d1 d2 = do
+  d1' <- D.unsnoc d1
+  case d1' of
+    Nothing -> pure d2
+    Just (d1i, d1l) -> dappendL d1i =<< D.cons d1l d2
+
+dappendR :: MonadInherit m => D.BDeque a m -> D.BDeque a m -> m (D.BDeque a m)
+dappendR d1 d2 = do
+  d2' <- D.uncons d2
+  case d2' of
+    Nothing -> pure d1
+    Just (d2h, d2t) -> join $ dappendR <$> D.snoc d1 d2h <*> pure d2t
+
+-- 5 * cost
+concat' :: MonadInherit m => ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
+concat' (Shallow d1) (Shallow d2) = do
+  if D.size d1 < 4 then Shallow <$> dappendL d1 d2
+  else if D.size d2 < 4 then Shallow <$> dappendR d1 d2
+  else do
+    (f, m, r) <- share d1 d2
+    e <- delay $ ILazy $ empty
+    deep f e m e r
+concat' (Shallow d) (Deep f a m b r) = do
+  if D.size d < 4 then do
+    df <- dappendL d f
+    deep df a m b r
+  else do
+    fa <- delay $ ILazy $ do
+      a `icreditWith` (5 * cost)
+      cons (Simple f) =<< force a
+    fa `icreditWith` cost
+    fa `icreditWith` (deepDanger r)
+    deep d fa m b r
+concat' (Deep f a m b r) (Shallow d) = do
+  if D.size d < 4 then do
+    rd <- dappendR r d
+    deep f a m b rd
+  else do
+    br <- delay $ ILazy $ do
+      b `icreditWith` (5 * cost)
+      (`snoc` (Simple r)) =<< force b
+    br `icreditWith` cost
+    br `icreditWith` (deepDanger f)
+    deep f a m br d
+concat' (Deep f1 a1 m1 b1 r1) (Deep f2 a2 m2 b2 r2) = do
+  (r1', m, f2') <- share r1 f2
+  -- Discharge debits on b1, a2 for compound element
+  when (D.size f1 > 3 && D.size r1 > 3) $
+    b1 `icreditWith` cost
+  when (D.size f2 > 3 && D.size r2 > 3) $
+    a2 `icreditWith` cost
+  c1 <- cmpd m1 b1 r1'
+  c2 <- cmpd f2' a2 m2
+  a1' <- delay $ ILazy $ do
+    a1 `icreditWith` (4 * (cost - deepDanger f1))
+    (`snoc` c1) =<< force a1
+  b2' <- delay $ ILazy $ do
+    b2 `icreditWith` (4 * (cost - deepDanger r2))
+    cons c2 =<< force b2
+  -- Discharge debits for snoc/cons onto a1/b2
+  a1' `icreditWith` cost
+  b2' `icreditWith` cost
+  -- Discharge the debit from swapping f/r
+  when (D.size f1 == 3 && D.size f2 > 3) $
+    b2 `icreditWith` cost
+  when (D.size r2 == 3 && D.size r1 > 3) $
+    a1 `icreditWith` cost
+  -- Notice that only two of the when-statements
+  -- can be true at the same time.
+  -- So we only discharge 4 debits.
+  deep f1 a1' m b2' r2
+
+replaceHead :: MonadInherit m => a -> ImplicitCat a m -> m (ImplicitCat a m)
+replaceHead x (Shallow d) = do
+  d' <- D.uncons d
+  case d' of
+    Nothing -> fail "replaceHead: empty deque"
+    Just (_, d') -> Shallow <$> D.cons x d'
+replaceHead x (Deep f a m b r) = do
+  f' <- D.uncons f
+  case f' of
+    Nothing -> fail "replaceHead: empty deque"
+    Just (_, f') -> do
+      f' <- D.cons x f'
+      deep f' a m b r
+
+-- 6 * cost + 1 tick
+-- TODO: is there an off-by-one error here?
+-- We assign 5 * cost to other thunks and also perform 1 * cost of work.
+-- So the cost of the thunk is 6 * cost, not 5 * cost as claimed by Okasaki.
+-- In particular consider the case where a = empty and uncons b returns a compound element.
+-- Here we need to assign an extra 1 * cost to the bt thunk, but we can't possibly pay for that.
+-- Does that mean that this function is not amortized O(1)?
+-- This doesn't show up in the testsuite, because we never concat two deep deques
+-- and so we never generate a deque with a compound element.
+uncons' :: MonadInherit m => ImplicitCat a m -> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
+uncons' (Shallow d) = tick >> do
+  m <- D.uncons d
+  case m of
+    Nothing -> pure Nothing
+    Just (x, d') -> fmap (Just . (x,)) $ delay $ ILazy $ do
+      pure $ Shallow d'
+uncons' (Deep f a m b r) = tick >> do
+  f' <- D.uncons f
+  case f' of
+    Nothing -> pure Nothing
+    Just (x, f') -> fmap (Just . (x,)) $ delay $ ILazy $ do
+      if D.size f' >= 3 -- iff D.size f > 3
+        then do
+          a `icreditWith` (4 * deepDanger f')
+          b `icreditWith` (deepDanger f')
+          deep f' a m b r
+        else do -- D.size f' == 2
+          a `icreditWith` (cost - deepDanger r)
+          a <- force a
+          if not (isEmpty a)
+            then do
+              a' <- uncons' a
+              case a' of
+                Nothing -> fail "uncons': a cannot be empty"
+                Just (ah, at) -> do
+                  case ah of
+                    Simple d -> do
+                      f'' <- dappendL f' d -- cost: 2 * (cons + unsnoc)
+                      at `icreditWith` cost
+                      at `icreditWith` (deepDanger r)
+                      deep f'' at m b r
+                    Cmpd f'' c' r' -> do
+                      f''' <- dappendL f' f'' -- cost: 2 * (cons + unsnoc)
+                      a'' <- delay $ ILazy $ do
+                        c'' <- force c'
+                        ra <- replaceHead (Simple r') a -- cost: uncons + cons
+                        concat' c'' ra
+                      c' `icreditWith` (4 * cost)
+                      a'' `icreditWith` (deepDanger r)
+                      deep f''' a'' m b r
+            else do
+              b `icreditWith` (4 * (cost - deepDanger r))
+              b <- force b
+              if not (isEmpty b)
+                then do
+                  b' <- uncons' b
+                  case b' of
+                    Nothing -> fail "uncons': b cannot be empty"
+                    Just (bh, bt) -> do
+                      case bh of
+                        Simple d -> do
+                          f'' <- dappendL f' m -- cost: 2 * (cons + unsnoc)
+                          -- TODO: this is ugly. Since bt has 6 * cost debits
+                          -- we need to assign 1 * cost extra credits to it. But we
+                          -- can not pay for that. Instead, we redirect credits
+                          -- passed to a to be sent to bt. Once r is in deepDanger,
+                          -- it will pass one credit to a, which is redirected to bt.
+                          -- This ensures that bt receives 6 * cost credits by the
+                          -- time it is forced.
+                          a <- delay $ IPay bt $ do
+                            fmap Shallow $ empty
+                          a `icreditWith` (deepDanger r)
+                          bt `icreditWith` (4 * deepDanger r)
+                          deep f'' a d bt r
+                        Cmpd f'' c' r' -> do
+                          f''' <- dappendL f' m -- cost: 2 * (cons + unsnoc)
+                          a'' <- delay $ ILazy $ do
+                            c' `icreditWith` (4 * cost)
+                            cons (Simple f'') =<< force c'
+                          a'' `icreditWith` (deepDanger r)
+                          bt `icreditWith` (4 * deepDanger r)
+                          -- TODO: Here bt has too many debits: it gets 6 * cost
+                          -- debits from uncons', but may only have 5 * cost.
+                          -- We have already exhausted the credits on the current
+                          -- thunk and cannot pay for the extra 1 * cost.
+                          deep f''' a'' r' bt r
+                else do -- 1 * cost
+                  fm <- dappendL f' m
+                  concat' (Shallow fm) (Shallow r)
+
+replaceLast :: MonadInherit m => ImplicitCat a m -> a -> m (ImplicitCat a m)
+replaceLast (Shallow d) x = do
+  d' <- D.unsnoc d
+  case d' of
+    Nothing -> fail "replaceLast: empty deque"
+    Just (d', _) -> Shallow <$> D.snoc d' x
+replaceLast (Deep f a m b r) x = do
+  r' <- D.unsnoc r
+  case r' of
+    Nothing -> fail "replaceLast: empty deque"
+    Just (r', _) -> do
+      r' <- D.snoc r' x
+      deep f a m b r'
+
+unsnoc' :: MonadInherit m => ImplicitCat a m -> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
+unsnoc' (Shallow d) = tick >> do
+  m <- D.unsnoc d
+  case m of
+    Nothing -> pure Nothing
+    Just (d', x) -> fmap (Just . (,x)) $ delay $ ILazy $ do
+      pure $ Shallow d'
+unsnoc' (Deep f a m b r) = tick >> do
+  r' <- D.unsnoc r
+  case r' of
+    Nothing -> pure Nothing
+    Just (r', x) -> fmap (Just . (,x)) $ delay $ ILazy $ do
+      if D.size r' >= 3 -- iff D.size r > 3
+        then do
+          a `icreditWith` (deepDanger r')
+          b `icreditWith` (4 * deepDanger r')
+          deep f a m b r'
+        else do
+          b `icreditWith` (cost - deepDanger f)
+          b <- force b
+          if not (isEmpty b)
+            then do
+              b' <- unsnoc' b
+              case b' of
+                Nothing -> fail "unsnoc': b cannot be empty"
+                Just (bi, bl) -> do
+                  case bl of
+                    Simple d -> do
+                      r'' <- dappendR d r'
+                      bi `icreditWith` cost
+                      bi `icreditWith` (deepDanger f)
+                      deep f a m bi r''
+                    Cmpd f' c' r'' -> do
+                      r''' <- dappendR r'' r'
+                      b'' <- delay $ ILazy $ do
+                        c'' <- force c'
+                        bf <- replaceLast b (Simple f')
+                        concat' bf c''
+                      c' `icreditWith` (4 * cost)
+                      b'' `icreditWith` (deepDanger f)
+                      deep f a m b'' r'''
+            else do
+              a `icreditWith` (4 * (cost - deepDanger f))
+              a <- force a
+              if not (isEmpty a)
+                then do
+                  a' <- unsnoc' a
+                  case a' of
+                    Nothing -> fail "unsnoc': a cannot be empty"
+                    Just (ai, al) -> do
+                      case al of
+                        Simple d -> do
+                          r'' <- dappendR m r'
+                          b <- delay $ IPay ai $ do
+                            fmap Shallow $ empty
+                          b `icreditWith` (deepDanger f)
+                          ai `icreditWith` (4 * deepDanger f)
+                          deep f ai d b r''
+                        Cmpd f' c' r'' -> do
+                          r''' <- dappendR m r'
+                          b'' <- delay $ ILazy $ do
+                            c' `icreditWith` (4 * cost)
+                            (`snoc` (Simple r'')) =<< force c'
+                          b'' `icreditWith` (deepDanger f)
+                          ai `icreditWith` (4 * deepDanger f)
+                          deep f ai f' b'' r'''
+                else do
+                  mr <- dappendR m r'
+                  concat' (Shallow f) (Shallow mr)
+
+instance Deque ImplicitCat where
+  empty = Shallow <$> D.empty
+  cons x (Shallow d) = Shallow <$> D.cons x d
+  cons x (Deep f a m b r) = do
+    f' <- D.cons x f
+    deep f' a m b r
+  snoc (Shallow d) x = Shallow <$> D.snoc d x
+  snoc (Deep f a m b r) x = Deep f a m b <$> D.snoc r x
+  uncons d = do
+    m <- uncons' d
+    case m of
+      Nothing -> pure Nothing
+      Just (x, t) -> do
+        t `icreditWith` (6 * cost)
+        Just . (x,) <$> force t
+  unsnoc d = do
+    m <- unsnoc' d
+    case m of
+      Nothing -> pure Nothing
+      Just (t, x) -> do
+        t `icreditWith` (6 * cost)
+        Just . (,x) <$> force t
+  concat xs ys = tick >> concat' xs ys
+
+instance BoundedDeque ImplicitCat where
+  qcost sz (Cons x) = qcost @(D.BDeque) sz (Cons x)
+  qcost sz (Snoc x) = qcost @(D.BDeque) sz (Snoc x)
+  qcost sz Uncons = 1 + 6 * cost + qcost @(D.BDeque) sz Uncons
+  qcost sz Unsnoc = 1 + 6 * cost + qcost @(D.BDeque) sz Unsnoc
+  qcost _ Concat = 1 + 5 * cost
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ILazyCon m a) where
+  prettyCell _ = pure $ mkMCell "<lazy>" []
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (CmpdElem a m) where
+  prettyCell (Simple d) = do
+    d' <- prettyCell d
+    pure $ mkMCell "Simple" [d']
+  prettyCell (Cmpd f m r) = do
+    f' <- prettyCell f
+    m' <- prettyCell m
+    r' <- prettyCell r
+    pure $ mkMCell "Cmpd" [f', m', r']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ImplicitCat a m) where
+  prettyCell (Shallow d) = do
+    d' <- prettyCell d
+    pure $ mkMCell "Shallow" [d']
+  prettyCell (Deep f a m b r) = do
+    f' <- prettyCell f
+    a' <- prettyCell a
+    m' <- prettyCell m
+    b' <- prettyCell b
+    r' <- prettyCell r
+    pure $ mkMCell "Deep" [f', a', m', b', r']
+
+instance Pretty a => MemoryStructure (ImplicitCat (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Deque/Realtime.hs b/src/Test/Credit/Deque/Realtime.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Deque/Realtime.hs
@@ -0,0 +1,84 @@
+module Test.Credit.Deque.Realtime where
+
+import Prelude hiding (lookup, reverse)
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit.Deque.Base
+import Test.Credit.Deque.Streams
+
+-- | Delay a computation, but do not consume any credits
+indirect :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)
+indirect t = delay t >>= pure . SIndirect
+
+data RDeque a m = RDeque
+  { lenf :: !Int
+  , front :: Stream m a
+  , sf :: Stream m a
+  , lenr :: !Int
+  , rear :: Stream m a
+  , sr :: Stream m a
+  }
+
+exec1 :: MonadInherit m => Stream m a -> m (Stream m a)
+exec1 xs = credit (fromIntegral c + 1) xs >> smatch xs
+  (\_ xs -> pure xs)
+  (pure SNil)
+
+exec2 :: MonadInherit m => Stream m a -> m (Stream m a)
+exec2 xs = exec1 xs >>= exec1
+
+rdeque :: MonadInherit m => RDeque a m -> m (RDeque a m)
+rdeque (RDeque lenf f sf lenr r sr)
+  | lenf > c * lenr + 1 = do
+    let i = (lenf + lenr) `div` 2
+    let j = lenf + lenr - i
+    f' <- indirect (STake i f)
+    f'' <- indirect (SRevDrop i f SNil)
+    r' <- indirect (SAppend r f'')
+    credit (fromIntegral c) f'' >> eval (fromIntegral c) f''
+    pure $ RDeque i f' f' j r' r'
+  | lenr > c * lenf + 1 = do
+    let j = (lenf + lenr) `div` 2
+    let i = lenf + lenr - j
+    r' <- indirect (STake j r)
+    r'' <- indirect (SRevDrop j r SNil)
+    f' <- indirect (SAppend f r'')
+    credit (fromIntegral c) r'' >> eval (fromIntegral c) r''
+    pure $ RDeque i f' f' j r' r'
+  | otherwise =
+    pure $ RDeque lenf f sf lenr r sr
+
+instance Deque RDeque where
+  empty = pure $ RDeque 0 SNil SNil 0 SNil SNil
+  cons x (RDeque lenf f sf lenr r sr) = exec1 sf >>= \sf -> exec1 sr >>= \sr ->
+    rdeque (RDeque (lenf + 1) (SCons x f) sf lenr r sr)
+  snoc (RDeque lenf f sf lenr r sr) x = exec1 sf >>= \sf -> exec1 sr >>= \sr ->
+    rdeque (RDeque lenf f sf (lenr + 1) (SCons x r) sr)
+  uncons (RDeque lenf f sf lenr r sr) = exec2 sf >>= \sf -> exec2 sr >>= \sr -> smatch f
+    (\x f -> rdeque (RDeque (lenf - 1) f sf lenr r sr) >>= \q -> pure $ Just (x, q))
+    (pure Nothing)
+  unsnoc (RDeque lenf f sf lenr r sr) = exec2 sf >>= \sf -> exec2 sr >>= \sr -> smatch r
+    (\x r -> rdeque (RDeque lenf f sf (lenr - 1) r sr) >>= \q -> pure $ Just (q, x))
+    (pure Nothing)
+  concat = undefined
+
+instance BoundedDeque RDeque where
+  qcost _ (Cons _) = 3 * fromIntegral c + 4
+  qcost _ (Snoc _) = 3 * fromIntegral c + 4
+  qcost _ Uncons = 5 * fromIntegral c + 8
+  qcost _ Unsnoc = 5 * fromIntegral c + 8
+  qcost _ Concat = 0
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (RDeque a m) where
+  prettyCell (RDeque lenf f sf lenr r sr) = do
+    lenf' <- prettyCell lenf
+    f' <- prettyCell f
+    sf' <- prettyCell sf
+    lenr' <- prettyCell lenr
+    r' <- prettyCell r
+    sr' <- prettyCell sr
+    pure $ mkMCell "Deque" [lenf', f', sf', lenr', r', sr']
+
+instance Pretty a => MemoryStructure (RDeque (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Deque/SimpleCat.hs b/src/Test/Credit/Deque/SimpleCat.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Deque/SimpleCat.hs
@@ -0,0 +1,200 @@
+module Test.Credit.Deque.SimpleCat where
+
+import Prelude hiding (head, tail, concat)
+import Prettyprinter (Pretty)
+import Control.Monad
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Deque.Base
+import qualified Test.Credit.Deque.Base as D
+import qualified Test.Credit.Deque.Bankers as D
+
+-- | "simple"
+data SimpleCat a m
+  = Shallow (D.BDeque a m)
+  | Deep (D.BDeque a m) -- ^ (>= 2 elements)
+         (Thunk m (Lazy m) (SimpleCat (D.BDeque a m) m))
+         (D.BDeque a m) -- ^ (>= 2 elements)
+
+dangerous :: D.BDeque a m -> Bool
+dangerous d = D.size d == 2
+
+cost :: Credit
+cost = qcost @(D.BDeque) undefined (Cons undefined) + 3 * qcost @(D.BDeque) undefined Uncons
+
+danger :: D.BDeque a m -> Credit
+danger d = if D.size d == 2 then cost else 0
+
+deep :: MonadInherit m => D.BDeque a m -> Thunk m (Lazy m) (SimpleCat (D.BDeque a m) m) -> D.BDeque a m -> m (SimpleCat a m)
+deep f m r = do
+  m `hasAtLeast` (danger f + danger r)
+  pure $ Deep f m r
+
+isEmpty :: SimpleCat a m -> Bool
+isEmpty (Shallow d) = D.isEmpty d
+isEmpty (Deep _ _ _) = False
+
+data DequeIs a m
+  = Small (Maybe a)
+  | Big (D.BDeque a m)
+
+tooSmall :: MonadInherit m => D.BDeque a m -> m (DequeIs a m)
+tooSmall d = do
+  m1 <- D.uncons d
+  case m1 of
+    Nothing -> pure $ Small Nothing
+    Just (x, d') -> do
+      m2 <- D.uncons d'
+      case m2 of
+        Nothing -> pure $ Small (Just x)
+        Just _ -> pure $ Big d
+
+dappendL :: MonadInherit m => Maybe a -> D.BDeque a m -> m (D.BDeque a m)
+dappendL Nothing d2 = pure d2
+dappendL (Just x) d2 = D.cons x d2
+
+dappendR :: MonadInherit m => D.BDeque a m -> Maybe a -> m (D.BDeque a m)
+dappendR d1 Nothing = pure d1
+dappendR d1 (Just x) = D.snoc d1 x
+
+uncons' :: MonadInherit m => SimpleCat a m -> m (Maybe (a, Thunk m (Lazy m) (SimpleCat a m)))
+uncons' (Shallow d) = tick >> do
+  m <- D.uncons d
+  case m of
+    Nothing -> pure Nothing
+    Just (x, d') -> fmap (Just . (x,)) $ delay $ Lazy $ do
+      pure $ Shallow d'
+uncons' (Deep f m r) = tick >> do
+  f' <- D.uncons f
+  case f' of
+    Nothing -> pure Nothing
+    Just (x, f') -> fmap (Just . (x,)) $ delay $ Lazy $ do
+      dis <- tooSmall f'
+      case dis of
+        Big f' -> do
+          when (dangerous f') $ m `creditWith` cost
+          deep f' m r
+        Small y -> do
+          unless (dangerous r) $ m `creditWith` cost
+          m' <- uncons' =<< force m
+          case m' of
+            Nothing -> Shallow <$> dappendL y r
+            Just (h, t) -> do
+              when (dangerous r) $ t `creditWith` cost
+              dappendL y h >>= \h -> deep h t r
+
+unsnoc' :: MonadInherit m => SimpleCat a m -> m (Maybe (Thunk m (Lazy m) (SimpleCat a m), a))
+unsnoc' (Shallow d) = tick >> do
+  m <- D.unsnoc d
+  case m of
+    Nothing -> pure Nothing
+    Just (d', x) -> fmap (Just . (,x)) $ delay $ Lazy $ do
+      pure $ Shallow d'
+unsnoc' (Deep f m r) = tick >> do
+  r' <- D.unsnoc r
+  case r' of
+    Nothing -> pure Nothing
+    Just (r', x) -> fmap (Just . (,x)) $ delay $ Lazy $ do
+      dis <- tooSmall r'
+      case dis of
+        Big r' -> do
+          when (dangerous r') $ m `creditWith` cost
+          deep f m r'
+        Small y -> do
+          unless (dangerous f) $ m `creditWith` cost
+          m' <- unsnoc' =<< force m
+          case m' of
+            Nothing -> Shallow <$> dappendR f y
+            Just (t, h) -> do
+              when (dangerous f) $ t `creditWith` cost
+              deep f t =<< dappendR h y
+
+concat' :: MonadInherit m => SimpleCat a m -> SimpleCat a m -> m (SimpleCat a m)
+concat' (Shallow d1) (Shallow d2) = tick >> do
+  dis1 <- tooSmall d1
+  case dis1 of
+    Small y -> Shallow <$> dappendL y d2
+    Big d1 -> do
+      dis2 <- tooSmall d2
+      case dis2 of
+        Small y -> Shallow <$> dappendR d1 y
+        Big d2 -> do
+          m <- delay $ Lazy empty
+          when (dangerous d1) $ m `creditWith` cost
+          when (dangerous d2) $ m `creditWith` cost
+          deep d1 m d2
+concat' (Shallow d1) (Deep f m r) = tick >> do
+  dis1 <- tooSmall d1
+  case dis1 of
+    Small y -> dappendL y f >>= \f -> deep f m r
+    Big d -> do
+      m `creditWith` cost
+      unless (dangerous r) $ m `creditWith` cost
+      m' <- delay $ Lazy $ cons f =<< force m
+      when (dangerous d) $ m' `creditWith` cost
+      when (dangerous r) $ m' `creditWith` cost
+      deep d m' r
+concat' (Deep f m r) (Shallow d2) = tick >> do
+  dis2 <- tooSmall d2
+  case dis2 of
+    Small y -> deep f m =<< dappendR r y
+    Big d -> do
+      m `creditWith` cost
+      unless (dangerous f) $ m `creditWith` cost
+      m' <- delay $ Lazy $ flip snoc r =<< force m
+      when (dangerous d) $ m' `creditWith` cost
+      when (dangerous f) $ m' `creditWith` cost
+      deep f m' d
+concat' (Deep f1 m1 r1) (Deep f2 m2 r2) = tick >> do
+  m <- delay $ Lazy $ do
+    m1 `creditWith` (2 * cost)
+    m1' <- flip snoc r1 =<< force m1
+    m2 `creditWith` (2 * cost)
+    m2' <- cons f2 =<< force m2
+    concat' m1' m2'
+  creditAllTo m
+  deep f1 m r2
+
+instance Deque SimpleCat where
+  empty = Shallow <$> D.empty
+  cons x (Shallow d) = Shallow <$> D.cons x d
+  cons x (Deep f m r) = do
+    f' <- D.cons x f
+    deep f' m r
+  snoc (Shallow d) x = Shallow <$> D.snoc d x
+  snoc (Deep f m r) x = deep f m =<< D.snoc r x
+  uncons d = do
+    m <- uncons' d
+    case m of
+      Nothing -> pure Nothing
+      Just (x, t) -> do
+        t `creditWith` (2 * cost)
+        Just . (x,) <$> force t
+  unsnoc d = do
+    m <- unsnoc' d
+    case m of
+      Nothing -> pure Nothing
+      Just (t, x) -> do
+        t `creditWith` (2 * cost)
+        Just . (,x) <$> force t
+  concat = concat'
+
+instance BoundedDeque SimpleCat where
+  qcost n (Cons x) = qcost @(D.BDeque) n (Cons x)
+  qcost n (Snoc x) = qcost @(D.BDeque) n (Snoc x)
+  qcost n Uncons = 1 + qcost @(D.BDeque) n Uncons + 2 * cost
+  qcost n Unsnoc = 1 + qcost @(D.BDeque) n Unsnoc + 2 * cost
+  qcost n Concat = (1 + 6 * cost) * log2 n
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SimpleCat a m) where
+  prettyCell (Shallow d) = do
+    d' <- prettyCell d
+    pure $ mkMCell "Shallow" [d']
+  prettyCell (Deep f m r) = do
+    f' <- prettyCell f
+    m' <- prettyCell m
+    r' <- prettyCell r
+    pure $ mkMCell "Deep" [f', m', r']
+
+instance Pretty a => MemoryStructure (SimpleCat (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Deque/Streams.hs b/src/Test/Credit/Deque/Streams.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Deque/Streams.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE GADTs #-}
+
+module Test.Credit.Deque.Streams (Stream(..), SLazyCon(..), smatch, credit, eval, c) where
+
+import Prelude hiding (lookup, reverse)
+import Control.Monad.Credit
+
+c :: Int
+c = 5
+
+data Stream m a
+  = SCons a (Stream m a)
+  | SNil
+  | SIndirect (SThunk m (Stream m a))
+
+type SThunk m = Thunk m (SLazyCon m)
+
+data SLazyCon m a where
+  SAppend :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)
+  SRevDrop :: Int -> Stream m a -> Stream m a -> SLazyCon m (Stream m a)
+  STake :: Int -> Stream m a -> SLazyCon m (Stream m a)
+
+instance MonadInherit m => HasStep (SLazyCon m) m where
+  step (SAppend xs ys) = sappend xs ys
+  step (SRevDrop n xs ys) = srevdrop n xs ys
+  step (STake n xs) = stake n xs
+
+-- | Smart destructor for streams, consuming one credit
+smatch :: MonadInherit m => Stream m a -- ^ Scrutinee
+       -> (a -> Stream m a -> m b) -- ^ Cons case
+       -> m b -- ^ Nil case
+       -> m b
+smatch x cons nil = tick >> eval x
+  where
+    eval x = case x of
+      SCons a as -> cons a as
+      SNil -> nil
+      SIndirect i -> force i >>= eval
+
+-- | delay a computation, consuming all credits
+taildelay :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)
+taildelay t = delay t >>= \x -> creditAllTo x >> pure (SIndirect x)
+
+stake :: MonadInherit m => Int -> Stream m a -> m (Stream m a)
+stake 0 xs = pure SNil
+stake n xs = smatch xs
+  (\x xs -> SCons x <$> taildelay (STake (n - 1) xs))
+  (pure SNil)
+
+srevdrop :: MonadInherit m => Int -> Stream m a -> Stream m a -> m (Stream m a)
+srevdrop 0 xs ys = smatch xs
+  (\x xs -> taildelay (SRevDrop 0 xs (SCons x ys)))
+  (pure ys)
+srevdrop n xs ys = smatch xs
+  (\x xs -> taildelay (SRevDrop (n - 1) xs ys))
+  (fail "drop: empty stream")
+
+credit :: MonadInherit m => Credit -> Stream m a -> m ()
+credit n (SIndirect i) = creditWith i n
+credit _ _ = pure ()
+
+evalone :: MonadInherit m => Stream m a -> m ()
+evalone (SIndirect i) = force i >> pure ()
+evalone _ = pure ()
+
+eval :: MonadInherit m => Int -> Stream m a -> m ()
+eval 0 s = pure ()
+eval n s = evalone s >> eval (n - 1) s
+
+sappend :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)
+sappend xs ys = credit (fromIntegral c) ys >> eval c ys >> smatch xs
+  (\x xs -> SCons x <$> taildelay (SAppend xs ys))
+  (pure ys)
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SLazyCon m a) where
+  prettyCell (SAppend xs ys) = do
+    xs' <- prettyCell xs
+    ys' <- prettyCell ys
+    pure $ mkMCell "SAppend" [xs', ys']
+  prettyCell (SRevDrop n xs ys) = do
+    n' <- prettyCell n
+    xs' <- prettyCell xs
+    ys' <- prettyCell ys
+    pure $ mkMCell "SRevDrop" [n', xs', ys']
+  prettyCell (STake n xs) = do
+    n' <- prettyCell n
+    xs' <- prettyCell xs
+    pure $ mkMCell "STake" [n', xs']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where
+  prettyCell xs = mkMList <$> toList xs <*> toHole xs
+    where
+      toList SNil = pure $ []
+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs
+      toList (SIndirect t) = pure $ []
+
+      toHole SNil = pure $ Nothing
+      toHole (SCons x xs) = toHole xs
+      toHole (SIndirect t) = Just <$> prettyCell t
diff --git a/src/Test/Credit/Finger.hs b/src/Test/Credit/Finger.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Finger.hs
@@ -0,0 +1,618 @@
+{-# LANGUAGE GADTs, OverloadedLists, LambdaCase #-}
+
+module Test.Credit.Finger where
+
+import Prelude hiding (head, tail, last, init)
+import Data.List.NonEmpty (NonEmpty(..), (<|))
+import qualified Data.List.NonEmpty as NE
+import Control.Monad (when, unless)
+import Data.Foldable (foldlM, foldrM)
+import Prettyprinter (Pretty)
+
+import Control.Monad.Credit
+import Test.Credit (linear, log2)
+import qualified Test.Credit.Deque.Base as D
+import qualified Test.Credit.Heap.Base as H
+import qualified Test.Credit.RandomAccess.Base as RA
+import qualified Test.Credit.Sortable.Base as S
+
+data Digit a = One a | Two a a | Three a a a
+  deriving (Eq, Ord, Show)
+
+data Tuple v a = Pair v a a | Triple v a a a
+  deriving (Eq, Ord, Show)
+
+data FingerTree v a m
+  = Empty
+  | Single a
+  | Deep (Thunk m (Lazy m) v) (Digit a) (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) (Digit a)
+
+data FLazyCon m a where
+  FPure :: a -> FLazyCon m a
+  FCons :: Measured a v => a -> Thunk m (FLazyCon m) (FingerTree v a m) -> FLazyCon m (FingerTree v a m)
+  FSnoc :: Measured a v => Thunk m (FLazyCon m) (FingerTree v a m) -> a -> FLazyCon m (FingerTree v a m)
+  FTail :: Measured a v => FingerTree v a m -> FLazyCon m (FingerTree v a m)
+  FInit :: Measured a v => FingerTree v a m -> FLazyCon m (FingerTree v a m)
+
+instance MonadCredit m => HasStep (FLazyCon m) m where
+  step (FPure xs) = pure xs
+  step (FCons x m) = cons x =<< force m
+  step (FSnoc m x) = flip snoc x =<< force m
+  step (FTail q) = tail q
+  step (FInit q) = init q
+
+-- Main idea:
+--  - cons, snoc, tail and init all cost two credits
+--  - the first credit is used to tick
+--  - We maintain the invariant: In each queue Deep(f, m, r), m has ||f| - 2| + ||r| - 2| credits.
+--  - The m thunk requires two credits to force.
+--  - snoc and tail spend their second credit on either the old m to be able to force it,
+--    or on the new m to maintain the invariant.
+
+class Monoid v => Measured a v where
+  measure :: a -> v
+
+instance Measured a v => Measured [a] v where
+  measure = mconcat . map measure
+
+instance Measured a v => Measured (Digit a) v where
+  measure = measure . toList
+
+instance Monoid v => Measured (Tuple v a) v where
+  measure (Pair v _ _) = v
+  measure (Triple v _ _ _) = v
+
+measurement :: (MonadCredit m, Measured a v) => FingerTree v a m -> m v
+measurement Empty = pure $ mempty
+measurement (Single x) = pure $ measure x
+measurement (Deep vm f m r) = do
+  vm' <- force vm
+  pure $ measure f <> vm' <> measure r
+
+forceAll :: (MonadCredit m, Measured a v) => FingerTree v a m -> m ()
+forceAll Empty = pure ()
+forceAll (Single _) = pure ()
+forceAll (Deep _ _ m _) = do
+  creditWith m 2
+  forceAll =<< force m
+
+isTwo :: Digit a -> Bool
+isTwo (Two _ _) = True
+isTwo _ = False
+
+empty :: MonadCredit m => m (Thunk m (FLazyCon m) (FingerTree v a m))
+empty = delay $ FPure Empty
+
+pair :: Measured a v => a -> a -> Tuple v a
+pair x y = Pair (measure x <> measure y) x y
+
+triple :: Measured a v => a -> a -> a -> Tuple v a
+triple x y z = Triple (measure x <> measure y <> measure z) x y z
+
+deep :: (MonadCredit m, Measured a v) => Thunk m (Lazy m) v -> Digit a -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)
+deep v f m r = do
+  let oneIfDangerous d = if isTwo d then 0 else 1
+  mIsPure <- lazymatch m (\_ -> pure True) $ \case
+    FPure _ -> pure True
+    _ -> pure False
+  unless mIsPure $
+    m `hasAtLeast` (oneIfDangerous f + oneIfDangerous r)
+  pure $ Deep v f m r
+
+deep' :: (MonadCredit m, Measured a v) => Digit a -> m (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) -> Digit a -> m (FingerTree v a m)
+deep' f mkM r = do
+  m <- mkM
+  vm <- delay $ Lazy $ measurement =<< force m
+  deep vm f m r
+
+isEmpty :: FingerTree v a m -> Bool
+isEmpty Empty = True
+isEmpty _ = False
+
+toList :: Digit a -> [a]
+toList (One x) = [x]
+toList (Two x y) = [x, y]
+toList (Three x y z) = [x, y, z]
+
+toTree :: (MonadCredit m, Measured a v) => [a] -> m (FingerTree v a m)
+toTree [] = pure Empty
+toTree [x] = pure $ Single x
+toTree [x,y] = deep' (One x) empty (One y)
+toTree [x,y,z] = deep' (Two x y) empty (One z)
+
+toDigit :: Tuple v a -> Digit a
+toDigit (Pair _ x y) = Two x y
+toDigit (Triple _ x y z) = Three x y z
+
+cons :: (MonadCredit m, Measured a v) => a -> FingerTree v a m -> m (FingerTree v a m)
+cons x q = tick >> cons' x q
+
+cons' :: (MonadCredit m, Measured a v) => a -> FingerTree v a m -> m (FingerTree v a m)
+cons' x Empty = pure $ Single x
+cons' x (Single y) = do
+  deep' (One x) empty (One y)
+cons' x (Deep vq pr q u) = case pr of
+  One y       -> deep vq (Two x y) q u
+  Two y z     -> creditWith q 1 >> pure (Deep vq (Three x y z) q u)
+  Three y z w -> do
+    q' <- delay $ FCons (pair z w) q
+    if isTwo u
+      then creditWith q 1
+      else creditWith q' 1
+    vq' <- delay $ Lazy $ measurement =<< force q'
+    deep vq' (Two x y) q' u
+
+head :: MonadCredit m => FingerTree v a m -> m a
+head Empty = fail "head: empty queue"
+head (Single x) = pure x
+head (Deep _ s _ _) = pure $ let (h:_) = toList s in h
+
+tail :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (FingerTree v a m)
+tail Empty = tick >> pure Empty
+tail (Single _) = tick >> pure Empty
+tail (Deep vq (Three _ x y) q u) = tick >> pure (Deep vq (Two x y) q u)
+tail (Deep vq (Two _ x) q u) = tick >> creditWith q 1 >> pure (Deep vq (One x) q u)
+tail (Deep _ (One _) q u) = tick >> do
+  when (isTwo u) $ creditWith q 1
+  q' <- force q
+  deep0 q' u
+
+deep0 :: (MonadCredit m, Measured a v) => FingerTree v (Tuple v a) m -> Digit a -> m (FingerTree v a m)
+deep0 Empty s = toTree $ toList s
+deep0 q u = do
+  h <- head q
+  case h of
+    Pair _ x y -> do
+      t <- delay $ FTail q
+      unless (isTwo u) $ creditWith t 1
+      vt <- delay $ Lazy $ measurement =<< force t
+      deep vt (Two x y) t u
+    Triple _ x _ _ -> do
+      q' <- map1 chop q
+      deep' (One x) (delay $ FPure q') u
+      where chop (Triple _ _ y z) = pair y z
+
+map1 :: (MonadCredit m, Measured a v) => (a -> a) -> FingerTree v a m -> m (FingerTree v a m)
+map1 _ Empty = pure Empty
+map1 f (Single x) = pure $ Single (f x)
+map1 f (Deep vq (One x) q u) = deep vq (One (f x)) q u
+map1 f (Deep vq (Two x y) q u) = deep vq (Two (f x) y) q u
+map1 f (Deep vq (Three x y z) q u) = deep vq (Three (f x) y z) q u
+
+uncons :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (Maybe (a, FingerTree v a m))
+uncons q =
+  if isEmpty q
+    then pure Nothing
+    else do
+      h <- head q
+      t <- tail q
+      pure $ Just (h, t)
+
+deepL :: (MonadCredit m, Measured a v) => [a] -> Thunk m (Lazy m) v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)
+deepL [] _ m sf = do
+  m' <- uncons =<< force m
+  case m' of
+    Nothing -> toTree $ toList sf
+    Just (Pair _ x y, m'') -> do
+      deep' (Two x y) (delay $ FPure m'') sf
+    Just (Triple _ x y z, m'') -> do
+      deep' (Three x y z) (delay $ FPure m'') sf
+deepL [x] vm m sf = deep vm (One x) m sf
+deepL [x,y] vm m sf = deep vm (Two x y) m sf
+deepL [x,y,z] vm m sf = deep vm (Three x y z) m sf
+
+last :: (MonadCredit m, Measured a v) => FingerTree v a m -> m a
+last Empty = fail "last: empty queue"
+last (Single x) = pure x
+last (Deep _ _ _ s) = pure $ let (h:_) = reverse $ toList s in h
+
+snoc :: (MonadCredit m, Measured a v) => FingerTree v a m -> a -> m (FingerTree v a m)
+snoc q y = tick >> snoc' q y
+
+snoc' :: (MonadCredit m, Measured a v) => FingerTree v a m -> a -> m (FingerTree v a m)
+snoc' Empty y = pure $ Single y
+snoc' (Single x) y = deep' (One x) empty (One y)
+snoc' (Deep vq u q (One x)) y = deep vq u q (Two x y)
+snoc' (Deep vq u q (Two x y)) z = creditWith q 1 >> pure (Deep vq u q (Three x y z))
+snoc' (Deep _ u q (Three x y z)) w = do
+  q' <- delay $ FSnoc q (pair x y)
+  if isTwo u
+    then creditWith q 1
+    else creditWith q' 1
+  vq' <- delay $ Lazy $ measurement =<< force q'
+  deep vq' u q' (Two z w)
+
+init :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (FingerTree v a m)
+init Empty = tick >> pure Empty
+init (Single _) = tick >> pure Empty
+init (Deep vq u q (Three x y _)) = tick >> pure (Deep vq u q (Two x y))
+init (Deep vq u q (Two x _)) = tick >> creditWith q 1 >> pure (Deep vq u q (One x))
+init (Deep _ u q (One _)) = tick >> when (isTwo u) (creditWith q 1) >> force q >>= deepN u
+
+deepN :: (MonadCredit m, Measured a v) => Digit a -> FingerTree v (Tuple v a) m -> m (FingerTree v a m)
+deepN s Empty = toTree $ toList s
+deepN u q = do
+  l <- last q
+  case l of
+    Pair _ x y -> do
+      t <- delay $ FInit q
+      unless (isTwo u) $ creditWith t 1
+      vt <- delay $ Lazy $ measurement =<< force t
+      deep vt u t (Two x y)
+    Triple _ _ _ z -> do
+      q' <- mapN chop q
+      deep' u (delay $ FPure q') (One z)
+      where chop (Triple _ x y _) = pair x y
+
+mapN :: (MonadCredit m, Measured a v) => (a -> a) -> FingerTree v a m -> m (FingerTree v a m)
+mapN _ Empty = pure $ Empty
+mapN f (Single x) = pure $ Single (f x)
+mapN f (Deep vq u q (One x)) = deep vq u q (One (f x))
+mapN f (Deep vq u q (Two x y)) = deep vq u q (Two x (f y))
+mapN f (Deep vq u q (Three x y z)) = deep vq u q (Three x y (f z))
+
+unsnoc :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (Maybe (FingerTree v a m, a))
+unsnoc q =
+  if isEmpty q
+    then pure Nothing
+    else do
+      h <- last q
+      t <- init q
+      pure $ Just (t, h)
+
+deepR :: (MonadCredit m, Measured a v) => Digit a -> Thunk m (Lazy m) v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> [a] -> m (FingerTree v a m)
+deepR s _ m [] = do
+  m' <- unsnoc =<< force m
+  case m' of
+    Nothing -> toTree $ toList s
+    Just (m'', Pair _ x y) -> do
+      deep' s (delay $ FPure m'') (Two x y)
+    Just (m'', Triple _ x y z) -> do
+      deep' s (delay $ FPure m'') (Three x y z)
+deepR s vm m [x] = deep vm s m (One x)
+deepR s vm m [x, y] = deep vm s m (Two x y)
+deepR s vm m [x, y, z] = deep vm s m (Three x y z)
+
+toTuples :: Measured a v => [a] -> [Tuple v a]
+toTuples [] = []
+toTuples [x, y] = [pair x y]
+toTuples [x, y, z, w] = [pair x y, pair z w]
+toTuples (x : y : z : xs) = triple x y z : toTuples xs
+
+glue :: (MonadCredit m, Measured a v) => FingerTree v a m -> [a] -> FingerTree v a m -> m (FingerTree v a m)
+glue Empty as q2 = foldrM cons q2 as
+glue q1 as Empty = foldlM snoc q1 as
+glue (Single x) as q2 = foldrM cons q2 (x : as)
+glue q1 as (Single y) = foldlM snoc q1 (as ++ [y])
+glue (Deep _ u1 q1 v1) as (Deep _ u2 q2 v2) = tick >> do
+  creditWith q1 2
+  q1 <- force q1
+  creditWith q2 2
+  q2 <- force q2
+  q <- glue q1 (toTuples (toList v1 ++ as ++ toList u2)) q2
+  deep' u1 (delay $ FPure q) v2
+
+concat' :: (MonadCredit m, Measured a v) => FingerTree v a m -> FingerTree v a m -> m (FingerTree v a m)
+concat' q1 q2 = glue q1 [] q2
+
+data Split v a m = Split
+  { measureOfSmaller :: v
+  , smaller :: FingerTree v a m
+  , found   :: a
+  , bigger  :: FingerTree v a m
+  }
+
+splitDigit :: Measured a v => (v -> Bool) -> v -> Digit a -> ([a], a, [a])
+splitDigit p i (One x) = ([], x, [])
+splitDigit p i (Two x y)
+  | p (i <> measure x) = ([], x, [y])
+  | otherwise = ([x], y, [])
+splitDigit p i (Three x y z)
+  | p (i <> measure x) = ([], x, [y, z])
+  | p (i <> measure x <> measure y) = ([x], y, [z])
+  | otherwise = ([x, y], z, [])
+
+-- For '(Split vml ml xs mr) <- splitTree p i m', we have 'vml = measurement ml'.
+splitTree :: (MonadCredit m, Measured a v) => (v -> Bool) -> v -> FingerTree v a m -> m (Split v a m)
+splitTree p i Empty = fail "splitTree: empty tree"
+splitTree p i (Single x) = pure $ Split mempty Empty x Empty
+splitTree p i (Deep vm pr m sf) = tick >> do
+  vm' <- force vm
+  let vpr = i <> measure pr
+  let vprm = vpr <> vm'
+  if p vpr then do
+    let (l, x, r) = splitDigit p i pr
+    Split (measure l) <$> toTree l <*> pure x <*> deepL r vm m sf
+  else if p vprm then do
+    Split vml ml xs mr <- splitTree p vpr =<< force m
+    let (l, x, r) = splitDigit p (vpr <> vml) (toDigit xs)
+    -- [ml', mr', vmr', vml'] <- mapM (delay . Lazy)
+      -- [pure ml, pure mr, measurement mr, pure vml]
+    ml' <- delay $ FPure ml
+    mr' <- delay $ FPure mr
+    vmr' <- delay $ Lazy $ measurement mr
+    vml' <- delay $ Lazy $ pure vml
+    Split (measure pr <> vml <> measure l) <$> deepR pr vml' ml' l <*> pure x <*> deepL r vmr' mr' sf
+  else do
+    let (l, x, r) = splitDigit p vprm sf
+    Split (measure pr <> vm' <> measure l) <$> deepR pr vm m l <*> pure x <*> toTree r
+
+split :: (MonadCredit m, Measured a v) => (v -> Bool) -> FingerTree v a m -> m (FingerTree v a m, FingerTree v a m)
+split p Empty = pure (Empty, Empty)
+split p xs = do
+  forceAll xs
+  mxs <- measurement xs
+  if p mxs
+    then do (Split _ l x r) <- splitTree p mempty xs
+            (l,) <$> cons x r
+    else pure (xs, Empty)
+
+takeUntil :: (MonadCredit m, Measured a v) => (v -> Bool) -> FingerTree v a m -> m (FingerTree v a m)
+takeUntil p m = fst <$> split p m
+
+dropUntil :: (MonadCredit m, Measured a v) => (v -> Bool) -> FingerTree v a m -> m (FingerTree v a m)
+dropUntil p m = snd <$> split p m
+
+lookupTree :: (MonadCredit m, Measured a v) => (v -> Bool) -> v -> FingerTree v a m -> m (Maybe (v, a))
+lookupTree p i Empty = pure Nothing
+lookupTree p i t = do
+  forceAll t
+  (Split ml _ x _) <- splitTree p i t
+  pure $ Just (i <> ml, x)
+
+instance MemoryCell m a => MemoryCell m (Digit a) where
+  prettyCell (One a) = do
+    a' <- prettyCell a
+    pure $ mkMCell "One" [a']
+  prettyCell (Two a b) = do
+    a' <- prettyCell a
+    b' <- prettyCell b
+    pure $ mkMCell "Two" [a', b']
+  prettyCell (Three a b c) = do
+    a' <- prettyCell a
+    b' <- prettyCell b
+    c' <- prettyCell c
+    pure $ mkMCell "Three" [a', b', c']
+
+instance MemoryCell m a => MemoryCell m (Tuple v a) where
+  prettyCell (Pair _ a b) = do
+    a' <- prettyCell a
+    b' <- prettyCell b
+    pure $ mkMCell "Pair" [a', b']
+  prettyCell (Triple _ a b c) = do
+    a' <- prettyCell a
+    b' <- prettyCell b
+    c' <- prettyCell c
+    pure $ mkMCell "Triple" [a', b', c']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FLazyCon m a) where
+  prettyCell (FPure x) = do
+    x' <- prettyCell x
+    pure $ mkMCell "FPure" [x']
+  prettyCell (FCons x m) = do
+    -- x' <- prettyCell x
+    m' <- prettyCell m
+    pure $ mkMCell "FCons" [m']
+  prettyCell (FSnoc m x) = do
+    m' <- prettyCell m
+    -- x' <- prettyCell x
+    pure $ mkMCell "FSnoc" [m']
+  prettyCell (FTail q) = do
+    q' <- prettyCell q
+    pure $ mkMCell "FTail" [q']
+  prettyCell (FInit q) = do
+    q' <- prettyCell q
+    pure $ mkMCell "FInit" [q']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerTree v a m) where
+  prettyCell Empty = pure $ mkMCell "Empty" []
+  prettyCell (Single a) = do
+    a' <- prettyCell a
+    pure $ mkMCell "Single" [a']
+  prettyCell (Deep _ s q u) = do
+    s' <- prettyCell s
+    q' <- prettyCell q
+    u' <- prettyCell u
+    pure $ mkMCell "Deep" [s', q', u']
+
+instance Pretty a => MemoryStructure (FingerTree v (PrettyCell a)) where
+  prettyStructure = prettyCell
+
+newtype Elem a = Elem a
+  deriving (Eq, Ord, Show)
+
+instance (MemoryCell m a) => MemoryCell m (Elem a) where
+  prettyCell (Elem x) = prettyCell x
+
+-- Deque
+
+instance Measured (Elem a) () where
+  measure (Elem x) = ()
+
+newtype FingerDeque a m = FingerDeque (FingerTree () (Elem a) m)
+
+instance D.Deque FingerDeque where
+  empty = pure $ FingerDeque Empty
+  cons x (FingerDeque q) = FingerDeque <$> cons (Elem x) q
+  snoc (FingerDeque q) x = FingerDeque <$> snoc q (Elem x)
+  uncons (FingerDeque q) = do
+    m <- uncons q
+    case m of
+      Nothing -> pure Nothing
+      Just (Elem x, q') -> pure $ Just (x, FingerDeque q')
+  unsnoc (FingerDeque q) = do
+    m <- unsnoc q
+    case m of
+      Nothing -> pure Nothing
+      Just (q', Elem x) -> pure $ Just (FingerDeque q', x)
+  concat (FingerDeque q1) (FingerDeque q2) = FingerDeque <$> concat' q1 q2
+
+instance D.BoundedDeque FingerDeque where
+  qcost _ (D.Cons _) = 2
+  qcost _ (D.Snoc _) = 2
+  qcost _ D.Uncons = 4
+  qcost _ D.Unsnoc = 2
+  qcost n D.Concat = 5 * log2 n
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerDeque a m) where
+  prettyCell (FingerDeque q) = prettyCell q
+
+instance Pretty a => MemoryStructure (FingerDeque (PrettyCell a)) where
+  prettyStructure = prettyCell
+
+-- Random Access
+
+newtype Size = Size Int
+  deriving (Eq, Ord, Show, Num)
+
+instance Semigroup Size where
+  x <> y = x + y
+
+instance Monoid Size where
+  mempty = 0
+
+instance Measured (Elem a) Size where
+  measure (Elem x) = 1
+
+newtype FingerRA a m = FingerRA (FingerTree Size (Elem a) m)
+
+-- Contrary to Hinze and Paterson, this is not O(1) but O(log n)
+-- because we need to force all thunks in the tree to get the size.
+length :: MonadCredit m => FingerRA a m -> m Size
+length (FingerRA t) = measurement t
+
+splitAt :: MonadCredit m => Int -> FingerRA a m -> m (FingerRA a m, FingerRA a m)
+splitAt i (FingerRA xs) = do
+   (l, r) <- split (fromIntegral i <) xs
+   pure $ (FingerRA l, FingerRA r)
+
+instance RA.RandomAccess FingerRA where
+  empty = pure $ FingerRA Empty
+  cons x (FingerRA q) = FingerRA <$> cons (Elem x) q
+  uncons (FingerRA q) = do
+    m <- uncons q
+    case m of
+      Nothing -> pure Nothing
+      Just (Elem x, m') -> do
+        pure $ Just (x, FingerRA m')
+  lookup i (FingerRA Empty) = pure Nothing
+  lookup i (FingerRA xs) = do
+    forceAll xs
+    (Split _ _ (Elem x) _) <- splitTree (fromIntegral i <) 0 xs
+    pure $ Just x
+  update i a (FingerRA Empty) = pure $ FingerRA Empty
+  update i a (FingerRA xs) = do
+    forceAll xs
+    (Split ml l (Elem x) r) <- splitTree (fromIntegral i <) 0 xs
+    if fromIntegral i > ml
+      then FingerRA <$> snoc l (Elem x)
+      else FingerRA <$> (concat' l =<< cons (Elem a) r)
+
+instance RA.BoundedRandomAccess FingerRA where
+  qcost n (RA.Cons _) = 2
+  qcost n RA.Uncons = 2
+  qcost n (RA.Lookup i) = 5 * log2 n
+  qcost n (RA.Update i _) = 2 + 10 * log2 n
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerRA a m) where
+  prettyCell (FingerRA q) = prettyCell q
+
+instance Pretty a => MemoryStructure (FingerRA (PrettyCell a)) where
+  prettyStructure = prettyCell
+
+-- Heap
+
+data Prio a = MInfty | Prio a
+  deriving (Eq, Ord, Show)
+
+instance Ord a => Semigroup (Prio a) where
+  MInfty <> p = p
+  p <> MInfty = p
+  Prio x <> Prio y = Prio (min x y)
+
+instance Ord a => Monoid (Prio a) where
+  mempty = MInfty
+
+instance Ord a => Measured (Elem a) (Prio a) where
+  measure (Elem x) = Prio x
+
+newtype FingerHeap a m = FingerHeap (FingerTree (Prio a) (Elem a) m)
+
+instance H.Heap FingerHeap where
+  empty = pure $ FingerHeap Empty
+  insert x (FingerHeap xs) = FingerHeap <$> cons (Elem x) xs
+  merge (FingerHeap a) (FingerHeap b) = FingerHeap <$> concat' a b
+  splitMin (FingerHeap Empty) = pure Nothing
+  splitMin (FingerHeap xs) = do
+    forceAll xs -- 2 * log n
+    k <- measurement xs
+    (Split _ l (Elem x) r) <- splitTree (k >=) mempty xs -- 3 * log n
+    lr <- concat' l r -- 5 log n
+    pure $ Just (x, FingerHeap lr)
+
+instance H.BoundedHeap FingerHeap where
+  hcost n (H.Insert _) = 2
+  hcost n H.Merge = 5 * log2 n
+  hcost n H.SplitMin = 1 + 10 * log2 (n + 1)
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerHeap a m) where
+  prettyCell (FingerHeap q) = prettyCell q
+
+instance Pretty a => MemoryStructure (FingerHeap (PrettyCell a)) where
+  prettyStructure = prettyCell
+
+-- Sortable Collection
+
+data Key a = NoKey | Key a
+  deriving (Eq, Ord, Show)
+
+instance Semigroup (Key a) where
+  k <> NoKey = k
+  _ <> k = k
+
+instance Monoid (Key a) where
+  mempty = NoKey
+
+instance Measured (Elem a) (Key a) where
+  measure (Elem x) = Key x
+
+newtype FingerSort a m = FingerSort (FingerTree (Key a) (Elem a) m)
+
+rev :: MonadCredit m => [a] -> [a] -> m [a]
+rev [] acc = pure acc
+rev (x : xs) acc = tick >> rev xs (x : acc) 
+
+append :: MonadCredit m => [a] -> [a] -> m [a]
+append [] ys = pure ys
+append (x : xs) ys = tick >> fmap (x:) (append xs ys)
+
+treeToList :: MonadCredit m => [b] -> (a -> m [b]) -> FingerTree v a m -> m [b]
+treeToList acc f Empty = rev acc []
+treeToList acc f (Single x) = do
+  fx <- f x
+  flip rev [] =<< append fx acc
+treeToList acc f (Deep _ s q u) = do
+  s' <- fmap (concatMap id) $ traverse f $ toList s
+  u' <- fmap (concatMap id) $ traverse f $ toList u
+  creditWith q 2
+  q' <- treeToList (u' ++ acc) (fmap (concatMap id) . traverse f . toList . toDigit) =<< force q
+  append s' q'
+
+instance S.Sortable FingerSort where
+  empty = pure $ FingerSort Empty
+  add x (FingerSort xs) = do
+    (l, r) <- split (>= Key x) xs
+    lxr <- concat' l =<< cons (Elem x) r
+    pure $ FingerSort lxr
+  sort (FingerSort xs) = do
+    treeToList [] (\(Elem x) -> tick >> pure [x]) xs
+
+instance S.BoundedSortable FingerSort where
+  scost n (S.Add _) = 1 + 10 * log2 (n + 1)
+  scost n S.Sort = 2 * log2 n + 3 * linear n
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerSort a m) where
+  prettyCell (FingerSort q) = prettyCell q
+
+instance Pretty a => MemoryStructure (FingerSort (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Heap/Base.hs b/src/Test/Credit/Heap/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Heap/Base.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}
+
+module Test.Credit.Heap.Base (HeapOp(..), Heap(..), BoundedHeap(..), H, BH) where
+
+import Control.Monad.Credit
+import Test.Credit
+import Test.QuickCheck
+
+data HeapOp a = Insert a | Merge | SplitMin
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (HeapOp a) where
+  arbitrary = frequency
+    [ (6, Insert <$> arbitrary)
+    , (3, pure SplitMin)
+    , (1, pure Merge)
+    ]
+
+class Heap h where
+  empty :: MonadCredit m => m (h a m)
+  insert :: MonadCredit m => Ord a => a -> h a m -> m (h a m)
+  merge :: MonadCredit m => Ord a => h a m -> h a m -> m (h a m)
+  splitMin :: MonadCredit m => Ord a => h a m -> m (Maybe (a, h a m))
+
+class Heap h => BoundedHeap h where
+  hcost :: Size -> HeapOp a -> Credit
+
+data H h a m = E | H Size (h (PrettyCell a) m)
+
+instance (MemoryCell m (h (PrettyCell a) m)) => MemoryCell m (H h a m) where
+  prettyCell E = pure $ mkMCell "" []
+  prettyCell (H _ h) = prettyCell h
+
+instance (MemoryStructure (h (PrettyCell a))) => MemoryStructure (H h a) where
+  prettyStructure E = pure $ mkMCell "" []
+  prettyStructure (H _ h) = prettyStructure h
+
+act :: (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m)
+act sz h (Insert x) = H (sz + 1) <$> insert (PrettyCell x) h
+act sz h Merge = pure $ H sz h
+act sz h SplitMin = do
+  m <- splitMin h
+  case m of
+    Nothing -> pure E
+    Just (_, h') -> pure $ H (max 0 (sz - 1)) h'
+
+instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (H h a) (HeapOp a) where
+  create = E
+  action E op = (hcost @h 0 op, empty >>= flip (act 0) op)
+  action (H sz h) op = (hcost @h sz op, act sz h op)
+
+size :: H h a m -> Size
+size E = 0
+size (H sz _) = sz
+
+data BH h a m = BH (H h a m) (H h a m)
+
+instance (MemoryCell m (h (PrettyCell a) m)) => MemoryCell m (BH h a m) where
+  prettyCell (BH h1 h2) = do
+    h1' <- prettyCell h1
+    h2' <- prettyCell h2
+    pure $ mkMCell "Merge" [h1', h2']
+
+instance (MemoryStructure (h (PrettyCell a))) => MemoryStructure (BH h a) where
+  prettyStructure (BH h1 h2) = do
+    h1' <- prettyStructure h1
+    h2' <- prettyStructure h2
+    pure $ mkMCell "Merge" [h1', h2']
+
+act1 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m)
+act1 op (BH h1 h2) = do
+  h1' <- case h1 of
+    E -> empty
+    H _ h -> pure h
+  h1'' <- act (size h1) h1' op 
+  pure $ BH h1'' h2
+
+act2 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m)
+act2 op (BH h1 h2) = do
+  h2' <- case h2 of
+    E -> empty
+    H _ h -> pure h
+  h2'' <- act (size h2) h2' op 
+  pure $ BH h1 h2''
+
+mergeH :: (MonadInherit m, Heap h, Ord a) => H h a m -> H h a m -> m (H h a m)
+mergeH E E = pure E
+mergeH (H sz1 h1) E = pure $ H sz1 h1
+mergeH E (H sz2 h2) = pure $ H sz2 h2
+mergeH (H sz1 h1) (H sz2 h2) = H (sz1 + sz2) <$> merge h1 h2
+
+instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (BH h a) (HeapOp a) where
+  create = BH E E
+  action (BH h1 h2) (Insert a) = (hcost @h (size h1) (Insert a),      act1 (Insert a) (BH h1 h2))
+  action (BH h1 h2) SplitMin   = (hcost @h (size h2) SplitMin,        act2 SplitMin (BH h1 h2))
+  action (BH h1 h2) Merge      = (hcost @h (size h1 + size h2) Merge, BH E <$> mergeH h1 h2)
diff --git a/src/Test/Credit/Heap/Binomial.hs b/src/Test/Credit/Heap/Binomial.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Heap/Binomial.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Test.Credit.Heap.Binomial where
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Heap.Base
+
+data Tree a = Node Int a [Tree a]
+  deriving (Eq, Ord, Show)
+
+rank :: Tree a -> Int
+rank (Node r _ _) = r
+
+root :: Tree a -> a
+root (Node _ x _) = x
+
+rev :: MonadCredit m => [a] -> [a] -> m [a]
+rev [] acc = pure acc
+rev (x : xs) acc = tick >> rev xs (x : acc)
+
+link :: Ord a => Tree a -> Tree a -> Tree a
+link t1@(Node r x1 c1) t2@(Node _ x2 c2)
+  | x1 <= x2 = Node (r+1) x1 (t2:c1)
+  | otherwise = Node (r+1) x2 (t1:c2)
+
+insTree :: MonadCredit m => Ord a => Tree a -> [Tree a] -> m [Tree a]
+insTree t [] = pure [t]
+insTree t ts@(t':ts')
+  | rank t < rank t' = pure $ t:ts
+  | otherwise = tick >> insTree (link t t') ts'
+
+mrg :: MonadCredit m => Ord a => [Tree a] -> [Tree a] -> m [Tree a]
+mrg ts1 [] = pure ts1
+mrg [] ts2 = pure ts2
+mrg ts1@(t1:ts1') ts2@(t2:ts2')
+  | rank t1 < rank t2 = tick >> (t1 :) <$> mrg ts1' ts2
+  | rank t2 < rank t1 = tick >> (t2 :) <$> mrg ts1 ts2'
+  | otherwise = tick >> do
+    insTree (link t1 t2) =<< mrg ts1' ts2'
+
+removeMinTree :: MonadCredit m => Ord a => [Tree a] -> m (Tree a, [Tree a])
+removeMinTree [] = error "removeMinTree"
+removeMinTree [t] = pure (t, [])
+removeMinTree (t:ts) = tick >> do
+  (t', ts') <- removeMinTree ts
+  pure $ if root t <= root t' then (t, ts) else (t', t:ts')
+
+data Binomial a m = Binomial Size (Thunk m (Lazy m) [Tree a])
+
+allZeros :: Size -> Credit
+allZeros 0 = 0
+allZeros n = (fromIntegral $ (n + 1) `mod` 2) + allZeros (n `div` 2)
+
+instance Heap Binomial where
+  empty = do
+    t <- delay $ Lazy $ pure []
+    pure $ Binomial 0 t
+  insert x (Binomial n h) = do
+    ts <- delay $ Lazy $ do 
+      creditWith h (allZeros n)
+      h' <- force h
+      insTree (Node 0 x []) h'
+    creditWith ts 2
+    pure $ Binomial (n + 1) ts
+  merge (Binomial n1 t1) (Binomial n2 t2) = do
+    t1 `creditWith` (allZeros n1)
+    ts1 <- force t1
+    t2 `creditWith` (allZeros n2)
+    ts2 <- force t2
+    ts <- delay $ Lazy $ mrg ts1 ts2
+    ts `creditWith` (log2 (n1 + n2))
+    pure $ Binomial (n1 + n2) ts
+  splitMin (Binomial n t) = do
+    creditWith t (log2 n)
+    ts <- force t
+    case ts of
+      [] -> pure Nothing
+      _ -> do
+        (Node _ x ts1, ts2) <- removeMinTree ts
+        t' <- delay $ Lazy $ do
+          rts1 <- rev ts1 []
+          mrg rts1 ts2
+        creditWith t' (2 * log2 n)
+        pure $ Just (x, Binomial (max 0 (n - 1)) t')
+
+instance BoundedHeap Binomial where
+  hcost _ (Insert _) = 2
+  hcost n Merge = 3 * log2 n
+  hcost n SplitMin = 4 * log2 n
+
+instance MemoryCell m a => MemoryCell m (Tree a) where
+  prettyCell (Node r x c) = do
+    r' <- prettyCell r
+    x' <- prettyCell x
+    c' <- mapM prettyCell c
+    pure $ mkMCell "Node" [r', x', mkMList c' Nothing]
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Binomial a m) where
+  prettyCell (Binomial _ t) = do
+    t' <- prettyCell t
+    pure $ mkMCell "Binomial" [t']
+
+instance Pretty a => MemoryStructure (Binomial (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Heap/LazyPairing.hs b/src/Test/Credit/Heap/LazyPairing.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Heap/LazyPairing.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE GADTs #-}
+
+module Test.Credit.Heap.LazyPairing where
+
+import Prettyprinter (Pretty)
+
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Heap.Base
+
+-- Okasaki does not present an amortized analysis and instead merely conjectures
+-- that they have O(log n) amortized cost for insert and splitMin (Section 6.5).
+-- An amortized analysis in a sequential setting is given by Nipkow and Brinkop
+-- in 'Amortized Complexity Verified' (2019), Section 8.
+-- Below we generalize it to the persistent setting.
+
+data LazyPairing a s
+  = Empty
+  | Heap Size a (LazyPairing a s) (PThunk s (LazyPairing a s))
+  -- ^ Changed from Okasaki is that we annotate the size of the thunk.
+  --   Invariant: For 'Heap sm x a m', we have either:
+  --   - 'a' is Empty and 'm' has (log2 sm) credits
+  --   - 'a' is not Empty and 'm' has (2 * log2 sm) credits
+  --   - Right before forcing, 'm' has (3 * log2 sm) credits
+
+size :: LazyPairing a s -> Size
+size Empty = 0
+size (Heap sm _ a _) = 1 + sm + size a
+
+data PLazyCon m a where
+  Em :: PLazyCon m (LazyPairing a m)
+  Link :: Ord a => Size -> LazyPairing a m -> LazyPairing a m -> Thunk m (PLazyCon m) (LazyPairing a m) -> PLazyCon m (LazyPairing a m)
+  -- ^ Merging 'h = Link(a, b, m)' costs one tick and performs two links, and assigns some credits to 'm'.
+  --   Because 'link a b' costs 'log2 (sa + sb)' credits, we have total costs of:
+  --     2 + 2*log2 (sa + sb + sm) + 2*log2 (sa + sb) + 2*log2 sm
+  --     <= 6 * log2 sh (since sa + sb + sm <= sh)
+
+instance MonadCredit m => HasStep (PLazyCon m) m where
+  step Em = pure Empty
+  step (Link sm a b m) = tick >> do -- 1
+    creditWith m (log2 sm) -- log2 sm
+    m <- force m -- free
+    ab <- link a b -- log2 (sa + sb)
+    link ab m -- log2 (sa + sb + sm)
+
+type PThunk s = Thunk s (PLazyCon s)
+
+data NEHeap s a = NEHeap Size a (LazyPairing a s) (PThunk s (LazyPairing a s))
+
+-- | 'mergePairs' costs up to 'log2 (sz + sa)' credits
+mergePairs :: MonadCredit m => Ord a => NEHeap m a -> LazyPairing a m -> m (LazyPairing a m)
+mergePairs (NEHeap sm x Empty m) a = do
+  creditWith m (log2 sm)
+  pure $ Heap sm x a m
+mergePairs (NEHeap sm x b m) a = do
+  t <- delay $ Link sm a b m
+  let sz = size a + size b + sm
+  creditWith t (log2 sz)
+  pure $ Heap sz x Empty t
+
+-- | 'link' costs up to 'log2 (sz + sa) + 1' credits
+link :: MonadCredit m => Ord a => LazyPairing a m -> LazyPairing a m -> m (LazyPairing a m)
+link a Empty = pure a
+link Empty b = pure b
+link a@(Heap sa x a1 a2) b@(Heap sb y b1 b2)
+  | x <= y    = mergePairs (NEHeap sa x a1 a2) b
+  | otherwise = mergePairs (NEHeap sb y b1 b2) a 
+
+instance Heap LazyPairing where
+  empty = pure Empty
+  insert x a = do
+    t <- delay $ Em
+    merge (Heap 0 x Empty t) a
+  -- | 'merge' costs '1 + log2 (sa + sb)' credits
+  merge a b = tick >> link a b
+  splitMin Empty = pure Nothing
+  splitMin (Heap sm x a m) = do
+    creditWith m (2 * log2 sm) -- in case 'a' is Empty
+    m <- force m
+    am <- merge a m
+    pure $ Just (x, am)
+
+instance BoundedHeap LazyPairing where
+  hcost n (Insert _) = 1 + log2 (n + 1)
+  hcost n Merge = 1 + log2 (n + 1)
+  hcost n SplitMin = 1 + 3 * log2 (n + 1)
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (PLazyCon m a) where
+  prettyCell Em = pure $ mkMCell "Empty" []
+  prettyCell (Link _ a b m) = do
+    a' <- prettyCell a
+    b' <- prettyCell b
+    m' <- prettyCell m
+    pure $ mkMCell "Link" [a', b', m']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (LazyPairing a m) where
+  prettyCell Empty = pure $ mkMCell "Empty" []
+  prettyCell (Heap sz x a m) = do
+    sz' <- prettyCell sz
+    x' <- prettyCell x
+    a' <- prettyCell a
+    m' <- prettyCell m
+    pure $ mkMCell "Heap" [sz', x', a', m']
+
+instance Pretty a => MemoryStructure (LazyPairing (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Heap/Pairing.hs b/src/Test/Credit/Heap/Pairing.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Heap/Pairing.hs
@@ -0,0 +1,59 @@
+module Test.Credit.Heap.Pairing where
+
+import Prettyprinter (Pretty)
+
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Heap.Base
+
+-- Binary pairing heaps as in Exercise 5.8 of Okasaki's book.
+
+data PairingHeap a m
+  = Nil
+  | Heap a (PairingHeap a m) (PairingHeap a m)
+
+-- | At the root, the right child is Empty.
+data Pairing a m = Empty | Root a (PairingHeap a m)
+
+link :: Ord a => Pairing a m -> Pairing a m -> Pairing a m
+link Empty b = b
+link a Empty = a
+link (Root x a) (Root y b)
+  | x <= y    = Root x (Heap y b a)
+  | otherwise = Root y (Heap x a b)
+
+mergePairs :: (MonadCredit m, Ord a) => PairingHeap a m -> m (Pairing a m)
+mergePairs Nil = pure $ Empty
+mergePairs (Heap x a1 Nil) = pure $ Root x a1
+mergePairs (Heap x a1 (Heap y a2 a3)) = tick >> link ((link (Root x a1) (Root y a2))) <$> mergePairs a3
+
+instance Heap Pairing where
+  empty = pure Empty
+  insert x h = merge (Root x Nil) h
+  merge a b = tick >> pure (link a b)
+  splitMin Empty = pure Nothing
+  splitMin (Root x h) = Just . (x,) <$> mergePairs h
+
+-- We can only prove a log(n) bound for insert, but this seems to work (as conjectured by Okasaki and others).
+instance BoundedHeap Pairing where
+  hcost n (Insert _) = 1
+  hcost n Merge = 1
+  hcost n SplitMin = 5 * log2 (n + 1)
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (PairingHeap a m) where
+  prettyCell Nil = pure $ mkMCell "Nil" []
+  prettyCell (Heap a l r) = do
+    a' <- prettyCell a
+    l' <- prettyCell l
+    r' <- prettyCell r
+    pure $ mkMCell "Heap" [a', l', r']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Pairing a m) where
+  prettyCell Empty = pure $ mkMCell "Empty" []
+  prettyCell (Root a l) = do
+    a' <- prettyCell a
+    l' <- prettyCell l
+    pure $ mkMCell "Root" [a', l']
+
+instance Pretty a => MemoryStructure (Pairing (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Heap/Scheduled.hs b/src/Test/Credit/Heap/Scheduled.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Heap/Scheduled.hs
@@ -0,0 +1,153 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Test.Credit.Heap.Scheduled where
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit hiding (exec)
+import Test.Credit
+import Test.Credit.Heap.Base
+
+data Stream m a
+  = SCons a (Stream m a)
+  | SNil
+  | SIndirect (Thunk m (Lazy m) (Stream m a))
+
+indirect :: MonadCredit m => m (Stream m a) -> m (Stream m a)
+indirect = fmap SIndirect . delay . Lazy
+
+credit :: MonadCredit m => Credit -> Stream m a -> m ()
+credit cr (SIndirect i) = creditWith i cr
+credit _ _ = pure ()
+
+-- | Smart destructor for streams, consuming one credit
+smatch :: MonadCredit m => Stream m a -- ^ Scrutinee
+       -> m b -- ^ Nil case
+       -> (a -> Stream m a -> m b) -- ^ Cons case
+       -> m b
+smatch x nil cons = tick >> eval x
+  where
+    eval x = case x of
+      SCons a as -> cons a as
+      SNil -> nil
+      SIndirect i -> force i >>= eval
+
+data Tree a = Node a [Tree a]
+  deriving (Eq, Ord, Show)
+
+data Digit a = Zero | One (Tree a)
+  deriving (Eq, Ord, Show)
+
+type Schedule m a = [Stream m (Digit a)]
+
+data Scheduled a m = Scheduled (Stream m (Digit a)) (Schedule m a)
+
+link :: Ord a => Tree a -> Tree a -> Tree a
+link t1@(Node x1 c1) t2@(Node x2 c2)
+  | x1 <= x2 = Node x1 (t2:c1)
+  | otherwise = Node x2 (t1:c2)
+
+insTree :: MonadCredit m => Ord a => Tree a -> Stream m (Digit a) -> m (Stream m (Digit a))
+insTree t s = smatch s
+  (pure $ SCons (One t) SNil)
+  (\d ds -> case d of
+    Zero -> pure $ SCons (One t) ds
+    One t' -> indirect $ do
+      SCons Zero <$> insTree (link t t') ds)
+
+mrg :: MonadCredit m => Ord a => Stream m (Digit a) -> Stream m (Digit a) -> m (Stream m (Digit a))
+mrg ds1 ds2 = credit 1 ds1 >> smatch ds1
+  (pure ds2)
+  (\d1 ds1 -> credit 1 ds1 >> smatch ds2
+    (pure $ SCons d1 ds1)
+    (\d2 ds2 -> case (d1, d2) of
+      (Zero, _) -> SCons d2 <$> mrg ds1 ds2
+      (_, Zero) -> SCons d1 <$> mrg ds1 ds2
+      (One t1, One t2) -> SCons Zero <$> (insTree (link t1 t2) =<< mrg ds1 ds2)))
+
+normalize :: MonadCredit m => Ord a => Stream m (Digit a) -> m (Stream m (Digit a))
+normalize ds = credit 1 ds >> smatch ds
+    (pure SNil)
+    (\d ds -> SCons d <$> normalize ds)
+
+exec :: MonadCredit m => Schedule m a -> m (Schedule m a)
+exec [] = pure []
+exec (ds:dss) = credit 1 ds >> smatch ds
+  (pure dss)
+  (\d job -> case d of
+    Zero -> pure $ job:dss
+    One _ -> pure dss)
+
+removeMinTree :: MonadCredit m => Ord a => Stream m (Digit a) -> m (Tree a, Stream m (Digit a))
+removeMinTree ds = credit 1 ds >> smatch ds
+  (fail "removeMinTree: empty stream")
+  (\d ds -> case d of
+      Zero -> do 
+        (t', ds') <- removeMinTree ds
+        pure (t', SCons Zero ds')
+      One (t@(Node x _)) -> credit 1 ds >> smatch ds
+        (pure (t, SNil))
+        (\_ _ -> do
+          (t'@(Node x' _), ds') <- removeMinTree ds
+          if x <= x'
+            then pure (t, SCons Zero ds)
+            else pure (t', SCons (One t) ds')))
+
+revOneStream :: MonadCredit m => [Tree a] -> Stream m (Digit a) -> m (Stream m (Digit a))
+revOneStream [] acc = pure acc
+revOneStream (t:ts) acc = tick >> revOneStream ts (SCons (One t) acc)
+
+instance Heap Scheduled where
+  empty = pure $ Scheduled SNil []
+  insert x (Scheduled ds sched) = do
+    ds' <- insTree (Node x []) ds -- 1
+    sched' <- exec =<< exec (ds':sched) -- 2 + 2
+    pure $ Scheduled ds' sched'
+  merge (Scheduled ds1 _) (Scheduled ds2 _) = do
+    normalize ds1 -- log2 n1
+    normalize ds2 -- log2 n2
+    ds <- mrg ds1 ds2 -- 5 * log2 (n1 + n2)
+    normalize ds -- log2 (n1 + n2)
+    pure $ Scheduled ds []
+  splitMin (Scheduled ds sched) = smatch ds
+    (pure Nothing)
+    (\_ _ -> do
+      (Node x c, ds') <- removeMinTree ds -- 4 * log2 n
+      c' <- revOneStream c SNil -- log2 n
+      ds'' <- mrg c' ds' -- 5 * log2 (n1 + n2)
+      normalize ds'' -- log2 (n1 + n2)
+      pure (Just (x, Scheduled ds'' [])))
+
+instance BoundedHeap Scheduled where
+  hcost _ (Insert _) = 5
+  hcost n Merge = 4 + 8 * log2 n
+  hcost n SplitMin = 1 + 5 * log2 n + 6 * log2 (2 * n)
+
+instance MemoryCell m a => MemoryCell m (Tree a) where
+  prettyCell (Node x c) = do
+    x' <- prettyCell x
+    c' <- mapM prettyCell c
+    pure $ mkMCell "Node" [x', mkMList c' Nothing]
+
+instance MemoryCell m a => MemoryCell m (Digit a) where
+  prettyCell Zero = pure $ mkMCell "Zero" []
+  prettyCell (One t) = mkMCell "One" . (:[]) <$> prettyCell t
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where
+  prettyCell xs = mkMList <$> toList xs <*> toHole xs
+    where
+      toList SNil = pure $ []
+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs
+      toList (SIndirect t) = pure $ []
+
+      toHole SNil = pure $ Nothing
+      toHole (SCons x xs) = toHole xs
+      toHole (SIndirect t) = Just <$> prettyCell t
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Scheduled a m) where
+  prettyCell (Scheduled ds sched) = do
+    ds' <- prettyCell ds
+    sched' <- mapM prettyCell sched
+    pure $ mkMCell "Scheduled" [ds', mkMList sched' Nothing]
+
+instance Pretty a => MemoryStructure (Scheduled (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Queue/Bankers.hs b/src/Test/Credit/Queue/Bankers.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Queue/Bankers.hs
@@ -0,0 +1,62 @@
+module Test.Credit.Queue.Bankers where
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Queue.Base
+import Test.Credit.Queue.Streams
+
+data BQueue a m = BQueue
+  { front :: Stream m a
+  , flen :: !Int
+  , rear :: Stream m a
+  , rlen :: !Int
+  }
+
+bqueue :: MonadInherit m => BQueue a m -> m (BQueue a m)
+bqueue (BQueue f fl r rl) = do
+  ifIndirect f (`hasAtLeast` fromIntegral rl)
+  if fl >= rl 
+    then pure $ BQueue f fl r rl
+    else do
+      r' <- delay (SReverse r SNil)
+      r' `creditWith` 1
+      f' <- delay (SAppend f (SIndirect r'))
+      pure $ BQueue (SIndirect f') (fl + rl) SNil 0
+
+instance Queue BQueue where
+  empty = pure $ BQueue SNil 0 SNil 0
+  snoc (BQueue f fl r rl) x = do
+    credit f
+    bqueue (BQueue f fl (SCons x r) (rl + 1))
+  uncons (BQueue f fl r rl) = do
+    credit f >> credit f
+    smatch f
+      (\x f -> do
+        q <- bqueue (BQueue f (fl - 1) r rl)
+        pure $ Just (x, q))
+      (pure Nothing)
+
+isEmpty :: BQueue a m -> Bool
+isEmpty (BQueue _ flen _ rlen) = flen == 0 && rlen == 0
+
+lazyqueue :: MonadInherit m => BQueue a m -> m [a]
+lazyqueue (BQueue f fl r rl) = do
+  f' <- toList f
+  r' <- toList r
+  pure $ f' ++ reverse r'
+
+instance BoundedQueue BQueue where
+  qcost _ (Snoc _) = 2
+  qcost _ Uncons = 4
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BQueue a m) where
+  prettyCell (BQueue f fl r rl) = do
+    f' <- prettyCell f
+    fl' <- prettyCell fl
+    r' <- prettyCell r
+    rl' <- prettyCell rl
+    pure $ mkMCell "Queue" [f', fl', r', rl']
+
+instance Pretty a => MemoryStructure (BQueue (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Queue/Base.hs b/src/Test/Credit/Queue/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Queue/Base.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, UndecidableInstances #-}
+
+module Test.Credit.Queue.Base where
+
+import Control.Monad.Credit
+import Prettyprinter
+import Test.Credit
+import Test.QuickCheck
+
+data QueueOp a = Snoc a | Uncons
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (QueueOp a) where
+  arbitrary = frequency
+    [ (7, Snoc <$> arbitrary)
+    , (3, pure Uncons)
+    ]
+
+class Queue q where
+  empty :: MonadInherit m => m (q a m)
+  snoc :: MonadInherit m => q a m -> a -> m (q a m)
+  uncons :: MonadInherit m => q a m -> m (Maybe (a, q a m))
+
+class Queue q => BoundedQueue q where
+  qcost :: Size -> QueueOp a -> Credit
+
+data Q q a m = E | Q Size (q (PrettyCell a) m)
+
+instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (Q q a) where
+  prettyStructure E = pure $ mkMCell "" []
+  prettyStructure (Q _ q) = prettyStructure q
+
+act :: (MonadInherit m, Queue q) => Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)
+act sz q (Snoc x) = Q (sz + 1) <$> snoc q (PrettyCell x)
+act sz q Uncons = do
+  m <- uncons q
+  case m of
+    Nothing -> pure E
+    Just (_, q') -> pure $ Q (max 0 (sz - 1)) q'
+
+instance (Arbitrary a, BoundedQueue q, Show a) => DataStructure (Q q a) (QueueOp a) where
+  create = E
+  action E op = (qcost @q 0 op, empty >>= flip (act 0) op)
+  action (Q sz q) op = (qcost @q sz op, act sz q op)
diff --git a/src/Test/Credit/Queue/Batched.hs b/src/Test/Credit/Queue/Batched.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Queue/Batched.hs
@@ -0,0 +1,35 @@
+module Test.Credit.Queue.Batched where
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Queue.Base
+
+data Batched a m = Batched [a] [a]
+
+rev :: MonadCount m => [a] -> [a] -> m [a]
+rev [] acc = pure acc
+rev (x : xs) acc = tick >> rev xs (x : acc)
+
+bqueue :: MonadCount m => Batched a m -> m (Batched a m)
+bqueue (Batched [] rear) = rev rear [] >>= \f -> pure $ Batched f []
+bqueue (Batched front rear) = pure $ Batched front rear
+
+instance Queue Batched where
+  empty = pure $ Batched [] []
+  snoc (Batched front rear) x = bqueue (Batched front (x : rear))
+  uncons (Batched [] rear) = pure Nothing
+  uncons (Batched (x:front) rear) = Just . (x,) <$> bqueue (Batched front rear)
+
+instance BoundedQueue Batched where
+  qcost n (Snoc _) = 1
+  qcost n Uncons = linear n
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Batched a m) where
+  prettyCell (Batched f r) = do
+    f' <- prettyCell f
+    r' <- prettyCell r
+    pure $ mkMCell "Queue" [f', r']
+
+instance Pretty a => MemoryStructure (Batched (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Queue/Bootstrapped.hs b/src/Test/Credit/Queue/Bootstrapped.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Queue/Bootstrapped.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE GADTs #-}
+
+module Test.Credit.Queue.Bootstrapped where
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Queue.Base
+
+rev :: MonadCredit m => [a] -> [a] -> m [a]
+rev [] acc = pure acc
+rev (x : xs) acc = tick >> rev xs (x : acc) 
+
+data BLazyCon m a where
+  Rev :: [a] -> BLazyCon m [a]
+
+instance MonadCredit m => HasStep (BLazyCon m) m where
+  step (Rev xs) = rev xs []
+
+type BThunk m = Thunk m (BLazyCon m)
+
+data NEQueue a m = NEQueue
+  { lenfm :: !Int
+  , f :: [a]
+  , m :: Bootstrapped (BThunk m [a]) m
+  , ghost :: BThunk m [a]
+  , lenr :: !Int
+  , r :: [a]
+  }
+
+data Bootstrapped a m = Empty | BQueue (NEQueue a m)
+
+checkQ :: MonadCredit m => NEQueue a m -> m (Bootstrapped a m)
+checkQ q@(NEQueue lenfm f m _ lenr r)
+  | lenr <= lenfm = checkF q
+  | otherwise = do
+    r' <- delay $ Rev r
+    creditWith r' 2
+    m' <- snoc' m r'
+    checkF (NEQueue (lenfm + lenr) f m' r' 0 [])
+
+checkF :: MonadCredit m => NEQueue a m -> m (Bootstrapped a m)
+checkF (NEQueue lenfm [] Empty _ lenr r) = pure Empty
+checkF (NEQueue lenfm [] (BQueue m) ghost lenr r) = do
+  (f, m') <- uncons'' m
+  f' <- force f
+  pure $ BQueue (NEQueue lenfm f' m' ghost lenr r)
+checkF q = pure $ BQueue q
+
+snoc' :: MonadCredit m => Bootstrapped a m -> a -> m (Bootstrapped a m)  
+snoc' Empty x = do
+  ghost <- delay $ Rev undefined -- never forced
+  pure $ BQueue (NEQueue 1 [x] Empty ghost 0 [])
+snoc' (BQueue (NEQueue lenfm f m g lenr r)) x = do
+  creditWith g 1
+  checkQ (NEQueue lenfm f m g (lenr + 1) (x : r))
+
+uncons'' :: MonadCredit m => NEQueue a m -> m (a, Bootstrapped a m)
+uncons'' (NEQueue lenfm (x : f') m g lenr r) = tick >> do
+  creditWith g 1
+  q <- checkQ (NEQueue (lenfm - 1) f' m g lenr r)
+  pure (x, q)
+
+uncons' :: MonadCredit m => Bootstrapped a m -> m (Maybe (a, Bootstrapped a m))
+uncons' Empty = pure Nothing
+uncons' (BQueue ne) = Just <$> uncons'' ne
+
+instance Queue Bootstrapped where
+  empty = pure Empty
+  snoc q x = snoc' q x
+  uncons q = uncons' q
+
+instance BoundedQueue Bootstrapped where
+  qcost n (Snoc _) = 3 * (max 1 (logstar n))
+  qcost n Uncons = 6 * (max 1 (logstar n))
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BLazyCon m a) where
+  prettyCell (Rev xs) = do
+    xs' <- prettyCell xs
+    pure $ mkMCell "Rev" [xs']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Bootstrapped a m) where
+  prettyCell Empty = pure $ mkMCell "Empty" []
+  prettyCell (BQueue (NEQueue lenfm f m _ lenr r)) = do
+    lenfm' <- prettyCell lenfm
+    f' <- prettyCell f
+    m' <- prettyCell m
+    lenr' <- prettyCell lenr
+    r' <- prettyCell r
+    pure $ mkMCell "Queue" [lenfm', f', m', lenr', r']
+
+instance Pretty a => MemoryStructure (Bootstrapped (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Queue/Implicit.hs b/src/Test/Credit/Queue/Implicit.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Queue/Implicit.hs
@@ -0,0 +1,167 @@
+{-# LANGUAGE GADTs, LambdaCase #-}
+
+module Test.Credit.Queue.Implicit where
+
+import Prelude hiding (head, tail)
+import Control.Monad (when, unless)
+import Control.Monad.Credit
+import Prettyprinter (Pretty)
+import Test.Credit.Queue.Base
+
+-- Main idea:
+--  - snoc and tail both cost two credits
+--  - the first credit is used to tick
+--  - We maintain the invariant: In each queue Deep(f, m, r), m has 2 - (|f| - |r|) credits.
+--  - The m thunk represents either a snoc or a tail, and thus requires two credits to force.
+--  - snoc and tail spend their second credit on either the old m to be able to force it,
+--    or on the new m to maintain the invariant.
+
+data Digit a = Zero | One a | Two a a
+  deriving (Eq, Ord)
+
+data Implicit a m
+  = Shallow (Digit a)
+  | Deep (Digit a) (Thunk m (ILazyCon m) (Implicit (a, a) m)) (Digit a)
+
+data ILazyCon m a where
+  IPure :: a -> ILazyCon m a
+  ISnoc :: Thunk m (ILazyCon m) (Implicit a m) -> a -> ILazyCon m (Implicit a m)
+  ITail :: Implicit a m -> ILazyCon m (Implicit a m)
+
+instance MonadCredit m => HasStep (ILazyCon m) m where
+  step (IPure x) = pure x
+  step (ISnoc t p) = do
+    q <- force t
+    snoc' q p
+  step (ITail q) = tail q
+
+isEmpty :: Implicit a m -> Bool
+isEmpty (Shallow Zero) = True
+isEmpty _ = False
+
+head :: MonadCredit m => Implicit a m -> m a
+head q = case q of
+  Shallow (One x) -> pure x
+  Deep (Two x _) _ _ -> pure x
+  Deep (One x) _ _ -> pure x
+  _ -> fail "head: empty queue"
+
+size :: Digit a -> Credit
+size = \case { Zero -> 0; One _ -> 1; Two _ _ -> 2 }
+
+deep :: MonadCredit m => Digit a -> Thunk m (ILazyCon m) (Implicit (a, a) m) -> Digit a -> m (Implicit a m)
+deep f m r = do
+  m `hasAtLeast` (2 - size f + size r)
+  pure $ Deep f m r
+
+snoc' :: MonadCredit m => Implicit a m -> a -> m (Implicit a m)
+snoc' q y = do
+  tick
+  case q of
+    Shallow Zero -> pure $ Shallow (One y)
+    Shallow (One x) -> do
+      middle <- delay $ IPure $ Shallow Zero
+      deep (Two x y) middle Zero
+    Deep front middle Zero -> do
+      middle `creditWith` 1
+      deep front middle (One y)
+    Deep front middle (One x) -> do
+      middle `hasAtLeast` (2 - size front + 1)
+      t <- delay $ ISnoc middle (x, y)
+      if size front == 1
+        then t      `creditWith` 1
+        else middle `creditWith` 1
+      deep front t Zero
+    _ -> fail "snoc: malformed queue"
+
+tail :: MonadCredit m => Implicit a m -> m (Implicit a m)
+tail q = tick >> case q of
+  Shallow (One _) -> pure $ Shallow Zero
+  Deep (Two _ y) m rear -> do
+    creditWith m 1
+    deep (One y) m rear
+  Deep (One _) m rear -> do
+    unless (size rear == 1) $ creditWith m 1
+    m' <- force m
+    if isEmpty m'
+      then pure $ Shallow rear
+      else do
+        (y, z) <- head m'
+        t <- delay $ ITail m'
+        when (size rear == 1) $ creditWith t 1
+        deep (Two y z) t rear
+  _ -> fail "tail: empty queue"
+
+instance Show a => Show (Digit a) where
+  show Zero = "Zero"
+  show (One a) = "(One " ++ show a ++ ")"
+  show (Two a b) = "(Two " ++ show a ++ " " ++ show b ++ ")"
+
+showThunk :: (MonadLazy m, Show a)
+          => Thunk m (ILazyCon m) (Implicit a m) -> m String
+showThunk t = lazymatch t showImplicit $ \case
+    IPure a -> showImplicit a
+    ISnoc middle xy -> do
+      m <- showThunk middle
+      pure $ "(snoc " ++ m ++ " " ++ show xy ++ ")"
+    ITail q -> do
+      m <- showImplicit q
+      pure $ "(tail " ++ m ++ ")"
+
+showImplicit :: (MonadLazy m, Show a)
+             => Implicit a m -> m String
+showImplicit (Shallow d) = do
+  pure $ "(Shallow " ++ show d ++ ")"
+showImplicit (Deep f m r) = do
+  m' <- showThunk m
+  pure $ "(Deep " ++ show f ++ " " ++ m' ++ " "
+                  ++ show r ++ ")"
+
+instance Queue Implicit where
+  empty = pure $ Shallow Zero
+  snoc q y = snoc' q y
+  uncons q =
+    if isEmpty q
+      then pure Nothing
+      else do
+        h <- head q
+        t <- tail q
+        pure $ Just (h, t)
+
+instance BoundedQueue Implicit where
+  qcost _ (Snoc _) = 2
+  qcost _ Uncons = 2
+
+instance MemoryCell m a => MemoryCell m (Digit a) where
+  prettyCell Zero = pure $ mkMCell "Zero" []
+  prettyCell (One a) = do
+    a' <- prettyCell a
+    pure $ mkMCell "One" [a']
+  prettyCell (Two a b) = do
+    a' <- prettyCell a
+    b' <- prettyCell b
+    pure $ mkMCell "Two" [a', b']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ILazyCon m a) where
+  prettyCell (IPure x) = do
+    x' <- prettyCell x
+    pure $ mkMCell "IPure" [x']
+  prettyCell (ISnoc t _) = do
+    t' <- prettyCell t
+    pure $ mkMCell "ISnoc" [t']
+  prettyCell (ITail q) = do
+    q' <- prettyCell q
+    pure $ mkMCell "ITail" [q']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Implicit a m) where
+  prettyCell (Shallow d) = do
+    d' <- prettyCell d
+    pure $ mkMCell "Shallow" [d']
+  prettyCell (Deep f m r) = do
+    f' <- prettyCell f
+    m' <- prettyCell m
+    r' <- prettyCell r
+    pure $ mkMCell "Deep" [f', m', r']
+
+instance Pretty a => MemoryStructure (Implicit (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Queue/Physicists.hs b/src/Test/Credit/Queue/Physicists.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Queue/Physicists.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Test.Credit.Queue.Physicists where
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Queue.Base
+
+app :: MonadCredit m => [a] -> [a] -> m [a]
+app [] ys = pure ys
+app (x : xs) ys = tick >> app xs (x : ys)
+
+rev :: MonadCredit m => [a] -> [a] -> m [a]
+rev [] acc = pure acc
+rev (x : xs) acc = tick >> rev xs (x : acc)
+
+data PLazyCon m a where
+  Empty :: PLazyCon m [a]
+  AppRev :: [a] -> [a] -> PLazyCon m [a]
+  Tail :: Thunk m (PLazyCon m) [a] -> PLazyCon m [a]
+
+instance MonadCredit m => HasStep (PLazyCon m) m where
+  step Empty = pure []
+  step (AppRev xs ys) = app xs =<< rev ys []
+  step (Tail xs) = tick >> drop 1 <$> force xs
+
+type PThunk m = Thunk m (PLazyCon m)
+
+data Physicists a m = Queue [a] Int (PThunk m [a]) (PThunk m [a]) Int [a]
+
+checkw :: MonadCredit m => Physicists a m -> m (Physicists a m)
+checkw (Queue working lenf front ghost lenr rear) = case working of
+  [] -> do
+    front' <- force front
+    pure $ Queue front' lenf front ghost lenr rear
+  _ -> pure $ Queue working lenf front ghost lenr rear
+
+check :: MonadCredit m => Physicists a m -> m (Physicists a m)
+check q@(Queue _ lenf front ghost lenr rear) =
+  if lenr <= lenf
+    then do
+      creditWith ghost 1
+      checkw q
+    else do
+      working <- force front
+      front' <- delay $ AppRev working rear
+      creditWith front' 1
+      checkw $ Queue working (lenf + lenr) front' front' 0 []
+
+instance Queue Physicists where
+  empty = do
+    front <- delay Empty
+    pure $ Queue [] 0 front front 0 []
+  snoc (Queue working lenf front ghost lenr rear) x = tick >> do
+    creditWith ghost 1
+    check (Queue working lenf front ghost (lenr + 1) (x : rear))
+  uncons (Queue [] lenf front ghost lenr rear) = tick >> pure Nothing
+  uncons (Queue (x : working) lenf front ghost lenr rear) = tick >> do
+    front' <- delay $ Tail front
+    creditWith front' 1
+    creditWith ghost 1
+    q' <- check $ Queue working (lenf - 1) front' ghost lenr rear
+    pure $ Just (x, q')
+
+instance BoundedQueue Physicists where
+  qcost _ (Snoc _) = 3
+  qcost _ Uncons = 4
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (PLazyCon m a) where
+  prettyCell Empty = pure $ mkMCell "Empty" []
+  prettyCell (AppRev xs ys) = do
+    xs' <- prettyCell xs
+    ys' <- prettyCell ys
+    pure $ mkMCell "AppRev" [xs', ys']
+  prettyCell (Tail xs) = do
+    xs' <- prettyCell xs
+    pure $ mkMCell "Tail" [xs']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Physicists a m) where
+  prettyCell (Queue working lenf front _ lenr rear) = do
+    working' <- prettyCell working
+    lenf' <- prettyCell lenf
+    front' <- prettyCell front
+    lenr' <- prettyCell lenr
+    rear' <- prettyCell rear
+    pure $ mkMCell "Queue" [working', lenf', front', lenr', rear']
+
+instance Pretty a => MemoryStructure (Physicists (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Queue/Realtime.hs b/src/Test/Credit/Queue/Realtime.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Queue/Realtime.hs
@@ -0,0 +1,48 @@
+module Test.Credit.Queue.Realtime where
+
+import Prelude hiding (lookup, reverse)
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit.Queue.Base
+import Test.Credit.Queue.Streams
+
+-- | Delay a computation, but do not consume any credits
+indirect :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)
+indirect t = delay t >>= pure . SIndirect
+
+data RQueue a m = RQueue
+  { front :: Stream m a
+  , rear :: Stream m a
+  , schedule :: Stream m a
+  }
+
+rqueue :: MonadInherit m => RQueue a m -> m (RQueue a m)
+rqueue (RQueue f r s) = credit s >> credit s >> smatch s
+  (\x s -> pure $ RQueue f r s)
+  (do
+    r' <- indirect (SReverse r SNil)
+    f' <- indirect (SAppend f r')
+    credit r' >> evalone r'
+    pure $ RQueue f' SNil f')
+
+instance Queue RQueue where
+  empty = pure $ RQueue SNil SNil SNil
+  snoc (RQueue f r s) x = rqueue (RQueue f (SCons x r) s)
+  uncons (RQueue f r s) = credit f >> credit f >> smatch f
+    (\x f -> rqueue (RQueue f r s) >>= \q -> pure $ Just (x, q))
+    (pure Nothing)
+
+instance BoundedQueue RQueue where
+  qcost _ (Snoc _) = 4
+  qcost _ Uncons = 7
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (RQueue a m) where
+  prettyCell (RQueue f r s) = do
+    f' <- prettyCell f
+    r' <- prettyCell r
+    s' <- prettyCell s
+    pure $ mkMCell "Queue" [f', r', s']
+
+instance Pretty a => MemoryStructure (RQueue (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Queue/Streams.hs b/src/Test/Credit/Queue/Streams.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Queue/Streams.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE GADTs, LambdaCase #-}
+
+module Test.Credit.Queue.Streams (Stream(..), SThunk, SLazyCon(..), smatch, credit, evalone, toList, ifIndirect, test) where
+
+import Control.Monad
+import Control.Monad.Credit
+
+data Stream m a
+  = SCons a (Stream m a)
+  | SNil
+  | SIndirect (SThunk m (Stream m a))
+
+type SThunk m = Thunk m (SLazyCon m)
+
+data SLazyCon m a where
+  SAppend :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)
+  SReverse :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)
+
+instance MonadInherit m => HasStep (SLazyCon m) m where
+  step (SAppend xs ys) = sappend xs ys
+  step (SReverse xs ys) = sreverse xs ys
+
+-- | Smart destructor for streams, consuming one credit
+smatch :: MonadInherit m => Stream m a -- ^ Scrutinee
+       -> (a -> Stream m a -> m b) -- ^ Cons case
+       -> m b -- ^ Nil case
+       -> m b
+smatch x cons nil = tick >> eval x
+  where
+    eval x = case x of
+      SCons a as -> cons a as
+      SNil -> nil
+      SIndirect i -> force i >>= eval
+
+-- | delay a computation, consuming all credits
+taildelay :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)
+taildelay t = do
+  x <- delay t
+  creditAllTo x
+  pure (SIndirect x)
+
+sreverse :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)
+sreverse xs ys = smatch xs
+  (\x xs -> taildelay (SReverse xs (SCons x ys)))
+  (pure ys)
+
+ifIndirect :: Monad m => Stream m a -> (SThunk m (Stream m a) -> m ()) -> m ()
+ifIndirect (SIndirect i) f = f i
+ifIndirect _ _ = pure ()
+
+credit :: MonadInherit m => Stream m a -> m ()
+credit s = ifIndirect s (`creditWith` 1)
+
+evalone :: MonadInherit m => Stream m a -> m ()
+evalone s = ifIndirect s (void . force)
+
+sappend :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)
+sappend xs ys = credit ys >> evalone ys >> smatch xs
+  (\x xs -> SCons x <$> taildelay (SAppend xs ys))
+  (pure ys)
+
+walk s = smatch s (\_ xs -> walk xs) (pure ())
+
+foo :: MonadInherit m => Stream m a -> m ()
+foo s = smatch s (\_ _ -> pure ()) (pure ())
+
+test :: MonadInherit m => m ()
+test = do
+  s <- sappend (SCons 1 SNil) (SCons 2 SNil)
+  credit s >> credit s
+  foo s
+  credit s
+  walk s
+
+toList :: MonadLazy m => Stream m a -> m [a]
+toList SNil = pure []
+toList (SCons x xs) = do
+  xs' <- toList xs
+  pure $ x : xs'
+toList (SIndirect t) = do
+  lazymatch t toList $ \case
+      SAppend xs ys -> do
+        xs' <- toList xs
+        ys' <- toList ys
+        pure $ xs' ++ ys'
+      SReverse xs ys -> do
+        xs' <- toList xs
+        ys' <- toList ys
+        pure $ reverse xs' ++ ys'
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SLazyCon m a) where
+  prettyCell (SAppend xs ys) = do
+    xs' <- prettyCell xs
+    ys' <- prettyCell ys
+    pure $ mkMCell "SAppend" [xs', ys']
+  prettyCell (SReverse xs ys) = do
+    xs' <- prettyCell xs
+    ys' <- prettyCell ys
+    pure $ mkMCell "SReverse" [xs', ys']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where
+  prettyCell xs = mkMList <$> toList xs <*> toHole xs
+    where
+      toList SNil = pure $ []
+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs
+      toList (SIndirect t) = pure $ []
+
+      toHole SNil = pure $ Nothing
+      toHole (SCons x xs) = toHole xs
+      toHole (SIndirect t) = Just <$> prettyCell t
diff --git a/src/Test/Credit/RandomAccess/Base.hs b/src/Test/Credit/RandomAccess/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/RandomAccess/Base.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}
+
+module Test.Credit.RandomAccess.Base where
+
+import Prelude hiding (lookup)
+import Control.Monad.Credit
+import Test.Credit
+import Test.QuickCheck
+
+data RandomAccessOp a = Cons a | Uncons | Lookup Int | Update Int a
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (RandomAccessOp a) where
+  arbitrary = frequency
+    [ (13, Cons <$> arbitrary)
+    , (6, pure Uncons)
+    , (1, Lookup <$> arbitrary)
+    , (1, Update <$> arbitrary <*> arbitrary)
+    ]
+
+class RandomAccess q where
+  empty :: MonadCredit m => m (q a m)
+  cons :: MonadCredit m => a -> q a m  -> m (q a m)
+  uncons :: MonadCredit m => q a m -> m (Maybe (a, q a m))
+  lookup :: MonadCredit m => Int -> q a m -> m (Maybe a)
+  update :: MonadCredit m => Int -> a -> q a m -> m (q a m)
+
+class RandomAccess q => BoundedRandomAccess q where
+  qcost :: Size -> RandomAccessOp a -> Credit
+
+data RA q a m = E | RA Size (q (PrettyCell a) m)
+
+instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (RA q a m) where
+  prettyCell E = pure $ mkMCell "" []
+  prettyCell (RA _ q) = prettyCell q
+
+instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (RA q a) where
+  prettyStructure E = pure $ mkMCell "" []
+  prettyStructure (RA _ q) = prettyStructure q
+
+idx :: Int -> Size -> Int
+idx i sz = if sz <= 0 then 0 else abs (i `mod` fromIntegral sz)
+
+norm :: Size -> RandomAccessOp a -> RandomAccessOp a
+norm sz (Lookup i) = Lookup (idx i sz)
+norm sz (Update i a) = Update (idx i sz) a
+norm _ op = op
+
+act :: (MonadCredit m, RandomAccess q) => Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)
+act sz q (Cons x) = RA (sz + 1) <$> cons (PrettyCell x) q
+act sz q Uncons = do
+  m <- uncons q
+  case m of
+    Nothing -> pure E
+    Just (_, q') -> pure $ RA (max 0 (sz - 1)) q'
+act sz q (Lookup i) = do
+  _ <- lookup i q
+  pure $ RA sz q
+act sz q (Update i a) = RA sz <$> update i (PrettyCell a) q
+
+instance (Arbitrary a, BoundedRandomAccess q, Show a) => DataStructure (RA q a) (RandomAccessOp a) where
+  create = E
+  action E op = (qcost @q 0 (norm 0 op), empty >>= flip (act 0) (norm 0 op))
+  action (RA sz q) op = (qcost @q sz (norm sz op), act sz q (norm sz op))
diff --git a/src/Test/Credit/RandomAccess/Binary.hs b/src/Test/Credit/RandomAccess/Binary.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/RandomAccess/Binary.hs
@@ -0,0 +1,174 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Test.Credit.RandomAccess.Binary where
+
+import Prelude hiding (lookup)
+import Prettyprinter (Pretty)
+import Control.Monad.Credit hiding (exec)
+import Test.Credit
+import Test.Credit.RandomAccess.Base
+
+data Stream m a
+  = SCons a (Stream m a)
+  | SNil
+  | SIndirect (Thunk m (Lazy m) (Stream m a))
+
+indirect :: MonadCredit m => m (Stream m a) -> m (Stream m a)
+indirect = fmap SIndirect . delay . Lazy
+
+credit :: MonadCredit m => Credit -> Stream m a -> m ()
+credit cr (SIndirect i) = creditWith i cr
+credit _ _ = pure ()
+
+-- | Smart destructor for streams, consuming one credit
+smatch :: MonadCredit m => Stream m a -- ^ Scrutinee
+       -> m b -- ^ Nil case
+       -> (a -> Stream m a -> m b) -- ^ Cons case
+       -> m b
+smatch x nil cons = tick >> eval x
+  where
+    eval x = case x of
+      SCons a as -> cons a as
+      SNil -> nil
+      SIndirect i -> force i >>= eval
+
+data Tree a = Leaf a | Node Int (Tree a) (Tree a)
+  deriving (Eq, Ord, Show)
+
+data Digit a = Zero | One (Tree a) | Two (Tree a) (Tree a)
+  deriving (Eq, Ord, Show)
+
+size :: Tree a -> Int
+size (Leaf _) = 1
+size (Node w _ _) = w
+
+link :: Tree a -> Tree a -> Tree a
+link t1 t2 = Node (size t1 + size t2) t1 t2
+
+consTree :: MonadCredit m => Tree a -> Stream m (Digit a) -> m (Stream m (Digit a))
+consTree t ts = smatch ts
+  (pure $ SCons (One t) SNil)
+  (\d ds -> case d of
+    Zero -> pure $ SCons (One t) ds
+    One t' -> credit 1 ds >> pure (SCons (Two t t') ds)
+    Two t2 t3 -> do
+      ds' <- indirect $ consTree (link t2 t3) ds
+      credit 1 ds'
+      pure $ SCons (One t) ds')
+
+unconsTree :: MonadCredit m => Stream m (Digit a) -> m (Maybe (Tree a, Stream m (Digit a)))
+unconsTree ts = smatch ts
+  (pure Nothing)
+  (\d ds -> case d of
+    One t -> credit 1 ds >> smatch ds
+      (pure $ Just (t, SNil))
+      (\_ _ -> pure $ Just (t, SCons Zero ds))
+    Two t t' -> pure $ Just (t, SCons (One t') ds)
+    Zero -> do
+      ds' <- unconsTree ds
+      case ds' of
+        Just (Node _ t1 t2, ds'') -> pure $ Just (t1, SCons (One t2) ds'')
+        _ -> pure Nothing)
+
+lookupTree :: MonadCredit m => Int -> Tree a -> m (Maybe a)
+lookupTree 0 (Leaf x) = pure $ Just x
+lookupTree i (Leaf _) = pure Nothing
+lookupTree i (Node w t1 t2)
+  | i < w `div` 2 = tick >> lookupTree i t1
+  | otherwise = tick >> lookupTree (i - w `div` 2) t2
+
+updateTree :: MonadCredit m => Int -> a -> Tree a -> m (Tree a)
+updateTree 0 y (Leaf _) = pure $ Leaf y
+updateTree i _ (Leaf x) = pure $ Leaf x
+updateTree i y (Node w t1 t2)
+  | i < w `div` 2 = tick >> do
+      t1' <- updateTree i y t1
+      pure $ Node w t1' t2
+  | otherwise = tick >> do
+      t2' <- updateTree (i - w `div` 2) y t2
+      pure $ Node w t1 t2'
+
+newtype BinaryRA a m = BinaryRA { unBinaryRA :: Stream m (Digit a) }
+
+instance RandomAccess BinaryRA where
+  empty = pure $ BinaryRA SNil
+  cons x (BinaryRA ts) = BinaryRA <$> consTree (Leaf x) ts
+  uncons (BinaryRA ts) = do
+    m <- unconsTree ts
+    case m of
+      Just (Leaf x, ts') -> pure $ Just (x, BinaryRA ts')
+      _ -> pure Nothing
+  lookup i (BinaryRA ts) = smatch ts
+    (pure Nothing)
+    (\d ds -> case d of
+      Zero -> lookup i (BinaryRA ds)
+      One t ->
+        if i < size t
+          then lookupTree i t
+          else credit 1 ds >> lookup (i - size t) (BinaryRA ds)
+      Two t1 t2 ->
+        if i < size t1
+          then lookupTree i t1
+          else let j = i - size t1 in
+            if j < size t2
+              then lookupTree j t2
+              else lookup (j - size t2) (BinaryRA ds))
+  update i y (BinaryRA ts) = smatch ts
+    (pure $ BinaryRA SNil)
+    (\d ds -> case d of
+      Zero -> BinaryRA . (SCons Zero) . unBinaryRA <$> update i y (BinaryRA ds)
+      One t ->
+        if i < size t
+          then BinaryRA . (flip SCons ds) . One <$> updateTree i y t
+          else credit 1 ds >> BinaryRA . (SCons (One t)) . unBinaryRA <$> update (i - size t) y (BinaryRA ds)
+      Two t1 t2 ->
+        if i < size t1
+          then BinaryRA . (flip SCons ds) . flip Two t2 <$> updateTree i y t1
+          else let j = i - size t1 in
+            if j < size t2
+              then BinaryRA . (flip SCons ds) . Two t1 <$> updateTree j y t2
+              else BinaryRA . (SCons (Two t1 t2)) . unBinaryRA <$> update (j - size t2) y (BinaryRA ds))
+
+instance BoundedRandomAccess BinaryRA where
+  qcost n (Cons _) = 2
+  qcost n Uncons = 3 + log2 n
+  qcost n (Lookup _) = 1 + 3 * log2 n
+  qcost n (Update _ _) = 1 + 3 * log2 n
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where
+  prettyCell xs = mkMList <$> toList xs <*> toHole xs
+    where
+      toList SNil = pure $ []
+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs
+      toList (SIndirect t) = pure $ []
+
+      toHole SNil = pure $ Nothing
+      toHole (SCons x xs) = toHole xs
+      toHole (SIndirect t) = Just <$> prettyCell t
+
+instance MemoryCell m a => MemoryCell m (Tree a) where
+  prettyCell (Leaf x) = do
+    x' <- prettyCell x
+    pure $ mkMCell "Leaf" [x']
+  prettyCell (Node w t1 t2) = do
+    t1' <- prettyCell t1
+    t2' <- prettyCell t2
+    pure $ mkMCell "Node" [t1', t2']
+
+instance MemoryCell m a => MemoryCell m (Digit a) where
+  prettyCell Zero = pure $ mkMCell "Zero" []
+  prettyCell (One t) = do
+    t' <- prettyCell t
+    pure $ mkMCell "One" [t']
+  prettyCell (Two t1 t2) = do
+    t1' <- prettyCell t1
+    t2' <- prettyCell t2
+    pure $ mkMCell "Two" [t1', t2']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BinaryRA a m) where
+  prettyCell (BinaryRA ts) = do
+    ts' <- prettyCell ts
+    pure $ mkMCell "BinaryRA" [ts']
+
+instance Pretty a => MemoryStructure (BinaryRA (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/RandomAccess/Zeroless.hs b/src/Test/Credit/RandomAccess/Zeroless.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/RandomAccess/Zeroless.hs
@@ -0,0 +1,200 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Test.Credit.RandomAccess.Zeroless where
+
+import Prelude hiding (lookup)
+import Prettyprinter (Pretty)
+import Control.Monad.Credit hiding (exec)
+import Test.Credit
+import Test.Credit.RandomAccess.Base
+
+data Stream m a
+  = SCons a (Stream m a)
+  | SNil
+  | SIndirect (Thunk m (Lazy m) (Stream m a))
+
+indirect :: MonadCredit m => m (Stream m a) -> m (Stream m a)
+indirect = fmap SIndirect . delay . Lazy
+
+credit :: MonadCredit m => Credit -> Stream m a -> m ()
+credit cr (SIndirect i) = creditWith i cr
+credit _ _ = pure ()
+
+-- | Smart destructor for streams, consuming one credit
+smatch :: MonadCredit m => Stream m a -- ^ Scrutinee
+       -> m b -- ^ Nil case
+       -> (a -> Stream m a -> m b) -- ^ Cons case
+       -> m b
+smatch x nil cons = tick >> eval x
+  where
+    eval x = case x of
+      SCons a as -> cons a as
+      SNil -> nil
+      SIndirect i -> force i >>= eval
+
+data Tree a = Leaf a | Node Int (Tree a) (Tree a)
+  deriving (Eq, Ord, Show)
+
+data Digit a = One (Tree a) | Two (Tree a) (Tree a) | Three (Tree a) (Tree a) (Tree a)
+  deriving (Eq, Ord, Show)
+
+size :: Tree a -> Int
+size (Leaf _) = 1
+size (Node w _ _) = w
+
+link :: Tree a -> Tree a -> Tree a
+link t1 t2 = Node (size t1 + size t2) t1 t2
+
+consTree :: MonadCredit m => Tree a -> Stream m (Digit a) -> m (Stream m (Digit a))
+consTree t1 ts = smatch ts
+  (pure $ SCons (One t1) SNil)
+  (\d ds -> case d of
+    One t2 -> pure $ SCons (Two t1 t2) ds
+    Two t2 t3 -> credit 2 ds >> pure (SCons (Three t1 t2 t3) ds)
+    Three t2 t3 t4 -> do
+      ds' <- indirect $ consTree (link t3 t4) ds
+      credit 2 ds'
+      pure $ SCons (Two t1 t2) ds')
+
+unconsTree :: MonadCredit m => Stream m (Digit a) -> m (Maybe (Tree a, Stream m (Digit a)))
+unconsTree ts = smatch ts
+  (pure Nothing)
+  (\d ds -> case d of
+      One t -> smatch ds
+        (pure $ Just (t, SNil))
+        (\_ _ -> do
+          ds' <- indirect $ do
+            ds' <- unconsTree ds
+            case ds' of
+              Just (Node _ t1 t2, ds'') -> do
+                pure $ SCons (Two t1 t2) ds''
+              Nothing -> fail "unconsTree: malformed tree"
+          credit 2 ds'
+          pure $ Just (t, ds'))
+      Two t1 t2 -> credit 2 ds >> pure (Just (t1, SCons (One t2) ds))
+      Three t1 t2 t3 -> pure $ Just (t1, SCons (Two t2 t3) ds))
+
+lookupTree :: MonadCredit m => Int -> Tree a -> m (Maybe a)
+lookupTree 0 (Leaf x) = pure $ Just x
+lookupTree i (Leaf _) = pure Nothing
+lookupTree i (Node w t1 t2)
+  | i < w `div` 2 = tick >> lookupTree i t1
+  | otherwise = tick >> lookupTree (i - w `div` 2) t2
+
+updateTree :: MonadCredit m => Int -> a -> Tree a -> m (Tree a)
+updateTree 0 y (Leaf _) = pure $ Leaf y
+updateTree i _ (Leaf x) = pure $ Leaf x
+updateTree i y (Node w t1 t2)
+  | i < w `div` 2 = tick >> do
+      t1' <- updateTree i y t1
+      pure $ Node w t1' t2
+  | otherwise = tick >> do
+      t2' <- updateTree (i - w `div` 2) y t2
+      pure $ Node w t1 t2'
+
+newtype ZerolessRA a m = ZerolessRA { unZerolessRA :: Stream m (Digit a) }
+
+instance RandomAccess ZerolessRA where
+  empty = pure $ ZerolessRA SNil
+  cons x (ZerolessRA ts) = credit 2 ts >> ZerolessRA <$> consTree (Leaf x) ts
+  uncons (ZerolessRA ts) = credit 2 ts >> do
+    m <- unconsTree ts
+    case m of
+      Just (Leaf x, ts') -> pure $ Just (x, ZerolessRA ts')
+      _ -> pure Nothing
+  lookup i (ZerolessRA ts) = credit 2 ts >> smatch ts
+    (pure Nothing)
+    (\d ds -> case d of
+      One t -> do
+        if i < size t
+          then lookupTree i t
+          else lookup (i - size t) (ZerolessRA ds)
+      Two t1 t2 -> do
+        if i < size t1
+          then lookupTree i t1
+          else let j = i - size t1 in
+            if j < size t2
+              then lookupTree j t2
+              else credit 2 ds >> lookup (j - size t2) (ZerolessRA ds)
+      Three t1 t2 t3 -> do
+        if i < size t1
+          then lookupTree i t1
+          else let j = i - size t1 in
+            if j < size t2
+              then lookupTree j t2
+              else let k = j - size t2 in
+                if k < size t3
+                  then lookupTree k t3
+                  else lookup (k - size t3) (ZerolessRA ds))
+  update i y (ZerolessRA ts) = credit 2 ts >> smatch ts
+    (pure $ ZerolessRA SNil)
+    (\d ds -> case d of
+        One t -> do
+            if i < size t
+              then ZerolessRA . (flip SCons ds) . One <$> updateTree i y t
+              else ZerolessRA . (SCons (One t)) . unZerolessRA <$> update (i - size t) y (ZerolessRA ds)
+        Two t1 t2 -> do
+            if i < size t1
+              then ZerolessRA . (flip SCons ds) . flip Two t2 <$> updateTree i y t1
+              else let j = i - size t1 in
+                if j < size t2
+                  then ZerolessRA . (flip SCons ds) . Two t1 <$> updateTree j y t2
+                  else credit 2 ds >> ZerolessRA . (SCons (Two t1 t2)) . unZerolessRA <$> update (j - size t2) y (ZerolessRA ds)
+        Three t1 t2 t3 -> do
+            if i < size t1
+              then ZerolessRA . (flip SCons ds) . (\t1' -> Three t1' t2 t3) <$> updateTree i y t1
+              else let j = i - size t1 in
+                if j < size t2
+                  then ZerolessRA . (flip SCons ds) . (\t2' -> Three t1 t2' t3) <$> updateTree j y t2
+                  else let k = j - size t2 in
+                    if k < size t3
+                      then ZerolessRA . (flip SCons ds) . Three t1 t2 <$> updateTree k y t3
+                      else ZerolessRA . (SCons (Three t1 t2 t3)) . unZerolessRA <$> update (k - size t3) y (ZerolessRA ds))
+
+instance BoundedRandomAccess ZerolessRA where
+  qcost n (Cons _) = 5
+  qcost n Uncons = 6
+  qcost _ (Lookup i) = 3 + 5 * log2 (fromIntegral i * 2)
+  qcost _ (Update i _) = 3 + 5 * log2 (fromIntegral i * 2)
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where
+  prettyCell xs = mkMList <$> toList xs <*> toHole xs
+    where
+      toList SNil = pure $ []
+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs
+      toList (SIndirect t) = pure $ []
+
+      toHole SNil = pure $ Nothing
+      toHole (SCons x xs) = toHole xs
+      toHole (SIndirect t) = Just <$> prettyCell t
+
+instance MemoryCell m a => MemoryCell m (Tree a) where
+  prettyCell (Leaf x) = do
+    x' <- prettyCell x
+    pure $ mkMCell "Leaf" [x']
+  prettyCell (Node w t1 t2) = do
+    t1' <- prettyCell t1
+    t2' <- prettyCell t2
+    pure $ mkMCell "Node" [t1', t2']
+
+instance MemoryCell m a => MemoryCell m (Digit a) where
+  prettyCell (One t) = do
+    t' <- prettyCell t
+    pure $ mkMCell "One" [t']
+  prettyCell (Two t1 t2) = do
+    t1' <- prettyCell t1
+    t2' <- prettyCell t2
+    pure $ mkMCell "Two" [t1', t2']
+  prettyCell (Three t1 t2 t3) = do
+    t1' <- prettyCell t1
+    t2' <- prettyCell t2
+    t3' <- prettyCell t3
+    pure $ mkMCell "Three" [t1', t2', t3']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ZerolessRA a m) where
+  prettyCell (ZerolessRA ts) = do
+    ts' <- prettyCell ts
+    pure $ mkMCell "ZerolessRA" [ts']
+
+instance Pretty a => MemoryStructure (ZerolessRA (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Sortable/Base.hs b/src/Test/Credit/Sortable/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Sortable/Base.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}
+
+module Test.Credit.Sortable.Base where
+
+import Control.Monad.Credit
+import Test.Credit
+import Test.QuickCheck
+
+data SortableOp a = Add a | Sort
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (SortableOp a) where
+  arbitrary = frequency
+    [ (9, Add <$> arbitrary)
+    , (1, pure Sort)
+    ]
+
+class Sortable q where
+  empty :: MonadCredit m => m (q a m)
+  add :: MonadCredit m => Ord a => a -> q a m -> m (q a m)
+  sort :: MonadCredit m => Ord a => q a m -> m [a] 
+
+class Sortable q => BoundedSortable q where
+  scost :: Size -> SortableOp a -> Credit
+
+data S q a m = E | S Size (q (PrettyCell a) m)
+
+instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (S q a m) where
+  prettyCell E = pure $ mkMCell "" []
+  prettyCell (S _ q) = prettyCell q
+
+instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (S q a) where
+  prettyStructure E = pure $ mkMCell "" []
+  prettyStructure (S sz q) = prettyStructure q
+
+act :: (MonadCredit m, Sortable q, Ord a) => Size -> q (PrettyCell a) m -> SortableOp a -> m (S q a m)
+act sz q (Add x) = S (sz + 1) <$> add (PrettyCell x) q
+act sz q Sort = do
+  xs <- sort q
+  pure $ S sz q
+
+instance (Arbitrary a, Ord a, BoundedSortable q, Show a) => DataStructure (S q a) (SortableOp a) where
+  create = E
+  action E op = (scost @q 0 op, empty >>= flip (act 0) op)
+  action (S sz q) op = (scost @q sz op, act sz q op)
diff --git a/src/Test/Credit/Sortable/MergeSort.hs b/src/Test/Credit/Sortable/MergeSort.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Sortable/MergeSort.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE GADTs #-}
+
+module Test.Credit.Sortable.MergeSort where
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Sortable.Base
+
+data MergeSort a m = MergeSort Size (Thunk m (MLazyCon m) [[a]])
+
+mrg :: MonadCredit m => Ord a => [a] -> [a] -> m [a]
+mrg [] ys = pure ys
+mrg xs [] = pure xs
+mrg (x:xs) (y:ys) = tick >>
+  if x <= y
+    then (x:) <$> mrg xs (y:ys)
+    else (y:) <$> mrg (x:xs) ys
+
+addSeg :: MonadCredit m => Ord a => [a] -> [[a]] -> Size -> m [[a]]
+addSeg seg segs size =
+  if size `mod` 2 == 0 then pure $ seg : segs
+  else do -- technically we should have a tick here, but Okasaki doesn't and we follow his presentation
+    let (seg1:segs') = segs
+    seg' <- mrg seg seg1 
+    addSeg seg' segs' (size `div` 2)
+
+psi :: Size -> Credit
+psi n = 2 * linear n - 2 * sum [ linear $ b i * (n `mod` 2^i + 1) | i <- [0..(log2 n + 1)] ]
+  where
+    b i = (n `div` 2^i) `mod` 2
+
+data MLazyCon m a where
+  Empty :: MLazyCon m [[a]]
+  AddSeg :: Ord a => [a] -> Thunk m (MLazyCon m) [[a]] -> Size -> MLazyCon m [[a]]
+
+instance MonadCredit m => HasStep (MLazyCon m) m where
+  step Empty = pure []
+  step (AddSeg seg segs size) = do
+    creditWith segs (psi size)
+    segs' <- force segs
+    addSeg seg segs' size
+
+mrgAll :: MonadCredit m => Ord a => [a] -> [[a]] -> m [a]
+mrgAll xs [] = pure xs
+mrgAll xs (seg:segs) = tick >> do
+  seg' <- mrg xs seg
+  mrgAll seg' segs
+
+instance Sortable MergeSort where
+  empty = do
+    segs <- delay Empty
+    pure $ MergeSort 0 segs
+  add x (MergeSort size segs) = do
+    segs' <- delay $ AddSeg [x] segs size
+    creditWith segs' (2 * log2 size + 1)
+    pure $ MergeSort (size + 1) segs'
+  sort (MergeSort size segs) = do
+    creditWith segs (psi size)
+    segs' <- force segs
+    mrgAll [] segs'
+
+instance BoundedSortable MergeSort where
+  scost n (Add _) = 2 * log2 n + 1
+  scost n Sort = psi n +  2 * linear n
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (MLazyCon m a) where
+  prettyCell Empty = pure $ mkMCell "Empty" []
+  prettyCell (AddSeg seg segs size) = do
+    -- seg' <- prettyCell seg
+    segs' <- prettyCell segs
+    size' <- prettyCell size
+    pure $ mkMCell "AddSeg" [segs', size']
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (MergeSort a m) where
+  prettyCell (MergeSort size segs) = do
+    size' <- prettyCell size
+    segs' <- prettyCell segs
+    pure $ mkMCell "MergeSort" [size', segs']
+
+instance Pretty a => MemoryStructure (MergeSort (PrettyCell a)) where
+  prettyStructure = prettyCell
diff --git a/src/Test/Credit/Sortable/Scheduled.hs b/src/Test/Credit/Sortable/Scheduled.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Credit/Sortable/Scheduled.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE GADTs #-}
+
+module Test.Credit.Sortable.Scheduled where
+
+import Prettyprinter (Pretty)
+import Control.Monad.Credit
+import Test.Credit
+import Test.Credit.Sortable.Base
+
+rev :: MonadCredit m => [a] -> [a] -> m [a]
+rev [] acc = pure acc
+rev (x : xs) acc = tick >> rev xs (x : acc)
+
+data Stream m a
+  = SCons a (Stream m a)
+  | SNil
+  | SIndirect (Thunk m (Lazy m) (Stream m a))
+
+indirect :: MonadCredit m => m (Stream m a) -> m (Stream m a)
+indirect = fmap SIndirect . delay . Lazy
+
+credit :: MonadCredit m => Credit -> Stream m a -> m ()
+credit cr (SIndirect i) = creditWith i cr
+credit _ _ = pure ()
+
+-- | Smart destructor for streams, consuming one credit
+smatch :: MonadCredit m => Stream m a -- ^ Scrutinee
+       -> m b -- ^ Nil case
+       -> (a -> Stream m a -> m b) -- ^ Cons case
+       -> m b
+smatch x nil cons = tick >> eval x
+  where
+    eval x = case x of
+      SCons a as -> cons a as
+      SNil -> nil
+      SIndirect i -> force i >>= eval
+
+streamToList :: MonadCredit m => Stream m a -> m [a]
+streamToList xs = smatch xs
+  (pure [])
+  (\x xs' -> (x:) <$> streamToList xs')
+
+type Schedule m a = [Stream m a]
+
+data SMergeSort a m = SMergeSort Size [(Stream m a, Schedule m a)]
+
+mrg :: MonadCredit m => Ord a => Stream m a -> Stream m a -> m (Stream m a)
+mrg xs ys = indirect $ do
+  smatch xs (pure ys) $ \x xs' ->
+    smatch ys (pure xs) $ \y ys' -> do
+      if x <= y
+        then (SCons x) <$> mrg xs' ys
+        else (SCons y) <$> mrg xs ys'
+
+exec1 :: MonadCredit m => Schedule m a -> m (Schedule m a)
+exec1 [] = pure []
+exec1 (ds:sched) = credit 2 ds >> smatch ds
+  (exec1 sched)
+  (\_ xs -> pure $ xs : sched)
+
+exec2 :: MonadCredit m => (Stream m a, Schedule m a) -> m (Stream m a, Schedule m a)
+exec2 (xs, sched) = exec1 sched >>= exec1 >>= pure . (xs,)
+
+execAll :: MonadCredit m => Schedule m a -> m ()
+execAll [] = pure ()
+execAll sched = exec1 sched >>= execAll
+
+addSeg :: MonadCredit m => Ord a => Stream m a -> [(Stream m a, Schedule m a)] -> Size -> Schedule m a -> m [(Stream m a, Schedule m a)]
+addSeg xs segs size rsched =
+  if size `mod` 2 == 0
+    then do
+      sched <- rev rsched [] -- log2 size
+      pure $ (xs, sched) : segs
+    else do
+      let ((xs', []) : segs') = segs
+      xs'' <- mrg xs xs'
+      addSeg xs'' segs' (size `div` 2) (xs'' : rsched)
+
+mrgAll :: MonadCredit m => Ord a => Stream m a -> [(Stream m a, Schedule m a)] -> m (Stream m a)
+mrgAll xs [] = pure xs
+mrgAll xs ((xs', sched):segs) = do
+  execAll sched -- total cost: 3 * linear size
+  seg <- mrg xs xs'
+  execAll [seg] -- total cost: 6 * linear size
+  mrgAll seg segs
+
+instance Sortable SMergeSort where
+  empty = pure $ SMergeSort 0 []
+  add x (SMergeSort size segs) = do
+    segs' <- addSeg (SCons x SNil) segs size [] -- 1 * (log2 size + 1)
+    segs'' <- mapM exec2 segs' -- 6 * (log2 size + 1)
+    pure $ SMergeSort (size + 1) segs''
+  sort (SMergeSort size segs) = do
+    s <- mrgAll SNil segs -- 9 * (log2 size + 1)
+    streamToList s -- linear size
+
+instance BoundedSortable SMergeSort where
+  scost n (Add _) = 7 * (log2 n + 1)
+  scost n Sort = 10 * (linear n + 1)
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where
+  prettyCell xs = mkMList <$> toList xs <*> toHole xs
+    where
+      toList SNil = pure $ []
+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs
+      toList (SIndirect t) = pure $ []
+
+      toHole SNil = pure $ Nothing
+      toHole (SCons x xs) = toHole xs
+      toHole (SIndirect t) = Just <$> prettyCell t
+
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SMergeSort a m) where
+  prettyCell (SMergeSort size segs) = do
+    size' <- prettyCell size
+    segs' <- prettyCell segs
+    pure $ mkMCell "SMergeSort" [size', segs']
+
+instance Pretty a => MemoryStructure (SMergeSort (PrettyCell a)) where
+  prettyStructure = prettyCell