[iv1.7, ivy1.8] collections.ivy array.append unsoundness bug

[plredmond]

Summary

Appending to an array whose domain is already exhausted should be an error, however it results in unsoundness (assert false; passes).

Steps to reproduce

Put the following in a file oops.ivy.

#lang ivy1.8

include collections

instance domain_t : iterable
type range_t
instance array_t : array(domain_t, range_t)

action oops = {
    var a: array_t;
    a := array_t.create(domain_t.max, 0);
    a := a.append(0);
    assert false;
}

export oops

Check the file with the following command.

$ ivy_check trace=true oops.ivy

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

Removing line 11 a := a.append(0); fixes the issue (line 12 assert false; fails).

Present in versions

On kenmcmil/ivy@dbe45e7 on macOS Sonoma.

---

Found by @nano-o.