Fix Verus: remove int bitwise ops in cpu_mask spec (int has no spec_bitand)

avrabe · avrabe · commit f365bead7be5 · 2026-04-02T20:31:34.000-04:00
diff --git a/src/cpu_mask.rs b/src/cpu_mask.rs
@@ -53,12 +53,12 @@ pub struct CpuMaskResult {
 /// Spec-level power-of-2 check: exactly one bit set.
 /// A value `m` has exactly one bit iff `m != 0 && (m & (m - 1)) == 0`.
 pub open spec fn is_power_of_two(m: u32) -> bool {
-    m != 0 && (m as int) & ((m as int) - 1) == 0
+    m != 0 && (m & (m - 1)) == 0
 }
 
 /// Spec-level mask computation.
 pub open spec fn compute_mask(current: u32, enable: u32, disable: u32) -> u32 {
-    ((current | enable) & !disable) as u32
+    (current | enable) & !disable
 }
 
 // ------------------------------------------------------------------

Original file line number	Diff line number	Diff line change
`@@ -53,12 +53,12 @@ pub struct CpuMaskResult {`
`53`	`53`	`/// Spec-level power-of-2 check: exactly one bit set.`
`54`	`54`	/// A value `m` has exactly one bit iff `m != 0 && (m & (m - 1)) == 0`.
`55`	`55`	`pub open spec fn is_power_of_two(m: u32) -> bool {`
`56`		`- m != 0 && (m as int) & ((m as int) - 1) == 0`
	`56`	`+ m != 0 && (m & (m - 1)) == 0`
`57`	`57`	`}`
`58`	`58`
`59`	`59`	`/// Spec-level mask computation.`
`60`	`60`	`pub open spec fn compute_mask(current: u32, enable: u32, disable: u32) -> u32 {`
`61`		`- ((current \| enable) & !disable) as u32`
	`61`	`+ (current \| enable) & !disable`
`62`	`62`	`}`
`63`	`63`
`64`	`64`	`// ------------------------------------------------------------------`