Tips, FAQ page

[reekamaharaj]

Things to add to an FAQ page

• Suggestions/things from notes can be added here

[reekamaharaj]

• [x] Adapted from @PetarMax on slack, can be added to a FAQ page, or a debugging tips page

A proving/debugging process:

1. Run the proof with no-break-on-calls, --max-depth 10000 and --max-iterations 5 or 10
2. Inspect the kcfg for branching.
3. If there is branching and check the branching condition is true or false:
   • Try to gigure out the simplifications to discharge it - for this to be most efficient, one has to be familiar with what simplifications already are there
   • Add the simplifications and a runLemma => doneLemma style claim that demonstrably simplifies the branching condition
   • Remove the branching node from the kcfg using foundry-remove-node
   • repeat from 1
4. repeat from 1

[reekamaharaj]

From @lucasmt Notes

• [x] If kontrol foundry-prove hangs during an execute step (after hours without a response) or crashes because kore-rpc returned an empty response, it could be due to the configuration becoming too large. To troubleshoot, inspect the node that was being extended using foundry-show or foundry-view-kcfg. Check if there are any unusually large expressions in any of the cells and consider writing lemmas to simplify them.
• [x] When writing a claim using the runLemma-doneLemma pattern to check if an expression simplifies, it's important to remember that running the claim includes an implication check. This means that if your claim is in the form of runLemma(A) => doneLemma(B) and it passes, it doesn't guarantee that A fully simplifies to B. Instead, it might simplify to an expression B' that implies B.
• [x] If you are using the infiniteGas cheatcode and the expression in the <gas> or <callGas> cell is growing out of control without being simplified, you can call kontrol foundry-prove with the --auto-abstract-gas option. This will automatically abstract the gas expression into a symbolic variable. Only do this if you are not concerned with measuring gas consumption, as you will lose that information. If possible, write lemmas to simplify the gas expression instead.
• [x] Some instructions in KEVM will cause branching based on whether a symbolic address already exists in the <accounts> cell or if it is a new address. This situation arises when the prank cheatcode is called with a symbolic address (refer to this issue for an example in foundry-show). To resolve this, the usual solution is to add one vm.assume(symbolicAddress != ...) for each of the preexisting addresses. These addresses should correspond to:
  • the test contract address
  • the cheatcodes contract address, and
  • the address of any other contracts deployed within the test.
  • [x] The && and || operators are short-circuit operators, meaning they introduce branching when evaluated. This means that if you have a line like vm.assume(p && q) or vm.assume(p || q), it will introduce branching in the execution, which might not be immediately apparent.
  • [x] When adding a new lemma to remove an unnecessary branch, be sure to delete the split node from the KCFG before continuing. Otherwise, both branches will still exist, but the unnecessary one will simplify to #Bottom.

[reekamaharaj]

From @lucasmt Notes

Decoding KEVM expressions

• [x] Solidity uses bitwise expressions, such as maxUInt160 &Int X, to extract a variable with a specific number of bits from a larger word. The number of bits can often provide a clue about the type of the variable. For example, maxUInt160 typically represents an address, while maxUInt8 represents a boolean value.
• [x] When using the symbolicStorage cheatcode, you may encounter expressions like #lookup(?STORAGE0:Map, 6). This expression accesses storage slot 6 of the symbolic storage represented by the STORAGE0 variable. If you want to determine which storage variable this expression corresponds to, you can follow these steps:
  • First, ascertain the contract that STORAGE0 corresponds to.
    • The first call of symbolicStorage creates the symbolic variable STORAGE, followed by STORAGE0, STORAGE1, STORAGE2, STORAGE3, and so on. Therefore, you can use the order in which symbolicStorage was called in each contract to map each variable to its contract.
    • Another option is to check the <accounts> cell in the KEVM configuration. In each <account>, the <acctId> cell contains the address of the contract, and the <storage> cell contains the storage. If you know the address of each contract, you can map it to the storage variable.
  • Next, determine which variable corresponds to storage slot 6.
    • The easiest way to do this is by calling forge inspect ContractName storage, where ContractName represents the contract identified in the previous step. This command will output a JSON result, with the storage field containing a list of all storage slots in the contract. The label of each slot corresponds to the name of the storage variable.
  • Some storage slots contain more than one variable at different offsets. If your expression is, for example, #lookup ( ?STORAGE0:Map , 6 ) >>Int 8, this is offsetting the storage slot by 8 bits, or 1 byte. This means that in the previous step you should look for the variable at that storage slot with offset 1.

[lucasmt]

More tips for debugging:

• [x] Use the Forge debugger (https://book.getfoundry.sh/forge/debugger) if you need to understand why the memory looks a certain way at some point of the execution (you will probably need to create a version of the test with concrete rather than symbolic values). You can use it to set breakpoints and then step through the EVM code to see how the memory changes. This can be helpful to understand details about the Solidity memory layout that are not well-documented.