From f7acad39ea36cbdd89320d346639c8ff63a544c8 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 21 Nov 2024 22:30:10 +0000 Subject: [PATCH] Zero index inclusion fix --- .../cpp/src/barretenberg/smt_verification/README.md | 2 ++ .../smt_verification/circuit/circuit_base.cpp | 13 ++++--------- .../smt_verification/circuit/standard_circuit.cpp | 9 ++------- .../standard_circuit_builder.cpp | 2 ++ .../ultra_circuit_builder.cpp | 1 + 5 files changed, 11 insertions(+), 16 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/README.md b/barretenberg/cpp/src/barretenberg/smt_verification/README.md index 680c974e469b..c62f07516fef 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/README.md +++ b/barretenberg/cpp/src/barretenberg/smt_verification/README.md @@ -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. diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp index edde7e005cf4..77e8f8f864a4 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp @@ -45,14 +45,9 @@ CircuitBase::CircuitBase(std::unordered_map& 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; @@ -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(); } /** @@ -83,4 +78,4 @@ STerm CircuitBase::operator[](const std::string& name) return this->symbolic_vars[idx]; } -} // namespace smt_circuit \ No newline at end of file +} // namespace smt_circuit diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp index 6d68d93333d0..5b47ba23afbc 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp @@ -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; @@ -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) { diff --git a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.cpp b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.cpp index b2fada856cbb..09e74567e40d 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.cpp +++ b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.cpp @@ -519,6 +519,8 @@ void StandardCircuitBuilder_::assert_equal_constant(uint32_t const a_idx, FF */ template msgpack::sbuffer StandardCircuitBuilder_::export_circuit() { + this->set_variable_name(this->zero_idx, "zero"); + this->set_variable_name(this->one_idx, "one"); using base = CircuitBuilderBase; CircuitSchemaInternal cir; diff --git a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp index 19c63fc87af3..29bf01cc42cf 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp +++ b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp @@ -2867,6 +2867,7 @@ template uint256_t UltraCircuitBuilder_ msgpack::sbuffer UltraCircuitBuilder_::export_circuit() { + this->set_variable_name(this->zero_idx, "zero"); using base = CircuitBuilderBase; CircuitSchemaInternal cir;