FV (WIP do not merge)

[d-xo]

Some notes on current FV progress. Mostly here for handover reasons. The easy stuff is all done, but progress on plot / drop/ exec is very slow.

Code Changes

The following changes have been made to ease FV:

• Switch from DSAuth to rely/deny (removes an external call)
• Replace mapping (bytes32 => bool) with mapping(bytes32 => int) (avoid dealing with solidity bool masking)
• Use bounded DSNote from dss (K cannot deal with unbounded msg.data size in the main DSNote)
• Make plot/drop/exec external and inline the hash helper (solidity uses a for loop when copying bytes memory types from calldata, but can directly use CALLDATACOPY for bytes calldata types)

I am also considering removing the proxy as part of the work on exec. It prevents malicious plans from plotting new undelayed plans, but since plans can modify auth on the pause anyway, I'm not sure it actually very useful. It also feels a little too baroque now that I come back to look at it.

Dynamic Data

K has a really hard time with the dynamic data in the pause. There are two problematic areas that I have encountered so far:

1. Computing the size of the call data. This requires a calculation that has symbolic inputs to chop and ceil32, both of which are concrete. I was able to figure out some (pretty ugly) custom lemmas that let K simplify these expressions.

2. Computing memory expansion costs for CALLDATACOPY. This requires calculations with symbolic inputs to #memoryUsageUpdate, which is [concrete]. I was unable to find a set of lemmas that would help K simplify these expressions. These expressions are more complex than those in the size calculations and they simplify to something of the form X * VGas < A * size(fax)^2 + B * size(fax) + C) and so I cannot see an easy way to help K simplify these expressions when both VGas and fax are symbolic.

For this reason my current approach is to first verify the pause with a fixed size for fax and CD, which although obviously not exhaustive, still explores significantly more state space than the unit tests. This has so far not been successful either.

[livnev]

For this reason my current approach is to first verify the pause with a fixed size for fax and CD, which although obviously not exhaustive, still explores significantly more state space than the unit tests. This has so far not been successful either.

I think this is a good way to start 👍

[d-xo]

So I fixed the calldata size to 64 in an if block. K still got stuck on the same calldatasize checking lemmas as before, and I spent quite a long time stuck trying to make it through.

If I readd the same (messy) lemmas that helped K out when the calldata size was bounded, I end up at some new mess of a gas term that I do not understand somewhere a little further along.

I've pretty much hit a brick wall here.