[WIP] Calldata generation for bytes, bytes[] parameters

[palinatolmach]

WIP.
Depends on the KEVM PR: runtimeverification/evm-semantics#2265.
Alternative to the manual approach taken in #223 (where assumptions for a specific OP proofs are being added manually).

To assist automated generation of calldata for functions with bytes, bytes[] parameters, as well as structs with such elements, this PR adds the following to solc_to_k:

• parsing of NatSpec comments on the following types:

    /// @custom:length _withdrawalProof: 10,
    /// @custom:element-length _withdrawalProof: 600,
    /// @custom:length amount: 20,

where @custom:length is used to specify the length (10) of array bytes[] _withdrawalProof, and @custom:element-length is used to specify the length of bytes elements in _withdrawalProof (600). Please use , as a delimiter between comments — otherwise, two comments starting from /// @custom:length will get merged into /// @custom:length _withdrawalProof: 10amount: 20.
These values are being added to Input as length and element_length fields, which are then used during syntactic sugar rules generation for a respective function.

To make NatSpec comments accessible in compilation artifacts, forge build command is adjusted to be called with --extra-output devdoc. These comments are function-level, so they're initially parsed as part of Method instantiation.

This functionality can be tested using the CallDataTest contract provided in the kontrol-calldata repository:

git clone https://github.com/runtimeverification/kontrol-calldata.git && git checkout calldata-gen
kontrol build --foundry-project-root ../kontrol-calldata  --require ../kontrol-calldata/lemmas.k --module-import CallDataTest:PAUSABILITY-LEMMAS
kontrol prove --foundry-project-root ../kontrol-calldata  --match-test test_array_encoding

• the information about bytes[] a array lengths and the length of its elements is then used to generate the rule used to generate calldata; this rule, for a bytes[] a array w/size 10 adds 10 elements (V0_V0_a_0: bytes, V0_V0_a_1: bytes, ...) to LHS (function signature) and RHS (#abiCallData ( ... )) expression, e.g., for

    /// @custom:length _withdrawalProof: 10,
    /// @custom:element-length _withdrawalProof: 600,
    function test_array_encoding(
        bytes memory data,
        uint256 _l2OutputIndex,
        bytes[] calldata _withdrawalProof
    )    

the rule looks as follows

    rule  ( S2KtestZModCallDataTest . S2KtestZUndarrayZUndencoding ( V0_data : bytes , V1__l2OutputIndex : uint256 , V2_V2__withdrawalProof_0 : bytes , V2_V2__withdrawalProof_1 : bytes , V2_V2__withdrawalProof_2 : bytes , V2_V2__withdrawalProof_3 : bytes , V2_V2__withdrawalProof_4 : bytes , V2_V2__withdrawalProof_5 : bytes , V2_V2__withdrawalProof_6 : bytes , V2_V2__withdrawalProof_7 : bytes , V2_V2__withdrawalProof_8 : bytes , V2_V2__withdrawalProof_9 : bytes ) => #abiCallData ( "test_array_encoding" , #bytes ( V0_data ) , #uint256 ( V1__l2OutputIndex ) , #bytesArray ( 10 , 600 , #bytes ( V2_V2__withdrawalProof_0 ) , #bytes ( V2_V2__withdrawalProof_1 ) , #bytes ( V2_V2__withdrawalProof_2 ) , #bytes ( V2_V2__withdrawalProof_3 ) , #bytes ( V2_V2__withdrawalProof_4 ) , #bytes ( V2_V2__withdrawalProof_5 ) , #bytes ( V2_V2__withdrawalProof_6 ) , #bytes ( V2_V2__withdrawalProof_7 ) , #bytes ( V2_V2__withdrawalProof_8 ) , #bytes ( V2_V2__withdrawalProof_9 ) , .TypedArgs ) , .TypedArgs ) )
       ensures ( **#rangeUInt ( 64 , lengthBytes ( V0_data ) **)
       andBool ( #rangeUInt ( 256 , V1__l2OutputIndex )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_0 ) )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_1 ) )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_2 ) )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_3 ) )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_4 ) )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_5 ) )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_6 ) )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_7 ) )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_8 ) )
       andBool ( #rangeUInt ( 64 , lengthBytes ( V2_V2__withdrawalProof_9 ) )
               ))))))))))))

• this PR also changes range predicate for bytes length from uint128 to uint64, reflecting the check inserted by the compiler.

Remaining work: this PR does not include support for other array types, e.g., uint256[] or tuple[], as well as nested arrays.

[anvacaru]

I've migrated the changes from this pr in #320 and #321 and created a new issue to add the [preserves-definednes] tag to missing productions in cheatcodes.md. If I missed anything, let's open an issue for it. Meanwhile I'm closing this.