diff --git a/examples/Makefile b/examples/Makefile new file mode 100644 index 0000000..cc80527 --- /dev/null +++ b/examples/Makefile @@ -0,0 +1,15 @@ +SUBDIRS = cryptanalysis matrix_search tree_generator hillclimb + +all: $(SUBDIRS) + +$(SUBDIRS): + $(MAKE) -C $@ + +define SUBDIR_RULE +$(1)/%: + $$(MAKE) -C $(1) $$* +endef + +$(foreach dir,$(SUBDIRS),$(eval $(call SUBDIR_RULE,$(dir)))) + +.PHONY: all $(SUBDIRS) diff --git a/examples/basic/assign.traq b/examples/basic/assign.traq new file mode 100644 index 0000000..87bba6e --- /dev/null +++ b/examples/basic/assign.traq @@ -0,0 +1,6 @@ +fn main(x : Fin<10>) -> Fin<10> do + one <- const 1 : Fin<10>; + x <- x + one; + x' <- x + one; + return x' +end \ No newline at end of file diff --git a/examples/cryptanalysis/3_round_feistel.qpl b/examples/cryptanalysis/3_round_feistel.qpl index db69ef9..727d006 100644 --- a/examples/cryptanalysis/3_round_feistel.qpl +++ b/examples/cryptanalysis/3_round_feistel.qpl @@ -106,7 +106,7 @@ uproc SimonOneRound_U_1(x_2 : OUT Fin<2>, x_3 : OUT BitVec<20>, y_2 : AUX Fin<2> } proc QSimon(AttackThreeRoundFeistel_zero : Fin<2>, AttackThreeRoundFeistel_s : BitVec<20>) { locals : (QSimon__u : Arr<32, Fin<2>>, QSimon__u_1 : Arr<32, BitVec<20>>) } { - for (i_1 in 0 .. < 32) { + for (#i_1 in 0 .. < 32) { meas SimonOneRound_U_1(QSimon__u[#i_1], QSimon__u_1[#i_1]); } // simon's post-processing: solve linear system: (AttackThreeRoundFeistel_zero, AttackThreeRoundFeistel_s) . (QSimon__u, QSimon__u_1) = 0 diff --git a/examples/cryptanalysis/even_mansour.qpl b/examples/cryptanalysis/even_mansour.qpl index b89545d..d5dd02e 100644 --- a/examples/cryptanalysis/even_mansour.qpl +++ b/examples/cryptanalysis/even_mansour.qpl @@ -6,70 +6,70 @@ ext uproc E_U(BitVec<20>, BitVec<20>); ext proc E(BitVec<20>, BitVec<20>); -uproc f_U(f_x : IN BitVec<20>, f_fx : OUT BitVec<20>, f_ex : AUX BitVec<20>, f_px : AUX BitVec<20>, f_ex_1 : AUX BitVec<20>, f_px_1 : AUX BitVec<20>, f_fx_1 : AUX BitVec<20>) { - call E_U(f_x, f_ex_1); - f_ex, f_ex_1 *= SWAP; - call P_U(f_x, f_px_1); - f_px, f_px_1 *= SWAP; - f_ex, f_px, f_fx_1 *= Embed[(f_ex, f_px) => (f_ex ^ f_px)]; - f_fx, f_fx_1 *= SWAP; +uproc f_U(x : IN BitVec<20>, fx : OUT BitVec<20>, ex : AUX BitVec<20>, px : AUX BitVec<20>, ex_1 : AUX BitVec<20>, px_1 : AUX BitVec<20>, fx_1 : AUX BitVec<20>) { + call E_U(x, ex_1); + ex, ex_1 *= SWAP; + call P_U(x, px_1); + px, px_1 *= SWAP; + ex, px, fx_1 *= Embed[(ex, px) => (ex ^ px)]; + fx, fx_1 *= SWAP; } -proc f(f_x : BitVec<20>, f_fx : BitVec<20>) { locals : (f_ex : BitVec<20>, f_px : BitVec<20>) } { - call E(f_x, f_ex); - call P(f_x, f_px); - f_fx := (f_ex ^ f_px); +proc f(x : BitVec<20>, fx : BitVec<20>) { locals : (ex : BitVec<20>, px : BitVec<20>) } { + call E(x, ex); + call P(x, px); + fx := (ex ^ px); } -uproc SimonOneRound_U(x : OUT BitVec<20>, y : AUX BitVec<20>, yy : AUX BitVec<20>, aux : AUX BitVec<20>, aux_1 : AUX BitVec<20>, aux_2 : AUX BitVec<20>, aux_3 : AUX BitVec<20>, aux_4 : AUX BitVec<20>) { - x *= Distr[uniform : BitVec<20>]; - call f_U(x, y, aux, aux_1, aux_2, aux_3, aux_4); +uproc SimonOneRound_U(x_1 : OUT BitVec<20>, y : AUX BitVec<20>, yy : AUX BitVec<20>, aux : AUX BitVec<20>, aux_1 : AUX BitVec<20>, aux_2 : AUX BitVec<20>, aux_3 : AUX BitVec<20>, aux_4 : AUX BitVec<20>) { + x_1 *= Distr[uniform : BitVec<20>]; + call f_U(x_1, y, aux, aux_1, aux_2, aux_3, aux_4); y, yy *= COPY; - call-adj f_U(x, y, aux, aux_1, aux_2, aux_3, aux_4); - x *= Adj-Distr[uniform : BitVec<20>]; + call-adj f_U(x_1, y, aux, aux_1, aux_2, aux_3, aux_4); + x_1 *= Adj-Distr[uniform : BitVec<20>]; } -uproc USimon(BreakEM_k1_1 : OUT BitVec<20>, USimon_aux : AUX Arr<31, BitVec<20>>, USimon_aux_1 : AUX Arr<31, BitVec<20>>, USimon_aux_2 : AUX Arr<31, BitVec<20>>, USimon_aux_3 : AUX Arr<31, BitVec<20>>, USimon_aux_4 : AUX Arr<31, BitVec<20>>, USimon_aux_5 : AUX Arr<31, BitVec<20>>, USimon_aux_6 : AUX Arr<31, BitVec<20>>, USimon_aux_7 : AUX Arr<31, BitVec<20>>) { +uproc USimon(k1_1 : OUT BitVec<20>, USimon_aux : AUX Arr<31, BitVec<20>>, USimon_aux_1 : AUX Arr<31, BitVec<20>>, USimon_aux_2 : AUX Arr<31, BitVec<20>>, USimon_aux_3 : AUX Arr<31, BitVec<20>>, USimon_aux_4 : AUX Arr<31, BitVec<20>>, USimon_aux_5 : AUX Arr<31, BitVec<20>>, USimon_aux_6 : AUX Arr<31, BitVec<20>>, USimon_aux_7 : AUX Arr<31, BitVec<20>>) { for (#i in 0 .. < 31) { call SimonOneRound_U(USimon_aux[#i], USimon_aux_1[#i], USimon_aux_2[#i], USimon_aux_3[#i], USimon_aux_4[#i], USimon_aux_5[#i], USimon_aux_6[#i], USimon_aux_7[#i]); } - // simon's post-processing: unitarily solve linear system: (BreakEM_k1_1) . (USimon_aux) = 0 + // simon's post-processing: unitarily solve linear system: (k1_1) . (USimon_aux) = 0 } -uproc BreakEM_U(BreakEM_k1 : OUT BitVec<20>, BreakEM_k2 : OUT BitVec<20>, BreakEM_ze : AUX BitVec<20>, BreakEM_e_0 : AUX BitVec<20>, BreakEM_p_k1 : AUX BitVec<20>, BreakEM_ze_1 : AUX BitVec<20>, BreakEM_k1_1 : AUX BitVec<20>, x : AUX BitVec<20>, y : AUX BitVec<20>, yy : AUX BitVec<20>, aux : AUX BitVec<20>, aux_1 : AUX BitVec<20>, aux_2 : AUX BitVec<20>, aux_3 : AUX BitVec<20>, aux_4 : AUX BitVec<20>, USimon_aux : AUX Arr<31, BitVec<20>>, USimon_aux_1 : AUX Arr<31, BitVec<20>>, USimon_aux_2 : AUX Arr<31, BitVec<20>>, USimon_aux_3 : AUX Arr<31, BitVec<20>>, USimon_aux_4 : AUX Arr<31, BitVec<20>>, USimon_aux_5 : AUX Arr<31, BitVec<20>>, USimon_aux_6 : AUX Arr<31, BitVec<20>>, USimon_aux_7 : AUX Arr<31, BitVec<20>>, aux_prim : AUX Arr<31, BitVec<20>>, aux_prim_1 : AUX Arr<31, BitVec<20>>, aux_prim_2 : AUX Arr<31, BitVec<20>>, aux_prim_3 : AUX Arr<31, BitVec<20>>, aux_prim_4 : AUX Arr<31, BitVec<20>>, aux_prim_5 : AUX Arr<31, BitVec<20>>, aux_prim_6 : AUX Arr<31, BitVec<20>>, aux_prim_7 : AUX Arr<31, BitVec<20>>, BreakEM_e_0_1 : AUX BitVec<20>, BreakEM_p_k1_1 : AUX BitVec<20>, BreakEM_k2_1 : AUX BitVec<20>) { - BreakEM_ze_1 *= Embed[() => 0:BitVec<20>]; - BreakEM_ze, BreakEM_ze_1 *= SWAP; - call USimon(BreakEM_k1_1, aux_prim, aux_prim_1, aux_prim_2, aux_prim_3, aux_prim_4, aux_prim_5, aux_prim_6, aux_prim_7); - BreakEM_k1, BreakEM_k1_1 *= SWAP; - call E_U(BreakEM_ze, BreakEM_e_0_1); - BreakEM_e_0, BreakEM_e_0_1 *= SWAP; - call P_U(BreakEM_k1, BreakEM_p_k1_1); - BreakEM_p_k1, BreakEM_p_k1_1 *= SWAP; - BreakEM_e_0, BreakEM_p_k1, BreakEM_k2_1 *= Embed[(BreakEM_e_0, BreakEM_p_k1) => (BreakEM_e_0 ^ BreakEM_p_k1)]; - BreakEM_k2, BreakEM_k2_1 *= SWAP; +uproc BreakEM_U(k1 : OUT BitVec<20>, k2 : OUT BitVec<20>, ze : AUX BitVec<20>, e_0 : AUX BitVec<20>, p_k1 : AUX BitVec<20>, ze_1 : AUX BitVec<20>, k1_1 : AUX BitVec<20>, x_1 : AUX BitVec<20>, y : AUX BitVec<20>, yy : AUX BitVec<20>, aux : AUX BitVec<20>, aux_1 : AUX BitVec<20>, aux_2 : AUX BitVec<20>, aux_3 : AUX BitVec<20>, aux_4 : AUX BitVec<20>, USimon_aux : AUX Arr<31, BitVec<20>>, USimon_aux_1 : AUX Arr<31, BitVec<20>>, USimon_aux_2 : AUX Arr<31, BitVec<20>>, USimon_aux_3 : AUX Arr<31, BitVec<20>>, USimon_aux_4 : AUX Arr<31, BitVec<20>>, USimon_aux_5 : AUX Arr<31, BitVec<20>>, USimon_aux_6 : AUX Arr<31, BitVec<20>>, USimon_aux_7 : AUX Arr<31, BitVec<20>>, aux_prim : AUX Arr<31, BitVec<20>>, aux_prim_1 : AUX Arr<31, BitVec<20>>, aux_prim_2 : AUX Arr<31, BitVec<20>>, aux_prim_3 : AUX Arr<31, BitVec<20>>, aux_prim_4 : AUX Arr<31, BitVec<20>>, aux_prim_5 : AUX Arr<31, BitVec<20>>, aux_prim_6 : AUX Arr<31, BitVec<20>>, aux_prim_7 : AUX Arr<31, BitVec<20>>, e_0_1 : AUX BitVec<20>, p_k1_1 : AUX BitVec<20>, k2_1 : AUX BitVec<20>) { + ze_1 *= Embed[() => 0:BitVec<20>]; + ze, ze_1 *= SWAP; + call USimon(k1_1, aux_prim, aux_prim_1, aux_prim_2, aux_prim_3, aux_prim_4, aux_prim_5, aux_prim_6, aux_prim_7); + k1, k1_1 *= SWAP; + call E_U(ze, e_0_1); + e_0, e_0_1 *= SWAP; + call P_U(k1, p_k1_1); + p_k1, p_k1_1 *= SWAP; + e_0, p_k1, k2_1 *= Embed[(e_0, p_k1) => (e_0 ^ p_k1)]; + k2, k2_1 *= SWAP; } -uproc SimonOneRound_U_1(x_1 : OUT BitVec<20>, y_1 : AUX BitVec<20>, yy_1 : AUX BitVec<20>, aux_5 : AUX BitVec<20>, aux_6 : AUX BitVec<20>, aux_7 : AUX BitVec<20>, aux_8 : AUX BitVec<20>, aux_9 : AUX BitVec<20>) { - x_1 *= Distr[uniform : BitVec<20>]; - call f_U(x_1, y_1, aux_5, aux_6, aux_7, aux_8, aux_9); +uproc SimonOneRound_U_1(x_2 : OUT BitVec<20>, y_1 : AUX BitVec<20>, yy_1 : AUX BitVec<20>, aux_5 : AUX BitVec<20>, aux_6 : AUX BitVec<20>, aux_7 : AUX BitVec<20>, aux_8 : AUX BitVec<20>, aux_9 : AUX BitVec<20>) { + x_2 *= Distr[uniform : BitVec<20>]; + call f_U(x_2, y_1, aux_5, aux_6, aux_7, aux_8, aux_9); y_1, yy_1 *= COPY; - call-adj f_U(x_1, y_1, aux_5, aux_6, aux_7, aux_8, aux_9); - x_1 *= Adj-Distr[uniform : BitVec<20>]; + call-adj f_U(x_2, y_1, aux_5, aux_6, aux_7, aux_8, aux_9); + x_2 *= Adj-Distr[uniform : BitVec<20>]; } -proc QSimon(BreakEM_k1 : BitVec<20>) { locals : (QSimon__u : Arr<31, BitVec<20>>) } { - for (i_1 in 0 .. < 31) { +proc QSimon(k1 : BitVec<20>) { locals : (QSimon__u : Arr<31, BitVec<20>>) } { + for (#i_1 in 0 .. < 31) { meas SimonOneRound_U_1(QSimon__u[#i_1]); } - // simon's post-processing: solve linear system: (BreakEM_k1) . (QSimon__u) = 0 + // simon's post-processing: solve linear system: (k1) . (QSimon__u) = 0 } -proc BreakEM(BreakEM_k1 : BitVec<20>, BreakEM_k2 : BitVec<20>) { locals : (BreakEM_ze : BitVec<20>, BreakEM_e_0 : BitVec<20>, BreakEM_p_k1 : BitVec<20>, x_1 : BitVec<20>, y_1 : BitVec<20>, yy_1 : BitVec<20>, aux_5 : BitVec<20>, aux_6 : BitVec<20>, aux_7 : BitVec<20>, aux_8 : BitVec<20>, aux_9 : BitVec<20>, QSimon__u : Arr<31, BitVec<20>>) } { - BreakEM_ze := 0:BitVec<20>; - call QSimon(BreakEM_k1); - call E(BreakEM_ze, BreakEM_e_0); - call P(BreakEM_k1, BreakEM_p_k1); - BreakEM_k2 := (BreakEM_e_0 ^ BreakEM_p_k1); +proc BreakEM(k1 : BitVec<20>, k2 : BitVec<20>) { locals : (ze : BitVec<20>, e_0 : BitVec<20>, p_k1 : BitVec<20>, x_2 : BitVec<20>, y_1 : BitVec<20>, yy_1 : BitVec<20>, aux_5 : BitVec<20>, aux_6 : BitVec<20>, aux_7 : BitVec<20>, aux_8 : BitVec<20>, aux_9 : BitVec<20>, QSimon__u : Arr<31, BitVec<20>>) } { + ze := 0:BitVec<20>; + call QSimon(k1); + call E(ze, e_0); + call P(k1, p_k1); + k2 := (e_0 ^ p_k1); } diff --git a/examples/cryptanalysis/grover_meets_simon.qpl b/examples/cryptanalysis/grover_meets_simon.qpl index 63bec77..fab4c3f 100644 --- a/examples/cryptanalysis/grover_meets_simon.qpl +++ b/examples/cryptanalysis/grover_meets_simon.qpl @@ -56,7 +56,7 @@ uproc SimonOneRound_U_1(innerAttack_k : BitVec<20>, x_1 : OUT BitVec<20>, y_1 : } proc QSimon(innerAttack_k : BitVec<20>, innerAttack_k1 : BitVec<20>) { locals : (QSimon__u : Arr<79, BitVec<20>>) } { - for (i_1 in 0 .. < 79) { + for (#i_1 in 0 .. < 79) { meas SimonOneRound_U_1(QSimon__u[#i_1]); } // simon's post-processing: solve linear system: (innerAttack_k1) . (QSimon__u) = 0 @@ -80,7 +80,7 @@ uproc USearch(outerAttack_ok_1 : OUT Fin<2>, outerAttack_k0_1 : OUT BitVec<20>, ctrl[#run_ix], aux_37, pred_out[#run_ix] *= Toffoli; call-adj innerAttack_U(s_arg[#run_ix], aux_37, aux_10, aux_11, aux_12, aux_13, aux_14, aux_15, aux_16, aux_17, aux_18, aux_19, aux_20, aux_21, aux_22, aux_23, aux_24, aux_25, aux_26, aux_27, aux_28, aux_29, aux_30, aux_31, aux_32, aux_33, aux_34, aux_35, aux_36); s_arg[#run_ix] *= Adj-Distr[uniform : BitVec<20>]; - s_arg[#run_ix] *= Refl0; + s_arg[#run_ix] *= PhaseOnZero(3.141592653589793); s_arg[#run_ix] *= Distr[uniform : BitVec<20>]; n_iter[#run_ix], ctrl[#run_ix] *= Embed[(a) => (a <= #LIM)]; } @@ -110,7 +110,7 @@ uproc Grover[k](x_2 : IN BitVec<20>, outerAttack_ok : OUT Fin<2>, aux_38 : AUX B repeat (#k) { call innerAttack_U(x_2, outerAttack_ok, aux_38, aux_39, aux_40, aux_41, aux_42, aux_43, aux_44, aux_45, aux_46, aux_47, aux_48, aux_49, aux_50, aux_51, aux_52, aux_53, aux_54, aux_55, aux_56, aux_57, aux_58, aux_59, aux_60, aux_61, aux_62, aux_63, aux_64); x_2 *= Adj-Distr[uniform : BitVec<20>]; - x_2 *= Refl0; + x_2 *= PhaseOnZero(3.141592653589793); x_2 *= Distr[uniform : BitVec<20>]; } outerAttack_ok *= H; diff --git a/examples/cryptanalysis/period_finding.qpl b/examples/cryptanalysis/period_finding.qpl index 65f4a80..b68f8aa 100644 --- a/examples/cryptanalysis/period_finding.qpl +++ b/examples/cryptanalysis/period_finding.qpl @@ -10,16 +10,16 @@ uproc SimonOneRound_U(x : OUT BitVec<20>, y : AUX BitVec<20>, yy : AUX BitVec<20 x *= Adj-Distr[uniform : BitVec<20>]; } -uproc USimon(main_s_1 : OUT BitVec<20>, USimon_aux : AUX Arr<31, BitVec<20>>, USimon_aux_1 : AUX Arr<31, BitVec<20>>, USimon_aux_2 : AUX Arr<31, BitVec<20>>) { +uproc USimon(s_1 : OUT BitVec<20>, USimon_aux : AUX Arr<31, BitVec<20>>, USimon_aux_1 : AUX Arr<31, BitVec<20>>, USimon_aux_2 : AUX Arr<31, BitVec<20>>) { for (#i in 0 .. < 31) { call SimonOneRound_U(USimon_aux[#i], USimon_aux_1[#i], USimon_aux_2[#i]); } - // simon's post-processing: unitarily solve linear system: (main_s_1) . (USimon_aux) = 0 + // simon's post-processing: unitarily solve linear system: (s_1) . (USimon_aux) = 0 } -uproc main_U(main_s : OUT BitVec<20>, main_s_1 : AUX BitVec<20>, x : AUX BitVec<20>, y : AUX BitVec<20>, yy : AUX BitVec<20>, USimon_aux : AUX Arr<31, BitVec<20>>, USimon_aux_1 : AUX Arr<31, BitVec<20>>, USimon_aux_2 : AUX Arr<31, BitVec<20>>, aux_prim : AUX Arr<31, BitVec<20>>, aux_prim_1 : AUX Arr<31, BitVec<20>>, aux_prim_2 : AUX Arr<31, BitVec<20>>) { - call USimon(main_s_1, aux_prim, aux_prim_1, aux_prim_2); - main_s, main_s_1 *= SWAP; +uproc main_U(s : OUT BitVec<20>, s_1 : AUX BitVec<20>, x : AUX BitVec<20>, y : AUX BitVec<20>, yy : AUX BitVec<20>, USimon_aux : AUX Arr<31, BitVec<20>>, USimon_aux_1 : AUX Arr<31, BitVec<20>>, USimon_aux_2 : AUX Arr<31, BitVec<20>>, aux_prim : AUX Arr<31, BitVec<20>>, aux_prim_1 : AUX Arr<31, BitVec<20>>, aux_prim_2 : AUX Arr<31, BitVec<20>>) { + call USimon(s_1, aux_prim, aux_prim_1, aux_prim_2); + s, s_1 *= SWAP; } uproc SimonOneRound_U_1(x_1 : OUT BitVec<20>, y_1 : AUX BitVec<20>, yy_1 : AUX BitVec<20>) { @@ -30,15 +30,15 @@ uproc SimonOneRound_U_1(x_1 : OUT BitVec<20>, y_1 : AUX BitVec<20>, yy_1 : AUX B x_1 *= Adj-Distr[uniform : BitVec<20>]; } -proc QSimon(main_s : BitVec<20>) { locals : (QSimon__u : Arr<31, BitVec<20>>) } { - for (i_1 in 0 .. < 31) { +proc QSimon(s : BitVec<20>) { locals : (QSimon__u : Arr<31, BitVec<20>>) } { + for (#i_1 in 0 .. < 31) { meas SimonOneRound_U_1(QSimon__u[#i_1]); } - // simon's post-processing: solve linear system: (main_s) . (QSimon__u) = 0 + // simon's post-processing: solve linear system: (s) . (QSimon__u) = 0 } -proc main(main_s : BitVec<20>) { locals : (x_1 : BitVec<20>, y_1 : BitVec<20>, yy_1 : BitVec<20>, QSimon__u : Arr<31, BitVec<20>>) } { - call QSimon(main_s); +proc main(s : BitVec<20>) { locals : (x_1 : BitVec<20>, y_1 : BitVec<20>, yy_1 : BitVec<20>, QSimon__u : Arr<31, BitVec<20>>) } { + call QSimon(s); } diff --git a/examples/hillclimb/Makefile b/examples/hillclimb/Makefile new file mode 100644 index 0000000..70307e1 --- /dev/null +++ b/examples/hillclimb/Makefile @@ -0,0 +1,11 @@ +PROJ_DEPS=../../src ../../tools ../../traq.cabal + +all: max_sat_hillclimb.qpl steep_max_sat.qpl + +%.qpl: %.traq $(PROJ_DEPS) + cd ../../ && cabal run compile -- \ + -i examples/hillclimb/$< \ + -o examples/hillclimb/$@ \ + -p 0.001 \ + --arg n=20 \ + --arg W=1000 diff --git a/examples/hillclimb/max_sat_hillclimb.qpl b/examples/hillclimb/max_sat_hillclimb.qpl new file mode 100644 index 0000000..40f15f8 --- /dev/null +++ b/examples/hillclimb/max_sat_hillclimb.qpl @@ -0,0 +1,130 @@ +ext uproc Phi_U(Arr<20, Fin<2>>, Fin<1000>); + +ext proc Phi(Arr<20, Fin<2>>, Fin<1000>); + +uproc good_U(good_x : IN Arr<20, Fin<2>>, good_i : IN Fin<20>, good_ok : OUT Fin<2>, good_w : AUX Fin<1000>, good_b : AUX Fin<2>, good_b' : AUX Fin<2>, good_x' : AUX Arr<20, Fin<2>>, good_w' : AUX Fin<1000>, good_w_1 : AUX Fin<1000>, good_b_1 : AUX Fin<2>, good_b'_1 : AUX Fin<2>, good_x'_1 : AUX Arr<20, Fin<2>>, good_w'_1 : AUX Fin<1000>, good_ok_1 : AUX Fin<2>) { + call Phi_U(good_x, good_w_1); + good_w, good_w_1 *= SWAP; + good_i, good_x, good_b_1 *= Embed[(good_i, good_x) => good_x[good_i]]; + good_b, good_b_1 *= SWAP; + good_b, good_b'_1 *= Embed[(good_b) => not good_b]; + good_b', good_b'_1 *= SWAP; + good_b, good_i, good_x, good_x'_1 *= Embed[(good_b, good_i, good_x) => update good_x[good_i] = good_b]; + good_x', good_x'_1 *= SWAP; + call Phi_U(good_x', good_w'_1); + good_w', good_w'_1 *= SWAP; + good_w, good_w', good_ok_1 *= Embed[(good_w, good_w') => (good_w < good_w')]; + good_ok, good_ok_1 *= SWAP; +} + +proc good(good_x : Arr<20, Fin<2>>, good_i : Fin<20>, good_ok : Fin<2>) { locals : (good_w : Fin<1000>, good_b : Fin<2>, good_b' : Fin<2>, good_x' : Arr<20, Fin<2>>, good_w' : Fin<1000>) } { + call Phi(good_x, good_w); + good_b := good_x[good_i]; + good_b' := not good_b; + good_x' := update good_x[good_i] = good_b; + call Phi(good_x', good_w'); + good_ok := (good_w < good_w'); +} + +// USearch[Fin 20, 3.333333333333333e-4] +uproc USearch(hillclimb_iter_x : Arr<20, Fin<2>>, hillclimb_iter_ok_1 : OUT Fin<2>, hillclimb_iter_i_1 : OUT Fin<20>, aux : AUX Fin<1000>, aux_1 : AUX Fin<2>, aux_2 : AUX Fin<2>, aux_3 : AUX Arr<20, Fin<2>>, aux_4 : AUX Fin<1000>, aux_5 : AUX Fin<1000>, aux_6 : AUX Fin<2>, aux_7 : AUX Fin<2>, aux_8 : AUX Arr<20, Fin<2>>, aux_9 : AUX Fin<1000>, aux_10 : AUX Fin<2>, aux_11 : AUX Fin<2>, ctrl : AUX Arr<17, Fin<2>>, pred_out : AUX Arr<17, Fin<2>>, n_iter : AUX Arr<17, Fin<4>>, s_arg : AUX Arr<17, Fin<20>>) { + for (#run_ix in 0 .. < 17) { + n_iter[#run_ix] *= Distr[uniform : Fin<4>]; + pred_out[#run_ix] *= X; + pred_out[#run_ix] *= H; + s_arg[#run_ix] *= Distr[uniform : Fin<20>]; + for (#LIM in 0 .. < 4) { + n_iter[#run_ix], ctrl[#run_ix] *= Embed[(a) => (a <= #LIM)]; + call good_U(hillclimb_iter_x, s_arg[#run_ix], aux_11, aux, aux_1, aux_2, aux_3, aux_4, aux_5, aux_6, aux_7, aux_8, aux_9, aux_10); + ctrl[#run_ix], aux_11, pred_out[#run_ix] *= Toffoli; + call-adj good_U(hillclimb_iter_x, s_arg[#run_ix], aux_11, aux, aux_1, aux_2, aux_3, aux_4, aux_5, aux_6, aux_7, aux_8, aux_9, aux_10); + s_arg[#run_ix] *= Adj-Distr[uniform : Fin<20>]; + s_arg[#run_ix] *= PhaseOnZero(3.141592653589793); + s_arg[#run_ix] *= Distr[uniform : Fin<20>]; + n_iter[#run_ix], ctrl[#run_ix] *= Embed[(a) => (a <= #LIM)]; + } + pred_out[#run_ix] *= H; + pred_out[#run_ix] *= X; + n_iter[#run_ix] *= Adj-Distr[uniform : Fin<4>]; + ctrl[#run_ix] *= X; + call good_U(hillclimb_iter_x, s_arg[#run_ix], aux_11, aux, aux_1, aux_2, aux_3, aux_4, aux_5, aux_6, aux_7, aux_8, aux_9, aux_10); + ctrl[#run_ix], aux_11, pred_out[#run_ix] *= Toffoli; + call-adj good_U(hillclimb_iter_x, s_arg[#run_ix], aux_11, aux, aux_1, aux_2, aux_3, aux_4, aux_5, aux_6, aux_7, aux_8, aux_9, aux_10); + ctrl[#run_ix] *= X; + } + pred_out, hillclimb_iter_ok_1 *= Embed[(a) => or a]; + s_arg, pred_out, hillclimb_iter_i_1 *= Embed[(a, f) => (a selectOn f)]; +} + +uproc hillclimb_iter_U(hillclimb_iter_x : IN Arr<20, Fin<2>>, hillclimb_iter_x' : OUT Arr<20, Fin<2>>, hillclimb_iter_ok : AUX Fin<2>, hillclimb_iter_i : AUX Fin<20>, hillclimb_iter_b : AUX Fin<2>, hillclimb_iter_b' : AUX Fin<2>, hillclimb_iter_ok_1 : AUX Fin<2>, hillclimb_iter_i_1 : AUX Fin<20>, aux : AUX Fin<1000>, aux_1 : AUX Fin<2>, aux_2 : AUX Fin<2>, aux_3 : AUX Arr<20, Fin<2>>, aux_4 : AUX Fin<1000>, aux_5 : AUX Fin<1000>, aux_6 : AUX Fin<2>, aux_7 : AUX Fin<2>, aux_8 : AUX Arr<20, Fin<2>>, aux_9 : AUX Fin<1000>, aux_10 : AUX Fin<2>, aux_11 : AUX Fin<2>, ctrl : AUX Arr<17, Fin<2>>, pred_out : AUX Arr<17, Fin<2>>, n_iter : AUX Arr<17, Fin<4>>, s_arg : AUX Arr<17, Fin<20>>, aux_prim : AUX Fin<1000>, aux_prim_1 : AUX Fin<2>, aux_prim_2 : AUX Fin<2>, aux_prim_3 : AUX Arr<20, Fin<2>>, aux_prim_4 : AUX Fin<1000>, aux_prim_5 : AUX Fin<1000>, aux_prim_6 : AUX Fin<2>, aux_prim_7 : AUX Fin<2>, aux_prim_8 : AUX Arr<20, Fin<2>>, aux_prim_9 : AUX Fin<1000>, aux_prim_10 : AUX Fin<2>, aux_prim_11 : AUX Fin<2>, aux_prim_12 : AUX Arr<17, Fin<2>>, aux_prim_13 : AUX Arr<17, Fin<2>>, aux_prim_14 : AUX Arr<17, Fin<4>>, aux_prim_15 : AUX Arr<17, Fin<20>>, hillclimb_iter_b_1 : AUX Fin<2>, hillclimb_iter_b'_1 : AUX Fin<2>, hillclimb_iter_x'_1 : AUX Arr<20, Fin<2>>) { + call USearch(hillclimb_iter_x, hillclimb_iter_ok_1, hillclimb_iter_i_1, aux_prim, aux_prim_1, aux_prim_2, aux_prim_3, aux_prim_4, aux_prim_5, aux_prim_6, aux_prim_7, aux_prim_8, aux_prim_9, aux_prim_10, aux_prim_11, aux_prim_12, aux_prim_13, aux_prim_14, aux_prim_15); + hillclimb_iter_ok, hillclimb_iter_i, hillclimb_iter_ok_1, hillclimb_iter_i_1 *= SWAP; + hillclimb_iter_i, hillclimb_iter_x, hillclimb_iter_b_1 *= Embed[(hillclimb_iter_i, hillclimb_iter_x) => hillclimb_iter_x[hillclimb_iter_i]]; + hillclimb_iter_b, hillclimb_iter_b_1 *= SWAP; + hillclimb_iter_b, hillclimb_iter_b'_1 *= Embed[(hillclimb_iter_b) => not hillclimb_iter_b]; + hillclimb_iter_b', hillclimb_iter_b'_1 *= SWAP; + hillclimb_iter_b, hillclimb_iter_i, hillclimb_iter_x, hillclimb_iter_x'_1 *= Embed[(hillclimb_iter_b, hillclimb_iter_i, hillclimb_iter_x) => update hillclimb_iter_x[hillclimb_iter_i] = hillclimb_iter_b]; + hillclimb_iter_x', hillclimb_iter_x'_1 *= SWAP; +} + +// Grover[...] +uproc Grover[k](hillclimb_iter_x : Arr<20, Fin<2>>, x : IN Fin<20>, hillclimb_iter_ok : OUT Fin<2>, aux_12 : AUX Fin<1000>, aux_13 : AUX Fin<2>, aux_14 : AUX Fin<2>, aux_15 : AUX Arr<20, Fin<2>>, aux_16 : AUX Fin<1000>, aux_17 : AUX Fin<1000>, aux_18 : AUX Fin<2>, aux_19 : AUX Fin<2>, aux_20 : AUX Arr<20, Fin<2>>, aux_21 : AUX Fin<1000>, aux_22 : AUX Fin<2>) { + hillclimb_iter_ok *= X; + hillclimb_iter_ok *= H; + x *= Distr[uniform : Fin<20>]; + repeat (#k) { + call good_U(hillclimb_iter_x, x, hillclimb_iter_ok, aux_12, aux_13, aux_14, aux_15, aux_16, aux_17, aux_18, aux_19, aux_20, aux_21, aux_22); + x *= Adj-Distr[uniform : Fin<20>]; + x *= PhaseOnZero(3.141592653589793); + x *= Distr[uniform : Fin<20>]; + } + hillclimb_iter_ok *= H; + hillclimb_iter_ok *= X; +} + +// QSearch[3.333333333333333e-4] +proc QSearch(hillclimb_iter_x : Arr<20, Fin<2>>, hillclimb_iter_ok : Fin<2>, hillclimb_iter_i : Fin<20>) { locals : (not_done : Fin<2>, Q_sum : Fin<42>, j : Fin<42>, j_lim : Fin<42>) } { + repeat (8) { + Q_sum := 0:Fin<42>; + for (j_lim in [1:Fin<42>, 1:Fin<42>, 1:Fin<42>, 2:Fin<42>, 2:Fin<42>, 2:Fin<42>, 3:Fin<42>, 4:Fin<42>, 4:Fin<42>, 4:Fin<42>, 4:Fin<42>, 4:Fin<42>, 4:Fin<42>, 4:Fin<42>]) { + j :=$ [1 .. j_lim]; + Q_sum := (Q_sum + j); + not_done := (not_done && (Q_sum <= j_lim)); + if (not_done) { + meas Grover[j](hillclimb_iter_x, hillclimb_iter_i, hillclimb_iter_ok); + meas good_U(hillclimb_iter_x, hillclimb_iter_i, hillclimb_iter_ok); + not_done := (not_done && hillclimb_iter_ok); + } else { + skip; + } + } + } +} + +proc hillclimb_iter(hillclimb_iter_x : Arr<20, Fin<2>>, hillclimb_iter_x' : Arr<20, Fin<2>>) { locals : (hillclimb_iter_ok : Fin<2>, hillclimb_iter_i : Fin<20>, hillclimb_iter_b : Fin<2>, hillclimb_iter_b' : Fin<2>) } { + call QSearch(hillclimb_iter_x, hillclimb_iter_ok, hillclimb_iter_i); + hillclimb_iter_b := hillclimb_iter_x[hillclimb_iter_i]; + hillclimb_iter_b' := not hillclimb_iter_b; + hillclimb_iter_x' := update hillclimb_iter_x[hillclimb_iter_i] = hillclimb_iter_b; +} + +uproc hillclimb_3_U(hillclimb_3_x_3 : OUT Arr<20, Fin<2>>, hillclimb_3_x_0 : AUX Arr<20, Fin<2>>, hillclimb_3_x_1 : AUX Arr<20, Fin<2>>, hillclimb_3_x_2 : AUX Arr<20, Fin<2>>, hillclimb_3_x_0_1 : AUX Arr<20, Fin<2>>, hillclimb_3_x_1_1 : AUX Arr<20, Fin<2>>, aux_23 : AUX Fin<2>, aux_24 : AUX Fin<20>, aux_25 : AUX Fin<2>, aux_26 : AUX Fin<2>, aux_27 : AUX Fin<2>, aux_28 : AUX Fin<20>, aux_29 : AUX Fin<1000>, aux_30 : AUX Fin<2>, aux_31 : AUX Fin<2>, aux_32 : AUX Arr<20, Fin<2>>, aux_33 : AUX Fin<1000>, aux_34 : AUX Fin<1000>, aux_35 : AUX Fin<2>, aux_36 : AUX Fin<2>, aux_37 : AUX Arr<20, Fin<2>>, aux_38 : AUX Fin<1000>, aux_39 : AUX Fin<2>, aux_40 : AUX Fin<2>, aux_41 : AUX Arr<17, Fin<2>>, aux_42 : AUX Arr<17, Fin<2>>, aux_43 : AUX Arr<17, Fin<4>>, aux_44 : AUX Arr<17, Fin<20>>, aux_45 : AUX Fin<1000>, aux_46 : AUX Fin<2>, aux_47 : AUX Fin<2>, aux_48 : AUX Arr<20, Fin<2>>, aux_49 : AUX Fin<1000>, aux_50 : AUX Fin<1000>, aux_51 : AUX Fin<2>, aux_52 : AUX Fin<2>, aux_53 : AUX Arr<20, Fin<2>>, aux_54 : AUX Fin<1000>, aux_55 : AUX Fin<2>, aux_56 : AUX Fin<2>, aux_57 : AUX Arr<17, Fin<2>>, aux_58 : AUX Arr<17, Fin<2>>, aux_59 : AUX Arr<17, Fin<4>>, aux_60 : AUX Arr<17, Fin<20>>, aux_61 : AUX Fin<2>, aux_62 : AUX Fin<2>, aux_63 : AUX Arr<20, Fin<2>>, hillclimb_3_x_2_1 : AUX Arr<20, Fin<2>>, aux_64 : AUX Fin<2>, aux_65 : AUX Fin<20>, aux_66 : AUX Fin<2>, aux_67 : AUX Fin<2>, aux_68 : AUX Fin<2>, aux_69 : AUX Fin<20>, aux_70 : AUX Fin<1000>, aux_71 : AUX Fin<2>, aux_72 : AUX Fin<2>, aux_73 : AUX Arr<20, Fin<2>>, aux_74 : AUX Fin<1000>, aux_75 : AUX Fin<1000>, aux_76 : AUX Fin<2>, aux_77 : AUX Fin<2>, aux_78 : AUX Arr<20, Fin<2>>, aux_79 : AUX Fin<1000>, aux_80 : AUX Fin<2>, aux_81 : AUX Fin<2>, aux_82 : AUX Arr<17, Fin<2>>, aux_83 : AUX Arr<17, Fin<2>>, aux_84 : AUX Arr<17, Fin<4>>, aux_85 : AUX Arr<17, Fin<20>>, aux_86 : AUX Fin<1000>, aux_87 : AUX Fin<2>, aux_88 : AUX Fin<2>, aux_89 : AUX Arr<20, Fin<2>>, aux_90 : AUX Fin<1000>, aux_91 : AUX Fin<1000>, aux_92 : AUX Fin<2>, aux_93 : AUX Fin<2>, aux_94 : AUX Arr<20, Fin<2>>, aux_95 : AUX Fin<1000>, aux_96 : AUX Fin<2>, aux_97 : AUX Fin<2>, aux_98 : AUX Arr<17, Fin<2>>, aux_99 : AUX Arr<17, Fin<2>>, aux_100 : AUX Arr<17, Fin<4>>, aux_101 : AUX Arr<17, Fin<20>>, aux_102 : AUX Fin<2>, aux_103 : AUX Fin<2>, aux_104 : AUX Arr<20, Fin<2>>, hillclimb_3_x_3_1 : AUX Arr<20, Fin<2>>, aux_105 : AUX Fin<2>, aux_106 : AUX Fin<20>, aux_107 : AUX Fin<2>, aux_108 : AUX Fin<2>, aux_109 : AUX Fin<2>, aux_110 : AUX Fin<20>, aux_111 : AUX Fin<1000>, aux_112 : AUX Fin<2>, aux_113 : AUX Fin<2>, aux_114 : AUX Arr<20, Fin<2>>, aux_115 : AUX Fin<1000>, aux_116 : AUX Fin<1000>, aux_117 : AUX Fin<2>, aux_118 : AUX Fin<2>, aux_119 : AUX Arr<20, Fin<2>>, aux_120 : AUX Fin<1000>, aux_121 : AUX Fin<2>, aux_122 : AUX Fin<2>, aux_123 : AUX Arr<17, Fin<2>>, aux_124 : AUX Arr<17, Fin<2>>, aux_125 : AUX Arr<17, Fin<4>>, aux_126 : AUX Arr<17, Fin<20>>, aux_127 : AUX Fin<1000>, aux_128 : AUX Fin<2>, aux_129 : AUX Fin<2>, aux_130 : AUX Arr<20, Fin<2>>, aux_131 : AUX Fin<1000>, aux_132 : AUX Fin<1000>, aux_133 : AUX Fin<2>, aux_134 : AUX Fin<2>, aux_135 : AUX Arr<20, Fin<2>>, aux_136 : AUX Fin<1000>, aux_137 : AUX Fin<2>, aux_138 : AUX Fin<2>, aux_139 : AUX Arr<17, Fin<2>>, aux_140 : AUX Arr<17, Fin<2>>, aux_141 : AUX Arr<17, Fin<4>>, aux_142 : AUX Arr<17, Fin<20>>, aux_143 : AUX Fin<2>, aux_144 : AUX Fin<2>, aux_145 : AUX Arr<20, Fin<2>>) { + hillclimb_3_x_0_1 *= Embed[() => default : Arr<20, Fin<2>>]; + hillclimb_3_x_0, hillclimb_3_x_0_1 *= SWAP; + call hillclimb_iter_U(hillclimb_3_x_0, hillclimb_3_x_1_1, aux_23, aux_24, aux_25, aux_26, aux_27, aux_28, aux_29, aux_30, aux_31, aux_32, aux_33, aux_34, aux_35, aux_36, aux_37, aux_38, aux_39, aux_40, aux_41, aux_42, aux_43, aux_44, aux_45, aux_46, aux_47, aux_48, aux_49, aux_50, aux_51, aux_52, aux_53, aux_54, aux_55, aux_56, aux_57, aux_58, aux_59, aux_60, aux_61, aux_62, aux_63); + hillclimb_3_x_1, hillclimb_3_x_1_1 *= SWAP; + call hillclimb_iter_U(hillclimb_3_x_1, hillclimb_3_x_2_1, aux_64, aux_65, aux_66, aux_67, aux_68, aux_69, aux_70, aux_71, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104); + hillclimb_3_x_2, hillclimb_3_x_2_1 *= SWAP; + call hillclimb_iter_U(hillclimb_3_x_2, hillclimb_3_x_3_1, aux_105, aux_106, aux_107, aux_108, aux_109, aux_110, aux_111, aux_112, aux_113, aux_114, aux_115, aux_116, aux_117, aux_118, aux_119, aux_120, aux_121, aux_122, aux_123, aux_124, aux_125, aux_126, aux_127, aux_128, aux_129, aux_130, aux_131, aux_132, aux_133, aux_134, aux_135, aux_136, aux_137, aux_138, aux_139, aux_140, aux_141, aux_142, aux_143, aux_144, aux_145); + hillclimb_3_x_3, hillclimb_3_x_3_1 *= SWAP; +} + +proc hillclimb_3(hillclimb_3_x_3 : Arr<20, Fin<2>>) { locals : (hillclimb_3_x_0 : Arr<20, Fin<2>>, hillclimb_3_x_1 : Arr<20, Fin<2>>, hillclimb_3_x_2 : Arr<20, Fin<2>>) } { + hillclimb_3_x_0 := default : Arr<20, Fin<2>>; + call hillclimb_iter(hillclimb_3_x_0, hillclimb_3_x_1); + call hillclimb_iter(hillclimb_3_x_1, hillclimb_3_x_2); + call hillclimb_iter(hillclimb_3_x_2, hillclimb_3_x_3); +} + + +// qubits: 1702 diff --git a/examples/matrix_search/depth3_NAND_formula.qpl b/examples/matrix_search/depth3_NAND_formula.qpl index 0bf47ba..a1776a9 100644 --- a/examples/matrix_search/depth3_NAND_formula.qpl +++ b/examples/matrix_search/depth3_NAND_formula.qpl @@ -14,7 +14,7 @@ proc NOR_0(i0 : Fin<20>, j0 : Fin<10>, k0 : Fin<10>, e' : Fin<2>) { locals : (e e' := not e; } -// UAny[Fin 10, 3.8011955e-32] +// UAny[Fin 10, 3.801194009254654e-32] uproc UAny(i1 : Fin<20>, j1 : Fin<10>, or_1_1 : OUT Fin<2>, s_result : OUT Fin<10>, aux : AUX Fin<2>, aux_1 : AUX Fin<2>, aux_2 : AUX Fin<2>, aux_3 : AUX Fin<2>, ctrl : AUX Arr<146, Fin<2>>, pred_out : AUX Arr<146, Fin<2>>, n_iter : AUX Arr<146, Fin<3>>, s_arg : AUX Arr<146, Fin<10>>) { for (#run_ix in 0 .. < 146) { n_iter[#run_ix] *= Distr[uniform : Fin<3>]; @@ -27,7 +27,7 @@ uproc UAny(i1 : Fin<20>, j1 : Fin<10>, or_1_1 : OUT Fin<2>, s_result : OUT Fin<1 ctrl[#run_ix], aux_3, pred_out[#run_ix] *= Toffoli; call-adj NOR_0_U(i1, j1, s_arg[#run_ix], aux_3, aux, aux_1, aux_2); s_arg[#run_ix] *= Adj-Distr[uniform : Fin<10>]; - s_arg[#run_ix] *= Refl0; + s_arg[#run_ix] *= PhaseOnZero(3.141592653589793); s_arg[#run_ix] *= Distr[uniform : Fin<10>]; n_iter[#run_ix], ctrl[#run_ix] *= Embed[(a) => (a <= #LIM)]; } @@ -59,14 +59,14 @@ uproc Grover[k](i1 : Fin<20>, j1 : Fin<10>, x : IN Fin<10>, or_1 : OUT Fin<2>, a repeat (#k) { call NOR_0_U(i1, j1, x, or_1, aux_4, aux_5, aux_6); x *= Adj-Distr[uniform : Fin<10>]; - x *= Refl0; + x *= PhaseOnZero(3.141592653589793); x *= Distr[uniform : Fin<10>]; } or_1 *= H; or_1 *= X; } -// QAny[3.8011955e-32] +// QAny[3.801194009254654e-32] proc QAny(i1 : Fin<20>, j1 : Fin<10>, or_1 : Fin<2>) { locals : (not_done : Fin<2>, Q_sum : Fin<30>, j : Fin<30>, j_lim : Fin<30>, s_result_1 : Fin<10>) } { repeat (66) { Q_sum := 0:Fin<30>; @@ -90,7 +90,7 @@ proc NOR_1(i1 : Fin<20>, j1 : Fin<10>, nor_1 : Fin<2>) { locals : (or_1 : Fin<2> nor_1 := not or_1; } -// UAny[Fin 10, 1.3387059e-13] +// UAny[Fin 10, 1.3387056295712027e-13] uproc UAny_1(i2 : Fin<20>, or_2_1 : OUT Fin<2>, s_result_2 : OUT Fin<10>, aux_7 : AUX Fin<2>, aux_8 : AUX Fin<2>, aux_9 : AUX Fin<10>, aux_10 : AUX Fin<2>, aux_11 : AUX Fin<2>, aux_12 : AUX Fin<2>, aux_13 : AUX Fin<2>, aux_14 : AUX Arr<146, Fin<2>>, aux_15 : AUX Arr<146, Fin<2>>, aux_16 : AUX Arr<146, Fin<3>>, aux_17 : AUX Arr<146, Fin<10>>, aux_18 : AUX Fin<10>, aux_19 : AUX Fin<2>, aux_20 : AUX Fin<2>, aux_21 : AUX Fin<2>, aux_22 : AUX Fin<2>, aux_23 : AUX Arr<146, Fin<2>>, aux_24 : AUX Arr<146, Fin<2>>, aux_25 : AUX Arr<146, Fin<3>>, aux_26 : AUX Arr<146, Fin<10>>, aux_27 : AUX Fin<2>, aux_28 : AUX Fin<2>, ctrl_1 : AUX Arr<60, Fin<2>>, pred_out_1 : AUX Arr<60, Fin<2>>, n_iter_1 : AUX Arr<60, Fin<3>>, s_arg_1 : AUX Arr<60, Fin<10>>) { for (#run_ix in 0 .. < 60) { n_iter_1[#run_ix] *= Distr[uniform : Fin<3>]; @@ -103,7 +103,7 @@ uproc UAny_1(i2 : Fin<20>, or_2_1 : OUT Fin<2>, s_result_2 : OUT Fin<10>, aux_7 ctrl_1[#run_ix], aux_28, pred_out_1[#run_ix] *= Toffoli; call-adj NOR_1_U(i2, s_arg_1[#run_ix], aux_28, aux_7, aux_8, aux_9, aux_10, aux_11, aux_12, aux_13, aux_14, aux_15, aux_16, aux_17, aux_18, aux_19, aux_20, aux_21, aux_22, aux_23, aux_24, aux_25, aux_26, aux_27); s_arg_1[#run_ix] *= Adj-Distr[uniform : Fin<10>]; - s_arg_1[#run_ix] *= Refl0; + s_arg_1[#run_ix] *= PhaseOnZero(3.141592653589793); s_arg_1[#run_ix] *= Distr[uniform : Fin<10>]; n_iter_1[#run_ix], ctrl_1[#run_ix] *= Embed[(a) => (a <= #LIM)]; } @@ -135,14 +135,14 @@ uproc Grover_1[k](i2 : Fin<20>, x_1 : IN Fin<10>, or_2 : OUT Fin<2>, aux_29 : AU repeat (#k) { call NOR_1_U(i2, x_1, or_2, aux_29, aux_30, aux_31, aux_32, aux_33, aux_34, aux_35, aux_36, aux_37, aux_38, aux_39, aux_40, aux_41, aux_42, aux_43, aux_44, aux_45, aux_46, aux_47, aux_48, aux_49); x_1 *= Adj-Distr[uniform : Fin<10>]; - x_1 *= Refl0; + x_1 *= PhaseOnZero(3.141592653589793); x_1 *= Distr[uniform : Fin<10>]; } or_2 *= H; or_2 *= X; } -// QAny[1.3387059e-13] +// QAny[1.3387056295712027e-13] proc QAny_1(i2 : Fin<20>, or_2 : Fin<2>) { locals : (not_done_1 : Fin<2>, Q_sum_1 : Fin<30>, j_1 : Fin<30>, j_lim_1 : Fin<30>, s_result_3 : Fin<10>) } { repeat (27) { Q_sum_1 := 0:Fin<30>; @@ -179,7 +179,7 @@ uproc UAny_2(or_3_1 : OUT Fin<2>, s_result_4 : OUT Fin<20>, aux_50 : AUX Fin<2>, ctrl_2[#run_ix], aux_107, pred_out_2[#run_ix] *= Toffoli; call-adj NOR_2_U(s_arg_2[#run_ix], aux_107, aux_50, aux_51, aux_52, aux_53, aux_54, aux_55, aux_56, aux_57, aux_58, aux_59, aux_60, aux_61, aux_62, aux_63, aux_64, aux_65, aux_66, aux_67, aux_68, aux_69, aux_70, aux_71, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106); s_arg_2[#run_ix] *= Adj-Distr[uniform : Fin<20>]; - s_arg_2[#run_ix] *= Refl0; + s_arg_2[#run_ix] *= PhaseOnZero(3.141592653589793); s_arg_2[#run_ix] *= Distr[uniform : Fin<20>]; n_iter_2[#run_ix], ctrl_2[#run_ix] *= Embed[(a) => (a <= #LIM)]; } @@ -209,7 +209,7 @@ uproc Grover_2[k](x_2 : IN Fin<20>, or_3 : OUT Fin<2>, aux_108 : AUX Fin<2>, aux repeat (#k) { call NOR_2_U(x_2, or_3, aux_108, aux_109, aux_110, aux_111, aux_112, aux_113, aux_114, aux_115, aux_116, aux_117, aux_118, aux_119, aux_120, aux_121, aux_122, aux_123, aux_124, aux_125, aux_126, aux_127, aux_128, aux_129, aux_130, aux_131, aux_132, aux_133, aux_134, aux_135, aux_136, aux_137, aux_138, aux_139, aux_140, aux_141, aux_142, aux_143, aux_144, aux_145, aux_146, aux_147, aux_148, aux_149, aux_150, aux_151, aux_152, aux_153, aux_154, aux_155, aux_156, aux_157, aux_158, aux_159, aux_160, aux_161, aux_162, aux_163, aux_164); x_2 *= Adj-Distr[uniform : Fin<20>]; - x_2 *= Refl0; + x_2 *= PhaseOnZero(3.141592653589793); x_2 *= Distr[uniform : Fin<20>]; } or_3 *= H; diff --git a/examples/matrix_search/matrix_search.qpl b/examples/matrix_search/matrix_search.qpl index a03cb47..732db9b 100644 --- a/examples/matrix_search/matrix_search.qpl +++ b/examples/matrix_search/matrix_search.qpl @@ -14,7 +14,7 @@ proc IsEntryZero(i0 : Fin<20>, j0 : Fin<10>, e' : Fin<2>) { locals : (e : Fin<2> e' := not e; } -// UAny[Fin 10, 2.6774118e-13] +// UAny[Fin 10, 2.6774112591424054e-13] uproc UAny(i : Fin<20>, hasZero_1 : OUT Fin<2>, s_result : OUT Fin<10>, aux : AUX Fin<2>, aux_1 : AUX Fin<2>, aux_2 : AUX Fin<2>, aux_3 : AUX Fin<2>, ctrl : AUX Arr<59, Fin<2>>, pred_out : AUX Arr<59, Fin<2>>, n_iter : AUX Arr<59, Fin<3>>, s_arg : AUX Arr<59, Fin<10>>) { for (#run_ix in 0 .. < 59) { n_iter[#run_ix] *= Distr[uniform : Fin<3>]; @@ -27,7 +27,7 @@ uproc UAny(i : Fin<20>, hasZero_1 : OUT Fin<2>, s_result : OUT Fin<10>, aux : AU ctrl[#run_ix], aux_3, pred_out[#run_ix] *= Toffoli; call-adj IsEntryZero_U(i, s_arg[#run_ix], aux_3, aux, aux_1, aux_2); s_arg[#run_ix] *= Adj-Distr[uniform : Fin<10>]; - s_arg[#run_ix] *= Refl0; + s_arg[#run_ix] *= PhaseOnZero(3.141592653589793); s_arg[#run_ix] *= Distr[uniform : Fin<10>]; n_iter[#run_ix], ctrl[#run_ix] *= Embed[(a) => (a <= #LIM)]; } @@ -59,14 +59,14 @@ uproc Grover[k](i : Fin<20>, x : IN Fin<10>, hasZero : OUT Fin<2>, aux_4 : AUX F repeat (#k) { call IsEntryZero_U(i, x, hasZero, aux_4, aux_5, aux_6); x *= Adj-Distr[uniform : Fin<10>]; - x *= Refl0; + x *= PhaseOnZero(3.141592653589793); x *= Distr[uniform : Fin<10>]; } hasZero *= H; hasZero *= X; } -// QAny[2.6774118e-13] +// QAny[2.6774112591424054e-13] proc QAny(i : Fin<20>, hasZero : Fin<2>) { locals : (not_done : Fin<2>, Q_sum : Fin<30>, j : Fin<30>, j_lim : Fin<30>, s_result_1 : Fin<10>) } { repeat (27) { Q_sum := 0:Fin<30>; @@ -103,7 +103,7 @@ uproc UAny_1(ok_1 : OUT Fin<2>, s_result_2 : OUT Fin<20>, aux_7 : AUX Fin<2>, au ctrl_1[#run_ix], aux_28, pred_out_1[#run_ix] *= Toffoli; call-adj IsRowAllOnes_U(s_arg_1[#run_ix], aux_28, aux_7, aux_8, aux_9, aux_10, aux_11, aux_12, aux_13, aux_14, aux_15, aux_16, aux_17, aux_18, aux_19, aux_20, aux_21, aux_22, aux_23, aux_24, aux_25, aux_26, aux_27); s_arg_1[#run_ix] *= Adj-Distr[uniform : Fin<20>]; - s_arg_1[#run_ix] *= Refl0; + s_arg_1[#run_ix] *= PhaseOnZero(3.141592653589793); s_arg_1[#run_ix] *= Distr[uniform : Fin<20>]; n_iter_1[#run_ix], ctrl_1[#run_ix] *= Embed[(a) => (a <= #LIM)]; } @@ -133,7 +133,7 @@ uproc Grover_1[k](x_1 : IN Fin<20>, ok : OUT Fin<2>, aux_29 : AUX Fin<2>, aux_30 repeat (#k) { call IsRowAllOnes_U(x_1, ok, aux_29, aux_30, aux_31, aux_32, aux_33, aux_34, aux_35, aux_36, aux_37, aux_38, aux_39, aux_40, aux_41, aux_42, aux_43, aux_44, aux_45, aux_46, aux_47, aux_48, aux_49); x_1 *= Adj-Distr[uniform : Fin<20>]; - x_1 *= Refl0; + x_1 *= PhaseOnZero(3.141592653589793); x_1 *= Distr[uniform : Fin<20>]; } ok *= H; diff --git a/examples/tree_generator/Makefile b/examples/tree_generator/Makefile new file mode 100644 index 0000000..38b7f74 --- /dev/null +++ b/examples/tree_generator/Makefile @@ -0,0 +1,13 @@ +PROJ_DEPS=../../src ../../tools ../../traq.cabal + +all: loop_example.qpl tree_generator_01_knapsack.qpl + +%.qpl: %.traq $(PROJ_DEPS) + cd ../../ && cabal run compile -- \ + -i examples/tree_generator/$< \ + -o examples/tree_generator/$@ \ + -p 0.001 \ + --arg W=1000 \ + --arg P=1000 \ + --arg N=10 \ + --arg K=3 diff --git a/examples/tree_generator/loop_example.qpl b/examples/tree_generator/loop_example.qpl new file mode 100644 index 0000000..c145346 --- /dev/null +++ b/examples/tree_generator/loop_example.qpl @@ -0,0 +1,34 @@ +uproc AddWeight_U(AddWeight_acc : IN Fin<1000>, AddWeight_i : IN Fin<10>, AddWeight_acc' : OUT Fin<1000>, AddWeight_one : AUX Fin<1000>, AddWeight_one_1 : AUX Fin<1000>, AddWeight_acc'_1 : AUX Fin<1000>) { + AddWeight_one_1 *= Embed[() => 1:Fin<1000>]; + AddWeight_one, AddWeight_one_1 *= SWAP; + AddWeight_acc, AddWeight_one, AddWeight_acc'_1 *= Embed[(AddWeight_acc, AddWeight_one) => (AddWeight_acc + AddWeight_one)]; + AddWeight_acc', AddWeight_acc'_1 *= SWAP; +} + +proc AddWeight(AddWeight_acc : Fin<1000>, AddWeight_i : Fin<10>, AddWeight_acc' : Fin<1000>) { locals : (AddWeight_one : Fin<1000>) } { + AddWeight_one := 1:Fin<1000>; + AddWeight_acc' := (AddWeight_acc + AddWeight_one); +} + +uproc main_U(main_tw : OUT Fin<1000>, main_acc : AUX Fin<1000>, main_acc_1 : AUX Fin<1000>, main_tw_1 : AUX Fin<1000>, aux : AUX Arr<10, Fin<1000>>, aux_1 : AUX Arr<10, Fin<1000>>, aux_2 : AUX Arr<10, Fin<1000>>, aux_3 : AUX Arr<10, Fin<10>>, aux_4 : AUX Arr<11, Fin<1000>>) { + main_acc_1 *= Embed[() => 0:Fin<1000>]; + main_acc, main_acc_1 *= SWAP; + main_acc, aux_4[0] *= COPY; + for (#ITER in 0 .. < 10) { + call AddWeight_U(aux_4[#ITER], aux_3[#ITER], aux_4[#ITER], aux[#ITER], aux_1[#ITER], aux_2[#ITER]); + } + aux_4[10], main_tw_1 *= COPY; + main_tw, main_tw_1 *= SWAP; +} + +proc main(main_tw : Fin<1000>) { locals : (main_acc : Fin<1000>, iter : Fin<10>) } { + main_acc := 0:Fin<1000>; + main_tw := main_acc; + for (#ITER_1 in 0 .. < 10) { + iter := #ITER_1; + call AddWeight(main_tw, iter, main_tw); + } +} + + +// qubits: 490 diff --git a/examples/tree_generator/tree_generator_01_knapsack.qpl b/examples/tree_generator/tree_generator_01_knapsack.qpl new file mode 100644 index 0000000..74c9b53 --- /dev/null +++ b/examples/tree_generator/tree_generator_01_knapsack.qpl @@ -0,0 +1,345 @@ +ext uproc Capacity_U(Fin<1000>); + +ext proc Capacity(Fin<1000>); + +ext uproc Profit_U(Fin<10>, Fin<1000>); + +ext proc Profit(Fin<10>, Fin<1000>); + +ext uproc Weight_U(Fin<10>, Fin<1000>); + +ext proc Weight(Fin<10>, Fin<1000>); + +uproc AddWeight_U(AddWeight_xs : IN Arr<10, Fin<2>>, AddWeight_cur_wt : IN Fin<1000>, AddWeight_i : IN Fin<10>, AddWeight_xs' : OUT Arr<10, Fin<2>>, AddWeight_new_wt : OUT Fin<1000>, AddWeight_xi : AUX Fin<2>, AddWeight_wi : AUX Fin<1000>, AddWeight_zero : AUX Fin<1000>, AddWeight_wi_pick : AUX Fin<1000>, AddWeight_xi_1 : AUX Fin<2>, AddWeight_wi_1 : AUX Fin<1000>, AddWeight_zero_1 : AUX Fin<1000>, AddWeight_wi_pick_1 : AUX Fin<1000>, AddWeight_new_wt_1 : AUX Fin<1000>, AddWeight_xs'_1 : AUX Arr<10, Fin<2>>) { + AddWeight_i, AddWeight_xs, AddWeight_xi_1 *= Embed[(AddWeight_i, AddWeight_xs) => AddWeight_xs[AddWeight_i]]; + AddWeight_xi, AddWeight_xi_1 *= SWAP; + call Weight_U(AddWeight_i, AddWeight_wi_1); + AddWeight_wi, AddWeight_wi_1 *= SWAP; + AddWeight_zero_1 *= Embed[() => 0:Fin<1000>]; + AddWeight_zero, AddWeight_zero_1 *= SWAP; + AddWeight_wi, AddWeight_xi, AddWeight_zero, AddWeight_wi_pick_1 *= Embed[(AddWeight_wi, AddWeight_xi, AddWeight_zero) => (ifte AddWeight_xi AddWeight_wi AddWeight_zero)]; + AddWeight_wi_pick, AddWeight_wi_pick_1 *= SWAP; + AddWeight_cur_wt, AddWeight_wi_pick, AddWeight_new_wt_1 *= Embed[(AddWeight_cur_wt, AddWeight_wi_pick) => (AddWeight_cur_wt + AddWeight_wi_pick)]; + AddWeight_new_wt, AddWeight_new_wt_1 *= SWAP; + AddWeight_xs, AddWeight_xs'_1 *= Embed[(AddWeight_xs) => AddWeight_xs]; + AddWeight_xs', AddWeight_xs'_1 *= SWAP; +} + +proc AddWeight(AddWeight_xs : Arr<10, Fin<2>>, AddWeight_cur_wt : Fin<1000>, AddWeight_i : Fin<10>, AddWeight_xs' : Arr<10, Fin<2>>, AddWeight_new_wt : Fin<1000>) { locals : (AddWeight_xi : Fin<2>, AddWeight_wi : Fin<1000>, AddWeight_zero : Fin<1000>, AddWeight_wi_pick : Fin<1000>) } { + AddWeight_xi := AddWeight_xs[AddWeight_i]; + call Weight(AddWeight_i, AddWeight_wi); + AddWeight_zero := 0:Fin<1000>; + AddWeight_wi_pick := (ifte AddWeight_xi AddWeight_wi AddWeight_zero); + AddWeight_new_wt := (AddWeight_cur_wt + AddWeight_wi_pick); + AddWeight_xs' := AddWeight_xs; +} + +uproc TotalWeight_U(TotalWeight_xs : IN Arr<10, Fin<2>>, TotalWeight_wt : OUT Fin<1000>, TotalWeight_zero : AUX Fin<1000>, TotalWeight_xs' : AUX Arr<10, Fin<2>>, TotalWeight_zero_1 : AUX Fin<1000>, TotalWeight_xs'_1 : AUX Arr<10, Fin<2>>, TotalWeight_wt_1 : AUX Fin<1000>, aux : AUX Arr<10, Fin<2>>, aux_1 : AUX Arr<10, Fin<1000>>, aux_2 : AUX Arr<10, Fin<1000>>, aux_3 : AUX Arr<10, Fin<1000>>, aux_4 : AUX Arr<10, Fin<2>>, aux_5 : AUX Arr<10, Fin<1000>>, aux_6 : AUX Arr<10, Fin<1000>>, aux_7 : AUX Arr<10, Fin<1000>>, aux_8 : AUX Arr<10, Fin<1000>>, aux_9 : AUX Arr<10, Arr<10, Fin<2>>>, aux_10 : AUX Arr<10, Fin<10>>, aux_11 : AUX Arr<11, Arr<10, Fin<2>>>, aux_12 : AUX Arr<11, Fin<1000>>) { + TotalWeight_zero_1 *= Embed[() => 0:Fin<1000>]; + TotalWeight_zero, TotalWeight_zero_1 *= SWAP; + TotalWeight_xs, aux_11[0] *= COPY; + TotalWeight_zero, aux_12[0] *= COPY; + for (#ITER in 0 .. < 10) { + call AddWeight_U(aux_11[#ITER], aux_12[#ITER], aux_10[#ITER], aux_11[#ITER], aux_12[#ITER], aux[#ITER], aux_1[#ITER], aux_2[#ITER], aux_3[#ITER], aux_4[#ITER], aux_5[#ITER], aux_6[#ITER], aux_7[#ITER], aux_8[#ITER], aux_9[#ITER]); + } + aux_11[10], TotalWeight_xs'_1 *= COPY; + aux_12[10], TotalWeight_wt_1 *= COPY; + TotalWeight_xs', TotalWeight_wt, TotalWeight_xs'_1, TotalWeight_wt_1 *= SWAP; +} + +proc TotalWeight(TotalWeight_xs : Arr<10, Fin<2>>, TotalWeight_wt : Fin<1000>) { locals : (TotalWeight_zero : Fin<1000>, TotalWeight_xs' : Arr<10, Fin<2>>, iter : Fin<10>) } { + TotalWeight_zero := 0:Fin<1000>; + TotalWeight_xs' := TotalWeight_xs; + TotalWeight_wt := TotalWeight_zero; + for (#ITER_1 in 0 .. < 10) { + iter := #ITER_1; + call AddWeight(TotalWeight_xs', TotalWeight_wt, iter, TotalWeight_xs', TotalWeight_wt); + } +} + +uproc AddProfit_U(AddProfit_xs : IN Arr<10, Fin<2>>, AddProfit_cur_pr : IN Fin<1000>, AddProfit_i : IN Fin<10>, AddProfit_xs' : OUT Arr<10, Fin<2>>, AddProfit_new_pr : OUT Fin<1000>, AddProfit_xi : AUX Fin<2>, AddProfit_pi : AUX Fin<1000>, AddProfit_zero : AUX Fin<1000>, AddProfit_pi_pick : AUX Fin<1000>, AddProfit_xi_1 : AUX Fin<2>, AddProfit_pi_1 : AUX Fin<1000>, AddProfit_zero_1 : AUX Fin<1000>, AddProfit_pi_pick_1 : AUX Fin<1000>, AddProfit_new_pr_1 : AUX Fin<1000>, AddProfit_xs'_1 : AUX Arr<10, Fin<2>>) { + AddProfit_i, AddProfit_xs, AddProfit_xi_1 *= Embed[(AddProfit_i, AddProfit_xs) => AddProfit_xs[AddProfit_i]]; + AddProfit_xi, AddProfit_xi_1 *= SWAP; + call Profit_U(AddProfit_i, AddProfit_pi_1); + AddProfit_pi, AddProfit_pi_1 *= SWAP; + AddProfit_zero_1 *= Embed[() => 0:Fin<1000>]; + AddProfit_zero, AddProfit_zero_1 *= SWAP; + AddProfit_pi, AddProfit_xi, AddProfit_zero, AddProfit_pi_pick_1 *= Embed[(AddProfit_pi, AddProfit_xi, AddProfit_zero) => (ifte AddProfit_xi AddProfit_pi AddProfit_zero)]; + AddProfit_pi_pick, AddProfit_pi_pick_1 *= SWAP; + AddProfit_cur_pr, AddProfit_pi_pick, AddProfit_new_pr_1 *= Embed[(AddProfit_cur_pr, AddProfit_pi_pick) => (AddProfit_cur_pr + AddProfit_pi_pick)]; + AddProfit_new_pr, AddProfit_new_pr_1 *= SWAP; + AddProfit_xs, AddProfit_xs'_1 *= Embed[(AddProfit_xs) => AddProfit_xs]; + AddProfit_xs', AddProfit_xs'_1 *= SWAP; +} + +proc AddProfit(AddProfit_xs : Arr<10, Fin<2>>, AddProfit_cur_pr : Fin<1000>, AddProfit_i : Fin<10>, AddProfit_xs' : Arr<10, Fin<2>>, AddProfit_new_pr : Fin<1000>) { locals : (AddProfit_xi : Fin<2>, AddProfit_pi : Fin<1000>, AddProfit_zero : Fin<1000>, AddProfit_pi_pick : Fin<1000>) } { + AddProfit_xi := AddProfit_xs[AddProfit_i]; + call Profit(AddProfit_i, AddProfit_pi); + AddProfit_zero := 0:Fin<1000>; + AddProfit_pi_pick := (ifte AddProfit_xi AddProfit_pi AddProfit_zero); + AddProfit_new_pr := (AddProfit_cur_pr + AddProfit_pi_pick); + AddProfit_xs' := AddProfit_xs; +} + +uproc TotalProfit_U(TotalProfit_xs : IN Arr<10, Fin<2>>, TotalProfit_pr : OUT Fin<1000>, TotalProfit_zero : AUX Fin<1000>, TotalProfit_xs' : AUX Arr<10, Fin<2>>, TotalProfit_zero_1 : AUX Fin<1000>, TotalProfit_xs'_1 : AUX Arr<10, Fin<2>>, TotalProfit_pr_1 : AUX Fin<1000>, aux_13 : AUX Arr<10, Fin<2>>, aux_14 : AUX Arr<10, Fin<1000>>, aux_15 : AUX Arr<10, Fin<1000>>, aux_16 : AUX Arr<10, Fin<1000>>, aux_17 : AUX Arr<10, Fin<2>>, aux_18 : AUX Arr<10, Fin<1000>>, aux_19 : AUX Arr<10, Fin<1000>>, aux_20 : AUX Arr<10, Fin<1000>>, aux_21 : AUX Arr<10, Fin<1000>>, aux_22 : AUX Arr<10, Arr<10, Fin<2>>>, aux_23 : AUX Arr<10, Fin<10>>, aux_24 : AUX Arr<11, Arr<10, Fin<2>>>, aux_25 : AUX Arr<11, Fin<1000>>) { + TotalProfit_zero_1 *= Embed[() => 0:Fin<1000>]; + TotalProfit_zero, TotalProfit_zero_1 *= SWAP; + TotalProfit_xs, aux_24[0] *= COPY; + TotalProfit_zero, aux_25[0] *= COPY; + for (#ITER_2 in 0 .. < 10) { + call AddProfit_U(aux_24[#ITER_2], aux_25[#ITER_2], aux_23[#ITER_2], aux_24[#ITER_2], aux_25[#ITER_2], aux_13[#ITER_2], aux_14[#ITER_2], aux_15[#ITER_2], aux_16[#ITER_2], aux_17[#ITER_2], aux_18[#ITER_2], aux_19[#ITER_2], aux_20[#ITER_2], aux_21[#ITER_2], aux_22[#ITER_2]); + } + aux_24[10], TotalProfit_xs'_1 *= COPY; + aux_25[10], TotalProfit_pr_1 *= COPY; + TotalProfit_xs', TotalProfit_pr, TotalProfit_xs'_1, TotalProfit_pr_1 *= SWAP; +} + +proc TotalProfit(TotalProfit_xs : Arr<10, Fin<2>>, TotalProfit_pr : Fin<1000>) { locals : (TotalProfit_zero : Fin<1000>, TotalProfit_xs' : Arr<10, Fin<2>>, iter_1 : Fin<10>) } { + TotalProfit_zero := 0:Fin<1000>; + TotalProfit_xs' := TotalProfit_xs; + TotalProfit_pr := TotalProfit_zero; + for (#ITER_3 in 0 .. < 10) { + iter_1 := #ITER_3; + call AddProfit(TotalProfit_xs', TotalProfit_pr, iter_1, TotalProfit_xs', TotalProfit_pr); + } +} + +uproc TreeGenLoopBody_U(TreeGenLoopBody_xs : IN Arr<10, Fin<2>>, TreeGenLoopBody_wt : IN Fin<1000>, TreeGenLoopBody_pr : IN Fin<1000>, TreeGenLoopBody_i : IN Fin<10>, TreeGenLoopBody_xs' : OUT Arr<10, Fin<2>>, TreeGenLoopBody_new_wt : OUT Fin<1000>, TreeGenLoopBody_new_pr : OUT Fin<1000>, TreeGenLoopBody_xi : AUX Fin<2>, TreeGenLoopBody_y : AUX Fin<2>, TreeGenLoopBody_try_pick : AUX Fin<2>, TreeGenLoopBody_wi : AUX Fin<1000>, TreeGenLoopBody_wt_picked : AUX Fin<1000>, TreeGenLoopBody_c : AUX Fin<1000>, TreeGenLoopBody_can_fit : AUX Fin<2>, TreeGenLoopBody_should_pick : AUX Fin<2>, TreeGenLoopBody_pi : AUX Fin<1000>, TreeGenLoopBody_pr_picked : AUX Fin<1000>, TreeGenLoopBody_xi_1 : AUX Fin<2>, TreeGenLoopBody_y_1 : AUX Fin<2>, TreeGenLoopBody_y_1_1 : AUX Fin<2>, TreeGenLoopBody_try_pick_1 : AUX Fin<2>, TreeGenLoopBody_wi_1 : AUX Fin<1000>, TreeGenLoopBody_wt_picked_1 : AUX Fin<1000>, TreeGenLoopBody_c_1 : AUX Fin<1000>, TreeGenLoopBody_can_fit_1 : AUX Fin<2>, TreeGenLoopBody_should_pick_1 : AUX Fin<2>, TreeGenLoopBody_xs'_1 : AUX Arr<10, Fin<2>>, TreeGenLoopBody_new_wt_1 : AUX Fin<1000>, TreeGenLoopBody_pi_1 : AUX Fin<1000>, TreeGenLoopBody_pr_picked_1 : AUX Fin<1000>, TreeGenLoopBody_new_pr_1 : AUX Fin<1000>) { + TreeGenLoopBody_i, TreeGenLoopBody_xs, TreeGenLoopBody_xi_1 *= Embed[(TreeGenLoopBody_i, TreeGenLoopBody_xs) => TreeGenLoopBody_xs[TreeGenLoopBody_i]]; + TreeGenLoopBody_xi, TreeGenLoopBody_xi_1 *= SWAP; + TreeGenLoopBody_y_1 *= Distr[bernoulli[0.2]]; + TreeGenLoopBody_y_1, TreeGenLoopBody_y_1_1 *= COPY; + TreeGenLoopBody_y, TreeGenLoopBody_y_1 *= SWAP; + TreeGenLoopBody_xi, TreeGenLoopBody_y, TreeGenLoopBody_try_pick_1 *= Embed[(TreeGenLoopBody_xi, TreeGenLoopBody_y) => (TreeGenLoopBody_xi ^ TreeGenLoopBody_y)]; + TreeGenLoopBody_try_pick, TreeGenLoopBody_try_pick_1 *= SWAP; + call Weight_U(TreeGenLoopBody_i, TreeGenLoopBody_wi_1); + TreeGenLoopBody_wi, TreeGenLoopBody_wi_1 *= SWAP; + TreeGenLoopBody_wi, TreeGenLoopBody_wt, TreeGenLoopBody_wt_picked_1 *= Embed[(TreeGenLoopBody_wi, TreeGenLoopBody_wt) => (TreeGenLoopBody_wt + TreeGenLoopBody_wi)]; + TreeGenLoopBody_wt_picked, TreeGenLoopBody_wt_picked_1 *= SWAP; + call Capacity_U(TreeGenLoopBody_c_1); + TreeGenLoopBody_c, TreeGenLoopBody_c_1 *= SWAP; + TreeGenLoopBody_c, TreeGenLoopBody_wt_picked, TreeGenLoopBody_can_fit_1 *= Embed[(TreeGenLoopBody_c, TreeGenLoopBody_wt_picked) => (TreeGenLoopBody_wt_picked <= TreeGenLoopBody_c)]; + TreeGenLoopBody_can_fit, TreeGenLoopBody_can_fit_1 *= SWAP; + TreeGenLoopBody_can_fit, TreeGenLoopBody_try_pick, TreeGenLoopBody_should_pick_1 *= Embed[(TreeGenLoopBody_can_fit, TreeGenLoopBody_try_pick) => (TreeGenLoopBody_try_pick && TreeGenLoopBody_can_fit)]; + TreeGenLoopBody_should_pick, TreeGenLoopBody_should_pick_1 *= SWAP; + TreeGenLoopBody_i, TreeGenLoopBody_should_pick, TreeGenLoopBody_xs, TreeGenLoopBody_xs'_1 *= Embed[(TreeGenLoopBody_i, TreeGenLoopBody_should_pick, TreeGenLoopBody_xs) => update TreeGenLoopBody_xs[TreeGenLoopBody_i] = TreeGenLoopBody_should_pick]; + TreeGenLoopBody_xs', TreeGenLoopBody_xs'_1 *= SWAP; + TreeGenLoopBody_should_pick, TreeGenLoopBody_wt, TreeGenLoopBody_wt_picked, TreeGenLoopBody_new_wt_1 *= Embed[(TreeGenLoopBody_should_pick, TreeGenLoopBody_wt, TreeGenLoopBody_wt_picked) => (ifte TreeGenLoopBody_should_pick TreeGenLoopBody_wt_picked TreeGenLoopBody_wt)]; + TreeGenLoopBody_new_wt, TreeGenLoopBody_new_wt_1 *= SWAP; + call Profit_U(TreeGenLoopBody_i, TreeGenLoopBody_pi_1); + TreeGenLoopBody_pi, TreeGenLoopBody_pi_1 *= SWAP; + TreeGenLoopBody_pi, TreeGenLoopBody_pr, TreeGenLoopBody_pr_picked_1 *= Embed[(TreeGenLoopBody_pi, TreeGenLoopBody_pr) => (TreeGenLoopBody_pr + TreeGenLoopBody_pi)]; + TreeGenLoopBody_pr_picked, TreeGenLoopBody_pr_picked_1 *= SWAP; + TreeGenLoopBody_pr, TreeGenLoopBody_pr_picked, TreeGenLoopBody_should_pick, TreeGenLoopBody_new_pr_1 *= Embed[(TreeGenLoopBody_pr, TreeGenLoopBody_pr_picked, TreeGenLoopBody_should_pick) => (ifte TreeGenLoopBody_should_pick TreeGenLoopBody_pr_picked TreeGenLoopBody_pr)]; + TreeGenLoopBody_new_pr, TreeGenLoopBody_new_pr_1 *= SWAP; +} + +proc TreeGenLoopBody(TreeGenLoopBody_xs : Arr<10, Fin<2>>, TreeGenLoopBody_wt : Fin<1000>, TreeGenLoopBody_pr : Fin<1000>, TreeGenLoopBody_i : Fin<10>, TreeGenLoopBody_xs' : Arr<10, Fin<2>>, TreeGenLoopBody_new_wt : Fin<1000>, TreeGenLoopBody_new_pr : Fin<1000>) { locals : (TreeGenLoopBody_xi : Fin<2>, TreeGenLoopBody_y : Fin<2>, TreeGenLoopBody_try_pick : Fin<2>, TreeGenLoopBody_wi : Fin<1000>, TreeGenLoopBody_wt_picked : Fin<1000>, TreeGenLoopBody_c : Fin<1000>, TreeGenLoopBody_can_fit : Fin<2>, TreeGenLoopBody_should_pick : Fin<2>, TreeGenLoopBody_pi : Fin<1000>, TreeGenLoopBody_pr_picked : Fin<1000>) } { + TreeGenLoopBody_xi := TreeGenLoopBody_xs[TreeGenLoopBody_i]; + TreeGenLoopBody_y :=$ bernoulli[0.2]; + TreeGenLoopBody_try_pick := (TreeGenLoopBody_xi ^ TreeGenLoopBody_y); + call Weight(TreeGenLoopBody_i, TreeGenLoopBody_wi); + TreeGenLoopBody_wt_picked := (TreeGenLoopBody_wt + TreeGenLoopBody_wi); + call Capacity(TreeGenLoopBody_c); + TreeGenLoopBody_can_fit := (TreeGenLoopBody_wt_picked <= TreeGenLoopBody_c); + TreeGenLoopBody_should_pick := (TreeGenLoopBody_try_pick && TreeGenLoopBody_can_fit); + TreeGenLoopBody_xs' := update TreeGenLoopBody_xs[TreeGenLoopBody_i] = TreeGenLoopBody_should_pick; + TreeGenLoopBody_new_wt := (ifte TreeGenLoopBody_should_pick TreeGenLoopBody_wt_picked TreeGenLoopBody_wt); + call Profit(TreeGenLoopBody_i, TreeGenLoopBody_pi); + TreeGenLoopBody_pr_picked := (TreeGenLoopBody_pr + TreeGenLoopBody_pi); + TreeGenLoopBody_new_pr := (ifte TreeGenLoopBody_should_pick TreeGenLoopBody_pr_picked TreeGenLoopBody_pr); +} + +uproc TreeGen_U(TreeGen_xs : IN Arr<10, Fin<2>>, TreeGen_pr : IN Fin<1000>, TreeGen_ok : OUT Fin<2>, TreeGen_xs' : OUT Arr<10, Fin<2>>, TreeGen_zero_wt : AUX Fin<1000>, TreeGen_zero_pr : AUX Fin<1000>, TreeGen_wt' : AUX Fin<1000>, TreeGen_pr' : AUX Fin<1000>, TreeGen_zero_wt_1 : AUX Fin<1000>, TreeGen_zero_pr_1 : AUX Fin<1000>, TreeGen_xs'_1 : AUX Arr<10, Fin<2>>, TreeGen_wt'_1 : AUX Fin<1000>, TreeGen_pr'_1 : AUX Fin<1000>, aux_26 : AUX Arr<10, Fin<2>>, aux_27 : AUX Arr<10, Fin<2>>, aux_28 : AUX Arr<10, Fin<2>>, aux_29 : AUX Arr<10, Fin<1000>>, aux_30 : AUX Arr<10, Fin<1000>>, aux_31 : AUX Arr<10, Fin<1000>>, aux_32 : AUX Arr<10, Fin<2>>, aux_33 : AUX Arr<10, Fin<2>>, aux_34 : AUX Arr<10, Fin<1000>>, aux_35 : AUX Arr<10, Fin<1000>>, aux_36 : AUX Arr<10, Fin<2>>, aux_37 : AUX Arr<10, Fin<2>>, aux_38 : AUX Arr<10, Fin<2>>, aux_39 : AUX Arr<10, Fin<2>>, aux_40 : AUX Arr<10, Fin<1000>>, aux_41 : AUX Arr<10, Fin<1000>>, aux_42 : AUX Arr<10, Fin<1000>>, aux_43 : AUX Arr<10, Fin<2>>, aux_44 : AUX Arr<10, Fin<2>>, aux_45 : AUX Arr<10, Arr<10, Fin<2>>>, aux_46 : AUX Arr<10, Fin<1000>>, aux_47 : AUX Arr<10, Fin<1000>>, aux_48 : AUX Arr<10, Fin<1000>>, aux_49 : AUX Arr<10, Fin<1000>>, aux_50 : AUX Arr<10, Fin<10>>, aux_51 : AUX Arr<11, Arr<10, Fin<2>>>, aux_52 : AUX Arr<11, Fin<1000>>, aux_53 : AUX Arr<11, Fin<1000>>, TreeGen_ok_1 : AUX Fin<2>) { + TreeGen_zero_wt_1 *= Embed[() => 0:Fin<1000>]; + TreeGen_zero_wt, TreeGen_zero_wt_1 *= SWAP; + TreeGen_zero_pr_1 *= Embed[() => 0:Fin<1000>]; + TreeGen_zero_pr, TreeGen_zero_pr_1 *= SWAP; + TreeGen_xs, aux_51[0] *= COPY; + TreeGen_zero_wt, aux_52[0] *= COPY; + TreeGen_zero_pr, aux_53[0] *= COPY; + for (#ITER_4 in 0 .. < 10) { + call TreeGenLoopBody_U(aux_51[#ITER_4], aux_52[#ITER_4], aux_53[#ITER_4], aux_50[#ITER_4], aux_51[#ITER_4], aux_52[#ITER_4], aux_53[#ITER_4], aux_26[#ITER_4], aux_27[#ITER_4], aux_28[#ITER_4], aux_29[#ITER_4], aux_30[#ITER_4], aux_31[#ITER_4], aux_32[#ITER_4], aux_33[#ITER_4], aux_34[#ITER_4], aux_35[#ITER_4], aux_36[#ITER_4], aux_37[#ITER_4], aux_38[#ITER_4], aux_39[#ITER_4], aux_40[#ITER_4], aux_41[#ITER_4], aux_42[#ITER_4], aux_43[#ITER_4], aux_44[#ITER_4], aux_45[#ITER_4], aux_46[#ITER_4], aux_47[#ITER_4], aux_48[#ITER_4], aux_49[#ITER_4]); + } + aux_51[10], TreeGen_xs'_1 *= COPY; + aux_52[10], TreeGen_wt'_1 *= COPY; + aux_53[10], TreeGen_pr'_1 *= COPY; + TreeGen_xs', TreeGen_wt', TreeGen_pr', TreeGen_xs'_1, TreeGen_wt'_1, TreeGen_pr'_1 *= SWAP; + TreeGen_pr, TreeGen_pr', TreeGen_ok_1 *= Embed[(TreeGen_pr, TreeGen_pr') => (TreeGen_pr < TreeGen_pr')]; + TreeGen_ok, TreeGen_ok_1 *= SWAP; +} + +proc TreeGen(TreeGen_xs : Arr<10, Fin<2>>, TreeGen_pr : Fin<1000>, TreeGen_ok : Fin<2>, TreeGen_xs' : Arr<10, Fin<2>>) { locals : (TreeGen_zero_wt : Fin<1000>, TreeGen_zero_pr : Fin<1000>, TreeGen_wt' : Fin<1000>, TreeGen_pr' : Fin<1000>, iter_2 : Fin<10>) } { + TreeGen_zero_wt := 0:Fin<1000>; + TreeGen_zero_pr := 0:Fin<1000>; + TreeGen_xs' := TreeGen_xs; + TreeGen_wt' := TreeGen_zero_wt; + TreeGen_pr' := TreeGen_zero_pr; + for (#ITER_5 in 0 .. < 10) { + iter_2 := #ITER_5; + call TreeGenLoopBody(TreeGen_xs', TreeGen_wt', TreeGen_pr', iter_2, TreeGen_xs', TreeGen_wt', TreeGen_pr'); + } + TreeGen_ok := (TreeGen_pr < TreeGen_pr'); +} + +uproc UAmplify(KnapsackLoopBody_xs : Arr<10, Fin<2>>, KnapsackLoopBody_pr : Fin<1000>, KnapsackLoopBody_ok_1 : OUT Fin<2>, KnapsackLoopBody_xs'_1 : OUT Arr<10, Fin<2>>, aux_72 : AUX Fin<1000>, aux_73 : AUX Fin<1000>, aux_74 : AUX Fin<1000>, aux_75 : AUX Fin<1000>, aux_76 : AUX Fin<1000>, aux_77 : AUX Fin<1000>, aux_78 : AUX Arr<10, Fin<2>>, aux_79 : AUX Fin<1000>, aux_80 : AUX Fin<1000>, aux_81 : AUX Arr<10, Fin<2>>, aux_82 : AUX Arr<10, Fin<2>>, aux_83 : AUX Arr<10, Fin<2>>, aux_84 : AUX Arr<10, Fin<1000>>, aux_85 : AUX Arr<10, Fin<1000>>, aux_86 : AUX Arr<10, Fin<1000>>, aux_87 : AUX Arr<10, Fin<2>>, aux_88 : AUX Arr<10, Fin<2>>, aux_89 : AUX Arr<10, Fin<1000>>, aux_90 : AUX Arr<10, Fin<1000>>, aux_91 : AUX Arr<10, Fin<2>>, aux_92 : AUX Arr<10, Fin<2>>, aux_93 : AUX Arr<10, Fin<2>>, aux_94 : AUX Arr<10, Fin<2>>, aux_95 : AUX Arr<10, Fin<1000>>, aux_96 : AUX Arr<10, Fin<1000>>, aux_97 : AUX Arr<10, Fin<1000>>, aux_98 : AUX Arr<10, Fin<2>>, aux_99 : AUX Arr<10, Fin<2>>, aux_100 : AUX Arr<10, Arr<10, Fin<2>>>, aux_101 : AUX Arr<10, Fin<1000>>, aux_102 : AUX Arr<10, Fin<1000>>, aux_103 : AUX Arr<10, Fin<1000>>, aux_104 : AUX Arr<10, Fin<1000>>, aux_105 : AUX Arr<10, Fin<10>>, aux_106 : AUX Arr<11, Arr<10, Fin<2>>>, aux_107 : AUX Arr<11, Fin<1000>>, aux_108 : AUX Arr<11, Fin<1000>>, aux_109 : AUX Fin<2>) { + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.011526049168105172); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.005737246821149794); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.0037960730984009164); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.0028167452554461367); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.0022220689602476425); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.001819622370843461); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.0015269182335347976); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.0013026936511006941); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.0011240063319286641); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.000977072800026606); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.0008531036527738527); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.0007462208791875804); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.0006523360773607303); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.000568509060304143); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.0004925625967566173); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.00042284114222675855); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.00035805416759807123); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.00029717106231432296); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.0002393484597632499); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.00018387845064632183); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.00013015048929663258); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(0.00007762234316309893); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(-0.000025796959484433774); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.000025796959484433774); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.00007762234316309893); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.00013015048929663258); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.00018387845064632183); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.0002393484597632499); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.00029717106231432296); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.00035805416759807123); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.00042284114222675855); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.0004925625967566173); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.000568509060304143); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.0006523360773607303); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.0007462208791875804); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.0008531036527738527); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.000977072800026606); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.0011240063319286641); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.0013026936511006941); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.0015269182335347976); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.001819622370843461); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.0022220689602476425); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.0028167452554461367); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.0037960730984009164); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1 *= Rz(0.005737246821149794); + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); + KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109 *= PhaseOnZero(-0.011526049168105172); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_72, aux_73, aux_74, aux_75, aux_76, aux_77, aux_78, aux_79, aux_80, aux_81, aux_82, aux_83, aux_84, aux_85, aux_86, aux_87, aux_88, aux_89, aux_90, aux_91, aux_92, aux_93, aux_94, aux_95, aux_96, aux_97, aux_98, aux_99, aux_100, aux_101, aux_102, aux_103, aux_104, aux_105, aux_106, aux_107, aux_108, aux_109); +} + +uproc KnapsackLoopBody_U(KnapsackLoopBody_xs : IN Arr<10, Fin<2>>, KnapsackLoopBody_i : IN Fin<3>, KnapsackLoopBody_xs_next : OUT Arr<10, Fin<2>>, KnapsackLoopBody_pr : AUX Fin<1000>, KnapsackLoopBody_ok : AUX Fin<2>, KnapsackLoopBody_xs' : AUX Arr<10, Fin<2>>, KnapsackLoopBody_pr_1 : AUX Fin<1000>, aux_54 : AUX Fin<1000>, aux_55 : AUX Arr<10, Fin<2>>, aux_56 : AUX Fin<1000>, aux_57 : AUX Arr<10, Fin<2>>, aux_58 : AUX Fin<1000>, aux_59 : AUX Arr<10, Fin<2>>, aux_60 : AUX Arr<10, Fin<1000>>, aux_61 : AUX Arr<10, Fin<1000>>, aux_62 : AUX Arr<10, Fin<1000>>, aux_63 : AUX Arr<10, Fin<2>>, aux_64 : AUX Arr<10, Fin<1000>>, aux_65 : AUX Arr<10, Fin<1000>>, aux_66 : AUX Arr<10, Fin<1000>>, aux_67 : AUX Arr<10, Fin<1000>>, aux_68 : AUX Arr<10, Arr<10, Fin<2>>>, aux_69 : AUX Arr<10, Fin<10>>, aux_70 : AUX Arr<11, Arr<10, Fin<2>>>, aux_71 : AUX Arr<11, Fin<1000>>, KnapsackLoopBody_ok_1 : AUX Fin<2>, KnapsackLoopBody_xs'_1 : AUX Arr<10, Fin<2>>, aux_72 : AUX Fin<1000>, aux_73 : AUX Fin<1000>, aux_74 : AUX Fin<1000>, aux_75 : AUX Fin<1000>, aux_76 : AUX Fin<1000>, aux_77 : AUX Fin<1000>, aux_78 : AUX Arr<10, Fin<2>>, aux_79 : AUX Fin<1000>, aux_80 : AUX Fin<1000>, aux_81 : AUX Arr<10, Fin<2>>, aux_82 : AUX Arr<10, Fin<2>>, aux_83 : AUX Arr<10, Fin<2>>, aux_84 : AUX Arr<10, Fin<1000>>, aux_85 : AUX Arr<10, Fin<1000>>, aux_86 : AUX Arr<10, Fin<1000>>, aux_87 : AUX Arr<10, Fin<2>>, aux_88 : AUX Arr<10, Fin<2>>, aux_89 : AUX Arr<10, Fin<1000>>, aux_90 : AUX Arr<10, Fin<1000>>, aux_91 : AUX Arr<10, Fin<2>>, aux_92 : AUX Arr<10, Fin<2>>, aux_93 : AUX Arr<10, Fin<2>>, aux_94 : AUX Arr<10, Fin<2>>, aux_95 : AUX Arr<10, Fin<1000>>, aux_96 : AUX Arr<10, Fin<1000>>, aux_97 : AUX Arr<10, Fin<1000>>, aux_98 : AUX Arr<10, Fin<2>>, aux_99 : AUX Arr<10, Fin<2>>, aux_100 : AUX Arr<10, Arr<10, Fin<2>>>, aux_101 : AUX Arr<10, Fin<1000>>, aux_102 : AUX Arr<10, Fin<1000>>, aux_103 : AUX Arr<10, Fin<1000>>, aux_104 : AUX Arr<10, Fin<1000>>, aux_105 : AUX Arr<10, Fin<10>>, aux_106 : AUX Arr<11, Arr<10, Fin<2>>>, aux_107 : AUX Arr<11, Fin<1000>>, aux_108 : AUX Arr<11, Fin<1000>>, aux_109 : AUX Fin<2>, aux_prim : AUX Fin<1000>, aux_prim_1 : AUX Fin<1000>, aux_prim_2 : AUX Fin<1000>, aux_prim_3 : AUX Fin<1000>, aux_prim_4 : AUX Fin<1000>, aux_prim_5 : AUX Fin<1000>, aux_prim_6 : AUX Arr<10, Fin<2>>, aux_prim_7 : AUX Fin<1000>, aux_prim_8 : AUX Fin<1000>, aux_prim_9 : AUX Arr<10, Fin<2>>, aux_prim_10 : AUX Arr<10, Fin<2>>, aux_prim_11 : AUX Arr<10, Fin<2>>, aux_prim_12 : AUX Arr<10, Fin<1000>>, aux_prim_13 : AUX Arr<10, Fin<1000>>, aux_prim_14 : AUX Arr<10, Fin<1000>>, aux_prim_15 : AUX Arr<10, Fin<2>>, aux_prim_16 : AUX Arr<10, Fin<2>>, aux_prim_17 : AUX Arr<10, Fin<1000>>, aux_prim_18 : AUX Arr<10, Fin<1000>>, aux_prim_19 : AUX Arr<10, Fin<2>>, aux_prim_20 : AUX Arr<10, Fin<2>>, aux_prim_21 : AUX Arr<10, Fin<2>>, aux_prim_22 : AUX Arr<10, Fin<2>>, aux_prim_23 : AUX Arr<10, Fin<1000>>, aux_prim_24 : AUX Arr<10, Fin<1000>>, aux_prim_25 : AUX Arr<10, Fin<1000>>, aux_prim_26 : AUX Arr<10, Fin<2>>, aux_prim_27 : AUX Arr<10, Fin<2>>, aux_prim_28 : AUX Arr<10, Arr<10, Fin<2>>>, aux_prim_29 : AUX Arr<10, Fin<1000>>, aux_prim_30 : AUX Arr<10, Fin<1000>>, aux_prim_31 : AUX Arr<10, Fin<1000>>, aux_prim_32 : AUX Arr<10, Fin<1000>>, aux_prim_33 : AUX Arr<10, Fin<10>>, aux_prim_34 : AUX Arr<11, Arr<10, Fin<2>>>, aux_prim_35 : AUX Arr<11, Fin<1000>>, aux_prim_36 : AUX Arr<11, Fin<1000>>, aux_prim_37 : AUX Fin<2>, KnapsackLoopBody_xs_next_1 : AUX Arr<10, Fin<2>>) { + call TotalProfit_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr_1, aux_54, aux_55, aux_56, aux_57, aux_58, aux_59, aux_60, aux_61, aux_62, aux_63, aux_64, aux_65, aux_66, aux_67, aux_68, aux_69, aux_70, aux_71); + KnapsackLoopBody_pr, KnapsackLoopBody_pr_1 *= SWAP; + call UAmplify(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1, aux_prim, aux_prim_1, aux_prim_2, aux_prim_3, aux_prim_4, aux_prim_5, aux_prim_6, aux_prim_7, aux_prim_8, aux_prim_9, aux_prim_10, aux_prim_11, aux_prim_12, aux_prim_13, aux_prim_14, aux_prim_15, aux_prim_16, aux_prim_17, aux_prim_18, aux_prim_19, aux_prim_20, aux_prim_21, aux_prim_22, aux_prim_23, aux_prim_24, aux_prim_25, aux_prim_26, aux_prim_27, aux_prim_28, aux_prim_29, aux_prim_30, aux_prim_31, aux_prim_32, aux_prim_33, aux_prim_34, aux_prim_35, aux_prim_36, aux_prim_37); + KnapsackLoopBody_ok, KnapsackLoopBody_xs', KnapsackLoopBody_ok_1, KnapsackLoopBody_xs'_1 *= SWAP; + KnapsackLoopBody_ok, KnapsackLoopBody_xs, KnapsackLoopBody_xs', KnapsackLoopBody_xs_next_1 *= Embed[(KnapsackLoopBody_ok, KnapsackLoopBody_xs, KnapsackLoopBody_xs') => (ifte KnapsackLoopBody_ok KnapsackLoopBody_xs' KnapsackLoopBody_xs)]; + KnapsackLoopBody_xs_next, KnapsackLoopBody_xs_next_1 *= SWAP; +} + +uproc Grover[k](KnapsackLoopBody_xs : Arr<10, Fin<2>>, KnapsackLoopBody_pr : Fin<1000>, KnapsackLoopBody_ok : OUT Fin<2>, KnapsackLoopBody_xs' : OUT Arr<10, Fin<2>>, aux_110 : AUX Fin<1000>, aux_111 : AUX Fin<1000>, aux_112 : AUX Fin<1000>, aux_113 : AUX Fin<1000>, aux_114 : AUX Fin<1000>, aux_115 : AUX Fin<1000>, aux_116 : AUX Arr<10, Fin<2>>, aux_117 : AUX Fin<1000>, aux_118 : AUX Fin<1000>, aux_119 : AUX Arr<10, Fin<2>>, aux_120 : AUX Arr<10, Fin<2>>, aux_121 : AUX Arr<10, Fin<2>>, aux_122 : AUX Arr<10, Fin<1000>>, aux_123 : AUX Arr<10, Fin<1000>>, aux_124 : AUX Arr<10, Fin<1000>>, aux_125 : AUX Arr<10, Fin<2>>, aux_126 : AUX Arr<10, Fin<2>>, aux_127 : AUX Arr<10, Fin<1000>>, aux_128 : AUX Arr<10, Fin<1000>>, aux_129 : AUX Arr<10, Fin<2>>, aux_130 : AUX Arr<10, Fin<2>>, aux_131 : AUX Arr<10, Fin<2>>, aux_132 : AUX Arr<10, Fin<2>>, aux_133 : AUX Arr<10, Fin<1000>>, aux_134 : AUX Arr<10, Fin<1000>>, aux_135 : AUX Arr<10, Fin<1000>>, aux_136 : AUX Arr<10, Fin<2>>, aux_137 : AUX Arr<10, Fin<2>>, aux_138 : AUX Arr<10, Arr<10, Fin<2>>>, aux_139 : AUX Arr<10, Fin<1000>>, aux_140 : AUX Arr<10, Fin<1000>>, aux_141 : AUX Arr<10, Fin<1000>>, aux_142 : AUX Arr<10, Fin<1000>>, aux_143 : AUX Arr<10, Fin<10>>, aux_144 : AUX Arr<11, Arr<10, Fin<2>>>, aux_145 : AUX Arr<11, Fin<1000>>, aux_146 : AUX Arr<11, Fin<1000>>, aux_147 : AUX Fin<2>) { + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok, KnapsackLoopBody_xs', aux_110, aux_111, aux_112, aux_113, aux_114, aux_115, aux_116, aux_117, aux_118, aux_119, aux_120, aux_121, aux_122, aux_123, aux_124, aux_125, aux_126, aux_127, aux_128, aux_129, aux_130, aux_131, aux_132, aux_133, aux_134, aux_135, aux_136, aux_137, aux_138, aux_139, aux_140, aux_141, aux_142, aux_143, aux_144, aux_145, aux_146, aux_147); + repeat (#k) { + KnapsackLoopBody_ok *= Z; + call-adj TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok, KnapsackLoopBody_xs', aux_110, aux_111, aux_112, aux_113, aux_114, aux_115, aux_116, aux_117, aux_118, aux_119, aux_120, aux_121, aux_122, aux_123, aux_124, aux_125, aux_126, aux_127, aux_128, aux_129, aux_130, aux_131, aux_132, aux_133, aux_134, aux_135, aux_136, aux_137, aux_138, aux_139, aux_140, aux_141, aux_142, aux_143, aux_144, aux_145, aux_146, aux_147); + KnapsackLoopBody_ok, KnapsackLoopBody_xs', aux_110, aux_111, aux_112, aux_113, aux_114, aux_115, aux_116, aux_117, aux_118, aux_119, aux_120, aux_121, aux_122, aux_123, aux_124, aux_125, aux_126, aux_127, aux_128, aux_129, aux_130, aux_131, aux_132, aux_133, aux_134, aux_135, aux_136, aux_137, aux_138, aux_139, aux_140, aux_141, aux_142, aux_143, aux_144, aux_145, aux_146, aux_147 *= PhaseOnZero(3.141592653589793); + call TreeGen_U(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok, KnapsackLoopBody_xs', aux_110, aux_111, aux_112, aux_113, aux_114, aux_115, aux_116, aux_117, aux_118, aux_119, aux_120, aux_121, aux_122, aux_123, aux_124, aux_125, aux_126, aux_127, aux_128, aux_129, aux_130, aux_131, aux_132, aux_133, aux_134, aux_135, aux_136, aux_137, aux_138, aux_139, aux_140, aux_141, aux_142, aux_143, aux_144, aux_145, aux_146, aux_147); + } +} + +proc QAmplify(KnapsackLoopBody_xs : Arr<10, Fin<2>>, KnapsackLoopBody_pr : Fin<1000>, KnapsackLoopBody_ok : Fin<2>, KnapsackLoopBody_xs' : Arr<10, Fin<2>>) { locals : (not_done : Fin<2>, Q_sum : Fin<92>, j : Fin<92>, j_lim : Fin<92>) } { + not_done := 0:Fin<2>; + repeat (8) { + Q_sum := 0:Fin<92>; + for (j_lim in [1:Fin<92>, 1:Fin<92>, 1:Fin<92>, 2:Fin<92>, 2:Fin<92>, 2:Fin<92>, 3:Fin<92>, 4:Fin<92>, 5:Fin<92>, 6:Fin<92>, 7:Fin<92>, 8:Fin<92>, 10:Fin<92>, 10:Fin<92>, 10:Fin<92>, 10:Fin<92>, 10:Fin<92>]) { + j :=$ [1 .. j_lim]; + Q_sum := (Q_sum + j); + not_done := (not_done && (Q_sum <= j_lim)); + if (not_done) { + meas Grover[j](KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok, KnapsackLoopBody_xs'); + not_done := (not_done && not KnapsackLoopBody_ok); + } else { + skip; + } + } + } +} + +proc KnapsackLoopBody(KnapsackLoopBody_xs : Arr<10, Fin<2>>, KnapsackLoopBody_i : Fin<3>, KnapsackLoopBody_xs_next : Arr<10, Fin<2>>) { locals : (KnapsackLoopBody_pr : Fin<1000>, KnapsackLoopBody_ok : Fin<2>, KnapsackLoopBody_xs' : Arr<10, Fin<2>>) } { + call TotalProfit(KnapsackLoopBody_xs, KnapsackLoopBody_pr); + call QAmplify(KnapsackLoopBody_xs, KnapsackLoopBody_pr, KnapsackLoopBody_ok, KnapsackLoopBody_xs'); + KnapsackLoopBody_xs_next := (ifte KnapsackLoopBody_ok KnapsackLoopBody_xs' KnapsackLoopBody_xs); +} + +uproc Knapsack_U(Knapsack_xs' : OUT Arr<10, Fin<2>>, Knapsack_xs : AUX Arr<10, Fin<2>>, Knapsack_xs_1 : AUX Arr<10, Fin<2>>, Knapsack_xs'_1 : AUX Arr<10, Fin<2>>, aux_110 : AUX Arr<3, Fin<1000>>, aux_111 : AUX Arr<3, Fin<2>>, aux_112 : AUX Arr<3, Arr<10, Fin<2>>>, aux_113 : AUX Arr<3, Fin<1000>>, aux_114 : AUX Arr<3, Fin<1000>>, aux_115 : AUX Arr<3, Arr<10, Fin<2>>>, aux_116 : AUX Arr<3, Fin<1000>>, aux_117 : AUX Arr<3, Arr<10, Fin<2>>>, aux_118 : AUX Arr<3, Fin<1000>>, aux_119 : AUX Arr<3, Arr<10, Fin<2>>>, aux_120 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_121 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_122 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_123 : AUX Arr<3, Arr<10, Fin<2>>>, aux_124 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_125 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_126 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_127 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_128 : AUX Arr<3, Arr<10, Arr<10, Fin<2>>>>, aux_129 : AUX Arr<3, Arr<10, Fin<10>>>, aux_130 : AUX Arr<3, Arr<11, Arr<10, Fin<2>>>>, aux_131 : AUX Arr<3, Arr<11, Fin<1000>>>, aux_132 : AUX Arr<3, Fin<2>>, aux_133 : AUX Arr<3, Arr<10, Fin<2>>>, aux_134 : AUX Arr<3, Fin<1000>>, aux_135 : AUX Arr<3, Fin<1000>>, aux_136 : AUX Arr<3, Fin<1000>>, aux_137 : AUX Arr<3, Fin<1000>>, aux_138 : AUX Arr<3, Fin<1000>>, aux_139 : AUX Arr<3, Fin<1000>>, aux_140 : AUX Arr<3, Arr<10, Fin<2>>>, aux_141 : AUX Arr<3, Fin<1000>>, aux_142 : AUX Arr<3, Fin<1000>>, aux_143 : AUX Arr<3, Arr<10, Fin<2>>>, aux_144 : AUX Arr<3, Arr<10, Fin<2>>>, aux_145 : AUX Arr<3, Arr<10, Fin<2>>>, aux_146 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_147 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_148 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_149 : AUX Arr<3, Arr<10, Fin<2>>>, aux_150 : AUX Arr<3, Arr<10, Fin<2>>>, aux_151 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_152 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_153 : AUX Arr<3, Arr<10, Fin<2>>>, aux_154 : AUX Arr<3, Arr<10, Fin<2>>>, aux_155 : AUX Arr<3, Arr<10, Fin<2>>>, aux_156 : AUX Arr<3, Arr<10, Fin<2>>>, aux_157 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_158 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_159 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_160 : AUX Arr<3, Arr<10, Fin<2>>>, aux_161 : AUX Arr<3, Arr<10, Fin<2>>>, aux_162 : AUX Arr<3, Arr<10, Arr<10, Fin<2>>>>, aux_163 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_164 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_165 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_166 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_167 : AUX Arr<3, Arr<10, Fin<10>>>, aux_168 : AUX Arr<3, Arr<11, Arr<10, Fin<2>>>>, aux_169 : AUX Arr<3, Arr<11, Fin<1000>>>, aux_170 : AUX Arr<3, Arr<11, Fin<1000>>>, aux_171 : AUX Arr<3, Fin<2>>, aux_172 : AUX Arr<3, Fin<1000>>, aux_173 : AUX Arr<3, Fin<1000>>, aux_174 : AUX Arr<3, Fin<1000>>, aux_175 : AUX Arr<3, Fin<1000>>, aux_176 : AUX Arr<3, Fin<1000>>, aux_177 : AUX Arr<3, Fin<1000>>, aux_178 : AUX Arr<3, Arr<10, Fin<2>>>, aux_179 : AUX Arr<3, Fin<1000>>, aux_180 : AUX Arr<3, Fin<1000>>, aux_181 : AUX Arr<3, Arr<10, Fin<2>>>, aux_182 : AUX Arr<3, Arr<10, Fin<2>>>, aux_183 : AUX Arr<3, Arr<10, Fin<2>>>, aux_184 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_185 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_186 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_187 : AUX Arr<3, Arr<10, Fin<2>>>, aux_188 : AUX Arr<3, Arr<10, Fin<2>>>, aux_189 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_190 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_191 : AUX Arr<3, Arr<10, Fin<2>>>, aux_192 : AUX Arr<3, Arr<10, Fin<2>>>, aux_193 : AUX Arr<3, Arr<10, Fin<2>>>, aux_194 : AUX Arr<3, Arr<10, Fin<2>>>, aux_195 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_196 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_197 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_198 : AUX Arr<3, Arr<10, Fin<2>>>, aux_199 : AUX Arr<3, Arr<10, Fin<2>>>, aux_200 : AUX Arr<3, Arr<10, Arr<10, Fin<2>>>>, aux_201 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_202 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_203 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_204 : AUX Arr<3, Arr<10, Fin<1000>>>, aux_205 : AUX Arr<3, Arr<10, Fin<10>>>, aux_206 : AUX Arr<3, Arr<11, Arr<10, Fin<2>>>>, aux_207 : AUX Arr<3, Arr<11, Fin<1000>>>, aux_208 : AUX Arr<3, Arr<11, Fin<1000>>>, aux_209 : AUX Arr<3, Fin<2>>, aux_210 : AUX Arr<3, Arr<10, Fin<2>>>, aux_211 : AUX Arr<3, Fin<3>>, aux_212 : AUX Arr<4, Arr<10, Fin<2>>>) { + Knapsack_xs_1 *= Embed[() => default : Arr<10, Fin<2>>]; + Knapsack_xs, Knapsack_xs_1 *= SWAP; + Knapsack_xs, aux_212[0] *= COPY; + for (#ITER_6 in 0 .. < 3) { + call KnapsackLoopBody_U(aux_212[#ITER_6], aux_211[#ITER_6], aux_212[#ITER_6], aux_110[#ITER_6], aux_111[#ITER_6], aux_112[#ITER_6], aux_113[#ITER_6], aux_114[#ITER_6], aux_115[#ITER_6], aux_116[#ITER_6], aux_117[#ITER_6], aux_118[#ITER_6], aux_119[#ITER_6], aux_120[#ITER_6], aux_121[#ITER_6], aux_122[#ITER_6], aux_123[#ITER_6], aux_124[#ITER_6], aux_125[#ITER_6], aux_126[#ITER_6], aux_127[#ITER_6], aux_128[#ITER_6], aux_129[#ITER_6], aux_130[#ITER_6], aux_131[#ITER_6], aux_132[#ITER_6], aux_133[#ITER_6], aux_134[#ITER_6], aux_135[#ITER_6], aux_136[#ITER_6], aux_137[#ITER_6], aux_138[#ITER_6], aux_139[#ITER_6], aux_140[#ITER_6], aux_141[#ITER_6], aux_142[#ITER_6], aux_143[#ITER_6], aux_144[#ITER_6], aux_145[#ITER_6], aux_146[#ITER_6], aux_147[#ITER_6], aux_148[#ITER_6], aux_149[#ITER_6], aux_150[#ITER_6], aux_151[#ITER_6], aux_152[#ITER_6], aux_153[#ITER_6], aux_154[#ITER_6], aux_155[#ITER_6], aux_156[#ITER_6], aux_157[#ITER_6], aux_158[#ITER_6], aux_159[#ITER_6], aux_160[#ITER_6], aux_161[#ITER_6], aux_162[#ITER_6], aux_163[#ITER_6], aux_164[#ITER_6], aux_165[#ITER_6], aux_166[#ITER_6], aux_167[#ITER_6], aux_168[#ITER_6], aux_169[#ITER_6], aux_170[#ITER_6], aux_171[#ITER_6], aux_172[#ITER_6], aux_173[#ITER_6], aux_174[#ITER_6], aux_175[#ITER_6], aux_176[#ITER_6], aux_177[#ITER_6], aux_178[#ITER_6], aux_179[#ITER_6], aux_180[#ITER_6], aux_181[#ITER_6], aux_182[#ITER_6], aux_183[#ITER_6], aux_184[#ITER_6], aux_185[#ITER_6], aux_186[#ITER_6], aux_187[#ITER_6], aux_188[#ITER_6], aux_189[#ITER_6], aux_190[#ITER_6], aux_191[#ITER_6], aux_192[#ITER_6], aux_193[#ITER_6], aux_194[#ITER_6], aux_195[#ITER_6], aux_196[#ITER_6], aux_197[#ITER_6], aux_198[#ITER_6], aux_199[#ITER_6], aux_200[#ITER_6], aux_201[#ITER_6], aux_202[#ITER_6], aux_203[#ITER_6], aux_204[#ITER_6], aux_205[#ITER_6], aux_206[#ITER_6], aux_207[#ITER_6], aux_208[#ITER_6], aux_209[#ITER_6], aux_210[#ITER_6]); + } + aux_212[3], Knapsack_xs'_1 *= COPY; + Knapsack_xs', Knapsack_xs'_1 *= SWAP; +} + +proc Knapsack(Knapsack_xs' : Arr<10, Fin<2>>) { locals : (Knapsack_xs : Arr<10, Fin<2>>, iter_3 : Fin<3>) } { + Knapsack_xs := default : Arr<10, Fin<2>>; + Knapsack_xs' := Knapsack_xs; + for (#ITER_7 in 0 .. < 3) { + iter_3 := #ITER_7; + call KnapsackLoopBody(Knapsack_xs', iter_3, Knapsack_xs'); + } +} + + +// qubits: 14858 diff --git a/src/Traq/Analysis/Cost/Quantum.hs b/src/Traq/Analysis/Cost/Quantum.hs index 449df6c..ea576ce 100644 --- a/src/Traq/Analysis/Cost/Quantum.hs +++ b/src/Traq/Analysis/Cost/Quantum.hs @@ -155,34 +155,25 @@ instance ExpCostQ1 Expr where return (distr >>= run_loop_body i, iter_cost) return $ Alg.sum cs --- | TODO unify this as a class instance, after unifying evaluation -expCostQStmt :: - forall ext size prec cost m. - ( m ~ CostAnalysisMonad ext - , ExpCostQ ext size prec - , CostModelReqs size prec cost - ) => - Stmt ext -> - ProgramState size -> - m cost -expCostQStmt ExprS{expr} sigma = expCostQ1 expr sigma -expCostQStmt IfThenElseS{cond, s_true, s_false} sigma = do - let b = - sigma - ^?! Ctx.at cond - . non' (error $ "cannot find variable" ++ cond) - . to valueToBool - expCostQStmt (if b then s_true else s_false) sigma -expCostQStmt (SeqS ss) sigma = do - env <- view _evaluationEnv - - let stepS s sigma_s = eval1 s sigma_s & (runReaderT ?? env) - - (_, cs) <- forAccumM (pure sigma) ss $ \distr s -> do - c <- Prob.expectationA (expCostQStmt s) distr - return (distr >>= stepS s, c) - - return $ Alg.sum cs +instance ExpCostQ1 Stmt where + expCostQ1 ExprS{expr} sigma = expCostQ1 expr sigma + expCostQ1 IfThenElseS{cond, s_true, s_false} sigma = do + let b = + sigma + ^?! Ctx.at cond + . non' (error $ "cannot find variable" ++ cond) + . to valueToBool + expCostQ1 (if b then s_true else s_false) sigma + expCostQ1 (SeqS ss) sigma = do + env <- view _evaluationEnv + + let stepS s sigma_s = eval1 s sigma_s & (runReaderT ?? env) + + (_, cs) <- forAccumM (pure sigma) ss $ \distr s -> do + c <- Prob.expectationA (expCostQ1 s) distr + return (distr >>= stepS s, c) + + return $ Alg.sum cs instance ExpCostQ1 NamedFunDef where -- query an external function @@ -198,7 +189,7 @@ instance ExpCostQ1 NamedFunDef where NamedFunDef { fun_def = FunDef{mbody = Just FunBody{param_names, body_stmt}} } - args = expCostQStmt body_stmt sigma + args = expCostQ1 body_stmt sigma where -- bind args to the parameter names sigma = Ctx.fromList $ zip param_names args diff --git a/src/Traq/CQPL/Syntax.hs b/src/Traq/CQPL/Syntax.hs index 94f23bd..2aa74e4 100644 --- a/src/Traq/CQPL/Syntax.hs +++ b/src/Traq/CQPL/Syntax.hs @@ -85,23 +85,29 @@ data BasicGate | CNOT | XGate | HGate + | ZGate | COPY | SWAP + | Rz Double + | PhaseOnZero Double deriving (Eq, Show, Read) instance PP.ToCodeString BasicGate where build XGate = PP.putWord "X" build HGate = PP.putWord "H" + build ZGate = PP.putWord "Z" + build (Rz theta) = PP.putWord $ printf "Rz(%f)" theta + build (PhaseOnZero theta) = PP.putWord $ printf "PhaseOnZero(%f)" theta build g = PP.putWord $ show g -isSelfAdjoint :: BasicGate -> Bool -isSelfAdjoint _ = True +instance HasAdjoint BasicGate where + adjoint (Rz theta) = Rz (-theta) + adjoint (PhaseOnZero theta) = PhaseOnZero (-theta) + adjoint g = g -- | Unitary operators in CQPL data Unitary sizeT = BasicGateU BasicGate - | -- | reflect about |0>_T - Refl0 | RevEmbedU [Ident] (P.BasicExpr sizeT) | DistrU (P.DistrExpr sizeT) | Controlled (Unitary sizeT) @@ -118,13 +124,11 @@ instance (Show sizeT) => PP.ToCodeString (Unitary sizeT) where build (DistrU mu) = do e_s <- PP.fromBuild mu PP.putWord $ printf "Distr[%s]" e_s - build Refl0 = PP.putWord $ printf "Refl0" build (Controlled u) = PP.putWord . ("Ctrl-" <>) =<< PP.fromBuild u build (Adjoint u) = PP.putWord . ("Adj-" <>) =<< PP.fromBuild u instance HasAdjoint (Unitary sizeT) where - adjoint u@(BasicGateU g) | isSelfAdjoint g = u - adjoint Refl0 = Refl0 + adjoint (BasicGateU g) = BasicGateU (adjoint g) adjoint u@(RevEmbedU _ _) = u adjoint (Controlled u) = Controlled (adjoint u) adjoint (Adjoint u) = u @@ -285,7 +289,7 @@ instance (Show sizeT) => PP.ToCodeString (Stmt sizeT) where build ForInRangeS{iter_meta_var, iter_lim, loop_body} = do n <- PP.fromBuild iter_lim PP.bracedBlockWith - (printf "for (%s in 0 .. < %s)" iter_meta_var n) + (printf "for (#%s in 0 .. < %s)" iter_meta_var n) $ PP.build loop_body -- ================================================================================ diff --git a/src/Traq/CQPL/TypeCheck.hs b/src/Traq/CQPL/TypeCheck.hs index 0070c24..eeabea6 100644 --- a/src/Traq/CQPL/TypeCheck.hs +++ b/src/Traq/CQPL/TypeCheck.hs @@ -18,7 +18,6 @@ import Control.Monad (forM, unless, when) import Control.Monad.Except (MonadError (throwError)) import Control.Monad.Reader (MonadReader, ReaderT, local, runReaderT) import Control.Monad.State (execStateT) -import Data.Foldable (toList) import Data.List (intersect) import GHC.Generics (Generic) import Text.Printf (printf) @@ -129,16 +128,19 @@ type TypeChecker sizeT = ReaderT (CheckingCtx sizeT) (Either Err.MyError) -- Type Checking -- ================================================================================ +typeCheckBasicGate :: forall size. (P.TypingReqs size) => BasicGate -> [P.VarType size] -> TypeChecker size () +typeCheckBasicGate Toffoli tys = verifyArgTys tys [P.tbool, P.tbool, P.tbool] +typeCheckBasicGate CNOT tys = verifyArgTys tys [P.tbool, P.tbool] +typeCheckBasicGate XGate tys = verifyArgTys tys [P.tbool] +typeCheckBasicGate HGate tys = verifyArgTys tys [P.tbool] +typeCheckBasicGate ZGate tys = verifyArgTys tys [P.tbool] +typeCheckBasicGate (Rz _) tys = verifyArgTys tys [P.tbool] +typeCheckBasicGate (PhaseOnZero _) _ = return () +typeCheckBasicGate COPY tys = let n = length tys `div` 2 in verifyArgTys (take n tys) (drop n tys) +typeCheckBasicGate SWAP tys = let n = length tys `div` 2 in verifyArgTys (take n tys) (drop n tys) + typeCheckUnitary :: forall sizeT. (P.TypingReqs sizeT) => Unitary sizeT -> [P.VarType sizeT] -> TypeChecker sizeT () --- basic gates -typeCheckUnitary (BasicGateU Toffoli) tys = verifyArgTys tys [P.tbool, P.tbool, P.tbool] -typeCheckUnitary (BasicGateU CNOT) tys = verifyArgTys tys [P.tbool, P.tbool] -typeCheckUnitary (BasicGateU XGate) tys = verifyArgTys tys [P.tbool] -typeCheckUnitary (BasicGateU HGate) tys = verifyArgTys tys [P.tbool] --- general gates -typeCheckUnitary (BasicGateU COPY) tys = let n = length tys `div` 2 in verifyArgTys (take n tys) (drop n tys) -typeCheckUnitary (BasicGateU SWAP) tys = let n = length tys `div` 2 in verifyArgTys (take n tys) (drop n tys) -typeCheckUnitary Refl0 _ = return () +typeCheckUnitary (BasicGateU g) tys = typeCheckBasicGate g tys typeCheckUnitary (DistrU (P.UniformE ty)) tys = verifyArgTys tys [ty] typeCheckUnitary (DistrU (P.BernoulliE _)) tys = verifyArgTys tys [P.tbool] typeCheckUnitary (RevEmbedU xs e) tys = do @@ -202,12 +204,7 @@ typeCheckStmt SkipS = return () typeCheckStmt (CommentS _) = return () -- Simple statements typeCheckStmt AssignS{rets, expr} = do - let expr_vars = toList $ P.freeVars expr - expr_var_tys <- forM expr_vars $ \var -> do - view (P._typingCtx . Ctx.at var) - >>= maybeWithError (Err.MessageE $ printf "cannot find %s" var) - let gamma = Ctx.fromList $ zip expr_vars expr_var_tys - + gamma <- view P._typingCtx actual_ret_tys <- case runReaderT ?? gamma $ P.typeCheckBasicExpr expr of Left err -> Err.throwErrorMessage err @@ -257,7 +254,13 @@ typeCheckStmt IfThenElseS{cond, s_true, s_false} = do typeCheckStmt s_true typeCheckStmt s_false typeCheckStmt RepeatS{loop_body} = typeCheckStmt loop_body -typeCheckStmt ForInRangeS{loop_body} = typeCheckStmt loop_body +typeCheckStmt ForInRangeS{loop_body, iter_meta_var, iter_lim} = do + iter_ty <- case iter_lim of + P.MetaSize n -> pure $ P.Fin n + P.MetaValue n -> pure $ P.Fin $ fromIntegral n + P.MetaName _ -> Err.throwErrorMessage "cannot find iteration" + local (P._typingCtx . Ctx.ins ('#' : iter_meta_var) .~ iter_ty) $ + typeCheckStmt loop_body -- try by desugaring typeCheckStmt s = case desugarS s of Just s' -> typeCheckStmt s' diff --git a/src/Traq/Compiler/Prelude.hs b/src/Traq/Compiler/Prelude.hs index db26479..003b796 100644 --- a/src/Traq/Compiler/Prelude.hs +++ b/src/Traq/Compiler/Prelude.hs @@ -163,6 +163,7 @@ compileWith :: ( m ~ CompilerT ext , size ~ SizeType ext , P.HasFreeVars ext + , P.TypeInferrable ext size ) => (P.Program ext -> m ()) -> P.Program ext -> @@ -170,6 +171,7 @@ compileWith :: compileWith compiler prog = do unless (P.checkVarsUnique prog) $ throwError "program does not have unique variables!" + P.typeCheckProg prog let config = default_ diff --git a/src/Traq/Compiler/Quantum.hs b/src/Traq/Compiler/Quantum.hs index b06a313..73eb7a9 100644 --- a/src/Traq/Compiler/Quantum.hs +++ b/src/Traq/Compiler/Quantum.hs @@ -9,6 +9,7 @@ module Traq.Compiler.Quantum ( ) where import Control.Monad (forM_) +import Control.Monad.Except (MonadError (..)) import Lens.Micro.GHC import Lens.Micro.Mtl @@ -16,6 +17,7 @@ import Lens.Micro.Mtl import Traq.Control.Monad import qualified Traq.Data.Context as Ctx +import qualified Traq.Analysis.Annotate.Prelude as A import Traq.CQPL.Syntax import Traq.Compiler.Prelude import Traq.Compiler.Unitary @@ -41,6 +43,9 @@ class (CompileU ext) => CompileQ ext where instance (P.TypingReqs size) => CompileQ (P.Core size prec) where compileQ = \case {} +instance (P.TypingReqs size) => CompileQ (A.AnnFailProb (P.Core size prec)) where + compileQ (A.AnnFailProb _ ext) = case ext of {} + class CompileQ1 f where -- | all arguments/info provided to compile the given data type CompileQArgs f ext @@ -72,7 +77,37 @@ instance CompileQ1 P.Expr where return $ CallS{fun = FunctionCall proc_id, args = map Arg (args ++ rets), meta_params = []} -- primitive call compileQ1 rets P.PrimCallE{P.prim} = compileQ prim rets - compileQ1 _ _ = error "TODO: UNSUPPORTED" + -- loops + compileQ1 rets P.LoopE{loop_body_fun, initial_args} = do + P.FunDef{param_types} <- view (P._funCtx . Ctx.at loop_body_fun) >>= maybeWithError "cannot find loop body fun" + n <- case last param_types of + P.Fin n -> pure n + _ -> throwError "loop index must be of type `Fin`" + + iter_meta_var <- newIdent "ITER" + + iter_var <- newIdent "iter" + P._typingCtx . Ctx.ins iter_var .= P.Fin n + + let proc_id = mkQProcName loop_body_fun + + return $ + SeqS $ + [AssignS [y] (P.VarE x) | (x, y) <- zip initial_args rets] + ++ [ ForInRangeS + { iter_meta_var + , iter_lim = P.MetaSize n + , loop_body = + SeqS + [ AssignS [iter_var] (P.ParamE iter_meta_var) + , CallS + { fun = FunctionCall proc_id + , meta_params = [] + , args = map Arg rets ++ [Arg iter_var] ++ map Arg rets + } + ] + } + ] instance CompileQ1 P.Stmt where type CompileQArgs P.Stmt ext = () diff --git a/src/Traq/Compiler/Unitary.hs b/src/Traq/Compiler/Unitary.hs index 1d5df01..b227cb0 100644 --- a/src/Traq/Compiler/Unitary.hs +++ b/src/Traq/Compiler/Unitary.hs @@ -19,6 +19,7 @@ module Traq.Compiler.Unitary ( ) where import Control.Monad (zipWithM) +import Control.Monad.Except (MonadError (throwError)) import Data.Foldable (Foldable (toList)) import Lens.Micro.GHC @@ -27,6 +28,7 @@ import Lens.Micro.Mtl import Traq.Control.Monad import qualified Traq.Data.Context as Ctx +import qualified Traq.Analysis.Annotate.Prelude as A import qualified Traq.CQPL as CQPL import Traq.CQPL.Syntax import Traq.Compiler.Prelude @@ -77,6 +79,9 @@ class (P.TypeInferrable ext (SizeType ext)) => CompileU ext where instance (P.TypingReqs size) => CompileU (P.Core size prec) where compileU = \case {} +instance (P.TypingReqs size) => CompileU (A.AnnFailProb (P.Core size prec)) where + compileU (A.AnnFailProb _ ext) = case ext of {} + class CompileU1 f where -- | all arguments/info provided to compile the given data type CompileArgs f ext @@ -117,7 +122,55 @@ instance CompileU1 P.Expr where let qargs = map Arg $ args ++ rets ++ aux_vars return UCallS{uproc_id, qargs, dagger = False} compileU1 rets P.PrimCallE{prim} = compileU prim rets - compileU1 rets P.LoopE{initial_args, loop_body_fun} = error "TODO: compileU1 rets P.LoopE{initial_args, loop_body_fun}" + compileU1 rets P.LoopE{initial_args, loop_body_fun} = do + P.FunDef{param_types, ret_types} <- view (P._funCtx . Ctx.at loop_body_fun) >>= maybeWithError "cannot find loop body fun" + n <- case last param_types of + P.Fin n -> pure n + _ -> throwError "loop index must be of type `Fin`" + + let uproc_id = mkUProcName loop_body_fun + ProcSignature{aux_tys} <- use (_procSignatures . at uproc_id) >>= maybeWithError "cannot find uproc signature" + + -- fresh aux for each iteration + aux_vars <- mapM (allocAncilla . P.Arr n) aux_tys + + iter_meta_var <- newIdent "ITER" + iter_vars <- allocAncilla (P.Arr n (P.Fin n)) + + intermediates <- mapM (allocAncilla . P.Arr (n + 1)) ret_types + + let at_ix x = ArrElemArg (Arg x) (P.MetaName iter_meta_var) + + return $ + USeqS $ + [ UnitaryS + [Arg x_in, ArrElemArg (Arg x_out) (MetaSize 0)] + (BasicGateU COPY) + | (x_out, x_in) <- zip intermediates initial_args + ] + ++ [ UForInRangeS + { iter_meta_var + , iter_lim = P.MetaSize n + , uloop_body = + USeqS + [ UCallS + { uproc_id = uproc_id + , dagger = False + , qargs = + map at_ix intermediates + ++ [at_ix iter_vars] + ++ map at_ix intermediates + ++ map at_ix aux_vars + } + ] + , dagger = False + } + ] + ++ [ UnitaryS + [ArrElemArg (Arg x_last) (MetaSize n), Arg x_ret] + (BasicGateU COPY) + | (x_ret, x_last) <- zip rets intermediates + ] instance CompileU1 P.Stmt where type CompileArgs P.Stmt ext = () diff --git a/src/Traq/Data/Context.hs b/src/Traq/Data/Context.hs index 5e5b123..4ed9169 100644 --- a/src/Traq/Data/Context.hs +++ b/src/Traq/Data/Context.hs @@ -33,11 +33,13 @@ module Traq.Data.Context ( lookup', unsafePut, put, + putOrMatch, ) where import Prelude hiding (lookup, null) import qualified Prelude +import Control.Monad (when) import Control.Monad.Except (MonadError, throwError) import Control.Monad.Reader (MonadReader) import Control.Monad.State (MonadState) @@ -174,3 +176,10 @@ put x v = use (at x) >>= \case Nothing -> unsafePut x v _ -> throwError (printf "variable `%s` already exists!" x) + +-- | Match value if key exists, otherwise insert. +putOrMatch :: (MonadError String m, MonadState (Context a) m, Eq a) => Ident -> a -> m () +putOrMatch x v = + use (at x) >>= \case + Nothing -> unsafePut x v + (Just v') -> when (v /= v') $ throwError (printf "variable `%s` already exists!" x) diff --git a/src/Traq/Primitives/Amplify/Prelude.hs b/src/Traq/Primitives/Amplify/Prelude.hs index a6b9ef6..3a92da2 100644 --- a/src/Traq/Primitives/Amplify/Prelude.hs +++ b/src/Traq/Primitives/Amplify/Prelude.hs @@ -80,11 +80,11 @@ instance EvalPrim (Amplify sizeT precT) sizeT precT where evalPrim Amplify{p_min} (SamplerFn sampler) = do - -- TODO also push this into the primitive class book-keeping. - eval_env <- view id - -- result distribution + eval_env <- view id let mu = sampler [] & runReaderT ?? eval_env + + -- success probability let p_succ = Prob.probabilityOf success mu lift $ diff --git a/src/Traq/Primitives/Amplify/QAmplify.hs b/src/Traq/Primitives/Amplify/QAmplify.hs index 433a929..3c2694a 100644 --- a/src/Traq/Primitives/Amplify/QAmplify.hs +++ b/src/Traq/Primitives/Amplify/QAmplify.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} @@ -11,14 +12,24 @@ module Traq.Primitives.Amplify.QAmplify ( _EQSearch, ) where +import Control.Monad (forM, replicateM, when) +import Control.Monad.Trans (lift) +import Control.Monad.Writer (WriterT (..), censor) +import Data.Bifunctor (second) import GHC.Generics (Generic) +import Lens.Micro.GHC +import Lens.Micro.Mtl import qualified Numeric.Algebra as Alg +import Traq.Control.Monad +import qualified Traq.Data.Context as Ctx import qualified Traq.Data.Probability as Prob import Traq.Data.Subtyping import qualified Traq.Analysis as A +import qualified Traq.CQPL as CQPL +import qualified Traq.Compiler as Compiler import Traq.Prelude import Traq.Primitives.Amplify.Prelude import Traq.Primitives.Class @@ -67,18 +78,23 @@ instance (P.TypingReqs size, Floating prec) => UnitaryCostPrim (QAmplify size pr {- | Cost of quantum search adapted to general amplitude amplification. Eq. 4 of https://arxiv.org/abs/2203.04975 -} +_WQSearch_alpha :: (Floating prec) => prec +_WQSearch_alpha = 9.2 + +_WQSearch_N_Runs :: forall prec. (Floating prec) => A.FailProb prec -> prec +_WQSearch_N_Runs eps = logBase 3 (1 / A.getFailProb eps) + +_WQSearch_Q_Max :: forall prec. (Floating prec) => prec -> prec +_WQSearch_Q_Max p_min = _WQSearch_alpha / sqrt p_min + _WQSearch :: forall precT. (Floating precT) => A.FailProb precT -> precT -> precT -_WQSearch eps p_min = alpha * log (1 / A.getFailProb eps) / sqrt p_min - where - alpha = 9.2 +_WQSearch eps p_min = _WQSearch_N_Runs eps * _WQSearch_Q_Max p_min -- | Eq. 3 of https://arxiv.org/abs/2203.04975 _F :: forall precT. (Floating precT, Ord precT) => precT -> precT _F p_good | p_good >= 0.25 = 2.0344 - | otherwise = alpha / (3 * sqrt p_good) - where - alpha = 9.2 + | otherwise = _WQSearch_alpha / (3 * sqrt p_good) {- | Cost of quantum search adapted to general amplitude amplification. Eq. 2 of https://arxiv.org/abs/2203.04975 @@ -88,8 +104,7 @@ _EQSearch eps p_min p_good | p_good == 0 = _WQSearch eps p_min | otherwise = _F p_good * (1 + 1 / (1 - term)) where - term = _F p_good * sqrt p_min / alpha - alpha = 9.2 + term = _F p_good * sqrt p_min / _WQSearch_alpha instance (P.TypingReqs size, A.SizeToPrec size prec, Floating prec) => QuantumHavocCostPrim (QAmplify size prec) size prec where quantumQueryCostsUnitary (QAmplify Amplify{p_min}) eps = SamplerFn $ strongQueries $ _WQSearch eps p_min @@ -115,10 +130,261 @@ instance (P.EvalReqs size prec, Floating prec, Ord prec) => QuantumExpCostPrim ( -- Compilation -- ================================================================================ -instance UnitaryCompilePrim (QAmplify size prec) size prec where - compileUPrim (QAmplify Amplify{}) eps = do - error "TODO: CompileU QAmplify" +-- -------------------------------------------------------------------------------- +-- Unitary Compilation +-- -------------------------------------------------------------------------------- + +instance (Floating prec, RealFrac prec) => UnitaryCompilePrim (QAmplify size prec) size prec where + compileUPrim (QAmplify Amplify{p_min}) eps = do + -- return vars and types + rets <- view $ to ret_vars + let b = head rets + ret_tys <- forM rets $ \x -> do + mty <- use $ P._typingCtx . Ctx.at x + maybeWithError "" mty + + -- sampler + (SamplerFn call_upred) <- view $ to mk_ucall + (SamplerFn pred_aux_tys) <- view $ to uproc_aux_types + + -- parameters + let l = ceiling ((_FPAA_L eps p_min - 1) / 2.0) :: Int + let _L = 2 * l + 1 :: Int + + let acot x = atan (1 / x) :: Double + let gamma = acosh ((1.0 / fromIntegral _L) * cosh (1.0 / sqrt (A.getFailProb eps))) :: prec + let alphas = [2.0 * acot (tan (2 * pi * fromIntegral i / fromIntegral _L) * (1.0 - realToFrac gamma ** 2)) | i <- [1 .. l]] + let betas = map negate $ reverse alphas + + -- algorithm + qamplify_proc_name <- lift $ Compiler.newIdent "UAmplify" + pred_aux <- lift $ mapM Compiler.allocAncilla pred_aux_tys + + let all_params = + zip3 [] (repeat CQPL.ParamInp) [] + ++ zip3 rets (repeat CQPL.ParamOut) ret_tys + ++ zip3 pred_aux (repeat CQPL.ParamAux) pred_aux_tys + + let sampler_call = call_upred (map CQPL.Arg (rets ++ pred_aux)) + let uproc_body_stmt = + CQPL.USeqS $ + sampler_call + : concat + [ [ CQPL.UnitaryS [CQPL.Arg b] $ CQPL.BasicGateU $ CQPL.Rz beta + , CQPL.adjoint sampler_call + , CQPL.UnitaryS (map CQPL.Arg (rets ++ pred_aux)) $ CQPL.BasicGateU $ CQPL.PhaseOnZero (-alpha) + , sampler_call + ] + | (alpha, beta) <- zip alphas betas + ] + + return + CQPL.ProcDef + { CQPL.info_comment = "" + , CQPL.proc_name = qamplify_proc_name + , CQPL.proc_meta_params = [] + , CQPL.proc_param_types = map (view _3) all_params + , CQPL.proc_body = + CQPL.ProcBodyU $ + CQPL.UProcBody + { CQPL.uproc_param_names = map (view _1) all_params + , CQPL.uproc_param_tags = map (view _2) all_params + , CQPL.uproc_body_stmt + } + } + +-- -------------------------------------------------------------------------------- +-- CQ Compilation +-- -------------------------------------------------------------------------------- + +-- | Run K grover iterations +mkGroverK :: + forall ext size prec m. + ( m ~ PrimCompileMonad ext (QAmplify size prec) + , size ~ SizeType ext + ) => + m (CQPL.ProcDef size) +mkGroverK = do + proc_name <- Compiler.newIdent "Grover" + meta_k <- Compiler.newIdent "k" + + rets <- view $ to ret_vars + let b = head rets + ret_tys <- forM rets $ \x -> + use (P._typingCtx . Ctx.at x) >>= maybeWithError "missing variable" + + (SamplerFn mk_sampler_call) <- view $ to mk_ucall + (SamplerFn aux_tys) <- view $ to uproc_aux_types + aux_vars <- replicateM (length aux_tys) $ Compiler.newIdent "aux" + + let sampler_call = mk_sampler_call (map CQPL.Arg (rets ++ aux_vars)) + + let grover_iteration = + CQPL.USeqS + [ CQPL.UnitaryS [CQPL.Arg b] $ CQPL.BasicGateU CQPL.ZGate + , CQPL.adjoint sampler_call + , CQPL.UnitaryS (map CQPL.Arg (rets ++ aux_vars)) $ CQPL.BasicGateU (CQPL.PhaseOnZero pi) + , sampler_call + ] + + let uproc_body_stmt = + CQPL.USeqS + [ sampler_call + , CQPL.URepeatS{n_iter = P.MetaName meta_k, uloop_body = grover_iteration} + ] + + let params = + Compiler.withTag CQPL.ParamOut (zip rets ret_tys) + ++ Compiler.withTag CQPL.ParamAux (zip aux_vars aux_tys) + return $ + CQPL.ProcDef + { CQPL.info_comment = "" + , CQPL.proc_name + , CQPL.proc_meta_params = [meta_k] + , CQPL.proc_param_types = map (view _3) params + , CQPL.proc_body = + CQPL.ProcBodyU $ + CQPL.UProcBody + { CQPL.uproc_param_names = map (view _1) params + , CQPL.uproc_param_tags = map (view _2) params + , CQPL.uproc_body_stmt + } + } + +type LocalVars = [(Ident, P.VarType SizeT)] +type AlgoMonad ext prec = + WriterT (LocalVars, [CQPL.Stmt SizeT]) (PrimCompileMonad ext (QAmplify SizeT prec)) + +allocLocal :: (m ~ AlgoMonad ext prec) => Ident -> P.VarType SizeT -> m Ident +allocLocal pref ty = do + x <- Compiler.newIdent pref + writeElemAt _1 (x, ty) + return x + +addStmt :: (m ~ AlgoMonad ext prec) => CQPL.Stmt SizeT -> m () +addStmt = writeElemAt _2 + +withStmt :: (m ~ AlgoMonad ext prec) => (CQPL.Stmt SizeT -> CQPL.Stmt SizeT) -> m a -> m a +withStmt f = censor (second f') + where + f' ss = [f (CQPL.SeqS ss)] + +-- compute the limits for sampling `j` in each iteration. +qamplifySamplingRanges :: forall prec. (RealFloat prec) => prec -> [SizeT] +qamplifySamplingRanges p_min = go q_max js + where + q_max :: SizeT + q_max = ceiling $ _WQSearch_Q_Max p_min + + lambda :: prec + lambda = 6 / 5 + + go :: SizeT -> [SizeT] -> [SizeT] + go _ [] = [] + go lim (x : _) | x > lim = [] + go lim (x : xs) = x : go (lim - x) xs + + js :: [SizeT] + js = map floor js_f + + js_f :: [prec] + js_f = lambda : map nxt js_f + + nxt :: prec -> prec + nxt m = min (lambda * m) (1 / sqrt p_min) + +-- | Implementation of the hybrid quantum search algorithm \( \textbf{QSearch} \). +buildQAmplify :: + forall ext prec m. + ( RealFloat prec + , SizeType ext ~ SizeT + , m ~ AlgoMonad ext prec + ) => + -- | n_samples: number of classical samples + SizeT -> + -- | eps: max fail prob + A.FailProb prec -> + -- | p_min: min success probability of sampler + prec -> + m () +buildQAmplify n_samples eps p_min = do + -- rets + rets <- view $ to ret_vars + let b = head rets + + -- flag + not_done <- allocLocal "not_done" P.tbool + addStmt $ CQPL.AssignS [not_done] (P.ConstE (P.FinV 0) P.tbool) + + -- classical sampling + SamplerFn mkSamplerCCall <- view $ to mk_call + let sampler_call_c = mkSamplerCCall (map CQPL.Arg rets) + + when (n_samples /= 0) $ + addStmt $ + CQPL.WhileKWithCondExpr + (CQPL.MetaSize n_samples) + not_done + (P.notE (P.VarE b)) + sampler_call_c + + -- quantum iterations + uproc_grover_k <- lift $ withSandbox mkGroverK + lift $ Compiler.addProc uproc_grover_k + + let j_type = P.Fin (ceiling $ _WQSearch_Q_Max p_min) -- type for j and Q_sum + q_sum <- allocLocal "Q_sum" j_type + j <- allocLocal "j" j_type + j_lim <- allocLocal "j_lim" j_type + + let n_runs = ceiling $ _WQSearch_N_Runs eps + + withStmt (CQPL.RepeatS (CQPL.MetaSize n_runs)) $ do + addStmt $ CQPL.AssignS [q_sum] (P.ConstE{P.val = P.FinV 0, P.ty = j_type}) + + let sampling_ranges = qamplifySamplingRanges p_min + withStmt + ( \s -> + CQPL.ForInArray + { CQPL.loop_index = j_lim + , CQPL.loop_index_ty = j_type + , CQPL.loop_values = [P.ConstE (P.FinV v_j) j_type | v_j <- sampling_ranges] + , CQPL.loop_body = s + } + ) + $ do + addStmt $ CQPL.RandomDynS j j_lim + addStmt $ CQPL.AssignS [q_sum] (P.BinOpE P.AddOp (P.VarE q_sum) (P.VarE j)) + addStmt $ CQPL.AssignS [not_done] (P.VarE not_done P..&&. (P.VarE q_sum P..<=. P.VarE j_lim)) + withStmt (CQPL.ifThenS not_done) $ do + addStmt $ + CQPL.CallS + { CQPL.fun = CQPL.UProcAndMeas (CQPL.proc_name uproc_grover_k) + , CQPL.meta_params = [Right j] + , CQPL.args = map CQPL.Arg rets + } + addStmt $ CQPL.AssignS [not_done] (P.VarE not_done P..&&. P.notE (P.VarE b)) + +instance (RealFloat prec) => QuantumCompilePrim (QAmplify SizeT prec) SizeT prec where + compileQPrim (QAmplify Amplify{p_min}) eps = do + rets <- view $ to ret_vars + ret_tys <- forM rets $ \x -> + use (P._typingCtx . Ctx.at x) >>= maybeWithError "missing variable" + + proc_name <- Compiler.newIdent "QAmplify" + ((), (local_vars, body)) <- runWriterT $ withSandbox $ buildQAmplify 0 eps p_min -instance QuantumCompilePrim (QAmplify size prec) size prec where - compileQPrim (QAmplify Amplify{}) eps = do - error "TODO: CompileQ QAmplify" + return $ + CQPL.ProcDef + { CQPL.info_comment = "" + , CQPL.proc_name + , CQPL.proc_meta_params = [] + , CQPL.proc_param_types = ret_tys + , CQPL.proc_body = + CQPL.ProcBodyC $ + CQPL.CProcBody + { CQPL.cproc_param_names = rets + , CQPL.cproc_local_vars = local_vars + , CQPL.cproc_body_stmt = CQPL.SeqS body + } + } diff --git a/src/Traq/Primitives/Class.hs b/src/Traq/Primitives/Class.hs index 3d036be..8febd31 100644 --- a/src/Traq/Primitives/Class.hs +++ b/src/Traq/Primitives/Class.hs @@ -546,7 +546,7 @@ instance CQPL.CallS { fun = CQPL.FunctionCall $ Compiler.mkQProcName pfun_name , meta_params = [] - , args = map CQPL.Arg $ placeArgsWithExcess pfun_args xs + , args = placeArgsWithExcess (map (fmap CQPL.Arg) pfun_args) xs } mk_meas <- @@ -555,7 +555,7 @@ instance CQPL.CallS { fun = CQPL.UProcAndMeas $ Compiler.mkUProcName pfun_name , meta_params = [] - , args = map CQPL.Arg $ placeArgsWithExcess pfun_args xs + , args = placeArgsWithExcess (map (fmap CQPL.Arg) pfun_args) xs } let builder = diff --git a/src/Traq/Primitives/Class/Compile.hs b/src/Traq/Primitives/Class/Compile.hs index f117859..67aa7d4 100644 --- a/src/Traq/Primitives/Class/Compile.hs +++ b/src/Traq/Primitives/Class/Compile.hs @@ -29,7 +29,7 @@ import qualified Traq.ProtoLang as P -- -------------------------------------------------------------------------------- type UCallBuilder size = [CQPL.Arg size] -> CQPL.UStmt size -type CallBuilder size = [Ident] -> CQPL.Stmt size +type CallBuilder size = [CQPL.Arg size] -> CQPL.Stmt size -- | Helpers to compile a primitive. data PrimCompileEnv shape size = PrimCompileEnv diff --git a/src/Traq/Primitives/Search/QSearchCFNW.hs b/src/Traq/Primitives/Search/QSearchCFNW.hs index 55f94ff..d84f467 100644 --- a/src/Traq/Primitives/Search/QSearchCFNW.hs +++ b/src/Traq/Primitives/Search/QSearchCFNW.hs @@ -255,7 +255,7 @@ addGroverIteration c x b = do let unifX = CQPL.DistrU (P.UniformE x_ty) addPredCall c x b writeElem $ CQPL.UnitaryS [x] (CQPL.Adjoint unifX) - writeElem $ CQPL.UnitaryS [x] CQPL.Refl0 + writeElem $ CQPL.UnitaryS [x] (CQPL.BasicGateU (CQPL.PhaseOnZero pi)) -- reflect on |0> writeElem $ CQPL.UnitaryS [x] unifX algoQSearchZalkaRandomIterStep :: @@ -506,7 +506,7 @@ groverK k (x, x_ty) b mk_pred = CQPL.USeqS [ mk_pred x b , CQPL.UnitaryS [CQPL.Arg x] (CQPL.Adjoint unifX) - , CQPL.UnitaryS [CQPL.Arg x] CQPL.Refl0 + , CQPL.UnitaryS [CQPL.Arg x] (CQPL.BasicGateU (CQPL.PhaseOnZero pi)) , CQPL.UnitaryS [CQPL.Arg x] unifX ] @@ -689,7 +689,7 @@ instance _ -> [(ret, P.tbool)] (BooleanPredicate meas_upred) <- view $ to mk_meas - let pred_caller x b = meas_upred [x, b] + let pred_caller x b = meas_upred [CQPL.Arg x, CQPL.Arg b] (qsearch_body, qsearch_local_vars) <- lift $ diff --git a/src/Traq/ProtoLang/Syntax.hs b/src/Traq/ProtoLang/Syntax.hs index a9407a9..60b2b13 100644 --- a/src/Traq/ProtoLang/Syntax.hs +++ b/src/Traq/ProtoLang/Syntax.hs @@ -430,6 +430,9 @@ data Core sizeT precT type instance SizeType (Core size prec) = size type instance PrecType (Core size prec) = prec +instance PP.ToCodeString (Core size prec) where + build = \case {} + {- | Simple void extension with integer size and double prec. Usage: @p :: Program Core'@ -} diff --git a/src/Traq/ProtoLang/TypeCheck.hs b/src/Traq/ProtoLang/TypeCheck.hs index e049933..8e2fd75 100644 --- a/src/Traq/ProtoLang/TypeCheck.hs +++ b/src/Traq/ProtoLang/TypeCheck.hs @@ -324,7 +324,7 @@ instance (TypeInferrable ext sizeT) => TypeInferrable (Stmt ext) sizeT where throwError $ ("Expected " <> show (length rets) <> " outputs, but given " <> show (length out_tys) <> " vars to bind.") <> (" (return variables: " <> show rets <> ", output types: " <> show out_tys <> ")") - zipWithM_ Ctx.put rets out_tys + zipWithM_ Ctx.putOrMatch rets out_tys pure [] -- sequence inferTypes (SeqS ss) = mapM_ inferTypes ss >> pure [] @@ -363,8 +363,7 @@ typeCheckFun throwError "number of returns must match the types" let gamma = Ctx.fromList $ zip param_names param_types - -- gamma' <- execStateT ?? gamma $ runReaderT ?? funCtx $ inferTypes body_stmt - (_, gamma', _) <- runRWST (inferTypes body_stmt) funCtx gamma + (_, gamma', ()) <- runRWST (inferTypes body_stmt) funCtx gamma forM_ (zip ret_names ret_types) $ \(x, t) -> do when (has _Just (gamma ^. Ctx.at x)) $ do throwError $ printf "parameter `%s` cannot be returned, please copy it into a new variable and return that" x diff --git a/src/Traq/ProtoLang/Vars.hs b/src/Traq/ProtoLang/Vars.hs index 1a922e4..4dc7f2e 100644 --- a/src/Traq/ProtoLang/Vars.hs +++ b/src/Traq/ProtoLang/Vars.hs @@ -147,6 +147,12 @@ instance RenameVars (BasicExpr size) where renameVars pref (DynIndexE a i) = DynIndexE (renameVars pref a) (renameVars pref i) renameVars pref (UpdateArrE a i v) = UpdateArrE (renameVars pref a) (renameVars pref i) (renameVars pref v) renameVars pref (ProjectE tup i) = ProjectE (renameVars pref tup) i + renameVars pref (TernaryE{branch, lhs, rhs}) = + TernaryE + { branch = renameVars pref branch + , lhs = renameVars pref lhs + , rhs = renameVars pref rhs + } renameVars _ e = e instance (RenameVars ext) => RenameVars (Expr ext) where @@ -154,7 +160,7 @@ instance (RenameVars ext) => RenameVars (Expr ext) where renameVars _ e@RandomSampleE{} = e renameVars prefix e@FunCallE{args} = e{args = addPrefix prefix args} renameVars prefix PrimCallE{prim} = PrimCallE $ renameVars prefix prim - renameVars _ _ = error "rename: unsupported expr" + renameVars prefix e@LoopE{initial_args} = e{initial_args = addPrefix prefix initial_args} instance (RenameVars ext) => RenameVars (Stmt ext) where renameVars prefix ExprS{rets, expr} = @@ -182,3 +188,6 @@ instance (RenameVars ext) => RenameVars (NamedFunDef ext) where instance (RenameVars ext) => RenameVars (Program ext) where renameVars pref (Program fs) = Program $ map (renameVars pref) fs + +instance RenameVars (Core size prec) where + renameVars _ = \case {} diff --git a/test/Traq/Examples/TreeGeneratorSpec.hs b/test/Traq/Examples/TreeGeneratorSpec.hs index 6e9de7c..5baf80e 100644 --- a/test/Traq/Examples/TreeGeneratorSpec.hs +++ b/test/Traq/Examples/TreeGeneratorSpec.hs @@ -15,6 +15,7 @@ import qualified Traq.Compiler as Compiler import Traq.Prelude import Traq.Primitives import Traq.ProtoLang +import qualified Traq.ProtoLang as P import Test.Hspec import TestHelpers @@ -121,16 +122,16 @@ spec = do , ([ArrV [FinV 1, FinV 1]], 0.2) ] - xdescribe "Compile" $ do + describe "Compile" $ do let eps = A.failProb (0.0001 :: Double) it "lowers" $ do - ex <- loadKnapsack 2 20 30 2 + ex <- P.renameVars' <$> loadKnapsack 2 20 30 2 ex' <- expectRight $ A.annotateProgWith (_exts (A.annSinglePrim eps)) ex assertRight $ Compiler.lowerProgram ex' it "typechecks" $ do - ex <- loadKnapsack 2 20 30 2 + ex <- P.renameVars' <$> loadKnapsack 2 20 30 2 ex' <- expectRight $ A.annotateProgWith (_exts (A.annSinglePrim eps)) ex ex_uqpl <- expectRight $ Compiler.lowerProgram ex' assertRight $ CQPL.typeCheckProgram ex_uqpl @@ -147,3 +148,15 @@ spec = do let result = runProgram @Core' (loopExample 10 20) funInterpCtx [] result `shouldBeDistribution` [([FinV 10], 1.0)] + + describe "Compile" $ do + it "lowers" $ do + let ex = P.renameVars' $ loopExample @Core' 10 20 + ex' <- expectRight $ A.annotateProgWith (_exts A.annNoPrims) ex + assertRight $ Compiler.lowerProgram ex' + + it "typechecks" $ do + let ex = P.renameVars' $ loopExample @Core' 10 20 + ex' <- expectRight $ A.annotateProgWith (_exts A.annNoPrims) ex + ex_uqpl <- expectRight $ Compiler.lowerProgram ex' + assertRight $ CQPL.typeCheckProgram ex_uqpl diff --git a/tools/compile.hs b/tools/compile.hs index b57e316..2b4552b 100644 --- a/tools/compile.hs +++ b/tools/compile.hs @@ -64,7 +64,7 @@ subsNM params s = Sym.unSym $ foldr subsOnce s params compile :: (RealFloat precT, Show precT) => P.Program (WorstCasePrims SizeT precT) -> precT -> IO String compile prog eps = do - let prog_rn = P.renameVars' prog + let prog_rn = if P.checkVarsUnique prog then prog else P.renameVars' prog prog' <- either fail pure $ A.annotateProgWithErrorBudget (P.failProb eps) prog_rn cqpl_prog <- either fail pure $ CompileQ.lowerProgram prog' let nqubits = CQPL.numQubits cqpl_prog