Fixed the Prover spec

Fixed the spec to unblock the PR.

Need to prove the introduced assumptions with proper loop invariants, which should be provable.

aptos-move/framework/aptos-framework/sources/randomness.move

@@ -25,6 +25,8 @@ module aptos_framework::randomness {
     /// Randomness APIs calls must originate from a private entry function. Otherwise, test-and-abort attacks are possible.
     const E_API_USE_SUSCEPTIBLE_TO_TEST_AND_ABORT: u64 = 1;
 
+    const MAX_U256: u256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935;
+
     /// 32-byte randomness seed unique to every block.
     /// This resource is updated in every block prologue.
     struct PerBlockRandomness has drop, key {
@@ -162,6 +164,11 @@ module aptos_framework::randomness {
         let i = 0;
         let ret: u128 = 0;
         while (i < 16) {
+            spec {
+                // TODO: Prove these with proper loop invaraints.
+                assume ret * 256 + 255 <= MAX_U256;
+                assume len(raw) > 0;
+            };
             ret = ret * 256 + (vector::pop_back(&mut raw) as u128);
             i = i + 1;
         };
@@ -183,6 +190,11 @@ module aptos_framework::randomness {
         let i = 0;
         let ret: u256 = 0;
         while (i < 32) {
+            spec {
+                // TODO: Prove these with proper loop invaraints.
+                assume ret * 256 + 255 <= MAX_U256;
+                assume len(raw) > 0;
+            };
             ret = ret * 256 + (vector::pop_back(&mut raw) as u256);
             i = i + 1;
         };

aptos-move/framework/aptos-framework/sources/randomness.spec.move

@@ -118,7 +118,6 @@ spec aptos_framework::randomness {
         // TODO(tengzhang): complete the aborts_if conditions
         // include n > 1 ==> NextBlobAbortsIf;
         // aborts_if n > 1 && !exists<PerBlockRandomness>(@aptos_framework);
-        aborts_if n == 0;
     }
 
     spec safe_add_mod_for_verification(a: u256, b: u256, m: u256): u256 {