1(* ========================================================================= *) 2(* FILE : alignmentScript.sml *) 3(* DESCRIPTION : Theory for address alignment. *) 4(* ========================================================================= *) 5 6open HolKernel Parse boolLib bossLib Q 7open wordsLib 8 9val () = new_theory "alignment"; 10 11val ERR = mk_HOL_ERR "alignmentScript" 12 13(* ------------------------------------------------------------------------- 14 Constant definitions 15 ------------------------------------------------------------------------- *) 16 17val align_def = Define `align p (w: 'a word) = (dimindex (:'a) - 1 '' p) w` 18val aligned_def = Define `aligned p w = (align p w = w)` 19 20val byte_align_def = Define` 21 byte_align (w: 'a word) = align (LOG2 (dimindex(:'a) DIV 8)) w` 22 23val byte_aligned_def = Define` 24 byte_aligned (w: 'a word) = aligned (LOG2 (dimindex(:'a) DIV 8)) w` 25 26(* ------------------------------------------------------------------------- 27 Theorems 28 ------------------------------------------------------------------------- *) 29 30val align_0 = Q.store_thm("align_0", 31 `!w. align 0 w = w`, 32 lrw [wordsTheory.WORD_SLICE_BITS_THM, wordsTheory.WORD_ALL_BITS, align_def] 33 ) 34 35val align_align = Q.store_thm("align_align", 36 `!p w. align p (align p w) = align p w`, 37 srw_tac [wordsLib.WORD_BIT_EQ_ss, boolSimps.CONJ_ss] [align_def] 38 ) 39 40val aligned_align = Q.store_thm ("aligned_align", 41 `!p w. aligned p (align p w)`, 42 rewrite_tac [aligned_def, align_align] 43 ) 44 45val align_aligned = Q.store_thm ("align_aligned", 46 `!p w. aligned p w ==> (align p w = w)`, 47 rewrite_tac [aligned_def] 48 ) 49 50val align_bitwise_and = Q.store_thm("align_bitwise_and", 51 `!p w. align p w = w && UINT_MAXw << p`, 52 srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def] 53 \\ decide_tac 54 ) 55 56val align_shift = Q.store_thm("align_shift", 57 `!p w. align p w = w >>> p << p`, 58 srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def] 59 \\ Cases_on `p <= i` 60 \\ simp [] 61 ) 62 63val align_w2n = Q.store_thm("align_w2n", 64 `!p w. align p w = n2w (w2n w DIV 2 ** p * 2 ** p)`, 65 strip_tac 66 \\ Cases 67 \\ lrw [align_shift, GSYM wordsTheory.n2w_DIV, wordsTheory.word_lsl_n2w, 68 wordsTheory.dimword_def] 69 \\ `dimindex(:'a) <= p` by decide_tac 70 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 71 \\ simp [arithmeticTheory.EXP_ADD, arithmeticTheory.MOD_EQ_0] 72 ) 73 74val ths = [GSYM wordsTheory.WORD_w2w_EXTRACT, wordsTheory.w2w_id] 75 76val lem = 77 wordsTheory.EXTRACT_JOIN_ADD 78 |> Thm.INST_TYPE [Type.beta |-> Type.alpha] 79 |> Q.SPECL [`dimindex(:'a) - 1`, `p - 1`, `p`, `0`, `p`, `w`] 80 |> Q.DISCH `0 < p` 81 |> SIMP_RULE (srw_ss()) (DECIDE ``0 < p ==> (p = p - 1 + 1)`` :: ths) 82 |> GSYM 83 84val align_sub = Q.store_thm("align_sub", 85 `!p w. align p w = if p = 0 then w else w - (p - 1 >< 0) w`, 86 rw_tac bool_ss [align_0] 87 \\ Cases_on `dimindex(:'a) <= p - 1` 88 >- ( 89 `(p - 1 >< 0) w : 'a word = (dimindex (:'a) - 1 >< 0) w` 90 by simp [wordsTheory.WORD_EXTRACT_MIN_HIGH] 91 \\ rule_assum_tac (SIMP_RULE (srw_ss()) ths) 92 \\ asm_rewrite_tac [] 93 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def] 94 ) 95 \\ Cases_on `p = dimindex(:'a)` 96 >- srw_tac [wordsLib.WORD_BIT_EQ_ss] (align_def :: ths) 97 \\ `0 < p /\ p <= dimindex (:'a) - 1` by decide_tac 98 \\ imp_res_tac lem 99 \\ pop_assum (qspec_then `w` (CONV_TAC o Conv.PATH_CONV "rlr" o Lib.K)) 100 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] [align_def] 101 ) 102 103val aligned_extract = Q.store_thm ("aligned_extract", 104 `!p w. aligned p (w: 'a word) = (p = 0) \/ ((p - 1 >< 0) w = 0w: 'a word)`, 105 rewrite_tac [aligned_def] 106 \\ Cases 107 >- rewrite_tac [align_0] 108 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def] 109 \\ eq_tac 110 \\ lrw [] 111 \\ res_tac 112 \\ Cases_on `i <= n` 113 \\ Cases_on `w ' i` 114 \\ fs [] 115 \\ decide_tac 116 ) 117 118val aligned_0 = Q.store_thm ("aligned_0", 119 `(!p. aligned p 0w) /\ (!w. aligned 0 w)`, 120 srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract] 121 ) 122 123val aligned_1_lsb = Q.store_thm ("aligned_1_lsb", 124 `!w. aligned 1 w = ~word_lsb w`, 125 srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract] 126 ) 127 128val aligned_ge_dim = Q.store_thm ("aligned_ge_dim", 129 `!p w:'a word. dimindex(:'a) <= p ==> (aligned p w = (w = 0w))`, 130 Cases \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract] 131 ) 132 133val aligned_bitwise_and = Q.store_thm("aligned_bitwise_and", 134 `!p w. aligned p (w: 'a word) = (w && n2w (2 ** p - 1) = 0w)`, 135 simp [aligned_def, align_bitwise_and] 136 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] 137 [wordsTheory.word_index, bitTheory.BIT_EXP_SUB1] 138 \\ eq_tac 139 \\ lrw [] 140 \\ res_tac 141 \\ Cases_on `i < SUC n` 142 \\ Cases_on `w ' i` 143 \\ fs [] 144 \\ decide_tac 145 ) 146 147val aligned_bit_count_upto = Q.store_thm ("aligned_bit_count_upto", 148 `!p w. 149 aligned p (w: 'a word) = (bit_count_upto (MIN (dimindex(:'a)) p) w = 0)`, 150 lrw [aligned_extract, wordsTheory.bit_count_upto_is_zero] 151 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [] 152 \\ Cases_on `p = 0` 153 \\ simp [] 154 \\ eq_tac 155 \\ lrw [] 156 \\ res_tac 157 >- decide_tac 158 \\ Cases_on `i < p` 159 \\ fs [] 160 \\ decide_tac 161 ) 162 163val aligned_add_sub = Q.store_thm("aligned_add_sub", 164 `!p a: 'a word b. 165 aligned p b ==> 166 (aligned p (a + b) = aligned p a) /\ 167 (aligned p (a - b) = aligned p a)`, 168 strip_tac 169 \\ Cases_on `dimindex(:'a) <= p` 170 >- simp [aligned_ge_dim] 171 \\ `p < dimindex(:'a)` by decide_tac 172 \\ Cases_on `p` 173 \\ simp [aligned_extract] 174 \\ Cases_on `SUC n = dimindex(:'a)` 175 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] [] 176 \\ simp [Once (GSYM wordsTheory.WORD_EXTRACT_OVER_ADD2), 177 Once (GSYM wordsTheory.WORD_EXTRACT_OVER_MUL2)] 178 \\ lrw [wordsTheory.WORD_EXTRACT_COMP_THM, arithmeticTheory.MIN_DEF] 179 \\ metis_tac [arithmeticTheory.SUC_SUB1] 180 ) 181 182val aligned_add_sub_cor = Q.store_thm("aligned_add_sub_cor", 183 `!p a: 'a word b. 184 aligned p a /\ aligned p b ==> aligned p (a + b) /\ aligned p (a - b)`, 185 metis_tac [aligned_add_sub] 186 ) 187 188val aligned_mul_shift_1 = Q.store_thm ("aligned_mul_shift_1", 189 `!p w: 'a word. aligned p (1w << p * w)`, 190 strip_tac 191 \\ Cases_on `dimindex(:'a) <= p` 192 >- simp [aligned_ge_dim] 193 \\ `p < dimindex(:'a)` by decide_tac 194 \\ Cases_on `p` 195 \\ srw_tac [ARITH_ss] 196 [aligned_extract, 197 Once (GSYM wordsTheory.WORD_EXTRACT_OVER_MUL2)] 198 \\ `(n >< 0) ((1w:'a word) << SUC n) = 0w: 'a word` 199 by lrw [wordsTheory.WORD_MUL_LSL, wordsTheory.word_extract_n2w, 200 arithmeticTheory.MIN_DEF, 201 bitTheory.BITS_SUM2 202 |> Q.SPECL [`n`, `0`, `1`, `0`] 203 |> SIMP_RULE (srw_ss()) []] 204 \\ simp [wordsTheory.WORD_EXTRACT_COMP_THM, arithmeticTheory.MIN_DEF] 205 ) 206 207val aligned_add_sub_prod = Q.store_thm("aligned_add_sub_prod", 208 `!p w: 'a word x. 209 (aligned p (w + (1w << p) * x) = aligned p w) /\ 210 (aligned p (w - (1w << p) * x) = aligned p w)`, 211 metis_tac [aligned_add_sub, aligned_mul_shift_1, wordsTheory.WORD_ADD_COMM] 212 ) 213 214val aligned_imp = Q.store_thm("aligned_imp", 215 `!p q w. p < q /\ aligned q w ==> aligned p w`, 216 srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract] 217 >- fs [] 218 \\ Cases_on `p` 219 \\ lrw [] 220 \\ res_tac 221 \\ simp [] 222 ) 223 224val align_add_aligned = Q.store_thm("align_add_aligned", 225 `!p a b : 'a word. 226 aligned p a /\ w2n b < 2 ** p ==> (align p (a + b) = a)`, 227 strip_tac 228 \\ Cases_on `dimindex(:'a) <= p` 229 >- (`w2n b < 2 ** p` 230 by metis_tac [wordsTheory.w2n_lt, wordsTheory.dimword_def, 231 bitTheory.TWOEXP_MONO2, arithmeticTheory.LESS_LESS_EQ_TRANS] 232 \\ simp [aligned_ge_dim, align_w2n, arithmeticTheory.LESS_DIV_EQ_ZERO]) 233 \\ fs [arithmeticTheory.NOT_LESS_EQUAL] 234 \\ rw [aligned_extract, align_sub, wordsTheory.WORD_EXTRACT_COMP_THM, 235 arithmeticTheory.MIN_DEF, 236 Once (GSYM wordsTheory.WORD_EXTRACT_OVER_ADD2), 237 wordsTheory.WORD_EXTRACT_ID 238 |> Q.SPECL [`w`, `p - 1`] 239 |> Q.DISCH `p <> 0n` 240 |> SIMP_RULE std_ss [DECIDE ``p <> 0n ==> (SUC (p - 1) = p)``] 241 ] 242 \\ fs [DECIDE ``(a < 1n) = (a = 0n)``, wordsTheory.w2n_eq_0] 243 ) 244 245(* ------------------------------------------------------------------------- 246 Theorems for standard alignment lengths of 1, 2 and 3 bits 247 ------------------------------------------------------------------------- *) 248 249fun f p = 250 let 251 val th1 = 252 aligned_add_sub_prod 253 |> Q.SPEC p 254 |> SIMP_RULE std_ss [fcpTheory.DIMINDEX_GE_1, wordsTheory.word_1_lsl] 255 val th2 = th1 |> Q.SPEC `0w` |> SIMP_RULE (srw_ss()) [aligned_0] 256 in 257 [th1, th2] 258 end 259 260val aligned_add_sub_123 = save_thm ("aligned_add_sub_123", 261 LIST_CONJ (List.concat (List.map f [`1`, `2`, `3`])) 262 ) 263 264local 265 val bit_lem = Q.prove( 266 `(!x. NUMERAL (BIT2 x) = 2 * (x + 1)) /\ 267 (!x. NUMERAL (BIT1 x) = 2 * x + 1) /\ 268 (!x. NUMERAL (BIT1 (BIT1 x)) = 4 * x + 3) /\ 269 (!x. NUMERAL (BIT1 (BIT2 x)) = 4 * (x + 1) + 1) /\ 270 (!x. NUMERAL (BIT2 (BIT1 x)) = 4 * (x + 1)) /\ 271 (!x. NUMERAL (BIT2 (BIT2 x)) = 4 * (x + 1) + 2) /\ 272 (!x. NUMERAL (BIT1 (BIT1 (BIT1 x))) = 8 * x + 7) /\ 273 (!x. NUMERAL (BIT1 (BIT1 (BIT2 x))) = 8 * (x + 1) + 3) /\ 274 (!x. NUMERAL (BIT1 (BIT2 (BIT1 x))) = 8 * (x + 1) + 1) /\ 275 (!x. NUMERAL (BIT1 (BIT2 (BIT2 x))) = 8 * (x + 1) + 5) /\ 276 (!x. NUMERAL (BIT2 (BIT1 (BIT1 x))) = 8 * (x + 1)) /\ 277 (!x. NUMERAL (BIT2 (BIT1 (BIT2 x))) = 8 * (x + 1) + 4) /\ 278 (!x. NUMERAL (BIT2 (BIT2 (BIT1 x))) = 8 * (x + 1) + 2) /\ 279 (!x. NUMERAL (BIT2 (BIT2 (BIT2 x))) = 8 * (x + 1) + 6)`, 280 REPEAT strip_tac 281 \\ CONV_TAC (Conv.LHS_CONV 282 (REWRITE_CONV [arithmeticTheory.BIT1, arithmeticTheory.BIT2, 283 arithmeticTheory.NUMERAL_DEF])) 284 \\ decide_tac 285 ) 286 val (_, _, dest_num, _) = HolKernel.syntax_fns1 "arithmetic" "NUMERAL" 287in 288 fun bit_lem_conv tm = 289 let 290 val x = dest_num (fst (wordsSyntax.dest_n2w tm)) 291 in 292 if List.null (Term.free_vars x) 293 then raise ERR "bit_lem_conv" "" 294 else Conv.RAND_CONV (ONCE_REWRITE_CONV [bit_lem]) tm 295 end 296end 297 298val aligned_numeric = Q.store_thm("aligned_numeric", 299 `(!x. aligned 3 (n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) /\ 300 (!x. aligned 2 (n2w (NUMERAL (BIT2 (BIT1 x))))) /\ 301 (!x. aligned 1 (n2w (NUMERAL (BIT2 x)))) /\ 302 (!x. aligned 3 (-n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) /\ 303 (!x. aligned 2 (-n2w (NUMERAL (BIT2 (BIT1 x))))) /\ 304 (!x. aligned 1 (-n2w (NUMERAL (BIT2 x)))) /\ 305 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) = 306 aligned 3 (y + 7w)) /\ 307 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) = 308 aligned 3 (y + 3w)) /\ 309 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) = 310 aligned 3 (y + 1w)) /\ 311 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) = 312 aligned 3 (y + 5w)) /\ 313 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) = 314 aligned 3 (y)) /\ 315 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) = 316 aligned 3 (y + 4w)) /\ 317 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) = 318 aligned 3 (y + 2w)) /\ 319 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) = 320 aligned 3 (y + 6w)) /\ 321 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) = 322 aligned 3 (y - 7w)) /\ 323 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) = 324 aligned 3 (y - 3w)) /\ 325 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) = 326 aligned 3 (y - 1w)) /\ 327 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) = 328 aligned 3 (y - 5w)) /\ 329 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) = 330 aligned 3 (y)) /\ 331 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) = 332 aligned 3 (y - 4w)) /\ 333 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) = 334 aligned 3 (y - 2w)) /\ 335 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) = 336 aligned 3 (y - 6w)) /\ 337 (!x y f. aligned 2 (y + n2w (NUMERAL (BIT1 (BIT1 (f x))))) = 338 aligned 2 (y + 3w)) /\ 339 (!x y. aligned 2 (y + n2w (NUMERAL (BIT1 (BIT2 x)))) = 340 aligned 2 (y + 1w)) /\ 341 (!x y. aligned 2 (y + n2w (NUMERAL (BIT2 (BIT1 x)))) = 342 aligned 2 (y)) /\ 343 (!x y. aligned 2 (y + n2w (NUMERAL (BIT2 (BIT2 x)))) = 344 aligned 2 (y + 2w)) /\ 345 (!x y f. aligned 2 (y - n2w (NUMERAL (BIT1 (BIT1 (f x))))) = 346 aligned 2 (y - 3w)) /\ 347 (!x y. aligned 2 (y - n2w (NUMERAL (BIT1 (BIT2 x)))) = 348 aligned 2 (y - 1w)) /\ 349 (!x y. aligned 2 (y - n2w (NUMERAL (BIT2 (BIT1 x)))) = 350 aligned 2 (y)) /\ 351 (!x y. aligned 2 (y - n2w (NUMERAL (BIT2 (BIT2 x)))) = 352 aligned 2 (y - 2w)) /\ 353 (!x y f. aligned 1 (y + n2w (NUMERAL (BIT1 (f x)))) = 354 aligned 1 (y + 1w)) /\ 355 (!x y f. aligned 1 (y - n2w (NUMERAL (BIT1 (f x)))) = 356 aligned 1 (y - 1w)) /\ 357 (!x y. aligned 1 (y + n2w (NUMERAL (BIT2 x))) = aligned 1 y) /\ 358 (!x y. aligned 1 (y - n2w (NUMERAL (BIT2 x))) = aligned 1 y)`, 359 REPEAT strip_tac 360 \\ CONV_TAC (DEPTH_CONV bit_lem_conv) 361 \\ rewrite_tac 362 [GSYM wordsTheory.word_mul_n2w, GSYM wordsTheory.word_add_n2w, 363 wordsLib.WORD_DECIDE ``a + (b * c + d) : 'a word = (a + d) + b * c``, 364 wordsLib.WORD_DECIDE ``a - (b * c + d) : 'a word = (a - d) - b * c``, 365 wordsTheory.WORD_NEG_LMUL, aligned_add_sub_123] 366 ) 367 368(* ------------------------------------------------------------------------- *) 369 370val () = export_theory () 371