Engine: remove recursive storage reads in diagnostics and proofs #166

Problem

Program execution holds a storage read guard and diagnostics acquire another read guard before releasing it. With a writer queued between those reads, the recursive acquisition can deadlock. Fix the lock boundary separately from richer diagnostics and proof indexing.

Evidence

Source: 5c1f313379a5cb2995a43a66ddba0b5cc9798b7f (inspected 2026-10-03). These are source findings; the acceptance scenarios below still need implementation and execution.

• src/protocol/handler.rs:2388: execute_program_sync retains its outer storage read guard.
• src/protocol/handler.rs:3481: Debug reacquires storage.read().
• src/protocol/handler.rs:3507: Why enters why_query before the outer guard is dropped.
• src/protocol/handler.rs:498: why_query acquires its own storage read guard.

Acceptance criteria

• Pass the existing guard or an immutable snapshot through diagnostic preparation; release storage before expensive proof evaluation.
• Audit .why, .why full, .why not and index/debug helper paths for the same pattern without making the lock recursively permissive.
• Use deterministic barriers to queue a writer between the outer read and diagnostic entry; all operations complete and concurrent writes make progress.
• Keep structured explain output in inputlayer/inputlayer-symbolic#169 and indexed proof responsiveness in .why: no KG deep copy, indexed subgoal proofs, release storage guard #134; this fix alone closes neither broader issue. Concurrent query/write/delta latency passes Performance: baseline and mandatory pre-PR regression pipeline #163.

Delivery

Plan item: S06. R1 - Safety + perf/e2e gates.

Dependencies / related work: #163.