1(*===========================================================================*)
2(* Simple theory of bytes.                                                   *)
3(*===========================================================================*)
4
5open HolKernel Parse boolLib bossLib
6     pairTheory;
7
8val _ = new_theory "word8";
9
10(*---------------------------------------------------------------------------*)
11(* 8 bits per byte, represented as an 8-tuple of truth values.               *)
12(*---------------------------------------------------------------------------*)
13
14val _ = type_abbrev("word8", Type`:bool#bool#bool#bool#bool#bool#bool#bool`);
15
16val ZERO_def   = Define   `ZERO = (F,F,F,F,F,F,F,F)`;
17val ONE_def    = Define    `ONE = (F,F,F,F,F,F,F,T)`;
18val TWO_def    = Define    `TWO = (F,F,F,F,F,F,T,F)`;
19val THREE_def  = Define  `THREE = (F,F,F,F,F,F,T,T)`;
20
21(*---------------------------------------------------------------------------*)
22(* There are two ways to do case-analysis on bytes: as an 8-tuple of         *)
23(* variables, or as 256 tuples of bits. The former is useful for symbolic    *)
24(* evaluation, while the other is good for brute-force.                      *)
25(*---------------------------------------------------------------------------*)
26
27val FORALL_BYTE_VARS = Q.store_thm
28("FORALL_BYTE_VARS",
29 `(!x:word8. P x) = !b7 b6 b5 b4 b3 b2 b1 b0. P(b7,b6,b5,b4,b3,b2,b1,b0)`,
30 SIMP_TAC std_ss [FORALL_PROD]);
31
32val FORALL_BYTE_BITS = Q.store_thm
33("FORALL_BYTE_BITS",
34 `(!x:word8. P x) =
35  P (F,F,F,F,F,F,F,F) /\ P (F,F,F,F,F,F,F,T) /\ P (F,F,F,F,F,F,T,F) /\
36  P (F,F,F,F,F,F,T,T) /\ P (F,F,F,F,F,T,F,F) /\ P (F,F,F,F,F,T,F,T) /\
37  P (F,F,F,F,F,T,T,F) /\ P (F,F,F,F,F,T,T,T) /\ P (F,F,F,F,T,F,F,F) /\
38  P (F,F,F,F,T,F,F,T) /\ P (F,F,F,F,T,F,T,F) /\ P (F,F,F,F,T,F,T,T) /\
39  P (F,F,F,F,T,T,F,F) /\ P (F,F,F,F,T,T,F,T) /\ P (F,F,F,F,T,T,T,F) /\
40  P (F,F,F,F,T,T,T,T) /\ P (F,F,F,T,F,F,F,F) /\ P (F,F,F,T,F,F,F,T) /\
41  P (F,F,F,T,F,F,T,F) /\ P (F,F,F,T,F,F,T,T) /\ P (F,F,F,T,F,T,F,F) /\
42  P (F,F,F,T,F,T,F,T) /\ P (F,F,F,T,F,T,T,F) /\ P (F,F,F,T,F,T,T,T) /\
43  P (F,F,F,T,T,F,F,F) /\ P (F,F,F,T,T,F,F,T) /\ P (F,F,F,T,T,F,T,F) /\
44  P (F,F,F,T,T,F,T,T) /\ P (F,F,F,T,T,T,F,F) /\ P (F,F,F,T,T,T,F,T) /\
45  P (F,F,F,T,T,T,T,F) /\ P (F,F,F,T,T,T,T,T) /\ P (F,F,T,F,F,F,F,F) /\
46  P (F,F,T,F,F,F,F,T) /\ P (F,F,T,F,F,F,T,F) /\ P (F,F,T,F,F,F,T,T) /\
47  P (F,F,T,F,F,T,F,F) /\ P (F,F,T,F,F,T,F,T) /\ P (F,F,T,F,F,T,T,F) /\
48  P (F,F,T,F,F,T,T,T) /\ P (F,F,T,F,T,F,F,F) /\ P (F,F,T,F,T,F,F,T) /\
49  P (F,F,T,F,T,F,T,F) /\ P (F,F,T,F,T,F,T,T) /\ P (F,F,T,F,T,T,F,F) /\
50  P (F,F,T,F,T,T,F,T) /\ P (F,F,T,F,T,T,T,F) /\ P (F,F,T,F,T,T,T,T) /\
51  P (F,F,T,T,F,F,F,F) /\ P (F,F,T,T,F,F,F,T) /\ P (F,F,T,T,F,F,T,F) /\
52  P (F,F,T,T,F,F,T,T) /\ P (F,F,T,T,F,T,F,F) /\ P (F,F,T,T,F,T,F,T) /\
53  P (F,F,T,T,F,T,T,F) /\ P (F,F,T,T,F,T,T,T) /\ P (F,F,T,T,T,F,F,F) /\
54  P (F,F,T,T,T,F,F,T) /\ P (F,F,T,T,T,F,T,F) /\ P (F,F,T,T,T,F,T,T) /\
55  P (F,F,T,T,T,T,F,F) /\ P (F,F,T,T,T,T,F,T) /\ P (F,F,T,T,T,T,T,F) /\
56  P (F,F,T,T,T,T,T,T) /\ P (F,T,F,F,F,F,F,F) /\ P (F,T,F,F,F,F,F,T) /\
57  P (F,T,F,F,F,F,T,F) /\ P (F,T,F,F,F,F,T,T) /\ P (F,T,F,F,F,T,F,F) /\
58  P (F,T,F,F,F,T,F,T) /\ P (F,T,F,F,F,T,T,F) /\ P (F,T,F,F,F,T,T,T) /\
59  P (F,T,F,F,T,F,F,F) /\ P (F,T,F,F,T,F,F,T) /\ P (F,T,F,F,T,F,T,F) /\
60  P (F,T,F,F,T,F,T,T) /\ P (F,T,F,F,T,T,F,F) /\ P (F,T,F,F,T,T,F,T) /\
61  P (F,T,F,F,T,T,T,F) /\ P (F,T,F,F,T,T,T,T) /\ P (F,T,F,T,F,F,F,F) /\
62  P (F,T,F,T,F,F,F,T) /\ P (F,T,F,T,F,F,T,F) /\ P (F,T,F,T,F,F,T,T) /\
63  P (F,T,F,T,F,T,F,F) /\ P (F,T,F,T,F,T,F,T) /\ P (F,T,F,T,F,T,T,F) /\
64  P (F,T,F,T,F,T,T,T) /\ P (F,T,F,T,T,F,F,F) /\ P (F,T,F,T,T,F,F,T) /\
65  P (F,T,F,T,T,F,T,F) /\ P (F,T,F,T,T,F,T,T) /\ P (F,T,F,T,T,T,F,F) /\
66  P (F,T,F,T,T,T,F,T) /\ P (F,T,F,T,T,T,T,F) /\ P (F,T,F,T,T,T,T,T) /\
67  P (F,T,T,F,F,F,F,F) /\ P (F,T,T,F,F,F,F,T) /\ P (F,T,T,F,F,F,T,F) /\
68  P (F,T,T,F,F,F,T,T) /\ P (F,T,T,F,F,T,F,F) /\ P (F,T,T,F,F,T,F,T) /\
69  P (F,T,T,F,F,T,T,F) /\ P (F,T,T,F,F,T,T,T) /\ P (F,T,T,F,T,F,F,F) /\
70  P (F,T,T,F,T,F,F,T) /\ P (F,T,T,F,T,F,T,F) /\ P (F,T,T,F,T,F,T,T) /\
71  P (F,T,T,F,T,T,F,F) /\ P (F,T,T,F,T,T,F,T) /\ P (F,T,T,F,T,T,T,F) /\
72  P (F,T,T,F,T,T,T,T) /\ P (F,T,T,T,F,F,F,F) /\ P (F,T,T,T,F,F,F,T) /\
73  P (F,T,T,T,F,F,T,F) /\ P (F,T,T,T,F,F,T,T) /\ P (F,T,T,T,F,T,F,F) /\
74  P (F,T,T,T,F,T,F,T) /\ P (F,T,T,T,F,T,T,F) /\ P (F,T,T,T,F,T,T,T) /\
75  P (F,T,T,T,T,F,F,F) /\ P (F,T,T,T,T,F,F,T) /\ P (F,T,T,T,T,F,T,F) /\
76  P (F,T,T,T,T,F,T,T) /\ P (F,T,T,T,T,T,F,F) /\ P (F,T,T,T,T,T,F,T) /\
77  P (F,T,T,T,T,T,T,F) /\ P (F,T,T,T,T,T,T,T) /\ P (T,F,F,F,F,F,F,F) /\
78  P (T,F,F,F,F,F,F,T) /\ P (T,F,F,F,F,F,T,F) /\ P (T,F,F,F,F,F,T,T) /\
79  P (T,F,F,F,F,T,F,F) /\ P (T,F,F,F,F,T,F,T) /\ P (T,F,F,F,F,T,T,F) /\
80  P (T,F,F,F,F,T,T,T) /\ P (T,F,F,F,T,F,F,F) /\ P (T,F,F,F,T,F,F,T) /\
81  P (T,F,F,F,T,F,T,F) /\ P (T,F,F,F,T,F,T,T) /\ P (T,F,F,F,T,T,F,F) /\
82  P (T,F,F,F,T,T,F,T) /\ P (T,F,F,F,T,T,T,F) /\ P (T,F,F,F,T,T,T,T) /\
83  P (T,F,F,T,F,F,F,F) /\ P (T,F,F,T,F,F,F,T) /\ P (T,F,F,T,F,F,T,F) /\
84  P (T,F,F,T,F,F,T,T) /\ P (T,F,F,T,F,T,F,F) /\ P (T,F,F,T,F,T,F,T) /\
85  P (T,F,F,T,F,T,T,F) /\ P (T,F,F,T,F,T,T,T) /\ P (T,F,F,T,T,F,F,F) /\
86  P (T,F,F,T,T,F,F,T) /\ P (T,F,F,T,T,F,T,F) /\ P (T,F,F,T,T,F,T,T) /\
87  P (T,F,F,T,T,T,F,F) /\ P (T,F,F,T,T,T,F,T) /\ P (T,F,F,T,T,T,T,F) /\
88  P (T,F,F,T,T,T,T,T) /\ P (T,F,T,F,F,F,F,F) /\ P (T,F,T,F,F,F,F,T) /\
89  P (T,F,T,F,F,F,T,F) /\ P (T,F,T,F,F,F,T,T) /\ P (T,F,T,F,F,T,F,F) /\
90  P (T,F,T,F,F,T,F,T) /\ P (T,F,T,F,F,T,T,F) /\ P (T,F,T,F,F,T,T,T) /\
91  P (T,F,T,F,T,F,F,F) /\ P (T,F,T,F,T,F,F,T) /\ P (T,F,T,F,T,F,T,F) /\
92  P (T,F,T,F,T,F,T,T) /\ P (T,F,T,F,T,T,F,F) /\ P (T,F,T,F,T,T,F,T) /\
93  P (T,F,T,F,T,T,T,F) /\ P (T,F,T,F,T,T,T,T) /\ P (T,F,T,T,F,F,F,F) /\
94  P (T,F,T,T,F,F,F,T) /\ P (T,F,T,T,F,F,T,F) /\ P (T,F,T,T,F,F,T,T) /\
95  P (T,F,T,T,F,T,F,F) /\ P (T,F,T,T,F,T,F,T) /\ P (T,F,T,T,F,T,T,F) /\
96  P (T,F,T,T,F,T,T,T) /\ P (T,F,T,T,T,F,F,F) /\ P (T,F,T,T,T,F,F,T) /\
97  P (T,F,T,T,T,F,T,F) /\ P (T,F,T,T,T,F,T,T) /\ P (T,F,T,T,T,T,F,F) /\
98  P (T,F,T,T,T,T,F,T) /\ P (T,F,T,T,T,T,T,F) /\ P (T,F,T,T,T,T,T,T) /\
99  P (T,T,F,F,F,F,F,F) /\ P (T,T,F,F,F,F,F,T) /\ P (T,T,F,F,F,F,T,F) /\
100  P (T,T,F,F,F,F,T,T) /\ P (T,T,F,F,F,T,F,F) /\ P (T,T,F,F,F,T,F,T) /\
101  P (T,T,F,F,F,T,T,F) /\ P (T,T,F,F,F,T,T,T) /\ P (T,T,F,F,T,F,F,F) /\
102  P (T,T,F,F,T,F,F,T) /\ P (T,T,F,F,T,F,T,F) /\ P (T,T,F,F,T,F,T,T) /\
103  P (T,T,F,F,T,T,F,F) /\ P (T,T,F,F,T,T,F,T) /\ P (T,T,F,F,T,T,T,F) /\
104  P (T,T,F,F,T,T,T,T) /\ P (T,T,F,T,F,F,F,F) /\ P (T,T,F,T,F,F,F,T) /\
105  P (T,T,F,T,F,F,T,F) /\ P (T,T,F,T,F,F,T,T) /\ P (T,T,F,T,F,T,F,F) /\
106  P (T,T,F,T,F,T,F,T) /\ P (T,T,F,T,F,T,T,F) /\ P (T,T,F,T,F,T,T,T) /\
107  P (T,T,F,T,T,F,F,F) /\ P (T,T,F,T,T,F,F,T) /\ P (T,T,F,T,T,F,T,F) /\
108  P (T,T,F,T,T,F,T,T) /\ P (T,T,F,T,T,T,F,F) /\ P (T,T,F,T,T,T,F,T) /\
109  P (T,T,F,T,T,T,T,F) /\ P (T,T,F,T,T,T,T,T) /\ P (T,T,T,F,F,F,F,F) /\
110  P (T,T,T,F,F,F,F,T) /\ P (T,T,T,F,F,F,T,F) /\ P (T,T,T,F,F,F,T,T) /\
111  P (T,T,T,F,F,T,F,F) /\ P (T,T,T,F,F,T,F,T) /\ P (T,T,T,F,F,T,T,F) /\
112  P (T,T,T,F,F,T,T,T) /\ P (T,T,T,F,T,F,F,F) /\ P (T,T,T,F,T,F,F,T) /\
113  P (T,T,T,F,T,F,T,F) /\ P (T,T,T,F,T,F,T,T) /\ P (T,T,T,F,T,T,F,F) /\
114  P (T,T,T,F,T,T,F,T) /\ P (T,T,T,F,T,T,T,F) /\ P (T,T,T,F,T,T,T,T) /\
115  P (T,T,T,T,F,F,F,F) /\ P (T,T,T,T,F,F,F,T) /\ P (T,T,T,T,F,F,T,F) /\
116  P (T,T,T,T,F,F,T,T) /\ P (T,T,T,T,F,T,F,F) /\ P (T,T,T,T,F,T,F,T) /\
117  P (T,T,T,T,F,T,T,F) /\ P (T,T,T,T,F,T,T,T) /\ P (T,T,T,T,T,F,F,F) /\
118  P (T,T,T,T,T,F,F,T) /\ P (T,T,T,T,T,F,T,F) /\ P (T,T,T,T,T,F,T,T) /\
119  P (T,T,T,T,T,T,F,F) /\ P (T,T,T,T,T,T,F,T) /\ P (T,T,T,T,T,T,T,F) /\
120  P (T,T,T,T,T,T,T,T)`,
121 EQ_TAC THENL
122  [DISCH_TAC THEN ASM_REWRITE_TAC [],
123   SIMP_TAC std_ss [FORALL_PROD, FORALL_BOOL]]);
124
125
126(*---------------------------------------------------------------------------*)
127(* Bytes and numbers.                                                        *)
128(*---------------------------------------------------------------------------*)
129
130val B2N = Define `(B2N T = 1) /\ (B2N F = 0)`;
131
132val BYTE_TO_NUM = Define
133   `BYTE_TO_NUM (b7,b6,b5,b4,b3,b2,b1,b0) =
134      128*B2N(b7) + 64*B2N(b6) + 32*B2N(b5) +
135       16*B2N(b4) +  8*B2N(b3) +  4*B2N(b2) + 2*B2N(b1) + B2N(b0)`;
136
137val NUM_TO_BYTE = Define
138   `NUM_TO_BYTE n7 =
139      let n6 = n7 DIV 2 in
140      let n5 = n6 DIV 2 in
141      let n4 = n5 DIV 2 in
142      let n3 = n4 DIV 2 in
143      let n2 = n3 DIV 2 in
144      let n1 = n2 DIV 2 in
145      let n0 = n1 DIV 2
146      in
147        (ODD n0, ODD n1, ODD n2, ODD n3,
148         ODD n4, ODD n5, ODD n6, ODD n7)`;
149
150
151val BYTE_TO_NUM_TO_BYTE = Q.store_thm
152("BYTE_TO_NUM_TO_BYTE",
153 `!b. NUM_TO_BYTE(BYTE_TO_NUM b) = b`,
154 SIMP_TAC std_ss [FORALL_BYTE_BITS] THEN EVAL_TAC);
155
156val NUM_TO_BYTE_TO_NUM = Q.store_thm
157("NUM_TO_BYTE_TO_NUM",
158 `!n. n < 256 ==> (BYTE_TO_NUM (NUM_TO_BYTE n) = n)`,
159 CONV_TAC (REPEATC (numLib.BOUNDED_FORALL_CONV EVAL)) THEN PROVE_TAC []);
160
161
162(*---------------------------------------------------------------------------
163        Shift a byte left and right
164 ---------------------------------------------------------------------------*)
165
166val LeftShift = Define
167   `LeftShift (b7,b6,b5,b4,b3,b2,b1,b0):word8 = (b6,b5,b4,b3,b2,b1,b0,F)`;
168
169val RightShift = Define
170   `RightShift (b7,b6,b5,b4,b3,b2,b1,b0):word8 = (F,b7,b6,b5,b4,b3,b2,b1)`;
171
172(*---------------------------------------------------------------------------
173       Compare bits and bytes as if they were numbers. Not currently used
174 ---------------------------------------------------------------------------*)
175
176(*
177
178val _ = Hol_datatype `order = LESS | EQUAL | GREATER`;
179
180val BIT_COMPARE = Define
181  `(BIT_COMPARE F T = LESS) /\
182   (BIT_COMPARE T F = GREATER) /\
183   (BIT_COMPARE x y = EQUAL)`;
184
185
186val BYTE_COMPARE = Define
187  `BYTE_COMPARE (a7,a6,a5,a4,a3,a2,a1,a0)
188                (b7,b6,b5,b4,b3,b2,b1,b0) =
189    case BIT_COMPARE a7 b7
190     of EQUAL ->
191        (case BIT_COMPARE a6 b6
192          of EQUAL ->
193             (case BIT_COMPARE a5 b5
194               of EQUAL ->
195                  (case BIT_COMPARE a4 b4
196                    of EQUAL ->
197                       (case BIT_COMPARE a3 b3
198                         of EQUAL ->
199                            (case BIT_COMPARE a2 b2
200                              of EQUAL ->
201                                 (case BIT_COMPARE a1 b1
202                                   of EQUAL -> BIT_COMPARE a0 b0
203                                   || other -> other)
204                              || other -> other)
205                         || other -> other)
206                    || other -> other)
207               || other -> other)
208          || other -> other)
209     || other -> other`;
210*)
211
212(*---------------------------------------------------------------------------*)
213(* XOR and AND on bytes                                                      *)
214(*---------------------------------------------------------------------------*)
215
216val _ = (set_fixity "XOR"     (Infixr 350);
217         set_fixity "XOR8x4"  (Infixr 350);
218         set_fixity "XOR8"    (Infixr 350);
219         set_fixity "AND8"    (Infixr 350));
220
221val XOR_def =  Define `(x:bool) XOR y = ~(x=y)`;
222
223val XOR8_def = Define
224 `(a,b,c,d,e,f,g,h) XOR8 (a1,b1,c1,d1,e1,f1,g1,h1)
225                     =
226                 (a XOR a1,
227                  b XOR b1,
228                  c XOR c1,
229                  d XOR d1,
230                  e XOR e1,
231                  f XOR f1,
232                  g XOR g1,
233                  h XOR h1)`;
234
235val _ = overload_on ("#",Term`$XOR8`);
236val _ = set_fixity "#" (Infixl 625);
237
238val AND8_def = Define
239 `(a,b,c,d,e,f,g,h) AND8 (a1,b1,c1,d1,e1,f1,g1,h1)
240                     =
241                 (a /\ a1,
242                  b /\ b1,
243                  c /\ c1,
244                  d /\ d1,
245                  e /\ e1,
246                  f /\ f1,
247                  g /\ g1,
248                  h /\ h1)`;
249
250val _ = overload_on ("&",Term`$AND8`);
251val _ = set_fixity "&" (Infixl 650);
252
253(*---------------------------------------------------------------------------*)
254(* Algebraic lemmas for XOR8                                                 *)
255(*---------------------------------------------------------------------------*)
256
257val XOR8_ZERO = Q.store_thm
258("XOR8_ZERO",
259 `!x. x # ZERO = x`,
260 SIMP_TAC std_ss [FORALL_BYTE_VARS,XOR_def,XOR8_def,ZERO_def]);
261
262val XOR8_INV = Q.store_thm
263("XOR8_INV",
264 `!x. x # x = ZERO`,
265 SIMP_TAC std_ss [FORALL_BYTE_VARS,XOR_def,XOR8_def,ZERO_def]);
266
267val XOR8_AC = Q.store_thm
268("XOR8_AC",
269 `(!x y z:word8. (x # y) # z = x # (y # z)) /\
270  (!x y:word8. (x # y) = (y # x))`,
271 SIMP_TAC std_ss [FORALL_BYTE_VARS,XOR_def,XOR8_def]
272 THEN REPEAT STRIP_TAC
273 THEN DECIDE_TAC);
274
275val _ = export_theory();
276
277