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