[move-prover] collect types in write-back chain for mono analysis

[awelc]

Motivation

It cherry picks a commit from the main branch whose corresponding PR (https://github.com/move-language/move/pull/872) has the following description.

In mono analysis, an implicit assumption is that all types used in the function body will appear either in parameters, locals, return tyupes, or spec exprs.

While this is true and in a rigourous implemention, should hold, it might be hit by a cornor case where an imcomplete (and potentially) inconsistent modeling of borrow natives are in place.

An example is shown in the dynamic_field::borrow_mut model:

module sui::dynamic_field {
    struct Field<Name: copy + drop + store, Value: store> has key {
        id: UID,
        name: Name.
        value: Value,
    }

    public fun borrow_mut<Name: copy + drop + store, Value: store>(
        object: &mut UID,
        name: Name,
    ): &mut Value {
        let object_addr = object::uid_to_address(object);
        let hash = hash_type_and_key(object_addr, name);
        let field = borrow_child_object_mut<Field<Name, Value>>(object, hash);
        &mut field.value
    }
    spec borrow_mut {
        pragma opaque;
    }

    public(friend) native fun borrow_child_object_mut<Child: key>(object: &mut UID, id: address): &mut Child;
}

With a declaration of in the prover CLI:

        options
            .prover
            .borrow_natives
            .push("dynamic_field::borrow_child_object_mut".to_string());
        options.backend.borrow_aggregates.push(
            move_prover_boogie_backend::options::BorrowAggregate::new(
                "dynamic_field::borrow_child_object_mut".to_string(),
                "GetDynField".to_string(),
                "UpdateDynField".to_string(),
            ),
        );

Now, the opaque pragma in borrow_mut mark that this funciton is abstract and when this borrow_mut is used, it actually causes an write-back to the internal Field struct which does not show-up in the function locals (or anything that is collected by mono analysis that has a type).

Of course in an ideal situation, the borrow_mut should be modeled completely such that the Field struct is either eliminated from the borrow chain or the Field should be exposed. However, achiving this complete modeling takes time and this half-backed solution might need to stay a bit longer. It is also possible that we do need this facility (of using Field but not exposing Field in the Prover). In any case, it merits a PR as a block.

Have you read the Contributing Guidelines on pull requests?

Yes

[awelc]

Stamping as it's a cherry.

Mmmm... Cherries... Thank you!