Unclear semantics for environment variables in the invariant block

[d-xo]

The semantics of invariants that refer to environment variables are currently very unclear. For example, does the following mean "value is always set to the CALLVALUE as it was in the constructor" or "value is always set to the CALLVALUE as it is during each method call":

constructor of C
interface constructor()

creates

    address value := CALLVALUE

invariants

    value == CALLVALUE

As currently implemented the meaning is the second meaning (the value of the env var at the time of the method invocation).

After discussing this offline for a while (as well as in this pr), the consensus seems to be that the best approach is to seperate the invariants block from the constructor definition and to have the environment variables refer to the value of the variable during each method call.

It can however sometimes be useful to be able to refer to the constructor arguments within the invariants block, for example:

constructor of C
interface constructor(uint _totalSupply)

creates

    uint totalSupply := _totalSupply

invariants

    totalSupply = _totalSupply

It would therefore perhaps be nice to allow invariants blocks to refer to constructor arguments in some way. Alternatively we may with to investigate adding some kind of pre / post operators allowing us to reformulate the above totalSupply invariant as:

pre(totalSupply) == post(totalSupply)

[leonardoalt]

I'm not sure how hacky this sounds, but for the second case you could also do

constructor of C
interface constructor(uint _totalSupply)

creates

    uint totalSupply := _totalSupply
    uint initialTotalSupply := _totalSupply

invariants

    totalSupply = initialTotalSupply

Which doesn't really prove the same. We're still missing a mechanism to prove that something doesn't change after deployment.

[d-xo]

I find this pretty usatisfying tbh. It's a pretty common pattern and I think we need a cleaner way to handle stuff like this.

[leonardoalt]

As currently implemented the meaning is the second meaning (the value of the env var at the time of the method invocation).

@xwvvvvwx I'm not sure about this. If that's true, shouldn't https://github.com/ethereum/act/blob/master/tests/invariants/pass/ethEnv.act fail?

[kjekac]

We're still missing a mechanism to prove that something doesn't change after deployment.

Would it be completely crazy to allow all types of expressions as invariants, not only booleans? So for example we could say

[...]
invariants
    totalSupply
[...]

Which is meant in the literal sense; totalSupply does not vary.

[d-xo]

As currently implemented the meaning is the second meaning (the value of the env var at the time of the method invocation).

@xwvvvvwx I'm not sure about this. If that's true, shouldn't https://github.com/ethereum/act/blob/master/tests/invariants/pass/ethEnv.act fail?

Hmmmm, this is a very good point. Currently each invariant is split up into multiple queries (one for the constructor, and one for each case in the behaviours), we declare a fresh constant for each environment variable referenced by the behaviour or the invariant for each of these queries. The ethEnv invariants hold (even if we add some additional behaviours to the spec) because we assert that the invariant holds over the prestate, and we also assert that the poststate of the storage variable is the same as the prestate (as long as there have been no updates to that storage var in the spec of course). As an example we generate two queries for the following spec:

constructor of Env
interface constructor()

creates

    uint value := CALLVALUE

invariants

    value == CALLVALUE

behaviour f of Env
interface f()

storage

    value

This produces the following query for the invariant over the constructor:

;STORAGE:
(declare-const Env_value_post Int)

;CALLDATA:

;ENVIRONMENT:
(declare-const CALLVALUE Int)

;ASSERTIONS:
(assert (not (= Env_value_post CALLVALUE)))
(assert (and (<= 0 CALLVALUE) (<= CALLVALUE 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(assert (= Env_value_post CALLVALUE))

and for the invariant over the behaviour:

;STORAGE:
(declare-const Env_value_pre Int)
(declare-const Env_value_post Int)

;CALLDATA:

;ENVIRONMENT:
(declare-const CALLVALUE Int)

;ASSERTIONS:
(assert (= Env_value_pre CALLVALUE))
(assert (not (= Env_value_post CALLVALUE)))
(assert (and (<= 0 Env_value_pre) (<= Env_value_pre 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(assert (and (<= 0 CALLVALUE) (<= CALLVALUE 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(assert (= Env_value_pre Env_value_post)

I'm actually not even sure what the semantics of environment variable references in the invariant blocks are in this case?

As a final note, adding an ensures block to f with value == CALLVALUE in the above example results in that postcodition being proven false, so we also seem to have some mixed semantics for environment references throughout the specs...

[leonardoalt]

In the second query, why is (assert (= Env_value_pre CALLVALUE)) there?

[leonardoalt]

Oh I guess it's the pre part of the induction.

[d-xo]

Oh I guess it's the pre part of the induction.

yes, exactly

[leonardoalt]

I think the "problem" in the second query is that CALLVALUE is the same in both places that it appears. That gives the semantics that it's the same as construction time.

[leonardoalt]

As a final note, adding an ensures block to f with value == CALLVALUE in the above example results in that postcodition being proven false, so we also seem to have some mixed semantics for environment references throughout the specs...

Can you also paste the check for that case?
My guess: the ensures query is not inductive, right? Which means that CALLVALUE there will be fully fresh, and that makes the check fail.

[d-xo]

Can you also paste the check for that case?

Sure, for the spec:

constructor of Env
interface constructor()

creates

    uint value := CALLVALUE

behaviour f of Env
interface f()

storage

    value

ensures

    value == CALLVALUE

We generate the following querty for the value == CALLVALUE query:

;STORAGE:
(declare-const Env_value_pre Int)
(declare-const Env_value_post Int)

;CALLDATA:

;ENVIRONMENT:
(declare-const CALLVALUE Int)

;ASSERTIONS:
(assert (not (= Env_value_pre CALLVALUE)))
(assert (and (<= 0 Env_value_pre) (<= Env_value_pre 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(assert (and (<= 0 CALLVALUE) (<= CALLVALUE 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(assert (= Env_value_pre Env_value_post))

My guess: the ensures query is not inductive, right? Which means that CALLVALUE there will be fully fresh, and that makes the check fail.

Yes, this is the case

[d-xo]

I think the "problem" in the second query is that CALLVALUE is the same in both places that it appears. That gives the semantics that it's the same as construction time.

You mean we should introduce a CALLVALUE_constructor and CALLVALUE_method or similar?

[leonardoalt]

Only if that's the semantics we want haha.
But yea, right now it is mixed, as you pointed out:

CALLVALUE is the constructor version in constructor and invariant blocks, and is the runtime tx version inside ensures.

[d-xo]

I'm not even sure how to construct the queries so that CALLVALUE would refer to the runtime tx version inside an invariant block... 🤔

[leonardoalt]

I think the safe way is to give it a different name for every block it's part of.

[d-xo]

Isn't that already effectively the case? We construct a totally isolated query for each behaviour...

[leonardoalt]

Ah right, sorry, got confused again.
Actually, now I interpret the invariant query CALLVALUE as the runtime one, and read it as: whatever the CALLVALUE in this tx is, assume pre(value) = that and prove that it doesn't change, which is correct to me.
So I think you were right before and https://github.com/ethereum/act/blob/master/tests/invariants/pass/ethEnv.act is also correct.

I think the encoding of ensures is also correct, but the spec is just too weak and leads to a false positive. To prove that, we need the same as pre condition.

[d-xo]

Taking this spec as an example:

constructor of Env
interface constructor()

creates

    uint value := CALLVALUE

invariants

    value == CALLVALUE

behaviour f of Env
interface f()

returns 1

whatever the CALLVALUE in this tx is, assume pre(value) = that

I think this is actually impossible to implement in EVM. I don't see a way to implement f from the example above so that value would always be equal to the tx level CALLVALUE before the method has even begun execution.

I think that the nature of the inductive query implicitly forces the semantics that environment variable references in the invariant block refer to the value of that variable at constructor time?

[MrChico]

another alternative would be to not allow environment variables in invariant blocks at all. Restricting invariants to be formulas over state variables would make the matter moot. I think having environment variables in ensures blocks; ensures is always associated with a state transition

[d-xo]

another alternative would be to not allow environment variables in invariant blocks at all. Restricting invariants to be formulas over state variables would make the matter moot.

I think I like this, removing all the constructor context from the invariants would also make the smt backend easier to implement.