dxo

> 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...

> 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...

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

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

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 ```...

> 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...

modules and imports at the haskell level or for the act language itself?

ah, yes that is quite of an interesting rabbit hole...

Did you have some ideas in this area? I've been having some vague thoughts around being able to export only invariants, and pre/post conditions from contracts for use in proving...

After discussing with @msooseth we came up with a more restricted case checking algorithm that should be decidable and very fast (even cases with 1000's of variables should be checkable...