source: Deliverables/D3.1/C-semantics/Integers.ma @ 487

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

Port Clight semantics to the new-new matita syntax.

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