No registry version admits a divergent terminal platform door

[dollspace-gay]

Gap

The eight divergent declarations in the frozen platform and synchronization packages reach L3 or L4 by no route that exists today.

The doors, all carrying diverge in their effect row:

Declaration	Source	Effect row
boot_entry_transfer	stdlib/kernel-primitives/platform/api.th	platform(boot), diverge
runtime_panic_terminal	same	platform(boot), diverge
runtime_contract_failure_terminal	same	platform(boot), diverge
runtime_allocation_failure_terminal	same	platform(boot), diverge
trap_context_return	same	platform(irq), diverge
power_reboot_terminal	same	platform(power), diverge
power_off_terminal	same	platform(power), diverge
cpu_halt_terminal	stdlib/kernel-primitives/synchronization/wait.th	platform(cpu), diverge

Two independent refusals stand between them and a verified build, and both are the design working:

1. .design/build/l3-verified-artifact.md section "Strict gates" makes fx diverge a hard failure of the Termination gate. fn strict_source_checks_with_registered_boundaries in verified_build.rs implements that row. Effect subsumption propagates diverge to every caller, so the whole path from the door to the export root would sit at the .design/forge/degrade-ladder.md REQ-9 partial-correctness L1 cap, below the artifact's L3 certificate floor.
2. .design/build/frozen-primitive-registry.md section "Source-derived minimum machine class" maps platform(boot), platform(irq), platform(cpu), and platform(power) to privileged. Section "The gate" rule 1 admits only sequential through the safe v1/v2 linkages, and rule 3 keeps separate_verus_machine_crate at one exact canonical atomic operation. No shipped schema models a privileged door.

Relaxing (1) alone publishes nothing new, because (2) still refuses.

What a future admission must settle

.design/build/synchronization-primitives.md section "Waiting surface" already names the missing artifact: "a registry version capable of expressing their concurrency and progress semantics". Such a version has to settle, at minimum:

1. the caller's obligation shape for a call with no continuation;
2. whether a divergent call is admitted in tail position only;
3. the emitted Rust for a non-returning boundary and how Verus discharges the caller proof;
4. how the receipt records the operation, and which assurance the artifact may claim once the privileged class rejects a safe linkage; and
5. which divergent shapes stay refused whatever the schema admits.

Scope note

.design/build/divergent-terminal-composition.md records the current position as a documented limit and states the two consumer routes that work today. This issue tracks the missing admission route only. .design/build/frozen-primitive-registry.md section "Remaining work" already lists "volatile and privileged models, and concurrent/liveness composition" as a prerequisite.