Skip to content

[TS] Support bounded sparse indexed writes with known own slots - #573

Open
CaelmBleidd wants to merge 5 commits into
caelmbleidd/ts-sparse-witness-guard-388from
caelmbleidd/ts-sparse-index-growth-388
Open

CaelmBleidd wants to merge 5 commits into
caelmbleidd/ts-sparse-witness-guard-388from
caelmbleidd/ts-sparse-index-growth-388

Conversation

@CaelmBleidd

@CaelmBleidd CaelmBleidd commented Oct 16, 2026 •

Copy link
Copy Markdown
Member

An indexed cache write such as iotaCache[2] = value into an empty array stopped the PGOrbit identity scenario at ARRAY_INDEX_GROWTH. Support non-dense indexed writes within maxArraySize when the engine already knows own-slot provenance: extend length to max(oldLength, index + 1), retain absent gaps and do not revive values deleted by shrinking.

Reuse existing presence and typed-value storage. Sparse growth revokes the existing dense-shape proof so a later shrink cannot silently re-enable dense-only models. Register the density already guaranteed by PBT ArrayDomain inputs through the existing presence helper. Capacity and unknown-provenance paths retain explicit limitations. The diagnostic regressions from #560 now exercise the remaining capacity boundary, and a separate DSL regression checks that the small sparse cache case succeeds.

Validation: 150 focused tests passed across TS array/models, PBT projection/search, DSL/native replay and Calls guard/registry/harness. Source-level coverage includes number/boolean/reference/unresolved/widened arrays, symbolic gap indices, shrink/regrow, array moves and fill. Removing only dense-proof invalidation makes its source regression fail. PBT candidate replay preserves the original dense input before mutation. TS/PBT/Calls Detekt main/test, FastCheck Detekt test and diff checks pass.

A one-shot preflight on the frozen original PGOrbit input [8,2,0,2,0,0,0,0] now reaches one terminal state past the cache write with no runtime limitations, unsupported calls, engine failures or timeout; native TypeScript accepts the same fixed property input. This is a fixed-input check, not a coverage benchmark.

Depends on #567 and #560. This PR targets #567; #560 is included as an exact prerequisite merge so its diagnostic fixtures remain compatible. The indexed-growth change is its final dedicated commit. Refs #388; the full issue remains open for direct length growth, array membership, unproven own slots, sparse transport and remaining exact output reconstruction.

CI regression follow-up: two legacy expectations still required all indexed growth to stop. They now verify the intended supported boundary: the existing element remains 22, and allocated sparse expansion reaches one terminal state with length 6, preserved values and undefined hole reads. Native replay checks that indices 3 and 4 remain absent own slots. Materializing the original sparse array still throws TsUnsupportedWitnessException at slot 3; the dense witness schema is not broadened or silently filled. Fractional, negative, and chained named-property writes retain their explicit unsupported assertions. The reported two failures were reproduced on 37a65d48b16f before editing; all 25 focused tests and DetektTest pass after the correction.

@Test
fun `supported counterexample and its native replay survive an excluded path`() {
val program = defineProperty(id = "runtime.mixed-counterexample") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
@Test
fun `supported counterexample and its native replay survive an excluded path`() {
val program = defineProperty(id = "runtime.mixed-counterexample") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
@Test
fun `supported counterexample and its native replay survive an excluded path`() {
val program = defineProperty(id = "runtime.mixed-counterexample") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
@Test
fun `supported counterexample and its native replay survive an excluded path`() {
val program = defineProperty(id = "runtime.mixed-counterexample") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
@Test
fun `supported counterexample and its native replay survive an excluded path`() {
val program = defineProperty(id = "runtime.mixed-counterexample") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
@Test
fun `supported successful paths do not hide excluded model paths`() {
val program = defineProperty(id = "runtime.mixed-no-violation") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
@Test
fun `supported successful paths do not hide excluded model paths`() {
val program = defineProperty(id = "runtime.mixed-no-violation") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
@Test
fun `supported successful paths do not hide excluded model paths`() {
val program = defineProperty(id = "runtime.mixed-no-violation") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
@Test
fun `supported successful paths do not hide excluded model paths`() {
val program = defineProperty(id = "runtime.mixed-no-violation") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
@Test
fun `supported successful paths do not hide excluded model paths`() {
val program = defineProperty(id = "runtime.mixed-no-violation") {
val write = function<(Double) -> Double>(module = "runtime-limitations.ts", exportName = "supportedOrSparse")
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants