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.

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

Already on GitHub? Sign in to your account

derive kani::Arbitrary on f16 and bf16 #80

Merged
merged 1 commit into from
Mar 28, 2023

Conversation

cameron1024
Copy link
Contributor

Hi, thanks for the great library 馃榿

I've been using kani to introduce some lightweight formal methods for a CBOR implementation I'm working on.

Kani has a trait Arbitrary which is used to generate symbolic values in the model checker (conceptually, a value that represents "for all Ts").

The rough motivation for this PR is an enum that looks like:

#[cfg_attr(kani, derive(kani::Arbitrary))]
enum Float {
  Half(half::f16),
  Single(f32),
  Double(f64),
}

This currently fails, since half::f16 doesn't implement kani::Arbitrary. This PR adds the derive macros, gated behind the kani compiler option being set. This doesn't add a cargo feature flag or optional dependency, since kani doesn't require this (when you verify a program, it compiles it with its own standard library, which injects the kani dependency).

I appreciate you may not want this sort of tool in the codebase, since it's fairly non-standard Rust, and could be unexpected/confusing for contributors, but FWIW, I've had very positive experiences with it. Happy to be given pushback on this though 馃槄 .

Usually I'd open an issue for this sort of thing first, but since the PR is so trivial, I thought it might just be easier this way.

Thanks 馃榿

@starkat99 starkat99 merged commit 846d0fa into starkat99:main Mar 28, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants