(* *********************************************************************) (* *) (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the GNU General Public License as published by *) (* the Free Software Foundation, either version 2 of the License, or *) (* (at your option) any later version. This file is also distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (* * Axiomatization of floating-point numbers. *) (* * In contrast with what we do with machine integers, we do not bother to formalize precisely IEEE floating-point arithmetic. Instead, we simply axiomatize a type [float] for IEEE double-precision floats and the associated operations. *) include "utilities/Coqlib.ma". include "common/Integers.ma". axiom float: Type[0]. (*Module Float.*) axiom Fzero: float. axiom Fone: float. axiom Fneg: float → float. axiom Fabs: float → float. axiom singleoffloat: float → float. axiom intoffloat: ∀n. float → BitVector n. axiom intuoffloat: ∀n. float → BitVector n. axiom floatofint: ∀n. BitVector n → float. axiom floatofintu: ∀n. BitVector n → float. axiom Fadd: float → float → float. axiom Fsub: float → float → float. axiom Fmul: float → float → float. axiom Fdiv: float → float → float. axiom Fcmp: comparison → float → float → bool. axiom eq_dec: ∀f1,f2: float. (f1 = f2) + (f1 ≠ f2). (* * Below are the only properties of floating-point arithmetic that we rely on in the compiler proof. *) axiom addf_commut: ∀f1,f2. Fadd f1 f2 = Fadd f2 f1. axiom subf_addf_opp: ∀f1,f2. Fsub f1 f2 = Fadd f1 (Fneg f2). axiom singleoffloat_idem: ∀f. singleoffloat (singleoffloat f) = singleoffloat f. axiom Fcmp_ne_eq: ∀ f1,f2. Fcmp Cne f1 f2 = ¬(Fcmp Ceq f1 f2). axiom Fcmp_le_lt_eq: ∀ f1,f2. Fcmp Cle f1 f2 = (Fcmp Clt f1 f2 ∨ Fcmp Ceq f1 f2). axiom Fcmp_ge_gt_eq: ∀f1,f2. Fcmp Cge f1 f2 = (Fcmp Cgt f1 f2 ∨ Fcmp Ceq f1 f2). axiom Feq_zero_true: Fcmp Ceq Fzero Fzero = true. axiom Feq_zero_false: ∀f. f ≠ Fzero → Fcmp Ceq f Fzero = false. (*End Float.*)