An export with a proof

Tiramemsu articles · 31 October 2026 · companion to Taking memory out whole

An export format is a promise: what goes out can come back. Usually the promise is backed by a few round-trip tests. For tm export --format sg-nt12 it is backed by theorems. The format is defined in LeanRDF, a Lean 4 library that writes the W3C semantics of RDF as Lean definitions, and the tiramemsu exporter is checked against that definition on every build.

What is proven

LeanRDF's leanrdf-statements package models a tiramemsu statement as a record: an id, a subject and an object (each a term or another record's id), a predicate, a transaction interval and a valid interval. toRDF v is the export in a view v, and decode v reads a graph back. Two theorems connect them:

theorem decode_toRDF (hw : sg.WellFormed) : decode v (sg.toRDF v) = .ok sg
theorem toRDF_decode (h : decode v g = .ok sg) :
    sg.WellFormed ∧ ∀ t, t ∈ sg.toRDF v ↔ t ∈ g

The first says that nothing is lost: export, then decode, and you get back the same statements. The second matters more for checking. Anything the decoder accepts is exactly the export of a well-formed set of statements. A stray triple, a missing clock or a missing assertion is rejected with an error that names it, and nothing is dropped silently. So a file that decodes is correct by that theorem, whoever wrote it.

Lean checks these proofs with its kernel. The library has no sorry and uses only the three standard axioms.

The paper, executable

The paper When Is a Temporal Statement Store a Statement Graph? came with an abstract Lean development. LeanRDF vendors it, with its DOI and source commit, and applies it to real RDF terms:

• criterion: a set of records has an identity-preserving export to a Gelling–Fletcher–Schmidt Statement Graph exactly when it is closed and acyclic, and that export is unique.
• kernel: an executable peel, proven equal to the paper's export kernel, the greatest closed acyclic subset (kernel_greatest). isClosed and isAcyclic are deciders proven equal to the paper's relations.
• History closure: under tiramemsu's write rules the full history is closed and its cycles stay inside one transaction (history_closed, history_cycle, history_kernel).
• Quoting: nesting each reference as a triple term gives generalized RDF 1.2, and a basic graph pattern has the same answers over the live statements as over their quoted image (bgp_view').

$ leanrdf-sg kernel snapshot.jsonl
kernel: [6]
removed eid 4: dangling reference to eid 1
removed eid 5: depends on removed eid 4
removed eid 7: on a reference cycle
removed eid 8: on a reference cycle

Proofs are about the definitions. To catch a definition that says the wrong thing, an exhaustive check runs every statement graph of at most four records over a small alphabet: 406,901 of them. On each one it compares the kernel with a brute-force search, quoting with the kernel, and decoding with exporting in three views.

Why the clocks are integers

Valid time was meant to be an xsd:dateTime. Then the decoder theorems would need a proven round trip between epoch milliseconds and calendar dates. The arithmetic behind that conversion turned out to be hard to prove in Lean, and the attempt was slow and incomplete. So the export writes milliseconds as xsd:integer. Their round trip is already proven in LeanRDF's core. Because tiramemsu's own tm:validFrom is a dateTime, the export uses tm:validFromMs instead (LeanRDF v0.3.1).

Closing the loop between Rust and Lean

A proof about LeanRDF's definition says nothing about tiramemsu's Rust code. Three choices connect them:

• One canonical form. The Rust writer sorts triples the way LeanRDF's derived Ord on terms does: IRIs before blank nodes, before literals, before triple terms, then field by field. It also escapes strings exactly as LeanRDF's serializer does. So there is one right byte string for each export.
• Recorded outputs. tiramemsu's tests build stores through the Rust API: a route, a superseded distance in four views, a statement that never became visible, and awkward literals. They export each store and compare it with a recorded file.
• A test in Lean. LeanRDF keeps a copy of those files. Its test suite decodes each one in its view and requires the re-export to equal it byte for byte. tiramemsu's route export is also byte-identical to the golden file LeanRDF's authors wrote by hand before tiramemsu had the format.

Together these give a narrower claim than "the exporter is correct", but a precise one: for every recorded case, what tiramemsu wrote is exactly the export of a well-formed statement graph, by toRDF_decode. When either side changes, one of the two test suites fails.

What is trusted

• The transcription of the paper's definitions into Lean, which is vendored unchanged except for imports.
• The N-Triples parser and the JSON-lines reader, which are tested, not proven.
• The Lean compiler, for leanrdf-sg and the exhaustive check.
• tiramemsu itself beyond the recorded cases.

The linear-time bound of the paper's kernel algorithm is not mechanized: kernel is proven correct, not fast.

LeanRDF's site has a chapter on statement graphs and the package reference. The source is at github.com/Volland/rdf-lean.