Add proof_with() and declare_with() builtin functions for ghost/track…

[ziqiaozhou]

…ed args

Why: to allow with spec in verus_spec for traits and external functions.

• Add builtin API: proof_with(), declare_with() (plus aliases declare_with_tracked/declare_with_ghost for backward compatibility)

• Infer Tracked vs Ghost mode from the type annotation via ADT DefId

• Add VIR lowering in fn_call_to_vir.rs with type and mode checking

• Add pre-scan for declare_with params in rust_to_vir_func.rs

• Add proof_with test suite

• Add first-pass lifetime checking to ensure that tracked/ghost arguments passed via proof_with() satisfy the lifetime constraints declared by declare_with() in the callee.

• Add proof_with_lifetime.rs module with region-aware lifetime checking

• Use rustc_hir_analysis::lower_ty() to preserve real regions instead of erased regions from typeck writeback

• Check that argument regions outlive expected parameter regions using the function's where-clause predicates

• Add test cases for lifetime mismatch detection (both Tracked and Ghost)

For trait methods, #[verus_spec(with...)] and proof_with! pair should rewrite code to following style

use vstd::prelude::*;
struct A {
    a: u64
}

trait AOp {
    fn test(&self) {
        let b: Tracked<u64> = declare_with();
        let c: Ghost<u32> = declare_with();
        requires(b@ == 1 && c@ == 2);
    }
}
impl AOp for A {
    fn test(&self)
    {
        let b: Tracked<u64> = declare_with();
        let c: Ghost<u32> = declare_with();
        assert(b@ == 1);
        assert(c@ == 0); // FAILS
    }
}
fn call_test() {
    let a = A { a: 0 };
    proof_with((Tracked(1u64), Ghost(2u32)), a.test());
}

#[verifier(external)]
fn unverified_call_test() {
    let a = A { a: 0 };
    a.test();
}

For external functions, we need to expand assume_specification and proof_with! to rewrite code in following style

use vstd::prelude::*;
#[verifier(external)]
fn negate_bool(b: bool, x: u8) -> bool {
    !b
}

#[verifier(external_fn_specification)]
fn negate_bool_requires_ensures(b: bool, x: u8) -> bool
{
    let extra: Tracked<u8> = declare_with();
    requires(x == extra@);
    ensures(|ret_b: bool| ret_b == !b);
    negate_bool(b, x)
}

fn call_test() {
    proof_with(Tracked(1u8), negate_bool(true, 1));
}

#[verifier(external)]
fn unverified_call_test() {
    negate_bool(true, 1);
}

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