Tests, gates and CI#

In Alpha, untested is unfinished. A new kernel, equation, numeric operation, encoder form, host command or plan arrives with a test that the checker or the build decides, in Alpha, in the same change. Scripts only drive alpha check and alpha build; they never compute the answer themselves.

There are four layers, from fastest to broadest:

The declared suite#

alpha test runs the cases in tests/alpha-tests. The file begins format alpha-tests-v1; each case is a test NAME line followed by indented fields, and lines beginning -- are comments:

test closure-checks
  kind check

test defect-corpus
  kind negative
  cases tests/defects

test cache-identity
  kind identity

Useful forms:

alpha test                          # the whole declared suite
alpha test --package bob-system     # one package's suite, from its alpha.package
alpha test --kind negative          # only one kind
alpha test --filter cache           # cases whose name matches
alpha test --list --strict          # the inventory, refusing unclassified cases
alpha coverage                      # what the suite exercises, by dimension

A selection that matches no case is an error, not a vacuous pass. A golden mismatch never rewrites its expectation silently: --propose-golden writes a reviewable proposal, and --apply-golden PATH --explicit applies it and re-verifies.

alpha coverage reports ten dimensions separately as inventory and as executed: public contracts, language rules, executed branches, diagnostics, compiler passes, numeric operations, codecs, resource transitions, hardware support and requirements. A missing denominator is reported as missing, never as an empty success.

Proof roots#

A proof root is a module of laws that ends with def main : Nat = zero. It is run by path and never imported. Each law states that a computation normalizes to an exact value:

def lossAgrees : (equal Nat resultLoss 1087635456) = (refl Nat 1087635456)

The checker accepts this only if it can normalize resultLoss to exactly 1087635456, the IEEE-754 bit pattern of the hand-computed loss. A numerical claim is therefore checked to the bit, not to a tolerance. What a proof root covers depends on what is being tested:

Every proof says what it does not prove. CheckedWarpSum, for instance, states that it establishes nothing about whether the model equals the silicon; that is a device run's job.

The negative corpus#

tests/defects/ holds 161 cases. Each is a directory with the broken module, a Positive.alpha control and a case.json that pins the expected diagnostics:

{
  "modules": ["Form.alpha"],
  "expected": [{
    "code": "ALPHA-TYPE-MISMATCH",
    "module": "Defects.FormByteAnd",
    "declaration": "broken",
    "span": { "lineStart": 4, "columnStart": 24, "lineEnd": 4, "columnEnd": 28 },
    "expected": "Byte",
    "actual": "Nat",
    "phase": "check"
  }],
  "reviewed": true,
  "positive": "Positive.alpha"
}

The observed diagnostics must match the expected set exactly: no missing code, no extra one, the same phase and the same primary span. An unreviewed record is itself an error, and the positive control must check clean in the same run, so a case cannot pass because the whole file is broken. Systems keep their own refusals under systems/*/tests/negative/.

Gates#

A gate is a script in scripts/ci/ that builds and checks real roots and prints one claim per line:

ok    check CheckedWarpSum: …
FAIL  mutant hmma-fragments: the checker accepted it

Any FAIL line fails the gate. Run under the recorder, every ok or FAIL line becomes a receipt in the AOS stream:

alpha observe gate checked-warp-paths -- scripts/ci/checked-warp-paths.sh out/checked-warp-paths

A non-zero exit with no FAIL line is recorded as inconclusive, not as a pass.

Break it before calling it tested#

A test that cannot fail proves nothing, so gates carry mutants: deliberately broken copies of the code that the gate must refuse. checked-warp-paths applies nine, among them swapped matrix fragments (hmma-fragments), a barrier replaced by a plain move (argmax-race) and commuted additions (sum-commuted), and requires each to be refused with a specific diagnostic. A mutation that did not apply is itself a FAIL, so a refactor that moves the mutated text cannot silently disable the test. Representative gates:

CI#

.github/workflows/ci.yml runs on every push to main and every pull request:

• commands builds the compiler, then runs the website checks and the cli-smoke gate. That gate runs the declared suite, the strict inventory, per-package suites, the negative corpus and coverage.
• gates is a six-shard matrix. Each gate is its own step under alpha observe gate, so every claim lands in the run's AOS stream.
• A final step lists every failing receipt with alpha observe receipts out/aos --failing, and validates the streams. It runs even when an earlier step failed, and the streams are uploaded as artifacts.

Gates that need hardware split in two. CI runs the static half: check, build and refused mutants. The device half runs on the device when its environment variable is set, for example ALPHA_AARCH64_SSH for the DGX Spark gates. The record of a device run is committed under tests/observability/import/<device>/, so the evidence outlives the machine.

Adding a test#

1. Write the semantic instance or the contract in Alpha, next to the code it tests or under tests/qualification/Proof/.
2. Add a case to the right suite (tests/alpha-tests or the package's own), or a gate step that checks or builds the root.
3. Add a mutant the test must refuse, and put one mutant in the CI script.
4. Wire it into .github/workflows/ci.yml.
5. Say what the test does not prove.

Read next#

• DiagnosticsReference · generatedDiagnosticsStable error codes, phases, and repair guidance.: the stable codes that negative cases pin.
• ObservabilityBuild · explanationObservabilityRecording any command as an AOS stream, reading it back, and how receipts and gates reach their verdicts.: the streams and receipts gates write.
• Evidence and statusEvaluate · analysisEvidence and statusHow to read checked, run and measured claims, and what each one does not establish.: what checked, run and measured each establish.