| 3803 | || *addr == p.nat_mod.addr |
| 3804 | || *addr == p.nat_gcd.addr |
| 3805 | { |
| 3806 | la.saturating_mul(lb) |
| 3807 | } else if *addr == p.nat_pow.addr { |
| 3808 | let lo = la.max(lb); |
| 3809 | lo.saturating_mul(lo) |
| 3810 | } else { |
| 3811 | la.max(lb) |
| 3812 | }; |
| 3813 | crate::profile::bump_nat_arith(work); |
| 3814 | } |
| 3815 | let r = if *addr == p.nat_add.addr { |
| 3816 | &a.0 + &b.0 |
| 3817 | } else if *addr == p.nat_sub.addr { |
| 3818 | if a.0 >= b.0 { &a.0 - &b.0 } else { zero } |
| 3819 | } else if *addr == p.nat_mul.addr { |
| 3820 | &a.0 * &b.0 |
| 3821 | } else if *addr == p.nat_div.addr { |
| 3822 | if b.0 == zero { zero } else { &a.0 / &b.0 } |
| 3823 | } else if *addr == p.nat_mod.addr { |
| 3824 | if b.0 == zero { a.0.clone() } else { &a.0 % &b.0 } |
| 3825 | } else if *addr == p.nat_pow.addr { |
| 3826 | // Limit matches C++ kernel `ReducePowMaxExp` and lean4lean `reducePowMaxExp`. |
| 3827 | const REDUCE_POW_MAX_EXP: u64 = 1 << 24; // 16_777_216 |
| 3828 | match b.to_u64() { |
| 3829 | #[allow(clippy::cast_possible_truncation)] // guarded: exp <= 2^24 |