Support symbolic indexing into concrete containers

[pschanely]

There is some in-progress work to Intercept identity operations. Once we have that we could, in theory, symbolic index into a concrete list, and return a proxy with a not-yet-determined identity.

Note also that, even without identity intercepts, we could be doing this when the values are of a uniform type and representable with symbolics.

[pschanely]

Note also that, even without identity intercepts, we could be doing this when the values are of a uniform type and representable with symbolics.

As of v0.0.86, this portion has been implemented. It's a big improvement for certain use cases; e.g. we can now solve stuff like this in a single iteration:

_ONE_HUNDRED_HASHES = [(k*13 ^ k) % 100 for k in range(100)]

def lookup_hash(n: int) -> int:
  '''
  pre: 0 <= n < 100
  post: __return__ != 40
  '''
  return _ONE_HUNDRED_HASHES[_ONE_HUNDRED_HASHES[_ONE_HUNDRED_HASHES[n]]]

/tmp/main.py:6: error: false when calling lookup_hash(86) (which returns 40)

(crosshair-web link)