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