String Dispatch

pick can select on a string. Because strings have an infinite domain, a (*) catch-all is always required.

func:failsafe = int32(tbb32:err) { exit 1i32; };
func:main = int32() {
    string:cmd = "start";
    pick (cmd) {
        ("start") { exit 0i32; },
        ("stop")  { exit 1i32; },
        ("pause") { exit 2i32; },
        (*)       { exit 9i32; }
    }
    exit 0i32;
};

How string arms are dispatched

There is no jump table for strings. The IR generator lowers a string pick to a chain of equality checks, each calling the runtime helper npk_string_equals on the selector and the arm literal. The first arm that compares equal runs; if none do, the (*) arm runs.

This means string pick is O(n) in the number of arms — fine for a handful of commands, but if you are dispatching on dozens of strings consider hashing to an integer first and picking on that.

Exhaustiveness

The checker treats string as an infinite domain, so it cannot prove any finite set of string literals is total. The (*) arm is therefore mandatory; omitting it is an Non-exhaustive pick error.

Duplicate string arms

Two arms with the same literal are a duplicate (ARIA-PICK-002):

error: ARIA-PICK-002: duplicate pick arm — "start" is already matched

(K models string as store/normalize only with no string-op rules, so string dispatch is not covered by a K core test — see SEMANTIC_GAPS.md.)