diff --git a/examples/Makefile b/examples/Makefile
index 4e7f87a..baa50cb 100644
--- a/examples/Makefile
+++ b/examples/Makefile
@@ -12,4 +12,9 @@ endef
 
 $(foreach dir,$(SUBDIRS),$(eval $(call SUBDIR_RULE,$(dir))))
 
-.PHONY: all $(SUBDIRS)
+# Generate the augmented Table 2 statistics (QPL size, error/cost bounds) for all
+# case studies: prints a Markdown table and writes case_study_stats.csv.
+stats:
+	cd .. && cabal run -v0 casestudystats
+
+.PHONY: all stats $(SUBDIRS)
diff --git a/examples/case_study_stats.csv b/examples/case_study_stats.csv
new file mode 100644
index 0000000..e1f5ca1
--- /dev/null
+++ b/examples/case_study_stats.csv
@@ -0,0 +1,10 @@
+program,domain,traq_loc,primitives,qpl_loc,qubits,eps_budget,error_concrete,cost_concrete,error_symbolic,cost_symbolic
+Triangle Finding,Search,43,search,198,2574,1.0e-3,1.00e-3,1488549.72,eps_1+188.0*(1.0+logBase 3.0 (1.0/eps_1))*sqrt (2.0*eps_0),188.0*(1.0+logBase 3.0 (1.0/eps_1))*(1.0+16.0*(1.0+logBase 0.6086 eps_0))
+Farthest Points,Search,40,search,149,5608,1.0e-3,1.00e-3,19299.83,4.0*eps_0,4.0*(3.0+564.0*(1.0+logBase 3.0 (1.0/eps_0)))
+Matrix Search,Search,18,"search, all",159,2224,1.0e-3,1.00e-3,324117.64,eps_1+86.28730157199226*(1.0+logBase 3.0 (1.0/eps_1))*sqrt (2.0*eps_0),690.2984125759381*(1.0+logBase 3.0 (1.0/eps_1))*(1.0+logBase 0.6086 eps_0)
+Depth-3 NAND,Search,28,all,232,11668,1.0e-3,1.00e-3,389304852.19,eps_2+86.28730157199226*(1.0+logBase 3.0 (1.0/eps_2))*sqrt (2.0*(eps_1+8.0*(1.0+logBase 0.6086 eps_1)*sqrt (2.0*eps_0))),5522.387300607505*(1.0+logBase 3.0 (1.0/eps_2))*(1.0+logBase 0.6086 eps_1)*(1.0+logBase 0.6086 eps_0)
+Max-k-SAT (simple),Optimization,34,search,125,1702,1.0e-3,1.00e-3,4290.74,eps_0+eps_0+eps_0,172.57460314398452*(1.0+logBase 3.0 (1.0/eps_0))+172.57460314398452*(1.0+logBase 3.0 (1.0/eps_0))+172.57460314398452*(1.0+logBase 3.0 (1.0/eps_0))
+Max-k-SAT (steep),Optimization,32,argmax,112,5682,1.0e-3,1.00e-3,8998.69,eps_0+eps_0+eps_0,374.64719258669794*log (1.0/eps_0)+374.64719258669794*log (1.0/eps_0)+374.64719258669794*log (1.0/eps_0)
+0/1 Knapsack,Optimization,80,amplify,1068,4319,1.0e-3,1.00e-3,90525.36,3.0*eps_0,3.0*(4.0+165.6*logBase 3.0 (1.0/eps_0)/sqrt (p**4.0))
+3-Round Feistel,Cryptanalysis,67,simon,120,39302,1.0e-3,1.00e-3,259.33,eps_0,8.0*(1.0+(21.0+logBase 2.0 (1.0/eps_0))/0.98564470702293)
+Even-Mansour,Cryptanalysis,25,simon,76,10280,1.0e-3,1.00e-3,127.61,eps_0,2.0+4.0*(1.0+(20.0+logBase 2.0 (1.0/eps_0))/0.98564470702293)
diff --git a/examples/matrix_search/demo_symbolic.hs b/examples/matrix_search/demo_symbolic.hs
new file mode 100644
index 0000000..793ef05
--- /dev/null
+++ b/examples/matrix_search/demo_symbolic.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE TypeApplications #-}
+
+module Main where
+
+import Text.Parsec.String (parseFromFile)
+
+import Lens.Micro.GHC
+
+import qualified Traq.Analysis as A
+import Traq.Analysis.CostModel.QueryCost
+import qualified Traq.CPL as CPL
+import qualified Traq.Data.Symbolic as Sym
+import Traq.Prelude
+import Traq.Primitives (DefaultPrims)
+
+matrixToFun :: (SizeT -> SizeT -> Bool) -> [CPL.Value SizeT] -> [CPL.Value SizeT]
+matrixToFun matrix [CPL.FinV i, CPL.FinV j] = [CPL.toValue $ matrix i j]
+matrixToFun _ _ = error "invalid indices"
+
+{- | Load matrix_search.traq, substitute concrete sizes N=n and M=m, then
+attach a fresh symbolic eps_i to each primitive call. Print the resulting
+symbolic error-budget constraint and the three cost analyses as raw Sym
+Double ASTs, so the output can be fed to an external optimizer.
+-}
+dumpSymbolic :: SizeT -> SizeT -> (SizeT -> SizeT -> Bool) -> IO ()
+dumpSymbolic n m sample_matrix = do
+  Right loaded_program <-
+    parseFromFile
+      (CPL.programParser @(DefaultPrims (Sym.Sym Int) (Sym.Sym Double)))
+      "examples/matrix_search/matrix_search.traq"
+
+  let prog =
+        CPL.mapSize
+          (Sym.unSym . Sym.subst "M" (Sym.con m) . Sym.subst "N" (Sym.con n))
+          loaded_program
+
+  prog_ann <- either fail pure $ A.annSymEpsProg prog
+
+  let interp = mempty & at "Matrix" ?~ matrixToFun sample_matrix
+
+  let tvErr = Sym.simpl $ A.getFailProb $ A.tvErrorQProg prog_ann
+  let costU_ = fmap Sym.simpl (A.costUProg prog_ann :: QueryCost (Sym.Sym Double))
+  let costQ_ = fmap Sym.simpl (A.costQProg prog_ann :: QueryCost (Sym.Sym Double))
+  let expCostQ_ = fmap Sym.simpl (A.expCostQProg prog_ann mempty interp :: QueryCost (Sym.Sym Double))
+
+  putStrLn "# Symbolic epsilon extraction for matrix_search"
+  putStrLn $ "#   parameters: N=" ++ show n ++ ", M=" ++ show m
+  putStrLn ""
+  putStrLn "## Error-budget constraint (tvErrorQ)"
+  putStrLn "# Solver constraint: the following expression <= user-chosen budget."
+  print tvErr
+  putStrLn ""
+  putStrLn "## costU (worst-case unitary cost, per external fn)"
+  print costU_
+  putStrLn ""
+  putStrLn "## costQ (worst-case quantum cost, per external fn)"
+  print costQ_
+  putStrLn ""
+  putStrLn "## expCostQ (expected quantum cost, per external fn, data-dependent)"
+  putStrLn "# Uses sample_matrix: (\\i j -> i <= j)"
+  print expCostQ_
+
+main :: IO ()
+main = dumpSymbolic 20 10 (\i j -> i <= j)
diff --git a/experiments/casestudy_stats.hs b/experiments/casestudy_stats.hs
new file mode 100644
index 0000000..c8c48c4
--- /dev/null
+++ b/experiments/casestudy_stats.hs
@@ -0,0 +1,371 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+{- | Generate the augmented case-study statistics table (Section 8.2 / Table 2).
+
+For every case study we report, at its paper/Makefile default parameters:
+
+  * LoC of the source @.traq@ program,
+  * size of the compiled QPL program (LoC of the @.qpl@ and qubit count),
+  * the proven error bound (worst-case total-variation failure probability), and
+  * the proven cost bound (worst-case quantum query cost).
+
+The error/cost bounds are produced in two forms:
+
+  * concrete   - a single number, after distributing the @eps@ budget across the
+                 primitive calls ('A.annotateProgWithErrorBudget'), exactly like
+                 the QPL backend of the @traq@ CLI;
+  * symbolic   - an expression in the per-call error budgets @eps_i@ (sizes are
+                 concrete; budget is left undistributed via 'A.annSymEpsProg'),
+                 exactly like the @-t Symbolic@ backend of the @traq@ CLI.
+
+This mirrors @tools/traq.hs@ (loadTraqProgram / emitQPL / emitSymbolic) and
+@experiments/compile_loc.hs@; we just fix the primitive type to
+'P.WorstCasePrims' (the type the CLI parses every example with) and tabulate.
+-}
+module Main (main) where
+
+import Control.Exception (SomeException, evaluate, try)
+import Control.Monad (forM)
+import Data.List (intercalate)
+import System.IO (IOMode (WriteMode), hPutStrLn, stderr, withFile)
+import Text.Parsec.String (parseFromFile)
+import Text.Printf (printf)
+
+import qualified Traq.Data.Symbolic as Sym
+
+import qualified Traq.Analysis as A
+import Traq.Analysis.CostModel.QueryCost (SimpleQueryCost (..))
+import qualified Traq.CPL as CPL
+import qualified Traq.Compiler as Compiler
+import Traq.Prelude
+import qualified Traq.Primitives as P
+import qualified Traq.QPL as QPL
+import qualified Traq.Utils.Printing as PP
+
+-- ============================================================
+-- Case-study configuration
+-- ============================================================
+
+data CaseStudy = CaseStudy
+  { csLabel :: String
+  , csDomain :: String
+  , csFile :: FilePath
+  , csPrims :: String
+  , csSizes :: [(Ident, SizeT)]
+  , csFloats :: [(Ident, Double)]
+  , csEps :: Double
+  }
+
+-- | The 9 case-study programs (Max-k-SAT contributes two), with the same
+-- parameters their Makefiles use to build the committed @.qpl@ files.
+caseStudies :: [CaseStudy]
+caseStudies =
+  [ CaseStudy
+      { csLabel = "Triangle Finding"
+      , csDomain = "Search"
+      , csFile = "examples/search/triangle_finding.traq"
+      , csPrims = "search"
+      , csSizes = [("N", 10)]
+      , csFloats = []
+      , csEps = 1e-3
+      }
+  , CaseStudy
+      { csLabel = "Farthest Points"
+      , csDomain = "Search"
+      , csFile = "examples/search/clustering.traq"
+      , csPrims = "search"
+      , csSizes = [("N", 10), ("M", 100)]
+      , csFloats = []
+      , csEps = 1e-3
+      }
+  , CaseStudy
+      { csLabel = "Matrix Search"
+      , csDomain = "Search"
+      , csFile = "examples/matrix_search/matrix_search.traq"
+      , csPrims = "search, all"
+      , csSizes = [("N", 20), ("M", 10)]
+      , csFloats = []
+      , csEps = 1e-3
+      }
+  , CaseStudy
+      { csLabel = "Depth-3 NAND"
+      , csDomain = "Search"
+      , csFile = "examples/matrix_search/depth3_NAND_formula.traq"
+      , csPrims = "all"
+      , csSizes = [("N", 20), ("M", 10), ("K", 10)]
+      , csFloats = []
+      , csEps = 1e-3
+      }
+  , CaseStudy
+      { csLabel = "Max-k-SAT (simple)"
+      , csDomain = "Optimization"
+      , csFile = "examples/hillclimb/max_sat_hillclimb.traq"
+      , csPrims = "search"
+      , csSizes = [("n", 20), ("W", 1000)]
+      , csFloats = []
+      , csEps = 1e-3
+      }
+  , CaseStudy
+      { csLabel = "Max-k-SAT (steep)"
+      , csDomain = "Optimization"
+      , csFile = "examples/hillclimb/steep_max_sat.traq"
+      , csPrims = "argmax"
+      , csSizes = [("n", 20), ("W", 1000)]
+      , csFloats = []
+      , csEps = 1e-3
+      }
+  , CaseStudy
+      { csLabel = "0/1 Knapsack"
+      , csDomain = "Optimization"
+      , csFile = "examples/tree_generator/tree_generator_01_knapsack.traq"
+      , csPrims = "amplify"
+      , csSizes = [("W", 1000), ("P", 1000), ("N", 4), ("K", 3)]
+      , csFloats = [("p", 0.2)]
+      , csEps = 1e-3
+      }
+  , CaseStudy
+      { csLabel = "3-Round Feistel"
+      , csDomain = "Cryptanalysis"
+      , csFile = "examples/cryptanalysis/3_round_feistel.traq"
+      , csPrims = "simon"
+      , csSizes = [("n", 20), ("n_plus_1", 21)]
+      , csFloats = []
+      , csEps = 1e-3
+      }
+  , CaseStudy
+      { csLabel = "Even-Mansour"
+      , csDomain = "Cryptanalysis"
+      , csFile = "examples/cryptanalysis/even_mansour.traq"
+      , csPrims = "simon"
+      , csSizes = [("n", 20), ("n_plus_1", 21)]
+      , csFloats = []
+      , csEps = 1e-3
+      }
+  ]
+
+-- ============================================================
+-- Parameter substitution (mirrors tools/traq.hs)
+-- ============================================================
+
+subsOnce :: (Num a, Eq a) => (Ident, a) -> Sym.Sym a -> Sym.Sym a
+subsOnce (k, v) = Sym.subst k (Sym.con v)
+
+-- | Substitute concrete sizes, collapsing the symbolic size to a concrete 'SizeT'.
+subsSizes :: [(Ident, SizeT)] -> Sym.Sym SizeT -> SizeT
+subsSizes ps s = Sym.unSym $ foldr subsOnce s ps
+
+-- | Substitute concrete float parameters into the (symbolic) precision.
+subsFloats :: [(Ident, Double)] -> Sym.Sym Double -> Double
+subsFloats ps s = Sym.unSym $ foldr subsOnce s ps
+
+-- | Substitute size parameters that appear inside *precision* expressions,
+-- keeping the result symbolic (so float params / @eps_i@ stay free). Needed
+-- because some programs reference a size in a precision position — e.g. the
+-- knapsack's @amplify<p ** N>@ — which the plain size substitution misses.
+subsSizesInPrec :: [(Ident, SizeT)] -> Sym.Sym Double -> Sym.Sym Double
+subsSizesInPrec ps s = foldr (\(k, v) -> Sym.subst k (Sym.con (fromIntegral v))) s ps
+
+-- | Size parameters as float substitutions, for the concrete precision pass.
+sizesAsFloats :: [(Ident, SizeT)] -> [(Ident, Double)]
+sizesAsFloats = map (fmap fromIntegral)
+
+type ParsedPrim = P.WorstCasePrims (Sym.Sym SizeT) (Sym.Sym Double)
+type SymPrim = P.WorstCasePrims SizeT (Sym.Sym Double)
+type ConcPrim = P.WorstCasePrims SizeT Double
+
+loadProgram :: FilePath -> IO (CPL.Program ParsedPrim)
+loadProgram fname = do
+  res <- parseFromFile (CPL.programParser @ParsedPrim) fname
+  either (fail . show) pure res
+
+-- ============================================================
+-- Concrete and symbolic analysis passes
+-- ============================================================
+
+-- | Concrete metrics at the given sizes/floats with the budget @eps@ distributed
+-- over the primitive calls: (QPL LoC, qubits, error bound, cost bound).
+concretePass :: CaseStudy -> IO (Either String (Int, Int, Double, Double))
+concretePass CaseStudy{..} = handleAny $ do
+  parsed <- loadProgram csFile
+  let progSym = CPL.mapSize (subsSizes csSizes) parsed :: CPL.Program SymPrim
+      progConc = CPL.mapPrec (subsFloats (csFloats ++ sizesAsFloats csSizes)) progSym :: CPL.Program ConcPrim
+  progAnn <- either fail pure $ A.annotateProgWithErrorBudget (A.failProb csEps) progConc
+  qpl <- either fail pure $ Compiler.lowerProgram progAnn
+  let loc = length . lines $ PP.toCodeString qpl
+      qubits = QPL.numQubits qpl
+      cost = getCost (A.costQProg progAnn :: SimpleQueryCost Double)
+      err = A.getFailProb (A.tvErrorQProg progAnn) :: Double
+  loc' <- evaluate loc
+  qubits' <- evaluate qubits
+  err' <- evaluate err
+  cost' <- evaluate cost
+  pure (loc', qubits', err', cost')
+
+-- | Symbolic metrics at the given sizes, with per-call budgets @eps_i@ left free:
+-- (error bound expression, cost bound expression).
+symbolicPass :: CaseStudy -> IO (Either String (String, String))
+symbolicPass CaseStudy{..} = handleAny $ do
+  parsed <- loadProgram csFile
+  let progSym =
+        CPL.mapPrec (subsSizesInPrec csSizes) $
+          CPL.mapSize (subsSizes csSizes) parsed ::
+          CPL.Program SymPrim
+  progAnn <- either fail pure $ A.annSymEpsProg progSym
+  let err = Sym.simpl $ A.getFailProb (A.tvErrorQProg progAnn)
+      cost = Sym.simpl $ getCost (A.costQProg progAnn :: SimpleQueryCost (Sym.Sym Double))
+      errS = show err
+      costS = show cost
+  errS' <- evaluate (length errS `seq` errS)
+  costS' <- evaluate (length costS `seq` costS)
+  pure (errS', costS')
+
+handleAny :: forall a. IO a -> IO (Either String a)
+handleAny act = do
+  res <- try act :: IO (Either SomeException a)
+  pure $ either (Left . show) Right res
+
+-- ============================================================
+-- A fully-computed row
+-- ============================================================
+
+data Row = Row
+  { rStudy :: CaseStudy
+  , rTraqLoC :: Int
+  , rConc :: Either String (Int, Int, Double, Double)
+  , rSym :: Either String (String, String)
+  }
+
+computeRow :: CaseStudy -> IO Row
+computeRow cs = do
+  traqLoC <- length . lines <$> readFile (csFile cs)
+  conc <- concretePass cs
+  sym <- symbolicPass cs
+  case conc of
+    Left e -> hPutStrLn stderr $ "[" ++ csLabel cs ++ "] concrete pass failed: " ++ e
+    Right _ -> pure ()
+  case sym of
+    Left e -> hPutStrLn stderr $ "[" ++ csLabel cs ++ "] symbolic pass failed: " ++ e
+    Right _ -> pure ()
+  pure $ Row cs traqLoC conc sym
+
+-- ============================================================
+-- Formatting
+-- ============================================================
+
+-- | Render a cost number compactly: integral values without a fraction.
+num :: Double -> String
+num x
+  | x == fromInteger (round x) = show (round x :: Integer)
+  | otherwise = printf "%.2f" x
+
+-- | Render a (small) failure probability with scientific precision.
+numProb :: Double -> String
+numProb x
+  | x == 0 = "0"
+  | otherwise = printf "%.2e" x
+
+mdTable :: [Row] -> String
+mdTable rows = unlines (header : sep : map rowLine rows)
+ where
+  header =
+    cells
+      ["Program", "Domain", "LoC", "Primitives", "|QPL| (LoC)", "qubits", "error bound (≤)", "cost bound"]
+  sep = cells (replicate 8 "---")
+  rowLine Row{..} =
+    let CaseStudy{..} = rStudy
+        (qloc, qub, err, cost) = case rConc of
+          Right (a, b, c, d) -> (show a, show b, numProb c, num d)
+          Left _ -> ("ERR", "ERR", "ERR", "ERR")
+     in cells [csLabel, csDomain, show rTraqLoC, csPrims, qloc, qub, err, cost]
+  cells xs = "| " ++ intercalate " | " xs ++ " |"
+
+symbolicAppendix :: [Row] -> String
+symbolicAppendix rows = unlines $ concatMap block rows
+ where
+  block Row{..} =
+    let CaseStudy{..} = rStudy
+        (errS, costS) = case rSym of
+          Right (e, c) -> (e, c)
+          Left e -> ("(unavailable: " ++ e ++ ")", "(unavailable)")
+     in [ "### " ++ csLabel
+        , "error bound (symbolic):  " ++ errS
+        , "cost bound  (symbolic):  " ++ costS
+        , ""
+        ]
+
+csvQuote :: String -> String
+csvQuote s
+  | any (`elem` ",\"\n") s = '"' : concatMap esc s ++ "\""
+  | otherwise = s
+ where
+  esc '"' = "\"\""
+  esc c = [c]
+
+writeCsv :: FilePath -> [Row] -> IO ()
+writeCsv path rows = withFile path WriteMode $ \h -> do
+  hPutStrLn h $
+    intercalate
+      ","
+      [ "program"
+      , "domain"
+      , "traq_loc"
+      , "primitives"
+      , "qpl_loc"
+      , "qubits"
+      , "eps_budget"
+      , "error_concrete"
+      , "cost_concrete"
+      , "error_symbolic"
+      , "cost_symbolic"
+      ]
+  mapM_ (hPutStrLn h . csvRow) rows
+ where
+  csvRow Row{..} =
+    let CaseStudy{..} = rStudy
+        (qloc, qub, err, cost) = case rConc of
+          Right (a, b, c, d) -> (show a, show b, numProb c, num d)
+          Left e -> let m = "ERR:" ++ e in (m, m, m, m)
+        (errS, costS) = case rSym of
+          Right (e, c) -> (e, c)
+          Left e -> ("ERR:" ++ e, "ERR:" ++ e)
+     in intercalate "," $
+          map
+            csvQuote
+            [ csLabel
+            , csDomain
+            , show rTraqLoC
+            , csPrims
+            , qloc
+            , qub
+            , printf "%g" csEps
+            , err
+            , cost
+            , errS
+            , costS
+            ]
+
+-- ============================================================
+-- Main
+-- ============================================================
+
+main :: IO ()
+main = do
+  rows <- forM caseStudies computeRow
+
+  putStrLn "## Case-study statistics (Table 2, augmented)\n"
+  putStrLn "Concrete bounds are at each program's default parameters (Makefile sizes,"
+  putStrLn "failure-probability budget ε = 10⁻³). `error bound` is the proven worst-case"
+  putStrLn "total-variation failure probability (≤ ε); `cost bound` is the proven worst-case"
+  putStrLn "quantum query cost (costQ).\n"
+  putStr $ mdTable rows
+
+  putStrLn "\n## Symbolic bounds\n"
+  putStrLn "Expressions at the same sizes, with the per-primitive error budgets `eps_i`"
+  putStrLn "left undistributed (and any float parameters symbolic). These are exactly what"
+  putStrLn "`traq -t Symbolic` emits.\n"
+  putStr $ symbolicAppendix rows
+
+  writeCsv "examples/case_study_stats.csv" rows
+  putStrLn "Wrote examples/case_study_stats.csv"
diff --git a/package.yaml b/package.yaml
index 79e6d03..9f7a777 100644
--- a/package.yaml
+++ b/package.yaml
@@ -99,6 +99,10 @@ executables:
     main: demo.hs
     <<: *expt_opts
     source-dirs: examples/matrix_search
+  matrixsearchdemosymbolic:
+    main: demo_symbolic.hs
+    <<: *expt_opts
+    source-dirs: examples/matrix_search
   knapsackdemo:
     main: demo.hs
     <<: *expt_opts
@@ -109,6 +113,9 @@ executables:
   compile_loc:
     main: compile_loc.hs
     <<: *expt_opts
+  casestudystats:
+    main: casestudy_stats.hs
+    <<: *expt_opts
 
 
 tests:
diff --git a/tools/traq.hs b/tools/traq.hs
index 64c4d73..7e85a6a 100644
--- a/tools/traq.hs
+++ b/tools/traq.hs
@@ -18,6 +18,7 @@ import Traq.Control.Monad
 import qualified Traq.Data.Symbolic as Sym
 
 import qualified Traq.Analysis as Analysis
+import Traq.Analysis.CostModel.QueryCost (QueryCost)
 import qualified Traq.CPL as CPL
 import qualified Traq.Compiler as Compiler
 import qualified Traq.Experimental.Compiler.Qiskit as Qiskit
@@ -31,7 +32,7 @@ import qualified Traq.Utils.Printing as PP
 -- CLI
 -- ============================================================
 
-data Backend = QPL | Qualtran | Qiskit
+data Backend = QPL | Qualtran | Qiskit | Symbolic
   deriving (Read, Show, Eq)
 
 data Options = Options
@@ -52,25 +53,29 @@ data Options = Options
 -- | Load a Traq program source, and substitute parameters.
 loadTraqProgram :: ReaderT Options IO (CPL.Program (P.WorstCasePrims SizeT Double))
 loadTraqProgram = do
+  prog <- loadTraqProgramSym
+  pf <- view (to paramsf)
+  pure $ CPL.mapPrec (subs_paramsf pf) prog
+
+-- | Load a Traq program source, substituting only size parameters. Precision
+-- stays as 'Sym.Sym Double' so epsilons remain symbolic for the Symbolic backend.
+loadTraqProgramSym :: ReaderT Options IO (CPL.Program (P.WorstCasePrims SizeT (Sym.Sym Double)))
+loadTraqProgramSym = do
   code <- lift . readFile =<< view (to in_file)
   case CPL.parseProgram @(P.WorstCasePrims _ (Sym.Sym Double)) code of
     Left err -> fail $ show err
     Right prog -> do
       ps <- view (to params)
-      pf <- view (to paramsf)
-      pure $ CPL.mapPrec (subs_paramsf ps pf) $ CPL.mapSize (subs_params ps) prog
- where
-  subsOnce :: (Num a, Eq a) => (Ident, a) -> Sym.Sym a -> Sym.Sym a
-  subsOnce (k, v) = Sym.subst k (Sym.con v)
+      pure $ CPL.mapSize (subs_params ps) prog
+
+subsOnce :: (Num a, Eq a) => (Ident, a) -> Sym.Sym a -> Sym.Sym a
+subsOnce (k, v) = Sym.subst k (Sym.con v)
 
-  subs_params :: [(Ident, SizeT)] -> (Sym.Sym Int -> SizeT)
-  subs_params params s = Sym.unSym $ foldr subsOnce s params
+subs_params :: [(Ident, SizeT)] -> (Sym.Sym Int -> SizeT)
+subs_params params s = Sym.unSym $ foldr subsOnce s params
 
-  subs_paramsf :: [(Ident, SizeT)] -> [(Ident, Double)] -> (Sym.Sym Double -> Double)
-  subs_paramsf ps pf s = Sym.unSym $ foldr subsOnce (foldr subsI s ps) pf
-   where
-    subsI :: (Ident, SizeT) -> Sym.Sym Double -> Sym.Sym Double
-    subsI (k, v) = subsOnce (k, fromIntegral v)
+subs_paramsf :: [(Ident, Double)] -> (Sym.Sym Double -> Double)
+subs_paramsf pf s = Sym.unSym $ foldr subsOnce s pf
 
 -- | Compile source CPL to target QPL.
 compileCPL :: (RealFloat prec, Show prec) => CPL.Program (P.WorstCasePrims SizeT prec) -> prec -> IO (QPL.Program SizeT)
@@ -108,6 +113,34 @@ emitQualtran = emitWithTemplate "tools/qualtran_prelude.py" . Qualtran.toPy
 emitQiskit :: QPL.Program SizeT -> IO String
 emitQiskit = emitWithTemplate "tools/qiskit_prelude.py" . Qiskit.toPy
 
+{- | Attach a fresh symbolic eps_i to each primitive in the (size-substituted,
+symbolic-precision) program, then dump:
+    * the total-error constraint from 'tvErrorQProg' (used as ... <= budget),
+    * 'costU', 'costQ' as QueryCost expressions in the eps_i.
+'expCostQ' is omitted because it requires external-function interpretations
+that are program-specific and not available from a generic CLI flag.
+-}
+emitSymbolic :: CPL.Program (P.WorstCasePrims SizeT (Sym.Sym Double)) -> IO String
+emitSymbolic prog = do
+  prog_ann <- either fail pure $ Analysis.annSymEpsProg prog
+  let tvErr = Sym.simpl $ Analysis.getFailProb $ Analysis.tvErrorQProg prog_ann
+  let costU_ = fmap Sym.simpl (Analysis.costUProg prog_ann :: QueryCost (Sym.Sym Double))
+  let costQ_ = fmap Sym.simpl (Analysis.costQProg prog_ann :: QueryCost (Sym.Sym Double))
+  pure $
+    unlines
+      [ "# Symbolic epsilon extraction"
+      , ""
+      , "## Error-budget constraint (tvErrorQ)"
+      , "# Solver constraint: the following expression <= user-chosen budget."
+      , show tvErr
+      , ""
+      , "## costU (worst-case unitary cost, per external fn)"
+      , show costU_
+      , ""
+      , "## costQ (worst-case quantum cost, per external fn)"
+      , show costQ_
+      ]
+
 -- ============================================================
 -- CLI parser
 -- ============================================================
@@ -189,18 +222,24 @@ main = do
           fail $
             "feature " <> feat <> " is experimental; pass --experimental to run it anyway"
 
-  qpl_prog <- (runReaderT ?? options) $ do
-    case takeExtension in_file of
-      ".traq" -> do
-        p <- loadTraqProgram
-        case eps of
-          Just e -> lift $ compileCPL p e
-          Nothing -> fail "--failprob is required when compiling .traq files"
-      ".qpl" -> loadQPLProgram
-      ext -> fail $ "Unsupported file extension: " ++ ext
-
   out_str <- case target of
-    QPL -> emitQPL qpl_prog
-    Qualtran -> guardExperimental "backend:Qualtran" >> emitQualtran qpl_prog
-    Qiskit -> guardExperimental "backend:Qiskit" >> emitQiskit qpl_prog
+    Symbolic -> do
+      unless (takeExtension in_file == ".traq") $
+        fail "Symbolic backend requires a .traq input"
+      p <- runReaderT loadTraqProgramSym options
+      emitSymbolic p
+    _ -> do
+      qpl_prog <- (runReaderT ?? options) $ do
+        case takeExtension in_file of
+          ".traq" -> do
+            p <- loadTraqProgram
+            case eps of
+              Just e -> lift $ compileCPL p e
+              Nothing -> fail "--failprob is required when compiling .traq files"
+          ".qpl" -> loadQPLProgram
+          ext -> fail $ "Unsupported file extension: " ++ ext
+      case target of
+        QPL -> emitQPL qpl_prog
+        Qualtran -> guardExperimental "backend:Qualtran" >> emitQualtran qpl_prog
+        Qiskit -> guardExperimental "backend:Qiskit" >> emitQiskit qpl_prog
   maybe putStr writeFile out_file out_str
diff --git a/traq.cabal b/traq.cabal
index 1405a63..4a184b5 100644
--- a/traq.cabal
+++ b/traq.cabal
@@ -163,6 +163,43 @@ executable compile_loc
     , traq
   default-language: Haskell2010
 
+executable casestudystats
+  main-is: casestudy_stats.hs
+  hs-source-dirs:
+      experiments
+  default-extensions:
+      LambdaCase
+      NamedFieldPuns
+      ScopedTypeVariables
+      ApplicativeDo
+      RankNTypes
+      FlexibleContexts
+      TypeFamilies
+      TypeOperators
+      MultiWayIf
+      EmptyCase
+      ConstraintKinds
+      RecordWildCards
+  ghc-options: -Wall -fprint-typechecker-elaboration
+  build-depends:
+      algebra ==4.3.*
+    , base >=4.10 && <5
+    , containers >=0.6 && <1
+    , deepseq
+    , extra >=1.8 && <2
+    , microlens-ghc ==0.4.*
+    , microlens-mtl ==0.2.*
+    , mtl >=2.2.2
+    , optparse-applicative ==0.18.*
+    , parsec >=3.1.17 && <3.2
+    , prettyprinter ==1.7.*
+    , random
+    , random-shuffle
+    , timeit ==2.0.*
+    , transformers >=0.5
+    , traq
+  default-language: Haskell2010
+
 executable knapsackdemo
   main-is: demo.hs
   hs-source-dirs:
@@ -274,6 +311,43 @@ executable matrixsearchdemo
     , traq
   default-language: Haskell2010
 
+executable matrixsearchdemosymbolic
+  main-is: demo_symbolic.hs
+  hs-source-dirs:
+      examples/matrix_search
+  default-extensions:
+      LambdaCase
+      NamedFieldPuns
+      ScopedTypeVariables
+      ApplicativeDo
+      RankNTypes
+      FlexibleContexts
+      TypeFamilies
+      TypeOperators
+      MultiWayIf
+      EmptyCase
+      ConstraintKinds
+      RecordWildCards
+  ghc-options: -Wall -fprint-typechecker-elaboration
+  build-depends:
+      algebra ==4.3.*
+    , base >=4.10 && <5
+    , containers >=0.6 && <1
+    , deepseq
+    , extra >=1.8 && <2
+    , microlens-ghc ==0.4.*
+    , microlens-mtl ==0.2.*
+    , mtl >=2.2.2
+    , optparse-applicative ==0.18.*
+    , parsec >=3.1.17 && <3.2
+    , prettyprinter ==1.7.*
+    , random
+    , random-shuffle
+    , timeit ==2.0.*
+    , transformers >=0.5
+    , traq
+  default-language: Haskell2010
+
 executable matrixsearchqcost
   main-is: matrixsearchqcost.hs
   hs-source-dirs: