RFC: rounding errors

[d-xo]

A little writeup of a proposed syntax for describing properties related to rounding error.

rendered

[MrChico]

Nice write up! I agree that this is a very nice thing to be able to express.

The annotations look a little ambiguous in their current location (how do we know that it refers to amt1 here?).
An alternative would be to be a bit more explicit (and flexible) about what the exactness is referring to, by doing explicit conversions to real numbers, maybe along the lines of something like this:

where
    amt0 := (token0.balanceOf[ACCT_ID] * shares) / totalSupply
    amt1 := (token1.balanceOf[ACCT_ID] * shares) / totalSupply

ensures
   amt0 <= toReal(token0.balanceOf[ACCT_ID]) * toReal(shares) / toReal(totalSupply)
   amt1 >= toReal(token1.balanceOf[ACCT_ID]) * toReal(shares) / toReal(totalSupply)

[d-xo]

hmmmm yes, good point re: ambiguity. In my head the annotation refered to the whole expresison on the RHS of the storage rewrite, not just amt1 or amt0. I think that I agree that being more explicit would be benficial.

I'm not sure about using ensures, would we be able to provide a toReal for the K and hevm backends? I think it might be confusing if only some of the claims in the postconditions are verified in those backends? We also lose the claims about the bounds of the error in your example.

I also think it would be harder to warn on expressions that do not have rounding annotations if we move them away from the storage writes and into the ensures.

Perhaps a dedicated rounding block at the behaviour level?

where
    amt0 := (token0.balanceOf[ACCT_ID] * shares) / totalSupply
    amt1 := (token1.balanceOf[ACCT_ID] * shares) / totalSupply

rounding
    amt0 <= exact(amt0), bound 1
    amt1 >= exact(amt1), bound 1

[d-xo]

turned this into an issue at #112.