OKlibrary  0.2.1.6
ConstraintTranslation.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 25.3.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/TestSystem/Lisp/Asserts.mac")$
00023 
00024 kill(f)$
00025 
00026 
00027 /* *******************
00028    * xor-Constraints *
00029    *******************
00030 */
00031 
00032 okltest_des_xor_desi(f) := block(
00033   assert(f(1) =
00034     [[[desr(32,0),desk(10),desi(1,1)],0],[[desr(1,0),desk(51),desi(2,1)],0],
00035     [[desr(2,0),desk(34),desi(3,1)],0],[[desr(3,0),desk(60),desi(4,1)],0],
00036     [[desr(4,0),desk(49),desi(5,1)],0],[[desr(5,0),desk(17),desi(6,1)],0],
00037     [[desr(4,0),desk(33),desi(7,1)],0],[[desr(5,0),desk(57),desi(8,1)],0],
00038     [[desr(6,0),desk(2),desi(9,1)],0],[[desr(7,0),desk(9),desi(10,1)],0],
00039     [[desr(8,0),desk(19),desi(11,1)],0],[[desr(9,0),desk(42),desi(12,1)],0],
00040     [[desr(8,0),desk(3),desi(13,1)],0],[[desr(9,0),desk(35),desi(14,1)],0],
00041     [[desr(10,0),desk(26),desi(15,1)],0],[[desr(11,0),desk(25),desi(16,1)],0],
00042     [[desr(12,0),desk(44),desi(17,1)],0],[[desr(13,0),desk(58),desi(18,1)],0],
00043     [[desr(12,0),desk(59),desi(19,1)],0],[[desr(13,0),desk(1),desi(20,1)],0],
00044     [[desr(14,0),desk(36),desi(21,1)],0],[[desr(15,0),desk(27),desi(22,1)],0],
00045     [[desr(16,0),desk(18),desi(23,1)],0],[[desr(17,0),desk(41),desi(24,1)],0],
00046     [[desr(16,0),desk(22),desi(25,1)],0],[[desr(17,0),desk(28),desi(26,1)],0],
00047     [[desr(18,0),desk(39),desi(27,1)],0],[[desr(19,0),desk(54),desi(28,1)],0],
00048     [[desr(20,0),desk(37),desi(29,1)],0],[[desr(21,0),desk(4),desi(30,1)],0],
00049     [[desr(20,0),desk(47),desi(31,1)],0],[[desr(21,0),desk(30),desi(32,1)],0],
00050     [[desr(22,0),desk(5),desi(33,1)],0],[[desr(23,0),desk(53),desi(34,1)],0],
00051     [[desr(24,0),desk(23),desi(35,1)],0],[[desr(25,0),desk(29),desi(36,1)],0],
00052     [[desr(24,0),desk(61),desi(37,1)],0],[[desr(25,0),desk(21),desi(38,1)],0],
00053     [[desr(26,0),desk(38),desi(39,1)],0],[[desr(27,0),desk(63),desi(40,1)],0],
00054     [[desr(28,0),desk(15),desi(41,1)],0],[[desr(29,0),desk(20),desi(42,1)],0],
00055     [[desr(28,0),desk(45),desi(43,1)],0],[[desr(29,0),desk(14),desi(44,1)],0],
00056     [[desr(30,0),desk(13),desi(45,1)],0],[[desr(31,0),desk(62),desi(46,1)],0],
00057     [[desr(32,0),desk(55),desi(47,1)],0],[[desr(1,0),desk(31),desi(48,1)],0]]),
00058   assert(f(8) =
00059     [[[desr(32,7),desk(36),desi(1,8)],0],[[desr(1,7),desk(41),desi(2,8)],0],
00060     [[desr(2,7),desk(60),desi(3,8)],0],[[desr(3,7),desk(50),desi(4,8)],0],
00061     [[desr(4,7),desk(10),desi(5,8)],0],[[desr(5,7),desk(43),desi(6,8)],0],
00062     [[desr(4,7),desk(59),desi(7,8)],0],[[desr(5,7),desk(18),desi(8,8)],0],
00063     [[desr(6,7),desk(57),desi(9,8)],0],[[desr(7,7),desk(35),desi(10,8)],0],
00064     [[desr(8,7),desk(9),desi(11,8)],0],[[desr(9,7),desk(3),desi(12,8)],0],
00065     [[desr(8,7),desk(58),desi(13,8)],0],[[desr(9,7),desk(25),desi(14,8)],0],
00066     [[desr(10,7),desk(52),desi(15,8)],0],[[desr(11,7),desk(51),desi(16,8)],0],
00067     [[desr(12,7),desk(34),desi(17,8)],0],[[desr(13,7),desk(19),desi(18,8)],0],
00068     [[desr(12,7),desk(49),desi(19,8)],0],[[desr(13,7),desk(27),desi(20,8)],0],
00069     [[desr(14,7),desk(26),desi(21,8)],0],[[desr(15,7),desk(17),desi(22,8)],0],
00070     [[desr(16,7),desk(44),desi(23,8)],0],[[desr(17,7),desk(2),desi(24,8)],0],
00071     [[desr(16,7),desk(12),desi(25,8)],0],[[desr(17,7),desk(54),desi(26,8)],0],
00072     [[desr(18,7),desk(61),desi(27,8)],0],[[desr(19,7),desk(13),desi(28,8)],0],
00073     [[desr(20,7),desk(31),desi(29,8)],0],[[desr(21,7),desk(30),desi(30,8)],0],
00074     [[desr(20,7),desk(6),desi(31,8)],0],[[desr(21,7),desk(20),desi(32,8)],0],
00075     [[desr(22,7),desk(62),desi(33,8)],0],[[desr(23,7),desk(47),desi(34,8)],0],
00076     [[desr(24,7),desk(45),desi(35,8)],0],[[desr(25,7),desk(23),desi(36,8)],0],
00077     [[desr(24,7),desk(55),desi(37,8)],0],[[desr(25,7),desk(15),desi(38,8)],0],
00078     [[desr(26,7),desk(28),desi(39,8)],0],[[desr(27,7),desk(22),desi(40,8)],0],
00079     [[desr(28,7),desk(37),desi(41,8)],0],[[desr(29,7),desk(46),desi(42,8)],0],
00080     [[desr(28,7),desk(39),desi(43,8)],0],[[desr(29,7),desk(4),desi(44,8)],0],
00081     [[desr(30,7),desk(7),desi(45,8)],0],[[desr(31,7),desk(21),desi(46,8)],0],
00082     [[desr(32,7),desk(14),desi(47,8)],0],[[desr(1,7),desk(53),desi(48,8)],0]]),
00083     true)$
00084 
00085 okltest_des_xor_desr(f) := block(
00086   assert(f(1) =
00087     [[[desr(1,-1),deso(16,1),desr(1,1)],0],
00088      [[desr(2,-1),deso(7,1),desr(2,1)],0],
00089      [[desr(3,-1),deso(20,1),desr(3,1)],0],
00090      [[desr(4,-1),deso(21,1),desr(4,1)],0],
00091      [[desr(5,-1),deso(29,1),desr(5,1)],0],
00092      [[desr(6,-1),deso(12,1),desr(6,1)],0],
00093      [[desr(7,-1),deso(28,1),desr(7,1)],0],
00094      [[desr(8,-1),deso(17,1),desr(8,1)],0],
00095      [[desr(9,-1),deso(1,1),desr(9,1)],0],
00096      [[desr(10,-1),deso(15,1),desr(10,1)],0],
00097      [[desr(11,-1),deso(23,1),desr(11,1)],0],
00098      [[desr(12,-1),deso(26,1),desr(12,1)],0],
00099      [[desr(13,-1),deso(5,1),desr(13,1)],0],
00100      [[desr(14,-1),deso(18,1),desr(14,1)],0],
00101      [[desr(15,-1),deso(31,1),desr(15,1)],0],
00102      [[desr(16,-1),deso(10,1),desr(16,1)],0],
00103      [[desr(17,-1),deso(2,1),desr(17,1)],0],
00104      [[desr(18,-1),deso(8,1),desr(18,1)],0],
00105      [[desr(19,-1),deso(24,1),desr(19,1)],0],
00106      [[desr(20,-1),deso(14,1),desr(20,1)],0],
00107      [[desr(21,-1),deso(32,1),desr(21,1)],0],
00108      [[desr(22,-1),deso(27,1),desr(22,1)],0],
00109      [[desr(23,-1),deso(3,1),desr(23,1)],0],
00110      [[desr(24,-1),deso(9,1),desr(24,1)],0],
00111      [[desr(25,-1),deso(19,1),desr(25,1)],0],
00112      [[desr(26,-1),deso(13,1),desr(26,1)],0],
00113      [[desr(27,-1),deso(30,1),desr(27,1)],0],
00114      [[desr(28,-1),deso(6,1),desr(28,1)],0],
00115      [[desr(29,-1),deso(22,1),desr(29,1)],0],
00116      [[desr(30,-1),deso(11,1),desr(30,1)],0],
00117      [[desr(31,-1),deso(4,1),desr(31,1)],0],
00118      [[desr(32,-1),deso(25,1),desr(32,1)],0]]),
00119   assert(f(8) =
00120     [[[desr(1,6),deso(16,8),desr(1,8)],0],
00121     [[desr(2,6),deso(7,8),desr(2,8)],0],
00122     [[desr(3,6),deso(20,8),desr(3,8)],0],
00123     [[desr(4,6),deso(21,8),desr(4,8)],0],
00124     [[desr(5,6),deso(29,8),desr(5,8)],0],
00125     [[desr(6,6),deso(12,8),desr(6,8)],0],
00126     [[desr(7,6),deso(28,8),desr(7,8)],0],
00127     [[desr(8,6),deso(17,8),desr(8,8)],0],
00128     [[desr(9,6),deso(1,8),desr(9,8)],0],
00129     [[desr(10,6),deso(15,8),desr(10,8)],0],
00130     [[desr(11,6),deso(23,8),desr(11,8)],0],
00131     [[desr(12,6),deso(26,8),desr(12,8)],0],
00132     [[desr(13,6),deso(5,8),desr(13,8)],0],
00133     [[desr(14,6),deso(18,8),desr(14,8)],0],
00134     [[desr(15,6),deso(31,8),desr(15,8)],0],
00135     [[desr(16,6),deso(10,8),desr(16,8)],0],
00136     [[desr(17,6),deso(2,8),desr(17,8)],0],
00137     [[desr(18,6),deso(8,8),desr(18,8)],0],
00138     [[desr(19,6),deso(24,8),desr(19,8)],0],
00139     [[desr(20,6),deso(14,8),desr(20,8)],0],
00140     [[desr(21,6),deso(32,8),desr(21,8)],0],
00141     [[desr(22,6),deso(27,8),desr(22,8)],0],
00142     [[desr(23,6),deso(3,8),desr(23,8)],0],
00143     [[desr(24,6),deso(9,8),desr(24,8)],0],
00144     [[desr(25,6),deso(19,8),desr(25,8)],0],
00145     [[desr(26,6),deso(13,8),desr(26,8)],0],
00146     [[desr(27,6),deso(30,8),desr(27,8)],0],
00147     [[desr(28,6),deso(6,8),desr(28,8)],0],
00148     [[desr(29,6),deso(22,8),desr(29,8)],0],
00149     [[desr(30,6),deso(11,8),desr(30,8)],0],
00150     [[desr(31,6),deso(4,8),desr(31,8)],0],
00151     [[desr(32,6),deso(25,8),desr(32,8)],0]]),
00152   true)$
00153 
00154 
00155 /* *********************
00156    * S-box constraints *
00157    *********************
00158 */
00159 
00160 okltest_des_sbox_deso(f) := block(
00161   assert(f(1) =
00162     [[1,[desi(1,1),desi(2,1),desi(3,1),desi(4,1),desi(5,1),desi(6,1)],
00163         [deso(1,1),deso(2,1),deso(3,1),deso(4,1)]],
00164      [2,[desi(7,1),desi(8,1),desi(9,1),desi(10,1),desi(11,1),desi(12,1)],
00165         [deso(5,1),deso(6,1),deso(7,1),deso(8,1)]],
00166      [3,[desi(13,1),desi(14,1),desi(15,1),desi(16,1),desi(17,1),desi(18,1)],
00167         [deso(9,1),deso(10,1),deso(11,1),deso(12,1)]],
00168      [4,[desi(19,1),desi(20,1),desi(21,1),desi(22,1),desi(23,1),desi(24,1)],
00169         [deso(13,1),deso(14,1),deso(15,1),deso(16,1)]],
00170      [5,[desi(25,1),desi(26,1),desi(27,1),desi(28,1),desi(29,1),desi(30,1)],
00171         [deso(17,1),deso(18,1),deso(19,1),deso(20,1)]],
00172      [6,[desi(31,1),desi(32,1),desi(33,1),desi(34,1),desi(35,1),desi(36,1)],
00173         [deso(21,1),deso(22,1),deso(23,1),deso(24,1)]],
00174      [7,[desi(37,1),desi(38,1),desi(39,1),desi(40,1),desi(41,1),desi(42,1)],
00175         [deso(25,1),deso(26,1),deso(27,1),deso(28,1)]],
00176      [8,[desi(43,1),desi(44,1),desi(45,1),desi(46,1),desi(47,1),desi(48,1)],
00177         [deso(29,1),deso(30,1),deso(31,1),deso(32,1)]]]),
00178   assert(f(8) =
00179     [[1,[desi(1,8),desi(2,8),desi(3,8),desi(4,8),desi(5,8),desi(6,8)],
00180         [deso(1,8),deso(2,8),deso(3,8),deso(4,8)]],
00181      [2,[desi(7,8),desi(8,8),desi(9,8),desi(10,8),desi(11,8),desi(12,8)],
00182         [deso(5,8),deso(6,8),deso(7,8),deso(8,8)]],
00183      [3,[desi(13,8),desi(14,8),desi(15,8),desi(16,8),desi(17,8),desi(18,8)],
00184         [deso(9,8),deso(10,8),deso(11,8),deso(12,8)]],
00185      [4,[desi(19,8),desi(20,8),desi(21,8),desi(22,8),desi(23,8),desi(24,8)],
00186         [deso(13,8),deso(14,8),deso(15,8),deso(16,8)]],
00187      [5,[desi(25,8),desi(26,8),desi(27,8),desi(28,8),desi(29,8),desi(30,8)],
00188         [deso(17,8),deso(18,8),deso(19,8),deso(20,8)]],
00189      [6,[desi(31,8),desi(32,8),desi(33,8),desi(34,8),desi(35,8),desi(36,8)],
00190         [deso(21,8),deso(22,8),deso(23,8),deso(24,8)]],
00191      [7,[desi(37,8),desi(38,8),desi(39,8),desi(40,8),desi(41,8),desi(42,8)],
00192         [deso(25,8),deso(26,8),deso(27,8),deso(28,8)]],
00193      [8,[desi(43,8),desi(44,8),desi(45,8),desi(46,8),desi(47,8),desi(48,8)],
00194         [deso(29,8),deso(30,8),deso(31,8),deso(32,8)]]]),
00195   true)$
00196 
00197 
00198 /* ***********************
00199    * The complete system *
00200    ***********************
00201 */
00202 
00203 
00204 okltest_des_plain2pa(f) := block(
00205   assert(f(create_list(und,i,1,64)) = {}),
00206   assert(f(des_validation_plain) =
00207     {-desr(8,0),-desr(8,-1),-desr(16,0),-desr(16,-1),
00208       -desr(24,0),-desr(24,-1),-desr(32,0),desr(32,-1),
00209       -desr(7,0),-desr(7,-1),desr(15,0),-desr(15,-1),
00210       -desr(23,0),-desr(23,-1),desr(31,0),desr(31,-1),
00211       -desr(6,0),desr(6,-1),-desr(14,0),-desr(14,-1),
00212       -desr(22,0),desr(22,-1),-desr(30,0),desr(30,-1),
00213       -desr(5,0),desr(5,-1),desr(13,0),-desr(13,-1),
00214       -desr(21,0),desr(21,-1),desr(29,0),desr(29,-1),
00215       desr(4,0),-desr(4,-1),-desr(12,0),-desr(12,-1),
00216       desr(20,0),-desr(20,-1),-desr(28,0),desr(28,-1),
00217       desr(3,0),-desr(3,-1),desr(11,0),-desr(11,-1),
00218       desr(19,0),-desr(19,-1),desr(27,0),desr(27,-1),
00219       desr(2,0),desr(2,-1),-desr(10,0),-desr(10,-1),
00220       desr(18,0),desr(18,-1),-desr(26,0),desr(26,-1),
00221       desr(1,0),desr(1,-1),desr(9,0),-desr(9,-1),
00222       -desr(17,0),desr(17,-1),desr(25,0),desr(25,-1)}),
00223   true)$
00224 
00225 okltest_des_plain2fcl(f) := block(
00226   assert(f(create_list(und,i,1,64)) =
00227     [create_list(desr_var(i,r), r,-1,0, i,1,32),[]]),
00228   assert(f(des_validation_plain) =
00229     [[desr(1,-1),desr(2,-1),desr(3,-1),desr(4,-1),desr(5,-1),desr(6,-1),
00230       desr(7,-1),desr(8,-1),desr(9,-1),desr(10,-1),desr(11,-1),desr(12,-1),
00231       desr(13,-1),desr(14,-1),desr(15,-1),desr(16,-1),desr(17,-1),desr(18,-1),
00232       desr(19,-1),desr(20,-1),desr(21,-1),desr(22,-1),desr(23,-1),desr(24,-1),
00233       desr(25,-1),desr(26,-1),desr(27,-1),desr(28,-1),desr(29,-1),desr(30,-1),
00234       desr(31,-1),desr(32,-1),desr(1,0),desr(2,0),desr(3,0),desr(4,0),
00235       desr(5,0),desr(6,0),desr(7,0),desr(8,0),desr(9,0),desr(10,0),desr(11,0),
00236       desr(12,0),desr(13,0),desr(14,0),desr(15,0),desr(16,0),desr(17,0),
00237       desr(18,0),desr(19,0),desr(20,0),desr(21,0),desr(22,0),desr(23,0),
00238       desr(24,0),desr(25,0),desr(26,0),desr(27,0),desr(28,0),desr(29,0),
00239       desr(30,0),desr(31,0),desr(32,0)],
00240      [{desr(1,-1)},{desr(2,-1)},{-desr(3,-1)},{-desr(4,-1)},{desr(5,-1)},
00241       {desr(6,-1)},{-desr(7,-1)},{-desr(8,-1)},{-desr(9,-1)},{-desr(10,-1)},
00242       {-desr(11,-1)},{-desr(12,-1)},{-desr(13,-1)},{-desr(14,-1)},
00243       {-desr(15,-1)},{-desr(16,-1)},{desr(17,-1)},{desr(18,-1)},
00244       {-desr(19,-1)},{-desr(20,-1)},{desr(21,-1)},{desr(22,-1)},
00245       {-desr(23,-1)},{-desr(24,-1)},{desr(25,-1)},{desr(26,-1)},{desr(27,-1)},
00246       {desr(28,-1)},{desr(29,-1)},{desr(30,-1)},{desr(31,-1)},{desr(32,-1)},
00247       {desr(1,0)},{desr(2,0)},{desr(3,0)},{desr(4,0)},{-desr(5,0)},
00248       {-desr(6,0)},{-desr(7,0)},{-desr(8,0)},{desr(9,0)},{-desr(10,0)},
00249       {desr(11,0)},{-desr(12,0)},{desr(13,0)},{-desr(14,0)},{desr(15,0)},
00250       {-desr(16,0)},{-desr(17,0)},{desr(18,0)},{desr(19,0)},{desr(20,0)},
00251       {-desr(21,0)},{-desr(22,0)},{-desr(23,0)},{-desr(24,0)},{desr(25,0)},
00252       {-desr(26,0)},{desr(27,0)},{-desr(28,0)},{desr(29,0)},{-desr(30,0)},
00253       {desr(31,0)},{-desr(32,0)}]]),
00254   true)$
00255 
00256 okltest_des_cipher2pa(f) := block(
00257   assert(f(create_list(und,i,1,64)) = {}),
00258   assert(f(des_validation_cipher) =
00259      {desr(8,15),desr(8,16),-desr(16,15),-desr(16,16),
00260       desr(24,15),-desr(24,16),-desr(32,15),desr(32,16),
00261       -desr(7,15),desr(7,16),-desr(15,15),desr(15,16),
00262       -desr(23,15),desr(23,16),desr(31,15),desr(31,16),
00263       -desr(6,15),desr(6,16),-desr(14,15),-desr(14,16),
00264       -desr(22,15),desr(22,16),-desr(30,15),-desr(30,16),
00265       -desr(5,15),-desr(5,16),desr(13,15),-desr(13,16),
00266       -desr(21,15),desr(21,16),-desr(29,15),desr(29,16),
00267       -desr(4,15),desr(4,16),desr(12,15),-desr(12,16),
00268       desr(20,15),-desr(20,16),desr(28,15),-desr(28,16),
00269       -desr(3,15),desr(3,16),-desr(11,15),desr(11,16),
00270       desr(19,15),desr(19,16),desr(27,15),-desr(27,16),
00271       desr(2,15),desr(2,16),-desr(10,15),desr(10,16),
00272       -desr(18,15),-desr(18,16),desr(26,15),desr(26,16),
00273       -desr(1,15),-desr(1,16),-desr(9,15),desr(9,16),
00274       desr(17,15),desr(17,16),-desr(25,15),desr(25,16)}),
00275   true)$
00276 
00277 okltest_des_cipher2fcl(f) := block(
00278   assert(f(create_list(und,i,1,64)) =
00279     [create_list(desr_var(i,r), r,[16,15], i,1,32),[]]),
00280   assert(f(des_validation_cipher) =
00281     [[desr(1,16),desr(2,16),desr(3,16),desr(4,16),desr(5,16),desr(6,16),
00282       desr(7,16),desr(8,16),desr(9,16),desr(10,16),desr(11,16),
00283       desr(12,16),desr(13,16),desr(14,16),desr(15,16),desr(16,16),
00284       desr(17,16),desr(18,16),desr(19,16),desr(20,16),desr(21,16),
00285       desr(22,16),desr(23,16),desr(24,16),desr(25,16),desr(26,16),
00286       desr(27,16),desr(28,16),desr(29,16),desr(30,16),desr(31,16),
00287       desr(32,16),desr(1,15),desr(2,15),desr(3,15),desr(4,15),desr(5,15),
00288       desr(6,15),desr(7,15),desr(8,15),desr(9,15),desr(10,15),desr(11,15),
00289       desr(12,15),desr(13,15),desr(14,15),desr(15,15),desr(16,15),
00290       desr(17,15),desr(18,15),desr(19,15),desr(20,15),desr(21,15),
00291       desr(22,15),desr(23,15),desr(24,15),desr(25,15),desr(26,15),
00292       desr(27,15),desr(28,15),desr(29,15),desr(30,15),desr(31,15),
00293       desr(32,15)],
00294      [{-desr(1,16)},{desr(2,16)},{desr(3,16)},{desr(4,16)},{-desr(5,16)},
00295       {desr(6,16)},{desr(7,16)},{desr(8,16)},{desr(9,16)},{desr(10,16)},
00296       {desr(11,16)},{-desr(12,16)},{-desr(13,16)},{-desr(14,16)},
00297       {desr(15,16)},{-desr(16,16)},{desr(17,16)},{-desr(18,16)},{desr(19,16)},
00298       {-desr(20,16)},{desr(21,16)},{desr(22,16)},{desr(23,16)},{-desr(24,16)},
00299       {desr(25,16)},{desr(26,16)},{-desr(27,16)},{-desr(28,16)},{desr(29,16)},
00300       {-desr(30,16)},{desr(31,16)},{desr(32,16)},{-desr(1,15)},{desr(2,15)},
00301       {-desr(3,15)},{-desr(4,15)},{-desr(5,15)},{-desr(6,15)},{-desr(7,15)},
00302       {desr(8,15)},{-desr(9,15)},{-desr(10,15)},{-desr(11,15)},{desr(12,15)},
00303       {desr(13,15)},{-desr(14,15)},{-desr(15,15)},{-desr(16,15)},
00304       {desr(17,15)},{-desr(18,15)},{desr(19,15)},{desr(20,15)},{-desr(21,15)},
00305       {-desr(22,15)},{-desr(23,15)},{desr(24,15)},{-desr(25,15)},
00306       {desr(26,15)},{desr(27,15)},{desr(28,15)},{-desr(29,15)},{-desr(30,15)},
00307       {desr(31,15)},{-desr(32,15)}]]),
00308   true)$
00309 
00310 okltest_des_key2pa(f) := block(
00311   assert(f(create_list(und,i,1,64)) = {}),
00312   assert(f(des_validation_key) =
00313     {-desk(1),-desk(2),-desk(3),-desk(4),-desk(5),-desk(6),
00314      -desk(7),desk(8),-desk(9),-desk(10),desk(11),-desk(12),
00315      -desk(13),-desk(14),desk(15),desk(16),-desk(17),
00316      desk(18),-desk(19),-desk(20),-desk(21),desk(22),
00317      -desk(23),desk(24),-desk(25),desk(26),desk(27),
00318      -desk(28),-desk(29),desk(30),desk(31),desk(32),desk(33),
00319      -desk(34),-desk(35),-desk(36),desk(37),-desk(38),
00320      -desk(39),desk(40),desk(41),-desk(42),desk(43),
00321      -desk(44),desk(45),-desk(46),desk(47),desk(48),desk(49),
00322      desk(50),-desk(51),-desk(52),desk(53),desk(54),
00323      -desk(55),desk(56),desk(57),desk(58),desk(59),-desk(60),
00324      desk(61),desk(62),desk(63),desk(64)}),
00325   true)$
00326 
00327 okltest_des_key2fcl(f) := block(
00328   assert(f(create_list(und,i,1,64)) = [create_list(desk_var(i), i,1,64),[]]),
00329   assert(f(des_validation_key) =
00330     [[desk(1),desk(2),desk(3),desk(4),desk(5),desk(6),desk(7),desk(8),
00331       desk(9),desk(10),desk(11),desk(12),desk(13),desk(14),desk(15),
00332       desk(16),desk(17),desk(18),desk(19),desk(20),desk(21),desk(22),
00333       desk(23),desk(24),desk(25),desk(26),desk(27),desk(28),desk(29),
00334       desk(30),desk(31),desk(32),desk(33),desk(34),desk(35),desk(36),
00335       desk(37),desk(38),desk(39),desk(40),desk(41),desk(42),desk(43),
00336       desk(44),desk(45),desk(46),desk(47),desk(48),desk(49),desk(50),
00337       desk(51),desk(52),desk(53),desk(54),desk(55),desk(56),desk(57),
00338       desk(58),desk(59),desk(60),desk(61),desk(62),desk(63),desk(64)],
00339      [{-desk(1)},{-desk(2)},{-desk(3)},{-desk(4)},{-desk(5)},{-desk(6)},
00340       {-desk(7)},{desk(8)},{-desk(9)},{-desk(10)},{desk(11)},{-desk(12)},
00341       {-desk(13)},{-desk(14)},{desk(15)},{desk(16)},{-desk(17)},
00342       {desk(18)},{-desk(19)},{-desk(20)},{-desk(21)},{desk(22)},
00343       {-desk(23)},{desk(24)},{-desk(25)},{desk(26)},{desk(27)},
00344       {-desk(28)},{-desk(29)},{desk(30)},{desk(31)},{desk(32)},{desk(33)},
00345       {-desk(34)},{-desk(35)},{-desk(36)},{desk(37)},{-desk(38)},
00346       {-desk(39)},{desk(40)},{desk(41)},{-desk(42)},{desk(43)},
00347       {-desk(44)},{desk(45)},{-desk(46)},{desk(47)},{desk(48)},{desk(49)},
00348       {desk(50)},{-desk(51)},{-desk(52)},{desk(53)},{desk(54)},
00349       {-desk(55)},{desk(56)},{desk(57)},{desk(58)},{desk(59)},{-desk(60)},
00350       {desk(61)},{desk(62)},{desk(63)},{desk(64)}]]),
00351   true)$
00352