[proggeramlug]

Class F (the last solver-side class but H) of the Activation / inactive body: body entered false proofs of check mode over the full parity corpus. The rule is the solver lane's commit c5b8b61, ported to main with a switch; the differences are listed below.

The hole

A promise is never fulfilled with a thenable (ECMA-262 27.2.1.3.2 Promise Resolve Functions steps 9-15, 27.2.2.2 NewPromiseResolveThenableJob): resolving with an object whose then is callable calls that then with fresh resolve functions. The solve's resolve function (builtins::resolver, the one the executor of new Promise receives and the one a thenable's then receives) copied its argument into the settled value as it is, so

new Promise((res) => res({ then(r: any) { r(1); } })).then((v) => console.log(v));

never called the thenable's then: that body was "inactive" while it ran. Check mode rc 86 on promise/test_gap_promise_tick_parity and promise/test_new_promise_only_thenable (the latter on purpose since #14538); with PERRY_FACTS_DCE=1 the removed body traps (SIGILL). The paths through builtins::adopt (Promise.resolve, await, a handler's result) already called then, but also let the thenable itself flow on as the settled value.

The fix (the lane's rule; in the one solve)

• One constraint, Cons::Fulfil { dst }, decides from the value's then read: a primitive, ⊤, a marker, or an object token whose then read may hold a value no call takes (guard::NOT_CALLABLE: a primitive, undefined of a missing key, a non-function object, ⊤; builtins::surely_callable) fulfils as itself; an object whose then is callable is adopted instead (its settled value, its then called with resolve functions), re-checked as the read grows (monotone). A native promise reads its locked Promise.prototype.then without the chain end's undefined (builtins::locked_chain_defines), its own then values as they are.
• builtins::adopt, the resolve function (builtins::resolver, whose argument is now adopted; memoized BEFORE it adopts, since adopt asks for the same resolver) and Gen::awaited (a second copy of the rule with a plain edge) share it. A reject function (builtins::rejecter, its own memo) keeps the plain edge: a reject function adopts nothing.
• Soundness direction: the rule ADDS call edges (a thenable's then is called) and its settled values flow on. A value fulfils "as itself" only under the lane's condition; no other shortcut.
• Switch PERRY_FACTS_REACH_THENABLE=0 = the previous model (reach.rs; in the compile env list, sorted; reach_thenable_switch_is_a_cache_input; test control noreachthenable).

Differences from the lane commit c5b8b61

1. The env switch (not in the lane): reach::thenable, Model::reach_thenable, lib.rs, the compile env entry and its test. Off arms: resolver / rejecter -> plain_resolver (main's old resolver, one memo, name <resolver>), adopt keeps m.edge(v, dst), Gen::awaited -> awaited_plain (main's body). Reason: lane rule, off = today's main.
2. The settled value is main's #value field (m.atom("#value"), unchanged lines), not the lane's promise_result_atom ([[PromiseResult]] internal slot, lane commits 1852863 / 82bee0c). Reason: lane-only infrastructure.
3. Model::field instead of Model::field_r in the Fulfil apply arm (own then values of a native promise). Reason: field_r (lane 0b775b7) is field without the ENUM3 enumerable-key mark, which main does not have.
4. guard::NOT_CALLABLE keeps the lane's value 11 although main's last guard is BOXED = 7 (the lane's 8-10, BOXED_STR / BOOL / OTHER from 16cb2be, are not on main), so the lane's next merge with main meets the same constant.
5. The Cons::Fulfil match arms sit beside NotNullish; in the lane they sit beside FieldTruthy (lane 5e514c7, not on main).
6. Gen::awaited is in gen_protocol.rs (moved from gen_expr.rs by wpfacts: move the promise and iteration protocol helpers out of gen_expr.rs (pure move, file size cap) #14525); Gen::resolver_fn is removed as in the lane (its only use was awaited; the off arm calls plain_resolver).
7. The Cons::Fulfil doc says "its settled value" for "its [[PromiseResult]]" (item 2).
8. The solve/apply.rs hunk is byte-identical to the lane's, so rustfmt's wrap of its two Cons::Load { .. } lines is not applied (the lane's own text).
9. Added on main only: wpfacts tests/reach_thenable.rs (activation controls), the parity fixture, the changelog fragment, the updated comment in promise/test_new_promise_only_thenable.ts.

Notes (solver lane)

1. On main the settled value of a promise is still the #value FIELD, which a spread, an unknown-key read and a for-in can reach: Object.assign({}, promise) or {...promise} copies the settled value, and awaiting that copy yields it. Adoption does not make this worse. This PR is adoption only, not adoption plus internal-slot hygiene; the internal-slot fix ([[PromiseResult]]) comes with the solver lane's head.
2. The Fulfil arm makes two nodes per (Fulfil constraint, token) and is applied on deltas. Measured solve-size deltas are in "Measured" below. The solver's owner accepted this cost for this PR and plans a per-token read node (one then read per token instead of per (constraint, token)) as a follow-up; a comment at the arm says so.

Solver files touched (owner CWN; the lane's code)

• crates/perry-wpfacts/src/builtins.rs 595-660 (resolver, rejecter, plain_resolver, settle_fn), 679, 742-757 (adopt), 946-954 (locked_chain_defines)
• builtins/constructors.rs 57, 59; builtins/methods.rs 694-710 (surely_callable)
• gen_protocol.rs 16-80 (Gen::awaited, awaited_plain)
• model.rs 86-90, 104 (guard::NOT_CALLABLE), 1830-1832, 1876-1877; model/cons.rs 241-252, 659, 677, 717
• solve/apply.rs 417-418 (Guard), 450-493 (the Fulfil arm)
• one match arm each: demand.rs 139, records.rs 246-247 / 392 / 1842, solve.rs 294 / 1685, summary.rs 277, summary/map.rs 120 / 481, summary/packet/symbols.rs 145, zero_sign.rs 124
• reach.rs 70-80 (switch), lib.rs 588

Fixtures

• wpfacts tests/promise_adopts_thenable.rs: the lane's 8 tests, unchanged (a then-callback's promise, a resolve function given a promise, await of a returned promise, a program thenable whose then runs with the runtime resolve function, a then: 5 object fulfils as itself; controls: an unknown own then, an unknown executor, an unknown value stay open).
• wpfacts tests/reach_thenable.rs: 5 programs where a marker hit runs only through a thenable's then reached by a resolve function (the executor's resolve, awaited, a kept resolve called later, a thenable that resolves a thenable, what a thenable resolves flowing on): active with the rule, inactive with noreachthenable (the control); 3 programs reached before through adopt (Promise.resolve, await, a handler's result): active both ways.
• Parity fixture tests/parity/language/promise/test_reach_thenable_adoption.ts (13 cases incl. reject / throwing then, a native promise, a class thenable, and negative controls then: 5, no then, a then getter returning undefined, a primitive).

Measured (qb10; build of 48f1043 on main 8654fbb; this PR's switch is the arm)

The head differs from the measured build by a test-list fix, a comment line at the Fulfil arm, and merges of main (cargo check of perry-wpfacts lib + tests and perry tests, and check_file_size, green after the last merge).

• Touched tests: wpfacts whole lib suite 2513 passed / 2 failed = the known red unit_mode::contracts::a_broken_namespace_field_function_resolves_only_the_units_that_see_it (red on main) and one case of this PR's own control module (moved to the covered list; rerun on abd6978: reach_thenable 2/0, promise_adopts_thenable 8/0, filters promise 21/0, resolver 4/0, thenable 15/0, await 2/0, builtins 13/0). tests/num_seeds_audit: red on main as well (main's prim::NUM counts already differ from NUM_SEEDS.md for bindings.rs, quiet_sites.rs, solve/apply.rs); this PR adds no prim::NUM use. perry compile_env 44 / 0. check_file_size.sh green. Release build: 4 Rust warnings, all runtime, a subset of main's (none added).
• Class F programs (r09, r09b, r09c, the new fixture, promise/test_gap_promise_tick_parity, promise/test_new_promise_only_thenable, promise/test_thenable_resolution_paths): on = rc 0 and = node in default mode, check mode (0 false proofs) and with PERRY_FACTS_DCE=1. With PERRY_FACTS_REACH_THENABLE=0: check mode rc 86 (Activation) and PERRY_FACTS_DCE=1 rc 132 (SIGILL) on r09, r09c, the new fixture, tick_parity and new_promise_only_thenable, as on main; r09b (the await form) and test_thenable_resolution_paths are clean either way.
• Full parity corpus in check mode (2657 programs): on = rc 86 3 = class/test_class_key_order_first_store (perf(layout): a class's keys are laid out in the order the constructor first stores them #14485 key order), object/test_vr_replacer_hole_main (JSON replacer hole), temporal/test_gap_temporal_keyed_read_chain (class H). Off = 4 (+ promise/test_gap_promise_tick_parity). On vs off, and on vs the reach stack's run, the only (compile rc, run rc) change is tick_parity 86 -> 0; no program entered; the same 5 compile failures.
• chess on vs off on one build, each x2 (perf stat -e instructions:u): byte-identical binary (sha256 8cb24f6b62482c6a, 9 365 576 B).

workload	on (M)	off (M)	checksum / PV	peak RSS on / off (KiB)
search 250000	11 858.458, 11 858.452	11 858.454, 11 858.463	OK	26 456 / 26 788
perft 4	258.869, 258.868	258.869, 258.868	OK	19 200 / 19 200
evaluate 100000	1 191.771, 1 191.769	1 191.768, 1 191.769	OK	19 200 / 19 200
legal 10000	354.748, 354.749	354.749, 354.750	OK	19 184 / 19 176

Chess check mode: 0 misses on all four workloads.

• tssrc (on vs off, one build): lost 0, gained 0 (24 578 of 64 169 proven both), active 14 076 of 20 419 both, code identical; nodes / constraints / work identical (3 866 122 / 4 409 030 / 96 178 010): it reaches no promise.
• Solve size (switch on vs off): full-corpus sum (2653 compiled) nodes +0.73% (4 769 450 vs 4 735 020), constraints +0.87%, work +1.01% (34 343 280 vs 33 998 752); three.js skin bench nodes +0.98% (305 327 vs 302 373), constraints +0.54%, work +0.54% (3 357 682 vs 3 339 538), binary identical, proven sites 340 vs 339. Chess and tssrc: 0. Cause on skin: 992 (Fulfil constraint, token) pairs (one NOT_CALLABLE guard, two nodes and a then load each; relations S guard +992, S load +1 004, S defined +224); the settled values of three solver-born promise templates (Promise@call4086 / 4312 / 4349, 18 Fulfil constraints each) hold 595 of them (266 / 192 / 137 tokens); gen-time each resolver now adopts (a then call with fresh resolve / reject nodes: B mcall +135, new nodes +1 335). The "fulfilled as itself" condition is the lane's, unchanged. Accepted by the solver's owner; the per-token read is a planned follow-up.
• Not run: IR census, Supabase (no compile), full suites other than perry-wpfacts.

[coderabbitai]

Caution

Review failed

The pull request is closed.

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn