formal_proofs.hpp

Go to the documentation of this file.

#pragma once
#include "acir_loader.hpp"
#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
#include "barretenberg/smt_verification/solver/solver.hpp"
#include "cvc5/cvc5.h"
#include <string>
#include <unordered_map>
void debug_solution(smt_solver::Solver* solver, std::unordered_map<std::string, cvc5::Term> terms);
 
bool verify_add(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_sub(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_mul(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_div(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_div_field(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_mod(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_or(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_and(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_xor(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_not_127(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_shl32(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_shl64(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_shr(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_eq_on_equlaity(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_eq_on_inequlaity(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_lt(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_gt(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit);
 
bool verify_non_uniqueness_for_casts(smt_solver::Solver* solver, AcirToSmtLoader* loader, smt_circuit::TermType type);