search

kenmcmil / ivy

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

Ivy doesn't expand a nested macro #41

Open hidenori-shinohara opened 2 years ago

hidenori-shinohara commented 2 years ago 
#lang ivy1.7

type mytype

relation always_true(MYTYPE:mytype)
definition always_true(MYTYPE) = true

relation always_true_macro(MYTYPE:mytype)
definition always_true_macro(mytype_:mytype) = true

relation nested_always_true(MYTYPE:mytype)
definition nested_always_true(mytype_:mytype) = always_true(mytype_)

relation nested_always_true_macro(MYTYPE:mytype)
definition nested_always_true_macro(mytype_:mytype) = always_true_macro(mytype_)

invariant forall X. always_true(X) # Pass
invariant forall X. always_true_macro(X) # Pass
invariant forall X. nested_always_true(X) # Pass
invariant forall X. nested_always_true_macro(X) # Fail

Ivy seems to fail to expand always_true_macro inside nested_always_true_macro and shows the following CTI:

searching for a small model... done
[
    @X = 0
    always_true(0) = true
    always_true_macro(0) = false
    nested_always_true_macro(0) = false
]