`Need` second argument can rely on first being false

[seebees]

Consider the following

function Work() : Result<int, string> {
  var something := Magic();
  :- Need(|something| == 0, "Woops => " + Join(something, ","));
}

function Join(ss: seq<string>) : string
  requires 0 < |ss|

This will fail to verify. Because Join requires 0 < |something|. But we know (because this is how Need works, that this condition is only important if |something| != 0.

It would be great to both rely on this. But also to automatically thunk the second argument. This way Dafny users can write nice clear code, and get all the efficiency benefits in the compiler :)

[robin-aws]

You can do this reasonably well in Dafny as is:

include "Wrappers.dfy"

module MoreWrappers {

  import opened Wrappers

  function method LazyNeed<E>(condition: bool, errorThunk: () --> E): (result: Outcome<E>)
    requires !condition ==> errorThunk.requires()
  {
    if condition then Pass else Fail(errorThunk())
  }

  function Work() : Result<int, string> {
    var something := Magic();
    :- LazyNeed(|something| == 0, () requires |something| > 0 => "Woops => " + Join(something, ","));
    Success(42)
  }

  function Magic(): seq<string>

  function Join(ss: seq<string>, sep: string) : string
    requires 0 < |ss|
}

The explicit lambda expression, especially with the explicit requires, is certainly a little unfortunate.