## miden::core::math::u256
| Procedure | Description |
| ----------- | ------------- |
| wrapping_add | Performs addition of two unsigned 256 bit integers discarding the overflow.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = (a + b) % 2^256.<br /> |
| overflowing_add | Performs addition of two unsigned 256 bit integers preserving the overflow.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [overflow, c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = (a + b) % 2^256.<br /> |
| widening_add | Performs addition of two unsigned 256 bit integers preserving the overflow with sum on top.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, overflow, ...], where c = (a + b) % 2^256.<br /> |
| wrapping_sub | Performs subtraction of two unsigned 256 bit integers discarding the underflow.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = (a - b) % 2^256.<br /> |
| overflowing_sub | Performs subtraction of two unsigned 256 bit integers preserving the underflow.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [underflow, c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = (a - b) % 2^256.<br /> |
| and | Computes bitwise AND of two unsigned 256 bit integers.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = a & b.<br /> |
| or | Computes bitwise OR of two unsigned 256 bit integers.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = a \| b.<br /> |
| xor | Computes bitwise XOR of two unsigned 256 bit integers.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = a ^ b.<br /> |
| not | Computes bitwise NOT of one unsigned 256 bit integer.<br />Stack transition looks as follows:<br />[a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = !a (i.e., 2^256 - 1 - a).<br /> |
| eqz | Returns 1 if the top u256 value is zero; lower stack values are preserved.<br />Stack transition looks as follows:<br />[a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [is_zero, ...].<br /> |
| eq | Returns 1 if two unsigned 256 bit integers are equal.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [is_equal, ...].<br /> |
| neq | Returns 1 if two unsigned 256 bit integers are not equal.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [is_neq, ...].<br /> |
| lt | Returns 1 if a < b for unsigned 256 bit integers.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [c, ...],<br />where c = 1 when a < b, and 0 otherwise.<br /> |
| gt | Returns 1 if a > b for unsigned 256 bit integers.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [c, ...],<br />where c = 1 when a > b, and 0 otherwise.<br /> |
| lte | Returns 1 if a <= b for unsigned 256 bit integers.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [c, ...],<br />where c = 1 when a <= b, and 0 otherwise.<br /> |
| gte | Returns 1 if a >= b for unsigned 256 bit integers.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [c, ...],<br />where c = 1 when a >= b, and 0 otherwise.<br /> |
| min | Returns the minimum of two unsigned 256 bit integers.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = min(a, b).<br /> |
| max | Returns the maximum of two unsigned 256 bit integers.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = max(a, b).<br /> |
| wrapping_mul | Performs multiplication of two unsigned 256 bit integers discarding the overflow.<br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = (a * b) % 2^256.<br /> |
| overflowing_mul | Performs multiplication of two unsigned 256 bit integers preserving the overflow flag.<br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [overflow, c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = (a * b) % 2^256<br />and overflow = 1 iff a * b >= 2^256.<br /> |
| widening_mul | Performs multiplication of two unsigned 256 bit integers preserving the full 512-bit product.<br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, ...],<br />where c = a * b as a 512-bit value with c0 being the least significant 32-bit limb.<br /> |
| clz | Counts the number of leading zeros of an unsigned 256 bit integer.<br />Stack transition looks as follows:<br />[a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [count, ...], where count is the number of leading<br />zero bits in a (0..=256).<br /> |
| ctz | Counts the number of trailing zeros of an unsigned 256 bit integer.<br />Stack transition looks as follows:<br />[a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [count, ...], where count is the number of trailing<br />zero bits in a (0..=256).<br /> |
| clo | Counts the number of leading ones of an unsigned 256 bit integer.<br />Stack transition looks as follows:<br />[a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [count, ...], where count is the number of leading<br />one bits in a (0..=256).<br /> |
| cto | Counts the number of trailing ones of an unsigned 256 bit integer.<br />Stack transition looks as follows:<br />[a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [count, ...], where count is the number of trailing<br />one bits in a (0..=256).<br /> |
| shl | Computes the left shift of an unsigned 256 bit integer.<br />The input value is assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[n, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = (a << n) mod 2^256.<br />Panics if n is not in the range [0, 256).<br /> |
| shr | Computes the right shift of an unsigned 256 bit integer.<br />The input value is assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[n, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = a >> n.<br />Panics if n is not in the range [0, 256).<br /> |
| rotl | Computes the left rotation of an unsigned 256 bit integer.<br />The input value is assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[n, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = rotl(a, n).<br />Panics if n is not in the range [0, 256).<br /> |
| rotr | Computes the right rotation of an unsigned 256 bit integer.<br />The input value is assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[n, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [c0, c1, c2, c3, c4, c5, c6, c7, ...], where c = rotr(a, n).<br />Panics if n is not in the range [0, 256).<br /> |
| divmod | Performs divmod of two unsigned 256 bit integers.<br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [r0, r1, r2, r3, r4, r5, r6, r7, q0, q1, q2, q3, q4, q5, q6, q7, ...],<br />where q = a / b and r = a % b. Panics if b is zero.<br /><br />Verification strategy: the prover hints (q, r) on the advice stack. We check that<br />(1) q * b + r = a as integers (no overflow at any step), and<br />(2) 0 <= r < b.<br />Together with uniqueness of Euclidean division, this guarantees q, r are correct.<br /> |
| div | Performs division of two unsigned 256 bit integers discarding the remainder.<br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [q0, q1, q2, q3, q4, q5, q6, q7, ...], where q = a / b. Panics if b is zero.<br /> |
| mod | Performs modulo operation of two unsigned 256 bit integers.<br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition looks as follows:<br />[b0, b1, b2, b3, b4, b5, b6, b7, a0, a1, a2, a3, a4, a5, a6, a7, ...]<br />-> [r0, r1, r2, r3, r4, r5, r6, r7, ...], where r = a mod b. Panics if b is zero.<br /> |