logos-storage/plonky2
1
0
Fork 0
mirror of https://github.com/logos-storage/plonky2.git synced 2026-01-02 13:53:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

Move system-zero to its own repo

Browse Source 
See https://github.com/mir-protocol/system-zero
This commit is contained in:
Daniel Lubarov 2023-02-25 16:19:00 -08:00
parent 7781dd366f
commit bfaa80a38c
30 changed files with 1 additions and 3009 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Cargo.toml
View File

@ -1,5 +1,5 @@
[workspace]
members = ["ecdsa", "evm", "field", "insertion", "maybe_rayon", "plonky2", "starky", "system_zero", "u32", "util", "waksman"]
members = ["ecdsa", "evm", "field", "insertion", "maybe_rayon", "plonky2", "starky", "u32", "util", "waksman"]
[profile.release]
opt-level = 3

26
system_zero/Cargo.toml
View File

@ -1,26 +0,0 @@
[package]
name = "system_zero"
description = "A VM whose execution can be verified with STARKs; designed for proving Ethereum transactions"
version = "0.1.0"
edition = "2021"
[dependencies]
anyhow = "1.0.40"
itertools = "0.10.0"
log = "0.4.14"
plonky2 = { version = "0.1.2" }
plonky2_util = { version = "0.1.0" }
rand = "0.8.4"
rand_chacha = "0.3.1"
starky = { version = "0.1.1" }
[dev-dependencies]
criterion = "0.4.0"
env_logger = "0.10.0"
[[bench]]
name = "lookup_permuted_cols"
harness = false
[target.'cfg(not(target_env = "msvc"))'.dev-dependencies]
jemallocator = "0.5.0"

7
system_zero/benches/allocator/mod.rs
View File

@ -1,7 +0,0 @@
// Set up Jemalloc
#[cfg(not(target_env = "msvc"))]
use jemallocator::Jemalloc;
#[cfg(not(target_env = "msvc"))]
#[global_allocator]
static GLOBAL: Jemalloc = Jemalloc;

32
system_zero/benches/lookup_permuted_cols.rs
View File

@ -1,32 +0,0 @@
mod allocator;
use criterion::{criterion_group, criterion_main, BenchmarkId, Criterion};
use itertools::Itertools;
use plonky2::field::goldilocks_field::GoldilocksField;
use plonky2::field::types::Field;
use rand::{thread_rng, Rng};
use system_zero::lookup::permuted_cols;
type F = GoldilocksField;
fn criterion_benchmark(c: &mut Criterion) {
let mut group = c.benchmark_group("lookup-permuted-cols");
for size_log in [16, 17, 18] {
let size = 1 << size_log;
group.bench_with_input(BenchmarkId::from_parameter(size), &size, |b, _| {
// We could benchmark a table of random values with
// let table = F::rand_vec(size);
// But in practice we currently use tables that are pre-sorted, which makes
// permuted_cols cheaper since it will sort the table.
let table = (0..size).map(F::from_canonical_usize).collect_vec();
let input = (0..size)
.map(|_| table[thread_rng().gen_range(0..size)])
.collect_vec();
b.iter(|| permuted_cols(&input, &table));
});
}
}
criterion_group!(benches, criterion_benchmark);
criterion_main!(benches);

70
system_zero/src/alu/addition.rs
View File

@ -1,70 +0,0 @@
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::{Field, PrimeField64};
use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use plonky2::plonk::plonk_common::reduce_with_powers_ext_circuit;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::registers::alu::*;
use crate::registers::NUM_COLUMNS;
pub(crate) fn generate_addition<F: PrimeField64>(values: &mut [F; NUM_COLUMNS]) {
let in_1 = values[COL_ADD_INPUT_0].to_canonical_u64();
let in_2 = values[COL_ADD_INPUT_1].to_canonical_u64();
let in_3 = values[COL_ADD_INPUT_2].to_canonical_u64();
let output = in_1 + in_2 + in_3;
values[COL_ADD_OUTPUT_0] = F::from_canonical_u16(output as u16);
values[COL_ADD_OUTPUT_1] = F::from_canonical_u16((output >> 16) as u16);
values[COL_ADD_OUTPUT_2] = F::from_canonical_u16((output >> 32) as u16);
}
pub(crate) fn eval_addition<F: Field, P: PackedField<Scalar = F>>(
local_values: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
) {
let is_add = local_values[IS_ADD];
let in_1 = local_values[COL_ADD_INPUT_0];
let in_2 = local_values[COL_ADD_INPUT_1];
let in_3 = local_values[COL_ADD_INPUT_2];
let out_1 = local_values[COL_ADD_OUTPUT_0];
let out_2 = local_values[COL_ADD_OUTPUT_1];
let out_3 = local_values[COL_ADD_OUTPUT_2];
let weight_2 = F::from_canonical_u64(1 << 16);
let weight_3 = F::from_canonical_u64(1 << 32);
// Note that this can't overflow. Since each output limb has been range checked as 16-bits,
// this sum can be around 48 bits at most.
let out = out_1 + out_2 * weight_2 + out_3 * weight_3;
let computed_out = in_1 + in_2 + in_3;
yield_constr.constraint(is_add * (out - computed_out));
}
pub(crate) fn eval_addition_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
local_values: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let is_add = local_values[IS_ADD];
let in_1 = local_values[COL_ADD_INPUT_0];
let in_2 = local_values[COL_ADD_INPUT_1];
let in_3 = local_values[COL_ADD_INPUT_2];
let out_1 = local_values[COL_ADD_OUTPUT_0];
let out_2 = local_values[COL_ADD_OUTPUT_1];
let out_3 = local_values[COL_ADD_OUTPUT_2];
let limb_base = builder.constant(F::from_canonical_u64(1 << 16));
// Note that this can't overflow. Since each output limb has been range checked as 16-bits,
// this sum can be around 48 bits at most.
let out = reduce_with_powers_ext_circuit(builder, &[out_1, out_2, out_3], limb_base);
let computed_out = builder.add_many_extension([in_1, in_2, in_3]);
let diff = builder.sub_extension(out, computed_out);
let filtered_diff = builder.mul_extension(is_add, diff);
yield_constr.constraint(builder, filtered_diff);
}

360
system_zero/src/alu/bitops.rs
View File

@ -1,360 +0,0 @@
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::{Field, PrimeField64};
use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use plonky2::plonk::plonk_common::reduce_with_powers_ext_circuit;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::registers::alu::*;
use crate::registers::NUM_COLUMNS;
/// Interpret the N <= 32 elements of `bits` as bits from low to high of a
/// u32 and return \sum_i bits[i] 2^i as an element of P.
pub(crate) fn binary_to_u32<F, P>(bits: [P; 32]) -> P
where
F: Field,
P: PackedField<Scalar = F>,
{
bits.into_iter()
.enumerate()
.map(|(i, b)| b * F::from_canonical_u64(1u64 << i))
.sum()
}
fn generate_bitop_32<F: PrimeField64>(
values: &mut [F; NUM_COLUMNS],
bitop: usize,
input_a_regs: [usize; 32],
input_b_regs: [usize; 32],
output_reg: usize,
) {
let a_bits = input_a_regs.map(|r| values[r]);
let b_bits = input_b_regs.map(|r| values[r]);
let a = binary_to_u32(a_bits).to_canonical_u64() as u32;
let b = binary_to_u32(b_bits).to_canonical_u64() as u32;
let out = match bitop {
IS_AND => a & b,
IS_IOR => a | b,
IS_XOR => a ^ b,
IS_ANDNOT => a & !b,
_ => panic!("unrecognized bitop instruction code"),
};
values[output_reg] = F::from_canonical_u32(out);
}
/// Use the `COL_BIT_DECOMP_INPUT_[AB]_{LO,HI}_*` registers to read
/// bits from `values`, apply `bitop` to the reconstructed u32's (both
/// lo and hi, for 64 bits total), and write the result to the
/// `COL_BITOP_OUTPUT_*` registers.
pub(crate) fn generate_bitop<F: PrimeField64>(values: &mut [F; NUM_COLUMNS], bitop: usize) {
// Generate lo half
generate_bitop_32(
values,
bitop,
COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS,
COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS,
COL_BITOP_OUTPUT_0,
);
// Generate hi half
generate_bitop_32(
values,
bitop,
COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS,
COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS,
COL_BITOP_OUTPUT_1,
);
}
fn eval_bitop_32<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
input_a_regs: [usize; 32],
input_b_regs: [usize; 32],
output_reg: usize,
yield_constr: &mut ConstraintConsumer<P>,
) {
// Filters
let is_and = lv[IS_AND];
let is_ior = lv[IS_IOR];
let is_xor = lv[IS_XOR];
let is_andnot = lv[IS_ANDNOT];
// Inputs
let a_bits = input_a_regs.map(|r| lv[r]);
let b_bits = input_b_regs.map(|r| lv[r]);
// Ensure that the inputs are bits
let inst_constr = is_and + is_ior + is_xor + is_andnot;
a_bits.map(|v| yield_constr.constraint(inst_constr * (v * v - v)));
b_bits.map(|v| yield_constr.constraint(inst_constr * (v * v - v)));
// Output
let output = lv[output_reg];
let a = binary_to_u32(a_bits);
let b = binary_to_u32(b_bits);
let a_and_b = binary_to_u32(a_bits.zip(b_bits).map(|(b0, b1)| b0 * b1));
let constraint = is_and * (a_and_b - output)
+ is_ior * (a + b - a_and_b - output)
+ is_xor * (a + b - a_and_b * F::TWO - output)
+ is_andnot * (a - a_and_b - output);
yield_constr.constraint(constraint);
}
/// Verify an AND, IOR, XOR, or ANDNOT instruction.
pub(crate) fn eval_bitop<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
) {
// Constraint for lo half
eval_bitop_32(
lv,
COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS,
COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS,
COL_BITOP_OUTPUT_0,
yield_constr,
);
// Constraint for hi half
eval_bitop_32(
lv,
COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS,
COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS,
COL_BITOP_OUTPUT_1,
yield_constr,
);
}
pub(crate) fn constrain_all_to_bits_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
filter: ExtensionTarget<D>,
vals: &[ExtensionTarget<D>],
) {
for v in vals.iter() {
let t0 = builder.mul_sub_extension(*v, *v, *v);
let t1 = builder.mul_extension(filter, t0);
yield_constr.constraint(builder, t1)
}
}
/// As for `eval_bitop`, but build with `builder`.
fn eval_bitop_32_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
input_a_regs: [usize; 32],
input_b_regs: [usize; 32],
output_reg: usize,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
// Filters
let is_and = lv[IS_AND];
let is_ior = lv[IS_IOR];
let is_xor = lv[IS_XOR];
let is_andnot = lv[IS_ANDNOT];
// Inputs
let a_bits = input_a_regs.map(|r| lv[r]);
let b_bits = input_b_regs.map(|r| lv[r]);
// Ensure that the inputs are bits
let inst_constr = builder.add_many_extension([is_and, is_ior, is_xor, is_andnot]);
constrain_all_to_bits_circuit(builder, yield_constr, inst_constr, &a_bits);
constrain_all_to_bits_circuit(builder, yield_constr, inst_constr, &b_bits);
// Output
let output = lv[output_reg];
let limb_base = builder.constant(F::TWO);
let a = reduce_with_powers_ext_circuit(builder, &a_bits, limb_base);
let b = reduce_with_powers_ext_circuit(builder, &b_bits, limb_base);
let a_and_b_bits = a_bits
.zip(b_bits)
.map(|(b0, b1)| builder.mul_extension(b0, b1));
let a_and_b = reduce_with_powers_ext_circuit(builder, &a_and_b_bits, limb_base);
let and_constr = {
let t = builder.sub_extension(a_and_b, output);
builder.mul_extension(t, is_and)
};
let ior_constr = {
let t0 = builder.add_extension(a, b);
let t1 = builder.sub_extension(t0, a_and_b);
let t2 = builder.sub_extension(t1, output);
builder.mul_extension(t2, is_ior)
};
let xor_constr = {
let t0 = builder.add_extension(a, b);
let t1 = builder.mul_const_extension(F::TWO, a_and_b);
let t2 = builder.sub_extension(t0, t1);
let t3 = builder.sub_extension(t2, output);
builder.mul_extension(t3, is_xor)
};
let andnot_constr = {
let t0 = builder.sub_extension(a, a_and_b);
let t1 = builder.sub_extension(t0, output);
builder.mul_extension(t1, is_andnot)
};
let constr = builder.add_many_extension([and_constr, ior_constr, xor_constr, andnot_constr]);
yield_constr.constraint(builder, constr);
}
/// As for `eval_bitop` but with a builder.
pub(crate) fn eval_bitop_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
// Recursive constraint for lo half
eval_bitop_32_circuit(
builder,
lv,
COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS,
COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS,
COL_BITOP_OUTPUT_0,
yield_constr,
);
// Recursive constraint for hi half
eval_bitop_32_circuit(
builder,
lv,
COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS,
COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS,
COL_BITOP_OUTPUT_1,
yield_constr,
);
}
#[cfg(test)]
mod tests {
use plonky2::field::goldilocks_field::GoldilocksField;
use plonky2::field::types::Sample;
use rand::{Rng, SeedableRng};
use rand_chacha::ChaCha8Rng;
use starky::constraint_consumer::ConstraintConsumer;
use super::*;
use crate::registers::NUM_COLUMNS;
#[test]
fn generate_eval_consistency_not_bitop() {
type F = GoldilocksField;
let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25);
let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng));
// if `IS_bitop == 0`, then the constraints should be met even
// if all values are garbage.
for bitop in [IS_AND, IS_IOR, IS_XOR, IS_ANDNOT] {
values[bitop] = F::ZERO;
}
let mut constrant_consumer = ConstraintConsumer::new(
vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)],
GoldilocksField::ONE,
GoldilocksField::ONE,
GoldilocksField::ONE,
);
eval_bitop(&values, &mut constrant_consumer);
for &acc in &constrant_consumer.constraint_accs {
assert_eq!(acc, GoldilocksField::ZERO);
}
}
#[test]
fn generate_eval_consistency_bitop() {
type F = GoldilocksField;
let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25);
let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng));
const BITOPS: [usize; 4] = [IS_AND, IS_IOR, IS_XOR, IS_ANDNOT];
for bitop in BITOPS {
// Reset all the instruction registers
for op in BITOPS {
values[op] = F::ZERO;
}
// set `IS_bitop == 1` and ensure all constraints are satisfied.
values[bitop] = F::ONE;
// Set inputs to random binary values
let all_bin_regs = COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS
.into_iter()
.chain(COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS)
.chain(COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS)
.chain(COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS);
for reg in all_bin_regs {
values[reg] = F::from_canonical_u32(rng.gen::<u32>() & 1);
}
generate_bitop(&mut values, bitop);
let mut constrant_consumer = ConstraintConsumer::new(
vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)],
GoldilocksField::ONE,
GoldilocksField::ONE,
GoldilocksField::ONE,
);
eval_bitop(&values, &mut constrant_consumer);
for &acc in &constrant_consumer.constraint_accs {
assert_eq!(acc, GoldilocksField::ZERO);
}
}
}
#[test]
fn generate_eval_consistency_bit_inputs() {
type F = GoldilocksField;
let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25);
let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng));
const BITOPS: [usize; 4] = [IS_AND, IS_IOR, IS_XOR, IS_ANDNOT];
for bitop in BITOPS {
// Reset all the instruction registers
for op in BITOPS {
values[op] = F::ZERO;
}
// set `IS_bitop == 1` and ensure all constraints are satisfied.
values[bitop] = F::ONE;
// Set inputs to random binary values
let all_bin_regs = COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS
.into_iter()
.chain(COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS)
.chain(COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS)
.chain(COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS);
for reg in all_bin_regs {
values[reg] = F::from_canonical_u32(rng.gen::<u32>() & 1);
}
// Make first "bit" non-binary.
values[COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS[0]] = F::TWO;
generate_bitop(&mut values, bitop);
let mut constrant_consumer = ConstraintConsumer::new(
vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)],
GoldilocksField::ONE,
GoldilocksField::ONE,
GoldilocksField::ONE,
);
eval_bitop(&values, &mut constrant_consumer);
for &acc in &constrant_consumer.constraint_accs {
assert_ne!(acc, GoldilocksField::ZERO);
}
}
}
// TODO: test eval_division_recursively.
}

109
system_zero/src/alu/canonical.rs
View File

@ -1,109 +0,0 @@
//! Helper methods for checking that a value is canonical, i.e. is less than `|F|`.
//!
//! See https://hackmd.io/NC-yRmmtRQSvToTHb96e8Q#Checking-element-validity
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::Field;
use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
/// Computes the helper value used in the is-canonical check.
pub(crate) fn compute_canonical_inv<F: Field>(value_to_check: u64) -> F {
let value_hi_32 = (value_to_check >> 32) as u32;
if value_hi_32 == u32::MAX {
debug_assert_eq!(value_to_check as u32, 0, "Value was not canonical.");
// In this case it doesn't matter what we put for the purported inverse value. The
// constraint containing this value will get multiplied by the low u32 limb, which will be
// zero, satisfying the constraint regardless of what we put here.
F::ZERO
} else {
F::from_canonical_u32(u32::MAX - value_hi_32).inverse()
}
}
/// Adds constraints to require that a list of four `u16`s, in little-endian order, represent a
/// canonical field element, i.e. that their combined value is less than `|F|`. Returns their
/// combined value.
pub(crate) fn combine_u16s_check_canonical<F: Field, P: PackedField<Scalar = F>>(
limb_0_u16: P,
limb_1_u16: P,
limb_2_u16: P,
limb_3_u16: P,
inverse: P,
yield_constr: &mut ConstraintConsumer<P>,
) -> P {
let base = F::from_canonical_u32(1 << 16);
let limb_0_u32 = limb_0_u16 + limb_1_u16 * base;
let limb_1_u32 = limb_2_u16 + limb_3_u16 * base;
combine_u32s_check_canonical(limb_0_u32, limb_1_u32, inverse, yield_constr)
}
/// Adds constraints to require that a list of four `u16`s, in little-endian order, represent a
/// canonical field element, i.e. that their combined value is less than `|F|`. Returns their
/// combined value.
pub(crate) fn combine_u16s_check_canonical_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
limb_0_u16: ExtensionTarget<D>,
limb_1_u16: ExtensionTarget<D>,
limb_2_u16: ExtensionTarget<D>,
limb_3_u16: ExtensionTarget<D>,
inverse: ExtensionTarget<D>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) -> ExtensionTarget<D> {
let base = F::from_canonical_u32(1 << 16);
let limb_0_u32 = builder.mul_const_add_extension(base, limb_1_u16, limb_0_u16);
let limb_1_u32 = builder.mul_const_add_extension(base, limb_3_u16, limb_2_u16);
combine_u32s_check_canonical_circuit(builder, limb_0_u32, limb_1_u32, inverse, yield_constr)
}
/// Adds constraints to require that a pair of `u32`s, in little-endian order, represent a canonical
/// field element, i.e. that their combined value is less than `|F|`. Returns their combined value.
pub(crate) fn combine_u32s_check_canonical<F: Field, P: PackedField<Scalar = F>>(
limb_0_u32: P,
limb_1_u32: P,
inverse: P,
yield_constr: &mut ConstraintConsumer<P>,
) -> P {
let u32_max = P::from(F::from_canonical_u32(u32::MAX));
// This is zero if and only if the high limb is `u32::MAX`.
let diff = u32_max - limb_1_u32;
// If this is zero, the diff is invertible, so the high limb is not `u32::MAX`.
let hi_not_max = inverse * diff - F::ONE;
// If this is zero, either the high limb is not `u32::MAX`, or the low limb is zero.
let hi_not_max_or_lo_zero = hi_not_max * limb_0_u32;
yield_constr.constraint(hi_not_max_or_lo_zero);
// Return the combined value.
limb_0_u32 + limb_1_u32 * F::from_canonical_u64(1 << 32)
}
/// Adds constraints to require that a pair of `u32`s, in little-endian order, represent a canonical
/// field element, i.e. that their combined value is less than `|F|`. Returns their combined value.
pub(crate) fn combine_u32s_check_canonical_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
limb_0_u32: ExtensionTarget<D>,
limb_1_u32: ExtensionTarget<D>,
inverse: ExtensionTarget<D>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) -> ExtensionTarget<D> {
let one = builder.one_extension();
let u32_max = builder.constant_extension(F::Extension::from_canonical_u32(u32::MAX));
// This is zero if and only if the high limb is `u32::MAX`.
let diff = builder.sub_extension(u32_max, limb_1_u32);
// If this is zero, the diff is invertible, so the high limb is not `u32::MAX`.
let hi_not_max = builder.mul_sub_extension(inverse, diff, one);
// If this is zero, either the high limb is not `u32::MAX`, or the low limb is zero.
let hi_not_max_or_lo_zero = builder.mul_extension(hi_not_max, limb_0_u32);
yield_constr.constraint(builder, hi_not_max_or_lo_zero);
// Return the combined value.
builder.mul_const_add_extension(F::from_canonical_u64(1 << 32), limb_1_u32, limb_0_u32)
}

93
system_zero/src/alu/div-constraints-proof.txt
View File

@ -1,93 +0,0 @@
Constraints A (implemented in code):
A1. dividend ∈ {0, …, u32::MAX}
A2. divisor ∈ {0, …, u32::MAX}
A3. quotient ∈ {0, …, u32::MAX}
A4. remainder ∈ {0, …, u32::MAX}
A5. divisor_rem_diff_m1 ∈ {0, …, u32::MAX}
A6. divisor * div_inverse = div_div_inverse
A7. (div_div_inverse - 1) * (remainder - quotient - u32::MAX) = 0
A8. divisor * (div_div_inverse - 1) = 0
A9. div_inverse * dividend = quotient + remainder * div_inverse
A10. divisor * (divisor - remainder - 1 - divisor_rem_diff_m1) = 0
Constraints B (intuitive division):
B1. dividend ∈ {0, …, u32::MAX}
B2. divisor ∈ {0, …, u32::MAX}
B3. divisor = 0 => quotient = 0
B4. divisor = 0 => remainder = u32::MAX
B5. divisor ≠ 0 => dividend = quotient * divisor + remainder
B6. divisor ≠ 0 => quotient ∈ {0, …, u32::MAX}
B7. divisor ≠ 0 => remainder ∈ {0, …, divisor - 1}
Assume we meet constraints A for some dividend, divisor, quotient, remainder, divisor_rem_diff_m1, div_inverse, and div_div_inverse. We want to show that constrants B are met.
B1. Trivial by A1.
B2. Trivial by A2.
B3. Assume divisor = 0. Then div_div_inverse = 0 by A6. div_div_inverse - 1 ≠ 0, so remainder - quotient = u32::MAX by A7.
quotient ∈ {0, …, u32::MAX} by A3 and remainder ∈ {0, …, u32::MAX} by A4. Then remainder - quotient ∈ {-quotient, …, u32::MAX - quotient}.
If quotient ≠ 0, then quotient ∈ {1, …, u32::MAX} and remainder - quotient ∈ {-u32::MAX, …, u32::MAX - 1}, which does not include u32::MAX, contradicting A7.
B4. Assume divisor = 0. Then div_div_inverse = 0 by A6. div_div_inverse - 1 ≠ 0, so remainder - quotient = u32::MAX by A7.
quotient ∈ {0, …, u32::MAX} by A3 and remainder ∈ {0, …, u32::MAX} by A4. Then remainder - quotient ∈ {remainder - u32::MAX, …, remainder}.
If remainder ≠ u32::MAX, then remainder ∈ {0, …, u32::MAX - 1} and remainder - quotient ∈ {-u32::MAX, …, u32::MAX - 1} which does not include u32::MAX, contradicting A7.
B5. Assume divisor ≠ 0. By A8, div_div_inverse = 1. By A6, div_inverse = divisor^-1. Multiplying both sides of A9 by divisor, dividend = quotient * divisor + remainder.
B6. Follows from A3.
B7. remainder ∈ {0, …, u32::MAX} by A4. Assume divisor ≠ 0. Then divisor_rem_diff_m1 = divisor - remainder - 1 by A10. divisor ∈ {1, …, u32::MAX} by A2. If remainder ∈ {divisor, …, u32::MAX}, then divisor - remainder - 1 ∈ {-u32::MAX, …, u32::MAX - divisor} ⊆ {-u32::MAX, …, u32::MAX - 1}, contradicting A5. Hence, remainder ∈ {0, …, divisor - 1}.
Assume we meet constraints B for some dividend, divisor, quotient, and remainder. We want to show
that there exist divisor_rem_diff_m1, div_inverse, div_div_inverse, such that constrants A are met.
If divisor = 0, set divisor_rem_diff_m1 = 0, div_inverse = 0, div_div_inverse = 0.
Otherwise, set divisor_rem_diff_m1 = divisor - remainder - 1, div_inverse = divisor^-1, div_div_inverse = 1.
A1. Trivial by B1.
A2. Trivial by B2.
The remainder is by cases:
(divisor = 0)
A3. Follows from B3.
A4. Follows from B4.
A5. Follows from our choice of divisor_rem_diff_m1 = 0.
A6. Follows from our choice of div_div_inverse = 0.
A7. quotient = 0 by B3. remainder = u32::MAX by B4. Then remainder - quotient = u32::MAX.
A8. Trivial since divisor = 0.
A9. By our choice, div_inverse = 0. quotient = 0 by B3.
A10. Trivial since divisor = 0.
(divisor ≠ 0)
A3. Follows from B6.
A4. By B7, remainder ∈ {0, …, divisor - 1}, and by B2, divisor ∈ {0, …, u32::MAX}, implying that remainder ∈ {0, …, u32::MAX - 1}.
A5. We've set divisor_rem_diff_m1 = divisor - remainder - 1. remainder ∈ {0, …, divisor - 1}, so divisor - remainder ∈ {1, …, divisor} and divisor - remainder - 1 = divisor_rem_diff_m1 ∈ {0, …, divisor - 1}. From B2, divisor ∈ {0, …, u32::MAX}, so divisor_rem_diff_m1 ∈ {0, …, u32::MAX - 1} as desired.
A6. div_inverse = divisor^-1 by choice, so divisor * div_inverse = 1. div_div_inverse = 1 by choice.
A7. div_div_inverse = 1 by choice, so div_div_inverse - 1 = 0.
A8. div_div_inverse = 1 by choice, so div_div_inverse - 1 = 0.
A9. From B5, dividend = quotient * divisor + remainder. Since divisor ≠ 0, div_inverse = divisor^-1 by choice. Multiplying both sides by div_inverse, dividend * div_inverse = quotient * divisor * div_inverse + remainder * div_inverse = quotient + remainder * div_inverse.
A10. By our choice of divisor_rem_diff_m1 = divisor - remainder - 1.

221
system_zero/src/alu/division.rs
View File

@ -1,221 +0,0 @@
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::{Field, PrimeField64};
use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::registers::alu::*;
use crate::registers::NUM_COLUMNS;
/// Division instruction of a u32 divisor N into a u32 dividend D,
/// with u32 quotient Q and u32 remainder R. If D is not zero, then
/// the values will satisfy N = Q*D + R with 0 <= R < D. If D is
/// zero, then the remainder is set to the special value u32::MAX =
/// 2^32 - 1 (which is not a valid remainder for any nonzero D) and
/// the quotient is set to zero. In particular, no overflow is
/// possible.
pub(crate) fn generate_division<F: PrimeField64>(values: &mut [F; NUM_COLUMNS]) {
let dividend = values[COL_DIV_INPUT_DIVIDEND].to_canonical_u64() as u32;
let divisor = values[COL_DIV_INPUT_DIVISOR].to_canonical_u64() as u32;
// `COL_DIV_INVDIVISOR` is `divisor^-1` if `divisor != 0` and `0` otherwise.
// `COL_DIV_NONZERO_DIVISOR` is `1` if `divisor != 0` and `0` otherwise.
// `COL_DIV_RANGE_CHECKED_TMP` is set to `divisor - rem - 1` if `divisor != 0` and `0`
// otherwise. This is used to ensure that `rem < divisor` when `divisor != 0`.
if divisor == 0 {
// Outputs
values[COL_DIV_OUTPUT_QUOT_0] = F::ZERO;
values[COL_DIV_OUTPUT_QUOT_1] = F::ZERO;
values[COL_DIV_OUTPUT_REM_0] = F::from_canonical_u16(u16::MAX);
values[COL_DIV_OUTPUT_REM_1] = F::from_canonical_u16(u16::MAX);
// Temporaries
values[COL_DIV_RANGE_CHECKED_TMP_0] = F::ZERO;
values[COL_DIV_RANGE_CHECKED_TMP_1] = F::ZERO;
values[COL_DIV_INVDIVISOR] = F::ZERO;
values[COL_DIV_NONZERO_DIVISOR] = F::ZERO;
} else {
let quo = dividend / divisor;
let rem = dividend % divisor;
let div_rem_diff_m1 = divisor - rem - 1;
// Outputs
values[COL_DIV_OUTPUT_QUOT_0] = F::from_canonical_u16(quo as u16);
values[COL_DIV_OUTPUT_QUOT_1] = F::from_canonical_u16((quo >> 16) as u16);
values[COL_DIV_OUTPUT_REM_0] = F::from_canonical_u16(rem as u16);
values[COL_DIV_OUTPUT_REM_1] = F::from_canonical_u16((rem >> 16) as u16);
// Temporaries
values[COL_DIV_RANGE_CHECKED_TMP_0] = F::from_canonical_u16(div_rem_diff_m1 as u16);
values[COL_DIV_RANGE_CHECKED_TMP_1] = F::from_canonical_u16((div_rem_diff_m1 >> 16) as u16);
values[COL_DIV_INVDIVISOR] = F::from_canonical_u32(divisor).inverse();
values[COL_DIV_NONZERO_DIVISOR] = F::ONE;
}
}
pub(crate) fn eval_division<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
) {
let base = F::from_canonical_u64(1 << 16);
let u32_max = P::from(F::from_canonical_u32(u32::MAX));
// Filter
let is_div = lv[IS_DIV];
// Inputs
let dividend = lv[COL_DIV_INPUT_DIVIDEND];
let divisor = lv[COL_DIV_INPUT_DIVISOR];
// Outputs
let quotient = lv[COL_DIV_OUTPUT_QUOT_0] + lv[COL_DIV_OUTPUT_QUOT_1] * base;
let remainder = lv[COL_DIV_OUTPUT_REM_0] + lv[COL_DIV_OUTPUT_REM_1] * base;
// Temporaries
let divinv = lv[COL_DIV_INVDIVISOR];
let div_divinv = lv[COL_DIV_NONZERO_DIVISOR];
let div_rem_diff_m1 = lv[COL_DIV_RANGE_CHECKED_TMP_0] + lv[COL_DIV_RANGE_CHECKED_TMP_1] * base;
// Constraints
yield_constr.constraint(is_div * (divisor * divinv - div_divinv));
yield_constr.constraint(is_div * (div_divinv - F::ONE) * (remainder - quotient - u32_max));
yield_constr.constraint(is_div * divisor * (div_divinv - F::ONE));
yield_constr.constraint(is_div * (quotient + remainder * divinv - divinv * dividend));
yield_constr.constraint(is_div * divisor * (divisor - remainder - F::ONE - div_rem_diff_m1));
}
pub(crate) fn eval_division_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let base = builder.constant_extension(F::Extension::from_canonical_u64(1 << 16));
let u32_max = builder.constant_extension(F::Extension::from_canonical_u32(u32::MAX));
let one = builder.constant_extension(F::Extension::ONE);
// Filter
let is_div = lv[IS_DIV];
// Inputs
let dividend = lv[COL_DIV_INPUT_DIVIDEND];
let divisor = lv[COL_DIV_INPUT_DIVISOR];
// Outputs
let quotient =
builder.mul_add_extension(lv[COL_DIV_OUTPUT_QUOT_1], base, lv[COL_DIV_OUTPUT_QUOT_0]);
let remainder =
builder.mul_add_extension(lv[COL_DIV_OUTPUT_REM_1], base, lv[COL_DIV_OUTPUT_REM_0]);
// Temporaries
let divinv = lv[COL_DIV_INVDIVISOR];
let div_divinv = lv[COL_DIV_NONZERO_DIVISOR];
let div_rem_diff_m1 = builder.mul_add_extension(
lv[COL_DIV_RANGE_CHECKED_TMP_1],
base,
lv[COL_DIV_RANGE_CHECKED_TMP_0],
);
// Constraints
let constr6 = builder.mul_sub_extension(divisor, divinv, div_divinv);
let constr7 = {
let t = builder.sub_extension(div_divinv, one);
let u = builder.sub_extension(remainder, quotient);
let v = builder.sub_extension(u, u32_max);
builder.mul_extension(t, v)
};
let constr8 = {
let t = builder.sub_extension(div_divinv, one);
builder.mul_extension(divisor, t)
};
let constr9 = {
let t = builder.sub_extension(remainder, dividend);
builder.mul_add_extension(t, divinv, quotient)
};
let constr10 = {
let t = builder.sub_extension(divisor, remainder);
let u = builder.add_extension(one, div_rem_diff_m1);
let v = builder.sub_extension(t, u);
builder.mul_extension(divisor, v)
};
let constr6 = builder.mul_extension(is_div, constr6);
let constr7 = builder.mul_extension(is_div, constr7);
let constr8 = builder.mul_extension(is_div, constr8);
let constr9 = builder.mul_extension(is_div, constr9);
let constr10 = builder.mul_extension(is_div, constr10);
yield_constr.constraint(builder, constr6);
yield_constr.constraint(builder, constr7);
yield_constr.constraint(builder, constr8);
yield_constr.constraint(builder, constr9);
yield_constr.constraint(builder, constr10);
}
#[cfg(test)]
mod tests {
use plonky2::field::goldilocks_field::GoldilocksField;
use plonky2::field::types::Sample;
use rand::{Rng, SeedableRng};
use rand_chacha::ChaCha8Rng;
use starky::constraint_consumer::ConstraintConsumer;
use super::*;
use crate::registers::NUM_COLUMNS;
#[test]
fn generate_eval_consistency_not_div() {
type F = GoldilocksField;
let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25);
let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng));
// if `IS_DIV == 0`, then the constraints should be met even if all values are garbage.
values[IS_DIV] = F::ZERO;
let mut constrant_consumer = ConstraintConsumer::new(
vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)],
GoldilocksField::ONE,
GoldilocksField::ONE,
GoldilocksField::ONE,
);
eval_division(&values, &mut constrant_consumer);
for &acc in &constrant_consumer.constraint_accs {
assert_eq!(acc, GoldilocksField::ZERO);
}
}
#[test]
fn generate_eval_consistency_div() {
type F = GoldilocksField;
let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25);
let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng));
// set `IS_DIV == 1` and ensure all constraints are satisfied.
values[IS_DIV] = F::ONE;
// set `DIVIDEND` and `DIVISOR` to `u32`s
values[COL_DIV_INPUT_DIVIDEND] = F::from_canonical_u32(rng.gen::<u32>());
values[COL_DIV_INPUT_DIVISOR] = F::from_canonical_u32(rng.gen::<u32>());
generate_division(&mut values);
let mut constrant_consumer = ConstraintConsumer::new(
vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)],
GoldilocksField::ONE,
GoldilocksField::ONE,
GoldilocksField::ONE,
);
eval_division(&values, &mut constrant_consumer);
for &acc in &constrant_consumer.constraint_accs {
assert_eq!(acc, GoldilocksField::ZERO);
}
}
// TODO: test eval_division_recursively.
}

107
system_zero/src/alu/mod.rs
View File

@ -1,107 +0,0 @@
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::{Field, PrimeField64};
use plonky2::hash::hash_types::RichField;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars};
use crate::alu::addition::{eval_addition, eval_addition_circuit, generate_addition};
use crate::alu::bitops::{eval_bitop, eval_bitop_circuit, generate_bitop};
use crate::alu::division::{eval_division, eval_division_circuit, generate_division};
use crate::alu::mul_add::{eval_mul_add, eval_mul_add_circuit, generate_mul_add};
use crate::alu::rotate_shift::{
eval_rotate_left, eval_rotate_left_circuit, eval_rotate_right, eval_rotate_right_circuit,
eval_shift_left, eval_shift_left_circuit, eval_shift_right, eval_shift_right_circuit,
generate_rotate_shift,
};
use crate::alu::subtraction::{eval_subtraction, eval_subtraction_circuit, generate_subtraction};
use crate::public_input_layout::NUM_PUBLIC_INPUTS;
use crate::registers::alu::*;
use crate::registers::NUM_COLUMNS;
mod addition;
mod bitops;
mod canonical;
mod division;
mod mul_add;
mod rotate_shift;
mod subtraction;
pub(crate) fn generate_alu<F: PrimeField64>(values: &mut [F; NUM_COLUMNS]) {
if values[IS_ADD].is_one() {
generate_addition(values);
} else if values[IS_SUB].is_one() {
generate_subtraction(values);
} else if values[IS_MUL_ADD].is_one() {
generate_mul_add(values);
} else if values[IS_DIV].is_one() {
generate_division(values);
} else if values[IS_AND].is_one() {
generate_bitop(values, IS_AND);
} else if values[IS_IOR].is_one() {
generate_bitop(values, IS_IOR);
} else if values[IS_XOR].is_one() {
generate_bitop(values, IS_XOR);
} else if values[IS_ANDNOT].is_one() {
generate_bitop(values, IS_ANDNOT);
} else if values[IS_ROTATE_LEFT].is_one() {
generate_rotate_shift(values, IS_ROTATE_LEFT);
} else if values[IS_ROTATE_RIGHT].is_one() {
generate_rotate_shift(values, IS_ROTATE_RIGHT);
} else if values[IS_SHIFT_LEFT].is_one() {
generate_rotate_shift(values, IS_SHIFT_LEFT);
} else if values[IS_SHIFT_RIGHT].is_one() {
generate_rotate_shift(values, IS_SHIFT_RIGHT);
} else {
//todo!("the requested operation has not yet been implemented");
}
}
pub(crate) fn eval_alu<F: Field, P: PackedField<Scalar = F>>(
vars: StarkEvaluationVars<F, P, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut ConstraintConsumer<P>,
) {
let local_values = &vars.local_values;
// Check that the operation flag values are binary.
for col in ALL_OPERATIONS {
let val = local_values[col];
yield_constr.constraint(val * val - val);
}
eval_addition(local_values, yield_constr);
eval_subtraction(local_values, yield_constr);
eval_mul_add(local_values, yield_constr);
eval_division(local_values, yield_constr);
eval_bitop(local_values, yield_constr);
eval_rotate_left(local_values, yield_constr);
eval_rotate_right(local_values, yield_constr);
eval_shift_left(local_values, yield_constr);
eval_shift_right(local_values, yield_constr);
}
pub(crate) fn eval_alu_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
vars: StarkEvaluationTargets<D, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let local_values = &vars.local_values;
// Check that the operation flag values are binary.
for col in ALL_OPERATIONS {
let val = local_values[col];
let constraint = builder.mul_sub_extension(val, val, val);
yield_constr.constraint(builder, constraint);
}
eval_addition_circuit(builder, local_values, yield_constr);
eval_subtraction_circuit(builder, local_values, yield_constr);
eval_mul_add_circuit(builder, local_values, yield_constr);
eval_division_circuit(builder, local_values, yield_constr);
eval_bitop_circuit(builder, local_values, yield_constr);
eval_rotate_left_circuit(builder, local_values, yield_constr);
eval_rotate_right_circuit(builder, local_values, yield_constr);
eval_shift_left_circuit(builder, local_values, yield_constr);
eval_shift_right_circuit(builder, local_values, yield_constr);
}

91
system_zero/src/alu/mul_add.rs
View File

@ -1,91 +0,0 @@
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::{Field, PrimeField64};
use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use plonky2_util::assume;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::alu::canonical::*;
use crate::registers::alu::*;
use crate::registers::NUM_COLUMNS;
pub(crate) fn generate_mul_add<F: PrimeField64>(values: &mut [F; NUM_COLUMNS]) {
let factor_0 = values[COL_MUL_ADD_FACTOR_0].to_canonical_u64();
let factor_1 = values[COL_MUL_ADD_FACTOR_1].to_canonical_u64();
let addend = values[COL_MUL_ADD_ADDEND].to_canonical_u64();
// Let the compiler know that each input must fit in 32 bits.
assume(factor_0 <= u32::MAX as u64);
assume(factor_1 <= u32::MAX as u64);
assume(addend <= u32::MAX as u64);
let output = factor_0 * factor_1 + addend;
// An advice value used to help verify that the limbs represent a canonical field element.
values[COL_MUL_ADD_RESULT_CANONICAL_INV] = compute_canonical_inv(output);
values[COL_MUL_ADD_OUTPUT_0] = F::from_canonical_u16(output as u16);
values[COL_MUL_ADD_OUTPUT_1] = F::from_canonical_u16((output >> 16) as u16);
values[COL_MUL_ADD_OUTPUT_2] = F::from_canonical_u16((output >> 32) as u16);
values[COL_MUL_ADD_OUTPUT_3] = F::from_canonical_u16((output >> 48) as u16);
}
pub(crate) fn eval_mul_add<F: Field, P: PackedField<Scalar = F>>(
local_values: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
) {
let is_mul = local_values[IS_MUL_ADD];
let factor_0 = local_values[COL_MUL_ADD_FACTOR_0];
let factor_1 = local_values[COL_MUL_ADD_FACTOR_1];
let addend = local_values[COL_MUL_ADD_ADDEND];
let output_1 = local_values[COL_MUL_ADD_OUTPUT_0];
let output_2 = local_values[COL_MUL_ADD_OUTPUT_1];
let output_3 = local_values[COL_MUL_ADD_OUTPUT_2];
let output_4 = local_values[COL_MUL_ADD_OUTPUT_3];
let result_canonical_inv = local_values[COL_MUL_ADD_RESULT_CANONICAL_INV];
let computed_output = factor_0 * factor_1 + addend;
// TODO: Needs to be filtered by IS_MUL_ADD.
let output = combine_u16s_check_canonical(
output_1,
output_2,
output_3,
output_4,
result_canonical_inv,
yield_constr,
);
yield_constr.constraint(is_mul * (computed_output - output));
}
pub(crate) fn eval_mul_add_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
local_values: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let is_mul = local_values[IS_MUL_ADD];
let factor_0 = local_values[COL_MUL_ADD_FACTOR_0];
let factor_1 = local_values[COL_MUL_ADD_FACTOR_1];
let addend = local_values[COL_MUL_ADD_ADDEND];
let output_1 = local_values[COL_MUL_ADD_OUTPUT_0];
let output_2 = local_values[COL_MUL_ADD_OUTPUT_1];
let output_3 = local_values[COL_MUL_ADD_OUTPUT_2];
let output_4 = local_values[COL_MUL_ADD_OUTPUT_3];
let result_canonical_inv = local_values[COL_MUL_ADD_RESULT_CANONICAL_INV];
let computed_output = builder.mul_add_extension(factor_0, factor_1, addend);
// TODO: Needs to be filtered by IS_MUL_ADD.
let output = combine_u16s_check_canonical_circuit(
builder,
output_1,
output_2,
output_3,
output_4,
result_canonical_inv,
yield_constr,
);
let diff = builder.sub_extension(computed_output, output);
let filtered_diff = builder.mul_extension(is_mul, diff);
yield_constr.constraint(builder, filtered_diff);
}

645
system_zero/src/alu/rotate_shift.rs
View File

@ -1,645 +0,0 @@
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::{Field, PrimeField64};
use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::alu::bitops::constrain_all_to_bits_circuit;
use crate::registers::alu::*;
use crate::registers::NUM_COLUMNS;
/// ROTATE and SHIFT instructions
///
/// To rotate a 64bit value by DELTA bit positions, the input is
///
/// - a 64-bit integer X to be rotated/shifted, given as high and low 32-bit
/// words X_lo and X_hi.
/// - a 32-bit integer EXP (given as its 5 bits) which is either DELTA
/// mod 32, if the operation direction is left, or (32 - (DELTA mod 32))
/// mod 32 if the operation direction is right.
/// - a single bit DELTA_DIV32 which is 1 if DELTA is >= 32 and 0 otherwise
/// - the value POW_EXP = 2^EXP, as well as three auxiliary values POW_EXP_AUX_[012]
/// to verify that POW_EXP == 2^EXP
/// - two 64-bit integers, INPUT_LO_DISPLACED and INPUT_HI_DISPLACED,
/// with INPUT_LO_DISPLACED being the high and low 32-bit words of
/// the value 2^EXP * X_lo; similarly for INPUT_HI_DISPLACED.
/// - two 64-bit auxiliary values DISPLACED_INPUT_{LO,HI}_AUX, one
/// each for INPUT_LO_DISPLACED and INPUT_HI_DISPLACED, used to prove
/// that INPUT_LO_DISPLACED and INPUT_HI_DISPLACED are valid
/// Goldilocks elements.
pub(crate) fn generate_rotate_shift<F: PrimeField64>(values: &mut [F; NUM_COLUMNS], op: usize) {
// input_{lo,hi} are the 32-bit lo and hi words of the input
let input_lo = values[COL_ROTATE_SHIFT_INPUT_LO].to_canonical_u64();
let input_hi = values[COL_ROTATE_SHIFT_INPUT_HI].to_canonical_u64();
// Given the 6 bits delta_bits[0..5], bits 0..4 represent
// delta_mod32 for left ops and (32 - delta_mod32) % 32 for right
// ops, and delta_bits[5] represents whether delta >= 32.
// delta is the displacement amount. EXP_BITS holds the 5 bits of
// either delta mod 32 (for left ops) or (32 - (delta mod 32)) mod 32
// for right ops.
let exp_bits = COL_ROTATE_SHIFT_EXP_BITS.map(|r| values[r].to_canonical_u64());
let is_right_op = op == IS_ROTATE_RIGHT || op == IS_SHIFT_RIGHT || op == IS_ARITH_SHIFT_RIGHT;
let exp: u64 = [0, 1, 2, 3, 4].map(|i| exp_bits[i] << i).into_iter().sum();
let delta_mod32 = if is_right_op { (32u64 - exp) % 32 } else { exp };
let exp_ge32_bit = values[COL_ROTATE_SHIFT_DELTA_DIV32].to_canonical_u64();
let delta = (exp_ge32_bit << 5) + delta_mod32;
// helper values
let pow_exp_aux_0 = (exp_bits[0] + 1) * (3 * exp_bits[1] + 1);
let pow_exp_aux_1 = (15 * exp_bits[2] + 1) * (255 * exp_bits[3] + 1);
let pow_exp_aux_2 = pow_exp_aux_0 * pow_exp_aux_1;
let pow_exp = pow_exp_aux_2 * (65535 * exp_bits[4] + 1);
values[COL_ROTATE_SHIFT_POW_EXP_AUX_0] = F::from_canonical_u64(pow_exp_aux_0);
values[COL_ROTATE_SHIFT_POW_EXP_AUX_1] = F::from_canonical_u64(pow_exp_aux_1);
values[COL_ROTATE_SHIFT_POW_EXP_AUX_2] = F::from_canonical_u64(pow_exp_aux_2);
values[COL_ROTATE_SHIFT_POW_EXP] = F::from_canonical_u64(pow_exp);
let lo_shifted = input_lo << exp;
let lo_shifted_0 = lo_shifted as u32;
let lo_shifted_1 = (lo_shifted >> 32) as u32;
values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0] = F::from_canonical_u32(lo_shifted_0);
values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1] = F::from_canonical_u32(lo_shifted_1);
let hi_shifted = input_hi << exp;
let hi_shifted_0 = hi_shifted as u32;
let hi_shifted_1 = (hi_shifted >> 32) as u32;
values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0] = F::from_canonical_u32(hi_shifted_0);
values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1] = F::from_canonical_u32(hi_shifted_1);
if lo_shifted_1 != u32::MAX {
let diff = F::from_canonical_u32(u32::MAX - lo_shifted_1);
let inv = diff.inverse();
values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0] = inv;
values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1] = diff * inv;
} else {
// lo_shifted_0 must be zero, so this is unused.
values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0] = F::ZERO;
values[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1] = F::ZERO;
}
if hi_shifted_1 != u32::MAX {
let diff = F::from_canonical_u32(u32::MAX - hi_shifted_1);
let inv = diff.inverse();
values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0] = inv;
values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1] = diff * inv;
} else {
// hi_shifted_0 must be zero, so this is unused.
values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0] = F::ZERO;
values[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1] = F::ZERO;
}
// the input and output as u64s
let input = (input_hi << 32) | input_lo;
let delta = delta as u32;
let output = match op {
IS_ROTATE_LEFT => input.rotate_left(delta),
IS_ROTATE_RIGHT => input.rotate_right(delta),
IS_SHIFT_LEFT => input << delta,
IS_SHIFT_RIGHT => input >> delta,
IS_ARITH_SHIFT_RIGHT => (input as i64 >> delta) as u64,
_ => panic!("unrecognized rotate/shift instruction code"),
};
// Output in base 2^16.
values[COL_ROTATE_SHIFT_OUTPUT_0] = F::from_canonical_u32(output as u32);
values[COL_ROTATE_SHIFT_OUTPUT_1] = F::from_canonical_u32((output >> 32) as u32);
}
/// Check that pow_exp = 2^exp, where exp is formed from the bits
/// exp_bits[0..4].
///
/// 2^exp = \prod_i=0^4 (2^(2^i) if exp_bits[i] = 1 else 1)
/// = \prod_i=0^4 ((2^(2^i) - 1) * exp_bits[i] + 1)
/// = pow_exp
///
/// on the conditions that:
///
/// pow_exp_aux_0 = \prod_i=0^1 ((2^i - 1) * exp_bits[i] + 1)
/// pow_exp_aux_1 = \prod_i=2^3 ((2^i - 1) * exp_bits[i] + 1)
/// pow_exp_aux_2 = pow_exp_aux_0 * pow_exp_aux_1
/// pow_exp_mod32 = pow_exp_aux_2 * ((2^(2^4) - 1) * exp_bits[4] + 1)
///
/// Also check that every "bit" of exp_bits and exp_ge32_bit is 0 or 1.
fn constrain_pow_exp<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
filter: P,
) {
let exp_bits = COL_ROTATE_SHIFT_EXP_BITS.map(|r| lv[r]);
let exp_ge32_bit = lv[COL_ROTATE_SHIFT_DELTA_DIV32];
let pow_exp_aux_0 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_0];
let pow_exp_aux_1 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_1];
let pow_exp_aux_2 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_2];
let pow_exp = lv[COL_ROTATE_SHIFT_POW_EXP];
// Check that every "bit" of exp_bits and exp_ge32_bit is 0 or 1
exp_bits.map(|b| yield_constr.constraint(filter * (b * b - b)));
yield_constr.constraint(filter * (exp_ge32_bit * exp_ge32_bit - exp_ge32_bit));
// c[i-1] = 2^(2^i) - 1
let c = [1, 2, 3, 4].map(|i| P::from(F::from_canonical_u64(1u64 << (1u32 << i))) - P::ONES);
let constr1 = (exp_bits[0] + P::ONES) * (c[0] * exp_bits[1] + P::ONES);
yield_constr.constraint(filter * (constr1 - pow_exp_aux_0));
let constr2 = (c[1] * exp_bits[2] + P::ONES) * (c[2] * exp_bits[3] + P::ONES);
yield_constr.constraint(filter * (constr2 - pow_exp_aux_1));
let constr3 = pow_exp_aux_0 * pow_exp_aux_1;
yield_constr.constraint(filter * (constr3 - pow_exp_aux_2));
let constr4 = pow_exp_aux_2 * (c[3] * exp_bits[4] + P::ONES);
yield_constr.constraint(filter * (constr4 - pow_exp));
}
/// An invalid lo_shifted (or _hi) can be too big to fit in Goldilocks
/// field; e.g. if both _0 and _1 parts are 2^32-1, then lo_shifted =
/// 2^32 - 1 + 2^32 (2^32 - 1) = 2^64 - 1 which overflows in
/// GoldilocksField. Hence we check that {lo,hi}_shifted are valid
/// Goldilocks elements following
/// https:///hackmd.io/NC-yRmmtRQSvToTHb96e8Q#Checking-element-validity
///
/// The idea is check that a value v = (v_lo, v_hi) (32-bit words)
/// satisfies the condition (v_lo == 0 OR v_hi != 2^32-1), which uses
/// the structure of Goldilocks to check that v has the right form.
/// The formula is:
/// v_lo * (one - aux * (u32_max - v_hi)) == 0
/// where aux = (m32_max - v_hi)^-1 if it exists.
fn constrain_shifted_are_valid<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
filter: P,
) {
let lo_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0];
let lo_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1];
let hi_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0];
let hi_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1];
let lo_shifted_aux_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0];
let lo_shifted_aux_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1];
let hi_shifted_aux_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0];
let hi_shifted_aux_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1];
// u32_max = 2^32 - 1
let u32_max = P::from(F::from_canonical_u32(u32::MAX));
let constr1 = lo_shifted_aux_0 * (u32_max - lo_shifted_1);
yield_constr.constraint(filter * (constr1 - lo_shifted_aux_1));
let constr2 = hi_shifted_aux_0 * (u32_max - hi_shifted_1);
yield_constr.constraint(filter * (constr2 - hi_shifted_aux_1));
let lo_shifted_is_valid = lo_shifted_0 * (P::ONES - lo_shifted_aux_1);
let hi_shifted_is_valid = hi_shifted_0 * (P::ONES - hi_shifted_aux_1);
yield_constr.constraint(filter * lo_shifted_is_valid);
yield_constr.constraint(filter * hi_shifted_is_valid);
}
fn eval_rotate_shift<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
filter: P,
) -> (P, P, P, P, P, P, P) {
// Input
let input_lo = lv[COL_ROTATE_SHIFT_INPUT_LO];
let input_hi = lv[COL_ROTATE_SHIFT_INPUT_HI];
// Delta is the shift/rotate displacement; exp is delta mod 32 or
// (32 - (delta mod 32)) mod 32, depending on whether the operation
// direction is left or right.
let exp_ge32_bit = lv[COL_ROTATE_SHIFT_DELTA_DIV32];
let pow_exp = lv[COL_ROTATE_SHIFT_POW_EXP];
let lo_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0];
let lo_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1];
let hi_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0];
let hi_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1];
// Output
let output_lo = lv[COL_ROTATE_SHIFT_OUTPUT_0];
let output_hi = lv[COL_ROTATE_SHIFT_OUTPUT_1];
constrain_pow_exp(lv, yield_constr, filter);
constrain_shifted_are_valid(lv, yield_constr, filter);
// Check
// 2^exp * input_lo == lo_shifted_0 + 2^32 * lo_shifted_1
// 2^exp * input_hi == hi_shifted_0 + 2^32 * hi_shifted_1
let base = F::from_canonical_u64(1u64 << 32);
let lo_shifted = lo_shifted_0 + lo_shifted_1 * base;
let hi_shifted = hi_shifted_0 + hi_shifted_1 * base;
// exp must be <= 32 for this to never overflow in
// GoldilocksField: since 0 <= input_{lo,hi} <= 2^32 - 1,
// input_{lo,hi} * 2^32 <= 2^64 - 2^32 < 2^64 - 2^32 + 1 = Goldilocks.
let lo_shifted_expected = input_lo * pow_exp;
let hi_shifted_expected = input_hi * pow_exp;
yield_constr.constraint(filter * (lo_shifted_expected - lo_shifted));
yield_constr.constraint(filter * (hi_shifted_expected - hi_shifted));
(
exp_ge32_bit,
lo_shifted_0,
lo_shifted_1,
hi_shifted_0,
hi_shifted_1,
output_lo,
output_hi,
)
}
pub(crate) fn eval_rotate_left<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
) {
let is_rol = lv[IS_ROTATE_LEFT];
let one = P::ONES;
let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) =
eval_rotate_shift(lv, yield_constr, is_rol);
// Intuitively we want to do this (which works when delta <= 32):
//let lo_constr = hi_shifted_1 + lo_shifted_0 - output_lo;
//let hi_constr = lo_shifted_1 + hi_shifted_0 - output_hi;
// If delta_bits[5] == 0, then delta < 32, so we use the bottom term.
// Otherwise delta_bits[5] == 1, so 32 <= delta < 64 and we need
// to swap the constraints for the hi and lo halves; hence we use
// the bottom term which is the top term from hi_constr.
let lo_constr = (one - delta_ge32) * (hi_shifted_1 + lo_shifted_0 - output_lo)
+ delta_ge32 * (lo_shifted_1 + hi_shifted_0 - output_lo);
let hi_constr = (one - delta_ge32) * (lo_shifted_1 + hi_shifted_0 - output_hi)
+ delta_ge32 * (hi_shifted_1 + lo_shifted_0 - output_hi);
yield_constr.constraint(is_rol * lo_constr);
yield_constr.constraint(is_rol * hi_constr);
}
pub(crate) fn eval_rotate_right<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
) {
let is_ror = lv[IS_ROTATE_RIGHT];
let one = P::ONES;
let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) =
eval_rotate_shift(lv, yield_constr, is_ror);
// Intuitively we want to do this (which works when delta <= 32):
// let lo_constr = lo_shifted_1 + hi_shifted_0 - output_lo;
// let hi_constr = hi_shifted_1 + lo_shifted_0 - output_hi;
let lo_constr = (one - delta_ge32) * (lo_shifted_1 + hi_shifted_0 - output_lo)
+ delta_ge32 * (hi_shifted_1 + lo_shifted_0 - output_lo);
let hi_constr = (one - delta_ge32) * (hi_shifted_1 + lo_shifted_0 - output_hi)
+ delta_ge32 * (lo_shifted_1 + hi_shifted_0 - output_hi);
yield_constr.constraint(is_ror * lo_constr);
yield_constr.constraint(is_ror * hi_constr);
}
pub(crate) fn eval_shift_left<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
) {
let is_shl = lv[IS_SHIFT_LEFT];
let one = P::ONES;
let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, _hi_shifted_1, output_lo, output_hi) =
eval_rotate_shift(lv, yield_constr, is_shl);
// Intuitively we want to do this (which works when delta <= 32):
//let lo_constr = lo_shifted_0 - output_lo;
//let hi_constr = lo_shifted_1 + hi_shifted_0 - output_hi;
let lo_constr =
(one - delta_ge32) * (lo_shifted_0 - output_lo) + delta_ge32 * (P::ZEROS - output_lo);
let hi_constr = (one - delta_ge32) * (lo_shifted_1 + hi_shifted_0 - output_hi)
+ delta_ge32 * (lo_shifted_0 - output_hi);
yield_constr.constraint(is_shl * lo_constr);
yield_constr.constraint(is_shl * hi_constr);
}
pub(crate) fn eval_shift_right<F: Field, P: PackedField<Scalar = F>>(
lv: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
) {
let is_shl = lv[IS_SHIFT_LEFT];
let one = P::ONES;
let (delta_ge32, _lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) =
eval_rotate_shift(lv, yield_constr, is_shl);
// Intuitively we want to do this (which works when delta <= 32):
//let lo_constr = lo_shifted_1 + hi_shifted_0 - output_hi;
//let hi_constr = hi_shifted_1 - output_lo;
let lo_constr = (one - delta_ge32) * (lo_shifted_1 + hi_shifted_0 - output_lo)
+ delta_ge32 * (hi_shifted_1 - output_lo);
let hi_constr =
(one - delta_ge32) * (hi_shifted_1 - output_hi) + delta_ge32 * (P::ZEROS - output_hi);
yield_constr.constraint(is_shl * lo_constr);
yield_constr.constraint(is_shl * hi_constr);
}
fn constrain_pow_exp_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
filter: ExtensionTarget<D>,
) {
let exp_bits = COL_ROTATE_SHIFT_EXP_BITS.map(|r| lv[r]);
let exp_ge32_bit = lv[COL_ROTATE_SHIFT_DELTA_DIV32];
let pow_exp_aux_0 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_0];
let pow_exp_aux_1 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_1];
let pow_exp_aux_2 = lv[COL_ROTATE_SHIFT_POW_EXP_AUX_2];
let pow_exp = lv[COL_ROTATE_SHIFT_POW_EXP];
// Check that every "bit" of exp_bits and exp_ge32_bit is 0 or 1
constrain_all_to_bits_circuit(builder, yield_constr, filter, &exp_bits);
constrain_all_to_bits_circuit(builder, yield_constr, filter, &[exp_ge32_bit]);
let one = builder.one_extension();
// c[i-1] = 2^(2^i) - 1
let c = [1, 2, 3, 4].map(|i| F::from_canonical_u64(1u64 << (1u32 << i)) - F::ONE);
let constr1 = {
let t0 = builder.add_extension(exp_bits[0], one);
let t1 = builder.mul_const_add_extension(c[0], exp_bits[1], one);
let t2 = builder.mul_sub_extension(t0, t1, pow_exp_aux_0);
builder.mul_extension(filter, t2)
};
yield_constr.constraint(builder, constr1);
let constr2 = {
let t0 = builder.mul_const_add_extension(c[1], exp_bits[2], one);
let t1 = builder.mul_const_add_extension(c[2], exp_bits[3], one);
let t2 = builder.mul_sub_extension(t0, t1, pow_exp_aux_1);
builder.mul_extension(filter, t2)
};
yield_constr.constraint(builder, constr2);
let constr3 = {
let t0 = builder.mul_sub_extension(pow_exp_aux_0, pow_exp_aux_1, pow_exp_aux_2);
builder.mul_extension(filter, t0)
};
yield_constr.constraint(builder, constr3);
let constr4 = {
let t0 = builder.mul_const_add_extension(c[3], exp_bits[4], one);
let t1 = builder.mul_sub_extension(pow_exp_aux_2, t0, pow_exp);
builder.mul_extension(filter, t1)
};
yield_constr.constraint(builder, constr4);
}
fn constrain_shifted_are_valid_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
filter: ExtensionTarget<D>,
) {
let lo_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0];
let lo_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1];
let hi_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0];
let hi_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1];
let lo_shifted_aux_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0];
let lo_shifted_aux_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1];
let hi_shifted_aux_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0];
let hi_shifted_aux_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1];
let one = builder.one_extension();
let u32_max = builder.constant_extension(F::Extension::from_canonical_u32(u32::MAX));
let constr1 = {
let t0 = builder.sub_extension(u32_max, lo_shifted_1);
let t1 = builder.mul_sub_extension(lo_shifted_aux_0, t0, lo_shifted_aux_1);
builder.mul_extension(filter, t1)
};
yield_constr.constraint(builder, constr1);
let constr2 = {
let t0 = builder.sub_extension(u32_max, hi_shifted_1);
let t1 = builder.mul_sub_extension(hi_shifted_aux_0, t0, hi_shifted_aux_1);
builder.mul_extension(filter, t1)
};
yield_constr.constraint(builder, constr2);
let lo_shifted_is_valid = {
let t0 = builder.sub_extension(one, lo_shifted_aux_1);
let t1 = builder.mul_extension(t0, lo_shifted_0);
builder.mul_extension(filter, t1)
};
let hi_shifted_is_valid = {
let t0 = builder.sub_extension(one, hi_shifted_aux_1);
let t1 = builder.mul_extension(t0, hi_shifted_0);
builder.mul_extension(filter, t1)
};
yield_constr.constraint(builder, lo_shifted_is_valid);
yield_constr.constraint(builder, hi_shifted_is_valid);
}
fn eval_rotate_shift_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
filter: ExtensionTarget<D>,
) -> (
ExtensionTarget<D>,
ExtensionTarget<D>,
ExtensionTarget<D>,
ExtensionTarget<D>,
ExtensionTarget<D>,
ExtensionTarget<D>,
ExtensionTarget<D>,
) {
// Input
let input_lo = lv[COL_ROTATE_SHIFT_INPUT_LO];
let input_hi = lv[COL_ROTATE_SHIFT_INPUT_HI];
let exp_ge32_bit = lv[COL_ROTATE_SHIFT_DELTA_DIV32];
let pow_exp = lv[COL_ROTATE_SHIFT_POW_EXP];
let lo_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0];
let lo_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1];
let hi_shifted_0 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0];
let hi_shifted_1 = lv[COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1];
// Output
let output_lo = lv[COL_ROTATE_SHIFT_OUTPUT_0];
let output_hi = lv[COL_ROTATE_SHIFT_OUTPUT_1];
constrain_pow_exp_circuit(builder, lv, yield_constr, filter);
constrain_shifted_are_valid_circuit(builder, lv, yield_constr, filter);
let base = builder.constant_extension(F::Extension::from_canonical_u64(1u64 << 32));
let lo_shifted = builder.mul_add_extension(lo_shifted_1, base, lo_shifted_0);
let hi_shifted = builder.mul_add_extension(hi_shifted_1, base, hi_shifted_0);
let lo_shifted_expected = builder.mul_extension(input_lo, pow_exp);
let hi_shifted_expected = builder.mul_extension(input_hi, pow_exp);
let lo_shifted_valid = {
let t0 = builder.sub_extension(lo_shifted_expected, lo_shifted);
builder.mul_extension(filter, t0)
};
yield_constr.constraint(builder, lo_shifted_valid);
let hi_shifted_valid = {
let t0 = builder.sub_extension(hi_shifted_expected, hi_shifted);
builder.mul_extension(filter, t0)
};
yield_constr.constraint(builder, hi_shifted_valid);
(
exp_ge32_bit,
lo_shifted_0,
lo_shifted_1,
hi_shifted_0,
hi_shifted_1,
output_lo,
output_hi,
)
}
pub(crate) fn eval_rotate_left_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let is_rol = lv[IS_ROTATE_LEFT];
let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) =
eval_rotate_shift_circuit(builder, lv, yield_constr, is_rol);
let one = builder.one_extension();
let s0 = builder.add_extension(hi_shifted_1, lo_shifted_0);
let s1 = builder.add_extension(lo_shifted_1, hi_shifted_0);
let c = builder.sub_extension(one, delta_ge32);
let lo_constr = {
let t0 = builder.sub_extension(s0, output_lo);
let t1 = builder.mul_extension(c, t0);
let t2 = builder.sub_extension(s1, output_lo);
let t3 = builder.mul_extension(delta_ge32, t2);
let t4 = builder.add_extension(t1, t3);
builder.mul_extension(is_rol, t4)
};
let hi_constr = {
let t0 = builder.sub_extension(s1, output_hi);
let t1 = builder.mul_extension(c, t0);
let t2 = builder.sub_extension(s0, output_hi);
let t3 = builder.mul_extension(delta_ge32, t2);
let t4 = builder.add_extension(t1, t3);
builder.mul_extension(is_rol, t4)
};
yield_constr.constraint(builder, lo_constr);
yield_constr.constraint(builder, hi_constr);
}
pub(crate) fn eval_rotate_right_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let is_ror = lv[IS_ROTATE_RIGHT];
let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) =
eval_rotate_shift_circuit(builder, lv, yield_constr, is_ror);
let one = builder.one_extension();
let s0 = builder.add_extension(hi_shifted_1, lo_shifted_0);
let s1 = builder.add_extension(lo_shifted_1, hi_shifted_0);
let c = builder.sub_extension(one, delta_ge32);
let lo_constr = {
let t0 = builder.sub_extension(s1, output_lo);
let t1 = builder.mul_extension(c, t0);
let t2 = builder.sub_extension(s0, output_lo);
let t3 = builder.mul_extension(delta_ge32, t2);
let t4 = builder.add_extension(t1, t3);
builder.mul_extension(is_ror, t4)
};
let hi_constr = {
let t0 = builder.sub_extension(s0, output_hi);
let t1 = builder.mul_extension(c, t0);
let t2 = builder.sub_extension(s1, output_hi);
let t3 = builder.mul_extension(delta_ge32, t2);
let t4 = builder.add_extension(t1, t3);
builder.mul_extension(is_ror, t4)
};
yield_constr.constraint(builder, lo_constr);
yield_constr.constraint(builder, hi_constr);
}
pub(crate) fn eval_shift_left_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let is_shl = lv[IS_SHIFT_LEFT];
let (delta_ge32, lo_shifted_0, lo_shifted_1, hi_shifted_0, _hi_shifted_1, output_lo, output_hi) =
eval_rotate_shift_circuit(builder, lv, yield_constr, is_shl);
let one = builder.one_extension();
let c = builder.sub_extension(one, delta_ge32);
let lo_constr = {
let t0 = builder.sub_extension(lo_shifted_0, output_lo);
let t1 = builder.mul_extension(c, t0);
let t2 = builder.mul_extension(delta_ge32, output_lo);
let t3 = builder.add_extension(t1, t2);
builder.mul_extension(is_shl, t3)
};
let hi_constr = {
let t0 = builder.add_extension(lo_shifted_1, hi_shifted_0);
let t1 = builder.sub_extension(t0, output_hi);
let t2 = builder.mul_extension(c, t1);
let t3 = builder.sub_extension(lo_shifted_0, output_hi);
let t4 = builder.mul_extension(delta_ge32, t3);
let t5 = builder.add_extension(t2, t4);
builder.mul_extension(is_shl, t5)
};
yield_constr.constraint(builder, lo_constr);
yield_constr.constraint(builder, hi_constr);
}
pub(crate) fn eval_shift_right_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
lv: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let is_shr = lv[IS_SHIFT_RIGHT];
let (delta_ge32, _lo_shifted_0, lo_shifted_1, hi_shifted_0, hi_shifted_1, output_lo, output_hi) =
eval_rotate_shift_circuit(builder, lv, yield_constr, is_shr);
let one = builder.one_extension();
let c = builder.sub_extension(one, delta_ge32);
let lo_constr = {
let t0 = builder.add_extension(lo_shifted_1, hi_shifted_0);
let t1 = builder.sub_extension(t0, output_lo);
let t2 = builder.mul_extension(c, t1);
let t3 = builder.sub_extension(hi_shifted_1, output_lo);
let t4 = builder.mul_extension(delta_ge32, t3);
let t5 = builder.add_extension(t2, t4);
builder.mul_extension(is_shr, t5)
};
let hi_constr = {
let t0 = builder.sub_extension(hi_shifted_1, output_hi);
let t1 = builder.mul_extension(c, t0);
let t2 = builder.mul_extension(delta_ge32, output_hi);
let t3 = builder.add_extension(t1, t2);
builder.mul_extension(is_shr, t3)
};
yield_constr.constraint(builder, lo_constr);
yield_constr.constraint(builder, hi_constr);
}

76
system_zero/src/alu/subtraction.rs
View File

@ -1,76 +0,0 @@
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::{Field, PrimeField64};
use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::registers::alu::*;
use crate::registers::NUM_COLUMNS;
pub(crate) fn generate_subtraction<F: PrimeField64>(values: &mut [F; NUM_COLUMNS]) {
let in_1 = values[COL_SUB_INPUT_0].to_canonical_u64() as u32;
let in_2 = values[COL_SUB_INPUT_1].to_canonical_u64() as u32;
// in_1 - in_2 == diff - br*2^32
let (diff, br) = in_1.overflowing_sub(in_2);
values[COL_SUB_OUTPUT_0] = F::from_canonical_u16(diff as u16);
values[COL_SUB_OUTPUT_1] = F::from_canonical_u16((diff >> 16) as u16);
values[COL_SUB_OUTPUT_BORROW] = F::from_bool(br);
}
pub(crate) fn eval_subtraction<F: Field, P: PackedField<Scalar = F>>(
local_values: &[P; NUM_COLUMNS],
yield_constr: &mut ConstraintConsumer<P>,
) {
let is_sub = local_values[IS_SUB];
let in_1 = local_values[COL_SUB_INPUT_0];
let in_2 = local_values[COL_SUB_INPUT_1];
let out_1 = local_values[COL_SUB_OUTPUT_0];
let out_2 = local_values[COL_SUB_OUTPUT_1];
let out_br = local_values[COL_SUB_OUTPUT_BORROW];
let base = F::from_canonical_u64(1 << 16);
let base_sqr = F::from_canonical_u64(1 << 32);
let out_br = out_br * base_sqr;
let lhs = (out_br + in_1) - in_2;
let rhs = out_1 + out_2 * base;
yield_constr.constraint(is_sub * (lhs - rhs));
// We don't need to check that out_br is in {0, 1} because it's
// checked by boolean::col_bit(0) in the ALU.
}
pub(crate) fn eval_subtraction_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
local_values: &[ExtensionTarget<D>; NUM_COLUMNS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let is_sub = local_values[IS_SUB];
let in_1 = local_values[COL_SUB_INPUT_0];
let in_2 = local_values[COL_SUB_INPUT_1];
let out_1 = local_values[COL_SUB_OUTPUT_0];
let out_2 = local_values[COL_SUB_OUTPUT_1];
let out_br = local_values[COL_SUB_OUTPUT_BORROW];
let base = builder.constant_extension(F::Extension::from_canonical_u64(1 << 16));
#[allow(unused)] // TODO
let base_sqr = builder.constant_extension(F::Extension::from_canonical_u64(1 << 32));
// lhs = (out_br + in_1) - in_2
let lhs = builder.add_extension(out_br, in_1);
let lhs = builder.sub_extension(lhs, in_2);
// rhs = out_1 + base * out_2
let rhs = builder.mul_add_extension(out_2, base, out_1);
// filtered_diff = is_sub * (lhs - rhs)
let diff = builder.sub_extension(lhs, rhs);
let filtered_diff = builder.mul_extension(is_sub, diff);
yield_constr.constraint(builder, filtered_diff);
}

92
system_zero/src/core_registers.rs
View File

@ -1,92 +0,0 @@
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::{Field, PrimeField64};
use plonky2::hash::hash_types::RichField;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars};
use crate::public_input_layout::NUM_PUBLIC_INPUTS;
use crate::registers::core::*;
use crate::registers::NUM_COLUMNS;
pub(crate) fn generate_first_row_core_registers<F: Field>(first_values: &mut [F; NUM_COLUMNS]) {
first_values[COL_CLOCK] = F::ZERO;
first_values[COL_RANGE_16] = F::ZERO;
first_values[COL_INSTRUCTION_PTR] = F::ZERO;
first_values[COL_FRAME_PTR] = F::ZERO;
first_values[COL_STACK_PTR] = F::ZERO;
}
pub(crate) fn generate_next_row_core_registers<F: PrimeField64>(
local_values: &[F; NUM_COLUMNS],
next_values: &mut [F; NUM_COLUMNS],
) {
// We increment the clock by 1.
next_values[COL_CLOCK] = local_values[COL_CLOCK] + F::ONE;
// We increment the 16-bit table by 1, unless we've reached the max value of 2^16 - 1, in
// which case we repeat that value.
let prev_range_16 = local_values[COL_RANGE_16].to_canonical_u64();
let next_range_16 = (prev_range_16 + 1).min((1 << 16) - 1);
next_values[COL_RANGE_16] = F::from_canonical_u64(next_range_16);
// next_values[COL_INSTRUCTION_PTR] = todo!();
// next_values[COL_FRAME_PTR] = todo!();
// next_values[COL_STACK_PTR] = todo!();
}
#[inline]
pub(crate) fn eval_core_registers<F: Field, P: PackedField<Scalar = F>>(
vars: StarkEvaluationVars<F, P, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut ConstraintConsumer<P>,
) {
// The clock must start with 0, and increment by 1.
let local_clock = vars.local_values[COL_CLOCK];
let next_clock = vars.next_values[COL_CLOCK];
let delta_clock = next_clock - local_clock;
yield_constr.constraint_first_row(local_clock);
yield_constr.constraint_transition(delta_clock - F::ONE);
// The 16-bit table must start with 0, end with 2^16 - 1, and increment by 0 or 1.
let local_range_16 = vars.local_values[COL_RANGE_16];
let next_range_16 = vars.next_values[COL_RANGE_16];
let delta_range_16 = next_range_16 - local_range_16;
yield_constr.constraint_first_row(local_range_16);
yield_constr.constraint_last_row(local_range_16 - F::from_canonical_u64((1 << 16) - 1));
yield_constr.constraint_transition(delta_range_16 * delta_range_16 - delta_range_16);
// TODO constraints for stack etc.
}
pub(crate) fn eval_core_registers_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
vars: StarkEvaluationTargets<D, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let one_ext = builder.one_extension();
let max_u16 = builder.constant(F::from_canonical_u64((1 << 16) - 1));
let max_u16_ext = builder.convert_to_ext(max_u16);
// The clock must start with 0, and increment by 1.
let local_clock = vars.local_values[COL_CLOCK];
let next_clock = vars.next_values[COL_CLOCK];
let delta_clock = builder.sub_extension(next_clock, local_clock);
yield_constr.constraint_first_row(builder, local_clock);
let constraint = builder.sub_extension(delta_clock, one_ext);
yield_constr.constraint_transition(builder, constraint);
// The 16-bit table must start with 0, end with 2^16 - 1, and increment by 0 or 1.
let local_range_16 = vars.local_values[COL_RANGE_16];
let next_range_16 = vars.next_values[COL_RANGE_16];
let delta_range_16 = builder.sub_extension(next_range_16, local_range_16);
yield_constr.constraint_first_row(builder, local_range_16);
let constraint = builder.sub_extension(local_range_16, max_u16_ext);
yield_constr.constraint_last_row(builder, constraint);
let constraint = builder.mul_add_extension(delta_range_16, delta_range_16, delta_range_16);
yield_constr.constraint_transition(builder, constraint);
// TODO constraints for stack etc.
}

10
system_zero/src/lib.rs
View File

@ -1,10 +0,0 @@
#![feature(array_zip)]
mod alu;
mod core_registers;
pub mod lookup;
mod memory;
mod permutation_unit;
mod public_input_layout;
mod registers;
pub mod system_zero;

146
system_zero/src/lookup.rs
View File

@ -1,146 +0,0 @@
//! Implementation of the Halo2 lookup argument.
//!
//! References:
//! - https://zcash.github.io/halo2/design/proving-system/lookup.html
//! - https://www.youtube.com/watch?v=YlTt12s7vGE&t=5237s
use std::cmp::Ordering;
use itertools::Itertools;
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
use plonky2::field::types::{Field, PrimeField64};
use plonky2::hash::hash_types::RichField;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars};
use crate::public_input_layout::NUM_PUBLIC_INPUTS;
use crate::registers::lookup::*;
use crate::registers::NUM_COLUMNS;
pub(crate) fn generate_lookups<F: PrimeField64>(trace_cols: &mut [Vec<F>]) {
for i in 0..NUM_LOOKUPS {
let inputs = &trace_cols[col_input(i)];
let table = &trace_cols[col_table(i)];
let (permuted_inputs, permuted_table) = permuted_cols(inputs, table);
trace_cols[col_permuted_input(i)] = permuted_inputs;
trace_cols[col_permuted_table(i)] = permuted_table;
}
}
/// 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)
}
pub(crate) fn eval_lookups<F: Field, P: PackedField<Scalar = F>>(
vars: StarkEvaluationVars<F, P, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut ConstraintConsumer<P>,
) {
for i in 0..NUM_LOOKUPS {
let local_perm_input = vars.local_values[col_permuted_input(i)];
let next_perm_table = vars.next_values[col_permuted_table(i)];
let next_perm_input = vars.next_values[col_permuted_input(i)];
// 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);
}
}
pub(crate) fn eval_lookups_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
vars: StarkEvaluationTargets<D, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
for i in 0..NUM_LOOKUPS {
let local_perm_input = vars.local_values[col_permuted_input(i)];
let next_perm_table = vars.next_values[col_permuted_table(i)];
let next_perm_input = vars.next_values[col_permuted_input(i)];
// 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);
}
}

16
system_zero/src/memory.rs
View File

@ -1,16 +0,0 @@
#[derive(Default)]
pub struct TransactionMemory {
pub calls: Vec<ContractMemory>,
}
/// A virtual memory space specific to the current contract call.
pub struct ContractMemory {
pub code: MemorySegment,
pub main: MemorySegment,
pub calldata: MemorySegment,
pub returndata: MemorySegment,
}
pub struct MemorySegment {
pub content: Vec<u8>,
}

321
system_zero/src/permutation_unit.rs
View File

@ -1,321 +0,0 @@
use plonky2::field::extension::{Extendable, FieldExtension};
use plonky2::field::packed::PackedField;
use plonky2::hash::hash_types::RichField;
use plonky2::hash::hashing::SPONGE_WIDTH;
use plonky2::hash::poseidon::{Poseidon, HALF_N_FULL_ROUNDS, N_PARTIAL_ROUNDS};
use plonky2::plonk::circuit_builder::CircuitBuilder;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars};
use crate::public_input_layout::NUM_PUBLIC_INPUTS;
use crate::registers::permutation::*;
use crate::registers::NUM_COLUMNS;
fn constant_layer<F, FE, P, const D: usize>(
mut state: [P; SPONGE_WIDTH],
round: usize,
) -> [P; SPONGE_WIDTH]
where
F: Poseidon,
FE: FieldExtension<D, BaseField = F>,
P: PackedField<Scalar = FE>,
{
// One day I might actually vectorize this, but today is not that day.
for i in 0..P::WIDTH {
let mut unpacked_state = [P::Scalar::default(); SPONGE_WIDTH];
for j in 0..SPONGE_WIDTH {
unpacked_state[j] = state[j].as_slice()[i];
}
F::constant_layer_field(&mut unpacked_state, round);
for j in 0..SPONGE_WIDTH {
state[j].as_slice_mut()[i] = unpacked_state[j];
}
}
state
}
fn mds_layer<F, FE, P, const D: usize>(mut state: [P; SPONGE_WIDTH]) -> [P; SPONGE_WIDTH]
where
F: Poseidon,
FE: FieldExtension<D, BaseField = F>,
P: PackedField<Scalar = FE>,
{
for i in 0..P::WIDTH {
let mut unpacked_state = [P::Scalar::default(); SPONGE_WIDTH];
for j in 0..SPONGE_WIDTH {
unpacked_state[j] = state[j].as_slice()[i];
}
unpacked_state = F::mds_layer_field(&unpacked_state);
for j in 0..SPONGE_WIDTH {
state[j].as_slice_mut()[i] = unpacked_state[j];
}
}
state
}
pub(crate) fn generate_permutation_unit<F: Poseidon>(values: &mut [F; NUM_COLUMNS]) {
// Load inputs.
let mut state = [F::ZERO; SPONGE_WIDTH];
for i in 0..SPONGE_WIDTH {
state[i] = values[col_input(i)];
}
for r in 0..HALF_N_FULL_ROUNDS {
F::constant_layer(&mut state, r);
for i in 0..SPONGE_WIDTH {
let state_cubed = state[i].cube();
values[col_full_first_mid_sbox(r, i)] = state_cubed;
state[i] *= state_cubed.square(); // Form state ** 7.
}
state = F::mds_layer(&state);
for i in 0..SPONGE_WIDTH {
values[col_full_first_after_mds(r, i)] = state[i];
}
}
for r in 0..N_PARTIAL_ROUNDS {
F::constant_layer(&mut state, HALF_N_FULL_ROUNDS + r);
let state0_cubed = state[0].cube();
values[col_partial_mid_sbox(r)] = state0_cubed;
state[0] *= state0_cubed.square(); // Form state ** 7.
values[col_partial_after_sbox(r)] = state[0];
state = F::mds_layer(&state);
}
for r in 0..HALF_N_FULL_ROUNDS {
F::constant_layer(&mut state, HALF_N_FULL_ROUNDS + N_PARTIAL_ROUNDS + r);
for i in 0..SPONGE_WIDTH {
let state_cubed = state[i].cube();
values[col_full_second_mid_sbox(r, i)] = state_cubed;
state[i] *= state_cubed.square(); // Form state ** 7.
}
state = F::mds_layer(&state);
for i in 0..SPONGE_WIDTH {
values[col_full_second_after_mds(r, i)] = state[i];
}
}
}
#[inline]
pub(crate) fn eval_permutation_unit<F, FE, P, const D: usize>(
vars: StarkEvaluationVars<FE, P, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut ConstraintConsumer<P>,
) where
F: Poseidon,
FE: FieldExtension<D, BaseField = F>,
P: PackedField<Scalar = FE>,
{
let local_values = &vars.local_values;
// Load inputs.
let mut state = [P::ZEROS; SPONGE_WIDTH];
for i in 0..SPONGE_WIDTH {
state[i] = local_values[col_input(i)];
}
for r in 0..HALF_N_FULL_ROUNDS {
state = constant_layer(state, r);
for i in 0..SPONGE_WIDTH {
let state_cubed = state[i] * state[i].square();
yield_constr.constraint(state_cubed - local_values[col_full_first_mid_sbox(r, i)]);
let state_cubed = local_values[col_full_first_mid_sbox(r, i)];
state[i] *= state_cubed.square(); // Form state ** 7.
}
state = mds_layer(state);
for i in 0..SPONGE_WIDTH {
yield_constr.constraint(state[i] - local_values[col_full_first_after_mds(r, i)]);
state[i] = local_values[col_full_first_after_mds(r, i)];
}
}
for r in 0..N_PARTIAL_ROUNDS {
state = constant_layer(state, HALF_N_FULL_ROUNDS + r);
let state0_cubed = state[0] * state[0].square();
yield_constr.constraint(state0_cubed - local_values[col_partial_mid_sbox(r)]);
let state0_cubed = local_values[col_partial_mid_sbox(r)];
state[0] *= state0_cubed.square(); // Form state ** 7.
yield_constr.constraint(state[0] - local_values[col_partial_after_sbox(r)]);
state[0] = local_values[col_partial_after_sbox(r)];
state = mds_layer(state);
}
for r in 0..HALF_N_FULL_ROUNDS {
state = constant_layer(state, HALF_N_FULL_ROUNDS + N_PARTIAL_ROUNDS + r);
for i in 0..SPONGE_WIDTH {
let state_cubed = state[i] * state[i].square();
yield_constr.constraint(state_cubed - local_values[col_full_second_mid_sbox(r, i)]);
let state_cubed = local_values[col_full_second_mid_sbox(r, i)];
state[i] *= state_cubed.square(); // Form state ** 7.
}
state = mds_layer(state);
for i in 0..SPONGE_WIDTH {
yield_constr.constraint(state[i] - local_values[col_full_second_after_mds(r, i)]);
state[i] = local_values[col_full_second_after_mds(r, i)];
}
}
}
pub(crate) fn eval_permutation_unit_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
vars: StarkEvaluationTargets<D, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let zero = builder.zero_extension();
let local_values = &vars.local_values;
// Load inputs.
let mut state = [zero; SPONGE_WIDTH];
for i in 0..SPONGE_WIDTH {
state[i] = local_values[col_input(i)];
}
for r in 0..HALF_N_FULL_ROUNDS {
F::constant_layer_circuit(builder, &mut state, r);
for i in 0..SPONGE_WIDTH {
let state_cubed = builder.cube_extension(state[i]);
let diff =
builder.sub_extension(state_cubed, local_values[col_full_first_mid_sbox(r, i)]);
yield_constr.constraint(builder, diff);
let state_cubed = local_values[col_full_first_mid_sbox(r, i)];
state[i] = builder.mul_many_extension([state[i], state_cubed, state_cubed]);
// Form state ** 7.
}
state = F::mds_layer_circuit(builder, &state);
for i in 0..SPONGE_WIDTH {
let diff =
builder.sub_extension(state[i], local_values[col_full_first_after_mds(r, i)]);
yield_constr.constraint(builder, diff);
state[i] = local_values[col_full_first_after_mds(r, i)];
}
}
for r in 0..N_PARTIAL_ROUNDS {
F::constant_layer_circuit(builder, &mut state, HALF_N_FULL_ROUNDS + r);
let state0_cubed = builder.cube_extension(state[0]);
let diff = builder.sub_extension(state0_cubed, local_values[col_partial_mid_sbox(r)]);
yield_constr.constraint(builder, diff);
let state0_cubed = local_values[col_partial_mid_sbox(r)];
state[0] = builder.mul_many_extension([state[0], state0_cubed, state0_cubed]); // Form state ** 7.
let diff = builder.sub_extension(state[0], local_values[col_partial_after_sbox(r)]);
yield_constr.constraint(builder, diff);
state[0] = local_values[col_partial_after_sbox(r)];
state = F::mds_layer_circuit(builder, &state);
}
for r in 0..HALF_N_FULL_ROUNDS {
F::constant_layer_circuit(
builder,
&mut state,
HALF_N_FULL_ROUNDS + N_PARTIAL_ROUNDS + r,
);
for i in 0..SPONGE_WIDTH {
let state_cubed = builder.cube_extension(state[i]);
let diff =
builder.sub_extension(state_cubed, local_values[col_full_second_mid_sbox(r, i)]);
yield_constr.constraint(builder, diff);
let state_cubed = local_values[col_full_second_mid_sbox(r, i)];
state[i] = builder.mul_many_extension([state[i], state_cubed, state_cubed]);
// Form state ** 7.
}
state = F::mds_layer_circuit(builder, &state);
for i in 0..SPONGE_WIDTH {
let diff =
builder.sub_extension(state[i], local_values[col_full_second_after_mds(r, i)]);
yield_constr.constraint(builder, diff);
state[i] = local_values[col_full_second_after_mds(r, i)];
}
}
}
#[cfg(test)]
mod tests {
use plonky2::field::goldilocks_field::GoldilocksField;
use plonky2::field::types::{Field, Sample};
use plonky2::hash::poseidon::Poseidon;
use rand::SeedableRng;
use rand_chacha::ChaCha8Rng;
use starky::constraint_consumer::ConstraintConsumer;
use starky::vars::StarkEvaluationVars;
use crate::permutation_unit::{eval_permutation_unit, generate_permutation_unit, SPONGE_WIDTH};
use crate::public_input_layout::NUM_PUBLIC_INPUTS;
use crate::registers::permutation::{col_input, col_output};
use crate::registers::NUM_COLUMNS;
#[test]
fn generate_eval_consistency() {
type F = GoldilocksField;
let mut values = [F::default(); NUM_COLUMNS];
generate_permutation_unit(&mut values);
let vars = StarkEvaluationVars {
local_values: &values,
next_values: &[F::default(); NUM_COLUMNS],
public_inputs: &[F::default(); NUM_PUBLIC_INPUTS],
};
let mut constrant_consumer = ConstraintConsumer::new(
vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)],
GoldilocksField::ONE,
GoldilocksField::ONE,
GoldilocksField::ONE,
);
eval_permutation_unit(vars, &mut constrant_consumer);
for &acc in &constrant_consumer.constraint_accs {
assert_eq!(acc, GoldilocksField::ZERO);
}
}
#[test]
fn poseidon_result() {
type F = GoldilocksField;
let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25);
let state = [F::default(); SPONGE_WIDTH].map(|_| F::sample(&mut rng));
// Get true Poseidon hash
let target = GoldilocksField::poseidon(state);
// Get result from `generate_permutation_unit`
// Initialize `values` with randomness to test that the code doesn't rely on zero-filling.
let mut values = [F::default(); NUM_COLUMNS].map(|_| F::sample(&mut rng));
for i in 0..SPONGE_WIDTH {
values[col_input(i)] = state[i];
}
generate_permutation_unit(&mut values);
let mut result = [F::default(); SPONGE_WIDTH];
for i in 0..SPONGE_WIDTH {
result[i] = values[col_output(i)];
}
assert_eq!(target, result);
}
// TODO(JN): test degree
// TODO(JN): test `eval_permutation_unit_recursively`
}

7
system_zero/src/public_input_layout.rs
View File

@ -1,7 +0,0 @@
/// The previous state root, before these transactions were executed.
const PI_OLD_STATE_ROOT: usize = 0;
/// The updated state root, after these transactions were executed.
const PI_NEW_STATE_ROOT: usize = PI_OLD_STATE_ROOT + 1;
pub(crate) const NUM_PUBLIC_INPUTS: usize = PI_NEW_STATE_ROOT + 1;

185
system_zero/src/registers/alu.rs
View File

@ -1,185 +0,0 @@
//! Arithmetic and logic unit.
pub(crate) const IS_ADD: usize = super::START_ALU;
pub(crate) const IS_SUB: usize = IS_ADD + 1;
pub(crate) const IS_MUL_ADD: usize = IS_SUB + 1;
pub(crate) const IS_DIV: usize = IS_MUL_ADD + 1;
pub(crate) const IS_AND: usize = IS_DIV + 1;
pub(crate) const IS_IOR: usize = IS_AND + 1;
pub(crate) const IS_XOR: usize = IS_IOR + 1;
pub(crate) const IS_ANDNOT: usize = IS_XOR + 1;
pub(crate) const IS_NOT: usize = IS_ANDNOT + 1;
pub(crate) const IS_ROTATE_LEFT: usize = IS_NOT + 1;
pub(crate) const IS_ROTATE_RIGHT: usize = IS_ROTATE_LEFT + 1;
pub(crate) const IS_SHIFT_LEFT: usize = IS_ROTATE_RIGHT + 1;
pub(crate) const IS_SHIFT_RIGHT: usize = IS_SHIFT_LEFT + 1;
pub(crate) const IS_ARITH_SHIFT_RIGHT: usize = IS_SHIFT_RIGHT + 1;
pub(crate) const ALL_OPERATIONS: [usize; 14] = [
IS_ADD,
IS_SUB,
IS_MUL_ADD,
IS_DIV,
IS_AND,
IS_IOR,
IS_XOR,
IS_ANDNOT,
IS_NOT,
IS_ROTATE_LEFT,
IS_ROTATE_RIGHT,
IS_SHIFT_LEFT,
IS_SHIFT_RIGHT,
IS_ARITH_SHIFT_RIGHT,
];
const START_SHARED_COLS: usize = IS_ARITH_SHIFT_RIGHT + 1;
/// Within the ALU, there are shared columns which can be used by any arithmetic/logic
/// circuit, depending on which one is active this cycle.
// Can be increased as needed as other operations are implemented.
const NUM_SHARED_COLS: usize = 130;
const fn shared_col(i: usize) -> usize {
debug_assert!(i < NUM_SHARED_COLS);
START_SHARED_COLS + i
}
/// The first value to be added; treated as an unsigned u32.
pub(crate) const COL_ADD_INPUT_0: usize = shared_col(0);
/// The second value to be added; treated as an unsigned u32.
pub(crate) const COL_ADD_INPUT_1: usize = shared_col(1);
/// The third value to be added; treated as an unsigned u32.
pub(crate) const COL_ADD_INPUT_2: usize = shared_col(2);
// Note: Addition outputs three 16-bit chunks, and since these values need to be range-checked
// anyway, we might as well use the range check unit's columns as our addition outputs. So the
// three proceeding columns are basically aliases, not columns owned by the ALU.
/// The first 16-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_ADD_OUTPUT_0: usize = super::range_check_16::col_rc_16_input(0);
/// The second 16-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_ADD_OUTPUT_1: usize = super::range_check_16::col_rc_16_input(1);
/// The third 16-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_ADD_OUTPUT_2: usize = super::range_check_16::col_rc_16_input(2);
/// Inputs for subtraction; the second value is subtracted from the
/// first; inputs treated as an unsigned u32.
pub(crate) const COL_SUB_INPUT_0: usize = shared_col(0);
pub(crate) const COL_SUB_INPUT_1: usize = shared_col(1);
/// The first 16-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_SUB_OUTPUT_0: usize = super::range_check_16::col_rc_16_input(0);
/// The second 16-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_SUB_OUTPUT_1: usize = super::range_check_16::col_rc_16_input(1);
/// The borrow output
pub(crate) const COL_SUB_OUTPUT_BORROW: usize = super::boolean::col_bit(0);
/// The first value to be multiplied; treated as an unsigned u32.
pub(crate) const COL_MUL_ADD_FACTOR_0: usize = shared_col(0);
/// The second value to be multiplied; treated as an unsigned u32.
pub(crate) const COL_MUL_ADD_FACTOR_1: usize = shared_col(1);
/// The value to be added to the product; treated as an unsigned u32.
pub(crate) const COL_MUL_ADD_ADDEND: usize = shared_col(2);
/// The inverse of `u32::MAX - result_hi`, where `output_hi` is the high 32-bits of the result.
/// See https://hackmd.io/NC-yRmmtRQSvToTHb96e8Q#Checking-element-validity
pub(crate) const COL_MUL_ADD_RESULT_CANONICAL_INV: usize = shared_col(3);
/// The first 16-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_MUL_ADD_OUTPUT_0: usize = super::range_check_16::col_rc_16_input(0);
/// The second 16-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_MUL_ADD_OUTPUT_1: usize = super::range_check_16::col_rc_16_input(1);
/// The third 16-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_MUL_ADD_OUTPUT_2: usize = super::range_check_16::col_rc_16_input(2);
/// The fourth 16-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_MUL_ADD_OUTPUT_3: usize = super::range_check_16::col_rc_16_input(3);
/// Dividend for division, as an unsigned u32
pub(crate) const COL_DIV_INPUT_DIVIDEND: usize = shared_col(0);
/// Divisor for division, as an unsigned u32
pub(crate) const COL_DIV_INPUT_DIVISOR: usize = shared_col(1);
/// Inverse of divisor, if one exists, and 0 otherwise
pub(crate) const COL_DIV_INVDIVISOR: usize = shared_col(2);
/// 1 if divisor is nonzero and 0 otherwise
pub(crate) const COL_DIV_NONZERO_DIVISOR: usize = shared_col(3);
/// The first 16-bit chunk of the quotient, based on little-endian ordering.
pub(crate) const COL_DIV_OUTPUT_QUOT_0: usize = super::range_check_16::col_rc_16_input(0);
/// The second 16-bit chunk of the quotient, based on little-endian ordering.
pub(crate) const COL_DIV_OUTPUT_QUOT_1: usize = super::range_check_16::col_rc_16_input(1);
/// The first 16-bit chunk of the remainder, based on little-endian ordering.
pub(crate) const COL_DIV_OUTPUT_REM_0: usize = super::range_check_16::col_rc_16_input(2);
/// The second 16-bit chunk of the remainder, based on little-endian ordering.
pub(crate) const COL_DIV_OUTPUT_REM_1: usize = super::range_check_16::col_rc_16_input(3);
/// The first 16-bit chunk of a temporary value (divisor - remainder - 1).
pub(crate) const COL_DIV_RANGE_CHECKED_TMP_0: usize = super::range_check_16::col_rc_16_input(4);
/// The second 16-bit chunk of a temporary value (divisor - remainder - 1).
pub(crate) const COL_DIV_RANGE_CHECKED_TMP_1: usize = super::range_check_16::col_rc_16_input(5);
///
/// Bitwise logic operations
///
/// Bit decomposition of 64-bit values, as 32-bit low and high halves.
const fn gen_bitop_nbit_input_regs<const N: usize>(start: usize) -> [usize; N] {
let mut regs = [0usize; N];
let mut i = 0;
while i < N {
regs[i] = shared_col(start + i);
i += 1;
}
regs
}
pub(crate) const COL_BIT_DECOMP_INPUT_A_LO_BIN_REGS: [usize; 32] =
gen_bitop_nbit_input_regs::<32>(0);
pub(crate) const COL_BIT_DECOMP_INPUT_A_HI_BIN_REGS: [usize; 32] =
gen_bitop_nbit_input_regs::<32>(32);
pub(crate) const COL_BIT_DECOMP_INPUT_B_LO_BIN_REGS: [usize; 32] =
gen_bitop_nbit_input_regs::<32>(64);
pub(crate) const COL_BIT_DECOMP_INPUT_B_HI_BIN_REGS: [usize; 32] =
gen_bitop_nbit_input_regs::<32>(96);
/// The first 32-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_BITOP_OUTPUT_0: usize = shared_col(128);
/// The second 32-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_BITOP_OUTPUT_1: usize = shared_col(129);
/// Input value to be rotated or shifted, low 32 bits
pub(crate) const COL_ROTATE_SHIFT_INPUT_LO: usize = shared_col(0);
/// Input value to be rotated or shifted, high 32 bits
pub(crate) const COL_ROTATE_SHIFT_INPUT_HI: usize = shared_col(1);
/// Bit decomposition of EXP, which is DELTA mod 32 for left
/// rotate/shift; bit decomposition of (32 - DELTA mod 32) mod 32 for
/// right rotate/shift.
pub(crate) const COL_ROTATE_SHIFT_EXP_BITS: [usize; 5] = gen_bitop_nbit_input_regs::<5>(2);
/// Top bit of the 6-bit value DELTA; also interpreted as DELTA >= 32.
pub(crate) const COL_ROTATE_SHIFT_DELTA_DIV32: usize = shared_col(7);
/// POW_EXP = 2^EXP, the AUX_i vars are helpers.
pub(crate) const COL_ROTATE_SHIFT_POW_EXP_AUX_0: usize = shared_col(8);
pub(crate) const COL_ROTATE_SHIFT_POW_EXP_AUX_1: usize = shared_col(9);
pub(crate) const COL_ROTATE_SHIFT_POW_EXP_AUX_2: usize = shared_col(10);
pub(crate) const COL_ROTATE_SHIFT_POW_EXP: usize = shared_col(11);
/// low 32 bits of INPUT_LO * 2^EXP
pub(crate) const COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_0: usize = shared_col(12);
/// high 32 bits of INPUT_LO * 2^EXP
pub(crate) const COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_1: usize = shared_col(13);
/// low 32 bits of INPUT_HI * 2^EXP
pub(crate) const COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_0: usize = shared_col(14);
/// high 32 bits of INPUT_HI * 2^EXP
pub(crate) const COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_1: usize = shared_col(15);
pub(crate) const COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_0: usize = shared_col(16);
pub(crate) const COL_ROTATE_SHIFT_INPUT_LO_DISPLACED_AUX_1: usize = shared_col(17);
pub(crate) const COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_0: usize = shared_col(18);
pub(crate) const COL_ROTATE_SHIFT_INPUT_HI_DISPLACED_AUX_1: usize = shared_col(19);
/// The first 32-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_ROTATE_SHIFT_OUTPUT_0: usize = shared_col(20);
/// The second 32-bit chunk of the output, based on little-endian ordering.
pub(crate) const COL_ROTATE_SHIFT_OUTPUT_1: usize = shared_col(21);
pub(super) const END: usize = START_SHARED_COLS + NUM_SHARED_COLS;

10
system_zero/src/registers/boolean.rs
View File

@ -1,10 +0,0 @@
//! Boolean unit. Contains columns whose values must be 0 or 1.
const NUM_BITS: usize = 128;
pub const fn col_bit(index: usize) -> usize {
debug_assert!(index < NUM_BITS);
super::START_BOOLEAN + index
}
pub(super) const END: usize = super::START_BOOLEAN + NUM_BITS;

20
system_zero/src/registers/core.rs
View File

@ -1,20 +0,0 @@
//! Core registers.
/// A cycle counter. Starts at 0; increments by 1.
pub(crate) const COL_CLOCK: usize = super::START_CORE;
/// A column which contains the values `[0, ... 2^16 - 1]`, potentially with duplicates. Used for
/// 16-bit range checks.
///
/// For ease of verification, we enforce that it must begin with 0 and end with `2^16 - 1`, and each
/// delta must be either 0 or 1.
pub(crate) const COL_RANGE_16: usize = COL_CLOCK + 1;
/// Pointer to the current instruction.
pub(crate) const COL_INSTRUCTION_PTR: usize = COL_RANGE_16 + 1;
/// Pointer to the base of the current call's stack frame.
pub(crate) const COL_FRAME_PTR: usize = COL_INSTRUCTION_PTR + 1;
/// Pointer to the tip of the current call's stack frame.
pub(crate) const COL_STACK_PTR: usize = COL_FRAME_PTR + 1;
pub(super) const END: usize = COL_STACK_PTR + 1;

3
system_zero/src/registers/logic.rs
View File

@ -1,3 +0,0 @@
//! Logic unit.
pub(super) const END: usize = super::START_LOGIC;

37
system_zero/src/registers/lookup.rs
View File

@ -1,37 +0,0 @@
//! Lookup unit.
//! See https://zcash.github.io/halo2/design/proving-system/lookup.html
const START_UNIT: usize = super::START_LOOKUP;
pub(crate) const NUM_LOOKUPS: usize =
super::range_check_16::NUM_RANGE_CHECKS + super::range_check_degree::NUM_RANGE_CHECKS;
pub(crate) const fn col_input(i: usize) -> usize {
if i < super::range_check_16::NUM_RANGE_CHECKS {
super::range_check_16::col_rc_16_input(i)
} else {
super::range_check_degree::col_rc_degree_input(i - super::range_check_16::NUM_RANGE_CHECKS)
}
}
/// This column contains a permutation of the input values.
pub(crate) const fn col_permuted_input(i: usize) -> usize {
debug_assert!(i < NUM_LOOKUPS);
START_UNIT + 2 * i
}
pub(crate) const fn col_table(i: usize) -> usize {
if i < super::range_check_16::NUM_RANGE_CHECKS {
super::core::COL_RANGE_16
} else {
super::core::COL_CLOCK
}
}
/// This column contains a permutation of the table values.
pub(crate) const fn col_permuted_table(i: usize) -> usize {
debug_assert!(i < NUM_LOOKUPS);
START_UNIT + 2 * i + 1
}
pub(super) const END: usize = START_UNIT + NUM_LOOKUPS * 2;

3
system_zero/src/registers/memory.rs
View File

@ -1,3 +0,0 @@
//! Memory unit.
pub(super) const END: usize = super::START_MEMORY;

20
system_zero/src/registers/mod.rs
View File

@ -1,20 +0,0 @@
pub(crate) mod alu;
pub(crate) mod boolean;
pub(crate) mod core;
pub(crate) mod logic;
pub(crate) mod lookup;
pub(crate) mod memory;
pub(crate) mod permutation;
pub(crate) mod range_check_16;
pub(crate) mod range_check_degree;
const START_ALU: usize = 0;
const START_BOOLEAN: usize = alu::END;
const START_CORE: usize = boolean::END;
const START_LOGIC: usize = core::END;
const START_LOOKUP: usize = logic::END;
const START_MEMORY: usize = lookup::END;
const START_PERMUTATION: usize = memory::END;
const START_RANGE_CHECK_16: usize = permutation::END;
const START_RANGE_CHECK_DEGREE: usize = range_check_16::END;
pub(crate) const NUM_COLUMNS: usize = range_check_degree::END;

57
system_zero/src/registers/permutation.rs
View File

@ -1,57 +0,0 @@
//! Permutation unit.
use plonky2::hash::hashing::SPONGE_WIDTH;
use plonky2::hash::poseidon;
const START_FULL_FIRST: usize = super::START_PERMUTATION + SPONGE_WIDTH;
pub const fn col_full_first_mid_sbox(round: usize, i: usize) -> usize {
debug_assert!(round < poseidon::HALF_N_FULL_ROUNDS);
debug_assert!(i < SPONGE_WIDTH);
START_FULL_FIRST + 2 * round * SPONGE_WIDTH + i
}
pub const fn col_full_first_after_mds(round: usize, i: usize) -> usize {
debug_assert!(round < poseidon::HALF_N_FULL_ROUNDS);
debug_assert!(i < SPONGE_WIDTH);
START_FULL_FIRST + (2 * round + 1) * SPONGE_WIDTH + i
}
const START_PARTIAL: usize =
col_full_first_after_mds(poseidon::HALF_N_FULL_ROUNDS - 1, SPONGE_WIDTH - 1) + 1;
pub const fn col_partial_mid_sbox(round: usize) -> usize {
debug_assert!(round < poseidon::N_PARTIAL_ROUNDS);
START_PARTIAL + 2 * round
}
pub const fn col_partial_after_sbox(round: usize) -> usize {
debug_assert!(round < poseidon::N_PARTIAL_ROUNDS);
START_PARTIAL + 2 * round + 1
}
const START_FULL_SECOND: usize = col_partial_after_sbox(poseidon::N_PARTIAL_ROUNDS - 1) + 1;
pub const fn col_full_second_mid_sbox(round: usize, i: usize) -> usize {
debug_assert!(round <= poseidon::HALF_N_FULL_ROUNDS);
debug_assert!(i < SPONGE_WIDTH);
START_FULL_SECOND + 2 * round * SPONGE_WIDTH + i
}
pub const fn col_full_second_after_mds(round: usize, i: usize) -> usize {
debug_assert!(round <= poseidon::HALF_N_FULL_ROUNDS);
debug_assert!(i < SPONGE_WIDTH);
START_FULL_SECOND + (2 * round + 1) * SPONGE_WIDTH + i
}
pub const fn col_input(i: usize) -> usize {
debug_assert!(i < SPONGE_WIDTH);
super::START_PERMUTATION + i
}
pub const fn col_output(i: usize) -> usize {
debug_assert!(i < SPONGE_WIDTH);
col_full_second_after_mds(poseidon::HALF_N_FULL_ROUNDS - 1, i)
}
pub(super) const END: usize = col_output(SPONGE_WIDTH - 1) + 1;

11
system_zero/src/registers/range_check_16.rs
View File

@ -1,11 +0,0 @@
//! Range check unit which checks that values are in `[0, 2^16)`.
pub(super) const NUM_RANGE_CHECKS: usize = 6;
/// The input of the `i`th range check, i.e. the value being range checked.
pub(crate) const fn col_rc_16_input(i: usize) -> usize {
debug_assert!(i < NUM_RANGE_CHECKS);
super::START_RANGE_CHECK_16 + i
}
pub(super) const END: usize = super::START_RANGE_CHECK_16 + NUM_RANGE_CHECKS;

11
system_zero/src/registers/range_check_degree.rs
View File

@ -1,11 +0,0 @@
//! Range check unit which checks that values are in `[0, degree)`.
pub(crate) const NUM_RANGE_CHECKS: usize = 5;
/// The input of the `i`th range check, i.e. the value being range checked.
pub(crate) const fn col_rc_degree_input(i: usize) -> usize {
debug_assert!(i < NUM_RANGE_CHECKS);
super::START_RANGE_CHECK_DEGREE + i
}
pub(super) const END: usize = super::START_RANGE_CHECK_DEGREE + NUM_RANGE_CHECKS;

222
system_zero/src/system_zero.rs
View File

@ -1,222 +0,0 @@
use std::marker::PhantomData;
use plonky2::field::extension::{Extendable, FieldExtension};
use plonky2::field::packed::PackedField;
use plonky2::field::polynomial::PolynomialValues;
use plonky2::hash::hash_types::RichField;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use plonky2::timed;
use plonky2::util::timing::TimingTree;
use plonky2::util::transpose;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use starky::permutation::PermutationPair;
use starky::stark::Stark;
use starky::vars::{StarkEvaluationTargets, StarkEvaluationVars};
use crate::alu::{eval_alu, eval_alu_circuit, generate_alu};
use crate::core_registers::{
eval_core_registers, eval_core_registers_circuit, generate_first_row_core_registers,
generate_next_row_core_registers,
};
use crate::lookup::{eval_lookups, eval_lookups_circuit, generate_lookups};
use crate::memory::TransactionMemory;
use crate::permutation_unit::{
eval_permutation_unit, eval_permutation_unit_circuit, generate_permutation_unit,
};
use crate::public_input_layout::NUM_PUBLIC_INPUTS;
use crate::registers::{lookup, NUM_COLUMNS};
/// We require at least 2^16 rows as it helps support efficient 16-bit range checks.
const MIN_TRACE_ROWS: usize = 1 << 16;
#[derive(Copy, Clone)]
pub struct SystemZero<F: RichField + Extendable<D>, const D: usize> {
_phantom: PhantomData<F>,
}
impl<F: RichField + Extendable<D>, const D: usize> SystemZero<F, D> {
/// Generate the rows of the trace. Note that this does not generate the permuted columns used
/// in our lookup arguments, as those are computed after transposing to column-wise form.
fn generate_trace_rows(&self) -> Vec<[F; NUM_COLUMNS]> {
#[allow(unused)] // TODO
let memory = TransactionMemory::default();
let mut row = [F::ZERO; NUM_COLUMNS];
generate_first_row_core_registers(&mut row);
generate_alu(&mut row);
generate_permutation_unit(&mut row);
let mut trace = Vec::with_capacity(MIN_TRACE_ROWS);
loop {
let mut next_row = [F::ZERO; NUM_COLUMNS];
generate_next_row_core_registers(&row, &mut next_row);
generate_alu(&mut next_row);
generate_permutation_unit(&mut next_row);
trace.push(row);
row = next_row;
// TODO: Replace with proper termination condition.
if trace.len() == (1 << 16) - 1 {
break;
}
}
trace.push(row);
trace
}
pub fn generate_trace(&self) -> Vec<PolynomialValues<F>> {
let mut timing = TimingTree::new("generate trace", log::Level::Debug);
// Generate the witness, except for permuted columns in the lookup argument.
let trace_rows = timed!(
&mut timing,
"generate trace rows",
self.generate_trace_rows()
);
// Transpose from row-wise to column-wise.
let trace_row_vecs: Vec<_> = timed!(
&mut timing,
"convert to Vecs",
trace_rows.into_iter().map(|row| row.to_vec()).collect()
);
let mut trace_col_vecs: Vec<Vec<F>> =
timed!(&mut timing, "transpose", transpose(&trace_row_vecs));
// Generate permuted columns in the lookup argument.
timed!(
&mut timing,
"generate lookup columns",
generate_lookups(&mut trace_col_vecs)
);
let trace_polys = timed!(
&mut timing,
"convert to PolynomialValues",
trace_col_vecs
.into_iter()
.map(|column| PolynomialValues::new(column))
.collect()
);
timing.print();
trace_polys
}
}
impl<F: RichField + Extendable<D>, const D: usize> Default for SystemZero<F, D> {
fn default() -> Self {
Self {
_phantom: PhantomData,
}
}
}
impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for SystemZero<F, D> {
const COLUMNS: usize = NUM_COLUMNS;
const PUBLIC_INPUTS: usize = NUM_PUBLIC_INPUTS;
fn eval_packed_generic<FE, P, const D2: usize>(
&self,
vars: StarkEvaluationVars<FE, P, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut ConstraintConsumer<P>,
) where
FE: FieldExtension<D2, BaseField = F>,
P: PackedField<Scalar = FE>,
{
eval_core_registers(vars, yield_constr);
eval_alu(vars, yield_constr);
eval_permutation_unit::<F, FE, P, D2>(vars, yield_constr);
eval_lookups(vars, yield_constr);
// TODO: Other units
}
fn eval_ext_circuit(
&self,
builder: &mut CircuitBuilder<F, D>,
vars: StarkEvaluationTargets<D, NUM_COLUMNS, NUM_PUBLIC_INPUTS>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
eval_core_registers_circuit(builder, vars, yield_constr);
eval_alu_circuit(builder, vars, yield_constr);
eval_permutation_unit_circuit(builder, vars, yield_constr);
eval_lookups_circuit(builder, vars, yield_constr);
// TODO: Other units
}
fn constraint_degree(&self) -> usize {
3
}
fn permutation_pairs(&self) -> Vec<PermutationPair> {
let mut pairs = Vec::new();
for i in 0..lookup::NUM_LOOKUPS {
pairs.push(PermutationPair::singletons(
lookup::col_input(i),
lookup::col_permuted_input(i),
));
pairs.push(PermutationPair::singletons(
lookup::col_table(i),
lookup::col_permuted_table(i),
));
}
// TODO: Add permutation pairs for memory.
pairs
}
}
#[cfg(test)]
mod tests {
use anyhow::Result;
use log::Level;
use plonky2::field::goldilocks_field::GoldilocksField;
use plonky2::field::types::Field;
use plonky2::plonk::config::PoseidonGoldilocksConfig;
use plonky2::util::timing::TimingTree;
use starky::config::StarkConfig;
use starky::prover::prove;
use starky::stark::Stark;
use starky::stark_testing::test_stark_low_degree;
use starky::verifier::verify_stark_proof;
use crate::system_zero::SystemZero;
#[test]
fn run() -> Result<()> {
init_logger();
type F = GoldilocksField;
type C = PoseidonGoldilocksConfig;
const D: usize = 2;
type S = SystemZero<F, D>;
let system = S::default();
let public_inputs = [F::ZERO; S::PUBLIC_INPUTS];
let config = StarkConfig::standard_fast_config();
let mut timing = TimingTree::new("prove", Level::Debug);
let trace = system.generate_trace();
let proof = prove::<F, C, S, D>(system, &config, trace, public_inputs, &mut timing)?;
verify_stark_proof(system, proof, &config)
}
#[test]
fn degree() -> Result<()> {
type F = GoldilocksField;
const D: usize = 2;
type S = SystemZero<F, D>;
let system = S::default();
test_stark_low_degree(system)
}
fn init_logger() {
let _ = env_logger::builder().format_timestamp(None).try_init();
}
}