Re: C aggregate passing (Rust kernel policy)

[Ralf Jung <post@ralfj.de>]

Hi VJ,

>> 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.

Ah, there might be some of the logic for getting the MIR out of rustc, or some 
test cases. But the "core parts" of Miri (the actual UB checking and Abstract 
Machine implementation) don't have anything to do with RefinedRust.

; Ralf