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

System Zero subtraction operation (#508)

Browse Source 
* First draft of subtraction operation.

* Daniel comments.

* Fix constraint calculation.

* cargo fmt

* Align native and recursive eval functions; fix typo.
This commit is contained in:
Hamish Ivey-Law 2022-03-03 14:18:19 +11:00 committed by GitHub
parent 6b386e756a
commit 2644f5f74a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 62 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -10,7 +10,18 @@ use crate::registers::alu::*;
use crate::registers::NUM_COLUMNS;
pub(crate) fn generate_subtraction<F: PrimeField64>(values: &mut [F; NUM_COLUMNS]) {
// TODO
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);
let diff_1 = F::from_canonical_u16(diff as u16);
let diff_2 = F::from_canonical_u16((diff >> 16) as u16);
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_canonical_u16(br as u16);
}
pub(crate) fn eval_subtraction<F: Field, P: PackedField<Scalar = F>>(
@ -18,7 +29,23 @@ pub(crate) fn eval_subtraction<F: Field, P: PackedField<Scalar = F>>(
yield_constr: &mut ConstraintConsumer<P>,
) {
let is_sub = local_values[IS_SUB];
// TODO
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_recursively<F: RichField + Extendable<D>, const D: usize>(
@ -27,5 +54,25 @@ pub(crate) fn eval_subtraction_recursively<F: RichField + Extendable<D>, const D
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let is_sub = local_values[IS_SUB];
// TODO
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));
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);
}

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

@ -34,6 +34,18 @@ pub(crate) const COL_ADD_OUTPUT_1: usize = super::range_check_16::col_rc_16_inpu
/// 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.