-
Notifications
You must be signed in to change notification settings - Fork 295
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
refactor(avm): avm memory trace building #3835
Merged
+1,100
−992
Merged
Changes from 4 commits
Commits
Show all changes
7 commits
Select commit
Hold shift + click to select a range
b4203a0
3738 - minor changes in import
jeanmon 6d48545
3738: create a common header files for AvmMini
jeanmon d52365c
Refactoring: move memory trace building and memory operations simluation
jeanmon 91e3a65
Style - snake casing of camel case variables and function names
jeanmon 052b240
3834 - Address some review feedback on missing documentation
jeanmon 6e03ab7
Remove superfluous import of header files
jeanmon a673e04
3834 - Moving trace building related files for avm into vm folder and
jeanmon File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
17 changes: 17 additions & 0 deletions
17
barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_common.hpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
#pragma once | ||
|
||
#include "barretenberg/proof_system/circuit_builder/circuit_builder_base.hpp" | ||
#include "barretenberg/proof_system/circuit_builder/generated/AvmMini_circuit_builder.hpp" | ||
|
||
using Flavor = proof_system::honk::flavor::AvmMiniFlavor; | ||
using FF = Flavor::FF; | ||
using Row = proof_system::AvmMiniFullRow<barretenberg::fr>; | ||
|
||
namespace proof_system { | ||
|
||
// Number of rows | ||
static const size_t AVM_TRACE_SIZE = 256; | ||
enum class IntermRegister : uint32_t { ia = 0, ib = 1, ic = 2 }; | ||
enum class AvmMemoryTag : uint32_t { u0 = 0, u8 = 1, u16 = 2, u32 = 3, u64 = 4, u128 = 5, ff = 6 }; | ||
|
||
} // namespace proof_system |
7 changes: 1 addition & 6 deletions
7
barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_helper.cpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
10 changes: 1 addition & 9 deletions
10
barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_helper.hpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,17 +1,9 @@ | ||
#pragma once | ||
|
||
#include "barretenberg/ecc/curves/bn254/fr.hpp" | ||
#include "barretenberg/proof_system/circuit_builder/circuit_builder_base.hpp" | ||
|
||
#include "barretenberg/flavor/generated/AvmMini_flavor.hpp" | ||
#include "barretenberg/proof_system/circuit_builder/generated/AvmMini_circuit_builder.hpp" | ||
#include "AvmMini_common.hpp" | ||
|
||
namespace proof_system { | ||
|
||
using Flavor = proof_system::honk::flavor::AvmMiniFlavor; | ||
using FF = Flavor::FF; | ||
using Row = proof_system::AvmMiniFullRow<barretenberg::fr>; | ||
|
||
void log_avmMini_trace(std::vector<Row> const& trace, size_t beg, size_t end); | ||
|
||
} // namespace proof_system |
235 changes: 235 additions & 0 deletions
235
barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_mem_trace.cpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,235 @@ | ||
#include "AvmMini_mem_trace.hpp" | ||
|
||
namespace proof_system { | ||
|
||
/** | ||
* @brief Constructor of a memory trace builder of AVM. Only serves to set the capacity of the | ||
* underlying traces. | ||
*/ | ||
AvmMiniMemTraceBuilder::AvmMiniMemTraceBuilder() | ||
{ | ||
mem_trace.reserve(AVM_TRACE_SIZE); | ||
} | ||
|
||
/** | ||
* @brief Resetting the internal state so that a new memory trace can be rebuilt using the same object. | ||
* | ||
*/ | ||
void AvmMiniMemTraceBuilder::reset() | ||
{ | ||
mem_trace.clear(); | ||
memory.fill(FF(0)); | ||
} | ||
|
||
/** | ||
* @brief A comparator on MemoryTraceEntry to be used by sorting algorithm. | ||
* | ||
*/ | ||
bool AvmMiniMemTraceBuilder::compare_mem_entries(const MemoryTraceEntry& left, const MemoryTraceEntry& right) | ||
{ | ||
if (left.m_addr < right.m_addr) { | ||
return true; | ||
} | ||
|
||
if (left.m_addr > right.m_addr) { | ||
return false; | ||
} | ||
|
||
if (left.m_clk < right.m_clk) { | ||
return true; | ||
} | ||
|
||
if (left.m_clk > right.m_clk) { | ||
return false; | ||
} | ||
|
||
// No safeguard in case they are equal. The caller should ensure this property. | ||
// Otherwise, relation will not be satisfied. | ||
return left.m_sub_clk < right.m_sub_clk; | ||
} | ||
|
||
/** | ||
* @brief Prepare the memory trace to be incorporated into the main trace. | ||
* | ||
* @return The memory trace (which is moved). | ||
*/ | ||
std::vector<AvmMiniMemTraceBuilder::MemoryTraceEntry> AvmMiniMemTraceBuilder::finalize() | ||
{ | ||
// Sort memTrace | ||
std::sort(mem_trace.begin(), mem_trace.end(), compare_mem_entries); | ||
return std::move(mem_trace); | ||
} | ||
|
||
/** | ||
* @brief A method to insert a row/entry in the memory trace. | ||
* | ||
* @param m_clk Main clock | ||
* @param m_sub_clk Sub-clock used to order load/store sub operations | ||
* @param m_addr Address pertaining to the memory operation | ||
* @param m_val Value (FF) pertaining to the memory operation | ||
* @param m_in_tag Memory tag pertaining to the instruction | ||
* @param m_rw Boolean telling whether it is a load (false) or store operation (true). | ||
*/ | ||
void AvmMiniMemTraceBuilder::insert_in_mem_trace(uint32_t const m_clk, | ||
uint32_t const m_sub_clk, | ||
uint32_t const m_addr, | ||
FF const& m_val, | ||
AvmMemoryTag const m_in_tag, | ||
bool const m_rw) | ||
{ | ||
mem_trace.emplace_back(MemoryTraceEntry{ | ||
.m_clk = m_clk, | ||
.m_sub_clk = m_sub_clk, | ||
.m_addr = m_addr, | ||
.m_val = m_val, | ||
.m_tag = m_in_tag, | ||
.m_in_tag = m_in_tag, | ||
.m_rw = m_rw, | ||
}); | ||
} | ||
|
||
// Memory operations need to be performed before the addition of the corresponding row in | ||
// MainTrace, otherwise the m_clk value will be wrong. This applies to loadInMemTrace and | ||
// storeInMemTrace. | ||
|
||
/** | ||
* @brief Add a memory trace entry for a load with a memory tag mismatching the instruction | ||
* memory tag. | ||
* | ||
* @param m_clk Main clock | ||
* @param m_sub_clk Sub-clock used to order load/store sub operations | ||
* @param m_addr Address pertaining to the memory operation | ||
* @param m_val Value (FF) pertaining to the memory operation | ||
* @param m_in_tag Memory tag pertaining to the instruction | ||
* @param m_tag Memory tag pertaining to the address | ||
*/ | ||
void AvmMiniMemTraceBuilder::load_mismatch_tag_in_mem_trace(uint32_t const m_clk, | ||
uint32_t const m_sub_clk, | ||
uint32_t const m_addr, | ||
FF const& m_val, | ||
AvmMemoryTag const m_in_tag, | ||
AvmMemoryTag const m_tag) | ||
{ | ||
FF one_min_inv = FF(1) - (FF(static_cast<uint32_t>(m_in_tag)) - FF(static_cast<uint32_t>(m_tag))).invert(); | ||
mem_trace.emplace_back(MemoryTraceEntry{ .m_clk = m_clk, | ||
.m_sub_clk = m_sub_clk, | ||
.m_addr = m_addr, | ||
.m_val = m_val, | ||
.m_tag = m_tag, | ||
.m_in_tag = m_in_tag, | ||
.m_tag_err = true, | ||
.m_one_min_inv = one_min_inv }); | ||
} | ||
|
||
/** | ||
* @brief Add a memory trace entry corresponding to a memory load into the intermediate | ||
* passed register. | ||
* | ||
* @param clk The main clock | ||
* @param interm_reg The intermediate register | ||
* @param addr The memory address | ||
* @param val The value to be loaded | ||
* @param m_in_tag The memory tag of the instruction | ||
*/ | ||
bool AvmMiniMemTraceBuilder::load_in_mem_trace( | ||
uint32_t clk, IntermRegister interm_reg, uint32_t addr, FF const& val, AvmMemoryTag m_in_tag) | ||
{ | ||
uint32_t sub_clk = 0; | ||
switch (interm_reg) { | ||
case IntermRegister::ia: | ||
sub_clk = SUB_CLK_LOAD_A; | ||
break; | ||
case IntermRegister::ib: | ||
sub_clk = SUB_CLK_LOAD_B; | ||
break; | ||
case IntermRegister::ic: | ||
sub_clk = SUB_CLK_LOAD_C; | ||
break; | ||
} | ||
|
||
auto m_tag = memory_tag.at(addr); | ||
if (m_tag == AvmMemoryTag::u0 || m_tag == m_in_tag) { | ||
insert_in_mem_trace(clk, sub_clk, addr, val, m_in_tag, false); | ||
return true; | ||
} | ||
|
||
// Handle memory tag inconsistency | ||
load_mismatch_tag_in_mem_trace(clk, sub_clk, addr, val, m_in_tag, m_tag); | ||
return false; | ||
} | ||
|
||
/** | ||
* @brief Add a memory trace entry corresponding to a memory store from the intermediate | ||
* register. | ||
* | ||
* @param clk The main clock | ||
* @param interm_reg The intermediate register | ||
* @param addr The memory address | ||
* @param val The value to be stored | ||
* @param m_in_tag The memory tag of the instruction | ||
*/ | ||
void AvmMiniMemTraceBuilder::store_in_mem_trace( | ||
uint32_t clk, IntermRegister interm_reg, uint32_t addr, FF const& val, AvmMemoryTag m_in_tag) | ||
{ | ||
uint32_t sub_clk = 0; | ||
switch (interm_reg) { | ||
case IntermRegister::ia: | ||
sub_clk = SUB_CLK_STORE_A; | ||
break; | ||
case IntermRegister::ib: | ||
sub_clk = SUB_CLK_STORE_B; | ||
break; | ||
case IntermRegister::ic: | ||
sub_clk = SUB_CLK_STORE_C; | ||
break; | ||
} | ||
|
||
insert_in_mem_trace(clk, sub_clk, addr, val, m_in_tag, true); | ||
} | ||
|
||
/** | ||
* @brief Handle a read memory operation and load the corresponding value to the | ||
* supplied intermediate register. A memory trace entry for the load operation | ||
* is added. | ||
* | ||
* @param clk Main clock | ||
* @param interm_reg Intermediate register where we load the value | ||
* @param addr Memory address to be read and loaded | ||
* @param m_in_tag Memory instruction tag | ||
* @return Result of the read operation containing the value and a boolean telling | ||
* potential mismatch between instruction tag and memory tag of the address. | ||
*/ | ||
AvmMiniMemTraceBuilder::MemRead AvmMiniMemTraceBuilder::read_and_load_from_memory(uint32_t const clk, | ||
IntermRegister const interm_reg, | ||
uint32_t const addr, | ||
AvmMemoryTag const m_in_tag) | ||
{ | ||
FF val = memory.at(addr); | ||
bool tagMatch = load_in_mem_trace(clk, interm_reg, addr, val, m_in_tag); | ||
|
||
return MemRead{ | ||
.tag_match = tagMatch, | ||
.val = val, | ||
}; | ||
} | ||
|
||
/** | ||
* @brief Handle a write memory operation and store the supplied value into memory | ||
* at the supplied address. A memory trace entry for the write operation | ||
* is added. | ||
* | ||
* @param clk Main clock | ||
* @param interm_reg Intermediate register where we write the value | ||
* @param addr Memory address to be written to | ||
* @param val Value to be written into memory | ||
* @param m_in_tag Memory instruction tag | ||
*/ | ||
void AvmMiniMemTraceBuilder::write_into_memory( | ||
uint32_t const clk, IntermRegister interm_reg, uint32_t addr, FF const& val, AvmMemoryTag m_in_tag) | ||
{ | ||
memory.at(addr) = val; | ||
memory_tag.at(addr) = m_in_tag; | ||
store_in_mem_trace(clk, interm_reg, addr, val, m_in_tag); | ||
} | ||
|
||
} // namespace proof_system |
68 changes: 68 additions & 0 deletions
68
barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_mem_trace.hpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,68 @@ | ||
#pragma once | ||
|
||
#include "AvmMini_common.hpp" | ||
|
||
namespace proof_system { | ||
|
||
class AvmMiniMemTraceBuilder { | ||
|
||
public: | ||
static const size_t MEM_SIZE = 1024; | ||
static const uint32_t SUB_CLK_LOAD_A = 0; | ||
static const uint32_t SUB_CLK_LOAD_B = 1; | ||
static const uint32_t SUB_CLK_LOAD_C = 2; | ||
static const uint32_t SUB_CLK_STORE_A = 3; | ||
static const uint32_t SUB_CLK_STORE_B = 4; | ||
static const uint32_t SUB_CLK_STORE_C = 5; | ||
|
||
struct MemoryTraceEntry { | ||
uint32_t m_clk; | ||
uint32_t m_sub_clk; | ||
uint32_t m_addr; | ||
FF m_val{}; | ||
AvmMemoryTag m_tag; | ||
AvmMemoryTag m_in_tag; | ||
bool m_rw = false; | ||
bool m_tag_err = false; | ||
FF m_one_min_inv{}; | ||
}; | ||
|
||
// Structure to return value and tag matching boolean after a memory read. | ||
struct MemRead { | ||
bool tag_match; | ||
FF val; | ||
}; | ||
|
||
AvmMiniMemTraceBuilder(); | ||
|
||
void reset(); | ||
|
||
std::vector<MemoryTraceEntry> finalize(); | ||
|
||
MemRead read_and_load_from_memory(uint32_t clk, IntermRegister interm_reg, uint32_t addr, AvmMemoryTag m_in_tag); | ||
void write_into_memory( | ||
uint32_t clk, IntermRegister interm_reg, uint32_t addr, FF const& val, AvmMemoryTag m_in_tag); | ||
|
||
private: | ||
std::vector<MemoryTraceEntry> mem_trace; // Entries will be sorted by m_clk, m_sub_clk after finalize(). | ||
std::array<FF, MEM_SIZE> memory{}; // Memory table (used for simulation) | ||
std::array<AvmMemoryTag, MEM_SIZE> memory_tag{}; // The tag of the corresponding memory | ||
// entry (aligned with the memory array). | ||
|
||
static bool compare_mem_entries(const MemoryTraceEntry& left, const MemoryTraceEntry& right); | ||
|
||
void insert_in_mem_trace( | ||
uint32_t m_clk, uint32_t m_sub_clk, uint32_t m_addr, FF const& m_val, AvmMemoryTag m_in_tag, bool m_rw); | ||
void load_mismatch_tag_in_mem_trace(uint32_t m_clk, | ||
uint32_t m_sub_clk, | ||
uint32_t m_addr, | ||
FF const& m_val, | ||
AvmMemoryTag m_in_tag, | ||
AvmMemoryTag m_tag); | ||
|
||
bool load_in_mem_trace( | ||
uint32_t clk, IntermRegister interm_reg, uint32_t addr, FF const& val, AvmMemoryTag m_in_tag); | ||
void store_in_mem_trace( | ||
uint32_t clk, IntermRegister interm_reg, uint32_t addr, FF const& val, AvmMemoryTag m_in_tag); | ||
}; | ||
} // namespace proof_system |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nit: missing doc on @return
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very good catch! I addressed it.