Skip to content
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.

word hi/lo utilities (initial version) #1394

Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
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
2 changes: 1 addition & 1 deletion keccak256/src/gate_helpers.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use eth_types::Field;
use num_bigint::BigUint;

/// Convert a bigUint value to FieldExt
/// Convert a bigUint value to Field
///
/// We assume the input value is smaller than the field size
pub fn biguint_to_f<F: Field>(x: &BigUint) -> F {
Expand Down
2 changes: 1 addition & 1 deletion zkevm-circuits/src/evm_circuit/execution.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1398,7 +1398,7 @@ impl<F: Field> ExecutionConfig<F> {
// plus the number of rw lookups done by the copy circuit.
if step.rw_indices.len() != assigned_rw_values.len() + step.copy_rw_counter_delta as usize {
log::error!(
"step.rw_indices.len: {} != assigned_rw_values.len: {} + step.copy_rw_counter_delta: {} in step: {:?}",
"step.rw_indices.len: {} != assigned_rw_values.len: {} + step.copy_rw_counter_delta: {} in step: {:?}",
step.rw_indices.len(),
assigned_rw_values.len(),
step.copy_rw_counter_delta,
Expand Down
20 changes: 12 additions & 8 deletions zkevm-circuits/src/evm_circuit/execution/add_sub.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,14 @@ use crate::{
common_gadget::SameContextGadget,
constraint_builder::{EVMConstraintBuilder, StepStateTransition, Transition::Delta},
math_gadget::{AddWordsGadget, PairSelectGadget},
select, CachedRegion,
CachedRegion,
},
witness::{Block, Call, ExecStep, Transaction},
},
util::Expr,
util::{
word::{Word, WordExpr},
Expr,
},
};
use bus_mapping::evm::OpcodeId;
use eth_types::Field;
Expand All @@ -35,9 +38,9 @@ impl<F: Field> ExecutionGadget<F> for AddSubGadget<F> {
fn configure(cb: &mut EVMConstraintBuilder<F>) -> Self {
let opcode = cb.query_cell();

let a = cb.query_word_rlc();
let b = cb.query_word_rlc();
let c = cb.query_word_rlc();
let a = cb.query_word32();
let b = cb.query_word32();
let c = cb.query_word32();
let add_words = AddWordsGadget::construct(cb, [a.clone(), b.clone()], c.clone());

// Swap a and c if opcode is SUB
Expand All @@ -50,9 +53,10 @@ impl<F: Field> ExecutionGadget<F> for AddSubGadget<F> {

// ADD: Pop a and b from the stack, push c on the stack
// SUB: Pop c and b from the stack, push a on the stack
cb.stack_pop(select::expr(is_sub.expr().0, c.expr(), a.expr()));
cb.stack_pop(b.expr());
cb.stack_push(select::expr(is_sub.expr().0, a.expr(), c.expr()));

cb.stack_pop(Word::select(is_sub.expr().0, c.to_word(), a.to_word()));
cb.stack_pop(b.to_word());
cb.stack_push(Word::select(is_sub.expr().0, a.to_word(), c.to_word()));

// State transition
let step_state_transition = StepStateTransition {
Expand Down
74 changes: 39 additions & 35 deletions zkevm-circuits/src/evm_circuit/execution/addmod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,42 +9,45 @@ use crate::{
Transition::Delta,
},
math_gadget::{
AddWordsGadget, CmpWordsGadget, IsZeroGadget, MulAddWords512Gadget,
AddWordsGadget, CmpWordsGadget, IsZeroWordGadget, MulAddWords512Gadget,
MulAddWordsGadget,
},
not, CachedRegion, Word,
not, CachedRegion,
},
witness::{Block, Call, ExecStep, Transaction},
},
util::Expr,
util::{
word::{Word, Word32Cell, WordExpr},
Expr,
},
};

use bus_mapping::evm::OpcodeId;
use eth_types::{Field, ToLittleEndian, U256, U512};
use halo2_proofs::plonk::Error;
use halo2_proofs::{circuit::Value, plonk::Error};

#[derive(Clone, Debug)]
pub(crate) struct AddModGadget<F> {
same_context: SameContextGadget<F>,

a: Word<F>,
b: Word<F>,
r: Word<F>,
n: Word<F>,
a: Word32Cell<F>,
b: Word32Cell<F>,
r: Word32Cell<F>,
n: Word32Cell<F>,

k: Word<F>,
d: Word<F>,
a_reduced: Word<F>,
k: Word32Cell<F>,
d: Word32Cell<F>,
a_reduced: Word32Cell<F>,

muladd_k_n_areduced: MulAddWordsGadget<F>,

sum_areduced_b: AddWordsGadget<F, 2, false>,
sum_areduced_b_overflow: Word<F>,
sum_areduced_b_overflow: Word32Cell<F>,
muladd_d_n_r: MulAddWords512Gadget<F>,

n_is_zero: IsZeroGadget<F>,
cmp_r_n: CmpWordsGadget<F>,
cmp_areduced_n: CmpWordsGadget<F>,
n_is_zero: IsZeroWordGadget<F>,
cmp_r_n: CmpWordsGadget<F, Word32Cell<F>, Word32Cell<F>>,
cmp_areduced_n: CmpWordsGadget<F, Word32Cell<F>, Word32Cell<F>>,
}

impl<F: Field> ExecutionGadget<F> for AddModGadget<F> {
Expand All @@ -56,17 +59,17 @@ impl<F: Field> ExecutionGadget<F> for AddModGadget<F> {
let opcode = cb.query_cell();

// values got from stack (original r is modified if n==0)
let a = cb.query_word_rlc();
let b = cb.query_word_rlc();
let n = cb.query_word_rlc();
let r = cb.query_word_rlc();
let a = cb.query_word32();
let b = cb.query_word32();
let n = cb.query_word32();
let r = cb.query_word32();

// auxiliar witness
let k = cb.query_word_rlc();
let a_reduced = cb.query_word_rlc();
let d = cb.query_word_rlc();
let k = cb.query_word32();
let a_reduced = cb.query_word32();
let d = cb.query_word32();

let n_is_zero = IsZeroGadget::construct(cb, n.clone().expr());
let n_is_zero = IsZeroWordGadget::construct(cb, n);

// 1. check k * N + a_reduced == a without overflow
let muladd_k_n_areduced = MulAddWordsGadget::construct(cb, [&k, &n, &a_reduced, &a]);
Expand All @@ -77,24 +80,25 @@ impl<F: Field> ExecutionGadget<F> for AddModGadget<F> {

// 2. check d * N + r == a_reduced + b, only checking carry if n != 0
let sum_areduced_b = {
let sum = cb.query_word_rlc();
let sum = cb.query_word32();
AddWordsGadget::construct(cb, [a_reduced.clone(), b.clone()], sum)
};
let sum_areduced_b_overflow = cb.query_word_rlc();
let sum_areduced_b_overflow = cb.query_word32();
let muladd_d_n_r = MulAddWords512Gadget::construct(
cb,
[&d, &n, &sum_areduced_b_overflow, sum_areduced_b.sum()],
Some(&r),
);

cb.require_equal(
cb.require_equal_word(
"check a_reduced + b 512 bit carry if n != 0",
sum_areduced_b_overflow.expr(),
sum_areduced_b.carry().clone().unwrap().expr() * not::expr(n_is_zero.expr()),
sum_areduced_b_overflow.to_word(),
Word::from_lo_unchecked(sum_areduced_b.carry())
.mul_selector(not::expr(n_is_zero.expr())),
);

let cmp_r_n = CmpWordsGadget::construct(cb, &r, &n);
let cmp_areduced_n = CmpWordsGadget::construct(cb, &a_reduced, &n);
let cmp_r_n = CmpWordsGadget::construct(cb, r, n);
let cmp_areduced_n = CmpWordsGadget::construct(cb, a_reduced, n);
hero78119 marked this conversation as resolved.
Show resolved Hide resolved

// 3. r < n and a_reduced < n if n > 0
cb.require_zero(
Expand All @@ -104,10 +108,10 @@ impl<F: Field> ExecutionGadget<F> for AddModGadget<F> {

// pop/push values
// take care that if n==0 pushed value for r should be zero also
cb.stack_pop(a.expr());
cb.stack_pop(b.expr());
cb.stack_pop(n.expr());
cb.stack_push(r.expr() * not::expr(n_is_zero.expr()));
cb.stack_pop(a.to_word());
cb.stack_pop(b.to_word());
cb.stack_pop(n.to_word());
cb.stack_push(r.to_word().mul_selector(not::expr(n_is_zero.expr())));

// State transition
let step_state_transition = StepStateTransition {
Expand Down Expand Up @@ -217,7 +221,7 @@ impl<F: Field> ExecutionGadget<F> for AddModGadget<F> {
self.cmp_areduced_n.assign(region, offset, a_reduced, n)?;

self.n_is_zero
.assign_value(region, offset, region.word_rlc(n))?;
.assign_value(region, offset, Value::known(Word::from_u256(n)))?;

Ok(())
}
Expand Down
30 changes: 8 additions & 22 deletions zkevm-circuits/src/evm_circuit/execution/address.rs
Original file line number Diff line number Diff line change
@@ -1,27 +1,25 @@
use crate::{
evm_circuit::{
execution::ExecutionGadget,
param::N_BYTES_ACCOUNT_ADDRESS,
step::ExecutionState,
util::{
common_gadget::SameContextGadget,
constraint_builder::{EVMConstraintBuilder, StepStateTransition, Transition::Delta},
from_bytes, CachedRegion, RandomLinearCombination,
AccountAddress, CachedRegion,
},
witness::{Block, Call, ExecStep, Transaction},
},
table::CallContextFieldTag,
util::Expr,
util::{word::WordExpr, Expr},
};
use bus_mapping::evm::OpcodeId;
use eth_types::{Field, ToAddress, ToLittleEndian};
use halo2_proofs::plonk::Error;
use std::convert::TryInto;

#[derive(Clone, Debug)]
pub(crate) struct AddressGadget<F> {
same_context: SameContextGadget<F>,
address: RandomLinearCombination<F, N_BYTES_ACCOUNT_ADDRESS>,
address: AccountAddress<F>,
}

impl<F: Field> ExecutionGadget<F> for AddressGadget<F> {
Expand All @@ -30,17 +28,12 @@ impl<F: Field> ExecutionGadget<F> for AddressGadget<F> {
const EXECUTION_STATE: ExecutionState = ExecutionState::ADDRESS;

fn configure(cb: &mut EVMConstraintBuilder<F>) -> Self {
let address = cb.query_word_rlc();
let address = cb.query_account_address();

// Lookup callee address in call context.
cb.call_context_lookup(
false.expr(),
None,
CallContextFieldTag::CalleeAddress,
from_bytes::expr(&address.cells),
);
cb.call_context_lookup_read(None, CallContextFieldTag::CalleeAddress, address.to_word());

cb.stack_push(address.expr());
cb.stack_push(address.to_word());

let step_state_transition = StepStateTransition {
rw_counter: Delta(2.expr()),
Expand Down Expand Up @@ -73,15 +66,8 @@ impl<F: Field> ExecutionGadget<F> for AddressGadget<F> {
let address = block.rws[step.rw_indices[1]].stack_value();
debug_assert_eq!(call.address, address.to_address());

self.address.assign(
region,
offset,
Some(
address.to_le_bytes()[..N_BYTES_ACCOUNT_ADDRESS]
.try_into()
.unwrap(),
),
)?;
self.address
.assign(region, offset, Some(address.to_le_bytes()))?;

Ok(())
}
Expand Down
40 changes: 22 additions & 18 deletions zkevm-circuits/src/evm_circuit/execution/balance.rs
Original file line number Diff line number Diff line change
@@ -1,34 +1,35 @@
use crate::{
evm_circuit::{
execution::ExecutionGadget,
param::N_BYTES_ACCOUNT_ADDRESS,
step::ExecutionState,
util::{
common_gadget::SameContextGadget,
constraint_builder::{
ConstrainBuilderCommon, EVMConstraintBuilder, ReversionInfo, StepStateTransition,
Transition::Delta,
},
from_bytes,
math_gadget::IsZeroGadget,
not, select, CachedRegion, Cell, Word,
math_gadget::{IsZeroGadget, IsZeroWordGadget},
not, select, AccountAddress, CachedRegion, Cell,
},
witness::{Block, Call, ExecStep, Transaction},
},
table::{AccountFieldTag, CallContextFieldTag},
util::Expr,
util::{
word::{Word32Cell, WordExpr},
Expr,
},
};
use eth_types::{evm_types::GasCost, Field, ToLittleEndian};
use halo2_proofs::{circuit::Value, plonk::Error};

#[derive(Clone, Debug)]
pub(crate) struct BalanceGadget<F> {
same_context: SameContextGadget<F>,
address_word: Word<F>,
address: AccountAddress<F>,
reversion_info: ReversionInfo<F>,
tx_id: Cell<F>,
is_warm: Cell<F>,
code_hash: Cell<F>,
code_hash: Word32Cell<F>,
not_exists: IsZeroGadget<F>,
balance: Cell<F>,
}
Expand All @@ -39,9 +40,8 @@ impl<F: Field> ExecutionGadget<F> for BalanceGadget<F> {
const EXECUTION_STATE: ExecutionState = ExecutionState::BALANCE;

fn configure(cb: &mut EVMConstraintBuilder<F>) -> Self {
let address_word = cb.query_word_rlc();
let address = from_bytes::expr(&address_word.cells[..N_BYTES_ACCOUNT_ADDRESS]);
cb.stack_pop(address_word.expr());
let address = cb.query_account_address();
cb.stack_pop(address.to_word());

let tx_id = cb.call_context(None, CallContextFieldTag::TxId);
let mut reversion_info = cb.reversion_info_read(None);
Expand All @@ -53,20 +53,24 @@ impl<F: Field> ExecutionGadget<F> for BalanceGadget<F> {
is_warm.expr(),
Some(&mut reversion_info),
);
let code_hash = cb.query_cell_phase2();
let code_hash = cb.query_word32();
// For non-existing accounts the code_hash must be 0 in the rw_table.
cb.account_read(address.expr(), AccountFieldTag::CodeHash, code_hash.expr());
let not_exists = IsZeroGadget::construct(cb, code_hash.expr());
cb.account_read(
address.expr(),
AccountFieldTag::CodeHash,
code_hash.to_word(),
);
let not_exists = IsZeroWordGadget::construct(cb, code_hash.to_word());
let exists = not::expr(not_exists.expr());
let balance = cb.query_cell_phase2();
let balance = cb.query_word32();
cb.condition(exists.expr(), |cb| {
cb.account_read(address.expr(), AccountFieldTag::Balance, balance.expr());
cb.account_read(address.expr(), AccountFieldTag::Balance, balance.to_word());
});
cb.condition(not_exists.expr(), |cb| {
cb.require_zero("balance is zero when non_exists", balance.expr());
cb.require_zero_word("balance is zero when non_exists", balance.to_word());
});

cb.stack_push(balance.expr());
cb.stack_push(balance.to_word());

let gas_cost = select::expr(
is_warm.expr(),
Expand All @@ -88,7 +92,7 @@ impl<F: Field> ExecutionGadget<F> for BalanceGadget<F> {

Self {
same_context,
address_word,
address,
reversion_info,
tx_id,
is_warm,
Expand Down
Loading