Running MIRAI in cargo test

[nud3l]

Running MIRAI in cargo test

[hermanventer]

The way this is supposed to work is to run "cargo mirai --tests". It is not being tested in CI and seems to have been broken by a rust compiler change. Oops.

When it gets fixed, your example above is almost right. The problem is just that since expected_result is abstract, nothing is known about it and hence the verify check will fail. (If you removed the abstract_value! calls, the code becomes verifiable because constant folding will handle it, but you are doing no better than just running cargo test.)

If you could write an assertion that only depends on the fact that some unknown number has been added to some other unknown number, that would be statically verifiable, but coming up with such an assertion would be a bit of a challenge, unless you further constrain the input values, for example if you add assume!(a < 10) and assume!(b < 20) then you can verify that result is less than 30.