scripts to get numbers for RQ2

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)

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)

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)