source: src/common/Integers.ma @ 697

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

Merge Clight branch of vectors and friends.
Start making stuff build.

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