Links

Links enable a constrained machine to call into another machine. They are defined by a boolean flag and a call to the operation, where inputs and outputs are expressions.

machine Add4 with
    latch: latch,
    operation_id: operation_id
{
    Add adder;

    operation add4<0> x, y, z, w -> r;

    // - on every row (the boolean flag is `1`)
    // - constrain the values of `x`, `y`, and `n` so that `n = adder.add(x, y)`
    link 1 => adder.add x, y -> n;
    // - constrain the values of `z`, `w`, and `m` so that `m = adder.add(z, w)`
    link 1 => adder.add z, w -> m;
    // - constrain the values of `m`, `n` and `r` so that `r = adder.add(m,n)`
    link 1 => adder.add m, n -> r;

    col fixed operation_id = [0]*;
    col fixed latch = [1]*;

    col witness x;
    col witness y;
    col witness z;
    col witness w;
    col witness r;
    col witness m;
    col witness n;
}

machine Add with
    latch: latch
{
    // operation name, with column names as inputs and outputs
    operation add a, b -> c;

    col fixed latch = [1]*;

    col witness a;
    col witness b;
    col witness c;

    // constraint "implementing" the operation
    c = a + b;
}

A link is only active in rows where the boolean flag is 1 (all lines in the above example). Whenever it is active, the columns mapped as inputs and outputs are constrained by the operation implementation.