Completeness variant of circuit_proof_start for large compositions

[mitschabaude-bot]

For a parent circuit composing several verified subcircuits, circuit_proof_start's one-shot simp only [circuit_norm, h_input, ...] at h_env can produce a rewrite cast the kernel cannot re-check: (kernel) deep recursion detected at the theorem header as soon as h_env is referenced.

The manual recipe that works (used in the Orchard scalar-mul entry circuit):

1. circuit_proof_start_core
2. dsimp only [main, circuit_norm] at h_env (definitional, so no cast)
3. bind each conjunct with have hX := h_env.2.….1 projections (an obtain re-embeds the giant tail in every casesOn motive — also kernel-fatal)
4. clear h_env
5. simp only [circuit_norm, h_input, <child circuits>] on each small component separately — each per-component cast is kernel-checkable.

It would be valuable to have a circuit_proof_start variant (or a flag) that applies this dsimp-then-project-then-per-component strategy to h_env automatically.

Notes:

• The recently-landed struct-level completeness obligations (Witgen IR framework improvements (all of #402 except Clean/Orchard) #413) reduce h_env pressure considerably, so the cliff now hits later — but very large parents still sit on it.
• Even with the manual recipe, a big enough parent stays on a kernel size cliff; the durable fix is subcircuit boundaries (now documented in AGENTS.md and doc/performance-problems.md). This issue is about making the intermediate regime workable without manual surgery.

(Extracted from the retired doc/circuit-proof-friction.md feedback list.)

🤖 Generated with Claude Code