source: src/common/Floats.ma @ 1298

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

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 2.7 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(* * Axiomatization of floating-point numbers. *)
17
18(* * In contrast with what we do with machine integers, we do not bother
19  to formalize precisely IEEE floating-point arithmetic.  Instead, we
20  simply axiomatize a type [float] for IEEE double-precision floats
21  and the associated operations.  *)
22
23include "utilities/Coqlib.ma".
24include "common/Integers.ma".
25
26axiom float: Type[0].
27
28(*Module Float.*)
29
30axiom Fzero: float.
31axiom Fone: float.
32
33axiom Fneg: float → float.
34axiom Fabs: float → float.
35axiom singleoffloat: float → float.
36axiom intoffloat: ∀n. float → BitVector n.
37axiom intuoffloat: ∀n. float → BitVector n.
38axiom floatofint: ∀n. BitVector n → float.
39axiom floatofintu: ∀n. BitVector n → float.
40
41axiom Fadd: float → float → float.
42axiom Fsub: float → float → float.
43axiom Fmul: float → float → float.
44axiom Fdiv: float → float → float.
45
46axiom Fcmp: comparison → float → float → bool.
47
48axiom eq_dec: ∀f1,f2: float. (f1 = f2) + (f1 ≠ f2).
49
50(* * Below are the only properties of floating-point arithmetic that we
51  rely on in the compiler proof. *)
52
53axiom addf_commut: ∀f1,f2. Fadd f1 f2 = Fadd f2 f1.
54
55axiom subf_addf_opp: ∀f1,f2. Fsub f1 f2 = Fadd f1 (Fneg f2).
56
57axiom singleoffloat_idem:
58  ∀f. singleoffloat (singleoffloat f) = singleoffloat f.
59
60axiom Fcmp_ne_eq:
61  ∀ f1,f2. Fcmp Cne f1 f2 = ¬(Fcmp Ceq f1 f2).
62axiom Fcmp_le_lt_eq:
63  ∀ f1,f2. Fcmp Cle f1 f2 = (Fcmp Clt f1 f2 ∨ Fcmp Ceq f1 f2).
64axiom Fcmp_ge_gt_eq:
65  ∀f1,f2. Fcmp Cge f1 f2 = (Fcmp Cgt f1 f2 ∨ Fcmp Ceq f1 f2).
66
67axiom Feq_zero_true: Fcmp Ceq Fzero Fzero = true.
68axiom Feq_zero_false: ∀f. f ≠ Fzero → Fcmp Ceq f Fzero = false.
69
70(*End Float.*)
Note: See TracBrowser for help on using the repository browser.