Execute `ar1cs` functions in `tasm` target

[chancehudson]

The tasm target can support ar1cs based functions by wrapping them in assembly automatically. The key is automatically building the input variables in a structured way.

Consider this ar1cs function:

(a) -> (b)

b = (2*one) radix (1*a) # b is the square root of a

0 = (1*b) * (1*b) - (1*a) # assert that a = b*b

a and b are variables being constrained by the provided equations. one is equal to 1.

The value of a is defined by the caller. The value of b is defined by the current scope and returned.

This might be expressed by the compiler in tasm as so:

(_) -> _

# accept value a as an argument
# read value b from io
#
# constrain the relationship between
# the variables

divine 1

# _ a b
dup 0
swap 2

# _ b a b
dup 0
mul
eq
assert

return

[Sword-Smith]

Triton VM comes with a code generator for circuits evaluations. This code generator can output both Rust code and tasm (Triton VM assembly). You can find the code generator for tasm here.

It assumes that your inputs (a and b variables in your example) live in memory though. So the code generator will not produce code using the divine instruction.

This means that you just need to be able to compile your ar1cs definitions to the Constraints definition in Triton VM, and then Triton VM can do the rest.

[chancehudson]

Haha, i figured ya'll had thought of this already. Using memory is probably a better idea than using secret inputs. I was planning to extend the user input to support this, but I'll include this with memory pre-loading instead.

Two questions:

1. The pre-loaded memory is included in the program transcript (hash), correct?
2. (Below)

This means that you just need to be able to compile your ar1cs definitions to the Constraints definition in Triton VM, and then Triton VM can do the rest.

So to clarify, I can define a constraint between memory indices? An r1cs constraint should always be a (max) degree 2 polynomial so it should be possible to convert to a stark constraint.

I'm probably going to dig into implementing triton stuff in a couple weeks. I have some more immediate plans around integrating r1cs provers, and building an ide in a hackathon 🤞.

[Sword-Smith]

The first two transition constraints relating to the processor table in Triton VM are defined like so[^1]:

    pub fn transition_constraints(
        circuit_builder: &ConstraintCircuitBuilder<DualRowIndicator>,
    ) -> Vec<ConstraintCircuitMonad<DualRowIndicator>> {
        let constant = |c: u64| circuit_builder.b_constant(c);
        let curr_base_row = |col: ProcessorBaseTableColumn| {
            circuit_builder.input(CurrentBaseRow(col.master_base_table_index()))
        };
        let next_base_row = |col: ProcessorBaseTableColumn| {
            circuit_builder.input(NextBaseRow(col.master_base_table_index()))
        };

        // constraints common to all instructions
        let clk_increases_by_1 = next_base_row(CLK) - curr_base_row(CLK) - constant(1);
        let is_padding_is_0_or_does_not_change =
            curr_base_row(IsPadding) * (next_base_row(IsPadding) - curr_base_row(IsPadding));

        let instruction_independent_constraints =
            vec![clk_increases_by_1, is_padding_is_0_or_does_not_change];

So you specify relations between "current row" and "next row", and it's then implicit that these rows live somewhere in memory. Then when you generate the TASM code that evaluates all these AIR constraints, you specify where in memory these rows live, or, you specify that their position is only known at run-time, and the generated code will then read their positions from the stack and evaluate all constraints and store the result in memory.

So yeah, I guess it is somewhat like defining constraints between memory cells, but you get a lot more context. It's better to think of this as defining relations between inputs, which are the rows in your algebraic execution trace.

You can think of the ConstraintCircuitBuilder as a type in Rust that captures some of the capabilities of the ar1cs language.

[^1]: Code copied from (https://github.com/TritonVM/triton-vm/blob/master/triton-vm/src/table/processor_table.rs#L3844)

[chancehudson]

This is great, i didn't think it would be possible to define a constraint in such a concrete way.