Theory byte

⊢ ∀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 = n2w (dimindex (:α) DIV 8)

⊢ (∀n. bytes_of_num 0 n = []) ∧
  ∀k n. bytes_of_num (SUC k) n = n2w n::bytes_of_num k (n DIV 256)

⊢ (∀k j a. first_byte_at k j a [] = 0w) ∧
  ∀k j a b bs.
    first_byte_at k j a (b::bs) =
    if w2n a MOD k = j then b else first_byte_at k j (a + 1w) bs

⊢ ∀a w is_bigendian.
    get_byte a w is_bigendian = w2w (w ⋙ byte_index a is_bigendian)

⊢ num_of_bytes [] = 0 ∧
  ∀b bs. num_of_bytes (b::bs) = w2n b + 256 * num_of_bytes bs

⊢ ∀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_be = word_of_bytes T 0w

⊢ (∀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_of_bytes_le = word_of_bytes F 0w

⊢ ∀h l w. word_slice_alt h l w = FCP i. l ≤ i ∧ i < h ∧ w ' i

⊢ (∀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]

⊢ ∀w. word_to_bytes_be w = word_to_bytes w T

⊢ ∀w be. word_to_bytes w be = word_to_bytes_aux (dimindex (:α) DIV 8) w be

⊢ ∀w. word_to_bytes_le w = word_to_bytes w F

⊢ 1 < d ⇒ (d ≤ n ⇔ 0 < n DIV d)

⊢ i < k ⇒ (bytes_of_num k n)❲i❳ = n2w (n DIV 256 ** i)

⊢ i < n ⇒ (word_to_bytes_aux n w be)❲i❳ = get_byte (n2w i) w be

⊢ ∀l res bs. LENGTH (be_bytes l res bs) = l + LENGTH res

⊢ ∀k n. LENGTH (bytes_of_num k n) = k

⊢ LENGTH (word_to_bytes w be) = dimindex (:α) DIV 8

⊢ LENGTH (word_to_bytes_aux n w b) = n

⊢ 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)

⊢ (∀res bs. be_bytes 0 res bs = res) ∧
  (∀res l.
     be_bytes (NUMERAL (BIT1 l)) res [] =
     be_bytes (NUMERAL (BIT1 l) − 1) (0w::res) []) ∧
  (∀res l.
     be_bytes (NUMERAL (BIT2 l)) res [] =
     be_bytes (NUMERAL (BIT1 l)) (0w::res) []) ∧
  (∀xs x res l.
     be_bytes (NUMERAL (BIT1 l)) res (x::xs) =
     be_bytes (NUMERAL (BIT1 l) − 1) (x::res) xs) ∧
  ∀xs x res l.
    be_bytes (NUMERAL (BIT2 l)) res (x::xs) =
    be_bytes (NUMERAL (BIT1 l)) (x::res) xs

⊢ (∀res bs. be_bytes 0 res bs = res) ∧
  (∀res l. be_bytes (SUC l) res [] = be_bytes l (0w::res) []) ∧
  ∀xs x res l. be_bytes (SUC l) res (x::xs) = be_bytes l (x::res) xs

⊢ ∀P. (∀res bs. P 0 res bs) ∧
      (∀l res. P l (0w::res) [] ⇒ P (SUC l) res []) ∧
      (∀l res x xs. P l (x::res) xs ⇒ P (SUC l) res (x::xs)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀l res bs.
    be_bytes l res bs = REVERSE (TAKE l (bs ⧺ REPLICATE l 0w)) ⧺ res

⊢ l1 ≤ h2 ∧ l2 ≤ SUC h1 ⇒
  bit_field_insert h1 l1 (w ⋙ l1) (word_slice_alt h2 l2 w) =
  word_slice_alt (MAX (SUC h1) h2) (MIN l1 l2) w

⊢ 8 ≤ dimindex (:α) ⇒
  byte_index (n2w (w2n a MOD (dimindex (:α) DIV 8))) be = byte_index a be

⊢ w2n n MOD (dimindex (:α) DIV 8) ≠ w2n m MOD (dimindex (:α) DIV 8) ∧
  8 ≤ dimindex (:α) ⇒
  byte_index n be + 8 ≤ byte_index m be ∨
  byte_index m be + 8 ≤ byte_index n be

⊢ 8 ≤ dimindex (:α) ⇒ byte_index a be + 8 ≤ dimindex (:α)

⊢ (∀n. bytes_of_num 0 n = []) ∧
  (∀k n.
     bytes_of_num (NUMERAL (BIT1 k)) n =
     n2w n::bytes_of_num (NUMERAL (BIT1 k) − 1) (n DIV 256)) ∧
  ∀k n.
    bytes_of_num (NUMERAL (BIT2 k)) n =
    n2w n::bytes_of_num (NUMERAL (BIT1 k)) (n DIV 256)

⊢ ∀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 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

⊢ ∀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

⊢ ∀bw k b1 w be b2.
    (∀n. n < bw ⇒ n < LENGTH b1 ∧ n < LENGTH b2 ∧ b1❲n❳ = b2❲n❳) ⇒
    bytes_to_word bw k b1 w be = bytes_to_word bw k b2 w be

⊢ 0 < k ∧ j < k ∧ k ≤ dimword (:α) ⇒
  first_byte_at k j 0w bs = if j < LENGTH bs then bs❲j❳ else 0w

⊢ ∀bs m k j.
    0 < k ∧ j < k ∧ m < k ∧ m ≤ j ∧ k ≤ dimword (:α) ⇒
    first_byte_at k j (n2w m) bs =
    if j − m < LENGTH bs then bs❲j − m❳ else 0w

⊢ 8 ≤ dimindex (:α) ⇒
  get_byte (n2w (w2n a MOD (dimindex (:α) DIV 8))) w be = get_byte a w be

⊢ 8 ≤ dimindex (:α) ∧ i < dimindex (:α) DIV 8 ⇒
  get_byte (n2w i) w T =
  n2w (w2n w DIV 256 ** (dimindex (:α) DIV 8 − 1 − i))

⊢ 8 ≤ dimindex (:α) ∧ i < dimindex (:α) DIV 8 ⇒
  get_byte (n2w i) w F = n2w (w2n w DIV 256 ** i)

⊢ 8 ≤ dimindex (:α) ⇒ get_byte a (set_byte a b w be) be = b

⊢ 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

⊢ ∀bs j a.
    8 ≤ dimindex (:α) ∧ j < dimindex (:α) DIV 8 ⇒
    get_byte (n2w j) (word_of_bytes T a bs) T =
    first_byte_at (dimindex (:α) DIV 8) j a bs

⊢ ∀bs j a.
    8 ≤ dimindex (:α) ∧ j < dimindex (:α) DIV 8 ⇒
    get_byte (n2w j) (word_of_bytes F a bs) F =
    first_byte_at (dimindex (:α) DIV 8) j a bs

⊢ ∀xs ys.
    num_of_bytes (xs ⧺ ys) =
    num_of_bytes xs + 256 ** LENGTH xs * num_of_bytes ys

⊢ ∀bs j.
    num_of_bytes bs DIV 256 ** j MOD 256 =
    if j < LENGTH bs then w2n bs❲j❳ else 0

⊢ ∀n. num_of_bytes (REPLICATE n 0w) = 0

⊢ 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 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 a b w be =
  bit_field_insert (byte_index a be + 7) (byte_index a be) b w

⊢ w2n a MOD (dimindex (:α) DIV 8) = w2n a' MOD (dimindex (:α) DIV 8) ⇒
  set_byte a b w be = set_byte a' b w be

⊢ 8 ≤ dimindex (:α) ⇒
  set_byte (n2w (w2n a MOD (dimindex (:α) DIV 8))) b w be =
  set_byte a b w be

⊢ (∀j. j < 8 ⇒ ¬w ' (byte_index ix bige + j)) ⇒
  set_byte ix b w bige = w ‖ w2w b ≪ byte_index ix bige

⊢ 8 ≤ dimindex (:α) ⇒ set_byte a (get_byte a w be) w be = w

⊢ 8 ≤ dimindex (:α) ⇒ set_byte a (get_byte a w be) w be = w

⊢ 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'

⊢ w2n n MOD (dimindex (:α) DIV 8) ≠ w2n m MOD (dimindex (:α) DIV 8) ∧
  8 ≤ dimindex (:α) ⇒
  set_byte n x (set_byte m y w be) be = set_byte m y (set_byte n x w be) be

⊢ 8 ≤ dimindex (:α) ∧ divides 8 (dimindex (:α)) ⇒
  (∀j. j < dimindex (:α) DIV 8 ⇒
       get_byte (n2w j) w1 be = get_byte (n2w j) w2 be) ⇒
  w1 = w2

⊢ LENGTH bs < dimindex (:α) DIV 8 ∧ w2n n + LENGTH bs < dimword (:α) ⇒
  word_of_bytes be n (SNOC b bs) =
  set_byte (n + n2w (LENGTH bs)) b (word_of_bytes be n bs) be

⊢ ∀be a bs k.
    LENGTH bs ≤ k ⇒ word_of_bytes be a bs = bytes_to_word k a bs 0w be

⊢ ∀bs ix.
    (w2n ix + LENGTH bs) * 8 ≤ dimindex (:α) ∧
    EVERYi (λi _0. ix + n2w i ≠ -1w) bs ⇒
    word_of_bytes F ix bs =
    FOLDRi (λi b w. w2w b ≪ ((w2n ix + i) * 8) ‖ w) 0w bs

⊢ 8 ≤ dimindex (:α) ∧ divides 8 (dimindex (:α)) ⇒
  word_of_bytes be 0w (word_to_bytes w be) = w

⊢ n ≤ dimindex (:α) DIV 8 ∧ 8 ≤ dimindex (:α) ⇒
  word_of_bytes T 0w (word_to_bytes_aux n w T) =
  word_slice_alt (8 * (dimindex (:α) DIV 8))
    (8 * (dimindex (:α) DIV 8 − n)) w

⊢ n ≤ dimindex (:α) DIV 8 ∧ 8 ≤ dimindex (:α) ⇒
  word_of_bytes F 0w (word_to_bytes_aux n w F) = word_slice_alt (8 * n) 0 w

⊢ h ≤ l ⇒ word_slice_alt h l w = 0w

⊢ dimindex (:α) ≤ h ⇒ word_slice_alt h 0 w = w

⊢ h ≤ dimindex (:α) ⇒
  word_slice_alt h l w =
  w ⋙ l ≪ l ≪ (dimindex (:α) − h) ⋙ (dimindex (:α) − h)

⊢ h ≤ dimindex (:α) ⇒ word_slice_alt (SUC h) l w = (h '' l) w

⊢ word_slice_alt h l 0w = 0w

⊢ h < dimindex (:α) ⇒
  (h '' l) w =
  w ⋙ l ≪ l ≪ (dimindex (:α) − SUC h) ⋙ (dimindex (:α) − SUC h)

⊢ (∀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_of_bytes be 0w (word_to_bytes w be) = w

⊢ word_of_bytes be 0w (word_to_bytes w be) = w

⊢ 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

⊢ 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

⊢ (∀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)

⊢ ∀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