Codegen struggles to infer information about a value computed before branching on related info

Explanation:

/// basically what the function looks like in core
fn strict_sub(x: u128, y: u128) -> u128 {
      let (diff, over) = x.overflowing_sub(y);
      if over { panic!() } else { diff }
}
/// this is better for some reason
fn strict_sub_1liner(x: u128, y: u128) -> u128 {
      if x <= y { panic!() } else { x - y }
}

/// Performs the Lucas Lehmer Test to see if `2^exp - 1` is prime.
/// Panics if `2^exp` does not fit in a u64.
pub fn lucas_lehmer_u64(exp: u8) -> bool {
    let n64: u64 = 1u64.strict_shl(exp as u32) - 1;
    let n: u128 = n64 as u128;
    
    let mut k: u128 = 4;
    
    // swapping out `strict_sub` here for `strict_sub_1line` allows the compiler to
    // figure out that the `strict_add` later won't panic.
    // For context, that wont panic because `k` is always less then `n` at the end and
    // `n` can fit in a `u64` so if you square it it won't be too large to then add a `n_m2`
    // if that also fits in a `u64` (basically the idea behind the `carrying_mul`  and 
    // `carrying_mul_add` function). 
    // If `n_m2` were to underflow, it won't fit anymore and the `strict_add` can overflow.
    let n_m2 = strict_sub(n, 2);
    
    let mut i = 2;
    
    while i < exp {
        k = (k*k).strict_add(n_m2);
        unsafe {
            k = (k & n).unchecked_add(k >> exp);
            k = (k & n).unchecked_add(k >> exp);
        }
        k = core::hint::select_unpredictable(k == n, 0, k);
        // above 3 statements perform `k mod n` so `k` is less then `n`
        unsafe { core::hint::assert_unchecked(k < n) }
        i += 1;
    }
    k == 0
}

godbolt link: https://godbolt.org/z/h4Gcn4Pvz

Start with the Godbolt reproduction and compare code generation for strict_sub and strict_sub_1liner in the Lucas–Lehmer example. Trace how the compiler reasons about the overflowing_sub result before the branch and how that affects the later strict_add. Done means the differing inference or code-generation behavior is understood and the issue has a verified compiler-side resolution.