v0.2.4

lean-rs-host honors subDir for git dependencies when building the .olean search path

LakeProject::olean_search_paths enumerates each lake-manifest.json package into a .lake/build/lib/lean search-path
entry. It honored the dir field of path dependencies but ignored the subDir field that Lake records for a git
dependency declared with the subdirectory form (require «pkg» from git "url" @ "tag" / "sub"). Lake checks such a
package out to <packagesDir>/<name>/<subDir>, so dropping subDir pointed the search path at the repo root instead of
the package and the package's modules became unreachable (unknown module prefix '...' at import time). The enumeration
now appends subDir when present, so git-subdirectory dependencies resolve. This also fixes the same import failure when
the search path is built for an out-of-process worker, since the worker child resolves imports through the same
LakeProject enumeration.

v0.2.3

lean-rs-abi is purely static; toolchain probing moves to the crates that link or discover Lean

lean-rs-abi no longer has a build script. Previously its build.rs probed an installed Lean toolchain (hashing
lean.h, reading the version) and panicked when none was found, so a crate documented as "link-free metadata" could not
be built by any pure-Rust consumer without a Lean toolchain on PATH (or DOCS_RS=1) — which kept downstream Rust-only
CI red. The crate is now purely static: the SUPPORTED_TOOLCHAINS window, REQUIRED_SYMBOLS, and the lean.h layout
literals, with no probe.

The live toolchain identity it used to bake (LEAN_VERSION, LEAN_RESOLVED_VERSION, LEAN_HEADER_PATH,
LEAN_HEADER_DIGEST) moves to the crates that legitimately have a toolchain at build time:

• lean-rs-sys (which links libleanshared) now bakes these from its own build script and exposes them at the same
  paths (lean_rs_sys::LEAN_VERSION, lean_rs_sys::consts::*).
• lean-toolchain (the discovery crate) now bakes them in its own build.rs and re-exports them at the same paths
  (lean_toolchain::LEAN_VERSION, …). Its probe degrades to the latest supported window entry when no toolchain is
  present instead of failing, so link-free downstream crates (and docs.rs) build with no Lean installed. It still
  fails the build when an installed toolchain's lean.h is outside the supported window.

lean_rs_abi::LEAN_VERSION, LEAN_RESOLVED_VERSION, LEAN_HEADER_PATH, and LEAN_HEADER_DIGEST are removed; consume
them from lean-rs-sys or lean-toolchain instead. No other public API or layout change.

v0.2.2

Supported Lean toolchain window: add 4.31.0-rc2

Lean 4.31.0-rc2 ships a byte-identical lean.h to 4.31.0-rc1, so it joins the same ABI-equivalence entry in
SUPPORTED_TOOLCHAINS and becomes the new head of the supported window (now 4.26.0 through 4.31.0-rc2). No public API or
layout change; the workspace test suite passes against rc2 on the local toolchain sweep.

Release recovery covers all publishable crates

The release-recover.yml recovery workflow now walks every publishable crate in dependency order, so a partial publish
that stalls on any crate—not just the tail—can be completed without burning a version.

v0.2.1

lean-toolchain: explicit capability manifest dependencies

CargoLeanCapability can now record caller-provided LeanLibraryDependency entries in the capability artifact
manifest. Downstream build scripts that build a primary Lake shared library against another packaged Lean shared library
can describe that dependency before the manifest is written, instead of editing JSON after build_quiet() returns. This
is domain-neutral: source ownership, package names, module names, and export metadata still live in the downstream
package that owns the Lean payload.

lean-toolchain: shared source-package materialization

lean-toolchain now exposes a domain-neutral source-package materializer for crates that ship Lean source payloads and
need to build them under a caller-selected toolchain. The helper owns the repeated cache mechanics: digest-keyed cache
entries, per-entry file locks, atomic temp-directory installation, generated lean-toolchain files, provenance
sidecars, generated-file validation, and explicit Lake manifest policy. It hides the copy/cache protocol behind one
request type so downstream crates do not hand-roll sibling-checkout discovery or racy .lake reuse.

lean-rs-interop-shims: release-shaped package surface

The package-owned lean-rs-interop-shims crate now uses the shared materializer, ships its license texts explicitly,
and has a package-list regression proving the Lean/C/Lake runtime payload and licenses are present while Rust crate
scaffolding is not copied into materialized Lake roots. lean-rs-host's parity guard now compares the runtime payload
only, so the canonical package can carry Rust packaging files without forcing the host's bundled Lean payload copy to
mirror them.

v0.2.0

This is a breaking release (pre-1.0, so a minor bump). The worker wire protocol moved from PROTOCOL_VERSION 8 to 10,
several LeanWorkerError variants gained fields and boxed an existing one, and Request::OpenHostSession /
Response::HostSessionOpened gained fields — a parent and child built from different 0.x lines will refuse to
handshake. Rebuild the whole worker stack from one version. lean-toolchain's DiscoverOptions also gains a field
(allow_lean_sysroot_env, see below). The headline theme is bounded, observable imports: every
host session now reports what it loaded and how much memory that cost, the pool can refuse imports that would breach an
RSS budget, and resource exhaustion surfaces as structured facts instead of an opaque failure.

New crate: lean-rs-abi (link-free Lean ABI and toolchain metadata)

The link-free Lean 4 ABI constants and toolchain-fingerprint metadata that previously lived in lean-rs-sys now live in
a new published crate, lean-rs-abi, which carries no link dependency on liblean. lean-rs-sys glob-re-exports
lean_rs_abi::consts::* and lean_rs_abi::supported::*, so existing paths such as lean_rs_sys::consts::LEAN_ARRAY,
lean_rs_sys::SUPPORTED_TOOLCHAINS, and lean_rs_sys::SupportedToolchain keep resolving unchanged; the items are simply
defined one crate deeper. Build tooling that needs the digest window or ABI tags without linking Lean can now depend on
lean-rs-abi directly. (cargo public-api cannot enumerate a cross-crate glob, so the lean-rs-sys baseline now renders
these as pub use …::<<lean_rs_abi::…::*>> rather than item-by-item; the public surface is unchanged.)

lean-toolchain: an explicit sysroot no longer leaks ambient LEAN_SYSROOT

DiscoverOptions gains an allow_lean_sysroot_env flag, completing the per-probe gating set. Previously the
LEAN_SYSROOT environment probe ran unconditionally, so passing an explicit (or deliberately invalid) sysroot still
fell back to an ambient LEAN_SYSROOT — contradicting explicit_sysroot's documented "probed first, ambient disabled"
contract. The build helpers now clear this flag whenever an explicit sysroot is set, so an explicit sysroot is the only
source. Default leaves it enabled, preserving the previous discovery order for callers that do not narrow the probe
set. This is the field that surfaced as a CI-only failure (CI exports LEAN_SYSROOT); local runs without it were
unaffected.

lean-rs-host: session import profiles bound what a session loads

New LeanSessionImportProfile (Private, Server, ExportedPublic, FullPrivateCompat) and the lower-level
LeanImportLevel / LeanImportProfileMode let a caller pick how much of a module's import closure a session pulls in,
instead of always importing everything. LeanCapabilities::session_with_profile(...) and
SessionPool::acquire_with_profile(...) open a session under a chosen profile; the existing session(...) /
acquire(...) keep the full-import behavior. On the wire this adds import_profile to Request::OpenHostSession
(part of the PROTOCOL_VERSION bump). Profiles default to the full-compatibility behavior, so an unset profile imports
as before.

lean-rs-host: import statistics and compact-region memory attribution

Every opened session now records a LeanImportStats (LeanSession::import_stats()), reporting effective module count,
imported byte and constant counts, extension counts, and per-region memory attribution split into memory-mapped,
non-memory-mapped, and compacted-region bytes/counts. LeanImportStats::memory_diagnostic() renders a human-readable
summary. LeanCapabilities::profiling_session(...) plus LeanImportProfilerOptions (profiler, trace_profiler,
trace_profiler_output) opt into Lean's import profiler for a one-off measured open. The stats ride the protocol as
import_stats on Response::HostSessionOpened and on the bracketed-import result (below), and are mirrored by
lean-rs-worker-protocol's LeanWorkerImportStats.

lean-rs-host: session-pool memory policy bounds import admission

SessionPoolMemoryPolicy lets a pool refuse work that would breach a memory ceiling: max_rss_kib(...) caps process
RSS and max_fresh_imports(...) caps how many fresh import-bearing sessions may be admitted, with disabled() for the
previous unbounded behavior. SessionPoolConfig (and SessionPool::with_config / with_memory_policy) thread the
policy in, and SessionPool::memory_policy() reads it back. When the policy refuses admission the caller gets a
resource-exhausted error (below) rather than an OOM abort.

Resource exhaustion is now a structured, honest diagnostic

Memory- and admission-pressure failures surface as facts instead of an opaque error. lean-rs gains
ResourceExhaustedFacts (cause, current/limit RSS, import counts and limits, whether work entered Lean, last import
stats), reachable via HostFailure::resource_exhausted_facts(), plus a HostStage::Resource stage and a
LeanDiagnosticCode::ResourceExhausted code. lean-rs-worker-protocol carries the richer LeanWorkerResourceExhaustedFacts
(adding operation, queue-wait and duration timing, worker generation, cold-open and import-like admission counters, and
restart reason). Breaking: several LeanWorkerError variants (Timeout, Cancelled, RssHardLimitExceeded,
WorkerPoolExhausted, WorkerPoolMemoryBudgetExceeded, WorkerPoolQueueTimeout) gained a boxed resource field, and
the existing last_import_stats field on the RSS/budget variants is now boxed (Option<Box<LeanWorkerImportStats>>);
read them through the new LeanWorkerError::resource_exhausted_facts() accessor.

lean-rs-worker-parent: session-reuse key diagnostics

LeanWorkerPoolSnapshot gains counters that make warm-session reuse auditable: key_hits, key_misses,
distinct_keys_seen, last_key_miss_reason, import_like_requests, and the cold-open accounting
(cold_open_attempts, cold_open_admitted, cold_open_refusals, concurrent_cold_opens_observed,
fresh_cold_opens_avoided). The host side exposes the same classification as SessionPoolKeyMissReason. These make it
possible to tell whether a workload is fragmenting the session-reuse key and paying for avoidable cold opens.

lean-rs-worker-parent: worker-replacement latency is measured

LeanWorkerReplacementTiming plus the last_replacement_timing, last_capability_load_elapsed,
last_first_command_elapsed, and last_replacement_skipped_reason fields on the pool snapshot record how long it takes
to stand up a replacement child (capability dylib load and first command) so replacement cost shows up in diagnostics
instead of as unexplained latency.

Bracketed lightweight import queries and batched warm module queries

The host gains a bracketed import path (LeanBracketedImportResult, carrying its own import_stats) for lightweight
module queries that do not need a full session, and the worker exposes
LeanWorkerSessionLease::process_module_query_batch(...) (LeanWorkerModuleQuerySelector →
LeanWorkerModuleQueryBatchOutcome) so a warm child can answer a batch of module queries in one round trip instead of
one command each.

Derived-work observability (LeanWorkerDerivedWorkFacts)

Declaration inspection and proof-search results now attach LeanWorkerDerivedWorkFacts, counting the derived work a
query triggered: parser/elaborator runs, pretty-prints, raw type renderings, docstring lookups, source-range lookups,
simp-extension lookups, module-snapshot builds, proof-search fact collections, and whether lazy discrimination-tree
import initialization was observed. Proof-search facts are gated by a new proof_search inspection field and report
computed / unavailable_reason, so a caller can tell eager from skipped derived work and avoid paying for it
needlessly.

lean-rs-worker-parent: capability sessions can import an external Lake workspace

LeanWorkerCapabilityBuilder::import_workspace_root(...) lets a manifest-backed worker capability load its dylib from
the capability project while opening the host session against a separate audited Lake workspace. The import root is one
Lake project and its manifest-declared dependency closure; it is not merged with the capability project's search path,
so capability dependencies cannot shadow the audited workspace's dependencies. The unset path keeps the previous
behavior (project_root is also the import root). Consumers whose capability project and target workspace differ must
set this override explicitly.

Capability exports that import modules must rely on the host-installed search path. They must not call
Lean.initSearchPath or reconstruct the search path from LEAN_PATH, because that would reset Lean's search path and
discard the selected import workspace root.

The worker-pool session key now includes the canonical effective import workspace root, so repeated audits of the same
workspace reuse the warm child session while different audited workspaces do not alias. The integration fixture records
the external-root workload, platform, module counts, cold first-lease cost, warm second-lease cost, worker count, warm
lease count, and import counter; warm same-workspace commands attach to the already-open child session instead of
reopening imports. This is parent-side only: OpenHostSession.project_root already existed on the wire, so
lean-rs-worker-protocol, lean-rs-worker-child, lean-rs-host, the Lean shims, and PROTOCOL_VERSION are unchanged.
The pool intentionally keeps one worker entry per compatible capability/import-workspace session for now; reusing one
loaded capability child across many target workspaces is deferred until a named workload measures dylib reload or worker
churn as the bottleneck.

v0.1.20

Pristine-entry proof position (ProofPositionSelector::Entry)

• New Entry proof-position selector — the goal state before any tactic runs. proof_state already exposed the
  pristine entry goal as the goals_before of the first position, but try_proof_step could only splice a candidate
  after the first tactic, so a from-scratch tactic block (e.g. intro …; exact …) read from goals_before ran with
  the first binder already introduced and failed. Entry anchors on the first tactic's pre-state and splices the
  candidate before the first tactic (aligned to its column, never dedented to a top-level command), so a from-scratch
  block elaborates against the untouched goal and the original tactics' downstream errors are reported as downstream,
  not candidate-local. For proof_state, Entry renders goals_before == goals_after. The variant is additive on the
  #[non_exhaustive] LeanWorkerProofPositionSelector (wire) and ProofPositionSelector (host); Index { index }
  keeps its existing "index-th tactic state" meaning. See docs/architecture/info-tree-projection.md.

Worker robustness: no verify crash, honest degraded verdict, pretty proof-state locals

A heavy verify_declaration / proof_state workload run against a RED module while the worker thrashed against its RSS
cap surfaced three defects in the read-only query path; all three are fixed.

• verify_declaration no longer aborts the child on a proof state degraded by memory pressure. The
  Lean.MetavarContext.getDecl … unknown metavariable panic on the proof-state walk is an uncatchable abort() under
  the child's LEAN_ABORT_ON_PANIC=1, so it is contained at two layers. The shim screens a captured proof state for
  dangling metavariables with the total MetavarContext.findDecl? (never the pure-panic! getDecl) before any
  renderer dereferences it, rendering a degraded goal as <goal unavailable: elaboration degraded under resource pressure> and routing the verdict to BudgetExceeded with axioms_available = false. As an authoritative backstop
  for any residual transitive-mvar abort, the supervisor maps a ChildPanicOrAbort during a verify / query-batch
  request to a synthesized degraded verdict (verify → BudgetExceeded with unavailable facts; batch → per-selector
  BudgetExceeded) and records a child_abort restart, so the caller always gets a verdict and the next call is served
  by a fresh child.
• verify_declaration no longer returns NotFound for a valid lemma degraded by memory pressure. The Lean shim
  reclassifies a notFound whose diagnostics carry a resource marker (deep recursion, interrupted, out of memory) to
  timeout / BudgetExceeded, and the worker child taints a non-positive verdict (never Accepted) to BudgetExceeded
  when its post-job RSS is at or above an internal, default-off ceiling. A clean name-absent query on a healthy worker
  still returns NotFound.
• proof_state.locals now render pretty and notation-aware, through the same delaborator as goals_before /
  goals_after, instead of raw Expr.toString (_uniq.NNNN, ~6 KB/decl — the proximate RSS-spike trigger). A new
  additive locals_raw: bool field on the ProofStateInDeclaration selector (#[serde(default)], default false)
  restores the raw form on request. The verify path and the try-proof-step goals path, which read only goals_after,
  now render no locals at all.

No new verification-status variant or protocol version bump: BudgetExceeded is reused for the degraded case and
locals_raw is backward compatible via #[serde(default)]. The internal env var LEAN_RS_VERIFY_RSS_TAINT_KIB
(plumbed from the pool's per-worker RSS ceiling) gates the child-side taint and defaults to off. See
docs/architecture/info-tree-projection.md for the degraded-verdict
semantics and locals rendering modes, and
docs/architecture/06-panic-containment.md for the supervisor
verdict-on-abort contract.

v0.1.19

Bounded module-query cost on an incomplete import closure

A module query (verify_declaration, proof_state, find_references, batched selectors) against a file whose import
closure is incomplete (MissingImports) no longer elaborates the body. With the imports absent the environment lacks
the file's symbols, so a full elaboration only produced unknown-symbol errors whose projection the caller already
discards as a needs_build / files_skipped degrade. The Lean shim now short-circuits to an empty projection with
elaboration_micros = 0, bounding each per-file query in a project-scope scan to header parsing instead of a full
failing elaboration. No protocol or API change; the MissingImports outcome and missing list are unchanged. The
remaining cross-query cost on a large scan — cold header re-import after an RSS-driven worker cycle — is documented in
docs/architecture/info-tree-projection.md with its mitigations
(limit, or build the project first).

Worker robustness: read-only resolution queries inside the panic boundary

A field re-evaluation recorded a one-off child abort (Lean.MetavarContext.getDecl … unknown metavariable → SIGABRT)
during a genuine-ambiguity verify_declaration. A faithful deterministic reproduction on the same toolchain (two open
namespaces exporting the same short name, a bare reference forcing Lean's ambiguous-overload error, the offending message
rendered) does not abort the child: the verdict resolves with both candidates and the supervisor performs no restart.
The abort was therefore incidental metavar churn, not a defect of the resolution path. A regression test pins the
no-restart invariant, and docs/architecture/06-panic-containment.md
records why a read-only query is still inside the process panic boundary (a Lean panic! under LEAN_ABORT_ON_PANIC=1
is uncatchable across the FFI, and relaxing it would let a defaulted value masquerade as a real verdict).

v0.1.18

Honest resolution verdicts on the worker query surface (protocol 7 → 8)

The worker's source-snapshot query path (verify_declaration, proof_state) now reports why a name failed to resolve
as a typed verdict instead of an infrastructure-flavoured string. LeanWorkerProofStateResult gains
Ambiguous { candidates } and NeedsBuild { missing }; Unavailable { message } is retained only for genuine
non-resolution failures (no proof position matched the selector, snapshot inconsistency), which are not resolution
verdicts. LeanWorkerDeclarationVerificationStatus gains NeedsBuild (its outcome is the existing
MissingImports { missing }, which already names the absent modules — no new field). These replace the previous
behaviour where an unresolved name in an incomplete environment surfaced as Unavailable { "declaration name is ambiguous in the module" } or as Ambiguous with no candidates. The verdict is classified once in the Lean shim at the
source-resolution boundary and mapped onto each result, so the rule the consumer applies is purely structural:
≥ 2 candidates ⇒ ambiguous, else needs_build. Env-based resolution (inspect_declaration, find_references, search)
is unique by construction and keeps no ambiguity variant.

Structural candidates for genuine ambiguity

LeanWorkerDeclarationVerificationFacts gains candidates: Vec<LeanWorkerDeclarationTargetInfo> (#[serde(default)]),
populated only when the status is Ambiguous (target stays None then). A candidate carries namespace_name as the
disambiguator; no module field is added because source-snapshot candidates have no loaded module (it would be None
everywhere). Behind this, the Lean shim deduplicates resolution candidates by declaration name before the
arity decision, so a once-defined declaration in a module / @[expose] public section file resolves cleanly instead
of spuriously reporting Ambiguous against identical copies of itself.

Real axiom collection with a typed availability flag

verify_declaration with report_axioms: true now runs an actual Lean.collectAxioms walk over the resolved
declaration in the elaborated environment (heartbeat- and byte-bounded), replacing the previous textual heuristic that
returned ["sorryAx"] iff the source mentioned sorry/admit and otherwise []. LeanWorkerDeclarationVerificationFacts
gains axioms_available: bool (#[serde(default)]): true with axioms: [] means the walk ran and found no
nontrivial axioms; false means the walk could not run (target unresolved, budget exhausted). This defines the
misleading empty list — which conflated "checked, none" with "never checked" — out of existence.

Pretty, notation-aware inspection statements

LeanWorkerDeclarationInspectionFields gains rendering: LeanWorkerRendering (default Pretty), and
LeanWorkerDeclarationInspection reports the path actually used via statement_rendering: Option<LeanWorkerRendering>.
Under Pretty the statement is rendered with Lean.PrettyPrinter.ppExpr (notation on, pp.universes false) instead of
the raw fully-elaborated Expr.toString; on exception or heartbeat exhaustion it falls back to the raw form and reports
Raw. The rendering knob is confined to inspection — it is not added to the shared LeanWorkerRenderedInfo, which would
over-expose every consumer (goals, type-at) for a knob only inspection uses.

v0.1.17

Version-range cfg flags for per-toolchain gating

lean-rs-sys's build script now emits a monotone lower-bound cfg family alongside the existing exact-version
lean_v_<token> flag: lean_at_least_<major>_<minor> is set for every supported-window minor at or below the resolved
toolchain (release candidates count as their target minor, so 4.31.0-rc1 ⇒ lean_at_least_4_31). Downstream code can
gate a symbol introduced in a given release with #[cfg(lean_at_least_4_31)] and the older path with
#[cfg(not(lean_at_least_4_31))], rather than OR-ing exact-version tokens. The script also emits rustc-check-cfg for
every version token and minor boundary the window spans, so gating on a non-active version stays lint-clean under
-D warnings; only boundaries within the window [floor ..= head] are registered.

Re-export the supported-window query API from lean-toolchain

lean-toolchain now re-exports SUPPORTED_TOOLCHAINS, SupportedToolchain, supported_for, and supported_by_digest
from lean-rs-sys, alongside the existing LEAN_VERSION / LEAN_HEADER_DIGEST / required_symbols() surface. This
lets a consumer answer "is this pin inside the supported window?" and "does this lean.h digest match a known
toolchain?" through the non-FFI facade, without a direct lean-rs-sys dependency (which carries link directives).

Guarded the bundled interop shim copy against drift

lean-rs-host's bundled lean-rs-interop-shims is now a verbatim copy of the canonical package under
crates/lean-rs/shims/lean-rs-interop-shims. The host copy had silently drifted — it was missing
LeanRsInterop.Worker.Stream (the worker row-streaming helpers), which had been added to the canonical copy alone. The
host copy is meant to be the full generic package, not a host-trimmed subset (it already carried Callback.String,
which the host policy shims also do not import), so the missing module was negligent drift, not design. Worker.Stream
is added to the host copy, and a new interop_shims_parity test asserts the two copies are byte-identical so they
cannot diverge again. The duplication itself is structural — a published crate's Cargo.toml include cannot reach
into another crate's directory, so each crate vendors its own self-contained copy.

Removed the obsolete lake/ shim package mirror

Deleted lake/lean-rs-host-shims and lake/lean-rs-interop-shims. These were the standalone Lake packages from the
original hybrid layout (v0.1.0), back when downstream consumers required the host shims over git. Once the shim
packages were bundled into the lean-rs and lean-rs-host crates — shipped via each crate's Cargo.toml include and
built on demand by the Rust loader — the lake/ copies became an unreferenced mirror that had drifted stale (they never
received the string-callback C path). Nothing in the build, tests, fixtures, or current docs referenced them. The
authoritative copies remain under crates/lean-rs/shims/lean-rs-interop-shims,
crates/lean-rs-host/shims/lean-rs-interop-shims, and crates/lean-rs-host/shims/lean-rs-host-shims.

Lean 4.31.0-rc1 added to the supported window

leanprover/lean4:v4.31.0-rc1 is now a supported and CI-tested toolchain (new lean.h digest; layout and
REQUIRED_SYMBOLS probes both clean, no missing symbols), and is promoted to the CI/release/sanitizer head. The
supported window is now 4.26.0 through 4.31.0-rc1.

Adopting rc1 also fixed a latent bug in the host "attempt proof" shim, surfaced by Lean 4.31's stricter tactic-block
indentation enforcement. When a candidate tactic was spliced into an existing proof, the bare by keyword atom could be
selected as the insertion position and the candidate indented from an unrelated line, emitting it at column 0 — accepted
leniently by Lean ≤ 4.30 but rejected as a parse error by Lean ≥ 4.31. The shim now models a selected proof position as
a type that, by construction, is a real tactic at a positive source column, and derives the candidate's indentation from
that tactic's own column, so insertion aligns with a sibling tactic the parser already accepted. This makes the host's
bounded proof-attempt path behave identically across the supported window.

Structured worker declaration search

lean-rs-worker-protocol replaces the 0.1.16 declaration-search request/row shape with a structured bounded search
surface: name contains/suffix matching, kind filters, required-constant filters, conclusion-head filters, namespace or
module scope biasing, deterministic scores/ranks, compact declaration flags, and fanout/timing facts. Search remains
metadata-only from the caller's perspective and does not render declaration type text; use the existing single-name
declaration-type query for explicit bounded rendering.

v0.1.16

Checked export signatures and host boundary tightening

Breaking pre-1.0 change: direct Lean export lookup is now split into a safe checked capability path and an explicit
unsafe unchecked module path. LeanCapability::exported validates the requested Rust ABI shape against trusted
manifest signature metadata before dispatch, while arbitrary raw symbol lookup moves to
unsafe LeanModule::exported_unchecked. The low-level function-address constructors and raw library symbol resolvers
are no longer public API.

CargoLeanCapability manifests now use schema version 2 and can record export signatures. The workspace also exposes
the public signature-description types (LeanExportSignature, LeanExportAbiRepr, ownership/result-convention
metadata, and related values) so downstream build scripts and capability loaders can describe the checked boundary
without duplicating Lean ABI knowledge.

Worker capability dispatch now uses those checked signatures for the closed operation shapes shared by parent, child,
and harness. lean-rs-worker-parent re-exports the newer module-query, declaration-search, proof-state, cache, and
budget result types, and the parent/protocol crates now forbid unsafe code.

Worker module snapshots and declaration lookup

Worker module processing gains a module snapshot cache and bounded declaration lookup surfaces for repeated query
workloads. The new query/result types expose cache status, timings, declaration summaries, target-info results, and
output-budget controls while preserving bounded responses for large modules.

Lean object decoding and progress callbacks

lean-rs adds safe Lean object view helpers for scalar/sum/constructor decoding and a dedicated
LeanProgressCallback wrapper for progress callback ABI plumbing. Host-side decoders were migrated onto these safe
views, and lean-rs-host no longer contains unsafe code.