source: src/common/Values.ma @ 880

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

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 34.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(* * This module defines the type of values that is used in the dynamic
17  semantics of all our intermediate languages. *)
18
19include "utilities/Coqlib.ma".
20include "common/AST.ma".
21include "common/Integers.ma".
22include "common/Floats.ma".
23include "common/Errors.ma".
24
25include "ASM/BitVectorZ.ma".
26
27include "basics/logic.ma".
28
29include "utilities/binary/Z.ma".
30include "utilities/extralib.ma".
31
32(* To define pointers we need a few details about the memory model.
33
34   There are several kinds of pointers, which differ in which regions of
35   memory they address and the pointer's representation.
36   
37   Pointers are given as kind, block, offset triples, where a block identifies
38   some memory in a given region with an arbitrary concrete address.  A proof
39   is also required that the representation is suitable for the region the
40   memory resides in.  Note that blocks cannot extend out of a region (in
41   particular, a pdata pointer can address any byte in a pdata block - we never
42   need to switch to a larger xdata pointer).
43 *)
44
45(* blocks - represented by the region the memory resides in and a unique id *)
46
47record block : Type[0] ≝
48{ block_region : region
49; block_id : Z
50}.
51
52definition eq_block ≝
53λb1,b2.
54  eq_region (block_region b1) (block_region b2) ∧
55  eqZb (block_id b1) (block_id b2)
56.
57
58lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
59  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
60  P (eq_block b1 b2).
61#P * #r1 #i1 * #r2 #i2 #H1 #H2
62whd in ⊢ (?%) @eq_region_elim #H3
63[ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
64| @H2 % #E destruct elim H3 /2/
65] qed.
66
67(* Characterise the memory regions which the pointer representations can
68   address.
69
70   pointer_compat <block> <pointer representation> *)
71
72inductive pointer_compat : block → region → Prop ≝
73|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
74|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
75|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
76
77lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
78* * #id *;
79try ( %1 // )
80%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
81qed.
82
83definition is_pointer_compat : block → region → bool ≝
84λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
85
86(* Offsets into the block.  We allow integers like CompCert so that we have
87   the option of extending blocks backwards. *)
88
89record offset : Type[0] ≝ { offv : Z }.
90
91definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
92definition shift_offset : offset → int → offset ≝
93  λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
94definition neg_shift_offset : offset → int → offset ≝
95  λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
96definition sub_offset : offset → offset → int ≝
97  λx,y. bitvector_of_Z ? (offv x - offv y).
98definition zero_offset ≝ mk_offset OZ.
99definition lt_offset : offset → offset → bool ≝
100  λx,y. Zltb (offv x) (offv y).
101
102(* * A value is either:
103- a machine integer;
104- a floating-point number;
105- a pointer: a triple giving the representation of the pointer (in terms of the
106             memory regions such a pointer could address), a memory address and
107             an integer offset with respect to this address;
108- a null pointer: the region denotes the representation (i.e., pointer size)
109- the [Vundef] value denoting an arbitrary bit pattern, such as the
110  value of an uninitialized variable.
111*)
112
113inductive val: Type[0] ≝
114  | Vundef: val
115  | Vint: int → val
116  | Vfloat: float → val
117  | Vnull: region → val
118  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
119
120definition Vzero: val ≝ Vint zero.
121definition Vone: val ≝ Vint one.
122definition Vmone: val ≝ Vint mone.
123
124definition Vtrue: val ≝ Vint one.
125definition Vfalse: val ≝ Vint zero.
126
127(* Values split into bytes.  Ideally we'd use some kind of sizeof for the
128   predicates here, but we don't (currently) have a single sizeof for Vundef.
129   We only split in stages of the compiler where all Vint values are byte sized.
130 *)
131
132definition ptr_may_be_single : region → bool ≝
133λr.match r with [ Data ⇒ true | IData ⇒ true | _ ⇒ false ].
134
135definition may_be_single : val → Prop ≝
136λv. match v with
137[ Vundef ⇒ True
138| Vint _ ⇒ True
139| Vfloat _ ⇒ False
140| Vnull r ⇒ ptr_may_be_single r = true
141| Vptr r _ _ _ ⇒ ptr_may_be_single r = true
142].
143
144definition may_be_split : val → Prop ≝
145λv.match v with
146[ Vint _ ⇒ False
147| Vnull r ⇒ ptr_may_be_single r = false
148| Vptr r _ _ _ ⇒ ptr_may_be_single r = false
149| _ ⇒ True
150].
151
152inductive split_val : Type[0] ≝
153| Single : ∀v:val. may_be_single v → split_val
154| High   : ∀v:val. may_be_split v → split_val
155| Low    : ∀v:val. may_be_split v → split_val.
156
157notation > "vbox('do' _ ← e; break e')" with precedence 40 for @{'bind ${e} (λ_.${e'})}.
158(*
159let rec assert_nat_eq (m,n:nat) : res (m = n) ≝
160match m return λx.res (x = n) with
161[ O ⇒ match n return λx. res (O = x) with [ O ⇒ OK ? (refl ??) | _ ⇒ Error ? ]
162| S m' ⇒ match n return λx.res (S m' = x) with [ O ⇒ Error ? | S n' ⇒
163  do E ← assert_nat_eq m' n';
164  match E return λx.λ_. res (S m' = S x) with [ refl ⇒ OK ? (refl ??) ] ]
165].
166
167definition res_eq_nat : ∀m,n:nat. ∀P:nat → Type[0]. P m → res (P n) ≝
168λm,n,P,p.
169  do E ← assert_nat_eq m n;
170  match E return λx.λ_. res (P x) with [ refl ⇒ OK ? p ].
171
172definition break : ∀n:nat. val → res (Vector split_val n) ≝
173λn,v. match v return λv'. (may_be_single v' → ?) → (may_be_split v' → ?) → ? with
174[ Vundef ⇒ λs.λt. res_eq_nat 1 n ? (s I)
175| Vint i ⇒ λs.λt. res_eq_nat 1 n ? (s I)
176| Vfloat f ⇒ λs.λt. res_eq_nat 2 n ? (t I)
177| Vnull r ⇒
178    match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with
179    [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))
180    | false ⇒ λs.λt. ?
181    ]
182| Vptr r b p o ⇒
183    match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with
184    [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))
185    | false ⇒ λs.λt. ?
186    ]
187] (λp. [[ Single v p ]]) (λp. [[ Low v p; High v p ]]).
188@(res_eq_nat 2 n ? (t (refl ??))) qed. (* XXX: I have no idea why this fails if you do it directly. *)
189
190definition val_eq : val → val → bool ≝
191λx,y.
192match x with
193[ Vundef ⇒ match y with [ Vundef ⇒ true | _ ⇒ false ]
194| Vint i ⇒ match y with [ Vint j ⇒ eq i j | _ ⇒ false ]
195| Vfloat f ⇒ match y with [ Vfloat f' ⇒ match eq_dec f f' with [ inl _ ⇒ true | _ ⇒ false ] | _ ⇒ false ]
196| Vnull r ⇒ match y with [ Vnull r' ⇒ eq_region r r' | _ ⇒ false ]
197| Vptr r b p o ⇒ match y with [ Vptr r' b' p' o' ⇒ eq_region r r' ∧ eq_block b b' ∧ eq_offset o o' | _ ⇒ false ]
198].
199
200definition merge : ∀n:nat. Vector split_val n → res val ≝
201λn,s. match s with
202[ VEmpty ⇒ Error ?
203| VCons _ h1 t1 ⇒
204  match t1 with
205  [ VEmpty ⇒ match h1 with [ Single v _ ⇒ OK ? v | _ ⇒ Error ? ]
206  | VCons _ h2 t2 ⇒
207    match t2 with
208    [ VEmpty ⇒ match h1 with [ Low v _ ⇒ match h2 with [ High v' _ ⇒ if val_eq v v' then OK ? v else Error ? | _ ⇒ Error ? ] | _ ⇒ Error ? ]
209    | VCons _ _ _ ⇒ Error ?
210    ]
211  ]
212].
213   
214*)
215(*
216(** The module [Val] defines a number of arithmetic and logical operations
217  over type [val].  Most of these operations are straightforward extensions
218  of the corresponding integer or floating-point operations. *)
219
220Module Val.
221*)
222definition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
223(*
224definition has_type ≝ λv: val. λt: typ.
225  match v with
226  [ Vundef ⇒ True
227  | Vint _ ⇒ match t with [ ASTint ⇒ True | _ ⇒ False ]
228  | Vfloat _ ⇒ match t with [ ASTfloat ⇒ True | _ ⇒ False ]
229  | Vptr _ _ _ ⇒ match t with [ ASTptr ⇒ True | _ ⇒ False ]
230  | _ ⇒ False
231  ].
232
233let rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝
234  match vl with
235  [ nil ⇒ match tl with [ nil ⇒ True | _ ⇒ False ]
236  | cons v1 vs ⇒ match tl with [ nil ⇒ False | cons t1 ts ⇒
237               has_type v1 t1 ∧ has_type_list vs ts ]
238  ].
239*)
240(* * Truth values.  Pointers and non-zero integers are treated as [True].
241  The integer 0 (also used to represent the null pointer) is [False].
242  [Vundef] and floats are neither true nor false. *)
243
244definition is_true : val → Prop ≝ λv.
245  match v with
246  [ Vint n ⇒ n ≠ zero
247  | Vptr _ b _ ofs ⇒ True
248  | _ ⇒ False
249  ].
250
251definition is_false : val → Prop ≝ λv.
252  match v with
253  [ Vint n ⇒ n = zero
254  | Vnull _ ⇒ True
255  | _ ⇒ False
256  ].
257
258inductive bool_of_val: val → bool → Prop ≝
259  | bool_of_val_int_true:
260      ∀n. n ≠ zero → bool_of_val (Vint n) true
261  | bool_of_val_int_false:
262      bool_of_val (Vint zero) false
263  | bool_of_val_ptr:
264      ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
265  | bool_of_val_null:
266      ∀r. bool_of_val (Vnull r) true.
267
268axiom ValueNotABoolean : String.
269
270definition eval_bool_of_val : val → res bool ≝
271λv. match v with
272[ Vint i ⇒ OK ? (notb (eq i zero))
273| Vnull _ ⇒ OK ? false
274| Vptr _ _ _ _ ⇒ OK ? true
275| _ ⇒ Error ? (msg ValueNotABoolean)
276].
277
278definition neg : val → val ≝ λv.
279  match v with
280  [ Vint n ⇒ Vint (neg n)
281  | _ ⇒ Vundef
282  ].
283
284definition negf : val → val ≝ λv.
285  match v with
286  [ Vfloat f ⇒ Vfloat (Fneg f)
287  | _ => Vundef
288  ].
289
290definition absf : val → val ≝ λv.
291  match v with
292  [ Vfloat f ⇒ Vfloat (Fabs f)
293  | _ ⇒ Vundef
294  ].
295
296definition intoffloat : val → val ≝ λv.
297  match v with
298  [ Vfloat f ⇒ Vint (intoffloat f)
299  | _ ⇒ Vundef
300  ].
301
302definition intuoffloat : val → val ≝ λv.
303  match v with
304  [ Vfloat f ⇒ Vint (intuoffloat f)
305  | _ ⇒ Vundef
306  ].
307
308definition floatofint : val → val ≝ λv.
309  match v with
310  [ Vint n ⇒ Vfloat (floatofint n)
311  | _ ⇒ Vundef
312  ].
313
314definition floatofintu : val → val ≝ λv.
315  match v with
316  [ Vint n ⇒ Vfloat (floatofintu n)
317  | _ ⇒ Vundef
318  ].
319
320definition notint : val → val ≝ λv.
321  match v with
322  [ Vint n ⇒ Vint (xor n mone)
323  | _ ⇒ Vundef
324  ].
325 
326(* FIXME: switch to alias, or rename, or … *)
327definition int_eq : int → int → bool ≝ eq.
328definition notbool : val → val ≝ λv.
329  match v with
330  [ Vint n ⇒ of_bool (int_eq n zero)
331  | Vptr _ b _ ofs ⇒ Vfalse
332  | Vnull _ ⇒ Vtrue
333  | _ ⇒ Vundef
334  ].
335
336definition zero_ext ≝ λnbits: nat. λv: val.
337  match v with
338  [ Vint n ⇒ Vint (zero_ext nbits n)
339  | _ ⇒ Vundef
340  ].
341
342definition sign_ext ≝ λnbits:nat. λv:val.
343  match v with
344  [ Vint i ⇒ Vint (sign_ext nbits i)
345  | _ ⇒ Vundef
346  ].
347
348definition singleoffloat : val → val ≝ λv.
349  match v with
350  [ Vfloat f ⇒ Vfloat (singleoffloat f)
351  | _ ⇒ Vundef
352  ].
353
354(* TODO: add zero to null? *)
355definition add ≝ λv1,v2: val.
356  match v1 with
357  [ Vint n1 ⇒ match v2 with
358    [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
359    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
360    | _ ⇒ Vundef ]
361  | Vptr r b1 p ofs1 ⇒ match v2 with
362    [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2)
363    | _ ⇒ Vundef ]
364  | _ ⇒ Vundef ].
365
366definition sub ≝ λv1,v2: val.
367  match v1 with
368  [ Vint n1 ⇒ match v2 with
369    [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
370    | _ ⇒ Vundef ]
371  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
372    [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)
373    | Vptr r2 b2 p2 ofs2 ⇒
374        if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef
375    | _ ⇒ Vundef ]
376  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
377  | _ ⇒ Vundef ].
378
379definition mul ≝ λv1, v2: val.
380  match v1 with
381  [ Vint n1 ⇒ match v2 with
382    [ Vint n2 ⇒ Vint (mul n1 n2)
383    | _ ⇒ Vundef ]
384  | _ ⇒ Vundef ].
385(*
386definition divs ≝ λv1, v2: val.
387  match v1 with
388  [ Vint n1 ⇒ match v2 with
389    [ Vint n2 ⇒ Vint (divs n1 n2)
390    | _ ⇒ Vundef ]
391  | _ ⇒ Vundef ].
392
393Definition mods (v1 v2: val): val :=
394  match v1, v2 with
395  | Vint n1, Vint n2 =>
396      if Int.eq n2 Int.zero then Vundef else Vint(Int.mods n1 n2)
397  | _, _ => Vundef
398  end.
399
400Definition divu (v1 v2: val): val :=
401  match v1, v2 with
402  | Vint n1, Vint n2 =>
403      if Int.eq n2 Int.zero then Vundef else Vint(Int.divu n1 n2)
404  | _, _ => Vundef
405  end.
406
407Definition modu (v1 v2: val): val :=
408  match v1, v2 with
409  | Vint n1, Vint n2 =>
410      if Int.eq n2 Int.zero then Vundef else Vint(Int.modu n1 n2)
411  | _, _ => Vundef
412  end.
413*)
414definition v_and ≝ λv1, v2: val.
415  match v1 with
416  [ Vint n1 ⇒ match v2 with
417    [ Vint n2 ⇒ Vint (i_and n1 n2)
418    | _ ⇒ Vundef ]
419  | _ ⇒ Vundef ].
420
421definition or ≝ λv1, v2: val.
422  match v1 with
423  [ Vint n1 ⇒ match v2 with
424    [ Vint n2 ⇒ Vint (or n1 n2)
425    | _ ⇒ Vundef ]
426  | _ ⇒ Vundef ].
427
428definition xor ≝ λv1, v2: val.
429  match v1 with
430  [ Vint n1 ⇒ match v2 with
431    [ Vint n2 ⇒ Vint (xor n1 n2)
432    | _ ⇒ Vundef ]
433  | _ ⇒ Vundef ].
434(*
435Definition shl (v1 v2: val): val :=
436  match v1, v2 with
437  | Vint n1, Vint n2 =>
438     if Int.ltu n2 Int.iwordsize
439     then Vint(Int.shl n1 n2)
440     else Vundef
441  | _, _ => Vundef
442  end.
443
444Definition shr (v1 v2: val): val :=
445  match v1, v2 with
446  | Vint n1, Vint n2 =>
447     if Int.ltu n2 Int.iwordsize
448     then Vint(Int.shr n1 n2)
449     else Vundef
450  | _, _ => Vundef
451  end.
452
453Definition shr_carry (v1 v2: val): val :=
454  match v1, v2 with
455  | Vint n1, Vint n2 =>
456     if Int.ltu n2 Int.iwordsize
457     then Vint(Int.shr_carry n1 n2)
458     else Vundef
459  | _, _ => Vundef
460  end.
461
462Definition shrx (v1 v2: val): val :=
463  match v1, v2 with
464  | Vint n1, Vint n2 =>
465     if Int.ltu n2 Int.iwordsize
466     then Vint(Int.shrx n1 n2)
467     else Vundef
468  | _, _ => Vundef
469  end.
470
471Definition shru (v1 v2: val): val :=
472  match v1, v2 with
473  | Vint n1, Vint n2 =>
474     if Int.ltu n2 Int.iwordsize
475     then Vint(Int.shru n1 n2)
476     else Vundef
477  | _, _ => Vundef
478  end.
479
480Definition rolm (v: val) (amount mask: int): val :=
481  match v with
482  | Vint n => Vint(Int.rolm n amount mask)
483  | _ => Vundef
484  end.
485
486Definition ror (v1 v2: val): val :=
487  match v1, v2 with
488  | Vint n1, Vint n2 =>
489     if Int.ltu n2 Int.iwordsize
490     then Vint(Int.ror n1 n2)
491     else Vundef
492  | _, _ => Vundef
493  end.
494*)
495definition addf ≝ λv1,v2: val.
496  match v1 with
497  [ Vfloat f1 ⇒ match v2 with
498    [ Vfloat f2 ⇒ Vfloat (Fadd f1 f2)
499    | _ ⇒ Vundef ]
500  | _ ⇒ Vundef ].
501
502definition subf ≝ λv1,v2: val.
503  match v1 with
504  [ Vfloat f1 ⇒ match v2 with
505    [ Vfloat f2 ⇒ Vfloat (Fsub f1 f2)
506    | _ ⇒ Vundef ]
507  | _ ⇒ Vundef ].
508
509definition mulf ≝ λv1,v2: val.
510  match v1 with
511  [ Vfloat f1 ⇒ match v2 with
512    [ Vfloat f2 ⇒ Vfloat (Fmul f1 f2)
513    | _ ⇒ Vundef ]
514  | _ ⇒ Vundef ].
515
516definition divf ≝ λv1,v2: val.
517  match v1 with
518  [ Vfloat f1 ⇒ match v2 with
519    [ Vfloat f2 ⇒ Vfloat (Fdiv f1 f2)
520    | _ ⇒ Vundef ]
521  | _ ⇒ Vundef ].
522
523definition cmp_match : comparison → val ≝ λc.
524  match c with
525  [ Ceq ⇒ Vtrue
526  | Cne ⇒ Vfalse
527  | _   ⇒ Vundef
528  ].
529
530definition cmp_mismatch : comparison → val ≝ λc.
531  match c with
532  [ Ceq ⇒ Vfalse
533  | Cne ⇒ Vtrue
534  | _   ⇒ Vundef
535  ].
536
537definition cmp_offset ≝
538λc: comparison. λx,y:offset.
539  match c with
540  [ Ceq ⇒  eq_offset x y
541  | Cne ⇒ ¬eq_offset x y
542  | Clt ⇒  lt_offset x y
543  | Cle ⇒ ¬lt_offset y x
544  | Cgt ⇒  lt_offset y x
545  | Cge ⇒ ¬lt_offset x y
546  ].
547
548definition cmp ≝ λc: comparison. λv1,v2: val.
549  match v1 with
550  [ Vint n1 ⇒ match v2 with
551    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
552    | _ ⇒ Vundef ]
553  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
554    [ Vptr r2 b2 p2 ofs2 ⇒
555        if eq_block b1 b2
556        then of_bool (cmp_offset c ofs1 ofs2)
557        else cmp_mismatch c
558    | Vnull r2 ⇒ cmp_mismatch c
559    | _ ⇒ Vundef ]
560  | Vnull r1 ⇒ match v2 with
561    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
562    | Vnull r2 ⇒ cmp_match c
563    | _ ⇒ Vundef
564    ]
565  | _ ⇒ Vundef ].
566
567definition cmpu ≝ λc: comparison. λv1,v2: val.
568  match v1 with
569  [ Vint n1 ⇒ match v2 with
570    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
571    | _ ⇒ Vundef ]
572  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
573    [ Vptr r2 b2 p2 ofs2 ⇒
574        if eq_block b1 b2
575        then of_bool (cmp_offset c ofs1 ofs2)
576        else cmp_mismatch c
577    | Vnull r2 ⇒ cmp_mismatch c
578    | _ ⇒ Vundef ]
579  | Vnull r1 ⇒ match v2 with
580    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
581    | Vnull r2 ⇒ cmp_match c
582    | _ ⇒ Vundef
583    ]
584  | _ ⇒ Vundef ].
585
586definition cmpf ≝ λc: comparison. λv1,v2: val.
587  match v1 with
588  [ Vfloat f1 ⇒ match v2 with
589    [ Vfloat f2 ⇒ of_bool (Fcmp c f1 f2)
590    | _ ⇒ Vundef ]
591  | _ ⇒ Vundef ].
592
593(* * [load_result] is used in the memory model (library [Mem])
594  to post-process the results of a memory read.  For instance,
595  consider storing the integer value [0xFFF] on 1 byte at a
596  given address, and reading it back.  If it is read back with
597  chunk [Mint8unsigned], zero-extension must be performed, resulting
598  in [0xFF].  If it is read back as a [Mint8signed], sign-extension
599  is performed and [0xFFFFFFFF] is returned.   Type mismatches
600  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
601
602let rec load_result (chunk: memory_chunk) (v: val) ≝
603  match v with
604  [ Vint n ⇒
605    match chunk with
606    [ Mint8signed ⇒ Vint (sign_ext 8 n)
607    | Mint8unsigned ⇒ Vint (zero_ext 8 n)
608    | Mint16signed ⇒ Vint (sign_ext 16 n)
609    | Mint16unsigned ⇒ Vint (zero_ext 16 n)
610    | Mint32 ⇒ Vint n
611    | _ ⇒ Vundef
612    ]
613  | Vptr r b p ofs ⇒
614    match chunk with
615    [ Mpointer r' ⇒ if eq_region r r' then Vptr r b p ofs else Vundef
616    | _ ⇒ Vundef
617    ]
618  | Vnull r ⇒
619    match chunk with
620    [ Mpointer r' ⇒ if eq_region r r' then Vnull r else Vundef
621    | _ ⇒ Vundef
622    ]
623  | Vfloat f ⇒
624    match chunk with
625    [ Mfloat32 ⇒ Vfloat(singleoffloat f)
626    | Mfloat64 ⇒ Vfloat f
627    | _ ⇒ Vundef
628    ]
629  | _ ⇒ Vundef
630  ].
631
632(*
633(** Theorems on arithmetic operations. *)
634
635Theorem cast8unsigned_and:
636  forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
637Proof.
638  destruct x; simpl; auto. decEq.
639  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. vm_compute; auto.
640Qed.
641
642Theorem cast16unsigned_and:
643  forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
644Proof.
645  destruct x; simpl; auto. decEq.
646  change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto.
647Qed.
648
649Theorem istrue_not_isfalse:
650  forall v, is_false v -> is_true (notbool v).
651Proof.
652  destruct v; simpl; try contradiction.
653  intros. subst i. simpl. discriminate.
654Qed.
655
656Theorem isfalse_not_istrue:
657  forall v, is_true v -> is_false (notbool v).
658Proof.
659  destruct v; simpl; try contradiction.
660  intros. generalize (Int.eq_spec i Int.zero).
661  case (Int.eq i Int.zero); intro.
662  contradiction. simpl. auto.
663  auto.
664Qed.
665
666Theorem bool_of_true_val:
667  forall v, is_true v -> bool_of_val v true.
668Proof.
669  intro. destruct v; simpl; intros; try contradiction.
670  constructor; auto. constructor.
671Qed.
672
673Theorem bool_of_true_val2:
674  forall v, bool_of_val v true -> is_true v.
675Proof.
676  intros. inversion H; simpl; auto.
677Qed.
678
679Theorem bool_of_true_val_inv:
680  forall v b, is_true v -> bool_of_val v b -> b = true.
681Proof.
682  intros. inversion H0; subst v b; simpl in H; auto.
683Qed.
684
685Theorem bool_of_false_val:
686  forall v, is_false v -> bool_of_val v false.
687Proof.
688  intro. destruct v; simpl; intros; try contradiction.
689  subst i;  constructor.
690Qed.
691
692Theorem bool_of_false_val2:
693  forall v, bool_of_val v false -> is_false v.
694Proof.
695  intros. inversion H; simpl; auto.
696Qed.
697
698Theorem bool_of_false_val_inv:
699  forall v b, is_false v -> bool_of_val v b -> b = false.
700Proof.
701  intros. inversion H0; subst v b; simpl in H.
702  congruence. auto. contradiction.
703Qed.
704
705Theorem notbool_negb_1:
706  forall b, of_bool (negb b) = notbool (of_bool b).
707Proof.
708  destruct b; reflexivity.
709Qed.
710
711Theorem notbool_negb_2:
712  forall b, of_bool b = notbool (of_bool (negb b)).
713Proof.
714  destruct b; reflexivity.
715Qed.
716
717Theorem notbool_idem2:
718  forall b, notbool(notbool(of_bool b)) = of_bool b.
719Proof.
720  destruct b; reflexivity.
721Qed.
722
723Theorem notbool_idem3:
724  forall x, notbool(notbool(notbool x)) = notbool x.
725Proof.
726  destruct x; simpl; auto.
727  case (Int.eq i Int.zero); reflexivity.
728Qed.
729
730Theorem add_commut: forall x y, add x y = add y x.
731Proof.
732  destruct x; destruct y; simpl; auto.
733  decEq. apply Int.add_commut.
734Qed.
735
736Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
737Proof.
738  destruct x; destruct y; destruct z; simpl; auto.
739  rewrite Int.add_assoc; auto.
740  rewrite Int.add_assoc; auto.
741  decEq. decEq. apply Int.add_commut.
742  decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc.
743  decEq. apply Int.add_commut.
744  decEq. rewrite Int.add_assoc. auto.
745Qed.
746
747Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
748Proof.
749  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut.
750Qed.
751
752Theorem add_permut_4:
753  forall x y z t, add (add x y) (add z t) = add (add x z) (add y t).
754Proof.
755  intros. rewrite add_permut. rewrite add_assoc.
756  rewrite add_permut. symmetry. apply add_assoc.
757Qed.
758
759Theorem neg_zero: neg Vzero = Vzero.
760Proof.
761  reflexivity.
762Qed.
763
764Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
765Proof.
766  destruct x; destruct y; simpl; auto. decEq. apply Int.neg_add_distr.
767Qed.
768
769Theorem sub_zero_r: forall x, sub Vzero x = neg x.
770Proof.
771  destruct x; simpl; auto.
772Qed.
773
774Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)).
775Proof.
776  destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto.
777Qed.
778
779Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y).
780Proof.
781  intros. unfold sub, add.
782  destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto.
783Qed.
784
785Theorem sub_add_l:
786  forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i).
787Proof.
788  destruct v1; destruct v2; intros; simpl; auto.
789  rewrite Int.sub_add_l. auto.
790  rewrite Int.sub_add_l. auto.
791  case (zeq b b0); intro. rewrite Int.sub_add_l. auto. reflexivity.
792Qed.
793
794Theorem sub_add_r:
795  forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)).
796Proof.
797  destruct v1; destruct v2; intros; simpl; auto.
798  rewrite Int.sub_add_r. auto.
799  repeat rewrite Int.sub_add_opp. decEq.
800  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
801  decEq. repeat rewrite Int.sub_add_opp.
802  rewrite Int.add_assoc. decEq. apply Int.neg_add_distr.
803  case (zeq b b0); intro. simpl. decEq.
804  repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq.
805  apply Int.neg_add_distr.
806  reflexivity.
807Qed.
808
809Theorem mul_commut: forall x y, mul x y = mul y x.
810Proof.
811  destruct x; destruct y; simpl; auto. decEq. apply Int.mul_commut.
812Qed.
813
814Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).
815Proof.
816  destruct x; destruct y; destruct z; simpl; auto.
817  decEq. apply Int.mul_assoc.
818Qed.
819
820Theorem mul_add_distr_l:
821  forall x y z, mul (add x y) z = add (mul x z) (mul y z).
822Proof.
823  destruct x; destruct y; destruct z; simpl; auto.
824  decEq. apply Int.mul_add_distr_l.
825Qed.
826
827
828Theorem mul_add_distr_r:
829  forall x y z, mul x (add y z) = add (mul x y) (mul x z).
830Proof.
831  destruct x; destruct y; destruct z; simpl; auto.
832  decEq. apply Int.mul_add_distr_r.
833Qed.
834
835Theorem mul_pow2:
836  forall x n logn,
837  Int.is_power2 n = Some logn ->
838  mul x (Vint n) = shl x (Vint logn).
839Proof.
840  intros; destruct x; simpl; auto.
841  change 32 with (Z_of_nat Int.wordsize).
842  rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto.
843Qed. 
844
845Theorem mods_divs:
846  forall x y, mods x y = sub x (mul (divs x y) y).
847Proof.
848  destruct x; destruct y; simpl; auto.
849  case (Int.eq i0 Int.zero); simpl. auto. decEq. apply Int.mods_divs.
850Qed.
851
852Theorem modu_divu:
853  forall x y, modu x y = sub x (mul (divu x y) y).
854Proof.
855  destruct x; destruct y; simpl; auto.
856  generalize (Int.eq_spec i0 Int.zero);
857  case (Int.eq i0 Int.zero); simpl. auto.
858  intro. decEq. apply Int.modu_divu. auto.
859Qed.
860
861Theorem divs_pow2:
862  forall x n logn,
863  Int.is_power2 n = Some logn ->
864  divs x (Vint n) = shrx x (Vint logn).
865Proof.
866  intros; destruct x; simpl; auto.
867  change 32 with (Z_of_nat Int.wordsize).
868  rewrite (Int.is_power2_range _ _ H).
869  generalize (Int.eq_spec n Int.zero);
870  case (Int.eq n Int.zero); intro.
871  subst n. compute in H. discriminate.
872  decEq. apply Int.divs_pow2. auto.
873Qed.
874
875Theorem divu_pow2:
876  forall x n logn,
877  Int.is_power2 n = Some logn ->
878  divu x (Vint n) = shru x (Vint logn).
879Proof.
880  intros; destruct x; simpl; auto.
881  change 32 with (Z_of_nat Int.wordsize).
882  rewrite (Int.is_power2_range _ _ H).
883  generalize (Int.eq_spec n Int.zero);
884  case (Int.eq n Int.zero); intro.
885  subst n. compute in H. discriminate.
886  decEq. apply Int.divu_pow2. auto.
887Qed.
888
889Theorem modu_pow2:
890  forall x n logn,
891  Int.is_power2 n = Some logn ->
892  modu x (Vint n) = and x (Vint (Int.sub n Int.one)).
893Proof.
894  intros; destruct x; simpl; auto.
895  generalize (Int.eq_spec n Int.zero);
896  case (Int.eq n Int.zero); intro.
897  subst n. compute in H. discriminate.
898  decEq. eapply Int.modu_and; eauto.
899Qed.
900
901Theorem and_commut: forall x y, and x y = and y x.
902Proof.
903  destruct x; destruct y; simpl; auto. decEq. apply Int.and_commut.
904Qed.
905
906Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
907Proof.
908  destruct x; destruct y; destruct z; simpl; auto.
909  decEq. apply Int.and_assoc.
910Qed.
911
912Theorem or_commut: forall x y, or x y = or y x.
913Proof.
914  destruct x; destruct y; simpl; auto. decEq. apply Int.or_commut.
915Qed.
916
917Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
918Proof.
919  destruct x; destruct y; destruct z; simpl; auto.
920  decEq. apply Int.or_assoc.
921Qed.
922
923Theorem xor_commut: forall x y, xor x y = xor y x.
924Proof.
925  destruct x; destruct y; simpl; auto. decEq. apply Int.xor_commut.
926Qed.
927
928Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
929Proof.
930  destruct x; destruct y; destruct z; simpl; auto.
931  decEq. apply Int.xor_assoc.
932Qed.
933
934Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y.
935Proof.
936  destruct x; destruct y; simpl; auto.
937  case (Int.ltu i0 Int.iwordsize); auto.
938  decEq. symmetry. apply Int.shl_mul.
939Qed.
940
941Theorem shl_rolm:
942  forall x n,
943  Int.ltu n Int.iwordsize = true ->
944  shl x (Vint n) = rolm x n (Int.shl Int.mone n).
945Proof.
946  intros; destruct x; simpl; auto.
947  rewrite H. decEq. apply Int.shl_rolm. exact H.
948Qed.
949
950Theorem shru_rolm:
951  forall x n,
952  Int.ltu n Int.iwordsize = true ->
953  shru x (Vint n) = rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n).
954Proof.
955  intros; destruct x; simpl; auto.
956  rewrite H. decEq. apply Int.shru_rolm. exact H.
957Qed.
958
959Theorem shrx_carry:
960  forall x y,
961  add (shr x y) (shr_carry x y) = shrx x y.
962Proof.
963  destruct x; destruct y; simpl; auto.
964  case (Int.ltu i0 Int.iwordsize); auto.
965  simpl. decEq. apply Int.shrx_carry.
966Qed.
967
968Theorem or_rolm:
969  forall x n m1 m2,
970  or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2).
971Proof.
972  intros; destruct x; simpl; auto.
973  decEq. apply Int.or_rolm.
974Qed.
975
976Theorem rolm_rolm:
977  forall x n1 m1 n2 m2,
978  rolm (rolm x n1 m1) n2 m2 =
979    rolm x (Int.modu (Int.add n1 n2) Int.iwordsize)
980           (Int.and (Int.rol m1 n2) m2).
981Proof.
982  intros; destruct x; simpl; auto.
983  decEq.
984  apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
985Qed.
986
987Theorem rolm_zero:
988  forall x m,
989  rolm x Int.zero m = and x (Vint m).
990Proof.
991  intros; destruct x; simpl; auto. decEq. apply Int.rolm_zero.
992Qed.
993
994Theorem addf_commut: forall x y, addf x y = addf y x.
995Proof.
996  destruct x; destruct y; simpl; auto. decEq. apply Float.addf_commut.
997Qed.
998
999Lemma negate_cmp_mismatch:
1000  forall c,
1001  cmp_mismatch (negate_comparison c) = notbool(cmp_mismatch c).
1002Proof.
1003  destruct c; reflexivity.
1004Qed.
1005
1006Theorem negate_cmp:
1007  forall c x y,
1008  cmp (negate_comparison c) x y = notbool (cmp c x y).
1009Proof.
1010  destruct x; destruct y; simpl; auto.
1011  rewrite Int.negate_cmp. apply notbool_negb_1.
1012  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
1013  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
1014  case (zeq b b0); intro.
1015  rewrite Int.negate_cmp. apply notbool_negb_1.
1016  apply negate_cmp_mismatch.
1017Qed.
1018
1019Theorem negate_cmpu:
1020  forall c x y,
1021  cmpu (negate_comparison c) x y = notbool (cmpu c x y).
1022Proof.
1023  destruct x; destruct y; simpl; auto.
1024  rewrite Int.negate_cmpu. apply notbool_negb_1.
1025  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
1026  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
1027  case (zeq b b0); intro.
1028  rewrite Int.negate_cmpu. apply notbool_negb_1.
1029  apply negate_cmp_mismatch.
1030Qed.
1031
1032Lemma swap_cmp_mismatch:
1033  forall c, cmp_mismatch (swap_comparison c) = cmp_mismatch c.
1034Proof.
1035  destruct c; reflexivity.
1036Qed.
1037 
1038Theorem swap_cmp:
1039  forall c x y,
1040  cmp (swap_comparison c) x y = cmp c y x.
1041Proof.
1042  destruct x; destruct y; simpl; auto.
1043  rewrite Int.swap_cmp. auto.
1044  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
1045  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
1046  case (zeq b b0); intro.
1047  subst b0. rewrite zeq_true. rewrite Int.swap_cmp. auto.
1048  rewrite zeq_false. apply swap_cmp_mismatch. auto.
1049Qed.
1050
1051Theorem swap_cmpu:
1052  forall c x y,
1053  cmpu (swap_comparison c) x y = cmpu c y x.
1054Proof.
1055  destruct x; destruct y; simpl; auto.
1056  rewrite Int.swap_cmpu. auto.
1057  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
1058  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
1059  case (zeq b b0); intro.
1060  subst b0. rewrite zeq_true. rewrite Int.swap_cmpu. auto.
1061  rewrite zeq_false. apply swap_cmp_mismatch. auto.
1062Qed.
1063
1064Theorem negate_cmpf_eq:
1065  forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2.
1066Proof.
1067  destruct v1; destruct v2; simpl; auto.
1068  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1.
1069  apply notbool_idem2.
1070Qed.
1071
1072Theorem negate_cmpf_ne:
1073  forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.
1074Proof.
1075  destruct v1; destruct v2; simpl; auto.
1076  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. auto.
1077Qed.
1078
1079Lemma or_of_bool:
1080  forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2).
1081Proof.
1082  destruct b1; destruct b2; reflexivity.
1083Qed.
1084
1085Theorem cmpf_le:
1086  forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2).
1087Proof.
1088  destruct v1; destruct v2; simpl; auto.
1089  rewrite or_of_bool. decEq. apply Float.cmp_le_lt_eq.
1090Qed.
1091
1092Theorem cmpf_ge:
1093  forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2).
1094Proof.
1095  destruct v1; destruct v2; simpl; auto.
1096  rewrite or_of_bool. decEq. apply Float.cmp_ge_gt_eq.
1097Qed.
1098
1099Definition is_bool (v: val) :=
1100  v = Vundef \/ v = Vtrue \/ v = Vfalse.
1101
1102Lemma of_bool_is_bool:
1103  forall b, is_bool (of_bool b).
1104Proof.
1105  destruct b; unfold is_bool; simpl; tauto.
1106Qed.
1107
1108Lemma undef_is_bool: is_bool Vundef.
1109Proof.
1110  unfold is_bool; tauto.
1111Qed.
1112
1113Lemma cmp_mismatch_is_bool:
1114  forall c, is_bool (cmp_mismatch c).
1115Proof.
1116  destruct c; simpl; unfold is_bool; tauto.
1117Qed.
1118
1119Lemma cmp_is_bool:
1120  forall c v1 v2, is_bool (cmp c v1 v2).
1121Proof.
1122  destruct v1; destruct v2; simpl; try apply undef_is_bool.
1123  apply of_bool_is_bool.
1124  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1125  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1126  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
1127Qed.
1128
1129Lemma cmpu_is_bool:
1130  forall c v1 v2, is_bool (cmpu c v1 v2).
1131Proof.
1132  destruct v1; destruct v2; simpl; try apply undef_is_bool.
1133  apply of_bool_is_bool.
1134  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1135  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1136  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
1137Qed.
1138
1139Lemma cmpf_is_bool:
1140  forall c v1 v2, is_bool (cmpf c v1 v2).
1141Proof.
1142  destruct v1; destruct v2; simpl;
1143  apply undef_is_bool || apply of_bool_is_bool.
1144Qed.
1145
1146Lemma notbool_is_bool:
1147  forall v, is_bool (notbool v).
1148Proof.
1149  destruct v; simpl.
1150  apply undef_is_bool. apply of_bool_is_bool.
1151  apply undef_is_bool. unfold is_bool; tauto.
1152Qed.
1153
1154Lemma notbool_xor:
1155  forall v, is_bool v -> v = xor (notbool v) Vone.
1156Proof.
1157  intros. elim H; intro. 
1158  subst v. reflexivity.
1159  elim H0; intro; subst v; reflexivity.
1160Qed.
1161
1162Lemma rolm_lt_zero:
1163  forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero).
1164Proof.
1165  intros. destruct v; simpl; auto.
1166  transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))).
1167  decEq. symmetry. rewrite Int.shru_rolm. auto. auto.
1168  rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto.
1169Qed.
1170
1171Lemma rolm_ge_zero:
1172  forall v,
1173  xor (rolm v Int.one Int.one) (Vint Int.one) = cmp Cge v (Vint Int.zero).
1174Proof.
1175  intros. rewrite rolm_lt_zero. destruct v; simpl; auto.
1176  destruct (Int.lt i Int.zero); auto.
1177Qed.
1178*)
1179(* * The ``is less defined'' relation between values.
1180    A value is less defined than itself, and [Vundef] is
1181    less defined than any value. *)
1182
1183inductive Val_lessdef: val → val → Prop ≝
1184  | lessdef_refl: ∀v. Val_lessdef v v
1185  | lessdef_undef: ∀v. Val_lessdef Vundef v.
1186
1187inductive lessdef_list: list val → list val → Prop ≝
1188  | lessdef_list_nil:
1189      lessdef_list (nil ?) (nil ?)
1190  | lessdef_list_cons:
1191      ∀v1,v2,vl1,vl2.
1192      Val_lessdef v1 v2 → lessdef_list vl1 vl2 →
1193      lessdef_list (v1 :: vl1) (v2 :: vl2).
1194
1195(*Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.*)
1196(*
1197lemma lessdef_list_inv:
1198  ∀vl1,vl2. lessdef_list vl1 vl2 → vl1 = vl2 ∨ in_list ? Vundef vl1.
1199#vl1 elim vl1;
1200[ #vl2 #H inversion H; /2/; #h1 #h2 #t1 #t2 #H1 #H2 #H3 #Hbad destruct
1201| #h #t #IH #vl2 #H
1202    inversion H;
1203    [ #H' destruct
1204    | #h1 #h2 #t1 #t2 #H1 #H2 #H3 #e1 #e2 destruct;
1205        elim H1;
1206        [ elim (IH t2 H2);
1207            [ #e destruct; /2/;
1208            | /3/ ]
1209        | /3/ ]
1210    ]
1211] qed.
1212*)
1213lemma load_result_lessdef:
1214  ∀chunk,v1,v2.
1215  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
1216#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 cases chunk
1217[ 8: #r ] whd in ⊢ (?%?); //;
1218qed.
1219
1220lemma zero_ext_lessdef:
1221  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2).
1222#n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //
1223qed.
1224
1225lemma sign_ext_lessdef:
1226  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
1227#n #v1 #v2 #H inversion H;//;#v #e1 #e2 <e1 in H >e2 //;
1228qed.
1229(*
1230Lemma singleoffloat_lessdef:
1231  forall v1 v2, lessdef v1 v2 -> lessdef (singleoffloat v1) (singleoffloat v2).
1232Proof.
1233  intros; inv H; simpl; auto.
1234Qed.
1235
1236End Val.
1237*)
Note: See TracBrowser for help on using the repository browser.