RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code