source: src/common/Values.ma @ 744

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

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

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