source: src/common/Values.ma @ 747

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

Merge the two AST files together (although some definitions still need to be
harmonised).

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