Refinement

A specification refines its kernel: it makes the interface more concrete, and it may not turn it into a different problem. The relation runs one way.

Parameters narrow

type T
 │
 ▼
type T: Integer
 │
 ▼
type T = i64

A kernel may declare a parameter at any rung; a specification must bring every type parameter to the bottom one. Settling must respect the class: kernel type T: Integer, specification type T = i64 is valid because i64 ∈ Integer; type T = f64 is not. The direction never reverses — if the kernel already says type T = i64, a specification may not reopen it.

Value parameters pass through unchanged, and a specification may add its own: representation parameters like L: u32 or q: u32 that the kernel never mentions. An added parameter that appears in no dimension still reaches the implementation in its Point.

Dimensions grow on the right

kernel   tensor<N x T>
              │  refinement
              ▼
spec     tensor<N x L x T>

A specification may add representation dimensions — how a logical element is laid out — and only on the right of the logical ones. The first positions must correspond to the kernel's:

tensor<N x L x T>      valid: L added on the right
tensor<L x N x T>      invalid: N displaced from the first position

Every ? the kernel left must be resolved, by a parameter or a literal.

Arguments keep their order

The kernel's arguments form a positional prefix of the specification's, with the same names. Nothing is removed, nothing is reordered, no result is dropped. Arguments added after the prefix are the representation's — see the = ident suffix for where their values come from.

Secrecy is invariant

secret<T> stays secret<T>; T stays T. Changing visibility changes who learns what, which is the problem itself — it requires a different kernel, not a bolder specification.

In one table

A specification may: settle a type parameter; pick any type its class admits; resolve ?; add representation dimensions on the right; add representation parameters; add technical arguments after the kernel's.

A specification may not: remove or reorder the kernel's arguments; drop a result; change secret either way; violate a class constraint; replace a concrete type with a more abstract one; displace a logical dimension; leave a parameter or a dimension unresolved.

The check is mechanical — a single pass over the two declarations, no code executed — and the platform runs it when a specification is submitted.