Clarify the semantics of the various kinds of assertions

[fare]

There is a good reason for our many types of assertions and how they're modeled in Z3. But I feel like we don't yet have a real good story why these are the right thing. I think we must find a simpler higher mental model from which we can derive them, which would allow us to put a single @A require statement that will do the right thing both in the private program and the consensual program.

For instance, I believe that some variant of @A require pred(x, y) would generate code for A that checks properties, code for the consensus that checks the properties when x and y are both revealed, verify that x and y are indeed revealed before any live termination of the protocol (as opposed to A or B timing out), and a safety proof that A can indeed come up with values x and y that satisfy the predicate.