Render structured declarations with pinned package dependencies

[williamjblair]

Consumers with already-elaborated declarations should not need to reconstruct source scopes or provide .ilean ranges. Add a source-free schema v2 accepting pinned packages, imports, typed declarations, explicit universe parameters and a nanoda setting.

• Render Challenge, Submission and reducible Solution adapters directly, including dependent definition holes.
• Preserve the v1 wire contract and legacy source renderer.
• Require consumers to validate signatures under their own Lean environment; the generator does not interpret type syntax using another toolchain.
• Use portable OpenSSL SHA-256 digests, with strict digest validation and empty/UTF-8 known-answer tests. GNU sha256sum is no longer required.

Validation at e611b55: lake --wfail build, v1 contract/quoted-module tests, SHA-256 fixtures, and structured integration tests resolving a real Git package and building dependent holes and a polymorphic theorem. The new path needs no source tree, source spans or compiler metadata.

Consumer: google-deepmind/formal-conjectures#5337. Its earlier Linux integration run passed ten fixtures with real Landrun and nanoda, negative proof checks, and all 100 FC100 exports at the previous generator pin. The consumer is being repinned to this hardening commit; the earlier run is not validation of this exact head.

The contract remains experimental until accepted upstream. Pin the source revision and executable digest for operational provenance.