Check that Invariant implementations refer to every field and every enum variant

[celinval]

Requested feature: Implementing an Invariant can be error prone and may lead to invalid symbolic variable generation or unsound assertions.
Use case: Users implementing Invariant for their custom enums and structs.
Link to relevant documentation (Rust reference, Nomicon, RFC):
Is this a breaking change? No

struct Header {
    type: Type,
    size: usize,
}

unsafe impl Invariant for Header {
    fn is_valid() -> bool {
        type.is_valid()
    }
}

We should also provide an attribute to suppress the warning if some fields were left out on purpose. E.g.:

struct Header {
    type: Type,
    data: u128,
}

unsafe impl Invariant for Header {
    #[rmc::allow_unchecked]
    fn is_valid() -> bool {
        type.is_valid()
    }
}

[tedinski]

With invariant removed, this is no longer relevant.