Kontrol Weekly Update

[yale-vinson]

Weekly report to update progress made by the Kontrol Team, comprised of a bullet list of where we are, what was completed, what's up next, etc., as well as a blog style recap for those that might want a little more detail.

As usual, the author reserves the right to modify the format as the project progresses in order to strive for continuous improvement and utility for the audience.

[yale-vinson]

TL;DR Summary

Where We Are

• Functions with array arguments give "Unsupported ABI type for method` error (Hao)
• Parallelize symbolic execution of tests (Noah)
• Issues running kclaim style proofs (Noah)
• Add struct support (Palina)
• Optimize symbolic execution using depth-based call graphs (Andrei)
• Clarify and Improve --test Parameter Functionality in kevm foundry-prove (Andrei)
• Downstream testing using engagement codebases (Juan)
• kevm foundry-prove: not running the constructor leads to unexpected behavior (Noah)
• Execution of contract initialization code (Noah)
• Add '--smt-tactic ' command-line option (Georgy)
• Introduce booster-doctor --- kore-rcp-booster abort analysis tool (Georgy)
• Make booster the default, disable tests on legacy backend (Everett)

Up Next

• Usability improvements to foundry-merge-node
• Automatically detect and warn user on bad branches
• Report SMT solver timeout in CLI output
• Outdated K causes incorrect KEVM/Kontrol output
• Run Nix tests on CI
• Move foundry.md from evm-semantics to kontrol
• Update documentation link in output

The Week That Was (29 Sep - 5 Oct)

I will try to normalize this over the next few weeks, but for this week I want to focus on some general items that the team has been working on over the last several weeks to reorganize the work on Kontrol.

The Triage status was a bit of a dumping ground with several aged items, so the team spent a few Standup meetings moving these items to the Backlog, In Progress, etc. to empty the Triage list except for items added since the last Standup.

Next, we added a new section to the Project Board inspired by the K Team titled Next Up, which is a list of the highest priority items from the Backlog. When the team completes an item or finds themself with bandwidth, they will first look at Next Up to ensure that we are focused on the most important items.

We added a few other nuances to the project board, listed below:

• More priority classifications to add subtlety to the relative priority of items in the Backlog
• Classification field to group items into Issue categories
• Added Blocked, Investigation, and Maintenance statuses to improve Project Board organization

Once we reworked these elements, Palina and I worked on re-prioritizing the Backlog and reviewed the Backlog with the team to ensure that we got the order right. From here, we are using the following general criteria to assess the relative priority of new issues opened in Kontrol:

• If the Issue is critical for the success of a paid engagement, it goes to the top of the list
• If the Issue significantly improves the Performance of Kontrol, then it is the next highest priority
• If the Issue significantly improves the User Experience, then it is balanced against the Performance Improvements from the previous item
• Remaining items are prioritized below these three classifications as agreed upon by the team

It is important to note that, much like the Pirate Code, these are guidelines as opposed to hard and fast rules, meaning that each item can be considered higher or lower priority depending on a number of factors that are not addressed in the criteria above.

With this new framework in place, the team meets Tuesday and Thursday to work through the Triage list to avoid a buildup, then update status on Issues In Progress, and assign new tasks to team members with bandwidth. In weeks to come I will update this Issue in the Maintenance section of the Project Board with details on how the work is progressing, so look back here every Friday for the latest news on Kontrol.