Skip to content

Commit

Permalink
Comments in pil file related to range checks of addresses
Browse files Browse the repository at this point in the history
  • Loading branch information
jeanmon committed Jun 3, 2024
1 parent 008cea1 commit dc81fae
Showing 1 changed file with 13 additions and 4 deletions.
17 changes: 13 additions & 4 deletions barretenberg/cpp/pil/avm/avm_main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -302,10 +302,19 @@ namespace avm_main(256);
ind_op_c * (1 - ind_op_c) = 0;
ind_op_d * (1 - ind_op_d) = 0;

// TODO - Constraints:
// - mem_idx_a, mem_idx_b, mem_idx_c, mem_idx_d to u32 type
// - ind_a, ind_b, ind_c, ind_d to u32 type
// - 0 <= r_in_tag, w_in_tag <= 6 // Maybe not needed as probably derived by the operation decomposition.
// TODO - Potential constraints to be implemented:
// - mem_idx_a, mem_idx_b, mem_idx_c, mem_idx_d to u32 type:
// - For direct memory accesses, this should be enforced by bytecode validation
// and instruction decomposition. Namely, in this case, only 32-bit immediate
// values should be written into these memory indices.
// - For indirect memory accesses, the memory trace constraints ensure that
// loaded values come from memory addresses with tag u32. This is enforced in the memory trace
// where each memory entry with flag ind_op_x (for x = a,b,c,d) constrains r_int_tag == 3 (u32).
//
// - ind_a, ind_b, ind_c, ind_d to u32 type: Should be guaranteed by bytecode validation and
// instruction decomposition as only immediate 32-bit values should be written into the indirect registers.
//
// - 0 <= r_in_tag, w_in_tag <= 6 // This should be constrained by the operation decomposition.

//====== COMPARATOR OPCODES CONSTRAINTS =====================================
// Enforce that the tag for the ouput of EQ opcode is u8 (i.e. equal to 1).
Expand Down

0 comments on commit dc81fae

Please sign in to comment.