- 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)
- 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
- 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. 1 < dimindex (:α) ∧ 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
- 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))