Skip to content

qualification.md

Latest commit

 

History

History
132 lines (104 loc) · 5.73 KB

qualification.md

File metadata and controls

132 lines (104 loc) · 5.73 KB
Raw

Scientific qualification method

Questions under test

Qualification is organized around falsifiable questions rather than a single coverage percentage:

  1. Do compact builders preserve exactly the caller's finite relation and reject every invalid reference?
  2. Does the Büchi producer agree with an independent language-emptiness oracle?
  3. Does every returned rank or lasso satisfy a narrower local checker?
  4. Does each native acceptance product preserve recurrence-set semantics in both directions?
  5. Do resource boundaries classify exact, insufficient, and invalid cases correctly before allocation?
  6. Is native call-stack use independent of subject depth?
  7. Can the tests detect the removal of individual obligations?
  8. Are published library packages byte-reproducible?
  9. Do closure, exact inclusion, equivalence, simulation, and bisimulation agree with independent language and fixed-point oracles inside their stated profiles?
  10. Do parity-game partitions agree with an independent strategy/cycle oracle, and do fairness products preserve infinite-play acceptance?

Experimental layers

Qualification evidence layers

Exhaustive finite domains

For bounded state and symbol cardinalities, tests enumerate every transition relation and relevant initial or accepting mask. Büchi results are compared with an independent transitive-closure oracle. Acceptance tests enumerate reachable recurrence sets and evaluate the native predicate directly, then compare it with the converted Büchi product. Language-relation tests enumerate all 256 ordered pairs of two-state, one-symbol deterministic-complete machines and compare inclusion and equivalence with a separate ultimately-periodic-word oracle. The complete relation protocol is documented in language-relation qualification. Parity-game tests enumerate all one- and two-vertex games and compare both winning regions with a separate positional-strategy and simple-cycle oracle; the full protocol is in parity-game qualification.

Exhaustion is valuable because it covers rare interactions without a sampling assumption. Its limitation is domain size, so it is paired with randomized and large-subject experiments.

Property-based generation

Generators vary insertion order, duplicates, disconnected states, overlapping acceptance sets, empty families, competing shortest witnesses, and each exact resource boundary. Assertions compare canonical forms or independent semantic consequences rather than internal intermediate state.

Adversarial mutation

Certificate tests begin from valid evidence and mutate one field or obligation: rank order, rank value, state identifier, symbol identifier, path continuity, cycle closure, acceptance, branch parameter, product origin, initial member, accepting member, or target transition. Each mutation must be rejected.

Source mutation testing complements hand-written mutations. A viable mutant is acceptable only when the suite catches it; surviving semantic mutants fail the qualification gate.

Coverage-guided fuzzing

Fuzz targets map arbitrary bytes into bounded typed model components. They do not exercise a transport decoder. The targets cover compact construction, Büchi decision, all acceptance-family conversions, arbitrary mathematical certificate candidates, and bounded language-relation construction and checking. A separate target covers parity solving, local checking, and generated justice products. Input length and algorithm limits bound each run.

Scale and stack experiments

Large deterministic models exercise asymptotic paths on 64 KiB worker stacks. The selected sizes distinguish explicit heap worklists from subject-depth recursion while remaining below declared memory bounds. See stack and resource safety and the pre-registered large-scale protocol.

Package reproducibility

Each publishable library is packaged twice in isolated target directories with the same locked dependency graph. Archive bytes must compare equal, and each archive must contain its normalized manifest. Reproducibility is checked for all component libraries and the facade, including the parity-game component.

Evidence interpretation

No single layer proves the implementation. The confidence argument is triangulated:

$$E= E_{\mathrm{formal}} \cup E_{\mathrm{exhaustive}} \cup E_{\mathrm{differential}} \cup E_{\mathrm{negative}} \cup E_{\mathrm{scale}} \cup E_{\mathrm{reproducible}}.$$

Formal proofs establish general implications under their definitions. Exhaustive and differential tests connect those definitions to executable behavior on complete finite domains. Negative controls establish test sensitivity. Scale tests address resource and stack contracts. Reproducibility addresses delivery identity. A release claim requires all applicable evidence classes to pass together.

Reproduction

Run the aggregate gate:

./scripts/verify.sh

The script renders diagrams before comparing documentation, then checks traceability, formal models, compilation, tests, boundaries, constrained-stack experiments, fuzzing, mutation adequacy, and packages. Command output should be captured by the invoking development workflow so a failure remains inspectable.

The graph-theoretic oracle basis follows Tarjan's strongly connected component (SCC) algorithm Tarjan 1972, while the infinite-word semantic basis follows Büchi's finite-state method Büchi 1962. These citations identify the mathematical lineage; the repository's formal statements and executable tests define the exact implemented contract.