Skip to content

Commit

Permalink
3738 - bugfixing PIL relation for u128 multiplication and unit tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@jeanmon
jeanmon committed Jan 12, 2024
1 parent 1536b28 commit 5d9bda5
Show file tree
Hide file tree
Showing 9 changed files with 261 additions and 162 deletions.
4 changes: 2 additions & 2 deletions barretenberg/cpp/pil/avm/alu_chip.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -186,7 +186,7 @@ namespace aluChip(256);
// b = b_l + b_h * 2^64
// We show that c satisfies: a_l * b_l + (a_h * b_l + a_l * b_h) * 2^64 = R * 2^128 + c
// for a R < 2^65. Equivalently:
// a * b_l + a_l * b_h * 2^64 = (CF * 2^65 + R') * 2^128 + c
// a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R') * 2^128 + c
// for a bit carry flag CF and R' range constrained to 64 bits.
// We use two lines in the execution trace. First line represents a
// as decomposed over 16-bit registers. Second line represents b.
Expand All @@ -209,6 +209,6 @@ namespace aluChip(256);
alu_u128_tag * alu_op_mul * (
alu_ia * sum_shifted_64
+ sum_64 * sum_high_shifted_64 * 2**64
- (alu_cf * 2**65 + alu_u64_r0) * 2**128
- (alu_cf * 2**64 + alu_u64_r0) * 2**128
- alu_ic
) = 0;
62 changes: 28 additions & 34 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::avm_mini<FF>, AvmMini_vm::alu_chip<FF>, AvmMini_vm::mem_trace<FF>>;
using Relations = std::tuple<AvmMini_vm::alu_chip<FF>, AvmMini_vm::avm_mini<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,19 +281,19 @@ class AvmMiniFlavor {
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last,
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_r2_shift,
aluChip_alu_u16_r3_shift,
aluChip_alu_u16_r4_shift,
aluChip_alu_u16_r2_shift,
aluChip_alu_u16_r0_shift,
aluChip_alu_u16_r1_shift,
aluChip_alu_u16_r5_shift,
memTrace_m_addr_shift,
aluChip_alu_u16_r7_shift,
avmMini_internal_return_ptr_shift,
avmMini_pc_shift,
memTrace_m_val_shift,
memTrace_m_tag_shift,
memTrace_m_addr_shift,
memTrace_m_rw_shift)

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

Expand All @@ -479,13 +475,11 @@ class AvmMiniFlavor {

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

// The plookup wires that store plookup read data.
Expand Down
32 changes: 16 additions & 16 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,19 +86,19 @@ template <typename FF> struct AvmMiniFullRow {
FF avmMini_mem_idx_b{};
FF avmMini_mem_idx_c{};
FF avmMini_last{};
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_r2_shift{};
FF aluChip_alu_u16_r3_shift{};
FF aluChip_alu_u16_r4_shift{};
FF aluChip_alu_u16_r2_shift{};
FF aluChip_alu_u16_r0_shift{};
FF aluChip_alu_u16_r1_shift{};
FF aluChip_alu_u16_r5_shift{};
FF memTrace_m_addr_shift{};
FF aluChip_alu_u16_r7_shift{};
FF avmMini_internal_return_ptr_shift{};
FF avmMini_pc_shift{};
FF memTrace_m_val_shift{};
FF memTrace_m_tag_shift{};
FF memTrace_m_addr_shift{};
FF memTrace_m_rw_shift{};
};

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

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_r2_shift = Polynomial(polys.aluChip_alu_u16_r2.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_r0_shift = Polynomial(polys.aluChip_alu_u16_r0.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.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted());
polys.aluChip_alu_u16_r7_shift = Polynomial(polys.aluChip_alu_u16_r7.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_val_shift = Polynomial(polys.memTrace_m_val.shifted());
polys.memTrace_m_tag_shift = Polynomial(polys.memTrace_m_tag.shifted());
polys.memTrace_m_addr_shift = Polynomial(polys.memTrace_m_addr.shifted());
polys.memTrace_m_rw_shift = Polynomial(polys.memTrace_m_rw.shifted());

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

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)) {
return false;
}
if (!evaluate_relation.template operator()<AvmMini_vm::mem_trace<FF>>(
"mem_trace", AvmMini_vm::get_relation_label_mem_trace)) {
return false;
Expand Down
52 changes: 26 additions & 26 deletions barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/alu_chip.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,51 +7,51 @@
namespace proof_system::AvmMini_vm {

template <typename FF> struct Alu_chipRow {
FF aluChip_alu_op_sub{};
FF aluChip_alu_u8_r0{};
FF aluChip_alu_u16_r0_shift{};
FF aluChip_alu_cf{};
FF aluChip_alu_ic{};
FF aluChip_alu_u16_r7_shift{};
FF aluChip_alu_u128_tag{};
FF aluChip_alu_u16_r1{};
FF aluChip_alu_u16_r4{};
FF aluChip_alu_u16_r1{};
FF aluChip_alu_u16_tag{};
FF aluChip_alu_u8_tag{};
FF aluChip_alu_u8_r0{};
FF aluChip_alu_u16_r6{};
FF aluChip_alu_u8_r1{};
FF aluChip_alu_u16_r5{};
FF aluChip_alu_u16_r6_shift{};
FF aluChip_alu_op_add{};
FF aluChip_alu_u64_tag{};
FF aluChip_alu_ff_tag{};
FF aluChip_alu_u16_r3{};
FF aluChip_alu_u16_r0{};
FF aluChip_alu_u16_r2_shift{};
FF aluChip_alu_ib{};
FF aluChip_alu_ic{};
FF aluChip_alu_u16_r3_shift{};
FF aluChip_alu_u16_r7{};
FF aluChip_alu_u16_tag{};
FF aluChip_alu_op_mul{};
FF aluChip_alu_u16_r5{};
FF aluChip_alu_u8_tag{};
FF aluChip_alu_op_sub{};
FF aluChip_alu_ff_tag{};
FF aluChip_alu_u16_r2{};
FF aluChip_alu_u16_r4_shift{};
FF aluChip_alu_u64_tag{};
FF aluChip_alu_u32_tag{};
FF aluChip_alu_ia{};
FF aluChip_alu_u64_r0{};
FF aluChip_alu_u16_r4_shift{};
FF aluChip_alu_u16_r2_shift{};
FF aluChip_alu_u16_r2{};
FF aluChip_alu_ib{};
FF aluChip_alu_u8_r1{};
FF aluChip_alu_u16_r0_shift{};
FF aluChip_alu_u16_r3{};
FF aluChip_alu_op_mul{};
FF aluChip_alu_u16_r1_shift{};
FF aluChip_alu_u128_tag{};
FF aluChip_alu_u16_r5_shift{};
FF aluChip_alu_u16_r0{};
FF aluChip_alu_op_add{};
FF aluChip_alu_cf{};
FF aluChip_alu_u16_r7_shift{};
};

inline std::string get_relation_label_alu_chip(int index)
{
switch (index) {
case 6:
return "SUBOP_ADDITION_FF";

case 17:
return "SUBOP_SUBTRACTION_FF";

case 28:
return "SUBOP_MULTIPLICATION_FF";

case 6:
return "SUBOP_ADDITION_FF";
}
return std::to_string(index);
}
Expand Down Expand Up @@ -507,7 +507,7 @@ template <typename FF_> class alu_chipImpl {
(aluChip_alu_u16_r6_shift * FF(4294967296UL))) +
(aluChip_alu_u16_r7_shift * FF(281474976710656UL)))) *
FF(uint256_t{ 0, 1, 0, 0 }))) -
(((aluChip_alu_cf * FF(uint256_t{ 0, 2, 0, 0 })) + aluChip_alu_u64_r0) *
(((aluChip_alu_cf * FF(uint256_t{ 0, 1, 0, 0 })) + aluChip_alu_u64_r0) *
FF(uint256_t{ 0, 0, 1, 0 }))) -
aluChip_alu_ic));
tmp *= scaling_factor;
Expand Down
62 changes: 31 additions & 31 deletions barretenberg/cpp/src/barretenberg/relations/generated/AvmMini/avm_mini.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,61 +7,61 @@
namespace proof_system::AvmMini_vm {

template <typename FF> struct Avm_miniRow {
FF avmMini_mem_idx_a{};
FF avmMini_tag_err{};
FF avmMini_sel_op_sub{};
FF avmMini_rwc{};
FF avmMini_ia{};
FF avmMini_pc{};
FF avmMini_inv{};
FF avmMini_internal_return_ptr{};
FF avmMini_first{};
FF avmMini_ib{};
FF avmMini_mem_op_c{};
FF avmMini_mem_op_a{};
FF avmMini_sel_internal_return{};
FF avmMini_sel_halt{};
FF avmMini_mem_idx_b{};
FF avmMini_pc{};
FF avmMini_sel_op_div{};
FF avmMini_sel_op_mul{};
FF avmMini_sel_op_add{};
FF avmMini_rwa{};
FF avmMini_ia{};
FF avmMini_sel_internal_call{};
FF avmMini_internal_return_ptr_shift{};
FF avmMini_mem_idx_a{};
FF avmMini_mem_op_a{};
FF avmMini_mem_op_b{};
FF avmMini_sel_jump{};
FF avmMini_op_err{};
FF avmMini_sel_op_add{};
FF avmMini_rwa{};
FF avmMini_rwc{};
FF avmMini_ic{};
FF avmMini_sel_internal_call{};
FF avmMini_rwb{};
FF avmMini_inv{};
FF avmMini_ib{};
FF avmMini_sel_op_sub{};
FF avmMini_sel_op_mul{};
FF avmMini_sel_internal_return{};
FF avmMini_tag_err{};
FF avmMini_sel_jump{};
FF avmMini_mem_op_c{};
FF avmMini_pc_shift{};
FF avmMini_internal_return_ptr_shift{};
FF avmMini_mem_idx_b{};
FF avmMini_sel_halt{};
};

inline std::string get_relation_label_avm_mini(int index)
{
switch (index) {
case 24:
return "RETURN_POINTER_INCREMENT";
case 20:
return "SUBOP_DIVISION_ZERO_ERR1";

case 30:
return "RETURN_POINTER_DECREMENT";
case 21:
return "SUBOP_DIVISION_ZERO_ERR2";

case 36:
return "INTERNAL_RETURN_POINTER_CONSISTENCY";

case 35:
return "PC_INCREMENT";

case 24:
return "RETURN_POINTER_INCREMENT";

case 19:
return "SUBOP_DIVISION_FF";

case 20:
return "SUBOP_DIVISION_ZERO_ERR1";

case 22:
return "SUBOP_ERROR_RELEVANT_OP";

case 36:
return "INTERNAL_RETURN_POINTER_CONSISTENCY";

case 21:
return "SUBOP_DIVISION_ZERO_ERR2";
case 30:
return "RETURN_POINTER_DECREMENT";
}
return std::to_string(index);
}
Expand Down
Loading

0 comments on commit 5d9bda5

Please sign in to comment.