Refinement Proofs in Rust Using Ghost Locks. - Aurel Bílý; João C. Pereira; Jan Schär; Peter Müller 001 (CoRR, 2023)