Reduce the small BitVec fragment that is definitionally Nat-backed: - `BitVec.toNat (BitVec.ofNat w n)` reduces to `n % 2^w` - `BitVec.ult w x y` reduces by evaluating `x.toNat < y.toNat` - `decide (x < y)` for BitVec reduces through the same comparison
(
&mut self,
e: &KExpr<M>,
)
| 2457 | if self.env.nat_succ_stuck.contains(&entry_key) { |
| 2458 | return Ok(None); |
| 2459 | } |
| 2460 | let mut visited: Vec<(super::env::Addr, super::env::CtxAddr)> = |
| 2461 | vec![entry_key]; |
| 2462 | let mut offset = num_bigint::BigUint::from(1u64); |
| 2463 | let mut cur = arg.clone(); |
| 2464 | |
| 2465 | loop { |
| 2466 | if let Some(result) = |
| 2467 | self.try_reduce_nat_succ_linear_rec(&cur, &offset)? |
| 2468 | { |
| 2469 | return Ok(Some(result)); |
| 2470 | } |
| 2471 | |
| 2472 | let w = self.whnf_with_nat_succ_mode(&cur, NatSuccMode::Stuck)?; |
| 2473 | if let Some(n) = extract_nat_lit(&w, &self.prims) { |
| 2474 | let result = Nat(&n.0 + &offset); |
| 2475 | let blob_addr = Address::hash(&result.to_le_bytes()); |
| 2476 | return Ok(Some(KExpr::nat(result, blob_addr))); |
| 2477 | } |
| 2478 | |
| 2479 | let (head, args) = collect_app_spine(&w); |
| 2480 | if let ExprData::Const(id, _, _) = head.data() |
| 2481 | && id.addr == self.prims.nat_succ.addr |
| 2482 | && args.len() == 1 |
| 2483 | { |
| 2484 | crate::perf::record_nat_succ_peel(); |
| 2485 | offset += 1u64; |
| 2486 | cur = args[0].clone(); |
| 2487 | let cur_key = self.whnf_key(&cur); |
| 2488 | if self.env.nat_succ_stuck.contains(&cur_key) { |
| 2489 | // Known-stuck suffix: the whole chain above it is stuck too. |
| 2490 | self.env.nat_succ_stuck.extend(visited); |
| 2491 | return Ok(None); |
| 2492 | } |
| 2493 | visited.push(cur_key); |
| 2494 | // The whnf'd form `succ(cur)` can also surface later as a |
| 2495 | // succ-iter argument; record it alongside the raw chain. |
no test coverage detected