Syntax

This page covers the complete syntax of the Lof language.

Comments

Single-line comments start with //:

// This is a comment
let x = 42  // Comment after code

Top-Level Declarations

Proof Definitions

Proofs are the top-level construct in Lof. They define a complete ZK circuit.

proof ProofName {
    // Signal declarations
    input x: field;
    witness secret: field;
    witness result: field;

    // Proof body (constraints and computations)
    assert x > 0;
    assert result === x + secret
}

Component Definitions

Reusable circuit components (like functions, but for circuits):

component Square {
    input x: field;
    witness y: field;

    {
        assert y === x * x;
        y
    }
}

Using Components in Proofs

component Multiplier {
    input a: field;
    input b: field;
    witness c: field;

    {
        assert c === a * b;
        c
    }
}

proof UseMultiplier {
    witness x: field;
    witness y: field;
    witness result: field;

    // Instantiate component
    assert result === Multiplier(x)(y)
}

Signal Declarations

Signals represent wires in the circuit. Two visibility levels:

input publicValue: field;      // Public input
witness privateData: field;    // Private witness (secret)

Each signal declaration must end with a semicolon.

Types

Primitive Types

field     // Finite field element
bool      // Boolean
nat       // Natural number

Compound Types

array<field, 10>              // Fixed-size array
(field, bool)                 // Tuple (2 elements)
(field, field, bool)          // Tuple (3 elements)

Type Identifiers

MyCustomType                  // User-defined type identifier

Refined Types

Refined types allow you to annotate types with predicates (currently accepted by type checker but predicates must be manually asserted):

witness x: refined { field, x > 0 && x < 100 };

// You must manually assert the refinement predicate
assert x > 0 && x < 100

Function Definitions

Functions are defined at the top level using let:

let functionName (param1: Type1) (param2: Type2): ReturnType =
    expression

Functions are curried by default:

let add (x: field) (y: field): field = x + y

let increment = add(1)  // Partial application
let five = increment(4)  // Returns 5

Let Bindings

Bind values within expressions:

let pattern = value in body

Examples:

let x = 42 in x + 10

let (a, b) = (1, 2) in a + b

let result = computeSomething() in
    assert result > 0

Important: Let-bound variables used in proof body return values must be constrained, or the typechecker will reject them.

Pattern Matching

Match expressions use match...with syntax:

match expression with
| pattern1 => result1
| pattern2 => result2
| pattern3 => result3

Pattern Types

Variable Pattern:

match x with
| value => value + 1

Tuple Pattern:

match pair with
| (a, b) => a + b

Literal Pattern:

match x with
| 0 => "zero"
| 1 => "one"
| n => "other"

Wildcard Pattern:

match x with
| 42 => "special"
| _ => "default"

Pattern Matching Notes

• Patterns can be separated by | or placed on consecutive lines
• The with keyword is required after the match expression
• Each pattern must have exactly one corresponding expression after =>

Expressions

Literals

42              // Number literal

Variables

variableName

Function Calls

functionName(arg1)(arg2)(arg3)   // Multiple arguments
singleArg(x)                      // Single argument

Tuples

()                    // Unit/empty tuple
(1, 2)               // 2-tuple
(a, b, c)            // 3-tuple

Binary Operations

Arithmetic:

x + y
x - y
x * y
x / y  // Division requires proof that divisor is non-zero

Comparison:

x == y      // Equality
x != y      // Inequality
x < y       // Less than
x > y       // Greater than
x <= y      // Less than or equal
x >= y      // Greater than or equal

Logical:

a && b      // AND
a || b      // OR
!x          // NOT

Constraint Equality:

x === y     // Circuit constraint (assert x equals y)

Operator Precedence

From lowest to highest:

1. Constraint assertion ===
2. Comparison ==, !=, <, >, <=, >=
3. Addition/Subtraction +, -
4. Multiplication/Division *, /

Use parentheses to override precedence: (a + b) * c

Assertions

assert condition

Example:

assert balance >= amount;
assert x > 0 && x < 100

Blocks

Group multiple statements:

{
    statement1;
    statement2;
    finalExpression
}

The last expression in a block is its value (no semicolon).

Complete Example

// Function definition
let square (x: field): field = x * x

// Proof with working features
proof RangeCheck {
    input value: field;
    witness is_small: field;

    // Compute and constrain result
    let check = value < 256 in
    assert is_small === check
}

Keywords

Reserved keywords in Lof:

proof       component     type        enum
input       witness
field       nat           bool
match       with
assert      let           in
refined

Symbols and Operators

{ }         Braces
( )         Parentheses
[ ]         Brackets
< >         Angle brackets (comparison)

=>          Fat arrow (pattern matching)
|           Pipe (pattern separator)

:           Colon (type annotation)
;           Semicolon (statement terminator)
,           Comma (separator)
.           Dot
..          Range

=           Assignment
===         Constraint equality
==          Equality comparison
!=          Not equal
<           Less than
>           Greater than
<=          Less than or equal
>=          Greater than or equal

+           Addition
-           Subtraction
*           Multiplication
/           Division

!           Logical NOT
&&          Logical AND
||          Logical OR

_           Wildcard pattern

Syntax Rules

1. Statements within proofs must end with semicolons (except the final expression)
2. Signal declarations always require semicolons
3. Pattern arms in match expressions use => not =
4. Function parameters are enclosed in separate parentheses: (x: T) (y: U)
5. Type annotations use : followed by the type

Important Type System Features

Division Safety

Division requires proof that the divisor is non-zero:

proof SafeDivision {
    witness numerator: field;
    witness denominator: field;
    witness result: field;

    // Must prove denominator is non-zero
    assert denominator != 0;

    // Now division is safe
    assert result === numerator / denominator
}

Boolean Constraints

The bool type automatically generates constraints ensuring values are 0 or 1:

proof BooleanLogic {
    witness flag: bool;  // Automatically constrained: flag * (1 - flag) === 0
    input value: field;
    witness result: field;

    assert result === flag * value
}

Unconstrained Witness Detection

All witnesses must be used in at least one constraint:

proof BadExample {
    witness x: field;
    witness y: field;

    assert y === 42  // ERROR: x is unconstrained!
}

Next Steps

• Types - Learn about Lof’s type system
• Operations - Detailed operator reference
• Data Types - Working with Field, arrays, tuples
• Tutorial - Practice with examples