Add evm_success predicate for non-test tests

runtimeverification · Dec 15, 2023 · 2d1b80f · 2d1b80f
1 parent aabd2d4
commit 2d1b80f
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 10 deletions.
diff --git a/src/kontrol/kdist/foundry.md b/src/kontrol/kdist/foundry.md
@@ -84,5 +84,14 @@ module FOUNDRY-SUCCESS
     rule foundry_success(EVMC_SUCCESS, 0, false, false, false, false) => true
     rule foundry_success(_, _, _, _, _, _)                            => false [owise]
 
+    syntax Bool ::=
+      "evm_success" "("
+        statusCode: StatusCode
+        // TODO: do we need to consider `opcodeExpected`, `recordEventExpected`, etc?
+      ")" [function, klabel(evm_success), symbol]
+ // -------------------------------------------------
+    rule evm_success(EVMC_SUCCESS) => true
+    rule evm_success(_)            => false [owise]
+
 endmodule
 ```
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -499,22 +499,25 @@ def _final_cterm(
     empty_config: KInner, contract_name: str, *, failing: bool, is_test: bool = True, use_init_code: bool = False
 ) -> CTerm:
     final_term = _final_term(empty_config, contract_name, use_init_code=use_init_code)
-    dst_failed_post = KEVM.lookup(KVariable('CHEATCODE_STORAGE_FINAL'), Foundry.loc_FOUNDRY_FAILED())
-    foundry_success = Foundry.success(
-        KVariable('STATUSCODE_FINAL'),
-        dst_failed_post,
-        KVariable('ISREVERTEXPECTED_FINAL'),
-        KVariable('ISOPCODEEXPECTED_FINAL'),
-        KVariable('RECORDEVENT_FINAL'),
-        KVariable('ISEVENTEXPECTED_FINAL'),
-    )
     final_cterm = CTerm.from_kast(final_term)
     if is_test:
+        dst_failed_post = KEVM.lookup(KVariable('CHEATCODE_STORAGE_FINAL'), Foundry.loc_FOUNDRY_FAILED())
+        foundry_success = Foundry.success(
+            KVariable('STATUSCODE_FINAL'),
+            dst_failed_post,
+            KVariable('ISREVERTEXPECTED_FINAL'),
+            KVariable('ISOPCODEEXPECTED_FINAL'),
+            KVariable('RECORDEVENT_FINAL'),
+            KVariable('ISEVENTEXPECTED_FINAL'),
+        )
+
         if not failing:
             return final_cterm.add_constraint(mlEqualsTrue(foundry_success))
         else:
             return final_cterm.add_constraint(mlEqualsTrue(notBool(foundry_success)))
-    return final_cterm
+
+    evm_success = KApply('evm_success', [KVariable('STATUSCODE_FINAL')])
+    return final_cterm.add_constraint(mlEqualsTrue(notBool(evm_success)))
 
 
 def _final_term(empty_config: KInner, contract_name: str, use_init_code: bool = False) -> KInner: