Allow top-level reveal in exec mode (without a proof block)

[jaylorch]

Just as we can assert in exec mode (by implicitly switching to proof mode), it seems like we should be able to reveal in exec mode as well.

[utaal]

This is currently working as expected, but the error message we're emitting isn't helpful. You're expected to use a proof block:

#[verifier(opaque)]
spec fn is_true(a: bool) -> bool {
    a
}

exec fn foo() {
    let a = true;
    let ghost b = is_true(a);
    proof {
        reveal(is_true);
    }
    assert(b);
}

Do you consider a better error message (#520) a sufficient fix, or would you expect to use reveal directly?

[jaylorch]

I should have tagged this as a feature request, but I didn't see such a tag available. I just thought that, since it's obvious that a reveal implies it's part of a proof, there was no need to require the developer to waste the characters putting a proof block around it. We already do that for assert, so I figured it would be analogously acceptable and natural to do it for reveal.

[jaylorch]

To more directly answer your question, I appreciate the error message but I was really hoping that this could be made to be not an error.

[utaal]

Noted. I've been using discussions to track feature requests, so I moved this conversation to a discussion.

[utaal]

This is now supported.