Xavier Denis

In large part, but actually many functions are implicitly using this especially in top level contracts.

It's not hard to special case these, in fact they already are.

That's already the case: we check that all functions called in logical programs are pure (or are one of a small list of traits we 'overload'). We just need to...

The current behavior was a rapid addition which mimics how Prusti disables bounds checks by changing the type that integers are translated to. I'd like to remove it entirely and...

Perhaps this could just be done by providing an alternate prelude in which we use a version of the machine integer types & functions with no preconditions?

We can't since attribute macros need to be attached to valid rust syntax, so there's no way for us to handle `^`, `forall`, `exists` or other logical operators.

> When the body of a logic function uses private symbols, what should we do? We should either emit an error or make the function opaque automatically. I guess the...

An initial design that @jhjourdan and I seem to have settled on is the following: - `#[predicate]` and `#[logic]` functions are _transparent_ wherever they are _visible_ by default. - If...

Good point, we need to do a check similar to with `pub` for this to be actually useful. I propose that we only allow it to be visible in child...

By body do you mean the recursive expansion of every referenced function? If not how is this different than just tagging each function with an 'opaque' attribute?