Skip to content

wpfacts, codegen: an element site consumes its key's interval: an int32 key takes no normalizer, a non-negative one no sign test (key signs) - #14458

Merged
proggeramlug merged 7 commits into
mainfrom
perf/index-sign-proof
Nov 11, 2026
Merged

proggeramlug merged 7 commits into
mainfrom
perf/index-sign-proof

Conversation

@proggeramlug

@proggeramlug proggeramlug commented Nov 11, 2026 •

Copy link
Copy Markdown
Contributor

The "interval proves ≥ 0" lever (CENSUS-residual cause (i), the part N10 #14426 left: "removing it is the 'interval
proves ≥ 0' case"). An element read or store whose key is only statically numeric goes through the canonical key
split: the shared normalizer perry_array_index_normalize_i32 maps every key that is no array index (a fraction,
NaN, a negative, a value past int32) to -1, and the sign of the result picks the element tier or the exact
property-key arm (since N10 the unsigned bound absorbs that test where a bound exists). When the whole-program facts
bound the key, none of that is needed. This PR exports the key interval of every element site and makes codegen
obey it.

Census first (main fd6e707, with the board at rest, #14439)

qb10, callgrind with --dump-instr=yes (exact executions per instruction; an x86-64-v3 build, valgrind cannot run
the native one), chess, all four workloads:

  • The split's own test; js/jns/cmovns on element keys is gone already: search 0.42 M executions (the N10
    miss-arm exit of one evaluate read, 2 per call), evaluate 0.20 M, perft 0, legal 0: below 0.01% everywhere. The
    other executed sign tests in chess code are no element keys: make 13.5 M (search) / 0.43 M (perft) / 0.40 M
    (legal) is the set call's index-clone admission of square and piece (lower_call/index_split.rs; piece
    really is negative; the typed-set lane), generatePseudo 2.0 M is color arithmetic, unmake 0.26 M a flag byte.

  • What is still executed is the admission in front of that test, the normalizer call (14 instructions per
    call, plus the call sequence and what the call keeps out of registers):

    workload normalizer calls self instructions share from
    search 250000 26.84 M 375.8 M 1.69% negamax (orderMoves inlined) 9.14 M, make (the set clone inlined) 8.95 M, set$pshape$generic 4.83 M, evaluate 3.31 M, repetitions 0.31 M, quiescence 0.26 M
    evaluate 100000 1.62 M 22.6 M 1.51% evaluate (own[file - 1], once per pawn)
    perft 4 0.43 M 6.1 M 1.17% make 0.23 M, set$pshape$generic 0.20 M
    legal 10000 0.40 M 5.7 M 0.77% make

    These are the keys codegen cannot prove an index by itself: evaluate's own[file - 1] (the pawn-file Arrays,
    [-1,6]), the four this.zobristA/B[(old + 6) * 128 + square] reads of set (chess.ts:466-472), and in
    orderMoves / negamax the VALUES[...], this.killers[ply * 2] and this.historyScores[from * 128 + to] reads
    and stores (:793-797, :846-849) and the insertion sort's result[i] / scores[j]. Statically the engine module
    has 47 normalizer calls and 44 property-key arms.

  • Their keys' intervals (the new probe): 36 of chess's 63 integer-key sites are non-negative int32 (VALUES
    [0,8], killers [0,254], historyScores [0,16383], the pawn-file Arrays [0,7]), 9 are int32 that may be
    negative (the zobrist keys [-384,1919], the board stores [-128,255], [-16,143]), 18 are integers past int32
    (loop counters bounded only by a .length: [0,4294967294] for a for-of, [1,2^60] for orderMoves' insertion
    sort).

What changes

  • wpfacts (element_keys::collect_signs, ModuleBindings::key_signs): every element site of any operation (a
    read, a store, a called element) whose key is an integer Number inside the int32 range at every copy, and at every
    site that shares its offset, with the hull of its interval. (element_keys, PR-C2, covers reads only and is
    unchanged.) Only the key node's own Number interval counts: a key the solve resolves to the name "3" may be that
    string at run time, so it has no key sign.
  • codegen (expr::index_key::{KeyFact, key_fact, store_key_fact, exact_i32}), at the three places that call the
    normalizer or lower an at-rest key as a double:
    • the read split (index_get/runtime_key.rs). A key proven a non-negative int32 is an array index at every
      evaluation: it is converted with one exact fptosi (or is the native integer it was widened from) and enters
      the element tier directly. No normalizer, no sign test, no -1 select, and the property-key arm is not emitted;
      the tier's own cold read serves every miss (the key may still be past the length). An int32 key that may be
      negative also takes no normalizer; its sign is handled as before (N10's miss-arm exit, or the split's test), so
      a negative key still reaches the runtime-key arm with its original double.
    • the runtime-key store (index_set.rs): an int32 key is its i32; the guarded store's one bound
      idx <u capacity declines a negative key onto the exact helper, as it declines the normalizer's -1. A source
      store a[k] = v is a PutValueSet whose index-set fast path (proxy_reflect.rs) built its IndexSet with
      element_offset: 0; it now carries the store's site offset, so the store finds its key fact.
    • at-rest reads (rest_elems::lower_read): a key only the facts prove an int32 takes the int32 forms (the
      rep-keyed tier or one k <u floor) instead of the double round trip.
  • Not touched: Array.prototype.at (a negative index counts from the end), the $idx_u31 index clones and their
    call split, typed arrays (their store keeps the normalizer), at-rest stores (rest_elems::lower_write, the
    typed-set lane's file), and a b1 call's synthesized read (it carries the body module's offset, so this module's
    key facts say nothing of it).

The evaluate site (own[file - 1], key [-1,6]; qb10, evaluate$sig, the x86-64-v3 builds of rel1):

off:  lea -0x1(%rbx),%eax ; vcvtsi2sd %eax,%xmm15,%xmm0 ; vmovsd %xmm0,-0x48(%rbp) ;
      call perry_array_index_normalize_i32 ; cmp 0x4(%r12),%eax ; jae <cold>
on:   lea -0x1(%rbx),%edx ; cmp 0x4(%rcx),%edx ; jae <cold>

Switch, probe, witness, sabotage

  • PERRY_FACTS_KEY_SIGN=0 (off, false): wpfacts exports no key sign and codegen consumes none (= main). A
    compile-cache input (compile_env.rs, test key_sign_switch_is_a_cache_input).
  • Probe (PERRY_FACTS_DUMP): # key_sign module=<m> site=<offset> op=<r|w|rw> key=[lo,hi] int32=<0|1> nonneg=<0|1>,
    one line per element site with an integer key.
  • Check mode (PERRY_VERIFY_FACTS=1): each consuming site first tests that its key is an integer inside int32 and,
    when the fact says so, not negative (index_key::witness_sign, Fact::KeySign, "key sign"); a miss reports the
    false proof and exits 86.
  • S0 arm key-sign-negative / PERRY_FACTS_SABOTAGE=keysign: every int32 key is claimed non-negative. Correct rc 0
    (the key -2 reads the named property), sabotaged rc 86, predicate key sign.

Results

Chess (qb10, instructions:u M, one build, on vs PERRY_FACTS_KEY_SIGN=0, twice each, identical runs,
checksums and PV equal in every arm).

The head's code (rel3 = d6b8328: this branch merged with main e4f004e, N12 #14442 among others):

workload on off change
search 250000 21 316.6 21 974.0 −2.99%
perft 4 497.4 511.4 −2.74%
evaluate 100000 1 425.6 1 487.8 −4.18%
legal 10000 700.9 715.8 −2.08%

Before merging main and before the stores consumed their key fact (rel1 = 88a78d4 on main fd6e707; the off
arm equals a separate build of that main on all four workloads):

workload on off = main change
search 250000 21 386.7 21 968.7 −2.65%
perft 4 498.2 509.9 −2.29%
evaluate 100000 1 437.8 1 500.0 −4.15%
legal 10000 710.4 723.1 −1.76%

Exact per function (callgrind, x86-64-v3 builds of rel3, off vs on; self instructions, M):

function search off on change evaluate perft legal
perry_array_index_normalize_i32 375.8 109.0 −266.8 22.6 → 0 6.1 → 0 5.7 → 0
make$sig 4 210.0 3 942.9 −267.1 125.2 → 117.8 140.2 → 129.8
evaluate$sig 2 532.4 2 475.7 −56.7 1 235.6 → 1 207.8
negamax$sig (recursive part, orderMoves inlined) 1 275.5 1 244.4 −31.1
set$pshape$generic 768.9 738.4 −30.5 32.3 → 31.1
total 22 301.3 21 634.4 −2.99% −3.38% −2.83% −2.19%

Normalizer calls: search 26.84 M → 7.79 M, evaluate 1.62 M → 0, perft 0.43 M → 0, legal 0.40 M → 0. Statically the
engine module goes from 47 normalizer calls to 17 and from 44 property-key arms to 30. The callers gain more than
the 14 instructions of the call: a call site keeps its live values out of the caller-saved registers. What is left
on search (0.50%; 7.35 M of the 7.79 M calls come from orderMoves' insertion sort) are keys that are integers but
not int32 by the facts; see "Not done".

Peak RSS (/usr/bin/time %M, KiB, 5 runs each). rel3, under load: search 25 600–26 368 on, 25 856–26 368
off; perft, evaluate and legal 18 688–19 456 in both arms. rel1, quieter: search 26 880 on and off (one 26 368 in
each arm), the other three 19 456 (one or two 19 200 in either arm). On = off inside the allocator's steps.

Gates

qb10, on vs PERRY_FACTS_KEY_SIGN=0. Gate builds: rel3 = d6b8328 (this branch merged with main e4f004e;
c8adb42 adds only an edit of the new parity fixture, and its arms were rerun on rel3; the PR head then merges
main 6d3cd78, typed set #14450 among others, with one additive conflict in compile_env/tests.rs: that head is cargo checked for perry-wpfacts, perry-codegen and perry with tests, not built or measured)
and rel1 =
88a78d4 (on main fd6e707, before the stores consumed their key fact). Rows without a build name are rel3's.

gate result
chess, instructions:u tables above; checksums and PV equal in every arm
chess check mode (PERRY_VERIFY_FACTS=1) compile rc 0; perft 3, legal 1000, search 20000, evaluate 1000: rc 0, 0 misses (rel1 the same)
chess IR / size IR differs in 1 of 2 modules (the engine). Every exec section: on 7 606 166 B, off 7 613 157 B: −6 991 B (.text −32, perry_js_text −6 959)
S0 rc 0, 123 executable controls pass; key-sign-negative: correct rc 0, sabotaged rc 86, predicate key sign; every older arm unchanged
parity fixtures × {on, off, verify, GC schedule stress on, stress off} 10 fixtures × 5 arms, 50/50 MATCH node v26.8.1: test_key_sign (new), test_unsigned_bound, test_range_tightening, test_array_reps_fields, test_array_reps_loop_base_gc, test_rest_capacity, test_rest_loops, test_rest_elems, test_n1_int_temps, test_facts_int32_bindings. The at-rest forms (PERRY_REST_DIAG=1) move as they should: test_key_sign 3 f64 → 2 rep + 1 rep_floor, test_rest_capacity 5 f64 / 20 rep → 3 / 22
GC schedule stress (instrumented runtime, PERRY_GC_SCHEDULE_SEED=7 at compile, PERRY_GC_SCHEDULE_SEED=7 PERRY_GC_SCHEDULE_RATE=1 at run) test_key_sign: 107 forced copying minors, 6 208 moved objects, the same in the off arm; test_array_reps_loop_base_gc 25 000 / 460 099; test_rest_capacity 4 253 / 95 666. Output equals node in every arm
parity IR census, on vs off 2 604 programs, 118 IRDIFF (every program with a consuming read or store), 0 compile-rc differences, 11 OUTDIFF: the known set that is non-deterministic or compiles in neither arm (Date.now, Math.random, pids, elapsed times). Ten of them have identical IR; the eleventh, array/test_issue63_escape, has changed IR and differs only in its three printed elapsed-millisecond lines (its sum: line is equal). rel1: 2 603 programs, 104 IRDIFF, the same 11 OUTDIFF, all with identical IR
vf, PERRY_VERIFY_FACTS=1 n = 1 538, rc86 = 0, crc ≠ 0 = 14 (the known pair test_gap_s8b_computed_fields, test_gap_10554_fn_identity_own_module, and 12 list entries no longer in the tree). rel1: the same plus test_gap_13049_chunked_literal_births at the 300 s compile timeout under load
tssrc lost sites 64 169 site lines, 24 552 proven in both arms: lost 0, gained 0 (rel1 the same). tssrc has 1 628 # key_sign lines: 554 int32, 552 of them non-negative
hello / hello2 on vs off byte-identical (md5 f446a6b50365, 07847e85a106); callgrind Ir 133 157 / 642 294 in all three runs of both arms
sizes chess −6 991 B (above); three.js skin 25 541 169 B on = off, every section equal; tssrc on 63 662 078 B, off 63 662 318 B: −240 B (.text +192, perry_js_text −432). Supabase: not run to the end (the on arm is 216 509 996 B; the off arm was stopped by the owner order of 13:40 UTC before it finished)
unit tests (new) wpfacts tests/key_signs.rs, 5: a read's and a store's interval; a key that may be negative keeps its lower bound; a fraction, a string, a string that names an index, an integer past int32 and an unbounded Number have no key sign; a compound store shares its read's hull; the sabotage. codegen expr/index_key_sign_tests.rs, 3: no fact or an interval past int32 keeps the normalizer and the property-key arm; a proven index has neither (and no miss-arm exit) in a read, a value read and a store; an int32 key that may be negative loses the normalizer and keeps its sign arm. perry key_sign_switch_is_a_cache_input
suites full library suites: not run (owner order 2026-11-11 13:40 UTC). Touched test modules: on rel1's tree (88a78d4) wpfacts array_reps 32, codegen rest 17, proven_array 19, index_get 55, index_set 10 passed, perry compile_env 9 passed and 1 failed (codegen_env_vars_are_build_cache_inputs, main's known failure); the new modules wpfacts key_signs (2 of 5 passed) and codegen index_key (13 of 15 passed) had the five failures described below. Their rerun after the fix is queued on qb10 and had no cargo slot when the PR opened; the result follows as a comment
-D warnings rel1: perry-hir, perry-wpfacts, perry-codegen, perry: 0 errors; perry-runtime: main's unused import in intl.rs. Not rerun on rel3
scripts/check_file_size.sh rel1: rc 0 (no allowlist count changes). Not rerun on rel3
rustfmt own hunks only (rustfmt --check on every touched file: the remaining diffs are main's)

A first run of the touched test modules on rel1's tree found five failures, all in this PR's new tests: three
wpfacts tests expected a hull from a single caller (the facts give the exact value), and the two codegen tests that
include a store failed because no store consumed its key fact: a[k] = v is a PutValueSet, and its index-set
fast path built the IndexSet with element_offset: 0. d6b8328 carries the site offset (the at-rest store was
already taken before that point, and no other consumer reads the offset of an IndexSet).

Not done

See FOLLOWUPS "[key-sign follow-ups]". In short:

  • an integer key past int32 keeps the normalizer: a counter bounded only by a .length is [0,4294967294] (for-of)
    or the widening ladder's top (for (let i = 1; i < xs.length; i++), j-- loops). On chess that is orderMoves'
    insertion sort: 7.35 M of the 7.79 M normalizer calls left on search (0.50%); none on the other three workloads;
  • at-rest stores and typed-array stores do not consume the key fact;
  • a b1 call's read gets no key fact (its own call_arg_ranges could give one);
  • the set call's index-clone admission in make (13.5 M sign tests on search) is the typed-set lane's.

@proggeramlug
proggeramlug merged commit 5bdb09d into main Nov 11, 2026
92 of 101 checks passed
@coderabbitai

coderabbitai Bot commented Nov 11, 2026 •

Copy link
Copy Markdown

Explain Change →

Pre-merge checks: Inconclusive 2

Failed Failed checks: 2 inconclusive

Check name Status Explanation Resolution
Title check Pending This assessment has not completed. The check will be retried on the next pre-merge check run.
Description check Pending This assessment has not completed. The check will be retried on the next pre-merge check run.
  • 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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant