[ivy1.7, ivy1.8] unsoundness with two `after init` blocks #82

plredmond · 2024-11-15T19:09:41Z

Summary

If you have a specification { after init { ... } } containing assertions and also an implementation { after init { ... } } containing actions, you can assert false in the specification { after init { ... } } if the other assertions in specification { after init { ... } } relate to the result of actions in implementation { after init { ... } }.

Steps to reproduce

Put the following in oops.ivy.

#lang ivy1.7

individual x:bool

specification {
    after init {
        assert x = true;
        assert false;
    }
}

implementation {
    after init {
        x := true;
    }
}

Check the file with the following command.

$ ivy_check trace=true oops.ivy

Expected: Line 8 assert false; should fail.
Actual: Whole file passes.

Removing line 7 assert x = true; or removing line 17 x := true; fixes the issue (line 8 assert false; fails). Additionally, moving both the asserts and the actions into a single after init { ... } outside of either specification { ... } and implementation { ... } resolves the issue.

Present in versions

On kenmcmil/ivy@dbe45e7 on macOS Sonoma.

The text was updated successfully, but these errors were encountered:

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[ivy1.7, ivy1.8] unsoundness with two `after init` blocks #82

[ivy1.7, ivy1.8] unsoundness with two `after init` blocks #82

[ivy1.7, ivy1.8] unsoundness with two after init blocks #82

[ivy1.7, ivy1.8] unsoundness with two after init blocks #82

Comments

Uh oh!

Summary

Steps to reproduce

Present in versions

[ivy1.7, ivy1.8] unsoundness with two `after init` blocks #82

[ivy1.7, ivy1.8] unsoundness with two `after init` blocks #82