Skip to content

Commit

Permalink
chore: reads the return data (#6669)
Browse files Browse the repository at this point in the history
Add reads to return_data to properly constrain the return_data wires.

---------

Co-authored-by: ledwards2225 <l.edwards.d@gmail.com>
  • Loading branch information
guipublic and ledwards2225 authored Jun 19, 2024
1 parent a0b9c4b commit ef85542
Show file tree
Hide file tree
Showing 4 changed files with 202 additions and 96 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ class AcirIntegrationTest : public ::testing::Test {
}

acir_format::AcirProgramStack get_program_stack_data_from_test_file(const std::string& test_program_name,
bool honk_recursion)
bool honk_recursion = false)
{
std::string base_path = "../../acir_tests/acir_tests/" + test_program_name + "/target";
std::string bytecode_path = base_path + "/program.json";
Expand All @@ -45,7 +45,8 @@ class AcirIntegrationTest : public ::testing::Test {
return acir_format::get_acir_program_stack(bytecode_path, witness_path, honk_recursion);
}

acir_format::AcirProgram get_program_data_from_test_file(const std::string& test_program_name, bool honk_recursion)
acir_format::AcirProgram get_program_data_from_test_file(const std::string& test_program_name,
bool honk_recursion = false)
{
auto program_stack = get_program_stack_data_from_test_file(test_program_name, honk_recursion);
ASSERT(program_stack.size() == 1); // Otherwise this method will not return full stack data
Expand Down Expand Up @@ -428,6 +429,29 @@ INSTANTIATE_TEST_SUITE_P(AcirTests,
AcirIntegrationFoldingTest,
testing::Values("fold_basic", "fold_basic_nested_call"));

/**
*@brief A basic test of a circuit generated in noir that makes use of the databus
*
*/
TEST_F(AcirIntegrationTest, DISABLED_Databus)
{
using Flavor = MegaFlavor;
using Builder = Flavor::CircuitBuilder;

std::string test_name = "databus";
info("Test: ", test_name);
acir_format::AcirProgram acir_program = get_program_data_from_test_file(test_name);

// Construct a bberg circuit from the acir representation
Builder builder = acir_format::create_circuit<Builder>(acir_program.constraints, 0, acir_program.witness);

// This prints a summary of the types of gates in the circuit
builder.blocks.summarize();

// Construct and verify Honk proof
EXPECT_TRUE(prove_and_verify_honk<Flavor>(builder));
}

/**
* @brief Ensure that adding gates post-facto to a circuit generated from acir still results in a valid circuit
* @details This is a pattern required by e.g. ClientIvc which appends recursive verifiers to acir-generated circuits
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -484,14 +484,11 @@ BlockConstraint handle_memory_init(Program::Opcode::MemoryInit const& mem_init)
});
}

// Databus is only supported for Goblin, non Goblin builders will treat call_data and return_data as normal
// array.
if (IsMegaBuilder<Builder>) {
if (std::holds_alternative<Program::BlockType::CallData>(mem_init.block_type.value)) {
block.type = BlockType::CallData;
} else if (std::holds_alternative<Program::BlockType::ReturnData>(mem_init.block_type.value)) {
block.type = BlockType::ReturnData;
}
// Databus is only supported for Goblin, non Goblin builders will treat call_data and return_data as normal array.
if (std::holds_alternative<Program::BlockType::CallData>(mem_init.block_type.value)) {
block.type = BlockType::CallData;
} else if (std::holds_alternative<Program::BlockType::ReturnData>(mem_init.block_type.value)) {
block.type = BlockType::ReturnData;
}

return block;
Expand Down Expand Up @@ -557,7 +554,8 @@ AcirFormat circuit_serde_to_acir_format(Program::Circuit const& circuit, bool ho
gate.value);
}
for (const auto& [block_id, block] : block_id_to_block_constraint) {
if (!block.first.trace.empty()) {
// Note: the trace will always be empty for ReturnData since it cannot be explicitly read from in noir
if (!block.first.trace.empty() || block.first.type == BlockType::ReturnData) {
af.block_constraints.push_back(block.first);
af.original_opcode_indices.block_constraints.push_back(block.second);
}
Expand Down
236 changes: 151 additions & 85 deletions barretenberg/cpp/src/barretenberg/dsl/acir_format/block_constraint.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,17 @@ template <typename Builder> stdlib::field_t<Builder> poly_to_field_ct(const poly
return x;
}

template <typename Builder>
void create_block_constraints(Builder& builder, const BlockConstraint& constraint, bool has_valid_witness_assignments)
/**
* @brief Create block constraints; Specialization for Ultra arithmetization
* @details Ultra does not support DataBus operations so calldata/returndata are treated as ROM ops
*
*/
template <>
void create_block_constraints(UltraCircuitBuilder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments)
{
using field_ct = stdlib::field_t<Builder>;
using rom_table_ct = stdlib::rom_table<Builder>;
using ram_table_ct = stdlib::ram_table<Builder>;
using databus_ct = stdlib::databus<Builder>;
using field_ct = bb::stdlib::field_t<UltraCircuitBuilder>;

std::vector<field_ct> init;
for (auto i : constraint.init) {
Expand All @@ -39,98 +43,160 @@ void create_block_constraints(Builder& builder, const BlockConstraint& constrain
}

switch (constraint.type) {
// Note: CallData/ReturnData not supported by Ultra; interpreted as ROM ops instead
case BlockType::CallData:
case BlockType::ReturnData:
case BlockType::ROM: {
rom_table_ct table(init);
for (auto& op : constraint.trace) {
ASSERT(op.access_type == 0);
field_ct value = poly_to_field_ct(op.value, builder);
field_ct index = poly_to_field_ct(op.index, builder);
// For a ROM table, constant read should be optimized out:
// The rom_table won't work with a constant read because the table may not be initialized
ASSERT(op.index.q_l != 0);
// We create a new witness w to avoid issues with non-valid witness assignements:
// if witness are not assigned, then w will be zero and table[w] will work
fr w_value = 0;
if (has_valid_witness_assignments) {
// If witness are assigned, we use the correct value for w
w_value = index.get_value();
}
field_ct w = field_ct::from_witness(&builder, w_value);
value.assert_equal(table[w]);
w.assert_equal(index);
}
process_ROM_operations(builder, constraint, has_valid_witness_assignments, init);
} break;
case BlockType::RAM: {
ram_table_ct table(init);
for (auto& op : constraint.trace) {
field_ct value = poly_to_field_ct(op.value, builder);
field_ct index = poly_to_field_ct(op.index, builder);

// We create a new witness w to avoid issues with non-valid witness assignements.
// If witness are not assigned, then index will be zero and table[index] won't hit bounds check.
fr index_value = has_valid_witness_assignments ? index.get_value() : 0;
// Create new witness and ensure equal to index.
field_ct::from_witness(&builder, index_value).assert_equal(index);

if (op.access_type == 0) {
value.assert_equal(table.read(index));
} else {
ASSERT(op.access_type == 1);
table.write(index, value);
}
}
process_RAM_operations(builder, constraint, has_valid_witness_assignments, init);
} break;
default:
ASSERT(false);
break;
}
}

/**
* @brief Create block constraints; Specialization for Mega arithmetization
*
*/
template <>
void create_block_constraints(MegaCircuitBuilder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments)
{
using field_ct = stdlib::field_t<MegaCircuitBuilder>;

std::vector<field_ct> init;
for (auto i : constraint.init) {
field_ct value = poly_to_field_ct(i, builder);
init.push_back(value);
}

switch (constraint.type) {
case BlockType::ROM: {
process_ROM_operations(builder, constraint, has_valid_witness_assignments, init);
} break;
case BlockType::RAM: {
process_RAM_operations(builder, constraint, has_valid_witness_assignments, init);
} break;
case BlockType::CallData: {
if constexpr (IsMegaBuilder<Builder>) {
databus_ct databus;
// Populate the calldata in the databus
databus.calldata.set_values(init);
for (const auto& op : constraint.trace) {
ASSERT(op.access_type == 0);
field_ct value = poly_to_field_ct(op.value, builder);
field_ct index = poly_to_field_ct(op.index, builder);
fr w_value = 0;
if (has_valid_witness_assignments) {
// If witness are assigned, we use the correct value for w
w_value = index.get_value();
}
field_ct w = field_ct::from_witness(&builder, w_value);
value.assert_equal(databus.calldata[w]);
w.assert_equal(index);
}
}
process_call_data_operations(builder, constraint, has_valid_witness_assignments, init);
} break;
case BlockType::ReturnData: {
if constexpr (IsMegaBuilder<Builder>) {
databus_ct databus;
// Populate the returndata in the databus
databus.return_data.set_values(init);
for (const auto& op : constraint.trace) {
ASSERT(op.access_type == 0);
field_ct value = poly_to_field_ct(op.value, builder);
field_ct index = poly_to_field_ct(op.index, builder);
fr w_value = 0;
if (has_valid_witness_assignments) {
// If witness are assigned, we use the correct value for w
w_value = index.get_value();
}
field_ct w = field_ct::from_witness(&builder, w_value);
value.assert_equal(databus.return_data[w]);
w.assert_equal(index);
}
}
process_return_data_operations(constraint, init);
} break;
default:
ASSERT(false);
break;
}
}

template void create_block_constraints<UltraCircuitBuilder>(UltraCircuitBuilder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments);
template void create_block_constraints<MegaCircuitBuilder>(MegaCircuitBuilder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments);
template <typename Builder>
void process_ROM_operations(Builder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments,
std::vector<bb::stdlib::field_t<Builder>>& init)
{
using field_ct = stdlib::field_t<Builder>;
using rom_table_ct = stdlib::rom_table<Builder>;

rom_table_ct table(init);
for (auto& op : constraint.trace) {
ASSERT(op.access_type == 0);
field_ct value = poly_to_field_ct(op.value, builder);
field_ct index = poly_to_field_ct(op.index, builder);
// For a ROM table, constant read should be optimized out:
// The rom_table won't work with a constant read because the table may not be initialized
ASSERT(op.index.q_l != 0);
// We create a new witness w to avoid issues with non-valid witness assignements:
// if witness are not assigned, then w will be zero and table[w] will work
fr w_value = 0;
if (has_valid_witness_assignments) {
// If witness are assigned, we use the correct value for w
w_value = index.get_value();
}
field_ct w = field_ct::from_witness(&builder, w_value);
value.assert_equal(table[w]);
w.assert_equal(index);
}
}

template <typename Builder>
void process_RAM_operations(Builder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments,
std::vector<bb::stdlib::field_t<Builder>>& init)
{
using field_ct = stdlib::field_t<Builder>;
using ram_table_ct = stdlib::ram_table<Builder>;

ram_table_ct table(init);
for (auto& op : constraint.trace) {
field_ct value = poly_to_field_ct(op.value, builder);
field_ct index = poly_to_field_ct(op.index, builder);

// We create a new witness w to avoid issues with non-valid witness assignements.
// If witness are not assigned, then index will be zero and table[index] won't hit bounds check.
fr index_value = has_valid_witness_assignments ? index.get_value() : 0;
// Create new witness and ensure equal to index.
field_ct::from_witness(&builder, index_value).assert_equal(index);

if (op.access_type == 0) {
value.assert_equal(table.read(index));
} else {
ASSERT(op.access_type == 1);
table.write(index, value);
}
}
}

template <typename Builder>
void process_call_data_operations(Builder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments,
std::vector<bb::stdlib::field_t<Builder>>& init)
{
using field_ct = stdlib::field_t<Builder>;
using databus_ct = stdlib::databus<Builder>;

databus_ct databus;
// Populate the calldata in the databus
databus.calldata.set_values(init);
for (const auto& op : constraint.trace) {
ASSERT(op.access_type == 0);
field_ct value = poly_to_field_ct(op.value, builder);
field_ct index = poly_to_field_ct(op.index, builder);
fr w_value = 0;
if (has_valid_witness_assignments) {
// If witness are assigned, we use the correct value for w
w_value = index.get_value();
}
field_ct w = field_ct::from_witness(&builder, w_value);
value.assert_equal(databus.calldata[w]);
w.assert_equal(index);
}
}

template <typename Builder>
void process_return_data_operations(const BlockConstraint& constraint, std::vector<bb::stdlib::field_t<Builder>>& init)
{
using databus_ct = stdlib::databus<Builder>;

databus_ct databus;
// Populate the returndata in the databus
databus.return_data.set_values(init);
// For each entry of the return data, explicitly assert equality with the initialization value. This implicitly
// creates the return data read gates that are required to connect witness values in the main wires to witness
// values in the databus return data column.
size_t c = 0;
for (const auto& value : init) {
value.assert_equal(databus.return_data[c]);
c++;
}
ASSERT(constraint.trace.size() == 0);
}

} // namespace acir_format
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,24 @@ void create_block_constraints(Builder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments = true);

template <typename Builder>
void process_ROM_operations(Builder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments,
std::vector<bb::stdlib::field_t<Builder>>& init);
template <typename Builder>
void process_RAM_operations(Builder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments,
std::vector<bb::stdlib::field_t<Builder>>& init);
template <typename Builder>
void process_call_data_operations(Builder& builder,
const BlockConstraint& constraint,
bool has_valid_witness_assignments,
std::vector<bb::stdlib::field_t<Builder>>& init);
template <typename Builder>
void process_return_data_operations(const BlockConstraint& constraint, std::vector<bb::stdlib::field_t<Builder>>& init);

template <typename B> inline void read(B& buf, MemOp& mem_op)
{
using serialize::read;
Expand Down

0 comments on commit ef85542

Please sign in to comment.