[proof-explore | low-priority] A Call for Improved Methods in Proof Exploration

[Stevengre]

Requirement

When exploring the generated KCFG, I want to perform bulk operations similar to SQL/Cypher for querying, updating, and modifying configurations. Additionally, to better align with Solidity, it may be necessary to define some custom syntactic sugar.

Solution

My proposed solution is to provide a Python API rather than relying solely on command-line operations. By leveraging this API, users can quickly locate states with specific characteristics through Python scripts or Jupyter notebooks. This approach eliminates the need for manual and time-consuming mouse operations and ensures reproducibility.

Priority

Low

This is a usability feature that requires effort and is not urgent.

The kontrol show command and kaas visualization can alleviate this issue to some extent.

[ehildenb]

@Stevengre can you provide an example of what you are thinking about specifically? Maybe type out the example interaction you hope to have in the Python terminal?

[Stevengre]

Currently, I can only outline some potentially useful cases, but I am not sure how to design the Python interface to achieve them. Furthermore, I am not yet familiar with the workflow of using kontrol for verification, so it might be difficult for me to provide good examples.

For me, I would like to:

1. Obtain all splits in a kcfg and view their branch conditions.
2. Find all branches of a specific split and compare their and at their termination node.
3. Customize some desugar steps in the output to make it easier to understand the results.
4. Call kontrol's verification service via Python, allowing me to add breakpoints in kontrol for debugging or to familiarize myself with the kontrol code.

It seems that these features could be achieved by directly importing kontrol and using the pyk interface (or putting the under verification program into kontrol's test-suite). I initially wanted to try this, but I found that using kontrol show with bash could achieve similar functionalities, so I gave up. However, I can only get some basic information from the generated KCFG and it is difficult for me to link it with the Solidity code. In other words, I am unable to determine if my algorithm will work effectively on a specific kcfg before trying it out. Therefore, I proposed #742 to integrate merging node directly into kontrol for testing.

Other possible application scenarios include:

1. After a verification failure, batch retrieve failed nodes or nodes, edges, or conditions with specific states, such as the condition of the nth split.
2. Check if a specific lemma is included in the current lemmas and add a specific lemma if it is not included.
3. Batch delete certain failed nodes to continue execution.

[Stevengre]

However, I believe these features might not be necessary once the output of kontrol is improved. Ideally, kontrol should automatically pinpoint the error location and output the possible cause of the error. For example, if verification fails, it should directly indicate which assertion was violated. In case of a timeout, it should output the branch conditions of all current branches or any abnormal call depth/loop count. Users of kontrol shouldn't need background knowledge of K and KEVM. The issues I encountered are actually problems that the developers of kontrol need to address.

[Stevengre]

Therefore, I think I should close this issue and open a discussion about how to eliminate the need for background knowledge beyond Solidity when using kontrol.

[ehildenb]

@Stevengre please also try out kontrol view .... That output should contain much of the information you've listed (though not all of it). So figuring out how to make that work on your machine could help! If it's not working on your machine, then it's a bug.

Perhaps look over the docs again? https://docs.runtimeverification.com/kontrol/guides/kontrol-example/k-control-flow-graph-kcfg

[Stevengre]

The view-kcfg tool is great, but it's not easy to apply node selection or comparison. In other words, I have to select and compare the nodes visually rather than using a simple expression.

[ehildenb]

@Stevengre you can do node comparison with kontrol show --node-delta NODE_1,NODE_2. Does taht do what you want?

No need to close this issue, we can continue discussing how to meet your needs. The reason I ask these questions is to understand what the minimal and fastest improvements we can make are to make your more productive.

[Stevengre]

Thank you! I don't know this option before. I'll try it out!

[Stevengre]

The delta-node option doesn’t show the differences in their path conditions, which I think would be very useful. Was this intentional? If not, I could create a small PR to address this.

[Stevengre]

My IDE supports it.