binius_circuits/lasso/
u8add.rs

1// Copyright 2024-2025 Irreducible Inc.
2
3use std::vec;
4
5use anyhow::Result;
6use binius_core::oracle::OracleId;
7use binius_field::{BinaryField1b, BinaryField32b, BinaryField8b, TowerField};
8
9use super::batch::LookupBatch;
10use crate::builder::{types::F, ConstraintSystemBuilder};
11
12type B1 = BinaryField1b;
13type B8 = BinaryField8b;
14type B32 = BinaryField32b;
15
16pub fn u8add(
17	builder: &mut ConstraintSystemBuilder,
18	lookup_batch: &mut LookupBatch,
19	name: impl ToString + Clone,
20	x_in: OracleId,
21	y_in: OracleId,
22	carry_in: OracleId,
23	log_size: usize,
24) -> Result<(OracleId, OracleId), anyhow::Error> {
25	builder.push_namespace(name);
26
27	let sum = builder.add_committed("sum", log_size, B8::TOWER_LEVEL);
28
29	let carry_out = builder.add_committed("cout", log_size, B1::TOWER_LEVEL);
30
31	let lookup_u = builder.add_linear_combination(
32		"lookup_u",
33		log_size,
34		[
35			(carry_in, <F as TowerField>::basis(0, 25)?),
36			(carry_out, <F as TowerField>::basis(3, 3)?),
37			(x_in, <F as TowerField>::basis(3, 2)?),
38			(y_in, <F as TowerField>::basis(3, 1)?),
39			(sum, <F as TowerField>::basis(3, 0)?),
40		],
41	)?;
42
43	let mut u_to_t_mapping = vec![];
44
45	if let Some(witness) = builder.witness() {
46		let mut sum_witness = witness.new_column::<B8>(sum);
47		let mut carry_out_witness = witness.new_column::<B1>(carry_out);
48		let mut lookup_u_witness = witness.new_column::<B32>(lookup_u);
49		let mut u_to_t_mapping_witness = vec![0; 1 << log_size];
50
51		let x_in_u8 = witness.get::<B8>(x_in)?.as_slice::<u8>();
52		let y_in_u8 = witness.get::<B8>(y_in)?.as_slice::<u8>();
53		let carry_in_u8_packed = witness.get::<B1>(carry_in)?.as_slice::<u8>();
54
55		let sum_u8 = sum_witness.as_mut_slice::<u8>();
56		let carry_out_u8_packed = carry_out_witness.as_mut_slice::<u8>();
57		let lookup_u_u32 = lookup_u_witness.as_mut_slice::<u32>();
58
59		for row_idx in 0..1 << log_size {
60			let carry_in_usize = ((carry_in_u8_packed[row_idx / 8] >> (row_idx % 8)) & 1) as usize;
61
62			let x_in_usize = x_in_u8[row_idx] as usize;
63			let y_in_usize = y_in_u8[row_idx] as usize;
64			let xy_sum_with_carry_out = x_in_usize + y_in_usize + carry_in_usize;
65			let xy_sum_usize = xy_sum_with_carry_out & 0xff;
66			let carry_out_usize = xy_sum_with_carry_out >> 8;
67			let lookup_index = (carry_in_usize << 16) | (x_in_usize << 8) | y_in_usize;
68			let lookup_value = (carry_in_usize << 25)
69				| (carry_out_usize << 24)
70				| (x_in_usize << 16)
71				| (y_in_usize << 8)
72				| xy_sum_usize;
73
74			lookup_u_u32[row_idx] = lookup_value as u32;
75
76			sum_u8[row_idx] = xy_sum_usize as u8;
77
78			// Zero out the bit in case it's uninitialized
79			carry_out_u8_packed[row_idx / 8] &= 0xff ^ (1 << (row_idx % 8));
80
81			// Write our value to the bit
82			carry_out_u8_packed[row_idx / 8] |= (carry_out_usize << (row_idx % 8)) as u8;
83
84			u_to_t_mapping_witness[row_idx] = lookup_index;
85		}
86
87		u_to_t_mapping = u_to_t_mapping_witness;
88	}
89
90	lookup_batch.add([lookup_u], u_to_t_mapping, 1 << log_size);
91
92	builder.pop_namespace();
93	Ok((carry_out, sum))
94}
binius_circuits/lasso/u8add.rs

binius_circuits/lasso/
u8add.rs
