evaluator: add optional ChoiceSource injection to Rand

[bkchr]

Motivation

Rand is the single point through which the evaluator draws nondeterministic choices: all five call sites (actionAny, oneOf, and nondet selection) route through Rand::next / Rand::next_biguint. Today those draws come from an internally seeded PRNG, which limits what can be done with a run after the fact:

• External replay. A run can be reproduced byte-for-byte by replaying the recorded sequence of choices through the same seam, independent of the PRNG seed or the evaluator version.
• Deterministic debugging. A specific execution path can be reproduced without relying on a fixed seed, which is fragile across spec and evaluator changes.
• Model-based testing. The evaluator can be driven down a chosen path by supplying a handcrafted sequence of choices, exercising invariants along that path.

This PR adds a small, additive seam for those use cases. Downstream consumers (fuzzing, exhaustive enumeration of choice sequences, symbolic guidance) can build on it without any change to the evaluator itself.

Non-breaking fallback

When no ChoiceSource is installed, the evaluator behaves exactly as before: Rand differs only by a None-valued field, and both draw methods take their original code paths verbatim. This was verified empirically rather than asserted: two binaries, one linking pristine 6fb2924e and one linking this branch, generated the same fixed-seed sequence of next() and next_biguint() draws — including bounds exceeding u64::MAX, which exercise the internal large-BigUint path — and produced byte-identical output.

Tests

Five new tests in evaluator/tests/choice_source_tests.rs:

• tape_delivers_values_in_order — a tape of [2, 0, 1, 7] is returned verbatim by next (values are forwarded, not reduced or transformed).
• no_source_counter_advances_by_one_per_draw — without a source, the counter advances by exactly 1 per draw (no-regression gate).
• with_source_counter_still_advances — with a source, the counter still advances per draw, keeping get_state() monotonic for simulator statistics.
• action_any_consumes_n_draws — actionAny over N actions consumes exactly N draws, one per Fisher–Yates iteration including the degenerate final draw with bound 1.
• nondet_retry_consumes_zero_extra_draws — a nondet retry is pure mixed-radix arithmetic; the retry path charges zero additional draws, verified order-independently over all four initial positions.

The two integration tests use the same helper-based quint CLI path as existing evaluator tests. The full pre-existing suite (164 tests) passes unmodified; cargo fmt --check and cargo clippy -- -D warnings are clean on the evaluator.

API surface

• One public trait: ChoiceSource, with two methods — fn next(&mut self, bound: u64) -> u64 and fn next_biguint(&mut self, bound: &BigUint) -> BigUint. It is object-safe, so it can be stored as Box<dyn ChoiceSource>, and both methods mirror Rand's own signatures. Implementations must return a value in [0, bound) and answer every call infallibly; there is no error path in the trait, keeping the seam free of Result plumbing.
• One private field on Rand: choice_source: Option<Box<dyn ChoiceSource>> (default None).
• Two public methods on Rand: set_choice_source(&mut self, source: Box<dyn ChoiceSource>) and take_choice_source(&mut self) -> Option<Box<dyn ChoiceSource>>.

Zero call-site changes: all five nondeterminism draw sites already route through Rand, so delegation inside next / next_biguint covers them all. Both methods advance the internal counter on every draw even when a source is present, preserving get_state() semantics.

Note on the second method: the large-powerset path in next_biguint seeds an internal StdRng directly rather than going through next. Delegating only next would therefore silently fall back to real randomness on large powersets and break replay; next_biguint on the trait closes that gap.