Witnesses can be a performance issue in Go

[tchajed]

If you provide a witness for a type, every method returning it initializes the return variable to the witness. If the witness is expensive to compute, this can be a big performance penalty (particularly when the output is never used, or assigned to an existing value of that type).

Here's an example that will actually be slow:

function method repeat<T>(x: T, n: nat): seq<T>
{
  seq(n, _ => x)
}

type Block = x:seq<int> | |x| == 4096 witness repeat(0, 4096)

method MkBlock() returns (b:Block)
{
  b := repeat(1, 4096);
}

The generated Go looks like this:

func (_static *CompanionStruct_Default___) MkBlock() _dafny.Seq {
  var b _dafny.Seq = Companion_Block_.Witness()
  _ = b
  b = Companion_Default___.Repeat(_dafny.One, _dafny.IntOfInt64(4096))
  return b
}

I looked at the generated C# and it looks fine, because the witness is a readonly field of the class. In Go there's no way to make this witness read-only, so maybe there's no good compiler fix; in that case it would be nice to document this somewhere on how to get good performance out of the Go backend. I've started using only ghost witness for this reason.

Amusingly this was the very first performance issue I fixed when profiling generated Dafny code (see mit-pdos/dafny-jrnl@2bf4aa9498) and it improved performance by 50%.

[RustanLeino]

If the type (here, Block) has no type parameters (indeed, Block has no type parameters), then the witness could be cached. Then, it would need to be computed at most once.

The target code could also be improved if Dafny did a def-use analysis, which would determine if the value assigned to b in its target-code definition could be a placebo value rather than the witness. A placebo is just a rubble of bits that pleases the target language's definite-assignment rules, if any. For Go, "assigning a placebo" can be a no-op.