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