Associate doc strings with all Push instructions

[Vaguery]

At the moment almost all instructions are defined using a macro called define-registered which does a bunch of stuff to register the instructions in a global catalog and so forth.

Also at the moment, none of the actual instructions are documented in a useful way; rather, some of them have comments.

It makes a kind of sense to (a) change the define-registered macro so it takes a string argument and socks it away in the metadata, (b) go through the entire codebase and fix the strings.

This probably touches on things mentioned in #122 and #147.