Specification

Kina Application Binary Interface (ABI) Stability Policy

This document outlines the ABI conventions for the Kina programming language, focusing on Phase 1 FFI boundaries, MLIR lowering expectations, and Algebraic Effects handlers.

1. Stability Guarantees

Kina is currently in early prototype stages (Phase 1). No stable ABI is guaranteed. Code authored against internal structures or FFI methods must expect breakage.

When stability is eventually introduced, boundaries will be marked explicitly:

#[stable] — Guaranteed not to break without a major version bump.
#[unstable] — Internal APIs subject to change without notice.

2. Compiler to Runtime Boundary (MLIR FFI)

The Kina compiler emits textual MLIR, lowering higher-order tensor operations to Standard, Linalg, and Arith dialects. Lowering to the LLVM dialect bridges the gap to the Rust runtime by relying on MLIR's _mlir_ciface C-ABI conventions.

Tensor and MemRef Layout

Kina tensor<T, [...]> types lower to MLIR memref<...xT>. When passing memrefs across the FFI boundary, they are wrapped in an MLIR C-Interface compatible struct.

For an unranked memref (used dynamically), the struct layout corresponds to:

struct StridedMemRefType<T, N> {
  T *basePtr;
  T *data;
  int64_t offset;
  int64_t sizes[N];
  int64_t strides[N];
};

When functions specify memref<*T> (unranked memref), the C ABI expects:

struct UnrankedMemRefType<T> {
  int64_t rank;
  void *descriptor;
};

Runtime Exported Functions

The Kina Rust runtime provides implementations for core operations (CPU and GPU) and exposes them using extern "C". The MLIR module defines them as private functions with the llvm.emit_c_interface attribute.

Memory Operations:

_mlir_ciface_runtime_copy_to_device_f32(memref<*f32>, memref<*f32>, i32) -> i32
_mlir_ciface_runtime_copy_to_device_f16(memref<*f16>, memref<*f16>, i32) -> i32
_mlir_ciface_runtime_copy_to_host_f32(memref<*f32>, memref<*f32>) -> i32

Compute Operations (GPU):

_mlir_ciface_runtime_gpu_matmul_f32(memref<*f32> out, memref<*f32> a, memref<*f32> b) -> i32
_mlir_ciface_runtime_gpu_gather_f32(memref<*f32> out, memref<*f32> values, memref<*i64> indices) -> i32
_mlir_ciface_runtime_gpu_softmax_f32(memref<*f32> out, memref<*f32> x, i32 axis) -> i32
_mlir_ciface_runtime_gpu_repeat_interleave_f32(memref<*f32> out, memref<*f32> x, i32 axis, i32 reps) -> i32

All FFI compute functions return an i32 status code:

0 indicates Success.
Non-zero indicates an execution error (e.g., CUDA launch failure).

3. Algebraic Effects and Fibers

Phase 2 will introduce Algebraic Effects for implementing Autograd tapes. The runtime uses stackful coroutines (fibers) for this capability. The ABI specifies the following C-exported functions:

kina_push_handler: Pushes an effect handler onto the current fiber's stack.
kina_pop_handler: Pops the current effect handler.
kina_get_perform_id: Identifies the effect that triggered the continuation.
kina_resume_fiber: Resumes the suspended fiber with the given continuation arguments.

These bindings rely strictly on the extern "C" calling convention and require that no panics cross the FFI boundary from Rust to OCaml or MLIR-compiled code.