Require Import Coqlib.
Require Import Axioms.
Require Import Integers.
Require Import Floats.
Require Import Psatz.
Lemma Forall_app:
forall A P (
l1 l2:
list A),
Forall P l1 ->
Forall P l2 ->
Forall P (
l1 ++
l2).
Proof.
Ltac assert_val val :=
match goal with
|-
context [
if ?
a then _ else _] =>
let x:=
fresh in assert (
x:
a=
val);[|
rewrite x in *;
clear x]
end.
Ltac inv' :=
match goal with
H: ?
a _ = ?
a _ |-
_ =>
inv H;
inv'
|
_ =>
idtac
end.
Ltac destr :=
try destr_cond_match;
simpl in *;
intuition try congruence.
Ltac des t :=
destruct t eqn:?;
subst;
simpl in *;
intuition try congruence.
Ltac destr_no_dep :=
destr;
repeat match goal with
H:
_ =
left _ |-
_ =>
clear H
|
H:
_ =
right _ |-
_ =>
clear H
end.
Lemma shl_zero_l:
forall i,
Int.shl Int.zero i =
Int.zero.
Proof.
Ltac solve_int :=
repeat
match goal with
| |-
context [
Int.shl _ (
Int.repr 0)] =>
rewrite Int.shl_zero
| |-
context [
Int.shl Int.zero _] =>
rewrite shl_zero_l
| |-
context [
Int.add Int.zero _] =>
rewrite Int.add_zero_l
| |-
context [
Int.shru (
Int.shl ?
i (
Int.repr ?
n)) (
Int.repr ?
n)] =>
change n with (
Int.zwordsize - (
Int.zwordsize -
n));
rewrite <-
Int.zero_ext_shru_shl by (
unfold Int.zwordsize;
simpl;
omega)
| |-
context [
Int.shru (
Int.shl ?
i (
Int.repr ?
n)) (
Int.repr ?
m)] =>
change (
Int.shru (
Int.shl i (
Int.repr n)) (
Int.repr m))
with
(
Int.shru (
Int.shl i (
Int.repr (
Int.zwordsize - (
Int.zwordsize -
n)))) (
Int.add (
Int.repr n) (
Int.sub (
Int.repr m) (
Int.repr n))));
rewrite <-
Int.shru_shru by (
vm_compute;
auto);
rewrite <-
Int.zero_ext_shru_shl by (
unfold Int.zwordsize;
simpl;
omega)
| |-
context [
Int.sub (
Int.repr ?
i) (
Int.repr ?
j)] =>
change (
Int.sub (
Int.repr i) (
Int.repr j))
with (
Int.repr (
i -
j));
simpl
| |-
context [
Int.add (
Int.repr ?
i) (
Int.repr ?
j)] =>
change (
Int.add (
Int.repr i) (
Int.repr j))
with (
Int.repr (
i +
j));
simpl
| |-
context [
Int.testbit (
Int.add _ _)
_] =>
rewrite Int.add_is_or;
simpl;
auto;
try omega
| |-
context [
Int.testbit (
Int.and _ _)
_] =>
rewrite Int.bits_and;
simpl;
auto
| |-
context [
Int.testbit (
Int.or _ _)
_] =>
rewrite Int.bits_or;
simpl;
auto;
try omega; [
idtac]
| |-
context [
Int.testbit (
Int.shl _ _)
_] =>
rewrite Int.bits_shl;
simpl;
auto;
try omega; [
idtac]
| |-
context [
Int.testbit (
Int.shru _ _)
_] =>
rewrite Int.bits_shru;
simpl;
auto;
try omega; [
idtac]
| |-
context [
Int.testbit (
Int.zero_ext _ _)
_] =>
rewrite Int.bits_zero_ext;
simpl
| |-
context [
Int.testbit (
Int.sign_ext _ _)
_] =>
f_equal;
apply Int.sign_ext_equal_if_zero_equal;
try omega
|
H:
context[
Int.unsigned (
Int.repr _)]|-
_ =>
rewrite Int.unsigned_repr in H by (
unfold Int.max_unsigned;
simpl;
omega)
| |-
context[
Int.unsigned (
Int.repr _)] =>
rewrite Int.unsigned_repr by (
unfold Int.max_unsigned;
simpl;
omega)
| |-
context [
_ ||
false] =>
rewrite orb_false_r
| |-
context [
_ &&
false] =>
rewrite andb_false_r
| |-
context [
Int.testbit Int.zero ?
i] =>
rewrite Int.bits_zero
| |-
context [?
n - ?
i + ?
i] =>
replace (
n -
i +
i)
with n by (
rewrite Z.sub_simpl_r;
auto)
| |-
Int.testbit ?
e ?
i =
Int.testbit ?
e ?
j =>
f_equal;
omega
| |- @
eq int _ _ =>
apply Int.same_bits_eq;
simpl;
intros
| |-
_ =>
destr;
repeat match goal with
|
H:
_ =
left _ |-
_ =>
clear H
|
H:
_ =
right _ |-
_ =>
clear H
end;
try omega
| |-
_ =>
progress simpl
end.
Lemma shl_zero_r_64:
forall i,
Int64.shl'
i (
Int.repr 0) =
i.
Proof.
Lemma shl_zero_l_64:
forall i,
Int64.shl'
Int64.zero i =
Int64.zero.
Proof.
Lemma shru'
_shru:
forall l i,
0 <=
Int.unsigned i <= 64 ->
Int64.shru'
l i =
Int64.shru l (
Int64.repr (
Int.unsigned i)).
Proof.
Lemma shl'
_shl:
forall l i,
0 <=
Int.unsigned i <= 64 ->
Int64.shl'
l i =
Int64.shl l (
Int64.repr (
Int.unsigned i)).
Proof.
Ltac solve_long :=
repeat
match goal with
| |-
context [
Int64.shl'
_ (
Int.repr 0)] =>
rewrite shl_zero_r_64
| |-
context [
Int64.shl'
Int64.zero _] =>
rewrite shl_zero_l_64
| |-
context [
Int64.add Int64.zero _] =>
rewrite Int64.add_zero_l
| |-
context [
Int64.mul Int64.zero _] =>
rewrite Int64.mul_commut;
rewrite Int64.mul_zero
| |-
context [
Int64.shru (
Int64.shl ?
i (
Int64.repr ?
n)) (
Int64.repr ?
n)] =>
change n with (
Int64.zwordsize - (
Int64.zwordsize -
n));
rewrite <-
Int64.zero_ext_shru_shl by (
unfold Int64.zwordsize;
simpl;
omega)
| |-
context [
Int64.shru (
Int64.shl ?
i (
Int64.repr ?
n)) (
Int64.repr ?
m)] =>
change (
Int64.shru (
Int64.shl i (
Int64.repr n)) (
Int64.repr m))
with
(
Int64.shru (
Int64.shl i (
Int64.repr (
Int64.zwordsize - (
Int64.zwordsize -
n)))) (
Int64.add (
Int64.repr n) (
Int64.sub (
Int64.repr m) (
Int64.repr n))));
rewrite <-
Int64.shru_shru by (
vm_compute;
auto);
rewrite <-
Int64.zero_ext_shru_shl by (
unfold Int64.zwordsize;
simpl;
omega)
| |-
context [
Int64.sub (
Int64.repr ?
i) (
Int64.repr ?
j)] =>
change (
Int64.sub (
Int64.repr i) (
Int64.repr j))
with (
Int64.repr (
i -
j));
simpl
| |-
context [
Int64.add (
Int64.repr ?
i) (
Int64.repr ?
j)] =>
change (
Int64.add (
Int64.repr i) (
Int64.repr j))
with (
Int64.repr (
i +
j));
simpl
| |-
context [
Int64.testbit (
Int64.and _ _)
_] =>
rewrite Int64.bits_and;
simpl;
auto
| |-
context [
Int64.testbit (
Int64.or _ _)
_] =>
rewrite Int64.bits_or;
simpl;
auto;
try omega; [
idtac]
| |-
context [
Int64.testbit (
Int64.shl _ _)
_] =>
rewrite Int64.bits_shl;
simpl;
auto;
try omega; [
idtac]
| |-
context [
Int64.testbit (
Int64.shru _ _)
_] =>
rewrite Int64.bits_shru;
simpl;
auto;
try omega; [
idtac]
| |-
context [
Int64.testbit (
Int64.zero_ext _ _)
_] =>
rewrite Int64.bits_zero_ext;
simpl
| |-
context [
Int64.testbit (
Int64.sign_ext _ _)
_] =>
f_equal;
apply Int64.sign_ext_equal_if_zero_equal;
try omega; [
idtac]
|
H:
context[
Int64.unsigned (
Int64.repr _)]|-
_ =>
rewrite Int64.unsigned_repr in H by (
unfold Int64.max_unsigned;
simpl;
omega)
| |-
context[
Int64.unsigned (
Int64.repr _)] =>
rewrite Int64.unsigned_repr by (
unfold Int64.max_unsigned;
simpl;
omega)
|
H:
context[
Int.unsigned (
Int.repr _)]|-
_ =>
rewrite Int.unsigned_repr in H by (
unfold Int.max_unsigned;
simpl;
omega)
| |-
context[
Int.unsigned (
Int.repr _)] =>
rewrite Int.unsigned_repr by (
unfold Int.max_unsigned;
simpl;
omega)
| |-
context [
_ ||
false] =>
rewrite orb_false_r
| |-
context [
_ &&
false] =>
rewrite andb_false_r
| |-
context [
Int64.testbit Int64.zero ?
i] =>
rewrite Int64.bits_zero
| |-
context [?
n - ?
i + ?
i] =>
replace (
n -
i +
i)
with n by (
rewrite Z.sub_simpl_r;
auto)
| |-
Int64.testbit ?
e ?
i =
Int64.testbit ?
e ?
j =>
f_equal;
omega
| |- @
eq int64 _ _ =>
apply Int64.same_bits_eq;
simpl;
intros
| |-
_ =>
destr;
repeat match goal with
|
H:
_ =
left _ |-
_ =>
clear H
|
H:
_ =
right _ |-
_ =>
clear H
end;
try omega
| |-
_ =>
progress simpl
end.
Lemma add_is_or_8:
forall i i0,
Int.add (
Int.shl i0 (
Int.repr 8)) (
Int.zero_ext 8
i) =
Int.or (
Int.shl i0 (
Int.repr 8)) (
Int.zero_ext 8
i).
Proof.
Lemma add_is_or_16:
forall i i0,
Int.add (
Int.shl i0 (
Int.repr 8)) (
Int.shru (
Int.zero_ext 16
i) (
Int.repr 8)) =
Int.or (
Int.shl i0 (
Int.repr 8)) (
Int.shru (
Int.zero_ext 16
i) (
Int.repr 8)).
Proof.
Lemma add_is_or_24:
forall i,
Int.add
(
Int.shl (
Int.shru i (
Int.repr 24))
(
Int.repr 8)) (
Int.shru (
Int.zero_ext 24
i) (
Int.repr 16)) =
Int.or
(
Int.shl (
Int.shru i (
Int.repr 24))
(
Int.repr 8)) (
Int.shru (
Int.zero_ext 24
i) (
Int.repr 16)).
Proof.
Lemma float_bits_of_double_inj:
forall f f',
Float.to_bits f =
Float.to_bits f' ->
f =
f'.
Proof.
Lemma float_bits_of_single_inj:
forall f f',
Float32.to_bits f =
Float32.to_bits f' ->
f =
f'.
Proof.
Lemma Forall_rev:
forall A P (
l:
list A),
Forall P (
rev l) ->
Forall P l.
Proof.
Lemma proof_irr_int64:
forall (
i i0:
int64),
match i with
Int64.mkint int64val _ =>
int64val
end =
match i0 with
Int64.mkint int64val _ =>
int64val
end ->
i =
i0.
Proof.
intros;
destruct i;
destruct i0;
subst.
f_equal.
apply proof_irr.
Qed.
Lemma proof_irr_int:
forall (
i i0:
int),
match i with
Int.mkint intval _ =>
intval
end =
match i0 with
Int.mkint intval _ =>
intval
end ->
i =
i0.
Proof.
intros;
destruct i;
destruct i0;
subst.
f_equal.
apply proof_irr.
Qed.
Lemma int_zwordsize:
Int.zwordsize = 32.
Proof.
reflexivity.
Qed.
Lemma int64_zwordsize:
Int64.zwordsize = 64.
Proof.
reflexivity.
Qed.
Lemma byte_zwordsize:
Byte.zwordsize = 8.
Proof.
reflexivity. Qed.
Lemma zero_ext_16_undef:
forall i i0,
(
Int.add
(
Int.shl
(
Int.add (
Int.shl Int.zero (
Int.repr 8))
(
Int.shru (
Int.shl i (
Int.repr 16)) (
Int.repr 24)))
(
Int.repr 8)) (
Int.shru (
Int.shl i0 (
Int.repr 24)) (
Int.repr 24))) =
(
Int.zero_ext 16
(
Int.add
(
Int.shl
(
Int.add (
Int.shl Int.zero (
Int.repr 8))
(
Int.shru (
Int.shl i (
Int.repr 16)) (
Int.repr 24)))
(
Int.repr 8))
(
Int.shru (
Int.shl i0 (
Int.repr 24)) (
Int.repr 24)))).
Proof.
intros.
solve_int.
Qed.
Lemma zero_ext_16_add_shl_shru:
forall i0,
Int.add
(
Int.shl
(
Int.add (
Int.shl Int.zero (
Int.repr 8))
(
Int.shru (
Int.shl i0 (
Int.repr 16)) (
Int.repr 24)))
(
Int.repr 8)) (
Int.shru (
Int.shl i0 (
Int.repr 24)) (
Int.repr 24)) =
Int.zero_ext 16
i0.
Proof.
intros.
solve_int.
Qed.
Lemma list_forall2_sym:
forall {
A} (
P:
A ->
A ->
Prop)
(
Psym:
forall a b,
P a b ->
P b a)
la lb,
list_forall2 P la lb ->
list_forall2 P lb la.
Proof.
intros.
induction H.
constructor.
constructor; auto.
Qed.
Lemma list_forall2_rev:
forall {
A} (
P:
A ->
A ->
Prop) (
l l':
list A),
list_forall2 P l l' ->
list_forall2 P (
rev l) (
rev l').
Proof.
induction l;
intros.
-
inv H.
simpl;
constructor.
-
simpl.
inv H.
apply IHl in H4.
simpl.
apply list_forall2_app;
auto.
constructor;
auto.
constructor.
Qed.
Lemma list_forall2_rev':
forall {
A} (
P:
A ->
A ->
Prop)
l1 l2,
list_forall2 P (
rev l1) (
rev l2) ->
list_forall2 P l1 l2.
Proof.
Lemma bits_255_below:
forall i0, 0 <=
i0 < 8 ->
Int.testbit (
Int.repr 255)
i0 =
true.
Proof.
Lemma bits_255_above:
forall i0, 8 <=
i0 <
Int.zwordsize ->
Int.testbit (
Int.repr 255)
i0 =
false.
Proof.
Lemma bits64_255_below:
forall i0, 0 <=
i0 < 8 ->
Int64.testbit (
Int64.repr 255)
i0 =
true.
Proof.
Lemma bits64_255_above:
forall i0, 8 <=
i0 <
Int64.zwordsize ->
Int64.testbit (
Int64.repr 255)
i0 =
false.
Proof.
Lemma sign_ext_8_id:
forall i0,
(
Int.sign_ext 8
(
Int.add (
Int.and i0 (
Int.repr 255)) (
Int.shl Int.zero (
Int.repr 8)))) =
(
Int.sign_ext 8
i0).
Proof.
Lemma zero_ext_8_id:
forall i0,
(
Int.zero_ext 8
(
Int.add (
Int.and i0 (
Int.repr 255)) (
Int.shl Int.zero (
Int.repr 8)))) =
(
Int.zero_ext 8
i0).
Proof.
Lemma sign_ext_16_id:
forall i0,
(
Int.sign_ext 16
(
Int.add (
Int.and i0 (
Int.repr 255))
(
Int.shl
(
Int.add (
Int.and (
Int.shru i0 (
Int.repr 8)) (
Int.repr 255))
(
Int.shl Int.zero (
Int.repr 8))) (
Int.repr 8)))) =
(
Int.sign_ext 16
i0).
Proof.
Lemma zero_ext_16_id:
forall i0,
(
Int.zero_ext 16
(
Int.add (
Int.and i0 (
Int.repr 255))
(
Int.shl
(
Int.add (
Int.and (
Int.shru i0 (
Int.repr 8)) (
Int.repr 255))
(
Int.shl Int.zero (
Int.repr 8))) (
Int.repr 8)))) =
(
Int.zero_ext 16
i0).
Proof.
Lemma add_and_shl_rew:
forall i i'
j,
0 <=
j <
Int64.zwordsize ->
Int64.testbit
(
Int64.add (
Int64.and i (
Int64.repr 255)) (
Int64.shl i' (
Int64.repr 8)))
j =
if zlt j 8
then Int64.testbit i j
else Int64.testbit i' (
j - 8 ).
Proof.
Lemma add_and_shl_rew_32:
forall i i'
j,
0 <=
j <
Int.zwordsize ->
Int.testbit
(
Int.add (
Int.and i (
Int.repr 255)) (
Int.shl i' (
Int.repr 8)))
j =
if zlt j 8
then Int.testbit i j
else Int.testbit i' (
j - 8 ).
Proof.
Lemma int_decomp:
forall i0,
Int.add (
Int.and i0 (
Int.repr 255))
(
Int.shl
(
Int.add (
Int.and (
Int.shru i0 (
Int.repr 8)) (
Int.repr 255))
(
Int.shl
(
Int.add
(
Int.and
(
Int.shru (
Int.shru i0 (
Int.repr 8)) (
Int.repr 8))
(
Int.repr 255))
(
Int.shl
(
Int.add
(
Int.and
(
Int.shru
(
Int.shru (
Int.shru i0 (
Int.repr 8))
(
Int.repr 8)) (
Int.repr 8))
(
Int.repr 255)) (
Int.shl Int.zero (
Int.repr 8)))
(
Int.repr 8))) (
Int.repr 8)))
(
Int.repr 8)) =
i0.
Proof.
Lemma int64_decomp:
forall i0,
Int64.add (
Int64.and i0 (
Int64.repr 255))
(
Int64.shl
(
Int64.add
(
Int64.and (
Int64.shru i0 (
Int64.repr 8)) (
Int64.repr 255))
(
Int64.shl
(
Int64.add
(
Int64.and (
Int64.shru i0 (
Int64.repr 16)) (
Int64.repr 255))
(
Int64.shl
(
Int64.add
(
Int64.and (
Int64.shru i0 (
Int64.repr 24))
(
Int64.repr 255))
(
Int64.shl
(
Int64.add
(
Int64.and (
Int64.shru i0 (
Int64.repr 32))
(
Int64.repr 255))
(
Int64.shl
(
Int64.add
(
Int64.and (
Int64.shru i0 (
Int64.repr 40))
(
Int64.repr 255))
(
Int64.shl
(
Int64.add
(
Int64.and
(
Int64.shru i0 (
Int64.repr 48))
(
Int64.repr 255))
(
Int64.shl
(
Int64.add
(
Int64.and
(
Int64.shru i0
(
Int64.repr 56))
(
Int64.repr 255))
(
Int64.shl Int64.zero
(
Int64.repr 8)))
(
Int64.repr 8)))
(
Int64.repr 8)))
(
Int64.repr 8))) (
Int64.repr 8)))
(
Int64.repr 8))) (
Int64.repr 8)))
(
Int64.repr 8)) =
i0.
Proof.
Lemma loword_add_byte:
forall z i2,
0 <=
z <
Byte.modulus ->
Int.add (
Int.repr z)
(
Int.shl (
Int64.loword i2) (
Int.repr 8)) =
Int64.loword
(
Int64.add (
Int64.repr z)
(
Int64.shl'
i2 (
Int.repr 8))).
Proof.
Lemma int64_sign_ext_of_words:
forall i1 i2,
Int64.sign_ext 64 (
Int64.ofwords i1 i2) =
Int64.ofwords (
Int.sign_ext 32
i1) (
Int.sign_ext 32
i2).
Proof.
Lemma aux_encode_2:
forall i i1,
i + 8 <
Int.zwordsize ->
0 <=
i <
Int.zwordsize ->
Int.testbit (
Int.repr (
Byte.unsigned (
Byte.repr (
Int.unsigned i1 / 256))))
i =
Int.testbit i1 (
i + 8) &&
Int.testbit (
Int.repr 255)
i.
Proof.
Lemma aux_encode_1:
forall i i0,
0 <=
i <
Int.zwordsize ->
Int.testbit (
Int.repr (
Byte.unsigned (
Byte.repr (
Int.unsigned i0))))
i =
Int.testbit i0 i &&
Int.testbit (
Int.repr 255)
i.
Proof.
Lemma aux_encode_3:
forall i i0,
0 <=
i <
Int.zwordsize ->
i + 8 + 8 <
Int.zwordsize ->
Int.testbit
(
Int.repr (
Byte.unsigned (
Byte.repr (
Int.unsigned i0 / 256 / 256))))
i =
Int.testbit i0 (
i + 8 + 8) &&
Int.testbit (
Int.repr 255)
i.
Proof.
Lemma aux_encode_4:
forall i i1,
0 <=
i ->
i + 8 + 8 + 8 <
Int.zwordsize ->
Int.testbit
(
Int.repr
(
Byte.unsigned (
Byte.repr (
Int.unsigned i1 / 256 / 256 / 256))))
i =
Int.testbit i1 (
i + 8 + 8 + 8) &&
Int.testbit (
Int.repr 255)
i.
Proof.
Lemma aux_encode_above_general:
forall i i1,
0 <=
i <
Int.zwordsize ->
i >= 8 ->
Int.testbit
(
Int.repr
(
Byte.unsigned (
Byte.repr i1)))
i =
false.
Proof.
Lemma int64_byte_and_255:
forall i,
Int64.repr (
Byte.unsigned (
Byte.repr (
Int.unsigned i))) =
Int64.repr (
Int.unsigned (
Int.and i (
Int.repr 255))).
Proof.
Lemma int64_byte_and_255':
forall i,
Int64.repr (
Byte.unsigned (
Byte.repr (
Int64.unsigned i))) =
Int64.and i (
Int64.repr 255).
Proof.
Lemma int_byte_and_255:
forall i,
Int.repr (
Byte.unsigned (
Byte.repr (
Int64.unsigned i))) =
Int.repr (
Int64.unsigned (
Int64.and i (
Int64.repr 255))).
Proof.
Lemma int64_div256:
forall i1,
Int64.repr (
Byte.unsigned (
Byte.repr (
Int.unsigned i1 / 256))) =
Int64.repr
(
Int.unsigned (
Int.and (
Int.shru i1 (
Int.repr 8)) (
Int.repr 255))).
Proof.
Lemma int64_div256_2:
forall i1,
Int64.repr (
Byte.unsigned (
Byte.repr (
Int.unsigned i1 / 256 / 256))) =
Int64.repr
(
Int.unsigned (
Int.and (
Int.shru (
Int.shru i1 (
Int.repr 8)) (
Int.repr 8)) (
Int.repr 255))).
Proof.
Lemma int64_div256_3:
forall i1,
Int64.repr (
Byte.unsigned (
Byte.repr (
Int.unsigned i1 / 256 / 256 / 256))) =
Int64.repr
(
Int.unsigned
(
Int.and
(
Int.shru (
Int.shru (
Int.shru i1 (
Int.repr 8)) (
Int.repr 8))
(
Int.repr 8)) (
Int.repr 255))).
Proof.
Lemma int_byte_and_255':
forall i,
Int.repr (
Byte.unsigned (
Byte.repr (
Int.unsigned i))) =
Int.and i (
Int.repr 255).
Proof.
Lemma zshiftr_unsigned_repr:
forall i0 n,
1 <=
n ->
Int64.unsigned (
Int64.repr (
Z.shiftr (
Int64.unsigned i0)
n)) =
Z.shiftr (
Int64.unsigned i0)
n.
Proof.
Lemma leq_ieq:
forall i i0,
Int64.repr (
Int.unsigned i) =
Int64.repr (
Int.unsigned i0) ->
i =
i0.
Proof.
Lemma ofbi_ieq:
forall i i0,
Float32.of_bits i =
Float32.of_bits i0 ->
i =
i0.
Proof.
Lemma byte_wordsize:
Byte.wordsize = 8%
nat.
Proof.
vm_compute; auto. Qed.
Lemma int64_wordsize:
Int64.wordsize = 64%
nat.
Proof.
vm_compute; auto. Qed.
Lemma twop_nat_8:
two_power_nat 8 = 256.
Proof.
vm_compute; auto. Qed.
Lemma twop_nat_64:
two_power_nat 64 = 18446744073709551616.
Proof.
vm_compute; auto. Qed.
Lemma int64_decomp':
forall i,
(
Int64.add
(
Int64.repr
(
Int.unsigned (
Int64.loword (
Int64.and i (
Int64.repr 255)))))
(
Int64.shl
(
Int64.add
(
Int64.repr
(
Int.unsigned
(
Int64.loword
(
Int64.and (
Int64.shru i (
Int64.repr 8))
(
Int64.repr 255)))))
(
Int64.shl
(
Int64.add
(
Int64.repr
(
Int.unsigned
(
Int64.loword
(
Int64.and (
Int64.shru i (
Int64.repr 16))
(
Int64.repr 255)))))
(
Int64.shl
(
Int64.add
(
Int64.repr
(
Int.unsigned
(
Int64.loword
(
Int64.and
(
Int64.shru i (
Int64.repr 24))
(
Int64.repr 255)))))
(
Int64.shl
(
Int64.add
(
Int64.repr
(
Int.unsigned
(
Int64.loword
(
Int64.and
(
Int64.shru i (
Int64.repr 32))
(
Int64.repr 255)))))
(
Int64.shl
(
Int64.add
(
Int64.repr
(
Int.unsigned
(
Int64.loword
(
Int64.and
(
Int64.shru i
(
Int64.repr 40))
(
Int64.repr 255)))))
(
Int64.shl
(
Int64.add
(
Int64.repr
(
Int.unsigned
(
Int64.loword
(
Int64.and
(
Int64.shru i
(
Int64.repr 48))
(
Int64.repr 255)))))
(
Int64.shl
(
Int64.add
(
Int64.repr
(
Int.unsigned
(
Int64.loword
(
Int64.and
(
Int64.shru i
(
Int64.repr 56))
(
Int64.repr 255)))))
(
Int64.shl Int64.zero
(
Int64.repr
(
Int.unsigned (
Int.repr 8)))))
(
Int64.repr
(
Int.unsigned (
Int.repr 8)))))
(
Int64.repr
(
Int.unsigned (
Int.repr 8)))))
(
Int64.repr (
Int.unsigned (
Int.repr 8)))))
(
Int64.repr (
Int.unsigned (
Int.repr 8)))))
(
Int64.repr (
Int.unsigned (
Int.repr 8)))))
(
Int64.repr (
Int.unsigned (
Int.repr 8)))))
(
Int64.repr (
Int.unsigned (
Int.repr 8))))) =
i.
Proof.
Lemma Int64_add_is_or_lt_256:
forall j j1,
Int64.unsigned j < 256 ->
Int64.add j (
Int64.shl'
j1 (
Int.repr 8)) =
Int64.or j (
Int64.shl'
j1 (
Int.repr 8)).
Proof.
Lemma int64_testbit_above_8:
forall i i3,
Int64.unsigned i < 256 ->
i3 >= 8 ->
Int64.testbit i i3 =
false.
Proof.
Lemma int64_testbit_lt_256:
forall i i3,
Int64.unsigned i < 256 ->
Int64.testbit i i3 =
if zlt i3 8
then Int64.testbit i i3 else false.
Proof.
Lemma int_testbit_above_8:
forall i i3,
Int.unsigned i < 256 ->
i3 >= 8 ->
Int.testbit i i3 =
false.
Proof.
Lemma int_testbit_lt_256:
forall i i3,
Int.unsigned i < 256 ->
Int.testbit i i3 =
if zlt i3 8
then Int.testbit i i3 else false.
Proof.
Lemma int64_testbit_lt_256_7:
forall i i3,
Int64.unsigned i < 256 ^ 7->
Int64.testbit i i3 =
if zlt (
i3 + 8)
Int64.zwordsize then Int64.testbit i i3 else false.
Proof.
Lemma add_byte_shl_eq_byte:
forall i0 i i1 i2,
Int.add (
Int.repr (
Byte.unsigned i0)) (
Int.shl i1 (
Int.repr 8)) =
Int.add (
Int.repr (
Byte.unsigned i)) (
Int.shl i2 (
Int.repr 8)) ->
Byte.unsigned i0 =
Byte.unsigned i.
Proof.
Lemma add_byte_shl_eq_byte_64:
forall i0 i i1 i2,
Int64.add (
Int64.repr (
Byte.unsigned i0)) (
Int64.shl i1 (
Int64.repr 8)) =
Int64.add (
Int64.repr (
Byte.unsigned i)) (
Int64.shl i2 (
Int64.repr 8)) ->
Byte.unsigned i0 =
Byte.unsigned i.
Proof.