Functions

Functions are the entry points to a virtual machine. They can be called from another machine or from the outside.

In this section, we describe functions with this simple virtual machine:

machine Machine with degree: 16 {
    reg pc[@pc];
    reg X[<=];
    reg Y[<=];
    reg Z[<=];
    reg CNT;
    reg A;
    reg B;

    // an instruction to assert that a number is zero
    instr assert_zero X {
        X = 0
    }

    // an instruction to jump to a label
    instr jmp l: label {
        pc' = l 
    }

    // an instruction to jump to a label iff `X` is `0`, otherwise continue
    instr jmpz X, l: label { 
        pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) 
    }
    
    // an instruction to return the square of an input as well as its double
    instr square_and_double X -> Y, Z {
        Y = X * X,
        Z = 2 * X
    }

    function main {
        // initialise `A` to 2
        A <=X= 2;
        // initialise `CNT` to `3`
        CNT <=X= 3;
        start:
        // if `CNT` is `0`, jump to `end`
        jmpz CNT, end;
        // decrement `CNT`
        CNT <=X= CNT - 1;
        // get the square and the double of `A`
        A, B <== square_and_double(A);
        // jump back to `start`
        jmp start;
        end:
        // check that `A == ((2**2)**2)**2`
        assert_zero A - ((2**2)**2)**2;
        // check that `B == ((2**2)**2)*2`
        assert_zero B - ((2**2)**2)*2;
        return;
    }

    // some superpowers on `X` to allow us to check if it's 0
    col witness XInv;
    col witness XIsZero;
    XIsZero  = 1 - X * XInv;
    XIsZero * X = 0;
    XIsZero * (1 - XIsZero) = 0;
}

Function inputs and outputs

Function inputs and outputs are not supported yet

Statements

Labels

Labels allow referring to a location in a function by name.

        start:

Assignments

Assignments allow setting the values of some write registers to the values of some expressions expression using assignment registers.

        CNT <=X= 3;

If the right-hand side of the assignment is an instruction, assignment registers can be inferred and are optional:

        A, B <== square_and_double(A);

This will be inferred to be the same as A, B <=Y, Z= square_and_double(A); from the definition of the instruction:

    instr square_and_double X -> Y, Z {
        Y = X * X,
        Z = 2 * X
    }

Instructions

Instructions which do not return outputs can be used as statements.

        assert_zero A - ((2**2)**2)**2;