[TS Calls] Audit and classify existing semantic approximations

Open
#368 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
5/5
Estimated time
Over a week
Newbie friendliness
35/100
Issue type
Refactor
Clarity
Mostly clear
Activity status
Active
Tech stack
kotlin, typescript

Research direction

Start with #361's production inventory and recovered archive, then compare them with the historical 29-model registry without repeating the inventory. For each item, record its origin, semantic operation, assumptions, domain, effects, tests and frontend assumptions, and assign a reasoned disposition. Done means every item has a disposition, accepted candidates have an implementation mechanism and validation status, and missing selected-family implementations have bounded follow-up issues.

Written by the indexing model from the issue text.

Description

Part of #360. Reuses #361 and feeds #367/#385.

Goal

Review existing production and historical approximations once, deciding what is sound to retain, migrate or reject.

Scope

  • Start from #361's production inventory and recovered archive. Add historical candidates, including the old 29-model registry, without redoing the same inventory from scratch.
  • For each item record its origin, semantic operation, proven target/receiver assumptions, supported/residual domain, effects/exceptions/aliases, tests and frontend assumptions.
  • Distinguish mandatory language semantics and engine/frontend correctness fixes from optional library-model choices.
  • Classify optional models as source-model migration, genuine engine intrinsic, rewrite, reject or deferred pending evidence.
  • Prefer ordinary TypeScript for expressible library semantics. Choose an intrinsic only for a justified symbolic engine operation.
  • Carry accepted candidates into #367's roadmap, but do not automatically require migration of every historical model.
  • Keep mandatory semantics and correctness fixes identical across #385 profiles; they are not experimental model toggles.

Definition of Done

  • Every inventoried item has a reasoned disposition; blocked cases have a concrete reason.
  • Accepted candidates have a domain, intended implementation mechanism and current validation status.
  • A small evaluation subset can be selected without merging the historical branch.
  • Missing selected-family implementations get bounded follow-up issues that block #385.
  • Inventory/audit work does not wait for unrelated model infrastructure.

This is a reviewed inventory, not implementation of the whole standard library or another registry framework.

Dominant language
Kotlin
Stars
33
Forks
27
Avg merge
4d 3h
Merged PRs (30d)
15

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from UnitTestBot/usvm

All issues in UnitTestBot/usvm

Similar issues

More Kotlin issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.