[EHotwagner]

Refs #727 (source slice only; publication needs a separate fdev admission).

What

Implements fdev's decided direction for #727:

1. Policy deadline bounds policy work only. A load still creates the Worker and posts its command at once (the browser queues it). The Worker's first Compile receipt for that command is its readiness report. Before readiness the load control is in phase start under a separate startup bound — default 5,000 ms (HostSettings.defaultWorkerStartTimeoutMilliseconds), selectable 1–60,000 ms via HostSettings.withWorkerStartTimeout, capped by any caller enclosing deadline. Expiry before readiness settles Discarded with the distinct, appended DeliveryReason.WorkerStartTimeout (outcome TimedOut/Compile/not dispatched), terminates the Worker and grants no game authority. Readiness replaces the startup timer with the unchanged 250 ms policy timer. Compilation, phase and digest receipts before readiness, repeated readiness and readiness after expiry are inert; a Worker failure, termination or protocol-violating invocation receipt before readiness still faults the starting Worker. Requests to ready Workers, disposal, replacement, candidates, freeze and terminal retirement are unchanged.
2. Model agreement. eng/wasm-shared/lifecycle.qnt gains the start phase, readiness, settleStartTimedOut, and invariants startingHasNoAuthority, deadlinesBounded, startTimeoutIsDistinct, startTimeoutTerminates; five new named Quint tests; five new deterministic correspondence schedules (startup boundary before/at/after, early compile receipt, candidate startup refusal); regenerated traces (default 58 / selected 16); two new causal mutants plus one raw-terminal mutant.
3. Browsers. The package-consumer and raw conformance suites run in Chromium, Firefox and WebKit. A new cold-load case runs 20 fresh-profile loads per browser under a hosted-like 4-CPU budget and records startup/policy timings, retained as the wasm-cold-load-* artifact.
4. Version. The public Browser API changes additively (new reason case, new HostSettings members) and its behavior changes, so the coherent set goes to 0.7.0, classified against published 0.6.0. No publication or tag.

Startup bound rationale and test evidence are in docs/roadmaps/wasm-shared-01.md and the PR thread.

Signed: fdev

🤖 Generated with Claude Code

[EHotwagner]

Independent review: PR #728 at 1f68f963bb0cb1b3de7a19ea8d001529165f8a21: ACCEPT

I reviewed the exact candidate 4b9bfb6..1f68f96 (3 commits: f6fcb16, 8958e53, 1f68f96; 131 files) against #727 and the original defect evidence (FS-GG/.github#4710 comment 6354156750). The PR head still equals the reviewed head. This review did not author any of the change.

Material findings

None. I found no defect that blocks acceptance.

What I verified against the source

Reducer (src/Wasm.Browser/Lifecycle.fs)

• Start phase. applyLoad gives a load the startup deadline Clock + workerStartTimeout, saturating and capped by EnclosingDeadlineMilliseconds, with Starting = true. startControl still arms that deadline and posts the command at creation.
• Readiness. observe/PhaseObserved with Some(pending, true) when pending.Starting accepts only InspectAndCompile, Compile that matches the Worker instance, identity and correlation. It re-derives the deadline as Clock + SelectedLimits.MaximumDeadlineMilliseconds, capped by enclosing, so the policy budget is unchanged and the captured SubmitLimited limits are respected. Its effects are CancelTimer then ArmTimer, on the same key because the timer phase stays Compile.
• Inert before readiness. Any other phase is inert. A repeated Compile after readiness falls into the pending.Phase = phase inert branch. AbiVersionObserved is guarded by not pending.Starting. Readiness after expiry is inert because expireAt runs before the input and has already removed the control. The boundary is inclusive, and the boundary-start-before/at/after traces confirm it.
• Expiry reason. expireAt maps a starting control to WorkerStartTimeout, everything else to DeadlineExpired. invalidateWorkerCore gives TimedOut/Compile/NotDispatched, terminates the Worker and settles Discarded. The RetireSession branch of invalidateWorker cannot apply because a starting control is never Current.
• Interactions. Disposal settles the starting control as HostDisposed and cancels its timer. ReplaceCurrent and abort invalidate a starting Active or Candidate as GenerationRetired. Startup expiry of a candidate keeps the Active authority (unit test and boundary-candidate-start-timeout trace). Freeze does not touch controls, as before. initialize refuses Busy while a control is present. Commit needs Initialized. Sc2SupervisorV1 shares the controls expiry path, and createCompatible carries the timeout through.

RuntimeProtocol.fs/.fsi

• WorkerStartTimeout is appended last in DeliveryReason, so the existing tags do not change.
• The new HostSettings field sits inside the private case, so it is not on the public surface.
• withWorkerStartTimeout validates [1, 60000] and uses the same finite-integer guard as the Fable boundary.
• No exhaustive DeliveryReason match exists elsewhere in src/tests.

Host.fs timer re-arm. I checked it against worker-client.mjs:

• ArmTimer calls clearTimeout on the existing key, and CancelTimer calls clearTimeout and deletes the key. A cancelled or replaced timer's callback never runs, so the re-arm cannot bring a cancelled timer back.
• The callback deletes its key before it observes, so a re-arm installs a fresh handle.
• After disposal it skips the re-arm and delivers ObserveTimer, which is a harmless stutter because every timer was already cancelled.
• The test transports fire timers manually, not synchronously, so there is no recursion. With a monotonic clock and delay >= 1, re-arming is bounded.
• The condition now <= due mirrors the reducer's strict deadline < now.

Readiness signal. WorkerEntry.createWireRuntime emits PhaseObserved(Compile) synchronously on receiving the load command. That is after the module graph has evaluated and onmessage is installed, and before admission, sha256 and compile/instantiate. All policy work therefore stays inside the 250 ms budget. The report is bound to the creating Worker's port, its identity and its correlation. The guest wasm cannot post to the page, so I consider the report adequately authenticated for this trust model.

5,000 ms default. It is defensible. Hosted evidence from this head's run, wasm-cold-load-*, ubuntu-latest, host:4, 20 cold loads per browser:

Browser	Startup p50	Startup max	Startup max ÷ 5000	Policy max	Policy max ÷ 250
Chromium 153	27.5 ms	37 ms	135×	5.7 ms	44×
Firefox 155	58 ms	76 ms	66×	8 ms	31×
WebKit 26.6	44 ms	52 ms	96×	9 ms	28×

Model and implementation agreement

• lifecycle.qnt has the start phase and requestFor uses workerStartBound. Timer effects project start as compile, which matches the F# TimerIdentity. Readiness sets deadline = clock + policyBudget; the compat module uses dueFor with the selected limits and startDueFor capped by enclosing. compiled is inert while starting. Expiry gives settleStartTimedOut with WorkerStartTimeout/TimedOut/compile/not dispatched.
• New invariants: startingHasNoAuthority, deadlinesBounded, startTimeoutIsDistinct and startTimeoutTerminates in lifecycleSafe, and selectedStartingHasNoAuthority in compatibilitySafe. No existing invariant was removed.
• Five named Quint tests were added; the preflight count goes from 8 to 13 and the expected set is updated. Two witnesses were added: sawWorkerReady and sawStartTimeout.
• Schedule changes only insert a readiness step: each schedule gets if starting → readyNow, and its step count rises by the number of fresh Workers. There are five new deterministic schedules (census 53/16 → 58/16, 71 → 76 paths). The readiness, expiry and inert-compile sequences in the new traces read correctly.
• Mutants added: startup-expiry-as-policy-expiry, readiness-keeps-startup-deadline and raw startup-cause-to-deadline. No existing mutant or witness was removed.
• verify-wasm-supervisor.sh adds a readyCandidateCompatible sampled entry, appended to model-ready.log. This adds samples and relaxes no gate: the witness set and the [1-9] threshold are unchanged. It is justified because the extra readiness step made sawFrozenCommitExpiryRefused unreachable at the pinned seed, where it had been a 1-in-1000 sample. That is better than changing the seed.

Tests

• Unit tests. New tests cover:

  • the startup bound for each profile, including the exact boundary, late readiness and termination;
  • readiness starting the policy budget, a duplicate readiness and policy expiry staying DeadlineExpired;
  • pre-readiness, foreign and wrong-correlation inertness;
  • range validation and compatibility retention;
  • the enclosing cap;
  • candidate preservation;
  • the early-timer re-arm;
  • disposal during startup.

  Existing fixtures only gained the readiness step.

• Browser specs.

  • The 1 ms compile-deadline test became a deterministic withheld-loaded test with stronger reason/disposition assertions. Its held ∈ {0,1} and Phase ∈ {Compile, Instantiate} checks reflect a real race, not a weakening.
  • The new withheld-readiness test exercises inert pre-readiness loaded receipts in a real browser.
  • Trap wording is now compared case-insensitively, which is a justified WebKit difference.
  • loadBounded → loadLimited in the fresh-Worker tests follows from the documented design: an enclosing deadline caps startup.

• Cold load.

  • Each sample uses a fresh context, so there is no HTTP, module or compile cache, but the browser process is warm after the first sample.
  • Startup is measured as Worker creation to the readiness wire. Policy is measured as readiness to settlement. The two are measured separately and correctly.
  • It asserts n ≥ 20, success, the advice bytes and max values under both bounds.

• Release-check updates. Playwright install moved to three engines in both install-browser-tools.sh and the workflow, with the matching step-name mutant updated in verify-wasm-workflow.sh. The cold-load artifact is retained with if: always().

Release coherence

• Everything moved to 0.7.0 together: version.props, sdk/wasm/VERSION, the Rust crates/locks, the worker bundle, compatibility-profile.v1.json, promotion.py and qualify-supervisor-installed.sh.
• api-baseline-policy.json is rebased on published 0.6.0, and I checked each value independently:
  • The tag wasm/v0.6.0 resolves to commit 8a5e63b… and tree 090906c….
  • The release asset digest of release-manifest.json is e40258fe….
  • The nuget.org served archives hash to 4245920d… (Contracts) and e869095e… (Browser).
• The historical policy is kept as api-baseline-policy-0.6.0.json (byte-identical to the former current) and is registered in release_manifest.py.
• bind-installed-release.py still binds published 0.6.0. That is correct, and matches earlier bumps: the binder moves only after publication.
• No tag or publication is created.

CI on the exact head

• gh pr checks 728: 34 pass, 1 skipping. The skipped job, "Prepare canonical WASM trace artifact (not qualification)", is skipped by design.
• wasm-shared run 39881900333 (headSha 1f68f96): success. It took 26 m 35 s against the job's timeout-minutes: 35. Every step passed, including Quint/correspondence, raw conformance in three browsers, package consumer plus cold-load in three browsers, and compatible supervisor source and installed custody.

Non-blocking notes

1. Docs wording. docs/wasm/runtime.md says "other receipts before readiness … are inert". That is true for phase and ABI receipts. It is not true for WorkerFailed, WorkerTerminated or a protocol-violating InvocationObserved/InvocationTerminated on the load control, which still fault or invalidate the starting Worker. That behavior is correct (faults should act before readiness); only the wording overstates.
2. Selected-policy coverage of startup expiry. Under Sc2SupervisorV1, startup expiry is never sampled: compat loads use enclosing: 0 and compatibleTimer advances +1. No selected deterministic schedule or F# expiry test covers it either. Also, deadlinesBounded is not part of compatibilitySafe. The risk is low because the F# expiry path is shared, but one selected schedule would close the gap.
3. Enclosing deadlines on loads. A caller enclosing deadline that elapses before readiness reports WorkerStartTimeout. This is consistent with the documented design. It also means a receiver that passes a short enclosing deadline (for example now + 250) on a load would still bound Worker startup by it. The Templates re-pin should not do that.
4. CI headroom. The wasm-shared job now takes about 26.5 of its 35 minutes, leaving about 8.5 minutes of headroom after adding two engines and 60 cold loads.
5. WorkerEntry.inspectAndCompile (public). It emits Compile only after compiling. A custom Worker built on it would report readiness late. The packaged Worker does not use it.
6. Naming. EndToEndFromEnqueue now starts counting at readiness for loads. The docs state this, but the name is now technical debt.
7. Early-timer path. It builds a full Projection on each early callback. That is cheap but avoidable.

fdev critic

[EHotwagner]

Delta review: PR #728, 1f68f96 → 9f202d9ed976fca667cdb8cf888099e2ed3d601f: REJECT (required CI fails on this head)

The docs/Atlas delta itself is accurate, and I accept it as written. The candidate cannot be accepted because the required "Shared WASM source, model, package, and browser qualification" check fails on this exact head. The cause is this PR's own CI change, not the delta.

Material finding

M1. The required wasm-shared job exceeds its 35-minute limit on the final head, and this PR's three-browser install causes it.

Run 39884877948 on headSha 9f202d9 was cancelled at 35m21s (01:35:42 → 02:11:03, ##[error]The operation was canceled.). It was inside "Qualify compatible supervisor source and installed custody" when the limit hit.

Every earlier qualification step passed: lifecycle/Quint, three-browser conformance, package consumer and cold-load. The time went to "Install pinned Playwright browsers", which took 16m28s. In the previous head's run 39881900333 the same step took 41s.

The log shows Fetched 119 MB in 15min 51s (125 kB/s) from azure.archive.ubuntu.com. That download is mostly the gstreamer and related system packages pulled in by npx playwright install --with-deps chromium firefox webkit (.github/workflows/wasm-shared.yml, "Install pinned Playwright browsers").

This PR added that download (Firefox and WebKit dependencies). It also raised the nominal job time to about 26.5 minutes but left the job at timeout-minutes: 35. One slow mirror is therefore enough to fail the required gate. In my previous review this was non-blocking note 4; it has now happened on the final candidate.

Requested repair (same owner, same PR):

• Give the job enough headroom for the three-engine install, for example by raising the job's timeout-minutes.
• Optionally bound the install step on its own and add a retry, or otherwise make the package fetch less sensitive to mirror speed.
• Then run required CI on the resulting head and request a fresh exact-candidate decision.

A plain rerun on 9f202d9 might pass, but it would not remove the demonstrated lack of headroom.

What I verified in the delta

• Scope. git diff 1f68f96..9f202d9 touches only these files: docs/wasm/runtime.md, docs/roadmaps/wasm-shared-01.md, docs/atlas/catalog.json, the removed record 53549c82… and the added record b091d938…. There are two commits, 7878a46 (docs) and 9f202d9 (Atlas). No source, test, model or workflow file changed.
• Wording against the reducer (src/Wasm.Browser/Lifecycle.fs, observe).
  • Compile, phase and digest receipts before readiness are inert:
    • a non-Compile PhaseObserved on a starting control returns state, [];
    • AbiVersionObserved is guarded by not pending.Starting;
    • ArtifactDigestObserved is unhandled and falls through to | _ -> state, [].
  • WorkerFailed with a matching correlation and WorkerTerminated both reach invalidateWorker … WorkerFault.
  • An InvocationObserved/InvocationTerminated on the load control takes the not isInitialize branch, which ends in invalidateWorker (WorkerFault "initialization failed").
  • "A caller enclosing deadline on a load also caps startup" matches applyLoad.
• Atlas.
  • atlas.py --archive docs/atlas validate from the worktree gives exit 0: {"records":39,"archiveBytes":200178,"fingerprint":"a853333d…"}.
  • The catalog lists 39 records and has 39 record files. The swap from 53549c… to b091d938… is the only catalog change, the file name matches the record, and 53549c… was never on origin/main, so withdrawing it supersedes nothing.
  • All 11 citations hash-match their files at 7878a46 and are byte-identical at 9f202d9. 7878a46 is an ancestor of the head.
  • The record's hosted numbers match the wasm-cold-load-39881900333-1 artifact, which I downloaded and summarized independently:
    • startup max: Chromium 37 ms, Firefox 76 ms, WebKit 52 ms;
    • policy-load max: 5.7, 8 and 9 ms.
  • The behavior summary matches the source.

CI on 9f202d9

gh pr checks 728 shows 33 pass, 1 skipping (trace-artifact preparation, skipped by design) and 1 fail: wasm-shared run 39884877948, which was cancelled by the job timeout as described above.

Non-blocking

1. A protocol-violating invocation receipt on a starting load control first settles that load with the Worker-supplied outcome (finishControl: disposition Current/HistoricalOnly, reason None) and only then invalidates the Worker. "Faults and retires the starting Worker" is accurate about the retirement. The settled result does not carry a WorkerFault reason. This behavior predates this PR.

fdev critic

[EHotwagner]

Exact-candidate decision: PR #728 at 5cbcbe7c913b9ab76333a5a3f246b1667add255c: ACCEPT

This head resolves M1 from my REJECT of 9f202d9. Required CI is green on this exact head.

Candidate identity and scope

• The PR head is 5cbcbe7, one commit on top of 9f202d9.
• git diff 1f68f96..5cbcbe7 touches only these 7 files:
  • .github/workflows/wasm-shared.yml
  • scripts/verify-wasm-workflow.sh
  • docs/wasm/runtime.md
  • docs/roadmaps/wasm-shared-01.md
  • docs/atlas/catalog.json
  • the withdrawn Atlas record 53549c… and the added record b091d938…
• So since my full review and ACCEPT of 1f68f96, the only changes are the docs/Atlas delta I accepted in my review of 9f202d9, plus the CI-headroom change below. No source, test, model, trace or version file changed after 1f68f96.

Delta 9f202d9..5cbcbe7 (resolves M1)

• Job limit. wasm-shared.yml raises the qualify job limit from 35 to 55 minutes, with a comment explaining why. The nominal run is about 24–27 minutes, so there is now about 28 minutes of headroom.
• Install step. "Install pinned Playwright browsers" now has its own timeout-minutes: 20. It also gets one bounded retry: each attempt is timeout 540, so two attempts are at most 18 minutes, which is inside the step limit. The loop's exit logic is correct.
  • A transient mirror failure is retried once.
  • A pathologically slow mirror now fails the install step clearly instead of cancelling the whole job late.
• Preflight. The required token in verify-wasm-workflow.sh is updated to timeout-minutes: 55. No other timeout-minutes: 35 reference remains, and the existing mutant controls (timeout-minutes: 30 for the trace job, and the install/compile step-order mutant) are unaffected.
• Roadmap. The new paragraph accurately records the cancelled run 39884877948 (install 16 min 28 s against 41 s earlier) and the new limits.

CI on 5cbcbe7

• gh pr checks 728: 34 pass, 1 skipping. The skipped job is trace-artifact preparation, which is skipped by design.
• wasm-shared run 39888632477 (headSha 5cbcbe7): success in 24m04s.
  • The install step took 53 s, and apt fetched 119 MB in 17 s on the first attempt.
  • The supervisor qualification took 9m15s.
• Cold-load artifact wasm-cold-load-39888632477-1, which I read independently: host 4 CPUs, 20 loads per browser.

Browser	Startup max	Policy-load max
Chromium	35.8 ms	5.7 ms
Firefox	100 ms	5 ms
WebKit	61 ms	8 ms

Firefox's 100 ms startup still leaves 50× margin under the 5,000 ms bound, and every policy load is at least 31× under 250 ms.

Material findings

None.

Non-blocking notes

1. Slow-mirror case. At the 125 kB/s seen in run 39884877948, a 119 MB fetch needs about 16 minutes. A single 9-minute attempt would therefore time out. The retry is likely to succeed because apt keeps fully downloaded .deb files in its cache, but that is marginal. The outcome is now a clear install-step failure rather than a late job cancellation, which is acceptable.
2. Interrupted install on retry. timeout sends its signal to the whole process group, so it can interrupt apt-get/dpkg mid-install. The retry may then hit an interrupted dpkg state. This is rare; a sudo dpkg --configure -a before the retry would harden it.
3. Preflight coverage. The workflow preflight pins the 55-minute job limit but not the install step's bound and retry tokens.
4. My earlier non-blocking notes on 1f68f96 still stand: selected-policy coverage of startup expiry, the EndToEndFromEnqueue naming, inspectAndCompile reporting readiness after compile, and the early-timer Projection cost.

fdev critic