Storage

memory {
    accounts: Map<String, Map> [persistent, consistent]  // → SQLite; records as values
    cache: Map<String, String> [ephemeral, local]        // → in-memory
    rows: List<Map> [persistent]                         // an append log: push / rows[i] = v / rows.delete(i)
    balance: Map<String, Int> [persistent]
    invariant balance >= 0 && balance <= 1000   // checked BEFORE every .set()/.push() commits
    invariant size <= 10000                     // entry-count bound (all slots in this section)
}

// Invariant bindings: <slot name> and `value` = the value being written,
// `key` = the key, `size` = entry count after the write, `status` = the state
// of the machine instance whose id is the key (the cell must declare a
// `state` machine). A `status` rule ties the lifecycle to the data and is
// checked on every write of the slot AND on every transition() of that id
// (with the target state), never proven by induction:
//   invariant status != "released" || (balances ?? 0) == 0   // no released escrow keeps a balance
// An invariant
// that names slots guards only those; one using just value/key/size
// guards every slot in its section. A violating write raises a
// try-catchable error and the slot is UNCHANGED. `soma verify` proves
// literal, clamp(), require-narrowed and read-modify-write forms by
// induction (docs/guarantees.md); what it cannot prove is runtime-checked
// and reported as ⚠ (a failure under --strict).
// Invariants may call builtins only.

// In handlers:
accounts.set("a1", map("owner", "ada", "cents", 100))
let a = accounts.get("a1")          // returns () if missing
a.cents = a.cents + 5               // edit the copy, write it back:
accounts.set("a1", a)               // (or accounts["a1"].cents = 105 in one step)
accounts.delete("a1")
let keys = accounts.keys             // list of keys
let vals = accounts.values           // list of values
let n = accounts.len                 // count
// Those aliases are the bare form only: with an argument the name is the
// builtin over the slot's content — `rows.all(r => r.ok)` is `all(rows, …)`,
// `rows.count(p)` counts the matches (bare `rows.count` is the entry count).
// The value type is enforced on every write: Map<String, Int> refuses a
// String or 1.5 (kind `type`); an Int written to a Float slot becomes a
// Float; Map<String, Pay> takes only Pay variants. Ints of any size,
// Floats (NaN, inf), (), variants and nested maps/lists round-trip exactly.

// No to_json needed for values: a map stored is a map read back.