Add initial foundry.md

Makefile

@@ -176,6 +176,7 @@ kevm_files := abi.md              \
               evm.md              \
               evm-types.md        \
               evm-node.md         \
+              foundry.md          \
               hashed-locations.md \
               infinite-gas.md     \
               json-rpc.md         \
@@ -606,7 +607,7 @@ test-failure: $(failure_tests:=.run-expected)
 # kevm_pyk Tests
 
 kevm_pyk_tests :=                                           \
-                  tests/foundry/foundry.k.prove             \
+                  tests/foundry/kompiled/timestamp          \
                   tests/foundry/foundry.k.check             \
                   tests/specs/bihu/functional-spec.k.prove  \
                   tests/specs/examples/empty-bin-runtime.k  \

edsl.md

@@ -12,6 +12,7 @@ requires "hashed-locations.md"
 requires "abi.md"
 requires "infinite-gas.md"
 requires "optimizations.md"
+requires "foundry.md"
 
 module EDSL
     imports BUF
@@ -20,6 +21,7 @@ module EDSL
     imports EVM-OPTIMIZATIONS
     imports INFINITE-GAS
     imports BIN-RUNTIME
+    imports FOUNDRY
 endmodule
 
 module BIN-RUNTIME

foundry.md

@@ -0,0 +1,38 @@
+Foundry Specifications
+======================
+
+### Overview
+
+Foundry's testing framework provides a series of cheatcodes so that developers can specify what situation they want to test.
+This file describes the KEVM specification of the Foundry testing framework, which includes the definition of said cheatcodes and what does it mean for a test to pass.
+
+```k
+requires "evm.md"
+module FOUNDRY
+    imports FOUNDRY-SUCCESS
+    imports FOUNDRY-CHEAT-CODES
+endmodule
+```
+
+Foundry Success Predicate
+-------------------------
+
+```k
+module FOUNDRY-SUCCESS
+    imports EVM
+
+    syntax Bool ::= "foundry_success" "(" ")" [function, klabel(foundry_success), symbol]
+ // -------------------------------------------------------------------------------------
+    rule foundry_success() => false
+endmodule
+```
+
+Foundry Cheat Codes
+-------------------
+
+```k
+module FOUNDRY-CHEAT-CODES
+    imports EVM
+endmodule
+```
+

kevm_pyk/src/kevm_pyk/kevm.py

@@ -212,6 +212,10 @@ def wordstack_len(constrainedTerm: KInner) -> int:
     def parse_bytestack(s: KInner) -> KApply:
         return KApply('#parseByteStack(_)_SERIALIZATION_ByteArray_String', [s])
 
+    @staticmethod
+    def foundry_success() -> KApply:
+        return KApply('foundry_success')
+
     @staticmethod
     def intlist(ints: List[KInner]) -> KApply:
         res = KApply('.List{"___HASHED-LOCATIONS_IntList_Int_IntList"}_IntList')

kevm_pyk/src/kevm_pyk/solc_to_k.py

@@ -30,7 +30,7 @@
     KVariable,
 )
 from pyk.kastManip import abstract_term_safely, substitute
-from pyk.prelude import Sorts, intToken, stringToken
+from pyk.prelude import Sorts, intToken, mlEqualsTrue, stringToken
 from pyk.utils import FrozenDict, intersperse
 
 from .kevm import KEVM
@@ -294,10 +294,11 @@ def gen_claims_for_contract(empty_config: KInner, contract_name: str, calldata_c
         init_terms = [(f'{contract_name.lower()}-{i}', substitute(init_term, {'CALLDATA_CELL': cd})) for i, cd in enumerate(calldata_cells)]
     else:
         init_terms = [(contract_name.lower(), init_term)]
-    final_term = abstract_cell_vars(substitute(empty_config, final_subst))
+    final_cterm = CTerm(abstract_cell_vars(substitute(empty_config, final_subst)))
+    final_cterm = final_cterm.add_constraint(mlEqualsTrue(KEVM.foundry_success()))
     claims: List[KClaim] = []
     for claim_id, i_term in init_terms:
-        claim, _ = build_claim(claim_id, CTerm(i_term), CTerm(final_term))
+        claim, _ = build_claim(claim_id, CTerm(i_term), final_cterm)
         claims.append(claim)
     return claims
 

tests/foundry/foundry.k.check.expected

@@ -307,6 +307,7 @@ module TOKENTEST-BIN-RUNTIME-SPEC
              </network>
            </ethereum>
          </kevm>
+       ensures foundry_success ( )
       [label(tokentest-0)]
 
     claim [tokentest-1]: <kevm>
@@ -498,6 +499,7 @@ module TOKENTEST-BIN-RUNTIME-SPEC
              </network>
            </ethereum>
          </kevm>
+       ensures foundry_success ( )
       [label(tokentest-1)]
 
 endmodule