diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index b18ae914d518c4183c59ecc3134d030d5715a9a8..077641365cca1b8a96e1151791c9c6924fbd5fd5 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -1089,10 +1089,10 @@ Proof.
simpl in H1. destruct (ms m0); try discriminate.
exists i0; split; auto. destruct (Int.ltu i (Int.repr 31)); discriminate || auto.
destruct H3 as [n [ARG1 LTU]].
- assert (LTU': Int.ltu i (Int.repr 32) = true).
+ assert (LTU': Int.ltu i Int.iwordsize = true).
exploit Int.ltu_inv. eexact LTU. intro.
unfold Int.ltu. apply zlt_true.
- assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto.
+ assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto.
omega.
assert (RSm0: rs (ireg_of m0) = Vint n).
rewrite <- ARG1. symmetry. eapply ireg_val; eauto.
diff --git a/arm/ConstpropOp.v b/arm/ConstpropOp.v
index b5e5a03ba2609d76dff2469321041628ae97584b..e55c7f99e718a0838796cea59b8c7783cc3f98af 100644
--- a/arm/ConstpropOp.v
+++ b/arm/ConstpropOp.v
@@ -174,9 +174,9 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
| Obicshift s, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not (eval_shift s n2)))
| Onot, I n1 :: nil => I(Int.not n1)
| Onotshift s, I n1 :: nil => I(Int.not (eval_shift s n1))
- | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown
- | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown
- | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown
+ | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
+ | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
+ | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
| Oshift s, I n1 :: nil => I(eval_shift s n1)
| Onegf, F n1 :: nil => F(Float.neg n1)
| Oabsf, F n1 :: nil => F(Float.abs n1)
@@ -543,11 +543,11 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
| eval_static_operation_case36 s n1 =>
I(Int.not (eval_shift s n1))
| eval_static_operation_case37 n1 n2 =>
- if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown
+ if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
| eval_static_operation_case38 n1 n2 =>
- if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown
+ if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
| eval_static_operation_case39 n1 n2 =>
- if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown
+ if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
| eval_static_operation_case40 s n1 =>
I(eval_shift s n1)
| eval_static_operation_case41 n1 =>
@@ -954,7 +954,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
| op_strength_reduction_case16 r1 r2 => (* Oshl *)
match intval r2 with
| Some n =>
- if Int.ltu n (Int.repr 32)
+ if Int.ltu n Int.iwordsize
then make_shlimm n r1
else (op, args)
| _ => (op, args)
@@ -962,7 +962,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
| op_strength_reduction_case17 r1 r2 => (* Oshr *)
match intval r2 with
| Some n =>
- if Int.ltu n (Int.repr 32)
+ if Int.ltu n Int.iwordsize
then make_shrimm n r1
else (op, args)
| _ => (op, args)
@@ -970,7 +970,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
| op_strength_reduction_case18 r1 r2 => (* Oshru *)
match intval r2 with
| Some n =>
- if Int.ltu n (Int.repr 32)
+ if Int.ltu n Int.iwordsize
then make_shruimm n r1
else (op, args)
| _ => (op, args)
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index bb9caffb8f394b1ae5fa95335a982af5b5c6b2e5..b718fc26d62985b6391fa126b7bc88cb8f93030c 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -130,13 +130,13 @@ Proof.
replace n2 with i0. destruct (Int.eq i0 Int.zero).
discriminate. injection H0; intro; subst v. simpl. congruence. congruence.
- replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)).
+ replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v. simpl. congruence. discriminate. congruence.
- replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)).
+ replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v. simpl. congruence. discriminate. congruence.
- replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)).
+ replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v. simpl. congruence. discriminate. congruence.
rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence.
@@ -284,7 +284,7 @@ Proof.
with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)).
apply make_shlimm_correct.
simpl. generalize (Int.is_power2_range _ _ H2).
- change (Z_of_nat wordsize) with 32. intro. rewrite H3.
+ change (Z_of_nat Int.wordsize) with 32. intro. rewrite H3.
destruct rs#r; auto. rewrite (Int.mul_pow2 i0 _ _ H2). auto.
simpl List.map. rewrite H. auto.
Qed.
@@ -400,7 +400,7 @@ Proof.
with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)).
apply make_shruimm_correct.
simpl. destruct rs#r1; auto.
- change 32 with (Z_of_nat wordsize).
+ change 32 with (Z_of_nat Int.wordsize).
rewrite (Int.is_power2_range _ _ H0).
generalize (Int.eq_spec i Int.zero); case (Int.eq i Int.zero); intros.
subst i. discriminate.
@@ -474,19 +474,19 @@ Proof.
assumption.
(* Oshl *)
caseEq (intval app r2); intros.
- caseEq (Int.ltu i (Int.repr 32)); intros.
+ caseEq (Int.ltu i Int.iwordsize); intros.
rewrite (intval_correct _ _ H). apply make_shlimm_correct.
assumption.
assumption.
(* Oshr *)
caseEq (intval app r2); intros.
- caseEq (Int.ltu i (Int.repr 32)); intros.
+ caseEq (Int.ltu i Int.iwordsize); intros.
rewrite (intval_correct _ _ H). apply make_shrimm_correct.
assumption.
assumption.
(* Oshru *)
caseEq (intval app r2); intros.
- caseEq (Int.ltu i (Int.repr 32)); intros.
+ caseEq (Int.ltu i Int.iwordsize); intros.
rewrite (intval_correct _ _ H). apply make_shruimm_correct.
assumption.
assumption.
diff --git a/arm/Op.v b/arm/Op.v
index 47cbc0cea7b4772975e088ba8b130f59135a957e..da9903bdcffd1767a95a7991a1781ec657e64b32 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -37,7 +37,7 @@ Set Implicit Arguments.
Record shift_amount : Type :=
mk_shift_amount {
s_amount: int;
- s_amount_ltu: Int.ltu s_amount (Int.repr 32) = true
+ s_amount_ltu: Int.ltu s_amount Int.iwordsize = true
}.
Inductive shift : Type :=
@@ -267,11 +267,11 @@ Definition eval_operation
| Onot, Vint n1 :: nil => Some (Vint (Int.not n1))
| Onotshift s, Vint n1 :: nil => Some (Vint (Int.not (eval_shift s n1)))
| Oshl, Vint n1 :: Vint n2 :: nil =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None
| Oshr, Vint n1 :: Vint n2 :: nil =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
| Oshru, Vint n1 :: Vint n2 :: nil =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
| Oshift s, Vint n :: nil => Some (Vint (eval_shift s n))
| Oshrximm n, Vint n1 :: nil =>
if Int.ltu n (Int.repr 31) then Some (Vint (Int.shrx n1 n)) else None
@@ -548,11 +548,11 @@ Proof.
injection H0; intro; subst v; exact I.
destruct (Int.eq i0 Int.zero). discriminate.
injection H0; intro; subst v; exact I.
- destruct (Int.ltu i0 (Int.repr 32)).
+ destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v; exact I. discriminate.
- destruct (Int.ltu i0 (Int.repr 32)).
+ destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v; exact I. discriminate.
- destruct (Int.ltu i0 (Int.repr 32)).
+ destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v; exact I. discriminate.
destruct (Int.ltu i (Int.repr 31)).
injection H0; intro; subst v; exact I. discriminate.
@@ -724,12 +724,12 @@ Proof.
unfold eq_block in H. destruct (zeq b b0); congruence.
destruct (Int.eq i0 Int.zero); congruence.
destruct (Int.eq i0 Int.zero); congruence.
- destruct (Int.ltu i0 (Int.repr 32)); congruence.
- destruct (Int.ltu i0 (Int.repr 32)); congruence.
- destruct (Int.ltu i0 (Int.repr 32)); congruence.
+ destruct (Int.ltu i0 Int.iwordsize); congruence.
+ destruct (Int.ltu i0 Int.iwordsize); congruence.
+ destruct (Int.ltu i0 Int.iwordsize); congruence.
unfold Int.ltu in H. destruct (zlt (Int.unsigned i) (Int.unsigned (Int.repr 31))).
unfold Int.ltu. rewrite zlt_true. congruence.
- assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto.
+ assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto.
omega. discriminate.
caseEq (eval_condition c vl); intros; rewrite H0 in H.
replace v with (Val.of_bool b).
@@ -825,11 +825,11 @@ Proof.
destruct (eq_block b b0); inv H0. TrivialExists.
destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
- destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists.
- destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists.
- destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists.
- destruct (Int.ltu i0 (Int.repr 32)); inv H1; TrivialExists.
- destruct (Int.ltu i0 (Int.repr 32)); inv H1; TrivialExists.
+ destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
+ destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
+ destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
+ destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
+ destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
destruct (Int.ltu i (Int.repr 31)); inv H0; TrivialExists.
exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
caseEq (eval_condition c vl1); intros. rewrite H1 in H0.
@@ -853,10 +853,10 @@ End EVAL_LESSDEF.
(** Recognition of integers that are valid shift amounts. *)
Definition is_shift_amount_aux (n: int) :
- { Int.ltu n (Int.repr 32) = true } +
- { Int.ltu n (Int.repr 32) = false }.
+ { Int.ltu n Int.iwordsize = true } +
+ { Int.ltu n Int.iwordsize = false }.
Proof.
- intro. case (Int.ltu n (Int.repr 32)). left; auto. right; auto.
+ intro. case (Int.ltu n Int.iwordsize). left; auto. right; auto.
Defined.
Definition is_shift_amount (n: int) : option shift_amount :=
@@ -875,7 +875,7 @@ Proof.
Qed.
Lemma is_shift_amount_None:
- forall n, is_shift_amount n = None -> Int.ltu n (Int.repr 32) = true -> False.
+ forall n, is_shift_amount n = None -> Int.ltu n Int.iwordsize = true -> False.
Proof.
intro n. unfold is_shift_amount.
destruct (is_shift_amount_aux n).
diff --git a/arm/SelectOp.v b/arm/SelectOp.v
index 4b5fde7ff9f65593bfc651ef68b3922a1614577e..abf39aff72474a79e2c57b449badca165664592d 100644
--- a/arm/SelectOp.v
+++ b/arm/SelectOp.v
@@ -385,7 +385,7 @@ Definition shlimm (e1: expr) :=
if Int.eq n Int.zero then e1 else
match e1 with
| Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n))
- | Eop (Oshift (Olsl n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsl (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsl n)) (e1:::Enil)
+ | Eop (Oshift (Olsl n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Olsl (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsl n)) (e1:::Enil)
| _ => Eop (Oshift (Olsl n)) (e1:::Enil)
end.
*)
@@ -436,7 +436,7 @@ Definition shruimm (e1: expr) :=
if Int.eq n Int.zero then e1 else
match e1 with
| Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n))
- | Eop (Oshift (Olsr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsr n)) (e1:::Enil)
+ | Eop (Oshift (Olsr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Olsr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsr n)) (e1:::Enil)
| _ => Eop (Oshift (Olsr n)) (e1:::Enil)
end.
*)
@@ -486,7 +486,7 @@ Definition shruimm (e1: expr) (n: int) :=
Definition shrimm (e1: expr) :=
match e1 with
| Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n))
- | Eop (Oshift (Oasr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Oasr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Oasr n)) (e1:::Enil)
+ | Eop (Oshift (Oasr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Oasr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Oasr n)) (e1:::Enil)
| _ => Eop (Oshift (Oasr n)) (e1:::Enil)
end.
*)
@@ -825,7 +825,7 @@ Definition or_match (e1: expr) (e2: expr) :=
Definition or (e1: expr) (e2: expr) :=
match or_match e1 e2 with
| or_case1 n1 t1 n2 t2 =>
- if Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32)
+ if Int.eq (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize
&& same_expr_pure t1 t2
then Eop (Oshift (Sror n2)) (t1:::Enil)
else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil)
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 68b49fd81745043ce716af8f6817bd45cd00aefd..32aba30c29e98835ddb7d1b06763a1c660e5f2b0 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -342,7 +342,7 @@ Qed.
Theorem eval_shlimm:
forall le a n x,
eval_expr ge sp e m le a (Vint x) ->
- Int.ltu n (Int.repr 32) = true ->
+ Int.ltu n Int.iwordsize = true ->
eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)).
Proof.
intros until x. unfold shlimm, is_shift_amount.
@@ -365,7 +365,7 @@ Qed.
Theorem eval_shruimm:
forall le a n x,
eval_expr ge sp e m le a (Vint x) ->
- Int.ltu n (Int.repr 32) = true ->
+ Int.ltu n Int.iwordsize = true ->
eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)).
Proof.
intros until x. unfold shruimm, is_shift_amount.
@@ -388,7 +388,7 @@ Qed.
Theorem eval_shrimm:
forall le a n x,
eval_expr ge sp e m le a (Vint x) ->
- Int.ltu n (Int.repr 32) = true ->
+ Int.ltu n Int.iwordsize = true ->
eval_expr ge sp e m le (shrimm a n) (Vint (Int.shr x n)).
Proof.
intros until x. unfold shrimm, is_shift_amount.
@@ -416,7 +416,7 @@ Proof.
intros; unfold mulimm_base.
generalize (Int.one_bits_decomp n).
generalize (Int.one_bits_range n).
- change (Z_of_nat wordsize) with 32.
+ change (Z_of_nat Int.wordsize) with 32.
destruct (Int.one_bits n).
intros. EvalOp. constructor. EvalOp. simpl; reflexivity.
constructor. eauto. constructor. simpl. rewrite Int.mul_commut. auto.
@@ -497,7 +497,7 @@ Proof.
rewrite (Int.divs_pow2 x y i H0). auto.
exploit Int.ltu_inv; eauto.
change (Int.unsigned (Int.repr 31)) with 31.
- change (Int.unsigned (Int.repr 32)) with 32.
+ change (Int.unsigned Int.iwordsize) with 32.
omega.
apply eval_divs_base. auto. EvalOp. auto.
apply eval_divs_base. auto. EvalOp. auto.
@@ -634,10 +634,10 @@ Lemma eval_or:
eval_expr ge sp e m le (or a b) (Vint (Int.or x y)).
Proof.
intros until y; unfold or; case (or_match a b); intros; InvEval.
- caseEq (Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32)
+ caseEq (Int.eq (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize
&& same_expr_pure t1 t2); intro.
destruct (andb_prop _ _ H1).
- generalize (Int.eq_spec (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32)).
+ generalize (Int.eq_spec (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize).
rewrite H4. intro.
exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2.
simpl. EvalOp. simpl. decEq. decEq. apply Int.or_ror.
@@ -666,7 +666,7 @@ Theorem eval_shl:
forall le a x b y,
eval_expr ge sp e m le a (Vint x) ->
eval_expr ge sp e m le b (Vint y) ->
- Int.ltu y (Int.repr 32) = true ->
+ Int.ltu y Int.iwordsize = true ->
eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)).
Proof.
intros until y; unfold shl; case (shift_match b); intros.
@@ -678,7 +678,7 @@ Theorem eval_shru:
forall le a x b y,
eval_expr ge sp e m le a (Vint x) ->
eval_expr ge sp e m le b (Vint y) ->
- Int.ltu y (Int.repr 32) = true ->
+ Int.ltu y Int.iwordsize = true ->
eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)).
Proof.
intros until y; unfold shru; case (shift_match b); intros.
@@ -690,7 +690,7 @@ Theorem eval_shr:
forall le a x b y,
eval_expr ge sp e m le a (Vint x) ->
eval_expr ge sp e m le b (Vint y) ->
- Int.ltu y (Int.repr 32) = true ->
+ Int.ltu y Int.iwordsize = true ->
eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)).
Proof.
intros until y; unfold shr; case (shift_match b); intros.
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 8cc2185da86229aab9c9bc171e7b28c420ad5fd9..aa9c5116bee64579f66d727a3934673d7d40830e 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -276,11 +276,11 @@ Definition eval_binop
| Oor, Vint n1, Vint n2 => Some (Vint (Int.or n1 n2))
| Oxor, Vint n1, Vint n2 => Some (Vint (Int.xor n1 n2))
| Oshl, Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None
| Oshr, Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
| Oshru, Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
| Oaddf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.add f1 f2))
| Osubf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.sub f1 f2))
| Omulf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2))
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 32f90f558fbde8419073d1f830be6065930dde86..70cbeb41caaef979c5d5805f8a20bd9236802cc6 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -253,11 +253,11 @@ Proof.
apply eval_and; auto.
apply eval_or; auto.
apply eval_xor; auto.
- caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
+ caseEq (Int.ltu i0 Int.iwordsize); intro; rewrite H2 in H1; inv H1.
apply eval_shl; auto.
- caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
+ caseEq (Int.ltu i0 Int.iwordsize); intro; rewrite H2 in H1; inv H1.
apply eval_shr; auto.
- caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
+ caseEq (Int.ltu i0 Int.iwordsize); intro; rewrite H2 in H1; inv H1.
apply eval_shru; auto.
apply eval_addf; auto.
apply eval_subf; auto.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 5eaf46b273a2fd091271e0ac35be8d7b4029b9aa..a472e709d932fc81e0137260b14f33d79fa66352 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -939,11 +939,11 @@ Proof.
inv H0; try discriminate; inv H1; inv H; TrivialOp.
inv H0; try discriminate; inv H1; inv H; TrivialOp.
inv H0; try discriminate; inv H1; inv H; TrivialOp.
- destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp.
+ destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialOp.
inv H0; try discriminate; inv H1; inv H; TrivialOp.
- destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp.
+ destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialOp.
inv H0; try discriminate; inv H1; inv H; TrivialOp.
- destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp.
+ destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialOp.
inv H0; try discriminate; inv H1; inv H; TrivialOp.
inv H0; try discriminate; inv H1; inv H; TrivialOp.
inv H0; try discriminate; inv H1; inv H; TrivialOp.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index ee13487582f42782f8b9108aca46f1ce65a5adbf..62e9dc70877c8f58d9ece2223940efb1acfce493 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -252,7 +252,7 @@ Function sem_xor (v1 v2: val): option val :=
Function sem_shl (v1 v2: val): option val :=
match v1, v2 with
| Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint(Int.shl n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint(Int.shl n1 n2)) else None
| _, _ => None
end.
@@ -261,13 +261,13 @@ Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val :=
| shr_case_I32unsi =>
match v1,v2 with
| Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
| _,_ => None
end
| shr_case_ii =>
match v1,v2 with
| Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
| _, _ => None
end
| shr_default=>
diff --git a/common/Values.v b/common/Values.v
index 9645e8ac6a34889284b0ac9d3188eebeb5fb4447..19a8077de813f3a501196187dc166270b30ef913 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -240,7 +240,7 @@ Definition xor (v1 v2: val): val :=
Definition shl (v1 v2: val): val :=
match v1, v2 with
| Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32)
+ if Int.ltu n2 Int.iwordsize
then Vint(Int.shl n1 n2)
else Vundef
| _, _ => Vundef
@@ -249,7 +249,7 @@ Definition shl (v1 v2: val): val :=
Definition shr (v1 v2: val): val :=
match v1, v2 with
| Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32)
+ if Int.ltu n2 Int.iwordsize
then Vint(Int.shr n1 n2)
else Vundef
| _, _ => Vundef
@@ -258,7 +258,7 @@ Definition shr (v1 v2: val): val :=
Definition shr_carry (v1 v2: val): val :=
match v1, v2 with
| Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32)
+ if Int.ltu n2 Int.iwordsize
then Vint(Int.shr_carry n1 n2)
else Vundef
| _, _ => Vundef
@@ -267,7 +267,7 @@ Definition shr_carry (v1 v2: val): val :=
Definition shrx (v1 v2: val): val :=
match v1, v2 with
| Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32)
+ if Int.ltu n2 Int.iwordsize
then Vint(Int.shrx n1 n2)
else Vundef
| _, _ => Vundef
@@ -276,7 +276,7 @@ Definition shrx (v1 v2: val): val :=
Definition shru (v1 v2: val): val :=
match v1, v2 with
| Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32)
+ if Int.ltu n2 Int.iwordsize
then Vint(Int.shru n1 n2)
else Vundef
| _, _ => Vundef
@@ -291,7 +291,7 @@ Definition rolm (v: val) (amount mask: int): val :=
Definition ror (v1 v2: val): val :=
match v1, v2 with
| Vint n1, Vint n2 =>
- if Int.ltu n2 (Int.repr 32)
+ if Int.ltu n2 Int.iwordsize
then Vint(Int.ror n1 n2)
else Vundef
| _, _ => Vundef
@@ -593,7 +593,7 @@ Theorem mul_pow2:
mul x (Vint n) = shl x (Vint logn).
Proof.
intros; destruct x; simpl; auto.
- change 32 with (Z_of_nat wordsize).
+ change 32 with (Z_of_nat Int.wordsize).
rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto.
Qed.
@@ -619,7 +619,7 @@ Theorem divs_pow2:
divs x (Vint n) = shrx x (Vint logn).
Proof.
intros; destruct x; simpl; auto.
- change 32 with (Z_of_nat wordsize).
+ change 32 with (Z_of_nat Int.wordsize).
rewrite (Int.is_power2_range _ _ H).
generalize (Int.eq_spec n Int.zero);
case (Int.eq n Int.zero); intro.
@@ -633,7 +633,7 @@ Theorem divu_pow2:
divu x (Vint n) = shru x (Vint logn).
Proof.
intros; destruct x; simpl; auto.
- change 32 with (Z_of_nat wordsize).
+ change 32 with (Z_of_nat Int.wordsize).
rewrite (Int.is_power2_range _ _ H).
generalize (Int.eq_spec n Int.zero);
case (Int.eq n Int.zero); intro.
@@ -689,13 +689,13 @@ Qed.
Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y.
Proof.
destruct x; destruct y; simpl; auto.
- case (Int.ltu i0 (Int.repr 32)); auto.
+ case (Int.ltu i0 Int.iwordsize); auto.
decEq. symmetry. apply Int.shl_mul.
Qed.
Theorem shl_rolm:
forall x n,
- Int.ltu n (Int.repr 32) = true ->
+ Int.ltu n Int.iwordsize = true ->
shl x (Vint n) = rolm x n (Int.shl Int.mone n).
Proof.
intros; destruct x; simpl; auto.
@@ -704,8 +704,8 @@ Qed.
Theorem shru_rolm:
forall x n,
- Int.ltu n (Int.repr 32) = true ->
- shru x (Vint n) = rolm x (Int.sub (Int.repr 32) n) (Int.shru Int.mone n).
+ Int.ltu n Int.iwordsize = true ->
+ shru x (Vint n) = rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n).
Proof.
intros; destruct x; simpl; auto.
rewrite H. decEq. apply Int.shru_rolm. exact H.
@@ -716,7 +716,7 @@ Theorem shrx_carry:
add (shr x y) (shr_carry x y) = shrx x y.
Proof.
destruct x; destruct y; simpl; auto.
- case (Int.ltu i0 (Int.repr 32)); auto.
+ case (Int.ltu i0 Int.iwordsize); auto.
simpl. decEq. apply Int.shrx_carry.
Qed.
@@ -731,16 +731,12 @@ Qed.
Theorem rolm_rolm:
forall x n1 m1 n2 m2,
rolm (rolm x n1 m1) n2 m2 =
- rolm x (Int.and (Int.add n1 n2) (Int.repr 31))
+ rolm x (Int.modu (Int.add n1 n2) Int.iwordsize)
(Int.and (Int.rol m1 n2) m2).
Proof.
intros; destruct x; simpl; auto.
decEq.
- replace (Int.and (Int.add n1 n2) (Int.repr 31))
- with (Int.modu (Int.add n1 n2) (Int.repr 32)).
- apply Int.rolm_rolm.
- change (Int.repr 31) with (Int.sub (Int.repr 32) Int.one).
- apply Int.modu_and with (Int.repr 5). reflexivity.
+ apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
Qed.
Theorem rolm_zero:
@@ -922,7 +918,7 @@ Lemma rolm_lt_zero:
forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero).
Proof.
intros. destruct v; simpl; auto.
- transitivity (Vint (Int.shru i (Int.repr (Z_of_nat wordsize - 1)))).
+ transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))).
decEq. symmetry. rewrite Int.shru_rolm. auto. auto.
rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto.
Qed.
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 0c58da09501d29f7d0e64928c4de6f5155ab98da..5375c0445a7117234da831daefd7471281cdabda 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -357,6 +357,13 @@ Proof.
rewrite two_power_nat_S. omega.
Qed.
+Lemma two_power_nat_two_p:
+ forall x, two_power_nat x = two_p (Z_of_nat x).
+Proof.
+ induction x. auto.
+ rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega.
+Qed.
+
Lemma two_p_monotone:
forall x y, 0 <= x <= y -> two_p x <= two_p y.
Proof.
@@ -369,11 +376,12 @@ Proof.
assert (two_p x > 0). apply two_p_gt_ZERO. omega. omega.
Qed.
-Lemma two_power_nat_two_p:
- forall x, two_power_nat x = two_p (Z_of_nat x).
+Lemma two_p_monotone_strict:
+ forall x y, 0 <= x < y -> two_p x < two_p y.
Proof.
- induction x. auto.
- rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega.
+ intros. assert (two_p x <= two_p (y - 1)). apply two_p_monotone; omega.
+ assert (two_p (y - 1) > 0). apply two_p_gt_ZERO. omega.
+ replace y with (Zsucc (y - 1)) by omega. rewrite two_p_S. omega. omega.
Qed.
Lemma two_p_strict:
@@ -385,6 +393,16 @@ Proof.
omega.
Qed.
+Lemma two_p_strict_2:
+ forall x, x >= 0 -> 2 * x - 1 < two_p x.
+Proof.
+ intros. assert (x = 0 \/ x - 1 >= 0) by omega. destruct H0.
+ subst. vm_compute. auto.
+ replace (two_p x) with (2 * two_p (x - 1)).
+ generalize (two_p_strict _ H0). omega.
+ rewrite <- two_p_S. decEq. omega. omega.
+Qed.
+
(** Properties of [Zmin] and [Zmax] *)
Lemma Zmin_spec:
@@ -522,7 +540,7 @@ Qed.
Lemma Zdiv_interval_2:
forall lo hi a b,
- lo <= a <= hi -> lo <= 0 -> hi > 0 -> b > 0 ->
+ lo <= a <= hi -> lo <= 0 -> hi >= 0 -> b > 0 ->
lo <= a/b <= hi.
Proof.
intros.
diff --git a/lib/Integers.v b/lib/Integers.v
index 625973a0600b6f1ab26872f474a9378aca8475a4..fb6eee23e8b2e89b81062115de5de026049f3e5c 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -13,14 +13,10 @@
(* *)
(* *********************************************************************)
-(** Formalizations of integers modulo $2^32$ #2<sup>32</sup>#. *)
+(** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *)
Require Import Coqlib.
-Definition wordsize : nat := 32%nat.
-Definition modulus : Z := two_power_nat wordsize.
-Definition half_modulus : Z := modulus / 2.
-
(** * Comparisons *)
Inductive comparison : Type :=
@@ -51,6 +47,40 @@ Definition swap_comparison (c: comparison): comparison :=
| Cge => Cle
end.
+(** * Parameterization by the word size, in bits. *)
+
+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.
+Proof.
+ unfold wordsize. generalize WS.wordsize_not_zero. omega.
+Qed.
+
+Remark modulus_power:
+ modulus = two_p (Z_of_nat wordsize).
+Proof.
+ unfold modulus. apply two_power_nat_two_p.
+Qed.
+
+Remark modulus_pos:
+ modulus > 0.
+Proof.
+ rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega.
+Qed.
+
(** * Representation of machine integers *)
(** A machine integer (type [int]) is represented as a Coq arbitrary-precision
@@ -59,12 +89,6 @@ Definition swap_comparison (c: comparison): comparison :=
Record int: Type := mkint { intval: Z; intrange: 0 <= intval < modulus }.
-Module Int.
-
-Definition max_unsigned : Z := modulus - 1.
-Definition max_signed : Z := half_modulus - 1.
-Definition min_signed : Z := - half_modulus.
-
(** The [unsigned] and [signed] functions return the Coq integer corresponding
to the given machine integer, interpreted as unsigned or signed
respectively. *)
@@ -76,22 +100,16 @@ Definition signed (n: int) : Z :=
then unsigned n
else unsigned n - modulus.
-Lemma mod_in_range:
- forall x, 0 <= Zmod x modulus < modulus.
-Proof.
- intro.
- exact (Z_mod_lt x modulus (two_power_nat_pos wordsize)).
-Qed.
-
(** 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) (mod_in_range x).
+ 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.
@@ -370,13 +388,125 @@ Definition notbool (x: int) : int := if eq x zero then one else zero.
(** * Properties of integers and integer arithmetic *)
-(** ** Properties of equality *)
+(** ** Properties of [modulus], [max_unsigned], etc. *)
+
+Remark half_modulus_power:
+ half_modulus = two_p (Z_of_nat wordsize - 1).
+Proof.
+ unfold half_modulus. rewrite modulus_power.
+ set (ws1 := Z_of_nat wordsize - 1).
+ replace (Z_of_nat wordsize) with (Zsucc ws1).
+ rewrite two_p_S. rewrite Zmult_comm. apply Z_div_mult. omega.
+ unfold ws1. generalize wordsize_pos; omega.
+ unfold ws1. omega.
+Qed.
+
+Remark half_modulus_modulus: modulus = 2 * half_modulus.
+Proof.
+ rewrite half_modulus_power. rewrite modulus_power.
+ rewrite <- two_p_S. decEq. omega.
+ generalize wordsize_pos; omega.
+Qed.
+
+(** 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.
+ rewrite half_modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega.
+Qed.
+
+Remark min_signed_neg: min_signed < 0.
+Proof.
+ unfold min_signed. generalize half_modulus_pos. omega.
+Qed.
-Theorem one_not_zero: Int.one <> Int.zero.
+Remark max_signed_pos: max_signed >= 0.
Proof.
- compute. congruence.
+ unfold max_signed. generalize half_modulus_pos. omega.
Qed.
+Remark wordsize_max_unsigned: Z_of_nat wordsize <= max_unsigned.
+Proof.
+ assert (Z_of_nat wordsize < modulus).
+ rewrite modulus_power. apply two_p_strict.
+ generalize wordsize_pos. omega.
+ unfold max_unsigned. omega.
+Qed.
+
+Remark two_wordsize_max_unsigned: 2 * Z_of_nat wordsize - 1 <= max_unsigned.
+Proof.
+ assert (2 * Z_of_nat wordsize - 1 < modulus).
+ rewrite modulus_power. apply two_p_strict_2. generalize wordsize_pos; omega.
+ unfold max_unsigned; omega.
+Qed.
+
+Remark max_signed_unsigned: max_signed < max_unsigned.
+Proof.
+ unfold max_signed, max_unsigned. rewrite half_modulus_modulus.
+ generalize half_modulus_pos. omega.
+Qed.
+
+(** ** Properties of zero, one, minus one *)
+
+Theorem unsigned_zero: unsigned zero = 0.
+Proof.
+ simpl. apply Zmod_0_l.
+Qed.
+
+Theorem unsigned_one: unsigned one = 1.
+Proof.
+ simpl. apply Zmod_small. split. omega.
+ unfold modulus. replace wordsize with (S(pred wordsize)).
+ rewrite two_power_nat_S. generalize (two_power_nat_pos (pred wordsize)).
+ omega.
+ generalize wordsize_pos. omega.
+Qed.
+
+Theorem unsigned_mone: unsigned mone = modulus - 1.
+Proof.
+ simpl unsigned.
+ replace (-1) with ((modulus - 1) + (-1) * modulus).
+ rewrite Z_mod_plus_full. apply Zmod_small.
+ generalize modulus_pos. omega. omega.
+Qed.
+
+Theorem signed_zero: signed zero = 0.
+Proof.
+ unfold signed. rewrite unsigned_zero. apply zlt_true. generalize half_modulus_pos; omega.
+Qed.
+
+Theorem signed_mone: signed mone = -1.
+Proof.
+ unfold signed. rewrite unsigned_mone.
+ rewrite zlt_false. omega.
+ rewrite half_modulus_modulus. generalize half_modulus_pos. omega.
+Qed.
+
+Theorem one_not_zero: one <> zero.
+Proof.
+ assert (unsigned one <> unsigned zero).
+ rewrite unsigned_one; rewrite unsigned_zero; congruence.
+ congruence.
+Qed.
+
+Theorem unsigned_repr_wordsize:
+ unsigned iwordsize = Z_of_nat wordsize.
+Proof.
+ simpl. apply Zmod_small.
+ generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega.
+Qed.
+
+(** ** Properties of equality *)
+
Theorem eq_sym:
forall x y, eq x y = eq y x.
Proof.
@@ -490,14 +620,16 @@ 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
- $2^32$ #2<sup>32</sup>#. *)
+ $2^{wordsize}$ #2<sup>wordsize</sup>#. *)
-Lemma modulus_pos:
- modulus > 0.
-Proof.
- unfold modulus. apply two_power_nat_pos.
-Qed.
Hint Resolve modulus_pos: ints.
Definition eqm := eqmod modulus.
@@ -605,10 +737,9 @@ Proof.
intros. unfold signed.
generalize (unsigned_range i). set (n := unsigned i). intros.
case (zlt n half_modulus); intro.
- unfold max_signed. assert (min_signed < 0). compute. auto.
- omega.
- unfold min_signed, max_signed. change modulus with (2 * half_modulus).
- change modulus with (2 * half_modulus) in H. omega.
+ unfold max_signed. generalize min_signed_neg. omega.
+ unfold min_signed, max_signed.
+ rewrite half_modulus_modulus in *. omega.
Qed.
Theorem repr_unsigned:
@@ -625,7 +756,7 @@ Proof.
intros. transitivity (repr (unsigned i)).
apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints.
Qed.
-Hint Resolve repr_unsigned: ints.
+Hint Resolve repr_signed: ints.
Theorem unsigned_repr:
forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z.
@@ -641,19 +772,16 @@ Proof.
intros. unfold signed. case (zle 0 z); intro.
replace (unsigned (repr z)) with z.
rewrite zlt_true. auto. unfold max_signed in H. omega.
- symmetry. apply unsigned_repr.
- split. auto. apply Zle_trans with max_signed. tauto.
- compute; intro; discriminate.
+ symmetry. apply unsigned_repr. generalize max_signed_unsigned. omega.
pose (z' := z + modulus).
replace (repr z) with (repr z').
replace (unsigned (repr z')) with z'.
rewrite zlt_false. unfold z'. omega.
- unfold z'. unfold min_signed in H.
- change modulus with (half_modulus + half_modulus). omega.
+ unfold z'. unfold min_signed in H.
+ rewrite half_modulus_modulus. omega.
symmetry. apply unsigned_repr.
unfold z', max_unsigned. unfold min_signed, max_signed in H.
- change modulus with (half_modulus + half_modulus).
- omega.
+ rewrite half_modulus_modulus. omega.
apply eqm_samerepr. unfold z'; red. exists 1. omega.
Qed.
@@ -815,7 +943,7 @@ Qed.
Theorem mul_one: forall x, mul x one = x.
Proof.
- intros; unfold mul. change (unsigned one) with 1.
+ intros; unfold mul. rewrite unsigned_one.
transitivity (repr (unsigned x)). decEq. ring.
apply repr_unsigned.
Qed.
@@ -1112,31 +1240,19 @@ Proof (bitwise_binop_assoc andb andb_assoc).
Theorem and_zero: forall x, and x zero = zero.
Proof.
- unfold and, bitwise_binop, zero; intros.
- transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize 0))).
- decEq. apply Z_of_bits_exten. intros.
- change (unsigned (repr 0)) with 0.
- rewrite bits_of_Z_zero. apply andb_b_false.
- auto with ints.
-Qed.
-
-Lemma mone_max_unsigned:
- mone = repr max_unsigned.
-Proof.
- unfold mone. apply eqm_samerepr. exists (-1).
- unfold max_unsigned. omega.
+ intros. unfold and, bitwise_binop.
+ apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
+ apply eqm_refl2. apply Z_of_bits_exten. intros.
+ rewrite unsigned_zero. rewrite bits_of_Z_zero. apply andb_b_false.
Qed.
Theorem and_mone: forall x, and x mone = x.
Proof.
- unfold and, bitwise_binop; intros.
- rewrite mone_max_unsigned. unfold max_unsigned, modulus.
- transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
- decEq. apply Z_of_bits_exten. intros.
- rewrite unsigned_repr. rewrite bits_of_Z_mone.
- apply andb_b_true. omega. compute. intuition congruence.
- transitivity (repr (unsigned x)).
- apply eqm_samerepr. apply Z_of_bits_of_Z.
+ intros. unfold and, bitwise_binop.
+ transitivity (repr(unsigned x)).
+ apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
+ apply eqm_refl2. apply Z_of_bits_exten. intros.
+ rewrite unsigned_mone. rewrite bits_of_Z_mone. apply andb_b_true. auto.
apply repr_unsigned.
Qed.
@@ -1155,26 +1271,22 @@ Proof (bitwise_binop_assoc orb orb_assoc).
Theorem or_zero: forall x, or x zero = x.
Proof.
- unfold or, bitwise_binop, zero; intros.
- transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
- decEq. apply Z_of_bits_exten. intros.
- change (unsigned (repr 0)) with 0.
- rewrite bits_of_Z_zero. apply orb_b_false.
- transitivity (repr (unsigned x)); auto with ints.
- apply eqm_samerepr. apply Z_of_bits_of_Z.
+ intros. unfold or, bitwise_binop.
+ transitivity (repr(unsigned x)).
+ apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
+ apply eqm_refl2. apply Z_of_bits_exten. intros.
+ rewrite unsigned_zero. rewrite bits_of_Z_zero. apply orb_b_false.
+ apply repr_unsigned.
Qed.
Theorem or_mone: forall x, or x mone = mone.
Proof.
- rewrite mone_max_unsigned.
- unfold or, bitwise_binop; intros.
- decEq.
- transitivity (Z_of_bits wordsize (bits_of_Z wordsize max_unsigned)).
- apply Z_of_bits_exten. intros.
- change (unsigned (repr max_unsigned)) with max_unsigned.
- unfold max_unsigned, modulus. rewrite bits_of_Z_mone; auto.
- apply orb_b_true.
- apply eqm_small_eq; auto with ints. compute; intuition congruence.
+ intros. unfold or, bitwise_binop.
+ transitivity (repr(unsigned mone)).
+ apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
+ apply eqm_refl2. apply Z_of_bits_exten. intros.
+ rewrite unsigned_mone. rewrite bits_of_Z_mone. apply orb_b_true. auto.
+ apply repr_unsigned.
Qed.
Theorem or_idem: forall x, or x x = x.
@@ -1207,20 +1319,29 @@ Qed.
Theorem xor_zero: forall x, xor x zero = x.
Proof.
- unfold xor, bitwise_binop, zero; intros.
- transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
- decEq. apply Z_of_bits_exten. intros.
- change (unsigned (repr 0)) with 0.
- rewrite bits_of_Z_zero. apply xorb_false.
- transitivity (repr (unsigned x)); auto with ints.
- apply eqm_samerepr. apply Z_of_bits_of_Z.
+ intros. unfold xor, bitwise_binop.
+ transitivity (repr(unsigned x)).
+ apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
+ apply eqm_refl2. apply Z_of_bits_exten. intros.
+ rewrite unsigned_zero. rewrite bits_of_Z_zero. apply xorb_false.
+ apply repr_unsigned.
+Qed.
+
+Theorem xor_idem: forall x, xor x x = zero.
+Proof.
+ intros. unfold xor, bitwise_binop.
+ transitivity (repr(unsigned zero)).
+ apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
+ apply eqm_refl2. apply Z_of_bits_exten. intros.
+ rewrite unsigned_zero. rewrite bits_of_Z_zero. apply xorb_nilpotent.
+ apply repr_unsigned.
Qed.
Theorem xor_zero_one: xor zero one = one.
-Proof. reflexivity. Qed.
+Proof. rewrite xor_commut. apply xor_zero. Qed.
Theorem xor_one_one: xor one one = zero.
-Proof. reflexivity. Qed.
+Proof. apply xor_idem. Qed.
Theorem and_xor_distrib:
forall x y z,
@@ -1238,64 +1359,9 @@ Qed.
Theorem not_involutive:
forall (x: int), not (not x) = x.
Proof.
- intros. unfold not. rewrite xor_assoc.
- change (xor mone mone) with zero.
- rewrite xor_zero. auto.
+ intros. unfold not. rewrite xor_assoc. rewrite xor_idem. apply xor_zero.
Qed.
-(** ** Proofs by reflexion *)
-
-(** To prove equalities involving shifts and rotates, we need to
- show complicated integer equalities involving one integer variable
- that ranges between 0 and 31. Rather than proving these equalities,
- we ask Coq to check them by computing the 32 values of the
- left and right-hand sides and checking that they are equal.
- This is an instance of proving by reflection. *)
-
-Section REFLECTION.
-
-Variables (f g: int -> int).
-
-Fixpoint check_equal_on_range (n: nat) : bool :=
- match n with
- | O => true
- | S n => if eq (f (repr (Z_of_nat n))) (g (repr (Z_of_nat n)))
- then check_equal_on_range n
- else false
- end.
-
-Lemma check_equal_on_range_correct:
- forall n,
- check_equal_on_range n = true ->
- forall z, 0 <= z < Z_of_nat n -> f (repr z) = g (repr z).
-Proof.
- induction n.
- simpl; intros; omegaContradiction.
- simpl check_equal_on_range.
- set (fn := f (repr (Z_of_nat n))).
- set (gn := g (repr (Z_of_nat n))).
- generalize (eq_spec fn gn).
- case (eq fn gn); intros.
- rewrite inj_S in H1.
- assert (0 <= z < Z_of_nat n \/ z = Z_of_nat n). omega.
- elim H2; intro.
- apply IHn. auto. auto.
- subst z; auto.
- discriminate.
-Qed.
-
-Lemma equal_on_range:
- check_equal_on_range wordsize = true ->
- forall n, 0 <= unsigned n < Z_of_nat wordsize ->
- f n = g n.
-Proof.
- intros. replace n with (repr (unsigned n)).
- apply check_equal_on_range_correct with wordsize; auto.
- apply repr_unsigned.
-Qed.
-
-End REFLECTION.
-
(** ** Properties of shifts and rotates *)
Lemma Z_of_bits_shift:
@@ -1374,30 +1440,34 @@ Proof.
rewrite H. apply shl_mul_two_p.
Qed.
+Lemma ltu_inv:
+ forall x y, ltu x y = true -> 0 <= unsigned x < unsigned y.
+Proof.
+ unfold ltu; intros. destruct (zlt (unsigned x) (unsigned y)).
+ split; auto. generalize (unsigned_range x); omega.
+ discriminate.
+Qed.
+
Theorem shl_rolm:
forall x n,
- ltu n (repr (Z_of_nat wordsize)) = true ->
+ ltu n iwordsize = true ->
shl x n = rolm x n (shl mone n).
Proof.
- intros x n. unfold ltu.
- rewrite unsigned_repr. case (zlt (unsigned n) (Z_of_nat wordsize)); intros LT XX.
+ intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize; intros.
unfold shl, rolm, rol, and, bitwise_binop.
decEq. apply Z_of_bits_exten; intros.
repeat rewrite unsigned_repr; auto with ints.
repeat rewrite bits_of_Z_of_bits; auto.
case (zlt z (unsigned n)); intro LT2.
assert (z - unsigned n < 0). omega.
- rewrite (bits_of_Z_below wordsize (unsigned x) _ H0).
- rewrite (bits_of_Z_below wordsize (unsigned mone) _ H0).
+ rewrite (bits_of_Z_below wordsize (unsigned x) _ H2).
+ rewrite (bits_of_Z_below wordsize (unsigned mone) _ H2).
symmetry. apply andb_b_false.
assert (z - unsigned n < Z_of_nat wordsize).
- generalize (unsigned_range n). omega.
- replace (unsigned mone) with (two_power_nat wordsize - 1).
+ generalize (unsigned_range n). omega.
+ rewrite unsigned_mone.
rewrite bits_of_Z_mone. rewrite andb_b_true. decEq.
- rewrite Zmod_small. auto. omega. omega.
- rewrite mone_max_unsigned. reflexivity.
- discriminate.
- compute; intuition congruence.
+ rewrite Zmod_small. auto. omega. omega.
Qed.
Lemma bitwise_binop_shl:
@@ -1416,32 +1486,25 @@ Proof.
generalize (unsigned_range n). omega.
Qed.
-Lemma and_shl:
+Theorem and_shl:
forall x y n,
and (shl x n) (shl y n) = shl (and x y) n.
Proof.
unfold and; intros. apply bitwise_binop_shl. reflexivity.
Qed.
-Remark ltu_inv:
- forall x y, ltu x y = true -> 0 <= unsigned x < unsigned y.
-Proof.
- unfold ltu; intros. destruct (zlt (unsigned x) (unsigned y)).
- split; auto. generalize (unsigned_range x); omega.
- discriminate.
-Qed.
Theorem shl_shl:
forall x y z,
- ltu y (repr (Z_of_nat wordsize)) = true ->
- ltu z (repr (Z_of_nat wordsize)) = true ->
- ltu (add y z) (repr (Z_of_nat wordsize)) = true ->
+ 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.
intros. unfold shl, add.
generalize (ltu_inv _ _ H).
generalize (ltu_inv _ _ H0).
- change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+ rewrite unsigned_repr_wordsize.
set (x' := unsigned x).
set (y' := unsigned y).
set (z' := unsigned z).
@@ -1454,21 +1517,21 @@ Proof.
destruct (zle (Z_of_nat wordsize) (n - z')).
symmetry. apply bits_of_Z_below. omega.
decEq. omega.
- assert (2 * Z_of_nat wordsize < max_unsigned). vm_compute; auto. omega.
+ generalize two_wordsize_max_unsigned; omega.
apply Z_of_bits_range_2.
Qed.
Theorem shru_shru:
forall x y z,
- ltu y (repr (Z_of_nat wordsize)) = true ->
- ltu z (repr (Z_of_nat wordsize)) = true ->
- ltu (add y z) (repr (Z_of_nat wordsize)) = true ->
+ 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.
intros. unfold shru, add.
generalize (ltu_inv _ _ H).
generalize (ltu_inv _ _ H0).
- change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+ rewrite unsigned_repr_wordsize.
set (x' := unsigned x).
set (y' := unsigned y).
set (z' := unsigned z).
@@ -1480,43 +1543,35 @@ Proof.
destruct (zle (Z_of_nat wordsize) (n + z')).
symmetry. apply bits_of_Z_above. omega.
decEq. omega.
- assert (2 * Z_of_nat wordsize < max_unsigned). vm_compute; auto. omega.
+ generalize two_wordsize_max_unsigned; omega.
apply Z_of_bits_range_2.
Qed.
Theorem shru_rolm:
forall x n,
- ltu n (repr (Z_of_nat wordsize)) = true ->
- shru x n = rolm x (sub (repr (Z_of_nat wordsize)) n) (shru mone n).
+ ltu n iwordsize = true ->
+ shru x n = rolm x (sub iwordsize n) (shru mone n).
Proof.
- intros x n. unfold ltu.
- rewrite unsigned_repr.
- case (zlt (unsigned n) (Z_of_nat wordsize)); intros LT XX.
+ intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize. intro.
unfold shru, rolm, rol, and, bitwise_binop.
decEq. apply Z_of_bits_exten; intros.
repeat rewrite unsigned_repr; auto with ints.
repeat rewrite bits_of_Z_of_bits; auto.
- unfold sub.
- change (unsigned (repr (Z_of_nat wordsize)))
- with (Z_of_nat wordsize).
+ unfold sub. rewrite unsigned_repr_wordsize.
rewrite unsigned_repr.
case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro LT2.
- replace (unsigned mone) with (two_power_nat wordsize - 1).
- rewrite bits_of_Z_mone. rewrite andb_b_true.
+ rewrite unsigned_mone. rewrite bits_of_Z_mone. rewrite andb_b_true.
decEq.
replace (z - (Z_of_nat wordsize - unsigned n))
with ((z + unsigned n) + (-1) * Z_of_nat wordsize).
rewrite Z_mod_plus. symmetry. apply Zmod_small.
generalize (unsigned_range n). omega. omega. omega.
generalize (unsigned_range n). omega.
- reflexivity.
rewrite (bits_of_Z_above wordsize (unsigned x) _ LT2).
rewrite (bits_of_Z_above wordsize (unsigned mone) _ LT2).
symmetry. apply andb_b_false.
split. omega. apply Zle_trans with (Z_of_nat wordsize).
- generalize (unsigned_range n); omega. compute; intuition congruence.
- discriminate.
- split. omega. compute; intuition congruence.
+ generalize (unsigned_range n); omega. apply wordsize_max_unsigned.
Qed.
Lemma bitwise_binop_shru:
@@ -1544,15 +1599,15 @@ Qed.
Theorem shr_shr:
forall x y z,
- ltu y (repr (Z_of_nat wordsize)) = true ->
- ltu z (repr (Z_of_nat wordsize)) = true ->
- ltu (add y z) (repr (Z_of_nat wordsize)) = true ->
+ 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.
intros. unfold shr, add.
generalize (ltu_inv _ _ H).
generalize (ltu_inv _ _ H0).
- change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+ rewrite unsigned_repr_wordsize.
set (x' := signed x).
set (y' := unsigned y).
set (z' := unsigned z).
@@ -1561,22 +1616,22 @@ Proof.
rewrite two_p_is_exp.
rewrite signed_repr.
decEq. apply Zdiv_Zdiv. apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega.
- apply Zdiv_interval_2. unfold x'; apply signed_range.
- vm_compute; congruence. vm_compute; auto. apply two_p_gt_ZERO. omega.
- omega. omega.
- assert (2 * Z_of_nat wordsize < max_unsigned). vm_compute; auto.
- omega.
+ apply Zdiv_interval_2. unfold x'; apply signed_range.
+ generalize min_signed_neg; omega.
+ generalize max_signed_pos; omega.
+ apply two_p_gt_ZERO. omega. omega. omega.
+ generalize two_wordsize_max_unsigned; omega.
Qed.
Theorem rol_zero:
forall x,
rol x zero = x.
Proof.
- intros. unfold rol. transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
- decEq.
- transitivity (repr (unsigned x)).
- decEq. apply eqm_small_eq. apply Z_of_bits_of_Z.
- auto with ints. auto with ints. auto with ints.
+ intros. transitivity (repr (unsigned x)).
+ unfold rol. apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
+ apply eqm_refl2. apply Z_of_bits_exten; intros. decEq. rewrite unsigned_zero.
+ replace (z - 0) with z by omega. apply Zmod_small. auto.
+ apply repr_unsigned.
Qed.
Lemma bitwise_binop_rol:
@@ -1587,7 +1642,7 @@ Proof.
decEq. repeat (rewrite unsigned_repr; auto with ints).
apply Z_of_bits_exten; intros.
repeat rewrite bits_of_Z_of_bits; auto.
- apply Z_mod_lt. compute. auto.
+ apply Z_mod_lt. generalize wordsize_pos; omega.
Qed.
Theorem rol_and:
@@ -1599,7 +1654,8 @@ Qed.
Theorem rol_rol:
forall x n m,
- rol (rol x n) m = rol x (modu (add n m) (repr (Z_of_nat wordsize))).
+ Zdivide (Z_of_nat wordsize) modulus ->
+ rol (rol x n) m = rol x (modu (add n m) iwordsize).
Proof.
intros. unfold rol. decEq.
repeat (rewrite unsigned_repr; auto with ints).
@@ -1608,14 +1664,11 @@ Proof.
decEq. unfold modu, add.
set (W := Z_of_nat wordsize).
set (M := unsigned m); set (N := unsigned n).
- assert (W > 0). compute; auto.
+ assert (W > 0). unfold W; generalize wordsize_pos; omega.
assert (forall a, eqmod W a (unsigned (repr a))).
- intro. elim (eqm_unsigned_repr a). intros k EQ.
- red. exists (k * (modulus / W)).
- replace (k * (modulus / W) * W) with (k * modulus). auto.
- rewrite <- Zmult_assoc. reflexivity.
+ intros. eapply eqmod_divides. apply eqm_unsigned_repr. assumption.
apply eqmod_mod_eq. auto.
- change (unsigned (repr W)) with W.
+ replace (unsigned iwordsize) with W.
apply eqmod_trans with (z - (N + M) mod W).
apply eqmod_trans with ((z - M) - N).
apply eqmod_sub. apply eqmod_sym. apply eqmod_mod. auto.
@@ -1624,11 +1677,12 @@ Proof.
apply eqmod_sub. apply eqmod_refl. apply eqmod_mod. auto.
omega.
apply eqmod_sub. apply eqmod_refl.
- eapply eqmod_trans; [idtac|apply H1].
+ eapply eqmod_trans; [idtac|apply H2].
eapply eqmod_trans; [idtac|apply eqmod_mod].
apply eqmod_sym. eapply eqmod_trans; [idtac|apply eqmod_mod].
- apply eqmod_sym. apply H1. auto. auto.
- apply Z_mod_lt. compute; auto.
+ apply eqmod_sym. apply H2. auto. auto.
+ symmetry. unfold W. apply unsigned_repr_wordsize.
+ apply Z_mod_lt. generalize wordsize_pos; omega.
Qed.
Theorem rolm_zero:
@@ -1640,13 +1694,14 @@ Qed.
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) (repr (Z_of_nat wordsize)))
+ rolm x (modu (add n1 n2) iwordsize)
(and (rol m1 n2) m2).
Proof.
intros.
unfold rolm. rewrite rol_and. rewrite and_assoc.
- rewrite rol_rol. reflexivity.
+ rewrite rol_rol. reflexivity. auto.
Qed.
Theorem rol_or:
@@ -1665,86 +1720,101 @@ Qed.
Theorem ror_rol:
forall x y,
- ltu y (repr (Z_of_nat wordsize)) = true ->
- ror x y = rol x (sub (Int.repr (Z_of_nat wordsize)) y).
+ ltu y iwordsize = true ->
+ ror x y = rol x (sub iwordsize y).
Proof.
intros. unfold ror, rol, sub.
generalize (ltu_inv _ _ H).
- change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+ rewrite unsigned_repr_wordsize.
intro. rewrite unsigned_repr.
decEq. apply Z_of_bits_exten. intros. decEq.
apply eqmod_mod_eq. omega.
exists 1. omega.
- assert (Z_of_nat wordsize < max_unsigned). vm_compute; auto. omega.
-Qed.
-
-Remark or_shl_shru_masks:
- forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
- or (shl mone (sub (repr (Z_of_nat wordsize)) logn)) (shru mone logn) = mone.
-Proof.
- apply (equal_on_range
- (fun l => or (shl mone (sub (repr (Z_of_nat wordsize)) l)) (shru mone l))
- (fun l => mone)).
- vm_compute; auto.
+ generalize wordsize_pos; generalize wordsize_max_unsigned; omega.
Qed.
Theorem or_ror:
forall x y z,
- ltu y (repr (Z_of_nat wordsize)) = true ->
- ltu z (repr (Z_of_nat wordsize)) = true ->
- add y z = repr (Z_of_nat wordsize) ->
+ ltu y iwordsize = true ->
+ ltu z iwordsize = true ->
+ add y z = iwordsize ->
ror x z = or (shl x y) (shru x z).
Proof.
intros.
generalize (ltu_inv _ _ H).
generalize (ltu_inv _ _ H0).
- change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+ rewrite unsigned_repr_wordsize.
intros.
- rewrite ror_rol; auto.
- rewrite shl_rolm; auto.
- rewrite shru_rolm; auto.
- replace y with (sub (repr (Z_of_nat wordsize)) z).
- rewrite or_rolm.
- rewrite or_shl_shru_masks; auto.
- unfold rolm. rewrite and_mone. auto.
- rewrite <- H1. rewrite sub_add_opp. rewrite add_assoc.
- rewrite <- sub_add_opp. rewrite sub_idem. apply add_zero.
-Qed.
-
-Remark shru_shl_and_1:
- forall y,
- 0 <= unsigned y < Z_of_nat wordsize ->
- modu (add y (sub (repr (Z_of_nat wordsize)) y)) (repr (Z_of_nat wordsize)) = zero.
+ unfold or, bitwise_binop, shl, shru, ror.
+ set (ux := unsigned x).
+ decEq. apply Z_of_bits_exten. intros i iRANGE.
+ repeat rewrite unsigned_repr.
+ repeat rewrite bits_of_Z_of_bits; auto.
+ assert (y = sub iwordsize z).
+ rewrite <- H1. rewrite add_commut. rewrite sub_add_l. rewrite sub_idem.
+ rewrite add_commut. rewrite add_zero. auto.
+ assert (unsigned y = Z_of_nat wordsize - unsigned z).
+ rewrite H4. unfold sub. rewrite unsigned_repr_wordsize. apply unsigned_repr.
+ generalize wordsize_max_unsigned; omega.
+ destruct (zlt (i + unsigned z) (Z_of_nat wordsize)).
+ rewrite Zmod_small.
+ replace (bits_of_Z wordsize ux (i - unsigned y)) with false.
+ auto.
+ symmetry. apply bits_of_Z_below. omega. omega.
+ replace (bits_of_Z wordsize ux (i + unsigned z)) with false.
+ rewrite orb_false_r. decEq.
+ replace (i + unsigned z) with (i - unsigned y + 1 * Z_of_nat wordsize) by omega.
+ rewrite Z_mod_plus. apply Zmod_small. omega. generalize wordsize_pos; omega.
+ symmetry. apply bits_of_Z_above. auto.
+ apply Z_of_bits_range_2. apply Z_of_bits_range_2.
+Qed.
+
+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.
Proof.
- intros.
- apply (equal_on_range
- (fun y => modu (add y (sub (repr (Z_of_nat wordsize)) y)) (repr (Z_of_nat wordsize)))
- (fun y => zero)).
- vm_compute. auto. auto.
+ induction n; intros.
+ simpl in H0. omegaContradiction.
+ destruct (zeq x 0). subst x. change (two_p 0 - 1) with 0. rewrite bits_of_Z_zero.
+ unfold proj_sumbool; rewrite zlt_false. auto. omega.
+ replace (two_p x) with (2 * two_p (x - 1)). simpl. rewrite Z_bin_decomp_2xm1.
+ destruct (zeq i 0). subst. unfold proj_sumbool. rewrite zlt_true. auto. omega.
+ rewrite inj_S in H0. rewrite IHn. unfold proj_sumbool. destruct (zlt i x).
+ apply zlt_true. omega.
+ apply zlt_false. omega.
+ omega. omega. rewrite <- two_p_S. decEq. omega. omega.
Qed.
-Remark shru_shl_and_2:
- forall y,
- 0 <= unsigned y < Z_of_nat wordsize ->
- and (rol (shl mone y) (sub (repr (Z_of_nat wordsize)) y)) (shru mone y) =
- Int.repr (two_p (Z_of_nat wordsize - unsigned y) - 1).
+Remark two_p_m1_range:
+ forall n,
+ 0 <= n <= Z_of_nat wordsize ->
+ 0 <= two_p n - 1 <= max_unsigned.
Proof.
- intros.
- apply (equal_on_range
- (fun y => and (rol (shl mone y) (sub (repr (Z_of_nat wordsize)) y)) (shru mone y))
- (fun y => Int.repr (two_p (Z_of_nat wordsize - unsigned y) - 1))).
- vm_compute. auto. auto.
+ intros. split.
+ assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega.
+ assert (two_p n <= two_p (Z_of_nat wordsize)). apply two_p_monotone. auto.
+ unfold max_unsigned. unfold modulus. rewrite two_power_nat_two_p. omega.
Qed.
Theorem shru_shl_and:
forall x y,
- ltu y (Int.repr (Z_of_nat wordsize)) = true ->
- shru (shl x y) y = and x (Int.repr (two_p (Z_of_nat wordsize - unsigned y) - 1)).
+ ltu y iwordsize = true ->
+ shru (shl x y) y = and x (repr (two_p (Z_of_nat wordsize - unsigned y) - 1)).
Proof.
- intros. rewrite shru_rolm; auto. rewrite shl_rolm; auto. rewrite rolm_rolm.
- rewrite shru_shl_and_1. rewrite shru_shl_and_2.
- apply rolm_zero.
- exact (ltu_inv _ _ H). exact (ltu_inv _ _ H).
+ intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize. intros.
+ unfold and, bitwise_binop, shl, shru.
+ decEq. apply Z_of_bits_exten. intros.
+ repeat rewrite unsigned_repr.
+ rewrite bits_of_Z_two_p.
+ destruct (zlt (z + unsigned y) (Z_of_nat wordsize)).
+ rewrite bits_of_Z_of_bits. unfold proj_sumbool. rewrite zlt_true.
+ rewrite andb_true_r. f_equal. omega.
+ omega. omega.
+ rewrite bits_of_Z_above. unfold proj_sumbool. rewrite zlt_false. rewrite andb_false_r; auto.
+ omega. omega. omega. auto.
+ apply two_p_m1_range. omega.
+ apply Z_of_bits_range_2.
Qed.
(** ** Relation between shifts and powers of 2 *)
@@ -1815,18 +1885,15 @@ Proof.
intros. injection H0; intro; subst logn; clear H0.
assert (0 <= z < Z_of_nat wordsize).
apply H. auto with coqlib.
- rewrite unsigned_repr. auto.
- assert (Z_of_nat wordsize < max_unsigned). compute. auto.
- omega.
+ rewrite unsigned_repr. auto. generalize wordsize_max_unsigned; omega.
intros; discriminate.
Qed.
Theorem is_power2_range:
forall n logn,
- is_power2 n = Some logn -> ltu logn (repr (Z_of_nat wordsize)) = true.
+ is_power2 n = Some logn -> ltu logn iwordsize = true.
Proof.
- intros. unfold ltu.
- change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+ intros. unfold ltu. rewrite unsigned_repr_wordsize.
generalize (is_power2_rng _ _ H).
case (zlt (unsigned logn) (Z_of_nat wordsize)); intros.
auto. omegaContradiction.
@@ -1845,9 +1912,9 @@ Proof.
destruct l.
intros. simpl in H0. injection H1; intros; subst logn; clear H1.
rewrite unsigned_repr. replace (two_p z) with (two_p z + 0).
- auto. omega. elim (H z); intros.
- assert (Z_of_nat wordsize < max_unsigned). compute; auto.
- omega. auto with coqlib.
+ auto. omega. elim (H z); intros.
+ generalize wordsize_max_unsigned; omega.
+ auto with coqlib.
intros; discriminate.
Qed.
@@ -1858,8 +1925,8 @@ Remark two_p_range:
Proof.
intros. split.
assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega.
- assert (two_p n <= two_p (Z_of_nat wordsize - 1)). apply two_p_monotone. omega.
- eapply Zle_trans. eauto. vm_compute. congruence.
+ generalize (two_p_monotone_strict _ _ H). rewrite <- two_power_nat_two_p.
+ unfold max_unsigned, modulus. omega.
Qed.
Remark Z_one_bits_zero:
@@ -2072,11 +2139,10 @@ Theorem shrx_shr:
forall x y,
ltu y (repr (Z_of_nat wordsize - 1)) = true ->
shrx x y =
- shr (if lt x Int.zero then add x (sub (shl one y) one) else x) y.
+ shr (if lt x zero then add x (sub (shl one y) one) else x) y.
Proof.
intros. unfold shrx, divs, shr. decEq.
- exploit ltu_inv; eauto.
- change (unsigned (repr (Z_of_nat wordsize - 1))) with (Z_of_nat wordsize - 1).
+ exploit ltu_inv; eauto. rewrite unsigned_repr.
set (uy := unsigned y).
intro RANGE.
assert (shl one y = repr (two_p uy)).
@@ -2085,34 +2151,30 @@ Proof.
apply is_power2_two_p. omega. unfold uy. apply repr_unsigned.
rewrite mul_commut. apply mul_one.
assert (two_p uy > 0). apply two_p_gt_ZERO. omega.
- assert (two_p uy <= two_p (Z_of_nat wordsize - 2)).
- apply two_p_monotone. omega.
+ assert (two_p uy < half_modulus).
+ rewrite half_modulus_power.
+ apply two_p_monotone_strict. auto.
+ assert (two_p uy < modulus).
+ rewrite modulus_power. apply two_p_monotone_strict. omega.
assert (unsigned (shl one y) = two_p uy).
- rewrite H0. apply unsigned_repr.
- assert (two_p (Z_of_nat wordsize - 2) < max_unsigned). vm_compute; auto.
- omega.
+ rewrite H0. apply unsigned_repr. unfold max_unsigned. omega.
assert (signed (shl one y) = two_p uy).
- rewrite H0. apply signed_repr.
- split. apply Zle_trans with 0. vm_compute; congruence. omega.
- apply Zle_trans with (two_p (Z_of_nat wordsize - 2)). auto.
- vm_compute; congruence.
- rewrite H4.
+ rewrite H0. apply signed_repr.
+ unfold max_signed. generalize min_signed_neg. omega.
+ rewrite H5.
rewrite Zdiv_round_Zdiv; auto.
- unfold lt. change (signed zero) with 0.
+ unfold lt. rewrite signed_zero.
destruct (zlt (signed x) 0); auto.
rewrite add_signed.
assert (signed (sub (shl one y) one) = two_p uy - 1).
- unfold sub. rewrite H3. change (unsigned one) with 1.
- apply signed_repr.
- split. apply Zle_trans with 0. vm_compute; congruence. omega.
- apply Zle_trans with (two_p (Z_of_nat wordsize - 2)). omega.
- vm_compute; congruence.
- rewrite H5. rewrite signed_repr. decEq. omega.
- generalize (signed_range x). intros.
- assert (two_p uy - 1 <= max_signed).
- apply Zle_trans with (two_p (Z_of_nat wordsize - 2)). omega.
- vm_compute; congruence.
+ unfold sub. rewrite H4. rewrite unsigned_one.
+ apply signed_repr.
+ generalize min_signed_neg. unfold max_signed. omega.
+ rewrite H6. rewrite signed_repr. decEq. omega.
+ generalize (signed_range x). intros.
+ assert (two_p uy - 1 <= max_signed). unfold max_signed. omega.
omega.
+ generalize wordsize_pos wordsize_max_unsigned; omega.
Qed.
Lemma add_and:
@@ -2140,36 +2202,64 @@ Proof.
rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits; auto.
Qed.
-Remark modu_and_masks_1:
- forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
- rol (shru mone logn) logn = shl mone logn.
+Lemma Z_of_bits_zero:
+ forall n f,
+ (forall i, i >= 0 -> f i = false) ->
+ Z_of_bits n f = 0.
Proof.
- apply (equal_on_range
- (fun l => rol (shru mone l) l)
- (fun l => shl mone l)).
- vm_compute; auto.
+ induction n; intros; simpl.
+ auto.
+ rewrite H. rewrite IHn. auto. intros. apply H. omega. omega.
Qed.
-Remark modu_and_masks_2:
- forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
- and (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = zero.
+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.
Proof.
- apply (equal_on_range
- (fun l => and (shl mone l)
- (sub (repr (two_p (unsigned l))) one))
- (fun l => zero)).
- vm_compute; auto.
-Qed.
-
-Remark modu_and_masks_3:
- forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
- or (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = mone.
+ induction n; intros.
+ simpl. assert (two_p k > 0). apply two_p_gt_ZERO; omega. omega.
+ destruct (zeq k 0). subst k.
+ change (two_p 0) with 1. rewrite Z_of_bits_zero. omega. auto.
+ simpl. replace (two_p k) with (2 * two_p (k - 1)).
+ assert (0 <= Z_of_bits n (fun i => f(i+1)) < two_p (k - 1)).
+ apply IHn. intros. apply H. omega. omega.
+ unfold Z_shift_add. destruct (f 0); omega.
+ rewrite <- two_p_S. decEq. omega. omega.
+Qed.
+
+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.
+Proof.
+ induction n; intros.
+ simpl. exists 0; omega.
+ destruct (zeq k 0). subst k.
+ exists (Z_of_bits (S n) f1 - Z_of_bits (S n) f2).
+ change (two_p 0) with 1. omega.
+ destruct (IHn (fun i => f1 (i + 1)) (fun i => f2 (i + 1)) (k - 1)) as [q EQ].
+ intros. apply H. omega. omega.
+ exists q. simpl. rewrite H. unfold Z_shift_add.
+ replace (two_p k) with (2 * two_p (k - 1)). rewrite EQ.
+ destruct (f1 0). ring. ring.
+ rewrite <- two_p_S. decEq. omega. omega. omega.
+Qed.
+
+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).
Proof.
- apply (equal_on_range
- (fun l => or (shl mone l)
- (sub (repr (two_p (unsigned l))) one))
- (fun l => mone)).
- vm_compute; auto.
+ intros.
+ set (g := fun i : Z => if zlt i k then f i else false).
+ destruct (Z_of_bits_trunc_2 n f g k).
+ intros. unfold g. apply zlt_true. auto.
+ auto.
+ apply Zmod_unique with x. auto.
+ apply Z_of_bits_trunc_1. intros. unfold g. apply zlt_false. auto. auto.
Qed.
Theorem modu_and:
@@ -2179,42 +2269,23 @@ Theorem modu_and:
Proof.
intros. generalize (is_power2_correct _ _ H); intro.
generalize (is_power2_rng _ _ H); intro.
- assert (n <> zero).
- red; intro. subst n. change (unsigned zero) with 0 in H0.
- assert (two_p (unsigned logn) > 0). apply two_p_gt_ZERO. omega.
- omegaContradiction.
- generalize (modu_divu_Euclid x n H2); intro.
- assert (forall a b c, add a b = add a c -> b = c).
- intros. assert (sub (add a b) a = sub (add a c) a). congruence.
- repeat rewrite sub_add_l in H5. repeat rewrite sub_idem in H5.
- rewrite add_commut in H5; rewrite add_zero in H5.
- rewrite add_commut in H5; rewrite add_zero in H5.
- auto.
- apply H4 with (mul (divu x n) n).
- rewrite <- H3.
- rewrite (divu_pow2 x n logn H).
- rewrite (mul_pow2 (shru x logn) n logn H).
- rewrite shru_rolm. rewrite shl_rolm. rewrite rolm_rolm.
- rewrite sub_add_opp. rewrite add_assoc.
- replace (add (neg logn) logn) with zero.
- rewrite add_zero.
- change (modu (repr (Z_of_nat wordsize)) (repr (Z_of_nat wordsize)))
- with zero.
- rewrite rolm_zero.
- symmetry.
- replace n with (repr (two_p (unsigned logn))).
- rewrite modu_and_masks_1; auto.
- rewrite and_idem.
- rewrite add_and. rewrite modu_and_masks_3; auto. apply and_mone.
- apply modu_and_masks_2; auto.
- transitivity (repr (unsigned n)). decEq. auto. auto with ints.
- rewrite add_commut. rewrite add_neg_zero. auto.
- unfold ltu. apply zlt_true.
- change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
- omega.
- unfold ltu. apply zlt_true.
- change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+ unfold modu, and, bitwise_binop.
+ decEq.
+ set (ux := unsigned x).
+ replace ux with (Z_of_bits wordsize (bits_of_Z wordsize ux)).
+ rewrite H0. rewrite Z_of_bits_trunc_3. apply Z_of_bits_exten. intros.
+ rewrite bits_of_Z_of_bits; auto.
+ replace (unsigned (sub n one)) with (two_p (unsigned logn) - 1).
+ rewrite bits_of_Z_two_p. unfold proj_sumbool.
+ destruct (zlt z (unsigned logn)). rewrite andb_true_r; auto. rewrite andb_false_r; auto.
+ omega. auto.
+ rewrite <- H0. unfold sub. symmetry. rewrite unsigned_one. apply unsigned_repr.
+ rewrite H0.
+ assert (two_p (unsigned logn) > 0). apply two_p_gt_ZERO. omega.
+ generalize (two_p_range _ H1). omega.
omega.
+ apply eqm_small_eq. apply Z_of_bits_of_Z. apply Z_of_bits_range.
+ unfold ux. apply unsigned_range.
Qed.
(** ** Properties of integer zero extension and sign extension. *)
@@ -2234,10 +2305,11 @@ Proof. apply two_p_range. omega. Qed.
Remark two_p_n_range':
two_p n <= max_signed + 1.
-Proof.
+Proof.
+ unfold max_signed. rewrite half_modulus_power.
assert (two_p n <= two_p (Z_of_nat wordsize - 1)).
apply two_p_monotone. omega.
- exact H.
+ omega.
Qed.
Remark unsigned_repr_two_p:
@@ -2254,7 +2326,8 @@ Proof.
apply is_power2_two_p. omega.
generalize (modu_and x _ _ H).
unfold modu. rewrite unsigned_repr_two_p. intro. rewrite H0.
- decEq. unfold sub. decEq. rewrite unsigned_repr_two_p. reflexivity.
+ decEq. unfold sub. decEq. rewrite unsigned_repr_two_p.
+ rewrite unsigned_one. reflexivity.
Qed.
Theorem zero_ext_idem:
@@ -2389,8 +2462,7 @@ Theorem sign_ext_shr_shl:
Proof.
intros.
assert (unsigned y = Z_of_nat wordsize - n).
- unfold y. apply unsigned_repr.
- assert (Z_of_nat wordsize < max_unsigned). vm_compute; auto. omega.
+ unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega.
apply sign_ext_charact.
(* inequalities *)
unfold shr. rewrite H.
@@ -2404,16 +2476,18 @@ Proof.
with (- (two_p (n-1) * two_p (Z_of_nat wordsize - n))) by ring.
rewrite <- two_p_is_exp.
replace (n - 1 + (Z_of_nat wordsize - n)) with (Z_of_nat wordsize - 1) by omega.
- change (min_signed <= z < max_signed + 1).
- generalize (signed_range (shl x y)). unfold z. omega.
+ rewrite <- half_modulus_power.
+ generalize (signed_range (shl x y)). unfold z, min_signed, max_signed. omega.
omega. omega.
- apply Zdiv_interval_2. unfold z. apply signed_range.
- vm_compute; congruence. vm_compute; auto. apply two_p_gt_ZERO; omega.
+ apply Zdiv_interval_2. unfold z. apply signed_range.
+ generalize min_signed_neg; omega. generalize max_signed_pos; omega.
+ apply two_p_gt_ZERO; omega.
(* eqmod *)
unfold shr. rewrite H.
apply eqmod_trans with (signed (shl x y) / two_p (Z_of_nat wordsize - n)).
apply eqmod_mult_div. omega. omega.
replace (Z_of_nat wordsize - n + n) with (Z_of_nat wordsize) by omega.
+ rewrite <- two_power_nat_two_p.
change (eqm (two_p (Z_of_nat wordsize - n) * unsigned x) (signed (shl x y))).
rewrite shl_mul_two_p. unfold mul. rewrite H.
apply eqm_sym. eapply eqm_trans. apply eqm_signed_unsigned.
@@ -2430,14 +2504,11 @@ Theorem zero_ext_shru_shl:
Proof.
intros.
assert (unsigned y = Z_of_nat wordsize - n).
- unfold y. apply unsigned_repr.
- assert (Z_of_nat wordsize < max_unsigned). vm_compute; auto.
- omega.
+ unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega.
rewrite zero_ext_and. symmetry.
replace n with (Z_of_nat wordsize - unsigned y).
apply shru_shl_and. unfold ltu. apply zlt_true.
- rewrite H. change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize). omega.
- omega.
+ rewrite H. rewrite unsigned_repr_wordsize. omega. omega.
Qed.
End EXTENSIONS.
@@ -2447,14 +2518,14 @@ End EXTENSIONS.
Opaque Z_one_bits. (* Otherwise, next Qed blows up! *)
Theorem one_bits_range:
- forall x i, In i (one_bits x) -> ltu i (repr (Z_of_nat wordsize)) = true.
+ forall x i, In i (one_bits x) -> ltu i iwordsize = true.
Proof.
intros. unfold one_bits in H.
elim (list_in_map_inv _ _ _ H). intros i0 [EQ IN].
- subst i. unfold ltu. apply zlt_true.
+ subst i. unfold ltu. unfold iwordsize. apply zlt_true.
generalize (Z_one_bits_range _ _ IN). intros.
assert (0 <= Z_of_nat wordsize <= max_unsigned).
- compute. intuition congruence.
+ generalize wordsize_pos wordsize_max_unsigned; omega.
repeat rewrite unsigned_repr; omega.
Qed.
@@ -2481,8 +2552,7 @@ Proof.
apply eqm_add. rewrite shl_mul_two_p. rewrite mul_commut.
rewrite mul_one. apply eqm_unsigned_repr_r.
rewrite unsigned_repr. auto with ints.
- generalize (H a (in_eq _ _)).
- assert (Z_of_nat wordsize < max_unsigned). compute; auto. omega.
+ generalize (H a (in_eq _ _)). generalize wordsize_max_unsigned. omega.
auto with ints.
intros; apply H; auto with coqlib.
Qed.
@@ -2555,7 +2625,7 @@ Theorem notbool_isfalse_istrue:
forall x, is_false x -> is_true (notbool x).
Proof.
unfold is_false, is_true, notbool; intros; subst x.
- simpl. discriminate.
+ simpl. apply one_not_zero.
Qed.
Theorem notbool_istrue_isfalse:
@@ -2571,19 +2641,20 @@ Theorem shru_lt_zero:
shru x (repr (Z_of_nat wordsize - 1)) = if lt x zero then one else zero.
Proof.
intros. rewrite shru_div_two_p.
- change (two_p (unsigned (repr (Z_of_nat wordsize - 1))))
+ replace (two_p (unsigned (repr (Z_of_nat wordsize - 1))))
with half_modulus.
generalize (unsigned_range x); intro.
- unfold lt. change (signed zero) with 0. unfold signed.
+ unfold lt. rewrite signed_zero. unfold signed.
destruct (zlt (unsigned x) half_modulus).
rewrite zlt_false.
replace (unsigned x / half_modulus) with 0. reflexivity.
symmetry. apply Zdiv_unique with (unsigned x). ring. omega. omega.
rewrite zlt_true.
replace (unsigned x / half_modulus) with 1. reflexivity.
- symmetry. apply Zdiv_unique with (unsigned x - half_modulus). ring.
- replace modulus with (2 * half_modulus) in H. omega. reflexivity.
- omega.
+ symmetry. apply Zdiv_unique with (unsigned x - half_modulus). ring.
+ rewrite half_modulus_modulus in H. omega. omega.
+ rewrite unsigned_repr. apply half_modulus_power.
+ generalize wordsize_pos wordsize_max_unsigned; omega.
Qed.
Theorem ltu_range_test:
@@ -2592,9 +2663,30 @@ Theorem ltu_range_test:
0 <= signed x < unsigned y.
Proof.
intros.
- unfold Int.ltu in H. destruct (zlt (unsigned x) (unsigned y)); try discriminate.
+ unfold ltu in H. destruct (zlt (unsigned x) (unsigned y)); try discriminate.
rewrite signed_eq_unsigned.
generalize (unsigned_range x). omega. omega.
Qed.
-End Int.
+End Make.
+
+(** * Specialization to 32-bit integers. *)
+
+Module IntWordsize.
+ Definition wordsize := 32%nat.
+ Remark wordsize_not_zero: wordsize <> 0%nat.
+ Proof. unfold wordsize; congruence. Qed.
+End IntWordsize.
+
+Module Int := Make(IntWordsize).
+
+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.
+
+
+
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 1582b414614d1b188ccb7e8bc81ab55229aacea0..60c3d34d6352b3fb600eb68fc32c95895da22c91 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -302,9 +302,7 @@ lbl: .long 0x43300000, 0x00000000
lwz r12, lo16(lbl)(r12)
mtctr r12
bctr r12
- .const_data
lbl: .long table[0], table[1], ...
- .text
>>
Note that [reg] contains 4 times the index of the desired table entry.
*)
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 3baeb795650348d822bfa7dfee995cb7f4be2964..7329e53937ed690669004db03167cb92b6559b3e 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -48,13 +48,13 @@ Proof.
intros. unfold high_u, low_u.
rewrite Int.shl_rolm. rewrite Int.shru_rolm.
rewrite Int.rolm_rolm.
- change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat wordsize)) (Int.repr 16))
+ change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
(Int.repr 16))
- (Int.repr (Z_of_nat wordsize)))
+ (Int.repr (Z_of_nat Int.wordsize)))
with (Int.zero).
rewrite Int.rolm_zero. rewrite <- Int.and_or_distrib.
exact (Int.and_mone n).
- reflexivity. reflexivity.
+ apply int_wordsize_divides_modulus. reflexivity. reflexivity.
Qed.
Lemma low_high_u_xor:
@@ -63,13 +63,13 @@ Proof.
intros. unfold high_u, low_u.
rewrite Int.shl_rolm. rewrite Int.shru_rolm.
rewrite Int.rolm_rolm.
- change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat wordsize)) (Int.repr 16))
+ change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
(Int.repr 16))
- (Int.repr (Z_of_nat wordsize)))
+ (Int.repr (Z_of_nat Int.wordsize)))
with (Int.zero).
rewrite Int.rolm_zero. rewrite <- Int.and_xor_distrib.
exact (Int.and_mone n).
- reflexivity. reflexivity.
+ apply int_wordsize_divides_modulus. reflexivity. reflexivity.
Qed.
Lemma low_high_s:
@@ -91,7 +91,7 @@ Proof.
unfold Int.sub.
assert (forall a b, Int.eqm a b -> b mod 65536 = 0 -> a mod 65536 = 0).
intros a b [k EQ] H1. rewrite EQ.
- change modulus with (65536 * 65536).
+ change Int.modulus with (65536 * 65536).
rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto.
omega.
eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr.
diff --git a/powerpc/ConstpropOp.v b/powerpc/ConstpropOp.v
index 87b2cfa40a66fa9ceb6c85add2b27385e6fca39b..ededce079d1537ca2855bc6d99424ddfc4f75e4a 100644
--- a/powerpc/ConstpropOp.v
+++ b/powerpc/ConstpropOp.v
@@ -166,11 +166,11 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
| Onand, I n1 :: I n2 :: nil => I(Int.xor (Int.and n1 n2) Int.mone)
| Onor, I n1 :: I n2 :: nil => I(Int.xor (Int.or n1 n2) Int.mone)
| Onxor, I n1 :: I n2 :: nil => I(Int.xor (Int.xor n1 n2) Int.mone)
- | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown
- | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown
- | Oshrimm n, I n1 :: nil => if Int.ltu n (Int.repr 32) then I(Int.shr n1 n) else Unknown
- | Oshrximm n, I n1 :: nil => if Int.ltu n (Int.repr 32) then I(Int.shrx n1 n) else Unknown
- | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown
+ | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
+ | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
+ | Oshrimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown
+ | Oshrximm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shrx n1 n) else Unknown
+ | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
| Orolm amount mask, I n1 :: nil => I(Int.rolm n1 amount mask)
| Onegf, F n1 :: nil => F(Float.neg n1)
| Oabsf, F n1 :: nil => F(Float.abs n1)
@@ -500,15 +500,15 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
| eval_static_operation_case28 n1 n2 =>
I(Int.xor (Int.xor n1 n2) Int.mone)
| eval_static_operation_case29 n1 n2 =>
- if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown
+ if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
| eval_static_operation_case30 n1 n2 =>
- if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown
+ if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
| eval_static_operation_case31 n n1 =>
- if Int.ltu n (Int.repr 32) then I(Int.shr n1 n) else Unknown
+ if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown
| eval_static_operation_case32 n n1 =>
- if Int.ltu n (Int.repr 32) then I(Int.shrx n1 n) else Unknown
+ if Int.ltu n Int.iwordsize then I(Int.shrx n1 n) else Unknown
| eval_static_operation_case33 n1 n2 =>
- if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown
+ if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
| eval_static_operation_case34 amount mask n1 =>
I(Int.rolm n1 amount mask)
| eval_static_operation_case35 n1 =>
@@ -628,7 +628,7 @@ Definition make_shrimm (n: int) (r: reg) :=
Definition make_shruimm (n: int) (r: reg) :=
if Int.eq n Int.zero
then (Omove, r :: nil)
- else (Orolm (Int.sub (Int.repr 32) n) (Int.shru Int.mone n), r :: nil).
+ else (Orolm (Int.sub Int.iwordsize n) (Int.shru Int.mone n), r :: nil).
Definition make_mulimm (n: int) (r: reg) :=
if Int.eq n Int.zero then
@@ -789,7 +789,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
| op_strength_reduction_case9 r1 r2 => (* Oshl *)
match intval r2 with
| Some n =>
- if Int.ltu n (Int.repr 32)
+ if Int.ltu n Int.iwordsize
then make_shlimm n r1
else (op, args)
| _ => (op, args)
@@ -797,7 +797,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
| op_strength_reduction_case10 r1 r2 => (* Oshr *)
match intval r2 with
| Some n =>
- if Int.ltu n (Int.repr 32)
+ if Int.ltu n Int.iwordsize
then make_shrimm n r1
else (op, args)
| _ => (op, args)
@@ -805,7 +805,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
| op_strength_reduction_case11 r1 r2 => (* Oshru *)
match intval r2 with
| Some n =>
- if Int.ltu n (Int.repr 32)
+ if Int.ltu n Int.iwordsize
then make_shruimm n r1
else (op, args)
| _ => (op, args)
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 0c7be7bd2812162c3c8ebf081001d7287ab73cb8..2e28d23f1d81b14c259b8c38830fafd413fc06cb 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -130,19 +130,19 @@ Proof.
subst v. unfold Int.not. congruence.
subst v. unfold Int.not. congruence.
- replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)).
+ replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v. simpl. congruence. discriminate. congruence.
- replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)).
+ replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v. simpl. congruence. discriminate. congruence.
- destruct (Int.ltu n (Int.repr 32)).
+ destruct (Int.ltu n Int.iwordsize).
injection H0; intro; subst v. simpl. congruence. discriminate.
- destruct (Int.ltu n (Int.repr 32)).
+ destruct (Int.ltu n Int.iwordsize).
injection H0; intro; subst v. simpl. congruence. discriminate.
- replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)).
+ replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v. simpl. congruence. discriminate. congruence.
rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence.
@@ -229,7 +229,7 @@ Proof.
intros; unfold make_shlimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
subst n. simpl in *. FuncInv. rewrite Int.shl_zero in H. congruence.
- simpl in *. FuncInv. caseEq (Int.ltu n (Int.repr 32)); intros.
+ simpl in *. FuncInv. caseEq (Int.ltu n Int.iwordsize); intros.
rewrite H1 in H0. rewrite Int.shl_rolm in H0. auto. exact H1.
rewrite H1 in H0. discriminate.
Qed.
@@ -255,7 +255,7 @@ Proof.
intros; unfold make_shruimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
subst n. simpl in *. FuncInv. rewrite Int.shru_zero in H. congruence.
- simpl in *. FuncInv. caseEq (Int.ltu n (Int.repr 32)); intros.
+ simpl in *. FuncInv. caseEq (Int.ltu n Int.iwordsize); intros.
rewrite H1 in H0. rewrite Int.shru_rolm in H0. auto. exact H1.
rewrite H1 in H0. discriminate.
Qed.
@@ -276,7 +276,7 @@ Proof.
with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)).
apply make_shlimm_correct.
simpl. generalize (Int.is_power2_range _ _ H1).
- change (Z_of_nat wordsize) with 32. intro. rewrite H2.
+ change (Z_of_nat Int.wordsize) with 32. intro. rewrite H2.
destruct rs#r; auto. rewrite (Int.mul_pow2 i0 _ _ H1). auto.
exact H2.
Qed.
@@ -364,7 +364,7 @@ Proof.
caseEq (Int.is_power2 i); intros.
rewrite (intval_correct _ _ H) in H1.
simpl in *; FuncInv. destruct (Int.eq i Int.zero). congruence.
- change 32 with (Z_of_nat wordsize).
+ change 32 with (Z_of_nat Int.wordsize).
rewrite (Int.is_power2_range _ _ H0).
rewrite (Int.divs_pow2 i1 _ _ H0) in H1. auto.
assumption.
@@ -377,7 +377,7 @@ Proof.
with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)).
apply make_shruimm_correct.
simpl. destruct rs#r1; auto.
- change 32 with (Z_of_nat wordsize).
+ change 32 with (Z_of_nat Int.wordsize).
rewrite (Int.is_power2_range _ _ H0).
generalize (Int.eq_spec i Int.zero); case (Int.eq i Int.zero); intros.
subst i. discriminate.
@@ -416,19 +416,19 @@ Proof.
assumption.
(* Oshl *)
caseEq (intval app r2); intros.
- caseEq (Int.ltu i (Int.repr 32)); intros.
+ caseEq (Int.ltu i Int.iwordsize); intros.
rewrite (intval_correct _ _ H). apply make_shlimm_correct.
assumption.
assumption.
(* Oshr *)
caseEq (intval app r2); intros.
- caseEq (Int.ltu i (Int.repr 32)); intros.
+ caseEq (Int.ltu i Int.iwordsize); intros.
rewrite (intval_correct _ _ H). apply make_shrimm_correct.
assumption.
assumption.
(* Oshru *)
caseEq (intval app r2); intros.
- caseEq (Int.ltu i (Int.repr 32)); intros.
+ caseEq (Int.ltu i Int.iwordsize); intros.
rewrite (intval_correct _ _ H). apply make_shruimm_correct.
assumption.
assumption.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 27e12c2c7d4b5f2a4ce893e3d3c2b43248f99f05..c6e196f3e7fccef445cb1b9f7a5ed9bc72e524f6 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -224,15 +224,15 @@ Definition eval_operation
| Onor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.or n1 n2)))
| Onxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.xor n1 n2)))
| Oshl, Vint n1 :: Vint n2 :: nil =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None
| Oshr, Vint n1 :: Vint n2 :: nil =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
| Oshrimm n, Vint n1 :: nil =>
- if Int.ltu n (Int.repr 32) then Some (Vint (Int.shr n1 n)) else None
+ if Int.ltu n Int.iwordsize then Some (Vint (Int.shr n1 n)) else None
| Oshrximm n, Vint n1 :: nil =>
- if Int.ltu n (Int.repr 32) then Some (Vint (Int.shrx n1 n)) else None
+ if Int.ltu n Int.iwordsize then Some (Vint (Int.shrx n1 n)) else None
| Oshru, Vint n1 :: Vint n2 :: nil =>
- if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
+ if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
| Orolm amount mask, Vint n1 :: nil =>
Some (Vint (Int.rolm n1 amount mask))
| Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1))
@@ -522,15 +522,15 @@ Proof.
injection H0; intro; subst v; exact I.
destruct (Int.eq i0 Int.zero). discriminate.
injection H0; intro; subst v; exact I.
- destruct (Int.ltu i0 (Int.repr 32)).
+ destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v; exact I. discriminate.
- destruct (Int.ltu i0 (Int.repr 32)).
+ destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v; exact I. discriminate.
- destruct (Int.ltu i (Int.repr 32)).
+ destruct (Int.ltu i Int.iwordsize).
injection H0; intro; subst v; exact I. discriminate.
- destruct (Int.ltu i (Int.repr 32)).
+ destruct (Int.ltu i Int.iwordsize).
injection H0; intro; subst v; exact I. discriminate.
- destruct (Int.ltu i0 (Int.repr 32)).
+ destruct (Int.ltu i0 Int.iwordsize).
injection H0; intro; subst v; exact I. discriminate.
destruct v0; exact I.
destruct (eval_condition c vl).
@@ -694,11 +694,11 @@ Proof.
unfold eq_block in H. destruct (zeq b b0); congruence.
destruct (Int.eq i0 Int.zero); congruence.
destruct (Int.eq i0 Int.zero); congruence.
- destruct (Int.ltu i0 (Int.repr 32)); congruence.
- destruct (Int.ltu i0 (Int.repr 32)); congruence.
- destruct (Int.ltu i (Int.repr 32)); congruence.
- destruct (Int.ltu i (Int.repr 32)); congruence.
- destruct (Int.ltu i0 (Int.repr 32)); congruence.
+ destruct (Int.ltu i0 Int.iwordsize); congruence.
+ destruct (Int.ltu i0 Int.iwordsize); congruence.
+ destruct (Int.ltu i Int.iwordsize); congruence.
+ destruct (Int.ltu i Int.iwordsize); congruence.
+ destruct (Int.ltu i0 Int.iwordsize); congruence.
caseEq (eval_condition c vl); intros; rewrite H0 in H.
replace v with (Val.of_bool b).
eapply eval_condition_weaken; eauto.
@@ -797,11 +797,11 @@ Proof.
destruct (eq_block b b0); inv H0. TrivialExists.
destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
- destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists.
- destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists.
- destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists.
- destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists.
- destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists.
+ destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
+ destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
+ destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
+ destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
+ destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
caseEq (eval_condition c vl1); intros. rewrite H1 in H0.
rewrite (eval_condition_lessdef c H H1).
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v
index ef55b8bb229435b32664945ff6981a64115c379c..40201e77d5b1ed1d2534434389bbe974faf1facc 100644
--- a/powerpc/SelectOp.v
+++ b/powerpc/SelectOp.v
@@ -396,7 +396,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) :=
| rolm_case1 n1 =>
Eop (Ointconst(Int.and (Int.rol n1 amount2) mask2)) Enil
| rolm_case2 amount1 mask1 t1 =>
- let amount := Int.and (Int.add amount1 amount2) (Int.repr 31) in
+ let amount := Int.modu (Int.add amount1 amount2) Int.iwordsize in
let mask := Int.and (Int.rol mask1 amount2) mask2 in
if Int.is_rlw_mask mask
then Eop (Orolm amount mask) (t1:::Enil)
@@ -408,7 +408,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) :=
Definition shlimm (e1: expr) (n2: int) :=
if Int.eq n2 Int.zero then
e1
- else if Int.ltu n2 (Int.repr 32) then
+ else if Int.ltu n2 Int.iwordsize then
rolm e1 n2 (Int.shl Int.mone n2)
else
Eop Oshl (e1:::Eop (Ointconst n2) Enil:::Enil).
@@ -416,8 +416,8 @@ Definition shlimm (e1: expr) (n2: int) :=
Definition shruimm (e1: expr) (n2: int) :=
if Int.eq n2 Int.zero then
e1
- else if Int.ltu n2 (Int.repr 32) then
- rolm e1 (Int.sub (Int.repr 32) n2) (Int.shru Int.mone n2)
+ else if Int.ltu n2 Int.iwordsize then
+ rolm e1 (Int.sub Int.iwordsize n2) (Int.shru Int.mone n2)
else
Eop Oshru (e1:::Eop (Ointconst n2) Enil:::Enil).
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 77bca50456f9aa97b75388e8abf5e72d11dbf405..ae152b388f9b135798b86a63e778f6bc9cc9d70b 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -346,11 +346,7 @@ Proof.
case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)).
EvalOp. simpl. subst x.
decEq. decEq.
- replace (Int.and (Int.add amount1 amount) (Int.repr 31))
- with (Int.modu (Int.add amount1 amount) (Int.repr 32)).
- symmetry. apply Int.rolm_rolm.
- change (Int.repr 31) with (Int.sub (Int.repr 32) Int.one).
- apply Int.modu_and with (Int.repr 5). reflexivity.
+ symmetry. apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
EvalOp. econstructor. EvalOp. simpl. rewrite H. reflexivity. constructor. auto.
EvalOp.
Qed.
@@ -358,7 +354,7 @@ Qed.
Theorem eval_shlimm:
forall le a n x,
eval_expr ge sp e m le a (Vint x) ->
- Int.ltu n (Int.repr 32) = true ->
+ Int.ltu n Int.iwordsize = true ->
eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)).
Proof.
intros. unfold shlimm.
@@ -372,14 +368,14 @@ Qed.
Theorem eval_shruimm:
forall le a n x,
eval_expr ge sp e m le a (Vint x) ->
- Int.ltu n (Int.repr 32) = true ->
+ Int.ltu n Int.iwordsize = true ->
eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)).
Proof.
intros. unfold shruimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro.
subst n. rewrite Int.shru_zero. auto.
rewrite H0.
- replace (Int.shru x n) with (Int.rolm x (Int.sub (Int.repr 32) n) (Int.shru Int.mone n)).
+ replace (Int.shru x n) with (Int.rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n)).
apply eval_rolm. auto. symmetry. apply Int.shru_rolm. exact H0.
Qed.
@@ -391,7 +387,7 @@ Proof.
intros; unfold mulimm_base.
generalize (Int.one_bits_decomp n).
generalize (Int.one_bits_range n).
- change (Z_of_nat wordsize) with 32.
+ change (Z_of_nat Int.wordsize) with 32.
destruct (Int.one_bits n).
intros. EvalOp.
destruct l.
@@ -611,7 +607,7 @@ Theorem eval_shl:
forall le a x b y,
eval_expr ge sp e m le a (Vint x) ->
eval_expr ge sp e m le b (Vint y) ->
- Int.ltu y (Int.repr 32) = true ->
+ Int.ltu y Int.iwordsize = true ->
eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)).
Proof.
intros until y; unfold shl; case (shift_match b); intros.
@@ -623,7 +619,7 @@ Theorem eval_shru:
forall le a x b y,
eval_expr ge sp e m le a (Vint x) ->
eval_expr ge sp e m le b (Vint y) ->
- Int.ltu y (Int.repr 32) = true ->
+ Int.ltu y Int.iwordsize = true ->
eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)).
Proof.
intros until y; unfold shru; case (shift_match b); intros.
@@ -908,7 +904,7 @@ Theorem eval_shr:
forall le a x b y,
eval_expr ge sp e m le a (Vint x) ->
eval_expr ge sp e m le b (Vint y) ->
- Int.ltu y (Int.repr 32) = true ->
+ Int.ltu y Int.iwordsize = true ->
eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)).
Proof. intros; unfold shr; EvalOp. simpl. rewrite H1. auto. Qed.