Skip to content
6 changes: 4 additions & 2 deletions examples/clustering_algorithm.qb
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@ declare D_n(Fin<N>) -> Arr<N, Fin<M>> end

declare Dist(Arr<N, Fin<M>>, Arr<N, Fin<M>>) -> Fin<M> end

def check(dmax : Fin<M>, i: Fin<N>, j: Fin<N>) -> Bool do
def check(dmax : Fin<M>, ij: Tup<Fin<N>, Fin<N>>) -> Bool do
i <- ij.0;
j <- ij.1;
xi <- D_n(i);
xj <- D_n(j);
dist' <- Dist(xi, xj);
Expand All @@ -22,7 +24,7 @@ def loop_body(i: Fin<N>, j: Fin<N>) -> (Fin<N>, Fin<N>) do
xj <- D_n(j);
dmax <- Dist(xi, xj);

i', j' <- @search<Fin<N>, Fin<N>>[check(dmax, _, _)];
i', j' <- @search<Tup<Fin<N>, Fin<N>>>[check(dmax, _)];
return i', j'
end

Expand Down
18 changes: 9 additions & 9 deletions examples/cryptanalysis/grover_meets_simon.qb
Original file line number Diff line number Diff line change
Expand Up @@ -2,31 +2,31 @@

// N = 2^n
// Block-cipher E(k, x)
declare E(Fin<N>, Fin<N>) -> Fin<N> end
declare E(BitVec<n>, BitVec<n>) -> BitVec<n> end

// FX-construction with secret keys (k0, k1, k2):
// Enc(x) = E_k0(x ^ k1) ^ k2
declare Enc(Fin<N>) -> Fin<N> end
declare Enc(BitVec<n>) -> BitVec<n> end

// FX-construction almost 2-1 function, when k = k0 (hidden)
def f(k: Fin<N>, x : Fin<N>) -> Fin<N> do
def f(k: BitVec<n>, x : BitVec<n>) -> BitVec<n> do
ex <- Enc(x);
p_kx <- E(k, x);
f_kx <- ex ^ p_kx;
return f_kx
end

// classifier(k: Fin<N>, k1: Fin<N>)
declare classifier(Fin<N>, Fin<N>) -> Bool end
// classifier(k: BitVec<n>, k1: BitVec<n>)
declare classifier(BitVec<n>, BitVec<n>) -> Bool end

// takes k and outputs some Fin<N>
def innerAttack(k: Fin<N>) -> Bool do
k1 <- @findXorPeriod[f, 0.01](k);
// takes k and outputs some BitVec<n>
def innerAttack(k: BitVec<n>) -> Bool do
k1 <- @findXorPeriod<n, 0.01>[f(k, _)];
res <- classifier(k, k1);
return res
end

def outerAttack() -> Bool do
k0 <- search[innerAttack]();
k0 <- @search<BitVec<n>>[innerAttack(_)];
return k0
end
963 changes: 156 additions & 807 deletions examples/matrix_search/matrix_search.qpl

Large diffs are not rendered by default.

250 changes: 20 additions & 230 deletions examples/matrix_search/matrix_search_cq.qpl

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions experiments/compile_loc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ module Main where
import Control.Monad (when)
import Text.Parsec.String (parseFromFile)
import Text.Printf (printf)
import qualified Traq.Analysis as P
import qualified Traq.Analysis as Traq
import qualified Traq.Compiler.Quantum
import qualified Traq.Data.Symbolic as Sym
Expand All @@ -30,7 +29,8 @@ subst vs p = P.mapSize Sym.unSym $ foldl substOne p vs

compileIt :: (ext ~ (Traq.DefaultPrims SizeT Double)) => P.Program ext -> Double -> Either String String
compileIt prog eps = do
compiled_prog <- Traq.Compiler.Quantum.lowerProgram P.SplitSimple (Traq.failProb eps) prog
prog_ann <- Traq.annotateProgWithErrorBudget (Traq.failProb eps) prog
compiled_prog <- Traq.Compiler.Quantum.lowerProgram prog_ann
return $ PP.toCodeString compiled_prog

data ExptConfig = ExptConfig
Expand Down
13 changes: 6 additions & 7 deletions experiments/matrixsearch.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ import Control.Monad (forM_)
import Data.List (inits)
import Text.Printf (printf)

import qualified Traq.Data.Context as Ctx
import qualified Traq.Data.Symbolic as Sym

import qualified Traq.Analysis as A
Expand Down Expand Up @@ -58,13 +57,13 @@ concreteEx = do
printDivider
putStrLn $ PP.toCodeString ex

let delta = P.l2NormError (0.001 :: Double)
let strat = P.SplitUsingNeedsEps
let eps = P.failProb (0.001 :: Double)
ex' <- either fail pure $ A.annotateProgWithErrorBudget eps ex

let u_formula_cost = P.unitaryQueryCost strat delta ex :: QueryCost Double
let u_formula_cost = P.costUProg ex' :: QueryCost Double

printDivider
Right exU <- return $ CompileU.lowerProgram strat Ctx.empty delta ex
Right exU <- return $ CompileU.lowerProgram ex'
putStrLn $ PP.toCodeString exU

let (u_true_cost, _) = CQPL.programCost exU
Expand All @@ -85,10 +84,10 @@ concreteQEx = do
putStrLn $ PP.toCodeString ex

let eps = P.failProb (0.001 :: Double)
let strat = P.SplitUsingNeedsEps
ex' <- either fail pure $ A.annotateProgWithErrorBudget eps ex

printDivider
Right exU <- return $ CompileQ.lowerProgram strat eps ex
Right exU <- return $ CompileQ.lowerProgram ex'
putStrLn $ PP.toCodeString exU
return ()

Expand Down
1 change: 1 addition & 0 deletions experiments/matrixsearchqcost.hs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ import Traq.Prelude
import Traq.Primitives
import Traq.Primitives.Search.DetSearch (DetSearch (..))
import Traq.Primitives.Search.Prelude
import Traq.Primitives.Search.QSearchCFNW
import Traq.Primitives.Search.RandomSearch (RandomSearch (..))
import qualified Traq.ProtoLang as P

Expand Down
5 changes: 3 additions & 2 deletions experiments/timing.hs
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ loadProgramFromFile fname = do
type ValidExt ext =
( PrecType ext ~ Double
, SizeType ext ~ SizeT
, Traq.Compiler.Quantum.Lowerable ext SizeT Double
, Traq.Compiler.Quantum.Lowerable (Traq.AnnFailProb ext) SizeT Double
, P.HasFreeVars ext
, Traq.AnnotateWithErrorBudgetU ext
, Traq.AnnotateWithErrorBudgetQ ext
Expand All @@ -47,7 +47,8 @@ type ValidExt ext =
-- | Compute the number of qubits used by the compiled program.
numQubitsRequired :: (ValidExt ext) => P.Program ext -> Double -> Either String SizeT
numQubitsRequired prog eps = do
compiled_prog <- Traq.Compiler.Quantum.lowerProgram Traq.SplitSimple (Traq.failProb eps) prog
prog' <- Traq.annotateProgWithErrorBudget (Traq.failProb eps) prog
compiled_prog <- Traq.Compiler.Quantum.lowerProgram prog'
return $ CQPL.numQubits compiled_prog

-- | Compute the wall-time by Traq to run a cost analysis
Expand Down
3 changes: 3 additions & 0 deletions src/Traq/Analysis/Annotate/Prelude.hs
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,9 @@ instance (TypeInferrable ext size) => (TypeInferrable (AnnFailProb ext) size) wh
instance (Evaluatable ext size prec) => Evaluatable (AnnFailProb ext) size prec where
eval (AnnFailProb _ e) = eval e

instance (HasFreeVars ext) => HasFreeVars (AnnFailProb ext) where
freeVarsList (AnnFailProb _ e) = freeVarsList e

-- ============================================================================
-- RS Monad to perform annotation
-- ============================================================================
Expand Down
Loading
Loading