Prove int32 array candidates in one analysis that revises dropped ones (#2196)

packages/compiler/src/backend/llvm/emitter.ts

@@ -17,6 +17,7 @@ import {
 import { youngNurseryRequested } from "../young-nursery.js";
 import { llvmBytes as llBytes, wtf8Bytes } from "../literals.js";
 import { InternalCompilerError } from "../../errors.js";
+import { serializeModuleParts } from "../../ir/serialize.js";
 import { createHash } from "node:crypto";
 import {
   endsWithJump,
@@ -88,6 +89,8 @@ import {
   fillAllocationLength,
   int32ArrayKey,
   selectInt32Arrays,
+  type Int32ArrayProof,
+  type Int32ArrayRevision,
 } from "../../ir/int32-arrays.js";
 import { everyExpr, everyExprChild, everyStmtChild, everyStmtList } from "../../ir/traverse.js";
 import {
@@ -103,6 +106,7 @@ import { resolveSelfCaptures } from "../../ir/self-captures.js";
 import {
   analyzeInt32Slots,
   dynamicFieldStores,
+  Int32RevisionConflict,
   type DynamicFieldStores,
   Int32Slots,
 } from "../../ir/int32-slots.js";
@@ -554,15 +558,60 @@ export interface Int32SlotAnalysis {
   readonly slots: Int32Slots;
 }
 
-/** The int32 slot analysis of `mod`, with the inputs LlEmitter gives it. */
-function analyzeModuleInt32Slots(mod: IrModule): Int32SlotAnalysis {
+/** The int32 slot analysis of `mod`, with the inputs LlEmitter gives it.
+ * With `revise`, the analysis revises the functions of candidates that drop
+ * (Int32SlotInputs.revise), and `mod` is the module it started from. */
+function analyzeModuleInt32Slots(
+  mod: IrModule,
+  revise?: (fnName: string, dropped: ReadonlySet<string>) => IrFunction,
+): Int32SlotAnalysis {
   const nodeIndex = new IrNodeIndex(mod);
   const initializerBindings = findInitializerBindings(mod, nodeIndex);
   const dynamicStores = dynamicFieldStores(mod, undefined, undefined, nodeIndex);
-  const slots = analyzeInt32Slots(mod, { dynamicStores, initializerBindings, nodes: nodeIndex });
+  const slots = analyzeInt32Slots(mod, {
+    dynamicStores,
+    initializerBindings,
+    nodes: nodeIndex,
+    ...(revise === undefined ? {} : { revise }),
+  });
   return { mod, nodeIndex, initializerBindings, dynamicStores, slots };
 }
 
+/** The candidates an analysis keeps: int32 arrays and checked ones. */
+function keptInt32Arrays(analysis: Int32SlotAnalysis): ReadonlySet<string> {
+  return new Set([...analysis.slots.int32Arrays, ...analysis.slots.checkedInt32Arrays]);
+}
+
+/** An analysis that revised functions (analyzeModuleInt32Slots' `revise`)
+ * as the analysis of `mod`, the module of the functions it ended with: the
+ * node index of `mod`, and its initializer bindings and dynamic stores,
+ * which must be the ones the analysis read. Null when they differ. */
+function revisedAnalysis(analysis: Int32SlotAnalysis, mod: IrModule): Int32SlotAnalysis | null {
+  const nodeIndex = new IrNodeIndex(mod);
+  const initializerBindings = findInitializerBindings(mod, nodeIndex);
+  const dynamicStores = dynamicFieldStores(mod, undefined, undefined, nodeIndex);
+  const read = analysis.initializerBindings;
+  if (initializerBindings.size !== read.size) return null;
+  for (const [name, globals] of initializerBindings) {
+    const other = read.get(name);
+    if (other?.length !== globals.length || globals.some((g, i) => other[i] !== g)) return null;
+  }
+  const stores = analysis.dynamicStores;
+  if (
+    dynamicStores.all !== stores.all ||
+    dynamicStores.names.size !== stores.names.size ||
+    [...dynamicStores.names].some((name) => !stores.names.has(name))
+  )
+    return null;
+  return {
+    mod,
+    nodeIndex,
+    initializerBindings,
+    dynamicStores,
+    slots: analysis.slots,
+  };
+}
+
 /** The functions whose calls the backend may emit as calls of their
  * result-slot entries (record-results.ts). */
 function resultEntryTargets(mod: IrModule): ReadonlySet<string> {
@@ -577,57 +626,127 @@ function moduleEmitter(input: IrModule, options: LlvmTargetOptions): LlEmitter {
   // Facts are keyed by node identity: emit the same module whether it was
   // lowered in memory or read back from its serialized form.
   const mod = unshareNodes(input);
-  // Each round of selectInt32Arrays analyzes the module it marks; the
-  // emitter of the module it returns reuses that round's analysis.
-  const rounds: { last: Int32SlotAnalysis | null } = { last: null };
-  const proven = (marked: IrModule): ReadonlySet<string> => {
-    const analysis = analyzeModuleInt32Slots(marked);
-    rounds.last = analysis;
-    return new Set([...analysis.slots.int32Arrays, ...analysis.slots.checkedInt32Arrays]);
+  // Each proof selectInt32Arrays asks for analyzes a marked module; the
+  // emitter of the module it returns reuses the last one. A proof that
+  // revised functions analyzed the module of the functions it ended with.
+  const rounds: {
+    last: Int32SlotAnalysis | null;
+    functions: readonly IrFunction[] | null;
+    revising: boolean;
+  } = { last: null, functions: null, revising: true };
+  const proven = (marked: IrModule, revise: Int32ArrayRevision | null): Int32ArrayProof | null => {
+    rounds.functions = null;
+    if (revise === null || !rounds.revising) {
+      rounds.last = analyzeModuleInt32Slots(marked);
+      return { kept: keptInt32Arrays(rounds.last), functions: null };
+    }
+    const latest = new Map<string, IrFunction>();
+    try {
+      rounds.last = analyzeModuleInt32Slots(marked, (fnName, dropped) => {
+        const fn = revise(fnName, dropped);
+        latest.set(fnName, fn);
+        return fn;
+      });
+    } catch (error) {
+      if (!(error instanceof Int32RevisionConflict)) throw error;
+      rounds.last = null;
+      return null;
+    }
+    if (latest.size === 0) return { kept: keptInt32Arrays(rounds.last), functions: null };
+    rounds.functions = marked.functions.map((fn) => latest.get(fn.name) ?? fn);
+    return { kept: keptInt32Arrays(rounds.last), functions: rounds.functions };
   };
   // Keep source storage intact for debugger inspection in dev builds.
-  const emitted =
-    options.debugSources === undefined
-      ? selectInt32Arrays(
-          versionParameters(
-            addRecordResultEntries(
-              scalarizeLiteralResults(
-                scalarizeNumericRecords(
-                  specializeCallbackCalls(
-                    specializeNumericCalls(
-                      pairRowSums(
-                        inlineExpressionFunctions(
-                          foldConstantGlobals(
-                            copyStableCaptures(
-                              resolveSelfCaptures(
-                                hoistFinalFieldReads(
-                                  freezeInitOnlyGlobals(
-                                    holdCharLocalsAsUnits(
-                                      dropUnwrittenPropertyBags(runPairedWhileLoopsAsFor(mod)),
-                                    ),
-                                  ),
-                                ),
-                              ),
+  if (options.debugSources !== undefined) return new LlEmitter(mod, options, null, null);
+  const passed = versionParameters(
+    addRecordResultEntries(
+      scalarizeLiteralResults(
+        scalarizeNumericRecords(
+          specializeCallbackCalls(
+            specializeNumericCalls(
+              pairRowSums(
+                inlineExpressionFunctions(
+                  foldConstantGlobals(
+                    copyStableCaptures(
+                      resolveSelfCaptures(
+                        hoistFinalFieldReads(
+                          freezeInitOnlyGlobals(
+                            holdCharLocalsAsUnits(
+                              dropUnwrittenPropertyBags(runPairedWhileLoopsAsFor(mod)),
                             ),
                           ),
                         ),
                       ),
-                      mangleFunction,
                     ),
-                    mangleFunction,
                   ),
                 ),
               ),
+              mangleFunction,
             ),
+            mangleFunction,
           ),
-          proven,
-          resultEntryTargets,
-        )
-      : mod;
-  const prepared = rounds.last;
+        ),
+      ),
+    ),
+  );
+  let emitted = selectInt32Arrays(passed, proven, resultEntryTargets);
+  let prepared = rounds.last;
+  // A proof that revised functions analyzed the module of the functions it
+  // ended with, which is the selected module unless selection fell back to
+  // rounds: then the selected module was proved by its own round.
+  if (prepared !== null && rounds.functions !== null && prepared.mod !== emitted) {
+    const functions = rounds.functions;
+    prepared =
+      emitted !== passed &&
+      emitted.functions.length === functions.length &&
+      emitted.functions.every((fn, i) => fn === functions[i])
+        ? revisedAnalysis(prepared, emitted)
+        : null;
+    if (prepared === null && emitted !== passed) {
+      rounds.revising = false;
+      emitted = selectInt32Arrays(passed, proven, resultEntryTargets);
+      prepared = rounds.last;
+    }
+  }
+  if (process.env["SCRIPTC_INT32_VERIFY"] === "1")
+    verifyInt32Selection(passed, emitted, prepared?.mod === emitted ? prepared : null);
   return new LlEmitter(emitted, options, null, prepared?.mod === emitted ? prepared : null);
 }
 
+/** SCRIPTC_INT32_VERIFY=1: throws unless the selection with revisions
+ * (`emitted`, and the analysis the emitter takes over) is the one rounds
+ * without revisions give: the same module, and the same facts. */
+function verifyInt32Selection(
+  passed: IrModule,
+  emitted: IrModule,
+  analysis: Int32SlotAnalysis | null,
+): void {
+  let last: Int32SlotAnalysis | null = null;
+  const reference = selectInt32Arrays(
+    passed,
+    (marked) => {
+      last = analyzeModuleInt32Slots(marked);
+      return { kept: keptInt32Arrays(last), functions: null };
+    },
+    resultEntryTargets,
+  );
+  const text = (mod: IrModule): string => serializeModuleParts(mod).join("");
+  if (text(reference) !== text(emitted))
+    throw new InternalCompilerError("int32 selection: the revised module differs from the rounds'");
+  const facts = (mod: IrModule, prepared: Int32SlotAnalysis | null): string =>
+    (prepared?.mod === mod ? prepared : analyzeModuleInt32Slots(mod)).slots.summary(mod);
+  const expected = facts(reference, last);
+  const actual = facts(emitted, analysis);
+  if (expected !== actual) {
+    const want = expected.split("\n");
+    const got = actual.split("\n");
+    const line = want.findIndex((entry, i) => entry !== got[i]);
+    throw new InternalCompilerError(
+      `int32 selection: the revised analysis differs from the rounds': ${want[line]?.slice(0, 400)} != ${got[line]?.slice(0, 400)}`,
+    );
+  }
+}
+
 /** Emits the module's parts, emitting it again with the functions an
  * UnwindAbiViolation names on the pending-flag ABI. */
 function emitModuleText(input: IrModule, options: LlvmTargetOptions): string[] {
@@ -1443,7 +1562,12 @@ export class LlEmitter {
   /** Preorder intervals of the runtime error classes under THIS module's
    * class-forest numbering (main() stamps scr_error_vts with them, exactly
    * like the runtime ABI’s errorVtStampLines). */
-  readonly errorIntervals: { kind: number; pre: number; post: number; lib: string }[] = [];
+  readonly errorIntervals: {
+    kind: number;
+    pre: number;
+    post: number;
+    lib: string;
+  }[] = [];
   /** The runtime emitter vtable's preorder interval, when the program
    * touches node:events (the class def rides the module exactly then) —
    * main() stamps scr_emitter_vt with it (emitterVtStampLines, ported). */
@@ -1452,7 +1576,12 @@ export class LlEmitter {
    * ported): the defs ride every emitter-touching module (the frontend
    * collects the whole emitter-rooted tree), and scr_stream.c links on
    * the same predicate, so the stamps always have their globals. */
-  readonly streamIntervals: { vt: string; pre: number; post: number; lib: string }[] = [];
+  readonly streamIntervals: {
+    vt: string;
+    pre: number;
+    post: number;
+    lib: string;
+  }[] = [];
 
   // ── per-function state (reset in emitFunction) ─────────────────────────
   B = new BlockBuilder();
@@ -1525,7 +1654,12 @@ export class LlEmitter {
   /** Active induction bindings retain their width independently of size_t. */
   integerLoopBindings = new Map<
     string,
-    { slot: string; type: "i32" | "i64"; signed?: boolean; range?: { min: number; max: number } }
+    {
+      slot: string;
+      type: "i32" | "i64";
+      signed?: boolean;
+      range?: { min: number; max: number };
+    }
   >();
   /** Constant number locals whose latest emitted declaration stored an
    * exact integer beside the double, such as `const j = i * 4` in a
@@ -1608,7 +1742,11 @@ export class LlEmitter {
    * (the fast copy) or as double arrays (an ordinary copy entered only
    * after they widened), as `function\0local` keys, and where each of the
    * fast copy's writes resumes in the third copy. */
-  int32Kinds: { int32: Set<string>; wide: Set<string>; resume: Map<IrStmt, string> } | null = null;
+  int32Kinds: {
+    int32: Set<string>;
+    wide: Set<string>;
+    resume: Map<IrStmt, string>;
+  } | null = null;
   /** The resume label of the fast-copy write being emitted. */
   int32KindResume: string | null = null;
   /** The function being emitted, for speculative globals. */
@@ -1682,7 +1820,12 @@ export class LlEmitter {
    * releases frames/scopes down to the recorded depths and branches to
    * `label` (the catch, or the exception-path finally) instead of
    * returning out of the function. Entering a try emits no code. */
-  tryStack: { label: string; used: boolean; frameDepth: number; scopeDepth: number }[] = [];
+  tryStack: {
+    label: string;
+    used: boolean;
+    frameDepth: number;
+    scopeDepth: number;
+  }[] = [];
   /** Return type of the function being emitted — the unwind path returns
    * a dummy of this type (never read: callers check the flag first). */
   currentReturnType: IrType = VOID;
@@ -7198,7 +7341,10 @@ export class LlEmitter {
     return childDataDynThunkFor(this, chunk);
   }
 
-  emitterFixedAdapter(cbT: IrType & { kind: "func" }): { fn: string; shim: string } {
+  emitterFixedAdapter(cbT: IrType & { kind: "func" }): {
+    fn: string;
+    shim: string;
+  } {
     return emitterFixedAdapter(this, cbT);
   }
 

packages/compiler/src/ir/int32-arrays.ts

@@ -805,6 +805,41 @@ function rewriteCandidates(
   return { ...fn, body, locals: locals.filter((local) => !popLocals.has(local.id)) };
 }
 
+/** A module marked for its int32 array candidates: the candidates of
+ * each function (int32ArrayCandidates) and the element readers the marking
+ * inlines. */
+interface Int32ArrayMarking {
+  readonly mod: IrModule;
+  readonly readers: ReadonlyMap<string, IrFunction>;
+  readonly candidates: ReadonlyMap<string, ReadonlySet<string>>;
+}
+
+/** markInt32ArrayCandidates with the candidates it marked; null when it
+ * marks none. */
+function markCandidates(
+  mod: IrModule,
+  keep: ReadonlySet<string> | null,
+  redirected: ReadonlySet<string>,
+): Int32ArrayMarking | null {
+  if (mod.lib !== undefined) return null;
+  const readers = new Map<string, IrFunction>();
+  for (const fn of mod.functions) if (isElementReader(fn)) readers.set(fn.name, fn);
+  const all = moduleInt32ArrayCandidates(mod, new Set(readers.keys()), keep, redirected);
+  if (all.size === 0) return null;
+  const keys = new Set<string>();
+  const functions = mod.functions.map((fn) => {
+    const candidates = all.get(fn.name);
+    if (!candidates) return fn;
+    for (const id of candidates) keys.add(int32ArrayKey(fn.name, id));
+    return rewriteCandidates(fn, candidates, readers);
+  });
+  return {
+    mod: { ...mod, functions, int32ArrayCandidates: [...keys] },
+    readers,
+    candidates: all,
+  };
+}
+
 /** Propose the module's int32 array candidates (int32ArrayKey keys in
  * `int32ArrayCandidates`), only those in `keep` when given, and rewrite
  * their functions. */
@@ -813,42 +848,126 @@ export function markInt32ArrayCandidates(
   keep: ReadonlySet<string> | null = null,
   redirected: ReadonlySet<string> = new Set(),
 ): IrModule {
-  if (mod.lib !== undefined) return mod;
-  const readers = new Map<string, IrFunction>();
-  for (const fn of mod.functions) if (isElementReader(fn)) readers.set(fn.name, fn);
-  const all = moduleInt32ArrayCandidates(mod, new Set(readers.keys()), keep, redirected);
-  if (all.size === 0) return mod;
-  const keys = new Set<string>();
-  const functions = mod.functions.map((fn) => {
-    const candidates = all.get(fn.name);
-    if (!candidates) return fn;
-    for (const id of candidates) keys.add(int32ArrayKey(fn.name, id));
-    return rewriteCandidates(fn, candidates, readers);
-  });
-  return { ...mod, functions, int32ArrayCandidates: [...keys] };
+  return markCandidates(mod, keep, redirected)?.mod ?? mod;
+}
+
+/** Revises a function of a module marked for int32 array candidates when
+ * some of them drop: the function marked for its candidates outside
+ * `dropped` (int32ArrayKey keys), which is the unmarked function when none
+ * is left. */
+export type Int32ArrayRevision = (fnName: string, dropped: ReadonlySet<string>) => IrFunction;
+
+/** What a proof of a marked module (selectInt32Arrays' `prove`) keeps. */
+export interface Int32ArrayProof {
+  /** The candidates it keeps. */
+  readonly kept: ReadonlySet<string>;
+  /** The functions of the module it proved, in module order, when it
+   * revised some through the Int32ArrayRevision it was given; otherwise
+   * null, for the marked module's own. */
+  readonly functions: readonly IrFunction[] | null;
 }
 
 /** The module the backend emits: rewritten for exactly the candidates the
- * int32 slot analysis (`prove`, returning its int32Arrays) keeps, so a
- * module without int32 arrays is `mod` itself. A dropped candidate's
- * rewrite is undone by marking again without it, until every candidate
- * marked is kept. `redirected` names the functions some of whose calls the
+ * int32 slot analysis (`prove`) keeps, so a module without int32 arrays is
+ * `mod` itself. `redirected` names the functions some of whose calls the
  * backend emits as calls of another function (a result-slot entry): their
- * parameters keep doubles. */
+ * parameters keep doubles.
+ *
+ * The proof of the marked module gets an Int32ArrayRevision: as candidates
+ * drop, it revises their functions and goes on proving the revised module,
+ * so one analysis ends with the module marked for the candidates it keeps.
+ * That module is the answer when marking for those candidates again proposes
+ * exactly them, in the functions the proof revised. A proof that cannot
+ * follow a revision answers null; then each round marks the module, proves
+ * it without revisions, and marks again without the dropped candidates,
+ * until a round keeps every candidate it marks (four rounds at most). */
 export function selectInt32Arrays(
   mod: IrModule,
-  prove: (marked: IrModule) => ReadonlySet<string>,
+  prove: (marked: IrModule, revise: Int32ArrayRevision | null) => Int32ArrayProof | null,
   redirected: (mod: IrModule) => ReadonlySet<string> = () => new Set(),
 ): IrModule {
-  let keep: ReadonlySet<string> | null = null;
   const others = redirected(mod);
-  for (let round = 0; round < 4; round++) {
+  const marking = markCandidates(mod, null, others);
+  if (marking === null) return mod;
+  const original = new Map(mod.functions.map((fn) => [fn.name, fn]));
+  const markedFunctions = new Map(marking.mod.functions.map((fn) => [fn.name, fn]));
+  // Each function's latest revision and the candidates it is marked for.
+  const revisions = new Map<string, { fn: IrFunction; ids: ReadonlySet<string> }>();
+  const revise: Int32ArrayRevision = (fnName, dropped) => {
+    const candidates = marking.candidates.get(fnName) ?? new Set<string>();
+    const ids = new Set<string>();
+    for (const id of candidates) if (!dropped.has(int32ArrayKey(fnName, id))) ids.add(id);
+    const latest = revisions.get(fnName);
+    if (latest !== undefined && latest.ids.size === ids.size) return latest.fn;
+    if (latest === undefined && ids.size === candidates.size) return markedFunctions.get(fnName)!;
+    const fn =
+      ids.size === 0
+        ? original.get(fnName)!
+        : rewriteCandidates(original.get(fnName)!, ids, marking.readers);
+    revisions.set(fnName, { fn, ids });
+    return fn;
+  };
+  const proof = prove(marking.mod, revise);
+  const proposed = marking.mod.int32ArrayCandidates ?? [];
+  let keep: ReadonlySet<string> | null = null;
+  let round = 0;
+  if (proof !== null && proof.functions === null) {
+    // The marked module itself was proved: the first round.
+    if (proposed.every((key) => proof.kept.has(key))) return marking.mod;
+    keep = new Set(proposed.filter((key) => proof.kept.has(key)));
+    round = 1;
+  } else if (proof !== null) {
+    const settled = settleRevisions(mod, marking, proof, revisions, others);
+    if (settled !== null) return settled;
+  }
+  for (; round < 4; round++) {
     const marked = markInt32ArrayCandidates(mod, keep, others);
     if (marked === mod) return mod;
-    const kept = prove(marked);
-    const proposed = marked.int32ArrayCandidates ?? [];
-    if (proposed.every((key) => kept.has(key))) return marked;
-    keep = new Set(proposed.filter((key) => kept.has(key)));
+    const kept = prove(marked, null)!.kept;
+    const roundProposed = marked.int32ArrayCandidates ?? [];
+    if (roundProposed.every((key) => kept.has(key))) return marked;
+    keep = new Set(roundProposed.filter((key) => kept.has(key)));
   }
   return mod;
 }
+
+/** The module marked for the candidates a revising proof kept, built from
+ * the functions it proved: null unless marking `mod` for those candidates
+ * proposes, in each function, exactly the candidates its proved function is
+ * marked for. `mod` itself when it proposes none. */
+function settleRevisions(
+  mod: IrModule,
+  marking: Int32ArrayMarking,
+  proof: Int32ArrayProof,
+  revisions: ReadonlyMap<string, { fn: IrFunction; ids: ReadonlySet<string> }>,
+  redirected: ReadonlySet<string>,
+): IrModule | null {
+  const kept = proof.kept;
+  const functions = proof.functions!;
+  if (functions.length !== mod.functions.length) return null;
+  const all = moduleInt32ArrayCandidates(
+    mod,
+    new Set(marking.readers.keys()),
+    new Set([...(marking.mod.int32ArrayCandidates ?? [])].filter((key) => kept.has(key))),
+    redirected,
+  );
+  const keys = new Set<string>();
+  for (let i = 0; i < mod.functions.length; i++) {
+    const fn = mod.functions[i]!;
+    const proved = functions[i]!;
+    const candidates = all.get(fn.name);
+    const revision = revisions.get(fn.name);
+    const marked = revision?.ids ?? marking.candidates.get(fn.name) ?? new Set<string>();
+    if ((candidates?.size ?? 0) !== marked.size) return null;
+    if (candidates !== undefined)
+      for (const id of candidates) {
+        if (!marked.has(id)) return null;
+        keys.add(int32ArrayKey(fn.name, id));
+      }
+    const expected =
+      revision?.fn ?? (marking.candidates.has(fn.name) ? marking.mod.functions[i]! : fn);
+    if (proved !== expected) return null;
+  }
+  if (all.size === 0) return mod;
+  return { ...mod, functions: [...functions], int32ArrayCandidates: [...keys] };
+}

packages/compiler/src/ir/int32-slots.ts

@@ -27,7 +27,7 @@ import {
   int32ArraySlot,
   int32ArrayStores,
 } from "./int32-arrays.js";
-import { everyExprChild, everyStmtChild, everyTypeChild } from "./traverse.js";
+import { everyExprChild, everyStmtChild, everyStmtList, everyTypeChild } from "./traverse.js";
 
 /** The storage slot an array-valued expression reads, as an
  * IrContracts.int32Elements key: a local or parameter
@@ -406,6 +406,47 @@ export class Int32Slots {
     for (const key of data.checkedInt32Arrays) slots.checkedInt32Arrays.add(key);
     return slots;
   }
+
+  /** Every fact, in a canonical order, with each proven write as its
+   * position in `mod` (function index, then walk order): two analyses of
+   * equal modules hold the same facts when their summaries are equal. */
+  summary(mod: IrModule): string {
+    const sorted = (values: Iterable<string>): string => [...values].sort().join(",");
+    const lines = [
+      `fields ${sorted(this.fields)}`,
+      `params ${sorted([...this.paramFacts].flatMap(([fn, params]) => [...params].map(([id, r]) => `${fn}\0${id}=${r.min}:${r.max}`)))}`,
+      `returns ${sorted(this.returns)}`,
+      `returnRanges ${sorted([...this.returnRanges].map(([fn, r]) => `${fn}=${r.min}:${r.max}`))}`,
+      `boxes ${sorted(this.boxes)}`,
+      `boxGroups ${sorted([...this.boxGroupOf].map(([member, group]) => `${member}=${group}`))}`,
+      `called ${sorted(this.called)}`,
+      `pinned ${sorted(this.pinned)}`,
+      `int32Locals ${sorted(this.int32Locals)}`,
+      `int32Elements ${sorted(this.int32Elements)}`,
+      `nonNegative ${sorted(this.nonNegative)}`,
+      `pinViolations ${sorted(this.pinViolations)}`,
+      `narrowedReads ${this.narrowedReads}`,
+      `int32Arrays ${sorted(this.int32Arrays)}`,
+      `checkedInt32Arrays ${sorted(this.checkedInt32Arrays)}`,
+    ];
+    const positions: string[] = [];
+    mod.functions.forEach((fn, f) => {
+      let at = 0;
+      everyStmtList(fn.body, {
+        expr: (e) => {
+          if (this.provenWrites.has(e)) positions.push(`${f}:${at}`);
+          at++;
+          return true;
+        },
+        stmt: () => {
+          at++;
+          return true;
+        },
+      });
+    });
+    lines.push(`provenWrites ${this.provenWrites.size} ${positions.join(",")}`);
+    return lines.join("\n");
+  }
 }
 
 /** Int32Slots as plain data (Int32Slots.encode). */
@@ -909,6 +950,95 @@ export interface Int32SlotInputs {
   initializerBindings?: ReadonlyMap<string, IrGlobal[]>;
   /** The module's node index, read instead of walking the bodies. */
   nodes?: IrNodeIndex;
+  /** Revises a function of a module marked for int32 array candidates when
+   * candidates drop (int32-arrays.ts Int32ArrayRevision): the function
+   * marked without the `dropped` candidates. With it, a candidate that drops
+   * (and keeps no checked stores) takes its sites back to the element-reader
+   * calls the marking inlined, and the fixpoint goes on over the revised
+   * functions, so its result is the analysis of the module marked for the
+   * candidates it keeps. A revision that changes more of a function than
+   * those sites throws Int32RevisionConflict. */
+  revise?: (fnName: string, dropped: ReadonlySet<string>) => IrFunction;
+}
+
+/** A revision (Int32SlotInputs.revise) changed a function in a way the
+ * fixpoint cannot follow: a call of a function no other call reaches, or
+ * any change besides element-reader calls taking the place of their
+ * inlined reads. The module needs an analysis of its own. */
+export class Int32RevisionConflict extends Error {}
+
+/** What the analysis's setup reads from a function body, besides direct
+ * calls: a revision must leave all of it unchanged. */
+function revisionStructure(fn: IrFunction): {
+  calls: { callee: string; args: number }[];
+  rest: string;
+} {
+  const calls: { callee: string; args: number }[] = [];
+  const rest: string[] = [];
+  const boxed = new Set(fn.locals.filter((local) => local.boxed).map((local) => local.id));
+  const expr = (e: IrExpr): boolean => {
+    const referenced = exprFunctionReference(e);
+    if (referenced !== undefined) rest.push(`ref:${referenced}`);
+    switch (e.kind) {
+      case "call":
+        calls.push({ callee: e.callee, args: e.args.length });
+        break;
+      case "new":
+        rest.push(`new:${e.className}:${e.args.length}`);
+        break;
+      case "varRef":
+        if (boxed.has(e.localId)) rest.push(`read:${e.localId}`);
+        break;
+      case "assignExpr":
+      case "incDec":
+        rest.push(`${e.kind}:${e.localId}`);
+        break;
+      case "fieldGet":
+      case "fieldIncDec":
+        rest.push(`${e.kind}:${e.className}\0${e.field}`);
+        break;
+      case "closure":
+        rest.push(`closure:${e.fnName}:${e.captures.join(",")}`);
+        break;
+      case "classRef":
+        rest.push(`classRef:${e.className}:${(e.captures ?? []).join(",")}`);
+        break;
+      case "virtualCall":
+        rest.push(`virtualCall:${e.className}.${e.method}`);
+        break;
+      case "instanceOfValue":
+        rest.push(`instanceOf:${e.classValue.kind}`);
+        break;
+    }
+    if (BOUNDARY_KINDS.has(e.kind)) rest.push(`boundary:${e.kind}`);
+    return everyExprChild(e, expr, stmt);
+  };
+  const stmt = (s: IrStmt): boolean => {
+    switch (s.kind) {
+      case "forOf":
+        rest.push(`forOf:${s.localId}`);
+        break;
+      case "tryCatch":
+        if (s.catchLocalId) rest.push(`catch:${s.catchLocalId}`);
+        break;
+      case "assign":
+      case "varDecl":
+        if (boxed.has(s.localId)) rest.push(`${s.kind}:${s.localId}`);
+        break;
+      case "throw":
+        rest.push("throw");
+        break;
+    }
+    return everyStmtChild(s, expr, stmt);
+  };
+  for (const s of fn.body) stmt(s);
+  rest.sort();
+  for (const local of fn.locals)
+    if (local.boxed || local.tdz)
+      rest.push(`local:${local.id}:${local.boxed === true}:${local.tdz === true}`);
+  for (const capture of fn.captures ?? []) rest.push(`capture:${capture.localId}`);
+  for (const capture of fn.classCaptures ?? []) rest.push(`classCapture:${capture.localId}`);
+  return { calls, rest: rest.join("\n") };
 }
 
 export function analyzeInt32Slots(mod: IrModule, inputs: Int32SlotInputs = {}): Int32Slots {
@@ -1280,6 +1410,36 @@ export function analyzeInt32Slots(mod: IrModule, inputs: Int32SlotInputs = {}):
     });
     return found;
   };
+  // Candidates dropped without checked stores, and the revision of the
+  // functions that hold them (Int32SlotInputs.revise).
+  const dropped = new Set<string>();
+  const revise = (names: ReadonlySet<string>): void => {
+    for (const name of names) {
+      const previous = functions.get(name)!;
+      const next = inputs.revise!(name, dropped);
+      if (next === previous) continue;
+      const before = revisionStructure(previous);
+      const after = revisionStructure(next);
+      if (before.rest !== after.rest) throw new Int32RevisionConflict(name);
+      // The revision adds the element-reader calls back: each must be of a
+      // function other calls already reach, with its arity.
+      const counts = new Map<string, number>();
+      for (const { callee } of before.calls) counts.set(callee, (counts.get(callee) ?? 0) + 1);
+      for (const { callee, args } of after.calls) {
+        const left = counts.get(callee) ?? 0;
+        if (left > 0) {
+          counts.set(callee, left - 1);
+          continue;
+        }
+        const target = functions.get(callee);
+        if (!called.has(callee) || target === undefined || target.params.length !== args)
+          throw new Int32RevisionConflict(name);
+        reads(`ret:${callee}`, name);
+      }
+      for (const left of counts.values()) if (left > 0) throw new Int32RevisionConflict(name);
+      functions.set(name, next);
+    }
+  };
   const provenByFunction = new Map<string, IrExpr[]>();
   // Each function's parameter and result writes under its latest analysis:
   // at the fixpoint, the ranges of every write under the final facts.
@@ -1324,6 +1484,8 @@ export function analyzeInt32Slots(mod: IrModule, inputs: Int32SlotInputs = {}):
       for (const id of globalArrays) both.add(id);
       arrays = both;
     }
+    // Functions whose candidates this visit drops, revised after it.
+    const revised = new Set<string>();
     if (arrays && arrayGroups) {
       const requeue = (name: string): void => {
         if (queued.has(name)) return;
@@ -1358,9 +1520,39 @@ export function analyzeInt32Slots(mod: IrModule, inputs: Int32SlotInputs = {}):
           checkableInt32Allocations(fn, id)
         )
           slots.checkedInt32Arrays.add(key);
-        else for (const member of group) reason(`array:${member}`, "an element store is not int32");
+        else {
+          for (const member of group) reason(`array:${member}`, "an element store is not int32");
+          if (inputs.revise !== undefined) {
+            // The revised module no longer marks the group: its functions
+            // leave the candidate sets the visits below consult.
+            for (const member of group) {
+              dropped.add(member);
+              if (member.startsWith("\0")) {
+                globalArrays.delete(member.slice(1));
+                const names = arrayGroups.globalReaders.get(member);
+                if (names) for (const name of names) revised.add(name);
+              } else {
+                const cut = member.indexOf("\0");
+                const owner = member.slice(0, cut);
+                const ids = arrayCandidates.get(owner);
+                ids?.delete(member.slice(cut + 1));
+                if (ids?.size === 0) arrayCandidates.delete(owner);
+                revised.add(owner);
+              }
+            }
+            globalArrayFunctions.clear();
+            for (const [member, names] of arrayGroups.globalReaders)
+              if (!dropped.has(member)) for (const name of names) globalArrayFunctions.add(name);
+          }
+        }
       }
     }
+    if (revised.size > 0) {
+      revise(revised);
+      // A revised body is analyzed again (it was queued with its readers);
+      // the writes of the body it replaces no longer count.
+      if (functions.get(fn.name) !== fn) continue;
+    }
     // An int32 written into a slot still assumed non-negative: widen the
     // assumption when the value may be negative, and reanalyze its readers.
     const settle = (slot: string, e: IrExpr): void => {

packages/compiler/test/int32-element-array-emission.test.ts

@@ -3,8 +3,10 @@ import { tmpdir } from "node:os";
 import { join } from "node:path";
 import { expect, test } from "vitest";
 import { compile, deserializeModule } from "../src/index.js";
-import type { IrModule } from "../src/ir/ir.js";
+import type { IrFunction, IrModule } from "../src/ir/ir.js";
 import { markInt32ArrayCandidates, selectInt32Arrays } from "../src/ir/int32-arrays.js";
+import { analyzeInt32Slots, type Int32Slots } from "../src/ir/int32-slots.js";
+import { serializeModule } from "../src/ir/serialize.js";
 
 async function emitLlvm(source: string): Promise<string> {
   const dir = await mkdtemp(join(tmpdir(), "scriptc-int32-elements-"));
@@ -210,12 +212,12 @@ test("only the candidates the proof keeps are rewritten", async () => {
   // An array that reaches `join` is never proposed.
   expect(proposed.some((key) => key.startsWith("joined\0"))).toBe(false);
   // Without a kept candidate, the module is the input itself.
-  expect(selectInt32Arrays(mod, () => new Set())).toBe(mod);
+  expect(selectInt32Arrays(mod, () => ({ kept: new Set(), functions: null }))).toBe(mod);
   const kept = new Set(["compose\0p.0", "compose\0q.0"]);
-  const selected = selectInt32Arrays(
-    mod,
-    (marked) => new Set((marked.int32ArrayCandidates ?? []).filter((key) => kept.has(key))),
-  );
+  const selected = selectInt32Arrays(mod, (marked) => ({
+    kept: new Set((marked.int32ArrayCandidates ?? []).filter((key) => kept.has(key))),
+    functions: null,
+  }));
   expect(selected.int32ArrayCandidates).toEqual([...kept]);
   for (const fn of selected.functions)
     if (fn.name !== "compose") expect(fn).toBe(mod.functions.find((f) => f.name === fn.name));
@@ -259,3 +261,47 @@ test("arrays passed to helpers and held in module globals get 4-byte slots", asy
   expect(functions(llvm, "mean")).not.toMatch(/getelementptr inbounds i32, ptr/);
   expect(llvm).toMatch(/@scr_arr_new(_small)?\(i32 7/);
 });
+
+/** The module selectInt32Arrays selects, the analysis of its last proof,
+ * and how many proofs it asked for: with `revising`, each proof revises
+ * the functions of candidates that drop. */
+function selection(
+  mod: IrModule,
+  revising: boolean,
+): { selected: IrModule; slots: Int32Slots; proofs: number } {
+  let slots: Int32Slots | null = null;
+  let proofs = 0;
+  const selected = selectInt32Arrays(mod, (marked, revise) => {
+    proofs++;
+    const latest = new Map<string, IrFunction>();
+    slots = analyzeInt32Slots(
+      marked,
+      revising && revise !== null
+        ? {
+            revise: (fnName, dropped) => {
+              const fn = revise(fnName, dropped);
+              latest.set(fnName, fn);
+              return fn;
+            },
+          }
+        : {},
+    );
+    const kept = new Set([...slots.int32Arrays, ...slots.checkedInt32Arrays]);
+    if (latest.size === 0) return { kept, functions: null };
+    return { kept, functions: marked.functions.map((fn) => latest.get(fn.name) ?? fn) };
+  });
+  return { selected, slots: slots!, proofs };
+}
+
+test("one proof that revises dropped candidates selects what rounds of proofs select", async () => {
+  for (const program of [source, sharedSource]) {
+    const mod = await lowerIr(program);
+    const rounds = selection(mod, false);
+    const revised = selection(mod, true);
+    // The rounds drop a candidate and prove the module again.
+    expect(rounds.proofs).toBeGreaterThan(1);
+    expect(revised.proofs).toBe(1);
+    expect(serializeModule(revised.selected, true)).toBe(serializeModule(rounds.selected, true));
+    expect(revised.slots.summary(revised.selected)).toBe(rounds.slots.summary(rounds.selected));
+  }
+});