Improvements to Kontrol UX

[palinatolmach]

There are currently several possible ways to improve the UX of K Foundry:

• Fix broken Discord link in the output:

  evm-semantics/kevm-pyk/src/kevm_pyk/utils.py

  Line 179 in bc5943c

  res_lines.append('Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD')

• Make infinite_gas the default option — will be addressed in Use infinite gas by default in Foundry tests kontrol#38
• When showing the results for failed proofs, distinguish between different failure reasons and show it to the user (e.g., failed assert, failed require , intoverflow, etc.)
• Provide users with a flag that lets them specify which failure reasons they care about, i.e., whether we should look for all possible failures or just, e.g., failing asserts.
• Consider renaming variable names is the generated model/counterexample to match their Solidity counterparts (currently, the names of the environmental variables correspond to the EVM opcodes that is used to retrieve their values). E.g., consider renaming block.number to NUMBER_CELL, x toVV0_x_114b9705;
• Introduce different verbosity levels for foundry-kompile, foundry-prove (Introduce verbosity levels for foundry-kompile #1950)
• Make KEVMCheats a library — will be addressed in Make KEVMCheats a Foundry lib kontrol#11

[yale-vinson]

@palinatolmach Does it make sense to create Backlog Issues for the open items above and then drop them in? I think #2 - #4 are worth considering, but I am a bit ambivalent about the verbosity one. Let me know what you think and I can build some and then add them for discussion in the next standup.