[cse] Precondition Refinement

Stevengre commented 1 month ago

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:

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.
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.
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:

Modify the current --cse option to run the constructor and setUp before executing functions from the leaf to the root of the call graph.
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:

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.
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 commented 1 month ago

[ ] 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 commented 1 month ago

[ ] 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 commented 1 month ago

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 commented 1 month ago

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.

Stevengre commented 1 month ago

Thank you for your comments, @PetarMax! Here are some of my thoughts. There are indeed some points I don't understand and am not familiar with. So if my explanations have any issues, please let me know.

Which specific improvements do you see with respect to the specific initial state of activateNextState?

Inputting a purely abstract initial state would generate more branches than expected and could lead to some unreachable states under a reasonable initial state. Therefore, we need to refine the initial state to a reasonable state set to make the proof pass.

I believe this is why we need to execute constructor and setUp before running the harness. Essentially, I think they serve as the precondition specification similar to Hoare Logic. The setUp function sets up the test environment, but this environment is fundamentally the function's precondition. Otherwise, the setUp is incorrect and cannot serve as a valid spec for the function verification.

Regarding activateNextState, the current --cse cannot generate a correct summary for ActivateNextStateTest.testActivateNextStateTermination and will result in a failed proof. I believe running constructor and setUp before the harness will help generate a correct summary. This way, all harnesses in ActivateNextStateTest can reuse this summary for verification, as they share the same precondition.

Additionally, I want to integrate merge_node into minimize-proof to evaluate the correctness and performance of merge_node.

Which values need to be constrained more tightly?

Sorry, I'm not sure. I think it's some variables assumed in the setUp function, but I don't know the specifics. The reason I concluded that we need to add the constructor and setUp to the CSE process is that when I directly match-tested activateNextState, it quickly reverted. However, after adding --run-constructor, it couldn't terminate. So, I suspect that setUp constraints certain values, reducing the number of branches and allowing the verification to pass within 20 minutes.

Why do the proofs fail specifically?

I think @palinatolmach addressed this question, but I'm not sure.

What are the branches that you see?

In fact, when I ran match-test activateNextState with --run-constructor, I didn't get a result. I started the process at 4 PM, but by the next morning, it had failed. Is there a way similar to krun --depth to stop it midway and print the results?

The way to get tighter pre-conditions is through annotations, which I believe @palinatolmach is implementing.

I also think it's a better approach, but it seems to take more time. Is there anything I can do to help, @palinatolmach?

Since I cannot validate the correctness of merge_node though code / kcfg review, I'd like to use it directly for LIDO. However, before merging nodes, I need to obtain a correct summary without minimization.

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.

Yes. So I think we need to remove unrelated context from the generated rules. As I mentioned before, I believe setUp serves as a precondition specification. What we need to do is eliminate the non-spec parts, such as the test contract loaded into <accounts>.

Moreover, constructors should be run only if there are immutable variables present. This should be understood by Kontrol automatically.

Ok, I understand. If we execute the mutable variable parts, the pre-state would be too concrete to be reused. But why are the results of match-testing activateNextState with --run-constructor different from those of match-testing activateNextState without it? And why is the result of match-testing activateNextState with --run-constructor different from match-testing testActivateNextStateTermination?

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.

Sorry, I don't fully understand these points. Is there anything I can help with?

Stevengre commented 1 month ago

Thank you, @palinatolmach! I'll give it a try!

Stevengre commented 1 month ago

The NatSpec (#650 and #662) might be the most pure solution for this refinement.

runtimeverification / kontrol