BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verifying Peephole Rewriting In SSA Compiler IRs - Tobias  Grosser
  (University of Cambridge)
DTSTART:20241010T134500Z
DTEND:20241010T143000Z
UID:TALK220336@talks.cam.ac.uk
DESCRIPTION:There is an increasing need for domain-specific reasoning in m
 odern compilers. This has fueled the use of tailored intermediate represen
 tations (IRs) based on static single assignment (SSA)\, like in the MLIR c
 ompiler framework. Interactive theorem provers (ITPs) provide strong guara
 ntees for the end-to-end verification of compilers (e.g.\, CompCert). Howe
 ver\, modern compilers and their IRs evolve at a rate that makes proof eng
 ineering alongside them prohibitively expensive. Nevertheless\, well-scope
 d push-button automated verification tools such as the Alive peephole veri
 fier for LLVM-IR gained recognition in domains where SMT solvers offer eff
 icient (semi) decision procedures. In this paper\, we aim to combine the c
 onvenience of automation with the versatility of ITPs for verifying peepho
 le rewrites across domain-specific IRs. We formalize a core calculus for S
 SA-based IRs that is generic over the IR and covers so-called regions (nes
 ted scoping used by many domain-specific IRs in the MLIR ecosystem). Our m
 echanization in the Lean proof assistant provides a user-friendly frontend
  for translating MLIR syntax into our calculus. We provide scaffolding for
  defining and verifying peephole rewrites\, offering tactics to eliminate 
 the abstraction overhead of our SSA calculus. We prove correctness theorem
 s about peephole rewriting\, as well as two classical program transformati
 ons. To evaluate our framework\, we consider three use cases from the MLIR
  ecosystem that cover different levels of abstractions: (1) bitvector rewr
 ites from LLVM\, (2) structured control flow\, and (3) fully homomorphic e
 ncryption. Our mechanization provides a foundation for formally verified r
 ewrites on new domain-specific IRs and has fueled recent advances in bitve
 ctor reasoning in the lean interactive theorem prover\, which I will share
  a recent update on.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR