source: C-semantics/Integers.ma @ 3

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

Import work-in-progress port of the CompCert? C semantics to matita.

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