[3] | 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 | |
---|
| 23 | include "Coqlib.ma". |
---|
| 24 | include "Integers.ma". |
---|
| 25 | |
---|
| 26 | naxiom float: Type. |
---|
| 27 | |
---|
| 28 | (*Module Float.*) |
---|
| 29 | |
---|
| 30 | naxiom Fzero: float. |
---|
| 31 | naxiom Fone: float. |
---|
| 32 | |
---|
| 33 | naxiom Fneg: float → float. |
---|
| 34 | naxiom Fabs: float → float. |
---|
| 35 | naxiom singleoffloat: float → float. |
---|
| 36 | naxiom intoffloat: float → int. |
---|
| 37 | naxiom intuoffloat: float → int. |
---|
| 38 | naxiom floatofint: int → float. |
---|
| 39 | naxiom floatofintu: int → float. |
---|
| 40 | |
---|
| 41 | naxiom Fadd: float → float → float. |
---|
| 42 | naxiom Fsub: float → float → float. |
---|
| 43 | naxiom Fmul: float → float → float. |
---|
| 44 | naxiom Fdiv: float → float → float. |
---|
| 45 | |
---|
| 46 | naxiom Fcmp: comparison → float → float → bool. |
---|
| 47 | |
---|
| 48 | naxiom 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 | |
---|
| 53 | naxiom addf_commut: ∀f1,f2. Fadd f1 f2 = Fadd f2 f1. |
---|
| 54 | |
---|
| 55 | naxiom subf_addf_opp: ∀f1,f2. Fsub f1 f2 = Fadd f1 (Fneg f2). |
---|
| 56 | |
---|
| 57 | naxiom singleoffloat_idem: |
---|
| 58 | ∀f. singleoffloat (singleoffloat f) = singleoffloat f. |
---|
| 59 | |
---|
| 60 | naxiom Fcmp_ne_eq: |
---|
| 61 | ∀ f1,f2. Fcmp Cne f1 f2 = ¬(Fcmp Ceq f1 f2). |
---|
| 62 | naxiom Fcmp_le_lt_eq: |
---|
| 63 | ∀ f1,f2. Fcmp Cle f1 f2 = (Fcmp Clt f1 f2 ∨ Fcmp Ceq f1 f2). |
---|
| 64 | naxiom Fcmp_ge_gt_eq: |
---|
| 65 | ∀f1,f2. Fcmp Cge f1 f2 = (Fcmp Cgt f1 f2 ∨ Fcmp Ceq f1 f2). |
---|
| 66 | |
---|
| 67 | naxiom Feq_zero_true: Fcmp Ceq Fzero Fzero = true. |
---|
| 68 | naxiom Feq_zero_false: ∀f. f ≠ Fzero → Fcmp Ceq f Fzero = false. |
---|
| 69 | |
---|
| 70 | (*End Float.*) |
---|