star: intersect cached FP64 CROWN per-layer bounds into estimateRanges on the approx/relax paths ("CROWN-star")

[ttj]

All paths relative to the nnv repo root; verified on master @ 376568b44. Gated by the relaxFactor=0 ceiling probe issue — build only for categories where the probe shows full-LP tightness decides.

Motivation (measured)

Star.estimateRanges (code/nnv/engine/set/Star.m:1085-1104) bounds each neuron by sign-split V times the predicate box — the constraint polytope Cα ≤ d is invisible, so every triangle-relaxation constraint accumulated by earlier layers contributes nothing to later cheap bounds, and looseness compounds with depth (each relaxed neuron's row becomes an independent [0,ub] box). Meanwhile the engine already computes CROWN-quality FP64 per-layer intermediate bounds and throws them away: gpu_bab_crown_tight returns preL/preU as explicit outputs (code/nnv/engine/nn/gpu_bab/gpu_bab_crown_tight.m:1), and the FC precheck that calls it (run_vnncomp_instance.m:1012 gate) discards them. Intersecting cached per-ReLU-layer preL/preU into the estimate (lb = max(lb_est, preL), ub = min(ub_est, preU)) grows the LP-free zeroing set, shrinks the LP-needing straddler set, and builds relax triangles on CROWN-quality bounds; relaxFactor=1 becomes a zero-LP "CROWN-star". Post-review sizing: +25-50 instances concentrated in cora (residual after the isFC routing fix), plus rung upgrades on dist_shift/tll/challenging (+5-12) and cersyve latency (+1-2). relusplitter expectation is only +0-8 (its 59 unknowns already survived exactly these bounds plus a 50k-node BaB).

Current behavior

• Estimate: Star.m:1085-1104 (silent ±1 default for an empty predicate box at :1091-1096).
• Consumers: approx-star one-shot path LP sites PosLin.m:817 (getMaxs) / :842 (getMins); all relax variants PosLin.m:861-1652; layer-entry prefilter PosLin.m:383-403.
• Oracle source: one FP64 gpu_bab_crown_tight run over the nn_to_ops op list per instance (seconds on FC nets).

Proposed change

At reach setup, run FP64 crown_tight once and cache per-ReLU-layer preL/preU; deliver to PosLin through a hardened per-layer oracle channel; intersect inside the estimate consumers on the approx/relax paths only.

Soundness notes (0-wrong rule) — the delivery channel is the single identified −150 hazard; all five items are mandatory

1. Never key oracle entries by dimension. A naive pop-stack guarded by length(preL)==I.dim is defeated by equal-width consecutive layers (relusplitter nets are literally 784→128→256×3→10). Use layer-ordinal keying with a monotone counter.
2. Arm/disarm hygiene: assert at arm time that #oracle entries == #ReLU layers of the target net; onCleanup disarm on every exit path; NEVER resume a partially consumed oracle after a reach error. A leaked armed oracle into a different net — or into the same-session exact-star closer (dist_shift runs one) — is a concrete wrong-bound → wrong-verdict path.
3. Exact-path fence: assert the oracle is never consulted from reach_star_exact/stepReach. Reach itself returns only safe/unknown through verify_specification (code/nnv/engine/utils/verify_specification.m:49-52), but NN.m PROMOTES unknown→violated under the exact-reach flag (code/nnv/engine/nn/NN.m:529-531, exactness via compute_exact_reach_flag), so a wrong exact-path bound can create a false SAT as well as a false UNSAT.
4. Validity domain: min-of-enclosures is sound only where both enclosures are valid. The CROWN bounds hold for the network's intermediate values over the ROOT input box; restrict intersection to the standard approx/relax pipeline (whose stars' concretizations stay within the root propagation). FP64 only.
5. Globals do not cross parfor workers — the feature silently disarms in parallel branches. That direction is safe (bounds merely stay looser); do not "fix" it by sharing mutable state across workers.

Validation plan

• Adversarial unit: two consecutive equal-width layers + a deliberately mis-armed oracle must trip the arm-time assertion.
• Containment suite (companion test-suite issue) with the oracle armed: sampled outputs contained, relax ⊇ approx nesting preserved.
• Dev-slice verdict diff: new-unsats-only allowed; run with the dist_shift exact closer in-session to prove no leakage; exclude soundnessbench until separately gated.

References

• code/nnv/engine/set/Star.m:1085-1104; code/nnv/engine/nn/funcs/PosLin.m:383-403, :817, :842, :861-1652
• code/nnv/engine/nn/gpu_bab/gpu_bab_crown_tight.m:1; code/nnv/examples/Submission/VNN_COMP2026/run_vnncomp_instance.m:1012
• code/nnv/engine/nn/NN.m:529-531, :1203-1231; code/nnv/engine/utils/verify_specification.m:49-52

---

Part of the star-set methods improvement roadmap (2026-07-01); effort estimate: M.

[ttj]

Blocked by #454 (the relaxFactor=0 ceiling probe) — build only for categories where the probe shows full-LP tightness decides. Alternative (not stacked) approach: #456; pick one per category based on the probe outcome.