Skip to content

Commit

Permalink
featBrillig and AVM default all uninitialized memory cells to Field 0
Browse files Browse the repository at this point in the history
  • Loading branch information
@dbanks12
dbanks12 committed Oct 11, 2024
1 parent 8adbdd5 commit e68b96b
Show file tree
Hide file tree
Showing 35 changed files with 163 additions and 195 deletions.
3 changes: 1 addition & 2 deletions avm-transpiler/src/instructions.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,14 +88,13 @@ impl Default for AvmInstruction {
#[allow(clippy::upper_case_acronyms, dead_code)]
#[derive(Copy, Clone, Debug)]
pub enum AvmTypeTag {
UNINITIALIZED,
FIELD,
UINT1,
UINT8,
UINT16,
UINT32,
UINT64,
UINT128,
FIELD,
INVALID,
}

Expand Down
1 change: 0 additions & 1 deletion avm-transpiler/src/transpile.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1497,6 +1497,5 @@ fn tag_from_bit_size(bit_size: BitSize) -> AvmTypeTag {
BitSize::Integer(IntegerBitSize::U64) => AvmTypeTag::UINT64,
BitSize::Integer(IntegerBitSize::U128) => AvmTypeTag::UINT128,
BitSize::Field => AvmTypeTag::FIELD,
_ => panic!("The AVM doesn't support integer bit size {:?}", bit_size),
}
}
2 changes: 1 addition & 1 deletion barretenberg/cpp/pil/avm/alu.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ namespace alu(256);
pol commit ic;
pol commit sel_alu; // Predicate to activate the copy of intermediate registers to ALU table.

// Instruction tag (1: u1, 2: u8, 3: u16, 4: u32, 5: u64, 6: u128, 7: field) copied from Main table
// Instruction tag copied from Main table (MEM_TAG enum defined in constants)
pol commit in_tag;

// Flattened boolean instruction tags
Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/pil/avm/constants_gen.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,13 @@ namespace constants(256);
pol MAX_NULLIFIER_NON_EXISTENT_READ_REQUESTS_PER_CALL = 16;
pol MAX_L1_TO_L2_MSG_READ_REQUESTS_PER_CALL = 16;
pol MAX_UNENCRYPTED_LOGS_PER_CALL = 4;
pol MEM_TAG_FF = 0;
pol MEM_TAG_U1 = 1;
pol MEM_TAG_U8 = 2;
pol MEM_TAG_U16 = 3;
pol MEM_TAG_U32 = 4;
pol MEM_TAG_U64 = 5;
pol MEM_TAG_U128 = 6;
pol MEM_TAG_FF = 7;
pol SENDER_KERNEL_INPUTS_COL_OFFSET = 0;
pol ADDRESS_KERNEL_INPUTS_COL_OFFSET = 1;
pol STORAGE_ADDRESS_KERNEL_INPUTS_COL_OFFSET = 1;
Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/pil/avm/main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ namespace main(256);
// Helper selector to characterize a Binary chiplet selector
pol commit sel_bin;

// Instruction memory tags read/write (1: u1, 2: u8, 3: u16, 4: u32, 5: u64, 6: u128, 7: field)
// Instruction memory tags read/write (enum defined in constants)
pol commit r_in_tag;
pol commit w_in_tag;
pol commit alu_in_tag; // Copy of r_in_tag or w_in_tag depending of the operation. It is sent to ALU trace.
Expand Down
16 changes: 9 additions & 7 deletions barretenberg/cpp/pil/avm/mem.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ namespace mem(256);
pol commit addr;
pol commit space_id;
pol commit glob_addr;
pol commit tag; // Memory tag (0: uninitialized, 1: u1, 2: u8, 3: u16, 4: u32, 5: u64, 6: u128, 7:field)
pol commit tag; // Memory tag (MEM_TAG enum defined in constants)
pol commit val;
pol commit rw; // Enum: 0 (read), 1 (write)
pol commit lastAccess; // Boolean (1 when this row is the last of a given address)
Expand Down Expand Up @@ -175,13 +175,16 @@ namespace mem(256);
#[MEM_READ_WRITE_TAG_CONSISTENCY]
(1 - lastAccess) * (1 - rw') * (tag' - tag) = 0;

// If this is the last row that an address is accessed, the next row must be the first access of another address.
// Constrain that the first load from a given address has value 0. (Consistency of memory initialization.)
// We do not constrain that the tag == 0 as the 0 value is compatible with any memory type.
// As we enforce lastAccess = 1 on the first row, the following condition applies also for the first memory entry:
#[MEM_ZERO_INIT]
lastAccess * (1 - rw') * val' = 0;
// Constrain that reading an uninitialized cell creates tag error unless it is expected to be of type FF.
#[MEM_ZERO_INIT_TAG_FF]
lastAccess * (1 - rw') * (tag' - constants.MEM_TAG_FF) = 0;

// TODO: Verfiy that skip_check_tag cannot be enabled maliciously by the prover.
// TODO: Verify that skip_check_tag cannot be enabled maliciously by the prover.
// Skip check tag enabled for some MOV opcodes and RETURN opcode (sel_op_slice)
#[SKIP_CHECK_TAG]
skip_check_tag = sel_op_slice;
Expand All @@ -199,14 +202,13 @@ namespace mem(256);
// instead of (r_in_tag - tag)^(-1) as this allows to store zero by default (i.e., when tag_err == 0).
// The new column one_min_inv is set to 1 - (r_in_tag - tag)^(-1) when tag_err == 1
// but must be set to 0 when tags are matching and tag_err = 0
// Relaxation: This relation is relaxed when skip_check_tag is enabled or for
// uninitialized memory, i.e. tag == 0.
// Relaxation: This relation is relaxed when skip_check_tag is enabled
#[MEM_IN_TAG_CONSISTENCY_1]
tag * (1 - skip_check_tag) * (1 - rw) * ((r_in_tag - tag) * (1 - one_min_inv) - tag_err) = 0;
(1 - skip_check_tag) * (1 - rw) * ((r_in_tag - tag) * (1 - one_min_inv) - tag_err) = 0;
// TODO: Try to decrease the degree of the above relation, e.g., skip_check_tag might be consolidated
// with tag == 0 and rw == 1.
#[MEM_IN_TAG_CONSISTENCY_2]
tag * (1 - tag_err) * one_min_inv = 0;
(1 - tag_err) * one_min_inv = 0;

#[NO_TAG_ERR_WRITE_OR_SKIP]
(skip_check_tag + rw) * tag_err = 0;
Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/src/barretenberg/vm/avm/generated/relations/alu.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,13 +21,13 @@ template <typename FF_> class aluImpl {
[[maybe_unused]] const RelationParameters<FF>&,
[[maybe_unused]] const FF& scaling_factor)
{
const auto constants_MEM_TAG_FF = FF(0);
const auto constants_MEM_TAG_U1 = FF(1);
const auto constants_MEM_TAG_U8 = FF(2);
const auto constants_MEM_TAG_U16 = FF(3);
const auto constants_MEM_TAG_U32 = FF(4);
const auto constants_MEM_TAG_U64 = FF(5);
const auto constants_MEM_TAG_U128 = FF(6);
const auto constants_MEM_TAG_FF = FF(7);
const auto alu_MAX_BITS =
((((((new_term.alu_u1_tag * FF(1)) + (new_term.alu_u8_tag * FF(8))) + (new_term.alu_u16_tag * FF(16))) +
(new_term.alu_u32_tag * FF(32))) +
Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/src/barretenberg/vm/avm/generated/relations/main.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ template <typename FF_> class mainImpl {
[[maybe_unused]] const RelationParameters<FF>&,
[[maybe_unused]] const FF& scaling_factor)
{
const auto constants_MEM_TAG_FF = FF(0);
const auto constants_MEM_TAG_U1 = FF(1);
const auto constants_MEM_TAG_FF = FF(7);
const auto constants_misc_INTERNAL_CALL_SPACE_ID = FF(255);
const auto main_KERNEL_INPUT_SELECTORS =
(((((((((((new_term.main_sel_op_address + new_term.main_sel_op_storage_address) +
Expand Down
83 changes: 46 additions & 37 deletions barretenberg/cpp/src/barretenberg/vm/avm/generated/relations/mem.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,19 +10,19 @@ template <typename FF_> class memImpl {
public:
using FF = FF_;

static constexpr std::array<size_t, 52> SUBRELATION_PARTIAL_LENGTHS = { 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3,
2, 3, 4, 3, 4, 3, 3, 2, 3, 3, 4, 4, 4,
4, 2, 6, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3,
3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3 };
static constexpr std::array<size_t, 53> SUBRELATION_PARTIAL_LENGTHS = { 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2,
3, 4, 3, 4, 3, 3, 2, 3, 3, 4, 4, 4, 4, 4,
2, 5, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3,
3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3 };

template <typename ContainerOverSubrelations, typename AllEntities>
void static accumulate(ContainerOverSubrelations& evals,
const AllEntities& new_term,
[[maybe_unused]] const RelationParameters<FF>&,
[[maybe_unused]] const FF& scaling_factor)
{
const auto constants_MEM_TAG_FF = FF(0);
const auto constants_MEM_TAG_U32 = FF(4);
const auto constants_MEM_TAG_FF = FF(7);
const auto mem_SEL_DIRECT_MEM_OP_A =
((new_term.mem_sel_op_a + new_term.mem_sel_op_poseidon_read_a) + new_term.mem_sel_op_poseidon_write_a);
const auto mem_SEL_DIRECT_MEM_OP_B =
Expand Down Expand Up @@ -218,156 +218,163 @@ template <typename FF_> class memImpl {
}
{
using Accumulator = typename std::tuple_element_t<27, ContainerOverSubrelations>;
auto tmp = (new_term.mem_skip_check_tag - new_term.mem_sel_op_slice);
auto tmp = ((new_term.mem_lastAccess * (FF(1) - new_term.mem_rw_shift)) *
(new_term.mem_tag_shift - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<27>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<28, ContainerOverSubrelations>;
auto tmp = (((new_term.mem_tag * (FF(1) - new_term.mem_skip_check_tag)) * (FF(1) - new_term.mem_rw)) *
(((new_term.mem_r_in_tag - new_term.mem_tag) * (FF(1) - new_term.mem_one_min_inv)) -
new_term.mem_tag_err));
auto tmp = (new_term.mem_skip_check_tag - new_term.mem_sel_op_slice);
tmp *= scaling_factor;
std::get<28>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<29, ContainerOverSubrelations>;
auto tmp = ((new_term.mem_tag * (FF(1) - new_term.mem_tag_err)) * new_term.mem_one_min_inv);
auto tmp = (((FF(1) - new_term.mem_skip_check_tag) * (FF(1) - new_term.mem_rw)) *
(((new_term.mem_r_in_tag - new_term.mem_tag) * (FF(1) - new_term.mem_one_min_inv)) -
new_term.mem_tag_err));
tmp *= scaling_factor;
std::get<29>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<30, ContainerOverSubrelations>;
auto tmp = ((new_term.mem_skip_check_tag + new_term.mem_rw) * new_term.mem_tag_err);
auto tmp = ((FF(1) - new_term.mem_tag_err) * new_term.mem_one_min_inv);
tmp *= scaling_factor;
std::get<30>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<31, ContainerOverSubrelations>;
auto tmp = (new_term.mem_rw * (new_term.mem_w_in_tag - new_term.mem_tag));
auto tmp = ((new_term.mem_skip_check_tag + new_term.mem_rw) * new_term.mem_tag_err);
tmp *= scaling_factor;
std::get<31>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<32, ContainerOverSubrelations>;
auto tmp = (new_term.mem_rw * new_term.mem_tag_err);
auto tmp = (new_term.mem_rw * (new_term.mem_w_in_tag - new_term.mem_tag));
tmp *= scaling_factor;
std::get<32>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<33, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_resolve_ind_addr_a * (new_term.mem_r_in_tag - constants_MEM_TAG_U32));
auto tmp = (new_term.mem_rw * new_term.mem_tag_err);
tmp *= scaling_factor;
std::get<33>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<34, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_resolve_ind_addr_b * (new_term.mem_r_in_tag - constants_MEM_TAG_U32));
auto tmp = (new_term.mem_sel_resolve_ind_addr_a * (new_term.mem_r_in_tag - constants_MEM_TAG_U32));
tmp *= scaling_factor;
std::get<34>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<35, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_resolve_ind_addr_c * (new_term.mem_r_in_tag - constants_MEM_TAG_U32));
auto tmp = (new_term.mem_sel_resolve_ind_addr_b * (new_term.mem_r_in_tag - constants_MEM_TAG_U32));
tmp *= scaling_factor;
std::get<35>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<36, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_resolve_ind_addr_d * (new_term.mem_r_in_tag - constants_MEM_TAG_U32));
auto tmp = (new_term.mem_sel_resolve_ind_addr_c * (new_term.mem_r_in_tag - constants_MEM_TAG_U32));
tmp *= scaling_factor;
std::get<36>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<37, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_resolve_ind_addr_a * new_term.mem_rw);
auto tmp = (new_term.mem_sel_resolve_ind_addr_d * (new_term.mem_r_in_tag - constants_MEM_TAG_U32));
tmp *= scaling_factor;
std::get<37>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<38, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_resolve_ind_addr_b * new_term.mem_rw);
auto tmp = (new_term.mem_sel_resolve_ind_addr_a * new_term.mem_rw);
tmp *= scaling_factor;
std::get<38>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<39, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_resolve_ind_addr_c * new_term.mem_rw);
auto tmp = (new_term.mem_sel_resolve_ind_addr_b * new_term.mem_rw);
tmp *= scaling_factor;
std::get<39>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<40, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_resolve_ind_addr_d * new_term.mem_rw);
auto tmp = (new_term.mem_sel_resolve_ind_addr_c * new_term.mem_rw);
tmp *= scaling_factor;
std::get<40>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<41, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_slice * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_resolve_ind_addr_d * new_term.mem_rw);
tmp *= scaling_factor;
std::get<41>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<42, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_slice * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_op_slice * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<42>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<43, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_poseidon_read_a * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_op_slice * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<43>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<44, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_poseidon_read_b * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_op_poseidon_read_a * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<44>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<45, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_poseidon_read_c * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_op_poseidon_read_b * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<45>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<46, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_poseidon_read_d * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_op_poseidon_read_c * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<46>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<47, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_poseidon_write_a * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_op_poseidon_read_d * (new_term.mem_w_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<47>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<48, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_poseidon_write_b * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_op_poseidon_write_a * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<48>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<49, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_poseidon_write_c * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_op_poseidon_write_b * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<49>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<50, ContainerOverSubrelations>;
auto tmp = (new_term.mem_sel_op_poseidon_write_d * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
auto tmp = (new_term.mem_sel_op_poseidon_write_c * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<50>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<51, ContainerOverSubrelations>;
auto tmp = ((new_term.mem_sel_mov_ia_to_ic + new_term.mem_sel_mov_ib_to_ic) * new_term.mem_tag_err);
auto tmp = (new_term.mem_sel_op_poseidon_write_d * (new_term.mem_r_in_tag - constants_MEM_TAG_FF));
tmp *= scaling_factor;
std::get<51>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<52, ContainerOverSubrelations>;
auto tmp = ((new_term.mem_sel_mov_ia_to_ic + new_term.mem_sel_mov_ib_to_ic) * new_term.mem_tag_err);
tmp *= scaling_factor;
std::get<52>(evals) += typename Accumulator::View(tmp);
}
}
};

Expand Down Expand Up @@ -399,16 +406,18 @@ template <typename FF> class mem : public Relation<memImpl<FF>> {
case 26:
return "MEM_ZERO_INIT";
case 27:
return "SKIP_CHECK_TAG";
return "MEM_ZERO_INIT_TAG_FF";
case 28:
return "MEM_IN_TAG_CONSISTENCY_1";
return "SKIP_CHECK_TAG";
case 29:
return "MEM_IN_TAG_CONSISTENCY_2";
return "MEM_IN_TAG_CONSISTENCY_1";
case 30:
return "MEM_IN_TAG_CONSISTENCY_2";
case 31:
return "NO_TAG_ERR_WRITE_OR_SKIP";
case 32:
case 33:
return "NO_TAG_ERR_WRITE";
case 51:
case 52:
return "MOV_SAME_TAG";
}
return std::to_string(index);
Expand Down
Loading

0 comments on commit e68b96b

Please sign in to comment.