=~= not doing its thing on a simple Option; maybe an extensionality problem for additive types?

[jonhnet]

In the before file, Verus fails to prove this extensional equality:

        assert( post.iptr(ptr) =~= PagedJournal_v::JournalRecord::discard_old_journal_rec(self.iptr(ptr), lsn) );

In the after file, I "fix" it by beginning a manual proof of extensional equality on the branches of the Option. Once I prove that the Option legs match, Verus is happy.

2023-07-24-15-01-48.zip
2023-07-24-15-01-54.zip

[utaal]

#[verifier::ext_equal] was missing on the specification for core::option::Option (#707), but I think this function suffers from instability; adding and removing #[verifier::spinoff_prover] changes the outcome.

[utaal]

It seems verus usually needs

        assert(post.iptr(ptr).is_Some() == PagedJournal_v::JournalRecord::discard_old_journal_rec(self.iptr(ptr), lsn).is_Some());

to prove extensional equality. Can you spell out the argument why this is true? (which definitions / lemmas this comes from)