Skip to content

Misc updates #50

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
anurudhp merged 1 commit into from
Apr 1, 2026
Merged

Misc updates #50

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions examples/cryptanalysis/3_round_feistel.qpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,14 +72,14 @@ proc f(b : Fin<2>, x : BitVec<20>, zero : Fin<2>, res : BitVec<20>) { locals : (
}

uproc SimonOneRound_U(x_1 : OUT Fin<2>, x_2 : OUT BitVec<20>, y : AUX Fin<2>, y_1 : AUX BitVec<20>, yy : AUX Fin<2>, yy_1 : AUX BitVec<20>, aux_20 : AUX BitVec<20>, aux_21 : AUX BitVec<20>, aux_22 : AUX BitVec<20>, aux_23 : AUX BitVec<20>, aux_24 : AUX BitVec<20>, aux_25 : AUX BitVec<20>, aux_26 : AUX BitVec<20>, aux_27 : AUX BitVec<20>, aux_28 : AUX BitVec<20>, aux_29 : AUX BitVec<20>, aux_30 : AUX BitVec<20>, aux_31 : AUX BitVec<20>, aux_32 : AUX BitVec<20>, aux_33 : AUX BitVec<20>, aux_34 : AUX BitVec<20>, aux_35 : AUX BitVec<20>, aux_36 : AUX BitVec<20>, aux_37 : AUX BitVec<20>, aux_38 : AUX BitVec<20>, aux_39 : AUX BitVec<20>, aux_40 : AUX BitVec<20>, aux_41 : AUX BitVec<20>, aux_42 : AUX BitVec<20>, aux_43 : AUX BitVec<20>, aux_44 : AUX BitVec<20>, aux_45 : AUX BitVec<20>, aux_46 : AUX BitVec<20>, aux_47 : AUX Fin<2>) {
x_1 *= Distr[uniform : Fin<2>];
x_2 *= Distr[uniform : BitVec<20>];
x_1 *= Unif;
x_2 *= Unif;
call f_U(x_1, x_2, y, y_1, 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, aux_37, aux_38, aux_39, aux_40, aux_41, aux_42, aux_43, aux_44, aux_45, aux_46, aux_47);
y, yy *= COPY;
y_1, yy_1 *= COPY;
call-adj f_U(x_1, x_2, y, y_1, 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, aux_37, aux_38, aux_39, aux_40, aux_41, aux_42, aux_43, aux_44, aux_45, aux_46, aux_47);
x_2 *= Adj-Distr[uniform : BitVec<20>];
x_1 *= Adj-Distr[uniform : Fin<2>];
x_2 *= Unif;
x_1 *= Unif;
}

uproc USimon(ret : OUT Fin<2>, ret_1 : OUT BitVec<20>, USimon_aux : AUX Arr<32, Fin<2>>, USimon_aux_1 : AUX Arr<32, BitVec<20>>, USimon_aux_2 : AUX Arr<32, Fin<2>>, USimon_aux_3 : AUX Arr<32, BitVec<20>>, USimon_aux_4 : AUX Arr<32, Fin<2>>, USimon_aux_5 : AUX Arr<32, BitVec<20>>, USimon_aux_6 : AUX Arr<32, BitVec<20>>, USimon_aux_7 : AUX Arr<32, BitVec<20>>, USimon_aux_8 : AUX Arr<32, BitVec<20>>, USimon_aux_9 : AUX Arr<32, BitVec<20>>, USimon_aux_10 : AUX Arr<32, BitVec<20>>, USimon_aux_11 : AUX Arr<32, BitVec<20>>, USimon_aux_12 : AUX Arr<32, BitVec<20>>, USimon_aux_13 : AUX Arr<32, BitVec<20>>, USimon_aux_14 : AUX Arr<32, BitVec<20>>, USimon_aux_15 : AUX Arr<32, BitVec<20>>, USimon_aux_16 : AUX Arr<32, BitVec<20>>, USimon_aux_17 : AUX Arr<32, BitVec<20>>, USimon_aux_18 : AUX Arr<32, BitVec<20>>, USimon_aux_19 : AUX Arr<32, BitVec<20>>, USimon_aux_20 : AUX Arr<32, BitVec<20>>, USimon_aux_21 : AUX Arr<32, BitVec<20>>, USimon_aux_22 : AUX Arr<32, BitVec<20>>, USimon_aux_23 : AUX Arr<32, BitVec<20>>, USimon_aux_24 : AUX Arr<32, BitVec<20>>, USimon_aux_25 : AUX Arr<32, BitVec<20>>, USimon_aux_26 : AUX Arr<32, BitVec<20>>, USimon_aux_27 : AUX Arr<32, BitVec<20>>, USimon_aux_28 : AUX Arr<32, BitVec<20>>, USimon_aux_29 : AUX Arr<32, BitVec<20>>, USimon_aux_30 : AUX Arr<32, BitVec<20>>, USimon_aux_31 : AUX Arr<32, BitVec<20>>, USimon_aux_32 : AUX Arr<32, BitVec<20>>, USimon_aux_33 : AUX Arr<32, Fin<2>>) {
Expand All @@ -96,14 +96,14 @@ uproc AttackThreeRoundFeistel_U(s : OUT BitVec<20>, zero : AUX Fin<2>, zero_2 :
}

uproc SimonOneRound_U_1(x_3 : OUT Fin<2>, x_4 : OUT BitVec<20>, y_2 : AUX Fin<2>, y_3 : AUX BitVec<20>, yy_2 : AUX Fin<2>, yy_3 : AUX BitVec<20>, aux_48 : AUX BitVec<20>, aux_49 : AUX BitVec<20>, aux_50 : AUX BitVec<20>, aux_51 : AUX BitVec<20>, aux_52 : AUX BitVec<20>, aux_53 : AUX BitVec<20>, aux_54 : AUX BitVec<20>, aux_55 : AUX BitVec<20>, aux_56 : AUX BitVec<20>, aux_57 : AUX BitVec<20>, aux_58 : AUX BitVec<20>, aux_59 : AUX BitVec<20>, aux_60 : AUX BitVec<20>, aux_61 : AUX BitVec<20>, aux_62 : AUX BitVec<20>, aux_63 : AUX BitVec<20>, aux_64 : AUX BitVec<20>, aux_65 : AUX BitVec<20>, aux_66 : AUX BitVec<20>, aux_67 : AUX BitVec<20>, aux_68 : AUX BitVec<20>, aux_69 : AUX BitVec<20>, aux_70 : AUX BitVec<20>, aux_71 : AUX BitVec<20>, aux_72 : AUX BitVec<20>, aux_73 : AUX BitVec<20>, aux_74 : AUX BitVec<20>, aux_75 : AUX Fin<2>) {
x_3 *= Distr[uniform : Fin<2>];
x_4 *= Distr[uniform : BitVec<20>];
x_3 *= Unif;
x_4 *= Unif;
call f_U(x_3, x_4, y_2, y_3, 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, aux_65, aux_66, aux_67, aux_68, aux_69, aux_70, aux_71, aux_72, aux_73, aux_74, aux_75);
y_2, yy_2 *= COPY;
y_3, yy_3 *= COPY;
call-adj f_U(x_3, x_4, y_2, y_3, 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, aux_65, aux_66, aux_67, aux_68, aux_69, aux_70, aux_71, aux_72, aux_73, aux_74, aux_75);
x_4 *= Adj-Distr[uniform : BitVec<20>];
x_3 *= Adj-Distr[uniform : Fin<2>];
x_4 *= Unif;
x_3 *= Unif;
}

proc QSimon(ret_2 : Fin<2>, ret_3 : BitVec<20>) { locals : (QSimon__u : Arr<32, Fin<2>>, QSimon__u_1 : Arr<32, BitVec<20>>) } {
Expand Down
8 changes: 4 additions & 4 deletions examples/cryptanalysis/even_mansour.qpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,11 +22,11 @@ proc f(x : BitVec<20>, fx : BitVec<20>) { locals : (ex : BitVec<20>, px : BitVec
}

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>];
x_1 *= Unif;
call f_U(x_1, y, aux, aux_1, aux_2, aux_3, aux_4);
y, yy *= COPY;
call-adj f_U(x_1, y, aux, aux_1, aux_2, aux_3, aux_4);
x_1 *= Adj-Distr[uniform : BitVec<20>];
x_1 *= Unif;
}

uproc USimon(ret : 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>>) {
Expand All @@ -51,11 +51,11 @@ uproc BreakEM_U(k1 : OUT BitVec<20>, k2 : OUT BitVec<20>, ze : AUX BitVec<20>, e
}

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>];
x_2 *= Unif;
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_2, y_1, aux_5, aux_6, aux_7, aux_8, aux_9);
x_2 *= Adj-Distr[uniform : BitVec<20>];
x_2 *= Unif;
}

proc QSimon(ret_1 : BitVec<20>) { locals : (QSimon__u : Arr<31, BitVec<20>>) } {
Expand Down
24 changes: 12 additions & 12 deletions examples/cryptanalysis/grover_meets_simon.qpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,11 @@ ext uproc classifier_U(BitVec<20>, BitVec<20>, Fin<2>);
ext proc classifier(BitVec<20>, BitVec<20>, Fin<2>);

uproc SimonOneRound_U(k : BitVec<20>, 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>];
x_1 *= Unif;
call f_U(k, x_1, y, aux, aux_1, aux_2, aux_3, aux_4);
y, yy *= COPY;
call-adj f_U(k, x_1, y, aux, aux_1, aux_2, aux_3, aux_4);
x_1 *= Adj-Distr[uniform : BitVec<20>];
x_1 *= Unif;
}

uproc USimon(k : BitVec<20>, ret : OUT BitVec<20>, USimon_aux : AUX Arr<79, BitVec<20>>, USimon_aux_1 : AUX Arr<79, BitVec<20>>, USimon_aux_2 : AUX Arr<79, BitVec<20>>, USimon_aux_3 : AUX Arr<79, BitVec<20>>, USimon_aux_4 : AUX Arr<79, BitVec<20>>, USimon_aux_5 : AUX Arr<79, BitVec<20>>, USimon_aux_6 : AUX Arr<79, BitVec<20>>, USimon_aux_7 : AUX Arr<79, BitVec<20>>) {
Expand All @@ -49,11 +49,11 @@ uproc innerAttack_U(k : IN BitVec<20>, res : OUT Fin<2>, k1 : AUX BitVec<20>, k1
}

uproc SimonOneRound_U_1(k : BitVec<20>, 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>];
x_2 *= Unif;
call f_U(k, x_2, y_1, aux_5, aux_6, aux_7, aux_8, aux_9);
y_1, yy_1 *= COPY;
call-adj f_U(k, x_2, y_1, aux_5, aux_6, aux_7, aux_8, aux_9);
x_2 *= Adj-Distr[uniform : BitVec<20>];
x_2 *= Unif;
}

proc QSimon(k : BitVec<20>, ret_1 : BitVec<20>) { locals : (QSimon__u : Arr<79, BitVec<20>>) } {
Expand All @@ -71,23 +71,23 @@ proc innerAttack(k : BitVec<20>, res : Fin<2>) { locals : (k1 : BitVec<20>, x_2

uproc USearch(ret_2 : OUT Fin<2>, ret_3 : OUT BitVec<20>, aux_10 : AUX BitVec<20>, aux_11 : AUX BitVec<20>, aux_12 : AUX BitVec<20>, aux_13 : AUX BitVec<20>, aux_14 : AUX BitVec<20>, aux_15 : AUX BitVec<20>, aux_16 : AUX BitVec<20>, aux_17 : AUX BitVec<20>, aux_18 : AUX BitVec<20>, aux_19 : AUX BitVec<20>, aux_20 : AUX Arr<79, BitVec<20>>, aux_21 : AUX Arr<79, BitVec<20>>, aux_22 : AUX Arr<79, BitVec<20>>, aux_23 : AUX Arr<79, BitVec<20>>, aux_24 : AUX Arr<79, BitVec<20>>, aux_25 : AUX Arr<79, BitVec<20>>, aux_26 : AUX Arr<79, BitVec<20>>, aux_27 : AUX Arr<79, BitVec<20>>, aux_28 : AUX Arr<79, BitVec<20>>, aux_29 : AUX Arr<79, BitVec<20>>, aux_30 : AUX Arr<79, BitVec<20>>, aux_31 : AUX Arr<79, BitVec<20>>, aux_32 : AUX Arr<79, BitVec<20>>, aux_33 : AUX Arr<79, BitVec<20>>, aux_34 : AUX Arr<79, BitVec<20>>, aux_35 : AUX Arr<79, BitVec<20>>, aux_36 : AUX Fin<2>, aux_37 : AUX Fin<2>, ctrl : AUX Arr<16, Fin<2>>, pred_out : AUX Arr<16, Fin<2>>, n_iter : AUX Arr<16, Fin<805>>, s_arg : AUX Arr<16, BitVec<20>>) {
for (#run_ix in 0 .. < 16) {
n_iter[#run_ix] *= Distr[uniform : Fin<805>];
n_iter[#run_ix] *= Unif;
pred_out[#run_ix] *= X;
pred_out[#run_ix] *= H;
s_arg[#run_ix] *= Distr[uniform : BitVec<20>];
s_arg[#run_ix] *= Unif;
for (#LIM in 0 .. < 805) {
n_iter[#run_ix], ctrl[#run_ix] *= Embed[(a) => (a <= #LIM)];
call 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);
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] *= Adj-Unif;
s_arg[#run_ix] *= PhaseOnZero(3.141592653589793);
s_arg[#run_ix] *= Distr[uniform : BitVec<20>];
s_arg[#run_ix] *= Unif;
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<805>];
n_iter[#run_ix] *= Unif;
ctrl[#run_ix] *= X;
call 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);
ctrl[#run_ix], aux_37, pred_out[#run_ix] *= Toffoli;
Expand All @@ -106,12 +106,12 @@ uproc outerAttack_U(k0 : OUT BitVec<20>, ok : AUX Fin<2>, ok_1 : AUX Fin<2>, k0_
uproc Grover[k](x_3 : IN BitVec<20>, ret_4 : OUT Fin<2>, aux_38 : AUX BitVec<20>, aux_39 : AUX BitVec<20>, aux_40 : AUX BitVec<20>, aux_41 : AUX BitVec<20>, aux_42 : AUX BitVec<20>, aux_43 : AUX BitVec<20>, aux_44 : AUX BitVec<20>, aux_45 : AUX BitVec<20>, aux_46 : AUX BitVec<20>, aux_47 : AUX BitVec<20>, aux_48 : AUX Arr<79, BitVec<20>>, aux_49 : AUX Arr<79, BitVec<20>>, aux_50 : AUX Arr<79, BitVec<20>>, aux_51 : AUX Arr<79, BitVec<20>>, aux_52 : AUX Arr<79, BitVec<20>>, aux_53 : AUX Arr<79, BitVec<20>>, aux_54 : AUX Arr<79, BitVec<20>>, aux_55 : AUX Arr<79, BitVec<20>>, aux_56 : AUX Arr<79, BitVec<20>>, aux_57 : AUX Arr<79, BitVec<20>>, aux_58 : AUX Arr<79, BitVec<20>>, aux_59 : AUX Arr<79, BitVec<20>>, aux_60 : AUX Arr<79, BitVec<20>>, aux_61 : AUX Arr<79, BitVec<20>>, aux_62 : AUX Arr<79, BitVec<20>>, aux_63 : AUX Arr<79, BitVec<20>>, aux_64 : AUX Fin<2>) {
ret_4 *= X;
ret_4 *= H;
x_3 *= Distr[uniform : BitVec<20>];
x_3 *= Unif;
repeat (#k) {
call innerAttack_U(x_3, ret_4, 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_3 *= Adj-Distr[uniform : BitVec<20>];
x_3 *= Adj-Unif;
x_3 *= PhaseOnZero(3.141592653589793);
x_3 *= Distr[uniform : BitVec<20>];
x_3 *= Unif;
}
ret_4 *= H;
ret_4 *= X;
Expand Down
8 changes: 4 additions & 4 deletions examples/cryptanalysis/period_finding.qpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@ ext uproc f_U(BitVec<20>, BitVec<20>);
ext proc f(BitVec<20>, BitVec<20>);

uproc SimonOneRound_U(x : OUT BitVec<20>, y : AUX BitVec<20>, yy : AUX BitVec<20>) {
x *= Distr[uniform : BitVec<20>];
x *= Unif;
call f_U(x, y);
y, yy *= COPY;
call-adj f_U(x, y);
x *= Adj-Distr[uniform : BitVec<20>];
x *= Unif;
}

uproc USimon(ret : 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>>) {
Expand All @@ -24,11 +24,11 @@ uproc main_U(s : OUT BitVec<20>, s_1 : AUX BitVec<20>, x : AUX BitVec<20>, y : A
}

uproc SimonOneRound_U_1(x_1 : OUT BitVec<20>, y_1 : AUX BitVec<20>, yy_1 : AUX BitVec<20>) {
x_1 *= Distr[uniform : BitVec<20>];
x_1 *= Unif;
call f_U(x_1, y_1);
y_1, yy_1 *= COPY;
call-adj f_U(x_1, y_1);
x_1 *= Adj-Distr[uniform : BitVec<20>];
x_1 *= Unif;
}

proc QSimon(ret_1 : BitVec<20>) { locals : (QSimon__u : Arr<31, BitVec<20>>) } {
Expand Down
16 changes: 8 additions & 8 deletions examples/hillclimb/max_sat_hillclimb.qpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,23 +28,23 @@ proc good(x : Arr<20, Fin<2>>, i : Fin<20>, ok : Fin<2>) { locals : (w : Fin<100

uproc USearch(x : Arr<20, Fin<2>>, ret : OUT Fin<2>, ret_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>];
n_iter[#run_ix] *= Unif;
pred_out[#run_ix] *= X;
pred_out[#run_ix] *= H;
s_arg[#run_ix] *= Distr[uniform : Fin<20>];
s_arg[#run_ix] *= Unif;
for (#LIM in 0 .. < 4) {
n_iter[#run_ix], ctrl[#run_ix] *= Embed[(a) => (a <= #LIM)];
call good_U(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(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] *= Adj-Unif;
s_arg[#run_ix] *= PhaseOnZero(3.141592653589793);
s_arg[#run_ix] *= Distr[uniform : Fin<20>];
s_arg[#run_ix] *= Unif;
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>];
n_iter[#run_ix] *= Unif;
ctrl[#run_ix] *= X;
call good_U(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;
Expand All @@ -69,12 +69,12 @@ uproc hillclimb_iter_U(x : IN Arr<20, Fin<2>>, x' : OUT Arr<20, Fin<2>>, ok : AU
uproc Grover[k](x : Arr<20, Fin<2>>, x_4 : IN Fin<20>, ret_2 : 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>) {
ret_2 *= X;
ret_2 *= H;
x_4 *= Distr[uniform : Fin<20>];
x_4 *= Unif;
repeat (#k) {
call good_U(x, x_4, ret_2, aux_12, aux_13, aux_14, aux_15, aux_16, aux_17, aux_18, aux_19, aux_20, aux_21, aux_22);
x_4 *= Adj-Distr[uniform : Fin<20>];
x_4 *= Adj-Unif;
x_4 *= PhaseOnZero(3.141592653589793);
x_4 *= Distr[uniform : Fin<20>];
x_4 *= Unif;
}
ret_2 *= H;
ret_2 *= X;
Expand Down
9 changes: 4 additions & 5 deletions examples/hillclimb/steep_max_sat.qpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,12 +50,12 @@ uproc Compare(x : Arr<20, Fin<2>>, y : Fin<1000>, x_5 : Fin<20>, b_3 : Fin<2>, o
uproc Grover[k](x : Arr<20, Fin<2>>, y_1 : Fin<1000>, x_6 : Fin<20>, b_4 : Fin<2>, aux_18 : AUX Fin<1000>, aux_19 : AUX Fin<1000>, aux_20 : AUX Fin<2>, aux_21 : AUX Fin<2>, aux_22 : AUX Arr<20, Fin<2>>, aux_23 : AUX Fin<1000>, aux_24 : AUX Fin<2>, aux_25 : AUX Fin<2>, aux_26 : AUX Arr<20, Fin<2>>, aux_27 : AUX Fin<1000>) {
b_4 *= X;
b_4 *= H;
x_6 *= Distr[uniform : Fin<20>];
x_6 *= Unif;
repeat (#k) {
call Compare(x, y_1, x_6, b_4, aux_18, aux_19, aux_20, aux_21, aux_22, aux_23, aux_24, aux_25, aux_26, aux_27);
x_6 *= Adj-Distr[uniform : Fin<20>];
x_6 *= Adj-Unif;
x_6 *= PhaseOnZero(3.141592653589793);
x_6 *= Distr[uniform : Fin<20>];
x_6 *= Unif;
}
b_4 *= H;
b_4 *= X;
Expand Down Expand Up @@ -93,8 +93,7 @@ proc hillclimb_iter(x : Arr<20, Fin<2>>, x' : Arr<20, Fin<2>>) { locals : (w : F
}

uproc hillclimb_3_U(x_3 : OUT Arr<20, Fin<2>>, x_0 : AUX Arr<20, Fin<2>>, x_1 : AUX Arr<20, Fin<2>>, x_2 : AUX Arr<20, Fin<2>>, x_0_1 : AUX Arr<20, Fin<2>>, x_0_1_1 : AUX Arr<20, Fin<2>>, x_1_1 : AUX Arr<20, Fin<2>>, aux_28 : AUX Fin<1000>, aux_29 : AUX Fin<20>, aux_30 : AUX Fin<2>, aux_31 : AUX Fin<2>, aux_32 : AUX Fin<1000>, aux_33 : AUX Fin<20>, aux_34 : AUX Arr<20, Fin<20>>, aux_35 : AUX Arr<20, Fin<1000>>, aux_36 : AUX Arr<20, Fin<1000>>, aux_37 : AUX Arr<20, Fin<2>>, aux_38 : AUX Arr<20, Fin<2>>, aux_39 : AUX Arr<20, Arr<20, Fin<2>>>, aux_40 : AUX Arr<20, Fin<1000>>, aux_41 : AUX Arr<20, Fin<2>>, aux_42 : AUX Arr<20, Fin<2>>, aux_43 : AUX Arr<20, Arr<20, Fin<2>>>, aux_44 : AUX Arr<20, Fin<1000>>, aux_45 : AUX Fin<2>, aux_46 : AUX Fin<2>, aux_47 : AUX Arr<20, Fin<2>>, x_2_1 : AUX Arr<20, Fin<2>>, aux_48 : AUX Fin<1000>, aux_49 : AUX Fin<20>, aux_50 : AUX Fin<2>, aux_51 : AUX Fin<2>, aux_52 : AUX Fin<1000>, aux_53 : AUX Fin<20>, aux_54 : AUX Arr<20, Fin<20>>, aux_55 : AUX Arr<20, Fin<1000>>, aux_56 : AUX Arr<20, Fin<1000>>, aux_57 : AUX Arr<20, Fin<2>>, aux_58 : AUX Arr<20, Fin<2>>, aux_59 : AUX Arr<20, Arr<20, Fin<2>>>, aux_60 : AUX Arr<20, Fin<1000>>, aux_61 : AUX Arr<20, Fin<2>>, aux_62 : AUX Arr<20, Fin<2>>, aux_63 : AUX Arr<20, Arr<20, Fin<2>>>, aux_64 : AUX Arr<20, Fin<1000>>, aux_65 : AUX Fin<2>, aux_66 : AUX Fin<2>, aux_67 : AUX Arr<20, Fin<2>>, x_3_1 : AUX Arr<20, Fin<2>>, aux_68 : AUX Fin<1000>, aux_69 : AUX Fin<20>, aux_70 : AUX Fin<2>, aux_71 : AUX Fin<2>, aux_72 : AUX Fin<1000>, aux_73 : AUX Fin<20>, aux_74 : AUX Arr<20, Fin<20>>, aux_75 : AUX Arr<20, Fin<1000>>, aux_76 : AUX Arr<20, Fin<1000>>, aux_77 : AUX Arr<20, Fin<2>>, aux_78 : AUX Arr<20, Fin<2>>, aux_79 : AUX Arr<20, Arr<20, Fin<2>>>, aux_80 : AUX Arr<20, Fin<1000>>, aux_81 : AUX Arr<20, Fin<2>>, aux_82 : AUX Arr<20, Fin<2>>, aux_83 : AUX Arr<20, Arr<20, Fin<2>>>, aux_84 : AUX Arr<20, Fin<1000>>, aux_85 : AUX Fin<2>, aux_86 : AUX Fin<2>, aux_87 : AUX Arr<20, Fin<2>>) {
x_0_1 *= Distr[uniform : Arr<20, Fin<2>>];
x_0_1, x_0_1_1 *= COPY;
x_0_1, x_0_1_1 *= Distr[uniform : Arr<20, Fin<2>>];
x_0, x_0_1 *= SWAP;
call hillclimb_iter_U(x_0, x_1_1, 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);
x_1, x_1_1 *= SWAP;
Expand Down
Loading
Loading