Loop invariants

[leonardoalt]

@wilcoxjay and I talked today, and he suggested the idea of also expressing loop invariants in the spec.

The challenge there is that loops don't have an interface, so how can we talk about them inside a function in the spec such that they represent loop behavior in different levels, eg, Solidity / bytecode?

One use case is, for example, a tool that runs on the Solidity level inferring loop invariants and trying to communicate these properties to tools that target bytecode.

An idea would be to have the basic spec level of abstraction similar to the ABI, and have extensions to that, such as spec that can also reason about bytecode.

[MrChico]

Here's how we wrote a loop invariant in the act flavor for rpow:

behaviour rpow-loop of Jug
lemma

//  0a3a => 0a7e
pc

    2618 => 2686

for all

    Half   : uint256
    Z      : uint256
    Base   : uint256
    N      : uint256
    X      : uint256

stack

    _ : _ : Half : _ : Z : Base : N : X : WS => Half : _ : #rpow(Z, X, N, Base) : Base : 0 : _ : WS

gas

    194 + ((num0(N) * 172) + (num1(N) * 287))

if

    Half == Base / 2
    0 <= #rpow(Z, X, N, Base)
    #rpow(Z, X, N, Base) * Base < pow256
    N =/= 0
    Base =/= 0
    #sizeWordStack(WS) <= 1000
    num0(N) >= 0
    num1(N) >= 0

which is unsatisfactory on a number of levels.

• Referring to the pc value means that this must be changed every time the bytecode is updated. How can we extract this information is a better way? Some sort of annotations in the source code?

• Referring to variables by their stack location forces such claims to be on the EVM level. Again, maybe annotations can help here

• The strategy around dealing with gas might be avoided completely if all proving engines have a "gas free" mode, where this doesn't matter at all. There are some abstractions in K already towards this goal.

Now, I think that this syntax is different from what you might like @leonardoalt . Do you have an alternative suggestion?