Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: rename avm_mini to avm #4580

Merged
merged 4 commits into from
Feb 13, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading