New attribute-based syntax for exec function specifications

[Chris-Hawblitzel]

This follows up the discussion in #1297 to replace the exec function requires/ensures attributes from #1297 with a single general-purpose attribute for exec function specifications that uses the familiar verus! syntax inside the exec function attribute. This pull request also tries to consolidate some code that was duplicated between the verus! and attribute-based syntax implementations.

Note that, as with #1297, this attribute-based syntax is an alternative to the verus! syntax for those who want such an alternative (see, for example, #1100 ). We do not intend to remove the verus! syntax. In particular, spec functions and proof functions are still always written using verus!, while exec functions can use either syntax.

The new function attribute syntax looks like:

#[verus_spec(sum =>
    requires
        x < 100,
        y < 100,
    ensures
        sum < 200,
)]
fn my_exec_fun(x: u32, y: u32) -> u32 {
    x + y
}

See example/syntax_attr.rs for more complete examples.

The new attribute name verus_spec avoids conflicts with verus_verify, which can still be used independently for things like verus_verify(external_body).

The attribute syntax for loop invariants remains the same as in #1297 .

[ziqiaozhou]

The change works well in both verification and non-verification build modes in my COCONUT change.

[ziqiaozhou]

The example below does not show how to use tracked/ghost ? Did I miss some changes to support tracked/ghost variable in verus_spec?

[ziqiaozhou]

I haven't used the invariant for loop in coconut code yet. But I am wondering whether the final format of loop specification will also be changed to

#[verus_spec(
invariant
   xxx
decreases
   xxx
)]?