Add precondition/postcondition testing to the compiler's nanopasses

[masak]

The idea is that we don't test exactly what intermediate code the nanopasses emit, but we state clearly (and testably) the expectations we have on their inputs, and the guarantees we leave in their outputs.

The preconditions are partly just the postconditions of all the previous steps (which we don't need to repeat, since they were already tested), and partly things that don't work yet, which we'd rather get caught in a nice error message up front before the step that cannot handle it, than deep inside its logic somewhere.

Here are the current pre/post for our steps:

• Pass 01 (alpha)
  • Precondition: function needs to have a single parameter (a temporary limitation)
  • Postcondition: all symbols are gensyms (for locals), primitives, forms (although not yet), or known globals ("known" means they were passed in with an "already compiled globals" cache)
• Pass 02 (flatten)
  • Precondition: control flow is a straight line; no branching or even function calls (yet; also a temporary limitation)
  • Postcondition: flat, a small closed set of operations (that we can pattern-match on)
  • Postcondition: no globals left, only gensyms, primitives, and forms (although not yet)
• Pass 03 (allocate registers)
  • Precondition: none
  • Postcondition: no gensyms left — 1-to-many mapping from registers to gensyms as evidence

The "evidence" in the last step is something that the pass can leave on a side channel to the postcondition, so that it can easily verify the "soundness" of the register allocation without having to do any work to re-create it.

It strikes me that all postcondition steps up until that point should be run for each nanopass. That is, they act in a cumulative way; each new step checks its new postconditions, but also all of the previous ones. I don't know whether that will always be true, but it is now, and it seems like it would be at least for most steps — we're constantly moving towards lower entropy and a more restricted language. (Edit: Then again, no. See comment below.)

Needless to say, the error message when a pre- or postcondition is broken should be excellent, and make the receiver (me) feel a little bit happy for reading it, discounting the obvious fact that some assumption broke.

I was going to suggest that the pre- and post-testing be switched off by default and switched on by the tests, but I will instead suggest that it be controlled by a switch local to L::B::Compiler, which is on by default and not exported, and with no outside mechanism to switch it off for now. That way, everyone gets the benefit of pre- and postcondition checking all the time, not just the test suite. If and when checking for pre- and postconditions turns into a significant time sink (likely in the future when re-compiling the globals), we can rethink whether to leave them on by default.

[masak]

From this nice introduction to contracts:

Bugs are localized to the violated contract. If a precondition is broken, the program stops right there as opposed to twenty function calls later. If all the preconditions pass but a postcondition is broken, the bug is probably in that specific function body.

I hadn't thought of it that way. I guess that's what I want out of the pre- and postconditions in this case: to localize bugs.

[masak]

It strikes me that all postcondition steps up until that point should be run for each nanopass. That is, they act in a cumulative way; each new step checks its new postconditions, but also all of the previous ones.

On second thought... I think I prefer whatever duplication would happen between the passes, than to couple them permanently using an external mechanism which can't be turned off.

[masak]

Going to close this one, since the work on the compiler in this repository seems to have stalled in a big way.

The good news is that it lives on in syntax-driven (repo), where in some sense I feel it has already gotten further.