Skip to content

[TS] Support array growth and sparse slots #388

Description

@CaelmBleidd

Current delivery (2026-10-17)

Partially implemented in an open PR; the full issue remains open. #573 at 643378c35a6cc8000cd7cd0942bc986269f2a45e is published, not merged, and all 7 CI checks are green. Its declared stack prerequisites are #567 and #560.

The published change supports bounded non-dense indexed writes when own-slot provenance is known, including allocated arrays and dense inputs projected from PBT ArrayDomain. It extends length to max(oldLength, index + 1), leaves intervening holes absent, preserves values deleted by shrinking, and invalidates the dense-shape proof after sparse growth. The original fixed PGOrbit cache-write input reaches a terminal state past that write and agrees with native execution; this is a fixed-input result, not whole-class coverage evidence.

Remaining acceptance is substantial:

  • Direct array.length = largerLength growth still reports ARRAY_LENGTH_GROWTH; the full symbolic resize/shrink-regrow contract is not delivered by indexed growth alone.
  • General array membership with in, unproven own slots, capacity limits, and the remaining sparse-operation/value-domain/alias cases retain their explicit boundaries.
  • Sparse witness transport/reconstruction is not complete. The legacy returned sparse-array fixture still raises TsUnsupportedWitnessException at hole slot 3; no dense witness schema was broadened and holes were not filled with ordinary undefined values. Scalar reads/length and native own-slot presence are separate validated observations.

#608 only retains unknown-call failure diagnostics; it does not implement growth or sparse transport. Preserve every original acceptance item below and do not close #388 solely for #573. The older pilot observation below describes the pre-#573 stop, not the current published indexed-write behavior.

Original report and acceptance (retained verbatim)

Two-phase PBT pilot priority (2026-10-16)

The fixed-input PGOrbit investigation stops at iotaCache[n] = c when a write to an empty cache requires sparse indexed growth. Native TypeScript completes that case. This is a concrete consumer for the existing sparse-growth scope below. #555 separately preserves the runtime limitation diagnostic; it must not be mistaken for implementing growth. The two-phase roadmap is #345.

Current state (2026-10-14)

Audited against usvm main at 19866c959d.

Known sparse-slot presence, indexed append and sparse-aware source reverse/unshift are implemented (#450/#477). Direct array.length growth remains explicitly unsupported; WriteField still reports ARRAY_LENGTH_GROWTH.

Remaining acceptance boundary

Complete direct symbolic length growth and non-dense indexed growth, shrink-then-grow deletion semantics and reconstruction for all specified value domains/aliases. Preserve presence across every supported operation; do not close the full issue for dense append or selected sparse models.

Original report and acceptance context, retained for traceability

Goal

Support growth of ordinary TypeScript arrays through array.length = n and writes beyond the current last element, with correct sparse-slot (hole) semantics.

Follow-up to #366 / PR #380. Existing push and unshift approximations already grow arrays; this issue covers direct length and indexed writes.

Current limitation

At PR #380 head 41961f7b, length assignment restricts the new length to the current length. Indexed writes also require an existing index.

Simply removing these bounds is incorrect: shrinking currently changes the length without removing the old payloads from symbolic memory. Growing again could expose deleted values. Numeric and Boolean storage also cannot represent a hole by writing their default value.

const values = [10, 20];
values.length = 1;
values.length = 2;

values[1] === undefined; // true; the old 20 must not reappear
1 in values;            // false

A hole must remain distinct from an existing element whose value is undefined:

const values: any[] = [];
values.length = 3;
values[2] = undefined;

0 in values; // false
2 in values; // true

Scope

  • Support nonnegative integral numeric length assignments within the configured maxArraySize, including symbolic lengths.
  • Shrinking deletes elements at and beyond the new length. Growing creates holes without reviving deleted payloads.
  • Support dense append via array[array.length] = value and writes to larger valid indices. Set the new length to max(oldLength, index + 1); intervening indices remain holes.
  • Reading a hole yields undefined for ordinary arrays in the supported domain, including arrays stored as number[] or boolean[].
  • Distinguish holes from explicit undefined for array-index membership with in. The current symbolic-Boolean approximation of in cannot establish this behavior.
  • Preserve hole information across aliases, repeated resizing, and existing supported array operations such as push, pop, shift, unshift, slice, concat, reverse, and fill. Audit other array approximations that read or copy elements; unsupported sparse cases must be handled explicitly.
  • Extend test-value reconstruction and JavaScript replay so holes are not materialized as ordinary undefined elements and mutations do not corrupt reconstructed input arrays.

Implementation direction

Prefer a TS-layer representation of element presence using the existing symbolic-memory regions, for example a Boolean region indexed by array reference and element index. Reads, writes, deletion, and array copying must agree on that representation.

Retain the storage-type normalization from #377 and the unresolved-value payload/kind representation. Current symbolic memory remains authoritative; allocation history is reconstruction metadata.

Dense append can be the first implementation step, but it alone does not complete this issue. Avoid a generic sparse-container framework or unrelated core redesign.

Acceptance criteria

  • Fresh growth, shrink-then-grow, repeated resize, dense append, and writes leaving gaps agree with native JavaScript.
  • Deleted values and reference aliases never reappear after growth.
  • Holes read as undefined, while in distinguishes holes from explicit undefined elements.
  • Cases cover concrete and symbolic lengths/indices, numeric and Boolean arrays, reference arrays, any[]/unknown[], and widened/wrapped aliases.
  • Affected array operations preserve their observable sparse-array behavior; regressions include pop on a trailing hole and shift with holes.
  • Generated inputs, return values, and before/after heap states replay correctly in JavaScript without filling holes accidentally.
  • Existing array/model regressions, TypeScript checks, and Detekt pass.

Boundaries

Keep existing numeric-length validation and explicit size bounds. Full coercion of nonnumeric lengths, exotic arrays, proxies, inherited indexed properties, and complete ECMAScript array semantics are outside this issue. Unsupported behavior must not silently be reported as a successful exact model result.

Activity

  1. CaelmBleidd commented on Oct 16, 2026

    @CaelmBleidd
    MemberAuthor

    Implemented the bounded indexed-growth slice in #573, with #567 guarding unrepresentable current array observations and #560 retaining runtime limitation diagnostics. The full issue remains open.

    The growth change uses existing own-slot presence, supports bounded non-dense numeric index writes, preserves gaps and deletion after shrinking, and revokes dense-shape proof. Unknown-provenance and over-capacity paths remain explicit limitations. PBT array inputs now register the own slots already guaranteed by ArrayDomain; candidate replay retains their original dense values.

    Local validation: 150 focused TS/PBT/DSL/Calls tests passed, followed by clean Detekt checks. The frozen PGOrbit input [8,2,0,2,0,0,0,0] now passes iotaCache[n] = c and reaches one terminal result true, with native TypeScript SUCCESS and no runtime limitation, unsupported call, engine failure or timeout. The input and original TS sources are unchanged. This is a fixed-input preflight, not a comparative coverage result.

    Still open: direct array.length growth; complete array-index membership semantics; sparse-aware transport and witness reconstruction; exact boxed output values currently rejected by the guard; unsupported own-slot provenance and the remaining operation/domain boundaries. #573 targets #567 and includes #560 as an explicit prerequisite for compatible diagnostic regressions. No merge has been performed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions