Define post-state predicate foundry_test_success

[ehildenb]

Go to Discord channel and read the description provided by the devs there about post-state success.

Define in KEVM a new module FOUNDRY with foundry.md, which defines this predicate.

[ehildenb]

syntax Bool ::= foundry_test_success(StatusCode, ByteArray, Map) [function]

You might also just use a contextual function https://kframework.org/USER_MANUAL/#matching-global-context-in-function-rules:

syntax Bool ::= foundry_test_success() [function]

rule [[ foundry_test_success() => SVAL ==Int 0 ]]
       <statusCode> EVMC_SUCCESS </statusCode>
       <account>
           <acctID> FOUNDRY_ACCOUNT </acctID>
           <storage> ... SPECIAL_KEY |-> SVAL ... </storage>
           ...
       </account>

rule [[ foundry_test_success() => false ]]
       <statusCode> EVMC_REVERT </statusCode>

[ehildenb]

https://github.com/foundry-rs/foundry/blob/a4b04caf66643e42d3d2c10f9b9845b4bc0cb0d8/evm/src/executor/mod.rs#L460

Rust code implementing this.

[ehildenb]

@bjberg on Discord:

if the test reverts then it failed,
otherwise if a special storage slot on a specific address is not 0 (refer to code) it failed,
otherwise if a call to failed() on the test contract returns true, it failed (this call is allowed to revert, and if it does it is the same as the call returning false)

if the test starts with testFail this is inverted (i.e. where it would fail in a normal test it would pass, otherwise fail) 

[ehildenb]

Example integration:

diff --git a/kevm_pyk/src/kevm_pyk/solc_to_k.py b/kevm_pyk/src/kevm_pyk/solc_to_k.py
index b818a91a2..8d599c750 100644
--- a/kevm_pyk/src/kevm_pyk/solc_to_k.py
+++ b/kevm_pyk/src/kevm_pyk/solc_to_k.py
@@ -291,6 +291,7 @@ def gen_claims_for_contract(empty_config: KInner, contract_name: str, calldata_c
     else:
         init_terms = [(contract_name.lower(), init_term)]
     final_term = abstract_cell_vars(substitute(empty_config, final_subst))
+    final_term = mlAnd([final_term, KApply('foundry_test_success', [arguments])])
     claims: List[KClaim] = []
     for claim_id, i_term in init_terms:
         claim, _ = build_claim(claim_id, CTerm(i_term), CTerm(final_term))

[ehildenb]

Example of declaring special accounts:

diff --git a/kevm_pyk/src/kevm_pyk/kevm.py b/kevm_pyk/src/kevm_pyk/kevm.py
index 43bb79259..565c6ee5b 100644
--- a/kevm_pyk/src/kevm_pyk/kevm.py
+++ b/kevm_pyk/src/kevm_pyk/kevm.py
@@ -204,6 +204,19 @@ class KEVM(KProve):
                                     KApply('<origStorage>', [origStorage]),
                                     KApply('<nonce>', [nonce])])
 
+    @staticmethod
+    def foundry_account() -> KApply:
+        return KEVM.account_cell(encoding, intToken(0), .ByteArray, .Map, .Map, 0)
+
+    @staticmethod
+    def accounts(accts: List[KInner]) -> KApply:
+        accounts = KApply('.AccountCellMap')
+        if not accts:
+            return accounts
+        for i in reversed(accts):
+            accounts = KApply('_AccountCellMap_', [i, accounts])
+        return accounts
+
     @staticmethod
     def wordstack_len(constrainedTerm: KInner) -> int:
         return len(flattenLabel('_:__EVM-TYPES_WordStack_Int_WordStack', getCell(constrainedTerm, 'WORDSTACK_CELL')))
diff --git a/kevm_pyk/src/kevm_pyk/solc_to_k.py b/kevm_pyk/src/kevm_pyk/solc_to_k.py
index 1cdad8038..5282e9664 100644
--- a/kevm_pyk/src/kevm_pyk/solc_to_k.py
+++ b/kevm_pyk/src/kevm_pyk/solc_to_k.py
@@ -298,7 +298,7 @@ def gen_claims_for_contract(empty_config: KInner, contract_name: str, calldata_c
         'PC_CELL': intToken(0),
         'GAS_CELL': KEVM.inf_gas(KVariable('VGAS')),
         'K_CELL': KSequence([KEVM.execute(), KVariable('CONTINUATION')]),
-        'ACCOUNTS_CELL': KApply('_AccountCellMap_', [account_cell, KVariable('ACCOUNTS')]),
+        'ACCOUNTS_CELL': KEVM.accounts([account_cell, KEVM.foundry_account(), KEVM.foundry_magic_accounts(), KEVM.hardhat_account()])                                                                               
     }
     final_subst = {'K_CELL': KSequence([KEVM.halt(), KVariable('CONTINUATION')])}                                                                                                                                   
     init_term = substitute(empty_config, init_subst)
diff --git a/tests/foundry/foundry.k.check.expected b/tests/foundry/foundry.k.check.expected
index 10e98be6f..33b5d79cc 100644
--- a/tests/foundry/foundry.k.check.expected
+++ b/tests/foundry/foundry.k.check.expected
@@ -293,6 +293,23 @@ module TOKENTEST-BIN-RUNTIME-SPEC
                    </code>
                    ...
                  </account>
+                 <account>
+                   <accoutID>
+                     ENCODE("FOUNDRY_TEST_ACCOUNT")
+                   </accountID>
+                   <code>
+                     .ByteArray
+                   </code>
+                   <nonce>
+                     0                                                                                                                                                                                              
+                   </nonce>
+                   <storage>
+                     .Map
+                   </storage>
+                   <origStorage>
+                     .Map
+                   </origStorage>
+                 </account>
                  _ACCOUNTS ) => ?_ACCOUNTS_CELL_acd26fc5 )
                </accounts>
                <txOrder>