This repository contains a Lean mechanization of the basic data structures and theorems of "A Complete, Formal Semantics for Rust Source Code" by Daniel Drodt, to be submitted to TOPLAS.
The basic definitions and work has been done by Thanh Long Nguyen for his BSc thesis (supervised by Daniel Drodt) and has been slightly extended by Daniel Drodt.
Other parts of the mechanization are work in progress.