Skip to content

[TS Calls] Add guarded semantic models with a simplified contract - #377

Open
CaelmBleidd wants to merge 8 commits into
mainfrom
caelmbleidd/issue-365-guarded-semantic-models
Open

[TS Calls] Add guarded semantic models with a simplified contract#377
CaelmBleidd wants to merge 8 commits into
mainfrom
caelmbleidd/issue-365-guarded-semantic-models

Conversation

@CaelmBleidd

@CaelmBleidd CaelmBleidd commented Aug 28, 2026

Copy link
Copy Markdown
Member

What this PR delivers

Capability work for #365

  • add guarded semantic-model selection and execution to the existing unknown-call boundary
  • preserve normal and exceptional completion, deferred state changes, aliases, residual fallback, and one observer decision per application
  • add Array.shift as the intrinsic example backed by symbolic-memory memcpy
  • require stable call-target evidence and a supported receiver representation; unknown and fake receivers use fallback

Contract simplification gate for #383

Starting from c996c996 (the last pre-simplification head after the original #365 registry and intrinsic packaging), this PR:

  • collapses descriptor, registration, backend, and implementation wrappers into one TsUnknownCallModel object with an ID, declarative target, and guarded execution
  • removes implementation-kind tags, supported-domain IDs, and stored precision values; residual presence expresses partial handling
  • replaces the old profile and registry layers with one immutable enabled-model catalog and one residual fallback setting
  • derives observable outcomes from model or residual decisions instead of storing a second outcome value
  • removes automatic runtime contract-validation queries for trusted model guards; focused tests own disjointness and completeness obligations
  • removes per-family fallback overrides
  • keeps enabled-set identity based only on model IDs rather than implementation-specific version fields

No obsolete contract or configuration layer from that list remains in the #383 code path.

Scope boundary

This PR completes the common contract and intrinsic integration only. It does not claim source-model execution as delivered.

PR #380 / #366 has the concrete downstream migration path: use the same model object and catalog, expose an EtsIR-backed successor completion, add model EtsIR files to the analysis scene, enter the source body through the normal interpreter, and keep external source or artifact hashes in experiment metadata. Array.pop remains the source-model example there. No second dispatcher, backend registry, or plugin framework is introduced here.

Diff accounting

The complete PR includes both new #365 capability and the later #383 simplification, so its aggregate size is not the size of the simplification alone.

Comparison Production (src/main) Tests (src/test) Documentation Total
Whole PR: origin/main...026c7186 +659 / -223 +711 / -170 +239 / -0 +1609 / -393
Contract simplification: c996c996..026c7186 +461 / -788 +387 / -776 +239 / -0 +1087 / -1564
Final #383 cleanup: 036030b1..026c7186 +8 / -23 +14 / -23 +20 / -18 +42 / -64

The contract-simplification production diff is net -327 lines. The final gate cleanup is net -15 production lines. These comparisons deliberately exclude the earlier capability additions when describing deletion of complexity.

Verification

Local verification:

  • ./gradlew :usvm-ts:test --rerun-tasks
  • ./gradlew :usvm-ts:detektMain :usvm-ts:detektTest --rerun-tasks
  • ./gradlew :usvm-ts:check
  • git diff --check

GitHub CI is green for ci-core, ci-jvm, ci-python, ci-ts, ci-ts-pbt, lint, and detekt at 026c7186.

This PR replaces #376 after its squash commit was removed from main.

Closes #365
Closes #383

Part of #360

@CaelmBleidd CaelmBleidd changed the title [TS Calls] Add guarded semantic model registry and execution [TS Calls] Add guarded semantic models with a simplified contract Sep 8, 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.

[TS Calls][P0] Finish simplifying the model contract before further integration [TS Calls] Register and execute guarded semantic models

1 participant