Small fixes to kevm-pyk library (#1462)

* kevm-pyk/kevm: correct klabel name

* .github/solc_to_k: correct klabel usage

* kevm-pyk/{kevm,solc-to-k}: correct some KTokens and fill in details

* kevm-pyk/solc_to_k: more KToken => KApply corrections

Author: ehildenb

kevm-pyk/src/kevm_pyk/kevm.py

@@ -368,14 +368,26 @@ def _patch_symbol_table(symbol_table: Dict[str, Any]) -> None:
 
     @staticmethod
     def success(s: KInner, dst: KInner, r: KInner, c: KInner) -> KApply:
-        return KApply('foundry_success ', [s, dst, r, c])
+        return KApply('foundry_success', [s, dst, r, c])
 
     @staticmethod
     def fail(s: KInner, dst: KInner, r: KInner, c: KInner) -> KApply:
         return notBool(Foundry.success(s, dst, r, c))
 
     # address(uint160(uint256(keccak256("foundry default caller"))))
 
+    @staticmethod
+    def loc_FOUNDRY_FAILED() -> KApply:  # noqa: N802
+        return KEVM.loc(
+            KApply(
+                'contract_access_field',
+                [
+                    KApply('FoundryCheat_FOUNDRY-ACCOUNTS_FoundryContract'),
+                    KApply('Failed_FOUNDRY-ACCOUNTS_FoundryField'),
+                ],
+            )
+        )
+
     @staticmethod
     def address_CALLER() -> KToken:  # noqa: N802
         return intToken(0x1804C8AB1F12E6BBF3894D4083F33E07309D1F38)

kevm-pyk/src/kevm_pyk/solc_to_k.py

@@ -10,17 +10,7 @@
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KAtt, KInner, KLabel, KRewrite, KSequence, KSort, KVariable, build_assoc
 from pyk.kast.manip import abstract_term_safely, substitute
-from pyk.kast.outer import (
-    KFlatModule,
-    KImport,
-    KNonTerminal,
-    KProduction,
-    KProductionItem,
-    KRule,
-    KSentence,
-    KTerminal,
-    KToken,
-)
+from pyk.kast.outer import KFlatModule, KImport, KNonTerminal, KProduction, KProductionItem, KRule, KSentence, KTerminal
 from pyk.kcfg import KCFG
 from pyk.prelude.kbool import FALSE, TRUE, andBool, notBool
 from pyk.prelude.kint import intToken
@@ -337,11 +327,10 @@ def method_to_cfg(empty_config: KInner, contract: Contract, method: Contract.Met
 
 
 def _init_cterm(init_term: KInner) -> CTerm:
-    key_dst = KEVM.loc(KToken('FoundryCheat . Failed', 'ContractAccess'))
-    dst_failed_prev = KEVM.lookup(KVariable('CHEATCODE_STORAGE'), key_dst)
+    dst_failed_prev = KEVM.lookup(KVariable('CHEATCODE_STORAGE'), Foundry.loc_FOUNDRY_FAILED())
     init_cterm = CTerm(init_term)
     init_cterm = KEVM.add_invariant(init_cterm)
-    init_cterm = init_cterm.add_constraint(mlEqualsTrue(KApply('_==Int_', [dst_failed_prev, KToken('0', 'Int')])))
+    init_cterm = init_cterm.add_constraint(mlEqualsTrue(KApply('_==Int_', [dst_failed_prev, intToken(0)])))
     return init_cterm
 
 
@@ -389,10 +378,10 @@ def _init_term(
             ),
         ),
         'LOCALMEM_CELL': KApply('.Memory_EVM-TYPES_Memory'),
-        'PREVCALLER_CELL': KToken('.Account', 'K'),
-        'PREVORIGIN_CELL': KToken('.Account', 'K'),
-        'NEWCALLER_CELL': KToken('.Account', 'K'),
-        'NEWORIGIN_CELL': KToken('.Account', 'K'),
+        'PREVCALLER_CELL': KApply('.Account_EVM-TYPES_Account'),
+        'PREVORIGIN_CELL': KApply('.Account_EVM-TYPES_Account'),
+        'NEWCALLER_CELL': KApply('.Account_EVM-TYPES_Account'),
+        'NEWORIGIN_CELL': KApply('.Account_EVM-TYPES_Account'),
         'ACTIVE_CELL': FALSE,
         'STATIC_CELL': FALSE,
         'MEMORYUSED_CELL': intToken(0),
@@ -412,10 +401,10 @@ def _init_term(
         'SINGLECALL_CELL': FALSE,
         'EXPECTEDREVERT_CELL': FALSE,
         'ISOPCODEEXPECTED_CELL': FALSE,
-        'EXPECTEDADDRESS_CELL': KToken('.Account', 'K'),
+        'EXPECTEDADDRESS_CELL': KApply('.Account_EVM-TYPES_Account'),
         'EXPECTEDVALUE_CELL': intToken(0),
-        'EXPECTEDDATA_CELL': KToken('.ByteArray', 'K'),
-        'OPCODETYPE_CELL': KToken('.OpcodeType', 'K'),
+        'EXPECTEDDATA_CELL': KApply('.ByteArray_EVM-TYPES_ByteArray'),
+        'OPCODETYPE_CELL': KApply('.OpcodeType_FOUNDRY-CHEAT-CODES_OpcodeType'),
     }
 
     if calldata is not None:
@@ -429,8 +418,7 @@ def _init_term(
 
 def _final_cterm(empty_config: KInner, contract_name: str, *, failing: bool, is_test: bool = True) -> CTerm:
     final_term = _final_term(empty_config, contract_name)
-    key_dst = KEVM.loc(KToken('FoundryCheat . Failed', 'ContractAccess'))
-    dst_failed_post = KEVM.lookup(KVariable('CHEATCODE_STORAGE_FINAL'), key_dst)
+    dst_failed_post = KEVM.lookup(KVariable('CHEATCODE_STORAGE_FINAL'), Foundry.loc_FOUNDRY_FAILED())
     foundry_success = Foundry.success(
         KVariable('STATUSCODE_FINAL'),
         dst_failed_post,