Skip to content

chore: simplify uint logic by removing witness_status [take 2]#16014

Merged
suyash67 merged 6 commits into
sb/uint-combinedfrom
sb/remove-uint-witness-status
Jul 27, 2025
Merged

chore: simplify uint logic by removing witness_status [take 2]#16014
suyash67 merged 6 commits into
sb/uint-combinedfrom
sb/remove-uint-witness-status

Conversation

@suyash67

Copy link
Copy Markdown
Contributor

TLDR: uint arithmetic operators + and - had a coding error and as a result, we weren't actually supporting lazy arithmetic over integers. This PR simplifies the uint class to now allow any "unbounded" values.

The Issue

In the current uint class, we allow "unbounded" values, for example, a uint32_ct can contain a value > 32 bits. This was done to allow lazy arithmetic before such values were "normalized". This is because a call to normalize() is expensive: it decomposes the value in 12-bit slices and range-constrains each slice.

In practice though, the addition and subtraction operator actually didn't allow any overflow due to a coding error.
On adding two $\textsf{uint}x$ values $a$ and $b$ (where $x \in [8, 16, 32, 64]$), we currently do:

// N.B. We assume that additive_constant is nonzero ONLY if value is constant
const uint256_t lhs = get_value();
const uint256_t rhs = other.get_value();
const uint256_t constants = (additive_constant + other.additive_constant) & MASK;
const uint256_t sum = lhs + rhs;
const uint256_t overflow = sum >> width;
const uint256_t remainder = sum & MASK;
const add_quad_<FF> gate{
is_constant() ? ctx->zero_idx : witness_index,
other.is_constant() ? ctx->zero_idx : other.witness_index,
ctx->add_variable(remainder),
ctx->add_variable(overflow),
FF::one(),
FF::one(),
FF::neg_one(),
-FF(CIRCUIT_UINT_MAX_PLUS_ONE),
constants,
};
ctx->create_balanced_add_gate(gate);

Assume $a, b$ are both witnesses, the create_balanced_add_gate creates the following constraint:

$$a + b = q \cdot \textcolor{grey}{2^x} + r$$

where the quotient $q$ and remainder $r$ are computed as:

$$q := \frac{(a \textsf{ mod } 2^x) + (b \textsf{ mod } 2^x)}{2^x}, \quad r := \left((a \textsf{ mod } 2^x) + (b \textsf{ mod } 2^x)\right) \textsf{ mod } 2^x.$$

In other words, the quotient and remainder are computed from the "truncated" values of $a$ and $b$ when it should have been from the "unbounded" values. Effectively, this means we are not actually supporting lazy arithmetic (i.e., arithmetic operations expect inputs to be "normalized"). I wrote a test here that fails when, ideally, it should have passed. This confirmed the coding error.

Solution(s)

One way to fix this is to actually use get_unbounded_value() in place of get_value() (on lines 27 and 28 in operator+ above). But we never really were using the benefits of lazy addition (because of this silly error). So we decided its better to remove functionality related to "unbounded" uint values.

Thus, we remove the witness_status member of the uint class as it tracks if a uint needs to be "normalized". As a consequence, we now need to "normalize" in every constructor where we weren't constraining the accumulators (i.e., byte_array and std::vector<bool_t>). Further, in operator+ and operator- we normalize the result. Also, removed the get_unbounded_value() as it isn't being used anywhere.

@suyash67 suyash67 merged commit 3a8f25b into sb/uint-combined Jul 27, 2025
5 of 6 checks passed
@suyash67 suyash67 deleted the sb/remove-uint-witness-status branch July 27, 2025 07:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant