fherma-lang

FHERMA Kernel Language: lexer, parser and emitters. A standalone package — text in, structure out. It knows nothing about any platform, has no dependencies, and is what everything else builds on: the fherma command line tool, a server, a build script, an editor.

pip install fherma-lang

Most people arrive through the command line tool, which is built on this package and brings it along: pipx install fherma. Install this one directly when you want the language and nothing else — a server validating a signature, an editor, a build step — and then it belongs in the environment that imports it.

The language in one example

A kernel states a computational problem as generally as it is true. A specification refines it: it settles the types, names the dimensions and adds whatever the representation needs.

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

spec rlwe 1.0.0 "Cyclotomic, at RLWE parameters" {
    kernel poly_mult<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>
}

A parameter says what it is. type T is a type left open; type T: Numeric ranges over a class; type T = i64 is settled. N: u32 is a value, and a value is never written with = — a signature does not fix a number, a point does.

A parameter may also be derived — computed from others rather than set:

L: u32 = W / 32              a relation the language folds
q: tensor<L x u32> (N, W)    a value a bundle getter returns, handed N and W

An expression the language folds (= …, over + - * /, / keeping counts whole) states a relation: a signature still fixes no number, but it may say that one count follows from another, so L can size a tensor. A dependency list ((N, W)) says only that q follows from N and W; the rule that computes it — a prime search, a table — lives in the bundle, because it is code rather than arithmetic. A derived parameter may be a tensor, so a wide value like a modulus is held as limbs. Either way the point resolves to a value the generator, the oracle and the solution all read.

Both are the same production: a specification is a header wrapping a kernel declaration. What tells them apart is not syntax but how much they leave open.

Reading a declaration

$ fherma-lang parse sig.fhk
specification  rlwe 1.0.0
               Cyclotomic, at RLWE parameters
refines kernel poly_mult
parameters
    T          type = i64
    N          : u32
    L          : u32
    q          : u32
arguments
    %a         tensor<N x L x T>
    %b         tensor<N x L x T>
results
    %c         tensor<N x L x T>

--json prints the parse result for another tool to consume, and it can be fed straight back in — see below.

Failures carry a code from the specification of the language, the place, and something to do about it:

$ fherma-lang parse bad.fhk
E-TYPE-1: Field is neither a class nor a type of this language
  line 1, column 13
  kernel f<T: Field>(%x: T) -> %y: T
              ^
  A value parameter takes a strict scalar type — i8..i64, u8..u64, f32, f64 —
  so its width on every wire is fixed. Classes are Numeric, Integer, Real;
  types are i8, i16, i32, i64, u8, u16, u32, u64, f32, f64.

Emitting a scaffold

A scaffold is a pure function of a declaration: the same signature always gives the same tree, which is what lets a command line tool and a web button hand out identical bundles without coordinating.

$ fherma-lang emit --testing sig.fhk
testing scaffold in poly_mult-rlwe-1.0.0
    fherma.py        5247  generated
    main.py         10089  generated
    generate.py       558  yours
    oracle.py         504  yours
    verify.py         625  yours
    README.md        1749  generated
    vectors/       (empty)
    assets/        (empty)

fherma.py holds the types derived from the signature — Point, Inputs, Outputs — along with the deterministic Stream and the codec. main.py is the bundle's command line: make writes a point's cases and the expected answers, verify judges what a solution left behind, info describes the bundle as JSON. The three stubs are where an author writes the generator, the oracle and the verifier.

Name the parts to scaffold one or two of them:

fherma-lang emit --testing sig.fhk --oracle --verifier

The other kind of scaffold is a solution — the skeleton for answering a specification, in Python, C++ or Rust. The author's file is solve and its three functions init, run, free; the types, the protocol loop and the build file are generated from the same signature:

fherma-lang emit --solution sig.fhk --lang cpp

Either a declaration or a stored parse result will do; the tool tells them apart by looking at the first character, and does the rest:

fherma-lang parse --json sig.fhk > parsed.json
fherma-lang emit --testing parsed.json --out ./bundle

The closed vocabularies — scalar types with their widths and signedness, the value types a parameter may range over, and which scalars satisfy which class — are printed by fherma-lang vocabulary as JSON, so anything with a type picker can ask instead of keeping a copy that goes stale.

As a library

from fherma_lang import emit, parse

declaration = parse(open("sig.fhk").read())
for file in emit(declaration, kind="testing", parts=["oracle"]):
    print(file.path, file.generated)

from fherma_lang import reference                    # "poly_mult/rlwe@1.0.0"
from fherma_lang.serde import from_plain, to_plain   # a declaration to JSON and back

reference is what a declaration calls itself, and there is one definition of it because more than one thing depends on the exact string: it keys the deterministic stream, and a bundle records it as its own origin.

What is refused, and why

A scaffold needs every parameter settled, because there is no honest Python type for an open one. This is about abstraction, not about the shape of the declaration: a kernel that pins all of its parameters scaffolds fine.

E-SPEC-3: parameter T is constrained to Numeric rather than settled
  A class admits many types; pick one, as in type T = i64.

Secrecy is a different matter. Where a signature hides a value, the scaffold sees through it: the generator and the oracle always work in cleartext, since encryption — where there is any — happens between them and the run.

Exit codes

0  done          1  the declaration was rejected          2  called wrongly