R2: Extension is conservative: C1–C8 over DI-47's relation on Σ_appreq:R2
- Open, not triaged: C2 for host rows outside the fragment StraightRows: operational; on the fragment it is meaningUnder_append (decisions row 313)
- Open, not triaged: C4 for TypedProg (the generic judgment is proved both ways)
- Open, not triaged: C5: the world projection with its back condition (its red controls are proved)
- Open, not triaged: C7: conditional on decisions row 115
- Open, not triaged: C8: per form
Requirement R2: Conservative extensionabout:req:R2
This page explains requirement R2 in Effect4. It covers what conservative extension requires across eight obligations, why typing signature independence matters, and how the property is checked.
What the requirement asksabout:req:R2:what-it-asks
Requirement R2 requires that extending an application signature is conservative across eight named obligations (DB-01, docs/core/system-map. §8):
- C1 syntax: extending a signature leaves existing program representations unchanged.
- C2 meaning: extending operations leaves existing program denotations unchanged.
- C3 checker: extending a signature admits exactly the same existing programs.
- C4 protocol typing: existing programs keep their protocol certificates.
- C5 world: extending allocated operations projects onto earlier world states.
- C6 local lawfulness: appending rows keeps signature validity intact.
- C7 representation: target representations remain compatible.
- C8 forms: higher-level form expansions remain stable under extension.
Extending a signature must never alter the typing, semantics, or admission of existing programs.
Why it mattersabout:req:R2:why-it-matters
Software composition relies on stability under modular extension.
If adding a new library, operation row, or service changed how existing programs run, modular verification would collapse.
Conservative extension lets separate modules compose without changing what the earlier ones mean.
How it is checkedabout:req:R2:how-it-is-checked
The requirement is checked by proving conservative extension theorems for syntax, checking, meaning, and sums:
- Checker extension and restriction are stated by
check_extandcheck_restrictinsrc/Effect4/Laws/Program/Signature..lean - Signature lawfulness under appending is stated by
lawful_appendin the same file. - Denotational meaning under row extension is stated on
StraightRowsbymeaningUnder_append(src/Effect4/Laws/Program/DenoteRowsAppend.).lean - That a signature sum is a coproduct of free monads is stated by
sum_is_coproduct(src/Effect4/Laws/Effects/Sum.).lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- Translation & Simulation proved, 2 nodes → No concept
- Initial Algebras & Folds proved, 7 nodes → No concept
- No concept proved, 9 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
check_ext | proved | — | check_sound, check_complete |
check_restrict | proved | — | cata_eff_congr_on, hom_eq_cata_eff |
lawful_append | proved | — | — |
meaningUnder_append | proved | — | — |
denoteRowsB_looped | proved | — | denoteRows_straight |
denoteRowsB_straight | proved | — | — |
checkModule_conservative | proved | — | defs_conservative |
checkModule_eq_check | proved | — | — |
defs_conservative | proved | — | cata_eff_congr_on, hom_eq_cata_eff |
moduleHasTy_ext | proved | — | — |
typeOfProgram_ext | proved | — | checkModule_sound, moduleHasTy_ext, checkModule_complete |
check_sound | proved | — | — |
check_complete | proved | — | — |
cata_eff_congr_on | proved | — | — |
hom_eq_cata_eff | proved | — | — |
denoteRows_straight | proved | — | — |
checkModule_sound | proved | — | check_sound |
checkModule_complete | proved | — | checkModule_eq_check, check_complete |