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

[plredmond]

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.