byteScript.sml
1(*
2 A theory about byte-level manipulation of machine words.
3*)
4Theory byte
5Ancestors
6 arithmetic list[qualified] words rich_list
7Libs
8 dep_rewrite
9
10
11val _ = temp_tight_equality();
12
13(* Get and set bytes in a word *)
14
15Definition byte_index_def:
16 byte_index (a:'a word) is_bigendian =
17 let d = dimindex (:'a) DIV 8 in
18 if is_bigendian then 8 * ((d - 1) - w2n a MOD d) else 8 * (w2n a MOD d)
19End
20
21Definition get_byte_def:
22 get_byte (a:'a word) (w:'a word) is_bigendian =
23 (w2w (w >>> byte_index a is_bigendian)):word8
24End
25
26Definition word_slice_alt_def:
27 (word_slice_alt h l (w:'a word) :'a word) = FCP i. l <= i /\ i < h /\ w ' i
28End
29
30Definition set_byte_def[nocompute]:
31 set_byte (a:'a word) (b:word8) (w:'a word) is_bigendian =
32 let i = byte_index a is_bigendian in
33 (word_slice_alt (dimindex (:'a)) (i + 8) w
34 || w2w b << i
35 || word_slice_alt i 0 w)
36End
37
38Theorem set_byte_32[compute]:
39 set_byte a b (w:word32) be =
40 let i = byte_index a be in
41 if i = 0 then w2w b || (w && 0xFFFFFF00w) else
42 if i = 8 then w2w b << 8 || (w && 0xFFFF00FFw) else
43 if i = 16 then w2w b << 16 || (w && 0xFF00FFFFw) else
44 w2w b << 24 || (w && 0x00FFFFFFw)
45Proof
46 fs [set_byte_def]
47 \\ qsuff_tac ‘byte_index a be = 0 \/
48 byte_index a be = 8 \/
49 byte_index a be = 16 \/
50 byte_index a be = 24’
51 THEN1 (rw [] \\ fs [word_slice_alt_def] \\ blastLib.BBLAST_TAC)
52 \\ fs [byte_index_def]
53 \\ ‘w2n a MOD 4 < 4’ by fs [MOD_LESS] \\ rw []
54QED
55
56Theorem set_byte_64[compute]:
57 set_byte a b (w:word64) be =
58 let i = byte_index a be in
59 if i = 0 then w2w b || (w && 0xFFFFFFFFFFFFFF00w) else
60 if i = 8 then w2w b << 8 || (w && 0xFFFFFFFFFFFF00FFw) else
61 if i = 16 then w2w b << 16 || (w && 0xFFFFFFFFFF00FFFFw) else
62 if i = 24 then w2w b << 24 || (w && 0xFFFFFFFF00FFFFFFw) else
63 if i = 32 then w2w b << 32 || (w && 0xFFFFFF00FFFFFFFFw) else
64 if i = 40 then w2w b << 40 || (w && 0xFFFF00FFFFFFFFFFw) else
65 if i = 48 then w2w b << 48 || (w && 0xFF00FFFFFFFFFFFFw) else
66 w2w b << 56 || (w && 0x00FFFFFFFFFFFFFFw)
67Proof
68 fs [set_byte_def]
69 \\ qsuff_tac ‘byte_index a be = 0 \/
70 byte_index a be = 8 \/
71 byte_index a be = 16 \/
72 byte_index a be = 24 \/
73 byte_index a be = 32 \/
74 byte_index a be = 40 \/
75 byte_index a be = 48 \/
76 byte_index a be = 56’
77 THEN1 (rw [] \\ fs [word_slice_alt_def] \\ blastLib.BBLAST_TAC)
78 \\ fs [byte_index_def]
79 \\ ‘w2n a MOD 8 < 8’ by fs [MOD_LESS] \\ rw []
80QED
81
82Theorem set_byte_bit_field_insert:
83 set_byte a b w be = bit_field_insert (byte_index a be + 7) (byte_index a be) b w
84Proof
85 asm_simp_tac (boss_ss () ++ fcpLib.FCP_ss) [set_byte_def, bit_field_insert_def, word_modify_def, w2w, word_lsl_def, word_slice_alt_def, word_or_def]
86 >> rpt strip_tac
87 >> IF_CASES_TAC
88 >> fs []
89QED
90
91Theorem set_byte_change_a:
92 w2n (a:'a word) MOD (dimindex(:'a) DIV 8) = w2n a' MOD (dimindex(:'a) DIV 8)
93 ==>
94 set_byte a b w be = set_byte a' b w be
95Proof
96 rw[set_byte_def,byte_index_def]
97QED
98
99Theorem set_byte_eq_or:
100 (!j. j < 8n ==> ~ w ' (byte_index ix bige + j)) ==>
101 set_byte ix b w bige = (w || (w2w b << byte_index ix bige))
102Proof
103 simp [set_byte_bit_field_insert, wordsTheory.bit_field_insert_def,
104 wordsTheory.word_modify_def, wordsTheory.word_or_def, wordsTheory.word_lsl_def]
105 \\ simp_tac (std_ss ++ fcpLib.FCP_ss) [wordsTheory.w2w]
106 \\ rw []
107 \\ iff_tac \\ CCONTR_TAC \\ gs [wordsTheory.w2w]
108 \\ first_x_assum (qspec_then `i - byte_index ix bige` assume_tac)
109 \\ gs []
110QED
111
112Theorem lt_or_gt[local]:
113 (a: num) <> b ==> a < b \/ b < a
114Proof
115 simp []
116QED
117
118Theorem num_bytes_nonzero[local]:
119 8 <= dimindex (:'a) <=> 0 < dimindex (:'a) DIV 8
120Proof
121 iff_tac
122 >- (rpt strip_tac
123 >> `8 DIV 8 <= dimindex (:'a) DIV 8` by simp [DIV_LE_MONOTONE]
124 >> fs [])
125 >- (rpt strip_tac
126 >> irule LE_TRANS
127 >> qexists `dimindex (:'a) DIV 8 * 8`
128 >> simp [dividesTheory.DIV_MULT_LE])
129QED
130
131Theorem byte_index_lt_or_gt:
132 w2n (n: 'a word) MOD (dimindex (:'a) DIV 8) <> w2n (m: 'a word) MOD (dimindex (:'a) DIV 8)
133 /\ 8 <= dimindex (:'a)
134 ==> byte_index n be + 8 <= byte_index m be \/ byte_index m be + 8 <= byte_index n be
135Proof
136 rpt strip_tac
137 >> drule_then strip_assume_tac lt_or_gt
138 >> Cases_on `be`
139 >> fs [byte_index_def, num_bytes_nonzero]
140 >> qabbrev_tac `bytes = dimindex (:'a) DIV 8`
141 >> `w2n m MOD bytes < bytes` by simp []
142 >> `w2n n MOD bytes < bytes` by simp []
143 >> simp []
144QED
145
146Theorem set_byte_transpose:
147 w2n n MOD (dimindex (:'a) DIV 8) <> w2n m MOD (dimindex (:'a) DIV 8)
148 /\ 8 <= dimindex (:'a)
149 ==> set_byte n x (set_byte m y (w: 'a word) be) be = set_byte m y (set_byte n x w be) be
150Proof
151 rpt strip_tac
152 >> simp [set_byte_bit_field_insert]
153 >> irule bit_field_insert_transpose
154 >> drule_all_then (qspec_then `be` assume_tac) byte_index_lt_or_gt
155 >> simp []
156QED
157
158Theorem get_byte_set_byte:
159 8 <= dimindex(:'a) ==>
160 (get_byte a (set_byte (a:'a word) b w be) be = b)
161Proof
162 fs [get_byte_def,set_byte_def]
163 \\ fs [fcpTheory.CART_EQ,w2w] \\ rpt strip_tac
164 \\ `i < dimindex (:'a)` by fs[dimindex_8]
165 \\ fs [word_or_def,fcpTheory.FCP_BETA,word_lsr_def,word_lsl_def]
166 \\ `i + byte_index a be < dimindex (:'a)` by (
167 fs [byte_index_def,LET_DEF]
168 \\ qmatch_goalsub_abbrev_tac`_ MOD dd`
169 \\ match_mp_tac LESS_EQ_LESS_TRANS
170 \\ qexists_tac`i + 8 * (dd-1)`
171 \\ `0 < dd` by fs[Abbr`dd`, X_LT_DIV, NOT_LESS, dimindex_8]
172 \\ conj_tac
173 >- (
174 rw[]
175 \\ `w2n a MOD dd < dd` by (match_mp_tac MOD_LESS \\ decide_tac)
176 \\ simp[] )
177 \\ match_mp_tac LESS_LESS_EQ_TRANS
178 \\ qexists_tac`8 * dd`
179 \\ simp[LEFT_SUB_DISTRIB]
180 \\ fs[dimindex_8]
181 \\ qspec_then`8`mp_tac DIVISION
182 \\ impl_tac >- simp[]
183 \\ disch_then(qspec_then`dimindex(:'a)`(SUBST1_TAC o CONJUNCT1))
184 \\ simp[] )
185 \\ fs [word_or_def,fcpTheory.FCP_BETA,word_lsr_def,word_lsl_def,
186 word_slice_alt_def,w2w] \\ rfs []
187 \\ `~(i + byte_index a be < byte_index a be)` by decide_tac
188 \\ fs[dimindex_8]
189QED
190
191(* Convert between lists of bytes and words *)
192
193Definition bytes_in_word_def:
194 bytes_in_word = n2w (dimindex (:'a) DIV 8):'a word
195End
196
197Definition word_of_bytes_def:
198 (word_of_bytes be a [] = 0w) /\
199 (word_of_bytes be a (b::bs) =
200 set_byte a b (word_of_bytes be (a+1w) bs) be)
201End
202
203Theorem word_of_bytes_SNOC:
204 LENGTH bs < dimindex (:'a) DIV 8 /\ w2n (n: 'a word) + LENGTH bs < dimword (:'a) ==>
205 word_of_bytes be n (SNOC b bs) = set_byte (n + n2w (LENGTH bs)) b (word_of_bytes be n bs) be
206Proof
207 qid_spec_tac `n`
208 >> Induct_on `bs`
209 >- simp [word_of_bytes_def]
210 >- (rpt strip_tac
211 >> last_x_assum (qspec_then `n + 1w` assume_tac)
212 >> rfs [w2n_add_2, word_of_bytes_def, ADD1, GSYM word_add_n2w]
213 >> irule set_byte_transpose
214 >> qspecl_then [`dimindex (:'a) DIV 8`, `LENGTH bs + 1`, `0`, `w2n n`] assume_tac ADD_MOD
215 >> rfs [w2n_add_2, num_bytes_nonzero])
216QED
217
218Theorem word_of_bytes_eq_or_helper[local]:
219 !bs n w. (!j. j < LENGTH bs ==> ~ (f (EL j bs) (j + n) ' ix)) /\
220 ~ ((w : 'a word) ' ix) /\ ix < dimindex (: 'a) ==>
221 ~ FOLDRi (\x b w. w || (f b (n + x))) w bs ' ix
222Proof
223 Induct
224 \\ simp []
225 \\ rw []
226 \\ ONCE_REWRITE_TAC [wordsTheory.word_or_def]
227 \\ simp [fcpTheory.FCP_BETA]
228 \\ conj_tac
229 >- (
230 first_x_assum (qspec_then `0n` mp_tac)
231 \\ simp []
232 )
233 \\ simp [combinTheory.o_DEF]
234 \\ last_x_assum (qspec_then `SUC n` mp_tac)
235 \\ simp [arithmeticTheory.ADD1]
236 \\ disch_then irule
237 \\ rw []
238 \\ first_x_assum (qspec_then `SUC j` mp_tac)
239 \\ simp [arithmeticTheory.ADD1]
240QED
241
242Theorem word_of_bytes_eq_or_helper2[local] =
243 word_of_bytes_eq_or_helper |> Q.SPECL [`bs`, `0n`]
244 |> SIMP_RULE std_ss []
245
246Theorem w2n_increment[local]:
247 w2n (x + 1w) = (if x = UINT_MAXw then 0n else w2n x + 1)
248Proof
249 qspec_then `x` mp_tac wordsTheory.w2n_plus1
250 \\ rw []
251QED
252
253Theorem word_of_bytes_eq_or:
254 !bs ix.
255 (w2n ix + LENGTH bs) * 8 <= dimindex (: 'a) /\
256 EVERYi (\i _. ix + n2w i <> -1w) bs ==>
257 word_of_bytes F ix bs =
258 FOLDRi (\i b w. (w2w b << ((w2n ix + i) * 8)) || w) (0w : 'a word) bs
259Proof
260 Induct
261 \\ simp [word_of_bytes_def]
262 \\ rw []
263 \\ first_x_assum (qspec_then `ix + 1w` mp_tac)
264 \\ fs [listTheory.EVERYi_def, w2n_increment]
265 \\ fs [combinTheory.o_DEF, wordsTheory.n2w_SUC]
266 \\ rw []
267 \\ dep_rewrite.DEP_ONCE_REWRITE_TAC [set_byte_eq_or]
268 \\ simp [byte_index_def]
269 \\ simp [arithmeticTheory.LESS_MOD, arithmeticTheory.X_LT_DIV]
270 \\ rw [arithmeticTheory.ADD1]
271 \\ ho_match_mp_tac word_of_bytes_eq_or_helper2
272 \\ rw [wordsTheory.word_0]
273 \\ simp [wordsTheory.word_lsl_def, wordsTheory.w2w, fcpTheory.FCP_BETA]
274QED
275
276Definition words_of_bytes_def:
277 (words_of_bytes be [] = ([]:'a word list)) /\
278 (words_of_bytes be bytes =
279 let xs = TAKE (MAX 1 (w2n (bytes_in_word:'a word))) bytes in
280 let ys = DROP (MAX 1 (w2n (bytes_in_word:'a word))) bytes in
281 word_of_bytes be 0w xs :: words_of_bytes be ys)
282Termination
283 WF_REL_TAC `measure (LENGTH o SND)` \\ fs []
284End
285
286Theorem LENGTH_words_of_bytes:
287 8 <= dimindex(:'a) ==>
288 !be ls.
289 (LENGTH (words_of_bytes be ls : 'a word list) =
290 LENGTH ls DIV (w2n (bytes_in_word : 'a word)) +
291 MIN 1 (LENGTH ls MOD (w2n (bytes_in_word : 'a word))))
292Proof
293 strip_tac
294 \\ recInduct words_of_bytes_ind
295 \\ `1 <= w2n bytes_in_word`
296 by (
297 simp[bytes_in_word_def,dimword_def]
298 \\ DEP_REWRITE_TAC[LESS_MOD]
299 \\ rw[DIV_LT_X, X_LT_DIV, X_LE_DIV]
300 \\ match_mp_tac LESS_TRANS
301 \\ qexists_tac`2 ** dimindex(:'a)`
302 \\ simp[X_LT_EXP_X] )
303 \\ simp[words_of_bytes_def]
304 \\ rw[ADD1]
305 \\ `MAX 1 (w2n (bytes_in_word:'a word)) = w2n (bytes_in_word:'a word)`
306 by rw[MAX_DEF]
307 \\ fs[]
308 \\ qmatch_goalsub_abbrev_tac`(m - n) DIV _`
309 \\ Cases_on`m < n` \\ fs[]
310 >- (
311 `m - n = 0` by fs[]
312 \\ simp[]
313 \\ simp[LESS_DIV_EQ_ZERO]
314 \\ rw[MIN_DEF]
315 \\ fs[Abbr`m`] )
316 \\ simp[SUB_MOD]
317 \\ qspec_then`1`(mp_tac o GEN_ALL)(Q.GEN`q`DIV_SUB) \\ fs[]
318 \\ disch_then kall_tac
319 \\ Cases_on`m MOD n = 0` \\ fs[]
320 >- (
321 DEP_REWRITE_TAC[SUB_ADD]
322 \\ fs[X_LE_DIV] )
323 \\ `MIN 1 (m MOD n) = 1` by simp[MIN_DEF]
324 \\ fs[]
325 \\ `m DIV n - 1 + 1 = m DIV n` suffices_by fs[]
326 \\ DEP_REWRITE_TAC[SUB_ADD]
327 \\ fs[X_LE_DIV]
328QED
329
330Theorem words_of_bytes_append:
331 0 < w2n(bytes_in_word:'a word) ==>
332 !l1 l2.
333 (LENGTH l1 MOD w2n (bytes_in_word:'a word) = 0) ==>
334 (words_of_bytes be (l1 ++ l2) : 'a word list =
335 words_of_bytes be l1 ++ words_of_bytes be l2)
336Proof
337 strip_tac
338 \\ gen_tac
339 \\ completeInduct_on`LENGTH l1`
340 \\ rw[]
341 \\ Cases_on`l1` \\ fs[]
342 >- EVAL_TAC
343 \\ rw[words_of_bytes_def]
344 \\ fs[PULL_FORALL]
345 >- (
346 simp[TAKE_APPEND]
347 \\ qmatch_goalsub_abbrev_tac`_ ++ xx`
348 \\ `xx = []` suffices_by rw[]
349 \\ simp[Abbr`xx`]
350 \\ fs[ADD1]
351 \\ rfs[MOD_EQ_0_DIVISOR]
352 \\ Cases_on`d` \\ fs[] )
353 \\ simp[DROP_APPEND]
354 \\ qmatch_goalsub_abbrev_tac`_ ++ DROP n l2`
355 \\ `n = 0`
356 by (
357 simp[Abbr`n`]
358 \\ rfs[MOD_EQ_0_DIVISOR]
359 \\ Cases_on`d` \\ fs[ADD1] )
360 \\ simp[]
361 \\ first_x_assum irule
362 \\ simp[]
363 \\ rfs[MOD_EQ_0_DIVISOR, ADD1]
364 \\ Cases_on`d` \\ fs[MULT]
365 \\ simp[MAX_DEF]
366 \\ IF_CASES_TAC \\ fs[NOT_LESS]
367 >- metis_tac[]
368 \\ Cases_on`w2n (bytes_in_word:'a word)` \\ fs[] \\ rw[]
369 \\ Cases_on`n''` \\ fs[] \\ metis_tac []
370QED
371
372Theorem words_of_bytes_append_word:
373 0 < LENGTH l1 /\ (LENGTH l1 = w2n (bytes_in_word:'a word)) ==>
374 (words_of_bytes be (l1 ++ l2) = word_of_bytes be (0w:'a word) l1 :: words_of_bytes be l2)
375Proof
376 rw[]
377 \\ Cases_on`l1` \\ rw[words_of_bytes_def] \\ fs[]
378 \\ fs[MAX_DEF]
379 \\ qabbrev_tac ‘k = w2n (bytes_in_word:'a word)’
380 \\ fs[ADD1]
381 \\ rw[TAKE_APPEND,DROP_APPEND,DROP_LENGTH_NIL] \\ fs[]
382QED
383
384Definition bytes_to_word_def:
385 bytes_to_word k a bs w be =
386 if k = 0:num then w else
387 case bs of
388 | [] => w
389 | (b::bs) => set_byte a b (bytes_to_word (k-1) (a+1w) bs w be) be
390End
391
392Theorem bytes_to_word_eq:
393 bytes_to_word 0 a bs w be = w /\
394 bytes_to_word k a [] w be = w /\
395 bytes_to_word (SUC k) a (b::bs) w be =
396 set_byte a b (bytes_to_word k (a+1w) bs w be) be
397Proof
398 rw [] \\ simp [Once bytes_to_word_def]
399QED
400
401Theorem word_of_bytes_bytes_to_word:
402 !be a bs k.
403 LENGTH bs <= k ==>
404 (word_of_bytes be a bs = bytes_to_word k a bs 0w be)
405Proof
406 Induct_on`bs`
407 >- (
408 EVAL_TAC
409 \\ Cases_on`k`
410 \\ EVAL_TAC
411 \\ rw[] )
412 \\ rw[word_of_bytes_def]
413 \\ Cases_on`k` \\ fs[]
414 \\ rw[Once bytes_to_word_def]
415 \\ AP_THM_TAC
416 \\ AP_TERM_TAC
417 \\ first_x_assum match_mp_tac
418 \\ fs[]
419QED
420
421Theorem bytes_to_word_same:
422 !bw k b1 w be b2.
423 (!n. n < bw ==> n < LENGTH b1 /\ n < LENGTH b2 /\ EL n b1 = EL n b2)
424 ==>
425 (bytes_to_word bw k b1 w be = bytes_to_word bw k b2 w be)
426Proof
427 ho_match_mp_tac bytes_to_word_ind \\ rw []
428 \\ once_rewrite_tac [bytes_to_word_def] \\ rw []
429 \\ Cases_on`b1` \\ fs[]
430 >- (first_x_assum(qspec_then`0`mp_tac) \\ simp[])
431 \\ Cases_on`b2` \\ fs[]
432 >- (first_x_assum(qspec_then`0`mp_tac) \\ simp[])
433 \\ first_assum(qspec_then`0`mp_tac)
434 \\ impl_tac >- simp[]
435 \\ simp_tac(srw_ss())[] \\ rw[]
436 \\ AP_THM_TAC \\ AP_TERM_TAC
437 \\ first_x_assum match_mp_tac
438 \\ gen_tac \\ strip_tac
439 \\ first_x_assum(qspec_then`SUC n`mp_tac)
440 \\ simp[]
441QED
442
443Definition word_to_bytes_aux_def: (* length, 'a word, endianness *)
444 word_to_bytes_aux 0 (w:'a word) be = [] /\
445 word_to_bytes_aux (SUC n) w be =
446 (word_to_bytes_aux n w be) ++ [get_byte (n2w n) w be]
447End
448(* cyclic repeat as get_byte does when length > bytes_in_word for 'a*)
449
450Definition word_to_bytes_def:
451 word_to_bytes (w:'a word) be =
452 word_to_bytes_aux (dimindex (:'a) DIV 8) w be
453End
454
455Theorem LENGTH_word_to_bytes_aux[simp]:
456 LENGTH (word_to_bytes_aux n w b) = n
457Proof
458 Induct_on`n` \\ rw[word_to_bytes_aux_def]
459QED
460
461Theorem LENGTH_word_to_bytes[simp]:
462 LENGTH (word_to_bytes (w:'a word) be) = dimindex(:'a) DIV 8
463Proof
464 rw[word_to_bytes_def]
465QED
466
467Theorem EL_word_to_bytes_aux:
468 i < n ==> EL i (word_to_bytes_aux n w be) = get_byte (n2w i) w be
469Proof
470 map_every qid_spec_tac [`i`,`n`]
471 \\ Induct \\ rw[word_to_bytes_aux_def]
472 \\ Cases_on `i < n`
473 >- simp[EL_APPEND1]
474 \\ `i = n` by gvs[]
475 \\ simp[EL_APPEND2]
476QED
477
478Theorem byte_index_cycle:
479 8 <= dimindex (:'a) ==>
480 byte_index (n2w ((w2n (a:'a word)) MOD (dimindex (:'a) DIV 8)):'a word) be = byte_index a be
481Proof
482 strip_tac>>
483 simp[byte_index_def]>>
484 ‘0 < dimindex(:'a) DIV 8’
485 by (CCONTR_TAC>>fs[NOT_LESS]>>
486 fs[DIV_EQ_0])>>
487 ‘w2n a MOD (dimindex (:'a) DIV 8) < dimword (:'a)’
488 by (irule LESS_EQ_LESS_TRANS>>
489 irule_at Any w2n_lt>>
490 irule_at Any MOD_LESS_EQ>>fs[])>>
491 simp[MOD_MOD]
492QED
493
494Theorem get_byte_cycle:
495 8 <= dimindex (:'a) ==>
496 get_byte (n2w ((w2n (a:'a word)) MOD (dimindex (:'a) DIV 8)):'a word) w be
497 = get_byte a w be
498Proof
499 rw[get_byte_def,byte_index_cycle]
500QED
501
502Theorem set_byte_cycle:
503 8 <= dimindex (:'a) ==>
504 set_byte (n2w ((w2n (a:'a word)) MOD (dimindex (:'a) DIV 8)):'a word) b w be
505 = set_byte a b w be
506Proof
507 rw[set_byte_def,byte_index_cycle]
508QED
509
510Theorem word_slice_alt_word_slice:
511 h <= dimindex (:'a) ==>
512 word_slice_alt (SUC h) l w = word_slice h l (w:'a word)
513Proof
514 rw[word_slice_alt_def,word_slice_def]>>
515 simp[GSYM WORD_EQ]>>rpt strip_tac>>
516 srw_tac[wordsLib.WORD_BIT_EQ_ss][]>>
517 simp[EQ_IMP_THM]>>rw[]
518QED
519
520Theorem word_slice_shift:
521 h < dimindex (:'a) ==>
522 word_slice h l (w:'a word) = w >>> l << l << (dimindex (:'a) - (SUC h)) >>> (dimindex (:'a) - (SUC h))
523Proof
524 strip_tac>>
525 Cases_on ‘l <= h’>>fs[NOT_LESS_EQUAL,WORD_SLICE_ZERO]>>
526 simp[WORD_SLICE_THM]>>
527 simp[word_lsr_n2w,ADD1]>>
528 simp[WORD_BITS_LSL]>>
529 simp[WORD_BITS_COMP_THM]>>
530 simp[MIN_DEF]>>
531 rewrite_tac[SUB_RIGHT_ADD]>>
532 IF_CASES_TAC>>fs[]
533QED
534
535Theorem word_slice_alt_shift:
536 h <= dimindex (:'a) ==>
537 word_slice_alt h l (w:'a word) = w >>> l << l << (dimindex (:'a) - h) >>> (dimindex (:'a) - h)
538Proof
539 strip_tac>>
540 Cases_on ‘h’>>fs[]>-
541 srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def]>>
542 rw[word_slice_alt_word_slice,word_slice_shift]
543QED
544
545Theorem byte_index_offset:
546 8 <= dimindex (:'a) ==>
547 byte_index (a:'a word) be + 8 <= dimindex (:'a)
548Proof
549 strip_tac>>
550 ‘0 < dimindex (:'a) DIV 8’ by
551 (simp[GSYM NOT_ZERO_LT_ZERO]>>
552 strip_tac>>
553 ‘dimindex (:'a) < 8’ by
554 (irule DIV_0_IMP_LT>>simp[])>>simp[])>>
555 assume_tac (Q.SPECL [‘dimindex(:'a)’,‘8’] DA)>>
556 fs[]>>
557 rw[byte_index_def]>-
558 (simp[LEFT_SUB_DISTRIB]>>
559 simp[LEFT_ADD_DISTRIB]>>
560 rewrite_tac[SUB_PLUS]>>
561 irule LESS_EQ_TRANS>>
562 qexists_tac ‘8 * (dimindex (:'a) DIV 8)’>>
563 simp[]>>
564 qpat_x_assum ‘_ = dimindex (:'a)’ $ assume_tac o GSYM>>
565 first_assum (fn h => rewrite_tac[h])>>
566 fs[GSYM DIV_EQ_0])>>
567 irule LESS_EQ_TRANS>>
568 qexists_tac ‘8 * ((w2n a MOD (dimindex (:'a) DIV 8)) + 1)’>>
569 conj_tac >- simp[LEFT_ADD_DISTRIB]>>
570 irule LESS_EQ_TRANS>>
571 irule_at Any (iffRL LE_MULT_LCANCEL)>>
572 simp[GSYM ADD1]>>simp[GSYM LESS_EQ]>>
573 irule_at Any MOD_LESS>>
574 simp[]>>
575 qpat_x_assum ‘_ = dimindex (:'a)’ $ assume_tac o GSYM>>
576 first_assum (fn h => rewrite_tac[h])>>
577 simp[]>>
578 fs[GSYM DIV_EQ_0]
579QED
580
581Theorem DIV_not_0:
582 1 < d ==> (d <= n <=> 0 < n DIV d)
583Proof
584 strip_tac>>
585 drule DIV_EQ_0>>strip_tac>>
586 first_x_assum $ qspec_then ‘n’ assume_tac>>fs[]
587QED
588
589Theorem get_byte_set_byte_irrelevant:
590 16 <= dimindex (:'a) /\
591 w2n (a:'a word) MOD (dimindex(:'a) DIV 8) <> w2n a' MOD (dimindex(:'a) DIV 8)
592 ==>
593 get_byte a' (set_byte a b w be) be = get_byte a' w be
594Proof
595 strip_tac>>
596 rewrite_tac[set_byte_def,get_byte_def]>>
597 simp[GSYM WORD_w2w_OVER_BITWISE]>>
598 ‘0 < dimindex (:'a) DIV 8’
599 by (simp[GSYM NOT_ZERO_LT_ZERO]>>
600 strip_tac>>
601 ‘dimindex (:'a) < 8’
602 by (irule DIV_0_IMP_LT>>simp[])>>simp[])>>
603 ‘w2n a' MOD (dimindex (:'a) DIV 8) < dimindex (:'a) DIV 8’ by
604 simp[MOD_LESS]>>
605 ‘w2n a MOD (dimindex (:'a) DIV 8) < dimindex (:'a) DIV 8’ by
606 simp[MOD_LESS]>>
607 ‘byte_index a be + 8 <= dimindex (:'a)’ by fs[byte_index_offset]>>
608 ‘byte_index a' be + 8 <= dimindex (:'a)’ by fs[byte_index_offset]>>
609 simp[word_slice_alt_shift]>>
610 simp[w2w_def,w2n_lsr]>>
611 simp[WORD_MUL_LSL]>>
612 simp[word_mul_n2w]>>
613 simp[word_mul_def]>>
614 ‘(w2n (w >>> (byte_index a be + 8)) * 2 ** (byte_index a be + 8)) < dimword (:'a)’ by
615 (simp[w2n_lsr]>>
616 ‘0:num < 2 ** (byte_index a be + 8)’ by simp[]>>
617 drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>>strip_tac>>
618 simp[]>>rewrite_tac[Once ADD_COMM]>>simp[DIV_MULT]>>
619 irule LESS_EQ_LESS_TRANS>>
620 irule_at Any w2n_lt>>
621 qexists_tac ‘w’>>simp[])>>
622 ‘(w2n b * 2 ** byte_index a be) < dimword (:'a)’ by
623 (irule LESS_LESS_EQ_TRANS>>
624 irule_at Any (iffRL LT_MULT_RCANCEL)>>
625 irule_at Any w2n_lt>>
626 simp[dimword_def]>>
627 irule LESS_EQ_TRANS>>
628 irule_at Any (iffRL EXP_BASE_LE_MONO)>>
629 qexists_tac ‘byte_index a be + 8’>>simp[EXP_ADD])>>
630 simp[MOD_LESS]>>
631 qmatch_goalsub_abbrev_tac ‘w1 || w2 || w3’>>
632 qpat_x_assum ‘_ <> _’ mp_tac>>
633 simp[NOT_NUM_EQ,GSYM LESS_EQ]>>strip_tac>-
634 (‘if be then byte_index a' be < byte_index a be
635 else byte_index a be < byte_index a' be’ by rw[byte_index_def]>>
636 Cases_on ‘be’>>simp[]>-
637 (‘w1 = 0w /\ w3 = n2w (w2n w DIV 2 ** byte_index a' T) /\ w2 = 0w’ by
638 (conj_tac >-
639 (simp[Abbr ‘w1’]>>
640 simp[w2n_lsr]>>
641 ‘0:num < 2 ** (byte_index a T + 8)’ by simp[ZERO_LT_EXP]>>
642 drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>>strip_tac>>
643 simp[]>>
644 rewrite_tac[Once ADD_COMM]>>
645 simp[DIV_MULT]>>
646 simp[EXP_ADD]>>
647 qpat_x_assum ‘if _ then _ else _’ mp_tac>>
648 simp[LESS_EQ,ADD1]>>strip_tac>>
649 drule LESS_EQUAL_ADD>>strip_tac>>
650 simp[EXP_ADD]>>
651 ntac 2 (rewrite_tac[Once MULT_ASSOC])>>
652 simp[MULT_DIV])>>
653 ‘byte_index a' T + 8 <= byte_index a T’ by
654 (simp[byte_index_def]>>
655 irule LESS_EQ_TRANS>>
656 qexists_tac ‘8 * (dimindex (:'a) DIV 8 - (w2n a' MOD (dimindex (:'a) DIV 8) + 1) + 1)’>>
657 simp[]>>
658 rewrite_tac[Once $ GSYM ADD1]>>
659 simp[GSYM LESS_EQ]>>
660 ‘w2n a' MOD (dimindex (:'a) DIV 8) < dimindex (:'a) DIV 8’ by
661 simp[MOD_LESS]>>
662 simp[])>>
663 conj_tac >-
664 (simp[Abbr ‘w3’]>>
665 ‘dimword (:'a) =
666 2 ** (dimindex (:'a) + byte_index a' T - byte_index a T)
667 * 2 ** (byte_index a T - byte_index a' T)’ by
668 fs[dimword_def,GSYM EXP_ADD]>>
669 pop_assum (fn h => rewrite_tac[h])>>
670 ‘0 < 2 ** (byte_index a T - byte_index a' T) /\
671 0 < 2 ** (dimindex (:'a) + byte_index a' T - byte_index a T)’ by
672 fs[ZERO_LT_EXP]>>
673 drule (GSYM DIV_MOD_MOD_DIV)>>
674 pop_assum kall_tac>>
675 disch_then $ drule>>strip_tac>>
676 pop_assum (fn h => rewrite_tac[h])>>
677 qmatch_goalsub_abbrev_tac ‘(_ * X) DIV Y’>>
678 ‘Y = X * 2 ** byte_index a' T’ by simp[Abbr ‘X’,Abbr ‘Y’,GSYM EXP_ADD]>>
679 pop_assum (fn h => rewrite_tac[h])>>
680 ‘0 < X /\ 0 < 2 ** byte_index a' T’ by simp[ZERO_LT_EXP,Abbr ‘X’]>>
681 simp[GSYM DIV_DIV_DIV_MULT]>>
682 simp[Abbr ‘X’]>>
683 drule LESS_EQUAL_ADD>>strip_tac>>
684 simp[EXP_ADD]>>
685 simp[MOD_MULT_MOD,MULT_DIV])>>
686 simp[Abbr ‘w2’]>>
687 drule LESS_EQUAL_ADD>>strip_tac>>
688 simp[EXP_ADD,MULT_DIV]>>
689 rewrite_tac[Once MULT_ASSOC]>>
690 simp[MULT_DIV])>>simp[])>>
691 ‘byte_index a F + 8 <= byte_index a' F’ by simp[byte_index_def]>>
692 ‘w3 = 0w /\ w1 = n2w (w2n w DIV 2 ** byte_index a' F) /\ w2 = 0w’ by
693 (conj_tac >-
694 (simp[Abbr ‘w3’]>>
695 qmatch_goalsub_abbrev_tac ‘(_ * X) MOD _ DIV Y’>>
696 ‘Y = X * 2 ** byte_index a' F’ by simp[Abbr ‘Y’,Abbr ‘X’,GSYM EXP_ADD]>>
697 pop_assum (fn h => rewrite_tac[h])>>
698 simp[GSYM DIV_DIV_DIV_MULT,ZERO_LT_EXP,Abbr ‘X’]>>
699 ‘dimword (:'a) =
700 2 ** (dimindex (:'a) - byte_index a F) * 2 ** (byte_index a F)’ by
701 fs[dimword_def,GSYM EXP_ADD]>>
702 pop_assum (fn h => rewrite_tac[h])>>
703 simp[GSYM DIV_MOD_MOD_DIV,ZERO_LT_EXP,MULT_DIV]>>
704 qmatch_goalsub_abbrev_tac ‘X MOD _’>>
705 ‘w2n w MOD 2 ** byte_index a F < 2 ** byte_index a' F’ by
706 (irule LESS_TRANS>>
707 irule_at (Pos hd) MOD_LESS>>
708 simp[])>>
709 pop_assum mp_tac>>
710 DEP_ONCE_REWRITE_TAC[GSYM DIV_EQ_0]>>
711 simp[EXP])>>
712 conj_tac >-
713 (simp[Abbr ‘w1’]>>
714 simp[w2n_lsr]>>
715 ‘0 < 2 ** (byte_index a F + 8)’ by simp[]>>
716 drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>>
717 strip_tac>>
718 simp[]>>
719 rewrite_tac[Once ADD_COMM]>>
720 simp[DIV_MULT]>>
721 drule LESS_EQUAL_ADD>>strip_tac>>
722 simp[]>>
723 qabbrev_tac ‘X = byte_index a F + 8’>>
724 simp[EXP_ADD]>>
725 simp[GSYM DIV_DIV_DIV_MULT]>>
726 rewrite_tac[Once ADD_COMM]>>
727 simp[DIV_MULT,MULT_DIV])>>
728 simp[Abbr ‘w2’]>>
729 drule LESS_EQUAL_ADD>>strip_tac>>
730 simp[]>>
731 simp[EXP_ADD]>>
732 rewrite_tac[MULT_ASSOC]>>
733 once_rewrite_tac[MULT_COMM]>>
734 simp[GSYM DIV_DIV_DIV_MULT,MULT_DIV]>>
735 ‘w2n b DIV 256 = 0’ by
736 (simp[DIV_EQ_0]>>
737 irule LESS_LESS_EQ_TRANS>>
738 irule_at Any w2n_lt>>
739 simp[])>>
740 simp[])>>simp[])>>
741 ‘if be then byte_index a be < byte_index a' be
742 else byte_index a' be < byte_index a be’ by rw[byte_index_def]>>
743 Cases_on ‘be’>>simp[]>-
744 (‘byte_index a T + 8 <= byte_index a' T’ by simp[byte_index_def]>>
745 ‘w3 = 0w /\ w1 = n2w (w2n w DIV 2 ** byte_index a' T) /\ w2 = 0w’ by
746 (conj_tac >-
747 (simp[Abbr ‘w3’]>>
748 qmatch_goalsub_abbrev_tac ‘(_ * X) MOD _ DIV Y’>>
749 ‘Y = X * 2 ** byte_index a' T’ by simp[Abbr ‘Y’,Abbr ‘X’,GSYM EXP_ADD]>>
750 pop_assum (fn h => rewrite_tac[h])>>
751 simp[GSYM DIV_DIV_DIV_MULT,ZERO_LT_EXP,Abbr ‘X’]>>
752 ‘dimword (:'a) =
753 2 ** (dimindex (:'a) - byte_index a T) * 2 ** (byte_index a T)’ by
754 fs[dimword_def,GSYM EXP_ADD]>>
755 pop_assum (fn h => rewrite_tac[h])>>
756 simp[GSYM DIV_MOD_MOD_DIV,ZERO_LT_EXP,MULT_DIV]>>
757 qmatch_goalsub_abbrev_tac ‘X MOD _’>>
758 ‘w2n w MOD 2 ** byte_index a T < 2 ** byte_index a' T’ by
759 (irule LESS_TRANS>>
760 irule_at (Pos hd) MOD_LESS>>
761 simp[])>>
762 pop_assum mp_tac>>
763 DEP_ONCE_REWRITE_TAC[GSYM DIV_EQ_0]>>
764 simp[EXP])>>
765 conj_tac >-
766 (simp[Abbr ‘w1’]>>
767 simp[w2n_lsr]>>
768 ‘0 < 2 ** (byte_index a T + 8)’ by simp[]>>
769 drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>>
770 strip_tac>>
771 simp[]>>
772 rewrite_tac[Once ADD_COMM]>>
773 simp[DIV_MULT]>>
774 drule LESS_EQUAL_ADD>>strip_tac>>
775 simp[]>>
776 qabbrev_tac ‘X = byte_index a T + 8’>>
777 simp[EXP_ADD]>>
778 simp[GSYM DIV_DIV_DIV_MULT,MULT_DIV]>>
779 rewrite_tac[Once ADD_COMM]>>
780 simp[DIV_MULT])>>
781 simp[Abbr ‘w2’]>>
782 drule LESS_EQUAL_ADD>>strip_tac>>
783 simp[]>>
784 simp[EXP_ADD]>>
785 rewrite_tac[MULT_ASSOC]>>
786 once_rewrite_tac[MULT_COMM]>>
787 simp[GSYM DIV_DIV_DIV_MULT,MULT_DIV]>>
788 ‘w2n b DIV 256 = 0’ by
789 (simp[DIV_EQ_0]>>
790 irule LESS_LESS_EQ_TRANS>>
791 irule_at Any w2n_lt>>
792 simp[])>>
793 simp[])>>simp[])>>
794 ‘w1 = 0w /\ w3 = n2w (w2n w DIV 2 ** byte_index a' F) /\ w2 = 0w’ by
795 (conj_tac >-
796 (simp[Abbr ‘w1’]>>
797 simp[w2n_lsr]>>
798 ‘0 < 2 ** (byte_index a F + 8)’ by simp[ZERO_LT_EXP]>>
799 drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>>strip_tac>>
800 simp[]>>
801 rewrite_tac[Once ADD_COMM]>>
802 simp[DIV_MULT]>>
803 simp[EXP_ADD]>>
804 qpat_x_assum ‘if _ then _ else _’ mp_tac>>
805 simp[LESS_EQ,ADD1]>>strip_tac>>
806 drule LESS_EQUAL_ADD>>strip_tac>>
807 simp[EXP_ADD]>>
808 ntac 2 (rewrite_tac[Once MULT_ASSOC])>>
809 simp[MULT_DIV])>>
810 ‘byte_index a' F + 8 <= byte_index a F’ by
811 (simp[byte_index_def]>>
812 irule LESS_EQ_TRANS>>
813 qexists_tac ‘8 * (dimindex (:'a) DIV 8 - (w2n a' MOD (dimindex (:'a) DIV 8) + 1) + 1)’>>
814 simp[]>>
815 rewrite_tac[Once $ GSYM ADD1]>>
816 simp[GSYM LESS_EQ]>>
817 ‘w2n a' MOD (dimindex (:'a) DIV 8) < dimindex (:'a) DIV 8’ by
818 simp[MOD_LESS]>>
819 simp[])>>
820 conj_tac >-
821 (simp[Abbr ‘w3’]>>
822 ‘dimword (:'a) =
823 2 ** (dimindex (:'a) + byte_index a' F - byte_index a F)
824 * 2 ** (byte_index a F - byte_index a' F)’ by
825 fs[dimword_def,GSYM EXP_ADD]>>
826 pop_assum (fn h => rewrite_tac[h])>>
827 ‘0 < 2 ** (byte_index a F - byte_index a' F) /\
828 0 < 2 ** (dimindex (:'a) + byte_index a' F - byte_index a F)’ by
829 fs[ZERO_LT_EXP]>>
830 simp[GSYM DIV_MOD_MOD_DIV]>>
831 qmatch_goalsub_abbrev_tac ‘(_ * X) DIV Y’>>
832 ‘Y = X * 2 ** byte_index a' F’ by simp[Abbr ‘X’,Abbr ‘Y’,GSYM EXP_ADD]>>
833 pop_assum (fn h => rewrite_tac[h])>>
834 ‘0 < X /\ 0 < 2 ** byte_index a' F’ by simp[ZERO_LT_EXP,Abbr ‘X’]>>
835 simp[GSYM DIV_DIV_DIV_MULT]>>
836 drule LESS_EQUAL_ADD>>strip_tac>>
837 simp[EXP_ADD]>>
838 rewrite_tac[Once MULT_COMM]>>
839 simp[MOD_MULT_MOD,MULT_DIV])>>
840 simp[Abbr ‘w2’]>>
841 drule LESS_EQUAL_ADD>>strip_tac>>
842 simp[EXP_ADD]>>
843 rewrite_tac[Once MULT_ASSOC]>>
844 simp[MULT_DIV])>>simp[]
845QED
846
847Theorem set_byte_get_byte:
848 8 <= dimindex (:'a) ==>
849 set_byte a (get_byte (a:'a word) (w:'a word) be) w be = w
850Proof
851 strip_tac>>
852 simp[get_byte_def,set_byte_def]>>
853 imp_res_tac byte_index_offset>>
854 first_x_assum $ qspecl_then [‘be’, ‘a’] assume_tac>>
855 qmatch_goalsub_abbrev_tac ‘w0 || _ || _’>>
856 ‘w0 = word_slice_alt (byte_index a be + 8) (byte_index a be) w’ by
857 (simp[Abbr ‘w0’]>>
858 ‘byte_index a be + 8 = SUC (byte_index a be + 7)’ by simp[]>>
859 simp[word_slice_alt_word_slice]>>
860 simp[WORD_SLICE_THM]>>
861 qmatch_abbrev_tac ‘A << _ = B << _’>>
862 ‘A = B’ by
863 (simp[Abbr ‘A’,Abbr ‘B’]>>
864 simp[w2w_w2w,word_lsr_n2w]>>
865 simp[WORD_BITS_COMP_THM]>>
866 simp[MIN_DEF])>>
867 simp[])>>simp[]>>
868 srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def]>>
869 Cases_on ‘i < byte_index a be’>>fs[NOT_LESS]>>
870 Cases_on ‘i < byte_index a be + 8’>>fs[]
871QED
872
873Theorem set_byte_get_byte_copy:
874 8 <= dimindex (:'a) ==>
875 set_byte a (get_byte (a:'a word) (w:'a word) be) w' be =
876 word_slice (byte_index a be + 7) (byte_index a be) w ||
877 (if byte_index a be + 8 = dimindex (:'a) then 0w
878 else word_slice (dimindex (:'a) - 1) (byte_index a be + 8) w') ||
879 if byte_index a be = 0 then 0w else word_slice (byte_index a be - 1) 0 w'
880Proof
881 strip_tac>>
882 simp[get_byte_def,set_byte_def]>>
883 imp_res_tac byte_index_offset>>
884 first_x_assum $ qspecl_then [‘be’, ‘a’] assume_tac>>
885 qmatch_goalsub_abbrev_tac ‘w0 || _ || _’>>
886 ‘w0 = word_slice (byte_index a be + 7) (byte_index a be) w’ by
887 (simp[Abbr ‘w0’]>>
888 simp[WORD_SLICE_THM]>>
889 qmatch_goalsub_abbrev_tac ‘A << _ = B << _’>>
890 ‘A = B’ by
891 (simp[Abbr ‘A’,Abbr ‘B’]>>
892 simp[w2w_w2w,word_lsr_n2w]>>
893 simp[WORD_BITS_COMP_THM]>>
894 simp[MIN_DEF])>>
895 simp[])>>simp[]>>
896 Cases_on ‘byte_index a be’>>fs[]>>
897 Cases_on ‘byte_index a be + 8 = dimindex (:'a)’>>fs[]>>
898 srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def]>>
899 Cases_on ‘i <= n’>>fs[NOT_LESS]
900QED
901
902Theorem set_byte_get_byte':
903 8 <= dimindex (:'a) ==>
904 set_byte a (get_byte (a:'a word) (w:'a word) be) w be = w
905Proof
906 rw[set_byte_get_byte_copy]>-
907 srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def]>-
908 (simp[WORD_SLICE_COMP_THM]>>
909 srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def])>-
910 (rewrite_tac[Once WORD_OR_COMM]>>
911 simp[WORD_SLICE_COMP_THM]>>
912 srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def])>>
913 qmatch_goalsub_abbrev_tac ‘w2 || w3 || w1’>>
914 ‘w3 || w2 || w1 = w’ by
915 (simp[Abbr ‘w2’]>>
916 simp[Abbr ‘w1’]>>
917 simp[WORD_SLICE_COMP_THM]>>
918 simp[Abbr ‘w3’]>>
919 rewrite_tac[Once WORD_OR_COMM]>>
920 drule byte_index_offset>>
921 disch_then $ qspecl_then [‘be’, ‘a’] assume_tac>>
922 simp[WORD_SLICE_COMP_THM]>>
923 srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def])>>
924 fs[]
925QED
926
927Theorem word_slice_alt_zero:
928 word_slice_alt h l 0w = 0w
929Proof
930 srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def]
931QED
932
933Theorem word_slice_alt_empty:
934 h <= l ==> word_slice_alt h l w = 0w
935Proof
936 asm_simp_tac (boss_ss () ++ fcpLib.FCP_ss) [word_slice_alt_def, word_0]
937 >> rpt strip_tac
938 >> spose_not_then assume_tac
939 >> simp []
940QED
941
942Theorem word_slice_alt_full:
943 dimindex (:'a) <= h ==> word_slice_alt h 0 (w: 'a word) = w
944Proof
945 asm_simp_tac (boss_ss () ++ fcpLib.FCP_ss) [word_slice_alt_def]
946QED
947
948Theorem bit_field_insert_self_word_slice_alt:
949 l1 <= h2 /\ l2 <= SUC h1 ==>
950 bit_field_insert h1 l1 (w >>> l1) (word_slice_alt h2 l2 w) = word_slice_alt (MAX (SUC h1) h2) (MIN l1 l2) w
951Proof
952 asm_simp_tac (boss_ss () ++ fcpLib.FCP_ss) [bit_field_insert_def, word_slice_alt_def, word_modify_def, word_lsr_def, LT_SUC_LE]
953 >> rpt strip_tac
954 >> IF_CASES_TAC
955 >- simp []
956 >- fs [NOT_LE]
957QED
958
959Theorem word_of_bytes_word_to_bytes_aux_le:
960 n <= dimindex (:'a) DIV 8 /\ 8 <= dimindex (:'a)
961 ==> word_of_bytes F 0w (word_to_bytes_aux n (w: 'a word) F) = word_slice_alt (8 * n) 0 w
962Proof
963 Induct_on `n`
964 >- simp [word_to_bytes_aux_def, word_of_bytes_def, word_slice_alt_empty]
965 >- (strip_tac
966 >> `dimindex (:'a) DIV 8 <= dimindex (:'a)` by simp [DIV_LESS_EQ]
967 >> `n < dimword (:'a)` by simp [dimindex_lt_dimword, LESS_TRANS, LESS_LESS_EQ_TRANS]
968 >> simp [word_to_bytes_aux_def, GSYM SNOC_APPEND, word_of_bytes_SNOC, set_byte_bit_field_insert, get_byte_def, bit_field_insert_w2w, byte_index_def, bit_field_insert_self_word_slice_alt, MAX_DEF, ADD1, LEFT_ADD_DISTRIB])
969QED
970
971Theorem word_of_bytes_word_to_bytes_aux_be:
972 n <= dimindex (:'a) DIV 8 /\ 8 <= dimindex (:'a)
973 ==> word_of_bytes T 0w (word_to_bytes_aux n (w: 'a word) T) = word_slice_alt (8 * (dimindex (:'a) DIV 8)) (8 * (dimindex (:'a) DIV 8 - n)) w
974Proof
975 Induct_on `n`
976 >- simp [word_to_bytes_aux_def, word_of_bytes_def, word_slice_alt_empty]
977 >- (rpt strip_tac
978 >> `dimindex (:'a) DIV 8 <= dimindex (:'a)` by simp [DIV_LESS_EQ]
979 >> `n < dimword (:'a)` by simp [dimindex_lt_dimword, LESS_TRANS, LESS_LESS_EQ_TRANS]
980 >> simp [word_to_bytes_aux_def, GSYM SNOC_APPEND, word_of_bytes_SNOC, set_byte_bit_field_insert, get_byte_def, bit_field_insert_w2w, byte_index_def, bit_field_insert_self_word_slice_alt, MAX_EQ_GE, MIN_EQ_LE, ADD1])
981QED
982
983Theorem word_of_bytes_word_to_bytes:
984 8 <= dimindex (:'a) /\ divides 8 (dimindex (:'a))
985 ==> word_of_bytes be 0w (word_to_bytes (w: 'a word) be) = w
986Proof
987 simp [word_to_bytes_def]
988 >> Cases_on `be`
989 >- simp [word_of_bytes_word_to_bytes_aux_be, dividesTheory.DIVIDES_DIV, word_slice_alt_full]
990 >- simp [word_of_bytes_word_to_bytes_aux_le, dividesTheory.DIVIDES_DIV, word_slice_alt_full]
991QED
992
993Theorem word_to_bytes_word_of_bytes_32 = word_of_bytes_word_to_bytes |> INST_TYPE [``:'a`` |-> ``:32``] |> SRULE [dividesTheory.compute_divides]
994Theorem word_to_bytes_word_of_bytes_64 = word_of_bytes_word_to_bytes |> INST_TYPE [``:'a`` |-> ``:64``] |> SRULE [dividesTheory.compute_divides]
995
996(* ------------------------------------------------------------------- *)
997(* Helper functions for cv translation of word_of_bytes/word_to_bytes *)
998(* ------------------------------------------------------------------- *)
999
1000(* Convert a list of bytes to a natural number (little-endian) *)
1001Definition num_of_bytes_def:
1002 num_of_bytes [] = 0 /\
1003 num_of_bytes ((b:word8)::bs) = w2n b + 256 * num_of_bytes bs
1004End
1005
1006(* Convert a natural number to a list of bytes (little-endian) *)
1007Definition bytes_of_num_def:
1008 bytes_of_num 0 n = [] /\
1009 bytes_of_num (SUC k) n = (n2w n : word8) :: bytes_of_num k (n DIV 256)
1010End
1011
1012(* Pad and reverse a byte list for big-endian conversion.
1013 be_bytes k res bs pads bs with zeros to length k and reverses,
1014 accumulating the result in res. *)
1015Definition be_bytes_def:
1016 be_bytes 0 res bs = res /\
1017 be_bytes (SUC l) res [] = be_bytes l ((0w:word8)::res) [] /\
1018 be_bytes (SUC l) res (x::xs) = be_bytes l (x::res) xs
1019End
1020
1021(* Basic properties of helper functions *)
1022
1023Theorem LENGTH_bytes_of_num[simp]:
1024 ∀k n. LENGTH (bytes_of_num k n) = k
1025Proof
1026 Induct \\ rw[bytes_of_num_def]
1027QED
1028
1029Theorem EL_bytes_of_num:
1030 i < k ==> EL i (bytes_of_num k n) = n2w (n DIV 256 ** i)
1031Proof
1032 map_every qid_spec_tac [`n`,`i`,`k`]
1033 \\ Induct \\ rw[bytes_of_num_def]
1034 \\ Cases_on `i` \\ gvs[]
1035 \\ simp[DIV_DIV_DIV_MULT, EXP]
1036QED
1037
1038Theorem LENGTH_be_bytes:
1039 !l res bs. LENGTH (be_bytes l res bs) = l + LENGTH res
1040Proof
1041 Induct \\ rw[be_bytes_def] \\ Cases_on ‘bs’ \\ rw[be_bytes_def]
1042QED
1043
1044Theorem be_bytes_thm:
1045 !l res bs. be_bytes l res bs =
1046 REVERSE (TAKE l (bs ++ REPLICATE l 0w)) ++ res
1047Proof
1048 Induct
1049 \\ rw[be_bytes_def]
1050 \\ Cases_on ‘bs’ \\ rw[be_bytes_def]
1051 \\ rw[TAKE_APPEND]
1052 \\ rw[listTheory.LIST_EQ_REWRITE, listTheory.LENGTH_TAKE_EQ]
1053 \\ rw[listTheory.EL_TAKE, EL_REPLICATE]
1054 \\ qmatch_goalsub_rename_tac`EL x _`
1055 \\ Cases_on ‘x’ \\ rw[listTheory.EL_TAKE, EL_REPLICATE]
1056QED
1057
1058Theorem num_of_bytes_REPLICATE_0w[simp]:
1059 ∀n. num_of_bytes (REPLICATE n 0w) = 0
1060Proof
1061 Induct \\ rw[num_of_bytes_def]
1062QED
1063
1064Theorem num_of_bytes_APPEND:
1065 ∀xs ys. num_of_bytes (xs ++ ys) =
1066 num_of_bytes xs + 256 ** LENGTH xs * num_of_bytes ys
1067Proof
1068 Induct \\ rw[num_of_bytes_def, EXP]
1069QED
1070
1071Theorem num_of_bytes_DIV_EXP_MOD:
1072 ∀bs j.
1073 (num_of_bytes bs DIV (256 ** j)) MOD 256 =
1074 if j < LENGTH bs then w2n (EL j bs) else 0
1075Proof
1076 Induct \\ simp[num_of_bytes_def]
1077 \\ qx_gen_tac `b` \\ Cases \\ gvs[]
1078 \\ `w2n b < 256`
1079 by (qspec_then`b`mp_tac w2n_lt \\ rw[dimword_def])
1080 \\ simp[EXP]
1081 \\ qmatch_goalsub_abbrev_tac`(c * a + bb)`
1082 \\ qspecl_then[`c`,`c ** n`]mp_tac(GSYM DIV_DIV_DIV_MULT)
1083 \\ impl_tac >- rw[Abbr`c`]
1084 \\ simp[] \\ disch_then kall_tac
1085 \\ `(bb + a * c) DIV c = a` by (
1086 qspecl_then[`c`,`bb`]mp_tac DIV_MULT
1087 \\ simp[] \\ disch_then(qspec_then`a`mp_tac) \\ rw[])
1088 \\ rw[]
1089QED
1090
1091(* first_byte_at k j a bs finds the first byte in bs that lands at position j
1092 when bytes are written starting at address a, with k byte positions (wrapping). *)
1093Definition first_byte_at_def:
1094 first_byte_at k j a [] = (0w:word8) /\
1095 first_byte_at k j a (b::bs) =
1096 if w2n a MOD k = j then b else first_byte_at k j (a + 1w) bs
1097End
1098
1099(* Connecting get_byte and word_of_bytes for little-endian *)
1100Theorem get_byte_word_of_bytes_le:
1101 ∀bs j a.
1102 8 <= dimindex(:'a) /\ j < dimindex(:'a) DIV 8 ==>
1103 get_byte (n2w j) (word_of_bytes F a bs : 'a word) F =
1104 first_byte_at (dimindex(:'a) DIV 8) j a bs
1105Proof
1106 Induct \\ rw[]
1107 >- rw[word_of_bytes_def, first_byte_at_def, get_byte_def]
1108 \\ rw[word_of_bytes_def]
1109 \\ Cases_on`j = w2n a MOD (dimindex (:'a) DIV 8)`
1110 >- (
1111 simp[first_byte_at_def] \\ gvs[]
1112 \\ qmatch_goalsub_abbrev_tac`get_byte a'`
1113 \\ qmatch_goalsub_abbrev_tac`set_byte a h w`
1114 \\ `set_byte a h w F = set_byte a' h w F`
1115 by ( irule set_byte_change_a \\ gvs[Abbr`a'`]
1116 \\ qmatch_goalsub_abbrev_tac`x = _`
1117 \\ qmatch_goalsub_abbrev_tac`x MOD k`
1118 \\ `x < k` by gvs[Abbr`k`,dimindex_lt_dimword,X_LT_DIV]
1119 \\ simp[LESS_MOD] )
1120 \\ rw[get_byte_set_byte] )
1121 \\ rw[first_byte_at_def]
1122 \\ reverse $ Cases_on`16 ≤ dimindex (:'a)`
1123 >- (
1124 gvs[X_LT_DIV] \\ Cases_on`j` \\ gvs[]
1125 \\ `1 ≤ dimindex (:'a) DIV 8` by gvs[X_LE_DIV]
1126 \\ `dimindex (:'a) DIV 8 ≤ 1` by gvs[DIV_LE_X]
1127 \\ `dimindex (:'a) DIV 8 = 1` by gvs[]
1128 \\ gvs[X_LT_DIV] )
1129 \\ DEP_REWRITE_TAC[get_byte_set_byte_irrelevant]
1130 \\ simp[]
1131 \\ gvs[LESS_MOD, X_LT_DIV, dimindex_lt_dimword]
1132QED
1133
1134(* Helper lemma: first_byte_at with offset starting address.
1135 This generalizes first_byte_at_0w to handle starting at n2w m instead of 0w. *)
1136Theorem first_byte_at_offset:
1137 ∀bs m k j.
1138 0 < k /\ j < k /\ m < k /\ m <= j /\ k <= dimword(:'a) ==>
1139 first_byte_at k j (n2w m : 'a word) bs =
1140 if j - m < LENGTH bs then EL (j - m) bs else 0w
1141Proof
1142 Induct
1143 >- rw[first_byte_at_def]
1144 \\ simp[first_byte_at_def]
1145 \\ rpt gen_tac \\ strip_tac
1146 \\ IF_CASES_TAC
1147 >- rw[]
1148 \\ Cases_on`m < j` \\ gvs[]
1149 \\ first_x_assum(qspec_then`m + 1`mp_tac)
1150 \\ simp[word_add_n2w]
1151 \\ rw[EL_CONS, PRE_SUB1]
1152 \\ gvs[ADD1]
1153QED
1154
1155(* Evaluating first_byte_at at starting index 0w.
1156 Immediate corollary of first_byte_at_offset with m = 0. *)
1157Theorem first_byte_at_0w:
1158 0 < k /\ j < k /\ k <= dimword(:'a) ==>
1159 first_byte_at k j (0w:'a word) bs = if j < LENGTH bs then EL j bs else 0w
1160Proof
1161 rw[]
1162 \\ qspecl_then [`bs`, `0`] mp_tac first_byte_at_offset
1163 \\ simp[]
1164QED
1165
1166(* Connecting get_byte and word_of_bytes for big-endian.
1167 Note: both get_byte and set_byte with big-endian flag T access byte_index 8*(k-1-j)
1168 for address n2w j, so they operate on the same byte position. Therefore the
1169 first_byte_at lookup uses j directly, same as the little-endian case. *)
1170Theorem get_byte_word_of_bytes_be:
1171 ∀bs j a.
1172 8 <= dimindex(:'a) /\ j < dimindex(:'a) DIV 8 ==>
1173 get_byte (n2w j) (word_of_bytes T a bs : 'a word) T =
1174 first_byte_at (dimindex(:'a) DIV 8) j a bs
1175Proof
1176 Induct \\ rw[]
1177 >- rw[word_of_bytes_def, first_byte_at_def, get_byte_def]
1178 \\ rw[word_of_bytes_def]
1179 \\ Cases_on `j = w2n a MOD (dimindex (:'a) DIV 8)`
1180 >- (
1181 simp[first_byte_at_def] \\ gvs[]
1182 \\ qmatch_goalsub_abbrev_tac `get_byte a'`
1183 \\ qmatch_goalsub_abbrev_tac `set_byte a h w`
1184 \\ `set_byte a h w T = set_byte a' h w T`
1185 by ( irule set_byte_change_a \\ gvs[Abbr`a'`]
1186 \\ qmatch_goalsub_abbrev_tac `x = _`
1187 \\ qmatch_goalsub_abbrev_tac `x MOD k`
1188 \\ `x < k` by gvs[Abbr`k`, dimindex_lt_dimword, X_LT_DIV]
1189 \\ simp[LESS_MOD] )
1190 \\ rw[get_byte_set_byte] )
1191 \\ rw[first_byte_at_def]
1192 \\ reverse $ Cases_on `16 ≤ dimindex (:'a)`
1193 >- (
1194 gvs[X_LT_DIV] \\ Cases_on `j` \\ gvs[]
1195 \\ `1 ≤ dimindex (:'a) DIV 8` by gvs[X_LE_DIV]
1196 \\ `dimindex (:'a) DIV 8 ≤ 1` by gvs[DIV_LE_X]
1197 \\ `dimindex (:'a) DIV 8 = 1` by gvs[]
1198 \\ gvs[X_LT_DIV] )
1199 \\ DEP_REWRITE_TAC[get_byte_set_byte_irrelevant]
1200 \\ simp[]
1201 \\ gvs[LESS_MOD, X_LT_DIV, dimindex_lt_dimword]
1202QED
1203
1204(* get_byte extracts the right byte from a word (little-endian) *)
1205Theorem get_byte_n2w_le:
1206 8 <= dimindex(:'a) /\ i < dimindex(:'a) DIV 8 ==>
1207 get_byte (n2w i : 'a word) w F = n2w ((w2n w) DIV (256 ** i))
1208Proof
1209 rw[get_byte_def, byte_index_def]
1210 \\ gvs[LESS_MOD, dimindex_lt_dimword, X_LT_DIV]
1211 \\ rw[w2w_def, w2n_lsr, EXP_EXP_MULT]
1212QED
1213
1214(* get_byte extracts the right byte from a word (big-endian) *)
1215Theorem get_byte_n2w_be:
1216 8 <= dimindex(:'a) /\ i < dimindex(:'a) DIV 8 ==>
1217 get_byte (n2w i : 'a word) w T =
1218 n2w ((w2n w) DIV (256 ** (dimindex(:'a) DIV 8 - 1 - i)))
1219Proof
1220 rw[get_byte_def, byte_index_def]
1221 \\ gvs[LESS_MOD, dimindex_lt_dimword, X_LT_DIV]
1222 \\ rw[w2w_def, w2n_lsr, EXP_EXP_MULT]
1223QED
1224
1225(* Two words are equal if all their bytes are equal.
1226 Requires dimindex divisible by 8 so that bytes cover all bits. *)
1227Theorem word_eq_of_get_byte:
1228 8 <= dimindex(:'a) /\ divides 8 (dimindex(:'a)) ==>
1229 ((!j. j < dimindex(:'a) DIV 8 ==> get_byte (n2w j) w1 be = get_byte (n2w j) w2 be) ==>
1230 (w1:'a word) = w2)
1231Proof
1232 simp[GSYM WORD_EQ, word_bit_def]
1233 \\ ntac 2 strip_tac
1234 \\ qx_gen_tac`i` \\ strip_tac
1235 \\ qspec_then`8`mp_tac DIVISION
1236 \\ impl_tac >- rw[]
1237 \\ disch_then(qspec_then`i`strip_assume_tac)
1238 \\ `i DIV 8 < dimindex(:'a) DIV 8` by (
1239 gvs[X_LT_DIV,DIV_LT_X,MULT_DIV]
1240 \\ gvs[dividesTheory.DIV_MULT_EQ] )
1241 \\ `dimindex(:'a) DIV 8 - 1 - i DIV 8 < dimindex(:'a) DIV 8`
1242 by ( gvs[X_LT_DIV] \\ Cases_on`i DIV 8 = 0` \\ gvs[] \\ rw[X_LT_DIV] )
1243 \\ first_assum drule
1244 \\ pop_assum kall_tac
1245 \\ first_x_assum drule
1246 \\ disch_then drule \\ strip_tac
1247 \\ disch_then drule \\ strip_tac
1248 \\ qmatch_asmsub_abbrev_tac`j * 8 + r`
1249 \\ `r < 8` by rw[Abbr`r`]
1250 \\ Cases_on`be=F`
1251 >- (
1252 qpat_x_assum`get_byte (n2w j) _ _ ' _ = _`mp_tac
1253 \\ simp[get_byte_def, byte_index_def]
1254 \\ gvs[LESS_MOD, dimindex_lt_dimword]
1255 \\ simp[w2w, word_lsr_def]
1256 \\ srw_tac[wordsLib.WORD_BIT_EQ_ss][] )
1257 \\ gvs[]
1258 \\ qpat_x_assum`_ <=> _`mp_tac
1259 \\ qmatch_goalsub_abbrev_tac`k - _`
1260 \\ `k - 1 - j < k` by gvs[]
1261 \\ `k - 1 - j < dimword(:'a)` by gvs[Abbr`k`,DIV_LT_X,dimindex_lt_dimword]
1262 \\ `w2n(n2w(k - 1 - j)) = k - 1 - j` by simp[]
1263 \\ simp[get_byte_def, byte_index_def, word_lsr_def, w2w]
1264 \\ srw_tac[wordsLib.WORD_BIT_EQ_ss][]
1265QED
1266
1267Definition word_of_bytes_le_def:
1268 word_of_bytes_le = word_of_bytes F 0w
1269End
1270
1271Definition word_of_bytes_be_def:
1272 word_of_bytes_be = word_of_bytes T 0w
1273End
1274
1275Definition word_to_bytes_le_def:
1276 word_to_bytes_le w = word_to_bytes w F
1277End
1278
1279Definition word_to_bytes_be_def:
1280 word_to_bytes_be w = word_to_bytes w T
1281End