Bringing ISA semantics to Lean and Lean-MLIR

In­struc­tion Set Ar­chi­tec­tures (ISA) are ab­stract mod­els which spec­i­fy the be­hav­ior of proces­sors at the ma­chine code lev­el. They are now spec­i­fied us­ing cus­tom pro­gram­ming lan­guages such as Sail and ASL in­stead of be­ing spec­i­fied us­ing prose. I will present a new, work-in-progress back­end for the Sail com­pil­er, which trans­lates the ISA spec­i­fi­ca­tions into Lean code. I will then sketch how this fits in ex­ist­ing for­mal­iza­tion ef­forts such as Lean-MLIR, a for­mal­iza­tion of the MLIR in­ter­me­di­ate rep­re­sen­ta­tion and com­pil­er in­fra­struc­ture in Lean.