`is_older_version` function violates anti-symmetry at boundary condition (version difference = 2^31)

[yanfenghu]

Hi,

I found a potential bug in the is_older_version function through Kani formal verification. The function violates the anti-symmetry property at a boundary condition.

Location: src/util.rs:25

Current Code:

pub fn is_older_version(a: u32, b: u32) -> bool {
let diff = a.wrapping_sub(b);
diff >= (1 << 31) // Should be > not >=
}
Problem:

When two versions differ by exactly 2^31, both is_older_version(a, b) and is_older_version(b, a) return true, violating anti-symmetry:

let a = 0u32;
let b = 0x80000000u32; // 2^31

// Both return true - violates anti-symmetry!
assert!(is_older_version(a, b) == true); // a is older than b?
assert!(is_older_version(b, a) == true); // b is also older than a??
Impact:

Incorrect version comparison in slot map operations

Potential data integrity issues when version numbers reach the boundary

Confusion in key validity checks

Suggested Fix:

pub fn is_older_version(a: u32, b: u32) -> bool {
let diff = a.wrapping_sub(b);
diff > (1 << 31) // Change >= to >
}
This maintains anti-symmetry: when diff == 2^31, neither version is considered “older”.

Could you please confirm if this is a valid bug? I’d be happy to submit a PR if needed.