perf(codegen): unary + proves a Number by construction — const v = +o.a goes 20 to 9 instructions (#10777)

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.

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 {