search

kenmcmil / 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
77 stars 24 forks source link

ivy_check assert=file:line doesn't really work #65

Open maxvonhippel opened 2 years ago

maxvonhippel commented 2 years ago

Per our discussion today. (I'll update with instructions to reproduce shortly.)

maxvonhippel commented 2 years ago

The problem occurs when you do, for example

ivy_check trace=true complete=fo assert=TCP:200 TCP.ivy

and it says 

...
OK

but then you run (in this case)

ivy_check trace=true complete=fo TCP.ivy

and among other things you get back

TCP.ivy: line 200: guarantee ... FAIL

I'll post a commit hash for reproducing w/ our model soon.

Note also, it would be nice if assert=file:line would check everything in the context of that line and not just the line itself. For example, I often find that I get a collections.ivy failure but it won't be reported if I check only the relevant line of my code as everything else (even stuff "in context") is assumed to pass.

maxvonhippel commented 2 years ago

Ok, you can reproduce using our TCP code w/ git hash ba6b042c8c2cc07c669d18958e234d36434709c6 and line 200 of TCP.ivy. I've pushed to both github and bitbucket so you can pull from whichever you'd like.