Improve proof management

[JuanCoRo]

During the verification of a property, multiple kcfg files are produced. Comparing and inspecting back and forth such files is often part of the verification process. Here are some improvements that would reduce the friction of handling such files.

• [ ] Have kontrol foundry-show testProperty and kontrol foundry-view-kcfg testProperty default to the latest kcfg of testProperty. Currently, if there are multiple kcfgs for testProperty, an error is thrown asking for the desired id
• [ ] Have kontrol foundry-show and kontrol foundry-view-kcfg with no more arguments show all different proofs possible for display, so that the user can interactively pick one from the list
• [ ] Allow deletion of kcfgs from the cli tool, perhaps with a new command like kontrol foundry-manage-kcfg
• [ ] Add KEVM/Kontrol version to proofs as logging info, similarly as ids. Such information would be displayed with kontrol foundry-list, and could be included with foundry-show and foundry-kcfg
• [ ] Allow users to custom proof names. For instance, appending some string to Test.testProperty like Test.testProperty-ModificationA. This would allow for keeping better track of the particularities of each proof

[yale-vinson]

@JuanCoRo Is this something specifically related to Solady, or is more general than that? If it is, how does the priority of this compare with other tasks associated with that project?

@hjorthjort Is this at all related to the items you have identified for Kontrol in support of the STXN engagement? I have a feeling this will help you too, but perhaps it makes sense to take this into account with those items so that we can effectively kill two birds with one stone?

[JuanCoRo]

@yale-vinson This is not project-specific, as it would impact (in a good way) the proof management of any project. As per priority, it doesn't fall into the "we're dealing with this issue by having internal expertise" and is not making us waste days. Regardless, it is true that having a more complete and intuitive proof management system would reduce friction during verification engagements, so it's not purely a cosmetic nice to have. In short, managing proofs is a task for every verification project, and the above are all improvements on how to do it. It's not blocking anything, but would make the verification process more efficient.

[hjorthjort]

@yale-vinson these are all better suggestions than the one I suggested.

[yale-vinson]

@JuanCoRo & @palinatolmach Is there anything we should pull into the backlog from this? I think we can hand some of this off to the KaaS team, as we discussed several of them in the User Feedback sessions. Let me know what you think and we can plan from there.