From e99d18c442c40a14e6eaea722cbc7ef0ca6dd26a Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 21 Aug 2010 10:21:11 +0000 Subject: Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext as bitwise operations rather than arithmetic ones. CastOptimproof: fixed for ARM port. Other files: adapted to changes in Integers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Integers.v | 2039 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 1012 insertions(+), 1027 deletions(-) (limited to 'lib') diff --git a/lib/Integers.v b/lib/Integers.v index f1440e9..1087728 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -138,13 +138,6 @@ Definition ltu (x y: int) : bool := Definition neg (x: int) : int := repr (- unsigned x). -Definition zero_ext (n: Z) (x: int) : int := - repr (Zmod (unsigned x) (two_p n)). -Definition sign_ext (n: Z) (x: int) : int := - repr (let p := two_p n in - let y := Zmod (unsigned x) p in - if zlt y (two_p (n-1)) then y else y - p). - Definition add (x y: int) : int := repr (unsigned x + unsigned y). Definition sub (x y: int) : int := @@ -152,6 +145,9 @@ Definition sub (x y: int) : int := Definition mul (x y: int) : int := repr (unsigned x * unsigned y). +(** [Zdiv_round] and [Zmod_round] implement signed division and modulus + with round-towards-zero behavior. *) + Definition Zdiv_round (x y: Z) : Z := if zlt x 0 then if zlt y 0 then (-x) / (-y) else - ((-x) / y) @@ -165,6 +161,7 @@ Definition divs (x y: int) : int := repr (Zdiv_round (signed x) (signed y)). Definition mods (x y: int) : int := repr (Zmod_round (signed x) (signed y)). + Definition divu (x y: int) : int := repr (unsigned x / unsigned y). Definition modu (x y: int) : int := @@ -174,8 +171,8 @@ Definition modu (x y: int) : int := and their bit-level representations. Bit-level representations are represented as characteristic functions, that is, functions [f] of type [nat -> bool] such that [f i] is the value of the [i]-th bit - of the number. The values of characteristic functions for [i] greater - than 32 are ignored. *) + of the number. For [i] less than 0 or greater or equal to [wordsize], + the characteristic function is [false]. *) Definition Z_shift_add (b: bool) (x: Z) := if b then 2 * x + 1 else 2 * x. @@ -207,18 +204,18 @@ Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool := (fun i: Z => if zeq i 0 then b else f (i - 1)) end. -Fixpoint Z_of_bits (n: nat) (f: Z -> bool) {struct n}: Z := +Fixpoint Z_of_bits (n: nat) (f: Z -> bool) (i: Z) {struct n}: Z := match n with | O => 0 - | S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1))) + | S m => Z_shift_add (f i) (Z_of_bits m f (Zsucc i)) end. -(** Bitwise logical ``and'', ``or'' and ``xor'' operations. *) +(** Bitwise logical "and", "or" and "xor" operations. *) Definition bitwise_binop (f: bool -> bool -> bool) (x y: int) := let fx := bits_of_Z wordsize (unsigned x) in let fy := bits_of_Z wordsize (unsigned y) in - repr (Z_of_bits wordsize (fun i => f (fx i) (fy i))). + repr(Z_of_bits wordsize (fun i => f (fx i) (fy i)) 0). Definition and (x y: int): int := bitwise_binop andb x y. Definition or (x y: int): int := bitwise_binop orb x y. @@ -230,21 +227,19 @@ Definition not (x: int) : int := xor x mone. Definition shl (x y: int): int := let fx := bits_of_Z wordsize (unsigned x) in - let vy := unsigned y in - repr (Z_of_bits wordsize (fun i => fx (i - vy))). + repr (Z_of_bits wordsize fx (- unsigned y)). Definition shru (x y: int): int := let fx := bits_of_Z wordsize (unsigned x) in - let vy := unsigned y in - repr (Z_of_bits wordsize (fun i => fx (i + vy))). - -(** Arithmetic right shift is defined as signed division by a power of two. - Two such shifts are defined: [shr] rounds towards minus infinity - (standard behaviour for arithmetic right shift) and - [shrx] rounds towards zero. *) + repr (Z_of_bits wordsize fx (unsigned y)). Definition shr (x y: int): int := - repr (signed x / two_p (unsigned y)). + let fx := bits_of_Z wordsize (unsigned x) in + let sx := fun i => fx (if zlt i (Z_of_nat wordsize) then i else Z_of_nat wordsize - 1) in + repr (Z_of_bits wordsize sx (unsigned y)). + +(** Viewed as signed divisions by powers of two, [shrx] rounds towards + zero, while [shr] rounds towards minus infinity. *) Definition shrx (x y: int): int := divs x (shl one y). @@ -254,18 +249,26 @@ Definition shr_carry (x y: int) := Definition rol (x y: int) : int := let fx := bits_of_Z wordsize (unsigned x) in - let vy := unsigned y in - repr (Z_of_bits wordsize - (fun i => fx (Zmod (i - vy) (Z_of_nat wordsize)))). + let rx := fun i => fx (Zmod i (Z_of_nat wordsize)) in + repr (Z_of_bits wordsize rx (-unsigned y)). 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)))). + let rx := fun i => fx (Zmod i (Z_of_nat wordsize)) in + repr (Z_of_bits wordsize rx (unsigned y)). Definition rolm (x a m: int): int := and (rol x a) m. +(** Zero and sign extensions *) + +Definition zero_ext (n: Z) (x: int) : int := + let fx := bits_of_Z wordsize (unsigned x) in + repr (Z_of_bits wordsize (fun i => if zlt i n then fx i else false) 0). + +Definition sign_ext (n: Z) (x: int) : int := + let fx := bits_of_Z wordsize (unsigned x) in + repr (Z_of_bits wordsize (fun i => if zlt i n then fx i else fx (n - 1)) 0). + (** Decomposition of a number as a sum of powers of two. *) Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z := @@ -287,80 +290,6 @@ Definition is_power2 (x: int) : option int := | _ => None end. -(** Recognition of integers that are acceptable as immediate operands - to the [rlwim] PowerPC instruction. These integers are of the form - [000011110000] or [111100001111], that is, a run of one bits - surrounded by zero bits, or conversely. We recognize these integers by - running the following automaton on the bits. The accepting states are - 2, 3, 4, 5, and 6. -<< - 0 1 0 - / \ / \ / \ - \ / \ / \ / - -0--> [1] --1--> [2] --0--> [3] - / - [0] - \ - -1--> [4] --0--> [5] --1--> [6] - / \ / \ / \ - \ / \ / \ / - 1 0 1 ->> -*) - -Inductive rlw_state: Type := - | RLW_S0 : rlw_state - | RLW_S1 : rlw_state - | RLW_S2 : rlw_state - | RLW_S3 : rlw_state - | RLW_S4 : rlw_state - | RLW_S5 : rlw_state - | RLW_S6 : rlw_state - | RLW_Sbad : rlw_state. - -Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state := - match s, b with - | RLW_S0, false => RLW_S1 - | RLW_S0, true => RLW_S4 - | RLW_S1, false => RLW_S1 - | RLW_S1, true => RLW_S2 - | RLW_S2, false => RLW_S3 - | RLW_S2, true => RLW_S2 - | RLW_S3, false => RLW_S3 - | RLW_S3, true => RLW_Sbad - | RLW_S4, false => RLW_S5 - | RLW_S4, true => RLW_S4 - | RLW_S5, false => RLW_S5 - | RLW_S5, true => RLW_S6 - | RLW_S6, false => RLW_Sbad - | RLW_S6, true => RLW_S6 - | RLW_Sbad, _ => RLW_Sbad - end. - -Definition rlw_accepting (s: rlw_state) : bool := - match s with - | RLW_S0 => false - | RLW_S1 => false - | RLW_S2 => true - | RLW_S3 => true - | RLW_S4 => true - | RLW_S5 => true - | RLW_S6 => true - | RLW_Sbad => false - end. - -Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool := - match n with - | O => - rlw_accepting s - | S m => - let (b, y) := Z_bin_decomp x in - is_rlw_mask_rec m (rlw_transition s b) y - end. - -Definition is_rlw_mask (x: int) : bool := - is_rlw_mask_rec wordsize RLW_S0 (unsigned x). - (** Comparisons. *) Definition cmp (c: comparison) (x y: int) : bool := @@ -456,85 +385,6 @@ Proof. 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. - intros; unfold eq. case (zeq (unsigned x) (unsigned y)); intro. - rewrite e. rewrite zeq_true. auto. - rewrite zeq_false. auto. auto. -Qed. - -Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y. -Proof. - intros; unfold eq. case (eq_dec x y); intro. - subst y. rewrite zeq_true. auto. - rewrite zeq_false. auto. - destruct x; destruct y. - simpl. red; intro. elim n. apply mkint_eq. auto. -Qed. - -Theorem eq_true: forall x, eq x x = true. -Proof. - intros. generalize (eq_spec x x); case (eq x x); intros; congruence. -Qed. - -Theorem eq_false: forall x y, x <> y -> eq x y = false. -Proof. - intros. generalize (eq_spec x y); case (eq x y); intros; congruence. -Qed. - (** ** Modulo arithmetic *) (** We define and state properties of equality and arithmetic modulo a @@ -652,12 +502,6 @@ Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z. Proof (eqmod_trans modulus). Hint Resolve eqm_trans: ints. -Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y. -Proof. - intros. unfold repr. apply mkint_eq. - apply eqmod_mod_eq. auto with ints. exact H. -Qed. - Lemma eqm_small_eq: forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y. Proof (eqmod_small_eq modulus). @@ -685,11 +529,16 @@ Hint Resolve eqm_mult: ints. (** ** Properties of the coercions between [Z] and [int] *) +Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y. +Proof. + intros. unfold repr. apply mkint_eq. + apply eqmod_mod_eq. auto with ints. exact H. +Qed. + Lemma eqm_unsigned_repr: forall z, eqm z (unsigned (repr z)). Proof. - unfold eqm, repr, unsigned; intros; simpl. - apply eqmod_mod. auto with ints. + unfold eqm, repr, unsigned; intros; simpl. apply eqmod_mod. auto with ints. Qed. Hint Resolve eqm_unsigned_repr: ints. @@ -720,7 +569,7 @@ Qed. Theorem unsigned_range: forall i, 0 <= unsigned i < modulus. Proof. - destruct i; simpl. auto. + destruct i; auto. Qed. Hint Resolve unsigned_range: ints. @@ -746,8 +595,7 @@ Qed. Theorem repr_unsigned: forall i, repr (unsigned i) = i. Proof. - destruct i; simpl. unfold repr. apply mkint_eq. - apply Zmod_small. auto. + destruct i; simpl. unfold repr. apply mkint_eq. apply Zmod_small; auto. Qed. Hint Resolve repr_unsigned: ints. @@ -759,11 +607,16 @@ Proof. Qed. Hint Resolve repr_signed: ints. +Lemma eqm_repr_eq: forall x y, eqm x (unsigned y) -> repr x = y. +Proof. + intros. rewrite <- (repr_unsigned y). apply eqm_samerepr; auto. +Qed. + Theorem unsigned_repr: forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z. Proof. - intros. unfold repr, unsigned; simpl. - apply Zmod_small. unfold max_unsigned in H. omega. + intros. unfold repr, unsigned; simpl. + apply Zmod_small. unfold max_unsigned in H. fold modulus. omega. Qed. Hint Resolve unsigned_repr: ints. @@ -793,6 +646,85 @@ Proof. auto. unfold max_signed in H. omegaContradiction. 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. + intros; unfold eq. case (zeq (unsigned x) (unsigned y)); intro. + rewrite e. rewrite zeq_true. auto. + rewrite zeq_false. auto. auto. +Qed. + +Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y. +Proof. + intros; unfold eq. case (eq_dec x y); intro. + subst y. rewrite zeq_true. auto. + rewrite zeq_false. auto. + destruct x; destruct y. + simpl. red; intro. elim n. apply mkint_eq. auto. +Qed. + +Theorem eq_true: forall x, eq x x = true. +Proof. + intros. generalize (eq_spec x x); case (eq x x); intros; congruence. +Qed. + +Theorem eq_false: forall x y, x <> y -> eq x y = false. +Proof. + intros. generalize (eq_spec x y); case (eq x y); intros; congruence. +Qed. + (** ** Properties of addition *) Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y). @@ -809,8 +741,8 @@ Theorem add_commut: forall x y, add x y = add y x. Proof. intros; unfold add. decEq. omega. Qed. Theorem add_zero: forall x, add x zero = x. -Proof. - intros; unfold add, zero. change (unsigned (repr 0)) with 0. +Proof. + intros. unfold add. rewrite unsigned_zero. rewrite Zplus_0_r. apply repr_unsigned. Qed. @@ -847,15 +779,14 @@ Qed. Theorem neg_zero: neg zero = zero. Proof. - unfold neg, zero. compute. apply mkint_eq. auto. + unfold neg. rewrite unsigned_zero. 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. + intros; unfold neg. + apply eqm_repr_eq. eapply eqm_trans. apply eqm_neg. + apply eqm_unsigned_repr_l. apply eqm_refl. apply eqm_refl2. omega. Qed. Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y). @@ -872,30 +803,24 @@ Qed. Theorem sub_zero_l: forall x, sub x zero = x. Proof. - intros; unfold sub. change (unsigned zero) with 0. - replace (unsigned x - 0) with (unsigned x). apply repr_unsigned. - omega. + intros; unfold sub. rewrite unsigned_zero. + replace (unsigned x - 0) with (unsigned x) by omega. apply repr_unsigned. Qed. Theorem sub_zero_r: forall x, sub zero x = neg x. Proof. - intros; unfold sub, neg. change (unsigned zero) with 0. - replace (0 - unsigned x) with (- unsigned x). auto. - omega. + intros; unfold sub, neg. rewrite unsigned_zero. auto. Qed. Theorem sub_add_opp: forall x y, sub x y = add x (neg y). Proof. - intros; unfold sub, add, neg. - replace (unsigned x - unsigned y) - with (unsigned x + (- unsigned y)). - apply eqm_samerepr. auto with ints. omega. + intros; unfold sub, add, neg. apply eqm_samerepr. + apply eqm_add; auto with ints. Qed. Theorem sub_idem: forall x, sub x x = zero. Proof. - intros; unfold sub. replace (unsigned x - unsigned x) with 0. - reflexivity. omega. + intros; unfold sub. unfold zero. decEq. omega. Qed. Theorem sub_add_l: forall x y z, sub (add x y) z = add (sub x z) y. @@ -938,13 +863,13 @@ Qed. Theorem mul_zero: forall x, mul x zero = zero. Proof. - intros; unfold mul. change (unsigned zero) with 0. + intros; unfold mul. rewrite unsigned_zero. unfold zero. decEq. ring. Qed. Theorem mul_one: forall x, mul x one = x. Proof. - intros; unfold mul. rewrite unsigned_one. + intros; unfold mul. rewrite unsigned_one. transitivity (repr (unsigned x)). decEq. ring. apply repr_unsigned. Qed. @@ -1007,6 +932,45 @@ Proof. apply eqm_mult; apply eqm_sym; apply eqm_signed_unsigned. Qed. +(** ** Properties of division and modulus *) + +Lemma modu_divu_Euclid: + forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y). +Proof. + intros. unfold add, mul, divu, modu. + transitivity (repr (unsigned x)). auto with ints. + apply eqm_samerepr. + set (x' := unsigned x). set (y' := unsigned y). + apply eqm_trans with ((x' / y') * y' + x' mod y'). + apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq. + generalize (unsigned_range y); intro. + assert (unsigned y <> 0). red; intro. + elim H. rewrite <- (repr_unsigned y). unfold zero. congruence. + unfold y'. omega. + auto with ints. +Qed. + +Theorem modu_divu: + forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y). +Proof. + intros. + assert (forall a b c, a = add b c -> c = sub a b). + intros. subst a. rewrite sub_add_l. rewrite sub_idem. + rewrite add_commut. rewrite add_zero. auto. + apply H0. apply modu_divu_Euclid. auto. +Qed. + +Theorem mods_divs: + forall x y, mods x y = sub x (mul (divs x y) y). +Proof. + intros; unfold mods, sub, mul, divs. + apply eqm_samerepr. + unfold Zmod_round. + apply eqm_sub. apply eqm_signed_unsigned. + apply eqm_unsigned_repr_r. + apply eqm_mult. auto with ints. apply eqm_signed_unsigned. +Qed. + (** ** Properties of binary decompositions *) Lemma Z_shift_add_bin_decomp: @@ -1021,45 +985,53 @@ Proof. generalize (H (Zpos p)); simpl. congruence. Qed. +Lemma Z_bin_decomp_shift_add: + forall b x, Z_bin_decomp (Z_shift_add b x) = (b, x). +Proof. + intros. + intros. unfold Z_shift_add. destruct b; destruct x; simpl; auto. + destruct p; simpl; auto. f_equal. f_equal. + rewrite <- Pplus_one_succ_r. apply Psucc_o_double_minus_one_eq_xO. +Qed. + Lemma Z_shift_add_inj: forall b1 x1 b2 x2, Z_shift_add b1 x1 = Z_shift_add b2 x2 -> b1 = b2 /\ x1 = x2. Proof. - intros until x2. - unfold Z_shift_add. - destruct b1; destruct b2; intros; - ((split; [reflexivity|omega]) || omegaContradiction). + intros. + assert ((b1, x1) = (b2, x2)). + repeat rewrite <- Z_bin_decomp_shift_add. rewrite H; auto. + split; congruence. Qed. Lemma Z_of_bits_exten: - forall n f1 f2, - (forall z, 0 <= z < Z_of_nat n -> f1 z = f2 z) -> - Z_of_bits n f1 = Z_of_bits n f2. + forall f1 f2 n i1 i2, + (forall i, 0 <= i < Z_of_nat n -> f1 (i + i1) = f2 (i + i2)) -> + Z_of_bits n f1 i1 = Z_of_bits n f2 i2. Proof. - induction n; intros. - reflexivity. - simpl. rewrite inj_S in H. decEq. apply H. omega. - apply IHn. intros; apply H. omega. + induction n; intros; simpl. + auto. + rewrite inj_S in H. decEq. apply (H 0). omega. + apply IHn. intros. + replace (i + Zsucc i1) with (Zsucc i + i1) by omega. + replace (i + Zsucc i2) with (Zsucc i + i2) by omega. + apply H. omega. Qed. -Opaque Zmult. - Lemma Z_of_bits_of_Z: - forall x, eqm (Z_of_bits wordsize (bits_of_Z wordsize x)) x. + forall x, eqm (Z_of_bits wordsize (bits_of_Z wordsize x) 0) x. Proof. assert (forall n x, exists k, - Z_of_bits n (bits_of_Z n x) = k * two_power_nat n + x). - induction n; intros. - rewrite two_power_nat_O. simpl. exists (-x). omega. - rewrite two_power_nat_S. simpl. - caseEq (Z_bin_decomp x). intros b y ZBD. simpl. - replace (Z_of_bits n (fun i => if zeq (i + 1) 0 then b else bits_of_Z n y (i + 1 - 1))) - with (Z_of_bits n (bits_of_Z n y)). - elim (IHn y). intros k1 EQ1. rewrite EQ1. - rewrite <- (Z_shift_add_bin_decomp x). - rewrite ZBD. simpl. - exists k1. - case b; unfold Z_shift_add; ring. + Z_of_bits n (bits_of_Z n x) 0 = k * two_power_nat n + x). + induction n; intros; simpl. + rewrite two_power_nat_O. exists (-x). omega. + rewrite two_power_nat_S. simpl bits_of_Z. caseEq (Z_bin_decomp x). intros b y ZBD. + rewrite zeq_true. destruct (IHn y) as [k EQ]. + replace (Z_of_bits n (fun i => if zeq i 0 then b else bits_of_Z n y (i - 1)) 1) + with (Z_of_bits n (bits_of_Z n y) 0). + rewrite EQ. exists k. + rewrite <- (Z_shift_add_bin_decomp x). rewrite ZBD. simpl fst; simpl snd. + unfold Z_shift_add; destruct b; ring. apply Z_of_bits_exten. intros. rewrite zeq_false. decEq. omega. omega. intro. exact (H wordsize x). @@ -1068,9 +1040,7 @@ Qed. Lemma bits_of_Z_zero: forall n x, bits_of_Z n 0 x = false. Proof. - induction n; simpl; intros. - auto. - case (zeq x 0); intro. auto. auto. + induction n; simpl; intros. auto. case (zeq x 0); intro. auto. auto. Qed. Remark Z_bin_decomp_2xm1: @@ -1078,73 +1048,90 @@ Remark Z_bin_decomp_2xm1: Proof. intros. caseEq (Z_bin_decomp (2 * x - 1)). intros b y EQ. generalize (Z_shift_add_bin_decomp (2 * x - 1)). - rewrite EQ; simpl. + rewrite EQ; simpl fst; simpl snd. replace (2 * x - 1) with (Z_shift_add true (x - 1)). intro. elim (Z_shift_add_inj _ _ _ _ H); intros. congruence. unfold Z_shift_add. omega. Qed. -Lemma bits_of_Z_mone: - forall n x, - 0 <= x < Z_of_nat n -> - bits_of_Z n (two_power_nat n - 1) x = true. +Lemma 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. induction n; intros. - simpl in H. omegaContradiction. - unfold bits_of_Z; fold bits_of_Z. - rewrite two_power_nat_S. rewrite Z_bin_decomp_2xm1. - rewrite inj_S in H. case (zeq x 0); intro. auto. - apply IHn. omega. + 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. + simpl. replace (two_p x) with (2 * two_p (x - 1)). 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. -Lemma Z_bin_decomp_shift_add: - forall b x, Z_bin_decomp (Z_shift_add b x) = (b, x). +Lemma bits_of_Z_mone: + forall x, + 0 <= x < Z_of_nat wordsize -> + bits_of_Z wordsize (modulus - 1) x = true. Proof. - intros. caseEq (Z_bin_decomp (Z_shift_add b x)); intros b' x' EQ. - generalize (Z_shift_add_bin_decomp (Z_shift_add b x)). - rewrite EQ; simpl fst; simpl snd. intro. - elim (Z_shift_add_inj _ _ _ _ H); intros. - congruence. + intros. unfold modulus. rewrite two_power_nat_two_p. + rewrite bits_of_Z_two_p. unfold proj_sumbool. apply zlt_true; omega. + omega. omega. Qed. -Lemma bits_of_Z_of_bits: - forall n f i, - 0 <= i < Z_of_nat n -> - bits_of_Z n (Z_of_bits n f) i = f i. -Proof. - induction n; intros; simpl. - simpl in H. omegaContradiction. - rewrite Z_bin_decomp_shift_add. - case (zeq i 0); intro. - congruence. - rewrite IHn. decEq. omega. rewrite inj_S in H. omega. -Qed. - Lemma Z_of_bits_range: - forall f, 0 <= Z_of_bits wordsize f < modulus. + forall f n i, 0 <= Z_of_bits n f i < two_power_nat n. Proof. - unfold max_unsigned, modulus. - generalize wordsize. induction n; simpl; intros. + induction n; simpl; intros. rewrite two_power_nat_O. omega. - rewrite two_power_nat_S. generalize (IHn (fun i => f (i + 1))). - set (x := Z_of_bits n (fun i => f (i + 1))). - intro. destruct (f 0); unfold Z_shift_add; omega. + rewrite two_power_nat_S. + generalize (IHn (Zsucc i)). + intro. destruct (f i); unfold Z_shift_add; omega. +Qed. + +Lemma Z_of_bits_range_1: + forall f i, 0 <= Z_of_bits wordsize f i < modulus. +Proof. + intros. apply Z_of_bits_range. Qed. -Hint Resolve Z_of_bits_range: ints. +Hint Resolve Z_of_bits_range_1: ints. Lemma Z_of_bits_range_2: - forall f, 0 <= Z_of_bits wordsize f <= max_unsigned. + forall f i, 0 <= Z_of_bits wordsize f i <= max_unsigned. Proof. intros. unfold max_unsigned. - generalize (Z_of_bits_range f). omega. + generalize (Z_of_bits_range_1 f i). omega. Qed. Hint Resolve Z_of_bits_range_2: ints. +Lemma bits_of_Z_of_bits_gen: + forall n f i j, + 0 <= i < Z_of_nat n -> + bits_of_Z n (Z_of_bits n f j) i = f (i + j). +Proof. + induction n; intros; simpl. + simpl in H. omegaContradiction. + rewrite Z_bin_decomp_shift_add. + destruct (zeq i 0). + f_equal. omega. + rewrite IHn. f_equal. omega. + rewrite inj_S in H. omega. +Qed. + +Lemma bits_of_Z_of_bits: + forall n f i, + 0 <= i < Z_of_nat n -> + bits_of_Z n (Z_of_bits n f 0) i = f i. +Proof. + intros. rewrite bits_of_Z_of_bits_gen; auto. decEq; omega. +Qed. + Lemma bits_of_Z_below: forall n x i, i < 0 -> bits_of_Z n x i = false. Proof. - induction n; simpl; intros. - reflexivity. + induction n; intros; simpl. auto. destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn. omega. omega. Qed. @@ -1153,48 +1140,91 @@ Lemma bits_of_Z_above: forall n x i, i >= Z_of_nat n -> bits_of_Z n x i = false. Proof. induction n; intros; simpl. - reflexivity. - destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn. + auto. + caseEq (Z_bin_decomp x); intros b x1 EQ. rewrite zeq_false. + rewrite IHn. + destruct x; simpl in EQ. inv EQ. auto. + destruct p; inv EQ; auto. + destruct p; inv EQ; auto. 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 = +Lemma bits_of_Z_of_bits_gen': + forall n f i j, + bits_of_Z n (Z_of_bits n f j) i = if zlt i 0 then false else if zle (Z_of_nat n) i then false - else f i. + else f (i + j). 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. + apply bits_of_Z_of_bits_gen. omega. Qed. -Opaque Zmult. - Lemma Z_of_bits_excl: - forall n f g h, - (forall i, 0 <= i < Z_of_nat n -> f i && g i = false) -> - (forall i, 0 <= i < Z_of_nat n -> f i || g i = h i) -> - Z_of_bits n f + Z_of_bits n g = Z_of_bits n h. + forall n f g h j, + (forall i, j <= i < j + Z_of_nat n -> f i && g i = false) -> + (forall i, j <= i < j + Z_of_nat n -> f i || g i = h i) -> + Z_of_bits n f j + Z_of_bits n g j = Z_of_bits n h j. Proof. induction n. intros; reflexivity. intros. simpl. rewrite inj_S in H. rewrite inj_S in H0. - rewrite <- (IHn (fun i => f(i+1)) (fun i => g(i+1)) (fun i => h(i+1))). - assert (0 <= 0 < Zsucc(Z_of_nat n)). omega. + rewrite <- (IHn f g h (Zsucc j)). + assert (j <= j < j + Zsucc(Z_of_nat n)). omega. unfold Z_shift_add. rewrite <- H0; auto. - set (F := Z_of_bits n (fun i => f(i + 1))). - set (G := Z_of_bits n (fun i => g(i + 1))). - caseEq (f 0); intros; caseEq (g 0); intros; simpl. - generalize (H 0 H1). rewrite H2; rewrite H3. simpl. intros; discriminate. + caseEq (f j); intros; caseEq (g j); intros; simpl orb. + generalize (H j H1). rewrite H2; rewrite H3. simpl andb; congruence. omega. omega. omega. intros; apply H. omega. intros; apply H0. omega. Qed. +Lemma Z_of_bits_compose: + forall f m n i, + Z_of_bits (m + n) f i = + Z_of_bits n f (i + Z_of_nat m) * two_power_nat m + + Z_of_bits m f i. +Proof. + induction m; intros. + simpl. repeat rewrite Zplus_0_r. rewrite two_power_nat_O. omega. + rewrite inj_S. rewrite two_power_nat_S. simpl Z_of_bits. + rewrite IHm. replace (i + Zsucc (Z_of_nat m)) with (Zsucc i + Z_of_nat m) by omega. + unfold Z_shift_add. destruct (f i); ring. +Qed. + +Lemma Z_of_bits_truncate: + forall f n i, + eqm (Z_of_bits (wordsize + n) f i) (Z_of_bits wordsize f i). +Proof. + intros. exists (Z_of_bits n f (i + Z_of_nat wordsize)). + rewrite Z_of_bits_compose. fold modulus. auto. +Qed. + +Lemma Z_of_bits_false: + forall f n i, + (forall j, i <= j < i + Z_of_nat n -> f j = false) -> + Z_of_bits n f i = 0. +Proof. + induction n; intros; simpl. auto. + rewrite inj_S in H. rewrite H. rewrite IHn. auto. + intros; apply H; omega. omega. +Qed. + +Lemma Z_of_bits_true: + forall f n i, + (forall j, i <= j < i + Z_of_nat n -> f j = true) -> + Z_of_bits n f i = two_power_nat n - 1. +Proof. + induction n; intros. + simpl. auto. + rewrite two_power_nat_S. simpl Z_of_bits. rewrite inj_S in H. + rewrite H. rewrite IHn. unfold Z_shift_add. omega. + intros; apply H. omega. omega. +Qed. + (** ** Properties of bitwise and, or, xor *) Lemma bitwise_binop_commut: @@ -1203,8 +1233,7 @@ Lemma bitwise_binop_commut: forall x y, bitwise_binop f x y = bitwise_binop f y x. Proof. - unfold bitwise_binop; intros. - decEq. apply Z_of_bits_exten; intros. auto. + unfold bitwise_binop; intros. decEq; apply Z_of_bits_exten; intros. auto. Qed. Lemma bitwise_binop_assoc: @@ -1214,10 +1243,9 @@ Lemma bitwise_binop_assoc: bitwise_binop f (bitwise_binop f x y) z = bitwise_binop f x (bitwise_binop f y z). Proof. - unfold bitwise_binop; intros. - repeat rewrite unsigned_repr; auto with ints. - decEq. apply Z_of_bits_exten; intros. - repeat (rewrite bits_of_Z_of_bits; auto). + unfold bitwise_binop; intros. repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite Zplus_0_r. repeat rewrite bits_of_Z_of_bits; auto. Qed. Lemma bitwise_binop_idem: @@ -1227,10 +1255,8 @@ Lemma bitwise_binop_idem: bitwise_binop f x x = x. Proof. unfold bitwise_binop; intros. - transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))). - decEq. apply Z_of_bits_exten; intros. auto. - transitivity (repr (unsigned x)). - apply eqm_samerepr. apply Z_of_bits_of_Z. apply repr_unsigned. + apply eqm_repr_eq. eapply eqm_trans. 2: apply Z_of_bits_of_Z. + apply eqm_refl2. apply Z_of_bits_exten. auto. Qed. Theorem and_commut: forall x y, and x y = and y x. @@ -1241,7 +1267,7 @@ Proof (bitwise_binop_assoc andb andb_assoc). Theorem and_zero: forall x, and x zero = zero. Proof. - intros. unfold and, bitwise_binop. + 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. @@ -1250,18 +1276,38 @@ Qed. Theorem and_mone: forall x, and x mone = x. Proof. 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. + apply eqm_repr_eq. 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. + omega. Qed. Theorem and_idem: forall x, and x x = x. Proof. - assert (forall b, b && b = b). - destruct b; reflexivity. - exact (bitwise_binop_idem andb H). + intros. apply (bitwise_binop_idem andb). destruct a; auto. +Qed. + +Theorem add_and: + forall x y z, + and y z = zero -> + add (and x y) (and x z) = and x (or y z). +Proof. + intros. unfold add, and, bitwise_binop. + repeat rewrite unsigned_repr; auto with ints. decEq. + 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 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). + rewrite H. rewrite unsigned_zero. + rewrite bits_of_Z_zero. apply andb_b_false. + unfold and, bitwise_binop. rewrite unsigned_repr; auto with ints. + rewrite bits_of_Z_of_bits. reflexivity. auto. + rewrite <- demorgan1. + unfold or, bitwise_binop. rewrite unsigned_repr; auto with ints. + rewrite bits_of_Z_of_bits; auto. Qed. Theorem or_commut: forall x y, or x y = or y x. @@ -1272,29 +1318,24 @@ Proof (bitwise_binop_assoc orb orb_assoc). Theorem or_zero: forall x, or x zero = x. Proof. - intros. unfold or, bitwise_binop. - transitivity (repr(unsigned x)). - apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z. + intros. unfold or, bitwise_binop. + apply eqm_repr_eq. 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. + rewrite unsigned_zero. rewrite bits_of_Z_zero. apply orb_b_false. Qed. Theorem or_mone: forall x, or x mone = mone. Proof. intros. unfold or, bitwise_binop. - transitivity (repr(unsigned mone)). - apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z. + apply eqm_repr_eq. 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. + rewrite unsigned_mone. rewrite bits_of_Z_mone. apply orb_b_true. + omega. Qed. Theorem or_idem: forall x, or x x = x. Proof. - assert (forall b, b || b = b). - destruct b; reflexivity. - exact (bitwise_binop_idem orb H). + intros. apply (bitwise_binop_idem orb). destruct a; auto. Qed. Theorem and_or_distrib: @@ -1302,9 +1343,9 @@ Theorem and_or_distrib: and x (or y z) = or (and x y) (and x z). Proof. intros; unfold and, or, bitwise_binop. - decEq. repeat rewrite unsigned_repr; auto with ints. - apply Z_of_bits_exten; intros. - repeat rewrite bits_of_Z_of_bits; auto. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits; repeat rewrite Zplus_0_r; auto. apply demorgan1. Qed. @@ -1313,29 +1354,24 @@ Proof (bitwise_binop_commut xorb xorb_comm). Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z). Proof. - assert (forall a b c, xorb a (xorb b c) = xorb (xorb a b) c). - symmetry. apply xorb_assoc. - exact (bitwise_binop_assoc xorb H). + intros. apply (bitwise_binop_assoc xorb). + intros. symmetry. apply xorb_assoc. Qed. Theorem xor_zero: forall x, xor x zero = x. Proof. intros. unfold xor, bitwise_binop. - transitivity (repr(unsigned x)). - apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z. + apply eqm_repr_eq. 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_repr_eq. 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. @@ -1349,9 +1385,9 @@ Theorem and_xor_distrib: and x (xor y z) = xor (and x y) (and x z). Proof. intros; unfold and, xor, bitwise_binop. - decEq. repeat rewrite unsigned_repr; auto with ints. - apply Z_of_bits_exten; intros. - repeat rewrite bits_of_Z_of_bits; auto. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits; repeat rewrite Zplus_0_r; auto. assert (forall a b c, a && (xorb b c) = xorb (a && b) (a && c)). destruct a; destruct b; destruct c; reflexivity. auto. @@ -1363,112 +1399,13 @@ Proof. intros. unfold not. rewrite xor_assoc. rewrite xor_idem. apply xor_zero. Qed. -(** ** Properties of shifts and rotates *) - -Lemma Z_of_bits_shift: - forall n f, - exists k, - Z_of_bits n (fun i => f (i - 1)) = - k * two_power_nat n + Z_shift_add (f (-1)) (Z_of_bits n f). -Proof. - induction n; intros. - simpl. rewrite two_power_nat_O. unfold Z_shift_add. - exists (if f (-1) then (-1) else 0). - destruct (f (-1)); omega. - rewrite two_power_nat_S. simpl. - elim (IHn (fun i => f (i + 1))). intros k' EQ. - replace (Z_of_bits n (fun i => f (i - 1 + 1))) - with (Z_of_bits n (fun i => f (i + 1 - 1))) in EQ. - rewrite EQ. - change (-1 + 1) with 0. - exists k'. - unfold Z_shift_add; destruct (f (-1)); destruct (f 0); ring. - apply Z_of_bits_exten; intros. - decEq. omega. -Qed. - -Lemma Z_of_bits_shifts: - forall m f, - 0 <= m -> - (forall i, i < 0 -> f i = false) -> - eqm (Z_of_bits wordsize (fun i => f (i - m))) - (two_p m * Z_of_bits wordsize f). -Proof. - intros. pattern m. apply natlike_ind. - apply eqm_refl2. transitivity (Z_of_bits wordsize f). - apply Z_of_bits_exten; intros. decEq. omega. - simpl two_p. omega. - intros. rewrite two_p_S; auto. - set (f' := fun i => f (i - x)). - apply eqm_trans with (Z_of_bits wordsize (fun i => f' (i - 1))). - apply eqm_refl2. apply Z_of_bits_exten; intros. - unfold f'. decEq. omega. - apply eqm_trans with (Z_shift_add (f' (-1)) (Z_of_bits wordsize f')). - exact (Z_of_bits_shift wordsize f'). - unfold f'. unfold Z_shift_add. rewrite H0. - rewrite <- Zmult_assoc. apply eqm_mult. apply eqm_refl. - apply H2. omega. assumption. -Qed. - -Lemma shl_mul_two_p: - forall x y, - shl x y = mul x (repr (two_p (unsigned y))). -Proof. - intros. unfold shl, mul. - apply eqm_samerepr. - eapply eqm_trans. - apply Z_of_bits_shifts. - generalize (unsigned_range y). omega. - intros; apply bits_of_Z_below; auto. - rewrite Zmult_comm. apply eqm_mult. - apply Z_of_bits_of_Z. apply eqm_unsigned_repr. -Qed. +(** ** Properties of shifts *) Theorem shl_zero: forall x, shl x zero = x. Proof. - intros. rewrite shl_mul_two_p. - change (repr (two_p (unsigned zero))) with one. - apply mul_one. -Qed. - -Theorem shl_mul: - forall x y, - shl x y = mul x (shl one y). -Proof. - intros. - assert (shl one y = repr (two_p (unsigned y))). - rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto. - 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 iwordsize = true -> - shl x n = rolm x n (shl mone n). -Proof. - 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) _ 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. - rewrite unsigned_mone. - rewrite bits_of_Z_mone. rewrite andb_b_true. decEq. - rewrite Zmod_small. auto. omega. omega. + intros. unfold shl. rewrite unsigned_zero. simpl (-0). + transitivity (repr (unsigned x)). apply eqm_samerepr. apply Z_of_bits_of_Z. + auto with ints. Qed. Lemma bitwise_binop_shl: @@ -1477,13 +1414,14 @@ Lemma bitwise_binop_shl: bitwise_binop f (shl x n) (shl y n) = shl (bitwise_binop f x y) n. Proof. intros. unfold bitwise_binop, shl. - decEq. repeat rewrite unsigned_repr; auto with ints. - apply Z_of_bits_exten; intros. - case (zlt (z - unsigned n) 0); intro. - transitivity false. repeat rewrite bits_of_Z_of_bits; auto. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite Zplus_0_r. + destruct (zlt (i + -unsigned n) 0). + rewrite bits_of_Z_of_bits_gen; auto. + rewrite bits_of_Z_of_bits_gen; auto. repeat rewrite bits_of_Z_below; auto. - rewrite bits_of_Z_below; auto. - repeat rewrite bits_of_Z_of_bits; auto. + repeat rewrite bits_of_Z_of_bits_gen; auto. repeat rewrite Zplus_0_r. auto. generalize (unsigned_range n). omega. Qed. @@ -1494,6 +1432,27 @@ Proof. unfold and; intros. apply bitwise_binop_shl. reflexivity. Qed. +Theorem or_shl: + forall x y n, + or (shl x n) (shl y n) = shl (or x y) n. +Proof. + unfold or; intros. apply bitwise_binop_shl. reflexivity. +Qed. + +Theorem xor_shl: + forall x y n, + xor (shl x n) (shl y n) = shl (xor x y) n. +Proof. + unfold xor; intros. apply bitwise_binop_shl. reflexivity. +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_shl: forall x y z, @@ -1510,16 +1469,59 @@ Proof. 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). + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros n R. + rewrite bits_of_Z_of_bits_gen'. + destruct (zlt (n + - z') 0). symmetry. apply bits_of_Z_below. omega. - destruct (zle (Z_of_nat wordsize) (n - z')). + destruct (zle (Z_of_nat wordsize) (n + - z')). symmetry. apply bits_of_Z_below. omega. decEq. omega. generalize two_wordsize_max_unsigned; omega. - apply Z_of_bits_range_2. +Qed. + +Theorem shru_zero: forall x, shru x zero = x. +Proof. + intros. unfold shru. rewrite unsigned_zero. + transitivity (repr (unsigned x)). apply eqm_samerepr. apply Z_of_bits_of_Z. + auto with ints. +Qed. + +Lemma bitwise_binop_shru: + forall f x y n, + f false false = false -> + bitwise_binop f (shru x n) (shru y n) = shru (bitwise_binop f x y) n. +Proof. + intros. unfold bitwise_binop, shru. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite Zplus_0_r. + rewrite bits_of_Z_of_bits_gen; auto. + rewrite bits_of_Z_of_bits_gen; auto. + destruct (zlt (i + unsigned n) (Z_of_nat wordsize)). + rewrite bits_of_Z_of_bits. auto. generalize (unsigned_range n); omega. + repeat rewrite bits_of_Z_above; auto. +Qed. + +Theorem and_shru: + forall x y n, + and (shru x n) (shru y n) = shru (and x y) n. +Proof. + unfold and; intros. apply bitwise_binop_shru. reflexivity. +Qed. + +Theorem or_shru: + forall x y n, + or (shru x n) (shru y n) = shru (or x y) n. +Proof. + unfold or; intros. apply bitwise_binop_shru. reflexivity. +Qed. + +Theorem xor_shru: + forall x y n, + xor (shru x n) (shru y n) = shru (xor x y) n. +Proof. + unfold xor; intros. apply bitwise_binop_shru. reflexivity. Qed. Theorem shru_shru: @@ -1536,66 +1538,57 @@ Proof. 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'. + intros. repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten. intros n R. + rewrite bits_of_Z_of_bits_gen'. destruct (zlt (n + z') 0). omegaContradiction. destruct (zle (Z_of_nat wordsize) (n + z')). symmetry. apply bits_of_Z_above. omega. decEq. omega. generalize two_wordsize_max_unsigned; omega. - apply Z_of_bits_range_2. Qed. -Theorem shru_rolm: - forall x n, - ltu n iwordsize = true -> - shru x n = rolm x (sub iwordsize n) (shru mone n). +Theorem shr_zero: forall x, shr x zero = x. Proof. - 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. rewrite unsigned_repr_wordsize. - rewrite unsigned_repr. - case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro LT2. - 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. - 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. apply wordsize_max_unsigned. + intros. unfold shr. rewrite unsigned_zero. + 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 zlt_true. auto. omega. + auto with ints. Qed. -Lemma bitwise_binop_shru: +Lemma bitwise_binop_shr: forall f x y n, - f false false = false -> - bitwise_binop f (shru x n) (shru y n) = shru (bitwise_binop f x y) n. + bitwise_binop f (shr x n) (shr y n) = shr (bitwise_binop f x y) n. Proof. - intros. unfold bitwise_binop, shru. - decEq. repeat rewrite unsigned_repr; auto with ints. - apply Z_of_bits_exten; intros. - case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro. - repeat rewrite bits_of_Z_of_bits; auto. - generalize (unsigned_range n); omega. - transitivity false. repeat rewrite bits_of_Z_of_bits; auto. - repeat rewrite bits_of_Z_above; auto. - rewrite bits_of_Z_above; auto. + intros. unfold bitwise_binop, shr. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits_gen; repeat rewrite Zplus_0_r; auto. + generalize (unsigned_range n); intro. + destruct (zlt (i + unsigned n) (Z_of_nat wordsize)); omega. Qed. -Lemma and_shru: +Theorem and_shr: forall x y n, - and (shru x n) (shru y n) = shru (and x y) n. + and (shr x n) (shr y n) = shr (and x y) n. Proof. - unfold and; intros. apply bitwise_binop_shru. reflexivity. + unfold and; intros. apply bitwise_binop_shr. +Qed. + +Theorem or_shr: + forall x y n, + or (shr x n) (shr y n) = shr (or x y) n. +Proof. + unfold or; intros. apply bitwise_binop_shr. +Qed. + +Theorem xor_shr: + forall x y n, + xor (shr x n) (shr y n) = shr (xor x y) n. +Proof. + unfold xor; intros. apply bitwise_binop_shr. Qed. Theorem shr_shr: @@ -1608,30 +1601,111 @@ Proof. intros. unfold shr, add. generalize (ltu_inv _ _ H). generalize (ltu_inv _ _ H0). - rewrite unsigned_repr_wordsize. - set (x' := signed x). + rewrite unsigned_repr_wordsize. + set (x' := unsigned 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. - generalize min_signed_neg; omega. - generalize max_signed_pos; omega. - apply two_p_gt_ZERO. omega. omega. omega. + intros. repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros n R. + destruct (zlt (n + z') (Z_of_nat wordsize)). + rewrite bits_of_Z_of_bits_gen. + rewrite (Zplus_comm y' z'). rewrite Zplus_assoc. auto. + omega. + rewrite bits_of_Z_of_bits_gen. + decEq. symmetry. rewrite zlt_false. + destruct (zeq y' 0). rewrite zlt_true; omega. rewrite zlt_false; omega. + omega. omega. generalize two_wordsize_max_unsigned; omega. Qed. -Theorem rol_zero: - forall x, - rol x zero = x. +Remark two_p_m1_range: + forall n, + 0 <= n <= Z_of_nat wordsize -> + 0 <= two_p n - 1 <= 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)). 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 iwordsize = true -> + shru (shl x y) y = and x (repr (two_p (Z_of_nat wordsize - unsigned y) - 1)). +Proof. + intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize. intros. + unfold and, bitwise_binop, shl, shru. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. rewrite Zplus_0_r. + rewrite bits_of_Z_two_p. + destruct (zlt (i + unsigned y) (Z_of_nat wordsize)). + rewrite bits_of_Z_of_bits_gen. 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. +Qed. + +(** ** Properties of rotations *) + +Theorem shl_rolm: + forall x n, + ltu n iwordsize = true -> + shl x n = rolm x n (shl mone n). +Proof. + intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize; intros. + unfold shl, rolm, rol, and, bitwise_binop. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. rewrite Zplus_0_r. + repeat rewrite bits_of_Z_of_bits_gen; auto. + destruct (zlt i (unsigned n)). + assert (i + - unsigned n < 0). omega. + rewrite (bits_of_Z_below wordsize (unsigned x) _ H2). + rewrite (bits_of_Z_below wordsize (unsigned mone) _ H2). + symmetry. apply andb_b_false. + assert (0 <= i + - unsigned n < Z_of_nat wordsize). + generalize (unsigned_range n). omega. + rewrite unsigned_mone. + rewrite bits_of_Z_mone; auto. rewrite andb_b_true. decEq. + rewrite Zmod_small. omega. omega. +Qed. + +Theorem shru_rolm: + forall x n, + ltu n iwordsize = true -> + shru x n = rolm x (sub iwordsize n) (shru mone n). +Proof. + intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize. intro. + unfold shru, rolm, rol, and, bitwise_binop. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. rewrite Zplus_0_r. + repeat rewrite bits_of_Z_of_bits_gen; auto. + unfold sub. rewrite unsigned_repr_wordsize. + rewrite unsigned_repr. + case (zlt (i + unsigned n) (Z_of_nat wordsize)); intro LT2. + rewrite unsigned_mone. rewrite bits_of_Z_mone. rewrite andb_b_true. + decEq. + replace (i + - (Z_of_nat wordsize - unsigned n)) + with ((i + unsigned n) + (-1) * Z_of_nat wordsize) by omega. + rewrite Z_mod_plus. symmetry. apply Zmod_small. + generalize (unsigned_range n). omega. omega. omega. + 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. apply wordsize_max_unsigned. +Qed. + +Theorem rol_zero: + forall x, + rol x zero = x. Proof. 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. + replace (i + - 0) with (i + 0) by omega. apply Zmod_small. omega. apply repr_unsigned. Qed. @@ -1640,10 +1714,12 @@ Lemma bitwise_binop_rol: bitwise_binop f (rol x n) (rol y n) = rol (bitwise_binop f x y) n. Proof. intros. unfold bitwise_binop, rol. - 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. generalize wordsize_pos; omega. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits_gen. + repeat rewrite Zplus_0_r. auto. + apply Z_mod_lt. generalize wordsize_pos; omega. + omega. omega. Qed. Theorem rol_and: @@ -1653,16 +1729,31 @@ Proof. intros. symmetry. unfold and. apply bitwise_binop_rol. Qed. +Theorem rol_or: + forall x y n, + rol (or x y) n = or (rol x n) (rol y n). +Proof. + intros. symmetry. unfold or. apply bitwise_binop_rol. +Qed. + +Theorem rol_xor: + forall x y n, + rol (xor x y) n = xor (rol x n) (rol y n). +Proof. + intros. symmetry. unfold xor. apply bitwise_binop_rol. +Qed. + Theorem rol_rol: forall x n m, Zdivide (Z_of_nat wordsize) modulus -> rol (rol x n) m = rol x (modu (add n m) iwordsize). Proof. - intros. unfold rol. decEq. - repeat (rewrite unsigned_repr; auto with ints). - apply Z_of_bits_exten; intros. - repeat rewrite bits_of_Z_of_bits; auto. - decEq. unfold modu, add. + intros. unfold rol. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits; repeat rewrite Zplus_0_r; auto. + rewrite bits_of_Z_of_bits_gen. decEq. + unfold modu, add. set (W := Z_of_nat wordsize). set (M := unsigned m); set (N := unsigned n). assert (W > 0). unfold W; generalize wordsize_pos; omega. @@ -1670,11 +1761,11 @@ Proof. intros. eapply eqmod_divides. apply eqm_unsigned_repr. assumption. apply eqmod_mod_eq. auto. replace (unsigned iwordsize) with W. - apply eqmod_trans with (z - (N + M) mod W). - apply eqmod_trans with ((z - M) - N). + apply eqmod_trans with (i - (N + M) mod W). + apply eqmod_trans with ((i - M) - N). apply eqmod_sub. apply eqmod_sym. apply eqmod_mod. auto. apply eqmod_refl. - replace (z - M - N) with (z - (N + M)). + replace (i - M - N) with (i - (N + M)). apply eqmod_sub. apply eqmod_refl. apply eqmod_mod. auto. omega. apply eqmod_sub. apply eqmod_refl. @@ -1705,13 +1796,6 @@ Proof. rewrite rol_rol. reflexivity. auto. Qed. -Theorem rol_or: - forall x y n, - rol (or x y) n = or (rol x n) (rol y n). -Proof. - intros. symmetry. unfold or. apply bitwise_binop_rol. -Qed. - Theorem or_rolm: forall x n m1 m2, or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2). @@ -1727,8 +1811,8 @@ Proof. intros. unfold ror, rol, sub. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize. - intro. rewrite unsigned_repr. - decEq. apply Z_of_bits_exten. intros. decEq. + intro. repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. decEq. apply eqmod_mod_eq. omega. exists 1. omega. generalize wordsize_pos; generalize wordsize_max_unsigned; omega. @@ -1748,9 +1832,9 @@ Proof. intros. 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. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten. intros i iRANGE. rewrite Zplus_0_r. + repeat rewrite bits_of_Z_of_bits_gen; 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. @@ -1759,66 +1843,16 @@ Proof. 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. + 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 (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. - 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 two_p_m1_range: - forall n, - 0 <= n <= Z_of_nat wordsize -> - 0 <= two_p n - 1 <= 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)). 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 iwordsize = true -> - shru (shl x y) y = and x (repr (two_p (Z_of_nat wordsize - unsigned y) - 1)). -Proof. - 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 *) +(** ** Properties of [Z_one_bits] and [is_power2]. *) Fixpoint powerserie (l: list Z): Z := match l with @@ -1961,6 +1995,50 @@ Proof. apply two_p_range. auto. Qed. +(** ** Relation between bitwise operations and multiplications / divisions by powers of 2 *) + +(** Left shifts and multiplications by powers of 2. *) + +Lemma Z_of_bits_shift_left: + forall f m, + m >= 0 -> + (forall i, i < 0 -> f i = false) -> + eqm (Z_of_bits wordsize f (-m)) (two_p m * Z_of_bits wordsize f 0). +Proof. + intros. + set (m' := nat_of_Z m). + assert (Z_of_nat m' = m). apply nat_of_Z_eq. auto. + generalize (Z_of_bits_compose f m' wordsize (-m)). rewrite H1. + replace (-m+m) with 0 by omega. rewrite two_power_nat_two_p. rewrite H1. + replace (Z_of_bits m' f (-m)) with 0. intro EQ. + eapply eqm_trans. apply eqm_sym. eapply Z_of_bits_truncate with (n := m'). + rewrite plus_comm. rewrite EQ. apply eqm_refl2. ring. + symmetry. apply Z_of_bits_false. rewrite H1. intros. apply H0. omega. +Qed. + +Lemma shl_mul_two_p: + forall x y, + shl x y = mul x (repr (two_p (unsigned y))). +Proof. + intros. unfold shl, mul. apply eqm_samerepr. + eapply eqm_trans. + apply Z_of_bits_shift_left. + generalize (unsigned_range y). omega. + intros; apply bits_of_Z_below; auto. + rewrite Zmult_comm. apply eqm_mult. + apply Z_of_bits_of_Z. apply eqm_unsigned_repr. +Qed. + +Theorem shl_mul: + forall x y, + shl x y = mul x (shl one y). +Proof. + intros. + assert (shl one y = repr (two_p (unsigned y))). + rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto. + rewrite H. apply shl_mul_two_p. +Qed. + Theorem mul_pow2: forall x n logn, is_power2 n = Some logn -> @@ -1971,47 +2049,26 @@ Proof. auto. Qed. -Lemma Z_of_bits_shift_rev: - forall n f, - (forall i, i >= Z_of_nat n -> f i = false) -> - Z_of_bits n f = Z_shift_add (f 0) (Z_of_bits n (fun i => f(i + 1))). -Proof. - induction n; intros. - simpl. rewrite H. reflexivity. unfold Z_of_nat. omega. - simpl. rewrite (IHn (fun i => f (i + 1))). - reflexivity. - intros. apply H. rewrite inj_S. omega. -Qed. +(** Unsigned right shifts and unsigned divisions by powers of 2. *) -Lemma Z_of_bits_shifts_rev: +Lemma Z_of_bits_shift_right: forall m f, - 0 <= m -> + m >= 0 -> (forall i, i >= Z_of_nat wordsize -> f i = false) -> exists k, - Z_of_bits wordsize f = k + two_p m * Z_of_bits wordsize (fun i => f(i + m)) - /\ 0 <= k < two_p m. + Z_of_bits wordsize f 0 = k + two_p m * Z_of_bits wordsize f m /\ 0 <= k < two_p m. Proof. - intros. pattern m. apply natlike_ind. - exists 0. change (two_p 0) with 1. split. - transitivity (Z_of_bits wordsize (fun i => f (i + 0))). - apply Z_of_bits_exten. intros. decEq. omega. - omega. omega. - intros x POSx [k [EQ1 RANGE1]]. - set (f' := fun i => f (i + x)) in *. - assert (forall i, i >= Z_of_nat wordsize -> f' i = false). - intros. unfold f'. apply H0. omega. - generalize (Z_of_bits_shift_rev wordsize f' H1). intro. - rewrite EQ1. rewrite H2. - set (z := Z_of_bits wordsize (fun i => f (i + Zsucc x))). - replace (Z_of_bits wordsize (fun i => f' (i + 1))) with z. - rewrite two_p_S. - case (f' 0); unfold Z_shift_add. - exists (k + two_p x). split. ring. omega. - exists k. split. ring. omega. - auto. - unfold z. apply Z_of_bits_exten; intros. unfold f'. - decEq. omega. - auto. + intros. + set (m' := nat_of_Z m). + assert (Z_of_nat m' = m). apply nat_of_Z_eq. auto. + generalize (Z_of_bits_compose f m' wordsize 0). + rewrite two_power_nat_two_p. rewrite H1. + rewrite plus_comm. rewrite Z_of_bits_compose. + replace (Z_of_bits m' f (0 + Z_of_nat wordsize)) with 0. + repeat rewrite Zplus_0_l. intros EQ. + exists (Z_of_bits m' f 0); split. rewrite EQ. ring. + rewrite <- H1. rewrite <- two_power_nat_two_p. apply Z_of_bits_range. + symmetry. apply Z_of_bits_false. intros. apply H0. omega. Qed. Lemma shru_div_two_p: @@ -2020,34 +2077,14 @@ Lemma shru_div_two_p: Proof. intros. unfold shru. set (x' := unsigned x). set (y' := unsigned y). - elim (Z_of_bits_shifts_rev y' (bits_of_Z wordsize x')). - intros k [EQ RANGE]. - replace (Z_of_bits wordsize (bits_of_Z wordsize x')) with x' in EQ. - rewrite Zplus_comm in EQ. rewrite Zmult_comm in EQ. - generalize (Zdiv_unique _ _ _ _ EQ RANGE). intros. - rewrite H. auto. - apply eqm_small_eq. apply eqm_sym. apply Z_of_bits_of_Z. - unfold x'. apply unsigned_range. - auto with ints. - generalize (unsigned_range y). unfold y'. omega. - intros. apply bits_of_Z_above. auto. -Qed. - -Theorem shru_zero: - forall x, shru x zero = x. -Proof. - intros. rewrite shru_div_two_p. change (two_p (unsigned zero)) with 1. - transitivity (repr (unsigned x)). decEq. apply Zdiv_unique with 0. - omega. omega. auto with ints. -Qed. - -Theorem shr_zero: - forall x, shr x zero = x. -Proof. - intros. unfold shr. change (two_p (unsigned zero)) with 1. - replace (signed x / 1) with (signed x). - apply repr_signed. - symmetry. apply Zdiv_unique with 0. omega. omega. + destruct (Z_of_bits_shift_right y' (bits_of_Z wordsize x')) as [k [EQ RANGE]]. + generalize (unsigned_range y). unfold y'; omega. + intros. rewrite bits_of_Z_above; auto. + decEq. symmetry. apply Zdiv_unique with k; auto. + transitivity (Z_of_bits wordsize (bits_of_Z wordsize x') 0). + apply eqm_small_eq. apply eqm_sym. apply Z_of_bits_of_Z. + unfold x'; auto with ints. auto with ints. + rewrite EQ. ring. Qed. Theorem divu_pow2: @@ -2059,41 +2096,105 @@ Proof. symmetry. unfold divu. rewrite H0. apply shru_div_two_p. Qed. -Lemma modu_divu_Euclid: - forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y). +(** Signed right shifts and signed divisions by powers of 2. *) + +Lemma Z_of_bits_shift_right_neg: + forall m f, + m >= 0 -> + (forall i, i >= Z_of_nat wordsize -> f i = true) -> + exists k, + Z_of_bits wordsize f 0 - modulus = + k + two_p m * (Z_of_bits wordsize f m - modulus) + /\ 0 <= k < two_p m. Proof. - intros. unfold add, mul, divu, modu. - transitivity (repr (unsigned x)). auto with ints. - apply eqm_samerepr. - set (x' := unsigned x). set (y' := unsigned y). - apply eqm_trans with ((x' / y') * y' + x' mod y'). - apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq. - generalize (unsigned_range y); intro. - assert (unsigned y <> 0). red; intro. - elim H. rewrite <- (repr_unsigned y). unfold zero. congruence. - unfold y'. omega. - auto with ints. + intros. + set (m' := nat_of_Z m). + assert (Z_of_nat m' = m). apply nat_of_Z_eq. auto. + generalize (Z_of_bits_compose f m' wordsize 0). + rewrite two_power_nat_two_p. rewrite H1. + rewrite plus_comm. rewrite Z_of_bits_compose. + repeat rewrite Zplus_0_l. fold modulus. + replace (Z_of_bits m' f (Z_of_nat wordsize)) with (two_p m - 1). + intros EQ. + exists (Z_of_bits m' f 0); split. + replace (Z_of_bits wordsize f 0) + with (Z_of_bits wordsize f m * two_p m + Z_of_bits m' f 0 - (two_p m - 1) * modulus) + by omega. + ring. + rewrite <- H1. rewrite <- two_power_nat_two_p. apply Z_of_bits_range. + rewrite <- H1. rewrite <- two_power_nat_two_p. + symmetry. apply Z_of_bits_true. intros. apply H0. omega. +Qed. + +Lemma sign_bit_of_Z_rec: + forall n x, + 0 <= x < two_power_nat (S n) -> + bits_of_Z (S n) x (Z_of_nat n) = if zlt x (two_power_nat n) then false else true. +Proof. + induction n; intros. + rewrite two_power_nat_S in H. rewrite two_power_nat_O in *. simpl. + caseEq (Z_bin_decomp x); intros b x1 ZBD. rewrite zeq_true. + generalize (Z_shift_add_bin_decomp x). rewrite ZBD; simpl. intros. subst x. + unfold Z_shift_add in *. + destruct b. rewrite zlt_false. auto. omega. rewrite zlt_true. auto. omega. + rewrite inj_S. remember (S n) as sn. simpl. rewrite two_power_nat_S in H. + generalize (Z_shift_add_bin_decomp x). destruct (Z_bin_decomp x) as [b x1]. + simpl. intros. rewrite zeq_false. + replace (Zsucc (Z_of_nat n) - 1) with (Z_of_nat n). rewrite IHn. + rewrite <- H0. subst sn. rewrite two_power_nat_S. + destruct (zlt x1 (two_power_nat n)). + rewrite zlt_true. auto. unfold Z_shift_add; destruct b; omega. + rewrite zlt_false. auto. unfold Z_shift_add; destruct b; omega. + subst x. unfold Z_shift_add in H. destruct b; omega. + omega. omega. Qed. -Theorem modu_divu: - forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y). +Lemma sign_bit_of_Z: + forall x, + bits_of_Z wordsize (unsigned x) (Z_of_nat wordsize - 1) = + if zlt (unsigned x) half_modulus then false else true. Proof. intros. - assert (forall a b c, a = add b c -> c = sub a b). - intros. subst a. rewrite sub_add_l. rewrite sub_idem. - rewrite add_commut. rewrite add_zero. auto. - apply H0. apply modu_divu_Euclid. auto. + rewrite half_modulus_power. + set (w1 := nat_of_Z (Z_of_nat wordsize - 1)). + assert (Z_of_nat wordsize - 1 = Z_of_nat w1). + unfold w1. rewrite nat_of_Z_eq; auto. generalize wordsize_pos; omega. + assert (wordsize = 1 + w1)%nat. + apply inj_eq_rev. rewrite inj_plus. simpl (Z_of_nat 1). omega. + rewrite H. rewrite <- two_power_nat_two_p. rewrite H0. + apply sign_bit_of_Z_rec. simpl in H0; rewrite <- H0. auto with ints. Qed. -Theorem mods_divs: - forall x y, mods x y = sub x (mul (divs x y) y). -Proof. - intros; unfold mods, sub, mul, divs. - apply eqm_samerepr. - unfold Zmod_round. - apply eqm_sub. apply eqm_signed_unsigned. - apply eqm_unsigned_repr_r. - apply eqm_mult. auto with ints. apply eqm_signed_unsigned. +Lemma shr_div_two_p: + forall x y, + shr x y = repr (signed x / two_p (unsigned y)). +Proof. + intros. unfold shr. + generalize (sign_bit_of_Z x); intro SIGN. + unfold signed. destruct (zlt (unsigned x) half_modulus). +(* positive case *) + rewrite <- shru_div_two_p. unfold shru. decEq; apply Z_of_bits_exten; intros. + destruct (zlt (i + unsigned y) (Z_of_nat wordsize)). auto. + rewrite SIGN. symmetry. apply bits_of_Z_above. auto. +(* negative case *) + set (x' := unsigned x) in *. set (y' := unsigned y) in *. + set (f := fun i => bits_of_Z wordsize x' + (if zlt i (Z_of_nat wordsize) then i else Z_of_nat wordsize - 1)). + destruct (Z_of_bits_shift_right_neg y' f) as [k [EQ RANGE]]. + generalize (unsigned_range y). unfold y'; omega. + intros. unfold f. rewrite zlt_false; auto. + set (A := Z_of_bits wordsize f y') in *. + set (B := Z_of_bits wordsize f 0) in *. + assert (B = Z_of_bits wordsize (bits_of_Z wordsize x') 0). + unfold B. apply Z_of_bits_exten; intros. + unfold f. rewrite zlt_true. auto. omega. + assert (B = x'). + apply eqm_small_eq. rewrite H. apply Z_of_bits_of_Z. + unfold B; apply Z_of_bits_range. + unfold x'; apply unsigned_range. + assert (Q: (x' - modulus) / two_p y' = A - modulus). + apply Zdiv_unique with k; auto. rewrite <- H0. rewrite EQ. ring. + rewrite Q. apply eqm_samerepr. exists 1; ring. Qed. Theorem divs_pow2: @@ -2107,6 +2208,61 @@ Proof. rewrite <- H0. rewrite repr_unsigned. auto. Qed. +(** Unsigned modulus over [2^n] is masking with [2^n-1]. *) + +Lemma Z_of_bits_mod_mask: + forall f n, + 0 <= n <= Z_of_nat wordsize -> + Z_of_bits wordsize (fun i => if zlt i n then f i else false) 0 = + (Z_of_bits wordsize f 0) mod (two_p n). +Proof. + intros. set (f' := fun i => if zlt i n then f i else false). + set (n1 := nat_of_Z n). set (m1 := nat_of_Z (Z_of_nat wordsize - n)). + assert (Z_of_nat n1 = n). apply nat_of_Z_eq; omega. + assert (Z_of_nat m1 = Z_of_nat wordsize - n). apply nat_of_Z_eq; omega. + assert (n1 + m1 = wordsize)%nat. apply inj_eq_rev. rewrite inj_plus. omega. + generalize (Z_of_bits_compose f n1 m1 0). + rewrite H2. rewrite Zplus_0_l. rewrite two_power_nat_two_p. rewrite H0. intros. + generalize (Z_of_bits_compose f' n1 m1 0). + rewrite H2. rewrite Zplus_0_l. rewrite two_power_nat_two_p. rewrite H0. intros. + assert (Z_of_bits n1 f' 0 = Z_of_bits n1 f 0). + apply Z_of_bits_exten; intros. unfold f'. apply zlt_true. omega. + assert (Z_of_bits m1 f' n = 0). + apply Z_of_bits_false; intros. unfold f'. apply zlt_false. omega. + assert (Z_of_bits wordsize f' 0 = Z_of_bits n1 f 0). + rewrite H4. rewrite H5. rewrite H6. ring. + symmetry. apply Zmod_unique with (Z_of_bits m1 f n). omega. + rewrite H7. rewrite <- H0. rewrite <- two_power_nat_two_p. apply Z_of_bits_range. +Qed. + +Theorem modu_and: + forall x n logn, + is_power2 n = Some logn -> + modu x n = and x (sub n one). +Proof. + intros. generalize (is_power2_correct _ _ H); intro. + generalize (is_power2_rng _ _ H); intro. + unfold modu, and, bitwise_binop. decEq. + set (ux := unsigned x). + replace ux with (Z_of_bits wordsize (bits_of_Z wordsize ux) 0). + rewrite H0. rewrite <- Z_of_bits_mod_mask. + apply Z_of_bits_exten; intros. rewrite Zplus_0_r. + 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 i (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 [shrx] (signed division by a power of 2) *) + Theorem shrx_carry: forall x y, add (shr x y) (shr_carry x y) = shrx x y. @@ -2142,14 +2298,13 @@ Theorem shrx_shr: shrx 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. rewrite unsigned_repr. - set (uy := unsigned y). - intro RANGE. + intros. rewrite shr_div_two_p. unfold shrx. unfold divs. + exploit ltu_inv; eauto. rewrite unsigned_repr. + 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. + apply is_power2_two_p. omega. apply repr_unsigned. rewrite mul_commut. apply mul_one. assert (two_p uy > 0). apply two_p_gt_ZERO. omega. assert (two_p uy < half_modulus). @@ -2161,7 +2316,7 @@ Proof. rewrite H0. apply unsigned_repr. unfold max_unsigned. omega. assert (signed (shl one y) = two_p uy). rewrite H0. apply signed_repr. - unfold max_signed. generalize min_signed_neg. omega. + unfold max_signed. generalize min_signed_neg. omega. rewrite H5. rewrite Zdiv_round_Zdiv; auto. unfold lt. rewrite signed_zero. @@ -2171,124 +2326,13 @@ Proof. 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. + rewrite H6. rewrite signed_repr. decEq. 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: - forall x y z, - and y z = zero -> - add (and x y) (and x z) = and x (or y z). -Proof. - intros. unfold add, and, bitwise_binop. - decEq. - repeat rewrite unsigned_repr; auto with ints. - 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 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). - rewrite H. change (unsigned zero) with 0. - rewrite bits_of_Z_zero. apply andb_b_false. - unfold and, bitwise_binop. - rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits. - reflexivity. auto. - rewrite <- demorgan1. - unfold or, bitwise_binop. - rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits; auto. -Qed. - -Lemma Z_of_bits_zero: - forall n f, - (forall i, i >= 0 -> f i = false) -> - Z_of_bits n f = 0. -Proof. - induction n; intros; simpl. - auto. - rewrite H. rewrite IHn. auto. intros. apply H. omega. omega. -Qed. - -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. - 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. - 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: - forall x n logn, - is_power2 n = Some logn -> - modu x n = and x (sub n one). -Proof. - intros. generalize (is_power2_correct _ _ H); intro. - generalize (is_power2_rng _ _ H); intro. - 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. *) Section EXTENSIONS. @@ -2319,26 +2363,7 @@ Proof. apply unsigned_repr. apply two_p_n_range. Qed. -Theorem zero_ext_and: - forall x, zero_ext n x = and x (repr (two_p n - 1)). -Proof. - 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. - rewrite unsigned_one. reflexivity. -Qed. - -Theorem zero_ext_idem: - forall x, zero_ext n (zero_ext n x) = zero_ext n x. -Proof. - intros. repeat rewrite zero_ext_and. - rewrite and_assoc. rewrite and_idem. auto. -Qed. - -Lemma eqm_eqmod_two_p: +Remark eqm_eqmod_two_p: forall a b, eqm a b -> eqmod (two_p n) a b. Proof. intros a b [k EQ]. @@ -2348,139 +2373,65 @@ Proof. decEq. omega. omega. omega. Qed. -Lemma zero_ext_range: - forall x, - 0 <= unsigned (zero_ext n x) < two_p n. -Proof. - intros. unfold zero_ext. - exploit (Z_mod_lt (unsigned x) (two_p n)). apply two_p_gt_ZERO; omega. intro EQ. - rewrite unsigned_repr. auto. - unfold max_unsigned. - assert (two_p n <= modulus). - rewrite modulus_power. apply two_p_monotone. omega. - omega. -Qed. - -Lemma zero_ext_charact: - forall x y, - 0 <= unsigned y < two_p n -> - eqmod (two_p n) (unsigned x) (unsigned y) -> - zero_ext n x = y. -Proof. - intros. unfold zero_ext. - destruct H0 as [k EQ]. exploit Zmod_unique; eauto. - intro. rewrite H0. apply repr_unsigned. -Qed. - -Lemma sign_ext_range: - forall x, - -(two_p (n-1)) <= signed (sign_ext n x) < two_p (n-1). -Proof. - intros. unfold sign_ext. set (m := unsigned x mod two_p n). - exploit (Z_mod_lt (unsigned x) (two_p n)). apply two_p_gt_ZERO; omega. fold m. intro A. - assert (B: two_p (n - 1) <= modulus). - rewrite modulus_power. apply two_p_monotone; omega. - assert (C: two_p (n - 1) <= half_modulus). - rewrite half_modulus_power. apply two_p_monotone; omega. - assert (D: two_p n <= modulus). - rewrite modulus_power. apply two_p_monotone; omega. - destruct (zlt m (two_p (n-1))). - unfold signed. rewrite zlt_true. rewrite unsigned_repr. omega. - unfold max_unsigned; omega. - rewrite unsigned_repr. omega. unfold max_unsigned; omega. - unfold signed. - set (m' := m - two_p n). - assert (unsigned (repr m') = m' + modulus). - apply eqm_small_eq. apply eqm_unsigned_repr_l. exists (-1). omega. - apply unsigned_range. unfold m'. omega. - assert (two_p (n-1) > 0). apply two_p_gt_ZERO; omega. - assert (two_p n = 2 * two_p (n-1)). - rewrite <- two_p_S. decEq. omega. omega. - assert (-two_p (n-1) <= m' <= 0). unfold m'. omega. - rewrite H. rewrite zlt_false. omega. - unfold m'. rewrite half_modulus_modulus. 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. - -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 zero_ext. decEq. apply eqmod_mod_eq. apply two_p_n_pos. auto. -Qed. - -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. +Theorem zero_ext_and: + forall x, zero_ext n x = and x (repr (two_p n - 1)). Proof. - 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. + intros; unfold zero_ext, and, bitwise_binop. + decEq; apply Z_of_bits_exten; intros. + rewrite unsigned_repr. rewrite bits_of_Z_two_p. + unfold proj_sumbool. destruct (zlt (i+0) n). + rewrite andb_true_r; auto. rewrite andb_false_r; auto. + omega. omega. + generalize two_p_n_range two_p_n_pos; omega. Qed. -Lemma eqmod_two_p_zero_ext: - forall x, eqmod (two_p n) (unsigned x) (unsigned (zero_ext n x)). +Theorem zero_ext_mod: + forall x, unsigned (zero_ext n x) = Zmod (unsigned x) (two_p n). 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. + intros. + replace (unsigned x) with (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)) 0). + unfold zero_ext. rewrite unsigned_repr; auto with ints. + apply Z_of_bits_mod_mask. omega. + apply eqm_small_eq; auto with ints. apply Z_of_bits_of_Z. Qed. -Lemma eqmod_two_p_sign_ext: - forall x, eqmod (two_p n) (unsigned x) (unsigned (sign_ext n x)). +Theorem zero_ext_idem: + forall x, zero_ext n (zero_ext n x) = zero_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. + intros. repeat rewrite zero_ext_and. + rewrite and_assoc. rewrite and_idem. auto. 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. + intros. unfold sign_ext. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. rewrite Zplus_0_r. + repeat rewrite bits_of_Z_of_bits; auto. + destruct (zlt i n). auto. destruct (zlt (n - 1) n); auto. + omega. 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. + intros. unfold sign_ext, zero_ext. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. rewrite Zplus_0_r. + destruct (zlt i n); rewrite bits_of_Z_of_bits; auto. + rewrite zlt_true; auto. rewrite zlt_true; auto. omega. omega. 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. + intros. unfold sign_ext, zero_ext. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros. rewrite Zplus_0_r. + destruct (zlt i n); auto. + rewrite bits_of_Z_of_bits; auto. + rewrite zlt_true; auto. Qed. Theorem sign_ext_equal_if_zero_equal: @@ -2492,21 +2443,18 @@ Proof. 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). +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. 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. + intros. + assert (unsigned y = Z_of_nat wordsize - n). + 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. rewrite unsigned_repr_wordsize. omega. omega. Qed. Theorem sign_ext_shr_shl: @@ -2517,52 +2465,90 @@ Proof. intros. assert (unsigned y = Z_of_nat wordsize - n). unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. 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. + unfold sign_ext, shr, shl. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros; rewrite Zplus_0_r. + destruct (zlt i n). rewrite zlt_true. rewrite bits_of_Z_of_bits_gen. + decEq. omega. omega. omega. + rewrite zlt_false. rewrite bits_of_Z_of_bits_gen. + decEq. omega. omega. omega. +Qed. + +(** [zero_ext n x] is the unique integer congruent to [x] modulo [2^n] + in the range [0...2^n-1]. *) + +Lemma zero_ext_range: + forall x, 0 <= unsigned (zero_ext n x) < two_p n. +Proof. + intros. rewrite zero_ext_mod. apply Z_mod_lt. apply two_p_gt_ZERO. omega. +Qed. + +Lemma eqmod_zero_ext: + forall x, eqmod (two_p n) (unsigned (zero_ext n x)) (unsigned x). +Proof. + intros. rewrite zero_ext_mod. apply eqmod_sym. apply eqmod_mod. 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. - 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. - 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. - 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. +(** [sign_ext n x] is the unique integer congruent to [x] modulo [2^n] + in the range [-2^(n-1)...2^(n-1) - 1]. *) + +Lemma sign_ext_div: + forall x, + signed (sign_ext n x) = + signed (repr (unsigned x * two_p (Z_of_nat wordsize - n))) / two_p (Z_of_nat wordsize - n). +Proof. + intros. + assert (two_p (Z_of_nat wordsize - n) > 0). apply two_p_gt_ZERO. omega. + rewrite sign_ext_shr_shl. rewrite shr_div_two_p. rewrite shl_mul_two_p. + unfold mul. repeat rewrite unsigned_repr. rewrite signed_repr. auto. + apply Zdiv_interval_2. apply signed_range. + generalize min_signed_neg; omega. apply max_signed_pos. + auto. + generalize wordsize_max_unsigned; omega. + assert (two_p (Z_of_nat wordsize - n) < modulus). + rewrite modulus_power. apply two_p_monotone_strict. omega. + unfold max_unsigned. omega. + generalize wordsize_max_unsigned; omega. +Qed. + +Lemma sign_ext_range: + forall x, -two_p (n-1) <= signed (sign_ext n x) < two_p (n-1). Proof. intros. - assert (unsigned y = Z_of_nat wordsize - n). - 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. rewrite unsigned_repr_wordsize. omega. omega. + assert (two_p (n - 1) > 0). apply two_p_gt_ZERO. omega. + rewrite sign_ext_div. apply Zdiv_interval_1. omega. auto. apply two_p_gt_ZERO; omega. + rewrite <- Zopp_mult_distr_l. rewrite <- two_p_is_exp. + replace (n - 1 + (Z_of_nat wordsize - n)) with (Z_of_nat wordsize - 1) by omega. + rewrite <- half_modulus_power. + generalize (signed_range (repr (unsigned x * two_p (Z_of_nat wordsize - n)))). + unfold min_signed, max_signed. omega. + omega. omega. +Qed. + +Lemma eqmod_sign_ext: + forall x, eqmod (two_p n) (signed (sign_ext n x)) (unsigned x). +Proof. + intros. rewrite sign_ext_div. + assert (eqm (signed (repr (unsigned x * two_p (Z_of_nat wordsize - n)))) + (unsigned x * two_p (Z_of_nat wordsize - n))). + eapply eqm_trans. apply eqm_signed_unsigned. apply eqm_sym. apply eqm_unsigned_repr. + destruct H as [k EQ]. exists k. + rewrite EQ. rewrite Z_div_plus. decEq. + replace modulus with (two_p (n + (Z_of_nat wordsize - n))). + rewrite two_p_is_exp. rewrite Zmult_assoc. apply Z_div_mult. + apply two_p_gt_ZERO; omega. + omega. omega. + rewrite modulus_power. decEq. omega. + apply two_p_gt_ZERO; omega. +Qed. + +Lemma eqmod_sign_ext': + forall x, eqmod (two_p n) (unsigned (sign_ext n x)) (unsigned x). +Proof. + intros. eapply eqmod_trans. + apply eqm_eqmod_two_p. auto. apply eqm_sym. apply eqm_signed_unsigned. + apply eqmod_sign_ext. Qed. End EXTENSIONS. @@ -2572,10 +2558,13 @@ Theorem zero_ext_widen: 0 < n < Z_of_nat wordsize -> n <= n' < Z_of_nat wordsize -> zero_ext n' (zero_ext n x) = zero_ext n x. Proof. - intros. apply zero_ext_charact. - assert (two_p n <= two_p n'). apply two_p_monotone. omega. - generalize (zero_ext_range n H x). omega. - apply eqmod_refl. + intros. unfold zero_ext. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros; rewrite Zplus_0_r. + destruct (zlt i n). rewrite zlt_true. rewrite bits_of_Z_of_bits. apply zlt_true. + auto. omega. omega. + destruct (zlt i n'); auto. rewrite bits_of_Z_of_bits. apply zlt_false. + auto. omega. Qed. Theorem sign_ext_widen: @@ -2583,14 +2572,16 @@ Theorem sign_ext_widen: 0 < n < Z_of_nat wordsize -> n <= n' < Z_of_nat wordsize -> sign_ext n' (sign_ext n x) = sign_ext n x. Proof. - intros. apply sign_ext_charact. omega. - generalize (sign_ext_range n H x). - assert (two_p (n-1) <= two_p (n'-1)). apply two_p_monotone. omega. - omega. - apply eqmod_divides with modulus. fold eqm. - apply eqm_sym. apply eqm_signed_unsigned. - rewrite modulus_power. exists (two_p (Z_of_nat wordsize - n')). - rewrite <- two_p_is_exp. decEq. omega. omega. omega. + intros. unfold sign_ext. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros; rewrite Zplus_0_r. + destruct (zlt i n). rewrite zlt_true. rewrite bits_of_Z_of_bits. apply zlt_true. + auto. omega. omega. + destruct (zlt i n'). rewrite bits_of_Z_of_bits. apply zlt_false. + auto. omega. + rewrite bits_of_Z_of_bits. + destruct (zlt (n' - 1) n). assert (n' = n) by omega. congruence. auto. + omega. Qed. Theorem sign_zero_ext_widen: @@ -2598,20 +2589,14 @@ Theorem sign_zero_ext_widen: 0 < n < Z_of_nat wordsize -> n < n' < Z_of_nat wordsize -> sign_ext n' (zero_ext n x) = zero_ext n x. Proof. - intros. apply sign_ext_charact. omega. - generalize (zero_ext_range n H x). intro. - assert (two_p n <= two_p (n' - 1)). apply two_p_monotone. omega. - assert (two_p (n' - 1) > 0). apply two_p_gt_ZERO. omega. - replace (signed (zero_ext n x)) with (unsigned (zero_ext n x)). - omega. - symmetry. unfold signed. apply zlt_true. - assert (two_p n <= half_modulus). - rewrite half_modulus_power. apply two_p_monotone. omega. - omega. - apply eqmod_divides with modulus. fold eqm. - apply eqm_sym. apply eqm_signed_unsigned. - rewrite modulus_power. exists (two_p (Z_of_nat wordsize - n')). - rewrite <- two_p_is_exp. decEq. omega. omega. omega. + intros. unfold sign_ext, zero_ext. + repeat rewrite unsigned_repr; auto with ints. + decEq; apply Z_of_bits_exten; intros; rewrite Zplus_0_r. + destruct (zlt i n). rewrite zlt_true. rewrite bits_of_Z_of_bits. apply zlt_true. + auto. omega. omega. + destruct (zlt i n'). rewrite bits_of_Z_of_bits. apply zlt_false. + auto. omega. + rewrite bits_of_Z_of_bits. apply zlt_false. omega. omega. Qed. (** ** Properties of [one_bits] (decomposition in sum of powers of two) *) @@ -2726,7 +2711,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. apply one_not_zero. + rewrite eq_true. apply one_not_zero. Qed. Theorem notbool_istrue_isfalse: @@ -2795,7 +2780,7 @@ Module Wordsize_8. Proof. unfold wordsize; congruence. Qed. End Wordsize_8. -Module Byte := Integers.Make(Wordsize_8). +Module Byte := Make(Wordsize_8). Notation byte := Byte.int. -- cgit v1.2.3