Revisit input formalism

[makaimann]

There are two world-views for how inputs should behave in a transition system:

1. they should be state variables with no update constraints
2. they should be affiliated only with the transition and thus not be involved in any formula referring to a set of states (only sets of pairs of states -- e.g. the transition relation)

Option 1 makes more sense in hardware and less sense for relational systems. However, adhering to closely to 2 can also cause problems (see #261). We should discuss how to best unify these ideas for different inputs to Pono.

[Po-Chun-Chien]

MoXI, a recently-proposed intermediate language for model checking,
treats inputs as a kind of state variable.

3.1 System Definition
...
3. partitions state variables into input, output, and local variables;

Although MoXI describes a system in a "relational" way,
I think it aligns more closely with option 1.