Mismtach between bitsInWords and bytesInWords

[SebastienGllmt]

From https://github.com/runtimeverification/iele-semantics/blob/master/data.md you get the following:

• bitsInWords converts a number of bits to a number of words.
• bytesInWords converts a number of bytes to a number of words.

    syntax Int ::= bitsInWords ( Int ) [function]
 // ---------------------------------------------
    rule bitsInWords(I) => I up/Int 256

    syntax Int ::= bytesInWords ( Int ) [function]
 // ----------------------------------------------
    rule bytesInWords(I) => I up/Int 8

However the two definitions cannot both be true and also the 'bitsInWords' definition does not match the definition of Sha3 in https://github.com/runtimeverification/iele-semantics/blob/master/iele-gas.md

// Result size of SHA3 is 256 bits, i.e., 4 words.

rule #memory [ REG = sha3 _ ] => #registerDelta(REG, bitsInWords(256))

Changing this to up/Int 64 causes some of the tests/iele/ERC20/transfer_Caller-Zero.iele.json.test test to fail.

[zuzunker]

Also iele-gas.md defines "Operations whose result should fit into a word" and "Operations whose result should fit into 256 bits", implying that those are different sizes.

[dwightguth]

This is definitely a good catch. bitsInWords is supposed to divide by 64...

Since this affects the output of a transaction I won't have a fix right away, but this should be batched into the upcoming set of changes to IELE's gas model.