source: C-semantics/Integers.ma @ 14

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

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

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