Compilation for amplitude amplification

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)

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

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

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);
 }
 
 

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;

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);
 }
 
 

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