restrict bytecode printing to certain values

update bytecode semantics so Print is protected by a new can_Print
predicate. update the compiler proof accordingly (it needs to ensure
that it only calls Print on can_Print values).