BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automatic Verification of BitVector Identities in SSA-Based Compil
 er IRs - Tobias Grosser (University of Cambridge)
DTSTART:20241128T170000Z
DTEND:20241128T180000Z
UID:TALK222772@talks.cam.ac.uk
CONTACT:Jonas Bayer
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. We envision that our mechanization provides a foundation for fo
 rmally verified rewrites on new domain-specific IRs.\n\n\n=== Hybrid talk 
 ===\n\nJoin Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTN
 kOcfVrIE1IppYCsbooOVqenzI.1\n\nMeeting ID: 871 4336 5195\n\nPasscode: 5411
 80
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR