R1: The signature is a parameter: one located refusal admits Σ_app, and every milestone statement takes itreq:R1
- Open, not triaged: program admission at declared services is reached by tests only: authoring, Built, the session and Run.open admit at the table's own signature ⟨table, []⟩, and code generation's admission check is at nativeSignature table (decisions row 21; the slice plan's steps 3 and 4, docs/research/2026-10-04-claude-lead/sigapp-slice-plan.md)
- Open, not triaged: the faces (22 lines) pinned to the built-in signature: Laws/Codegen/Admit, Laws/Codegen/Checked and Laws/Api/ModuleReadable take nativeSignature table (the Σ_app slice; C7, conditional on decisions row 115)
- Open, not triaged: meaning, loop and run soundness at service declarations that rebind a code: restored 2026-10-04 at fresh codes only (SoundAnySignature.lean)
- Open, waits on a ruling (decisions row 118: waits on a program that needs one): structured service carriers: LawfulSig admits flat carriers only (decisions row 118, open: waits on a program that needs one)
Requirement R1: The typing signature is a parameterabout:req:R1
This page explains requirement R1 in Effect4. It covers what the requirement asks about signature parameterization, why open signatures matter for extensible applications, and how the property is checked.
What the requirement asksabout:req:R1:what-it-asks
Requirement R1 demands that the language typing signature Σ remains an explicit parameter across all milestone statements and verification layers (docs/core/system-map. §8).
The specification requires:
- Program admission checks the application signature via
AdmittedSig ΣandadmitSig_ok_iff. - The typed machine state reads the source's signature dynamically.
- Core typing theorems and milestone statements take the signature as an explicit hypothesis.
The runtime must not hard-code operations to a closed built-in set.
Why it mattersabout:req:R1:why-it-matters
Real-world Effect applications define custom operations, host integrations, and application services.
If semantic theorems assumed a fixed operation signature, application-defined effects would lack formal verification.
A signature that is a parameter lets an application add operations, and every milestone statement then takes the application's signature.
How it is checkedabout:req:R1:how-it-is-checked
The requirement is checked by proving that typing and evaluation hold for an admitted signature:
- Algorithmic soundness and completeness against
HasTy(check_sound,check_complete) quantify over any lawful typing signature insrc/Effect4/Laws/Program/Typing/CheckSound..lean - Signature admission equivalence is stated by
admitSig_ok_iff(src/Effect4/Program/SigApp.).lean - Operational typing across application signatures is stated by
meaning_typed_appandrun_typed_app(src/Effect4/Laws/Program/SoundAnySignature.).lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- reachable_typed_admitted modulo → reachable_typed
- reachable_typed modulo → decision_preserves
- decision_preserves modulo → deliver_preserves, loop_preserves
- deliver_preserves modulo → countdown_parks_positional
- loop_preserves modulo → countdown_parks_positional
- countdown_parks_positional goal
The figure in words
- No concept open, 32 nodes, 5 open → Translation & Simulation, Store Typing, Residual Program Typing, Subtyping Algebra, Exact Codecs, Reactive Scheduling, Initial Algebras & Folds, Scope Lifetime & Finalization
- Initial Algebras & Folds proved, 6 nodes → No concept
- Translation & Simulation proved, 1 nodes → Initial Algebras & Folds
- Store Typing proved, 12 nodes → Subtyping Algebra, No concept
- Residual Program Typing proved, 17 nodes → Store Typing, Subtyping Algebra, No concept, Exact Codecs, Initial Algebras & Folds
- Subtyping Algebra proved, 44 nodes → No concept
- Exact Codecs proved, 1 nodes
- Reactive Scheduling open, 2 nodes, 1 open
- Scope Lifetime & Finalization proved, 4 nodes → Store Typing, Subtyping Algebra, Residual Program Typing, Initial Algebras & Folds, No concept
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
check_sound | proved | — | — |
check_complete | proved | — | — |
admitSig_ok_iff | proved | — | — |
meaning_typed_app | proved | — | check_restrict, meaning_typed |
run_typed_app | proved | — | check_restrict, meaning_typed, run_eq_meaning |
meaningB_typed_app | proved | — | check_restrict, order_refl, fits_mono, hom_eq_cata_ty, deferredMake_extension, refMake_extension, syncRow_typed, listOf_upper, fits_subN, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, check_sound, check_complete, subN_refl, optionTy_upper, errOf_payload, isPayload_of_hasTy_record, order_trans |
reachable_typed_admitted | modulo | countdown_parks_positional | reachable_typed, lawfulSig_of_admitted |
checkModule_complete | proved | — | checkModule_eq_check, check_complete |
checkModule_sound | proved | — | check_sound |
invoke_hasTy | proved | — | — |
check_restrict | proved | — | cata_eff_congr_on, hom_eq_cata_eff |
meaning_typed | proved | — | order_refl, fits_mono, hom_eq_cata_ty, deferredMake_extension, refMake_extension, syncRow_typed, listOf_upper, fits_subN, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, check_sound, check_complete, subN_refl, optionTy_upper, errOf_payload, isPayload_of_hasTy_record, order_trans |
run_eq_meaning | proved | — | at_append |
order_refl | proved | — | — |
fits_mono | proved | — | — |
hom_eq_cata_ty | proved | — | — |
deferredMake_extension | proved | — | — |
refMake_extension | 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 |
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 |
matchArgsB_sound | proved | — | — |
subN_refl | proved | — | — |
optionTy_upper | proved | — | option_eliminator, normalize_idem, subN_trans, subN_refl, Eliminator. |
errOf_payload | proved | — | — |
isPayload_of_hasTy_record | proved | — | handles_of_payloadFieldTy |
order_trans | proved | — | — |
reachable_typed | modulo | countdown_parks_positional | decision_preserves, load_typed, order_trans, order_refl |
lawfulSig_of_admitted | proved | — | admitSig_ok_iff |
checkModule_eq_check | proved | — | — |
cata_eff_congr_on | proved | — | — |
hom_eq_cata_eff | proved | — | — |
at_append | 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 |
matchB_sound | proved | — | lookup_solve_seed |
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 | — | — |
option_eliminator | proved | — | subN_option_iff, normalize_idem, subN_trans, subN_refl |
Eliminator. | proved | — | subN_refl, UnionRule. |
handles_of_payloadFieldTy | 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 |
lookup_solve_seed | proved | — | — |
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_option_iff | proved | — | — |
satisfies_empty | proved | — | — |
mono | proved | — | order_trans |
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 |
driveState_lift | 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 |
adjoint | proved | — | Eliminator., subN_trans, mapM_total, Eliminator. |
foldl_keeps | proved | — | — |
mapM_cons_eq_some | proved | — | — |
completionStrong_await | proved | — | subN_trans |
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 | — | — |
scopeParams_child | proved | — | — |
at_child | proved | — | at_append |
scopeParams_below | proved | — | — |
fiberTy_upper | proved | — | fiber_eliminator, normalize_idem, subN_trans, subN_refl, extendAll_upper |
withParams_of_none | proved | — | — |
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 |
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 |
Eliminator. | proved | — | UnionRule. |
mapM_total | proved | — | mapM_cons_eq_some |
closeOrder_eq | proved | — | — |
fiber_eliminator | proved | — | subN_fiberOf_iff, normalize_idem, subN_trans, subN_refl |
scopeParams_body | proved | — | — |
withParams_defOf | proved | — | — |
exit_eliminator | proved | — | subN_exitOf_iff, normalize_idem, subN_trans, subN_refl |
scopeParams_decl | proved | — | — |
withParams_param | proved | — | — |
UnionRule. | proved | — | subN_trans, mapM_source, joinAll_le |
subN_fiberOf_iff | proved | — | — |
mapM_source | proved | — | mapM_cons_eq_some |
joinAll_le | proved | — | joinAll_all |
joinAll_all | proved | — | foldl_all |
foldl_all | proved | — | — |