OKlibrary  0.2.1.6
ConstraintTemplateSmallScaleRewriteRules.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 28.9.2010 (Swansea) */
00002 /* Copyright 2010, 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00035 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/ConstraintTemplateRewriteSystem.mac")$
00036 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00037 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Permutations.mac")$
00038 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00039 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/SmallScaleFieldMulCNF.mac")$
00040 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/SmallScaleSboxCNF.mac")$
00041 
00042 
00043 /* ***********************************************
00044    * Constraint template rewrite translations    *
00045    ***********************************************
00046 */
00047 
00048 /* Small scale AES variables, ss_v(i,id), for i in NN where id is an
00049    identifier used to allow specialisation:  */
00050 kill(ss_v)$
00051 declare(ss_v, noun)$
00052 declare(ss_v, posfun)$
00053 ss_var(i,id) := nounify(ss_v)(i,id)$
00054 /* For example, ss_v(1,o) is the first output bit.
00055 
00056    Note that these variables are then later wrapped in namespaces. */
00057 
00058 /* Given two integers n and m, a namespace, and
00059    a noun identifier, returns a list of AES variables of the form
00060    namespace(ss_v(i,id)) for n <= i <= m. */
00061 generate_ss_constraint_vars(n,m,namespace, id) :=
00062   create_list(namespace(ss_var(i,id)),i,n,m)$
00063 
00064 /* Rewrite maps */
00065 
00066 /* Standard rewrite mapping: */
00067 ss_rewrite_mapping_std :
00068   [["ss_cst",ss_cstrb],["ss_key_expansion_cst",ss_key_expansion_cstrb],
00069   ["ss_round_cst",ss_round_cstrb],
00070   ["ss_final_round_cst",ss_final_round_cstrb],
00071   ["ss_subbytes_cst",ss_subbytes_cstrb],
00072   ["ss_shiftrows_cst",ss_shiftrows_cstrb],
00073   ["ss_mixcolumns_cst",ss_mixcolumns_cstrb],
00074   ["ss_mixcolumn_cst",ss_mixcolumn_cstrb]]$
00075 
00076 /* Rewrite mapping introducing both forward and backward
00077    MixColumns translations: */
00078 ss_bimc_rewrite_mapping_std :
00079   [["ss_cst",ss_cstrb],["ss_key_expansion_cst",ss_key_expansion_cstrb],
00080   ["ss_round_cst",ss_round_cstrb],
00081   ["ss_final_round_cst",ss_final_round_cstrb],
00082   ["ss_subbytes_cst",ss_subbytes_cstrb],
00083   ["ss_shiftrows_cst",ss_shiftrows_cstrb],
00084   ["ss_mixcolumns_cst",ss_mixcolumns_cstrb],
00085   ["ss_mixcolumn_cst",ss_bi_mixcolumn_cstrb]]$
00086 
00087 /* Rewrite mapping translating the MixColumns operation as a boolean
00088    matrix multiplication (using addition constraints): */
00089 ss_boolm_rewrite_mapping_std :
00090   [["ss_cst",ss_cstrb],["ss_key_expansion_cst",ss_key_expansion_cstrb],
00091   ["ss_round_cst",ss_round_cstrb],
00092   ["ss_final_round_cst",ss_final_round_cstrb],
00093   ["ss_subbytes_cst",ss_subbytes_cstrb],
00094   ["ss_shiftrows_cst",ss_shiftrows_cstrb],
00095   ["ss_mixcolumns_cst",ss_mixcolumns_cstrb],
00096   ["ss_mixcolumn_cst",ss_mixcolumn_boolm_cstrb]]$
00097 
00098 /* Rewrite mapping translating the MixColumns operation using
00099    the canonical translation: */
00100 ss_boxmc_rewrite_mapping_std :
00101   [["ss_cst",ss_cstrb],["ss_key_expansion_cst",ss_key_expansion_cstrb],
00102   ["ss_round_cst",ss_round_cstrb],
00103   ["ss_final_round_cst",ss_final_round_cstrb],
00104   ["ss_subbytes_cst",ss_subbytes_cstrb],
00105   ["ss_shiftrows_cst",ss_shiftrows_cstrb],
00106   ["ss_mixcolumns_cst",ss_mixcolumns_cstrb]]$
00107 /* Note that the MixColumns is left unspecified and
00108    the user must specify use the "ss_ts_translation_mapping" translation
00109    mapping which will then translate all constraints remaining after the
00110    constraint rewrite stage, using the canonical translation, including
00111    the MixColumn.
00112 
00113    In all other rewrite maps, the MixColumn is translated during the
00114    rewrite stage and therefore, even if one uses "ss_ts_translation_mapping",
00115    there are no "ss_mixcolumn_cst" constraints to be translated using the
00116    canonical translation, only the multiplications etc which the MixColumns
00117    was rewritten to.
00118 */
00119 
00120 /* Sbox and MixColumns combined: */
00121 ss_boxcombined_rewrite_mapping_std :
00122   [["ss_cst",ss_cstrb],["ss_key_expansion_cst",ss_key_expansion_cstrb],
00123   ["ss_round_cst",ss_round_cstrb],
00124   ["ss_final_round_cst",ss_final_round_cstrb],
00125   ["ss_shiftrows_cst",ss_shiftrows_cstrb],
00126   ["ss_mixcolumns_cst",ss_mixcolumns_cstrb],
00127   ["ss_mixcolumn_cst",ss_mixcolumn_cstrb],
00128   ["ss_subbytes_cst", [lambda([cst],[cons("eq_cst",rest(cst))]),lambda([cst],[]),cstt_id_ns]],
00129   ["ss_mul_cst",[lambda([cst],[cons("ss_sbox_w_mul_cst",rest(cst))]),lambda([cst],[]),cstt_id_ns]]]$
00130 
00131 /* Core round operation on single column treated as one operation: */
00132 ss_round_column_rewrite_mapping_std :
00133   [["ss_cst",ss_cstrb],["ss_key_expansion_cst",ss_key_expansion_cstrb],
00134   ["ss_round_cst",ss_round_core_box_cstrb],
00135   ["ss_final_round_cst",ss_final_round_cstrb],
00136   ["ss_shiftrows_cst",ss_shiftrows_cstrb],
00137   ["ss_round_columns_cst",ss_round_columns_cstrb]]$
00138 
00139 
00140 /* ***********************************************
00141    * Constraint template rewrite functions       *
00142    ***********************************************
00143 */
00144 
00145 /* Small scale AES constraint rewrite bundle: */
00146 ss_cstrb : [ss_cstr_cstl,ss_namespace,ss_ns_var_l]$
00147 
00148 /* Small scale AES namespace: */
00149 kill(ss_ctr_ns)$
00150 declare(ss_ctr_ns,noun)$
00151 declare(ss_ctr_ns,posfun)$
00152 ss_namespace([args]) := apply(nounify(ss_ctr_ns),args)$
00153 
00154 
00155 /* The list of new variables introduced by ss_cstr_cstl
00156    with the constraint template cst as input: */
00157 ss_ns_var_l(cst) := block(
00158   [ss_num_rounds,vars : [],namespace, ss_args_l,
00159   ss_num_columns, ss_num_rows, ss_base, ss_exp,
00160   num_block_bits],
00161   namespace : cstt_namespace_new (ss_namespace,cst),
00162   ss_arg_l : cstt_args_l(cst),
00163   ss_num_rounds : ss_arg_l[1],
00164   ss_num_columns : ss_arg_l[2],
00165   ss_num_rows : ss_arg_l[3],
00166   ss_base : ss_arg_l[4],
00167   ss_exp : ss_arg_l[5],
00168   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00169   vars : cons(
00170     generate_ss_constraint_vars(1,(ss_num_rounds+1)*num_block_bits,
00171       namespace,nounify(k)),vars),
00172   vars : cons(
00173     generate_ss_constraint_vars(1,ss_num_rounds*num_block_bits,
00174       namespace,nounify(o)),vars),
00175   return(lappend(vars)))$
00176 
00177 /* TODO: Rewrite documentation below. */
00178 
00179 /* Rewrite function designed to rewrite the AES constraint template "ss_ct".
00180 
00181    Takes as arguments 385 variables, which are the arguments of the "aes_ct"
00182    instance being rewritten.
00183 
00184    The first 384 of these are 128 plaintext, 128 key and 128 ciphertext
00185    variables respectively. The final argument is a pair (list) of auxiliary
00186    arguments, the first being the namespace to place all variables introduced
00187    by this function within, and the second being the integer number of rounds
00188    which specifies which round-variant of AES is being rewritten.
00189 
00190    The result of this function is a list of constraint template instances
00191    representing the AES constraint template instance being rewritten.
00192 */
00193 ss_cstr_cstl(cst) := block(
00194   [bits, pBits, kBits, cBits, ekBits, ib, ob, rs : [],namespace,
00195   ss_num_rounds, ss_num_columns, ss_num_rows, ss_base, ss_exp, ss_poly,
00196   ss_sbox_matrix, ss_affine_constant, ss_mixcolumns_matrix, ss_arg_l,
00197   final_round_b,num_block_bits ],
00198   ss_arg_l : cstt_args_l(cst),
00199   ss_num_rounds : ss_arg_l[1],
00200   ss_num_columns : ss_arg_l[2],
00201   ss_num_rows : ss_arg_l[3],
00202   ss_base : ss_arg_l[4],
00203   ss_exp : ss_arg_l[5],
00204   ss_poly : ss_arg_l[6],
00205   ss_sbox_matrix : ss_arg_l[7],
00206   ss_affine_constant : ss_arg_l[8],
00207   ss_mixcolumns_matrix : ss_arg_l[9],
00208   final_round_b : ss_arg_l[10],
00209   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00210   bits : cst[2],
00211   namespace : cstt_namespace_new(ss_namespace,cst),
00212   pBits : take_elements(num_block_bits,bits),
00213   kBits : take_elements(num_block_bits,rest(bits,num_block_bits)),
00214   cBits : rest(bits,num_block_bits*2),
00215   ekBits :
00216     generate_ss_constraint_vars(
00217       1,(ss_num_rounds+1)*num_block_bits,namespace,nounify(k)),
00218   /* Key Expansion */
00219   rs : cons(
00220     cstt_new(
00221       "ss_key_expansion_cst",append(kBits,ekBits),
00222       [ss_num_rounds, ss_num_columns, ss_num_rows, ss_base, ss_exp,
00223        ss_poly, ss_sbox_matrix, ss_affine_constant],namespace),
00224     rs),
00225   ib : pBits,
00226   all_ob :
00227     generate_ss_constraint_vars(1,(ss_num_rounds)*num_block_bits,
00228       namespace,nounify(o)),
00229   ob : take_elements(num_block_bits,all_ob),
00230   /* Initial Round Key Addition */
00231   rs : cons(
00232     cstt_new(
00233       "ss_add_cst",append(ib,take_elements(num_block_bits,ekBits),ob),
00234       [], namespace),
00235     rs),
00236   ib : ob,
00237   /* Rounds */
00238   for j : 1 thru (ss_num_rounds - 1) do block(
00239     ob : take_elements(num_block_bits,rest(all_ob,j*num_block_bits)),
00240     rs : cons(
00241       cstt_new("ss_round_cst",
00242         append(ib,take_elements(num_block_bits,rest(ekBits,j*num_block_bits)),
00243           ob),
00244         [j, ss_num_columns, ss_num_rows, ss_base, ss_exp,
00245        ss_poly, ss_sbox_matrix, ss_affine_constant, ss_mixcolumns_matrix],
00246        namespace),rs),
00247     ib : ob
00248   ),
00249   /* Final Round */
00250   /* If we have a variant with a reduced number of rounds, truncate rather
00251      than generalise */
00252   ob : cBits,
00253   if final_round_b then 
00254     rs : cons(
00255       cstt_new("ss_final_round_cst",
00256         append(ib,take_elements(num_block_bits,
00257             rest(ekBits,ss_num_rounds*num_block_bits)),ob),
00258         [ss_num_columns, ss_num_rows, ss_base, ss_exp,
00259        ss_poly, ss_sbox_matrix, ss_affine_constant],
00260        namespace),rs)
00261   else
00262     rs : cons(
00263       cstt_new("ss_round_cst",
00264         append(ib,take_elements(num_block_bits,
00265             rest(ekBits,ss_num_rounds*num_block_bits)),ob),
00266         [ss_num_rounds, ss_num_columns, ss_num_rows, ss_base, ss_exp,
00267        ss_poly, ss_sbox_matrix, ss_affine_constant, ss_mixcolumns_matrix],
00268        namespace),rs),
00269   return(rs)
00270 )$
00271 
00272 /*
00273    SS Round
00274 
00275 */
00276 
00277 ss_round_cstrb :
00278  [ss_round_cstr_cstl, ss_round_namespace, ss_round_ns_var_l]$
00279 
00280 /* SS round namespace */
00281 kill(ss_round_ns)$
00282 declare(ss_round_ns,noun)$
00283 declare(ss_round_ns,posfun)$
00284 ss_round_namespace([args]) := apply(nounify(ss_round_ns),args)$
00285 
00286 ss_round_ns_var_l(cst) := block([vars : [],namespace,
00287   ss_num_columns, ss_num_rows, ss_base, ss_exp, ss_poly,
00288   ss_sbox_matrix, ss_affine_constant, ss_mixcolumns_matrix, ss_arg_l,
00289   num_block_bits],
00290   ss_arg_l : cstt_args_l(cst),
00291   ss_num_columns : ss_arg_l[2],
00292   ss_num_rows : ss_arg_l[3],
00293   ss_exp : ss_arg_l[5],
00294   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00295   namespace : cstt_namespace_new(ss_round_namespace,cst),
00296   vars : cons(generate_ss_constraint_vars(1,num_block_bits,
00297       namespace,nounify(so)),vars),
00298   vars : cons(generate_ss_constraint_vars(1,num_block_bits,
00299       namespace,nounify(ro)),vars),
00300   vars : cons(generate_ss_constraint_vars(1,num_block_bits,
00301       namespace,nounify(mo)),vars),
00302   return(lappend(vars)))$
00303 /* Returns a set of conditions representing SS round given
00304    128 plaintext variables, 128 key variables and 128 output
00305    variables. */
00306 ss_round_cstr_cstl(cst) := block(
00307   [namespace,bits,iBits, rkBits, oBits,tBits,rs:[],
00308   ss_num_columns, ss_num_rows, ss_base, ss_exp, ss_poly,
00309   ss_sbox_matrix, ss_affine_constant, ss_mixcolumns_matrix, ss_arg_l,
00310   num_block_bits],
00311   ss_arg_l : cstt_args_l(cst),
00312   ss_num_rounds : ss_arg_l[1],
00313   ss_num_columns : ss_arg_l[2],
00314   ss_num_rows : ss_arg_l[3],
00315   ss_base : ss_arg_l[4],
00316   ss_exp : ss_arg_l[5],
00317   ss_poly : ss_arg_l[6],
00318   ss_sbox_matrix : ss_arg_l[7],
00319   ss_affine_constant : ss_arg_l[8],
00320   ss_mixcolumns_matrix : ss_arg_l[9],
00321   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00322   bits : cst[2],
00323   namespace : cstt_namespace_new(ss_round_namespace,cst),
00324   iBits : take_elements(num_block_bits,bits),
00325   rkBits : take_elements(num_block_bits,rest(bits,num_block_bits)),
00326   oBits : rest(bits,num_block_bits*2),
00327   tBits : generate_ss_constraint_vars(1,num_block_bits,namespace,nounify(so)),
00328   rs : cons(
00329     cstt_new("ss_subbytes_cst",
00330         append(iBits,tBits),
00331         [ss_base, ss_exp,
00332        ss_poly, ss_sbox_matrix, ss_affine_constant],namespace),
00333     rs),
00334   iBits : tBits,
00335   tBits : generate_ss_constraint_vars(1,num_block_bits,namespace,nounify(ro)),
00336   rs : cons(
00337     cstt_new("ss_shiftrows_cst",
00338         append(iBits,tBits),
00339         [ss_num_columns, ss_num_rows],namespace),
00340     rs),
00341   iBits : tBits,
00342   tBits : generate_ss_constraint_vars(1,num_block_bits,namespace,nounify(mo)),
00343   rs : cons(
00344     cstt_new("ss_mixcolumns_cst",
00345       append(iBits, tBits),
00346       [ss_num_columns, ss_num_rows, ss_base, ss_exp,
00347        ss_poly, ss_mixcolumns_matrix],namespace),
00348     rs),
00349   iBits : tBits,
00350   tBits : oBits,
00351   rs : cons(
00352     cstt_new("ss_add_cst",
00353       append(iBits, rkBits, tBits),
00354       [],namespace),
00355     rs),
00356   return(rs)
00357 )$
00358 
00359 /* The round as shiftrows then num_columns column boxes: */
00360 ss_round_core_box_cstrb :
00361  [ss_round_core_box_cstr_cstl, ss_round_core_box_namespace, ss_round_core_box_ns_var_l]$
00362 
00363 /* SS round namespace: */
00364 kill(ss_round_core_box_ns)$
00365 declare(ss_round_core_box_ns,noun)$
00366 declare(ss_round_core_box_ns,posfun)$
00367 ss_round_core_box_namespace([args]) := apply(nounify(ss_round_core_box_ns),args)$
00368 
00369 ss_round_core_box_ns_var_l(cst) := block([vars : [],namespace, ss_num_columns,
00370   ss_num_rows, ss_base, ss_exp, ss_poly, ss_sbox_matrix, ss_affine_constant,
00371   ss_mixcolumns_matrix, ss_arg_l, num_block_bits, gen_vars],
00372   ss_arg_l : cstt_args_l(cst),
00373   ss_num_columns : ss_arg_l[2],
00374   ss_num_rows : ss_arg_l[3],
00375   ss_exp : ss_arg_l[5],
00376   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00377   namespace : cstt_namespace_new(ss_round_core_box_namespace,cst),
00378   gen_vars : generate_ss_constraint_vars,
00379   vars : cons(gen_vars(1,num_block_bits,namespace,nounify(ro)), vars),
00380   vars : cons(gen_vars(1,num_block_bits,namespace,nounify(mo)), vars),
00381   return(lappend(vars)))$
00382 ss_round_core_box_cstr_cstl(cst) := block(
00383   [namespace,bits,iBits, rkBits, oBits,tBits,rs:[], ss_num_columns,
00384    ss_num_rows, ss_base, ss_exp, ss_poly, ss_sbox_matrix, ss_affine_constant,
00385    ss_mixcolumns_matrix, ss_arg_l, num_block_bits],
00386   ss_arg_l : cstt_args_l(cst),
00387   ss_num_rounds : ss_arg_l[1],
00388   ss_num_columns : ss_arg_l[2],
00389   ss_num_rows : ss_arg_l[3],
00390   ss_base : ss_arg_l[4],
00391   ss_exp : ss_arg_l[5],
00392   ss_poly : ss_arg_l[6],
00393   ss_sbox_matrix : ss_arg_l[7],
00394   ss_affine_constant : ss_arg_l[8],
00395   ss_mixcolumns_matrix : ss_arg_l[9],
00396   bits : cstt_vars_l(cst),
00397   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00398   namespace : cstt_namespace_new(ss_round_core_box_namespace,cst),
00399   gen_vars : generate_ss_constraint_vars,
00400   iBits : take_elements(num_block_bits,bits),
00401   oBits : rest(bits,num_block_bits*2),
00402   tBits : gen_vars(1,num_block_bits,namespace,nounify(ro)),
00403   rs : cons(
00404     cstt_new("ss_shiftrows_cst",
00405       append(iBits,tBits),[ss_num_columns, ss_num_rows],namespace),
00406     rs),
00407   iBits : tBits,
00408   tBits : gen_vars(1,num_block_bits,namespace,nounify(mo)),
00409   rs : cons(
00410     cstt_new("ss_round_columns_cst",
00411       append(iBits, tBits),
00412       [ss_num_columns, ss_num_rows, ss_base, ss_exp, ss_poly, ss_sbox_matrix,
00413        ss_affine_constant, ss_mixcolumns_matrix],
00414       namespace),
00415     rs),
00416   iBits : tBits,
00417   rkBits : take_elements(num_block_bits,rest(bits,num_block_bits)),
00418   tBits : oBits,
00419   rs : cons(
00420     cstt_new("ss_add_cst", append(iBits, rkBits, tBits), [],namespace),
00421     rs),
00422   return(rs)
00423 )$
00424 
00425 /*
00426    SS Final round
00427    
00428 */
00429 
00430 ss_final_round_cstrb :
00431  [ss_final_round_cstr_cstl, ss_final_round_namespace,ss_final_round_ns_var_l]$
00432 
00433 /* SS final round namespace */
00434 kill(ss_final_round_ns)$
00435 declare(ss_final_round_ns,noun)$
00436 declare(ss_final_round_ns,posfun)$
00437 ss_final_round_namespace([args]) := apply(nounify(ss_final_round_ns),args)$
00438 
00439 ss_final_round_ns_var_l(cst) := block(
00440   [vars : [],namespace,
00441   ss_num_columns, ss_num_rows, ss_base, ss_exp, ss_poly,
00442   ss_sbox_matrix, ss_affine_constant, ss_mixcolumns_matrix, ss_arg_l,
00443   num_block_bits],
00444   ss_arg_l : cstt_args_l(cst),
00445   ss_num_columns : ss_arg_l[1],
00446   ss_num_rows : ss_arg_l[2],
00447   ss_exp : ss_arg_l[4],
00448   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00449   namespace : cstt_namespace_new(ss_final_round_namespace,cst),
00450   vars : cons(generate_ss_constraint_vars(1,num_block_bits,namespace,
00451       nounify(so)),vars),
00452   vars : cons(generate_ss_constraint_vars(1,num_block_bits,namespace,
00453       nounify(ro)),vars),
00454   return(lappend(vars)))$
00455 /* Returns a set of conditions representing SS round given
00456    128 plaintext variables, 128 key variables and 128 output
00457    variables. */
00458 ss_final_round_cstr_cstl(cst) := block(
00459   [namespace,bits,iBits, rkBits, oBits,tBits,rs:[],
00460   ss_num_columns, ss_num_rows, ss_base, ss_exp, ss_poly,
00461   ss_sbox_matrix, ss_affine_constant, ss_mixcolumns_matrix, ss_arg_l,
00462   num_block_bits],
00463   ss_arg_l : cstt_args_l(cst),
00464   ss_num_columns : ss_arg_l[1],
00465   ss_num_rows : ss_arg_l[2],
00466   ss_base : ss_arg_l[3],
00467   ss_exp : ss_arg_l[4],
00468   ss_poly : ss_arg_l[5],
00469   ss_sbox_matrix : ss_arg_l[6],
00470   ss_affine_constant : ss_arg_l[7],
00471   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00472   bits : cst[2],
00473   namespace : cstt_namespace_new(ss_final_round_namespace,cst),
00474   iBits : take_elements(num_block_bits,bits),
00475   rkBits : take_elements(num_block_bits,rest(bits,num_block_bits)),
00476   oBits : rest(bits,num_block_bits*2),
00477   tBits : generate_ss_constraint_vars(1,num_block_bits,namespace,nounify(so)),
00478   rs : cons(
00479     cstt_new("ss_subbytes_cst",
00480         append(iBits,tBits),
00481         [ss_base, ss_exp,
00482        ss_poly, ss_sbox_matrix, ss_affine_constant],namespace),
00483     rs),
00484   iBits : tBits,
00485   tBits : generate_ss_constraint_vars(1,num_block_bits,namespace,nounify(ro)),
00486   rs : cons(
00487     cstt_new("ss_shiftrows_cst",
00488         append(iBits,tBits),
00489         [ss_num_columns, ss_num_rows],namespace),
00490     rs),
00491   iBits : tBits,
00492   tBits : oBits,
00493   rs : cons(
00494     cstt_new("ss_add_cst",
00495       append(iBits, rkBits, tBits),
00496       [],namespace),
00497     rs),
00498   return(rs)
00499 )$
00500 
00501 /*
00502    Subbytes
00503    
00504 */
00505 
00506 ss_subbytes_cstrb :
00507  [ss_subbytes_cstr_cstl,ss_subbytes_namespace,ss_subbytes_ns_var_l]$
00508 
00509 
00510 /* SS subbytes namespace */
00511 kill(ss_subbytes_ns)$
00512 declare(ss_subbytes_ns,noun)$
00513 declare(ss_subbytes_ns,posfun)$
00514 ss_subbytes_namespace([args]) := apply(nounify(ss_subbytes_ns),args)$
00515 
00516 ss_subbytes_ns_var_l([a]) := []$
00517 /* Returns a set of conditions representing the SS Subbytes operation given
00518    128 plaintext variables and 128 output variables. */
00519 ss_subbytes_cstr_cstl(cst) := block(
00520   [namespace,bits,iBits, rkBits, oBits,tBits,rs:[],ss_arg_l, num_block_bits,
00521   num_words,ss_base, ss_exp,ss_poly, ss_sbox_matrix, ss_affine_constant],
00522   ss_arg_l : cstt_args_l(cst),
00523   ss_base : ss_arg_l[1],
00524   ss_exp : ss_arg_l[2],
00525   ss_poly : ss_arg_l[3],
00526   ss_sbox_matrix : ss_arg_l[4],
00527   ss_affine_constant : ss_arg_l[5],
00528   bits : cst[2],
00529   num_block_bits : floor(length(bits) / 2),
00530   num_words : floor(num_block_bits / ss_exp),
00531   namespace : cstt_namespace_new(ss_subbytes_namespace,cst),
00532   iBits : take_elements(num_block_bits,bits),
00533   oBits : rest(bits,num_block_bits),
00534   for i : 0 thru num_words - 1 do
00535     rs : cons(
00536       cstt_new("ss_sbox_cst",
00537         append(
00538           take_elements(ss_exp, rest(iBits,i*ss_exp)),
00539           take_elements(ss_exp, rest(oBits,i*ss_exp))),
00540         [ss_base, ss_exp,ss_poly, ss_sbox_matrix, ss_affine_constant, i],
00541         namespace),
00542       rs),
00543   return(rs)
00544 )$
00545 
00546 
00547 /*
00548    Shiftrows
00549 
00550 */
00551 
00552 ss_shiftrows_cstrb :
00553  [ss_shiftrows_cstr_cstl,ss_shiftrows_namespace,ss_shiftrows_ns_var_l]$
00554 
00555 /* SS shiftrows namespace */
00556 kill(ss_shiftrows_ns)$
00557 declare(ss_shiftrows_ns,noun)$
00558 declare(ss_shiftrows_ns,posfun)$
00559 ss_shiftrows_namespace(arg_l) := apply(nounify(ss_shiftrows_ns),arg_l)$
00560 
00561 
00562 ss_shiftrows_ns_var_l([a]) := []$
00563 /* Returns a set of conditions representing the SS Shiftrows operation given
00564    128 plaintext variables and 128 output variables. */
00565 ss_shiftrows_cstr_cstl(cst) := block(
00566   [namespace,bits,iBits, oBits,count : 0, ss_arg_l, num_block_bits,
00567   ss_num_columns, ss_num_rows, ss_exp],
00568   ss_arg_l : cstt_args_l(cst),
00569   ss_num_columns : ss_arg_l[1],
00570   ss_num_rows : ss_arg_l[2],
00571   bits : cst[2],
00572   num_block_bits : floor(length(bits)/2),
00573   ss_exp : floor(num_block_bits / (ss_num_rows * ss_num_columns)),
00574   namespace : cstt_namespace_new(ss_shiftrows_namespace,cst),
00575   iBits : take_elements(num_block_bits,bits),
00576   oBits : take_elements(num_block_bits,rest(bits,num_block_bits)),
00577   map(
00578     lambda([a,b],
00579       cstt_new("eq_cst",[a,b],
00580         [],namespace)), oBits,
00581     lappend(
00582       rijn_m2l(ss_shiftrows(ss_l2m(
00583             partition_elements(iBits,ss_exp),ss_num_rows)))))
00584 )$
00585 
00586 
00587 /*
00588    Mixcolumns
00589 
00590 */
00591 
00592 ss_mixcolumns_cstrb :
00593  [ss_mixcolumns_cstr_cstl,ss_mixcolumns_namespace,ss_mixcolumns_ns_var_l]$
00594 
00595 /* SS mixcolumns namespace */
00596 kill(ss_mixcolumns_ns)$
00597 declare(ss_mixcolumns_ns,noun)$
00598 declare(ss_mixcolumns_ns,posfun)$
00599 ss_mixcolumns_namespace([arg_l]) := apply(nounify(ss_mixcolumns_ns),arg_l)$
00600 
00601 
00602 ss_mixcolumns_ns_var_l([a]) := []$
00603 /* Returns a set of conditions representing the SS Mixcolumns operation given
00604    128 plaintext variables and 128 output variables. */
00605 ss_mixcolumns_cstr_cstl(cst) := block(
00606   [namespace, bits,iBits, oBits, mc_i : 0,ss_arg_l,
00607   ss_num_columns, ss_num_rows, ss_base, ss_exp, ss_column_size,
00608        ss_poly, ss_mixcolumns_matrix, num_block_bits],
00609   ss_arg_l : cstt_args_l(cst),
00610   ss_num_columns : ss_arg_l[1],
00611   ss_num_rows : ss_arg_l[2],
00612   ss_base : ss_arg_l[3],
00613   ss_exp : ss_arg_l[4],
00614   ss_poly : ss_arg_l[5],
00615   ss_mixcolumns_matrix : ss_arg_l[6],
00616   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00617   ss_column_size : ss_num_rows * ss_exp,
00618   bits : cst[2],
00619   namespace : cstt_namespace_new(ss_mixcolumns_namespace,cst),
00620   iBits : take_elements(num_block_bits,bits),
00621   oBits : rest(bits,num_block_bits),
00622   map(lambda([a,b,column], 
00623     cstt_new("ss_mixcolumn_cst",
00624       append(lappend(a),lappend(b)),
00625       [ss_num_rows, ss_base, ss_exp,
00626        ss_poly, ss_mixcolumns_matrix, mc_i : mc_i + 1],namespace)),
00627     partition_elements(partition_elements(iBits,ss_exp),ss_num_rows),
00628     partition_elements(partition_elements(oBits,ss_exp),ss_num_rows),
00629     create_list(i,i,1,ss_num_columns))
00630 )$
00631 
00632 
00633 /*
00634    Whole column treated as one operation:
00635 
00636 */
00637 
00638 ss_round_columns_cstrb :
00639  [ss_round_columns_cstr_cstl,ss_round_columns_namespace,
00640   ss_round_columns_ns_var_l]$
00641 
00642 /* SS round_columns namespace: */
00643 kill(ss_round_columns_ns)$
00644 declare(ss_round_columns_ns,noun)$
00645 declare(ss_round_columns_ns,posfun)$
00646 ss_round_columns_namespace([arg_l]) :=
00647   apply(nounify(ss_round_columns_ns),arg_l)$
00648 
00649 
00650 ss_round_columns_ns_var_l([a]) := []$
00651 ss_round_columns_cstr_cstl(cst) := block(
00652   [namespace, bits,iBits, oBits, mc_i : 0,ss_arg_l,
00653    ss_num_columns, ss_num_rows, ss_base, ss_exp, ss_column_size,
00654    ss_poly, ss_mixcolumns_matrix, num_block_bits],
00655   ss_arg_l : cstt_args_l(cst),
00656   ss_num_columns : ss_arg_l[1],
00657   ss_num_rows : ss_arg_l[2],
00658   ss_base : ss_arg_l[3],
00659   ss_exp : ss_arg_l[4],
00660   ss_poly : ss_arg_l[5],
00661   ss_sbox_matrix : ss_arg_l[6],
00662   ss_sbox_affine_constant : ss_arg_l[7],
00663   ss_mixcolumns_matrix : ss_arg_l[8],
00664   num_block_bits : ss_num_columns * ss_num_rows * ss_exp,
00665   ss_column_size : ss_num_rows * ss_exp,
00666   bits : cst[2],
00667   namespace : cstt_namespace_new(ss_round_columns_namespace,cst),
00668   iBits : take_elements(num_block_bits,bits),
00669   oBits : rest(bits,num_block_bits),
00670   map(lambda([a,b,column], 
00671     cstt_new("ss_round_column_cst",
00672       append(lappend(a),lappend(b)),
00673       [ss_num_rows, ss_base, ss_exp,
00674        ss_poly,ss_sbox_matrix,ss_sbox_affine_constant,
00675        ss_mixcolumns_matrix, mc_i : mc_i + 1],namespace)),
00676     partition_elements(partition_elements(iBits,ss_exp),ss_num_rows),
00677     partition_elements(partition_elements(oBits,ss_exp),ss_num_rows),
00678     create_list(i,i,1,ss_num_columns))
00679 )$
00680 
00681 
00682 /*
00683    Bidirectional Mixcolumn
00684 
00685 */
00686 
00687 ss_bi_mixcolumn_cstrb :
00688  [ss_bi_mixcolumn_cstr_cstl,ss_bi_mixcolumn_namespace,ss_bi_mixcolumn_ns_var_l]$
00689 
00690 
00691 /* SS bi_mixcolumn namespace */
00692 kill(ss_bi_mixcolumn_ns)$
00693 declare(ss_bi_mixcolumn_ns,noun)$
00694 declare(ss_bi_mixcolumn_ns,posfun)$
00695 ss_bi_mixcolumn_namespace([args]) := apply(nounify(ss_bi_mixcolumn_ns),args)$
00696 
00697 ss_bi_mixcolumn_ns_var_l(cstt) := block(
00698   [cstt_new : cstt_namespace_replace(cstt,
00699     cstt_namespace_new(ss_bi_mixcolumn_namespace,cstt))],
00700   append(
00701     ss_mixcolumn_ns_var_l(cstt_new),
00702     ss_inv_mixcolumn_ns_var_l(cstt_new)))$
00703 /* Returns a set of conditions representing the SS bidirectional
00704    mixcolumn operation (the individual operation applied to a single column in
00705    SS bi_mixcolumns) given 128 plaintext variables and 128 output variables.
00706  */
00707 ss_bi_mixcolumn_cstr_cstl(cstt) := block(
00708   [cstt_new : cstt_namespace_replace(cstt,
00709     cstt_namespace_new(ss_bi_mixcolumn_namespace,cstt))],
00710   append(
00711     ss_mixcolumn_cstr_cstl(cstt_new),
00712     ss_inv_mixcolumn_cstr_cstl(cstt_new)))$
00713 
00714 
00715 /*
00716    Mixcolumn
00717 
00718 */
00719 
00720 ss_mixcolumn_cstrb :
00721  [ss_mixcolumn_cstr_cstl,ss_mixcolumn_namespace,ss_mixcolumn_ns_var_l]$
00722 
00723 
00724 /* SS mixcolumn namespace */
00725 kill(ss_mixcolumn_ns)$
00726 declare(ss_mixcolumn_ns,noun)$
00727 declare(ss_mixcolumn_ns,posfun)$
00728 ss_mixcolumn_namespace([args]) := apply(nounify(ss_mixcolumn_ns),args)$
00729 
00730 ss_mixcolumn_ns_var_l(cst) := block([vars : [],namespace,ss_arg_l,
00731   ss_column_size,ss_num_rows, ss_base, ss_exp, ss_column_size,ss_poly,
00732   ss_mixcolumns_matrix],
00733   ss_arg_l : cstt_args_l(cst),
00734   ss_num_rows : ss_arg_l[1],
00735   ss_base : ss_arg_l[2],
00736   ss_exp : ss_arg_l[3],
00737   ss_poly : ss_arg_l[4],
00738   ss_mixcolumns_matrix : ss_arg_l[5],
00739   ss_column_size : ss_exp * ss_num_rows,
00740   namespace :
00741     cstt_namespace_new(ss_mixcolumn_namespace,cst),
00742   for i : 1 thru ss_num_rows do
00743     for j : 1 thru ss_num_rows do block([var_block],
00744       var_block : ss_column_size * (i-1) + ss_exp * (j-1),
00745       if ss_mixcolumns_matrix[i,j] # 1 then
00746         vars : cons(
00747           generate_ss_constraint_vars(
00748             var_block+1,var_block+ss_exp,namespace,nounify(mc)),vars)),
00749   return(lappend(vars)))$
00750 /* Returns a set of conditions representing the SS Mixcolumn operation (the 
00751    individual operation applied to a single column in SS Mixcolumns) given
00752    128 plaintext variables and 128 output variables. */
00753 ss_mixcolumn_cstr_cstl(cst) := block(
00754   [namespace,bits,iBits, oBits, nc,rs : [],ss_arg_l, ss_column_size,
00755   ss_num_rows, ss_base, ss_exp, ss_column_size,
00756        ss_poly, ss_mixcolumns_matrix],
00757   ss_arg_l : cstt_args_l(cst),
00758   ss_num_rows : ss_arg_l[1],
00759   ss_base : ss_arg_l[2],
00760   ss_exp : ss_arg_l[3],
00761   ss_poly : ss_arg_l[4],
00762   ss_mixcolumns_matrix : ss_arg_l[5],
00763   ss_column_size : ss_exp * ss_num_rows,
00764   bits : cst[2],
00765   namespace :
00766     cstt_namespace_new(ss_mixcolumn_namespace,cst),
00767   iBits : partition_elements(take_elements(ss_column_size, bits),ss_exp),
00768   oBits : partition_elements(rest(bits, ss_column_size), ss_exp),
00769   /* First element */
00770   for i : 1 thru ss_num_rows do block([mul_vars, mul_vars_l : []],
00771     for j : ss_num_rows thru 1 step -1 do block([var_block],
00772       var_block : ss_column_size * (i-1) + ss_exp * (j-1),
00773       if ss_mixcolumns_matrix[i,j] = 1 then
00774         mul_vars : iBits[j]
00775       else block(
00776         mul_vars :
00777           generate_ss_constraint_vars(var_block + 1,var_block + ss_exp,
00778             namespace,nounify(mc)),
00779         rs : cons(
00780               cstt_new("ss_mul_cst", append(iBits[j],mul_vars),
00781                   [ss_mixcolumns_matrix[i,j],ss_base,ss_exp, ss_poly,i,j],
00782                   namespace),
00783                 rs)),
00784       mul_vars_l : cons(mul_vars, mul_vars_l)
00785     ),
00786     rs : cons(
00787       cstt_new("ss_add_cst",
00788         append(
00789           lappend(mul_vars_l),oBits[i]),[ss_num_rows], namespace),
00790       rs)
00791   ),
00792   return(rs)
00793 )$
00794 
00795 
00796 ss_mixcolumn_boolm_cstrb :
00797  [ss_mixcolumn_boolm_cstr_cstl,ss_mixcolumn_boolm_namespace,
00798   ss_mixcolumn_boolm_ns_var_l]$
00799 
00800 
00801 /* MixColumns translation as a boolean matrix. */
00802 
00803 kill(ss_mixcolumn_boolm_ns)$
00804 declare(ss_mixcolumn_boolm_ns,noun)$
00805 declare(ss_mixcolumn_boolm_ns,posfun)$
00806 ss_mixcolumn_boolm_namespace([args]) :=
00807   apply(nounify(ss_mixcolumn_boolm_ns),args)$
00808 
00809 ss_mixcolumn_boolm_ns_var_l(cst) := []$
00810 ss_mixcolumn_boolm_cstr_cstl(cst) := block(
00811   [namespace,bits,iBits, oBits, nc,rs : [],ss_arg_l, ss_column_size,
00812    ss_num_rows, ss_base, ss_exp, ss_column_size, ss_poly,
00813    ss_mixcolumns_matrix, ss_mixcolumns_boolm_l, extract_vars],
00814   ss_arg_l : cstt_args_l(cst),
00815   ss_num_rows : ss_arg_l[1],
00816   ss_base : ss_arg_l[2],
00817   ss_exp : ss_arg_l[3],
00818   ss_poly : ss_arg_l[4],
00819   ss_mixcolumns_matrix : ss_arg_l[5],
00820   ss_column_size : ss_exp * ss_num_rows,
00821   bits : cst[2],
00822   namespace :
00823     cstt_namespace_new(ss_mixcolumn_boolm_namespace,cst),
00824   iBits : take_elements(ss_column_size, bits),
00825   oBits : rest(bits, ss_column_size),
00826   ss_mixcolumns_boolm_l :
00827     ss_mixcolumn_gen_boolm(ss_base,ss_exp,ss_poly,ss_mixcolumns_matrix),
00828   ss_mixcolumns_boolm_l : args(ss_mixcolumns_boolm_l),
00829   extract_vars(V,sublist_ind) :=
00830     delete(false,
00831       map(lambda([v,i], if i = 1 then v else false),V,sublist_ind)),
00832   /* First element */
00833   for i : 1 thru ss_column_size do block(
00834     [involved_vars : extract_vars(iBits,ss_mixcolumns_boolm_l[i])],
00835     rs : cons(
00836       cstt_new("ss_add_cst",
00837         endcons(oBits[i],involved_vars),
00838         [length(involved_vars)], namespace),
00839       rs)
00840   ),
00841   return(rs)
00842 )$
00843 
00844 
00845 /*
00846    Inverse Mixcolumn
00847 
00848 */
00849 
00850 ss_inv_mixcolumn_cstrb :
00851  [ss_inv_mixcolumn_cstr_cstl,ss_inv_mixcolumn_namespace,ss_inv_mixcolumn_ns_var_l]$
00852 
00853 
00854 /* SS inv_mixcolumn namespace */
00855 kill(ss_inv_mixcolumn_ns)$
00856 declare(ss_inv_mixcolumn_ns,noun)$
00857 declare(ss_inv_mixcolumn_ns,posfun)$
00858 ss_inv_mixcolumn_namespace([args]) := apply(nounify(ss_inv_mixcolumn_ns),args)$
00859 
00860 
00861 ss_inv_mixcolumn_ns_var_l(cst) := block([vars : [],namespace,ss_arg_l,
00862   ss_column_size,ss_num_rows, ss_base, ss_exp, ss_column_size,ss_poly,
00863   ss_mixcolumns_matrix],
00864   ss_arg_l : cstt_args_l(cst),
00865   ss_num_rows : ss_arg_l[1],
00866   ss_base : ss_arg_l[2],
00867   ss_exp : ss_arg_l[3],
00868   ss_poly : ss_arg_l[4],
00869   ss_mixcolumns_matrix :
00870     ss_mixcolumns_matrix2inv_mixcolumns_matrix(ss_base,ss_exp,ss_arg_l[5]),
00871   ss_column_size : ss_exp * ss_num_rows,
00872   namespace :
00873     cstt_namespace_new(ss_inv_mixcolumn_namespace,cst),
00874   for i : 1 thru ss_num_rows do
00875     for j : 1 thru ss_num_rows do block([var_block],
00876       var_block : ss_column_size * (i-1) + ss_exp * (j-1),
00877       if ss_mixcolumns_matrix[i,j] # 1 then
00878         vars : cons(
00879           generate_ss_constraint_vars(
00880             var_block+1,var_block+ss_exp,namespace,nounify(mc)),vars)),
00881   return(lappend(vars)))$
00882 /* Returns a set of conditions representing the SS Mixcolumn operation (the 
00883    individual operation applied to a single column in SS Mixcolumns) given
00884    128 plaintext variables and 128 output variables. */
00885 ss_inv_mixcolumn_cstr_cstl(cst) := block(
00886   [namespace,bits,iBits, oBits, nc,rs : [],ss_arg_l, ss_column_size,
00887   ss_num_rows, ss_base, ss_exp, ss_column_size,
00888        ss_poly, ss_mixcolumns_matrix],
00889   ss_arg_l : cstt_args_l(cst),
00890   ss_num_rows : ss_arg_l[1],
00891   ss_base : ss_arg_l[2],
00892   ss_exp : ss_arg_l[3],
00893   ss_poly : ss_arg_l[4],
00894   ss_mixcolumns_matrix :
00895     ss_mixcolumns_matrix2inv_mixcolumns_matrix(ss_base,ss_exp,ss_arg_l[5]),
00896   ss_column_size : ss_exp * ss_num_rows,
00897   bits : cst[2],
00898   namespace :
00899     cstt_namespace_new(ss_inv_mixcolumn_namespace,cst),
00900   oBits : partition_elements(take_elements(ss_column_size, bits),ss_exp),
00901   iBits : partition_elements(rest(bits, ss_column_size), ss_exp),
00902   /* First element */
00903   for i : 1 thru ss_num_rows do block([mul_vars, mul_vars_l : []],
00904     for j : ss_num_rows thru 1 step -1 do block([var_block],
00905       var_block : ss_column_size * (i-1) + ss_exp * (j-1),
00906       if ss_mixcolumns_matrix[i,j] = 1 then
00907         mul_vars : iBits[j]
00908       else block(
00909         mul_vars :
00910           generate_ss_constraint_vars(var_block + 1,var_block + ss_exp,
00911             namespace,nounify(mc)),
00912         rs : cons(
00913               cstt_new("ss_mul_cst", append(iBits[j],mul_vars),
00914                   [ss_mixcolumns_matrix[i,j],ss_base,ss_exp, ss_poly,i,j],
00915                   namespace),
00916                 rs)),
00917       mul_vars_l : cons(mul_vars, mul_vars_l)
00918     ),
00919     rs : cons(
00920       cstt_new("ss_add_cst",
00921         append(
00922           lappend(mul_vars_l),oBits[i]),[ss_num_rows], namespace),
00923       rs)
00924   ),
00925   return(rs)
00926 )$
00927 
00928 /*
00929    Key expansion
00930 
00931 */
00932 
00933 
00934 ss_key_expansion_cstrb :
00935  [ss_key_expansion_cstr_cstl,ss_key_expansion_namespace,
00936   ss_key_expansion_ns_var_l]$
00937 
00938 /* Generates a set of unit-clauses (initially simpler than simplifying constants
00939    or making partial assignments) to set the given vars (representing the bits
00940    of SS round constants) to the round constant for round n */
00941 ss_round_constant_l(n, b, e, mod_poly) := block([rc_el,rc_l],
00942   rc_el : xreduce(lambda([a,c],ss_natmul(c,a,b,mod_poly)),
00943                create_list(2,i,1,(n -1)),1),
00944   return(nat2vec_ss(rc_el,b,e))
00945 )$
00946 
00947 /* SS key expansion namespace */
00948 kill(ss_key_expansion_ns)$
00949 declare(ss_key_expansion_ns,noun)$
00950 declare(ss_key_expansion_ns,posfun)$
00951 ss_key_expansion_namespace([args]) :=
00952   apply(nounify(ss_key_expansion_ns),args)$
00953 
00954 ss_key_expansion_ns_var_l(cst) := block(
00955   [vars : [],namespace,ss_arg_l,num_block_bits,
00956    ss_num_rounds, ss_num_columns, ss_num_rows, ss_base, ss_exp,
00957        ss_poly, ss_sbox_matrix, ss_affine_constant],
00958   ss_arg_l : cstt_args_l(cst),
00959   ss_num_rounds : ss_arg_l[1],
00960   ss_num_columns : ss_arg_l[2],
00961   ss_num_rows : ss_arg_l[3],
00962   ss_base : ss_arg_l[4],
00963   ss_exp : ss_arg_l[5],
00964   ss_poly : ss_arg_l[6],
00965   ss_sbox_matrix : ss_arg_l[7],
00966   ss_affine_constant : ss_arg_l[8],
00967   namespace : cstt_namespace_new(ss_key_expansion_namespace,cst),
00968   vars : cons(
00969     generate_ss_constraint_vars(1,ss_num_rows*ss_exp*ss_num_rounds,
00970       namespace,nounify(sb)),vars),
00971 /*  vars : cons(
00972     generate_ss_constraint_vars(1,ss_exp*ss_num_rounds,namespace,nounify(ke)),
00973     vars),*/
00974   vars : cons(
00975     generate_ss_constraint_vars(1,ss_exp*ss_num_rounds,namespace,nounify(rc)),
00976     vars),
00977   return(lappend(vars)))$
00978 /* Returns a set of conditions representing the SS keyschedule operation given
00979    128 key variables and 128 * (ss_num_rounds + 1) output variables
00980    (consecutive lots of 128 bits representing the individual round keys).
00981    
00982    The first 128 variables in the list "bits" represent the key block for the 
00983    cipher, and then the (i+1)'th consecutive 128 variables in "bits" represents
00984    the round key block for the i'th round. 
00985    
00986    */
00987 ss_key_expansion_cstr_cstl(cst) := block(
00988   [namespace,bits, n_b : 4, n_r,kBits, rkBits, nc,rs : [],
00989    sboxVars, addVars,fMat, kMat, sbox_i : 0, rc_i : 0,ss_arg_l,num_block_bits,
00990    ss_num_rounds, ss_num_columns, ss_num_rows, ss_base, ss_exp,
00991    ss_poly, ss_sbox_matrix, ss_affine_constant, gv, var_offset],
00992   ss_arg_l : cstt_args_l(cst),
00993   ss_num_rounds : ss_arg_l[1],
00994   ss_num_columns : ss_arg_l[2],
00995   ss_num_rows : ss_arg_l[3],
00996   ss_base : ss_arg_l[4],
00997   ss_exp : ss_arg_l[5],
00998   ss_poly : ss_arg_l[6],
00999   ss_sbox_matrix : ss_arg_l[7],
01000   ss_affine_constant : ss_arg_l[8],
01001   num_block_bits : ss_exp * ss_num_columns * ss_num_rows,
01002   bits : cst[2],
01003   namespace : cstt_namespace_new(ss_key_expansion_namespace,cst),
01004   /* Primary Variables */
01005   kBits : take_elements(num_block_bits,bits),
01006   rkBits : rest(bits,num_block_bits),
01007   fBits : take_elements(num_block_bits,rkBits),
01008   /* Split into columns */
01009   cols : partition_elements(
01010     partition_elements(partition_elements(rkBits,ss_exp),ss_num_rows),
01011     ss_num_columns),
01012   kMat : partition_elements(partition_elements(kBits,ss_exp),ss_num_rows),
01013   fMat : partition_elements(partition_elements(fBits,ss_exp),ss_num_rows),
01014   gvar : lambda([[args_]], apply(generate_ss_constraint_vars,args_)),
01015   /* Make first round key equal */
01016   for j : 1 thru ss_num_columns do
01017     for i : 1 thru ss_num_rows do
01018       rs : cons(
01019         cstt_new("eq_cst", append(kMat[j][i], fMat[j][i]), [],namespace),rs),
01020   /* First column of each row */
01021   for round : 2 thru ss_num_rounds + 1 do (
01022     var_offset : ((round-2)*ss_num_rows)*ss_exp,
01023     sboxVars : gvar(var_offset +1, var_offset+ss_exp, namespace, nounify(sb)),
01024     rs : cons(
01025       cstt_new("ss_sbox_cst",
01026         append(cols[round-1][ss_num_columns][mod(1,ss_num_rows)+1], sboxVars),
01027         [ss_base, ss_exp,ss_poly, ss_sbox_matrix, ss_affine_constant,
01028         sbox_i : sbox_i + 1],
01029         namespace),
01030       rs),
01031     var_offset : (round-2)*(ss_exp), 
01032     rcVars : gvar(var_offset + 1, var_offset + ss_exp, namespace, nounify(rc)),
01033     rs : cons(
01034       cstt_new("const_cst",
01035         rcVars,
01036         cons(rc_i : rc_i + 1,
01037           ss_round_constant_l(round-1,ss_base, ss_exp, ss_poly)),
01038         namespace),
01039       rs),
01040     if ss_num_columns > 1 then
01041       rs : cons(
01042         cstt_new("ss_add_cst", 
01043           append(rcVars, cols[round-1][1][1], sboxVars, cols[round][1][1]),
01044           [3],namespace),
01045         rs)
01046     else
01047       rs : cons(
01048         cstt_new("ss_add_cst", 
01049           append(rcVars,sboxVars, cols[round][1][1]), [],namespace),
01050         rs),
01051     for i : 2 thru ss_num_rows do block(
01052       [offset: ((round-2)*ss_num_rows + (i-1))*ss_exp],
01053       sboxVars : gvar(offset + 1, offset + ss_exp, namespace, nounify(sb)),
01054       rs : cons(
01055         cstt_new("ss_sbox_cst", 
01056           append(
01057             cols[round-1][ss_num_columns][mod(i,ss_num_rows)+1], sboxVars),
01058           [ss_base, ss_exp,ss_poly, ss_sbox_matrix, ss_affine_constant,
01059           sbox_i : sbox_i + 1],namespace),
01060         rs),
01061       if ss_num_columns > 1 then
01062         rs : cons(
01063           cstt_new("ss_add_cst", 
01064             append(cols[round-1][1][i],sboxVars, cols[round][1][i]),
01065             [],namespace),
01066           rs)
01067       else
01068         rs : cons(
01069           cstt_new("eq_cst", append(sboxVars, cols[round][1][i]), [], namespace), rs)
01070     ),
01071     for column : 2 thru ss_num_columns do block(
01072       for i : 1 thru ss_num_rows do 
01073         rs : cons(
01074           cstt_new("ss_add_cst",
01075             append(
01076               cols[round][column-1][i],
01077               cols[round-1][column][i],
01078               cols[round][column][i]), [],namespace), rs)
01079       )
01080     ),
01081   return(rs)
01082 )$
01083 
01084 
01085 /* ****************************************
01086    * CNF Translation functions            *
01087    ****************************************
01088 */
01089 
01090 ss_mul_ts_CNF : sm2hm({})$
01091 ss_mul_ts_gen(p, b,e,mod_poly) := block([hash_key : [p+1,b,e,mod_poly]],
01092   if ev_hm_d(ss_mul_ts_CNF,hash_key,false) = false then
01093     block([plus16 : lambda([x],x+2*e),
01094       mul_dnf : ssmult_fulldnf_fcs(p,b,e,mod_poly)],
01095       set_hm(ss_mul_ts_CNF,hash_key,
01096         dualts_fcl(
01097           [listify(mul_dnf[1]),
01098           sort(
01099             listify(mul_dnf[2]),
01100             lambda([c,d], is(
01101                 rank_lex_ksubsets(map(plus16,c),e*4) < 
01102                 rank_lex_ksubsets(map(plus16,d),e*4)))
01103             )]
01104           )),
01105       return(ev_hm(ss_mul_ts_CNF,hash_key))
01106       ) else ev_hm(ss_mul_ts_CNF,hash_key))$
01107 
01108 ss_sbox_ts_CNF : sm2hm({})$
01109 ss_sbox_ts_gen(b,e,mod_poly) := block([hash_key : [b,e,mod_poly]],
01110   if ev_hm_d(ss_sbox_ts_CNF,hash_key,false) = false then
01111     block([plus16 : lambda([x],x+e*2),
01112       sbox_dnf : ss_sbox_fulldnf_fcs(b,e,mod_poly)],
01113       set_hm(ss_sbox_ts_CNF,hash_key,
01114         dualts_fcl(
01115           [listify(sbox_dnf[1]),
01116           sort(
01117             listify(sbox_dnf[2]),
01118             lambda([c,d], is(
01119                 rank_lex_ksubsets(map(plus16,c),e*4) < 
01120                 rank_lex_ksubsets(map(plus16,d),e*4)))
01121             )]
01122           )), 
01123         return(ev_hm(ss_sbox_ts_CNF,hash_key))
01124         ) else ev_hm(ss_sbox_ts_CNF,hash_key))$
01125 
01126 ss_mixcolumn_ts_CNF : sm2hm({})$
01127 ss_mixcolumn_ts_gen(b,e,mod_poly,mixcolumns_matrix) := block(
01128   [hash_key : [b,e,mod_poly,mixcolumns_matrix],num_rows,num_col_bits],
01129   num_rows : length(mixcolumns_matrix),
01130   num_col_bits : 2*num_rows*e,
01131   if ev_hm_d(ss_mixcolumn_ts_CNF,hash_key,false) = false then
01132     block([plus16 : lambda([x],x+num_col_bits),
01133       mc_dnf :
01134         fcl2fcs(cl2fcl(bf2relation_fulldnf_cl(lambda([V],
01135             ss_mixcolumn_gen_bf(V,b,e,mod_poly,mixcolumns_matrix)),
01136           e*num_rows)))],
01137       set_hm(ss_mixcolumn_ts_CNF,hash_key,
01138         dualts_fcl(
01139           [listify(mc_dnf[1]),
01140           sort(
01141             listify(mc_dnf[2]),
01142             lambda([c,d], is(
01143                 rank_lex_ksubsets(map(plus16,c),2*num_col_bits) < 
01144                 rank_lex_ksubsets(map(plus16,d),2*num_col_bits)))
01145             )]
01146           )),
01147       return(ev_hm(ss_mixcolumn_ts_CNF,hash_key))
01148       ) else ev_hm(ss_mixcolumn_ts_CNF,hash_key))$
01149 
01150 ss_round_column_ts_CNF : sm2hm({})$
01151 ss_round_column_ts_gen(b,e,mod_poly,ss_sbox_matrix,
01152                        ss_affine_constant,mixcolumns_matrix) := block(
01153   [hash_key : [b,e,mod_poly,ss_sbox_matrix,
01154                ss_affine_constant,mixcolumns_matrix],num_rows,num_col_bits],
01155   num_rows : length(mixcolumns_matrix),
01156   num_col_bits : 2*num_rows*e,
01157   if ev_hm_d(ss_round_column_ts_CNF,hash_key,false) = false then
01158     block([plus16 : lambda([x],x+num_col_bits),
01159       mc_dnf :
01160         fcl2fcs(cl2fcl(bf2relation_fulldnf_cl(lambda([V],
01161             ss_round_column_gen_bf(V,b,e,mod_poly,mixcolumns_matrix,
01162               lambda([p],ss_sbox_gen(p,b,e,mod_poly,ss_sbox_matrix,
01163                        ss_affine_constant)))),
01164           e*num_rows)))],
01165       set_hm(ss_round_column_ts_CNF,hash_key,
01166         dualts_fcl(
01167           [listify(mc_dnf[1]),
01168           sort(
01169             listify(mc_dnf[2]),
01170             lambda([c,d], is(
01171                 rank_lex_ksubsets(map(plus16,c),2*num_col_bits) < 
01172                 rank_lex_ksubsets(map(plus16,d),2*num_col_bits)))
01173             )]
01174           )),
01175       return(ev_hm(ss_round_column_ts_CNF,hash_key))
01176       ) else ev_hm(ss_round_column_ts_CNF,hash_key))$
01177 
01178 ss_sbox_w_mul_ts_CNF : sm2hm({})$
01179 ss_sbox_w_mul_ts_gen(p, b,e,mod_poly) := block(
01180   [hash_key : [p,b,e,mod_poly]],
01181   if ev_hm_d(ss_sbox_w_mul_ts_CNF,hash_key,false) = false then
01182     block([plus16 : lambda([x],x+2*e),
01183       mc_dnf :
01184         fcl2fcs(cl2fcl(bf2relation_fulldnf_cl(lambda([V],
01185             ss_sbox_w_mul_bf(V,p,b,e)),
01186           e)))],
01187       set_hm(ss_sbox_w_mul_ts_CNF,hash_key,
01188         dualts_fcl(
01189           [listify(mc_dnf[1]),
01190           sort(
01191             listify(mc_dnf[2]),
01192             lambda([c,d], is(
01193                 rank_lex_ksubsets(map(plus16,c),e*4) < 
01194                 rank_lex_ksubsets(map(plus16,d),e*4)))
01195             )]
01196           )),
01197       return(ev_hm(ss_sbox_w_mul_ts_CNF,hash_key))
01198       ) else ev_hm(ss_sbox_w_mul_ts_CNF,hash_key))$
01199 
01200 /* Returns a list of CNF clauses representing the sbox relation
01201    given the appropriate sbox constraint ("ss_sbox_cst" with 16 variables
01202    in the constraint).
01203 
01204    The clauses returned are those originally produced manually through
01205    experimentation into finding small Sbox representations (see plans
01206    and SboxMinCNF).
01207 */
01208 ss_sbox_pi_cst_cl(cst) := block([ss_arg_l,
01209   ss_base, ss_exp,ss_poly, ss_sbox_matrix, ss_affine_constant],
01210   ss_arg_l : cstt_args_l(cst),  ss_exp : ss_arg_l[2],
01211   return(
01212     rename_fcl(map(listify,ev_hm(ss_sbox_cnfs,ss_exp)),cst[2])[2])
01213   )$
01214 
01215 /* Returns the canonical CNF clauses representing the sbox relation
01216    given the appropriate sbox constraint ("ss_sbox_cst" with 16 variables
01217    in the constraint).
01218 */
01219 ss_sbox_full_cst_cl(cst) := block([ss_arg_l, ss_exp],
01220   ss_arg_l : cstt_args_l(cst),  ss_exp : ss_arg_l[2],
01221   return(
01222     rename_fcl(
01223       fcs2fcl(ss_sbox_fullcnf_fcs(2,ss_exp,ss_polynomial(2,ss_exp))),
01224       cst[2])[2])
01225   )$
01226 
01227 /* Takes an "ss_sbox_cst" constraint with the small scale base, exponent,
01228    modulo polynomial, sbox_matrix and affine constant and returns the
01229    smallest known (in terms of number of clauses) r_1 base for the AES Sbox
01230    with the given parameters.
01231 
01232    Note, this result may be undefined if an r_1 base has not be computed
01233    for the given parameters.
01234 */
01235 ss_sbox_rbase_cst_cl(cst) := block([ss_arg_l,
01236   ss_base, ss_exp,ss_poly, ss_sbox_matrix, ss_affine_constant],
01237   ss_arg_l : cstt_args_l(cst),  ss_exp : ss_arg_l[2],
01238   return(
01239     rename_fcl(map(listify,ev_hm(ss_sbox_rbase_cnfs,ss_exp)),cst[2])[2])
01240   )$
01241 
01242 
01243 /* SS sbox namespace */
01244 kill(ss_sbox_ts_ns)$
01245 declare(ss_sbox_ts_ns,noun)$
01246 declare(ss_sbox_ts_ns,posfun)$
01247 ss_sbox_ts_namespace([args]) :=
01248   apply(nounify(ss_sbox_ts_ns),args)$
01249 
01250 /* Given an "ss_sbox_cst" constraint, returns the new variables
01251    introduced by "ss_sbox_ts_cst_cl" when given this constraint. */
01252 ss_sbox_ts_var_l(cst) := block(
01253   [bits : cst[2],namespace],
01254   namespace : cstt_namespace_new(ss_sbox_ts_namespace,cst),
01255   generate_ss_constraint_vars(1,2^(length(bits)/2), namespace,
01256     nounify(sbox_ts)))$
01257 
01258 /* Given an "ss_sbox_cst" constraint, returns a clause list
01259    generated by taking the canonical translation from DNF to CNF
01260    of the SS Sbox.
01261 */
01262 ss_sbox_ts_cst_cl(cst) := block(
01263   [bits : cst[2],namespace,ss_arg_l,
01264   ss_base, ss_exp,ss_poly, ss_sbox_matrix, ss_affine_constant],
01265   ss_arg_l : cstt_args_l(cst),
01266   ss_base : ss_arg_l[1],
01267   ss_exp : ss_arg_l[2],
01268   ss_poly : ss_arg_l[3],
01269   namespace : cstt_namespace_new(ss_sbox_ts_namespace,cst),
01270   sbox : ss_sbox_ts_gen(ss_base,ss_exp,ss_poly),
01271   vars : append(bits,
01272     generate_ss_constraint_vars(1,2^(length(bits)/2), namespace,
01273       nounify(sbox_ts))),
01274   cnf : rename_fcl(sbox,vars),
01275   cnf[2])$
01276 
01277 /* Sbox and multiplication operations as a single box: */
01278 
01279 kill(ss_sbox_w_mul_ts_ns)$
01280 declare(ss_sbox_w_mul_ts_ns,noun)$
01281 declare(ss_sbox_w_mul_ts_ns,posfun)$
01282 ss_sbox_w_mul_ts_namespace([args]) :=
01283   apply(nounify(ss_sbox_w_mul_ts_ns),args)$
01284 
01285 ss_sbox_w_mul_ts_var_l(cst) := block([bits : cst[2],namespace],
01286   namespace : cstt_namespace_new(ss_sbox_w_mul_ts_namespace,cst),
01287   generate_ss_constraint_vars(1,2^(length(bits)/2), namespace,nounify(sbox_w_mul_ts)))$
01288 
01289 ss_sbox_w_mul_full_cst_cl(cst) := block(
01290   [bits : cst[2],namespace,ss_arg_l,ss_base,ss_exp,ss_poly,ss_elem],
01291   ss_arg_l : cstt_args_l(cst),
01292   ss_elem : ss_arg_l[1],
01293   ss_base : ss_arg_l[2],
01294   ss_exp : ss_arg_l[3],
01295   ss_poly : ss_arg_l[4],
01296   namespace : cstt_namespace_new(ss_sbox_w_mul_ts_namespace,cst),
01297   rename_fcl(
01298     fcs2fcl(
01299       bf2relation_fullcnf_fcs(
01300         lambda([V],ss_sbox_w_mul_bf(V,ss_elem,ss_base,ss_exp)),ss_exp)),
01301     append(bits))[2])$
01302 
01303 ss_sbox_w_mul_ts_cst_cl(cst) := block(
01304   [bits : cst[2],namespace,ss_arg_l,ss_base,ss_exp,ss_poly,ss_elem],
01305   ss_arg_l : cstt_args_l(cst),
01306   ss_elem : ss_arg_l[1],
01307   ss_base : ss_arg_l[2],
01308   ss_exp : ss_arg_l[3],
01309   ss_poly : ss_arg_l[4],
01310   namespace : cstt_namespace_new(ss_sbox_w_mul_ts_namespace,cst),
01311   rename_fcl(ss_sbox_w_mul_ts_gen(ss_elem, ss_base, ss_exp, ss_poly),
01312     append(bits,
01313       generate_ss_constraint_vars(1,2^(length(bits)/2),
01314         namespace,nounify(sbox_w_mul_ts))))[2])$
01315 
01316 /* Takes an "ss_mul_cst" constraint with, as arguments, the field element e as
01317    a polynomial, the small scale base, exponent, modulo polynomial, and
01318    returns the smallest known (in terms of number of clauses) CNF for the
01319    multiplication by AES field element e with the given parameters. The CNF
01320    has as it's variables the variables given by the input constraint.
01321 */
01322 ss_mul_pi_cst_cl(cst) := block([ss_arg_l,ss_element,
01323   ss_base, ss_exp,ss_poly],
01324   ss_arg_l : cstt_args_l(cst),
01325   ss_element : ss_arg_l[1],
01326   ss_base : ss_arg_l[2],
01327   ss_exp : ss_arg_l[3],
01328   ss_poly : ss_arg_l[4],
01329   return(
01330     rename_fcl(map(listify,ev_hm(ss_field_cnfs,
01331           [ss_exp,poly2nat(ss_element,ss_base)])),
01332       cst[2])[2])
01333   )$
01334 
01335 
01336 ss_mul_full_cst_cl(cst) := block([ss_arg_l,ss_element,
01337   ss_base, ss_exp,ss_poly],
01338   ss_arg_l : cstt_args_l(cst),
01339   ss_element : ss_arg_l[1],
01340   ss_base : ss_arg_l[2],
01341   ss_exp : ss_arg_l[3],
01342   ss_poly : ss_arg_l[4],
01343   return(
01344     rename_fcl(
01345       fcs2fcl(ssmult_fullcnf_fcs(poly2nat(ss_element,ss_base), ss_base,ss_exp, ss_poly)),
01346       cst[2])[2])
01347   )$
01348 
01349 /* Returns a list of CNF clauses representing the multiplication by 02
01350    given the appropriate constraint ("ss_mul2_cst" with 16 variables
01351    in the constraint).
01352 
01353    The clauses returned are those originally produced manually through
01354    experimentation into finding small Sbox representations (see plans
01355    and FieldMul2CNF).
01356 */
01357 /* Takes an "ss_mul_cst" constraint with, as arguments, the field element e as
01358    a polynomial, the small scale base, exponent, modulo polynomial, and
01359    returns the smallest known (in terms of number of clauses) r_1 base for the
01360    AES field element e with the given parameters. The CNF has as it's
01361    variables the variables given by the input constraint.
01362 */
01363 ss_mul_rbase_cst_cl(cst) := block([ss_arg_l,ss_element,
01364   ss_base, ss_exp,ss_poly],
01365   ss_arg_l : cstt_args_l(cst),
01366   ss_element : ss_arg_l[1],
01367   ss_base : ss_arg_l[2],
01368   ss_exp : ss_arg_l[3],
01369   ss_poly : ss_arg_l[4],
01370   return(
01371     rename_fcl(map(listify,ev_hm(ss_field_rbase_cnfs,
01372           [ss_exp,poly2nat(ss_element,ss_base)])),
01373       cst[2])[2])
01374   )$
01375 
01376 kill(ss_mul_ts_ns)$
01377 declare(ss_mul_ts_ns,noun)$
01378 declare(ss_mul_ts_ns,posfun)$
01379 ss_mul_ts_namespace([args]) :=
01380   apply(nounify(ss_mul_ts_ns),args)$
01381 
01382 /* Given an "ss_mul_cst" constraint, returns the new variables
01383    introduced by "ss_mul_ts_cst_cl" when given this constraint. */
01384 ss_mul_ts_var_l(cst) := block([bits : cst[2],namespace],
01385   namespace : cstt_namespace_new(ss_mul_ts_namespace,cst),
01386   generate_ss_constraint_vars(1,2^(length(bits)/2), namespace,nounify(mul_ts)))$
01387 
01388 /* Returns a list of CNF clauses representing the multiplication by 02
01389    given the appropriate constraint ("ss_mul2_cst" with 16 variables
01390    in the constraint).
01391 
01392    The clauses returned are those given by the canonical translation
01393    using new variables. */
01394 /* Takes an "ss_mul_cst" constraint with, as arguments, the field element e as
01395    a polynomial, the small scale base, exponent, modulo polynomial, and
01396    returns the canonical translation for multiplication by the AES field
01397    element e with the given parameters. 
01398 */
01399 ss_mul_ts_cst_cl(cst) := block(
01400   [bits : cst[2],namespace,ss_arg_l,ss_base,ss_exp,ss_poly,ss_element],
01401   ss_arg_l : cstt_args_l(cst),
01402   ss_element : ss_arg_l[1],
01403   ss_base : ss_arg_l[2],
01404   ss_exp : ss_arg_l[3],
01405   ss_poly : ss_arg_l[4],
01406   namespace : cstt_namespace_new(ss_mul_ts_namespace,cst),
01407   rename_fcl(ss_mul_ts_gen(poly2nat(ss_element,ss_base),ss_base, ss_exp, ss_poly),
01408     append(bits,
01409       generate_ss_constraint_vars(1,2^(length(bits)/2),
01410         namespace,nounify(mul_ts))))[2])$
01411 
01412 
01413 /* MixColumns translation using the canonical translation: */
01414 
01415 kill(ss_mixcolumn_ts_ns)$
01416 declare(ss_mixcolumn_ts_ns,noun)$
01417 declare(ss_mixcolumn_ts_ns,posfun)$
01418 ss_mixcolumn_ts_namespace([args]) :=
01419   apply(nounify(ss_mixcolumn_ts_ns),args)$
01420 
01421 ss_mixcolumn_ts_var_l(cst) := block([bits : cst[2],namespace],
01422   namespace : cstt_namespace_new(ss_mixcolumn_ts_namespace,cst),
01423   generate_ss_constraint_vars(1,2^(length(bits)/2), namespace,nounify(mixcolumn_ts)))$
01424 
01425 ss_mixcolumn_ts_cst_cl(cst) := block(
01426   [bits : cst[2],namespace,ss_arg_l,ss_base,ss_exp,ss_poly,ss_element],
01427   ss_arg_l : cstt_args_l(cst),
01428   ss_num_rows : ss_arg_l[1],
01429   ss_base : ss_arg_l[2],
01430   ss_exp : ss_arg_l[3],
01431   ss_poly : ss_arg_l[4],
01432   ss_mixcolumns_matrix : ss_arg_l[5],
01433   namespace : cstt_namespace_new(ss_mixcolumn_ts_namespace,cst),
01434   rename_fcl(ss_mixcolumn_ts_gen(ss_base, ss_exp, ss_poly,ss_mixcolumns_matrix),
01435     append(bits,
01436       generate_ss_constraint_vars(1,2^(length(bits)/2),
01437         namespace,nounify(mixcolumn_ts))))[2])$
01438 
01439 ss_mixcolumn_full_cst_cl(cst) := block([ss_arg_l,ss_base,ss_exp,ss_poly,
01440    ss_element, ss_sbox_matrix, ss_sbox_affine_constant, ss_mixcolumns_matrix,
01441    ss_num_rows],
01442   ss_arg_l : cstt_args_l(cst),
01443   ss_num_rows : ss_arg_l[1],
01444   ss_base : ss_arg_l[2],
01445   ss_exp : ss_arg_l[3],
01446   ss_poly : ss_arg_l[4],
01447   ss_mixcolumns_matrix : ss_arg_l[5],
01448   return(
01449     rename_fcl(
01450       fcs2fcl(bf2relation_fullcnf_fcs(
01451           lambda([V], ss_mixcolumn_gen_bf(V,ss_base,ss_exp,ss_poly,ss_mixcolumns_matrix)),
01452           ss_exp*ss_num_rows)),
01453       cst[2])[2])
01454   )$
01455 
01456 /* Translating the whole round on one column:
01457 */
01458 
01459 ss_round_column_pi_cst_cl(cst) := block([ss_arg_l,ss_base,ss_exp,ss_poly,
01460    ss_element, ss_sbox_matrix, ss_sbox_affine_constant, ss_mixcolumns_matrix,
01461    ss_num_rows],
01462   ss_arg_l : cstt_args_l(cst),
01463   ss_num_rows : ss_arg_l[1],
01464   ss_base : ss_arg_l[2],
01465   ss_exp : ss_arg_l[3],
01466   ss_poly : ss_arg_l[4],
01467   ss_sbox_matrix : ss_arg_l[5],
01468   ss_sbox_affine_constant : ss_arg_l[6],
01469   ss_mixcolumns_matrix : ss_arg_l[7],
01470   return(
01471     rename_fcl(map(listify,ev_hm(ss_round_column_cnfs,
01472           [ss_exp,ss_num_rows])),
01473       cst[2])[2])
01474   )$
01475 
01476 ss_round_column_full_cst_cl(cst) := block([ss_arg_l,ss_base,ss_exp,ss_poly,
01477    ss_element, ss_sbox_matrix, ss_sbox_affine_constant, ss_mixcolumns_matrix,
01478    ss_num_rows],
01479   ss_arg_l : cstt_args_l(cst),
01480   ss_num_rows : ss_arg_l[1],
01481   ss_base : ss_arg_l[2],
01482   ss_exp : ss_arg_l[3],
01483   ss_poly : ss_arg_l[4],
01484   ss_sbox_matrix : ss_arg_l[5],
01485   ss_sbox_affine_constant : ss_arg_l[6],
01486   ss_mixcolumns_matrix : ss_arg_l[7],
01487   return(
01488     rename_fcl(
01489       fcs2fcl(bf2relation_fullcnf_fcs(
01490           lambda([V], ss_round_column_gen_bf(V,ss_base,ss_exp,ss_poly,ss_mixcolumns_matrix)),
01491           ss_exp*ss_num_rows)),
01492       cst[2])[2])
01493   )$
01494 
01495 ss_round_column_pi_cst_cl(cst) := block([ss_arg_l,ss_base,ss_exp,ss_poly,
01496    ss_element, ss_sbox_matrix, ss_sbox_affine_constant, ss_mixcolumns_matrix,
01497    ss_num_rows],
01498   ss_arg_l : cstt_args_l(cst),
01499   ss_num_rows : ss_arg_l[1],
01500   ss_base : ss_arg_l[2],
01501   ss_exp : ss_arg_l[3],
01502   ss_poly : ss_arg_l[4],
01503   ss_sbox_matrix : ss_arg_l[5],
01504   ss_sbox_affine_constant : ss_arg_l[6],
01505   ss_mixcolumns_matrix : ss_arg_l[7],
01506   return(
01507     rename_fcl(map(listify,ev_hm(ss_round_column_cnfs,
01508           [ss_exp,ss_num_rows])),
01509       cst[2])[2])
01510   )$
01511 
01512 ss_round_column_rbase_cst_cl(cst) := block([ss_arg_l,ss_base,ss_exp,ss_poly,
01513    ss_element, ss_sbox_matrix, ss_sbox_affine_constant, ss_mixcolumns_matrix,
01514    ss_num_rows],
01515   ss_arg_l : cstt_args_l(cst),
01516   ss_num_rows : ss_arg_l[1],
01517   ss_base : ss_arg_l[2],
01518   ss_exp : ss_arg_l[3],
01519   ss_poly : ss_arg_l[4],
01520   ss_sbox_matrix : ss_arg_l[5],
01521   ss_sbox_affine_constant : ss_arg_l[6],
01522   ss_mixcolumns_matrix : ss_arg_l[7],
01523   return(
01524     rename_fcl(map(listify,ev_hm(ss_round_column_rbase_cnfs,
01525           [ss_exp,ss_num_rows])),
01526       cst[2])[2])
01527   )$
01528 
01529 kill(ss_round_column_ts_ns)$
01530 declare(ss_round_column_ts_ns,noun)$
01531 declare(ss_round_column_ts_ns,posfun)$
01532 ss_round_column_ts_namespace([args]) :=
01533   apply(nounify(ss_round_column_ts_ns),args)$
01534 
01535 ss_round_column_ts_var_l(cst) := block([bits : cst[2],namespace],
01536   namespace : cstt_namespace_new(ss_round_column_ts_namespace,cst),
01537   generate_ss_constraint_vars(1,2^(length(bits)/2), namespace,nounify(round_column_ts)))$
01538 
01539 ss_round_column_ts_cst_cl(cst) := block(
01540   [bits : cst[2],namespace,ss_arg_l,ss_base,ss_exp,ss_poly,ss_element,
01541    ss_sbox_matrix, ss_sbox_affine_constant, ss_mixcolumns_matrix,ss_num_rows],
01542   ss_arg_l : cstt_args_l(cst),
01543   ss_num_rows : ss_arg_l[1],
01544   ss_base : ss_arg_l[2],
01545   ss_exp : ss_arg_l[3],
01546   ss_poly : ss_arg_l[4],
01547   ss_sbox_matrix : ss_arg_l[5],
01548   ss_sbox_affine_constant : ss_arg_l[6],
01549   ss_mixcolumns_matrix : ss_arg_l[7],
01550   namespace : cstt_namespace_new(ss_round_column_ts_namespace,cst),
01551   rename_fcl(
01552     ss_round_column_ts_gen(ss_base, ss_exp, ss_poly,
01553                            ss_sbox_matrix,
01554                            ss_sbox_affine_constant,
01555                            ss_mixcolumns_matrix),
01556     append(bits,
01557       generate_ss_constraint_vars(1,2^(length(bits)/2),
01558         namespace,nounify(round_column_ts))))[2])$
01559 
01560