Certified regexp matching in hardware: Source listing

You can browse the rocq generated source listing from this page. There are three ways to browse the source.

README
Recommended way to read the source. Gives a top down plan for reading source code. We have skipped what would be of only technical interest though whatever we describe in the paper should be available from this page. This listing is not exhaustive.
The Table of contents
The table of contents is exhaustive listing of the modules that constitute the source. The listing is mostly in the order in which one would want to read the source code. However, some of the modules are rather technical and have sparse documentation (we are working on improving it but it remains work in progress) and might not be of so much of interest.
The Index file
One can also consult the rocq-doc generated index for quick references.
Demo
An example demonstrating the use of our library to build a regular expression matcher for identifiers in the C language.