Open franck44 opened 8 months ago
Lots of predicates are verification-only and don't need to be compiled. IsValid is an example of such a predicate.
IsValid
At the moment they are declared as predicate and must be compilable which is not necessary.
predicate
make the IsValid predicates ghost predicates.
ghost
Lots of predicates are verification-only and don't need to be compiled.
IsValid
is an example of such a predicate.At the moment they are declared as
predicate
and must be compilable which is not necessary.To do
make the
IsValid
predicatesghost
predicates.