# Library compcert.Integers

Formalizations of machine integers modulo 2N.

Require Import Eqdep_dec.
Require Import Zquot.
Require Import Zwf.
Require Import Coqlib.

# Comparisons

Inductive comparison : Type :=
| Ceq : comparison
| Cne : comparison
| Clt : comparison
| Cle : comparison
| Cgt : comparison
| Cge : comparison.
Definition negate_comparison (c: comparison): comparison :=
match c with
| CeqCne
| CneCeq
| CltCge
| CleCgt
| CgtCle
| CgeClt
end.

Definition swap_comparison (c: comparison): comparison :=
match c with
| CeqCeq
| CneCne
| CltCgt
| CleCge
| CgtClt
| CgeCle
end.

# Parameterization by the word size, in bits.

Module Type WORDSIZE.
Variable wordsize: nat.
Axiom wordsize_not_zero: wordsize 0%nat.
End WORDSIZE.

LocalLocal
Module Make(WS: WORDSIZE).

Definition wordsize: nat := WS.wordsize.
Definition zwordsize: Z := Z_of_nat wordsize.
Definition modulus : Z := two_power_nat wordsize.
Definition half_modulus : Z := modulus / 2.
Definition max_unsigned : Z := modulus - 1.
Definition max_signed : Z := half_modulus - 1.
Definition min_signed : Z := - half_modulus.

Remark wordsize_pos: zwordsize > 0.

Remark modulus_power: modulus = two_p zwordsize.

Remark modulus_pos: modulus > 0.

# Representation of machine integers

A machine integer (type int) is represented as a Coq arbitrary-precision integer (type Z) plus a proof that it is in the range 0 (included) to modulus (excluded).

Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }.

Fast normalization modulo 2^wordsize

Fixpoint P_mod_two_p (p: positive) (n: nat) {struct n} : Z :=
match n with
| O ⇒ 0
| S m
match p with
| xH ⇒ 1
| xO qZ.double (P_mod_two_p q m)
| xI qZ.succ_double (P_mod_two_p q m)
end
end.

Definition Z_mod_modulus (x: Z) : Z :=
match x with
| Z0 ⇒ 0
| Zpos pP_mod_two_p p wordsize
| Zneg plet r := P_mod_two_p p wordsize in if zeq r 0 then 0 else modulus - r
end.

Lemma P_mod_two_p_range:
n p, 0 P_mod_two_p p n < two_power_nat n.

Lemma P_mod_two_p_eq:
n p, P_mod_two_p p n = (Zpos p) mod (two_power_nat n).

Lemma Z_mod_modulus_range:
x, 0 Z_mod_modulus x < modulus.

Lemma Z_mod_modulus_range':
x, -1 < Z_mod_modulus x < modulus.

Lemma Z_mod_modulus_eq:
x, Z_mod_modulus x = x mod modulus.

The unsigned and signed functions return the Coq integer corresponding to the given machine integer, interpreted as unsigned or signed respectively.

Definition unsigned (n: int) : Z := intval n.

Definition signed (n: int) : Z :=
let x := unsigned n in
if zlt x half_modulus then x else x - modulus.

Conversely, repr takes a Coq integer and returns the corresponding machine integer. The argument is treated modulo modulus.

Definition repr (x: Z) : int :=
mkint (Z_mod_modulus x) (Z_mod_modulus_range' x).

Definition zero := repr 0.
Definition one := repr 1.
Definition mone := repr (-1).
Definition iwordsize := repr zwordsize.

Lemma mkint_eq:
x y Px Py, x = ymkint x Px = mkint y Py.

Lemma eq_dec: (x y: int), {x = y} + {x y}.

# Arithmetic and logical operations over machine integers

Definition eq (x y: int) : bool :=
if zeq (unsigned x) (unsigned y) then true else false.
Definition lt (x y: int) : bool :=
if zlt (signed x) (signed y) then true else false.
Definition ltu (x y: int) : bool :=
if zlt (unsigned x) (unsigned y) then true else false.

Definition neg (x: int) : int := repr (- unsigned x).

Definition add (x y: int) : int :=
repr (unsigned x + unsigned y).
Definition sub (x y: int) : int :=
repr (unsigned x - unsigned y).
Definition mul (x y: int) : int :=
repr (unsigned x × unsigned y).

Definition divs (x y: int) : int :=
repr (Z.quot (signed x) (signed y)).
Definition mods (x y: int) : int :=
repr (Z.rem (signed x) (signed y)).

Definition divu (x y: int) : int :=
repr (unsigned x / unsigned y).
Definition modu (x y: int) : int :=
repr ((unsigned x) mod (unsigned y)).

Bitwise boolean operations.

Definition and (x y: int): int := repr (Z.land (unsigned x) (unsigned y)).
Definition or (x y: int): int := repr (Z.lor (unsigned x) (unsigned y)).
Definition xor (x y: int) : int := repr (Z.lxor (unsigned x) (unsigned y)).

Definition not (x: int) : int := xor x mone.

Shifts and rotates.

Definition shl (x y: int): int := repr (Z.shiftl (unsigned x) (unsigned y)).
Definition shru (x y: int): int := repr (Z.shiftr (unsigned x) (unsigned y)).
Definition shr (x y: int): int := repr (Z.shiftr (signed x) (unsigned y)).

Definition rol (x y: int) : int :=
let n := (unsigned y) mod zwordsize in
repr (Z.lor (Z.shiftl (unsigned x) n) (Z.shiftr (unsigned x) (zwordsize - n))).
Definition ror (x y: int) : int :=
let n := (unsigned y) mod zwordsize in
repr (Z.lor (Z.shiftr (unsigned x) n) (Z.shiftl (unsigned x) (zwordsize - n))).

Definition rolm (x a m: int): int := and (rol x a) m.

Viewed as signed divisions by powers of two, shrx rounds towards zero, while shr rounds towards minus infinity.

Definition shrx (x y: int): int :=
divs x (shl one y).

High half of full multiply.

Definition mulhu (x y: int): int := repr ((unsigned x × unsigned y) / modulus).
Definition mulhs (x y: int): int := repr ((signed x × signed y) / modulus).

Condition flags

Definition negative (x: int): int :=
if lt x zero then one else zero.

Definition add_carry (x y cin: int): int :=
if zlt (unsigned x + unsigned y + unsigned cin) modulus then zero else one.

Definition add_overflow (x y cin: int): int :=
let s := signed x + signed y + signed cin in
if zle min_signed s && zle s max_signed then zero else one.

Definition sub_borrow (x y bin: int): int :=
if zlt (unsigned x - unsigned y - unsigned bin) 0 then one else zero.

Definition sub_overflow (x y bin: int): int :=
let s := signed x - signed y - signed bin in
if zle min_signed s && zle s max_signed then zero else one.

shr_carry x y is 1 if x is negative and at least one 1 bit is shifted away.

Definition shr_carry (x y: int) : int :=
if lt x zero && negb (eq (and x (sub (shl one y) one)) zero)
then one else zero.

Zero and sign extensions

Definition Zshiftin (b: bool) (x: Z) : Z :=
if b then Z.succ_double x else Z.double x.

In pseudo-code:
```    Fixpoint Zzero_ext (n: Z) (x: Z) : Z :=
if zle n 0 then
0
else
Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
Fixpoint Zsign_ext (n: Z) (x: Z) : Z :=
if zle n 1 then
if Z.odd x then -1 else 0
else
Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
```
We encode this nat-like recursion using the Z.iter iteration function, in order to make the Zzero_ext and Zsign_ext functions efficiently executable within Coq.

Definition Zzero_ext (n: Z) (x: Z) : Z :=
Z.iter n
(fun rec xZshiftin (Z.odd x) (rec (Z.div2 x)))
(fun x ⇒ 0)
x.

Definition Zsign_ext (n: Z) (x: Z) : Z :=
Z.iter (Z.pred n)
(fun rec xZshiftin (Z.odd x) (rec (Z.div2 x)))
(fun xif Z.odd x then -1 else 0)
x.

Definition zero_ext (n: Z) (x: int) : int := repr (Zzero_ext n (unsigned x)).

Definition sign_ext (n: Z) (x: int) : int := repr (Zsign_ext n (unsigned x)).

Decomposition of a number as a sum of powers of two.

Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z :=
match n with
| Onil
| S m
if Z.odd x
then i :: Z_one_bits m (Z.div2 x) (i+1)
else Z_one_bits m (Z.div2 x) (i+1)
end.

Definition one_bits (x: int) : list int :=
List.map repr (Z_one_bits wordsize (unsigned x) 0).

Recognition of powers of two.

Definition is_power2 (x: int) : option int :=
match Z_one_bits wordsize (unsigned x) 0 with
| i :: nilSome (repr i)
| _None
end.

Comparisons.

Definition cmp (c: comparison) (x y: int) : bool :=
match c with
| Ceqeq x y
| Cnenegb (eq x y)
| Cltlt x y
| Clenegb (lt y x)
| Cgtlt y x
| Cgenegb (lt x y)
end.

Definition cmpu (c: comparison) (x y: int) : bool :=
match c with
| Ceqeq x y
| Cnenegb (eq x y)
| Cltltu x y
| Clenegb (ltu y x)
| Cgtltu y x
| Cgenegb (ltu x y)
end.

Definition is_false (x: int) : Prop := x = zero.
Definition is_true (x: int) : Prop := x zero.
Definition notbool (x: int) : int := if eq x zero then one else zero.

# Properties of integers and integer arithmetic

## Properties of modulus, max_unsigned, etc.

Relative positions, from greatest to smallest:
```      max_unsigned
max_signed
2*wordsize-1
wordsize
0
min_signed
```

## Modulo arithmetic

We define and state properties of equality and arithmetic modulo a positive integer.

Section EQ_MODULO.

Variable modul: Z.
Hypothesis modul_pos: modul > 0.

Definition eqmod (x y: Z) : Prop := k, x = k × modul + y.

Lemma eqmod_refl: x, eqmod x x.

Lemma eqmod_refl2: x y, x = yeqmod x y.

Lemma eqmod_sym: x y, eqmod x yeqmod y x.

Lemma eqmod_trans: x y z, eqmod x yeqmod y zeqmod x z.

Lemma eqmod_small_eq:
x y, eqmod x y → 0 x < modul → 0 y < modulx = y.

Lemma eqmod_mod_eq:
x y, eqmod x yx mod modul = y mod modul.

Lemma eqmod_mod:
x, eqmod x (x mod modul).

a b c d, eqmod a beqmod c deqmod (a + c) (b + d).

Lemma eqmod_neg:
x y, eqmod x yeqmod (-x) (-y).

Lemma eqmod_sub:
a b c d, eqmod a beqmod c deqmod (a - c) (b - d).

Lemma eqmod_mult:
a b c d, eqmod a ceqmod b deqmod (a × b) (c × d).

End EQ_MODULO.

Lemma eqmod_divides:
n m x y, eqmod n x yZdivide m neqmod m x y.

We then specialize these definitions to equality modulo 2wordsize.

Hint Resolve modulus_pos: ints.

Definition eqm := eqmod modulus.

Lemma eqm_refl: x, eqm x x.
Hint Resolve eqm_refl: ints.

Lemma eqm_refl2:
x y, x = yeqm x y.
Hint Resolve eqm_refl2: ints.

Lemma eqm_sym: x y, eqm x yeqm y x.
Hint Resolve eqm_sym: ints.

Lemma eqm_trans: x y z, eqm x yeqm y zeqm x z.
Hint Resolve eqm_trans: ints.

Lemma eqm_small_eq:
x y, eqm x y → 0 x < modulus → 0 y < modulusx = y.
Hint Resolve eqm_small_eq: ints.

a b c d, eqm a beqm c deqm (a + c) (b + d).

Lemma eqm_neg:
x y, eqm x yeqm (-x) (-y).
Hint Resolve eqm_neg: ints.

Lemma eqm_sub:
a b c d, eqm a beqm c deqm (a - c) (b - d).
Hint Resolve eqm_sub: ints.

Lemma eqm_mult:
a b c d, eqm a ceqm b deqm (a × b) (c × d).
Hint Resolve eqm_mult: ints.

## Properties of the coercions between Z and int

Lemma eqm_samerepr: x y, eqm x yrepr x = repr y.

Lemma eqm_unsigned_repr:
z, eqm z (unsigned (repr z)).
Hint Resolve eqm_unsigned_repr: ints.

Lemma eqm_unsigned_repr_l:
a b, eqm a beqm (unsigned (repr a)) b.
Hint Resolve eqm_unsigned_repr_l: ints.

Lemma eqm_unsigned_repr_r:
a b, eqm a beqm a (unsigned (repr b)).
Hint Resolve eqm_unsigned_repr_r: ints.

Lemma eqm_signed_unsigned:
x, eqm (signed x) (unsigned x).

Theorem unsigned_range:
i, 0 unsigned i < modulus.
Hint Resolve unsigned_range: ints.

Theorem unsigned_range_2:
i, 0 unsigned i max_unsigned.
Hint Resolve unsigned_range_2: ints.

Theorem signed_range:
i, min_signed signed i max_signed.

Theorem repr_unsigned:
i, repr (unsigned i) = i.
Hint Resolve repr_unsigned: ints.

Lemma repr_signed:
i, repr (signed i) = i.
Hint Resolve repr_signed: ints.

Opaque repr.

Lemma eqm_repr_eq: x y, eqm x (unsigned y) → repr x = y.

Theorem unsigned_repr:
z, 0 z max_unsignedunsigned (repr z) = z.
Hint Resolve unsigned_repr: ints.

Theorem signed_repr:
z, min_signed z max_signedsigned (repr z) = z.

Theorem signed_eq_unsigned:
x, unsigned x max_signedsigned x = unsigned x.

Theorem signed_positive:
x, signed x 0 unsigned x max_signed.

## Properties of equality

Theorem eq_sym:
x y, eq x y = eq y x.

Theorem eq_spec: (x y: int), if eq x y then x = y else x y.

Theorem eq_true: x, eq x x = true.

Theorem eq_false: x y, x yeq x y = false.

Theorem eq_signed:
x y, eq x y = if zeq (signed x) (signed y) then true else false.

Theorem add_unsigned: x y, add x y = repr (unsigned x + unsigned y).

Theorem add_signed: x y, add x y = repr (signed x + signed y).

x y,
unsigned (add x y) = unsigned x + unsigned y - unsigned (add_carry x y zero) × modulus.

x y,
unsigned (add x y) = unsigned x + unsigned y
unsigned (add x y) = unsigned x + unsigned y - modulus.

## Properties of negation

Theorem neg_repr: z, neg (repr z) = repr (-z).

Theorem neg_zero: neg zero = zero.

Theorem neg_involutive: x, neg (neg x) = x.

## Properties of subtraction

Theorem sub_zero_l: x, sub x zero = x.

Theorem sub_zero_r: x, sub zero x = neg x.

Theorem sub_add_opp: x y, sub x y = add x (neg y).

Theorem sub_idem: x, sub x x = zero.

Theorem sub_add_r: x y z, sub x (add y z) = add (sub x z) (neg y).

Theorem sub_shifted:
x y z,

Theorem sub_signed:
x y, sub x y = repr (signed x - signed y).

Theorem unsigned_sub_borrow:
x y,
unsigned (sub x y) = unsigned x - unsigned y + unsigned (sub_borrow x y zero) × modulus.

## Properties of multiplication

Theorem mul_commut: x y, mul x y = mul y x.

Theorem mul_zero: x, mul x zero = zero.

Theorem mul_one: x, mul x one = x.

Theorem mul_mone: x, mul x mone = neg x.

Theorem mul_assoc: x y z, mul (mul x y) z = mul x (mul y z).

x y z, mul (add x y) z = add (mul x z) (mul y z).

x y z, mul x (add y z) = add (mul x y) (mul x z).

Theorem neg_mul_distr_l:
x y, neg(mul x y) = mul (neg x) y.

Theorem neg_mul_distr_r:
x y, neg(mul x y) = mul x (neg y).

Theorem mul_signed:
x y, mul x y = repr (signed x × signed y).

## Properties of division and modulus

Lemma modu_divu_Euclid:
x y, y zerox = add (mul (divu x y) y) (modu x y).

Theorem modu_divu:
x y, y zeromodu x y = sub x (mul (divu x y) y).

Lemma mods_divs_Euclid:
x y, x = add (mul (divs x y) y) (mods x y).

Theorem mods_divs:
x y, mods x y = sub x (mul (divs x y) y).

Theorem divu_one:
x, divu x one = x.

Theorem modu_one:
x, modu x one = zero.

Theorem divs_mone:
x, divs x mone = neg x.

Theorem mods_mone:
x, mods x mone = zero.

## Properties of bit-level operations over Z

Remark Ztestbit_0: n, Z.testbit 0 n = false.

Remark Ztestbit_m1: n, 0 nZ.testbit (-1) n = true.

Remark Zshiftin_spec:
b x, Zshiftin b x = 2 × x + (if b then 1 else 0).

Remark Zshiftin_inj:
b1 x1 b2 x2,
Zshiftin b1 x1 = Zshiftin b2 x2b1 = b2 x1 = x2.

Remark Zdecomp:
x, x = Zshiftin (Z.odd x) (Z.div2 x).

Remark Ztestbit_shiftin:
b x n,
0 n
Z.testbit (Zshiftin b x) n = if zeq n 0 then b else Z.testbit x (Z.pred n).

Remark Ztestbit_shiftin_base:
b x, Z.testbit (Zshiftin b x) 0 = b.

Remark Ztestbit_shiftin_succ:
b x n, 0 nZ.testbit (Zshiftin b x) (Z.succ n) = Z.testbit x n.

Remark Ztestbit_eq:
n x, 0 n
Z.testbit x n = if zeq n 0 then Z.odd x else Z.testbit (Z.div2 x) (Z.pred n).

Remark Ztestbit_base:
x, Z.testbit x 0 = Z.odd x.

Remark Ztestbit_succ:
n x, 0 nZ.testbit x (Z.succ n) = Z.testbit (Z.div2 x) n.

Lemma eqmod_same_bits:
n x y,
( i, 0 i < Z.of_nat nZ.testbit x i = Z.testbit y i) →
eqmod (two_power_nat n) x y.

Lemma eqm_same_bits:
x y,
( i, 0 i < zwordsizeZ.testbit x i = Z.testbit y i) →
eqm x y.

Lemma same_bits_eqmod:
n x y i,
eqmod (two_power_nat n) x y → 0 i < Z.of_nat n
Z.testbit x i = Z.testbit y i.

Lemma same_bits_eqm:
x y i,
eqm x y
0 i < zwordsize
Z.testbit x i = Z.testbit y i.

Remark two_power_nat_infinity:
x, 0 x n, x < two_power_nat n.

Lemma equal_same_bits:
x y,
( i, 0 iZ.testbit x i = Z.testbit y i) →
x = y.

Lemma Z_one_complement:
i, 0 i
x, Z.testbit (-x-1) i = negb (Z.testbit x i).

Lemma Ztestbit_above:
n x i,
0 x < two_power_nat n
i Z.of_nat n
Z.testbit x i = false.

Lemma Ztestbit_above_neg:
n x i,
-two_power_nat n x < 0 →
i Z.of_nat n
Z.testbit x i = true.

Lemma Zsign_bit:
n x,
0 x < two_power_nat (S n) →
Z.testbit x (Z_of_nat n) = if zlt x (two_power_nat n) then false else true.

Lemma Zshiftin_ind:
(P: ZProp),
P 0 →
( b x, 0 xP xP (Zshiftin b x)) →
x, 0 xP x.

Lemma Zshiftin_pos_ind:
(P: ZProp),
P 1 →
( b x, 0 < xP xP (Zshiftin b x)) →
x, 0 < xP x.

Lemma Ztestbit_le:
x y,
0 y
( i, 0 iZ.testbit x i = trueZ.testbit y i = true) →
x y.

## Bit-level reasoning over type int

Definition testbit (x: int) (i: Z) : bool := Z.testbit (unsigned x) i.

Lemma testbit_repr:
x i,
0 i < zwordsize
testbit (repr x) i = Z.testbit x i.

Lemma same_bits_eq:
x y,
( i, 0 i < zwordsizetestbit x i = testbit y i) →
x = y.

Lemma bits_above:
x i, i zwordsizetestbit x i = false.

Lemma bits_zero:
i, testbit zero i = false.

Lemma bits_mone:
i, 0 i < zwordsizetestbit mone i = true.

Hint Rewrite bits_zero bits_mone : ints.

Ltac bit_solve :=
intros; apply same_bits_eq; intros; autorewrite with ints; auto with bool.

Lemma sign_bit_of_unsigned:
x, testbit x (zwordsize - 1) = if zlt (unsigned x) half_modulus then false else true.

Lemma bits_signed:
x i, 0 i
Z.testbit (signed x) i = testbit x (if zlt i zwordsize then i else zwordsize - 1).

Lemma bits_le:
x y,
( i, 0 i < zwordsizetestbit x i = truetestbit y i = true) →
unsigned x unsigned y.

## Properties of bitwise and, or, xor

Lemma bits_and:
x y i, 0 i < zwordsize
testbit (and x y) i = testbit x i && testbit y i.

Lemma bits_or:
x y i, 0 i < zwordsize
testbit (or x y) i = testbit x i || testbit y i.

Lemma bits_xor:
x y i, 0 i < zwordsize
testbit (xor x y) i = xorb (testbit x i) (testbit y i).

Lemma bits_not:
x i, 0 i < zwordsize
testbit (not x) i = negb (testbit x i).

Hint Rewrite bits_and bits_or bits_xor bits_not: ints.

Theorem and_commut: x y, and x y = and y x.

Theorem and_assoc: x y z, and (and x y) z = and x (and y z).

Theorem and_zero: x, and x zero = zero.

Corollary and_zero_l: x, and zero x = zero.

Theorem and_mone: x, and x mone = x.

Corollary and_mone_l: x, and mone x = x.

Theorem and_idem: x, and x x = x.

Theorem or_commut: x y, or x y = or y x.

Theorem or_assoc: x y z, or (or x y) z = or x (or y z).

Theorem or_zero: x, or x zero = x.

Corollary or_zero_l: x, or zero x = x.

Theorem or_mone: x, or x mone = mone.

Theorem or_idem: x, or x x = x.

Theorem and_or_distrib:
x y z,
and x (or y z) = or (and x y) (and x z).

Corollary and_or_distrib_l:
x y z,
and (or x y) z = or (and x z) (and y z).

Theorem or_and_distrib:
x y z,
or x (and y z) = and (or x y) (or x z).

Corollary or_and_distrib_l:
x y z,
or (and x y) z = and (or x z) (or y z).

Theorem and_or_absorb: x y, and x (or x y) = x.

Theorem or_and_absorb: x y, or x (and x y) = x.

Theorem xor_commut: x y, xor x y = xor y x.

Theorem xor_assoc: x y z, xor (xor x y) z = xor x (xor y z).

Theorem xor_zero: x, xor x zero = x.

Corollary xor_zero_l: x, xor zero x = x.

Theorem xor_idem: x, xor x x = zero.

Theorem xor_zero_one: xor zero one = one.

Theorem xor_one_one: xor one one = zero.

Theorem xor_zero_equal: x y, xor x y = zerox = y.

Theorem and_xor_distrib:
x y z,
and x (xor y z) = xor (and x y) (and x z).

Theorem and_le:
x y, unsigned (and x y) unsigned x.

Theorem or_le:
x y, unsigned x unsigned (or x y).

Properties of bitwise complement.

Theorem not_involutive:
(x: int), not (not x) = x.

Theorem not_zero:
not zero = mone.

Theorem not_mone:
not mone = zero.

Theorem not_or_and_not:
x y, not (or x y) = and (not x) (not y).

Theorem not_and_or_not:
x y, not (and x y) = or (not x) (not y).

Theorem and_not_self:
x, and x (not x) = zero.

Theorem or_not_self:
x, or x (not x) = mone.

Theorem xor_not_self:
x, xor x (not x) = mone.

Lemma unsigned_not:
x, unsigned (not x) = max_unsigned - unsigned x.

Theorem not_neg:
x, not x = add (neg x) mone.

Theorem neg_not:
x, neg x = add (not x) one.

x y, sub x y = add (add x (not y)) one.

x y b,
b = zero b = one
sub (sub x y) b = add (add x (not y)) (xor b one).

x y b,
b = zero b = one
sub_borrow x y b = xor (add_carry x (not y) (xor b one)) one.

Connections between add and bitwise logical operations.

i, 0 i
x y,
( j, 0 j iZ.testbit x j && Z.testbit y j = false) →
Z.testbit (x + y) i = Z.testbit x i || Z.testbit y i.
Opaque Z.mul.

x y,
and x y = zero
add x y = or x y.

Theorem xor_is_or:
x y, and x y = zeroxor x y = or x y.

x y,
and x y = zero
add x y = xor x y.

x y z,
and y z = zero
add (and x y) (and x z) = and x (or y z).

## Properties of shifts

Lemma bits_shl:
x y i,
0 i < zwordsize
testbit (shl x y) i =
if zlt i (unsigned y) then false else testbit x (i - unsigned y).

Lemma bits_shru:
x y i,
0 i < zwordsize
testbit (shru x y) i =
if zlt (i + unsigned y) zwordsize then testbit x (i + unsigned y) else false.

Lemma bits_shr:
x y i,
0 i < zwordsize
testbit (shr x y) i =
testbit x (if zlt (i + unsigned y) zwordsize then i + unsigned y else zwordsize - 1).

Hint Rewrite bits_shl bits_shru bits_shr: ints.

Theorem shl_zero: x, shl x zero = x.

Lemma bitwise_binop_shl:
f f' x y n,
( x y i, 0 i < zwordsizetestbit (f x y) i = f' (testbit x i) (testbit y i)) →
f' false false = false
f (shl x n) (shl y n) = shl (f x y) n.

Theorem and_shl:
x y n,
and (shl x n) (shl y n) = shl (and x y) n.

Theorem or_shl:
x y n,
or (shl x n) (shl y n) = shl (or x y) n.

Theorem xor_shl:
x y n,
xor (shl x n) (shl y n) = shl (xor x y) n.

Lemma ltu_inv:
x y, ltu x y = true → 0 unsigned x < unsigned y.

Lemma ltu_iwordsize_inv:
x, ltu x iwordsize = true → 0 unsigned x < zwordsize.

Theorem shl_shl:
x y z,
ltu y iwordsize = true
ltu z iwordsize = true
ltu (add y z) iwordsize = true
shl (shl x y) z = shl x (add y z).

Theorem shru_zero: x, shru x zero = x.

Lemma bitwise_binop_shru:
f f' x y n,
( x y i, 0 i < zwordsizetestbit (f x y) i = f' (testbit x i) (testbit y i)) →
f' false false = false
f (shru x n) (shru y n) = shru (f x y) n.

Theorem and_shru:
x y n,
and (shru x n) (shru y n) = shru (and x y) n.

Theorem or_shru:
x y n,
or (shru x n) (shru y n) = shru (or x y) n.

Theorem xor_shru:
x y n,
xor (shru x n) (shru y n) = shru (xor x y) n.

Theorem shru_shru:
x y z,
ltu y iwordsize = true
ltu z iwordsize = true
ltu (add y z) iwordsize = true
shru (shru x y) z = shru x (add y z).

Theorem shr_zero: x, shr x zero = x.

Lemma bitwise_binop_shr:
f f' x y n,
( x y i, 0 i < zwordsizetestbit (f x y) i = f' (testbit x i) (testbit y i)) →
f (shr x n) (shr y n) = shr (f x y) n.

Theorem and_shr:
x y n,
and (shr x n) (shr y n) = shr (and x y) n.

Theorem or_shr:
x y n,
or (shr x n) (shr y n) = shr (or x y) n.

Theorem xor_shr:
x y n,
xor (shr x n) (shr y n) = shr (xor x y) n.

Theorem shr_shr:
x y z,
ltu y iwordsize = true
ltu z iwordsize = true
ltu (add y z) iwordsize = true
shr (shr x y) z = shr x (add y z).

Theorem and_shr_shru:
x y z,
and (shr x z) (shru y z) = shru (and x y) z.

Theorem shr_and_shru_and:
x y z,
shru (shl z y) y = z
and (shr x y) z = and (shru x y) z.

Theorem shru_lt_zero:
x,
shru x (repr (zwordsize - 1)) = if lt x zero then one else zero.

Theorem shr_lt_zero:
x,
shr x (repr (zwordsize - 1)) = if lt x zero then mone else zero.

## Properties of rotations

Lemma bits_rol:
x y i,
0 i < zwordsize
testbit (rol x y) i = testbit x ((i - unsigned y) mod zwordsize).

Lemma bits_ror:
x y i,
0 i < zwordsize
testbit (ror x y) i = testbit x ((i + unsigned y) mod zwordsize).

Hint Rewrite bits_rol bits_ror: ints.

Theorem shl_rolm:
x n,
ltu n iwordsize = true
shl x n = rolm x n (shl mone n).

Theorem shru_rolm:
x n,
ltu n iwordsize = true
shru x n = rolm x (sub iwordsize n) (shru mone n).

Theorem rol_zero:
x,
rol x zero = x.

Lemma bitwise_binop_rol:
f f' x y n,
( x y i, 0 i < zwordsizetestbit (f x y) i = f' (testbit x i) (testbit y i)) →
rol (f x y) n = f (rol x n) (rol y n).

Theorem rol_and:
x y n,
rol (and x y) n = and (rol x n) (rol y n).

Theorem rol_or:
x y n,
rol (or x y) n = or (rol x n) (rol y n).

Theorem rol_xor:
x y n,
rol (xor x y) n = xor (rol x n) (rol y n).

Theorem rol_rol:
x n m,
Zdivide zwordsize modulus
rol (rol x n) m = rol x (modu (add n m) iwordsize).

Theorem rolm_zero:
x m,
rolm x zero m = and x m.

Theorem rolm_rolm:
x n1 m1 n2 m2,
Zdivide zwordsize modulus
rolm (rolm x n1 m1) n2 m2 =
rolm x (modu (add n1 n2) iwordsize)
(and (rol m1 n2) m2).

Theorem or_rolm:
x n m1 m2,
or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2).

Theorem ror_rol:
x y,
ltu y iwordsize = true
ror x y = rol x (sub iwordsize y).

Theorem or_ror:
x y z,
ltu y iwordsize = true
ltu z iwordsize = true
ror x z = or (shl x y) (shru x z).

## Properties of Z_one_bits and is_power2.

Fixpoint powerserie (l: list Z): Z :=
match l with
| nil ⇒ 0
| x :: xstwo_p x + powerserie xs
end.

Lemma Z_one_bits_powerserie:
x, 0 x < modulusx = powerserie (Z_one_bits wordsize x 0).

Lemma Z_one_bits_range:
x i, In i (Z_one_bits wordsize x 0) → 0 i < zwordsize.

Lemma is_power2_rng:
n logn,
is_power2 n = Some logn
0 unsigned logn < zwordsize.

Theorem is_power2_range:
n logn,
is_power2 n = Some lognltu logn iwordsize = true.

Lemma is_power2_correct:
n logn,
is_power2 n = Some logn
unsigned n = two_p (unsigned logn).

Remark two_p_range:
n,
0 n < zwordsize
0 two_p n max_unsigned.

Remark Z_one_bits_zero:
n i, Z_one_bits n 0 i = nil.

Remark Z_one_bits_two_p:
n x i,
0 x < Z_of_nat n
Z_one_bits n (two_p x) i = (i + x) :: nil.

Lemma is_power2_two_p:
n, 0 n < zwordsize
is_power2 (repr (two_p n)) = Some (repr n).

## Relation between bitwise operations and multiplications / divisions by powers of 2

Left shifts and multiplications by powers of 2.

Lemma Zshiftl_mul_two_p:
x n, 0 nZ.shiftl x n = x × two_p n.

Lemma shl_mul_two_p:
x y,
shl x y = mul x (repr (two_p (unsigned y))).

Theorem shl_mul:
x y,
shl x y = mul x (shl one y).

Theorem mul_pow2:
x n logn,
is_power2 n = Some logn
mul x n = shl x logn.

x y n,
0 n < zwordsize
unsigned y < two_p n
or (shl x (repr n)) y = repr(unsigned x × two_p n + unsigned y).

Unsigned right shifts and unsigned divisions by powers of 2.

Lemma Zshiftr_div_two_p:
x n, 0 nZ.shiftr x n = x / two_p n.

Lemma shru_div_two_p:
x y,
shru x y = repr (unsigned x / two_p (unsigned y)).

Theorem divu_pow2:
x n logn,
is_power2 n = Some logn
divu x n = shru x logn.

Signed right shifts and signed divisions by powers of 2.

Lemma shr_div_two_p:
x y,
shr x y = repr (signed x / two_p (unsigned y)).

Theorem divs_pow2:
x n logn,
is_power2 n = Some logn
divs x n = shrx x logn.

Unsigned modulus over 2^n is masking with 2^n-1.

Lemma Ztestbit_mod_two_p:
n x i,
0 n → 0 i
Z.testbit (x mod (two_p n)) i = if zlt i n then Z.testbit x i else false.

Corollary Ztestbit_two_p_m1:
n i, 0 n → 0 i
Z.testbit (two_p n - 1) i = if zlt i n then true else false.

Theorem modu_and:
x n logn,
is_power2 n = Some logn
modu x n = and x (sub n one).

## Properties of shrx (signed division by a power of 2)

Lemma Zquot_Zdiv:
x y,
y > 0 →
Z.quot x y = if zlt x 0 then (x + y - 1) / y else x / y.

Theorem shrx_shr:
x y,
ltu y (repr (zwordsize - 1)) = true
shrx x y = shr (if lt x zero then add x (sub (shl one y) one) else x) y.

Theorem shrx_shr_2:
x y,
ltu y (repr (zwordsize - 1)) = true
shrx x y = shr (add x (shru (shr x (repr (zwordsize - 1))) (sub iwordsize y))) y.

Lemma Zdiv_shift:
x y, y > 0 →
(x + (y - 1)) / y = x / y + if zeq (Zmod x y) 0 then 0 else 1.

Theorem shrx_carry:
x y,
ltu y (repr (zwordsize - 1)) = true
shrx x y = add (shr x y) (shr_carry x y).

Connections between shr and shru.

Lemma shr_shru_positive:
x y,
signed x 0 →
shr x y = shru x y.

Lemma and_positive:
x y, signed y 0 → signed (and x y) 0.

Theorem shr_and_is_shru_and:
x y z,
lt y zero = falseshr (and x y) z = shru (and x y) z.

## Properties of integer zero extension and sign extension.

Lemma Ziter_base:
(A: Type) n (f: AA) x, n 0 → Z.iter n f x = x.

Lemma Ziter_succ:
(A: Type) n (f: AA) x,
0 nZ.iter (Z.succ n) f x = f (Z.iter n f x).

Lemma Znatlike_ind:
(P: ZProp),
( n, n 0 → P n) →
( n, 0 nP nP (Z.succ n)) →
n, P n.

Lemma Zzero_ext_spec:
n x i, 0 i
Z.testbit (Zzero_ext n x) i = if zlt i n then Z.testbit x i else false.

Lemma bits_zero_ext:
n x i, 0 i
testbit (zero_ext n x) i = if zlt i n then testbit x i else false.

Lemma Zsign_ext_spec:
n x i, 0 i → 0 < n
Z.testbit (Zsign_ext n x) i = Z.testbit x (if zlt i n then i else n - 1).

Lemma bits_sign_ext:
n x i, 0 i < zwordsize → 0 < n
testbit (sign_ext n x) i = testbit x (if zlt i n then i else n - 1).

Hint Rewrite bits_zero_ext bits_sign_ext: ints.

Theorem zero_ext_above:
n x, n zwordsizezero_ext n x = x.

Theorem sign_ext_above:
n x, n zwordsizesign_ext n x = x.

Theorem zero_ext_and:
n x, 0 nzero_ext n x = and x (repr (two_p n - 1)).

Theorem zero_ext_mod:
n x, 0 n < zwordsize
unsigned (zero_ext n x) = Zmod (unsigned x) (two_p n).

Theorem zero_ext_widen:
x n n', 0 n n'
zero_ext n' (zero_ext n x) = zero_ext n x.

Theorem sign_ext_widen:
x n n', 0 < n n'
sign_ext n' (sign_ext n x) = sign_ext n x.

Theorem sign_zero_ext_widen:
x n n', 0 n < n'
sign_ext n' (zero_ext n x) = zero_ext n x.

Theorem zero_ext_narrow:
x n n', 0 n n'
zero_ext n (zero_ext n' x) = zero_ext n x.

Theorem sign_ext_narrow:
x n n', 0 < n n'
sign_ext n (sign_ext n' x) = sign_ext n x.

Theorem zero_sign_ext_narrow:
x n n', 0 < n n'
zero_ext n (sign_ext n' x) = zero_ext n x.

Theorem zero_ext_idem:
n x, 0 nzero_ext n (zero_ext n x) = zero_ext n x.

Theorem sign_ext_idem:
n x, 0 < nsign_ext n (sign_ext n x) = sign_ext n x.

Theorem sign_ext_zero_ext:
n x, 0 < nsign_ext n (zero_ext n x) = sign_ext n x.

Theorem zero_ext_sign_ext:
n x, 0 < nzero_ext n (sign_ext n x) = zero_ext n x.

Theorem sign_ext_equal_if_zero_equal:
n x y, 0 < n
zero_ext n x = zero_ext n y
sign_ext n x = sign_ext n y.

Theorem zero_ext_shru_shl:
n x,
0 < n < zwordsize
let y := repr (zwordsize - n) in
zero_ext n x = shru (shl x y) y.

Theorem sign_ext_shr_shl:
n x,
0 < n < zwordsize
let y := repr (zwordsize - n) in
sign_ext n x = shr (shl x y) y.

zero_ext n x is the unique integer congruent to x modulo 2^n in the range 0...2^n-1.

Lemma zero_ext_range:
n x, 0 n < zwordsize → 0 unsigned (zero_ext n x) < two_p n.

Lemma eqmod_zero_ext:
n x, 0 n < zwordsizeeqmod (two_p n) (unsigned (zero_ext n x)) (unsigned x).

sign_ext n x is the unique integer congruent to x modulo 2^n in the range -2^(n-1)...2^(n-1) - 1.

Lemma sign_ext_range:
n x, 0 < n < zwordsize-two_p (n-1) signed (sign_ext n x) < two_p (n-1).

Lemma eqmod_sign_ext':
n x, 0 < n < zwordsize
eqmod (two_p n) (unsigned (sign_ext n x)) (unsigned x).

Lemma eqmod_sign_ext:
n x, 0 < n < zwordsize
eqmod (two_p n) (signed (sign_ext n x)) (unsigned x).

## Properties of one_bits (decomposition in sum of powers of two)

Theorem one_bits_range:
x i, In i (one_bits x) → ltu i iwordsize = true.

Fixpoint int_of_one_bits (l: list int) : int :=
match l with
| nilzero
| a :: badd (shl one a) (int_of_one_bits b)
end.

Theorem one_bits_decomp:
x, x = int_of_one_bits (one_bits x).

## Properties of comparisons

Theorem negate_cmp:
c x y, cmp (negate_comparison c) x y = negb (cmp c x y).

Theorem negate_cmpu:
c x y, cmpu (negate_comparison c) x y = negb (cmpu c x y).

Theorem swap_cmp:
c x y, cmp (swap_comparison c) x y = cmp c y x.

Theorem swap_cmpu:
c x y, cmpu (swap_comparison c) x y = cmpu c y x.

Lemma translate_eq:
x y d,

Lemma translate_ltu:
x y d,
0 unsigned x + unsigned d max_unsigned
0 unsigned y + unsigned d max_unsigned

Theorem translate_cmpu:
c x y d,
0 unsigned x + unsigned d max_unsigned
0 unsigned y + unsigned d max_unsigned
cmpu c (add x d) (add y d) = cmpu c x y.

Lemma translate_lt:
x y d,
min_signed signed x + signed d max_signed
min_signed signed y + signed d max_signed

Theorem translate_cmp:
c x y d,
min_signed signed x + signed d max_signed
min_signed signed y + signed d max_signed
cmp c (add x d) (add y d) = cmp c x y.

Theorem notbool_isfalse_istrue:
x, is_false xis_true (notbool x).

Theorem notbool_istrue_isfalse:
x, is_true xis_false (notbool x).

Theorem ltu_range_test:
x y,
ltu x y = trueunsigned y max_signed
0 signed x < unsigned y.

Theorem lt_sub_overflow:
x y,
xor (sub_overflow x y zero) (negative (sub x y)) = if lt x y then one else zero.

Non-overlapping test

Definition no_overlap (ofs1: int) (sz1: Z) (ofs2: int) (sz2: Z) : bool :=
let x1 := unsigned ofs1 in let x2 := unsigned ofs2 in
zlt (x1 + sz1) modulus && zlt (x2 + sz2) modulus
&& (zle (x1 + sz1) x2 || zle (x2 + sz2) x1).

Lemma no_overlap_sound:
ofs1 sz1 ofs2 sz2 base,
sz1 > 0 → sz2 > 0 → no_overlap ofs1 sz1 ofs2 sz2 = true

Size of integers, in bits.

Definition Zsize (x: Z) : Z :=
match x with
| Zpos pZpos (Pos.size p)
| _ ⇒ 0
end.

Definition size (x: int) : Z := Zsize (unsigned x).

Remark Zsize_pos: x, 0 Zsize x.

Remark Zsize_pos': x, 0 < x → 0 < Zsize x.

Lemma Zsize_shiftin:
b x, 0 < xZsize (Zshiftin b x) = Zsucc (Zsize x).

Lemma Ztestbit_size_1:
x, 0 < xZ.testbit x (Zpred (Zsize x)) = true.

Lemma Ztestbit_size_2:
x, 0 x i, i Zsize xZ.testbit x i = false.

Lemma Zsize_interval_1:
x, 0 x → 0 x < two_p (Zsize x).

Lemma Zsize_interval_2:
x n, 0 n → 0 x < two_p nn Zsize x.

Lemma Zsize_monotone:
x y, 0 x yZsize x Zsize y.

Theorem size_zero: size zero = 0.

Theorem bits_size_1:
x, x = zero testbit x (Zpred (size x)) = true.

Theorem bits_size_2:
x i, size x itestbit x i = false.

Theorem size_range:
x, 0 size x zwordsize.

Theorem bits_size_3:
x n,
0 n
( i, n i < zwordsizetestbit x i = false) →
size x n.

Theorem bits_size_4:
x n,
0 n
testbit x (Zpred n) = true
( i, n i < zwordsizetestbit x i = false) →
size x = n.

Theorem size_interval_1:
x, 0 unsigned x < two_p (size x).

Theorem size_interval_2:
x n, 0 n → 0 unsigned x < two_p nn size x.

Theorem size_and:
a b, size (and a b) Z.min (size a) (size b).

Corollary and_interval:
a b, 0 unsigned (and a b) < two_p (Z.min (size a) (size b)).

Theorem size_or:
a b, size (or a b) = Z.max (size a) (size b).

Corollary or_interval:
a b, 0 unsigned (or a b) < two_p (Z.max (size a) (size b)).

Theorem size_xor:
a b, size (xor a b) Z.max (size a) (size b).

Corollary xor_interval:
a b, 0 unsigned (xor a b) < two_p (Z.max (size a) (size b)).

End Make.

# Specialization to integers of size 8, 32, and 64 bits

Module Wordsize_32.
Definition wordsize := 32%nat.
Remark wordsize_not_zero: wordsize 0%nat.
End Wordsize_32.

Module Int := Make(Wordsize_32).

Notation int := Int.int.

Remark int_wordsize_divides_modulus:
Zdivide (Z_of_nat Int.wordsize) Int.modulus.

Module Wordsize_8.
Definition wordsize := 8%nat.
Remark wordsize_not_zero: wordsize 0%nat.
End Wordsize_8.

Module Byte := Make(Wordsize_8).

Notation byte := Byte.int.

Module Wordsize_64.
Definition wordsize := 64%nat.
Remark wordsize_not_zero: wordsize 0%nat.
End Wordsize_64.

Module Int64.

Include Make(Wordsize_64).

Shifts with amount given as a 32-bit integer

Definition iwordsize': Int.int := Int.repr zwordsize.

Definition shl' (x: int) (y: Int.int): int :=
repr (Z.shiftl (unsigned x) (Int.unsigned y)).
Definition shru' (x: int) (y: Int.int): int :=
repr (Z.shiftr (unsigned x) (Int.unsigned y)).
Definition shr' (x: int) (y: Int.int): int :=
repr (Z.shiftr (signed x) (Int.unsigned y)).

Lemma bits_shl':
x y i,
0 i < zwordsize
testbit (shl' x y) i =
if zlt i (Int.unsigned y) then false else testbit x (i - Int.unsigned y).

Lemma bits_shru':
x y i,
0 i < zwordsize
testbit (shru' x y) i =
if zlt (i + Int.unsigned y) zwordsize then testbit x (i + Int.unsigned y) else false.

Lemma bits_shr':
x y i,
0 i < zwordsize
testbit (shr' x y) i =
testbit x (if zlt (i + Int.unsigned y) zwordsize then i + Int.unsigned y else zwordsize - 1).

Decomposing 64-bit ints as pairs of 32-bit ints

Definition loword (n: int) : Int.int := Int.repr (unsigned n).

Definition hiword (n: int) : Int.int := Int.repr (unsigned (shru n (repr Int.zwordsize))).

Definition ofwords (hi lo: Int.int) : int :=
or (shl (repr (Int.unsigned hi)) (repr Int.zwordsize)) (repr (Int.unsigned lo)).

Lemma bits_loword:
n i, 0 i < Int.zwordsizeInt.testbit (loword n) i = testbit n i.

Lemma bits_hiword:
n i, 0 i < Int.zwordsizeInt.testbit (hiword n) i = testbit n (i + Int.zwordsize).

Lemma bits_ofwords:
hi lo i, 0 i < zwordsize
testbit (ofwords hi lo) i =
if zlt i Int.zwordsize then Int.testbit lo i else Int.testbit hi (i - Int.zwordsize).

Lemma lo_ofwords:
hi lo, loword (ofwords hi lo) = lo.

Lemma hi_ofwords:
hi lo, hiword (ofwords hi lo) = hi.

Lemma ofwords_recompose:
n, ofwords (hiword n) (loword n) = n.

lo hi, ofwords hi lo = repr (Int.unsigned hi × two_p 32 + Int.unsigned lo).

lo hi, unsigned (ofwords hi lo) = Int.unsigned hi × two_p 32 + Int.unsigned lo.

Remark eqm_mul_2p32:
x y, Int.eqm x yeqm (x × two_p 32) (y × two_p 32).

lo hi, signed (ofwords hi lo) = Int.signed hi × two_p 32 + Int.unsigned lo.

Expressing 64-bit operations in terms of 32-bit operations

Lemma decompose_bitwise_binop:
f f64 f32 xh xl yh yl,
( x y i, 0 i < zwordsizetestbit (f64 x y) i = f (testbit x i) (testbit y i)) →
( x y i, 0 i < Int.zwordsizeInt.testbit (f32 x y) i = f (Int.testbit x i) (Int.testbit y i)) →
f64 (ofwords xh xl) (ofwords yh yl) = ofwords (f32 xh yh) (f32 xl yl).

Lemma decompose_and:
xh xl yh yl,
and (ofwords xh xl) (ofwords yh yl) = ofwords (Int.and xh yh) (Int.and xl yl).

Lemma decompose_or:
xh xl yh yl,
or (ofwords xh xl) (ofwords yh yl) = ofwords (Int.or xh yh) (Int.or xl yl).

Lemma decompose_xor:
xh xl yh yl,
xor (ofwords xh xl) (ofwords yh yl) = ofwords (Int.xor xh yh) (Int.xor xl yl).

Lemma decompose_not:
xh xl,
not (ofwords xh xl) = ofwords (Int.not xh) (Int.not xl).

Lemma decompose_shl_1:
xh xl y,
0 Int.unsigned y < Int.zwordsize
shl' (ofwords xh xl) y =
ofwords (Int.or (Int.shl xh y) (Int.shru xl (Int.sub Int.iwordsize y)))
(Int.shl xl y).

Lemma decompose_shl_2:
xh xl y,
Int.zwordsize Int.unsigned y < zwordsize
shl' (ofwords xh xl) y =
ofwords (Int.shl xl (Int.sub y Int.iwordsize)) Int.zero.

Lemma decompose_shru_1:
xh xl y,
0 Int.unsigned y < Int.zwordsize
shru' (ofwords xh xl) y =
ofwords (Int.shru xh y)
(Int.or (Int.shru xl y) (Int.shl xh (Int.sub Int.iwordsize y))).

Lemma decompose_shru_2:
xh xl y,
Int.zwordsize Int.unsigned y < zwordsize
shru' (ofwords xh xl) y =
ofwords Int.zero (Int.shru xh (Int.sub y Int.iwordsize)).

Lemma decompose_shr_1:
xh xl y,
0 Int.unsigned y < Int.zwordsize
shr' (ofwords xh xl) y =
ofwords (Int.shr xh y)
(Int.or (Int.shru xl y) (Int.shl xh (Int.sub Int.iwordsize y))).

Lemma decompose_shr_2:
xh xl y,
Int.zwordsize Int.unsigned y < zwordsize
shr' (ofwords xh xl) y =
ofwords (Int.shr xh (Int.sub Int.iwordsize Int.one))
(Int.shr xh (Int.sub y Int.iwordsize)).

xh xl yh yl,
add (ofwords xh xl) (ofwords yh yl) =

Lemma decompose_sub:
xh xl yh yl,
sub (ofwords xh xl) (ofwords yh yl) =
ofwords (Int.sub (Int.sub xh yh) (Int.sub_borrow xl yl Int.zero))
(Int.sub xl yl).

Lemma decompose_sub':
xh xl yh yl,
sub (ofwords xh xl) (ofwords yh yl) =
(Int.sub xl yl).

Definition mul' (x y: Int.int) : int := repr (Int.unsigned x × Int.unsigned y).

Lemma mul'_mulhu:
x y, mul' x y = ofwords (Int.mulhu x y) (Int.mul x y).

Lemma decompose_mul:
xh xl yh yl,
mul (ofwords xh xl) (ofwords yh yl) =
ofwords (Int.add (Int.add (hiword (mul' xl yl)) (Int.mul xl yh)) (Int.mul xh yl))
(loword (mul' xl yl)).

Lemma decompose_mul_2:
xh xl yh yl,
mul (ofwords xh xl) (ofwords yh yl) =
ofwords (Int.add (Int.add (Int.mulhu xl yl) (Int.mul xl yh)) (Int.mul xh yl))
(Int.mul xl yl).

Lemma decompose_ltu:
xh xl yh yl,
ltu (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.ltu xh yh.

Lemma decompose_leu:
xh xl yh yl,
negb (ltu (ofwords yh yl) (ofwords xh xl)) =
if Int.eq xh yh then negb (Int.ltu yl xl) else Int.ltu xh yh.

Lemma decompose_lt:
xh xl yh yl,
lt (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.lt xh yh.

Lemma decompose_le:
xh xl yh yl,
negb (lt (ofwords yh yl) (ofwords xh xl)) =
if Int.eq xh yh then negb (Int.ltu yl xl) else Int.lt xh yh.

End Int64.

Notation int64 := Int64.int.

Global Opaque Int.repr Int64.repr Byte.repr.