Skip to content

[TS PBT] Refute compiler-owned local relations and replay full original properties - #590

Open
CaelmBleidd wants to merge 1 commit into
caelmbleidd/pbt-dsl-local-refutation-basefrom
caelmbleidd/pbt-dsl-local-refutation
Open

CaelmBleidd wants to merge 1 commit into
caelmbleidd/pbt-dsl-local-refutation-basefrom
caelmbleidd/pbt-dsl-local-refutation

Conversation

@CaelmBleidd

Copy link
Copy Markdown
Member

PBT can now challenge a sampled numeric relation immediately after one compiler-owned local result is stored. UsvmDslNumericLocalRefuter.refute(compiled, mapping, concreteCapability, inference, relation) searches the declared domain and original admission with the relation negated at that exact store; it does not negate the original property or execute its suffix symbolically for this auxiliary query.

refutation.captureWitness() uses the existing native confirmation and shrinking coordinator. The declared compiler callback compares the computed result with the original numeric input snapshot. The complete original property still runs, and an original failure takes priority over a matched hypothesis refutation. Missing, wrong, repeated or nonnumeric receipts cannot confirm the target; the public witness hook cannot impersonate this callback.

The entry and local consumers share their existing machine lifecycle, projection and outcome classification internally. Their before-predicate and after-store triggers remain explicit. UsvmRelationRefutationStatus replaces the entry-only enum name; one Kotlin typealias preserves its source spelling, not JVM binary compatibility. Mixed admission followed by an exhausted local query reports NO_REFUTATION_REACHED, rather than treating a single rejected input as global rejection. Entry mapping consumers now reuse the canonical positional input-binding check as well.

Review scope

12 files, +928/-196: production +566/-196 and tests +362. Most removed lines are the entry lifecycle moved into the shared internal runner. The base branch pins #576 plus #584 (including its #580 dependency and canonical input-binding fix), at 7069bca714a020083c998e7c64c53f0b7836644e.

This delivers the explicit numeric result consumer for #398. Shared campaign deadline, cancellation and allocation belong to #399. Retained source hashes and compiler transport keep executable-build status UNVERIFIED; this does not establish transitive executable equivalence.

Validation

  • 59 nearby Kotlin tests passed, including actual PBT observations, the TypeScript project frontend, entry/local auxiliary search, ordinary original-property search, native confirmation and reduction.
  • New local cases cover holding and failing original properties, operand direction, real reduction from 420 to 417, stale callback identity, original admission, timeout, a runtime bound before the selected store, and an exhausted prefix stopping before an unsupported suffix.
  • 75 native adapter tests passed for compiler capture, external witnesses, entrypoints and property execution, including NaN, signed zero, infinities, malformed callbacks and public-hook impersonation.
  • Strict Detekt passed for every changed Kotlin file; diff checks passed.

No experiment or benchmark campaign was run.

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.

1 participant