Mechanizing the proof of a borrow calculus

In an ICFP'24 article, Ho, Fromherz and Protzenko propose a model of Rust borrowchecking. They provide a pen-and-paper proof of soundness, featuring original simulation invariants, defined as transitive closures. However, it also involves huge case analyses that are sometimes only sketched.We started the formalization of this proof in the Rocq prover. For mechanizing their reasoning, we introduced conditional rewriting systems and reduced some well-formedness conditions to arithmetic inequalities that we discharge with Rocq linear integer arithmetic procedure. On the way, we found a flaw in the proofs of some of their fundamental lemmas. We repaired their methodology using techniques from rewriting theory. This article presents the current state of our formalization.