R11: Resources are released: at most once per registration, exactly once in close orderreq:R11
- Open, worded as a proposed claim: pool-lease-return and pool-close-waits (proposed claims; scope-lifetime-finalization): a committed lease returns its item at most once, and exactly once where its exit ended; a lease that is refused at a closing pool commits nothing; the close ends only after every lease returned, and each item is then finalized once; the model's facts are giveBack_front, giveBack_once, close_refuses and drain_waits; the forms are stated, scoped and typed: use is the protected form over the lease's loop and the return, and the close is the wrapper over the closer's step, registered by make after the acquisitions (use_types, close_answers, make_types); their steps are return_attempt, close_attempt and drain_attempt; no goal states a clause, and each waits for the carrying fact of a region and for a finalizer's law of a run; finite controls: a lease in its own mask is lost under an interruption, a wait inside a mask of the form's making cannot be interrupted, the stand-in for the mask fails under a masked caller, and a close that does not wait finalizes an item that a borrower still holds (Test/Program/PoolTraces.lean, traces 4, 5 and 8; Test/Program/PoolPublic.lean, PP7) (decisions rows 222, 267, 268, 276, 279)
- Open, not triaged: the whole run open: release at most once per registration, counted by identity (DB-07); its planned goals are three, one program each: Workers.releases_once, cleans_once and QueueWorkers.releases_once
- Open, not triaged: the whole run open: exactly once in close order over closed scopes and structured regions, with a completed-cleanup receipt (DB-07, DI-65)
- Open, not triaged: state retained at a frontier, open scopes closed only by an explicit abandon (the owner's ruling of 2026-09-07)
- Open, waits on a ruling (the model probe's D8, not ruled (DB-07)): a scope a finished run leaves open is an observation, as in rc.112 (the model probe's D8, unruled per DB-07)
- Open, not triaged: the carrying fact of a region (scope-lifetime-finalization, serving saved-mask-region-bracket): the stack shape above ++ below is kept along the fiber machine's evaluator arms and commands while the fiber is inside the region, until the command that ends it; the bracket takes the shape as a premise at the later cut; its statement elaborates and a finite probe on eight runs finds no counterexample (docs/research/2026-10-06-seat-BRACKET-carry.lean.txt); the frame machine's own step keeps the shape (step_under); no goal states it
- Open, worded as a proposed claim: semaphore-protected-permit (proposed claim; scope-lifetime-finalization): across every prefix of a run a committed activation of Semaphore's protected form releases at most once; an activation whose exit has completed through its cleanup has released exactly once, with enough work for the cleanup or a retained frontier; while the cleanup has not completed, the release obligation stays in the observation, and a frontier is no completed exit; the form is one mask over the take's loop, the hook and the body at the restore site (protectedBy), scoped and typed (protectedBy_has, withPermits_types); no goal states a clause, and each waits for the carrying fact of a region; finite controls: a take in its own mask loses its permit under an interruption, a wait inside a mask of the form's making cannot be interrupted, and the stand-in for the mask fails under a masked caller (Test/Program/SemaphoreTraces.lean, traces 4, 5 and 8); Pool's lease is the second user (decisions rows 222, 259, 276)
- Open, worded as a proposed claim: waiting-request-obligation-preserved (proposed claim; reactive-scheduling, serving R10 to R12): a selected request's notification stays in store debt, queued commands, dispatcher work or the receiver's accepted continuation until it is discharged; when cancellation wins and withdraws the request before consumption, the operation consumes nothing; a completed commit stays committed, even when the caller is interrupted before its continuation; an interruption that is only requested, and stays pending under a mask, withdraws nothing; an old token is inert after rearming (decisions rows 221, 222); the Queue model's half of its first clause is proved on the first profile (queue-first-step-invariant), and the wrapper's run stays open
Requirement R11: Resource release and finalizationabout:req:R11
This page explains requirement R11 in Effect4. It covers what the requirement asks for resource release guarantees, why disciplined finalization matters, and how the property is checked.
What the requirement asksabout:req:R11:what-it-asks
Requirement R11 demands that allocated resources are released reliably across all exit paths (docs/core/system-map. §8, DB-07):
- At-most-once release: each registered cleanup executes at most once per registration, counted by identity.
- Strict close order: finalizers execute in reverse registration order across closed scopes and structured regions.
- State-first cleanup: a scope sets its closed bit before running any finalizer, preventing duplicate or re-entrant execution.
- Frontier state retention: state produced before reaching a live frontier is kept intact for subsequent continuation.
A scope that finishes cleanly or encounters a failure must not leak registered resources.
Why it mattersabout:req:R11:why-it-matters
Concurrent applications acquire external resources including file handles, database transactions, network sockets, and timer registrations.
If finalizers ran out of order or executed multiple times, systems would suffer from use-after-free defects or corrupted state.
Cleanup in the reverse order of acquisition releases a resource before the resources it depends on.
How it is checkedabout:req:R11:how-it-is-checked
The requirement is checked by proving scope transition, close ordering, and finalizer execution theorems:
- Idempotent closing and reverse-order execution are stated by
close_twiceandcloseOrder_eq(src/Effect4/Machine/Scope.).lean - Re-entrant addition semantics on closed scopes is stated by
close_reentrant_addin the same file. - Single close execution bounds are stated by
runState_completeandrunState_prefix(src/Effect4/Laws/Machine/ScopeMachine.).lean - Finalizer start bounding is stated by
starts_le_pushes(src/Effect4/Laws/Program/FinalizerRun.).lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- once_placed_pushes_once goal
- cleans_once modulo → log_debits
- log_debits goal
- QueueWorkers.releases_once modulo → cleanup_step
- cleanup_step modulo → logs_history
- logs_history goal
- cleanup_keeps goal
- Workers.releases_once modulo → logs_step
- logs_step goal
The figure in words
- Scope Lifetime & Finalization open, 256 nodes, 9 open → Initial Algebras & Folds, Reactive Scheduling, No concept, Store Typing, Subtyping Algebra, Residual Program Typing, Host Session Protocol, Translation & Simulation
- Reactive Scheduling proved, 5 nodes
- Host Session Protocol proved, 2 nodes
- Translation & Simulation proved, 17 nodes → No concept
- No concept proved, 13 nodes → Store Typing, Initial Algebras & Folds, Subtyping Algebra, Residual Program Typing, Exact Codecs
- Initial Algebras & Folds proved, 9 nodes
- Store Typing proved, 10 nodes → Subtyping Algebra, No concept
- Subtyping Algebra proved, 44 nodes → No concept
- Residual Program Typing proved, 14 nodes → Subtyping Algebra, Store Typing, No concept, Exact Codecs, Initial Algebras & Folds
- Exact Codecs proved, 1 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
runState_complete | proved | — | — |
runState_restore | proved | — | runState_complete |
runState_prefix | proved | — | — |
close_twice | proved | — | close_idempotent |
close_reentrant_add | proved | — | — |
closeOrder_eq | proved | — | — |
saved_mask_restoration | proved | — | at_append |
replace_sum | proved | — | — |
replace_sum_le_omitted | proved | — | replace_sum |
finalizerOr_debit | proved | — | step_debit, getCont_le |
getCont_le | proved | — | — |
step_debit | proved | — | getCont_le |
getCont_spec | proved | — | — |
StackLedger. | proved | — | replace_sum, driveState_lift |
saved_mask_chain_runs | proved | — | driveState_lift |
saved_mask_pop_discipline | proved | — | — |
saved_mask_region_bracket | proved | — | — |
close_refuses | proved | — | — |
drain_waits | proved | — | — |
giveBack_front | proved | — | — |
giveBack_once | proved | — | giveBack_front |
FinalizerRun. | proved | — | evaluatePrim_producer, getCont_le, step_debit, finalizerOr_debit, replace_sum, driveState_lift |
once_placed_pushes_once | goal | once_placed_pushes_once | — |
starts_le_pushes | proved | — | FinalizerRun. |
LedgerFinalizer. | proved | — | evaluatePrim_producer, getCont_le, step_debit, finalizerOr_debit, replace_sum, StackLedger. |
evaluateNative_maskChain | proved | — | evaluatePrim_producer |
evaluateNative_under | proved | — | evaluatePrim_under |
evaluatePrim_producer | proved | — | — |
evaluatePrim_under | proved | — | — |
iteration_currentOpCount | proved | — | evaluatePrim_producer |
iteration_under | proved | — | evaluateNative_under |
AdministrativeKept. | proved | — | noAdd_empty, interrupt, noAdd_cons, terminal |
AdministrativeQueue. | proved | — | — |
armE | proved | — | cancel, exit_credits, stack_credits_bounded, interp_contE |
failure_stack_eq | proved | — | — |
getCont_cause | proved | — | popFrom_cause, failure_stack_eq |
popFrom_cause | proved | — | failure_stack_le, stack_credits_bounded |
resumeCause | proved | — | armE, failure_stack_eq, getCont_cause |
CommandClosure. | proved | — | deliver, loop, AdministrativeQueue., AdministrativeKept., update_credits, emit_credits, failure_fiber_le, replace_sum, link, noAdd_full, exit_credits, resume_command, noAdd_empty, mem_addresses_iff |
joined | proved | — | evaluatePrim_producer, closeOrder_eq, at_append, mem_addresses_iff, CommandClosure. |
read | proved | — | — |
after_add_code_credits | proved | — | fin_program_credits |
async_route_credits | proved | — | — |
close_program_credits | proved | — | fin_program_credits |
compile_credits | proved | — | source_op_credits, async_route_credits |
emit_credits | proved | — | — |
fin_program_credits | proved | — | — |
load_credits | proved | — | compile_credits |
load_funded | proved | — | load_credits |
prog_of_credits | proved | — | fin_program_credits |
registration_template | proved | — | — |
response_credits_bounded | proved | — | — |
source_op_credits | proved | — | — |
stack_before_action | proved | — | — |
stack_before_iterator | proved | — | — |
stack_before_push | proved | — | — |
stack_before_suspend | proved | — | — |
stack_credits_bounded | proved | — | response_credits_bounded |
update_credits | proved | — | replace_sum |
add_memo_credits | proved | — | — |
bind_service_credits | proved | — | — |
build_scope_credits | proved | — | — |
combine_credits | proved | — | — |
constant_push_credits | proved | — | constant_stack_credits |
constant_stack_credits | proved | — | — |
constant_start | proved | — | — |
contA_credits | proved | — | bind_service_credits, service_lookup_credits, merge_context_credits, combine_credits, provide_then_credits, layer_resolve_credits, layer_construction_credits, registration_template, layer_inner_credits, add_memo_credits, build_scope_credits, update_body_credits, provide_body_credits, provide_layer_credits, fin_program_credits, store_contA_credits, exit_credits, resolve_credits |
contE_credits | proved | — | store_contE_credits, exit_credits, resolve_credits |
context_credits | proved | — | — |
exit_credits | proved | — | — |
failure_fiber_le | proved | — | failure_stack_le |
failure_stack_le | proved | — | — |
forced_yield_iteration | proved | — | constant_start |
forced_yield_loop_funded | proved | — | emit_credits, update_credits, forced_yield_iteration, loop_of_iteration |
layer_compile_credits | proved | — | — |
layer_construction_credits | proved | — | — |
layer_inner_credits | proved | — | layer_compile_credits, layer_resolve_credits |
layer_resolve_credits | proved | — | layer_with_credits |
layer_with_credits | proved | — | layer_compile_credits, layer_zero_credits |
layer_zero_credits | proved | — | layer_compile_credits |
loop_top_credits | proved | — | failure_stack_le |
merge_context_credits | proved | — | — |
provide_body_credits | proved | — | exit_credits |
provide_layer_credits | proved | — | — |
provide_then_credits | proved | — | — |
region_credits | proved | — | layer_resolve_credits, resolve_credits |
resolve_credits | proved | — | compile_credits |
service_lookup_credits | proved | — | — |
store_contA_credits | proved | — | prog_of_credits, store_exit_credits |
store_contE_credits | proved | — | store_exit_credits |
store_exit_credits | proved | — | — |
suspend_credits | proved | — | prog_of_credits, compile_credits, resolve_credits |
update_body_credits | proved | — | — |
yield_wrapper_credits | proved | — | constant_stack_credits |
Execution. | proved | — | decision, at_append, mem_addresses_iff, RuntimeShape., Execution. |
Execution. | proved | — | load_funded |
outer_custody | proved | — | ready_update, ready_emit, failure_fiber_le |
ready_emit | proved | — | emit_credits |
ready_update | proved | — | update_credits |
armA_counts | proved | — | — |
armE_counts | proved | — | — |
finalizerEvents_no_push | proved | — | — |
frame_failure_le | proved | — | failure_stack_le |
getCont_no_push | proved | — | popFrom_no_push |
interp_loopEnter | proved | — | loopNext_credits |
interp_suspend | proved | — | suspend_credits |
joinPushed_no_push | proved | — | passPushed_no_push, noPush_append |
noPush_append | proved | — | — |
noPush_counts | proved | — | — |
passEvents_no_push | proved | — | — |
passPushed_no_push | proved | — | passEvents_no_push |
popFrom_no_push | proved | — | joinPushed_no_push, noPush_append, passEvents_no_push |
push_onSuccess | proved | — | stack_before_push |
registrations_append | proved | — | — |
resumeCause_counts | proved | — | armE_counts, registrations_append, starts_append, finalizerEvents_no_push, getCont_no_push, noPush_counts |
resumeValue_counts | proved | — | armA_counts, registrations_append, starts_append, finalizerEvents_no_push, getCont_no_push, noPush_counts |
stack_full | proved | — | — |
starts_append | proved | — | — |
FrameDebit. | proved | — | interp_loopEnter, stack_full, constant_stack_credits, push_onSuccess, stack_before_iterator, armA_counts, armA, frame_failure_le, withFiber_suspend_le, stack_before_action, stack_credits_bounded, stack_before_suspend, interp_suspend, sync_stack_le, resumeCause_counts, resumeCause, resumeValue_counts, resumeValue |
sync_stack_le | proved | — | response_credits_bounded |
withFiber_suspend_le | proved | — | — |
FrameSequencing. | proved | — | constant_push_kept, noAdd_cons, noAdd_append, armA_noAdd, interrupt, resumeCause_kept, resumeValue_kept, opaque_noAdd |
decision | proved | — | driveState_lift, interrupt, ready_update, ready_emit, failure_fiber_le, closeOrder_eq, at_append, mem_addresses_iff, evaluatePrim_producer, joined, AdministrativeKept., update_credits, emit_credits, replace_sum, link, noAdd_full, exit_credits, resume_command, noAdd_empty, fold_lift |
fold_lift | proved | — | ready_emit, ready_update, joined, closeOrder_eq, at_append, mem_addresses_iff, evaluatePrim_producer, driveState_lift |
deliver | proved | — | noAdd_empty, interrupt, NativeMachineShape., replace_sum, failure_fiber_le, mem_addresses_iff, NativeScopeDebit., evaluatePrim_producer, native_returned |
loop | proved | — | noAdd_empty, interrupt, NativeMachineShape., replace_sum, failure_fiber_le, mem_addresses_iff, NativeIterationDebit., evaluatePrim_producer, iteration_returned |
sync_op | proved | — | after_add_exit_credit, add_open, replace_sum, after_add_unit_credit, syncOp, noAdd_full |
NativeIterationDebit. | proved | — | yield_wrapper_credits, forced_wrapper, NativeScopeDebit., loop_top_credits, loop_top_source, loop_top |
NativeMachineShape. | proved | — | noAdd_empty, interrupt |
NativeMachineShape. | proved | — | noAdd_empty, interrupt |
primitive | proved | — | noAdd_full, async_noAdd, stable_full, yield_stable, layer_resolve_credits, prog_of_credits, region_credits, resolve_credits, compile_credits, at_append, mem_addresses_iff, close, link, opaque_noAdd, resumeCause_counts, resumeValue_counts, FrameDebit., syncOp, sync_op, sync_stack_le, failure_stack_le, getCont_cause, getCont_no_push, noPush_counts, fin_program_credits, getCont_value, exit_pop_noAdd |
NativeScopeDebit. | proved | — | fin_program_credits, close_scope, replace_sum, noAdd_full, exit_credits, failure_stack_le, getCont_cause, getCont_value, exit_pop_noAdd, getCont_no_push, noPush_counts, resolve_credits, opaque_noAdd, primitive |
action_noAdd | proved | — | noAdd_mask, noAdd_asyncFinalizer |
action_not_finished | proved | — | — |
action_returned | proved | — | action_not_finished, action_noAdd, returned_clean |
countdown_noAdd | proved | — | action_noAdd |
exit_pop_noAdd | proved | — | getCont_cause_kept, getCont_value_finalizer |
finalizer_returned | proved | — | step_frame, returned_clean, exit_pop_noAdd |
frame_step | proved | — | FrameSequencing. |
iteration_returned | proved | — | forced_wrapper, native_returned, loop_top_source, loop_top |
loop_top | proved | — | interrupt |
loop_top_source | proved | — | — |
native_returned | proved | — | scoped_exit_returned, primitive_returned, returned_clean, opaque_noAdd |
primitive_returned | proved | — | async_noAdd, stable_value, yield_stable, action_returned, countdown_noAdd, noAdd_asyncFinalizer, returned_clean, value_response, finalizer_returned, opaque_noAdd, step_frame |
returned_clean | proved | — | — |
scoped_exit_returned | proved | — | returned_clean, exit_pop_noAdd |
step_frame | proved | — | noAdd_empty, returned_clean, frame_step |
armA | proved | — | iterator_future, interp_iter, interp_loopResume, exit_credits, after_add_code_credits, stack_credits_bounded, interp_contA |
getCont_value | proved | — | failure_stack_le, value_cap |
resumeValue | proved | — | armA, getCont_value |
value_cap | proved | — | stack_credits_bounded, response_credits_bounded |
answerOf_clean | proved | — | — |
armA_noAdd | proved | — | — |
armE_noAdd | proved | — | noAdd_empty |
constant_push_kept | proved | — | forced_unwrap, forced_push, noAdd_cons, opaque_noAdd |
ensure_noAdd | proved | — | — |
forced_unwrap | proved | — | — |
getCont_cause_kept | proved | — | popFrom_cause_kept |
getCont_noAdd | proved | — | noAdd_empty, popFrom_noAdd |
getCont_value_finalizer | proved | — | popFrom_value_finalizer |
noAdd_append | proved | — | — |
noAdd_cons | proved | — | — |
noAdd_tail | proved | — | — |
passPushed_noAdd | proved | — | answerOf_clean, ensure_noAdd, noAdd_tail |
popFrom_cause_kept | proved | — | noAdd_empty, popFrom_noAdd |
popFrom_noAdd | proved | — | noAdd_append, answerOf_clean, passPushed_noAdd, ensure_noAdd, noAdd_tail |
popFrom_value_finalizer | proved | — | noAdd_empty, popFrom_noAdd |
resumeCause_clean | proved | — | noAdd_append, armE_noAdd, getCont_noAdd |
resumeCause_kept | proved | — | noAdd_append, armE_noAdd, getCont_cause_kept |
resumeValue_clean | proved | — | noAdd_append, armA_noAdd, getCont_noAdd |
resumeValue_kept | proved | — | interrupt, resumeValue_kept_clear |
resumeValue_kept_clear | proved | — | resumeValue_clean |
cancel | proved | — | store_cancel |
closeSeq_credits | proved | — | fin_program_credits |
interp_contA | proved | — | contA_credits |
interp_contE | proved | — | contE_credits |
interp_iter | proved | — | closeSeq_credits, runStmts_credits |
interp_loopResume | proved | — | loopResume_credits |
iterator_future | proved | — | — |
loopFinish_credits | proved | — | — |
loopNext_credits | proved | — | loopFinish_credits, resolve_credits |
loopResume_credits | proved | — | loopNext_credits |
runStmts_credits | proved | — | yieldOf_credits |
store_cancel | proved | — | — |
yieldOf_credits | proved | — | compile_credits |
terminal | proved | — | mem_addresses_iff, stable_refGet, stable_cause, stable_value |
RuntimeShape. | proved | — | noAdd_empty |
close | proved | — | close_program_credits, close_scope, replace_sum |
link | proved | — | replace_sum, add_open |
syncOp | proved | — | replace_sum, after_add_exit_credit, add_open, after_add_unit_credit |
acquired_registration | proved | — | — |
async_noAdd | proved | — | opaque_noAdd |
async_producer | proved | — | noAdd_asyncFinalizer, async_noAdd |
forced_push | proved | — | — |
forced_wrapper | proved | — | — |
interrupt | proved | — | — |
Sequencing. | proved | — | noAdd_empty |
noAdd_asyncFinalizer | proved | — | — |
noAdd_empty | proved | — | — |
noAdd_full | proved | — | — |
noAdd_mask | proved | — | — |
opaque_noAdd | proved | — | — |
raw_yield_excluded | proved | — | — |
registration_step | proved | — | opaque_noAdd |
resume_command | proved | — | emit_credits, resume_frame_debit, update_credits |
resume_frame_debit | proved | — | stable_full |
saved_resume | proved | — | — |
stable_cause | proved | — | — |
stable_full | proved | — | noAdd_full |
stable_refGet | proved | — | — |
stable_value | proved | — | — |
value_response | proved | — | — |
yield_producer | proved | — | stable_value, yield_stable |
yield_response_full | proved | — | noAdd_full |
yield_stable | proved | — | — |
add_open | proved | — | — |
after_add_exit | proved | — | after_add_exit_credit |
after_add_exit_credit | proved | — | — |
after_add_unit | proved | — | after_add_unit_credit |
after_add_unit_credit | proved | — | — |
close_chain_transfer | proved | — | close_scope |
close_scope | proved | — | closeOrder_eq |
close_seq_command | proved | — | close_seq_start |
close_seq_start | proved | — | — |
foreign_suspension | proved | — | — |
release_loop_debit | proved | — | release_start_debit, release_start, iteration_below_budget, loop_of_iteration |
release_start | proved | — | — |
release_start_count | proved | — | release_start |
release_start_debit | proved | — | release_start_registered, release_start_count |
release_start_registered | proved | — | release_start |
scope_add_closed | proved | — | after_add_exit_credit, native_sync_op |
scope_add_open | proved | — | add_open, after_add_unit_credit, native_sync_op |
StackRegion. | proved | — | evaluateNative_under, evaluatePrim_producer, iteration_under |
compiled_region_bracket_of_prefix | proved | — | compiled_region_bracket, stepped_live, drive |
drive | proved | — | StackRegion., evaluatePrim_producer, guarded_driveStep_liveTransports |
settle_callback | proved | — | fits_subN, fits_mono, subN_never, subN_refl, order_refl, scopeParams_child, at_child, order_trans, fits_scope_inv, seq_typed, closeOrder_eq, mono, satisfies_empty, configTyped_frame, hom_eq_cata_ty |
clause_closeScope | proved | — | fits_mono, order_trans, mono, subN_never, fits_subN, order_refl, scopeParams_child, at_child, fits_scope_inv, seq_typed, closeOrder_eq, satisfies_empty, configTyped_frame, hom_eq_cata_ty |
clause_scoped | proved | — | fits_mono, order_trans, mono, order_refl, satisfies_empty, denotesTyped, configTyped_frame, hom_eq_cata_ty |
foreignFinalizer_ambient | proved | — | subN_never, fits_subN, fits_mono, order_refl, scopeParams_child, at_child, order_trans |
compiled_mask_chain_runs | proved | — | evaluateNative_maskChain, evaluatePrim_producer, driveState_lift |
compiled_region_bracket | proved | — | stepped_live |
guarded_driveStep_liveTransports | proved | — | evaluatePrim_producer |
stepped_live | proved | — | — |
log_debits | goal | log_debits | checkInput_eq_none_iff |
cleans_once | modulo | log_debits | Scenario., build_retains, checkInput_eq_none_iff, replace_sum, mem_addresses_iff, at_append, closeOrder_eq, evaluatePrim_producer, replace_sum_le_omitted, driveState_lift, starts_le_pushes, log_debits |
crew_acquire_once_placed | proved | — | workers_placement, workers_built_program, checkInput_eq_none_iff |
queueCrew_acquire_once_placed | proved | — | queue_placement, queue_built_program, checkInput_eq_none_iff |
queue_acquisition_sites | proved | — | — |
queue_placement | proved | — | — |
workers_acquisition_sites | proved | — | — |
workers_placement | proved | — | — |
cleanup_step | modulo | logs_history | releases, registrations, logs_history, reached_history, checkInput_eq_none_iff |
logs_history | goal | logs_history | checkInput_eq_none_iff |
registrations | proved | — | queue_built_program, checkInput_eq_none_iff, replace_sum, mem_addresses_iff, at_append, closeOrder_eq, evaluatePrim_producer, replace_sum_le_omitted, driveState_lift |
releases | proved | — | queue_built_program, checkInput_eq_none_iff, Execution., read |
QueueWorkers. | modulo | logs_history | cleanup_step, checkInput_eq_none_iff, reached_history, ledger_opened, queueCrew_acquire_once_placed, queue_acquisition_sites, queue_built_program |
cleanup_keeps | goal | cleanup_keeps | checkInput_eq_none_iff |
logs_step | goal | logs_step | checkInput_eq_none_iff |
registrations_step | proved | — | workers_built_program, checkInput_eq_none_iff, replace_sum, mem_addresses_iff, at_append, closeOrder_eq, evaluatePrim_producer, replace_sum_le_omitted, driveState_lift |
releases_step | proved | — | workers_built_program, checkInput_eq_none_iff, Execution., read |
Workers. | modulo | logs_step | logs_step, releases_step, registrations_step, checkInput_eq_none_iff, crew_acquire_once_placed, workers_acquisition_sites, workers_built_program, Scenario. |
close_idempotent | proved | — | — |
at_append | proved | — | — |
driveState_lift | proved | — | — |
mem_addresses_iff | proved | — | yieldAt_addressYield, mem_foldList_iff, addresses_eq_foldList |
loop_of_iteration | proved | — | — |
iteration_below_budget | proved | — | — |
native_sync_op | proved | — | — |
fits_subN | proved | — | subN_trans, fits_normalize |
fits_mono | proved | — | — |
subN_never | proved | — | — |
subN_refl | proved | — | — |
order_refl | proved | — | — |
scopeParams_child | proved | — | — |
at_child | proved | — | at_append |
order_trans | proved | — | — |
fits_scope_inv | proved | — | — |
seq_typed | proved | — | subN_refl, fits_subN, guardBind_typed |
mono | proved | — | order_trans |
satisfies_empty | proved | — | — |
configTyped_frame | proved | — | satisfies_empty, fits_mono, order_trans, mono, order_refl, hom_eq_cata_ty |
hom_eq_cata_ty | proved | — | — |
denotesTyped | proved | — | provideLayerArm, at_child, subN_refl, fits_subN, fits_normalize, fiberTy_upper, scopeParams_child, hom_eq_cata_ty, subN_trans, matchB_sound, syncRow_typed, withParams_of_none, listOf_upper, normalize_idem, lift_sound, causeInputError_upper, matchArgsB_sound, errOf_payload, isPayload_of_hasTy_record, satisfies_weaken, subN_never, fits_mono, order_trans, invoke_arm, optionTy_upper, withParams_serviceTy, scopeParams_below, exitOf_upper, fits_scope_inv, param_arm, call_arm |
checkInput_eq_none_iff | proved | — | — |
Scenario. | proved | — | reached_history |
build_retains | proved | — | finishBuild_retains, checkInput_eq_none_iff |
workers_built_program | proved | — | workers_elaborates, build_retains, checkInput_eq_none_iff |
queue_built_program | proved | — | queue_elaborates, build_retains, checkInput_eq_none_iff |
reached_history | proved | — | — |
ledger_opened | proved | — | opened_exit |
yieldAt_addressYield | proved | — | — |
mem_foldList_iff | proved | — | exists_at_of_mem_foldList |
addresses_eq_foldList | proved | — | — |
subN_trans | proved | — | — |
fits_normalize | proved | — | subN_trans, normalize_idem |
guardBind_typed | proved | — | — |
provideLayerArm | proved | — | fits_subN, subN_refl, fits_normalize, fiberTy_upper, scopeParams_child, at_child, hom_eq_cata_ty, subN_trans, matchB_sound, syncRow_typed, withParams_of_none, listOf_upper, normalize_idem, lift_sound, causeInputError_upper, matchArgsB_sound, errOf_payload, isPayload_of_hasTy_record, satisfies_weaken, subN_never, fits_mono, order_trans, fits_scope_inv |
fiberTy_upper | proved | — | fiber_eliminator, normalize_idem, subN_trans, subN_refl, extendAll_upper |
matchB_sound | proved | — | lookup_solve_seed |
syncRow_typed | proved | — | fits_normalize, subN_trans, fits_subN, termMaps_of_typed, matchB_sound, hom_eq_cata_ty, errOf_payload, isPayload_of_hasTy_record, normalize_idem, subN_refl |
withParams_of_none | proved | — | — |
listOf_upper | proved | — | list_eliminator, normalize_idem, subN_trans, subN_refl, extendAll_upper |
normalize_idem | proved | — | — |
lift_sound | proved | — | lift_transfer |
causeInputError_upper | proved | — | cause_upper, cause_mono, normalize_idem, subN_trans, subN_refl, UnionRule., subN_causeOf_causeUpper, subN_exitOf_causeUpper, extendAll_eq_some_iff |
matchArgsB_sound | proved | — | — |
errOf_payload | proved | — | — |
isPayload_of_hasTy_record | proved | — | handles_of_payloadFieldTy |
satisfies_weaken | proved | — | — |
invoke_arm | proved | — | normalize_idem, fits_mono, fits_subN, order_trans, at_child, scopeParams_below, listOf_upper, fits_normalize, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty, scopeParams_body, withParams_defOf |
optionTy_upper | proved | — | option_eliminator, normalize_idem, subN_trans, subN_refl, Eliminator. |
withParams_serviceTy | proved | — | — |
scopeParams_below | proved | — | — |
exitOf_upper | proved | — | exit_eliminator, normalize_idem, subN_trans, subN_refl, extendAll_upper |
param_arm | proved | — | normalize_idem, fits_mono, fits_subN, order_trans, listOf_upper, fits_normalize, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty, scopeParams_decl, withParams_param |
call_arm | proved | — | fits_mono, fits_subN, normalize_idem, order_trans, listOf_upper, fits_normalize, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty, scopeParams_body, withParams_of_none |
finishBuild_retains | proved | — | checkInput_eq_none_iff |
workers_elaborates | proved | — | workers_refs_nil, workers_main_eq, elaborateModule_no_declarations |
queue_elaborates | proved | — | queue_refs_nil, queue_main_eq, elaborateModule_no_declarations |
opened_exit | proved | — | exit_eq |
exists_at_of_mem_foldList | proved | — | sizeOf_child_lt, foldList_cases |
fiber_eliminator | proved | — | subN_fiberOf_iff, normalize_idem, subN_trans, subN_refl |
extendAll_upper | proved | — | extendAll_adjoint |
lookup_solve_seed | proved | — | — |
termMaps_of_typed | proved | — | listOf_upper, fits_subN, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty, fits_mono |
list_eliminator | proved | — | subN_list_iff, normalize_idem, subN_trans, subN_refl |
lift_transfer | proved | — | joinAll_keeps, mapM_answer |
cause_upper | proved | — | subN_causeOf_causeUpper, subN_exitOf_causeUpper |
cause_mono | proved | — | subN_exitOf_iff, subN_causeOf_causeUpper, subN_trans, subN_causeOf_iff |
UnionRule. | proved | — | le_joinAll, subN_trans, mapM_answer |
subN_causeOf_causeUpper | proved | — | — |
subN_exitOf_causeUpper | proved | — | subN_trans, subN_refl, subN_exitOf_iff |
extendAll_eq_some_iff | proved | — | — |
handles_of_payloadFieldTy | proved | — | — |
scopeParams_body | proved | — | — |
withParams_defOf | proved | — | — |
option_eliminator | proved | — | subN_option_iff, normalize_idem, subN_trans, subN_refl |
Eliminator. | proved | — | subN_refl, UnionRule. |
exit_eliminator | proved | — | subN_exitOf_iff, normalize_idem, subN_trans, subN_refl |
scopeParams_decl | proved | — | — |
withParams_param | proved | — | — |
workers_refs_nil | proved | — | — |
workers_main_eq | proved | — | workers_main_some, elaboration_eq_getD |
elaborateModule_no_declarations | proved | — | — |
queue_refs_nil | proved | — | — |
queue_main_eq | proved | — | queue_main_some, elaboration_eq_getD |
exit_eq | proved | — | — |
sizeOf_child_lt | proved | — | — |
foldList_cases | proved | — | — |
subN_fiberOf_iff | proved | — | — |
extendAll_adjoint | proved | — | adjoint, extendAll_eq_some_iff |
subN_list_iff | proved | — | — |
joinAll_keeps | proved | — | foldl_keeps |
mapM_answer | proved | — | mapM_cons_eq_some |
subN_exitOf_iff | proved | — | — |
subN_causeOf_iff | proved | — | — |
le_joinAll | proved | — | joinAll_keeps |
subN_option_iff | proved | — | — |
workers_main_some | proved | — | — |
elaboration_eq_getD | proved | — | — |
queue_main_some | proved | — | — |
adjoint | proved | — | Eliminator., subN_trans, mapM_total, Eliminator. |
foldl_keeps | proved | — | — |
mapM_cons_eq_some | proved | — | — |
Eliminator. | proved | — | UnionRule. |
mapM_total | proved | — | mapM_cons_eq_some |
UnionRule. | proved | — | subN_trans, mapM_source, joinAll_le |
mapM_source | proved | — | mapM_cons_eq_some |
joinAll_le | proved | — | joinAll_all |
joinAll_all | proved | — | foldl_all |
foldl_all | proved | — | — |