Correct and expand edsl copy (#611)

edsl.md

@@ -293,26 +293,39 @@ The detailed mechanism of calculating the location varies by compilers.
 In Vyper, for example, `map[key1][key2]` is stored at the location:
 
 ```
-  hash(hash(idx(map)) + key1) + key2
+  hash(hash(key1 ++ slot(map)) ++ key2)
 ```
 
-where `idx(map)` is the position index of `map` in the program, and `+` is the addition modulo `2**256`, while in Solidity, it is stored at:
+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 ++ idx(map)))
+  hash(key2 ++ hash(key1 ++ slot(map)))
 ```
 
-where `++` is byte-array concatenation.
-
 The eDSL provides `#hashedLocation` that allows to uniformly specify the locations in a form parameterized by the underlying compilers.
-For example, 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.
+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}, idx(map), key1 key2)
+  #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](https://solidity.readthedocs.io/en/v0.5.11/miscellaneous.html#layout-of-state-variables-in-storage). 
+
 Specifically, `#hashedLocation` is defined as follows, capturing the storage layout schemes of Solidity and Vyper.
 
 ```k
@@ -323,6 +336,7 @@ Specifically, `#hashedLocation` is defined as follows, capturing the storage lay
 
     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]
  // --------------------------------------------------