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