Library Integers
Formalizations of machine integers modulo 2N.
Require Import Coqlib.
Inductive comparison : Type :=
| Ceq : comparison
same
| Cne : comparison
different
| Clt : comparison
less than
| Cle : comparison
less than or equal
| Cgt : comparison
greater than
| Cge : comparison.
greater than or equal
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.
Module Make(WS: WORDSIZE).
Definition wordsize: nat := WS.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:
Z_of_nat wordsize > 0.
Remark modulus_power:
modulus = two_p (Z_of_nat wordsize).
Remark modulus_pos:
modulus > 0.
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: 0 <= intval < 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 :=
if zlt (unsigned n) half_modulus
then unsigned n
else unsigned n - 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 (Zmod x modulus) (Z_mod_lt x modulus modulus_pos).
Definition zero := repr 0.
Definition one := repr 1.
Definition mone := repr (-1).
Definition iwordsize := repr (Z_of_nat wordsize).
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 zero_ext (n: Z) (x: int) : int :=
repr (Zmod (unsigned x) (two_p n)).
Definition sign_ext (n: Z) (x: int) : int :=
repr (let p := two_p n in
let y := Zmod (unsigned x) p in
if zlt y (two_p (n-1)) then y else y - p).
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 Zdiv_round (x y: Z) : Z :=
if zlt x 0 then
if zlt y 0 then (-x) / (-y) else - ((-x) / y)
else
if zlt y 0 then -(x / (-y)) else x / y.
Definition Zmod_round (x y: Z) : Z :=
x - (Zdiv_round x y) * y.
Definition divs (x y: int) : int :=
repr (Zdiv_round (signed x) (signed y)).
Definition mods (x y: int) : int :=
repr (Zmod_round (signed x) (signed y)).
Definition divu (x y: int) : int :=
repr (unsigned x / unsigned y).
Definition modu (x y: int) : int :=
repr (Zmod (unsigned x) (unsigned y)).
For bitwise operations, we need to convert between Coq integers
Z
and their bit-level representations. Bit-level representations are
represented as characteristic functions, that is, functions f
of type nat -> bool such that f i is the value of the i-th bit
of the number. The values of characteristic functions for i greater
than 32 are ignored.
Definition Z_shift_add (b: bool) (x: Z) :=
if b then 2 * x + 1 else 2 * x.
Definition Z_bin_decomp (x: Z) : bool * Z :=
match x with
| Z0 => (false, 0)
| Zpos p =>
match p with
| xI q => (true, Zpos q)
| xO q => (false, Zpos q)
| xH => (true, 0)
end
| Zneg p =>
match p with
| xI q => (true, Zneg q - 1)
| xO q => (false, Zneg q)
| xH => (true, -1)
end
end.
Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool :=
match n with
| O =>
(fun i: Z => false)
| S m =>
let (b, y) := Z_bin_decomp x in
let f := bits_of_Z m y in
(fun i: Z => if zeq i 0 then b else f (i - 1))
end.
Fixpoint Z_of_bits (n: nat) (f: Z -> bool) {struct n}: Z :=
match n with
| O => 0
| S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1)))
end.
Bitwise logical ``and'', ``or'' and ``xor'' operations.
Definition bitwise_binop (f: bool -> bool -> bool) (x y: int) :=
let fx := bits_of_Z wordsize (unsigned x) in
let fy := bits_of_Z wordsize (unsigned y) in
repr (Z_of_bits wordsize (fun i => f (fx i) (fy i))).
Definition and (x y: int): int := bitwise_binop andb x y.
Definition or (x y: int): int := bitwise_binop orb x y.
Definition xor (x y: int) : int := bitwise_binop xorb x y.
Definition not (x: int) : int := xor x mone.
Shifts and rotates.
Definition shl (x y: int): int :=
let fx := bits_of_Z wordsize (unsigned x) in
let vy := unsigned y in
repr (Z_of_bits wordsize (fun i => fx (i - vy))).
Definition shru (x y: int): int :=
let fx := bits_of_Z wordsize (unsigned x) in
let vy := unsigned y in
repr (Z_of_bits wordsize (fun i => fx (i + vy))).
Arithmetic right shift is defined as signed division by a power of two.
Two such shifts are defined:
shr rounds towards minus infinity
(standard behaviour for arithmetic right shift) and
shrx rounds towards zero.
Definition shr (x y: int): int :=
repr (signed x / two_p (unsigned y)).
Definition shrx (x y: int): int :=
divs x (shl one y).
Definition shr_carry (x y: int) :=
sub (shrx x y) (shr x y).
Definition rol (x y: int) : int :=
let fx := bits_of_Z wordsize (unsigned x) in
let vy := unsigned y in
repr (Z_of_bits wordsize
(fun i => fx (Zmod (i - vy) (Z_of_nat wordsize)))).
Definition ror (x y: int) : int :=
let fx := bits_of_Z wordsize (unsigned x) in
let vy := unsigned y in
repr (Z_of_bits wordsize
(fun i => fx (Zmod (i + vy) (Z_of_nat wordsize)))).
Definition rolm (x a m: int): int := and (rol x a) m.
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 =>
let (b, y) := Z_bin_decomp x in
if b then i :: Z_one_bits m y (i+1) else Z_one_bits m y (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.
Recognition of integers that are acceptable as immediate operands
to the
rlwim PowerPC instruction. These integers are of the form
000011110000 or 111100001111, that is, a run of one bits
surrounded by zero bits, or conversely. We recognize these integers by
running the following automaton on the bits. The accepting states are
2, 3, 4, 5, and 6.
0 1 0
/ \ / \ / \
\ / \ / \ /
-0--> [1] --1--> [2] --0--> [3]
/
[0]
\
-1--> [4] --0--> [5] --1--> [6]
/ \ / \ / \
\ / \ / \ /
1 0 1
Inductive rlw_state: Type :=
| RLW_S0 : rlw_state
| RLW_S1 : rlw_state
| RLW_S2 : rlw_state
| RLW_S3 : rlw_state
| RLW_S4 : rlw_state
| RLW_S5 : rlw_state
| RLW_S6 : rlw_state
| RLW_Sbad : rlw_state.
Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state :=
match s, b with
| RLW_S0, false => RLW_S1
| RLW_S0, true => RLW_S4
| RLW_S1, false => RLW_S1
| RLW_S1, true => RLW_S2
| RLW_S2, false => RLW_S3
| RLW_S2, true => RLW_S2
| RLW_S3, false => RLW_S3
| RLW_S3, true => RLW_Sbad
| RLW_S4, false => RLW_S5
| RLW_S4, true => RLW_S4
| RLW_S5, false => RLW_S5
| RLW_S5, true => RLW_S6
| RLW_S6, false => RLW_Sbad
| RLW_S6, true => RLW_S6
| RLW_Sbad, _ => RLW_Sbad
end.
Definition rlw_accepting (s: rlw_state) : bool :=
match s with
| RLW_S0 => false
| RLW_S1 => false
| RLW_S2 => true
| RLW_S3 => true
| RLW_S4 => true
| RLW_S5 => true
| RLW_S6 => true
| RLW_Sbad => false
end.
Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool :=
match n with
| O =>
rlw_accepting s
| S m =>
let (b, y) := Z_bin_decomp x in
is_rlw_mask_rec m (rlw_transition s b) y
end.
Definition is_rlw_mask (x: int) : bool :=
is_rlw_mask_rec wordsize RLW_S0 (unsigned x).
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 (Z_of_nat wordsize - 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: Z_of_nat wordsize <= max_unsigned.
Remark two_wordsize_max_unsigned: 2 * Z_of_nat wordsize - 1 <= max_unsigned.
Remark max_signed_unsigned: max_signed < max_unsigned.
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 = Z_of_nat wordsize.
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.
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 := 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.
Proof (eqmod_refl modulus).
Hint Resolve eqm_refl: ints.
Lemma eqm_refl2:
forall x y, x = y -> eqm x y.
Proof (eqmod_refl2 modulus).
Hint Resolve eqm_refl2: ints.
Lemma eqm_sym: forall x y, eqm x y -> eqm y x.
Proof (eqmod_sym modulus).
Hint Resolve eqm_sym: ints.
Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z.
Proof (eqmod_trans modulus).
Hint Resolve eqm_trans: ints.
Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y.
Lemma eqm_small_eq:
forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y.
Proof (eqmod_small_eq modulus).
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).
Proof (eqmod_add modulus).
Hint Resolve eqm_add: ints.
Lemma eqm_neg:
forall x y, eqm x y -> eqm (-x) (-y).
Proof (eqmod_neg modulus).
Hint Resolve eqm_neg: ints.
Lemma eqm_sub:
forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d).
Proof (eqmod_sub modulus).
Hint Resolve eqm_sub: ints.
Lemma eqm_mult:
forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d).
Proof (eqmod_mult modulus).
Hint Resolve eqm_mult: ints.
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.
Hint Resolve repr_signed: ints.
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 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_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 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 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_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 Z_shift_add_bin_decomp:
forall x,
Z_shift_add (fst (Z_bin_decomp x)) (snd (Z_bin_decomp x)) = x.
Lemma Z_shift_add_inj:
forall b1 x1 b2 x2,
Z_shift_add b1 x1 = Z_shift_add b2 x2 -> b1 = b2 /\ x1 = x2.
Lemma Z_of_bits_exten:
forall n f1 f2,
(forall z, 0 <= z < Z_of_nat n -> f1 z = f2 z) ->
Z_of_bits n f1 = Z_of_bits n f2.
Opaque Zmult.
Lemma Z_of_bits_of_Z:
forall x, eqm (Z_of_bits wordsize (bits_of_Z wordsize x)) x.
Lemma bits_of_Z_zero:
forall n x, bits_of_Z n 0 x = false.
Remark Z_bin_decomp_2xm1:
forall x, Z_bin_decomp (2 * x - 1) = (true, x - 1).
Lemma bits_of_Z_mone:
forall n x,
0 <= x < Z_of_nat n ->
bits_of_Z n (two_power_nat n - 1) x = true.
Lemma Z_bin_decomp_shift_add:
forall b x, Z_bin_decomp (Z_shift_add b x) = (b, x).
Lemma bits_of_Z_of_bits:
forall n f i,
0 <= i < Z_of_nat n ->
bits_of_Z n (Z_of_bits n f) i = f i.
Lemma Z_of_bits_range:
forall f, 0 <= Z_of_bits wordsize f < modulus.
Hint Resolve Z_of_bits_range: ints.
Lemma Z_of_bits_range_2:
forall f, 0 <= Z_of_bits wordsize f <= max_unsigned.
Hint Resolve Z_of_bits_range_2: ints.
Lemma bits_of_Z_below:
forall n x i, i < 0 -> bits_of_Z n x i = false.
Lemma bits_of_Z_above:
forall n x i, i >= Z_of_nat n -> bits_of_Z n x i = false.
Lemma bits_of_Z_of_bits':
forall n f i,
bits_of_Z n (Z_of_bits n f) i =
if zlt i 0 then false
else if zle (Z_of_nat n) i then false
else f i.
Opaque Zmult.
Lemma Z_of_bits_excl:
forall n f g h,
(forall i, 0 <= i < Z_of_nat n -> f i && g i = false) ->
(forall i, 0 <= i < Z_of_nat n -> f i || g i = h i) ->
Z_of_bits n f + Z_of_bits n g = Z_of_bits n h.
Lemma bitwise_binop_commut:
forall f,
(forall a b, f a b = f b a) ->
forall x y,
bitwise_binop f x y = bitwise_binop f y x.
Lemma bitwise_binop_assoc:
forall f,
(forall a b c, f a (f b c) = f (f a b) c) ->
forall x y z,
bitwise_binop f (bitwise_binop f x y) z =
bitwise_binop f x (bitwise_binop f y z).
Lemma bitwise_binop_idem:
forall f,
(forall a, f a a = a) ->
forall x,
bitwise_binop f x x = x.
Theorem and_commut: forall x y, and x y = and y x.
Proof (bitwise_binop_commut andb andb_comm).
Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
Proof (bitwise_binop_assoc andb andb_assoc).
Theorem and_zero: forall x, and x zero = zero.
Theorem and_mone: forall x, and x mone = x.
Theorem and_idem: forall x, and x x = x.
Theorem or_commut: forall x y, or x y = or y x.
Proof (bitwise_binop_commut orb orb_comm).
Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
Proof (bitwise_binop_assoc orb orb_assoc).
Theorem or_zero: forall x, or x zero = 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).
Theorem xor_commut: forall x y, xor x y = xor y x.
Proof (bitwise_binop_commut xorb xorb_comm).
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.
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 and_xor_distrib:
forall x y z,
and x (xor y z) = xor (and x y) (and x z).
Theorem not_involutive:
forall (x: int), not (not x) = x.
Lemma Z_of_bits_shift:
forall n f,
exists k,
Z_of_bits n (fun i => f (i - 1)) =
k * two_power_nat n + Z_shift_add (f (-1)) (Z_of_bits n f).
Lemma Z_of_bits_shifts:
forall m f,
0 <= m ->
(forall i, i < 0 -> f i = false) ->
eqm (Z_of_bits wordsize (fun i => f (i - m)))
(two_p m * Z_of_bits wordsize f).
Lemma shl_mul_two_p:
forall x y,
shl x y = mul x (repr (two_p (unsigned y))).
Theorem shl_zero: forall x, shl x zero = x.
Theorem shl_mul:
forall x y,
shl x y = mul x (shl one y).
Lemma ltu_inv:
forall x y, ltu x y = true -> 0 <= unsigned x < unsigned y.
Theorem shl_rolm:
forall x n,
ltu n iwordsize = true ->
shl x n = rolm x n (shl mone n).
Lemma bitwise_binop_shl:
forall f x y n,
f false false = false ->
bitwise_binop f (shl x n) (shl y n) = shl (bitwise_binop f x y) n.
Theorem and_shl:
forall x y n,
and (shl x n) (shl y n) = shl (and x y) n.
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_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 shru_rolm:
forall x n,
ltu n iwordsize = true ->
shru x n = rolm x (sub iwordsize n) (shru mone n).
Lemma bitwise_binop_shru:
forall f x y n,
f false false = false ->
bitwise_binop f (shru x n) (shru y n) = shru (bitwise_binop f x y) n.
Lemma and_shru:
forall x y n,
and (shru x n) (shru y n) = shru (and 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 rol_zero:
forall x,
rol x zero = x.
Lemma bitwise_binop_rol:
forall f x y n,
bitwise_binop f (rol x n) (rol y n) = rol (bitwise_binop f x y) n.
Theorem rol_and:
forall x y n,
rol (and x y) n = and (rol x n) (rol y n).
Theorem rol_rol:
forall x n m,
Zdivide (Z_of_nat wordsize) 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 (Z_of_nat wordsize) modulus ->
rolm (rolm x n1 m1) n2 m2 =
rolm x (modu (add n1 n2) iwordsize)
(and (rol m1 n2) m2).
Theorem rol_or:
forall x y n,
rol (or x y) n = or (rol x n) (rol y n).
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 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).
Lemma bits_of_Z_two_p:
forall n x i,
x >= 0 -> 0 <= i < Z_of_nat n ->
bits_of_Z n (two_p x - 1) i = zlt i x.
Remark two_p_m1_range:
forall n,
0 <= n <= Z_of_nat wordsize ->
0 <= two_p n - 1 <= max_unsigned.
Theorem shru_shl_and:
forall x y,
ltu y iwordsize = true ->
shru (shl x y) y = and x (repr (two_p (Z_of_nat wordsize - unsigned y) - 1)).
Fixpoint powerserie (l: list Z): Z :=
match l with
| nil => 0
| x :: xs => two_p x + powerserie xs
end.
Lemma Z_bin_decomp_range:
forall x n,
0 <= x < 2 * n -> 0 <= snd (Z_bin_decomp x) < n.
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 < Z_of_nat wordsize.
Lemma is_power2_rng:
forall n logn,
is_power2 n = Some logn ->
0 <= unsigned logn < Z_of_nat wordsize.
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 < Z_of_nat wordsize ->
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 < Z_of_nat wordsize ->
is_power2 (repr (two_p n)) = Some (repr n).
Theorem mul_pow2:
forall x n logn,
is_power2 n = Some logn ->
mul x n = shl x logn.
Lemma Z_of_bits_shift_rev:
forall n f,
(forall i, i >= Z_of_nat n -> f i = false) ->
Z_of_bits n f = Z_shift_add (f 0) (Z_of_bits n (fun i => f(i + 1))).
Lemma Z_of_bits_shifts_rev:
forall m f,
0 <= m ->
(forall i, i >= Z_of_nat wordsize -> f i = false) ->
exists k,
Z_of_bits wordsize f = k + two_p m * Z_of_bits wordsize (fun i => f(i + m))
/\ 0 <= k < two_p m.
Lemma shru_div_two_p:
forall x y,
shru x y = repr (unsigned x / two_p (unsigned y)).
Theorem shru_zero:
forall x, shru x zero = x.
Theorem shr_zero:
forall x, shr x zero = x.
Theorem divu_pow2:
forall x n logn,
is_power2 n = Some logn ->
divu x n = shru x logn.
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).
Theorem mods_divs:
forall x y, mods x y = sub x (mul (divs x y) y).
Theorem divs_pow2:
forall x n logn,
is_power2 n = Some logn ->
divs x n = shrx x logn.
Theorem shrx_carry:
forall x y,
add (shr x y) (shr_carry x y) = shrx x y.
Lemma Zdiv_round_Zdiv:
forall x y,
y > 0 ->
Zdiv_round x y = if zlt x 0 then (x + y - 1) / y else x / y.
Theorem shrx_shr:
forall x y,
ltu y (repr (Z_of_nat wordsize - 1)) = true ->
shrx x y =
shr (if lt x zero then add x (sub (shl one y) one) else x) y.
Lemma add_and:
forall x y z,
and y z = zero ->
add (and x y) (and x z) = and x (or y z).
Lemma Z_of_bits_zero:
forall n f,
(forall i, i >= 0 -> f i = false) ->
Z_of_bits n f = 0.
Lemma Z_of_bits_trunc_1:
forall n f k,
(forall i, i >= k -> f i = false) ->
k >= 0 ->
0 <= Z_of_bits n f < two_p k.
Lemma Z_of_bits_trunc_2:
forall n f1 f2 k,
(forall i, i < k -> f2 i = f1 i) ->
k >= 0 ->
exists q, Z_of_bits n f1 = q * two_p k + Z_of_bits n f2.
Lemma Z_of_bits_trunc_3:
forall f n k,
k >= 0 ->
Zmod (Z_of_bits n f) (two_p k) = Z_of_bits n (fun i => if zlt i k then f i else false).
Theorem modu_and:
forall x n logn,
is_power2 n = Some logn ->
modu x n = and x (sub n one).
Section EXTENSIONS.
Variable n: Z.
Hypothesis RANGE: 0 < n < Z_of_nat wordsize.
Remark two_p_n_pos:
two_p n > 0.
Remark two_p_n_range:
0 <= two_p n <= max_unsigned.
Remark two_p_n_range':
two_p n <= max_signed + 1.
Remark unsigned_repr_two_p:
unsigned (repr (two_p n)) = two_p n.
Theorem zero_ext_and:
forall x, zero_ext n x = and x (repr (two_p n - 1)).
Theorem zero_ext_idem:
forall x, zero_ext n (zero_ext n x) = zero_ext n x.
Lemma eqm_eqmod_two_p:
forall a b, eqm a b -> eqmod (two_p n) a b.
Lemma sign_ext_charact:
forall x y,
-(two_p (n-1)) <= signed y < two_p (n-1) ->
eqmod (two_p n) (unsigned x) (signed y) ->
sign_ext n x = y.
Lemma zero_ext_eqmod_two_p:
forall x y,
eqmod (two_p n) (unsigned x) (unsigned y) -> zero_ext n x = zero_ext n y.
Lemma sign_ext_eqmod_two_p:
forall x y,
eqmod (two_p n) (unsigned x) (unsigned y) -> sign_ext n x = sign_ext n y.
Lemma eqmod_two_p_zero_ext:
forall x, eqmod (two_p n) (unsigned x) (unsigned (zero_ext n x)).
Lemma eqmod_two_p_sign_ext:
forall x, eqmod (two_p n) (unsigned x) (unsigned (sign_ext n x)).
Theorem sign_ext_idem:
forall x, sign_ext n (sign_ext n x) = sign_ext n x.
Theorem sign_ext_zero_ext:
forall x, sign_ext n (zero_ext n x) = sign_ext n x.
Theorem zero_ext_sign_ext:
forall x, zero_ext n (sign_ext n x) = zero_ext n x.
Theorem sign_ext_equal_if_zero_equal:
forall x y,
zero_ext n x = zero_ext n y ->
sign_ext n x = sign_ext n y.
Lemma eqmod_mult_div:
forall n1 n2 x y,
0 <= n1 -> 0 <= n2 ->
eqmod (two_p (n1+n2)) (two_p n1 * x) y ->
eqmod (two_p n2) x (y / two_p n1).
Theorem sign_ext_shr_shl:
forall x,
let y := repr (Z_of_nat wordsize - n) in
sign_ext n x = shr (shl x y) y.
Theorem zero_ext_shru_shl:
forall x,
let y := repr (Z_of_nat wordsize - n) in
zero_ext n x = shru (shl x y) y.
End EXTENSIONS.
Opaque Z_one_bits.
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_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 shru_lt_zero:
forall x,
shru x (repr (Z_of_nat wordsize - 1)) = if lt x zero then one else zero.
Theorem ltu_range_test:
forall x y,
ltu x y = true -> unsigned y <= max_signed ->
0 <= signed x < unsigned y.
End Make.
Module IntWordsize.
Definition wordsize := 32%nat.
Remark wordsize_not_zero: wordsize <> 0%nat.
End IntWordsize.
Module Int := Make(IntWordsize).
Notation int := Int.int.
Remark int_wordsize_divides_modulus:
Zdivide (Z_of_nat Int.wordsize) Int.modulus.