search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.11k stars 83 forks source link

Quantifiers for function contracts #2546

Open JustusAdam opened 1 year ago

JustusAdam commented 1 year ago

A rudimentary implementation for forall and exists for kani function contracts. They are implemented as higher-order builtins, which compile to __CPROVER_forall and __CPROVER_exists respectively.

d0nutptr commented 2 months ago

Hello! I was curious if there was a sense of when this functionality might be available?

I was trying to create a function contract to express the hashing property:

kani::ensures(result != hash(kani::any_where(|x| *x != input)))

but I believe I need quantifiers for this to actually work. Thank you!