[compiler-v2] Generic TypeInfo verification broken

[wrwg]

Consider code like:

module app::m {
    use aptos_stdlib::type_info;
    
    fun generic_type_info_verification_target<A>(): type_info::TypeInfo {
       type_info::type_of<A>()
    }
    spec generic_type_info_verification_target {
        ensures result == generic_type_info_verification_target<A>();
    }
}

This yields in the following Boogie compilation error:

Move prover returns: [internal] boogie exited with compilation errors:
type_reflection.bpl(5059,26): Error: cannot refer to a global variable in this context: #0_info
type_reflection.bpl(5059,38): Error: cannot refer to a global variable in this context: #0_info
type_reflection.bpl(5059,50): Error: cannot refer to a global variable in this context: #0_info

This seems to be a bug in the new specification function inferrer shared between compiler v1 and v2. The native function type_info::type_of cannot be called from a specification function as it refers to type reflection state #0_info.