Potential Z# footgun

[cmlsharp]

I have been writing up an internal reference document for Z# and it has occurred to me that a combination of features in Z# as it currently exists lend themselves to writing circuits that non-obviously leak information.

Imagine Bob writes a function verify_foo(Foo foo). Perhaps for efficiency reasons, perhaps because verify_foo contains table lookups, verify_foo imposes constraints strictly via assertion. Morally then, verify_foo(foo) is a statement, but Z# requires that all functions have return types, and disallows naked expressions in function bodies. So Bob reluctantly makes verify_foo return a bool which is unconditionally true, with the idea that callers can simply use assert(verify_foo(foo)) to call it. This exact idiom is not hypothetical and is used by necessity in our code all the time.

Later Alice comes along and wants to use Bob's code. She writes the quite sensible looking function below:

from "./bobs_lib" import Foo, verify_foo
struct Bar {
    // ...
}

// a truly "pure" function that doesn't assert and returns false sometimes
def verify_bar(Bar bar) -> bool:
    // ...

def main(private Foo foo, private Bar bar) -> bool:
    return verify_foo(foo) && verify_bar(bar)

To someone who didn't look too closely at Bob's code, the above looks sensible. It looks like the only information the verifier should get is whether or not both verify_foo(foo) and verify_bar(bar) succeed. But that's not what happens! If verify_foo succeeds, but verify_bar doesn't a .vin file with (return false) will successfully verify.

Proposed fixes by level of invasiveness:

• Don't require functions to have a return type (internally you could give them an unnameable type called e.g. void) and allow arbitrary expressions to be statements. This would have prevented Bob from having to write the misleading API in the first place. This would be a totally backwards compatible change. This would also fix the issue where you get weird compiler errors if you do anything but assert the output of value_in_array. You could instead make value_in_array be a void function and call it assert_in_array or something.
• Consider also requiring that main, when it is the entry point for a circuit, has no return type. This would not be backwards compatible, but I think this example shows that implicitly introducing a statement variable can be dangerous, especially in the presence of assertions. It's also just kind of hard to explain to new people. Someone can always opt in by explicitly adding an extra input parameter manually if they want. I'd view this restriction as being pretty analogous to the "main can't be generic rule"
• I wonder if "contains assertions" should color the function somehow (perhaps along the lines of how Roc handles effectful functions?). This way it is visually obvious when calling a function that it contains assertions. (Though this is so common that you probably just end up with ~every function being "assertion colored" which doesn't help much).