Did you consider using an established Rust verification toolchain like Aeneas?
Edit: I don't do this often, but why is my question being downvoted? Is this question not allowed?
AFAICT, Aeneas only supports a safe subset of Rust. I needed something that could support all of Rust
https://github.com/AeneasVerif/aeneas says
"Aeneas currently functionalizes a subset of safe Rust, and we are in the process of extending the functional model with reasoning based on separation logic to support unsafe code and concurrent code."
A Rust verification toolchain won't tell the GP whether his code does the same as the C code or not.