Structure byteTheory
signature byteTheory =
sig
type thm = Thm.thm
(* Definitions *)
val byte_index_def : thm
val bytes_in_word_def : thm
val get_byte_def : thm
val set_byte_def : thm
val word_of_bytes_def : thm
val word_slice_alt_def : thm
val word_to_bytes_aux_def : thm
val word_to_bytes_def : thm
(* Theorems *)
val DIV_not_0 : thm
val LENGTH_words_of_bytes : thm
val byte_index_cycle : thm
val byte_index_offset : thm
val bytes_to_word_def : thm
val bytes_to_word_eq : thm
val bytes_to_word_ind : thm
val bytes_to_word_same : thm
val get_byte_cycle : thm
val get_byte_set_byte : thm
val get_byte_set_byte_irrelevant : thm
val set_byte_32 : thm
val set_byte_64 : thm
val set_byte_change_a : thm
val set_byte_cycle : thm
val set_byte_get_byte : thm
val set_byte_get_byte' : thm
val set_byte_get_byte_copy : thm
val word_of_bytes_bytes_to_word : thm
val word_slice_alt_shift : thm
val word_slice_alt_word_slice : thm
val word_slice_alt_zero : thm
val word_slice_shift : thm
val word_to_bytes_aux_compute : thm
val word_to_bytes_word_of_bytes_32 : thm
val word_to_bytes_word_of_bytes_64 : thm
val words_of_bytes_append : thm
val words_of_bytes_append_word : thm
val words_of_bytes_def : thm
val words_of_bytes_ind : thm
val byte_grammars : type_grammar.grammar * term_grammar.grammar
(*
[bitstring] Parent theory of "byte"
[blast] Parent theory of "byte"
[byte_index_def] Definition
⊢ ∀a is_bigendian.
byte_index a is_bigendian =
(let
d = dimindex (:α) DIV 8
in
if is_bigendian then 8 * (d − 1 − w2n a MOD d)
else 8 * w2n a MOD d)
[bytes_in_word_def] Definition
⊢ bytes_in_word = n2w (dimindex (:α) DIV 8)
[get_byte_def] Definition
⊢ ∀a w is_bigendian.
get_byte a w is_bigendian = w2w (w ⋙ byte_index a is_bigendian)
[set_byte_def] Definition
⊢ ∀a b w is_bigendian.
set_byte a b w is_bigendian =
(let
i = byte_index a is_bigendian
in
word_slice_alt (dimindex (:α)) (i + 8) w ‖ w2w b ≪ i ‖
word_slice_alt i 0 w)
[word_of_bytes_def] Definition
⊢ (∀be a. word_of_bytes be a [] = 0w) ∧
∀be a b bs.
word_of_bytes be a (b::bs) =
set_byte a b (word_of_bytes be (a + 1w) bs) be
[word_slice_alt_def] Definition
⊢ ∀h l w. word_slice_alt h l w = FCP i. l ≤ i ∧ i < h ∧ w ' i
[word_to_bytes_aux_def] Definition
⊢ (∀w be. word_to_bytes_aux 0 w be = []) ∧
∀n w be.
word_to_bytes_aux (SUC n) w be =
word_to_bytes_aux n w be ⧺ [get_byte (n2w n) w be]
[word_to_bytes_def] Definition
⊢ ∀w be.
word_to_bytes w be = word_to_bytes_aux (dimindex (:α) DIV 8) w be
[DIV_not_0] Theorem
⊢ 1 < d ⇒ (d ≤ n ⇔ 0 < n DIV d)
[LENGTH_words_of_bytes] Theorem
⊢ 8 ≤ dimindex (:α) ⇒
∀be ls.
LENGTH (words_of_bytes be ls) =
LENGTH ls DIV w2n bytes_in_word +
MIN 1 (LENGTH ls MOD w2n bytes_in_word)
[byte_index_cycle] Theorem
⊢ 8 ≤ dimindex (:α) ⇒
byte_index (n2w (w2n a MOD (dimindex (:α) DIV 8))) be =
byte_index a be
[byte_index_offset] Theorem
⊢ 8 ≤ dimindex (:α) ⇒ byte_index a be + 8 ≤ dimindex (:α)
[bytes_to_word_def] Theorem
⊢ ∀w k bs be a.
bytes_to_word k a bs w be =
if k = 0 then w
else
case bs of
[] => w
| b::bs' =>
set_byte a b (bytes_to_word (k − 1) (a + 1w) bs' w be) be
[bytes_to_word_eq] Theorem
⊢ bytes_to_word 0 a bs w be = w ∧ bytes_to_word k a [] w be = w ∧
bytes_to_word (SUC k) a (b::bs) w be =
set_byte a b (bytes_to_word k (a + 1w) bs w be) be
[bytes_to_word_ind] Theorem
⊢ ∀P. (∀k a bs w be.
(∀b bs'. k ≠ 0 ∧ bs = b::bs' ⇒ P (k − 1) (a + 1w) bs' w be) ⇒
P k a bs w be) ⇒
∀v v1 v2 v3 v4. P v v1 v2 v3 v4
[bytes_to_word_same] Theorem
⊢ ∀bw k b1 w be b2.
(∀n. n < bw ⇒ n < LENGTH b1 ∧ n < LENGTH b2 ∧ EL n b1 = EL n b2) ⇒
bytes_to_word bw k b1 w be = bytes_to_word bw k b2 w be
[get_byte_cycle] Theorem
⊢ 8 ≤ dimindex (:α) ⇒
get_byte (n2w (w2n a MOD (dimindex (:α) DIV 8))) w be =
get_byte a w be
[get_byte_set_byte] Theorem
⊢ 8 ≤ dimindex (:α) ⇒ get_byte a (set_byte a b w be) be = b
[get_byte_set_byte_irrelevant] Theorem
⊢ 16 ≤ dimindex (:α) ∧
w2n a MOD (dimindex (:α) DIV 8) ≠ w2n a' MOD (dimindex (:α) DIV 8) ⇒
get_byte a' (set_byte a b w be) be = get_byte a' w be
[set_byte_32] Theorem
⊢ set_byte a b w be =
(let
i = byte_index a be
in
if i = 0 then w2w b ‖ w && 0xFFFFFF00w
else if i = 8 then w2w b ≪ 8 ‖ w && 0xFFFF00FFw
else if i = 16 then w2w b ≪ 16 ‖ w && 0xFF00FFFFw
else w2w b ≪ 24 ‖ w && 0xFFFFFFw)
[set_byte_64] Theorem
⊢ set_byte a b w be =
(let
i = byte_index a be
in
if i = 0 then w2w b ‖ w && 0xFFFFFFFFFFFFFF00w
else if i = 8 then w2w b ≪ 8 ‖ w && 0xFFFFFFFFFFFF00FFw
else if i = 16 then w2w b ≪ 16 ‖ w && 0xFFFFFFFFFF00FFFFw
else if i = 24 then w2w b ≪ 24 ‖ w && 0xFFFFFFFF00FFFFFFw
else if i = 32 then w2w b ≪ 32 ‖ w && 0xFFFFFF00FFFFFFFFw
else if i = 40 then w2w b ≪ 40 ‖ w && 0xFFFF00FFFFFFFFFFw
else if i = 48 then w2w b ≪ 48 ‖ w && 0xFF00FFFFFFFFFFFFw
else w2w b ≪ 56 ‖ w && 0xFFFFFFFFFFFFFFw)
[set_byte_change_a] Theorem
⊢ w2n a MOD (dimindex (:α) DIV 8) = w2n a' MOD (dimindex (:α) DIV 8) ⇒
set_byte a b w be = set_byte a' b w be
[set_byte_cycle] Theorem
⊢ 8 ≤ dimindex (:α) ⇒
set_byte (n2w (w2n a MOD (dimindex (:α) DIV 8))) b w be =
set_byte a b w be
[set_byte_get_byte] Theorem
⊢ 8 ≤ dimindex (:α) ⇒ set_byte a (get_byte a w be) w be = w
[set_byte_get_byte'] Theorem
⊢ 8 ≤ dimindex (:α) ⇒ set_byte a (get_byte a w be) w be = w
[set_byte_get_byte_copy] Theorem
⊢ 8 ≤ dimindex (:α) ⇒
set_byte a (get_byte a w be) w' be =
(byte_index a be + 7 '' byte_index a be) w ‖
(if byte_index a be + 8 = dimindex (:α) then 0w
else (dimindex (:α) − 1 '' byte_index a be + 8) w') ‖
if byte_index a be = 0 then 0w else (byte_index a be − 1 '' 0) w'
[word_of_bytes_bytes_to_word] Theorem
⊢ ∀be a bs k.
LENGTH bs ≤ k ⇒
word_of_bytes be a bs = bytes_to_word k a bs 0w be
[word_slice_alt_shift] Theorem
⊢ h ≤ dimindex (:α) ⇒
word_slice_alt h l w =
w ⋙ l ≪ l ≪ (dimindex (:α) − h) ⋙ (dimindex (:α) − h)
[word_slice_alt_word_slice] Theorem
⊢ h ≤ dimindex (:α) ⇒ word_slice_alt (SUC h) l w = (h '' l) w
[word_slice_alt_zero] Theorem
⊢ word_slice_alt h l 0w = 0w
[word_slice_shift] Theorem
⊢ h < dimindex (:α) ⇒
(h '' l) w =
w ⋙ l ≪ l ≪ (dimindex (:α) − SUC h) ⋙ (dimindex (:α) − SUC h)
[word_to_bytes_aux_compute] Theorem
⊢ (∀w be. word_to_bytes_aux 0 w be = []) ∧
(∀n w be.
word_to_bytes_aux (NUMERAL (BIT1 n)) w be =
word_to_bytes_aux (NUMERAL (BIT1 n) − 1) w be ⧺
[get_byte (n2w (NUMERAL (BIT1 n) − 1)) w be]) ∧
∀n w be.
word_to_bytes_aux (NUMERAL (BIT2 n)) w be =
word_to_bytes_aux (NUMERAL (BIT1 n)) w be ⧺
[get_byte (n2w (NUMERAL (BIT1 n))) w be]
[word_to_bytes_word_of_bytes_32] Theorem
⊢ word_of_bytes be 0w (word_to_bytes w be) = w
[word_to_bytes_word_of_bytes_64] Theorem
⊢ word_of_bytes be 0w (word_to_bytes w be) = w
[words_of_bytes_append] Theorem
⊢ 0 < w2n bytes_in_word ⇒
∀l1 l2.
LENGTH l1 MOD w2n bytes_in_word = 0 ⇒
words_of_bytes be (l1 ⧺ l2) =
words_of_bytes be l1 ⧺ words_of_bytes be l2
[words_of_bytes_append_word] Theorem
⊢ 0 < LENGTH l1 ∧ LENGTH l1 = w2n bytes_in_word ⇒
words_of_bytes be (l1 ⧺ l2) =
word_of_bytes be 0w l1::words_of_bytes be l2
[words_of_bytes_def] Theorem
⊢ (∀be. words_of_bytes be [] = []) ∧
∀v3 v2 be.
words_of_bytes be (v2::v3) =
(let
xs = TAKE (MAX 1 (w2n bytes_in_word)) (v2::v3);
ys = DROP (MAX 1 (w2n bytes_in_word)) (v2::v3)
in
word_of_bytes be 0w xs::words_of_bytes be ys)
[words_of_bytes_ind] Theorem
⊢ ∀P. (∀be. P be []) ∧
(∀be v2 v3.
(∀xs ys.
xs = TAKE (MAX 1 (w2n bytes_in_word)) (v2::v3) ∧
ys = DROP (MAX 1 (w2n bytes_in_word)) (v2::v3) ⇒
P be ys) ⇒
P be (v2::v3)) ⇒
∀v v1. P v v1
*)
end
HOL 4, Trindemossen-1