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.
Require Import Coqlib.
Require Import Integers.
Parameter float:
Type.
(* the type of IEE754 doubles *)
Definition swap_float_cmp_result r :=
match r with
|
FCunordered =>
FCunordered
|
FCless =>
FCgreater
|
FCequal =>
FCequal
|
FCgreater =>
FCless
end.
Module Float.
Parameter zero:
float.
(* the float +0.0 *)
Axiom eq_dec:
forall (
f1 f2:
float), {
f1 =
f2} + {
f1 <>
f2}.
Arithmetic operations
Parameter neg:
float ->
float.
(* opposite (change sign) *)
Parameter abs:
float ->
float.
(* absolute value (set sign to +) *)
Parameter singleoffloat:
float ->
float.
(* conversion to single precision *)
Parameter intoffloat:
float ->
int.
(* conversion to signed 32-bit int *)
Parameter intuoffloat:
float ->
int.
(* conversion to unsigned 32-bit int *)
Parameter floatofint:
int ->
float.
(* conversion from signed 32-bit int *)
Parameter floatofintu:
int ->
float.
(* conversion from unsigned 32-bit int *)
Parameter add:
float ->
float ->
float.
(* addition *)
Parameter sub:
float ->
float ->
float.
(* subtraction *)
Parameter mul:
float ->
float ->
float.
(* multiplication *)
Parameter div:
float ->
float ->
float.
(* division *)
Comparisons
Parameter internal_cmp:
float ->
float ->
float_cmp_result.
Definition cmp (
c:
comparison) (
x y:
float) :=
match tt with tt =>
match c,
internal_cmp x y with
|
Ceq,
FCequal =>
true
|
Cne,
FCunordered =>
true
|
Cne,
FCless =>
true
|
Cne,
FCgreater =>
true
|
Clt,
FCless =>
true
|
Cle,
FCless =>
true
|
Cle,
FCequal =>
true
|
Cgt,
FCgreater =>
true
|
Cge,
FCgreater =>
true
|
Cge,
FCequal =>
true
|
_,
_ =>
false
end end.
Conversions between floats and their concrete in-memory representation
as a sequence of 64 bits (double precision) or 32 bits (single precision).
Parameter bits_of_double:
float ->
int64.
Parameter double_of_bits:
int64 ->
float.
Parameter bits_of_single:
float ->
int.
Parameter single_of_bits:
int ->
float.
Definition from_words (
hi lo:
int) :
float :=
double_of_bits
(
Int64.or (
Int64.shl (
Int64.repr (
Int.unsigned hi)) (
Int64.repr 32))
(
Int64.repr (
Int.unsigned lo))).
Below are the only properties of floating-point arithmetic that we
rely on in the compiler proof.
Axiom addf_commut:
forall f1 f2,
add f1 f2 =
add f2 f1.
Axiom subf_addf_opp:
forall f1 f2,
sub f1 f2 =
add f1 (
neg f2).
Axiom singleoffloat_idem:
forall f,
singleoffloat (
singleoffloat f) =
singleoffloat f.
Axiom internal_cmp_swap:
forall x y,
internal_cmp x y =
swap_float_cmp_result (
internal_cmp y x).
Properties of comparisons.
Lemma cmp_swap:
forall c x y,
cmp (
swap_comparison c)
x y =
cmp c y x.
Proof.
Lemma cmp_ne_eq:
forall f1 f2,
cmp Cne f1 f2 =
negb (
cmp Ceq f1 f2).
Proof.
Lemma cmp_le_lt_eq:
forall f1 f2,
cmp Cle f1 f2 =
cmp Clt f1 f2 ||
cmp Ceq f1 f2.
Proof.
by unfold cmp;
intros x y;
simpl;
destruct internal_cmp.
Qed.
Lemma cmp_ge_gt_eq:
forall f1 f2,
cmp Cge f1 f2 =
cmp Cgt f1 f2 ||
cmp Ceq f1 f2.
Proof.
Lemma cmp_lt_eq_false:
forall x y,
cmp Clt x y ->
cmp Ceq x y =
false.
Proof.
by unfold cmp;
intros x y;
simpl;
destruct internal_cmp.
Qed.
Lemma cmp_gt_eq_false:
forall x y,
cmp Cgt x y ->
cmp Ceq x y =
false.
Proof.
by unfold cmp;
intros x y;
simpl;
destruct internal_cmp.
Qed.
Lemma cmp_lt_gt_false:
forall x y,
cmp Clt x y ->
cmp Cgt x y =
false.
Proof.
by unfold cmp;
intros x y;
simpl;
destruct internal_cmp.
Qed.
Definition unordered (
x y:
float) :=
negb (
cmp Cle x y) &&
negb (
cmp Ceq x y) &&
negb (
cmp Cgt x y).
Lemma unordered_internal:
forall x y,
unordered x y = (
match internal_cmp x y with
|
FCunordered =>
true
|
_ =>
false end).
Proof.
by intros;
unfold unordered,
cmp;
simpl;
destruct internal_cmp.
Qed.
Properties of conversions to/from in-memory representation.
The double-precision conversions are bijective (one-to-one).
The single-precision conversions lose precision exactly
as described by singleoffloat rounding.
Axiom double_of_bits_of_double:
forall f,
double_of_bits (
bits_of_double f) =
f.
Axiom single_of_bits_of_single:
forall f,
single_of_bits (
bits_of_single f) =
singleoffloat f.
Axiom bits_of_singleoffloat:
forall f,
bits_of_single (
singleoffloat f) =
bits_of_single f.
Axiom singleoffloat_of_bits:
forall b,
singleoffloat (
single_of_bits b) =
single_of_bits b.
Conversions between floats and unsigned ints can be defined
in terms of conversions between floats and signed ints.
(Most processors provide only the latter, forcing the compiler
to emulate the former.)
Definition ox8000_0000 :=
Int.repr Int.half_modulus.
(* 0x8000_0000 *)
Axiom floatofintu_floatofint_1:
forall x,
Int.ltu x ox8000_0000 =
true ->
floatofintu x =
floatofint x.
Axiom floatofintu_floatofint_2:
forall x,
Int.ltu x ox8000_0000 =
false ->
floatofintu x =
add (
floatofint (
Int.sub x ox8000_0000))
(
floatofintu ox8000_0000).
Axiom intuoffloat_intoffloat_1:
forall x,
cmp Clt x (
floatofintu ox8000_0000) =
true ->
intuoffloat x =
intoffloat x.
Axiom intuoffloat_intoffloat_2:
forall x,
cmp Clt x (
floatofintu ox8000_0000) =
false ->
intuoffloat x =
Int.add (
intoffloat (
sub x (
floatofintu ox8000_0000)))
ox8000_0000.
Conversions from ints to floats can be defined as bitwise manipulations
over the in-memory representation. This is what the PowerPC port does.
The trick is that from_words 0x4330_0000 x is the float
2^52 + floatofintu x.
Definition ox4330_0000 :=
Int.repr 1127219200.
(* 0x4330_0000 *)
Axiom floatofintu_from_words:
forall x,
floatofintu x =
sub (
from_words ox4330_0000 x) (
from_words ox4330_0000 Int.zero).
Axiom floatofint_from_words:
forall x,
floatofint x =
sub (
from_words ox4330_0000 (
Int.add x ox8000_0000))
(
from_words ox4330_0000 ox8000_0000).
End Float.