[Bug][Prover] Enum Data Invariants Incorrectly Enforced

[JakeSilverman]

🐛 Bug

There is an issue with how data invariants are enforced in enum types.

To reproduce

The following program

module 0x42::M {

    struct Foo {
        foo: u64,
    }

    struct Bar {
        bar: u64,
    }

    spec Bar{
        invariant self.bar >= 0;
    }

    enum Foobar {
        First {
            foo: Foo,
        },
        Second {
            bar: Bar,
        }
    }

    fun add_one_if_first(self: &mut Foobar) {
        match(self) {
            Foobar::First { foo } => foo.foo = foo.foo + 1,
            Foobar::Second { bar } => bar.bar = bar.bar + 1,
        }
    }
}

will give the error

error: data invariant does not hold
   ┌─ /Users/jake/Desktop/basic_coin/sources/first_module.move:12:9
   │
12 │         invariant self.bar >= 0;
   │         ^^^^^^^^^^^^^^^^^^^^^^^^

when attempting to prove. But this data invariant should be trivial to prove (especially since bar is u64). It seems to have to do with enforcement of the Bar data invariant on the foo path.

Expected Behavior

The above program should verify.

System information

Please complete the following information:
Aptos Core Version: 0ff932a (Jul 21 latest commit)
Rust Version: 1.87.0
Computer OS: macOS 15.5
Boogie version: 3.5.1.0

[JakeSilverman]

Here is another test case to check the solution against:

module 0x42::M {
    use std::signer;

    struct FirstStruct has copy, drop, store{
        fsnum: u64,
    }

    struct SecondStruct has copy, drop, store {
        ssnum : u64,
    }

    spec FirstStruct {
        invariant self.fsnum >= 666;
    }

    spec module {
        invariant (forall a: address : 
            exists<Foobar>(a) ==> 
                ((global<Foobar>(a) is Jake) ==> global<Foobar>(a).foo.fsnum >= 666));
    }

    enum InnerEnum has copy, drop, store {
        Alpha { value: FirstStruct },
        Beta { value: SecondStruct }
    }

    enum Foobar has copy, drop, store, key {
        Jake {
            foo: FirstStruct,
        },
        Silverman {
            bar: SecondStruct,
        }
    }

    enum NestedEnum has copy, drop, store, key {
        Outer {
            foobar: Foobar,
            inner: InnerEnum,
        }
    }

    fun add_one_if_first(account: &signer) acquires Foobar {
        let addr = signer::address_of(account);
        let foobar_ref = borrow_global_mut<Foobar>(addr);
        
        match(foobar_ref) {
            Foobar::Jake { foo } => foo.fsnum = 666,
            Foobar::Silverman { bar } => bar.ssnum = 555,
        }
    }

    fun test_nested_enum(account: &signer) acquires NestedEnum {
        let addr = signer::address_of(account);
        let nested_ref = borrow_global_mut<NestedEnum>(addr);
        
        match(nested_ref) {
            NestedEnum::Outer { foobar, inner } => {
                match(foobar) {
                    Foobar::Jake { foo } => {
                        match(inner) {
                            InnerEnum::Alpha { value } => {
                                foo.fsnum = 666;
                                value.fsnum = 666;
                            },
                            InnerEnum::Beta { value } => {
                                foo.fsnum = 888;
                                value.ssnum = 999;
                            }
                        }
                    },
                    Foobar::Silverman { bar } => {
                        match(inner) {
                            InnerEnum::Alpha { value } => {
                                bar.ssnum = 111;
                                value.fsnum = 666;
                            },
                            InnerEnum::Beta { value } => {
                                bar.ssnum = 333;
                                value.ssnum = 444;
                            }
                        }
                    }
                }
            }
        }
    }
}

This should pass verifcation, but changing the line

                            InnerEnum::Alpha { value } => {
                                foo.fsnum = 666;

to

                            InnerEnum::Alpha { value } => {
                                foo.fsnum = 333;

should cause invariant violation.