Overview

Every specification carries a signature: a precise statement of what goes in, what comes out, and — where it matters — which values are hidden. The FHERMA Kernel Language is the notation signatures are written in.

Before a notation existed, that statement was prose and free-form JSON, which meant nothing about it could be checked — not by a tool, and not by the person implementing against it. A signature in the language is parsed, validated, and then everything else is derived from it mechanically: the types a testing bundle is written in, the skeleton an implementation starts from, the size of every buffer, the layout of every file on disk.

The shortest complete example

A kernel states the problem as generally as it is true:

kernel polymult<type T: Numeric, N: u32>(
    %a: tensor<N x T>,
    %b: tensor<N x T>,
) -> %c: tensor<N x T>

A specification refines it — settles the types, names the dimensions, adds whatever the representation needs:

spec rlwe 1.0.0 "Cyclotomic, at RLWE parameters" {
    kernel polymult<type T = i64, N: u32, L: u32, q: u32>(
        %a: tensor<N x L x T>,
        %b: tensor<N x L x T>,
    ) -> %c: tensor<N x L x T>
}

Both are the same grammatical production: a specification is a spec header wrapping a kernel declaration. What tells them apart is not syntax but how much they leave open — a kernel constrains its types, a specification settles them.

Parameters say what they are

type T declares a type parameter: bare, it is any type; type T: Numeric ranges over a class; type T = i64 is settled. N: u32 declares a value parameter, and a value is never written with = — a signature does not fix a number; a point does, when something is measured.

The two signs each mean one thing: : reads as ranges over and takes a set — a class for a type, a strict scalar type for a value. = reads as is and takes one concrete type.

Reading on

• Declarations — the full shape of kernel and spec.
• Types — scalars, tensors, dimensions, secret.
• Refinement — what a specification may and may not do.
• Diagnostics — what the tools refuse, and how they say it.
• Grammar — the notation formally.

The reference implementation is fherma-lang — a standalone Python package with no dependencies, and the single implementation of the language: the platform, the CLI and the editor all call it rather than keeping copies that could drift. See the fherma-lang tool.