(Partially a note to self here)

We have a test in src/test/cargo-rmc/simple-proof-annotation that runs the code for proof harness attributes, but we don't have any tests checking that it produces the correct answer.

This test suite has special merit for ensuring that we're actually recognizing proof annotations is all cases. We had an issue early on where the function weren't being codegen'd at all, and so we never saw them to take note of the proof annotation.

So we should include: public functions, private functions, crate-type bin, crate-type lib, conflicting names, and whatever else we think of.