perf: do not log picks during the model checker's search

[zqy1018]

Problem. Extracted actions keep a log with every result: each pick records the candidate it chose, formatted with Repr. The model checker's search and #simulate never read it (tr drops the log as soon as an action returns), yet they paid for it on every state.

This PR puts the log behind a runtime switch, LogSwitch. The search and #simulate run with it off. Recovering a counterexample trace runs a second copy of the transition system with it on (findReachableThen takes a lazily built traceSys for recoverTrace), so the log stays available where it may be read.

Implementation details. LogSwitch is @[nospecialize]: the switch is a runtime argument, and every action is still compiled once. The log is invisible to wp, so the switched log instance is lawful and extraction stays certified; Veil's wrapper rules (pickSuchThat_VeilM, assume_VeilM, require_VeilM, pickSuchThat_bind_VeilM) are now generic in the log instance, like Loom's.

Why it saves both time and memory. With the log on, every candidate that has results costs a Repr call that allocates a Std.Format tree (a large one when the candidate is a message or a set), plus a fresh log and result pair for each result the entry is prepended to, all of it dropped right after the action returns. With the log off, the log is []: the compiler moves the Repr call into the branch that logs, and the bind after the pick takes Loom's empty-log fast path, returning the continuation's results untouched. The work and the allocations are gone, and so is the memory the entries took: results that are alive at the same time, notably the initial states, which are built as one list, no longer carry formatted copies of the values picked for them. Specs without picks are unaffected; the gain grows with the cost of formatting the picked values.

Tested by VeilTest/Regression/PickLogSwitch.lean: with the switch off every log is empty, with it on the logs list the picked candidates in order, and the results are the same.