Verified Derivatives for Fast Filtering and Schema Validation of Semi-Structured Data

Proofs written in Lean4 of the core katydid filtering algorithm for the paper: Verified Derivatives for Fast Filtering and Schema Validation of Semi-Structured Data.

Here we formalize the core of the Katydid filtering algorithm. This algorithm allows us to filtering through millions of serialized data structures per second on a single core. We recommend following the Readme documents, to get an overview of each folder.

Setup

• Install Lean4.
• Remember to also add lake (the build system for lean) to your PATH. You can do this on mac by adding export PATH=~/.elan/bin/:${PATH} to your ~/.zshrc file