How to execute more than one symbolic transaction

[gustavo-grieco]

We need an API or example on how to execute more than transaction with symbolic data. Typically, when you are doing invariant development you define:

• State transaction functions: take parameters and change the state.
• Invariants: (usually) take no parameters and run asserts.

Right now hevm/echidna cannot use symbolic execution directly with these since:

• State transaction functions can be explored, but they have no assertions, so nothing is really solved.
• Invariants can be explored, but they will only execute concretely as they have no symbolic inputs (except block time/number).

We need an example on how to use the current API or define a new one (one example is listed here, but it is very hacky). We can look on how halmos/certora is doing it. We don't need to start optimizing it right now (e.g. construct the CFG and discard which functions we could discard), but instead we need way to do it manually first.

[blishko]

For reference, here is an article about this topic in halmos: https://a16zcrypto.com/posts/article/modern-invariant-testing-with-halmos/

[gustavo-grieco]

Exactly, but ideally, we should aim for the modern halmos. In practice, I think having the first step where we have a decent API to do it symbolic multi-tx is a great step.