Move command framer to microcode

[MattWindsor91]

If command framing happens at the Microcode level instead of the BoolExpr level, then we have more/easier access to information about:

• Exactly which variables are being written to—in fact, we could reuse the write map code from normalisation;
• Which variables have been havoced and thus have no assigned value;
• The fact that only variables are being assigned, since BoolExprs are a lot more freeform. So, type safety.

I'm thinking of pushing this through as part of the run-up to #104, but whether or not we need #104 for symbolics is unclear at the moment.

[MattWindsor91]

Closed by #119.