Correctness

What twill's two central claims mean, how each is tested, and where each one stops. The claims are that grad computes the derivative and that the shape checker reports only real mistakes. Both are tested here against something other than themselves.

Every number below is regenerated by:

go test ./internal/tensor/  -run TestGradient -v -count=1
go test ./internal/checker/ -run TestChecker  -v -count=1

1. Gradient checking over the full operator set

What is checked

Every differentiable operator in internal/tensor, in 105 cases covering the broadcasting regimes, both axes of a non-square matrix, and the combinations where a bug shows up only in composition. The list is not maintained by hand. TestGradientCheckCoversEveryOperator parses the package's own source with go/parser, collects every exported function that takes or returns a *Tensor, and fails if one has neither a gradient-check case nor an entry in nonDifferentiable saying why it has none.

That closure property is the difference between "the full operator set" as a claim and as a fact. A new operator cannot be added without someone deciding, in writing, whether it carries a gradient.

Current coverage: 64 differentiable operators checked, 31 declared non-differentiable, 95 exported in total.

The non-differentiable list is not a way of quietly excusing operators. It holds the index-valued ones (argmax, argmin, argsort, argtopk, whose outputs are positions, integer and locally constant), the boolean comparisons, the two quantisers (QuantizeI8 and QuantizeI4 are step functions, though the gradient through the product they produce is checked), Cast, and the shape and dtype helpers that are not operators at all.

The method

For a case producing out = op(x), the harness differentiates the scalar

L(x) = sum(w * out)

for a fixed deterministic cotangent w, and compares reverse mode against a Richardson-extrapolated central difference:

D(h) = (L(x+h) - L(x-h)) / 2h            truncation O(h^2)
D*   = (4*D(h/2) - D(h)) / 3             truncation O(h^4)

Three details are load-bearing.

The cotangent is not all ones. An all-ones w makes an entire class of index-shuffling bugs invisible, because a permutation of the output has the same sum as the output. Every transpose, flip, roll, sort, gather and concat case would pass while scattering its gradient to the wrong elements. w is sin(1.7i + 0.3) * (1 + 0.25(i mod 5)): deterministic, no seed to get out of step, and irregular in sign and magnitude.

The extrapolation is what makes a tight tolerance honest. A plain central difference at the best available step carries roughly 1e-10 relative error in f64, which is close enough to a real small-magnitude gradient bug that a failure would be ambiguous. D* lands near 1e-12, so a disagreement above 1e-7 is a defect and not the difference method breathing. Measured error across the cases runs from 1e-13 to 1e-11, leaving four orders of headroom over the observed noise floor.

The step is scaled to the point, h = 1e-4 * max(1, |x_i|), so a coordinate of size 1000 is not probed with an absolute step its own rounding swallows.

Where finite differences cannot adjudicate, and what is done instead

relu, abs, clip, maximum, minimum, max, min, median, sort, topk, cummax, cummin and maxpool2d are piecewise. At a kink the derivative does not exist, and a central difference straddling one reports the average of the two one-sided slopes, which is not what any autodiff system returns. Reporting that as a defect would be reporting a property of the difference method.

So every case for a piecewise operator is sited away from its kinks: nothing near zero for relu, nothing near a bound for clip, no ties in any comparison or ordering. The kinks themselves are then asserted directly in TestGradientKinkConventions, because the convention twill picks is a decision and should be a stable one:

Three of these differ from PyTorch. None is wrong: the subgradient at a kink is a set, and any element of it is defensible. They are written down so that changing one is a deliberate act rather than a regression nobody notices.

The result

All 105 cases agree. Worst relative error by case, highest first:

composite/mlp-layer is two orders above the rest and is not a defect. It is a softmax over a tanh over a linear layer, so the finite difference is taken through a function whose output is bounded in (0, 1) and whose gradient is correspondingly small; the difference quotient loses digits to cancellation before any derivative is formed. It sits below the 1e-7 tolerance with room, and the tolerance is uniform rather than tuned per case.

One case carries a deliberately loosened tolerance, composite/long-cumprod at 1e-5, and the reason is stated in the source: a twelve-element cumulative product spans three orders of magnitude, so the forward pass is ill-conditioned before differentiation begins. It is loosened rather than removed, and the loosening is visible.

What this found

One real defect, and it is the headline of docs/BUGS.md: QLinear and QLinear4 returned tensors with no autodiff graph behind them, so grad through a quantised linear layer answered zero for every upstream parameter while still returning the right value. Fixed in 5344302.

It is worth being precise about why exhaustiveness rather than representativeness found it. The two quantised kernels were the least-exercised operators in the package. A gradient check over the operators someone thought to check would never have reached them, and the defect they had was the worst in the package: not a wrong number, but a plausible one.

What this does not check

Finite differences validate the derivative of the function the interpreter actually computes. If a forward kernel is wrong, the gradient check will happily confirm that its derivative is computed correctly. Forward correctness rests elsewhere: on the golden corpus, on the differential comparison against the self-hosted implementation, and on the closed forms the examples are measured against, such as the Black-Scholes price, delta and vega that examples/montecarlo_option.tw reproduces to four figures.

2. Shape checker soundness

The claim, stated precisely

The checker makes one claim and explicitly declines the other.

It claims: every diagnostic it reports is a real mistake. No false positives.

It does not claim: that a clean check means the program runs. The package comment says it "reports a diagnostic only when a mismatch is certain" and docs/design.md calls the bias toward precision over recall deliberate.

These are not two halves of one property, and conflating them is how a correctness section ends up asserting something untrue. What follows tests the first and measures the second. I am not going to argue that the checker is sound in the sense of accepting only correct programs, because it is not, and the counterexample is six lines.

The checker accepts programs that fail at runtime

let n = len([1.0, 2.0, 3.0])
let A = zeros(2, n)
let x = zeros(2)
let y = A @ x
print(y)

$ twill check unsound.tw
unsound.tw: no shape problems found

$ twill run unsound.tw
unsound.tw:4: runtime error: shape mismatch in @: [2 3] @ [2] (inner 3 != 2)
  4 | let y = A @ x

The mechanism is exactly the design. The checker cannot fold len([1.0, 2.0, 3.0]) to 3, so n types as Unknown, so zeros(2, n) types as Unknown, and an Unknown operand makes the @ undecidable. It stays silent, as designed, and the mismatch reaches the runtime.

This is not an obscure corner. Any shape derived from data read at runtime, from read_csv, from a length, or from a loop-carried value has the same property, and those are ordinary things for a program to do.

There is a second entrance to the same gap that has nothing to do with runtime data, and it is worth naming because it is easy to walk into: grad is a shape barrier. A lambda applied directly is checked. The identical lambda wrapped in grad is not.

let h = fn(v) = sum(zeros(2, 3) @ v)
print(h(zeros(2)))

$ twill check direct.tw
direct.tw:1: shape error: shape mismatch in @: [2, 3] @ [2] (inner 3 != 2)
  1 | let h = fn(v) = sum(zeros(2, 3) @ v)

let g = grad(fn(v) = sum(zeros(2, 3) @ v))
print(g(zeros(2)))

$ twill check viagrad.tw
viagrad.tw: no shape problems found

$ twill run viagrad.tw
viagrad.tw:1: runtime error: shape mismatch in @: [2 3] @ [2] (inner 3 != 2)
  1 | let g = grad(fn(v) = sum(zeros(2, 3) @ v))

Same body, same argument, same mistake; the only difference is grad. In the first program the checker pushes the applied argument's [2] into v and decides the @. In the second, grad returns a function whose parameter shape the checker does not relate to the shape of the lambda it was given, so v types as Unknown and the @ becomes undecidable.

This is the same Unknown-propagation mechanism as above rather than a new one, but it lands in the place twill most advertises, which makes it the version worth knowing. It is a completeness gap and not a soundness one: the checker still says nothing false. Relating grad(f)'s parameter to f's would close it and is a bounded change, since grad preserves the shape of the argument it differentiates with respect to.

Annotating the lambda parameter does not close it either, because the argument that goes wrong is supplied at the application of g, not inside the body.

The claim it does make, tested against the interpreter

Testing "no false positives" on hand-written examples proves little, since the examples are written by the same person who wrote the rules. So it is tested differentially against the interpreter over generated programs.

internal/checker/soundness_test.go generates programs from a small grammar: matmuls, matrix-vector products, elementwise combinations with and without broadcasting, reshapes, concats, calls to shape-annotated functions, and chains where a mismatch is several operations from its cause. Every dimension is a literal drawn from {1, 2, 3, 4}, so the checker has everything it needs to decide, roughly half the programs are broken, and 1 is in the set because it broadcasts against anything and is the case a naive equality rule gets wrong. The seed is fixed, so a disagreement found once can be found again.

Each program is both checked and run, and the two outcomes are treated asymmetrically:

• Checker reports a diagnostic and the program runs. A false positive. Breaks the claim. Fails the test.
• Checker is silent and the program fails at runtime. A false negative. Permitted by design. Counted and reported, so the number is visible rather than merely admitted to.

Result over 4,000 generated programs:

Zero false positives. The claim the checker makes holds over 4,000 programs it did not see while it was being written.

And the completeness it declines to claim, measured

Because every generated program has literal dimensions throughout, a shape error in one is statically decidable in principle. So the same corpus measures what fraction the checker actually decides, which turns "best-effort" from an adjective into a number.

Of 2,646 statically decidable shape errors, the checker caught 2,646, or 100%.

TestCheckerCatchesWhatItCanSee asserts a 95% floor rather than the exact figure, so improving the checker does not break the test and regressing it does.

Reading that honestly

100% on this corpus is a real result and a bounded one. It says that where shapes are statically knowable the checker does not miss, and the grammar covers the operations a numeric program is mostly made of. It does not say the checker is complete, because the corpus is by construction the decidable case. The gap between the two is exactly the example at the top of this section, and it is not narrowing: it is where the design put it.

The corpus is also small in another way. A generated program is at most five lines. It does not exercise nested closures, records, loops that reshape, or grad, all of which the checker leaves Unknown. Extending the generator is the obvious next step and would lower the 100%, which is the point of measuring it.

The other evidence

TestExamplesRunClean in internal/interp/examples_test.go shape-checks and runs every program in examples/, asserting zero diagnostics and a clean run. That is the no-false-positive property on 23 real programs rather than generated ones, and it has been in the suite since before this document.

3. What is verified, in one place

The gate, and why it is the whole of CI

make check runs what CI runs: build, gofmt, vet, the full test suite, and the race pass with CI's own flags and timeout. make ci adds the two linters, which are separate only because they fetch a tool and need the network.

This is written down because the gate was wrong once and it cost a release. check was vet test plus a gofmt check, and was commented "What CI runs", which it had stopped being: CI also ran go test -race -short -timeout 25m and a lint job. 1.6.5 was tagged on a green local run and its CI failed, because the test suite had grown past the race pass's budget and nothing local was measuring that.

The failure was a timeout rather than a data race, and the cause is worth knowing for anyone adding to the corpus: two of the examples train a small model and take fifteen seconds each where every other example is milliseconds, and the corpus is walked twice -- once as written, once as formatted. Under the race detector that was most of the budget. Those two, and the self-hosted differential runs, are skipped when -short is passed, which is the flag the race pass uses and the only pass that uses it. The ordinary run has no -short and runs all of them on every build.

So: a new example that trains anything belongs in heavyExamples, and a new test that spawns the self-hosted compiler belongs behind skipUnderShort. Neither reduces what is checked; both keep the race pass measuring what it is for, which is the parallel tensor kernels rather than a tree walk over a twill source file.