R6: The host: a lawful HostSpec, receipt and application, DI-57's table-aware referencereq:R6
- Open, waits on a ruling (decisions row 97: the handle declarations, parked by the owner on 2026-09-30): admit_sound's value half: executable admission implies the ghost AnswerOk on success values (waits on decisions row 97's handle declarations)
- Open, needs a definition (the host as a relation between the machine's calls and its answers (`HostSpec`), in place of a predicate on tapes): H related to the machine: M6's premise is a predicate on tapes (decisions row 95), not a host relation
- Open, waits on a ruling (decisions rows 98 to 100: the typed replay route, when the guarantee is claimed, host resources): receipt and application on the keyed lifecycle, and their converse (host-boundary §4.5; decisions rows 98–100, parked by the owner, 2026-09-30)
- Open, not triaged: a world extension meeting C5, a retirement edge, per-row cancellation, one root (DI-58, DI-65)
- Open, after other work (the table-aware reference and the reply correspondence above; decisions row 99 says when it is claimed): the public typed guarantee for programs using host services (decisions row 99)
- Open, worded as a proposed claim: expansion-keeps-call (proposed claim; host-session-protocol): the expansion of a program's layer references keeps a call at its address, so the instance that the session reads on the expanded program is the checker's answer at the call that ran; origin_addresses_call proves the address on the program itself, and a finite evaluation reads the instance (Test/Api/TypedReplies.lean) (decisions row 323)
- Open, worded as a proposed claim: replay-at-call-instance (proposed claim; host-session-protocol): the checked replay of a tape (replayCheckedFrom, Api.replay) and the OCaml engine still admit a reply at the row's own columns alone, so a tape that a session recorded with an answer admitted at its call's instance is refused there (decisions row 323)
Requirement R6: The host boundaryabout:req:R6
This page explains requirement R6 in Effect4. It covers what the requirement asks for external host interactions, why keyed host boundaries matter, and how the property is checked.
What the requirement asksabout:req:R6:what-it-asks
Requirement R6 demands that host interactions satisfy formal specifications and keyed session contracts (docs/core/system-map. §8, docs/core/host-boundary.):
- Host specification: external interactions follow a specification
H : HostSpecsatisfyingLawfulHostSpec. - Receipt and application: host answers submit through preflight checks and apply at most once.
- Envelope matching: replies correlate to waiting calls by matching version, session, call identifier, key, and row.
- Handle protection: internal handle kinds like cells and scopes are prohibited from crossing host boundaries (decisions row 97).
External replies must satisfy typing admission before resuming waiting fibers.
Why it mattersabout:req:R6:why-it-matters
Asynchronous software interacts with untrusted external environments such as web APIs, database drivers, and operating system calls.
If host completions bypassed verification, malformed data or duplicated callbacks could corrupt internal memory or trigger invalid transitions.
A defined host boundary lets a host's replies meet the machine's invariants without assuming that the host makes progress.
How it is checkedabout:req:R6:how-it-is-checked
The requirement is checked by proving reply admission, call correlation, and session agreement theorems:
- Admitted success preparation is stated by
preflight_success_prepared_fits(src/Effect4/Laws/Api/HostSession.).lean - Defect-free failure admission is stated by
preflight_failure_noShapeDefectin the same file. - Call instance correlation is stated by
instance_prepared_success(src/Effect4/Laws/Program/Admit.).lean - Session agreement with reference replay is stated by
session_eq_ref(src/Effect4/Laws/Api/SessionRef.).lean - Host comodel meaning is stated by
denoteRows_eq_session_host(src/Effect4/Laws/Api/SessionMeaning.).lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- reachable_typed modulo → decision_preserves
- bound_in_tree modulo → request_leads
- request_leads goal
- timeout modulo → cleanup_keeps, retries_declared
- workers modulo → releases_once
- decision_preserves modulo → deliver_preserves, loop_preserves
- cleanup_keeps goal
- retries_declared goal
- releases_once modulo → logs_step
- deliver_preserves modulo → countdown_parks_positional
- loop_preserves modulo → countdown_parks_positional
- logs_step goal
- countdown_parks_positional goal
The figure in words
- No concept open, 29 nodes, 4 open → Store Typing, Initial Algebras & Folds, Translation & Simulation, Host Session Protocol, Subtyping Algebra, Residual Program Typing, Reactive Scheduling, Scope Lifetime & Finalization, Exact Codecs
- Host Session Protocol open, 24 nodes, 2 open → No concept, Initial Algebras & Folds, Translation & Simulation, Reactive Scheduling, Scope Lifetime & Finalization
- Translation & Simulation open, 45 nodes, 3 open → No concept, Host Session Protocol, Initial Algebras & Folds, Reactive Scheduling
- Store Typing proved, 12 nodes → Subtyping Algebra, No concept
- Initial Algebras & Folds proved, 22 nodes → No concept
- Reactive Scheduling open, 3 nodes, 1 open
- Scope Lifetime & Finalization open, 187 nodes, 3 open → No concept, Translation & Simulation, Host Session Protocol, Initial Algebras & Folds, Reactive Scheduling, Store Typing, Subtyping Algebra, Residual Program Typing
- Subtyping Algebra proved, 44 nodes → No concept
- Residual Program Typing proved, 17 nodes → Subtyping Algebra, Store Typing, No concept, Exact Codecs, Initial Algebras & Folds
- Exact Codecs proved, 1 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
reachable_typed | modulo | countdown_parks_positional | decision_preserves, load_typed, order_trans, order_refl |
preflight_success_prepared_fits | proved | — | instance_prepared_success |
preflight_failure_noShapeDefect | proved | — | — |
instance_prepared_success | proved | — | — |
origin_addresses_call | proved | — | at_append, funded_replays |
reached_callInstance | proved | — | lookup_programCalls |
session_eq_ref | proved | — | run_eq_ref_table, journal_replays, funded_replays |
denoteRows_eq_session_host | proved | — | denoteRowsB_straight, localRunC_compileB, funded_replays |
runWith_denotes | proved | — | denoteRows_eq_session_host, allows_answer, observe_awaitingAsync_iff, tapeFrom_append |
h8_loopedRows | proved | — | hostRunB_stable, localRunC_to_rowsB, localRunC_compileB, funded_replays |
denoteRowsB_eq_session_host | proved | — | hostRunB_stable, localRunC_to_rowsB, funded_replays |
runWith_denotesB | proved | — | denoteRowsB_eq_session_host, allows_answer, observe_awaitingAsync_iff, tapeFrom_append |
compilesBO_bind | proved | — | at_append |
compilesBO_catchCause | proved | — | at_append |
compilesBO_catchIf | proved | — | at_append |
compilesBO_exit | proved | — | denoteRowsB_straight, at_append |
compilesBO_iterate | proved | — | at_append |
compilesBO_matchCause | proved | — | at_append |
compilesBO_onExit | proved | — | at_append |
compilesBO_select | proved | — | at_append |
compilesBO_suspend | proved | — | at_append |
localRunC_compileB | proved | — | localRunC_compileBO |
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 |
localRunC_to_rowsB | proved | — | localRunC_compileB |
localWaitC_to_rowsB | proved | — | localRunC_compileBO |
bodyAt | proved | — | — |
hostRunB_stable | proved | — | — |
observeRows_project | proved | — | — |
partAt_at | proved | — | bodyAt_at |
partAt_of_hasTy | proved | — | — |
bodyAt_at | proved | — | — |
run_eq_ref_table | proved | — | at_append |
checkModule_programCallAt | proved | — | checkModule_sound, moduleHasTy_programCallAt |
handles_of_payloadFieldTy | proved | — | — |
hasTy_callAt | proved | — | checkRow_rowBindings, focusAt_typed, hasTy_focusAt |
lookup_programCalls | proved | — | mem_addresses_iff, programCallAt_rowTy |
moduleHasTy_programCallAt | proved | — | partAt_of_hasTy, hasTy_callAt, bodyAt |
programCallAt_rowTy | proved | — | partAt_at, callAt_rowTy |
bound_in_tree | modulo | request_leads | denoteRowsB_straight, localWaitC_to_rowsB, request_leads, driveState_lift, evaluatePrim_producer, reached |
request_leads | goal | request_leads | — |
applied_selects | proved | — | — |
control_retires | proved | — | — |
denoteRows_eq_session | proved | — | denoteRowsB_straight, localRunC_compileB, funded_replays |
ending_of_tape | proved | — | funded_replays |
runWith_guarded_denotes | proved | — | hom_eq_cata_ty, runWith_denotes |
runWith_guarded_denotesB | proved | — | hom_eq_cata_ty, runWith_denotesB |
runWith_host_denotes | proved | — | runWith_guarded_denotes |
runWith_host_denotesB | proved | — | runWith_guarded_denotesB |
runWith_layer_denotes | proved | — | runWith_host_denotes |
sessionSystem_finished | proved | — | denoteRows_eq_session_host |
sessionSystem_finishes | proved | — | denoteRows_eq_session_host |
session_keys_once | proved | — | driveState_lift, evaluatePrim_producer, reached |
stale_never_applies | proved | — | checkInput_eq_none_iff |
timeout | modulo | cleanup_keeps, retries_declared | cleanup_keeps, stale_never_applies, retries_declared, checkInput_eq_none_iff |
workers | modulo | logs_step | releases_once, control_retires, applied_selects, receipt_inert, checkInput_eq_none_iff |
receipt_inert | proved | — | — |
decision_preserves | modulo | countdown_parks_positional | fits_subN, satisfies_empty, order_refl, fits_mono, order_trans, mono, subN_trans, configTyped_frame, hom_eq_cata_ty, wake_preserves, close_typed, seq_typed, registrationDone_preserves, launch_preserves, subN_never, guardBind_typed, deliver_preserves, loop_preserves, driveState_lift |
load_typed | proved | — | denotesTyped, checkModule_eq_check, check_complete, checkModule_sound, satisfies_empty |
order_trans | proved | — | — |
order_refl | proved | — | — |
at_append | proved | — | — |
funded_replays | proved | — | journal_replays, tape_replays |
journal_replays | proved | — | — |
denoteRowsB_straight | proved | — | — |
allows_answer | proved | — | — |
observe_awaitingAsync_iff | proved | — | — |
tapeFrom_append | proved | — | — |
denoteRows_straight | proved | — | — |
checkModule_sound | proved | — | check_sound |
checkRow_rowBindings | proved | — | — |
focusAt_typed | proved | — | check_sound, focusAt_eq_some |
hasTy_focusAt | proved | — | check_complete, check_sound, focusAt_eq_some, replace_envAt |
mem_addresses_iff | proved | — | yieldAt_addressYield, mem_foldList_iff, addresses_eq_foldList |
callAt_rowTy | proved | — | check_sound, focusAt_eq_some |
driveState_lift | proved | — | — |
evaluatePrim_producer | proved | — | — |
reached | proved | — | — |
hom_eq_cata_ty | proved | — | — |
checkInput_eq_none_iff | proved | — | — |
cleanup_keeps | goal | cleanup_keeps | checkInput_eq_none_iff |
retries_declared | goal | retries_declared | checkInput_eq_none_iff |
releases_once | modulo | logs_step | logs_step, releases_step, registrations_step, checkInput_eq_none_iff, crew_acquire_once_placed, workers_acquisition_sites, workers_built_program, Scenario. |
fits_subN | proved | — | subN_trans, fits_normalize |
satisfies_empty | proved | — | — |
fits_mono | proved | — | — |
mono | proved | — | order_trans |
subN_trans | proved | — | — |
configTyped_frame | proved | — | satisfies_empty, fits_mono, order_trans, mono, order_refl, hom_eq_cata_ty |
wake_preserves | proved | — | order_refl, configTyped_frame, fits_mono, completionStrong_await, hom_eq_cata_ty |
close_typed | proved | — | — |
seq_typed | proved | — | subN_refl, fits_subN, guardBind_typed |
registrationDone_preserves | proved | — | order_refl, fits_mono, order_trans, mono, satisfies_empty, close_typed, fits_subN |
launch_preserves | proved | — | subN_refl, fits_subN, satisfies_empty, order_refl, fits_mono, order_trans, mono, satisfies_weaken |
subN_never | proved | — | — |
guardBind_typed | proved | — | — |
deliver_preserves | modulo | countdown_parks_positional | order_refl, satisfies_empty, fits_mono, order_trans, mono, satisfies_weaken, settle_callback, hom_eq_cata_ty, completionStrong_await, memoBuild_extension, deferredMake_extension, refMake_extension, subN_never, fits_subN, scopeParams_child, at_child, denotesTyped, listOf_upper, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, subN_refl, at_append, scopeParams_below, fiberTy_upper, matchB_sound, syncRow_typed, withParams_of_none, errOf_payload, isPayload_of_hasTy_record, foreignFinalizer_ambient, fits_scope_inv, seq_typed, closeSeqProtocol, configTyped_frame, close_typed, clause_scoped, clause_closeScope, scopeParams_ref, scopeParams_layer_below, satisfies_union, withParams_serviceTy, guardBind_typed, countdown_parks_positional |
loop_preserves | modulo | countdown_parks_positional | order_refl, satisfies_empty, fits_mono, order_trans, mono, satisfies_weaken, settle_callback, hom_eq_cata_ty, completionStrong_await, memoBuild_extension, deferredMake_extension, refMake_extension, subN_never, fits_subN, scopeParams_child, at_child, denotesTyped, listOf_upper, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, subN_refl, at_append, scopeParams_below, fiberTy_upper, matchB_sound, syncRow_typed, withParams_of_none, errOf_payload, isPayload_of_hasTy_record, foreignFinalizer_ambient, fits_scope_inv, seq_typed, closeSeqProtocol, configTyped_frame, close_typed, clause_scoped, clause_closeScope, scopeParams_ref, scopeParams_layer_below, satisfies_union, withParams_serviceTy, guardBind_typed, countdown_parks_positional |
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 |
checkModule_eq_check | proved | — | — |
check_complete | proved | — | — |
tape_replays | proved | — | — |
check_sound | proved | — | — |
focusAt_eq_some | proved | — | — |
replace_envAt | proved | — | child_step |
yieldAt_addressYield | proved | — | — |
mem_foldList_iff | proved | — | exists_at_of_mem_foldList |
addresses_eq_foldList | proved | — | — |
logs_step | goal | logs_step | checkInput_eq_none_iff |
releases_step | proved | — | workers_built_program, checkInput_eq_none_iff, Execution., read |
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 |
crew_acquire_once_placed | proved | — | workers_placement, workers_built_program, checkInput_eq_none_iff |
workers_acquisition_sites | proved | — | — |
workers_built_program | proved | — | workers_elaborates, build_retains, checkInput_eq_none_iff |
Scenario. | proved | — | reached_history |
fits_normalize | proved | — | subN_trans, normalize_idem |
completionStrong_await | proved | — | subN_trans |
subN_refl | proved | — | — |
satisfies_weaken | proved | — | — |
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 |
memoBuild_extension | proved | — | — |
deferredMake_extension | proved | — | — |
refMake_extension | proved | — | — |
scopeParams_child | proved | — | — |
at_child | proved | — | at_append |
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 | — | — |
scopeParams_below | proved | — | — |
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 | — | — |
errOf_payload | proved | — | — |
isPayload_of_hasTy_record | proved | — | handles_of_payloadFieldTy |
foreignFinalizer_ambient | proved | — | subN_never, fits_subN, fits_mono, order_refl, scopeParams_child, at_child, order_trans |
fits_scope_inv | proved | — | — |
closeSeqProtocol | proved | — | order_trans, fits_mono |
clause_scoped | proved | — | fits_mono, order_trans, mono, order_refl, satisfies_empty, denotesTyped, 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 |
scopeParams_ref | proved | — | — |
scopeParams_layer_below | proved | — | — |
satisfies_union | proved | — | — |
withParams_serviceTy | proved | — | — |
countdown_parks_positional | goal | countdown_parks_positional | — |
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 |
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. |
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 |
child_step | proved | — | layersHasTy_cons, at_layers_nil, at_stmts_nil, effTy_map_of_hasTy |
exists_at_of_mem_foldList | proved | — | sizeOf_child_lt, foldList_cases |
Execution. | proved | — | decision, at_append, mem_addresses_iff, RuntimeShape., Execution. |
read | proved | — | — |
replace_sum | proved | — | — |
closeOrder_eq | proved | — | — |
replace_sum_le_omitted | proved | — | replace_sum |
workers_placement | proved | — | — |
workers_elaborates | proved | — | workers_refs_nil, workers_main_eq, elaborateModule_no_declarations |
build_retains | proved | — | finishBuild_retains, checkInput_eq_none_iff |
reached_history | proved | — | — |
list_eliminator | proved | — | subN_list_iff, normalize_idem, subN_trans, subN_refl |
extendAll_upper | proved | — | extendAll_adjoint |
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 | — | — |
fiber_eliminator | proved | — | subN_fiberOf_iff, normalize_idem, subN_trans, subN_refl |
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 |
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 | — | — |
layersHasTy_cons | proved | — | — |
at_layers_nil | proved | — | — |
at_stmts_nil | proved | — | — |
effTy_map_of_hasTy | proved | — | check_complete, check_sound |
sizeOf_child_lt | proved | — | — |
foldList_cases | proved | — | — |
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 |
RuntimeShape. | proved | — | noAdd_empty |
Execution. | proved | — | load_funded |
workers_refs_nil | proved | — | — |
workers_main_eq | proved | — | workers_main_some, elaboration_eq_getD |
elaborateModule_no_declarations | proved | — | — |
finishBuild_retains | proved | — | checkInput_eq_none_iff |
subN_list_iff | proved | — | — |
extendAll_adjoint | proved | — | adjoint, extendAll_eq_some_iff |
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_fiberOf_iff | proved | — | — |
subN_option_iff | proved | — | — |
interrupt | proved | — | — |
ready_update | proved | — | update_credits |
ready_emit | proved | — | emit_credits |
failure_fiber_le | proved | — | failure_stack_le |
joined | proved | — | evaluatePrim_producer, closeOrder_eq, at_append, mem_addresses_iff, command |
AdministrativeKept. | proved | — | noAdd_empty, interrupt, noAdd_cons, terminal |
update_credits | proved | — | replace_sum |
emit_credits | proved | — | — |
link | proved | — | replace_sum, add_open |
noAdd_full | proved | — | — |
exit_credits | proved | — | — |
resume_command | proved | — | emit_credits, resume_frame_debit, update_credits |
noAdd_empty | proved | — | — |
fold_lift | proved | — | ready_emit, ready_update, joined, closeOrder_eq, at_append, mem_addresses_iff, evaluatePrim_producer, driveState_lift |
load_funded | proved | — | load_credits |
workers_main_some | proved | — | — |
elaboration_eq_getD | proved | — | — |
adjoint | proved | — | Eliminator., subN_trans, mapM_total, Eliminator. |
foldl_keeps | proved | — | — |
mapM_cons_eq_some | proved | — | — |
failure_stack_le | proved | — | — |
command | 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 |
noAdd_cons | proved | — | — |
terminal | proved | — | mem_addresses_iff, stable_refGet, stable_cause, stable_value |
add_open | proved | — | — |
resume_frame_debit | proved | — | stable_full |
load_credits | proved | — | compile_credits |
Eliminator. | proved | — | UnionRule. |
mapM_total | proved | — | mapM_cons_eq_some |
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 |
AdministrativeQueue. | proved | — | — |
stable_refGet | proved | — | — |
stable_cause | proved | — | — |
stable_value | proved | — | — |
stable_full | proved | — | noAdd_full |
compile_credits | proved | — | source_op_credits, async_route_credits |
UnionRule. | proved | — | subN_trans, mapM_source, joinAll_le |
NativeMachineShape. | proved | — | noAdd_empty, interrupt |
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 |
native_returned | proved | — | scoped_exit_returned, primitive_returned, returned_clean, opaque_noAdd |
NativeMachineShape. | proved | — | noAdd_empty, interrupt |
NativeIterationDebit. | proved | — | yield_wrapper_credits, forced_wrapper, NativeScopeDebit., loop_top_credits, loop_top_source, loop_top |
iteration_returned | proved | — | forced_wrapper, native_returned, loop_top_source, loop_top |
source_op_credits | proved | — | — |
async_route_credits | proved | — | — |
mapM_source | proved | — | mapM_cons_eq_some |
joinAll_le | proved | — | joinAll_all |
fin_program_credits | proved | — | — |
close_scope | proved | — | closeOrder_eq |
getCont_cause | proved | — | popFrom_cause, failure_stack_eq |
getCont_value | proved | — | failure_stack_le, value_cap |
exit_pop_noAdd | proved | — | getCont_cause_kept, getCont_value_finalizer |
getCont_no_push | proved | — | popFrom_no_push |
noPush_counts | proved | — | — |
resolve_credits | proved | — | compile_credits |
opaque_noAdd | proved | — | — |
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 |
scoped_exit_returned | proved | — | returned_clean, exit_pop_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 | — | — |
yield_wrapper_credits | proved | — | constant_stack_credits |
forced_wrapper | proved | — | — |
loop_top_credits | proved | — | failure_stack_le |
loop_top_source | proved | — | — |
loop_top | proved | — | interrupt |
joinAll_all | proved | — | foldl_all |
popFrom_cause | proved | — | failure_stack_le, stack_credits_bounded |
failure_stack_eq | proved | — | — |
value_cap | proved | — | stack_credits_bounded, response_credits_bounded |
getCont_cause_kept | proved | — | popFrom_cause_kept |
getCont_value_finalizer | proved | — | popFrom_value_finalizer |
popFrom_no_push | proved | — | joinPushed_no_push, noPush_append, passEvents_no_push |
async_noAdd | proved | — | opaque_noAdd |
yield_stable | proved | — | — |
layer_resolve_credits | proved | — | layer_with_credits |
prog_of_credits | proved | — | fin_program_credits |
region_credits | proved | — | layer_resolve_credits, resolve_credits |
close | proved | — | close_program_credits, close_scope, replace_sum |
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 |
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 |
syncOp | proved | — | replace_sum, after_add_exit_credit, add_open, after_add_unit_credit |
sync_op | proved | — | after_add_exit_credit, add_open, replace_sum, after_add_unit_credit, syncOp, noAdd_full |
sync_stack_le | proved | — | response_credits_bounded |
action_returned | proved | — | action_not_finished, action_noAdd, returned_clean |
countdown_noAdd | proved | — | action_noAdd |
noAdd_asyncFinalizer | proved | — | — |
value_response | proved | — | — |
finalizer_returned | proved | — | step_frame, returned_clean, exit_pop_noAdd |
step_frame | proved | — | noAdd_empty, returned_clean, frame_step |
constant_stack_credits | proved | — | — |
foldl_all | proved | — | — |
stack_credits_bounded | proved | — | response_credits_bounded |
response_credits_bounded | proved | — | — |
popFrom_cause_kept | proved | — | noAdd_empty, popFrom_noAdd |
popFrom_value_finalizer | proved | — | noAdd_empty, popFrom_noAdd |
joinPushed_no_push | proved | — | passPushed_no_push, noPush_append |
noPush_append | proved | — | — |
passEvents_no_push | proved | — | — |
layer_with_credits | proved | — | layer_compile_credits, layer_zero_credits |
close_program_credits | proved | — | fin_program_credits |
armE_counts | proved | — | — |
registrations_append | proved | — | — |
starts_append | proved | — | — |
finalizerEvents_no_push | proved | — | — |
armA_counts | proved | — | — |
interp_loopEnter | proved | — | loopNext_credits |
stack_full | proved | — | — |
push_onSuccess | proved | — | stack_before_push |
stack_before_iterator | proved | — | — |
armA | proved | — | iterator_future, interp_iter, interp_loopResume, exit_credits, after_add_code_credits, stack_credits_bounded, interp_contA |
frame_failure_le | proved | — | failure_stack_le |
withFiber_suspend_le | proved | — | — |
stack_before_action | proved | — | — |
stack_before_suspend | proved | — | — |
interp_suspend | proved | — | suspend_credits |
resumeCause | proved | — | armE, failure_stack_eq, getCont_cause |
resumeValue | proved | — | armA, getCont_value |
after_add_exit_credit | proved | — | — |
after_add_unit_credit | proved | — | — |
action_not_finished | proved | — | — |
action_noAdd | proved | — | noAdd_mask, noAdd_asyncFinalizer |
frame_step | proved | — | FrameSequencing. |
popFrom_noAdd | proved | — | noAdd_append, answerOf_clean, passPushed_noAdd, ensure_noAdd, noAdd_tail |
passPushed_no_push | proved | — | passEvents_no_push |
layer_compile_credits | proved | — | — |
layer_zero_credits | proved | — | layer_compile_credits |
loopNext_credits | proved | — | loopFinish_credits, resolve_credits |
stack_before_push | proved | — | — |
iterator_future | proved | — | — |
interp_iter | proved | — | closeSeq_credits, runStmts_credits |
interp_loopResume | proved | — | loopResume_credits |
after_add_code_credits | proved | — | fin_program_credits |
interp_contA | proved | — | contA_credits |
suspend_credits | proved | — | prog_of_credits, compile_credits, resolve_credits |
armE | proved | — | cancel, exit_credits, stack_credits_bounded, interp_contE |
noAdd_mask | proved | — | — |
FrameSequencing. | proved | — | constant_push_kept, noAdd_cons, noAdd_append, armA_noAdd, interrupt, resumeCause_kept, resumeValue_kept, opaque_noAdd |
noAdd_append | proved | — | — |
answerOf_clean | proved | — | — |
passPushed_noAdd | proved | — | answerOf_clean, ensure_noAdd, noAdd_tail |
ensure_noAdd | proved | — | — |
noAdd_tail | proved | — | — |
loopFinish_credits | proved | — | — |
closeSeq_credits | proved | — | fin_program_credits |
runStmts_credits | proved | — | yieldOf_credits |
loopResume_credits | proved | — | loopNext_credits |
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 |
cancel | proved | — | store_cancel |
interp_contE | proved | — | contE_credits |
constant_push_kept | proved | — | forced_unwrap, forced_push, noAdd_cons, opaque_noAdd |
armA_noAdd | proved | — | — |
resumeCause_kept | proved | — | noAdd_append, armE_noAdd, getCont_cause_kept |
resumeValue_kept | proved | — | interrupt, resumeValue_kept_clear |
yieldOf_credits | proved | — | compile_credits |
bind_service_credits | proved | — | — |
service_lookup_credits | proved | — | — |
merge_context_credits | proved | — | — |
combine_credits | proved | — | — |
provide_then_credits | proved | — | — |
layer_construction_credits | proved | — | — |
registration_template | proved | — | — |
layer_inner_credits | proved | — | layer_compile_credits, layer_resolve_credits |
add_memo_credits | proved | — | — |
build_scope_credits | proved | — | — |
update_body_credits | proved | — | — |
provide_body_credits | proved | — | exit_credits |
provide_layer_credits | proved | — | — |
store_contA_credits | proved | — | prog_of_credits, store_exit_credits |
store_cancel | proved | — | — |
contE_credits | proved | — | store_contE_credits, exit_credits, resolve_credits |
forced_unwrap | proved | — | — |
forced_push | proved | — | — |
armE_noAdd | proved | — | noAdd_empty |
resumeValue_kept_clear | proved | — | resumeValue_clean |
store_exit_credits | proved | — | — |
store_contE_credits | proved | — | store_exit_credits |
resumeValue_clean | proved | — | noAdd_append, armA_noAdd, getCont_noAdd |
getCont_noAdd | proved | — | noAdd_empty, popFrom_noAdd |