Skip to content

[Calls] Preserve reached inputs and measure native class coverage - #479

Open
CaelmBleidd wants to merge 1 commit into
caelmbleidd/pr479-ts-primitive-string-conversionfrom
caelmbleidd/ts-calls-class-measurement
Open

CaelmBleidd wants to merge 1 commit into
caelmbleidd/pr479-ts-primitive-string-conversionfrom
caelmbleidd/ts-calls-class-measurement

Conversation

@CaelmBleidd

@CaelmBleidd CaelmBleidd commented Oct 13, 2026 •

Copy link
Copy Markdown
Member

Calls previously measured members independently and mixed native coverage with symbolic-result agreement. This change measures exact executable original TypeScript statements of one class under a shared 30- or 120-second budget, while retaining inputs when symbolic execution reaches an unsupported call or an execution limit.

The full frozen class surface schedules constructor, every member and all ordered two-member scenarios on one receiver. A single machine retains scenario queues with constant-time fairness, a 250 ms quantum, Yices and class-only symbolic novelty. The original AST denominator stays fixed across profiles and budgets; wrappers, foreign classes, model bodies, type-only declarations and preparation probes stay outside coverage.

Primary coverage now requires complete, agreeing original and independently instrumented native replays with checked target-class statement IDs. Symbolic returned-value/state consistency remains a separate strict diagnostic. A live reproduction of the published baseline on HashMap found 10 completed EMPTY_FRESH candidates and 43/66 matching native statements; the former strict gate reported 0/66 because every symbolic observation disagreed or was incomplete. The sealed v7 campaign retains its historical strict metric and is not reinterpreted or overwritten.

Stopped inputs are opt-in in the shared engine and enabled for class measurement. Feasible unknown-call prefixes are cloned before STOP_PATH pruning; runtime-bound paths and pending queues also emit input-only SUSPENDED candidates. Terminal states remain separate. Queue draining performs no additional interpreter steps or SAT checks, traverses deferred/wrapper queues without scheduling or merging effects, and preserves the original stop reason. Candidate origin participates in deduplication, so a prefix cannot suppress a later terminal observation with the same inputs. In-search inputs use actual emission times; final queue extraction contributes only to the final budget checkpoint. Extraction time, candidate caps and failures remain visible.

The increment also fixes cached conditional models that violated the selected guard and the step-limit off-by-one. It pins JacoDB 37327563ab from UnitTestBot/jacodb#437, correcting constructor parameter-property binding. Schema 2 explicitly binds both coverage and suspended-input policies; old manifests/results cannot silently resume under the new semantics.

Admission depends on source/IR preparation and independent native probes, rather than pilot completion. Frozen source closure, harness, domains, models, frontend and clean tool revision are bound into each cell. Original/instrumented native corruption invalidates the acquisition attempt, including resume and aggregation. Exact statement counters use bounded sets. Earlier integrated fixes preserve primitive String conversion, object-literal runtime kinds, void-result storage and source-attested companion constructors; all 95 optional model IDs remain unchanged.

The original screen contained 48 selected classes plus 152 ordered reserves. Of 200 records, 197 were rejected before machine execution: 82 imports/dependencies, 93 module initialization, 18 AST/reachability/instrumentation limits and 4 input/state domains. Only reserve Stats entered the original primary plan; Perm was blocked by source loading and FaceNameSwizzler by the known frontend defect. The separate engine-suited v7 plan had HashMap, HashUtils and Stats. The sealed 96-cell campaign therefore covers three unique classes and does not establish ecosystem representativeness. New HashMap runs are failure reproductions, not a replacement representative corpus.

Validation: 9 queue-drain checks, the focused TS machine/dispatcher checks and 21 Calls checks passed; 22 Python driver checks passed. After refactoring and adding the late-prefix checkpoint guard, all 13 stopped-state/prefix checks plus 7 class-measurement checks passed again. Affected-module Detekt has no new findings. Clean installDist completed at 421dd926ee39312ec678bfc23be5390066f5a398 with bundled:37327563ab. All seven CI checks passed on this exact published head. Broad local suites are left to CI. The obsolete local pre-commit hook invokes an unavailable checkLicense task; incremental commits use the previously established hook bypass, with focused compilation, tests, Detekt and whitespace checks performed separately.

Revised-protocol diagnostic: one unchanged real HashMap, seed 17, requested 30s in each of the four profiles,91 scenarios and66 original-class statements. All 475 candidate pairs passed complete agreeing original/instrumented replay, with no extraction, replay or native infrastructure failures. Two independent audits checked exact native/strict statement unions and unchanged historical input hashes.

Profile Primary native /66 Strict secondary /66 Terminal In-search prefix Post-stop frontier
EMPTY_STOP 57 0 0 91 0
EMPTY_FRESH 43 0 10 0 0
FROZEN_STOP 58 20 5 0 182
FROZEN_FRESH 58 20 5 0 182

EMPTY_STOP still exhausts after 3553 steps at the unsupported Array.push in construction. Its 91 preserved input scenarios now yield 57/66 actual native coverage. EMPTY_FRESH reproduces the original 10 completed candidates and 43/66 native coverage, despite strict symbolic rejection. Both frozen profiles retain 182 queued input candidates after timeout. Actual search times and overruns remain recorded; FROZEN_STOP took 31,523 ms search plus 1,439 ms final extraction. These are failure reproductions on one class, separate from the sealed v7 campaign. No revised 120s campaign or representative population claim is made.

@CaelmBleidd
CaelmBleidd marked this pull request as ready for review October 13, 2026 23:57
mirror(root, overlay, target)
}

private fun classReplayWrapper(
@CaelmBleidd
CaelmBleidd force-pushed the caelmbleidd/ts-calls-class-measurement branch from e0f349b to 700f8b9 Compare October 14, 2026 15:46
@CaelmBleidd
CaelmBleidd force-pushed the caelmbleidd/pr479-ts-primitive-string-conversion branch from 2f63d41 to 3370736 Compare October 14, 2026 15:46
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