Rustc 1.84.0

[utaal]

I think we now want to directly target 1.84, and skip 1.82 (#1330).

This is based on @ziqiaozhou's PR #1325 rebased after rustc-1.72.0 was merged, and on #1330.

• fix interface changes
• find proper solution to proof in consts with new const eval
• add vargo fmt commit to list of ignored revs

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[utaal]

We're going to need a solution to this:

#1330 (comment)

I rebased on top of main, where I added the test for

        #[verifier::opaque]
        spec fn f() -> int { 1 }
        proof fn e() -> (u: u64)
            ensures
                u == f(),
                u == 1
        {
            reveal(f);
            1
        }
        exec const E: u64 ensures E == f() {
            proof {
                let x = e();
                assert(x == f());
                assert(x == 1);
            }
            assert(1 == f());
            1
        }

which is something that projects use but was untested. We need a solution for that before merging (I'm open to alternative ideas to the const-eval hack).

[utaal]

#1330 (comment)

We could restrict proof in consts and const fn to appear in a single block at the top of the function, and move it into a closure, like I did for the rest of the header. A bit limiting, but maybe good enough. /cc @Chris-Hawblitzel @tjhance

[tjhance]

What about this? This code:

        exec const E: u64 ensures E == f() {
            proof {
                let x = e();
                assert(x == f());
                assert(x == 1);
            }
            assert(1 == f());
            1
        }

Could be translated by the syntax macro into:

const E: u64 = 1;

fn verus_proof_for_E() -> u64 {
    /* body with proof goes here */
}

(Though honestly, I'm tempted to try to solve this on the design level ... there's something really ugly about const items with proof blocks, even though I understand some people have found uses for them.)