Quantifiers for function contracts

[JustusAdam]

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]

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!