This might be related to #1391. Prusti does not generate an axiom to prove the bijection between an enum's constructor and its discriminant in case of the simple no-argument enum.
#[derive(PartialEq, Eq, Copy, Clone)]
#[repr(u16)]
enum T {
I1 = 1,
I2 = 2,
I3 = 3,
}
impl T {
#[pure]
#[ensures(1 <= result && result <= 3)]
#[ensures(matches!(self, T::I1) <==> result == 1)]
#[ensures(matches!(self, T::I2) <==> result == 2)]
#[ensures(matches!(self, T::I3) <==> result == 3)]
fn f(&self) -> u16 {
match self {
T::I1 => 1,
T::I2 => 2,
T::I3 => 3,
}
}
#[ensures(a.f() == b.f() <==> a == b)]
fn test_biject_2(a: T, b: T) {}
#[ensures(forall(|t: T| a == t <==> a.f() == t.f()))]
fn test_biject_1(a: T) {
let _ = T::I1; // added to generate axioms about discriminants
let _ = T::I2;
let _ = T::I3;
}
}
Expected: Both test_biject_2 and test_biject_1
Actual: Only test_biject_2 verifies.
This might be related to #1391. Prusti does not generate an axiom to prove the bijection between an enum's constructor and its discriminant in case of the simple no-argument enum.
Expected: Both
test_biject_2
andtest_biject_1
Actual: Onlytest_biject_2
verifies.Adding
makes
test_biject_1
verify. Credits to @zgrannan for the tip.