owned this note
owned this note
Published
Linked with GitHub
## Question 1. (RLP Circuit) ["Importance": Low - FOR DISCUSSION]
Indeed, the invalid RLP handling is not currently being done in the circuits. There are also some TODOs in the docs.
Are there plans to implement this? We're wondering if we should venture into the possibility of whether missing these checks lead to security vulnerability - but if there's already plans to implement them then it may become a waste of time (to figure out a reason for a check to be added when there are already plans for such checks to be added anyway)
## Question 2. (RLP Circuit) ["Importance": Low - OK]
This is more of a completeness question. On the documentation, it says that the check for the (tx_id, format) is that either tx_id' = tx_id + 1 or (tx_id' = tx_id and format' >= format + 1) unless the adjacent tuple is equal. However in the circuits, the check is that in the case of tx_id' = tx_id, then format' = format or format' = format + 1.
Which is the intended one? This could have some consequences depending on how the witnesses are generated. If there’s one tx with format 1 and one tx with format 3, how does the current witness generation work? If it’s handled as (tx_id, format) = (1, 1), (2, 3) then there isn’t an issue, but if it’s handled as (tx_id, format) = (1, 1), (1, 3) then we have a completeness issue, as this doesn't satisfy the circuits.
We do expect that this is for the TxSign and the TxHash instances, so probably not an issue.
## Finding 3. (RLP Circuit) ["Importance": High - FIXED]
In the data table checks,
```
- (tx_id' == tx_id, format' != format) or (tx_id' != tx_id, tx_id' != 0)
- byte_rev_idx = 1
- byte_idx' = 1
- bytes_rlc' = byte_value'
```
It seems that this allows the very last non-padding instance's final row to have `byte_rev_idx != 1`?
## Finding 4. (RLP Circuit) ["Importance": High - FIXED]
It seems like the byte value checks are being only done on the padding txs. Is this intended?
```rust
meta.lookup_any("byte value check", |meta| {
let cond = and::expr([
meta.query_fixed(q_enabled, Rotation::cur()),
is_padding_in_dt.expr(Rotation::cur())(meta),
]);
vec![meta.query_advice(data_table.byte_value, Rotation::cur())]
.into_iter()
.zip(range256_table.table_exprs(meta).into_iter())
.map(|(arg, table)| (cond.expr() * arg, table))
.collect()
});
```
## Finding 5. (RLP Circuit) ["Importance": Medium - FIXED]
Continuing the discussion on range checks, there seems to be no check on tag_length <= max_length, is this ok?
## Finding 6 (RLP Circuit) ["Importance": High - FIXED]
Continuing the discussion on range checks, are the assumptions for ComparatorChip checked anywhere?
the diff on the ComparatorChip must be checked to be a byte.
the LHS and the RHS should be within a range (this shouldn't be an issue if question 4, 5 are resolved)
## Finding 7. (RLP Circuit) ["Importance": High - FIXED]
in the state machine init, shouldn't we force the initial state to be DecodeTagStart?
Also, one of the scenarios to consider here is, what if we start on tag = BeginList even though the specs say that we should start on TxType - what would happen?
## Question 8. (RLP Circuit) ["Importance": Low - OK]
This one I’m not so sure about, and I think this isn’t that relevant, but
in the case `((0xc0 <= byte_value < 0xf8) && (is_tag_end == false))`
if `byte_value = 0xc0`, should `is_none = true`?
## Question 9. (RLP Circuit) ["Importance": Medium - FOR DISCUSSION]
Is the current RLP circuit implementation the version with the full EIP1559 support with the non-trivial access lists? (so we have to look deeper into depth >= 2 cases) One thing I noticed is that the tx circuit seems to only deal with eip155, pre-eip155, and l1msg, so was a bit confused there as well. Also was wondering if TxType is validated against the format somewhere?
## Finding 10. (RLP Circuit) ["Importance": High - FIXED]
in the transit_to_new_rlp_instance case, it constrains `tx_id' = tx_id + 1` or `format' = format + 1`
-> what if the next instance is something like ``(tx_id - 1, format + 1)`` or something like that?
also, there's the check
```rust
cb.require_zero(
"tag == TxType or tag == BeginList",
(tag_next.expr() - TxType.expr())
* (tag_next.expr() - BeginList.expr()),
);
```
this actually means that there are no checks against tag', as the checks are done against the column tag_next. is this ok?
## Finding 11. (RLP Circuit) ["Importance": High - FIXED]
It's clear that `0x00` and `0x0000` have the same RLC value - to differ them we also need the length value.
it seems that RlpFsmRlpTable doesn't have tag_length at all, so wondering if the distinguishing is currently done on some other way, or if it's just not needed at all.
## Finding 12. (Common Gadgets) ["Importance": High]
Some quick notes.
```rust
impl<F: Field, const N_BYTES: usize> ComparatorConfig<F, N_BYTES> {
/// Returns (lt, eq) for a comparison between lhs and rhs.
pub fn expr(
&self,
meta: &mut VirtualCells<F>,
rotation: Option<Rotation>,
) -> (Expression<F>, Expression<F>) {
(
self.lt_chip.config.is_lt(meta, rotation),
self.eq_chip.config.is_equal_expression.clone(),
)
}
}
```
The IsEqual part doesn't handle the rotation correctly, but I haven't seen a case where non-trivial rotation is used.
Also, the assign logic in the LtChip depends on the fact that to_repr of the PrimeField is little-endian, but it is stated that "Generic encodings of field elements should be treated as opaque."
## Finding 13. (RLP Circuit) ["Importance": High - FIXED]
In `Bytes => DecodeTagStart` case and `tag_index = tag_length`, there's no check `tag_value = tag_value_acc`
```rust=
// Bytes => DecodeTagStart
cb.condition(tidx_eq_tlen, |cb| {
// assertions
emit_rlp_tag!(meta, cb, tag_expr(meta), false);
// state transitions.
update_state!(meta, cb, tag, tag_next_expr(meta));
update_state!(meta, cb, state, State::DecodeTagStart);
constrain_unchanged_fields!(meta, cb; rlp_table.tx_id, rlp_table.format, depth);
});
```
## Finding 14 (RLP Circuit) ["Importance": High - FIXED]
shouldn't there be a do_not_emit for `DecodeTagStart => LongList`?
If so, we'll check further for more such cases.
UPD: there were no more cases of this type
## Question 15. (TX Circuit) ["Importance": Medium - OK]
It seems that the circuit layout in https://docs.google.com/spreadsheets/d/1CHKL7_7f954J29AoV67KTnjtFdXxtvvIWv3oaCW4YmU/edit#gid=0 is a bit outdated - could you update this to the current version? It's kinda confusing when auditing 😦
## Question 16. (PI Circuit) [Invalid]
It seems that the correct rpi_rlc_acc accumulation for the last 32 rows (where the keccak results is handled) is important - as this is then constrained to be equal to the keccak row's output
```rust
region.constrain_equal(
keccak_output_cell.cell(),
cells[RPI_RLC_ACC_CELL_IDX].cell(),
)?;
```
however, I actually don't see `q_not_end` being turned on for these rows, so there's no constraints on the `rlp_rlc_acc` that are actually applied. (It's only turned on the rows before the keccak row)
## Finding 17. (RLP Circuit) ["Importance": Medium - FIXED]
What happens if not all transactions in the data table are in the state machine? For example, what if we just start the state machine with the transaction id 3?
Also, should we constrain that the final state is `End`? If not, maybe we could mess with the final transaction, not moving to the `End` state even until the very end.
## Question 18. (RLP Circuit) ["Importance": Low - OK]
```rust
let padding_txs = (block.txs.len()..max_txs)
.into_iter()
.map(|i| {
let mut tx = Transaction::dummy(block.chain_id);
tx.id = i + 1;
tx
})
.collect::<Vec<Transaction>>();
let txs = [block.txs.clone(), padding_txs].concat();
```
Shouldn't the tx ids for the padding txs be `0`?
## Finding 19. (Tx Circuit) ["Importance": Low - FIXED]
```rust
let rlp_tag_map: Vec<(Expression<F>, RlpTag)> = vec![
(is_nonce(meta), Tag::Nonce.into()),
(is_gas_price(meta), Tag::GasPrice.into()),
(is_gas(meta), Tag::Gas.into()),
(is_to(meta), Tag::To.into()),
(is_value(meta), Tag::Value.into()),
(is_data_rlc(meta), Tag::Data.into()),
(is_sig_v(meta), Tag::SigV.into()),
(is_sig_r(meta), Tag::SigR.into()),
(is_sig_s(meta), Tag::SigS.into()),
(is_sign_length(meta), Len),
(is_sign_rlc(meta), RLC),
(is_hash_length(meta), Len),
(is_hash_rlc(meta), RLC),
(is_caller_addr(meta), Tag::Sender.into()),
// tx tags which correspond to Null
(is_null(meta), Null),
(is_create(meta), Null),
(is_data_length(meta), Null),
(is_data_gas_cost(meta), Null),
(is_sign_hash(meta), Null),
(is_hash(meta), Null),
(is_data(meta), Null),
(is_tx_gas_cost(meta), Null),
(is_block_num(meta), Null),
(is_chain_id_expr(meta), Null),
```
Is `is_chain_id_expr` not mapped to `Tag::ChainId`?
## Question 20. (Tx Circuit) [Invalid]
Is the `format` in the `RlpFsmRlpTable` validated against the `tx_type` in the tx circuit?
^ Yes.
## Finding 21. (Tx Circuit) ["Importance": Low - FIXED]
```rust
[
Value::known(F::from(self.id as u64)),
Value::known(F::from(TxContextFieldTag::Gas as u64)), // 4
Value::known(F::zero()),
Value::known(F::from(self.gas)),
],
[
Value::known(F::from(self.id as u64)),
Value::known(F::from(TxContextFieldTag::GasPrice as u64)), // 3
Value::known(F::zero()),
challenges
.evm_word()
.map(|challenge| rlc::value(&self.gas_price.to_le_bytes(), challenge)),
],
```
In the fixed assignment part, Gas (4) comes before GasPrice (3). I think letting Gas equal 3 and GasPrice equal 4 in the enum is cleaner, unless there is some other reason?
```rust
// the offset between CallerAddress and BlockNumber
let offset = usize::from(BlockNumber) - usize::from(CallerAddress);
```
There's logic like this, where the enum value is directly used for offset calculation, so keeping consistency sounds like a good idea.
## Finding 22. (Tx Circuit) ["Importance": High - FIXED]
In the calldata part
```rust
meta.create_gate("tx call data bytes", |meta| {
let mut cb = BaseConstraintBuilder::default();
let is_final_cur = meta.query_advice(is_final, Rotation::cur());
cb.require_boolean("is_final is boolean", is_final_cur.clone());
// checks for any row, except the final call data byte.
cb.condition(not::expr(is_final_cur.clone()), |cb| {
cb.require_equal(
"index::next == index::cur + 1",
meta.query_advice(tx_table.index, Rotation::next()),
meta.query_advice(tx_table.index, Rotation::cur()) + 1.expr(),
);
cb.require_equal(
"tx_id::next == tx_id::cur",
tx_id_unchanged.is_equal_expression.clone(),
1.expr(),
);
let value_next_is_zero = value_is_zero.expr(Rotation::next())(meta);
let gas_cost_next = select::expr(value_next_is_zero, 4.expr(), 16.expr());
// call data gas cost accumulator check.
cb.require_equal(
"calldata_gas_cost_acc::next == calldata_gas_cost::cur + gas_cost_next",
meta.query_advice(calldata_gas_cost_acc, Rotation::next()),
meta.query_advice(calldata_gas_cost_acc, Rotation::cur()) + gas_cost_next,
);
});
// on the final call data byte, tx_id must change.
cb.condition(is_final_cur, |cb| {
cb.require_zero(
"tx_id changes at is_final == 1",
tx_id_unchanged.is_equal_expression.clone(),
);
});
cb.gate(and::expr(vec![
meta.query_fixed(q_enable, Rotation::cur()),
meta.query_advice(is_calldata, Rotation::cur()),
not::expr(tx_id_is_zero.expr(Rotation::cur())(meta)),
]))
});
```
Where is the constrain that
- the first row (either the very first row or the first row of a new tx id) has `index = 0`
- the first row has `calldata_gas_cost_acc = value == 0 ? 4 : 16`
## Finding 23. (Tx Circuit) ["Importance": High - FIXED]
The constraints on the `sv_address` is weak.
```rust
meta.create_gate(
"caller address == sv_address if it's not zero and tx_type != L1Msg",
|meta| {
let mut cb = BaseConstraintBuilder::default();
cb.condition(not::expr(value_is_zero.expr(Rotation::cur())(meta)), |cb| {
cb.require_equal(
"caller address == sv_address",
meta.query_advice(tx_table.value, Rotation::cur()),
meta.query_advice(sv_address, Rotation::cur()),
);
});
cb.gate(and::expr([
meta.query_fixed(q_enable, Rotation::cur()),
meta.query_advice(is_caller_address, Rotation::cur()),
not::expr(meta.query_advice(is_l1_msg, Rotation::cur())),
]))
},
);
```
Here, the `sv_address` value at the offset of `CallerAddress` is checked against the `value` (caller address value) itself.
```rust
meta.lookup_any("Sig table lookup", |meta| {
let enabled = and::expr([
// use is_l1_msg_col instead of is_l1_msg(meta) because it has lower degree
not::expr(meta.query_advice(is_l1_msg_col, Rotation::cur())),
// lookup to sig table on the ChainID row because we have an indicator of degree 1
// for ChainID and ChainID is not far from (msg_hash_rlc, sig_v,
// ...)
meta.query_advice(is_chain_id, Rotation::cur()),
]);
let msg_hash_rlc = meta.query_advice(tx_table.value, Rotation(6));
let chain_id = meta.query_advice(tx_table.value, Rotation::cur());
let sig_v = meta.query_advice(tx_table.value, Rotation(1));
let sig_r = meta.query_advice(tx_table.value, Rotation(2));
let sig_s = meta.query_advice(tx_table.value, Rotation(3));
let sv_address = meta.query_advice(sv_address, Rotation::cur());
let v = is_eip155(meta) * (sig_v.expr() - 2.expr() * chain_id - 35.expr())
+ is_pre_eip155(meta) * (sig_v.expr() - 27.expr());
let input_exprs = vec![
1.expr(), // q_enable = true
msg_hash_rlc, // msg_hash_rlc
v, // sig_v
sig_r, // sig_r
sig_s, // sig_s
sv_address,
1.expr(), // is_valid
];
// LookupTable::table_exprs is not used here since `is_valid` not used by evm circuit.
let table_exprs = vec![
meta.query_fixed(sig_table.q_enable, Rotation::cur()),
// msg_hash_rlc not needed to be looked up for tx circuit?
meta.query_advice(sig_table.msg_hash_rlc, Rotation::cur()),
meta.query_advice(sig_table.sig_v, Rotation::cur()),
meta.query_advice(sig_table.sig_r_rlc, Rotation::cur()),
meta.query_advice(sig_table.sig_s_rlc, Rotation::cur()),
meta.query_advice(sig_table.recovered_addr, Rotation::cur()),
meta.query_advice(sig_table.is_valid, Rotation::cur()),
];
input_exprs
.into_iter()
.zip(table_exprs.into_iter())
.map(|(input, table)| (input * enabled.expr(), table))
.collect()
});
```
Here, the `sv_address` checked is at the `ChainId` offset - and there is no check that `sv_address` at this offset is equal to the one at the `CallerAddress` offset. This needs to be checked (by forcing `sv_address` to be equal for a single tx id) or the rotation/offset handling must be more precise.
## Finding 24. (Tx Circuit) ["Importance": High - FIXED]
```rust
/// Tx id must be no greater than cum_num_txs
tx_id_cmp_cum_num_txs: ComparatorConfig<F, 2>,
```
For a safe usage
- constrain that `tx_id, cum_num_txs` are within 16 bits
- constrain that the `diff` value inside the `LtChip` is a byte
## Finding 25. (Tx Circuit) ["Importance": High - FIXED]
First, the first tx_id in the first part of the tx circuit should be constrained to be 1.
```rust
meta.create_gate("tx_id transition", |meta| {
let mut cb = BaseConstraintBuilder::default();
// if tag_next == Nonce, then tx_id' = tx_id + 1
cb.condition(tag_bits.value_equals(Nonce, Rotation::next())(meta), |cb| {
cb.require_equal(
"tx_id increments",
meta.query_advice(tx_table.tx_id, Rotation::next()),
meta.query_advice(tx_table.tx_id, Rotation::cur()) + 1.expr(),
);
});
// if tag_next != Nonce, then tx_id' = tx_id, tx_type' = tx_type
cb.condition(
not::expr(tag_bits.value_equals(Nonce, Rotation::next())(meta)),
|cb| {
cb.require_equal(
"tx_id does not change",
meta.query_advice(tx_table.tx_id, Rotation::next()),
meta.query_advice(tx_table.tx_id, Rotation::cur()),
);
cb.require_equal(
"tx_type does not change",
meta.query_advice(tx_type, Rotation::next()),
meta.query_advice(tx_type, Rotation::cur()),
);
},
);
cb.gate(and::expr([
meta.query_fixed(q_enable, Rotation::cur()),
not::expr(meta.query_advice(is_calldata, Rotation::next())),
]))
});
```
## Question 26. (Tx Circuit) ["Importance": High - FIXED but need to check more (leads to another finding?) - FIXED AGAIN]
You can put arbitrary calldata in the calldata part, especially for transactions with `calldatalength = 0`. This is because the lookups aren't actually being done in this case.
Overall, the constraints on the calldata part of the tx circuit layout is weak. We are also worried about the `CallDataRLC` as well - while this value (in the first part of the tx circuit layout) is validated against the RLP table, it's never validated against the actual calldata in the second part of the tx circuit.
This means that we can actually put arbitrary values in the calldata section of the tx circuit (with the same number of nonzero/zero bytes, of course).
## Question 27. (Pi Circuit) [Invalid]
Where is `rpi = rpi_bytes_acc` when it's the end of the field? The constraints on `rpi_bytes_acc` itself is quite weak as well, with `rpi_bytes_acc = rpi_bytes` for the first byte of the field element missing as well.
These checks were implemented in commit hash 79caaf4339ab033eea33e4df4b997f5e3d3f1a32, why were they removed?
`rpi_rlc_acc[0] = rpi_bytes[0]` is also removed as well.
## Question 28. (Tx Circuit) ["Importance": Low - FIXED]
Just a few weird/maybe incorrect comments in the code:
```rust
// This does not seem related to eip2718 ?
//#[cfg(feature = "reject-eip2718")]
meta.create_gate(
"caller address == sv_address if it's not zero and tx_type != L1Msg",
// Maybe an outdated comment, because this function loads the u16 range check lookup table now.
/// Load ECDSA RangeChip table.
pub fn load_aux_tables(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
layouter.assign_table(
// I'm not sure what this comment is referring to? Is this a old column
1063: .zip(rlp_table.table_exprs(meta).into_iter()) // tag_length_eq_one is the 6th column in rlp table
```
Some small code quality suggestions:
```rust
cb.require_equal(
"is_calldata",
// why is this not re-using is_data?
tag_bits.value_equals(CallData, Rotation::cur())(meta),
meta.query_advice(is_calldata, Rotation::cur()),
);
cb.require_equal(
"is_caller_address",
// why is this not re-using is_caller_addr?
tag_bits.value_equals(CallerAddress, Rotation::cur())(meta),
meta.query_advice(is_caller_address, Rotation::cur()),
);
cb.require_equal(
"is_chain_id",
// why is this not re-using is_chain_id_expr?
tag_bits.value_equals(ChainID, Rotation::cur())(meta),
meta.query_advice(is_chain_id, Rotation::cur()),
);
```
## Finding 29. (Pi Circuit) ["Importance": High - FIXED]
```rust
for (row, tag) in block_ctx
.table_assignments(num_txs, cum_num_txs, challenges)
.into_iter()
.zip(tag.iter())
{
region.assign_fixed(
|| format!("block table row {offset}"),
self.block_table.tag,
offset,
|| row[0],
)?;
// index_cells of same block are equal to block_number.
let mut index_cells = vec![];
let mut block_number_cell = None;
for (column, value) in block_table_columns.iter().zip_eq(&row[1..]) {
let cell = region.assign_advice(
|| format!("block table row {offset}"),
*column,
offset,
|| *value,
)?;
if *tag == Number && *column == self.block_table.value {
block_number_cell = Some(cell.clone());
}
if *column == self.block_table.index {
index_cells.push(cell.clone());
}
if *column == self.block_table.value {
block_value_cells.push(cell);
}
}
for i in 0..(index_cells.len() - 1) {
region.constrain_equal(index_cells[i].cell(), index_cells[i + 1].cell())?;
}
if *tag == Number {
region.constrain_equal(
block_number_cell.unwrap().cell(),
index_cells[0].cell(),
)?;
}
```
what we need to constrain is that each index cells for the entire context (timestamp, numtx, chainid, basefee, etc) is equal, and that is also equal to the value cell for the number tag.
so to collect the necessary cells, shouldn't the `index_cell` be declared outside of this for loop?
the for loop iterates over the rows on a single block context
right now it's doing `let mut index_cells` for literally every row
## Finding 30. (Tx Circuits) ["Importance": Medium - FIXED]
where exactly is the block table's `num_txs` verified?
to be exact - currently the tx number related constraints we are aware of is
- `cum_num_txs = sum of num_txs` (Pi Circuits)
- `cum_num_txs` in tx circuits match the ones in the block table (lookup argument in Tx circuits)
- `tx_id <= cum_num_txs` (in Tx circuits)
so there aren't actually checks that say `num_txs = [number of transactions with block number = given value]` - in fact we believe that large `num_txs` value is ok (under the range that ComparatorChip allows)
I guess a better way to state question 30 is that where is the condition that `tx_id = cum_num_txs` in the very last tx_id for a certain block number?
## Finding 31. (MPT Circuits) ["Importance": High - FIXED]
In `one-hot.rs`, there is a critical typo.
```rust
pub fn previous<F: FieldExt>(&self) -> Query<F> {
T::iter().enumerate().fold(Query::zero(), |acc, (i, t)| {
acc.clone()
+ Query::from(u64::try_from(i).unwrap())
* self
.columns
.get(&t)
.map_or_else(BinaryQuery::zero, BinaryColumn::current)
})
}
```
It seems that `previous()` uses `BinaryColumn::current`, which is incorrect.
## Finding 32 (MPT Circuits) ["Importance": High - FIXED]
In `binary_column.rs`, the binary column is configured without any constraint.
```rust
pub fn configure<F: FieldExt>(
cs: &mut ConstraintSystem<F>,
_cb: &mut ConstraintBuilder<F>,
) -> Self {
let advice_column = cs.advice_column();
// TODO: constrain to be binary here...
// cb.add_constraint()
Self(advice_column)
}
```
We suggest to add the boolean constraint here, as suggested by the `TODO`.
## Finding 33. (MPT Circuits) ["Importance" : Low - FIXED]
In the `byte_representation.rs`, the comments for some constraints are incorrect.
```rust
cb.assert_equal(
"current value = previous value * 256 * (index == 0) + byte",
value.current(),
value.previous() * 256 * !index_is_zero.current() + byte.current(),
);
cb.assert_equal(
"current rlc = previous rlc * randomness * (index == 0) + byte",
rlc.current(),
rlc.previous() * randomness.query() * !index_is_zero.current() + byte.current(),
);
```
The explanation should be `"current value = previous value * 256 * (index != 0) + byte"` - similar for rlc.
## Finding 34. (MPT Circuits) ["Importance": Low - FIXED]
The main question here is if this code is used anywhere, or if it is being planned to use in the future. If not, is it okay to just delete it?
In `account.rs`, we believe the codes below are typos, and would like to verify.
```rust
impl AccountProof {
pub fn old_root(&self) -> Fr {
self.trie_rows
.old_root(|| self.old_leaf.hash(self.storage.new_root()))
// old_root, but uses new_root to hash
}
pub fn new_root(&self) -> Fr {
self.trie_rows
.new_root(|| self.new_leaf.hash(self.storage.old_root()))
// new_root, but uses old_root to hash
}
}
```
There is also a typo in implementing `From<&SMTTrace>` for `AccountProof`. This implementation is actually never used - so maybe even deleting this would be beneficial for the codebase.
```rust
impl From<&SMTTrace> for AccountProof {
fn from(trace: &SMTTrace) -> Self {
let address = Address::from(trace.address.0);
let [old_path, new_path] = &trace.account_path;
let old_leaf = old_path.leaf;
let new_leaf = new_path.leaf;
let trie_rows = TrieRows::new(
account_key(address),
&new_path.path, // here - might be old_path.path
&new_path.path,
old_path.leaf,
new_path.leaf,
);
```
## Question 35 (MPT Circuits) ["Importance": Medium - FIXED]
In `ByteRepresentation` gadget, there is a check to ensure that index is always increasing:
```rust
cb.assert_zero(
"index increases by 1 or resets to 0",
index.current() * (index.current() - index.previous() - 1),
);
```
What is the value of `index.previous()` at offset 0 in Halo2? Is there some unintended behaviour here? If so, there should be a check using a `is_first` selector.
## Question 36 (MPT Circuits) ["Importance": Medium - OK]
In `types.rs`, where we convert SMTTrace to a Proof, there is the following code:
```rust
if let Some(update) = state_update {
match update {
[None, None] => (),
[Some(old), Some(new)] => {
// The account must exist, because only contracts with bytecode can modify their own storage slots.
if !(account_old == account_new
|| (account_old.is_none() && account_new == &Some(Default::default())))
{
assert_eq!(account_old, account_new, "{:?}", state_update);
}
let old_value = u256_from_hex(old.value);
let new_value = u256_from_hex(new.value);
```
We were wondering if this assumption is correct because one can write to storage slots while in the constructor, and at this point the account has no bytecode.
Response fom Mason:
> The general idea is correct: the state circuit (aka rw circuit) re-orders mpt updates such that for a given address, account nonce, balance, code hash, etc. updates come before any storage updates. This means that the mpt circuit only needs to handle storage updates for accounts that already exist. I can make this more clear in the comment.
## Question 37 (MPT Circuits) ["Importance": Low]
In `types.rs`, it is mentioned that selfdestruct and account destruction are not supported:
```rust
MPTProofType::AccountDestructed => unimplemented!(),
},
[Some(_old), None] => unimplemented!("SELFDESTRUCT"),
```
But there seem to be many places in the `MptUpdate` circuit where these kind of functionality are implemented. For example:
* When we transition from Common to ExtensionOld at AccountLeaf0, this means that the account is being destructed.
* When we have path type ExtensionOld and proof type CodeSizeExists:
```rust
cb.condition(
config.path_type.current_matches(&[PathType::ExtensionOld]),
|cb| {
cb.add_lookup(
"old code size is 8 bytes",
[config.old_value.current(), Query::from(7)],
bytes.lookup(),
);
cb.assert_zero(
"old nonce is 0 for ExtensionOld code size update",
old_nonce,
);
},
);
```
What situation is this triggered in?
Continuing in this manner - there are a lot of cases where the path type is assumed to be either `Start` or `Common`, but afterwards there are constraints conditioned on the case where the path type is either `ExtensionOld` or `ExtensionNew`. For example, in `configure_code_size` -
```rust
fn configure_code_size<F: FieldExt>(
cb: &mut ConstraintBuilder<F>,
config: &MptUpdateConfig,
bytes: &impl BytesLookup,
) {
cb.assert(
"new accounts have balance or nonce set first",
config
.path_type
.current_matches(&[PathType::Start, PathType::Common]),
); // *must* be start or common!
for variant in SegmentType::iter() {
let conditional_constraints = |cb: &mut ConstraintBuilder<F>| match variant {
// ...
SegmentType::AccountLeaf3 => {
cb.assert_zero("direction is 0", config.direction.current());
// ...
cb.condition(
config.path_type.current_matches(&[PathType::ExtensionNew]),
// no reason for this, right?
|cb| {
cb.add_lookup(
"new nonce is 8 bytes",
[config.old_value.current(), Query::from(7)],
bytes.lookup(),
);
// ...
},
);
cb.condition(
config.path_type.current_matches(&[PathType::ExtensionOld]),
// no reason for this right?
|cb| {
cb.add_lookup(
"old code size is 8 bytes",
[config.old_value.current(), Query::from(7)],
bytes.lookup(),
);
// ...
},
);
}
_ => {}
};
cb.condition(
config.segment_type.current_matches(&[variant]),
conditional_constraints,
);
}
}
```
This is apparent in many codes - `configure_poseidon_code_hash` also has similar issues, matching `ExtensionOld` and `ExtensionNew` as well.
## Finding 38. (MPT Circuits) ["Importance": High - NEEDS FIX]
Assuming that `address` is already range checked externally to be within `20` bytes,
```rust
cb.condition(is_start.clone().and(cb.every_row_selector()), |cb| {
let [address, address_high, ..] = intermediate_values;
let [old_hash_rlc, new_hash_rlc, ..] = second_phase_intermediate_values;
let address_low: Query<F> = (address.current() - address_high.current() * (1 << 32))
* (1 << 32)
* (1 << 32)
* (1 << 32);
cb.poseidon_lookup(
"account mpt key = h(address_high, address_low)",
[address_high.current(), address_low, key.current()],
poseidon,
);
cb.add_lookup(
"rlc_old_root = rlc(old_root)",
[old_hash.current(), old_hash_rlc.current(), Query::from(31)],
fr_rlc.lookup(),
);
cb.add_lookup(
"rlc_new_root = rlc(new_root)",
[new_hash.current(), new_hash_rlc.current(), Query::from(31)],
fr_rlc.lookup(),
);
})
```
Here it should be checked that `address - address_high * 2^{32}` is within 4 bytes and `address_high` is within 16 bytes. Without this range check, there can be multiple possible values for `(address_low, address_high)`, so there can be multiple account keys for a single address.
## Question 39. (MPT Circuits) ["Importance": Low - FIXED]
In `types.rs` at `check()` - shouldn't these index be `[6][2]`?
```rust
assert_eq!(
hash(
hash(Fr::one(), self.leafs[0].unwrap().key),
self.leafs[0].unwrap().value_hash
),
self.old_account_hash_traces[5][2], // [6][2]
);
assert_eq!(
hash(
hash(Fr::one(), self.leafs[1].unwrap().key),
self.leafs[1].unwrap().value_hash
),
self.new_account_hash_traces[5][2], // [6][2]
);
```
## "Finding" 40. (MPT Circuits) ["Importance": High - FIXED]
In `configure_extension_old` and `configure_extension_new`, where is the check that `other_key_hash = hash(1, other_key)`?
```rust
let [.., other_key_hash, other_leaf_data_hash] = config.intermediate_values;
cb.condition(new_is_type_1, |cb| {
cb.poseidon_lookup(
"previous old_hash = h(other_key_hash, other_leaf_data_hash)",
[
other_key_hash.current(), // constraint on this?
other_leaf_data_hash.current(),
config.new_hash.previous(),
],
poseidon,
);
});
```
We do expect that this constraint will be mostly used on empty account / empty storage proofs, where there *is* a check that `other_key_hash = hash(1, other_key)`. Nonetheless, we believe that adding this check will be better for clarity and want to know Scroll's opinion.
## Finding 41. (MPT Circiuts) ["Importance": Low - FIXED]
We see that both `byte_representation.rs` and `canonical_representation.rs` implement `RlcLookup`. However, these two are very different - for example the `value` in the `byte_representation.rs` is the value of the accumulated bytes so far, but in the `canonical_representation.rs` it is the value of the entire field element.
This makes implementations like `word_rlc.rs`'s `configure` quite confusing - here, `rlc` must be from `byte_representation.rs` for this to work. The code does indeed use the `RlcLookup` from `byte_representation.rs`, but we believe that this is an awkward implementation and should be refactored.
```rust
pub fn configure<F: FieldExt>(
cb: &mut ConstraintBuilder<F>,
[word_hash, high, low]: [AdviceColumn; 3],
[rlc_word, rlc_high, rlc_low]: [SecondPhaseAdviceColumn; 3],
poseidon: &impl PoseidonLookup,
bytes: &impl BytesLookup,
rlc: &impl RlcLookup, // must be from byte_representation
randomness: Query<F>,
) {
cb.add_lookup(
"old_high is 16 bytes",
[high.current(), Query::from(15)],
bytes.lookup(),
);
cb.add_lookup(
"old_low is 16 bytes",
[low.current(), Query::from(15)],
bytes.lookup(),
);
cb.poseidon_lookup(
"word_hash = poseidon(high, low)",
[high.current(), low.current(), word_hash.current()],
poseidon,
);
cb.add_lookup(
"rlc_high = rlc(high) and high is 16 bytes",
[high.current(), Query::from(15), rlc_high.current()],
rlc.lookup(),
);
cb.add_lookup(
"rlc_low = rlc(low) and low is 16 bytes",
[low.current(), Query::from(15), rlc_low.current()],
rlc.lookup(),
);
let randomness_raised_to_16 = randomness.clone().square().square().square().square();
cb.assert_equal(
"word_rlc = rlc(high) * randomness ^ 16 + rlc(low)",
rlc_word.current(),
rlc_high.current() * randomness_raised_to_16.clone() + rlc_low.current(),
);
}
```
## Finding 42 (MPT Circuits) ["Importance": High - FIXED]
For `configure_balance`, if we are at `AccountLeaf3` with `ExtensionNew`, there must be a constraint that the `sibling = 0`. (i.e. `nonce = code_size = 0`)
This is currently missing: could cause soundness issues when we send ETH to a new address.
## Finding 43 (MPT Circuits) ["Importance": High - FIXED]
For `configure_empty_storage`, it seems that the check `old_hash == new_hash` is missing. (For reference, this is explicitly checked in `configure_empty_account`)
We also note that the "final segment" checks are being done with `config.segment_type.next_matches(&[SegmentType::Start]);` - this means that we should strictly enforce padding rows at the end, so that the final row has `SegmentType::Start`. This part is similar to the second part (about final state = `End`) of Question 17 above.
## Finding 44 (MPT Circuits) ["Importance": High - FIXED]
We note some things about `configure_nonce`.
- [1]: There is a typo `old_value` when it should be `new_value` to range check the new nonce.
- [2]: The `new_value` (not `old_value`) should be checked in the case of `ExtensionNew` path type.
- [3]: The `ExtensionOld` path type cannot happen in the `configure_nonce` case.
```rust
SegmentType::AccountLeaf3 => {
cb.assert_zero("direction is 0", config.direction.current());
let old_code_size = (config.old_hash.current() - config.old_value.current())
* Query::Constant(F::from(1 << 32).square().invert().unwrap());
let new_code_size = (config.new_hash.current() - config.new_value.current())
* Query::Constant(F::from(1 << 32).square().invert().unwrap());
cb.condition(
config.path_type.current_matches(&[PathType::Common]),
|cb| {
cb.add_lookup(
"old nonce is 8 bytes",
[config.old_value.current(), Query::from(7)],
bytes.lookup(),
);
cb.add_lookup(
"new nonce is 8 bytes",
[config.old_value.current(), Query::from(7)], // [1]: typo - should be new_value
bytes.lookup(),
);
cb.assert_equal(
"old_code_size = new_code_size for nonce update",
old_code_size.clone(),
new_code_size.clone(),
);
cb.add_lookup(
"existing code size is 8 bytes",
[old_code_size.clone(), Query::from(7)],
bytes.lookup(),
);
},
);
cb.condition(
config.path_type.current_matches(&[PathType::ExtensionNew]),
|cb| {
cb.add_lookup(
"new nonce is 8 bytes",
[config.old_value.current(), Query::from(7)], // [2]: typo - should be new_value
bytes.lookup(),
);
cb.assert_zero(
"code size is 0 for ExtensionNew nonce update",
new_code_size,
);
cb.assert_zero(
"balance is 0 for ExtensionNew nonce update",
config.sibling.current(),
);
},
);
cb.condition(
config.path_type.current_matches(&[PathType::ExtensionOld]), // [3]: is this case even reachable? wouldn't the proof type be StorageChanged anyway if the path type is ExtensionOld?
|cb| {
cb.add_lookup(
"old nonce is 8 bytes",
[config.old_value.current(), Query::from(7)],
bytes.lookup(),
);
cb.assert_zero(
"code size is 0 for ExtensionOld nonce update",
old_code_size,
);
},
);
```
## Question 45 (MPT Circuits) ["Importance": High]
We note some things about `configure_code_size`
The first point is that these code are unreachable as there is already an assertion that the path type matches either `Start` or `Common`.
Meanwhile, we note that ([1]) the `sibling = 0` check in the `ExtensionNew` case does not check that `nonce` and `code_size` are zero as the name of the constraint suggests - it checks that the `balance` is zero.
```rust
cb.condition(
config.path_type.current_matches(&[PathType::ExtensionNew]), // no reason for this, right?
|cb| {
cb.add_lookup(
"new nonce is 8 bytes",
[config.old_value.current(), Query::from(7)],
bytes.lookup(),
);
cb.assert_zero(
"new nonce is 0 for ExtensionNew code size update",
new_nonce,
);
cb.assert_zero(
"nonce and code size are 0 for ExtensionNew balance update",
config.sibling.current(), // [1]
);
},
);
cb.condition(
config.path_type.current_matches(&[PathType::ExtensionOld]), // no reason for this right?
|cb| {
cb.add_lookup(
"old code size is 8 bytes",
[config.old_value.current(), Query::from(7)],
bytes.lookup(),
);
cb.assert_zero(
"old nonce is 0 for ExtensionOld code size update",
old_nonce,
);
},
```
## Question 46 (MPT Circuit) ["Importance": Low - FIXED]
There is a minor typo at `mpt_update.rs`.
```rust
cb.condition(!is_start, |cb| {
cb.assert_equal(
"proof type does not change",
proof_type.current(),
proof_type.previous(),
);
cb.assert_equal(
"storage_key_rlc does not change",
storage_key_rlc.current(),
storage_key_rlc.previous(),
);
cb.assert_equal(
"old_value does not change",
old_value.current(),
old_value.previous(),
);
cb.assert_equal(
"old_value does not change", // typo here
new_value.current(),
new_value.previous(),
);
});
```
Google Drive
Gist
Clipboard
Sign in with Wallet
