[Proposal] explicitly annotate all trusted members

[jcp19]

At the moment, it is hard to get a grasp of all assumptions that are made in any large verified codebase. We can easily find occurrences of assume, inhale, explicitly trusted functions and domain definitions, but searching for abstract predicates and methods/functions is a bit more annoying (can be done with regex though).

I would suggest requiring that all abstract members take the trusted annotation to make this easy to search for.

On a related note, @ArquintL and I once discussed the possibility of introducing a new kind of member (spec) for closure specifications, instead of using abstract methods. This would also make it clear that we are not introducing an assumption.

[jcp19]

Any opinions @Dspil @ArquintL?

[Aurel300]

(My 2 cents: the solution you propose sounds like you want to make this easier to find using basic text search. Shouldn't this rather be something the Gobra tooling can do for you? It already has a parser which can tell which items are trusted, maybe add a command flag to dump them?)

[jcp19]

Sure, the tooling may produce a list of trusted items, regardless of whether there is a textual indication of this. I don't see why it would be a problem to have this at the source-code level though -- it makes the intention clear, and it helps in reviewing PRs that introduce new trusted members.

Separately, the introduction of spec members is, IMO, really necessary at this point, given that we need to be able to distinguish between trusted functions and closure specs that cannot be called directly

[ArquintL]

My comment goes in a similar direction as @Aurel300's: Imho Gobra already produces JSON output specifying what stuff did not get verified. Orthogonally, adding a bunch of trusted annotations all over the codebase only partially addresses the underlying problem: If you import a package but you forget to verify that package, you're also implicitly assuming its correctness. This case is imho covered by the JSON output but I don't see how a syntactic solution could give you the same

[jcp19]

hmm, I don't think that the json that is produced is intended for direct human consumption. In particular, it produces information at the Viper level rather than at the Gobra level: we use the Viper function ids, and we report on members that do not have a direct counterpart at the Gobra level. Second, the reporting in .json is inaccurate: I believe that an imported function is not counted as trusted if it is not marked as such, even if it is abstract. We discussed this when Johannes was developing the stats reporting mechanism, and back then we didn't really have a good idea of how to solve it (as it seemed that there was not a lot of information to decide this correctly because all imported functions are stripped of their bodies). In this case, requiring that you mark abstract functions as trusted actually allows you to produce more accurate json reports.

Finally, regarding this part here

Orthogonally, adding a bunch of trusted annotations all over the codebase only partially addresses the underlying problem: If you import a package but you forget to verify that package, you're also implicitly assuming its correctness.

I think this is not the underlying problem. I think this is a consequence of the very nature of modular verification - you assume the public interface of a package/method to hold, so that you can prove your package/method against that. From my perspective, this is not different from assuming that a contract of a callee holds when you are verifying the caller - ofc, the contract of the callee might not hold, but the guarantees that you get are relative anyway.

[ArquintL]

Regarding modularity, if you actually verify multiple packages (like Gobra supports), you could actually point out the remaining assumptions (unverified packages incl. standard library, abstract functions, ...)

[jcp19]

Regarding modularity, if you actually verify multiple packages (like Gobra supports), you could actually point out the remaining assumptions (unverified packages incl. standard library, abstract functions, ...)

Yes, I think that is a good idea!