Missing range constraints for TIMESTAMP_CELL symbolic variable

[lucasmt]

Kontrol uses the symbolic variable TIMESTAMP_CELL to represent the value block.timestamp in Solidity, but it doesn't introduce range constraints for this variable (0 <=Int TIMESTAMP_CELL and TIMESTAMP_CELL <Int pow256). This means, for example, that the following test will fail in Kontrol:

function testTimestamp() public {
    assertLe(block.timestamp, type(uint256).max);
}

It will also prevent expressions that use TIMESTAMP_CELL from simplifying. For example, #asWord ( #range ( #padToWidth ( 32 , #asByteStack ( TIMESTAMP_CELL:Int ) ) , 0 , 32 ) ) should simplify to just TIMESTAMP_CELL, but only if its range is constrained.

[lucasmt]

I'd be happy to submit a PR fixing this, but I don't actually know where these constraints get added

[anvacaru]

Constraints like this are added in evm-semantics, in KEVM.add_invariant method.

[anvacaru]

Closing this as it is a duplicate of runtimeverification/evm-semantics#2143.