Are verify and measure-complexity different?

[hmijail]

What change in documentation do you suggest?

Is there any fundamental difference between measure-complexity and verify?

Verify doesn't allow to set a random seed, which I guess means forces seed 0. Is there a reason?

Verify also doesn't have an --iterations argument. Both options can be brought to the verify command with --boogie options. Is that equivalent to measure-complexity?

I could just use measure-complexity with 1 iteration instead of verify, but then I can't use verify's new filter-symbol argument. But why is it not there to begin with?

It would be great to understand why the separation exists, to ensure I'm not doing something silly/risky by using them interchangeably.

[hmijail]

Well, actually I see that dafny 4.6 seems to neuter the --boogie options, so using them to create my own faux-measure-complexity on top of verify as I did on 4.4 is no longer possible.

So maybe that's (part of?) the answer: until recently measure-complexity and verify were very similar but the plan is to diverge?

[stefan-aws]

@atomb

[keyboardDrummer]

There's different ways of preventing proof complexity. A simple one is to limit the maximum resources used by a proof. This option is available in dafny verify, using --resource-limit <resource-limit>.

A more complicated way of preventing proof complexity is to run multiple iterations and to compare the resources used by each iteration. I did not want to increase the scope of dafny verify by adding options related to this statistical technique, so I added a separate command, measure-complexity, for doing that. The scope of measure-complexity is not entirely clear. In the future it might even be implemented in a separate repository as a plugin for the Dafny CLI.

Also I think the default behavior of measure-complexity should be quite different from verify. For example,dafny verify returns a success exit code if everything verified in a single iteration. measure-complexity currently returns a success code if everything verified in each iteration, but I intend to change that so that it only returns a success exit code if the relative standard deviation of the resource count used is within a a certain bound.

[hmijail]

Thank you for the explanation.

I mentioned --filter-symbol being available in verify but not in measure-complexity. It would be very useful in there too, to accelerate iterating. Will it be made available there too?
(Should I open a new issue?)

[keyboardDrummer]

Thank you for the explanation.

I mentioned --filter-symbol being available in verify but not in measure-complexity. It would be very useful in there too, to accelerate iterating. Will it be made available there too? (Should I open a new issue?)

In nightly, these options are already available for measure-complexity

[hmijail]

Thank you!