Skip to content
53 changes: 27 additions & 26 deletions barretenberg/cpp/pil/vm2/sha256.pil
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,8 @@ namespace sha256;
// We perform a compression operation if we are not at a latched row, or there is not an err
pol commit perform_round;
perform_round = (1 - LATCH_CONDITION) * SEL_NO_ERR;
pol LAST = SEL_NO_ERR * latch;
pol commit last;
last = SEL_NO_ERR * latch;

// Counter
pol NUM_ROUNDS = 64;
Expand Down Expand Up @@ -494,84 +495,84 @@ namespace sha256;

// TODO: These constraints could be better - we might have to reverse the order of the rounds
pol OUT_A = a + init_a;
LAST * (OUT_A - (output_a_lhs * 2**32 + output_a_rhs)) = 0;
last * (OUT_A - (output_a_lhs * 2**32 + output_a_rhs)) = 0;
pol OUT_B = b + init_b;
LAST * (OUT_B - (output_b_lhs * 2**32 + output_b_rhs)) = 0;
last * (OUT_B - (output_b_lhs * 2**32 + output_b_rhs)) = 0;
pol OUT_C = c + init_c;
LAST * (OUT_C - (output_c_lhs * 2**32 + output_c_rhs)) = 0;
last * (OUT_C - (output_c_lhs * 2**32 + output_c_rhs)) = 0;
pol OUT_D = d + init_d;
LAST * (OUT_D - (output_d_lhs * 2**32 + output_d_rhs)) = 0;
last * (OUT_D - (output_d_lhs * 2**32 + output_d_rhs)) = 0;
pol OUT_E = e + init_e;
LAST * (OUT_E - (output_e_lhs * 2**32 + output_e_rhs)) = 0;
last * (OUT_E - (output_e_lhs * 2**32 + output_e_rhs)) = 0;
pol OUT_F = f + init_f;
LAST * (OUT_F - (output_f_lhs * 2**32 + output_f_rhs)) = 0;
last * (OUT_F - (output_f_lhs * 2**32 + output_f_rhs)) = 0;
pol OUT_G = g + init_g;
LAST * (OUT_G - (output_g_lhs * 2**32 + output_g_rhs)) = 0;
last * (OUT_G - (output_g_lhs * 2**32 + output_g_rhs)) = 0;
pol OUT_H = h + init_h;
LAST * (OUT_H - (output_h_lhs * 2**32 + output_h_rhs)) = 0;
last * (OUT_H - (output_h_lhs * 2**32 + output_h_rhs)) = 0;

// Check Modulo Add Operation
// Check Modulo Add Operation for final outputs
#[RANGE_COMP_A_LHS]
perform_round { two_pow_32, output_a_lhs, /*result = 1*/ perform_round }
last { two_pow_32, output_a_lhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_A_RHS]
perform_round { two_pow_32, output_a_rhs, /*result = 1*/ perform_round }
last { two_pow_32, output_a_rhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_B_LHS]
perform_round { two_pow_32, output_b_lhs, /*result = 1*/ perform_round }
last { two_pow_32, output_b_lhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_B_RHS]
perform_round { two_pow_32, output_b_rhs, /*result = 1*/ perform_round }
last { two_pow_32, output_b_rhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_C_LHS]
perform_round { two_pow_32, output_c_lhs, /*result = 1*/ perform_round }
last { two_pow_32, output_c_lhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_C_RHS]
perform_round { two_pow_32, output_c_rhs, /*result = 1*/ perform_round }
last { two_pow_32, output_c_rhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_D_LHS]
perform_round { two_pow_32, output_d_lhs, /*result = 1*/ perform_round }
last { two_pow_32, output_d_lhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_D_RHS]
perform_round { two_pow_32, output_d_rhs, /*result = 1*/ perform_round }
last { two_pow_32, output_d_rhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_E_LHS]
perform_round { two_pow_32, output_e_lhs, /*result = 1*/ perform_round }
last { two_pow_32, output_e_lhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_E_RHS]
perform_round { two_pow_32, output_e_rhs, /*result = 1*/ perform_round }
last { two_pow_32, output_e_rhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_F_LHS]
perform_round { two_pow_32, output_f_lhs, /*result = 1*/ perform_round }
last { two_pow_32, output_f_lhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_F_RHS]
perform_round { two_pow_32, output_f_rhs, /*result = 1*/ perform_round }
last { two_pow_32, output_f_rhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_G_LHS]
perform_round { two_pow_32, output_g_lhs, /*result = 1*/ perform_round }
last { two_pow_32, output_g_lhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_G_RHS]
perform_round { two_pow_32, output_g_rhs, /*result = 1*/ perform_round }
last { two_pow_32, output_g_rhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_H_LHS]
perform_round { two_pow_32, output_h_lhs, /*result = 1*/ perform_round }
last { two_pow_32, output_h_lhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
#[RANGE_COMP_H_RHS]
perform_round { two_pow_32, output_h_rhs, /*result = 1*/ perform_round }
last { two_pow_32, output_h_rhs, /*result = 1*/ last }
in
gt.sel_sha256 { gt.input_a, gt.input_b, gt.res };
Original file line number Diff line number Diff line change
Expand Up @@ -158,8 +158,9 @@ ResolvedAddress MemoryManager::resolve_address(AddressRef address, uint32_t max_
address.base_offset_seed, address.pointer_address_seed, max_operand_address);
break;
case AddressingMode::Direct:
// Constrain address to fit in the operand (deserialized/mutated data may exceed max)
resolved_address.absolute_address = address.address % (max_operand_address + 1);
// Do not delete this assert, if it fails, it means that some address was generated / mutated incorrectly in
// instruction.cpp. Check all the `max_operand` parameters that you're passing to generate_address_ref.
BB_ASSERT_LTE(address.address, max_operand_address);
resolved_address.operand_address = resolved_address.absolute_address;
break;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1453,8 +1453,8 @@ void ProgramBlock::process_keccakf1600_instruction(KECCAKF1600_Instruction instr
preprocess_memory_addresses(dst.value().first);

auto keccakf1600_instruction = bb::avm2::testing::InstructionBuilder(bb::avm2::WireOpCode::KECCAKF1600)
.operand(src.value().second)
.operand(dst.value().second)
.operand(src.value().second)
.build();
instructions.push_back(keccakf1600_instruction);

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -101,16 +101,6 @@ std::vector<FuzzInstruction> generate_ecadd_instruction(std::mt19937_64& rng)
AddressRef p2_y_addr = generate_address_ref(rng, MAX_16BIT_OPERAND);
AddressRef p2_inf_addr = generate_address_ref(rng, MAX_8BIT_OPERAND);

// Force Direct addressing so SET instructions write to the same addresses that ECADD reads from.
// TODO: Implement smart backfilling for indirect addressing modes by also setting up
// the pointer addresses (e.g., M[pointer_address_seed] = target_address).
p1_x_addr.mode = AddressingMode::Direct;
p1_y_addr.mode = AddressingMode::Direct;
p1_inf_addr.mode = AddressingMode::Direct;
p2_x_addr.mode = AddressingMode::Direct;
p2_y_addr.mode = AddressingMode::Direct;
p2_inf_addr.mode = AddressingMode::Direct;

backfill_point(p1, p1_x_addr, p1_y_addr, p1_inf_addr);
backfill_point(p2, p2_x_addr, p2_y_addr, p2_inf_addr);

Expand All @@ -129,10 +119,11 @@ std::vector<FuzzInstruction> generate_ecadd_instruction(std::mt19937_64& rng)
FuzzInstruction generate_set_for_tag(bb::avm2::MemoryTag tag, AddressRef addr, std::mt19937_64& rng)
{
switch (tag) {
// We use set 16 for u1 and u8 because using set_8 will limit the address range to 255.
case bb::avm2::MemoryTag::U1:
return SET_8_Instruction{ .value_tag = tag, .result_address = addr, .value = static_cast<uint8_t>(rng() & 1) };
return SET_16_Instruction{ .value_tag = tag, .result_address = addr, .value = static_cast<uint8_t>(rng() & 1) };
case bb::avm2::MemoryTag::U8:
return SET_8_Instruction{ .value_tag = tag, .result_address = addr, .value = generate_random_uint8(rng) };
return SET_16_Instruction{ .value_tag = tag, .result_address = addr, .value = generate_random_uint8(rng) };
case bb::avm2::MemoryTag::U16:
return SET_16_Instruction{ .value_tag = tag, .result_address = addr, .value = generate_random_uint16(rng) };
case bb::avm2::MemoryTag::U32:
Expand Down Expand Up @@ -167,12 +158,6 @@ std::vector<FuzzInstruction> generate_alu_with_matching_tags(std::mt19937_64& rn
AddressRef a_addr = generate_address_ref(rng, max_operand);
AddressRef b_addr = generate_address_ref(rng, max_operand);

// Force Direct addressing so SET instructions write to the same addresses that ALU reads from.
// TODO: Implement smart backfilling for indirect addressing modes by also setting up
// the pointer addresses (e.g., M[pointer_address_seed] = target_address).
a_addr.mode = AddressingMode::Direct;
b_addr.mode = AddressingMode::Direct;

std::vector<FuzzInstruction> instructions;
instructions.push_back(generate_set_for_tag(tag, a_addr, rng));
instructions.push_back(generate_set_for_tag(tag, b_addr, rng));
Expand Down Expand Up @@ -205,12 +190,6 @@ std::vector<FuzzInstruction> generate_alu_with_matching_tags_not_ff(std::mt19937
AddressRef a_addr = generate_address_ref(rng, max_operand);
AddressRef b_addr = generate_address_ref(rng, max_operand);

// Force Direct addressing so SET instructions write to the same addresses that ALU reads from.
// TODO: Implement smart backfilling for indirect addressing modes by also setting up
// the pointer addresses (e.g., M[pointer_address_seed] = target_address).
a_addr.mode = AddressingMode::Direct;
b_addr.mode = AddressingMode::Direct;

std::vector<FuzzInstruction> instructions;
instructions.push_back(generate_set_for_tag(tag, a_addr, rng));
instructions.push_back(generate_set_for_tag(tag, b_addr, rng));
Expand Down Expand Up @@ -247,12 +226,6 @@ std::vector<FuzzInstruction> generate_fdiv_instruction(std::mt19937_64& rng, uin
AddressRef a_addr = generate_address_ref(rng, max_operand);
AddressRef b_addr = generate_address_ref(rng, max_operand);

// Force Direct addressing so SET instructions write to the same addresses that FDIV reads from.
// TODO: Implement smart backfilling for indirect addressing modes by also setting up
// the pointer addresses (e.g., M[pointer_address_seed] = target_address).
a_addr.mode = AddressingMode::Direct;
b_addr.mode = AddressingMode::Direct;

// SET the dividend (a)
instructions.push_back(SET_FF_Instruction{
.value_tag = bb::avm2::MemoryTag::FF, .result_address = a_addr, .value = generate_nonzero_field() });
Expand All @@ -279,19 +252,15 @@ std::vector<FuzzInstruction> generate_keccakf_instruction(std::mt19937_64& rng)
}
// Backfill mode
std::vector<FuzzInstruction> instructions;
// Keccak needs to backfill 25 U64 values, these need be contiguous in memory

// Keccak needs to backfill 25 U64 values, these need be contiguous in memory
AddressRef src_address = generate_address_ref(rng, MAX_16BIT_OPERAND - 24);
// Force Direct addressing so SET instructions write to the same addresses that KECCAKF1600 reads from.
// TODO: Implement smart backfilling for indirect addressing modes by also setting up
// the pointer addresses (e.g., M[pointer_address_seed] = target_address).
src_address.mode = AddressingMode::Direct;
for (size_t i = 0; i < 25; i++) {
instructions.push_back(
SET_64_Instruction{ .value_tag = bb::avm2::MemoryTag::U64,
.result_address = AddressRef{ .address = src_address.address + static_cast<uint32_t>(i),
.mode = AddressingMode::Direct },
.value = generate_random_uint64(rng) });
AddressRef item_address = src_address;
item_address.address += static_cast<uint32_t>(i);
instructions.push_back(SET_64_Instruction{ .value_tag = bb::avm2::MemoryTag::U64,
.result_address = item_address,
.value = generate_random_uint64(rng) });
}
instructions.push_back(KECCAKF1600_Instruction{ .src_address = src_address,
.dst_address = generate_address_ref(rng, MAX_16BIT_OPERAND) });
Expand All @@ -315,27 +284,24 @@ std::vector<FuzzInstruction> generate_sha256compression_instruction(std::mt19937

// Generate state address (8 contiguous U32 values)
AddressRef state_address = generate_address_ref(rng, MAX_16BIT_OPERAND - 7);
// Force Direct addressing so SET instructions write to the same addresses that SHA256COMPRESSION reads from.
// TODO: Implement smart backfilling for indirect addressing modes by also setting up
// the pointer addresses (e.g., M[pointer_address_seed] = target_address).
state_address.mode = AddressingMode::Direct;

for (size_t i = 0; i < 8; i++) {
instructions.push_back(SET_32_Instruction{
.value_tag = bb::avm2::MemoryTag::U32,
.result_address = AddressRef{ .address = state_address.address + static_cast<uint32_t>(i),
.mode = AddressingMode::Direct },
.value = generate_random_uint32(rng) });
AddressRef item_address = state_address;
item_address.address += static_cast<uint32_t>(i);
instructions.push_back(SET_32_Instruction{ .value_tag = bb::avm2::MemoryTag::U32,
.result_address = item_address,
.value = generate_random_uint32(rng) });
}

// Generate input address (16 contiguous U32 values)
AddressRef input_address = generate_address_ref(rng, MAX_16BIT_OPERAND - 15);
input_address.mode = AddressingMode::Direct;

for (size_t i = 0; i < 16; i++) {
instructions.push_back(SET_32_Instruction{
.value_tag = bb::avm2::MemoryTag::U32,
.result_address = AddressRef{ .address = input_address.address + static_cast<uint32_t>(i),
.mode = AddressingMode::Direct },
.value = generate_random_uint32(rng) });
AddressRef item_address = input_address;
item_address.address += static_cast<uint32_t>(i);
instructions.push_back(SET_32_Instruction{ .value_tag = bb::avm2::MemoryTag::U32,
.result_address = item_address,
.value = generate_random_uint32(rng) });
}

instructions.push_back(
Expand Down Expand Up @@ -368,36 +334,36 @@ std::vector<FuzzInstruction> generate_toradixbe_instruction(std::mt19937_64& rng
AddressRef num_limbs_addr = generate_address_ref(rng, MAX_16BIT_OPERAND);
AddressRef output_bits_addr = generate_address_ref(rng, MAX_8BIT_OPERAND);

// Force Direct addressing so SET instructions write to the same addresses that TORADIXBE reads from.
// TODO: Implement smart backfilling for indirect addressing modes by also setting up
// the pointer addresses (e.g., M[pointer_address_seed] = target_address).
value_addr.mode = AddressingMode::Direct;
radix_addr.mode = AddressingMode::Direct;
num_limbs_addr.mode = AddressingMode::Direct;
output_bits_addr.mode = AddressingMode::Direct;

// SET the radix (U32) - pick radix between 2 and 256
uint32_t radix = std::uniform_int_distribution<uint32_t>(2, 256)(rng);
instructions.push_back(
SET_32_Instruction{ .value_tag = bb::avm2::MemoryTag::U32, .result_address = radix_addr, .value = radix });

// SET the num_limbs (U32) - reasonable range based on radix
uint32_t num_limbs = std::uniform_int_distribution<uint32_t>(1, 256)(rng);
instructions.push_back(SET_32_Instruction{
.value_tag = bb::avm2::MemoryTag::U32, .result_address = num_limbs_addr, .value = num_limbs });

// SET the output_bits (U1)
bool is_output_bits = radix == 2;
instructions.push_back(SET_8_Instruction{ .value_tag = bb::avm2::MemoryTag::U1,
.result_address = output_bits_addr,
.value = static_cast<uint8_t>(is_output_bits ? 1 : 0) });
// Pick the value such that it fits within the specified number of limbs and radix, if we truncate it will error

// Generate value with num_limbs digits
uint32_t num_limbs = std::uniform_int_distribution<uint32_t>(1, 256)(rng);
bb::avm2::FF value = 0;
bb::avm2::FF exponent = radix;
bb::avm2::FF exponent = 1;
for (uint32_t i = 0; i < num_limbs; i++) {
value += bb::avm2::FF(generate_random_uint32(rng) % radix) * exponent;
uint32_t digit = std::uniform_int_distribution<uint32_t>(0, radix - 1)(rng);
value += bb::avm2::FF(digit) * exponent;
exponent *= radix;
}

// 20% chance to truncate - reduce the number of limbs we request
if (std::uniform_int_distribution<int>(0, 4)(rng) == 0) {
num_limbs--;
}

// SET the num_limbs (U32)
instructions.push_back(SET_32_Instruction{
.value_tag = bb::avm2::MemoryTag::U32, .result_address = num_limbs_addr, .value = num_limbs });

// SET the value (FF)
instructions.push_back(
SET_FF_Instruction{ .value_tag = bb::avm2::MemoryTag::FF, .result_address = value_addr, .value = value });
Expand Down Expand Up @@ -432,9 +398,6 @@ std::vector<FuzzInstruction> generate_sload_instruction(std::mt19937_64& rng)
instructions.reserve(3);

AddressRef sstore_src = generate_address_ref(rng, MAX_16BIT_OPERAND);
// Force Direct addressing so SET writes to the same address that SSTORE reads from.
// TODO: Implement smart backfilling for indirect addressing modes.
sstore_src.mode = AddressingMode::Direct;

// SET a value to store
instructions.push_back(SET_FF_Instruction{
Expand Down
Loading
Loading