Re: C aggregate passing (Rust kernel policy)

[Ventura Jack]

On Wed, Feb 26, 2025 at 2:39 PM Ralf Jung <post@xxxxxxxx> wrote:
> > On the other hand, RefinedRust reuses code from Miri.
>
> No, it does not use code from Miri, it is based on RustBelt -- my PhD thesis
> where I formalized a (rather abstract) version of the borrow checker in Coq/Rocq
> (i.e., in a tool for machine-checked proofs) and manually proved some pieces of
> small but tricky unsafe code to be sound.

I see, the reason why I claimed it was because

    https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev
        "We currently re-use code from the following projects:
        miri: https://github.com/rust-lang/miri (under the MIT license)"

but that code might be from RustBelt as you say, or maybe some
less relevant code, I am guessing.

Best, VJ.