Three small hardening items from consuming the generator in google-deepmind/formal-conjectures#4951. None changes contract v1; all came out of an external review of that PR, and the consumer-side halves are already landed there.
1. In-process SHA-256. Contract.lean shells out to sha256sum for the response digests. The utility is GNU coreutils; stock macOS ships shasum but not sha256sum, so the binary works in CI and fails on a contributor's laptop. Hashing in-process removes the only external-tool dependency the generator has.
2. Validate output paths before emitting the response. The response schema constrains path to a string, but nothing constrains it to a safe relative path. A consumer that materialises the file map with directory / path is one generator bug away from writing outside its staging tree. The FC adapter now refuses absolute paths, .././empty components, backslashes and NUL on its side; the same check before emission would make the invariant part of the contract rather than each consumer's caution.
3. A build-identity flag. The binary currently takes no flags — main accepts stdin or a single request path. A consumer pinning a revision in its lock has no way to ask the binary what it is; LEAN_EVAL_GENERATOR_BIN can point at anything that returns schema-shaped JSON. Something like:
lean-eval-generator --build-info
{"repository": "leanprover/lean-eval-generator", "commit": "...", "contractVersions": [1]}
would let the adapter verify the binary against tools.toml before generating.
For context: formal-conjectures#4951 pins 77373a5 — the same revision lean-eval pinned in leanprover/lean-eval#553 — and its seam test round-trips the emitted request through the binary byte-for-byte. Happy to send a PR for any or all three if that's easier than doing it yourself.
Three small hardening items from consuming the generator in google-deepmind/formal-conjectures#4951. None changes contract v1; all came out of an external review of that PR, and the consumer-side halves are already landed there.
1. In-process SHA-256.
Contract.leanshells out tosha256sumfor the response digests. The utility is GNU coreutils; stock macOS shipsshasumbut notsha256sum, so the binary works in CI and fails on a contributor's laptop. Hashing in-process removes the only external-tool dependency the generator has.2. Validate output paths before emitting the response. The response schema constrains
pathto a string, but nothing constrains it to a safe relative path. A consumer that materialises the file map withdirectory / pathis one generator bug away from writing outside its staging tree. The FC adapter now refuses absolute paths,.././empty components, backslashes and NUL on its side; the same check before emission would make the invariant part of the contract rather than each consumer's caution.3. A build-identity flag. The binary currently takes no flags —
mainaccepts stdin or a single request path. A consumer pinning a revision in its lock has no way to ask the binary what it is;LEAN_EVAL_GENERATOR_BINcan point at anything that returns schema-shaped JSON. Something like:would let the adapter verify the binary against
tools.tomlbefore generating.For context: formal-conjectures#4951 pins
77373a5— the same revision lean-eval pinned in leanprover/lean-eval#553 — and its seam test round-trips the emitted request through the binary byte-for-byte. Happy to send a PR for any or all three if that's easier than doing it yourself.