Setup verification

[ziqiaozhou]

• Set up verification tool and add verification CI.
  Change the minimum rust version to 1.77 since the verification tool still needs some efforts to support 1.80. This will not change the default version in non-verification mode, since rust-toolchain.toml specifies 1.80.
• cargo verify in kernel folder will run verification for functions that annotated with #[verus_verify]
• Added new crates verify_proof and verify_external, which will import the minimum required spec and proofs to help SVSM to do efficient proofs and stub out external crates.
• Add some proofs for address.rs as a basic example to show how verification works.
• ./script/vfmt.sh will do enhanced formatting for code ending with .verus.rs

[ziqiaozhou]

I have updated tool to support Rust-1.82, improved the verification document, and marked the verify.yml as manually triggered CI so that I can still run CI in my forked repo before sending my change here. I can remove it if you prefer to not keeping the manually-triggered CI.

[joergroedel]

I followed the documentation and ran a successful verification, but the process generated a few warnings which I'd like to see fixed:

warning: verus-related attribute has no effect because Verus is already ignoring this item. You may need to mark it as `#[verifier::verify]`.
  --> verify_proof/src/lib.rs:16:1
   |
16 | global size_of usize == 8;
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: broadcast functions should have explicit #[trigger] or #![trigger ...]
   --> verify_proof/src/bits.verus.rs:248:9
    |
248 |         pub broadcast proof fn $pname()
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...
347 | bit_shl_values! {u64, u64, 1u64, lemma_bit_u64_shl_values}
    | ---------------------------------------------------------- in this macro invocation
    |
    = note: this warning originates in the macro `bit_shl_values` (in Nightly builds, run with -Z macro-backtrace for more info)

warning: broadcast functions should have explicit #[trigger] or #![trigger ...]
   --> verify_proof/src/bits.verus.rs:248:9
    |
248 |         pub broadcast proof fn $pname()
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...
351 | bit_shl_values! {usize, u64, 1usize, lemma_bit_usize_shl_values}
    | ---------------------------------------------------------------- in this macro invocation
    |
    = note: this warning originates in the macro `bit_shl_values` (in Nightly builds, run with -Z macro-backtrace for more info)

verification results:: 0 verified, 0 errors
warning: `verify_proof` (lib) generated 3 warnings
note: preparing crate for verification

warning: broadcast functions should have explicit #[trigger] or #![trigger ...]
   --> /home/joro/src/svsm/verify_proof/src/bits.verus.rs:248:9
    |
248 |         pub broadcast proof fn $pname()
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Also, please look at the other review comments I left.

[ziqiaozhou]

I followed the documentation and ran a successful verification, but the process generated a few warnings which I'd like to see fixed:

warning: verus-related attribute has no effect because Verus is already ignoring this item. You may need to mark it as `#[verifier::verify]`.
  --> verify_proof/src/lib.rs:16:1
   |
16 | global size_of usize == 8;
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: broadcast functions should have explicit #[trigger] or #![trigger ...]
   --> verify_proof/src/bits.verus.rs:248:9
    |
248 |         pub broadcast proof fn $pname()
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...
347 | bit_shl_values! {u64, u64, 1u64, lemma_bit_u64_shl_values}
    | ---------------------------------------------------------- in this macro invocation
    |
    = note: this warning originates in the macro `bit_shl_values` (in Nightly builds, run with -Z macro-backtrace for more info)

warning: broadcast functions should have explicit #[trigger] or #![trigger ...]
   --> verify_proof/src/bits.verus.rs:248:9
    |
248 |         pub broadcast proof fn $pname()
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...
351 | bit_shl_values! {usize, u64, 1usize, lemma_bit_usize_shl_values}
    | ---------------------------------------------------------------- in this macro invocation
    |
    = note: this warning originates in the macro `bit_shl_values` (in Nightly builds, run with -Z macro-backtrace for more info)

verification results:: 0 verified, 0 errors
warning: `verify_proof` (lib) generated 3 warnings
note: preparing crate for verification

warning: broadcast functions should have explicit #[trigger] or #![trigger ...]
   --> /home/joro/src/svsm/verify_proof/src/bits.verus.rs:248:9
    |
248 |         pub broadcast proof fn $pname()
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Also, please look at the other review comments I left.

The warnings are removed. You need to run cargo v prepare-verus before cargo verify since I upgraded the verus version to avoid one warning due to mismatched version.