Skip to content
This repository was archived by the owner on Apr 18, 2025. It is now read-only.

Feat/da compression witgen batch fix rle #1265

Closed
noel2004 wants to merge 8 commits into from
Closed

Feat/da compression witgen batch fix rle #1265

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
cfe72c2
Fix repeated match byte slice:
darth-cy May 14, 2024
01ac90c
Add batch witgen test
darth-cy May 14, 2024
19ee614
Adjust test
darth-cy May 14, 2024
375df14
fix: handle predefined table appropriately in table reconstruction
roynalnaruto May 14, 2024
496566e
Skip predefined fse tables:
darth-cy May 15, 2024
08c4bf0
Add copy constraints and assigned exports
darth-cy May 15, 2024
f181535
add unit test for rle like instruction (match len > match offset)
noel2004 May 15, 2024
d6228d7
fixes for rle like instruction
noel2004 May 15, 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
82 changes: 52 additions & 30 deletions aggregator/src/aggregation/decoder.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ use halo2_proofs::{
circuit::{AssignedCell, Layouter, Value},
halo2curves::bn256::Fr,
plonk::{
Advice, Column, ConstraintSystem, Error, Expression, Fixed, SecondPhase, VirtualCells,
Advice, Assigned, Column, ConstraintSystem, Error, Expression, Fixed, SecondPhase, VirtualCells
},
poly::Rotation,
};
Expand Down Expand Up @@ -927,8 +927,12 @@ impl SequencesDataDecoder {
pub struct AssignedDecoderConfigExports {
/// The RLC of the zstd encoded bytes, i.e. blob bytes.
pub encoded_rlc: AssignedCell<Fr, Fr>,
/// The length of encoded data.
pub encoded_len: AssignedCell<Fr, Fr>,
/// The RLC of the decoded bytes, i.e. batch bytes.
pub decoded_rlc: AssignedCell<Fr, Fr>,
/// The length of decoded data.
pub decoded_len: AssignedCell<Fr, Fr>,
}

pub struct DecoderConfigArgs {
Expand Down Expand Up @@ -1051,6 +1055,8 @@ impl DecoderConfig {
fixed_table,
};

meta.enable_equality(config.decoded_len);

macro_rules! is_tag {
($var:ident, $tag_variant:ident) => {
let $var = |meta: &mut VirtualCells<Fr>| {
Expand Down Expand Up @@ -4098,8 +4104,8 @@ impl DecoderConfig {
challenges: &Challenges<Value<Fr>>,
k: u32,
// witgen_debug
// ) -> Result<AssignedDecoderConfigExports, Error> {
) -> Result<(), Error> {
) -> Result<AssignedDecoderConfigExports, Error> {
// ) -> Result<(), Error> {
let mut pow_of_rand: Vec<Value<Fr>> = vec![Value::known(Fr::ONE)];

assert!(!block_info_arr.is_empty(), "Must have at least 1 block");
Expand Down Expand Up @@ -4185,7 +4191,7 @@ impl DecoderConfig {
(1 << k) - self.unusable_rows(),
)?;
// TODO: use equality constraint for the exported_len and exported_rlc cell
let (_exported_len, _exported_rlc) = self.sequence_execution_config.assign(
let (exported_len, exported_rlc) = self.sequence_execution_config.assign(
layouter,
challenges,
literal_datas
Expand All @@ -4203,6 +4209,15 @@ impl DecoderConfig {
layouter.assign_region(
|| "Decompression table region",
|mut region| {
////////////////////////////////////////////////////////
//////// Capture Copy Constraint/Export Cells /////////
////////////////////////////////////////////////////////
let mut last_encoded_rlc: Value<Fr> = Value::known(Fr::zero());
let mut encoded_rlc_cell: Option<AssignedCell<Fr, Fr>> = None;
let mut byte_idx_cell: Option<AssignedCell<Fr, Fr>> = None;
let mut last_decoded_len: Value<Fr> = Value::known(Fr::zero());
let mut decoded_length_cell: Option<AssignedCell<Fr, Fr>> = None;

/////////////////////////////////////////
/////////// Assign First Row ///////////
/////////////////////////////////////////
Expand Down Expand Up @@ -4259,18 +4274,20 @@ impl DecoderConfig {
},
)?;
}
region.assign_advice(
encoded_rlc_cell = Some(region.assign_advice(
|| "encoded_rlc",
self.encoded_rlc,
i,
|| row.encoded_data.value_rlc,
)?;
region.assign_advice(
)?);
last_encoded_rlc = row.encoded_data.value_rlc;
decoded_length_cell = Some(region.assign_advice(
|| "decoded_len",
self.decoded_len,
i,
|| Value::known(Fr::from(row.decoded_data.decoded_len)),
)?;
)?);
last_decoded_len = Value::known(Fr::from(row.decoded_data.decoded_len));

/////////////////////////////////////////
///// Assign Bitstream Decoder /////////
Expand Down Expand Up @@ -4684,17 +4701,25 @@ impl DecoderConfig {
)?;
}

let mut padding_count = 2usize;
for idx in witness_rows.len()..((1 << k) - self.unusable_rows()) {
if padding_count > 0 {
region.assign_advice(
|| "byte_idx",
self.byte_idx,
idx,
|| Value::known(Fr::from(last_byte_idx + 1)),
)?;
padding_count -= 1;
}
byte_idx_cell = Some(region.assign_advice(
|| "byte_idx",
self.byte_idx,
idx,
|| Value::known(Fr::from(last_byte_idx + 1)),
)?);
encoded_rlc_cell = Some(region.assign_advice(
|| "encoded_rlc",
self.encoded_rlc,
idx,
|| last_encoded_rlc,
)?);
decoded_length_cell = Some(region.assign_advice(
|| "decoded_len",
self.decoded_len,
idx,
|| last_decoded_len,
)?);
region.assign_advice(
|| "tag_config.tag",
self.tag_config.tag,
Expand Down Expand Up @@ -4764,19 +4789,16 @@ impl DecoderConfig {
)?;
}

Ok(())
},
)?;

// witgen_debug
// pub struct AssignedDecoderConfigExports {
// /// The RLC of the zstd encoded bytes, i.e. blob bytes.
// pub encoded_rlc: AssignedCell<Fr, Fr>,
// /// The RLC of the decoded bytes, i.e. batch bytes.
// pub decoded_rlc: AssignedCell<Fr, Fr>,
// }
region.constrain_equal(exported_len.cell(), decoded_length_cell.as_ref().unwrap().cell())?;

Ok(())
Ok(AssignedDecoderConfigExports {
encoded_rlc: encoded_rlc_cell.unwrap(),
encoded_len: byte_idx_cell.unwrap(),
decoded_len: exported_len.clone(),
decoded_rlc: exported_rlc.clone(),
})
},
)
}

pub fn unusable_rows(&self) -> usize {
Expand Down
27 changes: 24 additions & 3 deletions aggregator/src/aggregation/decoder/seq_exec.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1094,8 +1094,9 @@ mod tests {
inst.instruction_idx as usize,
SequenceExecInfo::BackRef(r.clone()),
));
let matched_bytes = Vec::from(&outputs[r]);
outputs.extend(matched_bytes);
for ref_pos in r {
outputs.push(outputs[ref_pos]);
}
}
current_literal_pos = new_literal_pos;
}
Expand Down Expand Up @@ -1231,7 +1232,7 @@ mod tests {
AddressTableRow::mock_samples_full([
[1, 4, 1, 1, 4, 8],
[9, 1, 3, 6, 1, 4],
[3, 0, 4, 5, 6, 1],
[3, 0, 4, 5, 6, 1], // ref offset 3 while literal == 0
]),
);

Expand All @@ -1243,6 +1244,26 @@ mod tests {
mock_prover.verify().unwrap();
}

#[test]
fn seq_exec_rle_like() {
// no instructions, we only copy literals to output
let circuit = SeqExecMock::mock_generate(
Vec::from("abcdef".as_bytes()),
AddressTableRow::mock_samples_full([
[1, 4, 1, 1, 4, 8],
[9, 1, 3, 6, 1, 4],
[5, 0, 6, 2, 6, 1], // an RLE like inst, match len exceed match offset
]),
);

assert_eq!(circuit.outputs, Vec::from("abcddeabcbcbcbcf".as_bytes()));

let k = 12;
let mock_prover =
MockProver::<Fr>::run(k, &circuit, vec![]).expect("failed to run mock prover");
mock_prover.verify().unwrap();
}

#[test]
fn seq_exec_no_tail_cp() {
// no instructions, we only copy literals to output
Expand Down
Loading