search

runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
55 stars 9 forks source link

Support signed int `random` cheatcodes #890

Open palinatolmach opened 2 days ago

palinatolmach commented 2 days ago

Follow up to https://github.com/runtimeverification/kontrol/pull/877.

Cheatcodes generating fresh signed ints 

    /// Returns a random `int256` value.
    function randomInt() external view returns (int256);

    /// Returns a random `int256` value of given bits.
    function randomInt(uint256 bits) external view returns (int256);

are challenging to implement because of signed int specifics that cause branching during execution.

We have encountered a relevant (unresolved) issue previously when trying to implement assert functions that involve signed ints too: https://github.com/runtimeverification/kontrol/issues/559.