Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(3738): AVM basic arithmetic operations for non ff types #3881

Merged
merged 40 commits into from
Jan 23, 2024
Merged
Changes from 1 commit
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
8ff7315
PIL relations for u8, u16, u32, u64, u128 additions
jeanmon Dec 20, 2023
0258f34
PIL relations for subtraction of u8, u16, u32, u64, 128 types
jeanmon Dec 21, 2023
8594bfc
3738 - explanations on arithmetic operations PIL relations
jeanmon Jan 2, 2024
d3f0a13
3738 - additions and subtractions re-visited with 16-bit registers
jeanmon Jan 2, 2024
09a4490
Merge branch 'avm-main' into jm/3738-u32-arithmetic
jeanmon Jan 3, 2024
2300f96
3738 - pil relations for multiplication types u8, u16, u32, u64
jeanmon Jan 3, 2024
87b873b
3738 - pil relations for u128 multiplication
jeanmon Jan 3, 2024
f74ca13
Merge branch 'avm-main' into jm/3738-arithmetic-non-ff
jeanmon Jan 5, 2024
55fab70
3738 - First version of Alu trace files
jeanmon Jan 5, 2024
650eec3
3738 - witness generation for addition
jeanmon Jan 8, 2024
31ff1a7
Merge branch 'master' into jm/3738-arithmetic-non-ff
jeanmon Jan 8, 2024
7a64651
Merge branch 'master' into jm/3738-arithmetic-non-ff
jeanmon Jan 8, 2024
115a40a
3738 - create common header file for tests
jeanmon Jan 9, 2024
b9d878f
3738 - rename arithmetic test suite specific for FF
jeanmon Jan 9, 2024
ee53436
3738 - move FF addition to alu chip and create a unit test for u8
jeanmon Jan 9, 2024
95e9e9f
3738 - first unit tests for u8
jeanmon Jan 9, 2024
d365314
3738 - positive unit tests for addition
jeanmon Jan 10, 2024
a93c9b4
3738 - witness generation for subtraction and move ff pil relation to
jeanmon Jan 10, 2024
74e8714
3738 - add unit tests for subtraction and swap u128 addition unit tests
jeanmon Jan 11, 2024
8e4f299
3738 - add witness generation for multiplication with types u8, u16,
jeanmon Jan 11, 2024
0a65b54
3738 - add positive unit tests for addition with type u8, u16, u32, u64
jeanmon Jan 11, 2024
fab58b9
3738 - witness generation for addition over u128
jeanmon Jan 11, 2024
1536b28
3738: style improvement and comments
jeanmon Jan 12, 2024
5d9bda5
3738 - bugfixing PIL relation for u128 multiplication and unit tests
jeanmon Jan 12, 2024
c13c702
Merge branch 'master' into jm/3738-arithmetic-non-ff
jeanmon Jan 12, 2024
ecacbbc
Merge branch 'master' into jm/3738-arithmetic-non-ff
jeanmon Jan 12, 2024
5e7570e
Merge branch 'master' into jm/3738-arithmetic-non-ff
jeanmon Jan 15, 2024
5ab8ffc
3738 - add basic negative unit tests for each operation and type
jeanmon Jan 15, 2024
394d18c
3738 - rewrite addition and subtraction relations according to Zac's
jeanmon Jan 17, 2024
b2ed4f3
3738 - further PIL relation consolidation for add/sub
jeanmon Jan 17, 2024
41391f6
3738 - consolidate multiplication relations for u8, u16, u32, u64
jeanmon Jan 18, 2024
3feb72e
3738 - comparator for memory traces migrated as < operator overload
jeanmon Jan 18, 2024
10eebde
3738 - adding some TODO in comments
jeanmon Jan 18, 2024
7ce1cf6
Merge branch 'master' into jm/3738-arithmetic-non-ff
jeanmon Jan 18, 2024
ce60c4a
Merge branch 'master' into jm/3738-arithmetic-non-ff
jeanmon Jan 19, 2024
23e2dcd
3738 - Re-generate AVM related files with new namespace (after master
jeanmon Jan 19, 2024
2fecc75
Merge branch 'master' into testing-merge-arith
jeanmon Jan 22, 2024
b0d262d
3738 - capitalize enum values
jeanmon Jan 22, 2024
78457db
Merge branch 'master' into jm/3738-arithmetic-non-ff
jeanmon Jan 23, 2024
14f794c
Merge branch 'master' into jm/3738-arithmetic-non-ff
jeanmon Jan 23, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
3738 - first unit tests for u8
jeanmon committed Jan 9, 2024
commit 95e9e9f428b9054d2f29cbc3320b25e6c1f6d919
Original file line number Diff line number Diff line change
@@ -227,6 +227,37 @@ void AvmMiniTraceBuilder::div(uint32_t a_offset, uint32_t b_offset, uint32_t dst
});
}

// TODO: Finish SET opcode implementation. This is a partial implementation
// facilitating testing of arithmetic operations over non finite field types.
// We add an entry in the memory trace and a simplified one in the main trace
// without operation selector.
// No check is performed that val pertains to type defined by in_tag.
/**
* @brief Set a constant from bytecode with direct memory access.
*
* @param val The constant to be written upcasted to u128
* @param dst_offset Memory destination offset where val is written to
* @param in_tag The instruction memory tag
*/
void AvmMiniTraceBuilder::set(uint128_t val, uint32_t dst_offset, AvmMemoryTag in_tag)
{
auto clk = static_cast<uint32_t>(main_trace.size());
auto val_ff = FF{ uint256_t::from_uint128(val) };

mem_trace_builder.write_into_memory(clk, IntermRegister::ic, dst_offset, val_ff, in_tag);

main_trace.push_back(Row{
.avmMini_clk = clk,
.avmMini_pc = FF(pc++),
.avmMini_internal_return_ptr = FF(internal_return_ptr),
.avmMini_in_tag = FF(static_cast<uint32_t>(in_tag)),
.avmMini_ic = val_ff,
.avmMini_mem_op_c = FF(1),
.avmMini_rwc = FF(1),
.avmMini_mem_idx_c = FF(dst_offset),
});
}

/**
* @brief CALLDATACOPY opcode with direct memory access, i.e.,
* M[dst_offset:dst_offset+copy_size] = calldata[cd_offset:cd_offset+copy_size]
Original file line number Diff line number Diff line change
@@ -37,6 +37,9 @@ class AvmMiniTraceBuilder {
// Division with direct memory access.
void div(uint32_t a_offset, uint32_t b_offset, uint32_t dst_offset, AvmMemoryTag in_tag);

// Set a constant from bytecode with direct memory access.
void set(uint128_t val, uint32_t dst_offset, AvmMemoryTag in_tag);
jeanmon marked this conversation as resolved.
Show resolved Hide resolved

// Jump to a given program counter.
void jump(uint32_t jmp_dest);

Original file line number Diff line number Diff line change
@@ -1,5 +1,55 @@
#include "AvmMini_common.test.hpp"

namespace {

Row common_validate_add(std::vector<Row> const& trace,
FF const& a,
FF const& b,
FF const& c,
FF const& addr_a,
FF const& addr_b,
FF const& addr_c,
avm_trace::AvmMemoryTag const tag)
{
// Find the first row enabling the addition selector
auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_add == FF(1); });

// Check that the correct result is stored at the expected memory location.
EXPECT_TRUE(row != trace.end());
EXPECT_EQ(row->avmMini_ic, c);
EXPECT_EQ(row->avmMini_mem_idx_c, addr_c);
EXPECT_EQ(row->avmMini_mem_op_c, FF(1));
EXPECT_EQ(row->avmMini_rwc, FF(1));

// Check that ia and ib registers are correctly set with memory load operations.
EXPECT_EQ(row->avmMini_ia, a);
EXPECT_EQ(row->avmMini_mem_idx_a, addr_a);
EXPECT_EQ(row->avmMini_mem_op_a, FF(1));
EXPECT_EQ(row->avmMini_rwa, FF(0));
EXPECT_EQ(row->avmMini_ib, b);
EXPECT_EQ(row->avmMini_mem_idx_b, addr_b);
EXPECT_EQ(row->avmMini_mem_op_b, FF(1));
EXPECT_EQ(row->avmMini_rwb, FF(0));

// Check instruction tag and add selector are set.
EXPECT_EQ(row->avmMini_in_tag, FF(static_cast<uint32_t>(tag)));
EXPECT_EQ(row->avmMini_sel_op_add, FF(1));

// Check that Alu trace is as expected.
auto clk = row->avmMini_clk;
auto alu_row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { return r.aluChip_alu_clk == clk; });

EXPECT_TRUE(alu_row != trace.end());
EXPECT_EQ(alu_row->aluChip_alu_op_add, FF(1));
EXPECT_EQ(alu_row->aluChip_alu_ia, a);
EXPECT_EQ(alu_row->aluChip_alu_ib, b);
EXPECT_EQ(alu_row->aluChip_alu_ic, c);

return *alu_row;
}

} // anonymous namespace

namespace tests_avm {
using namespace avm_trace;

@@ -59,15 +109,9 @@ TEST_F(AvmMiniArithmeticTestsFF, addition)
trace_builder.return_op(0, 5);
auto trace = trace_builder.finalize();

// Find the first row enabling the addition selector
auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_add == FF(1); });
auto alu_row = common_validate_add(trace, FF(37), FF(4), FF(41), FF(0), FF(1), FF(4), AvmMemoryTag::ff);

// Check that the correct result is stored at the expected memory location.
EXPECT_TRUE(row != trace.end());
EXPECT_EQ(row->avmMini_ic, FF(41));
EXPECT_EQ(row->avmMini_mem_idx_c, FF(4));
EXPECT_EQ(row->avmMini_mem_op_c, FF(1));
EXPECT_EQ(row->avmMini_rwc, FF(1));
EXPECT_EQ(alu_row.aluChip_alu_ff_tag, FF(1));

validate_trace_proof(std::move(trace));
jeanmon marked this conversation as resolved.
Show resolved Hide resolved
}
@@ -268,20 +312,40 @@ TEST_F(AvmMiniArithmeticTestsFF, mixedOperationsWithError)
TEST_F(AvmMiniArithmeticTestsU8, addition)
{
// trace_builder
trace_builder.call_data_copy(0, 2, 0, std::vector<FF>{ 62, 29 });
trace_builder.set(62, 0, AvmMemoryTag::u8);
trace_builder.set(29, 1, AvmMemoryTag::u8);

// Memory layout: [62,29,0,0,0,....]
trace_builder.add(0, 1, 2, AvmMemoryTag::u8); // [62,29,91,0,0,....]
trace_builder.return_op(2, 1);
auto trace = trace_builder.finalize();

// Find the first row enabling the addition selector
auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avmMini_sel_op_add == FF(1); });
auto alu_row = common_validate_add(trace, FF(62), FF(29), FF(91), FF(0), FF(1), FF(2), AvmMemoryTag::u8);

// Check that the correct result is computed.
EXPECT_TRUE(row != trace.end());
EXPECT_EQ(row->avmMini_ic, FF(91));
// EXPECT_EQ(row->aluChip_alu_u8_tag, FF(1));
EXPECT_EQ(alu_row.aluChip_alu_u8_tag, FF(1));
EXPECT_EQ(alu_row.aluChip_alu_cf, FF(0));
EXPECT_EQ(alu_row.aluChip_alu_u8_r0, FF(91));

validate_trace_proof(std::move(trace));
}

// Test on basic addition over u8 type with carry.
TEST_F(AvmMiniArithmeticTestsU8, additionCarry)
{
// trace_builder
trace_builder.set(159, 0, AvmMemoryTag::u8);
trace_builder.set(100, 1, AvmMemoryTag::u8);

// Memory layout: [159,100,0,0,0,....]
trace_builder.add(0, 1, 2, AvmMemoryTag::u8); // [159,100,3,0,0,....]
trace_builder.return_op(2, 1);
auto trace = trace_builder.finalize();

auto alu_row = common_validate_add(trace, FF(159), FF(100), FF(3), FF(0), FF(1), FF(2), AvmMemoryTag::u8);

EXPECT_EQ(alu_row.aluChip_alu_u8_tag, FF(1));
EXPECT_EQ(alu_row.aluChip_alu_cf, FF(1));
EXPECT_EQ(alu_row.aluChip_alu_u8_r0, FF(3));

validate_trace_proof(std::move(trace));
}