Multiple dynamic array parameters

[suhabe]

Hi, I'm having difficulty verifying this program using the following eDSL:

pragma solidity 0.4.24;

contract simple15 {

    function getLength(uint[] xarr, uint[] zarr) pure external returns (uint) {
        return zarr.length;
    }
}

[getLength]
k: (#execute => #halt) ~> _
statusCode: _ => EVMC_SUCCESS
output: _ => #encodeArgs(#uint256(Z_LEN))
log: _
callStack: _
this: #CONTRACT_ID
msg_sender: MSG_SENDER
callData:  #abiCallData("getLength", (#array(#uint256(_), X_LEN, _), #array(#uint256(_), Z_LEN, _)))
callValue: 0
wordStack: .WordStack => _
localMem: .Map => _
pc: 0 => _
gas: #gas(INITGAS, 0, 0) => _
memoryUsed: 0 => _
refund: _
coinbase: _ => _
+requires:  andBool #range(0 <= CD < 1024)
            andBool #rangeAddress(MSG_SENDER)
            andBool #rangeUInt(256, X_LEN)
            andBool #rangeUInt(256, Z_LEN)

Interestingly, if I modify the code to return xarr.length instead of zarr.length (i.e. the length of the first dynamic array parameter instead of the second dynamic array parameter), the spec actually passes successfully (once the output cell is updated to output: _ => #encodeArgs(#uint256(X_LEN)). This seems to suggest that something may be missing from the spec or rewrite rules to handle extracting the length of a dynamic array parameter which is preceded by another dynamically-size array. I looked at the edsl.k file, and I couldn't figure out how the following rewrite rule would work:

rule #enc(#array(_, N, DATA)) => #enc(#uint256(N)) ++ #encodeArgs(DATA)

especially when compared to the similar rule for #enc(#bytes(WS)) which seems to "bottom-out" rather than recursively encoding WS via #encodeArgs:

rule #enc(#bytes(WS)) => #encBytes(#sizeWordStack(WS), WS)
rule #encBytes(N, WS) => #enc(#uint256(N)) ++ WS ++ #buf(#ceil32(N) -Int N, 0) 

Is there something missing from my spec?

[suhabe]

Also, it seems like eDSL doesn't currently handle statically-sized arrays as function arguments. Is that correct?