Formalizations of machine integers modulo 2N.
Require Import Eqdep_dec Zquot Zwf.
Require Import Coqlib.
Require Archi.
Comparisons
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.
Parameterization by the word size, in bits.
Module Type WORDSIZE.
Parameter wordsize:
nat.
Axiom wordsize_not_zero:
wordsize <> 0%
nat.
End WORDSIZE.
Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.
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.
Proof.
Remark modulus_power:
modulus =
two_p zwordsize.
Proof.
Remark modulus_pos:
modulus > 0.
Proof.
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 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.
Proof.
Lemma P_mod_two_p_eq:
forall n p,
P_mod_two_p p n = (
Zpos p)
mod (
two_power_nat n).
Proof.
Lemma Z_mod_modulus_range:
forall x, 0 <=
Z_mod_modulus x <
modulus.
Proof.
Lemma Z_mod_modulus_range':
forall x, -1 <
Z_mod_modulus x <
modulus.
Proof.
Lemma Z_mod_modulus_eq:
forall x,
Z_mod_modulus x =
x mod modulus.
Proof.
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.
Proof.
intros.
subst y.
assert (
forall (
n m:
Z) (
P1 P2:
n <
m),
P1 =
P2).
{
unfold Zlt;
intros.
apply eq_proofs_unicity.
intros c1 c2.
destruct c1;
destruct c2; (
left;
reflexivity) || (
right;
congruence).
}
destruct Px as [
Px1 Px2].
destruct Py as [
Py1 Py2].
rewrite (
H _ _ Px1 Py1).
rewrite (
H _ _ Px2 Py2).
reflexivity.
Qed.
Lemma eq_dec:
forall (
x y:
int), {
x =
y} + {
x <>
y}.
Proof.
intros.
destruct x;
destruct y.
destruct (
zeq intval0 intval1).
left.
apply mkint_eq.
auto.
right.
red;
intro.
injection H.
exact n.
Defined.
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 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.
x86-style extended division and modulus
Definition divmodu2 (
nhi nlo:
int) (
d:
int) :
option (
int *
int) :=
if eq_dec d zero then None else
(
let (
q,
r) :=
Z.div_eucl (
unsigned nhi *
modulus +
unsigned nlo) (
unsigned d)
in
if zle q max_unsigned then Some(
repr q,
repr r)
else None).
Definition divmods2 (
nhi nlo:
int) (
d:
int) :
option (
int *
int) :=
if eq_dec d zero then None else
(
let (
q,
r) :=
Z.quotrem (
signed nhi *
modulus +
unsigned nlo) (
signed d)
in
if zle min_signed q &&
zle q max_signed then Some(
repr q,
repr r)
else None).
Properties of integers and integer arithmetic
Properties of modulus, max_unsigned, etc.
Remark half_modulus_power:
half_modulus =
two_p (
zwordsize - 1).
Proof.
Remark half_modulus_modulus:
modulus = 2 *
half_modulus.
Proof.
Relative positions, from greatest to smallest:
max_unsigned
max_signed
2*wordsize-1
wordsize
0
min_signed
Remark half_modulus_pos:
half_modulus > 0.
Proof.
Remark min_signed_neg:
min_signed < 0.
Proof.
Remark max_signed_pos:
max_signed >= 0.
Proof.
Remark wordsize_max_unsigned:
zwordsize <=
max_unsigned.
Proof.
Remark two_wordsize_max_unsigned: 2 *
zwordsize - 1 <=
max_unsigned.
Proof.
Remark max_signed_unsigned:
max_signed <
max_unsigned.
Proof.
Lemma unsigned_repr_eq:
forall x,
unsigned (
repr x) =
Zmod x modulus.
Proof.
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.
Proof.
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 :=
exists k,
x =
k *
modul +
y.
Lemma eqmod_refl:
forall x,
eqmod x x.
Proof.
intros; red. exists 0. omega.
Qed.
Lemma eqmod_refl2:
forall x y,
x =
y ->
eqmod x y.
Proof.
Lemma eqmod_sym:
forall x y,
eqmod x y ->
eqmod y x.
Proof.
intros x y [k EQ]; red. exists (-k). subst x. ring.
Qed.
Lemma eqmod_trans:
forall x y z,
eqmod x y ->
eqmod y z ->
eqmod x z.
Proof.
intros x y z [k1 EQ1] [k2 EQ2]; red.
exists (k1 + k2). subst x; subst y. ring.
Qed.
Lemma eqmod_small_eq:
forall x y,
eqmod x y -> 0 <=
x <
modul -> 0 <=
y <
modul ->
x =
y.
Proof.
intros x y [
k EQ]
I1 I2.
generalize (
Zdiv_unique _ _ _ _ EQ I2).
intro.
rewrite (
Zdiv_small x modul I1)
in H.
subst k.
omega.
Qed.
Lemma eqmod_mod_eq:
forall x y,
eqmod x y ->
x mod modul =
y mod modul.
Proof.
Lemma eqmod_mod:
forall x,
eqmod x (
x mod modul).
Proof.
Lemma eqmod_add:
forall a b c d,
eqmod a b ->
eqmod c d ->
eqmod (
a +
c) (
b +
d).
Proof.
intros a b c d [k1 EQ1] [k2 EQ2]; red.
subst a; subst c. exists (k1 + k2). ring.
Qed.
Lemma eqmod_neg:
forall x y,
eqmod x y ->
eqmod (-
x) (-
y).
Proof.
intros x y [k EQ]; red. exists (-k). rewrite EQ. ring.
Qed.
Lemma eqmod_sub:
forall a b c d,
eqmod a b ->
eqmod c d ->
eqmod (
a -
c) (
b -
d).
Proof.
intros a b c d [k1 EQ1] [k2 EQ2]; red.
subst a; subst c. exists (k1 - k2). ring.
Qed.
Lemma eqmod_mult:
forall a b c d,
eqmod a c ->
eqmod b d ->
eqmod (
a *
b) (
c *
d).
Proof.
intros a b c d [
k1 EQ1] [
k2 EQ2];
red.
subst a;
subst b.
exists (
k1 *
k2 *
modul +
c *
k2 +
k1 *
d).
ring.
Qed.
End EQ_MODULO.
Lemma eqmod_divides:
forall n m x y,
eqmod n x y ->
Zdivide m n ->
eqmod m x y.
Proof.
intros.
destruct H as [
k1 EQ1].
destruct H0 as [
k2 EQ2].
exists (
k1*
k2).
rewrite <-
Zmult_assoc.
rewrite <-
EQ2.
auto.
Qed.
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_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.
Properties of the coercions between Z and int
Lemma eqm_samerepr:
forall x y,
eqm x y ->
repr x =
repr y.
Proof.
Lemma eqm_unsigned_repr:
forall z,
eqm z (
unsigned (
repr z)).
Proof.
Hint Resolve eqm_unsigned_repr:
ints.
Lemma eqm_unsigned_repr_l:
forall a b,
eqm a b ->
eqm (
unsigned (
repr a))
b.
Proof.
Hint Resolve eqm_unsigned_repr_l:
ints.
Lemma eqm_unsigned_repr_r:
forall a b,
eqm a b ->
eqm a (
unsigned (
repr b)).
Proof.
Hint Resolve eqm_unsigned_repr_r:
ints.
Lemma eqm_signed_unsigned:
forall x,
eqm (
signed x) (
unsigned x).
Proof.
Theorem unsigned_range:
forall i, 0 <=
unsigned i <
modulus.
Proof.
destruct i. simpl. omega.
Qed.
Hint Resolve unsigned_range:
ints.
Theorem unsigned_range_2:
forall i, 0 <=
unsigned i <=
max_unsigned.
Proof.
Hint Resolve unsigned_range_2:
ints.
Theorem signed_range:
forall i,
min_signed <=
signed i <=
max_signed.
Proof.
Theorem repr_unsigned:
forall i,
repr (
unsigned i) =
i.
Proof.
Hint Resolve repr_unsigned:
ints.
Lemma repr_signed:
forall i,
repr (
signed i) =
i.
Proof.
Hint Resolve repr_signed:
ints.
Opaque repr.
Lemma eqm_repr_eq:
forall x y,
eqm x (
unsigned y) ->
repr x =
y.
Proof.
Theorem unsigned_repr:
forall z, 0 <=
z <=
max_unsigned ->
unsigned (
repr z) =
z.
Proof.
Hint Resolve unsigned_repr:
ints.
Theorem signed_repr:
forall z,
min_signed <=
z <=
max_signed ->
signed (
repr z) =
z.
Proof.
Theorem signed_eq_unsigned:
forall x,
unsigned x <=
max_signed ->
signed x =
unsigned x.
Proof.
Theorem signed_positive:
forall x,
signed x >= 0 <->
unsigned x <=
max_signed.
Proof.
Properties of zero, one, minus one
Theorem unsigned_zero:
unsigned zero = 0.
Proof.
Theorem unsigned_one:
unsigned one = 1.
Proof.
Theorem unsigned_mone:
unsigned mone =
modulus - 1.
Proof.
Theorem signed_zero:
signed zero = 0.
Proof.
Theorem signed_mone:
signed mone = -1.
Proof.
Theorem one_not_zero:
one <>
zero.
Proof.
Theorem unsigned_repr_wordsize:
unsigned iwordsize =
zwordsize.
Proof.
Properties of equality
Theorem eq_sym:
forall x y,
eq x y =
eq y x.
Proof.
Theorem eq_spec:
forall (
x y:
int),
if eq x y then x =
y else x <>
y.
Proof.
intros;
unfold eq.
case (
eq_dec x y);
intro.
subst y.
rewrite zeq_true.
auto.
rewrite zeq_false.
auto.
destruct x;
destruct y.
simpl.
red;
intro.
elim n.
apply mkint_eq.
auto.
Qed.
Theorem eq_true:
forall x,
eq x x =
true.
Proof.
intros.
generalize (
eq_spec x x);
case (
eq x x);
intros;
congruence.
Qed.
Theorem eq_false:
forall x y,
x <>
y ->
eq x y =
false.
Proof.
intros.
generalize (
eq_spec x y);
case (
eq x y);
intros;
congruence.
Qed.
Theorem eq_signed:
forall x y,
eq x y =
if zeq (
signed x) (
signed y)
then true else false.
Proof.
Properties of addition
Theorem add_unsigned:
forall x y,
add x y =
repr (
unsigned x +
unsigned y).
Proof.
intros; reflexivity.
Qed.
Theorem add_signed:
forall x y,
add x y =
repr (
signed x +
signed y).
Proof.
Theorem add_commut:
forall x y,
add x y =
add y x.
Proof.
intros;
unfold add.
decEq.
omega. Qed.
Theorem add_zero:
forall x,
add x zero =
x.
Proof.
Theorem add_zero_l:
forall x,
add zero x =
x.
Proof.
Theorem add_assoc:
forall x y z,
add (
add x y)
z =
add x (
add y z).
Proof.
Theorem add_permut:
forall x y z,
add x (
add y z) =
add y (
add x z).
Proof.
Theorem add_neg_zero:
forall x,
add x (
neg x) =
zero.
Proof.
Theorem unsigned_add_carry:
forall x y,
unsigned (
add x y) =
unsigned x +
unsigned y -
unsigned (
add_carry x y zero) *
modulus.
Proof.
Corollary unsigned_add_either:
forall x y,
unsigned (
add x y) =
unsigned x +
unsigned y
\/
unsigned (
add x y) =
unsigned x +
unsigned y -
modulus.
Proof.
Properties of negation
Theorem neg_repr:
forall z,
neg (
repr z) =
repr (-
z).
Proof.
Theorem neg_zero:
neg zero =
zero.
Proof.
Theorem neg_involutive:
forall x,
neg (
neg x) =
x.
Proof.
Theorem neg_add_distr:
forall x y,
neg(
add x y) =
add (
neg x) (
neg y).
Proof.
Properties of subtraction
Theorem sub_zero_l:
forall x,
sub x zero =
x.
Proof.
Theorem sub_zero_r:
forall x,
sub zero x =
neg x.
Proof.
Theorem sub_add_opp:
forall x y,
sub x y =
add x (
neg y).
Proof.
Theorem sub_idem:
forall x,
sub x x =
zero.
Proof.
intros;
unfold sub.
unfold zero.
decEq.
omega.
Qed.
Theorem sub_add_l:
forall x y z,
sub (
add x y)
z =
add (
sub x z)
y.
Proof.
Theorem sub_add_r:
forall x y z,
sub x (
add y z) =
add (
sub x z) (
neg y).
Proof.
Theorem sub_shifted:
forall x y z,
sub (
add x z) (
add y z) =
sub x y.
Proof.
Theorem sub_signed:
forall x y,
sub x y =
repr (
signed x -
signed y).
Proof.
Theorem unsigned_sub_borrow:
forall x y,
unsigned (
sub x y) =
unsigned x -
unsigned y +
unsigned (
sub_borrow x y zero) *
modulus.
Proof.
Properties of multiplication
Theorem mul_commut:
forall x y,
mul x y =
mul y x.
Proof.
intros;
unfold mul.
decEq.
ring.
Qed.
Theorem mul_zero:
forall x,
mul x zero =
zero.
Proof.
Theorem mul_one:
forall x,
mul x one =
x.
Proof.
Theorem mul_mone:
forall x,
mul x mone =
neg x.
Proof.
Theorem mul_assoc:
forall x y z,
mul (
mul x y)
z =
mul x (
mul y z).
Proof.
Theorem mul_add_distr_l:
forall x y z,
mul (
add x y)
z =
add (
mul x z) (
mul y z).
Proof.
Theorem mul_add_distr_r:
forall x y z,
mul x (
add y z) =
add (
mul x y) (
mul x z).
Proof.
Theorem neg_mul_distr_l:
forall x y,
neg(
mul x y) =
mul (
neg x)
y.
Proof.
Theorem neg_mul_distr_r:
forall x y,
neg(
mul x y) =
mul x (
neg y).
Proof.
Theorem mul_signed:
forall x y,
mul x y =
repr (
signed x *
signed y).
Proof.
Properties of division and modulus
Lemma modu_divu_Euclid:
forall x y,
y <>
zero ->
x =
add (
mul (
divu x y)
y) (
modu x y).
Proof.
Theorem modu_divu:
forall x y,
y <>
zero ->
modu x y =
sub x (
mul (
divu x y)
y).
Proof.
Lemma mods_divs_Euclid:
forall x y,
x =
add (
mul (
divs x y)
y) (
mods x y).
Proof.
Theorem mods_divs:
forall x y,
mods x y =
sub x (
mul (
divs x y)
y).
Proof.
Theorem divu_one:
forall x,
divu x one =
x.
Proof.
Theorem modu_one:
forall x,
modu x one =
zero.
Proof.
Theorem divs_mone:
forall x,
divs x mone =
neg x.
Proof.
Theorem mods_mone:
forall x,
mods x mone =
zero.
Proof.
Theorem divmodu2_divu_modu:
forall n d,
d <>
zero ->
divmodu2 zero n d =
Some (
divu n d,
modu n d).
Proof.
Lemma unsigned_signed:
forall n,
unsigned n =
if lt n zero then signed n +
modulus else signed n.
Proof.
Theorem divmods2_divs_mods:
forall n d,
d <>
zero ->
n <>
repr min_signed \/
d <>
mone ->
divmods2 (
if lt n zero then mone else zero)
n d =
Some (
divs n d,
mods n d).
Proof.
unfold divmods2,
divs,
mods;
intros.
rewrite dec_eq_false by auto.
set (
N :=
signed (
if lt n zero then mone else zero) *
modulus +
unsigned n).
set (
D :=
signed d).
assert (
D <> 0).
{
unfold D;
red;
intros.
elim H.
rewrite <- (
repr_signed d).
rewrite H1;
auto. }
assert (
N =
signed n).
{
unfold N.
rewrite unsigned_signed.
destruct (
lt n zero).
rewrite signed_mone.
ring.
rewrite signed_zero.
ring. }
set (
Q :=
Z.quot N D);
set (
R :=
Z.rem N D).
assert (
E2:
Z.quotrem N D = (
Q,
R)).
{
unfold Q,
R,
Z.quot,
Z.rem.
destruct (
Z.quotrem N D);
auto. }
rewrite E2.
assert (
min_signed <=
N <=
max_signed)
by (
rewrite H2;
apply signed_range).
assert (
min_signed <=
Q <=
max_signed).
{
unfold Q.
destruct (
zeq D 1); [ |
destruct (
zeq D (-1))].
-
rewrite e.
rewrite Z.quot_1_r;
auto.
-
rewrite e.
change (-1)
with (
Z.opp 1).
rewrite Z.quot_opp_r by omega.
rewrite Z.quot_1_r.
assert (
N <>
min_signed).
{
red;
intros;
destruct H0.
+
elim H0.
rewrite <- (
repr_signed n).
rewrite <-
H2.
rewrite H4.
auto.
+
elim H0.
rewrite <- (
repr_signed d).
unfold D in e;
rewrite e;
auto. }
unfold min_signed,
max_signed in *.
omega.
-
assert (
Z.abs (
Z.quot N D) <
half_modulus).
{
rewrite <-
Z.quot_abs by omega.
apply Zquot_lt_upper_bound.
xomega.
xomega.
apply Zle_lt_trans with (
half_modulus * 1).
rewrite Z.mul_1_r.
unfold min_signed,
max_signed in H3;
xomega.
apply Zmult_lt_compat_l.
generalize half_modulus_pos;
omega.
xomega. }
rewrite Z.abs_lt in H4.
unfold min_signed,
max_signed;
omega.
}
unfold proj_sumbool;
rewrite !
zle_true by omega;
simpl.
unfold Q,
R;
rewrite H2;
auto.
Qed.
Bit-level properties
Properties of bit-level operations over Z
Remark Ztestbit_0:
forall n,
Z.testbit 0
n =
false.
Proof Z.testbit_0_l.
Remark Ztestbit_1:
forall n,
Z.testbit 1
n =
zeq n 0.
Proof.
intros. destruct n; simpl; auto.
Qed.
Remark Ztestbit_m1:
forall n, 0 <=
n ->
Z.testbit (-1)
n =
true.
Proof.
intros. destruct n; simpl; auto.
Qed.
Remark Zshiftin_spec:
forall b x,
Zshiftin b x = 2 *
x + (
if b then 1
else 0).
Proof.
Remark Zshiftin_inj:
forall b1 x1 b2 x2,
Zshiftin b1 x1 =
Zshiftin b2 x2 ->
b1 =
b2 /\
x1 =
x2.
Proof.
intros.
rewrite !
Zshiftin_spec in H.
destruct b1;
destruct b2.
split; [
auto|
omega].
omegaContradiction.
omegaContradiction.
split; [
auto|
omega].
Qed.
Remark Zdecomp:
forall x,
x =
Zshiftin (
Z.odd x) (
Z.div2 x).
Proof.
intros.
destruct x;
simpl.
-
auto.
-
destruct p;
auto.
-
destruct p;
auto.
simpl.
rewrite Pos.pred_double_succ.
auto.
Qed.
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).
Proof.
Remark Ztestbit_shiftin_base:
forall b x,
Z.testbit (
Zshiftin b x) 0 =
b.
Proof.
Remark Ztestbit_shiftin_succ:
forall b x n, 0 <=
n ->
Z.testbit (
Zshiftin b x) (
Z.succ n) =
Z.testbit x n.
Proof.
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).
Proof.
Remark Ztestbit_base:
forall x,
Z.testbit x 0 =
Z.odd x.
Proof.
Remark Ztestbit_succ:
forall n x, 0 <=
n ->
Z.testbit x (
Z.succ n) =
Z.testbit (
Z.div2 x)
n.
Proof.
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.
Proof.
Lemma eqm_same_bits:
forall x y,
(
forall i, 0 <=
i <
zwordsize ->
Z.testbit x i =
Z.testbit y i) ->
eqm x y.
Proof (
eqmod_same_bits wordsize).
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.
Proof.
Lemma same_bits_eqm:
forall x y i,
eqm x y ->
0 <=
i <
zwordsize ->
Z.testbit x i =
Z.testbit y i.
Proof (
same_bits_eqmod wordsize).
Remark two_power_nat_infinity:
forall x, 0 <=
x ->
exists n,
x <
two_power_nat n.
Proof.
Lemma equal_same_bits:
forall x y,
(
forall i, 0 <=
i ->
Z.testbit x i =
Z.testbit y i) ->
x =
y.
Proof.
Lemma Z_one_complement:
forall i, 0 <=
i ->
forall x,
Z.testbit (-
x-1)
i =
negb (
Z.testbit x i).
Proof.
Lemma Ztestbit_above:
forall n x i,
0 <=
x <
two_power_nat n ->
i >=
Z.of_nat n ->
Z.testbit x i =
false.
Proof.
Lemma Ztestbit_above_neg:
forall n x i,
-
two_power_nat n <=
x < 0 ->
i >=
Z.of_nat n ->
Z.testbit x i =
true.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma Ztestbit_le:
forall x y,
0 <=
y ->
(
forall i, 0 <=
i ->
Z.testbit x i =
true ->
Z.testbit y i =
true) ->
x <=
y.
Proof.
Bit-level reasoning over type int
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.
Proof.
Lemma same_bits_eq:
forall x y,
(
forall i, 0 <=
i <
zwordsize ->
testbit x i =
testbit y i) ->
x =
y.
Proof.
Lemma bits_above:
forall x i,
i >=
zwordsize ->
testbit x i =
false.
Proof.
Lemma bits_zero:
forall i,
testbit zero i =
false.
Proof.
Remark bits_one:
forall n,
testbit one n =
zeq n 0.
Proof.
Lemma bits_mone:
forall i, 0 <=
i <
zwordsize ->
testbit mone i =
true.
Proof.
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.
Proof.
Lemma bits_signed:
forall x i, 0 <=
i ->
Z.testbit (
signed x)
i =
testbit x (
if zlt i zwordsize then i else zwordsize - 1).
Proof.
Lemma bits_le:
forall x y,
(
forall i, 0 <=
i <
zwordsize ->
testbit x i =
true ->
testbit y i =
true) ->
unsigned x <=
unsigned y.
Proof.
Properties of bitwise and, or, xor
Lemma bits_and:
forall x y i, 0 <=
i <
zwordsize ->
testbit (
and x y)
i =
testbit x i &&
testbit y i.
Proof.
Lemma bits_or:
forall x y i, 0 <=
i <
zwordsize ->
testbit (
or x y)
i =
testbit x i ||
testbit y i.
Proof.
Lemma bits_xor:
forall x y i, 0 <=
i <
zwordsize ->
testbit (
xor x y)
i =
xorb (
testbit x i) (
testbit y i).
Proof.
Lemma bits_not:
forall x i, 0 <=
i <
zwordsize ->
testbit (
not x)
i =
negb (
testbit x i).
Proof.
Hint Rewrite bits_and bits_or bits_xor bits_not:
ints.
Theorem and_commut:
forall x y,
and x y =
and y x.
Proof.
bit_solve.
Qed.
Theorem and_assoc:
forall x y z,
and (
and x y)
z =
and x (
and y z).
Proof.
bit_solve.
Qed.
Theorem and_zero:
forall x,
and x zero =
zero.
Proof.
Corollary and_zero_l:
forall x,
and zero x =
zero.
Proof.
Theorem and_mone:
forall x,
and x mone =
x.
Proof.
Corollary and_mone_l:
forall x,
and mone x =
x.
Proof.
Theorem and_idem:
forall x,
and x x =
x.
Proof.
bit_solve.
destruct (
testbit x i);
auto.
Qed.
Theorem or_commut:
forall x y,
or x y =
or y x.
Proof.
bit_solve.
Qed.
Theorem or_assoc:
forall x y z,
or (
or x y)
z =
or x (
or y z).
Proof.
bit_solve.
Qed.
Theorem or_zero:
forall x,
or x zero =
x.
Proof.
bit_solve.
Qed.
Corollary or_zero_l:
forall x,
or zero x =
x.
Proof.
Theorem or_mone:
forall x,
or x mone =
mone.
Proof.
bit_solve.
Qed.
Theorem or_idem:
forall x,
or x x =
x.
Proof.
bit_solve.
destruct (
testbit x i);
auto.
Qed.
Theorem and_or_distrib:
forall x y z,
and x (
or y z) =
or (
and x y) (
and x z).
Proof.
Corollary and_or_distrib_l:
forall x y z,
and (
or x y)
z =
or (
and x z) (
and y z).
Proof.
Theorem or_and_distrib:
forall x y z,
or x (
and y z) =
and (
or x y) (
or x z).
Proof.
Corollary or_and_distrib_l:
forall x y z,
or (
and x y)
z =
and (
or x z) (
or y z).
Proof.
Theorem and_or_absorb:
forall x y,
and x (
or x y) =
x.
Proof.
bit_solve.
assert (
forall a b,
a && (
a ||
b) =
a)
by destr_bool.
auto.
Qed.
Theorem or_and_absorb:
forall x y,
or x (
and x y) =
x.
Proof.
bit_solve.
assert (
forall a b,
a || (
a &&
b) =
a)
by destr_bool.
auto.
Qed.
Theorem xor_commut:
forall x y,
xor x y =
xor y x.
Proof.
Theorem xor_assoc:
forall x y z,
xor (
xor x y)
z =
xor x (
xor y z).
Proof.
Theorem xor_zero:
forall x,
xor x zero =
x.
Proof.
Corollary xor_zero_l:
forall x,
xor zero x =
x.
Proof.
Theorem xor_idem:
forall x,
xor x x =
zero.
Proof.
Theorem xor_zero_one:
xor zero one =
one.
Proof.
Theorem xor_one_one:
xor one one =
zero.
Proof.
Theorem xor_zero_equal:
forall x y,
xor x y =
zero ->
x =
y.
Proof.
Theorem and_xor_distrib:
forall x y z,
and x (
xor y z) =
xor (
and x y) (
and x z).
Proof.
bit_solve.
assert (
forall a b c,
a && (
xorb b c) =
xorb (
a &&
b) (
a &&
c))
by destr_bool.
auto.
Qed.
Theorem and_le:
forall x y,
unsigned (
and x y) <=
unsigned x.
Proof.
Theorem or_le:
forall x y,
unsigned x <=
unsigned (
or x y).
Proof.
intros.
apply bits_le;
intros.
rewrite bits_or;
auto.
rewrite H0;
auto.
Qed.
Properties of bitwise complement.
Theorem not_involutive:
forall (
x:
int),
not (
not x) =
x.
Proof.
Theorem not_zero:
not zero =
mone.
Proof.
Theorem not_mone:
not mone =
zero.
Proof.
Theorem not_or_and_not:
forall x y,
not (
or x y) =
and (
not x) (
not y).
Proof.
Theorem not_and_or_not:
forall x y,
not (
and x y) =
or (
not x) (
not y).
Proof.
Theorem and_not_self:
forall x,
and x (
not x) =
zero.
Proof.
bit_solve.
Qed.
Theorem or_not_self:
forall x,
or x (
not x) =
mone.
Proof.
bit_solve.
Qed.
Theorem xor_not_self:
forall x,
xor x (
not x) =
mone.
Proof.
bit_solve.
destruct (
testbit x i);
auto.
Qed.
Lemma unsigned_not:
forall x,
unsigned (
not x) =
max_unsigned -
unsigned x.
Proof.
Theorem not_neg:
forall x,
not x =
add (
neg x)
mone.
Proof.
Theorem neg_not:
forall x,
neg x =
add (
not x)
one.
Proof.
Theorem sub_add_not:
forall x y,
sub x y =
add (
add x (
not y))
one.
Proof.
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).
Proof.
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.
Proof.
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.
Proof.
Theorem add_is_or:
forall x y,
and x y =
zero ->
add x y =
or x y.
Proof.
Theorem xor_is_or:
forall x y,
and x y =
zero ->
xor x y =
or x y.
Proof.
bit_solve.
assert (
testbit (
and x y)
i =
testbit zero i)
by congruence.
autorewrite with ints in H1;
auto.
destruct (
testbit x i);
destruct (
testbit y i);
simpl in *;
congruence.
Qed.
Theorem add_is_xor:
forall x y,
and x y =
zero ->
add x y =
xor x y.
Proof.
Theorem add_and:
forall x y z,
and y z =
zero ->
add (
and x y) (
and x z) =
and x (
or y z).
Proof.
Properties of shifts
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).
Proof.
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.
Proof.
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).
Proof.
Hint Rewrite bits_shl bits_shru bits_shr:
ints.
Theorem shl_zero:
forall x,
shl x zero =
x.
Proof.
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.
Proof.
Theorem and_shl:
forall x y n,
and (
shl x n) (
shl y n) =
shl (
and x y)
n.
Proof.
Theorem or_shl:
forall x y n,
or (
shl x n) (
shl y n) =
shl (
or x y)
n.
Proof.
Theorem xor_shl:
forall x y n,
xor (
shl x n) (
shl y n) =
shl (
xor x y)
n.
Proof.
Lemma ltu_inv:
forall x y,
ltu x y =
true -> 0 <=
unsigned x <
unsigned y.
Proof.
Lemma ltu_iwordsize_inv:
forall x,
ltu x iwordsize =
true -> 0 <=
unsigned x <
zwordsize.
Proof.
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).
Proof.
Theorem shru_zero:
forall x,
shru x zero =
x.
Proof.
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.
Proof.
Theorem and_shru:
forall x y n,
and (
shru x n) (
shru y n) =
shru (
and x y)
n.
Proof.
Theorem or_shru:
forall x y n,
or (
shru x n) (
shru y n) =
shru (
or x y)
n.
Proof.
Theorem xor_shru:
forall x y n,
xor (
shru x n) (
shru y n) =
shru (
xor x y)
n.
Proof.
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).
Proof.
Theorem shr_zero:
forall x,
shr x zero =
x.
Proof.
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.
Proof.
Theorem and_shr:
forall x y n,
and (
shr x n) (
shr y n) =
shr (
and x y)
n.
Proof.
Theorem or_shr:
forall x y n,
or (
shr x n) (
shr y n) =
shr (
or x y)
n.
Proof.
Theorem xor_shr:
forall x y n,
xor (
shr x n) (
shr y n) =
shr (
xor x y)
n.
Proof.
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).
Proof.
Theorem and_shr_shru:
forall x y z,
and (
shr x z) (
shru y z) =
shru (
and x y)
z.
Proof.
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.
Proof.
Theorem shru_lt_zero:
forall x,
shru x (
repr (
zwordsize - 1)) =
if lt x zero then one else zero.
Proof.
Theorem shr_lt_zero:
forall x,
shr x (
repr (
zwordsize - 1)) =
if lt x zero then mone else zero.
Proof.
Properties of rotations
Lemma bits_rol:
forall x y i,
0 <=
i <
zwordsize ->
testbit (
rol x y)
i =
testbit x ((
i -
unsigned y)
mod zwordsize).
Proof.
Lemma bits_ror:
forall x y i,
0 <=
i <
zwordsize ->
testbit (
ror x y)
i =
testbit x ((
i +
unsigned y)
mod zwordsize).
Proof.
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).
Proof.
Theorem shru_rolm:
forall x n,
ltu n iwordsize =
true ->
shru x n =
rolm x (
sub iwordsize n) (
shru mone n).
Proof.
Theorem rol_zero:
forall x,
rol x zero =
x.
Proof.
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).
Proof.
Theorem rol_and:
forall x y n,
rol (
and x y)
n =
and (
rol x n) (
rol y n).
Proof.
Theorem rol_or:
forall x y n,
rol (
or x y)
n =
or (
rol x n) (
rol y n).
Proof.
Theorem rol_xor:
forall x y n,
rol (
xor x y)
n =
xor (
rol x n) (
rol y n).
Proof.
Theorem rol_rol:
forall x n m,
Zdivide zwordsize modulus ->
rol (
rol x n)
m =
rol x (
modu (
add n m)
iwordsize).
Proof.
Theorem rolm_zero:
forall x m,
rolm x zero m =
and x m.
Proof.
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).
Proof.
Theorem or_rolm:
forall x n m1 m2,
or (
rolm x n m1) (
rolm x n m2) =
rolm x n (
or m1 m2).
Proof.
Theorem ror_rol:
forall x y,
ltu y iwordsize =
true ->
ror x y =
rol x (
sub iwordsize y).
Proof.
Theorem ror_rol_neg:
forall x y, (
zwordsize |
modulus) ->
ror x y =
rol x (
neg y).
Proof.
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).
Proof.
Properties of Z_one_bits and is_power2.
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).
Proof.
Lemma Z_one_bits_range:
forall x i,
In i (
Z_one_bits wordsize x 0) -> 0 <=
i <
zwordsize.
Proof.
Lemma is_power2_rng:
forall n logn,
is_power2 n =
Some logn ->
0 <=
unsigned logn <
zwordsize.
Proof.
Theorem is_power2_range:
forall n logn,
is_power2 n =
Some logn ->
ltu logn iwordsize =
true.
Proof.
Lemma is_power2_correct:
forall n logn,
is_power2 n =
Some logn ->
unsigned n =
two_p (
unsigned logn).
Proof.
Remark two_p_range:
forall n,
0 <=
n <
zwordsize ->
0 <=
two_p n <=
max_unsigned.
Proof.
Remark Z_one_bits_zero:
forall n i,
Z_one_bits n 0
i =
nil.
Proof.
induction n; intros; simpl; auto.
Qed.
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.
Proof.
Lemma is_power2_two_p:
forall n, 0 <=
n <
zwordsize ->
is_power2 (
repr (
two_p n)) =
Some (
repr n).
Proof.
Relation between bitwise operations and multiplications / divisions by powers of 2
Left shifts and multiplications by powers of 2.
Lemma Zshiftl_mul_two_p:
forall x n, 0 <=
n ->
Z.shiftl x n =
x *
two_p n.
Proof.
Lemma shl_mul_two_p:
forall x y,
shl x y =
mul x (
repr (
two_p (
unsigned y))).
Proof.
Theorem shl_mul:
forall x y,
shl x y =
mul x (
shl one y).
Proof.
Theorem mul_pow2:
forall x n logn,
is_power2 n =
Some logn ->
mul x n =
shl x logn.
Proof.
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).
Proof.
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.
Proof.
Lemma shru_div_two_p:
forall x y,
shru x y =
repr (
unsigned x /
two_p (
unsigned y)).
Proof.
Theorem divu_pow2:
forall x n logn,
is_power2 n =
Some logn ->
divu x n =
shru x logn.
Proof.
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)).
Proof.
Theorem divs_pow2:
forall x n logn,
is_power2 n =
Some logn ->
divs x n =
shrx x logn.
Proof.
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.
Proof.
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.
Proof.
Theorem modu_and:
forall x n logn,
is_power2 n =
Some logn ->
modu x n =
and x (
sub n one).
Proof.
Properties of shrx (signed division by a power of 2)
Lemma Zquot_Zdiv:
forall x y,
y > 0 ->
Z.quot x y =
if zlt x 0
then (
x +
y - 1) /
y else x /
y.
Proof.
intros.
destruct (
zlt x 0).
-
symmetry.
apply Zquot_unique_full with ((
x +
y - 1)
mod y - (
y - 1)).
+
red.
right;
split.
omega.
exploit (
Z_mod_lt (
x +
y - 1)
y);
auto.
rewrite Z.abs_eq.
omega.
omega.
+
transitivity ((
y * ((
x +
y - 1) /
y) + (
x +
y - 1)
mod y) - (
y-1)).
rewrite <-
Z_div_mod_eq.
ring.
auto.
ring.
-
apply Zquot_Zdiv_pos;
omega.
Qed.
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.
Proof.
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.
Proof.
Lemma Zdiv_shift:
forall x y,
y > 0 ->
(
x + (
y - 1)) /
y =
x /
y +
if zeq (
Zmod x y) 0
then 0
else 1.
Proof.
intros.
generalize (
Z_div_mod_eq x y H).
generalize (
Z_mod_lt x y H).
set (
q :=
x /
y).
set (
r :=
x mod y).
intros.
destruct (
zeq r 0).
apply Zdiv_unique with (
y - 1).
rewrite H1.
rewrite e.
ring.
omega.
apply Zdiv_unique with (
r - 1).
rewrite H1.
ring.
omega.
Qed.
Theorem shrx_carry:
forall x y,
ltu y (
repr (
zwordsize - 1)) =
true ->
shrx x y =
add (
shr x y) (
shr_carry x y).
Proof.
Connections between shr and shru.
Lemma shr_shru_positive:
forall x y,
signed x >= 0 ->
shr x y =
shru x y.
Proof.
Lemma and_positive:
forall x y,
signed y >= 0 ->
signed (
and x y) >= 0.
Proof.
Theorem shr_and_is_shru_and:
forall x y z,
lt y zero =
false ->
shr (
and x y)
z =
shru (
and x y)
z.
Proof.
Properties of integer zero extension and sign extension.
Lemma Ziter_base:
forall (
A:
Type)
n (
f:
A ->
A)
x,
n <= 0 ->
Z.iter n f x =
x.
Proof.
intros.
unfold Z.iter.
destruct n;
auto.
compute in H.
elim H;
auto.
Qed.
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).
Proof.
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.
Proof.
intros.
destruct (
zle 0
n).
apply natlike_ind;
auto.
apply H;
omega.
apply H.
omega.
Qed.
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.
Proof.
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.
Proof.
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).
Proof.
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).
Proof.
Hint Rewrite bits_zero_ext bits_sign_ext:
ints.
Theorem zero_ext_above:
forall n x,
n >=
zwordsize ->
zero_ext n x =
x.
Proof.
Theorem sign_ext_above:
forall n x,
n >=
zwordsize ->
sign_ext n x =
x.
Proof.
Theorem zero_ext_and:
forall n x, 0 <=
n ->
zero_ext n x =
and x (
repr (
two_p n - 1)).
Proof.
Theorem zero_ext_mod:
forall n x, 0 <=
n <
zwordsize ->
unsigned (
zero_ext n x) =
Zmod (
unsigned x) (
two_p n).
Proof.
Theorem zero_ext_widen:
forall x n n', 0 <=
n <=
n' ->
zero_ext n' (
zero_ext n x) =
zero_ext n x.
Proof.
bit_solve.
destruct (
zlt i n).
apply zlt_true.
omega.
destruct (
zlt i n');
auto.
tauto.
tauto.
Qed.
Theorem sign_ext_widen:
forall x n n', 0 <
n <=
n' ->
sign_ext n' (
sign_ext n x) =
sign_ext n x.
Proof.
intros.
destruct (
zlt n'
zwordsize).
bit_solve.
destruct (
zlt i n').
auto.
rewrite (
zlt_false _ i n).
destruct (
zlt (
n' - 1)
n);
f_equal;
omega.
omega.
omega.
destruct (
zlt i n');
omega.
omega.
omega.
apply sign_ext_above;
auto.
Qed.
Theorem sign_zero_ext_widen:
forall x n n', 0 <=
n <
n' ->
sign_ext n' (
zero_ext n x) =
zero_ext n x.
Proof.
Theorem zero_ext_narrow:
forall x n n', 0 <=
n <=
n' ->
zero_ext n (
zero_ext n'
x) =
zero_ext n x.
Proof.
bit_solve.
destruct (
zlt i n).
apply zlt_true.
omega.
auto.
omega.
omega.
omega.
Qed.
Theorem sign_ext_narrow:
forall x n n', 0 <
n <=
n' ->
sign_ext n (
sign_ext n'
x) =
sign_ext n x.
Proof.
Theorem zero_sign_ext_narrow:
forall x n n', 0 <
n <=
n' ->
zero_ext n (
sign_ext n'
x) =
zero_ext n x.
Proof.
Theorem zero_ext_idem:
forall n x, 0 <=
n ->
zero_ext n (
zero_ext n x) =
zero_ext n x.
Proof.
Theorem sign_ext_idem:
forall n x, 0 <
n ->
sign_ext n (
sign_ext n x) =
sign_ext n x.
Proof.
Theorem sign_ext_zero_ext:
forall n x, 0 <
n ->
sign_ext n (
zero_ext n x) =
sign_ext n x.
Proof.
Theorem zero_ext_sign_ext:
forall n x, 0 <
n ->
zero_ext n (
sign_ext n x) =
zero_ext n x.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma eqmod_zero_ext:
forall n x, 0 <=
n <
zwordsize ->
eqmod (
two_p n) (
unsigned (
zero_ext n x)) (
unsigned x).
Proof.
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).
Proof.
Lemma eqmod_sign_ext':
forall n x, 0 <
n <
zwordsize ->
eqmod (
two_p n) (
unsigned (
sign_ext n x)) (
unsigned x).
Proof.
Lemma eqmod_sign_ext:
forall n x, 0 <
n <
zwordsize ->
eqmod (
two_p n) (
signed (
sign_ext n x)) (
unsigned x).
Proof.
Properties of one_bits (decomposition in sum of powers of two)
Theorem one_bits_range:
forall x i,
In i (
one_bits x) ->
ltu i iwordsize =
true.
Proof.
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).
Proof.
Properties of comparisons
Theorem negate_cmp:
forall c x y,
cmp (
negate_comparison c)
x y =
negb (
cmp c x y).
Proof.
intros.
destruct c;
simpl;
try rewrite negb_elim;
auto.
Qed.
Theorem negate_cmpu:
forall c x y,
cmpu (
negate_comparison c)
x y =
negb (
cmpu c x y).
Proof.
intros.
destruct c;
simpl;
try rewrite negb_elim;
auto.
Qed.
Theorem swap_cmp:
forall c x y,
cmp (
swap_comparison c)
x y =
cmp c y x.
Proof.
intros.
destruct c;
simpl;
auto.
apply eq_sym.
decEq.
apply eq_sym.
Qed.
Theorem swap_cmpu:
forall c x y,
cmpu (
swap_comparison c)
x y =
cmpu c y x.
Proof.
intros.
destruct c;
simpl;
auto.
apply eq_sym.
decEq.
apply eq_sym.
Qed.
Lemma translate_eq:
forall x y d,
eq (
add x d) (
add y d) =
eq x y.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Theorem notbool_isfalse_istrue:
forall x,
is_false x ->
is_true (
notbool x).
Proof.
Theorem notbool_istrue_isfalse:
forall x,
is_true x ->
is_false (
notbool x).
Proof.
Theorem ltu_range_test:
forall x y,
ltu x y =
true ->
unsigned y <=
max_signed ->
0 <=
signed x <
unsigned y.
Proof.
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.
Proof.
Lemma signed_eq:
forall x y,
eq x y =
zeq (
signed x) (
signed y).
Proof.
Lemma not_lt:
forall x y,
negb (
lt y x) = (
lt x y ||
eq x y).
Proof.
Lemma lt_not:
forall x y,
lt y x =
negb (
lt x y) &&
negb (
eq x y).
Proof.
Lemma not_ltu:
forall x y,
negb (
ltu y x) = (
ltu x y ||
eq x y).
Proof.
Lemma ltu_not:
forall x y,
ltu y x =
negb (
ltu x y) &&
negb (
eq x y).
Proof.
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).
Proof.
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.
Proof.
destruct x; simpl. omega. compute; intuition congruence. omega.
Qed.
Remark Zsize_pos':
forall x, 0 <
x -> 0 <
Zsize x.
Proof.
destruct x; simpl; intros; try discriminate. compute; auto.
Qed.
Lemma Zsize_shiftin:
forall b x, 0 <
x ->
Zsize (
Zshiftin b x) =
Zsucc (
Zsize x).
Proof.
Lemma Ztestbit_size_1:
forall x, 0 <
x ->
Z.testbit x (
Zpred (
Zsize x)) =
true.
Proof.
Lemma Ztestbit_size_2:
forall x, 0 <=
x ->
forall i,
i >=
Zsize x ->
Z.testbit x i =
false.
Proof.
Lemma Zsize_interval_1:
forall x, 0 <=
x -> 0 <=
x <
two_p (
Zsize x).
Proof.
Lemma Zsize_interval_2:
forall x n, 0 <=
n -> 0 <=
x <
two_p n ->
n >=
Zsize x.
Proof.
Lemma Zsize_monotone:
forall x y, 0 <=
x <=
y ->
Zsize x <=
Zsize y.
Proof.
Theorem size_zero:
size zero = 0.
Proof.
Theorem bits_size_1:
forall x,
x =
zero \/
testbit x (
Zpred (
size x)) =
true.
Proof.
Theorem bits_size_2:
forall x i,
size x <=
i ->
testbit x i =
false.
Proof.
Theorem size_range:
forall x, 0 <=
size x <=
zwordsize.
Proof.
Theorem bits_size_3:
forall x n,
0 <=
n ->
(
forall i,
n <=
i <
zwordsize ->
testbit x i =
false) ->
size x <=
n.
Proof.
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.
Proof.
Theorem size_interval_1:
forall x, 0 <=
unsigned x <
two_p (
size x).
Proof.
Theorem size_interval_2:
forall x n, 0 <=
n -> 0 <=
unsigned x <
two_p n ->
n >=
size x.
Proof.
Theorem size_and:
forall a b,
size (
and a b) <=
Z.min (
size a) (
size b).
Proof.
Corollary and_interval:
forall a b, 0 <=
unsigned (
and a b) <
two_p (
Z.min (
size a) (
size b)).
Proof.
Theorem size_or:
forall a b,
size (
or a b) =
Z.max (
size a) (
size b).
Proof.
Corollary or_interval:
forall a b, 0 <=
unsigned (
or a b) <
two_p (
Z.max (
size a) (
size b)).
Proof.
Theorem size_xor:
forall a b,
size (
xor a b) <=
Z.max (
size a) (
size b).
Proof.
Corollary xor_interval:
forall a b, 0 <=
unsigned (
xor a b) <
two_p (
Z.max (
size a) (
size b)).
Proof.
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.
Proof.
End Wordsize_32.
Strategy opaque [
Wordsize_32.wordsize].
Module Int :=
Make(
Wordsize_32).
Strategy 0 [
Wordsize_32.wordsize].
Notation int :=
Int.int.
Remark int_wordsize_divides_modulus:
Zdivide (
Z_of_nat Int.wordsize)
Int.modulus.
Proof.
exists (
two_p (32-5));
reflexivity.
Qed.
Module Wordsize_8.
Definition wordsize := 8%
nat.
Remark wordsize_not_zero:
wordsize <> 0%
nat.
Proof.
End Wordsize_8.
Strategy opaque [
Wordsize_8.wordsize].
Module Byte :=
Make(
Wordsize_8).
Strategy 0 [
Wordsize_8.wordsize].
Notation byte :=
Byte.int.
Module Wordsize_64.
Definition wordsize := 64%
nat.
Remark wordsize_not_zero:
wordsize <> 0%
nat.
Proof.
End Wordsize_64.
Strategy opaque [
Wordsize_64.wordsize].
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)).
Definition shrx' (
x:
int) (
y:
Int.int):
int :=
divs x (
shl'
one 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).
Proof.
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.
Proof.
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).
Proof.
Lemma shl'
_mul_two_p:
forall x y,
shl'
x y =
mul x (
repr (
two_p (
Int.unsigned y))).
Proof.
Lemma shl'
_one_two_p:
forall y,
shl'
one y =
repr (
two_p (
Int.unsigned y)).
Proof.
Theorem shl'
_mul:
forall x y,
shl'
x y =
mul x (
shl'
one y).
Proof.
intros. rewrite shl'_one_two_p. apply shl'_mul_two_p.
Qed.
Theorem shrx'
_zero:
forall x,
shrx'
x Int.zero =
x.
Proof.
Theorem shrx'
_shr_2:
forall x y,
Int.ltu y (
Int.repr 63) =
true ->
shrx'
x y =
shr' (
add x (
shru' (
shr'
x (
Int.repr 63)) (
Int.sub (
Int.repr 64)
y)))
y.
Proof.
Remark int_ltu_2_inv:
forall y z,
Int.ltu y iwordsize' =
true ->
Int.ltu z iwordsize' =
true ->
Int.unsigned (
Int.add y z) <=
Int.unsigned iwordsize' ->
let y' :=
repr (
Int.unsigned y)
in
let z' :=
repr (
Int.unsigned z)
in
Int.unsigned y =
unsigned y'
/\
Int.unsigned z =
unsigned z'
/\
ltu y'
iwordsize =
true
/\
ltu z'
iwordsize =
true
/\
Int.unsigned (
Int.add y z) =
unsigned (
add y'
z')
/\
add y'
z' =
repr (
Int.unsigned (
Int.add y z)).
Proof.
Theorem or_ror':
forall x y z,
Int.ltu y iwordsize' =
true ->
Int.ltu z iwordsize' =
true ->
Int.add y z =
iwordsize' ->
ror x (
repr (
Int.unsigned z)) =
or (
shl'
x y) (
shru'
x z).
Proof.
intros.
destruct (
int_ltu_2_inv y z)
as (
A &
B &
C &
D &
E &
F);
auto.
rewrite H1;
omega.
replace (
shl'
x y)
with (
shl x (
repr (
Int.unsigned y))).
replace (
shru'
x z)
with (
shru x (
repr (
Int.unsigned z))).
apply or_ror;
auto.
rewrite F,
H1.
reflexivity.
unfold shru,
shru';
rewrite <-
B;
auto.
unfold shl,
shl';
rewrite <-
A;
auto.
Qed.
Theorem shl'
_shl':
forall x y z,
Int.ltu y iwordsize' =
true ->
Int.ltu z iwordsize' =
true ->
Int.ltu (
Int.add y z)
iwordsize' =
true ->
shl' (
shl'
x y)
z =
shl'
x (
Int.add y z).
Proof.
Theorem shru'
_shru':
forall x y z,
Int.ltu y iwordsize' =
true ->
Int.ltu z iwordsize' =
true ->
Int.ltu (
Int.add y z)
iwordsize' =
true ->
shru' (
shru'
x y)
z =
shru'
x (
Int.add y z).
Proof.
Theorem shr'
_shr':
forall x y z,
Int.ltu y iwordsize' =
true ->
Int.ltu z iwordsize' =
true ->
Int.ltu (
Int.add y z)
iwordsize' =
true ->
shr' (
shr'
x y)
z =
shr'
x (
Int.add y z).
Proof.
Powers of two with exponents given as 32-bit ints
Definition one_bits' (
x:
int) :
list Int.int :=
List.map Int.repr (
Z_one_bits wordsize (
unsigned x) 0).
Definition is_power2' (
x:
int) :
option Int.int :=
match Z_one_bits wordsize (
unsigned x) 0
with
|
i ::
nil =>
Some (
Int.repr i)
|
_ =>
None
end.
Theorem one_bits'
_range:
forall x i,
In i (
one_bits'
x) ->
Int.ltu i iwordsize' =
true.
Proof.
Fixpoint int_of_one_bits' (
l:
list Int.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).
Proof.
Lemma is_power2'
_rng:
forall n logn,
is_power2'
n =
Some logn ->
0 <=
Int.unsigned logn <
zwordsize.
Proof.
Theorem is_power2'
_range:
forall n logn,
is_power2'
n =
Some logn ->
Int.ltu logn iwordsize' =
true.
Proof.
Lemma is_power2'
_correct:
forall n logn,
is_power2'
n =
Some logn ->
unsigned n =
two_p (
Int.unsigned logn).
Proof.
Theorem mul_pow2':
forall x n logn,
is_power2'
n =
Some logn ->
mul x n =
shl'
x logn.
Proof.
intros.
rewrite shl'
_mul.
f_equal.
rewrite shl'
_one_two_p.
rewrite <- (
repr_unsigned n).
f_equal.
apply is_power2'
_correct;
auto.
Qed.
Theorem divu_pow2':
forall x n logn,
is_power2'
n =
Some logn ->
divu x n =
shru'
x logn.
Proof.
intros.
generalize (
is_power2'
_correct n logn H).
intro.
symmetry.
unfold divu.
rewrite H0.
unfold shru'.
rewrite Zshiftr_div_two_p.
auto.
eapply is_power2'
_rng;
eauto.
Qed.
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.
Proof.
Lemma bits_hiword:
forall n i, 0 <=
i <
Int.zwordsize ->
Int.testbit (
hiword n)
i =
testbit n (
i +
Int.zwordsize).
Proof.
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).
Proof.
Lemma lo_ofwords:
forall hi lo,
loword (
ofwords hi lo) =
lo.
Proof.
Lemma hi_ofwords:
forall hi lo,
hiword (
ofwords hi lo) =
hi.
Proof.
Lemma ofwords_recompose:
forall n,
ofwords (
hiword n) (
loword n) =
n.
Proof.
Lemma ofwords_add:
forall lo hi,
ofwords hi lo =
repr (
Int.unsigned hi *
two_p 32 +
Int.unsigned lo).
Proof.
Lemma ofwords_add':
forall lo hi,
unsigned (
ofwords hi lo) =
Int.unsigned hi *
two_p 32 +
Int.unsigned lo.
Proof.
Remark eqm_mul_2p32:
forall x y,
Int.eqm x y ->
eqm (
x *
two_p 32) (
y *
two_p 32).
Proof.
Lemma ofwords_add'':
forall lo hi,
signed (
ofwords hi lo) =
Int.signed hi *
two_p 32 +
Int.unsigned lo.
Proof.
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).
Proof.
Lemma decompose_and:
forall xh xl yh yl,
and (
ofwords xh xl) (
ofwords yh yl) =
ofwords (
Int.and xh yh) (
Int.and xl yl).
Proof.
Lemma decompose_or:
forall xh xl yh yl,
or (
ofwords xh xl) (
ofwords yh yl) =
ofwords (
Int.or xh yh) (
Int.or xl yl).
Proof.
Lemma decompose_xor:
forall xh xl yh yl,
xor (
ofwords xh xl) (
ofwords yh yl) =
ofwords (
Int.xor xh yh) (
Int.xor xl yl).
Proof.
Lemma decompose_not:
forall xh xl,
not (
ofwords xh xl) =
ofwords (
Int.not xh) (
Int.not xl).
Proof.
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).
Proof.
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.
Proof.
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))).
Proof.
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)).
Proof.
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))).
Proof.
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)).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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)).
Proof.
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).
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
End Int64.
Strategy 0 [
Wordsize_64.wordsize].
Notation int64 :=
Int64.int.
Global Opaque Int.repr Int64.repr Byte.repr.
Specialization to offsets in pointer values
Module Wordsize_Ptrofs.
Definition wordsize :=
if Archi.ptr64 then 64%
nat else 32%
nat.
Remark wordsize_not_zero:
wordsize <> 0%
nat.
Proof.
End Wordsize_Ptrofs.
Strategy opaque [
Wordsize_Ptrofs.wordsize].
Module Ptrofs.
Include Make(
Wordsize_Ptrofs).
Definition to_int (
x:
int):
Int.int :=
Int.repr (
unsigned x).
Definition to_int64 (
x:
int):
Int64.int :=
Int64.repr (
unsigned x).
Definition of_int (
x:
Int.int) :
int :=
repr (
Int.unsigned x).
Definition of_intu :=
of_int.
Definition of_ints (
x:
Int.int) :
int :=
repr (
Int.signed x).
Definition of_int64 (
x:
Int64.int) :
int :=
repr (
Int64.unsigned x).
Definition of_int64u :=
of_int64.
Definition of_int64s (
x:
Int64.int) :
int :=
repr (
Int64.signed x).
Section AGREE32.
Hypothesis _32:
Archi.ptr64 =
false.
Lemma modulus_eq32:
modulus =
Int.modulus.
Proof.
Lemma eqm32:
forall x y,
Int.eqm x y <->
eqm x y.
Proof.
Definition agree32 (
a:
Ptrofs.int) (
b:
Int.int) :
Prop :=
Ptrofs.unsigned a =
Int.unsigned b.
Lemma agree32_repr:
forall i,
agree32 (
Ptrofs.repr i) (
Int.repr i).
Proof.
Lemma agree32_signed:
forall a b,
agree32 a b ->
Ptrofs.signed a =
Int.signed b.
Proof.
Lemma agree32_of_int:
forall b,
agree32 (
of_int b)
b.
Proof.
Lemma agree32_of_ints:
forall b,
agree32 (
of_ints b)
b.
Proof.
Lemma agree32_of_int_eq:
forall a b,
agree32 a b ->
of_int b =
a.
Proof.
Lemma agree32_of_ints_eq:
forall a b,
agree32 a b ->
of_ints b =
a.
Proof.
Lemma agree32_to_int:
forall a,
agree32 a (
to_int a).
Proof.
Lemma agree32_to_int_eq:
forall a b,
agree32 a b ->
to_int a =
b.
Proof.
Lemma agree32_neg:
forall a1 b1,
agree32 a1 b1 ->
agree32 (
Ptrofs.neg a1) (
Int.neg b1).
Proof.
Lemma agree32_add:
forall a1 b1 a2 b2,
agree32 a1 b1 ->
agree32 a2 b2 ->
agree32 (
Ptrofs.add a1 a2) (
Int.add b1 b2).
Proof.
Lemma agree32_sub:
forall a1 b1 a2 b2,
agree32 a1 b1 ->
agree32 a2 b2 ->
agree32 (
Ptrofs.sub a1 a2) (
Int.sub b1 b2).
Proof.
Lemma agree32_mul:
forall a1 b1 a2 b2,
agree32 a1 b1 ->
agree32 a2 b2 ->
agree32 (
Ptrofs.mul a1 a2) (
Int.mul b1 b2).
Proof.
Lemma agree32_divs:
forall a1 b1 a2 b2,
agree32 a1 b1 ->
agree32 a2 b2 ->
agree32 (
Ptrofs.divs a1 a2) (
Int.divs b1 b2).
Proof.
Lemma of_int_to_int:
forall n,
of_int (
to_int n) =
n.
Proof.
End AGREE32.
Section AGREE64.
Hypothesis _64:
Archi.ptr64 =
true.
Lemma modulus_eq64:
modulus =
Int64.modulus.
Proof.
Lemma eqm64:
forall x y,
Int64.eqm x y <->
eqm x y.
Proof.
Definition agree64 (
a:
Ptrofs.int) (
b:
Int64.int) :
Prop :=
Ptrofs.unsigned a =
Int64.unsigned b.
Lemma agree64_repr:
forall i,
agree64 (
Ptrofs.repr i) (
Int64.repr i).
Proof.
Lemma agree64_signed:
forall a b,
agree64 a b ->
Ptrofs.signed a =
Int64.signed b.
Proof.
Lemma agree64_of_int:
forall b,
agree64 (
of_int64 b)
b.
Proof.
Lemma agree64_of_int_eq:
forall a b,
agree64 a b ->
of_int64 b =
a.
Proof.
Lemma agree64_to_int:
forall a,
agree64 a (
to_int64 a).
Proof.
Lemma agree64_to_int_eq:
forall a b,
agree64 a b ->
to_int64 a =
b.
Proof.
Lemma agree64_neg:
forall a1 b1,
agree64 a1 b1 ->
agree64 (
Ptrofs.neg a1) (
Int64.neg b1).
Proof.
Lemma agree64_add:
forall a1 b1 a2 b2,
agree64 a1 b1 ->
agree64 a2 b2 ->
agree64 (
Ptrofs.add a1 a2) (
Int64.add b1 b2).
Proof.
Lemma agree64_sub:
forall a1 b1 a2 b2,
agree64 a1 b1 ->
agree64 a2 b2 ->
agree64 (
Ptrofs.sub a1 a2) (
Int64.sub b1 b2).
Proof.
Lemma agree64_mul:
forall a1 b1 a2 b2,
agree64 a1 b1 ->
agree64 a2 b2 ->
agree64 (
Ptrofs.mul a1 a2) (
Int64.mul b1 b2).
Proof.
Lemma agree64_divs:
forall a1 b1 a2 b2,
agree64 a1 b1 ->
agree64 a2 b2 ->
agree64 (
Ptrofs.divs a1 a2) (
Int64.divs b1 b2).
Proof.
Lemma of_int64_to_int64:
forall n,
of_int64 (
to_int64 n) =
n.
Proof.
End AGREE64.
Hint Resolve
agree32_repr agree32_of_int agree32_of_ints agree32_of_int_eq agree32_of_ints_eq
agree32_to_int agree32_to_int_eq agree32_neg agree32_add agree32_sub agree32_mul agree32_divs
agree64_repr agree64_of_int agree64_of_int_eq
agree64_to_int agree64_to_int_eq agree64_neg agree64_add agree64_sub agree64_mul agree64_divs :
ptrofs.
End Ptrofs.
Strategy 0 [
Wordsize_Ptrofs.wordsize].
Notation ptrofs :=
Ptrofs.int.
Global Opaque Ptrofs.repr.
Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans
Int.eqm_small_eq Int.eqm_add Int.eqm_neg Int.eqm_sub Int.eqm_mult
Int.eqm_unsigned_repr Int.eqm_unsigned_repr_l Int.eqm_unsigned_repr_r
Int.unsigned_range Int.unsigned_range_2
Int.repr_unsigned Int.repr_signed Int.unsigned_repr :
ints.
Hint Resolve Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans
Int64.eqm_small_eq Int64.eqm_add Int64.eqm_neg Int64.eqm_sub Int64.eqm_mult
Int64.eqm_unsigned_repr Int64.eqm_unsigned_repr_l Int64.eqm_unsigned_repr_r
Int64.unsigned_range Int64.unsigned_range_2
Int64.repr_unsigned Int64.repr_signed Int64.unsigned_repr :
ints.
Hint Resolve Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans
Ptrofs.eqm_small_eq Ptrofs.eqm_add Ptrofs.eqm_neg Ptrofs.eqm_sub Ptrofs.eqm_mult
Ptrofs.eqm_unsigned_repr Ptrofs.eqm_unsigned_repr_l Ptrofs.eqm_unsigned_repr_r
Ptrofs.unsigned_range Ptrofs.unsigned_range_2
Ptrofs.repr_unsigned Ptrofs.repr_signed Ptrofs.unsigned_repr :
ints.