source: src/common/Integers.ma @ 747

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

Merge the two AST files together (although some definitions still need to be
harmonised).

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