Verify proveX and checkX functions similarly to testX (#249)

* Add `prove`, `check` prefixes for functions to be verified; add a test * Set Version: 0.1.108 * Skip `prove_assert_true` in legacy CI job * Set Version: 0.1.110 * Add support for `proveFail`, `checkFail` prefixes * Rename `testFail_assert_false` to `check...`; update expected output * Set Version: 0.1.111 * Updated expected output after merge * Another exected output update after merge --------- Co-authored-by: devops <[email protected]>
runtimeverification · Jan 12, 2024 · a207bd4 · a207bd4
1 parent 26df055
commit a207bd4
Show file tree

Hide file tree

Showing 16 changed files with 145 additions and 130 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.110
+0.1.111
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.110"
+version = "0.1.111"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.110'
+VERSION: Final = '0.1.111'
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -419,8 +419,9 @@ def _method_to_cfg(
         new_node_ids = [init_node.id]
         init_node_id = init_node.id
 
-    is_test = method.signature.startswith('test')
-    failing = method.signature.startswith('testFail')
+    proof_prefixes = ['test', 'prove', 'check']
+    is_test = any(method.signature.startswith(prefix) for prefix in proof_prefixes)
+    failing = any(method.signature.startswith(prefix + 'Fail') for prefix in proof_prefixes)
     final_cterm = _final_cterm(
         empty_config, contract.name_with_path, failing=failing, is_test=is_test, use_init_code=use_init_code
     )

diff --git a/src/tests/integration/test-data/contracts.k.expected b/src/tests/integration/test-data/contracts.k.expected
diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all
@@ -38,8 +38,9 @@ ArithmeticTest.test_wmul_wdiv_inverse_underflow(uint256,uint256)
 ArithmeticTest.test_wmul_weakly_increasing_positive(uint256,uint256)
 AssertTest.test_assert_false()
 AssertTest.test_assert_true()
+AssertTest.prove_assert_true()
 AssertTest.test_assert_true_branch(uint256)
-AssertTest.testFail_assert_false()
+AssertTest.checkFail_assert_false()
 AssertTest.testFail_assert_true()
 AssertTest.testFail_expect_revert()
 AssertTest.test_failing_branch(uint256)

diff --git a/src/tests/integration/test-data/foundry-prove-skip-legacy b/src/tests/integration/test-data/foundry-prove-skip-legacy
@@ -31,6 +31,7 @@ ArithmeticTest.test_wmul_rounding(uint256,uint256)
 ArithmeticTest.test_wmul_wdiv_inverse(uint256,uint256)
 ArithmeticTest.test_wmul_wdiv_inverse_underflow(uint256,uint256)
 ArithmeticTest.test_wmul_weakly_increasing_positive(uint256,uint256)
+AssertTest.prove_assert_true()
 AssertTest.test_assert_false()
 AssertTest.testFail_assert_true()
 AssertTest.testFail_expect_revert()

diff --git a/src/tests/integration/test-data/foundry-show b/src/tests/integration/test-data/foundry-show
@@ -1,6 +1,6 @@
 AssertTest.test_assert_false()
 AssertTest.test_assert_true()
-AssertTest.testFail_assert_false()
+AssertTest.checkFail_assert_false()
 AssertTest.testFail_assert_true()
 AssertTest.testFail_expect_revert()
 AssertTest.test_failing_branch(uint256)

diff --git a/src/tests/integration/test-data/foundry/test/Simple.t.sol b/src/tests/integration/test-data/foundry/test/Simple.t.sol
@@ -21,6 +21,10 @@ contract AssertTest is Test, KEVMCheats {
         assert(true);
     }
 
+    function prove_assert_true() public pure {
+        assert(true);
+    }
+
     function test_assert_true_branch(uint x) public {
         if (x < 3) {
             y = x;
@@ -40,7 +44,7 @@ contract AssertTest is Test, KEVMCheats {
         assert(true);
     }
 
-    function testFail_assert_false() public pure {
+    function checkFail_assert_false() public pure {
          assert(false);
      }
 

diff --git a/...sertTest.testFail_assert_false().expected → ...ertTest.checkFail_assert_false().expected b/...sertTest.testFail_assert_false().expected → ...ertTest.checkFail_assert_false().expected
@@ -8,21 +8,21 @@
 │  (179 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
-│   pc: 317
+│   pc: 328
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
 ├─ 4
 │   k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
-│   pc: 317
+│   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
 ├─ 5 (terminal)
 │   k: #halt ~> CONTINUATION:K
-│   pc: 317
+│   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
@@ -33,24 +33,24 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (244 steps)
+│  (307 steps)
 ├─ 8
 │   k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
-│   pc: 2984
+│   pc: 2995
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
 ├─ 9
 │   k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
-│   pc: 2984
+│   pc: 2995
 │   callDepth: 0
 │   statusCode: EVMC_REVERT
 │
 │  (2 steps)
 ├─ 10 (terminal)
 │   k: #halt ~> CONTINUATION:K
-│   pc: 2984
+│   pc: 2995
 │   callDepth: 0
 │   statusCode: EVMC_REVERT
 │
@@ -751,7 +751,7 @@
                      CALLER_ID:Int
                    </caller>
                    <callData>
-                     ( b"\n\x92T\xe4" => b"z\xa9\xcc\xae" )
+                     ( b"\n\x92T\xe4" => b"\xa2]\xdf\xf4" )
                    </callData>
                    <callValue>
                      0
@@ -961,13 +961,13 @@
                      728815563385977040452943777879061427756277306518
                    </id>
                    <callData>
-                     b"z\xa9\xcc\xae"
+                     b"\xa2]\xdf\xf4"
                    </callData>
                    <callValue>
                      0
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( 603 : ( 316 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) ) )
+                     ( .WordStack => ( 614 : ( 327 : ( selector ( "checkFail_assert_false()" ) : .WordStack ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
@@ -1159,13 +1159,13 @@
                      728815563385977040452943777879061427756277306518
                    </id>
                    <callData>
-                     b"z\xa9\xcc\xae"
+                     b"\xa2]\xdf\xf4"
                    </callData>
                    <callValue>
                      0
                    </callValue>
                    <wordStack>
-                     ( 603 : ( 316 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) )
+                     ( 614 : ( 327 : ( selector ( "checkFail_assert_false()" ) : .WordStack ) ) )
                    </wordStack>
                    <localMem>
                      b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80"
@@ -1357,13 +1357,13 @@
                      728815563385977040452943777879061427756277306518
                    </id>
                    <callData>
-                     b"z\xa9\xcc\xae"
+                     b"\xa2]\xdf\xf4"
                    </callData>
                    <callValue>
                      0
                    </callValue>
                    <wordStack>
-                     ( 603 : ( 316 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) )
+                     ( 614 : ( 327 : ( selector ( "checkFail_assert_false()" ) : .WordStack ) ) )
                    </wordStack>
                    <localMem>
                      b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80"

diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected
@@ -8,21 +8,21 @@
 │  (179 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
-│   pc: 317
+│   pc: 328
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
 ├─ 4
 │   k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
-│   pc: 317
+│   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
 ├─ 5 (terminal)
 │   k: #halt ~> CONTINUATION:K
-│   pc: 317
+│   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
@@ -36,21 +36,21 @@
 │  (200 steps)
 ├─ 8
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
-│   pc: 317
+│   pc: 328
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
 ├─ 9
 │   k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
-│   pc: 317
+│   pc: 328
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
 └─ 10 (leaf, terminal)
     k: #halt ~> CONTINUATION:K
-    pc: 317
+    pc: 328
     callDepth: 0
     statusCode: EVMC_SUCCESS