parsebot
A simple grammar is enough to extract a correct parser. parsebot writes that parser from a BNF in Rocq, proves it agrees with the grammar, and extracts it to OCaml. A faster zero-copy parser is then proved to refine the first: the same parse, for every input.
What it covers
Three grammars are certified end to end. JSON follows RFC 8259. HTTP/1.1 chunked transfer uses a value-dependent grammar for the chunk length. TOML covers integer scalars, dotted keys, tables, and arrays of tables, including the decision that statements are separated by one or more whitespace characters.
Soundness and completeness are Qed for all three: the parser only produces real denotations, and every denotation can be parsed. The parsers extract to self-contained OCaml. A zero-copy JSON tokenizer is proved to agree with the certified parser on every input, recording spans instead of rebuilding strings.
Results
- ~30 MB/s
parse_jsonparses 4.75 MB in about 0.16 s. - 10–13 MB/s Chunked decoding, linear in the input.
- 267.9 MB/s Zero-copy tokenizer on
gsoc-2018.json(3.3 MB, 1,264 nested objects): 24.4× the list-based parser on that file, and 2.43× on a geometric mean of 13 files. - 20–30 MB/s TOML surface parser on synthetic flat documents.
The certified TOML document fold is O(n²) in the number of statements. Lookup scans a list. That cost is in the certified state machine, not in extraction.