Functions in Circuits

How functions work inside circuit compilation.

Functions in circuits use the same fn syntax as regular Achronyme code, but they behave differently under the hood — every call is inlined.

Syntax

Define functions the same way as in regular mode:

fn double(x) {
    x + x
}

Functions can include type annotations on parameters and return types:

fn double(x: Field) -> Field {
    x + x
}

Call them as usual:

circuit double_demo(vals: Witness[3]) {
    fn double(x) { x + x }
    assert_eq(double(vals[0]), vals[0] + vals[0])
}

Inlining

There is no function call stack in circuits. Every call site expands the function body with the arguments substituted in. If you call a function 5 times, its body is compiled 5 times.

circuit square_demo(vals: Witness[3]) {
    fn square(x) { x * x }

    // Each call inlines independently — 1 constraint each
    let a = square(vals[0])
    let b = square(vals[1])
    let c = square(vals[2])
}

This means functions are a convenience for code organization, not a mechanism for reducing constraint count.

Constraint Cost

The cost of a function call equals the sum of its body’s constraints, plus any type enforcement costs. A function with two multiplications costs 2 constraints per call.

fn dot(a0, a1, b0, b1) {
    a0 * b0 + a1 * b1      // 2 constraints (two variable multiplications)
}

Calling dot three times produces 6 constraints.

Type Enforcement Costs

When a function has typed parameters or a return type, the compiler may emit additional constraints:

: Bool parameter with untyped argument: +1 constraint per parameter (emits RangeCheck(arg, 1))
-> Bool return with untyped body result: +1 constraint (emits RangeCheck(result, 1))
Already-typed arguments/results that match: No extra cost

circuit type_cost_demo(w: Witness, b: Witness Bool) {
    fn check(b: Bool) { assert(b) }    // body: 2 constraints (assert)

    check(w)                            // total: 2 + 1 = 3 constraints (1 for param enforcement)
    check(b)                            // total: 2 constraints (no enforcement needed)
}

Restrictions

Restriction	Error	Reason
No recursion	`RecursiveFunction`	Functions are inlined — recursion would loop forever
No closures	—	No runtime environment to capture
No higher-order functions	—	Cannot pass functions as circuit values
No anonymous functions	—	Only named `fn` definitions are supported
Type mismatch	`AnnotationMismatch`	Argument type doesn’t match typed parameter (e.g., `Field` arg to `Bool` param)
Bool enforcement	—	Untyped arg to `: Bool` param emits `RangeCheck` (+1 constraint)

Functions in circuits are purely a compile-time mechanism. They cannot capture variables from outer scopes (except declared inputs), cannot be passed as values, and cannot call themselves.

Example

A complete circuit using a helper function:

circuit sum_and_double(expected_sum: Public, vals: Witness[3]) {
    let acc = vals[0]
    let acc = acc + vals[1]
    let acc = acc + vals[2]
    assert_eq(acc, expected_sum)

    let n = len(vals)
    assert_eq(n, 3)

    fn double(x) { x + x }
    assert_eq(double(vals[0]), vals[0] + vals[0])
}