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

Fix soundness bug in aggregator pi datahash #691

Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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 aggregator/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ snark-verifier-sdk = { git = "https://github.com/scroll-tech/snark-verifier", br


[features]
default = [ ]
default = [ ]
print-trace = [ "ark-std/print-trace" ]
# This feature is useful for unit tests where we check the SAT of pi aggregation circuit
disable_proof_aggregation = []
2 changes: 1 addition & 1 deletion aggregator/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ for i in 1 ... n:
chunk_i.data_hash == [0u8; 32]
```
7. chunk[i]'s data_hash len is `0` when chunk[i] is padded

8. batch data hash is correct w.r.t. its RLCs

### Handling dynamic inputs

Expand Down
15 changes: 15 additions & 0 deletions aggregator/src/aggregation/rlc/gates.rs
Original file line number Diff line number Diff line change
Expand Up @@ -288,6 +288,21 @@ impl RlcConfig {
self.mul_add(region, b, &cond_not, &tmp, offset)
}

// if cond = 1, enforce a==b
// caller need to ensure cond is binary
pub(crate) fn conditional_enforce_equal(
&self,
region: &mut Region<Fr>,
a: &AssignedCell<Fr, Fr>,
b: &AssignedCell<Fr, Fr>,
cond: &AssignedCell<Fr, Fr>,
offset: &mut usize,
) -> Result<(), Error> {
let diff = self.sub(region, a, b, offset)?;
let res = self.mul(region, &diff, cond, offset)?;
self.enforce_zero(region, &res)
}

// Returns inputs[0] + challenge * inputs[1] + ... + challenge^k * inputs[k]
#[allow(dead_code)]
pub(crate) fn rlc(
Expand Down
141 changes: 82 additions & 59 deletions aggregator/src/core.rs
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,7 @@ pub(crate) fn extract_accumulators_and_proof(
// 5. batch and all its chunks use a same chain id
// 6. chunk[i]'s prev_state_root == post_state_root when chunk[i] is padded
// 7. chunk[i]'s data_hash == "" when chunk[i] is padded
// 8. batch data hash is correct w.r.t. its RLCs
#[allow(clippy::type_complexity)]
pub(crate) fn assign_batch_hashes(
config: &AggregationConfig,
Expand Down Expand Up @@ -128,6 +129,7 @@ pub(crate) fn assign_batch_hashes(
// padded
// 6. chunk[i]'s prev_state_root == post_state_root when chunk[i] is padded
// 7. chunk[i]'s data_hash == "" when chunk[i] is padded
// 8. batch data hash is correct w.r.t. its RLCs
let num_valid_snarks = conditional_constraints(
&config.rlc_config,
// config.flex_gate(),
Expand Down Expand Up @@ -406,6 +408,7 @@ fn copy_constraints(
// 3. batch_data_hash and chunk[i].pi_hash use a same chunk[i].data_hash when chunk[i] is not padded
// 6. chunk[i]'s prev_state_root == post_state_root when chunk[i] is padded
// 7. chunk[i]'s data_hash == "" when chunk[i] is padded
// 8. batch data hash is correct w.r.t. its RLCs
#[allow(clippy::too_many_arguments)]
pub(crate) fn conditional_constraints(
rlc_config: &RlcConfig,
Expand Down Expand Up @@ -578,65 +581,22 @@ pub(crate) fn conditional_constraints(
// chunk[i].postStateRoot ||
// chunk[i].withdrawRoot ||
// chunk[i].datahash)
let challenge_cell =
rlc_config.read_challenge(&mut region, challenges, &mut offset)?;

let flags = chunk_is_valid_cells
.iter()
.flat_map(|cell| vec![cell; 32])
.cloned()
.collect::<Vec<_>>();

let rlc_cell = rlc_config.rlc_with_flag(
&mut region,
potential_batch_data_hash_preimage[..DIGEST_LEN * MAX_AGG_SNARKS].as_ref(),
&challenge_cell,
&flags,
&mut offset,
)?;

assert_exist(
&rlc_cell,
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 3],
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 4],
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 5],
);
log::trace!("rlc from chip {:?}", rlc_cell.value());
log::trace!(
"rlc from table {:?}",
data_rlc_cells[MAX_AGG_SNARKS * 2 + 3].value()
);
log::trace!(
"rlc from table {:?}",
data_rlc_cells[MAX_AGG_SNARKS * 2 + 4].value()
);
log::trace!(
"rlc from table {:?}",
data_rlc_cells[MAX_AGG_SNARKS * 2 + 5].value()
);

// assertion
let t1 = rlc_config.sub(
&mut region,
&rlc_cell,
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 3],
&mut offset,
)?;
let t2 = rlc_config.sub(
&mut region,
&rlc_cell,
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 4],
&mut offset,
)?;
let t3 = rlc_config.sub(
&mut region,
&rlc_cell,
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 5],
&mut offset,
)?;
let t1t2 = rlc_config.mul(&mut region, &t1, &t2, &mut offset)?;
let t1t2t3 = rlc_config.mul(&mut region, &t1t2, &t3, &mut offset)?;
rlc_config.enforce_zero(&mut region, &t1t2t3)?;
for i in 0..MAX_AGG_SNARKS {
for j in 0..DIGEST_LEN {
assert_conditional_equal(
&chunk_pi_hash_preimages[i][j + CHUNK_DATA_HASH_INDEX],
&potential_batch_data_hash_preimage[i * DIGEST_LEN + j],
&chunk_is_valid_cells[i],
);
rlc_config.conditional_enforce_equal(
&mut region,
&chunk_pi_hash_preimages[i][j + CHUNK_DATA_HASH_INDEX],
&potential_batch_data_hash_preimage[i * DIGEST_LEN + j],
&chunk_is_valid_cells[i],
&mut offset,
)?;
}
}

// 6. chunk[i]'s prev_state_root == post_state_root when chunk[i] is padded
for (i, chunk_hash_input) in chunk_pi_hash_preimages.iter().enumerate() {
Expand Down Expand Up @@ -716,6 +676,69 @@ pub(crate) fn conditional_constraints(
// sanity check
assert_equal(&data_hash_inputs, &data_hash_inputs_rec);
region.constrain_equal(data_hash_inputs.cell(), data_hash_inputs_rec.cell())?;

// 8. batch data hash is correct w.r.t. its RLCs
// batchDataHash = keccak(chunk[0].dataHash || ... || chunk[k-1].dataHash)
let challenge_cell =
rlc_config.read_challenge(&mut region, challenges, &mut offset)?;

let flags = chunk_is_valid_cells
.iter()
.flat_map(|cell| vec![cell; 32])
.cloned()
.collect::<Vec<_>>();

let rlc_cell = rlc_config.rlc_with_flag(
&mut region,
potential_batch_data_hash_preimage[..DIGEST_LEN * MAX_AGG_SNARKS].as_ref(),
&challenge_cell,
&flags,
&mut offset,
)?;

assert_exist(
&rlc_cell,
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 3],
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 4],
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 5],
);
log::trace!("rlc from chip {:?}", rlc_cell.value());
log::trace!(
"rlc from table {:?}",
data_rlc_cells[MAX_AGG_SNARKS * 2 + 3].value()
);
log::trace!(
"rlc from table {:?}",
data_rlc_cells[MAX_AGG_SNARKS * 2 + 4].value()
);
log::trace!(
"rlc from table {:?}",
data_rlc_cells[MAX_AGG_SNARKS * 2 + 5].value()
);

// assertion
let t1 = rlc_config.sub(
&mut region,
&rlc_cell,
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 3],
&mut offset,
)?;
let t2 = rlc_config.sub(
&mut region,
&rlc_cell,
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 4],
&mut offset,
)?;
let t3 = rlc_config.sub(
&mut region,
&rlc_cell,
&data_rlc_cells[MAX_AGG_SNARKS * 2 + 5],
&mut offset,
)?;
let t1t2 = rlc_config.mul(&mut region, &t1, &t2, &mut offset)?;
let t1t2t3 = rlc_config.mul(&mut region, &t1t2, &t3, &mut offset)?;
rlc_config.enforce_zero(&mut region, &t1t2t3)?;

log::trace!("rlc chip uses {} rows", offset);
Ok(num_of_valid_snarks_cell)
},
Expand Down
27 changes: 27 additions & 0 deletions aggregator/src/tests/rlc/gates.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ struct ArithTestCircuit {
f5: Fr,
f6: Fr,
f7: Fr,
f8: Fr,
}

impl Circuit<Fr> for ArithTestCircuit {
Expand Down Expand Up @@ -63,6 +64,7 @@ impl Circuit<Fr> for ArithTestCircuit {
let f5 = config.load_private(&mut region, &self.f5, &mut offset)?;
let f6 = config.load_private(&mut region, &self.f6, &mut offset)?;
let f7 = config.load_private(&mut region, &self.f7, &mut offset)?;
let f8 = config.load_private(&mut region, &self.f8, &mut offset)?;

// unit test: addition
{
Expand Down Expand Up @@ -109,6 +111,9 @@ impl Circuit<Fr> for ArithTestCircuit {

let f1_rec = config.select(&mut region, &f1, &f2, &one, &mut offset)?;
region.constrain_equal(f1.cell(), f1_rec.cell())?;

config.conditional_enforce_equal(&mut region, &f1, &f8, &one, &mut offset)?;
config.conditional_enforce_equal(&mut region, &f1, &f2, &zero, &mut offset)?;
}

let inputs = vec![f1, f2, f3, f4];
Expand Down Expand Up @@ -185,6 +190,7 @@ fn test_field_ops() {
let f5 = f1 * f2 + f3; // 19
let f6 = rlc(&[f1, f2, f3, f4], &f5);
let f7 = Fr::zero();
let f8 = f1;

{
let circuit = ArithTestCircuit {
Expand All @@ -195,6 +201,7 @@ fn test_field_ops() {
f5,
f6,
f7,
f8,
};
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
prover.assert_satisfied();
Expand All @@ -209,6 +216,7 @@ fn test_field_ops() {
f5,
f6,
f7,
f8,
};
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
assert!(prover.verify().is_err());
Expand All @@ -223,6 +231,7 @@ fn test_field_ops() {
f5,
f6,
f7,
f8,
};
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
assert!(prover.verify().is_err());
Expand All @@ -237,6 +246,7 @@ fn test_field_ops() {
f5: Fr::zero(),
f6,
f7,
f8,
};
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
assert!(prover.verify().is_err());
Expand All @@ -251,6 +261,7 @@ fn test_field_ops() {
f5,
f6: Fr::zero(),
f7,
f8,
};
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
assert!(prover.verify().is_err());
Expand All @@ -265,6 +276,22 @@ fn test_field_ops() {
f5,
f6,
f7: Fr::one(),
f8,
};
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
assert!(prover.verify().is_err());
}

{
let circuit = ArithTestCircuit {
f1,
f2,
f3,
f4,
f5,
f6,
f7,
f8: Fr::one(),
};
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
assert!(prover.verify().is_err());
Expand Down