Re: C aggregate passing (Rust kernel policy)

Ralf Jung
2025-02-26T16:10:51Z

Hi,

>> [Omitted] (However, verification tools are
>> in the works as well, and thanks to Miri we have a very good idea of what
>> exactly it is that these tools have to check for.) [Omitted]
>
> Verification as in static verification? That is some interesting and
> exciting stuff if so.

Yes. There's various projects, from bounded model checkers (Kani) that can
"only" statically guarantee "all executions that run loops at most N times are
fine" to full-fledged static verification tools (Gillian-Rust, VeriFast, Verus,
Prusti, RefinedRust -- just to mention the ones that support unsafe code). None
of the latter tools is production-ready yet, and some will always stay research
prototypes, but there's a lot of work going on, and having a precise model of
the entire Abstract Machine that is blessed by the compiler devs (i.e., Miri) is
a key part for this to work. It'll be even better when this Abstract Machine
exists not just implicitly in Miri but explicitly in a Rust Specification, and
is subject to stability guarantees -- and we'll get there, but it'll take some
more time. :)

Kind regards,
Ralf