&inator: Correct, Precise C-to-Rust Interface Translation
summary
&inator automatically produces Rust declarations for C top-levels by formulating semantic-equivalence and borrow-checking as SMT constraints and solving them to assign Rust types to C occurrences, using Z3 and a fragment-based IR that permits pointer transformations and optimality objectives. It claims correctness (a safe-Rust implementation exists) and precision (chooses minimal-cost types), proves this on nine benchmarks with artifacts available, and reports solver time dominating (a 350-line RB tree → 20 minutes solve). type fragments
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:42Why C to Rust translation matters
- 1:47Challenges in C to Rust translation
- 2:50Refinement's interface translation
- 3:55Correctness and precision in Rust
- 7:53Refinement's architecture & SMT constraints
- 10:41Constraint categories for correctness
- 15:04Evaluation results & performance
- 16:49Conclusion & future directions
- 17:11Q&A
related talks
15mTranslating C to Safer Rust
22mDon’t Write, but Return: Replacing Output Parameters with Algebraic Data Types in(…)
58m(Almost) Everything You Should Know About The Compiler Frontend
34mMiniRust: A core language for specifying Rust
19mTerms for Efficient Proof Checking and Parsing
17mFoundations for a Rust-Like Borrow Checker for C
36mRust's trait system is a proof engine, let's make it prove us an ABI!
19mRustlantis: Randomized Differential Testing of the Rust Compiler