Skip to content

Commit

Permalink
3738 - add witness generation for multiplication with types u8, u16,
Browse files Browse the repository at this point in the history 
u32, u64
  • Loading branch information
@jeanmon
jeanmon committed Jan 11, 2024
1 parent 74e8714 commit 8e4f299
Show file tree
Hide file tree
Showing 13 changed files with 362 additions and 254 deletions.
4 changes: 4 additions & 0 deletions barretenberg/cpp/pil/avm/alu_chip.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,6 +157,10 @@ namespace aluChip(256);

// ========= MULTIPLICATION Operation Constraints ===============================

// ff multiplication
#[SUBOP_MULTIPLICATION_FF]
alu_ff_tag * alu_op_mul * (alu_ia * alu_ib - alu_ic) = 0;

// We need 2k bits to express the product (a*b) over the integer, i.e., for type uk
// we express the product as sum_k (u8 is an exception as we need 8-bit registers)

Expand Down
4 changes: 0 additions & 4 deletions barretenberg/cpp/pil/avm/avm_mini.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,10 +103,6 @@ namespace avmMini(256);
tag_err * ib = 0;
tag_err * ic = 0;

// Relation for multiplication over the finite field
#[SUBOP_MULTIPLICATION_FF]
sel_op_mul * (ia * ib - 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]
Expand Down
105 changes: 42 additions & 63 deletions barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ class AvmMiniFlavor {
// the unshifted and one for the shifted
static constexpr size_t NUM_ALL_ENTITIES = 80;

using Relations = std::tuple<AvmMini_vm::mem_trace<FF>, AvmMini_vm::alu_chip<FF>, AvmMini_vm::avm_mini<FF>>;
using Relations = std::tuple<AvmMini_vm::avm_mini<FF>, AvmMini_vm::alu_chip<FF>, AvmMini_vm::mem_trace<FF>>;

static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length<Relations>();

Expand Down Expand Up @@ -281,20 +281,20 @@ class AvmMiniFlavor {
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last,
memTrace_m_rw_shift,
memTrace_m_val_shift,
memTrace_m_addr_shift,
memTrace_m_tag_shift,
avmMini_pc_shift,
avmMini_internal_return_ptr_shift,
aluChip_alu_u16_r0_shift,
aluChip_alu_u16_r7_shift,
aluChip_alu_u16_r6_shift,
aluChip_alu_u16_r1_shift,
aluChip_alu_u16_r3_shift,
aluChip_alu_u16_r4_shift,
aluChip_alu_u16_r2_shift,
aluChip_alu_u16_r1_shift,
aluChip_alu_u16_r5_shift,
aluChip_alu_u16_r0_shift,
aluChip_alu_u16_r7_shift,
aluChip_alu_u16_r3_shift,
avmMini_internal_return_ptr_shift,
avmMini_pc_shift)
memTrace_m_addr_shift,
memTrace_m_val_shift,
memTrace_m_tag_shift,
memTrace_m_rw_shift)

RefVector<DataType> get_wires()
{
Expand Down Expand Up @@ -364,20 +364,20 @@ class AvmMiniFlavor {
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last,
memTrace_m_rw_shift,
memTrace_m_val_shift,
memTrace_m_addr_shift,
memTrace_m_tag_shift,
avmMini_pc_shift,
avmMini_internal_return_ptr_shift,
aluChip_alu_u16_r0_shift,
aluChip_alu_u16_r7_shift,
aluChip_alu_u16_r6_shift,
aluChip_alu_u16_r1_shift,
aluChip_alu_u16_r3_shift,
aluChip_alu_u16_r4_shift,
aluChip_alu_u16_r2_shift,
aluChip_alu_u16_r1_shift,
aluChip_alu_u16_r5_shift,
aluChip_alu_u16_r0_shift,
aluChip_alu_u16_r7_shift,
aluChip_alu_u16_r3_shift,
avmMini_internal_return_ptr_shift,
avmMini_pc_shift };
memTrace_m_addr_shift,
memTrace_m_val_shift,
memTrace_m_tag_shift,
memTrace_m_rw_shift };
};
RefVector<DataType> get_unshifted()
{
Expand Down Expand Up @@ -450,37 +450,23 @@ class AvmMiniFlavor {
};
RefVector<DataType> get_to_be_shifted()
{
return { memTrace_m_rw,
memTrace_m_val,
memTrace_m_addr,
memTrace_m_tag,
aluChip_alu_u16_r6,
aluChip_alu_u16_r1,
aluChip_alu_u16_r4,
aluChip_alu_u16_r2,
aluChip_alu_u16_r5,
aluChip_alu_u16_r0,
aluChip_alu_u16_r7,
aluChip_alu_u16_r3,
avmMini_internal_return_ptr,
avmMini_pc };
return { avmMini_pc, avmMini_internal_return_ptr,
aluChip_alu_u16_r0, aluChip_alu_u16_r7,
aluChip_alu_u16_r6, aluChip_alu_u16_r3,
aluChip_alu_u16_r4, aluChip_alu_u16_r2,
aluChip_alu_u16_r1, aluChip_alu_u16_r5,
memTrace_m_addr, memTrace_m_val,
memTrace_m_tag, memTrace_m_rw };
};
RefVector<DataType> get_shifted()
{
return { memTrace_m_rw_shift,
memTrace_m_val_shift,
memTrace_m_addr_shift,
memTrace_m_tag_shift,
aluChip_alu_u16_r6_shift,
aluChip_alu_u16_r1_shift,
aluChip_alu_u16_r4_shift,
aluChip_alu_u16_r2_shift,
aluChip_alu_u16_r5_shift,
aluChip_alu_u16_r0_shift,
aluChip_alu_u16_r7_shift,
aluChip_alu_u16_r3_shift,
avmMini_internal_return_ptr_shift,
avmMini_pc_shift };
return { avmMini_pc_shift, avmMini_internal_return_ptr_shift,
aluChip_alu_u16_r0_shift, aluChip_alu_u16_r7_shift,
aluChip_alu_u16_r6_shift, aluChip_alu_u16_r3_shift,
aluChip_alu_u16_r4_shift, aluChip_alu_u16_r2_shift,
aluChip_alu_u16_r1_shift, aluChip_alu_u16_r5_shift,
memTrace_m_addr_shift, memTrace_m_val_shift,
memTrace_m_tag_shift, memTrace_m_rw_shift };
};
};

Expand All @@ -493,20 +479,13 @@ class AvmMiniFlavor {

RefVector<DataType> get_to_be_shifted()
{
return { memTrace_m_rw,
memTrace_m_val,
memTrace_m_addr,
memTrace_m_tag,
aluChip_alu_u16_r6,
aluChip_alu_u16_r1,
aluChip_alu_u16_r4,
aluChip_alu_u16_r2,
aluChip_alu_u16_r5,
aluChip_alu_u16_r0,
aluChip_alu_u16_r7,
aluChip_alu_u16_r3,
avmMini_internal_return_ptr,
avmMini_pc };
return { avmMini_pc, avmMini_internal_return_ptr,
aluChip_alu_u16_r0, aluChip_alu_u16_r7,
aluChip_alu_u16_r6, aluChip_alu_u16_r3,
aluChip_alu_u16_r4, aluChip_alu_u16_r2,
aluChip_alu_u16_r1, aluChip_alu_u16_r5,
memTrace_m_addr, memTrace_m_val,
memTrace_m_tag, memTrace_m_rw };
};

// The plookup wires that store plookup read data.
Expand Down
48 changes: 24 additions & 24 deletions ...g/cpp/src/barretenberg/proof_system/circuit_builder/generated/AvmMini_circuit_builder.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,20 +86,20 @@ template <typename FF> struct AvmMiniFullRow {
FF avmMini_mem_idx_b{};
FF avmMini_mem_idx_c{};
FF avmMini_last{};
FF memTrace_m_rw_shift{};
FF memTrace_m_val_shift{};
FF memTrace_m_addr_shift{};
FF memTrace_m_tag_shift{};
FF avmMini_pc_shift{};
FF avmMini_internal_return_ptr_shift{};
FF aluChip_alu_u16_r0_shift{};
FF aluChip_alu_u16_r7_shift{};
FF aluChip_alu_u16_r6_shift{};
FF aluChip_alu_u16_r1_shift{};
FF aluChip_alu_u16_r3_shift{};
FF aluChip_alu_u16_r4_shift{};
FF aluChip_alu_u16_r2_shift{};
FF aluChip_alu_u16_r1_shift{};
FF aluChip_alu_u16_r5_shift{};
FF aluChip_alu_u16_r0_shift{};
FF aluChip_alu_u16_r7_shift{};
FF aluChip_alu_u16_r3_shift{};
FF avmMini_internal_return_ptr_shift{};
FF avmMini_pc_shift{};
FF memTrace_m_addr_shift{};
FF memTrace_m_val_shift{};
FF memTrace_m_tag_shift{};
FF memTrace_m_rw_shift{};
};

class AvmMiniCircuitBuilder {
Expand Down Expand Up @@ -197,20 +197,20 @@ class AvmMiniCircuitBuilder {
polys.avmMini_last[i] = rows[i].avmMini_last;
}

polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.shifted());
polys.memTrace_m_val_shift = Polynomial(polys.memTrace_m_val.shifted());
polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted());
polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted());
polys.avmMini_pc_shift = Polynomial(polys.avmMini_pc.shifted());
polys.avmMini_internal_return_ptr_shift = Polynomial(polys.avmMini_internal_return_ptr.shifted());
polys.aluChip_alu_u16_r0_shift = Polynomial(polys.aluChip_alu_u16_r0.shifted());
polys.aluChip_alu_u16_r7_shift = Polynomial(polys.aluChip_alu_u16_r7.shifted());
polys.aluChip_alu_u16_r6_shift = Polynomial(polys.aluChip_alu_u16_r6.shifted());
polys.aluChip_alu_u16_r1_shift = Polynomial(polys.aluChip_alu_u16_r1.shifted());
polys.aluChip_alu_u16_r3_shift = Polynomial(polys.aluChip_alu_u16_r3.shifted());
polys.aluChip_alu_u16_r4_shift = Polynomial(polys.aluChip_alu_u16_r4.shifted());
polys.aluChip_alu_u16_r2_shift = Polynomial(polys.aluChip_alu_u16_r2.shifted());
polys.aluChip_alu_u16_r1_shift = Polynomial(polys.aluChip_alu_u16_r1.shifted());
polys.aluChip_alu_u16_r5_shift = Polynomial(polys.aluChip_alu_u16_r5.shifted());
polys.aluChip_alu_u16_r0_shift = Polynomial(polys.aluChip_alu_u16_r0.shifted());
polys.aluChip_alu_u16_r7_shift = Polynomial(polys.aluChip_alu_u16_r7.shifted());
polys.aluChip_alu_u16_r3_shift = Polynomial(polys.aluChip_alu_u16_r3.shifted());
polys.avmMini_internal_return_ptr_shift = Polynomial(polys.avmMini_internal_return_ptr.shifted());
polys.avmMini_pc_shift = Polynomial(polys.avmMini_pc.shifted());
polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted());
polys.memTrace_m_val_shift = Polynomial(polys.memTrace_m_val.shifted());
polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted());
polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.shifted());

return polys;
}
Expand Down Expand Up @@ -248,16 +248,16 @@ class AvmMiniCircuitBuilder {
return true;
};

if (!evaluate_relation.template operator()<AvmMini_vm::mem_trace<FF>>(
"mem_trace", AvmMini_vm::get_relation_label_mem_trace)) {
if (!evaluate_relation.template operator()<AvmMini_vm::avm_mini<FF>>("avm_mini",
AvmMini_vm::get_relation_label_avm_mini)) {
return false;
}
if (!evaluate_relation.template operator()<AvmMini_vm::alu_chip<FF>>("alu_chip",
AvmMini_vm::get_relation_label_alu_chip)) {
return false;
}
if (!evaluate_relation.template operator()<AvmMini_vm::avm_mini<FF>>("avm_mini",
AvmMini_vm::get_relation_label_avm_mini)) {
if (!evaluate_relation.template operator()<AvmMini_vm::mem_trace<FF>>(
"mem_trace", AvmMini_vm::get_relation_label_mem_trace)) {
return false;
}

Expand Down
Loading

0 comments on commit 8e4f299

Please sign in to comment.