Skip to content

Commit

Permalink
fix: test globals, run write oracles inline
Browse files Browse the repository at this point in the history
  • Loading branch information
Maddiaa0 committed Feb 5, 2024
1 parent a546ff4 commit a973df0
Show file tree
Hide file tree
Showing 7 changed files with 253 additions and 151 deletions.
6 changes: 4 additions & 2 deletions avm-transpiler/src/transpile.rs
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,9 @@ pub fn brillig_to_avm(brillig: &Brillig) -> Vec<u8> {
bytecode
}

/// Handle foreign function calls
/// - Environment getting opcodes will be represented as foreign calls
/// - TODO: support for avm external calls through this function
fn handle_foreign_call(
avm_instrs: &mut Vec<AvmInstruction>,
function: &String,
Expand Down Expand Up @@ -301,8 +304,7 @@ fn handle_foreign_call(
"version" => AvmOpcode::VERSION,
"blockNumber" => AvmOpcode::BLOCKNUMBER,
"timestamp" => AvmOpcode::TIMESTAMP,
// "isStaticCall" => AvmOpcode::ISSTATICCALL,
// "isDelegateCall" => AvmOpcode::ISDELEGATECALL,
// "callStackDepth" => AvmOpcode::CallStackDepth,
_ => panic!(
"Transpiler doesn't know how to process ForeignCall function {:?}",
function
Expand Down
191 changes: 191 additions & 0 deletions barretenberg/cpp/pil/avm/avm.pil
Original file line number Diff line number Diff line change
@@ -0,0 +1,191 @@

include "mem_trace.pil";
include "alu_chip.pil";

namespace avmMini(256);

//===== CONSTANT POLYNOMIALS ==================================================
pol constant clk(i) { i };
pol constant first = [1] + [0]*; // Used mostly to toggle off the first row consisting
// only in first element of shifted polynomials.

//===== CONTROL FLOW ==========================================================
// Program counter
pol commit pc;
// Return Pointer
pol commit internal_return_ptr;

pol commit sel_internal_call;
pol commit sel_internal_return;
pol commit sel_jump;

// Halt program execution
pol commit sel_halt;

//===== TABLE SUBOP-TR ========================================================
// Boolean selectors for (sub-)operations. Only one operation is activated at
// a time.

// ADD
pol commit sel_op_add;
// SUB
pol commit sel_op_sub;
// MUL
pol commit sel_op_mul;
// DIV
pol commit sel_op_div;

// Instruction memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field)
pol commit in_tag;

// Errors
pol commit op_err; // Boolean flag pertaining to an operation error
pol commit tag_err; // Boolean flag (foreign key to memTrace.m_tag_err)

// A helper witness being the inverse of some value
// to show a non-zero equality
pol commit inv;

// Intermediate register values
pol commit ia;
pol commit ib;
pol commit ic;

// Memory operation per intermediate register
pol commit mem_op_a;
pol commit mem_op_b;
pol commit mem_op_c;

// Read-write flag per intermediate register: Read = 0, Write = 1
pol commit rwa;
pol commit rwb;
pol commit rwc;

// Memory index involved into a memory operation per pertaining intermediate register
// We should range constrain it to 32 bits ultimately. For first mini-AVM,
// we will assume that these columns are of the right type.
pol commit mem_idx_a;
pol commit mem_idx_b;
pol commit mem_idx_c;


// Track the last line of the execution trace. It does NOT correspond to the last row of the whole table
// of size N. As this depends on the supplied bytecode, this polynomial cannot be constant.
pol commit last;

// Relations on type constraints

sel_op_add * (1 - sel_op_add) = 0;
sel_op_sub * (1 - sel_op_sub) = 0;
sel_op_mul * (1 - sel_op_mul) = 0;
sel_op_div * (1 - sel_op_div) = 0;

sel_internal_call * (1 - sel_internal_call) = 0;
sel_internal_return * (1 - sel_internal_return) = 0;
sel_jump * (1 - sel_jump) = 0;
sel_halt * (1 - sel_halt) = 0;

op_err * (1 - op_err) = 0;
tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to memTrace)?

mem_op_a * (1 - mem_op_a) = 0;
mem_op_b * (1 - mem_op_b) = 0;
mem_op_c * (1 - mem_op_c) = 0;

rwa * (1 - rwa) = 0;
rwb * (1 - rwb) = 0;
rwc * (1 - rwc) = 0;

// TODO: Constrain rwa, rwb, rwc to u32 type and 0 <= in_tag <= 6

// Set intermediate registers to 0 whenever tag_err occurs
tag_err * ia = 0;
tag_err * ib = 0;
tag_err * ic = 0;

// Relation for division over the finite field
// If tag_err == 1 in a division, then ib == 0 and op_err == 1.
#[SUBOP_DIVISION_FF]
sel_op_div * (1 - op_err) * (ic * ib - ia) = 0;

// When sel_op_div == 1, we want ib == 0 <==> op_err == 1
// This can be achieved with the 2 following relations.
// inv is an extra witness to show that we can invert ib, i.e., inv = ib^(-1)
// If ib == 0, we have to set inv = 1 to satisfy the second relation,
// because op_err == 1 from the first relation.
#[SUBOP_DIVISION_ZERO_ERR1]
sel_op_div * (ib * inv - 1 + op_err) = 0;
#[SUBOP_DIVISION_ZERO_ERR2]
sel_op_div * op_err * (1 - inv) = 0;

// op_err cannot be maliciously activated for a non-relevant
// operation selector, i.e., op_err == 1 ==> sel_op_div || sel_op_XXX || ...
// op_err * (sel_op_div + sel_op_XXX + ... - 1) == 0
// Note that the above is even a stronger constraint, as it shows
// that exactly one sel_op_XXX must be true.
// At this time, we have only division producing an error.
#[SUBOP_ERROR_RELEVANT_OP]
op_err * (sel_op_div - 1) = 0;

// TODO: constraint that we stop execution at the first error (tag_err or op_err)
// An error can only happen at the last sub-operation row.

// OPEN/POTENTIAL OPTIMIZATION: Dedicated error per relevant operation?
// For the division, we could lower the degree from 4 to 3
// (sel_op_div - op_div_err) * (ic * ib - ia) = 0;
// Same for the relations related to the error activation:
// (ib * inv - 1 + op_div_err) = 0 && op_err * (1 - inv) = 0
// This works in combination with op_div_err * (sel_op_div - 1) = 0;
// Drawback is the need to paralllelize the latter.

//===== CONTROL FLOW =======================================================
//===== JUMP ===============================================================
sel_jump * (pc' - ia) = 0;

//===== INTERNAL_CALL ======================================================
// - The program counter in the next row should be equal to the value loaded from the ia register
// - We then write the return location (pc + 1) into the call stack (in memory)

#[RETURN_POINTER_INCREMENT]
sel_internal_call * (internal_return_ptr' - (internal_return_ptr + 1)) = 0;
sel_internal_call * (internal_return_ptr - mem_idx_b) = 0;
sel_internal_call * (pc' - ia) = 0;
sel_internal_call * ((pc + 1) - ib) = 0;

// TODO(md): Below relations may be removed through sub-op table lookup
sel_internal_call * (rwb - 1) = 0;
sel_internal_call * (mem_op_b - 1) = 0;

//===== INTERNAL_RETURN ===================================================
// - We load the memory pointer to be the internal_return_ptr
// - Constrain then next program counter to be the loaded value
// - decrement the internal_return_ptr

#[RETURN_POINTER_DECREMENT]
sel_internal_return * (internal_return_ptr' - (internal_return_ptr - 1)) = 0;
sel_internal_return * ((internal_return_ptr - 1) - mem_idx_a) = 0;
sel_internal_return * (pc' - ia) = 0;

// TODO(md): Below relations may be removed through sub-op table lookup
sel_internal_return * rwa = 0;
sel_internal_return * (mem_op_a - 1) = 0;

//===== CONTROL_FLOW_CONSISTENCY ============================================
pol INTERNAL_CALL_STACK_SELECTORS = (first + sel_internal_call + sel_internal_return + sel_halt);
pol OPCODE_SELECTORS = (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul);

// Program counter must increment if not jumping or returning
#[PC_INCREMENT]
(1 - first) * (1 - sel_halt) * OPCODE_SELECTORS * (pc' - (pc + 1)) = 0;

// first == 0 && sel_internal_call == 0 && sel_internal_return == 0 && sel_halt == 0 ==> internal_return_ptr == internal_return_ptr'
#[INTERNAL_RETURN_POINTER_CONSISTENCY]
(1 - INTERNAL_CALL_STACK_SELECTORS) * (internal_return_ptr' - internal_return_ptr) = 0;

// TODO: we want to set an initial number for the reserved memory of the jump pointer

// Inter-table Constraints

// TODO: tag_err {clk} IS memTrace.m_tag_err {memTrace.m_clk}
// TODO: Map memory trace with intermediate register values whenever there is no tag error, sthg like:
// mem_op_a * (1 - tag_err) {mem_idx_a, clk, ia, rwa} IS m_sub_clk == 0 && 1 - m_tag_err {m_addr, m_clk, m_val, m_rw}
51 changes: 29 additions & 22 deletions yarn-project/acir-simulator/src/avm/index.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import { MockProxy, mock } from 'jest-mock-extended';

import { AvmMachineState } from './avm_machine_state.js';
import { TypeTag } from './avm_memory_types.js';
import { initExecutionEnvironment } from './fixtures/index.js';
import { initExecutionEnvironment, initGlobalVariables } from './fixtures/index.js';
import { executeAvm } from './interpreter/interpreter.js';
import { AvmJournal } from './journal/journal.js';
import { Add, CalldataCopy, Return } from './opcodes/index.js';
Expand Down Expand Up @@ -68,14 +68,21 @@ describe('avm', () => {
});

describe('Test env getters from noir contract', () => {
const testEnvGetter = async (valueName: string, value: any, functionName: string) => {
const testEnvGetter = async (valueName: string, value: any, functionName: string, globalVar: boolean = false) => {
const getterArtifact = AvmTestContractArtifact.functions.find(f => f.name === functionName);

// Decode
const instructions = decodeFromBytecode(Buffer.from(getterArtifact!.bytecode, 'base64'));

// Execute
const overrides = { [valueName]: value };
let overrides = {};
if (globalVar === true) {
const globals = initGlobalVariables({ [valueName]: value });
overrides = { globals };
} else {
overrides = { [valueName]: value };
}

const context = new AvmMachineState(initExecutionEnvironment(overrides));
const avmReturnData = await executeAvm(context, journal, instructions);

Expand Down Expand Up @@ -126,25 +133,25 @@ describe('avm', () => {
await testEnvGetter('feePerDaGas', fee, 'avm_getFeePerDaGas');
});

// it('chainId', async () => {
// const chainId = new Fr(1);
// await testEnvGetter('chainId', chainId, 'avm_getChainId');
// });

// it('version', async () => {
// const version = new Fr(1);
// await testEnvGetter('version', version, 'avm_getVersion');
// });

// it('blockNumber', async () => {
// const blockNumber = new Fr(1);
// await testEnvGetter('blockNumber', blockNumber, 'avm_getBlockNumber');
// });

// it('timestamp', async () => {
// const timestamp = new Fr(1);
// await testEnvGetter('timestamp', timestamp, 'avm_getTimestamp');
// });
it('chainId', async () => {
const chainId = new Fr(1);
await testEnvGetter('chainId', chainId, 'avm_getChainId', /*globalVar=*/ true);
});

it('version', async () => {
const version = new Fr(1);
await testEnvGetter('version', version, 'avm_getVersion', /*globalVar=*/ true);
});

it('blockNumber', async () => {
const blockNumber = new Fr(1);
await testEnvGetter('blockNumber', blockNumber, 'avm_getBlockNumber', /*globalVar=*/ true);
});

it('timestamp', async () => {
const timestamp = new Fr(1);
await testEnvGetter('timestamp', timestamp, 'avm_getTimestamp', /*globalVar=*/ true);
});
});
});
});
1 change: 0 additions & 1 deletion yarn-project/aztec-nr/aztec/src/avm.nr
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
mod context;
mod env_getters;
Loading

0 comments on commit a973df0

Please sign in to comment.