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

Last change on this file since 535 was 535, checked in by campbell, 8 years ago

Minimal integration of bitvectors into Clight semantics

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