Move prover returns: exiting with verification errors
error: post-condition does not hold
   ┌─ tests/sources/functional/hash_model.move:48:9
   │
48 │         ensures len(result_1) > 0 ==> result_1[0] < max_u8(); // should be <=
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/hash_model.move:39: hash_test1_incorrect
   =         v1 = <redacted>
   =         v2 = <redacted>
   =     at tests/sources/functional/hash_model.move:41: hash_test1_incorrect
   =         h1 = <redacted>
   =     at tests/sources/functional/hash_model.move:42: hash_test1_incorrect
   =         h2 = <redacted>
   =     at tests/sources/functional/hash_model.move:43: hash_test1_incorrect
   =         result_1 = <redacted>
   =         result_2 = <redacted>
   =     at tests/sources/functional/hash_model.move:44: hash_test1_incorrect
   =     at tests/sources/functional/hash_model.move:46: hash_test1_incorrect (spec)
   =     at tests/sources/functional/hash_model.move:48: hash_test1_incorrect (spec)

error: post-condition does not hold
   ┌─ tests/sources/functional/hash_model.move:91:9
   │
91 │         ensures len(result_1) > 0 ==> result_1[0] < max_u8();
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/hash_model.move:82: hash_test2_incorrect
   =         v1 = <redacted>
   =         v2 = <redacted>
   =     at tests/sources/functional/hash_model.move:84: hash_test2_incorrect
   =         h1 = <redacted>
   =     at tests/sources/functional/hash_model.move:85: hash_test2_incorrect
   =         h2 = <redacted>
   =     at tests/sources/functional/hash_model.move:86: hash_test2_incorrect
   =         result_1 = <redacted>
   =         result_2 = <redacted>
   =     at tests/sources/functional/hash_model.move:87: hash_test2_incorrect
   =     at tests/sources/functional/hash_model.move:89: hash_test2_incorrect (spec)
   =     at tests/sources/functional/hash_model.move:91: hash_test2_incorrect (spec)