Library machine_int

Require Import ProofIrrelevance Lia.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import ssrZ ZArith_ext Init_ext ssrnat_ext seq_ext.
Require Import listbit listbit_correct order.


Reserved Notation "'`(' x ')_' n" (at level 9, format "'`(' x ')_' n").
Reserved Notation "'`(' x ')c_' n" (at level 9, format "'`(' x ')c_' n").
Reserved Notation "'`(' x ')s_' n" (at level 9, format "'`(' x ')s_' n").
Reserved Notation "'`(' x ')sc_' n" (at level 9, format "'`(' x ')sc_' n").
Reserved Notation "a '`<' b" (at level 75, format "'[' a `< b ']'").
Reserved Notation "a '`<=' b" (at level 75, format "'[' a `<= b ']'").
Reserved Notation "a '`+' b" (at level 35, format "'[' a `+ b ']'").
Reserved Notation "a '`-' b" (at level 35, format "'[' a `- b ']'").
Reserved Notation "a '`*' b" (at level 50, format "'[' a `* b ']'").
Reserved Notation "a '`%' n" (at level 50, format "'[' a `% n ']'").
Reserved Notation "a '`<<' n" (at level 50, format "'[' a `<< n ']'").
Reserved Notation "a '`>>' n" (at level 50, format "'[' a `>> n ']'").
Reserved Notation "a '`&' b" (at level 50).
Reserved Notation "a '`|`' b" (at level 50, format "'[' a `|` b ']'").
Reserved Notation "a '`(+)' b" (at level 50).
Reserved Notation "a '`||' b " (at level 68, left associativity, format "'[' a `|| b ']'").

Declare Scope machine_int_scope.

Set Implicit Arguments.
Unset Strict Implicit.

Local Close Scope N_scope.
Local Open Scope zarith_ext_scope.

Inductive int n : Type := mk_int (lst : list bool) of size lst = n.

Module Type MACHINE_INT.

Parameter make_int : forall (n : nat) (lst : list bool), size lst = n -> int n.
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_subnK {k n : nat} (H : (k <= n)%nat) := cast subnK H.
Definition cast_subnKC {k n : nat} (H : (k <= n)%nat) := cast subnKC H.
Parameter castC : forall {n m : nat} (H : n = m), int n -> int m.
Parameter castA : forall {n m k} (H : (n + (m + k) = n + m + k)%nat),
  int (n + (m + k)) -> int (n + m + k).

Parameter u2Z : forall n, int n -> Z.
Parameter u2Zc : forall n, int n -> Z.
Parameter u2ZE : forall n (a : int n), u2Z a = u2Zc a.
Parameter max_u2Z : forall n (a : int n), u2Z a < 2 ^^ n.
Parameter min_u2Z : forall n (a : int n), 0 <= u2Z a.
Arguments min_u2Z [n] _ _.
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 u2Z_eq_rect : forall n (a : int n) m (H : n = m),
  u2Z (eq_rect _ _ a _ H) = u2Z a.
Parameter u2Z_castC :
  forall m n (a : int n) (H : n = m), u2Z (castC H a) = u2Z a.
Parameter u2Z_castA : forall n m k (a : int _) (H : (n + (m + k) = n + m + k)%nat),
  u2Z (castA H a) = u2Z a.

Parameter bits : forall (n : nat), int n -> list bool.
Parameter size_bits : forall n (a : int n), size (bits a) = n.
Parameter bits2u : forall n : nat, list bool -> int n.
Parameter u2Z_bits2u_u2Z : forall n l, size l = n -> u2Z (bits2u n l) = bitZ.u2Z l.

Parameter Z2u : forall n (z : Z), int n.
Parameter Z2uc : forall n (z : Z), int n.
Notation "'`(' x ')_' n" := (Z2u n x) : machine_int_scope.
Notation "'`(' x ')c_' n" := (Z2uc n x) : machine_int_scope.
Local Open Scope machine_int_scope.
Parameter Z2uE : forall n (z : Z), `( z )_ n = `( z )c_ n.
Parameter Z2uK : 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) = bits.zeros n.
Parameter Z2u_inj : forall n a b, (0 <= a < 2 ^^ n)%Z -> (0 <= b < 2 ^^ n)%Z ->
  Z2u n a = Z2u n b -> a = b.

Parameter zext : forall m n, int n -> int (m + n).
Parameter zext_zext : forall n (a : int n) m k, castA (@addnA _ _ _) (zext k (zext m a)) = (zext (k + m) a).
Parameter zext_Z2u : forall n m m', n < 2 ^^ m -> zext m' (Z2u m.+1 n) = Z2u (m' + m.+1) n.
Parameter u2Z_zext : forall k n (a : int n), u2Z (zext k a) = u2Z a.

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

Parameter lt_n : forall n, int n -> int n -> bool.
Notation "a '`<' b" := (lt_n a b) : 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) : machine_int_scope.
Parameter le_n_refl : forall n (a : int n), a `<= a.
Parameter le_nE : forall n (a b : int n), a `<= b -> a = b \/ a `< b.

Parameter add : forall n, int n -> int n -> int n.
Notation "a '`+' b" := (add a b) : machine_int_scope.
Parameter addC : forall n (a b : int n), a `+ b = b `+ a.
Parameter addA : forall n (a b c : int n), (a `+ b) `+ c = a `+ (b `+ c).
Parameter addi0 : forall n (a : int n), a `+ Z2u n 0 = a.

Parameter sub : forall n, int n -> int n -> int n.
Notation "a '`-' b" := (sub a b) : machine_int_scope.

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) : machine_int_scope.
Parameter umulC : 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).

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

Parameter shl : forall (m : nat) n (a : int n), int n.
Notation "a '`<<' n" := (shl n a) : 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) = bits.zeros m ++ true::nil ++ bits.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_ext : forall m n (a : int n), int (m + n).

Parameter shrl : nat -> forall n, int n -> int n.
Notation "a '`>>' n" := (shrl n a) : 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.
Parameter shrl_rem : forall n (a : int n) k k' (kk' : (n = k + k')%nat),
  (zext k ((a `>> k )`% k')) = @eq_rect _ _ _ (a `>> k) _ kk'.

Parameter shra : nat -> forall n, int n -> int n.
Parameter shr_shrink : forall m n (a : 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) : machine_int_scope.

Parameter int_and_0 : forall n a, a `& Z2u n 0 = Z2u n 0.
Parameter int_andC : 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_subnK 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) : machine_int_scope.

Parameter int_or_0 : forall n (a : int n), a `|` Z2u n 0 = a.
Parameter int_orC : 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) = bits.or (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_subnK H (zext (n - k) (a `% k))).

Parameter int_xor : forall n, int n -> int n -> int n.
Notation "a '`(+)' b" := (int_xor a b) : machine_int_scope.

Parameter int_xor_0 : forall n (a : int n), a `(+) Z2u n 0 = a.
Parameter int_xorC : forall n (a b : int n), a `(+) b = b `(+) a.
Parameter int_xorA : 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 a, a `& int_not (Z2u n 0) = a.

Parameter int_not_or : forall n (a b : int n), int_not (a `|` b) = int_not a `& int_not b.

Parameter int_xor_1s : forall n (a : int n), a `(+) int_not (Z2u n 0) = int_not a.

Parameter cplt2 : forall n, int n -> int n.
Parameter cplt2_zero : forall n, cplt2 (Z2u n 0) = Z2u n 0.
Parameter cplt2_1s : forall n, cplt2 (int_not (Z2u n 0)) = Z2u n 1.
Parameter not_add_1_cplt2: forall n (v : int n), (n > 1)%nat -> int_not v `+ Z2u n 1 = cplt2 v.
Parameter cplt2_inj : forall n (a b : int n), cplt2 a = cplt2 b -> a = b.
Parameter sub_cplt2 : forall n (a b : int n.+1), a `- b = a `+ cplt2 b.

Parameter concat : forall n m (a : int n) (b : int m), int (n + m).
Notation "a '`||' b " := (concat a b) : machine_int_scope.
Parameter zext_concat : forall n (a : int n) m, zext m a = `( 0 )_ m `|| a.
Parameter concatA : forall k m n (a : int k) (b : int m) (c : int n),
  a `|| b `|| c = castA (@addnA _ _ _) (a `|| (b `|| c)).

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_subnK Hkn ((shr_shrink k b) `|| (a `% k)).
Parameter rem_concat : forall n (a : int n) m (b : int m), (a `|| b) `% m = b.
Parameter concat_shl : forall n (a : int n) m,
  a `|| Z2u m 0 = castC (@addnC _ _) (zext m a `<< m).

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 cast_shl : forall n k (a : int k) (Hkn : (k <= n)%nat) m (kmn : (k + m <= n)%nat),
  cast_subnK Hkn (zext (n - k) a `<< m) = (cast_subnK Hkn (zext (n - k) a )) `<< m.
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_ext : forall k n (x : int n), u2Z (shl_ext k x) = u2Z x * 2 ^^ k.
Parameter u2Z_shl_ext' : forall n (x : int n), forall m, u2Z x < 2 ^^ m -> forall k,
  u2Z (shl_ext k x) <= 2 ^^ (m + k) - 2 ^^ k.
Parameter u2Z_shl_ext'' : forall l (x : int l), forall k, u2Z x < 2 ^^ k -> forall n,
  u2Z (shl_ext 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_or : forall m n (a : int m) (b : int n),
  u2Z ((a `|| Z2u n 0) `|` zext m b) = (u2Z a * 2 ^^ n + u2Z b)%Z.

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 ^^ k.+1 * a' -> u2Z (a `% k.+1) = 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 le_n2Zle : forall n (a b:int 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 s2Zc : forall n, int n -> Z.
Parameter s2ZE : forall n (a : int n), s2Z a = s2Zc a.
Parameter max_s2Z : forall n (a : int n), s2Z a < 2 ^^ n.-1.
Parameter min_s2Z : forall n (a : int n.+1), - 2 ^^ n <= s2Z a.
Parameter s2Z_zext : forall k n (a : int n), (0 < k)%nat -> s2Z (zext k a) = u2Z a.
Arguments s2Z_zext _ [n] _ _.
Parameter s2Z_inj : forall n (v w : int n), s2Z v = s2Z w -> v = w.
Parameter s2Z_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,
  s2Z (cast H Hkn a) = s2Z a.
Parameter s2Z_castA : forall k m n (a : int (k + (m + n))),
                    s2Z (castA (@addnA _ _ _) a) = s2Z a.

Parameter weird : forall n (v : int n.+1), Prop.
Parameter weirdE : forall n (a : int n.+1), weird a <-> u2Z a = 2 ^^ n.
Parameter weirdE2 : forall n (a : int n.+1), weird a <-> s2Z a = - 2 ^^ n.

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

Parameter Z2s : forall n (z : Z), int n.
Parameter Z2sc : forall n (z : Z), int n.
Notation "'`(' x ')s_' n" := (Z2s n x) : machine_int_scope.
Notation "'`(' x ')sc_' n" := (Z2sc n x) : machine_int_scope.
Parameter Z2sE : forall n (z : Z), `( z )s_ n = `( z )sc_ n.
Parameter Z2sK : forall z m, - 2 ^^ m <= z < 2 ^^ m -> s2Z (`( z )s_m.+1) = z.
Parameter Z2s_dis : forall n a b, - 2 ^^ n <= a < 2 ^^ n -> - 2 ^^ n <= b < 2 ^^ n ->
  a <> b -> `( a )s_n.+1 <> `( b )s_n.+1.
Parameter int_even_and_1_converse : forall n (a : int n), a `& Z2u n 1 = Z2u n 0 -> Zeven (s2Z a).
Parameter sext_Z2s : forall m z n, - 2 ^^ m <= z < 2 ^^ m -> sext n (`( z )s_m.+1) = `( z)s_(m.+1 + n).

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 ^^ n.-1 -> 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 (`(- 2 ^^ n)s_n.+1) = 2 ^^ n.
Parameter u2Z_Z2s_neg : forall z n, - 2 ^^ n.-1 <= z < 0 -> u2Z (`( z )s_ n) = 2 ^^ n + z.
Parameter u2Z_Z2s_pos : forall z n, 0 <= z < 2 ^^ n.-1 -> u2Z (`( z )s_ n) = z.

Parameter s2Z_add: forall n (a b : int n.+1), - 2 ^^ n <= s2Z a + s2Z b < 2 ^^ n -> s2Z (a `+ b) = s2Z a + s2Z b.
Parameter s2Z_sub: forall n (a b : int n.+1), (- 2 ^^ n <= s2Z a - s2Z b < 2 ^^ n)%Z -> s2Z (a `- b) = (s2Z a - s2Z b)%Z.
Parameter Z2s_Z2u_k : forall n k, 0 <= k < 2 ^^ n -> `( k )s_ n = `( k )_ n.

Parameter s2Z_smul : forall n (a b : int n), s2Z (smul a b) = s2Z a * s2Z b.
Parameter s2Z_shl : forall m k n (x : int n), (k + m.+1 <= n)%nat -> - 2 ^^ m <= s2Z x < 2 ^^ m ->
  s2Z (shl k x) = s2Z x * 2 ^^ k.
Parameter bits_shra_neg : forall n (a : int n.+1) m, s2Z a < 0 ->
  (n <= m)%nat ->
  bits (shra m a) = bits.ones n.+1.
Parameter bits_shra_nonneg : forall n (a : int n.+1) m, 0 <= s2Z a ->
  (n <= m)%nat ->
  bits (shra m a) = bits.zeros n.+1.
Parameter s2Z_shra_neg : forall n (a : int n.+1) m, s2Z a < 0 -> (n <= m)%nat ->
  shra m a = int_not (Z2u n.+1 0).
Parameter s2Z_shra_pos : forall n (a : int n.+1) m, 0 <= s2Z a -> (n <= m)%nat ->
  shra m a = Z2u n.+1 0.
Parameter le0concat : forall m n (a : int n), (0 <= s2Z ( `( 0 )_m.+1 `|| a))%Z.

Parameter shrl_sign_bit : forall (n : nat) (a : int (2 ^ n)),
 a `>> (2 ^ n - 1) = Z2u (2 ^ n) 0 \/ a `>> (2 ^ n - 1) = Z2u (2 ^ n) 1.
Parameter bZsgn_Zsgn_s2Z : forall (n : nat) (a : int (2 ^ n)), u2Z a <> 0 ->
  bZsgn (u2Z (a `>> (2 ^ n - 1))) = sgZ (s2Z a).
Parameter le0_or : forall n (a b : int n.+1),
  0 <=? s2Z a -> 0 <=? s2Z b -> 0 <=? s2Z (a `|` b).

Local Close Scope machine_int_scope.

Parameter int_break : forall n k q, n = (q * k)%nat -> forall (a : int n), list (int k).
Parameter size_int_break : forall (n k q : nat) (Hn : n = (q * k.+1)%nat) (a : int n),
    size (int_break Hn a) = q.
Parameter int_break_cons :
  forall n k q v (H : n = (q.+1 * k)%nat) (H' : (n - k)%nat = (q * k)%nat),
  k <> O ->
  int_break H v = Z2u k (u2Z v / 2 ^^ (n - k)) :: int_break H' (Z2u (n - k) (u2Z v)).
Parameter int_flat : forall n k q, n = (q * k)%nat -> list (int k) -> option (int n).
Parameter int_flat_Some : forall n k q (H : n = (q * k)%nat) (l : list (int k)),
  size l = q -> { x | int_flat H l = Some x }.
Parameter int_flat_None : forall n k q (H : n = (q * k)%nat) (l : list (int k)),
  k <> O -> size l <> q -> int_flat H l = None.
Parameter int_flat_ok :
  forall n k q (H: n = (q * k)%nat) (l : list (int k)) (Hl : size l = q), int n.
Parameter int_flat_ok_id : forall n (a : int n) H H',
    @int_flat_ok n n 1 H (a :: nil) H' = a.
Parameter int_flat_take : forall n k q (H : n = (q * k)%nat) (l : list (int k)) x x',
  k <> O -> int_flat H l = Some x ->
  int_flat H (take n l) = Some x' -> x = x'.
Parameter int_flat_inj : forall n k l1 l2 nk x,
  n != O -> forall (H : nk = (k * n)%nat),
  int_flat H l1 = Some x ->
  int_flat H l2 = Some x ->
  l1 = l2.

Parameter int_flat_ok_inj : forall n k q H l1 Hl1 l2 Hl2, (k != 0)%nat ->
  @int_flat_ok n k q H l1 Hl1 = @int_flat_ok n k q H l2 Hl2 ->
  l1 = l2.

Parameter int_flat_int_flat_ok : forall n k q (Hn : (n = q * k)%nat) a a' H,
  @int_flat n k q Hn a = Some a' -> @int_flat_ok n k q Hn a H = a'.
Parameter int_flat_ok_int_flat : forall (n k q : nat) (Hn : (n = q * k)%nat)
  (a : list (int k)) (a' : int n) (H : size a = q),
  int_flat_ok Hn H = a' -> int_flat Hn a = Some a'.

Parameter int_flat_int_break : forall n k q (a : int n) (Hn : (n = q * k)%nat),
  int_flat Hn (int_break Hn a) = Some a.
Parameter int_flat_break :
  forall q n k (a : list (int k.+1)) (b : int n) (Hn : (n = q * k.+1)%nat),
  int_flat Hn a = Some b -> int_break Hn b = a.
Parameter int_break_flat : forall (n k q : nat) (Hn : (n = q * k)%nat)
  (a : list (int k)) (a' : int n) (H : size a = q),
  int_break Hn a' = a -> int_flat Hn a = Some a'.
Parameter int_break_0 : forall q n k (H : n = (q * k.+1)%nat),
  int_break H (Z2u n 0) = nseq q (Z2u k.+1 0).
Parameter int_break_inj : forall n k nk (l1 l2 : int nk) ,
  n <> O -> forall (H : nk = (k * n)%nat),
  int_break H l1 = int_break H l2 ->
  l1 = l2.

End MACHINE_INT.

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

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

Module MachineInt : MACHINE_INT
with Definition u2Zc := fun n (a : int n) => match a with mk_int lst _ => bitZ.u2Z lst end
with Definition s2Zc := fun n (a : int n) => match a with mk_int lst _ => bitZ.s2Z lst end
with Definition Z2uc := fun n (l : Z) => mk_int (bits.size_adjust_u n (bitZ.Z2u l))
with Definition Z2sc := fun n (l : Z) => mk_int (bits.size_adjust_s n (bitZ.Z2s l))
with Definition add := fun l (a b : int l) => mk_int
  (bits.size_add l (int_lst a) (int_lst b) (int_prf a) (int_prf b) false)
with Definition int_and := fun n (a b : int n) =>
  mk_int (bits.size_and n (int_lst a) (int_lst b) (int_prf a) (int_prf b))
with Definition int_or := fun n (a b : int n) =>
  mk_int (bits.size_or n (int_lst a) (int_lst b) (int_prf a) (int_prf b))
with Definition int_xor := fun n (a b : int n) =>
  mk_int (bits.size_xor n (int_lst a) (int_lst b) (int_prf a) (int_prf b))
with Definition shl := fun m n (a: int n) => mk_int (bits.size_shl m n (int_lst a) (int_prf a))
with Definition shrl := fun m n (a : int n) => mk_int (bits.size_shrl n m (int_lst a) (int_prf a))
with Definition mul := fun n (a b : int n) => mk_int
  (bits.size_adjust_u n (bits.umul (int_lst a) (int_lst b))).

Definition make_int : forall (n : nat) (lst : list bool), size lst = n -> int n := mk_int.

Lemma mk_int_pi : forall n l (H : size l = n) l' (H' : size l' = n),
  l = l' -> mk_int H = mk_int H'.
Proof. move=> n l H l' H' H''; subst l; by rewrite (proof_irrelevance _ H H'). Qed.

Lemma mk_int_pi' : forall n l (H : size l = n) n' l' (H' : size l' = n') (n_n' : n = n'),
  l = l' -> eq_rect n int (mk_int H) _ n_n' = mk_int H'.
Proof.
move=> n l H n' l' H' n_n' H''; subst l'.
move: (n_n') H H'.
rewrite n_n' => {}n_n'.
have : n_n' = refl_equal n'.
apply proof_irrelevance.
rewrite /eq_rect.
move=> -> H H'; by apply mk_int_pi.
Qed.


Lemma mk_int_pi'' : forall n l (H : size l = n) n' (n_n' : n = n'),
  int_lst (eq_rect n int (mk_int H) _ n_n') = l.
Proof.
move=> n l H n' n_n'.
move: (n_n') H.
rewrite n_n' => {}n_n'.
have : n_n' = refl_equal n' by apply proof_irrelevance.
by move=> ->.
Qed.

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


Lemma dec_int : forall l (a b : int l), { a = b } + { a <> b }.
Proof.
move=> l [a Ha] [b Hb] /=.
elim (bits.dec_equ_lst_bit a b) => H.
- left; subst a; by apply: mk_int_pi.
- right; by move=> [H'].
Qed.

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.
Proof. exact (fun x => eq_rect (f k n) _ x n (HPf k n HP)). Defined.

Definition cast_subnK {k n : nat} (H : (k <= n)%nat) := cast subnK H.
Definition cast_subnKC {k n : nat} (H : (k <= n)%nat) := cast subnKC H.

Definition castC {n m : nat} (H : n = m) : int n -> int m.
move=> a.
exact match a with
 | mk_int lst e =>
     mk_int
       ((fun x : size lst = n =>
         eq_ind n (fun y : nat => size lst = y)
           x m H) e)
 end.
Defined.

Definition castA {n m k} (H : (n + (m + k) = n + m + k)%nat) : int (n + (m + k)) -> int (n + m + k).
move=> a.
exact match a with
 | mk_int lst e =>
     mk_int
       ((fun x : size lst = (n + (m + k))%nat =>
         eq_ind (n + (m + k))%nat (fun y : nat => size lst = y)
           x (n + m + k)%nat H) e)
 end.
Defined.

Definition u2Z len (a : int len) : Z := match a with mk_int lst _ => bitZ.u2Z lst end.
Definition u2Zc len (a : int len) : Z := match a with mk_int lst _ => bitZ.u2Z lst end.
Lemma u2ZE : forall n (a : int n), u2Z a = u2Zc a. Proof. done. Qed.

Lemma max_u2Z : forall l (a : int l), u2Z a < 2 ^^ l.
Proof. move=> l [lst H] /=. apply bitZ.max_u2Z; by rewrite H. Qed.

Lemma min_u2Z n : forall (a : int n), 0 <= u2Z a.
Proof. case=> l H /=; by apply bitZ.min_u2Z. Qed.
Arguments min_u2Z [n] _ _.

Lemma u2Z_inj : forall l (v w : int l), u2Z v = u2Z w -> v = w.
Proof.
move=> l [vl Hv] [wl Hw] /= H.
apply: mk_int_pi.
by eapply bitZ.u2Z_inj; eauto.
Qed.

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.
Proof.
move=> f P H k n Hkn [a Ha] /=.
rewrite /cast /eq_rect.
move: (H k n Hkn).
move: Ha.
rewrite H // => Ha H0.
suff : H0 = refl_equal n by move=> ->.
by apply proof_irrelevance.
Qed.

Lemma u2Z_eq_rect : forall n (a : int n) m (H : n = m),
  u2Z (eq_rect _ _ a _ H) = u2Z a.
Proof.
move=> n [a Ha] /= m H.
rewrite (@mk_int_pi' n a Ha m a) //.
by subst.
Qed.

Lemma u2Z_castC : forall m n (a : int n) (H : n = m), u2Z (castC H a) = u2Z a.
Proof. by move=> m n []. Qed.

Lemma u2Z_castA : forall n m k (a : int _) (H : (n + (m + k) = n + m + k)%nat), u2Z (castA H a) = u2Z a.
Proof. by move=> n m k []. Qed.

Lemma size_bits : forall n (a : int n), size (bits a) = n.
Proof. move=> n [a H]. by rewrite /bits size_rev. Qed.

Definition bits2u n (l : list bool) : int n := mk_int (bits.size_adjust_u n l).

Lemma u2Z_bits2u_u2Z n l : size l = n -> u2Z (bits2u n l) = bitZ.u2Z l.
Proof.
move=> H.
rewrite /bits2u /= /bits.adjust_u.
have -> : (size l < n)%nat = false by rewrite H ltnn.
rewrite (bitZ.skipn_Zmod (size l)) //; last first.
  by rewrite H /= -minusE /= -minus_n_n.
have -> : (size l - (size l - n) = n)%nat.
  rewrite subnBA //; last by rewrite H.
  by rewrite addnC addnK.
rewrite Zmod_small //.
split; [by apply bitZ.min_u2Z | apply bitZ.max_u2Z; by rewrite H].
Qed.

Definition Z2u n (l : Z) : int n := mk_int (bits.size_adjust_u n (bitZ.Z2u l)).
Definition Z2uc n (l : Z) : int n := mk_int (bits.size_adjust_u n (bitZ.Z2u l)).
Local Notation "'`(' x ')_' n" := (Z2u n x).
Notation "'`(' x ')c_' n" := (Z2uc n x) : machine_int_scope.
Local Open Scope machine_int_scope.

Lemma Z2uE : forall n z, `( z )_n = `( z )c_ n. Proof. done. Qed.

Lemma Z2uK z m : 0 <= z < 2 ^^ m -> u2Z `( z )_m = z.
Proof.
case=> H1 H2.
rewrite /u2Z /Z2u.
destruct z as [|p|p].
- by rewrite /= bits.adjust_u_nil bitZ.u2Z_zeros.
- destruct m as [|m].
  + by destruct p.
  + rewrite bitZ.adjust_u2Z; last first.
      apply bitZ.max_u2Z => /=.
      rewrite size_rev.
      by apply bitZ.pos2lst_len.
    by apply bitZ.Z2uK.
- by move: (Zlt_neg_0 p) => ?; lia.
Qed.

Lemma u2Z_Z2u_Zmod' : forall z n, 2 ^^ n <= z -> u2Z `( z )_n = z mod (2 ^^ n).
Proof.
move=> z n H.
rewrite /u2Z /Z2u.
destruct z as [|p|p].
- by rewrite /= bits.adjust_u_nil bitZ.u2Z_zeros.
- by rewrite bitZ.adjust_u2Z_overflow bitZ.Z2uK.
- by move: (Zlt_neg_0 p) (expZ_gt0 n) => ? ?; lia.
Qed.

Lemma u2Z_Z2u_Zmod : forall z n, 0 <= z -> u2Z (Z2u n z) = z mod (2 ^^ n).
Proof.
move=> z n H.
case: (Z_lt_le_dec z (2 ^^ n)) => X.
by rewrite Zmod_small // Z2uK.
by apply u2Z_Z2u_Zmod'.
Qed.

Lemma u2Z_Z2u_neg: forall z n, z < 0 -> u2Z (Z2u n z) = 0.
Proof. case=> //=. move=> p n _; by rewrite bits.adjust_u_nil bitZ.u2Z_zeros. Qed.

Lemma Z2u_dis l a b : 0 <= a < 2 ^^ l -> 0 <= b < 2 ^^ l ->
  a <> b -> Z2u l a <> Z2u l b.
Proof.
move=> Ha Hb Hab; contradict Hab.
by rewrite -(Z2uK Ha) // -(Z2uK Hb) // Hab.
Qed.

Lemma Z2u_u2Z : forall n (a : int n), Z2u n (u2Z a) = a.
Proof.
move=> n [lst Hlst] /=.
rewrite /Z2u.
apply mk_int_pi.
rewrite (bitZ.u2ZK _ _ Hlst).
have X : (size (bits.erase_leading_zeros lst) <= n)%nat.
  by apply bits.size_erase_leading_zeros.
rewrite (bits.adjust_u_S'' n _ (bits.erase_leading_zeros lst) (refl_equal _)).
by rewrite bits.erase_leading_zeros_prop.
exact X.
Qed.

Lemma bits_zeros : forall n, bits (Z2u n 0) = bits.zeros n.
Proof. move=> n /=. by rewrite /bits /= bits.adjust_u_nil bits.rev_zeros. Qed.

Lemma Z2u_inj {n} : forall a b, (0 <= a < 2 ^^ n)%Z -> (0 <= b < 2 ^^ n)%Z ->
  Z2u n a = Z2u n b -> a = b.
Proof.
move=> a b Ha Hb ab.
have {}ab : u2Z (Z2u n a) = u2Z (Z2u n b) by rewrite ab.
by rewrite !Z2uK in ab.
Qed.

Definition zext m n (a : int n) : int (m + n) :=
  mk_int (bits.size_zext n (int_lst a) m (int_prf a)).

Lemma zext_zext n (a : int n) m k : castA (@addnA _ _ _) (zext k (zext m a)) = (zext (k + m) a).
Proof. apply mk_int_pi => /=. by rewrite /bits.zext catA bits.zeros_app. Qed.

Lemma zext_Z2u n m m' : n < 2 ^^ m -> zext m' (Z2u m.+1 n) = Z2u (m' + m.+1) n.
Proof. move=> Hn. apply mk_int_pi => //=. by rewrite bitZ.zext_Z2u // -addSn addnC. Qed.

Lemma u2Z_zext : forall (k : nat) l (a : int l), u2Z (zext k a) = u2Z a.
Proof. move=> k l [a Ha] //. rewrite /u2Z /zext /=. by elim: k. Qed.

Lemma size_sext' m l k : size l = k -> size (bits.sext m l) = (k + m)%nat.
Proof. move=> <-. by rewrite bits.size_sext. Qed.

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

Lemma u2Z_sext : forall l (v:int l) n, 0 <= u2Z v < 2 ^^ l.-1 ->
  u2Z (sext n v) = u2Z v.
Proof. move=> l [v Hv] /= n H. by eapply bitZ.sext_u2Z; eauto. Qed.

Lemma sext_Z2u n m m' : n < 2 ^^ m -> sext m' (Z2u m.+1 n) = Z2u (m.+1 + m') n.
Proof. move=> Hn. apply mk_int_pi => //=. by rewrite bitZ.sext_Z2u. Qed.

Definition lt_n n (a b : int n) : bool := bits.ult (int_lst a) (int_lst b).
Notation "a '`<' b" := (lt_n a b) : machine_int_scope.

Definition le_n n (a b : int n) : bool := bits.ule (int_lst a) (int_lst b).
Notation "a '`<=' b" := (le_n a b) : machine_int_scope.

Lemma le_n_refl : forall n (a : int n), a `<= a.
Proof. move=> n a; rewrite /le_n /bits.ule. apply/orP; right; by apply bits.listbit_eq_refl. Qed.

Lemma le_nE : forall n (a b : int n), a `<= b -> a = b \/ a `< b.
Proof.
move=> n a b; rewrite /le_n /bits.ule.
case/orP => H.
right; by rewrite /lt_n.
left; move/bits.listbit_eq_eq in H.
destruct a; destruct b.
rewrite /= in H.
by apply mk_int_pi.
Qed.

Lemma lt_nW : forall n (a b : int n), a `< b -> a `<= b.
Proof. move=> n a b H; rewrite /le_n /bits.ule; apply/orP; by auto. Qed.

Definition add l (a b : int l) : int l := mk_int
  (bits.size_add l (int_lst a) (int_lst b) (int_prf a) (int_prf b) false).
Notation "a '`+' b" := (add a b) : machine_int_scope.

Lemma addC n : forall (a b : int n), a `+ b = b `+ a.
Proof. move=> [a Ha] [b Hb] /=. apply mk_int_pi => /=. by rewrite bits.addC. Qed.

Lemma addA n : forall (a b c : int n), (a `+ b) `+ c = a `+ (b `+ c).
Proof. move=> [a Ha] [b Hb] [c Hc]. apply mk_int_pi. by apply bits.addA with n. Qed.

Lemma addi0 : forall l (a : int l), a `+ Z2u l 0 = a.
Proof.
move=> l [lst prf].
rewrite /add /=.
apply mk_int_pi.
by rewrite bits.adjust_u_nil bits.addl0 // prf.
Qed.

Definition sub n (a b : int n) : int n := mk_int
  (bits.size_sub n (int_lst a) (int_lst b) false (int_prf a) (int_prf b)).
Notation "a '`-' b" := (sub a b) : machine_int_scope.

Definition mul n (a b : int n) : int n := mk_int
  (bits.size_adjust_u n (bits.umul (int_lst a) (int_lst b))).

Definition umul : forall l (a b : int l), int (l + l).
Proof.
move=> l [a Ha] [b Hb].
have H : size (bits.umul a b) = (l + l)%nat by rewrite bits.size_umul Ha Hb.
exact (mk_int H).
Defined.
Notation "a '`*' b" := (umul a b) : machine_int_scope.

Lemma umulC : forall l (a b : int l), a `* b = b `* a.
Proof.
move=> [|l] [ [|a0 a] Ha] [ [|b0 b] Hb] //.
rewrite (proof_irrelevance _ Ha Hb) // /umul.
apply mk_int_pi.
by apply (bits.umulC l.+1).
Qed.

Lemma umul_1 : forall l (x : int l), x `* `( 1 )_ l = zext l x.
Proof.
move=> l [lst prf].
rewrite /= /zext.
apply mk_int_pi => /=.
destruct l.
- by destruct lst.
- by rewrite (bits.adjust_u_S'' (l.+1) 1) //= subSS subn0 bits.umull1.
Qed.

Lemma umul_0 : forall n (x : int n), x `* `( 0 )_ n = `( 0 )_ (n + n).
Proof.
move=> n [x Hx] /=.
apply mk_int_pi => /=.
by rewrite 2!bits.adjust_u_nil bits.umull0 Hx.
Qed.

Lemma smul_lst_size_size : forall n (a b : int n),
  (size (bits.smul (int_lst a) (int_lst b)) = 2 * n)%nat.
Proof. move=> n [a Ha] [b Hb] /=; by rewrite (bits.size_smul n). Qed.

Definition smul n (a b : int n) : int (2 * n) := mk_int (smul_lst_size_size a b).

Definition rem n m (a : int m) : int n.
Proof. case: a => a Ha. exists (bits.adjust_u a n); by rewrite bits.size_adjust_u. Defined.
Notation "a '`%' n" := (rem n a) : machine_int_scope.

Lemma rem_Zpower : forall n k, (k < n)%nat -> Z2u n (2 ^^ k) `% k = Z2u k 0.
Proof.
move=> n k Hkn.
rewrite /Z2u.
apply mk_int_pi.
rewrite bits.adjust_u_nil bitZ.Z2u_2_Zpower /bits.adjust_u.
rewrite [size (_ :: _)]/= !size_nseq.
have [X|X] : (k.+1 < n \/ k.+1 < n = false)%nat by case (k.+1 < n)%nat; auto.
- rewrite X.
  rewrite (bits.size_zext k.+1); last by rewrite /= size_nseq.
  rewrite subnK //.
  have Y : (n < k = false)%nat. by apply/negbTE; rewrite -leqNgt ltnW.
  rewrite Y /bits.zext.
  rewrite -cat1s catA drop_size_cat //.
  by rewrite size_cat size_nseq addn1 -subSn //.
- rewrite X.
  rewrite size_drop [size (_ :: _)]/= size_nseq subKn; last by rewrite leqNgt X.
  rewrite ltnNge ltnW //.
  rewrite [drop]lock /= -lock.
  have -> : (succn k - n = 0)%nat.
    apply/eqP.
    by rewrite subn_eq0.
  rewrite drop0.
  have -> : n = succn k.
    move/negbT in X.
    rewrite -leqNgt in X.
    apply/eqP; rewrite eqn_leq.
    by rewrite X Hkn.
  by rewrite subSn // subnn /= drop0.
Qed.

Definition shl m n (a: int n) : int n := mk_int (bits.size_shl m n (int_lst a) (int_prf a)).
Notation "a '`<<' n" := (shl n a) : machine_int_scope.

Lemma shl_zero : forall n m, Z2u n 0 `<< m = Z2u n 0.
Proof. move=> n m; apply mk_int_pi => /=; by rewrite bits.adjust_u_nil bits.shl_zeros. Qed.

Lemma shl_1 : forall n k, (k <= n)%nat -> Z2u n 1 `<< k = Z2u n (2 ^^ k).
Proof.
move=> n k Hkn.
apply mk_int_pi => /=.
rewrite bitZ.Z2u_2_Zpower /bits.adjust_u /= size_nseq.
have [X|X] : (1 < n \/ 1 < n = false)%nat by destruct (1 < n)%nat; auto.
- rewrite X.
  have [Y|Y] : (k.+1 < n \/ k.+1 < n = false)%nat by destruct (k.+1 < n)%nat; auto.
  + rewrite Y /bits.zext (bits.shl_app' _ (n - 1)); last 2 first.
      by rewrite size_nseq.
      move/ltP in Y.
      apply/leP.
      by rewrite -minusE; lia.
    rewrite bits.skipn_zeros (_ : _ - _ - _ = n - k.+1)%nat //.
    move/ltP in Y.
    by rewrite -!minusE; lia.
  + rewrite Y.
    have [Z|Z] : (k = n \/ k = n-1)%nat.
      by rewrite -minusE; move/ltP in X; move/ltP in Y; move/leP in Hkn; lia.
    * subst k.
      rewrite (_ : n.+1 - n = 1)%nat /=.
      rewrite (bits.shl_overflow _ n) // ?drop0 // (bits.size_zext 1) //.
      rewrite subn1 addn1 prednK //.
      by apply: ltn_trans X.
      by rewrite subSn // subnn.
    * subst k.
      rewrite (_ : (n-1).+1 - n = 0)%nat /=; last first.
        rewrite -!minusE.
        by move/ltP in X; lia.
      rewrite /bits.zext (bits.shl_app' _ (n - 1)); last 2 first.
        by rewrite size_nseq.
        by apply leqnn.
      by rewrite bits.skipn_zeros subnn.
- rewrite X.
  move/leP in Hkn.
  destruct n => /=.
  move/leP in Hkn; by destruct k.
  destruct n => //.
  destruct k => //.
  move/leP in Hkn; by destruct k.
Qed.

Lemma bits_shl_1 n m : (m < n)%nat ->
  bits (Z2u n 1 `<< m) = bits.zeros m ++ true :: nil ++ bits.zeros (n - m - 1).
Proof.
move=> Hmn.
rewrite /Z2u /bits /bits.adjust_u /=.
case: ifP => X.
- rewrite /bits.zext (bits.shl_app' m (n - 1)); last 2 first.
    + by rewrite size_nseq.
    + by rewrite -(leq_add2r 1) 2!addn1 subn1 prednK // (ltn_trans _ X).
  rewrite rev_cat /= rev_cons -cats1 bits.rev_zeros bits.skipn_zeros bits.rev_zeros -catA /=.
  by rewrite -subnDA add1n -subnDA addn1.
- move/ltP : Hmn => Hmn.
  destruct n => //=.
  by move/ltP in Hmn; destruct m.
  move/ltP in Hmn; destruct n => //=.
  by destruct m.
Qed.

Lemma shl_rem_m : forall n (a : int n) m, (m <= n)%nat -> (a `<< m) `% m = Z2u m 0.
Proof.
move=> n [a Ha] m Hmn /=.
apply mk_int_pi => /=.
rewrite bits.adjust_u_nil /bits.adjust_u (bits.size_shl m n) //.
rewrite leqNgt in Hmn.
rewrite (negbTE Hmn).
subst n.
rewrite -leqNgt in Hmn.
rewrite -(cat_take_drop m a) size_cat.
rewrite bits.shl_cat; last first.
  rewrite size_take.
  case: ifP => // /negbT.
  rewrite -leqNgt => H1.
  by apply/eqP; rewrite eqn_leq H1.
rewrite drop_size_cat // size_drop size_take.
case: ifP => // H1.
  by rewrite addnC addnK.
move/negbT in H1.
rewrite -leqNgt in H1.
have /eqP <- : m == size a by rewrite eqn_leq Hmn H1.
by rewrite !(subnn, addn0).
Qed.

Definition shl_ext m n (a : int n) : int (m + n) :=
  mk_int (bits.size_shl_ext n (int_lst a) m (int_prf a)).

Definition shrl m n (a : int n) := mk_int (bits.size_shrl n m (int_lst a) (int_prf a)).
Notation "a '`>>' k" := (shrl k a) : machine_int_scope.

Lemma shrl_comp : forall m k n (a : int n), (a `>> k) `>> m = a `>> (k + m).
Proof. move=> m k n [a Ha] /=. apply mk_int_pi => /=. by rewrite bits.shrl_comp addnC. Qed.

Lemma shrl_0 : forall n (a : int n), (a `>> 0) = a.
Proof. move=> n [a Ha]. apply mk_int_pi. by rewrite bits.shrl_0. Qed.

Lemma shrl_Z2u_0 : forall n k, Z2u n 0 `>> k = Z2u n 0.
Proof. move=> n k. apply mk_int_pi => /=. by rewrite bits.adjust_u_nil bits.shrl_zeros. Qed.

Lemma shrl_Zpower : forall n k l, (k < n)%nat -> (l <= k)%nat -> Z2u n (2 ^^ k) `>> l = Z2u n (2 ^^ (k - l)).
Proof.
move=> n k l Hkn Hlk.
apply mk_int_pi => /=.
rewrite !bitZ.Z2u_2_Zpower /bits.adjust_u /= !size_nseq.
have [X|X] : (k.+1 < n \/ k.+1 < n = false)%nat by destruct (k.+1 < n)%nat; auto.
- rewrite X.
  move/leP : Hkn => Hkn.
  move/leP : X => X.
  have [Y|Y] : ((k - l).+1 < n \/ (k - l).+1 < n = false)%nat by destruct ((k - l).+1 < n)%nat; auto.
  + rewrite Y.
    move/ltP : Y => Y.
    rewrite /bits.zext (_ : bits.zeros k = bits.zeros (k - l) ++ bits.zeros l); last first.
      rewrite bits.zeros_app.
      f_equal.
      by rewrite -minusE -plusE; move/leP in Hlk; lia.
    rewrite -cat1s 2!catA (bits.shrl_app_zeros l (n - l)); last first.
      rewrite !size_cat /= !size_nseq.
      rewrite addnBA // addn1 -subSn //; last first.
        by move/leP : Hkn.
      rewrite addnC subSS subnKC //.
      by move/leP in Hkn; rewrite ltnW.
    rewrite !catA bits.zeros_app.
    rewrite -catA.
    f_equal.
    f_equal.
    rewrite addnC -subSn // subnBA; last first.
      by move/leP in Hkn; rewrite ltnW.
    rewrite addnC addnBA //.
    by rewrite addnC.
    by move/leP in Hkn.
  + rewrite Y.
    move/ltP : Y.
    move/not_gt => Y.
    rewrite /bits.zext (_ : bits.zeros k = bits.zeros (k - l) ++ bits.zeros l); last first.
      rewrite bits.zeros_app.
      f_equal.
      by rewrite -minusE -plusE; move/leP in Hlk; lia.
    rewrite -cat1s 2!catA (bits.shrl_app_zeros l (n - l)); last first.
      rewrite !size_cat /= !size_nseq.
      rewrite addnBA // addn1 -subSn //; last first.
        by move/leP : Hkn.
      rewrite addnC subSS subnKC //.
      by move/leP in Hkn; rewrite ltnW.
    have Z : ((k - l).+1 - n)%nat = O by rewrite -!minusE; lia.
    rewrite Z /= !catA bits.zeros_app.
    suff : (l + (n - k.+1))%nat = O by move => ->.
    rewrite -!minusE -plusE.
    by rewrite -!minusE in Z Y; lia.
- rewrite X.
  move/leP in X.
  apply not_lt in X.
  have Y : k = (n - 1)%coq_nat by move/ltP in Hkn; lia.
  rewrite minusE in Y.
  rewrite Y /= (_ : (n-1).+1 - n = O)%nat; last first.
    by rewrite -!minusE in Y *; move/ltP in Hkn; lia.
  rewrite /=.
  destruct n => //.
  inversion Hkn.
  rewrite subSS subn0 in Y; subst k.
  clear Hkn X.
  destruct l.
    by rewrite subn0 subSS subn0 ltnn subnn.
  have -> : ((n.+1 - 1 - l.+1).+1 < n.+1)%nat = true.
    rewrite subSS subn0 subnS ltnS prednK //; last by ssromega.
    by rewrite leq_subr.
  rewrite /bits.zext.
  rewrite (_ : n.+1 - 1 = n)%nat; last by rewrite subn1.
  have -> : bits.zeros n = bits.zeros (n - l.+1) ++ bits.zeros l.+1.
    by rewrite bits.zeros_app subnK.
  rewrite -cat1s catA (bits.shrl_app_zeros _ (n - l)); last by rewrite /= size_nseq -subSn.
  do 2 f_equal.
  rewrite -subSn // subnBA //; last by ssromega.
  by rewrite addnC addnK.
Qed.

Lemma shrl_overflow : forall n (a : int n) k, u2Z a < 2 ^^ k -> a `>> k = Z2u n 0.
Proof.
move=> n [a Ha] k H.
case: (le_lt_dec n k) => [|/ltP]X.
- apply mk_int_pi => /=.
  rewrite (bits.shrl_overflow n) //; last by apply/leP.
  by rewrite bits.adjust_u_nil.
- rewrite /le_n /= in H.
  apply mk_int_pi.
  rewrite bits.adjust_u_nil [int_lst _]/=.
  apply bitZ.ult_shrl_overflow => //.
  rewrite (_ : 2 ^^ k = bitZ.u2Z (bits.zeros (n - k.+1) ++ true :: bits.zeros k) ) in H; last first.
    by rewrite bitZ.u2Z_app bits.zeros_app bitZ.u2Z_zeros /= bitZ.u2Z_zeros size_nseq addZ0.
  apply (bitZ.ult_correct' n) in H => //.
  rewrite (bits.adjust_u_S'' n k.+1 (bitZ.Z2u (2 ^^ k))) //.
  by rewrite bitZ.Z2u_2_Zpower.
  by rewrite bitZ.Z2u_2_Zpower /= size_nseq.
  by rewrite size_cat /= !size_nseq addnC subnKC.
Qed.

Lemma shl_shrl : forall n (a : int n) m, u2Z a < 2 ^^ m -> (a `<< (n - m)) `>> (n - m) = a.
Proof. move=> n [l Hn] m /= H. apply mk_int_pi => /=. by apply bitZ.shrl_lst_shl. Qed.

Lemma shrl_shl : forall n (a : int n) m, a `% m = Z2u m 0 -> (a `>> m) `<< m = a.
Proof.
move=> n [a Ha] m //= [H].
apply mk_int_pi => /=.
rewrite bits.adjust_u_nil in H.
case/boolP : (m <= n)%nat => X.
- rewrite (bits.shl_shrl n) //.
  rewrite -H /bits.adjust_u Ha.
  have -> : (n < m = false)%nat by move/leP in X; apply/ltP; lia.
  by rewrite cat_take_drop.
- rewrite (bits.shrl_overflow n) //; last by rewrite -ltnNge in X; rewrite ltnW.
  rewrite bits.shl_zeros.
  rewrite /bits.adjust_u Ha in H.
  move: H.
  rewrite -ltnNge in X.
  rewrite X /bits.zext (bits.zeros_app2 m (m - n)); last by apply/leP; rewrite leq_subr.
  rewrite subnBA; last by rewrite ltnW.
  move/eqP.
  rewrite eqseq_cat; last by rewrite size_nseq.
  case/andP => _ /eqP ->.
  by rewrite addnC addnK.
Qed.

Lemma shrl_rem : forall n (a : int n) k k' (kk' : (n = k + k')%nat),
  zext k ((a `>> k ) `% k') = @eq_rect _ _ _ (a `>> k) _ kk'.
Proof.
move=> n [a Ha] /= k k' kk'.
symmetry.
apply mk_int_pi'.
rewrite /= /bits.zext (bits.shrl_tail n) //; last by rewrite kk'; ssromega.
f_equal.
rewrite /bits.adjust_u size_cat size_nseq.
rewrite size_take kk' addnC addnK Ha kk'.
case: (boolP (k == O)) => k0.
  by rewrite (eqP k0) add0n add0n ltnn ltnn subnn drop0.
have H1 : (k' < k + k')%nat.
  destruct k as [|k] => //.
  by rewrite addSn ltnS leq_addl.
rewrite H1.
by rewrite ltnNge ltnW //= addnK drop_size_cat // size_nseq.
Qed.

Definition shra m n (a : int n) : int n := mk_int (bits.size_shra n m (int_lst a) (int_prf a)).

Definition shr_shrink m n (a : int n) : int (n - m)%nat :=
  mk_int (bits.size_shr_shrink n m (int_lst a) (int_prf a)).

Lemma shr_shrink_overflow : forall n (a : int n) k, (k >= n)%nat ->
  shr_shrink k a = Z2u (n - k)%nat 0.
Proof.
move=> n [a Ha] k Hn.
rewrite /shr_shrink /= /Z2u.
apply: mk_int_pi.
rewrite -subn_eq0 in Hn.
move/eqP in Hn.
rewrite bits.shr_shrink_overflow.
- by rewrite Hn bits.adjust_u_0.
- rewrite Ha -subn_eq0; by apply/eqP.
Qed.

Definition int_and n (a b : int n) : int n :=
  mk_int (bits.size_and n (int_lst a) (int_lst b) (int_prf a) (int_prf b)).
Notation "a '`&' b" := (int_and a b) : machine_int_scope.

Lemma int_and_0 : forall n a, a `& Z2u n 0 = Z2u n 0.
Proof.
move=> n [j H].
rewrite /int_and /=.
apply: mk_int_pi.
by rewrite (bits.adjust_u_nil n) bits.andl0.
Qed.

Lemma int_andC : forall n (a b : int n), a `& b = b `& a.
Proof. move=> n [a Ha] [b Hb] /=. apply: mk_int_pi => /=. by rewrite (bits.andC n). Qed.

Lemma int_and_idempotent : forall n (a : int n), a `& a = a.
Proof. move=> n [a Ha]; apply mk_int_pi => /=. by apply (bits.and_idempotent n). Qed.

Lemma int_even_and_1 : forall n (a : int n), Zeven (u2Z a) -> a `& Z2u n 1 = Z2u n 0.
Proof.
move=> n [a Ha] /= H.
apply: mk_int_pi => /=.
rewrite bits.adjust_u_nil // /bits.adjust_u /=.
have [X|X] : (1 < n)%nat \/ (1 < n)%nat = false by case (1 < n)%nat; auto.
- rewrite X /bits.zext.
  destruct n => //.
  destruct n => //.
  case/lastP : a => // hda tla in Ha H *.
  move: Ha; rewrite size_rcons; case => Ha.
  destruct tla => //.
  + move: (bitZ.Zodd_lst_true hda) => Hnot.
    rewrite -cats1 in H.
    by apply Zeven_not_Zodd in H.
  + rewrite -cats1 (bits.and_app n.+1) /= /bits.bit_and //=.
      by rewrite (_ : false :: bits.zeros n = bits.zeros n.+1) // bits.andl0 // -nseqS.
    by rewrite size_nseq.
- rewrite X.
  destruct n => //.
  destruct a => //.
  destruct n => //.
  destruct a => //.
  destruct a => //.
  by destruct b.
Qed.

Lemma int_odd_and_1 : forall n (a : int n), Zodd (u2Z a) -> a `& Z2u n 1 = Z2u n 1.
Proof.
move=> n [a Ha] /= H.
apply: mk_int_pi => /=.
rewrite /bits.adjust_u /=.
case/boolP : (1 < n)%nat => X.
- rewrite /bits.zext.
  destruct n => //.
  case/lastP : a => // hda tla in Ha H *.
  move: Ha; rewrite size_rcons; case => Ha.
  destruct tla => //.
  + rewrite -cats1 subSS subn0 (bits.and_app n) /= /bits.bit_and //=.
      by rewrite bits.andl0.
    by rewrite size_nseq.
  + move: (bitZ.Zeven_ulst_false hda).
    by rewrite cats1 => /Zeven_not_Zodd.
- destruct n => //.
  destruct a => //.
  destruct n => //.
  destruct a => //.
  destruct a => //.
  by destruct b.
Qed.

Lemma int_and_rem_1 : forall n (a : int n), u2Z (a `& Z2u n 1) = u2Z (a `% 1).
Proof.
move=> [|n] [a Ha] /=.
- rewrite /bits.adjust_u Ha /=.
  by destruct a.
- move: a n Ha.
  elim/last_ind => //.
  move=> hd tl _ n H.
  rewrite size_rcons in H.
  case: H => H.
  rewrite (bits.adjust_u_S'' n.+1 1 (true :: nil)) //= subSS subn0 -cats1 (bits.and_app n) //.
  rewrite bits.andl0 //.
  rewrite bitZ.u2Z_app bits.zeros_app bitZ.u2Z_zeros.
  rewrite (bits.adjust_u_S O hd tl n.+1) //; last by rewrite size_cat addn1 H.
  rewrite bits.adjust_u_0 /=.
  by destruct tl.
  by rewrite size_nseq.
Qed.

Lemma rem_and : forall n (a : int n) k (Hkn : (k <= n)%nat),
  cast_subnK Hkn (zext (n - k)%nat (a `% k)) = (a `& Z2u n (2 ^^ k - 1)).
Proof.
move=> n [a Ha] k Hkn.
rewrite /cast_subnK /cast.
apply: mk_int_pi' => /=.
rewrite bitZ.Z2u_2_Zpower_m1 /bits.adjust_u Ha size_nseq.
have -> : (n < k)%nat = false by apply/negbTE; rewrite -leqNgt.
rewrite leq_eqVlt in Hkn.
case/orP : Hkn => X.
- move/eqP in X; subst k.
  by rewrite ltnn subnn /= /bits.zext /= !drop0 bits.andl1.
- rewrite X /bits.zext -(cat_take_drop (n - k)%nat a) (bits.and_app (n - k)); last 2 first.
    by rewrite size_takel // Ha leq_subr.
    by rewrite size_nseq.
  rewrite bits.andl0; last by rewrite size_takel // -Ha leq_subr.
  rewrite bits.andl1; last first.
    rewrite size_drop Ha subnBA; last by rewrite ltnW.
    by rewrite addnC addnK.
  by rewrite drop_size_cat // size_takel // Ha leq_subr.
Qed.

Definition int_or n (a b : int n) : int n :=
  mk_int (bits.size_or n (int_lst a) (int_lst b) (int_prf a) (int_prf b)).
Notation "a '`|`' b" := (int_or a b) : machine_int_scope.

Lemma int_or_0 n : forall (v : int n), v `|` Z2u n 0 = v.
Proof. case=> v Hv; apply mk_int_pi => /=; by rewrite (bits.adjust_u_nil n) bits.orl0. Qed.

Lemma int_orC : forall n (a b : int n), a `|` b = b `|` a.
Proof. move=> n [a Ha] [b Hb]. apply mk_int_pi. by rewrite (bits.orC n). Qed.

Lemma int_or_idempotent : forall n (a : int n), a `|` a = a.
Proof. move=> n [a Ha]; apply mk_int_pi => /=. by apply (bits.or_idempotent n). Qed.

Lemma bits_int_or : forall n (a b : int n), bits (a `|` b) = bits.or (bits a) (bits b).
Proof.
move=> n [a Ha] [b Hb].
by rewrite /bits /= (bits.orC n) // (bits.rev_or n) // (bits.orC n) // size_rev.
Qed.

Lemma shl_distr_or : forall n (a b : int n) m, (a `|` b) `<< m = (a `<< m) `|` (b `<< m).
Proof.
move=> n [a Ha] [b Hb] m; apply mk_int_pi => /=.
by eapply bits.shr_or; eauto.
Qed.

Lemma shrl_distr_or : forall n (a b : int n) m, (a `|` b) `>> m = (a `>> m) `|` (b `>> m).
Proof.
move=> n [a Ha] [b Hb] m; apply mk_int_pi => /=.
by eapply bits.shrl_or; eauto.
Qed.

Lemma rem_distr_or : forall n (a b : int n) m, (a `|` b) `% m = (a `% m) `|` (b `% m).
Proof.
move=> n [a Ha] [b Hb] m /=; apply mk_int_pi => /=.
by apply (bits.adjust_u_or n).
Qed.

Lemma or_sh_rem : forall n (a : int n) k (H : (k <= n)%nat),
  a = ((a `>> k) `<< k) `|` (cast_subnK H (zext (n - k) (a `% k))).
Proof.
move=> n [a Ha] k Hkn /=.
apply mk_int_pi => /=.
rewrite (bits.shl_shrl n) //.
rewrite mk_int_pi'' /= /zext /bits.zext.
rewrite (bits.or_cat (n - k) k); last 4 first.
  rewrite size_take Ha.
  by case: ifP => // /negbT; rewrite -leqNgt; rewrite -!minusE => /leP; move/leP in Hkn =>?; lia.
  by apply size_nseq.
  by apply size_nseq.
  by apply bits.size_adjust_u.
rewrite bits.orl0; last first.
  rewrite size_take Ha.
  by case: ifP => // /negbT; rewrite -leqNgt; rewrite -!minusE => /leP; move/leP in Hkn =>?; lia.
rewrite (bits.orC k) //; last 2 first.
  by apply size_nseq.
  by apply bits.size_adjust_u.
rewrite bits.orl0; last by apply bits.size_adjust_u.
rewrite /bits.adjust_u Ha.
have -> : (n < k = false)%nat by apply/negbTE; rewrite -leqNgt.
by rewrite cat_take_drop.
Qed.

Definition int_xor n (a b : int n) : int n :=
  mk_int (bits.size_xor n (int_lst a) (int_lst b) (int_prf a) (int_prf b)).
Notation "a '`(+)' b" := (int_xor a b) : machine_int_scope.

Lemma int_xor_0: forall n (v : int n), v `(+) Z2u n 0 = v.
Proof.
move=> n [lst e]; rewrite /int_xor /=.
apply: mk_int_pi.
by rewrite (bits.adjust_u_nil n) bits.xorl0.
Qed.

Lemma int_xorC : forall n (a b : int n), a `(+) b = b `(+) a.
Proof. move=> n [a Ha] [b Hb]. apply: mk_int_pi => /=. by eapply bits.xorC; eauto. Qed.

Lemma int_xorA : forall n (a b c : int n), (a `(+) b) `(+) c = a `(+) (b `(+) c).
Proof. move=> n [a Ha] [b Hb] [c Hc]. apply: mk_int_pi => /=. symmetry. by eapply bits.xorA; eauto. Qed.

Lemma int_xor_self : forall n (a : int n), a `(+) a = `( 0 )_ n.
Proof. move=> n [a Ha]. apply: mk_int_pi => /=. rewrite bits.adjust_u_nil. by apply bits.xor_self. Qed.

Lemma size_cplt1' n a : size a = n -> size (bits.cplt1 a) = n.
Proof. move=> H; by rewrite bits.size_cplt1. Qed.

Definition int_not n (a : int n) : int n := mk_int (@size_cplt1' n (int_lst a) (int_prf a)).

Lemma int_and_1s : forall n a, a `& int_not (Z2u n 0) = a.
Proof.
move=> n [j H].
rewrite /int_and /=.
apply: mk_int_pi.
by rewrite (bits.adjust_u_nil n) bits.cplt1_zeros bits.andl1.
Qed.

Lemma int_not_or n : forall (a b : int n), int_not (a `|` b) = int_not a `& int_not b.
Proof.
move=> [a Ha] [b Hb]; apply mk_int_pi => /=; by apply (bits.cplt1_or n).
Qed.

Lemma int_xor_1s n : forall (a : int n), a `(+) int_not (Z2u n 0) = int_not a.
Proof.
case=> a Ha.
apply mk_int_pi => /=.
rewrite bits.adjust_u_nil bits.cplt1_zeros; by apply bits.xor_ones.
Qed.



Definition cplt2 n (a : int n) : int n.
apply mk_int with (bits.cplt2 (int_lst a)).
rewrite bits.size_cplt2.
by destruct a.
Defined.

Lemma cplt2_zero n : cplt2 (Z2u n 0) = Z2u n 0.
Proof.
rewrite /cplt2.
apply mk_int_pi => /=.
by rewrite bits.adjust_u_nil bits.cplt2_zeros.
Qed.

Lemma cplt2_1s n : cplt2 (int_not (Z2u n 0)) = Z2u n 1.
Proof.
rewrite /cplt2.
apply mk_int_pi => /=.
by rewrite bits.adjust_u_nil bits.cplt1_zeros bits.cplt2_ones.
Qed.

Lemma not_add_1_cplt2: forall n (v : int n), (n > 1)%nat ->
  int_not v `+ Z2u n 1 = cplt2 v.
Proof.
move=> n [lst e] Hn.
rewrite /add /cplt2 /=.
apply mk_int_pi.
rewrite /bits.cplt2 bits.zext_true /bits.adjust_u /=.
destruct n.
- by inversion Hn.
- destruct n.
  + by rewrite ltnn in Hn.
  + by rewrite /= /bits.zext e.
Qed.

Lemma cplt2_inj {n} : forall (a b : int n), cplt2 a = cplt2 b -> a = b.
Proof.
move=> [a Ha] [b Hb].
rewrite /cplt2 /=.
case.
destruct n.
  destruct a => //.
  destruct b => // _.
  by apply mk_int_pi.
move/(@bits.cplt2_inj _ _ _ Ha Hb) => ?; subst a.
by apply mk_int_pi.
Qed.

Lemma sub_cplt2 : forall n (a b : int n.+1), a `- b = a `+ cplt2 b.
Proof.
move=> n [a Ha] [b Hb].
apply mk_int_pi => /=.
rewrite (bits.sub_add_cplt1 n.+1) //.
rewrite /bits.cplt2.
rewrite -(bits.addA n.+1) //; last 2 first.
  by rewrite bits.size_cplt1.
  by rewrite (bits.size_zext 1) // Hb subnK.
rewrite -(bits.carry_add _ _ (bits.zeros n.+1)); last 2 first.
  rewrite (bits.size_add n.+1) //; last by rewrite bits.size_cplt1.
  by rewrite Hb -addn1 subnK.
  by rewrite (bits.size_add n.+1) // bits.size_cplt1.
rewrite (bits.addA n.+1) //; last 2 first.
  by rewrite bits.size_cplt1.
  by rewrite size_nseq.
by rewrite bits.addl0 // bits.size_cplt1 Hb.
Qed.

Definition concat_size n m : int (n + m) -> int (m + n).
Proof. move=> [nm Hnm]; exists nm; by rewrite addnC. Defined.

Definition concat n m (a : int n) (b : int m) : int (n + m) :=
  add (concat_size (shl_ext m a)) (zext n b).
Notation "a `|| b " := (concat a b) (at level 68, left associativity, format "'[' a `|| b ']'") : machine_int_scope.

Program Definition concatE_def := forall n m (a : int n) (b : int m),
  a `|| b = @mk_int _ (int_lst a ++ int_lst b) _.
Next Obligation.
destruct a. destruct b.
by rewrite size_cat /= e e0.
Defined.

Lemma concatE : concatE_def.
Proof.
red.
move=> n m [a Ha] [b Hb] /=.
apply mk_int_pi => /=.
by rewrite /bits.shl_ext /bits.zext bits.addC bits.add_app.
Qed.

Lemma zext_concat : forall n (a : int n) m, zext m a = `( 0 )_ m `|| a.
Proof.
move=> n [a Ha] /= m.
rewrite concatE.
rewrite /zext /= /concat /=.
apply mk_int_pi => /=.
by rewrite /bits.zext bits.adjust_u_nil.
Qed.

Lemma concatA : forall k m n (a : int k) (b : int m) (c : int n),
  a `|| b `|| c = castA (@addnA _ _ _) (a `|| (b `|| c)).
Proof.
move=> k m n a b c.
rewrite !concatE.
apply mk_int_pi => /=.
by rewrite catA.
Qed.

Lemma or_concat n : forall (a : int n) (b : int n) k (Hkn: (k <= n)%nat),
  u2Z a < 2 ^^ k ->
  b `% k = Z2u k 0 ->
  (b `|` a) = cast_subnK Hkn (shr_shrink k b `|| (a `% k)).
Proof.
move=> [a Ha] [b Hb] k Hkn Hu2Za [Hbk].
rewrite bits.adjust_u_nil in Hbk.
symmetry.
apply mk_int_pi' => /=.
rewrite /bits.shl_ext /bits.zext.
rewrite bits.addC bits.add_app; last 2 first.
  by rewrite (bits.size_shr_shrink n).
  by rewrite bits.size_adjust_u.
rewrite -{2}(bits.shr_shrink_adjust_u _ _ _ Hb Hkn) Hbk.
rewrite -{2}(bits.shr_shrink_adjust_u _ _ _ Ha Hkn).
rewrite (bits.or_cat (n - k) k); last 4 first.
  by rewrite (bits.size_shr_shrink n).
  by rewrite size_nseq.
  by rewrite (bits.size_shr_shrink n).
  by rewrite bits.size_adjust_u.
congr cat.
- rewrite /= in Hu2Za.
  apply (bitZ.u2Z_power_inv n) in Hu2Za => //.
  case: Hu2Za => a' Hu2Za.
  rewrite Hu2Za bits.shr_shrink_app //.
  by rewrite bits.orl0 // (bits.size_shr_shrink n).
  rewrite Hu2Za size_cat addnC /= size_nseq -minusE -plusE in Ha.
  move/leP in Hkn.
  by lia.
- rewrite (bits.orC k) //; last 2 first.
    by rewrite size_nseq.
    by rewrite bits.size_adjust_u.
  by rewrite bits.orl0 // bits.size_adjust_u.
Qed.

Lemma rem_concat n : forall (a : int n) m (b : int m), (a `|| b) `% m = b.
Proof.
move=> [l e] m [l0 e0] /=.
apply mk_int_pi.
rewrite /bits.adjust_u (bits.size_add (n + m)); last 2 first.
  by rewrite (bits.size_shl_ext _ _ m e) addnC.
  by rewrite (bits.size_zext _ _ n e0).
have -> : (n + m < m = false)%nat by apply/negbTE; rewrite -leqNgt leq_addl.
by rewrite /bits.zext /bits.shl_ext bits.addC bits.add_app // addnK drop_size_cat.
Qed.

Lemma concat_shl : forall n (a : int n) m,
  a `|| Z2u m 0 = castC (@addnC _ _) (zext m a `<< m).
Proof.
move=> n [a Ha] m.
apply mk_int_pi => /=.
rewrite bits.adjust_u_nil.
rewrite /bits.zext bits.zeros_app bits.addl0.
by rewrite /bits.shl_ext bits.shl_zeros_cat.
by rewrite (@bits.size_shl_ext n) // addnC.
Qed.