trusted/untrusted split

[tjhance]

Verus should provide tools to help the user understand what trusted code they are relying on. This tool should understand that there are multiple kinds of “trusted code” that a user would want to learn about.

• “Unintentionally trusted” code. Things like unfinished proofs that you've procrastinated on.
• “Intentionally trusted” code. This has a few categories:
  • Bottom bread code, like the Verus core library or specifications of fancy hardware intrinsics
  • Top bread code, i.e., the specification you provide to the user
  • Environmental specifications (e.g., state machine model of an external disk or network)

(In our previous projects, this was a total mess, despite @jonhnet's valid protests that we should clean things up. There was little-to-no distinction between the three types of intentionally trusted code, since they were all lumped under .s. The only way to declare an axiom as "intentional" was to declare it as :external, but there was nothing that ensured there were no :external lemmas in the .i files, because the toolchain didn't actually know about the .s / .i distinction. Also, .s files could only include other .s files, which was sometimes undesirable - when you write a definition, you don't always know a priori if somebody is going to want to use that definition in a specification.)

I don't actually have any proposals! I just wanted to create a discussion place for this.

[tjhance]

Another quick point: The .s/.i thing really only makes sense in monolithic developments, because one developer's top bread is another one's middle bread. What I mean is that a library exposes some functions, they might declare that to be their API with trusted specifications, but if another developer imports that library, they might prove their own code valid against the library's specifications, and provide their own trusted specifications. I think the best way to think of the "top bread" is just "whatever the library (crate) exports". No need to overthink that one.

[parno]

this was a total mess

That might be a bit harsh. In general, I think we've been pretty disciplined in keeping trusted code to .s files and verified code in.i. In the past our build system did prevent the inclusion of axioms in .i files (via Dafny's /noCheating flag, which turns up unintentionally trusted code), and it prevented .s files from including .i files. It's possible that atrophied in the VeriBetrFS development though.

It sounds like you're proposing an additional level of refinement among the trusted files, which is a fine point to discuss.

[tjhance]

I guess it was a little harsh. If it makes you feel better, I was mostly thinking of Seagull. 😅

[jonhnet]

I don't think VeribetrFS slipped on this axis, but I do think there's room to improve.

because one developer's top bread is another one's middle bread

This is an important, subtle point. Even in monolithic VeriBetrFS, we carefully split Sequences into "parts of the library we needed Player 1 to read" (.s) and "everything else" (.i). As Travis points out here, the problem gets worse when we start composing, as code that was once .s can be downgraded to .i in the new context.

The high-level goal to keep in mind is this: We want to clearly identify the code involved in the statement of the theorem supported by verification. Alternatively, we want to clearly identify lines of code that must be inspected by Player 1. I don't know how to solve that problem in the presence of the issues identified in this thread, but I'm hoping reminding us of the problem statement may help.

In vying for "least important contribution", I think we should rename ".s" to ".t" (trusted) and ".i" to ".v" (verified).

[parno]

One option would be to introduce an additional suffix (.ifc?) for the exported API. For a library, the exported API would be trusted. For the client code that uses the API, it would be proof, but the client's exported API would be trusted. It seems feasible for a tool to detect the difference between a top-level API (one that isn't included anywhere else) and an internal API.

[jonhnet]

The idea of tooling illuminates the issue. Suppose for a moment we didn't use any suffixes; we could have a tool print out the transitive closure of the theorem; that should, in principle, emit what find -name \*.s does today.

However, I think the only reason that would work is because humans carefully design the separation -- and use file suffixes to express their intent. If we didn't have the suffix convention, it'd be very easy to lose track of what was included, and suddenly the closure tool is printing out every line of the whole system. The file suffixes capture intent in a way that produces early warnings (errors from the build system) if a user violates that intent.

So I'm thinking the challenge here is to figure out what we want the intent to be in the presence of libraries that are used in multiple settings (Sequences.s) and in the presence of verification sandwich composition.

[tjhance]

I don't think a suffix is needed for an exported API, because we already have the pub keyword to determine what gets exported, and I think we should lean into the tools we already have.

I think it should be the job of the documentation toolchain to help the user understand what's being exported and the transitive closure of the spec functions that are used in those definitions.

[tjhance]

engineers are already familiar with the notion of public/private. Also, it's pretty flexible and easy to mark a type as 'export this type but not its fields'. If "interface files" were a thing, we'd need a notion of stubbed types and stubbed functions that could be filled in elsewhere in the crate. This would not only be awkward, it would be redundant with existing lang features. It's also kind of a pain - in Seagull, I always dreaded having to create these stubs.

On the other hand, if we got rustdoc working with verus, it would immediately allow us to see all the exported functions in a crate. With a bit of work, we could make it convenient to browse spec functions.

I think the unique-ish challenge here is trusted bottom bread code. If I depend on VeriBetrFS which depends on VeriBetrKV which depends on a CRC-32 library that depends on someone's trusted specifications of intel's polynomial division instructions, I might want to know about that. This isn't the usual sort of thing user-documentation would ordinarily surface, but a verification engineer would want to know about it.

[utaal]

I have added a #[verus::trusted] attribute to mark system and environment specification. There is no automatic checking that only trusted functions are reachable from other trusted functions.

[utaal]

[Verus retreat '24]

@jaylorch: consider --print-auditor-report.

@jonhnet: engineers read source code.

[utaal]

#![verus::trusted] is already supported, but has no restrictions -- it should restrict what you're allowed to include (plus vstd). @jonhnet: this gets us 90% of the way, one can then grep for #![verus::trusted].

@jonhnet would want cargo verus to enforce the file structure.

@tjhance mentions that it's hard to delineate things along file names. It requires adding additional traits for example.

[utaal]

@parno: in a PR you wouldn't necessarily see the report from the auditing tool.

[utaal]

@tjhance, @Chris-Hawblitzel: attribute to mark "only the signature is trusted".

#[verus::trusted_signature]

[utaal]

@Chris-Hawblitzel: someone propose a sample project structure that they'd want to enforce.

@tjhance consider the crates that go up on crates.verus.io, where you'd want to be able to mark trustedness.
@jonhnet: I've only thought about this on a single instance of a project, but what about more complex interactions of developers and consumers.

[utaal]

@tjhance: vstd could use some separation between trusted stuff and untrusted stuff.