[jasisz]

Both entries now convert the test's ndjson to Susz first, then Pestka checks the Susz file. Susz is a binary form of lean4export's output. It holds the same records with no text to parse, and the proofs used by only one theorem sit in blocks of their own. Pestka leaves those blocks as bytes until it checks the theorem.

The conversion is done by susz, a small converter written in Rust. Both steps run inside the entry's command, so the converter's time, memory and instructions are counted too.

The converter doesn't have to be trusted. A Susz file holds structure only, with no hashes and no precomputed facts. Pestka checks every reference, count and offset itself and rejects a file that doesn't add up. Only Pestka can say accepted. If the converter finds the export invalid, the entry rejects it. If it can't convert the export, the entry declines.

Pestka also has a converter of its own, written in Aver, which writes the same bytes. It is slower, so the entries use susz.

mathlib, on an M2 Pro:

	instructions	time	memory
pestka today	1210 G	190 s	6.93 GB
pestka with Susz (pack + check, 4 workers)	1149 G	71 s	6.19 GB
pestka-wasm today	7051 G	507 s	12.95 GB
pestka-wasm with Susz	5813 G	408 s	11.25 GB

Both entries give the expected verdict on every Arena test we have locally: the 183 small tests (in file order and grouped by namespace), the 29 perf/ tests and the 7 large ones, mathlib included.

pestka now runs on four workers (threads: 4). That's how a user runs it, and it is why the wall time drops so much. Over all threads the instruction count is about what it was.

The Arena gives checkers ndjson, and a converter step inside run seemed within the rules; if you'd rather entries didn't do that, Pestka still reads ndjson directly.

[nomeata]

I think it's fair game to do a conversion in the run step.