From 2644f5f74a241244de19e306ae75b7d07a029e2a Mon Sep 17 00:00:00 2001
From: Hamish Ivey-Law <426294+unzvfu@users.noreply.github.com>
Date: Thu, 3 Mar 2022 14:18:19 +1100
Subject: [PATCH] System Zero subtraction operation (#508)

* First draft of subtraction operation.

* Daniel comments.

* Fix constraint calculation.

* cargo fmt

* Align native and recursive eval functions; fix typo.
---
 system_zero/src/alu/subtraction.rs | 53 ++++++++++++++++++++++++++++--
 system_zero/src/registers/alu.rs   | 12 +++++++
 2 files changed, 62 insertions(+), 3 deletions(-)

diff --git a/system_zero/src/alu/subtraction.rs b/system_zero/src/alu/subtraction.rs
index 8f8bb810..8b795cbb 100644
--- a/system_zero/src/alu/subtraction.rs
+++ b/system_zero/src/alu/subtraction.rs
@@ -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);
 }
diff --git a/system_zero/src/registers/alu.rs b/system_zero/src/registers/alu.rs
index e678d8e4..6a9412a1 100644
--- a/system_zero/src/registers/alu.rs
+++ b/system_zero/src/registers/alu.rs
@@ -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.