[move-prover] algorithm for progressive instantiation

[meng-xu-cs]

This algorithm deals with finding a complete set of instantiation
combinations for all type parameters when unifying two types.

// problem definition

The algorithm is encapsulated in struct TypeInstantiationDerivation
and is not conceptually hard to understand:

Suppose we aim to unify T1 [X0, X1, ..., Xm] vs T2 [Y0, Y1, ..., Yn],
where T1 and T2 are types while Xs and Ys are type parameters
that show up in T1 and T2, respectively.

We want to find all instantiations to <X0, X1, ..., Xm> such that
for each instantiation (x0, x1, ..., xm), there exists a valid
instantiation (y0, y1, ..., yn) which makes T1 and T2 equivelant,
i.e., T1<x0, x1, ..., xm> == T2<y0, y1, ..., yn>.

We put all these instantiation in a set denoted as |(x0, x1, ..., xm)|
and this algorithm is about finding this set of instantiations.

// algorithm description

The algorithm works by finding all instantiations for X0 first, and
then progress to X1, X2, ..., until finishing Xn.

• unify T1 [X0, X1, ..., Xm] vs T2 [Y0, Y1, ..., Yn], get all
  possible substitutions for X0, denoted as |x0|
• for each x0 in |x0|:
  • refine T1 with x0
  • unify T1 [X0 := x0, X1, ..., Xm] vs T2 [Y0, Y1, ..., Yn], get
    all possible substitutions for X1, denoted as |x1|
  • for each x1 in |x1|:
    • refine T1 with x1
    • unify T1 [X0 := x0, X1 := x1, ..., Xm] vs T2 [Y0, Y1, ..., Yn],
      get all possible substitutions for X2, denoted as |x2|
    • for each x2 in |x2|:
      • ......

The process continues until we reach the end of Xn. After which, the
algorithm should have collected all the legal instantiation combinations
for type parameters <X0, X1, ..., Xm>.

// other notes

• The implementation has a bit of fine-tuning rooted by the fact that
  sometimes we want to treat a type parameter as a variable (i.e.,
  participate in type unification) while in other cases, we want to
  treat a type parameter as a concrete type (i.e., do not participate in
  type unification).

• We also have a fine-tuning on whether we treat a type parameter that
  does not have any valid instantiations as an error or remains as a
  concrete type parameter. This is rooted by the differentation of type
  parameters in function vs type parameters in a global invariant.
  Essentially, all type parameters in a global invariant must be
  instantiated in order for the invariant to be instrumented. But not
  all function type paramters need to be instantiated.

• This is not the most efficient algorithm, especially when we have a
  large number of type parameters. But a vast majority of Move code we
  have seen so far have at most one type parameter, so in this commit,
  we trade-off efficiency with simplicity.

Motivation

Work item needed for global invariant instrumentation

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

• CI

[wrwg]

Why do we need progressive instantiation? As far as I can tell from the paper, a concept like this is not needed, is there something wrong in the paper?

[meng-xu-cs]

The need for finding all instantiations of <T0, T1, ..., Tn> is given in the paper, in the monomorphization section to be specific.

Foreach memory |M in modify(f)|, if there is a memory
|M' in modify(f)+read(f)| such that |M| and |M'| can unify via |T1,..,Tn|,
collect an instantiation of the type parameters |Ti| from the resulting
substitution. This instantiation may not assign values to all type parameters,
and those unassigned parameters stay as is. For instance, |f<T1, T2>| might
have a partial instantiation |f<T1, u8>|.

This paragraph does not specify how to collect each concrete instantiation of <T1, T2, ..., Tn> that unifies. It assumes that there is such an algorithm and the algorithm is trivial (which is correct).

Previously we have been using the cartesian product as a proxy. For example, if we have a function
f<T1, T2> that modifies M<bool, bool> and M<u64, u64> respectively,
the cartesian product approach will give us T1: {bool, u64} * T2: {bool, u64}, which include infeasible combinations such as M<bool, u64> and M<u64, bool>, which f never touches.

This progressive instantiation algorithm is to solve this issue while also ensuring that we find a complete set for all possible instantiations of <T1, T2, ..., Tn>. I am not claiming that this is the only way or the best way, this is just one algorithm that I feel OK about and the implementation is not that complicated.

[meng-xu-cs]

/land

[github-actions]

Cluster Test Result

Test runner setup time spent 259 secs
Compatibility test results for land_753dcfc9 ==> land_2a96d320 (PR)
1. All instances running land_753dcfc9, generating some traffic on network
2. First full node land_753dcfc9 ==> land_2a96d320, to validate new full node to old validator node traffic
3. First Validator node land_753dcfc9 ==> land_2a96d320, to validate storage compatibility
4. First batch validators (14) land_753dcfc9 ==> land_2a96d320, to test consensus and traffic between old full nodes and new validator node
5. First batch full nodes (14) land_753dcfc9 ==> land_2a96d320
6. Second batch validators (15) land_753dcfc9 ==> land_2a96d320, to upgrade rest of the validators
7. Second batch of full nodes (15) land_753dcfc9 ==> land_2a96d320, to finish the network upgrade, time spent 692 secs
all up : 1253 TPS, 3617 ms latency, 4200 ms p99 latency, no expired txns, time spent 249 secs
Logs: http://kibana.ct-1-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2021-09-01T15:29:31Z',to:'2021-09-01T15:52:29Z'))
Dashboard: http://grafana.ct-1-k8s-testnet.aws.hlw3truzy4ls.com/d/performance/performance?from=1630510171000&to=1630511549000
Validator 1 logs: http://kibana.ct-1-k8s-testnet.aws.hlw3truzy4ls.com/app/kibana#/discover?_g=(time:(from:'2021-09-01T15:29:31Z',to:'2021-09-01T15:52:29Z'))&_a=(columns:!(log),query:(language:kuery,query:'kubernetes.pod_name:"val-1"'),sort:!(!('@timestamp',desc)))

Repro cmd:

./scripts/cti --tag land_753dcfc9 --cluster-test-tag land_2a96d320 -E BATCH_SIZE=15 -E UPDATE_TO_TAG=land_2a96d320 --report report.json --suite land_blocking_compat

🎉 Land-blocking cluster test passed! 👌