deprecate execution of testFail* tests

src/kontrol/foundry.py

@@ -738,19 +738,11 @@ def symbolic_account(prefix: str, program: KInner, storage: KInner | None = None
     def help_info(proof_id: str, hevm: bool) -> list[str]:
         res_lines: list[str] = []
         if hevm:
-            _, test = proof_id.split('.')
-            if not any(test.startswith(prefix) for prefix in ['testFail', 'checkFail', 'proveFail']):
-                res_lines.append('')
-                res_lines.append('See `hevm_success` predicate for more information:')
-                res_lines.append(
-                    'https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/hevm.md#hevm-success-predicate'
-                )
-            else:
-                res_lines.append('')
-                res_lines.append('See `hevm_fail` predicate for more information:')
-                res_lines.append(
-                    'https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/hevm.md#hevm-fail-predicate'
-                )
+            res_lines.append('')
+            res_lines.append('See `hevm_success` predicate for more information:')
+            res_lines.append(
+                'https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/hevm.md#hevm-success-predicate'
+            )
         else:
             res_lines.append('')
             res_lines.append('See `foundry_success` predicate for more information:')
@@ -935,8 +927,7 @@ def remove_old_proofs(self, force_remove: bool = False) -> bool:
         if force_remove or any(
             # We need to check only the methods that get written to the digest file
             # Otherwise we'd get vacuous positives
-            (method.is_test or method.is_testfail or method.is_setup)
-            and not method.contract_up_to_date(Path(self.digest_file))
+            (method.is_test or method.is_setup) and not method.contract_up_to_date(Path(self.digest_file))
             for contract in self.contracts.values()
             for method in contract.methods
         ):

src/kontrol/prove.py

@@ -19,7 +19,7 @@
 from pyk.kast.prelude.bytes import bytesToken
 from pyk.kast.prelude.collections import list_empty, map_empty, map_item, set_empty
 from pyk.kast.prelude.k import GENERATED_TOP_CELL
-from pyk.kast.prelude.kbool import FALSE, TRUE, boolToken, notBool
+from pyk.kast.prelude.kbool import FALSE, TRUE, boolToken
 from pyk.kast.prelude.kint import eqInt, intToken, leInt, ltInt
 from pyk.kast.prelude.ml import mlEqualsFalse, mlEqualsTrue
 from pyk.kast.prelude.utils import token
@@ -215,6 +215,11 @@ def collect_tests(
     res: list[FoundryTest] = []
     for sig, ver in tests:
         contract, method = foundry.get_contract_and_method(sig)
+        if method.is_testfail:
+            console.print(
+                f":cross_mark: [bold red]testFail has been removed. Consider changing to test_Revert[If|When]_Condition and expecting a revert[/bold red] :cross_mark: {sig.split('%')[-1]}"
+            )
+            continue
         version = foundry.resolve_proof_version(sig, reinit, ver)
         res.append(FoundryTest(contract, method, version))
     return res
@@ -790,7 +795,6 @@ def _method_to_cfg(
     final_cterm = _final_cterm(
         empty_config,
         program=bytesToken(contract_code),
-        failing=method.is_testfail,
         config_type=config_type,
         is_test=method.is_test,
         is_setup=method.is_setup,
@@ -808,7 +812,7 @@ def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, config_type: ConfigTy
             'ACCOUNTS_CELL',
             'NUMBER_CELL',
             'TIMESTAMP_CELL',
-            'BASEFEE_CELL',
+            'BASEFEE_CEL',
             'CHAINID_CELL',
             'COINBASE_CELL',
             'PREVCALLER_CELL',
@@ -1271,7 +1275,6 @@ def _final_cterm(
     config_type: ConfigType,
     additional_accounts: list[KInner],
     *,
-    failing: bool,
     is_test: bool = True,
     is_setup: bool = False,
     hevm: bool = False,
@@ -1289,22 +1292,13 @@ def _final_cterm(
                 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.add_constraint(mlEqualsTrue(foundry_success))
         else:
-            if not failing:
-                return final_cterm.add_constraint(
-                    mlEqualsTrue(
-                        Foundry.hevm_success(KVariable('STATUSCODE_FINAL'), dst_failed_post, KVariable('OUTPUT_FINAL'))
-                    )
-                )
-            else:
-                # To do: Print warning to the user
-                return final_cterm.add_constraint(
-                    mlEqualsTrue(Foundry.hevm_fail(KVariable('STATUSCODE_FINAL'), dst_failed_post))
+            return final_cterm.add_constraint(
+                mlEqualsTrue(
+                    Foundry.hevm_success(KVariable('STATUSCODE_FINAL'), dst_failed_post, KVariable('OUTPUT_FINAL'))
                 )
+            )
 
     return final_cterm
 

src/tests/integration/test-data/end-to-end-prove-all

@@ -1,5 +1,4 @@
 AllowChangesTest.testAllowCalls(uint256)
-AllowChangesTest.testFailAllowCalls_ifNotWhitelisted(uint256)
 CounterTest.test_Increment()
 ForgetBranchTest.test_forgetBranch(uint256)
 RandomVarTest.test_custom_names()

src/tests/integration/test-data/foundry-fail

@@ -1,8 +1,5 @@
 AssertTest.test_assert_false()
-AssertTest.testFail_assert_true()
-AssertTest.testFail_expect_revert()
 AssertTest.test_failing_branch(uint256)
 AssertTest.test_revert_branch(uint256,uint256)
 AssumeTest.test_assume_false(uint256,uint256)
-AssumeTest.testFail_assume_false(uint256,uint256)
 ImmutableVarsTest.test_run_deployment(uint256)

src/tests/integration/test-data/foundry-init-code

@@ -1,7 +1,5 @@
 InitCodeTest.test_init()
-InitCodeTest.testFail_init()
 ConstructorArgsTest.test_constructor_args()
 ConstructorTest.test_constructor()
-ConstructorTest.testFail_constructor()
 ConstructorTest.run_constructor()
 ExternalNestedLibraryTest.testExtLibs()

src/tests/integration/test-data/foundry-minimize

@@ -1,5 +1,4 @@
 AssertTest.test_assert_false()
-AssertTest.testFail_expect_revert()
 AssertTest.test_failing_branch(uint256)
 AssertTest.test_revert_branch(uint256,uint256)
 MergeKCFGTest.test_branch_merge(uint256,uint256,bool)

src/tests/integration/test-data/foundry-prove-all

@@ -2,8 +2,6 @@ AccountParamsTest.testDealConcrete()
 AccountParamsTest.testDealSymbolic(uint256)
 AccountParamsTest.testEtchConcrete()
 AccountParamsTest.testEtchSymbolic(bytes)
-AccountParamsTest.testFail_GetNonce_false()
-AccountParamsTest.testFail_GetNonce_true()
 AccountParamsTest.test_GetNonce_false()
 AccountParamsTest.test_GetNonce_true()
 AccountParamsTest.test_getNonce_unknownSymbolic(address)
@@ -14,16 +12,12 @@ AddrTest.test_addr_false()
 AddrTest.test_addr_symbolic(uint256)
 AddrTest.test_addr_true()
 AddrTest.test_builtInAddresses()
-AddrTest.testFail_addr_false()
-AddrTest.testFail_addr_true()
 AddrTest.test_notBuiltinAddress_concrete()
 AddrTest.test_notBuiltinAddress_symbolic(address)
 AllowChangesTest.test()
 AllowChangesTest.testAllow()
 AllowChangesTest.testAllowSymbolic()
 AllowChangesTest.testAllow_fail()
-AllowChangesTest.testFailAllowCallsToAddress()
-AllowChangesTest.testFailAllowChangesToStorage()
 ArithmeticCallTest.test_double_add(uint256,uint256)
 ArithmeticCallTest.test_double_add_double_sub(uint256,uint256)
 ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256)
@@ -45,16 +39,11 @@ AssertTest.test_assert_false()
 AssertTest.test_assert_true()
 AssertTest.prove_assert_true()
 AssertTest.test_assert_true_branch(uint256)
-AssertTest.checkFail_assert_false()
-AssertTest.testFail_assert_true()
-AssertTest.testFail_expect_revert()
 AssertTest.test_failing_branch(uint256)
 AssertTest.test_revert_branch(uint256,uint256)
 AssumeTest.test_assume_false(uint256,uint256)
 AssumeTest.test_assume_staticCall(bool)
 AssumeTest.test_assume_true(uint256,uint256)
-AssumeTest.testFail_assume_false(uint256,uint256)
-AssumeTest.testFail_assume_true(uint256,uint256)
 AssumeTest.test_multi_assume(address,address)
 BlockParamsTest.testBlockNumber()
 BlockParamsTest.testChainId(uint256)
@@ -67,13 +56,10 @@ BytesTypeTest.test_bytes32(bytes32)
 BytesTypeTest.test_bytes32_fail(bytes32)
 BytesTypeTest.test_bytes4(bytes4)
 BytesTypeTest.test_bytes4_fail(bytes4)
-BytesTypeTest.testFail_bytes32(bytes32)
-BytesTypeTest.testFail_bytes4(bytes4)
 ChainIdTest.test_chainid_setup()
 CoinBaseTest.test_coinbase_setup()
 ConstructorTest.run_constructor()
 ContractBTest.testCannotSubtract43()
-ContractBTest.testFailSubtract43()
 ContractBTest.testNumberIs42()
 ContractTest.testExample()
 CopyStorageTest.testCopyStorage()
@@ -109,19 +95,13 @@ ExpectRevertTest.test_expectRevert_internalCall()
 ExpectRevertTest.test_expectRevert_message()
 ExpectRevertTest.test_expectRevert_returnValue()
 ExpectRevertTest.test_expectRevert_true()
-ExpectRevertTest.testFail_expectRevert_bytes4()
-ExpectRevertTest.testFail_expectRevert_empty()
-ExpectRevertTest.testFail_ExpectRevert_failAndSuccess()
-ExpectRevertTest.testFail_expectRevert_false()
-ExpectRevertTest.testFail_expectRevert_multipleReverts()
 ExternalLibTest.testSquare(uint256)
 ExternalLibTest.testSum()
 FeeTest.test_fee_setup()
 FfiTest.testffi()
 FfiTest.testFFIFOO()
 FfiTest.testFFIScript()
 FfiTest.testFFIScript2()
-FilesTest.testFailRemoveFile()
 FilesTest.testReadWriteFile()
 FilesTest.testReadWriteLine()
 ForkTest.testActiveFork()
@@ -136,7 +116,6 @@ ForkTest.testRPCUrl()
 ForkTest.testRPCUrlRevert()
 FreshCheatcodes.test_bool()
 FreshCheatcodes.test_int128()
-FreshCheatcodes.testFail_int128()
 FreshCheatcodes.test_address()
 FreshCheatcodes.test_freshUints(uint8)
 FreshCheatcodes.test_freshSymbolicWord()
@@ -190,11 +169,8 @@ MockFunctionTest.test_mock_function()
 MockFunctionTest.test_mock_function_all_args()
 MockFunctionTest.test_mock_function_concrete_args()
 NestedStructsTest.prove_fourfold_nested_struct(((((uint8,uint256),bytes32)[],bytes32)))
-OwnerUpOnlyTest.testFailIncrementAsNotOwner()
 OwnerUpOnlyTest.testIncrementAsNotOwner()
 OwnerUpOnlyTest.testIncrementAsOwner()
-PlainPrankTest.testFail_startPrank_existingAlready()
-PlainPrankTest.testFail_startPrank_internalCall()
 PlainPrankTest.test_prank_zeroAddress_true()
 PlainPrankTest.test_startPrank_true()
 PlainPrankTest.test_startPrankWithOrigin_true()
@@ -204,7 +180,6 @@ PlainPrankTest.test_prank_expectRevert()
 PortalTest.test_withdrawal_paused((uint256,address,address,uint256,uint256,bytes),uint256,(bytes32,bytes32,bytes32,bytes32),bytes[])
 PrankTest.testAddAsOwner(uint256)
 PrankTest.testAddStartPrank(uint256)
-PrankTest.testFailAddPrank(uint256)
 PrankTest.testSubtractAsTxOrigin(uint256,uint256)
 PrankTest.testSubtractFail(uint256)
 PrankTest.testSubtractStartPrank(uint256,uint256)
@@ -214,7 +189,6 @@ RecordLogsTest.testRecordLogs()
 RollTest.test_roll_setup()
 SafeTest.testWithdraw()
 SafeTest.testWithdrawFuzz(uint96)
-Setup2Test.testFail_setup()
 Setup2Test.test_setup()
 SetUpDeployTest.test_extcodesize()
 SetUpTest.testSetUpCalled()
@@ -236,46 +210,12 @@ StoreTest.testLoadNonExistent()
 StoreTest.testStoreLoad()
 StoreTest.testStoreLoadNonExistent()
 SymbolicStorageTest.testEmptyInitialStorage(uint256)
-SymbolicStorageTest.testFail_SymbolicStorage(uint256)
-SymbolicStorageTest.testFail_SymbolicStorage1(uint256)
 ToStringTest.testAddressToString()
 ToStringTest.testBoolToString()
 ToStringTest.testBytes32ToString()
 ToStringTest.testBytesToString()
 ToStringTest.testIntToString()
 ToStringTest.testUint256ToString()
-UintTypeTest.testFail_uint104(uint104)
-UintTypeTest.testFail_uint112(uint112)
-UintTypeTest.testFail_uint120(uint120)
-UintTypeTest.testFail_uint128(uint128)
-UintTypeTest.testFail_uint136(uint136)
-UintTypeTest.testFail_uint144(uint144)
-UintTypeTest.testFail_uint152(uint152)
-UintTypeTest.testFail_uint16(uint16)
-UintTypeTest.testFail_uint160(uint160)
-UintTypeTest.testFail_uint168(uint168)
-UintTypeTest.testFail_uint176(uint176)
-UintTypeTest.testFail_uint184(uint184)
-UintTypeTest.testFail_uint192(uint192)
-UintTypeTest.testFail_uint200(uint200)
-UintTypeTest.testFail_uint208(uint208)
-UintTypeTest.testFail_uint216(uint216)
-UintTypeTest.testFail_uint224(uint224)
-UintTypeTest.testFail_uint232(uint232)
-UintTypeTest.testFail_uint24(uint24)
-UintTypeTest.testFail_uint240(uint240)
-UintTypeTest.testFail_uint248(uint248)
-UintTypeTest.testFail_uint256(uint256)
-UintTypeTest.testFail_uint32(uint32)
-UintTypeTest.testFail_uint40(uint40)
-UintTypeTest.testFail_uint48(uint48)
-UintTypeTest.testFail_uint56(uint56)
-UintTypeTest.testFail_uint64(uint64)
-UintTypeTest.testFail_uint72(uint72)
-UintTypeTest.testFail_uint8(uint8)
-UintTypeTest.testFail_uint80(uint80)
-UintTypeTest.testFail_uint88(uint88)
-UintTypeTest.testFail_uint96(uint96)
 UintTypeTest.test_uint104(uint104)
 UintTypeTest.test_uint104_fail(uint104)
 UintTypeTest.test_uint112(uint112)
@@ -340,9 +280,6 @@ UintTypeTest.test_uint88_fail(uint88)
 UintTypeTest.test_uint8_fail(uint8)
 UintTypeTest.test_uint96(uint96)
 UintTypeTest.test_uint96_fail(uint96)
-IntTypeTest.testFail_uint128(uint128)
-IntTypeTest.testFail_uint256(uint256)
-IntTypeTest.testFail_uint64(uint64)
 IntTypeTest.test_uint128(uint128)
 IntTypeTest.test_uint128_fail(uint128)
 IntTypeTest.test_uint256(uint256)