Support vyper jumptables

[0xkarmacoma]

Is your feature request related to a problem? Please describe.

Newer versions of vyper use jumptable-based dispatchers. We don't currently handle them very gracefully because of the mod operation.

For instance say a vyper contract implements 3 functions, the dispatcher will do something like this:

jump_table_offset = XXX   # (typically at the end of bytecode)
jump_table_index = input % 3
jump_target = codecopy(jump_table_offset + jump_table_index * 2)
JUMP(jump_target)

Because of the mod operation, halmos will fail with NotConcreteError(f"symbolic JUMP target: {dst}") or a symbolic CODECOPY error

Doing this from memory, so I'm not sure exactly what input is used, but if it is concrete then we should be able to resolve it. If it is symbolic, we may have to run a solver query to know which are the possible values, or identify the pattern and loop over the jumptable values

cc @zobront @charles-cooper