Sketch Pulse short-circuiting for stateful boolean operands

[eluvane]

This PR is a draft Pulse follow-up to #4322 and #4335. It is not intended as a polished final fix; it is a concrete sketch of the checker changes and regressions that may help the Pulse maintainers finish the design.

The change explores short-circuit-aware hoisting for stateful && and || operands in expression positions such as let b = ...; b, while keeping top-level hoisting conservative so existing while-guard proofs continue to use the old path.

The checker-side changes recognize Prims.op_AmpAmp and Prims.op_BarBar before generic argument hoisting, reify them as Pulse control flow when hoisting nested/control-flow return bodies, and keep branch-post joining conservative. Existing rewrites_to facts stay on the old elimination path, while plain eq2 branch facts may substitute local result variables before those variables are closed. That lets inferred branch posts simplify under branch facts without broadly changing rewrites_to handling.

A new regression file, ShortCircuitStatefulBool.fst, uses stateful boolean helpers that increment a counter when evaluated. The positive cases cover &&, ||, nested short-circuiting, expression-position conditionals, and pure boolean operands. The while-guard case remains marked expect_failure, documenting the remaining limitation without breaking existing Pulse examples.

[eluvane]

...