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

Different result between if statement and if expression #55

Open MadeByMars opened 4 years ago

MadeByMars commented 4 years ago

I wrote something like

instance node: iterable
...
call shim.unicast(self, 0 if node.is_max(self) else node.next(self), m);

Ivy complains that ivy/include/1.7/order.ivy: line 92: guarantee ... FAIL. That assertion is assert exists S. S > x;

Once I change it to:

if node.is_max(self) {
    call shim.unicast(self, 0, m);
} else {
    call shim.unicast(self, node.next(self), m);
}

it passes.

I guess the condition may not be correctly instantiated in if-expression.

kenmcmil commented 4 years ago

The problem here is that the Ivy if-then-else and logical operators are not 'short-circuiting'. This means that the call to node.next occurs whether the condition node.is_max(self) is true or false.

My intention is to change this in the next version of the language. I will leave this issue open until then. Meanwhile, you have to work around the issue, as shown above.