Async Side Effects Need Provenance

Capturing a side effect during a function call is straightforward while the call remains on the stack.

After an await, timer, event, or promise continuation, attribution becomes harder. Another case may be running. A callback may escape and fire later. An uninstrumented API may schedule work the harness cannot associate safely.

Guessing can make the equivalence report worse than incomplete: it can blame an effect on the wrong function.

Ownership is the standard

An effect should be attributed only when the harness owns the continuation that produced it.

The tracing model can offer tiers:

• none: make no effect-attribution claim;
• synchronous frame: attribute effects before the call yields;
• continuation: carry case identity across supported asynchronous boundaries.

The deeper tier costs more because it creates and tracks continuation context. A low-risk check should not pay that cost automatically.

Abstain beyond the owned boundary

If an effect arrives without an owned continuation, through an uninstrumented API, or through a scheduling path the framework did not declare, the harness records no claim with a reason.

Examples include:

• no owned continuation;
• API path not instrumented;
• framework hook mismatch;
• selected tier does not track continuations.

An absent effect record is then distinguishable from an application that produced no effects.

Interleaved cases must not steal effects

Portable replay may execute several asynchronous cases near each other. A process-global “current recorder” lets one case capture another’s delayed effect.

Continuation-local state keeps the recorder and request plan attached to the case that scheduled the work. A callback escaping one case remains associated with its origin even if another case begins before it fires.

This is essential for deterministic comparison.

Framework hooks are contracts

Framework-specific scheduling can be modelled when a declared hook establishes the relationship. A mismatch should not be coerced merely because an originating identity is still available.

The trace should preserve the mismatch as a coverage limitation. Otherwise a framework update can silently change scheduling while the harness continues assigning effects under obsolete assumptions.

Counts make under-attribution visible

The run can report:

• effects attributed;
• total no-claim effects;
• no-claim counts by reason;
• browser-side unattributed effects;
• the provenance tier selected.

These metrics keep a sparse trace from looking deceptively clean.

Why refactors expose this problem

Performance and architecture changes often alter asynchronous structure:

• a synchronous call becomes deferred;
• callbacks move across modules;
• promise chains are flattened;
• batching changes effect order;
• one shared subscription replaces several listeners.

Return values may remain identical while externally observable timing changes.

Static analysis can identify schedules and known host channels. Runtime provenance shows which observed effects were actually tied to the changed continuation.

KodeProof’s standard is conservative: a misattributed effect is a false fact that can block the wrong patch or approve the wrong one. When continuation ownership is absent, “we cannot claim this effect” is the more trustworthy verdict.