sum/usum Example
#154
sum/usum Example
#154
Conversation
| * `sum` - Used to sum elements with signed values (e.g. int). | ||
| * `usum` - Used to sum elements with unsigned values (e.g. uint) including `mathint`. |
There was a problem hiding this comment.
one can use sum also on unsigned values. usum adds some more assumptions that promise that the sum is always greater than its parts, but it might be harder on the prover so if that property isn't needed one may prefer to use the normal sum also on unsigned.
One more thing is that when using usum on mathint then we add internal assertions that all writes to the ghost are indeed non-negative.
There was a problem hiding this comment.
Thanks I noted that.
| Restrictions: | ||
| * We can only sum ghosts, not e.g. direct storage access of mappings. | ||
| * The summed variables must be used, and can only be used as indices to the ghost (so e.g. sum uint u. myGhost[a][u*2] won't work). | ||
| * We only sum values that were written to the ghost, we don't know what there is in the other slots. |
There was a problem hiding this comment.
This is true for sum, for usum it's more nuanced since we also look at reads to promise the "sum is greater than its parts" property
There was a problem hiding this comment.
this is really really hard. I would redo this and have:
- very simple solidity case that there is a total field and then spec that has the mirror ghost and verify that the sum is total
- same spec with persistent, should fail to verify
- the nested ghost spec in a different file with the example of quantifiers
| @@ -0,0 +1,7 @@ | |||
| { | |||
| files: ["ghostSums.sol:C"], | |||
| process: "emv", | |||
There was a problem hiding this comment.
| process: "emv", | |
| files: ["ghostSums.sol:C"], | ||
| process: "emv", | ||
| rule_sanity: "basic", | ||
| solc: "solc8.24", |
There was a problem hiding this comment.
| solc: "solc8.24", | |
| mapping(address => int) _n; | ||
| bool internal _b; | ||
|
|
||
| function ghostUpdater(address a, int n) external { |
There was a problem hiding this comment.
| function ghostUpdater(address a, int n) external { | |
| function storageUpdater(address a, int n) external { |
| _n[a] = n; | ||
| } | ||
|
|
||
| function ghostUpdaterReverts(address a, int n) external { |
There was a problem hiding this comment.
| function ghostUpdaterReverts(address a, int n) external { | |
| function storageUpdaterReverts(address a, int n) external { |
| function ghostUpdaterReverts(address a, int n) external envfree; | ||
| } | ||
|
|
||
| ghost mapping(address => int) ghostAddrToInt256; |
There was a problem hiding this comment.
this is a mirror ghost, right? lets keep it simple
|
|
||
| ghost mapping(address => int) ghostAddrToInt256; | ||
| ghost mapping(uint8 => mapping(bytes4 => mapping(mathint => mapping(address => int8)))) ghostNestedMapping; | ||
| persistent ghost mapping(address => int) persistentGhostAddrToInt256; |
There was a problem hiding this comment.
persistent behave differently so lets have a copy of the spec with persistent mirror and show the difference
| @@ -0,0 +1,15 @@ | |||
| contract C { | |||
| mapping(address => int) _n; | |||
| bool internal _b; | |||
| bool internal _b; | ||
|
|
||
| function ghostUpdater(address a, int n) external { | ||
| _n[a] = n; |
|
|
||
| function ghostUpdaterReverts(address a, int n) external { | ||
| _n[a] = n; | ||
| if (!_b) { |
| // Verify we "hook" onto reads of the ghost also when in an assigning command _to_ that ghost. | ||
| ghostAddrToInt256[addr] = require_int256(ghostAddrToInt256[addr] * 2); | ||
| assert (sum address a. ghostAddrToInt256[a]) == initialSum + (newVal * 2) - oldVal; | ||
| satisfy true; // to force creation of calltrace |
There was a problem hiding this comment.
just show that total is the sum of mirrorghost
|
I ended up doing a much much simpler solution in a new PR. Closing this one. |
No description provided.