fix: an Array literal of numbers is numeric storage for the Add proof only while its elements are only read

changelog.d/literal-array-sum-proof.md

@@ -0,0 +1 @@
+`t = t + a[i]` over a local bound to an Array literal of numbers (`const a = [1, 2, 3]`) no longer drops the elements after a string: the Add proof (`collectors/ptr_shape_numeric.rs`, `numeric_view_value_or_undefined`) treated the literal as numeric storage whatever the body stored into it later, so the accumulator counted as a Number by construction and the numeric arm of the guarded add `fadd`ed the string it held after `(a as any)[1] = "two"` (`1two` where node prints `1two3`). A literal is now numeric storage only while every use of the local in the body is an element read or a `length` read (`retain_unwritten_literal_arrays`, applied to the stable initializers of the numeric fixpoint and to the `Ptr<Shape>` walk's const initializers); an element store, a method call, an alias, an argument or a capture voids it. Switch `PERRY_LITERAL_ARRAY_WRITE_CHECK=0` keeps today's lowering. Fixture `tests/parity/language/array/test_literal_array_sum_after_store.ts`.

crates/perry-codegen/src/collectors/ptr_shape.rs

@@ -506,6 +506,10 @@ fn collect_shape_proven_ptr_locals_impl(
         family_present,
         ..
     } = walk;
+    // An Array literal of numbers is numeric storage only while nothing but
+    // element and `length` reads use it.
+    let mut const_local_inits = const_local_inits;
+    numeric::retain_unwritten_literal_arrays(stmts, &[], &mut const_local_inits);
     // #7770: locals whose every write is number-producing by construction —
     // they let a provenance `new C(i, i + 1)` resolve its parameters.
     let mut numeric_locals = collect_numeric_by_construction_locals(

crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs

@@ -1021,3 +1021,65 @@ fn update_value_resolves_via_not_bigint() {
         "without the not-BigInt fact the update's value is unproven"
     );
 }
+
+/// `t = t + a[i]` over `const a = [1, 2, 3]`: the literal is numeric storage
+/// while only element and `length` reads use it; one element store (or any
+/// other use) voids the accumulator's proof.
+#[test]
+fn literal_array_sum_loses_its_proof_to_an_element_store() {
+    let program = |store: bool| {
+        let mut stmts = vec![
+            Stmt::Let {
+                id: 40,
+                name: "a".to_string(),
+                ty: Type::Any,
+                mutable: false,
+                init: Some(Expr::Array(
+                    vec![Expr::Integer(1), Expr::Integer(2), Expr::Integer(3)],
+                    None,
+                )),
+            },
+            Stmt::Let {
+                id: 41,
+                name: "t".to_string(),
+                ty: Type::Any,
+                mutable: true,
+                init: Some(Expr::Number(0.0)),
+            },
+        ];
+        if store {
+            stmts.push(Stmt::Expr(Expr::IndexSet {
+                object: Box::new(Expr::LocalGet(40)),
+                index: Box::new(Expr::Integer(1)),
+                value: Box::new(Expr::String("two".to_string())),
+                byte_offset: 0,
+                byte_end: 0,
+                element_offset: 0,
+            }));
+        }
+        stmts.push(counted_loop(
+            42,
+            arr_len(40),
+            vec![Stmt::Expr(Expr::LocalSet(
+                41,
+                Box::new(Expr::Binary {
+                    op: BinaryOp::Add,
+                    left: Box::new(Expr::LocalGet(41)),
+                    right: Box::new(Expr::IndexGet {
+                        element_offset: 0,
+                        byte_offset: 0,
+                        byte_end: 0,
+                        object: Box::new(Expr::LocalGet(40)),
+                        index: Box::new(Expr::LocalGet(42)),
+                    }),
+                }),
+            ))],
+        ));
+        stmts
+    };
+    assert!(numeric_locals_of(&program(false)).contains(&41));
+    assert!(
+        !numeric_locals_of(&program(true)).contains(&41),
+        "a string stored into the literal makes `t + a[i]` a concatenation"
+    );
+}

crates/perry-codegen/src/collectors/ptr_shape_numeric.rs

@@ -413,6 +413,79 @@ pub(super) fn prove_group_numeric_fields<'a>(
 
 // ── #7770: numeric-by-construction locals ──────────────────────────────────
 
+/// `PERRY_LITERAL_ARRAY_WRITE_CHECK=0` (`off`, `false`) keeps today's main:
+/// a local bound to an Array literal of numbers counts as numeric storage
+/// whatever the body later stores into it. Read per call; a compile-cache
+/// input.
+pub(crate) fn literal_array_write_check_enabled() -> bool {
+    !matches!(
+        std::env::var("PERRY_LITERAL_ARRAY_WRITE_CHECK").as_deref(),
+        Ok("0") | Ok("off") | Ok("false")
+    )
+}
+
+/// Drop from `inits` every local bound to an Array literal of numbers
+/// (`const a = [1, 2, 3]`, the Add rule's `numeric_storage`) that `stmts` use
+/// other than to read an element (`a[i]`) or `length`. An element store, a
+/// method call, an alias, an argument or a capture can put a non-Number into
+/// the Array; then `a[i]` is no Number-or-`undefined` and the accumulator of
+/// `t = t + a[i]` is no Number by construction: after
+/// `(a as any)[1] = "two"` its numeric arm `fadd`ed the string it held
+/// (`1two` where node prints `1two3`). The locals are block-scoped bindings
+/// of this body, so its expressions (closure bodies included) are all their
+/// uses.
+pub(super) fn retain_unwritten_literal_arrays(
+    stmts: &[Stmt],
+    extra: &[&Expr],
+    inits: &mut HashMap<u32, Option<&Expr>>,
+) {
+    if !literal_array_write_check_enabled() {
+        return;
+    }
+    let candidates: HashSet<u32> = inits
+        .iter()
+        .filter(|(_, init)| {
+            matches!(init, Some(Expr::Array(elements, _))
+                if elements.iter().all(|e| matches!(e, Expr::Integer(_) | Expr::Number(_))))
+        })
+        .map(|(&id, _)| id)
+        .collect();
+    if candidates.is_empty() {
+        return;
+    }
+    // Every use of a candidate, and the uses that only read it.
+    let mut uses: HashMap<u32, (usize, usize)> = HashMap::new();
+    let mut visit = |e: &Expr| {
+        let read = match e {
+            Expr::LocalGet(id) => {
+                if candidates.contains(id) {
+                    uses.entry(*id).or_default().0 += 1;
+                }
+                return;
+            }
+            Expr::IndexGet { object, .. } => object,
+            Expr::PropertyGet {
+                object, property, ..
+            } if property == "length" => object,
+            _ => return,
+        };
+        if let Expr::LocalGet(id) = read.as_ref() {
+            if candidates.contains(id) {
+                uses.entry(*id).or_default().1 += 1;
+            }
+        }
+    };
+    perry_hir::tdz_check::for_each_stmts_expr(stmts, &mut visit);
+    for e in extra {
+        perry_hir::tdz_check::for_each_expr_in(e, &mut visit);
+    }
+    for id in candidates {
+        if uses.get(&id).is_some_and(|&(all, reads)| all != reads) {
+            inits.remove(&id);
+        }
+    }
+}
+
 /// Extra leaves and entry candidates for one guarded region's F clone.
 pub(crate) struct RegionNumberAssumptions<'a> {
     pub(crate) entry_candidates: &'a HashSet<u32>,
@@ -524,6 +597,11 @@ pub(crate) fn collect_numeric_by_construction_locals_in_region<'a>(
             stable_local_inits.entry(id).or_insert(Some(*init));
         }
     }
+    retain_unwritten_literal_arrays(
+        stmts,
+        region.map_or(&[][..], |r| r.loop_control),
+        &mut stable_local_inits,
+    );
     let empty_members: HashSet<u32> = shape_members.clone();
     let empty_fields: HashSet<String> = shape_numeric_fields.clone();
     let mut numeric: HashSet<u32> = let_bound

crates/perry/src/commands/compile/compile_env.rs

@@ -199,6 +199,7 @@ pub(super) const COMPILE_ENV_VARS: &[&str] = &[
     "PERRY_LINUX_MUSL_SYSROOT",
     "PERRY_LINUX_SYSROOT",
     "PERRY_LIST_BIRTH_CAPACITY",
+    "PERRY_LITERAL_ARRAY_WRITE_CHECK",
     "PERRY_LITERAL_FOR_OF",
     "PERRY_LLD_LINK",
     "PERRY_LLVM_AR",

tests/parity/language/array/test_literal_array_sum_after_store.ts

@@ -0,0 +1,96 @@
+// `t = t + a[i]` over a local bound to an Array literal of numbers: the Add proof took the literal as numeric storage
+// whatever the body stored into it later, so the accumulator counted as a Number by construction and its numeric arm
+// `fadd`ed the string it held after a string element (`1two` where node prints `1two3`). Every use other than an
+// element or `length` read now voids the proof. Controls: unwritten literals (numeric sums), typed arrays, a
+// numeric store, sums through a helper.
+function direct(): any {
+  const a = [1, 2, 3];
+  (a as any)[1] = "two";
+  let t: any = 0;
+  for (let i = 0; i < a.length; i++) t = t + a[i];
+  return t;
+}
+function pushed(): any {
+  const a = [1, 2, 3];
+  (a as any[]).push("four", 5);
+  let t: any = 0;
+  for (let i = 0; i < a.length; i++) t = t + a[i];
+  return t;
+}
+function aliased(): any {
+  const a = [4, 5, 6];
+  const b: any = a;
+  b[0] = "x";
+  let t: any = 0;
+  for (let i = 0; i < a.length; i++) t = t + a[i];
+  return t;
+}
+function writeFirst(arr: any): void {
+  arr[0] = "w";
+}
+function viaCall(): any {
+  const a = [7, 8, 9];
+  writeFirst(a);
+  let t: any = 0;
+  for (let i = 0; i < a.length; i++) t = t + a[i];
+  return t;
+}
+function viaClosure(): any {
+  const a = [1, 1, 1];
+  const set = (k: number) => {
+    (a as any)[k] = "c";
+  };
+  set(2);
+  let t: any = 10;
+  for (let i = 0; i < a.length; i++) t = t + a[i];
+  return t;
+}
+function filled(): any {
+  const a = [1, 2, 3];
+  (a as any).fill("f", 1, 2);
+  let t: any = 0;
+  for (let i = 0; i < a.length; i++) t = t + a[i];
+  return t;
+}
+function twice(): string {
+  // The same loop over the same literal before and after a string store.
+  const a = [1, 2, 3];
+  let out = "";
+  for (let round = 0; round < 2; round++) {
+    let t: any = 0;
+    for (let i = 0; i < a.length; i++) t = t + a[i];
+    out += String(t) + ";";
+    (a as any)[0] = "s";
+  }
+  return out;
+}
+// Controls.
+function untouched(): any {
+  const a = [1.5, 2.5, 3];
+  let t: any = 0;
+  for (let i = 0; i < a.length; i++) t = t + a[i];
+  return t;
+}
+function numericStore(): any {
+  const a = [1, 2, 3];
+  a[1] = 20;
+  let t = 0;
+  for (let i = 0; i < a.length; i++) t = t + a[i];
+  return t;
+}
+function typed(): any {
+  const a = new Float64Array([1, 2, 3]);
+  (a as any)[1] = "5";
+  let t: any = 0;
+  for (let i = 0; i < a.length; i++) t = t + a[i];
+  return t;
+}
+function outOfBounds(): any {
+  const a = [1, 2];
+  let t: any = 0;
+  for (let i = 0; i <= a.length; i++) t = t + a[i];
+  return t;
+}
+console.log(direct(), pushed(), aliased(), viaCall(), viaClosure(), filled());
+console.log(twice());
+console.log(untouched(), numericStore(), typed(), outOfBounds());