Skip to content

Commit

Permalink
feat(avm): e2e proving of storage (#6967)
Browse files Browse the repository at this point in the history
Co-authored-by: IlyasRidhuan <[email protected]>
  • Loading branch information
dbanks12 and IlyasRidhuan authored Jun 7, 2024
1 parent f330bff commit 6a7be0c
Show file tree
Hide file tree
Showing 12 changed files with 489 additions and 143 deletions.
8 changes: 4 additions & 4 deletions avm-transpiler/src/transpile.rs
Original file line number Diff line number Diff line change
Expand Up @@ -894,7 +894,7 @@ fn handle_storage_write(
};

let src_offset_maybe = inputs[1];
let (src_offset, src_size) = match src_offset_maybe {
let (src_offset, size) = match src_offset_maybe {
ValueOrArray::HeapArray(HeapArray { pointer, size }) => (pointer.0, size),
_ => panic!("Storage write address inputs should be an array of values"),
};
Expand All @@ -904,7 +904,7 @@ fn handle_storage_write(
indirect: Some(ZEROTH_OPERAND_INDIRECT),
operands: vec![
AvmOperand::U32 { value: src_offset as u32 },
AvmOperand::U32 { value: src_size as u32 },
AvmOperand::U32 { value: size as u32 },
AvmOperand::U32 { value: slot_offset as u32 },
],
..Default::default()
Expand Down Expand Up @@ -961,7 +961,7 @@ fn handle_storage_read(
};

let dest_offset_maybe = destinations[0];
let (dest_offset, src_size) = match dest_offset_maybe {
let (dest_offset, size) = match dest_offset_maybe {
ValueOrArray::HeapArray(HeapArray { pointer, size }) => (pointer.0, size),
_ => panic!("Storage write address inputs should be an array of values"),
};
Expand All @@ -971,7 +971,7 @@ fn handle_storage_read(
indirect: Some(FIRST_OPERAND_INDIRECT),
operands: vec![
AvmOperand::U32 { value: slot_offset as u32 },
AvmOperand::U32 { value: src_size as u32 },
AvmOperand::U32 { value: size as u32 },
AvmOperand::U32 { value: dest_offset as u32 },
],
..Default::default()
Expand Down
7 changes: 5 additions & 2 deletions barretenberg/cpp/pil/avm/avm_main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -391,7 +391,7 @@ namespace avm_main(256);

pol KERNEL_OUTPUT_SELECTORS = (
sel_op_note_hash_exists + sel_op_emit_note_hash + sel_op_nullifier_exists + sel_op_emit_nullifier + sel_op_l1_to_l2_msg_exists +
sel_op_emit_unencrypted_log + sel_op_emit_l2_to_l1_msg + sel_op_sload + sel_op_sstore
sel_op_emit_unencrypted_log + sel_op_emit_l2_to_l1_msg
);
#[KERNEL_OUTPUT_ACTIVE_CHECK]
KERNEL_OUTPUT_SELECTORS * (1 - q_kernel_output_lookup) = 0;
Expand Down Expand Up @@ -454,7 +454,10 @@ namespace avm_main(256);
// Note: External call gas cost is not constrained
pol commit gas_cost_active;
pol commit mem_op_activate_gas; // TODO: remove this one
gas_cost_active - OPCODE_SELECTORS - ALL_CTRL_FLOW_SEL - mem_op_activate_gas = 0;
// TODO: remove sload and sstore from here
// This temporarily disables gas tracking for sload and sstore because our gas
// tracking doesn't work properly for instructions that span multiple rows
gas_cost_active - OPCODE_SELECTORS - ALL_CTRL_FLOW_SEL - sel_op_sload - sel_op_sstore - mem_op_activate_gas = 0;

// Program counter must increment if not jumping or returning
#[PC_INCREMENT]
Expand Down
120 changes: 56 additions & 64 deletions barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -937,14 +937,12 @@ template <typename FF_> class avm_mainImpl {
{
Avm_DECLARE_VIEWS(78);

auto tmp = (((((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
avm_main_sel_op_nullifier_exists) +
avm_main_sel_op_emit_nullifier) +
avm_main_sel_op_l1_to_l2_msg_exists) +
avm_main_sel_op_emit_unencrypted_log) +
avm_main_sel_op_emit_l2_to_l1_msg) +
avm_main_sel_op_sload) +
avm_main_sel_op_sstore) *
auto tmp = (((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
avm_main_sel_op_nullifier_exists) +
avm_main_sel_op_emit_nullifier) +
avm_main_sel_op_l1_to_l2_msg_exists) +
avm_main_sel_op_emit_unencrypted_log) +
avm_main_sel_op_emit_l2_to_l1_msg) *
(-avm_main_q_kernel_output_lookup + FF(1)));
tmp *= scaling_factor;
std::get<78>(evals) += tmp;
Expand Down Expand Up @@ -1061,42 +1059,42 @@ template <typename FF_> class avm_mainImpl {
Avm_DECLARE_VIEWS(92);

auto tmp =
(((avm_main_gas_cost_active -
(((((((avm_main_sel_op_fdiv +
((((((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_mul) +
avm_main_sel_op_div) +
avm_main_sel_op_not) +
avm_main_sel_op_eq) +
avm_main_sel_op_lt) +
avm_main_sel_op_lte) +
avm_main_sel_op_shr) +
avm_main_sel_op_shl) +
avm_main_sel_op_cast)) +
((avm_main_sel_op_and + avm_main_sel_op_or) + avm_main_sel_op_xor)) +
(avm_main_sel_cmov + avm_main_sel_mov)) +
((((avm_main_sel_op_radix_le + avm_main_sel_op_sha256) + avm_main_sel_op_poseidon2) +
avm_main_sel_op_keccak) +
avm_main_sel_op_pedersen)) +
((((((((((avm_main_sel_op_sender + avm_main_sel_op_address) + avm_main_sel_op_storage_address) +
avm_main_sel_op_chain_id) +
avm_main_sel_op_version) +
avm_main_sel_op_block_number) +
avm_main_sel_op_coinbase) +
avm_main_sel_op_timestamp) +
avm_main_sel_op_fee_per_l2_gas) +
avm_main_sel_op_fee_per_da_gas) +
avm_main_sel_op_transaction_fee)) +
((((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
(((((avm_main_gas_cost_active -
(((((((avm_main_sel_op_fdiv +
((((((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_mul) +
avm_main_sel_op_div) +
avm_main_sel_op_not) +
avm_main_sel_op_eq) +
avm_main_sel_op_lt) +
avm_main_sel_op_lte) +
avm_main_sel_op_shr) +
avm_main_sel_op_shl) +
avm_main_sel_op_cast)) +
((avm_main_sel_op_and + avm_main_sel_op_or) + avm_main_sel_op_xor)) +
(avm_main_sel_cmov + avm_main_sel_mov)) +
((((avm_main_sel_op_radix_le + avm_main_sel_op_sha256) + avm_main_sel_op_poseidon2) +
avm_main_sel_op_keccak) +
avm_main_sel_op_pedersen)) +
((((((((((avm_main_sel_op_sender + avm_main_sel_op_address) + avm_main_sel_op_storage_address) +
avm_main_sel_op_chain_id) +
avm_main_sel_op_version) +
avm_main_sel_op_block_number) +
avm_main_sel_op_coinbase) +
avm_main_sel_op_timestamp) +
avm_main_sel_op_fee_per_l2_gas) +
avm_main_sel_op_fee_per_da_gas) +
avm_main_sel_op_transaction_fee)) +
((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
avm_main_sel_op_nullifier_exists) +
avm_main_sel_op_emit_nullifier) +
avm_main_sel_op_l1_to_l2_msg_exists) +
avm_main_sel_op_emit_unencrypted_log) +
avm_main_sel_op_emit_l2_to_l1_msg) +
avm_main_sel_op_sload) +
avm_main_sel_op_sstore)) +
(avm_main_sel_op_dagasleft + avm_main_sel_op_l2gasleft))) -
(((avm_main_sel_jump + avm_main_sel_jumpi) + avm_main_sel_internal_call) +
avm_main_sel_internal_return)) -
avm_main_sel_op_emit_l2_to_l1_msg)) +
(avm_main_sel_op_dagasleft + avm_main_sel_op_l2gasleft))) -
(((avm_main_sel_jump + avm_main_sel_jumpi) + avm_main_sel_internal_call) +
avm_main_sel_internal_return)) -
avm_main_sel_op_sload) -
avm_main_sel_op_sstore) -
avm_main_mem_op_activate_gas);
tmp *= scaling_factor;
std::get<92>(evals) += tmp;
Expand Down Expand Up @@ -1131,14 +1129,12 @@ template <typename FF_> class avm_mainImpl {
avm_main_sel_op_fee_per_l2_gas) +
avm_main_sel_op_fee_per_da_gas) +
avm_main_sel_op_transaction_fee)) +
((((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
avm_main_sel_op_nullifier_exists) +
avm_main_sel_op_emit_nullifier) +
avm_main_sel_op_l1_to_l2_msg_exists) +
avm_main_sel_op_emit_unencrypted_log) +
avm_main_sel_op_emit_l2_to_l1_msg) +
avm_main_sel_op_sload) +
avm_main_sel_op_sstore)) +
((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
avm_main_sel_op_nullifier_exists) +
avm_main_sel_op_emit_nullifier) +
avm_main_sel_op_l1_to_l2_msg_exists) +
avm_main_sel_op_emit_unencrypted_log) +
avm_main_sel_op_emit_l2_to_l1_msg)) +
(avm_main_sel_op_dagasleft + avm_main_sel_op_l2gasleft))) *
(avm_main_pc_shift - (avm_main_pc + FF(1))));
tmp *= scaling_factor;
Expand Down Expand Up @@ -1192,14 +1188,12 @@ template <typename FF_> class avm_mainImpl {
avm_main_sel_op_fee_per_l2_gas) +
avm_main_sel_op_fee_per_da_gas) +
avm_main_sel_op_transaction_fee)) +
((((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
avm_main_sel_op_nullifier_exists) +
avm_main_sel_op_emit_nullifier) +
avm_main_sel_op_l1_to_l2_msg_exists) +
avm_main_sel_op_emit_unencrypted_log) +
avm_main_sel_op_emit_l2_to_l1_msg) +
avm_main_sel_op_sload) +
avm_main_sel_op_sstore)) +
((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
avm_main_sel_op_nullifier_exists) +
avm_main_sel_op_emit_nullifier) +
avm_main_sel_op_l1_to_l2_msg_exists) +
avm_main_sel_op_emit_unencrypted_log) +
avm_main_sel_op_emit_l2_to_l1_msg)) +
(avm_main_sel_op_dagasleft + avm_main_sel_op_l2gasleft)) *
(avm_main_call_ptr - avm_main_space_id));
tmp *= scaling_factor;
Expand Down Expand Up @@ -1576,14 +1570,12 @@ template <typename FF_> class avm_mainImpl {
{
Avm_DECLARE_VIEWS(139);

auto tmp = (((((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
avm_main_sel_op_nullifier_exists) +
avm_main_sel_op_emit_nullifier) +
avm_main_sel_op_l1_to_l2_msg_exists) +
avm_main_sel_op_emit_unencrypted_log) +
avm_main_sel_op_emit_l2_to_l1_msg) +
avm_main_sel_op_sload) +
avm_main_sel_op_sstore) *
auto tmp = (((((((avm_main_sel_op_note_hash_exists + avm_main_sel_op_emit_note_hash) +
avm_main_sel_op_nullifier_exists) +
avm_main_sel_op_emit_nullifier) +
avm_main_sel_op_l1_to_l2_msg_exists) +
avm_main_sel_op_emit_unencrypted_log) +
avm_main_sel_op_emit_l2_to_l1_msg) *
(avm_kernel_side_effect_counter_shift - (avm_kernel_side_effect_counter + FF(1))));
tmp *= scaling_factor;
std::get<139>(evals) += tmp;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -71,8 +71,8 @@ const std::unordered_map<OpCode, std::vector<OperandType>> OPCODE_WIRE_FORMAT =
{ OpCode::EMITNULLIFIER, getter_format }, // TODO: new format for these
{ OpCode::EMITUNENCRYPTEDLOG, getter_format },
{ OpCode::SENDL2TOL1MSG, { OperandType::INDIRECT, OperandType::UINT32, OperandType::UINT32 } },
{ OpCode::SLOAD, { OperandType::INDIRECT, OperandType::UINT32, OperandType::UINT32 } },
{ OpCode::SSTORE, { OperandType::INDIRECT, OperandType::UINT32, OperandType::UINT32 } },
{ OpCode::SLOAD, { OperandType::INDIRECT, OperandType::UINT32, OperandType::UINT32, OperandType::UINT32 } },
{ OpCode::SSTORE, { OperandType::INDIRECT, OperandType::UINT32, OperandType::UINT32, OperandType::UINT32 } },
/*TODO: leafIndexOffset is not constrained*/
{ OpCode::NOTEHASHEXISTS,
{ OperandType::INDIRECT,
Expand Down Expand Up @@ -259,7 +259,7 @@ std::vector<Instruction> Deserialization::parse(std::vector<uint8_t> const& byte
uint8_t tag_u8 = bytecode.at(pos);
if (tag_u8 == static_cast<uint8_t>(AvmMemoryTag::U0) || tag_u8 > MAX_MEM_TAG) {
throw_or_abort("Instruction tag is invalid at position " + std::to_string(pos) +
" value: " + std::to_string(tag_u8) + " for opcode: " + to_hex(opcode));
" value: " + std::to_string(tag_u8) + " for opcode: " + to_string(opcode));
}
operands.emplace_back(static_cast<AvmMemoryTag>(tag_u8));
break;
Expand Down
11 changes: 8 additions & 3 deletions barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,6 @@ std::tuple<AvmFlavor::VerificationKey, HonkProof> Execution::prove(std::vector<u
auto circuit_builder = bb::AvmCircuitBuilder();
circuit_builder.set_trace(std::move(trace));

info("Checking circuit");
circuit_builder.check_circuit();

auto composer = AvmComposer();
Expand Down Expand Up @@ -493,10 +492,16 @@ std::vector<Row> Execution::gen_trace(std::vector<Instruction> const& instructio
std::get<uint32_t>(inst.operands.at(1)));
break;
case OpCode::SLOAD:
trace_builder.op_sload(std::get<uint32_t>(inst.operands.at(1)), std::get<uint32_t>(inst.operands.at(2)));
trace_builder.op_sload(std::get<uint8_t>(inst.operands.at(0)),
std::get<uint32_t>(inst.operands.at(1)),
std::get<uint32_t>(inst.operands.at(2)),
std::get<uint32_t>(inst.operands.at(3)));
break;
case OpCode::SSTORE:
trace_builder.op_sstore(std::get<uint32_t>(inst.operands.at(1)), std::get<uint32_t>(inst.operands.at(2)));
trace_builder.op_sstore(std::get<uint8_t>(inst.operands.at(0)),
std::get<uint32_t>(inst.operands.at(1)),
std::get<uint32_t>(inst.operands.at(2)),
std::get<uint32_t>(inst.operands.at(3)));
break;
case OpCode::L1TOL2MSGEXISTS:
trace_builder.op_l1_to_l2_msg_exists(std::get<uint8_t>(inst.operands.at(0)),
Expand Down
Loading

0 comments on commit 6a7be0c

Please sign in to comment.