start adding arrays and byte arrays to the bytecode

partial progress: have added new instructions, updated the refs state
component, and given semantics to some of the instructions, but haven't
fixed any proofs