Theory "integer_word"

Signature

Definitions

toString_def

⊢ ∀i.
      toString i = if i < 0 then STRCAT "~" (toString (Num (-i)))
      else toString (Num i)

fromString_primitive_def

⊢ fromString =
  WFREC (@R. WF R)
    (λfromString a.
         case a of
           "" => I (&toNum "")
         | STRING #"~" t => I (-&toNum t)
         | STRING #"-" t => I (-&toNum t)
         | STRING v4 t => I (&toNum (STRING v4 t)))

i2w_def

⊢ ∀i. i2w i = if i < 0 then -n2w (Num (-i)) else n2w (Num i)

w2i_def

⊢ ∀w. w2i w = if word_msb w then -&w2n (-w) else &w2n w

UINT_MAX_def

⊢ UINT_MAX (:α) = &dimword (:α) − 1

INT_MAX_def

⊢ INT_MAX (:α) = &INT_MIN (:α) − 1

INT_MIN_def

⊢ INT_MIN (:α) = -INT_MAX (:α) − 1

saturate_i2w_def

⊢ ∀i.
      saturate_i2w i = if UINT_MAX (:α) ≤ i then UINT_MAXw
      else if i < 0 then 0w else n2w (Num i)

saturate_i2sw_def

⊢ ∀i.
      saturate_i2sw i = if INT_MAX (:α) ≤ i then INT_MAXw
      else if i ≤ INT_MIN (:α) then INT_MINw else i2w i

saturate_sw2sw_def

⊢ ∀w. saturate_sw2sw w = saturate_i2sw (w2i w)

saturate_w2sw_def

⊢ ∀w. saturate_w2sw w = saturate_i2sw (&w2n w)

saturate_sw2w_def

⊢ ∀w. saturate_sw2w w = saturate_i2w (w2i w)

signed_saturate_add_def

⊢ ∀a b. signed_saturate_add a b = saturate_i2sw (w2i a + w2i b)

signed_saturate_sub_def

⊢ ∀a b. signed_saturate_sub a b = saturate_i2sw (w2i a − w2i b)

word_sdiv_def

⊢ ∀a b. word_sdiv a b = i2w (w2i a / w2i b)

word_smod_def

⊢ ∀a b. word_smod a b = i2w (w2i a % w2i b)

Theorems

fromString_ind

⊢ ∀P.
      (∀t. P (STRING #"~" t)) ∧ (∀t. P (STRING #"-" t)) ∧ P "" ∧
      (∀v4 v1. P (STRING v4 v1)) ⇒
      ∀v. P v

fromString_def

⊢ fromString (STRING #"~" t) = -&toNum t ∧
  fromString (STRING #"-" t) = -&toNum t ∧ fromString "" = &toNum "" ∧
  fromString (STRING v4 v1) = if v4 = #"~" then -&toNum v1
  else if v4 = #"-" then -&toNum v1 else &toNum (STRING v4 v1)

ONE_LE_TWOEXP

⊢ ∀n. 1 ≤ 2 ** n

w2i_w2n_pos

⊢ ∀w n. ¬word_msb w ∧ w2i w < &n ⇒ w2n w < n

w2i_n2w_pos

⊢ ∀n. n < INT_MIN (:α) ⇒ w2i (n2w n) = &n

w2i_n2w_neg

⊢ ∀n. INT_MIN (:α) ≤ n ∧ n < dimword (:α) ⇒ w2i (n2w n) = -&(dimword (:α) − n)

i2w_w2i

⊢ ∀w. i2w (w2i w) = w

w2i_i2w

⊢ ∀i. INT_MIN (:α) ≤ i ∧ i ≤ INT_MAX (:α) ⇒ w2i (i2w i) = i

word_msb_i2w

⊢ ∀i. word_msb (i2w i) ⇔ &INT_MIN (:α) ≤ i % &dimword (:α)

w2i_11

⊢ ∀v w. w2i v = w2i w ⇔ v = w

int_word_nchotomy

⊢ ∀w. ∃i. w = i2w i

w2i_le

⊢ ∀w. w2i w ≤ INT_MAX (:α)

w2i_ge

⊢ ∀w. INT_MIN (:α) ≤ w2i w

ranged_int_word_nchotomy

⊢ ∀w. ∃i. w = i2w i ∧ INT_MIN (:α) ≤ i ∧ i ≤ INT_MAX (:α)

sw2sw_i2w

⊢ ∀j.
      INT_MIN (:β) ≤ j ∧ j ≤ INT_MAX (:β) ∧ dimindex (:β) ≤ dimindex (:α) ⇒
      sw2sw (i2w j) = i2w j

w2w_i2w

⊢ ∀i. dimindex (:α) ≤ dimindex (:β) ⇒ w2w (i2w i) = i2w i

WORD_LTi

⊢ ∀a b. a < b ⇔ w2i a < w2i b

WORD_GTi

⊢ ∀a b. a > b ⇔ w2i a > w2i b

WORD_LEi

⊢ ∀a b. a ≤ b ⇔ w2i a ≤ w2i b

WORD_GEi

⊢ ∀a b. a ≥ b ⇔ w2i a ≥ w2i b

word_add_i2w_w2n

⊢ ∀a b. i2w (&w2n a + &w2n b) = a + b

word_add_i2w

⊢ ∀a b. i2w (w2i a + w2i b) = a + b

word_sub_i2w_w2n

⊢ ∀a b. i2w (&w2n a − &w2n b) = a − b

word_sub_i2w

⊢ ∀a b. i2w (w2i a − w2i b) = a − b

word_mul_i2w_w2n

⊢ ∀a b. i2w (&w2n a * &w2n b) = a * b

word_mul_i2w

⊢ ∀a b. i2w (w2i a * w2i b) = a * b

word_i2w_add

⊢ ∀a b. i2w a + i2w b = i2w (a + b)

word_i2w_mul

⊢ ∀a b. i2w a * i2w b = i2w (a * b)

MULT_MINUS_ONE

⊢ ∀i. -1w * i2w i = i2w (-i)

word_0_w2i

⊢ w2i 0w = 0

w2i_eq_0

⊢ ∀w. w2i w = 0 ⇔ w = 0w

i2w_DIV

⊢ ∀n i.
      n < dimindex (:α) ∧ INT_MIN (:α) ≤ i ∧ i ≤ INT_MAX (:α) ⇒
      i2w (i / 2 ** n) = i2w i ≫ n

INT_MIN_MONOTONIC

⊢ dimindex (:α) ≤ dimindex (:β) ⇒ INT_MIN (:β) ≤ INT_MIN (:α)

INT_MAX_MONOTONIC

⊢ dimindex (:α) ≤ dimindex (:β) ⇒ INT_MAX (:α) ≤ INT_MAX (:β)

w2i_sw2sw_bounds

⊢ ∀w. INT_MIN (:α) ≤ w2i (sw2sw w) ∧ w2i (sw2sw w) ≤ INT_MAX (:α)

w2i_i2w_id

⊢ ∀i.
      INT_MIN (:α) ≤ i ∧ i ≤ INT_MAX (:α) ∧ dimindex (:β) ≤ dimindex (:α) ⇒
      (i = w2i (i2w i) ⇔ i2w i = sw2sw (i2w i))

w2i_11_lift

⊢ ∀a b.
      dimindex (:α) ≤ dimindex (:γ) ∧ dimindex (:β) ≤ dimindex (:γ) ⇒
      (w2i a = w2i b ⇔ sw2sw a = sw2sw b)

w2i_n2w_mod

⊢ ∀n m.
      n < dimword (:α) ∧ m ≤ dimindex (:α) ⇒
      Num (w2i (n2w n) % 2 ** m) = n MOD 2 ** m

word_abs_w2i

⊢ ∀w. word_abs w = n2w (Num (ABS (w2i w)))

word_abs_i2w

⊢ ∀i.
      INT_MIN (:α) ≤ i ∧ i ≤ INT_MAX (:α) ⇒
      word_abs (i2w i) = n2w (Num (ABS i))

INT_MIN

⊢ INT_MIN (:α) = -&INT_MIN (:α)

INT_MAX

⊢ INT_MAX (:α) = &INT_MAX (:α)

UINT_MAX

⊢ UINT_MAX (:α) = &UINT_MAX (:α)

INT_BOUND_ORDER

⊢ INT_MIN (:α) < INT_MAX (:α) ∧ INT_MAX (:α) < UINT_MAX (:α) ∧
  UINT_MAX (:α) < &dimword (:α)

INT_ZERO_LT_INT_MIN

⊢ INT_MIN (:α) < 0

INT_ZERO_LT_INT_MAX

⊢ 1 < dimindex (:α) ⇒ 0 < INT_MAX (:α)

INT_ZERO_LE_INT_MAX

⊢ 0 ≤ INT_MAX (:α)

INT_ZERO_LT_UINT_MAX

⊢ 0 < UINT_MAX (:α)

w2i_1

⊢ w2i 1w = if dimindex (:α) = 1 then -1 else 1

w2i_INT_MINw

⊢ w2i INT_MINw = INT_MIN (:α)

w2i_UINT_MAXw

⊢ w2i UINT_MAXw = -1

w2i_INT_MAXw

⊢ w2i INT_MAXw = INT_MAX (:α)

w2i_minus_1

⊢ w2i (-1w) = -1

w2i_lt_0

⊢ ∀w. w2i w < 0 ⇔ w < 0w

w2i_neg

⊢ ∀w. w ≠ INT_MINw ⇒ w2i (-w) = -w2i w

i2w_0

⊢ i2w 0 = 0w

i2w_minus_1

⊢ i2w (-1) = -1w

i2w_INT_MIN

⊢ i2w (INT_MIN (:α)) = INT_MINw

i2w_INT_MAX

⊢ i2w (INT_MAX (:α)) = INT_MAXw

i2w_UINT_MAX

⊢ i2w (UINT_MAX (:α)) = UINT_MAXw

word_msb_i2w_lt_0

⊢ ∀i. INT_MIN (:α) ≤ i ∧ i ≤ INT_MAX (:α) ⇒ (word_msb (i2w i) ⇔ i < 0)

i2w_pos

⊢ ∀n. i2w (&n) = n2w n

word_quot

⊢ ∀a b. b ≠ 0w ⇒ a / b = i2w (w2i a quot w2i b)

word_rem

⊢ ∀a b. b ≠ 0w ⇒ word_rem a b = i2w (w2i a rem w2i b)

saturate_i2w_0

⊢ saturate_i2w 0 = 0w

saturate_i2sw_0

⊢ saturate_i2sw 0 = 0w

saturate_w2sw

⊢ ∀w.
      saturate_w2sw w =
      if dimindex (:β) ≤ dimindex (:α) ∧ w2w INT_MAXw ≤₊ w then INT_MAXw
      else w2w w

saturate_i2sw

⊢ ∀i. saturate_i2w i = if i < 0 then 0w else saturate_n2w (Num i)

saturate_sw2w

⊢ ∀w. saturate_sw2w w = if w < 0w then 0w else saturate_w2w w

saturate_sw2sw

⊢ ∀w.
      saturate_sw2sw w = if dimindex (:α) ≤ dimindex (:β) then sw2sw w
      else if sw2sw INT_MAXw ≤ w then INT_MAXw
      else if w ≤ sw2sw INT_MINw then INT_MINw else w2w w

signed_saturate_sub

⊢ ∀a b.
      signed_saturate_sub a b =
      if b = INT_MINw then if 0w ≤ a then INT_MAXw else a + INT_MINw
      else if dimindex (:α) = 1 then a && ¬b else signed_saturate_add a (-b)

signed_saturate_add

⊢ ∀a b.
      signed_saturate_add a b =
      (let
         sum = a + b and msba = word_msb a
       in
         if (msba ⇔ word_msb b) ∧ (msba ⇎ word_msb sum) then
           if msba then INT_MINw else INT_MAXw else sum)

different_sign_then_no_overflow

⊢ ∀x y. (word_msb x ⇎ word_msb y) ⇒ w2i (x + y) = w2i x + w2i y

w2i_i2w_pos

⊢ ∀n. n ≤ INT_MAX (:α) ⇒ w2i (i2w (&n)) = &n

w2i_i2w_neg

⊢ ∀n. n ≤ INT_MIN (:α) ⇒ w2i (i2w (-&n)) = -&n

overflow

⊢ ∀x y.
      w2i (x + y) ≠ w2i x + w2i y ⇔
      (word_msb x ⇔ word_msb y) ∧ (word_msb x ⇎ word_msb (x + y))

sub_overflow

⊢ ∀x y.
      w2i (x − y) ≠ w2i x − w2i y ⇔
      (word_msb x ⇎ word_msb y) ∧ (word_msb x ⇎ word_msb (x − y))

overflow_add

⊢ ∀x y. w2i (x + y) ≠ w2i x + w2i y ⇔ OVERFLOW x y F

overflow_sub

⊢ ∀x y. w2i (x − y) ≠ w2i x − w2i y ⇔ OVERFLOW x (¬y) T

i2w_w2n_w2w

⊢ ∀w. i2w (&w2n w) = w2w w

i2w_w2n

⊢ i2w (&w2n w) = w

w2n_i2w

⊢ &w2n (i2w n) = n % &dimword (:α)

w2i_eq_w2n

⊢ w2i w = if w2n w < INT_MIN (:α) then &w2n w else &w2n w − &dimword (:α)