[isabelle] A formal model of IEEE-754 floating-point arit... · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] A formal model of IEEE-754 floating-point arit...

Email Gateway (Jun 07 2022 at 14:04):

From: Tjark Weber <tjark.weber@it.uu.se>
Dear floating-point enthusiasts,

As you may know, a formalization of IEEE-754 floating-point arithmetic
in Isabelle/HOL is readily available from the AFP [1].

The type "('e, 'f) float" of floating-point values that is defined in
this AFP entry is based on the bit-vector representation of floating-
point values. Specifically, the type contains several bit-vector
representations of the NaN ("Not-a-Number") value.

In contrast, SMT-LIB defines a floating-point theory [2] whose type of
floating-point values contains exactly one NaN value. (According to
SMT-LIB, this is "in agreement with Level 2 of IEEE 754-2008.")

This means that the two types are not isomorphic: we cannot (soundly)
map Isabelle's floating-point type to SMT-LIB's if we want to benefit
from the decision procedures for floating-point values that are
available in SMT solvers.

To address this, it seems clear to me that one should define a
floating-point type in Isabelle that corresponds to the SMT-LIB type,
i.e. that formalizes floating-point values at specification level 2 of
the IEEE standard.

My question then is: what to do with the current type of floating-point
values? Should it be retained, or replaced with the new type?

The bit-vector notation for floating-point values is undoubtedly
useful, but there is a many-to-one relationship between bit vectors and
floating-point data at specification level 2, so a (non-injective)
embedding function onto the new type would suffice to retain this
notation. Is there much point in reasoning about floating-point
operations at the representation level when a formalization of
floating-point data at specification level 2 is available?

Best,
Tjark

[1] https://www.isa-afp.org/entries/IEEE_Floating_Point.html
[2] https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

Email Gateway (Jun 07 2022 at 14:47):

From: Peter Lammich <lammich@in.tum.de>
Hi Tjark,

when I worked with the AFP entry, I try to identify all NaNs anyway, as
doing so makes proofs easier.

even for my formalization of LLVM floating point semantics, I currently
do not support distinguishing NaNs, as their semantics seems to be
implementation defined.

Email Gateway (Jun 07 2022 at 15:13):

From: Lennart Beringer <eberinge@cs.princeton.edu>
Hi Tjark,

I notice that the dependency graph of modules at https://flocq.gitlabpages.inria.fr/
has nodes IEEE754.Binary and BinarySingleNaN, the former importing the latter.
I'm not a "floating point enthusiast" and haven't used Flocq much myself but
maybe the relationship between the types defined in these modules is relevant for
this discussion, and treatments of this aspect could be harmonized between
different provers?

Best,

Lennart.

----- Forwarded Message -----
From: "Tjark Weber" <tjark.weber@it.uu.se>
To: "isabelle-users" <isabelle-users@cl.cam.ac.uk>
Cc: ly271@cam.ac.uk, hellauer@in.tum.de, fimmler@apple.com
Sent: Tuesday, 7 June, 2022 10:03:34
Subject: [isabelle] A formal model of IEEE-754 floating-point arithmetic: Specification level

Dear floating-point enthusiasts,

As you may know, a formalization of IEEE-754 floating-point arithmetic
in Isabelle/HOL is readily available from the AFP [1].

My question then is: what to do with the current type of floating-point
values? Should it be retained, or replaced with the new type?

Best,
Tjark

[1] https://www.isa-afp.org/entries/IEEE_Floating_Point.html
[2] https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

Email Gateway (Jun 07 2022 at 23:18):

From: Gerwin Klein <kleing@unsw.edu.au>
Hi Tjark,

I would have thought that it's the only useful representation for implementation verification, because that is what implementations have to use. E.g. a C or assembly program operates on bit vector representations and will have to deal with the fact that multiple of these map to the abstract value NaN.

If you remove that, what semantics do you give to a program that manipulates bit vector representations of floating point values?

Cheers,
Gerwin

Email Gateway (Jun 07 2022 at 23:19):

From: Gerwin Klein <kleing@unsw.edu.au>
That sounds like an excellent idea to me.

Cheers,
Gerwin

Email Gateway (Jun 08 2022 at 06:13):

From: Tobias Nipkow <nipkow@in.tum.de>
If IEEE has two treatments of NaN, we should not trash the one we have but
derive the other one as well, as the Coq library seems to (thanks, Lennart).

Tjark: I would encourage you to extend the AFP entry accordingly (in
consultation with one of the authors or contributors, if they still reply...)

Tobias
smime.p7s

Email Gateway (Jun 08 2022 at 08:09):

From: Peter Lammich <lammich@in.tum.de>
Note that the NaN is slightly over specified in the current entry. They use
some_nan as the only value for NaN produced by operations, which allows you to
prove that all NaN results from operations are equal.

Peter

Email Gateway (Jun 08 2022 at 10:17):

From: Tjark Weber <tjark.weber@it.uu.se>
Gerwin,

I would think that the abstract ("level 2") semantics is sufficient to
verify most code that uses floating points. Code that cares about the
specific bit-vector representation of floating-point values should be
relatively rare in comparison, but I acknowledge that it exists (for
instance, you might want to verify an implementation of IEEE-754).

Best,
Tjark

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

Email Gateway (Jun 08 2022 at 12:51):

From: Tjark Weber <tjark.weber@it.uu.se>
Dear all,

Thank you for your input! I will try to summarize what I think are some
key points from this discussion:

Both the abstract ("level 2") specification of floating-point data
and the bit-vector representation are potentially useful.
Flocq defines two kinds of (binary) floating-point types: one with a
single NaN value, and one with multiple NaN values. The latter is based
on the former.
The AFP entry currently only defines a floating-point type with
multiple NaN values.
However, only one of these NaN values ("some_nan") is returned as
the result of floating-point operations.¹ Flocq is more flexible in
this regard: its floating-point operations are parameterized on
functions that return a NaN result for NaN arguments.

Perhaps the best way forward then is to add a new floating-point type
with a single NaN value to the AFP entry, to define the floating-point
operations (also) on this type, and to redefine the floating-point
operations on the existing floating-point type in terms of the new type
(much like in Flocq).

I hope to be able to make some progress in this direction in the near
future. If anyone wants to contribute or has further input (especially
authors/maintainers of the current AFP entry), please get in touch!

Best,
Tjark

¹ This is arguably not conforming to the IEEE standard, which specifies
that the result should be one of the input NaNs.

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

Email Gateway (Jun 08 2022 at 13:06):

From: Peter Lammich <lammich@in.tum.de>

I hope to be able to make some progress in this direction in the near
future. If anyone wants to contribute or has further input (especially
authors/maintainers of the current AFP entry), please get in touch!

I have written an automated test suite, that tests the current floating
point semantics against pre-defined operation+result vectors, currently
drawn from IBM's FPGen testsuite (the publically available 32bit test
vectors). Its core is an executable result checker, that currently works
for +,-,*,div, fmadd, and sqrt.

While this is not very polished yet, it already can discover the bug in
the formalization of fmadd (fixed in afp-devel).

I'm not sure how to best integrate this development though, as the AFP
does not support the scripts + C programs etc that I used for the test runs.

Email Gateway (Jun 08 2022 at 23:14):

From: Gerwin Klein <kleing@unsw.edu.au>
Hi Tjark,

I strongly disagree with the "rare" point, not because it is wrong, but because it is not an argument.

This is a common fallacy in program verification: if the semantics of a language allows specific (unwanted) behaviours, you cannot verify the program in a semantics that assumes these behaviours do not exist, no matter if used rarely or even never. Instead, you must use a semantics that has those behaviours (or at least can detect them) and prove their absence. So if you assume a unique representation of NaN in your formalisation, the formalisation is already disqualified for safety proofs in programs in languages that have direct access to the bit vector representation, because you cannot observe those failures.

There are multiple ways to deal with this of course -- instead of modelling all representations, you could have a semantics that explicitly fails as soon as there is an unwanted representation, but this would mean something like an option type into whatever is used for float. I doubt that this is what one would want (esp since this is what NaN neatly expresses anyway). You could also try to prove a language invariant that the representation is always valid, but this excludes languages like C and assembly. You could try to have that invariant as a program invariant, but then you still need to be able to distinguish valid from non-valid representations and you'll have a problem that is isomorphic to projecting to an option type (maybe nicer to deal with on the technical level).

I have not looked closely at the Flocq formalisation, but it sounds to me like the level 2 semantics is basically a quotient on the bitvector representation. It should be possible to transport most properties both ways across that quotient, so that you can have a level 1 semantics for the program, and use the level 2 semantics for verifying properties about it together with suitable transport theorems. The difficulties one encounters transporting properties across are exactly the parts where the level 2 semantics fails to observe failure in real implementations. It would be very nice to crystallise that out in an abstract way that is independent of specific programming languages.

This has similarities to using integers for program verification vs machine words (much smaller scope here, but still there): there are many properties that are perfectly preserved and useful if you verify a program with integer semantics, but if you only use integers you won't know. What the machine word type does is force you to acknowledge the limitations of the real program and deal with them. You can either reason about the more complex machine word type or you can reason about the integer type and suitably generate side conditions about overflow (assuming you manage to catch all cases). Both are fine. What is not fine is only using integers and saying that the property still holds because overflow is rare.

Cheers,
Gerwin

Email Gateway (Jun 09 2022 at 00:03):

From: Matthew Fernandez <matthew.fernandez@gmail.com>
I read Tjark’s comments to mean code that needs to distinguish differing NaN representations or to recover from a NaN result is rare. If so, I would say this is accurate, and using a single NaN representation seems sufficient. There’s a lot of floating point code that treats any NaN result as “give up.” In contrast, there’s only a much smaller amount of code that tries to distinguish different NaNs or cast back and forth between integer and floating point representations.

For the former code, a proof would simply give you nothing in the face of NaNs. I.e. you’d have to prove a NaN value never arose or add the absence of intermediate NaNs to your assumptions. Maybe I misunderstand you though, Gerwin.

Email Gateway (Jun 09 2022 at 00:38):

From: Tjark Weber <tjark.weber@it.uu.se>
Gerwin,

On Wed, 2022-06-08 at 23:13 +0000, Gerwin Klein wrote:

On 8 Jun 2022, at 20:16, Tjark Weber <tjark.weber@it.uu.se> wrote:
I would think that the abstract ("level 2") semantics is sufficient
to verify most code that uses floating points. Code that cares
about the specific bit-vector representation of floating-point
values should be relatively rare in comparison, but I acknowledge
that it exists (for instance, you might want to verify an
implementation of IEEE-754).

I strongly disagree with the "rare" point, not because it is wrong,
but because it is not an argument.

This is a common fallacy in program verification: if the semantics of
a language allows specific (unwanted) behaviours, you cannot verify
the program in a semantics that assumes these behaviours do not
exist, no matter if used rarely or even never. Instead, you must use
a semantics that has those behaviours (or at least can detect them)
and prove their absence. So if you assume a unique representation of
NaN in your formalisation, the formalisation is already disqualified
for safety proofs in programs in languages that have direct access to
the bit vector representation, because you cannot observe those
failures.

I agree, but for programs that (are written in language fragments that)
do not directly access the bit-vector representation of floating-point
data, verification against the abstract ("level 2") semantics is sound.

Of course, one should not use that semantics to verify arbitrary C
programs without further checks. In fact, one couldn't: level 2 does
not specify the bit encoding of floating-point data. If we need to
reason about the bit encoding, it would clearly be unsound to assume
that NaN has only one encoding.

This has similarities to using integers for program verification vs
machine words (much smaller scope here, but still there): there are
many properties that are perfectly preserved and useful if you verify
a program with integer semantics, but if you only use integers you
won't know. What the machine word type does is force you to
acknowledge the limitations of the real program and deal with them.
You can either reason about the more complex machine word type or you
can reason about the integer type and suitably generate side
conditions about overflow (assuming you manage to catch all cases).
Both are fine. What is not fine is only using integers and saying
that the property still holds because overflow is rare.

I think a more apt comparison would be between bounded integers (that
correctly model C arithmetic including overflow) and machine words.
Machine-word semantics is needed for programs that apply bit operations
to integer data; but bounded-integer semantics suffices to verify
programs that only use arithmetic operations on integers. Neither
semantics will ignore overflows.

Best,
Tjark

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

Email Gateway (Jun 09 2022 at 09:29):

From: Gerwin Klein <kleing@unsw.edu.au>
Hi Tjark,

On 9 Jun 2022, at 10:37, Tjark Weber <tjark.weber@it.uu.se> wrote:

On Wed, 2022-06-08 at 23:13 +0000, Gerwin Klein wrote:

On 8 Jun 2022, at 20:16, Tjark Weber <tjark.weber@it.uu.se> wrote:

I would think that the abstract ("level 2") semantics is sufficient
to verify most code that uses floating points. Code that cares
about the specific bit-vector representation of floating-point
values should be relatively rare in comparison, but I acknowledge
that it exists (for instance, you might want to verify an
implementation of IEEE-754).

I strongly disagree with the "rare" point, not because it is wrong,
but because it is not an argument.

This is a common fallacy in program verification: if the semantics of
a language allows specific (unwanted) behaviours, you cannot verify
the program in a semantics that assumes these behaviours do not
exist, no matter if used rarely or even never. Instead, you must use
a semantics that has those behaviours (or at least can detect them)
and prove their absence. So if you assume a unique representation of
NaN in your formalisation, the formalisation is already disqualified
for safety proofs in programs in languages that have direct access to
the bit vector representation, because you cannot observe those
failures.

I agree, but for programs that (are written in language fragments that)
do not directly access the bit-vector representation of floating-point
data, verification against the abstract ("level 2") semantics is sound.

Of course, one should not use that semantics to verify arbitrary C
programs without further checks. In fact, one couldn't: level 2 does
not specify the bit encoding of floating-point data. If we need to
reason about the bit encoding, it would clearly be unsound to assume
that NaN has only one encoding.

Cool, I think we are in agreement then. My point was that if I'm verifying arbitrary C programs with type unsoundness etc (which I do regularly) I don't know if I'm in a fragment for which level 2 is sound or not until I've done the verification. For that, level 1 is useful. Having both levels available would be even more useful, so I'm all for adding level 2, but I'm against removing level 1.

This has similarities to using integers for program verification vs
machine words (much smaller scope here, but still there): there are
many properties that are perfectly preserved and useful if you verify
a program with integer semantics, but if you only use integers you
won't know. What the machine word type does is force you to
acknowledge the limitations of the real program and deal with them.
You can either reason about the more complex machine word type or you
can reason about the integer type and suitably generate side
conditions about overflow (assuming you manage to catch all cases).
Both are fine. What is not fine is only using integers and saying
that the property still holds because overflow is rare.

I think a more apt comparison would be between bounded integers (that
correctly model C arithmetic including overflow) and machine words.
Machine-word semantics is needed for programs that apply bit operations
to integer data; but bounded-integer semantics suffices to verify
programs that only use arithmetic operations on integers. Neither
semantics will ignore overflows.

I shouldn't have started that rabbit hole, but now that we're here I need to point out that bounded integers are exactly equivalent to machine words (in fact that is what the machine word representation can be derived from), so bounded integers don't work as analogy for the float problem. But I think we agree sufficiently that we don't need to search for a better analogy :-)

Cheers,
Gerwin

Email Gateway (Jun 09 2022 at 10:05):

From: Gerwin Klein <kleing@unsw.edu.au>

On 9 Jun 2022, at 10:02, Matthew Fernandez <matthew.fernandez@gmail.com> wrote:

I read Tjark’s comments to mean code that needs to distinguish differing NaN representations or to recover from a NaN result is rare.

Agreed so far.

If so, I would say this is accurate, and using a single NaN representation seems sufficient.

I don't agree with the second part as stated (but possibly with what you meant). It'd certainly be possible to write a semantics that only has a single NaN value, but you'd basically be reconstructing the cases the level 1 semantics deals with when you are either projecting multiple representations into one abstract NaN or trying to exclude those representations before they are abstracted. Either way you have to be able to say that they either don't occur or if you allow them to occur, how they behave. The level 1 semantics makes that straightforward. The level 2 semantics doesn't (it basically assumes this has already happened, e.g. as a language invariant).

It's not like C programs don't screw with representations all the time. They will absolutely rely on things like zeroing a memory region being equivalent to the value 0 in float etc. If you want to be able to deal with that, you need to be able to deal with representations. You can forbid some etc, but you can't start the semantics with just abstract values.

There’s a lot of floating point code that treats any NaN result as “give up.” In contrast, there’s only a much smaller amount of code that tries to distinguish different NaNs or cast back and forth between integer and floating point representations.

Yes, I do agree that actually using them for computation is rare and I likely wouldn't be interested in verifying such programs. I could maybe see a NaN in/NaN out situation, but I'd mostly be interested in showing that a particular program doesn't produce NaN. I claim that for that purpose, you can't start with the level 2 semantics if the programming language doesn't implement it. You can end up there, but your basic program semantics has to do more and what it has to do is modelled nicely by level 1.

There is a lot of design space on how you could model all this, and I think I understand your point about proving that no NaN ever happens. I'd still say that a level 1 float representation fits extremely well for that. It can deal with NaN in expressions (so you don't have to generate side conditions for every sub-expression), it can deal with multiple representations of NaN for code that screws up representations in stupid ways, and I can easily state that I want none of these NaN representations to occur, because they are just values in the float type, not something extra.

(As added bonus, if you have multiple NaN, you don't have to work hard to make sure Isabelle doesn't produce reflexivity for NaN)

For the former code, a proof would simply give you nothing in the face of NaNs. I.e. you’d have to prove a NaN value never arose or add the absence of intermediate NaNs to your assumptions.

Demanding absence of NaN for every intermediate sub-expression is a lot of side conditions that you have to solve before you get to reason about what the program actually does. It'd be possible, but I don't think it'd be nice.

Maybe I misunderstand you though, Gerwin.

I think we're converging.

Cheers,
Gerwin

Email Gateway (Jun 09 2022 at 11:18):

From: Tjark Weber <tjark.weber@it.uu.se>
Gerwin,

This is justified by the fact that the floating-point operations in
IEEE-754 treat (different representations of) NaN uniformly. Therefore,
the level 2 semantics is simply a quotient of the more detailed bit-
vector semantics.

Anyway, I think we are mostly in agreement (at least, I have no plans
to remove the bit-vector semantics from the AFP entry). Just for the
record (and to avoid potential confusion), I'd like to mention that
what you are calling "level 1" semantics in this thread (i.e., the bit
representation of floating-point data) is actually specification level
4 in IEEE-754.

Best,
Tjark

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

Email Gateway (Jun 09 2022 at 23:39):

From: Gerwin Klein <kleing@unsw.edu.au>

On 9 Jun 2022, at 21:18, Tjark Weber <tjark.weber@it.uu.se> wrote:

Gerwin,

On Thu, 2022-06-09 at 10:04 +0000, Gerwin Klein wrote:

If so, I would say this is accurate, and using a single NaN
representation seems sufficient.

I don't agree with the second part as stated (but possibly with what
you meant). It'd certainly be possible to write a semantics that only
has a single NaN value, but you'd basically be reconstructing the
cases the level 1 semantics deals with when you are either projecting
multiple representations into one abstract NaN or trying to exclude
those representations before they are abstracted. Either way you have
to be able to say that they either don't occur or if you allow them
to occur, how they behave. The level 1 semantics makes that
straightforward. The level 2 semantics doesn't (it basically assumes
this has already happened, e.g. as a language invariant).

This is justified by the fact that the floating-point operations in
IEEE-754 treat (different representations of) NaN uniformly. Therefore,
the level 2 semantics is simply a quotient of the more detailed bit-
vector semantics.

Yup, exactly.

Anyway, I think we are mostly in agreement (at least, I have no plans
to remove the bit-vector semantics from the AFP entry). Just for the
record (and to avoid potential confusion), I'd like to mention that
what you are calling "level 1" semantics in this thread (i.e., the bit
representation of floating-point data) is actually specification level
4 in IEEE-754.

Thanks, yes, good point. I didn't actually look that up and just used 1 as the counter point.

Cheers,
Gerwin

Last updated: Apr 23 2024 at 08:19 UTC