Enum discriminant completeness

[nishanthkarthik]

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.

Adding

  axiom oneof {
    forall self: Snap$m_T$_beg_$_end_ :: {discriminant$__$TY$__Snap$m_T$_beg_$_end_$Snap$m_T$_beg_$_end_$$int$(self)}
      self == cons$0$__$TY$__Snap$m_T$_beg_$_end_$Snap$m_T$_beg_$_end_() ||
      self == cons$1$__$TY$__Snap$m_T$_beg_$_end_$Snap$m_T$_beg_$_end_() ||
      self == cons$2$__$TY$__Snap$m_T$_beg_$_end_$Snap$m_T$_beg_$_end_()
  }

makes test_biject_1 verify. Credits to @zgrannan for the tip.