Method try_reduce_bitvec_ult

crates/kernel/src/whnf.rs:2494–2535

(
    &mut self,
    width: &KExpr<M>,
    lhs: &KExpr<M>,
    rhs: &KExpr<M>,
  )

    if self.env.nat_succ_stuck.contains(&entry_key) {
      return Ok(None);
    }
    let mut visited: Vec<(super::env::Addr, super::env::CtxAddr)> =
      vec![entry_key];
    let mut offset = num_bigint::BigUint::from(1u64);
    let mut cur = arg.clone();

    loop {
      if let Some(result) =
        self.try_reduce_nat_succ_linear_rec(&cur, &offset)?
      {
        return Ok(Some(result));
      }

      let w = self.whnf_with_nat_succ_mode(&cur, NatSuccMode::Stuck)?;
      if let Some(n) = extract_nat_lit(&w, &self.prims) {
        let result = Nat(&n.0 + &offset);
        let blob_addr = Address::hash(&result.to_le_bytes());
        return Ok(Some(KExpr::nat(result, blob_addr)));
      }

      let (head, args) = collect_app_spine(&w);
      if let ExprData::Const(id, _, _) = head.data()
        && id.addr == self.prims.nat_succ.addr
        && args.len() == 1
      {
        crate::perf::record_nat_succ_peel();
        offset += 1u64;
        cur = args[0].clone();
        let cur_key = self.whnf_key(&cur);
        if self.env.nat_succ_stuck.contains(&cur_key) {
          // Known-stuck suffix: the whole chain above it is stuck too.
          self.env.nat_succ_stuck.extend(visited);
          return Ok(None);
        }
        visited.push(cur_key);
        // The whnf'd form `succ(cur)` can also surface later as a
        // succ-iter argument; record it alongside the raw chain.
        let w_key = self.whnf_key(&w);
        visited.push(w_key);
        continue;
      }

      self.env.nat_succ_stuck.extend(visited);
      return Ok(None);
    }