BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Formalisation of mathematics with interactive theo
 rem provers 
SUMMARY:Automatic Verification of BitVector Identities in 
 SSA-Based Compiler IRs - Tobias Grosser (Universit
 y of Cambridge)
DTSTART;TZID=Europe/London:20241128T170000
DTEND;TZID=Europe/London:20241128T180000
UID:TALK222772AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/222772
DESCRIPTION:There is an increasing need for domain-specific re
 asoning in modern compilers. This has fueled the u
 se of tailored intermediate representations (IRs) 
 based on static single assignment (SSA)\, like in 
 the MLIR compiler framework. Interactive theorem p
 rovers (ITPs) provide strong guarantees for the en
 d-to-end verification of compilers (e.g.\, CompCer
 t). However\, modern compilers and their IRs evolv
 e at a rate that makes proof engineering alongside
  them prohibitively expensive. Nevertheless\, well
 -scoped push-button automated verification tools s
 uch as the Alive peephole verifier for LLVM-IR gai
 ned recognition in domains where SMT solvers offer
  efficient (semi) decision procedures. In this pap
 er\, we aim to combine the convenience of automati
 on with the versatility of ITPs for verifying peep
 hole rewrites across domain-specific IRs. We forma
 lize a core calculus for SSA-based IRs that is gen
 eric over the IR and covers so-called regions (nes
 ted scoping used by many domain-specific IRs in th
 e MLIR ecosystem). Our mechanization in the Lean p
 roof assistant provides a user-friendly frontend f
 or translating MLIR syntax into our calculus. We p
 rovide scaffolding for defining and verifying peep
 hole rewrites\, offering tactics to eliminate the 
 abstraction overhead of our SSA calculus. We prove
  correctness theorems about peephole rewriting\, a
 s well as two classical program transformations. T
 o evaluate our framework\, we consider three use c
 ases from the MLIR ecosystem that cover different 
 levels of abstractions: (1) bitvector rewrites fro
 m LLVM\, (2) structured control flow\, and (3) ful
 ly homomorphic encryption. We envision that our me
 chanization provides a foundation for formally ver
 ified rewrites on new domain-specific IRs.\n\n\n==
 = Hybrid talk ===\n\nJoin Zoom Meeting https://cam
 -ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1Ipp
 YCsbooOVqenzI.1\n\nMeeting ID: 871 4336 5195\n\nPa
 sscode: 541180
LOCATION:MR14 Centre for Mathematical Sciences
CONTACT:Jonas Bayer
END:VEVENT
END:VCALENDAR