search

runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
48 stars 5 forks source link

Support ranges for dynamic types' lengths #385

Open palinatolmach opened 7 months ago

palinatolmach commented 7 months ago

Related: https://github.com/runtimeverification/kontrol/issues/353

Dynamic array support implemented in https://github.com/runtimeverification/kontrol/pull/321 relies on the assumption that the array and its elements' length is fixed to a particular concrete value, e.g., 

    /// @custom:length _withdrawalProof: 10,
    /// @custom:length _withdrawalProof[]: 600,
    function test_finalizeWithdrawalTransaction_paused(
        bytes[] calldata _withdrawalProof
    )

The feedback we received from the Optimism team, however, suggests that it'd be better if allowed specification of a range (min/max bounds) instead of a fixed value for bytes (and array) length. For example, in this test, the min proof length is 5 and the max is 8. The element lengths range from 32 to 532 bytes, so using 32 and 600 as the bounds would be better.

yale-vinson commented 6 months ago

@palinatolmach Can we move this one to Next Up? I think it makes sense to address this one sooner rather than later.