source: C-semantics/Integers.ma @ 173

Last change on this file since 173 was 15, checked in by campbell, 10 years ago

Make some definitions more normalization friendly by a little 'nlet rec'
abuse.

File size: 80.5 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *)
17
18include "arithmetics/nat.ma".
19include "binary/Z.ma".
20include "extralib.ma".
21
22
23(* * * Comparisons *)
24
25ninductive comparison : Type ≝
26  | Ceq : comparison               (**r same *)
27  | Cne : comparison               (**r different *)
28  | Clt : comparison               (**r less than *)
29  | Cle : comparison               (**r less than or equal *)
30  | Cgt : comparison               (**r greater than *)
31  | Cge : comparison.              (**r greater than or equal *)
32
33ndefinition negate_comparison : comparison → comparison ≝ λc.
34  match c with
35  [ Ceq ⇒ Cne
36  | Cne ⇒ Ceq
37  | Clt ⇒ Cge
38  | Cle ⇒ Cgt
39  | Cgt ⇒ Cle
40  | Cge ⇒ Clt
41  ].
42
43ndefinition swap_comparison : comparison → comparison ≝ λc.
44  match c with
45  [ Ceq ⇒ Ceq
46  | Cne ⇒ Cne
47  | Clt ⇒ Cgt
48  | Cle ⇒ Cge
49  | Cgt ⇒ Clt
50  | Cge ⇒ Cle
51  ].
52(*
53(** * Parameterization by the word size, in bits. *)
54
55Module Type WORDSIZE.
56  Variable wordsize: nat.
57  Axiom wordsize_not_zero: wordsize <> 0%nat.
58End WORDSIZE.
59
60Module Make(WS: WORDSIZE).
61
62*)
63
64(*naxiom two_power_nat : nat → Z.*)
65
66ndefinition wordsize : nat ≝ 32.
67ndefinition modulus : Z ≝ Z_two_power_nat wordsize.
68ndefinition half_modulus : Z ≝ modulus / 2.
69ndefinition max_unsigned : Z ≝ modulus - 1.
70ndefinition max_signed : Z ≝ half_modulus - 1.
71ndefinition min_signed : Z ≝ - half_modulus.
72
73nlemma wordsize_pos:
74  Z_of_nat wordsize > 0.
75nnormalize; //; nqed.
76
77nremark modulus_power:
78  modulus = two_p (Z_of_nat wordsize).
79//; nqed.
80
81nremark modulus_pos:
82  modulus > 0.
83//; nqed.
84
85(* * Representation of machine integers *)
86
87(* A machine integer (type [int]) is represented as a Coq arbitrary-precision
88  integer (type [Z]) plus a proof that it is in the range 0 (included) to
89  [modulus] (excluded. *)
90(* XXX: hack to prevent normalization of huge proof term. *)
91ninductive inrange : Z → Prop ≝
92| inrg_mod : ∀i:Z. inrange (i \mod modulus)
93| inrg_pf : ∀i:Z. (0 ≤ i) ∧ i < modulus → inrange i.
94ninductive int: Type ≝
95| mk_int: ∀i:Z. inrange i → int.
96(*
97nrecord int: Type ≝ { intval: Z ; intrange: (0 ≤ intval) ∧ intval < modulus }.
98*)
99ndefinition intval: int → Z ≝ λi.match i with [ mk_int x _ ⇒ x ].
100ndefinition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus.
101#i;ncases i;
102#x H; ncases H;
103##[ #x'; napply modZ_lt_mod; //;
104##| //;
105##] nqed.
106
107(* The [unsigned] and [signed] functions return the Coq integer corresponding
108  to the given machine integer, interpreted as unsigned or signed
109  respectively. *)
110
111ndefinition unsigned : int → Z ≝ intval.
112
113ndefinition signed : int → Z ≝ λn.
114  if Zltb (unsigned n) half_modulus
115  then unsigned n
116  else unsigned n - modulus.
117
118(* Conversely, [repr] takes a Coq integer and returns the corresponding
119  machine integer.  The argument is treated modulo [modulus]. *)
120(*naxiom repr : Z → int.*)
121(*
122ndefinition repr : Z → int := λx.
123  mk_int (x \mod modulus) (modZ_lt_mod x modulus modulus_pos).
124*)
125ndefinition repr : Z → int ≝ λx. mk_int (x \mod modulus) (inrg_mod x).
126
127ndefinition zero := repr 0.
128ndefinition one  := repr 1.
129ndefinition mone := repr (-1).
130ndefinition iwordsize := repr (Z_of_nat wordsize).
131
132naxiom mk_int_eq:
133  ∀x,y,Px,Py. x = y → mk_int x Px = mk_int y Py.
134(*Proof.
135  intros. subst y.
136  generalize (proof_irrelevance _ Px Py); intro.
137  subst Py. reflexivity.
138Qed.*)
139
140naxiom eq_dec: ∀x,y: int. (x = y) + (x ≠ y).
141(*Proof.
142  intros. destruct x; destruct y. case (zeq intval0 intval1); intro.
143  left. apply mkint_eq. auto.
144  right. red; intro. injection H. exact n.
145Qed.*)
146
147(* * Arithmetic and logical operations over machine integers *)
148
149ndefinition eq : int → int → bool ≝ λx,y: int.
150  if eqZb (unsigned x) (unsigned y) then true else false.
151ndefinition lt : int → int → bool ≝ λx,y:int.
152  if Zltb (signed x) (signed y) then true else false.
153ndefinition ltu : int → int → bool ≝ λx,y: int.
154  if Zltb (unsigned x) (unsigned y) then true else false.
155
156ndefinition neg : int → int ≝ λx. repr (- unsigned x).
157
158(*
159ndefinition zero_ext : Z → int → int ≝
160λn,x. repr (modZ (unsigned x) (two_p n)).
161ndefinition sign_ext : Z → int → int ≝
162λn,x. repr (let p ≝ two_p n in
163        let y ≝ modZ (unsigned x) p in
164        if Zltb y (two_p (n-1)) then y else y - p).
165*)
166nlet rec zero_ext (n:Z) (x:int) on x : int ≝
167  repr (modZ (unsigned x) (two_p n)).
168nlet rec sign_ext (n:Z) (x:int) on x : int ≝
169  repr (let p ≝ two_p n in
170        let y ≝ modZ (unsigned x) p in
171        if Zltb y (two_p (n-1)) then y else y - p).
172
173ndefinition add ≝ λx,y: int.
174  repr (unsigned x + unsigned y).
175ndefinition sub ≝ λx,y: int.
176  repr (unsigned x - unsigned y).
177ndefinition mul ≝ λx,y: int.
178  repr (unsigned x * unsigned y).
179ndefinition Zdiv_round : Z → Z → Z ≝ λx,y: Z.
180  if Zltb x 0 then
181    if Zltb y 0 then (-x) / (-y) else - ((-x) / y)
182  else
183    if Zltb y 0 then -(x / (-y)) else x / y.
184
185ndefinition Zmod_round : Z → Z → Z ≝ λx,y: Z.
186  x - (Zdiv_round x y) * y.
187
188ndefinition divs : int → int → int ≝ λx,y:int.
189  repr (Zdiv_round (signed x) (signed y)).
190ndefinition mods : int → int → int ≝ λx,y:int.
191  repr (Zmod_round (signed x) (signed y)).
192ndefinition divu : int → int → int ≝ λx,y.
193  repr (unsigned x / unsigned y).
194ndefinition modu : int → int → int ≝ λx,y.
195  repr (unsigned x \mod unsigned y).
196
197(* * For bitwise operations, we need to convert between Coq integers [Z]
198  and their bit-level representations.  Bit-level representations are
199  represented as characteristic functions, that is, functions [f]
200  of type [nat -> bool] such that [f i] is the value of the [i]-th bit
201  of the number.  The values of characteristic functions for [i] greater
202  than 32 are ignored. *)
203
204ndefinition Z_shift_add ≝ λb: bool. λx: Z.
205  if b then 2 * x + 1 else 2 * x.
206(*
207Definition Z_bin_decomp (x: Z) : bool * Z :=
208  match x with
209  | Z0 => (false, 0)
210  | Zpos p =>
211      match p with
212      | xI q => (true, Zpos q)
213      | xO q => (false, Zpos q)
214      | xH => (true, 0)
215      end
216  | Zneg p =>
217      match p with
218      | xI q => (true, Zneg q - 1)
219      | xO q => (false, Zneg q)
220      | xH => (true, -1)
221      end
222  end.
223*)
224naxiom bits_of_Z : nat → Z → Z → bool.
225naxiom Z_of_bits : nat → (Z → bool) → Z.
226(*
227Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool :=
228  match n with
229  | O =>
230      (fun i: Z => false)
231  | S m =>
232      let (b, y) := Z_bin_decomp x in
233      let f := bits_of_Z m y in
234      (fun i: Z => if zeq i 0 then b else f (i - 1))
235  end.
236
237Fixpoint Z_of_bits (n: nat) (f: Z -> bool) {struct n}: Z :=
238  match n with
239  | O => 0
240  | S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1)))
241  end.
242*)
243(* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *)
244
245ndefinition bitwise_binop ≝ λf: bool -> bool -> bool. λx,y: int.
246  let fx ≝ bits_of_Z wordsize (unsigned x) in
247  let fy ≝ bits_of_Z wordsize (unsigned y) in
248  repr (Z_of_bits wordsize (λi. f (fx i) (fy i))).
249
250ndefinition i_and : int → int → int ≝ λx,y. bitwise_binop andb x y.
251ndefinition or : int → int → int ≝ λx,y. bitwise_binop orb x y.
252ndefinition xor : int → int → int ≝ λx,y. bitwise_binop xorb x y.
253
254ndefinition not : int → int ≝ λx.xor x mone.
255
256(* * Shifts and rotates. *)
257
258ndefinition shl : int → int → int ≝ λx,y.
259  let fx ≝ bits_of_Z wordsize (unsigned x) in
260  let vy ≝ unsigned y in
261  repr (Z_of_bits wordsize (λi. fx (i - vy))).
262
263ndefinition shru : int → int → int ≝ λx,y.
264  let fx ≝ bits_of_Z wordsize (unsigned x) in
265  let vy ≝ unsigned y in
266  repr (Z_of_bits wordsize (λi. fx (i + vy))).
267
268(* * Arithmetic right shift is defined as signed division by a power of two.
269  Two such shifts are defined: [shr] rounds towards minus infinity
270  (standard behaviour for arithmetic right shift) and
271  [shrx] rounds towards zero. *)
272
273ndefinition shr : int → int → int ≝ λx,y.
274  repr (signed x / two_p (unsigned y)).
275
276ndefinition shrx : int → int → int ≝ λx,y.
277  divs x (shl one y).
278
279ndefinition shr_carry ≝ λx,y: int.
280  sub (shrx x y) (shr x y).
281
282ndefinition rol : int → int → int ≝ λx,y.
283  let fx ≝ bits_of_Z wordsize (unsigned x) in
284  let vy ≝ unsigned y in
285  repr (Z_of_bits wordsize
286         (λi. fx (i - vy \mod Z_of_nat wordsize))).
287
288ndefinition ror : int → int → int ≝ λx,y.
289  let fx := bits_of_Z wordsize (unsigned x) in
290  let vy := unsigned y in
291  repr (Z_of_bits wordsize
292         (λi. fx (i + vy \mod Z_of_nat wordsize))).
293
294ndefinition rolm ≝ λx,a,m: int. i_and (rol x a) m.
295(*
296(** Decomposition of a number as a sum of powers of two. *)
297
298Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z :=
299  match n with
300  | O => nil
301  | S m =>
302      let (b, y) := Z_bin_decomp x in
303      if b then i :: Z_one_bits m y (i+1) else Z_one_bits m y (i+1)
304  end.
305
306Definition one_bits (x: int) : list int :=
307  List.map repr (Z_one_bits wordsize (unsigned x) 0).
308
309(** Recognition of powers of two. *)
310
311Definition is_power2 (x: int) : option int :=
312  match Z_one_bits wordsize (unsigned x) 0 with
313  | i :: nil => Some (repr i)
314  | _ => None
315  end.
316
317(** Recognition of integers that are acceptable as immediate operands
318  to the [rlwim] PowerPC instruction.  These integers are of the form
319  [000011110000] or [111100001111], that is, a run of one bits
320  surrounded by zero bits, or conversely.  We recognize these integers by
321  running the following automaton on the bits.  The accepting states are
322  2, 3, 4, 5, and 6.
323<<
324               0          1          0
325              / \        / \        / \
326              \ /        \ /        \ /
327        -0--> [1] --1--> [2] --0--> [3]
328       /     
329     [0]
330       \
331        -1--> [4] --0--> [5] --1--> [6]
332              / \        / \        / \
333              \ /        \ /        \ /
334               1          0          1
335>>
336*)
337
338Inductive rlw_state: Type :=
339  | RLW_S0 : rlw_state
340  | RLW_S1 : rlw_state
341  | RLW_S2 : rlw_state
342  | RLW_S3 : rlw_state
343  | RLW_S4 : rlw_state
344  | RLW_S5 : rlw_state
345  | RLW_S6 : rlw_state
346  | RLW_Sbad : rlw_state.
347
348Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state :=
349  match s, b with
350  | RLW_S0, false => RLW_S1
351  | RLW_S0, true  => RLW_S4
352  | RLW_S1, false => RLW_S1
353  | RLW_S1, true  => RLW_S2
354  | RLW_S2, false => RLW_S3
355  | RLW_S2, true  => RLW_S2
356  | RLW_S3, false => RLW_S3
357  | RLW_S3, true  => RLW_Sbad
358  | RLW_S4, false => RLW_S5
359  | RLW_S4, true  => RLW_S4
360  | RLW_S5, false => RLW_S5
361  | RLW_S5, true  => RLW_S6
362  | RLW_S6, false => RLW_Sbad
363  | RLW_S6, true  => RLW_S6
364  | RLW_Sbad, _ => RLW_Sbad
365  end.
366
367Definition rlw_accepting (s: rlw_state) : bool :=
368  match s with
369  | RLW_S0 => false
370  | RLW_S1 => false
371  | RLW_S2 => true
372  | RLW_S3 => true
373  | RLW_S4 => true
374  | RLW_S5 => true
375  | RLW_S6 => true
376  | RLW_Sbad => false
377  end.
378
379Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool :=
380  match n with
381  | O =>
382      rlw_accepting s
383  | S m =>
384      let (b, y) := Z_bin_decomp x in
385      is_rlw_mask_rec m (rlw_transition s b) y
386  end.
387
388Definition is_rlw_mask (x: int) : bool :=
389  is_rlw_mask_rec wordsize RLW_S0 (unsigned x).
390*)
391(* * Comparisons. *)
392
393ndefinition cmp : comparison → int → int → bool ≝ λc,x,y.
394  match c with
395  [ Ceq ⇒ eq x y
396  | Cne ⇒ notb (eq x y)
397  | Clt ⇒ lt x y
398  | Cle ⇒ notb (lt y x)
399  | Cgt ⇒ lt y x
400  | Cge ⇒ notb (lt x y)
401  ].
402
403ndefinition cmpu : comparison → int → int → bool ≝ λc,x,y.
404  match c with
405  [ Ceq ⇒ eq x y
406  | Cne ⇒ notb (eq x y)
407  | Clt ⇒ ltu x y
408  | Cle ⇒ notb (ltu y x)
409  | Cgt ⇒ ltu y x
410  | Cge ⇒ notb (ltu x y)
411  ].
412
413ndefinition is_false : int → Prop ≝ λx. x = zero.
414ndefinition is_true  : int → Prop ≝ λx. x ≠ zero.
415ndefinition notbool  : int → int  ≝ λx. if eq x zero then one else zero.
416(*
417(** * Properties of integers and integer arithmetic *)
418
419(** ** Properties of [modulus], [max_unsigned], etc. *)
420
421Remark half_modulus_power:
422  half_modulus = two_p (Z_of_nat wordsize - 1).
423Proof.
424  unfold half_modulus. rewrite modulus_power.
425  set (ws1 := Z_of_nat wordsize - 1).
426  replace (Z_of_nat wordsize) with (Zsucc ws1).
427  rewrite two_p_S. rewrite Zmult_comm. apply Z_div_mult. omega.
428  unfold ws1. generalize wordsize_pos; omega.
429  unfold ws1. omega.
430Qed.
431
432Remark half_modulus_modulus: modulus = 2 * half_modulus.
433Proof.
434  rewrite half_modulus_power. rewrite modulus_power.
435  rewrite <- two_p_S. decEq. omega.
436  generalize wordsize_pos; omega.
437Qed.
438
439(** Relative positions, from greatest to smallest:
440<<
441      max_unsigned
442      max_signed
443      2*wordsize-1
444      wordsize
445      0
446      min_signed
447>>
448*)
449
450Remark half_modulus_pos: half_modulus > 0.
451Proof.
452  rewrite half_modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega.
453Qed.
454
455Remark min_signed_neg: min_signed < 0.
456Proof.
457  unfold min_signed. generalize half_modulus_pos. omega.
458Qed.
459
460Remark max_signed_pos: max_signed >= 0.
461Proof.
462  unfold max_signed. generalize half_modulus_pos. omega.
463Qed.
464
465Remark wordsize_max_unsigned: Z_of_nat wordsize <= max_unsigned.
466Proof.
467  assert (Z_of_nat wordsize < modulus).
468    rewrite modulus_power. apply two_p_strict.
469    generalize wordsize_pos. omega.
470  unfold max_unsigned. omega.
471Qed.
472
473Remark two_wordsize_max_unsigned: 2 * Z_of_nat wordsize - 1 <= max_unsigned.
474Proof.
475  assert (2 * Z_of_nat wordsize - 1 < modulus).
476    rewrite modulus_power. apply two_p_strict_2. generalize wordsize_pos; omega.
477  unfold max_unsigned; omega.
478Qed.
479
480Remark max_signed_unsigned: max_signed < max_unsigned.
481Proof.
482  unfold max_signed, max_unsigned. rewrite half_modulus_modulus.
483  generalize half_modulus_pos. omega.
484Qed.
485
486(** ** Properties of zero, one, minus one *)
487
488Theorem unsigned_zero: unsigned zero = 0.
489Proof.
490  simpl. apply Zmod_0_l.
491Qed.
492
493Theorem unsigned_one: unsigned one = 1.
494Proof.
495  simpl. apply Zmod_small. split. omega.
496  unfold modulus. replace wordsize with (S(pred wordsize)).
497  rewrite two_power_nat_S. generalize (two_power_nat_pos (pred wordsize)).
498  omega.
499  generalize wordsize_pos. omega.
500Qed.
501
502Theorem unsigned_mone: unsigned mone = modulus - 1.
503Proof.
504  simpl unsigned.
505  replace (-1) with ((modulus - 1) + (-1) * modulus).
506  rewrite Z_mod_plus_full. apply Zmod_small.
507  generalize modulus_pos. omega. omega.
508Qed.
509
510Theorem signed_zero: signed zero = 0.
511Proof.
512  unfold signed. rewrite unsigned_zero. apply zlt_true. generalize half_modulus_pos; omega.
513Qed.
514
515Theorem signed_mone: signed mone = -1.
516Proof.
517  unfold signed. rewrite unsigned_mone.
518  rewrite zlt_false. omega.
519  rewrite half_modulus_modulus. generalize half_modulus_pos. omega. 
520Qed.
521*)
522naxiom one_not_zero: one ≠ zero.
523(*
524Theorem one_not_zero: one <> zero.
525Proof.
526  assert (unsigned one <> unsigned zero).
527  rewrite unsigned_one; rewrite unsigned_zero; congruence.
528  congruence.
529Qed.
530
531Theorem unsigned_repr_wordsize:
532  unsigned iwordsize = Z_of_nat wordsize.
533Proof.
534  simpl. apply Zmod_small.
535  generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega.
536Qed.
537*)
538(* * ** Properties of equality *)
539
540ntheorem eq_sym:
541  ∀x,y. eq x y = eq y x.
542#x y; nwhd in ⊢ (??%%); napply eqZb_elim; #H;
543##[ nrewrite > H; nrewrite > (eqZb_z_z …); //
544##| nrewrite > (eqZb_false … (sym_neq … H)); //
545##] nqed.
546
547ntheorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y).
548#x y; nwhd in ⊢ (??%??); nelim (eq_dec x y); #H;
549##[ nrewrite > H; nrewrite > (eqZb_z_z …); //;
550##| nrewrite > (eqZb_false …); //;
551    nelim x in H ⊢ %; nelim y;
552    #x' Px y' Py H; nnormalize; napply (not_to_not … H); napply mk_int_eq;
553##] nqed.
554
555ntheorem eq_true: ∀x. eq x x = true.
556#x; nlapply (eq_spec x x); nelim (eq x x); //;
557#H; nnormalize in H; napply False_ind; napply (absurd ? (refl ??) H);
558nqed.
559
560ntheorem eq_false: ∀x,y. x ≠ y → eq x y = false.
561#x y; nlapply (eq_spec x y); nelim (eq x y); //;
562#H H'; napply False_ind; napply (absurd ? H H');
563nqed.
564(*
565(** ** Modulo arithmetic *)
566
567(** We define and state properties of equality and arithmetic modulo a
568  positive integer. *)
569
570Section EQ_MODULO.
571
572Variable modul: Z.
573Hypothesis modul_pos: modul > 0.
574
575Definition eqmod (x y: Z) : Prop := exists k, x = k * modul + y.
576
577Lemma eqmod_refl: forall x, eqmod x x.
578Proof.
579  intros; red. exists 0. omega.
580Qed.
581
582Lemma eqmod_refl2: forall x y, x = y -> eqmod x y.
583Proof.
584  intros. subst y. apply eqmod_refl.
585Qed.
586
587Lemma eqmod_sym: forall x y, eqmod x y -> eqmod y x.
588Proof.
589  intros x y [k EQ]; red. exists (-k). subst x. ring.
590Qed.
591
592Lemma eqmod_trans: forall x y z, eqmod x y -> eqmod y z -> eqmod x z.
593Proof.
594  intros x y z [k1 EQ1] [k2 EQ2]; red.
595  exists (k1 + k2). subst x; subst y. ring.
596Qed.
597
598Lemma eqmod_small_eq:
599  forall x y, eqmod x y -> 0 <= x < modul -> 0 <= y < modul -> x = y.
600Proof.
601  intros x y [k EQ] I1 I2.
602  generalize (Zdiv_unique _ _ _ _ EQ I2). intro.
603  rewrite (Zdiv_small x modul I1) in H. subst k. omega.
604Qed.
605
606Lemma eqmod_mod_eq:
607  forall x y, eqmod x y -> x mod modul = y mod modul.
608Proof.
609  intros x y [k EQ]. subst x.
610  rewrite Zplus_comm. apply Z_mod_plus. auto.
611Qed.
612
613Lemma eqmod_mod:
614  forall x, eqmod x (x mod modul).
615Proof.
616  intros; red. exists (x / modul).
617  rewrite Zmult_comm. apply Z_div_mod_eq. auto.
618Qed.
619
620Lemma eqmod_add:
621  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a + c) (b + d).
622Proof.
623  intros a b c d [k1 EQ1] [k2 EQ2]; red.
624  subst a; subst c. exists (k1 + k2). ring.
625Qed.
626
627Lemma eqmod_neg:
628  forall x y, eqmod x y -> eqmod (-x) (-y).
629Proof.
630  intros x y [k EQ]; red. exists (-k). rewrite EQ. ring.
631Qed.
632
633Lemma eqmod_sub:
634  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a - c) (b - d).
635Proof.
636  intros a b c d [k1 EQ1] [k2 EQ2]; red.
637  subst a; subst c. exists (k1 - k2). ring.
638Qed.
639
640Lemma eqmod_mult:
641  forall a b c d, eqmod a c -> eqmod b d -> eqmod (a * b) (c * d).
642Proof.
643  intros a b c d [k1 EQ1] [k2 EQ2]; red.
644  subst a; subst b.
645  exists (k1 * k2 * modul + c * k2 + k1 * d).
646  ring.
647Qed.
648
649End EQ_MODULO.
650
651Lemma eqmod_divides:
652  forall n m x y, eqmod n x y -> Zdivide m n -> eqmod m x y.
653Proof.
654  intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2].
655  exists (k1*k2). rewrite <- Zmult_assoc. rewrite <- EQ2. auto.
656Qed.
657
658(** We then specialize these definitions to equality modulo
659  $2^{wordsize}$ #2<sup>wordsize</sup>#. *)
660
661Hint Resolve modulus_pos: ints.
662
663Definition eqm := eqmod modulus.
664
665Lemma eqm_refl: forall x, eqm x x.
666Proof (eqmod_refl modulus).
667Hint Resolve eqm_refl: ints.
668
669Lemma eqm_refl2:
670  forall x y, x = y -> eqm x y.
671Proof (eqmod_refl2 modulus).
672Hint Resolve eqm_refl2: ints.
673
674Lemma eqm_sym: forall x y, eqm x y -> eqm y x.
675Proof (eqmod_sym modulus).
676Hint Resolve eqm_sym: ints.
677
678Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z.
679Proof (eqmod_trans modulus).
680Hint Resolve eqm_trans: ints.
681
682Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y.
683Proof.
684  intros. unfold repr. apply mkint_eq.
685  apply eqmod_mod_eq. auto with ints. exact H.
686Qed.
687
688Lemma eqm_small_eq:
689  forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y.
690Proof (eqmod_small_eq modulus).
691Hint Resolve eqm_small_eq: ints.
692
693Lemma eqm_add:
694  forall a b c d, eqm a b -> eqm c d -> eqm (a + c) (b + d).
695Proof (eqmod_add modulus).
696Hint Resolve eqm_add: ints.
697
698Lemma eqm_neg:
699  forall x y, eqm x y -> eqm (-x) (-y).
700Proof (eqmod_neg modulus).
701Hint Resolve eqm_neg: ints.
702
703Lemma eqm_sub:
704  forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d).
705Proof (eqmod_sub modulus).
706Hint Resolve eqm_sub: ints.
707
708Lemma eqm_mult:
709  forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d).
710Proof (eqmod_mult modulus).
711Hint Resolve eqm_mult: ints.
712
713(** ** Properties of the coercions between [Z] and [int] *)
714
715Lemma eqm_unsigned_repr:
716  forall z, eqm z (unsigned (repr z)).
717Proof.
718  unfold eqm, repr, unsigned; intros; simpl.
719  apply eqmod_mod. auto with ints.
720Qed.
721Hint Resolve eqm_unsigned_repr: ints.
722
723Lemma eqm_unsigned_repr_l:
724  forall a b, eqm a b -> eqm (unsigned (repr a)) b.
725Proof.
726  intros. apply eqm_trans with a.
727  apply eqm_sym. apply eqm_unsigned_repr. auto.
728Qed.
729Hint Resolve eqm_unsigned_repr_l: ints.
730
731Lemma eqm_unsigned_repr_r:
732  forall a b, eqm a b -> eqm a (unsigned (repr b)).
733Proof.
734  intros. apply eqm_trans with b. auto.
735  apply eqm_unsigned_repr.
736Qed.
737Hint Resolve eqm_unsigned_repr_r: ints.
738
739Lemma eqm_signed_unsigned:
740  forall x, eqm (signed x) (unsigned x).
741Proof.
742  intro; red; unfold signed. set (y := unsigned x).
743  case (zlt y half_modulus); intro.
744  apply eqmod_refl. red; exists (-1); ring.
745Qed.
746
747Theorem unsigned_range:
748  forall i, 0 <= unsigned i < modulus.
749Proof.
750  destruct i; simpl. auto.
751Qed.
752Hint Resolve unsigned_range: ints.
753
754Theorem unsigned_range_2:
755  forall i, 0 <= unsigned i <= max_unsigned.
756Proof.
757  intro; unfold max_unsigned.
758  generalize (unsigned_range i). omega.
759Qed.
760Hint Resolve unsigned_range_2: ints.
761*)
762naxiom signed_range:
763  ∀i. min_signed ≤ signed i ∧ signed i ≤ max_signed.
764(*
765Theorem signed_range:
766  forall i, min_signed <= signed i <= max_signed.
767Proof.
768  intros. unfold signed.
769  generalize (unsigned_range i). set (n := unsigned i). intros.
770  case (zlt n half_modulus); intro.
771  unfold max_signed. generalize min_signed_neg. omega.
772  unfold min_signed, max_signed.
773  rewrite half_modulus_modulus in *. omega.
774Qed. 
775
776Theorem repr_unsigned:
777  forall i, repr (unsigned i) = i.
778Proof.
779  destruct i; simpl. unfold repr. apply mkint_eq.
780  apply Zmod_small. auto.
781Qed.
782Hint Resolve repr_unsigned: ints.
783
784Lemma repr_signed:
785  forall i, repr (signed i) = i.
786Proof.
787  intros. transitivity (repr (unsigned i)).
788  apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints.
789Qed.
790Hint Resolve repr_signed: ints.
791
792Theorem unsigned_repr:
793  forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z.
794Proof.
795  intros. unfold repr, unsigned; simpl.
796  apply Zmod_small. unfold max_unsigned in H. omega.
797Qed.
798Hint Resolve unsigned_repr: ints.
799*)
800naxiom signed_repr:
801  ∀z. min_signed ≤ z ∧ z ≤ max_signed → signed (repr z) = z.
802(*
803Theorem signed_repr:
804  forall z, min_signed <= z <= max_signed -> signed (repr z) = z.
805Proof.
806  intros. unfold signed. case (zle 0 z); intro.
807  replace (unsigned (repr z)) with z.
808  rewrite zlt_true. auto. unfold max_signed in H. omega.
809  symmetry. apply unsigned_repr. generalize max_signed_unsigned. omega.
810  pose (z' := z + modulus).
811  replace (repr z) with (repr z').
812  replace (unsigned (repr z')) with z'.
813  rewrite zlt_false. unfold z'. omega.
814  unfold z'. unfold min_signed in H.
815  rewrite half_modulus_modulus. omega.
816  symmetry. apply unsigned_repr.
817  unfold z', max_unsigned. unfold min_signed, max_signed in H.
818  rewrite half_modulus_modulus. omega.
819  apply eqm_samerepr. unfold z'; red. exists 1. omega.
820Qed.
821
822Theorem signed_eq_unsigned:
823  forall x, unsigned x <= max_signed -> signed x = unsigned x.
824Proof.
825  intros. unfold signed. destruct (zlt (unsigned x) half_modulus).
826  auto. unfold max_signed in H. omegaContradiction.
827Qed.
828
829(** ** Properties of addition *)
830
831*)
832naxiom add_unsigned: ∀x,y. add x y = repr (unsigned x + unsigned y).
833naxiom add_signed: ∀x,y. add x y = repr (signed x + signed y).
834naxiom add_zero: ∀x. add x zero = x.
835
836(*
837Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y).
838Proof. intros; reflexivity.
839Qed.
840
841Theorem add_signed: forall x y, add x y = repr (signed x + signed y).
842Proof.
843  intros. rewrite add_unsigned. apply eqm_samerepr.
844  apply eqm_add; apply eqm_sym; apply eqm_signed_unsigned.
845Qed.
846
847Theorem add_commut: forall x y, add x y = add y x.
848Proof. intros; unfold add. decEq. omega. Qed.
849
850Theorem add_zero: forall x, add x zero = x.
851Proof.
852  intros; unfold add, zero. change (unsigned (repr 0)) with 0.
853  rewrite Zplus_0_r. apply repr_unsigned.
854Qed.
855
856Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
857Proof.
858  intros; unfold add.
859  set (x' := unsigned x).
860  set (y' := unsigned y).
861  set (z' := unsigned z).
862  apply eqm_samerepr.
863  apply eqm_trans with ((x' + y') + z').
864  auto with ints.
865  rewrite <- Zplus_assoc. auto with ints.
866Qed.
867
868Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
869Proof.
870  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut.
871Qed.
872
873Theorem add_neg_zero: forall x, add x (neg x) = zero.
874Proof.
875  intros; unfold add, neg, zero. apply eqm_samerepr.
876  replace 0 with (unsigned x + (- (unsigned x))).
877  auto with ints. omega.
878Qed.
879
880(** ** Properties of negation *)
881
882Theorem neg_repr: forall z, neg (repr z) = repr (-z).
883Proof.
884  intros; unfold neg. apply eqm_samerepr. auto with ints.
885Qed.
886
887Theorem neg_zero: neg zero = zero.
888Proof.
889  unfold neg, zero. compute. apply mkint_eq. auto.
890Qed.
891
892Theorem neg_involutive: forall x, neg (neg x) = x.
893Proof.
894  intros; unfold neg. transitivity (repr (unsigned x)).
895  apply eqm_samerepr. apply eqm_trans with (- (- (unsigned x))).
896  apply eqm_neg. apply eqm_unsigned_repr_l. apply eqm_refl.
897  apply eqm_refl2. omega. apply repr_unsigned.
898Qed.
899
900Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
901Proof.
902  intros; unfold neg, add. apply eqm_samerepr.
903  apply eqm_trans with (- (unsigned x + unsigned y)).
904  auto with ints.
905  replace (- (unsigned x + unsigned y))
906     with ((- unsigned x) + (- unsigned y)).
907  auto with ints. omega.
908Qed.
909
910(** ** Properties of subtraction *)
911
912Theorem sub_zero_l: forall x, sub x zero = x.
913Proof.
914  intros; unfold sub. change (unsigned zero) with 0.
915  replace (unsigned x - 0) with (unsigned x). apply repr_unsigned.
916  omega.
917Qed.
918
919Theorem sub_zero_r: forall x, sub zero x = neg x.
920Proof.
921  intros; unfold sub, neg. change (unsigned zero) with 0.
922  replace (0 - unsigned x) with (- unsigned x). auto.
923  omega.
924Qed.
925
926Theorem sub_add_opp: forall x y, sub x y = add x (neg y).
927Proof.
928  intros; unfold sub, add, neg.
929  replace (unsigned x - unsigned y)
930     with (unsigned x + (- unsigned y)).
931  apply eqm_samerepr. auto with ints. omega.
932Qed.
933
934Theorem sub_idem: forall x, sub x x = zero.
935Proof.
936  intros; unfold sub. replace (unsigned x - unsigned x) with 0.
937  reflexivity. omega.
938Qed.
939
940Theorem sub_add_l: forall x y z, sub (add x y) z = add (sub x z) y.
941Proof.
942  intros. repeat rewrite sub_add_opp.
943  repeat rewrite add_assoc. decEq. apply add_commut.
944Qed.
945
946Theorem sub_add_r: forall x y z, sub x (add y z) = add (sub x z) (neg y).
947Proof.
948  intros. repeat rewrite sub_add_opp.
949  rewrite neg_add_distr. rewrite add_permut. apply add_commut.
950Qed.
951
952Theorem sub_shifted:
953  forall x y z,
954  sub (add x z) (add y z) = sub x y.
955Proof.
956  intros. rewrite sub_add_opp. rewrite neg_add_distr.
957  rewrite add_assoc.
958  rewrite (add_commut (neg y) (neg z)).
959  rewrite <- (add_assoc z). rewrite add_neg_zero.
960  rewrite (add_commut zero). rewrite add_zero.
961  symmetry. apply sub_add_opp.
962Qed.
963
964Theorem sub_signed:
965  forall x y, sub x y = repr (signed x - signed y).
966Proof.
967  intros. unfold sub. apply eqm_samerepr.
968  apply eqm_sub; apply eqm_sym; apply eqm_signed_unsigned.
969Qed.
970
971(** ** Properties of multiplication *)
972
973Theorem mul_commut: forall x y, mul x y = mul y x.
974Proof.
975  intros; unfold mul. decEq. ring.
976Qed.
977
978Theorem mul_zero: forall x, mul x zero = zero.
979Proof.
980  intros; unfold mul. change (unsigned zero) with 0.
981  unfold zero. decEq. ring.
982Qed.
983
984Theorem mul_one: forall x, mul x one = x.
985Proof.
986  intros; unfold mul. rewrite unsigned_one.
987  transitivity (repr (unsigned x)). decEq. ring.
988  apply repr_unsigned.
989Qed.
990
991Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).
992Proof.
993  intros; unfold mul.
994  set (x' := unsigned x).
995  set (y' := unsigned y).
996  set (z' := unsigned z).
997  apply eqm_samerepr. apply eqm_trans with ((x' * y') * z').
998  auto with ints.
999  rewrite <- Zmult_assoc. auto with ints.
1000Qed.
1001
1002Theorem mul_add_distr_l:
1003  forall x y z, mul (add x y) z = add (mul x z) (mul y z).
1004Proof.
1005  intros; unfold mul, add.
1006  apply eqm_samerepr.
1007  set (x' := unsigned x).
1008  set (y' := unsigned y).
1009  set (z' := unsigned z).
1010  apply eqm_trans with ((x' + y') * z').
1011  auto with ints.
1012  replace ((x' + y') * z') with (x' * z' + y' * z').
1013  auto with ints.
1014  ring.
1015Qed.
1016
1017Theorem mul_add_distr_r:
1018  forall x y z, mul x (add y z) = add (mul x y) (mul x z).
1019Proof.
1020  intros. rewrite mul_commut. rewrite mul_add_distr_l.
1021  decEq; apply mul_commut.
1022Qed.
1023
1024Theorem neg_mul_distr_l:
1025  forall x y, neg(mul x y) = mul (neg x) y.
1026Proof.
1027  intros. unfold mul, neg.
1028  set (x' := unsigned x).  set (y' := unsigned y).
1029  apply eqm_samerepr. apply eqm_trans with (- (x' * y')).
1030  auto with ints.
1031  replace (- (x' * y')) with ((-x') * y') by ring.
1032  auto with ints.
1033Qed.
1034
1035Theorem neg_mul_distr_r:
1036   forall x y, neg(mul x y) = mul x (neg y).
1037Proof.
1038  intros. rewrite (mul_commut x y). rewrite (mul_commut x (neg y)).
1039  apply neg_mul_distr_l.
1040Qed.
1041
1042Theorem mul_signed:
1043  forall x y, mul x y = repr (signed x * signed y).
1044Proof.
1045  intros; unfold mul. apply eqm_samerepr.
1046  apply eqm_mult; apply eqm_sym; apply eqm_signed_unsigned.
1047Qed.
1048
1049(** ** Properties of binary decompositions *)
1050
1051Lemma Z_shift_add_bin_decomp:
1052  forall x,
1053  Z_shift_add (fst (Z_bin_decomp x)) (snd (Z_bin_decomp x)) = x.
1054Proof.
1055  destruct x; simpl.
1056  auto.
1057  destruct p; reflexivity.
1058  destruct p; try reflexivity. simpl.
1059  assert (forall z, 2 * (z + 1) - 1 = 2 * z + 1). intro; omega.
1060  generalize (H (Zpos p)); simpl. congruence.
1061Qed.
1062
1063Lemma Z_shift_add_inj:
1064  forall b1 x1 b2 x2,
1065  Z_shift_add b1 x1 = Z_shift_add b2 x2 -> b1 = b2 /\ x1 = x2.
1066Proof.
1067  intros until x2.
1068  unfold Z_shift_add.
1069  destruct b1; destruct b2; intros;
1070  ((split; [reflexivity|omega]) || omegaContradiction).
1071Qed.
1072
1073Lemma Z_of_bits_exten:
1074  forall n f1 f2,
1075  (forall z, 0 <= z < Z_of_nat n -> f1 z = f2 z) ->
1076  Z_of_bits n f1 = Z_of_bits n f2.
1077Proof.
1078  induction n; intros.
1079  reflexivity.
1080  simpl. rewrite inj_S in H. decEq. apply H. omega.
1081  apply IHn. intros; apply H. omega.
1082Qed.
1083
1084Opaque Zmult.
1085
1086Lemma Z_of_bits_of_Z:
1087  forall x, eqm (Z_of_bits wordsize (bits_of_Z wordsize x)) x.
1088Proof.
1089  assert (forall n x, exists k,
1090    Z_of_bits n (bits_of_Z n x) = k * two_power_nat n + x).
1091  induction n; intros.
1092  rewrite two_power_nat_O. simpl. exists (-x). omega.
1093  rewrite two_power_nat_S. simpl.
1094  caseEq (Z_bin_decomp x). intros b y ZBD. simpl.
1095  replace (Z_of_bits n (fun i => if zeq (i + 1) 0 then b else bits_of_Z n y (i + 1 - 1)))
1096     with (Z_of_bits n (bits_of_Z n y)).
1097  elim (IHn y). intros k1 EQ1. rewrite EQ1.
1098  rewrite <- (Z_shift_add_bin_decomp x).
1099  rewrite ZBD. simpl.
1100  exists k1.
1101  case b; unfold Z_shift_add; ring.
1102  apply Z_of_bits_exten. intros.
1103  rewrite zeq_false. decEq. omega. omega.
1104  intro. exact (H wordsize x).
1105Qed.
1106
1107Lemma bits_of_Z_zero:
1108  forall n x, bits_of_Z n 0 x = false.
1109Proof.
1110  induction n; simpl; intros.
1111  auto.
1112  case (zeq x 0); intro. auto. auto.
1113Qed.
1114
1115Remark Z_bin_decomp_2xm1:
1116  forall x, Z_bin_decomp (2 * x - 1) = (true, x - 1).
1117Proof.
1118  intros. caseEq (Z_bin_decomp (2 * x - 1)). intros b y EQ.
1119  generalize (Z_shift_add_bin_decomp (2 * x - 1)).
1120  rewrite EQ; simpl.
1121  replace (2 * x - 1) with (Z_shift_add true (x - 1)).
1122  intro. elim (Z_shift_add_inj _ _ _ _ H); intros.
1123  congruence. unfold Z_shift_add. omega.
1124Qed.
1125
1126Lemma bits_of_Z_mone:
1127  forall n x,
1128  0 <= x < Z_of_nat n ->
1129  bits_of_Z n (two_power_nat n - 1) x = true.
1130Proof.
1131  induction n; intros.
1132  simpl in H. omegaContradiction.
1133  unfold bits_of_Z; fold bits_of_Z.
1134  rewrite two_power_nat_S. rewrite Z_bin_decomp_2xm1.
1135  rewrite inj_S in H. case (zeq x 0); intro. auto.
1136  apply IHn. omega.
1137Qed.
1138
1139Lemma Z_bin_decomp_shift_add:
1140  forall b x, Z_bin_decomp (Z_shift_add b x) = (b, x).
1141Proof.
1142  intros. caseEq (Z_bin_decomp (Z_shift_add b x)); intros b' x' EQ.
1143  generalize (Z_shift_add_bin_decomp (Z_shift_add b x)).
1144  rewrite EQ; simpl fst; simpl snd. intro.
1145  elim (Z_shift_add_inj _ _ _ _ H); intros.
1146  congruence.
1147Qed.
1148
1149Lemma bits_of_Z_of_bits:
1150  forall n f i,
1151  0 <= i < Z_of_nat n ->
1152  bits_of_Z n (Z_of_bits n f) i = f i.
1153Proof.
1154  induction n; intros; simpl.
1155  simpl in H. omegaContradiction.
1156  rewrite Z_bin_decomp_shift_add.
1157  case (zeq i 0); intro.
1158  congruence.
1159  rewrite IHn. decEq. omega. rewrite inj_S in H. omega.
1160Qed. 
1161
1162Lemma Z_of_bits_range:
1163  forall f, 0 <= Z_of_bits wordsize f < modulus.
1164Proof.
1165  unfold max_unsigned, modulus.
1166  generalize wordsize. induction n; simpl; intros.
1167  rewrite two_power_nat_O. omega.
1168  rewrite two_power_nat_S. generalize (IHn (fun i => f (i + 1))).
1169  set (x := Z_of_bits n (fun i => f (i + 1))).
1170  intro. destruct (f 0); unfold Z_shift_add; omega.
1171Qed.
1172Hint Resolve Z_of_bits_range: ints.
1173
1174Lemma Z_of_bits_range_2:
1175  forall f, 0 <= Z_of_bits wordsize f <= max_unsigned.
1176Proof.
1177  intros. unfold max_unsigned.
1178  generalize (Z_of_bits_range f). omega.
1179Qed.
1180Hint Resolve Z_of_bits_range_2: ints.
1181
1182Lemma bits_of_Z_below:
1183  forall n x i, i < 0 -> bits_of_Z n x i = false.
1184Proof.
1185  induction n; simpl; intros.
1186  reflexivity.
1187  destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn.
1188  omega. omega.
1189Qed.
1190
1191Lemma bits_of_Z_above:
1192  forall n x i, i >= Z_of_nat n -> bits_of_Z n x i = false.
1193Proof.
1194  induction n; intros; simpl.
1195  reflexivity.
1196  destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn.
1197  rewrite inj_S in H. omega. rewrite inj_S in H. omega.
1198Qed.
1199
1200Lemma bits_of_Z_of_bits':
1201  forall n f i,
1202  bits_of_Z n (Z_of_bits n f) i =
1203  if zlt i 0 then false
1204  else if zle (Z_of_nat n) i then false
1205  else f i.
1206Proof.
1207  intros.
1208  destruct (zlt i 0). apply bits_of_Z_below; auto.
1209  destruct (zle (Z_of_nat n) i). apply bits_of_Z_above. omega.
1210  apply bits_of_Z_of_bits. omega.
1211Qed.
1212
1213Opaque Zmult.
1214
1215Lemma Z_of_bits_excl:
1216  forall n f g h,
1217  (forall i, 0 <= i < Z_of_nat n -> f i && g i = false) ->
1218  (forall i, 0 <= i < Z_of_nat n -> f i || g i = h i) ->
1219  Z_of_bits n f + Z_of_bits n g = Z_of_bits n h.
1220Proof.
1221  induction n.
1222  intros; reflexivity.
1223  intros. simpl. rewrite inj_S in H. rewrite inj_S in H0.
1224  rewrite <- (IHn (fun i => f(i+1)) (fun i => g(i+1)) (fun i => h(i+1))).
1225  assert (0 <= 0 < Zsucc(Z_of_nat n)). omega.
1226  unfold Z_shift_add.
1227  rewrite <- H0; auto.
1228  set (F := Z_of_bits n (fun i => f(i + 1))).
1229  set (G := Z_of_bits n (fun i => g(i + 1))).
1230  caseEq (f 0); intros; caseEq (g 0); intros; simpl.
1231  generalize (H 0 H1). rewrite H2; rewrite H3. simpl. intros; discriminate.
1232  omega. omega. omega.
1233  intros; apply H. omega.
1234  intros; apply H0. omega.
1235Qed.
1236
1237(** ** Properties of bitwise and, or, xor *)
1238
1239Lemma bitwise_binop_commut:
1240  forall f,
1241  (forall a b, f a b = f b a) ->
1242  forall x y,
1243  bitwise_binop f x y = bitwise_binop f y x.
1244Proof.
1245  unfold bitwise_binop; intros.
1246  decEq. apply Z_of_bits_exten; intros. auto.
1247Qed.
1248
1249Lemma bitwise_binop_assoc:
1250  forall f,
1251  (forall a b c, f a (f b c) = f (f a b) c) ->
1252  forall x y z,
1253  bitwise_binop f (bitwise_binop f x y) z =
1254  bitwise_binop f x (bitwise_binop f y z).
1255Proof.
1256  unfold bitwise_binop; intros.
1257  repeat rewrite unsigned_repr; auto with ints.
1258  decEq. apply Z_of_bits_exten; intros.
1259  repeat (rewrite bits_of_Z_of_bits; auto).
1260Qed.
1261
1262Lemma bitwise_binop_idem:
1263  forall f,
1264  (forall a, f a a = a) ->
1265  forall x,
1266  bitwise_binop f x x = x.
1267Proof.
1268  unfold bitwise_binop; intros.
1269  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
1270  decEq. apply Z_of_bits_exten; intros. auto.
1271  transitivity (repr (unsigned x)).
1272  apply eqm_samerepr. apply Z_of_bits_of_Z. apply repr_unsigned.
1273Qed.
1274
1275Theorem and_commut: forall x y, and x y = and y x.
1276Proof (bitwise_binop_commut andb andb_comm).
1277
1278Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
1279Proof (bitwise_binop_assoc andb andb_assoc).
1280
1281Theorem and_zero: forall x, and x zero = zero.
1282Proof.
1283  intros. unfold and, bitwise_binop.
1284  apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
1285  apply eqm_refl2. apply Z_of_bits_exten. intros.
1286  rewrite unsigned_zero. rewrite bits_of_Z_zero. apply andb_b_false.
1287Qed.
1288
1289Theorem and_mone: forall x, and x mone = x.
1290Proof.
1291  intros. unfold and, bitwise_binop.
1292  transitivity (repr(unsigned x)).
1293  apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
1294  apply eqm_refl2. apply Z_of_bits_exten. intros.
1295  rewrite unsigned_mone. rewrite bits_of_Z_mone. apply andb_b_true. auto.
1296  apply repr_unsigned.
1297Qed.
1298
1299Theorem and_idem: forall x, and x x = x.
1300Proof.
1301  assert (forall b, b && b = b).
1302    destruct b; reflexivity.
1303  exact (bitwise_binop_idem andb H).
1304Qed.
1305
1306Theorem or_commut: forall x y, or x y = or y x.
1307Proof (bitwise_binop_commut orb orb_comm).
1308
1309Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
1310Proof (bitwise_binop_assoc orb orb_assoc).
1311
1312Theorem or_zero: forall x, or x zero = x.
1313Proof.
1314  intros. unfold or, bitwise_binop.
1315  transitivity (repr(unsigned x)).
1316  apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
1317  apply eqm_refl2. apply Z_of_bits_exten. intros.
1318  rewrite unsigned_zero. rewrite bits_of_Z_zero. apply orb_b_false.
1319  apply repr_unsigned.
1320Qed.
1321
1322Theorem or_mone: forall x, or x mone = mone.
1323Proof.
1324  intros. unfold or, bitwise_binop.
1325  transitivity (repr(unsigned mone)).
1326  apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
1327  apply eqm_refl2. apply Z_of_bits_exten. intros.
1328  rewrite unsigned_mone. rewrite bits_of_Z_mone. apply orb_b_true. auto.
1329  apply repr_unsigned.
1330Qed.
1331
1332Theorem or_idem: forall x, or x x = x.
1333Proof.
1334  assert (forall b, b || b = b).
1335    destruct b; reflexivity.
1336  exact (bitwise_binop_idem orb H).
1337Qed.
1338
1339Theorem and_or_distrib:
1340  forall x y z,
1341  and x (or y z) = or (and x y) (and x z).
1342Proof.
1343  intros; unfold and, or, bitwise_binop.
1344  decEq. repeat rewrite unsigned_repr; auto with ints.
1345  apply Z_of_bits_exten; intros.
1346  repeat rewrite bits_of_Z_of_bits; auto.
1347  apply demorgan1.
1348Qed. 
1349
1350Theorem xor_commut: forall x y, xor x y = xor y x.
1351Proof (bitwise_binop_commut xorb xorb_comm).
1352
1353Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
1354Proof.
1355  assert (forall a b c, xorb a (xorb b c) = xorb (xorb a b) c).
1356  symmetry. apply xorb_assoc.
1357  exact (bitwise_binop_assoc xorb H).
1358Qed.
1359
1360Theorem xor_zero: forall x, xor x zero = x.
1361Proof.
1362  intros. unfold xor, bitwise_binop.
1363  transitivity (repr(unsigned x)).
1364  apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
1365  apply eqm_refl2. apply Z_of_bits_exten. intros.
1366  rewrite unsigned_zero. rewrite bits_of_Z_zero. apply xorb_false.
1367  apply repr_unsigned.
1368Qed.
1369
1370Theorem xor_idem: forall x, xor x x = zero.
1371Proof.
1372  intros. unfold xor, bitwise_binop.
1373  transitivity (repr(unsigned zero)).
1374  apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
1375  apply eqm_refl2. apply Z_of_bits_exten. intros.
1376  rewrite unsigned_zero. rewrite bits_of_Z_zero. apply xorb_nilpotent.
1377  apply repr_unsigned.
1378Qed.
1379
1380Theorem xor_zero_one: xor zero one = one.
1381Proof. rewrite xor_commut. apply xor_zero. Qed.
1382
1383Theorem xor_one_one: xor one one = zero.
1384Proof. apply xor_idem. Qed.
1385
1386Theorem and_xor_distrib:
1387  forall x y z,
1388  and x (xor y z) = xor (and x y) (and x z).
1389Proof.
1390  intros; unfold and, xor, bitwise_binop.
1391  decEq. repeat rewrite unsigned_repr; auto with ints.
1392  apply Z_of_bits_exten; intros.
1393  repeat rewrite bits_of_Z_of_bits; auto.
1394  assert (forall a b c, a && (xorb b c) = xorb (a && b) (a && c)).
1395    destruct a; destruct b; destruct c; reflexivity.
1396  auto.
1397Qed. 
1398
1399Theorem not_involutive:
1400  forall (x: int), not (not x) = x.
1401Proof.
1402  intros. unfold not. rewrite xor_assoc. rewrite xor_idem. apply xor_zero.
1403Qed.
1404
1405(** ** Properties of shifts and rotates *)
1406
1407Lemma Z_of_bits_shift:
1408  forall n f,
1409  exists k,
1410  Z_of_bits n (fun i => f (i - 1)) =
1411    k * two_power_nat n + Z_shift_add (f (-1)) (Z_of_bits n f).
1412Proof.
1413  induction n; intros.
1414  simpl. rewrite two_power_nat_O. unfold Z_shift_add.
1415  exists (if f (-1) then (-1) else 0).
1416  destruct (f (-1)); omega.
1417  rewrite two_power_nat_S. simpl.
1418  elim (IHn (fun i => f (i + 1))). intros k' EQ.
1419  replace (Z_of_bits n (fun i => f (i - 1 + 1)))
1420     with (Z_of_bits n (fun i => f (i + 1 - 1))) in EQ.
1421  rewrite EQ.
1422  change (-1 + 1) with 0.
1423  exists k'.
1424  unfold Z_shift_add; destruct (f (-1)); destruct (f 0); ring.
1425  apply Z_of_bits_exten; intros.
1426  decEq. omega.
1427Qed.
1428
1429Lemma Z_of_bits_shifts:
1430  forall m f,
1431  0 <= m ->
1432  (forall i, i < 0 -> f i = false) ->
1433  eqm (Z_of_bits wordsize (fun i => f (i - m)))
1434      (two_p m * Z_of_bits wordsize f).
1435Proof.
1436  intros. pattern m. apply natlike_ind.
1437  apply eqm_refl2. transitivity (Z_of_bits wordsize f).
1438  apply Z_of_bits_exten; intros. decEq. omega.
1439  simpl two_p. omega.
1440  intros. rewrite two_p_S; auto.
1441  set (f' := fun i => f (i - x)).
1442  apply eqm_trans with (Z_of_bits wordsize (fun i => f' (i - 1))).
1443  apply eqm_refl2. apply Z_of_bits_exten; intros.
1444  unfold f'. decEq. omega.
1445  apply eqm_trans with (Z_shift_add (f' (-1)) (Z_of_bits wordsize f')).
1446  exact (Z_of_bits_shift wordsize f').
1447  unfold f'. unfold Z_shift_add. rewrite H0.
1448  rewrite <- Zmult_assoc. apply eqm_mult. apply eqm_refl.
1449  apply H2. omega. assumption.
1450Qed.
1451
1452Lemma shl_mul_two_p:
1453  forall x y,
1454  shl x y = mul x (repr (two_p (unsigned y))).
1455Proof.
1456  intros. unfold shl, mul.
1457  apply eqm_samerepr.
1458  eapply eqm_trans.
1459  apply Z_of_bits_shifts.
1460  generalize (unsigned_range y). omega.
1461  intros; apply bits_of_Z_below; auto.
1462  rewrite Zmult_comm. apply eqm_mult.
1463  apply Z_of_bits_of_Z. apply eqm_unsigned_repr.
1464Qed.
1465
1466Theorem shl_zero: forall x, shl x zero = x.
1467Proof.
1468  intros. rewrite shl_mul_two_p.
1469  change (repr (two_p (unsigned zero))) with one.
1470  apply mul_one.
1471Qed.
1472
1473Theorem shl_mul:
1474  forall x y,
1475  shl x y = mul x (shl one y).
1476Proof.
1477  intros.
1478  assert (shl one y = repr (two_p (unsigned y))).
1479  rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto.
1480  rewrite H. apply shl_mul_two_p.
1481Qed.
1482
1483Lemma ltu_inv:
1484  forall x y, ltu x y = true -> 0 <= unsigned x < unsigned y.
1485Proof.
1486  unfold ltu; intros. destruct (zlt (unsigned x) (unsigned y)).
1487  split; auto. generalize (unsigned_range x); omega.
1488  discriminate.
1489Qed.
1490
1491Theorem shl_rolm:
1492  forall x n,
1493  ltu n iwordsize = true ->
1494  shl x n = rolm x n (shl mone n).
1495Proof.
1496  intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize; intros.
1497  unfold shl, rolm, rol, and, bitwise_binop.
1498  decEq. apply Z_of_bits_exten; intros.
1499  repeat rewrite unsigned_repr; auto with ints.
1500  repeat rewrite bits_of_Z_of_bits; auto.
1501  case (zlt z (unsigned n)); intro LT2.
1502  assert (z - unsigned n < 0). omega.
1503  rewrite (bits_of_Z_below wordsize (unsigned x) _ H2).
1504  rewrite (bits_of_Z_below wordsize (unsigned mone) _ H2).
1505  symmetry. apply andb_b_false.
1506  assert (z - unsigned n < Z_of_nat wordsize).
1507    generalize (unsigned_range n). omega.
1508  rewrite unsigned_mone.
1509  rewrite bits_of_Z_mone. rewrite andb_b_true. decEq.
1510  rewrite Zmod_small. auto. omega. omega.
1511Qed.
1512
1513Lemma bitwise_binop_shl:
1514  forall f x y n,
1515  f false false = false ->
1516  bitwise_binop f (shl x n) (shl y n) = shl (bitwise_binop f x y) n.
1517Proof.
1518  intros. unfold bitwise_binop, shl.
1519  decEq. repeat rewrite unsigned_repr; auto with ints.
1520  apply Z_of_bits_exten; intros.
1521  case (zlt (z - unsigned n) 0); intro.
1522  transitivity false. repeat rewrite bits_of_Z_of_bits; auto.
1523  repeat rewrite bits_of_Z_below; auto.
1524  rewrite bits_of_Z_below; auto.
1525  repeat rewrite bits_of_Z_of_bits; auto.
1526  generalize (unsigned_range n). omega.
1527Qed.
1528
1529Theorem and_shl:
1530  forall x y n,
1531  and (shl x n) (shl y n) = shl (and x y) n.
1532Proof.
1533  unfold and; intros. apply bitwise_binop_shl. reflexivity.
1534Qed.
1535
1536
1537Theorem shl_shl:
1538  forall x y z,
1539  ltu y iwordsize = true ->
1540  ltu z iwordsize = true ->
1541  ltu (add y z) iwordsize = true ->
1542  shl (shl x y) z = shl x (add y z).
1543Proof.
1544  intros. unfold shl, add.
1545  generalize (ltu_inv _ _ H).
1546  generalize (ltu_inv _ _ H0).
1547  rewrite unsigned_repr_wordsize.
1548  set (x' := unsigned x).
1549  set (y' := unsigned y).
1550  set (z' := unsigned z).
1551  intros.
1552  repeat rewrite unsigned_repr.
1553  decEq. apply Z_of_bits_exten. intros n R.
1554  rewrite bits_of_Z_of_bits'.
1555  destruct (zlt (n - z') 0).
1556  symmetry. apply bits_of_Z_below. omega.
1557  destruct (zle (Z_of_nat wordsize) (n - z')).
1558  symmetry. apply bits_of_Z_below. omega.
1559  decEq. omega.
1560  generalize two_wordsize_max_unsigned; omega.
1561  apply Z_of_bits_range_2.
1562Qed.
1563
1564Theorem shru_shru:
1565  forall x y z,
1566  ltu y iwordsize = true ->
1567  ltu z iwordsize = true ->
1568  ltu (add y z) iwordsize = true ->
1569  shru (shru x y) z = shru x (add y z).
1570Proof.
1571  intros. unfold shru, add.
1572  generalize (ltu_inv _ _ H).
1573  generalize (ltu_inv _ _ H0).
1574  rewrite unsigned_repr_wordsize.
1575  set (x' := unsigned x).
1576  set (y' := unsigned y).
1577  set (z' := unsigned z).
1578  intros.
1579  repeat rewrite unsigned_repr.
1580  decEq. apply Z_of_bits_exten. intros n R.
1581  rewrite bits_of_Z_of_bits'.
1582  destruct (zlt (n + z') 0). omegaContradiction.
1583  destruct (zle (Z_of_nat wordsize) (n + z')).
1584  symmetry. apply bits_of_Z_above. omega.
1585  decEq. omega.
1586  generalize two_wordsize_max_unsigned; omega.
1587  apply Z_of_bits_range_2.
1588Qed.
1589
1590Theorem shru_rolm:
1591  forall x n,
1592  ltu n iwordsize = true ->
1593  shru x n = rolm x (sub iwordsize n) (shru mone n).
1594Proof.
1595  intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize. intro.
1596  unfold shru, rolm, rol, and, bitwise_binop.
1597  decEq. apply Z_of_bits_exten; intros.
1598  repeat rewrite unsigned_repr; auto with ints.
1599  repeat rewrite bits_of_Z_of_bits; auto.
1600  unfold sub. rewrite unsigned_repr_wordsize.
1601  rewrite unsigned_repr.
1602  case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro LT2.
1603  rewrite unsigned_mone. rewrite bits_of_Z_mone. rewrite andb_b_true.
1604  decEq.
1605  replace (z - (Z_of_nat wordsize - unsigned n))
1606     with ((z + unsigned n) + (-1) * Z_of_nat wordsize).
1607  rewrite Z_mod_plus. symmetry. apply Zmod_small.
1608  generalize (unsigned_range n). omega. omega. omega.
1609  generalize (unsigned_range n). omega.
1610  rewrite (bits_of_Z_above wordsize (unsigned x) _ LT2).
1611  rewrite (bits_of_Z_above wordsize (unsigned mone) _ LT2).
1612  symmetry. apply andb_b_false.
1613  split. omega. apply Zle_trans with (Z_of_nat wordsize).
1614  generalize (unsigned_range n); omega. apply wordsize_max_unsigned.
1615Qed.
1616
1617Lemma bitwise_binop_shru:
1618  forall f x y n,
1619  f false false = false ->
1620  bitwise_binop f (shru x n) (shru y n) = shru (bitwise_binop f x y) n.
1621Proof.
1622  intros. unfold bitwise_binop, shru.
1623  decEq. repeat rewrite unsigned_repr; auto with ints.
1624  apply Z_of_bits_exten; intros.
1625  case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro.
1626  repeat rewrite bits_of_Z_of_bits; auto.
1627  generalize (unsigned_range n); omega.
1628  transitivity false. repeat rewrite bits_of_Z_of_bits; auto.
1629  repeat rewrite bits_of_Z_above; auto.
1630  rewrite bits_of_Z_above; auto.
1631Qed.
1632
1633Lemma and_shru:
1634  forall x y n,
1635  and (shru x n) (shru y n) = shru (and x y) n.
1636Proof.
1637  unfold and; intros. apply bitwise_binop_shru. reflexivity.
1638Qed.
1639
1640Theorem shr_shr:
1641  forall x y z,
1642  ltu y iwordsize = true ->
1643  ltu z iwordsize = true ->
1644  ltu (add y z) iwordsize = true ->
1645  shr (shr x y) z = shr x (add y z).
1646Proof.
1647  intros. unfold shr, add.
1648  generalize (ltu_inv _ _ H).
1649  generalize (ltu_inv _ _ H0).
1650  rewrite unsigned_repr_wordsize.
1651  set (x' := signed x).
1652  set (y' := unsigned y).
1653  set (z' := unsigned z).
1654  intros.
1655  rewrite unsigned_repr.
1656  rewrite two_p_is_exp.
1657  rewrite signed_repr.
1658  decEq. apply Zdiv_Zdiv. apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega.
1659  apply Zdiv_interval_2. unfold x'; apply signed_range.
1660  generalize min_signed_neg; omega.
1661  generalize max_signed_pos; omega.
1662  apply two_p_gt_ZERO. omega.  omega. omega.
1663  generalize two_wordsize_max_unsigned; omega.
1664Qed.
1665
1666Theorem rol_zero:
1667  forall x,
1668  rol x zero = x.
1669Proof.
1670  intros. transitivity (repr (unsigned x)).
1671  unfold rol. apply eqm_samerepr. eapply eqm_trans. 2: apply Z_of_bits_of_Z.
1672  apply eqm_refl2. apply Z_of_bits_exten; intros. decEq. rewrite unsigned_zero.
1673  replace (z - 0) with z by omega. apply Zmod_small. auto.
1674  apply repr_unsigned.
1675Qed.
1676
1677Lemma bitwise_binop_rol:
1678  forall f x y n,
1679  bitwise_binop f (rol x n) (rol y n) = rol (bitwise_binop f x y) n.
1680Proof.
1681  intros. unfold bitwise_binop, rol.
1682  decEq. repeat (rewrite unsigned_repr; auto with ints).
1683  apply Z_of_bits_exten; intros.
1684  repeat rewrite bits_of_Z_of_bits; auto.
1685  apply Z_mod_lt. generalize wordsize_pos; omega.
1686Qed.
1687
1688Theorem rol_and:
1689  forall x y n,
1690  rol (and x y) n = and (rol x n) (rol y n).
1691Proof.
1692  intros. symmetry. unfold and. apply bitwise_binop_rol.
1693Qed.
1694
1695Theorem rol_rol:
1696  forall x n m,
1697  Zdivide (Z_of_nat wordsize) modulus ->
1698  rol (rol x n) m = rol x (modu (add n m) iwordsize).
1699Proof.
1700  intros. unfold rol. decEq.
1701  repeat (rewrite unsigned_repr; auto with ints).
1702  apply Z_of_bits_exten; intros.
1703  repeat rewrite bits_of_Z_of_bits; auto.
1704  decEq. unfold modu, add.
1705  set (W := Z_of_nat wordsize).
1706  set (M := unsigned m); set (N := unsigned n).
1707  assert (W > 0). unfold W; generalize wordsize_pos; omega.
1708  assert (forall a, eqmod W a (unsigned (repr a))).
1709    intros. eapply eqmod_divides. apply eqm_unsigned_repr. assumption.
1710  apply eqmod_mod_eq. auto.
1711  replace (unsigned iwordsize) with W.
1712  apply eqmod_trans with (z - (N + M) mod W).
1713  apply eqmod_trans with ((z - M) - N).
1714  apply eqmod_sub. apply eqmod_sym. apply eqmod_mod. auto.
1715  apply eqmod_refl.
1716  replace (z - M - N) with (z - (N + M)).
1717  apply eqmod_sub. apply eqmod_refl. apply eqmod_mod. auto.
1718  omega.
1719  apply eqmod_sub. apply eqmod_refl.
1720  eapply eqmod_trans; [idtac|apply H2].
1721  eapply eqmod_trans; [idtac|apply eqmod_mod].
1722  apply eqmod_sym. eapply eqmod_trans; [idtac|apply eqmod_mod].
1723  apply eqmod_sym. apply H2. auto. auto.
1724  symmetry. unfold W. apply unsigned_repr_wordsize.
1725  apply Z_mod_lt. generalize wordsize_pos; omega.
1726Qed.
1727
1728Theorem rolm_zero:
1729  forall x m,
1730  rolm x zero m = and x m.
1731Proof.
1732  intros. unfold rolm. rewrite rol_zero. auto.
1733Qed.
1734
1735Theorem rolm_rolm:
1736  forall x n1 m1 n2 m2,
1737  Zdivide (Z_of_nat wordsize) modulus ->
1738  rolm (rolm x n1 m1) n2 m2 =
1739    rolm x (modu (add n1 n2) iwordsize)
1740           (and (rol m1 n2) m2).
1741Proof.
1742  intros.
1743  unfold rolm. rewrite rol_and. rewrite and_assoc.
1744  rewrite rol_rol. reflexivity. auto.
1745Qed.
1746
1747Theorem rol_or:
1748  forall x y n,
1749  rol (or x y) n = or (rol x n) (rol y n).
1750Proof.
1751  intros. symmetry. unfold or. apply bitwise_binop_rol.
1752Qed.
1753
1754Theorem or_rolm:
1755  forall x n m1 m2,
1756  or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2).
1757Proof.
1758  intros; unfold rolm. symmetry. apply and_or_distrib.
1759Qed.
1760
1761Theorem ror_rol:
1762  forall x y,
1763  ltu y iwordsize = true ->
1764  ror x y = rol x (sub iwordsize y).
1765Proof.
1766  intros. unfold ror, rol, sub.
1767  generalize (ltu_inv _ _ H).
1768  rewrite unsigned_repr_wordsize.
1769  intro. rewrite unsigned_repr.
1770  decEq. apply Z_of_bits_exten. intros. decEq.
1771  apply eqmod_mod_eq. omega.
1772  exists 1. omega.
1773  generalize wordsize_pos; generalize wordsize_max_unsigned; omega.
1774Qed.
1775
1776Theorem or_ror:
1777  forall x y z,
1778  ltu y iwordsize = true ->
1779  ltu z iwordsize = true ->
1780  add y z = iwordsize ->
1781  ror x z = or (shl x y) (shru x z).
1782Proof.
1783  intros.
1784  generalize (ltu_inv _ _ H).
1785  generalize (ltu_inv _ _ H0).
1786  rewrite unsigned_repr_wordsize.
1787  intros.
1788  unfold or, bitwise_binop, shl, shru, ror.
1789  set (ux := unsigned x).
1790  decEq. apply Z_of_bits_exten. intros i iRANGE.
1791  repeat rewrite unsigned_repr.
1792  repeat rewrite bits_of_Z_of_bits; auto.
1793  assert (y = sub iwordsize z).
1794    rewrite <- H1. rewrite add_commut. rewrite sub_add_l. rewrite sub_idem.
1795    rewrite add_commut. rewrite add_zero. auto.
1796  assert (unsigned y = Z_of_nat wordsize - unsigned z).
1797    rewrite H4. unfold sub. rewrite unsigned_repr_wordsize. apply unsigned_repr.
1798    generalize wordsize_max_unsigned; omega.
1799  destruct (zlt (i + unsigned z) (Z_of_nat wordsize)).
1800  rewrite Zmod_small.
1801  replace (bits_of_Z wordsize ux (i - unsigned y)) with false.
1802  auto.
1803  symmetry. apply bits_of_Z_below. omega. omega.
1804  replace (bits_of_Z wordsize ux (i + unsigned z)) with false.
1805  rewrite orb_false_r. decEq.
1806  replace (i + unsigned z) with (i - unsigned y + 1 * Z_of_nat wordsize) by omega.
1807  rewrite Z_mod_plus. apply Zmod_small. omega. generalize wordsize_pos; omega.
1808  symmetry. apply bits_of_Z_above. auto.
1809  apply Z_of_bits_range_2. apply Z_of_bits_range_2.
1810Qed.
1811
1812Lemma bits_of_Z_two_p:
1813  forall n x i,
1814  x >= 0 -> 0 <= i < Z_of_nat n ->
1815  bits_of_Z n (two_p x - 1) i = zlt i x.
1816Proof.
1817  induction n; intros.
1818  simpl in H0. omegaContradiction.
1819  destruct (zeq x 0). subst x. change (two_p 0 - 1) with 0. rewrite bits_of_Z_zero.
1820  unfold proj_sumbool; rewrite zlt_false. auto. omega.
1821  replace (two_p x) with (2 * two_p (x - 1)). simpl. rewrite Z_bin_decomp_2xm1.
1822  destruct (zeq i 0). subst. unfold proj_sumbool. rewrite zlt_true. auto. omega.
1823  rewrite inj_S in H0. rewrite IHn. unfold proj_sumbool. destruct (zlt i x).
1824  apply zlt_true. omega.
1825  apply zlt_false. omega.
1826  omega. omega. rewrite <- two_p_S. decEq. omega. omega.
1827Qed.
1828
1829Remark two_p_m1_range:
1830  forall n,
1831  0 <= n <= Z_of_nat wordsize ->
1832  0 <= two_p n - 1 <= max_unsigned.
1833Proof.
1834  intros. split.
1835  assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega.
1836  assert (two_p n <= two_p (Z_of_nat wordsize)). apply two_p_monotone. auto.
1837  unfold max_unsigned. unfold modulus. rewrite two_power_nat_two_p. omega.
1838Qed.
1839
1840Theorem shru_shl_and:
1841  forall x y,
1842  ltu y iwordsize = true ->
1843  shru (shl x y) y = and x (repr (two_p (Z_of_nat wordsize - unsigned y) - 1)).
1844Proof.
1845  intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize. intros.
1846  unfold and, bitwise_binop, shl, shru.
1847  decEq. apply Z_of_bits_exten. intros.
1848  repeat rewrite unsigned_repr.
1849  rewrite bits_of_Z_two_p.
1850  destruct (zlt (z + unsigned y) (Z_of_nat wordsize)).
1851  rewrite bits_of_Z_of_bits. unfold proj_sumbool. rewrite zlt_true.
1852  rewrite andb_true_r. f_equal. omega.
1853  omega. omega.
1854  rewrite bits_of_Z_above. unfold proj_sumbool. rewrite zlt_false. rewrite andb_false_r; auto.
1855  omega. omega. omega. auto.
1856  apply two_p_m1_range. omega.
1857  apply Z_of_bits_range_2.
1858Qed.
1859
1860(** ** Relation between shifts and powers of 2 *)
1861
1862Fixpoint powerserie (l: list Z): Z :=
1863  match l with
1864  | nil => 0
1865  | x :: xs => two_p x + powerserie xs
1866  end.
1867
1868Lemma Z_bin_decomp_range:
1869  forall x n,
1870  0 <= x < 2 * n -> 0 <= snd (Z_bin_decomp x) < n.
1871Proof.
1872  intros. rewrite <- (Z_shift_add_bin_decomp x) in H.
1873  unfold Z_shift_add in H. destruct (fst (Z_bin_decomp x)); omega.
1874Qed.
1875
1876Lemma Z_one_bits_powerserie:
1877  forall x, 0 <= x < modulus -> x = powerserie (Z_one_bits wordsize x 0).
1878Proof.
1879  assert (forall n x i,
1880    0 <= i ->
1881    0 <= x < two_power_nat n ->
1882    x * two_p i = powerserie (Z_one_bits n x i)).
1883  induction n; intros.
1884  simpl. rewrite two_power_nat_O in H0.
1885  assert (x = 0). omega. subst x. omega.
1886  rewrite two_power_nat_S in H0. simpl Z_one_bits.
1887  generalize (Z_shift_add_bin_decomp x).
1888  generalize (Z_bin_decomp_range x _ H0).
1889  case (Z_bin_decomp x). simpl. intros b y RANGE SHADD.
1890  subst x. unfold Z_shift_add.
1891  destruct b. simpl powerserie. rewrite <- IHn.
1892  rewrite two_p_is_exp. change (two_p 1) with 2. ring.
1893  auto. omega. omega. auto.
1894  rewrite <- IHn.
1895  rewrite two_p_is_exp. change (two_p 1) with 2. ring.
1896  auto. omega. omega. auto.
1897  intros. rewrite <- H. change (two_p 0) with 1. omega.
1898  omega. exact H0.
1899Qed.
1900
1901Lemma Z_one_bits_range:
1902  forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < Z_of_nat wordsize.
1903Proof.
1904  assert (forall n x i j,
1905    In j (Z_one_bits n x i) -> i <= j < i + Z_of_nat n).
1906  induction n; simpl In.
1907  intros; elim H.
1908  intros x i j. destruct (Z_bin_decomp x). case b.
1909  rewrite inj_S. simpl. intros [A|B]. subst j. omega.
1910  generalize (IHn _ _ _ B). omega.
1911  intros B. rewrite inj_S. generalize (IHn _ _ _ B). omega.
1912  intros. generalize (H wordsize x 0 i H0). omega.
1913Qed.
1914
1915Lemma is_power2_rng:
1916  forall n logn,
1917  is_power2 n = Some logn ->
1918  0 <= unsigned logn < Z_of_nat wordsize.
1919Proof.
1920  intros n logn. unfold is_power2.
1921  generalize (Z_one_bits_range (unsigned n)).
1922  destruct (Z_one_bits wordsize (unsigned n) 0).
1923  intros; discriminate.
1924  destruct l.
1925  intros. injection H0; intro; subst logn; clear H0.
1926  assert (0 <= z < Z_of_nat wordsize).
1927  apply H. auto with coqlib.
1928  rewrite unsigned_repr. auto. generalize wordsize_max_unsigned; omega.
1929  intros; discriminate.
1930Qed.
1931
1932Theorem is_power2_range:
1933  forall n logn,
1934  is_power2 n = Some logn -> ltu logn iwordsize = true.
1935Proof.
1936  intros. unfold ltu. rewrite unsigned_repr_wordsize.
1937  generalize (is_power2_rng _ _ H).
1938  case (zlt (unsigned logn) (Z_of_nat wordsize)); intros.
1939  auto. omegaContradiction.
1940Qed.
1941
1942Lemma is_power2_correct:
1943  forall n logn,
1944  is_power2 n = Some logn ->
1945  unsigned n = two_p (unsigned logn).
1946Proof.
1947  intros n logn. unfold is_power2.
1948  generalize (Z_one_bits_powerserie (unsigned n) (unsigned_range n)).
1949  generalize (Z_one_bits_range (unsigned n)).
1950  destruct (Z_one_bits wordsize (unsigned n) 0).
1951  intros; discriminate.
1952  destruct l.
1953  intros. simpl in H0. injection H1; intros; subst logn; clear H1.
1954  rewrite unsigned_repr. replace (two_p z) with (two_p z + 0).
1955  auto. omega. elim (H z); intros.
1956  generalize wordsize_max_unsigned; omega.
1957  auto with coqlib.
1958  intros; discriminate.
1959Qed.
1960
1961Remark two_p_range:
1962  forall n,
1963  0 <= n < Z_of_nat wordsize ->
1964  0 <= two_p n <= max_unsigned.
1965Proof.
1966  intros. split.
1967  assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega.
1968  generalize (two_p_monotone_strict _ _ H). rewrite <- two_power_nat_two_p.
1969  unfold max_unsigned, modulus. omega.
1970Qed.
1971
1972Remark Z_one_bits_zero:
1973  forall n i, Z_one_bits n 0 i = nil.
1974Proof.
1975  induction n; intros; simpl; auto.
1976Qed.
1977
1978Remark Z_one_bits_two_p:
1979  forall n x i,
1980  0 <= x < Z_of_nat n ->
1981  Z_one_bits n (two_p x) i = (i + x) :: nil.
1982Proof.
1983  induction n; intros; simpl. simpl in H. omegaContradiction.
1984  rewrite inj_S in H.
1985  assert (x = 0 \/ 0 < x) by omega. destruct H0.
1986  subst x; simpl. decEq. omega. apply Z_one_bits_zero.
1987  replace (two_p x) with (Z_shift_add false (two_p (x-1))).
1988  rewrite Z_bin_decomp_shift_add.
1989  replace (i + x) with ((i + 1) + (x - 1)) by omega.
1990  apply IHn. omega.
1991  unfold Z_shift_add. rewrite <- two_p_S. decEq; omega. omega.
1992Qed.
1993
1994Lemma is_power2_two_p:
1995  forall n, 0 <= n < Z_of_nat wordsize ->
1996  is_power2 (repr (two_p n)) = Some (repr n).
1997Proof.
1998  intros. unfold is_power2. rewrite unsigned_repr.
1999  rewrite Z_one_bits_two_p. auto. auto.
2000  apply two_p_range. auto.
2001Qed.
2002
2003Theorem mul_pow2:
2004  forall x n logn,
2005  is_power2 n = Some logn ->
2006  mul x n = shl x logn.
2007Proof.
2008  intros. generalize (is_power2_correct n logn H); intro.
2009  rewrite shl_mul_two_p. rewrite <- H0. rewrite repr_unsigned.
2010  auto.
2011Qed.
2012
2013Lemma Z_of_bits_shift_rev:
2014  forall n f,
2015  (forall i, i >= Z_of_nat n -> f i = false) ->
2016  Z_of_bits n f = Z_shift_add (f 0) (Z_of_bits n (fun i => f(i + 1))).
2017Proof.
2018  induction n; intros.
2019  simpl. rewrite H. reflexivity. unfold Z_of_nat. omega.
2020  simpl. rewrite (IHn (fun i => f (i + 1))).
2021  reflexivity.
2022  intros. apply H. rewrite inj_S. omega.
2023Qed.
2024
2025Lemma Z_of_bits_shifts_rev:
2026  forall m f,
2027  0 <= m ->
2028  (forall i, i >= Z_of_nat wordsize -> f i = false) ->
2029  exists k,
2030  Z_of_bits wordsize f = k + two_p m * Z_of_bits wordsize (fun i => f(i + m))
2031  /\ 0 <= k < two_p m.
2032Proof.
2033  intros. pattern m. apply natlike_ind.
2034  exists 0. change (two_p 0) with 1. split.
2035  transitivity (Z_of_bits wordsize (fun i => f (i + 0))).
2036  apply Z_of_bits_exten. intros. decEq. omega.
2037  omega. omega.
2038  intros x POSx [k [EQ1 RANGE1]].
2039  set (f' := fun i => f (i + x)) in *.
2040  assert (forall i, i >= Z_of_nat wordsize -> f' i = false).
2041  intros. unfold f'. apply H0. omega. 
2042  generalize (Z_of_bits_shift_rev wordsize f' H1). intro.
2043  rewrite EQ1. rewrite H2.
2044  set (z := Z_of_bits wordsize (fun i => f (i + Zsucc x))).
2045  replace (Z_of_bits wordsize (fun i => f' (i + 1))) with z.
2046  rewrite two_p_S.
2047  case (f' 0); unfold Z_shift_add.
2048  exists (k + two_p x). split. ring. omega.
2049  exists k. split. ring. omega.
2050  auto.
2051  unfold z. apply Z_of_bits_exten; intros. unfold f'.
2052  decEq. omega.
2053  auto.
2054Qed.
2055
2056Lemma shru_div_two_p:
2057  forall x y,
2058  shru x y = repr (unsigned x / two_p (unsigned y)).
2059Proof.
2060  intros. unfold shru.
2061  set (x' := unsigned x). set (y' := unsigned y).
2062  elim (Z_of_bits_shifts_rev y' (bits_of_Z wordsize x')).
2063  intros k [EQ RANGE].
2064  replace (Z_of_bits wordsize (bits_of_Z wordsize x')) with x' in EQ.
2065  rewrite Zplus_comm in EQ. rewrite Zmult_comm in EQ.
2066  generalize (Zdiv_unique _ _ _ _ EQ RANGE). intros.
2067  rewrite H. auto.
2068  apply eqm_small_eq. apply eqm_sym. apply Z_of_bits_of_Z.
2069  unfold x'. apply unsigned_range.
2070  auto with ints.
2071  generalize (unsigned_range y). unfold y'. omega.
2072  intros. apply bits_of_Z_above. auto.
2073Qed.
2074
2075Theorem shru_zero:
2076  forall x, shru x zero = x.
2077Proof.
2078  intros. rewrite shru_div_two_p. change (two_p (unsigned zero)) with 1.
2079  transitivity (repr (unsigned x)). decEq. apply Zdiv_unique with 0.
2080  omega. omega. auto with ints.
2081Qed.
2082
2083Theorem shr_zero:
2084  forall x, shr x zero = x.
2085Proof.
2086  intros. unfold shr. change (two_p (unsigned zero)) with 1.
2087  replace (signed x / 1) with (signed x).
2088  apply repr_signed.
2089  symmetry. apply Zdiv_unique with 0. omega. omega.
2090Qed.
2091
2092Theorem divu_pow2:
2093  forall x n logn,
2094  is_power2 n = Some logn ->
2095  divu x n = shru x logn.
2096Proof.
2097  intros. generalize (is_power2_correct n logn H). intro.
2098  symmetry. unfold divu. rewrite H0. apply shru_div_two_p.
2099Qed.
2100
2101Lemma modu_divu_Euclid:
2102  forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y).
2103Proof.
2104  intros. unfold add, mul, divu, modu.
2105  transitivity (repr (unsigned x)). auto with ints.
2106  apply eqm_samerepr.
2107  set (x' := unsigned x). set (y' := unsigned y).
2108  apply eqm_trans with ((x' / y') * y' + x' mod y').
2109  apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq.
2110  generalize (unsigned_range y); intro.
2111  assert (unsigned y <> 0). red; intro.
2112  elim H. rewrite <- (repr_unsigned y). unfold zero. congruence.
2113  unfold y'. omega.
2114  auto with ints.
2115Qed.
2116
2117Theorem modu_divu:
2118  forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y).
2119Proof.
2120  intros.
2121  assert (forall a b c, a = add b c -> c = sub a b).
2122  intros. subst a. rewrite sub_add_l. rewrite sub_idem.
2123  rewrite add_commut. rewrite add_zero. auto.
2124  apply H0. apply modu_divu_Euclid. auto.
2125Qed.
2126
2127Theorem mods_divs:
2128  forall x y, mods x y = sub x (mul (divs x y) y).
2129Proof.
2130  intros; unfold mods, sub, mul, divs.
2131  apply eqm_samerepr.
2132  unfold Zmod_round.
2133  apply eqm_sub. apply eqm_signed_unsigned.
2134  apply eqm_unsigned_repr_r.
2135  apply eqm_mult. auto with ints. apply eqm_signed_unsigned.
2136Qed.
2137
2138Theorem divs_pow2:
2139  forall x n logn,
2140  is_power2 n = Some logn ->
2141  divs x n = shrx x logn.
2142Proof.
2143  intros. generalize (is_power2_correct _ _ H); intro.
2144  unfold shrx. rewrite shl_mul_two_p.
2145  rewrite mul_commut. rewrite mul_one.
2146  rewrite <- H0. rewrite repr_unsigned. auto.
2147Qed.
2148
2149Theorem shrx_carry:
2150  forall x y,
2151  add (shr x y) (shr_carry x y) = shrx x y.
2152Proof.
2153  intros. unfold shr_carry.
2154  rewrite sub_add_opp. rewrite add_permut.
2155  rewrite add_neg_zero. apply add_zero.
2156Qed.
2157
2158Lemma Zdiv_round_Zdiv:
2159  forall x y,
2160  y > 0 ->
2161  Zdiv_round x y = if zlt x 0 then (x + y - 1) / y else x / y.
2162Proof.
2163  intros. unfold Zdiv_round.
2164  destruct (zlt x 0).
2165  rewrite zlt_false; try omega.
2166  generalize (Z_div_mod_eq (-x) y H).
2167  generalize (Z_mod_lt (-x) y H).
2168  set (q := (-x) / y). set (r := (-x) mod y). intros.
2169  symmetry.
2170  apply Zdiv_unique with (y - r - 1).
2171  replace x with (- (y * q) - r) by omega.
2172  replace (-(y * q)) with ((-q) * y) by ring.
2173  omega.
2174  omega.
2175  apply zlt_false. omega.
2176Qed.
2177
2178Theorem shrx_shr:
2179  forall x y,
2180  ltu y (repr (Z_of_nat wordsize - 1)) = true ->
2181  shrx x y =
2182  shr (if lt x zero then add x (sub (shl one y) one) else x) y.
2183Proof.
2184  intros. unfold shrx, divs, shr. decEq.
2185  exploit ltu_inv; eauto. rewrite unsigned_repr.   
2186  set (uy := unsigned y).
2187  intro RANGE.
2188  assert (shl one y = repr (two_p uy)).
2189    transitivity (mul one (repr (two_p uy))).
2190    symmetry. apply mul_pow2. replace y with (repr uy).
2191    apply is_power2_two_p. omega. unfold uy. apply repr_unsigned.
2192    rewrite mul_commut. apply mul_one.
2193  assert (two_p uy > 0). apply two_p_gt_ZERO. omega.
2194  assert (two_p uy < half_modulus).
2195    rewrite half_modulus_power.
2196    apply two_p_monotone_strict. auto.
2197  assert (two_p uy < modulus).
2198    rewrite modulus_power. apply two_p_monotone_strict. omega.
2199  assert (unsigned (shl one y) = two_p uy).
2200    rewrite H0. apply unsigned_repr. unfold max_unsigned. omega.
2201  assert (signed (shl one y) = two_p uy).
2202    rewrite H0. apply signed_repr.
2203    unfold max_signed. generalize min_signed_neg. omega.
2204  rewrite H5.
2205  rewrite Zdiv_round_Zdiv; auto.
2206  unfold lt. rewrite signed_zero. 
2207  destruct (zlt (signed x) 0); auto.
2208  rewrite add_signed.
2209  assert (signed (sub (shl one y) one) = two_p uy - 1).
2210    unfold sub. rewrite H4. rewrite unsigned_one. 
2211    apply signed_repr.
2212    generalize min_signed_neg. unfold max_signed. omega.
2213  rewrite H6. rewrite signed_repr. decEq. omega.
2214  generalize (signed_range x). intros. 
2215  assert (two_p uy - 1 <= max_signed). unfold max_signed. omega.
2216  omega.
2217  generalize wordsize_pos wordsize_max_unsigned; omega.
2218Qed.
2219
2220Lemma add_and:
2221  forall x y z,
2222  and y z = zero ->
2223  add (and x y) (and x z) = and x (or y z).
2224Proof.
2225  intros. unfold add, and, bitwise_binop.
2226  decEq.
2227  repeat rewrite unsigned_repr; auto with ints.
2228  apply Z_of_bits_excl; intros.
2229  assert (forall a b c, a && b && (a && c) = a && (b && c)).
2230    destruct a; destruct b; destruct c; reflexivity.
2231  rewrite H1.
2232  replace (bits_of_Z wordsize (unsigned y) i &&
2233           bits_of_Z wordsize (unsigned z) i)
2234     with (bits_of_Z wordsize (unsigned (and y z)) i).
2235  rewrite H. change (unsigned zero) with 0.
2236  rewrite bits_of_Z_zero. apply andb_b_false.
2237  unfold and, bitwise_binop.
2238  rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits.
2239  reflexivity. auto.
2240  rewrite <- demorgan1.
2241  unfold or, bitwise_binop.
2242  rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits; auto.
2243Qed.
2244
2245Lemma Z_of_bits_zero:
2246  forall n f,
2247  (forall i, i >= 0 -> f i = false) ->
2248  Z_of_bits n f = 0.
2249Proof.
2250  induction n; intros; simpl.
2251  auto.
2252  rewrite H. rewrite IHn. auto.  intros. apply H. omega. omega.
2253Qed.
2254
2255Lemma Z_of_bits_trunc_1:
2256  forall n f k,
2257  (forall i, i >= k -> f i = false) ->
2258  k >= 0 ->
2259  0 <= Z_of_bits n f < two_p k.
2260Proof.
2261  induction n; intros.
2262  simpl. assert (two_p k > 0). apply two_p_gt_ZERO; omega. omega.
2263  destruct (zeq k 0). subst k.
2264  change (two_p 0) with 1. rewrite Z_of_bits_zero. omega. auto.
2265  simpl. replace (two_p k) with (2 * two_p (k - 1)).
2266  assert (0 <= Z_of_bits n (fun i => f(i+1)) < two_p (k - 1)).
2267    apply IHn. intros. apply H. omega. omega.
2268  unfold Z_shift_add. destruct (f 0); omega.
2269  rewrite <- two_p_S. decEq. omega. omega.
2270Qed.
2271
2272Lemma Z_of_bits_trunc_2:
2273  forall n f1 f2 k,
2274  (forall i, i < k -> f2 i = f1 i) ->
2275  k >= 0 ->
2276  exists q, Z_of_bits n f1 = q * two_p k + Z_of_bits n f2.
2277Proof.
2278  induction n; intros.
2279  simpl. exists 0; omega.
2280  destruct (zeq k 0). subst k.
2281  exists (Z_of_bits (S n) f1 - Z_of_bits (S n) f2).
2282  change (two_p 0) with 1. omega.
2283  destruct (IHn (fun i => f1 (i + 1)) (fun i => f2 (i + 1)) (k - 1)) as [q EQ].
2284  intros. apply H. omega. omega.
2285  exists q. simpl. rewrite H. unfold Z_shift_add.
2286  replace (two_p k) with (2 * two_p (k - 1)). rewrite EQ.
2287  destruct (f1 0). ring. ring.
2288  rewrite <- two_p_S. decEq. omega. omega. omega.
2289Qed.
2290
2291Lemma Z_of_bits_trunc_3:
2292  forall f n k,
2293  k >= 0 ->
2294  Zmod (Z_of_bits n f) (two_p k) = Z_of_bits n (fun i => if zlt i k then f i else false).
2295Proof.
2296  intros.
2297  set (g := fun i : Z => if zlt i k then f i else false).
2298  destruct (Z_of_bits_trunc_2 n f g k).
2299    intros. unfold g. apply zlt_true. auto.
2300    auto.
2301  apply Zmod_unique with x. auto.
2302  apply Z_of_bits_trunc_1. intros. unfold g. apply zlt_false. auto. auto.
2303Qed.
2304
2305Theorem modu_and:
2306  forall x n logn,
2307  is_power2 n = Some logn ->
2308  modu x n = and x (sub n one).
2309Proof.
2310  intros. generalize (is_power2_correct _ _ H); intro.
2311  generalize (is_power2_rng _ _ H); intro.
2312  unfold modu, and, bitwise_binop.
2313  decEq.
2314  set (ux := unsigned x).
2315  replace ux with (Z_of_bits wordsize (bits_of_Z wordsize ux)).
2316  rewrite H0. rewrite Z_of_bits_trunc_3. apply Z_of_bits_exten. intros.
2317  rewrite bits_of_Z_of_bits; auto.
2318  replace (unsigned (sub n one)) with (two_p (unsigned logn) - 1).
2319  rewrite bits_of_Z_two_p. unfold proj_sumbool.
2320  destruct (zlt z (unsigned logn)). rewrite andb_true_r; auto. rewrite andb_false_r; auto.
2321  omega. auto.
2322  rewrite <- H0. unfold sub. symmetry. rewrite unsigned_one. apply unsigned_repr.
2323  rewrite H0.
2324  assert (two_p (unsigned logn) > 0). apply two_p_gt_ZERO. omega.
2325  generalize (two_p_range _ H1). omega.
2326  omega.
2327  apply eqm_small_eq. apply Z_of_bits_of_Z. apply Z_of_bits_range.
2328  unfold ux. apply unsigned_range.
2329Qed.
2330
2331(** ** Properties of integer zero extension and sign extension. *)
2332
2333Section EXTENSIONS.
2334
2335Variable n: Z.
2336Hypothesis RANGE: 0 < n < Z_of_nat wordsize.
2337
2338Remark two_p_n_pos:
2339  two_p n > 0.
2340Proof. apply two_p_gt_ZERO. omega. Qed.
2341
2342Remark two_p_n_range:
2343  0 <= two_p n <= max_unsigned.
2344Proof. apply two_p_range. omega. Qed.
2345
2346Remark two_p_n_range':
2347  two_p n <= max_signed + 1.
2348Proof.
2349  unfold max_signed. rewrite half_modulus_power.
2350  assert (two_p n <= two_p (Z_of_nat wordsize - 1)).
2351  apply two_p_monotone. omega.
2352  omega.
2353Qed.
2354
2355Remark unsigned_repr_two_p:
2356  unsigned (repr (two_p n)) = two_p n.
2357Proof.
2358  apply unsigned_repr. apply two_p_n_range.
2359Qed.
2360
2361Theorem zero_ext_and:
2362  forall x, zero_ext n x = and x (repr (two_p n - 1)).
2363Proof.
2364  intros; unfold zero_ext.
2365  assert (is_power2 (repr (two_p n)) = Some (repr n)).
2366    apply is_power2_two_p. omega.
2367  generalize (modu_and x _ _ H).
2368  unfold modu. rewrite unsigned_repr_two_p. intro. rewrite H0.
2369  decEq. unfold sub. decEq. rewrite unsigned_repr_two_p.
2370  rewrite unsigned_one. reflexivity.
2371Qed.
2372
2373Theorem zero_ext_idem:
2374  forall x, zero_ext n (zero_ext n x) = zero_ext n x.
2375Proof.
2376  intros. repeat rewrite zero_ext_and.
2377  rewrite and_assoc. rewrite and_idem. auto.
2378Qed.
2379
2380Lemma eqm_eqmod_two_p:
2381  forall a b, eqm a b -> eqmod (two_p n) a b.
2382Proof.
2383  intros a b [k EQ].
2384  exists (k * two_p (Z_of_nat wordsize - n)).
2385  rewrite EQ. decEq. rewrite <- Zmult_assoc. decEq.
2386  rewrite <- two_p_is_exp. unfold modulus. rewrite two_power_nat_two_p.
2387  decEq. omega. omega. omega.
2388Qed.
2389
2390Lemma sign_ext_charact:
2391  forall x y,
2392  -(two_p (n-1)) <= signed y < two_p (n-1) ->
2393  eqmod (two_p n) (unsigned x) (signed y) ->
2394  sign_ext n x = y.
2395Proof.
2396  intros. unfold sign_ext. set (x' := unsigned x) in *.
2397  destruct H0 as [k EQ].
2398  assert (two_p n = 2 * two_p (n - 1)). rewrite <- two_p_S. decEq. omega. omega.
2399  assert (signed y >= 0 \/ signed y < 0) by omega. destruct H1.
2400  assert (x' mod two_p n = signed y).
2401  apply Zmod_unique with k; auto. omega.
2402  rewrite zlt_true. rewrite H2. apply repr_signed. omega.
2403  assert (x' mod two_p n = signed y + two_p n).
2404  apply Zmod_unique with (k-1). rewrite EQ. ring. omega.
2405  rewrite zlt_false. replace (x' mod two_p n - two_p n) with (signed y) by omega. apply repr_signed.
2406  omega.
2407Qed.
2408
2409Lemma zero_ext_eqmod_two_p:
2410  forall x y,
2411  eqmod (two_p n) (unsigned x) (unsigned y) -> zero_ext n x = zero_ext n y.
2412Proof.
2413  intros. unfold zero_ext. decEq. apply eqmod_mod_eq. apply two_p_n_pos. auto.
2414Qed.
2415
2416Lemma sign_ext_eqmod_two_p:
2417  forall x y,
2418  eqmod (two_p n) (unsigned x) (unsigned y) -> sign_ext n x = sign_ext n y.
2419Proof.
2420  intros. unfold sign_ext.
2421  assert (unsigned x mod two_p n = unsigned y mod two_p n).
2422  apply eqmod_mod_eq. apply two_p_n_pos. auto.
2423  rewrite H0. auto.
2424Qed.
2425
2426Lemma eqmod_two_p_zero_ext:
2427  forall x, eqmod (two_p n) (unsigned x) (unsigned (zero_ext n x)).
2428Proof.
2429  intros. unfold zero_ext.
2430  apply eqmod_trans with (unsigned x mod two_p n).
2431  apply eqmod_mod. apply two_p_n_pos.
2432  apply eqm_eqmod_two_p. apply eqm_unsigned_repr.
2433Qed.
2434
2435Lemma eqmod_two_p_sign_ext:
2436  forall x, eqmod (two_p n) (unsigned x) (unsigned (sign_ext n x)).
2437Proof.
2438  intros. unfold sign_ext. destruct (zlt (unsigned x mod two_p n) (two_p (n-1))).
2439  apply eqmod_trans with (unsigned x mod two_p n).
2440  apply eqmod_mod. apply two_p_n_pos.
2441  apply eqm_eqmod_two_p. apply eqm_unsigned_repr.
2442  apply eqmod_trans with (unsigned x mod two_p n).
2443  apply eqmod_mod. apply two_p_n_pos.
2444  apply eqmod_trans with (unsigned x mod two_p n - 0).
2445  apply eqmod_refl2. omega.
2446  apply eqmod_trans with (unsigned x mod two_p n - two_p n).
2447  apply eqmod_sub. apply eqmod_refl. exists (-1). ring.
2448  apply eqm_eqmod_two_p. apply eqm_unsigned_repr.
2449Qed.
2450
2451Theorem sign_ext_idem:
2452  forall x, sign_ext n (sign_ext n x) = sign_ext n x.
2453Proof.
2454  intros. apply sign_ext_eqmod_two_p.
2455  apply eqmod_sym. apply eqmod_two_p_sign_ext.
2456Qed.
2457*)
2458naxiom sign_ext_zero_ext:
2459  ∀n:Z.∀RANGE: 0 < n ∧ n < wordsize.∀x. sign_ext n (zero_ext n x) = sign_ext n x.
2460(*
2461Theorem sign_ext_zero_ext:
2462  forall x, sign_ext n (zero_ext n x) = sign_ext n x.
2463Proof.
2464  intros. apply sign_ext_eqmod_two_p.
2465  apply eqmod_sym. apply eqmod_two_p_zero_ext.
2466Qed.
2467
2468Theorem zero_ext_sign_ext:
2469  forall x, zero_ext n (sign_ext n x) = zero_ext n x.
2470Proof.
2471  intros. apply zero_ext_eqmod_two_p.
2472  apply eqmod_sym. apply eqmod_two_p_sign_ext.
2473Qed.
2474*)
2475naxiom sign_ext_equal_if_zero_equal:
2476  ∀n:Z.∀RANGE: 0 < n ∧ n < wordsize.∀x,y.
2477  zero_ext n x = zero_ext n y ->
2478  sign_ext n x = sign_ext n y.
2479(*
2480Theorem sign_ext_equal_if_zero_equal:
2481  forall x y,
2482  zero_ext n x = zero_ext n y ->
2483  sign_ext n x = sign_ext n y.
2484Proof.
2485  intros. rewrite <- (sign_ext_zero_ext x).
2486  rewrite <- (sign_ext_zero_ext y). congruence.
2487Qed.
2488
2489Lemma eqmod_mult_div:
2490  forall n1 n2 x y,
2491  0 <= n1 -> 0 <= n2 ->
2492  eqmod (two_p (n1+n2)) (two_p n1 * x) y ->
2493  eqmod (two_p n2) x (y / two_p n1).
2494Proof.
2495  intros. rewrite two_p_is_exp in H1; auto.
2496  destruct H1 as [k EQ]. exists k.
2497  change x with (0 / two_p n1 + x). rewrite <- Z_div_plus.
2498  replace (0 + x * two_p n1) with (two_p n1 * x) by ring.
2499  rewrite EQ.
2500  replace (k * (two_p n1 * two_p n2) + y) with (y + (k * two_p n2) * two_p n1) by ring.
2501  rewrite Z_div_plus. ring.
2502  apply two_p_gt_ZERO; auto.
2503  apply two_p_gt_ZERO; auto.
2504Qed.
2505
2506Theorem sign_ext_shr_shl:
2507  forall x,
2508  let y := repr (Z_of_nat wordsize - n) in
2509  sign_ext n x = shr (shl x y) y.
2510Proof.
2511  intros.
2512  assert (unsigned y = Z_of_nat wordsize - n).
2513    unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega.
2514  apply sign_ext_charact.
2515  (* inequalities *)
2516  unfold shr. rewrite H.
2517  set (z := signed (shl x y)).
2518  rewrite signed_repr.
2519  apply Zdiv_interval_1.
2520  assert (two_p (n - 1) > 0). apply two_p_gt_ZERO. omega. omega.
2521  apply two_p_gt_ZERO. omega.
2522  apply two_p_gt_ZERO. omega.
2523  replace ((- two_p (n-1)) * two_p (Z_of_nat wordsize - n))
2524     with (- (two_p (n-1) * two_p (Z_of_nat wordsize - n))) by ring.
2525  rewrite <- two_p_is_exp.
2526  replace (n - 1 + (Z_of_nat wordsize - n)) with (Z_of_nat wordsize - 1) by omega.
2527  rewrite <- half_modulus_power.
2528  generalize (signed_range (shl x y)). unfold z, min_signed, max_signed. omega.
2529  omega. omega.
2530  apply Zdiv_interval_2. unfold z. apply signed_range.
2531  generalize min_signed_neg; omega. generalize max_signed_pos; omega.
2532  apply two_p_gt_ZERO; omega.
2533  (* eqmod *)
2534  unfold shr. rewrite H.
2535  apply eqmod_trans with (signed (shl x y) / two_p (Z_of_nat wordsize - n)).
2536  apply eqmod_mult_div. omega. omega.
2537  replace (Z_of_nat wordsize - n + n) with (Z_of_nat wordsize) by omega.
2538  rewrite <- two_power_nat_two_p.
2539  change (eqm (two_p (Z_of_nat wordsize - n) * unsigned x) (signed (shl x y))).
2540  rewrite shl_mul_two_p. unfold mul. rewrite H.
2541  apply eqm_sym. eapply eqm_trans. apply eqm_signed_unsigned.
2542  apply eqm_unsigned_repr_l. rewrite (Zmult_comm (unsigned x)).
2543  apply eqm_mult. apply eqm_sym. apply eqm_unsigned_repr. apply eqm_refl.
2544  apply eqm_eqmod_two_p. apply eqm_sym. eapply eqm_trans.
2545  apply eqm_signed_unsigned. apply eqm_sym. apply eqm_unsigned_repr.
2546Qed.
2547
2548Theorem zero_ext_shru_shl:
2549  forall x,
2550  let y := repr (Z_of_nat wordsize - n) in
2551  zero_ext n x = shru (shl x y) y.
2552Proof.
2553  intros.
2554  assert (unsigned y = Z_of_nat wordsize - n).
2555    unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega.
2556  rewrite zero_ext_and. symmetry.
2557  replace n with (Z_of_nat wordsize - unsigned y).
2558  apply shru_shl_and. unfold ltu. apply zlt_true.
2559  rewrite H. rewrite unsigned_repr_wordsize. omega. omega.
2560Qed.
2561
2562End EXTENSIONS.
2563
2564(** ** Properties of [one_bits] (decomposition in sum of powers of two) *)
2565
2566Opaque Z_one_bits. (* Otherwise, next Qed blows up! *)
2567
2568Theorem one_bits_range:
2569  forall x i, In i (one_bits x) -> ltu i iwordsize = true.
2570Proof.
2571  intros. unfold one_bits in H.
2572  elim (list_in_map_inv _ _ _ H). intros i0 [EQ IN].
2573  subst i. unfold ltu. unfold iwordsize. apply zlt_true.
2574  generalize (Z_one_bits_range _ _ IN). intros.
2575  assert (0 <= Z_of_nat wordsize <= max_unsigned).
2576    generalize wordsize_pos wordsize_max_unsigned; omega.
2577  repeat rewrite unsigned_repr; omega.
2578Qed.
2579
2580Fixpoint int_of_one_bits (l: list int) : int :=
2581  match l with
2582  | nil => zero
2583  | a :: b => add (shl one a) (int_of_one_bits b)
2584  end.
2585
2586Theorem one_bits_decomp:
2587  forall x, x = int_of_one_bits (one_bits x).
2588Proof.
2589  intros.
2590  transitivity (repr (powerserie (Z_one_bits wordsize (unsigned x) 0))).
2591  transitivity (repr (unsigned x)).
2592  auto with ints. decEq. apply Z_one_bits_powerserie.
2593  auto with ints.
2594  unfold one_bits.
2595  generalize (Z_one_bits_range (unsigned x)).
2596  generalize (Z_one_bits wordsize (unsigned x) 0).
2597  induction l.
2598  intros; reflexivity.
2599  intros; simpl. rewrite <- IHl. unfold add. apply eqm_samerepr.
2600  apply eqm_add. rewrite shl_mul_two_p. rewrite mul_commut.
2601  rewrite mul_one. apply eqm_unsigned_repr_r.
2602  rewrite unsigned_repr. auto with ints.
2603  generalize (H a (in_eq _ _)). generalize wordsize_max_unsigned. omega. 
2604  auto with ints.
2605  intros; apply H; auto with coqlib.
2606Qed.
2607
2608(** ** Properties of comparisons *)
2609
2610Theorem negate_cmp:
2611  forall c x y, cmp (negate_comparison c) x y = negb (cmp c x y).
2612Proof.
2613  intros. destruct c; simpl; try rewrite negb_elim; auto.
2614Qed.
2615
2616Theorem negate_cmpu:
2617  forall c x y, cmpu (negate_comparison c) x y = negb (cmpu c x y).
2618Proof.
2619  intros. destruct c; simpl; try rewrite negb_elim; auto.
2620Qed.
2621
2622Theorem swap_cmp:
2623  forall c x y, cmp (swap_comparison c) x y = cmp c y x.
2624Proof.
2625  intros. destruct c; simpl; auto. apply eq_sym. decEq. apply eq_sym.
2626Qed.
2627
2628Theorem swap_cmpu:
2629  forall c x y, cmpu (swap_comparison c) x y = cmpu c y x.
2630Proof.
2631  intros. destruct c; simpl; auto. apply eq_sym. decEq. apply eq_sym.
2632Qed.
2633
2634Lemma translate_eq:
2635  forall x y d,
2636  eq (add x d) (add y d) = eq x y.
2637Proof.
2638  intros. unfold eq. case (zeq (unsigned x) (unsigned y)); intro.
2639  unfold add. rewrite e. apply zeq_true.
2640  apply zeq_false. unfold add. red; intro. apply n.
2641  apply eqm_small_eq; auto with ints.
2642  replace (unsigned x) with ((unsigned x + unsigned d) - unsigned d).
2643  replace (unsigned y) with ((unsigned y + unsigned d) - unsigned d).
2644  apply eqm_sub. apply eqm_trans with (unsigned (repr (unsigned x + unsigned d))).
2645  eauto with ints. apply eqm_trans with (unsigned (repr (unsigned y + unsigned d))).
2646  eauto with ints. eauto with ints. eauto with ints.
2647  omega. omega.
2648Qed.
2649
2650Lemma translate_lt:
2651  forall x y d,
2652  min_signed <= signed x + signed d <= max_signed ->
2653  min_signed <= signed y + signed d <= max_signed ->
2654  lt (add x d) (add y d) = lt x y.
2655Proof.
2656  intros. repeat rewrite add_signed. unfold lt.
2657  repeat rewrite signed_repr; auto. case (zlt (signed x) (signed y)); intro.
2658  apply zlt_true. omega.
2659  apply zlt_false. omega.
2660Qed.
2661
2662Theorem translate_cmp:
2663  forall c x y d,
2664  min_signed <= signed x + signed d <= max_signed ->
2665  min_signed <= signed y + signed d <= max_signed ->
2666  cmp c (add x d) (add y d) = cmp c x y.
2667Proof.
2668  intros. unfold cmp.
2669  rewrite translate_eq. repeat rewrite translate_lt; auto.
2670Qed. 
2671
2672Theorem notbool_isfalse_istrue:
2673  forall x, is_false x -> is_true (notbool x).
2674Proof.
2675  unfold is_false, is_true, notbool; intros; subst x.
2676  simpl. apply one_not_zero.
2677Qed.
2678
2679Theorem notbool_istrue_isfalse:
2680  forall x, is_true x -> is_false (notbool x).
2681Proof.
2682  unfold is_false, is_true, notbool; intros.
2683  generalize (eq_spec x zero). case (eq x zero); intro.
2684  contradiction. auto.
2685Qed.
2686
2687Theorem shru_lt_zero:
2688  forall x,
2689  shru x (repr (Z_of_nat wordsize - 1)) = if lt x zero then one else zero.
2690Proof.
2691  intros. rewrite shru_div_two_p.
2692  replace (two_p (unsigned (repr (Z_of_nat wordsize - 1))))
2693    with half_modulus.
2694  generalize (unsigned_range x); intro.
2695  unfold lt. rewrite signed_zero. unfold signed.
2696  destruct (zlt (unsigned x) half_modulus).
2697  rewrite zlt_false.
2698  replace (unsigned x / half_modulus) with 0. reflexivity.
2699  symmetry. apply Zdiv_unique with (unsigned x). ring. omega. omega.
2700  rewrite zlt_true.
2701  replace (unsigned x / half_modulus) with 1. reflexivity.
2702  symmetry. apply Zdiv_unique with (unsigned x - half_modulus). ring.
2703  rewrite half_modulus_modulus in H. omega. omega.
2704  rewrite unsigned_repr. apply half_modulus_power.
2705  generalize wordsize_pos wordsize_max_unsigned; omega.
2706Qed.
2707
2708Theorem ltu_range_test:
2709  forall x y,
2710  ltu x y = true -> unsigned y <= max_signed ->
2711  0 <= signed x < unsigned y.
2712Proof.
2713  intros.
2714  unfold ltu in H. destruct (zlt (unsigned x) (unsigned y)); try discriminate.
2715  rewrite signed_eq_unsigned.
2716  generalize (unsigned_range x). omega. omega.
2717Qed.
2718
2719End Make.
2720
2721(** * Specialization to 32-bit integers. *)
2722
2723Module IntWordsize.
2724  Definition wordsize := 32%nat.
2725  Remark wordsize_not_zero: wordsize <> 0%nat.
2726  Proof. unfold wordsize; congruence. Qed.
2727End IntWordsize.
2728
2729Module Int := Make(IntWordsize).
2730
2731Notation int := Int.int.
2732
2733Remark int_wordsize_divides_modulus:
2734  Zdivide (Z_of_nat Int.wordsize) Int.modulus.
2735Proof.
2736  exists (two_p (32-5)); reflexivity.
2737Qed.
2738*)
2739
2740
Note: See TracBrowser for help on using the repository browser.