Skip to content

Commit

Permalink
chore: rename avm_mini to avm (#4580)
Browse files Browse the repository at this point in the history
Resolves #4533
  • Loading branch information
jeanmon authored Feb 13, 2024
1 parent e23d048 commit 5896a92
Show file tree
Hide file tree
Showing 50 changed files with 3,322 additions and 3,346 deletions.
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
include "avm_mini.pil";
include "avm_main.pil";

namespace aluChip(256);
namespace avm_alu(256);

// ========= Table ALU-TR =================================================

Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@

include "mem_trace.pil";
include "alu_chip.pil";
include "avm_mem.pil";
include "avm_alu.pil";

namespace avmMini(256);
namespace avm_main(256);

//===== CONSTANT POLYNOMIALS ==================================================
pol constant clk(i) { i };
Expand Down Expand Up @@ -42,7 +42,7 @@ namespace avmMini(256);

// Errors
pol commit op_err; // Boolean flag pertaining to an operation error
pol commit tag_err; // Boolean flag (foreign key to memTrace.m_tag_err)
pol commit tag_err; // Boolean flag (foreign key to avm_mem.m_tag_err)

// A helper witness being the inverse of some value
// to show a non-zero equality
Expand Down Expand Up @@ -89,7 +89,7 @@ namespace avmMini(256);
sel_halt * (1 - sel_halt) = 0;

op_err * (1 - op_err) = 0;
tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to memTrace)?
tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to avm_mem)?

mem_op_a * (1 - mem_op_a) = 0;
mem_op_b * (1 - mem_op_b) = 0;
Expand Down Expand Up @@ -189,6 +189,6 @@ namespace avmMini(256);

// Inter-table Constraints

// TODO: tag_err {clk} IS memTrace.m_tag_err {memTrace.m_clk}
// TODO: tag_err {clk} IS avm_mem.m_tag_err {avm_mem.m_clk}
// TODO: Map memory trace with intermediate register values whenever there is no tag error, sthg like:
// 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}
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@


include "avm_mini.pil";
include "avm_main.pil";

namespace memTrace(256);
namespace avm_mem(256);
// ========= Table MEM-TR =================
pol commit m_clk;
pol commit m_sub_clk;
Expand All @@ -13,7 +13,7 @@ namespace memTrace(256);
pol commit m_last; // Boolean indicating the last row of the memory trace (not execution trace)
pol commit m_rw; // Enum: 0 (read), 1 (write)

pol commit m_in_tag; // Instruction memory tag ("foreign key" pointing to avmMini.in_tag)
pol commit m_in_tag; // Instruction memory tag ("foreign key" pointing to avm_main.in_tag)

// Error columns
pol commit m_tag_err; // Boolean (1 if m_in_tag != m_tag is detected)
Expand All @@ -31,11 +31,11 @@ namespace memTrace(256);
// (m_in_tag will be constrained through inclusion check to main trace)

// Remark: m_lastAccess == 1 on first row and therefore any relation with the
// multiplicative term (1 - m_lastAccess) implicitly includes (1 - avmMini.first)
// multiplicative term (1 - m_lastAccess) implicitly includes (1 - avm_main.first)
// Similarly, this includes (1 - m_last) as well.

// m_lastAccess == 0 ==> m_addr' == m_addr
// Optimization: We removed the term (1 - avmMini.first)
// Optimization: We removed the term (1 - avm_main.first)
#[MEM_LAST_ACCESS_DELIMITER]
(1 - m_lastAccess) * (m_addr' - m_addr) = 0;

Expand All @@ -61,12 +61,12 @@ namespace memTrace(256);
// 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

// Optimization: We removed the term (1 - avmMini.first) and (1 - m_last)
// Optimization: We removed the term (1 - avm_main.first) and (1 - m_last)
#[MEM_READ_WRITE_VAL_CONSISTENCY]
(1 - m_lastAccess) * (1 - m_rw') * (m_val' - m_val) = 0;

// m_lastAccess == 0 && m_rw' == 0 ==> m_tag == m_tag'
// Optimization: We removed the term (1 - avmMini.first) and (1 - m_last)
// Optimization: We removed the term (1 - avm_main.first) and (1 - m_last)
#[MEM_READ_WRITE_TAG_CONSISTENCY]
(1 - m_lastAccess) * (1 - m_rw') * (m_tag' - m_tag) = 0;

Expand Down Expand Up @@ -103,4 +103,4 @@ namespace memTrace(256);

// Inter-table Constraints

// TODO: {m_clk, m_in_tag} IN {avmMini.clk, avmMini.in_tag}
// TODO: {m_clk, m_in_tag} IN {avm_main.clk, avm_main.in_tag}
2 changes: 1 addition & 1 deletion barretenberg/cpp/src/barretenberg/bb/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
#include "barretenberg/dsl/types.hpp"
#include "barretenberg/honk/proof_system/types/proof.hpp"
#include "barretenberg/plonk/proof_system/proving_key/serialize.hpp"
#include "barretenberg/vm/avm_trace/AvmMini_execution.hpp"
#include "barretenberg/vm/avm_trace/avm_execution.hpp"
#include "config.hpp"
#include "get_bn254_crs.hpp"
#include "get_bytecode.hpp"
Expand Down
Loading

0 comments on commit 5896a92

Please sign in to comment.