Library Integers
Inductive comparison : Type :=
| Ceq : comparison
| Cne : comparison
| Clt : comparison
| Cle : comparison
| Cgt : comparison
| Cge : comparison.
Definition negate_comparison (c: comparison): comparison :=
match c with
| Ceq => Cne
| Cne => Ceq
| Clt => Cge
| Cle => Cgt
| Cgt => Cle
| Cge => Clt
end.
Definition swap_comparison (c: comparison): comparison :=
match c with
| Ceq => Ceq
| Cne => Cne
| Clt => Cgt
| Cle => Cge
| Cgt => Clt
| Cge => Cle
end.
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
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 q => Z.double (P_mod_two_p q m)
| xI q => Z.succ_double (P_mod_two_p q m)
end
end.
Definition Z_mod_modulus (x: Z) : Z :=
match x with
| Z0 => 0
| Zpos p => P_mod_two_p p wordsize
| Zneg p => let r := P_mod_two_p p wordsize in if zeq r 0 then 0 else modulus - r
end.
Lemma P_mod_two_p_range:
forall n p, 0 <= P_mod_two_p p n < two_power_nat n.
Lemma P_mod_two_p_eq:
forall n p, P_mod_two_p p n = (Zpos p) mod (two_power_nat n).
Lemma Z_mod_modulus_range:
forall x, 0 <= Z_mod_modulus x < modulus.
Lemma Z_mod_modulus_range´:
forall x, -1 < Z_mod_modulus x < modulus.
Lemma Z_mod_modulus_eq:
forall 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:
forall x y Px Py, x = y -> mkint x Px = mkint y Py.
Lemma eq_dec: forall (x y: int), {x = y} + {x <> y}.
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.
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
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 x => Zshiftin (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 x => Zshiftin (Z.odd x) (rec (Z.div2 x)))
(fun x => if 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
| O => nil
| 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 :: nil => Some (repr i)
| _ => None
end.
Comparisons.
Definition cmp (c: comparison) (x y: int) : bool :=
match c with
| Ceq => eq x y
| Cne => negb (eq x y)
| Clt => lt x y
| Cle => negb (lt y x)
| Cgt => lt y x
| Cge => negb (lt x y)
end.
Definition cmpu (c: comparison) (x y: int) : bool :=
match c with
| Ceq => eq x y
| Cne => negb (eq x y)
| Clt => ltu x y
| Cle => negb (ltu y x)
| Cgt => ltu y x
| Cge => negb (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.
Remark half_modulus_power:
half_modulus = two_p (zwordsize - 1).
Remark half_modulus_modulus: modulus = 2 * half_modulus.
Relative positions, from greatest to smallest:
max_unsigned
max_signed
2*wordsize-1
wordsize
0
min_signed
Remark half_modulus_pos: half_modulus > 0.
Remark min_signed_neg: min_signed < 0.
Remark max_signed_pos: max_signed >= 0.
Remark wordsize_max_unsigned: zwordsize <= max_unsigned.
Remark two_wordsize_max_unsigned: 2 * zwordsize - 1 <= max_unsigned.
Remark max_signed_unsigned: max_signed < max_unsigned.
Lemma unsigned_repr_eq:
forall x, unsigned (repr x) = Zmod x modulus.
Lemma signed_repr_eq:
forall x, signed (repr x) = if zlt (Zmod x modulus) half_modulus then Zmod x modulus else Zmod x modulus - modulus.
Modulo arithmetic
Section EQ_MODULO.
Variable modul: Z.
Hypothesis modul_pos: modul > 0.
Definition eqmod (x y: Z) : Prop := exists k, x = k * modul + y.
Lemma eqmod_refl: forall x, eqmod x x.
Lemma eqmod_refl2: forall x y, x = y -> eqmod x y.
Lemma eqmod_sym: forall x y, eqmod x y -> eqmod y x.
Lemma eqmod_trans: forall x y z, eqmod x y -> eqmod y z -> eqmod x z.
Lemma eqmod_small_eq:
forall x y, eqmod x y -> 0 <= x < modul -> 0 <= y < modul -> x = y.
Lemma eqmod_mod_eq:
forall x y, eqmod x y -> x mod modul = y mod modul.
Lemma eqmod_mod:
forall x, eqmod x (x mod modul).
Lemma eqmod_add:
forall a b c d, eqmod a b -> eqmod c d -> eqmod (a + c) (b + d).
Lemma eqmod_neg:
forall x y, eqmod x y -> eqmod (-x) (-y).
Lemma eqmod_sub:
forall a b c d, eqmod a b -> eqmod c d -> eqmod (a - c) (b - d).
Lemma eqmod_mult:
forall a b c d, eqmod a c -> eqmod b d -> eqmod (a * b) (c * d).
End EQ_MODULO.
Lemma eqmod_divides:
forall n m x y, eqmod n x y -> Zdivide m n -> eqmod m x y.
We then specialize these definitions to equality modulo
2wordsize.
Hint Resolve modulus_pos: ints.
Definition eqm := eqmod modulus.
Lemma eqm_refl: forall x, eqm x x.
Hint Resolve eqm_refl: ints.
Lemma eqm_refl2:
forall x y, x = y -> eqm x y.
Hint Resolve eqm_refl2: ints.
Lemma eqm_sym: forall x y, eqm x y -> eqm y x.
Hint Resolve eqm_sym: ints.
Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z.
Hint Resolve eqm_trans: ints.
Lemma eqm_small_eq:
forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y.
Hint Resolve eqm_small_eq: ints.
Lemma eqm_add:
forall a b c d, eqm a b -> eqm c d -> eqm (a + c) (b + d).
Hint Resolve eqm_add: ints.
Lemma eqm_neg:
forall x y, eqm x y -> eqm (-x) (-y).
Hint Resolve eqm_neg: ints.
Lemma eqm_sub:
forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d).
Hint Resolve eqm_sub: ints.
Lemma eqm_mult:
forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d).
Hint Resolve eqm_mult: ints.
Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y.
Lemma eqm_unsigned_repr:
forall z, eqm z (unsigned (repr z)).
Hint Resolve eqm_unsigned_repr: ints.
Lemma eqm_unsigned_repr_l:
forall a b, eqm a b -> eqm (unsigned (repr a)) b.
Hint Resolve eqm_unsigned_repr_l: ints.
Lemma eqm_unsigned_repr_r:
forall a b, eqm a b -> eqm a (unsigned (repr b)).
Hint Resolve eqm_unsigned_repr_r: ints.
Lemma eqm_signed_unsigned:
forall x, eqm (signed x) (unsigned x).
Theorem unsigned_range:
forall i, 0 <= unsigned i < modulus.
Hint Resolve unsigned_range: ints.
Theorem unsigned_range_2:
forall i, 0 <= unsigned i <= max_unsigned.
Hint Resolve unsigned_range_2: ints.
Theorem signed_range:
forall i, min_signed <= signed i <= max_signed.
Theorem repr_unsigned:
forall i, repr (unsigned i) = i.
Hint Resolve repr_unsigned: ints.
Lemma repr_signed:
forall i, repr (signed i) = i.
Lemma signed_eq_zero :
forall i,
signed i = 0 ->
i = zero.
Lemma unsigned_eq_zero :
forall i,
unsigned i = 0 ->
i = zero.
Hint Resolve repr_signed: ints.
Opaque repr.
Lemma eqm_repr_eq: forall x y, eqm x (unsigned y) -> repr x = y.
Theorem unsigned_repr:
forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z.
Hint Resolve unsigned_repr: ints.
Theorem signed_repr:
forall z, min_signed <= z <= max_signed -> signed (repr z) = z.
Theorem signed_eq_unsigned:
forall x, unsigned x <= max_signed -> signed x = unsigned x.
Theorem signed_positive:
forall x, signed x >= 0 <-> unsigned x <= max_signed.
Theorem unsigned_zero: unsigned zero = 0.
Theorem unsigned_one: unsigned one = 1.
Theorem unsigned_mone: unsigned mone = modulus - 1.
Theorem signed_zero: signed zero = 0.
Theorem signed_mone: signed mone = -1.
Theorem one_not_zero: one <> zero.
Theorem unsigned_repr_wordsize:
unsigned iwordsize = zwordsize.
Theorem eq_sym:
forall x y, eq x y = eq y x.
Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y.
Theorem eq_true: forall x, eq x x = true.
Theorem eq_false: forall x y, x <> y -> eq x y = false.
Theorem eq_signed:
forall x y, eq x y = if zeq (signed x) (signed y) then true else false.
Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y).
Theorem add_signed: forall x y, add x y = repr (signed x + signed y).
Theorem add_commut: forall x y, add x y = add y x.
Theorem add_zero: forall x, add x zero = x.
Theorem add_zero_l: forall x, add zero x = x.
Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
Theorem add_neg_zero: forall x, add x (neg x) = zero.
Theorem unsigned_add_carry:
forall x y,
unsigned (add x y) = unsigned x + unsigned y - unsigned (add_carry x y zero) * modulus.
Corollary unsigned_add_either:
forall x y,
unsigned (add x y) = unsigned x + unsigned y
\/ unsigned (add x y) = unsigned x + unsigned y - modulus.
Theorem neg_repr: forall z, neg (repr z) = repr (-z).
Theorem neg_zero: neg zero = zero.
Theorem neg_involutive: forall x, neg (neg x) = x.
Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
Theorem sub_zero_l: forall x, sub x zero = x.
Theorem sub_zero_r: forall x, sub zero x = neg x.
Theorem sub_add_opp: forall x y, sub x y = add x (neg y).
Theorem sub_idem: forall x, sub x x = zero.
Theorem sub_add_l: forall x y z, sub (add x y) z = add (sub x z) y.
Theorem sub_add_r: forall x y z, sub x (add y z) = add (sub x z) (neg y).
Theorem sub_shifted:
forall x y z,
sub (add x z) (add y z) = sub x y.
Theorem sub_signed:
forall x y, sub x y = repr (signed x - signed y).
Theorem unsigned_sub_borrow:
forall x y,
unsigned (sub x y) = unsigned x - unsigned y + unsigned (sub_borrow x y zero) * modulus.
Theorem mul_commut: forall x y, mul x y = mul y x.
Theorem mul_zero: forall x, mul x zero = zero.
Theorem mul_one: forall x, mul x one = x.
Theorem mul_mone: forall x, mul x mone = neg x.
Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).
Theorem mul_add_distr_l:
forall x y z, mul (add x y) z = add (mul x z) (mul y z).
Theorem mul_add_distr_r:
forall x y z, mul x (add y z) = add (mul x y) (mul x z).
Theorem neg_mul_distr_l:
forall x y, neg(mul x y) = mul (neg x) y.
Theorem neg_mul_distr_r:
forall x y, neg(mul x y) = mul x (neg y).
Theorem mul_signed:
forall x y, mul x y = repr (signed x * signed y).
Lemma modu_divu_Euclid:
forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y).
Theorem modu_divu:
forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y).
Lemma mods_divs_Euclid:
forall x y, x = add (mul (divs x y) y) (mods x y).
Theorem mods_divs:
forall x y, mods x y = sub x (mul (divs x y) y).
Theorem divu_one:
forall x, divu x one = x.
Theorem modu_one:
forall x, modu x one = zero.
Theorem divs_mone:
forall x, divs x mone = neg x.
Theorem mods_mone:
forall x, mods x mone = zero.
Remark Ztestbit_0: forall n, Z.testbit 0 n = false.
Remark Ztestbit_1: forall n, Z.testbit 1 n = zeq n 0.
Remark Ztestbit_m1: forall n, 0 <= n -> Z.testbit (-1) n = true.
Remark Zshiftin_spec:
forall b x, Zshiftin b x = 2 * x + (if b then 1 else 0).
Remark Zshiftin_inj:
forall b1 x1 b2 x2,
Zshiftin b1 x1 = Zshiftin b2 x2 -> b1 = b2 /\ x1 = x2.
Remark Zdecomp:
forall x, x = Zshiftin (Z.odd x) (Z.div2 x).
Remark Ztestbit_shiftin:
forall 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:
forall b x, Z.testbit (Zshiftin b x) 0 = b.
Remark Ztestbit_shiftin_succ:
forall b x n, 0 <= n -> Z.testbit (Zshiftin b x) (Z.succ n) = Z.testbit x n.
Remark Ztestbit_eq:
forall 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:
forall x, Z.testbit x 0 = Z.odd x.
Remark Ztestbit_succ:
forall n x, 0 <= n -> Z.testbit x (Z.succ n) = Z.testbit (Z.div2 x) n.
Lemma eqmod_same_bits:
forall n x y,
(forall i, 0 <= i < Z.of_nat n -> Z.testbit x i = Z.testbit y i) ->
eqmod (two_power_nat n) x y.
Lemma eqm_same_bits:
forall x y,
(forall i, 0 <= i < zwordsize -> Z.testbit x i = Z.testbit y i) ->
eqm x y.
Lemma same_bits_eqmod:
forall 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:
forall x y i,
eqm x y ->
0 <= i < zwordsize ->
Z.testbit x i = Z.testbit y i.
Remark two_power_nat_infinity:
forall x, 0 <= x -> exists n, x < two_power_nat n.
Lemma equal_same_bits:
forall x y,
(forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) ->
x = y.
Lemma Z_one_complement:
forall i, 0 <= i ->
forall x, Z.testbit (-x-1) i = negb (Z.testbit x i).
Lemma Ztestbit_above:
forall n x i,
0 <= x < two_power_nat n ->
i >= Z.of_nat n ->
Z.testbit x i = false.
Lemma Ztestbit_above_neg:
forall n x i,
-two_power_nat n <= x < 0 ->
i >= Z.of_nat n ->
Z.testbit x i = true.
Lemma Zsign_bit:
forall 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:
forall (P: Z -> Prop),
P 0 ->
(forall b x, 0 <= x -> P x -> P (Zshiftin b x)) ->
forall x, 0 <= x -> P x.
Lemma Zshiftin_pos_ind:
forall (P: Z -> Prop),
P 1 ->
(forall b x, 0 < x -> P x -> P (Zshiftin b x)) ->
forall x, 0 < x -> P x.
Lemma Ztestbit_le:
forall x y,
0 <= y ->
(forall i, 0 <= i -> Z.testbit x i = true -> Z.testbit y i = true) ->
x <= y.
Definition testbit (x: int) (i: Z) : bool := Z.testbit (unsigned x) i.
Lemma testbit_repr:
forall x i,
0 <= i < zwordsize ->
testbit (repr x) i = Z.testbit x i.
Lemma same_bits_eq:
forall x y,
(forall i, 0 <= i < zwordsize -> testbit x i = testbit y i) ->
x = y.
Lemma bits_above:
forall x i, i >= zwordsize -> testbit x i = false.
Lemma bits_zero:
forall i, testbit zero i = false.
Remark bits_one: forall n, testbit one n = zeq n 0.
Lemma bits_mone:
forall i, 0 <= i < zwordsize -> testbit 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:
forall x, testbit x (zwordsize - 1) = if zlt (unsigned x) half_modulus then false else true.
Lemma bits_signed:
forall x i, 0 <= i ->
Z.testbit (signed x) i = testbit x (if zlt i zwordsize then i else zwordsize - 1).
Lemma bits_le:
forall x y,
(forall i, 0 <= i < zwordsize -> testbit x i = true -> testbit y i = true) ->
unsigned x <= unsigned y.
Lemma bits_and:
forall x y i, 0 <= i < zwordsize ->
testbit (and x y) i = testbit x i && testbit y i.
Lemma bits_or:
forall x y i, 0 <= i < zwordsize ->
testbit (or x y) i = testbit x i || testbit y i.
Lemma bits_xor:
forall x y i, 0 <= i < zwordsize ->
testbit (xor x y) i = xorb (testbit x i) (testbit y i).
Lemma bits_not:
forall 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: forall x y, and x y = and y x.
Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
Theorem and_zero: forall x, and x zero = zero.
Corollary and_zero_l: forall x, and zero x = zero.
Theorem and_mone: forall x, and x mone = x.
Corollary and_mone_l: forall x, and mone x = x.
Theorem and_idem: forall x, and x x = x.
Theorem or_commut: forall x y, or x y = or y x.
Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
Theorem or_zero: forall x, or x zero = x.
Corollary or_zero_l: forall x, or zero x = x.
Theorem or_mone: forall x, or x mone = mone.
Theorem or_idem: forall x, or x x = x.
Theorem and_or_distrib:
forall x y z,
and x (or y z) = or (and x y) (and x z).
Corollary and_or_distrib_l:
forall x y z,
and (or x y) z = or (and x z) (and y z).
Theorem or_and_distrib:
forall x y z,
or x (and y z) = and (or x y) (or x z).
Corollary or_and_distrib_l:
forall x y z,
or (and x y) z = and (or x z) (or y z).
Theorem and_or_absorb: forall x y, and x (or x y) = x.
Theorem or_and_absorb: forall x y, or x (and x y) = x.
Theorem xor_commut: forall x y, xor x y = xor y x.
Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
Theorem xor_zero: forall x, xor x zero = x.
Corollary xor_zero_l: forall x, xor zero x = x.
Theorem xor_idem: forall 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: forall x y, xor x y = zero -> x = y.
Theorem and_xor_distrib:
forall x y z,
and x (xor y z) = xor (and x y) (and x z).
Theorem and_le:
forall x y, unsigned (and x y) <= unsigned x.
Theorem or_le:
forall x y, unsigned x <= unsigned (or x y).
Properties of bitwise complement.
Theorem not_involutive:
forall (x: int), not (not x) = x.
Theorem not_zero:
not zero = mone.
Theorem not_mone:
not mone = zero.
Theorem not_or_and_not:
forall x y, not (or x y) = and (not x) (not y).
Theorem not_and_or_not:
forall x y, not (and x y) = or (not x) (not y).
Theorem and_not_self:
forall x, and x (not x) = zero.
Theorem or_not_self:
forall x, or x (not x) = mone.
Theorem xor_not_self:
forall x, xor x (not x) = mone.
Lemma unsigned_not:
forall x, unsigned (not x) = max_unsigned - unsigned x.
Theorem not_neg:
forall x, not x = add (neg x) mone.
Theorem neg_not:
forall x, neg x = add (not x) one.
Theorem sub_add_not:
forall x y, sub x y = add (add x (not y)) one.
Theorem sub_add_not_3:
forall x y b,
b = zero \/ b = one ->
sub (sub x y) b = add (add x (not y)) (xor b one).
Theorem sub_borrow_add_carry:
forall 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.
Lemma Z_add_is_or:
forall i, 0 <= i ->
forall x y,
(forall j, 0 <= j <= i -> Z.testbit x j && Z.testbit y j = false) ->
Z.testbit (x + y) i = Z.testbit x i || Z.testbit y i.
Opaque Z.mul.
Theorem add_is_or:
forall x y,
and x y = zero ->
add x y = or x y.
Theorem xor_is_or:
forall x y, and x y = zero -> xor x y = or x y.
Theorem add_is_xor:
forall x y,
and x y = zero ->
add x y = xor x y.
Theorem add_and:
forall x y z,
and y z = zero ->
add (and x y) (and x z) = and x (or y z).
Lemma bits_shl:
forall 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:
forall 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:
forall 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: forall x, shl x zero = x.
Lemma bitwise_binop_shl:
forall f f´ x y n,
(forall x y i, 0 <= i < zwordsize -> testbit (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:
forall x y n,
and (shl x n) (shl y n) = shl (and x y) n.
Theorem or_shl:
forall x y n,
or (shl x n) (shl y n) = shl (or x y) n.
Theorem xor_shl:
forall x y n,
xor (shl x n) (shl y n) = shl (xor x y) n.
Lemma ltu_inv:
forall x y, ltu x y = true -> 0 <= unsigned x < unsigned y.
Lemma ltu_iwordsize_inv:
forall x, ltu x iwordsize = true -> 0 <= unsigned x < zwordsize.
Theorem shl_shl:
forall 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: forall x, shru x zero = x.
Lemma bitwise_binop_shru:
forall f f´ x y n,
(forall x y i, 0 <= i < zwordsize -> testbit (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:
forall x y n,
and (shru x n) (shru y n) = shru (and x y) n.
Theorem or_shru:
forall x y n,
or (shru x n) (shru y n) = shru (or x y) n.
Theorem xor_shru:
forall x y n,
xor (shru x n) (shru y n) = shru (xor x y) n.
Theorem shru_shru:
forall 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: forall x, shr x zero = x.
Lemma bitwise_binop_shr:
forall f f´ x y n,
(forall x y i, 0 <= i < zwordsize -> testbit (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:
forall x y n,
and (shr x n) (shr y n) = shr (and x y) n.
Theorem or_shr:
forall x y n,
or (shr x n) (shr y n) = shr (or x y) n.
Theorem xor_shr:
forall x y n,
xor (shr x n) (shr y n) = shr (xor x y) n.
Theorem shr_shr:
forall 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:
forall x y z,
and (shr x z) (shru y z) = shru (and x y) z.
Theorem shr_and_shru_and:
forall x y z,
shru (shl z y) y = z ->
and (shr x y) z = and (shru x y) z.
Theorem shru_lt_zero:
forall x,
shru x (repr (zwordsize - 1)) = if lt x zero then one else zero.
Theorem shr_lt_zero:
forall x,
shr x (repr (zwordsize - 1)) = if lt x zero then mone else zero.
Lemma bits_rol:
forall x y i,
0 <= i < zwordsize ->
testbit (rol x y) i = testbit x ((i - unsigned y) mod zwordsize).
Lemma bits_ror:
forall 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:
forall x n,
ltu n iwordsize = true ->
shl x n = rolm x n (shl mone n).
Theorem shru_rolm:
forall x n,
ltu n iwordsize = true ->
shru x n = rolm x (sub iwordsize n) (shru mone n).
Theorem rol_zero:
forall x,
rol x zero = x.
Lemma bitwise_binop_rol:
forall f f´ x y n,
(forall x y i, 0 <= i < zwordsize -> testbit (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:
forall x y n,
rol (and x y) n = and (rol x n) (rol y n).
Theorem rol_or:
forall x y n,
rol (or x y) n = or (rol x n) (rol y n).
Theorem rol_xor:
forall x y n,
rol (xor x y) n = xor (rol x n) (rol y n).
Theorem rol_rol:
forall x n m,
Zdivide zwordsize modulus ->
rol (rol x n) m = rol x (modu (add n m) iwordsize).
Theorem rolm_zero:
forall x m,
rolm x zero m = and x m.
Theorem rolm_rolm:
forall 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:
forall x n m1 m2,
or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2).
Theorem ror_rol:
forall x y,
ltu y iwordsize = true ->
ror x y = rol x (sub iwordsize y).
Theorem ror_rol_neg:
forall x y, (zwordsize | modulus) -> ror x y = rol x (neg y).
Theorem or_ror:
forall x y z,
ltu y iwordsize = true ->
ltu z iwordsize = true ->
add y z = iwordsize ->
ror x z = or (shl x y) (shru x z).
Fixpoint powerserie (l: list Z): Z :=
match l with
| nil => 0
| x :: xs => two_p x + powerserie xs
end.
Lemma Z_one_bits_powerserie:
forall x, 0 <= x < modulus -> x = powerserie (Z_one_bits wordsize x 0).
Lemma Z_one_bits_range:
forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < zwordsize.
Lemma is_power2_rng:
forall n logn,
is_power2 n = Some logn ->
0 <= unsigned logn < zwordsize.
Theorem is_power2_range:
forall n logn,
is_power2 n = Some logn -> ltu logn iwordsize = true.
Lemma is_power2_correct:
forall n logn,
is_power2 n = Some logn ->
unsigned n = two_p (unsigned logn).
Remark two_p_range:
forall n,
0 <= n < zwordsize ->
0 <= two_p n <= max_unsigned.
Remark Z_one_bits_zero:
forall n i, Z_one_bits n 0 i = nil.
Remark Z_one_bits_two_p:
forall 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:
forall n, 0 <= n < zwordsize ->
is_power2 (repr (two_p n)) = Some (repr n).
Relation between bitwise operations and multiplications / divisions by powers of 2
Lemma Zshiftl_mul_two_p:
forall x n, 0 <= n -> Z.shiftl x n = x * two_p n.
Lemma shl_mul_two_p:
forall x y,
shl x y = mul x (repr (two_p (unsigned y))).
Theorem shl_mul:
forall x y,
shl x y = mul x (shl one y).
Theorem mul_pow2:
forall x n logn,
is_power2 n = Some logn ->
mul x n = shl x logn.
Theorem shifted_or_is_add:
forall 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:
forall x n, 0 <= n -> Z.shiftr x n = x / two_p n.
Lemma shru_div_two_p:
forall x y,
shru x y = repr (unsigned x / two_p (unsigned y)).
Theorem divu_pow2:
forall 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:
forall x y,
shr x y = repr (signed x / two_p (unsigned y)).
Theorem divs_pow2:
forall 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:
forall 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:
forall n i, 0 <= n -> 0 <= i ->
Z.testbit (two_p n - 1) i = if zlt i n then true else false.
Theorem modu_and:
forall x n logn,
is_power2 n = Some logn ->
modu x n = and x (sub n one).
Lemma Zquot_Zdiv:
forall x y,
y > 0 ->
Z.quot x y = if zlt x 0 then (x + y - 1) / y else x / y.
Theorem shrx_shr:
forall 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:
forall 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:
forall x y, y > 0 ->
(x + (y - 1)) / y = x / y + if zeq (Zmod x y) 0 then 0 else 1.
Theorem shrx_carry:
forall 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:
forall x y,
signed x >= 0 ->
shr x y = shru x y.
Lemma and_positive:
forall x y, signed y >= 0 -> signed (and x y) >= 0.
Theorem shr_and_is_shru_and:
forall x y z,
lt y zero = false -> shr (and x y) z = shru (and x y) z.
Lemma Ziter_base:
forall (A: Type) n (f: A -> A) x, n <= 0 -> Z.iter n f x = x.
Lemma Ziter_succ:
forall (A: Type) n (f: A -> A) x,
0 <= n -> Z.iter (Z.succ n) f x = f (Z.iter n f x).
Lemma Znatlike_ind:
forall (P: Z -> Prop),
(forall n, n <= 0 -> P n) ->
(forall n, 0 <= n -> P n -> P (Z.succ n)) ->
forall n, P n.
Lemma Zzero_ext_spec:
forall 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:
forall 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:
forall 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:
forall 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:
forall n x, n >= zwordsize -> zero_ext n x = x.
Theorem sign_ext_above:
forall n x, n >= zwordsize -> sign_ext n x = x.
Theorem zero_ext_and:
forall n x, 0 <= n -> zero_ext n x = and x (repr (two_p n - 1)).
Theorem zero_ext_mod:
forall n x, 0 <= n < zwordsize ->
unsigned (zero_ext n x) = Zmod (unsigned x) (two_p n).
Theorem zero_ext_widen:
forall x n n´, 0 <= n <= n´ ->
zero_ext n´ (zero_ext n x) = zero_ext n x.
Theorem sign_ext_widen:
forall x n n´, 0 < n <= n´ ->
sign_ext n´ (sign_ext n x) = sign_ext n x.
Theorem sign_zero_ext_widen:
forall x n n´, 0 <= n < n´ ->
sign_ext n´ (zero_ext n x) = zero_ext n x.
Theorem zero_ext_narrow:
forall x n n´, 0 <= n <= n´ ->
zero_ext n (zero_ext n´ x) = zero_ext n x.
Theorem sign_ext_narrow:
forall x n n´, 0 < n <= n´ ->
sign_ext n (sign_ext n´ x) = sign_ext n x.
Theorem zero_sign_ext_narrow:
forall x n n´, 0 < n <= n´ ->
zero_ext n (sign_ext n´ x) = zero_ext n x.
Theorem zero_ext_idem:
forall n x, 0 <= n -> zero_ext n (zero_ext n x) = zero_ext n x.
Theorem sign_ext_idem:
forall n x, 0 < n -> sign_ext n (sign_ext n x) = sign_ext n x.
Theorem sign_ext_zero_ext:
forall n x, 0 < n -> sign_ext n (zero_ext n x) = sign_ext n x.
Theorem zero_ext_sign_ext:
forall n x, 0 < n -> zero_ext n (sign_ext n x) = zero_ext n x.
Theorem sign_ext_equal_if_zero_equal:
forall 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:
forall 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:
forall 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:
forall n x, 0 <= n < zwordsize -> 0 <= unsigned (zero_ext n x) < two_p n.
Lemma eqmod_zero_ext:
forall n x, 0 <= n < zwordsize -> eqmod (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:
forall n x, 0 < n < zwordsize -> -two_p (n-1) <= signed (sign_ext n x) < two_p (n-1).
Lemma eqmod_sign_ext´:
forall n x, 0 < n < zwordsize ->
eqmod (two_p n) (unsigned (sign_ext n x)) (unsigned x).
Lemma eqmod_sign_ext:
forall n x, 0 < n < zwordsize ->
eqmod (two_p n) (signed (sign_ext n x)) (unsigned x).
Theorem one_bits_range:
forall x i, In i (one_bits x) -> ltu i iwordsize = true.
Fixpoint int_of_one_bits (l: list int) : int :=
match l with
| nil => zero
| a :: b => add (shl one a) (int_of_one_bits b)
end.
Theorem one_bits_decomp:
forall x, x = int_of_one_bits (one_bits x).
Theorem negate_cmp:
forall c x y, cmp (negate_comparison c) x y = negb (cmp c x y).
Theorem negate_cmpu:
forall c x y, cmpu (negate_comparison c) x y = negb (cmpu c x y).
Theorem swap_cmp:
forall c x y, cmp (swap_comparison c) x y = cmp c y x.
Theorem swap_cmpu:
forall c x y, cmpu (swap_comparison c) x y = cmpu c y x.
Lemma translate_eq:
forall x y d,
eq (add x d) (add y d) = eq x y.
Lemma translate_ltu:
forall x y d,
0 <= unsigned x + unsigned d <= max_unsigned ->
0 <= unsigned y + unsigned d <= max_unsigned ->
ltu (add x d) (add y d) = ltu x y.
Theorem translate_cmpu:
forall 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:
forall x y d,
min_signed <= signed x + signed d <= max_signed ->
min_signed <= signed y + signed d <= max_signed ->
lt (add x d) (add y d) = lt x y.
Theorem translate_cmp:
forall 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:
forall x, is_false x -> is_true (notbool x).
Theorem notbool_istrue_isfalse:
forall x, is_true x -> is_false (notbool x).
Theorem ltu_range_test:
forall x y,
ltu x y = true -> unsigned y <= max_signed ->
0 <= signed x < unsigned y.
Theorem lt_sub_overflow:
forall 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:
forall ofs1 sz1 ofs2 sz2 base,
sz1 > 0 -> sz2 > 0 -> no_overlap ofs1 sz1 ofs2 sz2 = true ->
unsigned (add base ofs1) + sz1 <= unsigned (add base ofs2)
\/ unsigned (add base ofs2) + sz2 <= unsigned (add base ofs1).
Size of integers, in bits.
Definition Zsize (x: Z) : Z :=
match x with
| Zpos p => Zpos (Pos.size p)
| _ => 0
end.
Definition size (x: int) : Z := Zsize (unsigned x).
Remark Zsize_pos: forall x, 0 <= Zsize x.
Remark Zsize_pos´: forall x, 0 < x -> 0 < Zsize x.
Lemma Zsize_shiftin:
forall b x, 0 < x -> Zsize (Zshiftin b x) = Zsucc (Zsize x).
Lemma Ztestbit_size_1:
forall x, 0 < x -> Z.testbit x (Zpred (Zsize x)) = true.
Lemma Ztestbit_size_2:
forall x, 0 <= x -> forall i, i >= Zsize x -> Z.testbit x i = false.
Lemma Zsize_interval_1:
forall x, 0 <= x -> 0 <= x < two_p (Zsize x).
Lemma Zsize_interval_2:
forall x n, 0 <= n -> 0 <= x < two_p n -> n >= Zsize x.
Lemma Zsize_monotone:
forall x y, 0 <= x <= y -> Zsize x <= Zsize y.
Theorem size_zero: size zero = 0.
Theorem bits_size_1:
forall x, x = zero \/ testbit x (Zpred (size x)) = true.
Theorem bits_size_2:
forall x i, size x <= i -> testbit x i = false.
Theorem size_range:
forall x, 0 <= size x <= zwordsize.
Theorem bits_size_3:
forall x n,
0 <= n ->
(forall i, n <= i < zwordsize -> testbit x i = false) ->
size x <= n.
Theorem bits_size_4:
forall x n,
0 <= n ->
testbit x (Zpred n) = true ->
(forall i, n <= i < zwordsize -> testbit x i = false) ->
size x = n.
Theorem size_interval_1:
forall x, 0 <= unsigned x < two_p (size x).
Theorem size_interval_2:
forall x n, 0 <= n -> 0 <= unsigned x < two_p n -> n >= size x.
Theorem size_and:
forall a b, size (and a b) <= Z.min (size a) (size b).
Corollary and_interval:
forall a b, 0 <= unsigned (and a b) < two_p (Z.min (size a) (size b)).
Theorem size_or:
forall a b, size (or a b) = Z.max (size a) (size b).
Corollary or_interval:
forall a b, 0 <= unsigned (or a b) < two_p (Z.max (size a) (size b)).
Theorem size_xor:
forall a b, size (xor a b) <= Z.max (size a) (size b).
Corollary xor_interval:
forall a b, 0 <= unsigned (xor a b) < two_p (Z.max (size a) (size b)).
End Make.
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.
Notation int32 := Int.int.
Remark int_wordsize_divides_modulus:
Zdivide (Z_of_nat Int.wordsize) Int.modulus.
Module Wordsize_16.
Definition wordsize := 16%nat.
Remark wordsize_not_zero: wordsize <> 0%nat.
End Wordsize_16.
Module Int16 := Make(Wordsize_16).
Notation int16 := Int16.int.
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.
Notation int8 := 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´:
forall 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´:
forall 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´:
forall 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:
forall n i, 0 <= i < Int.zwordsize -> Int.testbit (loword n) i = testbit n i.
Lemma bits_hiword:
forall n i, 0 <= i < Int.zwordsize -> Int.testbit (hiword n) i = testbit n (i + Int.zwordsize).
Lemma bits_ofwords:
forall 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:
forall hi lo, loword (ofwords hi lo) = lo.
Lemma hi_ofwords:
forall hi lo, hiword (ofwords hi lo) = hi.
Lemma ofwords_recompose:
forall n, ofwords (hiword n) (loword n) = n.
Lemma ofwords_add:
forall lo hi, ofwords hi lo = repr (Int.unsigned hi * two_p 32 + Int.unsigned lo).
Lemma ofwords_add´:
forall lo hi, unsigned (ofwords hi lo) = Int.unsigned hi * two_p 32 + Int.unsigned lo.
Remark eqm_mul_2p32:
forall x y, Int.eqm x y -> eqm (x * two_p 32) (y * two_p 32).
Lemma ofwords_add´´:
forall 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:
forall f f64 f32 xh xl yh yl,
(forall x y i, 0 <= i < zwordsize -> testbit (f64 x y) i = f (testbit x i) (testbit y i)) ->
(forall x y i, 0 <= i < Int.zwordsize -> Int.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:
forall xh xl yh yl,
and (ofwords xh xl) (ofwords yh yl) = ofwords (Int.and xh yh) (Int.and xl yl).
Lemma decompose_or:
forall xh xl yh yl,
or (ofwords xh xl) (ofwords yh yl) = ofwords (Int.or xh yh) (Int.or xl yl).
Lemma decompose_xor:
forall xh xl yh yl,
xor (ofwords xh xl) (ofwords yh yl) = ofwords (Int.xor xh yh) (Int.xor xl yl).
Lemma decompose_not:
forall xh xl,
not (ofwords xh xl) = ofwords (Int.not xh) (Int.not xl).
Lemma decompose_shl_1:
forall 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:
forall 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:
forall 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:
forall 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:
forall 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:
forall 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)).
Lemma decompose_add:
forall xh xl yh yl,
add (ofwords xh xl) (ofwords yh yl) =
ofwords (Int.add (Int.add xh yh) (Int.add_carry xl yl Int.zero))
(Int.add xl yl).
Lemma decompose_sub:
forall 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´:
forall xh xl yh yl,
sub (ofwords xh xl) (ofwords yh yl) =
ofwords (Int.add (Int.add xh (Int.not yh)) (Int.add_carry xl (Int.not yl) Int.one))
(Int.sub xl yl).
Definition mul´ (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y).
Lemma mul´_mulhu:
forall x y, mul´ x y = ofwords (Int.mulhu x y) (Int.mul x y).
Lemma decompose_mul:
forall 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:
forall 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:
forall 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:
forall 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:
forall 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:
forall 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.