Document the contract of Boogie's float type - #1154
Open
fabiomadge wants to merge 4 commits into
Open
fabiomadge wants to merge 4 commits into
fabiomadge wants to merge 4 commits into
Conversation
This was referenced Aug 31, 2026
fabiomadge
force-pushed
the
fix/document-float-semantics
branch
from
September 20, 2026 15:50
d201436 to
257d372
Compare
shazqadeer
previously approved these changes
Sep 20, 2026
Contributor
Author
|
Thanks for the review, but feel free to wait with the others until I can have a proper look myself and undraft them. |
fabiomadge
marked this pull request as ready for review
September 21, 2026 16:04
Nothing recorded the contract, and the code shows it: `Expr.Not` has reversed a
negated order relation since 2010, correctly for every type the language had
then; the interval domain has described a variable by a pair of integer bounds
since 2011; and floats arrived in 2015 with the commit message "adding references
to the floating point type wherever references to the real type exist. This
remains a work in progress." Each defect since has been a transformation
inheriting an assumption that a float breaks.
So this states it on the type, where someone asking what `==` means on a float
will look:
* `==` and `!=` are SMT `=`, i.e. bit identity -- total, reflexive even at NaN
since the sort has one NaN, and they keep `-0.0` and `+0.0` apart.
* `<`, `<=`, `>` and `>=` are the IEEE predicates -- partial, false whenever an
operand is NaN, and they tie the two zeros. So `x <= x` is not a tautology:
it holds exactly when `x` is not NaN, which is how the core language says
that.
* The two do not agree and neither implies the other. Trichotomy does not hold
and nothing may assume it -- in particular a negated order relation is not
the reverse relation, and a pair of numeric bounds does not describe a float.
* Arithmetic rounds, overflows to an infinity, and produces NaN from `0/0`.
* The IEEE predicates with no surface syntax, and `fp.eq`, are reachable only
through a `{:builtin}` function.
No code changes.
The type is the SMT-LIB FloatingPoint sort, and every surprise in the comment comes from where that sort departs from IEEE 754: it has exactly one NaN, no signalling NaNs, no exception flags, and no bit-level access, so a payload cannot be observed. Opening with "IEEE 754" invites the reader to expect "x == x" to be false at a NaN, which is the opposite of what Boogie does. For the same reason "==" is not bit identity but identity on the sort: there is one NaN to be identical to. The test now pins the two equalities disagreeing on the same NaN, which is the whole reason fp.eq exists.
The guard used "!(x == 0NaN24e8)", which reads as a comparison against a particular NaN but works only because the sort has one -- true, and pinned directly by SmtAndIeeeEqualityDisagree, so there is no reason for this procedure to depend on it too. The point it makes about the core language, that "x <= x" is how to say "not a NaN" without a builtin, is now in the comment rather than smuggled into the guard.
fabiomadge
force-pushed
the
fix/document-float-semantics
branch
from
September 21, 2026 16:04
c8bb830 to
0e57ae3
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Boogie has no language reference, so what its float operators mean is recoverable only by reading the
SMT-LIB translator. This states it on
FloatType, and pins the parts no test covered.The type is the SMT-LIB
FloatingPointsort, which approximates IEEE 754. The approximation is wherethe surprises are, so the comment leads with it: the sort has exactly one NaN, there are no signalling
NaNs and no exception flags, and a float has no bit-level access, so a payload cannot be observed.
==and!=are SMT=— identity on the sort, not bit identity, there being one NaN to be identicalto. So they are total and reflexive even at NaN, where IEEE equality is false, and they keep
-0.0and+0.0apart.<,<=,>,>=arefp.lt,fp.leq,fp.gt,fp.geq: partial, false whenever anoperand is NaN, and tying the two zeros. Neither implies the other, so trichotomy fails — a negated order
relation is not the reverse relation, and a pair of numeric bounds does not describe a float. Arithmetic is
the
fp.*operations under round-to-nearest-even; other rounding modes, the IEEE predicates and IEEEequality (
fp.eq) are reachable only through{:builtin}.Testing.
Test/floats/FloatContract.bplpins the claimsEqual2.bplandSpecialValues.bpldo not:five procedures verify and
assert x <= xfails, which is what the doc says. One of them pins the twoequalities disagreeing on the same NaN —
x == x && !FEQ(x, x)— which is the whole reasonfp.eqexists,and the clearest statement of the gap between this sort and IEEE 754.
One of six; best read first, since #1156 and #1157 cite it.