source: C-semantics/Integers.ma @ 9

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

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

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