[Prover] broken spec of fixed_point32

[junkil-park]

The spec of fixed_point32 in aptos-core/aptos-move/framework/move-stdlib is broken. Perhaps, it's due to the recent update on the semantics of shift operators.

How to reproduce

Go to aptos-core/aptos-move/framework/move-stdlib, and run move prove. Prover will produce the following error:

$ move prove
[INFO] preparing module 0x1::bcs
[INFO] preparing module 0x1::fixed_point32
[INFO] preparing module 0x1::hash
[INFO] preparing module 0x1::vector
[INFO] preparing module 0x1::error
[INFO] preparing module 0x1::acl
[INFO] preparing module 0x1::bit_vector
[INFO] preparing module 0x1::signer
[INFO] preparing module 0x1::features
[INFO] preparing module 0x1::option
[INFO] preparing module 0x1::string
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 60 verification conditions
[INFO] running solver
[INFO] 0.026s build, 0.012s trafo, 0.005s gen, 3.882s verify, total 3.925s
error: function does not abort under this condition
    ┌─ ./sources/fixed_point32.move:127:9
    │
127 │         aborts_if scaled_denominator == 0 with EDENOMINATOR;
    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    │
    =     at ./sources/fixed_point32.move:101: create_from_rational
    =     at ./sources/fixed_point32.move:124
    =     at ./sources/fixed_point32.move:125
    =     at ./sources/fixed_point32.move:126
    =     at ./sources/fixed_point32.move:101: create_from_rational
    =         numerator = 15
    =         denominator = 8589934592
    =     at ./sources/fixed_point32.move:106: create_from_rational
    =         scaled_numerator = 276701161105643274240u128
    =     at ./sources/fixed_point32.move:107: create_from_rational
    =         scaled_denominator = 36893488147419103232u128
    =     at ./sources/fixed_point32.move:108: create_from_rational
    =     at ./sources/fixed_point32.move:109: create_from_rational
    =         quotient = 7u128
    =     at ./sources/fixed_point32.move:110: create_from_rational
    =     at ./sources/fixed_point32.move:113: create_from_rational
    =     at ./sources/fixed_point32.move:114: create_from_rational
    =         result = fixed_point32.FixedPoint32{value = 7}
    =     at ./sources/fixed_point32.move:115: create_from_rational
    =     at ./sources/fixed_point32.move:127

error: abort not covered by any of the `aborts_if` clauses
    ┌─ ./sources/fixed_point32.move:116:5
    │
113 │           assert!(quotient <= MAX_U64, ERATIO_OUT_OF_RANGE);
    │           ------------------------------------------------- abort happened here with code 0x20005
    ·
116 │ ╭     spec create_from_rational {
117 │ │         pragma opaque;
118 │ │         include CreateFromRationalAbortsIf;
119 │ │         ensures result == spec_create_from_rational(numerator, denominator);
120 │ │     }
    │ ╰─────^
    │
    =     at ./sources/fixed_point32.move:101: create_from_rational
    =     at ./sources/fixed_point32.move:124
    =     at ./sources/fixed_point32.move:125
    =     at ./sources/fixed_point32.move:126
    =     at ./sources/fixed_point32.move:101: create_from_rational
    =         numerator = 4294967296
    =         denominator = 1
    =     at ./sources/fixed_point32.move:106: create_from_rational
    =         scaled_numerator = 79228162514264337593543950336u128
    =     at ./sources/fixed_point32.move:107: create_from_rational
    =         scaled_denominator = 4294967296u128
    =     at ./sources/fixed_point32.move:108: create_from_rational
    =     at ./sources/fixed_point32.move:109: create_from_rational
    =         quotient = 18446744073709551616u128
    =     at ./sources/fixed_point32.move:110: create_from_rational
    =     at ./sources/fixed_point32.move:113: create_from_rational
    =         ABORTED

error: abort code not covered by any of the `aborts_if` or `aborts_with` clauses
    ┌─ ./sources/fixed_point32.move:116:5
    │
110 │           assert!(quotient != 0 || numerator == 0, ERATIO_OUT_OF_RANGE);
    │           ------------------------------------------------------------- abort happened here with code 0x20005
    ·
116 │ ╭     spec create_from_rational {
117 │ │         pragma opaque;
118 │ │         include CreateFromRationalAbortsIf;
119 │ │         ensures result == spec_create_from_rational(numerator, denominator);
120 │ │     }
    │ ╰─────^
    │
    =     at ./sources/fixed_point32.move:101: create_from_rational
    =     at ./sources/fixed_point32.move:124
    =     at ./sources/fixed_point32.move:125
    =     at ./sources/fixed_point32.move:126
    =     at ./sources/fixed_point32.move:101: create_from_rational
    =         numerator = 2
    =         denominator = 12884901888
    =     at ./sources/fixed_point32.move:106: create_from_rational
    =         scaled_numerator = 36893488147419103232u128
    =     at ./sources/fixed_point32.move:107: create_from_rational
    =         scaled_denominator = 55340232221128654848u128
    =     at ./sources/fixed_point32.move:108: create_from_rational
    =     at ./sources/fixed_point32.move:109: create_from_rational
    =         quotient = 0u128
    =     at ./sources/fixed_point32.move:110: create_from_rational
    =         ABORTED

Error: exiting with verification errors

Expected result

Prover produces no error.

[rahxephon89]

I changed the spec of fixed_point32 in the move repo due to change of semantics in shift operator: https://github.com/move-language/move/blob/main/language/move-stdlib/sources/fixed_point32.move

[junkil-park]

This issue has been resolved.