search

microsoft / 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
223 stars 80 forks source link

l2s: proving invariant with theorem fails with syntax error #69

Open nano-o opened 4 years ago

nano-o commented 4 years ago

The following fails with error: token 'proof': syntax error. 

#lang ivy1.7

type t
relation r(X:t)

export action my_action = { r(X) := true }

axiom [test] {
    property true
}

temporal property forall X . eventually r(X)
proof {
    tactic l2s with
        invariant true
        proof {
            assume test
        }
}
kenmcmil commented 4 years ago

The proof at line 16 is not supported. I might consider that as a feature request. Do you have a use case for it?

nano-o commented 4 years ago

I do, but I might be able to get around it by using the theorem to prove a helper invariant outside the l2s tactic.