Hacktoberfest 2026：メンテナが10月に向けて印を付けた、オープンで初心者向けの issue。 Hacktoberfest の issue を見る

[TS PBT][P0] Align and simplify property execution semantics before integration

クローズ
  • 何か問題がありますか？
#384 コメント 0 件 リアクション 0 件 担当者 0 名 GitHub で見る

メンテナーはふだん 1 日以内に返信

まだ誰も着手していません。

評価

難易度
5/5
見積もり時間
1週間以上
初心者へのやさしさ
25/100
issue の種類
リファクタリング
明瞭さ
おおむね明確
活発さ
活発
技術スタック
kotlin, typescript
領域
devtools, testing

調査の方向性

Start by locating the existing concrete invocation, symbolic projection/search paths, and the shared property API referenced in the issue. Review the work from #351 and #352 before adding the listed cross-backend fixtures, then compare classifications for preconditions, predicates, special values, aliases, and mutation isolation. Done means the shared contract and focused regressions are integrated without duplicating the invocation or property framework.

索引モデルが issue の本文から書いたものです。

説明

Part of #345. Priority: P0 / Urgent.

Goal

Make fast-check execution, USVM search and replay implement one explicit property contract before extending #351–#354.

Why

The current concrete adapter passes a thrown precondition to fast-check, while symbolic precondition projection discards unsuccessful completions. The concrete adapter also clones arguments separately for the precondition and predicate. One shared manifest alone does not guarantee equivalent execution.

Shared execution contract

  • Inputs follow the existing Kotlin domains and JsConcreteValue encoding. Preserve argument order, special primitive values, and aliases within each supported input graph.
  • A supported precondition is a pure boolean function of its inputs. true admits the input; false discards it. An escaping exception or a non-boolean result is a property-definition/execution error, never a discard or a counterexample.
  • Purity is an author obligation for the supported subset. Do not build a general purity analyzer, heap snapshot framework, or arbitrary side-effect rollback. Fixtures using global state or mutating preconditions are outside this subset.
  • A predicate returns boolean: false is a candidate violation; true holds for that invocation. Any escaping predicate exception, including an assertion exception, is a candidate violation. Expected exceptions must be caught and checked inside the predicate. A non-boolean result is a property-definition error.
  • Predicate-local mutation is allowed. Isolate supported input values between samples, explicit examples, replay and shrinking while preserving aliases within one invocation. No persistent external/module state is supported by the initial symbolic contract.
  • Async predicates/preconditions remain concrete-only where already supported; symbolic execution reports unsupported rather than silently changing their meaning.
  • Timeout, unsupported execution, solver uncertainty and tool errors are not property violations or proof that the property holds.

Scope and implementation boundary

  • Document this contract once beside the common property API; link it from execution, projection, search and replay.
  • Reuse the existing backend invocation and value codec. Fix concrete/symbolic differences at their actual execution points; do not introduce a second property framework or duplicate process clients.
  • Audit the minimal process/coverage helpers touched by these fixes for duplicate validation and hand-written replacements for standard APIs. Keep necessary timeout/cleanup and lossless transport guarantees; unrelated cleanup stays in its owning issue.
  • Before adding replay/shrinking orchestration, add small cross-backend fixtures for true/false/throwing/non-boolean preconditions, false/throwing predicates, special numbers, aliases, and mutation isolation. Test observable behavior rather than internal helper structure.
  • Define exact/approximate/unsupported projection relative to the declared input domain; document the direction and limitation of every retained approximation.

Definition of Done

  • Shared fixtures produce consistent classifications in the existing concrete invocation and symbolic projection/search paths where each supports the property. Replay uses the same existing concrete invocation; completion of #353 orchestration is not a prerequisite for this gate.
  • Existing fast-check generation, reproduction and shrinking still use the same invocation contract.
  • Existing work for #351/#352 is adjusted and reused; it is not reimplemented in parallel.
  • The contract and focused regressions are integrated before #351–#354 are marked complete.
  • No claim of general purity checking, arbitrary mutable-object support, or proof from a bounded unsuccessful search is introduced.
主要言語
Kotlin
スター
33
フォーク
27
平均マージ
3日 8時間
マージ済み PR（30日）
7

環境構築

このプロジェクトには開発コンテナ、Dockerfile、コントリビューションガイドがありません。まず README を読み、一般的な手順ははじめてのコントリビューションガイドを参照してください。

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

UnitTestBot/usvm のほかの issue

UnitTestBot/usvm の issue をすべて見る

似ている issue

Kotlin の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。