source: src/common/Integers.ma @ 889

Last change on this file since 889 was 889, checked in by sacerdot, 8 years ago

Minor changes because of the new, weaker (but much faster) delift.

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