From 6f3225b0623b9c97eed7d40ddc320b08c79c6518 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 10 Feb 2013 10:08:27 +0000 Subject: lib/Integers.v: revised and extended, faster implementation based on bit-level operations provided by ZArith in Coq 8.4. Other modules: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Coqlib.v | 86 +- lib/Floats.v | 62 +- lib/Integers.v | 2878 +++++++++++++++++++++++++++++++------------------------- lib/Ordered.v | 10 +- 4 files changed, 1655 insertions(+), 1381 deletions(-) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 676aa0a..8aeadb9 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -90,13 +90,8 @@ Ltac exploit x := (** * Definitions and theorems over the type [positive] *) -Definition peq (x y: positive): {x = y} + {x <> y}. -Proof. - intros. caseEq (Pcompare x y Eq). - intro. left. apply Pcompare_Eq_eq; auto. - intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. - intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. -Qed. +Definition peq: forall (x y: positive), {x = y} + {x <> y} := Pos.eq_dec. +Global Opaque peq. Lemma peq_true: forall (A: Type) (x: positive) (a b: A), (if peq x x then a else b) = a. @@ -114,32 +109,23 @@ Proof. auto. Qed. -Definition Plt (x y: positive): Prop := Zlt (Zpos x) (Zpos y). +Definition Plt: positive -> positive -> Prop := Pos.lt. Lemma Plt_ne: forall (x y: positive), Plt x y -> x <> y. Proof. - unfold Plt; intros. red; intro. subst y. omega. + unfold Plt; intros. red; intro. subst y. eelim Pos.lt_irrefl; eauto. Qed. Hint Resolve Plt_ne: coqlib. Lemma Plt_trans: forall (x y z: positive), Plt x y -> Plt y z -> Plt x z. -Proof. - unfold Plt; intros; omega. -Qed. - -Remark Psucc_Zsucc: - forall (x: positive), Zpos (Psucc x) = Zsucc (Zpos x). -Proof. - intros. rewrite Pplus_one_succ_r. - reflexivity. -Qed. +Proof (Pos.lt_trans). Lemma Plt_succ: forall (x: positive), Plt x (Psucc x). Proof. - intro. unfold Plt. rewrite Psucc_Zsucc. omega. + unfold Plt; intros. apply Pos.lt_succ_r. apply Pos.le_refl. Qed. Hint Resolve Plt_succ: coqlib. @@ -153,32 +139,29 @@ Hint Resolve Plt_succ: coqlib. Lemma Plt_succ_inv: forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y. Proof. - intros x y. unfold Plt. rewrite Psucc_Zsucc. - intro. assert (A: (Zpos x < Zpos y)%Z \/ Zpos x = Zpos y). omega. - elim A; intro. left; auto. right; injection H0; auto. + unfold Plt; intros. rewrite Pos.lt_succ_r in H. + apply Pos.le_lteq; auto. Qed. Definition plt (x y: positive) : {Plt x y} + {~ Plt x y}. Proof. - intros. unfold Plt. apply Z_lt_dec. -Qed. + unfold Plt, Pos.lt; intros. destruct (Pos.compare x y). + - right; congruence. + - left; auto. + - right; congruence. +Defined. +Global Opaque plt. -Definition Ple (p q: positive) := Zle (Zpos p) (Zpos q). +Definition Ple: positive -> positive -> Prop := Pos.le. Lemma Ple_refl: forall (p: positive), Ple p p. -Proof. - unfold Ple; intros; omega. -Qed. +Proof (Pos.le_refl). Lemma Ple_trans: forall (p q r: positive), Ple p q -> Ple q r -> Ple p r. -Proof. - unfold Ple; intros; omega. -Qed. +Proof (Pos.le_trans). Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q. -Proof. - unfold Plt, Ple; intros; omega. -Qed. +Proof (Pos.lt_le_incl). Lemma Ple_succ: forall (p: positive), Ple p (Psucc p). Proof. @@ -187,14 +170,10 @@ Qed. Lemma Plt_Ple_trans: forall (p q r: positive), Plt p q -> Ple q r -> Plt p r. -Proof. - unfold Plt, Ple; intros; omega. -Qed. +Proof (Pos.lt_le_trans). Lemma Plt_strict: forall p, ~ Plt p p. -Proof. - unfold Plt; intros. omega. -Qed. +Proof (Pos.lt_irrefl). Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. @@ -271,7 +250,7 @@ End POSITIVE_ITERATION. (** * Definitions and theorems over the type [Z] *) -Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z_eq_dec. +Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z.eq_dec. Lemma zeq_true: forall (A: Type) (x: Z) (a b: A), (if zeq x x then a else b) = a. @@ -291,7 +270,7 @@ Qed. Open Scope Z_scope. -Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec. +Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_dec. Lemma zlt_true: forall (A: Type) (x y: Z) (a b: A), @@ -581,31 +560,26 @@ Qed. (** Conversion from [Z] to [nat]. *) -Definition nat_of_Z (z: Z) : nat := - match z with - | Z0 => O - | Zpos p => nat_of_P p - | Zneg p => O - end. +Definition nat_of_Z: Z -> nat := Z.to_nat. Lemma nat_of_Z_of_nat: forall n, nat_of_Z (Z_of_nat n) = n. Proof. - intros. unfold Z_of_nat. destruct n. auto. - simpl. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. auto. + exact Nat2Z.id. Qed. Lemma nat_of_Z_max: forall z, Z_of_nat (nat_of_Z z) = Zmax z 0. Proof. - intros. unfold Zmax. destruct z; simpl; auto. - symmetry. apply Zpos_eq_Z_of_nat_o_nat_of_P. + intros. unfold Zmax. destruct z; simpl; auto. + change (Z.of_nat (Z.to_nat (Zpos p)) = Zpos p). + apply Z2Nat.id. compute; intuition congruence. Qed. Lemma nat_of_Z_eq: forall z, z >= 0 -> Z_of_nat (nat_of_Z z) = z. Proof. - intros. rewrite nat_of_Z_max. apply Zmax_left. auto. + unfold nat_of_Z; intros. apply Z2Nat.id. omega. Qed. Lemma nat_of_Z_neg: @@ -619,9 +593,7 @@ Lemma nat_of_Z_plus: p >= 0 -> q >= 0 -> nat_of_Z (p + q) = (nat_of_Z p + nat_of_Z q)%nat. Proof. - intros. - apply inj_eq_rev. rewrite inj_plus. - repeat rewrite nat_of_Z_eq; auto. omega. + unfold nat_of_Z; intros. apply Z2Nat.inj_add; omega. Qed. diff --git a/lib/Floats.v b/lib/Floats.v index 711fd61..2c23d45 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -230,7 +230,7 @@ Proof. intros. unfold from_words. decEq. rewrite Int64.shifted_or_is_add. apply Int64.eqm_samerepr. auto with ints. - change (Z_of_nat Int64.wordsize) with 64. omega. + change Int64.zwordsize with 64. omega. generalize (Int.unsigned_range lo). intros [A B]. rewrite Int64.unsigned_repr. assumption. assert (Int.modulus < Int64.max_unsigned). compute; auto. omega. @@ -753,38 +753,34 @@ Lemma split_bits_or: (Int64.shl (Int64.repr (Int.unsigned ox4330_0000)) (Int64.repr 32)) (Int64.repr (Int.unsigned x)))) = (false, Int.unsigned x, 1075). Proof. -intro; pose proof (Int.unsigned_range x); unfold split_bits; f_equal; f_equal. -apply Zle_bool_false. -match goal with [|-_ ?x < _] => - pose proof (Int64.sign_bit_of_Z x); - destruct (zlt (Int64.unsigned x) Int64.half_modulus) -end. -assumption. -unfold Int64.or, Int64.bitwise_binop in H0. -rewrite Int64.unsigned_repr, Int64.bits_of_Z_of_bits in H0. -rewrite orb_false_intro in H0; [discriminate|reflexivity|]. -rewrite Int64.sign_bit_of_Z. -match goal with [|- ((if ?c then _ else _) = _)] => destruct c as [z0|z0] end. -reflexivity. -rewrite Int64.unsigned_repr in z0; [exfalso|]; now smart_omega. -vm_compute; split; congruence. -now apply Int64.Z_of_bits_range_2. -change (2^52) with (two_p 52). -rewrite <- Int64.zero_ext_mod, Int64.zero_ext_and by (vm_compute; intuition). -rewrite Int64.and_commut, Int64.and_or_distrib. -match goal with [|- _ (_ ?o _) = _] => change o with Int64.zero end. -rewrite Int64.or_commut, Int64.or_zero, Int64.and_commut. -rewrite <- Int64.zero_ext_and, Int64.zero_ext_mod by (compute; intuition). -rewrite Int64.unsigned_repr; [apply Zmod_small; compute_this (two_p 52)|]; now smart_omega. -match goal with [|- ?x mod _ = _] => rewrite <- (Int64.unsigned_repr x) end. -change (2^52) with (two_p (Int64.unsigned (Int64.repr 52))). rewrite <- Int64.shru_div_two_p. -change (2^11) with (two_p 11). rewrite <- Int64.or_shru. -replace (Int64.shru (Int64.repr (Int.unsigned x)) (Int64.repr 52)) with Int64.zero; - [vm_compute; reflexivity|]. -rewrite Int64.shru_div_two_p, Int64.unsigned_repr by smart_omega. -unfold Int64.zero; f_equal; rewrite Zdiv_small; [reflexivity|]. -simpl; compute_this (two_power_pos 52); now smart_omega. -apply Zdiv_interval_2; try smart_omega; now apply Int64.unsigned_range_2. + intros. + transitivity (split_bits 52 11 (join_bits 52 11 false (Int.unsigned x) 1075)). + - f_equal. + assert (Int64.unsigned (Int64.repr (Int.unsigned x)) = Int.unsigned x). + apply Int64.unsigned_repr. + generalize (Int.unsigned_range x). + compute_this (Int.modulus). + compute_this (Int64.max_unsigned). + omega. + rewrite Int64.shifted_or_is_add. + unfold join_bits. + rewrite H. + apply Int64.unsigned_repr. + generalize (Int.unsigned_range x). + compute_this ((0 + 1075) * 2 ^ 52). + compute_this (Int.modulus). + compute_this (Int64.max_unsigned). + omega. + compute_this Int64.zwordsize. omega. + rewrite H. + generalize (Int.unsigned_range x). + change (two_p 32) with Int.modulus. + omega. + - apply split_join_bits. + compute; auto. + generalize (Int.unsigned_range x). + compute_this Int.modulus; compute_this (2^52); omega. + compute_this (2^11); omega. Qed. Lemma from_words_value: diff --git a/lib/Integers.v b/lib/Integers.v index a76049b..3609fda 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -15,7 +15,9 @@ (** Formalizations of machine integers modulo $2^N$ #2N#. *) -Require Import Axioms. +Require Import Eqdep_dec. +Require Import Zwf. +Require Recdef. Require Import Coqlib. (** * Comparisons *) @@ -58,26 +60,24 @@ End WORDSIZE. Module Make(WS: WORDSIZE). Definition wordsize: nat := WS.wordsize. +Definition zwordsize: Z := Z_of_nat wordsize. Definition modulus : Z := two_power_nat wordsize. Definition half_modulus : Z := modulus / 2. Definition max_unsigned : Z := modulus - 1. Definition max_signed : Z := half_modulus - 1. Definition min_signed : Z := - half_modulus. -Remark wordsize_pos: - Z_of_nat wordsize > 0. +Remark wordsize_pos: zwordsize > 0. Proof. - unfold wordsize. generalize WS.wordsize_not_zero. omega. + unfold zwordsize, wordsize. generalize WS.wordsize_not_zero. omega. Qed. -Remark modulus_power: - modulus = two_p (Z_of_nat wordsize). +Remark modulus_power: modulus = two_p zwordsize. Proof. unfold modulus. apply two_power_nat_two_p. Qed. -Remark modulus_pos: - modulus > 0. +Remark modulus_pos: modulus > 0. Proof. rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega. Qed. @@ -86,106 +86,99 @@ Qed. (** A machine integer (type [int]) is represented as a Coq arbitrary-precision integer (type [Z]) plus a proof that it is in the range 0 (included) to - [modulus] (excluded. *) + [modulus] (excluded). *) -Record int: Type := mkint { intval: Z; intrange: 0 <= intval < modulus }. +Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }. -(** Binary decomposition of integers (type [Z]) *) +(** Fast normalization modulo [2^wordsize] *) -Definition Z_bin_decomp (x: Z) : bool * Z := - match x with - | Z0 => (false, 0) - | Zpos p => - match p with - | xI q => (true, Zpos q) - | xO q => (false, Zpos q) - | xH => (true, 0) - end - | Zneg p => +Fixpoint P_mod_two_p (p: positive) (n: nat) {struct n} : Z := + match n with + | O => 0 + | S m => match p with - | xI q => (true, Zneg q - 1) - | xO q => (false, Zneg q) - | xH => (true, -1) + | xH => 1 + | xO q => Z.double (P_mod_two_p q m) + | xI q => Z.succ_double (P_mod_two_p q m) end end. -Definition Z_bin_comp (b: bool) (x: Z) : Z := - if b then Zdouble_plus_one x else Zdouble x. - -Lemma Z_bin_comp_eq: - forall b x, Z_bin_comp b x = 2 * x + (if b then 1 else 0). -Proof. - unfold Z_bin_comp; intros. destruct b. - apply Zdouble_plus_one_mult. - rewrite Zdouble_mult. omega. -Qed. - -Lemma Z_bin_comp_decomp: - forall x, Z_bin_comp (fst (Z_bin_decomp x)) (snd (Z_bin_decomp x)) = x. -Proof. - destruct x; simpl. - auto. - destruct p; auto. - destruct p; auto. simpl. - rewrite <- Pplus_one_succ_r. rewrite Pdouble_minus_one_o_succ_eq_xI. auto. -Qed. +Definition Z_mod_modulus (x: Z) : Z := + match x with + | Z0 => 0 + | Zpos p => P_mod_two_p p wordsize + | Zneg p => let r := P_mod_two_p p wordsize in if zeq r 0 then 0 else modulus - r + end. -Lemma Z_bin_comp_decomp2: - forall x b y, Z_bin_decomp x = (b, y) -> x = Z_bin_comp b y. +Lemma P_mod_two_p_range: + forall n p, 0 <= P_mod_two_p p n < two_power_nat n. Proof. - intros. rewrite <- (Z_bin_comp_decomp x). rewrite H; auto. + induction n; simpl; intros. + - rewrite two_power_nat_O. omega. + - rewrite two_power_nat_S. destruct p. + + generalize (IHn p). rewrite Z.succ_double_spec. omega. + + generalize (IHn p). rewrite Z.double_spec. omega. + + generalize (two_power_nat_pos n). omega. Qed. -Lemma Z_bin_decomp_comp: - forall b x, Z_bin_decomp (Z_bin_comp b x) = (b, x). +Lemma P_mod_two_p_eq: + forall n p, P_mod_two_p p n = (Zpos p) mod (two_power_nat n). Proof. - intros. 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. + assert (forall n p, exists y, Zpos p = y * two_power_nat n + P_mod_two_p p n). + { + induction n; simpl; intros. + - rewrite two_power_nat_O. exists (Zpos p). ring. + - rewrite two_power_nat_S. destruct p. + + destruct (IHn p) as [y EQ]. exists y. + change (Zpos p~1) with (2 * Zpos p + 1). rewrite EQ. + rewrite Z.succ_double_spec. ring. + + destruct (IHn p) as [y EQ]. exists y. + change (Zpos p~0) with (2 * Zpos p). rewrite EQ. + rewrite (Z.double_spec (P_mod_two_p p n)). ring. + + exists 0; omega. + } + intros. + destruct (H n p) as [y EQ]. + symmetry. apply Zmod_unique with y. auto. apply P_mod_two_p_range. Qed. -Lemma Z_bin_comp_inj: - forall b1 b2 x1 x2, Z_bin_comp b1 x1 = Z_bin_comp b2 x2 -> (b1, x1) = (b2, x2). +Lemma Z_mod_modulus_range: + forall x, 0 <= Z_mod_modulus x < modulus. Proof. - intros. repeat rewrite Z_bin_comp_eq in H. - destruct b1; destruct b2. - f_equal. omega. - omegaContradiction. - omegaContradiction. - f_equal. omega. + intros; unfold Z_mod_modulus. + destruct x. + - generalize modulus_pos; omega. + - apply P_mod_two_p_range. + - set (r := P_mod_two_p p wordsize). + assert (0 <= r < modulus) by apply P_mod_two_p_range. + destruct (zeq r 0). + + generalize modulus_pos; omega. + + omega. Qed. -(** Fast normalization modulo [2^n]. *) - -Fixpoint Z_mod_two_p (x: Z) (n: nat) {struct n} : Z := - match n with - | O => 0 - | S m => let (b, y) := Z_bin_decomp x in Z_bin_comp b (Z_mod_two_p y m) - end. - -Lemma Z_mod_two_p_range: - forall n x, 0 <= Z_mod_two_p x n < two_power_nat n. +Lemma Z_mod_modulus_range': + forall x, -1 < Z_mod_modulus x < modulus. Proof. - induction n; simpl; intros. - rewrite two_power_nat_O. omega. - rewrite two_power_nat_S. destruct (Z_bin_decomp x) as [b y] eqn:?. - rewrite Z_bin_comp_eq. generalize (IHn y). destruct b; omega. + intros. generalize (Z_mod_modulus_range x); omega. Qed. -Lemma Z_mod_two_p_eq: - forall n x, Z_mod_two_p x n = Zmod x (two_power_nat n). +Lemma Z_mod_modulus_eq: + forall x, Z_mod_modulus x = x mod modulus. Proof. - assert (forall n x, exists y, x = y * two_power_nat n + Z_mod_two_p x n). - induction n; simpl; intros. - rewrite two_power_nat_O. exists x. ring. - rewrite two_power_nat_S. - destruct (Z_bin_decomp x) as [b y] eqn:?. - destruct (IHn y) as [z EQ]. - exists z. rewrite (Z_bin_comp_decomp2 _ _ _ Heqp). - repeat rewrite Z_bin_comp_eq. rewrite EQ at 1. ring. - intros. - destruct (H n x) as [y EQ]. - symmetry. apply Zmod_unique with y. auto. apply Z_mod_two_p_range. + intros. unfold Z_mod_modulus. destruct x. + - rewrite Zmod_0_l. auto. + - apply P_mod_two_p_eq. + - generalize (P_mod_two_p_range wordsize p) (P_mod_two_p_eq wordsize p). + fold modulus. intros A B. + exploit (Z_div_mod_eq (Zpos p) modulus). apply modulus_pos. intros C. + set (q := Zpos p / modulus) in *. + set (r := P_mod_two_p p wordsize) in *. + rewrite <- B in C. + change (Z.neg p) with (- (Z.pos p)). destruct (zeq r 0). + + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. ring. + generalize modulus_pos; omega. + + symmetry. apply Zmod_unique with (-q - 1). rewrite C. ring. + omega. Qed. (** The [unsigned] and [signed] functions return the Coq integer corresponding @@ -195,32 +188,39 @@ Qed. Definition unsigned (n: int) : Z := intval n. Definition signed (n: int) : Z := - if zlt (unsigned n) half_modulus - then unsigned n - else unsigned n - modulus. + let x := unsigned n in + if zlt x half_modulus then x else x - modulus. (** Conversely, [repr] takes a Coq integer and returns the corresponding machine integer. The argument is treated modulo [modulus]. *) Definition repr (x: Z) : int := - mkint (Z_mod_two_p x wordsize) (Z_mod_two_p_range wordsize x). + mkint (Z_mod_modulus x) (Z_mod_modulus_range' x). Definition zero := repr 0. Definition one := repr 1. Definition mone := repr (-1). -Definition iwordsize := repr (Z_of_nat wordsize). +Definition iwordsize := repr zwordsize. Lemma mkint_eq: forall x y Px Py, x = y -> mkint x Px = mkint y Py. Proof. - intros. subst y. - generalize (proof_irr Px Py); intro. - subst Py. reflexivity. + intros. subst y. + assert (forall (n m: Z) (P1 P2: n < m), P1 = P2). + { + unfold Zlt; intros. + apply eq_proofs_unicity. + intros c1 c2. destruct c1; destruct c2; (left; reflexivity) || (right; congruence). + } + destruct Px as [Px1 Px2]. destruct Py as [Py1 Py2]. + rewrite (H _ _ Px1 Py1). + rewrite (H _ _ Px2 Py2). + reflexivity. Qed. Lemma eq_dec: forall (x y: int), {x = y} + {x <> y}. Proof. - intros. destruct x; destruct y. case (zeq intval0 intval1); intro. + intros. destruct x; destruct y. destruct (zeq intval0 intval1). left. apply mkint_eq. auto. right. red; intro. injection H. exact n. Qed. @@ -243,93 +243,41 @@ 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) - else - if zlt y 0 then -(x / (-y)) else x / y. - -Definition Zmod_round (x y: Z) : Z := - x - (Zdiv_round x y) * y. - Definition divs (x y: int) : int := - repr (Zdiv_round (signed x) (signed y)). + repr (Z.quot (signed x) (signed y)). Definition mods (x y: int) : int := - repr (Zmod_round (signed x) (signed y)). + repr (Z.rem (signed x) (signed y)). Definition divu (x y: int) : int := repr (unsigned x / unsigned y). Definition modu (x y: int) : int := - repr (Zmod (unsigned x) (unsigned y)). + repr ((unsigned x) mod (unsigned y)). Definition add_carry (x y cin: int): int := if zlt (unsigned x + unsigned y + unsigned cin) modulus then zero else one. -(** For bitwise operations, we need to convert between Coq integers [Z] - 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. For [i] less than 0 or greater or equal to [wordsize], - the characteristic function is [false]. *) +(** Bitwise boolean operations. *) -Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool := - match n with - | O => - (fun i: Z => false) - | S m => - let (b, y) := Z_bin_decomp x in - let f := bits_of_Z m y in - (fun i: Z => if zeq i 0 then b else f (i - 1)) - end. - -Fixpoint Z_of_bits (n: nat) (f: Z -> bool) (i: Z) {struct n}: Z := - match n with - | O => 0 - | S m => Z_bin_comp (f i) (Z_of_bits m f (Zsucc i)) - end. - -(** 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)) 0). - -Definition and (x y: int): int := bitwise_binop andb x y. -Definition or (x y: int): int := bitwise_binop orb x y. -Definition xor (x y: int) : int := bitwise_binop xorb x y. +Definition and (x y: int): int := repr (Z.land (unsigned x) (unsigned y)). +Definition or (x y: int): int := repr (Z.lor (unsigned x) (unsigned y)). +Definition xor (x y: int) : int := repr (Z.lxor (unsigned x) (unsigned y)). Definition not (x: int) : int := xor x mone. (** Shifts and rotates. *) -Definition shl (x y: int): int := - let fx := bits_of_Z wordsize (unsigned x) in - repr (Z_of_bits wordsize fx (- unsigned y)). - -Definition shru (x y: int): int := - let fx := bits_of_Z wordsize (unsigned x) in - repr (Z_of_bits wordsize fx (unsigned y)). - -Definition shr (x y: int): int := - 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)). +Definition shl (x y: int): int := repr (Z.shiftl (unsigned x) (unsigned y)). +Definition shru (x y: int): int := repr (Z.shiftr (unsigned x) (unsigned y)). +Definition shr (x y: int): int := repr (Z.shiftr (signed x) (unsigned y)). Definition rol (x y: int) : int := - let fx := bits_of_Z wordsize (unsigned x) in - let rx := fun i => fx (Zmod i (Z_of_nat wordsize)) in - repr (Z_of_bits wordsize rx (-unsigned y)). - + let n := (unsigned y) mod zwordsize in + repr (Z.lor (Z.shiftl (unsigned x) n) (Z.shiftr (unsigned x) (zwordsize - n))). Definition ror (x y: int) : int := - let fx := bits_of_Z wordsize (unsigned x) in - let rx := fun i => fx (Zmod i (Z_of_nat wordsize)) in - repr (Z_of_bits wordsize rx (unsigned y)). + let n := (unsigned y) mod zwordsize in + repr (Z.lor (Z.shiftr (unsigned x) n) (Z.shiftl (unsigned x) (zwordsize - n))). Definition rolm (x a m: int): int := and (rol x a) m. @@ -346,13 +294,42 @@ Definition shr_carry (x y: int) := (** 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 Zshiftin (b: bool) (x: Z) : Z := + if b then Z.succ_double x else Z.double x. + +(** In pseudo-code: +<< + Fixpoint Zzero_ext (n: Z) (x: Z) : Z := + if zle n 0 then + 0 + else + Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)). + Fixpoint Zsign_ext (n: Z) (x: Z) : Z := + if zle n 1 then + if Z.odd x then -1 else 0 + else + Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)). +>> + We encode this [nat]-like recursion using the [Z.iter] iteration + function, in order to make the [Zzero_ext] and [Zsign_ext] + functions efficiently executable within Coq. +*) + +Definition Zzero_ext (n: Z) (x: Z) : Z := + Z.iter n + (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x))) + (fun x => 0) + x. + +Definition Zsign_ext (n: Z) (x: Z) : Z := + Z.iter (Z.pred n) + (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x))) + (fun x => if Z.odd x then -1 else 0) + x. -Definition 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). +Definition zero_ext (n: Z) (x: int) : int := repr (Zzero_ext n (unsigned x)). + +Definition sign_ext (n: Z) (x: int) : int := repr (Zsign_ext n (unsigned x)). (** Decomposition of a number as a sum of powers of two. *) @@ -360,8 +337,9 @@ Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z := match n with | O => nil | S m => - let (b, y) := Z_bin_decomp x in - if b then i :: Z_one_bits m y (i+1) else Z_one_bits m y (i+1) + if Z.odd x + then i :: Z_one_bits m (Z.div2 x) (i+1) + else Z_one_bits m (Z.div2 x) (i+1) end. Definition one_bits (x: int) : list int := @@ -406,11 +384,11 @@ Definition notbool (x: int) : int := if eq x zero then one else zero. (** ** Properties of [modulus], [max_unsigned], etc. *) Remark half_modulus_power: - half_modulus = two_p (Z_of_nat wordsize - 1). + half_modulus = two_p (zwordsize - 1). Proof. unfold half_modulus. rewrite modulus_power. - set (ws1 := Z_of_nat wordsize - 1). - replace (Z_of_nat wordsize) with (Zsucc ws1). + set (ws1 := zwordsize - 1). + replace (zwordsize) with (Zsucc ws1). rewrite two_p_S. rewrite Zmult_comm. apply Z_div_mult. omega. unfold ws1. generalize wordsize_pos; omega. unfold ws1. omega. @@ -449,17 +427,17 @@ Proof. unfold max_signed. generalize half_modulus_pos. omega. Qed. -Remark wordsize_max_unsigned: Z_of_nat wordsize <= max_unsigned. +Remark wordsize_max_unsigned: zwordsize <= max_unsigned. Proof. - assert (Z_of_nat wordsize < modulus). + assert (zwordsize < modulus). rewrite modulus_power. apply two_p_strict. generalize wordsize_pos. omega. unfold max_unsigned. omega. Qed. -Remark two_wordsize_max_unsigned: 2 * Z_of_nat wordsize - 1 <= max_unsigned. +Remark two_wordsize_max_unsigned: 2 * zwordsize - 1 <= max_unsigned. Proof. - assert (2 * Z_of_nat wordsize - 1 < modulus). + assert (2 * zwordsize - 1 < modulus). rewrite modulus_power. apply two_p_strict_2. generalize wordsize_pos; omega. unfold max_unsigned; omega. Qed. @@ -473,7 +451,7 @@ Qed. Lemma unsigned_repr_eq: forall x, unsigned (repr x) = Zmod x modulus. Proof. - intros. simpl. apply Z_mod_two_p_eq. + intros. simpl. apply Z_mod_modulus_eq. Qed. Lemma signed_repr_eq: @@ -629,7 +607,7 @@ Hint Resolve eqm_mult: ints. Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y. Proof. intros. unfold repr. apply mkint_eq. - repeat rewrite Z_mod_two_p_eq. apply eqmod_mod_eq. auto with ints. exact H. + rewrite !Z_mod_modulus_eq. apply eqmod_mod_eq. auto with ints. exact H. Qed. Lemma eqm_unsigned_repr: @@ -666,7 +644,7 @@ Qed. Theorem unsigned_range: forall i, 0 <= unsigned i < modulus. Proof. - destruct i; auto. + destruct i. simpl. omega. Qed. Hint Resolve unsigned_range: ints. @@ -693,7 +671,7 @@ Theorem repr_unsigned: forall i, repr (unsigned i) = i. Proof. destruct i; simpl. unfold repr. apply mkint_eq. - rewrite Z_mod_two_p_eq. apply Zmod_small; auto. + rewrite Z_mod_modulus_eq. apply Zmod_small; omega. Qed. Hint Resolve repr_unsigned: ints. @@ -767,7 +745,7 @@ Proof. 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. + generalize wordsize_pos. unfold zwordsize. omega. Qed. Theorem unsigned_mone: unsigned mone = modulus - 1. @@ -798,7 +776,7 @@ Proof. Qed. Theorem unsigned_repr_wordsize: - unsigned iwordsize = Z_of_nat wordsize. + unsigned iwordsize = zwordsize. Proof. unfold iwordsize; rewrite unsigned_repr_eq. apply Zmod_small. generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega. @@ -1079,7 +1057,36 @@ Proof. apply eqm_mult; apply eqm_sym; apply eqm_signed_unsigned. Qed. -(** ** Properties of division and modulus *) +(** ** Properties of division and Lemma Ztestbit_same_equal: + forall x y, + (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) -> + x = y. +Proof. + assert (forall x, 0 <= x -> + forall y, + (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) -> + x = y). + { + intros x0 POS0; pattern x0; apply Zdiv2_pos_ind; auto. + - intros. symmetry. apply Ztestbit_is_zero. + intros. rewrite <- H; auto. apply Z.testbit_0_l. + - intros. rewrite (Zdecomp x); rewrite (Zdecomp y). f_equal. + + exploit (H0 0). omega. rewrite !(Ztestbit_eq 0). + rewrite !zeq_true. auto. omega. omega. + + intros. apply H; intros. + exploit (H0 (Zsucc i)). omega. rewrite !(Ztestbit_eq (Z.succ i)). + rewrite !zeq_false. rewrite !Z.pred_succ. auto. + omega. omega. omega. omega. + } + intros. destruct (zle 0 x). + - apply H; auto. + - assert (-x-1 = -y-1). + { apply H. omega. intros. rewrite !Z_one_complement; auto. + rewrite H0; auto. + } + omega. +Qed. +modulus *) Lemma modu_divu_Euclid: forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y). @@ -1107,15 +1114,28 @@ Proof. apply H0. apply modu_divu_Euclid. auto. Qed. +Lemma mods_divs_Euclid: + forall x y, x = add (mul (divs x y) y) (mods x y). +Proof. + intros. unfold add, mul, divs, mods. + transitivity (repr (signed x)). auto with ints. + apply eqm_samerepr. + set (x' := signed x). set (y' := signed y). + apply eqm_trans with ((Z.quot x' y') * y' + Z.rem x' y'). + apply eqm_refl2. rewrite Zmult_comm. apply Z.quot_rem'. + apply eqm_add; auto with ints. + apply eqm_unsigned_repr_r. apply eqm_mult; auto with ints. + unfold y'. apply eqm_signed_unsigned. +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. + 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 H. apply mods_divs_Euclid. Qed. Theorem divu_one: @@ -1131,14 +1151,24 @@ Proof. apply one_not_zero. Qed. +Require Import Zquot. + Theorem divs_mone: forall x, divs x mone = neg x. Proof. unfold divs, neg; intros. - rewrite signed_mone. replace (Zdiv_round (signed x) (-1)) with (- (signed x)). + rewrite signed_mone. + replace (Z.quot (signed x) (-1)) with (- (signed x)). apply eqm_samerepr. apply eqm_neg. apply eqm_signed_unsigned. - unfold Zdiv_round. destruct (zlt (signed x) 0). - simpl. rewrite Zdiv_1_r. auto. simpl. rewrite Zdiv_1_r. auto. + set (x' := signed x). + set (one := 1). + change (-1) with (- one). rewrite Zquot_opp_r. + assert (Z.quot x' one = x'). + symmetry. apply Zquot_unique_full with 0. red. + change (Z.abs one) with 1. + destruct (zle 0 x'). left. omega. right. omega. + unfold one; ring. + congruence. Qed. Theorem mods_mone: @@ -1148,308 +1178,423 @@ Proof. rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem. Qed. -(** ** Properties of binary decompositions *) +(** ** Bit-level properties *) + +(** ** Properties of bit-level operations over [Z] *) -Lemma Z_of_bits_exten: - 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. +Remark Ztestbit_0: forall n, Z.testbit 0 n = false. +Proof Z.testbit_0_l. + +Remark Ztestbit_m1: forall n, 0 <= n -> Z.testbit (-1) n = true. Proof. - 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. + intros. destruct n; simpl; auto. Qed. -Lemma Z_of_bits_of_Z: - forall x, eqm (Z_of_bits wordsize (bits_of_Z wordsize x) 0) x. +Remark Zshiftin_spec: + forall b x, Zshiftin b x = 2 * x + (if b then 1 else 0). Proof. - assert (forall n x, exists k, - 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. destruct (Z_bin_decomp x) as [b y] eqn:?. - 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_bin_comp_decomp2 _ _ _ Heqp). - repeat rewrite Z_bin_comp_eq. ring. - apply Z_of_bits_exten. intros. - rewrite zeq_false. decEq. omega. omega. - intro. exact (H wordsize x). + unfold Zshiftin; intros. destruct b. + - rewrite Z.succ_double_spec. omega. + - rewrite Z.double_spec. omega. Qed. -Lemma bits_of_Z_zero: - forall n x, bits_of_Z n 0 x = false. +Remark Zshiftin_inj: + forall b1 x1 b2 x2, + Zshiftin b1 x1 = Zshiftin b2 x2 -> b1 = b2 /\ x1 = x2. Proof. - induction n; simpl; intros. auto. destruct (zeq x 0); auto. + intros. rewrite !Zshiftin_spec in H. + destruct b1; destruct b2. + split; [auto|omega]. + omegaContradiction. + omegaContradiction. + split; [auto|omega]. Qed. -Remark Z_bin_decomp_2xm1: - forall x, Z_bin_decomp (2 * x - 1) = (true, x - 1). +Remark Zdecomp: + forall x, x = Zshiftin (Z.odd x) (Z.div2 x). Proof. - intros. caseEq (Z_bin_decomp (2 * x - 1)). intros b y EQ. - apply Z_bin_comp_inj. - rewrite <- (Z_bin_comp_decomp2 _ _ _ EQ). - rewrite Z_bin_comp_eq. - omega. + intros. destruct x; simpl. + - auto. + - destruct p; auto. + - destruct p; auto. simpl. rewrite Pos.pred_double_succ. auto. 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. +Remark Ztestbit_shiftin: + forall b x n, + 0 <= n -> + Z.testbit (Zshiftin b x) n = if zeq n 0 then b else Z.testbit x (Z.pred n). Proof. - 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. - 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. + intros. rewrite Zshiftin_spec. destruct (zeq n 0). + - subst n. destruct b. + + apply Z.testbit_odd_0. + + rewrite Zplus_0_r. apply Z.testbit_even_0. + - assert (0 <= Z.pred n) by omega. + set (n' := Z.pred n) in *. + replace n with (Z.succ n') by (unfold n'; omega). + destruct b. + + apply Z.testbit_odd_succ; auto. + + rewrite Zplus_0_r. apply Z.testbit_even_succ; auto. Qed. -Lemma bits_of_Z_mone: - forall x, - 0 <= x < Z_of_nat wordsize -> - bits_of_Z wordsize (modulus - 1) x = true. +Remark Ztestbit_shiftin_base: + forall b x, Z.testbit (Zshiftin b x) 0 = b. Proof. - intros. unfold modulus. rewrite two_power_nat_two_p. - rewrite bits_of_Z_two_p. unfold proj_sumbool. apply zlt_true; omega. - omega. omega. + intros. rewrite Ztestbit_shiftin. apply zeq_true. omega. Qed. -Lemma Z_of_bits_range: - forall f n i, 0 <= Z_of_bits n f i < two_power_nat n. +Remark Ztestbit_shiftin_succ: + forall b x n, 0 <= n -> Z.testbit (Zshiftin b x) (Z.succ n) = Z.testbit x n. Proof. - induction n; simpl; intros. - rewrite two_power_nat_O. omega. - rewrite two_power_nat_S. - generalize (IHn (Zsucc i)). - intro. rewrite Z_bin_comp_eq. destruct (f i); omega. + intros. rewrite Ztestbit_shiftin. rewrite zeq_false. rewrite Z.pred_succ. auto. + omega. omega. Qed. -Lemma Z_of_bits_range_1: - forall f i, 0 <= Z_of_bits wordsize f i < modulus. +Remark Ztestbit_eq: + forall n x, 0 <= n -> + Z.testbit x n = if zeq n 0 then Z.odd x else Z.testbit (Z.div2 x) (Z.pred n). Proof. - intros. apply Z_of_bits_range. + intros. rewrite (Zdecomp x) at 1. apply Ztestbit_shiftin; auto. Qed. -Hint Resolve Z_of_bits_range_1: ints. -Lemma Z_of_bits_range_2: - forall f i, 0 <= Z_of_bits wordsize f i <= max_unsigned. +Remark Ztestbit_base: + forall x, Z.testbit x 0 = Z.odd x. Proof. - intros. unfold max_unsigned. - generalize (Z_of_bits_range_1 f i). omega. + intros. rewrite Ztestbit_eq. apply zeq_true. 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). +Remark Ztestbit_succ: + forall n x, 0 <= n -> Z.testbit x (Z.succ n) = Z.testbit (Z.div2 x) n. Proof. - induction n; intros; simpl. - simpl in H. omegaContradiction. - rewrite Z_bin_decomp_comp. - destruct (zeq i 0). - f_equal. omega. - rewrite IHn. f_equal. omega. - rewrite inj_S in H. omega. -Qed. + intros. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. auto. + 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 0) i = f i. +Lemma eqmod_same_bits: + forall n x y, + (forall i, 0 <= i < Z.of_nat n -> Z.testbit x i = Z.testbit y i) -> + eqmod (two_power_nat n) x y. Proof. - intros. rewrite bits_of_Z_of_bits_gen; auto. decEq; omega. -Qed. + induction n; intros. + - change (two_power_nat 0) with 1. exists (x-y); ring. + - rewrite two_power_nat_S. + assert (eqmod (two_power_nat n) (Z.div2 x) (Z.div2 y)). + apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite inj_S; omega. + omega. omega. + destruct H0 as [k EQ]. + exists k. rewrite (Zdecomp x). rewrite (Zdecomp y). + replace (Z.odd y) with (Z.odd x). + rewrite EQ. rewrite !Zshiftin_spec. ring. + exploit (H 0). rewrite inj_S; omega. + rewrite !Ztestbit_base. auto. +Qed. + +Lemma eqm_same_bits: + forall x y, + (forall i, 0 <= i < zwordsize -> Z.testbit x i = Z.testbit y i) -> + eqm x y. +Proof (eqmod_same_bits wordsize). -Lemma bits_of_Z_below: - forall n x i, i < 0 -> bits_of_Z n x i = false. +Lemma same_bits_eqmod: + forall n x y i, + eqmod (two_power_nat n) x y -> 0 <= i < Z.of_nat n -> + Z.testbit x i = Z.testbit y i. Proof. - induction n; intros; simpl. auto. - destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn. - omega. omega. -Qed. - -Lemma bits_of_Z_above: - forall n x i, i >= Z_of_nat n -> bits_of_Z n x i = false. + induction n; intros. + - simpl in H0. omegaContradiction. + - rewrite inj_S in H0. rewrite two_power_nat_S in H. + rewrite !(Ztestbit_eq i); intuition. + destruct H as [k EQ]. + assert (EQ': Zshiftin (Z.odd x) (Z.div2 x) = + Zshiftin (Z.odd y) (k * two_power_nat n + Z.div2 y)). + { + rewrite (Zdecomp x) in EQ. rewrite (Zdecomp y) in EQ. + rewrite EQ. rewrite !Zshiftin_spec. ring. + } + exploit Zshiftin_inj; eauto. intros [A B]. + destruct (zeq i 0). + + auto. + + apply IHn. exists k; auto. omega. +Qed. + +Lemma same_bits_eqm: + forall x y i, + eqm x y -> + 0 <= i < zwordsize -> + Z.testbit x i = Z.testbit y i. +Proof (same_bits_eqmod wordsize). + +Remark two_power_nat_infinity: + forall x, 0 <= x -> exists n, x < two_power_nat n. +Proof. + intros x0 POS0; pattern x0; apply natlike_ind; auto. + exists O. compute; auto. + intros. destruct H0 as [n LT]. exists (S n). rewrite two_power_nat_S. + generalize (two_power_nat_pos n). omega. +Qed. + +Lemma equal_same_bits: + forall x y, + (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) -> + x = y. Proof. - induction n; intros; simpl. - 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. + intros. + set (z := if zlt x y then y - x else x - y). + assert (0 <= z). + unfold z; destruct (zlt x y); omega. + exploit (two_power_nat_infinity z); auto. intros [n LT]. + assert (eqmod (two_power_nat n) x y). + apply eqmod_same_bits. intros. apply H. tauto. + assert (eqmod (two_power_nat n) z 0). + unfold z. destruct (zlt x y). + replace 0 with (y - y) by omega. apply eqmod_sub. apply eqmod_refl. auto. + replace 0 with (x - x) by omega. apply eqmod_sub. apply eqmod_refl. apply eqmod_sym; auto. + assert (z = 0). + apply eqmod_small_eq with (two_power_nat n). auto. omega. generalize (two_power_nat_pos n); omega. + unfold z in H3. destruct (zlt x y); omega. +Qed. + +Lemma Z_one_complement: + forall i, 0 <= i -> + forall x, Z.testbit (-x-1) i = negb (Z.testbit x i). +Proof. + intros i0 POS0. pattern i0. apply Zlt_0_ind; auto. + intros i IND POS x. + rewrite (Zdecomp x). set (y := Z.div2 x). + replace (- Zshiftin (Z.odd x) y - 1) + with (Zshiftin (negb (Z.odd x)) (- y - 1)). + rewrite !Ztestbit_shiftin; auto. + destruct (zeq i 0). auto. apply IND. omega. + rewrite !Zshiftin_spec. destruct (Z.odd x); simpl negb; ring. +Qed. + +Lemma Ztestbit_above: + forall n x i, + 0 <= x < two_power_nat n -> + i >= Z.of_nat n -> + Z.testbit x i = false. +Proof. + induction n; intros. + - change (two_power_nat 0) with 1 in H. + replace x with 0 by omega. + apply Z.testbit_0_l. + - rewrite inj_S in H0. rewrite Ztestbit_eq. rewrite zeq_false. + apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H. + rewrite Zshiftin_spec in H. destruct (Z.odd x); omega. + omega. omega. omega. Qed. -Lemma bits_of_Z_greater: +Lemma Ztestbit_above_neg: forall n x i, - 0 <= x < two_p i -> bits_of_Z n x i = false. -Proof. - induction n; intros. - auto. - destruct (zlt i 0). apply bits_of_Z_below. auto. - simpl. - destruct (Z_bin_decomp x) as [b x1] eqn:?. - destruct (zeq i 0). - subst i. simpl in H. assert (x = 0) by omega. subst x. simpl in Heqp. congruence. - apply IHn. - rewrite (Z_bin_comp_decomp2 _ _ _ Heqp) in H. - replace i with (Zsucc (i-1)) in H by omega. rewrite two_p_S in H. - rewrite Z_bin_comp_eq in H. destruct b; omega. + -two_power_nat n <= x < 0 -> + i >= Z.of_nat n -> + Z.testbit x i = true. +Proof. + intros. set (y := -x-1). + assert (Z.testbit y i = false). + apply Ztestbit_above with n. + unfold y; omega. auto. + unfold y in H1. rewrite Z_one_complement in H1. + change true with (negb false). rewrite <- H1. rewrite negb_involutive; auto. omega. Qed. -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 + j). +Lemma Zsign_bit: + forall n x, + 0 <= x < two_power_nat (S n) -> + Z.testbit x (Z_of_nat n) = if zlt x (two_power_nat n) then false else true. +Proof. + induction n; intros. + - change (two_power_nat 1) with 2 in H. + assert (x = 0 \/ x = 1) by omega. + destruct H0; subst x; reflexivity. + - rewrite inj_S. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. + rewrite IHn. rewrite two_power_nat_S. + destruct (zlt (Z.div2 x) (two_power_nat n)); rewrite (Zdecomp x); rewrite Zshiftin_spec. + rewrite zlt_true. auto. destruct (Z.odd x); omega. + rewrite zlt_false. auto. destruct (Z.odd x); omega. + rewrite (Zdecomp x) in H; rewrite Zshiftin_spec in H. + rewrite two_power_nat_S in H. destruct (Z.odd x); omega. + omega. omega. +Qed. + +Lemma Zshiftin_ind: + forall (P: Z -> Prop), + P 0 -> + (forall b x, 0 <= x -> P x -> P (Zshiftin b x)) -> + forall x, 0 <= x -> P x. +Proof. + intros. destruct x. + - auto. + - induction p. + + change (P (Zshiftin true (Z.pos p))). auto. + + change (P (Zshiftin false (Z.pos p))). auto. + + change (P (Zshiftin true 0)). apply H0. omega. auto. + - compute in H1. intuition congruence. +Qed. + +Lemma Zshiftin_pos_ind: + forall (P: Z -> Prop), + P 1 -> + (forall b x, 0 < x -> P x -> P (Zshiftin b x)) -> + forall x, 0 < x -> P x. +Proof. + intros. destruct x; simpl in H1; try discriminate. + induction p. + + change (P (Zshiftin true (Z.pos p))). auto. + + change (P (Zshiftin false (Z.pos p))). auto. + + auto. +Qed. + +Lemma Ztestbit_le: + forall x y, + 0 <= y -> + (forall i, 0 <= i -> Z.testbit x i = true -> Z.testbit y i = true) -> + x <= y. Proof. - 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_gen. omega. -Qed. + intros x y0 POS0; revert x; pattern y0; apply Zshiftin_ind; auto; intros. + - replace x with 0. omega. apply equal_same_bits; intros. + rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto. + exploit H; eauto. rewrite Ztestbit_0. auto. + - assert (Z.div2 x0 <= x). + { apply H0. intros. exploit (H1 (Zsucc i)). + omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto. + } + rewrite (Zdecomp x0). rewrite !Zshiftin_spec. + destruct (Z.odd x0) as [] eqn:E1; destruct b as [] eqn:E2; try omega. + exploit (H1 0). omega. rewrite Ztestbit_base; auto. + rewrite Ztestbit_shiftin_base. congruence. +Qed. + +(** ** Bit-level reasoning over type [int] *) -Lemma Z_of_bits_excl: - 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. +Definition testbit (x: int) (i: Z) : bool := Z.testbit (unsigned x) i. + +Lemma testbit_repr: + forall x i, + 0 <= i < zwordsize -> + testbit (repr x) i = Z.testbit x i. Proof. - induction n. - intros; reflexivity. - intros. simpl. rewrite inj_S in H. rewrite inj_S in H0. - rewrite <- (IHn f g h (Zsucc j)). - assert (j <= j < j + Zsucc(Z_of_nat n)). omega. - repeat rewrite Z_bin_comp_eq. - rewrite <- H0; auto. - 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. + intros. unfold testbit. apply same_bits_eqm; auto with ints. 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. +Lemma same_bits_eq: + forall x y, + (forall i, 0 <= i < zwordsize -> testbit x i = testbit y i) -> + x = y. 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. - repeat rewrite Z_bin_comp_eq. ring. + intros. rewrite <- (repr_unsigned x). rewrite <- (repr_unsigned y). + apply eqm_samerepr. apply eqm_same_bits. auto. Qed. -Lemma Z_of_bits_truncate: - forall f n i, - eqm (Z_of_bits (wordsize + n) f i) (Z_of_bits wordsize f i). +Lemma bits_above: + forall x i, i >= zwordsize -> testbit x i = false. Proof. - intros. exists (Z_of_bits n f (i + Z_of_nat wordsize)). - rewrite Z_of_bits_compose. fold modulus. auto. -Qed. + intros. apply Ztestbit_above with wordsize; auto. apply unsigned_range. +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. +Lemma bits_zero: + forall i, testbit zero i = false. Proof. - induction n; intros; simpl. auto. - rewrite inj_S in H. rewrite H. rewrite IHn. auto. - intros; apply H; omega. omega. + intros. unfold testbit. rewrite unsigned_zero. apply Ztestbit_0. Qed. -Lemma Z_of_bits_complement: - forall f n i, - Z_of_bits n (fun j => negb (f j)) i = two_power_nat n - 1 - Z_of_bits n f i. +Lemma bits_mone: + forall i, 0 <= i < zwordsize -> testbit mone i = true. Proof. - induction n; intros; simpl Z_of_bits. - auto. - rewrite two_power_nat_S. rewrite IHn. repeat rewrite Z_bin_comp_eq. - destruct (f i); simpl negb; ring. + intros. unfold mone. rewrite testbit_repr; auto. apply Ztestbit_m1. 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. +Hint Rewrite bits_zero bits_mone : ints. + +Ltac bit_solve := + intros; apply same_bits_eq; intros; autorewrite with ints; auto with bool. + +Lemma sign_bit_of_unsigned: + forall x, testbit x (zwordsize - 1) = if zlt (unsigned x) half_modulus then false else true. Proof. - intros. set (z := fun (i: Z) => false). - transitivity (Z_of_bits n (fun j => negb (z j)) i). - apply Z_of_bits_exten; intros. unfold z. rewrite H. auto. omega. - rewrite Z_of_bits_complement. rewrite Z_of_bits_false. omega. - unfold z; auto. + intros. unfold testbit. + set (ws1 := pred wordsize). + assert (zwordsize - 1 = Z_of_nat ws1). + unfold zwordsize, ws1, wordsize. + destruct WS.wordsize as [] eqn:E. + elim WS.wordsize_not_zero; auto. + rewrite inj_S. simpl. omega. + assert (half_modulus = two_power_nat ws1). + rewrite two_power_nat_two_p. rewrite <- H. apply half_modulus_power. + rewrite H; rewrite H0. + apply Zsign_bit. rewrite two_power_nat_S. rewrite <- H0. + rewrite <- half_modulus_modulus. apply unsigned_range. Qed. - -Lemma Z_of_bits_equal: - forall f x, - (forall i, 0 <= i < Z_of_nat wordsize -> f i = bits_of_Z wordsize (unsigned x) i) -> - repr (Z_of_bits wordsize f 0) = x. + +Lemma bits_signed: + forall x i, 0 <= i -> + Z.testbit (signed x) i = testbit x (if zlt i zwordsize then i else zwordsize - 1). Proof. - intros. transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)) 0)). - f_equal. apply Z_of_bits_exten; intros. apply H. omega. - apply eqm_repr_eq. apply Z_of_bits_of_Z. + intros. + destruct (zlt i zwordsize). + - apply same_bits_eqm. apply eqm_signed_unsigned. omega. + - unfold signed. rewrite sign_bit_of_unsigned. destruct (zlt (unsigned x) half_modulus). + + apply Ztestbit_above with wordsize. apply unsigned_range. auto. + + apply Ztestbit_above_neg with wordsize. + fold modulus. generalize (unsigned_range x). omega. auto. Qed. +Lemma bits_le: + forall x y, + (forall i, 0 <= i < zwordsize -> testbit x i = true -> testbit y i = true) -> + unsigned x <= unsigned y. +Proof. + intros. apply Ztestbit_le. generalize (unsigned_range y); omega. + intros. fold (testbit y i). destruct (zlt i zwordsize). + apply H. omega. auto. + fold (testbit x i) in H1. rewrite bits_above in H1; auto. congruence. +Qed. + (** ** Properties of bitwise and, or, xor *) -Lemma bitwise_binop_commut: - forall f, - (forall a b, f a b = f b a) -> - forall x y, - bitwise_binop f x y = bitwise_binop f y x. +Lemma bits_and: + forall x y i, 0 <= i < zwordsize -> + testbit (and x y) i = testbit x i && testbit y i. Proof. - unfold bitwise_binop; intros. decEq; apply Z_of_bits_exten; intros. auto. + intros. unfold and. rewrite testbit_repr; auto. rewrite Z.land_spec; intuition. Qed. -Lemma bitwise_binop_assoc: - forall f, - (forall a b c, f a (f b c) = f (f a b) c) -> - forall x y z, - bitwise_binop f (bitwise_binop f x y) z = - bitwise_binop f x (bitwise_binop f y z). +Lemma bits_or: + forall x y i, 0 <= i < zwordsize -> + testbit (or x y) i = testbit x i || testbit y i. Proof. - 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. + intros. unfold or. rewrite testbit_repr; auto. rewrite Z.lor_spec; intuition. Qed. -Lemma bitwise_binop_idem: - forall f, - (forall a, f a a = a) -> - forall x, - bitwise_binop f x x = x. +Lemma bits_xor: + forall x y i, 0 <= i < zwordsize -> + testbit (xor x y) i = xorb (testbit x i) (testbit y i). Proof. - unfold bitwise_binop; intros. apply Z_of_bits_equal; intros. auto. + intros. unfold xor. rewrite testbit_repr; auto. rewrite Z.lxor_spec; intuition. Qed. +Lemma bits_not: + forall x i, 0 <= i < zwordsize -> + testbit (not x) i = negb (testbit x i). +Proof. + intros. unfold not. rewrite bits_xor; auto. rewrite bits_mone; auto. +Qed. + +Hint Rewrite bits_and bits_or bits_xor bits_not: ints. + Theorem and_commut: forall x y, and x y = and y x. -Proof (bitwise_binop_commut andb andb_comm). +Proof. + bit_solve. +Qed. Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z). -Proof (bitwise_binop_assoc andb andb_assoc). +Proof. + bit_solve. +Qed. Theorem and_zero: forall x, and x zero = zero. Proof. - intros. unfold and, bitwise_binop. apply Z_of_bits_equal; intros. - rewrite unsigned_zero. rewrite bits_of_Z_zero. apply andb_b_false. + bit_solve. apply andb_b_false. Qed. Corollary and_zero_l: forall x, and zero x = zero. @@ -1459,9 +1604,7 @@ Qed. Theorem and_mone: forall x, and x mone = x. Proof. - intros. unfold and, bitwise_binop. apply Z_of_bits_equal; intros. - rewrite unsigned_mone. rewrite bits_of_Z_mone. apply andb_b_true. - omega. + bit_solve. apply andb_b_true. Qed. Corollary and_mone_l: forall x, and mone x = x. @@ -1471,19 +1614,22 @@ Qed. Theorem and_idem: forall x, and x x = x. Proof. - intros. apply (bitwise_binop_idem andb). destruct a; auto. + bit_solve. destruct (testbit x i); auto. Qed. Theorem or_commut: forall x y, or x y = or y x. -Proof (bitwise_binop_commut orb orb_comm). +Proof. + bit_solve. +Qed. Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z). -Proof (bitwise_binop_assoc orb orb_assoc). +Proof. + bit_solve. +Qed. Theorem or_zero: forall x, or x zero = x. Proof. - intros. unfold or, bitwise_binop. apply Z_of_bits_equal; intros. - rewrite unsigned_zero. rewrite bits_of_Z_zero. apply orb_b_false. + bit_solve. Qed. Corollary or_zero_l: forall x, or zero x = x. @@ -1493,30 +1639,19 @@ Qed. Theorem or_mone: forall x, or x mone = mone. Proof. - intros. unfold or, bitwise_binop. apply Z_of_bits_equal; intros. - rewrite unsigned_mone. rewrite bits_of_Z_mone. apply orb_b_true. - omega. -Qed. - -Corollary or_mone_l: forall x, or mone x = mone. -Proof. - intros. rewrite or_commut. apply or_mone. + bit_solve. Qed. Theorem or_idem: forall x, or x x = x. Proof. - intros. apply (bitwise_binop_idem orb). destruct a; auto. + bit_solve. destruct (testbit x i); auto. Qed. Theorem and_or_distrib: forall x y z, and x (or y z) = or (and x y) (and x z). Proof. - intros; unfold and, or, bitwise_binop. - 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. + bit_solve. apply demorgan1. Qed. Corollary and_or_distrib_l: @@ -1530,11 +1665,7 @@ Theorem or_and_distrib: forall x y z, or x (and y z) = and (or x y) (or x z). Proof. - intros; unfold and, or, bitwise_binop. - 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 orb_andb_distrib_r. + bit_solve. apply orb_andb_distrib_r. Qed. Corollary or_and_distrib_l: @@ -1546,35 +1677,31 @@ Qed. Theorem and_or_absorb: forall x y, and x (or x y) = x. Proof. - intros; unfold and, or, bitwise_binop. apply Z_of_bits_equal; intros. - rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits. - assert (forall a b, a && (a || b) = a) by (destruct a; destruct b; auto). + bit_solve. + assert (forall a b, a && (a || b) = a) by destr_bool. auto. - omega. Qed. Theorem or_and_absorb: forall x y, or x (and x y) = x. Proof. - intros; unfold and, or, bitwise_binop. apply Z_of_bits_equal; intros. - rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits. - assert (forall a b, a || (a && b) = a) by (destruct a; destruct b; auto). + bit_solve. + assert (forall a b, a || (a && b) = a) by destr_bool. auto. - omega. Qed. Theorem xor_commut: forall x y, xor x y = xor y x. -Proof (bitwise_binop_commut xorb xorb_comm). +Proof. + bit_solve. apply xorb_comm. +Qed. Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z). Proof. - intros. apply (bitwise_binop_assoc xorb). - intros. symmetry. apply xorb_assoc. + bit_solve. apply xorb_assoc. Qed. Theorem xor_zero: forall x, xor x zero = x. Proof. - intros. unfold xor, bitwise_binop. apply Z_of_bits_equal; intros. - rewrite unsigned_zero. rewrite bits_of_Z_zero. apply xorb_false. + bit_solve. apply xorb_false. Qed. Corollary xor_zero_l: forall x, xor zero x = x. @@ -1584,8 +1711,7 @@ Qed. Theorem xor_idem: forall x, xor x x = zero. Proof. - intros. unfold xor, bitwise_binop. apply Z_of_bits_equal; intros. - rewrite unsigned_zero. rewrite bits_of_Z_zero. apply xorb_nilpotent. + bit_solve. apply xorb_nilpotent. Qed. Theorem xor_zero_one: xor zero one = one. @@ -1596,39 +1722,35 @@ Proof. apply xor_idem. Qed. Theorem xor_zero_equal: forall x y, xor x y = zero -> x = y. Proof. - unfold xor, bitwise_binop; intros. - set (ux := unsigned x) in *. set (uy := unsigned y) in *. - set (fx := bits_of_Z wordsize ux) in *. - set (fy := bits_of_Z wordsize uy) in *. - assert (forall i, 0 <= i < Z_of_nat wordsize -> fx i = fy i). - intros. - assert (bits_of_Z wordsize (unsigned (repr (Z_of_bits wordsize (fun i => xorb (fx i) (fy i)) 0))) i = false). - rewrite H. rewrite unsigned_zero. apply bits_of_Z_zero. - rewrite unsigned_repr in H1; auto with ints. - rewrite bits_of_Z_of_bits in H1; auto. - destruct (fx i); destruct (fy i); simpl in H1; congruence. - rewrite <- (repr_unsigned x); fold ux. - rewrite <- (repr_unsigned y); fold uy. - apply eqm_samerepr. - eapply eqm_trans. apply eqm_sym. apply Z_of_bits_of_Z. - eapply eqm_trans. 2: apply Z_of_bits_of_Z. - fold fx; fold fy. apply eqm_refl2. - apply Z_of_bits_exten. intros; apply H0; omega. + intros. apply same_bits_eq; intros. + assert (xorb (testbit x i) (testbit y i) = false). + rewrite <- bits_xor; auto. rewrite H. apply bits_zero. + destruct (testbit x i); destruct (testbit y i); reflexivity || discriminate. Qed. Theorem and_xor_distrib: forall x y z, and x (xor y z) = xor (and x y) (and x z). Proof. - intros; unfold and, xor, bitwise_binop. - 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. + bit_solve. + assert (forall a b c, a && (xorb b c) = xorb (a && b) (a && c)) by destr_bool. auto. Qed. +Theorem and_le: + forall x y, unsigned (and x y) <= unsigned x. +Proof. + intros. apply bits_le; intros. + rewrite bits_and in H0; auto. rewrite andb_true_iff in H0. tauto. +Qed. + +Theorem or_le: + forall x y, unsigned x <= unsigned (or x y). +Proof. + intros. apply bits_le; intros. + rewrite bits_or; auto. rewrite H0; auto. +Qed. + (** Properties of bitwise complement.*) Theorem not_involutive: @@ -1652,57 +1774,46 @@ Qed. Theorem not_or_and_not: forall x y, not (or x y) = and (not x) (not y). Proof. - intros; unfold not, xor, and, or, bitwise_binop. - 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 unsigned_mone. rewrite bits_of_Z_mone; auto. - assert (forall a b, xorb (a || b) true = xorb a true && xorb b true). - destruct a; destruct b; reflexivity. - auto. + bit_solve. apply negb_orb. Qed. Theorem not_and_or_not: forall x y, not (and x y) = or (not x) (not y). Proof. - intros. rewrite <- (not_involutive x) at 1. rewrite <- (not_involutive y) at 1. - rewrite <- not_or_and_not. apply not_involutive. + bit_solve. apply negb_andb. Qed. Theorem and_not_self: forall x, and x (not x) = zero. Proof. - intros. unfold not. rewrite and_xor_distrib. - rewrite and_idem. rewrite and_mone. apply xor_idem. + bit_solve. Qed. Theorem or_not_self: forall x, or x (not x) = mone. Proof. - intros. rewrite <- (not_involutive x) at 1. rewrite or_commut. - rewrite <- not_and_or_not. rewrite and_not_self. apply not_zero. + bit_solve. Qed. Theorem xor_not_self: forall x, xor x (not x) = mone. Proof. - intros. unfold not. rewrite <- xor_assoc. rewrite xor_idem. apply not_zero. + bit_solve. destruct (testbit x i); auto. Qed. Theorem not_neg: forall x, not x = add (neg x) mone. Proof. - intros. - unfold not, xor, bitwise_binop. rewrite unsigned_mone. - set (ux := unsigned x). - set (bx := bits_of_Z wordsize ux). - transitivity (repr (Z_of_bits wordsize (fun i => negb (bx i)) 0)). - decEq. apply Z_of_bits_exten. intros. rewrite bits_of_Z_mone; auto. omega. - rewrite Z_of_bits_complement. apply eqm_samerepr. rewrite unsigned_mone. fold modulus. - replace (modulus - 1 - Z_of_bits wordsize bx 0) - with ((- Z_of_bits wordsize bx 0) + (modulus - 1)) by omega. - apply eqm_add. unfold neg. apply eqm_unsigned_repr_r. apply eqm_neg. - apply Z_of_bits_of_Z. apply eqm_refl. + bit_solve. + rewrite <- (repr_unsigned x) at 1. unfold add. + rewrite !testbit_repr; auto. + transitivity (Z.testbit (-unsigned x - 1) i). + symmetry. apply Z_one_complement. omega. + apply same_bits_eqm; auto. + replace (-unsigned x - 1) with (-unsigned x + (-1)) by omega. + apply eqm_add. + unfold neg. apply eqm_unsigned_repr. + rewrite unsigned_mone. exists (-1). ring. Qed. Theorem neg_not: @@ -1716,42 +1827,48 @@ Qed. (** Connections between [add] and bitwise logical operations. *) +Lemma Z_add_is_or: + forall i, 0 <= i -> + forall x y, + (forall j, 0 <= j <= i -> Z.testbit x j && Z.testbit y j = false) -> + Z.testbit (x + y) i = Z.testbit x i || Z.testbit y i. +Proof. + intros i0 POS0. pattern i0. apply Zlt_0_ind; auto. + intros i IND POS x y EXCL. + rewrite (Zdecomp x) in *. rewrite (Zdecomp y) in *. + transitivity (Z.testbit (Zshiftin (Z.odd x || Z.odd y) (Z.div2 x + Z.div2 y)) i). + - f_equal. rewrite !Zshiftin_spec. + exploit (EXCL 0). omega. rewrite !Ztestbit_shiftin_base. intros. +Opaque Z.mul. + destruct (Z.odd x); destruct (Z.odd y); simpl in *; discriminate || ring. + - rewrite !Ztestbit_shiftin; auto. + destruct (zeq i 0). + + auto. + + apply IND. omega. intros. + exploit (EXCL (Z.succ j)). omega. + rewrite !Ztestbit_shiftin_succ. auto. + omega. omega. +Qed. + Theorem add_is_or: forall x y, and x y = zero -> add x y = or x y. Proof. - intros. unfold add, or, bitwise_binop. - apply eqm_samerepr. eapply eqm_trans. apply eqm_add. - apply eqm_sym. apply Z_of_bits_of_Z. - apply eqm_sym. apply Z_of_bits_of_Z. - apply eqm_refl2. - apply Z_of_bits_excl. + bit_solve. unfold add. rewrite testbit_repr; auto. + apply Z_add_is_or. omega. intros. - replace (bits_of_Z wordsize (unsigned x) i && - bits_of_Z wordsize (unsigned y) i) - with (bits_of_Z wordsize (unsigned (and x y)) i). - rewrite H. rewrite unsigned_zero. rewrite bits_of_Z_zero. auto. - unfold and, bitwise_binop. rewrite unsigned_repr; auto with ints. - rewrite bits_of_Z_of_bits. reflexivity. auto. - auto. + assert (testbit (and x y) j = testbit zero j) by congruence. + autorewrite with ints in H2. assumption. omega. Qed. Theorem xor_is_or: forall x y, and x y = zero -> xor x y = or x y. Proof. - intros. unfold xor, or, bitwise_binop. - decEq. apply Z_of_bits_exten; intros. - set (bitx := bits_of_Z wordsize (unsigned x) (i + 0)). - set (bity := bits_of_Z wordsize (unsigned y) (i + 0)). - assert (bitx && bity = false). - replace (bitx && bity) - with (bits_of_Z wordsize (unsigned (and x y)) (i + 0)). - rewrite H. rewrite unsigned_zero. apply bits_of_Z_zero. - unfold and, bitwise_binop. rewrite unsigned_repr; auto with ints. - unfold bitx, bity. rewrite bits_of_Z_of_bits. reflexivity. - omega. - destruct bitx; destruct bity; auto; simpl in H1; congruence. + bit_solve. + assert (testbit (and x y) i = testbit zero i) by congruence. + autorewrite with ints in H1; auto. + destruct (testbit x i); destruct (testbit y i); simpl in *; congruence. Qed. Theorem add_is_xor: @@ -1779,49 +1896,82 @@ Qed. (** ** Properties of shifts *) +Lemma bits_shl: + forall x y i, + 0 <= i < zwordsize -> + testbit (shl x y) i = + if zlt i (unsigned y) then false else testbit x (i - unsigned y). +Proof. + intros. unfold shl. rewrite testbit_repr; auto. + destruct (zlt i (unsigned y)). + apply Z.shiftl_spec_low. auto. + apply Z.shiftl_spec_high. omega. omega. +Qed. + +Lemma bits_shru: + forall x y i, + 0 <= i < zwordsize -> + testbit (shru x y) i = + if zlt (i + unsigned y) zwordsize then testbit x (i + unsigned y) else false. +Proof. + intros. unfold shru. rewrite testbit_repr; auto. + rewrite Z.shiftr_spec. fold (testbit x (i + unsigned y)). + destruct (zlt (i + unsigned y) zwordsize). + auto. + apply bits_above; auto. + omega. +Qed. + +Lemma bits_shr: + forall x y i, + 0 <= i < zwordsize -> + testbit (shr x y) i = + testbit x (if zlt (i + unsigned y) zwordsize then i + unsigned y else zwordsize - 1). +Proof. + intros. unfold shr. rewrite testbit_repr; auto. + rewrite Z.shiftr_spec. apply bits_signed. + generalize (unsigned_range y); omega. + omega. +Qed. + +Hint Rewrite bits_shl bits_shru bits_shr: ints. + Theorem shl_zero: forall x, shl x zero = x. Proof. - intros. unfold shl. rewrite unsigned_zero. simpl (-0). - transitivity (repr (unsigned x)). apply eqm_samerepr. apply Z_of_bits_of_Z. - auto with ints. + bit_solve. rewrite unsigned_zero. rewrite zlt_false. f_equal; omega. omega. Qed. Lemma bitwise_binop_shl: - forall f x y n, - f false false = false -> - bitwise_binop f (shl x n) (shl y n) = shl (bitwise_binop f x y) n. -Proof. - intros. unfold bitwise_binop, shl. - 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. - repeat rewrite bits_of_Z_of_bits_gen; auto. repeat rewrite Zplus_0_r. auto. - generalize (unsigned_range n). omega. + forall f f' x y n, + (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) -> + f' false false = false -> + f (shl x n) (shl y n) = shl (f x y) n. +Proof. + intros. apply same_bits_eq; intros. + rewrite H; auto. rewrite !bits_shl; auto. + destruct (zlt i (unsigned n)); auto. + rewrite H; auto. generalize (unsigned_range n); omega. Qed. Theorem and_shl: forall x y n, and (shl x n) (shl y n) = shl (and x y) n. Proof. - unfold and; intros. apply bitwise_binop_shl. reflexivity. + intros. apply bitwise_binop_shl with andb. exact bits_and. auto. 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. + intros. apply bitwise_binop_shl with orb. exact bits_or. auto. 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. + intros. apply bitwise_binop_shl with xorb. exact bits_xor. auto. Qed. Lemma ltu_inv: @@ -1832,6 +1982,12 @@ Proof. discriminate. Qed. +Lemma ltu_iwordsize_inv: + forall x, ltu x iwordsize = true -> 0 <= unsigned x < zwordsize. +Proof. + intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize. auto. +Qed. + Theorem shl_shl: forall x y z, ltu y iwordsize = true -> @@ -1839,67 +1995,57 @@ Theorem shl_shl: ltu (add y z) iwordsize = true -> shl (shl x y) z = shl x (add y z). Proof. - intros. unfold shl, add. - generalize (ltu_inv _ _ H). - generalize (ltu_inv _ _ H0). - rewrite unsigned_repr_wordsize. - set (x' := unsigned x). - set (y' := unsigned y). - set (z' := unsigned z). - 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). - symmetry. apply bits_of_Z_below. omega. - destruct (zle (Z_of_nat wordsize) (n + - z')). - symmetry. apply bits_of_Z_below. omega. - decEq. omega. - generalize two_wordsize_max_unsigned; omega. + intros. + generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. + assert (unsigned (add y z) = unsigned y + unsigned z). + unfold add. apply unsigned_repr. + generalize two_wordsize_max_unsigned; omega. + apply same_bits_eq; intros. + rewrite bits_shl; auto. + destruct (zlt i (unsigned z)). + - rewrite bits_shl; auto. rewrite zlt_true. auto. omega. + - rewrite bits_shl. destruct (zlt (i - unsigned z) (unsigned y)). + + rewrite bits_shl; auto. rewrite zlt_true. auto. omega. + + rewrite bits_shl; auto. rewrite zlt_false. f_equal. omega. omega. + + omega. 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. + bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; omega. omega. 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. + forall f f' x y n, + (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) -> + f' false false = false -> + f (shru x n) (shru y n) = shru (f x y) n. Proof. - 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. + intros. apply same_bits_eq; intros. + rewrite H; auto. rewrite !bits_shru; auto. + destruct (zlt (i + unsigned n) zwordsize); auto. + rewrite H; auto. generalize (unsigned_range n); omega. 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. + intros. apply bitwise_binop_shru with andb; auto. exact bits_and. 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. + intros. apply bitwise_binop_shru with orb; auto. exact bits_or. 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. + intros. apply bitwise_binop_shru with xorb; auto. exact bits_xor. Qed. Theorem shru_shru: @@ -1909,64 +2055,58 @@ Theorem shru_shru: ltu (add y z) iwordsize = true -> shru (shru x y) z = shru x (add y z). Proof. - intros. unfold shru, add. - generalize (ltu_inv _ _ H). - generalize (ltu_inv _ _ H0). - rewrite unsigned_repr_wordsize. - set (x' := unsigned x). - set (y' := unsigned y). - set (z' := unsigned z). - 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. + intros. + generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. + assert (unsigned (add y z) = unsigned y + unsigned z). + unfold add. apply unsigned_repr. + generalize two_wordsize_max_unsigned; omega. + apply same_bits_eq; intros. + rewrite bits_shru; auto. + destruct (zlt (i + unsigned z) zwordsize). + - rewrite bits_shru. destruct (zlt (i + unsigned z + unsigned y) zwordsize). + + rewrite bits_shru; auto. rewrite zlt_true. f_equal. omega. omega. + + rewrite bits_shru; auto. rewrite zlt_false. auto. omega. + + omega. + - rewrite bits_shru; auto. rewrite zlt_false. auto. omega. Qed. Theorem shr_zero: forall x, shr x zero = x. Proof. - 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. + bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; omega. omega. Qed. Lemma bitwise_binop_shr: - forall 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, 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. + forall f f' x y n, + (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) -> + f (shr x n) (shr y n) = shr (f x y) n. +Proof. + intros. apply same_bits_eq; intros. + rewrite H; auto. rewrite !bits_shr; auto. + rewrite H; auto. + destruct (zlt (i + unsigned n) zwordsize). + generalize (unsigned_range n); omega. + omega. Qed. Theorem and_shr: forall x y n, and (shr x n) (shr y n) = shr (and x y) n. Proof. - unfold and; intros. apply bitwise_binop_shr. + intros. apply bitwise_binop_shr with andb. exact bits_and. 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. + intros. apply bitwise_binop_shr with orb. exact bits_or. 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. + intros. apply bitwise_binop_shr with xorb. exact bits_xor. Qed. Theorem shr_shr: @@ -1976,73 +2116,31 @@ Theorem shr_shr: ltu (add y z) iwordsize = true -> shr (shr x y) z = shr x (add y z). Proof. - intros. unfold shr, add. - generalize (ltu_inv _ _ H). - generalize (ltu_inv _ _ H0). - rewrite unsigned_repr_wordsize. - set (x' := unsigned x). - set (y' := unsigned y). - set (z' := unsigned z). - 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. + intros. + generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. + assert (unsigned (add y z) = unsigned y + unsigned z). + unfold add. apply unsigned_repr. + generalize two_wordsize_max_unsigned; omega. + apply same_bits_eq; intros. + rewrite !bits_shr; auto. f_equal. + destruct (zlt (i + unsigned z) zwordsize). + rewrite H4. replace (i + (unsigned y + unsigned z)) with (i + unsigned z + unsigned y) by omega. auto. + rewrite (zlt_false _ (i + unsigned (add y z))). + destruct (zlt (zwordsize - 1 + unsigned y) zwordsize); omega. 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. - -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. + destruct (zlt (i + unsigned z) zwordsize); omega. Qed. Theorem and_shr_shru: forall x y z, and (shr x z) (shru y z) = shru (and x y) z. Proof. - intros. unfold and, shr, shru, bitwise_binop. - 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. - generalize (unsigned_range z); intros. - destruct (zlt (i + unsigned z) (Z_of_nat wordsize)). - rewrite bits_of_Z_of_bits_gen. - repeat rewrite Zplus_0_r. auto. omega. - set (b := bits_of_Z wordsize (unsigned x) (Z_of_nat wordsize - 1)). - repeat rewrite bits_of_Z_above; auto. apply andb_false_r. -Qed. + intros. apply same_bits_eq; intros. + rewrite bits_and; auto. rewrite bits_shr; auto. rewrite !bits_shru; auto. + destruct (zlt (i + unsigned z) zwordsize). + - rewrite bits_and; auto. generalize (unsigned_range z); omega. + - apply andb_false_r. +Qed. Theorem shr_and_shru_and: forall x y z, @@ -2056,26 +2154,78 @@ Qed. (** ** Properties of rotations *) +Lemma bits_rol: + forall x y i, + 0 <= i < zwordsize -> + testbit (rol x y) i = testbit x ((i - unsigned y) mod zwordsize). +Proof. + intros. unfold rol. + exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos. + set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize). + intros EQ. + exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos. + fold j. intros RANGE. + rewrite testbit_repr; auto. + rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega. + destruct (zlt i j). + - rewrite Z.shiftl_spec_low; auto. simpl. + unfold testbit. f_equal. + symmetry. apply Zmod_unique with (-k - 1). + rewrite EQ. ring. + omega. + - rewrite Z.shiftl_spec_high. + fold (testbit x (i + (zwordsize - j))). + rewrite bits_above. rewrite orb_false_r. + fold (testbit x (i - j)). + f_equal. symmetry. apply Zmod_unique with (-k). + rewrite EQ. ring. + omega. omega. omega. omega. +Qed. + +Lemma bits_ror: + forall x y i, + 0 <= i < zwordsize -> + testbit (ror x y) i = testbit x ((i + unsigned y) mod zwordsize). +Proof. + intros. unfold ror. + exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos. + set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize). + intros EQ. + exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos. + fold j. intros RANGE. + rewrite testbit_repr; auto. + rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega. + destruct (zlt (i + j) zwordsize). + - rewrite Z.shiftl_spec_low; auto. rewrite orb_false_r. + unfold testbit. f_equal. + symmetry. apply Zmod_unique with k. + rewrite EQ. ring. + omega. omega. + - rewrite Z.shiftl_spec_high. + fold (testbit x (i + j)). + rewrite bits_above. simpl. + unfold testbit. f_equal. + symmetry. apply Zmod_unique with (k + 1). + rewrite EQ. ring. + omega. omega. omega. omega. +Qed. + +Hint Rewrite bits_rol bits_ror: ints. + Theorem shl_rolm: forall x n, ltu n iwordsize = true -> shl x n = rolm x n (shl mone n). Proof. 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. + unfold rolm. apply same_bits_eq; intros. + rewrite bits_and; auto. rewrite !bits_shl; auto. rewrite bits_rol; 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. + - rewrite andb_false_r; auto. + - generalize (unsigned_range n); intros. + rewrite bits_mone. rewrite andb_true_r. f_equal. + symmetry. apply Zmod_small. omega. + omega. Qed. Theorem shru_rolm: @@ -2083,104 +2233,80 @@ Theorem shru_rolm: 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. + intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize; intros. + unfold rolm. apply same_bits_eq; intros. + rewrite bits_and; auto. rewrite !bits_shru; auto. rewrite bits_rol; auto. + destruct (zlt (i + unsigned n) zwordsize). + - generalize (unsigned_range n); intros. + rewrite bits_mone. rewrite andb_true_r. f_equal. + unfold sub. rewrite unsigned_repr. rewrite unsigned_repr_wordsize. + symmetry. apply Zmod_unique with (-1). ring. omega. + rewrite unsigned_repr_wordsize. generalize wordsize_max_unsigned. omega. + omega. + - rewrite andb_false_r; auto. 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 (i + - 0) with (i + 0) by omega. apply Zmod_small. omega. - apply repr_unsigned. + bit_solve. f_equal. rewrite unsigned_zero. rewrite Zminus_0_r. + apply Zmod_small; auto. Qed. Lemma bitwise_binop_rol: - forall f x y n, - bitwise_binop f (rol x n) (rol y n) = rol (bitwise_binop f x y) n. -Proof. - intros. unfold bitwise_binop, rol. - 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. + forall f f' x y n, + (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) -> + rol (f x y) n = f (rol x n) (rol y n). +Proof. + intros. apply same_bits_eq; intros. + rewrite H; auto. rewrite !bits_rol; auto. rewrite H; auto. + apply Z_mod_lt. apply wordsize_pos. Qed. Theorem rol_and: forall x y n, rol (and x y) n = and (rol x n) (rol y n). Proof. - intros. symmetry. unfold and. apply bitwise_binop_rol. + intros. apply bitwise_binop_rol with andb. exact bits_and. 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. + intros. apply bitwise_binop_rol with orb. exact bits_or. 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. + intros. apply bitwise_binop_rol with xorb. exact bits_xor. Qed. Theorem rol_rol: forall x n m, - Zdivide (Z_of_nat wordsize) modulus -> + Zdivide zwordsize modulus -> rol (rol x n) m = rol x (modu (add n m) iwordsize). Proof. - 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). + bit_solve. f_equal. apply eqmod_mod_eq. apply wordsize_pos. set (M := unsigned m); set (N := unsigned n). - assert (W > 0). unfold W; generalize wordsize_pos; omega. - assert (forall a, eqmod W a (unsigned (repr a))). + apply eqmod_trans with (i - M - N). + apply eqmod_sub. + apply eqmod_sym. apply eqmod_mod. apply wordsize_pos. + apply eqmod_refl. + replace (i - M - N) with (i - (M + N)) by omega. + apply eqmod_sub. + apply eqmod_refl. + apply eqmod_trans with (Zmod (unsigned n + unsigned m) zwordsize). + replace (M + N) with (N + M) by omega. apply eqmod_mod. apply wordsize_pos. + unfold modu, add. fold M; fold N. rewrite unsigned_repr_wordsize. + assert (forall a, eqmod zwordsize a (unsigned (repr a))). intros. eapply eqmod_divides. apply eqm_unsigned_repr. assumption. - apply eqmod_mod_eq. auto. - replace (unsigned iwordsize) with W. - 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 (i - M - N) with (i - (N + M)). - apply eqmod_sub. apply eqmod_refl. apply eqmod_mod. auto. - omega. - apply eqmod_sub. apply eqmod_refl. - eapply eqmod_trans; [idtac|apply H2]. - eapply eqmod_trans; [idtac|apply eqmod_mod]. - apply eqmod_sym. eapply eqmod_trans; [idtac|apply eqmod_mod]. - apply eqmod_sym. apply H2. auto. auto. - symmetry. unfold W. apply unsigned_repr_wordsize. - apply Z_mod_lt. generalize wordsize_pos; omega. + eapply eqmod_trans. 2: apply H1. + apply eqmod_refl2. apply eqmod_mod_eq. apply wordsize_pos. auto. + apply Z_mod_lt. apply wordsize_pos. Qed. Theorem rolm_zero: @@ -2192,7 +2318,7 @@ Qed. Theorem rolm_rolm: forall x n1 m1 n2 m2, - Zdivide (Z_of_nat wordsize) modulus -> + Zdivide zwordsize modulus -> rolm (rolm x n1 m1) n2 m2 = rolm x (modu (add n1 n2) iwordsize) (and (rol m1 n2) m2). @@ -2214,13 +2340,13 @@ Theorem ror_rol: ltu y iwordsize = true -> ror x y = rol x (sub iwordsize y). Proof. - intros. unfold ror, rol, sub. - generalize (ltu_inv _ _ H). + intros. + generalize (ltu_iwordsize_inv _ H); intros. + apply same_bits_eq; intros. + rewrite bits_ror; auto. rewrite bits_rol; auto. f_equal. + unfold sub. rewrite unsigned_repr. rewrite unsigned_repr_wordsize. + apply eqmod_mod_eq. apply wordsize_pos. exists 1. ring. rewrite unsigned_repr_wordsize. - 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. Qed. @@ -2232,30 +2358,19 @@ Theorem or_ror: ror x z = or (shl x y) (shru x z). Proof. intros. - generalize (ltu_inv _ _ H). - generalize (ltu_inv _ _ H0). - rewrite unsigned_repr_wordsize. - intros. - unfold or, bitwise_binop, shl, shru, ror. - set (ux := unsigned x). - 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. - assert (unsigned y = Z_of_nat wordsize - unsigned z). - rewrite H4. unfold sub. rewrite unsigned_repr_wordsize. apply unsigned_repr. - generalize wordsize_max_unsigned; omega. - destruct (zlt (i + unsigned z) (Z_of_nat wordsize)). - rewrite Zmod_small. - replace (bits_of_Z wordsize ux (i + - unsigned y)) with false. auto. - symmetry. apply bits_of_Z_below. omega. omega. - replace (bits_of_Z wordsize ux (i + unsigned z)) with false. rewrite orb_false_r. - decEq. - replace (i + unsigned z) with (i - unsigned y + 1 * Z_of_nat wordsize) by omega. - rewrite Z_mod_plus. apply Zmod_small. omega. generalize wordsize_pos; omega. - symmetry. apply bits_of_Z_above. auto. + generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. + unfold ror, or, shl, shru. apply same_bits_eq; intros. + rewrite !testbit_repr; auto. + rewrite !Z.lor_spec. rewrite orb_comm. f_equal; apply same_bits_eqm; auto. + - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal. + rewrite Zmod_small; auto. + assert (unsigned (add y z) = zwordsize). + rewrite H1. apply unsigned_repr_wordsize. + unfold add in H5. rewrite unsigned_repr in H5. + omega. + generalize two_wordsize_max_unsigned; omega. + - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal. + apply Zmod_small; auto. Qed. (** ** Properties of [Z_one_bits] and [is_power2]. *) @@ -2266,14 +2381,6 @@ Fixpoint powerserie (l: list Z): Z := | x :: xs => two_p x + powerserie xs end. -Lemma Z_bin_decomp_range: - forall x n, - 0 <= x < 2 * n -> 0 <= snd (Z_bin_decomp x) < n. -Proof. - intros. rewrite <- (Z_bin_comp_decomp x) in H. rewrite Z_bin_comp_eq in H. - destruct (fst (Z_bin_decomp x)); omega. -Qed. - Lemma Z_one_bits_powerserie: forall x, 0 <= x < modulus -> x = powerserie (Z_one_bits wordsize x 0). Proof. @@ -2281,42 +2388,46 @@ Proof. 0 <= i -> 0 <= x < two_power_nat n -> x * two_p i = powerserie (Z_one_bits n x i)). + { induction n; intros. simpl. rewrite two_power_nat_O in H0. - assert (x = 0). omega. subst x. omega. + assert (x = 0) by omega. subst x. omega. rewrite two_power_nat_S in H0. simpl Z_one_bits. - destruct (Z_bin_decomp x) as [b y] eqn:?. - rewrite (Z_bin_comp_decomp2 _ _ _ Heqp). - assert (EQ: y * two_p (i + 1) = powerserie (Z_one_bits n y (i + 1))). - apply IHn. omega. - replace y with (snd (Z_bin_decomp x)). apply Z_bin_decomp_range; auto. - rewrite Heqp; auto. + rewrite (Zdecomp x) in H0. rewrite Zshiftin_spec in H0. + assert (EQ: Z.div2 x * two_p (i + 1) = powerserie (Z_one_bits n (Z.div2 x) (i + 1))). + apply IHn. omega. + destruct (Z.odd x); omega. rewrite two_p_is_exp in EQ. change (two_p 1) with 2 in EQ. - rewrite Z_bin_comp_eq. - destruct b; simpl powerserie; rewrite <- EQ; ring. + rewrite (Zdecomp x) at 1. rewrite Zshiftin_spec. + destruct (Z.odd x); simpl powerserie; rewrite <- EQ; ring. omega. omega. + } intros. rewrite <- H. change (two_p 0) with 1. omega. omega. exact H0. Qed. Lemma Z_one_bits_range: - forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < Z_of_nat wordsize. + forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < zwordsize. Proof. assert (forall n x i j, In j (Z_one_bits n x i) -> i <= j < i + Z_of_nat n). + { induction n; simpl In. - intros; elim H. - intros x i j. destruct (Z_bin_decomp x). case b. - rewrite inj_S. simpl. intros [A|B]. subst j. omega. - generalize (IHn _ _ _ B). omega. - intros B. rewrite inj_S. generalize (IHn _ _ _ B). omega. - intros. generalize (H wordsize x 0 i H0). omega. + tauto. + intros x i j. rewrite inj_S. + assert (In j (Z_one_bits n (Z.div2 x) (i + 1)) -> i <= j < i + Z.succ (Z.of_nat n)). + intros. exploit IHn; eauto. omega. + destruct (Z.odd x); simpl. + intros [A|B]. subst j. omega. auto. + auto. + } + intros. generalize (H wordsize x 0 i H0). fold zwordsize; omega. Qed. Lemma is_power2_rng: forall n logn, is_power2 n = Some logn -> - 0 <= unsigned logn < Z_of_nat wordsize. + 0 <= unsigned logn < zwordsize. Proof. intros n logn. unfold is_power2. generalize (Z_one_bits_range (unsigned n)). @@ -2324,7 +2435,7 @@ Proof. intros; discriminate. destruct l. intros. injection H0; intro; subst logn; clear H0. - assert (0 <= z < Z_of_nat wordsize). + assert (0 <= z < zwordsize). apply H. auto with coqlib. rewrite unsigned_repr. auto. generalize wordsize_max_unsigned; omega. intros; discriminate. @@ -2335,9 +2446,7 @@ Theorem is_power2_range: is_power2 n = Some logn -> ltu logn iwordsize = true. Proof. intros. unfold ltu. rewrite unsigned_repr_wordsize. - generalize (is_power2_rng _ _ H). - case (zlt (unsigned logn) (Z_of_nat wordsize)); intros. - auto. omegaContradiction. + apply zlt_true. generalize (is_power2_rng _ _ H). tauto. Qed. Lemma is_power2_correct: @@ -2361,12 +2470,13 @@ Qed. Remark two_p_range: forall n, - 0 <= n < Z_of_nat wordsize -> + 0 <= n < zwordsize -> 0 <= two_p n <= max_unsigned. Proof. intros. split. assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega. - generalize (two_p_monotone_strict _ _ H). rewrite <- two_power_nat_two_p. + generalize (two_p_monotone_strict _ _ H). + unfold zwordsize; rewrite <- two_power_nat_two_p. unfold max_unsigned, modulus. omega. Qed. @@ -2385,16 +2495,15 @@ Proof. 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_bin_comp false (two_p (x-1))). - rewrite Z_bin_decomp_comp. - replace (i + x) with ((i + 1) + (x - 1)) by omega. - apply IHn. omega. - rewrite Z_bin_comp_eq. rewrite <- two_p_S. - rewrite Zplus_0_r. decEq; omega. omega. + assert (Z.odd (two_p x) = false /\ Z.div2 (two_p x) = two_p (x-1)). + apply Zshiftin_inj. rewrite <- Zdecomp. rewrite !Zshiftin_spec. + rewrite <- two_p_S. rewrite Zplus_0_r. f_equal; omega. omega. + destruct H1 as [A B]; rewrite A; rewrite B. + rewrite IHn. f_equal; omega. omega. Qed. Lemma is_power2_two_p: - forall n, 0 <= n < Z_of_nat wordsize -> + forall n, 0 <= n < zwordsize -> is_power2 (repr (two_p n)) = Some (repr n). Proof. intros. unfold is_power2. rewrite unsigned_repr. @@ -2406,34 +2515,26 @@ Qed. (** 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). +Lemma Zshiftl_mul_two_p: + forall x n, 0 <= n -> Z.shiftl x n = x * two_p n. 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. + intros. destruct n; simpl. + - omega. + - pattern p. apply Pos.peano_ind. + + change (two_power_pos 1) with 2. simpl. ring. + + intros. rewrite Pos.iter_succ. rewrite H0. + rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp. + change (two_power_pos 1) with 2. ring. + - compute in H. congruence. 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. + intros. unfold shl, mul. apply eqm_samerepr. + rewrite Zshiftl_mul_two_p. auto with ints. + generalize (unsigned_range y); omega. Qed. Theorem shl_mul: @@ -2442,7 +2543,9 @@ Theorem shl_mul: Proof. intros. assert (shl one y = repr (two_p (unsigned y))). - rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto. + { + rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto. + } rewrite H. apply shl_mul_two_p. Qed. @@ -2458,46 +2561,45 @@ Qed. Theorem shifted_or_is_add: forall x y n, - 0 <= n < Z_of_nat wordsize -> + 0 <= n < zwordsize -> unsigned y < two_p n -> or (shl x (repr n)) y = repr(unsigned x * two_p n + unsigned y). Proof. intros. rewrite <- add_is_or. - rewrite shl_mul_two_p. rewrite unsigned_repr. - unfold add. apply eqm_samerepr. unfold mul. auto with ints. - generalize wordsize_max_unsigned; omega. - unfold and, shl, bitwise_binop. unfold zero. decEq. apply Z_of_bits_false. intros. - rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits_gen. - rewrite unsigned_repr. apply andb_false_iff. - destruct (zlt j n). - left. apply bits_of_Z_below. omega. - right. apply bits_of_Z_greater. - split. generalize (unsigned_range y); omega. - assert (two_p n <= two_p j). apply two_p_monotone. omega. omega. - generalize wordsize_max_unsigned; omega. - omega. + - unfold add. apply eqm_samerepr. apply eqm_add; auto with ints. + rewrite shl_mul_two_p. unfold mul. apply eqm_unsigned_repr_l. + apply eqm_mult; auto with ints. apply eqm_unsigned_repr_l. + apply eqm_refl2. rewrite unsigned_repr. auto. + generalize wordsize_max_unsigned; omega. + - bit_solve. + rewrite unsigned_repr. + destruct (zlt i n). + + auto. + + replace (testbit y i) with false. apply andb_false_r. + symmetry. unfold testbit. + assert (EQ: Z.of_nat (Z.to_nat n) = n) by (apply Z2Nat.id; omega). + apply Ztestbit_above with (Z.to_nat n). + rewrite <- EQ in H0. rewrite <- two_power_nat_two_p in H0. + generalize (unsigned_range y); omega. + rewrite EQ; auto. + + generalize wordsize_max_unsigned; omega. Qed. (** Unsigned right shifts and unsigned divisions by powers of 2. *) -Lemma Z_of_bits_shift_right: - forall m f, - m >= 0 -> - (forall i, i >= Z_of_nat wordsize -> f i = false) -> - exists k, - Z_of_bits wordsize f 0 = k + two_p m * Z_of_bits wordsize f m /\ 0 <= k < two_p m. +Lemma Zshiftr_div_two_p: + forall x n, 0 <= n -> Z.shiftr x n = x / two_p n. 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 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. + intros. destruct n; unfold Z.shiftr; simpl. + - rewrite Zdiv_1_r. auto. + - pattern p. apply Pos.peano_ind. + + change (two_power_pos 1) with 2. simpl. apply Zdiv2_div. + + intros. rewrite Pos.iter_succ. rewrite H0. + rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp. + change (two_power_pos 1) with 2. + rewrite Zdiv2_div. rewrite Zmult_comm. apply Zdiv_Zdiv. + rewrite two_power_pos_nat. apply two_power_nat_pos. omega. + - compute in H. congruence. Qed. Lemma shru_div_two_p: @@ -2505,15 +2607,8 @@ Lemma shru_div_two_p: shru x y = repr (unsigned x / two_p (unsigned y)). Proof. intros. unfold shru. - set (x' := unsigned x). set (y' := unsigned y). - 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. + rewrite Zshiftr_div_two_p. auto. + generalize (unsigned_range y); omega. Qed. Theorem divu_pow2: @@ -2527,103 +2622,13 @@ Qed. (** 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. - 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. - generalize (Z_bin_comp_decomp x). destruct (Z_bin_decomp x) as [b y]; simpl. - intros; subst x. rewrite Z_bin_comp_eq 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_bin_comp_decomp x). destruct (Z_bin_decomp x) as [b y]; simpl. - intros; subst x. rewrite Z_bin_comp_eq in *. - rewrite zeq_false. - replace (Zsucc (Z_of_nat n) - 1) with (Z_of_nat n). rewrite IHn. - subst sn. rewrite two_power_nat_S. - destruct (zlt y (two_power_nat n)). - rewrite zlt_true. auto. destruct b; omega. - rewrite zlt_false. auto. destruct b; omega. - destruct b; omega. - omega. omega. -Qed. - -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. - 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. - 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. + rewrite Zshiftr_div_two_p. auto. + generalize (unsigned_range y); omega. Qed. Theorem divs_pow2: @@ -2639,29 +2644,41 @@ 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. +Lemma Ztestbit_mod_two_p: + forall n x i, + 0 <= n -> 0 <= i -> + Z.testbit (x mod (two_p n)) i = if zlt i n then Z.testbit x i else false. +Proof. + intros n0 x i N0POS. revert x i; pattern n0; apply natlike_ind; auto. + - intros. change (two_p 0) with 1. rewrite Zmod_1_r. rewrite Z.testbit_0_l. + rewrite zlt_false; auto. omega. + - intros. rewrite two_p_S; auto. + replace (x0 mod (2 * two_p x)) + with (Zshiftin (Z.odd x0) (Z.div2 x0 mod two_p x)). + rewrite Ztestbit_shiftin; auto. rewrite (Ztestbit_eq i x0); auto. destruct (zeq i 0). + + rewrite zlt_true; auto. omega. + + rewrite H0. destruct (zlt (Z.pred i) x). + * rewrite zlt_true; auto. omega. + * rewrite zlt_false; auto. omega. + * omega. + + rewrite (Zdecomp x0) at 3. set (x1 := Z.div2 x0). symmetry. + apply Zmod_unique with (x1 / two_p x). + rewrite !Zshiftin_spec. rewrite Zplus_assoc. f_equal. + transitivity (2 * (two_p x * (x1 / two_p x) + x1 mod two_p x)). + f_equal. apply Z_div_mod_eq. apply two_p_gt_ZERO; auto. + ring. + rewrite Zshiftin_spec. exploit (Z_mod_lt x1 (two_p x)). apply two_p_gt_ZERO; auto. + destruct (Z.odd x0); omega. +Qed. + +Corollary Ztestbit_two_p_m1: + forall n i, 0 <= n -> 0 <= i -> + Z.testbit (two_p n - 1) i = if zlt i n then true else false. +Proof. + intros. replace (two_p n - 1) with ((-1) mod (two_p n)). + rewrite Ztestbit_mod_two_p; auto. destruct (zlt i n); auto. apply Ztestbit_m1; auto. + apply Zmod_unique with (-1). ring. + exploit (two_p_gt_ZERO n). auto. omega. Qed. Theorem modu_and: @@ -2671,55 +2688,46 @@ Theorem modu_and: 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. + apply same_bits_eq; intros. + rewrite bits_and; auto. + unfold sub. rewrite testbit_repr; auto. + rewrite H0. rewrite unsigned_one. + unfold modu. rewrite testbit_repr; auto. rewrite H0. + rewrite Ztestbit_mod_two_p. rewrite Ztestbit_two_p_m1. + destruct (zlt i (unsigned logn)). + rewrite andb_true_r; auto. + rewrite andb_false_r; auto. + tauto. tauto. tauto. tauto. Qed. (** ** Properties of [shrx] (signed division by a power of 2) *) -Lemma Zdiv_round_Zdiv: +Lemma Zquot_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. + Z.quot x y = if zlt x 0 then (x + y - 1) / y else x / y. +Proof. + intros. destruct (zlt x 0). + - symmetry. apply Zquot_unique_full with ((x + y - 1) mod y - (y - 1)). + + red. right; split. omega. + exploit (Z_mod_lt (x + y - 1) y); auto. + rewrite Z.abs_eq. omega. omega. + + transitivity ((y * ((x + y - 1) / y) + (x + y - 1) mod y) - (y-1)). + rewrite <- Z_div_mod_eq. ring. auto. ring. + - apply Zquot_Zdiv_pos; omega. Qed. Theorem shrx_shr: forall x y, - ltu y (repr (Z_of_nat wordsize - 1)) = true -> + ltu y (repr (zwordsize - 1)) = true -> shrx x y = shr (if lt x zero then add x (sub (shl one y) one) else x) y. Proof. - intros. rewrite shr_div_two_p. unfold shrx. unfold divs. - exploit ltu_inv; eauto. rewrite unsigned_repr. - set (uy := unsigned y). intro RANGE. + intros. + set (uy := unsigned y). + assert (0 <= uy < zwordsize - 1). + exploit ltu_inv; eauto. rewrite unsigned_repr. auto. + generalize wordsize_pos wordsize_max_unsigned; omega. + rewrite shr_div_two_p. unfold shrx. unfold divs. assert (shl one y = repr (two_p uy)). transitivity (mul one (repr (two_p uy))). symmetry. apply mul_pow2. replace y with (repr uy). @@ -2732,24 +2740,22 @@ Proof. assert (two_p uy < modulus). rewrite modulus_power. apply two_p_monotone_strict. omega. assert (unsigned (shl one y) = two_p uy). - rewrite H0. apply unsigned_repr. unfold max_unsigned. omega. + rewrite H1. apply unsigned_repr. unfold max_unsigned. omega. assert (signed (shl one y) = two_p uy). - rewrite H0. apply signed_repr. + rewrite H1. apply signed_repr. unfold max_signed. generalize min_signed_neg. omega. - rewrite H5. - rewrite Zdiv_round_Zdiv; auto. + rewrite H6. + rewrite Zquot_Zdiv; auto. unfold lt. rewrite signed_zero. destruct (zlt (signed x) 0); auto. rewrite add_signed. assert (signed (sub (shl one y) one) = two_p uy - 1). - unfold sub. rewrite H4. rewrite unsigned_one. + unfold sub. rewrite H5. rewrite unsigned_one. apply signed_repr. generalize min_signed_neg. unfold max_signed. omega. - rewrite H6. rewrite signed_repr. decEq. decEq. omega. + rewrite H7. rewrite signed_repr. f_equal. f_equal. 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. + assert (two_p uy - 1 <= max_signed). unfold max_signed. omega. omega. Qed. Lemma Zdiv_shift: @@ -2765,7 +2771,7 @@ Qed. Theorem shrx_carry: forall x y, - ltu y (repr (Z_of_nat wordsize - 1)) = true -> + ltu y (repr (zwordsize - 1)) = true -> shrx x y = add (shr x y) (shr_carry x y). Proof. intros. rewrite shrx_shr; auto. unfold shr_carry. @@ -2773,7 +2779,7 @@ Proof. destruct (zlt sx 0); simpl. 2: rewrite add_zero; auto. set (uy := unsigned y). - assert (0 <= uy < Z_of_nat wordsize - 1). + assert (0 <= uy < zwordsize - 1). exploit ltu_inv; eauto. rewrite unsigned_repr. auto. generalize wordsize_pos wordsize_max_unsigned; omega. assert (shl one y = repr (two_p uy)). @@ -2803,8 +2809,8 @@ Proof. apply eqmod_mod_eq; auto. apply eqmod_divides with modulus. fold eqm. unfold sx. apply eqm_sym. apply eqm_signed_unsigned. unfold modulus. rewrite two_power_nat_two_p. - exists (two_p (Z_of_nat wordsize - uy)). rewrite <- two_p_is_exp. - decEq. omega. omega. omega. + exists (two_p (zwordsize - uy)). rewrite <- two_p_is_exp. + f_equal. fold zwordsize; omega. omega. omega. rewrite H8. rewrite Zdiv_shift; auto. unfold add. apply eqm_samerepr. apply eqm_add. apply eqm_unsigned_repr. @@ -2833,16 +2839,12 @@ Lemma and_positive: forall x y, signed y >= 0 -> signed (and x y) >= 0. Proof. intros. - assert (unsigned y < half_modulus). rewrite signed_positive in H. unfold max_signed in H; omega. - generalize (sign_bit_of_Z y). rewrite zlt_true; auto. intros A. - generalize (sign_bit_of_Z (and x y)). - unfold and at 1. unfold bitwise_binop at 1. - set (fx := bits_of_Z wordsize (unsigned x)). - set (fy := bits_of_Z wordsize (unsigned y)). - rewrite unsigned_repr; auto with ints. - rewrite bits_of_Z_of_bits. unfold fy. rewrite A. rewrite andb_false_r. - destruct (zlt (unsigned (and x y)) half_modulus); intros. - rewrite signed_positive. unfold max_signed; omega. + assert (unsigned y < half_modulus). rewrite signed_positive in H. unfold max_signed in H; omega. + generalize (sign_bit_of_unsigned y). rewrite zlt_true; auto. intros A. + generalize (sign_bit_of_unsigned (and x y)). rewrite bits_and. rewrite A. + rewrite andb_false_r. unfold signed. + destruct (zlt (unsigned (and x y)) half_modulus). + intros. generalize (unsigned_range (and x y)); omega. congruence. generalize wordsize_pos; omega. Qed. @@ -2857,292 +2859,364 @@ Qed. (** ** Properties of integer zero extension and sign extension. *) -Section EXTENSIONS. +(* +Lemma Ziter_ind: + forall (A: Type) (f: A -> A) (P: Z -> A -> Prop) n x, + (n <= 0 -> P n x) -> + (forall n x, 0 <= n -> P n x -> P (Z.succ n) (f x)) -> + P n (Z.iter n f x). +Proof. + intros until x; intros BASE SUCC. intros. + unfold Z.iter. destruct n. + - apply BASE. omega. + - induction p using Pos.peano_ind. + + simpl Pos.iter. apply (SUCC 0). omega. apply BASE. omega. + + rewrite Pos2Z.inj_succ. rewrite Pos.iter_succ. + apply SUCC. compute; intuition congruence. auto. + - apply BASE. compute; intuition congruence. +Qed. +*) -Variable n: Z. -Hypothesis RANGE: 0 < n < Z_of_nat wordsize. +Lemma Ziter_base: + forall (A: Type) n (f: A -> A) x, n <= 0 -> Z.iter n f x = x. +Proof. + intros. unfold Z.iter. destruct n; auto. compute in H. elim H; auto. +Qed. -Remark two_p_n_pos: - two_p n > 0. -Proof. apply two_p_gt_ZERO. omega. Qed. +Lemma Ziter_succ: + forall (A: Type) n (f: A -> A) x, + 0 <= n -> Z.iter (Z.succ n) f x = f (Z.iter n f x). +Proof. + intros. destruct n; simpl. + - auto. + - rewrite Pos.add_1_r. apply Pos.iter_succ. + - compute in H. elim H; auto. +Qed. -Remark two_p_n_range: - 0 <= two_p n <= max_unsigned. -Proof. apply two_p_range. omega. Qed. +Lemma Znatlike_ind: + forall (P: Z -> Prop), + (forall n, n <= 0 -> P n) -> + (forall n, 0 <= n -> P n -> P (Z.succ n)) -> + forall n, P n. +Proof. + intros. destruct (zle 0 n). + apply natlike_ind; auto. apply H; omega. + apply H. omega. +Qed. -Remark two_p_n_range': - two_p n <= max_signed + 1. +Lemma Zzero_ext_spec: + forall n x i, 0 <= i -> + Z.testbit (Zzero_ext n x) i = if zlt i n then Z.testbit x i else false. +Proof. + unfold Zzero_ext. induction n using Znatlike_ind. + - intros. rewrite Ziter_base; auto. + rewrite zlt_false. rewrite Ztestbit_0; auto. omega. + - intros. rewrite Ziter_succ; auto. + rewrite Ztestbit_shiftin; auto. + rewrite (Ztestbit_eq i x); auto. + destruct (zeq i 0). + + subst i. rewrite zlt_true; auto. omega. + + rewrite IHn. destruct (zlt (Z.pred i) n). + rewrite zlt_true; auto. omega. + rewrite zlt_false; auto. omega. + omega. +Qed. + +Lemma bits_zero_ext: + forall n x i, 0 <= i -> + testbit (zero_ext n x) i = if zlt i n then testbit x i else false. +Proof. + intros. unfold zero_ext. destruct (zlt i zwordsize). + rewrite testbit_repr; auto. rewrite Zzero_ext_spec. auto. auto. + rewrite !bits_above; auto. destruct (zlt i n); auto. +Qed. + +Lemma Zsign_ext_spec: + forall n x i, 0 <= i -> 0 < n -> + Z.testbit (Zsign_ext n x) i = Z.testbit x (if zlt i n then i else n - 1). +Proof. + intros n0 x i I0 N0. + revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1). + - unfold Zsign_ext. intros. + destruct (zeq x 1). + + subst x; simpl. + replace (if zlt i 1 then i else 0) with 0. + rewrite Ztestbit_base. + destruct (Z.odd x0). + apply Ztestbit_m1; auto. + apply Ztestbit_0. + destruct (zlt i 1); omega. + + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)). + rewrite Ziter_succ. rewrite Ztestbit_shiftin. + destruct (zeq i 0). + * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega. + * rewrite H. unfold x1. destruct (zlt (Z.pred i) (Z.pred x)). + rewrite zlt_true. rewrite (Ztestbit_eq i x0); auto. rewrite zeq_false; auto. omega. + rewrite zlt_false. rewrite (Ztestbit_eq (x - 1) x0). rewrite zeq_false; auto. + omega. omega. omega. unfold x1; omega. omega. + * omega. + * unfold x1; omega. + * omega. + - omega. +Qed. + +Lemma bits_sign_ext: + forall n x i, 0 <= i < zwordsize -> 0 < n -> + testbit (sign_ext n x) i = testbit x (if zlt i n then i else n - 1). Proof. - unfold max_signed. rewrite half_modulus_power. - assert (two_p n <= two_p (Z_of_nat wordsize - 1)). - apply two_p_monotone. omega. - omega. + intros. unfold sign_ext. + rewrite testbit_repr; auto. rewrite Zsign_ext_spec. destruct (zlt i n); auto. + omega. auto. Qed. -Remark unsigned_repr_two_p: - unsigned (repr (two_p n)) = two_p n. +Hint Rewrite bits_zero_ext bits_sign_ext: ints. + +Theorem zero_ext_above: + forall n x, n >= zwordsize -> zero_ext n x = x. Proof. - apply unsigned_repr. apply two_p_n_range. + intros. apply same_bits_eq; intros. + rewrite bits_zero_ext. apply zlt_true. omega. omega. Qed. -Remark eqm_eqmod_two_p: - forall a b, eqm a b -> eqmod (two_p n) a b. +Theorem sign_ext_above: + forall n x, n >= zwordsize -> sign_ext n x = x. Proof. - 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. + intros. apply same_bits_eq; intros. + unfold sign_ext; rewrite testbit_repr; auto. + rewrite Zsign_ext_spec. rewrite zlt_true. auto. omega. omega. omega. Qed. Theorem zero_ext_and: - forall x, zero_ext n x = and x (repr (two_p n - 1)). + forall n x, 0 <= n -> zero_ext n x = and x (repr (two_p n - 1)). Proof. - 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. + bit_solve. rewrite testbit_repr; auto. rewrite Ztestbit_two_p_m1; intuition. + destruct (zlt i n). + rewrite andb_true_r; auto. + rewrite andb_false_r; auto. + tauto. Qed. Theorem zero_ext_mod: - forall x, unsigned (zero_ext n x) = Zmod (unsigned x) (two_p n). + forall n x, 0 <= n < zwordsize -> + unsigned (zero_ext n x) = Zmod (unsigned x) (two_p n). +Proof. + intros. apply equal_same_bits. intros. + rewrite Ztestbit_mod_two_p; auto. + fold (testbit (zero_ext n x) i). + destruct (zlt i zwordsize). + rewrite bits_zero_ext; auto. + rewrite bits_above. rewrite zlt_false; auto. omega. omega. + omega. +Qed. + +Theorem zero_ext_widen: + forall x n n', 0 <= n <= n' -> + zero_ext n' (zero_ext n x) = zero_ext n x. Proof. - 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. + bit_solve. destruct (zlt i n). + apply zlt_true. omega. + destruct (zlt i n'); auto. + tauto. tauto. +Qed. + +Theorem sign_ext_widen: + forall x n n', 0 < n <= n' -> + sign_ext n' (sign_ext n x) = sign_ext n x. +Proof. + intros. destruct (zlt n' zwordsize). + bit_solve. destruct (zlt i n'). + auto. + rewrite (zlt_false _ i n). + destruct (zlt (n' - 1) n); f_equal; omega. + omega. omega. + destruct (zlt i n'); omega. + omega. omega. + apply sign_ext_above; auto. +Qed. + +Theorem sign_zero_ext_widen: + forall x n n', 0 <= n < n' -> + sign_ext n' (zero_ext n x) = zero_ext n x. +Proof. + intros. destruct (zlt n' zwordsize). + bit_solve. + destruct (zlt i n'). + auto. + rewrite !zlt_false. auto. omega. omega. omega. + destruct (zlt i n'); omega. + omega. + apply sign_ext_above; auto. +Qed. + +Theorem zero_ext_narrow: + forall x n n', 0 <= n <= n' -> + zero_ext n (zero_ext n' x) = zero_ext n x. +Proof. + bit_solve. destruct (zlt i n). + apply zlt_true. omega. + auto. + omega. omega. omega. +Qed. + +Theorem zero_sign_ext_narrow: + forall x n n', 0 < n <= n' -> + zero_ext n (sign_ext n' x) = zero_ext n x. +Proof. + intros. destruct (zlt n' zwordsize). + bit_solve. + destruct (zlt i n); auto. + rewrite zlt_true; auto. omega. + omega. omega. omega. + rewrite sign_ext_above; auto. Qed. Theorem zero_ext_idem: - forall x, zero_ext n (zero_ext n x) = zero_ext n x. + forall n x, 0 <= n -> 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. + intros. apply zero_ext_widen. omega. Qed. Theorem sign_ext_idem: - forall x, sign_ext n (sign_ext n x) = sign_ext n x. + forall n x, 0 < n -> sign_ext n (sign_ext n x) = sign_ext n x. Proof. - 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. + intros. apply sign_ext_widen. omega. Qed. Theorem sign_ext_zero_ext: - forall x, sign_ext n (zero_ext n x) = sign_ext n x. + forall n x, 0 < n -> sign_ext n (zero_ext n x) = sign_ext n x. Proof. - 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. + intros. destruct (zlt n zwordsize). + bit_solve. + destruct (zlt i n). + rewrite zlt_true; auto. + rewrite zlt_true; auto. omega. + destruct (zlt i n); omega. + rewrite zero_ext_above; auto. Qed. Theorem zero_ext_sign_ext: - forall x, zero_ext n (sign_ext n x) = zero_ext n x. + forall n x, 0 < n -> zero_ext n (sign_ext n x) = zero_ext n x. Proof. - 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. + intros. apply zero_sign_ext_narrow. omega. Qed. Theorem sign_ext_equal_if_zero_equal: - forall x y, + forall n x y, 0 < n -> 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. + intros. rewrite <- (sign_ext_zero_ext n x H). + rewrite <- (sign_ext_zero_ext n y H). congruence. Qed. Theorem zero_ext_shru_shl: - forall x, - let y := repr (Z_of_nat wordsize - n) in + forall n x, + 0 < n < zwordsize -> + let y := repr (zwordsize - n) in zero_ext n x = shru (shl x y) y. Proof. intros. - assert (unsigned y = Z_of_nat wordsize - n). + assert (unsigned y = zwordsize - 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. + apply same_bits_eq; intros. + rewrite bits_zero_ext. + rewrite bits_shru; auto. + destruct (zlt i n). + rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega. + omega. omega. omega. + rewrite zlt_false. auto. omega. + omega. Qed. Theorem sign_ext_shr_shl: - forall x, - let y := repr (Z_of_nat wordsize - n) in + forall n x, + 0 < n < zwordsize -> + let y := repr (zwordsize - n) in sign_ext n x = shr (shl x y) y. Proof. intros. - assert (unsigned y = Z_of_nat wordsize - n). + assert (unsigned y = zwordsize - n). unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. 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. + apply same_bits_eq; intros. + rewrite bits_sign_ext. + rewrite bits_shr; auto. + destruct (zlt i n). + rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega. + omega. omega. omega. + rewrite zlt_false. rewrite bits_shl. rewrite zlt_false. f_equal. omega. + omega. omega. 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. + forall n x, 0 <= n < zwordsize -> 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. + intros. rewrite zero_ext_mod; auto. 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). + forall n x, 0 <= n < zwordsize -> eqmod (two_p n) (unsigned (zero_ext n x)) (unsigned x). Proof. - intros. rewrite zero_ext_mod. apply eqmod_sym. apply eqmod_mod. + intros. rewrite zero_ext_mod; auto. apply eqmod_sym. apply eqmod_mod. apply two_p_gt_ZERO. omega. Qed. (** [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 (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. + forall n x, 0 < n < zwordsize -> -two_p (n-1) <= signed (sign_ext n x) < two_p (n-1). +Proof. + intros. rewrite sign_ext_shr_shl; auto. + set (X := shl x (repr (zwordsize - n))). + assert (two_p (n - 1) > 0) by (apply two_p_gt_ZERO; omega). + assert (unsigned (repr (zwordsize - n)) = zwordsize - n). + apply unsigned_repr. + split. omega. generalize wordsize_max_unsigned; omega. + rewrite shr_div_two_p. + rewrite signed_repr. + rewrite H1. + apply Zdiv_interval_1. + omega. omega. apply two_p_gt_ZERO; omega. + replace (- two_p (n - 1) * two_p (zwordsize - n)) + with (- (two_p (n - 1) * two_p (zwordsize - n))) by ring. + rewrite <- two_p_is_exp. + replace (n - 1 + (zwordsize - n)) with (zwordsize - 1) by omega. + rewrite <- half_modulus_power. + generalize (signed_range X). unfold min_signed, max_signed. omega. omega. omega. - rewrite modulus_power. decEq. omega. - apply two_p_gt_ZERO; omega. + apply Zdiv_interval_2. apply signed_range. + generalize min_signed_neg; omega. + generalize max_signed_pos; omega. + rewrite H1. apply two_p_gt_ZERO. omega. Qed. Lemma eqmod_sign_ext': - forall x, eqmod (two_p n) (unsigned (sign_ext n x)) (unsigned x). + forall n x, 0 < n < zwordsize -> + 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. - -Theorem zero_ext_widen: - forall x n n', - 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. 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: - forall x n n', - 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. 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: - forall x n n', - 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. 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. - -Theorem zero_ext_narrow: - forall x n n', - 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. 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); auto. - rewrite bits_of_Z_of_bits; auto. apply zlt_true. omega. + intros. + set (N := Z.to_nat n). + assert (Z.of_nat N = n) by (apply Z2Nat.id; omega). + rewrite <- H0. rewrite <- two_power_nat_two_p. + apply eqmod_same_bits; intros. + rewrite H0 in H1. rewrite H0. + fold (testbit (sign_ext n x) i). rewrite bits_sign_ext. + rewrite zlt_true. auto. omega. omega. omega. Qed. -Theorem zero_sign_ext_narrow: - forall x n n', - 0 < n < Z_of_nat wordsize -> n <= n' < Z_of_nat wordsize -> - zero_ext n (sign_ext n' x) = zero_ext n x. +Lemma eqmod_sign_ext: + forall n x, 0 < n < zwordsize -> + eqmod (two_p n) (signed (sign_ext n x)) (unsigned x). Proof. - 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. apply zlt_true. omega. + intros. apply eqmod_trans with (unsigned (sign_ext n x)). + apply eqmod_divides with modulus. apply eqm_signed_unsigned. + exists (two_p (zwordsize - n)). + unfold modulus. rewrite two_power_nat_two_p. fold zwordsize. + rewrite <- two_p_is_exp. f_equal. omega. omega. omega. + apply eqmod_sign_ext'; auto. Qed. (** ** Properties of [one_bits] (decomposition in sum of powers of two) *) @@ -3150,11 +3224,11 @@ Qed. Theorem one_bits_range: forall x i, In i (one_bits x) -> ltu i iwordsize = true. Proof. - assert (A: forall p, 0 <= p < Z_of_nat wordsize -> ltu (repr p) iwordsize = true). + assert (A: forall p, 0 <= p < zwordsize -> ltu (repr p) iwordsize = true). intros. unfold ltu, iwordsize. apply zlt_true. repeat rewrite unsigned_repr. tauto. - generalize wordsize_max_unsigned. omega. - generalize wordsize_max_unsigned. omega. + generalize wordsize_max_unsigned; omega. + generalize wordsize_max_unsigned; omega. intros. unfold one_bits in H. destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]]. subst i. apply A. apply Z_one_bits_range with (unsigned x); auto. @@ -3291,23 +3365,27 @@ Qed. Theorem shru_lt_zero: forall x, - shru x (repr (Z_of_nat wordsize - 1)) = if lt x zero then one else zero. + shru x (repr (zwordsize - 1)) = if lt x zero then one else zero. Proof. - intros. rewrite shru_div_two_p. - replace (two_p (unsigned (repr (Z_of_nat wordsize - 1)))) - with half_modulus. - generalize (unsigned_range x); intro. + intros. apply same_bits_eq; intros. + rewrite bits_shru; auto. + rewrite unsigned_repr. + destruct (zeq i 0). + subst i. rewrite Zplus_0_l. rewrite zlt_true. + rewrite sign_bit_of_unsigned. unfold lt. rewrite signed_zero. unfold signed. destruct (zlt (unsigned x) half_modulus). + rewrite zlt_false. auto. generalize (unsigned_range x); omega. + rewrite zlt_true. unfold one; rewrite testbit_repr; auto. + generalize (unsigned_range x); omega. + omega. rewrite zlt_false. - replace (unsigned x / half_modulus) with 0. reflexivity. - symmetry. apply Zdiv_unique with (unsigned x). ring. omega. omega. - rewrite zlt_true. - replace (unsigned x / half_modulus) with 1. reflexivity. - symmetry. apply Zdiv_unique with (unsigned x - half_modulus). ring. - rewrite half_modulus_modulus in H. omega. omega. - rewrite unsigned_repr. apply half_modulus_power. - generalize wordsize_pos wordsize_max_unsigned; omega. + unfold testbit. rewrite Ztestbit_eq. rewrite zeq_false. + destruct (lt x zero). + rewrite unsigned_one. simpl Z.div2. rewrite Z.testbit_0_l; auto. + rewrite unsigned_zero. simpl Z.div2. rewrite Z.testbit_0_l; auto. + auto. omega. omega. + generalize wordsize_max_unsigned; omega. Qed. Theorem ltu_range_test: @@ -3347,6 +3425,236 @@ Proof. intros [C|C] [D|D]; omega. Qed. +(** Size of integers, in bits. *) + +Definition Zsize (x: Z) : Z := + match x with + | Zpos p => Zpos (Pos.size p) + | _ => 0 + end. + +Definition size (x: int) : Z := Zsize (unsigned x). + +Remark Zsize_pos: forall x, 0 <= Zsize x. +Proof. + destruct x; simpl. omega. compute; intuition congruence. omega. +Qed. + +Remark Zsize_pos': forall x, 0 < x -> 0 < Zsize x. +Proof. + destruct x; simpl; intros; try discriminate. compute; auto. +Qed. + +Lemma Zsize_shiftin: + forall b x, 0 < x -> Zsize (Zshiftin b x) = Zsucc (Zsize x). +Proof. + intros. destruct x; compute in H; try discriminate. + destruct b. + change (Zshiftin true (Zpos p)) with (Zpos (p~1)). + simpl. f_equal. rewrite Pos.add_1_r; auto. + change (Zshiftin false (Zpos p)) with (Zpos (p~0)). + simpl. f_equal. rewrite Pos.add_1_r; auto. +Qed. + +Lemma Ztestbit_size_1: + forall x, 0 < x -> Z.testbit x (Zpred (Zsize x)) = true. +Proof. + intros x0 POS0; pattern x0; apply Zshiftin_pos_ind; auto. + intros. rewrite Zsize_shiftin; auto. + replace (Z.pred (Z.succ (Zsize x))) with (Z.succ (Z.pred (Zsize x))) by omega. + rewrite Ztestbit_shiftin_succ. auto. generalize (Zsize_pos' x H); omega. +Qed. + +Lemma Ztestbit_size_2: + forall x, 0 <= x -> forall i, i >= Zsize x -> Z.testbit x i = false. +Proof. + intros x0 POS0. destruct (zeq x0 0). + - subst x0; intros. apply Ztestbit_0. + - pattern x0; apply Zshiftin_pos_ind. + + simpl. intros. change 1 with (Zshiftin true 0). rewrite Ztestbit_shiftin. + rewrite zeq_false. apply Ztestbit_0. omega. omega. + + intros. rewrite Zsize_shiftin in H1; auto. + generalize (Zsize_pos' _ H); intros. + rewrite Ztestbit_shiftin. rewrite zeq_false. apply H0. omega. + omega. omega. + + omega. +Qed. + +Lemma Zsize_interval_1: + forall x, 0 <= x -> 0 <= x < two_p (Zsize x). +Proof. + intros. + assert (x = x mod (two_p (Zsize x))). + apply equal_same_bits; intros. + rewrite Ztestbit_mod_two_p; auto. + destruct (zlt i (Zsize x)). auto. apply Ztestbit_size_2; auto. + apply Zsize_pos; auto. + rewrite H0 at 1. rewrite H0 at 3. apply Z_mod_lt. apply two_p_gt_ZERO. apply Zsize_pos; auto. +Qed. + +Lemma Zsize_interval_2: + forall x n, 0 <= n -> 0 <= x < two_p n -> n >= Zsize x. +Proof. + intros. set (N := Z.to_nat n). + assert (Z.of_nat N = n) by (apply Z2Nat.id; auto). + rewrite <- H1 in H0. rewrite <- two_power_nat_two_p in H0. + destruct (zeq x 0). + subst x; simpl; omega. + destruct (zlt n (Zsize x)); auto. + exploit (Ztestbit_above N x (Zpred (Zsize x))). auto. omega. + rewrite Ztestbit_size_1. congruence. omega. +Qed. + +Lemma Zsize_monotone: + forall x y, 0 <= x <= y -> Zsize x <= Zsize y. +Proof. + intros. apply Zge_le. apply Zsize_interval_2. apply Zsize_pos. + exploit (Zsize_interval_1 y). omega. + omega. +Qed. + +Theorem size_zero: size zero = 0. +Proof. + unfold size; rewrite unsigned_zero; auto. +Qed. + +Theorem bits_size_1: + forall x, x = zero \/ testbit x (Zpred (size x)) = true. +Proof. + intros. destruct (zeq (unsigned x) 0). + left. rewrite <- (repr_unsigned x). rewrite e; auto. + right. apply Ztestbit_size_1. generalize (unsigned_range x); omega. +Qed. + +Theorem bits_size_2: + forall x i, size x <= i -> testbit x i = false. +Proof. + intros. apply Ztestbit_size_2. generalize (unsigned_range x); omega. + fold (size x); omega. +Qed. + +Theorem size_range: + forall x, 0 <= size x <= zwordsize. +Proof. + intros; split. apply Zsize_pos. + destruct (bits_size_1 x). + subst x; unfold size; rewrite unsigned_zero; simpl. generalize wordsize_pos; omega. + destruct (zle (size x) zwordsize); auto. + rewrite bits_above in H. congruence. omega. +Qed. + +Theorem bits_size_3: + forall x n, + 0 <= n -> + (forall i, n <= i < zwordsize -> testbit x i = false) -> + size x <= n. +Proof. + intros. destruct (zle (size x) n). auto. + destruct (bits_size_1 x). + subst x. unfold size; rewrite unsigned_zero; assumption. + rewrite (H0 (Z.pred (size x))) in H1. congruence. + generalize (size_range x); omega. +Qed. + +Theorem bits_size_4: + forall x n, + 0 <= n -> + testbit x (Zpred n) = true -> + (forall i, n <= i < zwordsize -> testbit x i = false) -> + size x = n. +Proof. + intros. + assert (size x <= n). + apply bits_size_3; auto. + destruct (zlt (size x) n). + rewrite bits_size_2 in H0. congruence. omega. + omega. +Qed. + +Theorem size_interval_1: + forall x, 0 <= unsigned x < two_p (size x). +Proof. + intros; apply Zsize_interval_1. generalize (unsigned_range x); omega. +Qed. + +Theorem size_interval_2: + forall x n, 0 <= n -> 0 <= unsigned x < two_p n -> n >= size x. +Proof. + intros. apply Zsize_interval_2; auto. +Qed. + +Theorem size_and: + forall a b, size (and a b) <= Z.min (size a) (size b). +Proof. + intros. + assert (0 <= Z.min (size a) (size b)). + generalize (size_range a) (size_range b). zify; omega. + apply bits_size_3. auto. intros. + rewrite bits_and. zify. subst z z0. destruct H1. + rewrite (bits_size_2 a). auto. omega. + rewrite (bits_size_2 b). apply andb_false_r. omega. + omega. +Qed. + +Corollary and_interval: + forall a b, 0 <= unsigned (and a b) < two_p (Z.min (size a) (size b)). +Proof. + intros. + generalize (size_interval_1 (and a b)); intros. + assert (two_p (size (and a b)) <= two_p (Z.min (size a) (size b))). + apply two_p_monotone. split. generalize (size_range (and a b)); omega. + apply size_and. + omega. +Qed. + +Theorem size_or: + forall a b, size (or a b) = Z.max (size a) (size b). +Proof. + intros. generalize (size_range a) (size_range b); intros. + destruct (bits_size_1 a). + subst a. rewrite size_zero. rewrite or_zero_l. zify; omega. + destruct (bits_size_1 b). + subst b. rewrite size_zero. rewrite or_zero. zify; omega. + zify. destruct H3 as [[P Q] | [P Q]]; subst. + apply bits_size_4. tauto. rewrite bits_or. rewrite H2. apply orb_true_r. + omega. + intros. rewrite bits_or. rewrite !bits_size_2. auto. omega. omega. omega. + apply bits_size_4. tauto. rewrite bits_or. rewrite H1. apply orb_true_l. + destruct (zeq (size a) 0). unfold testbit in H1. rewrite Z.testbit_neg_r in H1. + congruence. omega. omega. + intros. rewrite bits_or. rewrite !bits_size_2. auto. omega. omega. omega. +Qed. + +Corollary or_interval: + forall a b, 0 <= unsigned (or a b) < two_p (Z.max (size a) (size b)). +Proof. + intros. rewrite <- size_or. apply size_interval_1. +Qed. + +Theorem size_xor: + forall a b, size (xor a b) <= Z.max (size a) (size b). +Proof. + intros. + assert (0 <= Z.max (size a) (size b)). + generalize (size_range a) (size_range b). zify; omega. + apply bits_size_3. auto. intros. + rewrite bits_xor. rewrite !bits_size_2. auto. + zify; omega. + zify; omega. + omega. +Qed. + +Corollary xor_interval: + forall a b, 0 <= unsigned (xor a b) < two_p (Z.max (size a) (size b)). +Proof. + intros. + generalize (size_interval_1 (xor a b)); intros. + assert (two_p (size (xor a b)) <= two_p (Z.max (size a) (size b))). + apply two_p_monotone. split. generalize (size_range (xor a b)); omega. + apply size_xor. + omega. +Qed. + End Make. (** * Specialization to integers of size 8, 32, and 64 bits *) diff --git a/lib/Ordered.v b/lib/Ordered.v index 1c7c7f4..ce1eca8 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -38,12 +38,10 @@ Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof Plt_ne. Lemma compare : forall x y : t, Compare lt eq x y. Proof. - intros. case (plt x y); intro. - apply LT. auto. - case (peq x y); intro. - apply EQ. auto. - apply GT. red; unfold Plt in *. - assert (Zpos x <> Zpos y). congruence. omega. + intros. destruct (Pos.compare x y) as [] eqn:E. + apply EQ. red. apply Pos.compare_eq_iff. assumption. + apply LT. assumption. + apply GT. apply Pos.compare_gt_iff. assumption. Qed. Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq. -- cgit v1.2.3