Type Annotations

Optional type annotations for circuit variables, functions, and bindings.

Achronyme supports gradual typing in circuits. You can add optional type annotations to declarations, bindings, and functions. Unannotated code works exactly as before — annotations are strictly opt-in.

Type Universe

Four types are available in circuit context:

Bool is a subtype of Field — a boolean value can be used anywhere a field element is expected. The reverse is an error unless the value is a proven boolean (e.g., a comparison result or constant 0/1).

Field and Bool are not keywords. They are contextual identifiers recognized only after : or ->. You can still use Field and Bool as variable names in regular code.

Input Declarations

Add : Type after the parameter name in the circuit signature. Use Public or Witness visibility before the type:

circuit typed_inputs(root: Public Field, flag: Witness Bool, secret: Witness Field, path: Witness Field[3], indices: Witness Bool[3]) {
    // circuit body
}

Without annotations, inputs default to untyped — same behavior as before:

circuit untyped_inputs(root: Public, secret: Witness) {
    // circuit body
}

Both forms can coexist in the same circuit:

circuit mixed_inputs(root: Public Field, leaf: Witness, path: Witness Field[3], indices: Witness) {
    // circuit body
}

Let Bindings

Annotate local bindings with : Type after the name, before =:

circuit let_bindings(a: Witness Field, b: Witness Field) {
    let product: Field = a * b
    let is_equal: Bool = a == b
}

The compiler handles annotations depending on the expression’s inferred type:

• Typed expression matches annotation: No extra cost. let eq: Bool = a == b is free because == already produces Bool.
• Typed expression conflicts: Error. let x: Bool = a + 1 fails because + produces Field, which is incompatible with Bool.
• Untyped expression with : Bool: The compiler emits a RangeCheck(v, 1) constraint to enforce v * (1 - v) = 0, costing 1 extra constraint. This is necessary for soundness — without enforcement, a malicious prover could assign any value.
• Untyped expression with : Field: No enforcement needed. Field is the default and doesn’t restrict the value space.

circuit mismatch_example(a: Witness Field) {
    // Error: type annotation mismatch for `x`: declared as Bool,
    //        but expression has type Field
    let x: Bool = a + 1
}

circuit enforced_bool(w: Witness) {
    // Enforced: emits RangeCheck(w, 1) — costs 1 constraint
    let b: Bool = w
}

Arithmetic operations (+, -, *, /, ^) produce Field. Comparisons and logical operations (==, !=, <, <=, >, >=, &&, ||, !) produce Bool.

Array Bindings

For array annotations, the compiler validates that the array length matches the declared size:

circuit array_length_error(x: Witness, y: Witness) {
    // Error: array length mismatch: expected 3, got 2
    let a: Field[3] = [x, y]
}

Bool[N] annotations enforce each untyped element individually (1 constraint per element):

circuit bool_array_enforcement(x: Witness, y: Witness) {
    // Enforced: emits RangeCheck for each untyped element — costs 2 constraints
    let flags: Bool[2] = [x, y]
}

Functions

Annotate parameters with : Type and return types with -> Type:

circuit with_functions(a: Witness Field, b: Witness Field) {
    fn hash_pair(a: Field, b: Field) -> Field {
        poseidon(a, b)
    }

    fn is_valid(x: Field, y: Field) -> Bool {
        x == y
    }

    let h = hash_pair(a, b)
    let valid = is_valid(a, b)
}

Mixed typed and untyped parameters are allowed:

circuit mixed_params(a: Witness Field, b: Witness) {
    fn scale(x: Field, factor) {
        x * factor
    }

    let result = scale(a, b)
}

The compiler checks that arguments match the declared parameter types at each call site:

circuit call_site_check(a: Witness Field) {
    fn double(x: Field) -> Field { x + x }

    let result: Field = double(a)    // ok
}

Bool Enforcement on Parameters and Return Types

When a : Bool parameter receives an untyped argument, the compiler emits a RangeCheck to enforce the boolean constraint (1 extra constraint per untyped argument):

circuit bool_param_enforcement(w: Witness) {
    fn check(b: Bool) { assert(b) }
    check(w)     // emits RangeCheck(w, 1) — 1 extra constraint
}

Similarly, when a function with -> Bool return type produces an untyped body result, the compiler enforces boolean on the return value:

circuit bool_return_enforcement(w: Witness) {
    fn to_flag(x: Field) -> Bool { x }
    let f = to_flag(w)    // emits RangeCheck on return value — 1 extra constraint
}

If the argument or return value already has a proven type (e.g., from a comparison), no extra constraint is emitted.

Subtyping: Bool as Field

Bool values can be used in arithmetic (field) context. This is safe because booleans are 0 or 1 in the field:

circuit bool_subtyping(flag: Witness Bool) {
    // Bool used in arithmetic — allowed (Bool is subtype of Field)
    let as_field: Field = flag + flag
}

The reverse depends on the source value’s type:

• Typed as Field: Error. A value explicitly typed as Field cannot be narrowed to Bool:

  circuit field_to_bool_error(x: Witness Field) {
      // Error: x is Field, cannot annotate as Bool
      let b: Bool = x
  }

• Untyped: Enforcement. The compiler emits RangeCheck(x, 1) to enforce x * (1 - x) = 0 (1 constraint):

  circuit untyped_enforcement(x: Witness) {
      // Enforced: emits RangeCheck — 1 extra constraint
      let b: Bool = x
  }

• Already proven boolean: Free. No extra constraint is emitted:

  circuit proven_boolean(a: Witness Field, b: Witness Field) {
      // Comparison result is a proven boolean — annotation is free
      let eq: Bool = a == b
  }

Constraint Savings

Annotating an input as : Bool emits a one-time RangeCheck enforcement constraint (v * (1-v) = 0) at the declaration site. This enforced boolean status propagates through bool_prop, allowing all downstream uses to skip redundant boolean enforcement. The net effect is a saving when the variable is used multiple times in boolean context.

// Without annotation: each mux adds 1 boolean enforcement for cond
circuit no_annotation(cond: Witness, a: Witness, b: Witness, c: Witness, d: Witness) {
    let r1 = mux(cond, a, b)   // 2 constraints (1 enforcement + 1 selection)
    let r2 = mux(cond, c, d)   // 2 constraints (1 enforcement + 1 selection)
    // Total: 4 constraints
}

// With annotation: 1 enforcement at declaration, downstream skips
circuit with_annotation(cond: Witness Bool, a: Witness, b: Witness, c: Witness, d: Witness) {
    // cond declared as Bool — 1 constraint (RangeCheck enforcement)
    let r1 = mux(cond, a, b)   // 1 constraint (selection only, enforcement skipped)
    let r2 = mux(cond, c, d)   // 1 constraint (selection only, enforcement skipped)
    // Total: 3 constraints (saved 1)
}

This optimization is applied by the bool_prop pass, which tracks proven-boolean variables through the program. The pass recognizes these sources as proven-boolean:

• Constants 0 and 1
• Comparison results (==, !=, <, <=, >, >=)
• RangeCheck(x, 1) results (including those emitted by : Bool enforcement on declarations, let bindings, function params, and return types)
• Assert operands and results
• Not/And/Or/Mux of proven-boolean operands

Enforcement vs. Savings

All : Bool annotations emit enforcement constraints for soundness. The cost is one-time per variable; downstream uses benefit from bool_prop savings.

The enforcement cost is a one-time soundness guarantee. Downstream uses of the enforced variable benefit from bool_prop savings.

Complete Example

A fully typed Merkle membership proof:

circuit merkle_proof(root: Public Field, leaf: Witness Field, path: Witness Field[3], indices: Witness Bool[3]) {
    merkle_verify(root, leaf, path, indices)
}

The same circuit with typed helper functions:

circuit hash_chain_verify(expected: Public Field, a: Witness Field, b: Witness Field, c: Witness Field) {
    fn hash_chain(x: Field, y: Field, z: Field) -> Field {
        let h: Field = poseidon(x, y)
        poseidon(h, z)
    }

    let result: Field = hash_chain(a, b, c)
    assert_eq(result, expected)
}

Quick Reference

Errors

VM Mode

Type annotations work in both circuit and VM modes. In circuit mode they generate constraints (as described above). In VM mode they produce compile-time warnings when the annotation doesn’t match the value:

W006: Type Mismatch

Emitted when a literal value’s type doesn’t match the annotation:

let x: Bool = 0p42    // W006: type annotation `Bool` on `x` does not match value type `Field`
let y: Field = "hello" // W006: type annotation `Field` on `y` does not match value type `String`

The code still runs — the VM is dynamically typed and annotations are advisory. But the warning catches potential bugs early.

W007: Array Size Mismatch

Emitted when an array literal has a different length than the annotation:

let a: Field[3] = [1, 2]  // W007: type `Field[3]` expects 3 elements, but array has 2

What Is Not Checked

Warnings are only emitted for literal values that can be statically analyzed. Dynamic expressions (function calls, variable references, binary operations) are not checked:

let x: Bool = f()   // No warning — return type of f() is unknown at compile time
let y: Field = a + b // No warning — expression type depends on runtime values

Recommendation

Use type annotations in VM code to:

• Document intent — make it clear that a variable holds a field element vs a boolean
• Catch typos — assigning a string to a : Field binding is immediately flagged
• Prepare for circuits — annotated VM code transitions to circuit mode with zero changes
• Help prove blocks — array annotations like Field[N] enable automatic array capture in prove(name: Public) blocks