Only the code of a thrown exception is observed. The generated code throws from nowhere but __fail.

>>> 0 is ToUint32: the non-negative representative modulo 2^32.

Array.from splits by code point, not by the UTF-16 units JS's < uses.

The digits read as a number, with no bound on the answer. A character that is not a digit contributes its code point less 48; strToInt throws that away by printing the answer back.

What __toInt answers: the value, read back and printed again, has to be the string it was handed. That admits exactly the strings String(n) prints for an Int53, so "007", "+5", " 5" and "-0" are all refused.

Where needle first sits in the haystack, counted in code points. The empty needle sits at 0.

A position past the safe integers is what __i53 refuses, exactly as a length is.

s written n times over, one copy at a time.

A result longer than the safe integers is what __i53 refuses, exactly as a length is. An empty string answers before the bound is consulted, because no count makes it longer.

An array holding anything but Strings is past what the compiler builds, so the table leaves it unanswered rather than modelling what JS would print for it.

Map.set overwrites in place and appends a key it has not seen, so iteration order survives both.

What a Map filled from a list of entries holds: each one set in the order the list carries them. This model holds an object as an association list, which can carry a key twice where a real object cannot; a Map keeps the last of such a pair, at the place the first took, and saying so here is what lets a dictionary rebuilt out of an object need nothing of the object's keys.

The whole numbers below n, as the model's numbers.

The runtime helpers the generated code calls. Guarded by the reserved prefix every helper name carries, which is what tells a call to a declaration apart from a call to a helper.

The raised budget is what lets a proof case-split on this table: split builds the splitter with the options this declaration was elaborated under, not the ones in force where it is called.

The calls the table above answers. Stated as an inductive rather than read off helper at the use site because split builds its splitter in whatever module asks, under options that module cannot raise, and this table is past what they allow; here the matcher is at hand. A row added to helper without a constructor here fails helper_row.

A declaration's body function is no runtime helper. Every row of the table names a literal, and none of them carries _ where the body prefix does, so a call the compiler redirects to a body reaches the module's own function and not the table. Read off HelperRow rather than off helper, for the reason HelperRow exists.

=== compares values on scalars and references on everything else. The generated code calls __eq in the latter case, so the model admits only the former.

What a step that does not descend into the value shrinks instead. Entering a mu lands on the ctors node it binds, and resolving a ref lands on the one its binder holds, so both reach rank one and every step after that is measured by the value.

Whether a value matches the type its declaration promised. This mirrors Value.hasTy on every value a caller can hand over; the two are held together by the vectors that call an exported function with an argument of the wrong shape. The one value they disagree on is a dictionary holding the same key twice, which hasTy refuses and this accepts — a Map cannot hold one, and dictKeysDistinctList is the hypothesis that fences it out of the statements that need the two to coincide.

A constructor's fields are read by name, so the order they arrive in does not matter and a key the descriptor does not name is ignored. normTy below is what puts such a value back into the shape encodeValue writes.

What an environment a ref may be resolved in has to be: each binder's alternatives well formed at the depth that binder sits at, which is its own plus everything outside it.

The environment from a binder outwards is an environment: a ref resolved in it is resolved in one whose entries are still well formed at the depth they sit at.

What a binder holds is well formed at the depth of the environment it opens.

The function a call lands on. A binding holding a function shadows the module's own, the way a local name shadows a function declaration in real JavaScript; anything else bound to the name is not something the compiler emits a call through.

The order __sortBy puts its keys in. A number is compared with <= and a string through __strcmp, which is the code-point order the rest of the model already uses for < on two strings.

The keys are asked to be all numbers or all strings, which is more than the helper asks and exactly what the key type gives. Mixing them would put __strcmp on a number, which the model has no answer for.

Evaluation of the generated code. && and || short-circuit as they do in JS.

The combinators are walked here rather than modelled as a function value handed to a helper, so that nothing in the model is ever a closure.

What __fold computes, walked here rather than reached as a call to the helper, the way mapJs is: the node is rebuilt out of the fields the spec names, with each field that came round replaced by the answer for it, and body runs on the rebuilt node with binder bound to it.

A field the spec names and the node does not carry is a missing property read, which this model refuses exactly as member does — real JavaScript reads undefined there, and a node the entry check accepted carries every field its constructor declares.

A field the spec says holds a list of the type coming round. Anything but an array is a value the entry check would not have let through, so the walk refuses it rather than guessing.