source: Deliverables/D3.1/C-semantics/Values.ma @ 636

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

A few definitions that will be useful for some preliminary rtlabs semantics.

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