summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backend/Cminor.v8
-rw-r--r--backend/Constprop.v16
-rw-r--r--backend/Op.v24
-rw-r--r--backend/PPC.v4
-rw-r--r--backend/PPCgen.v2
-rw-r--r--backend/PPCgenproof.v4
-rw-r--r--backend/PPCgenproof1.v15
-rw-r--r--backend/Selectionproof.v20
-rw-r--r--cfrontend/Cminorgenproof.v16
-rw-r--r--cfrontend/Csem.v8
-rw-r--r--common/Mem.v20
-rw-r--r--common/Values.v80
-rw-r--r--extraction/.depend12
-rw-r--r--lib/Coqlib.v86
-rw-r--r--lib/Integers.v896
15 files changed, 844 insertions, 367 deletions
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 910eaa4..b6186f2 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -230,10 +230,10 @@ Definition eval_constant (sp: val) (cst: constant) : option val :=
Definition eval_unop (op: unary_operation) (arg: val) : option val :=
match op, arg with
- | Ocast8unsigned, _ => Some (Val.cast8unsigned arg)
- | Ocast8signed, _ => Some (Val.cast8signed arg)
- | Ocast16unsigned, _ => Some (Val.cast16unsigned arg)
- | Ocast16signed, _ => Some (Val.cast16signed arg)
+ | Ocast8unsigned, _ => Some (Val.zero_ext 8 arg)
+ | Ocast8signed, _ => Some (Val.sign_ext 8 arg)
+ | Ocast16unsigned, _ => Some (Val.zero_ext 16 arg)
+ | Ocast16signed, _ => Some (Val.sign_ext 16 arg)
| Onegint, Vint n1 => Some (Vint (Int.neg n1))
| Onotbool, Vint n1 => Some (Val.of_bool (Int.eq n1 Int.zero))
| Onotbool, Vptr b1 n1 => Some Vfalse
diff --git a/backend/Constprop.v b/backend/Constprop.v
index e7feb10..75fb148 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -219,10 +219,10 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
| Ointconst n, nil => I n
| Ofloatconst n, nil => F n
| Oaddrsymbol s n, nil => S s n
- | Ocast8signed, I n1 :: nil => I(Int.cast8signed n)
- | Ocast8unsigned, I n1 :: nil => I(Int.cast8unsigned n)
- | Ocast16signed, I n1 :: nil => I(Int.cast16signed n)
- | Ocast16unsigned, I n1 :: nil => I(Int.cast16unsigned n)
+ | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n)
+ | Ocast8unsigned, I n1 :: nil => I(Int.zero_ext 8 n)
+ | Ocast16signed, I n1 :: nil => I(Int.sign_ext 16 n)
+ | Ocast16unsigned, I n1 :: nil => I(Int.zero_ext 16 n)
| Oadd, I n1 :: I n2 :: nil => I(Int.add n1 n2)
| Oadd, S s1 n1 :: I n2 :: nil => S s1 (Int.add n1 n2)
| Oaddimm n, I n1 :: nil => I (Int.add n1 n)
@@ -533,9 +533,9 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
| eval_static_operation_case4 s n =>
S s n
| eval_static_operation_case6 n1 =>
- I(Int.cast8signed n1)
+ I(Int.sign_ext 8 n1)
| eval_static_operation_case7 n1 =>
- I(Int.cast16signed n1)
+ I(Int.sign_ext 16 n1)
| eval_static_operation_case8 n1 n2 =>
I(Int.add n1 n2)
| eval_static_operation_case9 s1 n1 n2 =>
@@ -618,9 +618,9 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
| Some b => I(if b then Int.one else Int.zero)
end
| eval_static_operation_case48 n1 =>
- I(Int.cast8unsigned n1)
+ I(Int.zero_ext 8 n1)
| eval_static_operation_case49 n1 =>
- I(Int.cast16unsigned n1)
+ I(Int.zero_ext 16 n1)
| eval_static_operation_case50 n1 =>
I(Float.intuoffloat n1)
| eval_static_operation_default op vl =>
diff --git a/backend/Op.v b/backend/Op.v
index 707bcb0..5665d72 100644
--- a/backend/Op.v
+++ b/backend/Op.v
@@ -175,10 +175,10 @@ Definition eval_operation
| Some b => Some (Vptr b ofs)
end
| Oaddrstack ofs, nil => offset_sp sp ofs
- | Ocast8signed, v1 :: nil => Some (Val.cast8signed v1)
- | Ocast8unsigned, v1 :: nil => Some (Val.cast8unsigned v1)
- | Ocast16signed, v1 :: nil => Some (Val.cast16signed v1)
- | Ocast16unsigned, v1 :: nil => Some (Val.cast16unsigned v1)
+ | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
+ | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1)
+ | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
+ | Ocast16unsigned, v1 :: nil => Some (Val.zero_ext 16 v1)
| Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2))
| Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1))
| Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2))
@@ -632,10 +632,10 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :
| Ofloatconst n, nil => Vfloat n
| Oaddrsymbol s ofs, nil => find_symbol_offset s ofs
| Oaddrstack ofs, nil => Val.add sp (Vint ofs)
- | Ocast8signed, v1::nil => Val.cast8signed v1
- | Ocast8unsigned, v1::nil => Val.cast8unsigned v1
- | Ocast16signed, v1::nil => Val.cast16signed v1
- | Ocast16unsigned, v1::nil => Val.cast16unsigned v1
+ | Ocast8signed, v1::nil => Val.sign_ext 8 v1
+ | Ocast8unsigned, v1::nil => Val.zero_ext 8 v1
+ | Ocast16signed, v1::nil => Val.sign_ext 16 v1
+ | Ocast16unsigned, v1::nil => Val.zero_ext 16 v1
| Oadd, v1::v2::nil => Val.add v1 v2
| Oaddimm n, v1::nil => Val.add v1 (Vint n)
| Osub, v1::v2::nil => Val.sub v1 v2
@@ -843,10 +843,10 @@ Proof.
exists v2; auto.
destruct (Genv.find_symbol genv i); inv H0. TrivialExists.
exists v1; auto.
- exists (Val.cast8signed v2); split. auto. apply Val.cast8signed_lessdef; auto.
- exists (Val.cast8unsigned v2); split. auto. apply Val.cast8unsigned_lessdef; auto.
- exists (Val.cast16signed v2); split. auto. apply Val.cast16signed_lessdef; auto.
- exists (Val.cast16unsigned v2); split. auto. apply Val.cast16unsigned_lessdef; auto.
+ exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto.
+ exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto.
+ exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto.
+ exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto.
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.
diff --git a/backend/PPC.v b/backend/PPC.v
index 13c7a87..e47cba0 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -616,9 +616,9 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| Peqv rd r1 r2 =>
OK (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m
| Pextsb rd r1 =>
- OK (nextinstr (rs#rd <- (Val.cast8signed rs#r1))) m
+ OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m
| Pextsh rd r1 =>
- OK (nextinstr (rs#rd <- (Val.cast16signed rs#r1))) m
+ OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m
| Pfreeframe ofs =>
match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with
| None => Error
diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index 1484a1e..faedcb1 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -80,7 +80,7 @@ Definition freg_of (r: mreg) : freg :=
Definition low_u (n: int) := Int.and n (Int.repr 65535).
Definition high_u (n: int) := Int.shru n (Int.repr 16).
-Definition low_s (n: int) := Int.cast16signed n.
+Definition low_s (n: int) := Int.sign_ext 16 n.
Definition high_s (n: int) := Int.shru (Int.sub n (low_s n)) (Int.repr 16).
(** Smart constructors for arithmetic operations involving
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v
index fd5843b..6db8b47 100644
--- a/backend/PPCgenproof.v
+++ b/backend/PPCgenproof.v
@@ -567,14 +567,14 @@ Qed.
Lemma loadv_8_signed_unsigned:
forall m a,
Mem.loadv Mint8signed m a =
- option_map Val.cast8signed (Mem.loadv Mint8unsigned m a).
+ option_map (Val.sign_ext 8) (Mem.loadv Mint8unsigned m a).
Proof.
intros. unfold Mem.loadv. destruct a; try reflexivity.
unfold load. rewrite (in_bounds_equiv Mint8signed Mint8unsigned).
destruct (in_bounds m Mint8unsigned b (Int.signed i)); auto.
simpl.
destruct (getN 0 (Int.signed i) (contents (blocks m b))); auto.
- simpl. rewrite Int.cast8_signed_unsigned. auto.
+ simpl. rewrite Int.sign_ext_zero_ext. auto. compute; auto.
auto.
Qed.
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v
index ba347ea..dd142c5 100644
--- a/backend/PPCgenproof1.v
+++ b/backend/PPCgenproof1.v
@@ -95,7 +95,8 @@ Proof.
rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto.
omega.
eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr.
- unfold low_s. unfold Int.cast16signed.
+ unfold low_s. unfold Int.sign_ext.
+ change (two_p 16) with 65536. change (two_p (16-1)) with 32768.
set (N := Int.unsigned n).
case (zlt (N mod 65536) 32768); intro.
apply H0 with (N - N mod 65536). auto with ints.
@@ -1273,19 +1274,19 @@ Proof.
(* Ocast8unsigned *)
exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 255)))).
split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity.
- replace (Val.cast8unsigned (ms m0))
+ replace (Val.zero_ext 8 (ms m0))
with (Val.rolm (ms m0) Int.zero (Int.repr 255)).
auto with ppcgen.
- unfold Val.rolm, Val.cast8unsigned. destruct (ms m0); auto.
- rewrite Int.rolm_zero. rewrite Int.cast8unsigned_and. auto.
+ unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto.
+ rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
(* Ocast16unsigned *)
exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 65535)))).
split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity.
- replace (Val.cast16unsigned (ms m0))
+ replace (Val.zero_ext 16 (ms m0))
with (Val.rolm (ms m0) Int.zero (Int.repr 65535)).
auto with ppcgen.
- unfold Val.rolm, Val.cast16unsigned. destruct (ms m0); auto.
- rewrite Int.rolm_zero. rewrite Int.cast16unsigned_and. auto.
+ unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto.
+ rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
(* Oaddimm *)
generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m
(ireg_of_not_GPR12 m0)).
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index b779488..6d62979 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -748,40 +748,44 @@ Qed.
Theorem eval_cast8signed:
forall le a v,
eval_expr ge sp e m le a v ->
- eval_expr ge sp e m le (cast8signed a) (Val.cast8signed v).
+ eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v).
Proof.
intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval.
- EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_signed_idem. reflexivity.
+ EvalOp. simpl. subst v. destruct v1; simpl; auto.
+ rewrite Int.sign_ext_idem. reflexivity. compute; auto.
EvalOp.
Qed.
Theorem eval_cast8unsigned:
forall le a v,
eval_expr ge sp e m le a v ->
- eval_expr ge sp e m le (cast8unsigned a) (Val.cast8unsigned v).
+ eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v).
Proof.
intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval.
- EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_unsigned_idem. reflexivity.
+ EvalOp. simpl. subst v. destruct v1; simpl; auto.
+ rewrite Int.zero_ext_idem. reflexivity. compute; auto.
EvalOp.
Qed.
Theorem eval_cast16signed:
forall le a v,
eval_expr ge sp e m le a v ->
- eval_expr ge sp e m le (cast16signed a) (Val.cast16signed v).
+ eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v).
Proof.
intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval.
- EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_signed_idem. reflexivity.
+ EvalOp. simpl. subst v. destruct v1; simpl; auto.
+ rewrite Int.sign_ext_idem. reflexivity. compute; auto.
EvalOp.
Qed.
Theorem eval_cast16unsigned:
forall le a v,
eval_expr ge sp e m le a v ->
- eval_expr ge sp e m le (cast16unsigned a) (Val.cast16unsigned v).
+ eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v).
Proof.
intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval.
- EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_unsigned_idem. reflexivity.
+ EvalOp. simpl. subst v. destruct v1; simpl; auto.
+ rewrite Int.zero_ext_idem. reflexivity. compute; auto.
EvalOp.
Qed.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9dfb573..e1224bd 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -962,16 +962,16 @@ Lemma make_cast_correct:
Proof.
intros. destruct chunk; simpl make_cast.
- exists (Val.cast8signed tv).
+ exists (Val.sign_ext 8 tv).
split. eauto with evalexpr. inversion H0; simpl; constructor.
- exists (Val.cast8unsigned tv).
+ exists (Val.zero_ext 8 tv).
split. eauto with evalexpr. inversion H0; simpl; constructor.
- exists (Val.cast16signed tv).
+ exists (Val.sign_ext 16 tv).
split. eauto with evalexpr. inversion H0; simpl; constructor.
- exists (Val.cast16unsigned tv).
+ exists (Val.zero_ext 16 tv).
split. eauto with evalexpr. inversion H0; simpl; constructor.
exists tv.
@@ -1025,10 +1025,10 @@ Proof.
inv H; simpl in H6; inv H6;
econstructor; (split; [eauto|idtac]);
destruct v1; simpl in H0; inv H0; try (constructor; constructor).
- apply val_content_inject_8. auto. apply Int.cast8_unsigned_idem.
- apply val_content_inject_8; auto. apply Int.cast8_unsigned_signed.
- apply val_content_inject_16; auto. apply Int.cast16_unsigned_idem.
- apply val_content_inject_16; auto. apply Int.cast16_unsigned_signed.
+ apply val_content_inject_8. auto. apply Int.zero_ext_idem. compute; auto.
+ apply val_content_inject_8; auto. apply Int.zero_ext_sign_ext. compute; auto.
+ apply val_content_inject_16; auto. apply Int.zero_ext_idem. compute; auto.
+ apply val_content_inject_16; auto. apply Int.zero_ext_sign_ext. compute; auto.
apply val_content_inject_32. apply Float.singleoffloat_idem.
Qed.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 2213912..14b8053 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -351,10 +351,10 @@ Definition sem_binary_operation
Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
match sz, sg with
- | I8, Signed => Int.cast8signed i
- | I8, Unsigned => Int.cast8unsigned i
- | I16, Signed => Int.cast16signed i
- | I16, Unsigned => Int.cast16unsigned i
+ | I8, Signed => Int.sign_ext 8 i
+ | I8, Unsigned => Int.zero_ext 8 i
+ | I16, Signed => Int.sign_ext 16 i
+ | I16, Unsigned => Int.zero_ext 16 i
| I32 , _ => i
end.
diff --git a/common/Mem.v b/common/Mem.v
index 35d93ed..3db2ceb 100644
--- a/common/Mem.v
+++ b/common/Mem.v
@@ -1932,12 +1932,12 @@ Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop :=
| val_content_inject_8:
forall chunk n1 n2,
chunk = Mint8unsigned \/ chunk = Mint8signed ->
- Int.cast8unsigned n1 = Int.cast8unsigned n2 ->
+ Int.zero_ext 8 n1 = Int.zero_ext 8 n2 ->
val_content_inject f chunk (Vint n1) (Vint n2)
| val_content_inject_16:
forall chunk n1 n2,
chunk = Mint16unsigned \/ chunk = Mint16signed ->
- Int.cast16unsigned n1 = Int.cast16unsigned n2 ->
+ Int.zero_ext 16 n1 = Int.zero_ext 16 n2 ->
val_content_inject f chunk (Vint n1) (Vint n2)
| val_content_inject_32:
forall f1 f2,
@@ -1957,20 +1957,20 @@ Proof.
elim H1; intro; subst chunk;
destruct chunk'; simpl in H0; try discriminate; simpl.
- replace (Int.cast8signed n1) with (Int.cast8signed n2).
- constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto.
+ replace (Int.sign_ext 8 n1) with (Int.sign_ext 8 n2).
+ constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto.
rewrite H2. constructor.
- replace (Int.cast8signed n1) with (Int.cast8signed n2).
- constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto.
+ replace (Int.sign_ext 8 n1) with (Int.sign_ext 8 n2).
+ constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto.
rewrite H2. constructor.
elim H1; intro; subst chunk;
destruct chunk'; simpl in H0; try discriminate; simpl.
- replace (Int.cast16signed n1) with (Int.cast16signed n2).
- constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto.
+ replace (Int.sign_ext 16 n1) with (Int.sign_ext 16 n2).
+ constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto.
rewrite H2. constructor.
- replace (Int.cast16signed n1) with (Int.cast16signed n2).
- constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto.
+ replace (Int.sign_ext 16 n1) with (Int.sign_ext 16 n2).
+ constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto.
rewrite H2. constructor.
destruct chunk'; simpl in H0; try discriminate; simpl.
diff --git a/common/Values.v b/common/Values.v
index 1977244..27d4f50 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -150,27 +150,15 @@ Definition notbool (v: val) : val :=
| _ => Vundef
end.
-Definition cast8signed (v: val) : val :=
+Definition zero_ext (nbits: Z) (v: val) : val :=
match v with
- | Vint n => Vint(Int.cast8signed n)
+ | Vint n => Vint(Int.zero_ext nbits n)
| _ => Vundef
end.
-Definition cast8unsigned (v: val) : val :=
+Definition sign_ext (nbits: Z) (v: val) : val :=
match v with
- | Vint n => Vint(Int.cast8unsigned n)
- | _ => Vundef
- end.
-
-Definition cast16signed (v: val) : val :=
- match v with
- | Vint n => Vint(Int.cast16signed n)
- | _ => Vundef
- end.
-
-Definition cast16unsigned (v: val) : val :=
- match v with
- | Vint n => Vint(Int.cast16unsigned n)
+ | Vint n => Vint(Int.sign_ext nbits n)
| _ => Vundef
end.
@@ -300,6 +288,15 @@ Definition rolm (v: val) (amount mask: int): val :=
| _ => Vundef
end.
+Definition ror (v1 v2: val): val :=
+ match v1, v2 with
+ | Vint n1, Vint n2 =>
+ if Int.ltu n2 (Int.repr 32)
+ then Vint(Int.ror n1 n2)
+ else Vundef
+ | _, _ => Vundef
+ end.
+
Definition addf (v1 v2: val): val :=
match v1, v2 with
| Vfloat f1, Vfloat f2 => Vfloat(Float.add f1 f2)
@@ -377,10 +374,10 @@ Definition cmpf (c: comparison) (v1 v2: val): val :=
Definition load_result (chunk: memory_chunk) (v: val) :=
match chunk, v with
- | Mint8signed, Vint n => Vint (Int.cast8signed n)
- | Mint8unsigned, Vint n => Vint (Int.cast8unsigned n)
- | Mint16signed, Vint n => Vint (Int.cast16signed n)
- | Mint16unsigned, Vint n => Vint (Int.cast16unsigned n)
+ | Mint8signed, Vint n => Vint (Int.sign_ext 8 n)
+ | Mint8unsigned, Vint n => Vint (Int.zero_ext 8 n)
+ | Mint16signed, Vint n => Vint (Int.sign_ext 16 n)
+ | Mint16unsigned, Vint n => Vint (Int.zero_ext 16 n)
| Mint32, Vint n => Vint n
| Mint32, Vptr b ofs => Vptr b ofs
| Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f)
@@ -391,15 +388,17 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
(** Theorems on arithmetic operations. *)
Theorem cast8unsigned_and:
- forall x, cast8unsigned x = and x (Vint(Int.repr 255)).
+ forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
Proof.
- destruct x; simpl; auto. decEq. apply Int.cast8unsigned_and.
+ destruct x; simpl; auto. decEq.
+ change 255 with (two_p 8 - 1). apply Int.zero_ext_and. vm_compute; auto.
Qed.
Theorem cast16unsigned_and:
- forall x, cast16unsigned x = and x (Vint(Int.repr 65535)).
+ forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
Proof.
- destruct x; simpl; auto. decEq. apply Int.cast16unsigned_and.
+ destruct x; simpl; auto. decEq.
+ change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto.
Qed.
Theorem istrue_not_isfalse:
@@ -532,6 +531,12 @@ Proof.
destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto.
Qed.
+Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y).
+Proof.
+ intros. unfold sub, add.
+ destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto.
+Qed.
+
Theorem sub_add_l:
forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i).
Proof.
@@ -823,6 +828,13 @@ Proof.
apply notbool_idem2.
Qed.
+Theorem negate_cmpf_ne:
+ forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.
+Proof.
+ destruct v1; destruct v2; simpl; auto.
+ rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. auto.
+Qed.
+
Lemma or_of_bool:
forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2).
Proof.
@@ -940,26 +952,14 @@ Proof.
intros. inv H. auto. destruct chunk; simpl; auto.
Qed.
-Lemma cast8signed_lessdef:
- forall v1 v2, lessdef v1 v2 -> lessdef (cast8signed v1) (cast8signed v2).
-Proof.
- intros; inv H; simpl; auto.
-Qed.
-
-Lemma cast8unsigned_lessdef:
- forall v1 v2, lessdef v1 v2 -> lessdef (cast8unsigned v1) (cast8unsigned v2).
-Proof.
- intros; inv H; simpl; auto.
-Qed.
-
-Lemma cast16signed_lessdef:
- forall v1 v2, lessdef v1 v2 -> lessdef (cast16signed v1) (cast16signed v2).
+Lemma zero_ext_lessdef:
+ forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2).
Proof.
intros; inv H; simpl; auto.
Qed.
-Lemma cast16unsigned_lessdef:
- forall v1 v2, lessdef v1 v2 -> lessdef (cast16unsigned v1) (cast16unsigned v2).
+Lemma sign_ext_lessdef:
+ forall n v1 v2, lessdef v1 v2 -> lessdef (sign_ext n v1) (sign_ext n v2).
Proof.
intros; inv H; simpl; auto.
Qed.
diff --git a/extraction/.depend b/extraction/.depend
index 4730714..83dc5dc 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -46,6 +46,10 @@
Coqlib.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi
../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTL.cmx Datatypes.cmx \
Coqlib.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx
+../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
+ ../caml/Camlcoq.cmo CList.cmi AST.cmi
+../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
+ ../caml/Camlcoq.cmx CList.cmx AST.cmx
../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
CList.cmi AST.cmi
../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
@@ -170,7 +174,7 @@ PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \
Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi
Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
- LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi
+ LTLin.cmi Integers.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi
RTLgen.cmi: Switch.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi \
Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CminorSel.cmi Cminor.cmi \
CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi
@@ -446,9 +450,11 @@ Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \
Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
Registers.cmi
Reload.cmo: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
- LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi Reload.cmi
+ LTLin.cmi Integers.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi \
+ Reload.cmi
Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \
- LTLin.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx Reload.cmi
+ LTLin.cmx Integers.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx \
+ Reload.cmi
RTLgen.cmo: Switch.cmi Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi \
Op.cmi Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
CminorSel.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi \
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index c14ed79..ff6e9ae 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -356,6 +356,25 @@ Proof.
rewrite two_power_nat_S. omega.
Qed.
+Lemma two_p_monotone:
+ forall x y, 0 <= x <= y -> two_p x <= two_p y.
+Proof.
+ intros.
+ replace (two_p x) with (two_p x * 1) by omega.
+ replace y with (x + (y - x)) by omega.
+ rewrite two_p_is_exp; try omega.
+ apply Zmult_le_compat_l.
+ assert (two_p (y - x) > 0). apply two_p_gt_ZERO. omega. omega.
+ 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).
+Proof.
+ induction x. auto.
+ rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega.
+Qed.
+
(** Properties of [Zmin] and [Zmax] *)
Lemma Zmin_spec:
@@ -440,6 +459,73 @@ Proof.
rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega.
Qed.
+Lemma Zdiv_Zdiv:
+ forall a b c,
+ b > 0 -> c > 0 -> (a / b) / c = a / (b * c).
+Proof.
+ intros.
+ generalize (Z_div_mod_eq a b H). generalize (Z_mod_lt a b H). intros.
+ generalize (Z_div_mod_eq (a/b) c H0). generalize (Z_mod_lt (a/b) c H0). intros.
+ set (q1 := a / b) in *. set (r1 := a mod b) in *.
+ set (q2 := q1 / c) in *. set (r2 := q1 mod c) in *.
+ symmetry. apply Zdiv_unique with (r2 * b + r1).
+ rewrite H2. rewrite H4. ring.
+ split.
+ assert (0 <= r2 * b). apply Zmult_le_0_compat. omega. omega. omega.
+ assert ((r2 + 1) * b <= c * b).
+ apply Zmult_le_compat_r. omega. omega.
+ replace ((r2 + 1) * b) with (r2 * b + b) in H5 by ring.
+ replace (c * b) with (b * c) in H5 by ring.
+ omega.
+Qed.
+
+Lemma Zmult_le_compat_l_neg :
+ forall n m p:Z, n >= m -> p <= 0 -> p * n <= p * m.
+Proof.
+ intros.
+ assert ((-p) * n >= (-p) * m). apply Zmult_ge_compat_l. auto. omega.
+ replace (p * n) with (- ((-p) * n)) by ring.
+ replace (p * m) with (- ((-p) * m)) by ring.
+ omega.
+Qed.
+
+Lemma Zdiv_interval_1:
+ forall lo hi a b,
+ lo <= 0 -> hi > 0 -> b > 0 ->
+ lo * b <= a < hi * b ->
+ lo <= a/b < hi.
+Proof.
+ intros.
+ generalize (Z_div_mod_eq a b H1). generalize (Z_mod_lt a b H1). intros.
+ set (q := a/b) in *. set (r := a mod b) in *.
+ split.
+ assert (lo < (q + 1)).
+ apply Zmult_lt_reg_r with b. omega.
+ apply Zle_lt_trans with a. omega.
+ replace ((q + 1) * b) with (b * q + b) by ring.
+ omega.
+ omega.
+ apply Zmult_lt_reg_r with b. omega.
+ replace (q * b) with (b * q) by ring.
+ omega.
+Qed.
+
+Lemma Zdiv_interval_2:
+ forall lo hi a b,
+ lo <= a <= hi -> lo <= 0 -> hi > 0 -> b > 0 ->
+ lo <= a/b <= hi.
+Proof.
+ intros.
+ assert (lo <= a / b < hi+1).
+ apply Zdiv_interval_1. omega. omega. auto.
+ assert (lo * b <= lo * 1). apply Zmult_le_compat_l_neg. omega. omega.
+ replace (lo * 1) with lo in H3 by ring.
+ assert ((hi + 1) * 1 <= (hi + 1) * b). apply Zmult_le_compat_l. omega. omega.
+ replace ((hi + 1) * 1) with (hi + 1) in H4 by ring.
+ omega.
+ omega.
+Qed.
+
(** Alignment: [align n amount] returns the smallest multiple of [amount]
greater than or equal to [n]. *)
diff --git a/lib/Integers.v b/lib/Integers.v
index 2d548fb..a9644bc 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -118,16 +118,13 @@ Definition ltu (x y: int) : bool :=
if zlt (unsigned x) (unsigned y) then true else false.
Definition neg (x: int) : int := repr (- unsigned x).
-Definition cast8signed (x: int) : int :=
- let y := Zmod (unsigned x) 256 in
- if zlt y 128 then repr y else repr (y - 256).
-Definition cast8unsigned (x: int) : int :=
- repr (Zmod (unsigned x) 256).
-Definition cast16signed (x: int) : int :=
- let y := Zmod (unsigned x) 65536 in
- if zlt y 32768 then repr y else repr (y - 65536).
-Definition cast16unsigned (x: int) : int :=
- repr (Zmod (unsigned x) 65536).
+
+Definition zero_ext (n: Z) (x: int) : int :=
+ repr (Zmod (unsigned x) (two_p n)).
+Definition sign_ext (n: Z) (x: int) : int :=
+ repr (let p := two_p n in
+ let y := Zmod (unsigned x) p in
+ if zlt y (two_p (n-1)) then y else y - p).
Definition add (x y: int) : int :=
repr (unsigned x + unsigned y).
@@ -229,6 +226,7 @@ Definition shru (x y: int): int :=
Definition shr (x y: int): int :=
repr (signed x / two_p (unsigned y)).
+
Definition shrx (x y: int): int :=
divs x (shl one y).
@@ -241,6 +239,12 @@ Definition rol (x y: int) : int :=
repr (Z_of_bits wordsize
(fun i => fx (Zmod (i - vy) (Z_of_nat wordsize)))).
+Definition ror (x y: int) : int :=
+ let fx := bits_of_Z wordsize (unsigned x) in
+ let vy := unsigned y in
+ repr (Z_of_bits wordsize
+ (fun i => fx (Zmod (i + vy) (Z_of_nat wordsize)))).
+
Definition rolm (x a m: int): int := and (rol x a) m.
(** Decomposition of a number as a sum of powers of two. *)
@@ -710,6 +714,14 @@ Proof.
unfold neg, zero. compute. apply mkint_eq. auto.
Qed.
+Theorem neg_involutive: forall x, neg (neg x) = x.
+Proof.
+ intros; unfold neg. transitivity (repr (unsigned x)).
+ apply eqm_samerepr. apply eqm_trans with (- (- (unsigned x))).
+ apply eqm_neg. apply eqm_unsigned_repr_l. apply eqm_refl.
+ apply eqm_refl2. omega. apply repr_unsigned.
+Qed.
+
Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
Proof.
intros; unfold neg, add. apply eqm_samerepr.
@@ -996,6 +1008,19 @@ Proof.
rewrite inj_S in H. omega. rewrite inj_S in H. omega.
Qed.
+Lemma bits_of_Z_of_bits':
+ forall n f i,
+ bits_of_Z n (Z_of_bits n f) i =
+ if zlt i 0 then false
+ else if zle (Z_of_nat n) i then false
+ else f i.
+Proof.
+ intros.
+ destruct (zlt i 0). apply bits_of_Z_below; auto.
+ destruct (zle (Z_of_nat n) i). apply bits_of_Z_above. omega.
+ apply bits_of_Z_of_bits. omega.
+Qed.
+
Opaque Zmult.
Lemma Z_of_bits_excl:
@@ -1189,6 +1214,67 @@ Proof.
auto.
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.
+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:
@@ -1316,6 +1402,67 @@ 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 ->
+ 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).
+ set (x' := unsigned x).
+ set (y' := unsigned y).
+ set (z' := unsigned z).
+ intros.
+ repeat rewrite unsigned_repr.
+ decEq. apply Z_of_bits_exten. intros n R.
+ rewrite bits_of_Z_of_bits'.
+ destruct (zlt (n - z') 0).
+ symmetry. apply bits_of_Z_below. omega.
+ 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.
+ 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 ->
+ 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).
+ set (x' := unsigned x).
+ set (y' := unsigned y).
+ set (z' := unsigned z).
+ intros.
+ repeat rewrite unsigned_repr.
+ decEq. apply Z_of_bits_exten. intros n R.
+ rewrite bits_of_Z_of_bits'.
+ destruct (zlt (n + z') 0). omegaContradiction.
+ 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.
+ apply Z_of_bits_range_2.
+Qed.
+
Theorem shru_rolm:
forall x n,
ltu n (repr (Z_of_nat wordsize)) = true ->
@@ -1374,6 +1521,32 @@ Proof.
unfold and; intros. apply bitwise_binop_shru. reflexivity.
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 ->
+ 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).
+ set (x' := signed x).
+ set (y' := unsigned y).
+ set (z' := unsigned z).
+ intros.
+ rewrite unsigned_repr.
+ 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.
+Qed.
+
Theorem rol_zero:
forall x,
rol x zero = x.
@@ -1469,6 +1642,90 @@ Proof.
intros; unfold rolm. symmetry. apply and_or_distrib.
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).
+Proof.
+ intros. unfold ror, rol, sub.
+ generalize (ltu_inv _ _ H).
+ change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat 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.
+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) ->
+ 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).
+ 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.
+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.
+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).
+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.
+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)).
+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).
+Qed.
+
(** ** Relation between shifts and powers of 2 *)
Fixpoint powerserie (l: list Z): Z :=
@@ -1573,6 +1830,48 @@ Proof.
intros; discriminate.
Qed.
+Remark two_p_range:
+ forall n,
+ 0 <= n < Z_of_nat wordsize ->
+ 0 <= two_p n <= max_unsigned.
+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.
+Qed.
+
+Remark Z_one_bits_zero:
+ forall n i, Z_one_bits n 0 i = nil.
+Proof.
+ induction n; intros; simpl; auto.
+Qed.
+
+Remark Z_one_bits_two_p:
+ forall n x i,
+ 0 <= x < Z_of_nat n ->
+ Z_one_bits n (two_p x) i = (i + x) :: nil.
+Proof.
+ induction n; intros; simpl. simpl in H. omegaContradiction.
+ rewrite inj_S in H.
+ assert (x = 0 \/ 0 < x) by omega. destruct H0.
+ subst x; simpl. decEq. omega. apply Z_one_bits_zero.
+ replace (two_p x) with (Z_shift_add false (two_p (x-1))).
+ rewrite Z_bin_decomp_shift_add.
+ replace (i + x) with ((i + 1) + (x - 1)) by omega.
+ apply IHn. omega.
+ unfold Z_shift_add. rewrite <- two_p_S. decEq; omega. omega.
+Qed.
+
+Lemma is_power2_two_p:
+ forall n, 0 <= n < Z_of_nat wordsize ->
+ is_power2 (repr (two_p n)) = Some (repr n).
+Proof.
+ intros. unfold is_power2. rewrite unsigned_repr.
+ rewrite Z_one_bits_two_p. auto. auto.
+ apply two_p_range. auto.
+Qed.
+
Theorem mul_pow2:
forall x n logn,
is_power2 n = Some logn ->
@@ -1728,20 +2027,85 @@ Proof.
rewrite add_neg_zero. apply add_zero.
Qed.
+Lemma Zdiv_round_Zdiv:
+ forall x y,
+ y > 0 ->
+ Zdiv_round x y = if zlt x 0 then (x + y - 1) / y else x / y.
+Proof.
+ intros. unfold Zdiv_round.
+ destruct (zlt x 0).
+ rewrite zlt_false; try omega.
+ generalize (Z_div_mod_eq (-x) y H).
+ generalize (Z_mod_lt (-x) y H).
+ set (q := (-x) / y). set (r := (-x) mod y). intros.
+ symmetry.
+ apply Zdiv_unique with (y - r - 1).
+ replace x with (- (y * q) - r) by omega.
+ replace (-(y * q)) with ((-q) * y) by ring.
+ omega.
+ omega.
+ apply zlt_false. omega.
+Qed.
+
+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.
+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).
+ set (uy := unsigned y).
+ intro RANGE.
+ assert (shl one y = repr (two_p uy)).
+ transitivity (mul one (repr (two_p uy))).
+ symmetry. apply mul_pow2. replace y with (repr uy).
+ 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 (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.
+ 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 Zdiv_round_Zdiv; auto.
+ unfold lt. change (signed zero) with 0.
+ 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.
+ omega.
+Qed.
+
Lemma add_and:
forall x y z,
and y z = zero ->
- or y z = mone ->
- add (and x y) (and x z) = x.
+ add (and x y) (and x z) = and x (or y z).
Proof.
- intros. unfold add. transitivity (repr (unsigned x)); auto with ints.
- decEq. unfold and, bitwise_binop.
+ intros. unfold add, and, bitwise_binop.
+ decEq.
repeat rewrite unsigned_repr; auto with ints.
- transitivity (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x))).
- apply Z_of_bits_excl. intros.
+ apply Z_of_bits_excl; intros.
assert (forall a b c, a && b && (a && c) = a && (b && c)).
destruct a; destruct b; destruct c; reflexivity.
- rewrite H2.
+ rewrite H1.
replace (bits_of_Z wordsize (unsigned y) i &&
bits_of_Z wordsize (unsigned z) i)
with (bits_of_Z wordsize (unsigned (and y z)) i).
@@ -1750,70 +2114,11 @@ Proof.
unfold and, bitwise_binop.
rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits.
reflexivity. auto.
- intros. rewrite <- demorgan1.
- replace (bits_of_Z wordsize (unsigned y) i ||
- bits_of_Z wordsize (unsigned z) i)
- with (bits_of_Z wordsize (unsigned (or y z)) i).
- rewrite H0. change (unsigned mone) with (two_power_nat wordsize - 1).
- rewrite bits_of_Z_mone; auto. apply andb_b_true.
+ rewrite <- demorgan1.
unfold or, bitwise_binop.
rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits; auto.
- apply eqm_small_eq; auto with ints. apply Z_of_bits_of_Z.
-Qed.
-
-(** To prove equalities involving modulus and bitwise ``and'', 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.
-
-(** Here are the three equalities that we prove by reflection. *)
-
Remark modu_and_masks_1:
forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
rol (shru mone logn) logn = shl mone logn.
@@ -1879,7 +2184,8 @@ Proof.
replace n with (repr (two_p (unsigned logn))).
rewrite modu_and_masks_1; auto.
rewrite and_idem.
- apply add_and. apply modu_and_masks_2; auto. apply modu_and_masks_3; auto.
+ 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.
@@ -1892,208 +2198,282 @@ Qed.
(** ** Properties of integer zero extension and sign extension. *)
-Theorem cast8unsigned_and:
- forall x, cast8unsigned x = and x (repr 255).
-Proof.
- intros; unfold cast8unsigned.
- change (repr (unsigned x mod 256)) with (modu x (repr 256)).
- change (repr 255) with (sub (repr 256) one).
- apply modu_and with (repr 8). reflexivity.
+Section EXTENSIONS.
+
+Variable n: Z.
+Hypothesis RANGE: 0 < n < Z_of_nat wordsize.
+
+Remark two_p_n_pos:
+ two_p n > 0.
+Proof. apply two_p_gt_ZERO. omega. Qed.
+
+Remark two_p_n_range:
+ 0 <= two_p n <= max_unsigned.
+Proof. apply two_p_range. omega. Qed.
+
+Remark two_p_n_range':
+ two_p n <= max_signed + 1.
+Proof.
+ assert (two_p n <= two_p (Z_of_nat wordsize - 1)).
+ apply two_p_monotone. omega.
+ exact H.
Qed.
-Theorem cast16unsigned_and:
- forall x, cast16unsigned x = and x (repr 65535).
+Remark unsigned_repr_two_p:
+ unsigned (repr (two_p n)) = two_p n.
Proof.
- intros; unfold cast16unsigned.
- change (repr (unsigned x mod 65536)) with (modu x (repr 65536)).
- change (repr 65535) with (sub (repr 65536) one).
- apply modu_and with (repr 16). reflexivity.
+ apply unsigned_repr. apply two_p_n_range.
Qed.
-Lemma eqmod_256_unsigned_repr:
- forall a, eqmod 256 a (unsigned (repr a)).
+Theorem zero_ext_and:
+ forall x, zero_ext n x = and x (repr (two_p n - 1)).
Proof.
- intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod.
- intros [k EQ]. exists (k * (modulus / 256)).
- replace (k * (modulus / 256) * 256)
- with (k * ((modulus / 256) * 256)).
- exact EQ. ring.
+ intros; unfold zero_ext.
+ assert (is_power2 (repr (two_p n)) = Some (repr n)).
+ 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.
Qed.
-Lemma eqmod_65536_unsigned_repr:
- forall a, eqmod 65536 a (unsigned (repr a)).
+Theorem zero_ext_idem:
+ forall x, zero_ext n (zero_ext n x) = zero_ext n x.
Proof.
- intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod.
- intros [k EQ]. exists (k * (modulus / 65536)).
- replace (k * (modulus / 65536) * 65536)
- with (k * ((modulus / 65536) * 65536)).
- exact EQ. ring.
+ intros. repeat rewrite zero_ext_and.
+ rewrite and_assoc. rewrite and_idem. auto.
Qed.
-Theorem cast8_signed_unsigned:
- forall n, cast8signed (cast8unsigned n) = cast8signed n.
+Lemma eqm_eqmod_two_p:
+ forall a b, eqm a b -> eqmod (two_p n) a b.
Proof.
- intros; unfold cast8signed, cast8unsigned.
- set (N := unsigned n).
- rewrite unsigned_repr.
- replace ((N mod 256) mod 256) with (N mod 256).
- auto.
- symmetry. apply Zmod_small. apply Z_mod_lt. omega.
- assert (0 <= N mod 256 < 256). apply Z_mod_lt. omega.
- assert (256 < max_unsigned). compute; auto.
+ intros a b [k EQ].
+ exists (k * two_p (Z_of_nat wordsize - n)).
+ rewrite EQ. decEq. rewrite <- Zmult_assoc. decEq.
+ rewrite <- two_p_is_exp. unfold modulus. rewrite two_power_nat_two_p.
+ decEq. omega. omega. omega.
+Qed.
+(*
+Lemma zero_ext_charact:
+ forall x y,
+ zero_ext n x = y <->
+ 0 <= unsigned y < two_p n /\ eqmod (two_p n) (unsigned x) (unsigned y).
+Proof.
+ intros. unfold zero_ext. set (x' := unsigned x). split; intros.
+ subst y.
+ assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos.
+ rewrite unsigned_repr. split. auto.
+ apply eqmod_mod. apply two_p_n_pos.
+ generalize two_p_n_range. omega.
+ destruct H. destruct H0 as [k EQ].
+ assert (x' mod two_p n = unsigned y).
+ apply Zmod_unique with k; auto.
+ rewrite H0. apply repr_unsigned.
+Qed.
+
+Lemma sign_ext_charact:
+ forall x y,
+ sign_ext n x = y <->
+ -(two_p (n-1)) <= signed y < two_p (n-1)
+ /\ eqmod (two_p n) (unsigned x) (signed y).
+Proof.
+ intros. unfold sign_ext. set (x' := unsigned x). split; intros.
+ assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos.
+ destruct (zlt (x' mod two_p n) (two_p (n - 1))); subst y.
+ rewrite signed_repr. split. omega.
+ apply eqmod_mod. apply two_p_n_pos.
+ assert (min_signed < 0). vm_compute; auto.
+ generalize two_p_n_range'. omega.
+ rewrite signed_repr. split.
+ assert (two_p n = 2 * two_p (n-1)). rewrite <- two_p_S. decEq. omega. omega.
+ omega.
+ apply eqmod_trans with (x' - 0). apply eqmod_refl2. omega.
+ apply eqmod_sub. apply eqmod_mod. apply two_p_n_pos.
+ exists (-1). ring.
+ split. generalize two_p_n_range'.
+ change (max_signed + 1) with (- min_signed). omega.
+ generalize two_p_n_range'. omega.
+
+ destruct H. destruct H0 as [k EQ].
+ assert (two_p n = 2 * two_p (n - 1)). rewrite <- two_p_S. decEq. omega. omega.
+ assert (signed y >= 0 \/ signed y < 0) by omega. destruct H1.
+ assert (x' mod two_p n = signed y).
+ apply Zmod_unique with k; auto. omega.
+ rewrite zlt_true. rewrite H2. apply repr_signed. omega.
+ assert (x' mod two_p n = signed y + two_p n).
+ apply Zmod_unique with (k-1). rewrite EQ. ring. omega.
+ rewrite zlt_false. replace (x' mod two_p n - two_p n) with (signed y) by omega. apply repr_signed.
+ omega.
+Qed.
+*)
+
+Lemma sign_ext_charact:
+ forall x y,
+ -(two_p (n-1)) <= signed y < two_p (n-1) ->
+ eqmod (two_p n) (unsigned x) (signed y) ->
+ sign_ext n x = y.
+Proof.
+ intros. unfold sign_ext. set (x' := unsigned x) in *.
+ destruct H0 as [k EQ].
+ assert (two_p n = 2 * two_p (n - 1)). rewrite <- two_p_S. decEq. omega. omega.
+ assert (signed y >= 0 \/ signed y < 0) by omega. destruct H1.
+ assert (x' mod two_p n = signed y).
+ apply Zmod_unique with k; auto. omega.
+ rewrite zlt_true. rewrite H2. apply repr_signed. omega.
+ assert (x' mod two_p n = signed y + two_p n).
+ apply Zmod_unique with (k-1). rewrite EQ. ring. omega.
+ rewrite zlt_false. replace (x' mod two_p n - two_p n) with (signed y) by omega. apply repr_signed.
omega.
Qed.
-Theorem cast8_unsigned_signed:
- forall n, cast8unsigned (cast8signed n) = cast8unsigned n.
+Lemma zero_ext_eqmod_two_p:
+ forall x y,
+ eqmod (two_p n) (unsigned x) (unsigned y) -> zero_ext n x = zero_ext n y.
Proof.
- intros; unfold cast8signed, cast8unsigned.
- set (N := unsigned n mod 256).
- assert (0 <= N < 256). unfold N; apply Z_mod_lt. omega.
- assert (N mod 256 = N). apply Zmod_small. auto.
- assert (256 <= max_unsigned). compute; congruence.
- decEq.
- case (zlt N 128); intro.
- rewrite unsigned_repr. auto. omega.
- transitivity (N mod 256); auto.
- apply eqmod_mod_eq. omega.
- apply eqmod_trans with (N - 256). apply eqmod_sym. apply eqmod_256_unsigned_repr.
- assert (eqmod 256 (N - 256) (N - 0)).
- apply eqmod_sub. apply eqmod_refl.
- red. exists 1; reflexivity.
- replace (N - 0) with N in H2. auto. omega.
+ intros. unfold zero_ext. decEq. apply eqmod_mod_eq. apply two_p_n_pos. auto.
Qed.
-Theorem cast16_unsigned_signed:
- forall n, cast16unsigned (cast16signed n) = cast16unsigned n.
+Lemma sign_ext_eqmod_two_p:
+ forall x y,
+ eqmod (two_p n) (unsigned x) (unsigned y) -> sign_ext n x = sign_ext n y.
Proof.
- intros; unfold cast16signed, cast16unsigned.
- set (N := unsigned n mod 65536).
- assert (0 <= N < 65536). unfold N; apply Z_mod_lt. omega.
- assert (N mod 65536 = N). apply Zmod_small. auto.
- assert (65536 <= max_unsigned). compute; congruence.
- decEq.
- case (zlt N 32768); intro.
- rewrite unsigned_repr. auto. omega.
- transitivity (N mod 65536); auto.
- apply eqmod_mod_eq. omega.
- apply eqmod_trans with (N - 65536). apply eqmod_sym. apply eqmod_65536_unsigned_repr.
- assert (eqmod 65536 (N - 65536) (N - 0)).
- apply eqmod_sub. apply eqmod_refl.
- red. exists 1; reflexivity.
- replace (N - 0) with N in H2. auto. omega.
-Qed.
-
-Theorem cast8_unsigned_idem:
- forall n, cast8unsigned (cast8unsigned n) = cast8unsigned n.
-Proof.
- intros. repeat rewrite cast8unsigned_and.
- rewrite and_assoc. reflexivity.
-Qed.
-
-Theorem cast16_unsigned_idem:
- forall n, cast16unsigned (cast16unsigned n) = cast16unsigned n.
-Proof.
- intros. repeat rewrite cast16unsigned_and.
- rewrite and_assoc. reflexivity.
-Qed.
-
-Theorem cast8_signed_idem:
- forall n, cast8signed (cast8signed n) = cast8signed n.
-Proof.
- intros; unfold cast8signed.
- set (N := unsigned n mod 256).
- assert (256 < max_unsigned). compute; auto.
- assert (0 <= N < 256). unfold N. apply Z_mod_lt. omega.
- case (zlt N 128); intro.
- assert (unsigned (repr N) = N).
- apply unsigned_repr. omega.
- rewrite H1.
- replace (N mod 256) with N. apply zlt_true. auto.
- symmetry. apply Zmod_small. auto.
- set (M := (unsigned (repr (N - 256)) mod 256)).
- assert (M = N).
- unfold M, N. apply eqmod_mod_eq. omega.
- apply eqmod_trans with (unsigned n mod 256 - 256).
- apply eqmod_sym. apply eqmod_256_unsigned_repr.
- apply eqmod_trans with (unsigned n - 0).
- apply eqmod_sub.
- apply eqmod_sym. apply eqmod_mod. omega.
- unfold eqmod. exists 1; omega.
- apply eqmod_refl2. omega.
- rewrite H1. rewrite zlt_false; auto.
-Qed.
-
-Theorem cast16_signed_idem:
- forall n, cast16signed (cast16signed n) = cast16signed n.
-Proof.
- intros; unfold cast16signed.
- set (N := unsigned n mod 65536).
- assert (65536 < max_unsigned). compute; auto.
- assert (0 <= N < 65536). unfold N. apply Z_mod_lt. omega.
- case (zlt N 32768); intro.
- assert (unsigned (repr N) = N).
- apply unsigned_repr. omega.
- rewrite H1.
- replace (N mod 65536) with N. apply zlt_true. auto.
- symmetry. apply Zmod_small. auto.
- set (M := (unsigned (repr (N - 65536)) mod 65536)).
- assert (M = N).
- unfold M, N. apply eqmod_mod_eq. omega.
- apply eqmod_trans with (unsigned n mod 65536 - 65536).
- apply eqmod_sym. apply eqmod_65536_unsigned_repr.
- apply eqmod_trans with (unsigned n - 0).
- apply eqmod_sub.
- apply eqmod_sym. apply eqmod_mod. omega.
- unfold eqmod. exists 1; omega.
- apply eqmod_refl2. omega.
- rewrite H1. rewrite zlt_false; auto.
-Qed.
-
-Theorem cast8_signed_equal_if_unsigned_equal:
- forall x y,
- cast8unsigned x = cast8unsigned y ->
- cast8signed x = cast8signed y.
-Proof.
- unfold cast8unsigned, cast8signed; intros until y.
- set (x' := unsigned x mod 256).
- set (y' := unsigned y mod 256).
- intro.
- assert (eqm x' y').
- apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr.
- rewrite H. apply eqm_sym. apply eqm_unsigned_repr.
- assert (forall z, 0 <= z mod 256 < modulus).
- intros.
- assert (0 <= z mod 256 < 256). apply Z_mod_lt. omega.
- assert (256 <= modulus). compute. congruence.
- omega.
- assert (x' = y').
- apply eqm_small_eq; unfold x', y'; auto.
- rewrite H2. auto.
-Qed.
-
-Theorem cast16_signed_equal_if_unsigned_equal:
- forall x y,
- cast16unsigned x = cast16unsigned y ->
- cast16signed x = cast16signed y.
-Proof.
- unfold cast16unsigned, cast16signed; intros until y.
- set (x' := unsigned x mod 65536).
- set (y' := unsigned y mod 65536).
- intro.
- assert (eqm x' y').
- apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr.
- rewrite H. apply eqm_sym. apply eqm_unsigned_repr.
- assert (forall z, 0 <= z mod 65536 < modulus).
- intros.
- assert (0 <= z mod 65536 < 65536). apply Z_mod_lt. omega.
- assert (65536 <= modulus). compute. congruence.
+ intros. unfold sign_ext.
+ assert (unsigned x mod two_p n = unsigned y mod two_p n).
+ apply eqmod_mod_eq. apply two_p_n_pos. auto.
+ rewrite H0. auto.
+Qed.
+
+Lemma eqmod_two_p_zero_ext:
+ forall x, eqmod (two_p n) (unsigned x) (unsigned (zero_ext n x)).
+Proof.
+ intros. unfold zero_ext.
+ apply eqmod_trans with (unsigned x mod two_p n).
+ apply eqmod_mod. apply two_p_n_pos.
+ apply eqm_eqmod_two_p. apply eqm_unsigned_repr.
+Qed.
+
+Lemma eqmod_two_p_sign_ext:
+ forall x, eqmod (two_p n) (unsigned x) (unsigned (sign_ext n x)).
+Proof.
+ intros. unfold sign_ext. destruct (zlt (unsigned x mod two_p n) (two_p (n-1))).
+ apply eqmod_trans with (unsigned x mod two_p n).
+ apply eqmod_mod. apply two_p_n_pos.
+ apply eqm_eqmod_two_p. apply eqm_unsigned_repr.
+ apply eqmod_trans with (unsigned x mod two_p n).
+ apply eqmod_mod. apply two_p_n_pos.
+ apply eqmod_trans with (unsigned x mod two_p n - 0).
+ apply eqmod_refl2. omega.
+ apply eqmod_trans with (unsigned x mod two_p n - two_p n).
+ apply eqmod_sub. apply eqmod_refl. exists (-1). ring.
+ apply eqm_eqmod_two_p. apply eqm_unsigned_repr.
+Qed.
+
+Theorem sign_ext_idem:
+ forall x, sign_ext n (sign_ext n x) = sign_ext n x.
+Proof.
+ intros. apply sign_ext_eqmod_two_p.
+ apply eqmod_sym. apply eqmod_two_p_sign_ext.
+Qed.
+
+Theorem sign_ext_zero_ext:
+ forall x, sign_ext n (zero_ext n x) = sign_ext n x.
+Proof.
+ intros. apply sign_ext_eqmod_two_p.
+ apply eqmod_sym. apply eqmod_two_p_zero_ext.
+Qed.
+
+Theorem zero_ext_sign_ext:
+ forall x, zero_ext n (sign_ext n x) = zero_ext n x.
+Proof.
+ intros. apply zero_ext_eqmod_two_p.
+ apply eqmod_sym. apply eqmod_two_p_sign_ext.
+Qed.
+
+Theorem sign_ext_equal_if_zero_equal:
+ forall x y,
+ zero_ext n x = zero_ext n y ->
+ sign_ext n x = sign_ext n y.
+Proof.
+ intros. rewrite <- (sign_ext_zero_ext x).
+ rewrite <- (sign_ext_zero_ext y). congruence.
+Qed.
+
+Lemma eqmod_mult_div:
+ forall n1 n2 x y,
+ 0 <= n1 -> 0 <= n2 ->
+ eqmod (two_p (n1+n2)) (two_p n1 * x) y ->
+ eqmod (two_p n2) x (y / two_p n1).
+Proof.
+ intros. rewrite two_p_is_exp in H1; auto.
+ destruct H1 as [k EQ]. exists k.
+ change x with (0 / two_p n1 + x). rewrite <- Z_div_plus.
+ replace (0 + x * two_p n1) with (two_p n1 * x) by ring.
+ rewrite EQ.
+ replace (k * (two_p n1 * two_p n2) + y) with (y + (k * two_p n2) * two_p n1) by ring.
+ rewrite Z_div_plus. ring.
+ apply two_p_gt_ZERO; auto.
+ apply two_p_gt_ZERO; auto.
+Qed.
+
+Theorem sign_ext_shr_shl:
+ forall x,
+ let y := repr (Z_of_nat wordsize - n) in
+ sign_ext n x = shr (shl x y) y.
+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.
+ apply sign_ext_charact.
+ (* inequalities *)
+ unfold shr. rewrite H.
+ set (z := signed (shl x y)).
+ rewrite signed_repr.
+ apply Zdiv_interval_1.
+ assert (two_p (n - 1) > 0). apply two_p_gt_ZERO. omega. omega.
+ apply two_p_gt_ZERO. omega.
+ apply two_p_gt_ZERO. omega.
+ replace ((- two_p (n-1)) * two_p (Z_of_nat wordsize - n))
+ 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.
+ omega. omega.
+ apply Zdiv_interval_2. unfold z. apply signed_range.
+ vm_compute; congruence. vm_compute; auto. 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.
+ 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.
+ apply eqm_unsigned_repr_l. rewrite (Zmult_comm (unsigned x)).
+ apply eqm_mult. apply eqm_sym. apply eqm_unsigned_repr. apply eqm_refl.
+ apply eqm_eqmod_two_p. apply eqm_sym. eapply eqm_trans.
+ apply eqm_signed_unsigned. apply eqm_sym. apply eqm_unsigned_repr.
+Qed.
+
+Theorem zero_ext_shru_shl:
+ forall x,
+ let y := repr (Z_of_nat wordsize - n) in
+ zero_ext n x = shru (shl x y) y.
+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.
- assert (x' = y').
- apply eqm_small_eq; unfold x', y'; auto.
- rewrite H2. auto.
+ 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.
Qed.
+End EXTENSIONS.
+
(** ** Properties of [one_bits] (decomposition in sum of powers of two) *)
Opaque Z_one_bits. (* Otherwise, next Qed blows up! *)