Library machine_int

Require Import ProofIrrelevance.
Require Import ssreflect ssrbool.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import listbit listbit_correct.

Local Open Scope zarith_ext_scope.

This file provides:

a module type for the type "int : nat -> Type" of integers of finite-length

(the parameter is the length in bits of the underlying bitstring); this type can be regarded as an signed (resp. unsigned) integer using function s2Z (resp. u2Z); this type is accompanied with various functions and their arithmetic properties

an implementation using lists of bits

Further properties derivable outside the module

Definitions of often-used finite size integers

Module Type MACHINE_INT.

Parameter int : nat -> Type.
Parameter dec_int : forall n (a b : int n), {a = b} + {a <> b}.

Parameter cast : forall {f : nat -> nat -> nat} {P}
  (_ : forall k n, P k n -> f k n = n) {k n} (_ : P k n),
  int (f k n) -> int n.
Definition cast_le_plus_minus_r2 {k n : nat} (H : (k <= n)%nat) := cast le_plus_minus_r2 H.
Definition cast_le_plus_minus_r {k n : nat} (H : (k <= n)%nat) := cast le_plus_minus_r H.

Parameter u2Z : forall n, int n -> Z.
Parameter max_u2Z : forall n (a : int n), u2Z a < 2 ^^ n.
Parameter min_u2Z : forall n (a : int n), 0 <= u2Z a.
Parameter u2Z_inj : forall n (v w : int n), u2Z v = u2Z w -> v = w.
Parameter u2Z_cast : forall (f : nat -> nat -> nat) (P : nat -> nat -> Type)
  (H : forall k n : nat, P k n -> f k n = n) k n (Hkn : P k n) a,
  u2Z (cast H Hkn a) = u2Z a.

Parameter bits : forall (n : nat), int n -> list bool.
Parameter length_bits : forall n (a : int n), length (bits a) = n.
Parameter bits2u : forall n : nat, list bool -> int n.
Parameter u2Z_bits2u_ulst2Z : forall n l, length l = n -> u2Z (bits2u n l) = listbit_correct.ulst2Z l.

Z2u n z builds an unsigned machine integer of decimal value z and length n (if possible).

Parameter Z2u : forall n (z : Z), int n.
Parameter u2Z_Z2u : forall z n, 0 <= z < 2 ^^ n -> u2Z (Z2u n z) = z.
Parameter u2Z_Z2u_Zmod : forall z n, 0 <= z -> u2Z (Z2u n z) = z mod (2 ^^ n).
Parameter u2Z_Z2u_neg : forall z n, z < 0 -> u2Z (Z2u n z) = 0.
Parameter Z2u_u2Z : forall n (a : int n), Z2u n (u2Z a) = a.
Parameter Z2u_dis : forall n a b, 0 <= a < 2 ^^ n -> 0 <= b < 2 ^^ n ->
a <> b -> Z2u n a <> Z2u n b.
Parameter bits_zeros : forall n, bits (Z2u n 0) = ListBit.zeros n.

zero extend

Parameter zext : forall m n, int n -> int (m + n).
Parameter zext_Z2u : forall n m m', n < 2 ^^ m -> zext m' (Z2u (S m) n) = Z2u (m' + S m) n.
Parameter u2Z_zext : forall k n (a : int n), u2Z (zext k a) = u2Z a.

sign extend

Parameter sext : forall m n (i : int n), int (n + m).
Parameter u2Z_sext : forall n (v : int n) k, 0 <= u2Z v < 2 ^^ (Peano.pred n) ->
  u2Z (sext k v) = u2Z v.
Parameter sext_Z2u: forall n m m', n < 2 ^^ m -> sext m' (Z2u (S m) n) = Z2u (S m + m') n.

Parameter lt_n : forall n, int n -> int n -> bool.
  Notation "a '[.<]' b" := (lt_n a b) (at level 75) : machine_int_scope.
Local Open Scope machine_int_scope.

Parameter le_n : forall n, int n -> int n -> bool.
  Notation "a '[.<=]' b" := (le_n a b) (at level 75) : machine_int_scope.
Parameter le_n_refl : forall n (a : int n), a [.<=] a.
Parameter le_n_unfold : forall n (a b : int n), a [.<=] b -> a = b \/ a [.<] b.

arithmetic/logical operations and their properties

Parameter add : forall n, int n -> int n -> int n.
Notation "a '[.+]' b" := (add a b) (at level 35) : machine_int_scope.
Parameter add_com : forall n (a b : int n), a [.+] b = b [.+] a.
Parameter add_assoc : forall n (a b c : int n), (a [.+] b) [.+] c = a [.+] (b [.+] c).
Parameter add_0 : forall n (a : int n), add a (Z2u n 0) = a.

Parameter sub : forall n, int n -> int n -> int n.
Notation "a '[.-]' b" := (sub a b) (at level 50) : machine_int_scope.

unsigned multiplication with truncation

Parameter mul : forall n, int n -> int n -> int n.

Parameter umul : forall n (a b : int n), int (n + n).
Notation "a '[.*]' b" := (umul a b) (at level 50) : machine_int_scope.
Parameter umul_com : forall n (a b : int n), a [.*] b = b [.*] a.
Parameter umul_1 : forall n (x : int n), x [.*] Z2u n 1 = zext n x.
Parameter umul_0 : forall n (x : int n), x [.*] Z2u n 0 = Z2u (n + n) 0.

Parameter smul : forall n, int n -> int n -> int (2 * n).

returns the m last bits of (int n)

Parameter rem : forall m n, int n -> int m.
Notation "a '[.%]' n" := (rem n a) (at level 50) : machine_int_scope.
Parameter rem_Zpower : forall n k, (k < n)%nat -> Z2u n (2 ^^ k) [.%] k = Z2u k 0.

left shift

Parameter shl : forall (m : nat) n (i : int n), int n.
Notation "a '[.<<]' n" := (shl n a) (at level 50) : machine_int_scope.
Parameter shl_zero : forall n m, Z2u n 0 [.<<] m = Z2u n 0.
Parameter shl_1 : forall n k, (k <= n)%nat -> Z2u n 1 [.<<] k = Z2u n (2 ^^ k).
Parameter bits_shl_1 : forall n m, (m < n)%nat -> bits (Z2u n 1 [.<<] m) = ListBit.zeros m ++ true ::nil ++ ListBit.zeros (n - m - 1).
Parameter shl_rem_m : forall n (a : int n) m, (m <= n)%nat -> (a [.<<] m) [.%] m = Z2u m 0.

Parameter shl_extend : forall m n (i : int n), int (m + n).

logical right shift

Parameter shrl : nat -> forall n, int n -> int n.
Notation "a '[.>>]' n" := (shrl n a) (at level 50) : machine_int_scope.
Parameter shrl_comp : forall m k n (a : int n), (a [.>>] k) [.>>] m = a [.>>] (k + m).
Parameter shrl_0 : forall n (a : int n), a [.>>] 0 = a.
Parameter shrl_Z2u_0 : forall n k, Z2u n 0 [.>>] k = Z2u n 0.
Parameter shrl_Zpower : forall n k l, (k < n)%nat -> (l <= k)%nat -> Z2u n (2 ^^ k) [.>>] l = Z2u n (2 ^^ (k - l)).

Parameter shrl_overflow : forall n (a : int n) k, u2Z a < 2 ^^ k -> a [.>>] k = Z2u n 0.
Parameter shl_shrl : forall n (a : int n) m, u2Z a < 2 ^^ m -> (a [.<<] (n - m)) [.>>] (n - m) = a.
Parameter shrl_shl : forall n (a : int n) m, a [.%] m = Z2u m 0 -> (a [.>>] m) [.<<] m = a.

arithmetic right shift

Parameter shra : nat -> forall n, int n -> int n.
Parameter shr_shrink : forall m n (i : int n), int (n - m)%nat.
Parameter shr_shrink_overflow : forall n (a : int n) k, (k >= n)%nat -> shr_shrink k a = Z2u (n - k)%nat 0.

Parameter int_and : forall n, int n -> int n -> int n.
  Notation "a '[.&]' b" := (int_and a b) (at level 50) : machine_int_scope.
Parameter int_and_0 : forall n i, i [.&] Z2u n 0 = Z2u n 0.
Parameter int_and_comm : forall n (a b : int n), a [.&] b = b [.&] a.
Parameter int_and_idempotent : forall n (a : int n), a [.&] a = a.
Parameter int_even_and_1 : forall n (a : int n), Zeven (u2Z a) -> a [.&] Z2u n 1 = Z2u n 0.
Parameter int_odd_and_1 : forall n (a : int n), Zodd (u2Z a) -> a [.&] Z2u n 1 = Z2u n 1.
Parameter int_and_rem_1 : forall n (a : int n), u2Z (a [.&] Z2u n 1) = u2Z (a [.%] 1).
Parameter rem_and : forall n (a : int n) k (Hkn : (k <= n)%nat),
  cast_le_plus_minus_r2 Hkn (zext (n - k)%nat (a [.%] k)) = a [.&] Z2u n (2 ^^ k - 1).

Parameter int_or : forall n, int n -> int n -> int n.
  Notation "a '[.|]' b" := (int_or a b) (at level 50) : machine_int_scope.
Parameter int_or_0: forall n (a : int n), a [.|] Z2u n 0 = a.
Parameter int_or_comm : forall n (a b : int n), a [.|] b = b [.|] a.
Parameter int_or_idempotent : forall n (a : int n), a [.|] a = a.
Parameter bits_int_or : forall n (a b : int n), bits (a [.|] b) = ListBit.or_lst (bits a) (bits b).
Parameter shl_distr_or : forall n (a b : int n) m, (a [.|] b) [.<<] m = (a [.<<] m) [.|] (b [.<<] m).
Parameter shrl_distr_or : forall n (a b : int n) m, (a [.|] b) [.>>] m = (a [.>>] m) [.|] (b [.>>] m).
Parameter rem_distr_or : forall n (a b : int n) m, (a [.|] b) [.%] m = (a [.%] m) [.|] (b [.%] m).
Parameter or_sh_rem : forall n (a : int n) k (H : (k <= n)%nat),
  a = ((a [.>>] k) [.<<] k) [.|] (cast_le_plus_minus_r2 H (zext (n - k) (a [.%] k))).

Parameter int_xor : forall n, int n -> int n -> int n.
  Notation "a '[.(+)]' b" := (int_xor a b) (at level 50) : machine_int_scope.
Parameter int_xor_0 : forall n (a : int n), a [.(+)] Z2u n 0 = a.
Parameter int_xor_comm : forall n (a b : int n), a [.(+)] b = b [.(+)] a.
Parameter int_xor_assoc : forall n (a b c : int n), (a [.(+)] b) [.(+)] c = a [.(+)] (b [.(+)] c).
Parameter int_xor_self : forall n (a : int n), a [.(+)] a = Z2u n 0.

Parameter int_not : forall n, int n -> int n.
Parameter int_and_1s : forall n i, i [.&] int_not (Z2u n 0) = i.
Parameter int_not_or : forall n (a b : int n), int_not (a [.|] b) = int_not a [.&] int_not b.

Parameter cplt2 : forall n, int n -> int n.
Parameter not_add_1_cplt2: forall n (v : int n), (n > 1)%nat -> int_not v [.+] Z2u n 1 = cplt2 v.

Parameter concat : forall n m (a : int n) (b : int m), int (n + m).
  Notation "a '[.||]' b " := (concat a b) (at level 75) : machine_int_scope.
Parameter or_concat : forall n (a : int n) (b : int n) k (Hkn: (k <= n)%nat),
  u2Z a < 2 ^^ k ->
  b [.%] k = Z2u k 0 ->
  (b [.|] a) = cast_le_plus_minus_r2 Hkn ((shr_shrink k b) [.||] (a [.%] k)).
Parameter rem_concat : forall n (a : int n) m (b : int m), (a [.||] b) [.%] m = b.

interpretation of int as unsigned integers and related properties

Parameter u2Z_add : forall n (a b : int n), u2Z a + u2Z b < 2 ^^ n -> u2Z (a [.+] b) = u2Z a + u2Z b.
Parameter u2Z_add_overflow : forall n (a b : int n), 2 ^^ n <= u2Z a + u2Z b -> u2Z (a [.+] b) + 2 ^^ n = u2Z a + u2Z b.
Parameter u2Z_sub : forall n (a b : int n), u2Z a >= u2Z b -> u2Z (a [.-] b) = u2Z a - u2Z b.
Parameter u2Z_sub_overflow : forall n (a b : int n), u2Z a < u2Z b -> u2Z (a [.-] b) = u2Z a + 2 ^^ n - u2Z b.
Parameter u2Z_mul : forall n (a b : int n), u2Z a * u2Z b < 2 ^^ n -> u2Z (mul a b) = u2Z a * u2Z b.
Parameter u2Z_umul: forall n (a b : int n), u2Z (a [.*] b) = u2Z a * u2Z b.

Parameter u2Z_shl : forall k n (x : int n) m, (k + m <= n)%nat -> u2Z x < 2 ^^ m ->
  u2Z (x [.<<] k) = u2Z x * 2 ^^ k.
Parameter u2Z_shl' : forall n (x : int n), forall m, u2Z x < 2 ^^ m -> forall k, (k + m <= n)%nat ->
  u2Z (x [.<<] k) <= 2 ^^ (m + k) - 2 ^^ k.
Parameter u2Z_shl_overflow : forall k n (x : int n), (k >= n)%nat -> u2Z (x [.<<] k) = 0.
Parameter u2Z_shl_Zmod : forall n (a : int n) k, (k < n)%nat ->
  u2Z (a [.<<] k) = (u2Z a * 2 ^^ k) mod 2 ^^ n.
Parameter u2Z_shl_rem : forall n (a : int n) k, u2Z (a [.<<] k) = 2 ^^ k * u2Z (a [.%] (n - k)).

Parameter u2Z_shl_extend : forall k n (x : int n),
  u2Z (shl_extend k x) = u2Z x * 2 ^^ k.
Parameter u2Z_shl_extend' : forall n (x : int n), forall m, u2Z x < 2 ^^ m -> forall k,
  u2Z (shl_extend k x) <= 2 ^^ (m + k) - 2 ^^ k.
Parameter u2Z_shl_extend'' : forall l (x : int l), forall k, u2Z x < 2 ^^ k -> forall n,
  u2Z (shl_extend n x) + 2 ^^ n <= 2 ^^ (k + n).

Parameter Zle_u2Z_shr_shrink : forall n (a : int n) k,
  u2Z (shr_shrink k a) * 2 ^^ k <= u2Z a.
Parameter u2Z_shr_shrink : forall l (x : int l) n, (l >= n)%nat ->
  u2Z (shr_shrink n x) * 2 ^^ n + u2Z (x [.%] n) = u2Z x.
Parameter u2Z_shr_shrink': forall l (x : int l) n, (l >= n)%nat ->
  u2Z (shr_shrink n x) * 2 ^^ n = u2Z x - u2Z (x [.%] n).

Parameter u2Z_shrl : forall {n} (x : int n) k, (n >= k)%nat ->
  u2Z (x [.>>] k) * 2 ^^ k + u2Z (x [.%] k) = u2Z x.

Parameter shrl_lt : forall n (a : int n) m, u2Z (a [.>>] m) < 2 ^^ (n - m).

Parameter u2Z_rem : forall n (x : int n) k, (n >= k)%nat -> u2Z (x [.%] k) = u2Z x - u2Z (shr_shrink k x) * 2 ^^ k.
Parameter u2Z_rem' : forall n (a : int n) k, u2Z a < 2 ^^ k -> u2Z (a [.%] k) = u2Z a.

Parameter u2Z_rem'' : forall {n} (a : int n) k a', u2Z a = 2 ^^ (S k) * a' -> u2Z (a [.%] S k) = 0.

Parameter u2Z_rem_zext : forall n (a : int n) k m, u2Z (zext k a [.%] m) = u2Z (a [.%] m).

Parameter u2Z_concat : forall n l (a : int n) (b : int l), u2Z (a [.||] b) = u2Z a * 2 ^^ l + u2Z b.

Parameter lt_n2Zlt : forall n (a b : int n), lt_n a b -> u2Z a < u2Z b.
Parameter Zlt2lt_n : forall n (a b : int n), u2Z a < u2Z b -> lt_n a b.
Parameter Zle2le_n : forall n (a b:int n), u2Z a <= u2Z b -> a [.<=] b.

Parameter s2Z : forall n, int n -> Z.
Parameter max_s2Z : forall n (a : int n), s2Z a < 2 ^^ (Coq.Init.Peano.pred n).
Parameter min_s2Z : forall n (a : int (S n)), - 2 ^^ n <= s2Z a.
Parameter s2Z_inj : forall n (v w : int n), s2Z v = s2Z w -> v = w.
Parameter weird : forall n (v : int (S n)), Prop.
Parameter weirdE : forall n (a : int (S n)), weird a <-> u2Z a = 2 ^^ n.
Parameter weirdE2 : forall n (a : int (S n)), weird a <-> s2Z a = - 2 ^^ n.

Parameter s2Z_cplt2: forall n (v : int (S n)), ~ weird v -> s2Z (cplt2 v) = - (s2Z v).
Parameter sext_s2Z : forall n (v : int n) k, s2Z (sext k v) = s2Z v.

Z2s n z builds a signed machine integer of decimal value z and length n (if possible).

Parameter Z2s : forall n (z : Z), int n.
Parameter s2Z_Z2s : forall z m, - 2 ^^ m <= z < 2 ^^ m -> s2Z (Z2s (S m) z) = z.
Parameter Z2s_dis : forall n a b, - 2 ^^ n <= a < 2 ^^ n -> - 2 ^^ n <= b < 2 ^^ n ->
a <> b -> Z2s (S n) a <> Z2s (S n) b.
Parameter sext_Z2s : forall m z n, - 2 ^^ m <= z < 2 ^^ m -> sext n (Z2s (S m) z) = Z2s (S m + n) z.

relations between u2Z and s2Z/Z2s

Parameter s2Z_u2Z_pos : forall n (a : int n), 0 <= s2Z a -> s2Z a = u2Z a.
Parameter s2Z_u2Z_pos' : forall n (a : int n), 0 <= u2Z a < 2 ^^ (Coq.Init.Peano.pred n) -> s2Z a = u2Z a.
Parameter s2Z_u2Z_neg : forall n (a : int n), s2Z a < 0 -> u2Z a = s2Z a + 2^^n.
Parameter Z2s_weird : forall n, u2Z (Z2s (S n) (- 2 ^^ n)) = 2 ^^ n.
Parameter u2Z_Z2s_neg : forall z n, - 2 ^^ (Peano.pred n) <= z < 0 -> u2Z (Z2s n z) = 2 ^^ n + z.
Parameter u2Z_Z2s_pos : forall z n, 0 <= z < 2 ^^ (Peano.pred n) -> u2Z (Z2s n z) = z.

interpretation of int as signed integers and related properties

Parameter s2Z_add: forall n (a b : int (S n)), - 2 ^^ n <= s2Z a + s2Z b < 2 ^^ n -> s2Z (a [.+] b) = s2Z a + s2Z b.
Parameter s2Z_smul : forall n (a b : int n), s2Z (smul a b) = s2Z a * s2Z b.
Parameter s2Z_shl : forall k n (x : int n) m, (k + S m <= n)%nat -> - 2 ^^ m <= s2Z x < 2 ^^ m ->
  s2Z (shl k x) = s2Z x * 2 ^^ k.
Parameter s2Z_sra : forall n (a : int (S n)) m, s2Z a < 0 ->
  (n < m)%nat ->
  bits (shra m a) = ListBit.ones (S n).
Parameter s2Z_sra_pos : forall n (a : int (S n)) m, 0 <= s2Z a ->
  (n < m)%nat ->
  bits (shra m a) = ListBit.zeros (S n).
Parameter shrl_sign_bit : forall (n : nat) (a : int (power 2 n)),
a [.>>] (power 2 n - 1) = Z2u (power 2 n) 0 \/ a [.>>] (power 2 n - 1) = Z2u (power 2 n) 1.
Parameter bZsgn_Zsgn_s2Z : forall (n : nat) (a : int (power 2 n)), u2Z a <> 0 ->
  bZsgn (u2Z (a [.>>] (power 2 n - 1))) = Zsgn (s2Z a).

Local Close Scope machine_int_scope.

Parameter int_div_list : forall n k q, n = (q * k)%nat -> forall (a : int n), list (int k).
Parameter len_int_div_list : forall (n k q : nat) (Hn : n = (q * S k)%nat)
  (a : int n),
  Datatypes.length (int_div_list _ _ _ Hn a) = q.
Parameter int_mul_list : forall n k q, n = (q * k)%nat -> list (int k) -> option (int n).
Parameter int_mul_list_Some : forall n k q (H : n = (q * k)%nat) (l : list (int k)),
  length l = q -> exists x, int_mul_list n k q H l = Some x.
Parameter int_mul_list_None : forall n k q (H : n = (q * k)%nat) (l : list (int k)),
  k <> O ->
  List.length l <> q ->
  int_mul_list n k q H l = None.
Parameter int_mul_list_firstn : forall n k q (H : n = (q * k)%nat) (l : list (int k)) x x',
  k <> O ->
  int_mul_list n k q H l = Some x ->
  int_mul_list n k q H (firstn n l) = Some x' -> x = x'.

Parameter int_mul_list_inj : forall n k l1 l2 nk x,
  n <> O -> forall (H : nk = (k * n)%nat),
  int_mul_list nk n k H l1 = Some x ->
  int_mul_list nk n k H l2 = Some x ->
  l1 = l2.

Parameter int_mul_div_list : forall n k q (a : int n) (Hn : (n = q * S k)%nat),
  int_mul_list n (S k) q Hn (int_div_list n (S k) q Hn a) = Some a.

End MACHINE_INT.

Module MachineInt : MACHINE_INT.

Require Import ssrnat.

Import ListBit.

definition of machine integers: a machine integer is a list of bits of a known length

Inductive int' n : Type := mk_int : forall (lst : list bool), length lst = n -> int' n.

Definition mk_i lst := mk_int lst (refl_equal (length lst)).

Definition int n := int' n.

Lemma mk_int_pi : forall n l (H : length l = n) l' (H' : length l' = n),
  l = l' -> mk_int l H = mk_int l' H'.

Lemma mk_int_pi' : forall n l (H : length l = n) n' l' (H' : length l' = n') (n_n' : n = n'),
  l = l' -> eq_rect n int' (mk_int l H) _ n_n' = mk_int l' H'.

Definition int_lst n (b : int' n) := match b with mk_int lst _ => lst end.

Lemma mk_int_pi'' : forall n l (H : length l = n) n' (n_n' : n = n'),
  int_lst (eq_rect n int' (mk_int l H) _ n_n') = l.

Definition bits n (b : int n) := rev (int_lst b).

Definition int_prf n (b : int' n) : length (int_lst b) = n :=
  match b return length (int_lst b) = n with mk_int l prf => prf end.

Lemma dec_int : forall l (a b : int l), { a = b } + { a <> b }.

Definition cast {f : nat -> nat -> nat} {P}
  (HPf : forall k n, P k n -> f k n = n) {k n} (HP : P k n) :
  int (f k n) -> int n.

Definition cast_le_plus_minus_r2 {k n : nat} (H : (k <= n)%coq_nat) := cast le_plus_minus_r2 H.
Definition cast_le_plus_minus_r {k n : nat} (H : (k <= n)%coq_nat) := cast le_plus_minus_r H.

Definition u2Z len (a : int' len) : Z := match a with mk_int lst _ => ulst2Z lst end.

Lemma max_u2Z : forall l (a : int l), u2Z a < 2 ^^ l.

Lemma min_u2Z : forall l (a : int l), 0 <= u2Z a.

Lemma u2Z_inj : forall l (v w : int l), u2Z v = u2Z w -> v = w.

Lemma u2Z_cast : forall (f : nat -> nat -> nat) (P : nat -> nat -> Type)
  (H : forall k n : nat, P k n -> f k n = n) k n (Hkn : P k n) a,
  u2Z (cast H Hkn a) = u2Z a.

Lemma length_bits : forall n (a : int n), length (bits a) = n.

Definition bits2u n (l : list bool) : int n := mk_int (adjust_ulist l n) (len_adjust_ulist n _).

Lemma u2Z_bits2u_ulst2Z : forall n l, length l = n -> u2Z (bits2u n l) = listbit_correct.ulst2Z l.

Definition Z2u n (l : Z) : int n := mk_int (adjust_ulist (Z2ulst l) n) (len_adjust_ulist n _).

Lemma u2Z_Z2u : forall z m, 0 <= z < 2 ^^ m -> u2Z (Z2u m z) = z.

Lemma u2Z_Z2u_Zmod' : forall z n, 2 ^^ n <= z -> u2Z (Z2u n z) = z mod (2 ^^ n).

Lemma u2Z_Z2u_Zmod : forall z n, 0 <= z -> u2Z (Z2u n z) = z mod (2 ^^ n).

Lemma u2Z_Z2u_neg: forall z n, z < 0 -> u2Z (Z2u n z) = 0.

Lemma Z2u_dis l a b : 0 <= a < 2 ^^ l -> 0 <= b < 2 ^^ l ->
  a <> b -> Z2u l a <> Z2u l b.

Lemma Z2u_u2Z : forall n (a : int n), Z2u n (u2Z a) = a.

Lemma bits_zeros : forall n, bits (Z2u n 0) = ListBit.zeros n.

Definition zext m n (a : int n) : int (m + n) :=
  mk_int (zext_lst m (int_lst a)) (len_zext_lst n (int_lst a) (int_prf a) m).

Lemma zext_Z2u: forall n m m', n < 2 ^^ m ->
  zext m' (Z2u (S m) n) = Z2u (m' + S m) n.

Lemma u2Z_zext : forall (k : nat) l (a : int l), u2Z (zext k a) = u2Z a.

Definition sext (m: nat) n (a: int n) : int (n + m) :=
  mk_int (sext_lst m (int_lst a)) (len_sext_lst' m n (int_lst a) (int_prf a)).

Lemma pred_predn : forall n, Peano.pred n = ssrnat.predn n.

Lemma u2Z_sext : forall l (v:int l) n, 0 <= u2Z v < 2 ^^ (Coq.Init.Peano.pred l) ->
  u2Z (sext n v) = u2Z v.

Lemma sext_Z2u: forall n m m', n < 2 ^^ m ->
  sext m' (Z2u (S m) n) = Z2u (S m + m') n.

Definition lt_n n (a b : int n) : bool := listbit_lt (int_lst a) (int_lst b).
Notation "a '[.<]' b" := (lt_n a b) (at level 75) : machine_int_scope.

Local Open Scope machine_int_scope.

Definition le_n n (a b : int n) : bool := listbit_le (int_lst a) (int_lst b).
Notation "a '[.<=]' b" := (le_n a b) (at level 75) : machine_int_scope.

Lemma le_n_refl : forall n (a : int n), a [.<=] a.

Lemma le_n_unfold : forall n (a b : int n), a [.<=] b -> a = b \/ a [.<] b.

Lemma lt_nW : forall n (a b : int n), a [.<] b -> a [.<=] b.

Definition add l (a b : int' l) : int' l := mk_int
  (add_lst (int_lst a) (int_lst b) false)
  (len_add_lst l (int_lst a) (int_lst b) (int_prf a) (int_prf b) false).
Notation "a '[.+]' b" := (add a b) (at level 35) : machine_int_scope.

Lemma add_com : forall l (a b : int' l), a [.+] b = b [.+] a.

Lemma add_assoc : forall l (a b c : int' l), (a [.+] b) [.+] c = a [.+] (b [.+] c).

Lemma add_0 : forall l (a : int l), a [.+] Z2u l 0 = a.

Definition sub n (a b : int' n) : int' n := mk_int
  (sub_lst (int_lst a) (int_lst b) false)
  (len_sub_lst n (int_lst a) (int_lst b) false (int_prf a) (int_prf b)).

unsigned multiplication with truncation

Definition mul n (a b:int' n) : int' n := mk_int
(adjust_ulist (umul_lst (int_lst a) (int_lst b)) n)
(len_adjust_ulist n (umul_lst (int_lst a) (int_lst b))).

unsigned multiplication (traditional one, without truncation)

Definition umul : forall l (a b:int' l), int' (l + l).

Lemma umul_com : forall l (a b : int l), umul a b = umul b a.

Lemma umul_1 : forall l (x : int l), umul x (Z2u l 1) = zext l x.

Notation "a '[.*]' b" := (umul a b) (at level 50) : machine_int_scope.

Lemma umul_0 : forall n (x : int n), x [.*] Z2u n 0 = Z2u (n + n) 0.

signed multiplication

Lemma smul_lst_length_length : forall n (a b: int' n),
  (length (smul_lst (int_lst a) (int_lst b)) = 2 * n)%nat.

Definition smul n (a b:int' n) : int' (2 * n) := mk_int
  (smul_lst (int_lst a) (int_lst b))
  (smul_lst_length_length a b).

remainder

Definition rem n m (a : int' m) : int' n.
Notation "a '[.%]' n" := (rem n a) (at level 50) : machine_int_scope.

Lemma rem_Zpower : forall n k, (k < n)%coq_nat -> Z2u n (2 ^^ k) [.%] k = Z2u k 0.

Definition shl m n (a: int n) : int n :=
  mk_int (shl_lst m (int_lst a)) (len_shl_lst m n (int_lst a) (int_prf a)).
Notation "a '[.<<]' n" := (shl n a) (at level 50) : machine_int_scope.

Lemma shl_zero : forall n m, Z2u n 0 [.<<] m = Z2u n 0.

Lemma shl_1 : forall n k, (k <= n)%coq_nat -> Z2u n 1 [.<<] k = Z2u n (2 ^^ k).

Lemma bits_shl_1 : forall n m, (m < n)%coq_nat ->
  bits (Z2u n 1 [.<<] m) = zeros m ++ true :: nil ++ zeros (n - m - 1).

Lemma shl_rem_m : forall n (a : int n) m, (m <= n)%coq_nat -> (a [.<<] m) [.%] m = Z2u m 0.

Definition shl_extend m n (a : int n) : int (m + n) :=
  mk_int (shl_extend_lst m (int_lst a)) (len_shl_extend_lst n (int_lst a) (int_prf a) m).

Definition shrl m n (a : int n) :=
  mk_int (shrl_lst m (int_lst a)) (len_shrl_lst n m (int_lst a) (int_prf a)).
Notation "a '[.>>]' k" := (shrl k a) (at level 50) : machine_int_scope.

Lemma shrl_comp : forall m k n (a : int n), (a [.>>] k) [.>>] m = a [.>>] (k + m).

Lemma shrl_0 : forall n (a : int n), (a [.>>] 0) = a.

Lemma shrl_Z2u_0 : forall n k, Z2u n 0 [.>>] k = Z2u n 0.

Lemma shrl_Zpower : forall n k l, (k < n)%coq_nat -> (l <= k)%coq_nat -> Z2u n (2 ^^ k) [.>>] l = Z2u n (2 ^^ (k - l)).

Lemma shrl_overflow : forall n (a : int n) k, u2Z a < 2 ^^ k -> a [.>>] k = Z2u n 0.

Lemma shl_shrl : forall n (a : int n) m, u2Z a < 2 ^^ m -> (a [.<<] (n - m)) [.>>] (n - m) = a.

Lemma shrl_shl : forall n (a : int n) m, a [.%] m = Z2u m 0 -> (a [.>>] m) [.<<] m = a.

Definition shra m n (a : int n) : int n :=
  mk_int (shra_lst m (int_lst a)) (len_shra_lst n m (int_lst a) (int_prf a)).

Definition shr_shrink m n (a : int n) : int (n - m)%coq_nat :=
  mk_int (shr_shrink_lst m (int_lst a)) (len_shr_shrink_lst n m (int_lst a) (int_prf a)).

Lemma shr_shrink_overflow : forall n (a : int n) k, (k >= n)%coq_nat ->
  shr_shrink k a = Z2u (n - k)%coq_nat 0.

Definition int_and n (a b : int n) : int n :=
  mk_int (and_lst (int_lst a) (int_lst b)) (len_and_lst n (int_lst a) (int_lst b) (int_prf a) (int_prf b)).
Notation "a '[.&]' b" := (int_and a b) (at level 50) : machine_int_scope.

Lemma int_and_0 : forall n true, true [.&] Z2u n 0 = Z2u n 0.

Lemma int_and_comm : forall n (a b : int n), a [.&] b = b [.&] a.

Lemma int_and_idempotent : forall n (a : int n), a [.&] a = a.

Lemma int_even_and_1 : forall n (a : int n), Zeven (u2Z a) -> a [.&] Z2u n 1 = Z2u n 0.

Lemma int_odd_and_1 : forall n (a : int n), Zodd (u2Z a) -> a [.&] Z2u n 1 = Z2u n 1.

Lemma int_and_rem_1 : forall n (a : int n), u2Z (a [.&] Z2u n 1) = u2Z (a [.%] 1).

Lemma rem_and : forall n (a : int n) k (Hkn : (k <= n)%coq_nat),
  cast_le_plus_minus_r2 Hkn (zext (n - k)%nat (a [.%] k)) =
  (a [.&] Z2u n (2 ^^ k - 1)).

Definition int_or n (a b : int n) : int n :=
  mk_int (or_lst (int_lst a) (int_lst b))
  (len_or_lst n (int_lst a) (int_lst b) (int_prf a) (int_prf b)).
Notation "a '[.|]' b" := (int_or a b) (at level 50) : machine_int_scope.

Lemma int_or_0: forall n (v : int n), v [.|] Z2u n 0 = v.

Lemma int_or_comm : forall n (a b : int n), a [.|] b = b [.|] a.

Lemma int_or_idempotent : forall n (a : int n), a [.|] a = a.

Lemma bits_int_or : forall n (a b : int n),
  bits (a [.|] b) = ListBit.or_lst (bits a) (bits b).

Lemma shl_distr_or : forall n (a b : int n) m,
  (a [.|] b) [.<<] m = (a [.<<] m) [.|] (b [.<<] m).

Lemma shrl_distr_or : forall n (a b : int n) m,
  (a [.|] b) [.>>] m = (a [.>>] m) [.|] (b [.>>] m).

Lemma rem_distr_or : forall n (a b : int n) m,
  (a [.|] b) [.%] m = (a [.%] m) [.|] (b [.%] m).

Lemma or_sh_rem : forall n (a : int n) k (H : (k <= n)%coq_nat),
  a = ((a [.>>] k) [.<<] k) [.|] (cast_le_plus_minus_r2 H (zext (n - k) (a [.%] k))).

Definition int_xor n (a b : int n) : int n :=
  mk_int (xor_lst (int_lst a) (int_lst b))
  (len_xor_lst n (int_lst a) (int_lst b) (int_prf a) (int_prf b)).
Notation "a '[.(+)]' b" := (int_xor a b) (at level 50) : machine_int_scope.

Lemma int_xor_0: forall n (v : int n), v [.(+)] Z2u n 0 = v.

Lemma int_xor_comm : forall n (a b : int n), a [.(+)] b = b [.(+)] a.

Lemma int_xor_assoc : forall n (a b c : int n), (a [.(+)] b) [.(+)] c = a [.(+)] (b [.(+)] c).

Lemma int_xor_self : forall n (a : int n), a [.(+)] a = Z2u n 0.

Definition int_not n (a : int n) : int n := mk_int (cplt1 (int_lst a)) (len_cplt1' n (int_lst a) (int_prf a)).

Lemma int_and_1s : forall n a, a [.&] int_not (Z2u n 0) = a.

Lemma int_not_or : forall n (a b : int n),
  int_not (a [.|] b) = int_not a [.&] int_not b.

Definition cplt2 n (a : int n) : int n :=
  mk_int (cplt2_lst (int_lst a)) (len_cplt2_lst' n (int_lst a) (int_prf a)).

Lemma not_add_1_cplt2: forall n (v : int n), (n > 1)%coq_nat ->
  int_not v [.+] Z2u n 1 = cplt2 v.

Definition concat_length : forall n m, int (n + m) -> int (m + n).

Definition concat n m (a : int' n) (b : int' m) : int' (n + m) :=
  add (concat_length _ _ (shl_extend m a)) (zext n b).
Notation "a [.||] b " := (concat a b) (at level 75) : machine_int_scope.

Lemma or_concat : forall n (a : int n) (b : int n) k (Hkn: (k <= n)%coq_nat),
  u2Z a < 2 ^^ k ->
  b [.%] k = Z2u k 0 ->
  (b [.|] a) = cast_le_plus_minus_r2 Hkn (shr_shrink k b [.||] (a [.%] k)).

Lemma rem_concat : forall n (a : int n) m (b : int m), (a [.||] b) [.%] m = b.

interpretation of int as unsigned integers and related properties

correctness of the addition w.r.t. unsigned integers

Lemma u2Z_add : forall n (a b : int' n), u2Z a + u2Z b < 2 ^^ n ->
u2Z (a [.+] b) = u2Z a + u2Z b.

Lemma u2Z_add_overflow : forall n (a b : int n), 2 ^^ n <= u2Z a + u2Z b ->
u2Z (a [.+] b) + 2 ^^ n = u2Z a + u2Z b.

correctness of subtraction w.r.t. unsigned integers

Lemma u2Z_sub : forall n (a b : int n), u2Z a >= u2Z b ->
u2Z (sub a b) = u2Z a - u2Z b.

Lemma u2Z_sub_overflow : forall n (a b : int n), u2Z a < u2Z b ->
u2Z (sub a b) = u2Z a + 2 ^^ n - u2Z b.

correctness of the unsigned multiplication (with truncation)

Lemma u2Z_mul : forall n (a b : int' n), u2Z a * u2Z b < 2 ^^ n ->
u2Z (mul a b) = u2Z a * u2Z b.

correctness of the unsigned multiplication

Lemma u2Z_umul: forall n (a b : int' n), u2Z (umul a b) = u2Z a * u2Z b.

Lemma u2Z_shl : forall n L (x : int L) l, (n + l <= L)%coq_nat -> u2Z x < 2 ^^ l ->
  u2Z (shl n x) = u2Z x * 2 ^^ n.

Lemma u2Z_shl' : forall l (x : int l), forall L, u2Z x < 2 ^^ L -> forall n, (n + L <= l)%coq_nat ->
  u2Z (shl n x) <= 2 ^^ (L + n) - 2 ^^ n.

Lemma u2Z_shl_overflow : forall n l (x : int l), (n >= l)%coq_nat -> u2Z (shl n x) = 0.

Lemma u2Z_shl_Zmod : forall l (a: int l) k, (k < l)%coq_nat ->
  u2Z (shl k a) = (u2Z a * 2 ^^ k) mod 2 ^^ l.

Lemma u2Z_shl_rem : forall n (a : int n) k, u2Z (a [.<<] k) = 2 ^^ k * u2Z (a [.%] (n - k)).

Lemma u2Z_shl_extend : forall n l (x : int l), u2Z (shl_extend n x) = u2Z x * 2 ^^ n.

Lemma u2Z_shl_extend' : forall l (x : int l), forall k, u2Z x < 2 ^^ k -> forall n,
  u2Z (shl_extend n x) <= 2 ^^ (k + n) - 2 ^^ n.

Lemma u2Z_shl_extend'' : forall l (x : int l), forall k, u2Z x < 2 ^^ k -> forall n,
  u2Z (shl_extend n x) + 2 ^^ n <= 2 ^^ (k + n).

Lemma Zle_u2Z_shr_shrink : forall n (a : int n) k, u2Z (shr_shrink k a) * 2 ^^ k <= u2Z a.

Lemma u2Z_shr_shrink : forall l (x : int l) n, (l >= n)%coq_nat ->
  u2Z (shr_shrink n x) * 2^^n + u2Z (x [.%] n) = u2Z x.

Lemma u2Z_shr_shrink' : forall l (x : int l) (n : nat), (l >= n)%coq_nat ->
  u2Z (shr_shrink n x) * 2^^n = u2Z x - u2Z (x [.%] n).

Lemma u2Z_shrl : forall l (x : int l) n, (l >= n)%coq_nat ->
  u2Z (x [.>>] n) * 2^^n + u2Z (x [.%] n) = u2Z x.

Lemma shrl_lt : forall n (a : int n) m, u2Z (a [.>>] m) < 2 ^^ (n - m).

Lemma u2Z_rem : forall n (x : int n) m, (n >= m)%coq_nat ->
  u2Z (x [.%] m) = u2Z x - u2Z (shr_shrink m x) * 2 ^^ m.

Lemma u2Z_rem' : forall n (a : int n) k, u2Z a < 2 ^^ k -> u2Z (a [.%] k) = u2Z a.

Lemma u2Z_rem''_ : forall n (a : int n) k a', 0 < a' -> k <> O -> u2Z a = 2 ^^ k * a' -> u2Z (a [.%] k) = 0.

Lemma rem_Z2u_0 : forall n k, Z2u n 0 [.%] k = Z2u k 0.

Lemma u2Z_rem'' : forall n (a : int n) k a', u2Z a = 2 ^^ (S k) * a' -> u2Z (a [.%] (S k)) = 0.

Lemma u2Z_rem_zext : forall n (a : int n) k m, u2Z (zext k a [.%] m) = u2Z (a [.%] m).

Local Open Scope listbit_correct_scope.

Lemma u2Z_concat : forall n l (a : int n) (b : int l), u2Z (a [.||] b) = u2Z a * 2 ^^ l + u2Z b.

Definition lt_n2Zlt : forall n (a b : int n), a [.<] b -> u2Z a < u2Z b.

Lemma Zlt2lt_n : forall n (a b : int n), u2Z a < u2Z b -> a [.<] b.

Lemma Zle2le_n : forall n (a b:int n), u2Z a <= u2Z b -> a [.<=] b.

interpretation of int as relative integers and related properties

Definition s2Z l (a : int' l) : Z := match a with mk_int lst _ => slst2Z lst end.

Lemma max_s2Z : forall l (a : int l), s2Z a < 2 ^^ (Coq.Init.Peano.pred l).

Lemma min_s2Z : forall n (a : int (S n)), - 2 ^^ n <= s2Z a.

Lemma s2Z_inj : forall l (v w : int l), s2Z v = s2Z w -> v = w.

Definition weird n (a : int (S n)) : Prop := int_lst a = true :: zeros n.

Lemma weirdE : forall n (a : int (S n)), weird a <-> u2Z a = Zpower 2 n.

Lemma weirdE2 : forall n (a : int (S n)), weird a <-> s2Z a = - Zpower 2 n.

Lemma s2Z_cplt2: forall n (v : int (S n)), ~ weird v -> s2Z (cplt2 v) = - (s2Z v).

Lemma sext_s2Z : forall l (v : int l) n, s2Z (sext n v) = s2Z v.

Definition Z2s n (l : Z) : int n := mk_int (adjust_slist (Z2slst l) n) (len_adjust_slist n _).

Lemma s2Z_Z2s' : forall (z : Z) m, - 2 ^^ m < z < 2 ^^ m -> s2Z (Z2s (S m) z) = z.

Lemma s2Z_Z2s'': forall z m, z = - 2^^m -> s2Z (Z2s (S m) z) = z.

Lemma s2Z_Z2s : forall z m, - 2 ^^ m <= z < 2 ^^ m -> s2Z (Z2s (S m) z) = z.

Lemma Z2s_dis n a b : - 2 ^^ n <= a < 2 ^^ n -> - 2 ^^ n <= b < 2 ^^ n ->
  a <> b -> Z2s (S n) a <> Z2s (S n) b.

Lemma sext_Z2s : forall m z n, - 2 ^^ m <= z < 2 ^^ m ->
  sext n (Z2s (S m) z) = Z2s (S m + n) z.

Lemma s2Z_u2Z_pos : forall l (a : int l), 0 <= s2Z a -> s2Z a = u2Z a.

Lemma s2Z_u2Z_pos' : forall n (a:int n), 0 <= u2Z a < 2^^(Coq.Init.Peano.pred n) -> s2Z a = u2Z a.

Lemma s2Z_u2Z_neg : forall (l:nat) (a:int l), s2Z a < 0 -> u2Z a = s2Z a + 2^^l.

Lemma u2Z_Z2s_neg' : forall (p:positive) l, - 2^^(Coq.Init.Peano.pred l) < Zneg p < 0 ->
  u2Z (Z2s l (Zneg p)) = 2^^l - Zpos p.

Lemma Z2s_weird : forall n, u2Z (Z2s n.+1 ( - 2 ^^ n)) = 2 ^^ n.

Lemma u2Z_Z2s_neg : forall z n, - 2 ^^ (Peano.pred n) <= z < 0 -> u2Z (Z2s n z) = 2 ^^ n + z.

Lemma u2Z_Z2s_zero : forall n, u2Z (Z2s n Z0) = Z0.

Lemma u2Z_Z2s_pos_old : forall z n, 0 < z < 2 ^^ (Peano.pred n) -> u2Z (Z2s n z) = z.

Lemma u2Z_Z2s_pos : forall z n, 0 <= z < 2 ^^ (Peano.pred n) -> u2Z (Z2s n z) = z.

correctness of the addition w.r.t. relative integers

Lemma s2Z_add: forall n (a b : int' (S n)), - 2 ^^ n <= s2Z a + s2Z b < 2 ^^ n -> s2Z (a [.+] b) = s2Z a + s2Z b.

correctness of the signed multiplication w.r.t. relative integers

Lemma s2Z_smul : forall n (a b : int n), s2Z (smul a b) = s2Z a * s2Z b.

Lemma s2Z_shl : forall n l (x : int l) l', (n + S l' <= l)%coq_nat -> - 2 ^^ l' <= s2Z x < 2 ^^ l' ->
  s2Z (shl n x) = s2Z x * 2^^n.

Lemma s2Z_sra : forall n (a : int (S n)) m, s2Z a < 0 ->
  (n < m)%coq_nat ->
  bits (shra m a) = ListBit.ones (S n).

Lemma s2Z_sra_pos : forall n (a : int (S n)) m, 0 <= s2Z a ->
  (n < m)%coq_nat ->
  bits (shra m a) = ListBit.zeros (S n).

Lemma shrl_sign_bit : forall (n : nat) (a : int (power 2 n)),
a [.>>] (power 2 n - 1) = Z2u (power 2 n) 0 \/ a [.>>] (power 2 n - 1) = Z2u (power 2 n) 1.

Lemma bZsgn_Zsgn_s2Z : forall (n : nat) (a : int (power 2 n)), u2Z a <> 0 ->
  bZsgn (u2Z (a [.>>] (power 2 n - 1))) = Zsgn (s2Z a).

Fixpoint partial_map (A B : Type) (a : list (list A))
  (f : list A -> B) : list B :=
  match a with
    | nil => nil
    | hd :: tl => f hd :: partial_map tl f
  end.

Lemma len_partial_map : forall (A B : Type) (a : list (list A)) (f : list A -> B),
  length (partial_map a f) = @length (list A) a.

Definition int_div_list : forall n k q, n = (q * k)%coq_nat ->
  forall (a : int n), list (int k).

Lemma len_int_div_list : forall (n k q : nat) (Hn : n = (q * S k)%coq_nat) (a : int n),
  Datatypes.length (int_div_list _ _ Hn a) = q.

Definition int_mul_list : forall n k q, n = (q * k)%coq_nat -> list (int k) -> option (int n).

Lemma int_mul_list_Some : forall n k q (H : n = (q * k)%coq_nat) (l : list (int k)),
  length l = q ->
  exists x, int_mul_list q H l = Some x.

Lemma int_mul_list_None : forall n k q (H : n = (q * k)%coq_nat) (l : list (int k)),
  k <> O -> length l <> q -> int_mul_list q H l = None.

Lemma int_mul_list_firstn : forall n k q (H : n = (q * k)%nat) (l : list (int k)) x x',
  k <> O -> int_mul_list q H l = Some x ->
  int_mul_list q H (firstn n l) = Some x' -> x = x'.

Lemma int_lst_injection : forall n, injection (fun x : int n => int_lst x).

Lemma int_mul_list_inj : forall n k l1 l2 nk x, n <> O ->
  forall (H : nk = (k * n)%nat),
    int_mul_list k H l1 = Some x -> int_mul_list k H l2 = Some x ->
    l1 = l2.

Lemma flat_map_id' : forall (q n k : nat) (a : list bool),
  length a = n -> n = (q * S k)%coq_nat ->
  flat_map (fun x0 : int' k.+1 => int_lst x0)
  (partial_map (firstns' k.+1 (length a) a)
    (fun x0 => mk_int (adjust_ulist x0 k.+1)
      (eq_ind_r (fun x => x = k.+1) (eq_refl k.+1)
        (len_adjust_ulist k.+1 x0)))) = a.

Lemma int_mul_div_list : forall n k q (a : int n) (Hn : (n = q * S k)%nat),
  int_mul_list q Hn (int_div_list (S k) q Hn a) = Some a.

Local Close Scope machine_int_scope.

End MachineInt.

Import MachineInt.

Local Open Scope machine_int_scope.

Lemma sext_0 : forall n m, sext n (Z2u m 0) = Z2u (m + n) 0.

Local Open Scope eqmod_scope.

Lemma add_0_L : forall n x, Z2u n 0 [.+] x = x.

Lemma u2Z_add_eqmod : forall n (a b : int n), u2Z (a [.+] b) =m u2Z a + u2Z b {{ 2^^n }}.

Lemma add_Z2u : forall l a b, 0 <= a -> 0 <= b ->
  Z2u l a [.+] Z2u l b = Z2u l (a + b).

Lemma u2Z_add_Z2u : forall n (a : int n) b, 0 <= b -> u2Z a + b < 2 ^^ n ->
  u2Z (a [.+] Z2u n b) = u2Z a + b.

Lemma u2Z_add_Z_of_nat : forall n (a : int n) b,
  u2Z a + Z_of_nat b < 2 ^^ n -> u2Z (a [.+] Z2u n (Z_of_nat b)) = u2Z a + Z_of_nat b.

Lemma u2Z_add_Z2s : forall n (a : int (S n)) b,
  - 2 ^^ n < b < 0 -> 0 <= u2Z a + b -> u2Z (a [.+] Z2s (S n) b) = u2Z a + b.

Lemma u2Z_add_Z2u_overflow : forall l (a : int (S l)), u2Z (a [.+] Z2u (S l) 1) = 0 ->
  u2Z a = 2 ^^ (S l) - 1.

Lemma u2Z_add_plus_u2Z_s2Z : forall n (a b : int n), 0 <= u2Z a + s2Z b < 2 ^^ n ->
  u2Z (a [.+] b) = u2Z a + s2Z b.

Lemma lt_n_irrefl : forall n (a : int n), ~ a [.<] a.

Lemma u2Z_add_no_overflow : forall n (a b : int n), u2Z a <= u2Z (a [.+] b) ->
  u2Z a + u2Z b < 2 ^^ n.

Lemma u2Z_add_overflow' : forall n (a b: int n), u2Z (a [.+] b) < u2Z a ->
  2^^n <= u2Z a + u2Z b.

Lemma u2Z_add_mod' : forall (n:nat) (a : int n) m k,
  0 <= k -> (u2Z a) mod m = 0 ->
  0 <= k * m -> (2 ^^ n) mod m = 0 ->
  u2Z (a [.+] Z2u n (k * m)) mod m = 0.

Lemma u2Z_add_mod : forall n (a : int n) m,
  (u2Z a) mod m = 0 -> 0 <= m ->
  (2 ^^ n) mod m = 0 ->
  u2Z (a [.+] Z2u n m) mod m = 0.

Definition scale n (a : int n) (m : nat) (k : nat) : int n := a [.+] Z2u n (Z_of_nat (m * k)).

Definition scalez n (a : int n) (m : nat) (k : Z) : int n :=
  if Zle_bool 0 k then a [.+] Z2u n (Z_of_nat m * k) else a [.-] Z2u n (Z_of_nat m * k).

Lemma scale_prop : forall n (a : int n) (m : nat),
  (u2Z a) mod (Z_of_nat m) = 0 ->
  (2 ^^ n) mod (Z_of_nat m) = 0 ->
  forall (k : nat), (u2Z (scale a m k)) mod (Z_of_nat m) = 0%Z.

Lemma add_n_lt_n : forall n (a b : int (S n)), a [.<] b ->
  a [.+] Z2u (S n) 1 [.<=] b.

Lemma max_u2Z_umul : forall l (a b : int l), u2Z (a [.*] b) <= (2 ^^ l - 1) * (2 ^^ l - 1).

Lemma umul_assoc : forall l (a b c : int l), (a [.*] b) [.*] zext l c = zext l a [.*] (b [.*] c).

Lemma umul_add_distr : forall l (a b c : int l), u2Z b + u2Z c < 2 ^^ l ->
  a [.*] (b [.+] c) = (a [.*] b) [.+] (a [.*] c).

Lemma shl_0 : forall n m, shl n (Z2u m 0) = Z2u m 0.

Lemma shl_Z2u : forall l (a : int l) k, shl k a = Z2u l (u2Z a * 2 ^^ k).

Lemma shrl_2 : forall (v : int 32) z, u2Z v = 4 * z -> v [.>>] 2 = Z2u 32 z.

Lemma u2Z_shrl' : forall n (x : int n) k, (n >= k)%nat ->
  u2Z (x [.>>] k) = u2Z x / 2 ^^ k.

Some constants:

Definition one5 := Z2u 5 1.
Definition two5 := Z2u 5 2.
Definition thirtyone5 := Z2u 5 31.
Definition zero16 := Z2u 16 0.
Definition one16 := Z2u 16 1.
Definition four16 := Z2u 16 4.
Definition mone16 := MachineInt.Z2s 16 (-1)%Z.
Definition mfour16 := Z2s 16 (-4)%Z.
Definition zero8 := Z2u 8 0.
Definition zero32 := Z2u 32 0.
Definition one32 := Z2u 32 1.
Definition four32 := Z2u 32 4.

Definition int_32 := int 32.

Definition eq_int_32 (a b:int_32) : bool := Zeq_bool (u2Z a) (u2Z b).

Require Import ssrbool eqtype.
Require Import ZArith_ext.

Lemma eq_int32P : Equality.axiom eq_int_32.

Canonical Structure int_32_eqMixin := EqMixin eq_int32P.
Canonical Structure int_32_eqType := Eval hnf in EqType _ int_32_eqMixin.

Definition int_8 := int 8.

Definition eq_int_8 (a b : int_8) : bool := Zeq_bool (u2Z a) (u2Z b).

Lemma eq_int8P : Equality.axiom eq_int_8.

Canonical Structure int_8_eqMixin := EqMixin eq_int8P.
Canonical Structure int_8_eqType := Eval hnf in EqType _ int_8_eqMixin.