R5: Services: the service table, layers and provisionreq:R5
- Open, not triaged: lower_refines_build: the machine's build of a layer refines `build` (decisions row 147)
- Open, not triaged: reference keys, Config, minted keys, and context validation at any runtime bridge (system map §8, R5)
Requirement R5: Services and layer provisionabout:req:R5
This page explains requirement R5 in Effect4. It covers what the requirement asks for service tables and layers, why static requirement grading matters, and how the property is checked.
What the requirement asksabout:req:R5:what-it-asks
Requirement R5 demands that services are managed through static service tables in the application typing signature and discharged by layers (docs/core/system-map. §8):
- Service tables: service keys and types form an explicit static component of Σ_app.
- Value typing: constructed layer values must fit their declared service keys.
- Flat coeffect grading: requirement rows grade programs by the service keys they need for execution.
- Capability discharge: providing a layer discharges its output requirement keys.
A program with an unfilled service requirement must not execute at the top level.
Why it mattersabout:req:R5:why-it-matters
Enterprise applications structure dependencies using modular layers that construct database clients, loggers, and authentication handlers.
If requirement rows were untracked, a program could fail at runtime with missing service defects deep inside execution.
Grading a program by its requirement row lets the checker refuse a missing service before the run begins.
How it is checkedabout:req:R5:how-it-is-checked
The requirement is checked by proving layer construction, requirement discharge, and context algebra theorems:
- Totality of layer building under satisfying contexts is stated by
build_total(src/Effect4/Laws/Program/BuildTotal.).lean - Capability discharge under layer provision is stated by
provide_discharges(src/Effect4/Program/Provision.).lean - Closure of layer composition is stated by
provide_closedin the same file. - Commutativity of row merging is stated by
merge_rows_commin the same file.
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- unauthorized_calls_nothing modulo → bound_in_tree
- bound_in_tree modulo → request_leads
- request_leads goal
The figure in words
- Context Requirements open, 2 nodes, 1 open → Translation & Simulation, No concept
- Translation & Simulation open, 14 nodes, 2 open → Reactive Scheduling, Host Session Protocol, No concept, Initial Algebras & Folds
- No concept proved, 6 nodes
- Initial Algebras & Folds proved, 3 nodes
- Reactive Scheduling proved, 2 nodes
- Host Session Protocol proved, 1 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
build_total | proved | — | satisfies_union, satisfies_weaken, satisfies_empty |
expanded_refs_nil_of_wf | proved | — | — |
typeOfProgram_expandRefs | proved | — | expanded_refs_nil_of_wf |
tree_needs_token | proved | — | — |
unauthorized_calls_nothing | modulo | request_leads | tree_needs_token, bound_in_tree, checkInput_eq_none_iff |
satisfies_union | proved | — | — |
satisfies_weaken | proved | — | — |
satisfies_empty | proved | — | — |
bound_in_tree | modulo | request_leads | denoteRowsB_straight, localWaitC_to_rowsB, request_leads, driveState_lift, evaluatePrim_producer, reached |
checkInput_eq_none_iff | proved | — | — |
denoteRowsB_straight | proved | — | — |
localWaitC_to_rowsB | proved | — | localRunC_compileBO |
request_leads | goal | request_leads | — |
driveState_lift | proved | — | — |
evaluatePrim_producer | proved | — | — |
reached | proved | — | — |
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 |
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 | — | — |
at_append | proved | — | — |