source: C-semantics/Integers.ma @ 10

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

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

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