Ability to write properties across the Smart Contracts and Functions

[dearzubi]

VerX provides the way to write properties across the smart contracts and functions. For example, if a variable change in contract A happens then there must be some change in contract B. This sort of stuff. Better understandable through their documentation. VerX Multi contract Invariants

Can we do something like this with Scribble?

[cd1m0]

Good question. VerX expresses multi-contract invariants using temporal logic, which is a fairly expressive logic.

In scribble we can do something more limited - you can write an invariant over one contract, that holds at all observable points on that contract. If you want to access the state of another contract, you can only access whatever is returned by existing view functions on that contract. Also you don't have access to the 'temporal' modalities, that allow you to specify orders on events.

So in the VerX documentation they have the following example:

// escrow is in state success only if the amount of raised
// funds exceed the goal of the crowdsale
property success_implies_goal_is_reached {
  always((Escrow.state == 1) ==> (Crowdsale.goal <= Crowdsale.raised));
}

If the Escrow.state variable is public, and you have a reference to Escrow in the Crowdsale contract, you can express a slightly weaker version of this in Scribble as follows:

contract Escrow {
    public uint8 state;
    ...
}

/// invariant escrow.state() == 1 ==> goal <= raised;
contract Crowdsale {
    Escrow escrow;
    uint goal;
    uint raised;
}

This property is slightly weaker than the original temporal invariant in VerX, as the condition is not checked immediately when state is set by 1, but instead its checked the first time that we call into Crowdsale, after setting Escrow.state to 1.

I hope this answers your question.

[dearzubi]

Thanks for the elaboration. Is there any possibility that in future we can do it in Scribble exactly the way VerX allows?

[cd1m0]

We have been discussing adding some form of temporal logic to Scribble which should get you close. Whether the semantics will be exactly the semantics of VerX is still unknown. The subtleties arise when you decide at what "ticks" in time the properties are checked. So short answer - there is a strong possibility you can get close to the VerX semantics, but there may be some multi-contract properties that are not easy to express in the exact same way.

[cd1m0]

@dearzubi If this answers your question, may I close this issue?