Rewrite Coq pass: de Bruijn compiler with Michelson "strengthening"
type:internal
The new Coq pass is a "naive" de Bruijn pass into a custom representation of a subset of Michelson.
The motivation here is just to make the backend easier to prove and to improve, and easier to read and understand. For users there should be almost no change at all...
After the de Bruijn pass, a new "strengthening" pass, also written in Coq, is applied on the Michelson, in order to keep the stacks small (to reduce typechecking gas) and recover linearity (for tickets etc.)
There is currently one major sleight of hand; a fictional FUNC instruction which provides a "direct" translation of closures, making compilation of closures easier, but also making it easier to do the Michelson strengthening while producing closures with minimal captured environments. This is translated to LAMBDA and APPLY during a final "printing to Micheline" pass. This should be solved somehow later, but, no solutions I found so far seemed worth the cost at this moment, since closures are not even common in contracts. One possible future solution could be to add some version of FUNC to Michelson.
I am sorry this is doing at least two things. I started with an empty Coq file and wrote what I wanted to write, then figured out how to connect it to LIGO at the end -- and that meant moving the production of the "predefined" Michelson pieces from the stacking pass to the "scoping" pass.
I am considering breaking out a separate MR which does the predefined/inline michelson changes only, backporting them to the current backend (deleting or admiting theorem statements and proofs as necessary.)