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: creating an smt checker for standard_circuit_builder #622

Draft
wants to merge 41 commits into
base: master
Choose a base branch
from
Draft
Changes from all commits
Commits
Show all changes
41 commits
Select commit Hold shift + click to select a range
6f25f18
added naming functionality to circuit_builder_base. Added export_circ…
Sarkoxed Jul 21, 2023
8c340ce
Merge branch 'master' into as/smt_checker
Sarkoxed Jul 21, 2023
50cc781
field_t tests
Sarkoxed Jul 25, 2023
fcfabfa
feat: Add the prototype of goblin translator circuit builder (#577)
Rumata888 Jul 27, 2023
e412be7
fixed set_variable_name + optimized finzlize_variable_name
Sarkoxed Jul 27, 2023
9c8b519
reorder the positions in json file + fixed witness indicies in gates
Sarkoxed Jul 27, 2023
c8dc7de
polynomial evaluation tests
Sarkoxed Jul 27, 2023
2f846c5
ff arithmetic + ordering
Sarkoxed Jul 27, 2023
d3ec72a
Merge branch 'master' into as/smt_checker
Sarkoxed Jul 27, 2023
b8f8050
cvc5 checker
Sarkoxed Aug 1, 2023
1827f64
Merge branch 'master' into as/smt_checker
Sarkoxed Aug 1, 2023
cdc63cd
added cvc5 submodule
Sarkoxed Aug 15, 2023
27090d4
msgpack circuit extraction + moved the tests
Sarkoxed Aug 15, 2023
28cb8dd
msgpack exctraction virtual function
Sarkoxed Aug 15, 2023
6db9040
side tests
Sarkoxed Aug 15, 2023
3a6be79
del
Sarkoxed Aug 15, 2023
9b85e43
Directory using cvc5
Sarkoxed Aug 15, 2023
2a68cc9
Merge branch 'master' into as/smt_checker
Sarkoxed Aug 15, 2023
b012ae2
Rename smt functions
Sarkoxed Aug 16, 2023
f36cde5
minor changes
Sarkoxed Aug 18, 2023
8b2d384
-
Sarkoxed Aug 18, 2023
9c25469
decorating the stuff
Sarkoxed Aug 19, 2023
a3f2de4
merge gone well...
Sarkoxed Aug 19, 2023
67ddd5f
massive change. Circuit, Solver and FFTerm classes added. Examples an…
Sarkoxed Aug 19, 2023
059a874
Merge branch 'master' into as/smt_checker
Sarkoxed Aug 19, 2023
c94f2ef
Cleaned up a little + Fixed Circuit.init()
Sarkoxed Aug 19, 2023
97597eb
Cleaned up
Sarkoxed Aug 19, 2023
7c56bea
fixing bugs
Sarkoxed Aug 19, 2023
4e09c8a
Fixed mistakes
Sarkoxed Aug 19, 2023
b1a03d6
Building cvc5 added to README
Sarkoxed Aug 21, 2023
aeb6727
fixed the issues stated during the call
Sarkoxed Aug 22, 2023
ded5cc5
exctract_circuit returns a buffer now
Sarkoxed Aug 22, 2023
79ce911
finally tests work
Sarkoxed Aug 22, 2023
c934b46
unique_witness in charge
Sarkoxed Aug 23, 2023
f8ffef0
batch_or improvement
Sarkoxed Aug 23, 2023
65d7e00
unique_witness test
Sarkoxed Aug 23, 2023
7563e53
Documentation
Sarkoxed Aug 29, 2023
17cd968
Bool and FFterm separation
Sarkoxed Aug 29, 2023
462c4d0
Unique witness function
Sarkoxed Aug 29, 2023
dc64592
Few bugs out
Sarkoxed Aug 29, 2023
48f8c88
Merge branch 'master' into as/smt_checker
Sarkoxed Aug 29, 2023
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
3 changes: 3 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -10,3 +10,6 @@
[submodule "build-system"]
path = build-system
url = git@github.com:AztecProtocol/build-system.git
[submodule "cpp/src/cvc5"]
path = cpp/src/cvc5
url = git@github.com:Sarkoxed/cvc5.git
25 changes: 25 additions & 0 deletions cpp/src/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -39,6 +39,29 @@ endif()

include_directories(${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/msgpack-c/include)

#include(ExternalProject)
#ExternalProject_Add(cvc5
# GIT_REPOSITORY https://github.com/Sarkoxed/cvc5
# GIT_TAG origin/finite-field-base-support
# SOURCE_DIR src/cvc5
# BINARY_DIR build-cvc5
# CMAKE_ARGS
# # -DCMAKE_INSTAL_PREFIX:PATH=
# # -DCMAKE_PREFIX_PATH="${CMAKE_BINARY_DIR}/tmp"
# -DCMAKE_BUILD_TYPE=Production
# -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}
# -DCMAKE_C_COMPILER=/usr/bin/clang
# -DCMAKE_CXX_COMPILER=/usr/bin/clang++
# -DENABLE_AUTO_DOWNLOAD=ON
# -DBUILD_SHARED_LIBS=OFF
# -DUSE_CRYPTOMINISAT=ON
# -DUSE_POLY=ON
# -DUSE_COCOA=ON
# )
include_directories(${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/tmp-build/include)
#add_subdirectory(cvc5)


# I feel this should be limited to ecc, however it's currently used in headers that go across libraries,
# and there currently isn't an easy way to inherit the DDISABLE_SHENANIGANS parameter.
if(DISABLE_ASM)
@@ -68,6 +91,8 @@ add_subdirectory(barretenberg/solidity_helpers)
add_subdirectory(barretenberg/wasi)
add_subdirectory(barretenberg/grumpkin_srs_gen)
add_subdirectory(barretenberg/bb)
add_subdirectory(barretenberg/smt_verification)


if(BENCHMARKS)
add_subdirectory(barretenberg/benchmark)
2 changes: 1 addition & 1 deletion cpp/src/barretenberg/crypto/blake3s/c_bind.cpp
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#include "barretenberg/ecc/curves/bn254/fr.hpp"
#include "barretenberg/common/wasm_export.hpp"
#include "barretenberg/ecc/curves/bn254/fr.hpp"
#include "blake3s.hpp"

WASM_EXPORT void blake3s_to_field(uint8_t const* data, size_t length, uint8_t* r)
2 changes: 1 addition & 1 deletion cpp/src/barretenberg/crypto/schnorr/schnorr.hpp
Original file line number Diff line number Diff line change
@@ -9,8 +9,8 @@
#include "barretenberg/crypto/hashers/hashers.hpp"

#include "barretenberg/common/serialize.hpp"
#include "barretenberg/serialize/msgpack.hpp"
#include "barretenberg/common/streams.hpp"
#include "barretenberg/serialize/msgpack.hpp"

namespace crypto {
namespace schnorr {
2 changes: 1 addition & 1 deletion cpp/src/barretenberg/crypto/sha256/c_bind.cpp
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#include "sha256.hpp"
#include "barretenberg/common/wasm_export.hpp"
#include "sha256.hpp"

WASM_EXPORT void sha256__hash(uint8_t* in, const size_t length, uint8_t* r)
{
6 changes: 3 additions & 3 deletions cpp/src/barretenberg/dsl/acir_format/recursion_constraint.cpp
Original file line number Diff line number Diff line change
@@ -88,9 +88,9 @@ void create_recursion_constraints(Builder& builder,
for (size_t i = 0; i < 4; ++i) {
aggregation_elements[i] =
bn254::BaseField(field_ct::from_witness_index(&builder, aggregation_input[4 * i]),
field_ct::from_witness_index(&builder, aggregation_input[4 * i + 1]),
field_ct::from_witness_index(&builder, aggregation_input[4 * i + 2]),
field_ct::from_witness_index(&builder, aggregation_input[4 * i + 3]));
field_ct::from_witness_index(&builder, aggregation_input[4 * i + 1]),
field_ct::from_witness_index(&builder, aggregation_input[4 * i + 2]),
field_ct::from_witness_index(&builder, aggregation_input[4 * i + 3]));
aggregation_elements[i].assert_is_in_field();
}
// If we have a previous aggregation object, assign it to `previous_aggregation` so that it is included
2 changes: 1 addition & 1 deletion cpp/src/barretenberg/honk/flavor/standard_grumpkin.hpp
Original file line number Diff line number Diff line change
@@ -33,7 +33,7 @@ class StandardGrumpkin {
using PolynomialHandle = std::span<FF>;
using CommitmentKey = pcs::CommitmentKey<Curve>;
using VerifierCommitmentKey = pcs::VerifierCommitmentKey<Curve>;

static constexpr size_t NUM_WIRES = CircuitBuilder::NUM_WIRES;
// The number of multivariate polynomials on which a sumcheck prover sumcheck operates (including shifts). We often
// need containers of this size to hold related data, so we choose a name more agnostic than `NUM_POLYNOMIALS`
2 changes: 1 addition & 1 deletion cpp/src/barretenberg/honk/pcs/claim.hpp
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#pragma once

#include "barretenberg/polynomials/polynomial.hpp"
#include "barretenberg/honk/pcs/commitment_key.hpp"
#include "barretenberg/polynomials/polynomial.hpp"

namespace proof_system::honk::pcs {
/**
7 changes: 5 additions & 2 deletions cpp/src/barretenberg/honk/pcs/commitment_key.test.hpp
Original file line number Diff line number Diff line change
@@ -46,7 +46,9 @@ template <typename CK> inline std::shared_ptr<CK> CreateCommitmentKey()

template <class VK> inline std::shared_ptr<VK> CreateVerifierCommitmentKey();

template <> inline std::shared_ptr<VerifierCommitmentKey<curve::BN254>> CreateVerifierCommitmentKey<VerifierCommitmentKey<curve::BN254>>()
template <>
inline std::shared_ptr<VerifierCommitmentKey<curve::BN254>> CreateVerifierCommitmentKey<
VerifierCommitmentKey<curve::BN254>>()
{
constexpr size_t n = 4096;
std::shared_ptr<barretenberg::srs::factories::CrsFactory<curve::BN254>> crs_factory(
@@ -55,7 +57,8 @@ template <> inline std::shared_ptr<VerifierCommitmentKey<curve::BN254>> CreateVe
}
// For IPA
template <>
inline std::shared_ptr<VerifierCommitmentKey<curve::Grumpkin>> CreateVerifierCommitmentKey<VerifierCommitmentKey<curve::Grumpkin>>()
inline std::shared_ptr<VerifierCommitmentKey<curve::Grumpkin>> CreateVerifierCommitmentKey<
VerifierCommitmentKey<curve::Grumpkin>>()
{
constexpr size_t n = 4096;
std::shared_ptr<barretenberg::srs::factories::CrsFactory<curve::Grumpkin>> crs_factory(
12 changes: 6 additions & 6 deletions cpp/src/barretenberg/honk/pcs/gemini/gemini.cpp
Original file line number Diff line number Diff line change
@@ -53,8 +53,10 @@ namespace proof_system::honk::pcs::gemini {
* @return std::vector<Polynomial>
*/
template <typename Curve>
std::vector<typename barretenberg::Polynomial<typename Curve::ScalarField>> GeminiProver_<Curve>::compute_fold_polynomials(
std::span<const Fr> mle_opening_point, Polynomial&& batched_unshifted, Polynomial&& batched_to_be_shifted)
std::vector<typename barretenberg::Polynomial<typename Curve::ScalarField>> GeminiProver_<
Curve>::compute_fold_polynomials(std::span<const Fr> mle_opening_point,
Polynomial&& batched_unshifted,
Polynomial&& batched_to_be_shifted)
{
const size_t num_variables = mle_opening_point.size(); // m

@@ -141,9 +143,8 @@ std::vector<typename barretenberg::Polynomial<typename Curve::ScalarField>> Gemi
* @param r_challenge univariate opening challenge
*/
template <typename Curve>
ProverOutput<Curve> GeminiProver_<Curve>::compute_fold_polynomial_evaluations(std::span<const Fr> mle_opening_point,
std::vector<Polynomial>&& fold_polynomials,
const Fr& r_challenge)
ProverOutput<Curve> GeminiProver_<Curve>::compute_fold_polynomial_evaluations(
std::span<const Fr> mle_opening_point, std::vector<Polynomial>&& fold_polynomials, const Fr& r_challenge)
{
const size_t num_variables = mle_opening_point.size(); // m

@@ -186,7 +187,6 @@ ProverOutput<Curve> GeminiProver_<Curve>::compute_fold_polynomial_evaluations(st
return { fold_poly_opening_pairs, std::move(fold_polynomials) };
};


template class GeminiProver_<curve::BN254>;
template class GeminiProver_<curve::Grumpkin>;
}; // namespace proof_system::honk::pcs::gemini
8 changes: 4 additions & 4 deletions cpp/src/barretenberg/honk/pcs/gemini/gemini.test.cpp
Original file line number Diff line number Diff line change
@@ -86,10 +86,10 @@ template <class Curve> class GeminiTest : public CommitmentTest<Curve> {
// - 2 partially evaluated Fold polynomial commitments [Fold_{r}^(0)] and [Fold_{-r}^(0)]
// Aggregate: d+1 opening pairs and d+1 Fold poly commitments into verifier claim
auto verifier_claim = GeminiVerifier::reduce_verification(multilinear_evaluation_point,
batched_evaluation,
batched_commitment_unshifted,
batched_commitment_to_be_shifted,
verifier_transcript);
batched_evaluation,
batched_commitment_unshifted,
batched_commitment_to_be_shifted,
verifier_transcript);

// Check equality of the opening pairs computed by prover and verifier
for (size_t i = 0; i < (log_n + 1); ++i) {
14 changes: 8 additions & 6 deletions cpp/src/barretenberg/honk/pcs/ipa/ipa.test.cpp
Original file line number Diff line number Diff line change
@@ -152,7 +152,8 @@ TEST_F(IPATest, GeminiShplonkIPAWithShift)
}

const Fr nu_challenge = prover_transcript.get_challenge("Shplonk:nu");
auto batched_quotient_Q = ShplonkProver::compute_batched_quotient(gemini_opening_pairs, gemini_witnesses, nu_challenge);
auto batched_quotient_Q =
ShplonkProver::compute_batched_quotient(gemini_opening_pairs, gemini_witnesses, nu_challenge);
prover_transcript.send_to_verifier("Shplonk:Q", this->ck()->commit(batched_quotient_Q));

const Fr z_challenge = prover_transcript.get_challenge("Shplonk:z");
@@ -164,12 +165,13 @@ TEST_F(IPATest, GeminiShplonkIPAWithShift)
auto verifier_transcript = VerifierTranscript<Fr>::init_empty(prover_transcript);

auto gemini_verifier_claim = GeminiVerifier::reduce_verification(mle_opening_point,
batched_evaluation,
batched_commitment_unshifted,
batched_commitment_to_be_shifted,
verifier_transcript);
batched_evaluation,
batched_commitment_unshifted,
batched_commitment_to_be_shifted,
verifier_transcript);

const auto shplonk_verifier_claim = ShplonkVerifier::reduce_verification(this->vk(), gemini_verifier_claim, verifier_transcript);
const auto shplonk_verifier_claim =
ShplonkVerifier::reduce_verification(this->vk(), gemini_verifier_claim, verifier_transcript);
bool verified = IPA::verify(this->vk(), shplonk_verifier_claim, verifier_transcript);

EXPECT_EQ(verified, true);
14 changes: 8 additions & 6 deletions cpp/src/barretenberg/honk/pcs/kzg/kzg.test.cpp
Original file line number Diff line number Diff line change
@@ -140,7 +140,8 @@ TYPED_TEST(KZGTest, GeminiShplonkKzgWithShift)
// - opening pair: (z_challenge, 0)
// - witness: polynomial Q - Q_z
const Fr nu_challenge = prover_transcript.get_challenge("Shplonk:nu");
auto batched_quotient_Q = ShplonkProver::compute_batched_quotient(gemini_opening_pairs, gemini_witnesses, nu_challenge);
auto batched_quotient_Q =
ShplonkProver::compute_batched_quotient(gemini_opening_pairs, gemini_witnesses, nu_challenge);
prover_transcript.send_to_verifier("Shplonk:Q", this->ck()->commit(batched_quotient_Q));

const Fr z_challenge = prover_transcript.get_challenge("Shplonk:z");
@@ -158,13 +159,14 @@ TYPED_TEST(KZGTest, GeminiShplonkKzgWithShift)
// Gemini verifier output:
// - claim: d+1 commitments to Fold_{r}^(0), Fold_{-r}^(0), Fold^(l), d+1 evaluations a_0_pos, a_l, l = 0:d-1
auto gemini_verifier_claim = GeminiVerifier::reduce_verification(mle_opening_point,
batched_evaluation,
batched_commitment_unshifted,
batched_commitment_to_be_shifted,
verifier_transcript);
batched_evaluation,
batched_commitment_unshifted,
batched_commitment_to_be_shifted,
verifier_transcript);

// Shplonk verifier claim: commitment [Q] - [Q_z], opening point (z_challenge, 0)
const auto shplonk_verifier_claim = ShplonkVerifier::reduce_verification(this->vk(), gemini_verifier_claim, verifier_transcript);
const auto shplonk_verifier_claim =
ShplonkVerifier::reduce_verification(this->vk(), gemini_verifier_claim, verifier_transcript);

// KZG verifier:
// aggregates inputs [Q] - [Q_z] and [W] into an 'accumulator' (can perform pairing check on result)
5 changes: 3 additions & 2 deletions cpp/src/barretenberg/honk/pcs/shplonk/shplonk.test.cpp
Original file line number Diff line number Diff line change
@@ -52,8 +52,9 @@ TYPED_TEST(ShplonkTest, ShplonkSimple)
prover_transcript.send_to_verifier("Shplonk:Q", this->ck()->commit(batched_quotient_Q));

const Fr z_challenge = prover_transcript.get_challenge("Shplonk:z");
const auto [prover_opening_pair, shplonk_prover_witness] = ShplonkProver::compute_partially_evaluated_batched_quotient(
opening_pairs, polynomials, std::move(batched_quotient_Q), nu_challenge, z_challenge);
const auto [prover_opening_pair, shplonk_prover_witness] =
ShplonkProver::compute_partially_evaluated_batched_quotient(
opening_pairs, polynomials, std::move(batched_quotient_Q), nu_challenge, z_challenge);

// An intermediate check to confirm the opening of the shplonk prover witness Q
this->verify_opening_pair(prover_opening_pair, shplonk_prover_witness);
9 changes: 5 additions & 4 deletions cpp/src/barretenberg/honk/pcs/verification_key.hpp
Original file line number Diff line number Diff line change
@@ -26,7 +26,7 @@ template <class Curve> class VerifierCommitmentKey;

/**
* @brief Specialization for bn254
*
*
* @tparam curve::BN254
*/
template <> class VerifierCommitmentKey<curve::BN254> {
@@ -44,7 +44,7 @@ template <> class VerifierCommitmentKey<curve::BN254> {
* @param srs verifier G2 point
*/
VerifierCommitmentKey([[maybe_unused]] size_t num_points,
std::shared_ptr<barretenberg::srs::factories::CrsFactory<Curve>> crs_factory)
std::shared_ptr<barretenberg::srs::factories::CrsFactory<Curve>> crs_factory)
: srs(crs_factory->get_verifier_crs())
{}

@@ -70,7 +70,7 @@ template <> class VerifierCommitmentKey<curve::BN254> {

/**
* @brief Specialization for Grumpkin
*
*
* @tparam curve::Grumpkin
*/
template <> class VerifierCommitmentKey<curve::Grumpkin> {
@@ -88,7 +88,8 @@ template <> class VerifierCommitmentKey<curve::Grumpkin> {
* @param num_points specifies the length of the SRS
* @param path is the location to the SRS file
*/
VerifierCommitmentKey(size_t num_points, std::shared_ptr<barretenberg::srs::factories::CrsFactory<Curve>> crs_factory)
VerifierCommitmentKey(size_t num_points,
std::shared_ptr<barretenberg::srs::factories::CrsFactory<Curve>> crs_factory)
: pippenger_runtime_state(num_points)
, srs(crs_factory->get_verifier_crs(num_points))

8 changes: 4 additions & 4 deletions cpp/src/barretenberg/honk/proof_system/verifier.cpp
Original file line number Diff line number Diff line change
@@ -154,10 +154,10 @@ template <typename Flavor> bool StandardVerifier_<Flavor>::verify_proof(const pl
// - d+1 commitments [Fold_{r}^(0)], [Fold_{-r}^(0)], and [Fold^(l)], l = 1:d-1
// - d+1 evaluations a_0_pos, and a_l, l = 0:d-1
auto gemini_claim = Gemini::reduce_verification(multivariate_challenge,
batched_evaluation,
batched_commitment_unshifted,
batched_commitment_to_be_shifted,
transcript);
batched_evaluation,
batched_commitment_unshifted,
batched_commitment_to_be_shifted,
transcript);

// Produce a Shplonk claim: commitment [Q] - [Q_z], evaluation zero (at random challenge z)
auto shplonk_claim = Shplonk::reduce_verification(pcs_verification_key, gemini_claim, transcript);
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#include "barycentric_data.hpp"
#include "barretenberg/ecc/curves/bn254/fr.hpp"
#include "barycentric_data.hpp"

#include "barretenberg/numeric/random/engine.hpp"
#include <gtest/gtest.h>
8 changes: 4 additions & 4 deletions cpp/src/barretenberg/honk/sumcheck/sumcheck.hpp
Original file line number Diff line number Diff line change
@@ -77,8 +77,8 @@ template <typename Flavor> class SumcheckProver {
*
* @details
*/
SumcheckOutput<Flavor> prove(
auto full_polynomials, const RelationParameters<FF>& relation_parameters) // pass by value, not by reference
SumcheckOutput<Flavor> prove(auto full_polynomials,
const RelationParameters<FF>& relation_parameters) // pass by value, not by reference
{
auto [alpha, zeta] = transcript.get_challenges("Sumcheck:alpha", "Sumcheck:zeta");

@@ -176,8 +176,8 @@ template <typename Flavor> class SumcheckVerifier {
* target sum.
*
* @details If verification fails, returns std::nullopt, otherwise returns SumcheckOutput
* @param relation_parameters
* @param transcript
* @param relation_parameters
* @param transcript
*/
std::optional<SumcheckOutput<Flavor>> verify(const RelationParameters<FF>& relation_parameters, auto& transcript)
{
1 change: 1 addition & 0 deletions cpp/src/barretenberg/honk/transcript/transcript.hpp
Original file line number Diff line number Diff line change
@@ -67,6 +67,7 @@ template <typename FF> class BaseTranscript {
// TODO(Adrian): Make these tweakable
public:
static constexpr size_t HASH_OUTPUT_SIZE = 32;

private:
static constexpr size_t MIN_BYTES_PER_CHALLENGE = 128 / 8; // 128 bit challenges

2 changes: 1 addition & 1 deletion cpp/src/barretenberg/plonk/composer/composer_lib.cpp
Original file line number Diff line number Diff line change
@@ -3,8 +3,8 @@
* @brief Contains some functions that are shared between the various Plonk composers.
*/
#include "composer_lib.hpp"
#include "barretenberg/srs/factories/crs_factory.hpp"
#include "barretenberg/honk/pcs/commitment_key.hpp"
#include "barretenberg/srs/factories/crs_factory.hpp"

namespace proof_system::plonk {

Loading