Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

[TS PBT] Confirm, classify and shrink symbolic property and hypothesis witnesses

Abierto
  • ¿Algo no está bien?
#353 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Los mantenedores suelen responder en 1 día

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
4/5
Tiempo estimado
3-5 días
Aptitud para principiantes
35/100
Tipo de issue
Nueva funcionalidad
Claridad
Bastante claro
Estado de actividad
Activo
Stack tecnológico
kotlin, typescript
Área
devtools, testing

Línea de trabajo

Start with the candidate inputs from #352, JsConcreteValue, and the shared invocation contract from #384; trace them through the existing backend execution and reproduction path. Add focused tests using the existing adapters and codecs for replay classifications, explicit examples, and shrinking. Done means real TypeScript-runtime fixtures preserve values and aliases, minimized witnesses still violate the property, and unsupported or timed-out shrinking is reported without publishing unconfirmed counterexamples.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

Part of #345. Direct-counterexample delivery depends on #352/#384. The core contract includes hypothesis replay through #398 and is required by #405. Generator-choice and command-sequence reduction are later integrations owned by #400/#402; their acceptance gates do not block core completion.

Goal

Confirm every symbolic candidate in original TypeScript and reuse backend shrinking while preserving exactly what the witness demonstrates.

Scope

  • Consume #352's extracted JsConcreteValue inputs; reuse the current backend invocation, codecs and process supervision.
  • Validate declared domain/generator support as applicable, execute the original precondition and original predicate using #384.
  • Keep outcomes distinct: confirmed original-property violation, confirmed hypothesis refutation with original property holding, no refutation/property holds, domain/precondition rejection, unrepresentable input, unsupported replay, nondeterminism, and property/engine/replay error.
  • A hypothesis replay checks the same program point, context, guard and relation that generated the symbolic target. A different invocation/site does not confirm it. A full original oracle is still required even for an intermediate-prefix target.
  • Preserve target/assertion/hypothesis identity and original input alongside replay status. An exception in a precondition is an error; predicate exceptions follow #384. Hypothesis refutation alone is not counted as a program defect.
  • Preserve special values, argument order and supported aliases/isolation without coercion. Generator-source/context revisions are pinned.
  • Feed eligible external witnesses to backend shrinking; inspect canShrinkWithoutContext or retained native context as appropriate. Explicit-example execution and a zero shrink count are not proof of minimality.
  • Use a target-specific reduction predicate: same original assertion failure, or same guarded hypothesis refutation. Recheck domain/admission and original predicate on the final result. Preserve the original confirmed witness if shrinking is unavailable, fails or times out.
  • For #400, preserve dependent generator construction/choice validity. For #402, reduce commands/arguments while retaining valid guards and the same failure. Add small adapters to backend facilities rather than a general custom shrinker.
  • Return both confirmed failing inputs and useful non-failing behavioral witnesses to #355 with provenance and a reproducible replay artifact. A replay token is not portable across arbitrary generator/backend revisions.
  • Replay/reduction share #354's monotonic deadline. Reserve validation budget and retain unconfirmed candidates when it expires.

Definition of Done

  • Real-runtime fixtures cover confirmed/spurious/rejected/unrepresentable inputs, exceptions, hypothesis-only refutation and unsupported shrinking.
  • At least one external supported witness actually shrinks and still reproduces the same target-specific failure.
  • Source/context mismatch, mutation isolation and core target-preserving reduction have explicit behavior tests. Generator-choice dependency and command-sequence reduction tests are delivered with #400/#402.
  • Artifacts retain original candidate, concrete classification, minimized result if any, reduction metric/attempts, backend revision and reproduction data.
  • No candidate is reported as a final fault before original-oracle replay; no hypothesis-only witness is counted as an original-property violation.
Lenguaje dominante
Kotlin
Estrellas
33
Forks
27
Merge medio
3 d 8 h
PR fusionados (30 d)
7

Preparar el entorno

Este proyecto no incluye contenedor de desarrollo, Dockerfile ni guía de contribución, así que la configuración corre por tu cuenta: empieza por su README y consulta nuestra guía para la primera contribución para los pasos generales.

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de UnitTestBot/usvm

Todos los issues de UnitTestBot/usvm

Issues similares

Más issues de Kotlin

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.