IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77
stars
24
forks
source link
Unexpected behavior with a macro inside an if statement #42
The following code throws a CTI with my_obj.always_false_macro(0) = true in the pre-state, which doesn't make much sense.
#lang ivy1.7
type my_type
object my_obj = {
relation relation_that_we_never_update(SOMETHING:my_type)
after init {
relation_that_we_never_update(X) := true;
}
relation always_false_macro(SOMETHING:my_type)
definition always_false_macro(something:my_type) = false
action my_action_macro(something:my_type) = {
if (always_false_macro(something)) {
# We should never get here because `always_false_macro` is always false.
# But Ivy seems to get confused and think that this is reachable.
relation_that_we_never_update(something) := false;
}
}
}
# This should always be true since
# (1) We set relation_that_we_never_update to be `true` in the initialization.
# (2) We never update this relation.
invariant forall X. my_obj.relation_that_we_never_update(X)
export my_obj.my_action_macro
The following code throws a CTI with
my_obj.always_false_macro(0) = true
in the pre-state, which doesn't make much sense.