hopefully useful bootstrap lemma

says what the references look like in the bytecode state when the
compiler invariant holds; hoping this will do some (or most) of the work
of allowing the references to be changed.