Hashed Storage Locations

requires "evm.md"
requires "buf.md"

module HASHED-LOCATIONS
    imports EVM
    imports BUF

Hashed Location for Storage

The storage accommodates permanent data such as the balances map. A map is laid out in the storage where the map entries are scattered over the entire storage space using the (256-bit) hash of each key to determine the location. The detailed mechanism of calculating the location varies by compilers. In Vyper, for example, map[key1][key2] is stored at the location:

  hash(hash(key1 ++ slot(map)) ++ key2)

where slot(map) is the position index of map in the program, and ++ is byte-array concatenation, while in Solidity, it is stored at:

  hash(key2 ++ hash(key1 ++ slot(map)))

The eDSL provides #hashedLocation that allows to uniformly specify the locations in a form parameterized by the underlying compilers. For maps, the location of map[key1][key2] can be specified as follows, where {COMPILER} is a place-holder to be replaced by the name of the compiler. Note that the keys are separated by the white spaces instead of commas.

  #hashedLocation({COMPILER}, slot(map), key1 key2)

This notation makes the specification independent of the underlying compilers, enabling it to be reused for differently compiled programs.

For dynamically sized arrays in Solidity, and both statically and dynamically sized arrays in Vyper, the length of the array is stored at:

  hash(slot(array))

and the element at index i is stored at:

  hash(slot(array)) + i

More information about how storage locations are defined in Solidity can be found here.

Specifically, #hashedLocation is defined as follows, capturing the storage layout schemes of Solidity and Vyper.

    syntax IntList ::= List{Int, ""}                             [klabel(intList)]
    syntax Int     ::= #hashedLocation( String , Int , IntList ) [function]
 // -----------------------------------------------------------------------
    rule #hashedLocation(_LANG, BASE, .IntList) => BASE

    rule #hashedLocation("Vyper",    BASE, OFFSET OFFSETS) => #hashedLocation("Vyper",    keccakIntList(BASE OFFSET),       OFFSETS)
    rule #hashedLocation("Solidity", BASE, OFFSET OFFSETS) => #hashedLocation("Solidity", keccakIntList(OFFSET BASE),       OFFSETS)
    rule #hashedLocation("Array",    BASE, OFFSET OFFSETS) => #hashedLocation("Array",    keccakIntList(BASE) +Word OFFSET, OFFSETS)

    syntax Int ::= keccakIntList( IntList ) [function]
 // --------------------------------------------------
    rule [keccakIntList]: keccakIntList(VS) => keccak(intList2ByteArray(VS))

    syntax ByteArray ::= intList2ByteArray( IntList ) [function]
 // ------------------------------------------------------------
    rule intList2ByteArray(.IntList) => .ByteArray
    rule intList2ByteArray(V VS)     => #bufStrict(32, V) ++ intList2ByteArray(VS)
      requires 0 <=Int V andBool V <Int pow256

    syntax IntList ::= byteStack2IntList ( ByteArray )       [function]
                     | byteStack2IntList ( ByteArray , Int ) [function]
 // -------------------------------------------------------------------
    rule byteStack2IntList ( WS ) => byteStack2IntList ( WS , #sizeByteArray(WS) /Int 32 )

    // #sizeWordStack(WS) is not necessarily a multiple of 32.
    rule byteStack2IntList ( WS , N )
         => #asWord ( WS [ 0 .. bytesInNextInt(WS, N) ] ) byteStack2IntList ( #drop(bytesInNextInt(WS, N), WS) , N -Int 1 )
         requires N >Int 0

    rule byteStack2IntList ( _WS , 0 ) => .IntList

    syntax Int ::= bytesInNextInt ( ByteArray , Int ) [function]
 // ------------------------------------------------------------
    rule bytesInNextInt(WS, N) => #sizeByteArray(WS) -Int 32 *Int (N -Int 1)

Solidity stores values of type bytes and string in one slot if they are short enough. If the data is at most 31 bytes long, it is stored in the higher-order bytes (left aligned) and the lowest-order byte stores 2 * length.

    syntax Int ::= #packBytes ( ByteArray ) [function]
 // --------------------------------------------------
    rule #packBytes( WS ) => #asInteger(#padRightToWidth(31, WS) ++ #asByteStack(2 *Int #sizeByteArray(WS)))
      requires #sizeByteArray(WS) <=Int 31
endmodule