Move prover returns: exiting with verification errors
error: post-condition does not hold
   ┌─ tests/sources/functional/hash_model_invalid.move:22:9
   │
22 │         ensures len(result_1) > 0 ==> result_1[0] < max_u8(); // should be <=
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/hash_model_invalid.move:11: hash_test1
   =         v1 = <redacted>
   =         v2 = <redacted>
   =     at tests/sources/functional/hash_model_invalid.move:13: hash_test1
   =         h1 = <redacted>
   =     at tests/sources/functional/hash_model_invalid.move:14: hash_test1
   =         h2 = <redacted>
   =     at tests/sources/functional/hash_model_invalid.move:15: hash_test1
   =         result_1 = <redacted>
   =         result_2 = <redacted>
   =     at tests/sources/functional/hash_model_invalid.move:16: hash_test1
   =     at tests/sources/functional/hash_model_invalid.move:18: hash_test1 (spec)
   =     at tests/sources/functional/hash_model_invalid.move:22: hash_test1 (spec)

error: post-condition does not hold
   ┌─ tests/sources/functional/hash_model_invalid.move:35:9
   │
35 │         ensures len(result_1) > 0 ==> result_1[0] < max_u8();
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/hash_model_invalid.move:26: hash_test2
   =         v1 = <redacted>
   =         v2 = <redacted>
   =     at tests/sources/functional/hash_model_invalid.move:28: hash_test2
   =         h1 = <redacted>
   =     at tests/sources/functional/hash_model_invalid.move:29: hash_test2
   =         h2 = <redacted>
   =     at tests/sources/functional/hash_model_invalid.move:30: hash_test2
   =         result_1 = <redacted>
   =         result_2 = <redacted>
   =     at tests/sources/functional/hash_model_invalid.move:31: hash_test2
   =     at tests/sources/functional/hash_model_invalid.move:33: hash_test2 (spec)
   =     at tests/sources/functional/hash_model_invalid.move:35: hash_test2 (spec)