Compilation for Simon's algorithm

examples/clustering_algorithm.traq

@@ -3,11 +3,11 @@
 
 // type point = Arr<N, Fin<M>>
 
-declare D_n(Fin<N>) -> Arr<N, Fin<M>> end
+ext fn D_n(Fin<N>) -> Arr<N, Fin<M>> end
 
-declare Dist(Arr<N, Fin<M>>, Arr<N, Fin<M>>) -> Fin<M> end
+ext fn Dist(Arr<N, Fin<M>>, Arr<N, Fin<M>>) -> Fin<M> end
 
-def check(dmax : Fin<M>, ij: Tup<Fin<N>, Fin<N>>) -> Bool do
+fn check(dmax : Fin<M>, ij: Tup<Fin<N>, Fin<N>>) -> Bool do
     i <- ij.0;
     j <- ij.1;
     xi <- D_n(i);
@@ -19,16 +19,18 @@ def check(dmax : Fin<M>, ij: Tup<Fin<N>, Fin<N>>) -> Bool do
     return ok
 end
 
-def loop_body(i: Fin<N>, j: Fin<N>) -> (Fin<N>, Fin<N>) do
+fn loop_body(i: Fin<N>, j: Fin<N>) -> (Fin<N>, Fin<N>) do
     xi <- D_n(i);
     xj <- D_n(j);
     dmax <- Dist(xi, xj);
 
-    i', j' <- @search<Tup<Fin<N>, Fin<N>>>[check(dmax, _)];
+    ok, ij' <- @search<Tup<Fin<N>, Fin<N>>>[check(dmax, _)];
+    i' <- ij'.0;
+    j' <- ij'.1;
     return i', j'
 end
 
-def main () -> (Fin<N>, Fin<N>) do
+fn main () -> (Fin<N>, Fin<N>) do
     i0 <-$ uniform : Fin<N>;
     j0 <-$ uniform : Fin<N>;
 

examples/cryptanalysis/3_round_feistel.qpl

@@ -0,0 +1,120 @@
+ext uproc R1_U(BitVec<20>, BitVec<20>);
+
+ext proc R1(BitVec<20>, BitVec<20>);
+
+ext uproc R2_U(BitVec<20>, BitVec<20>);
+
+ext proc R2(BitVec<20>, BitVec<20>);
+
+ext uproc R3_U(BitVec<20>, BitVec<20>);
+
+ext proc R3(BitVec<20>, BitVec<20>);
+
+uproc E_U(E_xL : IN BitVec<20>, E_xR : IN BitVec<20>, E_u3 : OUT BitVec<20>, E_v3 : OUT BitVec<20>, E_u0 : AUX BitVec<20>, E_v0 : AUX BitVec<20>, E_R1u0 : AUX BitVec<20>, E_u1 : AUX BitVec<20>, E_v1 : AUX BitVec<20>, E_R2u0 : AUX BitVec<20>, E_u2 : AUX BitVec<20>, E_v2 : AUX BitVec<20>, E_R3u2 : AUX BitVec<20>, E_u0_1 : AUX BitVec<20>, E_v0_1 : AUX BitVec<20>, E_R1u0_1 : AUX BitVec<20>, E_u1_1 : AUX BitVec<20>, E_v1_1 : AUX BitVec<20>, E_R2u0_1 : AUX BitVec<20>, E_u2_1 : AUX BitVec<20>, E_v2_1 : AUX BitVec<20>, E_R3u2_1 : AUX BitVec<20>, E_u3_1 : AUX BitVec<20>, E_v3_1 : AUX BitVec<20>) {
+  E_xL, E_u0_1 *= Embed[(E_xL) => E_xL];
+  E_u0, E_u0_1 *= SWAP;
+  E_xR, E_v0_1 *= Embed[(E_xR) => E_xR];
+  E_v0, E_v0_1 *= SWAP;
+  call R1_U(E_u0, E_R1u0_1);
+  E_R1u0, E_R1u0_1 *= SWAP;
+  E_R1u0, E_v0, E_u1_1 *= Embed[(E_R1u0, E_v0) => (E_v0 ^ E_R1u0)];
+  E_u1, E_u1_1 *= SWAP;
+  E_u0, E_v1_1 *= Embed[(E_u0) => E_u0];
+  E_v1, E_v1_1 *= SWAP;
+  call R2_U(E_u1, E_R2u0_1);
+  E_R2u0, E_R2u0_1 *= SWAP;
+  E_R2u0, E_v1, E_u2_1 *= Embed[(E_R2u0, E_v1) => (E_v1 ^ E_R2u0)];
+  E_u2, E_u2_1 *= SWAP;
+  E_u1, E_v2_1 *= Embed[(E_u1) => E_u1];
+  E_v2, E_v2_1 *= SWAP;
+  call R3_U(E_u2, E_R3u2_1);
+  E_R3u2, E_R3u2_1 *= SWAP;
+  E_R3u2, E_v2, E_u3_1 *= Embed[(E_R3u2, E_v2) => (E_v2 ^ E_R3u2)];
+  E_u3, E_u3_1 *= SWAP;
+  E_u2, E_v3_1 *= Embed[(E_u2) => E_u2];
+  E_v3, E_v3_1 *= SWAP;
+}
+
+proc E(E_xL : BitVec<20>, E_xR : BitVec<20>, E_u3 : BitVec<20>, E_v3 : BitVec<20>) { locals : (E_u0 : BitVec<20>, E_v0 : BitVec<20>, E_R1u0 : BitVec<20>, E_u1 : BitVec<20>, E_v1 : BitVec<20>, E_R2u0 : BitVec<20>, E_u2 : BitVec<20>, E_v2 : BitVec<20>, E_R3u2 : BitVec<20>) } {
+  E_u0 := E_xL;
+  E_v0 := E_xR;
+  call R1(E_u0, E_R1u0);
+  E_u1 := (E_v0 ^ E_R1u0);
+  E_v1 := E_u0;
+  call R2(E_u1, E_R2u0);
+  E_u2 := (E_v1 ^ E_R2u0);
+  E_v2 := E_u1;
+  call R3(E_u2, E_R3u2);
+  E_u3 := (E_v2 ^ E_R3u2);
+  E_v3 := E_u2;
+}
+
+ext uproc alpha_U(Fin<2>, BitVec<20>);
+
+ext proc alpha(Fin<2>, BitVec<20>);
+
+uproc f_U(f_b : IN Fin<2>, f_x : IN BitVec<20>, f_zero : OUT Fin<2>, f_res : OUT BitVec<20>, f_alpha_b : AUX BitVec<20>, f_yL : AUX BitVec<20>, f_yR : AUX BitVec<20>, f_alpha_b_1 : AUX BitVec<20>, f_yL_1 : AUX BitVec<20>, f_yR_1 : 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>, 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>, 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>, f_res_1 : AUX BitVec<20>, f_zero_1 : AUX Fin<2>) {
+  call alpha_U(f_b, f_alpha_b_1);
+  f_alpha_b, f_alpha_b_1 *= SWAP;
+  call E_U(f_alpha_b, f_x, f_yL_1, f_yR_1, aux, aux_1, aux_2, aux_3, aux_4, aux_5, aux_6, 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);
+  f_yL, f_yR, f_yL_1, f_yR_1 *= SWAP;
+  f_alpha_b, f_yR, f_res_1 *= Embed[(f_alpha_b, f_yR) => (f_yR ^ f_alpha_b)];
+  f_res, f_res_1 *= SWAP;
+  f_zero_1 *= Embed[() => 0:Fin<2>];
+  f_zero, f_zero_1 *= SWAP;
+}
+
+proc f(f_b : Fin<2>, f_x : BitVec<20>, f_zero : Fin<2>, f_res : BitVec<20>) { locals : (f_alpha_b : BitVec<20>, f_yL : BitVec<20>, f_yR : BitVec<20>) } {
+  call alpha(f_b, f_alpha_b);
+  call E(f_alpha_b, f_x, f_yL, f_yR);
+  f_res := (f_yR ^ f_alpha_b);
+  f_zero := 0:Fin<2>;
+}
+
+uproc SimonOneRound_U(x : OUT Fin<2>, x_1 : 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 *= Distr[uniform : Fin<2>];
+  x_1 *= Distr[uniform : BitVec<20>];
+  call f_U(x, x_1, 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, x_1, 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_1 *= Adj-Distr[uniform : BitVec<20>];
+  x *= Adj-Distr[uniform : Fin<2>];
+}
+
+uproc USimon(AttackThreeRoundFeistel_zero_1 : OUT Fin<2>, AttackThreeRoundFeistel_s_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>>) {
+  for (#i in 0 .. < 32) {
+    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], USimon_aux_8[#i], USimon_aux_9[#i], USimon_aux_10[#i], USimon_aux_11[#i], USimon_aux_12[#i], USimon_aux_13[#i], USimon_aux_14[#i], USimon_aux_15[#i], USimon_aux_16[#i], USimon_aux_17[#i], USimon_aux_18[#i], USimon_aux_19[#i], USimon_aux_20[#i], USimon_aux_21[#i], USimon_aux_22[#i], USimon_aux_23[#i], USimon_aux_24[#i], USimon_aux_25[#i], USimon_aux_26[#i], USimon_aux_27[#i], USimon_aux_28[#i], USimon_aux_29[#i], USimon_aux_30[#i], USimon_aux_31[#i], USimon_aux_32[#i], USimon_aux_33[#i]);
+  }
+  // simon's post-processing: unitarily solve linear system: (AttackThreeRoundFeistel_zero_1, AttackThreeRoundFeistel_s_1) . (USimon_aux, USimon_aux_1) = 0
+}
+
+uproc AttackThreeRoundFeistel_U(AttackThreeRoundFeistel_s : OUT BitVec<20>, AttackThreeRoundFeistel_zero : AUX Fin<2>, AttackThreeRoundFeistel_zero_1 : AUX Fin<2>, AttackThreeRoundFeistel_s_1 : AUX BitVec<20>, x : AUX Fin<2>, x_1 : AUX 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>, 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>>, aux_prim : AUX Arr<32, Fin<2>>, aux_prim_1 : AUX Arr<32, BitVec<20>>, aux_prim_2 : AUX Arr<32, Fin<2>>, aux_prim_3 : AUX Arr<32, BitVec<20>>, aux_prim_4 : AUX Arr<32, Fin<2>>, aux_prim_5 : AUX Arr<32, BitVec<20>>, aux_prim_6 : AUX Arr<32, BitVec<20>>, aux_prim_7 : AUX Arr<32, BitVec<20>>, aux_prim_8 : AUX Arr<32, BitVec<20>>, aux_prim_9 : AUX Arr<32, BitVec<20>>, aux_prim_10 : AUX Arr<32, BitVec<20>>, aux_prim_11 : AUX Arr<32, BitVec<20>>, aux_prim_12 : AUX Arr<32, BitVec<20>>, aux_prim_13 : AUX Arr<32, BitVec<20>>, aux_prim_14 : AUX Arr<32, BitVec<20>>, aux_prim_15 : AUX Arr<32, BitVec<20>>, aux_prim_16 : AUX Arr<32, BitVec<20>>, aux_prim_17 : AUX Arr<32, BitVec<20>>, aux_prim_18 : AUX Arr<32, BitVec<20>>, aux_prim_19 : AUX Arr<32, BitVec<20>>, aux_prim_20 : AUX Arr<32, BitVec<20>>, aux_prim_21 : AUX Arr<32, BitVec<20>>, aux_prim_22 : AUX Arr<32, BitVec<20>>, aux_prim_23 : AUX Arr<32, BitVec<20>>, aux_prim_24 : AUX Arr<32, BitVec<20>>, aux_prim_25 : AUX Arr<32, BitVec<20>>, aux_prim_26 : AUX Arr<32, BitVec<20>>, aux_prim_27 : AUX Arr<32, BitVec<20>>, aux_prim_28 : AUX Arr<32, BitVec<20>>, aux_prim_29 : AUX Arr<32, BitVec<20>>, aux_prim_30 : AUX Arr<32, BitVec<20>>, aux_prim_31 : AUX Arr<32, BitVec<20>>, aux_prim_32 : AUX Arr<32, BitVec<20>>, aux_prim_33 : AUX Arr<32, Fin<2>>) {
+  call USimon(AttackThreeRoundFeistel_zero_1, AttackThreeRoundFeistel_s_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);
+  AttackThreeRoundFeistel_zero, AttackThreeRoundFeistel_s, AttackThreeRoundFeistel_zero_1, AttackThreeRoundFeistel_s_1 *= SWAP;
+}
+
+uproc SimonOneRound_U_1(x_2 : OUT Fin<2>, x_3 : 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_2 *= Distr[uniform : Fin<2>];
+  x_3 *= Distr[uniform : BitVec<20>];
+  call f_U(x_2, x_3, 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_2, x_3, 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_3 *= Adj-Distr[uniform : BitVec<20>];
+  x_2 *= Adj-Distr[uniform : 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) {
+    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
+}
+
+proc AttackThreeRoundFeistel(AttackThreeRoundFeistel_s : BitVec<20>) { locals : (AttackThreeRoundFeistel_zero : Fin<2>, x_2 : Fin<2>, x_3 : BitVec<20>, y_2 : Fin<2>, y_3 : BitVec<20>, yy_2 : Fin<2>, yy_3 : BitVec<20>, aux_48 : BitVec<20>, aux_49 : BitVec<20>, aux_50 : BitVec<20>, aux_51 : BitVec<20>, aux_52 : BitVec<20>, aux_53 : BitVec<20>, aux_54 : BitVec<20>, aux_55 : BitVec<20>, aux_56 : BitVec<20>, aux_57 : BitVec<20>, aux_58 : BitVec<20>, aux_59 : BitVec<20>, aux_60 : BitVec<20>, aux_61 : BitVec<20>, aux_62 : BitVec<20>, aux_63 : BitVec<20>, aux_64 : BitVec<20>, aux_65 : BitVec<20>, aux_66 : BitVec<20>, aux_67 : BitVec<20>, aux_68 : BitVec<20>, aux_69 : BitVec<20>, aux_70 : BitVec<20>, aux_71 : BitVec<20>, aux_72 : BitVec<20>, aux_73 : BitVec<20>, aux_74 : BitVec<20>, aux_75 : Fin<2>, QSimon__u : Arr<32, Fin<2>>, QSimon__u_1 : Arr<32, BitVec<20>>) } {
+  call QSimon(AttackThreeRoundFeistel_zero, AttackThreeRoundFeistel_s);
+}
+
+
+// qubits: 39302

examples/cryptanalysis/3_round_feistel.traq

@@ -1,12 +1,12 @@
 // Taken from paper: Breaking Symmetric Cryptosystems Using Quantum Period Finding
 // https://link.springer.com/chapter/10.1007/978-3-662-53008-5_8
 
-declare R1(BitVec<n>) -> BitVec<n> end
-declare R2(BitVec<n>) -> BitVec<n> end
-declare R3(BitVec<n>) -> BitVec<n> end
+ext fn R1(BitVec<n>) -> BitVec<n> end
+ext fn R2(BitVec<n>) -> BitVec<n> end
+ext fn R3(BitVec<n>) -> BitVec<n> end
 
 // Figure 3
-def E(xL: BitVec<n>, xR: BitVec<n>) -> (BitVec<n>, BitVec<n>) do
+fn E(xL: BitVec<n>, xR: BitVec<n>) -> (BitVec<n>, BitVec<n>) do
     u0 <- xL;
     v0 <- xR;
 
@@ -28,21 +28,23 @@ def E(xL: BitVec<n>, xR: BitVec<n>) -> (BitVec<n>, BitVec<n>) do
     return u3, v3
 end 
 
-declare alpha(Bool) -> BitVec<n> end
+ext fn alpha(Bool) -> BitVec<n> end
 
-def f(b : Bool, x : BitVec<n>) -> BitVec<n> do
+fn f(b : Bool, x : BitVec<n>) -> (Bool, BitVec<n>) do
     alpha_b <- alpha(b);
     yL, yR <- E(alpha_b, x);
 
     res <- yR ^ alpha_b;
 
-    return res
+    zero <- const 0 : Bool;
+
+    return zero, res
 end
 
-def AttackThreeRoundFeistel() -> Bool do
-    b, s <- @findXorPeriod<n, 0.01>[f()];
+fn AttackThreeRoundFeistel() -> BitVec<n> do
+    zero, s <- @findXorPeriod<n_plus_1, 0.01>[f(_, _)];
 
-    return b, s
+    return s
 
     //// Verify the computed period:
     // zero <- const 0 : Bool;

examples/cryptanalysis/Makefile

@@ -0,0 +1,11 @@
+PROJ_DEPS=../../src ../../tools ../../traq.cabal
+
+all: period_finding.qpl even_mansour.qpl 3_round_feistel.qpl grover_meets_simon.qpl
+
+%.qpl: %.traq $(PROJ_DEPS)
+	cd ../../ && cabal run compile -- \
+		-i examples/cryptanalysis/$< \
+		-o examples/cryptanalysis/$@ \
+		-p 0.001 \
+		--arg n=20 \
+		--arg n_plus_1=21