Skip to content

Commit cc540cc

Browse files
author
AztecBot
committed
Merge branch 'next' into merge-train/barretenberg
2 parents 1c0d764 + 87fc924 commit cc540cc

File tree

149 files changed

+6533
-6269
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

149 files changed

+6533
-6269
lines changed

‎barretenberg/cpp/src/barretenberg/acir_formal_proofs/README.md‎

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#Formal Verification of ACIR Instructions
1+
# Formal Verification of ACIR Instructions
22

33
This module provides formal verification capabilities for ACIR (Arithmetic Circuit Intermediate Representation) instructions generated from Noir SSA code.
44

@@ -20,31 +20,31 @@ The verifier uses SMT (Satisfiability Modulo Theories) solving to formally verif
2020

2121
| Opcode | Lhs type/size | Rhs type/size | Time/seconds | Memory/GB | Success | SMT Term Type | Reason |
2222
| ----------- | ------------- | ------------- | ------------ | --------- | ------- | ---------------- | ------------------------------------------------------------------------------------------------------------- |
23-
| Binary::Add | Field | Field | 0.024 | - | ✓
24-
| TermType::FFTerm | | | Binary::Add | Unsigned_127 | Unsigned_127 | 2.8 | - | ✓
25-
| TermType::BVTerm | | | Binary::And | Unsigned_32 | Unsigned_32 | 6.7 | - | ✓
26-
| TermType::BVTerm | | | Binary::And | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | [smt solver lookup doesnt support 2bits tables](https://github.com/AztecProtocol/aztec-packages/issues/11721) |
27-
| Binary::Div | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | |
28-
| Binary::Div | Unsigned_126 | Unsigned_126 | 402.7 | 3.5 | ✗ | TermType::BVTerm | [Field and bitvector logic mixing](https://github.com/AztecProtocol/aztec-packages/issues/11722) |
29-
| Binary::Div | Signed_126 | Signed_126 | >17 days | 5.1 | ✗ | TermType::BVTerm | [Field and bitvector logic mixing](https://github.com/AztecProtocol/aztec-packages/issues/11722) |
30-
| Binary::Eq | Field | Field | 19.2 | - | ✓ | TermType::FFTerm | |
31-
| Binary::Eq | Unsigned_127 | Unsigned_127 | 22.8 | - | ✓ | TermType::BVTerm | |
32-
| Binary::Lt | Unsigned_127 | Unsigned_127 | 56.7 | - | ✓ | TermType::BVTerm | |
33-
| Binary::Mod | Unsigned_127 | Unsigned_127 | - | 3.2 | ✗ | TermType::BVTerm | [Field and bitvector logic mixing](https://github.com/AztecProtocol/aztec-packages/issues/11722) |
34-
| Binary::Mul | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | |
35-
| Binary::Mul | Unsigned_127 | Unsigned_127 | 10.0 | - | ✓ | TermType::BVTerm | |
36-
| Binary::Or | Unsigned_32 | Unsigned_32 | 18.0 | - | ✓ | TermType::BVTerm | |
23+
| Binary::Add | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | - |
24+
| Binary::Add | Unsigned_127 | Unsigned_127 | 2.8 | - | ✓ | TermType::BVTerm | - |
25+
| Binary::And | Unsigned_32 | Unsigned_32 | 6.7 | - | ✓ | TermType::BVTerm | - |
26+
| Binary::And | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | [smt solver lookup doesnt support 2bits tables](https://github.com/AztecProtocol/aztec-packages/issues/11721) |
27+
| Binary::Div | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | - |
28+
| Binary::Div | Unsigned_126 | Unsigned_126 | >130 days | 20 | ✗ | TermType::BVTerm | Test takes too long |
29+
| Binary::Div | Signed_126 | Signed_126 | >130 days | 20 | ✗ | TermType::BVTerm | Test takes too long |
30+
| Binary::Eq | Field | Field | 19.2 | - | ✓ | TermType::FFTerm | - |
31+
| Binary::Eq | Unsigned_127 | Unsigned_127 | 22.8 | - | ✓ | TermType::BVTerm | - |
32+
| Binary::Lt | Unsigned_127 | Unsigned_127 | 56.7 | - | ✓ | TermType::BVTerm | - |
33+
| Binary::Mod | Unsigned_127 | Unsigned_127 | >130 days | 3.2 | ✗ | TermType::BVTerm | Test takes too long |
34+
| Binary::Mul | Field | Field | 0.024 | - | ✓ | TermType::FFTerm | - |
35+
| Binary::Mul | Unsigned_127 | Unsigned_127 | 10.0 | - | ✓ | TermType::BVTerm | - |
36+
| Binary::Or | Unsigned_32 | Unsigned_32 | 18.0 | - | ✓ | TermType::BVTerm | - |
3737
| Binary::Or | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | [smt solver lookup doesnt support 2bits tables](https://github.com/AztecProtocol/aztec-packages/issues/11721) |
38-
| Binary::Shl | Unsigned_64 | Unsigned_8 | 42331.61 | 63.2 | ✓ | TermType::BVTerm | |
39-
| Binary::Shl | Unsigned_32 | Unsigned_8 | 4574.0 | 30 | ✓ | TermType::BVTerm | |
40-
| Binary::Shr | Unsigned_64 | Unsigned_8 | 3927.88 | 10 | ✓ | TermType::BVTerm | |
41-
| Binary::Sub | Unsigned_127 | Unsigned_127 | 3.3 | - | ✓ | TermType::BVTerm | |
42-
| Binary::Xor | Unsigned_32 | Unsigned_32 | 14.7 | - | ✓ | TermType::BVTerm | |
38+
| Binary::Shl | Unsigned_64 | Unsigned_8 | 42331.61 | 63.2 | ✓ | TermType::BVTerm | - |
39+
| Binary::Shl | Unsigned_32 | Unsigned_8 | 4574.0 | 30 | ✓ | TermType::BVTerm | - |
40+
| Binary::Shr | Unsigned_64 | Unsigned_8 | 3927.88 | 10 | ✓ | TermType::BVTerm | - |
41+
| Binary::Sub | Unsigned_127 | Unsigned_127 | 3.3 | - | ✓ | TermType::BVTerm | - |
42+
| Binary::Xor | Unsigned_32 | Unsigned_32 | 14.7 | - | ✓ | TermType::BVTerm | - |
4343
| Binary::Xor | Unsigned_127 | Unsigned_127 | 7.5 | - | ✗ | TermType::BVTerm | [smt solver lookup doesnt support 2bits tables](https://github.com/AztecProtocol/aztec-packages/issues/11721) |
44-
| Not | Unsigned_127 | - | 0.2 | - | ✓ | TermType::BVTerm | |
45-
| Cast | Field | Unsigned_64 | 0.05 | - | ✓ | TermType::FFTerm | |
46-
| Cast | Unsigned_64 | Unsigned_8 | 0.07 | - | ✓ | TermType::BVTerm | |
47-
| Cast | Unsigned_8 | Unsigned_64 | 0.6 | - | ✓ | TermType::BVTerm | |
44+
| Not | Unsigned_127 | - | 0.2 | - | ✓ | TermType::BVTerm | - |
45+
| Cast | Field | Unsigned_64 | 0.05 | - | ✓ | TermType::FFTerm | - |
46+
| Cast | Unsigned_64 | Unsigned_8 | 0.07 | - | ✓ | TermType::BVTerm | - |
47+
| Cast | Unsigned_8 | Unsigned_64 | 0.6 | - | ✓ | TermType::BVTerm | - |
4848

4949
Each test attempts to find counterexamples that violate the expected behavior. A passing test indicates the operation is correctly implemented, while a failing test reveals potential issues.
5050

‎barretenberg/cpp/src/barretenberg/vm2/common/aztec_constants.hpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@
169169
#define AVM_V2_PUBLIC_INPUTS_FLATTENED_SIZE 1
170170
#define AVM_V2_PROOF_LENGTH_IN_FIELDS_PADDED 20000
171171
#define AVM_V2_VERIFICATION_KEY_LENGTH_IN_FIELDS_PADDED 1000
172-
#define MAX_L2_GAS_PER_TX_PUBLIC_PORTION 6000000
172+
#define AVM_MAX_PROCESSABLE_L2_GAS 6000000
173173
#define AVM_GAS_PER_ROW 3
174174
#define AVM_MERKLE_CHECK_ROWS_PUBLIC_WRITE 80
175175
#define AVM_MERKLE_CHECK_ROWS_PUBLIC_READ 40

‎barretenberg/cpp/src/barretenberg/vm2/simulation/execution.cpp‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1144,8 +1144,6 @@ ExecutionResult Execution::execute(std::unique_ptr<ContextInterface> enqueued_ca
11441144

11451145
// State after the opcode.
11461146
ex_event.after_context_event = context.serialize_context_event();
1147-
// TODO(dbanks12): fix phase. Should come from TX execution and be forwarded to nested calls.
1148-
ex_event.after_context_event.phase = TransactionPhase::APP_LOGIC;
11491147
events.emit(std::move(ex_event));
11501148

11511149
// If the context has halted, we need to exit the external call.

‎barretenberg/cpp/src/barretenberg/vm2/simulation/tx_execution.cpp‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -174,8 +174,7 @@ void TxExecution::simulate(const Tx& tx)
174174
tx_context.side_effect_states = result.side_effect_states;
175175
// Check what to do here for GAS
176176
emit_public_call_request(*tx.teardownEnqueuedCall,
177-
// TODO(dbanks12): This should be TEARDOWN.
178-
TransactionPhase::APP_LOGIC,
177+
TransactionPhase::TEARDOWN,
179178
fee,
180179
result.success,
181180
start_gas,

‎barretenberg/cpp/src/barretenberg/vm2/testing/avm_inputs.testdata.bin‎

0 Bytes
Binary file not shown.

‎barretenberg/cpp/src/barretenberg/vm2/testing/minimal_tx.testdata.bin‎

0 Bytes
Binary file not shown.

‎barretenberg/cpp/src/barretenberg/vm2/tracegen/execution_trace.cpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -350,9 +350,10 @@ void ExecutionTraceBuilder::process(
350350
{ C::execution_context_id, ex_event.after_context_event.id },
351351
{ C::execution_parent_id, ex_event.after_context_event.parent_id },
352352
{ C::execution_pc, ex_event.before_context_event.pc },
353-
{ C::execution_is_static, ex_event.after_context_event.is_static },
354353
{ C::execution_msg_sender, ex_event.after_context_event.msg_sender },
355354
{ C::execution_contract_address, ex_event.after_context_event.contract_addr },
355+
{ C::execution_transaction_fee, ex_event.after_context_event.transaction_fee },
356+
{ C::execution_is_static, ex_event.after_context_event.is_static },
356357
{ C::execution_parent_calldata_addr, ex_event.after_context_event.parent_cd_addr },
357358
{ C::execution_parent_calldata_size, ex_event.after_context_event.parent_cd_size_addr },
358359
{ C::execution_last_child_returndata_addr, ex_event.after_context_event.last_child_rd_addr },

‎barretenberg/docs/docs/getting_started.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ Although it is a standandalone prover, Barretenberg is designed to be used with
1818
Inspired by `rustup`, `noirup` and similar tools, you can use the `bbup` installation script to quickly install and update Barretenberg's CLI tool:
1919

2020
```bash
21-
curl -L https://raw.githubusercontent.com/AztecProtocol/aztec-packages/refs/heads/master/barretenberg/bbup/install | bash
21+
curl -L https://raw.githubusercontent.com/AztecProtocol/aztec-packages/refs/heads/next/barretenberg/bbup/install | bash
2222
bbup
2323
```
2424

‎barretenberg/docs/versioned_docs/version-v0.87.0/getting_started.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ Although it is a standandalone prover, Barretenberg is designed to be used with
1818
Inspired by `rustup`, `noirup` and similar tools, you can use the `bbup` installation script to quickly install and update Barretenberg's CLI tool:
1919

2020
```bash
21-
curl -L https://raw.githubusercontent.com/AztecProtocol/aztec-packages/refs/heads/master/barretenberg/bbup/install | bash
21+
curl -L https://raw.githubusercontent.com/AztecProtocol/aztec-packages/refs/heads/next/barretenberg/bbup/install | bash
2222
bbup
2323
```
2424

‎docs/docs-words.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -345,3 +345,5 @@ woooh
345345
zcash
346346
Zcash
347347
Zybil
348+
nothin
349+
whoooaa

0 commit comments

Comments
 (0)