SMTChecker: Contract invariants support

[leonardoalt]

Abstract

Currently the SMTChecker does not reason about contract global invariants.

contract C
{
    uint a;
    function f1() public { a = 1; }
    function f2() public { a = 2; }
    function f1(uint x) public 
        require(x < 10);
        a = x;
    }
}

In the example above, a >= 0 && a < 10 is an invariant that might be useful to prove properties of other functions in the contract.

Specification

Ideally we'd have a way to provide global invariants such that, for each invariant I:

• assert(I) is added in the end of the constructor
• require(I) is added in the beginning of every non-view function
• assert(I) is added in the end of every non-view function

If the SMTChecker proves all assertions, the invariant is inductive and safe.

Previous example updated with new suggested syntax:

contract C
{
    uint a;
    invariant { a >= 0 && a < 10 }
    function f1() public { a = 1; }
    function f2() public { a = 2; }
    function f1(uint x) public 
        require(x < 10);
        a = x;
    }
}

[chriseth]

I think if the content of the invariant is an expression, then it should not have {-}.

Also, the invariant should be used with all external (and perhaps also internal) function calls.

[axic]

This kind of calls for static_assert-esque feature :)

[chriseth]

It might be useful to name invariants and then allow to annotate function that are expected to violate certain invariants: violates invariantName

For example, a mint function is fine to violated the constant-ness of the sum of balances.

On the other hand, something like ghost variables might be a better way to achieve the same goal.

[chriseth]

Another way to implement this would be a list of functions that violate an invariant to be specified with the invariant (instead of with the function).

[ekpyron]

I would still think about how this relates to modifier areas and pre- and postconditions defined in modifiers.
Having global invariants can be achieved with just putting everything in one modifier area; excluding some functions would just mean defining them outside that modifier area, etc.

As for overlapping sets of invariants - would defining invariants while excluding some functions really be better than modifier areas in that case?

[lojikil]

@ekpyron I'm with you; may as well add full Hoare logic à la pre- and post-conditions. You could also go with refinement types, but that may be a bit further than the current direction may wish to go.

[leonardoalt]

This was brought up again in #8433.

My current proposal including expressiveness/syntax/code generation is:

contract C {
    uint x;
    property { x < 2 };
    function f() public { if (x == 0) x = 1; }
    function g() public { if (x == 1) x = 0; }
}

This would add

• assert(x < 2) in the end of the constructor
• require(x < 2) in the beginning of f and g
• assert(x < 2) in the end of f and g.
  (all the functions that can be called externally).

As @MicahZoltu pointed out, the code generation above should be done only if the function was called externally.

The expressions inside property must be side effect free.
If the property doesn't hold over all public functions, it can be further specified by
property { x < 2 } over f, h;

[leonardoalt]

Any other syntax suggestions?

[dddejan]

It would be nice if the property expressions language is extensible in some way to support tool-specific language. I'm not sure how easily this is done. This is one of the reasons why at the moment in solc-verify we put all the specs in the comments.

For example something like:

contract C {
    int[] a;
    property (uint i) { forall(i, !(i < a.length) || a[i] < 100) };
    function add(int x) {
        require(x < 100);
        a.push(x);
    }
}

Above declares a new variables i to ease parsing, and has a new tool-specific function forall.

Edit: maybe one could specify the language of the properties somehow with "magic" functions that support any number of arbitrary arguments (this is on the tool to interpret), e.g.:

pragma add-property-predicate forall;
pragma add-property-function sum_int int;

contract C {
    int[] a;

    property boundedLength() dynamic { a.length <= 100 }
    property boundedElements(uint i) static { forall(i, !(i < a.length) || a[i] < 100) };
    property boundedSum(uint i) static { sum_int(i, a[i]) > -100 }    

    function add(int x) {
        require(x >= -1 && x < 100 && a.length < 100);
        a.push(x);
    }
    function remove(uint i) {
        require(a.length > 0 && i < a.length);
        a[i] = a[a.length-1];
        a.pop();
    } 
}

Edit: added modifiers and more functionality that shows some dynamic checks unnecessary.

[leonardoalt]

I think this could be useful, but considering this is supposed to generate bytecode as well I find it rather dangerous, since these custom properties wouldn't generate code (but they look the same as the ones that would).

[leonardoalt]

@dddejan what other operators would you say are important? Maybe we could have a spec language inside Solidity that doesn't generate code but accepts that.

[dddejan]

Yes, I didn't realize that you're doing code generation. Examples we have now are sums over collections and and equality over complex datatypes (e.g., comparing two arrays/structs). We plan to add some quantification soon.

It's really impossible to say what's useful. It would be great if you could have some kind of modifier on properties (dynamic/static) to distinguish which ones generate code.

[leonardoalt]

Yea this dynamic/static separation is something I also really want

[axic]

#2918 could replace this for number types at least.

[leonardoalt]

With Solidity's recent custom Natspec tags, doing something like the following examples annotates the AST node of the contract with the given invariant similarly to how the other Natspec tags apply to contracts.

/// @custom:formal invariants {x == 0}
contract D {
	uint x;
}

$ solc a.sol --devdoc
======= a.sol:D =======
Developer Documentation
{
  "custom:formal": "invariants {x == 0}",
  "kind": "dev",
  "methods": {},
  "version": 1
}

Since this is/could be used by various tools without changing the language itself, maybe this is an easier and more practical way to go.