Implemented surfaces

Status. This is the implemented bootstrap surface for programs whose file extension is .kina. The compiler still accepts the older S-expression core through Sexpr_parser (see 02-surface-kina.md). The roadmap’s Phase 7 surface (frozen grammar, inference, LSP) has not happened; this page documents what the Menhir parser actually accepts.

Pipeline. Text → Kina_parser_wrapper.parse_kina_program → Ast_surface.expr → Type_formation.check_program → optional Ad_pass.transform_ad → Emitter.emit_tensor_program (MLIR).

Limits visitors hit. Tensor payloads in { … } are parsed and discarded; a tensor<F32, [2, 3], @host> { 1.0 } is still a typed placeholder. There is no packaged standard library. See 03-current-status.md.

Grammar and Syntactic Conventions

Lexical Rules

• Comments: Support for // (single-line comments) and /* ... */ (multi-line comments).
• Dimensions: Separated by commas inside brackets, e.g., [B, S, D]. Static dimensions are integers ≥ 1; symbolic dimensions are variables starting with a letter.
• Named Parameters: Certain methods use explicit parameter names to verify usage correctness (e.g., axis=1).

Syntax Mapping Reference

The following table maps the older S-expression core to the bootstrap .kina syntax:

Detailed Syntax Examples

The parser also accepts fn / let / if / while, effect rows (!{…}), perform, and handle. Those forms are early Phase 2 surface, not a completed effect system. A destructuring let (y, g) = e in … names components of a flat tuple (Section 13); it is not a tensor operator. Restricted reverse-mode VJPs for reshape, variadic-batch matmul, and 2D gather are Section 14; there is no surface scatter_add. NLL ∘ decoder plus multi-weight SGD is Section 15 composition, not a new form. Functional AdamW is Section 16 composition (pow, sqrt, broadcast), not a new form. Host argmax is the existing reduce form x.reduce(op=argmax, axis=…) (Section 17); the result dtype is I64. Seeded sampling is Section 18 composition (host Uniform, log / neg, Gumbel-max, argmax), not a new form. KV-cache append is Section 19 composition (concat on the sequence axis plus rank-4 attention), not a new form. The host generation loop is Section 20 composition (static-S decode plus Section 17 argmax), not a new form. Prefill → decode handoff is Section 21 composition (forward returns Kᵀ/V; Phase 0 slice on last logits), not a new form.

1. 2D Matrix Multiplication

• S-expression core:

  (matmul (tensor F32 [2 3]) (tensor F32 [3 4]))

• Bootstrap .kina:

  tensor<F32, [2, 3], @host> @ tensor<F32, [3, 4], @host>

2. Constraint validation with requires

• S-expression core:

  (requires (= B B_prime) (= K K_prime) (matmul (tensor F32 [B M K]) (tensor F32 [B_prime K_prime N])))

• Bootstrap .kina:

  requires [B = B_prime, K = K_prime] compute {
    tensor<F32, [B, M, K], @host> @ tensor<F32, [B_prime, K_prime, N], @host>
  }

3. Reductions & Keepdims

• S-expression core:

  (reduce_keep mean 1 (tensor F32 [2 3]))

• Bootstrap .kina:

  tensor<F32, [2, 3], @host>.reduce_keep(op=mean, axis=1)

4. Slicing & Concatenating Tensors

• S-expression core:

  (slice 0 0 1 (tensor F32 [2 3]))

• Bootstrap .kina:

  tensor<F32, [2, 3], @host>.slice(axis=0, start=0, stop=1)

5. Reshaping, Transposing & Broadcasting

• S-expression core:

  (transpose [1 0] (tensor F32 [2 3]))

• Bootstrap .kina:

  tensor<F32, [2, 3], @host>.transpose([1, 0])

Status. This is the older S-expression core, still accepted by Sexpr_parser.parse_program. It is not the user-facing surface the public site and tests/compiler/examples/*.kina use. That bootstrap .kina grammar lives in 01-surface-kina.md. Normative typing rules live in docs/10-spec/11-phase-0/01–03. The roadmap still lists a Phase 7 surface freeze; that has not happened, and this page is no longer “the only syntax.”

Pipeline. Text → Sexpr_parser.parse_program → Ast_surface.expr → Type_formation.check_program → Emitter.emit_tensor_program (MLIR).

Lexical rules

• Whitespace: spaces separate tokens; no significance beyond token boundaries.
• Identifiers (dtype, unary op name): letters, digits, underscore (_), matched case-sensitively where the parser uses exact tokens (e.g. F32, sum).
• Symbolic dimensions: non-empty strings of [a-zA-Z0-9_] that are not parsed as positive decimal integers. Examples: B, batch, d0.
• Static dimensions: decimal integers ≥ 1 (tensor axis lengths). Zero or negative literals are rejected for normal tensor shapes.
• Integers elsewhere: slice bounds, transpose permutation entries, reduce / concat / slice axis indices — as signed or unsigned per the form below.

Programs

Program ::= Expr
          | RequiresProgram

RequiresProgram ::= '(' 'requires' RequireClause+ Expr ')'
RequireClause   ::= '(' '=' DimAtom DimAtom ')'
DimAtom         ::= <static-dim> | <symbolic-dim>

• requires is allowed only at the root: one (requires …) wrapping the whole program. Nested requires in sub-expressions is rejected at type-check.
• Each RequireClause is a dimension equality (same meaning as tensor shape entries). They are asserted as extra integer equalities in Z3 together with the default axiom every symbolic dim ≥ 1 (phase-0/02 §15).
• Sugar: (requires (e)) with no (= …) clauses is accepted and treated as e (parser unwraps).

Tensor literal

TensorLiteral ::= '(' 'tensor' DType Shape ')'
DType         ::= 'F32' | 'F16' | 'BF16' | 'F8E4M3' | 'F8E5M2'
                | 'I64' | 'I32' | 'I16' | 'I8' | 'I4' | 'Bool'
Shape         ::= '[' (Dim (' ' Dim)*)? ']'
Dim           ::= <static-dim> | <symbolic-dim>

Expressions

Axes in transpose, reduce, slice, concat are 0-based (first axis is 0).

Expr ::=
    TensorLiteral
  | '(' 'add' Expr Expr ')'
  | '(' 'mul' Expr Expr ')'
  | '(' 'sub' Expr Expr ')'
  | '(' 'div' Expr Expr ')'
  | '(' 'pow' Expr Expr ')'
  | '(' 'max' Expr Expr ')'
  | '(' 'min' Expr Expr ')'
  | '(' 'eq' Expr Expr ')'
  | '(' 'ne' Expr Expr ')'
  | '(' 'lt' Expr Expr ')'
  | '(' 'le' Expr Expr ')'
  | '(' 'gt' Expr Expr ')'
  | '(' 'ge' Expr Expr ')'
  | '(' 'bitwise_and' Expr Expr ')'
  | '(' 'bitwise_or' Expr Expr ')'
  | '(' 'bitwise_xor' Expr Expr ')'
  | '(' 'rem' Expr Expr ')'
  | '(' 'frem' Expr Expr ')'
  | '(' 'matmul' Expr Expr ')'
  | '(' 'unary' <name> Expr ')'
  | '(' 'cast' DType Expr ')'
  | '(' 'transpose' Permutation Expr ')'
  | '(' 'reduce' <op> <axis> Expr ')'
  | '(' 'reduce_keep' <op> <axis> Expr ')'
  | '(' 'broadcast' Shape Expr ')'
  | '(' 'slice' <axis> <start> <stop> Expr ')'
  | '(' 'concat' <axis> Expr Expr ')'
  | '(' 'reshape' Expr Shape ')'
  | '(' 'gather' Expr Expr ')'
  | '(' 'softmax' Expr <axis> ')'
  | '(' 'log_softmax' Expr <axis> ')'
  | '(' 'take_along_axis' Expr Expr <axis> ')'
  | '(' 'repeat_interleave' Expr <axis> <n_rep> ')'

Permutation ::= '[' (<int> (' ' <int>)*)? ']'

• Elementwise binary: add / mul / sub / div share dtypes and shapes; pow is on all float dtypes (float8 uses extf → math.powf → truncf in a linalg.generic); max / min use linalg.maxf / minf for f32/f16/bf16 and arith.maximumf / minimumf for float8, or signed int max/min; comparisons eq … ge yield Bool tensors (i1 in MLIR); lt–ge are not defined for bool operands. bitwise_* require bool or signed int operands. rem is signed int remainder (arith.remsi). frem is floating remainder (arith.remf, with an f32 bridge for float8).
• unary: <name> is lowered for relu, neg, abs, exp, log, sqrt, rsqrt, tanh, sigmoid, silu, gelu, bitwise_not, …; float8 nonlinear ops use an f32 bridge inside linalg.generic (see ADR). Typed reduce mean on float8 is supported.
• reduce / reduce_keep: <op> is a word (sum, mean, max, min, …); <axis> is a non-negative int. reduce_keep keeps the reduced axis as length 1.
• broadcast: target Shape must have rank ≥ source rank; rules match shape_ops.broadcastable (NumPy-style trailing alignment).
• slice: static axis size required in the checker for the sliced dimension.
• reshape: element count (∏ dims) must be provable — static product, or Z3 (including requires). MLIR lowering still requires a fully static target Shape for tensor.reshape’s shape operand.

Unsupported leading keywords → parse error: "unsupported expression form".

Examples

(add (tensor F32 [2 3]) (tensor F32 [2 3]))
(matmul (tensor F32 [2 3]) (tensor F32 [3 4]))
(reduce sum 1 (tensor F32 [2 3]))
(broadcast [2 3] (tensor F32 [1 3]))
(requires (= B A) (broadcast [A A] (tensor F32 [B 1])))
(requires (= A 6) (reshape (tensor F32 [A]) [1 6]))
(log_softmax (tensor F32 [2 3]) 1)
(take_along_axis (tensor F32 [1 4 8]) (tensor I64 [1 4]) 2)

Runnable copies live under tests/compiler/examples/*.kina (see tests/compiler/examples/README.md).

API: pretty-printing

The OCaml module Ast_surface exposes pp_tensor and pp_expr: turn a parsed expr back into canonical S-expression text (for docs, diffs, and tests). This is not a full formatter for arbitrary user spacing; it emits a consistent shape.

Compiler work next (after surface)

Ordered backlog aligned with docs/30-decisions/32-phase-0-reference-implementation-status.md:

1. MLIR lowering gaps: any remaining unary_ok vs emit holes; cast pairs still rejected at emit; extra binary ops if §06 grows (floored mod, div rounding modes, …); optional native float8 linalg.* where a bridge is slower than a dedicated op.
2. Reduce: prod, argmin, … in reduce_ok + emitter. Host argmax is Phase 1 Section 17.
3. Types / SMT: refinements R on tensor types and §03-style implication (large); extend requires beyond pairwise = on dims when the spec demands it.
4. Reshape emit: symbolic target dims (dynamic tensor.reshape shape operand or equivalent).
5. Infra: CI workflow when policy allows; exercise toolchain pins on runners.
6. Surface: a bootstrap .kina text already desugars to this AST (01-surface-kina.md). Phase 7 still owns a frozen grammar, inference, error quality, and tooling.

Last updated: 2026-08-23.