lexpat
lexpat is a Lean 4 port of the XML 1.0 parsing semantics that libexpat implements, written for untrusted input. Agreement is at the specification level: the same document meaning, and the same event and error categories, not a byte-for-byte copy of the C library. A bounded C header exposes the calls that are implemented. Anything else fails closed.
What it covers
The core is a pure, total, resumable parser. It accepts UTF-8, UTF-16, ISO-8859-1 and US-ASCII, elements and attributes, character data, CDATA, comments, processing instructions, and the five predefined entities plus numeric character references. A document can be fed in any chunking. For an accepted document the events match the one-shot parse. For a rejected one, the error is the same and any events already returned are a prefix.
DTDs, external entities, namespace processing, XML 1.1 and unknown encodings are refused. There is no resolver, and no system identifier is read. Each document has fixed budgets: 8 MiB of input, 1 MiB for one token, 256 open elements, and 1 MiB of reference expansion. Crossing a budget is a named error. Those limits, and the missing resolver, are what remove the usual unbounded recursion and entity-amplification failure modes. A failure inside the Lean runtime allocator is not claimed to be impossible.
Two properties of the real UTF-8 decoder are machine-checked. The overlong leads 0xC0 and 0xC1 are rejected for every possible tail, and an ASCII scalar encodes and decodes back to itself. The Lean sources reject sorry, partial and unsafe. Those proofs do not extend to the whole parser. Behaviour against libexpat is the corpus and a differential against version 2.8.5, and that comparison is not a proof of end-to-end correspondence.
The integration route is the bounded C ABI on x86_64-linux: include/expat.h and liblexpat.so.1, for a parser created with XML_ParserCreate(NULL). Calls outside that subset fail closed. It is not a drop-in replacement for libexpat. The Lean API and the trace executable are for inspection, not a production interface.
Results
- Fail closed Unsupported
XML_*calls return failure. Namespace processing, DTDs, external entities, unknown encodings and suspend/resume are not implemented, and no resolver, file or network path exists. - 8 MiB Default input budget. One token stops at 1 MiB, the element stack at 256, and reference expansion at 1 MiB. Each miss names the budget it crossed.
- Decoder Two machine-checked properties of
decodeUtf8One: overlong two-byte leads are rejected, and ASCII round-trips. The reported axioms arepropextandQuot.sound. - 2.8.5 Differential against the pinned libexpat. Accepted documents are compared event by event. Rejected ones are compared by the accept or reject decision and by error code. Every deliberate difference is declared.
The decoder proofs do not cover the rest of the parser. A completed fuzzing run is not a proof that the parser is free of bugs, and refusing a feature this library does not implement is not a fix for that feature in libexpat.