Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Acir formal proofs #10973

Merged
merged 35 commits into from
Jan 7, 2025
Merged
Changes from 1 commit
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
a837887
IT FINALLY WORKS :D
jewelofchaos9 Nov 18, 2024
5750f4c
i forgot cmakelists
jewelofchaos9 Nov 18, 2024
cc71c30
save artifacts
jewelofchaos9 Nov 18, 2024
a791e76
stable version for verifying
jewelofchaos9 Nov 21, 2024
56559cf
dummy
jewelofchaos9 Nov 22, 2024
c364e63
IT FINALLY WORKS :D
jewelofchaos9 Nov 18, 2024
579c5ff
i forgot cmakelists
jewelofchaos9 Nov 18, 2024
be6ef36
save artifacts
jewelofchaos9 Nov 18, 2024
6b27d0e
stable version for verifying
jewelofchaos9 Nov 21, 2024
84319b2
dummy
jewelofchaos9 Nov 22, 2024
28cd1f9
smol refactor
jewelofchaos9 Nov 25, 2024
8ea00fc
smol refactor
jewelofchaos9 Nov 25, 2024
2ff5084
smol refactor
jewelofchaos9 Nov 25, 2024
58c1268
forgot to resolve merge conflicts
jewelofchaos9 Nov 25, 2024
e1a6541
i forgor to resolve conflicts in cargolock...
Nov 26, 2024
7dd7e98
hmm
jewelofchaos9 Nov 27, 2024
d58a19a
smol refactor
jewelofchaos9 Nov 29, 2024
4f07105
ples have a patient i have problems
jewelofchaos9 Dec 2, 2024
e33a29f
verif changes
jewelofchaos9 Dec 3, 2024
802b0cd
smol shifts
jewelofchaos9 Dec 9, 2024
d7dd95d
deleted codegen + shl + shr
jewelofchaos9 Dec 12, 2024
2cf19f0
bug in acir builder
jewelofchaos9 Dec 12, 2024
10b361f
recaftor
jewelofchaos9 Dec 16, 2024
3cc7f44
docs + small refactor
jewelofchaos9 Dec 27, 2024
884b2aa
readme mistake, artifacts dirs
jewelofchaos9 Dec 27, 2024
ef9c730
restore cmake list
jewelofchaos9 Dec 27, 2024
208f9ce
bug in verify_mod
jewelofchaos9 Dec 27, 2024
97bfad1
still bug in verify_mod
jewelofchaos9 Dec 27, 2024
1c90845
deleted gitignores + table + shl64 bug + directory flag for binary
jewelofchaos9 Jan 6, 2025
442e387
readme mistake, deleted all noir stuff
jewelofchaos9 Jan 6, 2025
29ed080
broken table
jewelofchaos9 Jan 6, 2025
f32a27e
last readme fix
jewelofchaos9 Jan 6, 2025
d9d77f5
Merge branch 'master' into sa/acir_formal_proofs
jewelofchaos9 Jan 6, 2025
d800214
Merge branch 'master' of https://github.com/AztecProtocol/aztec-packa…
jewelofchaos9 Jan 7, 2025
9dd4709
ACIR_FORMAL_PROOFS flag for cmake
jewelofchaos9 Jan 7, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
forgot to resolve merge conflicts
  • Loading branch information
jewelofchaos9 committed Nov 25, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 58c1268eee6c3468cae382b857403ea9f32c4acd
Original file line number Diff line number Diff line change
@@ -1,19 +1,12 @@
#include "acir_loader.hpp"
#include "barretenberg/dsl/acir_format/acir_format.hpp"
#include "barretenberg/dsl/acir_format/acir_to_constraint_buf.hpp"
<<<<<<< HEAD
#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
#include "barretenberg/smt_verification/terms/term.hpp"
#include "msgpack/v3/sbuffer_decl.hpp"
#include <fstream>
#include <string>
#include <vector>
=======
#include <vector>
#include <string>
#include <fstream>

>>>>>>> 56559cf7fce08564b1b28ebe20726ba486af2379

std::vector<uint8_t> readFile(std::string filename)
{
@@ -28,18 +21,11 @@ std::vector<uint8_t> readFile(std::string filename)

std::vector<uint8_t> vec;

<<<<<<< HEAD
vec.insert(vec.begin(), std::istream_iterator<uint8_t>(file), std::istream_iterator<uint8_t>());
=======
vec.insert(vec.begin(),
std::istream_iterator<uint8_t>(file),
std::istream_iterator<uint8_t>());
>>>>>>> 56559cf7fce08564b1b28ebe20726ba486af2379
file.close();
return vec;
}

<<<<<<< HEAD
AcirToSmtLoader::AcirToSmtLoader(std::string filename)
{
this->acir_program_buf = readFile(filename);
@@ -66,18 +52,4 @@ smt_circuit::UltraCircuit AcirToSmtLoader::get_circuit(smt_solver::Solver* solve
{
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);
=======

AcirInstructionLoader::AcirInstructionLoader(std::vector<uint8_t> const& acir_bytes, std::string instruction_name)
{
this->acir_program_buf = acir_bytes;
this->instruction_name = instruction_name;
this->constraint_systems = acir_format::program_buf_to_acir_format(acir_bytes, false);
}

AcirInstructionLoader::AcirInstructionLoader(std::string filename) {
this->acir_program_buf = readFile(filename);
this->instruction_name = filename;
this->constraint_systems = acir_format::program_buf_to_acir_format(this->acir_program_buf, false);
>>>>>>> 56559cf7fce08564b1b28ebe20726ba486af2379
}
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
#pragma once
#include "barretenberg/dsl/acir_format/acir_format.hpp"
<<<<<<< HEAD
#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
#include "msgpack/v3/sbuffer_decl.hpp"
#include <string>
@@ -26,29 +25,4 @@ class AcirToSmtLoader {
std::vector<uint8_t> acir_program_buf;
acir_format::AcirFormat constraint_system;
msgpack::sbuffer circuit_buf;
=======
#include <vector>
#include <string>


class AcirInstructionLoader {
public:
AcirInstructionLoader() = default;
AcirInstructionLoader(const AcirInstructionLoader& other) = default;
AcirInstructionLoader(AcirInstructionLoader&& other) = default;
AcirInstructionLoader& operator=(const AcirInstructionLoader other) = delete;
AcirInstructionLoader&& operator=(AcirInstructionLoader&& other) = delete;

~AcirInstructionLoader() = default;

AcirInstructionLoader(std::vector<uint8_t> const& acir_program_buf, std::string instruction_name);
AcirInstructionLoader(std::string filename);

std::vector<acir_format::AcirFormat> get_constraint_systems() { return this->constraint_systems; }

private:
std::string instruction_name;
std::vector<uint8_t> acir_program_buf;
std::vector<acir_format::AcirFormat> constraint_systems;
>>>>>>> 56559cf7fce08564b1b28ebe20726ba486af2379
};
Original file line number Diff line number Diff line change
@@ -3,18 +3,13 @@
#include "barretenberg/common/test.hpp"
#include "barretenberg/dsl/acir_format/acir_format.hpp"
#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
<<<<<<< HEAD
#include "barretenberg/smt_verification/solver/solver.hpp"
=======
>>>>>>> 56559cf7fce08564b1b28ebe20726ba486af2379
#include "barretenberg/stdlib/client_ivc_verifier/client_ivc_recursive_verifier.hpp"
#include "barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp"
#include <vector>

<<<<<<< HEAD
TEST(acir_formal_proofs, uint_terms_add)
{
AcirToSmtLoader loader = AcirToSmtLoader("../src/barretenberg/acir_formal_proofs/artifacts/Binary::Add.acir");
smt_solver::Solver solver = loader.get_solver();
smt_circuit::UltraCircuit circuit = loader.get_circuit(&solver);
auto a = circuit["a"];
@@ -203,110 +198,3 @@ TEST(acir_formal_proofs, uint_terms_xor)
info(solver.getResult());
EXPECT_FALSE(res);
}
=======
TEST(acir_formal_proofs, slow)
{
AcirInstructionLoader add =
AcirInstructionLoader("../src/barretenberg/acir_formal_proofs/artifacts/Binary::Add.acir");
auto system = add.get_constraint_systems().at(0);
bb::UltraCircuitBuilder builder = acir_format::create_circuit(system, false);
info(builder.public_inputs);
// info(builder.variables);
builder.set_variable_name(0, "a");
builder.set_variable_name(1, "b");
builder.set_variable_name(2, "c");
builder.set_variable_name(3, "d");
builder.set_variable_name(4, "e");
EXPECT_TRUE(bb::CircuitChecker::check(builder));

auto buf = builder.export_circuit();
smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(buf);
smt_solver::Solver s(circuit_info.modulus);
smt_circuit::UltraCircuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm);
auto a = circuit["a"];
auto b = circuit["b"];
auto c = circuit["c"];
info(c);
auto cr = a + b;
c != cr;
bool res = s.check();
EXPECT_TRUE(false);
s.print_assertions();
info(s.getResult());
EXPECT_FALSE(res);
}

TEST(acir_formal_proofs, uint_terms_add)
{
AcirInstructionLoader add =
AcirInstructionLoader("../src/barretenberg/acir_formal_proofs/artifacts/Binary::Add.acir");
auto system = add.get_constraint_systems().at(0);
bb::UltraCircuitBuilder builder = acir_format::create_circuit(system, false);
info(builder.public_inputs);
// info(builder.variables);
builder.set_variable_name(0, "a");
builder.set_variable_name(1, "b");
builder.set_variable_name(2, "c");
builder.set_variable_name(3, "d");
builder.set_variable_name(4, "e");
EXPECT_TRUE(bb::CircuitChecker::check(builder));

auto buf = builder.export_circuit();
smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(buf);
smt_solver::Solver s(circuit_info.modulus);
smt_circuit::UltraCircuit circuit(circuit_info, &s, smt_terms::TermType::BVTerm);
auto a = circuit["a"];
auto b = circuit["b"];
auto c = circuit["c"];
info(c);
auto cr = a + b;
c != cr;
bool res = s.check();
EXPECT_TRUE(false);
s.print_assertions();
info(s.getResult());
EXPECT_FALSE(res);
}

TEST(acir_formal_proofs, public_inputs)
{
AcirInstructionLoader add =
AcirInstructionLoader("../src/barretenberg/acir_formal_proofs/artifacts/Binary::Add.public.acir");
auto system = add.get_constraint_systems().at(0);
bb::UltraCircuitBuilder builder = acir_format::create_circuit(system, false);
// builder.zero_idx = 4;
info(builder.zero_idx);
info("Public inputs in builder", builder.public_inputs);
info(builder.real_variable_index[2]);
info(builder.real_variable_index[3]);
builder.variables[0] = 10;
builder.variables[1] = 10;
// if we set second variable check circuit throws error :(, so output in third???
builder.variables[3] = 20;
EXPECT_TRUE(bb::CircuitChecker::check(builder));

builder.set_variable_name(0, "a");
builder.set_variable_name(1, "b");
builder.set_variable_name(2, "c");
builder.set_variable_name(3, "d");
builder.set_variable_name(4, "e");
EXPECT_TRUE(bb::CircuitChecker::check(builder));

auto buf = builder.export_circuit();
smt_circuit::CircuitSchema circuit_info = smt_circuit_schema::unpack_from_buffer(buf);
info("Circuit info public inputs", circuit_info.public_inps);
smt_solver::Solver s(circuit_info.modulus);
smt_circuit::UltraCircuit circuit(circuit_info, &s, smt_terms::TermType::BVTerm);
auto a = circuit["a"];
auto b = circuit["b"];
auto c = circuit["c"];
info(c);
auto cr = a + b;
c != cr;
bool res = s.check();
EXPECT_TRUE(false);
s.print_assertions();
info(s.getResult());
EXPECT_FALSE(res);
}
>>>>>>> 56559cf7fce08564b1b28ebe20726ba486af2379
1 change: 0 additions & 1 deletion noir/noir-repo/compiler/noirc_evaluator/Cargo.toml
Original file line number Diff line number Diff line change
@@ -26,7 +26,6 @@ serde_json.workspace = true
serde_with = "3.2.0"
tracing.workspace = true
chrono = "0.4.37"
flate2 = "1.0.35"
rayon.workspace = true
cfg-if.workspace = true

Loading