Lack of documentation on how to execute bytecode-only Ethereum contracts

There is no clear documentation or examples of how to symbolically execute a bytecode-only Ethereum contract. In this case, the ABI will be provided by the user, but there is no public interface to associate it with bytecode to run.

Further explanation:

We need clear documentation and examples for creating and interacting with bytecode-only contracts. There are two sets of scenarios to consider: ones where a constructor generates the running bytecode and one where we just paste in an already-known and running bytecode.

The documentation and examples should contemplate the association of a previously known ABI description and the usage of symbolic parameters on both create and normal transactions.

Here are some writeups we would love to see!

• Create and analyze a contract account from the constructor bytecode
• Create and analyze a contract account from the constructor bytecode that uses concrete arguments.
• Create and analyze a contract account from the constructor bytecode that uses symbolic arguments.
• Create and analyze a contract account from the runtime bytecode
• Send transactions with concrete arguments to bytecode-only contracts using the ABI module
• Send transaction with symbolic arguments to bytecode-only contracts using the ABI module
• Associate a known ABI with a bytecode-only contract and then use EVMAccount to send transactions with concrete parameters to it
• Associate a known ABI with bytecode-only contract and then use EVMAccount to send transactions with symbolic parameters to it
• Iterate over final states and print out interesting knowledge about the accounts. E.g., balance, storage values, or other invariants.

You may want to reference the minimal_bytecode.py example to get started!