source: src/common/Values.ma @ 751

Last change on this file since 751 was 751, checked in by campbell, 10 years ago

Initial version of the Cminor syntax and semantics.

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
268definition eval_bool_of_val : val → res bool ≝
269λv. match v with
270[ Vint i ⇒ OK ? (notb (eq i zero))
271| Vnull _ ⇒ OK ? false
272| Vptr _ _ _ _ ⇒ OK ? true
273| _ ⇒ Error ?
274].
275
276definition neg : val → val ≝ λv.
277  match v with
278  [ Vint n ⇒ Vint (neg n)
279  | _ ⇒ Vundef
280  ].
281
282definition negf : val → val ≝ λv.
283  match v with
284  [ Vfloat f ⇒ Vfloat (Fneg f)
285  | _ => Vundef
286  ].
287
288definition absf : val → val ≝ λv.
289  match v with
290  [ Vfloat f ⇒ Vfloat (Fabs f)
291  | _ ⇒ Vundef
292  ].
293
294definition intoffloat : val → val ≝ λv.
295  match v with
296  [ Vfloat f ⇒ Vint (intoffloat f)
297  | _ ⇒ Vundef
298  ].
299
300definition intuoffloat : val → val ≝ λv.
301  match v with
302  [ Vfloat f ⇒ Vint (intuoffloat f)
303  | _ ⇒ Vundef
304  ].
305
306definition floatofint : val → val ≝ λv.
307  match v with
308  [ Vint n ⇒ Vfloat (floatofint n)
309  | _ ⇒ Vundef
310  ].
311
312definition floatofintu : val → val ≝ λv.
313  match v with
314  [ Vint n ⇒ Vfloat (floatofintu n)
315  | _ ⇒ Vundef
316  ].
317
318definition notint : val → val ≝ λv.
319  match v with
320  [ Vint n ⇒ Vint (xor n mone)
321  | _ ⇒ Vundef
322  ].
323 
324(* FIXME: switch to alias, or rename, or … *)
325definition int_eq : int → int → bool ≝ eq.
326definition notbool : val → val ≝ λv.
327  match v with
328  [ Vint n ⇒ of_bool (int_eq n zero)
329  | Vptr _ b _ ofs ⇒ Vfalse
330  | Vnull _ ⇒ Vtrue
331  | _ ⇒ Vundef
332  ].
333
334definition zero_ext ≝ λnbits: nat. λv: val.
335  match v with
336  [ Vint n ⇒ Vint (zero_ext nbits n)
337  | _ ⇒ Vundef
338  ].
339
340definition sign_ext ≝ λnbits:nat. λv:val.
341  match v with
342  [ Vint i ⇒ Vint (sign_ext nbits i)
343  | _ ⇒ Vundef
344  ].
345
346definition singleoffloat : val → val ≝ λv.
347  match v with
348  [ Vfloat f ⇒ Vfloat (singleoffloat f)
349  | _ ⇒ Vundef
350  ].
351
352(* TODO: add zero to null? *)
353definition add ≝ λv1,v2: val.
354  match v1 with
355  [ Vint n1 ⇒ match v2 with
356    [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
357    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
358    | _ ⇒ Vundef ]
359  | Vptr r b1 p ofs1 ⇒ match v2 with
360    [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2)
361    | _ ⇒ Vundef ]
362  | _ ⇒ Vundef ].
363
364definition sub ≝ λv1,v2: val.
365  match v1 with
366  [ Vint n1 ⇒ match v2 with
367    [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
368    | _ ⇒ Vundef ]
369  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
370    [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)
371    | Vptr r2 b2 p2 ofs2 ⇒
372        if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef
373    | _ ⇒ Vundef ]
374  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
375  | _ ⇒ Vundef ].
376
377definition mul ≝ λv1, v2: val.
378  match v1 with
379  [ Vint n1 ⇒ match v2 with
380    [ Vint n2 ⇒ Vint (mul n1 n2)
381    | _ ⇒ Vundef ]
382  | _ ⇒ Vundef ].
383(*
384definition divs ≝ λv1, v2: val.
385  match v1 with
386  [ Vint n1 ⇒ match v2 with
387    [ Vint n2 ⇒ Vint (divs n1 n2)
388    | _ ⇒ Vundef ]
389  | _ ⇒ Vundef ].
390
391Definition mods (v1 v2: val): val :=
392  match v1, v2 with
393  | Vint n1, Vint n2 =>
394      if Int.eq n2 Int.zero then Vundef else Vint(Int.mods n1 n2)
395  | _, _ => Vundef
396  end.
397
398Definition divu (v1 v2: val): val :=
399  match v1, v2 with
400  | Vint n1, Vint n2 =>
401      if Int.eq n2 Int.zero then Vundef else Vint(Int.divu n1 n2)
402  | _, _ => Vundef
403  end.
404
405Definition modu (v1 v2: val): val :=
406  match v1, v2 with
407  | Vint n1, Vint n2 =>
408      if Int.eq n2 Int.zero then Vundef else Vint(Int.modu n1 n2)
409  | _, _ => Vundef
410  end.
411*)
412definition v_and ≝ λv1, v2: val.
413  match v1 with
414  [ Vint n1 ⇒ match v2 with
415    [ Vint n2 ⇒ Vint (i_and n1 n2)
416    | _ ⇒ Vundef ]
417  | _ ⇒ Vundef ].
418
419definition or ≝ λv1, v2: val.
420  match v1 with
421  [ Vint n1 ⇒ match v2 with
422    [ Vint n2 ⇒ Vint (or n1 n2)
423    | _ ⇒ Vundef ]
424  | _ ⇒ Vundef ].
425
426definition xor ≝ λv1, v2: val.
427  match v1 with
428  [ Vint n1 ⇒ match v2 with
429    [ Vint n2 ⇒ Vint (xor n1 n2)
430    | _ ⇒ Vundef ]
431  | _ ⇒ Vundef ].
432(*
433Definition shl (v1 v2: val): val :=
434  match v1, v2 with
435  | Vint n1, Vint n2 =>
436     if Int.ltu n2 Int.iwordsize
437     then Vint(Int.shl n1 n2)
438     else Vundef
439  | _, _ => Vundef
440  end.
441
442Definition shr (v1 v2: val): val :=
443  match v1, v2 with
444  | Vint n1, Vint n2 =>
445     if Int.ltu n2 Int.iwordsize
446     then Vint(Int.shr n1 n2)
447     else Vundef
448  | _, _ => Vundef
449  end.
450
451Definition shr_carry (v1 v2: val): val :=
452  match v1, v2 with
453  | Vint n1, Vint n2 =>
454     if Int.ltu n2 Int.iwordsize
455     then Vint(Int.shr_carry n1 n2)
456     else Vundef
457  | _, _ => Vundef
458  end.
459
460Definition shrx (v1 v2: val): val :=
461  match v1, v2 with
462  | Vint n1, Vint n2 =>
463     if Int.ltu n2 Int.iwordsize
464     then Vint(Int.shrx n1 n2)
465     else Vundef
466  | _, _ => Vundef
467  end.
468
469Definition shru (v1 v2: val): val :=
470  match v1, v2 with
471  | Vint n1, Vint n2 =>
472     if Int.ltu n2 Int.iwordsize
473     then Vint(Int.shru n1 n2)
474     else Vundef
475  | _, _ => Vundef
476  end.
477
478Definition rolm (v: val) (amount mask: int): val :=
479  match v with
480  | Vint n => Vint(Int.rolm n amount mask)
481  | _ => Vundef
482  end.
483
484Definition ror (v1 v2: val): val :=
485  match v1, v2 with
486  | Vint n1, Vint n2 =>
487     if Int.ltu n2 Int.iwordsize
488     then Vint(Int.ror n1 n2)
489     else Vundef
490  | _, _ => Vundef
491  end.
492*)
493definition addf ≝ λv1,v2: val.
494  match v1 with
495  [ Vfloat f1 ⇒ match v2 with
496    [ Vfloat f2 ⇒ Vfloat (Fadd f1 f2)
497    | _ ⇒ Vundef ]
498  | _ ⇒ Vundef ].
499
500definition subf ≝ λv1,v2: val.
501  match v1 with
502  [ Vfloat f1 ⇒ match v2 with
503    [ Vfloat f2 ⇒ Vfloat (Fsub f1 f2)
504    | _ ⇒ Vundef ]
505  | _ ⇒ Vundef ].
506
507definition mulf ≝ λv1,v2: val.
508  match v1 with
509  [ Vfloat f1 ⇒ match v2 with
510    [ Vfloat f2 ⇒ Vfloat (Fmul f1 f2)
511    | _ ⇒ Vundef ]
512  | _ ⇒ Vundef ].
513
514definition divf ≝ λv1,v2: val.
515  match v1 with
516  [ Vfloat f1 ⇒ match v2 with
517    [ Vfloat f2 ⇒ Vfloat (Fdiv f1 f2)
518    | _ ⇒ Vundef ]
519  | _ ⇒ Vundef ].
520
521definition cmp_match : comparison → val ≝ λc.
522  match c with
523  [ Ceq ⇒ Vtrue
524  | Cne ⇒ Vfalse
525  | _   ⇒ Vundef
526  ].
527
528definition cmp_mismatch : comparison → val ≝ λc.
529  match c with
530  [ Ceq ⇒ Vfalse
531  | Cne ⇒ Vtrue
532  | _   ⇒ Vundef
533  ].
534
535definition cmp_offset ≝
536λc: comparison. λx,y:offset.
537  match c with
538  [ Ceq ⇒  eq_offset x y
539  | Cne ⇒ ¬eq_offset x y
540  | Clt ⇒  lt_offset x y
541  | Cle ⇒ ¬lt_offset y x
542  | Cgt ⇒  lt_offset y x
543  | Cge ⇒ ¬lt_offset x y
544  ].
545
546definition cmp ≝ λc: comparison. λv1,v2: val.
547  match v1 with
548  [ Vint n1 ⇒ match v2 with
549    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
550    | _ ⇒ Vundef ]
551  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
552    [ Vptr r2 b2 p2 ofs2 ⇒
553        if eq_block b1 b2
554        then of_bool (cmp_offset c ofs1 ofs2)
555        else cmp_mismatch c
556    | Vnull r2 ⇒ cmp_mismatch c
557    | _ ⇒ Vundef ]
558  | Vnull r1 ⇒ match v2 with
559    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
560    | Vnull r2 ⇒ cmp_match c
561    | _ ⇒ Vundef
562    ]
563  | _ ⇒ Vundef ].
564
565definition cmpu ≝ λc: comparison. λv1,v2: val.
566  match v1 with
567  [ Vint n1 ⇒ match v2 with
568    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
569    | _ ⇒ Vundef ]
570  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
571    [ Vptr r2 b2 p2 ofs2 ⇒
572        if eq_block b1 b2
573        then of_bool (cmp_offset c ofs1 ofs2)
574        else cmp_mismatch c
575    | Vnull r2 ⇒ cmp_mismatch c
576    | _ ⇒ Vundef ]
577  | Vnull r1 ⇒ match v2 with
578    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
579    | Vnull r2 ⇒ cmp_match c
580    | _ ⇒ Vundef
581    ]
582  | _ ⇒ Vundef ].
583
584definition cmpf ≝ λc: comparison. λv1,v2: val.
585  match v1 with
586  [ Vfloat f1 ⇒ match v2 with
587    [ Vfloat f2 ⇒ of_bool (Fcmp c f1 f2)
588    | _ ⇒ Vundef ]
589  | _ ⇒ Vundef ].
590
591(* * [load_result] is used in the memory model (library [Mem])
592  to post-process the results of a memory read.  For instance,
593  consider storing the integer value [0xFFF] on 1 byte at a
594  given address, and reading it back.  If it is read back with
595  chunk [Mint8unsigned], zero-extension must be performed, resulting
596  in [0xFF].  If it is read back as a [Mint8signed], sign-extension
597  is performed and [0xFFFFFFFF] is returned.   Type mismatches
598  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
599
600let rec load_result (chunk: memory_chunk) (v: val) ≝
601  match v with
602  [ Vint n ⇒
603    match chunk with
604    [ Mint8signed ⇒ Vint (sign_ext 8 n)
605    | Mint8unsigned ⇒ Vint (zero_ext 8 n)
606    | Mint16signed ⇒ Vint (sign_ext 16 n)
607    | Mint16unsigned ⇒ Vint (zero_ext 16 n)
608    | Mint32 ⇒ Vint n
609    | _ ⇒ Vundef
610    ]
611  | Vptr r b p ofs ⇒
612    match chunk with
613    [ Mpointer r' ⇒ if eq_region r r' then Vptr r b p ofs else Vundef
614    | _ ⇒ Vundef
615    ]
616  | Vnull r ⇒
617    match chunk with
618    [ Mpointer r' ⇒ if eq_region r r' then Vnull r else Vundef
619    | _ ⇒ Vundef
620    ]
621  | Vfloat f ⇒
622    match chunk with
623    [ Mfloat32 ⇒ Vfloat(singleoffloat f)
624    | Mfloat64 ⇒ Vfloat f
625    | _ ⇒ Vundef
626    ]
627  | _ ⇒ Vundef
628  ].
629
630(*
631(** Theorems on arithmetic operations. *)
632
633Theorem cast8unsigned_and:
634  forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
635Proof.
636  destruct x; simpl; auto. decEq.
637  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. vm_compute; auto.
638Qed.
639
640Theorem cast16unsigned_and:
641  forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
642Proof.
643  destruct x; simpl; auto. decEq.
644  change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto.
645Qed.
646
647Theorem istrue_not_isfalse:
648  forall v, is_false v -> is_true (notbool v).
649Proof.
650  destruct v; simpl; try contradiction.
651  intros. subst i. simpl. discriminate.
652Qed.
653
654Theorem isfalse_not_istrue:
655  forall v, is_true v -> is_false (notbool v).
656Proof.
657  destruct v; simpl; try contradiction.
658  intros. generalize (Int.eq_spec i Int.zero).
659  case (Int.eq i Int.zero); intro.
660  contradiction. simpl. auto.
661  auto.
662Qed.
663
664Theorem bool_of_true_val:
665  forall v, is_true v -> bool_of_val v true.
666Proof.
667  intro. destruct v; simpl; intros; try contradiction.
668  constructor; auto. constructor.
669Qed.
670
671Theorem bool_of_true_val2:
672  forall v, bool_of_val v true -> is_true v.
673Proof.
674  intros. inversion H; simpl; auto.
675Qed.
676
677Theorem bool_of_true_val_inv:
678  forall v b, is_true v -> bool_of_val v b -> b = true.
679Proof.
680  intros. inversion H0; subst v b; simpl in H; auto.
681Qed.
682
683Theorem bool_of_false_val:
684  forall v, is_false v -> bool_of_val v false.
685Proof.
686  intro. destruct v; simpl; intros; try contradiction.
687  subst i;  constructor.
688Qed.
689
690Theorem bool_of_false_val2:
691  forall v, bool_of_val v false -> is_false v.
692Proof.
693  intros. inversion H; simpl; auto.
694Qed.
695
696Theorem bool_of_false_val_inv:
697  forall v b, is_false v -> bool_of_val v b -> b = false.
698Proof.
699  intros. inversion H0; subst v b; simpl in H.
700  congruence. auto. contradiction.
701Qed.
702
703Theorem notbool_negb_1:
704  forall b, of_bool (negb b) = notbool (of_bool b).
705Proof.
706  destruct b; reflexivity.
707Qed.
708
709Theorem notbool_negb_2:
710  forall b, of_bool b = notbool (of_bool (negb b)).
711Proof.
712  destruct b; reflexivity.
713Qed.
714
715Theorem notbool_idem2:
716  forall b, notbool(notbool(of_bool b)) = of_bool b.
717Proof.
718  destruct b; reflexivity.
719Qed.
720
721Theorem notbool_idem3:
722  forall x, notbool(notbool(notbool x)) = notbool x.
723Proof.
724  destruct x; simpl; auto.
725  case (Int.eq i Int.zero); reflexivity.
726Qed.
727
728Theorem add_commut: forall x y, add x y = add y x.
729Proof.
730  destruct x; destruct y; simpl; auto.
731  decEq. apply Int.add_commut.
732Qed.
733
734Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
735Proof.
736  destruct x; destruct y; destruct z; simpl; auto.
737  rewrite Int.add_assoc; auto.
738  rewrite Int.add_assoc; auto.
739  decEq. decEq. apply Int.add_commut.
740  decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc.
741  decEq. apply Int.add_commut.
742  decEq. rewrite Int.add_assoc. auto.
743Qed.
744
745Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
746Proof.
747  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut.
748Qed.
749
750Theorem add_permut_4:
751  forall x y z t, add (add x y) (add z t) = add (add x z) (add y t).
752Proof.
753  intros. rewrite add_permut. rewrite add_assoc.
754  rewrite add_permut. symmetry. apply add_assoc.
755Qed.
756
757Theorem neg_zero: neg Vzero = Vzero.
758Proof.
759  reflexivity.
760Qed.
761
762Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
763Proof.
764  destruct x; destruct y; simpl; auto. decEq. apply Int.neg_add_distr.
765Qed.
766
767Theorem sub_zero_r: forall x, sub Vzero x = neg x.
768Proof.
769  destruct x; simpl; auto.
770Qed.
771
772Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)).
773Proof.
774  destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto.
775Qed.
776
777Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y).
778Proof.
779  intros. unfold sub, add.
780  destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto.
781Qed.
782
783Theorem sub_add_l:
784  forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i).
785Proof.
786  destruct v1; destruct v2; intros; simpl; auto.
787  rewrite Int.sub_add_l. auto.
788  rewrite Int.sub_add_l. auto.
789  case (zeq b b0); intro. rewrite Int.sub_add_l. auto. reflexivity.
790Qed.
791
792Theorem sub_add_r:
793  forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)).
794Proof.
795  destruct v1; destruct v2; intros; simpl; auto.
796  rewrite Int.sub_add_r. auto.
797  repeat rewrite Int.sub_add_opp. decEq.
798  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
799  decEq. repeat rewrite Int.sub_add_opp.
800  rewrite Int.add_assoc. decEq. apply Int.neg_add_distr.
801  case (zeq b b0); intro. simpl. decEq.
802  repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq.
803  apply Int.neg_add_distr.
804  reflexivity.
805Qed.
806
807Theorem mul_commut: forall x y, mul x y = mul y x.
808Proof.
809  destruct x; destruct y; simpl; auto. decEq. apply Int.mul_commut.
810Qed.
811
812Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).
813Proof.
814  destruct x; destruct y; destruct z; simpl; auto.
815  decEq. apply Int.mul_assoc.
816Qed.
817
818Theorem mul_add_distr_l:
819  forall x y z, mul (add x y) z = add (mul x z) (mul y z).
820Proof.
821  destruct x; destruct y; destruct z; simpl; auto.
822  decEq. apply Int.mul_add_distr_l.
823Qed.
824
825
826Theorem mul_add_distr_r:
827  forall x y z, mul x (add y z) = add (mul x y) (mul x z).
828Proof.
829  destruct x; destruct y; destruct z; simpl; auto.
830  decEq. apply Int.mul_add_distr_r.
831Qed.
832
833Theorem mul_pow2:
834  forall x n logn,
835  Int.is_power2 n = Some logn ->
836  mul x (Vint n) = shl x (Vint logn).
837Proof.
838  intros; destruct x; simpl; auto.
839  change 32 with (Z_of_nat Int.wordsize).
840  rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto.
841Qed. 
842
843Theorem mods_divs:
844  forall x y, mods x y = sub x (mul (divs x y) y).
845Proof.
846  destruct x; destruct y; simpl; auto.
847  case (Int.eq i0 Int.zero); simpl. auto. decEq. apply Int.mods_divs.
848Qed.
849
850Theorem modu_divu:
851  forall x y, modu x y = sub x (mul (divu x y) y).
852Proof.
853  destruct x; destruct y; simpl; auto.
854  generalize (Int.eq_spec i0 Int.zero);
855  case (Int.eq i0 Int.zero); simpl. auto.
856  intro. decEq. apply Int.modu_divu. auto.
857Qed.
858
859Theorem divs_pow2:
860  forall x n logn,
861  Int.is_power2 n = Some logn ->
862  divs x (Vint n) = shrx x (Vint logn).
863Proof.
864  intros; destruct x; simpl; auto.
865  change 32 with (Z_of_nat Int.wordsize).
866  rewrite (Int.is_power2_range _ _ H).
867  generalize (Int.eq_spec n Int.zero);
868  case (Int.eq n Int.zero); intro.
869  subst n. compute in H. discriminate.
870  decEq. apply Int.divs_pow2. auto.
871Qed.
872
873Theorem divu_pow2:
874  forall x n logn,
875  Int.is_power2 n = Some logn ->
876  divu x (Vint n) = shru x (Vint logn).
877Proof.
878  intros; destruct x; simpl; auto.
879  change 32 with (Z_of_nat Int.wordsize).
880  rewrite (Int.is_power2_range _ _ H).
881  generalize (Int.eq_spec n Int.zero);
882  case (Int.eq n Int.zero); intro.
883  subst n. compute in H. discriminate.
884  decEq. apply Int.divu_pow2. auto.
885Qed.
886
887Theorem modu_pow2:
888  forall x n logn,
889  Int.is_power2 n = Some logn ->
890  modu x (Vint n) = and x (Vint (Int.sub n Int.one)).
891Proof.
892  intros; destruct x; simpl; auto.
893  generalize (Int.eq_spec n Int.zero);
894  case (Int.eq n Int.zero); intro.
895  subst n. compute in H. discriminate.
896  decEq. eapply Int.modu_and; eauto.
897Qed.
898
899Theorem and_commut: forall x y, and x y = and y x.
900Proof.
901  destruct x; destruct y; simpl; auto. decEq. apply Int.and_commut.
902Qed.
903
904Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
905Proof.
906  destruct x; destruct y; destruct z; simpl; auto.
907  decEq. apply Int.and_assoc.
908Qed.
909
910Theorem or_commut: forall x y, or x y = or y x.
911Proof.
912  destruct x; destruct y; simpl; auto. decEq. apply Int.or_commut.
913Qed.
914
915Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
916Proof.
917  destruct x; destruct y; destruct z; simpl; auto.
918  decEq. apply Int.or_assoc.
919Qed.
920
921Theorem xor_commut: forall x y, xor x y = xor y x.
922Proof.
923  destruct x; destruct y; simpl; auto. decEq. apply Int.xor_commut.
924Qed.
925
926Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
927Proof.
928  destruct x; destruct y; destruct z; simpl; auto.
929  decEq. apply Int.xor_assoc.
930Qed.
931
932Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y.
933Proof.
934  destruct x; destruct y; simpl; auto.
935  case (Int.ltu i0 Int.iwordsize); auto.
936  decEq. symmetry. apply Int.shl_mul.
937Qed.
938
939Theorem shl_rolm:
940  forall x n,
941  Int.ltu n Int.iwordsize = true ->
942  shl x (Vint n) = rolm x n (Int.shl Int.mone n).
943Proof.
944  intros; destruct x; simpl; auto.
945  rewrite H. decEq. apply Int.shl_rolm. exact H.
946Qed.
947
948Theorem shru_rolm:
949  forall x n,
950  Int.ltu n Int.iwordsize = true ->
951  shru x (Vint n) = rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n).
952Proof.
953  intros; destruct x; simpl; auto.
954  rewrite H. decEq. apply Int.shru_rolm. exact H.
955Qed.
956
957Theorem shrx_carry:
958  forall x y,
959  add (shr x y) (shr_carry x y) = shrx x y.
960Proof.
961  destruct x; destruct y; simpl; auto.
962  case (Int.ltu i0 Int.iwordsize); auto.
963  simpl. decEq. apply Int.shrx_carry.
964Qed.
965
966Theorem or_rolm:
967  forall x n m1 m2,
968  or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2).
969Proof.
970  intros; destruct x; simpl; auto.
971  decEq. apply Int.or_rolm.
972Qed.
973
974Theorem rolm_rolm:
975  forall x n1 m1 n2 m2,
976  rolm (rolm x n1 m1) n2 m2 =
977    rolm x (Int.modu (Int.add n1 n2) Int.iwordsize)
978           (Int.and (Int.rol m1 n2) m2).
979Proof.
980  intros; destruct x; simpl; auto.
981  decEq.
982  apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
983Qed.
984
985Theorem rolm_zero:
986  forall x m,
987  rolm x Int.zero m = and x (Vint m).
988Proof.
989  intros; destruct x; simpl; auto. decEq. apply Int.rolm_zero.
990Qed.
991
992Theorem addf_commut: forall x y, addf x y = addf y x.
993Proof.
994  destruct x; destruct y; simpl; auto. decEq. apply Float.addf_commut.
995Qed.
996
997Lemma negate_cmp_mismatch:
998  forall c,
999  cmp_mismatch (negate_comparison c) = notbool(cmp_mismatch c).
1000Proof.
1001  destruct c; reflexivity.
1002Qed.
1003
1004Theorem negate_cmp:
1005  forall c x y,
1006  cmp (negate_comparison c) x y = notbool (cmp c x y).
1007Proof.
1008  destruct x; destruct y; simpl; auto.
1009  rewrite Int.negate_cmp. apply notbool_negb_1.
1010  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
1011  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
1012  case (zeq b b0); intro.
1013  rewrite Int.negate_cmp. apply notbool_negb_1.
1014  apply negate_cmp_mismatch.
1015Qed.
1016
1017Theorem negate_cmpu:
1018  forall c x y,
1019  cmpu (negate_comparison c) x y = notbool (cmpu c x y).
1020Proof.
1021  destruct x; destruct y; simpl; auto.
1022  rewrite Int.negate_cmpu. apply notbool_negb_1.
1023  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
1024  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
1025  case (zeq b b0); intro.
1026  rewrite Int.negate_cmpu. apply notbool_negb_1.
1027  apply negate_cmp_mismatch.
1028Qed.
1029
1030Lemma swap_cmp_mismatch:
1031  forall c, cmp_mismatch (swap_comparison c) = cmp_mismatch c.
1032Proof.
1033  destruct c; reflexivity.
1034Qed.
1035 
1036Theorem swap_cmp:
1037  forall c x y,
1038  cmp (swap_comparison c) x y = cmp c y x.
1039Proof.
1040  destruct x; destruct y; simpl; auto.
1041  rewrite Int.swap_cmp. auto.
1042  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
1043  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
1044  case (zeq b b0); intro.
1045  subst b0. rewrite zeq_true. rewrite Int.swap_cmp. auto.
1046  rewrite zeq_false. apply swap_cmp_mismatch. auto.
1047Qed.
1048
1049Theorem swap_cmpu:
1050  forall c x y,
1051  cmpu (swap_comparison c) x y = cmpu c y x.
1052Proof.
1053  destruct x; destruct y; simpl; auto.
1054  rewrite Int.swap_cmpu. auto.
1055  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
1056  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
1057  case (zeq b b0); intro.
1058  subst b0. rewrite zeq_true. rewrite Int.swap_cmpu. auto.
1059  rewrite zeq_false. apply swap_cmp_mismatch. auto.
1060Qed.
1061
1062Theorem negate_cmpf_eq:
1063  forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2.
1064Proof.
1065  destruct v1; destruct v2; simpl; auto.
1066  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1.
1067  apply notbool_idem2.
1068Qed.
1069
1070Theorem negate_cmpf_ne:
1071  forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.
1072Proof.
1073  destruct v1; destruct v2; simpl; auto.
1074  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. auto.
1075Qed.
1076
1077Lemma or_of_bool:
1078  forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2).
1079Proof.
1080  destruct b1; destruct b2; reflexivity.
1081Qed.
1082
1083Theorem cmpf_le:
1084  forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2).
1085Proof.
1086  destruct v1; destruct v2; simpl; auto.
1087  rewrite or_of_bool. decEq. apply Float.cmp_le_lt_eq.
1088Qed.
1089
1090Theorem cmpf_ge:
1091  forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2).
1092Proof.
1093  destruct v1; destruct v2; simpl; auto.
1094  rewrite or_of_bool. decEq. apply Float.cmp_ge_gt_eq.
1095Qed.
1096
1097Definition is_bool (v: val) :=
1098  v = Vundef \/ v = Vtrue \/ v = Vfalse.
1099
1100Lemma of_bool_is_bool:
1101  forall b, is_bool (of_bool b).
1102Proof.
1103  destruct b; unfold is_bool; simpl; tauto.
1104Qed.
1105
1106Lemma undef_is_bool: is_bool Vundef.
1107Proof.
1108  unfold is_bool; tauto.
1109Qed.
1110
1111Lemma cmp_mismatch_is_bool:
1112  forall c, is_bool (cmp_mismatch c).
1113Proof.
1114  destruct c; simpl; unfold is_bool; tauto.
1115Qed.
1116
1117Lemma cmp_is_bool:
1118  forall c v1 v2, is_bool (cmp c v1 v2).
1119Proof.
1120  destruct v1; destruct v2; simpl; try apply undef_is_bool.
1121  apply of_bool_is_bool.
1122  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1123  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1124  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
1125Qed.
1126
1127Lemma cmpu_is_bool:
1128  forall c v1 v2, is_bool (cmpu c v1 v2).
1129Proof.
1130  destruct v1; destruct v2; simpl; try apply undef_is_bool.
1131  apply of_bool_is_bool.
1132  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1133  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1134  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
1135Qed.
1136
1137Lemma cmpf_is_bool:
1138  forall c v1 v2, is_bool (cmpf c v1 v2).
1139Proof.
1140  destruct v1; destruct v2; simpl;
1141  apply undef_is_bool || apply of_bool_is_bool.
1142Qed.
1143
1144Lemma notbool_is_bool:
1145  forall v, is_bool (notbool v).
1146Proof.
1147  destruct v; simpl.
1148  apply undef_is_bool. apply of_bool_is_bool.
1149  apply undef_is_bool. unfold is_bool; tauto.
1150Qed.
1151
1152Lemma notbool_xor:
1153  forall v, is_bool v -> v = xor (notbool v) Vone.
1154Proof.
1155  intros. elim H; intro. 
1156  subst v. reflexivity.
1157  elim H0; intro; subst v; reflexivity.
1158Qed.
1159
1160Lemma rolm_lt_zero:
1161  forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero).
1162Proof.
1163  intros. destruct v; simpl; auto.
1164  transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))).
1165  decEq. symmetry. rewrite Int.shru_rolm. auto. auto.
1166  rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto.
1167Qed.
1168
1169Lemma rolm_ge_zero:
1170  forall v,
1171  xor (rolm v Int.one Int.one) (Vint Int.one) = cmp Cge v (Vint Int.zero).
1172Proof.
1173  intros. rewrite rolm_lt_zero. destruct v; simpl; auto.
1174  destruct (Int.lt i Int.zero); auto.
1175Qed.
1176*)
1177(* * The ``is less defined'' relation between values.
1178    A value is less defined than itself, and [Vundef] is
1179    less defined than any value. *)
1180
1181inductive Val_lessdef: val → val → Prop ≝
1182  | lessdef_refl: ∀v. Val_lessdef v v
1183  | lessdef_undef: ∀v. Val_lessdef Vundef v.
1184
1185inductive lessdef_list: list val → list val → Prop ≝
1186  | lessdef_list_nil:
1187      lessdef_list (nil ?) (nil ?)
1188  | lessdef_list_cons:
1189      ∀v1,v2,vl1,vl2.
1190      Val_lessdef v1 v2 → lessdef_list vl1 vl2 →
1191      lessdef_list (v1 :: vl1) (v2 :: vl2).
1192
1193(*Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.*)
1194(*
1195lemma lessdef_list_inv:
1196  ∀vl1,vl2. lessdef_list vl1 vl2 → vl1 = vl2 ∨ in_list ? Vundef vl1.
1197#vl1 elim vl1;
1198[ #vl2 #H inversion H; /2/; #h1 #h2 #t1 #t2 #H1 #H2 #H3 #Hbad destruct
1199| #h #t #IH #vl2 #H
1200    inversion H;
1201    [ #H' destruct
1202    | #h1 #h2 #t1 #t2 #H1 #H2 #H3 #e1 #e2 destruct;
1203        elim H1;
1204        [ elim (IH t2 H2);
1205            [ #e destruct; /2/;
1206            | /3/ ]
1207        | /3/ ]
1208    ]
1209] qed.
1210*)
1211lemma load_result_lessdef:
1212  ∀chunk,v1,v2.
1213  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
1214#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 cases chunk
1215[ 8: #r ] whd in ⊢ (?%?); //;
1216qed.
1217
1218lemma zero_ext_lessdef:
1219  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2).
1220#n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //
1221qed.
1222
1223lemma sign_ext_lessdef:
1224  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
1225#n #v1 #v2 #H inversion H;//;#v #e1 #e2 <e1 in H >e2 //;
1226qed.
1227(*
1228Lemma singleoffloat_lessdef:
1229  forall v1 v2, lessdef v1 v2 -> lessdef (singleoffloat v1) (singleoffloat v2).
1230Proof.
1231  intros; inv H; simpl; auto.
1232Qed.
1233
1234End Val.
1235*)
Note: See TracBrowser for help on using the repository browser.