comptime: symbolic free memory pointer allowing to eval keccak256 over memory

[mbenke]

Let the partial evaluator run memory operations and keccak256 at compile time, so that hashing idioms such as the EIP-712 domain separator fold to a literal.

Memory ops (mload/mstore/mstore8/keccak256) are gated on comptime mode: outside it, hashing memory the compiler cannot see would be unsound, so the block is abandoned. Memory is byte-level and sparse; an unwritten byte reads as unknown rather than zero, since runtime code may have written it first.

The free memory pointer's value is unknown at compile time, so it is tracked symbolically as YulVal = Concrete | FreeOffset: mload(0x40) yields FreeOffset 0, add/sub shift the offset, and every other operation on it fails. That address has no MAST form, so evaluating an expression now yields both what to emit and what the evaluator additionally knows (EvalResult); emission goes through the former, which makes leaking a symbolic address into the program impossible by construction.

Absolute and free-relative addresses may alias at run time, so one evaluation may use only one region, and any write disturbing the pointer slot aborts the evaluation.

Finally, a call to a '-> comptime' function whose arguments are all known must have folded by the time the verifier runs; if it survived, the annotation's promise was not kept and the call site is reported.

Assisted-By: Claude Opus 5 (claude-opus-5)