[proggeramlug]

P3 B1: element reads that the whole-program facts prove plain Numbers drop their INT32 tests. Design: /root/CHB/DESIGN-p3-canonical-numbers.md rev 3.1, which answers REVIEW-p3 (R1–R7, D1–D5). It builds on #14353 (the exact int32 predicate, merged).

The fact: the NUM declaration (REVIEW-p3 R2)

• No new encoding bit. A node holds only Number when every value reaching it is either:
  • a program Number: literals and arithmetic, which codegen lowers to plain doubles; or
  • an audited builtin NUM seed.
• The audit (D2): every non-test prim::NUM use in perry-wpfacts (124) has a row in perry-wpfacts/NUM_SEEDS.md:
  • a seed row names the runtime function or the lowering that produces the value;
  • a read/map row records that the use seeds nothing.
  • tests/num_seeds_audit.rs fails when a file's count of uses differs from its rows, or when a row has no citation.
• New export (wpfacts canonical_numbers): ModuleBindings::number_element_reads.
  • An element read qualifies when, at every copy (gen copies and summarized instance copies), its value node holds
    Number, optionally undefined, and nothing else.

Spot check (15 seed rows drawn at random, seed 1109, each re-read against its cited code):

• 14 confirmed:
  • EventEmitter _ keys (NUM|UNDEF);
  • Array.from map index (from_concat.rs:557, index as f64);
  • the entries() pair index (iter_object.rs:591, idx as f64);
  • timers (NUM|timer object);
  • fresh typed-array elements (NUM|BIGINT);
  • lastIndexOf/findIndexOf (NUM|BOOL);
  • Date.now (date.rs:110 js_date_now -> wall_millis());
  • TextEncoder.encode elements (typed-array reads; REVIEW-p3 t4/t5);
  • copyWithin operand ToNumber (discarded);
  • encodeInto read/written (text.rs:535-536, as f64);
  • typed-array elements;
  • the two arithmetic and + results (solve/apply.rs);
  • Array.prototype length.
• 1 wrong citation, value still sound: typed_array_methods.rs:142 cited a non-existent
  js_typed_array_index_of. The real producer is object/native_call_method/typed_array.rs:271
  (js_array_indexOf_jsvalue(..) as f64). The row is fixed.
• Refined: the arithmetic rows now also cite the runtime dynamic-add arm (dynamic_arith.rs
dynamic_add_non_plain), which decodes INT32 operands and returns an f64.

Consumers (codegen expr/facts_canonical.rs)

• C1 compare (expr/compare.rs), when both operands are proven and at least one by the facts:
  • relationals: ordered fcmp;
  • ===/!== with a plain Number: fcmp oeq/une;
  • two Number-or-undefined operands: fcmp oeq || (bits equal && undefined), and !== is its exact negation (D1).
• C2 arithmetic (expr/binary.rs): a guarded leaf proven a Number is not tested.
• C4 parameter entry (codegen/facts_number_locals.rs): a facts-proven Number parameter takes its argument's bits
  without the INT32 conversion.
• Not in this PR: C3 (an i32 index from proven integral operands). It needs the temporaries' value_reps and
  rep_rules (DESIGN-p3 §2.4), so B1 ships without it, and it follows as its own change.

The two INT32 producers claimed by comments

value_call.rs:410 (V8) and stringify_scalars.rs:33 (sqlite) claimed live INT32 Number producers. Neither is live:

• V8 was removed in Remove perry-jsruntime (V8/deno_core) runtime — ship V8-free binaries #1696;
• every sqlite integer reader returns n as f64.

Both are proved from the code and by running against node, and raw bits are pinned by the new runtime and stdlib tests
(NUM_SEEDS.md, "INT32-box producers claimed by code comments"). The comments are fixed.

Check mode, sabotage, switch

• Witness (Fact::CanonicalNumber): every trusted operand is tested "plain double" (outside the tag band and not
  HANDLE_TAG), or exactly undefined where the fact allows it. A miss exits 86. C4 uses the existing parameter
  entry witness.
• Sabotage (D4), runtime-side:
  • PERRY_FACTS_SABOTAGE=canonnum cargo build-perry --release (scripts/p3-canonnum-runtime.sh, which also checks
    the archive's mtime) builds js_math_round to return an INT32 word.
  • S0 canonical-number-negative with --canonnum-runtime <target>/release must give rc 86. The correct arm gives
    rc 0 and node-equal output.
• Switch: PERRY_FACTS_CANONICAL_NUMBERS=0 turns off both the export and the consumers.

Gates (qb9 x86-64; merged head ba0afd6 = this branch + main 369605c)

gate	result
check -D warnings	perry-wpfacts, perry-codegen and perry clean. perry-runtime has 4 dead-code errors and the perry-stdlib build of perry-runtime adds unused imports; all are in files this PR does not touch and are pre-existing on main (as #14353 noted)
wpfacts	2046/0, plus the NUM seed audit tests 2/0
codegen lib	2837/0 on ba0afd6. On dba5d8f, 1 failure: facts_number_locals_tests still asserted C4's old INT32 entry decode. The test now asserts the new behaviour (0d43f44)
perry-runtime full suite	6603/0 plus the integration tests, including the two new v8 wire-int32 raw-bits tests
perry-stdlib sqlite::bind	3/0 (raw-double INTEGER columns, node:sqlite included)
vf (1538)	json=0 abort=0 rc86=0, crc!=0=2 (the main baseline)
lost sites	tssrc on vs PERRY_FACTS_CANONICAL_NUMBERS=0: 66666/66666 site lines, diff 0; proven 24680 = 24680; skinbench 335/8021 both
S0	43 executable controls passed (correct arms)
canonnum sabotage (D4)	scripts/p3-canonnum-runtime.sh rebuilt the archive (mtime check passed). False arm: rc 86, predicate "canonical number". With the same sabotaged runtime and B1 off: rc 0 (no consumer trusts the word)
controls vs node	test_p3_canonical_numbers.ts and REVIEW-p3's holey probe (/tmp/drev/p3.js): on, off and check mode all match node
hello / hello2	identical on vs off: text 1238 / 5926142; startup Ir 127752 / 633353
class-heavy startup (300 classes)	text −11.6 KB with B1 on. Ir over 3 runs per arm: on 38411723–38412062, off 38411509–38415252 (means: on 1358 lower). The per-function delta is in runtime HashMap<.., RandomState>::insert (a random hash seed per run) and the symbol cache, not in compiled code. No increase
IR census (parity corpus, 2522)	IR differs in 760, compile rc differs in 0, outputs differ in 9, none of them real: 4 vary between runs of one binary (PID in a warning, Date.now, Math.random, and two counts that swap between runs), and the on/off differences fall only on those lines; 5 fail to compile in both arms, so there is no output to compare
file size	clean (expr/mod.rs +1 line, allowlist re-asserted)
chess Linux instructions:u, on vs off	search 37979.7 → 37349.4 M (−1.7%); perft 907.3 → 895.9 (−1.3%); evaluate 3262.5 → 3183.1 (−2.4%); legal 1293.2 → 1248.2 (−3.5%). Fingerprints identical

The earlier rev-1 prototype measurement (p3a.txt, "BUILD FAILED") ran without the GC sidecar and is not part of these gates.

Files

• wpfacts: canonical_numbers.rs (new), gen.rs/gen_expr.rs (record element value nodes), bindings.rs, lib.rs,
  NUM_SEEDS.md, tests/num_seeds_audit.rs.
• codegen: expr/facts_canonical.rs (new), compare.rs, binary.rs, codegen/facts_number_locals.rs,
  program_facts_view.rs, verify_facts/coverage.rs, expr/mod.rs (+1 line, allowlist re-asserted).
• perry: program_facts.rs, compile_env.rs.
• runtime: math.rs (the build-time sabotage branch).
• Scripts: S0 entry and fixture, p3-canonnum-runtime.sh.
• Changelog: wpfacts-p3-b1-canonical-numbers.md.

[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