Assert for the elephant let-or-fail operator in expressions

[MikaelMayer]

It's possible to write the following:

function SubTest(a: int): (r: Result<string, int>)

function Test(): (r: Result<string, int>) {
    var s :- SubTest(3);
    Success(s)
}

but let's say I would like to assert that SubTest won't fail (because of some conditions in the inputs of SubTest).
In methods, it's possible to prefix the call to SubTest with assert, and it will emit the assertion. However, it's not possible for functions yet.

It would be however obvious that

function SubTest(a: int): (r: Result<string, int>)

function Test(): (r: Result<string, int>) {
    var s :- assert SubTest(3);
    Success(s)
}

should be rewritten to:

function SubTest(a: int): (r: Result<bool, int>)

function Test(): (r: Result<string, int>) {
    var tmp := SubTest(3);
    assert !tmp.IsFailure();
    var s := tmp.Extract();
    Success(s);
}

The same goes for the assume and expect keywords, since many users use function methods, might use them for testing, and also to assume something before coming back to it and revisiting the keyword later.

[cpitclaudel]

This makes sense for expect, but for assert, why not just write var s := SubTest(3).value;?

[MikaelMayer]

I get your point in this particular case; however, there is no guarantee in the general case that .Extract() is equivalent to .value. The precondition of .Extract() is that the object is not .IsFailure(), which might be stronger than just being of the success sub-constructor.

[cpitclaudel]

Then why not just call Extract?

[MikaelMayer]

Good point. But then, why support the keyword :- assert even for statements?
I think it has to do with the fact that it's easier to deal with the "assume" / "assert" / "expect" keywords easily, rather than remembering the precise method "Extract".

[cpitclaudel]

I was not aware of that syntax, and it's mightily confusing!

function method SubTest(a: int): (r: Result<string, int>)

method Test() returns (r: Result<string, int>) {
    var s :- assert X; Success("A");
    return Success(s);
}

does not mean the same as

function method SubTest(a: int): (r: Result<string, int>)

method Test() returns (r: Result<string, int>) {
    var s :- (assert X; Success("A"));
    return Success(s);
}

Normally assert … is unambiguous in expression context despite using ; like var does because assert … must be followed by a ; and another expression… except in expressions passed to the elephant operator?!

[MikaelMayer]

This ambiguity is actually documented in the Dafny reference already.
https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-failure-return-keyword

I don't think it's a problem, you can disambiguate with parentheses, and the first syntax gives a handy way to assert that something should return a success and return its value at the same time.
Plus, one would never use the second syntax to assert X inside the expression, they'd put it in a previous statement anyway, so it's unlikely anyone is going to run into "oh no, my assert is not valid... oh I just discovered the elephant assert syntax".

[davidcok]

cf. #1434