R8: Runs and faces as named connections: equal to the reference inside a profile, refused outside itreq:R8
- Open, waits on a ruling (decisions row 28: what verified lowering means): typed lowering open: what verified lowering means (decisions row 28); the OCaml engine is outside M7 until it is ruled
- Open, waits on a ruling (decisions row 108: the owner places the numbers slice): numbers open (decisions row 108): each face equal to the reference inside its bounded profile and refusing outside it, intermediates included (DI-56)
- Open, not triaged: K2 holds on the readable domain; since the state plan's T5, part B, a loop's stated cursor type and an operation's type arguments read back through one checked type reader (Classes.readTyChecked, DI-91's fallback (a) in a checked form), and the domain excludes a stated type outside the readable types (Classes.ReadableTy: a collision such as int, a spelling with no reading such as a handle type) and every list fold that states its accumulator's type, which is printed and not read
- Open, after other work (the fiber identity carrier of DI-81, ruled and not landed): one identity bijection across faces: the fiber identity carrier is ruled, not landed (DI-81)
- Open, not triaged: the TypeScript face against rc.112: finite checks only, by the truth harness and by the keyed lane's runs of the scenarios' scripts on their printed modules (DI-49; decisions row 254); the truth harness compares each entry's exit with the same entry's, the fork run's and the sync run's apart; two Semaphore programs settle on two exits under their two entries, and the two faces give one exit on each; three Pool programs settle on two exits too, and their sync runs are pinned apart from the allocation order on the Lean face (lateSightsSync, harness/truth/Truth.lean) (Test/contracts/faces.contract.md, the amendments of 2026-10-06; decisions row 279)
- Open, not triaged: the profile as data, named by each face's law (decisions row 79, R79.5)
Requirement R8: Runs and faces as named connectionsabout:req:R8
This page explains requirement R8 in Effect4. It covers what the requirement asks for execution faces and profiles, why named connections matter, and how the property is checked.
What the requirement asksabout:req:R8:what-it-asks
Requirement R8 demands that every face and backend operates as a named connection bounded by explicit profile data (docs/core/system-map. §8, decisions row 79):
- Profile bounds: inside its declared profile, a face's observation equals the reference observation up to an identity bijection.
- Located refusal: outside its profile, the face refuses execution, including intermediate values that exceed supported bounds.
- Profile as data: target capabilities and numerical ranges are defined as first-order profile data rather than ad-hoc heuristics.
- Invertible target syntax: printing and reading target code form partial isomorphisms on readable domains.
A face must never silently compute unvetted answers outside its certified profile.
Why it mattersabout:req:R8:why-it-matters
Effect4 presents multiple faces: application interfaces, printed TypeScript modules, and native OCaml engines lowered through LCNF.
Different target runtimes enforce different scalar limits, memory layouts, and feature subsets.
An explicit profile makes each face state the boundary it supports, so a difference between platforms is a refusal and not a silent divergence.
How it is checkedabout:req:R8:how-it-is-checked
The requirement is checked by proving face simulations and print-read isomorphisms over declared profiles:
- Invertible syntax round-tripping is stated by
read_printandread_exactinsrc/Effect4/Laws/Codegen/ReadPrint..lean - Meaning agreement on the
Straightfragment is stated byrun_eq_meaning(src/Effect4/Laws/Program/Agreement/Segment.).lean - Loop step agreement on the
Loopedfragment is stated byloopAgreement_of_straight(src/Effect4/Laws/Program/LoopAgreement.).lean - Reference simulation at the empty row table is stated by
run_eq_ref(src/Effect4/Laws/Program/RuntimeR.).lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- Exact Codecs proved, 12 nodes → No concept, Initial Algebras & Folds
- Translation & Simulation proved, 8 nodes → Initial Algebras & Folds, No concept
- No concept proved, 7 nodes → Translation & Simulation
- Initial Algebras & Folds proved, 43 nodes → No concept
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
read_print | proved | — | readTerm_printTerm |
read_exact | proved | — | — |
run_eq_meaning | proved | — | at_append |
loopAgreement | proved | — | at_append |
run_eq_ref | proved | — | at_append |
mask_rows_table_premises | proved | — | read_exact, read_print |
printTyped_eq_print | proved | — | printTypedAt_none |
printTypedAt_none | proved | — | hom_eq_cata_eff |
eraseJoinArgs_printTyped | proved | — | eraseJoinArgs_printTypedSitesAt, eraseJoinArgs_printTypedAt |
eraseJoinArgs_printTypedAt | proved | — | readTerm_printTerm |
eraseJoinArgs_printTypedSitesAt | proved | — | envAt_append, annotate_eq_table, at_child, readTerm_printTerm, envAt_child |
readTyped_exact | proved | — | read_exact |
readTyped_printTyped | proved | — | eraseJoinArgs_printTyped, read_print |
readTyped_printTypedAt | proved | — | eraseJoinArgs_printTypedAt, read_print |
readModule_printModule_defs | proved | — | replaceAt_spec |
funded_replays | proved | — | journal_replays, tape_replays |
tape_replays | proved | — | — |
unsuspended_runs | proved | — | run_agrees |
shown_views_opened | proved | — | tapeFrom_position_replays |
readTerm_printTerm | proved | — | — |
at_append | proved | — | — |
hom_eq_cata_eff | proved | — | — |
envAt_append | proved | — | — |
annotate_eq_table | proved | — | check_eq, table_eq_tableAt |
at_child | proved | — | at_append |
envAt_child | proved | — | envAt_append |
replaceAt_spec | proved | — | — |
journal_replays | proved | — | — |
run_agrees | proved | — | run_eq_meaning |
tapeFrom_position_replays | proved | — | tape_replays |
check_eq | proved | — | tableAt_eq_cons, tableAt_none, checkStmt_step_binds, effTy_of_check, termTy_of_term? |
table_eq_tableAt | proved | — | — |
tableAt_eq_cons | proved | — | tableEntryAt_nil, childAddresses_map_tableEntryAt, addresses_eq_cons |
tableAt_none | proved | — | — |
checkStmt_step_binds | proved | — | — |
effTy_of_check | proved | — | check_sound, check_complete |
termTy_of_term? | proved | — | — |
tableEntryAt_nil | proved | — | — |
childAddresses_map_tableEntryAt | proved | — | — |
addresses_eq_cons | proved | — | foldMapAt_stmt_paths_cons, foldMapAt_layers_paths_cons, foldMapAt_effs_paths_cons, foldMapAt_layer_paths_cons, foldMapAt_action_paths_cons, foldMapAt_stmts_paths_cons, foldMapAt_eff_paths_cons |
check_sound | proved | — | — |
check_complete | proved | — | — |
foldMapAt_stmt_paths_cons | proved | — | foldMapAt_stmt_paths_shift |
foldMapAt_layers_paths_cons | proved | — | foldMapAt_layers_paths_shift |
foldMapAt_effs_paths_cons | proved | — | foldMapAt_effs_paths_shift |
foldMapAt_layer_paths_cons | proved | — | foldMapAt_layer_paths_shift |
foldMapAt_action_paths_cons | proved | — | foldMapAt_action_paths_shift |
foldMapAt_stmts_paths_cons | proved | — | foldMapAt_stmts_paths_shift |
foldMapAt_eff_paths_cons | proved | — | foldMapAt_eff_paths_shift |
foldMapAt_stmt_paths_shift | proved | — | foldMapAt_stmt_hom, foldMapAt_stmt_base |
foldMapAt_layers_paths_shift | proved | — | foldMapAt_layers_hom, foldMapAt_layers_base |
foldMapAt_effs_paths_shift | proved | — | foldMapAt_effs_hom, foldMapAt_effs_base |
foldMapAt_layer_paths_shift | proved | — | foldMapAt_layer_hom, foldMapAt_layer_base |
foldMapAt_action_paths_shift | proved | — | foldMapAt_action_hom, foldMapAt_action_base |
foldMapAt_stmts_paths_shift | proved | — | foldMapAt_stmts_hom, foldMapAt_stmts_base |
foldMapAt_eff_paths_shift | proved | — | foldMapAt_eff_hom, foldMapAt_eff_base |
foldMapAt_stmt_hom | proved | — | — |
foldMapAt_stmt_base | proved | — | — |
foldMapAt_layers_hom | proved | — | — |
foldMapAt_layers_base | proved | — | — |
foldMapAt_effs_hom | proved | — | — |
foldMapAt_effs_base | proved | — | — |
foldMapAt_layer_hom | proved | — | — |
foldMapAt_layer_base | proved | — | — |
foldMapAt_action_hom | proved | — | — |
foldMapAt_action_base | proved | — | — |
foldMapAt_stmts_hom | proved | — | — |
foldMapAt_stmts_base | proved | — | — |
foldMapAt_eff_hom | proved | — | — |
foldMapAt_eff_base | proved | — | — |