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 committed Oct 16, 2024
1 parent dc1d77f commit 771a399
Show file tree
Hide file tree
Showing 35 changed files with 163 additions and 248 deletions.
3 changes: 1 addition & 2 deletions avm-transpiler/src/instructions.rs
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
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
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
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
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
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
55 changes: 1 addition & 54 deletions barretenberg/cpp/src/barretenberg/dsl/acir_format/serde/acir.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -145,12 +145,6 @@ struct BinaryIntOp {

struct IntegerBitSize {

struct U0 {
friend bool operator==(const U0&, const U0&);
std::vector<uint8_t> bincodeSerialize() const;
static U0 bincodeDeserialize(std::vector<uint8_t>);
};

struct U1 {
friend bool operator==(const U1&, const U1&);
std::vector<uint8_t> bincodeSerialize() const;
Expand Down Expand Up @@ -187,7 +181,7 @@ struct IntegerBitSize {
static U128 bincodeDeserialize(std::vector<uint8_t>);
};

std::variant<U0, U1, U8, U16, U32, U64, U128> value;
std::variant<U1, U8, U16, U32, U64, U128> value;

friend bool operator==(const IntegerBitSize&, const IntegerBitSize&);
std::vector<uint8_t> bincodeSerialize() const;
Expand Down Expand Up @@ -6690,53 +6684,6 @@ Program::BrilligOpcode::Store serde::Deserializable<Program::BrilligOpcode::Stor

namespace Program {

inline bool operator==(const BrilligOpcode::BlackBox& lhs, const BrilligOpcode::BlackBox& rhs)
{
if (!(lhs.value == rhs.value)) {
return false;
}
return true;
}

inline std::vector<uint8_t> BrilligOpcode::BlackBox::bincodeSerialize() const
{
auto serializer = serde::BincodeSerializer();
serde::Serializable<BrilligOpcode::BlackBox>::serialize(*this, serializer);
return std::move(serializer).bytes();
}

inline BrilligOpcode::BlackBox BrilligOpcode::BlackBox::bincodeDeserialize(std::vector<uint8_t> input)
{
auto deserializer = serde::BincodeDeserializer(input);
auto value = serde::Deserializable<BrilligOpcode::BlackBox>::deserialize(deserializer);
if (deserializer.get_buffer_offset() < input.size()) {
throw_or_abort("Some input bytes were not read");
}
return value;
}

} // end of namespace Program

template <>
template <typename Serializer>
void serde::Serializable<Program::BrilligOpcode::BlackBox>::serialize(const Program::BrilligOpcode::BlackBox& obj,
Serializer& serializer)
{
serde::Serializable<decltype(obj.value)>::serialize(obj.value, serializer);
}

template <>
template <typename Deserializer>
Program::BrilligOpcode::BlackBox serde::Deserializable<Program::BrilligOpcode::BlackBox>::deserialize(
Deserializer& deserializer)
{
Program::BrilligOpcode::BlackBox obj;
obj.value = serde::Deserializable<decltype(obj.value)>::deserialize(deserializer);
return obj;
}

namespace Program {

inline bool operator==(const BrilligOpcode::Trap& lhs, const BrilligOpcode::Trap& rhs)
{
if (!(lhs.revert_data == rhs.revert_data)) {
Expand Down
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
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
Loading

0 comments on commit 771a399

Please sign in to comment.