-
Notifications
You must be signed in to change notification settings - Fork 265
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: test globals, run write oracles inline
- Loading branch information
Showing
7 changed files
with
274 additions
and
172 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1 @@ | ||
mod context; | ||
mod env_getters; |
Oops, something went wrong.