Skip to content

Commit e534204

Browse files
authored
feat(avm-mini): call and return opcodes (AztecProtocol#3704)
closes: AztecProtocol#3697
1 parent 739fe90 commit e534204

18 files changed

+821
-133
lines changed

barretenberg/cpp/pil/avm/avm_mini.pil

+56-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,18 @@ namespace avmMini(256);
77
pol constant clk(i) { i };
88
pol constant first = [1] + [0]*; // Used mostly to toggle off the first row consisting
99
// only in first element of shifted polynomials.
10+
11+
//===== CONTROL FLOW ==========================================================
12+
// Program counter
13+
pol commit pc;
14+
// Return Pointer
15+
pol commit internal_return_ptr;
16+
17+
pol commit sel_internal_call;
18+
pol commit sel_internal_return;
19+
20+
// Halt program execution
21+
pol commit sel_halt;
1022

1123
//===== TABLE SUBOP-TR ========================================================
1224
// Boolean selectors for (sub-)operations. Only one operation is activated at
@@ -66,6 +78,10 @@ namespace avmMini(256);
6678
sel_op_mul * (1 - sel_op_mul) = 0;
6779
sel_op_div * (1 - sel_op_div) = 0;
6880

81+
sel_internal_call * (1 - sel_internal_call) = 0;
82+
sel_internal_return * (1 - sel_internal_return) = 0;
83+
sel_halt * (1 - sel_halt) = 0;
84+
6985
op_err * (1 - op_err) = 0;
7086
tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to memTrace)?
7187

@@ -131,8 +147,47 @@ namespace avmMini(256);
131147
// This works in combination with op_div_err * (sel_op_div - 1) = 0;
132148
// Drawback is the need to paralllelize the latter.
133149

150+
151+
//===== CALL_RETURN ========================================================
152+
// The program counter in the next row should be equal to the value loaded from the ia register
153+
// This implies that a load from memory must occur at the same time
154+
// Imply that we must load the return location into mem_idx_a
155+
156+
#[RETURN_POINTER_INCREMENT]
157+
sel_internal_call * ( internal_return_ptr' - ( internal_return_ptr + 1)) = 0;
158+
sel_internal_call * ( internal_return_ptr - mem_idx_a) = 0;
159+
sel_internal_call * ((pc + 1) - ia) = 0;
160+
161+
// TODO(md): Below relations may be removed through sub-op table lookup
162+
sel_internal_call * (rwa - 1) = 0;
163+
sel_internal_call * (mem_op_a - 1) = 0;
164+
165+
// We must load the memory pointer to be the internal_return_ptr
166+
#[RETURN_POINTER_DECREMENT]
167+
sel_internal_return * ( internal_return_ptr' - ( internal_return_ptr - 1)) = 0;
168+
sel_internal_return * ( (internal_return_ptr - 1) - mem_idx_a) = 0;
169+
sel_internal_return * (pc' - ia) = 0;
170+
171+
// TODO(md): Below relations may be removed through sub-op table lookup
172+
sel_internal_return * rwa = 0;
173+
sel_internal_return * (mem_op_a - 1) = 0;
174+
175+
//===== CONTROL_FLOW_CONSISTENCY ============================================
176+
pol CONTROL_FLOW_SELECTORS = (first + sel_internal_call + sel_internal_return + sel_halt);
177+
pol OPCODE_SELECTORS = (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul);
178+
179+
// Program counter must increment if not jumping or returning
180+
#[PC_INCREMENT]
181+
(1 - first) * (1 - sel_halt) * OPCODE_SELECTORS * (pc' - (pc + 1)) = 0;
182+
183+
// first == 0 && sel_internal_call == 0 && sel_internal_return == 0 && sel_halt == 0 ==> internal_return_ptr == internal_return_ptr'
184+
#[INTERNAL_RETURN_POINTER_CONSISTENCY]
185+
(1 - CONTROL_FLOW_SELECTORS) * (internal_return_ptr' - internal_return_ptr) = 0;
186+
187+
// TODO: we want to set an initial number for the reserved memory of the jump pointer
188+
134189
// Inter-table Constraints
135190

136191
// TODO: tag_err {clk} IS memTrace.m_tag_err {memTrace.m_clk}
137192
// TODO: Map memory trace with intermediate register values whenever there is no tag error, sthg like:
138-
// mem_op_a * (1 - tag_err) {mem_idx_a, clk, ia, rwa} IS m_sub_clk == 0 && 1 - m_tag_err {m_addr, m_clk, m_val, m_rw}
193+
// mem_op_a * (1 - tag_err) {mem_idx_a, clk, ia, rwa} IS m_sub_clk == 0 && 1 - m_tag_err {m_addr, m_clk, m_val, m_rw}

barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp

+68-10
Original file line numberDiff line numberDiff line change
@@ -36,13 +36,13 @@ class AvmMiniFlavor {
3636
using VerifierCommitmentKey = pcs::VerifierCommitmentKey<Curve>;
3737

3838
static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2;
39-
static constexpr size_t NUM_WITNESS_ENTITIES = 32;
39+
static constexpr size_t NUM_WITNESS_ENTITIES = 37;
4040
static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES;
4141
// We have two copies of the witness entities, so we subtract the number of fixed ones (they have no shift), one for
4242
// the unshifted and one for the shifted
43-
static constexpr size_t NUM_ALL_ENTITIES = 38;
43+
static constexpr size_t NUM_ALL_ENTITIES = 45;
4444

45-
using Relations = std::tuple<AvmMini_vm::mem_trace<FF>, AvmMini_vm::avm_mini<FF>>;
45+
using Relations = std::tuple<AvmMini_vm::avm_mini<FF>, AvmMini_vm::mem_trace<FF>>;
4646

4747
static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length<Relations>();
4848

@@ -87,6 +87,11 @@ class AvmMiniFlavor {
8787
memTrace_m_in_tag,
8888
memTrace_m_tag_err,
8989
memTrace_m_one_min_inv,
90+
avmMini_pc,
91+
avmMini_internal_return_ptr,
92+
avmMini_sel_internal_call,
93+
avmMini_sel_internal_return,
94+
avmMini_sel_halt,
9095
avmMini_sel_op_add,
9196
avmMini_sel_op_sub,
9297
avmMini_sel_op_mul,
@@ -122,6 +127,11 @@ class AvmMiniFlavor {
122127
memTrace_m_in_tag,
123128
memTrace_m_tag_err,
124129
memTrace_m_one_min_inv,
130+
avmMini_pc,
131+
avmMini_internal_return_ptr,
132+
avmMini_sel_internal_call,
133+
avmMini_sel_internal_return,
134+
avmMini_sel_halt,
125135
avmMini_sel_op_add,
126136
avmMini_sel_op_sub,
127137
avmMini_sel_op_mul,
@@ -163,6 +173,11 @@ class AvmMiniFlavor {
163173
memTrace_m_in_tag,
164174
memTrace_m_tag_err,
165175
memTrace_m_one_min_inv,
176+
avmMini_pc,
177+
avmMini_internal_return_ptr,
178+
avmMini_sel_internal_call,
179+
avmMini_sel_internal_return,
180+
avmMini_sel_halt,
166181
avmMini_sel_op_add,
167182
avmMini_sel_op_sub,
168183
avmMini_sel_op_mul,
@@ -184,10 +199,12 @@ class AvmMiniFlavor {
184199
avmMini_mem_idx_b,
185200
avmMini_mem_idx_c,
186201
avmMini_last,
202+
avmMini_internal_return_ptr_shift,
203+
avmMini_pc_shift,
204+
memTrace_m_tag_shift,
187205
memTrace_m_val_shift,
188-
memTrace_m_addr_shift,
189206
memTrace_m_rw_shift,
190-
memTrace_m_tag_shift)
207+
memTrace_m_addr_shift)
191208

192209
RefVector<DataType> get_wires()
193210
{
@@ -204,6 +221,11 @@ class AvmMiniFlavor {
204221
memTrace_m_in_tag,
205222
memTrace_m_tag_err,
206223
memTrace_m_one_min_inv,
224+
avmMini_pc,
225+
avmMini_internal_return_ptr,
226+
avmMini_sel_internal_call,
227+
avmMini_sel_internal_return,
228+
avmMini_sel_halt,
207229
avmMini_sel_op_add,
208230
avmMini_sel_op_sub,
209231
avmMini_sel_op_mul,
@@ -225,10 +247,12 @@ class AvmMiniFlavor {
225247
avmMini_mem_idx_b,
226248
avmMini_mem_idx_c,
227249
avmMini_last,
250+
avmMini_internal_return_ptr_shift,
251+
avmMini_pc_shift,
252+
memTrace_m_tag_shift,
228253
memTrace_m_val_shift,
229-
memTrace_m_addr_shift,
230254
memTrace_m_rw_shift,
231-
memTrace_m_tag_shift };
255+
memTrace_m_addr_shift };
232256
};
233257
RefVector<DataType> get_unshifted()
234258
{
@@ -245,6 +269,11 @@ class AvmMiniFlavor {
245269
memTrace_m_in_tag,
246270
memTrace_m_tag_err,
247271
memTrace_m_one_min_inv,
272+
avmMini_pc,
273+
avmMini_internal_return_ptr,
274+
avmMini_sel_internal_call,
275+
avmMini_sel_internal_return,
276+
avmMini_sel_halt,
248277
avmMini_sel_op_add,
249278
avmMini_sel_op_sub,
250279
avmMini_sel_op_mul,
@@ -269,11 +298,18 @@ class AvmMiniFlavor {
269298
};
270299
RefVector<DataType> get_to_be_shifted()
271300
{
272-
return { memTrace_m_val, memTrace_m_addr, memTrace_m_rw, memTrace_m_tag };
301+
return {
302+
avmMini_internal_return_ptr, avmMini_pc, memTrace_m_tag, memTrace_m_val, memTrace_m_rw, memTrace_m_addr
303+
};
273304
};
274305
RefVector<DataType> get_shifted()
275306
{
276-
return { memTrace_m_val_shift, memTrace_m_addr_shift, memTrace_m_rw_shift, memTrace_m_tag_shift };
307+
return { avmMini_internal_return_ptr_shift,
308+
avmMini_pc_shift,
309+
memTrace_m_tag_shift,
310+
memTrace_m_val_shift,
311+
memTrace_m_rw_shift,
312+
memTrace_m_addr_shift };
277313
};
278314
};
279315

@@ -286,7 +322,9 @@ class AvmMiniFlavor {
286322

287323
RefVector<DataType> get_to_be_shifted()
288324
{
289-
return { memTrace_m_val, memTrace_m_addr, memTrace_m_rw, memTrace_m_tag };
325+
return {
326+
avmMini_internal_return_ptr, avmMini_pc, memTrace_m_tag, memTrace_m_val, memTrace_m_rw, memTrace_m_addr
327+
};
290328
};
291329

292330
// The plookup wires that store plookup read data.
@@ -376,6 +414,11 @@ class AvmMiniFlavor {
376414
Base::memTrace_m_in_tag = "MEMTRACE_M_IN_TAG";
377415
Base::memTrace_m_tag_err = "MEMTRACE_M_TAG_ERR";
378416
Base::memTrace_m_one_min_inv = "MEMTRACE_M_ONE_MIN_INV";
417+
Base::avmMini_pc = "AVMMINI_PC";
418+
Base::avmMini_internal_return_ptr = "AVMMINI_INTERNAL_RETURN_PTR";
419+
Base::avmMini_sel_internal_call = "AVMMINI_SEL_INTERNAL_CALL";
420+
Base::avmMini_sel_internal_return = "AVMMINI_SEL_INTERNAL_RETURN";
421+
Base::avmMini_sel_halt = "AVMMINI_SEL_HALT";
379422
Base::avmMini_sel_op_add = "AVMMINI_SEL_OP_ADD";
380423
Base::avmMini_sel_op_sub = "AVMMINI_SEL_OP_SUB";
381424
Base::avmMini_sel_op_mul = "AVMMINI_SEL_OP_MUL";
@@ -427,6 +470,11 @@ class AvmMiniFlavor {
427470
Commitment memTrace_m_in_tag;
428471
Commitment memTrace_m_tag_err;
429472
Commitment memTrace_m_one_min_inv;
473+
Commitment avmMini_pc;
474+
Commitment avmMini_internal_return_ptr;
475+
Commitment avmMini_sel_internal_call;
476+
Commitment avmMini_sel_internal_return;
477+
Commitment avmMini_sel_halt;
430478
Commitment avmMini_sel_op_add;
431479
Commitment avmMini_sel_op_sub;
432480
Commitment avmMini_sel_op_mul;
@@ -478,6 +526,11 @@ class AvmMiniFlavor {
478526
memTrace_m_in_tag = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
479527
memTrace_m_tag_err = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
480528
memTrace_m_one_min_inv = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
529+
avmMini_pc = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
530+
avmMini_internal_return_ptr = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
531+
avmMini_sel_internal_call = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
532+
avmMini_sel_internal_return = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
533+
avmMini_sel_halt = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
481534
avmMini_sel_op_add = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
482535
avmMini_sel_op_sub = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
483536
avmMini_sel_op_mul = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
@@ -533,6 +586,11 @@ class AvmMiniFlavor {
533586
serialize_to_buffer<Commitment>(memTrace_m_in_tag, Transcript::proof_data);
534587
serialize_to_buffer<Commitment>(memTrace_m_tag_err, Transcript::proof_data);
535588
serialize_to_buffer<Commitment>(memTrace_m_one_min_inv, Transcript::proof_data);
589+
serialize_to_buffer<Commitment>(avmMini_pc, Transcript::proof_data);
590+
serialize_to_buffer<Commitment>(avmMini_internal_return_ptr, Transcript::proof_data);
591+
serialize_to_buffer<Commitment>(avmMini_sel_internal_call, Transcript::proof_data);
592+
serialize_to_buffer<Commitment>(avmMini_sel_internal_return, Transcript::proof_data);
593+
serialize_to_buffer<Commitment>(avmMini_sel_halt, Transcript::proof_data);
536594
serialize_to_buffer<Commitment>(avmMini_sel_op_add, Transcript::proof_data);
537595
serialize_to_buffer<Commitment>(avmMini_sel_op_sub, Transcript::proof_data);
538596
serialize_to_buffer<Commitment>(avmMini_sel_op_mul, Transcript::proof_data);

barretenberg/cpp/src/barretenberg/flavor/generated/Toy_flavor.hpp

+1-3
Original file line numberDiff line numberDiff line change
@@ -142,8 +142,6 @@ class ToyFlavor {
142142
using Base::Base;
143143
};
144144

145-
using RowPolynomials = AllEntities<FF>;
146-
147145
/**
148146
* @brief A container for the prover polynomials handles.
149147
*/
@@ -156,7 +154,7 @@ class ToyFlavor {
156154
ProverPolynomials(ProverPolynomials&& o) noexcept = default;
157155
ProverPolynomials& operator=(ProverPolynomials&& o) noexcept = default;
158156
~ProverPolynomials() = default;
159-
[[nodiscard]] size_t get_polynomial_size() const { return toy_first.size(); }
157+
[[nodiscard]] size_t get_polynomial_size() const { return toy_q_tuple_set.size(); }
160158
/**
161159
* @brief Returns the evaluations of all prover polynomials at one point on the boolean hypercube, which
162160
* represents one row in the execution trace.

barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_helper.cpp

+41-35
Original file line numberDiff line numberDiff line change
@@ -19,47 +19,53 @@ void log_avmMini_trace(std::vector<Row> const& trace, size_t beg, size_t end)
1919
info("Built circuit with ", trace.size(), " rows");
2020

2121
for (size_t i = beg; i < end; i++) {
22-
info("================================================================================");
23-
info("== ROW ", i);
24-
info("================================================================================");
22+
info("=====================================================================================");
23+
info("== ROW ", i);
24+
info("=====================================================================================");
2525

26-
info("=======MEMORY TRACE=============================================================");
27-
info("m_addr: ", trace.at(i).memTrace_m_addr);
28-
info("m_clk: ", trace.at(i).memTrace_m_clk);
29-
info("m_sub_clk: ", trace.at(i).memTrace_m_sub_clk);
30-
info("m_val: ", trace.at(i).memTrace_m_val);
31-
info("m_rw: ", trace.at(i).memTrace_m_rw);
32-
info("m_tag: ", trace.at(i).memTrace_m_tag);
33-
info("m_in_tag: ", trace.at(i).memTrace_m_in_tag);
34-
info("m_tag_err: ", trace.at(i).memTrace_m_tag_err);
35-
info("m_one_min_inv:", trace.at(i).memTrace_m_one_min_inv);
26+
info("=======MEMORY TRACE==================================================================");
27+
info("m_addr: ", trace.at(i).memTrace_m_addr);
28+
info("m_clk: ", trace.at(i).memTrace_m_clk);
29+
info("m_sub_clk: ", trace.at(i).memTrace_m_sub_clk);
30+
info("m_val: ", trace.at(i).memTrace_m_val);
31+
info("m_rw: ", trace.at(i).memTrace_m_rw);
32+
info("m_tag: ", trace.at(i).memTrace_m_tag);
33+
info("m_in_tag: ", trace.at(i).memTrace_m_in_tag);
34+
info("m_tag_err: ", trace.at(i).memTrace_m_tag_err);
35+
info("m_one_min_inv: ", trace.at(i).memTrace_m_one_min_inv);
3636

37-
info("m_lastAccess: ", trace.at(i).memTrace_m_lastAccess);
38-
info("m_last: ", trace.at(i).memTrace_m_last);
39-
info("m_val_shift: ", trace.at(i).memTrace_m_val_shift);
37+
info("m_lastAccess: ", trace.at(i).memTrace_m_lastAccess);
38+
info("m_last: ", trace.at(i).memTrace_m_last);
39+
info("m_val_shift: ", trace.at(i).memTrace_m_val_shift);
4040

41-
info("=======MAIN TRACE===============================================================");
42-
info("ia: ", trace.at(i).avmMini_ia);
43-
info("ib: ", trace.at(i).avmMini_ib);
44-
info("ic: ", trace.at(i).avmMini_ic);
45-
info("first: ", trace.at(i).avmMini_first);
46-
info("last: ", trace.at(i).avmMini_last);
41+
info("=======CONTROL_FLOW===================================================================");
42+
info("pc: ", trace.at(i).avmMini_pc);
43+
info("internal_call: ", trace.at(i).avmMini_sel_internal_call);
44+
info("internal_return: ", trace.at(i).avmMini_sel_internal_return);
45+
info("internal_return_ptr:", trace.at(i).avmMini_internal_return_ptr);
4746

48-
info("=======MEM_OP_A=================================================================");
49-
info("clk: ", trace.at(i).avmMini_clk);
50-
info("mem_op_a: ", trace.at(i).avmMini_mem_op_a);
51-
info("mem_idx_a: ", trace.at(i).avmMini_mem_idx_a);
52-
info("rwa: ", trace.at(i).avmMini_rwa);
47+
info("=======MAIN TRACE====================================================================");
48+
info("ia: ", trace.at(i).avmMini_ia);
49+
info("ib: ", trace.at(i).avmMini_ib);
50+
info("ic: ", trace.at(i).avmMini_ic);
51+
info("first: ", trace.at(i).avmMini_first);
52+
info("last: ", trace.at(i).avmMini_last);
5353

54-
info("=======MEM_OP_B=================================================================");
55-
info("mem_op_b: ", trace.at(i).avmMini_mem_op_b);
56-
info("mem_idx_b: ", trace.at(i).avmMini_mem_idx_b);
57-
info("rwb: ", trace.at(i).avmMini_rwb);
54+
info("=======MEM_OP_A======================================================================");
55+
info("clk: ", trace.at(i).avmMini_clk);
56+
info("mem_op_a: ", trace.at(i).avmMini_mem_op_a);
57+
info("mem_idx_a: ", trace.at(i).avmMini_mem_idx_a);
58+
info("rwa: ", trace.at(i).avmMini_rwa);
5859

59-
info("=======MEM_OP_C=================================================================");
60-
info("mem_op_c: ", trace.at(i).avmMini_mem_op_c);
61-
info("mem_idx_c: ", trace.at(i).avmMini_mem_idx_c);
62-
info("rwc: ", trace.at(i).avmMini_rwc);
60+
info("=======MEM_OP_B======================================================================");
61+
info("mem_op_b: ", trace.at(i).avmMini_mem_op_b);
62+
info("mem_idx_b: ", trace.at(i).avmMini_mem_idx_b);
63+
info("rwb: ", trace.at(i).avmMini_rwb);
64+
65+
info("=======MEM_OP_C======================================================================");
66+
info("mem_op_c: ", trace.at(i).avmMini_mem_op_c);
67+
info("mem_idx_c: ", trace.at(i).avmMini_mem_idx_c);
68+
info("rwc: ", trace.at(i).avmMini_rwc);
6369
info("\n");
6470
}
6571
}

0 commit comments

Comments
 (0)