diff --git a/changelog.d/10777-unary-pos-numeric.md b/changelog.d/10777-unary-pos-numeric.md new file mode 100644 index 0000000000..421f220a14 --- /dev/null +++ b/changelog.d/10777-unary-pos-numeric.md @@ -0,0 +1,7 @@ +**Unary `+` now proves a Number by construction.** + +`expr_numeric_by_construction` required `rec(operand)` for `Pos` as though it were a soundness guard. It is not: unary `+` is ToNumber, which either completes holding a Number or throws — BigInt and Symbol throw, an object re-enters ToNumber after ToPrimitive, `undefined` is NaN. A throw stores no value, so the store-universe question the fixpoint asks is vacuous there. + +`Neg` and `BitNot` keep their condition, because ToNumeric is BigInt-preserving (`-1n` is `-1n`). + +The missed proof left the *accumulator* unproven, so its add kept a per-iteration tag test: `const v = +o.a; … h += v` goes **20 → 9 instructions per iteration**, the same figure `o.a * 1` and `o.a - 0` already reached. diff --git a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs index 7c1c69c9cd..a29c049847 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs +++ b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs @@ -626,9 +626,26 @@ pub(super) fn expr_numeric_by_construction( | Expr::PodLayoutAlignOf { .. } | Expr::PodLayoutOffsetOf { .. } => true, Expr::Unary { op, operand } => match op { - perry_hir::UnaryOp::Neg | perry_hir::UnaryOp::Pos | perry_hir::UnaryOp::BitNot => { - rec(operand) - } + // Unary `+` is ToNumber, and ToNumber either COMPLETES with a + // Number or THROWS — there is no input for which `+x` finishes + // holding something else. A BigInt and a Symbol both throw a + // TypeError, an object goes through ToPrimitive and then ToNumber + // again (so a `valueOf` returning a string yields a Number, and + // one returning a BigInt throws), `undefined` is NaN, and NaN is + // a Number. A throw stores no value, so the store-universe + // question this fixpoint asks is vacuous on that path. + // + // So `Pos` needs no operand condition at all. Requiring + // `rec(operand)` here was not a soundness guard, it was a missed + // proof: `const v = +o.a; for (…) h += v` left the ACCUMULATOR + // unproven, and `h`'s add kept a per-iteration tag test — 20 + // Ir/iteration where `o.a * 1` and `o.a - 0` reach 9 (#10777). + // `const v = +a[0]` on a Float64Array is the same 20 -> 9. + perry_hir::UnaryOp::Pos => true, + // `-x` and `~x` are ToNumeric, which is BigInt-preserving: + // `-1n` is `-1n` and `~1n` is `-2n`, both BigInts, neither a + // Number. They therefore keep their operand condition unchanged. + perry_hir::UnaryOp::Neg | perry_hir::UnaryOp::BitNot => rec(operand), _ => false, }, Expr::Binary { op, left, right } => match op {