require "std_lookup.pil"
require "std_range_check.pil"
require "operations.pil"
require "opids.pil"
airtemplate BinaryAdd(const int N = 2**21, const int RC = 2) {
col witness bits(32) a[RC];
col witness bits(32) b[RC];
col witness bits(16) c_chunks[RC*2];
col witness bits(1) cout[RC];
const expr c[RC];
for (int i = 0; i < RC; i++) {
cout[i] * (1 - cout[i]) === 0;
expr left = a[i] + b[i];
if (i > 0) {
left = left + cout[i-1];
}
left === cout[i] * 2 ** 32 + c_chunks[i * 2 + 1] * 2 ** 16 + c_chunks[i * 2];
c[i] = c_chunks[i * 2 + 1] * 2 ** 16 + c_chunks[i * 2];
range_check(expression: c_chunks[i * 2], min: 0, max: 2**16 - 1);
range_check(expression: c_chunks[i * 2 + 1], min: 0, max: 2**16 - 1);
}
proves_operation(op: OP_ADD, a:, b:, c:);
airval padding_size;
assumes_padding_operation(op: OP_ADD, padding_size:);
}