An invariant between two slots defaults both sides

Pitfall 18 of writing Soma, the programming language: a habit from another language, or a rule that surprises, with what the Soma compiler answers and the form to write.

An invariant is checked on every write to either slot it names: the written slot is its new value, the other one is read at the SAME key — and a key it has no entry for reads as (), which no comparison accepts.

memory { a: Map<String, Int>  b: Map<String, Int>  invariant a + b <= 100 }
// error: memory invariant between slots (a, b) — the other slot is read at the
//        SAME key, and a key it has no entry for reads as (), which no
//        comparison accepts: default the sides (`(reserved ?? 0) <= (stock ?? 0)`)

memory {
    stock: Map<String, Int>  reserved: Map<String, Int>
    invariant (reserved ?? 0) <= (stock ?? 0)   // runtime-checked on both slots
}

A rule between two slots stays runtime-checked (verify cannot prove it by induction). size invariants are enforced on delete too: invariant size >= 1 rejects removing the last entry.