Large Performance Regressions with Dafny 4.4.0?

[DavePearce]

Dafny version

4.4.0

Code to produce this issue

newtype u8 = a:int | 0 <= a < 256
  
function ToBytes(v:nat) : (r:seq<u8>)
  ensures |r| > 0 {
    // Extract the byte
    var byte : u8 := (v % 256) as u8;
    // Determine what's left
    var w : nat := v/256;
    if w == 0 then [byte]
    else
      ToBytes(w) + [byte]
}

function FromBytes(bytes:seq<u8>) : (r:nat) {
  if |bytes| == 0 then 0
  else
    var last := |bytes| - 1;
    var byte := bytes[last] as nat;
    var msw := FromBytes(bytes[..last]);
    (msw * 256) + byte
}

lemma LemmaToFromBytes(bytes:seq<u8>)
  requires |bytes| > 0 && (|bytes| == 1 || bytes[0] != 0)
  ensures ToBytes(FromBytes(bytes)) == bytes {
    var n := |bytes| - 1;
    if |bytes| > 1 {
      LemmaToFromBytes(bytes[..n]);
    }
}

Command to run and resulting output

%> time ~/pkg/dafny-4.2.0/dafny verify --solver-path=$HOME/pkg/dafny-4.4.0/z3/bin/z3-4.8.5 problems.dfy

Dafny program verifier finished with 5 verified, 0 errors

real    0m1.807s
user    0m1.952s
sys     0m0.257s


%> time ~/pkg/dafny-4.3.0/dafny verify --solver-path=$HOME/pkg/dafny-4.4.0/z3/bin/z3-4.8.5 problems.dfy

Dafny program verifier finished with 5 verified, 0 errors

real    0m1.851s
user    0m2.042s
sys     0m0.196s


%> time ~/pkg/dafny-4.4.0/dafny verify --solver-path=$HOME/pkg/dafny-4.4.0/z3/bin/z3-4.8.5 problems.dfy

Dafny program verifier finished with 5 verified, 0 errors

real    0m10.500s
user    0m1.824s
sys     0m0.194s

What happened?

Basically, we're seeing a roughly 10x slowdown on this short example. Note that Z3 version 4.8.5 is needed to verify this example in reasonable time.

What type of operating system are you experiencing the problem on?

Linux

[DavePearce]

An update here. The default combination of Dafny 4.4.0 and Z3 4.12.1 perhaps performs better than Dafny 4.4.0 and Z3 4.8.5. However, its performance is wildly unpredictable.

[atomb]

This seems to have been caused by #4428.

[DavePearce]

Curious, as that looks like it should improve performance !?

[atomb]

Yeah, it does seem like it should! It could, however, lead to omission of an axiom that was previously being used. I'm thinking of reverting it for now, though.

[DavePearce]

Maybe if its mistakenly removing an axiom then? Or, what about moving something out of the uses clause ... Could that have some unexpected effect?

And, are you experiencing this elsewhere?

[atomb]

Maybe if its mistakenly removing an axiom then? Or, what about moving something out of the uses clause ... Could that have some unexpected effect?

Yeah, I expect it's something like that.

And, are you experiencing this elsewhere?

Not notably, but I think it's worth some deeper experimentation.