Merge f7acad3 into 95e8406

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.

barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.cpp

@@ -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;
@@ -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
+} // namespace smt_circuit

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) {

barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/standard_circuit_builder.cpp

@@ -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;
 

barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp

@@ -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;