Repository navigation
feat(effects): infer conservative operation effects with resource identities and foreign-call contracts #197
Description
Audited on master at 5630d74ec9cd912d4e2f325349f1943cbc15bcc6. This is a scoped implementation item under #147, based on the typed control/dataflow/effect audit. Proposed syntax below is illustrative unless explicitly marked as a current reproducer.
Gap and evidence
nlsc/schema.py:99–147 has value-use/dependency metadata but no effect contract. Arbitrary supported Python expressions and literal overrides can read/write external or shared state. The documented lists/records remain mutable/reference-bearing; immutable bindings do not make their referents pure.
A current source with items.append(1) -> first and items.append(2) -> second yields no inter-step data dependencies and groups [[1, 2]], even though both mutate the same list. This motivates effect analysis; current emitters still execute source order.
Minimum deliverable
Introduce effect summaries such as:
Pure, Read(resource), Write(resource), IO(capability), and conservative Unknown, with explicit treatment of clock/random/resource lifetime observations. These are semantic contracts, not guessed properties of English verbs.
Implementation hints
- Attach an effect set and provenance to checked operations/calls. Known core primitives may have verified summaries; compose user ANLU summaries over the resolved call graph.
- Missing metadata for a native import, dynamically dispatched call, or
@literalmeans Unknown, never Pure. An explicitly trusted external signature is an assumption that tools should expose. - Preserve resource identity through aliases and caller-to-callee parameter substitution. Distinct variable names do not prove distinct objects/accounts.
- Start conservatively: concrete identities where provable, symbolic regions where justified, wildcard overlap otherwise. Defer rich predicates such as
inventory.write(order.items)until their meaning is defined. - Validate explicit declarations as upper bounds on inferred effects, including effects inside guards, branches, loops, and called operations. Keep failure summaries separate and composable.
- Handle supported recursion with monotone/fixed-point summaries; retain current restrictions on unsupported recursive forms.
- Do not claim an effect declaration sandboxes or verifies arbitrary foreign implementations. Coordinate that trust boundary with Security model: sandboxing, import trust, and safe execution docs #150.
Acceptance criteria
- Pure arithmetic, shared-list mutation, nested calls, guards, and unknown external calls produce expected conservative summaries.
- A declared Pure function calling a writer or unknown foreign operation is rejected in checked mode.
- Aliases and resource argument substitution preserve conflicts through call boundaries.
- Unknown effects remain explicit in serialized IR/diagnostics and block unsafe optimization.
- Summaries are deterministic, included in effective build identity, and documented with their trusted assumptions.
Scope: declarations/inference and checking. Scheduling and runtime concurrency are separate work.
Implementation ordering
Integration depends on #194, #195. Add the behavior/diagnostic fixtures before implementation.
Osprey-informed implementation refinements
Build on the summary slots in the IR delivered by #194 / #203. The key refinement is to keep two different effect facts, alongside the failure set in #198:
| Fact | Meaning | Effect of installing a handler |
|---|---|---|
| Required operations | Which typed requests still need an implementation | Subtract only the exact supplied operation arms, with matching type instances when supported |
| Observable footprint | Reads/writes, I/O, clock/random observations, resource lifetime, and unknown effects of executing the computation | Include the selected handler implementation's effects and preserve alias/resource provenance |
An empty set of unhandled operations does not imply purity, commutativity, replayability, or absence of failure. Handling a payment request through a gateway still affects the account. A disk-backed Storage handler and an in-memory handler can discharge the same operation while having different footprints.
Implementation refinements:
- Add stable operation identities and keep
required_operations,resource_effects, andunknown/provenancedistinct in the semantic summary and serialization; names are illustrative. - Infer both dimensions through supported calls and callback invocation. Merely constructing/passing a callback is not invoking it; calling a returned closure or callable record field contributes its latent effects.
- Key builtin callback/iterator contracts by resolved symbol identity from feat(semantics): resolve operation signatures and type-check calls, bindings, and returns #195, never by identifier spelling. Preserve callback provenance through aliases and supported wrappers.
- Use deterministic monotone fixed-point analysis for supported recursion. If an analysis bound is reached or dynamic provenance cannot be resolved, widen conservatively; never silently drop a requirement or resource effect.
- Handler selection in feat(effects): add typed lexical handlers and injectable operation implementations #207 substitutes the implementation summary in its lexical context. Unknown host implementation/resource identity remains unknown; a trusted signature is a visible assumption, not verified sandboxing.
- Validate declarations as upper bounds for the dimension they describe. Declaring a required operation does not install a handler or authorize an effect.
Additional acceptance cases:
- Handling
Storage.saveleavesStorage.loadunresolved when no matching outer arm exists. - The disk and memory handlers discharge the same requirements but retain different footprints; the disk variant cannot be classified Pure.
- An effectful callback survives supported forwarding/return paths and recursion; an escaping closure does not inherit a completed handler region's discharge.
- A shadowed builtin and unresolved callable provenance cannot falsely erase effects.
- Summary serialization/build identity preserves both dimensions and the assumptions used.
References: Osprey's operation-level fixed-point implementation, negative and positive checker fixtures, and effect contract. Its operation rows are a reference for requirements analysis; NLS's resource/alias conflict analysis remains additional work.
#207 implements handler syntax/runtime integration; this issue owns the summary representation and inference foundations and does not wait for that runtime.
Activity
Mnehmos commentedon Sep 12, 2026
Slice plan (planning pass, 2026-09-13)
Current state:
nlsc/effects.pyinfers onlyunknownmarkers (populate_effect_sets, deterministic callee fixpoint) plus analyzed-empty for purely structural code.IREffectSpecalready reserves the fields this issue needs (kind: read | write | unknown,resource) but nothing populates them; effects participate in thesem2semantic hash and are printed bynlsc ir.Next slice (one PR): read/write resource identities for structural code + declared upper bounds.
nlsc/effects.py: populatekind="read"/"write"withresource= param/binding name for structural nodes (refs read; method calls whose base resolves to a param/binding conservatively write it); foreign content staysunknown. Add call-site substitution so a callee'swrite(p)becomeswrite(arg)at the caller.nlsc/ir.py: no shape change (the fields exist); addIROperation.declared_effects: Optional[tuple[IREffectSpec, ...]]and extendoperation_unchecked_nodes/assert_checked_moduleto refuse checked status when inferred effects exceed a declaration.EFFECTS:ANLU contract line (EFFECTS: pure,EFFECTS: write(items) read(log),EFFECTS: unknown), lowered ontodeclared_effects.EFX001(declaration exceeded — unknown-inside-pure included) andEFX002(malformed declaration), wired intoevaluate_semantic_gatewith the fatal/strict tier decided per the ESEM009 foreign-call precedent.operation_semantic_canonicalfor most operations, so this slice must bumpSEMANTIC_HASH_SCHEMEsem2→sem3and regenerate the committed example lockfiles; existing locks invalidate conservatively (documented migration, same as the sem2 change).tests/test_issue_197_resource_identities.py— write identity for repeated appends to one list; refs read; argument substitution across an ANLU call;EFFECTS: pure+ foreign call → EFX001; malformed → EFX002; hash sensitivity; determinism.Remaining after that slice (kept open): required-operations vs observable-footprint split and callback latent effects from the issue's Osprey refinements.
Merge pull request #247 from Mnehmos/feat/197-effect-resource-identities
Mnehmos commentedon Sep 13, 2026
Slice landed (PR #247). Against this issue's core asks:
write(<resource>)(withorigin=call) instead of a blanketunknown; call-site substitution maps callee effects through the caller's argument names (positional and keyword), so[mutate](rows)gives the callerwrite(rows) origin=callee. Callee-internal resources propagate asunknownconservatively. Guard-condition calls now propagate too (effects and failures).@literalbodies, method calls on unnamed bases — keeps explicitunknownmarkers; nothing is silently treated as pure.EFFECTS:acceptspure,unknown,read,write,read(name),write(name). Exceeding the declared bound isEFX001; malformed/blank declarations areEFX002, fatal in every mode. Declarations render canonically and participate in thesem3semantic hash.SEMANTIC_HASH_SCHEMEmovedsem2→sem3; example locks regenerated and verified reproducible.Still open in this issue for a later slice: the Osprey-refinement distinction between required operations (what a caller must provide/handle) and the observable footprint (what the summary reports), plus callback latent effects. Keeping the issue open for that.
Merge pull request #259 from Mnehmos/fix/localization-literal-safety