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

We present a high-performance filtering and schema-validation algorithm based on Brzozowski’s derivatives extended to regular hedge grammars for semi-structured data. Our algorithm inherits the expressiveness of regular hedge grammars to support a wide range of schema languages and serialization formats, such as XML/RelaxNG, JSONSchema and Protocol Buffers. High performance is achieved by refactoring the derivative algorithm to make it more amenable to memoization of hedges and elimination of heap allocations. We verify the correctness of our memoized algorithm and several simpler derivative algorithms for regular hedge grammars in Lean, providing certified guarantees that any accepted or rejected data truly match the semantics of an intended schema. This is the first proof of correctness in an interactive theorem prover of a derivative algorithm for regular hedge grammars or any schema language. We benchmark our algorithm in Golang, showing it can filter millions of records per second.