do the labels removal without cheats

adds to the database of known code_labels_ok whenever evaluating
compile_Cexp (and compile_prog). makes progToBytecode depend on
compiler/proofs, since that's where the proof of code_labels_ok comes
from; but the compset builder should be moved out of progToBytecode
anyway.

it seems to run fast enough on small examples, but there might be a
possibility for improvement if the long lists of bytecode were
abbreviated: currently doing net matching etc. on the raw list.