The values the fragment computes with: the ones JsSem has, plus the ones only hand-written code meets — null and undefined reach __ck from the caller, and a function value reaches __map.

stuck is the model declining to answer: a shape no helper produces. It is not an error the generated code can observe, and a theorem about a helper has to rule it out rather than accept it.

===. Across two types it is always false, so a number never equals a bigint. Two references to the same top-level function are the same object, so those compare by name; the model has no other references, and the values that carry one compare as unequal here.

Math.imul: both arguments truncated to int32, multiplied, truncated again.

Comparison. Mixing a number and a bigint is mathematical, the way JS defines it; strings compare by code point, the assumption JsSem.arith already makes.

What a Map filled from a list of entries holds: each one set in the order the list carries them. A later entry under a key an earlier one already took replaces it, at the place the earlier one had.

What Object.fromEntries builds: the pairs written in order, a later one replacing an earlier one that carries the same key, which is where it parts company with a plain List.

Looking a key up in an object or a dictionary: the first entry that carries it, undefined when none does. Duplicate keys are the caller's problem, not this model's — Object.keys and Map both answer from the first match.

The methods the helpers call. toUpperCase and toLowerCase are defined only on the single ASCII letters the callers guard for: the full Unicode mappings are what the helpers exist to avoid.

x[k] for a string k is x.k, so it reads the same way field does: the helpers index an object with a key the descriptor carries, and a Map answers such a read out of its prototype rather than out of its entries.

What a statement list did. A block's own declarations do not escape it, but an assignment to a binding the block did not make does — restore is what tells the two apart.

ext is how a function the generated code passed in gets called: __map is handed one, and the model of the generated code decides what it does.

"With enough fuel". The fuel is the model's device for totality, so a claim about a helper is stated for every large enough amount, the way the claims about the generated code already are.

What a helper call means: __name(args) settles on r once the fuel is large enough.