Skip to content

Commit

Permalink
fix: Zero index is not always 0 (#10135)
Browse files Browse the repository at this point in the history
This pr changes the export method of circuit builders, adding the name
"zero" to an appropriate index, which is not always 0.
  • Loading branch information
Sarkoxed authored Nov 22, 2024
1 parent 95e8406 commit bbac3d9
Show file tree
Hide file tree
Showing 5 changed files with 11 additions and 16 deletions.
2 changes: 2 additions & 0 deletions barretenberg/cpp/src/barretenberg/smt_verification/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ Then just build with `smt-verification` preset.

- ```set_variable_name(u32 index, str name)``` - assignes a name to a variable. Specifically, binds a name with the first index of an equivalence class.

**!Note that you don't have to name a zero or one(in standard). It has the name `zero` by default.**

- ```update_variable_names(u32 idx)``` - in case you've called ```assert_equal``` and ```update_real_variable_indices``` somewhere and you know that two or more variables from the equivalence class have separate names, call this method. Idx is the index of one of the variables of this class. The name of the first variable in class will remain.

- ```finalize_variable_names()``` - in case you don't want to mess with previous method, this one finds all the collisions and removes them.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -45,14 +45,9 @@ CircuitBase::CircuitBase(std::unordered_map<uint32_t, std::string>& variable_nam
*/
void CircuitBase::init()
{
variable_names.insert({ 0, "zero" });
variable_names_inverse.insert({ "zero", 0 });
symbolic_vars.insert({ 0, STerm::Var("zero" + this->tag, this->solver, this->type) });
optimized.insert({ 0, false });
size_t num_vars = this->variables.size();

size_t num_vars = variables.size();

for (uint32_t i = 1; i < num_vars; i++) {
for (uint32_t i = 0; i < num_vars; i++) {
uint32_t real_idx = this->real_variable_index[i];
if (this->symbolic_vars.contains(real_idx)) {
continue;
Expand All @@ -65,7 +60,7 @@ void CircuitBase::init()
optimized.insert({ real_idx, true });
}

symbolic_vars[0] == bb::fr(0);
this->symbolic_vars[this->variable_names_inverse["zero"]] == bb::fr::zero();
}

/**
Expand All @@ -83,4 +78,4 @@ STerm CircuitBase::operator[](const std::string& name)
return this->symbolic_vars[idx];
}

} // namespace smt_circuit
} // namespace smt_circuit
Original file line number Diff line number Diff line change
Expand Up @@ -24,12 +24,7 @@ StandardCircuit::StandardCircuit(
, selectors(circuit_info.selectors[0])
, wires_idxs(circuit_info.wires[0])
{
variable_names[1] = "one";
variable_names_inverse.insert({ "one", 1 });
symbolic_vars[1] = STerm::Var("one" + this->tag, this->solver, this->type);
symbolic_vars[1] == 1;
optimized[1] = false;

this->symbolic_vars[this->variable_names_inverse["one"]] == bb::fr::one();
// Perform all relaxations for gates or
// add gate in its normal state to solver
size_t i = 0;
Expand Down Expand Up @@ -264,7 +259,7 @@ size_t StandardCircuit::handle_logic_constraint(size_t cursor)
(j % single_iteration_size != relative_acc_idx) || (j == relative_acc_idx) ||
(this->wires_idxs[j + cursor][0] == this->wires_idxs[j + cursor - single_iteration_size][2]);
and_flag &=
(j % single_iteration_size != relative_acc_index) || (j == relative_acc_index) ||
(j % single_iteration_size != relative_acc_idx) || (j == relative_acc_idx) ||
(this->wires_idxs[j + cursor][0] == this->wires_idxs[j + cursor - single_iteration_size][2]);

if (!xor_flag && !and_flag) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -519,6 +519,8 @@ void StandardCircuitBuilder_<FF>::assert_equal_constant(uint32_t const a_idx, FF
*/
template <typename FF> msgpack::sbuffer StandardCircuitBuilder_<FF>::export_circuit()
{
this->set_variable_name(this->zero_idx, "zero");
this->set_variable_name(this->one_idx, "one");
using base = CircuitBuilderBase<FF>;
CircuitSchemaInternal<FF> cir;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2867,6 +2867,7 @@ template <typename ExecutionTrace> uint256_t UltraCircuitBuilder_<ExecutionTrace
*/
template <typename ExecutionTrace> msgpack::sbuffer UltraCircuitBuilder_<ExecutionTrace>::export_circuit()
{
this->set_variable_name(this->zero_idx, "zero");
using base = CircuitBuilderBase<FF>;
CircuitSchemaInternal<FF> cir;

Expand Down

1 comment on commit bbac3d9

@AztecBot
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'C++ Benchmark'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.05.

Benchmark suite Current: bbac3d9 Previous: 62a6b66 Ratio
nativeconstruct_proof_ultrahonk_power_of_2/20 5023.482313000002 ms/iter 4574.616918000003 ms/iter 1.10
Goblin::merge(t) 151546125 ns/iter 132029384 ns/iter 1.15

This comment was automatically generated by workflow using github-action-benchmark.

CC: @ludamad @codygunton

Please sign in to comment.