Phase 1, Section 7: Testing, Quality, and Public ABI

Phase 1: Implementation — the shape-typed core compiled end-to-end. Section 7 of 8: Testing, Quality, and Public ABI.

1. What this section commits to

The cross-cutting quality concerns that make Phase 1's deliverables reliable and consumable. Specifically:

• The testing pyramid: unit, integration, end-to-end, with explicit commitments at each level.
• Golden-output tests against PyTorch as the numerical-correctness ground truth.
• GPU testing infrastructure: how GPU-required tests run in CI without forcing every contributor to have a GPU.
• Performance regression infrastructure consuming the observability traces from Section 4.
• Public ABI discipline: three stability categories, the SemVer commitments, the deprecation policy.
• The library author's guide v0.1: the first version of the document that lets external users build on the runtime.
• Documentation requirements: what gets documented, where, and to what standard.

This section is broader than the implementation sections because quality is cross-cutting — every component has testing, ABI, and documentation responsibilities. The unifying discipline: quality is engineering, not vibes. Each commitment here is a specific deliverable with an acceptance criterion.

2. The testing pyramid

Phase 1 commits to the standard testing pyramid: many cheap fast tests at the bottom, fewer expensive slow tests at the top.

                    ╱──────────────╲
                   ╱  GPU end-to-   ╲      ~10 tests, runs minutely
                  ╱    end demos    ╲      Real hardware, real workloads
                 ╱──────────────────╲
                ╱  Golden-output    ╲     ~50 tests, runs on every PR
               ╱  vs. PyTorch       ╲     CPU + GPU; FP tolerance
              ╱──────────────────────╲
             ╱  Integration tests    ╲    ~200 tests, runs on every PR
            ╱  (compile + run)        ╲   Mostly CPU; small workloads
           ╱──────────────────────────╲
          ╱      Unit tests            ╲  ~2000 tests, runs on every push
         ╱  (per module)                ╲ OCaml + Rust + Lean
        ╱──────────────────────────────╲

The shape is conventional. The substantive commitments are at each layer.

3. Unit testing

The largest layer. Per-module, fast, no external dependencies.

3.1 OCaml side: alcotest

The compiler uses alcotest (per Phase 0 §5.2). One test executable per library, organized as:

compiler/test/unit/
├── lexer_tests.ml          — tokenization edge cases
├── parser_tests.ml         — S-expression parsing; well-formed and malformed inputs
├── ast_tests.ml            — AST equality, traversal, location preservation
├── elab_tests.ml           — type-checker positive and negative cases
├── unify_tests.ml          — shape unification three-way outcomes
├── smt_tests.ml            — Z3 wrapper; canonical-hash caching; timeout handling
├── ir_tests.ml             — IR construction and well-formedness invariants
├── lowering_tests.ml       — MLIR text emission; per-operation patterns
└── error_tests.ml          — error formatting; source-span carets; counterexample rendering

Each library has a corresponding test file. Coverage: every public function has at least one positive and one negative test. Tools like bisect_ppx measure coverage; the goal is >85% line coverage in the OCaml side.

3.2 Rust side: built-in test framework

The runtime uses Rust's built-in #[test] machinery. Tests live alongside source code (in-module) for unit tests; in tests/ for integration tests:

runtime/src/
├── memory/
│   ├── mod.rs              — contains #[cfg(test)] mod tests { ... }
│   ├── pool.rs             — same
│   └── ...
└── ...

runtime/tests/
├── tensor_lifecycle.rs     — cross-module tests
├── dlpack_roundtrip.rs     — flagship interop demo (Section 3 §5.4)
└── ...

Coverage measured by cargo-tarpaulin; goal >85% on the runtime. Some FFI entry points are difficult to cover without a GPU; those are exercised by integration tests instead (§4).

3.3 Lean side: minimal

The verification track (Section 6) has its own correctness story — a Lean theorem either type-checks (proof valid) or doesn't (proof invalid). Unit tests in Lean cover example uses of the mechanized definitions, not the proofs themselves. A few hundred lines of verify/test/. Smaller relative scope; the proofs are the tests.

3.4 Property-based and fuzz testing

Two specific patterns worth investing in:

• qcheck for the parser and type-checker. Generate random S-expressions; assert the parser doesn't crash on malformed input and that valid inputs round-trip through parse → unparse. Assert the type-checker terminates on all inputs (no infinite recursion in elaboration).
• Fuzz testing on the FFI surface. Use cargo-fuzz to throw random byte sequences at the FFI entry points; assert no crashes, only error returns.

Both surface bugs that example-based tests miss. The cost is bounded — a few thousand lines of test infrastructure that runs ~hourly in CI rather than per-PR.

4. Integration tests

End-to-end small-scale: compile a program, load it, run it, verify the output.

compiler/test/integration/
├── mlp_forward.ml          — MLP on CPU; matches a hand-computed reference
├── mlp_forward_gpu.ml      — same on GPU
├── attention_block.ml      — Q, K, V → softmax → output on CPU
├── attention_block_gpu.ml  — same on GPU
├── stdlib_compositions.ml  — proto-stdlib test cases (per bootstrap track)
└── error_paths.ml          — programs that should fail; verify error messages

Each integration test is a complete compile-and-run cycle. They're slower than unit tests (each one shells out to mlir-opt, llc, clang) but still bounded — under 5 seconds per test, ~10 minutes for the integration suite.

Integration tests run on every PR. Failures are PR-blocking.

4.1 Error-path tests

Often skipped, always valuable. For each kind of error the language can surface:

• A test program that triggers it.
• A snapshot of the expected error message (using expect-test or similar).
• The test fails if the error message changes; updating requires explicit acknowledgment.

This catches accidental regression in error quality. Phase 1's Section 2 §10 commits to good error messages; this is how that commitment stays alive.

5. Golden-output tests against PyTorch

The numerical-correctness ground truth. PyTorch is the reference implementation; our compiled programs are correct when their outputs match PyTorch's within FP tolerance.

5.1 The pattern

For each operation (and each composition we care about):

# golden_tests/test_matmul.py
import torch
import kina  # our runtime's Python bindings (Phase 1 may use ctypes)

def test_matmul_basic():
    torch.manual_seed(42)
    a_torch = torch.randn(128, 256, dtype=torch.float32)
    b_torch = torch.randn(256, 64, dtype=torch.float32)
    
    # Compile and run our version
    a_ours = kina.from_torch(a_torch)
    b_ours = kina.from_torch(b_torch)
    program = kina.compile_fixture("matmul.sexp")
    c_ours = program(a_ours, b_ours)
    
    # PyTorch reference
    c_torch = a_torch @ b_torch
    
    # Compare
    assert torch.allclose(
        kina.to_torch(c_ours), c_torch,
        rtol=1e-5, atol=1e-6
    )

The pattern is uniform: torch produces the reference, our runtime produces the candidate, allclose verifies. FP tolerance:

These are PyTorch's defaults for the same comparisons; we adopt them.

5.2 Coverage

Every Phase 0 operation gets golden tests. Every Phase 1 operation extension (Section 5) gets golden tests. The flagship transformer block from Section 1 §3.3's exit criterion gets golden tests against a PyTorch implementation of the same block.

The library author's guide (§9) ships with golden tests as worked examples — every documented usage pattern has a corresponding test that verifies it works.

5.3 What golden tests catch (and don't catch)

Catch:

• Semantic regressions (an operation produces wrong values).
• Numerical regressions (an operation drifts outside tolerance).
• Lowering bugs (CPU output differs from GPU output in incorrect ways).

Don't catch:

• Performance regressions (a test that's 100x slower still passes if numerically correct).
• Memory leaks.
• Crash-on-invalid-input bugs.
• ABI breakage that doesn't affect numerical output.

Each gap has dedicated tooling in §6, §7.

6. Performance regression infrastructure

Built on Section 4's observability commitments. The traces emitted during golden tests are the raw material for performance tracking.

6.1 What gets measured

Per benchmark (the transformer block, an MLP, an attention layer, individual operations):

• End-to-end time — wall-clock from input to output.
• Per-operation time — extracted from observability spans.
• Per-kernel-launch time — extracted from NVTX ranges.
• Memory-allocation count and total bytes — extracted from the TracingMemoryResource events.
• GPU utilization — sampled from CUDA events in the runtime.

These are the dimensions that matter for an ML compiler. Wall-clock alone is insufficient — it doesn't tell you where the regression came from.

6.2 The regression policy

Three thresholds:

The "explicit acknowledgment" path is for legitimate regressions — a correctness fix that happens to slow things down, an architectural change that improves something else. The PR description has to justify the regression and the reviewer has to approve.

This policy errs on the side of permissive at the low end (5% noise is real on shared CI hardware) and strict at the high end (>15% is a real regression that deserves attention).

6.3 Baseline management

Baselines are stored per-benchmark in a tracking file (benchmarks/baselines.json). They update on the main branch's most recent successful run; PRs compare against the baseline at branch-off time.

Hardware variability is handled by running each benchmark N=20 times, taking the median as the comparison number. Outliers (top and bottom 10%) are discarded. This gives stable enough numbers on shared CI hardware to make the 5% / 15% thresholds meaningful.

6.4 What's deferred

A full performance-tracking dashboard with historical graphs, drill-down by operation, GPU-vs-CPU comparison, etc. is not Phase 1 work. The Phase 1 deliverable is the regression detection in CI — the dashboard is Phase 5+ work, plausibly served by a Grafana plugin consuming the same observability data.

7. GPU testing infrastructure

GPU tests need GPU hardware. Phase 1's commitment: GPU CI exists, but runs on a separate path from the standard CI flow.

7.1 The two-tier CI

• Standard CI runs on every push. CPU-only. Unit + integration + golden tests for CPU paths. Most contributors only ever interact with this tier.
• GPU CI runs on PRs that touch GPU-relevant code (the runtime, the lowering pipeline, the FFI surface) and on a periodic schedule for everything else. Self-hosted runners with CUDA hardware.

The split keeps standard CI fast (under 10 minutes per push) while still catching GPU regressions before merge for code that affects GPU paths.

7.2 Self-hosted runners

GPU CI requires self-hosted runners. Phase 1's discipline:

• Single GPU model per runner pool — picking one (e.g., RTX 4090 or a data-center card the project has access to) and running all GPU CI on identical hardware. Cross-GPU compatibility testing is Phase 5+ work.
• Dedicated to this project — no shared CI runners; performance baselines depend on consistent hardware.
• Documented setup — a docs/gpu-ci-setup.md covering OS, CUDA driver version, NVIDIA Container Toolkit (if running tests in containers).

7.3 GPU-specific test categories

Beyond running standard tests on GPU, three GPU-specific categories:

• Multi-stream tests — operations on different streams produce results in correct order; cross-stream synchronization works.
• Memory pressure tests — stress the memory manager with allocations until OOM; verify graceful failure.
• Determinism tests — the same program with the same input produces bitwise-identical output across runs. CUDA's determinism settings have to be enabled (the runtime sets them by default in tests).

The determinism tests are the most interesting. Many ML workloads are non-deterministic by default in CUDA (atomic operations on float values can produce different orderings). The runtime forces deterministic mode (per CUDA_LAUNCH_BLOCKING and similar). Verifying determinism in CI catches accidental regressions.

8. Public ABI: categories and discipline

The runtime is a library that other code links against. Stability matters. Phase 1 commits to three categories.

8.1 The three categories

Stable — covered by SemVer. Breaking changes only at major version bumps. Documented in docs/api/stable.md.

What's stable in Phase 1:

• The C ABI of Tensor's #[repr(C)] prefix (per Section 3 §5.1).
• The DLPack import/export functions and the DLPack version supported.
• The MemoryResource C-callable interface.
• The 17 FFI entry points the compiler emits calls to (Section 3 §6.1).
• The runtime's error-code enum.
• The compiler CLI flags marked stable in the documentation.
• The compiled program's entry-point conventions (how to load, how to call).

Unstable — public but not stability-promised. Documented as such; can change between any version. Used by ourselves and by adventurous early adopters.

What's unstable in Phase 1:

• The internal IR types (the typed-IR data structures from Section 2 §5.1).
• The MLIR text format we emit (subject to upstream MLIR changes).
• The memory manager's internal allocator algorithms (only the trait is stable).
• The Lean mechanization (research artifact; not a contract).
• The library author's guide patterns marked "unstable."

Internal — not for external use. May change without notice. Not documented for outside consumers.

What's internal:

• OCaml module boundaries within the compiler.
• Rust module boundaries within the runtime (only public re-exports are public).
• The compiler's intermediate file formats (the .mlir text output is for debugging).
• Test fixtures and their organization.

8.2 The deprecation cycle

A stable API gets removed only after:

1. Mark deprecated in version X.Y.Z. Compile-time warning emitted when used.
2. Document removal target in the same release. Typical: removed in X+1.0.0 (next major) or X.(Y+2).0 (two minor versions).
3. Provide a migration path in docs/migrations/.
4. Remove in target version.

Three-version deprecation cycles are the norm for libraries with serious users; Phase 1 adopts the same discipline.

8.3 ABI testing

For each stable surface, an ABI snapshot test:

• The struct layout is recorded (sizes, alignments, field offsets).
• The function signatures are recorded.
• A change to either fails CI unless the snapshot is explicitly updated.

This catches accidental ABI breakage — an unintended #[repr(C)] field reorder, a parameter type change, a return-type widening. The cost is one test file per stable surface; the value is enormous.

9. The library author's guide v0.1

The first version of the document that lets external users build on the runtime. Per the ecosystem-architecture forward track, this is a Phase 1 deliverable.

9.1 What v0.1 covers

• Allocating tensors — using the MemoryResource trait, picking an implementation, configuring the current resource.
• Constructing tensors — from raw data, from DLPack, from compiled-program outputs.
• Calling compiled programs — loading a .so, finding entry points, invoking with type-checked arguments.
• Adding custom operations — the simple case where the operation is already in the runtime; the harder case where it isn't (deferred to a Phase 5+ doc).
• Custom memory managers — implementing the MemoryResource trait, plugging it in.
• DLPack interop — exporting tensors to other frameworks, importing tensors from them.
• Error handling — what error codes mean, how to recover.
• A worked example — a small library (e.g., a minimal softmax_with_temperature library) implemented end-to-end.

The guide is a real document, not a stub. Estimated length: 30–50 pages. Lives at docs/library-authors-guide.md.

9.2 What v0.1 explicitly doesn't cover

• Custom operations that extend the type system (Phase 5+ via the Open vs. Closed Compiler issue from the bootstrap track).
• New refinement-language extensions.
• Cross-runtime compatibility (only our runtime).
• Performance tuning beyond basic patterns.
• Security considerations (Phase 7+).

These get their own documents in later phases. v0.1's scope is bounded by what's actually possible in Phase 1's runtime.

9.3 Acceptance criterion

The worked example (a small library implementing one or two custom patterns) must compile, link, and run cleanly using only the documentation. No undocumented internal functions; no workarounds. If the documentation isn't sufficient to build the worked example, the documentation is wrong.

This is the test that the guide is honest. Most "library author's guides" in young projects accidentally rely on internal knowledge; explicit acceptance against the worked example prevents this.

10. Documentation requirements

Beyond the library author's guide, the rest of the documentation surface.

10.1 What gets documented

10.2 The doc-build pipeline

cargo doc for Rust; dune build @doc for OCaml; lake build :docs for Lean. All three are invoked by make docs; the output is a single static site at docs/_build/html/.

The doc site is built and uploaded to a hosted location (GitHub Pages or similar) on every push to main. PR previews available for documentation changes.

10.3 Documentation as testable artifacts

Code examples in documentation are runnable. Rust's doctest mechanism executes code in doc comments as part of cargo test. OCaml's mdx does the same for .md files. Both are wired into CI.

This catches the most common documentation rot: examples that worked once but stopped working when the API changed. Treating doc examples as tests means doc examples can't drift silently.

11. Implementation milestones (testing/quality-specific)

The testing and quality work spreads across Phase 1's three milestones:

11.1 Milestone 1 (months 1–2): foundations

• Unit testing infrastructure for OCaml + Rust.
• Standard CI pipeline for CPU paths.
• Baseline coverage measurement (>85% target).
• ADR for ABI categories.
• Initial docs/architecture/ covering compiler and runtime overviews.

11.2 Milestone 2 (months 3–4): GPU and golden tests

• GPU CI pipeline with self-hosted runners.
• Golden-output tests for all Phase 0 operations + Phase 1 extensions.
• DLPack roundtrip test in CI (Section 3 §5.4).
• Performance regression infrastructure consuming observability traces.
• ABI snapshot tests for the runtime's C surface.

11.3 Milestone 3 (months 5–6): library author's guide and polish

• Library author's guide v0.1 with worked example.
• Documentation site live; doctests passing.
• Property-based testing for parser and type-checker.
• Fuzz testing for FFI surface.
• Migration guides for any stable-API changes during Phase 1.

12. Acceptance criteria

The single load-bearing criterion is the library author's guide worked example builds from documentation alone. Everything else is supporting infrastructure; this one criterion is the empirical evidence that the runtime is actually consumable by external users.

13. Open issues introduced by this section

1. Cross-platform GPU CI. Phase 1 commits to a single GPU model on self-hosted runners. Cross-GPU portability testing (different generations, different vendors) is Phase 5+ work. This means Phase 1 may ship code that subtly relies on a single GPU's behavior; risk is real but bounded.

2. CUDA driver version pinning. Phase 1 pins to CUDA 12.x. Driver upgrades on the GPU CI runners can cause flakiness. The discipline: deliberate-cycle upgrades (per Phase 0 §5.7), with at least one full CI cycle of validation before merging the upgrade.

3. Documentation maintenance burden. Doc-as-tests + every public item documented + worked-example-must-build is a real maintenance burden. If contributors find it onerous, the documentation rots. Phase 1's bet: the burden is worth it because it forces the API to be explicable. If it isn't worth it in practice, lower the standard for unstable APIs.

4. The "explicit acknowledgment" path for performance regressions. §6.2's >15% threshold can be acknowledged for legitimate reasons. This creates a slow drift risk — small acknowledged regressions stack up. Mitigation: a quarterly performance review that examines all acknowledgments since the last review; if cumulative drift exceeds 30%, an investigation is mandatory.

5. Self-hosted runners' availability. GPU CI fails when the runner is offline or under maintenance. PRs that touch GPU paths may queue. Phase 1's response: a fallback to manual sign-off when GPU CI is unavailable (with notification to a maintainer); not ideal but pragmatic. Phase 5+ may invest in redundant runners.

6. The library author's guide as living documentation. v0.1 is Phase 1's commitment; subsequent versions track API changes. The risk: v0.1 lands and then doesn't get updated. Mitigation: every PR that changes a stable API must update the guide if the guide references the changed surface.

14. Section 8 preview

Section 8, the final section, covers Exit Criteria and Phase 2 Entry:

• The full Phase 1 acceptance criteria summary, consolidating from all seven preceding sections.
• The judgment-call exit criterion (Section 1 §4 #7) — when Phase 1 is "done enough" to commit to Phase 2.
• The risk-and-abandonment criteria from Section 1 §6, revisited with the implementation context now visible.
• Phase 2 entry conditions: what Phase 1 must hand off to Phase 2.
• Closing notes on the project's overall arc.

After Section 8, Phase 1 specification is complete. Implementation work can begin (or be reconsidered) against a fully-defined target.

End of Phase 1, Section 7.