Do not warn about {:verify false} on methods when using --allow-axiom

[keyboardDrummer]

What was changed?

Do not warn about {:verify false} on methods when using --allow-axiom

How has this been tested?

Updated existing test methods.dfy

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[robin-aws]

I don't think this is a reasonable interpretation of --allow-axiom. Implicit axioms are things that are assumed true without explicit proof. {:verify false} means attempts at proof DO explicitly exist, but might not be correct or even well-formed.

If you want to allow {:verify false} without warnings I think we should have a separate option. But I'm hoping we don't have the need for that.

[keyboardDrummer]

I don't think this is a reasonable interpretation of --allow-axiom. Implicit axioms are things that are assumed true without explicit proof. {:verify false} means attempts at proof DO explicitly exist, but might not be correct or even well-formed.

That's not entirely true. {:verify false} means attempts at proof MIGHT exist. You can also use this annotation on a bodyless member, to indicate that the contract does not need to be checked for wellformedness and for implying the contract of the base declaration, which is how I was using it.

If you want to allow {:verify false} without warnings I think we should have a separate option. But I'm hoping we don't have the need for that.

What would be use-cases where you want to use on of these options but not the other? To me --allow-axioms means "do not warn me if I'm explicitly skipping proofs". How does it matter if there is an attempt at proof?

[robin-aws]

I don't think this is a reasonable interpretation of --allow-axiom. Implicit axioms are things that are assumed true without explicit proof. {:verify false} means attempts at proof DO explicitly exist, but might not be correct or even well-formed.

That's not entirely true. {:verify false} means attempts at proof MIGHT exist. You can also use this annotation on a bodyless member, to indicate that the contract does not need to be checked for wellformedness and for implying the contract of the base declaration, which is how I was using it.

Fair enough on MIGHT vs. DO. I still stand by the interpretation that axioms are about missing pieces rather than not checking pieces that do exist. If you have something like A && B and you're not checking whether B is well-formed when A is true, I don't think it's right to call that an axiom.

I also don't like the fact that --allow-axiom is about allowing implicit axioms, and actually doesn't care about {:axiom}. I mention that in case there's a way to improve how we talk about both cases and the naming of options.

If you want to allow {:verify false} without warnings I think we should have a separate option. But I'm hoping we don't have the need for that.

What would be use-cases where you want to use on of these options but not the other? To me --allow-axioms means "do not warn me if I'm explicitly skipping proofs". How does it matter if there is an attempt at proof?

I think there's a use case for allowing axioms and not verify false, although I agree there's probably no use case for the reverse.

[keyboardDrummer]

Closing this for now