Links

Links enable a constrained machine to call into another machine. They are defined by a call to an operation, where inputs and outputs are expressions. An optional boolean flag restricts the rows in which the link is active. Links without a boolean flag are active in every row.

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

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

    // Links without a flag are active on every row.
    // - constrain the values of `x`, `y`, and `n` so that `n = adder.add(x, y)`
    link => n = adder.add(x, y);
    // - constrain the values of `z`, `w`, and `m` so that `m = adder.add(z, w)`
    link => m = adder.add(z, w);
    // - constrain the values of `m`, `n` and `r` so that `r = adder.add(m,n)`
    link => r = adder.add(m, n);

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

If a boolean flag is given, the link is only active in rows where the flag evaluates to 1. Whenever a link is active, the columns mapped as inputs and outputs are constrained by the operation implementation. The following example demonstrates how to use links with flags.

col fixed odd_row = [0,1]*;

link if odd_row => z = submachine.foo(x, y); // active on odd rows only
link if (1 - odd_row) => z = submachine.bar(x, y); // active on even rows only