Update readme and Demo

Contributing.md

@@ -0,0 +1,25 @@
+Contributing
+============
+
+1. `hpack` to regenerate the `.cabal` configuration (from `package.yaml`).
+2. Tests are written using [`hspec`](https://hackage.haskell.org/package/hspec), in `test/`.
+3. Formatting: [`formolu`](https://fourmolu.github.io/).
+
+Design
+------
+
+### Lenses
+
+For (deeply nested) data-structures, we manually write classy lenses to support access/updates, similar to ones generated by [microlens-th](https://hackage-content.haskell.org/package/microlens-th-0.4.3.17).
+
+Here is an example: 
+```haskell
+-- | A function context contains a list of functions
+type FunCtx primT sizeT = Ctx.Context (FunDef primT sizeT)
+
+class HasFunCtx p where
+  -- prefix the lens with an underscore.
+  _funCtx :: (primT ~ PrimitiveType p, sizeT ~ SizeType p) => Lens' p (FunCtx primT sizeT)
+
+instance HasFunCtx (FunCtx primT sizeT) where _funCtx = id
+```

Readme.md

@@ -1,4 +1,4 @@
-Traq: Estimating Quantum Cost of Classical Programs [![CI](https://github.com/qi-rub/hs-traq/actions/workflows/ci.yml/badge.svg)](https://github.com/qi-rub/hs-traq/actions/workflows/ci.yml)
+Traq: Estimating Quantum Cost of Classical Programs [![CI](../../actions/workflows/ci.yml/badge.svg)](../../actions/workflows/ci.yml)
 ================
 
 A Haskell tool to estimate data-dependent expected quantum costs of high-level classical programs.
@@ -12,8 +12,14 @@ Currently being developed against `GHC 9.6.7`. See the CI for other compatible v
 1. `cabal run` to run the main entry point.
 1. `cabal test` to run the tests.
 
-Develop
--------
+Usage
+-----
+
+Traq takes high-level classical programs in our prototype language, and produces expected cost estimates.
+See [demo.hs](examples/matrix_search/demo.hs) for the code to run the matrix search example.
+
+
+Contributing
+------------
 
-1. `hpack` to regenerate the `.cabal` configuration (from `package.yaml`).
-2. Tests are written using [`hspec`](https://hackage.haskell.org/package/hspec), in `test/`.
+Please see [Contributing.md](Contributing.md).

examples/matrix_search/demo.hs

@@ -0,0 +1,73 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main where
+
+import qualified Data.Map as Map
+import Text.Parsec.String (parseFromFile)
+import qualified Traq.Data.Context as Ctx
+import qualified Traq.Data.Symbolic as Sym
+
+import Traq.Prelude
+import qualified Traq.ProtoLang as P
+
+import Traq.Primitives.Search.DetSearch (DetSearch (..))
+import Traq.Primitives.Search.QSearchCFNW (QSearchCFNW (..))
+import Traq.Primitives.Search.RandomSearch (RandomSearch (..))
+
+type Matrix = SizeT -> SizeT -> Bool
+
+matrixToFun :: Matrix -> [P.Value SizeT] -> [P.Value SizeT]
+matrixToFun matrix [P.FinV i, P.FinV j] = [P.boolToValue $ matrix i j]
+matrixToFun _ _ = error "invalid indices"
+
+expectedCost ::
+  forall primT.
+  ( P.CanParsePrimitive primT
+  , P.QuantumCostablePrimitive primT primT SizeT Double
+  ) =>
+  Int ->
+  Int ->
+  Matrix ->
+  Double ->
+  IO Double
+expectedCost n m matrix eps = do
+  -- load the program
+  Right loaded_program <- parseFromFile (P.programParser @primT) "examples/matrix_search/matrix_search.qb"
+  let program = Sym.unSym . Sym.subst "M" (Sym.con m) . Sym.subst "N" (Sym.con n) <$> loaded_program
+
+  -- cost of each _unitary_ call to Matrix
+  let uticks = Map.singleton "Matrix" 1
+  -- cost of each _classical_ call to Matrix
+  let cticks = Map.singleton "Matrix" 1
+
+  -- the functionality of Matrix, provided as input data
+  let interp = Ctx.singleton "Matrix" (matrixToFun matrix)
+
+  return $
+    P.quantumQueryCost @primT
+      P.SplitUsingNeedsEps -- precision splitting strategy
+      eps -- maximum failure probability
+      program
+      uticks
+      cticks
+      interp
+      mempty
+
+main :: IO ()
+main = do
+  putStrLn "Demo: Matrix Search"
+
+  let (n, m) = (1000, 1000)
+  let sample_matrix i j = j /= m - 1
+  let eps = 0.01
+
+  putStrLn "Costs for sample matrix:"
+
+  putStr "  Quantum      : "
+  print =<< expectedCost @QSearchCFNW n m sample_matrix eps
+  putStr "  Deterministic: "
+  print =<< expectedCost @DetSearch n m sample_matrix eps
+  putStr "  Randomized   : "
+  print =<< expectedCost @RandomSearch n m sample_matrix eps

examples/matrix_search/matrix_search.qb

@@ -1,7 +1,7 @@
-declare Oracle(Fin<N>, Fin<M>) -> Bool end
+declare Matrix(Fin<N>, Fin<M>) -> Bool end
 
 def IsEntryZero(i0: Fin<N>, j0: Fin<M>) -> Bool do
-	e <- Oracle(i0, j0);
+	e <- Matrix(i0, j0);
 	e' <- !e;
 	return e'
 end

examples/matrix_search/matrix_search.qpl

@@ -1,19 +1,19 @@
-uproc Oracle(Fin<20>, Fin<10>, Fin<2>) :: tick(1.0)
+uproc Matrix(Fin<20>, Fin<10>, Fin<2>) :: tick(1.0)
 
 // Cost         : 2.0
 // Formula Cost : ()
-// Clean[Oracle, 6.671777e-11]
-uproc Oracle_1(in_0 : IN Fin<20>, in_1 : IN Fin<10>, out_0 : OUT Fin<2>, aux : AUX Fin<2>) {
-  call Oracle(in_0, in_1, aux);
+// Clean[Matrix, 6.671777e-11]
+uproc Matrix_1(in_0 : IN Fin<20>, in_1 : IN Fin<10>, out_0 : OUT Fin<2>, aux : AUX Fin<2>) {
+  call Matrix(in_0, in_1, aux);
   aux, out_0 *= Embed[(a) => a];
-  call-adj Oracle(in_0, in_1, aux);
+  call-adj Matrix(in_0, in_1, aux);
 }
 
 // Cost         : 2.0
 // Formula Cost : ()
 // IsEntryZero[1.3343554e-10]
 uproc IsEntryZero(i0 : IN Fin<20>, j0 : IN Fin<10>, e' : OUT Fin<2>, e : AUX Fin<2>, aux_1 : AUX Fin<2>) {
-  call Oracle_1(i0, j0, e, aux_1);
+  call Matrix_1(i0, j0, e, aux_1);
   e, e' *= Embed[(e) => not e];
 }
 
@@ -2284,3 +2284,6 @@ uproc main(result : Fin<2>, aux_988 : Fin<2>, aux_989 : Fin<2>, aux_990 : Fin<2>
   call HasAllOnesRow_1(result, aux_988, aux_989, aux_990, aux_991, aux_992, aux_993, aux_994, aux_995, aux_996, aux_997, aux_998, aux_999, aux_1000, aux_1001, aux_1002, aux_1003, aux_1004, aux_1005, aux_1006, aux_1007, aux_1008, aux_1009, aux_1010, aux_1011, aux_1012, aux_1013, aux_1014, aux_1015, aux_1016, aux_1017, aux_1018, aux_1019, aux_1020, aux_1021, aux_1022, aux_1023, aux_1024, aux_1025, aux_1026, aux_1027, aux_1028, aux_1029, aux_1030, aux_1031, aux_1032, aux_1033, aux_1034, aux_1035, aux_1036, aux_1037, aux_1038, aux_1039, aux_1040, aux_1041, aux_1042, aux_1043, aux_1044, aux_1045, aux_1046, aux_1047, aux_1048, aux_1049, aux_1050, aux_1051, aux_1052, aux_1053, aux_1054, aux_1055, aux_1056, aux_1057, aux_1058, aux_1059, aux_1060, aux_1061, aux_1062, aux_1063, aux_1064, aux_1065, aux_1066, aux_1067, aux_1068, aux_1069, aux_1070, aux_1071, aux_1072, aux_1073, aux_1074, aux_1075, aux_1076, aux_1077, aux_1078, aux_1079, aux_1080, aux_1081, aux_1082, aux_1083, aux_1084, aux_1085, aux_1086, aux_1087, aux_1088, aux_1089, aux_1090, aux_1091, aux_1092, aux_1093, aux_1094, aux_1095, aux_1096, aux_1097, aux_1098, aux_1099, aux_1100, aux_1101, aux_1102, aux_1103, aux_1104, aux_1105, aux_1106, aux_1107, aux_1108, aux_1109, aux_1110, aux_1111, aux_1112, aux_1113, aux_1114, aux_1115, aux_1116, aux_1117, aux_1118, aux_1119, aux_1120, aux_1121, aux_1122, aux_1123, aux_1124, aux_1125, aux_1126, aux_1127, aux_1128, aux_1129, aux_1130, aux_1131, aux_1132, aux_1133, aux_1134, aux_1135, aux_1136, aux_1137, aux_1138, aux_1139, aux_1140, aux_1141, aux_1142, aux_1143, aux_1144, aux_1145, aux_1146, aux_1147, aux_1148, aux_1149, aux_1150, aux_1151, aux_1152, aux_1153, aux_1154, aux_1155, aux_1156, aux_1157, aux_1158, aux_1159, aux_1160, aux_1161, aux_1162, aux_1163, aux_1164, aux_1165, aux_1166, aux_1167, aux_1168, aux_1169, aux_1170, aux_1171, aux_1172, aux_1173, aux_1174, aux_1175, aux_1176, aux_1177, aux_1178, aux_1179, aux_1180, aux_1181, aux_1182, aux_1183, aux_1184, aux_1185, aux_1186, aux_1187, aux_1188, aux_1189, aux_1190, aux_1191, aux_1192, aux_1193, aux_1194, aux_1195, aux_1196, aux_1197, aux_1198, aux_1199, aux_1200, aux_1201, aux_1202, aux_1203, aux_1204, aux_1205, aux_1206, aux_1207, aux_1208, aux_1209, aux_1210, aux_1211, aux_1212, aux_1213, aux_1214, aux_1215, aux_1216, aux_1217, aux_1218, aux_1219, aux_1220, aux_1221, aux_1222, aux_1223, aux_1224, aux_1225, aux_1226, aux_1227, aux_1228, aux_1229, aux_1230, aux_1231, aux_1232, aux_1233, aux_1234, aux_1235, aux_1236, aux_1237, aux_1238, aux_1239, aux_1240, aux_1241, aux_1242, aux_1243, aux_1244, aux_1245, aux_1246, aux_1247, aux_1248, aux_1249, aux_1250, aux_1251, aux_1252, aux_1253, aux_1254, aux_1255, aux_1256, aux_1257, aux_1258, aux_1259, aux_1260, aux_1261, aux_1262, aux_1263, aux_1264, aux_1265, aux_1266, aux_1267, aux_1268, aux_1269, aux_1270, aux_1271, aux_1272, aux_1273, aux_1274, aux_1275, aux_1276, aux_1277, aux_1278, aux_1279, aux_1280, aux_1281, aux_1282, aux_1283, aux_1284, aux_1285, aux_1286, aux_1287, aux_1288, aux_1289, aux_1290, aux_1291, aux_1292, aux_1293, aux_1294, aux_1295, aux_1296, aux_1297, aux_1298, aux_1299, aux_1300, aux_1301, aux_1302, aux_1303, aux_1304, aux_1305, aux_1306, aux_1307, aux_1308, aux_1309, aux_1310, aux_1311, aux_1312, aux_1313, aux_1314, aux_1315, aux_1316, aux_1317, aux_1318, aux_1319, aux_1320, aux_1321, aux_1322, aux_1323, aux_1324, aux_1325, aux_1326, aux_1327, aux_1328, aux_1329, aux_1330, aux_1331, aux_1332, aux_1333, aux_1334, aux_1335, aux_1336, aux_1337, aux_1338, aux_1339, aux_1340, aux_1341, aux_1342, aux_1343, aux_1344, aux_1345, aux_1346, aux_1347, aux_1348, aux_1349, aux_1350, aux_1351, aux_1352, aux_1353, aux_1354, aux_1355, aux_1356, aux_1357, aux_1358, aux_1359, aux_1360, aux_1361, aux_1362, aux_1363, aux_1364, aux_1365, aux_1366, aux_1367, aux_1368, aux_1369, aux_1370, aux_1371, aux_1372, aux_1373, aux_1374, aux_1375, aux_1376, aux_1377, aux_1378, aux_1379, aux_1380, aux_1381, aux_1382, aux_1383, aux_1384, aux_1385, aux_1386, aux_1387, aux_1388, aux_1389, aux_1390, aux_1391, aux_1392, aux_1393, aux_1394, aux_1395, aux_1396, aux_1397, aux_1398, aux_1399, aux_1400, aux_1401, aux_1402, aux_1403, aux_1404, aux_1405, aux_1406, aux_1407, aux_1408, aux_1409, aux_1410, aux_1411, aux_1412, aux_1413);
 }
 
+
+// qubits: 884
+

examples/matrix_search/matrix_search_cq.qpl

@@ -1,15 +1,15 @@
-uproc Oracle(Fin<20>, Fin<10>, Fin<2>) :: tick(1.0)
+uproc Matrix(Fin<20>, Fin<10>, Fin<2>) :: tick(1.0)
 
-// Clean[Oracle, 6.14927e-11]
-uproc Oracle_1(in_0 : IN Fin<20>, in_1 : IN Fin<10>, out_0 : OUT Fin<2>, aux : AUX Fin<2>) {
-  call Oracle(in_0, in_1, aux);
+// Clean[Matrix, 6.14927e-11]
+uproc Matrix_1(in_0 : IN Fin<20>, in_1 : IN Fin<10>, out_0 : OUT Fin<2>, aux : AUX Fin<2>) {
+  call Matrix(in_0, in_1, aux);
   aux, out_0 *= Embed[(a) => a];
-  call-adj Oracle(in_0, in_1, aux);
+  call-adj Matrix(in_0, in_1, aux);
 }
 
 // IsEntryZero[1.229854e-10]
 uproc IsEntryZero(i0 : IN Fin<20>, j0 : IN Fin<10>, e' : OUT Fin<2>, e : AUX Fin<2>, aux_1 : AUX Fin<2>) {
-  call Oracle_1(i0, j0, e, aux_1);
+  call Matrix_1(i0, j0, e, aux_1);
   e, e' *= Embed[(e) => not e];
 }
 
@@ -1509,3 +1509,5 @@ proc main(result : Fin<2>) { locals : () } {
   call HasAllOnesRow(result);
 }
 
+
+// qubits: 555

package.yaml

@@ -86,6 +86,11 @@ executables:
   #     - optparse-applicative ^>= 0.18
   #     - quipper-language == 0.9.0.0
   #     - quipper-libraries == 0.9.0.0
+  matrixsearchdemo:
+    main: demo.hs
+    <<: *exe_opts
+    source-dirs: examples/matrix_search
+
 
 tests:
   spec:

src/Traq/CQPL.hs

@@ -2,8 +2,10 @@ module Traq.CQPL (
   module Traq.CQPL.Syntax,
   module Traq.CQPL.TypeCheck,
   module Traq.CQPL.Cost,
+  module Traq.CQPL.Memory,
 ) where
 
 import Traq.CQPL.Cost
+import Traq.CQPL.Memory
 import Traq.CQPL.Syntax
 import Traq.CQPL.TypeCheck

src/Traq/CQPL/Memory.hs

@@ -0,0 +1,18 @@
+module Traq.CQPL.Memory (numQubits) where
+
+import qualified Traq.Data.Context as Ctx
+
+import Traq.CQPL.Syntax
+import Traq.Prelude
+import Traq.ProtoLang (VarType (..))
+
+numQubitsForType :: VarType SizeT -> SizeT
+numQubitsForType (Fin n) = ceiling $ logBase (2 :: Double) (fromIntegral n)
+
+numQubitsForProc :: ProcDef h SizeT c -> SizeT
+numQubitsForProc p@ProcDef{proc_param_types}
+  | isUProc p = sum $ map numQubitsForType proc_param_types
+numQubitsForProc _ = 0
+
+numQubits :: Program h SizeT c -> SizeT
+numQubits Program{proc_defs} = maximum . map numQubitsForProc $ Ctx.elems proc_defs

src/Traq/Examples/MatrixSearch.hs

@@ -25,7 +25,7 @@ matrixExample n m tyBool =
   tyJ = Fin m
 
   oracle_name :: Ident
-  oracle_name = "Oracle"
+  oracle_name = "Matrix"
 
   oracle_decl :: FunDef primsT sizeT
   oracle_decl = FunDef{param_types = [tyI, tyJ], ret_types = [tyBool], mbody = Nothing}

src/Traq/Primitives/Search/DetSearch.hs

@@ -136,7 +136,7 @@ instance
       return (is_sol, cost_v)
 
     -- average costs of a solution and a non-solution respectively
-    let (non_sols, sol_and_rest) = span fst costs & (each %~ map snd)
+    let (non_sols, sol_and_rest) = break fst costs & (each %~ map snd)
     let sol_cost = case sol_and_rest of [] -> 0; (c : _) -> c
 
     return $ sum non_sols + sol_cost

src/Traq/ProtoLang/Parser.hs

@@ -179,10 +179,14 @@ funDecl tp@TokenParser{..} = do
   let fun_def = FunDef{mbody = Nothing, ..}
   return NamedFunDef{..}
 
+funCtxP :: (CanParsePrimitive primT) => TokenParser () -> Parser (FunCtx primT SymbSize)
+funCtxP tp = do
+  fs <- many (namedFunDef tp <|> funDecl tp)
+  return $ Ctx.fromList [(fun_name f, fun_def f) | f <- fs]
+
 program :: (CanParsePrimitive primT) => TokenParser () -> Parser (Program primT SymbSize)
 program tp = do
-  fs <- many (namedFunDef tp <|> funDecl tp)
-  let funCtx = Ctx.fromList [(fun_name f, fun_def f) | f <- fs]
+  funCtx <- funCtxP tp
   stmt <- stmtP tp
   return Program{..}
 

test/Traq/Examples/MatrixSearchSpec.hs

@@ -26,8 +26,8 @@ spec = do
   describe "matrix search example" $ do
     let (n, m) = (5, 5)
     let ex = matrixExampleS n m
-    let uticks = mempty & at "Oracle" ?~ 1.0
-    let cticks = mempty & at "Oracle" ?~ 1.0
+    let uticks = mempty & at "Matrix" ?~ 1.0
+    let cticks = mempty & at "Matrix" ?~ 1.0
 
     it "type checks" $ do
       assertRight $ P.typeCheckProg Ctx.empty ex
@@ -36,7 +36,7 @@ spec = do
       P.checkVarsUnique ex `shouldBe` True
 
     let oracleF = \[P.FinV i, P.FinV j] -> [P.boolToValue $ i == j]
-    let interpCtx = Ctx.singleton "Oracle" oracleF
+    let interpCtx = Ctx.singleton "Matrix" oracleF
 
     it "evaluates" $ do
       let res = P.runProgram ex interpCtx Ctx.empty
@@ -96,8 +96,8 @@ spec = do
     let m = Sym.var "m" :: Sym.Sym Int
     let sbool = P.Fin (Sym.con 2) :: P.VarType (Sym.Sym Int)
     let ex = matrixExample @QSearchSym n m sbool
-    let uticks = mempty & at "Oracle" ?~ 1.0
-    let cticks = mempty & at "Oracle" ?~ 1.0
+    let uticks = mempty & at "Matrix" ?~ 1.0
+    let cticks = mempty & at "Matrix" ?~ 1.0
 
     -- expected, worst, unitary
     let ucF = _QryU

test/Traq/Primitives/Search/RandomSearchSpec.hs

@@ -26,7 +26,7 @@ spec = do
     it "expected cost" $ do
       let eps = 0.001
       let n = 10
-      let ticks = mempty & at "Oracle" ?~ 1.0
-      let fun_interp = Ctx.singleton "Oracle" diagMatrix
+      let ticks = mempty & at "Matrix" ?~ 1.0
+      let fun_interp = Ctx.singleton "Matrix" diagMatrix
       let c = P.quantumQueryCost default_ eps (mat_prog n n) ticks ticks fun_interp default_
       c `shouldSatisfy` (< (292 :: Double))

tools/cqplcompile.hs

@@ -2,13 +2,15 @@ module Main (main) where
 
 import qualified Data.Map as Map
 import Options.Applicative
+import Text.Printf (printf)
 import Text.Read (readMaybe)
 
 import qualified Traq.Data.Context as Ctx
 import Traq.Data.Default
 import qualified Traq.Data.Symbolic as Sym
 
-import qualified Traq.Compiler.Quantum as CQPL
+import qualified Traq.CQPL as CQPL
+import qualified Traq.Compiler.Quantum as CompileQ
 import Traq.Prelude
 import qualified Traq.ProtoLang as P
 import qualified Traq.Utils.Printing as PP
@@ -60,10 +62,12 @@ subsNM params s = Sym.unSym $ foldr subsOnce s params
 
 compile :: (RealFloat costT, Show costT) => P.Program DefaultPrims SizeT -> costT -> IO String
 compile prog eps = do
-  let oracle_ticks = Map.singleton "Oracle" 1.0
-  Right cqpl_prog <- return $ CQPL.lowerProgram default_ Ctx.empty oracle_ticks oracle_ticks eps prog
+  let oracle_name = "Matrix"
+  let oracle_ticks = Map.singleton oracle_name 1.0
+  Right cqpl_prog <- return $ CompileQ.lowerProgram default_ Ctx.empty oracle_ticks oracle_ticks eps prog
+  let nqubits = CQPL.numQubits cqpl_prog
 
-  return $ PP.toCodeString cqpl_prog
+  return $ PP.toCodeString cqpl_prog ++ printf "\n// qubits: %d\n" nqubits
 
 main :: IO ()
 main = do

tools/uqplcompile.hs

@@ -5,6 +5,7 @@ import Control.Monad.Writer (MonadWriter, execWriterT, tell)
 import Data.Maybe (fromMaybe)
 import Lens.Micro.GHC
 import Options.Applicative
+import Text.Printf (printf)
 import Text.Read (readMaybe)
 
 import qualified Traq.Data.Context as Ctx
@@ -67,7 +68,8 @@ tellLn x = tell $ unlines [x]
 
 compile :: forall costT. (RealFloat costT, Show costT) => P.Program DefaultPrims SizeT -> costT -> IO String
 compile prog delta = do
-  let oracle_ticks = mempty & at "Oracle" ?~ (fromRational 1.0 :: costT)
+  let oracle_name = "Matrix"
+  let oracle_ticks = mempty & at oracle_name ?~ (fromRational 1.0 :: costT)
   Right cqpl_prog <- return $ CompileU.lowerProgram default_ Ctx.empty oracle_ticks delta prog
   -- get costs
   let (_ :: costT, proc_costs) = CQPL.programCost cqpl_prog
@@ -77,7 +79,7 @@ compile prog delta = do
     forM_ (cqpl_prog ^. to CQPL.proc_defs . to Ctx.elems) $ \p -> do
       let pname = p ^. to CQPL.proc_name
 
-      when (pname /= "Oracle") $ do
+      when (pname /= oracle_name) $ do
         let f_cost =
               fromMaybe
                 "()"
@@ -96,15 +98,18 @@ compile prog delta = do
                               { stmt = body ^. to P.body_stmt
                               , funCtx = prog ^. to P.funCtx
                               }
-                            (mempty & at "Oracle" ?~ 1.0)
+                            (mempty & at oracle_name ?~ 1.0)
                     return $ show cf
                 )
 
         let t_cost = proc_costs ^. at pname
         tellLn $ "// Cost         : " <> maybe "()" show t_cost
         tellLn $ "// Formula Cost : " <> f_cost
+
       tellLn $ PP.toCodeString p
 
+    tellLn $ printf "\n// qubits: %d\n" $ CQPL.numQubits cqpl_prog
+
 main :: IO ()
 main = do
   Options{..} <- execParser opts