act icon indicating copy to clipboard operation
act copied to clipboard

Important fixes in hevm equivalence

Open zoep opened this issue 1 year ago • 0 comments

Proper handling of initial state so that it is not threaded

Previously the state was treaded between rewrites, which is not the correct semantics of Act. Now the left hand side of all rewrites uses the initial state, as opposed to the intermediate.

Keep track of caller so that it can be used when the

The ActM monad now keeps track of the symbolic address of the caller, so that the CALLER variable is implemented correctly.

Implementation of This context variable

This is no longer a TODO.

AMM example in hevm test

This currently times out (under investigation), but trying to fix this example lead to the above fixes.

zoep avatar Feb 05 '24 16:02 zoep