test(core): strengthen async/global-state property laws beyond deterministic boundary sweeps

[joeldsouzax]

Gap surfaced by #77. The @property/@model laws over async / actor / process-global state in #77 use DETERMINISTIC boundary-SWEEPS (the # GEN:-named values {0, 1, MAX-1, MAX} plus seeded-LCG op sequences) rather than real proptest!, because proptest! is synchronous and cannot cleanly drive tokio actors + nested spawn/Barrier concurrency. This covers the named boundaries but NOT the full input space, and gives no shrinking.

Scope

• Evaluate options to widen the async laws' input space: proptest's async support / a custom proptest runtime bridge (block_in_place + a current-thread runtime) / randomized-schedule fuzzing.
• Apply to the async/global laws: mailbox MPSC ordering, registry same-name election, supervision intensity window, links notify fan-out, request_* timeout predicates.
• Where a real proptest! bridge is genuinely infeasible (documented in test(core): wire core feature scenarios to the SUT #77's runners), broaden the deterministic sweep instead and state the trade-off explicitly.

Done when the async laws either run under real randomized input generation or carry a documented, widened deterministic sweep.

[joeldsouzax]

Deferred (not closed) — picking this up later. Design settled; parked on ROI grounds so future-us doesn't re-brainstorm.

Why deferred

This is a coverage/rigor card, not a stability card — it widens the input space, it does not de-flake anything. Weighed against M1:

• Near-zero stability gain, slight downside risk. The @property laws that would get the bridge are single-actor and deterministic. The flaky family is the @model concurrency laws (mailbox/supervision) — widening their seeded op-sequences adds timing-sensitive cases to a suite we just spent a session stabilizing (test(core): de-flake supervision property scenarios (timed settle barrier races under load) #100/test(core): de-flake message_features (core_message_bdd) — concurrent ask/tell race #106/test(core): de-flake ctx.reply early-reply scenario — single-writer settle barrier (#106) #108/test(core): de-flake supervision props strategy scenario (#100) #110).
• Boundary-value analysis already covers the high-value points. Existing sweeps hit {0, 1, c-1, c, c+1, MAX}; random interior values find comparatively few new bugs.
• M7-doomed code. This exercises the hand-rolled kameo core that M7 (de-handroll) will replace with best-in-class crates. Deep property-testing of soon-to-be-deleted code is low ROI vs. the actual M1 goal (Zenoh remote layer).

Settled design (for when we resume)

Split by what each law actually tests — do not run everything through one bridge:

Law type	Runtime	Generation	Rationale
@property (∀-input, single logical actor)	fresh current_thread via tokio::task::block_in_place	real proptest! + shrinking	deterministic replay from the input → shrinking is sound and valuable
@model / @linearizability (P threads + Barrier)	ambient multi_thread (unchanged)	widened seeded op-sequences	true parallelism is the whole point (CLAUDE.md rule 8); the failure lives in the non-deterministic interleaving, which the input does not capture, so proptest shrinking is unsound here

Key technical facts that drove this:

• The re-entrant bridge the console card (test(console): cucumber harness + wire console pure-helper scenarios #76) rejected — block_in_place + Handle::current().block_on on the same multi-thread worker — deadlocks under nested spawn/Barrier. The @property plan avoids it by building a fresh current_thread runtime on the blocking thread (not re-entrant).
• Proptest shrinking assumes deterministic replay; a truly-parallel @model run is non-deterministic, so a "shrunk" counterexample would not reliably re-fail. That is why @model laws keep real overlap + widened deterministic sweeps instead of being forced through proptest.

Recommended resume scope

Start descoped: build the small @property-only bridge (mailbox FIFO/try_send/unbounded/front-drain/post-close; request_* timeout predicates), leave every @model law untouched. Real coverage + shrinking win, ~1/3 the work, near-zero flake risk. Expand to @model widening only if a concrete bug motivates it.