Chain of read+writes could be improved by analyzing array/map indices

As documented in:

```
-- This does not strip writes that cannot possibly match a read, in case there are
-- some write(s) in between that it cannot statically determine to be removable, because
-- it will early-abort. So (load idx1 (store idx1 (store idx1 (store idx0)))) will not strip
-- the idx0 store, in case things in between cannot be stripped. Potential for improvement. TODO.
-- See simplify-storage-map-todo test for an example where this happens
readStorage :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
readStorage w st = go (simplify w) st
```

A good example test where this is obvious:

```
, test "simplify-storage-map-todo" $ do
Just c <- solcRuntime "MyContract"
[i|
contract MyContract {
mapping (uint => uint) a;
mapping (uint => uint) b;
function fun(uint v, uint i) public {
require(i < 1000);
require(v < 1000);
a[i] = v;
b[i+1] = v+1;
b[i+v] = 55; // note: this can overwrite b[i+1], hence assert below can fail
assert(a[i] == v);
assert(b[i+1] == v+1);
}
}
```

Which will do things like below, where we read from 0x1, and write to a bunch of 0x1, but ALSO write to 0x0, which could be stripped.

```
(SLoad
slot:
(Keccak
(WriteWord
idx:
0
val:
(Add
1
(Var "arg2")
)
)
(ConcreteBuf
Length: 64 (0x40) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 01 ................
)
)
storage:
(SStore
slot:
(Keccak
(WriteWord
idx:
0
val:
(Add
(Var "arg2")
(Var "arg1")
)
)
(ConcreteBuf
Length: 64 (0x40) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 01 ................
)
)
val:
55
)
(SStore
slot:
(Keccak
(WriteWord
idx:
0
val:
(Add
1
(Var "arg2")
)
)
(ConcreteBuf
Length: 64 (0x40) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 01 ................
)
)
val:
(Add
1
(Var "arg1")
)
)
(SStore
slot:
(Keccak
(WriteWord
idx:
0
val:
(Add
1
(Var "arg2")
)
)
(ConcreteBuf
Length: 64 (0x40) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 01 ................
)
)
val:
(Add
1
(Var "arg1")
)
)
(SStore
slot:
(Keccak
(WriteWord
idx:
0
val:
(Var "arg2")
)
(ConcreteBuf
Length: 64 (0x40) bytes
0000: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0010: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0020: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
0030: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
)
)
val:
(Var "arg1")
)
(AbstractStore (SymAddr "entrypoint") Nothing)
)
```

Start with the readStorage simplifier and the simplify-storage-map-todo test case shown in the issue; inspect how chained SStore entries are analyzed against a later SLoad. Run that test before and after the change, and consider the work complete when provably nonmatching writes such as the idx0 store are removed without changing the asserted storage behavior.

Written by the indexing model from the issue text.