feat: Merge SMT Terms in one class #5254

Sarkoxed · 2024-03-15T16:57:20Z

This pr brings major changes in symbolic terms usage.

STerm

A new class that is merged from FFTerm and FFITerm classes. Now you can use FFTerm or FFITerm by providing a TermType::FFTerm or TermType::FFITerm to STerm constructor.

All the operations are now stored in unordered_map<OpType, cvc5::Kind> operations. e.g. if the type is FFTerm, then operations[OpType::ADD] = cvc5::Kind::FINITE_FIELD_ADD, and operations[OpType::ADD] = cvc5::Kind::ADD for FFITerm

Also now you can use new BVTerm type. It can be used to solve constraints with lots of bitwise operations. However, it can be used only once all the optimizations are added. You simply can't use it to simulate finite field operations and it's not really optimal.

Symbolic variables can be initialized using new functions FFVar, FFIVar and BVVar

Solver

Added bv_sort member

Added bitvector operations parser to stringify_term

Circuit

No more templates. All the circuit methods are moved to .cpp file

Fixes:

range constraint is now made to be <= 2^n - 1 instead of < 2^n
changed xor_gate to logic_gate in info function
Removed setting optimized variables to zero, since it didn't affect anything except polluted output
Restored public_variables initialization. It was deleted some time ago. I don't know why.

Utils

smt_timer now has bool mins param, that tells in what format to output elapsed time

STerm: - fixed lots of errors in methods Tests: - fixed old ones to use STerm class - added new tests to check for unsupported functionality

- Switch to field_t native operations - Switch to the new STerm api - Use smt_timer

- removed zero initialization for optimized variables, since it doesn't do anything helpful - fixed logic_flag output - fixed range constraint so it now fits in bitvector size

Rumata888 · 2024-03-19T16:15:05Z

barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp

+
+// MUL, LSH, RSH, AND and OR are not tested, since they are not bijective
+
+TEST(BVTerm, unsupported_operations)


What does this test do exactly?

Rumata888 · 2024-03-19T16:23:45Z

barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp

+    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct b = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct c = a + b;
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32);


What are the values 16 and 32?

Rumata888 · 2024-03-19T16:33:49Z

barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp

 namespace {
 auto& engine = numeric::get_debug_randomness();
 }

-msgpack::sbuffer create_circuit(size_t n, bool pub_coeffs)
+msgpack::sbuffer create_polynomial_evaluation_circuit(size_t n, bool pub_coeffs)


What do we need this for?

I'm using this function in the two tests below. Since it is quite large, I decided to take it out separately.

Rumata888 · 2024-03-19T17:33:14Z

barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp

    std::string bvals = s.getValue(bval.term).getIntegerValue();
    ASSERT_EQ(bvals, yvals);
 }
+
+TEST(FFITerm, unsupported_operations)


What does this function do?

Rumata888 · 2024-03-19T17:33:38Z

barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp

    std::string bvals = s.getValue(bval.term).getFiniteFieldValue();
    ASSERT_EQ(bvals, yvals);
+}
+
+TEST(FFTerm, unsupported_operations)


What does this function do?

Rumata888 · 2024-03-19T17:34:46Z

barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp

+ */
+STerm STerm::operator/(const STerm& other) const
+{
+    if (!this->operations.contains(OpType::DIV)) {


Uhm. Why can't you replace it with multilication and non-zero?

Because of BitVectors. They are not supposed to be divided by each other(well at least not like the real division, truncated - maybe. At least for now they are not)

Rumata888

Please address my comments

AztecBot · 2024-03-19T23:16:21Z

Benchmark results

No metrics with a significant change found.

Detailed results

All benchmarks are run on txs on the Benchmarking contract on the repository. Each tx consists of a batch call to create_note and increment_balance, which guarantees that each tx has a private call, a nested private call, a public call, and a nested public call, as well as an emitted private note, an unencrypted log, and public storage read and write.

This benchmark source data is available in JSON format on S3 here.

Values are compared against data from master at commit 10ef9702 and shown if the difference exceeds 1%.

L2 block published to L1

Each column represents the number of txs on an L2 block published to L1.

Metric	8 txs	32 txs	64 txs
l1_rollup_calldata_size_in_bytes	5,668	18,820	36,356
l1_rollup_calldata_gas	66,400	239,068	468,992
l1_rollup_execution_gas	647,498	929,426	1,305,172
l2_block_processing_time_in_ms	1,301	4,684 (-2%)	8,965 (-4%)
note_successful_decrypting_time_in_ms	194 (+12%)	515 (-8%)	983 (-1%)
note_trial_decrypting_time_in_ms	98.5 (+31%)	30.5 (-61%)	115 (-8%)
l2_block_building_time_in_ms	18,073	68,326	135,850 (-1%)
l2_block_rollup_simulation_time_in_ms	8,053	28,563	56,502
l2_block_public_tx_process_time_in_ms	9,999 (-1%)	39,708 (-1%)	79,254 (-1%)

L2 chain processing

Each column represents the number of blocks on the L2 chain where each block has 16 txs.

Metric	5 blocks	10 blocks
node_history_sync_time_in_ms	14,521 (-1%)	27,418 (+3%)
note_history_successful_decrypting_time_in_ms	1,219 (-1%)	2,475
note_history_trial_decrypting_time_in_ms	59.2 (-2%)	179 (-2%)
node_database_size_in_bytes	18,624,592	35,053,648
pxe_database_size_in_bytes	29,859	59,414

Circuits stats

Stats on running time and I/O sizes collected for every circuit run across all benchmarks.

Circuit	circuit_simulation_time_in_ms	circuit_input_size_in_bytes	circuit_output_size_in_bytes
private-kernel-init	284 (+1%)	44,366	28,244
private-kernel-ordering	215 (+1%)	52,868	14,326
base-parity	1,836 (+3%)	128	311
base-rollup	716 (-1%)	165,787	925
root-parity	1,533 (-6%)	1,244	311
root-rollup	53.6 (+4%)	4,487	725
private-kernel-inner	648 (+1%)	73,771	28,244
public-kernel-app-logic	450 (+1%)	35,260	28,215
public-kernel-tail	174 (+1%)	40,926	28,215
merge-rollup	8.48 (+2%)	2,696	925

Tree insertion stats

The duration to insert a fixed batch of leaves into each tree type.

Metric	1 leaves	16 leaves	64 leaves	128 leaves	512 leaves	1024 leaves	2048 leaves	4096 leaves	32 leaves
batch_insert_into_append_only_tree_16_depth_ms	10.1 (+1%)	16.3 (+2%)	N/A	N/A	N/A	N/A	N/A	N/A	N/A
batch_insert_into_append_only_tree_16_depth_hash_count	16.8	31.6	N/A	N/A	N/A	N/A	N/A	N/A	N/A
batch_insert_into_append_only_tree_16_depth_hash_ms	0.590 (+1%)	0.504 (+2%)	N/A	N/A	N/A	N/A	N/A	N/A	N/A
batch_insert_into_append_only_tree_32_depth_ms	N/A	N/A	45.8	71.8 (-1%)	229	444	863 (-2%)	1,727	N/A
batch_insert_into_append_only_tree_32_depth_hash_count	N/A	N/A	96.0	159	543	1,055	2,079	4,127	N/A
batch_insert_into_append_only_tree_32_depth_hash_ms	N/A	N/A	0.470	0.443 (-1%)	0.419	0.416	0.411 (-1%)	0.413	N/A
batch_insert_into_indexed_tree_20_depth_ms	N/A	N/A	53.8 (-2%)	106 (-2%)	336 (-1%)	671 (+2%)	1,310 (-1%)	2,607 (-1%)	N/A
batch_insert_into_indexed_tree_20_depth_hash_count	N/A	N/A	104	207	691	1,363	2,707	5,395	N/A
batch_insert_into_indexed_tree_20_depth_hash_ms	N/A	N/A	0.480 (-2%)	0.479 (-1%)	0.456 (-1%)	0.463 (+2%)	0.454 (-1%)	0.452 (-1%)	N/A
batch_insert_into_indexed_tree_40_depth_ms	N/A	N/A	N/A	N/A	N/A	N/A	N/A	N/A	60.9 (-1%)
batch_insert_into_indexed_tree_40_depth_hash_count	N/A	N/A	N/A	N/A	N/A	N/A	N/A	N/A	109
batch_insert_into_indexed_tree_40_depth_hash_ms	N/A	N/A	N/A	N/A	N/A	N/A	N/A	N/A	0.534

Miscellaneous

Transaction sizes based on how many contract classes are registered in the tx.

Metric	0 registered classes
tx_size_in_bytes	22,012

Transaction processing duration by data writes.

Metric	0 new note hashes	1 new note hashes
tx_pxe_processing_time_ms	3,164 (-2%)	1,750 (+1%)

Metric	0 public data writes	1 public data writes
tx_sequencer_processing_time_ms	13.9 (+21%)	1,253 (+1%)

🤖 I have created a release *beep* *boop* --- <details><summary>aztec-package: 0.30.1</summary> ## [0.30.1](aztec-package-v0.30.0...aztec-package-v0.30.1) (2024-03-20) ### Miscellaneous * **aztec-package:** Synchronize aztec-packages versions </details> <details><summary>barretenberg.js: 0.30.1</summary> ## [0.30.1](barretenberg.js-v0.30.0...barretenberg.js-v0.30.1) (2024-03-20) ### Miscellaneous * **barretenberg.js:** Synchronize aztec-packages versions </details> <details><summary>aztec-cli: 0.30.1</summary> ## [0.30.1](aztec-cli-v0.30.0...aztec-cli-v0.30.1) (2024-03-20) ### Miscellaneous * **aztec-cli:** Synchronize aztec-packages versions </details> <details><summary>aztec-packages: 0.30.1</summary> ## [0.30.1](aztec-packages-v0.30.0...aztec-packages-v0.30.1) (2024-03-20) ### Features * Add CMOV instruction to brillig and brillig gen ([#5308](#5308)) ([208abbb](208abbb)) * **avm:** Indirect memory support for arithmetic/bitwise opcodes ([#5328](#5328)) ([d5ffa17](d5ffa17)), closes [#5273](#5273) * **avm:** Indirect memory support for MOV ([#5257](#5257)) ([10ef970](10ef970)), closes [#5205](#5205) * Merge SMT Terms in one class ([#5254](#5254)) ([f5c9b0f](f5c9b0f)) * Sorted execution trace ([#5252](#5252)) ([a216759](a216759)) ### Bug Fixes * Fix recursion tests and reinstate in CI ([#5300](#5300)) ([96c6f21](96c6f21)) * Skip uniswap l1 tests ([#5334](#5334)) ([7a56941](7a56941)) * Update smt_verification README.md ([#5332](#5332)) ([46b15e3](46b15e3)) ### Miscellaneous * Avm team as generated codeowners ([#5325](#5325)) ([06d2786](06d2786)) * No Translator composer ([#5202](#5202)) ([c8897ca](c8897ca)) * Remove toy vm files ([#5326](#5326)) ([d940356](d940356)) * Replace relative paths to noir-protocol-circuits ([ea2ac09](ea2ac09)) </details> <details><summary>barretenberg: 0.30.1</summary> ## [0.30.1](barretenberg-v0.30.0...barretenberg-v0.30.1) (2024-03-20) ### Features * Add CMOV instruction to brillig and brillig gen ([#5308](#5308)) ([208abbb](208abbb)) * **avm:** Indirect memory support for arithmetic/bitwise opcodes ([#5328](#5328)) ([d5ffa17](d5ffa17)), closes [#5273](#5273) * **avm:** Indirect memory support for MOV ([#5257](#5257)) ([10ef970](10ef970)), closes [#5205](#5205) * Merge SMT Terms in one class ([#5254](#5254)) ([f5c9b0f](f5c9b0f)) * Sorted execution trace ([#5252](#5252)) ([a216759](a216759)) ### Bug Fixes * Fix recursion tests and reinstate in CI ([#5300](#5300)) ([96c6f21](96c6f21)) * Update smt_verification README.md ([#5332](#5332)) ([46b15e3](46b15e3)) ### Miscellaneous * No Translator composer ([#5202](#5202)) ([c8897ca](c8897ca)) * Remove toy vm files ([#5326](#5326)) ([d940356](d940356)) </details> --- This PR was generated with [Release Please](https://github.com/googleapis/release-please). See [documentation](https://github.com/googleapis/release-please#release-please).

🤖 I have created a release *beep* *boop* --- <details><summary>aztec-package: 0.30.1</summary> ## [0.30.1](AztecProtocol/aztec-packages@aztec-package-v0.30.0...aztec-package-v0.30.1) (2024-03-20) ### Miscellaneous * **aztec-package:** Synchronize aztec-packages versions </details> <details><summary>barretenberg.js: 0.30.1</summary> ## [0.30.1](AztecProtocol/aztec-packages@barretenberg.js-v0.30.0...barretenberg.js-v0.30.1) (2024-03-20) ### Miscellaneous * **barretenberg.js:** Synchronize aztec-packages versions </details> <details><summary>aztec-cli: 0.30.1</summary> ## [0.30.1](AztecProtocol/aztec-packages@aztec-cli-v0.30.0...aztec-cli-v0.30.1) (2024-03-20) ### Miscellaneous * **aztec-cli:** Synchronize aztec-packages versions </details> <details><summary>aztec-packages: 0.30.1</summary> ## [0.30.1](AztecProtocol/aztec-packages@aztec-packages-v0.30.0...aztec-packages-v0.30.1) (2024-03-20) ### Features * Add CMOV instruction to brillig and brillig gen ([#5308](AztecProtocol/aztec-packages#5308)) ([208abbb](AztecProtocol/aztec-packages@208abbb)) * **avm:** Indirect memory support for arithmetic/bitwise opcodes ([#5328](AztecProtocol/aztec-packages#5328)) ([d5ffa17](AztecProtocol/aztec-packages@d5ffa17)), closes [#5273](AztecProtocol/aztec-packages#5273) * **avm:** Indirect memory support for MOV ([#5257](AztecProtocol/aztec-packages#5257)) ([10ef970](AztecProtocol/aztec-packages@10ef970)), closes [#5205](AztecProtocol/aztec-packages#5205) * Merge SMT Terms in one class ([#5254](AztecProtocol/aztec-packages#5254)) ([f5c9b0f](AztecProtocol/aztec-packages@f5c9b0f)) * Sorted execution trace ([#5252](AztecProtocol/aztec-packages#5252)) ([a216759](AztecProtocol/aztec-packages@a216759)) ### Bug Fixes * Fix recursion tests and reinstate in CI ([#5300](AztecProtocol/aztec-packages#5300)) ([96c6f21](AztecProtocol/aztec-packages@96c6f21)) * Skip uniswap l1 tests ([#5334](AztecProtocol/aztec-packages#5334)) ([7a56941](AztecProtocol/aztec-packages@7a56941)) * Update smt_verification README.md ([#5332](AztecProtocol/aztec-packages#5332)) ([46b15e3](AztecProtocol/aztec-packages@46b15e3)) ### Miscellaneous * Avm team as generated codeowners ([#5325](AztecProtocol/aztec-packages#5325)) ([06d2786](AztecProtocol/aztec-packages@06d2786)) * No Translator composer ([#5202](AztecProtocol/aztec-packages#5202)) ([c8897ca](AztecProtocol/aztec-packages@c8897ca)) * Remove toy vm files ([#5326](AztecProtocol/aztec-packages#5326)) ([d940356](AztecProtocol/aztec-packages@d940356)) * Replace relative paths to noir-protocol-circuits ([ea2ac09](AztecProtocol/aztec-packages@ea2ac09)) </details> <details><summary>barretenberg: 0.30.1</summary> ## [0.30.1](AztecProtocol/aztec-packages@barretenberg-v0.30.0...barretenberg-v0.30.1) (2024-03-20) ### Features * Add CMOV instruction to brillig and brillig gen ([#5308](AztecProtocol/aztec-packages#5308)) ([208abbb](AztecProtocol/aztec-packages@208abbb)) * **avm:** Indirect memory support for arithmetic/bitwise opcodes ([#5328](AztecProtocol/aztec-packages#5328)) ([d5ffa17](AztecProtocol/aztec-packages@d5ffa17)), closes [#5273](AztecProtocol/aztec-packages#5273) * **avm:** Indirect memory support for MOV ([#5257](AztecProtocol/aztec-packages#5257)) ([10ef970](AztecProtocol/aztec-packages@10ef970)), closes [#5205](AztecProtocol/aztec-packages#5205) * Merge SMT Terms in one class ([#5254](AztecProtocol/aztec-packages#5254)) ([f5c9b0f](AztecProtocol/aztec-packages@f5c9b0f)) * Sorted execution trace ([#5252](AztecProtocol/aztec-packages#5252)) ([a216759](AztecProtocol/aztec-packages@a216759)) ### Bug Fixes * Fix recursion tests and reinstate in CI ([#5300](AztecProtocol/aztec-packages#5300)) ([96c6f21](AztecProtocol/aztec-packages@96c6f21)) * Update smt_verification README.md ([#5332](AztecProtocol/aztec-packages#5332)) ([46b15e3](AztecProtocol/aztec-packages@46b15e3)) ### Miscellaneous * No Translator composer ([#5202](AztecProtocol/aztec-packages#5202)) ([c8897ca](AztecProtocol/aztec-packages@c8897ca)) * Remove toy vm files ([#5326](AztecProtocol/aztec-packages#5326)) ([d940356](AztecProtocol/aztec-packages@d940356)) </details> --- This PR was generated with [Release Please](https://github.com/googleapis/release-please). See [documentation](https://github.com/googleapis/release-please#release-please).

Sarkoxed added 23 commits March 15, 2024 16:56

New merged class.

fa0b44c

BitVector sort

a8b3483

Major changes in Symbolic Terms usage

d3694f7

STerm: - fixed lots of errors in methods Tests: - fixed old ones to use STerm class - added new tests to check for unsupported functionality

Tests for BitVectors and fix in STerm

4ca7e58

Merge branch 'master' into as/smt-merge-terms-2

e0e44f7

Bool Terms update

6de3a72

Commit to have a more readable diff

8d9c579

Get rid of templates

7bcf447

Get rid of templates

e1bf853

Meet BitVector tests

3c978de

Set default type to be FFTerm

b9a90ca

Update to the new STerm api

32d7f98

Update polynomials tests

af43cc1

- Switch to field_t native operations - Switch to the new STerm api - Use smt_timer

See you later

6198adf

Fix circuit internals

8889638

- removed zero initialization for optimized variables, since it doesn't do anything helpful - fixed logic_flag output - fixed range constraint so it now fits in bitvector size

Added empty constructor

c648f25

Operation instead of Kind

c38790d

Bitvector operations parser

74238d2

I forgot it for some reason

924ba0c

Minutes/Seconds in timer

c6bf293

Zero initization

50bcf8d

Doc strings

57a64b1

Got rid of ffterm and ffiter

ee663ca

Sarkoxed marked this pull request as ready for review March 19, 2024 14:24

Sarkoxed requested a review from Rumata888 March 19, 2024 14:24

Sarkoxed added crypto cryptography product-security PRs extending our security mechanisms labels Mar 19, 2024

Rumata888 reviewed Mar 19, 2024

View reviewed changes

Rumata888 requested changes Mar 19, 2024

View reviewed changes

Rumata888 assigned Sarkoxed Mar 19, 2024

Rumata888 and others added 3 commits March 19, 2024 17:58

Merge branch 'master' into as/smt-merge-terms-2

1780937

Addressing comments

85bbda2

Merge branch 'master' into as/smt-merge-terms-2

7e4fde3

Rumata888 approved these changes Mar 20, 2024

View reviewed changes

Sarkoxed merged commit f5c9b0f into master Mar 20, 2024
97 checks passed

Sarkoxed deleted the as/smt-merge-terms-2 branch March 20, 2024 11:08

AztecBot mentioned this pull request Mar 20, 2024

chore(master): Release 0.30.1 #5322

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Merge SMT Terms in one class #5254

feat: Merge SMT Terms in one class #5254

Sarkoxed commented Mar 15, 2024 •

edited

Loading

Rumata888 Mar 19, 2024

Rumata888 Mar 19, 2024

Rumata888 Mar 19, 2024

Sarkoxed Mar 19, 2024

Rumata888 Mar 19, 2024

Rumata888 Mar 19, 2024 •

edited

Loading

Rumata888 Mar 19, 2024

Sarkoxed Mar 19, 2024

Rumata888 left a comment

AztecBot commented Mar 19, 2024

L2 block published to L1

L2 chain processing

Circuits stats

Tree insertion stats

Miscellaneous


		// MUL, LSH, RSH, AND and OR are not tested, since they are not bijective

		TEST(BVTerm, unsupported_operations)

feat: Merge SMT Terms in one class #5254

feat: Merge SMT Terms in one class #5254

Conversation

Sarkoxed commented Mar 15, 2024 • edited Loading

STerm

Solver

Circuit

Utils

Rumata888 Mar 19, 2024

Choose a reason for hiding this comment

Rumata888 Mar 19, 2024

Choose a reason for hiding this comment

Rumata888 Mar 19, 2024

Choose a reason for hiding this comment

Sarkoxed Mar 19, 2024

Choose a reason for hiding this comment

Rumata888 Mar 19, 2024

Choose a reason for hiding this comment

Rumata888 Mar 19, 2024 • edited Loading

Choose a reason for hiding this comment

Rumata888 Mar 19, 2024

Choose a reason for hiding this comment

Sarkoxed Mar 19, 2024

Choose a reason for hiding this comment

Rumata888 left a comment

Choose a reason for hiding this comment

AztecBot commented Mar 19, 2024

Benchmark results

L2 block published to L1

L2 chain processing

Circuits stats

Tree insertion stats

Miscellaneous

Sarkoxed commented Mar 15, 2024 •

edited

Loading

Rumata888 Mar 19, 2024 •

edited

Loading