Link higher-order, class and platform boundaries in the Corsa check

[mizchi]

The default Corsa check resolved only free-function calls and exact Owner#member contracts, so a class-based, callback-heavy browser codebase reached almost nothing. Four mechanisms close that, each fail-closed by construction.

Higher-order composition

A function that invokes one of its own plain-identifier parameters carries InvokeUserCode, and every call of that boundary — a plain call, a construction, super, or in-class dispatch — owes an analyzed boundary at that argument position or becomes unknown. Obligations propagate to a fixed point, so a caller that forwards its own parameter inherits one rather than discharging it.

Inherited contracts

A reviewed contract is keyed by the interface that declares the member and is now reached through the inheritance lib.dom.d.ts itself declares: Node#ownerDocument applies to an HTMLElement receiver, while a receiver that reaches no interface carrying that member stays unknown — NodeList#length still never selects Storage#length. Three interfaces whose named members the standard leaves open (CSSStyleDeclarationBase, DOMStringMap, DOMTokenList) carry one whole-surface contract, consulted only after every member-specific key on the chain has missed.

Class construction and dispatch

new C(), super(...) and super.m(...) link to the class body they run. this.m() and a member call on a nominal class link to the declared body only when nothing in the analyzed files can replace it: a private or # member always qualifies; a public one additionally needs no subclass declaring that name, no assignment that could install a function on that receiver type, an unnarrowed file list, and every statically imported binding declared in a file the run read.

Reviewed contracts

The catalog gains the legacy request object, the document tree, the window surface, the style, dataset and class-list surfaces, the URI functions, and the standard constructors and conversions. mutate is read as the ownership fact it is rather than an unmodelled primitive, clone and transfer render as their capabilities, and a contract's callback may be the function assigned to a handler property.

Review

Five independent adversarial reviews ran against this change — three spec reviews of the catalog and two attempts to break the linking mechanisms by execution. They reproduced 10 unsound proofs and over 40 contract defects; every one is fixed and pinned by a regression test. The ones worth naming:

• PromiseLike#then had been given Promise.prototype.then's semantics, though it is a structural interface any value with a then method satisfies, so the call is synchronous, arbitrarily repeating user code.
• DOMRect redeclares DOMRectReadOnly's geometry members as writable, so the inheritance walk landed on the read-only entry and proved that assigning them was harmless.
• A TypeScript this parameter shifted every argument index, silently dropping the obligation it named.
• new C(cb), this.m(cb) and super.m(cb) never discharged the callee's obligation at all.
• An anonymous class extends Base, extends Alias, a mixin call, a decorator, C.prototype.m = f and this.m() written inside an object literal each defeated override detection.

Over-claims were corrected in the same pass, which is why some effect counts go down: new Error("literal") no longer carries InvokeUserCode (the declared message is a string, so its coercion is total), and the Event constructor and new Promise no longer carry a TypeError that typed code cannot reach.

Measured

On a 224-file browser ad delivery codebase, analyzed with no changes to it, counting production sources only:

	before	after
unknown	1,094	892
trusted	17	175
inferred	299	350

Net becomes observable for the first time. This repository's own check runs in 29 s against 33 s before, while reporting 75 syntax errors where the earlier build reported 1,024.

One limit is worth recording because it is a property of the analyzed codebase rather than of the checker: 576 member-call sites there are blocked by a single deep-merge helper whose target parameter is any and whose assignment is computed. That write could install a function on any object, so no public method of any class can be proved un-replaced.

Verification

• fast tier 95 files / 1,718 tests, Corsa and catalog suites 25 files / 324 tests, all passing
• tsc --noEmit across all four project configurations
• ci/check-examples.mjs and ci/check-skills.mjs pass
• The detection oracle still fires: the unrepaired handler reports its unguarded parts[1], the repaired one does not
• The integration tier's 53 failures are byte-identical to clean main — a 2 GB WASM limit in the Z3 backend, unrelated to this change

🤖 Generated with Claude Code

[mizchi]

Pre-merge review found 16 unsound proofs; the leaky half is cut

Five adversarial reviewers re-attacked this branch by execution before merge. They reproduced 16 unsound proofs — cases where a summary claimed inferred/trusted with an effect set the function actually exceeds at runtime. Fourteen of them were in one mechanism, and the pattern was not a bug list but a design verdict, so that mechanism is now cut rather than patched.

What was cut

Linking a public this.m(), and a member call on a receiver the caller supplies, both needed the analyzed file set to be closed. That precondition was implemented by walking ImportDeclaration specifiers, and reviewers defeated it five different ways — a export * from barrel, a bare side-effect import "./sub.js", a dynamic import(), a triple-slash /// <reference path>, and an ambient .d.ts subclass declaration each leave a file unread while a subclass in it overrides the method. The nominality argument for the receiver case failed independently: an optional private tag?: number imposes nothing on an object literal, so { run() { fetch(...) } } type-checks as that class and its body is what runs. Six more findings showed the member-write invalidation missing Object.assign(C.prototype, …), Object.defineProperty, delete, writes through a structurally-compatible alias, writes through a base-typed receiver, and a write whose value is cast to a function.

super.m() went with them: it names a base declaration but nothing proved that declaration is still the body.

What remains, and why it needs no assumption

• new C() runs C's constructor, or the inherited one when it declares none. Exact.
• super(...) runs the base the extends clause resolves to. Exact.
• this.#m() runs the body its declaration fixes. A # name is not a property: no subclass redeclares it, no code outside the class body writes it, and Object.assign, Object.defineProperty and delete cannot reach it.

Two further fixes came out of the same review: a property site whose member the checker resolves to no declaration — a nullable receiver, an any, an index signature — is now unknown rather than a silent proof, which was dropping DOM handler registrations entirely.

One reported defect is left unfixed and is pre-existing on main: Promise#then/catch/finally omit the invoke-user-code and TypeError that SpeciesConstructor and the IsPromise check imply. Declaring them needs the checker-fact exporter to discharge a synchronous throw across an async boundary the way the summary path already does, which is a separate change; the trustReason now records the gap.

Cost

Production summaries on the external codebase move to 954 unknown / 144 trusted / 319 inferred, against 1,094 / 17 / 299 before this branch and 892 / 175 / 350 with the unsound mechanism in. Roughly 60 summaries and most of the Timer attribution are the price of not publishing a proof that is wrong.

🤖 Generated with Claude Code