schema_version

integer

Always 1 for v1 rows.

kind

string

"parametric" or "fixed". Readers MUST reject a row whose kind mismatches the expected kind for the parser.

function

string

Fully-qualified Lean name of the registered benchmark.

total_nanos

integer

Wall time in nanoseconds for the measured work.

status

string

One of "ok", "timed_out", "killed_at_cap", "error".

param

integer

Ladder parameter the function was invoked with.

inner_repeats

integer

Auto-tuned inner repeat count. 0 on synthesized error rows.

repeat_index

integer

0-based index across the configured repeats.

result_hash

string | null

Hex-prefixed 0xDEADBEEF literal (case-insensitive). null when the function's return type lacks Hashable.

error

string | null

Free-form message for status == "error". null otherwise.

env

object | null

Reproducibility metadata captured at child startup — see the Environment metadata section below. Emitted on every row by current writers.

alloc_bytes

integer | null

Total bytes allocated by the Lean runtime over the child's lifetime. Always null today — Lean 4 has no portable in-process API to read this. The key is reserved so the field can land additively when a future Lean release exposes allocation counters.

peak_rss_kb

integer | null

Peak resident-set size of the child process, in kibibytes (1024 bytes). On Linux read from /proc/self/status (VmHWM:); null on macOS, Windows, and any other platform without /proc.

per_call_nanos

number | null

total_nanos / inner_repeats precomputed. Derived; readers MAY recompute it from total_nanos and inner_repeats when absent. Emitted as null on synthesized error / killed-at-cap rows where inner_repeats == 0 (a real division-by-zero), to keep every emitted row valid JSON.

cache_mode

string

"warm" (auto-tuned inner repeats inside one child, the v0.1 default) or "cold" (single untuned invocation; the parent respawns the child for every ladder rung). See the Cache-modes section of the Advanced page.