add better syntax for external_fn_specification

[tjhance]

external_fn_specification is ugly and hard to read. This adds better syntax

examples:

pub assume_specification<T> [core::mem::swap::<T>] (a: &mut T, b: &mut T)
     ensures
         *a == *old(b),
         *b == *old(a),

For trait methods:

pub assume_specification [<bool as Clone>::clone](b: &bool) -> (res: bool)
    returns b;

The brackets make it easier to parse.

[tjhance]

if this syntax seems fine, i will port all the instances in vstd/std_specs and change all the error msgs and update docs etc.

[jaybosamiya-ms]

I like the new syntax. Let me know if you need help with adding it to verusfmt.

[tjhance]

@jaybosamiya-ms Indeed, if you add this to verusfmt, it would be a big help.

[parno]

Thanks for adding the cleaner syntax and for adding documentation! I notice that the new documentation lives under the "Reference" section at the end. Could we add at least a small pointer to it in the "Tutorial: Verification and Rust" section, possibly either as a top-level (short) chapter, or as a page under "Understanding the guarantees of a verified program"? The "Verification and Rust" section seems like the most likely spot for someone to look for this functionality, and I'm not sure they would immediately think to look under "assume_specification" in the Reference.

[jaybosamiya-ms]

Latest release of verusfmt (v0.5.1) contains support for assume_specification; it should automatically be picked up by the CI upon your next push to this PR.

[tjhance]

Tyvm!

Bryan: I will add a bit more introductory documentation like you suggest.