Work on making the initial bytecode state explicit

I'm not really sure why this needs to happen in the end, since the
initial x86 state should be what we care about, and this will be
generated from the initial x86 program. However, this initial bytecode
state will be necessary for dealing with the bytecode machine on it own.

Right now there are 2 problems.

1. I can't load the bytecode compset without breaking HOL's parser, so I
can't get the actual concrete initial bytecode state.

2. There is a cheat where we need to know that the existentially
quantified bytecode state returned from the compiler theorem is the same
as the bytecode state that we build by running bc_eval on the bytecode
program that the compiler gives us. I think this should follow from
determinism of the bytecode language.