sum from mapping of structs?

[naps62]

Is it possible to achieve something like this?

contract Vault {
  struct Account {
    uint256 id;
    uint256 shares;
  }

  mapping(address => Account) accounts;
  uint256 totalShares;

  /// #invariant unchecked_sum(accounts.shares) == totalShares;
  function deposit() {
    /// ...
  }
}

[GNSPS]

Are you using Scribble for any smart contracts going into production, Miguel? I'd love to talk about it and maybe extend an offer for some free fuzzing campaigns with https://fuzzing.diligence.tools

I can also swing by Subvisual's office when I'm back in Portugal so we can discuss Scribble/Fuzzing usage in greater detail! 😊

[naps62]

@GNSPS thanks for the offer (I will hold you up to that 😄 )

It's both for a production project, and to potentially use in yAcademy which just started
I had scribble on my todo list for a few months now, and decided to give it a try these days to see if it could be a better fit than echidna

[cd1m0]

@naps62 unfortunately that can't be expressed with scribble at the moment. To say that, you need a map function, that maps each struct Account in the accounts map, into its shares uint256 variable, and then computes the sum over the mapped values. We are discussing several ideas on how to extend scribble to support this. One possible idea is to add arbitrary "ghost state" that you can compute and maintain. Another is to consider limited map functionality. Whenever we begin to experiment with something I will ping you

[naps62]

@cd1m0 thanks. I'd appreciate it yes

I'm sure there are several ways to achieve this.

The idea of ghost state sounds very interesting for many other reasons as well, but it also feels like out of scope for scribble.
I've often felt the need to instrument my code with additional data and/or logic that wouldn't go into production, but I don't know of any confortable tool to do that in solidity right now. Feels like it would be a tool on its own (useful for all kinds of purposes), and not just a scribble features

[nettrino]

Similar question I had when playing with the tool is whether it is possible to compute a sum by combining let and forall and then specifing an invariant on top of that (e.g., if_succeeds, sum over forall <= some value. My understanding is that this is not doable as of today unless we break down the function into smaller functions and apply separate statements there?

[cd1m0]

@nettrino you're correct - it is not currently possible. However could you post a sample of what you would like supported? If there is enough interest in this feature, and if we can figure out a way to implement it thats friendly to underlying tools (fuzzers/sym. exec engines/verifiers for example) then we can consider it.