Feature Requests Triage at the Verus Retreat '24

[utaal]

Add a feature request, up vote it if you care about it, and add comments on why you want it.

Use ## Feature title as the comment header.

[utaal]

Lightweight termination checking for exec

Ignore liveness.

[utaal]

More sources of non-termination than just checking for decreases clauses on loop and recursion.

[utaal]

Already supported for recursion, and loops. No enforcement yet.

How to do UX?
error (initially warning) in the absence of a decreases clause in exec code, and crate-level attributes to opt-in or opt-out of total correctness.

[utaal]

@matthias-brun, @jaylorch: consider opting out for individual function, i.e. main, with an attributes. Folks are not against the idea.

@jaylorch: find a name flaggable by the auditor.

[utaal]

From and Into traits

[utaal]

You can do it for whatever type you want https://doc.rust-lang.org/std/convert/trait.From.html

? desugars into something that has a trait bound that interacts with FromResidual.

• proper spec for From and remove hack for ?.

[utaal]

One can add their own external spec.

• document that process.

[utaal]

Vector literals

[utaal]

@tjhance, @Chris-Hawblitzel: it may be pretty easy to support.

[utaal]

vstd functions for (debug) printing

[utaal]

@jaybosamiya: something that's easier than println

It's supposed to be transparent. Encode the body, ignore the dbg!.

Add Debug to the ignored traits.

[utaal]

@Chris-Hawblitzel: find all the things we want Verus to ignore.

[jaybosamiya-ms]

Specifically, dbg! (https://doc.rust-lang.org/std/macro.dbg.html)

[utaal]

@Chris-Hawblitzel treat the Debug impl as external, and enforce it to be called from the dbg! macro.

Add an attribute "this comes from the dbg! macro".

[utaal]

Support for dyn

[marshtompsxd]

A use case that also motivates this: in the Anvil project we have to define a struct that needs to take a sequence of different types that all implement a trait T. Right now our solution is: (1) define an opaque type and use that type in the struct, (2) define (uninterpretable) functions to convert between each type to/from the opaque type, (3) define axioms for each type that any object of this type remains unchanged after a RTT of the conversion --- similar to marshal and unmarshal.

[utaal]

Type invariants

[utaal]

High priority feature for @tjhance. But what do people want?

• do you want invariants to be temporarily broken?

@y1ca1: don't want the invariant to ever be broken, and in the use case it's not going to be mutable.

[utaal]

James G.: have two different types, one with the invariant enforced, and one without.

[utaal]

Separating and identifying trusted vs. untrusted code

[utaal]

Discussed in the discussion.

[utaal]

Dual mode spec/exec

[utaal]

'returns' clause for exec functions

[utaal]

returns clause one step forward;
maybe other proposals are two steps forward.

[utaal]

make eager checking for spec fn requires configurable

[jaybosamiya-ms]

Solved by #1178

[utaal]

Support for some fields pub and some private in a struct

@utaal: it's relatively easy.

[utaal]

Smoke test

Insert assert(false), or perhaps focus on assert(precondition => false).

Using (unsat-core) to see which conjuncts were actually used for a proof

Also potentially run the query multiple times.

Oded: Environment with precondition with 10 conjuncts, and only 2 are needed.

[utaal]

Document external_*

• external_fn_specification
• external_type_specification
• external_trait_specification

Not many votes, but asked verbally many times.

[utaal]

These have been folded into the relative discussions and otherwise ported over to Verus Features