Had to slightly tweak (strengthen) stack3's spec for that

Using concurrent runners

- Implement the concurrent runners library

- Changed the shared bag specification to allow the predicate `P` to
  depend on the bag itself -- this is needed for the `isRunner`
  invariant: since the bag is *part* of the `Runner` class, the bag is
  constructed/allocated before the `Runner` itself is construted; but
  we want the bag invariant to depend on the `Runner` instance.

- evmap is dropped
- per-item invariant is implemented with inv-in-inv
- peritem.v is simplified by proving an ad-hoc iter spec
- update to latest iris
- related fixes

Also update IRIS_VERSION because I can't be bothered to downgrade now...