R12: Frontiers name what they awaitreq:R12
- Open, worded as a proposed claim: pool-wake-selection (proposed claim; reactive-scheduling): the helper selects the first count waiters of the state that it finds, and it notifies exactly those, in order; the model's fact is select_takes_first, and one selection is one store step (select_attempt); the helper is a library program, one selection step and then each selected hint in order; the selection is by count, so the law takes the withdrawal as a premise: every entry of the waiters belongs to a request that still waits; finite controls: a selection at the post serves a waiter that left, and with no withdrawal the wake is lost (Test/Program/PoolPublic.lean, PP4; Test/Program/PoolTraces.lean, trace 2) (decisions rows 221, 267)
- Open, waits on a ruling (a ruling on infinite tapes): R12-c: liveness on infinite tapes under FairTape (waits on a ruling on infinite tapes)
- Open, not triaged: stability over the allowed internal decisions, with a named progress observation (not stated)
- Open, not triaged: divergence by compatible prefixes (DB-03; not stated)
- Open, worded as a proposed claim: driver-continuation-split and driver-suspension-keeps-typed (proposed claims; reactive-scheduling, extending drivestate-lift): a retained driver suspension keeps the commands, the remaining dispatcher tasks, the enclosing flush or clock phase and any atomic owner, and continuing it with budgets n and k equals one run with n + k; until then an owned operation runs under a proved embedded budget (decisions rows 84, 226); a finite control: at a reply application the command loop's leftover commands are not kept, and one run then stands at rest with no exit of the root (the run dropped of Test/Dogfood/Scenario/QueueWorkers.lean; one script at seven budgets)
- Open, worded as a proposed claim: embedded-budget-sufficient (proposed claim; reactive-scheduling, serving R10 and R12): the embedded budget of an owned operation covers its registration, its cleanup and its selected delivery, so no cut falls inside the operation; a cut inside is excluded and is no resumption (decisions rows 84, 226); no theorem states a sufficient budget; a finite control measures the least fuel of one helper's task at eight lengths of the receiver's continuation, and at one unit less the remaining work is lost and five later flushes do not end the root (Test/Program/QueueTraces.lean, Test/Program/SemaphoreTraces.lean and Test/Program/PoolTraces.lean, trace 7 of each; Pool's measures seven lengths); no bound is claimed; at a run the premise has one name, funded (src/Effect4/Run/Tape.lean), and funded_replays says what it gives; a journal's verdicts do not decide it
- Open, worded as a proposed claim: wait-registration-no-gap (proposed claim; reactive-scheduling): the decision to wait and the registration are one transition, so each eligible waiter is retrying or owns a notification (decisions rows 221, 223; finite controls in docs/research/2026-10-05-claude-lead/tx-probes/TxModel.lean); the Queue model's half is proved on the first profile (queue-first-step-invariant, queue-first-run-flags), and the wrapper's run stays open; an instance at rest on one program is the planned goal queue_settled (Test/Dogfood/Scenario/QueueWorkers.lean)
- Open, worded as a proposed claim: posted-task-decision-preserves (proposed claim; reactive-scheduling): a posted task keeps the typed state, with its execution identity, its owner, its receiver's token and a stale delivery (decisions row 225)
- Open, not triaged: posted-wake-debt-progress and a module's request progress: separate claims under named fairness, body-progress and budget premises; dispatcher service (flush_fair) does not give them (decisions rows 220, 225, 230)
Requirement R12: Frontiers name what they awaitabout:req:R12
This page explains requirement R12 in Effect4. It covers what the requirement asks for live frontiers, why distinguishing waiting from deadlocks matters, and how the property is checked.
What the requirement asksabout:req:R12:what-it-asks
Requirement R12 demands that non-terminal machine states explicitly name what they await rather than conflating pauses with failures (docs/core/system-map. §8, DB-03):
- Live frontiers: a frontier state represents a live pause waiting for fuel, host replies, or scheduling decisions.
- Frontier characterization: when execution runs out of decisions, the frontier is empty if and only if the machine is deadlocked (
frontier_empty_iff_deadlocked). - Deadlock definition:
Deadlockedrequires no runnable fiber, no armed listener, no pending host request, no active timer, and no compile budget. - Fairness draining: a fair decision tape leaves no armed listener at its live end (
fairTape_unarmed).
A pause caused by resource exhaustion or external silence must never be reported as an error.
Why it mattersabout:req:R12:why-it-matters
Asynchronous and concurrent systems pause frequently when waiting for external responses or when running out of budgeted time.
If a runtime treated pauses as deadlocks or exceptions, programs would fail prematurely during legitimate long-running tasks.
Naming frontier causes allows external drivers to supply appropriate budget, deliver host replies, and resume paused fibers cleanly.
How it is checkedabout:req:R12:how-it-is-checked
The requirement is checked by proving frontier characterization, deadlock criteria, and fair tape draining theorems:
- Deadlock characterization is stated by
frontier_empty_iff_deadlockedinsrc/Effect4/Laws/Api/Frontier..lean - Fair tape draining of armed listeners is stated by
fairTape_unarmed(src/Effect4/Laws/Machine/Scheduling.).lean - Loop frontier characterization under host reply tapes is stated by
rows_loop_frontier(src/Effect4/Laws/Api/SessionMeaningLoop.).lean - Meaning frontiers under silent hosts are stated by
rows_loop_frontier_hostin the same file.
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
The figure in words
- Reactive Scheduling open, 24 nodes, 3 open → No concept, Translation & Simulation, Host Session Protocol, Scope Lifetime & Finalization
- Host Session Protocol proved, 3 nodes → Translation & Simulation
- Scope Lifetime & Finalization proved, 3 nodes → Translation & Simulation, No concept
- Translation & Simulation open, 31 nodes, 1 open → No concept, Initial Algebras & Folds
- No concept proved, 3 nodes
- Initial Algebras & Folds proved, 1 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
fairTape_unarmed | proved | — | — |
frontier_empty_iff_deadlocked | proved | — | — |
rows_loop_frontier | proved | — | localWaitC_to_rowsB, funded_replays |
rows_loop_frontier_host | proved | — | localWaitC_to_rowsB, funded_replays |
driveState_loop | proved | — | loop_of_iteration |
iteration_below_budget | proved | — | — |
loop_of_iteration | proved | — | — |
bounded | proved | — | — |
complete_unique | proved | — | — |
select_takes_first | proved | — | — |
first_run_flags | proved | — | first_run_inv |
first_run_inv | proved | — | first_step_inv |
first_step_inv | proved | — | positive_suspend_step_capacity, first_profile_closed |
visit_selects_earliest | proved | — | — |
visit_stops_iff | proved | — | — |
quiet_nil | proved | — | — |
settled_of_ledger | proved | — | within_one, spent_one, quiet_nil, settled_of_view |
settled_of_view | proved | — | — |
spent_one | proved | — | — |
within_one | proved | — | — |
rest_step | goal | rest_step | checkInput_eq_none_iff |
fed_accounted | modulo | jobs_step, rest_step | accounted_of_ledger, rest_step, exit_eq, jobs_step, checkInput_eq_none_iff, reached_history, ledger_opened, queueCrew_acquire_once_placed, queue_acquisition_sites, queue_built_program |
queue_settled | modulo | jobs_step, rest_step | settled_of_ledger, rest_step, exit_eq, jobs_step, checkInput_eq_none_iff, reached_history, ledger_opened, queueCrew_acquire_once_placed, queue_acquisition_sites, queue_built_program |
localWaitC_to_rowsB | proved | — | localRunC_compileBO |
funded_replays | proved | — | journal_replays, tape_replays |
positive_suspend_step_capacity | proved | — | acceptLoop_length_le |
first_profile_closed | proved | — | — |
checkInput_eq_none_iff | proved | — | — |
accounted_of_ledger | proved | — | held_of_shows |
exit_eq | proved | — | — |
jobs_step | goal | jobs_step | checkInput_eq_none_iff |
reached_history | proved | — | — |
ledger_opened | proved | — | opened_exit |
queueCrew_acquire_once_placed | proved | — | queue_placement, queue_built_program, checkInput_eq_none_iff |
queue_acquisition_sites | proved | — | — |
queue_built_program | proved | — | queue_elaborates, build_retains, checkInput_eq_none_iff |
localRunC_compileBO | proved | — | compilesBO_onExit, compilesBO_matchCause, compilesBO_catchIf, compilesBO_catchCause, compilesBO_select, compilesBO_bind, compilesBO_iterate, compilesBO_exit, compilesBO_suspend, denoteRowsB_straight, denoteRows_straight |
journal_replays | proved | — | — |
tape_replays | proved | — | — |
acceptLoop_length_le | proved | — | — |
held_of_shows | proved | — | flatMap_offers, filterMap_gave |
opened_exit | proved | — | exit_eq |
queue_placement | proved | — | — |
queue_elaborates | proved | — | queue_refs_nil, queue_main_eq, elaborateModule_no_declarations |
build_retains | proved | — | finishBuild_retains, checkInput_eq_none_iff |
compilesBO_onExit | proved | — | at_append |
compilesBO_matchCause | proved | — | at_append |
compilesBO_catchIf | proved | — | at_append |
compilesBO_catchCause | proved | — | at_append |
compilesBO_select | proved | — | at_append |
compilesBO_bind | proved | — | at_append |
compilesBO_iterate | proved | — | at_append |
compilesBO_exit | proved | — | denoteRowsB_straight, at_append |
compilesBO_suspend | proved | — | at_append |
denoteRowsB_straight | proved | — | — |
denoteRows_straight | proved | — | — |
flatMap_offers | proved | — | — |
filterMap_gave | proved | — | — |
queue_refs_nil | proved | — | — |
queue_main_eq | proved | — | queue_main_some, elaboration_eq_getD |
elaborateModule_no_declarations | proved | — | — |
finishBuild_retains | proved | — | checkInput_eq_none_iff |
at_append | proved | — | — |
queue_main_some | proved | — | — |
elaboration_eq_getD | proved | — | — |