Component reference

Generated types

All authored components are written against types generated from the specification's signature. For:

spec negacyclic 1.0.0 "Negacyclic, with a wide modulus" {
    kernel polymul<N: u32, W: u32>(
        %a: tensor<N x W x u64>,
        %b: tensor<N x W x u64>,
        %q: tensor<W x u64>,
    ) -> %c: tensor<N x W x u64>
}

the generated module contains:

@dataclass(frozen=True)
class Point:                 # one field per value parameter
    N: int
    W: int

@dataclass
class Inputs:                # one field per argument
    a: Tensor
    b: Tensor
    q: Tensor

@dataclass
class Outputs:               # one field per result
    c: Tensor

@dataclass
class Verdict:
    passed: bool
    metrics: dict

These types are regenerated when the signature changes and are not edited by hand. The module also provides Tensor, the codec (encode/decode, pack/unpack for multi-word integers), and Stream.

Stream

The only permitted source of randomness. Defined normatively:

block(i) = SHA256(spec-reference | seed | i)
stream   = block(0) ‖ block(1) ‖ …

API: bytes(n), bits(k), below(n) (uniform on [0, n), bias below 2⁻⁶⁴). Properties:

• identical output in every implementation language, because the construction is written down;
• seekable, so large inputs can be generated in parallel;
• keyed by the specification reference, so two specifications draw different data from the same seed.

random, time, urandom, secrets and other ambient sources are rejected at upload.

generator

generate(p: Point, seed: int) -> Inputs

Produces the input data for one case. Requirements:

• Deterministic: the same (point, seed) must produce identical bytes on any machine, at any time. This is what allows shipping a recipe instead of data and re-verifying any result independently.
• Pure: no file access, no network, no state between calls.
• Produces values only for the kernel's own arguments. Arguments added by the specification are filled by the platform from the point (see Declarations).

One function covers all arguments, because arguments can be mutually constrained (e.g. the second operand invertible modulo the first).

Checks gating accepted:

oracle

oracle(p: Point, seed: int, inp: Inputs) -> Outputs

Computes the expected output. Requirements:

• Deterministic on identical inputs.
• Pure, as above.
• Operates on cleartext regardless of the kernel's secret annotations; encryption is outside the bundle.

Performance is not a requirement: the oracle runs once per case and the result is cached. A direct, obviously-correct algorithm is preferred over an optimised one, because the oracle defines correctness and cannot itself be cross-checked against anything except the test vectors.

Versioning: the oracle's digest is pinned. Changing the oracle changes the definition of correctness, so a change produces a new bundle version; results remain attached to the bundle version they were judged under.

Checks gating accepted:

verifier

verify(p: Point, inp: Inputs, exp: Outputs, got: Outputs) -> Verdict

Compares a submitted output against the expected one. Optional; see absence semantics. The verdict carries metrics beside the flag — for approximate kernels the error value is the useful output, passed is a threshold on it.

Checks gating accepted:

The perturbation check exists because a verifier that returns passed=True unconditionally would otherwise pass review.

Test vectors

Worked examples stored under vectors/ in the bundle: inputs with their expected outputs, produced or checked by hand. Their role is to validate the oracle — the oracle is not trusted until it reproduces all of them. A bundle with no vectors has an unvalidated oracle, and the Testing tab reports that.