Consumer-side hardening: in-process SHA-256, output-path validation, --build-info

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.

Start with Contract.lean for response digest generation and main for stdin, request-path, and flag handling; inspect tools.toml and the seam test context for the build identity expected by consumers. Done means hashing no longer depends on sha256sum, emitted paths reject the listed unsafe forms, and --build-info reports the repository, commit, and contract versions.