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

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

Use bit vector operations widely instead of round-trips through Z.
Implement more efficient addition, subtraction and comparison on bit vectors.

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