From 6e83d26e95362a3c0e1f3a22dc3a61ba0b8064bb Mon Sep 17 00:00:00 2001
From: Chris Tate <chris@ctate.dev>
Date: Thu, 8 Oct 2026 21:55:09 -0500
Subject: [PATCH] Read in-bounds string elements without boxing

- String element reads proven to be inside the string (counted loops, `i < text.length` guards, early exits, const length aliases) give plain strings, so one-character helpers keep plain string parameters
- Unproven, fractional, negative and out-of-range reads still give `undefined`, with new corpus programs pinning both directions
---
 .../src/frontend/lowering/lower-exprs.ts      |  11 +
 .../compiler/src/frontend/lowering/lowerer.ts |  19 +-
 .../lowering/string-index-bounds.test.ts      | 235 +++++++
 .../frontend/lowering/string-index-bounds.ts  | 598 ++++++++++++++++++
 .../test/ts7/baselines/order-parity.json      |  12 +
 tests/corpus/4080-string-index-bounds.ts      | 111 ++++
 tests/corpus/4081-string-index-unproven.ts    | 127 ++++
 7 files changed, 1111 insertions(+), 2 deletions(-)
 create mode 100644 packages/compiler/src/frontend/lowering/string-index-bounds.test.ts
 create mode 100644 packages/compiler/src/frontend/lowering/string-index-bounds.ts
 create mode 100644 tests/corpus/4080-string-index-bounds.ts
 create mode 100644 tests/corpus/4081-string-index-unproven.ts

diff --git a/packages/compiler/src/frontend/lowering/lower-exprs.ts b/packages/compiler/src/frontend/lowering/lower-exprs.ts
index e79133d40..d9534dca1 100644
--- a/packages/compiler/src/frontend/lowering/lower-exprs.ts
+++ b/packages/compiler/src/frontend/lowering/lower-exprs.ts
@@ -6868,6 +6868,17 @@ export function lowerElementAccess(lowerer: Lowerer, expr: ts.ElementAccessExpre
         expr.argumentExpression,
       );
       if (index.type.kind === "f64" && recv.type.kind === "string") {
+        // A proven in-bounds integer index always names a code unit, where
+        // charAt and the property read agree.
+        if (lowerer.stringIndexBounds.inBounds(expr))
+          return {
+            kind: "strIntrinsic",
+            method: "charAt",
+            receiver: recv,
+            args: [index],
+            type: STRING,
+            loc: locOf(expr),
+          };
         return lowerOptionalStringIndex(
           lowerer,
           recv,
diff --git a/packages/compiler/src/frontend/lowering/lowerer.ts b/packages/compiler/src/frontend/lowering/lowerer.ts
index 455da4a90..23b6097e7 100644
--- a/packages/compiler/src/frontend/lowering/lowerer.ts
+++ b/packages/compiler/src/frontend/lowering/lowerer.ts
@@ -67,6 +67,7 @@ import {
 } from "./lower-builtin-values.js";
 import { everyExprChild, everyStmtChild, transformStmtList } from "../../ir/traverse.js";
 import { RuntimeOptionalProvenance } from "./runtime-optional-provenance.js";
+import { StringIndexBounds } from "./string-index-bounds.js";
 import { RuntimeOptionalLocals } from "./runtime-optional-locals.js";
 import { sanitizeUnregisteredClassTypes } from "./sanitize-class-types.js";
 import { UnregisteredClassTypes } from "./unregistered-class-types.js";
@@ -1570,6 +1571,18 @@ export class Lowerer {
   /** Per-symbol result of the never-reassigned file scan
    * (bindingNeverReassigned — object-literal generic-method receivers). */
   readonly neverReassignedCache = new Map<ts.Symbol, boolean>();
+  private stringIndexBoundsCache: StringIndexBounds | null = null;
+  /** Proofs that a string element read names an existing code unit. The
+   * indexed-read analysis and expression lowering share one instance, so a
+   * read's representation and its callers' signatures always agree. */
+  get stringIndexBounds(): StringIndexBounds {
+    this.stringIndexBoundsCache ??= new StringIndexBounds(
+      (node) => this.checker.getSymbolAtLocation(node) ?? null,
+      (symbol) => this.checker.valueDeclarationOf(symbol),
+      (node) => (this.typeOf(node).flags & ts.TypeFlags.StringLike) !== 0,
+    );
+    return this.stringIndexBoundsCache;
+  }
   /** Syntactic writes indexed once per JS scope. Symbol and RHS type
    * checks remain contextual to each binding probe. */
   readonly jsBindingWritesByOwner = new Map<ts.Node, Map<string, ts.BinaryExpression[]>>();
@@ -3806,7 +3819,8 @@ export class Lowerer {
       const e = peel(node);
       if (!ts.isElementAccessExpression(e)) return false;
       const kind = this.mapTypeOf(this.typeOf(e.expression))?.kind;
-      return kind === "array" || kind === "string";
+      if (kind === "string") return !this.stringIndexBounds.inBounds(e);
+      return kind === "array";
     };
     const isDynamicObjectEntryRead = (node: ts.Expression): boolean => {
       const read = peel(node);
@@ -3927,7 +3941,8 @@ export class Lowerer {
         const t = this.mapTypeOf(this.typeOf(part));
         if (t?.kind !== "string") return false;
         const recv = this.mapTypeOf(this.typeOf(p.expression));
-        return recv?.kind === "string" || (recv?.kind === "array" && recv.elem.kind === "string");
+        if (recv?.kind === "string") return !this.stringIndexBounds.inBounds(p);
+        return recv?.kind === "array" && recv.elem.kind === "string";
       };
       const primitive = (part: ts.Expression): boolean => {
         const t = this.mapTypeOf(this.typeOf(part));
diff --git a/packages/compiler/src/frontend/lowering/string-index-bounds.test.ts b/packages/compiler/src/frontend/lowering/string-index-bounds.test.ts
new file mode 100644
index 000000000..52d6116bc
--- /dev/null
+++ b/packages/compiler/src/frontend/lowering/string-index-bounds.test.ts
@@ -0,0 +1,235 @@
+import { mkdtemp, readFile, rm, writeFile } from "node:fs/promises";
+import { tmpdir } from "node:os";
+import { join } from "node:path";
+import { expect, test } from "vitest";
+import { compile, deserializeModule, validateModule } from "../../index.js";
+import type { IrModule } from "../../ir/ir.js";
+
+async function lower(source: string): Promise<IrModule> {
+  const dir = await mkdtemp(join(tmpdir(), "scriptc-string-index-bounds-"));
+  try {
+    const entry = join(dir, "main.ts"),
+      output = join(dir, "main.ir.json");
+    await writeFile(entry, source);
+    const result = await compile(entry, {
+      outDir: dir,
+      outPath: output,
+      outputKind: "ir",
+    });
+    if (!result.ok)
+      throw new Error(result.diagnostics.map((item) => `${item.code}: ${item.message}`).join("\n"));
+    const module = deserializeModule(await readFile(output, "utf8"));
+    expect(validateModule(module)).toEqual([]);
+    return module;
+  } finally {
+    await rm(dir, { recursive: true, force: true });
+  }
+}
+
+/** Functions whose string element reads keep the optional (checked) form. */
+function optionalReads(module: IrModule): Set<string> {
+  return new Set(
+    module.functions
+      .filter((fn) => fn.locals.some((local) => local.name === "%indexedString"))
+      .map((fn) => fn.name),
+  );
+}
+
+const PROVEN = `
+function upward(s: string): string {
+  let out = "";
+  for (let i = 0; i < s.length; i++) out += s[i];
+  return out;
+}
+function downward(s: string): string {
+  let out = "";
+  for (let i = s.length - 1; i >= 0; i--) out += s[i];
+  return out;
+}
+function stepped(s: string): string {
+  let out = "";
+  for (let i = 1; i < s.length; i += 2) out += s[i];
+  return out;
+}
+function scanned(s: string): number {
+  let words = 0;
+  let i = 0;
+  while (i < s.length) {
+    const ch = s[i];
+    if (ch === " ") { i++; continue; }
+    while (i < s.length && s[i] !== " ") i++;
+    words++;
+  }
+  return words;
+}
+function exitFirst(s: string): string {
+  let i = 0;
+  while (true) {
+    if (i >= s.length) return "";
+    if (s[i] !== " ") return s[i];
+    i++;
+  }
+}
+function aliased(s: string): number {
+  const n = s.length;
+  let count = 0;
+  for (let i = 0; i < n; i++) if (s[i] === "a") count++;
+  return count;
+}
+function inclusive(s: string): number {
+  let count = 0;
+  for (let i = 0; i <= s.length - 1; i++) if (s[i] === "b") count++;
+  return count;
+}
+function choice(s: string): string {
+  const i = 2;
+  return i < s.length ? s[i] : "-";
+}
+function negated(s: string): string {
+  let i = 0;
+  if (!(i < s.length)) return "-";
+  return s[i];
+}
+function trimmed(s: string): number {
+  let end = s.length - 1;
+  while (end >= 0 && s[end] === " ") end--;
+  return end + 1;
+}
+function nested(text: string): number {
+  const count = (): number => {
+    let k = 0;
+    for (let i = 0; i < text.length; i++) if (text[i] === "x") k++;
+    return k;
+  };
+  return count() + count();
+}
+console.log(upward("ab"), downward("ab"), stepped("abcd"), scanned("a b"), exitFirst(" q"));
+console.log(aliased("aa"), inclusive("bb"), choice("abc"), negated("z"), trimmed("a "), nested("x"));
+`;
+
+const UNPROVEN = `
+function bumped(s: string): string | undefined {
+  let i = 0;
+  if (i < s.length) { i++; return s[i]; }
+  return "";
+}
+function innerLoop(s: string): string {
+  let out = "";
+  let i = 0;
+  if (i < s.length) for (let k = 0; k < 3; k++) { out += String(s[i]); i++; }
+  return out;
+}
+function replaced(s: string): string | undefined {
+  let t = s;
+  const i = 1;
+  if (i < t.length) { t = ""; return t[i]; }
+  return "";
+}
+function capturedText(s: string): string {
+  let t = s;
+  const clear = (): void => { t = ""; };
+  let out = "";
+  for (let i = 0; i < t.length; i++) { clear(); out += String(t[i]); }
+  return out;
+}
+function capturedIndex(s: string): string {
+  let i = 0;
+  const skip = (): void => { i += 5; };
+  let out = "";
+  while (i < s.length) { skip(); out += String(s[i]); }
+  return out;
+}
+function fractional(s: string): string | undefined {
+  const i = 0.5;
+  return i < s.length ? s[i] : "";
+}
+function negative(s: string): string | undefined {
+  const i = -1;
+  return i < s.length ? s[i] : "";
+}
+function pastEnd(s: string): string {
+  let out = "";
+  for (let i = 0; i <= s.length; i++) out += String(s[i]);
+  return out;
+}
+function otherText(s: string, t: string): string {
+  let out = "";
+  for (let i = 0; i < s.length; i++) out += String(t[i]);
+  return out;
+}
+function parameterIndex(s: string, i: number): string | undefined {
+  return i < s.length ? s[i] : "";
+}
+function afterLoop(s: string): string | undefined {
+  let i = 0;
+  do { i++; } while (i < s.length);
+  return s[i];
+}
+function unguarded(s: string): string | undefined {
+  const i = 0;
+  return s[i];
+}
+console.log(bumped("a"), innerLoop("ab"), replaced("ab"), capturedText("ab"), capturedIndex("ab"));
+console.log(fractional("a"), negative("a"), pastEnd("a"), otherText("abc", "a"), parameterIndex("a", 0.5));
+console.log(afterLoop("ab"), unguarded(""));
+`;
+
+test("proven in-bounds string element reads lower to plain strings", async () => {
+  const module = await lower(PROVEN);
+  const names = [
+    "upward",
+    "downward",
+    "stepped",
+    "scanned",
+    "exitFirst",
+    "aliased",
+    "inclusive",
+    "choice",
+    "negated",
+    "trimmed",
+    "nested",
+  ];
+  for (const name of names)
+    expect(
+      module.functions.some((fn) => fn.name === name),
+      name,
+    ).toBe(true);
+  expect([...optionalReads(module)]).toEqual([]);
+});
+
+test("reads without a bounds proof keep the optional result", async () => {
+  const module = await lower(UNPROVEN);
+  const optional = optionalReads(module);
+  for (const name of [
+    "bumped",
+    "innerLoop",
+    "replaced",
+    "capturedText",
+    "capturedIndex",
+    "fractional",
+    "negative",
+    "pastEnd",
+    "otherText",
+    "parameterIndex",
+    "afterLoop",
+    "unguarded",
+  ])
+    expect(optional.has(name), name).toBe(true);
+});
+
+test("a callee keeps a plain string parameter when every caller is proven", async () => {
+  const module = await lower(`
+function isDigit(ch: string): boolean { return ch >= "0" && ch <= "9"; }
+function isUpper(ch: string): boolean { return ch >= "A" && ch <= "Z"; }
+function count(text: string): number {
+  let n = 0;
+  for (let i = 0; i < text.length; i++) if (isDigit(text[i])) n++;
+  return n;
+}
+function peekUpper(text: string, at: number): boolean { return isUpper(text[at]); }
+console.log(count("a1b2"), peekUpper("Ab", 0), peekUpper("Ab", 9));
+`);
+  const param = (name: string) => module.functions.find((fn) => fn.name === name)!.params[0]!.type;
+  expect(param("isDigit")).toEqual({ kind: "string" });
+  expect(param("isUpper").kind).toBe("union");
+});
diff --git a/packages/compiler/src/frontend/lowering/string-index-bounds.ts b/packages/compiler/src/frontend/lowering/string-index-bounds.ts
new file mode 100644
index 000000000..43368556c
--- /dev/null
+++ b/packages/compiler/src/frontend/lowering/string-index-bounds.ts
@@ -0,0 +1,598 @@
+import * as ts from "../ts7/adapter.js";
+import { isJsSourceFile } from "../program.js";
+
+/* Proves that a string element read `text[i]` names an existing UTF-16 code
+ * unit, so the read always yields a one-character string and never
+ * undefined. Strings are immutable and have no holes: the read is present
+ * exactly when `i` is an integer with `0 <= i < text.length`.
+ *
+ * The proof is syntactic and local. Both operands must be plain bindings.
+ * The index binding is a block-scoped local whose every write keeps it an
+ * integer (literals, `x.length`, constant steps). Bounds come from the
+ * binding's own writes (a counter that only grows from a non-negative
+ * literal, or one that only shrinks from `text.length - k`) or from a guard
+ * that dominates the read: a loop or `if` condition, the left side of `&&`
+ * or `||`, a conditional, or an earlier `if (...) <exit>` statement.
+ *
+ * A guard holds at the read only when neither binding can change between
+ * them. Every write of either binding must be in the function that declares
+ * it, so calls cannot reach one; no write may sit between the guard and the
+ * read in source order; and no loop between them may write either binding,
+ * since a later iteration would observe it. Reads in a nested function only
+ * use guards inside that function. */
+
+type Bound = "upper" | "lower";
+
+interface Write {
+  /** Start of the written identifier (or declaration name). */
+  at: number;
+  /** A constant integer step (`i++`, `i -= 2`), an assigned value, or an
+   * untracked write such as destructuring. */
+  step: number | null;
+  value: ts.Expression | null;
+}
+
+interface Binding {
+  container: ts.Node;
+  declaration: ts.Node;
+  writes: Write[];
+  /** Some write sits in a function other than the declaring one. */
+  escapes: boolean;
+  /** No write beyond the declaration's own initializer. */
+  constant: boolean;
+}
+
+interface IndexFacts {
+  integer: boolean;
+  nonNegative: boolean;
+  /** Always below this string binding's length. */
+  belowLengthOf: ts.Symbol | null;
+}
+
+const NO_FACTS: IndexFacts = {
+  integer: false,
+  nonNegative: false,
+  belowLengthOf: null,
+};
+
+function peel(node: ts.Expression): ts.Expression {
+  let e = node;
+  while (ts.isParenthesizedExpression(e)) e = e.expression;
+  return e;
+}
+
+function isBoundary(node: ts.Node): boolean {
+  return (
+    ts.isSourceFile(node) ||
+    ts.isFunctionLike(node) ||
+    ts.isClassStaticBlockDeclaration(node) ||
+    ts.isPropertyDeclaration(node)
+  );
+}
+
+function containerOf(node: ts.Node): ts.Node {
+  let n = node.parent;
+  while (n && !isBoundary(n)) n = n.parent;
+  return n ?? node.getSourceFile();
+}
+
+function isLoop(node: ts.Node): boolean {
+  return (
+    ts.isForStatement(node) ||
+    ts.isForOfStatement(node) ||
+    ts.isForInStatement(node) ||
+    ts.isWhileStatement(node) ||
+    ts.isDoStatement(node)
+  );
+}
+
+function integerLiteral(node: ts.Expression): number | null {
+  const e = peel(node);
+  if (ts.isNumericLiteral(e)) {
+    const value = Number(e.text);
+    return Number.isSafeInteger(value) ? value : null;
+  }
+  if (
+    ts.isPrefixUnaryExpression(e) &&
+    e.operator === ts.SyntaxKind.MinusToken &&
+    ts.isNumericLiteral(e.operand)
+  ) {
+    const value = Number(e.operand.text);
+    return Number.isSafeInteger(value) && value !== 0 ? -value : null;
+  }
+  return null;
+}
+
+/** An always-exiting statement: control never reaches the next sibling. */
+function exits(node: ts.Statement): boolean {
+  if (
+    ts.isReturnStatement(node) ||
+    ts.isThrowStatement(node) ||
+    ts.isBreakStatement(node) ||
+    ts.isContinueStatement(node)
+  )
+    return true;
+  if (ts.isBlock(node)) {
+    const last = node.statements[node.statements.length - 1];
+    return last !== undefined && exits(last);
+  }
+  return false;
+}
+
+/** The identifier's role when it is written, or null for a read. */
+function writeOf(id: ts.Identifier): Write | null {
+  let n: ts.Node = id;
+  let destructured = false;
+  for (;;) {
+    const p: ts.Node | undefined = n.parent;
+    if (!p) return null;
+    if (ts.isBinaryExpression(p)) {
+      const k = p.operatorToken.kind;
+      if (p.left !== n || k < ts.SyntaxKind.FirstAssignment || k > ts.SyntaxKind.LastAssignment)
+        return null;
+      const at = id.getStart();
+      if (destructured) return { at, step: null, value: null };
+      if (k === ts.SyntaxKind.EqualsToken) return { at, step: null, value: p.right };
+      const amount = integerLiteral(p.right);
+      if (amount !== null && k === ts.SyntaxKind.PlusEqualsToken)
+        return { at, step: amount, value: null };
+      if (amount !== null && k === ts.SyntaxKind.MinusEqualsToken)
+        return { at, step: -amount, value: null };
+      return { at, step: null, value: null };
+    }
+    if (ts.isPostfixUnaryExpression(p) || ts.isPrefixUnaryExpression(p)) {
+      if (
+        p.operand !== n ||
+        (p.operator !== ts.SyntaxKind.PlusPlusToken && p.operator !== ts.SyntaxKind.MinusMinusToken)
+      )
+        return null;
+      if (destructured) return { at: id.getStart(), step: null, value: null };
+      return {
+        at: id.getStart(),
+        step: p.operator === ts.SyntaxKind.PlusPlusToken ? 1 : -1,
+        value: null,
+      };
+    }
+    if (ts.isForOfStatement(p) || ts.isForInStatement(p))
+      return p.initializer === n ? { at: id.getStart(), step: null, value: null } : null;
+    if (ts.isParenthesizedExpression(p)) {
+      n = p;
+      continue;
+    }
+    if (
+      ts.isArrayLiteralExpression(p) ||
+      ts.isSpreadElement(p) ||
+      ts.isSpreadAssignment(p) ||
+      ts.isShorthandPropertyAssignment(p) ||
+      ts.isObjectLiteralExpression(p) ||
+      (ts.isPropertyAssignment(p) && p.initializer === n)
+    ) {
+      destructured = true;
+      n = p;
+      continue;
+    }
+    return null;
+  }
+}
+
+export class StringIndexBounds {
+  private readonly proofs = new Map<ts.Node, boolean>();
+  private readonly bindings = new Map<ts.Symbol, Binding | null>();
+  private readonly indexFacts = new Map<ts.Symbol, IndexFacts>();
+  private readonly identifiers = new Map<ts.Node, Map<string, ts.Identifier[]>>();
+
+  constructor(
+    private readonly symbolAt: (node: ts.Node) => ts.Symbol | null,
+    private readonly declarationOf: (symbol: ts.Symbol) => ts.Node | undefined,
+    private readonly isString: (node: ts.Expression) => boolean,
+  ) {}
+
+  /** True when `read` (an element access on a string receiver) is proven
+   * to name an existing code unit. */
+  inBounds(read: ts.ElementAccessExpression): boolean {
+    const cached = this.proofs.get(read);
+    if (cached !== undefined) return cached;
+    const proven = this.prove(read);
+    this.proofs.set(read, proven);
+    return proven;
+  }
+
+  private prove(read: ts.ElementAccessExpression): boolean {
+    // JavaScript declarations are not checked against callers.
+    if (read.questionDotToken || isJsSourceFile(read.getSourceFile())) return false;
+    const textNode = read.expression;
+    const indexNode = read.argumentExpression;
+    if (!ts.isIdentifier(textNode) || !ts.isIdentifier(indexNode)) return false;
+    if (writeOfElement(read)) return false;
+    const textSymbol = this.symbolAt(textNode);
+    const indexSymbol = this.symbolAt(indexNode);
+    if (!textSymbol || !indexSymbol || textSymbol === indexSymbol) return false;
+    const container = containerOf(read);
+    const text = this.binding(textSymbol);
+    if (!text || text.escapes || (!text.constant && text.container !== container)) return false;
+    // Sloppy-mode `arguments` aliases parameters.
+    if (ts.isParameter(text.declaration) && this.namesIn(text.container).has("arguments"))
+      return false;
+    const index = this.binding(indexSymbol);
+    if (!index || index.escapes || index.container !== container) return false;
+    const facts = this.indexFactsOf(indexSymbol, index);
+    if (!facts.integer) return false;
+    const symbols = [textSymbol, indexSymbol];
+    const upper =
+      (facts.belowLengthOf === textSymbol && text.constant) ||
+      this.guarded(read, "upper", indexSymbol, textSymbol, symbols);
+    if (!upper) return false;
+    return facts.nonNegative || this.guarded(read, "lower", indexSymbol, textSymbol, symbols);
+  }
+
+  private namesIn(container: ts.Node): Map<string, ts.Identifier[]> {
+    let names = this.identifiers.get(container);
+    if (names) return names;
+    names = new Map();
+    const found = names;
+    ts.walkPreorder(container, (node) => {
+      if (!ts.isIdentifier(node)) return;
+      const list = found.get(node.text);
+      if (list) list.push(node);
+      else found.set(node.text, [node]);
+    });
+    this.identifiers.set(container, names);
+    return names;
+  }
+
+  /** Every write of a block-scoped local or parameter, or null for any
+   * other binding (module imports, var, class members, ...). */
+  private binding(symbol: ts.Symbol): Binding | null {
+    if (this.bindings.has(symbol)) return this.bindings.get(symbol)!;
+    const result = this.scanBinding(symbol);
+    this.bindings.set(symbol, result);
+    return result;
+  }
+
+  private scanBinding(symbol: ts.Symbol): Binding | null {
+    const declaration = this.declarationOf(symbol);
+    if (!declaration) return null;
+    let nameNode: ts.Node;
+    const writes: Write[] = [];
+    if (ts.isVariableDeclaration(declaration)) {
+      const list = declaration.parent;
+      if (
+        !ts.isIdentifier(declaration.name) ||
+        !ts.isVariableDeclarationList(list) ||
+        !(list.flags & (ts.NodeFlags.Let | ts.NodeFlags.Const))
+      )
+        return null;
+      nameNode = declaration.name;
+      if (ts.isForOfStatement(list.parent) || ts.isForInStatement(list.parent)) {
+        // Each iteration binds a fresh constant; a `let` element may change.
+        if (!(list.flags & ts.NodeFlags.Const)) return null;
+      } else if (declaration.initializer) {
+        writes.push({
+          at: declaration.name.getStart(),
+          step: null,
+          value: declaration.initializer,
+        });
+      } else return null;
+    } else if (ts.isParameter(declaration)) {
+      if (!ts.isIdentifier(declaration.name) || declaration.dotDotDotToken) return null;
+      nameNode = declaration.name;
+    } else return null;
+    const container = containerOf(declaration);
+    let escapes = false;
+    let assigned = 0;
+    for (const id of this.namesIn(container).get(symbol.name) ?? []) {
+      if (id === nameNode) continue;
+      const write = writeOf(id);
+      if (!write) continue;
+      // A destructuring or loop target may name the binding through a
+      // shorthand property; count any same-named target conservatively.
+      if (write.step === null && write.value === null) {
+        writes.push(write);
+        assigned++;
+        if (containerOf(id) !== container) escapes = true;
+        continue;
+      }
+      if (this.symbolAt(id) !== symbol) continue;
+      writes.push(write);
+      assigned++;
+      if (containerOf(id) !== container) escapes = true;
+    }
+    return {
+      container,
+      declaration,
+      writes,
+      escapes,
+      constant: assigned === 0,
+    };
+  }
+
+  private valueFacts(value: ts.Expression): IndexFacts {
+    const literal = integerLiteral(value);
+    if (literal !== null) return { integer: true, nonNegative: literal >= 0, belowLengthOf: null };
+    const e = peel(value);
+    if (this.lengthOf(e)) return { integer: true, nonNegative: true, belowLengthOf: null };
+    if (
+      ts.isBinaryExpression(e) &&
+      (e.operatorToken.kind === ts.SyntaxKind.MinusToken ||
+        e.operatorToken.kind === ts.SyntaxKind.PlusToken)
+    ) {
+      const of = this.lengthOf(peel(e.left));
+      const amount = integerLiteral(e.right);
+      if (of && amount !== null) {
+        const delta = e.operatorToken.kind === ts.SyntaxKind.PlusToken ? amount : -amount;
+        return {
+          integer: true,
+          nonNegative: delta >= 0,
+          belowLengthOf: delta <= -1 ? of : null,
+        };
+      }
+    }
+    return NO_FACTS;
+  }
+
+  /** `text.length` on a string binding: its symbol, else null. */
+  private lengthOf(e: ts.Expression): ts.Symbol | null {
+    if (
+      !ts.isPropertyAccessExpression(e) ||
+      e.questionDotToken ||
+      e.name.text !== "length" ||
+      !ts.isIdentifier(e.expression) ||
+      !this.isString(e.expression)
+    )
+      return null;
+    return this.symbolAt(e.expression);
+  }
+
+  private indexFactsOf(symbol: ts.Symbol, binding: Binding): IndexFacts {
+    const cached = this.indexFacts.get(symbol);
+    if (cached) return cached;
+    let facts: IndexFacts = NO_FACTS;
+    if (ts.isVariableDeclaration(binding.declaration)) {
+      const [initial, ...rest] = binding.writes;
+      facts = initial?.value ? this.valueFacts(initial.value) : NO_FACTS;
+      for (const write of rest) {
+        if (!facts.integer) break;
+        if (write.step !== null) {
+          facts = {
+            integer: true,
+            nonNegative: facts.nonNegative && write.step > 0,
+            belowLengthOf: write.step < 0 ? facts.belowLengthOf : null,
+          };
+        } else if (write.value) {
+          const value = this.valueFacts(write.value);
+          facts = {
+            integer: value.integer,
+            nonNegative: facts.nonNegative && value.nonNegative,
+            belowLengthOf: value.belowLengthOf === facts.belowLengthOf ? facts.belowLengthOf : null,
+          };
+        } else facts = NO_FACTS;
+      }
+    }
+    this.indexFacts.set(symbol, facts);
+    return facts;
+  }
+
+  /** `text.length`, or a const binding initialized from it while `text`
+   * itself is never reassigned. */
+  private isLength(node: ts.Expression, text: ts.Symbol): boolean {
+    const e = peel(node);
+    if (ts.isPropertyAccessExpression(e)) return this.lengthOf(e) === text;
+    if (!ts.isIdentifier(e)) return false;
+    const alias = this.symbolAt(e);
+    const declaration = alias ? this.declarationOf(alias) : undefined;
+    if (
+      !declaration ||
+      !ts.isVariableDeclaration(declaration) ||
+      !declaration.initializer ||
+      !ts.isVariableDeclarationList(declaration.parent) ||
+      !(declaration.parent.flags & ts.NodeFlags.Const)
+    )
+      return false;
+    if (this.lengthOf(peel(declaration.initializer)) !== text) return false;
+    return this.binding(text)?.constant === true;
+  }
+
+  /** `text.length - k` for an integer k >= 1. */
+  private isLengthMinusOne(node: ts.Expression, text: ts.Symbol): boolean {
+    const e = peel(node);
+    if (!ts.isBinaryExpression(e) || e.operatorToken.kind !== ts.SyntaxKind.MinusToken)
+      return false;
+    const amount = integerLiteral(e.right);
+    return amount !== null && amount >= 1 && this.isLength(e.left, text);
+  }
+
+  private isIndex(node: ts.Expression, index: ts.Symbol): boolean {
+    const e = peel(node);
+    return ts.isIdentifier(e) && this.symbolAt(e) === index;
+  }
+
+  /** Does `cond` evaluating to `truthy` establish the bound? The index is
+   * an integer and lengths are numbers, so a false comparison is its
+   * negation. */
+  private holds(
+    node: ts.Expression,
+    truthy: boolean,
+    bound: Bound,
+    index: ts.Symbol,
+    text: ts.Symbol,
+  ): boolean {
+    const e = peel(node);
+    if (ts.isPrefixUnaryExpression(e) && e.operator === ts.SyntaxKind.ExclamationToken)
+      return this.holds(e.operand, !truthy, bound, index, text);
+    if (!ts.isBinaryExpression(e)) return false;
+    let op: ts.SyntaxKind = e.operatorToken.kind;
+    if (op === ts.SyntaxKind.AmpersandAmpersandToken || op === ts.SyntaxKind.BarBarToken) {
+      const conjunction = op === ts.SyntaxKind.AmpersandAmpersandToken;
+      if (conjunction !== truthy) return false;
+      return (
+        this.holds(e.left, truthy, bound, index, text) ||
+        this.holds(e.right, truthy, bound, index, text)
+      );
+    }
+    let left = e.left,
+      right = e.right;
+    // Normalize to `index OP other`.
+    if (!this.isIndex(left, index)) {
+      if (!this.isIndex(right, index)) return false;
+      [left, right] = [right, left];
+      op =
+        op === ts.SyntaxKind.LessThanToken
+          ? ts.SyntaxKind.GreaterThanToken
+          : op === ts.SyntaxKind.GreaterThanToken
+            ? ts.SyntaxKind.LessThanToken
+            : op === ts.SyntaxKind.LessThanEqualsToken
+              ? ts.SyntaxKind.GreaterThanEqualsToken
+              : op === ts.SyntaxKind.GreaterThanEqualsToken
+                ? ts.SyntaxKind.LessThanEqualsToken
+                : op;
+    }
+    if (!truthy) {
+      op =
+        op === ts.SyntaxKind.LessThanToken
+          ? ts.SyntaxKind.GreaterThanEqualsToken
+          : op === ts.SyntaxKind.GreaterThanEqualsToken
+            ? ts.SyntaxKind.LessThanToken
+            : op === ts.SyntaxKind.GreaterThanToken
+              ? ts.SyntaxKind.LessThanEqualsToken
+              : op === ts.SyntaxKind.LessThanEqualsToken
+                ? ts.SyntaxKind.GreaterThanToken
+                : ts.SyntaxKind.Unknown;
+    }
+    if (bound === "upper")
+      return (
+        (op === ts.SyntaxKind.LessThanToken && this.isLength(right, text)) ||
+        (op === ts.SyntaxKind.LessThanEqualsToken && this.isLengthMinusOne(right, text))
+      );
+    const limit = integerLiteral(right);
+    if (limit === null) return false;
+    return (
+      (op === ts.SyntaxKind.GreaterThanEqualsToken && limit >= 0) ||
+      (op === ts.SyntaxKind.GreaterThanToken && limit >= -1)
+    );
+  }
+
+  /** Find a guard establishing `bound` that still holds at `read`. */
+  private guarded(
+    read: ts.Node,
+    bound: Bound,
+    index: ts.Symbol,
+    text: ts.Symbol,
+    symbols: readonly ts.Symbol[],
+  ): boolean {
+    const loops: ts.Node[] = [];
+    const end = read.pos;
+    const valid = (ranges: readonly (readonly [number, number])[]): boolean => {
+      for (const symbol of symbols) {
+        for (const write of this.binding(symbol)!.writes) {
+          if (ranges.some(([from, to]) => write.at >= from && write.at < to)) return false;
+          if (loops.some((loop) => write.at >= loop.pos && write.at < loop.end)) return false;
+        }
+      }
+      return true;
+    };
+    const holds = (cond: ts.Expression, truthy: boolean): boolean =>
+      this.holds(cond, truthy, bound, index, text);
+    let child: ts.Node = read;
+    for (let node = read.parent; node && !isBoundary(node); child = node, node = node.parent) {
+      if (ts.isBinaryExpression(node) && node.right === child) {
+        const op = node.operatorToken.kind;
+        if (
+          (op === ts.SyntaxKind.AmpersandAmpersandToken && holds(node.left, true)) ||
+          (op === ts.SyntaxKind.BarBarToken && holds(node.left, false))
+        ) {
+          if (valid([[node.left.pos, end]])) return true;
+        }
+      } else if (ts.isConditionalExpression(node)) {
+        if (node.whenTrue === child && holds(node.condition, true)) {
+          if (valid([[node.condition.pos, end]])) return true;
+        } else if (node.whenFalse === child && holds(node.condition, false)) {
+          if (
+            valid([
+              [node.condition.pos, node.condition.end],
+              [node.whenFalse.pos, end],
+            ])
+          )
+            return true;
+        }
+      } else if (ts.isIfStatement(node)) {
+        if (node.thenStatement === child && holds(node.expression, true)) {
+          if (valid([[node.expression.pos, end]])) return true;
+        } else if (node.elseStatement === child && holds(node.expression, false)) {
+          if (
+            valid([
+              [node.expression.pos, node.expression.end],
+              [node.elseStatement.pos, end],
+            ])
+          )
+            return true;
+        }
+      } else if (ts.isWhileStatement(node)) {
+        if (node.statement === child && holds(node.expression, true)) {
+          if (valid([[node.expression.pos, end]])) return true;
+        }
+      } else if (ts.isForStatement(node)) {
+        // The update runs before the condition is tested again.
+        if (node.statement === child && node.condition && holds(node.condition, true)) {
+          if (
+            valid([
+              [node.condition.pos, node.condition.end],
+              [node.statement.pos, end],
+            ])
+          )
+            return true;
+        }
+      } else if (ts.isBlock(node) || ts.isCaseClause(node) || ts.isDefaultClause(node)) {
+        const statements = node.statements;
+        for (let i = statements.indexOf(child as ts.Statement) - 1; i >= 0; i--) {
+          const statement = statements[i]!;
+          if (
+            ts.isIfStatement(statement) &&
+            !statement.elseStatement &&
+            exits(statement.thenStatement) &&
+            holds(statement.expression, false) &&
+            valid([
+              [statement.expression.pos, statement.expression.end],
+              [statement.end, end],
+            ])
+          )
+            return true;
+        }
+      }
+      if (isLoop(node)) loops.push(node);
+    }
+    return false;
+  }
+}
+
+/** A string element in a write position (assignment, update, or a
+ * destructuring/loop target), never a plain read. */
+function writeOfElement(read: ts.ElementAccessExpression): boolean {
+  let n: ts.Node = read;
+  for (;;) {
+    const p: ts.Node | undefined = n.parent;
+    if (!p) return false;
+    if (ts.isBinaryExpression(p))
+      return (
+        p.left === n &&
+        p.operatorToken.kind >= ts.SyntaxKind.FirstAssignment &&
+        p.operatorToken.kind <= ts.SyntaxKind.LastAssignment
+      );
+    if (ts.isPostfixUnaryExpression(p) || ts.isPrefixUnaryExpression(p))
+      return (
+        p.operator === ts.SyntaxKind.PlusPlusToken || p.operator === ts.SyntaxKind.MinusMinusToken
+      );
+    if (ts.isForOfStatement(p) || ts.isForInStatement(p)) return p.initializer === n;
+    if (
+      ts.isParenthesizedExpression(p) ||
+      ts.isArrayLiteralExpression(p) ||
+      ts.isSpreadElement(p) ||
+      ts.isSpreadAssignment(p) ||
+      ts.isObjectLiteralExpression(p) ||
+      (ts.isPropertyAssignment(p) && p.initializer === n)
+    ) {
+      n = p;
+      continue;
+    }
+    return false;
+  }
+}
diff --git a/packages/compiler/test/ts7/baselines/order-parity.json b/packages/compiler/test/ts7/baselines/order-parity.json
index cd5b15ebc..5b145f136 100644
--- a/packages/compiler/test/ts7/baselines/order-parity.json
+++ b/packages/compiler/test/ts7/baselines/order-parity.json
@@ -15126,6 +15126,18 @@
     "<repo>/tests/corpus/timers-clear-many.ts"
    ],
    "diags": []
+  },
+  "<repo>/tests/corpus/4080-string-index-bounds.ts": {
+   "order": [
+    "<repo>/tests/corpus/4080-string-index-bounds.ts"
+   ],
+   "diags": []
+  },
+  "<repo>/tests/corpus/4081-string-index-unproven.ts": {
+   "order": [
+    "<repo>/tests/corpus/4081-string-index-unproven.ts"
+   ],
+   "diags": []
   }
  }
 }
diff --git a/tests/corpus/4080-string-index-bounds.ts b/tests/corpus/4080-string-index-bounds.ts
new file mode 100644
index 000000000..3e93337d4
--- /dev/null
+++ b/tests/corpus/4080-string-index-bounds.ts
@@ -0,0 +1,111 @@
+// String element reads whose index is proven inside the string: counted
+// loops in both directions, scanner loops guarded by `i < text.length`,
+// early exits, length aliases, and helpers that take one character.
+function isDigit(ch: string): boolean {
+  return ch >= "0" && ch <= "9";
+}
+function isLetter(ch: string): boolean {
+  return (ch >= "a" && ch <= "z") || (ch >= "A" && ch <= "Z");
+}
+
+function tokens(text: string): string[] {
+  const out: string[] = [];
+  let i = 0;
+  while (i < text.length) {
+    const ch = text[i];
+    if (ch === " ") {
+      i++;
+      continue;
+    }
+    const start = i;
+    if (isDigit(ch)) {
+      while (i < text.length && isDigit(text[i])) i++;
+      out.push(`num:${text.slice(start, i)}`);
+    } else if (isLetter(ch)) {
+      while (i < text.length && (isLetter(text[i]) || isDigit(text[i]))) i++;
+      out.push(`word:${text.slice(start, i)}`);
+    } else {
+      out.push(`sym:${ch}`);
+      i++;
+    }
+  }
+  return out;
+}
+
+function reversed(text: string): string {
+  let out = "";
+  for (let i = text.length - 1; i >= 0; i--) out += text[i];
+  return out;
+}
+
+function everyOther(text: string): string {
+  let out = "";
+  for (let i = 0; i <= text.length - 1; i += 2) out += text[i];
+  return out;
+}
+
+function firstNonSpace(text: string): string {
+  let i = 0;
+  while (true) {
+    if (i >= text.length) return "(none)";
+    if (text[i] !== " ") return text[i];
+    i++;
+  }
+}
+
+function countOf(text: string, wanted: string): number {
+  const n = text.length;
+  let count = 0;
+  for (let i = 0; i < n; i++) if (text[i] === wanted) count++;
+  return count;
+}
+
+function trimRight(text: string): string {
+  let end = text.length - 1;
+  while (end >= 0 && text[end] === " ") end--;
+  return text.slice(0, end + 1);
+}
+
+function middle(text: string): string {
+  const i = 1;
+  return i < text.length ? text[i] : "-";
+}
+
+function digitsInLines(lines: string[]): number[] {
+  const counts: number[] = [];
+  for (let r = 0; r < lines.length; r++) {
+    const line = lines[r]!;
+    let n = 0;
+    for (let i = 0; i < line.length; i++) if (isDigit(line[i])) n++;
+    counts.push(n);
+  }
+  return counts;
+}
+
+function codes(text: string): number[] {
+  const out: number[] = [];
+  const read = (): void => {
+    for (let i = 0; i < text.length; i++) out.push(text[i].charCodeAt(0));
+  };
+  read();
+  return out;
+}
+
+console.log(tokens("width 42 + height7 * (3)").join(" | "));
+console.log(tokens("").length, tokens("   ").length, tokens("x").join(""));
+console.log(
+  reversed("stone"),
+  JSON.stringify(reversed("")),
+  everyOther("abcdefg"),
+  everyOther(""),
+);
+console.log(firstNonSpace("   q"), firstNonSpace("    "), firstNonSpace(""));
+console.log(countOf("banana", "a"), countOf("", "a"), countOf("€uro€", "€"));
+console.log(
+  JSON.stringify(trimRight("pad   ")),
+  JSON.stringify(trimRight("   ")),
+  JSON.stringify(trimRight("")),
+);
+console.log(middle("ok"), middle("o"), middle(""));
+console.log(digitsInLines(["a1", "22b", "", "x"]).join(","));
+console.log(codes("A€z").join(","));
diff --git a/tests/corpus/4081-string-index-unproven.ts b/tests/corpus/4081-string-index-unproven.ts
new file mode 100644
index 000000000..90e6aca7e
--- /dev/null
+++ b/tests/corpus/4081-string-index-unproven.ts
@@ -0,0 +1,127 @@
+// String element reads that may fall outside the string still produce
+// undefined: writes between a guard and the read, writes from closures,
+// fractional, negative and inclusive bounds, and guards on another string.
+function show(label: string, value: string | undefined): void {
+  console.log(label, value === undefined ? "undefined" : JSON.stringify(value));
+}
+
+const word = "kite";
+
+{
+  let i = 3;
+  if (i < word.length) {
+    i++;
+    show("bumped", word[i]);
+  }
+}
+
+{
+  let i = 0;
+  if (i < word.length) {
+    for (let k = 0; k < 6; k++) {
+      show("inner", word[i]);
+      i++;
+    }
+  }
+}
+
+{
+  let text = "abcdef";
+  const i = 4;
+  if (i < text.length) {
+    text = "ab";
+    show("shrunk", text[i]);
+  }
+}
+
+{
+  let text = "abc";
+  const shorten = (): void => {
+    text = "a";
+  };
+  for (let i = 0; i < text.length; i++) {
+    shorten();
+    show("closure-text", text[i]);
+  }
+}
+
+{
+  let i = 0;
+  const jump = (): void => {
+    i += 3;
+  };
+  while (i < word.length) {
+    jump();
+    show("closure-index", word[i]);
+  }
+}
+
+{
+  const half = 0.5;
+  if (half < word.length) show("half", word[half]);
+  const before = -1;
+  if (before < word.length) show("negative", word[before]);
+  let down = 0;
+  down = down - 1;
+  if (down < word.length) show("minus", word[down]);
+}
+
+{
+  const text = "abc";
+  for (let i = 0; i <= text.length; i++) show("inclusive", text[i]);
+}
+
+{
+  const long = "longer text";
+  const short = "s";
+  for (let i = 0; i < long.length; i++) if (i > 8) show("other", short[i]);
+}
+
+{
+  const text = "abcd";
+  for (let i = 0; i < text.length; i++) {
+    show("ahead", text[i + 1]);
+    i++;
+    show("stepped", text[i]);
+  }
+}
+
+{
+  const text = "pq";
+  let i = 0;
+  let rest = 0;
+  if (i < text.length) {
+    [i, rest] = [7, 1];
+    show("destructured", text[i]);
+  }
+  console.log("rest", rest);
+}
+
+function at(text: string, index: number): string | undefined {
+  return index < text.length ? text[index] : "-";
+}
+show("param-frac", at("abc", 1.5));
+show("param-neg", at("abc", -2));
+show("param-ok", at("abc", 2));
+
+function afterLoop(text: string): string | undefined {
+  let i = 0;
+  do {
+    i++;
+  } while (i < text.length);
+  return text[i];
+}
+show("after-loop", afterLoop("xyz"));
+
+let shared = 0;
+function advance(): void {
+  shared += 10;
+}
+function readShared(text: string): string | undefined {
+  if (shared < text.length) {
+    advance();
+    return text[shared];
+  }
+  return "-";
+}
+show("module-index", readShared("abc"));