OKlibrary  0.2.1.6
GeneralisedConstraintTranslation.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 22.5.2011 (Swansea) */
00002 /* Copyright 2011, 2012 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/Cryptology/Lisp/Cryptanalysis/DataEncryptionStandard/tests/ConstraintTranslation.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00024 
00025 kill(f)$
00026 
00027 
00028 /* ***********************
00029    * The complete system *
00030    ***********************
00031 */
00032 
00033 okltest_des_sbox_output2inputs(f) := block(
00034   assert(f(1) = [1,2,3,4,5,6]),
00035   assert(f(2) = [1,2,3,4,5,6]),
00036   assert(f(3) = [1,2,3,4,5,6]),
00037   assert(f(4) = [1,2,3,4,5,6]),
00038   assert(f(5) = [7,8,9,10,11,12]),
00039   assert(f(6) = [7,8,9,10,11,12]),
00040   assert(f(7) = [7,8,9,10,11,12]),
00041   assert(f(8) = [7,8,9,10,11,12]),
00042   assert(f(9) = [13,14,15,16,17,18]),
00043   assert(f(10) = [13,14,15,16,17,18]),
00044   assert(f(11) = [13,14,15,16,17,18]),
00045   assert(f(12) = [13,14,15,16,17,18]),
00046   assert(f(13) = [19,20,21,22,23,24]),
00047   assert(f(14) = [19,20,21,22,23,24]),
00048   assert(f(15) = [19,20,21,22,23,24]),
00049   assert(f(16) = [19,20,21,22,23,24]),
00050   assert(f(17) = [25,26,27,28,29,30]),
00051   assert(f(18) = [25,26,27,28,29,30]),
00052   assert(f(19) = [25,26,27,28,29,30]),
00053   assert(f(20) = [25,26,27,28,29,30]),
00054   assert(f(21) = [31,32,33,34,35,36]),
00055   assert(f(22) = [31,32,33,34,35,36]),
00056   assert(f(23) = [31,32,33,34,35,36]),
00057   assert(f(24) = [31,32,33,34,35,36]),
00058   assert(f(25) = [37,38,39,40,41,42]),
00059   assert(f(26) = [37,38,39,40,41,42]),
00060   assert(f(27) = [37,38,39,40,41,42]),
00061   assert(f(28) = [37,38,39,40,41,42]),
00062   assert(f(29) = [43,44,45,46,47,48]),
00063   assert(f(30) = [43,44,45,46,47,48]),
00064   assert(f(31) = [43,44,45,46,47,48]),
00065   assert(f(32) = [43,44,45,46,47,48]),
00066   true)$
00067 
00068 okltest_des_sbox_outputs2inputs(f) := block(
00069   assert(f([]) = []),
00070   assert(
00071     okltest_des_sbox_output2inputs(buildq([f], lambda([i], f([i]))))),
00072   assert(f([1,5]) = [1,2,3,4,5,6,7,8,9,10,11,12]),
00073   assert(f([1,5,6]) = [1,2,3,4,5,6,7,8,9,10,11,12]),
00074   assert(f([1,5,6,9]) = [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18]),
00075   assert(f([1,9]) = [1,2,3,4,5,6,13,14,15,16,17,18]),
00076   true)$
00077 
00078 
00079 /* **************************************************************
00080    * Assignments to plaintext, key and ciphertext variables     *
00081    **************************************************************
00082 */
00083 
00084 okltest_des_cipher2fcl_gen(f) := block(
00085   assert(
00086     okltest_des_cipher2fcl(
00087       buildq([f],lambda([a],f(a,16))))),
00088   true)$
00089 
00090 okltest_des_cipher2pa_gen(f) := block(
00091   for r : 1 thru 16 do
00092     assert(f(create_list(und,i,1,64),r) = {}),
00093   for r : 1 thru 16 do
00094     assert(f(create_list(0,i,1,64), r) =
00095       setify(create_list(-desr_var(i,r_t), r_t,[r,r-1], i,1,32))),
00096   for r : 1 thru 16 do
00097     assert(f(create_list(1,i,1,64), r) =
00098       setify(create_list(desr_var(i,r_t), r_t,[r,r-1], i,1,32))),
00099   assert(okltest_des_cipher2pa(buildq([f],lambda([cipher], f(cipher,16))))),
00100   true)$
00101 
00102 okltest_des_random_pkctriple(f) := block(
00103   assert(map(binv2hexstr,f(1,1)) =
00104     ["FF4780EB6AC1F425","EEBC1448B8672F8C","EE03C5BF2AC1A160"]),
00105   assert(map(binv2hexstr,f(1,16)) =
00106     ["FF4780EB6AC1F425","EEBC1448B8672F8C","9AB8D366109AB260"]),
00107   assert(map(binv2hexstr,f(2,16)) =
00108     ["2F618A0F6F9D5CA8","EE79764806A319ED","476E21472ACCE009"]),
00109   if oklib_test_level = 0 then return(true),
00110   for r : 1 thru 16 do
00111     assert(map(binv2hexstr,f(1,r)) =
00112       ["FF4780EB6AC1F425","EEBC1448B8672F8C",
00113        des_encryption_hex_gen(r,"FF4780EB6AC1F425","EEBC1448B8672F8C")]),
00114   assert(map(binv2hexstr, f(2^75,1)) =
00115     ["97C4AA2F8C7F0AAC","D821CCC0B716A675","C384EB6B993F5FFC"]),
00116   true)$
00117 
00118 
00119 okltest_des_random_pkctriple_pa(f) := block(
00120   assert(f(1,1) =
00121     {desk(1),-desr(1,-1),-desr(1,0),desr(1,1),desk(2),desr(2,-1),
00122      desr(2,0),-desr(2,1),desk(3),desr(3,-1),desr(3,0),desr(3,1),
00123      -desk(4),desr(4,-1),-desr(4,0),-desr(4,1),desk(5),desr(5,-1),
00124      desr(5,0),-desr(5,1),desk(6),-desr(6,-1),desr(6,0),desr(6,1),
00125      desk(7),desr(7,-1),-desr(7,0),-desr(7,1),-desk(8),desr(8,-1),
00126      desr(8,0),desr(8,1),desk(9),-desr(9,-1),desr(9,0),-desr(9,1),
00127      -desk(10),desr(10,-1),desr(10,0),-desr(10,1),desk(11),
00128      -desr(11,-1),-desr(11,0),-desr(11,1),desk(12),-desr(12,-1),
00129      desr(12,0),-desr(12,1),desk(13),-desr(13,-1),desr(13,0),
00130      desr(13,1),desk(14),-desr(14,-1),-desr(14,0),-desr(14,1),
00131      -desk(15),-desr(15,-1),-desr(15,0),-desr(15,1),-desk(16),
00132      desr(16,-1),desr(16,0),-desr(16,1),-desk(17),desr(17,-1),
00133      -desr(17,0),-desr(17,1),-desk(18),desr(18,-1),-desr(18,0),
00134      -desr(18,1),-desk(19),-desr(19,-1),-desr(19,0),-desr(19,1),
00135      desk(20),-desr(20,-1),desr(20,0),-desr(20,1),-desk(21),
00136      -desr(21,-1),desr(21,0),desr(21,1),desk(22),-desr(22,-1),
00137      -desr(22,0),desr(22,1),-desk(23),desr(23,-1),-desr(23,0),
00138      -desr(23,1),-desk(24),desr(24,-1),desr(24,0),desr(24,1),
00139      -desk(25),desr(25,-1),-desr(25,0),-desr(25,1),desk(26),
00140      -desr(26,-1),-desr(26,0),desr(26,1),-desk(27),desr(27,-1),
00141      -desr(27,0),desr(27,1),-desk(28),-desr(28,-1),desr(28,0),
00142      -desr(28,1),desk(29),desr(29,-1),desr(29,0),desr(29,1),
00143      -desk(30),-desr(30,-1),-desr(30,0),desr(30,1),-desk(31),
00144      desr(31,-1),desr(31,0),desr(31,1),-desk(32),desr(32,-1),
00145      desr(32,0),-desr(32,1),desk(33),-desk(34),desk(35),desk(36),
00146      desk(37),-desk(38),-desk(39),-desk(40),-desk(41),desk(42),
00147      desk(43),-desk(44),-desk(45),desk(46),desk(47),desk(48),
00148      -desk(49),-desk(50),desk(51),-desk(52),desk(53),desk(54),
00149      desk(55),desk(56),desk(57),-desk(58),-desk(59),-desk(60),
00150      desk(61),desk(62),-desk(63),-desk(64)}),
00151   assert(f(1,16) =
00152     {desk(1),-desr(1,-1),-desr(1,0),-desr(1,15),desr(1,16),desk(2),
00153      desr(2,-1),desr(2,0),desr(2,15),-desr(2,16),desk(3),
00154      desr(3,-1),desr(3,0),desr(3,15),-desr(3,16),-desk(4),
00155      desr(4,-1),-desr(4,0),-desr(4,15),-desr(4,16),desk(5),
00156      desr(5,-1),desr(5,0),-desr(5,15),desr(5,16),desk(6),
00157      -desr(6,-1),desr(6,0),desr(6,15),desr(6,16),desk(7),
00158      desr(7,-1),-desr(7,0),desr(7,15),-desr(7,16),-desk(8),
00159      desr(8,-1),desr(8,0),desr(8,15),-desr(8,16),desk(9),
00160      -desr(9,-1),desr(9,0),desr(9,15),-desr(9,16),-desk(10),
00161      desr(10,-1),desr(10,0),desr(10,15),desr(10,16),desk(11),
00162      -desr(11,-1),-desr(11,0),-desr(11,15),desr(11,16),desk(12),
00163      -desr(12,-1),desr(12,0),-desr(12,15),desr(12,16),desk(13),
00164      -desr(13,-1),desr(13,0),desr(13,15),-desr(13,16),desk(14),
00165      -desr(14,-1),-desr(14,0),-desr(14,15),desr(14,16),-desk(15),
00166      -desr(15,-1),-desr(15,0),desr(15,15),desr(15,16),-desk(16),
00167      desr(16,-1),desr(16,0),-desr(16,15),desr(16,16),-desk(17),
00168      desr(17,-1),-desr(17,0),-desr(17,15),-desr(17,16),-desk(18),
00169      desr(18,-1),-desr(18,0),-desr(18,15),-desr(18,16),-desk(19),
00170      -desr(19,-1),-desr(19,0),desr(19,15),-desr(19,16),desk(20),
00171      -desr(20,-1),desr(20,0),-desr(20,15),-desr(20,16),-desk(21),
00172      -desr(21,-1),desr(21,0),-desr(21,15),desr(21,16),desk(22),
00173      -desr(22,-1),-desr(22,0),-desr(22,15),-desr(22,16),-desk(23),
00174      desr(23,-1),-desr(23,0),desr(23,15),-desr(23,16),-desk(24),
00175      desr(24,-1),desr(24,0),desr(24,15),-desr(24,16),-desk(25),
00176      desr(25,-1),-desr(25,0),-desr(25,15),-desr(25,16),desk(26),
00177      -desr(26,-1),-desr(26,0),desr(26,15),-desr(26,16),-desk(27),
00178      desr(27,-1),-desr(27,0),desr(27,15),-desr(27,16),-desk(28),
00179      -desr(28,-1),desr(28,0),-desr(28,15),-desr(28,16),desk(29),
00180      desr(29,-1),desr(29,0),desr(29,15),-desr(29,16),-desk(30),
00181      -desr(30,-1),-desr(30,0),desr(30,15),desr(30,16),-desk(31),
00182      desr(31,-1),desr(31,0),-desr(31,15),-desr(31,16),-desk(32),
00183      desr(32,-1),desr(32,0),desr(32,15),-desr(32,16),desk(33),
00184      -desk(34),desk(35),desk(36),desk(37),-desk(38),-desk(39),
00185      -desk(40),-desk(41),desk(42),desk(43),-desk(44),-desk(45),
00186      desk(46),desk(47),desk(48),-desk(49),-desk(50),desk(51),
00187      -desk(52),desk(53),desk(54),desk(55),desk(56),desk(57),
00188      -desk(58),-desk(59),-desk(60),desk(61),desk(62),-desk(63),
00189      -desk(64)}),
00190   true)$
00191 
00192 okltest_des_random_pkctriple_pa_std(f) := block(
00193   assert(f(1,1) =
00194     {-160,-156,-153,-151,-148,-147,-146,-145,-144,-143,-142,-140,
00195     -139,-138,-137,-135,-133,-132,-130,-126,-123,-122,-121,-119,
00196     -118,-115,-114,-113,-111,-110,-107,-103,-100,-97,-94,-92,-90,
00197     -86,-85,-84,-83,-79,-78,-77,-76,-75,-73,-70,-65,-64,-63,-60,
00198     -59,-58,-52,-50,-49,-45,-44,-41,-40,-39,-38,-34,-32,-31,-30,
00199     -28,-27,-25,-24,-23,-21,-19,-18,-17,-16,-15,-10,-8,-4,1,2,3,
00200     5,6,7,9,11,12,13,14,20,22,26,29,33,35,36,37,42,43,46,47,48,
00201     51,53,54,55,56,57,61,62,66,67,68,69,71,72,74,80,81,82,87,88,
00202     89,91,93,95,96,98,99,101,102,104,105,106,108,109,112,116,117,
00203     120,124,125,127,128,129,131,134,136,141,149,150,152,154,155,
00204     157,158,159}),
00205   assert(f(1,16) =
00206     {-1840,-1839,-1837,-1836,-1835,-1834,-1833,-1832,-1831,-1830,
00207      -1828,-1827,-1826,-1825,-1821,-1817,-1816,-1815,-1812,-1811,
00208      -1810,-1727,-1724,-1721,-1718,-1717,-1716,-1714,-1713,-1712,
00209      -1710,-1708,-1707,-1701,-1700,-1697,-126,-123,-122,-121,
00210      -119,-118,-115,-114,-113,-111,-110,-107,-103,-100,-97,-94,
00211      -92,-90,-86,-85,-84,-83,-79,-78,-77,-76,-75,-73,-70,-65,-64,
00212      -63,-60,-59,-58,-52,-50,-49,-45,-44,-41,-40,-39,-38,-34,-32,
00213      -31,-30,-28,-27,-25,-24,-23,-21,-19,-18,-17,-16,-15,-10,-8,
00214      -4,1,2,3,5,6,7,9,11,12,13,14,20,22,26,29,33,35,36,37,42,43,
00215      46,47,48,51,53,54,55,56,57,61,62,66,67,68,69,71,72,74,80,81,
00216      82,87,88,89,91,93,95,96,98,99,101,102,104,105,106,108,109,
00217      112,116,117,120,124,125,127,128,1698,1699,1702,1703,1704,
00218      1705,1706,1709,1711,1715,1719,1720,1722,1723,1725,1726,1728,
00219      1809,1813,1814,1818,1819,1820,1822,1823,1824,1829,1838}),
00220    assert(f(2,16) =
00221      {-1839,-1836,-1835,-1834,-1830,-1828,-1826,-1825,-1824,-1823,
00222       -1822,-1821,-1820,-1819,-1818,-1817,-1814,-1812,-1809,-1726,
00223       -1723,-1722,-1721,-1720,-1718,-1717,-1714,-1712,-1709,-1707,
00224       -1705,-1704,-1703,-1702,-1701,-1700,-1697,-127,-123,-122,
00225       -121,-119,-110,-109,-107,-106,-104,-103,-101,-100,-98,-94,
00226       -90,-89,-87,-86,-81,-80,-79,-78,-77,-76,-73,-72,-70,-69,-67,
00227       -65,-63,-60,-55,-54,-51,-50,-49,-46,-45,-44,-42,-40,-37,-36,
00228       -35,-34,-33,-32,-31,-30,-28,-27,-25,-24,-21,-17,-15,-14,-9,
00229       -8,-4,1,2,3,5,6,7,10,11,12,13,16,18,19,20,22,23,26,29,38,39,
00230       41,43,47,48,52,53,56,57,58,59,61,62,64,66,68,71,74,75,82,83,
00231       84,85,88,91,92,93,95,96,97,99,102,105,108,111,112,113,114,
00232       115,116,117,118,120,124,125,126,128,1698,1699,1706,1708,
00233       1710,1711,1713,1715,1716,1719,1724,1725,1727,1728,1810,1811,
00234       1813,1815,1816,1827,1829,1831,1832,1833,1837,1838,1840}),
00235   true)$
00236 
00237 okltest_des_random_pcpair_pa(f) := block(
00238   assert(f(1,1) =
00239     {-desr(1,-1),-desr(1,0),desr(1,1),desr(2,-1),desr(2,0),
00240      -desr(2,1),desr(3,-1),desr(3,0),desr(3,1),desr(4,-1),
00241      -desr(4,0),-desr(4,1),desr(5,-1),desr(5,0),-desr(5,1),
00242      -desr(6,-1),desr(6,0),desr(6,1),desr(7,-1),-desr(7,0),
00243      -desr(7,1),desr(8,-1),desr(8,0),desr(8,1),-desr(9,-1),
00244      desr(9,0),-desr(9,1),desr(10,-1),desr(10,0),-desr(10,1),
00245      -desr(11,-1),-desr(11,0),-desr(11,1),-desr(12,-1),
00246      desr(12,0),-desr(12,1),-desr(13,-1),desr(13,0),desr(13,1),
00247      -desr(14,-1),-desr(14,0),-desr(14,1),-desr(15,-1),
00248      -desr(15,0),-desr(15,1),desr(16,-1),desr(16,0),-desr(16,1),
00249      desr(17,-1),-desr(17,0),-desr(17,1),desr(18,-1),-desr(18,0),
00250      -desr(18,1),-desr(19,-1),-desr(19,0),-desr(19,1),
00251      -desr(20,-1),desr(20,0),-desr(20,1),-desr(21,-1),desr(21,0),
00252      desr(21,1),-desr(22,-1),-desr(22,0),desr(22,1),desr(23,-1),
00253      -desr(23,0),-desr(23,1),desr(24,-1),desr(24,0),desr(24,1),
00254      desr(25,-1),-desr(25,0),-desr(25,1),-desr(26,-1),
00255      -desr(26,0),desr(26,1),desr(27,-1),-desr(27,0),desr(27,1),
00256      -desr(28,-1),desr(28,0),-desr(28,1),desr(29,-1),desr(29,0),
00257      desr(29,1),-desr(30,-1),-desr(30,0),desr(30,1),desr(31,-1),
00258      desr(31,0),desr(31,1),desr(32,-1),desr(32,0),-desr(32,1)}),
00259   assert(f(1,16) =
00260     {-desr(1,-1),-desr(1,0),-desr(1,15),desr(1,16),desr(2,-1),
00261      desr(2,0),desr(2,15),-desr(2,16),desr(3,-1),desr(3,0),
00262      desr(3,15),-desr(3,16),desr(4,-1),-desr(4,0),-desr(4,15),
00263      -desr(4,16),desr(5,-1),desr(5,0),-desr(5,15),desr(5,16),
00264      -desr(6,-1),desr(6,0),desr(6,15),desr(6,16),desr(7,-1),
00265      -desr(7,0),desr(7,15),-desr(7,16),desr(8,-1),desr(8,0),
00266      desr(8,15),-desr(8,16),-desr(9,-1),desr(9,0),desr(9,15),
00267      -desr(9,16),desr(10,-1),desr(10,0),desr(10,15),desr(10,16),
00268      -desr(11,-1),-desr(11,0),-desr(11,15),desr(11,16),
00269      -desr(12,-1),desr(12,0),-desr(12,15),desr(12,16),
00270      -desr(13,-1),desr(13,0),desr(13,15),-desr(13,16),
00271      -desr(14,-1),-desr(14,0),-desr(14,15),desr(14,16),
00272      -desr(15,-1),-desr(15,0),desr(15,15),desr(15,16),
00273      desr(16,-1),desr(16,0),-desr(16,15),desr(16,16),desr(17,-1),
00274      -desr(17,0),-desr(17,15),-desr(17,16),desr(18,-1),
00275      -desr(18,0),-desr(18,15),-desr(18,16),-desr(19,-1),
00276      -desr(19,0),desr(19,15),-desr(19,16),-desr(20,-1),
00277      desr(20,0),-desr(20,15),-desr(20,16),-desr(21,-1),
00278      desr(21,0),-desr(21,15),desr(21,16),-desr(22,-1),
00279      -desr(22,0),-desr(22,15),-desr(22,16),desr(23,-1),
00280      -desr(23,0),desr(23,15),-desr(23,16),desr(24,-1),desr(24,0),
00281      desr(24,15),-desr(24,16),desr(25,-1),-desr(25,0),
00282      -desr(25,15),-desr(25,16),-desr(26,-1),-desr(26,0),
00283      desr(26,15),-desr(26,16),desr(27,-1),-desr(27,0),
00284      desr(27,15),-desr(27,16),-desr(28,-1),desr(28,0),
00285      -desr(28,15),-desr(28,16),desr(29,-1),desr(29,0),
00286      desr(29,15),-desr(29,16),-desr(30,-1),-desr(30,0),
00287      desr(30,15),desr(30,16),desr(31,-1),desr(31,0),-desr(31,15),
00288      -desr(31,16),desr(32,-1),desr(32,0),desr(32,15),
00289      -desr(32,16)}),
00290   assert(f(2,16) =
00291     {-desr(1,-1),desr(1,0),-desr(1,15),-desr(1,16),desr(2,-1),
00292      -desr(2,0),desr(2,15),desr(2,16),-desr(3,-1),desr(3,0),
00293      desr(3,15),desr(3,16),desr(4,-1),-desr(4,0),-desr(4,15),
00294      -desr(4,16),-desr(5,-1),-desr(5,0),-desr(5,15),desr(5,16),
00295      -desr(6,-1),desr(6,0),-desr(6,15),-desr(6,16),desr(7,-1),
00296      -desr(7,0),-desr(7,15),desr(7,16),-desr(8,-1),-desr(8,0),
00297      -desr(8,15),desr(8,16),-desr(9,-1),desr(9,0),-desr(9,15),
00298      -desr(9,16),desr(10,-1),-desr(10,0),desr(10,15),
00299      -desr(10,16),desr(11,-1),-desr(11,0),-desr(11,15),
00300      -desr(11,16),-desr(12,-1),desr(12,0),desr(12,15),
00301      -desr(12,16),-desr(13,-1),-desr(13,0),-desr(13,15),
00302      -desr(13,16),-desr(14,-1),-desr(14,0),desr(14,15),
00303      -desr(14,16),-desr(15,-1),desr(15,0),desr(15,15),
00304      -desr(15,16),-desr(16,-1),desr(16,0),-desr(16,15),
00305      -desr(16,16),-desr(17,-1),desr(17,0),desr(17,15),
00306      -desr(17,16),desr(18,-1),desr(18,0),-desr(18,15),
00307      -desr(18,16),desr(19,-1),desr(19,0),desr(19,15),desr(19,16),
00308      desr(20,-1),desr(20,0),desr(20,15),-desr(20,16),desr(21,-1),
00309      desr(21,0),-desr(21,15),desr(21,16),-desr(22,-1),desr(22,0),
00310      -desr(22,15),-desr(22,16),-desr(23,-1),-desr(23,0),
00311      desr(23,15),desr(23,16),desr(24,-1),desr(24,0),-desr(24,15),
00312      desr(24,16),-desr(25,-1),-desr(25,0),-desr(25,15),
00313      desr(25,16),-desr(26,-1),-desr(26,0),-desr(26,15),
00314      -desr(26,16),desr(27,-1),-desr(27,0),-desr(27,15),
00315      -desr(27,16),desr(28,-1),desr(28,0),desr(28,15),
00316      -desr(28,16),desr(29,-1),desr(29,0),desr(29,15),desr(29,16),
00317      -desr(30,-1),desr(30,0),-desr(30,15),desr(30,16),
00318      desr(31,-1),-desr(31,0),desr(31,15),-desr(31,16),
00319      desr(32,-1),desr(32,0),desr(32,15),desr(32,16)}),
00320   true)$
00321 
00322 okltest_des_random_pcpair_pa_std(f) := block(
00323   assert(f(1,1) =
00324     {-160,-156,-153,-151,-148,-147,-146,-145,-144,-143,-142,-140,
00325      -139,-138,-137,-135,-133,-132,-130,-126,-123,-122,-121,-119,
00326      -118,-115,-114,-113,-111,-110,-107,-103,-100,-97,-94,-92,
00327      -90,-86,-85,-84,-83,-79,-78,-77,-76,-75,-73,-70,-65,66,67,
00328      68,69,71,72,74,80,81,82,87,88,89,91,93,95,96,98,99,101,102,
00329      104,105,106,108,109,112,116,117,120,124,125,127,128,129,131,
00330      134,136,141,149,150,152,154,155,157,158,159}),
00331   assert(f(1,16) =
00332     {-1840,-1839,-1837,-1836,-1835,-1834,-1833,-1832,-1831,-1830,
00333      -1828,-1827,-1826,-1825,-1821,-1817,-1816,-1815,-1812,-1811,
00334      -1810,-1727,-1724,-1721,-1718,-1717,-1716,-1714,-1713,-1712,
00335      -1710,-1708,-1707,-1701,-1700,-1697,-126,-123,-122,-121,
00336      -119,-118,-115,-114,-113,-111,-110,-107,-103,-100,-97,-94,
00337      -92,-90,-86,-85,-84,-83,-79,-78,-77,-76,-75,-73,-70,-65,66,
00338      67,68,69,71,72,74,80,81,82,87,88,89,91,93,95,96,98,99,101,
00339      102,104,105,106,108,109,112,116,117,120,124,125,127,128,
00340      1698,1699,1702,1703,1704,1705,1706,1709,1711,1715,1719,1720,
00341      1722,1723,1725,1726,1728,1809,1813,1814,1818,1819,1820,1822,
00342      1823,1824,1829,1838}),
00343   assert(f(2,16) =
00344     {-1839,-1836,-1835,-1834,-1830,-1828,-1826,-1825,-1824,-1823,
00345      -1822,-1821,-1820,-1819,-1818,-1817,-1814,-1812,-1809,-1726,
00346      -1723,-1722,-1721,-1720,-1718,-1717,-1714,-1712,-1709,-1707,
00347      -1705,-1704,-1703,-1702,-1701,-1700,-1697,-127,-123,-122,
00348      -121,-119,-110,-109,-107,-106,-104,-103,-101,-100,-98,-94,
00349      -90,-89,-87,-86,-81,-80,-79,-78,-77,-76,-73,-72,-70,-69,-67,
00350      -65,66,68,71,74,75,82,83,84,85,88,91,92,93,95,96,97,99,102,
00351      105,108,111,112,113,114,115,116,117,118,120,124,125,126,128,
00352      1698,1699,1706,1708,1710,1711,1713,1715,1716,1719,1724,1725,
00353      1727,1728,1810,1811,1813,1815,1816,1827,1829,1831,1832,1833,
00354      1837,1838,1840}),
00355   true)$
00356 
00357 okltest_des_random_pkpair_pa(f) := block([phi],
00358   phi : f(1,1),
00359   asset(phi =
00360     {desk(1),-desr(1,-1),-desr(1,0),desk(2),desr(2,-1),desr(2,0),
00361      desk(3),desr(3,-1),desr(3,0),-desk(4),desr(4,-1),-desr(4,0),
00362      desk(5),desr(5,-1),desr(5,0),desk(6),-desr(6,-1),desr(6,0),
00363      desk(7),desr(7,-1),-desr(7,0),-desk(8),desr(8,-1),desr(8,0),
00364      desk(9),-desr(9,-1),desr(9,0),-desk(10),desr(10,-1),
00365      desr(10,0),desk(11),-desr(11,-1),-desr(11,0),desk(12),
00366      -desr(12,-1),desr(12,0),desk(13),-desr(13,-1),desr(13,0),
00367      desk(14),-desr(14,-1),-desr(14,0),-desk(15),-desr(15,-1),
00368      -desr(15,0),-desk(16),desr(16,-1),desr(16,0),-desk(17),
00369      desr(17,-1),-desr(17,0),-desk(18),desr(18,-1),-desr(18,0),
00370      -desk(19),-desr(19,-1),-desr(19,0),desk(20),-desr(20,-1),
00371      desr(20,0),-desk(21),-desr(21,-1),desr(21,0),desk(22),
00372      -desr(22,-1),-desr(22,0),-desk(23),desr(23,-1),-desr(23,0),
00373      -desk(24),desr(24,-1),desr(24,0),-desk(25),desr(25,-1),
00374      -desr(25,0),desk(26),-desr(26,-1),-desr(26,0),-desk(27),
00375      desr(27,-1),-desr(27,0),-desk(28),-desr(28,-1),desr(28,0),
00376      desk(29),desr(29,-1),desr(29,0),-desk(30),-desr(30,-1),
00377      -desr(30,0),-desk(31),desr(31,-1),desr(31,0),-desk(32),
00378      desr(32,-1),desr(32,0),desk(33),-desk(34),desk(35),desk(36),
00379      desk(37),-desk(38),-desk(39),-desk(40),-desk(41),desk(42),
00380      desk(43),-desk(44),-desk(45),desk(46),desk(47),desk(48),
00381      -desk(49),-desk(50),desk(51),-desk(52),desk(53),desk(54),
00382      desk(55),desk(56),desk(57),-desk(58),-desk(59),-desk(60),
00383      desk(61),desk(62),-desk(63),-desk(64)}),
00384   assert(phi = f(1,16)),
00385   assert(f(2,16) =
00386     {desk(1),-desr(1,-1),desr(1,0),desk(2),desr(2,-1),-desr(2,0),
00387      desk(3),-desr(3,-1),desr(3,0),-desk(4),desr(4,-1),
00388      -desr(4,0),desk(5),-desr(5,-1),-desr(5,0),desk(6),
00389      -desr(6,-1),desr(6,0),desk(7),desr(7,-1),-desr(7,0),
00390      -desk(8),-desr(8,-1),-desr(8,0),-desk(9),-desr(9,-1),
00391      desr(9,0),desk(10),desr(10,-1),-desr(10,0),desk(11),
00392      desr(11,-1),-desr(11,0),desk(12),-desr(12,-1),desr(12,0),
00393      desk(13),-desr(13,-1),-desr(13,0),-desk(14),-desr(14,-1),
00394      -desr(14,0),-desk(15),-desr(15,-1),desr(15,0),desk(16),
00395      -desr(16,-1),desr(16,0),-desk(17),-desr(17,-1),desr(17,0),
00396      desk(18),desr(18,-1),desr(18,0),desk(19),desr(19,-1),
00397      desr(19,0),desk(20),desr(20,-1),desr(20,0),-desk(21),
00398      desr(21,-1),desr(21,0),desk(22),-desr(22,-1),desr(22,0),
00399      desk(23),-desr(23,-1),-desr(23,0),-desk(24),desr(24,-1),
00400      desr(24,0),-desk(25),-desr(25,-1),-desr(25,0),desk(26),
00401      -desr(26,-1),-desr(26,0),-desk(27),desr(27,-1),-desr(27,0),
00402      -desk(28),desr(28,-1),desr(28,0),desk(29),desr(29,-1),
00403      desr(29,0),-desk(30),-desr(30,-1),desr(30,0),-desk(31),
00404      desr(31,-1),-desr(31,0),-desk(32),desr(32,-1),desr(32,0),
00405      -desk(33),-desk(34),-desk(35),-desk(36),-desk(37),desk(38),
00406      desk(39),-desk(40),desk(41),-desk(42),desk(43),-desk(44),
00407      -desk(45),-desk(46),desk(47),desk(48),-desk(49),-desk(50),
00408      -desk(51),desk(52),desk(53),-desk(54),-desk(55),desk(56),
00409      desk(57),desk(58),desk(59),-desk(60),desk(61),desk(62),
00410      -desk(63),desk(64)}),
00411   true)$
00412 
00413 okltest_des_random_pkpair_pa_std(f) := block([phi],
00414   phi : f(1,1),
00415   assert(phi =
00416     {-126,-123,-122,-121,-119,-118,-115,-114,-113,-111,-110,-107,
00417      -103,-100,-97,-94,-92,-90,-86,-85,-84,-83,-79,-78,-77,-76,
00418      -75,-73,-70,-65,-64,-63,-60,-59,-58,-52,-50,-49,-45,-44,-41,
00419      -40,-39,-38,-34,-32,-31,-30,-28,-27,-25,-24,-23,-21,-19,-18,
00420      -17,-16,-15,-10,-8,-4,1,2,3,5,6,7,9,11,12,13,14,20,22,26,29,
00421      33,35,36,37,42,43,46,47,48,51,53,54,55,56,57,61,62,66,67,68,
00422      69,71,72,74,80,81,82,87,88,89,91,93,95,96,98,99,101,102,104,
00423      105,106,108,109,112,116,117,120,124,125,127,128}),
00424   assert(f(1,16) = phi),
00425   assert(f(2,16) =
00426     {-127,-123,-122,-121,-119,-110,-109,-107,-106,-104,-103,-101,
00427          -100,-98,-94,-90,-89,-87,-86,-81,-80,-79,-78,-77,-76,-73,
00428          -72,-70,-69,-67,-65,-63,-60,-55,-54,-51,-50,-49,-46,-45,-44,
00429          -42,-40,-37,-36,-35,-34,-33,-32,-31,-30,-28,-27,-25,-24,-21,
00430          -17,-15,-14,-9,-8,-4,1,2,3,5,6,7,10,11,12,13,16,18,19,20,22,
00431          23,26,29,38,39,41,43,47,48,52,53,56,57,58,59,61,62,64,66,68,
00432          71,74,75,82,83,84,85,88,91,92,93,95,96,97,99,102,105,108,
00433          111,112,113,114,115,116,117,118,120,124,125,126,128}),
00434   true)$
00435 
00436 okltest_des_random_kcpair_pa(f) := block(
00437   assert(f(1,1) =
00438     {desk(1),-desr(1,0),desr(1,1),desk(2),desr(2,0),-desr(2,1),
00439      desk(3),desr(3,0),desr(3,1),-desk(4),-desr(4,0),-desr(4,1),
00440      desk(5),desr(5,0),-desr(5,1),desk(6),desr(6,0),desr(6,1),
00441      desk(7),-desr(7,0),-desr(7,1),-desk(8),desr(8,0),desr(8,1),
00442      desk(9),desr(9,0),-desr(9,1),-desk(10),desr(10,0),
00443      -desr(10,1),desk(11),-desr(11,0),-desr(11,1),desk(12),
00444      desr(12,0),-desr(12,1),desk(13),desr(13,0),desr(13,1),
00445      desk(14),-desr(14,0),-desr(14,1),-desk(15),-desr(15,0),
00446      -desr(15,1),-desk(16),desr(16,0),-desr(16,1),-desk(17),
00447      -desr(17,0),-desr(17,1),-desk(18),-desr(18,0),-desr(18,1),
00448      -desk(19),-desr(19,0),-desr(19,1),desk(20),desr(20,0),
00449      -desr(20,1),-desk(21),desr(21,0),desr(21,1),desk(22),
00450      -desr(22,0),desr(22,1),-desk(23),-desr(23,0),-desr(23,1),
00451      -desk(24),desr(24,0),desr(24,1),-desk(25),-desr(25,0),
00452      -desr(25,1),desk(26),-desr(26,0),desr(26,1),-desk(27),
00453      -desr(27,0),desr(27,1),-desk(28),desr(28,0),-desr(28,1),
00454      desk(29),desr(29,0),desr(29,1),-desk(30),-desr(30,0),
00455      desr(30,1),-desk(31),desr(31,0),desr(31,1),-desk(32),
00456      desr(32,0),-desr(32,1),desk(33),-desk(34),desk(35),desk(36),
00457      desk(37),-desk(38),-desk(39),-desk(40),-desk(41),desk(42),
00458      desk(43),-desk(44),-desk(45),desk(46),desk(47),desk(48),
00459      -desk(49),-desk(50),desk(51),-desk(52),desk(53),desk(54),
00460      desk(55),desk(56),desk(57),-desk(58),-desk(59),-desk(60),
00461      desk(61),desk(62),-desk(63),-desk(64)}),
00462   assert(f(1,16) =
00463     {desk(1),-desr(1,15),desr(1,16),desk(2),desr(2,15),
00464      -desr(2,16),desk(3),desr(3,15),-desr(3,16),-desk(4),
00465      -desr(4,15),-desr(4,16),desk(5),-desr(5,15),desr(5,16),
00466      desk(6),desr(6,15),desr(6,16),desk(7),desr(7,15),
00467      -desr(7,16),-desk(8),desr(8,15),-desr(8,16),desk(9),
00468      desr(9,15),-desr(9,16),-desk(10),desr(10,15),desr(10,16),
00469      desk(11),-desr(11,15),desr(11,16),desk(12),-desr(12,15),
00470      desr(12,16),desk(13),desr(13,15),-desr(13,16),desk(14),
00471      -desr(14,15),desr(14,16),-desk(15),desr(15,15),desr(15,16),
00472      -desk(16),-desr(16,15),desr(16,16),-desk(17),-desr(17,15),
00473      -desr(17,16),-desk(18),-desr(18,15),-desr(18,16),-desk(19),
00474      desr(19,15),-desr(19,16),desk(20),-desr(20,15),-desr(20,16),
00475      -desk(21),-desr(21,15),desr(21,16),desk(22),-desr(22,15),
00476      -desr(22,16),-desk(23),desr(23,15),-desr(23,16),-desk(24),
00477      desr(24,15),-desr(24,16),-desk(25),-desr(25,15),
00478      -desr(25,16),desk(26),desr(26,15),-desr(26,16),-desk(27),
00479      desr(27,15),-desr(27,16),-desk(28),-desr(28,15),
00480      -desr(28,16),desk(29),desr(29,15),-desr(29,16),-desk(30),
00481      desr(30,15),desr(30,16),-desk(31),-desr(31,15),-desr(31,16),
00482      -desk(32),desr(32,15),-desr(32,16),desk(33),-desk(34),
00483      desk(35),desk(36),desk(37),-desk(38),-desk(39),-desk(40),
00484      -desk(41),desk(42),desk(43),-desk(44),-desk(45),desk(46),
00485      desk(47),desk(48),-desk(49),-desk(50),desk(51),-desk(52),
00486      desk(53),desk(54),desk(55),desk(56),desk(57),-desk(58),
00487      -desk(59),-desk(60),desk(61),desk(62),-desk(63),-desk(64)}),
00488   assert(f(2,16) =
00489     {desk(1),-desr(1,15),-desr(1,16),desk(2),desr(2,15),
00490      desr(2,16),desk(3),desr(3,15),desr(3,16),-desk(4),
00491      -desr(4,15),-desr(4,16),desk(5),-desr(5,15),desr(5,16),
00492      desk(6),-desr(6,15),-desr(6,16),desk(7),-desr(7,15),
00493      desr(7,16),-desk(8),-desr(8,15),desr(8,16),-desk(9),
00494      -desr(9,15),-desr(9,16),desk(10),desr(10,15),-desr(10,16),
00495      desk(11),-desr(11,15),-desr(11,16),desk(12),desr(12,15),
00496      -desr(12,16),desk(13),-desr(13,15),-desr(13,16),-desk(14),
00497      desr(14,15),-desr(14,16),-desk(15),desr(15,15),-desr(15,16),
00498      desk(16),-desr(16,15),-desr(16,16),-desk(17),desr(17,15),
00499      -desr(17,16),desk(18),-desr(18,15),-desr(18,16),desk(19),
00500      desr(19,15),desr(19,16),desk(20),desr(20,15),-desr(20,16),
00501      -desk(21),-desr(21,15),desr(21,16),desk(22),-desr(22,15),
00502      -desr(22,16),desk(23),desr(23,15),desr(23,16),-desk(24),
00503      -desr(24,15),desr(24,16),-desk(25),-desr(25,15),desr(25,16),
00504      desk(26),-desr(26,15),-desr(26,16),-desk(27),-desr(27,15),
00505      -desr(27,16),-desk(28),desr(28,15),-desr(28,16),desk(29),
00506      desr(29,15),desr(29,16),-desk(30),-desr(30,15),desr(30,16),
00507      -desk(31),desr(31,15),-desr(31,16),-desk(32),desr(32,15),
00508      desr(32,16),-desk(33),-desk(34),-desk(35),-desk(36),
00509      -desk(37),desk(38),desk(39),-desk(40),desk(41),-desk(42),
00510      desk(43),-desk(44),-desk(45),-desk(46),desk(47),desk(48),
00511      -desk(49),-desk(50),-desk(51),desk(52),desk(53),-desk(54),
00512      -desk(55),desk(56),desk(57),desk(58),desk(59),-desk(60),
00513      desk(61),desk(62),-desk(63),desk(64)}),
00514   true)$
00515 
00516 okltest_des_random_kcpair_pa_std(f) := block(
00517   assert(f(1,1) =
00518     {-160,-156,-153,-151,-148,-147,-146,-145,-144,-143,-142,-140,
00519      -139,-138,-137,-135,-133,-132,-130,-126,-123,-122,-121,-119,
00520      -118,-115,-114,-113,-111,-110,-107,-103,-100,-97,-64,-63,
00521      -60,-59,-58,-52,-50,-49,-45,-44,-41,-40,-39,-38,-34,-32,-31,
00522      -30,-28,-27,-25,-24,-23,-21,-19,-18,-17,-16,-15,-10,-8,-4,1,
00523      2,3,5,6,7,9,11,12,13,14,20,22,26,29,33,35,36,37,42,43,46,47,
00524      48,51,53,54,55,56,57,61,62,98,99,101,102,104,105,106,108,
00525      109,112,116,117,120,124,125,127,128,129,131,134,136,141,149,
00526      150,152,154,155,157,158,159}),
00527   assert(f(1,16) =
00528     {-1840,-1839,-1837,-1836,-1835,-1834,-1833,-1832,-1831,-1830,
00529      -1828,-1827,-1826,-1825,-1821,-1817,-1816,-1815,-1812,-1811,
00530      -1810,-1727,-1724,-1721,-1718,-1717,-1716,-1714,-1713,-1712,
00531      -1710,-1708,-1707,-1701,-1700,-1697,-64,-63,-60,-59,-58,-52,
00532      -50,-49,-45,-44,-41,-40,-39,-38,-34,-32,-31,-30,-28,-27,-25,
00533      -24,-23,-21,-19,-18,-17,-16,-15,-10,-8,-4,1,2,3,5,6,7,9,11,
00534      12,13,14,20,22,26,29,33,35,36,37,42,43,46,47,48,51,53,54,55,
00535      56,57,61,62,1698,1699,1702,1703,1704,1705,1706,1709,1711,
00536      1715,1719,1720,1722,1723,1725,1726,1728,1809,1813,1814,1818,
00537      1819,1820,1822,1823,1824,1829,1838}),
00538   assert(f(2,16) =
00539     {-1839,-1836,-1835,-1834,-1830,-1828,-1826,-1825,-1824,-1823,
00540      -1822,-1821,-1820,-1819,-1818,-1817,-1814,-1812,-1809,-1726,
00541      -1723,-1722,-1721,-1720,-1718,-1717,-1714,-1712,-1709,-1707,
00542      -1705,-1704,-1703,-1702,-1701,-1700,-1697,-63,-60,-55,-54,
00543      -51,-50,-49,-46,-45,-44,-42,-40,-37,-36,-35,-34,-33,-32,-31,
00544      -30,-28,-27,-25,-24,-21,-17,-15,-14,-9,-8,-4,1,2,3,5,6,7,10,
00545      11,12,13,16,18,19,20,22,23,26,29,38,39,41,43,47,48,52,53,56,
00546      57,58,59,61,62,64,1698,1699,1706,1708,1710,1711,1713,1715,
00547      1716,1719,1724,1725,1727,1728,1810,1811,1813,1815,1816,1827,
00548      1829,1831,1832,1833,1837,1838,1840}),
00549   true)$
00550