It is widely recognized that interaction is indispensable in deductive
verification of real-world code. A verification engineer has to guide the
proof search and provide information reflecting their insight into the
workings of the program. Lately we have seen a shift towards a paradigm,
called verifying compilers, where the required information is provided in form
of program annotations instead of interactively during proof construction.

In this paper, we discuss the different purposes that annotations can
serve. Based on a clarification of what the notion of completeness means in
the framework of verifying compilers, we show that some auxiliary
(non-requirement) annotations are (only) needed for efficiency of proof
search, while others are essential for completeness, i.e., indispensable for
proof construction.