[Feature Request][Move prover] Specification for lambda expressions

[rahxephon89]

🚀 Feature Request

To prove inline functions with lambda expressions, we may want to extend the specification language to support function-level specification for lambda expressions. The syntax is not determined yet but one possible solution is to attach a spec block to the lambda expression where pre- and post-conditions are provided.

    vector::for_each_mut(&mut registry.packages, |pack| {
        let package: &mut PackageMetadata = pack;
        package.upgrade_policy = upgrade_policy_immutable();
	    }
	    spec {
	        ensures pack.upgrade_policy == upgrade_policy_immutable();
	    }
    );