Function covers_var

crates/kernel/src/level.rs:595–599

Check whether some entry `(p2, n2)` in `l2` with `p2 ⊆ p1` contains a variable node that dominates `(w, off)`: i.e., some `v ∈ n_p2.var` with `v.idx == w && v.offset >= off`. Because `v.idx` is always in `p2`, the matching p2 automatically has `w ∈ p2 ⊆ p1`, keeping the branch analysis consistent.

(l2: &NormLevel, p1: &[u64], w: u64, off: u64)

    is_subset(p2, p1)
      && (c <= n2.constant || n2.var.iter().any(|v| c <= v.offset + 1))
  })
}

/// Check whether some entry `(p2, n2)` in `l2` with `p2 ⊆ p1` contains a
/// variable node that dominates `(w, off)`: i.e., some `v ∈ n_p2.var` with
/// `v.idx == w && v.offset >= off`. Because `v.idx` is always in `p2`, the
/// matching p2 automatically has `w ∈ p2 ⊆ p1`, keeping the branch analysis
/// consistent.