A dict whose key type is wider than its init domain panics at runtime when an action indexes a key that was never initialized.
Repro
module M
const HOLDERS: 0..5
var bal: Dict[0..5, 0..30]
var total: 0..30
init { bal = {h: 0 for h in 0..HOLDERS} and total = 0 }
action Mint(h: 0..5, amt: 1..3) { require h <= HOLDERS; require total + amt <= 30; bal = bal | {h: bal[h] + amt} and total = total + amt }
invariant C { sum(bal) == total }
specl check m.specl -c HOLDERS=3 => index out of bounds: the len is 4 but the index is 5 (panic at crates/specl-mc/src/state.rs:460).
The dict's IntMap is sized to the init domain (4) but the key type / action parameter ranges over 0..5. Expected: a clean type/compile error (init must cover the full key domain, or indexing an uninitialized key is rejected), not a panic.
A dict whose key type is wider than its init domain panics at runtime when an action indexes a key that was never initialized.
Repro
specl check m.specl -c HOLDERS=3=>index out of bounds: the len is 4 but the index is 5(panic at crates/specl-mc/src/state.rs:460).The dict's IntMap is sized to the init domain (4) but the key type / action parameter ranges over 0..5. Expected: a clean type/compile error (init must cover the full key domain, or indexing an uninitialized key is rejected), not a panic.