OKlibrary  0.2.1.6
ConstraintTemplateRewriteRules.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 28.9.2010 (Swansea) */
00002 /* Copyright 2010, 2011, 2013 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 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/SboxAnalysis.mac")$
00024 
00025 kill(f)$
00026 
00027 
00028 /* ***********************************************
00029    * Constraint template rewrite translation     *
00030    ***********************************************
00031 */
00032 
00033 oktest_generate_aes_constraint_vars(f) := block(
00034   for i : 0 thru 5 do
00035     assert(f(i,i-1,lambda([a],a),nounify(id)) = []),
00036   for i : 0 thru 5 do
00037     assert(f(i,i, lambda([a],a),nounify(id)) = [aes_v(i,nounify(id))]),
00038  for i : 0 thru 5 do
00039     assert(f(i,i, nounify(n),nounify(id)) =
00040       [nounify(n)(aes_v(i,nounify(id)))]),
00041   assert(f(1,2, nounify(n),nounify(id)) =
00042     [nounify(n)(aes_v(1,nounify(id))),nounify(n)(aes_v(2,nounify(id)))]),
00043   true)$
00044 
00045 /* ***********************************************
00046    * Constraint template rewrite functions       *
00047    ***********************************************
00048 */
00049 
00050 okltest_aes_ns_var_l(f) := block([cst],
00051   cst : ["aes_cst",create_list(i,i,1,384),1,lambda([a],a)],
00052   namespace : cstt_namespace_new(aes_namespace, cst),
00053   assert(
00054     f(cst) =
00055     append(
00056       map(
00057         lambda([a],namespace(aes_var(a,nounify(o)))),
00058         create_list(i,i,1,128)),
00059       map(
00060         lambda([a],namespace(aes_var(a,nounify(k)))),
00061         create_list(i,i,1,256)))),
00062   true)$
00063 
00064 okltest_aes_cstr_cstl(f) := block([ctl,ct],
00065   cst : ["aes_cst",create_list(i,i,1,384),1,nounify(n)],
00066   namespace : cstt_namespace_new(aes_namespace, cst),
00067   ctl : f(cst),
00068   assert(map(first,ctl) =
00069     ["aes_round_cst","aes_add_cst","aes_key_expansion_cst"]),
00070   assert(map(lambda([a],length(a[2])), ctl) = [384,384,384]),
00071   assert(every_s(lambda([a], is(last(a) =
00072           namespace)),ctl)),
00073   assert(ctl[1][2][50] =
00074     namespace(aes_v(50,nounify(o)))),
00075   assert(ctl[2][2][200] =
00076     namespace(aes_v(72,nounify(k)))),
00077   if oklib_test_level = 0 then return(true),
00078   assert(
00079     setify(aes_ns_var_l(cst)) =
00080     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00081       setify(create_list(i,i,1,384)))),
00082   true)$
00083 
00084 okltest_aes_round_ns_var_l(f) := block([cst],
00085   cst : ["aes_round_cst",create_list(i,i,1,384),lambda([a],a)],
00086   namespace : cstt_namespace_new(aes_round_namespace, cst),
00087   assert(
00088     f(cst) =
00089     append(
00090       map(
00091         lambda([a],namespace(aes_var(a,nounify(mo)))),
00092         create_list(i,i,1,128)),
00093       map(
00094         lambda([a],namespace(aes_var(a,nounify(ro)))),
00095         create_list(i,i,1,128)),
00096       map(
00097         lambda([a],namespace(aes_var(a,nounify(so)))),
00098         create_list(i,i,1,128)))),
00099   true)$
00100 
00101 okltest_aes_round_cstr_cstl(f) := block([cst],
00102   cst : ["aes_round_cst",create_list(i,i,1,384),nounify(n)],
00103   namespace : cstt_namespace_new(aes_round_namespace, cst),
00104   ctl : f(cst),
00105   assert(map(first,ctl) =
00106     ["aes_add_cst","aes_mixcolumns_cst","aes_shiftrows_cst",
00107      "aes_subbytes_cst"]),
00108   assert(map(lambda([a],length(a[2])), ctl) = [384,256,256,256]),
00109     assert(every_s(lambda([a], is(last(a) =
00110           namespace)),ctl)),
00111   if oklib_test_level = 0 then return(true),
00112   assert(
00113     setify(aes_round_ns_var_l(cst)) =
00114     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00115       setify(create_list(i,i,1,384)))),
00116   true)$
00117 
00118 
00119 okltest_aes_final_round_ns_var_l(f) := block([cst],
00120   cst : ["aes_final_round_cst",create_list(i,i,1,384),lambda([a],a)],
00121   namespace : cstt_namespace_new(aes_final_round_namespace, cst),
00122   assert(
00123     f(cst) =
00124     append(
00125       map(
00126         lambda([a],namespace(aes_var(a,nounify(ro)))),
00127         create_list(i,i,1,128)),
00128       map(
00129         lambda([a],namespace(aes_var(a,nounify(so)))),
00130         create_list(i,i,1,128)))),
00131   true)$
00132 
00133 
00134 okltest_aes_final_round_cstr_cstl(f) := block([cst],
00135   cst : ["aes_final_round_cst",create_list(i,i,1,384),nounify(n)],
00136   namespace : cstt_namespace_new(aes_final_round_namespace, cst),
00137   ctl : f(cst),
00138   assert(map(first,ctl) =
00139     ["aes_add_cst","aes_shiftrows_cst","aes_subbytes_cst"]),
00140   assert(map(lambda([a],length(a[2])), ctl) = [384,256,256]),
00141   assert(every_s(lambda([a], is(last(a) =
00142           namespace)),ctl)),
00143   if oklib_test_level = 0 then return(true),
00144   assert(
00145     setify(aes_final_round_ns_var_l(cst)) =
00146     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00147       setify(create_list(i,i,1,384)))),
00148   true)$
00149 
00150 
00151 okltest_aes_subbytes_ns_var_l(f) := block([cst],
00152   cst : ["aes_subbytes_cst",create_list(i,i,1,384),nounify(n)],
00153   assert(f(cst) = []),
00154   true)$
00155 
00156 
00157 okltest_aes_subbytes_cstr_cstl(f) := block([cst],
00158   cst : ["aes_subbytes_cst",create_list(i,i,1,256),nounify(n)],
00159   namespace : cstt_namespace_new(aes_subbytes_namespace, cst),
00160   ctl : f(cst),
00161   assert(map(first,ctl) = create_list("aes_sbox_cst",i,1,16)),
00162   assert(map(lambda([a],length(a[2])), ctl) = create_list(16,i,1,16)),
00163   assert(every_s(lambda([a], is(last(a) =
00164           namespace)),ctl)),
00165   if oklib_test_level = 0 then return(true),
00166   assert(
00167     setify(aes_subbytes_ns_var_l(cst)) =
00168     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00169       setify(create_list(i,i,1,384)))),
00170   true)$
00171 
00172 
00173 okltest_aes_shiftrows_ns_var_l(f) := block([cst],
00174   cst : ["aes_shiftrows_cst",create_list(i,i,1,384),nounify(n)],
00175   assert(f(cst) = []),
00176   true)$
00177 
00178 
00179 okltest_aes_shiftrows_cstr_cstl(f) := block([cst],
00180   cst : ["aes_shiftrows_cst",create_list(i,i,1,256),nounify(n)],
00181   namespace : cstt_namespace_new(aes_shiftrows_namespace, cst),
00182   ctl : f(cst),
00183   assert(map(first,ctl) = create_list("eq_cst",i,1,128)),
00184   assert(map(lambda([a],length(a[2])), ctl) = create_list(2,i,1,128)),
00185   assert(every_s(lambda([a], is(last(a) =
00186           namespace)),ctl)),
00187   if oklib_test_level = 0 then return(true),
00188   assert(
00189     setify(aes_shiftrows_ns_var_l(cst)) =
00190     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00191       setify(create_list(i,i,1,384)))),
00192   true)$
00193 
00194 
00195 okltest_aes_mixcolumns_ns_var_l(f) := block([cst],
00196   cst : ["aes_mixcolumns_cst",create_list(i,i,1,384),nounify(n)],
00197   assert(f(cst) = []),
00198   true)$
00199 
00200 okltest_aes_mixcolumns_cstr_cstl(f) := block([cst],
00201   cst : ["aes_mixcolumns_cst",create_list(i,i,1,256),nounify(n)],
00202   namespace : cstt_namespace_new(aes_mixcolumns_namespace, cst),
00203   ctl : f(cst),
00204   assert(map(first,ctl) = create_list("aes_mixcolumn_cst",i,1,4)),
00205   assert(map(lambda([a],length(a[2])), ctl) = create_list(64,i,1,4)),
00206   assert(every_s(lambda([a], is(last(a) =
00207           namespace)),ctl)),
00208   if oklib_test_level = 0 then return(true),
00209   assert(
00210     setify(aes_mixcolumns_ns_var_l(cst)) =
00211     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00212       setify(create_list(i,i,1,384)))),
00213   true)$
00214 
00215 
00216 okltest_aes_bi_mixcolumn_ns_var_l(f) := block([cst],
00217   cstt : ["aes_mixcolumn_cst",create_list(i,i,1,64),lambda([a],a)],
00218   cstt_new : cstt_namespace_replace(cstt,
00219     cstt_namespace_new(aes_bi_mixcolumn_namespace,cstt)),
00220   namespace_mc : cstt_namespace_new(aes_mixcolumn_namespace,cstt_new),
00221   namespace_invmc : cstt_namespace_new(aes_inv_mixcolumn_namespace,cstt_new),
00222   assert(
00223     f(cstt) =
00224     append(
00225       map(
00226         lambda([a],namespace_mc(aes_var(a,nounify(mc3)))),
00227         create_list(i,i,1,32)),
00228       map(
00229         lambda([a],namespace_mc(aes_var(a,nounify(mc2)))),
00230         create_list(i,i,1,32)),
00231       map(
00232         lambda([a],namespace_invmc(aes_var(a,nounify(mc9)))),
00233         create_list(i,i,1,32)),      
00234       map(
00235         lambda([a],namespace_invmc(aes_var(a,nounify(mc13)))),
00236         create_list(i,i,1,32)),      
00237       map(
00238         lambda([a],namespace_invmc(aes_var(a,nounify(mc11)))),
00239         create_list(i,i,1,32)),      
00240       map(
00241         lambda([a],namespace_invmc(aes_var(a,nounify(mc14)))),
00242         create_list(i,i,1,32)))),
00243   true)$
00244 
00245 okltest_aes_mixcolumn_ns_var_l(f) := block([cst],
00246   cst : ["aes_mixcolumn_cst",create_list(i,i,1,64),lambda([a],a)],
00247   namespace : cstt_namespace_new(aes_mixcolumn_namespace, cst),
00248   assert(
00249     f(cst) =
00250     append(
00251       map(
00252         lambda([a],namespace(aes_var(a,nounify(mc3)))),
00253         create_list(i,i,1,32)),
00254       map(
00255         lambda([a],namespace(aes_var(a,nounify(mc2)))),
00256         create_list(i,i,1,32)))),
00257   true)$
00258 
00259 
00260 okltest_aes_inv_mixcolumn_ns_var_l(f) := block([cst],
00261   cst : ["aes_mixcolumn_cst",create_list(i,i,1,64),lambda([a],a)],
00262   namespace : cstt_namespace_new(aes_inv_mixcolumn_namespace, cst),
00263   assert(
00264     f(cst) =
00265     append(
00266       map(
00267         lambda([a],namespace(aes_var(a,nounify(mc9)))),
00268         create_list(i,i,1,32)),      
00269       map(
00270         lambda([a],namespace(aes_var(a,nounify(mc13)))),
00271         create_list(i,i,1,32)),      
00272       map(
00273         lambda([a],namespace(aes_var(a,nounify(mc11)))),
00274         create_list(i,i,1,32)),      
00275       map(
00276         lambda([a],namespace(aes_var(a,nounify(mc14)))),
00277         create_list(i,i,1,32)))),
00278   true)$
00279 
00280 okltest_aes_bi_mixcolumn_cstr_cstl(f) := block([cst],
00281   cst : ["aes_mixcolumn_cst",create_list(i,i,1,64),nounify(n)],
00282   cstt_new : cstt_namespace_replace(cst,
00283     cstt_namespace_new(aes_bi_mixcolumn_namespace,cst)),
00284   namespace_mc : cstt_namespace_new(aes_mixcolumn_namespace,cstt_new),
00285   namespace_invmc : cstt_namespace_new(aes_inv_mixcolumn_namespace,cstt_new),
00286   ctl : f(cst),
00287   assert(map(first,ctl) =
00288     ["aes_add_cst","aes_mul3_cst","aes_mul2_cst","aes_add_cst","aes_mul3_cst",
00289      "aes_mul2_cst","aes_add_cst","aes_mul3_cst","aes_mul2_cst",
00290      "aes_add_cst","aes_mul3_cst","aes_mul2_cst",
00291      "aes_add_cst","aes_mul9_cst","aes_mul13_cst",
00292      "aes_mul11_cst","aes_mul14_cst",
00293      "aes_add_cst","aes_mul9_cst","aes_mul13_cst","aes_mul11_cst",
00294      "aes_mul14_cst","aes_add_cst","aes_mul9_cst",
00295      "aes_mul13_cst","aes_mul11_cst","aes_mul14_cst","aes_add_cst",
00296      "aes_mul9_cst","aes_mul13_cst",
00297      "aes_mul11_cst","aes_mul14_cst"]),
00298   assert(map(lambda([a],length(a[2])), ctl) =
00299     [40,16,16,40,16,16,40,16,16,40,16,16,40,16,16,16,16,40,16,
00300      16,16,16,40,16,16,16,16,40,16,16,16,16]),
00301   assert(every_s(lambda([a], is(last(a) = namespace_mc) or
00302         is(last(a) = namespace_invmc)),ctl)),
00303   if oklib_test_level = 0 then return(true),
00304   assert(
00305     setify(aes_bi_mixcolumn_ns_var_l(cst)) =
00306     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00307       setify(create_list(i,i,1,384)))),
00308   true)$
00309 
00310 okltest_aes_mixcolumn_cstr_cstl(f) := block([cst],
00311   cst : ["aes_mixcolumn_cst",create_list(i,i,1,64),nounify(n)],
00312   namespace : cstt_namespace_new(aes_mixcolumn_namespace, cst),
00313   ctl : f(cst),
00314   assert(map(first,ctl) =
00315     ["aes_add_cst","aes_mul3_cst","aes_mul2_cst","aes_add_cst","aes_mul3_cst",
00316      "aes_mul2_cst","aes_add_cst","aes_mul3_cst","aes_mul2_cst",
00317      "aes_add_cst","aes_mul3_cst","aes_mul2_cst"]),
00318   assert(map(lambda([a],length(a[2])), ctl) =
00319     [40,16,16,40,16,16,40,16,16,40,16,16]),
00320   assert(every_s(lambda([a], is(last(a) = namespace)),ctl)),
00321   if oklib_test_level = 0 then return(true),
00322   assert(
00323     setify(aes_mixcolumn_ns_var_l(cst)) =
00324     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00325       setify(create_list(i,i,1,384)))),
00326   true)$
00327 
00328 okltest_aes_key_expansion_ns_var_l(f) := block([cst],
00329   cst : ["aes_key_expansion_cst",create_list(i,i,1,384),1,lambda([a],a)],
00330   namespace : cstt_namespace_new(aes_key_expansion_namespace, cst),
00331   assert(
00332     f(cst) =
00333     append(
00334       map(
00335         lambda([a],namespace(aes_var(a,nounify(rc)))),
00336         create_list(i,i,1,8)),
00337       map(
00338         lambda([a],namespace(aes_var(a,nounify(ke)))),
00339         create_list(i,i,1,8)),
00340       map(
00341         lambda([a],namespace(aes_var(a,nounify(sb)))),
00342         create_list(i,i,1,32)))),
00343   true)$
00344 
00345 
00346 okltest_aes_key_expansion_cstr_cstl(f) := block([cst],
00347   cst : ["aes_key_expansion_cst",create_list(i,i,1,384),1,nounify(n)],
00348   namespace : cstt_namespace_new(aes_key_expansion_namespace, cst),
00349   ctl : f(cst),
00350   assert(map(first,ctl) =
00351     ["aes_add_cst","aes_add_cst","aes_add_cst","aes_add_cst","aes_add_cst",
00352      "aes_add_cst","aes_add_cst","aes_add_cst","aes_add_cst","aes_add_cst",
00353      "aes_add_cst","aes_add_cst","aes_add_cst","aes_sbox_cst","aes_add_cst",
00354      "aes_sbox_cst","aes_add_cst","aes_sbox_cst","aes_add_cst","const_cst",
00355      "aes_add_cst","aes_sbox_cst","eq_cst","eq_cst","eq_cst",
00356      "eq_cst","eq_cst","eq_cst","eq_cst","eq_cst",
00357      "eq_cst","eq_cst","eq_cst","eq_cst","eq_cst",
00358      "eq_cst","eq_cst","eq_cst"]),
00359   assert(map(lambda([a],length(a[2])), ctl) =
00360     [24,24,24,24,24,24,24,24,24,24,24,24,24,16,24,16,24,16,24,8,24,16,16,16,
00361      16,16,16,16,16,16,16,16,16,16,16,16,16,16]),
00362   assert(every_s(lambda([a], is(last(a) = namespace)),ctl)),
00363   if oklib_test_level = 0 then return(true),
00364   assert(
00365     setify(aes_key_expansion_ns_var_l(cst)) =
00366     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00367       setify(create_list(i,i,1,384)))),
00368   true)$
00369 
00370 
00371 /* ****************************************
00372    * Translation functions                *
00373    ****************************************
00374 */
00375 
00376 okltest_aes_add_cst_cl(f) := block(
00377   assert(f(["aes_add_cst", create_list(i,i,1,3)]) = [{-3,-2,-1},{-3,1,2},{-2,1,3},{-1,2,3}]),
00378   assert(f(["aes_add_cst", create_list(i,i,1,6)]) = [{-5,-3,-1},{-5,1,3},{-3,1,5},{-1,3,5},{-6,-4,-2},{-6,2,4},{-4,2,6},{-2,4,6}]),
00379   assert(f(["aes_add_cst", [7,8,9,10,11,12]]) = [{-11,-9,-7},{-11,7,9},{-9,7,11},{-7,9,11},{-12,-10,-8},{-12,8,10},{-10,8,12},{-8,10,12}]),
00380   assert(f(["aes_add_cst", [7,8,9,10,11,12,13,14],3, 'n]) = [{-13,-11,-9,7},{-13,-11,-7,9},{-13,-9,-7,11},{-13,7,9,11},{-11,-9,-7,13},{-11,7,9,13},{-9,7,11,13},{-7,9,11,13},{-14,-12,-10,8},{-14,-12,-8,10},{-14,-10,-8,12},{-14,8,10,12},{-12,-10,-8,14},{-12,8,10,14},{-10,8,12,14},{-8,10,12,14}]),
00381   true)$
00382 
00383 okltest_aes_eq_cst_cl(f) := block(
00384   assert(f(["aes_eq_cst", create_list(i,i,1,2)]) =
00385     [{-1,2},{1,-2}]),
00386   assert(f(["aes_eq_cst", create_list(i,i,1,4)]) =
00387     [{-1,3},{1,-3},{-2,4},{2,-4}]),
00388   assert(f(["aes_eq_cst", [1,true]]) = [{1}]),
00389   assert(f(["aes_eq_cst", [1,-2,true,true]]) = [{1},{-2}]),
00390   true)$
00391 
00392 okltest_aes_const_cst_cl(f) := block(
00393   assert(f(["const_cst",[],1,nounify(g)]) = []),
00394   assert(f(["const_cst",[1],1,1, nounify(g)]) = [{1}]),
00395   assert(f(["const_cst",[1,2],1,1,0, nounify(g)]) = [{1},{-2}]),
00396   true)$
00397 
00398 okltest_aes_sbox_pi_cst_cl(f) := block([cl],
00399   cl : f(["aes_sbox_cst", create_list(i,i,1,16)]),
00400   assert(first(cl) = {-10,-9,-7,-6,-5,3,4}),
00401   assert(last(cl) = {-4,5,7,11,13,14,15,16}),
00402   assert(length(cl) = 294),
00403   if oklib_test_level = 0 then return(true),
00404   assert(rijnsbox_cnfp(fcl2fcs(cl2fcl(cl)))),
00405   true)$
00406 
00407 okltest_aes_sbox_ts_var_l(f) := block([cst],
00408   cst : ["aes_sbox_cst", create_list(i,i,1,16),nounify(n)],
00409   namespace : cstt_namespace_new(aes_sbox_ts_namespace, cst),
00410   assert(f(cst) = create_list(
00411       namespace(aes_v(i,nounify(sbox_ts))),i,1,256)),
00412   true)$
00413 
00414 okltest_aes_sbox_ts_cst_cl(f) := block([cl,cst],
00415   if oklib_test_level = 0 then return(true),
00416   cst : ["aes_sbox_cst", create_list(i,i,1,16),nounify(n)],
00417   namespace : cstt_namespace_new(aes_sbox_ts_namespace, cst),
00418   cl : f(cst),
00419   assert(cl[1] =
00420     {-7,-4,-2,1,3,5,6,8,9,10,11,12,13,14,15,16,
00421          namespace(aes_v(1,nounify(sbox_ts)))}),
00422   assert(last(rest(cl,-1)) =
00423     {16,
00424          -namespace(aes_v(256,nounify(sbox_ts)))}),
00425   assert(length(last(cl)) = 256),
00426   true)$
00427 
00428 okltest_aes_mul2_pi_cst_cl(f) := block([cl],
00429   assert(f(["aes_mul2_cst", create_list(i,i,1,16)]) =
00430     [{-16,-15,-8},{-16,8,15},{-15,1,8},{-14,7},{-13,-6,-1},{-13,6,16},
00431      {-12,-5,-1},{-12,1,5},{-11,4},{-10,3},{-9,2},{-8,1,15},{-7,14},
00432      {-6,13,16},{-5,1,12},{-4,11},{-3,10},{-2,9},{-1,5,12},{-1,6,13}]),
00433   true)$
00434 
00435 okltest_aes_mul2_ts_var_l(f) := block([cst],
00436   cst : ["aes_mul2_cst", create_list(i,i,1,16),nounify(n)],
00437   namespace : cstt_namespace_new(aes_mul2_ts_namespace, cst),
00438   assert(f(cst) = create_list(
00439       namespace(aes_v(i,nounify(mul2_ts))),i,1,256)),
00440   true)$
00441 
00442 okltest_aes_mul2_ts_cst_cl(f) := block([cl,cst],
00443   if oklib_test_level = 0 then return(true),
00444   cst : ["aes_mul2_cst", create_list(i,i,1,16),nounify(n)],
00445   namespace : cstt_namespace_new(aes_mul2_ts_namespace, cst),
00446   cl : f(cst),
00447   assert(cl[1] =
00448     {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,
00449          namespace(aes_v(1,nounify(mul2_ts)))}),
00450   assert(last(rest(cl,-1)) =
00451     {16,
00452          -namespace(aes_v(256,nounify(mul2_ts)))}),
00453   assert(length(last(cl)) = 256),
00454   true)$
00455 
00456 okltest_aes_mul3_pi_cst_cl(f) := block([cl],
00457   assert(f(["aes_mul3_cst", create_list(i,i,1,16)]) =
00458     [{-16,-15,-7},{-16,-8,-1},{-16,1,8},{-16,7,15},{-15,-8,-5,13,14},
00459      {-15,7,16},{-15,8,9,10,11,12,13,14},{-14,-7,-6},{-14,6,7},{-14,6,15,16},
00460      {-13,-8,-5,14,15},{-13,-6,-5,1},{-13,-6,-1,5},{-13,-5,-1,6},
00461      {-13,-5,-1,7,14},{-13,1,5,6},{-13,1,5,7,14},{-13,5,8,14,15},
00462      {-12,-5,-4,1},{-12,-5,-1,4},{-12,-4,-1,5},{-12,1,4,5},{-12,4,6,13},
00463      {-12,4,7,13,14},{-12,4,13,14,15,16},{-11,-4,-3},{-11,3,4},
00464      {-11,3,6,12,13},{-11,3,7,12,13,14},{-11,3,12,13,14,15,16},
00465      {-11,5,9,10,12},{-10,-9,-3,1},{-10,-9,-3,4,5,12},{-10,-9,-3,5,7,13,14},
00466      {-10,-3,-2},{-10,-2,-1,5,11,12},{-10,2,3},{-10,2,4,11},
00467      {-10,2,6,11,12,13},{-10,2,11,12,13,14,15,16},{-9,-2,-1},{-9,1,3,10},
00468      {-9,1,4,10,11},{-9,5,10,11,12},{-9,8,10,11,12,13,14,15},{-8,1,16},
00469      {-7,6,14},{-6,-5,-1,13},{-6,1,5,13},{-5,-4,-1,12},{-5,1,4,12},
00470      {-4,1,5,12},{-4,3,11},{-3,2,10},{-2,1,9},{-2,6,10,11,12,13},{-1,2,9},
00471      {-1,3,9,10},{-1,4,9,10,11},{-1,8,16},{-1,9,10,11,12,13,14,15,16}]),
00472   true)$
00473 
00474 okltest_aes_mul3_ts_var_l(f) := block([cst],
00475   cst : ["aes_mul3_cst", create_list(i,i,1,16),nounify(n)],
00476   namespace : cstt_namespace_new(aes_mul3_ts_namespace, cst),
00477   assert(f(cst) = create_list(
00478       namespace(aes_v(i,nounify(mul3_ts))),i,1,256)),
00479   true)$
00480 
00481 okltest_aes_mul3_ts_cst_cl(f) := block([cl,cst],
00482   if oklib_test_level = 0 then return(true),
00483   cst : ["aes_mul3_cst", create_list(i,i,1,16),nounify(n)],
00484   namespace : cstt_namespace_new(aes_mul3_ts_namespace, cst),
00485   cl : f(cst),
00486   assert(cl[1] =
00487     {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,
00488          namespace(aes_v(1,nounify(mul3_ts)))}),
00489   assert(last(rest(cl,-1)) =
00490     {16,
00491          -namespace(aes_v(256,nounify(mul3_ts)))}),
00492   assert(length(last(cl)) = 256),
00493   true)$
00494 
00495 okltest_aes_mul14_pi_cst_cl(f) := block([cl],
00496   assert(f(["aes_mul14_cst", create_list(i,i,1,16)]) =
00497     [{-16,-14,-11,-10,-3,13},{-16,-14,-3,10,11,13},{-16,-13,-12,-10,-8,4},
00498      {-16,-13,-12,-10,-4,3,15},{-16,-13,-12,-8,-4,10},{-16,-13,-12,3,4,10,15},
00499      {-16,-13,-11,-10,-3,14},{-16,-13,-10,-8,-4,12},{-16,-13,-10,3,4,12,15},
00500      {-16,-13,-8,4,10,12},{-16,-13,-4,3,10,12,15},{-16,-13,-3,10,11,14},
00501      {-16,-12,-8,4,10,13},{-16,-11,-10,3,13,14},{-16,-11,-6,10},
00502      {-16,-10,-6,11},{-16,-8,-4,10,12,13},{-16,3,10,11,13,14},
00503      {-15,-14,-12,-11,-4},{-15,-14,-12,4,11},{-15,-14,-11,4,12},
00504      {-15,-14,-4,11,12},{-15,-12,-11,4,14},{-15,-12,-4,11,14},
00505      {-15,-11,-4,12,14},{-15,4,11,12,14},{-14,-13,-3,6},{-14,-12,-11,3,4,8},
00506      {-14,-12,-11,4,15},{-14,-12,-4,3,8,11},{-14,-12,-4,11,15},
00507      {-14,-11,-4,3,8,12},{-14,-11,-4,12,15},{-14,-11,-3,10,13,16},
00508      {-14,-10,-3,11,13,16},{-14,3,4,8,11,12},{-14,3,6,13},{-14,4,11,12,15},
00509      {-13,-12,-10,-8,-4,16},{-13,-12,-10,3,4,15,16},{-13,-12,-8,4,10,16},
00510      {-13,-12,-4,3,10,15,16},{-13,-11,-3,10,14,16},{-13,-10,-8,4,12,16},
00511      {-13,-10,-4,3,12,15,16},{-13,-10,-3,11,14,16},{-13,-8,-4,10,12,16},
00512      {-13,3,4,10,12,15,16},{-13,3,6,14},{-12,-11,-7,9},{-12,-11,-4,3,8,14},
00513      {-12,-10,-8,4,13,16},{-12,-9,-7,11},{-12,-6,-3,5,7},{-12,3,4,8,11,14},
00514      {-12,3,5,6,7},{-12,7,9,11},{-11,-10,-9,-6,-1,4},{-11,-10,-6,-3,-1,2},
00515      {-11,-10,-6,1,2,3},{-11,-10,-6,1,4,9},{-11,-9,-7,12},{-11,-9,-6,-5,-3},
00516      {-11,-9,-5,3,6},{-11,-9,-4,1,6,10},{-11,-6,-5,3,9},{-11,-5,-3,6,9},
00517      {-11,-4,-1,6,9,10},{-11,-3,-1,2,6,10},{-11,1,4,6,9,10},{-11,3,4,8,12,14},
00518      {-10,-9,-1,4,6,11},{-10,-8,-1,7,11,13},{-10,-4,-3,1,5},{-10,-4,-1,3,5},
00519      {-10,-3,-1,2,6,11},{-10,-2,-1,5,9},{-10,1,2,3,6,11},{-10,1,3,4,5},
00520      {-10,1,4,6,9,11},{-10,2,4,5,16},{-9,-8,-7,-6,-4,13},{-9,-8,-7,3,4,14},
00521      {-9,-8,-7,4,6,13},{-9,-7,-4,14,15},{-9,-6,-5,3,11},{-9,-6,-4,1,10,11},
00522      {-9,-5,-3,6,11},{-9,-4,-2,3},{-9,-4,-1,16},{-9,-3,-2,4},{-9,1,4,16},
00523      {-9,2,3,4},{-8,-7,-6,4,9,13},{-8,-7,-4,6,9,13},{-8,-6,-2,3,7,13},
00524      {-8,1,6,7,13,16},{-8,2,7,14},{-7,4,9,14,15},{-7,9,11,12},{-6,-5,-3,7,12},
00525      {-6,-5,-3,9,11},{-6,-4,-1,9,10,11},{-6,-3,-1,2,10,11},{-6,1,4,9,10,11},
00526      {-6,2,7,13,15},{-6,8,13,14,15},{-5,3,6,7,12},{-5,3,6,9,11},
00527      {-5,9,11,13,14},{-4,-3,-2,9},{-4,-3,-1,5,10},{-4,1,9,16},{-4,2,3,9},
00528      {-4,2,5,10,16},{-4,3,8,11,12,14},{-3,1,2,16},{-3,1,4,5,10},
00529      {-3,2,6,7,8,13},{-3,5,6,7,12},{-3,6,13,14},{-3,8,15},{-2,1,5,9,10},
00530      {-2,3,4,9},{-2,6,7,13,15},{-2,7,8,14},{-1,3,4,5,10},{-1,4,9,16},
00531      {-1,5,12,13,15,16}]),
00532   true)$
00533 
00534 okltest_aes_mul14_ts_var_l(f) := block([cst],
00535   cst : ["aes_mul14_cst", create_list(i,i,1,16),nounify(n)],
00536   namespace : cstt_namespace_new(aes_mul14_ts_namespace, cst),
00537   assert(f(cst) = create_list(
00538       namespace(aes_v(i,nounify(mul14_ts))),i,1,256)),
00539   true)$
00540 
00541 okltest_aes_mul14_ts_cst_cl(f) := block([cl,cst],
00542   if oklib_test_level = 0 then return(true),
00543   cst : ["aes_mul14_cst", create_list(i,i,1,16),nounify(n)],
00544   namespace : cstt_namespace_new(aes_mul14_ts_namespace, cst),
00545   cl : f(cst),
00546   assert(cl[1] =
00547     {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,
00548          namespace(aes_v(1,nounify(mul14_ts)))}),
00549   assert(last(rest(cl,-1)) =
00550     {16,
00551          -namespace(aes_v(256,nounify(mul14_ts)))}),
00552   assert(length(last(cl)) = 256),
00553   true)$
00554 
00555 okltest_aes_mul11_pi_cst_cl(f) := block([cl],
00556   assert(f(["aes_mul11_cst", create_list(i,i,1,16)]) =
00557     [{-16,-13,-11,-9,-3,1,5},{-16,-13,-11,-5,-1,3,9},
00558      {-16,-13,-10,-5,-2,3,7,11,12},{-16,-13,-10,-3,-2,6},{-16,-13,-5,1,6},
00559      {-16,-13,-3,1,5,9,11},{-16,-13,-1,4,10,11},{-16,-13,-1,5,6},
00560      {-16,-11,-1,3,5,9,13},{-16,-10,-9,-5,-2,11,14,15},{-16,-10,-2,3,6,13},
00561      {-16,-10,-2,5,8},{-16,-10,-2,9,11,13},{-16,-9,-5,-3,-2,12,15},
00562      {-16,-9,-5,1,10,12,13,14},{-16,-9,-2,3,5,12,15},{-16,-9,-2,10,11,13},
00563      {-16,-9,-1,3,5,11,13},{-16,-5,-3,1,7,10,15},{-16,-5,-2,7,13,14},
00564      {-16,-5,-2,8,10},{-16,-5,-1,6,13},{-16,-3,-2,5,9,12,15},{-16,-3,-1,8},
00565      {-16,1,3,8},{-16,1,4,10,11,13},{-16,1,5,6,13},{-15,-14,-13,5},
00566      {-15,-14,-5,13},{-15,-13,-5,14},{-15,5,13,14},{-14,-12,-11,-10,-3},
00567      {-14,-12,-11,3,10},{-14,-12,-10,3,11},{-14,-12,-3,10,11},
00568      {-14,-11,-10,3,12},{-14,-11,-3,10,12},{-14,-10,-3,11,12},
00569      {-14,3,10,11,12},{-13,-11,-10,-9,-2,16},{-13,-11,-9,-8,-5},
00570      {-13,-11,-8,5,9},{-13,-11,-5,1,3,9,16},{-13,-11,-2,9,10,16},
00571      {-13,-10,-2,9,11,16},{-13,-9,-8,5,11},{-13,-8,-5,9,11},
00572      {-13,-5,-2,3,4,11,16},{-13,-5,-1,6,16},{-13,-3,-2,6,10,16},
00573      {-13,-3,-1,7,10,14,16},{-13,1,5,6,16},{-13,1,7,11,12,16},
00574      {-12,-11,-10,3,14},{-12,-10,-9,-8,-3,15},{-12,-10,-8,3,9,15},
00575      {-12,-9,-8,3,10,15},{-12,-9,-7,-5,-3},{-12,-9,-7,3,5},
00576      {-12,-8,-3,9,10,15},{-12,-7,-5,3,9},{-12,-7,-3,5,9},
00577      {-12,-5,-4,-2,-1,3,7},{-12,-5,-4,2,7,8,16},{-12,-5,-3,7,9},
00578      {-12,-3,-1,4,5,15,16},{-12,3,5,7,9},{-12,4,7,10},{-12,5,6,7,11},
00579      {-11,-10,-3,12,14},{-11,-10,-2,9,13,16},{-11,-9,-8,5,13},
00580      {-11,-9,-7,5,10,14},{-11,-9,-6,3},{-11,-8,-5,9,13},{-11,-6,-3,9},
00581      {-11,-4,-3,-2,-1,6},{-11,-4,-3,1,2,6},{-11,1,4,10,13,16},
00582      {-10,-9,-8,3,12,15},{-10,-9,-7,5,11,14},{-10,-9,-5,-4,-3},
00583      {-10,-9,-4,3,5},{-10,-8,-3,9,12,15},{-10,-7,-5,8,15},{-10,-7,-5,9,11,14},
00584      {-10,-5,-4,3,9},{-10,-5,-3,1,2},{-10,-5,-2,8,16},{-10,-5,-1,2,3},
00585      {-10,-4,-3,5,9},{-10,-3,-2,6,13,16},{-10,-3,-1,2,5},{-10,1,2,3,5},
00586      {-9,-8,-5,11,13},{-9,-8,-3,10,12,15},{-9,-7,-5,3,12},{-9,-7,-3,5,12},
00587      {-9,-6,-3,11},{-9,-5,-4,3,10},{-9,-4,-3,5,10},{-9,-3,-2,12,13,14,16},
00588      {-9,-2,-1,4},{-9,1,2,4},{-9,1,3,5,11,13,16},{-9,1,3,11,14,15,16},
00589      {-8,3,9,10,12,15},{-8,5,9,11,13},{-7,-5,-3,9,12},{-7,3,5,9,12},
00590      {-7,5,8,10,15},{-7,5,9,10,11,14},{-7,8,10,13,14},{-6,-2,-1,7,14},
00591      {-6,1,2,7,14},{-6,3,9,11},{-5,-4,-3,9,10},{-5,-3,-2,1,4,7,12},
00592      {-5,-3,-1,2,4,7,12},{-5,-3,-1,2,10},{-5,-3,-1,4,12,15,16},
00593      {-5,-3,-1,9,11,13,16},{-5,1,2,3,10},{-5,1,2,6,7,13,15},{-5,1,6,13,16},
00594      {-5,2,7,13,14,16},{-5,6,7,11,12},{-4,3,5,9,10},{-4,7,10,12},
00595      {-3,1,2,5,10},{-3,1,2,7,8,15},{-3,1,7,10,13,14,16},{-3,1,8,16},
00596      {-3,5,7,9,12},{-2,1,3,4,5,7,12},{-2,1,4,9},{-2,1,6,7,14},{-2,5,8,10,16},
00597      {-2,7,15,16},{-2,9,10,11,13,16},{-1,2,3,5,10},{-1,2,3,7,8,15},{-1,2,4,9},
00598      {-1,2,5,11,12,14},{-1,2,6,7,14},{-1,3,8,16},{-1,5,6,13,16},
00599      {-1,7,11,12,13,16},{-1,9,10,12,15,16}]),
00600   true)$
00601 
00602 okltest_aes_mul11_ts_var_l(f) := block([cst],
00603   cst : ["aes_mul11_cst", create_list(i,i,1,16),nounify(n)],
00604   namespace : cstt_namespace_new(aes_mul11_ts_namespace, cst),
00605   assert(f(cst) = create_list(
00606       namespace(aes_v(i,nounify(mul11_ts))),i,1,256)),
00607   true)$
00608 
00609 okltest_aes_mul11_ts_cst_cl(f) := block([cl,cst],
00610   if oklib_test_level = 0 then return(true),
00611   cst : ["aes_mul11_cst", create_list(i,i,1,16),nounify(n)],
00612   namespace : cstt_namespace_new(aes_mul11_ts_namespace, cst),
00613   cl : f(cst),
00614   assert(cl[1] =
00615     {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,
00616          namespace(aes_v(1,nounify(mul11_ts)))}),
00617   assert(last(rest(cl,-1)) =
00618     {16,
00619          -namespace(aes_v(256,nounify(mul11_ts)))}),
00620   assert(length(last(cl)) = 256),
00621   true)$
00622 
00623 okltest_aes_mul13_pi_cst_cl(f) := block([cl],
00624   assert(f(["aes_mul13_cst", create_list(i,i,1,16)]) =
00625     [{-16,-15,-14,-13,-11,8},{-16,-15,-14,-13,-8,11},{-16,-15,-14,-11,-8,13},
00626      {-16,-15,-14,8,11,13},{-16,-15,-13,-11,-8,14},{-16,-15,-13,8,11,14},
00627      {-16,-15,-11,8,13,14},{-16,-15,-8,11,13,14},{-16,-14,-13,-11,-8,15},
00628      {-16,-14,-13,8,11,15},{-16,-14,-11,8,13,15},{-16,-14,-8,11,13,15},
00629      {-16,-13,-11,8,14,15},{-16,-13,-8,11,14,15},{-16,-11,-8,13,14,15},
00630      {-16,8,11,13,14,15},{-15,-14,-13,-11,-10,-9,-5},
00631      {-15,-14,-13,-11,-5,9,10},{-15,-14,-13,-10,-5,9,11},
00632      {-15,-14,-13,-9,-5,10,11},{-15,-14,-5,6,13},{-15,-13,-10,-9,-3,8},
00633      {-15,-13,-10,-8,-3,9},{-15,-13,-9,-8,-3,10},{-15,-13,-3,8,9,10},
00634      {-15,-11,-10,-9,-5,13,14},{-15,-11,-5,9,10,13,14},
00635      {-15,-10,-5,9,11,13,14},{-15,-9,-5,10,11,13,14},{-15,-9,-4,7},
00636      {-15,-7,-4,9},{-15,-7,-1,3},{-15,1,3,7},{-14,-11,-10,-9,-5,13,15},
00637      {-14,-11,-10,-9,-3,16},{-14,-11,-10,-9,-2,8},{-14,-11,-5,9,10,13,15},
00638      {-14,-11,-3,9,10,16},{-14,-11,-2,8,9,10},{-14,-10,-8,2,9,11},
00639      {-14,-10,-5,9,11,13,15},{-14,-10,-3,9,11,16},{-14,-9,-8,2,10,11},
00640      {-14,-9,-5,10,11,13,15},{-14,-9,-3,10,11,16},{-14,-8,-2,6},{-14,2,6,8},
00641      {-13,-11,-10,-9,-5,14,15},{-13,-11,-5,9,10,14,15},{-13,-10,-9,-8,-7,1},
00642      {-13,-10,-9,-8,-1,7},{-13,-10,-9,1,7,8},{-13,-10,-8,-7,-1,9},
00643      {-13,-10,-8,1,7,9},{-13,-10,-7,1,8,9},{-13,-10,-5,9,11,14,15},
00644      {-13,-10,-3,8,9,15},{-13,-10,-1,4,8,15},{-13,-10,-1,7,8,9},
00645      {-13,-9,-8,1,7,10},{-13,-9,-7,1,8,10},{-13,-9,-5,10,11,14,15},
00646      {-13,-9,-3,8,10,15},{-13,-9,-1,7,8,10},{-13,-8,-7,1,9,10},
00647      {-13,-8,-3,6,11,15},{-13,-8,-1,4,10,15},{-13,-8,-1,7,9,10},
00648      {-13,-7,-1,8,9,10},{-13,1,7,8,9,10},{-12,-11,-10,7},{-12,-11,-7,10},
00649      {-12,-10,-7,11},{-12,7,10,11},{-11,-10,-9,-8,-2,14},{-11,-10,-9,2,8,14},
00650      {-11,-10,-6,9},{-11,-9,-6,10},{-11,-8,-3,5,14},{-11,-8,-2,9,10,14},
00651      {-11,-5,-3,2,6},{-11,-5,-2,3,6},{-11,-3,-2,5,6},{-11,2,8,9,10,14},
00652      {-10,-9,-7,1,8,13},{-10,-9,-6,11},{-10,-9,-3,8,13,15},{-10,-9,-1,7,8,13},
00653      {-10,-8,-2,9,11,14},{-10,-8,-1,7,9,13},{-10,-7,-1,8,9,13},
00654      {-10,-4,-2,1,5},{-10,-4,-1,2,5},{-10,-2,-1,4,5},{-10,1,2,4,5},
00655      {-10,2,8,9,11,14},{-9,-8,-7,1,10,13},{-9,-8,-3,10,13,15},
00656      {-9,-8,-2,10,11,14},{-9,-7,-6,12},{-9,-7,-4,15},{-9,-3,-1,4},{-9,1,3,4},
00657      {-9,1,7,8,10,13},{-9,2,8,10,11,14},{-8,-7,-3,9,11,12,13,15},
00658      {-8,-7,-1,9,10,13},{-8,-3,-2,1,5,7,13},{-8,1,2,7,15,16},{-8,2,3,16},
00659      {-8,2,5,13,15},{-8,2,6,14},{-8,3,4,11,12,13},{-7,1,3,15},
00660      {-7,3,4,8,10,13},{-7,4,5,6,9,13,14},{-7,6,9,12},{-6,7,9,12},{-6,9,10,11},
00661      {-5,-3,-2,6,11},{-5,2,3,6,11},{-5,7,9,12,13,14,15},{-4,-2,-1,5,10},
00662      {-4,1,2,5,10},{-4,6,12,15},{-4,7,9,15},{-3,1,4,6,7,12},{-3,1,4,9},
00663      {-3,2,5,6,11},{-3,5,8,11,14},{-3,6,14,16},{-3,8,9,10,13,15},
00664      {-2,1,4,5,10},{-2,3,8,16},{-2,3,11,13,14,15},{-2,5,8,13,15},{-2,6,8,14},
00665      {-1,2,4,5,10},{-1,3,4,6,7,12},{-1,3,4,9},{-1,3,5,6,7,13,14},{-1,3,7,15},
00666      {-1,7,8,9,10,13}]),
00667   true)$
00668 
00669 okltest_aes_mul13_ts_var_l(f) := block([cst],
00670   cst : ["aes_mul13_cst", create_list(i,i,1,16),nounify(n)],
00671   namespace : cstt_namespace_new(aes_mul13_ts_namespace, cst),
00672   assert(f(cst) = create_list(
00673       namespace(aes_v(i,nounify(mul13_ts))),i,1,256)),
00674   true)$
00675 
00676 okltest_aes_mul13_ts_cst_cl(f) := block([cl,cst],
00677   if oklib_test_level = 0 then return(true),
00678   cst : ["aes_mul13_cst", create_list(i,i,1,16),nounify(n)],
00679   namespace : cstt_namespace_new(aes_mul13_ts_namespace, cst),
00680   cl : f(cst),
00681   assert(cl[1] =
00682     {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,
00683          namespace(aes_v(1,nounify(mul13_ts)))}),
00684   assert(last(rest(cl,-1)) =
00685     {16,
00686          -namespace(aes_v(256,nounify(mul13_ts)))}),
00687   assert(length(last(cl)) = 256),
00688   true)$
00689 
00690 okltest_aes_mul9_pi_cst_cl(f) := block([cl],
00691   assert(f(["aes_mul9_cst", create_list(i,i,1,16)]) =
00692     [{-16,-14,-8,11},{-16,-11,-8,14},{-16,3,8},{-15,-12,-4},{-15,4,12},
00693      {-14,-11,-3},{-14,3,11},{-13,-12,-10,-8,-7,4},{-13,-12,-7,4,8,10},
00694      {-13,-10,-8,-7,-4,12},{-13,-10,-8,2,3},{-13,-10,-7,8,15},{-13,-10,-3,2,8},
00695      {-13,-10,-2,16},{-13,-8,-7,10,15},{-13,-8,-2,3,10},
00696      {-13,-7,-4,8,10,12},{-13,-3,-2,8,10},{-13,2,10,16},{-12,-10,-7,4,8,13},
00697      {-12,-8,-7,4,10,13},{-12,-3,-2,4,7},{-12,2,3,4,7},{-11,-9,-6,-4,-2,3},
00698      {-11,-9,-6,2,3,4},{-11,-6,-4,2,3,9},{-11,-6,-2,3,4,9},{-11,-2,-1,3,6},
00699      {-11,1,2,3,6},{-10,-9,-5,-4,-2},{-10,-9,-5,2,4},{-10,-8,-7,13,15},
00700      {-10,-7,-4,8,12,13},{-10,-5,-4,2,9},{-10,-5,-2,4,9},{-10,-2,-1,5},
00701      {-10,1,2,5},{-9,-8,-5,3,4,13},{-9,-6,-4,-3,-2,11},{-9,-6,-4,2,14},
00702      {-9,-6,-3,2,4,11},{-9,-6,-2,4,14},{-9,-5,-4,2,10},{-9,-5,-4,13,16},
00703      {-9,-5,-3,8,12,13,15},{-9,-5,-2,4,10},{-9,-4,-1},{-9,1,4},
00704      {-8,-7,-4,10,12,13},{-8,-5,-4,3,9,13},{-8,1,3,5,13},{-7,8,10,13,15},
00705      {-6,-4,-3,2,9,11},{-6,-4,-2,9,14},{-6,-3,-2,4,9,11},{-6,2,4,9,14},
00706      {-5,-4,-3,8,9,13},{-5,-4,-2,9,10},{-5,2,4,9,10},{-5,4,9,13,16},
00707      {-4,-3,-2,7,12},{-4,1,9},{-4,2,3,7,12},{-3,-2,-1,6,11},{-3,1,2,6,11},
00708      {-3,1,5,8,13},{-3,2,7,15},{-3,2,8,10,13},{-2,1,5,10},{-2,1,6,14},
00709      {-2,3,7,15},{-1,2,5,10},{-1,2,6,14},{-1,4,9},{-1,5,13,16}]),
00710   true)$
00711 
00712 okltest_aes_mul9_ts_var_l(f) := block([cst],
00713   cst : ["aes_mul9_cst", create_list(i,i,1,16),nounify(n)],
00714   namespace : cstt_namespace_new(aes_mul9_ts_namespace, cst),
00715   assert(f(cst) = create_list(
00716       namespace(aes_v(i,nounify(mul9_ts))),i,1,256)),
00717   true)$
00718 
00719 okltest_aes_mul9_ts_cst_cl(f) := block([cl,cst],
00720   if oklib_test_level = 0 then return(true),
00721   cst : ["aes_mul9_cst", create_list(i,i,1,16),nounify(n)],
00722   namespace : cstt_namespace_new(aes_mul9_ts_namespace, cst),
00723   cl : f(cst),
00724   assert(cl[1] =
00725     {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,
00726          namespace(aes_v(1,nounify(mul9_ts)))}),
00727   assert(last(rest(cl,-1)) =
00728     {16,
00729          -namespace(aes_v(256,nounify(mul9_ts)))}),
00730   assert(length(last(cl)) = 256),
00731   true)$
00732 /*
00733 okltest_aes_constraints2cnf_pi_cl(f) := block(
00734   assert(f([]) = []),
00735   okltest_aes_eq_cst_cl(buildq([f:f],lambda([a],f([a])))),
00736   okltest_aes_sbox_pi_cst_cl(buildq([f:f],lambda([a],f([a])))),
00737   okltest_aes_mul2_pi_cst_cl(buildq([f:f],lambda([a],f([a])))),
00738   assert(f([["aes_eq_cst", [1,2]],["aes_add_cst", [1,2,3]]]) =
00739     [{-1,2},{-2,1},{-1,2,3},{-2,1,3},{-3,-2,-1},{-3,1,2}]),
00740   true)$
00741 
00742 okltest_aes_constraints2cnf_ts_cl(f) := block(
00743   assert(f([]) = []),
00744   okltest_aes_eq_cst_cl(buildq([f:f],lambda([a],f([a])))),
00745   okltest_aes_sbox_ts_cst_cl(buildq([f:f],lambda([a],f([a])))),
00746   okltest_aes_mul2_ts_cst_cl(buildq([f:f],lambda([a],f([a])))),
00747   assert(f([["aes_eq_cst", [1,2]],["aes_add_cst", [1,2,3]]]) =
00748     [{-1,2},{-2,1},{-1,2,3},{-2,1,3},{-3,-2,-1},{-3,1,2}]),
00749   true)$*/
00750 
00751