## miden::core::math::u128
| Procedure | Description |
| ----------- | ------------- |
| overflowing_add | Performs addition of two unsigned 128 bit integers preserving the overflow.<br /><br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition is as follows:<br />[b0, b1, b2, b3, a0, a1, a2, a3, ...] -> [overflow, c0, c1, c2, c3, ...], where c = (a + b) % 2^128<br /> |
| widening_add | Performs addition of two unsigned 128 bit integers preserving the overflow with sum on top.<br /><br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition is as follows:<br />[b0, b1, b2, b3, a0, a1, a2, a3, ...] -> [c0, c1, c2, c3, overflow, ...], where c = (a + b) % 2^128<br /> |
| wrapping_add | Performs addition of two unsigned 128 bit integers discarding the overflow.<br /><br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition is as follows:<br />[b0, b1, b2, b3, a0, a1, a2, a3, ...] -> [c0, c1, c2, c3, ...], where c = (a + b) % 2^128<br /> |
| overflowing_sub | Performs subtraction of two unsigned 128 bit integers preserving the underflow.<br /><br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition is as follows:<br />[b0, b1, b2, b3, a0, a1, a2, a3, ...] -> [underflow, c0, c1, c2, c3, ...], where c = (a - b) % 2^128<br /> |
| wrapping_sub | Performs subtraction of two unsigned 128 bit integers discarding the underflow.<br /><br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition is as follows:<br />[b0, b1, b2, b3, a0, a1, a2, a3, ...] -> [c0, c1, c2, c3, ...], where c = (a - b) % 2^128<br /> |
| overflowing_mul | Performs multiplication of two unsigned 128 bit integers preserving the overflow.<br /><br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition is as follows:<br />[b0, b1, b2, b3, a0, a1, a2, a3, ...] -> [overflow, c0, c1, c2, c3, ...], where c = (a * b) % 2^128<br /><br />Schoolbook multiplication (LE layout with low limbs on top):<br /><br />a0 a1 a2 a3<br />x b0 b1 b2 b3<br />-------------------------------------------<br />(position) 0 1 2 3 4 5 6<br /><br />Partial products contributing to each position:<br />c0 (pos 0): a0*b0<br />c1 (pos 1): a1*b0 + a0*b1 + carries from pos 0<br />c2 (pos 2): a2*b0 + a1*b1 + a0*b2 + carries from pos 1<br />c3 (pos 3): a3*b0 + a2*b1 + a1*b2 + a0*b3 + carries from pos 2<br />overflow (pos 4+): a3*b1 + a2*b2 + a1*b3 + carries from pos 3<br />+ a3*b2 + a2*b3 (pos 5)<br />+ a3*b3 (pos 6)<br /><br /> |
| widening_mul | Performs multiplication of two unsigned 128 bit integers preserving the overflow with sum on top.<br />The input values are assumed to be represented using 32 bit limbs, but this is not checked.<br />Stack transition is as follows:<br />[b0, b1, b2, b3, a0, a1, a2, a3, ...] -> [c0, c1, c2, c3, overflow, ...], where c = (a * b) % 2^128<br /> |
| wrapping_mul | Performs multiplication of two unsigned 128 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 is as follows:<br />[b0, b1, b2, b3, a0, a1, a2, a3, ...] -> [c0, c1, c2, c3, ...], where c = (a * b) % 2^128<br /><br />Uses schoolbook multiplication with u32wrapping_madd for products contributing to c3<br />since overflow there doesn't affect the result.<br /> |
| eq | Compares two unsigned 128-bit integers for equality.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [result]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- result is 1 if a == b, and 0 otherwise.<br /><br />Invocation: exec<br /> |
| neq | Compares two unsigned 128-bit integers for inequality.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [result]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- result is 1 if a != b, and 0 otherwise.<br /><br />Invocation: exec<br /> |
| eqz | Compares an unsigned 128-bit integer to zero.<br /><br />Inputs: [a0, a1, a2, a3]<br />Outputs: [result]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- result is 1 if a == 0, and 0 otherwise.<br /><br />Invocation: exec<br /> |
| lt | Compares two unsigned 128-bit integers for a < b.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [result]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- result is 1 if a < b, and 0 otherwise.<br /><br />Invocation: exec<br /> |
| gt | Compares two unsigned 128-bit integers for a > b.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [result]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- result is 1 if a > b, and 0 otherwise.<br /><br />Invocation: exec<br /> |
| lte | Compares two unsigned 128-bit integers for a <= b.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [result]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- result is 1 if a <= b, and 0 otherwise.<br /><br />Invocation: exec<br /> |
| gte | Compares two unsigned 128-bit integers for a >= b.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [result]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- result is 1 if a >= b, and 0 otherwise.<br /><br />Invocation: exec<br /> |
| min | Computes the minimum of two unsigned 128-bit integers.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- c0 is the least significant 32-bit limb of min(a, b).<br />- c1 is the second 32-bit limb of min(a, b).<br />- c2 is the third 32-bit limb of min(a, b).<br />- c3 is the most significant 32-bit limb of min(a, b).<br /><br />Invocation: exec<br /> |
| max | Computes the maximum of two unsigned 128-bit integers.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- c0 is the least significant 32-bit limb of max(a, b).<br />- c1 is the second 32-bit limb of max(a, b).<br />- c2 is the third 32-bit limb of max(a, b).<br />- c3 is the most significant 32-bit limb of max(a, b).<br /><br />Invocation: exec<br /> |
| and | Computes bitwise AND of two unsigned 128-bit integers.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- c0 is the least significant 32-bit limb of (a AND b).<br />- c1 is the second 32-bit limb of (a AND b).<br />- c2 is the third 32-bit limb of (a AND b).<br />- c3 is the most significant 32-bit limb of (a AND b).<br /><br />Invocation: exec<br /> |
| or | Computes bitwise OR of two unsigned 128-bit integers.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- c0 is the least significant 32-bit limb of (a OR b).<br />- c1 is the second 32-bit limb of (a OR b).<br />- c2 is the third 32-bit limb of (a OR b).<br />- c3 is the most significant 32-bit limb of (a OR b).<br /><br />Invocation: exec<br /> |
| xor | Computes bitwise XOR of two unsigned 128-bit integers.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- b0 is the least significant 32-bit limb of b.<br />- b1 is the second 32-bit limb of b.<br />- b2 is the third 32-bit limb of b.<br />- b3 is the most significant 32-bit limb of b.<br />- c0 is the least significant 32-bit limb of (a XOR b).<br />- c1 is the second 32-bit limb of (a XOR b).<br />- c2 is the third 32-bit limb of (a XOR b).<br />- c3 is the most significant 32-bit limb of (a XOR b).<br /><br />Invocation: exec<br /> |
| not | Computes bitwise NOT of an unsigned 128-bit integer.<br /><br />Inputs: [a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- c0 is the least significant 32-bit limb of NOT(a).<br />- c1 is the second 32-bit limb of NOT(a).<br />- c2 is the third 32-bit limb of NOT(a).<br />- c3 is the most significant 32-bit limb of NOT(a).<br /><br />Invocation: exec<br /> |
| clz | Computes the number of leading zeros in an unsigned 128-bit integer.<br /><br />Inputs: [a0, a1, a2, a3]<br />Outputs: [count]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- count is the number of leading zero bits in a (0..=128).<br /><br />Invocation: exec<br /> |
| ctz | Computes the number of trailing zeros in an unsigned 128-bit integer.<br /><br />Inputs: [a0, a1, a2, a3]<br />Outputs: [count]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- count is the number of trailing zero bits in a (0..=128).<br /><br />Invocation: exec<br /> |
| clo | Computes the number of leading ones in an unsigned 128-bit integer.<br /><br />Inputs: [a0, a1, a2, a3]<br />Outputs: [count]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- count is the number of leading one bits in a (0..=128).<br /><br />Invocation: exec<br /> |
| cto | Computes the number of trailing ones in an unsigned 128-bit integer.<br /><br />Inputs: [a0, a1, a2, a3]<br />Outputs: [count]<br /><br />Where:<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- count is the number of trailing one bits in a (0..=128).<br /><br />Invocation: exec<br /> |
| shl | Computes a left shift of an unsigned 128-bit integer.<br /><br />Inputs: [n, a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- n is the shift amount in bits.<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- c0 is the least significant 32-bit limb of (a << n) mod 2^128.<br />- c1 is the second 32-bit limb of (a << n) mod 2^128.<br />- c2 is the third 32-bit limb of (a << n) mod 2^128.<br />- c3 is the most significant 32-bit limb of (a << n) mod 2^128.<br /><br />Panics if:<br />- n is not in the range [0, 128).<br /><br />Invocation: exec<br /> |
| shr | Computes a right shift of an unsigned 128-bit integer.<br /><br />Inputs: [n, a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- n is the shift amount in bits.<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- c0 is the least significant 32-bit limb of (a >> n).<br />- c1 is the second 32-bit limb of (a >> n).<br />- c2 is the third 32-bit limb of (a >> n).<br />- c3 is the most significant 32-bit limb of (a >> n).<br /><br />Panics if:<br />- n is not in the range [0, 128).<br /><br />Invocation: exec<br /> |
| rotl | Computes a left rotation of an unsigned 128-bit integer.<br /><br />Inputs: [n, a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- n is the rotation amount in bits.<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- c0 is the least significant 32-bit limb of rotl(a, n).<br />- c1 is the second 32-bit limb of rotl(a, n).<br />- c2 is the third 32-bit limb of rotl(a, n).<br />- c3 is the most significant 32-bit limb of rotl(a, n).<br /><br />Panics if:<br />- n is not in the range [0, 128).<br /><br />Invocation: exec<br /> |
| rotr | Computes a right rotation of an unsigned 128-bit integer.<br /><br />Inputs: [n, a0, a1, a2, a3]<br />Outputs: [c0, c1, c2, c3]<br /><br />Where:<br />- n is the rotation amount in bits.<br />- a0 is the least significant 32-bit limb of a.<br />- a1 is the second 32-bit limb of a.<br />- a2 is the third 32-bit limb of a.<br />- a3 is the most significant 32-bit limb of a.<br />- c0 is the least significant 32-bit limb of rotr(a, n).<br />- c1 is the second 32-bit limb of rotr(a, n).<br />- c2 is the third 32-bit limb of rotr(a, n).<br />- c3 is the most significant 32-bit limb of rotr(a, n).<br /><br />Panics if:<br />- n is not in the range [0, 128).<br /><br />Invocation: exec<br /> |
| div | Performs division of two unsigned 128-bit integers discarding the remainder.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3, ...]<br />Outputs: [q0, q1, q2, q3, ...]<br /><br />Where:<br />- a0..a3 are the 32-bit limbs of the dividend (a0 least significant).<br />- b0..b3 are the 32-bit limbs of the divisor (b0 least significant).<br />- q0..q3 are the 32-bit limbs of a / b (q0 least significant).<br /><br />Panics if:<br />- b is zero (divide by zero).<br /><br />Invocation: exec<br /> |
| mod | Performs modulo operation of two unsigned 128-bit integers.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3, ...]<br />Outputs: [r0, r1, r2, r3, ...]<br /><br />Where:<br />- a0..a3 are the 32-bit limbs of the dividend (a0 least significant).<br />- b0..b3 are the 32-bit limbs of the divisor (b0 least significant).<br />- r0..r3 are the 32-bit limbs of a % b (r0 least significant).<br /><br />Panics if:<br />- b is zero (divide by zero).<br /><br />Invocation: exec<br /> |
| divmod | Performs divmod operation of two unsigned 128-bit integers.<br /><br />Inputs: [b0, b1, b2, b3, a0, a1, a2, a3, ...]<br />Outputs: [r0, r1, r2, r3, q0, q1, q2, q3, ...]<br /><br />Where:<br />- a0..a3 are the 32-bit limbs of the dividend (a0 least significant).<br />- b0..b3 are the 32-bit limbs of the divisor (b0 least significant).<br />- q0..q3 are the 32-bit limbs of a / b (q0 least significant).<br />- r0..r3 are the 32-bit limbs of a % b (r0 least significant).<br /><br />Panics if:<br />- b is zero (divide by zero).<br /><br />Invocation: exec<br /><br />## Verification strategy<br /><br />The prover computes q and r natively and pushes them onto the advice stack. The verifier<br />checks two conditions that, by uniqueness of Euclidean division, guarantee correctness:<br /><br />(1) q * b + r = a (as integers)<br />(2) 0 <= r < b<br /><br />### Condition (1): column-by-column schoolbook verification<br /><br />The 256-bit product q * b (4 limbs x 4 limbs) has contributions to columns 0-6,<br />where column k = sum of q_i * b_j for all i+j=k:<br /><br />col 0: q0*b0<br />col 1: q1*b0 + q0*b1<br />col 2: q2*b0 + q1*b1 + q0*b2<br />col 3: q3*b0 + q2*b1 + q1*b2 + q0*b3<br />col 4: q3*b1 + q2*b2 + q1*b3<br />col 5: q3*b2 + q2*b3<br />col 6: q3*b3<br /><br />For each column k in 0..3, we compute: sum_k = (column_k products) + r_k + carry_{k-1},<br />then assert sum_k mod 2^32 = a_k, and propagate carry_k = sum_k / 2^32 to the next column.<br /><br />After column 3, we assert carry_3 = 0 (no carry out of the lower 128 bits).<br />We also assert that all 6 products in columns 4-6 are individually zero.<br /><br />Together: carry_3 = 0 means no carry flows from column 3 into column 4, and zero products<br />in columns 4-6 means no direct contributions there either. So q*b + r has zero upper bits,<br />i.e., q*b + r < 2^128. Combined with the per-column a_k assertions, this proves<br />q*b + r = a as integers.<br /><br />### Condition (2): strict remainder bound<br /><br />An inline lexicographic comparison verifies r < b (strict), cascading from LSB to MSB.<br />Combined with u32assertw on r (ensuring each limb is a valid u32), this gives 0 <= r < b.<br /> |