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.
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 whenx
andy
are both revealed, verify thatx
andy
are indeed revealed before any live termination of the protocol (as opposed toA
orB
timing out), and a safety proof thatA
can indeed come up with valuesx
andy
that satisfy the predicate.