Repository navigation
codegen: a method's typed body covers its index clones when the index parameters are int32 of any sign (typed set) - #14450
Merged
Merged
Conversation
added 11 commits
November 11, 2026 10:13
…ot of any sign; probes # typed_call and PERRY_SIG_DIAG
Pre-merge checks:
|
This was referenced Nov 11, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A method whose parameters feed element keys gets the non-negative index clones on main (
$idx_u31_…, with their$i32raw bodies, and the same again under the proven-thisclone). P2's selector (signature_entry::select_methods)types such a method only when the signature is at least as precise as every tier it would replace, and for the index
clone that was read as "each index parameter is an I32 whose interval starts at 0". The chess board helper
has the signature
(i32[-128,255], i32[-8,7])on main (both parameters are int32 since the board's element interval,#14429), and the index clone covers both parameters (
pieceis index-used through(piece + 6) * 128 + square).Neither interval can ever start at 0, so
setstayed untyped (why=index-clone):makeinlined three copies of the$i32index clone, kept guarded splits for the sites whose tuple is not proven non-negative, and called thedouble-ABI
set$pshape$generic0.92 times permake(198 542 calls in perft 4, 163 instructions each).What changes
signature_entry::index_param_covered,signed_index_params). An index clone's parameteris covered by an I32 signature slot of any sign. The clone proves its parameters non-negative int32s so that an
element key built from them needs no sign test. Since the unsigned bound (N10, codegen: an unsigned bound absorbs the element key's sign test (N10) #14426) an int32 key is bounded by
one unsigned compare that declines every negative key onto the property path, so the sign buys the clone nothing a
typed body lacks; and the typed body takes the parameter as a word at every site, where the clone needs each
site to prove the whole tuple non-negative, or its guarded entry. A parameter the signature gives F64 or Boxed
still keeps the clones (unchanged).
M$sigis the generic body withthe parameter in an i32 slot; only a parameter whose interval has
lo >= 0seedsnonnegative_integer_locals(
nonnegative_params, unchanged). A negative key reaches the runtime-key arm with its original value (theunsigned bound's miss arm) and names a property.
Switch, probes, witness, sabotage
PERRY_SIG_SIGNED_INDEX=0(off,false): main's rule (lo >= 0). The rule is also off withPERRY_UNSIGNED_BOUND=0, which it rests on. Compile-cache input (compile_env.rs, testsigned_index_switch_is_a_cache_input).PERRY_FACTS_DUMP:# typed_call module=<m> call=<offset> callee=<name> typed=1, ortyped=0 why=<reason>, foreach call that resolves to a body with a signature and each method call that names candidates but not one body
(
why:argument-<i>-outside-the-interval,argument-<i>-not-a-number,argument-<i>-omitted,method-not-one-target,callee-not-one-body,distinct-calls-share-the-key,spread, …). wpfactssignatures::collect; the typed call sites are unchanged (call_targetsisresolvefiltered;refusalisthe old
admitswith its reason).PERRY_SIG_DIAG=1(codegen, stderr):[perry sig] Class.method typed=1 params=(…)ortyped=0 why=<tier>foreach method a typed call reaches (
index-clone,typed-abi-clone,proven-this,proven-argument,tower,excluded-tier,excluded-shape,default,all-boxed).Fact::Signature, rep and interval at every typed site and atthe boxed entry) and the unsigned bound's witness (
Fact::UnsignedBound) cover the newly typed bodies.signed-index-negative(sabotagesignature-range): a method typed by this rule whose two indexparameters receive negative values; the sabotage claims
[0, 127]for both. Correct rc 0, sabotaged rc 86,predicate
signature.Results
Chess (qb10,
instructions:uM, one build, on vsPERRY_SIG_SIGNED_INDEX=0, twice each, identical runs,checksums and PV equal in every arm). Build r2 = 1d11007 (this branch's code merged with main e4f004e, which has
the prologue PR #14442; the PR head adds test and comment changes, a dead-code removal and the merge of main
80c09e3, not re-measured):
Before merging main (build r1 = 90d8424 on main fd6e707): 21 420.9 / 491.3 / 1 500.0 / 709.4 vs 21 968.7 /
509.9 / 1 500.0 / 723.1 (−2.49 / −3.65 / 0 / −1.89%).
Probes (chess):
[perry sig] Chess.set typed=1 params=(I32[-128,255],I32[-8,7]), offtyped=0 why=index-clone;Chess.at typed=0 why=index-clone params=(F64)on both arms (a double key reachesat; everyatcall is a fieldread call, so it has no cost).
# typed_call: all sixsetsitestyped=1, the threeaddPawnsitestyped=1(they are typed on main too: the FOLLOWUPS entry "[N1: addPawn typed sites]" is stale), one refusal in the engine
(
generateLegal,distinct-calls-share-the-key).Where it lands (r1).
set$sigis inlined at its five sites inmakeand its site inreadFen; the eight bodies ofseton main (set,$generic,$idx_u31_245_246,…$i32, and the four under$pshape) are oneset$sigandthe boxed entry.
make$sigselfset$pshape$genericself (198 542 calls)make(216 386 calls),make+setmake$sigset$pshape$genericThe +219 M of
make$sigreported in #14439 (on vsPERRY_REST_CAPACITY=0, perf record at e0f2ca1, beforePR C #14436 was merged in) does not exist on main: with the board at rest
make$sigis 5 149.5 M vs 5 250.1 M(perf record, search), 123.86 M vs 130.23 M (callgrind, perft 4). That commit was not rebuilt; the likely cause
[E] is the i32 → double crossing of each board value
makeputs into theUndoliteral, which PR C's I32 lanesremoved. The cost that is really in
makeis the one this PR starts on:set's index clones inlined into it plusthe generic body.
Peak RSS (
/usr/bin/time %M, KiB, 5 runs each, r2): search on 25 856–26 624, off 26 368–26 880; perft 18 944–19 200 both; evaluate on 18 688–19 200, off 18 944–19 456; legal 18 688–19 200 both. Equal inside the 256 KiB
allocator step.
Where else it engages (parity IR census, 2 603 programs): five programs change IR beside main's
declaration-order case, each with the same output:
test_array_reps_fields(Board.masked),test_array_reps_fields_growth(Queue.at),test_unsigned_bound(Board.at),test_rest_capacity(Board.at)and the new fixture. In each, a method's
$generic/$idx_u31/$idx_u31…$i32bodies (and the same under$pshape) become one$sig. tssrc and the three.js skin have no such method (IR and sizes equal).Gates
qb10, on vs
PERRY_SIG_SIGNED_INDEX=0. Builds: r1 = 90d8424 (the change, on main fd6e707) and r2 =1d11007 (r1 + tests + main e4f004e). The PR head 9752c1e is r2's compiler plus: the fixture's last
sections, rustfmt of two hunks, the
PERRY_SIG_DIAGexclusion entry, the removal of the deadadmits, and themerge of main 80c09e3 (clean). The rows say which build they ran on.
PERRY_VERIFY_FACTS=1)signed-index-negative: correct rc 0, sabotaged rc 86, predicatesignature)PERRY_REST_ELEMS=0, verify, GC schedule stress on, stress off}function/test_p2_signed_index_params(new),test_p2_signature_methods,test_p2_signature_functions,test_rest_capacity,test_rest_loops,test_rest_elems,test_rest_fields,test_rest_zero_sign,test_n1_int_temps,test_facts_int32_bindings,test_array_reps_fields,test_array_reps_loop_base_gcPERRY_GC_SCHEDULE_SEED=7,RATE=1)test_rest_capacity4 253 / 95 666;test_array_reps_loop_base_gc25 000 / 460 099;test_p2_signature_functions245 / 27 866. Output equals node in every armPERRY_VERIFY_FACTS=1test_gap_13049_chunked_literal_births, whose compile passes the runner's 300 s limit under load)/root/supa-one.sh, r2): every exec section on 216 508 924 B = off 216 508 924 B, each section equal (no method of Supabase changes tier)signature_entry::tests:a_signed_i32_slot_covers_an_index_clone_parameter,without_the_rule_a_negative_interval_keeps_the_index_clone; wpfactssignatures:a_signed_key_and_value_are_i32_parameters_with_their_intervals,the_probe_names_each_typed_call_and_each_refusal,without_diagnostics_there_is_no_probe_line; perrycompile_env:signed_index_switch_is_a_cache_inputsignatures25 passed; codegensignature_entry2 passed; perrycompile_env10 passed, 1 failed (codegen_env_vars_are_build_cache_inputs, "shared list must be sorted and unique", main's known failure)PERRY_SIG_DIAGexclusion entry, the removal of a dead function and the merge of main 80c09e3)num_seeds_audit2 passed; perry-hir 887 passed; perry-runtime 6 682 passed, 0 failed-D warningsadmitsunused afterrefusaltook its place): removed in the head, and the head's perry-wpfacts is clean (cargo check -p perry-wpfactswith-D warnings, on the Mac). perry-runtime 1 error, main's unused import atintl.rs:72(this PR does not touch the file). perry failed only through perry-wpfactsscripts/check_file_size.shcodegen/mod.rs3 666 vs 3 662,expr/mod.rs2 839 vs 2 838,tests/native_proof_regressions.rs15 688 vs 15 687,run_pipeline.rs6 254 vs 6 204). This PR changes no line count of an allowlisted fileNot done
See FOLLOWUPS "[typed set follow-ups]". In short:
PERRY_REST_DIAG:form=f64), where the$i32index clone took the int32 form for its non-negative key: codegen has no interval for a signed I32parameter. The typed body also computes its Zobrist keys in doubles and normalizes them by a call, as the
generic body did. Both are the next PR of this lane (
perf/int32-local-ranges: the facts' interval of an int32local reaches codegen's range proofs, and a key they bound to int32 is lowered as its i32; measured on top of
this PR: search −4.2%, perft −4.7%, evaluate −3.9%, legal −3.1%);
atis untyped (params=(f64)), which costs nothing while everyatcall is a field read call;const f = o.set) has Boxed parameters by the facts and keeps its clones(the fixture's
Kept.set).