Skip to content

Execute JavaScript builtins with symbolic strings and arrays - #391

Draft
CaelmBleidd wants to merge 33 commits into
mainfrom
caelmbleidd/stdlib-source-models
Draft

CaelmBleidd wants to merge 33 commits into
mainfrom
caelmbleidd/stdlib-source-models

Conversation

@CaelmBleidd

@CaelmBleidd CaelmBleidd commented Sep 20, 2026

Copy link
Copy Markdown
Member

JavaScript library functions can now accept symbolic strings and dense arrays in the Calls runner and execute supported standard-library operations through a selectable model catalog. Array, String, Date and Error algorithms are TypeScript bodies interpreted as EtsIR; Kotlin supplies heap, type, UTF-16 and floating-point primitives.

  • Add bounded Array allocation, mutation and copying; String searches, slicing, trimming and literal replaceAll; Error construction; numeric predicates and Date/calendar models.
  • Preserve JavaScript runtime kinds across erased TypeScript assertions, mixed-value comparisons, array reads and typed writes. Check builtin provenance and retain unsupported argument domains as residual calls. Keep Error storage separate from ordinary user fields.
  • Bind exported callable inputs, including supported builtin captures; preflight reachable source/IR and module initializers; count completed-return targets only after evaluating the return expression.
  • Extract original inputs before mutation and replay reached witnesses against pinned original JavaScript. Record model dispatch, residual fallback and runtime limitations separately, including events from externally interrupted searches.

Validation: the combined TS, Calls and FastCheck gate passed with 1,157 tests passing, 143 skipped and no failures before the final narrow guard/storage refinements. Those refinements passed focused tests and independent probes; all seven CI checks passed at 1ec9cd9b. Independent literal replaceAll checks matched native JavaScript in 23,859 cases.

The unchanged 186-target development repeat at 1ec9cd9b produced 61 reached witnesses, all native-confirmed, with no rejected witnesses or tool errors; 58 targets were rejected by readiness, 30 were unreached and 37 hit the external analysis deadline. Compared with the preceding development revision, nine targets gained confirmation and four lost it. The original diagnostic and every earlier result remain preserved. The historical 32-cell mechanics repeat still has eight old ENTRY-origin mapping refusals; completed-return targets are measured separately.

A held-out comparison froze the implementation, frontend, catalog, admission rules, source revisions, targets and input domains before any held-out outcome. It scheduled 66 completed-return targets from 56 functions in five projects: four profiles, seeds 17 and 29, 30 seconds of symbolic analysis per target/profile/seed, Z3, two workers, and mandatory native replay. Startup and replay have separate recorded deadlines. All 528 scheduled cells are accounted for.

Profile Scheduled Native confirmed Rejected witness Tool error External analysis timeout
EMPTY_STOP 132 66 0 0 0
EMPTY_FRESH 132 88 4 14 6
FROZEN_STOP 132 77 0 0 17
FROZEN_FRESH 132 79 2 8 21

EMPTY_STOP, EMPTY_FRESH and FROZEN_STOP are primary profiles; FROZEN_FRESH is an ablation. Only native-confirmed outcomes count as success. An external timeout is an unknown analysis result; an unreached result is not a proof of source-level unreachability.

Paired outcomes: FROZEN_STOP gained 14 confirmed cells and lost 3 versus EMPTY_STOP; it gained 4 and lost 15 versus EMPTY_FRESH. Thus this version improves over EMPTY_STOP but does not show an overall search-success gain over EMPTY_FRESH at 30 seconds. On string-ts, FROZEN_STOP had eight analysis timeouts and two unreached outcomes across ten cells; EMPTY_FRESH confirmed all ten.

The outer held-out support denominator is 5,177 distinct exported functions across eight projects. Uniform static selection retained 192 functions/208 targets; engine admission retained 56 functions/66 targets in five projects. Excluded functions and the three empty projects remain in the outer ledger once, rather than being multiplied by profiles. The original 16 projects were used only for development.

New Error and Array families have actual model dispatch plus native-confirmed development witnesses. Two fixed-input executions of pinned original wrapAnsi.ts matched native JavaScript and exercised replaceAll, while both full-domain 30-second searches timed out; the controls do not count as search successes.

Bounds remain explicit: input strings and dense arrays have lengths 0–10; source Array models have capacity 16. Regex/callback replacement, dynamic coercions, arbitrary object/callback inputs, sparse-array property presence, host effects and unsupported imports remain outside the implemented domains. Standard builtins are not monkey-patched; Date local operations use UTC and clock-dependent operations require a fixed clock. This remains a draft and does not claim complete JavaScript support.

@CaelmBleidd CaelmBleidd changed the title Model Date, Array, String and numeric JavaScript builtins Execute JavaScript builtins with symbolic strings and arrays Sep 20, 2026
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.

1 participant