search

microsoft / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
223 stars 80 forks source link

wrapping code in "if true {...}" causes verification condition to fail #60

Closed nano-o closed 4 years ago

nano-o commented 4 years ago

Hello, I have a case where wrapping code in "if true {...}" causes a verification condition to fail. The code is here: https://github.com/nano-o/ivy-proofs/blob/bfbeed009f44a4d84852b7d62c7e4588f6c27f9e/multi-paxos-impl/multi_paxos_system_2.ivy

The issue can be demonstrated by running: ivy_check isolate=system.iso_model action=shim.two_b_handler.handle multi_paxos_system_2.ivy. With lines 326 and 362 of multi_paxos_system_2.ivy uncommented, it fails. Commenting them out, it passes.

nano-o commented 4 years ago

I now remember that there was a (possibly different) problem triggered by adding "if true {}" around code. It had to do with macros, and there is an attempted fix in branch macro. But it looks like it never made to master.

kenmcmil commented 4 years ago

Thanks, Giuliano. I can see there's a bug in the VC generation. Until I can get it fixed, please avoid "if true"!

nano-o commented 4 years ago

Okay, will do. But the problem also happens if I replace true by the condition I need.

nano-o commented 4 years ago

Any hint about what triggers the bug, so that I can work around it in the meantime?

kenmcmil commented 4 years ago

That's interesting. I thought that the problem was an incorrect optimization, but I guess not. I'll look into it.

nano-o commented 4 years ago

It might be the case that my condition was a tautology in the given context (but I don't have that exact code anymore). I'll post other examples if it happens again.

nano-o commented 4 years ago

The problem came up again here: https://github.com/nano-o/ivy-proofs/tree/d09cf253eeb5186393c6f23597f90862c390791a/multi-paxos-impl This time it does not seem like there is a vacuous if condition involved.

ivy_check multi_paxos_system_2.ivy succeeds. But if you comment-out the seemingly useless assert at line 357, then the require at line 66 of multi_paxos_protocol fails, e.g. ivy_check isolate=system.iso_model action=shim.two_b_handler.handle assert=multi_paxos_protocol:66 multi_paxos_system_2.ivy fails. Also, if you place that assert inside the next if statement, the assert itself fails.

kenmcmil commented 4 years ago

Fixed in commit da91bef.

That bug has been in the VC generator for years.