1open HolKernel Parse boolLib bossLib pairTools word8Theory; 2 3infix THEN 4 5val _ = new_theory "sbox"; 6 7 8(*--------------------------------------------------------------------------- 9 Sbox and its inverse. 10 11 val Sbox : word8 list = 12 [0wx63, 0wx7c, 0wx77, 0wx7b, 0wxf2, 0wx6b, 0wx6f, 0wxc5, 13 0wx30, 0wx01, 0wx67, 0wx2b, 0wxfe, 0wxd7, 0wxab, 0wx76, 14 0wxca, 0wx82, 0wxc9, 0wx7d, 0wxfa, 0wx59, 0wx47, 0wxf0, 15 0wxad, 0wxd4, 0wxa2, 0wxaf, 0wx9c, 0wxa4, 0wx72, 0wxc0, 16 0wxb7, 0wxfd, 0wx93, 0wx26, 0wx36, 0wx3f, 0wxf7, 0wxcc, 17 0wx34, 0wxa5, 0wxe5, 0wxf1, 0wx71, 0wxd8, 0wx31, 0wx15, 18 0wx04, 0wxc7, 0wx23, 0wxc3, 0wx18, 0wx96, 0wx05, 0wx9a, 19 0wx07, 0wx12, 0wx80, 0wxe2, 0wxeb, 0wx27, 0wxb2, 0wx75, 20 0wx09, 0wx83, 0wx2c, 0wx1a, 0wx1b, 0wx6e, 0wx5a, 0wxa0, 21 0wx52, 0wx3b, 0wxd6, 0wxb3, 0wx29, 0wxe3, 0wx2f, 0wx84, 22 0wx53, 0wxd1, 0wx00, 0wxed, 0wx20, 0wxfc, 0wxb1, 0wx5b, 23 0wx6a, 0wxcb, 0wxbe, 0wx39, 0wx4a, 0wx4c, 0wx58, 0wxcf, 24 0wxd0, 0wxef, 0wxaa, 0wxfb, 0wx43, 0wx4d, 0wx33, 0wx85, 25 0wx45, 0wxf9, 0wx02, 0wx7f, 0wx50, 0wx3c, 0wx9f, 0wxa8, 26 0wx51, 0wxa3, 0wx40, 0wx8f, 0wx92, 0wx9d, 0wx38, 0wxf5, 27 0wxbc, 0wxb6, 0wxda, 0wx21, 0wx10, 0wxff, 0wxf3, 0wxd2, 28 0wxcd, 0wx0c, 0wx13, 0wxec, 0wx5f, 0wx97, 0wx44, 0wx17, 29 0wxc4, 0wxa7, 0wx7e, 0wx3d, 0wx64, 0wx5d, 0wx19, 0wx73, 30 0wx60, 0wx81, 0wx4f, 0wxdc, 0wx22, 0wx2a, 0wx90, 0wx88, 31 0wx46, 0wxee, 0wxb8, 0wx14, 0wxde, 0wx5e, 0wx0b, 0wxdb, 32 0wxe0, 0wx32, 0wx3a, 0wx0a, 0wx49, 0wx06, 0wx24, 0wx5c, 33 0wxc2, 0wxd3, 0wxac, 0wx62, 0wx91, 0wx95, 0wxe4, 0wx79, 34 0wxe7, 0wxc8, 0wx37, 0wx6d, 0wx8d, 0wxd5, 0wx4e, 0wxa9, 35 0wx6c, 0wx56, 0wxf4, 0wxea, 0wx65, 0wx7a, 0wxae, 0wx08, 36 0wxba, 0wx78, 0wx25, 0wx2e, 0wx1c, 0wxa6, 0wxb4, 0wxc6, 37 0wxe8, 0wxdd, 0wx74, 0wx1f, 0wx4b, 0wxbd, 0wx8b, 0wx8a, 38 0wx70, 0wx3e, 0wxb5, 0wx66, 0wx48, 0wx03, 0wxf6, 0wx0e, 39 0wx61, 0wx35, 0wx57, 0wxb9, 0wx86, 0wxc1, 0wx1d, 0wx9e, 40 0wxe1, 0wxf8, 0wx98, 0wx11, 0wx69, 0wxd9, 0wx83, 0wx94, 41 0wx9b, 0wx1e, 0wx87, 0wxe9, 0wxce, 0wx55, 0wx28, 0wxdf, 42 0wx8c, 0wxa1, 0wx89, 0wx0d, 0wxbf, 0wxe6, 0wx42, 0wx68, 43 0wx41, 0wx99, 0wx2d, 0wx0f, 0wxb0, 0wx54, 0wxbb, 0wx16] 44 45 val InvSbox : word8 list = 46 [0wx52, 0wx09, 0wx6a, 0wxd5, 0wx30, 0wx36, 0wxa5, 47 0wx38, 0wxbf, 0wx40, 0wxa3, 0wx9e, 0wx81, 0wxf3, 0wxd7, 0wxfb, 48 0wx7c, 0wxe3, 0wx39, 0wx82, 0wx9b, 0wx2f, 0wxff, 49 0wx87, 0wx34, 0wx8e, 0wx43, 0wx44, 0wxc4, 0wxde, 0wxe9, 0wxcb, 50 0wx54, 0wx7b, 0wx94, 0wx32, 0wxa6, 0wxc2, 0wx23, 51 0wx3d, 0wxee, 0wx4c, 0wx95, 0wx0b, 0wx42, 0wxfa, 0wxc3, 0wx4e, 52 0wx08, 0wx2e, 0wxa1, 0wx66, 0wx28, 0wxd9, 0wx24, 53 0wxb2, 0wx76, 0wx5b, 0wxa2, 0wx49, 0wx6d, 0wx8b, 0wxd1, 0wx25, 54 0wx72, 0wxf8, 0wxf6, 0wx64, 0wx86, 0wx68, 0wx98, 55 0wx16, 0wxd4, 0wxa4, 0wx5c, 0wxcc, 0wx5d, 0wx65, 0wxb6, 0wx92, 56 0wx6c, 0wx70, 0wx48, 0wx50, 0wxfd, 0wxed, 0wxb9, 57 0wxda, 0wx5e, 0wx15, 0wx46, 0wx57, 0wxa7, 0wx8d, 0wx9d, 0wx84, 58 0wx90, 0wxd8, 0wxab, 0wx00, 0wx8c, 0wxbc, 0wxd3, 59 0wx0a, 0wxf7, 0wxe4, 0wx58, 0wx05, 0wxb8, 0wxb3, 0wx45, 0wx06, 60 0wxd0, 0wx2c, 0wx1e, 0wx8f, 0wxca, 0wx3f, 0wx0f, 61 0wx02, 0wxc1, 0wxaf, 0wxbd, 0wx03, 0wx01, 0wx13, 0wx8a, 0wx6b, 62 0wx3a, 0wx91, 0wx11, 0wx41, 0wx4f, 0wx67, 0wxdc, 63 0wxea, 0wx97, 0wxf2, 0wxcf, 0wxce, 0wxf0, 0wxb4, 0wxe6, 0wx73, 64 0wx96, 0wxac, 0wx74, 0wx22, 0wxe7, 0wxad, 0wx35, 65 0wx85, 0wxe2, 0wxf9, 0wx37, 0wxe8, 0wx1c, 0wx75, 0wxdf, 0wx6e, 66 0wx47, 0wxf1, 0wx1a, 0wx71, 0wx1d, 0wx29, 0wxc5, 67 0wx89, 0wx6f, 0wxb7, 0wx62, 0wx0e, 0wxaa, 0wx18, 0wxbe, 0wx1b, 68 0wxfc, 0wx56, 0wx3e, 0wx4b, 0wxc6, 0wxd2, 0wx79, 69 0wx20, 0wx9a, 0wxdb, 0wxc0, 0wxfe, 0wx78, 0wxcd, 0wx5a, 0wxf4, 70 0wx1f, 0wxdd, 0wxa8, 0wx33, 0wx88, 0wx07, 0wxc7, 71 0wx31, 0wxb1, 0wx12, 0wx10, 0wx59, 0wx27, 0wx80, 0wxec, 0wx5f, 72 0wx60, 0wx51, 0wx7f, 0wxa9, 0wx19, 0wxb5, 0wx4a, 73 0wx0d, 0wx2d, 0wxe5, 0wx7a, 0wx9f, 0wx93, 0wxc9, 0wx9c, 0wxef, 74 0wxa0, 0wxe0, 0wx3b, 0wx4d, 0wxae, 0wx2a, 0wxf5, 75 0wxb0, 0wxc8, 0wxeb, 0wxbb, 0wx3c, 0wx83, 0wx53, 0wx99, 0wx61, 76 0wx17, 0wx2b, 0wx04, 0wx7e, 0wxba, 0wx77, 0wxd6, 77 0wx26, 0wxe1, 0wx69, 0wx14, 0wx63, 0wx55, 0wx21, 0wx0c, 0wx7d]; 78 79 ---------------------------------------------------------------------------*) 80 81 82 83(*--------------------------------------------------------------------------- 84 Support for constructing HOL Sboxen from ML. 85 A byte is represented as bool^8 in HOL. 86 ---------------------------------------------------------------------------*) 87(* 88load "Word8"; 89datatype bit = T | F; 90 91fun int_of T = 1 | int_of F = 0 92fun bit_of 1 = T | bit_of 0 = F 93 94fun char_to_int #"1" = 1 | char_to_int #"0" = 0; 95val char_to_bit = bit_of o char_to_int; 96fun to_8tuple [a,b,c,d,e,f,g,h] = (a,b,c,d,e,f,g,h); 97 98local fun pad 0 = "" 99 | pad 1 = "0" 100 | pad 2 = "00" 101 | pad 3 = "000" 102 | pad 4 = "0000" 103 | pad 5 = "00000" 104 | pad 6 = "000000" 105 | pad 7 = "0000000" 106in 107fun padword s = pad (8 - String.size s)^s 108end 109 110val word8_to_8tuple = 111 to_8tuple 112 o map char_to_bit 113 o String.explode 114 o padword 115 o Word8.fmt stringCvt.BIN; 116 117val int_to_8tuple = word8_to_8tuple o Word8.fromInt; 118 119fun upto b t acc = if b>t then rev acc else upto (b+1) t (b::acc); 120val ilist = upto 0 255 []; 121val wlist = map Word8.fromInt ilist; 122val blist = map word8_to_8tuple wlist; 123*) 124 125(*--------------------------------------------------------------------------- 126 This is just a one dimensional array indexed by words up to 256. 127 ---------------------------------------------------------------------------*) 128 129val Sbox_def = 130 Count.apply Define 131 `(Sbox (F,F,F,F,F,F,F,F) = (F,T,T,F,F,F,T,T)) /\ 132 (Sbox (F,F,F,F,F,F,F,T) = (F,T,T,T,T,T,F,F)) /\ 133 (Sbox (F,F,F,F,F,F,T,F) = (F,T,T,T,F,T,T,T)) /\ 134 (Sbox (F,F,F,F,F,F,T,T) = (F,T,T,T,T,F,T,T)) /\ 135 (Sbox (F,F,F,F,F,T,F,F) = (T,T,T,T,F,F,T,F)) /\ 136 (Sbox (F,F,F,F,F,T,F,T) = (F,T,T,F,T,F,T,T)) /\ 137 (Sbox (F,F,F,F,F,T,T,F) = (F,T,T,F,T,T,T,T)) /\ 138 (Sbox (F,F,F,F,F,T,T,T) = (T,T,F,F,F,T,F,T)) /\ 139 (Sbox (F,F,F,F,T,F,F,F) = (F,F,T,T,F,F,F,F)) /\ 140 (Sbox (F,F,F,F,T,F,F,T) = (F,F,F,F,F,F,F,T)) /\ 141 (Sbox (F,F,F,F,T,F,T,F) = (F,T,T,F,F,T,T,T)) /\ 142 (Sbox (F,F,F,F,T,F,T,T) = (F,F,T,F,T,F,T,T)) /\ 143 (Sbox (F,F,F,F,T,T,F,F) = (T,T,T,T,T,T,T,F)) /\ 144 (Sbox (F,F,F,F,T,T,F,T) = (T,T,F,T,F,T,T,T)) /\ 145 (Sbox (F,F,F,F,T,T,T,F) = (T,F,T,F,T,F,T,T)) /\ 146 (Sbox (F,F,F,F,T,T,T,T) = (F,T,T,T,F,T,T,F)) /\ 147 (Sbox (F,F,F,T,F,F,F,F) = (T,T,F,F,T,F,T,F)) /\ 148 (Sbox (F,F,F,T,F,F,F,T) = (T,F,F,F,F,F,T,F)) /\ 149 (Sbox (F,F,F,T,F,F,T,F) = (T,T,F,F,T,F,F,T)) /\ 150 (Sbox (F,F,F,T,F,F,T,T) = (F,T,T,T,T,T,F,T)) /\ 151 (Sbox (F,F,F,T,F,T,F,F) = (T,T,T,T,T,F,T,F)) /\ 152 (Sbox (F,F,F,T,F,T,F,T) = (F,T,F,T,T,F,F,T)) /\ 153 (Sbox (F,F,F,T,F,T,T,F) = (F,T,F,F,F,T,T,T)) /\ 154 (Sbox (F,F,F,T,F,T,T,T) = (T,T,T,T,F,F,F,F)) /\ 155 (Sbox (F,F,F,T,T,F,F,F) = (T,F,T,F,T,T,F,T)) /\ 156 (Sbox (F,F,F,T,T,F,F,T) = (T,T,F,T,F,T,F,F)) /\ 157 (Sbox (F,F,F,T,T,F,T,F) = (T,F,T,F,F,F,T,F)) /\ 158 (Sbox (F,F,F,T,T,F,T,T) = (T,F,T,F,T,T,T,T)) /\ 159 (Sbox (F,F,F,T,T,T,F,F) = (T,F,F,T,T,T,F,F)) /\ 160 (Sbox (F,F,F,T,T,T,F,T) = (T,F,T,F,F,T,F,F)) /\ 161 (Sbox (F,F,F,T,T,T,T,F) = (F,T,T,T,F,F,T,F)) /\ 162 (Sbox (F,F,F,T,T,T,T,T) = (T,T,F,F,F,F,F,F)) /\ 163 (Sbox (F,F,T,F,F,F,F,F) = (T,F,T,T,F,T,T,T)) /\ 164 (Sbox (F,F,T,F,F,F,F,T) = (T,T,T,T,T,T,F,T)) /\ 165 (Sbox (F,F,T,F,F,F,T,F) = (T,F,F,T,F,F,T,T)) /\ 166 (Sbox (F,F,T,F,F,F,T,T) = (F,F,T,F,F,T,T,F)) /\ 167 (Sbox (F,F,T,F,F,T,F,F) = (F,F,T,T,F,T,T,F)) /\ 168 (Sbox (F,F,T,F,F,T,F,T) = (F,F,T,T,T,T,T,T)) /\ 169 (Sbox (F,F,T,F,F,T,T,F) = (T,T,T,T,F,T,T,T)) /\ 170 (Sbox (F,F,T,F,F,T,T,T) = (T,T,F,F,T,T,F,F)) /\ 171 (Sbox (F,F,T,F,T,F,F,F) = (F,F,T,T,F,T,F,F)) /\ 172 (Sbox (F,F,T,F,T,F,F,T) = (T,F,T,F,F,T,F,T)) /\ 173 (Sbox (F,F,T,F,T,F,T,F) = (T,T,T,F,F,T,F,T)) /\ 174 (Sbox (F,F,T,F,T,F,T,T) = (T,T,T,T,F,F,F,T)) /\ 175 (Sbox (F,F,T,F,T,T,F,F) = (F,T,T,T,F,F,F,T)) /\ 176 (Sbox (F,F,T,F,T,T,F,T) = (T,T,F,T,T,F,F,F)) /\ 177 (Sbox (F,F,T,F,T,T,T,F) = (F,F,T,T,F,F,F,T)) /\ 178 (Sbox (F,F,T,F,T,T,T,T) = (F,F,F,T,F,T,F,T)) /\ 179 (Sbox (F,F,T,T,F,F,F,F) = (F,F,F,F,F,T,F,F)) /\ 180 (Sbox (F,F,T,T,F,F,F,T) = (T,T,F,F,F,T,T,T)) /\ 181 (Sbox (F,F,T,T,F,F,T,F) = (F,F,T,F,F,F,T,T)) /\ 182 (Sbox (F,F,T,T,F,F,T,T) = (T,T,F,F,F,F,T,T)) /\ 183 (Sbox (F,F,T,T,F,T,F,F) = (F,F,F,T,T,F,F,F)) /\ 184 (Sbox (F,F,T,T,F,T,F,T) = (T,F,F,T,F,T,T,F)) /\ 185 (Sbox (F,F,T,T,F,T,T,F) = (F,F,F,F,F,T,F,T)) /\ 186 (Sbox (F,F,T,T,F,T,T,T) = (T,F,F,T,T,F,T,F)) /\ 187 (Sbox (F,F,T,T,T,F,F,F) = (F,F,F,F,F,T,T,T)) /\ 188 (Sbox (F,F,T,T,T,F,F,T) = (F,F,F,T,F,F,T,F)) /\ 189 (Sbox (F,F,T,T,T,F,T,F) = (T,F,F,F,F,F,F,F)) /\ 190 (Sbox (F,F,T,T,T,F,T,T) = (T,T,T,F,F,F,T,F)) /\ 191 (Sbox (F,F,T,T,T,T,F,F) = (T,T,T,F,T,F,T,T)) /\ 192 (Sbox (F,F,T,T,T,T,F,T) = (F,F,T,F,F,T,T,T)) /\ 193 (Sbox (F,F,T,T,T,T,T,F) = (T,F,T,T,F,F,T,F)) /\ 194 (Sbox (F,F,T,T,T,T,T,T) = (F,T,T,T,F,T,F,T)) /\ 195 (Sbox (F,T,F,F,F,F,F,F) = (F,F,F,F,T,F,F,T)) /\ 196 (Sbox (F,T,F,F,F,F,F,T) = (T,F,F,F,F,F,T,T)) /\ 197 (Sbox (F,T,F,F,F,F,T,F) = (F,F,T,F,T,T,F,F)) /\ 198 (Sbox (F,T,F,F,F,F,T,T) = (F,F,F,T,T,F,T,F)) /\ 199 (Sbox (F,T,F,F,F,T,F,F) = (F,F,F,T,T,F,T,T)) /\ 200 (Sbox (F,T,F,F,F,T,F,T) = (F,T,T,F,T,T,T,F)) /\ 201 (Sbox (F,T,F,F,F,T,T,F) = (F,T,F,T,T,F,T,F)) /\ 202 (Sbox (F,T,F,F,F,T,T,T) = (T,F,T,F,F,F,F,F)) /\ 203 (Sbox (F,T,F,F,T,F,F,F) = (F,T,F,T,F,F,T,F)) /\ 204 (Sbox (F,T,F,F,T,F,F,T) = (F,F,T,T,T,F,T,T)) /\ 205 (Sbox (F,T,F,F,T,F,T,F) = (T,T,F,T,F,T,T,F)) /\ 206 (Sbox (F,T,F,F,T,F,T,T) = (T,F,T,T,F,F,T,T)) /\ 207 (Sbox (F,T,F,F,T,T,F,F) = (F,F,T,F,T,F,F,T)) /\ 208 (Sbox (F,T,F,F,T,T,F,T) = (T,T,T,F,F,F,T,T)) /\ 209 (Sbox (F,T,F,F,T,T,T,F) = (F,F,T,F,T,T,T,T)) /\ 210 (Sbox (F,T,F,F,T,T,T,T) = (T,F,F,F,F,T,F,F)) /\ 211 (Sbox (F,T,F,T,F,F,F,F) = (F,T,F,T,F,F,T,T)) /\ 212 (Sbox (F,T,F,T,F,F,F,T) = (T,T,F,T,F,F,F,T)) /\ 213 (Sbox (F,T,F,T,F,F,T,F) = (F,F,F,F,F,F,F,F)) /\ 214 (Sbox (F,T,F,T,F,F,T,T) = (T,T,T,F,T,T,F,T)) /\ 215 (Sbox (F,T,F,T,F,T,F,F) = (F,F,T,F,F,F,F,F)) /\ 216 (Sbox (F,T,F,T,F,T,F,T) = (T,T,T,T,T,T,F,F)) /\ 217 (Sbox (F,T,F,T,F,T,T,F) = (T,F,T,T,F,F,F,T)) /\ 218 (Sbox (F,T,F,T,F,T,T,T) = (F,T,F,T,T,F,T,T)) /\ 219 (Sbox (F,T,F,T,T,F,F,F) = (F,T,T,F,T,F,T,F)) /\ 220 (Sbox (F,T,F,T,T,F,F,T) = (T,T,F,F,T,F,T,T)) /\ 221 (Sbox (F,T,F,T,T,F,T,F) = (T,F,T,T,T,T,T,F)) /\ 222 (Sbox (F,T,F,T,T,F,T,T) = (F,F,T,T,T,F,F,T)) /\ 223 (Sbox (F,T,F,T,T,T,F,F) = (F,T,F,F,T,F,T,F)) /\ 224 (Sbox (F,T,F,T,T,T,F,T) = (F,T,F,F,T,T,F,F)) /\ 225 (Sbox (F,T,F,T,T,T,T,F) = (F,T,F,T,T,F,F,F)) /\ 226 (Sbox (F,T,F,T,T,T,T,T) = (T,T,F,F,T,T,T,T)) /\ 227 (Sbox (F,T,T,F,F,F,F,F) = (T,T,F,T,F,F,F,F)) /\ 228 (Sbox (F,T,T,F,F,F,F,T) = (T,T,T,F,T,T,T,T)) /\ 229 (Sbox (F,T,T,F,F,F,T,F) = (T,F,T,F,T,F,T,F)) /\ 230 (Sbox (F,T,T,F,F,F,T,T) = (T,T,T,T,T,F,T,T)) /\ 231 (Sbox (F,T,T,F,F,T,F,F) = (F,T,F,F,F,F,T,T)) /\ 232 (Sbox (F,T,T,F,F,T,F,T) = (F,T,F,F,T,T,F,T)) /\ 233 (Sbox (F,T,T,F,F,T,T,F) = (F,F,T,T,F,F,T,T)) /\ 234 (Sbox (F,T,T,F,F,T,T,T) = (T,F,F,F,F,T,F,T)) /\ 235 (Sbox (F,T,T,F,T,F,F,F) = (F,T,F,F,F,T,F,T)) /\ 236 (Sbox (F,T,T,F,T,F,F,T) = (T,T,T,T,T,F,F,T)) /\ 237 (Sbox (F,T,T,F,T,F,T,F) = (F,F,F,F,F,F,T,F)) /\ 238 (Sbox (F,T,T,F,T,F,T,T) = (F,T,T,T,T,T,T,T)) /\ 239 (Sbox (F,T,T,F,T,T,F,F) = (F,T,F,T,F,F,F,F)) /\ 240 (Sbox (F,T,T,F,T,T,F,T) = (F,F,T,T,T,T,F,F)) /\ 241 (Sbox (F,T,T,F,T,T,T,F) = (T,F,F,T,T,T,T,T)) /\ 242 (Sbox (F,T,T,F,T,T,T,T) = (T,F,T,F,T,F,F,F)) /\ 243 (Sbox (F,T,T,T,F,F,F,F) = (F,T,F,T,F,F,F,T)) /\ 244 (Sbox (F,T,T,T,F,F,F,T) = (T,F,T,F,F,F,T,T)) /\ 245 (Sbox (F,T,T,T,F,F,T,F) = (F,T,F,F,F,F,F,F)) /\ 246 (Sbox (F,T,T,T,F,F,T,T) = (T,F,F,F,T,T,T,T)) /\ 247 (Sbox (F,T,T,T,F,T,F,F) = (T,F,F,T,F,F,T,F)) /\ 248 (Sbox (F,T,T,T,F,T,F,T) = (T,F,F,T,T,T,F,T)) /\ 249 (Sbox (F,T,T,T,F,T,T,F) = (F,F,T,T,T,F,F,F)) /\ 250 (Sbox (F,T,T,T,F,T,T,T) = (T,T,T,T,F,T,F,T)) /\ 251 (Sbox (F,T,T,T,T,F,F,F) = (T,F,T,T,T,T,F,F)) /\ 252 (Sbox (F,T,T,T,T,F,F,T) = (T,F,T,T,F,T,T,F)) /\ 253 (Sbox (F,T,T,T,T,F,T,F) = (T,T,F,T,T,F,T,F)) /\ 254 (Sbox (F,T,T,T,T,F,T,T) = (F,F,T,F,F,F,F,T)) /\ 255 (Sbox (F,T,T,T,T,T,F,F) = (F,F,F,T,F,F,F,F)) /\ 256 (Sbox (F,T,T,T,T,T,F,T) = (T,T,T,T,T,T,T,T)) /\ 257 (Sbox (F,T,T,T,T,T,T,F) = (T,T,T,T,F,F,T,T)) /\ 258 (Sbox (F,T,T,T,T,T,T,T) = (T,T,F,T,F,F,T,F)) /\ 259 (Sbox (T,F,F,F,F,F,F,F) = (T,T,F,F,T,T,F,T)) /\ 260 (Sbox (T,F,F,F,F,F,F,T) = (F,F,F,F,T,T,F,F)) /\ 261 (Sbox (T,F,F,F,F,F,T,F) = (F,F,F,T,F,F,T,T)) /\ 262 (Sbox (T,F,F,F,F,F,T,T) = (T,T,T,F,T,T,F,F)) /\ 263 (Sbox (T,F,F,F,F,T,F,F) = (F,T,F,T,T,T,T,T)) /\ 264 (Sbox (T,F,F,F,F,T,F,T) = (T,F,F,T,F,T,T,T)) /\ 265 (Sbox (T,F,F,F,F,T,T,F) = (F,T,F,F,F,T,F,F)) /\ 266 (Sbox (T,F,F,F,F,T,T,T) = (F,F,F,T,F,T,T,T)) /\ 267 (Sbox (T,F,F,F,T,F,F,F) = (T,T,F,F,F,T,F,F)) /\ 268 (Sbox (T,F,F,F,T,F,F,T) = (T,F,T,F,F,T,T,T)) /\ 269 (Sbox (T,F,F,F,T,F,T,F) = (F,T,T,T,T,T,T,F)) /\ 270 (Sbox (T,F,F,F,T,F,T,T) = (F,F,T,T,T,T,F,T)) /\ 271 (Sbox (T,F,F,F,T,T,F,F) = (F,T,T,F,F,T,F,F)) /\ 272 (Sbox (T,F,F,F,T,T,F,T) = (F,T,F,T,T,T,F,T)) /\ 273 (Sbox (T,F,F,F,T,T,T,F) = (F,F,F,T,T,F,F,T)) /\ 274 (Sbox (T,F,F,F,T,T,T,T) = (F,T,T,T,F,F,T,T)) /\ 275 (Sbox (T,F,F,T,F,F,F,F) = (F,T,T,F,F,F,F,F)) /\ 276 (Sbox (T,F,F,T,F,F,F,T) = (T,F,F,F,F,F,F,T)) /\ 277 (Sbox (T,F,F,T,F,F,T,F) = (F,T,F,F,T,T,T,T)) /\ 278 (Sbox (T,F,F,T,F,F,T,T) = (T,T,F,T,T,T,F,F)) /\ 279 (Sbox (T,F,F,T,F,T,F,F) = (F,F,T,F,F,F,T,F)) /\ 280 (Sbox (T,F,F,T,F,T,F,T) = (F,F,T,F,T,F,T,F)) /\ 281 (Sbox (T,F,F,T,F,T,T,F) = (T,F,F,T,F,F,F,F)) /\ 282 (Sbox (T,F,F,T,F,T,T,T) = (T,F,F,F,T,F,F,F)) /\ 283 (Sbox (T,F,F,T,T,F,F,F) = (F,T,F,F,F,T,T,F)) /\ 284 (Sbox (T,F,F,T,T,F,F,T) = (T,T,T,F,T,T,T,F)) /\ 285 (Sbox (T,F,F,T,T,F,T,F) = (T,F,T,T,T,F,F,F)) /\ 286 (Sbox (T,F,F,T,T,F,T,T) = (F,F,F,T,F,T,F,F)) /\ 287 (Sbox (T,F,F,T,T,T,F,F) = (T,T,F,T,T,T,T,F)) /\ 288 (Sbox (T,F,F,T,T,T,F,T) = (F,T,F,T,T,T,T,F)) /\ 289 (Sbox (T,F,F,T,T,T,T,F) = (F,F,F,F,T,F,T,T)) /\ 290 (Sbox (T,F,F,T,T,T,T,T) = (T,T,F,T,T,F,T,T)) /\ 291 (Sbox (T,F,T,F,F,F,F,F) = (T,T,T,F,F,F,F,F)) /\ 292 (Sbox (T,F,T,F,F,F,F,T) = (F,F,T,T,F,F,T,F)) /\ 293 (Sbox (T,F,T,F,F,F,T,F) = (F,F,T,T,T,F,T,F)) /\ 294 (Sbox (T,F,T,F,F,F,T,T) = (F,F,F,F,T,F,T,F)) /\ 295 (Sbox (T,F,T,F,F,T,F,F) = (F,T,F,F,T,F,F,T)) /\ 296 (Sbox (T,F,T,F,F,T,F,T) = (F,F,F,F,F,T,T,F)) /\ 297 (Sbox (T,F,T,F,F,T,T,F) = (F,F,T,F,F,T,F,F)) /\ 298 (Sbox (T,F,T,F,F,T,T,T) = (F,T,F,T,T,T,F,F)) /\ 299 (Sbox (T,F,T,F,T,F,F,F) = (T,T,F,F,F,F,T,F)) /\ 300 (Sbox (T,F,T,F,T,F,F,T) = (T,T,F,T,F,F,T,T)) /\ 301 (Sbox (T,F,T,F,T,F,T,F) = (T,F,T,F,T,T,F,F)) /\ 302 (Sbox (T,F,T,F,T,F,T,T) = (F,T,T,F,F,F,T,F)) /\ 303 (Sbox (T,F,T,F,T,T,F,F) = (T,F,F,T,F,F,F,T)) /\ 304 (Sbox (T,F,T,F,T,T,F,T) = (T,F,F,T,F,T,F,T)) /\ 305 (Sbox (T,F,T,F,T,T,T,F) = (T,T,T,F,F,T,F,F)) /\ 306 (Sbox (T,F,T,F,T,T,T,T) = (F,T,T,T,T,F,F,T)) /\ 307 (Sbox (T,F,T,T,F,F,F,F) = (T,T,T,F,F,T,T,T)) /\ 308 (Sbox (T,F,T,T,F,F,F,T) = (T,T,F,F,T,F,F,F)) /\ 309 (Sbox (T,F,T,T,F,F,T,F) = (F,F,T,T,F,T,T,T)) /\ 310 (Sbox (T,F,T,T,F,F,T,T) = (F,T,T,F,T,T,F,T)) /\ 311 (Sbox (T,F,T,T,F,T,F,F) = (T,F,F,F,T,T,F,T)) /\ 312 (Sbox (T,F,T,T,F,T,F,T) = (T,T,F,T,F,T,F,T)) /\ 313 (Sbox (T,F,T,T,F,T,T,F) = (F,T,F,F,T,T,T,F)) /\ 314 (Sbox (T,F,T,T,F,T,T,T) = (T,F,T,F,T,F,F,T)) /\ 315 (Sbox (T,F,T,T,T,F,F,F) = (F,T,T,F,T,T,F,F)) /\ 316 (Sbox (T,F,T,T,T,F,F,T) = (F,T,F,T,F,T,T,F)) /\ 317 (Sbox (T,F,T,T,T,F,T,F) = (T,T,T,T,F,T,F,F)) /\ 318 (Sbox (T,F,T,T,T,F,T,T) = (T,T,T,F,T,F,T,F)) /\ 319 (Sbox (T,F,T,T,T,T,F,F) = (F,T,T,F,F,T,F,T)) /\ 320 (Sbox (T,F,T,T,T,T,F,T) = (F,T,T,T,T,F,T,F)) /\ 321 (Sbox (T,F,T,T,T,T,T,F) = (T,F,T,F,T,T,T,F)) /\ 322 (Sbox (T,F,T,T,T,T,T,T) = (F,F,F,F,T,F,F,F)) /\ 323 (Sbox (T,T,F,F,F,F,F,F) = (T,F,T,T,T,F,T,F)) /\ 324 (Sbox (T,T,F,F,F,F,F,T) = (F,T,T,T,T,F,F,F)) /\ 325 (Sbox (T,T,F,F,F,F,T,F) = (F,F,T,F,F,T,F,T)) /\ 326 (Sbox (T,T,F,F,F,F,T,T) = (F,F,T,F,T,T,T,F)) /\ 327 (Sbox (T,T,F,F,F,T,F,F) = (F,F,F,T,T,T,F,F)) /\ 328 (Sbox (T,T,F,F,F,T,F,T) = (T,F,T,F,F,T,T,F)) /\ 329 (Sbox (T,T,F,F,F,T,T,F) = (T,F,T,T,F,T,F,F)) /\ 330 (Sbox (T,T,F,F,F,T,T,T) = (T,T,F,F,F,T,T,F)) /\ 331 (Sbox (T,T,F,F,T,F,F,F) = (T,T,T,F,T,F,F,F)) /\ 332 (Sbox (T,T,F,F,T,F,F,T) = (T,T,F,T,T,T,F,T)) /\ 333 (Sbox (T,T,F,F,T,F,T,F) = (F,T,T,T,F,T,F,F)) /\ 334 (Sbox (T,T,F,F,T,F,T,T) = (F,F,F,T,T,T,T,T)) /\ 335 (Sbox (T,T,F,F,T,T,F,F) = (F,T,F,F,T,F,T,T)) /\ 336 (Sbox (T,T,F,F,T,T,F,T) = (T,F,T,T,T,T,F,T)) /\ 337 (Sbox (T,T,F,F,T,T,T,F) = (T,F,F,F,T,F,T,T)) /\ 338 (Sbox (T,T,F,F,T,T,T,T) = (T,F,F,F,T,F,T,F)) /\ 339 (Sbox (T,T,F,T,F,F,F,F) = (F,T,T,T,F,F,F,F)) /\ 340 (Sbox (T,T,F,T,F,F,F,T) = (F,F,T,T,T,T,T,F)) /\ 341 (Sbox (T,T,F,T,F,F,T,F) = (T,F,T,T,F,T,F,T)) /\ 342 (Sbox (T,T,F,T,F,F,T,T) = (F,T,T,F,F,T,T,F)) /\ 343 (Sbox (T,T,F,T,F,T,F,F) = (F,T,F,F,T,F,F,F)) /\ 344 (Sbox (T,T,F,T,F,T,F,T) = (F,F,F,F,F,F,T,T)) /\ 345 (Sbox (T,T,F,T,F,T,T,F) = (T,T,T,T,F,T,T,F)) /\ 346 (Sbox (T,T,F,T,F,T,T,T) = (F,F,F,F,T,T,T,F)) /\ 347 (Sbox (T,T,F,T,T,F,F,F) = (F,T,T,F,F,F,F,T)) /\ 348 (Sbox (T,T,F,T,T,F,F,T) = (F,F,T,T,F,T,F,T)) /\ 349 (Sbox (T,T,F,T,T,F,T,F) = (F,T,F,T,F,T,T,T)) /\ 350 (Sbox (T,T,F,T,T,F,T,T) = (T,F,T,T,T,F,F,T)) /\ 351 (Sbox (T,T,F,T,T,T,F,F) = (T,F,F,F,F,T,T,F)) /\ 352 (Sbox (T,T,F,T,T,T,F,T) = (T,T,F,F,F,F,F,T)) /\ 353 (Sbox (T,T,F,T,T,T,T,F) = (F,F,F,T,T,T,F,T)) /\ 354 (Sbox (T,T,F,T,T,T,T,T) = (T,F,F,T,T,T,T,F)) /\ 355 (Sbox (T,T,T,F,F,F,F,F) = (T,T,T,F,F,F,F,T)) /\ 356 (Sbox (T,T,T,F,F,F,F,T) = (T,T,T,T,T,F,F,F)) /\ 357 (Sbox (T,T,T,F,F,F,T,F) = (T,F,F,T,T,F,F,F)) /\ 358 (Sbox (T,T,T,F,F,F,T,T) = (F,F,F,T,F,F,F,T)) /\ 359 (Sbox (T,T,T,F,F,T,F,F) = (F,T,T,F,T,F,F,T)) /\ 360 (Sbox (T,T,T,F,F,T,F,T) = (T,T,F,T,T,F,F,T)) /\ 361 (Sbox (T,T,T,F,F,T,T,F) = (T,F,F,F,T,T,T,F)) /\ 362 (Sbox (T,T,T,F,F,T,T,T) = (T,F,F,T,F,T,F,F)) /\ 363 (Sbox (T,T,T,F,T,F,F,F) = (T,F,F,T,T,F,T,T)) /\ 364 (Sbox (T,T,T,F,T,F,F,T) = (F,F,F,T,T,T,T,F)) /\ 365 (Sbox (T,T,T,F,T,F,T,F) = (T,F,F,F,F,T,T,T)) /\ 366 (Sbox (T,T,T,F,T,F,T,T) = (T,T,T,F,T,F,F,T)) /\ 367 (Sbox (T,T,T,F,T,T,F,F) = (T,T,F,F,T,T,T,F)) /\ 368 (Sbox (T,T,T,F,T,T,F,T) = (F,T,F,T,F,T,F,T)) /\ 369 (Sbox (T,T,T,F,T,T,T,F) = (F,F,T,F,T,F,F,F)) /\ 370 (Sbox (T,T,T,F,T,T,T,T) = (T,T,F,T,T,T,T,T)) /\ 371 (Sbox (T,T,T,T,F,F,F,F) = (T,F,F,F,T,T,F,F)) /\ 372 (Sbox (T,T,T,T,F,F,F,T) = (T,F,T,F,F,F,F,T)) /\ 373 (Sbox (T,T,T,T,F,F,T,F) = (T,F,F,F,T,F,F,T)) /\ 374 (Sbox (T,T,T,T,F,F,T,T) = (F,F,F,F,T,T,F,T)) /\ 375 (Sbox (T,T,T,T,F,T,F,F) = (T,F,T,T,T,T,T,T)) /\ 376 (Sbox (T,T,T,T,F,T,F,T) = (T,T,T,F,F,T,T,F)) /\ 377 (Sbox (T,T,T,T,F,T,T,F) = (F,T,F,F,F,F,T,F)) /\ 378 (Sbox (T,T,T,T,F,T,T,T) = (F,T,T,F,T,F,F,F)) /\ 379 (Sbox (T,T,T,T,T,F,F,F) = (F,T,F,F,F,F,F,T)) /\ 380 (Sbox (T,T,T,T,T,F,F,T) = (T,F,F,T,T,F,F,T)) /\ 381 (Sbox (T,T,T,T,T,F,T,F) = (F,F,T,F,T,T,F,T)) /\ 382 (Sbox (T,T,T,T,T,F,T,T) = (F,F,F,F,T,T,T,T)) /\ 383 (Sbox (T,T,T,T,T,T,F,F) = (T,F,T,T,F,F,F,F)) /\ 384 (Sbox (T,T,T,T,T,T,F,T) = (F,T,F,T,F,T,F,F)) /\ 385 (Sbox (T,T,T,T,T,T,T,F) = (T,F,T,T,T,F,T,T)) /\ 386 (Sbox (T,T,T,T,T,T,T,T) = (F,F,F,T,F,T,T,F))`; 387 388 389val InvSbox_def = 390 Count.apply Define 391 `(InvSbox(F,F,F,F,F,F,F,F) = (F,T,F,T,F,F,T,F)) /\ 392 (InvSbox(F,F,F,F,F,F,F,T) = (F,F,F,F,T,F,F,T)) /\ 393 (InvSbox(F,F,F,F,F,F,T,F) = (F,T,T,F,T,F,T,F)) /\ 394 (InvSbox(F,F,F,F,F,F,T,T) = (T,T,F,T,F,T,F,T)) /\ 395 (InvSbox(F,F,F,F,F,T,F,F) = (F,F,T,T,F,F,F,F)) /\ 396 (InvSbox(F,F,F,F,F,T,F,T) = (F,F,T,T,F,T,T,F)) /\ 397 (InvSbox(F,F,F,F,F,T,T,F) = (T,F,T,F,F,T,F,T)) /\ 398 (InvSbox(F,F,F,F,F,T,T,T) = (F,F,T,T,T,F,F,F)) /\ 399 (InvSbox(F,F,F,F,T,F,F,F) = (T,F,T,T,T,T,T,T)) /\ 400 (InvSbox(F,F,F,F,T,F,F,T) = (F,T,F,F,F,F,F,F)) /\ 401 (InvSbox(F,F,F,F,T,F,T,F) = (T,F,T,F,F,F,T,T)) /\ 402 (InvSbox(F,F,F,F,T,F,T,T) = (T,F,F,T,T,T,T,F)) /\ 403 (InvSbox(F,F,F,F,T,T,F,F) = (T,F,F,F,F,F,F,T)) /\ 404 (InvSbox(F,F,F,F,T,T,F,T) = (T,T,T,T,F,F,T,T)) /\ 405 (InvSbox(F,F,F,F,T,T,T,F) = (T,T,F,T,F,T,T,T)) /\ 406 (InvSbox(F,F,F,F,T,T,T,T) = (T,T,T,T,T,F,T,T)) /\ 407 (InvSbox(F,F,F,T,F,F,F,F) = (F,T,T,T,T,T,F,F)) /\ 408 (InvSbox(F,F,F,T,F,F,F,T) = (T,T,T,F,F,F,T,T)) /\ 409 (InvSbox(F,F,F,T,F,F,T,F) = (F,F,T,T,T,F,F,T)) /\ 410 (InvSbox(F,F,F,T,F,F,T,T) = (T,F,F,F,F,F,T,F)) /\ 411 (InvSbox(F,F,F,T,F,T,F,F) = (T,F,F,T,T,F,T,T)) /\ 412 (InvSbox(F,F,F,T,F,T,F,T) = (F,F,T,F,T,T,T,T)) /\ 413 (InvSbox(F,F,F,T,F,T,T,F) = (T,T,T,T,T,T,T,T)) /\ 414 (InvSbox(F,F,F,T,F,T,T,T) = (T,F,F,F,F,T,T,T)) /\ 415 (InvSbox(F,F,F,T,T,F,F,F) = (F,F,T,T,F,T,F,F)) /\ 416 (InvSbox(F,F,F,T,T,F,F,T) = (T,F,F,F,T,T,T,F)) /\ 417 (InvSbox(F,F,F,T,T,F,T,F) = (F,T,F,F,F,F,T,T)) /\ 418 (InvSbox(F,F,F,T,T,F,T,T) = (F,T,F,F,F,T,F,F)) /\ 419 (InvSbox(F,F,F,T,T,T,F,F) = (T,T,F,F,F,T,F,F)) /\ 420 (InvSbox(F,F,F,T,T,T,F,T) = (T,T,F,T,T,T,T,F)) /\ 421 (InvSbox(F,F,F,T,T,T,T,F) = (T,T,T,F,T,F,F,T)) /\ 422 (InvSbox(F,F,F,T,T,T,T,T) = (T,T,F,F,T,F,T,T)) /\ 423 (InvSbox(F,F,T,F,F,F,F,F) = (F,T,F,T,F,T,F,F)) /\ 424 (InvSbox(F,F,T,F,F,F,F,T) = (F,T,T,T,T,F,T,T)) /\ 425 (InvSbox(F,F,T,F,F,F,T,F) = (T,F,F,T,F,T,F,F)) /\ 426 (InvSbox(F,F,T,F,F,F,T,T) = (F,F,T,T,F,F,T,F)) /\ 427 (InvSbox(F,F,T,F,F,T,F,F) = (T,F,T,F,F,T,T,F)) /\ 428 (InvSbox(F,F,T,F,F,T,F,T) = (T,T,F,F,F,F,T,F)) /\ 429 (InvSbox(F,F,T,F,F,T,T,F) = (F,F,T,F,F,F,T,T)) /\ 430 (InvSbox(F,F,T,F,F,T,T,T) = (F,F,T,T,T,T,F,T)) /\ 431 (InvSbox(F,F,T,F,T,F,F,F) = (T,T,T,F,T,T,T,F)) /\ 432 (InvSbox(F,F,T,F,T,F,F,T) = (F,T,F,F,T,T,F,F)) /\ 433 (InvSbox(F,F,T,F,T,F,T,F) = (T,F,F,T,F,T,F,T)) /\ 434 (InvSbox(F,F,T,F,T,F,T,T) = (F,F,F,F,T,F,T,T)) /\ 435 (InvSbox(F,F,T,F,T,T,F,F) = (F,T,F,F,F,F,T,F)) /\ 436 (InvSbox(F,F,T,F,T,T,F,T) = (T,T,T,T,T,F,T,F)) /\ 437 (InvSbox(F,F,T,F,T,T,T,F) = (T,T,F,F,F,F,T,T)) /\ 438 (InvSbox(F,F,T,F,T,T,T,T) = (F,T,F,F,T,T,T,F)) /\ 439 (InvSbox(F,F,T,T,F,F,F,F) = (F,F,F,F,T,F,F,F)) /\ 440 (InvSbox(F,F,T,T,F,F,F,T) = (F,F,T,F,T,T,T,F)) /\ 441 (InvSbox(F,F,T,T,F,F,T,F) = (T,F,T,F,F,F,F,T)) /\ 442 (InvSbox(F,F,T,T,F,F,T,T) = (F,T,T,F,F,T,T,F)) /\ 443 (InvSbox(F,F,T,T,F,T,F,F) = (F,F,T,F,T,F,F,F)) /\ 444 (InvSbox(F,F,T,T,F,T,F,T) = (T,T,F,T,T,F,F,T)) /\ 445 (InvSbox(F,F,T,T,F,T,T,F) = (F,F,T,F,F,T,F,F)) /\ 446 (InvSbox(F,F,T,T,F,T,T,T) = (T,F,T,T,F,F,T,F)) /\ 447 (InvSbox(F,F,T,T,T,F,F,F) = (F,T,T,T,F,T,T,F)) /\ 448 (InvSbox(F,F,T,T,T,F,F,T) = (F,T,F,T,T,F,T,T)) /\ 449 (InvSbox(F,F,T,T,T,F,T,F) = (T,F,T,F,F,F,T,F)) /\ 450 (InvSbox(F,F,T,T,T,F,T,T) = (F,T,F,F,T,F,F,T)) /\ 451 (InvSbox(F,F,T,T,T,T,F,F) = (F,T,T,F,T,T,F,T)) /\ 452 (InvSbox(F,F,T,T,T,T,F,T) = (T,F,F,F,T,F,T,T)) /\ 453 (InvSbox(F,F,T,T,T,T,T,F) = (T,T,F,T,F,F,F,T)) /\ 454 (InvSbox(F,F,T,T,T,T,T,T) = (F,F,T,F,F,T,F,T)) /\ 455 (InvSbox(F,T,F,F,F,F,F,F) = (F,T,T,T,F,F,T,F)) /\ 456 (InvSbox(F,T,F,F,F,F,F,T) = (T,T,T,T,T,F,F,F)) /\ 457 (InvSbox(F,T,F,F,F,F,T,F) = (T,T,T,T,F,T,T,F)) /\ 458 (InvSbox(F,T,F,F,F,F,T,T) = (F,T,T,F,F,T,F,F)) /\ 459 (InvSbox(F,T,F,F,F,T,F,F) = (T,F,F,F,F,T,T,F)) /\ 460 (InvSbox(F,T,F,F,F,T,F,T) = (F,T,T,F,T,F,F,F)) /\ 461 (InvSbox(F,T,F,F,F,T,T,F) = (T,F,F,T,T,F,F,F)) /\ 462 (InvSbox(F,T,F,F,F,T,T,T) = (F,F,F,T,F,T,T,F)) /\ 463 (InvSbox(F,T,F,F,T,F,F,F) = (T,T,F,T,F,T,F,F)) /\ 464 (InvSbox(F,T,F,F,T,F,F,T) = (T,F,T,F,F,T,F,F)) /\ 465 (InvSbox(F,T,F,F,T,F,T,F) = (F,T,F,T,T,T,F,F)) /\ 466 (InvSbox(F,T,F,F,T,F,T,T) = (T,T,F,F,T,T,F,F)) /\ 467 (InvSbox(F,T,F,F,T,T,F,F) = (F,T,F,T,T,T,F,T)) /\ 468 (InvSbox(F,T,F,F,T,T,F,T) = (F,T,T,F,F,T,F,T)) /\ 469 (InvSbox(F,T,F,F,T,T,T,F) = (T,F,T,T,F,T,T,F)) /\ 470 (InvSbox(F,T,F,F,T,T,T,T) = (T,F,F,T,F,F,T,F)) /\ 471 (InvSbox(F,T,F,T,F,F,F,F) = (F,T,T,F,T,T,F,F)) /\ 472 (InvSbox(F,T,F,T,F,F,F,T) = (F,T,T,T,F,F,F,F)) /\ 473 (InvSbox(F,T,F,T,F,F,T,F) = (F,T,F,F,T,F,F,F)) /\ 474 (InvSbox(F,T,F,T,F,F,T,T) = (F,T,F,T,F,F,F,F)) /\ 475 (InvSbox(F,T,F,T,F,T,F,F) = (T,T,T,T,T,T,F,T)) /\ 476 (InvSbox(F,T,F,T,F,T,F,T) = (T,T,T,F,T,T,F,T)) /\ 477 (InvSbox(F,T,F,T,F,T,T,F) = (T,F,T,T,T,F,F,T)) /\ 478 (InvSbox(F,T,F,T,F,T,T,T) = (T,T,F,T,T,F,T,F)) /\ 479 (InvSbox(F,T,F,T,T,F,F,F) = (F,T,F,T,T,T,T,F)) /\ 480 (InvSbox(F,T,F,T,T,F,F,T) = (F,F,F,T,F,T,F,T)) /\ 481 (InvSbox(F,T,F,T,T,F,T,F) = (F,T,F,F,F,T,T,F)) /\ 482 (InvSbox(F,T,F,T,T,F,T,T) = (F,T,F,T,F,T,T,T)) /\ 483 (InvSbox(F,T,F,T,T,T,F,F) = (T,F,T,F,F,T,T,T)) /\ 484 (InvSbox(F,T,F,T,T,T,F,T) = (T,F,F,F,T,T,F,T)) /\ 485 (InvSbox(F,T,F,T,T,T,T,F) = (T,F,F,T,T,T,F,T)) /\ 486 (InvSbox(F,T,F,T,T,T,T,T) = (T,F,F,F,F,T,F,F)) /\ 487 (InvSbox(F,T,T,F,F,F,F,F) = (T,F,F,T,F,F,F,F)) /\ 488 (InvSbox(F,T,T,F,F,F,F,T) = (T,T,F,T,T,F,F,F)) /\ 489 (InvSbox(F,T,T,F,F,F,T,F) = (T,F,T,F,T,F,T,T)) /\ 490 (InvSbox(F,T,T,F,F,F,T,T) = (F,F,F,F,F,F,F,F)) /\ 491 (InvSbox(F,T,T,F,F,T,F,F) = (T,F,F,F,T,T,F,F)) /\ 492 (InvSbox(F,T,T,F,F,T,F,T) = (T,F,T,T,T,T,F,F)) /\ 493 (InvSbox(F,T,T,F,F,T,T,F) = (T,T,F,T,F,F,T,T)) /\ 494 (InvSbox(F,T,T,F,F,T,T,T) = (F,F,F,F,T,F,T,F)) /\ 495 (InvSbox(F,T,T,F,T,F,F,F) = (T,T,T,T,F,T,T,T)) /\ 496 (InvSbox(F,T,T,F,T,F,F,T) = (T,T,T,F,F,T,F,F)) /\ 497 (InvSbox(F,T,T,F,T,F,T,F) = (F,T,F,T,T,F,F,F)) /\ 498 (InvSbox(F,T,T,F,T,F,T,T) = (F,F,F,F,F,T,F,T)) /\ 499 (InvSbox(F,T,T,F,T,T,F,F) = (T,F,T,T,T,F,F,F)) /\ 500 (InvSbox(F,T,T,F,T,T,F,T) = (T,F,T,T,F,F,T,T)) /\ 501 (InvSbox(F,T,T,F,T,T,T,F) = (F,T,F,F,F,T,F,T)) /\ 502 (InvSbox(F,T,T,F,T,T,T,T) = (F,F,F,F,F,T,T,F)) /\ 503 (InvSbox(F,T,T,T,F,F,F,F) = (T,T,F,T,F,F,F,F)) /\ 504 (InvSbox(F,T,T,T,F,F,F,T) = (F,F,T,F,T,T,F,F)) /\ 505 (InvSbox(F,T,T,T,F,F,T,F) = (F,F,F,T,T,T,T,F)) /\ 506 (InvSbox(F,T,T,T,F,F,T,T) = (T,F,F,F,T,T,T,T)) /\ 507 (InvSbox(F,T,T,T,F,T,F,F) = (T,T,F,F,T,F,T,F)) /\ 508 (InvSbox(F,T,T,T,F,T,F,T) = (F,F,T,T,T,T,T,T)) /\ 509 (InvSbox(F,T,T,T,F,T,T,F) = (F,F,F,F,T,T,T,T)) /\ 510 (InvSbox(F,T,T,T,F,T,T,T) = (F,F,F,F,F,F,T,F)) /\ 511 (InvSbox(F,T,T,T,T,F,F,F) = (T,T,F,F,F,F,F,T)) /\ 512 (InvSbox(F,T,T,T,T,F,F,T) = (T,F,T,F,T,T,T,T)) /\ 513 (InvSbox(F,T,T,T,T,F,T,F) = (T,F,T,T,T,T,F,T)) /\ 514 (InvSbox(F,T,T,T,T,F,T,T) = (F,F,F,F,F,F,T,T)) /\ 515 (InvSbox(F,T,T,T,T,T,F,F) = (F,F,F,F,F,F,F,T)) /\ 516 (InvSbox(F,T,T,T,T,T,F,T) = (F,F,F,T,F,F,T,T)) /\ 517 (InvSbox(F,T,T,T,T,T,T,F) = (T,F,F,F,T,F,T,F)) /\ 518 (InvSbox(F,T,T,T,T,T,T,T) = (F,T,T,F,T,F,T,T)) /\ 519 (InvSbox(T,F,F,F,F,F,F,F) = (F,F,T,T,T,F,T,F)) /\ 520 (InvSbox(T,F,F,F,F,F,F,T) = (T,F,F,T,F,F,F,T)) /\ 521 (InvSbox(T,F,F,F,F,F,T,F) = (F,F,F,T,F,F,F,T)) /\ 522 (InvSbox(T,F,F,F,F,F,T,T) = (F,T,F,F,F,F,F,T)) /\ 523 (InvSbox(T,F,F,F,F,T,F,F) = (F,T,F,F,T,T,T,T)) /\ 524 (InvSbox(T,F,F,F,F,T,F,T) = (F,T,T,F,F,T,T,T)) /\ 525 (InvSbox(T,F,F,F,F,T,T,F) = (T,T,F,T,T,T,F,F)) /\ 526 (InvSbox(T,F,F,F,F,T,T,T) = (T,T,T,F,T,F,T,F)) /\ 527 (InvSbox(T,F,F,F,T,F,F,F) = (T,F,F,T,F,T,T,T)) /\ 528 (InvSbox(T,F,F,F,T,F,F,T) = (T,T,T,T,F,F,T,F)) /\ 529 (InvSbox(T,F,F,F,T,F,T,F) = (T,T,F,F,T,T,T,T)) /\ 530 (InvSbox(T,F,F,F,T,F,T,T) = (T,T,F,F,T,T,T,F)) /\ 531 (InvSbox(T,F,F,F,T,T,F,F) = (T,T,T,T,F,F,F,F)) /\ 532 (InvSbox(T,F,F,F,T,T,F,T) = (T,F,T,T,F,T,F,F)) /\ 533 (InvSbox(T,F,F,F,T,T,T,F) = (T,T,T,F,F,T,T,F)) /\ 534 (InvSbox(T,F,F,F,T,T,T,T) = (F,T,T,T,F,F,T,T)) /\ 535 (InvSbox(T,F,F,T,F,F,F,F) = (T,F,F,T,F,T,T,F)) /\ 536 (InvSbox(T,F,F,T,F,F,F,T) = (T,F,T,F,T,T,F,F)) /\ 537 (InvSbox(T,F,F,T,F,F,T,F) = (F,T,T,T,F,T,F,F)) /\ 538 (InvSbox(T,F,F,T,F,F,T,T) = (F,F,T,F,F,F,T,F)) /\ 539 (InvSbox(T,F,F,T,F,T,F,F) = (T,T,T,F,F,T,T,T)) /\ 540 (InvSbox(T,F,F,T,F,T,F,T) = (T,F,T,F,T,T,F,T)) /\ 541 (InvSbox(T,F,F,T,F,T,T,F) = (F,F,T,T,F,T,F,T)) /\ 542 (InvSbox(T,F,F,T,F,T,T,T) = (T,F,F,F,F,T,F,T)) /\ 543 (InvSbox(T,F,F,T,T,F,F,F) = (T,T,T,F,F,F,T,F)) /\ 544 (InvSbox(T,F,F,T,T,F,F,T) = (T,T,T,T,T,F,F,T)) /\ 545 (InvSbox(T,F,F,T,T,F,T,F) = (F,F,T,T,F,T,T,T)) /\ 546 (InvSbox(T,F,F,T,T,F,T,T) = (T,T,T,F,T,F,F,F)) /\ 547 (InvSbox(T,F,F,T,T,T,F,F) = (F,F,F,T,T,T,F,F)) /\ 548 (InvSbox(T,F,F,T,T,T,F,T) = (F,T,T,T,F,T,F,T)) /\ 549 (InvSbox(T,F,F,T,T,T,T,F) = (T,T,F,T,T,T,T,T)) /\ 550 (InvSbox(T,F,F,T,T,T,T,T) = (F,T,T,F,T,T,T,F)) /\ 551 (InvSbox(T,F,T,F,F,F,F,F) = (F,T,F,F,F,T,T,T)) /\ 552 (InvSbox(T,F,T,F,F,F,F,T) = (T,T,T,T,F,F,F,T)) /\ 553 (InvSbox(T,F,T,F,F,F,T,F) = (F,F,F,T,T,F,T,F)) /\ 554 (InvSbox(T,F,T,F,F,F,T,T) = (F,T,T,T,F,F,F,T)) /\ 555 (InvSbox(T,F,T,F,F,T,F,F) = (F,F,F,T,T,T,F,T)) /\ 556 (InvSbox(T,F,T,F,F,T,F,T) = (F,F,T,F,T,F,F,T)) /\ 557 (InvSbox(T,F,T,F,F,T,T,F) = (T,T,F,F,F,T,F,T)) /\ 558 (InvSbox(T,F,T,F,F,T,T,T) = (T,F,F,F,T,F,F,T)) /\ 559 (InvSbox(T,F,T,F,T,F,F,F) = (F,T,T,F,T,T,T,T)) /\ 560 (InvSbox(T,F,T,F,T,F,F,T) = (T,F,T,T,F,T,T,T)) /\ 561 (InvSbox(T,F,T,F,T,F,T,F) = (F,T,T,F,F,F,T,F)) /\ 562 (InvSbox(T,F,T,F,T,F,T,T) = (F,F,F,F,T,T,T,F)) /\ 563 (InvSbox(T,F,T,F,T,T,F,F) = (T,F,T,F,T,F,T,F)) /\ 564 (InvSbox(T,F,T,F,T,T,F,T) = (F,F,F,T,T,F,F,F)) /\ 565 (InvSbox(T,F,T,F,T,T,T,F) = (T,F,T,T,T,T,T,F)) /\ 566 (InvSbox(T,F,T,F,T,T,T,T) = (F,F,F,T,T,F,T,T)) /\ 567 (InvSbox(T,F,T,T,F,F,F,F) = (T,T,T,T,T,T,F,F)) /\ 568 (InvSbox(T,F,T,T,F,F,F,T) = (F,T,F,T,F,T,T,F)) /\ 569 (InvSbox(T,F,T,T,F,F,T,F) = (F,F,T,T,T,T,T,F)) /\ 570 (InvSbox(T,F,T,T,F,F,T,T) = (F,T,F,F,T,F,T,T)) /\ 571 (InvSbox(T,F,T,T,F,T,F,F) = (T,T,F,F,F,T,T,F)) /\ 572 (InvSbox(T,F,T,T,F,T,F,T) = (T,T,F,T,F,F,T,F)) /\ 573 (InvSbox(T,F,T,T,F,T,T,F) = (F,T,T,T,T,F,F,T)) /\ 574 (InvSbox(T,F,T,T,F,T,T,T) = (F,F,T,F,F,F,F,F)) /\ 575 (InvSbox(T,F,T,T,T,F,F,F) = (T,F,F,T,T,F,T,F)) /\ 576 (InvSbox(T,F,T,T,T,F,F,T) = (T,T,F,T,T,F,T,T)) /\ 577 (InvSbox(T,F,T,T,T,F,T,F) = (T,T,F,F,F,F,F,F)) /\ 578 (InvSbox(T,F,T,T,T,F,T,T) = (T,T,T,T,T,T,T,F)) /\ 579 (InvSbox(T,F,T,T,T,T,F,F) = (F,T,T,T,T,F,F,F)) /\ 580 (InvSbox(T,F,T,T,T,T,F,T) = (T,T,F,F,T,T,F,T)) /\ 581 (InvSbox(T,F,T,T,T,T,T,F) = (F,T,F,T,T,F,T,F)) /\ 582 (InvSbox(T,F,T,T,T,T,T,T) = (T,T,T,T,F,T,F,F)) /\ 583 (InvSbox(T,T,F,F,F,F,F,F) = (F,F,F,T,T,T,T,T)) /\ 584 (InvSbox(T,T,F,F,F,F,F,T) = (T,T,F,T,T,T,F,T)) /\ 585 (InvSbox(T,T,F,F,F,F,T,F) = (T,F,T,F,T,F,F,F)) /\ 586 (InvSbox(T,T,F,F,F,F,T,T) = (F,F,T,T,F,F,T,T)) /\ 587 (InvSbox(T,T,F,F,F,T,F,F) = (T,F,F,F,T,F,F,F)) /\ 588 (InvSbox(T,T,F,F,F,T,F,T) = (F,F,F,F,F,T,T,T)) /\ 589 (InvSbox(T,T,F,F,F,T,T,F) = (T,T,F,F,F,T,T,T)) /\ 590 (InvSbox(T,T,F,F,F,T,T,T) = (F,F,T,T,F,F,F,T)) /\ 591 (InvSbox(T,T,F,F,T,F,F,F) = (T,F,T,T,F,F,F,T)) /\ 592 (InvSbox(T,T,F,F,T,F,F,T) = (F,F,F,T,F,F,T,F)) /\ 593 (InvSbox(T,T,F,F,T,F,T,F) = (F,F,F,T,F,F,F,F)) /\ 594 (InvSbox(T,T,F,F,T,F,T,T) = (F,T,F,T,T,F,F,T)) /\ 595 (InvSbox(T,T,F,F,T,T,F,F) = (F,F,T,F,F,T,T,T)) /\ 596 (InvSbox(T,T,F,F,T,T,F,T) = (T,F,F,F,F,F,F,F)) /\ 597 (InvSbox(T,T,F,F,T,T,T,F) = (T,T,T,F,T,T,F,F)) /\ 598 (InvSbox(T,T,F,F,T,T,T,T) = (F,T,F,T,T,T,T,T)) /\ 599 (InvSbox(T,T,F,T,F,F,F,F) = (F,T,T,F,F,F,F,F)) /\ 600 (InvSbox(T,T,F,T,F,F,F,T) = (F,T,F,T,F,F,F,T)) /\ 601 (InvSbox(T,T,F,T,F,F,T,F) = (F,T,T,T,T,T,T,T)) /\ 602 (InvSbox(T,T,F,T,F,F,T,T) = (T,F,T,F,T,F,F,T)) /\ 603 (InvSbox(T,T,F,T,F,T,F,F) = (F,F,F,T,T,F,F,T)) /\ 604 (InvSbox(T,T,F,T,F,T,F,T) = (T,F,T,T,F,T,F,T)) /\ 605 (InvSbox(T,T,F,T,F,T,T,F) = (F,T,F,F,T,F,T,F)) /\ 606 (InvSbox(T,T,F,T,F,T,T,T) = (F,F,F,F,T,T,F,T)) /\ 607 (InvSbox(T,T,F,T,T,F,F,F) = (F,F,T,F,T,T,F,T)) /\ 608 (InvSbox(T,T,F,T,T,F,F,T) = (T,T,T,F,F,T,F,T)) /\ 609 (InvSbox(T,T,F,T,T,F,T,F) = (F,T,T,T,T,F,T,F)) /\ 610 (InvSbox(T,T,F,T,T,F,T,T) = (T,F,F,T,T,T,T,T)) /\ 611 (InvSbox(T,T,F,T,T,T,F,F) = (T,F,F,T,F,F,T,T)) /\ 612 (InvSbox(T,T,F,T,T,T,F,T) = (T,T,F,F,T,F,F,T)) /\ 613 (InvSbox(T,T,F,T,T,T,T,F) = (T,F,F,T,T,T,F,F)) /\ 614 (InvSbox(T,T,F,T,T,T,T,T) = (T,T,T,F,T,T,T,T)) /\ 615 (InvSbox(T,T,T,F,F,F,F,F) = (T,F,T,F,F,F,F,F)) /\ 616 (InvSbox(T,T,T,F,F,F,F,T) = (T,T,T,F,F,F,F,F)) /\ 617 (InvSbox(T,T,T,F,F,F,T,F) = (F,F,T,T,T,F,T,T)) /\ 618 (InvSbox(T,T,T,F,F,F,T,T) = (F,T,F,F,T,T,F,T)) /\ 619 (InvSbox(T,T,T,F,F,T,F,F) = (T,F,T,F,T,T,T,F)) /\ 620 (InvSbox(T,T,T,F,F,T,F,T) = (F,F,T,F,T,F,T,F)) /\ 621 (InvSbox(T,T,T,F,F,T,T,F) = (T,T,T,T,F,T,F,T)) /\ 622 (InvSbox(T,T,T,F,F,T,T,T) = (T,F,T,T,F,F,F,F)) /\ 623 (InvSbox(T,T,T,F,T,F,F,F) = (T,T,F,F,T,F,F,F)) /\ 624 (InvSbox(T,T,T,F,T,F,F,T) = (T,T,T,F,T,F,T,T)) /\ 625 (InvSbox(T,T,T,F,T,F,T,F) = (T,F,T,T,T,F,T,T)) /\ 626 (InvSbox(T,T,T,F,T,F,T,T) = (F,F,T,T,T,T,F,F)) /\ 627 (InvSbox(T,T,T,F,T,T,F,F) = (T,F,F,F,F,F,T,T)) /\ 628 (InvSbox(T,T,T,F,T,T,F,T) = (F,T,F,T,F,F,T,T)) /\ 629 (InvSbox(T,T,T,F,T,T,T,F) = (T,F,F,T,T,F,F,T)) /\ 630 (InvSbox(T,T,T,F,T,T,T,T) = (F,T,T,F,F,F,F,T)) /\ 631 (InvSbox(T,T,T,T,F,F,F,F) = (F,F,F,T,F,T,T,T)) /\ 632 (InvSbox(T,T,T,T,F,F,F,T) = (F,F,T,F,T,F,T,T)) /\ 633 (InvSbox(T,T,T,T,F,F,T,F) = (F,F,F,F,F,T,F,F)) /\ 634 (InvSbox(T,T,T,T,F,F,T,T) = (F,T,T,T,T,T,T,F)) /\ 635 (InvSbox(T,T,T,T,F,T,F,F) = (T,F,T,T,T,F,T,F)) /\ 636 (InvSbox(T,T,T,T,F,T,F,T) = (F,T,T,T,F,T,T,T)) /\ 637 (InvSbox(T,T,T,T,F,T,T,F) = (T,T,F,T,F,T,T,F)) /\ 638 (InvSbox(T,T,T,T,F,T,T,T) = (F,F,T,F,F,T,T,F)) /\ 639 (InvSbox(T,T,T,T,T,F,F,F) = (T,T,T,F,F,F,F,T)) /\ 640 (InvSbox(T,T,T,T,T,F,F,T) = (F,T,T,F,T,F,F,T)) /\ 641 (InvSbox(T,T,T,T,T,F,T,F) = (F,F,F,T,F,T,F,F)) /\ 642 (InvSbox(T,T,T,T,T,F,T,T) = (F,T,T,F,F,F,T,T)) /\ 643 (InvSbox(T,T,T,T,T,T,F,F) = (F,T,F,T,F,T,F,T)) /\ 644 (InvSbox(T,T,T,T,T,T,F,T) = (F,F,T,F,F,F,F,T)) /\ 645 (InvSbox(T,T,T,T,T,T,T,F) = (F,F,F,F,T,T,F,F)) /\ 646 (InvSbox(T,T,T,T,T,T,T,T) = (F,T,T,T,T,T,F,T))`; 647 648 649 650val Sbox_Inversion = Q.store_thm 651("Sbox_Inversion", 652 `!w:word8. InvSbox (Sbox w) = w`, 653 SIMP_TAC std_ss [FORALL_BYTE_BITS,Sbox_def, InvSbox_def]); 654 655val _ = export_theory(); 656