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 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 
00024 kill(f)$
00025 
00026 
00027 /* ***********************************************
00028    * Constraint template rewrite translation     *
00029    ***********************************************
00030 */
00031 
00032 oktest_generate_ss_constraint_vars(f) := block(
00033   for i : 0 thru 5 do
00034     assert(f(i,i-1,lambda([a],a),nounify(id)) = []),
00035   for i : 0 thru 5 do
00036     assert(f(i,i, lambda([a],a),nounify(id)) = [ss_v(i,nounify(id))]),
00037  for i : 0 thru 5 do
00038     assert(f(i,i, nounify(n),nounify(id)) =
00039       [nounify(n)(ss_v(i,nounify(id)))]),
00040   assert(f(1,2, nounify(n),nounify(id)) =
00041     [nounify(n)(ss_v(1,nounify(id))),nounify(n)(ss_v(2,nounify(id)))]),
00042   true)$
00043 
00044 /* ***********************************************
00045    * Constraint template rewrite functions       *
00046    ***********************************************
00047 */
00048 
00049 okltest_ss_ns_var_l(f) := block([cst],
00050   cst : ["ss_cst",create_list(i,i,1,384),1,
00051   4,4,2, 8, ss_polynomial_2_8, ss_sbox_matrix_2_8, ss_affine_constant_2_8,
00052   ss_mixcolumns_matrix_2_8_4,false,lambda([a],a)],
00053   namespace : cstt_namespace_new(ss_namespace, cst),
00054   assert(
00055     f(cst) =
00056     append(
00057       map(
00058         lambda([a],namespace(ss_var(a,nounify(o)))),
00059         create_list(i,i,1,128)),
00060       map(
00061         lambda([a],namespace(ss_var(a,nounify(k)))),
00062         create_list(i,i,1,256)))),
00063   true)$
00064 
00065 okltest_ss_cstr_cstl(f) := block([ctl,ct],
00066   cst : ["ss_cst",create_list(i,i,1,384),1,
00067   4,4,2, 8, ss_polynomial_2_8, ss_sbox_matrix_2_8, ss_affine_constant_2_8,
00068   ss_mixcolumns_matrix_2_8_4,false,nounify(n)],
00069   namespace : cstt_namespace_new(ss_namespace, cst),
00070   ctl : f(cst),
00071   assert(map(cstt_name,ctl) =
00072     ["ss_round_cst","ss_add_cst","ss_key_expansion_cst"]),
00073   assert(map(lambda([a],length(a[2])), ctl) = [384,384,384]),
00074   assert(every_s(lambda([a], is(last(a) =
00075           namespace)),ctl)),
00076   assert(ctl[1][2][50] =
00077     namespace(ss_v(50,nounify(o)))),
00078   assert(ctl[2][2][200] =
00079     namespace(ss_v(72,nounify(k)))),
00080   if oklib_test_level = 0 then return(true),
00081   assert(
00082     setify(ss_ns_var_l(cst)) =
00083     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00084       setify(create_list(i,i,1,384)))),
00085   true)$
00086 
00087 okltest_ss_round_ns_var_l(f) := block([cst],
00088   cst : ["ss_round_cst",create_list(i,i,1,384),1,
00089   4,4,2, 8, ss_polynomial_2_8, ss_sbox_matrix_2_8, ss_affine_constant_2_8,
00090   ss_mixcolumns_matrix_2_8_4, lambda([a],a)],
00091   namespace : cstt_namespace_new(ss_round_namespace, cst),
00092   assert(
00093     f(cst) =
00094     append(
00095       map(
00096         lambda([a],namespace(ss_var(a,nounify(mo)))),
00097         create_list(i,i,1,128)),
00098       map(
00099         lambda([a],namespace(ss_var(a,nounify(ro)))),
00100         create_list(i,i,1,128)),
00101       map(
00102         lambda([a],namespace(ss_var(a,nounify(so)))),
00103         create_list(i,i,1,128)))),
00104   true)$
00105 
00106 okltest_ss_round_cstr_cstl(f) := block([cst],
00107   cst : ["ss_round_cst",create_list(i,i,1,384),1,
00108   4,4,2, 8, ss_polynomial_2_8, ss_sbox_matrix_2_8, ss_affine_constant_2_8,
00109   ss_mixcolumns_matrix_2_8_4,nounify(n)],
00110   namespace : cstt_namespace_new(ss_round_namespace, cst),
00111   ctl : f(cst),
00112   assert(map(first,ctl) =
00113     ["ss_add_cst","ss_mixcolumns_cst","ss_shiftrows_cst",
00114      "ss_subbytes_cst"]),
00115   assert(map(lambda([a],length(a[2])), ctl) = [384,256,256,256]),
00116     assert(every_s(lambda([a], is(last(a) =
00117           namespace)),ctl)),
00118   if oklib_test_level = 0 then return(true),
00119   assert(
00120     setify(ss_round_ns_var_l(cst)) =
00121     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00122       setify(create_list(i,i,1,384)))),
00123   true)$
00124 
00125 okltest_ss_round_core_box_ns_var_l(f) := block([cst],
00126   cst : ["ss_round_cst",create_list(i,i,1,384),1,
00127   4,4,2, 8, ss_polynomial_2_8, ss_sbox_matrix_2_8, ss_affine_constant_2_8,
00128   ss_mixcolumns_matrix_2_8_4, lambda([a],a)],
00129   namespace : cstt_namespace_new(ss_round_core_box_namespace, cst),
00130   assert(
00131     f(cst) =
00132     append(
00133       map(lambda([a],namespace(ss_var(a,nounify(mo)))),
00134           create_list(i,i,1,128)),
00135       map(lambda([a],namespace(ss_var(a,nounify(ro)))),
00136           create_list(i,i,1,128)))),
00137   true)$
00138 
00139 okltest_ss_round_core_box_cstr_cstl(f) := block([cst],
00140   cst : ["ss_round_cst",create_list(i,i,1,384),1,
00141   4,4,2, 8, ss_polynomial_2_8, ss_sbox_matrix_2_8, ss_affine_constant_2_8,
00142   ss_mixcolumns_matrix_2_8_4,nounify(n)],
00143   namespace : cstt_namespace_new(ss_round_core_box_namespace, cst),
00144   ctl : f(cst),
00145   assert(map(first,ctl) =
00146     ["ss_add_cst","ss_round_columns_cst","ss_shiftrows_cst"]),
00147   assert(map(lambda([a],length(a[2])), ctl) = [384,256,256]),
00148     assert(every_s(lambda([a], is(last(a) =
00149           namespace)),ctl)),
00150   if oklib_test_level = 0 then return(true),
00151   assert(
00152     setify(ss_round_core_box_ns_var_l(cst)) =
00153     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00154       setify(create_list(i,i,1,384)))),
00155   true)$
00156 
00157 okltest_ss_final_round_ns_var_l(f) := block([cst],
00158   cst : ["ss_final_round_cst",create_list(i,i,1,384),
00159   4,4,2, 8, ss_polynomial_2_8, ss_sbox_matrix_2_8, ss_affine_constant_2_8,
00160   ss_mixcolumns_matrix_2_8_4, lambda([a],a)],
00161   namespace : cstt_namespace_new(ss_final_round_namespace, cst),
00162   assert(
00163     f(cst) =
00164     append(
00165       map(
00166         lambda([a],namespace(ss_var(a,nounify(ro)))),
00167         create_list(i,i,1,128)),
00168       map(
00169         lambda([a],namespace(ss_var(a,nounify(so)))),
00170         create_list(i,i,1,128)))),
00171   true)$
00172 
00173 
00174 okltest_ss_final_round_cstr_cstl(f) := block([cst],
00175   cst : ["ss_final_round_cst",create_list(i,i,1,384),
00176   4,4,2, 8, ss_polynomial_2_8, ss_sbox_matrix_2_8, ss_affine_constant_2_8,
00177   ss_mixcolumns_matrix_2_8_4, nounify(n)],
00178   namespace : cstt_namespace_new(ss_final_round_namespace, cst),
00179   ctl : f(cst),
00180   assert(map(first,ctl) =
00181     ["ss_add_cst","ss_shiftrows_cst","ss_subbytes_cst"]),
00182   assert(map(lambda([a],length(a[2])), ctl) = [384,256,256]),
00183   assert(every_s(lambda([a], is(last(a) =
00184           namespace)),ctl)),
00185   if oklib_test_level = 0 then return(true),
00186   assert(
00187     setify(ss_final_round_ns_var_l(cst)) =
00188     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00189       setify(create_list(i,i,1,384)))),
00190   true)$
00191 
00192 
00193 okltest_ss_subbytes_ns_var_l(f) := block([cst],
00194   cst : ["ss_subbytes_cst",create_list(i,i,1,384),nounify(n)],
00195   assert(f(cst) = []),
00196   true)$
00197 
00198 
00199 okltest_ss_subbytes_cstr_cstl(f) := block([cst],
00200   cst : ["ss_subbytes_cst",create_list(i,i,1,256),
00201   2, 8, ss_polynomial_2_8, ss_sbox_matrix_2_8, ss_affine_constant_2_8,
00202   nounify(n)],
00203   namespace : cstt_namespace_new(ss_subbytes_namespace, cst),
00204   ctl : f(cst),
00205   assert(map(first,ctl) = create_list("ss_sbox_cst",i,1,16)),
00206   assert(map(lambda([a],length(a[2])), ctl) = create_list(16,i,1,16)),
00207   assert(every_s(lambda([a], is(last(a) =
00208           namespace)),ctl)),
00209   true)$
00210 
00211 
00212 okltest_ss_shiftrows_ns_var_l(f) := block([cst],
00213   cst : ["ss_shiftrows_cst",create_list(i,i,1,384),nounify(n)],
00214   assert(f(cst) = []),
00215   true)$
00216 
00217 
00218 okltest_ss_shiftrows_cstr_cstl(f) := block([cst],
00219   cst : ["ss_shiftrows_cst",create_list(i,i,1,256),4,4,nounify(n)],
00220   namespace : cstt_namespace_new(ss_shiftrows_namespace, cst),
00221   ctl : f(cst),
00222   assert(map(first,ctl) = create_list("eq_cst",i,1,128)),
00223   assert(map(lambda([a],length(a[2])), ctl) = create_list(2,i,1,128)),
00224   assert(every_s(lambda([a], is(last(a) =
00225           namespace)),ctl)),
00226   true)$
00227 
00228 
00229 okltest_ss_mixcolumns_ns_var_l(f) := block([cst],
00230   cst : ["ss_mixcolumns_cst",create_list(i,i,1,384),nounify(n)],
00231   assert(f(cst) = []),
00232   true)$
00233 
00234 okltest_ss_mixcolumns_cstr_cstl(f) := block([cst],
00235   cst : ["ss_mixcolumns_cst",create_list(i,i,1,256),
00236   4, 4,2, 8, ss_polynomial_2_8, ss_mixcolumns_matrix_2_8_4,nounify(n)],
00237   namespace : cstt_namespace_new(ss_mixcolumns_namespace, cst),
00238   ctl : f(cst),
00239   assert(map(first,ctl) = create_list("ss_mixcolumn_cst",i,1,4)),
00240   assert(map(lambda([a],length(a[2])), ctl) = create_list(64,i,1,4)),
00241   assert(every_s(lambda([a], is(last(a) =
00242           namespace)),ctl)),
00243   if oklib_test_level = 0 then return(true),
00244   assert(
00245     setify(ss_mixcolumns_ns_var_l(cst)) =
00246     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00247       setify(create_list(i,i,1,384)))),
00248   true)$
00249 
00250 
00251 okltest_ss_bi_mixcolumn_ns_var_l(f) := block([cst],
00252   cstt : ["ss_mixcolumn_cst",create_list(i,i,1,64),
00253   4,2,8,ss_polynomial_2_8, ss_mixcolumns_matrix_2_8_4,lambda([a],a)],
00254   cstt_new : cstt_namespace_replace(cstt,
00255     cstt_namespace_new(ss_bi_mixcolumn_namespace,cstt)),
00256   namespace_mc : cstt_namespace_new(ss_mixcolumn_namespace,cstt_new),
00257   namespace_invmc : cstt_namespace_new(ss_inv_mixcolumn_namespace,cstt_new),
00258   assert(
00259     length(f(cstt)) = 6*32),
00260   true)$
00261 
00262 
00263 okltest_ss_bi_mixcolumn_cstr_cstl(f) := block([cst],
00264   cst : ["ss_mixcolumn_cst",create_list(i,i,1,64),
00265   4,2,8,ss_polynomial_2_8, ss_mixcolumns_matrix_2_8_4,nounify(n)],
00266   cstt_new : cstt_namespace_replace(cst,
00267     cstt_namespace_new(ss_bi_mixcolumn_namespace,cst)),
00268   namespace_mc : cstt_namespace_new(ss_mixcolumn_namespace,cstt_new),
00269   namespace_invmc : cstt_namespace_new(ss_inv_mixcolumn_namespace,cstt_new),
00270   ctl : f(cst),
00271   assert(map(lambda([a],[first(a),third(a)]),ctl) =
00272     [["ss_add_cst",4],["ss_mul_cst",x+1],["ss_mul_cst",x],["ss_add_cst",4],
00273     ["ss_mul_cst",x],["ss_mul_cst",x+1],["ss_add_cst",4],["ss_mul_cst",x],
00274     ["ss_mul_cst",x+1],["ss_add_cst",4],["ss_mul_cst",x],["ss_mul_cst",x+1],
00275     ["ss_add_cst",4],["ss_mul_cst",x^3+x+1],["ss_mul_cst",x^3+x^2+1],
00276     ["ss_mul_cst",x^3+1],["ss_mul_cst",x^3+x^2+x],["ss_add_cst",4],
00277     ["ss_mul_cst",x^3+x^2+1],["ss_mul_cst",x^3+1],["ss_mul_cst",x^3+x^2+x],
00278     ["ss_mul_cst",x^3+x+1],["ss_add_cst",4],["ss_mul_cst",x^3+1],
00279     ["ss_mul_cst",x^3+x^2+x],["ss_mul_cst",x^3+x+1],
00280     ["ss_mul_cst",x^3+x^2+1],["ss_add_cst",4],["ss_mul_cst",x^3+x^2+x],
00281     ["ss_mul_cst",x^3+x+1],["ss_mul_cst",x^3+x^2+1],["ss_mul_cst",x^3+1]]),
00282   assert(map(lambda([a],length(a[2])), ctl) =
00283     [40,16,16,40,16,16,40,16,16,40,16,16,40,16,16,16,16,40,16,
00284      16,16,16,40,16,16,16,16,40,16,16,16,16]),
00285   assert(every_s(lambda([a], is(last(a) = namespace_mc) or
00286         is(last(a) = namespace_invmc)),ctl)),
00287   if oklib_test_level = 0 then return(true),
00288   assert(
00289     setify(ss_bi_mixcolumn_ns_var_l(cst)) =
00290     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00291       setify(create_list(i,i,1,384)))),
00292   true)$
00293 
00294 
00295 okltest_ss_mixcolumn_ns_var_l(f) := block([cst],
00296   cst : ["ss_mixcolumn_cst",create_list(i,i,1,64),
00297   4,2, 8, ss_polynomial_2_8, ss_mixcolumns_matrix_2_8_4,lambda([a],a)],
00298   namespace : cstt_namespace_new(ss_mixcolumn_namespace, cst),
00299   assert(
00300     length(f(cst)) = 64),
00301   true)$
00302 
00303 
00304 okltest_ss_mixcolumn_cstr_cstl(f) := block([cst],
00305   cst : ["ss_mixcolumn_cst",create_list(i,i,1,64),
00306   4,2, 8, ss_polynomial_2_8, ss_mixcolumns_matrix_2_8_4,nounify(n)],
00307   namespace : cstt_namespace_new(ss_mixcolumn_namespace, cst),
00308   ctl : f(cst),
00309   assert(map(lambda([a],[first(a),third(a)]),ctl) =
00310     [["ss_add_cst",4],["ss_mul_cst",x+1],["ss_mul_cst",x],
00311      ["ss_add_cst",4],["ss_mul_cst",x],["ss_mul_cst",x+1],["ss_add_cst",4],
00312      ["ss_mul_cst",x],["ss_mul_cst",x+1],["ss_add_cst",4],["ss_mul_cst",x],
00313      ["ss_mul_cst",x+1]]),
00314   assert(map(lambda([a],length(a[2])), ctl) =
00315     [40,16,16,40,16,16,40,16,16,40,16,16]),
00316   assert(every_s(lambda([a], is(last(a) = namespace)),ctl)),
00317   if oklib_test_level = 0 then return(true),
00318   assert(
00319     setify(ss_mixcolumn_ns_var_l(cst)) =
00320     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00321       setify(create_list(i,i,1,384)))),
00322   true)$
00323 
00324 okltest_ss_mixcolumn_boolm_ns_var_l(f) := block([cst],
00325   cst : ["ss_mixcolumn_cst",create_list(i,i,1,64),
00326   4,2, 8, ss_polynomial_2_8, ss_mixcolumns_matrix_2_8_4,lambda([a],a)],
00327   namespace : cstt_namespace_new(ss_mixcolumn_namespace, cst),
00328   assert(f(cst) = []),
00329   true)$
00330 
00331 okltest_ss_mixcolumn_boolm_cstr_cstl(f) := (
00332   cst : ["ss_mixcolumn_cst",create_list(i,i,1,64),
00333   4,2, 8, ss_polynomial_2_8, ss_mixcolumns_matrix_2_8_4,nounify(n)],
00334   namespace : cstt_namespace_new(ss_mixcolumn_boolm_namespace, cst),
00335   ctl : f(cst),
00336   assert(map(lambda([a],[first(a),third(a)]),ctl) =
00337     [["ss_add_cst",5],["ss_add_cst",7],["ss_add_cst",5],["ss_add_cst",7],
00338     ["ss_add_cst",7],["ss_add_cst",5],["ss_add_cst",5],["ss_add_cst",5],
00339     ["ss_add_cst",5],["ss_add_cst",7],["ss_add_cst",5],["ss_add_cst",7],
00340     ["ss_add_cst",7],["ss_add_cst",5],["ss_add_cst",5],["ss_add_cst",5],
00341     ["ss_add_cst",5],["ss_add_cst",7],["ss_add_cst",5],["ss_add_cst",7],
00342     ["ss_add_cst",7],["ss_add_cst",5],["ss_add_cst",5],["ss_add_cst",5],
00343     ["ss_add_cst",5],["ss_add_cst",7],["ss_add_cst",5],["ss_add_cst",7],
00344     ["ss_add_cst",7],["ss_add_cst",5],["ss_add_cst",5],["ss_add_cst",5]]),
00345   assert(map(lambda([a],length(a[2])), ctl) =
00346     [6,8,6,8,8,6,6,6,6,8,6,8,8,6,6,6,6,8,6,8,8,6,6,6,6,8,6,8,8,6,6,6]),
00347   assert(every_s(lambda([a], is(last(a) = namespace)),ctl)),
00348   true)$
00349 
00350 okltest_ss_inv_mixcolumn_ns_var_l(f) := block([cst],
00351   cst : ["ss_mixcolumn_cst",create_list(i,i,1,64),
00352   4,2,8,ss_polynomial_2_8, ss_mixcolumns_2_8_4,lambda([a],a)],
00353   namespace : cstt_namespace_new(ss_inv_mixcolumn_namespace, cst),
00354   assert(
00355     length(f(cst)) = 128),
00356   true)$
00357 
00358 okltest_ss_inv_mixcolumn_cstr_cstl(f) := block([cst],
00359   cst : ["ss_inv_mixcolumn_cst",create_list(i,i,1,64),
00360   4,2, 8, ss_polynomial_2_8, ss_mixcolumns_matrix_2_8_4,nounify(n)],
00361   namespace : cstt_namespace_new(ss_inv_mixcolumn_namespace, cst),
00362   ctl : f(cst),
00363   assert(map(lambda([a],[first(a),third(a)]),ctl) =
00364     [["ss_add_cst",4],["ss_mul_cst",x^3+x+1],["ss_mul_cst",x^3+x^2+1],
00365      ["ss_mul_cst",x^3+1],["ss_mul_cst",x^3+x^2+x],["ss_add_cst",4],
00366      ["ss_mul_cst",x^3+x^2+1],["ss_mul_cst",x^3+1],["ss_mul_cst",x^3+x^2+x],
00367      ["ss_mul_cst",x^3+x+1],["ss_add_cst",4],["ss_mul_cst",x^3+1],
00368      ["ss_mul_cst",x^3+x^2+x],["ss_mul_cst",x^3+x+1],["ss_mul_cst",x^3+x^2+1],
00369      ["ss_add_cst",4],["ss_mul_cst",x^3+x^2+x],["ss_mul_cst",x^3+x+1],
00370      ["ss_mul_cst",x^3+x^2+1],["ss_mul_cst",x^3+1]]),
00371   assert(map(lambda([a],length(a[2])), ctl) =
00372     [40,16,16,16,16,40,16,16,16,16,40,16,16,16,16,40,16,16,16,16]),
00373   assert(every_s(lambda([a], is(last(a) = namespace)),ctl)),
00374   assert(
00375     sublist(
00376       stable_unique(flatten(map(cstt_vars_l,ctl))),
00377       lambda([v], elementp(v, setn(64)))) =
00378     [25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,
00379      49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,17,18,19,20,21,22,23,24,
00380      9,10,11,12,13,14,15,16,1,2,3,4,5,6,7,8]),
00381   if oklib_test_level = 0 then return(true),
00382   assert(
00383     setify(ss_inv_mixcolumn_ns_var_l(cst)) =
00384     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00385       setify(create_list(i,i,1,384)))),
00386   true)$
00387 
00388 okltest_ss_key_expansion_ns_var_l(f) := block([cst],
00389   cst : ["ss_key_expansion_cst",create_list(i,i,1,384),1,
00390   4,4,2,8,ss_polynomial_2_8,ss_sbox_matrix_2_8,ss_affine_constant_2_8,
00391   lambda([a],a)],
00392   namespace : cstt_namespace_new(ss_key_expansion_namespace, cst),
00393   assert(
00394     f(cst) =
00395     append(
00396       map(
00397         lambda([a],namespace(ss_var(a,nounify(rc)))),
00398         create_list(i,i,1,8)),
00399       map(
00400         lambda([a],namespace(ss_var(a,nounify(sb)))),
00401         create_list(i,i,1,32)))),
00402   true)$
00403 
00404 
00405 okltest_ss_key_expansion_cstr_cstl(f) := block([cst],
00406   cst : ["ss_key_expansion_cst",create_list(i,i,1,384),1,
00407   4,4,2,8,ss_polynomial_2_8,ss_sbox_matrix_2_8,ss_affine_constant_2_8,
00408   nounify(n)],
00409   namespace : cstt_namespace_new(ss_key_expansion_namespace, cst),
00410   ctl : f(cst),
00411   assert(map(first,ctl) =
00412     ["ss_add_cst","ss_add_cst","ss_add_cst","ss_add_cst","ss_add_cst",
00413      "ss_add_cst","ss_add_cst","ss_add_cst","ss_add_cst","ss_add_cst",
00414      "ss_add_cst","ss_add_cst","ss_add_cst","ss_sbox_cst","ss_add_cst",
00415      "ss_sbox_cst","ss_add_cst","ss_sbox_cst","ss_add_cst","const_cst",
00416      "ss_sbox_cst","eq_cst","eq_cst","eq_cst","eq_cst","eq_cst","eq_cst",
00417      "eq_cst","eq_cst","eq_cst","eq_cst","eq_cst","eq_cst","eq_cst","eq_cst",
00418      "eq_cst","eq_cst"]),
00419   assert(map(lambda([a],length(a[2])), ctl) =
00420     [24,24,24,24,24,24,24,24,24,24,24,24,24,16,24,16,24,16,32,8,16,16,16,16,
00421      16,16,16,16,16,16,16,16,16,16,16,16,16]),
00422   assert(every_s(lambda([a], is(last(a) = namespace)),ctl)),
00423   if oklib_test_level = 0 then return(true),
00424   assert(
00425     setify(ss_key_expansion_ns_var_l(cst)) =
00426     setdifference(setify(lappend(map(cstt_vars_l,ctl))),
00427       setify(create_list(i,i,1,384)))),
00428   true)$
00429 
00430 
00431 /* ****************************************
00432    * Translation functions                *
00433    ****************************************
00434 */
00435 
00436 
00437 okltest_ss_mul_ts_gen(f) := block([ss_mul_ts_CNF : sm2hm({})],
00438   assert(f(2,2,4,ss_polynomial_2_4) =
00439     [[1,2,3,4,5,6,7,8,dts(1),dts(2),dts(3),dts(4),dts(5),dts(6),dts(7),dts(8),
00440      dts(9),dts(10),dts(11),dts(12),dts(13),dts(14),dts(15),dts(16)],
00441      [{1,2,3,4,5,6,7,8,dts(1)},{-5,-2,1,3,4,6,7,8,dts(2)},
00442      {-6,-3,1,2,4,5,7,8,dts(3)},{-6,-5,-3,-2,1,4,7,8,dts(4)},
00443      {-7,-4,1,2,3,5,6,8,dts(5)},{-7,-5,-4,-2,1,3,6,8,dts(6)},
00444      {-7,-6,-4,-3,1,2,5,8,dts(7)},{-7,-6,-5,-4,-3,-2,1,8,dts(8)},
00445      {-8,-4,-1,2,3,5,6,7,dts(9)},{-8,-5,-4,-2,-1,3,6,7,dts(10)},
00446      {-8,-6,-4,-3,-1,2,5,7,dts(11)},{-8,-6,-5,-4,-3,-2,-1,7,dts(12)},
00447      {-8,-7,-1,2,3,4,5,6,dts(13)},{-8,-7,-5,-2,-1,3,4,6,dts(14)},
00448      {-8,-7,-6,-3,-1,2,4,5,dts(15)},{-8,-7,-6,-5,-3,-2,-1,4,dts(16)},
00449      {-8,-dts(1)},{-7,-dts(1)},{-6,-dts(1)},{-5,-dts(1)},{-4,-dts(1)},
00450      {-3,-dts(1)},{-2,-dts(1)},{-1,-dts(1)},{-8,-dts(2)},{-7,-dts(2)},
00451      {-6,-dts(2)},{-4,-dts(2)},{-3,-dts(2)},{-1,-dts(2)},{2,-dts(2)},
00452      {5,-dts(2)},{-8,-dts(3)},{-7,-dts(3)},{-5,-dts(3)},{-4,-dts(3)},
00453      {-2,-dts(3)},{-1,-dts(3)},{3,-dts(3)},{6,-dts(3)},{-8,-dts(4)},
00454      {-7,-dts(4)},{-4,-dts(4)},{-1,-dts(4)},{2,-dts(4)},{3,-dts(4)},
00455      {5,-dts(4)},{6,-dts(4)},{-8,-dts(5)},{-6,-dts(5)},{-5,-dts(5)},
00456      {-3,-dts(5)},{-2,-dts(5)},{-1,-dts(5)},{4,-dts(5)},{7,-dts(5)},
00457      {-8,-dts(6)},{-6,-dts(6)},{-3,-dts(6)},{-1,-dts(6)},{2,-dts(6)},
00458      {4,-dts(6)},{5,-dts(6)},{7,-dts(6)},{-8,-dts(7)},{-5,-dts(7)},
00459      {-2,-dts(7)},{-1,-dts(7)},{3,-dts(7)},{4,-dts(7)},{6,-dts(7)},
00460      {7,-dts(7)},{-8,-dts(8)},{-1,-dts(8)},{2,-dts(8)},{3,-dts(8)},
00461      {4,-dts(8)},{5,-dts(8)},{6,-dts(8)},{7,-dts(8)},{-7,-dts(9)},
00462      {-6,-dts(9)},{-5,-dts(9)},{-3,-dts(9)},{-2,-dts(9)},{1,-dts(9)},
00463      {4,-dts(9)},{8,-dts(9)},{-7,-dts(10)},{-6,-dts(10)},{-3,-dts(10)},
00464      {1,-dts(10)},{2,-dts(10)},{4,-dts(10)},{5,-dts(10)},{8,-dts(10)},
00465      {-7,-dts(11)},{-5,-dts(11)},{-2,-dts(11)},{1,-dts(11)},{3,-dts(11)},
00466      {4,-dts(11)},{6,-dts(11)},{8,-dts(11)},{-7,-dts(12)},{1,-dts(12)},
00467      {2,-dts(12)},{3,-dts(12)},{4,-dts(12)},{5,-dts(12)},{6,-dts(12)},
00468      {8,-dts(12)},{-6,-dts(13)},{-5,-dts(13)},{-4,-dts(13)},{-3,-dts(13)},
00469      {-2,-dts(13)},{1,-dts(13)},{7,-dts(13)},{8,-dts(13)},{-6,-dts(14)},
00470      {-4,-dts(14)},{-3,-dts(14)},{1,-dts(14)},{2,-dts(14)},{5,-dts(14)},
00471      {7,-dts(14)},{8,-dts(14)},{-5,-dts(15)},{-4,-dts(15)},{-2,-dts(15)},
00472      {1,-dts(15)},{3,-dts(15)},{6,-dts(15)},{7,-dts(15)},{8,-dts(15)},
00473      {-4,-dts(16)},{1,-dts(16)},{2,-dts(16)},{3,-dts(16)},{5,-dts(16)},
00474      {6,-dts(16)},{7,-dts(16)},{8,-dts(16)},{dts(1),dts(2),dts(3),dts(4),
00475      dts(5),dts(6),dts(7),dts(8),dts(9),dts(10),dts(11),dts(12),
00476      dts(13),dts(14),dts(15),dts(16)}]]),
00477    assert(length(f(2,2,8,ss_polynomial_2_8)[2]) = 4353),
00478   true)$
00479 
00480 okltest_ss_sbox_ts_gen(f) := block([ss_sbox_ts_CNF : sm2hm({})],
00481   assert(f(2,4,ss_polynomial_2_4) =
00482   [[1,2,3,4,5,6,7,8,dts(1),dts(2),dts(3),dts(4),dts(5),dts(6),dts(7),dts(8),
00483   dts(9),dts(10), dts(11),dts(12),dts(13),dts(14),dts(15),dts(16)],
00484   [{-3,-2,-1,4,5,6,7,8,dts(1)}, {-5,-4,-3,-2,-1,6,7,8,dts(2)},
00485   {-6,-4,-3,1,2,5,7,8,dts(3)}, {-6,-5,-4,-3,-1,2,7,8,dts(4)},
00486   {-7,-2,1,3,4,5,6,8,dts(5)}, {-7,-5,-4,-3,-2,1,6,8,dts(6)},
00487   {-7,-6,1,2,3,4,5,8,dts(7)}, {-7,-6,-5,-4,-2,1,3,8,dts(8)},
00488   {-8,-4,-2,-1,3,5,6,7,dts(9)}, {-8,-5,-1,2,3,4,6,7,dts(10)},
00489   {-8,-6,-3,1,2,4,5,7,dts(11)}, {-8,-6,-5,-4,-1,2,3,7,dts(12)},
00490   {-8,-7,-2,-1,3,4,5,6,dts(13)}, {-8,-7,-5,-4,1,2,3,6,dts(14)},
00491   {-8,-7,-6,-3,-2,1,4,5,dts(15)}, {-8,-7,-6,-5,-3,-1,2,4,dts(16)},
00492   {-8,-dts(1)}, {-7,-dts(1)}, {-6,-dts(1)}, {-5,-dts(1)}, {-4,-dts(1)},
00493   {1,-dts(1)}, {2,-dts(1)}, {3,-dts(1)}, {-8,-dts(2)}, {-7,-dts(2)},
00494   {-6,-dts(2)}, {1,-dts(2)}, {2,-dts(2)}, {3,-dts(2)}, {4,-dts(2)},
00495   {5,-dts(2)}, {-8,-dts(3)}, {-7,-dts(3)}, {-5,-dts(3)}, {-2,-dts(3)},
00496   {-1,-dts(3)}, {3,-dts(3)}, {4,-dts(3)}, {6,-dts(3)}, {-8,-dts(4)},
00497   {-7,-dts(4)}, {-2,-dts(4)}, {1,-dts(4)}, {3,-dts(4)}, {4,-dts(4)},
00498   {5,-dts(4)}, {6,-dts(4)}, {-8,-dts(5)}, {-6,-dts(5)}, {-5,-dts(5)},
00499   {-4,-dts(5)}, {-3,-dts(5)}, {-1,-dts(5)}, {2,-dts(5)}, {7,-dts(5)},
00500   {-8,-dts(6)}, {-6,-dts(6)}, {-1,-dts(6)}, {2,-dts(6)}, {3,-dts(6)},
00501   {4,-dts(6)}, {5,-dts(6)}, {7,-dts(6)}, {-8,-dts(7)}, {-5,-dts(7)},
00502   {-4,-dts(7)}, {-3,-dts(7)}, {-2,-dts(7)}, {-1,-dts(7)}, {6,-dts(7)},
00503   {7,-dts(7)}, {-8,-dts(8)}, {-3,-dts(8)}, {-1,-dts(8)}, {2,-dts(8)},
00504   {4,-dts(8)}, {5,-dts(8)}, {6,-dts(8)}, {7,-dts(8)}, {-7,-dts(9)},
00505   {-6,-dts(9)}, {-5,-dts(9)}, {-3,-dts(9)}, {1,-dts(9)}, {2,-dts(9)},
00506   {4,-dts(9)}, {8,-dts(9)}, {-7,-dts(10)}, {-6,-dts(10)}, {-4,-dts(10)},
00507   {-3,-dts(10)}, {-2,-dts(10)}, {1,-dts(10)}, {5,-dts(10)}, {8,-dts(10)},
00508   {-7,-dts(11)}, {-5,-dts(11)}, {-4,-dts(11)}, {-2,-dts(11)}, {-1,-dts(11)},
00509   {3,-dts(11)}, {6,-dts(11)}, {8,-dts(11)}, {-7,-dts(12)}, {-3,-dts(12)},
00510   {-2,-dts(12)}, {1,-dts(12)}, {4,-dts(12)}, {5,-dts(12)}, {6,-dts(12)},
00511   {8,-dts(12)}, {-6,-dts(13)}, {-5,-dts(13)}, {-4,-dts(13)}, {-3,-dts(13)},
00512   {1,-dts(13)}, {2,-dts(13)}, {7,-dts(13)}, {8,-dts(13)}, {-6,-dts(14)},
00513   {-3,-dts(14)}, {-2,-dts(14)}, {-1,-dts(14)}, {4,-dts(14)}, {5,-dts(14)},
00514   {7,-dts(14)}, {8,-dts(14)}, {-5,-dts(15)}, {-4,-dts(15)}, {-1,-dts(15)},
00515   {2,-dts(15)}, {3,-dts(15)}, {6,-dts(15)}, {7,-dts(15)}, {8,-dts(15)},
00516   {-4,-dts(16)}, {-2,-dts(16)}, {1,-dts(16)}, {3,-dts(16)}, {5,-dts(16)},
00517   {6,-dts(16)}, {7,-dts(16)}, {8,-dts(16)},{dts(1),dts(2),dts(3),dts(4),
00518   dts(5),dts(6),dts(7),dts(8),dts(9),dts(10),dts(11),dts(12),dts(13),dts(14),
00519   dts(15),dts(16)}]]),
00520   assert(length(f(2,8,ss_polynomial_2_8)[2]) = 4353),
00521   true)$
00522 
00523 okltest_ss_sbox_w_mul_ts_gen(f) := block([ss_sbox_w_mul_ts_CNF : sm2hm({})],
00524   assert(f(1,2,4,ss_polynomial_2_4) =
00525   [[1,2,3,4,5,6,7,8,dts(1),dts(2),dts(3),dts(4),dts(5),dts(6),dts(7),dts(8),
00526   dts(9),dts(10), dts(11),dts(12),dts(13),dts(14),dts(15),dts(16)],
00527   [{-3,-2,-1,4,5,6,7,8,dts(1)}, {-5,-4,-3,-2,-1,6,7,8,dts(2)},
00528   {-6,-4,-3,1,2,5,7,8,dts(3)}, {-6,-5,-4,-3,-1,2,7,8,dts(4)},
00529   {-7,-2,1,3,4,5,6,8,dts(5)}, {-7,-5,-4,-3,-2,1,6,8,dts(6)},
00530   {-7,-6,1,2,3,4,5,8,dts(7)}, {-7,-6,-5,-4,-2,1,3,8,dts(8)},
00531   {-8,-4,-2,-1,3,5,6,7,dts(9)}, {-8,-5,-1,2,3,4,6,7,dts(10)},
00532   {-8,-6,-3,1,2,4,5,7,dts(11)}, {-8,-6,-5,-4,-1,2,3,7,dts(12)},
00533   {-8,-7,-2,-1,3,4,5,6,dts(13)}, {-8,-7,-5,-4,1,2,3,6,dts(14)},
00534   {-8,-7,-6,-3,-2,1,4,5,dts(15)}, {-8,-7,-6,-5,-3,-1,2,4,dts(16)},
00535   {-8,-dts(1)}, {-7,-dts(1)}, {-6,-dts(1)}, {-5,-dts(1)}, {-4,-dts(1)},
00536   {1,-dts(1)}, {2,-dts(1)}, {3,-dts(1)}, {-8,-dts(2)}, {-7,-dts(2)},
00537   {-6,-dts(2)}, {1,-dts(2)}, {2,-dts(2)}, {3,-dts(2)}, {4,-dts(2)},
00538   {5,-dts(2)}, {-8,-dts(3)}, {-7,-dts(3)}, {-5,-dts(3)}, {-2,-dts(3)},
00539   {-1,-dts(3)}, {3,-dts(3)}, {4,-dts(3)}, {6,-dts(3)}, {-8,-dts(4)},
00540   {-7,-dts(4)}, {-2,-dts(4)}, {1,-dts(4)}, {3,-dts(4)}, {4,-dts(4)},
00541   {5,-dts(4)}, {6,-dts(4)}, {-8,-dts(5)}, {-6,-dts(5)}, {-5,-dts(5)},
00542   {-4,-dts(5)}, {-3,-dts(5)}, {-1,-dts(5)}, {2,-dts(5)}, {7,-dts(5)},
00543   {-8,-dts(6)}, {-6,-dts(6)}, {-1,-dts(6)}, {2,-dts(6)}, {3,-dts(6)},
00544   {4,-dts(6)}, {5,-dts(6)}, {7,-dts(6)}, {-8,-dts(7)}, {-5,-dts(7)},
00545   {-4,-dts(7)}, {-3,-dts(7)}, {-2,-dts(7)}, {-1,-dts(7)}, {6,-dts(7)},
00546   {7,-dts(7)}, {-8,-dts(8)}, {-3,-dts(8)}, {-1,-dts(8)}, {2,-dts(8)},
00547   {4,-dts(8)}, {5,-dts(8)}, {6,-dts(8)}, {7,-dts(8)}, {-7,-dts(9)},
00548   {-6,-dts(9)}, {-5,-dts(9)}, {-3,-dts(9)}, {1,-dts(9)}, {2,-dts(9)},
00549   {4,-dts(9)}, {8,-dts(9)}, {-7,-dts(10)}, {-6,-dts(10)}, {-4,-dts(10)},
00550   {-3,-dts(10)}, {-2,-dts(10)}, {1,-dts(10)}, {5,-dts(10)}, {8,-dts(10)},
00551   {-7,-dts(11)}, {-5,-dts(11)}, {-4,-dts(11)}, {-2,-dts(11)}, {-1,-dts(11)},
00552   {3,-dts(11)}, {6,-dts(11)}, {8,-dts(11)}, {-7,-dts(12)}, {-3,-dts(12)},
00553   {-2,-dts(12)}, {1,-dts(12)}, {4,-dts(12)}, {5,-dts(12)}, {6,-dts(12)},
00554   {8,-dts(12)}, {-6,-dts(13)}, {-5,-dts(13)}, {-4,-dts(13)}, {-3,-dts(13)},
00555   {1,-dts(13)}, {2,-dts(13)}, {7,-dts(13)}, {8,-dts(13)}, {-6,-dts(14)},
00556   {-3,-dts(14)}, {-2,-dts(14)}, {-1,-dts(14)}, {4,-dts(14)}, {5,-dts(14)},
00557   {7,-dts(14)}, {8,-dts(14)}, {-5,-dts(15)}, {-4,-dts(15)}, {-1,-dts(15)},
00558   {2,-dts(15)}, {3,-dts(15)}, {6,-dts(15)}, {7,-dts(15)}, {8,-dts(15)},
00559   {-4,-dts(16)}, {-2,-dts(16)}, {1,-dts(16)}, {3,-dts(16)}, {5,-dts(16)},
00560   {6,-dts(16)}, {7,-dts(16)}, {8,-dts(16)},{dts(1),dts(2),dts(3),dts(4),
00561   dts(5),dts(6),dts(7),dts(8),dts(9),dts(10),dts(11),dts(12),dts(13),dts(14),
00562   dts(15),dts(16)}]]),
00563   assert(length(f(1,2,8,ss_polynomial_2_8)[2]) = 4353),
00564   assert(f('x,2,4,ss_polynomial_2_4) =
00565     [[1,2,3,4,5,6,7,8,dts(1),dts(2),dts(3),dts(4),dts(5),dts(6),dts(7),dts(8),
00566     dts(9),dts(10),dts(11),dts(12),dts(13),dts(14),dts(15),dts(16)],
00567     [{-3,-2,-1,4,5,6,7,8,dts(1)},{-5,-4,-3,1,2,6,7,8,dts(2)},
00568      {-6,-2,1,3,4,5,7,8,dts(3)}, {-6,-5,1,2,3,4,7,8,dts(4)},
00569      {-7,-4,-2,-1,3,5,6,8,dts(5)},{-7,-5,-3,1,2,4,6,8,dts(6)},
00570      {-7,-6,-2,-1,3,4,5,8,dts(7)},{-7,-6,-5,-3,-2,1,4,8,dts(8)},
00571      {-8,-1,2,3,4,5,6,7,dts(9)},{-8,-5,-4,-1,2,3,6,7,dts(10)},
00572      {-8,-6,-4,1,2,3,5,7,dts(11)},{-8,-6,-5,-3,-1,2,4,7,dts(12)},
00573      {-8,-7,-4,-3,-2,-1,5,6,dts(13)},{-8,-7,-5,-4,-3,-1,2,6,dts(14)},
00574      {-8,-7,-6,-4,-3,-2,1,5,dts(15)},{-8,-7,-6,-5,-4,-2,1,3,dts(16)},
00575      {-8,-dts(1)},{-7,-dts(1)},{-6,-dts(1)},{-5,-dts(1)},{-4,-dts(1)},
00576      {1,-dts(1)},{2,-dts(1)},{3,-dts(1)},{-8,-dts(2)},{-7,-dts(2)},
00577      {-6,-dts(2)},{-2,-dts(2)},{-1,-dts(2)},{3,-dts(2)},{4,-dts(2)},
00578      {5,-dts(2)},{-8,-dts(3)},{-7,-dts(3)},{-5,-dts(3)},{-4,-dts(3)},
00579      {-3,-dts(3)},{-1,-dts(3)},{2,-dts(3)},{6,-dts(3)},{-8,-dts(4)},
00580      {-7,-dts(4)},{-4,-dts(4)},{-3,-dts(4)},{-2,-dts(4)},{-1,-dts(4)},
00581      {5,-dts(4)},{6,-dts(4)},{-8,-dts(5)},{-6,-dts(5)},{-5,-dts(5)},
00582      {-3,-dts(5)},{1,-dts(5)},{2,-dts(5)},{4,-dts(5)},{7,-dts(5)},
00583      {-8,-dts(6)},{-6,-dts(6)},{-4,-dts(6)},{-2,-dts(6)},{-1,-dts(6)},
00584      {3,-dts(6)},{5,-dts(6)},{7,-dts(6)},{-8,-dts(7)},{-5,-dts(7)},
00585      {-4,-dts(7)},{-3,-dts(7)},{1,-dts(7)},{2,-dts(7)},{6,-dts(7)},
00586      {7,-dts(7)},{-8,-dts(8)},{-4,-dts(8)},{-1,-dts(8)},{2,-dts(8)},
00587      {3,-dts(8)},{5,-dts(8)},{6,-dts(8)},{7,-dts(8)},{-7,-dts(9)},
00588      {-6,-dts(9)},{-5,-dts(9)},{-4,-dts(9)},{-3,-dts(9)},{-2,-dts(9)},
00589      {1,-dts(9)},{8,-dts(9)},{-7,-dts(10)},{-6,-dts(10)},{-3,-dts(10)},
00590      {-2,-dts(10)},{1,-dts(10)},{4,-dts(10)},{5,-dts(10)},{8,-dts(10)},
00591      {-7,-dts(11)},{-5,-dts(11)},{-3,-dts(11)},{-2,-dts(11)},
00592      {-1,-dts(11)},{4,-dts(11)},{6,-dts(11)},{8,-dts(11)},{-7,-dts(12)},
00593      {-4,-dts(12)},{-2,-dts(12)},{1,-dts(12)},{3,-dts(12)},{5,-dts(12)},
00594      {6,-dts(12)},{8,-dts(12)},{-6,-dts(13)},{-5,-dts(13)},{1,-dts(13)},
00595      {2,-dts(13)},{3,-dts(13)},{4,-dts(13)},{7,-dts(13)},{8,-dts(13)},
00596      {-6,-dts(14)},{-2,-dts(14)},{1,-dts(14)},{3,-dts(14)},{4,-dts(14)},
00597      {5,-dts(14)},{7,-dts(14)},{8,-dts(14)},{-5,-dts(15)},{-1,-dts(15)},
00598      {2,-dts(15)},{3,-dts(15)},{4,-dts(15)},{6,-dts(15)},{7,-dts(15)},
00599      {8,-dts(15)},{-3,-dts(16)},{-1,-dts(16)},{2,-dts(16)},{4,-dts(16)},
00600      {5,-dts(16)},{6,-dts(16)},{7,-dts(16)},{8,-dts(16)},
00601      {dts(1),dts(2),dts(3),dts(4),dts(5),dts(6),dts(7),dts(8),dts(9),dts(10),
00602      dts(11),dts(12),dts(13),dts(14),dts(15),dts(16)}]]),
00603   true)$
00604 
00605 okltest_ss_mixcolumn_ts_gen(f) := block([ss_mixcolumn_ts_CNF : sm2hm({})],
00606   if oklib_test_level = 0 then return(true),
00607   assert(f(2,4,ss_polynomial_2_4,ss_mixcolumns_matrix(2,4,1)) =
00608     [[1,2,3,4,5,6,7,8,dts(1),dts(2),dts(3),dts(4),dts(5),dts(6),dts(7),dts(8),
00609       dts(9),dts(10),dts(11),dts(12),dts(13),dts(14),dts(15),dts(16)],
00610      [{1,2,3,4,5,6,7,8,dts(1)},{-5,-1,2,3,4,6,7,8,dts(2)},
00611       {-6,-2,1,3,4,5,7,8,dts(3)},{-6,-5,-2,-1,3,4,7,8,dts(4)},
00612       {-7,-3,1,2,4,5,6,8,dts(5)},{-7,-5,-3,-1,2,4,6,8,dts(6)},
00613       {-7,-6,-3,-2,1,4,5,8,dts(7)},{-7,-6,-5,-3,-2,-1,4,8,dts(8)},
00614       {-8,-4,1,2,3,5,6,7,dts(9)},{-8,-5,-4,-1,2,3,6,7,dts(10)},
00615       {-8,-6,-4,-2,1,3,5,7,dts(11)},{-8,-6,-5,-4,-2,-1,3,7,dts(12)},
00616       {-8,-7,-4,-3,1,2,5,6,dts(13)},{-8,-7,-5,-4,-3,-1,2,6,dts(14)},
00617       {-8,-7,-6,-4,-3,-2,1,5,dts(15)},{-8,-7,-6,-5,-4,-3,-2,-1,dts(16)},
00618       {-8,-dts(1)},{-7,-dts(1)},{-6,-dts(1)},{-5,-dts(1)},{-4,-dts(1)},
00619       {-3,-dts(1)},{-2,-dts(1)},{-1,-dts(1)},{-8,-dts(2)},{-7,-dts(2)},
00620       {-6,-dts(2)},{-4,-dts(2)},{-3,-dts(2)},{-2,-dts(2)},{1,-dts(2)},
00621       {5,-dts(2)},{-8,-dts(3)},{-7,-dts(3)}, {-5,-dts(3)},{-4,-dts(3)},
00622       {-3,-dts(3)},{-1,-dts(3)},{2,-dts(3)},{6,-dts(3)},{-8,-dts(4)},
00623       {-7,-dts(4)},{-4,-dts(4)},{-3,-dts(4)},{1,-dts(4)},{2,-dts(4)},
00624       {5,-dts(4)},{6,-dts(4)}, {-8,-dts(5)},{-6,-dts(5)},{-5,-dts(5)},
00625       {-4,-dts(5)},{-2,-dts(5)},{-1,-dts(5)},{3,-dts(5)},{7,-dts(5)},
00626       {-8,-dts(6)},{-6,-dts(6)},{-4,-dts(6)},{-2,-dts(6)},{1,-dts(6)},
00627       {3,-dts(6)}, {5,-dts(6)},{7,-dts(6)},{-8,-dts(7)},{-5,-dts(7)},
00628       {-4,-dts(7)},{-1,-dts(7)},{2,-dts(7)},{3,-dts(7)},{6,-dts(7)},
00629       {7,-dts(7)},{-8,-dts(8)},{-4,-dts(8)},{1,-dts(8)},{2,-dts(8)},
00630       {3,-dts(8)},{5,-dts(8)},{6,-dts(8)},{7,-dts(8)},{-7,-dts(9)},
00631       {-6,-dts(9)},{-5,-dts(9)},{-3,-dts(9)},{-2,-dts(9)},{-1,-dts(9)},
00632       {4,-dts(9)},{8,-dts(9)},{-7,-dts(10)},{-6,-dts(10)},{-3,-dts(10)},
00633       {-2,-dts(10)},{1,-dts(10)},{4,-dts(10)},{5,-dts(10)},{8,-dts(10)},
00634       {-7,-dts(11)},{-5,-dts(11)},{-3,-dts(11)},{-1,-dts(11)},{2,-dts(11)},
00635       {4,-dts(11)},{6,-dts(11)},{8,-dts(11)},{-7,-dts(12)},{-3,-dts(12)},
00636       {1,-dts(12)},{2,-dts(12)},{4,-dts(12)},{5,-dts(12)},{6,-dts(12)},
00637       {8,-dts(12)},{-6,-dts(13)},{-5,-dts(13)},{-2,-dts(13)},{-1,-dts(13)},
00638       {3,-dts(13)},{4,-dts(13)},{7,-dts(13)},{8,-dts(13)},{-6,-dts(14)},
00639       {-2,-dts(14)},{1,-dts(14)},{3,-dts(14)},{4,-dts(14)},{5,-dts(14)},
00640       {7,-dts(14)},{8,-dts(14)},{-5,-dts(15)},{-1,-dts(15)},{2,-dts(15)},
00641       {3,-dts(15)},{4,-dts(15)},{6,-dts(15)},{7,-dts(15)},{8,-dts(15)},
00642       {1,-dts(16)},{2,-dts(16)},{3,-dts(16)},{4,-dts(16)},{5,-dts(16)},
00643       {6,-dts(16)},{7,-dts(16)},{8,-dts(16)},
00644       {dts(1),dts(2),dts(3),dts(4),dts(5),dts(6),dts(7),dts(8),dts(9),dts(10),
00645        dts(11),dts(12),dts(13),dts(14),dts(15),dts(16)}]]),
00646     assert(length(
00647         f(2,4,ss_polynomial_2_4,ss_mixcolumns_matrix(2,4,2))[2]) = 4353),
00648   true)$
00649 
00650 okltest_ss_round_column_ts_gen(f) := block(
00651   [ss_round_column_ts_CNF : sm2hm({})],
00652   if oklib_test_level = 0 then return(true),
00653   assert(f(2,4,ss_polynomial_2_4,
00654            ss_sbox_matrix(2,4),ss_affine_constant(2,4),
00655            ss_mixcolumns_matrix(2,4,1)) =
00656          [[1,2,3,4,5,6,7,8,dts(1),dts(2),dts(3),dts(4),dts(5),dts(6),dts(7),
00657            dts(8),dts(9),dts(10),dts(11),dts(12),dts(13),dts(14),dts(15),dts(16)],
00658           [{-3,-2,-1,4,5,6,7,8,dts(1)},{-5,-4,-3,-2,-1,6,7,8,dts(2)},
00659            {-6,-4,-3,1,2,5,7,8,dts(3)},{-6,-5,-4,-3,-1,2,7,8,dts(4)},
00660            {-7,-2,1,3,4,5,6,8,dts(5)},{-7,-5,-4,-3,-2,1,6,8,dts(6)},
00661            {-7,-6,1,2,3,4,5,8,dts(7)},{-7,-6,-5,-4,-2,1,3,8,dts(8)},
00662            {-8,-4,-2,-1,3,5,6,7,dts(9)},{-8,-5,-1,2,3,4,6,7,dts(10)},
00663            {-8,-6,-3,1,2,4,5,7,dts(11)},{-8,-6,-5,-4,-1,2,3,7,dts(12)},
00664            {-8,-7,-2,-1,3,4,5,6,dts(13)},{-8,-7,-5,-4,1,2,3,6,dts(14)},
00665            {-8,-7,-6,-3,-2,1,4,5,dts(15)},{-8,-7,-6,-5,-3,-1,2,4,dts(16)},
00666            {-8,-dts(1)},{-7,-dts(1)},{-6,-dts(1)},{-5,-dts(1)},{-4,-dts(1)},
00667            {1,-dts(1)},{2,-dts(1)},{3,-dts(1)},{-8,-dts(2)},{-7,-dts(2)},
00668            {-6,-dts(2)},{1,-dts(2)},{2,-dts(2)},{3,-dts(2)},{4,-dts(2)},
00669            {5,-dts(2)},{-8,-dts(3)},{-7,-dts(3)},{-5,-dts(3)},{-2,-dts(3)},
00670            {-1,-dts(3)},{3,-dts(3)},{4,-dts(3)},{6,-dts(3)},{-8,-dts(4)},
00671            {-7,-dts(4)},{-2,-dts(4)},{1,-dts(4)},{3,-dts(4)},{4,-dts(4)},
00672            {5,-dts(4)},{6,-dts(4)},{-8,-dts(5)},{-6,-dts(5)},{-5,-dts(5)},
00673            {-4,-dts(5)},{-3,-dts(5)},{-1,-dts(5)},{2,-dts(5)},{7,-dts(5)},
00674            {-8,-dts(6)},{-6,-dts(6)},{-1,-dts(6)},{2,-dts(6)},{3,-dts(6)},
00675            {4,-dts(6)},{5,-dts(6)},{7,-dts(6)},{-8,-dts(7)},{-5,-dts(7)},
00676            {-4,-dts(7)},{-3,-dts(7)},{-2,-dts(7)},{-1,-dts(7)},{6,-dts(7)},
00677            {7,-dts(7)},{-8,-dts(8)},{-3,-dts(8)},{-1,-dts(8)},{2,-dts(8)},
00678            {4,-dts(8)},{5,-dts(8)},{6,-dts(8)},{7,-dts(8)},{-7,-dts(9)},
00679            {-6,-dts(9)},{-5,-dts(9)},{-3,-dts(9)},{1,-dts(9)},{2,-dts(9)},
00680            {4,-dts(9)},{8,-dts(9)},{-7,-dts(10)},{-6,-dts(10)},{-4,-dts(10)},
00681            {-3,-dts(10)},{-2,-dts(10)},{1,-dts(10)},{5,-dts(10)},{8,-dts(10)},
00682            {-7,-dts(11)},{-5,-dts(11)},{-4,-dts(11)},{-2,-dts(11)},
00683            {-1,-dts(11)},{3,-dts(11)},{6,-dts(11)},{8,-dts(11)},{-7,-dts(12)},
00684            {-3,-dts(12)},{-2,-dts(12)},{1,-dts(12)},{4,-dts(12)},{5,-dts(12)},
00685            {6,-dts(12)},{8,-dts(12)},{-6,-dts(13)},{-5,-dts(13)},
00686            {-4,-dts(13)},{-3,-dts(13)},{1,-dts(13)},{2,-dts(13)},
00687            {7,-dts(13)},{8,-dts(13)},{-6,-dts(14)},{-3,-dts(14)},
00688            {-2,-dts(14)},{-1,-dts(14)},{4,-dts(14)},{5,-dts(14)},{7,-dts(14)},
00689            {8,-dts(14)},{-5,-dts(15)},{-4,-dts(15)},{-1,-dts(15)},
00690            {2,-dts(15)},{3,-dts(15)},{6,-dts(15)},{7,-dts(15)},{8,-dts(15)},
00691            {-4,-dts(16)},{-2,-dts(16)},{1,-dts(16)},{3,-dts(16)},{5,-dts(16)},
00692            {6,-dts(16)},{7,-dts(16)},{8,-dts(16)},
00693            {dts(1),dts(2),dts(3),dts(4),dts(5),dts(6),dts(7),dts(8),dts(9),
00694            dts(10),dts(11),dts(12),dts(13),dts(14),dts(15),dts(16)}]]),
00695     assert(length(
00696         f(2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4),ss_affine_constant(2,4),
00697           ss_mixcolumns_matrix(2,4,2))[2]) = 4353),
00698   true)$
00699 
00700 
00701 okltest_ss_sbox_pi_cst_cl(f) := block([cl],
00702   cl : f(["ss_sbox_cst", create_list(i,i,1,8),2,4,ss_polynomial_2_4]),
00703   assert(first(cl) = {-4,-3,-2,5}),
00704   assert(last(cl) = {3,7,8}),
00705   assert(length(cl) = 22),
00706   assert(ss_sbox_cnfp(fcl2fcs(cl2fcl(cl)), 2, 4, ss_polynomial_2_4)),
00707   cl : f(["ss_sbox_cst", create_list(i,i,1,16),2,8,ss_polynomial_2_8]),
00708   assert(first(cl) = {-10,-9,-7,-6,-5,3,4}),
00709   assert(last(cl) = {-4,5,7,11,13,14,15,16}),
00710   assert(length(cl) = 294),
00711   if oklib_test_level = 0 then return(true),
00712   assert(ss_sbox_cnfp(fcl2fcs(cl2fcl(cl)), 2, 8, ss_polynomial_2_8)),
00713   true)$
00714 
00715 okltest_ss_sbox_ts_var_l(f) := block([cst],
00716   cst : ["ss_sbox_cst", create_list(i,i,1,8),2,4,ss_polynomial_2_4,
00717          nounify(n)],
00718   namespace : cstt_namespace_new(ss_sbox_ts_namespace, cst),
00719   assert(f(cst) = create_list(
00720       namespace(ss_v(i,nounify(sbox_ts))),i,1,16)),
00721   cst : ["ss_sbox_cst", create_list(i,i,1,16),2,8,ss_polynomial_2_8,
00722          nounify(n)],
00723   namespace : cstt_namespace_new(ss_sbox_ts_namespace, cst),
00724   assert(f(cst) = create_list(
00725       namespace(ss_v(i,nounify(sbox_ts))),i,1,256)),
00726   true)$
00727 
00728 okltest_ss_sbox_ts_cst_cl(f) := block([cl,cst],
00729   cst : ["ss_sbox_cst", create_list(i,i,1,8),2,4,ss_polynomial_2_4,
00730          nounify(n)],
00731   namespace : cstt_namespace_new(ss_sbox_ts_namespace, cst),
00732   cl : f(cst),
00733   assert(first(cl) =
00734     {-3,-2,-1,4,5,6,7,8,namespace(ss_v(1,nounify(sbox_ts)))}),
00735   assert(last(rest(cl,-1)) = {8,-namespace(ss_v(16,nounify(sbox_ts)))}),
00736   assert(length(last(cl)) = 16),
00737   if oklib_test_level = 0 then return(true),
00738   cst : ["ss_sbox_cst", create_list(i,i,1,16),2,8,ss_polynomial_2_8,
00739          nounify(n)],
00740   namespace : cstt_namespace_new(ss_sbox_ts_namespace, cst),
00741   cl : f(cst),
00742   assert(first(cl) =
00743     {-7,-4,-2,1,3,5,6,8,9,10,11,12,13,14,15,16,
00744          namespace(ss_v(1,nounify(sbox_ts)))}),
00745   assert(last(rest(cl,-1)) =
00746     {16,
00747          -namespace(ss_v(256,nounify(sbox_ts)))}),
00748   assert(length(last(cl)) = 256),
00749   true)$
00750 
00751 okltest_ss_sbox_w_mul_ts_var_l(f) := block([cst],
00752   cst : ["ss_sbox_cst", create_list(i,i,1,8),1,2,4,ss_polynomial_2_4,
00753          nounify(n)],
00754   namespace : cstt_namespace_new(ss_sbox_w_mul_ts_namespace, cst),
00755   assert(f(cst) = create_list(
00756       namespace(ss_v(i,nounify(sbox_w_mul_ts))),i,1,16)),
00757   cst : ["ss_sbox_cst", create_list(i,i,1,16),1,2,8,ss_polynomial_2_8,
00758          nounify(n)],
00759   namespace : cstt_namespace_new(ss_sbox_w_mul_ts_namespace, cst),
00760   assert(f(cst) = create_list(
00761       namespace(ss_v(i,nounify(sbox_w_mul_ts))),i,1,256)),
00762   true)$
00763 
00764 okltest_ss_sbox_w_mul_ts_cst_cl(f) := block([cl,cst],
00765   cst : ["ss_sbox_cst", create_list(i,i,1,8),1,2,4,ss_polynomial_2_4,
00766          nounify(n)],
00767   namespace : cstt_namespace_new(ss_sbox_w_mul_ts_namespace, cst),
00768   cl : f(cst),
00769   assert(first(cl) =
00770     {-3,-2,-1,4,5,6,7,8,namespace(ss_v(1,nounify(sbox_w_mul_ts)))}),
00771   assert(last(rest(cl,-1)) = {8,-namespace(ss_v(16,nounify(sbox_w_mul_ts)))}),
00772   assert(length(last(cl)) = 16),
00773   if oklib_test_level = 0 then return(true),
00774   cst : ["ss_sbox_cst", create_list(i,i,1,16),1,2,8,ss_polynomial_2_8,
00775          nounify(n)],
00776   namespace : cstt_namespace_new(ss_sbox_w_mul_ts_namespace, cst),
00777   cl : f(cst),
00778   assert(first(cl) =
00779     {-7,-4,-2,1,3,5,6,8,9,10,11,12,13,14,15,16,
00780          namespace(ss_v(1,nounify(sbox_w_mul_ts)))}),
00781   assert(last(rest(cl,-1)) =
00782     {16,
00783     -namespace(ss_v(256,nounify(sbox_w_mul_ts)))}),
00784   assert(length(last(cl)) = 256),
00785   true)$
00786 
00787 okltest_ss_mul_pi_cst_cl(f) := block([cl],
00788   assert(length(f(["ss_mul_cst",create_list(i,i,1,8),x,2,4,ss_polynomial_2_4,
00789         'n])) = 9),
00790   assert(f(["ss_mul_cst",create_list(i,i,1,8),x+1,2,4,ss_polynomial_2_4,'n]) =
00791     [{-5,1,2},{-1,2,5},{-6,-3,-2},{-6,-5,-1,3},{-6,1,3,5},{-2,3,6},
00792      {-5,-3,-1,6},{-3,1,5,6},{-8,-4,-1},{-8,1,4},{-8,-7,-3},{-8,3,7},
00793      {-4,1,8},{-1,4,8},{-7,3,8},{-3,7,8}]),
00794   assert(f(["ss_mul_cst",create_list(i,i,1,16),x,2,8,ss_polynomial_2_8,'n]) =
00795     [{-16,-15,-8},{-16,8,15},{-15,1,8},{-14,7},{-13,-6,-1},{-13,6,16},
00796      {-12,-5,-1},{-12,1,5},{-11,4},{-10,3},{-9,2},{-8,1,15},{-7,14},{-6,13,16},
00797      {-5,1,12},{-4,11},{-3,10},{-2,9},{-1,5,12},{-1,6,13}]),
00798   true)$
00799 
00800 okltest_ss_mul_ts_var_l(f) := block([cst],
00801   cst : ["ss_mul_cst",create_list(i,i,1,8),x,2,4,ss_polynomial_2_4,
00802          nounify(n)],
00803   namespace : cstt_namespace_new(ss_mul_ts_namespace, cst),
00804   assert(f(cst) = create_list(
00805       namespace(ss_v(i,nounify(mul_ts))),i,1,16)),
00806   cst : ["ss_mul_cst",create_list(i,i,1,16),x,2,8,ss_polynomial_2_8,
00807          nounify(n)],
00808   namespace : cstt_namespace_new(ss_mul_ts_namespace, cst),
00809   assert(f(cst) = create_list(
00810       namespace(ss_v(i,nounify(mul_ts))),i,1,256)),
00811   true)$
00812 
00813 okltest_ss_mul_ts_cst_cl(f) := block([cl,cst],
00814   if oklib_test_level = 0 then return(true),
00815   cst : ["ss_mul_cst",create_list(i,i,1,8),x,2,4,ss_polynomial_2_4,
00816          nounify(n)],
00817   namespace : cstt_namespace_new(ss_mul_ts_namespace, cst),
00818   cl : f(cst),
00819   assert(first(cl) =
00820     {1,2,3,4,5,6,7,8,namespace(ss_v(1,nounify(mul_ts)))}),
00821   assert(last(rest(cl,-1)) =
00822     {8,-namespace(ss_v(16,nounify(mul_ts)))}),
00823   assert(length(last(cl)) = 16),
00824   if oklib_test_level = 0 then return(true),
00825   cst : ["ss_mul_cst",create_list(i,i,1,16),x,2,8,ss_polynomial_2_8,
00826          nounify(n)],
00827   namespace : cstt_namespace_new(ss_mul_ts_namespace, cst),
00828   cl : f(cst),
00829   assert(first(cl) =
00830     {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,
00831          namespace(ss_v(1,nounify(mul_ts)))}),
00832   assert(last(rest(cl,-1)) =
00833     {16,
00834          -namespace(ss_v(256,nounify(mul_ts)))}),
00835   assert(length(last(cl)) = 256),
00836   true)$
00837 
00838 okltest_ss_mixcolumn_ts_var_l(f) := block([cst],
00839   cst : ["ss_mixcolumn_cst",create_list(i,i,1,16),2,2,4,ss_polynomial_2_4,
00840          matrix([x+1,x],[x,x+1]),nounify(n)],
00841   namespace : cstt_namespace_new(ss_mixcolumn_ts_namespace, cst),
00842   assert(f(cst) = create_list(
00843       namespace(ss_v(i,nounify(mixcolumn_ts))),i,1,256)),
00844   true)$
00845 
00846 okltest_ss_mixcolumn_ts_cst_cl(f) := block([cl,cst],
00847   if oklib_test_level = 0 then return(true),
00848   cst : ["ss_mixcolumn_cst",create_list(i,i,1,16),2,2,4,ss_polynomial_2_4,
00849          matrix([x+1,x],[x,x+1]),nounify(n)],
00850   namespace : cstt_namespace_new(ss_mixcolumn_ts_namespace, cst),
00851   cl : f(cst),
00852   assert(first(cl) =
00853     {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,
00854       namespace(ss_v(1,nounify(mixcolumn_ts)))}),
00855   assert(last(rest(cl,-1)) =
00856     {16,-namespace(ss_v(256,nounify(mixcolumn_ts)))}),
00857   assert(length(last(cl)) = 256),
00858   true)$
00859 
00860 
00861 okltest_ss_round_column_ts_var_l(f) := block([cst],
00862   cst : ["ss_round_column_cst",create_list(i,i,1,16),2,2,4,ss_polynomial_2_4,
00863          ss_sbox_matrix(2,4), ss_affine_constant(2,4),
00864          ss_mixcolumns_matrix(2,4,2), nounify(n)],
00865   namespace : cstt_namespace_new(ss_round_column_ts_namespace, cst),
00866   assert(f(cst) = create_list(
00867       namespace(ss_v(i,nounify(round_column_ts))),i,1,256)),
00868   true)$
00869 
00870 okltest_ss_round_column_ts_cst_cl(f) := block([cl,cst],
00871   if oklib_test_level = 0 then return(true),
00872   cst : ["ss_round_column_cst",create_list(i,i,1,16),2,2,4,ss_polynomial_2_4,
00873          ss_sbox_matrix(2,4), ss_affine_constant(2,4),
00874          ss_mixcolumns_matrix(2,4,2), nounify(n)],
00875   namespace : cstt_namespace_new(ss_round_column_ts_namespace, cst),
00876   cl : f(cst),
00877   assert(first(cl) =
00878     {-7,-6,-5,-3,-2,-1,4,8,9,10,11,12,13,14,15,16,
00879       namespace(ss_v(1,nounify(round_column_ts)))}),
00880   assert(last(rest(cl,-1)) =
00881     {16,-namespace(ss_v(256,nounify(round_column_ts)))}),
00882   assert(length(last(cl)) = 256),
00883   true)$
00884 
00885