Executing constructor code with CSE enabled

[nwatson22]

Additions

• Adds option --config-type [SUMMARY_CONFIG | TEST_CONFIG] to kontrol prove to control what mode to create the proof(s) in. SUMMARY_CONFIG mode is for running functions for CSE summarization and TEST_CONFIG mode is for running functions as kontrol tests.
• This mode affects the abstractness of the initial and target node configurations, as well as the behavior when using another proof as setup, as we do for constructor proofs and setUp functions.
• TEST_CONFIG is the default mode. When CSE is enabled, there are recursive calls to foundry_prove for called functions. These calls will always be made with config_type=SUMMARY_CONFIG, because the purpose of running proofs for called functions is to create CSE summaries for them.
• Proofs run with config_type=SUMMARY_CONFIG will always have KCFG minimization enabled.
• Constructors are no longer grafted in the same way as setUp functions. Certain fields are still copied from the constructor final state to the new initial state, but the nodes of the constructor KCFG don't appear in the new KCFG. As such, branching constructors are no longer allowed.
• The constructor bytecode is now only inserted into the program cell when creating a constructor proof, not the code cell of any account.
• Callvalue is now set for constructors in the same way it was for methods.
• _update_cterm_from_node previously assumed Foundry.address_TEST_CONTRACT() is in the accounts list, which is only the case under TEST_CONFIG mode.
• This accounts cell manipulation logic was also breaking with the presence of the ACCOUNTS_REST variable. To handle this, we split those members of the account list into cells and non-cells, with non-cells assumed to be variables.
• Abstracts storage of all accounts in summary mode. The use case for this is when we are executing a function in summary mode using its contract's constructor as a setup proof. We want to use the constructor as a setup proof to get access to immutable and constant variables set in the constructor, but not assume the contract state is as such as no other method has been called since construction. (More might need to be done here.)
• Remove useless constraints at the end of _update_cterm_from_node
• To prevent constructors that modify the storage from branching, always sets static cell to false for constructors, because constructors are always associated with contract creation, which is non-static.
• When CSE rules are generated and included for multiple functions of the same contract, when the LHS of the respective rules are the same except the callData, we needed an additional pair of lemmas to simplify the generated conditions like: true #Equals b"\xe5\xc1\x9b-\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158" ~> .K ==K b"\xe5\xc1\x9b-" +Bytes #buf ( 32 , chop ( VV0_x_114b9705:Int ) ) ~> .K to prevent a branch where the wrong function is called.
• Adds a test in ConstructorTest which exercises using constructors alongside CSE. ConstructorTest.test_contract_call is run, using the constructor for ConstructorTest as setup proof, both in TEST_CONFIG mode, and supported by CSE rules generated by running ImportedContract.add and ImportedContract.set, each with ImportedContract constructor as setup proof, all in SUMMARY_CONFIG mode.
• On test_foundry_dependency_automated, enables --run-constructor. functions are either run with SUMMARY_CONFIG or TEST_CONFIG depending on whether the contract is a "Test" contract.
• Adds test_contract_call to test_foundry_dependency_automated. Re-enables ConstructorTest.run_constructor() in this test.

Further issues

• We need to make sure this works with the test in Integration tests for symbolic constructor #573.
• If you run without CSE, I think currently you can have constructors with arguments in called contracts, you just can't pass symbolic variables as those arguments. Having CSE tests now take into account the constructors means that with this PR, you can no longer have constructors with arguments in called contracts (when using --cse), for the same reason we already can't have constructors with arguments in top-level/test contracts.
• We might want to abstract other contract account fields, e.g. balance when using constructors as setup proofs.
• We might want to have the return value of the constructor used as the new bytecode rather than simply getting the (predicted) bytecode from the compiled json file, otherwise the immutables will not be set correctly.

[nwatson22]

There is currently still a bug with this. When you graft a constructor KCFG to the beginning, this causes a bad circularity module (RHS too general). I discovered this because the circularity rule was conflicting with the CSE-generated dependency rules, which are the same priority, in some cases, causing nondeterministic branches.
The fix for this is going to involve removing the grafting.
This is fixed now by no longer grafting constructor KCFGs to the beginning, only setUp, which are never intended to be used in summary mode.

[PetarMax]

Left a number of comments to resolve/address.