R10: Library code inherits theorems: a composed module's law is Agrees profile module expansionreq:R10
- Open, worded as a proposed claim: pool-expansion-agrees (proposed claim; translation-simulation): Pool's expansion agrees with the first profile's public observation, under its premises on the callers, interruption, the close and the work budget; its parts on one atomic step are pool_steps_agree and the eleven attempt statements of the operations, each on every model state (lease_attempt, withdraw_attempt, return_attempt, select_attempt, close_attempt, drain_attempt, make_makes, and four at the names that the operation mints; the lease, the withdrawal and the closer's step take an injective table); the operations, the wake, the close and the refusal at a closed pool are library programs (src/Effect4/Library/Pool/Ops.lean); the wrapper's run for the borrower and for the closer, the wake across helpers and the protected lease's run are not stated; finite controls: ten cases on the Lean machine, on the generated engine and on rc.112, one schedule each (Test/Program/PoolPublic.lean) (decisions rows 79, 226, 267 to 269, 276, 279)
- Open, not triaged: a composed module's law, Agrees profile module expansion (decisions row 79, R79.5; DI-89)
- Open, not triaged: no form has a behaviour law (DI-89)
- Open, not triaged: the agreement half of mask-printed-form-profile (translation-simulation, serving R10 and R11): the compiled derived form against the named release's printed form, equal observation on a named observation under compatible decisions; the three operations more than the native mask are measured on the machine and on the target, not proved, and the cuts at the two checkpoints on the pin rest on Codex's runs; the expansion, the typing, the readability and the two checkpoints on the machine are mask_printed_form_profile (decisions rows 245, 246); no goal states the agreement
- Open, not triaged: none of DI-89's named forms exists: retry, catchTag, forEach, all, Schedule over iterate, the option and result eliminators
- Open, waits on a ruling (the model probe's D9, not ruled (DI-89)): per form: reader admission, a readable expansion (C8) and a stable identity (DI-89; the model probe's D9, unruled)
- Open, not triaged: DI-39's six rows not landed
- Open, not triaged: a composite's contract by a stuttering route (post-Phase C §11.4)
- Open, worded as a proposed claim: queue-expansion-agrees (proposed claim; translation-simulation): the Queue's expansion agrees with its application-signature clients on the Queue's profile, which defines the public requests, commits, replies, interruptions and terminations before it hides a private cell or a helper identity (decisions rows 79, 219 to 222, 230); its first application on one program is two planned goals, held_within_fed and fed_accounted (Test/Dogfood/Scenario/QueueWorkers.lean), with finite controls on the Lean machine, three engine runs and 25 host runs; no law of a whole run
- Open, worded as a proposed claim: semaphore-expansion-agrees (proposed claim; translation-simulation): Semaphore's expansion agrees with the first profile's public observation; it keeps the selected identities and the permit commits, with its premises on the wake's policy, the admitted callers, interruption and the work budget; its parts on one atomic step are semaphore-steps-agree and the nine attempt statements of the operations, each on every model state; the operations, the walk and the protected form are library programs (src/Effect4/Library/Semaphore/Ops.lean); the wrapper's run, the walk across visits and the protected form's run are not stated (decisions rows 79, 226, 259 to 261, 276)
- Open, worded as a proposed claim: partitioned-semaphore-expansion-agrees (proposed claim; translation-simulation): latest's finite natural-count profile observes registration, partial reservation, ordered partition selection, cancellation settlement, inline client execution and the final reply under admitted client tapes; partitioned-semaphore-bookkeeping proves only four scalar source readings, including explicit premises for reservation; the waiter model, contextual identity correspondence, delivery and protected acquisition connection remain unstated; no whole-run or progress claim (decisions rows 330, 331, 333 and 335)
- Open, worded as a proposed claim: stream-array-run-agrees (proposed claim; translation-simulation): the array source's public pulls return its initial finite sequence once and then End, under the admitted caller and observation profile; stream-array-step-agreement proves the allocated cell's batch transition; whole pulls, repeated opens, finalization and the signed Done/End correspondence remain open (decisions rows 331 and 335)
- Open, worded as a proposed claim: synchronized-ref-expansion-agrees (proposed claim; translation-simulation): pure callback modification observes Ref's reply and stored value under Semaphore's protected permit protocol; make_answers, get_answers and modify_answers prove typing under their stated premises; protected acquisition, cancellation, cleanup and composed run agreement remain open; effectful callbacks stay outside this slice (decisions rows 330, 331 and 335)
- Open, worded as a proposed claim: pubsub-single-expansion-agrees (proposed claim; translation-simulation): the capacity-one, replay-zero profile observes natural messages and live logical subscriptions; pubsub-single-steps-agree proves six source readings under fresh subscription and scope premises; contextual source-object correspondence, exact numeric host admission, waiting, delivery, cancellation, lifetime and backpressure execution remain open (decisions rows 330, 331 and 335)
- Open, worded as a proposed claim: posted-wake-profile-agrees (proposed claim; translation-simulation): one producer's posted delivery, with its dispatch owner, priority, receiver and token, capture time, coalescing and cancellation, agrees with its module expansion; the Queue's producer is first (decisions rows 81, 220, 225; DB-13)
- Open, worded as a proposed claim: atomic-attempt-agreement (proposed claim; translation-simulation): the restricted transaction profile against the named release, with flat nesting, immutable payloads and explicit retry; then tx-choice-rollback-union for the retry-only alternative (decisions rows 80, 84, 223, 224)
- Open, not triaged: fair composition of tickets that are enrolled apart is outside the first profile: the opposing-ticket cycle stays a refused case until an enrolment protocol resolves it (decisions row 223)
Requirement R10: Composed libraries inherit theoremsabout:req:R10
This page explains requirement R10 in Effect4. It covers what the requirement asks for library forms, why behavioral inheritance matters for composite modules, and how the property is checked.
What the requirement asksabout:req:R10:what-it-asks
Requirement R10 demands that high-level library modules inherit formal theorems from their underlying primitive representations (docs/core/system-map. §8, decisions row 79, DI-89):
- Agreement laws: each composed module satisfies
Agrees profile module expansionon a named profile. - Form obligations: every authoring form owes a typing lemma, a behavior law, lexical scoping, module reader admission, and a stable identity.
- Expansion stability: composite modules like Queue, Pool and Semaphore state step agreement against their primitive expansions.
High-level library utilities must not introduce unvetted runtime primitives.
Why it mattersabout:req:R10:why-it-matters
Effect provides extensive library modules for concurrent data structures, synchronization primitives, and resource pools.
If composite modules were treated as black boxes with hand-written runtime implementations, their correctness could not be formally assured.
Behavioural agreement is what lets library code take the core language's typing and simulation theorems, where each is proved.
How it is checkedabout:req:R10:how-it-is-checked
The requirement is checked by proving form typing lemmas and step agreement laws for library structures:
- Form typing lemmas for combinators like
andThenEffect,ensuring, andforkScopedDefaultare stated insrc/Effect4/Laws/Codegen/Forms..lean - Step agreement laws relating composite modules to primitive expansions are stated for
Latch,Pool,PubSub,Queue,Ref, andSemaphorein their respective profile modules. - Stream array step agreement is stated by
arrayStep_agrees(src/Effect4/Laws/Library/Stream/Array.).lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- queueWorkers modulo → releases_once, queue_settled, fed_accounted, held_within_fed
- held_within_fed modulo → jobs_step
- routing modulo → unauthorized_calls_nothing
- retries_declared goal
- releases_once modulo → cleanup_step
- queue_settled modulo → rest_step, jobs_step
- fed_accounted modulo → rest_step, jobs_step
- jobs_step goal
- unauthorized_calls_nothing modulo → bound_in_tree
- cleanup_step modulo → logs_history
- rest_step goal
- bound_in_tree modulo → request_leads
- logs_history goal
- request_leads goal
The figure in words
- No concept proved, 27 nodes
- Translation & Simulation open, 167 nodes, 7 open → Scope Lifetime & Finalization, Exact Codecs, No concept, Store Typing, Subtyping Algebra, Host Session Protocol, Reactive Scheduling, Context Requirements, Residual Program Typing, Initial Algebras & Folds
- Residual Program Typing proved, 2 nodes
- Subtyping Algebra proved, 47 nodes → No concept
- Reactive Scheduling open, 15 nodes, 3 open → Translation & Simulation, No concept, Host Session Protocol, Scope Lifetime & Finalization
- Scope Lifetime & Finalization open, 184 nodes, 3 open → Initial Algebras & Folds, Translation & Simulation, No concept, Host Session Protocol, Reactive Scheduling
- Exact Codecs proved, 1 nodes → No concept
- Store Typing proved, 30 nodes → Reactive Scheduling, No concept, Subtyping Algebra
- Host Session Protocol proved, 5 nodes
- Context Requirements open, 2 nodes, 1 open → Translation & Simulation, No concept
- Initial Algebras & Folds proved, 8 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
andThenEffect_typed | proved | — | check_sound, check_complete |
andThenContinuation_typed | proved | — | check_sound, check_complete |
andThenThunk_typed | proved | — | andThenEffect_typed |
as_typed | proved | — | check_sound, check_complete |
asVoid_typed | proved | — | as_typed |
tapContinuation_typed | proved | — | normalize_idem, check_sound, check_complete |
tapEffect_typed | proved | — | normalize_idem, check_sound, check_complete |
ensuring_typed | proved | — | check_sound, check_complete |
void_typed | proved | — | check_complete, check_sound |
die_typed | proved | — | check_complete, check_sound |
yieldKey_typed | proved | — | check_complete, check_sound |
matchCause_typed | proved | — | check_sound, check_complete |
matchCauseEffect_typed | proved | — | check_sound, check_complete |
yieldNow_typed | proved | — | check_complete, check_sound |
forkChildDefault_typed | proved | — | check_sound, check_complete |
forkDetachDefault_typed | proved | — | check_sound, check_complete |
forkInDefault_typed | proved | — | check_sound, check_complete |
forkScopedDefault_typed | proved | — | check_sound, check_complete |
releaseOne_typed | proved | — | check_sound, check_complete |
mask_printed_form_profile | proved | — | saved_mask_restoration, read_print, check_sound, check_complete |
build_retains | proved | — | finishBuild_retains, checkInput_eq_none_iff |
elaborateModule_no_declarations | proved | — | — |
elaboration_eq_getD | proved | — | — |
finishBuild_retains | proved | — | checkInput_eq_none_iff |
mapDoneEffectOf_protocol | proved | — | matchAnswer_meaning |
mapEffectOf_protocol | proved | — | matchAnswer_meaning |
awaitStep_agrees | proved | — | sound |
Latch. | proved | — | sound |
flushStep_agrees | proved | — | sound |
initialStep_agrees | proved | — | sound |
isOpenStep_agrees | proved | — | sound |
latch_registration_agrees | proved | — | Latch., awaitStep_agrees, initialStep_agrees |
latch_steps_agree | proved | — | Latch., flushStep_agrees, wakeStep_agrees, isOpenStep_agrees |
wakeStep_agrees | proved | — | sound |
Latch. | proved | — | sound |
frame | proved | — | — |
sound | proved | — | reads_ascribe |
cell_read | proved | — | — |
reads_ascribe | proved | — | — |
step_updates | proved | — | — |
available_eval | proved | — | — |
available_reads | proved | — | available_eval, sound |
bookkeeping_agrees | proved | — | reserve_reads, tryTake_reads, available_reads, PartitionedSemaphore. |
PartitionedSemaphore. | proved | — | — |
PartitionedSemaphore. | proved | — | PartitionedSemaphore., sound |
reserve_eval | proved | — | — |
reserve_reads | proved | — | reserve_eval, sound |
tryTake_eval | proved | — | — |
tryTake_reads | proved | — | tryTake_eval, sound |
Pool. | proved | — | sound |
drainStep_agrees | proved | — | sound |
leaseStep_agrees | proved | — | sound |
pool_steps_agree | proved | — | drainStep_agrees, Pool., Pool., selectStep_agrees, returnStep_agrees, leaseStep_agrees |
returnStep_agrees | proved | — | sound |
selectStep_agrees | proved | — | sound |
Pool. | proved | — | sound |
close_attempt | proved | — | step_keeps_cell, closeStep_types, step_updates, Pool. |
drain_attempt | proved | — | step_keeps_cell, drainStep_types, step_updates, drainStep_agrees |
drain_attempt_minted | proved | — | drain_attempt |
lease_attempt | proved | — | step_keeps_cell, leaseStep_types, step_updates, leaseStep_agrees |
lease_attempt_minted | proved | — | lease_attempt |
Pool. | proved | — | — |
return_attempt | proved | — | step_keeps_cell, returnStep_types, step_updates, returnStep_agrees |
return_attempt_minted | proved | — | lift_member, normalize_idem, return_attempt |
select_attempt | proved | — | step_keeps_cell, selectStep_types, step_updates, selectStep_agrees |
withdraw_attempt | proved | — | step_keeps_cell, Pool., step_updates, Pool. |
withdraw_attempt_minted | proved | — | withdraw_attempt |
tagHit_record | proved | — | — |
modify_loop | proved | — | loop_sync_op |
sub_instantiate_polarity | proved | — | — |
semiring_laws | proved | — | — |
PubSub. | proved | — | — |
PubSub. | proved | — | PubSub., sound |
poll_eval | proved | — | — |
poll_reads | proved | — | poll_eval, sound |
single_steps_agree | proved | — | slide_reads, unsubscribe_reads, poll_reads, tryPublish_reads, subscribe_reads, PubSub. |
slide_eval | proved | — | — |
slide_reads | proved | — | slide_eval, sound |
subscribe_eval | proved | — | — |
subscribe_reads | proved | — | subscribe_eval, sound |
tryPublish_eval | proved | — | — |
tryPublish_reads | proved | — | tryPublish_eval, sound |
unsubscribe_eval | proved | — | — |
unsubscribe_reads | proved | — | unsubscribe_eval, sound |
catchDone_meaning | proved | — | — |
matchAnswer_meaning | proved | — | — |
matchEffect_meaning | proved | — | — |
matchEffect_protocol | proved | — | matchEffect_meaning, matchAnswer_meaning |
offer_loop | proved | — | offer_jobs, modify_loop, offer_attempt |
take_loop | proved | — | take_jobs, modify_loop, Queue. |
acceptLoop_length_le | proved | — | — |
first_profile_closed | proved | — | — |
flatMap_split | proved | — | — |
offerStep_agrees | proved | — | sound |
offer_jobs | proved | — | — |
pollStep_agrees | proved | — | sound |
poll_jobs | proved | — | stateJobs_afterAccept |
positive_suspend_step_capacity | proved | — | acceptLoop_length_le |
queue_steps_agree | proved | — | withdrawOffer_agrees, withdrawTake_agrees, sizeStep_agrees, pollStep_agrees, offerStep_agrees, Queue. |
sizeStep_agrees | proved | — | sound |
stateJobs_afterAccept | proved | — | — |
Queue. | proved | — | sound |
take_jobs | proved | — | stateJobs_afterAccept |
withdrawOffer_agrees | proved | — | sound |
withdrawOffer_jobs | proved | — | flatMap_split |
withdrawTake_agrees | proved | — | sound |
withdrawTake_jobs | proved | — | — |
bounded_makes | proved | — | — |
offer_attempt | proved | — | step_keeps_cell, offerStep_types, step_updates, offerStep_agrees |
offer_attempt_minted | proved | — | offer_attempt |
offer_withdrawal | proved | — | step_keeps_cell, withdrawOffer_types, step_updates, withdrawOffer_agrees |
offer_withdrawal_minted | proved | — | offer_withdrawal |
poll_attempt | proved | — | step_keeps_cell, pollStep_types, step_updates, pollStep_agrees |
size_read | proved | — | sizeStep_agrees, cell_read |
Queue. | proved | — | step_keeps_cell, Queue., step_updates, Queue. |
Queue. | proved | — | Queue. |
Queue. | proved | — | step_keeps_cell, withdrawTake_types, step_updates, withdrawTake_agrees |
Queue. | proved | — | Queue. |
decode_modifySome | proved | — | — |
decode_option | proved | — | — |
encode_getD | proved | — | — |
getAndSet_agrees | proved | — | kernel_agrees |
getAndUpdateSome_agrees | proved | — | decode_option, kernel_agrees |
getAndUpdate_agrees | proved | — | kernel_agrees |
get_agrees | proved | — | kernel_agrees |
kernel_agrees | proved | — | — |
make_agrees | proved | — | — |
modifySome_agrees | proved | — | encode_getD, decode_modifySome, kernel_agrees |
modify_agrees | proved | — | kernel_agrees |
modify_callback_agrees | proved | — | modify_agrees, sound |
ref_steps_agree | proved | — | modifySome_agrees, modify_agrees, updateSomeAndGet_agrees, getAndUpdateSome_agrees, updateSome_agrees, updateAndGet_agrees, getAndUpdate_agrees, update_agrees, setAndGet_agrees, getAndSet_agrees, set_agrees, get_agrees, make_agrees |
setAndGet_agrees | proved | — | kernel_agrees |
set_agrees | proved | — | kernel_agrees |
updateAndGet_agrees | proved | — | kernel_agrees |
updateSomeAndGet_agrees | proved | — | encode_getD, decode_option, kernel_agrees |
updateSome_agrees | proved | — | decode_option, kernel_agrees |
update_agrees | proved | — | kernel_agrees |
releaseStep_agrees | proved | — | sound |
semaphore_steps_agree | proved | — | Semaphore., visitStep_agrees, releaseStep_agrees, takeIfAvailableStep_agrees, Semaphore. |
takeIfAvailableStep_agrees | proved | — | sound |
Semaphore. | proved | — | sound |
visitStep_agrees | proved | — | sound |
Semaphore. | proved | — | sound |
Semaphore. | proved | — | — |
release_attempt | proved | — | step_keeps_cell, releaseStep_types, step_updates, releaseStep_agrees |
takeIfAvailable_attempt | proved | — | step_keeps_cell, takeIfAvailableStep_types, step_updates, takeIfAvailableStep_agrees |
Semaphore. | proved | — | step_keeps_cell, Semaphore., step_updates, Semaphore. |
Semaphore. | proved | — | Semaphore. |
Semaphore. | proved | — | step_keeps_cell, Semaphore., step_updates, Semaphore. |
Semaphore. | proved | — | Semaphore. |
visit_attempt | proved | — | step_keeps_cell, visitStep_types, step_updates, visitStep_agrees |
visit_attempt_minted | proved | — | visit_attempt |
arrayStep_agrees | proved | — | modify_callback_agrees |
queue_built_program | proved | — | queue_elaborates, build_retains, checkInput_eq_none_iff |
queue_elaborates | proved | — | queue_refs_nil, queue_main_eq, elaborateModule_no_declarations |
queue_main_eq | proved | — | queue_main_some, elaboration_eq_getD |
queue_main_some | proved | — | — |
queue_refs_nil | proved | — | — |
workers_built_program | proved | — | workers_elaborates, build_retains, checkInput_eq_none_iff |
workers_elaborates | proved | — | workers_refs_nil, workers_main_eq, elaborateModule_no_declarations |
workers_main_eq | proved | — | workers_main_some, elaboration_eq_getD |
workers_main_some | proved | — | — |
workers_refs_nil | proved | — | — |
accounted_of_ledger | proved | — | held_of_shows |
exit_eq | proved | — | — |
fed_perm | proved | — | — |
filterMap_gave | proved | — | — |
flatMap_offers | proved | — | — |
heldWithin_of_ledger | proved | — | fed_perm, held_of_shows |
held_of_shows | proved | — | flatMap_offers, filterMap_gave |
ledger_opened | proved | — | opened_exit |
opened_exit | proved | — | exit_eq |
jobs_step | goal | jobs_step | checkInput_eq_none_iff |
held_within_fed | modulo | jobs_step | heldWithin_of_ledger, exit_eq, jobs_step, checkInput_eq_none_iff, reached_history, ledger_opened, queueCrew_acquire_once_placed, queue_acquisition_sites, queue_built_program |
queueWorkers | modulo | jobs_step, logs_history, rest_step | releases_once, queue_settled, fed_accounted, held_within_fed, control_retires, applied_selects, receipt_inert, checkInput_eq_none_iff |
infrastructure_escapes | proved | — | checkInput_eq_none_iff |
routing | modulo | request_leads | unauthorized_calls_nothing, infrastructure_escapes, tagIs_pair, checkInput_eq_none_iff |
tagIs_pair | proved | — | — |
retries_declared | goal | retries_declared | checkInput_eq_none_iff |
check_sound | proved | — | — |
check_complete | proved | — | — |
normalize_idem | proved | — | — |
saved_mask_restoration | proved | — | at_append |
read_print | proved | — | readTerm_printTerm |
checkInput_eq_none_iff | proved | — | — |
step_keeps_cell | proved | — | fold_typed_atomic_update |
closeStep_types | proved | — | typed |
drainStep_types | proved | — | typed |
leaseStep_types | proved | — | typed |
returnStep_types | proved | — | typed |
lift_member | proved | — | — |
selectStep_types | proved | — | typed |
Pool. | proved | — | typed |
loop_sync_op | proved | — | native_sync_op, iteration_below_budget, loop_of_iteration |
offerStep_types | proved | — | offer_nodes_for_steps, message_nodes_for_steps, ascribe_formed_for_steps, typed |
withdrawOffer_types | proved | — | typed |
pollStep_types | proved | — | offer_nodes_for_steps, message_nodes_for_steps, ascribe_formed_for_steps, typed |
Queue. | proved | — | offer_nodes_for_steps, message_nodes_for_steps, ascribe_formed_for_steps, typed |
withdrawTake_types | proved | — | typed |
releaseStep_types | proved | — | typed |
takeIfAvailableStep_types | proved | — | typed |
Semaphore. | proved | — | typed |
Semaphore. | proved | — | typed |
visitStep_types | proved | — | typed |
reached_history | proved | — | — |
queueCrew_acquire_once_placed | proved | — | queue_placement, queue_built_program, checkInput_eq_none_iff |
queue_acquisition_sites | proved | — | — |
releases_once | modulo | logs_history | cleanup_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 |
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 |
control_retires | proved | — | — |
applied_selects | proved | — | — |
receipt_inert | proved | — | — |
unauthorized_calls_nothing | modulo | request_leads | tree_needs_token, bound_in_tree, checkInput_eq_none_iff |
at_append | proved | — | — |
readTerm_printTerm | proved | — | — |
fold_typed_atomic_update | proved | — | readTerm_printTerm, order_refl, termMaps_of_typed, listOf_upper, fits_subN, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty |
typed | proved | — | candsList_nil, cands_var, candsList_cons, types_ascribe, normalize_idem, subN_refl, matchArgsB_list_var_nat, matchArgsB_append, matchArgsB_cons_nil, lift_member, matchArgsB_one_var, matchArgsB_two_vars, join_eq_right_of_subN, matchArgsB_ite |
native_sync_op | proved | — | — |
iteration_below_budget | proved | — | — |
loop_of_iteration | proved | — | — |
offer_nodes_for_steps | proved | — | message_nodes_for_steps |
message_nodes_for_steps | proved | — | — |
ascribe_formed_for_steps | proved | — | — |
queue_placement | proved | — | — |
cleanup_step | modulo | logs_history | releases, registrations, logs_history, reached_history, checkInput_eq_none_iff |
settled_of_ledger | proved | — | within_one, spent_one, quiet_nil, settled_of_view |
rest_step | goal | rest_step | checkInput_eq_none_iff |
tree_needs_token | proved | — | — |
bound_in_tree | modulo | request_leads | denoteRowsB_straight, localWaitC_to_rowsB, request_leads, driveState_lift, evaluatePrim_producer, reached |
order_refl | 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 |
listOf_upper | proved | — | list_eliminator, normalize_idem, subN_trans, subN_refl, extendAll_upper |
fits_subN | proved | — | subN_trans, fits_normalize |
fits_normalize | proved | — | subN_trans, normalize_idem |
lift_sound | proved | — | lift_transfer |
subN_trans | proved | — | — |
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 | — | — |
hom_eq_cata_ty | proved | — | — |
candsList_nil | proved | — | — |
cands_var | proved | — | — |
candsList_cons | proved | — | — |
types_ascribe | proved | — | lift_member, normalize_idem |
subN_refl | proved | — | — |
matchArgsB_list_var_nat | proved | — | candsList_nil, cands_var, candsList_cons |
matchArgsB_append | proved | — | candsList_nil, cands_var, candsList_cons |
matchArgsB_cons_nil | proved | — | candsList_nil, cands_var, candsList_cons |
matchArgsB_one_var | proved | — | cands_var, candsList_nil, candsList_cons |
matchArgsB_two_vars | proved | — | candsList_nil, cands_var, candsList_cons |
join_eq_right_of_subN | proved | — | normalize_idem, subN_refl, subN_join_least |
matchArgsB_ite | proved | — | normalize_idem, candsList_nil, cands_var, candsList_cons |
releases | proved | — | queue_built_program, checkInput_eq_none_iff, history, read |
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 |
logs_history | goal | logs_history | checkInput_eq_none_iff |
within_one | proved | — | — |
spent_one | proved | — | — |
quiet_nil | proved | — | — |
settled_of_view | proved | — | — |
denoteRowsB_straight | proved | — | — |
localWaitC_to_rowsB | proved | — | localRunC_compileBO |
request_leads | goal | request_leads | — |
driveState_lift | proved | — | — |
evaluatePrim_producer | proved | — | — |
reached | proved | — | — |
fits_mono | 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 | — | — |
subN_join_least | proved | — | normalize_idem |
history | proved | — | decision, at_append, mem_addresses_iff, RuntimeShape., Execution. |
read | proved | — | — |
replace_sum | proved | — | — |
mem_addresses_iff | proved | — | yieldAt_addressYield, mem_foldList_iff, addresses_eq_foldList |
closeOrder_eq | proved | — | — |
replace_sum_le_omitted | proved | — | replace_sum |
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 |
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 |
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 |
yieldAt_addressYield | proved | — | — |
mem_foldList_iff | proved | — | exists_at_of_mem_foldList |
addresses_eq_foldList | proved | — | — |
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 |
denoteRows_straight | proved | — | — |
adjoint | proved | — | Eliminator., subN_trans, mapM_total, Eliminator. |
foldl_keeps | proved | — | — |
mapM_cons_eq_some | 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 |
exists_at_of_mem_foldList | proved | — | sizeOf_child_lt, foldList_cases |
Eliminator. | proved | — | UnionRule. |
mapM_total | proved | — | mapM_cons_eq_some |
Eliminator. | proved | — | subN_refl, UnionRule. |
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 |
sizeOf_child_lt | proved | — | — |
foldList_cases | proved | — | — |
UnionRule. | proved | — | subN_trans, mapM_source, joinAll_le |
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 |
mapM_source | proved | — | mapM_cons_eq_some |
joinAll_le | proved | — | joinAll_all |
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 | — | — |
joinAll_all | proved | — | foldl_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 |
foldl_all | proved | — | — |
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 | — | — |
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 |