Compilation for quantum max-finding

.ghci

@@ -1,19 +1,38 @@
 :set -DTEST -isrc -itest
 
-:set -XNamedFieldPuns
-:set -XLambdaCase
-:set -XScopedTypeVariables 
-:set -XApplicativeDo 
-:set -XRankNTypes 
+:set -XAllowAmbiguousTypes
+:set -XApplicativeDo
+:set -XBangPatterns
+:set -XConstraintKinds
+:set -XCPP
+:set -XDefaultSignatures
+:set -XDeriveAnyClass
+:set -XDeriveFoldable
+:set -XDeriveFunctor
+:set -XDeriveGeneric
+:set -XDerivingStrategies
+:set -XDuplicateRecordFields
+:set -XEmptyCase
+:set -XEmptyDataDeriving
+:set -XExplicitForAll
 :set -XFlexibleContexts 
-:set -XTypeFamilies 
-:set -XTypeOperators
-:set -XMultiWayIf
-
 :set -XFlexibleInstances
-:set -XFunctionalDependencies 
-:set -XMultiParamTypeClasses 
-:set -XUndecidableInstances
+:set -XFunctionalDependencies
+:set -XGeneralisedNewtypeDeriving
+:set -XGeneralizedNewtypeDeriving
+:set -XImplicitParams
+:set -XInstanceSigs
+:set -XLambdaCase
+:set -XMultiParamTypeClasses
+:set -XMultiWayIf
+:set -XNamedFieldPuns
+:set -XNoRebindableSyntax
+:set -XRankNTypes 
+:set -XRecordWildCards
+:set -XScopedTypeVariables
+:set -XStandaloneDeriving
 :set -XTupleSections
 :set -XTypeApplications
-:set -XRecordWildCards
+:set -XTypeFamilies
+:set -XTypeOperators
+:set -XUndecidableInstances

examples/cryptanalysis/3_round_feistel.qpl

@@ -82,11 +82,11 @@ uproc SimonOneRound_U(x : OUT Fin<2>, x_1 : OUT BitVec<20>, y : AUX Fin<2>, y_1
   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>>) {
+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>>) {
   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
+  // simon's post-processing: unitarily solve linear system: (ret, ret_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>>) {
@@ -105,11 +105,11 @@ uproc SimonOneRound_U_1(x_2 : OUT Fin<2>, x_3 : OUT BitVec<20>, y_2 : AUX Fin<2>
   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>>) } {
+proc QSimon(ret_2 : Fin<2>, ret_3 : 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
+  // simon's post-processing: solve linear system: (ret_2, ret_3) . (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>>) } {

examples/cryptanalysis/even_mansour.qpl

@@ -29,11 +29,11 @@ uproc SimonOneRound_U(x_1 : OUT BitVec<20>, y : AUX BitVec<20>, yy : AUX BitVec<
   x_1 *= Adj-Distr[uniform : 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>>) {
+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>>) {
   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: (k1_1) . (USimon_aux) = 0
+  // simon's post-processing: unitarily solve linear system: (ret) . (USimon_aux) = 0
 }
 
 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>) {
@@ -57,11 +57,11 @@ uproc SimonOneRound_U_1(x_2 : OUT BitVec<20>, y_1 : AUX BitVec<20>, yy_1 : AUX B
   x_2 *= Adj-Distr[uniform : BitVec<20>];
 }
 
-proc QSimon(k1 : BitVec<20>) { locals : (QSimon__u : Arr<31, BitVec<20>>) } {
+proc QSimon(ret_1 : 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: (k1) . (QSimon__u) = 0
+  // simon's post-processing: solve linear system: (ret_1) . (QSimon__u) = 0
 }
 
 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>>) } {