A certified programming project in rocq (like CompCert for example) develops the program together with its proof of correctness in rocq. Actual executable software is then obtained by first extracting to Haskell (or Ocaml or Scheme) followed by compiling with the the Haskell compiler. The machine checked proofs that are part of the original rocq source acts as quality assurance certificates of the executable.
The Clash project is a Haskell to Hardware (VHDL or Verilog) compiler so with the extraction mechanism one can use a similar approach for hardware as well. However, due to the nature of Hardware this is not so straight forward. In this talk, I will show how to use the above outlined approach to get high assurance, high performance hardware. Our main contribution is a rocq library for building certified regular expression matcher in hardware. I will start by explaining the basics of interactive theorem proving in rocq and the
mechanism for developing certified programs. We will look at some of the challenges that needs to be addressed in order to get hardware out of such programs.
This is joint work with Julin Shaji and Sandeep Chandran. The associated code is available from the public repository.
https://gitlab.com/piyush-kurur/regexp-hardware
Brief bio: Ph.D, Institute of Mathematical Science then faculty at IIT Kanpur and currently at IIT Palakkad.
