Truncated division never leaves the Int53 range the numerator was already in, which is why __i53div can return without the range check the model still writes.

What a call has to satisfy for the shipped source to answer what the model's table says. Three rows are the model being the more careful of the two — two re-check an Int53 range the type has already given, and one is stated on dictionaries a Map can actually hold — and one is a real divergence.

Every row of Js.helper is answered by the JavaScript the compiler writes out, so what the helpers behind the table are left trusted for is what helperArgsOk still asks of a call.

The table is not the whole of what the model assumes about hand-written JavaScript. JsSem.eval carries __ck, __out and the seven traversal helpers as rules of its own rather than as rows, and those are answered by HelperProof.calls_ck_checkTy, calls_out_outTy, calls_map, calls_filter, calls_find, calls_all, calls_any, calls_reduce and calls_sortBy. calls_out_outTy is the one of those that asks something of its argument: __out walks a value the declared type accepts, which is what the entry hands it and what decl_correct says the body produced. __sortBy asks something of its arguments the way four of the rows do: the keys of one call are all numbers or all strings, which is what the key type the compiler insists on gives.