alignmentScript.sml
1(* ========================================================================= *)
2(* FILE : alignmentScript.sml *)
3(* DESCRIPTION : Theory for address alignment. *)
4(* ========================================================================= *)
5Theory alignment
6Ancestors
7 words
8Libs
9 Q dep_rewrite wordsLib
10
11
12val ERR = mk_HOL_ERR "alignmentScript"
13
14(* -------------------------------------------------------------------------
15 Constant definitions
16 ------------------------------------------------------------------------- *)
17
18Definition align_def: align p (w: 'a word) = (dimindex (:'a) - 1 '' p) w
19End
20Definition aligned_def: aligned p w = (align p w = w)
21End
22
23Definition byte_align_def:
24 byte_align (w: 'a word) = align (LOG2 (dimindex(:'a) DIV 8)) w
25End
26
27Definition byte_aligned_def:
28 byte_aligned (w: 'a word) = aligned (LOG2 (dimindex(:'a) DIV 8)) w
29End
30
31(* -------------------------------------------------------------------------
32 Theorems
33 ------------------------------------------------------------------------- *)
34
35Theorem align_0:
36 !w. align 0 w = w
37Proof
38 lrw [wordsTheory.WORD_SLICE_BITS_THM, wordsTheory.WORD_ALL_BITS, align_def]
39QED
40
41Theorem align_align:
42 !p w. align p (align p w) = align p w
43Proof
44 srw_tac [wordsLib.WORD_BIT_EQ_ss, boolSimps.CONJ_ss] [align_def]
45QED
46
47Theorem aligned_align:
48 !p w. aligned p (align p w)
49Proof
50 rewrite_tac [aligned_def, align_align]
51QED
52
53Theorem align_aligned:
54 !p w. aligned p w ==> (align p w = w)
55Proof
56 rewrite_tac [aligned_def]
57QED
58
59Theorem align_bitwise_and:
60 !p w. align p w = w && UINT_MAXw << p
61Proof
62 srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def]
63 \\ decide_tac
64QED
65
66Theorem align_shift:
67 !p w. align p w = w >>> p << p
68Proof
69 srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def]
70 \\ Cases_on `p <= i`
71 \\ simp []
72QED
73
74Theorem align_w2n:
75 !p w. align p w = n2w (w2n w DIV 2 ** p * 2 ** p)
76Proof
77 strip_tac
78 \\ Cases
79 \\ lrw [align_shift, GSYM wordsTheory.n2w_DIV, wordsTheory.word_lsl_n2w,
80 wordsTheory.dimword_def]
81 \\ `dimindex(:'a) <= p` by decide_tac
82 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD
83 \\ simp [arithmeticTheory.EXP_ADD, arithmeticTheory.MOD_EQ_0]
84QED
85
86val ths = [GSYM wordsTheory.WORD_w2w_EXTRACT, wordsTheory.w2w_id]
87
88val lem =
89 wordsTheory.EXTRACT_JOIN_ADD
90 |> Thm.INST_TYPE [Type.beta |-> Type.alpha]
91 |> Q.SPECL [`dimindex(:'a) - 1`, `p - 1`, `p`, `0`, `p`, `w`]
92 |> Q.DISCH `0 < p`
93 |> SIMP_RULE (srw_ss()) (DECIDE ``0 < p ==> (p = p - 1 + 1)`` :: ths)
94 |> GSYM
95
96Theorem align_sub:
97 !p w. align p w = if p = 0 then w else w - (p - 1 >< 0) w
98Proof
99 rw_tac bool_ss [align_0]
100 \\ Cases_on `dimindex(:'a) <= p - 1`
101 >- (
102 `(p - 1 >< 0) w : 'a word = (dimindex (:'a) - 1 >< 0) w`
103 by simp [wordsTheory.WORD_EXTRACT_MIN_HIGH]
104 \\ rule_assum_tac (SIMP_RULE (srw_ss()) ths)
105 \\ asm_rewrite_tac []
106 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def]
107 )
108 \\ Cases_on `p = dimindex(:'a)`
109 >- srw_tac [wordsLib.WORD_BIT_EQ_ss] (align_def :: ths)
110 \\ `0 < p /\ p <= dimindex (:'a) - 1` by decide_tac
111 \\ imp_res_tac lem
112 \\ pop_assum (qspec_then `w` (CONV_TAC o Conv.PATH_CONV "rlr" o Lib.K))
113 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] [align_def]
114QED
115
116Theorem aligned_extract:
117 !p w. aligned p (w: 'a word) <=> (p = 0) \/ ((p - 1 >< 0) w = 0w: 'a word)
118Proof
119 rewrite_tac [aligned_def]
120 \\ Cases
121 >- rewrite_tac [align_0]
122 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def]
123 \\ eq_tac
124 \\ lrw []
125 \\ res_tac
126 \\ Cases_on `i <= n`
127 \\ Cases_on `w ' i`
128 \\ fs []
129 \\ decide_tac
130QED
131
132Theorem aligned_0:
133 (!p. aligned p 0w) /\ (!w. aligned 0 w)
134Proof
135 srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract]
136QED
137
138Theorem aligned_1_lsb:
139 !w. aligned 1 w = ~word_lsb w
140Proof
141 srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract]
142QED
143
144Theorem aligned_ge_dim:
145 !p w:'a word. dimindex(:'a) <= p ==> (aligned p w = (w = 0w))
146Proof
147 Cases \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract]
148QED
149
150Theorem aligned_bitwise_and:
151 !p w. aligned p (w: 'a word) = (w && n2w (2 ** p - 1) = 0w)
152Proof
153 simp [aligned_def, align_bitwise_and]
154 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss]
155 [wordsTheory.word_index, bitTheory.BIT_EXP_SUB1]
156 \\ eq_tac
157 \\ lrw []
158 \\ res_tac
159 \\ Cases_on `i < SUC n`
160 \\ Cases_on `w ' i`
161 \\ fs []
162 \\ decide_tac
163QED
164
165Theorem aligned_bit_count_upto:
166 !p w.
167 aligned p (w: 'a word) = (bit_count_upto (MIN (dimindex(:'a)) p) w = 0)
168Proof
169 lrw [aligned_extract, wordsTheory.bit_count_upto_is_zero]
170 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] []
171 \\ Cases_on `p = 0`
172 \\ simp []
173 \\ eq_tac
174 \\ lrw []
175 \\ res_tac
176 >- decide_tac
177 \\ Cases_on `i < p`
178 \\ fs []
179 \\ decide_tac
180QED
181
182Theorem aligned_add_sub:
183 !p a: 'a word b.
184 aligned p b ==>
185 (aligned p (a + b) = aligned p a) /\
186 (aligned p (a - b) = aligned p a)
187Proof
188 strip_tac
189 \\ Cases_on `dimindex(:'a) <= p`
190 >- simp [aligned_ge_dim]
191 \\ `p < dimindex(:'a)` by decide_tac
192 \\ Cases_on `p`
193 \\ simp [aligned_extract]
194 \\ Cases_on `SUC n = dimindex(:'a)`
195 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] []
196 \\ simp [Once (GSYM wordsTheory.WORD_EXTRACT_OVER_ADD2),
197 Once (GSYM wordsTheory.WORD_EXTRACT_OVER_MUL2)]
198 \\ lrw [wordsTheory.WORD_EXTRACT_COMP_THM, arithmeticTheory.MIN_DEF]
199 \\ metis_tac [arithmeticTheory.SUC_SUB1]
200QED
201
202Theorem aligned_add_sub_cor:
203 !p a: 'a word b.
204 aligned p a /\ aligned p b ==> aligned p (a + b) /\ aligned p (a - b)
205Proof
206 metis_tac [aligned_add_sub]
207QED
208
209Theorem aligned_mul_shift_1:
210 !p w: 'a word. aligned p (1w << p * w)
211Proof
212 strip_tac
213 \\ Cases_on `dimindex(:'a) <= p`
214 >- simp [aligned_ge_dim]
215 \\ `p < dimindex(:'a)` by decide_tac
216 \\ Cases_on `p`
217 \\ srw_tac [ARITH_ss]
218 [aligned_extract,
219 Once (GSYM wordsTheory.WORD_EXTRACT_OVER_MUL2)]
220 \\ `(n >< 0) ((1w:'a word) << SUC n) = 0w: 'a word`
221 by lrw [wordsTheory.WORD_MUL_LSL, wordsTheory.word_extract_n2w,
222 arithmeticTheory.MIN_DEF,
223 bitTheory.BITS_SUM2
224 |> Q.SPECL [`n`, `0`, `1`, `0`]
225 |> SIMP_RULE (srw_ss()) []]
226 \\ simp [wordsTheory.WORD_EXTRACT_COMP_THM, arithmeticTheory.MIN_DEF]
227QED
228
229Theorem aligned_add_sub_prod:
230 !p w: 'a word x.
231 (aligned p (w + (1w << p) * x) = aligned p w) /\
232 (aligned p (w - (1w << p) * x) = aligned p w)
233Proof
234 metis_tac [aligned_add_sub, aligned_mul_shift_1, wordsTheory.WORD_ADD_COMM]
235QED
236
237Theorem aligned_imp:
238 !p q w. p < q /\ aligned q w ==> aligned p w
239Proof
240 srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract]
241 >- fs []
242 \\ Cases_on `p`
243 \\ lrw []
244 \\ res_tac
245 \\ simp []
246QED
247
248Theorem align_add_aligned:
249 !p a b : 'a word.
250 aligned p a /\ w2n b < 2 ** p ==> (align p (a + b) = a)
251Proof
252 strip_tac
253 \\ Cases_on `dimindex(:'a) <= p`
254 >- (`w2n b < 2 ** p`
255 by metis_tac [wordsTheory.w2n_lt, wordsTheory.dimword_def,
256 bitTheory.TWOEXP_MONO2, arithmeticTheory.LESS_LESS_EQ_TRANS]
257 \\ simp [aligned_ge_dim, align_w2n, arithmeticTheory.LESS_DIV_EQ_ZERO])
258 \\ fs [arithmeticTheory.NOT_LESS_EQUAL]
259 \\ rw [aligned_extract, align_sub, wordsTheory.WORD_EXTRACT_COMP_THM,
260 arithmeticTheory.MIN_DEF,
261 Once (GSYM wordsTheory.WORD_EXTRACT_OVER_ADD2),
262 wordsTheory.WORD_EXTRACT_ID
263 |> Q.SPECL [`w`, `p - 1`]
264 |> Q.DISCH `p <> 0n`
265 |> SIMP_RULE std_ss [DECIDE ``p <> 0n ==> (SUC (p - 1) = p)``]
266 ]
267 \\ fs [DECIDE ``(a < 1n) = (a = 0n)``, wordsTheory.w2n_eq_0]
268QED
269
270Theorem lt_align_eq_0:
271 w2n a < 2 ** p ==> (align p a = 0w)
272Proof
273 Cases_on`a` \\ fs[]
274 \\ rw[align_w2n]
275 \\ Cases_on`p = 0` \\ fs[]
276 \\ `1 < 2 ** p` by fs[arithmeticTheory.ONE_LT_EXP]
277 \\ `n DIV 2 ** p = 0` by fs[arithmeticTheory.DIV_EQ_0]
278 \\ fs[]
279QED
280
281Theorem aligned_or:
282 aligned n (w || v) <=> aligned n w /\ aligned n v
283Proof
284 Cases_on `n = 0`
285 \\ srw_tac [WORD_BIT_EQ_ss] [aligned_extract]
286 \\ metis_tac []
287QED
288
289Theorem aligned_w2n:
290 aligned k w <=> (w2n (w:'a word) MOD 2 ** k = 0)
291Proof
292 Cases_on `w`
293 \\ fs [aligned_def,align_w2n]
294 \\ `0n < 2 ** k` by simp []
295 \\ drule arithmeticTheory.DIVISION
296 \\ disch_then (qspec_then `n` assume_tac)
297 \\ `(n DIV 2 ** k * 2 ** k) < dimword (:'a)` by decide_tac
298 \\ asm_simp_tac std_ss [] \\ decide_tac
299QED
300
301Theorem MOD_0_aligned:
302 !n p. (n MOD 2 ** p = 0) ==> aligned p (n2w n)
303Proof
304 fs [aligned_bitwise_and]
305 \\ once_rewrite_tac [wordsTheory.WORD_AND_COMM]
306 \\ fs [wordsTheory.WORD_AND_EXP_SUB1]
307QED
308
309Theorem aligned_lsl_leq:
310 k <= l ==> aligned k (w << l)
311Proof
312 fs [aligned_def,align_def]
313 \\ fs [fcpTheory.CART_EQ,wordsTheory.word_lsl_def,
314 wordsTheory.word_slice_def,fcpTheory.FCP_BETA]
315 \\ rw [] \\ eq_tac \\ fs []
316QED
317
318Theorem aligned_lsl[simp]:
319 aligned k (w << k)
320Proof match_mp_tac aligned_lsl_leq \\ fs[]
321QED
322
323Theorem align_align_MAX:
324 !k l w. align k (align l w) = align (MAX k l) w
325Proof
326 fs[align_def,fcpTheory.CART_EQ,wordsTheory.word_slice_def,fcpTheory.FCP_BETA]
327 \\ rw [] \\ eq_tac \\ fs []
328QED
329
330Theorem pow2_eq_0:
331 dimindex (:'a) <= k ==> (n2w (2 ** k) = 0w:'a word)
332Proof
333 fs [wordsTheory.dimword_def] \\ fs [arithmeticTheory.LESS_EQ_EXISTS]
334 \\ rw [] \\ fs [arithmeticTheory.EXP_ADD,arithmeticTheory.MOD_EQ_0]
335QED
336
337Theorem aligned_pow2:
338 aligned k (n2w (2 ** k))
339Proof
340 Cases_on `k < dimindex (:'a)`
341 \\ fs [arithmeticTheory.NOT_LESS,pow2_eq_0,aligned_0]
342 \\ `2 ** k < dimword (:'a)` by fs [wordsTheory.dimword_def]
343 \\ fs [aligned_def,align_w2n]
344QED
345
346Theorem word_msb_align:
347 p < dimindex(:'a) ==> (word_msb (align p w) = word_msb (w:'a word))
348Proof
349 rw[align_bitwise_and,wordsTheory.word_msb]
350 \\ rw[wordsTheory.word_bit_and]
351 \\ rw[wordsTheory.word_bit_lsl]
352 \\ rw[wordsTheory.word_bit_test,
353 arithmeticTheory.MOD_EQ_0_DIVISOR,
354 wordsTheory.dimword_def]
355QED
356
357Theorem align_ls:
358 align p n <=+ n
359Proof
360 simp[wordsTheory.WORD_LS]
361 \\ Cases_on`n`
362 \\ fs[align_w2n]
363 \\ qmatch_asmsub_rename_tac`n < _`
364 \\ DEP_REWRITE_TAC[arithmeticTheory.LESS_MOD]
365 \\ conj_asm2_tac >- fs[]
366 \\ DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV]
367 \\ simp[]
368QED
369
370Theorem align_lo:
371 ~aligned p n ==> align p n <+ n
372Proof
373 simp[wordsTheory.WORD_LO]
374 \\ Cases_on`n`
375 \\ fs[align_w2n, aligned_def]
376 \\ strip_tac
377 \\ qmatch_goalsub_abbrev_tac`a < b`
378 \\ `a <= b` suffices_by fs[]
379 \\ qmatch_asmsub_rename_tac`n < _`
380 \\ simp[Abbr`a`]
381 \\ DEP_REWRITE_TAC[arithmeticTheory.LESS_MOD]
382 \\ conj_asm2_tac >- fs[]
383 \\ DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV]
384 \\ simp[]
385QED
386
387Theorem aligned_between:
388 ~aligned p n /\ aligned p m /\ align p n <+ m ==> n <+ m
389Proof
390 rw[wordsTheory.WORD_LO]
391 \\ fs[align_w2n, aligned_def]
392 \\ Cases_on`n` \\ Cases_on`m` \\ fs[]
393 \\ CCONTR_TAC \\ fs[arithmeticTheory.NOT_LESS]
394 \\ qmatch_asmsub_abbrev_tac`n DIV d * d`
395 \\ `n DIV d * d <= n` by (
396 DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV] \\ fs[Abbr`d`] )
397 \\ fs[]
398 \\ qmatch_asmsub_rename_tac`(d * (m DIV d)) MOD _`
399 \\ `m DIV d * d <= m` by (
400 DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV] \\ fs[Abbr`d`] )
401 \\ fs[]
402 \\ `d * (n DIV d) <= m` by metis_tac[]
403 \\ pop_assum mp_tac
404 \\ simp_tac pure_ss [Once arithmeticTheory.MULT_COMM]
405 \\ DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV]
406 \\ conj_tac >- simp[Abbr`d`]
407 \\ simp[arithmeticTheory.NOT_LESS_EQUAL]
408 \\ `d * (m DIV d) < d * (n DIV d)` suffices_by fs[]
409 \\ metis_tac[]
410QED
411
412local
413 val aligned_add_mult_lemma = Q.prove(
414 `aligned k (w + n2w (2 ** k)) = aligned k w`,
415 fs [aligned_add_sub,aligned_pow2]) |> GEN_ALL
416 val aligned_add_mult_any = Q.prove(
417 `!n w. aligned k (w + n2w (n * 2 ** k)) = aligned k w`,
418 Induct \\ fs [arithmeticTheory.MULT_CLAUSES,
419 GSYM wordsTheory.word_add_n2w]
420 \\ rw []
421 \\ pop_assum (qspec_then `w + n2w (2 ** k)` mp_tac)
422 \\ fs [aligned_add_mult_lemma]) |> GEN_ALL
423in
424Theorem aligned_add_pow[simp] =
425 CONJ aligned_add_mult_lemma aligned_add_mult_any;
426end
427
428Theorem align_add_aligned_gen:
429 !a. aligned p a ==> (align p (a + b) = a + align p b)
430Proof
431 completeInduct_on`w2n b`
432 \\ rw[]
433 \\ Cases_on`w2n b < 2 ** p`
434 >- (
435 simp[align_add_aligned]
436 \\ `align p b = 0w` by simp[lt_align_eq_0]
437 \\ simp[] )
438 \\ fs[arithmeticTheory.NOT_LESS]
439 \\ Cases_on`w2n b = 2 ** p`
440 >- (
441 `aligned p b` by(
442 simp[aligned_def,align_w2n]
443 \\ metis_tac[wordsTheory.n2w_w2n] )
444 \\ `aligned p (a + b)` by metis_tac[aligned_add_sub_cor]
445 \\ fs[aligned_def])
446 \\ fs[arithmeticTheory.LESS_EQ_EXISTS]
447 \\ qmatch_asmsub_rename_tac`w2n b = z + _`
448 \\ first_x_assum(qspec_then`z`mp_tac)
449 \\ impl_keep_tac >- fs[]
450 \\ `z < dimword(:'a)` by metis_tac[wordsTheory.w2n_lt, arithmeticTheory.LESS_TRANS]
451 \\ disch_then(qspec_then`n2w z`mp_tac)
452 \\ impl_tac >- simp[]
453 \\ strip_tac
454 \\ first_assum(qspec_then`a + n2w (2 ** p)`mp_tac)
455 \\ impl_tac >- fs[]
456 \\ rewrite_tac[wordsTheory.word_add_n2w, GSYM wordsTheory.WORD_ADD_ASSOC]
457 \\ Cases_on`b` \\ fs[GSYM wordsTheory.word_add_n2w]
458 \\ strip_tac
459 \\ first_x_assum(qspec_then`n2w (2**p)`mp_tac)
460 \\ impl_tac >- fs[aligned_w2n]
461 \\ simp[]
462QED
463
464Theorem byte_align_aligned:
465 byte_aligned x <=> (byte_align x = x)
466Proof EVAL_TAC
467QED
468
469Theorem byte_aligned_add:
470 byte_aligned x /\ byte_aligned y ==> byte_aligned (x+y)
471Proof
472 rw[byte_aligned_def]
473 \\ metis_tac[aligned_add_sub_cor]
474QED
475
476(* -------------------------------------------------------------------------
477 Theorems for standard alignment lengths of 1, 2 and 3 bits
478 ------------------------------------------------------------------------- *)
479
480fun f p =
481 let
482 val th1 =
483 aligned_add_sub_prod
484 |> Q.SPEC p
485 |> SIMP_RULE std_ss [fcpTheory.DIMINDEX_GE_1, wordsTheory.word_1_lsl]
486 val th2 = th1 |> Q.SPEC `0w` |> SIMP_RULE (srw_ss()) [aligned_0]
487 in
488 [th1, th2]
489 end
490
491Theorem aligned_add_sub_123 =
492 LIST_CONJ (List.concat (List.map f [`1`, `2`, `3`]))
493
494
495local
496 val bit_lem = Q.prove(
497 `(!x. NUMERAL (BIT2 x) = 2 * (x + 1)) /\
498 (!x. NUMERAL (BIT1 x) = 2 * x + 1) /\
499 (!x. NUMERAL (BIT1 (BIT1 x)) = 4 * x + 3) /\
500 (!x. NUMERAL (BIT1 (BIT2 x)) = 4 * (x + 1) + 1) /\
501 (!x. NUMERAL (BIT2 (BIT1 x)) = 4 * (x + 1)) /\
502 (!x. NUMERAL (BIT2 (BIT2 x)) = 4 * (x + 1) + 2) /\
503 (!x. NUMERAL (BIT1 (BIT1 (BIT1 x))) = 8 * x + 7) /\
504 (!x. NUMERAL (BIT1 (BIT1 (BIT2 x))) = 8 * (x + 1) + 3) /\
505 (!x. NUMERAL (BIT1 (BIT2 (BIT1 x))) = 8 * (x + 1) + 1) /\
506 (!x. NUMERAL (BIT1 (BIT2 (BIT2 x))) = 8 * (x + 1) + 5) /\
507 (!x. NUMERAL (BIT2 (BIT1 (BIT1 x))) = 8 * (x + 1)) /\
508 (!x. NUMERAL (BIT2 (BIT1 (BIT2 x))) = 8 * (x + 1) + 4) /\
509 (!x. NUMERAL (BIT2 (BIT2 (BIT1 x))) = 8 * (x + 1) + 2) /\
510 (!x. NUMERAL (BIT2 (BIT2 (BIT2 x))) = 8 * (x + 1) + 6)`,
511 REPEAT strip_tac
512 \\ CONV_TAC (Conv.LHS_CONV
513 (REWRITE_CONV [arithmeticTheory.BIT1, arithmeticTheory.BIT2,
514 arithmeticTheory.NUMERAL_DEF]))
515 \\ decide_tac
516 )
517 val (_, _, dest_num, _) = HolKernel.syntax_fns1 "arithmetic" "NUMERAL"
518in
519 fun bit_lem_conv tm =
520 let
521 val x = dest_num (fst (wordsSyntax.dest_n2w tm))
522 in
523 if List.null (Term.free_vars x)
524 then raise ERR "bit_lem_conv" ""
525 else Conv.RAND_CONV (ONCE_REWRITE_CONV [bit_lem]) tm
526 end
527end
528
529Theorem aligned_numeric:
530 (!x. aligned 3 (n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) /\
531 (!x. aligned 2 (n2w (NUMERAL (BIT2 (BIT1 x))))) /\
532 (!x. aligned 1 (n2w (NUMERAL (BIT2 x)))) /\
533 (!x. aligned 3 (-n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) /\
534 (!x. aligned 2 (-n2w (NUMERAL (BIT2 (BIT1 x))))) /\
535 (!x. aligned 1 (-n2w (NUMERAL (BIT2 x)))) /\
536 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) =
537 aligned 3 (y + 7w)) /\
538 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) =
539 aligned 3 (y + 3w)) /\
540 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) =
541 aligned 3 (y + 1w)) /\
542 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) =
543 aligned 3 (y + 5w)) /\
544 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) =
545 aligned 3 (y)) /\
546 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) =
547 aligned 3 (y + 4w)) /\
548 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) =
549 aligned 3 (y + 2w)) /\
550 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) =
551 aligned 3 (y + 6w)) /\
552 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) =
553 aligned 3 (y - 7w)) /\
554 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) =
555 aligned 3 (y - 3w)) /\
556 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) =
557 aligned 3 (y - 1w)) /\
558 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) =
559 aligned 3 (y - 5w)) /\
560 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) =
561 aligned 3 (y)) /\
562 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) =
563 aligned 3 (y - 4w)) /\
564 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) =
565 aligned 3 (y - 2w)) /\
566 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) =
567 aligned 3 (y - 6w)) /\
568 (!x y f. aligned 2 (y + n2w (NUMERAL (BIT1 (BIT1 (f x))))) =
569 aligned 2 (y + 3w)) /\
570 (!x y. aligned 2 (y + n2w (NUMERAL (BIT1 (BIT2 x)))) =
571 aligned 2 (y + 1w)) /\
572 (!x y. aligned 2 (y + n2w (NUMERAL (BIT2 (BIT1 x)))) =
573 aligned 2 (y)) /\
574 (!x y. aligned 2 (y + n2w (NUMERAL (BIT2 (BIT2 x)))) =
575 aligned 2 (y + 2w)) /\
576 (!x y f. aligned 2 (y - n2w (NUMERAL (BIT1 (BIT1 (f x))))) =
577 aligned 2 (y - 3w)) /\
578 (!x y. aligned 2 (y - n2w (NUMERAL (BIT1 (BIT2 x)))) =
579 aligned 2 (y - 1w)) /\
580 (!x y. aligned 2 (y - n2w (NUMERAL (BIT2 (BIT1 x)))) =
581 aligned 2 (y)) /\
582 (!x y. aligned 2 (y - n2w (NUMERAL (BIT2 (BIT2 x)))) =
583 aligned 2 (y - 2w)) /\
584 (!x y f. aligned 1 (y + n2w (NUMERAL (BIT1 (f x)))) =
585 aligned 1 (y + 1w)) /\
586 (!x y f. aligned 1 (y - n2w (NUMERAL (BIT1 (f x)))) =
587 aligned 1 (y - 1w)) /\
588 (!x y. aligned 1 (y + n2w (NUMERAL (BIT2 x))) = aligned 1 y) /\
589 (!x y. aligned 1 (y - n2w (NUMERAL (BIT2 x))) = aligned 1 y)
590Proof
591 REPEAT strip_tac
592 \\ CONV_TAC (DEPTH_CONV bit_lem_conv)
593 \\ rewrite_tac
594 [GSYM wordsTheory.word_mul_n2w, GSYM wordsTheory.word_add_n2w,
595 wordsLib.WORD_DECIDE ``a + (b * c + d) : 'a word = (a + d) + b * c``,
596 wordsLib.WORD_DECIDE ``a - (b * c + d) : 'a word = (a - d) - b * c``,
597 wordsTheory.WORD_NEG_LMUL, aligned_add_sub_123]
598QED
599
600(* ------------------------------------------------------------------------- *)