The syntax the proof reaches.

Every shape of the subset is in the fragment. The proof reaches the whole syntax, so the induction the judgement drives reads as a case analysis on the expression.

Everything the correctness proof reaches is also reached by type soundness, which the arithmetic cases need to know that the values in the environment match the types the compiler read.

The relation "given enough fuel, the generated code returns this value". Quantifying the fuel existentially lets subexpressions compose even when each needs a different amount.

A constructor value is an object literal whose first field is the tag.

The list an object, array or dictionary literal evaluates before it builds the value.

The string helpers the compiler emits compute what applyStrUn and applyStrBin compute; the two sides are written as the same functions on the code points.

indexOf is the one string pair that can fail: a position past the safe integers traps the way a length does.

repeat is the other one: a result longer than the safe integers traps before the string is built.

substring counts code points on both sides. The model's extra guard against a bound outside the safe integers is the one the reference semantics gets from the argument being an Int53 at all.

The dictionary helpers read and write the encoded entries the way the reference semantics reads and writes the entries themselves; the encoding only touches the values.

A field read finds the field, not the constructor's name the value carries in front of it. The two cannot collide: a type may not declare a field named the key it carries that name under, and the fragment reads no such name.

The array reads count elements on both sides. The model's extra guard against an index outside the safe integers is the one the reference semantics gets from the index being an Int53 at all.

Encoding preserves equality, but only between values of one type. Untyped the statement is false: Int53 0 and UInt32 0 are different values that both encode to .num 0.