[casselc]

Attribute protocol-property timeouts to a replayable run

Summary

Replace the single opaque protocol-property namespace run with a discovered,
source-ordered run of its individual deftest vars. Before each property starts,
the runner now records:

• the exact property var;
• an explicit seed that is passed to Hegel; and
• the observable phase, :hegel-run.

Each property has a 60-second watchdog inside the existing 300-second aggregate
watchdog. A timeout stops the remaining suite, because Jolt does not expose
cooperative future cancellation and starting another property beside the stuck
worker would make both results suspect.

Why

On exact head c30804f98cc9bb9428a556745d4d1a36f9190ebb, one macOS CI attempt reached
the protocol-property namespace and hit its 300000 ms watchdog. The failure said
only protocol properties timed out; it did not identify which of 18 properties
was active or the Hegel seed. A same-SHA PR-event run and failed-job rerun passed,
confirming that the symptom was intermittent but leaving no evidence with which
to isolate it.

Hegel already resolves and supplies a fresh seed internally, but the pinned API
returns that seed only after a run completes. Choosing the seed at the jolt-http
runner boundary preserves randomized coverage while making a hung invocation
identifiable and replayable before control enters Hegel.

The reported phase is intentionally coarse. The current API does not expose
whether libhegel is generating, executing, or shrinking, so this change reports
only the source-supported fact that the var entered its Hegel run.

Fail-closed and non-vacuous controls

• A non-positive timeout is rejected at namespace load.
• A fault selector that names no discovered property fails instead of silently
  running a normal green suite.
• The per-var runner fails closed if the property namespace gains :once or
  :each fixtures that it does not yet know how to apply.
• The checked-in watchdog control covers completion, throw, deliberate block,
  nonempty property/seed/phase context, ordinary-scenario continuation, and
  protocol-timeout abort; it releases and joins its blocked worker.
• JOLT_HTTP_FAULT_HANG_PROPERTY deliberately blocks a selected real property
  only after its context is durable, exercising the production watchdog and
  report path.
• JOLT_HTTP_FAULT_THROW_PROPERTY proves an unexpected real property-body
  throw reaches the same attributed report path instead of being swallowed by
  clojure.test/test-var.

Chiasmus model

The bounded model covers the 18 current property IDs, a 60000 ms property bound,
and the existing 300000 ms aggregate bound. Its violation query asks whether a
timeout or throw can pass the gate or be reported without exact property, seed,
and observable phase.

• current runner: UNSAT (no counterexample in the bounded model);
• former namespace runner: SAT (property 0, reported ID -1, no seed/phase);
• completed passing property: SAT (the gate can still pass); and
• exact 300000 ms aggregate timeout: SAT with exact attribution.

The model, controls, source facts, assumptions, and semantic gaps are checked in
under docs/proofs/protocol-property-attribution.md.

Objective measure

The target was set before implementation: preserve all 18 properties and 23
assertions, keep the healthy focused run at or below 31 seconds (20 percent over
the 25.82-second baseline), localize an injected hang at a 100 ms test bound,
and retain the 300-second aggregate ceiling.

The final comparison alternated three base and three candidate runs on the same
machine and dependency cache rather than selecting a best run:

Gate	Previous baseline	This branch
Healthy protocol properties	initial 25.82s; A samples 21.77/19.19/24.12s, median 21.77s	B samples 18.75/21.07/20.58s, median 20.58s; 18 properties, 23/23 assertions
Timeout attribution	300s, namespace only, no seed/phase	100ms injected bound; exact property/seed/phase; process exited in 0.62s
Full suite	342 checks	350 checks, 0 failures, 25.04s

The focused healthy median is 5.5 percent faster than the paired base median;
every candidate sample also passed the precommitted 31-second ceiling. The
eight added checks are watchdog, timeout-policy, fixture, and fault-selector
semantic controls.

Validation

Exact base: c73db8da2218e32b8a1b94ea777ce00a9563b3f6

Exact head: 849db5b7cfd1ff6b4a09eb486d8088cb9533debe

$ jolt -M:test "watchdog controls"
8 checks, 0 failures

$ jolt -M:test "protocol properties"
Ran 18 protocol properties. 23 assertions passed, 0 failures, 0 errors.
23 checks, 0 failures
candidate samples: 18.75s, 21.07s, 20.58s

$ JOLT_HTTP_PROTOCOL_PROPERTY_TIMEOUT_MS=100 \
    JOLT_HTTP_FAULT_HANG_PROPERTY=request-parsing-is-invariant-under-chunking \
    jolt -M:test "protocol properties"
FAIL protocol property request-parsing-is-invariant-under-chunking timed out after 100 ms [property=request-parsing-is-invariant-under-chunking seed=9223370250071073194 phase=:hegel-run]
0 checks, 1 failures
HANG wall=0.62 exit=1

$ jolt -M:test
350 checks, 0 failures
FULL_FINAL wall=25.04 exit=0

All Jolt commands ran through the workspace's Chez 10.4.1 fail-closed wrapper.
All four SMT-LIB files were linted and verified from disk with Chiasmus/Z3.

Exact-head hosted validation also passed on both workflow triggers:

• PR-event run 34005859972: canonical policy, Linux x86_64, macOS arm64;
• push-event run 34005858250: canonical policy, Linux x86_64, macOS arm64.

Scope

This changes only the test runner, protocol-property test support, and bounded
proof documentation. It does not change HTTP production behavior, loosen a
timeout, require aspects/instrumentation, or claim to reproduce the original
macOS scheduling condition.

Tracks chucklehead-dev/jolt-aspect-packs#101.