Theory "bitstring"

Signature

Definitions

extend_def

⊢ (∀v0 l. extend v0 0 l = l) ∧ ∀c n l. extend c (SUC n) l = extend c n (c::l)

boolify_def

⊢ (∀a. boolify a [] = a) ∧ ∀a n l. boolify a (n::l) = boolify ((n ≠ 0)::a) l

n2v_def

⊢ ∀n. n2v n = boolify [] (num_to_bin_list n)

v2n_def

⊢ ∀l. v2n l = num_from_bin_list (bitify [] l)

s2v_def

⊢ s2v = MAP (λc. c = #"1" ∨ c = #"T")

v2s_def

⊢ v2s = MAP (λb. if b then #"1" else #"0")

zero_extend_def

⊢ ∀n v. zero_extend n v = PAD_LEFT F n v

sign_extend_def

⊢ ∀n v. sign_extend n v = PAD_LEFT (HD v) n v

fixwidth_def

⊢ ∀n v.
      fixwidth n v =
      (let l = LENGTH v in if l < n then zero_extend n v else DROP (l − n) v)

shiftl_def

⊢ ∀v m. shiftl v m = PAD_RIGHT F (LENGTH v + m) v

shiftr_def

⊢ ∀v m. shiftr v m = TAKE (LENGTH v − m) v

field_def

⊢ ∀h l v. field h l v = fixwidth (SUC h − l) (shiftr v l)

rotate_def

⊢ ∀v m.
      rotate v m =
      (let
         l = LENGTH v ;
         x = m MOD l
       in
         if l = 0 ∨ x = 0 then v else field (x − 1) 0 v ++ field (l − 1) x v)

testbit_def

⊢ ∀b v. testbit b v ⇔ field b b v = [T]

w2v_def

⊢ ∀w. w2v w = GENLIST (λi. w ' (dimindex (:α) − 1 − i)) (dimindex (:α))

v2w_def

⊢ ∀v. v2w v = FCP i. testbit i v

rev_count_list_def

⊢ ∀n. rev_count_list n = GENLIST (λi. n − 1 − i) n

modify_def

⊢ ∀f v. modify f v = MAP (UNCURRY f) (ZIP (rev_count_list (LENGTH v),v))

field_insert_def

⊢ ∀h l s.
      field_insert h l s =
      modify (λi. COND (l ≤ i ∧ i ≤ h) (testbit (i − l) s))

add_def

⊢ ∀a b.
      add a b =
      (let
         m = MAX (LENGTH a) (LENGTH b)
       in
         zero_extend m (n2v (v2n a + v2n b)))

bitwise_def

⊢ ∀f v1 v2.
      bitwise f v1 v2 =
      (let
         m = MAX (LENGTH v1) (LENGTH v2)
       in
         MAP (UNCURRY f) (ZIP (fixwidth m v1,fixwidth m v2)))

bnot_def

⊢ bnot = MAP $~

bor_def

⊢ bor = bitwise $\/

band_def

⊢ band = bitwise $/\

bxor_def

⊢ bxor = bitwise (λx y. x ⇎ y)

bnor_def

⊢ bnor = bitwise (λx y. ¬(x ∨ y))

bxnor_def

⊢ bxnor = bitwise $<=>

bnand_def

⊢ bnand = bitwise (λx y. ¬(x ∧ y))

replicate_def

⊢ ∀v n. replicate v n = FLAT (GENLIST (K v) n)

Theorems

extend_def_compute

⊢ (∀v0 l. extend v0 0 l = l) ∧
  (∀c n l.
       extend c (NUMERAL (BIT1 n)) l = extend c (NUMERAL (BIT1 n) − 1) (c::l)) ∧
  ∀c n l. extend c (NUMERAL (BIT2 n)) l = extend c (NUMERAL (BIT1 n)) (c::l)

bitify_ind

⊢ ∀P.
      (∀a. P a []) ∧ (∀a l. P (0::a) l ⇒ P a (F::l)) ∧
      (∀a l. P (1::a) l ⇒ P a (T::l)) ⇒
      ∀v v1. P v v1

bitify_def

⊢ (∀a. bitify a [] = a) ∧ (∀l a. bitify a (F::l) = bitify (0::a) l) ∧
  ∀l a. bitify a (T::l) = bitify (1::a) l

extend_cons

⊢ ∀n c l. extend c (SUC n) l = c::extend c n l

pad_left_extend

⊢ ∀n l c. PAD_LEFT c n l = extend c (n − LENGTH l) l

extend

⊢ (∀n v. zero_extend n v = extend F (n − LENGTH v) v) ∧
  ∀n v. sign_extend n v = extend (HD v) (n − LENGTH v) v

fixwidth

⊢ ∀n v.
      fixwidth n v =
      (let
         l = LENGTH v
       in
         if l < n then extend F (n − l) v else DROP (l − n) v)

fixwidth_id

⊢ ∀w. fixwidth (LENGTH w) w = w

fixwidth_id_imp

⊢ ∀n w. n = LENGTH w ⇒ fixwidth n w = w

boolify_reverse_map

⊢ ∀v a. boolify a v = REVERSE (MAP (λn. n ≠ 0) v) ++ a

bitify_reverse_map

⊢ ∀v a. bitify a v = REVERSE (MAP (λb. if b then 1 else 0) v) ++ a

every_bit_bitify

⊢ ∀v. EVERY ($> 2) (bitify [] v)

length_pad_left

⊢ ∀x n a. LENGTH (PAD_LEFT x n a) = if LENGTH a < n then n else LENGTH a

length_pad_right

⊢ ∀x n a. LENGTH (PAD_RIGHT x n a) = if LENGTH a < n then n else LENGTH a

length_zero_extend

⊢ ∀n v. LENGTH v < n ⇒ LENGTH (zero_extend n v) = n

length_sign_extend

⊢ ∀n v. LENGTH v < n ⇒ LENGTH (sign_extend n v) = n

length_fixwidth

⊢ ∀n v. LENGTH (fixwidth n v) = n

length_field

⊢ ∀h l v. LENGTH (field h l v) = SUC h − l

length_bitify

⊢ ∀v l. LENGTH (bitify l v) = LENGTH l + LENGTH v

length_bitify_null

⊢ ∀v l. LENGTH (bitify [] v) = LENGTH v

length_shiftr

⊢ ∀v n. LENGTH (shiftr v n) = LENGTH v − n

length_rev_count_list

⊢ ∀n. LENGTH (rev_count_list n) = n

length_w2v

⊢ ∀w. LENGTH (w2v w) = dimindex (:α)

length_rotate

⊢ ∀v n. LENGTH (rotate v n) = LENGTH v

el_rev_count_list

⊢ ∀n i. i < n ⇒ EL i (rev_count_list n) = n − 1 − i

el_zero_extend

⊢ ∀n i v.
      EL i (zero_extend n v) ⇔ n − LENGTH v ≤ i ∧ EL (i − (n − LENGTH v)) v

el_sign_extend

⊢ ∀n i v.
      EL i (sign_extend n v) = if i < n − LENGTH v then EL 0 v
      else EL (i − (n − LENGTH v)) v

el_fixwidth

⊢ ∀i n w.
      i < n ⇒
      (EL i (fixwidth n w) ⇔
       if LENGTH w < n then n − LENGTH w ≤ i ∧ EL (i − (n − LENGTH w)) w
       else EL (i + (LENGTH w − n)) w)

el_field

⊢ ∀v h l i.
      i < SUC h − l ⇒
      (EL i (field h l v) ⇔ SUC h ≤ i + LENGTH v ∧ EL (i + LENGTH v − SUC h) v)

el_w2v

⊢ ∀w n. n < dimindex (:α) ⇒ (EL n (w2v w) ⇔ w ' (dimindex (:α) − 1 − n))

el_shiftr

⊢ ∀i v n d.
      n < d ∧ i < d − n ∧ 0 < d ⇒
      (EL i (shiftr (fixwidth d v) n) ⇔
       d ≤ i + LENGTH v ∧ EL (i + LENGTH v − d) v)

shiftr_0

⊢ ∀v. shiftr v 0 = v

field_fixwidth

⊢ ∀h v. field h 0 v = fixwidth (SUC h) v

testbit

⊢ ∀b v. testbit b v ⇔ (let n = LENGTH v in b < n ∧ EL (n − 1 − b) v)

testbit_geq_len

⊢ ∀v i. LENGTH v ≤ i ⇒ ¬testbit i v

testbit_el

⊢ ∀v i. i < LENGTH v ⇒ (testbit i v ⇔ EL (LENGTH v − 1 − i) v)

bit_v2w

⊢ ∀n v. word_bit n (v2w v) ⇔ n < dimindex (:α) ∧ testbit n v

word_index_v2w

⊢ ∀v i.
      v2w v ' i ⇔ if i < dimindex (:α) then testbit i v
      else FAIL $' index too large (v2w v) i

testbit_w2v

⊢ ∀n w. testbit n (w2v w) ⇔ word_bit n w

w2v_v2w

⊢ ∀v. w2v (v2w v) = fixwidth (dimindex (:α)) v

v2w_w2v

⊢ ∀w. v2w (w2v w) = w

v2w_fixwidth

⊢ ∀v. v2w (fixwidth (dimindex (:α)) v) = v2w v

fixwidth_fixwidth

⊢ ∀n v. fixwidth n (fixwidth n v) = fixwidth n v

bitstring_nchotomy

⊢ ∀w. ∃v. w = v2w v

ranged_bitstring_nchotomy

⊢ ∀w. ∃v. w = v2w v ∧ Abbrev (LENGTH v = dimindex (:α))

fixwidth_eq

⊢ ∀n v w.
      fixwidth n v = fixwidth n w ⇔ ∀i. i < n ⇒ (testbit i v ⇔ testbit i w)

v2w_11

⊢ ∀v w.
      v2w v = v2w w ⇔ fixwidth (dimindex (:α)) v = fixwidth (dimindex (:α)) w

field_concat_right

⊢ ∀h a b. LENGTH b = SUC h ⇒ field h 0 (a ++ b) = b

field_concat_left

⊢ ∀h l a b.
      l ≤ h ∧ LENGTH b ≤ l ⇒
      field h l (a ++ b) = field (h − LENGTH b) (l − LENGTH b) a

field_id_imp

⊢ ∀n v. SUC n = LENGTH v ⇒ field n 0 v = v

shiftl_replicate_F

⊢ ∀v n. shiftl v n = v ++ replicate [F] n

word_lsb_v2w

⊢ ∀v. word_lsb (v2w v) ⇔ v ≠ [] ∧ LAST v

word_msb_v2w

⊢ ∀v. word_msb (v2w v) ⇔ testbit (dimindex (:α) − 1) v

w2w_v2w

⊢ ∀v.
      w2w (v2w v) =
      v2w
        (fixwidth
           (if dimindex (:β) < dimindex (:α) then dimindex (:β)
            else dimindex (:α)) v)

sw2sw_v2w

⊢ ∀v.
      sw2sw (v2w v) =
      if dimindex (:α) < dimindex (:β) then
        v2w (sign_extend (dimindex (:β)) (fixwidth (dimindex (:α)) v))
      else v2w (fixwidth (dimindex (:β)) v)

n2w_v2n

⊢ ∀v. n2w (v2n v) = v2w v

v2n_n2v

⊢ ∀n. v2n (n2v n) = n

v2w_n2v

⊢ ∀n. v2w (n2v n) = n2w n

w2n_v2w

⊢ ∀v. w2n (v2w v) = MOD_2EXP (dimindex (:α)) (v2n v)

v2n_lt

⊢ ∀v. v2n v < 2 ** LENGTH v

word_and_v2w

⊢ ∀v w. (v2w v && v2w w) = v2w (band v w)

word_or_v2w

⊢ ∀v w. (v2w v ‖ v2w w) = v2w (bor v w)

word_xor_v2w

⊢ ∀v w. (v2w v ⊕ v2w w) = v2w (bxor v w)

word_nand_v2w

⊢ ∀v w.
      (v2w v ~&& v2w w) =
      v2w (bnand (fixwidth (dimindex (:α)) v) (fixwidth (dimindex (:α)) w))

word_nor_v2w

⊢ ∀v w.
      (v2w v ~|| v2w w) =
      v2w (bnor (fixwidth (dimindex (:α)) v) (fixwidth (dimindex (:α)) w))

word_xnor_v2w

⊢ ∀v w.
      (v2w v ~?? v2w w) =
      v2w (bxnor (fixwidth (dimindex (:α)) v) (fixwidth (dimindex (:α)) w))

word_1comp_v2w

⊢ ∀v. ¬v2w v = v2w (bnot (fixwidth (dimindex (:α)) v))

word_lsl_v2w

⊢ ∀n v. v2w v ≪ n = v2w (shiftl v n)

word_lsr_v2w

⊢ ∀n v. v2w v ⋙ n = v2w (shiftr (fixwidth (dimindex (:α)) v) n)

word_modify_v2w

⊢ ∀f v. word_modify f (v2w v) = v2w (modify f (fixwidth (dimindex (:α)) v))

word_bits_v2w

⊢ ∀h l v. (h -- l) (v2w v) = v2w (field h l (fixwidth (dimindex (:α)) v))

word_extract_v2w

⊢ ∀h l v. (h >< l) (v2w v) = w2w ((h -- l) (v2w v))

word_slice_v2w

⊢ ∀h l v.
      (h '' l) (v2w v) =
      v2w (shiftl (field h l (fixwidth (dimindex (:α)) v)) l)

word_asr_v2w

⊢ ∀n v.
      v2w v ≫ n =
      (let
         l = fixwidth (dimindex (:α)) v
       in
         v2w
           (sign_extend (dimindex (:α))
              (if dimindex (:α) ≤ n then [HD l] else shiftr l n)))

word_ror_v2w

⊢ ∀n v. v2w v ⇄ n = v2w (rotate (fixwidth (dimindex (:α)) v) n)

word_reverse_v2w

⊢ ∀v. word_reverse (v2w v) = v2w (REVERSE (fixwidth (dimindex (:α)) v))

word_join_v2w

⊢ ∀v1 v2.
      FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) ⇒
      word_join (v2w v1) (v2w v2) = v2w (v1 ++ fixwidth (dimindex (:β)) v2)

word_concat_v2w

⊢ ∀v1 v2.
      FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) ⇒
      v2w v1 @@ v2w v2 =
      v2w
        (fixwidth (MIN (dimindex (:γ)) (dimindex (:α) + dimindex (:β)))
           (v1 ++ fixwidth (dimindex (:β)) v2))

word_join_v2w_rwt

⊢ ∀v1 v2.
      word_join (v2w v1) (v2w v2) =
      if FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) then
        v2w (v1 ++ fixwidth (dimindex (:β)) v2)
      else FAIL word_join bad domain (v2w v1) (v2w v2)

word_concat_v2w_rwt

⊢ ∀v1 v2.
      v2w v1 @@ v2w v2 =
      if FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) then
        v2w
          (fixwidth (MIN (dimindex (:γ)) (dimindex (:α) + dimindex (:β)))
             (v1 ++ fixwidth (dimindex (:β)) v2))
      else FAIL $@@ bad domain (v2w v1) (v2w v2)

word_reduce_v2w

⊢ ∀f v.
      word_reduce f (v2w v) =
      (let l = fixwidth (dimindex (:α)) v in v2w [FOLDL f (HD l) (TL l)])

reduce_and_v2w

⊢ ∀v. reduce_and (v2w v) = word_reduce $/\ (v2w v)

reduce_or_v2w

⊢ ∀v. reduce_or (v2w v) = word_reduce $\/ (v2w v)

extract_v2w

⊢ ∀h l v.
      LENGTH v ≤ dimindex (:α) ∧ dimindex (:β) = SUC h − l ∧
      dimindex (:β) ≤ dimindex (:α) ⇒
      (h >< l) (v2w v) = v2w (field h l v)

word_bit_last_shiftr

⊢ ∀i v.
      i < dimindex (:α) ⇒
      (word_bit i (v2w v) ⇔ (let l = shiftr v i in ¬NULL l ∧ LAST l))

ops_to_v2w

⊢ (∀v n. (v2w v ‖ n2w n) = (v2w v ‖ v2w (n2v n))) ∧
  (∀v n. (n2w n ‖ v2w v) = (v2w (n2v n) ‖ v2w v)) ∧
  (∀v n. (v2w v && n2w n) = (v2w v && v2w (n2v n))) ∧
  (∀v n. (n2w n && v2w v) = (v2w (n2v n) && v2w v)) ∧
  (∀v n. (v2w v ⊕ n2w n) = (v2w v ⊕ v2w (n2v n))) ∧
  (∀v n. (n2w n ⊕ v2w v) = (v2w (n2v n) ⊕ v2w v)) ∧
  (∀v n. (v2w v ~|| n2w n) = (v2w v ~|| v2w (n2v n))) ∧
  (∀v n. (n2w n ~|| v2w v) = (v2w (n2v n) ~|| v2w v)) ∧
  (∀v n. (v2w v ~&& n2w n) = (v2w v ~&& v2w (n2v n))) ∧
  (∀v n. (n2w n ~&& v2w v) = (v2w (n2v n) ~&& v2w v)) ∧
  (∀v n. (v2w v ~?? n2w n) = (v2w v ~?? v2w (n2v n))) ∧
  (∀v n. (n2w n ~?? v2w v) = (v2w (n2v n) ~?? v2w v)) ∧
  (∀v n. v2w v @@ n2w n = v2w v @@ v2w (n2v n)) ∧
  (∀v n. n2w n @@ v2w v = v2w (n2v n) @@ v2w v) ∧
  (∀v n. word_join (v2w v) (n2w n) = word_join (v2w v) (v2w (n2v n))) ∧
  ∀v n. word_join (n2w n) (v2w v) = word_join (v2w (n2v n)) (v2w v)

ops_to_n2w

⊢ (∀v. -v2w v = -n2w (v2n v)) ∧
  (∀v. word_log2 (v2w v) = word_log2 (n2w (v2n v))) ∧
  (∀v n. v2w v = n2w n ⇔ n2w (v2n v) = n2w n) ∧
  (∀v n. n2w n = v2w v ⇔ n2w n = n2w (v2n v)) ∧
  (∀v w. v2w v + w = n2w (v2n v) + w) ∧ (∀v w. w + v2w v = w + n2w (v2n v)) ∧
  (∀v w. v2w v − w = n2w (v2n v) − w) ∧ (∀v w. w − v2w v = w − n2w (v2n v)) ∧
  (∀v w. v2w v * w = n2w (v2n v) * w) ∧ (∀v w. w * v2w v = w * n2w (v2n v)) ∧
  (∀v w. v2w v / w = n2w (v2n v) / w) ∧ (∀v w. w / v2w v = w / n2w (v2n v)) ∧
  (∀v w. v2w v // w = n2w (v2n v) // w) ∧
  (∀v w. w // v2w v = w // n2w (v2n v)) ∧
  (∀v w. word_mod (v2w v) w = word_mod (n2w (v2n v)) w) ∧
  (∀v w. word_mod w (v2w v) = word_mod w (n2w (v2n v))) ∧
  (∀v w. v2w v < w ⇔ n2w (v2n v) < w) ∧ (∀v w. w < v2w v ⇔ w < n2w (v2n v)) ∧
  (∀v w. v2w v > w ⇔ n2w (v2n v) > w) ∧ (∀v w. w > v2w v ⇔ w > n2w (v2n v)) ∧
  (∀v w. v2w v ≤ w ⇔ n2w (v2n v) ≤ w) ∧ (∀v w. w ≤ v2w v ⇔ w ≤ n2w (v2n v)) ∧
  (∀v w. v2w v ≥ w ⇔ n2w (v2n v) ≥ w) ∧ (∀v w. w ≥ v2w v ⇔ w ≥ n2w (v2n v)) ∧
  (∀v w. v2w v <₊ w ⇔ n2w (v2n v) <₊ w) ∧
  (∀v w. w <₊ v2w v ⇔ w <₊ n2w (v2n v)) ∧
  (∀v w. v2w v >₊ w ⇔ n2w (v2n v) >₊ w) ∧
  (∀v w. w >₊ v2w v ⇔ w >₊ n2w (v2n v)) ∧
  (∀v w. v2w v ≤₊ w ⇔ n2w (v2n v) ≤₊ w) ∧
  (∀v w. w ≤₊ v2w v ⇔ w ≤₊ n2w (v2n v)) ∧
  (∀v w. v2w v ≥₊ w ⇔ n2w (v2n v) ≥₊ w) ∧ ∀v w. w ≥₊ v2w v ⇔ w ≥₊ n2w (v2n v)