Correctness at the boundary a caller crosses: one public function #

Turns the fragment's expression-level correctness into a claim about one public function. The bridge is built at the boundary a caller actually crosses: the entry check the generated code runs on its arguments, the environment that check hands the body, and the fuel the model spends getting there.

The entry check #

Value.hasTy is what evalCall requires of an argument; Js.checkTy is what the generated function runs on the encoded one. They are separate definitions over separate value types, so nothing but a proof holds them together.

The environment a descriptor is read under #

tyDescIn walks under a stack of the declared types it is inside; the entry check walks under an environment of what those types bound. StackAgrees is the two lined up: the k-th binder of the environment is what expanding the k-th name on the stack produces, from that point outwards.

Reading the shape check #

Js.checkTy is well-founded too, so it needs the same one-lemma-per-shape treatment Value.hasTy got.

Finding a constructor's descriptor #

Value.hasTy looks the constructor up in the declaration; the generated check looks it up in the descriptor list the compiler built from that same declaration.

The entry check agrees #

If a value satisfies the type its declaration promised, its encoding passes the shape check the generated function runs at the boundary. This is the positive direction only: a value that fails Value.hasTy is left to the run-time agreement check.

Normalisation leaves the canonical shape alone #

encodeValue already writes tag first, the declared fields in declared order, and nothing else, so the entry check's normalisation has nothing to rebuild on what the reference semantics produced.

The walk out reads the same value through its declared type #

outTy parts from normTy at one node and encodeAt parts from encodeValue at the same one, so the two meet: what a declaration's entry hands back is the value the reference semantics produced, read through the type the declaration was declared to return.

encodeValue v on the left is what the body built, which is what decl_correct says, and the walk is what the entry runs over it. Where the return type reaches no dictObj, Js.outTy_eq_normTy makes this normTy_encodeValue again and the entry emits no walk at all.

The entry check refuses #

The other direction. What matters at the boundary is not that a bad Value fails the check — it is that everything the check accepts is the encoding of a value the reference semantics accepts too, which is what turns a refusal on one side into a refusal on the other.

The claim is stated about JS values rather than about Values because encodeValue is not injective: an Int53 and a UInt32 holding the same number both encode to .num, so nothing on the generated side could tell them apart. Over Values the direction is false; over what actually crosses the boundary it holds.

The entry check reads back what the walk out wrote #

A call through a function value goes to the entry, which hands its result back through the declared type. What the caller is holding is then encodeAt, not encodeValue, so the check it runs on the way back in has to accept it and rebuild the Map the module works in. These are checkTy_encodeValue and normTy_encodeValue with encodeAt on the left, and they part from them at the one node the two encodings part at.

Normalisation leaves the canonical shape alone #

encodeValue already writes tag first, the declared fields in declared order, and nothing else, so the entry check's normalisation has nothing to rebuild on what the reference semantics produced.

The entry environment #

A public function's body runs under two layers: the checked parameters the entry left on top, and the raw __p0, __p1, … the check read them from. Value.hasTy knows nothing about either, so the two have to be lined up by hand. The reserved prefix is what keeps the layers apart.