"we model a scenario where the original code is memory-safe; the ported code is memory-safe; and we consider memory safety and undefined behavior that may arise across the FFI layer between the two pieces of code."

I may be stating the obvious, but that's a bit of a strawman. Yes, writing good FFI code is hard; yes it could result in security/soundness issues; yes, we could use better tools in this space.

But nobody rewrites C code in Rust if they believe existing codebase is free of memory safety hazards; they rewrite it because they think the result will contain fewer hazards, even accounting for the potential problems at the FFI boundary.

If I could remove tens of thousands of lines of hard-to-analyze C code, and replace it with tens of thousands of lines of safe Rust, paired with a few hundred lines of hard-to-analyze FFI adapters, that sounds like a pretty good tradeoff to me. I now know exactly where to focus my attention, and I can have confidence that the situation will only improve with time: better tooling may allow me to improve the dangerous FFI layer, and in the meantime I can recklessly improve the safe Rust module without fear of introducing new memory unsafety bugs, unsound behavior, or data races.