Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Float types are not testable with :exhaust #1051

Closed
brianhuffman opened this issue Jan 27, 2021 · 0 comments
Closed

Float types are not testable with :exhaust #1051

brianhuffman opened this issue Jan 27, 2021 · 0 comments
Labels
cryptol-quickcheck Related to REPL :check command

Comments

@brianhuffman
Copy link
Contributor

While attempting to run some tests related to #1049, I discovered that the floating point types don't work with :exhaust. (Apparently they do work with :check, though.)

Cryptol> :m Float
Loading module Cryptol
Loading module Float
Float> :check \x -> fpFromBits (fpToBits`{6,10} x) == x
Using random testing.
Passed 100 tests.
Float> :exhaust \x -> fpFromBits (fpToBits`{6,10} x) == x

The expression is not of a testable type.
Type: Float 6 10 -> Bit
@brianhuffman brianhuffman mentioned this issue Jan 27, 2021
Closed
@robdockins robdockins added the cryptol-quickcheck Related to REPL :check command label Feb 9, 2021
robdockins added a commit that referenced this issue Feb 9, 2021
@robdockins
Allow :exhaust to work directly on floating-point values
b413294 
by enumerating all bitpatterns.

Note, this overcounts somewhat the number of distinct floating point
values there are, since all NaNs are considered identical
as `Float` values.  We could be more careful here to avoid
generating more NaN values than required, but I'm not sure it's worth
the effort.

Fixes #1051
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
cryptol-quickcheck Related to REPL :check command
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@brianhuffman @robdockins