Phase 0, Section 2: Core Operation Set & Typing Rules

Phase 0: Foundation — establishing the formal core calculus. Section 2 of 5: Core Operation Set & Typing Rules.

1. What this section commits to

The minimum viable operation set, the typing judgment for expressions, and the rules for each operation. Every operation included here must work end-to-end: parse, type-check, lower to MLIR linalg, execute correctly. Every operation excluded is deferred — possibly to a later phase, possibly to never.

This section addresses some open issues from Section 1 (reshape's variable-product problem, the placement of requires vs. inline refinements) and introduces the broadcasting commitment.

2. Conventions and judgment forms

Three judgments in play:

The third is the one that does the real work. Whenever an operation has a shape constraint between inputs (matmul's contraction dim equality, concat's matching outer dims, reshape's volume conservation), it appears as a premise of the form Γ ⊨ φ, and Z3 discharges it. If Z3 returns unsat or times out, the operation does not type-check.

Shape unification — Γ ⊢ s₁ ≡ s₂ — is shorthand for "the lengths of s₁ and s₂ are equal and Γ ⊨ s₁[i] = s₂[i] for each i." It is not a separate judgment; it expands to the SMT calls.

Throughout, T ranges over types, e over expressions, dt over dtypes, s over shapes, α over shape variables.

The signed-integer admissibility class is {I64, I32, I16, I8, I4}. Any operation admitted for signed integer dtypes admits all five unless its rule states otherwise.

2.1 Tensor operations vs shape expressions

Do not confuse value-level tensor ops with type-level shape arithmetic:

• binop mul (§6) multiplies tensor elements pointwise on two tensors of the same shape. It is a runtime operation on data.
• Shape dimensions are built from the grammar in Section 1 §2: literals, variables, +, −, multiplication by a constant, mod by a constant, and division by a constant when in Presburger form. There is no “tensor multiply” at the type level.
• Variable×variable products in shapes are not expressible inside the refinement algebra; use the axiomatic escape hatch (fresh name + asserted equality; Section 1 §3, reshape Section §10).

3. The operation set

Phase 0 commits to ten core operations, organized by what they do to shape. Reduce is a single operation in the IR with a keepdims mode; the type system gives two typing rules in §8 (reduce and reduce-keep) for the same construct—this does not increase the operation count.

This is the smallest set that supports a non-trivial neural network forward pass (transformer attention, MLP, layer norm). Operations not listed — pad, gather/scatter, sort, scan, FFT, conv — are deferred. They can be added later without changing the type system; the design is for additivity.

Notably not in Phase 0:

• Convolution. Tractable in this type system but the rule is complex (stride, padding, dilation, groups). Deferred.
• Gather / scatter / index. Data-dependent shape and value lookups. Connects to existential dimensions (Section 1, §5), deferred.
• Conditional / control flow. No if over tensor values, no while. Phase 0 is straight-line code.
• Stateful operations. No mutation, no parameters-as-state. Functions are pure. State enters with the effect work in Phase 2.

4. Elementwise unary

Γ ⊢ x : Tensor[dt, s, R]    Γ ⊢ unaryOp(dt) ok
─────────────────────────────────────────────────  (unary)
       Γ ⊢ unaryOp x : Tensor[dt, s, R]

Unary operations preserve shape, dtype, and refinements. The unaryOp(dt) ok premise enforces dtype admissibility — relu works on FP and signed integer types; exp requires FP; bitwise_not requires integers. The admissibility set is fixed per operation.

Operations included: relu, gelu, silu, tanh, sigmoid, exp, log, neg, abs, sqrt, rsqrt, bitwise_not. The list is not load-bearing — adding more is mechanical.

Note on refinements. Refinements are propagated by unary operations because the data layout doesn't change. If the input was guaranteed D mod 8 = 0, the output is too.

5. Cast

Γ ⊢ x : Tensor[dt₁, s, R]    Γ ⊢ castOk(dt₁, dt₂)
──────────────────────────────────────────────────  (cast)
       Γ ⊢ cast[dt₂] x : Tensor[dt₂, s, R]

Cast changes dtype, preserves shape and refinements. The castOk(dt₁, dt₂) premise is a fixed admissibility table — most casts are allowed (FP↔FP, FP↔INT, narrowing/widening), with the understanding that lossy casts are allowed but produce approximate results. Numerical error analysis (Phase 6 territory) refines this.

For Phase 0: castOk is total — every dtype pair is admissible. This is permissive; later phases can tighten it (e.g., disallow Bool → F32 if the semantics aren't right).

6. Elementwise binary

Γ ⊢ x : Tensor[dt, s, R₁]
Γ ⊢ y : Tensor[dt, s, R₂]
Γ ⊢ binOp(dt) ok
──────────────────────────────────────────────────  (binary)
   Γ ⊢ binOp x y : Tensor[dt, s, R₁ ∧ R₂]

Binary operations require exactly matching shapes and exactly matching dtypes. There is no implicit broadcasting in the core IR. If the user wants broadcasting, they call broadcast explicitly.

This is the single most contentious decision in Section 2. The rationale is in §11.

The output refinement set is the conjunction of input refinements: anything true of both inputs is true of the elementwise result.

Operations included: add, sub, mul, div, pow, min, max, eq, lt, le, bitwise_and, bitwise_or, bitwise_xor. Comparison operations have a special case where the output dtype is Bool:

Γ ⊢ x : Tensor[dt, s, R₁]
Γ ⊢ y : Tensor[dt, s, R₂]
Γ ⊢ cmpOp(dt) ok
─────────────────────────────────────────────  (compare)
    Γ ⊢ cmpOp x y : Tensor[Bool, s, R₁ ∧ R₂]

7. Matmul

Γ ⊢ a : Tensor[dt, [B, M, K], R₁]
Γ ⊢ b : Tensor[dt, [B', K', N], R₂]
Γ ⊨ B = B'
Γ ⊨ K = K'
─────────────────────────────────────────────  (matmul)
   Γ ⊢ matmul a b : Tensor[dt, [B, M, N], R₁ ∧ R₂]

Standard batched matmul. Dtype must match (no mixed-precision in the core IR; mixed precision is a separate cast-then-matmul pipeline). The contraction dimension K must equal K', and the batch dimension B must equal B' — both discharged via SMT.

Why batched matmul as the core operation rather than 2D matmul. Production ML uses batched matmuls; making 2D the core means every real call site uses a unsqueeze-then-matmul-then-squeeze pattern. Defining batched as core and 2D as a special case (with a one-element batch) is cleaner.

No higher-rank matmul. A matmul of [..., M, K] against [..., K, N] with arbitrary leading batch dims is not supported in Phase 0. The user reshapes leading dims into a single batch dim, calls matmul, reshapes back. Surface syntax can sugar this later (Phase 7).

8. Reduce

Γ ⊢ x : Tensor[dt, [d₁, ..., dₖ], R]
i ∈ {1, ..., k}
Γ ⊢ reduceOp(dt) ok
─────────────────────────────────────────────────────────────  (reduce)
   Γ ⊢ reduce[reduceOp, axis=i] x : Tensor[dt, sᵢ, R]
   where sᵢ = [d₁, ..., dᵢ₋₁, dᵢ₊₁, ..., dₖ]

The axis to reduce over is a compile-time integer. Reductions remove that dimension from the shape. For keepdims=true behavior, the reduced dimension becomes 1:

Γ ⊢ x : Tensor[dt, [d₁, ..., dₖ], R]
i ∈ {1, ..., k}
─────────────────────────────────────────────────────────────  (reduce-keep)
   Γ ⊢ reduceKeep[reduceOp, axis=i] x : Tensor[dt, s'ᵢ, R]
   where s'ᵢ = [d₁, ..., dᵢ₋₁, 1, dᵢ₊₁, ..., dₖ]

Multi-axis reduce desugars to repeated single-axis reduce, evaluated outside-in (largest axis first to keep intermediate shapes well-formed).

Operations included: sum, mean, max, min, prod, any, all, argmax, argmin. The last two have output dtype I64 regardless of input.

9. Transpose

Γ ⊢ x : Tensor[dt, [d₁, ..., dₖ], R]
π : permutation of {1, ..., k}
─────────────────────────────────────────────────────────────  (transpose)
   Γ ⊢ transpose[π] x : Tensor[dt, [d_{π(1)}, ..., d_{π(k)}], R]

The permutation π is a compile-time list of axis indices. Type-checking is mechanical — substitute the permuted shape into the result type.

Refinements survive transpose because they're symbolic predicates on shape variables, not on positional indices. A predicate D mod H = 0 references D regardless of which position D occupies in the shape list.

10. Reshape

This is the operation Section 1 §7 flagged as awkward. Section 2 commits to a special form.

Γ ⊢ x : Tensor[dt, [d₁, ..., dₘ], R]
target shape s' = [e₁, ..., eₙ]
Γ; volEq([d₁, ..., dₘ], [e₁, ..., eₙ]) ⊨ ⊤
─────────────────────────────────────────────────────────────  (reshape)
   Γ ⊢ reshape[s'] x : Tensor[dt, s', R']

The premise Γ; volEq(s, s') ⊨ ⊤ says "in context Γ augmented with the volume-equality assumption between s and s', the obligation ⊤ holds" — which is trivially true, but the augmentation is the work. volEq is a built-in axiom schema:

volEq([d₁, ..., dₘ], [e₁, ..., eₙ]) ≡ d₁ · d₂ · ... · dₘ = e₁ · e₂ · ... · eₙ

Outside Presburger because of variable-times-variable products. Phase 0 commits to trusting the user: the equality is asserted into the context, not proven. If the user is right, the type-checker propagates the assertion through subsequent operations. If the user is wrong, the runtime catches the mismatch (the actual reshape opcode checks element count and faults).

This is unsound in the strict type-theoretic sense and the spec says so. The unsoundness is bounded — a reshape with wrong volume only affects reshape operations and their immediate descendants. Anywhere downstream that depends on a specific output shape value will have already been type-checked under that assumed shape, and the runtime's reshape check is a backstop. This is the same compromise PyTorch's symbolic shape engine makes (torch.compile accepts reshape volume assertions axiomatically and verifies at runtime).

The output refinement set R' is not the input refinement set in general: refinements that mention shape variables that don't appear in the output type must be dropped. Specifically: R' = { p ∈ R : free_vars(p) ⊆ {α : α appears in s'} }. A refinement on D does not survive a reshape that eliminates D.

A future phase can refine this with a verified reshape — proving the volume equality from a compositional reasoning about how dimensions split or merge — but Phase 0 leaves it as the controlled escape hatch.

11. Broadcast (explicit)

Γ ⊢ x : Tensor[dt, s, R]
target shape s'
Γ ⊨ broadcastable(s, s')
─────────────────────────────────────────────────────────────  (broadcast)
   Γ ⊢ broadcast[s'] x : Tensor[dt, s', R'']

The broadcastable(s, s') predicate is:

broadcastable([], _) ≡ ⊤
broadcastable([d₁, ..., dₖ], [e₁, ..., eₙ]) where k > n ≡ ⊥
broadcastable([d₁, ..., dₖ], [e₁, ..., eₙ]) where k ≤ n ≡
    let pad = n − k in
    ⋀ᵢ₌₁ⁿ (i ≤ pad ∨ d_{i−pad} = e_i ∨ d_{i−pad} = 1)

In words: shapes broadcast if the source can be left-padded with 1s to the target's rank, and each dimension after padding either equals the target dim or is 1. NumPy semantics, formalized.

The output refinement set R'' drops refinements that mentioned dimensions that get broadcast (became 1 in the source, larger in the target). A refinement on D survives iff D appears in s' with the same value.

Decision: explicit broadcast in the core IR; no implicit broadcasting in elementwise binary operations. Rationale:

• Implicit broadcasting in the elementwise rule produces a complex typing rule with shape unification under "equal or one is 1" — workable but adds case analysis at every binary operation.
• Explicit broadcast adds visible operations to the IR. Lowering can fuse them with the immediately-following elementwise op so there's no runtime cost.
• Surface syntax (Phase 7) can sugar x + y into broadcast(x, common_shape) + broadcast(y, common_shape) based on shape inference. The core IR stays clean.

This trades user friction at the IR level for a simpler type system. Phase 0 is meant to be the contract, not the user-facing surface; the trade is right at this level.

12. Slice

Γ ⊢ x : Tensor[dt, [d₁, ..., dₖ], R]
i ∈ {1, ..., k}
a, b : Dim
Γ ⊨ 0 ≤ a ∧ a ≤ b ∧ b ≤ dᵢ
─────────────────────────────────────────────────────────────  (slice)
   Γ ⊢ slice[axis=i, start=a, stop=b] x : Tensor[dt, sᵢ, R']
   where sᵢ = [d₁, ..., dᵢ₋₁, b−a, dᵢ₊₁, ..., dₖ]

The slice bounds a, b can be constants, shape variables, or Presburger expressions over shape variables. The bounds-check premise discharges via SMT. If the bounds are constants and the dimension is symbolic, the check might require the user to have asserted a lower bound on the symbolic dimension elsewhere.

Strided slicing (step ≠ 1) is deferred. Negative indices (-1 for last) are deferred — they're surface-syntax sugar for the symbolic form dᵢ − 1.

The output refinement set drops refinements mentioning dᵢ (since the new dimension is b−a, not dᵢ); refinements unrelated to the sliced axis survive.

13. Concat

Γ ⊢ x : Tensor[dt, [d₁, ..., dᵢ, ..., dₖ], R₁]
Γ ⊢ y : Tensor[dt, [d'₁, ..., d'ᵢ, ..., d'ₖ], R₂]
Γ ⊨ d_j = d'_j for all j ≠ i
─────────────────────────────────────────────────────────────  (concat)
   Γ ⊢ concat[axis=i] x y : Tensor[dt, sᵢ, R₁ ∧ R₂]
   where sᵢ = [d₁, ..., dᵢ + d'ᵢ, ..., dₖ]

All non-concat dimensions must match (SMT discharge). The concat axis sums. Variadic concat (concat[axis=i] x₁ ... xₙ) desugars to repeated binary concat, left-associated.

14. SMT discharge mechanics

Every operation rule above includes one or more Γ ⊨ φ premises. The compiler discharges these by:

1. Walking up the proof tree, collecting all refinements in scope (from input tensor types, function signatures' requires clauses, and explicitly bound predicates).
2. Asserting them as SMT constraints in a fresh Z3 context.
3. Asserting the negation of φ.
4. Checking satisfiability. If unsat, Γ ⊨ φ holds. If sat, the obligation fails and the user gets the counterexample. If unknown (timeout), the operation is rejected with a "could not prove" error.

The implementation will need a strategy for SMT timeouts. Options:

• Reject on timeout. Conservative, predictable, sometimes too strict.
• Accept on timeout with a warning. Permissive, documented as unsound, gates with a flag.
• Retry with simplified constraints. Drop refinements that aren't immediately relevant; retry. Heuristic but often enough.

Phase 0 commits to reject on timeout, with a 2-second timeout per discharge. Tunable; can be relaxed in later phases if it bites.

15. Resolved open issues from Section 1

Of the four open issues §9 listed, this section resolves three:

The fourth issue (refinement set canonicalization) becomes implementation work: any total order on predicates suffices; lexicographic on a normal form is the obvious choice. Section 5 (implementation) revisits.

16. New open issues

1. Operation overloading (resolved for Phase 0). add, mul, etc. admit multiple dtypes via admissibility tables (binOp(dt) ok, unaryOp(dt) ok, castOk). Phase 0 does not use typeclasses or user-defined overloading: the core IR has a fixed, small dtype set. Later phases: if user-defined dtypes or heavy overloading land, replace or augment tables with an explicit trait system — document the migration in an ADR.

2. mul and refinements (resolved). Clarified in §2.1: tensor mul is value-level; shape “multiplication” is the restricted type-level grammar. No separate issue.

3. Reduction over symbolic axes (accepted limitation). reduce[axis=i] requires i to be a compile-time literal in Phase 0. Workarounds: macros, metaprogramming, or duplicated specialized ops generated by the compiler for known static axes. Phase 7 surface may sugar common patterns. Extending the IR so axis is a non-literal compile-time expression is out of scope for Phase 0.

4. Numeric semantics of reduction. sum over FP values is order-dependent under floating-point arithmetic. The type system says nothing about reduction order; the runtime / lowering picks. This becomes a Phase 6 issue (reproducibility) and is not a type-system concern here.

5. Empty-tensor handling. With default α ≥ 1, the type system rules out tensors with a zero-sized dimension. Some valid programs want zero-sized intermediates (empty masks, no-op concat). Decision: opt-in via explicit refinement α ≥ 0 overriding the default. Documented.

17. Decisions, summarized

18. Section 3 preview

Section 3 commits to (see that section for the authoritative rules):

• Subtyping rules. When does Tensor[dt, s, R₁] <: Tensor[dt, s, R₂]? Same dt, same shape; R₁ ⇒ R₂ under SMT (Section 3 §3.3).
• Refinement implication. The bidirectional check between an inferred refinement set and an annotated one.
• Width vs. depth. No width subtyping for refinement sets; implication handles semantics (Section 3 §3.5).
• Coercions distinct from subtyping. Explicit IR operations (cast, broadcast, reshape, etc.) vs. refinement-only subtyping (Section 3 §2, §6).

The grammar from Section 1 and the operation typing from Section 2 are not expected to change in Section 3. If they do, that's evidence of a design issue worth revisiting.

19. Reference implementation (non-normative)

The rules above are normative for Phase 0. The OCaml compiler under compiler/ is a partial executable realization: structural shape checks plus Z3-backed dimension equality and reshape volume (volEq style) when symbols appear, with optional root (requires (= …) …) user equalities (Section 2 §14–§15); S-expression surface; MLIR lowering for a subset of the operation and cast tables in Sections 4–8. Full refinement discharge and every Γ ⊨ φ premise remain incomplete in the implementation.

For an enumerated mapping (binary/unary/reduce coverage, reshape behavior, test artifacts), see decisions/phase-0-reference-implementation-status.md. If that ADR and this section disagree on intended Phase 0 semantics, this section file wins until a spec amendment or ADR updates the contract.

End of Phase 0, Section 2.