more updates of bytecodeProofScript.sml
fix definition of compile_envref

the bytecode Deref instruction now requires an index on the stack
update proof of compile_varref_thm