[cse] Precondition Refinement

[Stevengre]

Background

Presently, the CSE initiates symbolic execution from the call graph's leaf nodes progressing towards the root (enabled by the --cse option). The contract execution commences either from the symbolic values of its parameters or from the state post-execution of the constructor (using --run-constructor). This approach results in overly abstract initial states for the functions, making it exceedingly time-consuming to determine the final states of the functions. Consequently, this prevents us from synthesizing reusable function summaries.

Running Example

Using DualGovernance.activateNextState() as an example, the ActivateNextStateTest.testActivateNextStateTermination serves as a test harness for this function. The current situation is as follows:

1. kontrol prove ActivateNextStateTest.testActivateNextStateTermination: The proof is successful. The process starts from the root of the call graph, executing the constructor and setUp before running testActivateNextStateTermination, and finally invoking activateNextState.
2. Adding cse with kontrol prove ActivateNextStateTest.testActivateNextStateTermination --cse: The proof fails. This failure occurs because DualGovernance.activateNextState() is symbolically executed without calling the constructor and setUp, resulting in a PROOF-FAILED outcome for DualGovernance.activateNextState(). Consequently, ActivateNextStateTest.testActivateNextStateTermination inherits this failure when it uses the summary, leading to its own failure. This indicates that we should not execute activateNextState from the most abstract state to obtain its summary, i.e., kontrol prove DualGovernance.activateNextState.
3. Adding --run-constructor with kontrol prove DualGovernance.activateNextState: Verification out-of-time or out-of-memory. While the function inputs are correctly configured by the constructor, the state includes improbable and unreasonable conditions that can arise during function calls. The excessive branching states prevent termination. Even if termination is achieved, the final state obtained through minimize_proof and node merging remains too abstract, causing the verification to fail.

Solution

To address the above problem, precondition refinement is necessary: more reasonable constraints should be provided for the initial state of the function. The following approaches can be considered. Given the simplicity of the activateNextState example, the first approach should suffice to resolve the issue:

1. Modify the current --cse option to run the constructor and setUp before executing functions from the leaf to the root of the call graph.
2. Introduce a new method to specify preconditions for each contract function, where the initial state is derived from these preconditions.

Additionally, function summaries should do the following before being included as lemmas:

1. Ensure the summary can be used by removing any context unrelated to the callee contract and function, such as the test contract loaded during setUp.
2. Improve rewrite efficiency by minimizing summaries using minimize_proof and node merging.

Result / Expected

Upon the successful implementation of minimize_proof with node merging (issue #703), all tests within ActivateNextStateTest are expected to be verified within seconds or minutes.

[Stevengre]

• Add the constructor and setUp to the --cse process. The execution sequence will be: constructor -> setUp -> call graph's leaf to root.
• Add the --minimize_proof option to automatically minimize the summary during --cse.
• Add the merge_node functionality to minimize_proof.

---

Results: These implementations will improve the performance in verifying all the test harnesses in ActivateNextStateTest.

[Stevengre]

• Remove unrelated context from the generated rules.

---

Results: This will improve performance when verifying functions that use activateNextState, but are not in the ActivateNextStateTest contract.

[PetarMax]

Which specific improvements do you see with respect to the specific initial state of activateNextState? Which values need to be constrained more tightly? Why do the proofs fail specifically? What are the branches that you see?

The way to get tighter pre-conditions is through annotations, which I believe @palinatolmach is implementing. CSE should not use a setUp function, because the entire point is to run the function in isolation, and not as part of the testing environment. Moreover, constructors should be run only if there are immutable variables present. This should be understood by Kontrol automatically.

The problems that are not allowing us to get activateNextState running in CSE mode are, as far as I remember (I do need to try again), are:

• a sorting error originating from the compier, where a cell map fragment is put instead of a cell map - this needs to be fixed in the front-end, but I don't know who is handling that (@ehildenb, who should I ask?);
• map unification, which will soon be enabled in the Booster; and
• syntactic simplifications, which will also soon be enabled in the Booster.

[palinatolmach]

I just tried running DualGovernance.activateNextState, and I think it also reverts on all branches because it tries to call contracts or interfaces that are not in <accounts>, even with --cse. I think there's a way to address it with @custom:kontrol-instantiate-interface and making sure that we add an account for each contract field.