Rust LSP: rebaseline per-kit scope for lift/materialize/emit/prove parity

[TSavo]

Gap

Rust has an older LSP forward-propagation issue (#313), but the four-kit parity audit needs a broader per-kit LSP rebaseline. LSP is not just the forward-prop demo; it is the editor-facing consumer of lift/materialize/emit/prove state.

Boundary rule

Rust parsing and source-position mapping are Rust kit work, even though the CLI is also written in Rust. The LSP server/daemon may coordinate normalized data, verifier queries, receipts, and diagnostics, but it must not put Rust language parsing into CLI-owned logic. The Rust LSP path must use Rust-kit-owned parsing/lift surfaces and speak RPC.

Scope to rebaseline

Define the Rust LSP parity slice for the same route the CLI proves offline:

• lift: Rust parser recognizes #[provekit::boundary], #[provekit::sugar], callsite/test assertions, and returns normalized IR plus ranges/diagnostics.
• mint/prove: normalized contract/callsite data feeds shared bridge/prove computation.
• materialize: editor surface can show whether a boundary/sugar site has a resolvable Rust-kit materialization route or a refusal.
• emit: editor surface can show cargo-test emission availability/status without owning cargo-test semantics.
• prove: diagnostics/lenses reflect real non-vacuous claim status, not totalClaims: 0 green.

Acceptance criteria

• Write the Rust LSP scope matrix for lift/materialize/emit/prove/LSP interaction.
• Reconcile this ticket with the older forward-propagation issue [kit:rust][lsp] forward-propagation loop #313; keep [kit:rust][lsp] forward-propagation loop #313 as child work if still correct.
• Identify which existing Rust LSP/plugin code is current vs stale/demo-only.
• Open child implementation issues for missing Rust LSP pieces instead of stuffing all work into this ticket.
• Confirm the Rust LSP path uses Rust-kit parser/source ranges, not CLI-owned Rust source parsing.
• Confirm any check/emit status delegates to Rust kit RPC instead of hardcoded cargo logic.
• Add at least one integration fixture requirement for open/change source -> diagnostics/lens output.

Related

• Existing Rust LSP forward-prop issue: [kit:rust][lsp] forward-propagation loop #313
• Parent LSP epic: [epic] LSP forward-propagation loop — undeniable-value demo for v1.0.0 #308
• Substrate overlay: LSP substrate overlay: hover / inline hints / code lens / diagnostics #664
• Four-kit parity tracker: Tracker: materialize/lift/emit/prove/LSP parity gaps by kit #1486
• Rust materialize boundary leak: Rust materialize: remove Rust source parsing/carrier injection from CLI path #1494
• Rust emit gap: Rust emit: wire cargo-test emitter into CLI dispatch and project registration #1493