acir_loader.cpp

Go to the documentation of this file.

#include "acir_loader.hpp"
#include "barretenberg/dsl/acir_format/acir_format.hpp"
#include "barretenberg/dsl/acir_format/acir_to_constraint_buf.hpp"
#include "barretenberg/serialize/msgpack_impl.hpp"
#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
#include "barretenberg/smt_verification/terms/term.hpp"
#include <fstream>
#include <string>
#include <vector>
 
std::vector<uint8_t> readFile(std::string filename)
{
    std::ifstream file(filename, std::ios::binary);
    file.unsetf(std::ios::skipws);
 
    std::streampos fileSize;
 
    file.seekg(0, std::ios::end);
    fileSize = file.tellg();
    file.seekg(0, std::ios::beg);
 
    std::vector<uint8_t> vec;
 
    vec.insert(vec.begin(), std::istream_iterator<uint8_t>(file), std::istream_iterator<uint8_t>());
    file.close();
    return vec;
}
 
AcirToSmtLoader::AcirToSmtLoader(std::string filename)
{
    this->instruction_name = filename;
    this->constraint_system = acir_format::circuit_buf_to_acir_format(readFile(filename));
    this->circuit_buf = this->get_circuit_builder().export_circuit();
}
 
bb::UltraCircuitBuilder AcirToSmtLoader::get_circuit_builder()
{
    acir_format::AcirProgram program{ .constraints = this->constraint_system };
    auto builder = acir_format::create_circuit<bb::UltraCircuitBuilder>(program);
    builder.set_variable_name(0, "a");
    builder.set_variable_name(1, "b");
    builder.set_variable_name(2, "c");
    return builder;
}
 
smt_solver::Solver AcirToSmtLoader::get_smt_solver()
{
    smt_circuit::CircuitSchema circuit_info = this->get_circuit_schema();
    // In circuits generated by the shift left (shl) opcode, there is a variable with bit length 197.
    // This is likely because the shl operation internally calls truncate opcode to handle overflow
    return smt_solver::Solver(circuit_info.modulus, smt_circuit::default_solver_config, 16, 255);
}
 
smt_circuit::CircuitSchema AcirToSmtLoader::get_circuit_schema()
{
    return smt_circuit_schema::unpack_from_buffer(this->circuit_buf);
}
 
smt_circuit::UltraCircuit AcirToSmtLoader::get_bitvec_smt_circuit(smt_solver::Solver* solver)
{
    smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(this->circuit_buf);
    return smt_circuit::UltraCircuit(circuit_info, solver, smt_terms::TermType::BVTerm);
}
 
smt_circuit::UltraCircuit AcirToSmtLoader::get_field_smt_circuit(smt_solver::Solver* solver)
{
    smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(this->circuit_buf);
    return smt_circuit::UltraCircuit(circuit_info, solver, smt_terms::TermType::FFTerm);
}
 
smt_circuit::UltraCircuit AcirToSmtLoader::get_integer_smt_circuit(smt_solver::Solver* solver)
{
    smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(this->circuit_buf);
    return smt_circuit::UltraCircuit(circuit_info, solver, smt_terms::TermType::ITerm);
}