R4: State: the world types every cell at any type, with rows as templatesreq:R4
- Open, worded as a proposed claim: pool-profile-preserved (proposed claim; store-typing): along a run of the public operations the cell stays a member of its type and its state stays in the first profile; the model's half is profile_closed on six transitions; the cell's half is the seven typing statements of the cell and of the steps with step_keeps_cell, and each attempt statement of the operations gives the membership of the reply and of the stored value from the membership of the cell before the step; the operations are typed at every scope (use_types, make_types, close_answers), and make's type requires the scope; no statement says that a client writes the cell by the operations alone, none keeps the table injective along a run, and no goal states the run-level claim (decisions rows 267 to 269, 276)
- Open, not triaged: the faces of Ref<A> and Deferred<A, E>, the type arguments' part: landed in the state plan's T5 for a binder term and for Deferred.make: a read-modify-write row's binder term is printed as a function of the cell's current value and read back (part A: printPerform, readPerform); Deferred.make<A, E>() is printed from the operation's own type arguments and read back at every instance whose types are readable (part B: Signature.typeArgsOf and withTypeArgs, printCall, readCall, LawfulTypeArgs; Classes.readTyChecked on Classes.ReadableTy), a bare Deferred.make() is refused by its spelling and never typed at a default, the native row declares no type argument of its own, and an operation's type arguments are program annotations (ScopedOp.typeArgs: raw formation, the integer scan and the module's class table read them; decisions row 212); read_print and read_exact keep their statements; open: Ref.make<A>, which needs an appended constructor (decisions rows 210 and 212); a type argument outside the readable types (a handle type, unknown, a class name: printed where it has a printed form, and refused at reading; int and number: read at nat); a list fold's stated accumulator type, which is printed and not read; and the instance's row in the other estates: the TypeScript profile and the OCaml metadata list Deferred.make once, at the face's instance, so a consumer that needs an instance's answer column derives it from the operation
- Open, not triaged: the target half of handle-identity-laws (decisions row 229): the identity correspondence in each target's relation, in both directions: two handles have equal keys exactly when their host objects are one object; no goal states it, and the laws over Fits and the world's order are handle_identity_laws
- Open, worded as a proposed claim: semaphore-accounting-preserved (proposed claim; store-typing): along a run of the public operations the cell stays a member of its type and its state stays in the first profile; the model's half is profile_closed; the cell's half is the six typing statements of the steps with step_keeps_cell, and each attempt statement of the operations gives the membership of the reply and of the stored value from the membership of the cell before the step; no statement gives that first membership from the handles that the table names, and no goal states the run-level claim (decisions rows 260, 261, 265, 276)
- Open, worded as a proposed claim: atomic-attempt-isolation (proposed claim; store-typing and reactive-scheduling): an admitted atomic body's ordered dynamic reads and writes, the exact state that a failure or a retry restores, and no step of another fiber between its first access and its commit (decisions rows 80, 223; waits on the body profile's grammar and on row 226's budget or suspension)
- Open, not triaged: the second half of scoped-body-substitution-boundary (residual-program-typing): for a later constructor that does bind a scope, the code after the scope runs only after it, and substitution neither captures it nor copies it into a child body (decisions rows 225, 227); no goal states it: the mask adds no scoped constructor, and its restore node's half is scoped_body_substitution_boundary
Requirement R4: Stateful memory and row templatesabout:req:R4
This page explains requirement R4 in Effect4. It covers what the requirement asks for mutable cells and row templates, why stateful typing matters, and how the property is checked.
What the requirement asksabout:req:R4:what-it-asks
Requirement R4 demands that the typed world supports mutable cells at arbitrary types and models operation rows as templates (docs/core/system-map. §8):
- World typing:
Worldexplicitly tracks types for cells (w.), deferred promises (Ρ w.), fibers (Π w.), and tokens (Γ w.).Θ - Row templates: operation rows act as templates whose type parameters instantiate via match by bounds.
- Binder terms: function rows take first-order binder terms that map cell types under environment extensions.
Allocating a fresh cell or promise must extend the world monotonically without invalidating earlier allocations.
Why it mattersabout:req:R4:why-it-matters
Concurrent programs coordinate across fibers using shared mutable state, asynchronous promises, and synchronized queues.
If stateful references supported only primitive numbers or hard-coded payload types, applications could not manage complex state.
Matching row templates by bounds lets a generic operation take its type arguments from the program, before the run.
How it is checkedabout:req:R4:how-it-is-checked
The requirement is checked by proving world extension, template matching, and step typing theorems:
- World order reflexivity and transitivity are stated in
src/Effect4/Laws/Program/Typed/World..lean - Allocation monotonicity is stated by
refMake_extensionanddeferredMake_extensionin the same file. - Totality of template matching by bounds is stated by
Bounds.(matchB_complete src/Effect4/Laws/Program/Bounds.).lean - Atomic update typing is stated by
fold_typed_atomic_update(src/Effect4/Laws/Program/Typed/ListFold.).lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- atomic modulo → cleans_once, committed, counted
- committed modulo → shop_stages
- counted modulo → shop_stages
- shop_stages goal
- cleans_once modulo → log_debits
- log_debits goal
The figure in words
- Store Typing open, 99 nodes, 4 open → No concept, Subtyping Algebra, Translation & Simulation, Reactive Scheduling, Initial Algebras & Folds, Scope Lifetime & Finalization, Host Session Protocol
- Residual Program Typing proved, 15 nodes → No concept, Initial Algebras & Folds, Store Typing, Subtyping Algebra, Exact Codecs
- Translation & Simulation proved, 6 nodes → Scope Lifetime & Finalization, Exact Codecs, No concept, Initial Algebras & Folds
- Reactive Scheduling proved, 7 nodes
- Initial Algebras & Folds proved, 11 nodes
- Subtyping Algebra proved, 108 nodes → No concept
- No concept proved, 13 nodes → Initial Algebras & Folds, Subtyping Algebra, Store Typing, Residual Program Typing, Exact Codecs, Translation & Simulation
- Exact Codecs proved, 2 nodes → No concept
- Scope Lifetime & Finalization open, 10 nodes, 2 open → Host Session Protocol, Translation & Simulation, No concept, Initial Algebras & Folds, Reactive Scheduling
- Host Session Protocol proved, 2 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
order_refl | proved | — | — |
order_trans | proved | — | — |
refMake_extension | proved | — | — |
deferredMake_extension | proved | — | — |
memoBuild_extension | 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 |
handle_identity_laws | proved | — | fits_mono |
saved_mask_image_membership | proved | — | — |
scoped_body_substitution_boundary | proved | — | denotesTyped, scopeParams_child, at_child, fits_subN, listOf_upper, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty, at_append |
awaitStep_types | proved | — | typed |
Latch. | proved | — | typed |
flushStep_types | proved | — | typed |
initialStep_types | proved | — | typed |
isOpenStep_types | proved | — | typed |
wakeStep_types | proved | — | typed |
Latch. | proved | — | typed |
image_agrees | proved | — | — |
afterExit_first | proved | — | raceCompleteFirst_accepts |
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 |
ascribe_untyped | proved | — | — |
step_keeps_cell | proved | — | fold_typed_atomic_update |
types_ascribe | proved | — | lift_member, normalize_idem |
available_types | proved | — | typed |
PartitionedSemaphore. | proved | — | typed |
reserve_types | proved | — | typed |
tryTake_types | proved | — | typed |
Pool. | proved | — | typed |
drainStep_types | proved | — | typed |
Model. | proved | — | matchArgsB_cons_nil, matchArgsB_append |
leaseStep_types | proved | — | typed |
lease_enrols_iff | proved | — | — |
Pool. | proved | — | — |
returnStep_types | proved | — | typed |
selectStep_types | proved | — | typed |
Pool. | proved | — | typed |
close_answers | proved | — | Pool., check_complete, check_sound, drainStep_types, matchB_modify_use, matchB_refOf_var, waitRetryAt_answers, mask_printed_form_profile, subN_refl, lift_member, normalize_idem, matchArgsB_two_vars, matchArgsB_list_var_nat, optionTy_option, selectStep_types, Pool. |
Pool. | proved | — | normalize_idem, check_complete, check_sound, close_answers, Model., matchB_one_var |
use_types | proved | — | check_complete, check_sound, subN_refl, lift_member, normalize_idem, matchArgsB_two_vars, matchArgsB_list_var_nat, optionTy_option, selectStep_types, matchB_modify_use, matchB_refOf_var, returnStep_types, Pool., leaseStep_types, waitRetryAt_answers, protectedBy_has |
ascribe_scoped | proved | — | — |
args | proved | — | noApp_args |
head | proved | — | — |
above_args | proved | — | mem_zip_map_right, instance_shape |
above_prod | proved | — | — |
admits_normalize | proved | — | normalize_idem |
below_args | proved | — | — |
candsFields_eq | proved | — | — |
candsItems_eq | proved | — | — |
candsList_below | proved | — | cands_below |
candsList_cons | proved | — | — |
candsList_nil | proved | — | — |
cands_args | proved | — | candsItems_eq, candsFields_eq, comp_inv, comp_co |
cands_below | proved | — | args, comp_ne_contra, cands_args, below_args, cands_union_right, cands_mem_members, head, cands_var |
cands_mem_members | proved | — | cands_union_right |
cands_union_right | proved | — | — |
cands_var | proved | — | — |
comp_co | proved | — | — |
comp_inv | proved | — | — |
comp_ne_contra | proved | — | comp_inv, comp_co |
covers | proved | — | above_args, above_prod, prod_or_not, recovers, cands_args, args, below_args, cands_union_right, head, cands_var |
instance_shape | proved | — | — |
instantiate_solve | proved | — | lookup_added |
joinCands_least | proved | — | subN_join_least, subN_never |
joinCands_upper | proved | — | normalize_idem, subN_trans, subN_refl |
join_eq_left_of_subN | proved | — | join_eq_right_of_subN |
join_eq_right_of_subN | proved | — | normalize_idem, subN_refl, subN_join_least |
lookup_added | proved | — | lowers_cons |
lookup_solve_seed | proved | — | — |
lowers_cons | proved | — | — |
matchArgsB_append | proved | — | candsList_nil, cands_var, candsList_cons |
matchArgsB_complete | proved | — | covers, candsList_below, solve_between |
matchArgsB_cons_nil | proved | — | candsList_nil, cands_var, candsList_cons |
matchArgsB_ite | proved | — | normalize_idem, candsList_nil, cands_var, candsList_cons |
matchArgsB_least | proved | — | candsList_below, solve_between |
matchArgsB_list_var_nat | proved | — | candsList_nil, cands_var, candsList_cons |
matchArgsB_one_var | proved | — | cands_var, candsList_nil, candsList_cons |
matchArgsB_sound | proved | — | — |
matchArgsB_two_vars | proved | — | candsList_nil, cands_var, candsList_cons |
matchArgsN_complete | proved | — | admits_normalize, matchArgsB_complete |
matchArgsN_least | proved | — | admits_normalize, matchArgsB_least |
matchB_cell_fixed | proved | — | matchB_sound |
matchB_complete | proved | — | covers, cands_below, solve_between |
matchB_least | proved | — | cands_below, solve_between |
matchB_modify_use | proved | — | cands_var |
matchB_one_var | proved | — | cands_var |
matchB_refOf_var | proved | — | cands_var, comp_inv |
matchB_sound | proved | — | lookup_solve_seed |
matchN_congr | proved | — | — |
mem_lowers | proved | — | — |
mem_varsOf_args | proved | — | — |
mem_zip_map_right | proved | — | — |
mem_zip_self_map | proved | — | — |
noAppFields_eq_all | proved | — | — |
noAppItems_eq_all | proved | — | — |
noApp_args | proved | — | noAppItems_eq_all, noAppFields_eq_all |
prod_left_cands | proved | — | head, args, cands_var, cands_mem_members, prod_member_left |
prod_member_left | proved | — | — |
prod_member_right | proved | — | — |
prod_or_not | proved | — | — |
prod_right_cands | proved | — | head, args, cands_var, cands_mem_members, prod_member_right |
recovers | proved | — | mem_zip_self_map, cands_args, instance_shape, mem_varsOf_args, prod_right_cands, prod_left_cands, args, prod_or_not, head, cands_var |
solve_between | proved | — | joinCands_upper, lookup_solve_seed, mem_lowers, joinCands_least, instantiate_solve |
subN_join_least | proved | — | normalize_idem |
subN_never | proved | — | — |
templateOK_of | proved | — | — |
loop_sync_op | proved | — | native_sync_op, iteration_below_budget, loop_of_iteration |
native_sync_answer | proved | — | native_sync_op |
native_sync_op | proved | — | — |
perform_scoped_iff | proved | — | — |
heap_sites_keep | proved | — | at_append, mem_addresses_iff, evaluatePrim_producer, closeOrder_eq, driveState_lift |
withParams_defOf | proved | — | — |
withParams_of_none | proved | — | — |
withParams_param | proved | — | — |
withParams_serviceTy | proved | — | — |
admitted_heap_history | proved | — | evaluatePrim_producer, closeOrder_eq, at_append, mem_addresses_iff, driveState_lift |
mono | proved | — | order_trans |
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 |
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 |
scopeParams_ref | proved | — | — |
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 |
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_below | proved | — | — |
scopeParams_body | proved | — | — |
scopeParams_child | proved | — | — |
scopeParams_decl | proved | — | — |
scopeParams_layer_below | proved | — | — |
PubSub. | proved | — | typed |
PubSub. | proved | — | typed |
slide_types | proved | — | typed |
subscribe_types | proved | — | typed |
tryPublish_types | proved | — | typed |
unsubscribe_types | proved | — | typed |
ascribe_formed_for_steps | proved | — | — |
empty_typed | proved | — | — |
message_nodes_for_steps | proved | — | — |
offerStep_typed | proved | — | offerStep_types |
offerStep_types | proved | — | offer_nodes_for_steps, message_nodes_for_steps, ascribe_formed_for_steps, typed |
offer_nodes_for_steps | proved | — | message_nodes_for_steps |
pollStep_typed | proved | — | pollStep_types |
pollStep_types | proved | — | offer_nodes_for_steps, message_nodes_for_steps, ascribe_formed_for_steps, typed |
sizeStep_typed | proved | — | typed |
takeStep_typed | proved | — | Queue. |
Queue. | proved | — | offer_nodes_for_steps, message_nodes_for_steps, ascribe_formed_for_steps, typed |
withdrawOffer_typed | proved | — | withdrawOffer_types |
withdrawOffer_types | proved | — | typed |
withdrawTake_typed | proved | — | withdrawTake_types |
withdrawTake_types | proved | — | typed |
bounded_types | proved | — | empty_typed, offer_nodes_for_steps, message_nodes_for_steps, matchB_one_var, check_complete, check_sound |
offer_types | proved | — | withdrawOffer_types, check_complete, check_sound, optionTy_option, lift_member, normalize_idem, subN_refl, matchArgsB_two_vars, matchArgsB_list_var_nat, offerStep_types, matchB_modify_use, matchB_refOf_var, rowTy_instantiated_formed, mask_printed_form_profile, offer_nodes_for_steps, message_nodes_for_steps |
Queue. | proved | — | check_complete, check_sound, lift_member, normalize_idem, subN_refl, matchArgsB_two_vars, matchArgsB_list_var_nat, optionTy_option, pollStep_types, offer_nodes_for_steps, message_nodes_for_steps, matchB_modify_use, matchB_refOf_var |
size_types | proved | — | lift_member, normalize_idem, check_complete, check_sound, offer_nodes_for_steps, message_nodes_for_steps, matchB_refOf_var |
Queue. | proved | — | withdrawTake_types, check_complete, check_sound, optionTy_option, lift_member, normalize_idem, subN_refl, matchArgsB_two_vars, matchArgsB_list_var_nat, Queue., offer_nodes_for_steps, message_nodes_for_steps, matchB_modify_use, matchB_refOf_var, waitRetryAt_answers, mask_printed_form_profile |
modify_callback_answers | proved | — | typed, check_complete, check_sound, matchB_modify_use, matchB_refOf_var |
empty_types | proved | — | — |
Semaphore. | proved | — | — |
releaseStep_types | proved | — | typed |
takeIfAvailableStep_types | proved | — | typed |
Semaphore. | proved | — | typed |
visitStep_types | proved | — | typed |
Semaphore. | proved | — | typed |
Semaphore. | proved | — | empty_types, matchB_one_var, check_complete, check_sound |
release_types | proved | — | check_complete, check_sound, normalize_idem, subN_refl, lift_member, matchArgsB_two_vars, optionTy_option, visitStep_types, matchB_modify_use, matchB_refOf_var, matchArgsB_one_var, releaseStep_types |
takeIfAvailable_types | proved | — | takeIfAvailableStep_types, check_complete, check_sound, matchB_modify_use, matchB_refOf_var |
Semaphore. | proved | — | Semaphore., check_complete, check_sound, Semaphore., matchB_modify_use, matchB_refOf_var, waitRetryAt_answers, mask_printed_form_profile |
withPermitsIfAvailable_types | proved | — | release_types, check_sound, check_complete, normalize_idem, matchArgsB_one_var, takeIfAvailable_types, protectedBy_has, sub_antisymm_canonical |
withPermits_types | proved | — | release_types, Semaphore., check_complete, check_sound, Semaphore., matchB_modify_use, matchB_refOf_var, waitRetryAt_answers, protectedBy_has |
fromDefinitions_declarations | proved | — | — |
arrayBatch_answers | proved | — | modify_callback_answers |
raceCompleteFirst_accepts | proved | — | — |
raceCompleteFirst_keeps | proved | — | — |
get_answers | proved | — | lift_member, normalize_idem, matchB_refOf_var, check_complete, check_sound |
make_answers | proved | — | check_complete, check_sound, Semaphore., matchB_one_var |
modify_answers | proved | — | lift_member, normalize_idem, modify_callback_answers, withPermits_types |
shop_stages | goal | shop_stages | checkInput_eq_none_iff |
atomic | modulo | log_debits, shop_stages | unsuspended_runs, cleans_once, committed, counted, bounded, checkInput_eq_none_iff |
bounded | proved | — | history, build_retains, checkInput_eq_none_iff, mem_addresses_iff, heap_sites_keep |
committed | modulo | shop_stages | history, build_retains, checkInput_eq_none_iff, shop_stages |
counted | modulo | shop_stages | history, build_retains, checkInput_eq_none_iff, shop_stages |
readTerm_printTerm | proved | — | — |
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 |
normalize_idem | proved | — | — |
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 |
hom_eq_cata_ty | proved | — | — |
fits_mono | 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 |
at_child | proved | — | at_append |
at_append | proved | — | — |
subN_refl | proved | — | — |
lift_member | proved | — | — |
check_complete | proved | — | — |
check_sound | proved | — | — |
waitRetryAt_answers | proved | — | check_complete, check_sound, optionTy_option, normalize_idem, matchArgsB_one_var |
mask_printed_form_profile | proved | — | saved_mask_restoration, read_print, check_sound, check_complete |
optionTy_option | proved | — | lift_member |
protectedBy_has | proved | — | normalize_idem, check_sound, check_complete, mask_printed_form_profile |
iteration_below_budget | proved | — | — |
loop_of_iteration | proved | — | — |
mem_addresses_iff | proved | — | yieldAt_addressYield, mem_foldList_iff, addresses_eq_foldList |
evaluatePrim_producer | proved | — | — |
closeOrder_eq | proved | — | — |
driveState_lift | proved | — | — |
errOf_payload | proved | — | — |
isPayload_of_hasTy_record | proved | — | handles_of_payloadFieldTy |
rowTy_instantiated_formed | proved | — | — |
sub_antisymm_canonical | proved | — | — |
checkInput_eq_none_iff | proved | — | — |
unsuspended_runs | proved | — | run_agrees |
cleans_once | modulo | log_debits | history, 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 |
history | proved | — | reached_history |
build_retains | proved | — | finishBuild_retains, checkInput_eq_none_iff |
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 | — | — |
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 |
satisfies_weaken | proved | — | — |
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 |
fits_scope_inv | proved | — | — |
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 |
saved_mask_restoration | proved | — | at_append |
read_print | proved | — | readTerm_printTerm |
yieldAt_addressYield | proved | — | — |
mem_foldList_iff | proved | — | exists_at_of_mem_foldList |
addresses_eq_foldList | proved | — | — |
handles_of_payloadFieldTy | proved | — | — |
run_agrees | proved | — | run_eq_meaning |
replace_sum | proved | — | — |
replace_sum_le_omitted | proved | — | replace_sum |
starts_le_pushes | proved | — | funded_reachable |
log_debits | goal | log_debits | checkInput_eq_none_iff |
reached_history | 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 |
fiber_eliminator | proved | — | subN_fiberOf_iff, normalize_idem, subN_trans, subN_refl |
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 |
exists_at_of_mem_foldList | proved | — | sizeOf_child_lt, foldList_cases |
run_eq_meaning | proved | — | at_append |
funded_reachable | proved | — | evaluatePrim_producer, getCont_le, step_debit, finalizerOr_debit, replace_sum, driveState_lift |
adjoint | proved | — | Eliminator., subN_trans, mapM_total, Eliminator. |
foldl_keeps | proved | — | — |
mapM_cons_eq_some | proved | — | — |
subN_fiberOf_iff | proved | — | — |
subN_option_iff | proved | — | — |
sizeOf_child_lt | proved | — | — |
foldList_cases | proved | — | — |
getCont_le | proved | — | — |
step_debit | proved | — | getCont_le |
finalizerOr_debit | proved | — | step_debit, getCont_le |
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 | — | — |