source: src/common/Values.ma @ 891

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

Revise proofs affected by recent matita change.

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