source: src/common/Integers.ma @ 2500

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

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

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