search

aptos-labs / aptos-core

Aptos is a layer 1 blockchain built to support the widespread use of blockchain through better technology and user experience.
https://aptosfoundation.org
Other
6.18k stars 3.64k forks source link

[Bug] [Move Prover] CFG simplification breaks up the prover #15044

Open fEst1ck opened 1 week ago

fEst1ck commented 1 week ago

🐛 Bug

Running

MOVE_COMPILER_V2=1 cargo test --package aptos-framework --test move_prover_tests -- move_aptos_stdlib_prover_tests --exact --show-output

gives

running 1 test
error: post-condition does not hold
   ┌─ /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.spec.move:40:9
   │
40 │ ╭         ensures (result.inner == EQUAL) ==> (
41 │ │             (left_length == right_length) &&
42 │ │                 (forall i: u64 where i < left_length: left[i] == right[i])
43 │ │         );
   │ ╰──────────^
   │
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:38: compare_u8_vector
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.spec.move:37
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.spec.move:38
   =         left = vector{190u8, 34u8}
   =         right = vector{190u8, 33u8}
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:39: compare_u8_vector
   =         left_length = 2
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:40: compare_u8_vector
   =         right_length = 2
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:42: compare_u8_vector
   =         idx = 0
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:44: compare_u8_vector
   =         $t9 = true
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:44: compare_u8_vector
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:45: compare_u8_vector
   =         left_byte = 190u8
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:46: compare_u8_vector
   =         right_byte = 190u8
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:48: compare_u8_vector
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:50: compare_u8_vector
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:53: compare_u8_vector
   =         idx = 1
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:44: compare_u8_vector
   =         $t9 = true
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:61: compare_u8_vector
   =         $t9 = false
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:44: compare_u8_vector
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:56: compare_u8_vector
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:58: compare_u8_vector
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:59: compare_u8_vector
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.spec.move:3
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:61: compare_u8_vector
   =         return = comparator.Result{inner = 0u8}
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.move:57: compare_u8_vector
   =         result = comparator.Result{inner = 0u8}
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.spec.move:35
   =     at /Users/zw/aptos-core/aptos-move/framework/aptos-stdlib/sources/comparator.spec.move:40

test move_aptos_stdlib_prover_tests ... FAILED

even though the compiled bytecode is still correct for compare_u8_vector.

Expected Behavior

The test should pass.

rahxephon89 commented 1 week ago

The issue happens when there is a while loop which is unrolled for bounded verification.