addressed comments

This commit is contained in:
Nicholas Ward 2022-06-21 14:35:19 -07:00
parent a7f6bf3b00
commit 9434819829
4 changed files with 22 additions and 108 deletions

View File

@ -221,11 +221,12 @@ mod tests {
.to_canonical_u64()
.try_into()
.unwrap();
let clock = mem_timestamp / NUM_MEMORY_OPS;
let op = mem_timestamp % NUM_MEMORY_OPS;
let clock = mem_timestamp;
let op = (0..4)
.filter(|&o| memory_trace[memory::registers::is_memop(o)].values[i] == F::ONE)
.collect_vec()[0];
cpu_trace_rows[i][cpu::columns::uses_memop(op)] = F::ONE;
memory_trace[memory::registers::is_memop(op)].values[i] = F::ONE;
cpu_trace_rows[i][cpu::columns::CLOCK] = F::from_canonical_usize(clock);
cpu_trace_rows[i][cpu::columns::memop_is_read(op)] =
memory_trace[memory::registers::IS_READ].values[i];

View File

@ -12,6 +12,7 @@ pub mod cross_table_lookup;
mod get_challenges;
pub mod keccak;
pub mod logic;
pub mod lookup;
pub mod memory;
pub mod permutation;
pub mod proof;

View File

@ -10,7 +10,9 @@ use plonky2::timed;
use plonky2::util::timing::TimingTree;
use rand::Rng;
use super::registers::is_memop;
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::lookup::{eval_lookups, eval_lookups_circuit, permuted_cols};
use crate::memory::registers::{
sorted_value_limb, value_limb, ADDR_CONTEXT, ADDR_SEGMENT, ADDR_VIRTUAL, CONTEXT_FIRST_CHANGE,
COUNTER, COUNTER_PERMUTED, IS_READ, NUM_REGISTERS, RANGE_CHECK, RANGE_CHECK_PERMUTED,
@ -19,7 +21,7 @@ use crate::memory::registers::{
};
use crate::permutation::PermutationPair;
use crate::stark::Stark;
use crate::util::{permuted_cols, trace_rows_to_poly_values};
use crate::util::trace_rows_to_poly_values;
use crate::vars::{StarkEvaluationTargets, StarkEvaluationVars};
pub(crate) const NUM_PUBLIC_INPUTS: usize = 0;
@ -30,6 +32,7 @@ pub struct MemoryStark<F, const D: usize> {
}
pub struct MemoryOp<F> {
channel_index: usize,
timestamp: F,
is_read: F,
context: F,
@ -73,8 +76,10 @@ pub fn generate_random_memory_ops<F: RichField, R: Rng>(
};
let timestamp = F::from_canonical_usize(i);
let channel_index = rng.gen_range(0..4);
memory_ops.push(MemoryOp {
channel_index,
timestamp,
is_read: is_read_field,
context,
@ -191,6 +196,7 @@ impl<F: RichField + Extendable<D>, const D: usize> MemoryStark<F, D> {
let mut trace_cols = [(); NUM_REGISTERS].map(|_| vec![F::ZERO; num_ops]);
for i in 0..num_ops {
let MemoryOp {
channel_index,
timestamp,
is_read,
context,
@ -198,6 +204,7 @@ impl<F: RichField + Extendable<D>, const D: usize> MemoryStark<F, D> {
virt,
value,
} = memory_ops[i];
trace_cols[is_memop(channel_index)][i] = F::ONE;
trace_cols[TIMESTAMP][i] = timestamp;
trace_cols[IS_READ][i] = is_read;
trace_cols[ADDR_CONTEXT][i] = context;
@ -382,22 +389,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
.constraint(next_is_read * address_unchanged * (next_values[i] - values[i]));
}
// Lookup argument for the range check.
let local_perm_input = vars.local_values[RANGE_CHECK_PERMUTED];
let next_perm_table = vars.next_values[COUNTER_PERMUTED];
let next_perm_input = vars.next_values[RANGE_CHECK_PERMUTED];
// A "vertical" diff between the local and next permuted inputs.
let diff_input_prev = next_perm_input - local_perm_input;
// A "horizontal" diff between the next permuted input and permuted table value.
let diff_input_table = next_perm_input - next_perm_table;
yield_constr.constraint(diff_input_prev * diff_input_table);
// This is actually constraining the first row, as per the spec, since `diff_input_table`
// is a diff of the next row's values. In the context of `constraint_last_row`, the next
// row is the first row.
yield_constr.constraint_last_row(diff_input_table);
eval_lookups(vars, yield_constr, RANGE_CHECK_PERMUTED, COUNTER_PERMUTED)
}
fn eval_ext_circuit(
@ -513,23 +505,13 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
yield_constr.constraint(builder, read_constraint);
}
// Lookup argument for range check.
let local_perm_input = vars.local_values[RANGE_CHECK_PERMUTED];
let next_perm_table = vars.next_values[COUNTER_PERMUTED];
let next_perm_input = vars.next_values[RANGE_CHECK_PERMUTED];
// A "vertical" diff between the local and next permuted inputs.
let diff_input_prev = builder.sub_extension(next_perm_input, local_perm_input);
// A "horizontal" diff between the next permuted input and permuted table value.
let diff_input_table = builder.sub_extension(next_perm_input, next_perm_table);
let diff_product = builder.mul_extension(diff_input_prev, diff_input_table);
yield_constr.constraint(builder, diff_product);
// This is actually constraining the first row, as per the spec, since `diff_input_table`
// is a diff of the next row's values. In the context of `constraint_last_row`, the next
// row is the first row.
yield_constr.constraint_last_row(builder, diff_input_table);
eval_lookups_circuit(
builder,
vars,
yield_constr,
RANGE_CHECK_PERMUTED,
COUNTER_PERMUTED,
)
}
fn constraint_degree(&self) -> usize {

View File

@ -1,7 +1,5 @@
use std::cmp::Ordering;
use itertools::Itertools;
use plonky2::field::field_types::{Field, PrimeField64};
use plonky2::field::field_types::Field;
use plonky2::field::polynomial::PolynomialValues;
use plonky2::util::transpose;
@ -16,71 +14,3 @@ pub fn trace_rows_to_poly_values<F: Field, const COLUMNS: usize>(
.map(|column| PolynomialValues::new(column))
.collect()
}
/// Given an input column and a table column, generate the permuted input and permuted table columns
/// used in the Halo2 permutation argument.
pub fn permuted_cols<F: PrimeField64>(inputs: &[F], table: &[F]) -> (Vec<F>, Vec<F>) {
let n = inputs.len();
// The permuted inputs do not have to be ordered, but we found that sorting was faster than
// hash-based grouping. We also sort the table, as this helps us identify "unused" table
// elements efficiently.
// To compare elements, e.g. for sorting, we first need them in canonical form. It would be
// wasteful to canonicalize in each comparison, as a single element may be involved in many
// comparisons. So we will canonicalize once upfront, then use `to_noncanonical_u64` when
// comparing elements.
let sorted_inputs = inputs
.iter()
.map(|x| x.to_canonical())
.sorted_unstable_by_key(|x| x.to_noncanonical_u64())
.collect_vec();
let sorted_table = table
.iter()
.map(|x| x.to_canonical())
.sorted_unstable_by_key(|x| x.to_noncanonical_u64())
.collect_vec();
let mut unused_table_inds = Vec::with_capacity(n);
let mut unused_table_vals = Vec::with_capacity(n);
let mut permuted_table = vec![F::ZERO; n];
let mut i = 0;
let mut j = 0;
while (j < n) && (i < n) {
let input_val = sorted_inputs[i].to_noncanonical_u64();
let table_val = sorted_table[j].to_noncanonical_u64();
match input_val.cmp(&table_val) {
Ordering::Greater => {
unused_table_vals.push(sorted_table[j]);
j += 1;
}
Ordering::Less => {
if let Some(x) = unused_table_vals.pop() {
permuted_table[i] = x;
} else {
unused_table_inds.push(i);
}
i += 1;
}
Ordering::Equal => {
permuted_table[i] = sorted_table[j];
i += 1;
j += 1;
}
}
}
#[allow(clippy::needless_range_loop)] // indexing is just more natural here
for jj in j..n {
unused_table_vals.push(sorted_table[jj]);
}
for ii in i..n {
unused_table_inds.push(ii);
}
for (ind, val) in unused_table_inds.into_iter().zip_eq(unused_table_vals) {
permuted_table[ind] = val;
}
(sorted_inputs, permuted_table)
}