Formally Verifying Loops: Part 2

This is the second introductory article on formal verification of loops in the Solidity and EVM smart contracts. In the first article, we covered loop unrolling, an automatic reasoning technique that enforces termination by cutting off reachable states, which can lead to missed bugs and vulnerabilities. We also saw that increasing the looping limit is insufficient for unbounded loops. This follow-up article solves this problem by introducing loop invariants to prove properties about unbounded loops!

Be warned that proving loop invariants is generally considered one of the most (if not the most) difficult challenge of formal verification. Unlike loop unrolling, loop invariants are not fully automated and require human input to guide the prover. From the tools presented in the first article, Kontrol is the only prover capable of proving properties about unbounded loops; consequently the other tools won’t reappear in this article. We will cover some of the most advanced features Kontrol has to offer.

In this blog post, you will learn:

• What are loop invariants?
• What is natural induction?
• How to prove loop invariants with pen and paper
• How to spot bytecode level loops
• How to inspect EVM states
• The difference between black-box and glass-box formal verification
• How to prove loop invariants with Kontrol

Recap: Gauss’ Looping Problem

This article continues our attempt to prove the equivalence of the sumToN and triangleNumber functions introduced in the first post. Here is a quick reminder of the code and the specification (the full source code used in this article can be found on GitHub).

function sumToN(uint256 n) public pure returns (uint256) {
    uint256 result = 0;
    uint256 i = 0;
    while (i < n) {
        i = i + 1;
        result = result + i;
    }
    return result;
}

function triangleNumber(uint256 n) public pure returns (uint256) {
    return n * (n + 1) / 2;
}

function check_equivalence(uint256 n) public pure returns (bool) {
    vm.assume(n < 2**128); // prevent overflow
    assert(sumToN(n) == triangleNumber(n));
}

An Inductive Approach

The problem in front of us is proving a property about an unbounded loop in finite time. So, just proving the property for 1,2,3... iterations is hopeless. Let’s take inspiration from Gauss: Gauss summed up all numbers from 1 to 100 without adding one number at a time. Instead, Gauss only calculated the result of the expression 100 * 101 / 2. How can we know that these numbers are the same? A mathematician's solution usually involves natural induction.

In this exercise, we aim to prove Gauss’ childhood observation to remind ourselves of the natural induction principle: a proof technique that can be used for claims of the form $\forall n.P(n)$. It tells us that it is sufficient to prove $P(0)$ (called the base case) and $\forall n .P(n) => P(n+1)$ (called the inductive case). The principle can also be given as an inference rule:

$\frac{P(0) \quad \forall n .P(n) \implies P(n+1)}{\forall n.P(n)}$

Now, let’s apply this principle to Gauss’ formula: $\forall n. \Sigma_{i=0}^{n} i = \frac{n(n+1)}{2}$

First, we must show the base case, where we substitute $n$ for $0$.

$\Sigma_{i=0}^{0} i = 0 = \frac{0(0+1)}{2}$

Clearly, both sides simplify to 0, so the base case holds.

Next, we must show the inductive case:

$\forall n.(\Sigma_{i=0}^{n} i = \frac{n(n+1)}{2}) \implies (\Sigma_{i=0}^{n+1} i = \frac{(n+1)((n+1)+1)}{2})$

The trick here is first to extract the final summand from the series $\Sigma_{i=0}^{n+1} i$:

$\forall n.(\Sigma_{i=0}^{n} i = \frac{n(n+1)}{2}) \implies ((\Sigma_{i=0}^{n} i) + n + 1 = \frac{(n+1)((n+1)+1)}{2})$

Now, we can apply the induction hypothesis by replacing $\Sigma_{i=0}^{n} i$ with $\frac{n(n+1)}{2}$.

$\forall n.(\Sigma_{i=0}^{n} i = \frac{n(n+1)}{2}) \implies (\frac{n(n+1)}{2} + n + 1 = \frac{(n+1)((n+1)+1)}{2})$

Finally, we can show the remaining equality by some simple arithmetic manipulation:

$\forall n.(\Sigma_{i=0}^{n} i = \frac{n(n+1)}{2}) \implies (\frac{(n+1)((n+1)+1)}{2} = \frac{(n+1)((n+1)+1)}{2}) \quad \blacksquare$

This completed our natural induction proof. We now return our focus to formally verifying the equivalence of two Solidity algorithms. The idea stays the same: we develop a closed formula that captures the computational effect of the loop, and then prove the equivalence of the closed formula and the loop inductively.

The Pen and Paper Method

Before we use a mechanized approach to explore loop invariants, let’s do it once with pen and paper.
Forgetting our running example for a minute, we will perform the manual proof on an even simpler codebase.

Using loop invariants in formal proofs is usually a three-step process:

1. Hypothesizing a closed formula
2. Proving the closed formula holds after any number of loop iterations
3. Apply the loop invariant to the original problem

Step 1: Hypothesizing a Closed Formula

This is arguably the most challenging part. Coming up with closed formulas to capture the essence of a loop often requires creative thinking, and that is why it is so hard to automate this process. Our best chance in tackling looping programs is human creativity.

Have a look at the following program:

uint256 result = 0;
uint256 i = 0   
while (i < n) {
    i += 1;
    result += 2;
}
assert(result == 2 * n);

We aim to prove that the result equals two times n after the loop. Looking carefully at the loop, we see that the variable i increases by one and the result by two in each iteration of the loop. In other words, the result is increasing at twice the rate of i, so we come up with the following closed formula: result = 2 * i

Step 2: Prove the Closed Formula Holds After Any Number of Loop Iterations

So far, our loop invariant is just a hypothesis, not a theorem. So, let’s prove it. We do so by induction on the number of loop iterations.

In our base case, we must prove that the invariant holds after 0 loop iterations. We have result = 0 and i = 0, hence result = 2 * i is true.

In the inductive case, we must show that the loop's body preserves the loop invariant:

Assuming that result = 2 * i holds for some fixed i. After incrementing i by one, we have result = 2 * (i - 1); after incrementing the result by two, we have result = 2 * (i - 1) + 2, which simplifies to result = 2 * i.

Concluding, the loop invariant holds before the loop, and every loop iteration preserves the loop invariant. Hence, the loop invariant holds. Notice that it temporarily breaks inside the loop body - but that is okay.

In the literature, this argument is often associated with partial correctness. It is called partial because we have not proven that the loop terminates. After all, it could be an infinite loop. So, let’s prove termination: i increases by 1 in every loop iteration, and n stays constant. Further, the body of the loop terminates in each iteration. Therefore, the loop eventually terminates when i = n. Partial correctness and termination establish total correctness.

Step 3: Applying the Loop Invariant

Our final goal is to show that result = 2 * n. After the loop, we know that i = n and result = 2 * i. A simple substitution of n for i gives us the final result = 2 * n $\blacksquare$

The mechanized method using Kontrol

Let's return our attention to the original running example, and formally verify our claim using Kontrol.

Kontrol helps us to prove and apply invariants. Unfortunately, it cannot hypothesize the closed formulas for us - we must supply it to Kontrol. That doesn’t mean Kontrol trusts us - we will verify the invariant before applying it. Moreover, Kontrol operates on the bytecode level, not the Solidity level, where loops are encoded with JUMPI instructions instead of for or while statements, but the principle stays the same. As a final word of caution, Kontrol cannot read even your prettiest handwriting and therefore expects the loop invariants in a machine-readable format called K. K is special purpose programming language for designing, implementing and verifyging other programing languages. Ever wondered why it's called Kontrol? Now you know.

We’re now getting to the bottom of smart contracts on the implementation and specification language levels. So far, we have only looked at Solidity. Now, we’re turning our attention to EVM bytecode, and K specifications. We will take one step at a time, and break down our process as follows.

1. Hypothesize a closed formula at the Solidity level
2. Translate the formula into an KEVM formula
3. Formally prove the bytecode-level invariant
4. Apply the bytecode-level invariant to the original program.

Step 1: Hypothesizing a Closed Formula

As a reminder, we’re looking for an invariant for this loop:

function sumToN(uint256 n) public pure returns (uint256) {
    uint256 result = 0;
    uint256 i = 0;
    while (i < n) {
        i = i + 1;
        result = result + i;
    }
    return result;
}

Fortunately, Gauss already figured it out for us. The loop invariant we’re looking for is result = i * (i + 1) / 2

Step 2: Translate the formula into an KEVM formula

The first step in our translation from paper to a KEVM-claim is figuring out what the loop looks like at the EVM level. This requires the use of a disassembler (we recommend the one shipped with Foundry).

Simply run the following command:

forge inspect GaussSpec assembly

Here, we manually annotated the bytecode with the corresponding source code, and draw arrows to depict the control flow for our convinience.

Interestingly, the EVM loop inverted the condition of the original while loop. The reason is that the JUMPI instruction jumps to the desired JUMPDEST only if the condition differs from zero.

The next step is understanding how the EVM state changes when we jump out of the loop. Now it would be really beneficial for our purpose to set breakpoints at the entry and exit of the loop. While breakpoints are common for concrete execution, they are rarely found in symbolic execution engines. Fortunately, Kontrol is an exception to this rule. Setting breakpoints on JUMP and JUMPI instructions turns out to be so valuable that there is even a flag for it. Now let’s run Kontrol with breakpoints and in bounded loop unrolling mode (remember, we have not proven the loop invariant yet, so loop unrolling is our best chance).

kontrol prove --match-test 'GaussSpec.check_equivalence' --bmc-depth 3 --break-on-jumpi

After the exploration is complete, we can inspect our (symbolic) execution trace. There are two built-in subcommands for inspection: kontrol view-kcfg launches an interactive terminal user interface (TUI) and kontrol show prints the output non-interactively. In this example, we will use the interactive TUI. If you’re about to use the kcfg viewer for the first time, you will definitely want to review the documentation first.

To launch the TUI, use the following command:

kontrol view-kcfg GaussSpec.check_equivalence

Take your time and play around in the TUI a little.

Let's take a step back for a minute and talk about a unique feature of Kontrol: State inspection is an invaluable asset for all kinds of proofs, useful way beyond just loop invariants. The other tools we discussed earlier, including the Certora Prover, Halmos, and HEVM, treat the EVM as a black box. This means the internal workings are hidden, making it difficult to understand what’s happening when the symbolic execution gets stuck or times out.

Kontrol, on the other hand, treats the EVM as a glass box. With this approach, you can observe how the EVM state evolves, seeing every internal detail and mechanism at work. Imagine watching all the gears turning inside, gaining insight into how each part contributes to the overall process. If you've used formal verification before, you might be familiar with tools getting stuck or timing out unexpectedly. With Kontrol’s glass box approach, you can inspect the exact state where progress halted, identify the stuck gearwheel, and make the necessary adjustments to keep the machine moving forward.

In formal verification, black box tools are typically referred to as fully automated provers, while glass box tools are known as interactive provers. This terminology can be a bit misleading, as it might imply that interactive provers require more manual intervention and are, therefore, less automated. However, this is not the case. Kontrol, for example, excels in automation, often outperforming others in automated reasoning tasks, as demonstrated by its results in the eth-sc-comp benchmark suite. The key distinction lies in Kontrol's ability to combine powerful automation with the transparency of a glass box, offering both insight and efficiency.

Now, let's see how it works in practice. With the help of the kcfg viewer, we can identify that node 31 marks the loop's entry, and node 34 marks its exit after 0 loop iterations. Not visible in the screenshot but equally interesting are nodes 43 and 46, which mark the loop's entry and exit after one iteration. Nodes 55 and 58 mark the entry and exit after two iterations.

We can ask Kontrol to get a summary of the changes between two nodes. Let's ask for the difference between the first entry of the loop and the exit after two iterations. This gives us a good impression of which parts of the EVM state change during the loop. We removed some pieces from the output for brevity. Watch out for the arrow => telling us exactly which pieces change:

$ kontrol show GaussSpec.check_equivalence --node-delta 31,58
State Delta 31 => 58:

<generatedTop>
  <foundry>
    <kevm>
      <k>
        ( JUMPI 898 bool2Word ( VV0_n_114b9705:Int <=Int 0 ) => JUMP 898 )
        ~> #pc [ JUMPI ]
        ~> #execute
        ~> CONTINUATION:K
      </k>
      <ethereum>
        <evm>
          <callState>
            <wordStack>
              ( ( 0 => 2 ) : ( ( 0 => 3 ) : ( 0 : ( VV0_n_114b9705:Int : ( 1816 : ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( VV0_n_114b9705:Int : ( 402 : ( selector ( "check_equivalence(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
            </wordStack>

The beauty of Kontrol is that the summary is actually a rewrite rule telling us exactly how to go from node 31 to 58. The rule tells us what every single bit of the internal EVM state looked like before and after we executed two loop iterations. There is no hidden or private state. Kontrol makes every single bit inspectable: the memory, the word stack, the program counter, the bytecode, accounts storage, etc. We will use this rewrite rule as the foundation for our loop invariant! However, the rule is overly specific. For our loop invariant, this detail can get in the way; after all, most of the state components don’t change and do not constrain the rule in any specific way. Let’s remove all the noise from the rule and only keep the relevant parts:

<k>
   ( JUMPI 898 bool2Word ( N:Int <=Int 0 ) => JUMP 898)
   ~> #pc [ JUMPI ]
   ~> #execute
   ~> _CONTINUATION:K
</k>
<pc> 860 </pc>
<wordStack>
   ( ( 0 => 2 ) : ( ( 0 => 3 ) : ( 0 : ( VV0_n_114b9705:Int : ( 1816 : ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( VV0_n_114b9705:Int : ( 402 : ( selector ( "check_equivalence(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
</wordStack>
<useGas> false </useGas>
<program>  #binRuntime </program>
<jumpDests> #computeValidJumpDests( #binRuntime ) </jumpDests>

Now we have a rule that takes us from the $0^{th}$ loop iteration to the loop exit after two iterations. What we actually need is a rule to take us from the $i^{th}$ iteration to the exit after $n$ iterations. Hence, we must generalize our rule, so it matches at every iteration. It's handy to look at some more node deltas to learn which parts of the state we must generalize. Eventually, we came up with the following hypothesis for our loop invariant:

    claim  <k>
                ( JUMPI 898 bool2Word ( N:Int <=Int I:Int ) => JUMP 898 )
                ~> #pc [ JUMPI ]
                ~> #execute
                ~> _CONTINUATION:K
            </k>
            <program> #binRuntime </program>
            <pc> 860 </pc>
            <wordStack> ( I => N ) : ( RESULT => N *Int ( N +Int 1 ) /Int 2 ) : 0 : N : WS </wordStack>
            <useGas> false </useGas>
            <activeTracing> false </activeTracing>
            <jumpDests> DESTS </jumpDests>
    requires   0 <=Int N andBool N <Int 2 ^Int 128
       andBool 0 <=Int I andBool I <=Int N
       andBool RESULT ==Int I *Int (I +Int 1) /Int 2
       andBool #sizeWordStack(WS) <Int 1013
       andBool DESTS ==K #computeValidJumpDests( #binRuntime )

Let's take a closer look at the claim above.

• <k> JUMPI 898 bool2Word ( N:Int <=Int I ) => JUMP 898 … </k>
  This line claims that when we reach the loop head, we will eventually jump out of the loop (to program counter 898). Hence, it claims termination of our while loop.
• The <program> cell contains the runtime bytecode of our smart contract. The value inside is just a human-readable variable name that maps to the actual bytecode. Nobody wants to type out the entire bytecode.
• The <pc> cell tells us that this claim applies only to the program counter 860 (the offset of the JUMPI instructions).
• The <wordStack> is the most exciting part of the loop invariant. It tells us how the I and RESULT variables are supposed to change during the loop. We know that these variables are allocated on top of the stack and we claim that I will be equal to N, and RESULT will be equal to N *Int ( N +Int 1 ) /Int 2 after the loop.
• The <useGas> cells disables all reasoning about gas. This is Kontrol’s default setting for performance. If we enable gas reasoning, we must develop a closed formula for the total amount of gas consumed by the loop - but we want to to keep it simple for the sake of this article.
• The <jumpDests> is a bitstring marking all valid JUMPDEST locations. It is needed only for technical reasons and is always computed from the bytecode.
• After the requires keyword we list a bunch of constraints about our claim. For example, we require that N is in the range [0, 2^128] and I is in the range [0, N].
• The most noteworthy contraint is RESULT ==Int I *Int (I +Int 1) /Int 2 telling us that our claim only applies if the RESULT variable equals the closed formula.

To summarize, here is a recipe to develop loop invariants with Kontrol.

1. Unroll the loop a couple of times with kontrol prove --bmc-depth
2. Find nodes corresponding to the loop’s entry and exit using kontrol view-kcfg or kontrol show.
3. Use kontrol show --node-delta to obtain a rewrite rule from the entry to the exit node.
4. Generalize the rule to go from the entry of the $i^{th}$ iteration to the loop’s exit.

Step 3: Proving the Invariant

So far, the loop invariant is just a hypothesis; it is still our obligation to prove it before we apply it in a bigger context. This is where Kontrol really shines. Recall the manual effort of the natural induction proof at the beginning of this article, and then again when we used the pen and paper method to prove a simple invariant at the Solidity level. Try to imagine how tedious and nasty these proofs can get on the bytecode level! However, with Kontrol this process is mostly automated.

Let’s make an attempt with kevm prove: We first copy our invariant into a file called lemmas.k and then run the following commands to prove it (again the full source code is available on GitHub).

$ kontrol build --require src/lemmas.k --module-import GaussSpec:GAUSS-CONTRACT --regen --rekompile
$ kevm prove --definition out/kompiled --spec-module LOOP-INVARIANTS src/lemmas.k --break-on-jumpi --max-depth 100
PROOF PASSED: a5f38b84d9889082be3e485d304f57b9a559a94e32726fdd0bb55f3fa7850fa9

Success! The Kontrol prover was smart enough to prove the invariant all by itself!

Notice that we are not always this lucky. Sometimes, the prover can get stuck and demand human intervention to drive the proof forward. Overcoming stuck states is out of the scope for this blog post, but the interested reader can continue reading our official documentation.

Step 4: Applying the Loop Invariant

Kontrol will not apply the loop invariant to our program automatically. After all, throwing random theorems at math problems is rarely a wise idea. How would Kontrol know that this theorem is actually making progress towards the final proof obligation in a bigger context? We must introduce this theorem as a rewrite rule with a higher priority than the default rules, thereby ensuring that when Kontrol reaches our loop it will apply the loop invariant instead of unrolling it one iteration at a time.

This is a simple mechanical process; we just copy the claim and replace the claim keyword with rule. When rebuilding the project, K will complain about non-functional symbols on the left-hand side of the rule, which is an unfortunate technical limitation but simple to resolve by a process we call defunctionalization: We must move all function calls from the left-hand side of our rule into the side-conditions.

    rule  <k>
                ( JUMPI 898 CONDITION => JUMP 898 )
                ~> #pc [ JUMPI ]
                ~> #execute
                ~> _CONTINUATION:K
            </k>
            <program> BYTECODE </program>
            <pc> 860 </pc>
            <wordStack> ( I => N ) : ( RESULT => N *Int ( N +Int 1 ) /Int 2 ) : 0 : N : WS </wordStack>
            <useGas> false </useGas>
            <activeTracing> false </activeTracing>
            <jumpDests> DESTS </jumpDests>
    requires   0 <=Int N andBool N <Int 2 ^Int 128
       andBool 0 <=Int I andBool I <=Int N
       andBool RESULT ==Int I *Int (I +Int 1) /Int 2
       andBool #sizeWordStack(WS) <Int 1013
       andBool DESTS ==K #computeValidJumpDests( #binRuntime )
       andBool CONDITION ==K bool2Word ( N:Int <=Int I )
       andBool BYTECODE ==K #binRuntime
       [priority(40)]

For example, we moved the function call bool2Word ( N:Int <=Int I ) into a side condition CONDITION ==K bool2Word ( N:Int <=Int I ) and replaced all occurrences of the call with CONDITION.

The alert reader might wonder if this rule is still identical to the proven claim after defunctionalizing it. Indeed, we must be very careful not to introduce unsound rules. At this stage, it is best to modify the original claim to match the defunctionalized rule and prove it again. We must ensure that the module containing the claim does not include the module defining the rule, or we would end up with a circular argument!

Finally, let’s prove our original claim with the loop invariant:

$ kontrol build --require src/lemmas.k --module-import GaussSpec:GAUSS-LEMMAS --regen --rekompile
$ kontrol prove --match-test GaussSpec.check_equivalence
🏃 Running Kontrol proofs 🏃 
 Add `--verbose` to `kontrol prove` for more details!
Selected functions: src%GaussSpec.check_equivalence(uint256)
Running setup functions in parallel: 

Running test functions in parallel: src%GaussSpec.check_equivalence(uint256)
  0:00:47 src%GaussSpec.check_equivalence(uint256):0 Finished PASSED: 5 nodes: 0 pending|1 passed|0 failing|0 vacuous|0 refuted|0 stuck
✨ PROOF PASSED ✨ src%GaussSpec.check_equivalence(uint256):0
⏳ Time: 48s ⏳

This brings us to the end of our journey into the depths of proving loop invariants. Let's take a moment to reflect on what we've covered. You've journeyed through some of the most complex territories in formal verification, tackling one of the hardest challenges: proving properties about unbounded loops. Together, we've demystified loop invariants, ventured through natural induction, and explored a mechanized approach with Kontrol. What’s more, we’ve witnessed how Kontrol’s unique glass-box approach allows for unparalleled transparency and control during symbolic execution.

Feel proud of these accomplishments. While formal verification can feel daunting, you've taken steps toward mastering techniques that most developers only touch on the surface. And with Kontrol, you're not just using any prover — you’re utilizing a tool capable of handling even the most challenging aspects of smart contract verification.

So, take a breath and pat yourself on the back. You’re now well on your way to mastering the intricacies of formal verification, and each loop you prove adds another notch to your growing expertise.