Everything emit refuses by reading the program alone, and the module it compiles to when it refuses nothing. The fuel check is not per vector but per program: Cost.cost is decided from the syntax alone, so one comparison covers every call any caller can make. Bound.programBounded is the same shape for the one result that grows with a value instead of with the syntax.

#eval program.check puts the same wall in a user's lake build, where it costs a compile rather than the differential run emit does. Without it a program that no fuel bound covers, or that the compiler rejects, builds clean and is refused only once lean2js runs.

Checks before it writes. Every vector has to agree between eval and the model of the generated JS, the text of the module has to read back as the module it was compiled from, and the package, assembled in a scratch directory, has to agree with eval on every vector when Node runs it. A disagreement fails the build rather than reaching the package, and so does a node that never got as far as disagreeing — the two are refused under different names, because only one of them is the compiler's to fix.