fix: use iterator.seq() for frame mapping for Verus breaking change

[Marsman1996]

No description provided.

[Marsman1996]

Updated: fixed by the fix: no error error commit

---

Well, strange error message...

error: assertion failed
   --> /home/yuwei/ruzykaller/kverus/database/verified/code/ostd/src/../specs/mm/page_table/cursor/owners.rs:850:16
    |
850 |         assert(self.va.inv());
    |                ^^^^^^^^^^^^^ assertion failed

note: diagnostics via expansion

note: 

(mut_ref_current(self)).va.inv()
|   let tmp%% = 0;
|       let tmp%% = (mut_ref_current(self)).va.offset;
|           let tmp%% = PAGE_SIZE();
|               tmp%% <= tmp%% ✔
|               tmp%% < tmp%% ✔
|   (mut_ref_current(self)).va.index.dom() =~= new((|i| let tmp%% = 0 in let tmp%% = i in let tmp%% = NR_LEVELS() in tmp%% <= tmp%% && tmp%% < tmp%%)) ✔
|   forall |i|
|       let tmp%% = 0 in let tmp%% = i in let tmp%% = NR_LEVELS() in tmp%% <= tmp%% && tmp%% < tmp%% ==>
|           (mut_ref_current(self)).va.index.dom().contains(i) ✔
|           let tmp%% = 0;
|               let tmp%% = (mut_ref_current(self)).va.index.index(i);
|                   let tmp%% = NR_ENTRIES();
|                       tmp%% <= tmp%% ✔
|                       tmp%% < tmp%% ✔
|   let tmp%% = 0;
|       let tmp%% = (mut_ref_current(self)).va.leading_bits;
|           let tmp%% = 65536;
|               tmp%% <= tmp%% ✔
|               tmp%% < tmp%% ✔
+---

    NOTE: Verus failed to prove an assertion even though all of its
    sub-assertions succeeded. This is usually unexpected, and it may
    indicate that the proof is "flaky". It might also be a result
    of additional expressions in the triggering context in the expanded
    version.

[Marsman1996]

Weeeell, it of course will fail the CI...

[rikosellic]

/ci-upstream-verus

[rikosellic]

According to the migration guide, we should use it.seq() instead of the raw snapshot definition.

[rikosellic]

/ci-upstream-verus