fix(modelchecker): evaluate exists assertions without the retained graph

[jp-fizzbee]

Summary

Fixes the silent false-negative for exists assertions under --experimental_no_graph: they were never evaluated (the post-run CheckSimpleExistsWitness pass needs the retained node list, and the no_graph path returns before it), so an unsatisfiable exists reported PASSED.

Repro (from the bug report):

exists assertion ImpossibleProbe:
    return len(db.appointments) > 999

Command	Before	After
fizz --experimental_no_graph spec.fizz	PASSED ❌	FAILED: Expected states never reached ✅
fizz spec.fizz	FAILED ✅	unchanged

Approach

exists needs a single witness state, ever — not the graph. The processor now OR-accumulates the per-state Witness flags into a run-level matrix as states are discarded, hooked at all four evaluation sites (init, yield, both crash paths). The accumulated signal is the exact same flag the full-graph CheckSimpleExistsWitness pass reads — CheckInvariants sets Witness[i][j] for exists assertions; if this signal were wrong, default mode would have been broken all along.

Mode-appropriate semantics:

• no_graph (exhaustive): missing witness = proof of unreachability → same FAILED verdict + format as full-graph. Skipped for guided traces (same rationale as full-graph path).
• simulation (non-exhaustive): missing witness across all runs = coverage observation → WARNING naming the assertions, with a pointer to model-check for certainty. Intersected across runs. (Explicitly requested behavior; previously exists was silently ignored in simulation.)
• Default full-graph mode untouched.

Regression tests (added per review)

test_references.py now supports an optional flags.txt sidecar per example — read only by the test harness (no CLI or user-facing change; examples without it run exactly as before). This closes a standing harness gap: flagged modes previously could not have automated baselines.

Three new reference examples pin the verdicts:

• 09-10: unsatisfiable exists + --experimental_no_graph → FAILED. Verified to fail against pre-fix code (reports PASSED there — the bug).
• 09-11: satisfiable exists + --experimental_no_graph → PASSED (accumulator detects witnesses, not just failures).
• 09-12: unsatisfiable exists + simulation with fixed seed (deterministic single run) → named WARNING, no failure.

Reference suite: 101/101.

🤖 Generated with Claude Code