> For the complete documentation index, see [llms.txt](https://docs.runtimeverification.com/kontrol/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.runtimeverification.com/kontrol/guides/kontrol-example/linked-library-example.md).
# Debugging a Proof
In Solidity, a library is a collection of functions that other contracts can call. If you're unfamiliar with libraries, we strongly recommend checking the [official documentation](https://docs.soliditylang.org/en/latest/contracts.html#libraries). An important note is that if a library only has internal or private functions, it is considered an embedded library and will be deployed with the contract that uses it. However, if a library has at least one external or public function, it needs to be deployed independently of the contract. Additionally, the generated bytecode of the contract that uses this library will have a placeholder like `__$30bbc0abd4d6364515865950d3e0d10953$__` in place of the library address, as the compiler does not know where the library will be deployed. The new Kontrol release and Forge automatically deploy the libraries and link them to the test contract when executing tests involving linked libraries.
Now, let's set up a Kontrol project and run some proofs!
First, ensure you have the latest Kontrol version and set up a new project using `kontrol init`. Next, we can create a new file under `test/LinkedLibTest.t.sol` with the following code.
```sol
import "forge-std/Test.sol";
library SimpleMath {
function square(uint256 x) public pure returns (uint256) {
return x * x;
}
}
contract LinkedLibTest is Test {
function testSquare(uint256 n) public {
uint256 result = SimpleMath.square(n);
assertEq(result, n * n);
}
}
```
For this example, we will use a library with a single function that computes the square of a number.
Let's have a look at the test to see what happens. First, we run `kontrol build` to prepare the proofs for execution. Next, we run `kontrol prove --mt LinkedLibTest.testSquare --verbose`. We use `--verbose` to get detailed logs, allowing us to quickly identify and troubleshoot issues in real-time. The output may seem overwhelming initially, but that's what this tutorial is here for.
Verbose output of kontrol prove
First, highlighted in blue, you can see the proof's live status. This shows the time elapsed, the proof's name, its status, and a summary of the control flow graph.
You can see the new address where the linked library is deployed, which is highlighted in yellow.
Highlighted in green, you can see when the KCFG is extended with one or multiple nodes. The second message, `Extending current KCFG with the following: 3 non-deterministic branches: 3 --> [4,5,6]`, tells us that the prover discovered three possible states to which the execution of node 3 can lead.
Shortly after seeing these messages, the proof fails with the message shown in the screenshot below.
output of a failing proof
Towards the top of the output, we see the message `5 Failure nods. (4 pending and 1 failing)`. By default, Kontrol uses the fail-fast strategy, stopping the execution when it is confident that a node has reached a failing state. The `4 pending` nodes represent execution paths that Kontrol has not explored yet.
Let's set aside the output for now and look closer at the 3-way non-deterministic branching we noticed during the proof execution. We can view the proof's CFG in the Kontrol Terminal User Interface with `kontrol view-kcfg LinkedLibTest.testSquare`.
Once the interface has loaded, you can select the third node from the left panel. Now, your interface should look like in the screenshot below.
Kontrol_TUI_0
In the bottom right corner, we see that the source map points to the `uint256 result = SimpleMath.square(n);` line.
In addition, we can see that the internal rule, marked with `k:` at which the node was `cut` is `#transferFunds CALLER_ID: Int 728815563385977040452943777879061427756277306518 0`. This is partially displayed in the node information, highlighted in green in the screenshot above. The complete rule is displayed in the configuration loaded in the upper right tab. The `#transferFunds` rule represents an internal step that the EVM semantics apply during a call, explicitly handling the transfer of Ether between accounts. At this point, our intuition tells us that the execution branches when the machine tries to send `0` funds from a symbolic address named `CALLER_ID` to the `728815563385977040452943777879061427756277306518` address. This branching occurs because the prover considers every possible scenario regarding the transfer, even when no funds are involved.
Why is there a symbolic `CALLER_ID`? After all, the `LinkedLibTest` contract calls the `SimpleMath.square(uint256)` function, so the address used should be the contract's address.
Let's rerun the proof with `kontrol prove --mt LinkedLibTest.testSquare --verbose --reinit --break-on-calls`. Here, `--reinit` would ensure that we are re-running the proof from the very beginning, and `--break-on-calls` will add a node to a KCFG every time a call instruction is encountered. We already know the proof is failing, so let's stop the process as soon as the 3-way branch is detected.
Notice that in the proof's live status, the version has increased to 1. We can inspect the new KCFG using `kontrol view-kcfg LinkedLibTest.testSquare --version 1`.
Kontrol_TUI_1
In this version, we notice two additional nodes before the branching occurs. Additionally, we can see that the call to `SimpleMath.square` is made using a `DELEGATECALL` opcode. The use of `DELEGATECALL` is also confirmed by the official documentation, which states:
> ... code is reused using the DELEGATECALL (CALLCODE until Homestead) feature of the EVM. This means that if library functions are called, their code is executed in the context of the calling contract, ...
The symbolic `CALLER_ID` represents the address used by Kontrol to initiate the proof and to invoke the `LinkedLibTest.testSquare` function in the test contract. Since the library function is accessed using `DELEGATECALL`, the same symbolic caller is used. The branching occurs because the prover evaluates all possible scenarios where:
1. `CALLER_ID` matches one of the addresses present in the network state.
2. `CALLER_ID` it is distinct from any of the existing accounts.
So, what can we do?
The three posibilities that the prover found are:
1. `CALLER_ID` is `728815563385977040452943777879061427756277306518`
2. `CALLER_ID` is `856800046449367729202688009541038160569764461356`
3. `CALLER_ID` is not a known address from the network state.
We need to determine if the caller to the library could affect the execution of the call. In our current case, the outcome of the `SimpleMath.square` shouldn't differ depending on the test's initial caller. We can introduce new preconditions for `CALLER_ID` using `vm.assume` before the `SimpleMath.square(uint256)` call.
For example, we can assume that `CALLER_ID` differs from any address in the `` state, leaving a single path for the prover to explore.
```sol
vm.assume(msg.sender != address(728815563385977040452943777879061427756277306518));
vm.assume(msg.sender != address(856800046449367729202688009541038160569764461356));
```
...or we can assume that `CALLER_ID` is equals to a concrete address.
```sol
vm.assume(msg.sender == address(0xc0ffee));
```
Let's go with the first approach, updating the test function to:
```sol
function testSquare(uint256 n) public {
vm.assume(msg.sender != address(728815563385977040452943777879061427756277306518));
vm.assume(msg.sender != address(856800046449367729202688009541038160569764461356));
uint256 result = SimpleMath.square(n);
assertEq(result, n * n);
}
```
> An important note is that, by default, Kontrol automatically adds a few preconditions on the symbolic addresses used: `CALLER_ID`, `ORIGIN_ID`, and any new address generated by the `kevm.freshAddress()` cheat code. These include the symbolic address not being equal to the addresses of the precompiled contracts nor the address of the cheat-code interface, which is `64532647442654720331341006915390590852536243434`. Additional preconditions, like the ones presented above, could be introduced by default in a future Kontrol update.
> You can always see the path constraints of the symbolic variables used in the proof by inspecting the middle tab on the right-hand side of the TUI.
Next, we must rebuild the project with `kontrol build --regen --rekompile`. With this approach, we preserve the previous proof executions but update the project definition we are analyzing. Now let's run the new test with `kontrol prove --mt LinkedLibTest.testSquare --reinit`.
The proof still fails, but we see only one pending node and one failing node. In addition to this, the three-way branching no longer takes place.
However, we need to investigate one more branching to determine why the proof is failing.
We could inspect the KCFG once more to see what the control flow graph looks like now, but that is optional, as the information we need right now is also present in the final output of Kontrol.
Kontrol_TUI_2
The output summarizes the first failure identified while running the proof. We determine if a node represents a failure based on multiple conditions, such as a revert status code or a failed assertion. [You can learn more about the success predicate used in Kontrol here](https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate). It has three components: the failure reason, the path condition, and the model. The output shows that the status code is EVMC\_REVERT, indicating that the execution of the test reverted in at least one branch.
Let's focus on the path condition first. We can see that it is a conjunction of two negated conditions: 1. `#Not ( { VV0_n_114b9705:Int #Equals chop ( VV0_n_114b9705:Int *Int VV0_n_114b9705:Int ) /Word VV0_n_114b9705:Int } )` 2. `#Not ( { VV0_n_114b9705:Int #Equals 0 } )`
The second condition is straightforward; it asserts that the symbolic argument `VV0_n_114b9705` (a K representation of `uint256 n`) is non-zero.
The first condition can be simplified by renaming the variable, resulting in `#Not( n #Equals chop (n *Int n /Word n))`. To break this down further:
* `chop()` is an internal function that ensures its argument is less than `2^256`. Essentially, it functions like a modulus operation (`%`).
* In the K language, operators also include the sort on which they operate. For example, `*Int` represents the product of two unbounded integers, and `/Word` represents the division of two 32 bytes EVM words.
The equation above is equivalent to `n != (n * n / n) mod pow128` which looks more like an overflow check. And that's what it actually is: a compiler-inserted overflow check for the operation inside the `square` function. In other words, the proof will run into an overflow and revert if `n` is neither `0` nor equal `to ((n * n / n) % pow128)`.
The model also demonstrates `VV0_n_114b9705 = pow128` as a counter-example--the value that `n` should take for the failure to occur. In Solidity, to avoid overflow when squaring a number, the result must stay within the `uint256` range, which has a maximum value of `2^256 - 1`. The largest number you can safely square is `n=2^128 - 1` which is the maximum value for a `uint128` (i.e., `type(uint128).max`). This is because `n^2` must be less than `2^256`. The square root of `2^256` is `2^128`, meaning any number greater than or equal to `2^128` would cause an overflow.
Now, we can avoid this branch by adding a new precondition using:
```sol
vm.assume(n <= type(uint128).max);
```
To conclude, we can execute `kontrol build --regen --rekompile` followed by `kontrol prove --mt LinkedLibTest.testSquare --reinit --verbose`, and the proof should now pass.
Successful output of kontrol prove
---
# Agent Instructions
This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com.
## Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.
Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter:
```
GET https://docs.runtimeverification.com/kontrol/guides/kontrol-example/linked-library-example.md?ask=&goal=
```
`ask` is the immediate question: it should be specific, self-contained, and written in natural language.
`goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.
Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.