Add #[verifier(unforgeable)] attribute for #[proof] structs

[tjhance]

There are - fundamentally - two different kinds of "proof" objects. One kind is basically like a normal struct, except that it gets erased. With such types, you build up a "struct" of smaller proof objects.

The other kind is the "base" objects that represent permissions or some other fancy thing, e.g., Permission. To make it easier to handle this second type, I added an attribute #[verifier(unforgeable)] to declare such types.

The rules:

• An unforgeable datatype must be proof.
• An unforgeable datatype can only have spec fields.
• You cannot call a constructor of an unforgeable datatype (in proof mode)
• You cannot modify a field of an unforgeable datatype.

Here, I add the attribute, implement these rules, and add tests. Although, it doesn't look like there is any support at all for field updates yet, so there was nothing to do for the last step.

[parno]

This does seem like a useful primitive to support. In the past, we've used a similar notion for things like "the file system" or "the trace of network operations".

When adding features like this, I think it would be a good idea to include some example uses in a file in source/rust_verify/example/, along with some basic documentation, so people can get an idea of how to use the feature.

[tjhance]

there's an example in cells.rs

[parno]

Do you mean source/rust_verify/example/cells.rs? If I'm reading GitHub correctly, that doesn't seem to have unforgeable yet. I also see source/pervasive/cell.rs, which uses one invocation of unforgeable, but it seems like it's using it for a specific implementation, not as a documentation example. I was thinking of something more along the lines of source/rust_verify/example/recursion.rs, source/rust_verify/example/datatypes.rs or source/rust_verify/example/integers.rs. Or possibly something even more documented!

[tjhance]

There aren't any ways to create a (useful) user-defined untrusted #[unforgeable] token. It's an attribute meant for trusted primitives like Permission, and later, for LTS token types.

Regarding documentation, is there a document for mode-related rules & decisions? This kind of thing should go there.

[parno]

There aren't any ways to create a (useful) user-defined untrusted #[unforgeable] token.

It seems like it would be useful for users to create their own (trusted) tokens, so that they don't have to cobble together a solution as we've done a number of times in Dafny for things like the contents of the file system, IO operations, or for LTS.

[utaal]

Regarding documentation, is there a document for mode-related rules & decisions? This kind of thing should go there.

I've imported Chris' modes doc from the old wiki into docs/design, where I've suggested we keep track of design decisions and motivations:

https://github.com/secure-foundations/verus/tree/main/source/docs/design

Another file here may be good, if examples are insufficient. In the fullness of time we'll probably need a manual, but probably not a priority yet.

[utaal]

The test harness changes look good to me (@Chris-Hawblitzel asked me to take a look at those).

[tjhance]

It seems like it would be useful for users to create their own (trusted) tokens, so that they don't have to cobble together a solution as we've done a number of times in Dafny for things like the contents of the file system, IO operations, or for LTS.

I think it would be useful; the tokens we made for the verified cache were very ad hoc and as we only have the one example (using the ghost token methodology) I think we don't yet have a clear idea of the trusted-yet-principled way to structure the token definitions in conjunction with the model of the external system.

Anyway, this PR is mostly meant to be a technical detail so we can build the more advanced stuff later, so I'm going to go ahead and merge it.