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 pip install fherma, which brings this package along — the command line tool is built on it. Install it directly when you want the language and nothing else: a server validating a signature, an editor, a build step.

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<T: Numeric, N: uint>(
    %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<T: i64, N: uint, L: uint, q: uint>(
        %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 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          i64
    N          uint
    L          uint
    q          uint
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
              ^
  Classes are Numeric, Integer, Real. Types are i8…i64, f8…f64, index, uint, int, real.

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        3729  generated
    generate.py       558  yours
    oracle.py         504  yours
    verify.py         625  yours
    README.md         889  generated

fherma.py holds the types derived from the signature — Point, Inputs, Outputs — along with the deterministic Stream and the codec. 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

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

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 <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