feat(AVM): First version for mini AVM (ADD, RETURN, CALLDATACOPY) (#3439

)

First version of a mini AVM.

Resolves #3376
Resolves #3378
Resolves #3379 
Resolves #3380
Resolves #3320
Resolves #3321

---------

Co-authored-by: Maddiaa0 <[email protected]>

barretenberg/cpp/pil/avm/avm_mini.pil

@@ -0,0 +1,97 @@
+constant %N = 256;
+
+namespace avmMini(%N);
+
+    //===== CONSTANT POLYNOMIALS ==================================================
+    pol constant clk(i) { i };
+    pol constant first = [1] + [0]*; // Used mostly to toggle off the first row consisting
+                                     // only in first element of shifted polynomials.
+
+    //===== TABLE SUBOP-TR ========================================================
+    // Enum over sub operations
+    // 0: VOID
+    // 1: ADD
+    pol commit subop;
+
+    // Intermediate register values
+    pol commit ia;
+    pol commit ib;
+    pol commit ic;
+
+    // Memory operation per intermediate register
+    pol commit mem_op_a;
+    pol commit mem_op_b;
+    pol commit mem_op_c;
+
+    // Read-write flag per intermediate register: Read = 0, Write = 1
+    pol commit rwa;
+    pol commit rwb;
+    pol commit rwc;
+
+    // Memory index involved into a memory operation per pertaining intermediate register
+    // We should range constrain it to 32 bits ultimately. For first mini-AVM,
+    // we will assume that these columns are of the right type.
+    pol commit mem_idx_a;
+    pol commit mem_idx_b;
+    pol commit mem_idx_c;
+
+
+    // Track the last line of the execution trace. It does NOT correspond to the last row of the whole table
+    // of size N. As this depends on the supplied bytecode, this polynomial cannot be constant.
+    pol commit last;
+
+    // Relations on type constraints
+    subop * (1 - subop) = 0;
+    mem_op_a * (1 - mem_op_a) = 0;
+    mem_op_b * (1 - mem_op_b) = 0;
+    mem_op_c * (1 - mem_op_c) = 0;
+    rwa * (1 - rwa) = 0;
+    rwb * (1 - rwb) = 0;
+    rwc * (1 - rwc) = 0;
+
+    // Relation for addition over the finite field
+    subop * (ia + ib - ic) = 0;
+
+    // ========= Table MEM-TR =================
+    pol commit m_clk;
+    pol commit m_sub_clk;
+    pol commit m_addr;
+    pol commit m_val;
+    pol commit m_lastAccess; // Boolean (1 when this row is the last of a given address)
+    pol commit m_rw; // Enum: 0 (read), 1 (write)
+
+    // Type constraints
+    m_lastAccess * (1 - m_lastAccess) = 0;
+    m_rw * (1 - m_rw) = 0;
+
+    // m_lastAccess == 0 ==> m_addr' == m_addr
+    (1 - first) * (1 - m_lastAccess) * (m_addr' - m_addr) = 0;
+
+    // We need: m_lastAccess == 1 ==> m_addr' > m_addr
+    // The above implies: m_addr' == m_addr ==> m_lastAccess == 0
+    // This condition does not apply on the last row.
+    // clk + 1 used as an expression for positive integers
+    // TODO: Uncomment when lookups are supported
+    // (1 - first) * (1 - last) * m_lastAccess { (m_addr' - m_addr) } in clk + 1; // Gated inclusion check. Is it supported?
+
+    // TODO: following constraint
+    // m_addr' == m_addr && m_clk == m_clk' ==> m_sub_clk' - m_sub_clk > 0
+    // Can be enforced with (1 - first) * (1 - last) * (1 - m_lastAccess) { 6 * (m_clk' - m_clk) + m_sub_clk' - m_sub_clk } in clk + 1
+
+    // Alternatively to the above, one could require 
+    // that m_addr' - m_addr is 0 or 1 (needs to add placeholders m_addr values):
+    // (m_addr' - m_addr) * (m_addr' - m_addr) - (m_addr' - m_addr) = 0;
+    // if m_addr' - m_addr is 0 or 1, the following is equiv. to m_lastAccess
+    // (m_addr' - m_addr)
+
+    // m_lastAccess == 0 && m_rw' == 0 ==> m_val == m_val'
+    // This condition does not apply on the last row.
+    // Note: in barretenberg, a shifted polynomial will be 0 on the last row (shift is not cyclic)
+    // Note2: in barretenberg, if a poynomial is shifted, its non-shifted equivalent must be 0 on the first row
+
+    (1 - first) * (1 - last) * (1 - m_lastAccess) * (1 - m_rw') * (m_val' - m_val) = 0;
+
+    // TODO: Constraint the first load from a given adress has value 0. (Consistency of memory initialization.)
+    // TODO: when introducing load/store as sub-operations, we will have to add consistency of intermediate
+    // register values ia, ib, ic
+

barretenberg/cpp/pil/avm/avm_mini_opt.pil

@@ -0,0 +1,37 @@
+constant %N = 256;
+namespace avmMini(256);
+    col fixed clk(i) { i };
+    col fixed positive(i) { (i + 1) };
+    col fixed first = [1] + [0]*;
+    col witness subop;
+    col witness ia;
+    col witness ib;
+    col witness ic;
+    col witness mem_op_a;
+    col witness mem_op_b;
+    col witness mem_op_c;
+    col witness rwa;
+    col witness rwb;
+    col witness rwc;
+    col witness mem_idx_a;
+    col witness mem_idx_b;
+    col witness mem_idx_c;
+    col witness last;
+    (avmMini.subop * (1 - avmMini.subop)) = 0;
+    (avmMini.mem_op_a * (1 - avmMini.mem_op_a)) = 0;
+    (avmMini.mem_op_b * (1 - avmMini.mem_op_b)) = 0;
+    (avmMini.mem_op_c * (1 - avmMini.mem_op_c)) = 0;
+    (avmMini.rwa * (1 - avmMini.rwa)) = 0;
+    (avmMini.rwb * (1 - avmMini.rwb)) = 0;
+    (avmMini.rwc * (1 - avmMini.rwc)) = 0;
+    (avmMini.subop * ((avmMini.ia + avmMini.ib) - avmMini.ic)) = 0;
+    col witness m_clk;
+    col witness m_sub_clk;
+    col witness m_addr;
+    col witness m_val;
+    col witness m_lastAccess;
+    col witness m_rw;
+    (avmMini.m_lastAccess * (1 - avmMini.m_lastAccess)) = 0;
+    (avmMini.m_rw * (1 - avmMini.m_rw)) = 0;
+    (((1 - avmMini.first) * (1 - avmMini.m_lastAccess)) * (avmMini.m_addr' - avmMini.m_addr)) = 0;
+    (((((1 - avmMini.first) * (1 - avmMini.last)) * (1 - avmMini.m_lastAccess)) * (1 - avmMini.m_rw')) * (avmMini.m_val' - avmMini.m_val)) = 0;

barretenberg/cpp/pil/fib/fibonacci.pil

@@ -0,0 +1,18 @@
+constant %N = 16;
+
+// This uses the alternative nomenclature as well.
+
+namespace Fibonacci(%N);
+    col fixed LAST(i) { match i {
+        %N - 1 => 1,
+        _ => 0,
+    } };
+    col fixed FIRST(i) { match i {
+        0 => 1,
+        _ => 0,
+    } };
+    col witness x, y;
+
+    (1-FIRST) * (1-LAST) * (x' - y) = 0;
+    (1-FIRST) * (1-LAST) * (y' - (x + y)) = 0;
+

barretenberg/cpp/pil/fib/fibonacci_opt.pil

@@ -0,0 +1,8 @@
+constant %N = 16;
+namespace Fibonacci(16);
+    col fixed LAST(i) { match i { (%N - 1) => 1, _ => 0, } };
+    col fixed FIRST(i) { match i { 0 => 1, _ => 0, } };
+    col witness x;
+    col witness y;
+    (((1 - Fibonacci.FIRST) * (1 - Fibonacci.LAST)) * (Fibonacci.x' - Fibonacci.y)) = 0;
+    (((1 - Fibonacci.FIRST) * (1 - Fibonacci.LAST)) * (Fibonacci.y' - (Fibonacci.x + Fibonacci.y))) = 0;

barretenberg/cpp/src/CMakeLists.txt

@@ -76,6 +76,7 @@ add_subdirectory(barretenberg/sumcheck)
 add_subdirectory(barretenberg/transcript)
 add_subdirectory(barretenberg/translator_vm)
 add_subdirectory(barretenberg/ultra_honk)
+add_subdirectory(barretenberg/vm)
 add_subdirectory(barretenberg/wasi)